From 85ce8e0f1c7c608eb558fd73b2bf37e817c056e1 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 15 Oct 2025 23:25:20 +0200 Subject: [PATCH 1/4] Add tests for quantifier visitation/variable extraction in SolverVisitorTest with more than one bound variable --- .../java_smt/test/SolverVisitorTest.java | 87 +++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 491ef036fa..16ec6bb906 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/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 array1 = + amgr.makeArray("array1", FormulaType.IntegerType, FormulaType.IntegerType); + ArrayFormula 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 freeVars = ImmutableList.of(var2, var3, array2); + List boundVars = ImmutableList.of(var1, array1); + List allVars = ImmutableList.of(var1, var2, var3, array1, array2); + Map variablesInBody = mgr.extractVariables(body); + assertThat(variablesInBody.values()).containsExactlyElementsIn(allVars); + + for (Quantifier quantifier : Quantifier.values()) { + BooleanFormula quantifiedFormula = qmgr.mkQuantifier(quantifier, boundVars, body); + + Map variablesInQuantifiedFormula = mgr.extractVariables(quantifiedFormula); + Map 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 array1 = + amgr.makeArray("array1", bvType, bvType); + ArrayFormula 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 freeVars = ImmutableList.of(var2, var3, array2); + List boundVars = ImmutableList.of(var1, array1); + List allVars = ImmutableList.of(var1, var2, var3, array1, array2); + Map variablesInBody = mgr.extractVariables(body); + assertThat(variablesInBody.values()).containsExactlyElementsIn(allVars); + + for (Quantifier quantifier : Quantifier.values()) { + BooleanFormula quantifiedFormula = qmgr.mkQuantifier(quantifier, boundVars, body); + + Map variablesInQuantifiedFormula = mgr.extractVariables(quantifiedFormula); + Map 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 + } + } } From c4158341649661ed939e0ef4ca98a1a3fd4c8213 Mon Sep 17 00:00:00 2001 From: BaierD Date: Wed, 15 Oct 2025 23:31:57 +0200 Subject: [PATCH 2/4] Z3 visitor: reverse order of bound variables in the visitor, as they are instantiated reversed --- src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index edd4da657d..f40446e8b8 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -588,8 +588,11 @@ private R visitQuantifier(FormulaVisitor 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; From a0c62e92524715526220b958973d6b7aee7f9100 Mon Sep 17 00:00:00 2001 From: BaierD Date: Thu, 16 Oct 2025 09:46:19 +0200 Subject: [PATCH 3/4] Access BitvectorType directly in SolverVisitorTest.java --- src/org/sosy_lab/java_smt/test/SolverVisitorTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 16ec6bb906..4ed57deb77 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -1661,7 +1661,7 @@ public void testQuantifierAndBoundVariablesWithBitvectors() { requireVisitor(); int bvLen = 32; - BitvectorType bvType = FormulaType.BitvectorType.getBitvectorTypeWithSize(bvLen); + BitvectorType bvType = BitvectorType.getBitvectorTypeWithSize(bvLen); BitvectorFormula four = bvmgr.makeBitvector(bvLen, 4); BitvectorFormula var1 = bvmgr.makeVariable(bvType, "var1"); From b54cb3b6bcdf5b4896bbcd20c0419ec630d229e0 Mon Sep 17 00:00:00 2001 From: BaierD Date: Thu, 16 Oct 2025 09:49:26 +0200 Subject: [PATCH 4/4] Access getBitvectorTypeWithSize() directly from FormulaType instead of BitvectorType in SolverVisitorTest.java --- src/org/sosy_lab/java_smt/test/SolverVisitorTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 4ed57deb77..bb2bd14f3d 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -1661,7 +1661,7 @@ public void testQuantifierAndBoundVariablesWithBitvectors() { requireVisitor(); int bvLen = 32; - BitvectorType bvType = BitvectorType.getBitvectorTypeWithSize(bvLen); + BitvectorType bvType = FormulaType.getBitvectorTypeWithSize(bvLen); BitvectorFormula four = bvmgr.makeBitvector(bvLen, 4); BitvectorFormula var1 = bvmgr.makeVariable(bvType, "var1");