From 465cd4287212926c59e90036534c37b16e3f416d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 28 Oct 2025 19:04:33 +0100 Subject: [PATCH 1/9] Bitwuzla: Fix array value generation in the model Ported from CVC5, see 0d463c83410a332ed81ff4f7628d25ae729b3782 --- .../solvers/bitwuzla/BitwuzlaModel.java | 165 +++++++++--------- 1 file changed, 81 insertions(+), 84 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java index 722fcaf05f..a02e38f4ec 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java @@ -9,21 +9,21 @@ package org.sosy_lab.java_smt.solvers.bitwuzla; import com.google.common.base.Preconditions; +import com.google.common.collect.FluentIterable; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Collection; import java.util.Deque; -import java.util.HashSet; import java.util.List; -import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.java_smt.basicimpl.AbstractModel; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Kind; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Sort; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Term; +import org.sosy_lab.java_smt.solvers.bitwuzla.api.TermManager; import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Term; class BitwuzlaModel extends AbstractModel { @@ -82,7 +82,7 @@ public ImmutableList asList() { variablesBuilder.add(getSimpleAssignment(term)); } else if (sort.is_array() && term.is_const()) { - variablesBuilder.addAll(getArrayAssignment(term)); + variablesBuilder.addAll(buildArrayAssignment(term, bitwuzlaEnv.get_value(term))); } else { for (Term child : children) { @@ -108,94 +108,91 @@ private ValueAssignment getSimpleAssignment(Term pTerm) { argumentInterpretation); } - private Collection getArrayAssignment(Term pTerm) { - return getArrayAssignments(pTerm, ImmutableList.of()); + /** Takes a (nested) select statement and returns its indices. */ + private Iterable getArgs(Term array) { + if (array.kind().equals(Kind.ARRAY_SELECT)) { + return FluentIterable.concat(getArgs(array.get(0)), ImmutableList.of(array.get(1))); + } else { + return ImmutableList.of(); + } } - // TODO: check this in detail. I think this might be incomplete. - // We should add more Model tests in general. As most are parsing and int based! - private Collection getArrayAssignments(Term pTerm, List upperIndices) { - // Array children for store are structured in the following way: - // {starting array, index, value} in "we add value at index to array" - // Selections are structured: {starting array, index} - // Just declared (empty) arrays return an empty array - - // Example Formula: (SELECT ARRAY INDEX) - // new ValueAssignment((SELECT ARRAY INDEX), value formula of INDEX, (SELECT ARRAY INDEX) = - // value of index, name of INDEX, actual java value of index, {return java value of the - // formula}) - - // TODO: Array equals value - Term array = pTerm; - Collection assignments = new ArrayList<>(); - Set indices = new HashSet<>(); - while (array.sort().is_array()) { - // Here we either have STORE; SELECT or an empty Array - Vector_Term children = array.children(); - List innerIndices = new ArrayList<>(upperIndices); - String name = getArrayName(array); - Preconditions.checkNotNull(name, "unexpected array %s without name", array); - if (children.isEmpty()) { - // Empty array - return assignments; - } else if (children.size() == 2) { - // SELECT expression - Term index = children.get(1); - if (!indices.add(index)) { - continue; - } - - Term indexValue = bitwuzlaEnv.get_value(index); - innerIndices.add(evaluateImpl(indexValue)); - - // The value of an SELECT is equal to the content - Term valueTerm = bitwuzlaEnv.get_value(array); - - assignments.add( - new ValueAssignment( - bitwuzlaCreator.encapsulateWithTypeOf(array), - bitwuzlaCreator.encapsulateWithTypeOf(valueTerm), - creator.encapsulateBoolean(buildEqForTwoTerms(array, valueTerm)), - name, - evaluateImpl(valueTerm), - innerIndices)); - array = children.get(0); + /** Takes a select statement with multiple indices and returns the variable name at the bottom. */ + private String getVar(Term array) { + if (array.kind().equals(Kind.ARRAY_SELECT)) { + return getVar(array.get(0)); + } else { + return array.symbol(); + } + } + /** Build assignment for an array value. */ + private Iterable buildArrayAssignment(Term expr, Term value) { + // Bitwuzla returns values such as "(Store (Store ... i1,1 e1,1) i1,0 e1,0)" where the i1,x + // match the first index of the array and the elements e1,Y can again be arrays (if there is + // more than one index). We need "pattern match" this values to extract assignments from it. + // Initially we have: + // arr = (Store (Store ... i1,1 e1,1) i1,0 e1,0) + // where 'arr' is the name of the variable. By applying (Select i1,0 ...) to both side we get: + // (Select i1,0 arr) = (Select i1,0 (Store (Store ... i1,1 e1,1) i1,0 e1,0)) + // The right side simplifies to e1,0 as the index matches. We need to continue with this for + // all other matches to the first index, that is + // (Select i1,1 arr) = (Select i1,0 (Store (Store ... i1,1 e1,1) i1,0 e1,0)) + // = (Select i1,0 (Store ... i1,1 e1,1)) + // = e1,1 + // until all matches are explored and the bottom of the Store chain is reached. If the array + // has more than one dimension we also have to descend into the elements to apply the next + // index there. For instance, let's consider a 2-dimensional array with type (Array Int -> + // (Array Int -> Int)). After matching the first index just as in the above example we might + // have: + // (Select i1,0 arr) = (Select i1,0 (Store (Store ... i1,1 e1,1) i1,0 e1,0)) = e1,0 + // In this case e1,0 is again a Store chain, let's say e1,0 := (Store (Store ... i2,1 e2,1) + // i2,0 e2,0), and we now continue with the second index: + // (Select i2,1 (Select i1,0 arr)) = (Select i2,1 (Store (Store ... i2,1 e2,1) i2,0 e2,0)) = + // = e2,1 + // This again has to be done for all possible matches. + // Once we've reached the last index, the successor element will be a non-array value. We + // then create the final assignments and return: + // (Select iK,mK ... (Select i2,1 (Select i1,0 arr)) = eik,mK + if (value.kind().equals(Kind.ARRAY_STORE)) { + // This is a Store node for the current index. We need to follow the chain downwards to + // match this index, while also exploring the successor for the other indices + Term index = value.get(1); + Term element = value.get(2); + + TermManager termManager = bitwuzlaCreator.getTermManager(); + Term select = termManager.mk_term(Kind.ARRAY_SELECT, expr, index); + + Iterable current; + if (expr.sort().array_element().is_array()) { + current = buildArrayAssignment(select, element); } else { - // STORE expression - assert children.size() == 3; - Term index = children.get(1); - Term content = children.get(2); - - if (!indices.add(index)) { - continue; - } - - Term indexValue = bitwuzlaEnv.get_value(index); - Term contentValue = bitwuzlaEnv.get_value(content); - innerIndices.add(evaluateImpl(indexValue)); - assignments.add( - new ValueAssignment( - bitwuzlaCreator.encapsulateWithTypeOf(array), - bitwuzlaCreator.encapsulateWithTypeOf(content), - creator.encapsulateBoolean(buildEqForTwoTerms(array, contentValue)), - name, - evaluateImpl(contentValue), - innerIndices)); - - array = children.get(0); - assignments.addAll(getArrayAssignments(array, innerIndices)); + Term equation = termManager.mk_term(Kind.EQUAL, select, element); + + current = + FluentIterable.of( + new ValueAssignment( + creator.encapsulate(creator.getFormulaType(element), select), + creator.encapsulate(creator.getFormulaType(element), element), + creator.encapsulateBoolean(equation), + getVar(expr), + creator.convertValue(element, element), + FluentIterable.from(getArgs(select)) + .transform(creator::convertValue) + .toList())); } - } - return assignments; - } + return FluentIterable.concat(current, buildArrayAssignment(expr, value.get(0))); + + } else if (value.kind().equals(Kind.CONST_ARRAY)) { + // We've reached the end of the Store chain + return ImmutableList.of(); - private String getArrayName(Term array) { - String name = array.symbol(); - if (name != null) { - return name; + } else { + // Should be unreachable + // We assume that array values are made up of "const" and "store" nodes with non-array + // constants as leaves + throw new AssertionError(); } - return getArrayName(array.get(0)); } private Term buildEqForTwoTerms(Term left, Term right) { From d9944675664003900661c300aab240e30543a33d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 28 Oct 2025 19:08:07 +0100 Subject: [PATCH 2/9] Bitwuzla: Disable a test as Bitwuzla is too slow --- src/org/sosy_lab/java_smt/test/ModelTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 40213bd4e0..ba7cd216c9 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -2243,7 +2243,7 @@ public void arrayTest5() assume() .withMessage("Solver is quite slow for this example") .that(solverToUse()) - .isNotEqualTo(Solvers.PRINCESS); + .isNoneOf(Solvers.PRINCESS, Solvers.BITWUZLA); BooleanFormula formula = context From 68cb59c25f0da60312cea0c0f70bf88e9bf89274 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 16 Sep 2025 14:28:50 +0200 Subject: [PATCH 3/9] Add tests for array and Uf values in the model --- src/org/sosy_lab/java_smt/test/ModelTest.java | 379 ++++++++++++++++++ 1 file changed, 379 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index ba7cd216c9..20ade77d57 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -16,7 +16,9 @@ import static org.sosy_lab.java_smt.api.FormulaType.IntegerType; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; +import com.google.common.collect.FluentIterable; import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; import com.google.common.collect.Iterables; import java.io.IOException; import java.math.BigInteger; @@ -24,6 +26,7 @@ import java.nio.file.Path; import java.util.ArrayList; import java.util.List; +import java.util.Map; import java.util.function.Function; import java.util.stream.Collectors; import org.checkerframework.checker.nullness.qual.Nullable; @@ -42,6 +45,7 @@ import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.FunctionDeclarationKind; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; @@ -49,6 +53,7 @@ import org.sosy_lab.java_smt.api.ProverEnvironment; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; /** Test that values from models are appropriately parsed. */ public class ModelTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -2254,6 +2259,380 @@ public void arrayTest5() checkModelIteration(formula, false); } + /** Returns the arguments of an UF or array definition from the model. */ + private Iterable getFunctionArgs(Formula f) { + requireVisitor(); + return mgr.visit( + f, + new DefaultFormulaVisitor<>() { + @Override + protected Iterable visitDefault(Formula f) { + throw new IllegalArgumentException(); + } + + @Override + public Iterable visitFreeVariable(Formula f, String name) { + // Base case for array values + return ImmutableList.of(); + } + + @Override + public Iterable visitFunction( + Formula f, List args, FunctionDeclaration functionDeclaration) { + if (functionDeclaration.getKind().equals(FunctionDeclarationKind.SELECT)) { + return FluentIterable.concat( + getFunctionArgs(args.get(0)), ImmutableList.of(args.get(1))); + } else { + // Assume its an UF value + return args; + } + } + }); + } + + /** Evaluate the UF or array constraint and check that the model contains the expected values. */ + private void checkModelContains( + BooleanFormula pFormula, String pVar, Map, Formula> expected) { + try (var prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + prover.addConstraint(pFormula); + assertThat(prover.isUnsat()).isFalse(); + + ImmutableMap.Builder, Formula> builder = ImmutableMap.builder(); + for (var assignment : prover.getModel().asList()) { + if (assignment.getName().equals(pVar)) { + builder.put( + ImmutableList.copyOf(getFunctionArgs(assignment.getKey())), + assignment.getValueAsFormula()); + } + } + var model = builder.build(); + assertThat(model).containsAtLeastEntriesIn(expected); + + } catch (SolverException | InterruptedException e) { + throw new RuntimeException(e); + } + } + + @Test + public void testArray1Bv() { + requireArrays(); + requireBitvectors(); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var array = amgr.makeArray("array", bitvectorType, bitvectorType); + + var idx = bvmgr.makeBitvector(8, 1); + var val = bvmgr.makeBitvector(8, 10); + + checkModelContains( + bvmgr.equal(amgr.select(array, idx), val), + "array", + ImmutableMap.of(ImmutableList.of(idx), val)); + } + + @Test + public void testArray2Bv() { + requireArrays(); + requireBitvectors(); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var array = amgr.makeArray("array", bitvectorType, bitvectorType); + + var idxA = bvmgr.makeBitvector(8, 1); + var valA = bvmgr.makeBitvector(8, 10); + + var idxB = bvmgr.makeBitvector(8, 2); + var valB = bvmgr.makeBitvector(8, 5); + + checkModelContains( + bmgr.and( + bvmgr.equal(amgr.select(array, idxA), valA), + bvmgr.equal(amgr.select(array, idxB), valB)), + "array", + ImmutableMap.of(ImmutableList.of(idxA), valA, ImmutableList.of(idxB), valB)); + } + + @Test + public void testArray1BvBV() { + requireArrays(); + requireBitvectors(); + + // Boolector doesn't support multiple indices + assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var array = + amgr.makeArray( + "array", bitvectorType, FormulaType.getArrayType(bitvectorType, bitvectorType)); + + var idxA = bvmgr.makeBitvector(8, 1); + var idxB = bvmgr.makeBitvector(8, 7); + var val = bvmgr.makeBitvector(8, 10); + + checkModelContains( + bvmgr.equal(amgr.select(amgr.select(array, idxA), idxB), val), + "array", + ImmutableMap.of(ImmutableList.of(idxA, idxB), val)); + } + + @Test + public void testArray2BvBv() { + requireArrays(); + requireBitvectors(); + + // Boolector doesn't support multiple indices + assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var array = + amgr.makeArray( + "array", bitvectorType, FormulaType.getArrayType(bitvectorType, bitvectorType)); + + var idxA1 = bvmgr.makeBitvector(8, 1); + var idxA2 = bvmgr.makeBitvector(8, 7); + var valA = bvmgr.makeBitvector(8, 10); + + var idxB1 = bvmgr.makeBitvector(8, 3); + var idxB2 = bvmgr.makeBitvector(8, 2); + var valB = bvmgr.makeBitvector(8, 5); + + checkModelContains( + bmgr.and( + bvmgr.equal(amgr.select(amgr.select(array, idxA1), idxA2), valA), + bvmgr.equal(amgr.select(amgr.select(array, idxB1), idxB2), valB)), + "array", + ImmutableMap.of( + ImmutableList.of(idxA1, idxA2), valA, ImmutableList.of(idxB1, idxB2), valB)); + } + + @Test + public void testUf1Bv() { + requireBitvectors(); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var uf = fmgr.declareUF("uf", bitvectorType, bitvectorType); + + var idx = bvmgr.makeBitvector(8, 1); + var val = bvmgr.makeBitvector(8, 10); + + checkModelContains( + bvmgr.equal(fmgr.callUF(uf, idx), val), "uf", ImmutableMap.of(ImmutableList.of(idx), val)); + } + + @Test + public void testUf2Bv() { + requireBitvectors(); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var uf = fmgr.declareUF("uf", bitvectorType, bitvectorType); + + var idxA = bvmgr.makeBitvector(8, 1); + var valA = bvmgr.makeBitvector(8, 10); + + var idxB = bvmgr.makeBitvector(8, 2); + var valB = bvmgr.makeBitvector(8, 5); + + checkModelContains( + bmgr.and( + bvmgr.equal(fmgr.callUF(uf, idxA), valA), bvmgr.equal(fmgr.callUF(uf, idxB), valB)), + "uf", + ImmutableMap.of(ImmutableList.of(idxA), valA, ImmutableList.of(idxB), valB)); + } + + @Test + public void testUf1BvBV() { + requireBitvectors(); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var uf = fmgr.declareUF("uf", bitvectorType, bitvectorType, bitvectorType); + + var idxA = bvmgr.makeBitvector(8, 1); + var idxB = bvmgr.makeBitvector(8, 7); + var val = bvmgr.makeBitvector(8, 10); + + checkModelContains( + bvmgr.equal(fmgr.callUF(uf, idxA, idxB), val), + "uf", + ImmutableMap.of(ImmutableList.of(idxA, idxB), val)); + } + + @Test + public void testUf2BvBv() { + requireBitvectors(); + + var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); + var uf = fmgr.declareUF("uf", bitvectorType, bitvectorType, bitvectorType); + + var idxA1 = bvmgr.makeBitvector(8, 1); + var idxA2 = bvmgr.makeBitvector(8, 7); + var valA = bvmgr.makeBitvector(8, 10); + + var idxB1 = bvmgr.makeBitvector(8, 3); + var idxB2 = bvmgr.makeBitvector(8, 2); + var valB = bvmgr.makeBitvector(8, 5); + + checkModelContains( + bmgr.and( + bvmgr.equal(fmgr.callUF(uf, idxA1, idxA2), valA), + bvmgr.equal(fmgr.callUF(uf, idxB1, idxB2), valB)), + "uf", + ImmutableMap.of( + ImmutableList.of(idxA1, idxA2), valA, ImmutableList.of(idxB1, idxB2), valB)); + } + + @Test + public void testArray1Int() { + requireArrays(); + requireArrayModel(); + requireIntegers(); + + var array = amgr.makeArray("array", IntegerType, IntegerType); + + var idx = imgr.makeNumber(1); + var val = imgr.makeNumber(10); + + checkModelContains( + imgr.equal(amgr.select(array, idx), val), + "array", + ImmutableMap.of(ImmutableList.of(idx), val)); + } + + @Test + public void testArray2Int() { + requireArrays(); + requireArrayModel(); + requireIntegers(); + + var array = amgr.makeArray("array", IntegerType, IntegerType); + + var idxA = imgr.makeNumber(1); + var valA = imgr.makeNumber(10); + + var idxB = imgr.makeNumber(2); + var valB = imgr.makeNumber(5); + + checkModelContains( + bmgr.and( + imgr.equal(amgr.select(array, idxA), valA), imgr.equal(amgr.select(array, idxB), valB)), + "array", + ImmutableMap.of(ImmutableList.of(idxA), valA, ImmutableList.of(idxB), valB)); + } + + @Test + public void testArray1IntInt() { + requireArrays(); + requireArrayModel(); + requireIntegers(); + + var array = + amgr.makeArray("array", IntegerType, FormulaType.getArrayType(IntegerType, IntegerType)); + + var idxA = imgr.makeNumber(1); + var idxB = imgr.makeNumber(7); + var val = imgr.makeNumber(10); + + checkModelContains( + imgr.equal(amgr.select(amgr.select(array, idxA), idxB), val), + "array", + ImmutableMap.of(ImmutableList.of(idxA, idxB), val)); + } + + @Test + public void testArray2IntInt() { + requireArrays(); + requireArrayModel(); + requireIntegers(); + + var array = + amgr.makeArray("array", IntegerType, FormulaType.getArrayType(IntegerType, IntegerType)); + + var idxA1 = imgr.makeNumber(1); + var idxA2 = imgr.makeNumber(7); + var valA = imgr.makeNumber(10); + + var idxB1 = imgr.makeNumber(3); + var idxB2 = imgr.makeNumber(2); + var valB = imgr.makeNumber(5); + + checkModelContains( + bmgr.and( + imgr.equal(amgr.select(amgr.select(array, idxA1), idxA2), valA), + imgr.equal(amgr.select(amgr.select(array, idxB1), idxB2), valB)), + "array", + ImmutableMap.of( + ImmutableList.of(idxA1, idxA2), valA, ImmutableList.of(idxB1, idxB2), valB)); + } + + @Test + public void testUf1Int() { + requireIntegers(); + + var uf = fmgr.declareUF("uf", IntegerType, IntegerType); + + var idx = imgr.makeNumber(1); + var val = imgr.makeNumber(10); + + checkModelContains( + imgr.equal(fmgr.callUF(uf, idx), val), "uf", ImmutableMap.of(ImmutableList.of(idx), val)); + } + + @Test + public void testUf2Int() { + requireIntegers(); + + var uf = fmgr.declareUF("uf", IntegerType, IntegerType); + + var idxA = imgr.makeNumber(1); + var valA = imgr.makeNumber(10); + + var idxB = imgr.makeNumber(2); + var valB = imgr.makeNumber(5); + + checkModelContains( + bmgr.and(imgr.equal(fmgr.callUF(uf, idxA), valA), imgr.equal(fmgr.callUF(uf, idxB), valB)), + "uf", + ImmutableMap.of(ImmutableList.of(idxA), valA, ImmutableList.of(idxB), valB)); + } + + @Test + public void testUf1IntInt() { + requireIntegers(); + + var uf = fmgr.declareUF("uf", IntegerType, IntegerType, IntegerType); + + var idxA = imgr.makeNumber(1); + var idxB = imgr.makeNumber(7); + var val = imgr.makeNumber(10); + + checkModelContains( + imgr.equal(fmgr.callUF(uf, idxA, idxB), val), + "uf", + ImmutableMap.of(ImmutableList.of(idxA, idxB), val)); + } + + @Test + public void testUf2IntInt() { + requireIntegers(); + + var uf = fmgr.declareUF("uf", IntegerType, IntegerType, IntegerType); + + var idxA1 = imgr.makeNumber(1); + var idxA2 = imgr.makeNumber(7); + var valA = imgr.makeNumber(10); + + var idxB1 = imgr.makeNumber(3); + var idxB2 = imgr.makeNumber(2); + var valB = imgr.makeNumber(5); + + checkModelContains( + bmgr.and( + imgr.equal(fmgr.callUF(uf, idxA1, idxA2), valA), + imgr.equal(fmgr.callUF(uf, idxB1, idxB2), valB)), + "uf", + ImmutableMap.of( + ImmutableList.of(idxA1, idxA2), valA, ImmutableList.of(idxB1, idxB2), valB)); + } + @Test @SuppressWarnings("resource") public void multiCloseTest() throws SolverException, InterruptedException { From 9f8a5941c9b58610f529c0cd5caadd1584965a44 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 29 Oct 2025 12:25:21 +0100 Subject: [PATCH 4/9] Add tests for 3d arrays with a single stored value --- src/org/sosy_lab/java_smt/test/ModelTest.java | 73 +++++++++++++++++++ 1 file changed, 73 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 20ade77d57..2a175db45d 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -2405,6 +2405,44 @@ public void testArray2BvBv() { ImmutableList.of(idxA1, idxA2), valA, ImmutableList.of(idxB1, idxB2), valB)); } + @Test + public void testArrayStore1BvBvBv() { + // Test for 3d bitvector arrays with exactly one element + // array = (Store (const ...) idxA (Store (const ..) idxB (Store (const ...) idx C val)) + requireArrays(); + requireBitvectors(); + + // Boolector doesn't support multiple indices + assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); + + var scalarType = FormulaType.getBitvectorTypeWithSize(8); + + var array1Type = FormulaType.getArrayType(scalarType, scalarType); + var array2Type = FormulaType.getArrayType(scalarType, array1Type); + var array3Type = FormulaType.getArrayType(scalarType, array2Type); + + var array = amgr.makeArray("array", array3Type.getIndexType(), array3Type.getElementType()); + + var idxA = bvmgr.makeBitvector(scalarType.getSize(), 1); + var idxB = bvmgr.makeBitvector(scalarType.getSize(), 7); + var idxC = bvmgr.makeBitvector(scalarType.getSize(), 2); + var val = bvmgr.makeBitvector(scalarType.getSize(), 10); + + var scalarConst = bvmgr.makeBitvector(scalarType.getSize(), 0); + var array1Const = amgr.makeArray(array1Type, scalarConst); + var array2Const = amgr.makeArray(array2Type, array1Const); + var array3Const = amgr.makeArray(array3Type, array2Const); + + var array1Value = amgr.store(array1Const, idxC, val); + var array2Value = amgr.store(array2Const, idxB, array1Value); + var array3Value = amgr.store(array3Const, idxA, array2Value); + + checkModelContains( + amgr.equivalence(array, array3Value), + "array", + ImmutableMap.of(ImmutableList.of(idxA, idxB, idxC), val)); + } + @Test public void testUf1Bv() { requireBitvectors(); @@ -2537,6 +2575,41 @@ public void testArray1IntInt() { ImmutableMap.of(ImmutableList.of(idxA, idxB), val)); } + @Test + public void testArrayStore1IntIntInt() { + // Test for 3d integer arrays with exactly one element + // array = (Store (const ...) idxA (Store (const ..) idxB (Store (const ...) idx C val)) + requireArrays(); + requireIntegers(); + + var scalarType = FormulaType.IntegerType; + + var array1Type = FormulaType.getArrayType(scalarType, scalarType); + var array2Type = FormulaType.getArrayType(scalarType, array1Type); + var array3Type = FormulaType.getArrayType(scalarType, array2Type); + + var array = amgr.makeArray("array", array3Type.getIndexType(), array3Type.getElementType()); + + var idxA = imgr.makeNumber(1); + var idxB = imgr.makeNumber(7); + var idxC = imgr.makeNumber(2); + var val = imgr.makeNumber(10); + + var scalarConst = imgr.makeNumber(0); + var array1Const = amgr.makeArray(array1Type, scalarConst); + var array2Const = amgr.makeArray(array2Type, array1Const); + var array3Const = amgr.makeArray(array3Type, array2Const); + + var array1Value = amgr.store(array1Const, idxC, val); + var array2Value = amgr.store(array2Const, idxB, array1Value); + var array3Value = amgr.store(array3Const, idxA, array2Value); + + checkModelContains( + amgr.equivalence(array, array3Value), + "array", + ImmutableMap.of(ImmutableList.of(idxA, idxB, idxC), val)); + } + @Test public void testArray2IntInt() { requireArrays(); From 18b25b317e61c80dcb989dbfca668af3675c2964 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 29 Oct 2025 12:40:55 +0100 Subject: [PATCH 5/9] Apply error-prone patch --- src/org/sosy_lab/java_smt/test/ModelTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 2a175db45d..3d121264f4 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -2305,7 +2305,7 @@ private void checkModelContains( assignment.getValueAsFormula()); } } - var model = builder.build(); + var model = builder.buildOrThrow(); assertThat(model).containsAtLeastEntriesIn(expected); } catch (SolverException | InterruptedException e) { From 5c8d5fffe6b41d683fce7f85b889fbb147c0d64c Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 29 Oct 2025 13:40:35 +0100 Subject: [PATCH 6/9] Removed UF test again These will be added later. The quickfix is just about array values in the model --- src/org/sosy_lab/java_smt/test/ModelTest.java | 145 ------------------ 1 file changed, 145 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 3d121264f4..de46e3465d 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -2443,81 +2443,6 @@ public void testArrayStore1BvBvBv() { ImmutableMap.of(ImmutableList.of(idxA, idxB, idxC), val)); } - @Test - public void testUf1Bv() { - requireBitvectors(); - - var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); - var uf = fmgr.declareUF("uf", bitvectorType, bitvectorType); - - var idx = bvmgr.makeBitvector(8, 1); - var val = bvmgr.makeBitvector(8, 10); - - checkModelContains( - bvmgr.equal(fmgr.callUF(uf, idx), val), "uf", ImmutableMap.of(ImmutableList.of(idx), val)); - } - - @Test - public void testUf2Bv() { - requireBitvectors(); - - var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); - var uf = fmgr.declareUF("uf", bitvectorType, bitvectorType); - - var idxA = bvmgr.makeBitvector(8, 1); - var valA = bvmgr.makeBitvector(8, 10); - - var idxB = bvmgr.makeBitvector(8, 2); - var valB = bvmgr.makeBitvector(8, 5); - - checkModelContains( - bmgr.and( - bvmgr.equal(fmgr.callUF(uf, idxA), valA), bvmgr.equal(fmgr.callUF(uf, idxB), valB)), - "uf", - ImmutableMap.of(ImmutableList.of(idxA), valA, ImmutableList.of(idxB), valB)); - } - - @Test - public void testUf1BvBV() { - requireBitvectors(); - - var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); - var uf = fmgr.declareUF("uf", bitvectorType, bitvectorType, bitvectorType); - - var idxA = bvmgr.makeBitvector(8, 1); - var idxB = bvmgr.makeBitvector(8, 7); - var val = bvmgr.makeBitvector(8, 10); - - checkModelContains( - bvmgr.equal(fmgr.callUF(uf, idxA, idxB), val), - "uf", - ImmutableMap.of(ImmutableList.of(idxA, idxB), val)); - } - - @Test - public void testUf2BvBv() { - requireBitvectors(); - - var bitvectorType = FormulaType.getBitvectorTypeWithSize(8); - var uf = fmgr.declareUF("uf", bitvectorType, bitvectorType, bitvectorType); - - var idxA1 = bvmgr.makeBitvector(8, 1); - var idxA2 = bvmgr.makeBitvector(8, 7); - var valA = bvmgr.makeBitvector(8, 10); - - var idxB1 = bvmgr.makeBitvector(8, 3); - var idxB2 = bvmgr.makeBitvector(8, 2); - var valB = bvmgr.makeBitvector(8, 5); - - checkModelContains( - bmgr.and( - bvmgr.equal(fmgr.callUF(uf, idxA1, idxA2), valA), - bvmgr.equal(fmgr.callUF(uf, idxB1, idxB2), valB)), - "uf", - ImmutableMap.of( - ImmutableList.of(idxA1, idxA2), valA, ImmutableList.of(idxB1, idxB2), valB)); - } - @Test public void testArray1Int() { requireArrays(); @@ -2636,76 +2561,6 @@ public void testArray2IntInt() { ImmutableList.of(idxA1, idxA2), valA, ImmutableList.of(idxB1, idxB2), valB)); } - @Test - public void testUf1Int() { - requireIntegers(); - - var uf = fmgr.declareUF("uf", IntegerType, IntegerType); - - var idx = imgr.makeNumber(1); - var val = imgr.makeNumber(10); - - checkModelContains( - imgr.equal(fmgr.callUF(uf, idx), val), "uf", ImmutableMap.of(ImmutableList.of(idx), val)); - } - - @Test - public void testUf2Int() { - requireIntegers(); - - var uf = fmgr.declareUF("uf", IntegerType, IntegerType); - - var idxA = imgr.makeNumber(1); - var valA = imgr.makeNumber(10); - - var idxB = imgr.makeNumber(2); - var valB = imgr.makeNumber(5); - - checkModelContains( - bmgr.and(imgr.equal(fmgr.callUF(uf, idxA), valA), imgr.equal(fmgr.callUF(uf, idxB), valB)), - "uf", - ImmutableMap.of(ImmutableList.of(idxA), valA, ImmutableList.of(idxB), valB)); - } - - @Test - public void testUf1IntInt() { - requireIntegers(); - - var uf = fmgr.declareUF("uf", IntegerType, IntegerType, IntegerType); - - var idxA = imgr.makeNumber(1); - var idxB = imgr.makeNumber(7); - var val = imgr.makeNumber(10); - - checkModelContains( - imgr.equal(fmgr.callUF(uf, idxA, idxB), val), - "uf", - ImmutableMap.of(ImmutableList.of(idxA, idxB), val)); - } - - @Test - public void testUf2IntInt() { - requireIntegers(); - - var uf = fmgr.declareUF("uf", IntegerType, IntegerType, IntegerType); - - var idxA1 = imgr.makeNumber(1); - var idxA2 = imgr.makeNumber(7); - var valA = imgr.makeNumber(10); - - var idxB1 = imgr.makeNumber(3); - var idxB2 = imgr.makeNumber(2); - var valB = imgr.makeNumber(5); - - checkModelContains( - bmgr.and( - imgr.equal(fmgr.callUF(uf, idxA1, idxA2), valA), - imgr.equal(fmgr.callUF(uf, idxB1, idxB2), valB)), - "uf", - ImmutableMap.of( - ImmutableList.of(idxA1, idxA2), valA, ImmutableList.of(idxB1, idxB2), valB)); - } - @Test @SuppressWarnings("resource") public void multiCloseTest() throws SolverException, InterruptedException { From a79537819e226531049eea5b607848e155c30c3a Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 29 Oct 2025 19:38:49 +0100 Subject: [PATCH 7/9] Fix CI --- src/org/sosy_lab/java_smt/test/ModelTest.java | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index de46e3465d..68a12678a1 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -2260,10 +2260,10 @@ public void arrayTest5() } /** Returns the arguments of an UF or array definition from the model. */ - private Iterable getFunctionArgs(Formula f) { + private Iterable getFunctionArgs(Formula pValue) { requireVisitor(); return mgr.visit( - f, + pValue, new DefaultFormulaVisitor<>() { @Override protected Iterable visitDefault(Formula f) { @@ -2291,18 +2291,20 @@ public Iterable visitFunction( } /** Evaluate the UF or array constraint and check that the model contains the expected values. */ - private void checkModelContains( + private void checkModelContains( BooleanFormula pFormula, String pVar, Map, Formula> expected) { try (var prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { prover.addConstraint(pFormula); assertThat(prover.isUnsat()).isFalse(); ImmutableMap.Builder, Formula> builder = ImmutableMap.builder(); - for (var assignment : prover.getModel().asList()) { - if (assignment.getName().equals(pVar)) { - builder.put( - ImmutableList.copyOf(getFunctionArgs(assignment.getKey())), - assignment.getValueAsFormula()); + try (var model = prover.getModel()) { + for (var assignment : model.asList()) { + if (assignment.getName().equals(pVar)) { + builder.put( + ImmutableList.copyOf(getFunctionArgs(assignment.getKey())), + assignment.getValueAsFormula()); + } } } var model = builder.buildOrThrow(); From 093d29a5fa6553eea6e86ce0319cadadd1f2ced7 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Wed, 29 Oct 2025 19:42:47 +0100 Subject: [PATCH 8/9] Require array model generation for the tests --- src/org/sosy_lab/java_smt/test/ModelTest.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index 68a12678a1..d35ae7f11e 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -2293,6 +2293,8 @@ public Iterable visitFunction( /** Evaluate the UF or array constraint and check that the model contains the expected values. */ private void checkModelContains( BooleanFormula pFormula, String pVar, Map, Formula> expected) { + requireArrayModel(); + try (var prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { prover.addConstraint(pFormula); assertThat(prover.isUnsat()).isFalse(); From d13960a6dc06bf41c3f5752469c76da398b35686 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 31 Oct 2025 21:12:34 +0100 Subject: [PATCH 9/9] Bitwuzla: Print a more descriptive error message when we can't parse an array value for the model --- .../sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java index a02e38f4ec..83b5f4e486 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java @@ -191,7 +191,11 @@ private Iterable buildArrayAssignment(Term expr, Term value) { // Should be unreachable // We assume that array values are made up of "const" and "store" nodes with non-array // constants as leaves - throw new AssertionError(); + throw new AssertionError( + String.format( + "Can't process model value for variable '%s'. Please report this issue to the " + + "JavaSMT developers", + getVar(expr))); } }