Solver_internal (sidekick.Sidekick_smt_solver.Solver

type t

Main type for the SMT solver

type solver = t

val tst : t -> Sigs.term_store

val stats : t -> Sidekick_util.Stat.t

val tracer : t -> Tracer.t

Access the tracer object

val registry : t -> Registry.t

A solver contains a registry so that theories can share data

Actions for the theories

type theory_actions

Handle that the theories can use to perform actions.

Congruence Closure

val cc : t -> Sidekick_cc.CC.t

Congruence closure for this solver

Backtracking

include Sidekick_sigs.BACKTRACKABLE0 with type t := t

val n_levels : t -> int

Number of levels

val push_level : t -> unit

Push a backtracking point

val pop_levels : t -> int -> unit

pop_levels st n removes n levels

Interface to SAT

val to_sat_plugin : t -> (module Sidekick_sat.PLUGIN)

Simplifiers

type simplify_hook = Sidekick_simplify.hook

val simplifier : t -> Sidekick_simplify.t

val add_simplifier : t -> Sidekick_simplify.hook -> unit

Add a simplifier hook for preprocessing.

val simplify_t : t -> Sigs.term -> (Sigs.term * Sigs.step_id) option

Simplify input term, returns Some u if some simplification occurred.

val simp_t : t -> Sigs.term -> Sigs.term * Sigs.step_id option

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 = Preprocess.PREPROCESS_ACTS

type preprocess_actions = (module PREPROCESS_ACTS)

Actions available to the preprocessor

type preprocess_hook =
  Preprocess.t ->
  is_sub:bool ->
  recurse:(Sigs.term -> Sigs.term) ->
  preprocess_actions ->
  Sigs.term ->
  Sigs.term option

Given a term, preprocess it.

The idea is to add literals and clauses to help define the meaning of the term, if needed. For example for boolean formulas, clauses for their Tseitin encoding can be added, with the formula acting as its own proxy symbol.

parameter preprocess_actions
actions available during preprocessing.

val preprocess : t -> Preprocess.t

val on_preprocess : t -> preprocess_hook -> unit

Add a hook that will be called when terms are preprocessed

val preprocess_clause : 
  t ->
  Sigs.lit list ->
  Sigs.step_id ->
  Sigs.lit list * Sigs.step_id

val preprocess_clause_array : 
  t ->
  Sigs.lit array ->
  Sigs.step_id ->
  Sigs.lit array * Sigs.step_id

val simplify_and_preproc_lit : t -> Sigs.lit -> Sigs.lit * Sigs.step_id option

Simplify literal then preprocess it

Finding foreign variables

val find_foreign : t -> Find_foreign.t

val on_find_foreign : t -> Find_foreign.hook -> unit

Add a hook for finding foreign variables

hooks for the theory

val raise_conflict : 
  t ->
  theory_actions ->
  Sigs.lit list ->
  Sidekick_proof.Pterm.delayed ->
  'a

Give a conflict clause to the solver

val push_decision : t -> theory_actions -> Sigs.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 ->
  Sigs.lit ->
  reason:(unit -> Sigs.lit list * Sidekick_proof.Pterm.delayed) ->
  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 ->
  Sigs.lit ->
  Sigs.lit list ->
  Sidekick_proof.Pterm.delayed ->
  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 ->
  Sigs.lit list ->
  Sidekick_proof.Pterm.delayed ->
  unit

Add local clause to the SAT solver. This clause will be removed when the solver backtracks.

val add_clause_permanent : 
  t ->
  theory_actions ->
  Sigs.lit list ->
  Sidekick_proof.Pterm.delayed ->
  unit

Add toplevel clause to the SAT solver. This clause will not be backtracked.

val add_ty : t -> ty:Sigs.term -> unit

Declare a sort for the SMT solver

val mk_lit : t -> ?sign:bool -> Sigs.term -> Sigs.lit

Create a literal. This automatically preprocesses the term.

val add_lit : t -> theory_actions -> ?default_pol:bool -> Sigs.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 -> Sigs.term -> unit

Add the given (signed) bool term to the SAT solver, so it gets assigned a boolean value

val cc_find : t -> Sidekick_cc.E_node.t -> Sidekick_cc.E_node.t

Find representative of the node

val cc_are_equal : t -> Sigs.term -> Sigs.term -> bool

Are these two terms equal in the congruence closure?

val cc_resolve_expl : 
  t ->
  Sidekick_cc.Expl.t ->
  Sigs.lit list * Sidekick_proof.Pterm.delayed

val cc_add_term : t -> Sigs.term -> Sidekick_cc.E_node.t

Add/retrieve congruence closure node for this term. To be used in theories

val cc_mem_term : t -> Sigs.term -> bool

Return true if the term is explicitly in the congruence closure. To be used in theories

val on_cc_pre_merge : 
  t ->
  ((Sidekick_cc.CC.t
    * Sidekick_cc.E_node.t
    * Sidekick_cc.E_node.t
    * Sidekick_cc.Expl.t) ->
    Sidekick_cc.CC.Handler_action.or_conflict) ->
  unit

Callback for when two classes containing data for this key are merged (called before)

val on_cc_post_merge : 
  t ->
  ((Sidekick_cc.CC.t * Sidekick_cc.E_node.t * Sidekick_cc.E_node.t) ->
    Sidekick_cc.CC.Handler_action.t list) ->
  unit

Callback for when two classes containing data for this key are merged (called after)

val on_cc_new_term : 
  t ->
  ((Sidekick_cc.CC.t * Sidekick_cc.E_node.t * Sigs.term) ->
    Sidekick_cc.CC.Handler_action.t list) ->
  unit

Callback to add data on terms when they are added to the congruence closure

val on_cc_is_subterm : 
  t ->
  ((Sidekick_cc.CC.t * Sidekick_cc.E_node.t * Sigs.term) ->
    Sidekick_cc.CC.Handler_action.t list) ->
  unit

Callback for when a term is a subterm of another term in the congruence closure

val on_cc_conflict : t -> (Sidekick_cc.CC.ev_on_conflict -> unit) -> unit

Callback called on every CC conflict

val on_cc_propagate : 
  t ->
  ((Sidekick_cc.CC.t
    * Sigs.lit
    * (unit ->
    Sigs.lit list * Sidekick_proof.Pterm.delayed)) ->
    Sidekick_cc.CC.Handler_action.t list) ->
  unit

Callback called on every CC propagation

val on_new_ty : t -> (Sigs.ty, unit) Sidekick_util.Event.t

Add a callback for when new types are added via add_ty

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

val declare_pb_is_incomplete : t -> unit

Declare that, in some theory, the problem is outside the logic fragment that is decidable (e.g. if we meet proper NIA formulas). The solver will not reply "SAT" from now on.

Model production

type model_ask_hook =
  t ->
  Model_builder.t ->
  Sidekick_core.Term.t ->
  (Sigs.value * Sidekick_core.Term.t list) option

A model-production hook to query values from a theory.

It takes the solver, a class, and returns an optional value for this class (potentially with sub-terms to find values for, if the value is actually a skeleton).

For example, an arithmetic theory might detect that a class contains a numeric constant, and return this constant as a model value. The theory of arrays might return array.const $v for an array Array A B, where $v will be picked by the theory of the sort B.

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

type model_completion_hook = t -> add:(Sigs.term -> Sigs.value -> unit) -> unit

A model production hook, for the theory to add values. The hook is given a add function to add bindings to the model.

val on_model : 
  ?ask:model_ask_hook ->
  ?complete:model_completion_hook ->
  t ->
  unit

Add model production/completion hooks.

val on_progress : t -> (unit, unit) Sidekick_util.Event.t

val is_complete : t -> bool

Are we still in a complete logic fragment?

val last_model : t -> Model.t option

Delayed actions

module type PERFORM_ACTS = sig ... end

module Perform_delayed (A : PERFORM_ACTS) : sig ... end

val add_theory_state : 
  st:'a ->
  push_level:('a -> unit) ->
  pop_levels:('a -> int -> unit) ->
  t ->
  unit

val create : 
  (module Sigs.ARG) ->
  stat:Sidekick_util.Stat.t ->
  tracer:Tracer.t ->
  Sidekick_core.Term.store ->
  unit ->
  t