sig
  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 : SrkApron.scalar -> QQ.t
  val qq_of_coeff : SrkApron.coeff -> QQ.t option
  val coeff_of_qq : QQ.t -> SrkApron.coeff
  module Env :
    sig
      type 'a t
      val pp : Format.formatter -> 'a SrkApron.Env.t -> unit
      val empty : 'a Syntax.context -> 'a SrkApron.Env.t
      val of_set :
        'a Syntax.context -> Syntax.Symbol.Set.t -> 'a SrkApron.Env.t
      val of_enum :
        'a Syntax.context -> Syntax.symbol BatEnum.t -> 'a SrkApron.Env.t
      val of_list :
        'a Syntax.context -> Syntax.symbol list -> 'a SrkApron.Env.t
      val vars : 'a SrkApron.Env.t -> Syntax.symbol BatEnum.t
      val dimensions : 'a SrkApron.Env.t -> int BatEnum.t
      val mem : Syntax.symbol -> 'a SrkApron.Env.t -> bool
      val int_dim : 'a SrkApron.Env.t -> int
      val real_dim : 'a SrkApron.Env.t -> int
      val dimension : 'a SrkApron.Env.t -> int
      val var_of_dim : 'a SrkApron.Env.t -> int -> Syntax.symbol
      val dim_of_var : 'a SrkApron.Env.t -> Syntax.symbol -> int
      val filter :
        (Syntax.symbol -> bool) -> 'a SrkApron.Env.t -> 'a SrkApron.Env.t
    end
  type ('a, 'abs) property
  val pp : Format.formatter -> ('a, 'abs) SrkApron.property -> unit
  val show : ('a, 'abs) SrkApron.property -> string
  val get_manager : ('a, 'abs) SrkApron.property -> 'abs Apron.Manager.t
  val is_bottom : ('a, 'abs) SrkApron.property -> bool
  val is_top : ('a, 'abs) SrkApron.property -> bool
  val top :
    'abs Apron.Manager.t -> 'a SrkApron.Env.t -> ('a, 'abs) SrkApron.property
  val bottom :
    'abs Apron.Manager.t -> 'a SrkApron.Env.t -> ('a, 'abs) SrkApron.property
  val meet_tcons :
    ('a, 'abs) SrkApron.property ->
    SrkApron.tcons list -> ('a, 'abs) SrkApron.property
  val meet_lcons :
    ('a, 'abs) SrkApron.property ->
    SrkApron.lcons list -> ('a, 'abs) SrkApron.property
  val leq :
    ('a, 'abs) SrkApron.property -> ('a, 'abs) SrkApron.property -> bool
  val equal :
    ('a, 'abs) SrkApron.property -> ('a, 'abs) SrkApron.property -> bool
  val join :
    ('a, 'abs) SrkApron.property ->
    ('a, 'abs) SrkApron.property -> ('a, 'abs) SrkApron.property
  val meet :
    ('a, 'abs) SrkApron.property ->
    ('a, 'abs) SrkApron.property -> ('a, 'abs) SrkApron.property
  val widen :
    ('a, 'abs) SrkApron.property ->
    ('a, 'abs) SrkApron.property -> ('a, 'abs) SrkApron.property
  val exists :
    'abs Apron.Manager.t ->
    (Syntax.symbol -> bool) ->
    ('a, 'abs) SrkApron.property -> ('a, 'abs) SrkApron.property
  val add_vars :
    Syntax.symbol BatEnum.t ->
    ('a, 'abs) SrkApron.property -> ('a, 'abs) SrkApron.property
  val boxify : ('a, 'abs) SrkApron.property -> ('a, 'abs) SrkApron.property
  val rename :
    (Syntax.symbol -> Syntax.symbol) ->
    ('a, 'abs) SrkApron.property -> ('a, 'abs) SrkApron.property
  val lexpr_of_vec : 'a SrkApron.Env.t -> Linear.QQVector.t -> SrkApron.lexpr
  val vec_of_lexpr : 'a SrkApron.Env.t -> SrkApron.lexpr -> Linear.QQVector.t
  val texpr_of_term : 'a SrkApron.Env.t -> 'a Syntax.term -> SrkApron.texpr
  val term_of_texpr : 'a SrkApron.Env.t -> SrkApron.texpr -> 'a Syntax.term
  val tcons_geqz : SrkApron.texpr -> SrkApron.tcons
  val tcons_eqz : SrkApron.texpr -> SrkApron.tcons
  val tcons_gtz : SrkApron.texpr -> SrkApron.tcons
  val lcons_geqz : SrkApron.lexpr -> SrkApron.lcons
  val lcons_eqz : SrkApron.lexpr -> SrkApron.lcons
  val lcons_gtz : SrkApron.lexpr -> SrkApron.lcons
  val formula_of_property : ('a, 'abs) SrkApron.property -> 'a Syntax.formula
  val eval_texpr : SrkApron.texpr -> Apron.Interval.t
end