package msat

  1. Overview
  2. Docs
Library containing a SAT solver that can be parametrized by a theory

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (16)

Authors

  1. S
    Simon Cruanes
  2. G
    Guillaume Bury

Maintainers

  1. G
    guillaume.bury@gmail.com
  2. S
    simon.cruanes.2007@m4x.org

Sources

v0.9.1.tar.gz
md5=ba623630b0b8e0edc016079dd214c80b
sha512=51c133cefe8550125e7b1db18549e893bac15663fdd7a9fac87235c07de755f39eab9fc3cfdf6571612fd79b3d5b22f49f459581b480c7349bacddf2618c8a99

doc/msat/Msat/index.html

Module Msat

Main API

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 lbool = Solver_intf.lbool =
  1. | L_true
  2. | L_false
  3. | L_undefined
type ('term, 'form, 'value) sat_state = ('term, 'form, 'value) Solver_intf.sat_state = {
  1. eval : 'form -> bool;
  2. eval_level : 'form -> bool * int;
  3. iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
  4. model : unit -> ('term * 'value) list;
}
type ('atom, 'clause, 'proof) unsat_state = ('atom, 'clause, 'proof) Solver_intf.unsat_state = {
  1. unsat_conflict : unit -> 'clause;
  2. get_proof : unit -> 'proof;
  3. unsat_assumptions : unit -> 'atom list;
}
type 'clause export = 'clause Solver_intf.export = {
  1. hyps : 'clause Vec.t;
  2. history : 'clause Vec.t;
}
type ('term, 'formula, 'value) assumption = ('term, 'formula, 'value) Solver_intf.assumption =
  1. | Lit of 'formula
    (*

    The given formula is asserted true by the solver

    *)
  2. | Assign of 'term * 'value
    (*

    The term is assigned to the value

    *)
type ('term, 'formula, 'proof) reason = ('term, 'formula, 'proof) Solver_intf.reason =
  1. | Eval of 'term list
  2. | Consequence of unit -> 'formula list * 'proof
type ('term, 'formula, 'value, 'proof) acts = ('term, 'formula, 'value, 'proof) Solver_intf.acts = {
  1. acts_iter_assumptions : (('term, 'formula, 'value) assumption -> unit) -> unit;
  2. acts_eval_lit : 'formula -> lbool;
  3. acts_mk_lit : ?default_pol:bool -> 'formula -> unit;
  4. acts_mk_term : 'term -> unit;
  5. acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit;
  6. acts_raise_conflict : 'b. 'formula list -> 'proof -> 'b;
  7. acts_propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit;
  8. acts_add_decision_lit : 'formula -> bool -> unit;
}
type negated = Solver_intf.negated =
  1. | Negated
  2. | Same_sign
val pp_negated : Format.formatter -> negated -> unit

Print negated values

val pp_lbool : Format.formatter -> lbool -> unit

Print lbool values

exception No_proof
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