package msat

  1. Overview
  2. Docs

Parameters

module E : Expr_intf.S
module Th : sig ... end
module Dummy : sig ... end

Signature

exception Unsat
module St : sig ... end
module Proof : sig ... end
val solve : unit -> unit
val assume : ?tag:int -> E.Formula.t list list -> unit
val eval : E.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