Module `Solver.Solver_internal`

module T : sig ... end

module P : sig ... end

type ty = T.Ty.t
type term = T.Term.t
type term_store = T.Term.store
type ty_store = T.Ty.store
type proof = P.t
type t = Sidekick_msat_solver.Make(Solver_arg).Solver_internal.t
type solver = t

val tst : t -> term_store
val ty_st : t -> ty_store
val stats : t -> Sidekick_util.Stat.t

type actions = Sidekick_msat_solver.Make(Solver_arg).Solver_internal.actions

module Lit : sig ... end

type lit = Lit.t

val define_const : t -> const:term -> rhs:term -> unit

module CC : sig ... end

val cc : t -> CC.t

module Simplify : sig ... end

type simplify_hook = Simplify.hook

val add_simplifier : t -> Simplify.hook -> unit
val simplifier : t -> Simplify.t
val simplify_t : t -> term -> (term * proof) option
val simp_t : t -> term -> term * proof
val raise_conflict : t -> actions -> lit list -> proof -> 'a
val push_decision : t -> actions -> lit -> unit
val propagate : t -> actions -> lit -> reason:(unit -> lit list * proof) -> unit
val propagate_l : t -> actions -> lit -> lit list -> proof -> unit
val add_clause_temp : t -> actions -> lit list -> proof -> unit
val add_clause_permanent : t -> actions -> lit list -> proof -> unit
val mk_lit : t -> actions -> ?⁠sign:bool -> term -> lit
val preprocess_term : t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * proof
val add_lit : t -> actions -> lit -> unit
val add_lit_t : t -> actions -> ?⁠sign:bool -> term -> unit
val cc_raise_conflict_expl : t -> actions -> CC.Expl.t -> 'a
val cc_find : t -> CC.N.t -> CC.N.t
val cc_are_equal : t -> term -> term -> bool
val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
val cc_merge_t : t -> actions -> term -> term -> CC.Expl.t -> unit
val cc_add_term : t -> term -> CC.N.t
val cc_mem_term : t -> term -> bool
val on_cc_pre_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit
val on_cc_post_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> unit) -> unit
val on_cc_new_term : t -> (CC.t -> CC.N.t -> term -> unit) -> unit
val on_cc_is_subterm : t -> (CC.N.t -> term -> unit) -> unit
val on_cc_conflict : t -> (CC.t -> th:bool -> lit list -> unit) -> unit
val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * proof) -> unit) -> unit
val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit
val on_final_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit

type preprocess_hook = t -> mk_lit:(term -> lit) -> add_clause:(lit list -> proof -> unit) -> term -> (term * proof) option

val on_preprocess : t -> preprocess_hook -> unit

type model_hook = recurse:(t -> CC.N.t -> term) -> t -> CC.N.t -> term option

val on_model_gen : t -> model_hook -> unit