module SAT : Sat_solver_sig.Stype sat_env = SAT.tThe SAT working environment.
type env = private {used_context : used_context;consistent_dep_stack : (res * Explanation.t) Stack.t;sat_env : sat_env;mutable res : res;mutable expl : Explanation.t;}val init_env : ?sat_env:sat_env -> used_context -> envProcess 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 processval pop : int processval query : (string * Expr.t * Ty.goal_sort) processval th_assume : Expr.th_elt processval optimize : Objective.Function.t processval process_decl :
?hook_on_status:(sat_env status -> int -> unit) ->
env ->
Commands.sat_tdecl ->
unit