Module Sidekick_base.Solver

include module type of struct include Sidekick_smt_solver.Solver end
type t

The solver's state.

A solver contains a registry so that theories can share data

val mk_theory : name:string -> create_and_setup: ( id:Sidekick_smt_solver.Theory_id.t -> Sidekick_smt_solver.Solver_internal.t -> 'th ) -> ?push_level:( 'th -> unit ) -> ?pop_levels:( 'th -> int -> unit ) -> unit -> Sidekick_smt_solver.Theory.t

Helper to create a theory.

module Unknown : sig ... end

Main API

val stats : t -> Sidekick_util.Stat.t
val create : (module Sidekick_smt_solver.Sigs.ARG) -> ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Tiny | `Small ] -> ?tracer:Sidekick_smt_solver.Tracer.t -> proof:Sidekick_smt_solver.Sigs.proof_trace -> theories:Sidekick_smt_solver.Theory.t list -> Sidekick_smt_solver.Sigs.Term.store -> unit -> t

Create a new solver.

It needs a term state and a type state to manipulate terms and types. All terms and types interacting with this solver will need to come from these exact states.

  • parameter store_proof

    if true, proofs from the SAT solver and theories are retained and potentially accessible after solve returns UNSAT.

  • parameter size

    influences the size of initial allocations.

  • parameter theories

    theories to load from the start. Other theories can be added using add_theory.

val add_theory : t -> Sidekick_smt_solver.Theory.t -> unit

Add a theory to the solver. This should be called before any call to solve or to add_clause and the likes (otherwise the theory will have a partial view of the problem).

val add_theory_p : t -> 'a Sidekick_smt_solver.Theory.p -> 'a

Add the given theory and obtain its state

val add_theory_l : t -> Sidekick_smt_solver.Theory.t list -> unit

mk_lit_t _ ~sign t returns lit', where lit' is preprocess(lit) and lit is an internal representation of ± t.

The proof of |- lit = lit' is directly added to the solver's proof.

add_clause solver cs adds a boolean clause to the solver. Subsequent calls to solve will need to satisfy this clause.

Add a clause to the solver, given as a list.

val assert_terms : t -> Sidekick_smt_solver.Sigs.term list -> unit

Helper that turns each term into an atom, before adding disjunction of the resulting atoms to the solver as a clause assertion

val assert_term : t -> Sidekick_smt_solver.Sigs.term -> unit

Helper that turns the term into an atom, before adding the result to the solver as a unit clause assertion

val add_ty : t -> Sidekick_smt_solver.Sigs.ty -> unit
type res =
| Sat of Sidekick_smt_solver.Sigs.Model.t(*

Satisfiable

*)
| Unsat of {
unsat_core : unit -> Sidekick_smt_solver.Sigs.lit Iter.t;(*

Unsat core (subset of assumptions), or empty

*)
unsat_step_id : unit -> Sidekick_smt_solver.Sigs.step_id option;(*

Proof step for the empty clause

*)
}		(*

Unsatisfiable

*)
| Unknown of Unknown.t(*

Unknown, obtained after a timeout, memory limit, etc.

*)

Result of solving for the current set of clauses

val solve : ?on_exit:( unit -> unit ) list -> ?check:bool -> ?on_progress:( t -> unit ) -> ?should_stop:( t -> int -> bool ) -> assumptions:Sidekick_smt_solver.Sigs.lit list -> t -> res

solve s checks the satisfiability of the clauses added so far to s.

  • parameter check

    if true, the model is checked before returning.

  • parameter on_progress

    called regularly during solving.

  • parameter assumptions

    a set of atoms held to be true. The unsat core, if any, will be a subset of assumptions.

  • parameter should_stop

    a callback regularly called with the solver, and with a number of "steps" done since last call. The exact notion of step is not defined, but is guaranteed to increase regularly. The function should return true if it judges solving must stop (returning Unknown), false if solving can proceed.

  • parameter on_exit

    functions to be run before this returns

val last_res : t -> res option

Last result, if any. Some operations will erase this (e.g. assert_term).

val push_assumption : t -> Sidekick_smt_solver.Sigs.lit -> unit

Pushes an assumption onto the assumption stack. It will remain there until it's pop'd by pop_assumptions.

val pop_assumptions : t -> int -> unit

pop_assumptions solver n removes n assumptions from the stack. It removes the assumptions that were the most recently added via push_assumptions. Note that check_sat_propagations_only can call this if it meets a conflict.

type propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> Sidekick_smt_solver.Sigs.lit Iter.t;
}
val check_sat_propagations_only : assumptions:Sidekick_smt_solver.Sigs.lit list -> t -> propagation_result

check_sat_propagations_only solver uses assumptions (including the assumptions parameter, and atoms previously added via push_assumptions) and boolean+theory propagation to quickly assess satisfiability. It is not complete; calling solve is required to get an accurate result.

  • returns

    one of:

    • PR_sat if the current state seems satisfiable
    • PR_conflict {backtracked=n} if a conflict was found and resolved, leading to backtracking n levels of assumptions
    • PR_unsat … if the assumptions were found to be unsatisfiable, with the given core.
val pp_stats : t CCFormat.printer

Print some statistics. What it prints exactly is unspecified.

val default_arg : (module Sidekick_smt_solver.Sigs.ARG)
val create_default : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Small | `Tiny ] -> ?tracer:Sidekick_smt_solver.Tracer.t -> proof:Sidekick_smt_solver.Sigs.proof_trace -> theories:Sidekick_smt_solver.Theory.t list -> Sidekick_smt_solver.Sigs.Term.store -> t