module Wedge: sig .. end
Wedge abstract domain.
type 'a t
val pp : Format.formatter -> 'a t -> unit
val show : 'a t -> string
val join : ?integrity:('a Syntax.formula -> unit) ->
'a t -> 'a t -> 'a t
val meet : 'a t -> 'a t -> 'a t
val meet_atoms : 'a t -> 'a Syntax.formula list -> unit
val equal : 'a t -> 'a t -> bool
val widen : 'a t -> 'a t -> 'a t
val of_atoms : 'a Syntax.context -> 'a Syntax.formula list -> 'a t
val to_atoms : 'a t -> 'a Syntax.formula list
val to_formula : 'a t -> 'a Syntax.formula
val exists : ?integrity:('a Syntax.formula -> unit) ->
?subterm:(Syntax.symbol -> bool) ->
(Syntax.symbol -> bool) -> 'a t -> 'a t
Project symbols out of a wedge that do not satisfy the given predicate.
Additionally project out terms that contain a symbol that does not satisfy
the subterm predicate.
val top : 'a Syntax.context -> 'a t
val bottom : 'a Syntax.context -> 'a t
val is_bottom : 'a t -> bool
val is_top : 'a t -> bool
val farkas_equalities : 'a t -> ('a Syntax.term * Linear.QQVector.t) list
Compute a representation of the set of equalities that are entailed by a
given wedge as a list (term0, vector0),...,(termn,vectorn). The
interpretation of this representation is that for any vector v,
wedge |= (vector0 . v) term0 + ... + (vectorn . v) termn = 0
where . represents the dot product.
val symbolic_bounds : 'a t -> Syntax.symbol -> 'a Syntax.term list * 'a Syntax.term list
Given a wedge wedge and a symbol symbol, compute a list of lower bounds
and upper bounds for symbol that are implied by wedge.
val bounds : 'a t -> 'a Syntax.term -> Interval.t
Given a wedge wedge and a term term, compute a lower and upper bounds
for term within the region wedge.
val ensure_nonlinear_symbols : 'a Syntax.context -> unit
Ensure that the named symbols pow : Real x Real -> Real and log : Real
x Real -> Real belong to a given context.
val ensure_min_max : 'a Syntax.context -> unit
val abstract : ?exists:(Syntax.symbol -> bool) ->
?subterm:(Syntax.symbol -> bool) ->
'a Syntax.context -> 'a Syntax.formula -> 'a t
Compute a wedge that over-approximates a given formula
val is_sat : 'a Syntax.context -> 'a Syntax.formula -> [ `Sat | `Unknown | `Unsat ]
Check if a formula is satisfiable by computing an over-approximating wedge
and checking whether it is feasible. This procedure improves on the naive
implementation by returning `Unknown as soon as it finds a disjunct that
it can't prove to be infeasible.
val symbolic_bounds_formula : ?exists:(Syntax.symbol -> bool) ->
'a Syntax.context ->
'a Syntax.formula ->
Syntax.symbol ->
[ `Sat of 'a Syntax.term option * 'a Syntax.term option | `Unsat ]
Compute lower and upper bounds for a symbol that are implied by the given
formula (if they exist). The upper and lower bounds may involve only
symbols that satisfy the exist predicate, and may involve the functions
max and min (binary named symbols). (For example, if x is bounded
above by 0 and y, then the upper bound computed by symbolic_bounds
is min(0,y)).
val coordinate_system : 'a t -> 'a CoordinateSystem.t
val polyhedron : 'a t -> ([ `Eq | `Geq ] * Linear.QQVector.t) list
val vanishing_ideal : 'a t -> Polynomial.Mvp.t list
val copy : 'a t -> 'a t
val equational_saturation : ?integrity:('a Syntax.formula -> unit) -> 'a t -> Polynomial.Rewrite.t
val strengthen : ?integrity:('a Syntax.formula -> unit) -> 'a t -> unit