Module Fun_sat.Make

A functional SAT solver implementation.

Parameters

module _ : Theory.S

Signature

type t
exception Sat of t
exception Unsat of Expr.Labeled.Set.t
exception I_dont_know of t
val empty : ?selector:(Expr.t -> bool) -> unit -> t
val declare : t -> Id.typed -> t
val push : t -> int -> t
val pop : t -> int -> t

pop env n pops n assertion levels of the environment env.

  • raises Errors.Error

    if there is no n assertion levels in env.

val assume : t -> Expr.gformula -> Expr.Labeled.Set.t -> t
val assume_th_elt : t -> Expr.th_elt -> Expr.Labeled.Set.t -> t
val pred_def : t -> Expr.t -> string -> Expr.Labeled.Set.t -> Loc.t -> t
val reset_refs : unit -> unit
val reinit_ctx : unit -> unit
val get_model : t -> Models.t option
val get_unknown_reason : t -> Sat_solver_sig.unknown_reason option
val get_value : t -> Expr.t -> Expr.t option