Skip to content

Fix Z3 bound variable substitution #535

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Fix Z3 bound variable substitution #535

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
85ce8e0
Add tests for quantifier visitation/variable extraction in SolverVisi…
Oct 15, 2025
c415834
Z3 visitor: reverse order of bound variables in the visitor, as they …
Oct 15, 2025
a0c62e9
Access BitvectorType directly in SolverVisitorTest.java
Oct 16, 2025
b54cb3b
Access getBitvectorTypeWithSize() directly from FormulaType instead o…
Oct 16, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
87 changes: 87 additions & 0 deletions src/org/sosy_lab/java_smt/test/SolverVisitorTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.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
}
}
}