Up  Next

Module Bddapron.Apronexpr

module Apronexpr: sig .. end

Types of numerical variables (distinction is exploited when negating constraints)
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, [> typ ]) typ_of_var = 'a -> ([> typ ] as 'b)

Expressions



Linear expressions


module Lin: sig .. end

Polynomial expressions


module Poly: sig .. end

Tree expressions


module Tree: sig .. end

Conversions


val lin_of_poly : 'a symbol ->
       'a Poly.t -> 'a Lin.t
val lin_of_tree : 'a symbol ->
       'a Tree.t -> 'a Lin.t
val poly_of_tree : 'a symbol ->
       'a Tree.t -> 'a Poly.t
val tree_of_lin : 'a Lin.t -> 'a Tree.t
val tree_of_poly : 'a Poly.t -> 'a Tree.t

General expressions and operations


type 'a t =
| Lin of 'a Lin.t
| Poly of 'a Poly.t
| Tree of 'a Tree.t 
type 'a expr = 'a t 
val var : 'a symbol ->
       ('a, [> typ ]) typ_of_var ->
       'a -> 'a t
val zero : 'a t
val one : 'a t
val cst : Apron.Coeff.t -> 'a t
val add : 'a symbol ->
       ?typ:Apron.Texpr1.typ ->
       ?round:Apron.Texpr1.round ->
       'a t -> 'a t -> 'a t
val sub : 'a symbol ->
       ?typ:Apron.Texpr1.typ ->
       ?round:Apron.Texpr1.round ->
       'a t -> 'a t -> 'a t
val mul : 'a symbol ->
       ?typ:Apron.Texpr1.typ ->
       ?round:Apron.Texpr1.round ->
       'a t -> 'a t -> 'a t
val div : 'a symbol ->
       ?typ:Apron.Texpr1.typ ->
       ?round:Apron.Texpr1.round ->
       'a t -> 'a t -> 'a t
val gmod : 'a symbol ->
       ?typ:Apron.Texpr1.typ ->
       ?round:Apron.Texpr1.round ->
       'a t -> 'a t -> 'a t
val negate : 'a t -> 'a t
val cast : ?typ:Apron.Texpr1.typ ->
       ?round:Apron.Texpr1.round ->
       'a t -> 'a t
val sqrt : ?typ:Apron.Texpr1.typ ->
       ?round:Apron.Texpr1.round ->
       'a t -> 'a t
val support : 'a symbol -> 'a t -> 'a PSette.t
val substitute_by_var : 'a symbol ->
       'a t -> ('a, 'a) PMappe.t -> 'a t
val normalize : 'a symbol ->
       'a t -> 'a t
val equal : 'a symbol ->
       'a t -> 'a t -> bool
val hash : 'a symbol -> 'a t -> int
val compare : 'a symbol ->
       'a t -> 'a t -> int
val normalize_as_constraint : 'a t -> 'a t
val is_dependent_on_integer_only : ('a, [> typ ]) typ_of_var ->
       'a t -> bool
val typ_of_expr : ('a, [> typ ]) typ_of_var ->
       'a t -> [ `Int | `Real ]
val print : 'a symbol ->
       Format.formatter -> 'a t -> unit
val print_typ : Format.formatter -> [> typ ] -> unit
val of_linexpr0 : 'a symbol ->
       Apron.Environment.t -> Apron.Linexpr0.t -> 'a t
val of_linexpr1 : 'a symbol -> Apron.Linexpr1.t -> 'a t
val to_linexpr0 : 'a symbol ->
       Apron.Environment.t -> 'a t -> Apron.Linexpr0.t
val to_linexpr1 : 'a symbol ->
       Apron.Environment.t -> 'a t -> Apron.Linexpr1.t
val of_texpr0 : 'a symbol ->
       Apron.Environment.t -> Apron.Texpr0.t -> 'a t
val of_texpr1 : 'a symbol -> Apron.Texpr1.t -> 'a t
val to_texpr0 : 'a symbol ->
       Apron.Environment.t -> 'a t -> Apron.Texpr0.t
val to_texpr1 : 'a symbol ->
       Apron.Environment.t -> 'a t -> Apron.Texpr1.t
val to_apron0 : 'a symbol ->
       Apron.Environment.t ->
       'a t ->
       [ `Lin of Apron.Linexpr0.t | `Tree of Apron.Texpr0.t ]
val to_apron1 : 'a symbol ->
       Apron.Environment.t ->
       'a t ->
       [ `Lin of Apron.Linexpr1.t | `Tree of Apron.Texpr1.t ]

Constraints


module Condition: sig .. end