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

@@ -553,6 +553,38 @@ namespace Microsoft.Z3
 	     }
 	}
 
+        /// <summary>
+        /// Retrieve the trail and their associated decision levels after a <c>Check</c> call.
+        /// The trail contains Boolean literals (decisions and propagations), and the levels
+        /// array contains the corresponding decision levels at which each literal was assigned.
+        /// </summary>
+        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;
+            }
+        }
+
+        /// <summary>
+        /// 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.
+        /// </summary>
+        /// <param name="var">The variable to set an initial value for</param>
+        /// <param name="value">The initial value for the variable</param>
+        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);
+        }
+
         /// <summary>
         /// Create a clone of the current solver with respect to <c>ctx</c>.
         /// </summary>

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<BoolExpr[]> 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<BoolExpr[]>() {
+            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}.
      */