Override `default` methods in `BasicProverEnvironment` for all delegates by daniel-raffler · Pull Request #685 · sosy-lab/java-smt

daniel-raffler · 2026-07-07T14:38:09Z

Hello,

this PR adds overrides for all default methods in BasicProverEnvironment for all of our delegates. This makes sure that the solver implementation is used when available, and that we don't fall back to the default implementation when using a delegate

… so that calls are always passed through

…cking delegates

…a, don't add the result to the list of tracked formulas

…he assertions

…ion script

baierd

Looks good besides the open points! Nice work!

Please open multiple smaller PRs next time instead of one giant one ;D

Did you test whether we handle push(BooleanFormula) correctly in all cases? (I saw that you added it to the trace test. Good!) The used delegate calls addConstraint(BooleanFormula) due to the default implementation, but is that addConstraint() call then tracked by the delegate layers?
Do we even need to add push(BooleanFormula) to the delegates? The default impl. uses two methods that are already part of the layers, and it is never overridden.

We should test most of our additional layers (logging/debugging etc.) from time to time! Would you be so kind and open issues (per delegate) to do this? Running CPAchecker with distinct analyses for each should be fine for now to get a sense of whether they work or collect problems.

baierd · 2026-07-09T11:48:22Z

+  @Override
+  public @Nullable T push(BooleanFormula f) throws InterruptedException {
+    stats.push.getAndIncrement();
+    stats.pop.getAndIncrement();


I think this line should not be here.

Nice catch! I've replaced it with

@Override public @Nullable T push(BooleanFormula f) throws InterruptedException { stats.push.getAndIncrement(); stats.constraint.getAndIncrement(); return delegate.push(f); }

which is what the default method would have produced

Should I get rid of the stats.constraint.getAndIncrement() entirely?

baierd · 2026-07-09T11:49:01Z


+  @Override
+  public ImmutableMap<String, String> getStatistics() {
+    return ImmutableMap.of();


Missing delegate call?

Hmm.. I wasn't quite sure what to put there. In StatisticsSolverContext the getStatistics method includes the data that we're collecting. However, this won't work for StatisticsBasicProverEnvironment as we're not tracking statistics for each prover individually

I've now simply added a call to the delegate

We can always just return the solvers statistics if it provides some.

But i agree that this is actually a interesting question. I'll take a closer look.

baierd · 2026-07-09T12:17:01Z

+
+  @Override
+  public <T extends Formula> @Nullable T eval(T pFormula) {
+    throw new UnsupportedOperationException(UNSUPPORTED_OPERATION);


Why can't we synchronize evaluators with contexts?

I know that the old code also did not allow this, but why?

I think it's just because FormulaManager.translate expects a boolean formula. We could allow eval for boolean formulas, but throwing an UnsupportedOperationException only for some inputs may be a bit confusing to the user

I think the current message is confusing, as it actually says that only boolean formulas are allowed.

Would you be so kind and test boolean formulas only + add a small test for this? Essentially just try to eval a boolean and a non-boolean formula.

I've implemented it for booleans now, see here

baierd · 2026-07-09T12:42:01Z

+        logger.logDefDiscard(
+            logger.toVariable(this), "getModelAssignments()", delegate::getModelAssignments);
+    return FluentIterable.from(result)
+        // TODO Fix this in the Z3 model


Would you be so kind and open a issue for this?

I think the issue has already been fixed by 48b66d4 and 3e665e5

Good point.
If that's the case, we should remove the TODO. Could you double check with the commit that added the TODO whether we can be sure that it is related to the 2 fixes and remove the TODO if they are?

…rEnvironment

daniel-raffler · 2026-07-10T07:14:29Z

Looks good besides the open points! Nice work!

Thanks!

Please open multiple smaller PRs next time instead of one giant one ;D

Sure, I'll try to keep the PRs smaller 😅. Most of the large changes are just copy and paste, but I can see how it's hard to review

Did you test whether we handle push(BooleanFormula) correctly in all cases? (I saw that you added it to the trace test. Good!) The used delegate calls addConstraint(BooleanFormula) due to the default implementation, but is that addConstraint() call then tracked by the delegate layers?

The tracing delegate will just write prover.push(f) to the log. The formula for f has already been unrolled and is just a variable name. When translating to SMTLIB the call then needs to be split up and we generate (push 1) (assert f)

There is an example of how the trace changed in one of the tests. Before adding the override we had:

var var1 = mgr.getBooleanFormulaManager().makeTrue();
var0.push();
var var2 = var0.addConstraint(var1);

Now it's just:

var var1 = mgr.getBooleanFormulaManager().makeTrue();
var var2 = var0.push(var1);

We should test most of our additional layers (logging/debugging etc.) from time to time! Would you be so kind and open issues (per delegate) to do this? Running CPAchecker with distinct analyses for each should be fine for now to get a sense of whether they work or collect problems.

I've open some issues here

…atorWithContext

daniel-raffler added 8 commits July 7, 2026 11:35

Override default methods from BasicProverEnvironment in all delegates…

d00f928

… so that calls are always passed through

Override default methods from BasicProverEnvironment in new error che…

9b69459

…cking delegates

Debugging Mode: If the solver returns null when evaluating a formul…

6bd9dc5

…a, don't add the result to the list of tracked formulas

Logging Mode: Print a message to the log when a formula is added to t…

31fcc36

…he assertions

Suppress resource warnings for getEvaluator in the delegates

92e6bf7

Fix prover.push(f) in TraceBasicProverEnvironment

0826479

Trace: Update path to the trace in the test script

c5ec2d3

Trace: Add support for push(f) and getEvaluator in the trace translat…

45eaabc

…ion script

daniel-raffler requested review from baierd and kfriedberger July 7, 2026 14:38

daniel-raffler self-assigned this Jul 7, 2026

daniel-raffler added the enhancement label Jul 7, 2026

daniel-raffler linked an issue Jul 7, 2026 that may be closed by this pull request

Methods with default implementations missing from delegates #672

Open

baierd requested changes Jul 9, 2026

View reviewed changes

daniel-raffler added 7 commits July 9, 2026 19:43

Fix push(f) in StatisticsBasicProverEnvironment

590b812

Return delegate statistics in getStatistics from StatisticsBasicProve…

05862b6

…rEnvironment

Make package private fields private

ba7318d

Remove unused field

49a3383

Remove outdated TODOs

1f77e05

Errorprone

4840033

Remove unused imports

c06e0f5

Allow boolean formulas to be evaluated by eval in SynchronizedEvalu…

71ca20c

…atorWithContext

Uh oh!

Conversation

daniel-raffler commented Jul 7, 2026

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!

Choose a reason for hiding this comment

Uh oh!

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!

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 Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

2 participants

daniel-raffler commented Jul 10, 2026 •

edited

Loading