sig
type 'a symbol =
'a Bdd.Env.symbol = {
compare : 'a -> 'a -> int;
marshal : 'a -> string;
unmarshal : string -> 'a;
mutable print : Format.formatter -> 'a -> unit;
}
type typ = [ `Int | `Real ]
type ('a, 'b) typ_of_var = 'a -> 'b
constraint 'b = [> Bddapron.Apronexpr.typ ]
module Lin :
sig
type 'a term = Mpqf.t * 'a
type 'a t = {
cst : Mpqf.t;
lterm : 'a Bddapron.Apronexpr.Lin.term list;
}
val normalize :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Lin.t -> 'a Bddapron.Apronexpr.Lin.t
val compare_lterm :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Lin.term list ->
'a Bddapron.Apronexpr.Lin.term list -> int
val compare :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Lin.t -> 'a Bddapron.Apronexpr.Lin.t -> int
val var : 'a -> 'a Bddapron.Apronexpr.Lin.t
val zero : 'a Bddapron.Apronexpr.Lin.t
val one : 'a Bddapron.Apronexpr.Lin.t
val cst : Mpqf.t -> 'a Bddapron.Apronexpr.Lin.t
val add :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Lin.t ->
'a Bddapron.Apronexpr.Lin.t -> 'a Bddapron.Apronexpr.Lin.t
val sub :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Lin.t ->
'a Bddapron.Apronexpr.Lin.t -> 'a Bddapron.Apronexpr.Lin.t
val scale :
Mpqf.t -> 'a Bddapron.Apronexpr.Lin.t -> 'a Bddapron.Apronexpr.Lin.t
val negate : 'a Bddapron.Apronexpr.Lin.t -> 'a Bddapron.Apronexpr.Lin.t
val support :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Lin.t -> 'a PSette.t
val substitute_by_var :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Lin.t ->
('a, 'a) PMappe.t -> 'a Bddapron.Apronexpr.Lin.t
val normalize_as_constraint :
'a Bddapron.Apronexpr.Lin.t -> 'a Bddapron.Apronexpr.Lin.t
val print :
'a Bddapron.Apronexpr.symbol ->
Format.formatter -> 'a Bddapron.Apronexpr.Lin.t -> unit
val of_linexpr0 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t ->
Apron.Linexpr0.t -> 'a Bddapron.Apronexpr.Lin.t
val of_linexpr1 :
'a Bddapron.Apronexpr.symbol ->
Apron.Linexpr1.t -> 'a Bddapron.Apronexpr.Lin.t
val to_linexpr0 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t ->
'a Bddapron.Apronexpr.Lin.t -> Apron.Linexpr0.t
val to_linexpr1 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t ->
'a Bddapron.Apronexpr.Lin.t -> Apron.Linexpr1.t
end
module Poly :
sig
type 'a varexp = 'a * int
type 'a monomial = 'a Bddapron.Apronexpr.Poly.varexp list
type 'a term = Mpqf.t * 'a Bddapron.Apronexpr.Poly.monomial
type 'a t = 'a Bddapron.Apronexpr.Poly.term list
val compare_varexp :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.varexp ->
'a Bddapron.Apronexpr.Poly.varexp -> int
val compare_monomial :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.monomial ->
'a Bddapron.Apronexpr.Poly.monomial -> int
val normalize_monomial :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.monomial ->
'a Bddapron.Apronexpr.Poly.monomial
val normalize :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Poly.t
val normalize_full :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Poly.t
val compare :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Poly.t -> int
val cst : Mpqf.t -> 'a Bddapron.Apronexpr.Poly.t
val var : 'a -> 'a Bddapron.Apronexpr.Poly.t
val add :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.t ->
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Poly.t
val sub :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.t ->
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Poly.t
val scale :
'a Bddapron.Apronexpr.symbol ->
Mpqf.t * 'a Bddapron.Apronexpr.Poly.monomial ->
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Poly.t
val mul :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.t ->
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Poly.t
val div :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.t ->
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Poly.t
val negate :
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Poly.t
val support :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.t -> 'a PSette.t
val substitute_by_var :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.t ->
('a, 'a) PMappe.t -> 'a Bddapron.Apronexpr.Poly.t
val normalize_as_constraint :
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Poly.t
val print :
'a Bddapron.Apronexpr.symbol ->
Format.formatter -> 'a Bddapron.Apronexpr.Poly.t -> unit
end
module Tree :
sig
type unop = Apron.Texpr1.unop = Neg | Cast | Sqrt
type binop = Apron.Texpr1.binop = Add | Sub | Mul | Div | Mod | Pow
type typ =
Apron.Texpr1.typ =
Real
| Int
| Single
| Double
| Extended
| Quad
type round = Apron.Texpr1.round = Near | Zero | Up | Down | Rnd
type 'a t =
Cst of Apron.Coeff.t
| Var of 'a
| Unop of Bddapron.Apronexpr.Tree.unop *
'a Bddapron.Apronexpr.Tree.t * Bddapron.Apronexpr.Tree.typ *
Bddapron.Apronexpr.Tree.round
| Binop of Bddapron.Apronexpr.Tree.binop *
'a Bddapron.Apronexpr.Tree.t * 'a Bddapron.Apronexpr.Tree.t *
Bddapron.Apronexpr.Tree.typ * Bddapron.Apronexpr.Tree.round
val support :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Tree.t -> 'a PSette.t
val substitute_by_var :
'a Bddapron.Apronexpr.Tree.t ->
('a, 'a) PMappe.t -> 'a Bddapron.Apronexpr.Tree.t
val print :
'a Bddapron.Apronexpr.symbol ->
Format.formatter -> 'a Bddapron.Apronexpr.Tree.t -> unit
val compare :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Tree.t -> 'a Bddapron.Apronexpr.Tree.t -> int
val of_expr :
'a Bddapron.Apronexpr.symbol ->
Apron.Texpr1.expr -> 'a Bddapron.Apronexpr.Tree.t
val to_expr :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Tree.t -> Apron.Texpr1.expr
end
val lin_of_poly :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Lin.t
val lin_of_tree :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Tree.t -> 'a Bddapron.Apronexpr.Lin.t
val poly_of_tree :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Tree.t -> 'a Bddapron.Apronexpr.Poly.t
val tree_of_lin :
'a Bddapron.Apronexpr.Lin.t -> 'a Bddapron.Apronexpr.Tree.t
val tree_of_poly :
'a Bddapron.Apronexpr.Poly.t -> 'a Bddapron.Apronexpr.Tree.t
type 'a t =
Lin of 'a Bddapron.Apronexpr.Lin.t
| Poly of 'a Bddapron.Apronexpr.Poly.t
| Tree of 'a Bddapron.Apronexpr.Tree.t
type 'a expr = 'a Bddapron.Apronexpr.t
val var :
'a Bddapron.Apronexpr.symbol ->
('a, [> Bddapron.Apronexpr.typ ]) Bddapron.Apronexpr.typ_of_var ->
'a -> 'a Bddapron.Apronexpr.t
val zero : 'a Bddapron.Apronexpr.t
val one : 'a Bddapron.Apronexpr.t
val cst : Apron.Coeff.t -> 'a Bddapron.Apronexpr.t
val add :
'a Bddapron.Apronexpr.symbol ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Apronexpr.t ->
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t
val sub :
'a Bddapron.Apronexpr.symbol ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Apronexpr.t ->
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t
val mul :
'a Bddapron.Apronexpr.symbol ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Apronexpr.t ->
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t
val div :
'a Bddapron.Apronexpr.symbol ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Apronexpr.t ->
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t
val gmod :
'a Bddapron.Apronexpr.symbol ->
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Apronexpr.t ->
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t
val negate : 'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t
val cast :
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t
val sqrt :
?typ:Apron.Texpr1.typ ->
?round:Apron.Texpr1.round ->
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t
val support :
'a Bddapron.Apronexpr.symbol -> 'a Bddapron.Apronexpr.t -> 'a PSette.t
val substitute_by_var :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.t -> ('a, 'a) PMappe.t -> 'a Bddapron.Apronexpr.t
val normalize :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t
val equal :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t -> bool
val hash : 'a Bddapron.Apronexpr.symbol -> 'a Bddapron.Apronexpr.t -> int
val compare :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t -> int
val normalize_as_constraint :
'a Bddapron.Apronexpr.t -> 'a Bddapron.Apronexpr.t
val is_dependent_on_integer_only :
('a, [> Bddapron.Apronexpr.typ ]) Bddapron.Apronexpr.typ_of_var ->
'a Bddapron.Apronexpr.t -> bool
val typ_of_expr :
('a, [> Bddapron.Apronexpr.typ ]) Bddapron.Apronexpr.typ_of_var ->
'a Bddapron.Apronexpr.t -> [ `Int | `Real ]
val print :
'a Bddapron.Apronexpr.symbol ->
Format.formatter -> 'a Bddapron.Apronexpr.t -> unit
val print_typ : Format.formatter -> [> Bddapron.Apronexpr.typ ] -> unit
val of_linexpr0 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t -> Apron.Linexpr0.t -> 'a Bddapron.Apronexpr.t
val of_linexpr1 :
'a Bddapron.Apronexpr.symbol ->
Apron.Linexpr1.t -> 'a Bddapron.Apronexpr.t
val to_linexpr0 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t -> 'a Bddapron.Apronexpr.t -> Apron.Linexpr0.t
val to_linexpr1 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t -> 'a Bddapron.Apronexpr.t -> Apron.Linexpr1.t
val of_texpr0 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t -> Apron.Texpr0.t -> 'a Bddapron.Apronexpr.t
val of_texpr1 :
'a Bddapron.Apronexpr.symbol -> Apron.Texpr1.t -> 'a Bddapron.Apronexpr.t
val to_texpr0 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t -> 'a Bddapron.Apronexpr.t -> Apron.Texpr0.t
val to_texpr1 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t -> 'a Bddapron.Apronexpr.t -> Apron.Texpr1.t
val to_apron0 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t ->
'a Bddapron.Apronexpr.t ->
[ `Lin of Apron.Linexpr0.t | `Tree of Apron.Texpr0.t ]
val to_apron1 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t ->
'a Bddapron.Apronexpr.t ->
[ `Lin of Apron.Linexpr1.t | `Tree of Apron.Texpr1.t ]
module Condition :
sig
type typ =
Apron.Tcons1.typ =
EQ
| SUPEQ
| SUP
| DISEQ
| EQMOD of Apron.Scalar.t
type 'a t =
Bddapron.Apronexpr.Condition.typ * 'a Bddapron.Apronexpr.expr
val make :
('a, [> Bddapron.Apronexpr.Condition.typ ])
Bddapron.Apronexpr.typ_of_var ->
Bddapron.Apronexpr.Condition.typ ->
'a Bddapron.Apronexpr.expr ->
[ `Bool of bool | `Cond of 'a Bddapron.Apronexpr.Condition.t ]
val negate :
('a, [> Bddapron.Apronexpr.Condition.typ ])
Bddapron.Apronexpr.typ_of_var ->
'a Bddapron.Apronexpr.Condition.t ->
'a Bddapron.Apronexpr.Condition.t
val support :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Condition.t -> 'a PSette.t
val print :
'a Bddapron.Apronexpr.symbol ->
Format.formatter -> 'a Bddapron.Apronexpr.Condition.t -> unit
val compare :
'a Bddapron.Apronexpr.symbol ->
'a Bddapron.Apronexpr.Condition.t ->
'a Bddapron.Apronexpr.Condition.t -> int
val of_lincons0 :
'a Bddapron.Apronexpr.symbol ->
('a, [> Bddapron.Apronexpr.Condition.typ ])
Bddapron.Apronexpr.typ_of_var ->
Apron.Environment.t ->
Apron.Lincons0.t ->
[ `Bool of bool | `Cond of 'a Bddapron.Apronexpr.Condition.t ]
val of_lincons1 :
'a Bddapron.Apronexpr.symbol ->
('a, [> Bddapron.Apronexpr.Condition.typ ])
Bddapron.Apronexpr.typ_of_var ->
Apron.Lincons1.t ->
[ `Bool of bool | `Cond of 'a Bddapron.Apronexpr.Condition.t ]
val of_tcons0 :
'a Bddapron.Apronexpr.symbol ->
('a, [> Bddapron.Apronexpr.Condition.typ ])
Bddapron.Apronexpr.typ_of_var ->
Apron.Environment.t ->
Apron.Tcons0.t ->
[ `Bool of bool | `Cond of 'a Bddapron.Apronexpr.Condition.t ]
val of_tcons1 :
'a Bddapron.Apronexpr.symbol ->
('a, [> Bddapron.Apronexpr.Condition.typ ])
Bddapron.Apronexpr.typ_of_var ->
Apron.Tcons1.t ->
[ `Bool of bool | `Cond of 'a Bddapron.Apronexpr.Condition.t ]
val to_tcons0 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t ->
'a Bddapron.Apronexpr.Condition.t -> Apron.Tcons0.t
val to_tcons1 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t ->
'a Bddapron.Apronexpr.Condition.t -> Apron.Tcons1.t
val to_apron0 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t ->
'a Bddapron.Apronexpr.Condition.t ->
[ `Lin of Apron.Lincons0.t | `Tree of Apron.Tcons0.t ]
val to_apron1 :
'a Bddapron.Apronexpr.symbol ->
Apron.Environment.t ->
'a Bddapron.Apronexpr.Condition.t ->
[ `Lin of Apron.Lincons1.t | `Tree of Apron.Tcons1.t ]
end
end