Module Abstract

module Abstract: sig .. end

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