Merge pull request #8702 from Z3Prover/copilot/fix-issues-in-discussion-8701

Add missing solver/optimizer API bindings across language targets

src/api/dotnet/Optimize.cs

@@ -437,6 +437,16 @@ namespace Microsoft.Z3
         }
 
 
+        /// <summary>
+        /// Set an initial value for a variable to guide the optimizer's search heuristics.
+        /// </summary>
+        public void SetInitialValue(Expr var, Expr value)
+        {
+            Debug.Assert(var != null);
+            Debug.Assert(value != null);
+            Native.Z3_optimize_set_initial_value(Context.nCtx, NativeObject, var.NativeObject, value.NativeObject);
+        }
+
         /// <summary>
         /// Optimize statistics.
         /// </summary>

src/api/go/solver.go

@@ -288,6 +288,68 @@ func (s *Solver) SetInitialValue(variable, value *Expr) {
 	C.Z3_solver_set_initial_value(s.ctx.ptr, s.ptr, variable.ptr, value.ptr)
 }
 
+// Cube extracts a cube (conjunction of literals) from the solver state.
+// vars is an optional list of variables to use as cube variables; if nil, the solver decides.
+// cutoff specifies the backtrack level cutoff for cube generation.
+// Returns a slice of expressions representing the cube, or nil when the search space is exhausted.
+func (s *Solver) Cube(vars []*Expr, cutoff uint) []*Expr {
+	varVec := C.Z3_mk_ast_vector(s.ctx.ptr)
+	C.Z3_ast_vector_inc_ref(s.ctx.ptr, varVec)
+	defer C.Z3_ast_vector_dec_ref(s.ctx.ptr, varVec)
+	for _, v := range vars {
+		C.Z3_ast_vector_push(s.ctx.ptr, varVec, v.ptr)
+	}
+	result := C.Z3_solver_cube(s.ctx.ptr, s.ptr, varVec, C.uint(cutoff))
+	return astVectorToExprs(s.ctx, result)
+}
+
+// GetConsequences retrieves fixed assignments for variables given assumptions.
+// Returns the status and the set of consequences as implications.
+func (s *Solver) GetConsequences(assumptions []*Expr, variables []*Expr) (Status, []*Expr) {
+	asmVec := C.Z3_mk_ast_vector(s.ctx.ptr)
+	C.Z3_ast_vector_inc_ref(s.ctx.ptr, asmVec)
+	defer C.Z3_ast_vector_dec_ref(s.ctx.ptr, asmVec)
+	varVec := C.Z3_mk_ast_vector(s.ctx.ptr)
+	C.Z3_ast_vector_inc_ref(s.ctx.ptr, varVec)
+	defer C.Z3_ast_vector_dec_ref(s.ctx.ptr, varVec)
+	consVec := C.Z3_mk_ast_vector(s.ctx.ptr)
+	C.Z3_ast_vector_inc_ref(s.ctx.ptr, consVec)
+	defer C.Z3_ast_vector_dec_ref(s.ctx.ptr, consVec)
+	for _, a := range assumptions {
+		C.Z3_ast_vector_push(s.ctx.ptr, asmVec, a.ptr)
+	}
+	for _, v := range variables {
+		C.Z3_ast_vector_push(s.ctx.ptr, varVec, v.ptr)
+	}
+	r := Status(C.Z3_solver_get_consequences(s.ctx.ptr, s.ptr, asmVec, varVec, consVec))
+	return r, astVectorToExprs(s.ctx, consVec)
+}
+
+// SolveFor solves constraints treating given variables symbolically.
+// variables are the variables to solve for, terms are the substitution terms,
+// and guards are the Boolean guards for the substitutions.
+func (s *Solver) SolveFor(variables []*Expr, terms []*Expr, guards []*Expr) {
+	varVec := C.Z3_mk_ast_vector(s.ctx.ptr)
+	C.Z3_ast_vector_inc_ref(s.ctx.ptr, varVec)
+	defer C.Z3_ast_vector_dec_ref(s.ctx.ptr, varVec)
+	termVec := C.Z3_mk_ast_vector(s.ctx.ptr)
+	C.Z3_ast_vector_inc_ref(s.ctx.ptr, termVec)
+	defer C.Z3_ast_vector_dec_ref(s.ctx.ptr, termVec)
+	guardVec := C.Z3_mk_ast_vector(s.ctx.ptr)
+	C.Z3_ast_vector_inc_ref(s.ctx.ptr, guardVec)
+	defer C.Z3_ast_vector_dec_ref(s.ctx.ptr, guardVec)
+	for _, v := range variables {
+		C.Z3_ast_vector_push(s.ctx.ptr, varVec, v.ptr)
+	}
+	for _, t := range terms {
+		C.Z3_ast_vector_push(s.ctx.ptr, termVec, t.ptr)
+	}
+	for _, g := range guards {
+		C.Z3_ast_vector_push(s.ctx.ptr, guardVec, g.ptr)
+	}
+	C.Z3_solver_solve_for(s.ctx.ptr, s.ptr, varVec, termVec, guardVec)
+}
+
 // Model represents a Z3 model (satisfying assignment).
 type Model struct {
 	ctx *Context

src/api/java/Optimize.java

@@ -397,6 +397,22 @@ public class Optimize extends Z3Object {
         return objectives.ToExprArray();
     }
 
+    /**
+     * Set an initial value for a variable to guide the optimizer's search heuristics.
+     * This can improve performance when a good initial value is known for the variable.
+     *
+     * @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.optimizeSetInitialValue(getContext().nCtx(), getNativeObject(),
+            var.getNativeObject(), value.getNativeObject());
+    }
+
     /**
      *  Optimize statistics.
      **/

src/api/java/Solver.java

@@ -464,6 +464,74 @@ public class Solver extends Z3Object {
         };
     }
 
+    /**
+     * Return the congruence class representative of the given expression.
+     * This is useful for querying the equality reasoning performed by the solver.
+     *
+     * @param t The expression to find the congruence root for
+     * @return The root expression of the congruence class
+     * @throws Z3Exception
+     **/
+    public Expr<?> getCongruenceRoot(Expr<?> t)
+    {
+        getContext().checkContextMatch(t);
+        return Expr.create(getContext(),
+            Native.solverCongruenceRoot(getContext().nCtx(), getNativeObject(), t.getNativeObject()));
+    }
+
+    /**
+     * Return the next element in the congruence class of the given expression.
+     * The congruence class forms a circular linked list.
+     *
+     * @param t The expression to find the next congruent expression for
+     * @return The next expression in the congruence class
+     * @throws Z3Exception
+     **/
+    public Expr<?> getCongruenceNext(Expr<?> t)
+    {
+        getContext().checkContextMatch(t);
+        return Expr.create(getContext(),
+            Native.solverCongruenceNext(getContext().nCtx(), getNativeObject(), t.getNativeObject()));
+    }
+
+    /**
+     * Return an explanation for why two expressions are congruent.
+     *
+     * @param a First expression
+     * @param b Second expression
+     * @return An expression explaining the congruence between a and b
+     * @throws Z3Exception
+     **/
+    public Expr<?> getCongruenceExplain(Expr<?> a, Expr<?> b)
+    {
+        getContext().checkContextMatch(a);
+        getContext().checkContextMatch(b);
+        return Expr.create(getContext(),
+            Native.solverCongruenceExplain(getContext().nCtx(), getNativeObject(),
+                a.getNativeObject(), b.getNativeObject()));
+    }
+
+    /**
+     * Solve constraints for given variables, replacing their occurrences by terms.
+     * Guards are used to guard substitutions.
+     *
+     * @param variables Array of variables to solve for
+     * @param terms Array of terms to substitute for the variables
+     * @param guards Array of Boolean guards for the substitutions
+     * @throws Z3Exception
+     **/
+    public void solveFor(Expr<?>[] variables, Expr<?>[] terms, BoolExpr[] guards)
+    {
+        ASTVector vars = new ASTVector(getContext());
+        ASTVector termVec = new ASTVector(getContext());
+        ASTVector guardVec = new ASTVector(getContext());
+        for (Expr<?> v : variables) vars.push(v);
+        for (Expr<?> t : terms) termVec.push(t);
+        for (BoolExpr g : guards) guardVec.push(g);
+        Native.solverSolveFor(getContext().nCtx(), getNativeObject(),
+            vars.getNativeObject(), termVec.getNativeObject(), guardVec.getNativeObject());
+    }
+
     /**
      * 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.

src/api/js/src/high-level/high-level.ts

@@ -2147,6 +2147,79 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new AstVectorImpl(check(Z3.solver_get_trail(contextPtr, this.ptr)));
       }
 
+      trailLevels(): number[] {
+        const trailVec = check(Z3.solver_get_trail(contextPtr, this.ptr));
+        const n = Z3.ast_vector_size(contextPtr, trailVec);
+        return check(Z3.solver_get_levels(contextPtr, this.ptr, trailVec, n));
+      }
+
+      async cube(vars?: AstVector<Name, Bool<Name>>, cutoff: number = 0xFFFFFFFF): Promise<AstVector<Name, Bool<Name>>> {
+        const tempVars = vars ?? new AstVectorImpl();
+        const result = await asyncMutex.runExclusive(() =>
+          check(Z3.solver_cube(contextPtr, this.ptr, tempVars.ptr, cutoff)),
+        );
+        return new AstVectorImpl(result);
+      }
+
+      async getConsequences(
+        assumptions: (Bool<Name> | AstVector<Name, Bool<Name>>)[],
+        variables: Expr<Name>[],
+      ): Promise<[CheckSatResult, AstVector<Name, Bool<Name>>]> {
+        const asmsVec = new AstVectorImpl();
+        const varsVec = new AstVectorImpl();
+        const consVec = new AstVectorImpl<Bool<Name>>();
+        _flattenArgs(assumptions).forEach(expr => {
+          _assertContext(expr);
+          Z3.ast_vector_push(contextPtr, asmsVec.ptr, expr.ast);
+        });
+        variables.forEach(v => {
+          _assertContext(v);
+          Z3.ast_vector_push(contextPtr, varsVec.ptr, v.ast);
+        });
+        const r = await asyncMutex.runExclusive(() =>
+          check(Z3.solver_get_consequences(contextPtr, this.ptr, asmsVec.ptr, varsVec.ptr, consVec.ptr)),
+        );
+        let status: CheckSatResult;
+        switch (r) {
+          case Z3_lbool.Z3_L_FALSE:
+            status = 'unsat';
+            break;
+          case Z3_lbool.Z3_L_TRUE:
+            status = 'sat';
+            break;
+          default:
+            status = 'unknown';
+        }
+        return [status, consVec];
+      }
+
+      solveFor(variables: Expr<Name>[], terms: Expr<Name>[], guards: Bool<Name>[]): void {
+        const varsVec = new AstVectorImpl();
+        const termsVec = new AstVectorImpl();
+        const guardsVec = new AstVectorImpl();
+        variables.forEach(v => {
+          _assertContext(v);
+          Z3.ast_vector_push(contextPtr, varsVec.ptr, v.ast);
+        });
+        terms.forEach(t => {
+          _assertContext(t);
+          Z3.ast_vector_push(contextPtr, termsVec.ptr, t.ast);
+        });
+        guards.forEach(g => {
+          _assertContext(g);
+          Z3.ast_vector_push(contextPtr, guardsVec.ptr, g.ast);
+        });
+        Z3.solver_solve_for(contextPtr, this.ptr, varsVec.ptr, termsVec.ptr, guardsVec.ptr);
+        throwIfError();
+      }
+
+      setInitialValue(variable: Expr<Name>, value: Expr<Name>): void {
+        _assertContext(variable);
+        _assertContext(value);
+        Z3.solver_set_initial_value(contextPtr, this.ptr, variable.ast, value.ast);
+        throwIfError();
+      }
+
       congruenceRoot(expr: Expr<Name>): Expr<Name> {
         _assertContext(expr);
         return _toExpr(check(Z3.solver_congruence_root(contextPtr, this.ptr, expr.ast)));
@@ -2267,6 +2340,13 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new StatisticsImpl(check(Z3.optimize_get_statistics(contextPtr, this.ptr)));
       }
 
+      setInitialValue(variable: Expr<Name>, value: Expr<Name>): void {
+        _assertContext(variable);
+        _assertContext(value);
+        Z3.optimize_set_initial_value(contextPtr, this.ptr, variable.ast, value.ast);
+        throwIfError();
+      }
+
       toString() {
         return check(Z3.optimize_to_string(contextPtr, this.ptr));
       }

src/api/js/src/high-level/types.ts

@@ -1190,6 +1190,105 @@ export interface Solver<Name extends string = 'main'> {
    */
   trail(): AstVector<Name, Bool<Name>>;
 
+  /**
+   * Retrieve the decision levels for each literal in the solver's trail.
+   * The returned array has one entry per trail literal, indicating at which
+   * decision level it was assigned.
+   *
+   * @returns An array of numbers where element i is the decision level of the i-th trail literal
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Bool.const('x');
+   * solver.add(x);
+   * await solver.check();
+   * const levels = solver.trailLevels();
+   * console.log('Trail levels:', levels);
+   * ```
+   */
+  trailLevels(): number[];
+
+  /**
+   * Extract cubes from the solver for cube-and-conquer parallel solving.
+   * Each call returns the next cube (conjunction of literals) from the solver.
+   * Returns an empty AstVector when the search space is exhausted.
+   *
+   * @param vars - Optional vector of variables to use as cube variables
+   * @param cutoff - Backtrack level cutoff for cube generation (default: 0xFFFFFFFF)
+   * @returns A promise resolving to an AstVector containing the cube literals
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Bool.const('x');
+   * const y = Bool.const('y');
+   * solver.add(x.or(y));
+   * const cube = await solver.cube(undefined, 1);
+   * console.log('Cube length:', cube.length());
+   * ```
+   */
+  cube(vars?: AstVector<Name, Bool<Name>>, cutoff?: number): Promise<AstVector<Name, Bool<Name>>>;
+
+  /**
+   * Retrieve fixed assignments to a set of variables as consequences given assumptions.
+   * Each consequence is an implication: assumptions => variable = value.
+   *
+   * @param assumptions - Assumptions to use during consequence finding
+   * @param variables - Variables to find consequences for
+   * @returns A promise resolving to the status and a vector of consequence expressions
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Bool.const('x');
+   * const y = Bool.const('y');
+   * solver.add(x.implies(y));
+   * const [status, consequences] = await solver.getConsequences([], [x, y]);
+   * ```
+   */
+  getConsequences(
+    assumptions: (Bool<Name> | AstVector<Name, Bool<Name>>)[],
+    variables: Expr<Name>[],
+  ): Promise<[CheckSatResult, AstVector<Name, Bool<Name>>]>;
+
+  /**
+   * Solve constraints treating given variables symbolically, replacing their
+   * occurrences by terms. Guards condition the substitutions.
+   *
+   * @param variables - Variables to solve for
+   * @param terms - Substitution terms for the variables
+   * @param guards - Boolean guards for the substitutions
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Int.const('x');
+   * const y = Int.const('y');
+   * solver.add(x.eq(y.add(1)));
+   * solver.solveFor([x], [y.add(1)], []);
+   * ```
+   */
+  solveFor(variables: Expr<Name>[], terms: Expr<Name>[], guards: Bool<Name>[]): void;
+
+  /**
+   * Set an initial value hint for a variable to guide the solver's search heuristics.
+   * This can improve performance when a good initial value is known.
+   *
+   * @param variable - The variable to set an initial value for
+   * @param value - The initial value for the variable
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Int.const('x');
+   * solver.setInitialValue(x, Int.val(42));
+   * solver.add(x.gt(0));
+   * await solver.check();
+   * ```
+   */
+  setInitialValue(variable: Expr<Name>, value: Expr<Name>): void;
+
   /**
    * Retrieve the root of the congruence class containing the given expression.
    * This is useful for understanding equality reasoning in the solver.
@@ -1357,6 +1456,25 @@ export interface Optimize<Name extends string = 'main'> {
 
   statistics(): Statistics<Name>;
 
+  /**
+   * Set an initial value hint for a variable to guide the optimizer's search heuristics.
+   * This can improve performance when a good initial value is known.
+   *
+   * @param variable - The variable to set an initial value for
+   * @param value - The initial value for the variable
+   *
+   * @example
+   * ```typescript
+   * const opt = new Optimize();
+   * const x = Int.const('x');
+   * opt.setInitialValue(x, Int.val(42));
+   * opt.add(x.gt(0));
+   * opt.maximize(x);
+   * await opt.check();
+   * ```
+   */
+  setInitialValue(variable: Expr<Name>, value: Expr<Name>): void;
+
   /**
    * Manually decrease the reference count of the optimize
    * This is automatically done when the optimize is garbage collected,

src/api/ml/z3.ml

@@ -1989,6 +1989,35 @@ struct
   let from_string x = Z3native.solver_from_string (gc x) x
 
   let set_initial_value x var value = Z3native.solver_set_initial_value (gc x) x var value
+
+  let cube x variables cutoff =
+    let av = Z3native.mk_ast_vector (gc x) in
+    List.iter (fun e -> Z3native.ast_vector_push (gc x) av e) variables;
+    let result = Z3native.solver_cube (gc x) x av cutoff in
+    AST.ASTVector.to_expr_list result
+
+  let get_consequences x assumptions variables =
+    let asms = Z3native.mk_ast_vector (gc x) in
+    let vars = Z3native.mk_ast_vector (gc x) in
+    let cons = Z3native.mk_ast_vector (gc x) in
+    List.iter (fun e -> Z3native.ast_vector_push (gc x) asms e) assumptions;
+    List.iter (fun e -> Z3native.ast_vector_push (gc x) vars e) variables;
+    let r = Z3native.solver_get_consequences (gc x) x asms vars cons in
+    let status = match lbool_of_int r with
+      | L_TRUE -> SATISFIABLE
+      | L_FALSE -> UNSATISFIABLE
+      | _ -> UNKNOWN
+    in
+    (status, AST.ASTVector.to_expr_list cons)
+
+  let solve_for x variables terms guards =
+    let var_vec = Z3native.mk_ast_vector (gc x) in
+    let term_vec = Z3native.mk_ast_vector (gc x) in
+    let guard_vec = Z3native.mk_ast_vector (gc x) in
+    List.iter (fun e -> Z3native.ast_vector_push (gc x) var_vec e) variables;
+    List.iter (fun e -> Z3native.ast_vector_push (gc x) term_vec e) terms;
+    List.iter (fun e -> Z3native.ast_vector_push (gc x) guard_vec e) guards;
+    Z3native.solver_solve_for (gc x) x var_vec term_vec guard_vec
 end
 
 

src/api/ml/z3.mli

@@ -3476,6 +3476,22 @@ sig
   (** Provide an initial value hint for a variable to the solver.
       This can help guide the solver to find solutions more efficiently. *)
   val set_initial_value : solver -> Expr.expr -> Expr.expr -> unit
+
+  (** Extract cubes from the solver for cube-and-conquer parallel solving.
+      vars is a list of variables to use as cube variables; use an empty list for automatic selection.
+      cutoff is the backtrack level cutoff for cube generation.
+      Returns a list of expressions representing the cube literals. *)
+  val cube : solver -> Expr.expr list -> int -> Expr.expr list
+
+  (** Retrieve fixed assignments to variables as consequences given assumptions.
+      Returns the solver status and a list of consequence expressions.
+      Each consequence is an implication: assumptions => variable = value. *)
+  val get_consequences : solver -> Expr.expr list -> Expr.expr list -> status * Expr.expr list
+
+  (** Solve constraints treating given variables symbolically.
+      variables are the variables to solve for, terms are the substitution terms,
+      and guards are Boolean guards for the substitutions. *)
+  val solve_for : solver -> Expr.expr list -> Expr.expr list -> Expr.expr list -> unit
 end
 
 (** Fixedpoint solving *)