package msat

  1. Overview
  2. Docs
type term
type formula
type proof
type level
val dummy : level
val current_level : unit -> level
val assume : (term, formula, proof) slice -> (formula, proof) res
val if_sat : (term, formula, proof) slice -> (formula, proof) res
val backtrack : level -> unit
val assign : term -> term
val iter_assignable : (term -> unit) -> formula -> unit
val eval : formula -> term eval_res