module SrkApron: sig
.. end
Interface to
Apron numerical
abstract domain library
type
dim = int
type
texpr = Apron.Texpr0.t
type
lexpr = Apron.Linexpr0.t
type
tcons = Apron.Tcons0.t
type
lcons = Apron.Lincons0.t
type
scalar = Apron.Scalar.t
type
coeff = Apron.Coeff.t
val qq_of_scalar : scalar -> QQ.t
val qq_of_coeff : coeff -> QQ.t option
val coeff_of_qq : QQ.t -> coeff
module Env: sig
.. end
type ('a, 'abs)
property
val pp : Format.formatter -> ('a, 'abs) property -> unit
val show : ('a, 'abs) property -> string
val get_manager : ('a, 'abs) property -> 'abs Apron.Manager.t
val is_bottom : ('a, 'abs) property -> bool
val is_top : ('a, 'abs) property -> bool
val top : 'abs Apron.Manager.t -> 'a Env.t -> ('a, 'abs) property
val bottom : 'abs Apron.Manager.t -> 'a Env.t -> ('a, 'abs) property
val meet_tcons : ('a, 'abs) property ->
tcons list -> ('a, 'abs) property
val meet_lcons : ('a, 'abs) property ->
lcons list -> ('a, 'abs) property
val leq : ('a, 'abs) property -> ('a, 'abs) property -> bool
val equal : ('a, 'abs) property -> ('a, 'abs) property -> bool
val join : ('a, 'abs) property ->
('a, 'abs) property -> ('a, 'abs) property
val meet : ('a, 'abs) property ->
('a, 'abs) property -> ('a, 'abs) property
val widen : ('a, 'abs) property ->
('a, 'abs) property -> ('a, 'abs) property
val exists : 'abs Apron.Manager.t ->
(Syntax.symbol -> bool) ->
('a, 'abs) property -> ('a, 'abs) property
val add_vars : Syntax.symbol BatEnum.t ->
('a, 'abs) property -> ('a, 'abs) property
val boxify : ('a, 'abs) property -> ('a, 'abs) property
val rename : (Syntax.symbol -> Syntax.symbol) ->
('a, 'abs) property -> ('a, 'abs) property
val lexpr_of_vec : 'a Env.t -> Linear.QQVector.t -> lexpr
val vec_of_lexpr : 'a Env.t -> lexpr -> Linear.QQVector.t
val texpr_of_term : 'a Env.t -> 'a Syntax.term -> texpr
val term_of_texpr : 'a Env.t -> texpr -> 'a Syntax.term
val tcons_geqz : texpr -> tcons
val tcons_eqz : texpr -> tcons
val tcons_gtz : texpr -> tcons
val lcons_geqz : lexpr -> lcons
val lcons_eqz : lexpr -> lcons
val lcons_gtz : lexpr -> lcons
val formula_of_property : ('a, 'abs) property -> 'a Syntax.formula
val eval_texpr : texpr -> Apron.Interval.t
Evaluate an expression in the environment Top.