Module Abstract

module Abstract: sig .. end
Symbolic abstraction routines.

val affine_hull : 'a Syntax.context ->
'a Syntax.formula -> Syntax.symbol list -> 'a Syntax.term list
affine_hull srk phi symbols computes a basis for the affine hull of phi, projected onto the given set of symbols. The basis is represented as a list of terms, with the interpretation that a point p belongs to the affine hull if every term in the list evaluates to 0 at p.
val boxify : 'a Syntax.context ->
'a Syntax.formula -> 'a Syntax.term list -> 'a Syntax.formula
boxify srk phi terms computes the strongest formula of the form /\ { lo <= t <= hi : t in terms } that is implied by phi.
val abstract : ?exists:(Syntax.symbol -> bool) ->
'a Syntax.context ->
'abs Apron.Manager.t -> 'a Syntax.formula -> ('a, 'abs) SrkApron.property
abstract ?exists srk man phi computes the strongest property that is implied by phi which is expressible within a given abstract domain. The property is restricted to use only the symbols that satisfy the ?exists predicate (which defaults to the constant true predicate).