package msat

  1. Overview
  2. Docs
module M : sig ... end
module CC : sig ... end
type term = Fsmt.Term.t
type formula = Fsmt.t
type proof = unit
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 = {
  1. cc : CC.t;
  2. assign : (term * int) M.t;
}
type res =
  1. | Sat
  2. | Unsat of formula list * proof
type eval_res =
  1. | Valued of bool * int
  2. | Unknown
val dummy : level
val env : level ref
val current_level : unit -> level
val to_clause : (Fsmt.var * Fsmt.var * Fsmt.var list) -> Fsmt.t list
val assume : slice -> res
val backtrack : level -> unit
val assign : String.t -> String.t
val iter_assignable : (Fsmt.var -> unit) -> Fsmt.formula -> unit
val max : int -> int -> int
val eval : Fsmt.formula -> eval_res
val if_sat : 'a -> unit