package msat

  1. Overview
  2. Docs
type formula
type proof
type slice = {
  1. start : int;
  2. length : int;
  3. get : int -> formula;
  4. push : formula list -> proof -> unit;
}
type level
type res =
  1. | Sat of level
  2. | Unsat of formula list * proof
val dummy : level
val current_level : unit -> level
val assume : slice -> res
val backtrack : level -> unit