package msat

  1. Overview
  2. Docs
type !'term eval_res =
  1. | Unknown
  2. | Valued of bool * 'term list
type (!'formula, !'proof) res =
  1. | Sat
  2. | Unsat of 'formula list * 'proof
type (!'term, !'formula) assumption =
  1. | Lit of 'formula
  2. | Assign of 'term * 'term
type (!'term, !'formula, !'proof) reason =
  1. | Eval of 'term list
  2. | Consequence of 'formula list * 'proof
type (!'term, !'formula, !'proof) slice = {
  1. start : int;
  2. length : int;
  3. get : int -> ('term, 'formula) assumption;
  4. push : 'formula list -> 'proof -> unit;
  5. propagate : 'formula -> ('term, 'formula, 'proof) reason -> unit;
}
module type S = sig ... end