From fc504558c1b4e38d42e3ddeddc5fdbe3dd65dceb Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 11 Apr 2026 17:26:08 +0200 Subject: [PATCH 1/3] Bitwuzla: Avoid building a full model for each allSat iteration --- .../bitwuzla/BitwuzlaAbstractProver.java | 17 ++++----- .../solvers/bitwuzla/BitwuzlaEvaluator.java | 37 +++++++++++++++++++ 2 files changed, 45 insertions(+), 9 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaEvaluator.java diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java index e7247fff72..17b2f36631 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -169,7 +169,12 @@ public Model getModel() throws SolverException { checkGenerateModels(); // special case for Bitwuzla: Models are not permanent and need to be closed // before any change is applied to the prover stack. So, we register the Model as Evaluator. - return getEvaluatorWithoutChecks(); + return registerEvaluator( + new BitwuzlaModel( + env, + this, + creator, + Collections2.transform(getAssertedFormulas(), creator::extractInfo))); } /** @@ -225,15 +230,9 @@ public void close() { super.close(); } - @SuppressWarnings("resource") @Override - protected BitwuzlaModel getEvaluatorWithoutChecks() { - return registerEvaluator( - new BitwuzlaModel( - env, - this, - creator, - Collections2.transform(getAssertedFormulas(), creator::extractInfo))); + protected BitwuzlaEvaluator getEvaluatorWithoutChecks() { + return registerEvaluator(new BitwuzlaEvaluator(this, creator)); } public boolean isClosed() { diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaEvaluator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaEvaluator.java new file mode 100644 index 0000000000..d3eceb821b --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaEvaluator.java @@ -0,0 +1,37 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2026 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.bitwuzla; + +import static com.google.common.base.Preconditions.checkState; + +import org.jspecify.annotations.Nullable; +import org.sosy_lab.java_smt.basicimpl.AbstractEvaluator; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; +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; + +class BitwuzlaEvaluator extends AbstractEvaluator { + private final BitwuzlaAbstractProver prover; + + protected BitwuzlaEvaluator( + BitwuzlaAbstractProver pProver, FormulaCreator creator) { + super(pProver, creator); + prover = pProver; + } + + @Override + protected @Nullable Term evalImpl(Term formula) { + checkState(!isClosed()); + checkState(!prover.isClosed(), "Cannot use model after prover is closed"); + return prover.env.get_value(formula); + } +} From 69d33710c1760fd89a27b7a7906096f8d236c088 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 11 Apr 2026 20:40:24 +0200 Subject: [PATCH 2/3] Add resource annotation --- .../java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java index 17b2f36631..1600a3f6ec 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaAbstractProver.java @@ -230,6 +230,7 @@ public void close() { super.close(); } + @SuppressWarnings("resource") @Override protected BitwuzlaEvaluator getEvaluatorWithoutChecks() { return registerEvaluator(new BitwuzlaEvaluator(this, creator)); From 9c863a9428e6dd3e284292e65437ea71ad0b71c9 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 12 Apr 2026 10:35:50 +0200 Subject: [PATCH 3/3] Bitwuzla: Avoid creating unnecessary Java proxies in extractVariablesAndUFs --- .../bitwuzla/BitwuzlaFormulaCreator.java | 38 +++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index 0589b194d0..ecba64a07a 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -15,6 +15,7 @@ import com.google.common.base.Preconditions; import com.google.common.collect.HashBasedTable; import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableSet; import com.google.common.collect.Table; import java.math.BigInteger; import java.util.ArrayDeque; @@ -22,6 +23,7 @@ import java.util.Collection; import java.util.Deque; import java.util.HashMap; +import java.util.HashSet; import java.util.Iterator; import java.util.LinkedHashSet; import java.util.List; @@ -29,6 +31,7 @@ import java.util.Map.Entry; import java.util.Optional; import java.util.Set; +import java.util.function.BiConsumer; import org.sosy_lab.java_smt.api.ArrayFormula; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -633,6 +636,41 @@ public Collection getConstraintsForTerm(Term pTerm) { return transformedImmutableSetCopy(usedConstraintVariables, constraintsForVariables::get); } + @Override + public void extractVariablesAndUFs( + final Formula pFormula, + final boolean extractUF, + final BiConsumer pConsumer) { + ImmutableSet.Builder builder = ImmutableSet.builder(); + var cache = new HashSet(); + var work = new ArrayDeque<>(ImmutableList.of(extractInfo(pFormula))); + while (!work.isEmpty()) { + var term = work.pop(); + if (cache.add(term)) { + var kind = term.kind(); + if (kind == Kind.CONSTANT) { + builder.add(term); + } else if (kind == Kind.APPLY) { + if (extractUF) { + builder.add(term); + } + for (int c = 1; c < term.num_children(); c++) { + work.push(term.get(c)); + } + } else { + for (int c = 0; c < term.num_children(); c++) { + work.push(term.get(c)); + } + } + } + } + for (var term : builder.build()) { + pConsumer.accept( + term.kind() == Kind.APPLY ? term.get(0).symbol() : term.symbol(), + encapsulateWithTypeOf(term)); + } + } + @Override protected FloatingPointRoundingMode getRoundingMode(Term term) { checkArgument(term.sort().is_rm(), "Term '%s' is not of rounding mode sort.", term);