diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index 3a54df5d9..da3b1eb52 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -437,6 +437,16 @@ namespace Microsoft.Z3 } + /// + /// Set an initial value for a variable to guide the optimizer's search heuristics. + /// + 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); + } + /// /// Optimize statistics. /// diff --git a/src/api/go/solver.go b/src/api/go/solver.go index bbda4f42e..2f14b6479 100644 --- a/src/api/go/solver.go +++ b/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 diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index 391cf943c..9364b8dff 100644 --- a/src/api/java/Optimize.java +++ b/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. **/ diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index adeeb6234..8efa977c4 100644 --- a/src/api/java/Solver.java +++ b/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. diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index bed9313bb..9aaa6a1a4 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/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>, cutoff: number = 0xFFFFFFFF): Promise>> { + 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 | AstVector>)[], + variables: Expr[], + ): Promise<[CheckSatResult, AstVector>]> { + const asmsVec = new AstVectorImpl(); + const varsVec = new AstVectorImpl(); + const consVec = new AstVectorImpl>(); + _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[], terms: Expr[], guards: Bool[]): 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, value: Expr): void { + _assertContext(variable); + _assertContext(value); + Z3.solver_set_initial_value(contextPtr, this.ptr, variable.ast, value.ast); + throwIfError(); + } + congruenceRoot(expr: Expr): Expr { _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, value: Expr): 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)); } diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 4a6d13f2d..e6d29f340 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -1190,6 +1190,105 @@ export interface Solver { */ trail(): AstVector>; + /** + * 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>, cutoff?: number): Promise>>; + + /** + * 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 | AstVector>)[], + variables: Expr[], + ): Promise<[CheckSatResult, AstVector>]>; + + /** + * 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[], terms: Expr[], guards: Bool[]): 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, value: Expr): 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 { statistics(): Statistics; + /** + * 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, value: Expr): void; + /** * Manually decrease the reference count of the optimize * This is automatically done when the optimize is garbage collected, diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index af170808e..40e0a1451 100644 --- a/src/api/ml/z3.ml +++ b/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 diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 11aec782e..5c13941aa 100644 --- a/src/api/ml/z3.mli +++ b/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 *)