package msat

  1. Overview
  2. Docs
type (!'formula, !'proof) res = ('formula, 'proof) Plugin_intf.res =
  1. | Sat
  2. | Unsat of 'formula list * 'proof
type (!'form, !'proof) slice = {
  1. start : int;
  2. length : int;
  3. get : int -> 'form;
  4. push : 'form list -> 'proof -> unit;
  5. propagate : 'form -> 'form list -> 'proof -> unit;
}
module type S = sig ... end