package msat

  1. Overview
  2. Docs
type (!'term, !'form) sat_state = {
  1. eval : 'form -> bool;
  2. eval_level : 'form -> bool * int;
  3. iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
  4. model : unit -> ('term * 'term) list;
}
type (!'clause, !'proof) unsat_state = {
  1. unsat_conflict : unit -> 'clause;
  2. get_proof : unit -> 'proof;
}
module type S = sig ... end