exception Unsat of Explanation.tempty ~selector () creates an empty environment.
The optional argument selector is used to filter ground facts discovered by the instantiation engine.
declare env id declares a new identifier id.
If the environment env isn't unsatisfiable and the model generation is enabled, the solver produces a model term for id which can be retrieved with get_model.
val push : t -> int -> unitpush env n adds n new assertion levels in env.
Internally, for each new assertion level, a fresh guard g is created and all formulas f assumed at this assertion level is replaced by g ==> f.
The guard g is forced to be true but not propagated at level 0.
val pop : t -> int -> unitpop env n removes n assertion levels in env.
Internally, the guard g introduced in push corresponding to this pop is propagated to false at level 0.
Errors.Error if there is no n assertion levels in env.
val assume : t -> Expr.gformula -> Explanation.t -> unitassume env f dep assumes the ground formula f in env. The dep argument can be used to generate an unsat core.
Unsat if f is unsatisfiable in env.
val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unitassume env f exp assumes a new formula f with the explanation exp in the theory environment of env.
val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> unitpred_def env f assumes a new predicate definition f in env.
val optimize : t -> Objective.Function.t -> unitoptimize env fn registers the objective function fn.
After optimization, the value of this objective is returned by get_objectives.
val unsat : t -> Expr.gformula -> Explanation.tunsat env f checks the unsatisfiability of f in env.
I_dont_know if the solver cannot prove the unsatisfiability of env.
Sat if f is satisfiable in env.
get_model t produces the current first-order model. Notice that this model is a best-effort.
None if the model generation is not enabled or the environment is unsatisfiable.
val get_unknown_reason : t -> Sat_solver_sig.unknown_reason optionget_unknown_reason t returns the reason Alt-Ergo raised I_dont_know if it did. If it did not, returns None.
get_value t e returns the value of e as a constant expression in the current model generated. Returns None if can't decide.
val get_objectives : t -> Objective.Model.t optionget_objectives t returns the current objective values.
None if there is no objective or the environment is unsatisfiable.