Merge pull request #8681 from Z3Prover/copilot/fix-discussion-issues-8680

Add missing solver and model APIs to Go and OCaml bindings

src/api/go/solver.go

@@ -280,6 +280,14 @@ func (s *Solver) CongruenceExplain(a, b *Expr) *Expr {
 	return newExpr(s.ctx, ast)
 }
 
+// SetInitialValue provides an initial value hint for a variable to the solver.
+// This can help guide the solver to find solutions more efficiently.
+// The variable must be a constant or function application, and the value must be
+// compatible with the variable's sort.
+func (s *Solver) SetInitialValue(variable, value *Expr) {
+	C.Z3_solver_set_initial_value(s.ctx.ptr, s.ptr, variable.ptr, value.ptr)
+}
+
 // Model represents a Z3 model (satisfying assignment).
 type Model struct {
 	ctx *Context
@@ -382,3 +390,14 @@ func (fi *FuncInterp) GetElse() *Expr {
 func (fi *FuncInterp) GetArity() uint {
 	return uint(C.Z3_func_interp_get_arity(fi.ctx.ptr, fi.ptr))
 }
+
+// SortUniverse returns the universe of values for an uninterpreted sort in the model.
+// The universe is represented as a list of distinct expressions.
+// Returns nil if the sort is not an uninterpreted sort in this model.
+func (m *Model) SortUniverse(sort *Sort) []*Expr {
+	vec := C.Z3_model_get_sort_universe(m.ctx.ptr, m.ptr, sort.ptr)
+	if vec == nil {
+		return nil
+	}
+	return astVectorToExprs(m.ctx, vec)
+}

src/api/ml/z3.ml

@@ -1940,6 +1940,38 @@ struct
 
   let interrupt (ctx:context) (s:solver) =
     Z3native.solver_interrupt ctx s
+
+  let get_units x =
+    let av = Z3native.solver_get_units (gc x) x in
+    AST.ASTVector.to_expr_list av
+
+  let get_non_units x =
+    let av = Z3native.solver_get_non_units (gc x) x in
+    AST.ASTVector.to_expr_list av
+
+  let get_trail x =
+    let av = Z3native.solver_get_trail (gc x) x in
+    AST.ASTVector.to_expr_list av
+
+  let get_levels x literals =
+    let n = List.length literals in
+    let levels = Array.make n 0 in
+    let av = Z3native.mk_ast_vector (gc x) in
+    List.iter (fun e -> Z3native.ast_vector_push (gc x) av e) literals;
+    Z3native.solver_get_levels (gc x) x av n levels;
+    levels
+
+  let congruence_root x a = Z3native.solver_congruence_root (gc x) x a
+
+  let congruence_next x a = Z3native.solver_congruence_next (gc x) x a
+
+  let congruence_explain x a b = Z3native.solver_congruence_explain (gc x) x a b
+
+  let from_file x = Z3native.solver_from_file (gc x) x
+
+  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
 end
 
 

src/api/ml/z3.mli

@@ -3389,6 +3389,46 @@ sig
       it is more convenient to cancel a specific solver. Solvers
       that are not selected for interrupts are left alone.*)
   val interrupt: context -> solver -> unit
+
+  (** Retrieve the set of units from the solver.
+      Units are clauses of size 1 learned by the solver during solving. *)
+  val get_units : solver -> Expr.expr list
+
+  (** Retrieve the set of non-units from the solver.
+      Non-units are clauses of size greater than 1 learned by the solver. *)
+  val get_non_units : solver -> Expr.expr list
+
+  (** Retrieve the trail (sequence of assignments) from the solver.
+      The trail shows the sequence of literal assignments made by the solver. *)
+  val get_trail : solver -> Expr.expr list
+
+  (** Retrieve the decision levels of trail literals.
+      Given a list of literals from the trail, returns an array of their decision levels.
+      @param literals List of literals from the trail
+      @return Array of decision levels corresponding to the input literals *)
+  val get_levels : solver -> Expr.expr list -> int array
+
+  (** Retrieve the congruence closure root of an expression.
+      Returns the representative of the equivalence class containing the expression. *)
+  val congruence_root : solver -> Expr.expr -> Expr.expr
+
+  (** Retrieve the next element in the congruence closure equivalence class.
+      Congruence classes form a circular list; this returns the next element. *)
+  val congruence_next : solver -> Expr.expr -> Expr.expr
+
+  (** Retrieve an explanation for why two expressions are congruent.
+      Returns an expression that justifies the congruence between a and b. *)
+  val congruence_explain : solver -> Expr.expr -> Expr.expr -> Expr.expr
+
+  (** Parse SMT-LIB2 formulas from a file and assert them into the solver. *)
+  val from_file : solver -> string -> unit
+
+  (** Parse SMT-LIB2 formulas from a string and assert them into the solver. *)
+  val from_string : solver -> string -> unit
+
+  (** 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
 end
 
 (** Fixedpoint solving *)