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
and proof_node = Mcsolver.Make(Log)(Fsmt)(Tsmt).Proof.proof_node = {
  1. conclusion : clause;
  2. step : step;
}
and step = Mcsolver.Make(Log)(Fsmt)(Tsmt).Proof.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 has_been_proved : clause -> bool
val is_proven : clause -> bool
val prove : clause -> unit
val learn : clause Vec.t -> unit
val assert_can_prove_unsat : clause -> unit
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 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