Module Satml_frontend_hybrid.Make

Parameters

module _ : Theory.S

Signature

type t
exception Bottom of Explanation.t * AltErgoLib.Expr.Set.t list * t
val empty : unit -> t
val is_true : t -> Expr.t -> (Explanation.t Stdlib.Lazy.t * int) option
val assume : bool -> t -> (Expr.gformula * Explanation.t) list -> t
val decide : t -> Expr.t -> int -> t
val forget_decision : t -> Expr.t -> int -> t
val reset_decisions : t -> t
val get_decisions : t -> (int * Expr.t) list