msat
Library containing a SAT solver that can be parametrized by a theory
1024" x-on:close-sidebar="sidebar=window.innerWidth > 1024 && true">
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Library msat
module Solver_intf : sig ... end
Interface for Solvers
module type S = Solver_intf.S
module type FORMULA = Solver_intf.FORMULA
module type EXPR = Solver_intf.EXPR
module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T
module type PLUGIN_MCSAT = Solver_intf.PLUGIN_MCSAT
module type PROOF = Solver_intf.PROOF
type void = ( unit, bool ) Solver_intf.gadt_eq
Empty type
type ('term, 'form, 'value) sat_state =
( 'term, 'form, 'value ) Solver_intf.sat_state =
{
eval : 'form -> bool; |
eval_level : 'form -> bool * int; |
iter_trail : ( 'form -> unit ) -> ( 'term -> unit ) -> unit; |
model : unit -> ('term * 'value) list; |
}
type ('atom, 'clause, 'proof) unsat_state =
( 'atom, 'clause, 'proof ) Solver_intf.unsat_state =
{
unsat_conflict : unit -> 'clause; |
get_proof : unit -> 'proof; |
unsat_assumptions : unit -> 'atom list; |
}
type 'clause export = 'clause Solver_intf.export = {
hyps : 'clause Msat__Vec.t; |
history : 'clause Msat__Vec.t; |
}
type ('term, 'formula, 'value) assumption =
( 'term, 'formula, 'value ) Solver_intf.assumption =
| Lit of 'formula | (* The given formula is asserted true by the solver *) |
| Assign of 'term * 'value | (* The term is assigned to the value *) |
type ('term, 'formula, 'proof) reason =
( 'term, 'formula, 'proof ) Solver_intf.reason =
| Eval of 'term list |
| Consequence of unit -> 'formula list * 'proof |
type ('term, 'formula, 'value, 'proof) acts =
( 'term, 'formula, 'value, 'proof ) Solver_intf.acts =
{
acts_iter_assumptions : ( ( 'term, 'formula, 'value ) assumption -> unit ) ->
unit; |
acts_eval_lit : 'formula -> lbool; |
acts_mk_lit : 'formula -> unit; |
acts_mk_term : 'term -> unit; |
acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit; |
acts_raise_conflict : 'b. 'formula list -> 'proof -> 'b; |
acts_propagate : 'formula -> ( 'term, 'formula, 'proof ) reason -> unit; |
}
val pp_negated : Format.formatter -> negated -> unit
Print negated
values
val pp_lbool : Format.formatter -> lbool -> unit
Print lbool
values
module Make_mcsat (Th : Solver_intf.PLUGIN_MCSAT) : sig ... end
module Make_cdcl_t (Th : Solver_intf.PLUGIN_CDCL_T) : sig ... end
module Make_pure_sat (Th : Solver_intf.PLUGIN_SAT) : sig ... end