Quickfix for array model generation in Bitwuzla #541

daniel-raffler · 2025-10-28T18:20:30Z

This MR adds Bitwuzla multi-dimensional array model evaluation.
(Similar to #539 for CVC5)

Also, more tests for this not based on SMTLIb2 parsing are added.

Ported from CVC5, see 0d463c8

baierd

LGTM. But i would like to test this with at least the 2 tests from the related CVC5 branch, if possible more.

baierd · 2025-10-28T20:03:38Z

@daniel-raffler could you maybe add a test that (for Integer and BV if possible) that uses multi-dimensional arrays, but with at least 1 store instruction?

Bonus points if the store itself stores a multi-dimensional array.

baierd

Thanks for adding the tests! I think many can be combined to test the behavior in 2 tests (per theory). Something like:

Nested arrays with UFs (you can combine store and select)
Nested arrays with UFs and non UFs (store and select combined)

(The CVC5 branch already has tests for only nested arrays w select, so no need for that)

baierd · 2025-10-29T11:36:15Z

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

+  }
+
+  /** Evaluate the UF or array constraint and check that the model contains the expected values. */
+  private <T> void checkModelContains(


Methods like this already exist AFAIK. Could you check and reuse the existing ones?

Sure, I can rewrite the tests to use testModelGetters just as on the CVC5 branch

baierd · 2025-10-29T11:37:47Z

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

+
+    checkModelContains(
+        bmgr.and(
+            bvmgr.equal(amgr.select(array, idxA), valA),


Is this not covered by existing tests?
(It might be that there are only Integer based tests for this)

baierd · 2025-10-29T11:38:30Z

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

+  }
+
+  @Test
+  public void testArray1BvBV() {


A description, e.g. SMTLIB2, of whats tested should be added to all new tests.

daniel-raffler · 2025-10-29T11:41:22Z

@daniel-raffler could you maybe add a test that (for Integer and BV if possible) that uses multi-dimensional arrays, but with at least 1 store instruction?

Bonus points if the store itself stores a multi-dimensional array.

I've added 68cb59c from the modelArrayGeneration branch and two more tests for 3d arrays that use stores. Is that what you had in mind?

LGTM. But i would like to test this with at least the 2 tests from the related CVC5 branch, if possible more.

The tests from the CVC5 branch also seem to be working

These will be added later. The quickfix is just about array values in the model

daniel-raffler · 2025-10-30T13:29:06Z

Thanks for adding the tests! I think many can be combined to test the behavior in 2 tests (per theory). Something like:
1. Nested arrays with UFs (you can combine store and select)

2. Nested arrays with UFs and non UFs (store and select combined)
(The CVC5 branch already has tests for only nested arrays w select, so no need for that)

I've removed the UF tests again as they were meant to test assignments for uninterpreted functions and aren't needed here. Other than that there is some overlap with the tests from the CVC5 branch and I'm not if we can't just remove all of the tests here.

What do you think still needs testing that isn't already covered by the CVC5 branch?

I'm getting different results for testArray1BvBV and testArray2BvBV on Z3 and Yices (EDIT: See here for the JUnit results). In the first test we get an incomplete model while the second test crashes, so maybe these two should be kept? Since testArray1BvBV is essentially the same as testGetArrays3BitvectorNoParsing from the CVC5 branch we would then only need to add testArray2BvBV (and maybe testArray2IntInt for completeness sake)

baierd · 2025-10-31T19:37:03Z

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java

+      // 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();


A more expressive exception and message could be added here.

baierd · 2025-10-31T19:40:39Z

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

  }

+  /** Returns the arguments of an UF or array definition from the model. */
+  private Iterable<Formula> getFunctionArgs(Formula pValue) {


Actually why don't we have a visitor method for retrieving all UFs, including all applications? @kfriedberger do you know? Seems like this might be helpful in general.

baierd · 2025-10-31T19:43:44Z

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

+        new DefaultFormulaVisitor<>() {
+          @Override
+          protected Iterable<Formula> visitDefault(Formula f) {
+            throw new IllegalArgumentException();


Are you sure this is correct?
Since you don't override all methods of the super-class, this can be called!

Yeah, that's fine. The argument to this function is a "key" formula from the model. So it's either (f 1 2 3) for a UF mapping f(1,2,3) or (Select (Select (Select 1 arr) 2) 3) for an array mapping arr(1,2,3). We then get the arguments 1, 2 and 3 by simply returning them for the UF mapping: this is the else branch in visitFunction. Or descending the term recursively if we have an array: that's the if part of visitFunction and visitFreeVariable for the base case

The whole function could be removed if we rewrite the tests to use testModelGetters

baierd · 2025-10-31T19:46:50Z

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

+              return FluentIterable.concat(
+                  getFunctionArgs(args.get(0)), ImmutableList.of(args.get(1)));
+            } else {
+              // Assume its an UF value


visitFunction() is defined to be called on any function, including UFs. I would recommend explicitly checking for UFs. You could take a look at the VariableAndUFExtractor for inspiration.

…an array value for the model

daniel-raffler added 2 commits October 28, 2025 19:12

Bitwuzla: Fix array value generation in the model

465cd42

Ported from CVC5, see 0d463c8

Bitwuzla: Disable a test as Bitwuzla is too slow

d994467

daniel-raffler added this to the Release 6.0.0 milestone Oct 28, 2025

daniel-raffler added the Bitwuzla label Oct 28, 2025

daniel-raffler requested a review from kfriedberger October 28, 2025 18:23

daniel-raffler self-assigned this Oct 28, 2025

baierd self-requested a review October 28, 2025 19:38

baierd reviewed Oct 28, 2025

View reviewed changes

daniel-raffler added 3 commits October 29, 2025 11:40

Add tests for array and Uf values in the model

68cb59c

Add tests for 3d arrays with a single stored value

9f8a594

Apply error-prone patch

18b25b3

baierd requested changes Oct 29, 2025

View reviewed changes

daniel-raffler added 3 commits October 29, 2025 13:40

Removed UF test again

5c8d5ff

These will be added later. The quickfix is just about array values in the model

Fix CI

a795378

Require array model generation for the tests

093d29a

baierd requested changes Oct 31, 2025

View reviewed changes

Bitwuzla: Print a more descriptive error message when we can't parse …

d13960a

…an array value for the model

Quickfix for array model generation in Bitwuzla #541

Are you sure you want to change the base?

Quickfix for array model generation in Bitwuzla #541

Uh oh!

Conversation

daniel-raffler commented Oct 28, 2025 • edited by baierd Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

baierd left a comment

Choose a reason for hiding this comment

Uh oh!

baierd commented Oct 28, 2025

Uh oh!

baierd left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

daniel-raffler commented Oct 29, 2025

Uh oh!

daniel-raffler commented Oct 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

2 participants

daniel-raffler commented Oct 28, 2025 •

edited by baierd

Loading

daniel-raffler commented Oct 30, 2025 •

edited

Loading