package msat

  1. Overview
  2. Docs

Parameters

module Dummy : sig ... end

Signature

module SmtSolver : sig ... end
module Proof = SmtSolver.Proof
module Dot : sig ... end
type atom = Fsmt.t
type clause = SmtSolver.St.clause
type res =
  1. | Sat
  2. | Unsat
val solve : unit -> res
val assume : Fsmt.Formula.t list list -> unit
val get_proof : unit -> SmtSolver.Proof.proof
val eval : Fsmt.Formula.t -> bool
val print_atom : Format.formatter -> Fsmt.t -> unit
val print_clause : Format.formatter -> SmtSolver.St.clause -> unit
val print_proof : Format.formatter -> SmtSolver.Proof.proof -> unit