package msat

  1. Overview
  2. Docs
module St : sig ... end
exception Insuficient_hyps
type atom = St.atom
type clause = St.clause
type lemma = St.proof
type proof
and proof_node = {
  1. conclusion : clause;
  2. step : step;
}
and step =
  1. | Hypothesis
  2. | Lemma of lemma
  3. | Resolution of proof * proof * atom
val to_list : clause -> atom list
val merge : atom list -> atom list -> atom list
val resolve : atom list -> atom list * atom list
val prove : clause -> proof
val prove_unsat : clause -> proof
val expand : proof -> proof_node
val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> 'a
val unsat_core : proof -> clause list
val check : proof -> unit
val print_clause : Format.formatter -> clause -> unit
OCaml

Innovation. Community. Security.