Module Fun_sat.Make

Parameters

module Th : Theory.S

Signature

type t
exception Sat of t
exception Unsat of Explanation.t
exception I_dont_know of t
val empty : unit -> t
val empty_with_inst : ( Expr.t -> bool ) -> t
val assume : t -> Expr.gformula -> Explanation.t -> t
val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> t
val unsat : t -> Expr.gformula -> Explanation.t
val print_model : header:bool -> Stdlib.Format.formatter -> t -> unit
val reset_refs : unit -> unit
val get_steps : unit -> int64