package msat

  1. Overview
  2. Docs
module Proof : sig ... end
type atom = St.formula
type res =
  1. | Sat of (St.term, St.formula) sat_state
  2. | Unsat of (St.clause, Proof.proof) unsat_state
exception UndecidedLit
val assume : ?tag:int -> atom list list -> unit
val solve : ?assumptions:atom list -> unit -> res
val new_lit : St.term -> unit
val new_atom : atom -> unit
val unsat_core : Proof.proof -> St.clause list
val true_at_level0 : atom -> bool
val get_tag : St.clause -> int option
val export_dimacs : Format.formatter -> unit -> unit
val export_icnf : Format.formatter -> unit -> unit