Module `Solver.Solver_internal`

Internal solver, available to theories.

module T = T

module Lit = Lit

type ty = T.Ty.t
type term = T.Term.t
type term_store = T.Term.store
type ty_store = T.Ty.store
type proof = proof
type dproof = proof -> unit: Delayed proof. This is used to build a proof step on demand.

module P = P

type t: Main type for a solver

type solver = t

val tst : t -> term_store
val ty_st : t -> ty_store
val stats : t -> Sidekick_util.Stat.t
val with_proof : t -> (proof -> unit) -> unit

Actions for the theories

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

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 Lit = Lit and type proof = proof and type P.t = proof and type P.lit = lit and type Actions.t = theory_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 option: Simplify input term, returns Some u if some simplification occurred.

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

Preprocessors

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

module type PREPROCESS_ACTS = sig ... end

type preprocess_actions = (module PREPROCESS_ACTS): Actions available to the preprocessor

type preprocess_hook = t -> preprocess_actions -> term -> term option

Given a term, try to preprocess it. Return None if it didn't change, or Some (u) if 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 preprocess_actions: actions available during preprocessing.

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

val preprocess_acts_of_acts : t -> theory_actions -> preprocess_actions: Obtain preprocessor actions, from theory actions

hooks for the theory

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

val push_decision : t -> theory_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 -> theory_actions -> lit -> reason:(unit -> lit list * dproof) -> unit: Propagate a boolean using a unit clause. expl => lit must be a theory lemma, that is, a T-tautology

val propagate_l : t -> theory_actions -> lit -> lit list -> dproof -> 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 -> theory_actions -> lit list -> dproof -> unit: Add local clause to the SAT solver. This clause will be removed when the solver backtracks.

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

val mk_lit : t -> theory_actions -> ?⁠sign:bool -> term -> lit: Create a literal. This automatically preprocesses the term.

val preprocess_term : t -> preprocess_actions -> term -> term: Preprocess a term. The preprocessing proof is automatically emitted.

val add_lit : t -> theory_actions -> ?⁠default_pol:bool -> lit -> unit

Add the given literal to the SAT solver, so it gets assigned a boolean value.

parameter default_pol: default polarity for the corresponding atom

val add_lit_t : t -> theory_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 -> theory_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 -> theory_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 -> theory_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 -> theory_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 -> theory_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 * dproof) -> unit) -> unit: Callback called on every CC propagation

val on_partial_check : t -> (t -> theory_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 -> theory_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.

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