package msat

  1. Overview
  2. Docs
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. | 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 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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct