package msat

  1. Overview
  2. Docs

Parameters

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

Signature

exception Unsat
exception UndecidedLit
module Proof : sig ... end
val solve : unit -> unit
val assume : ?tag:int -> St.formula list list -> 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 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
OCaml

Innovation. Community. Security.