Module `QE`

Quantifier elimination

author: Christoph Sticksel, Adrien Champion, Alain Mebsout,

Daniel Larraz

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