Merge pull request #535 from sosy-lab/fix_Z3_bound_variable_substitution

Fix Z3 bound variable substitution

Author: baierd

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

@@ -588,8 +588,11 @@ private <R> R visitQuantifier(FormulaVisitor<R> pVisitor, BooleanFormula pFormul
     int numBound = Native.getQuantifierNumBound(environment, pF);
     long[] freeVars = new long[numBound];
     for (int i = 0; i < numBound; i++) {
-      long varName = Native.getQuantifierBoundName(environment, pF, i);
-      long varSort = Native.getQuantifierBoundSort(environment, pF, i);
+      // The indices are reversed according to
+      //  https://github.com/Z3Prover/z3/issues/7970#issuecomment-3407924907
+      int inverseIndex = numBound - 1 - i;
+      long varName = Native.getQuantifierBoundName(environment, pF, inverseIndex);
+      long varSort = Native.getQuantifierBoundSort(environment, pF, inverseIndex);
       long freeVar = Native.mkConst(environment, varName, varSort);
       Native.incRef(environment, freeVar);
       freeVars[i] = freeVar;

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

@@ -1661,4 +1661,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.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
+    }
+  }
 }