package msat

  1. Overview
  2. Docs
module St : sig ... end
exception Insuficient_hyps
type atom = St.atom
type lemma = St.proof
type clause = St.clause
type proof
and proof_node = {
  1. conclusion : clause;
  2. step : step;
}
and step =
  1. | Hypothesis
  2. | Assumption
  3. | Lemma of lemma
  4. | Duplicate of proof * atom list
  5. | 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 prove_atom : atom -> proof option
val parents : step -> proof list
val is_leaf : step -> bool
val expl : step -> string
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
module H : sig ... end