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 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
type level
val base_level : level
val current_level : unit -> level
val push : unit -> level
val pop : level -> unit
val reset : unit -> unit
OCaml

Innovation. Community. Security.