Module Apronexpr

module Apronexpr: sig .. end

Purely arithmetic expressions (internal)

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

module Lin: sig .. end

module Poly: sig .. end

module Tree: sig .. end

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

type 'a 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 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_apron : 'a symbol ->
       Apron.Environment.t ->
       'a t ->
       [ `Linexpr1 of Apron.Linexpr1.t | `Texpr1 of Apron.Texpr1.t ]

module Condition: sig .. end