Module `Solver.Solver_internal`

Internal solver, available to theories.

module A = A

module CC_A = CC_A

module CC : Sidekick_core.CC_S with module CC_A = CC_A

type ty = A.Ty.t
type term = A.Term.t
type term_state = A.Term.state
type proof = A.Proof.t
type t: Main type for a solver

type solver = t

module Expl = CC.Expl

module N = CC.N

val tst : t -> term_state
val cc : t -> CC.t: Congruence closure for this solver

module Lit : sig ... end

type lit = Lit.t

Simplifiers

module Simplify : sig ... end

type simplify_hook = Simplify.hook

val add_simplifier : t -> Simplify.hook -> unit
val simplifier : t -> Simplify.t
val simp_t : t -> term -> term

hooks for the theory

type actions

val propagate : t -> actions -> lit -> reason:(unit -> lit list) -> A.Proof.t -> unit
val raise_conflict : t -> actions -> lit list -> A.Proof.t -> 'a: Give a conflict clause to the solver

val propagate : t -> actions -> lit -> (unit -> lit list) -> unit: Propagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology

val propagate_l : t -> actions -> lit -> lit list -> unit: Propagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology

val add_clause_temp : t -> actions -> lit list -> unit: Add local clause to the SAT solver. This clause will be removed when the solver backtracks.

val add_clause_permanent : t -> actions -> lit list -> unit: Add toplevel clause to the SAT solver. This clause will not be backtracked.

val mk_lit : t -> actions -> ?⁠sign:bool -> term -> lit: Create a literal

val add_lit : t -> actions -> lit -> unit: Add the given literal to the SAT solver, so it gets assigned a boolean value

val add_lit_t : t -> actions -> ?⁠sign:bool -> term -> unit: Add the given (signed) bool term to the SAT solver, so it gets assigned a boolean value

val cc_raise_conflict_expl : t -> actions -> Expl.t -> 'a: Raise a conflict with the given congruence closure explanation. it must be a theory tautology that expl ==> absurd. To be used in theories.

val cc_find : t -> N.t -> N.t: Find representative of the node

val cc_merge : t -> actions -> N.t -> N.t -> Expl.t -> unit: Merge these two nodes in the congruence closure, given this explanation. It must be a theory tautology that expl ==> n1 = n2. To be used in theories.

val cc_merge_t : t -> actions -> term -> term -> Expl.t -> unit: Merge these two terms in the congruence closure, given this explanation. See cc_merge

val cc_add_term : t -> term -> N.t: Add/retrieve congruence closure node for this term. To be used in theories

val on_cc_merge : t -> (CC.t -> actions -> N.t -> N.t -> Expl.t -> unit) -> unit: Callback for when two classes containing data for this key are merged

val on_cc_new_term : t -> (CC.t -> N.t -> term -> unit) -> unit: Callback to add data on terms when they are added to the congruence closure

val on_cc_conflict : t -> (CC.t -> lit list -> unit) -> unit: Callback called on every CC conflict

val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list) -> unit) -> unit: Callback called on every CC propagation

val on_partial_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit

This is called very often and should be efficient. It doesn't have to be complete, only correct. It's given only the slice of the trail consisting in new literals.

val on_final_check : t -> (t -> actions -> lit Iter.t -> unit) -> unit

Must be complete (i.e. must raise a conflict if the set of literals is not satisfiable) and can be expensive. The function is given the whole trail.

Preprocessors

These preprocessors turn mixed, raw literals (possibly simplified) into literals suitable for reasoning. Typically some clauses are also added to the solver.

type preprocess_hook = t -> mk_lit:(term -> lit) -> add_clause:(lit list -> unit) -> term -> term option: Given a term, try to preprocess it. Return None if it didn't change. Can also add clauses to define new terms.

val add_preprocess : t -> preprocess_hook -> unit

Main type for a solver