Log
Logging function, for debugging
Formula_intf
Signature of formulas that parametrises the SAT/SMT Solver Module.
Theory_intf
Type returned by the theory, either the current set of assumptions is satisfiable, or it is not, in which case a tautological clause (hopefully minimal) is returned.
Plugin_intf
The type of evaluation results, either the given formula cannot be evaluated, or it can thanks to assignment.
Expr_intf
Signature of formulas that parametrises the Mcsat Solver Module.
Res_intf
Signature for a module handling proof by resolution from sat solving traces
Solver_types_intf
The signatures of clauses used in the Solver.
Solver_intf
Returns the valuation of a formula in the current state of the sat solver.
Tseitin_intf
Type of atomic formulas
Res
Functor to create a module building proofs from a sat-solver unsat trace.
Internal
Functor to create a solver parametrised by the atomic formulas and a theory.
External
Solver_types
Functor to instantiate the types of clauses for a solver.
Solver
Simple case where the proof type is unit and the theory is empty
Mcsolver
Functor to create a solver parametrised by the atomic formulas and a theory.
Tseitin
Dot
Dedukti
Functor to generate a backend to output proofs for the dedukti type checker.
Backend_intf
Hashcons
Expr_sat
Make a proposition from an integer.
Sat
Type_sat
Typechecking of terms from Dolmen.Term.t This module provides functions to parse terms from the untyped syntax tree defined in Dolmen, and generate formulas as defined in the Expr_sat module.
Expr_smt
Expressions for TabSat
Smt
Type_smt
Typechecking of terms from Dolmen.Term.t This module provides functions to parse terms from the untyped syntax tree defined in Dolmen, and generate formulas as defined in the Expr_smt module.
Unionfind
Eclosure
Equality closure using an union-find structure.
Mcsat
Plugin_mcsat