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 |