Module Sidekick_base_solver.Solver

SMT solver, obtained from Sidekick_smt_solver

module T : sig ... end
module Lit : sig ... end
type proof = Solver_arg.proof
type proof_step = Solver_arg.proof_step
module P : sig ... end
module Solver_internal : sig ... end
type solver = t
type term = T.Term.t
type ty = T.Ty.t
type lit = Lit.t
module type THEORY = sig ... end
type theory = (module THEORY)
type !'a theory_p = (module THEORY with type t = 'a)
val mk_theory : name:string -> create_and_setup:(Solver_internal.t -> 'th) -> ?push_level:('th -> unit) -> ?pop_levels:('th -> int -> unit) -> unit -> theory
module Model : sig ... end
module Unknown : sig ... end
val stats : t -> Sidekick_util.Stat.t
val tst : t -> T.Term.store
val ty_st : t -> T.Ty.store
val proof : t -> proof
val create : ?stat:Sidekick_util.Stat.t -> ?size:[ `Big | `Small | `Tiny ] -> proof:proof -> theories:theory list -> T.Term.store -> T.Ty.store -> unit -> t
val add_theory : t -> theory -> unit
val add_theory_p : t -> 'a theory_p -> 'a
val add_theory_l : t -> theory list -> unit
val mk_lit_t : t -> ?sign:bool -> term -> lit
val add_clause : t -> lit Sidekick_util.IArray.t -> proof_step -> unit
val add_clause_l : t -> lit list -> proof_step -> unit
val assert_terms : t -> term list -> unit
val assert_term : t -> term -> unit
type res = Sidekick_smt_solver.Make(Solver_arg).res =
| Sat of Model.t
| Unsat of {
unsat_core : unit -> lit Iter.t;
unsat_proof_step : unit -> proof_step option;
}
| Unknown of Unknown.t
val solve : ?on_exit:(unit -> unit) list -> ?check:bool -> ?on_progress:(t -> unit) -> ?should_stop:(t -> int -> bool) -> assumptions:lit list -> t -> res
val push_assumption : t -> lit -> unit
val pop_assumptions : t -> int -> unit
type propagation_result = Sidekick_smt_solver.Make(Solver_arg).propagation_result =
| PR_sat
| PR_conflict of {
backtracked : int;
}
| PR_unsat of {
unsat_core : unit -> lit Iter.t;
}
val check_sat_propagations_only : assumptions:lit list -> t -> propagation_result
val pp_stats : t CCFormat.printer