Module `Solver.Solver_internal`

Internal solver, available to theories.

module T = T

module P = P

type ty = T.Ty.t
type term = T.Term.t
type term_state = T.Term.state
type ty_state = T.Ty.state
type proof = P.t
type t: Main type for a solver

type solver = t

val tst : t -> term_state
val ty_st : t -> ty_state
val stats : t -> Sidekick_util.Stat.t

Actions for the theories

type actions: Handle that the theories can use to perform actions.

module Lit = Lit

type lit = Lit.t

Proof helpers

val define_const : t -> const:term -> rhs:term -> unit: define_const si ~const ~rhs adds the definition const := rhs to the (future) proof. const should be a fresh constant that occurs nowhere else, and rhs a term defined without const.

Congruence Closure

module CC : Sidekick_core.CC_S with module T = T and module P = P and module Lit = Lit and type Actions.t = actions: Congruence closure instance

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

Simplifiers

module Simplify : sig ... end: Simplify terms

type simplify_hook = Simplify.hook

val add_simplifier : t -> Simplify.hook -> unit: Add a simplifier hook for preprocessing.

val simplifier : t -> Simplify.t
val simplify_t : t -> term -> (term * proof) option: Simplify input term, returns Some (u, |- t=u) if some simplification occurred.

val simp_t : t -> term -> term * proof: simp_t si t returns u, |- t=u even if no simplification occurred (in which case t == u syntactically). (see simplifier)

hooks for the theory

val raise_conflict : t -> actions -> lit list -> proof -> 'a: Give a conflict clause to the solver

val push_decision : t -> actions -> lit -> unit: Ask the SAT solver to decide the given literal in an extension of the current trail. This is useful for theory combination. If the SAT solver backtracks, this (potential) decision is removed and forgotten.

val propagate : t -> actions -> lit -> reason:(unit -> lit list * proof) -> 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 -> proof -> 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 -> proof -> 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 -> proof -> 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. This automatically preprocesses the term.

val preprocess_term : t -> add_clause:(Lit.t list -> proof -> unit) -> term -> term * proof: Preprocess a term.

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 -> CC.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 -> CC.N.t -> CC.N.t: Find representative of the node

val cc_are_equal : t -> term -> term -> bool: Are these two terms equal in the congruence closure?

val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.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 -> CC.Expl.t -> unit: Merge these two terms in the congruence closure, given this explanation. See cc_merge

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

val cc_mem_term : t -> term -> bool: Return true if the term is explicitly in the congruence closure. To be used in theories

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

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

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

val on_cc_is_subterm : t -> (CC.N.t -> term -> unit) -> unit: Callback for when a term is a subterm of another term in the congruence closure

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

val on_cc_propagate : t -> (CC.t -> lit -> (unit -> lit list * proof) -> 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 -> proof -> unit) -> term -> (term * proof) option

Given a term, try to preprocess it. Return None if it didn't change, or Some (u,p) if t=u and p is a proof of t=u. Can also add clauses to define new terms.

Preprocessing might transform terms to make them more amenable to reasoning, e.g. by removing boolean formulas via Tseitin encoding, adding clauses that encode their meaning in the same move.

parameter mk_lit: creates a new literal for a boolean term.

parameter add_clause: pushes a new clause into the SAT solver.

val on_preprocess : t -> preprocess_hook -> unit: Add a hook that will be called when terms are preprocessed

Model production

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

A model-production hook. It takes the solver, a class, and returns a term for this class. For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value.

If no hook assigns a value to a class, a fake value is created for it.

val on_model_gen : t -> model_hook -> unit: Add a hook that will be called when a model is being produced

Main type for a solver