package msat

  1. Overview
  2. Docs
exception Unsat
module St : sig ... end
module Proof : sig ... end
val solve : unit -> unit
val assume : ?tag:int -> Fsmt.Formula.t list list -> unit
val eval : Fsmt.Formula.t -> bool
val hyps : unit -> St.clause Vec.t
val history : unit -> St.clause Vec.t
val unsat_conflict : unit -> St.clause option
val model : unit -> (St.term * St.term) list
type level
val base_level : level
val current_level : unit -> level
val push : unit -> level
val pop : level -> unit
val reset : unit -> unit