Module SrkApron

module SrkApron: sig .. end

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