The Incremental module, like Batch, presents a solver parameterized by the mapping module M. In this mode, the Incremental solver engages with the underlying SMT solver in nearly every interaction.
module _ : Mappings_intf.Sval solver_time : float Smtml_prelude.refsolver_time tracks the time spent inside the SMT solver.
val solver_count : int Smtml_prelude.refsolver_count tracks the number of queries made to the SMT solver.
pp_statistics fmt solver pretty-prints solver statistics using the formatter fmt.
create ?params ?logic () creates a new solver.
val interrupt : t -> unitinterrupt solver interrupts the current solver operation.
val push : t -> unitpush solver creates a backtracking point in the solver solver.
val pop : t -> int -> unitpop solver n backtracks n backtracking points in the solver solver.
val reset : t -> unitreset solver resets the solver solver, removing all assertions.
add solver exprs asserts one or multiple constraints exprs into the solver solver.
val add_set : t -> Expr.Set.t -> unitadd_set solver set asserts constraints from the set set into the solver solver.
get_assertions solver retrieves the set of assertions in the solver solver.
val get_statistics : t -> Statistics.tget_statistics solver retrieves statistics from the solver solver.
check solver es checks the satisfiability of the assertions in the solver solver using the assumptions in es. Returns `Sat, `Unsat, or `Unknown.
val check_set : t -> Expr.Set.t -> [ `Sat | `Unsat | `Unknown ]check_set solver set checks the satisfiability of the assertions in the solver solver using the assumptions in the set set. Returns `Sat, `Unsat, or `Unknown.
get_value solver expr retrieves an expression denoting the model value of the given expression expr. Requires that the last check query returned `Sat.
model ?symbols solver retrieves the model of the last check query. If ?symbols is provided, only the values of the specified symbols are included. Returns None if check was not invoked before or its result was not `Sat.
@warning Not compatible with cached solver mode - use get_sat_model instead
get_sat_model For cached solver-compatible alternative
val get_sat_model :
?symbols:Symbol.t list ->
t ->
Expr.Set.t ->
[ `Model of Model.t | `Unsat | `Unknown ]Compute and retrieve a model for specific constraints.
get_sat_model ?symbols solver exprs performs: 1. check_set with exprs constraints 2. Returns model if result is `Sat
Filters output using ?symbols when provided. Designed for cached solvers.
@see model For non-cached solvers when you have already performed your own check/check_set and want to retrieve the results