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).