Bitwuzla: Optimize memory usage

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)));
   }
 
   /**
@@ -227,13 +232,8 @@ public void 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() {

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 <https://www.sosy-lab.org>
+ *
+ * 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<Term, Sort, TermManager> {
+  private final BitwuzlaAbstractProver<?> prover;
+
+  protected BitwuzlaEvaluator(
+      BitwuzlaAbstractProver<?> pProver, FormulaCreator<Term, Sort, TermManager, ?> 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);
+  }
+}

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

@@ -15,20 +15,23 @@
 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;
 import java.util.ArrayList;
 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;
 import java.util.Map;
 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<Term> getConstraintsForTerm(Term pTerm) {
     return transformedImmutableSetCopy(usedConstraintVariables, constraintsForVariables::get);
   }
 
+  @Override
+  public void extractVariablesAndUFs(
+      final Formula pFormula,
+      final boolean extractUF,
+      final BiConsumer<String, Formula> pConsumer) {
+    ImmutableSet.Builder<Term> builder = ImmutableSet.builder();
+    var cache = new HashSet<Term>();
+    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);