Add tests for quantifier visitation/variable extraction in SolverVisitorTest with more than one bound variable

Author: BaierD

src/org/sosy_lab/java_smt/test/SolverVisitorTest.java

@@ -1610,4 +1610,91 @@ public void testSl() throws SolverException, InterruptedException {
     assertThat(f2).isEqualTo(f);
     assertThatFormula(f).isEquivalentTo(f2);
   }
+
+  @Test
+  public void testQuantifierAndBoundVariablesWithIntegers() {
+    requireQuantifiers();
+    requireArrays();
+    requireIntegers();
+    requireVisitor();
+
+    IntegerFormula four = imgr.makeNumber(4);
+    IntegerFormula var1 = imgr.makeVariable("var1");
+    IntegerFormula var2 = imgr.makeVariable("var2");
+    IntegerFormula var3 = imgr.makeVariable("var3");
+
+    ArrayFormula<IntegerFormula, IntegerFormula> array1 =
+        amgr.makeArray("array1", FormulaType.IntegerType, FormulaType.IntegerType);
+    ArrayFormula<IntegerFormula, IntegerFormula> array2 =
+        amgr.makeArray("array2", FormulaType.IntegerType, FormulaType.IntegerType);
+
+    IntegerFormula bvIndex = imgr.add(var2, imgr.multiply(four, var1));
+    BooleanFormula body = amgr.equivalence(array2, amgr.store(array1, bvIndex, var3));
+
+    List<? extends Formula> freeVars = ImmutableList.of(var2, var3, array2);
+    List<? extends Formula> boundVars = ImmutableList.of(var1, array1);
+    List<? extends Formula> allVars = ImmutableList.of(var1, var2, var3, array1, array2);
+    Map<String, Formula> variablesInBody = mgr.extractVariables(body);
+    assertThat(variablesInBody.values()).containsExactlyElementsIn(allVars);
+
+    for (Quantifier quantifier : Quantifier.values()) {
+      BooleanFormula quantifiedFormula = qmgr.mkQuantifier(quantifier, boundVars, body);
+
+      Map<String, Formula> variablesInQuantifiedFormula = mgr.extractVariables(quantifiedFormula);
+      Map<String, Formula> variablesAndUFsInQuantifiedFormula =
+          mgr.extractVariablesAndUFs(quantifiedFormula);
+
+      assertThat(variablesAndUFsInQuantifiedFormula).isEqualTo(variablesInQuantifiedFormula);
+      assertThat(variablesInQuantifiedFormula.values()).containsExactlyElementsIn(freeVars);
+      assertThat(variablesInQuantifiedFormula.values()).containsNoneIn(boundVars);
+
+      // TODO: add collection of bound variables through new visitor implementation and test
+      //  failure of the old
+    }
+  }
+
+  @Test
+  public void testQuantifierAndBoundVariablesWithBitvectors() {
+    requireQuantifiers();
+    requireArrays();
+    requireBitvectors();
+    requireVisitor();
+
+    int bvLen = 32;
+    BitvectorType bvType = FormulaType.BitvectorType.getBitvectorTypeWithSize(bvLen);
+
+    BitvectorFormula four = bvmgr.makeBitvector(bvLen, 4);
+    BitvectorFormula var1 = bvmgr.makeVariable(bvType, "var1");
+    BitvectorFormula var2 = bvmgr.makeVariable(bvType, "var2");
+    BitvectorFormula var3 = bvmgr.makeVariable(bvType, "var3");
+
+    ArrayFormula<BitvectorFormula, BitvectorFormula> array1 =
+        amgr.makeArray("array1", bvType, bvType);
+    ArrayFormula<BitvectorFormula, BitvectorFormula> array2 =
+        amgr.makeArray("array2", bvType, bvType);
+
+    BitvectorFormula bvIndex = bvmgr.add(var2, bvmgr.multiply(four, var1));
+    BooleanFormula body = amgr.equivalence(array2, amgr.store(array1, bvIndex, var3));
+
+    List<? extends Formula> freeVars = ImmutableList.of(var2, var3, array2);
+    List<? extends Formula> boundVars = ImmutableList.of(var1, array1);
+    List<? extends Formula> allVars = ImmutableList.of(var1, var2, var3, array1, array2);
+    Map<String, Formula> variablesInBody = mgr.extractVariables(body);
+    assertThat(variablesInBody.values()).containsExactlyElementsIn(allVars);
+
+    for (Quantifier quantifier : Quantifier.values()) {
+      BooleanFormula quantifiedFormula = qmgr.mkQuantifier(quantifier, boundVars, body);
+
+      Map<String, Formula> variablesInQuantifiedFormula = mgr.extractVariables(quantifiedFormula);
+      Map<String, Formula> variablesAndUFsInQuantifiedFormula =
+          mgr.extractVariablesAndUFs(quantifiedFormula);
+
+      assertThat(variablesAndUFsInQuantifiedFormula).isEqualTo(variablesInQuantifiedFormula);
+      assertThat(variablesInQuantifiedFormula.values()).containsExactlyElementsIn(freeVars);
+      assertThat(variablesInQuantifiedFormula.values()).containsNoneIn(boundVars);
+
+      // TODO: add collection of bound variables through new visitor implementation and test
+      //  failure of the old
+    }
+  }
 }