package msat

  1. Overview
  2. Docs
type term = E.Term.t
type formula = E.Formula.t
type proof = E.proof
type assumption =
  1. | Lit of formula
  2. | Assign of term * term
type slice = {
  1. start : int;
  2. length : int;
  3. get : int -> assumption * int;
  4. push : formula list -> proof -> unit;
  5. propagate : formula -> int -> unit;
}
type level
type res =
  1. | Sat
  2. | Unsat of formula list * proof
type eval_res =
  1. | Valued of bool * int
  2. | Unknown
val dummy : level
val current_level : unit -> level
val assume : slice -> res
val backtrack : level -> unit
val assign : term -> term
val iter_assignable : (term -> unit) -> formula -> unit
val eval : formula -> eval_res
val if_sat : slice -> unit