package msat

  1. Overview
  2. Docs

Parameters

module F : Formula_intf.S

Signature

type formula = F.t
type proof = F.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
OCaml

Innovation. Community. Security.