Module Sidekick_base

Sidekick base

This library is a starting point for writing concrete implementations of SMT solvers with Sidekick.

It provides a representation of terms, boolean formulas, linear arithmetic expressions, datatypes for the functors in Sidekick.

In addition, it has a notion of Statement. Statements are instructions for the SMT solver to do something, such as: define a new constant, declare a new constant, assert a formula as being true, set an option, check satisfiability of the set of statements added so far, etc. Logic formats such as SMT-LIB 2.6 are in fact based on a similar notion of statements, and a .smt2 files contains a list of statements.

module Types_ : sig ... end
module Term : sig ... end
module Const = Sidekick_core.Const
module Ty : sig ... end
module ID : sig ... end

Unique Identifiers

module Form : sig ... end

Formulas (boolean terms).

module Data_ty : sig ... end
module Cstor = Data_ty.Cstor
module Select = Data_ty.Select
module Statement : sig ... end

Statements.

module Solver : sig ... end
module Uconst : sig ... end

Uninterpreted constants

module Config : sig ... end

Configuration

module LRA_term : sig ... end
module Th_data : sig ... end

Theory of datatypes

module Th_bool : sig ... end

Reducing boolean formulas to clauses

module Th_lra : sig ... end

Theory of Linear Rational Arithmetic

module Th_ty_unin : sig ... end
val k_th_bool_config : [ `Dyn | `Static ] Config.Key.t
val th_bool : Config.t -> Solver.theory
val th_bool_dyn : Solver.theory
val th_bool_static : Solver.theory
val th_data : Solver.theory
val th_lra : Solver.theory
val th_ty_unin : Solver.theory
val const_decoders : (string * Sidekick_core.Const.Ops.t * (Sidekick_core_logic__.Types_.term Sidekick_util.Ser_decode.t -> Sidekick_core.Const.view Sidekick_util.Ser_decode.t)) list

All constant decoders