Module type Frontend.S

type sat_env

The SAT working environment.

type res = [
  1. | `Sat
  2. | `Unknown
  3. | `Unsat
]
type env = private {
  1. used_context : used_context;
  2. consistent_dep_stack : (res * Explanation.t) Stdlib.Stack.t;
  3. sat_env : sat_env;
  4. mutable res : res;
  5. mutable expl : Explanation.t;
}
val init_env : ?selector_inst:(Expr.t -> bool) -> used_context -> env
type 'a process = ?loc:Loc.t -> 'a -> env -> unit

Process are wrappers of calls to the SAT solver. They catch the Sat, Unsat and I_dont_know exceptions to update the frontend environment, but not the Timeout exception which is raised to the user.

val push : int process
val pop : int process
val assume : (string * Expr.t * bool) process
val pred_def : (string * Expr.t) process
val query : (string * Expr.t * Ty.goal_sort) process
val th_assume : Expr.th_elt process
val process_decl : ?hook_on_status:(status -> int -> unit) -> env -> Commands.sat_tdecl -> unit
val print_model : sat_env Fmt.t