Module QE

module QE: sig .. end
Quantifier elimination
Author(s): Christoph Sticksel

val generalize : TransSys.t ->
(UfSymbol.t * (Var.t list * Term.t)) list ->
Model.t -> Var.t list -> Term.t -> Term.t list
generalize f m evaluates the term f with the model m and returns a term g that is implied by the model m and that implies the term f with the post-state variables existentially quantified. The returned term g contains only pre-state variables.

M |= g

g |= exists y f[y]

with y being the vector of post-state variables in f.

val on_exit : unit -> unit
Cleanup before exit