fix issue 293 involving evaluation of CHOOSE expressions

by detecting quantified variables

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

src/main/java/de/tla2bAst/ExpressionTranslator.java

@@ -215,6 +215,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 		TreeNode expr = n_operatorDefintion.heirs()[2];
 		searchVarInSyntaxTree(expr);
         
+        // this code seems to assume that there is no variable clash between outer and nested variables
 		for (int i = 0; i < noVariables.size(); i++) {
 			variables.remove(noVariables.get(i));
 		}
@@ -273,10 +274,23 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 			noVariables.add(treeNode.heirs()[0].getImage());
 			break;
 		}
-		case N_UnboundQuant: {
+		case N_UnboundQuant: { // TOOD: check: is this an unbounded quantifier with infinite domain or a quantifier that does not hide the quantified variables?
 			TreeNode[] children = treeNode.heirs();
 			for (int i = 1; i < children.length - 2; i = i + 2) {
-				// System.out.println(children[i].getImage());
+			   // System.out.println("N_UnboundQuant: "+children[i].getImage());
+			}
+			searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
+			break;
+		}
+		case N_UnboundOrBoundChoose: { // not sure the format is the same as N_QuantBound
+			TreeNode[] children = treeNode.heirs();
+			for (int i = 1; i < children.length - 2; i = i + 2) {
+				String boundedVar = children[i].getImage();
+				// typically children[i+1] is N_MaybeBound
+				if (!noVariables.contains(boundedVar)) {
+					noVariables.add(boundedVar);
+					//System.out.println("CHOOSE quantified variable: " + boundedVar);
+				}
 			}
 			searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);
 			break;
@@ -287,6 +301,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 				String boundedVar = children[i].getImage();
 				if (!noVariables.contains(boundedVar)) {
 					noVariables.add(boundedVar);
+					// System.out.println("N_QuantBound: locally quantified variable" + boundedVar);
 				}
 			}
 			searchVarInSyntaxTree(treeNode.heirs()[children.length - 1]);

src/test/java/de/tla2b/expression/ComplexExpressionTest.java

@@ -74,5 +74,15 @@ public class ComplexExpressionTest {
 				"r = [a |-> [x|->1,y|->TRUE], b |-> 1] "
 						+ "/\\ r2 = [r EXCEPT !.a.x = 2]");
 	}
+	@Test
+	public void testConstraint1() throws Exception {
+		compareExpr("x**3 - 20*x**2 + 7*x = 14388",
+				    "x^3 - 20*x^2 + 7*x = 14388");
+	}
+	@Test
+	public void testConstraintCHOOSE() throws Exception {
+		compareExpr("CHOOSE({x|x:0..100 & x**3 - 20*x**2 + 7*x = 14388})",
+				    "CHOOSE x \\in 0..100: x^3 - 20*x^2 + 7*x = 14388");
+	}
 
 }