package msat

  1. Overview
  2. Docs

Parameters

module Th : sig ... end
module Dummy : sig ... end

Signature

exception Unsat
exception UndecidedLit
val solve : unit -> unit
val assume : ?tag:int -> St.formula list list -> unit
val new_lit : St.term -> unit
val new_atom : St.formula -> unit
val push : unit -> unit
val pop : unit -> unit
val local : St.formula list -> unit
val eval : St.formula -> bool
val eval_level : St.formula -> bool * int
val model : unit -> (St.term * St.term) list
val check : unit -> bool
module Proof : sig ... end
val unsat_conflict : unit -> St.clause option
val full_slice : unit -> (St.term, St.formula, St.proof) Plugin_intf.slice
val trail : unit -> St.t Vec.t
val hyps : unit -> St.clause Vec.t
val temp : unit -> St.clause Vec.t
val history : unit -> St.clause Vec.t