From f5a44cf0b914d509ffb0105419797c8030616ff0 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Mon, 2 Feb 2026 09:01:01 -0800
Subject: [PATCH] Add missing solver APIs to Java and C# bindings (#8464)
* Initial plan
* Add missing solver APIs for Java and C#
- Issue 3: Add getTrailLevels() to Java and TrailLevels property to C#
- Issue 4: Add cube() iterator to Java (C# already had Cube())
- Issue 5: Add setInitialValue() to Java and SetInitialValue() to C#
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix code review feedback: eliminate redundant trail retrieval
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Improve documentation and efficiency based on code review
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
src/api/dotnet/Solver.cs | 32 ++++++++++++++
src/api/java/Solver.java | 90 ++++++++++++++++++++++++++++++++++++++++
2 files changed, 122 insertions(+)
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 19e798452..4b57257d8 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -553,6 +553,38 @@ namespace Microsoft.Z3
}
}
+ ///
+ /// Retrieve the trail and their associated decision levels after a Check call.
+ /// The trail contains Boolean literals (decisions and propagations), and the levels
+ /// array contains the corresponding decision levels at which each literal was assigned.
+ ///
+ public uint[] TrailLevels
+ {
+ get
+ {
+ using ASTVector trail = new ASTVector(Context, Native.Z3_solver_get_trail(Context.nCtx, NativeObject));
+ uint[] levels = new uint[trail.Size];
+ Native.Z3_solver_get_levels(Context.nCtx, NativeObject, trail.NativeObject, (uint)trail.Size, levels);
+ return levels;
+ }
+ }
+
+ ///
+ /// Set an initial value for a variable to guide the solver's search heuristics.
+ /// This can improve performance when good initial values are known for the problem domain.
+ ///
+ /// The variable to set an initial value for
+ /// The initial value for the variable
+ public void SetInitialValue(Expr var, Expr value)
+ {
+ Debug.Assert(var != null);
+ Debug.Assert(value != null);
+
+ Context.CheckContextMatch(var);
+ Context.CheckContextMatch(value);
+ Native.Z3_solver_set_initial_value(Context.nCtx, NativeObject, var.NativeObject, value.NativeObject);
+ }
+
///
/// Create a clone of the current solver with respect to ctx.
///
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index b34b72e3b..adeeb6234 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -390,6 +390,96 @@ public class Solver extends Z3Object {
getNativeObject());
}
+ /**
+ * Retrieve the decision levels for each literal in the solver's trail after a {@code check} call.
+ * The trail contains Boolean literals (decisions and propagations) in the order they were assigned.
+ * The returned array has one entry per trail literal, indicating at which decision level it was assigned.
+ * Use {@link #getTrail()} to retrieve the trail literals themselves.
+ *
+ * @return An array where element i contains the decision level for the i-th trail literal
+ * @throws Z3Exception
+ **/
+ public int[] getTrailLevels()
+ {
+ ASTVector trailVector = new ASTVector(getContext(), Native.solverGetTrail(getContext().nCtx(), getNativeObject()));
+ int[] levels = new int[trailVector.size()];
+ Native.solverGetLevels(getContext().nCtx(), getNativeObject(), trailVector.getNativeObject(), trailVector.size(), levels);
+ return levels;
+ }
+
+ /**
+ * Return a sequence of cubes (conjunctions of literals) for partitioning the search space.
+ * Each cube represents a partial assignment that can be used as a starting point for parallel solving.
+ * This is primarily useful for cube-and-conquer parallel SAT solving strategies, where different
+ * cubes can be solved independently by different workers.
+ * The iterator yields cubes until the search space is exhausted.
+ *
+ * @param vars Optional array of variables to use as initial cube variables. If null, solver decides.
+ * @param cutoff Backtrack level cutoff for cube generation
+ * @return Iterator over arrays of Boolean expressions representing cubes
+ * @throws Z3Exception
+ **/
+ public java.util.Iterator cube(Expr[] vars, int cutoff)
+ {
+ ASTVector cubeVars = new ASTVector(getContext());
+ if (vars != null) {
+ for (Expr v : vars) {
+ cubeVars.push(v);
+ }
+ }
+
+ return new java.util.Iterator() {
+ private BoolExpr[] nextCube = computeNext();
+
+ private BoolExpr[] computeNext() {
+ ASTVector result = new ASTVector(getContext(),
+ Native.solverCube(getContext().nCtx(), getNativeObject(),
+ cubeVars.getNativeObject(), cutoff));
+ BoolExpr[] cube = result.ToBoolExprArray();
+
+ // Check for termination conditions
+ if (cube.length == 1 && cube[0].isFalse()) {
+ return null; // No more cubes
+ }
+ if (cube.length == 0) {
+ return null; // Search space exhausted
+ }
+ return cube;
+ }
+
+ @Override
+ public boolean hasNext() {
+ return nextCube != null;
+ }
+
+ @Override
+ public BoolExpr[] next() {
+ if (nextCube == null) {
+ throw new java.util.NoSuchElementException();
+ }
+ BoolExpr[] current = nextCube;
+ nextCube = computeNext();
+ return current;
+ }
+ };
+ }
+
+ /**
+ * Set an initial value for a variable to guide the solver's search heuristics.
+ * This can improve performance when good initial values are known for the problem domain.
+ *
+ * @param var The variable to set an initial value for
+ * @param value The initial value for the variable
+ * @throws Z3Exception
+ **/
+ public void setInitialValue(Expr var, Expr value)
+ {
+ getContext().checkContextMatch(var);
+ getContext().checkContextMatch(value);
+ Native.solverSetInitialValue(getContext().nCtx(), getNativeObject(),
+ var.getNativeObject(), value.getNativeObject());
+ }
+
/**
* Create a clone of the current solver with respect to{@code ctx}.
*/