Add logic, engine and further options for Z3

build/checkstyle.xml

@@ -77,7 +77,9 @@ SPDX-License-Identifier: Apache-2.0
     <module name="RedundantImport"/>
     <module name="UnusedImports"/>
     <module name="OuterTypeNumber"/>
-    <module name="ParameterNumber"/>
+    <module name="ParameterNumber">
+      <property name="max" value="8"/>
+    </module>
     <module name="GenericWhitespace"/>
     <module name="EmptyForInitializerPad"/>
     <module name="EmptyForIteratorPad">

src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java

@@ -36,13 +36,17 @@
 import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat;
 import org.sosy_lab.java_smt.basicimpl.CachingModel;
+import org.sosy_lab.java_smt.solvers.z3.Z3SolverContext.ENGINE;
 
 abstract class Z3AbstractProver extends AbstractProverWithAllSat<Void> {
 
   protected final Z3FormulaCreator creator;
   protected final long z3context;
   protected final Z3FormulaManager mgr;
 
+  protected final ENGINE engine;
+  protected final Optional<String> logic;
+
   private final UniqueIdGenerator trackId = new UniqueIdGenerator();
   @Nullable private final Deque<PersistentMap<String, BooleanFormula>> storedConstraints;
 
@@ -51,12 +55,16 @@ abstract class Z3AbstractProver extends AbstractProverWithAllSat<Void> {
   Z3AbstractProver(
       Z3FormulaCreator pCreator,
       Z3FormulaManager pMgr,
+      Optional<String> pLogic,
+      ENGINE pEngine,
       Set<ProverOptions> pOptions,
       @Nullable PathCounterTemplate pLogfile,
       ShutdownNotifier pShutdownNotifier) {
     super(pOptions, pMgr.getBooleanFormulaManager(), pShutdownNotifier);
     creator = pCreator;
     z3context = creator.getEnv();
+    logic = pLogic;
+    engine = pEngine;
 
     if (pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE)) {
       storedConstraints = new ArrayDeque<>();

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java

@@ -207,6 +207,18 @@ assert getFormulaCreator().getFormulaType(expr) == FormulaType.BooleanType
     return serialized;
   }
 
+  /**
+   * Options string for all available options tied to the environment of the solver. The options are
+   * returned 1 per line, with the pattern:
+   *
+   * <p>optionName{.detailedName} (type) infoText that may include brackets (default: defaultValue)
+   *
+   * <p>e.g.: local_ctx (bool) perform local (i.e., cheap) context simplifications (default: false)
+   */
+  String getAllZ3Options() {
+    return Native.simplifyGetHelp(getEnvironment());
+  }
+
   @Override
   protected Long simplify(Long pF) throws InterruptedException {
     try {

src/org/sosy_lab/java_smt/solvers/z3/Z3NativeApiTest.java

@@ -0,0 +1,196 @@
+/*
+ * 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.z3;
+
+import static com.google.common.truth.Truth.assertThat;
+import static org.sosy_lab.java_smt.solvers.z3.Z3SolverContext.doubleOptions;
+
+import com.google.common.base.Splitter;
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableSet;
+import com.google.common.collect.Sets;
+import com.microsoft.z3.BoolSort;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.FuncDecl;
+import com.microsoft.z3.Global;
+import com.microsoft.z3.IntSort;
+import com.microsoft.z3.Model;
+import com.microsoft.z3.Params;
+import com.microsoft.z3.Solver;
+import com.microsoft.z3.Sort;
+import com.microsoft.z3.Status;
+import java.util.ArrayDeque;
+import java.util.Deque;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+import java.util.stream.Stream;
+import org.junit.AssumptionViolatedException;
+import org.junit.BeforeClass;
+import org.junit.Test;
+import org.sosy_lab.common.NativeLibraries;
+
+public class Z3NativeApiTest {
+
+  @BeforeClass
+  public static void loadLibraries() {
+    try {
+      NativeLibraries.loadLibrary("z3");
+      NativeLibraries.loadLibrary("z3java");
+    } catch (UnsatisfiedLinkError e) {
+      throw new AssumptionViolatedException("Z3 is not available", e);
+    }
+
+    System.setProperty("z3.skipLibraryLoad", "true");
+  }
+
+  @Test
+  public void interpolationTest() {
+    // Translation of an example by Arie Gurfinkel for calculating interpolants with spacer in Z3
+    // See https://github.com/agurfinkel/spacer-on-jupyter/blob/master/Dagstuhl2019.ipynb for the
+    // original Python code
+
+    try (Context env = new Context()) {
+      Global.setParameter("smt.random_seed", "42");
+      Global.setParameter("model.compact", "false");
+
+      Expr<IntSort> a = env.mkIntConst("a");
+      Expr<IntSort> b = env.mkIntConst("b");
+      Expr<IntSort> x = env.mkIntConst("x");
+
+      Expr<BoolSort> formulasA = env.mkAnd(env.mkLt(a, x), env.mkLt(x, b));
+      Expr<BoolSort> formulasB = env.mkLt(b, a);
+
+      Expr<BoolSort> interpolant = interpolate(env, formulasA, formulasB);
+
+      assertThat(validate(env, formulasA, formulasB, interpolant)).isTrue();
+    }
+  }
+
+  // Test that we correctly discern between int and double for options set in Z3, even after
+  // updates! This is very much a white-box test that utilizes internal info about the
+  // Z3SolverContext implementation.
+  // If this fails: update the doubleOptions set with the missing option!
+  @Test
+  public void z3OptionsTypeTest() {
+    try (Context env = new Context()) {
+      String options = env.mkSolver().getHelp();
+      options += env.mkSimplifier("propagate-values").getHelp();
+      options += env.mkTactic("simplify").getHelp();
+      options += env.mkFixedpoint().getHelp();
+      options += env.mkOptimize().getHelp();
+
+      Set<String> optionsByLine = ImmutableSet.copyOf(Splitter.on('\n').splitToList(options));
+      ImmutableSet.Builder<String> doubleOptionsExtracted = ImmutableSet.builder();
+      for (String line : optionsByLine) {
+        // Z3 options encode the type always following the option name, e.g.: option.name (type)
+        if (line.contains("(double)")) {
+          List<String> optionAndSuffix = Splitter.on(" (double)").splitToList(line);
+          // Make sure there is only one (double) type declaration in the line
+          assertThat(optionAndSuffix).hasSize(2);
+          doubleOptionsExtracted.add(optionAndSuffix.get(0));
+        }
+      }
+
+      assertThat(doubleOptions).containsExactlyElementsIn(doubleOptionsExtracted.build());
+    }
+  }
+
+  private Set<Expr<?>> getFreeVars(Expr<?> expr) {
+    Deque<Expr<?>> worklist = new ArrayDeque<>();
+    worklist.push(expr);
+
+    Set<Expr<?>> vars = new HashSet<>();
+
+    while (!worklist.isEmpty()) {
+      Expr<?> f = worklist.removeFirst();
+      if (f.isConst()) {
+        vars.add(f);
+      }
+      for (Expr<?> c : f.getArgs()) {
+        worklist.addLast(c);
+      }
+    }
+    return vars;
+  }
+
+  @SuppressWarnings("unchecked")
+  private Model solveHornClauses(Context env, List<Expr<BoolSort>> chc) {
+    Params opts = env.mkParams();
+    opts.add("engine", "spacer");
+    opts.add("spacer.order_children", 2);
+    opts.add("xform.inline_eager", false);
+    opts.add("xform.inline_linear", false);
+    opts.add("xform.slice", false);
+    opts.add("spacer.max_level", 10);
+
+    Solver solver = env.mkSolver("HORN");
+    solver.setParameters(opts);
+
+    for (Expr<BoolSort> c : chc) {
+      solver.add(c);
+    }
+    Status status = solver.check();
+
+    assertThat(status).isEqualTo(Status.SATISFIABLE);
+
+    return solver.getModel();
+  }
+
+  private Expr<BoolSort> interpolate(
+      Context env, Expr<BoolSort> formulasA, Expr<BoolSort> formulasB) {
+    Set<Expr<?>> varsA = getFreeVars(formulasA);
+    Set<Expr<?>> varsB = getFreeVars(formulasB);
+
+    Expr<?>[] shared = Sets.intersection(varsA, varsB).toArray(new Expr<?>[0]);
+
+    FuncDecl<BoolSort> symbolItp =
+        env.mkFuncDecl(
+            "Itp", Stream.of(shared).map(Expr::getSort).toArray(Sort[]::new), env.mkBoolSort());
+    Expr<BoolSort> constant = symbolItp.apply(shared);
+
+    Expr<BoolSort> left =
+        env.mkForall(
+            varsA.toArray(new Expr<?>[0]),
+            env.mkImplies(formulasA, constant),
+            1,
+            null,
+            null,
+            null,
+            null);
+
+    Expr<BoolSort> right =
+        env.mkForall(
+            varsB.toArray(new Expr<?>[0]),
+            env.mkImplies(constant, env.mkNot(formulasB)),
+            1,
+            null,
+            null,
+            null,
+            null);
+
+    Model model = solveHornClauses(env, ImmutableList.of(left, right));
+    return model.eval(constant, false);
+  }
+
+  /** Validate that itp is an interpolant for formula(s) A and formula(s) B. */
+  private boolean validate(
+      Context env, Expr<BoolSort> formulasA, Expr<BoolSort> formulasB, Expr<BoolSort> itp) {
+    Solver solver = env.mkSolver("QF_LIA");
+    return solver.check(env.mkNot(env.mkImplies(formulasA, itp))).equals(Status.UNSATISFIABLE)
+        && solver
+            .check(env.mkNot(env.mkImplies(itp, env.mkNot(formulasB))))
+            .equals(Status.UNSATISFIABLE)
+        && Sets.intersection(getFreeVars(formulasA), getFreeVars(formulasB))
+            .containsAll(getFreeVars(itp));
+  }
+}

src/org/sosy_lab/java_smt/solvers/z3/Z3OptimizationProver.java

@@ -31,6 +31,7 @@
 import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.solvers.z3.Z3SolverContext.ENGINE;
 
 class Z3OptimizationProver extends Z3AbstractProver implements OptimizationProverEnvironment {
 
@@ -42,11 +43,13 @@ class Z3OptimizationProver extends Z3AbstractProver implements OptimizationProve
       Z3FormulaCreator creator,
       LogManager pLogger,
       Z3FormulaManager pMgr,
+      Optional<String> pLogic,
+      ENGINE pEngine,
       Set<ProverOptions> pOptions,
       ImmutableMap<String, Object> pSolverOptions,
       @Nullable PathCounterTemplate pLogfile,
       ShutdownNotifier pShutdownNotifier) {
-    super(creator, pMgr, pOptions, pLogfile, pShutdownNotifier);
+    super(creator, pMgr, pLogic, pEngine, pOptions, pLogfile, pShutdownNotifier);
     z3optSolver = Native.mkOptimize(z3context);
     Native.optimizeIncRef(z3context, z3optSolver);
     logger = pLogger;