package msat

  1. Overview
  2. Docs

Parameters

module Dummy : sig ... end

Signature

module St : sig ... end
module Proof : sig ... end
type atom = St.formula
type res =
  1. | Sat
  2. | Unsat
exception UndecidedLit
val assume : ?tag:int -> atom list list -> unit
val solve : unit -> res
val eval : atom -> bool
val eval_level : atom -> bool * int
val get_proof : unit -> Proof.proof
val unsat_core : Proof.proof -> St.clause list
val get_tag : St.clause -> int option
type level
val base_level : level
val current_level : unit -> level
val push : unit -> level
val pop : level -> unit
val reset : unit -> unit
val print_atom : Format.formatter -> atom -> unit
val print_clause : Format.formatter -> St.clause -> unit
val print_proof : Format.formatter -> Proof.proof -> unit
val print_dimacs : Format.formatter -> St.clause list -> unit