Index of values

Decompose an abstract value

Unsafe conversion from and to Mpfr.t.

Unsafe conversion from and to Mpq.t.

Return resp.

Modify abstract element to have n disjunct at most.

Get the linear constraints of the n-th disjunct.

Get the tree constraints of the n-th disjunct.

Returns true if abs1 is geometrically contained in abs2

Returns true if abs is a powerset of polyhedra

Get the number of disjuncts of a polyhedra powerset.

Splits abstract element on linear constraint

Adding to an environment a set of integer and real variables.

Perturbation.

Perturbation.

Add the array of generators to the abstract value (time elapse operator).

Add the array of generators to the abstract value (time elapse operator).

approximate man abs alg perform some transformation on the abstract value, guided by the argument alg.

approximate man abs alg perform some transformation on the abstract value, guided by the argument alg.

Change the environment of the array of constraints for a super-environment.

Change the environment of the array of generators for a super-environment.

Change the environment of the array of constraints for a super-environment.

Side-effect version of the previous function

Side-effect version of the previous function

Side-effect version of the previous function

Get the element of the given index (which is not a copy)

Get the element of the given index (which is not a copy)

Get the element of the given index (which is not a copy)

Get the environment of the array

Get the environment of the array

Get the size of the array

Get the size of the array

Get the size of the array

Make an array of tree expression constraints with the given size and defined on the given environment.

Make an array of generators with the given size and defined on the given environment.

Make an array of linear constraints with the given size and defined on the given environment.

Print an array of constraints

Print an array of generators

Print an array of constraints

Set the element of the given index (without any copy).

Set the element of the given index (without any copy).

Set the element of the given index (without any copy).

Parallel assignement of an array of dimensions by an array of same size of linear expressions

Parallel assignement of an array of dimensions by an array of same size of linear expressions

Parallel assignement of an array of dimensions by an array of same size of tree expressions

Parallel assignement of an array of dimensions by an array of same size of tree expressions

Create a bottom (empty) value defined on the given environment

Create a bottom (empty) value with the given number of integer and real variables

Top and bottom intervals (using DOUBLE coefficients)

Return the interval of variation of the dimension in the abstract value.

Return the interval of variation of the linear expression in the abstract value.

Return the interval of variation of the linear expression in the abstract value.

Return the interval of variation of the tree expression in the abstract value.

Return the interval of variation of the tree expression in the abstract value.

Return the interval of variation of the variable in the abstract value.

Put the abstract value in canonical form.

Put the abstract value in canonical form.

The first parameter holds the quotient.

The first parameter holds the quotient.

The first parameter holds the quotient.

The two first parameters hold resp.

The two first parameters hold resp.

The first parameter holds the remainder.

The first parameter holds the remainder.

The first parameter holds the remainder.

Assuming a transformation for add_dimensions, invert it in-place to obtain the inverse transformation using remove_dimensions

Change the environment of the abstract values.

Closure: transform strict constraints into non-strict ones.

Closure: transform strict constraints into non-strict ones.

Side-effect version

Side-effect version

Compare two environment.

Comparison with lexicographic ordering using Coeff.cmp, terminating by constant.

Non Total Comparison: If the 2 coefficients are both scalars, corresp. to Scalar.cmp, If the 2 coefficients are both intervals, corresp. to Interval.cmp, otherwise, -3 if the first is a scalar, 3 otherwise

Non Total Comparison: 0: equality -1: i1 included in i2 +1: i2 included in i1 -2: i1.inf less than or equal to i2.inf +2: i1.inf greater than i2.inf

Compare two coefficients, possibly converting to Mpqf.t.

Compare a coefficient with an integer

Comparison function.

Compose an abstract value

Copy a value

Copy (deep copy)

Copy

Copy (deep copy)

Copy (deep copy)

Copy

Copy a value

Copy a tree expression constraint (deep copy)

Copy

Copy a generator (deep copy)

Copy a linear constraint (deep copy)

Copy

Decompose an abstract value

Return the dimension associated to the given variable in the environment.

dimchange e1 e2 computes the transformation for converting from an environment e1 to a superenvironment e2.

dimchange2 e1 e2 computes the transformation for converting from an environment e1 to a (compatible) environment e2, by first adding (some) variables of e2 and then removing (some) variables of e1.

Return the dimension of the environment

Test the equality of two environments

Equality test

Equality comparison

Equality test

Equality test

Equality test, possibly using a conversion to Mpqf.t.

Is the coefficient equal to scalar b or interval b,b ?

Is the interval equal to i,i ?

Equality test with an integer

Expansion: expand a var tvar expands the variable var into itself and the additional variables in tvar, which are given the same type as var.

Expansion: expand a dim n expands the dimension dim into itself + n additional dimensions.

Change the environment of the constraint for a super-environment.

Change the environment of the expression for a super-environment.

Change the environment of the generator for a super-environment.

Change the environment of the constraint for a super-environment.

Change the environment of the expression for a super-environment.

Side-effect version of the previous function

Side-effet version of the previous function

Side-effect version of the previous function

Side-effect version of the previous function

Side-effet version of the previous function

Dump on the stdout C stream the internal representation of an abstract value, for debugging purposes

Dump on the stdout C stream the internal representation of an abstract value, for debugging purposes

Folding: fold a tvar fold the variables in the array tvar of size n>=1 and put the result in the first variable of the array.

Folding: fold a tdim fold the dimensions in the array tdim of size n>=1 and put the result in the first dimension of the array.

Return the default options for any function (0 or false for al fields)

Conversion from lexing buffers to resp.

Conversion from lists of strings to array of resp.

Conversion from strings to resp.

Get the coefficient of the variable in the underlying linear expression

Get the coefficient of the variable in the underlying linear expression

Get the coefficient of the variable

Get the coefficient corresponding to the dimension

Get the constant of the underlying linear expression

Get the constant

Get the constant

Get the environment of the tree expression constraint

Get the environment of the expression

Get the environment of the generator

Get the environment of the linear constraint

Get the environment of the expression

Get the corresponding result flag

Get the corresponding result flag

Get the options sets for the function.

Get the underlying generator of level 0.

Get the name of the effective library which allocated the manager

Get the underlying linear constraint of level 0.

Get the underlying expression of level 0 (which is not a copy).

Get the underlying linear expression.

Get the underlying linear expression.

Get the size of the linear expression (which may be sparse or dense)

Get the underlying tree expression constraint of level 0.

Get the underlying expression of level 0 (which is not a copy).

Get the underlying linear expression.

Get the constraint type

Get the generator type

Get the constraint type

Get the version of the effective library which allocated the manager

Hashing function for environments

Hash function

Hashing function

Hashing function

Create an interval coefficient from resp.

Build an interval from a lower and an upper bound

Emptiness test

Emptiness test

Does the interval contain no value ([a,b] with a>b) ?

Return true iff the argument value is a box value

Return true iff the argument value is a box value

Return true iff the argument value is a box value

Is the dimension unconstrained in the abstract value ? If yes, this means that the existential quantification of the dimension does not change the value.

Return true iff the argument value is a disjunction value

Return true iff the argument value is a disjunction value

Equality test.

Equality test.

Infinity test.

Does the linear expression depend only on integer variables ?

Inclusion test.

Inclusion test.

Inclusion test.

Return true iff the argument value is an oct value

Return true iff the argument value is an oct value

Return true iff the argument manager is a polka value

Return true iff the argument manager is a polka value

Return true iff the argument manager is a polkagrid value

Return true iff the argument manager is a polkagrid value

Return true iff the argument manager is a ppl value

Return true iff the argument manager is a ppl value

Return true iff the argument manager is a PPLite value

Return true iff the argument manager is a PPLite value

Does the linear expression depend only on real variables ?

Universality test

Universality test

Does the interval represent the universe ([-oo,+oo]) ?

Is the constraint not satisfiable ?

Is the variable unconstrained in the abstract value ? If yes, this means that the existential quantification of the dimension does not change the value.

Is the coefficient equal to scalar 0 or interval 0,0 ?

Is the interval equal to 0,0 ?

Iter the function on the pair coefficient/variable of the underlying linear expression

Iter the function on the pair coefficient/variable of the underlying linear expression

Iter the function on the pair coefficient/variable of the linear expression

Join of 2 abstract values.

Join of 2 abstract values.

Join of a non empty array of abstract values.

Join of a non empty array of abstract values.

Compute the least common environment of 2 environment, that is, the environment composed of all the variables of the 2 environments.

Similar to the previous function, but returns also the transformations required to convert from e1 (resp.

Make a tree expression constraint.

Make a generator.

Make a linear constraint.

Build a linear expression defined on the given argument, which is sparse by default.

Making an environment from a set of integer and real variables.

Make a tree expression constraint.

Making a generator.

Make a linear constraint.

Create a linear expression.

Build the unsatisfiable constraint -1>=0

Policy, general

Create a PolkaGrid manager from a (loose or strict) polka manager, and a PPL grid manager

Create a Taylor1+ manager.

Allocate a new manager to manipulate octagons.

Create a Box manager.

Create a NewPolka manager for conjunctions of linear equalities.

Allocate a new manager for linear congruences (grids)

Allocate a PPLite manager for loose convex polyhedra.

Allocate a PPL manager for loose convex polyhedra.

Create a NewPolka manager for loose convex polyhedra.

Allocate a PPLite manager for strict convex polyhedra.

Allocate a PPL manager for strict convex polyhedra.

Create a NewPolka manager for strict convex polyhedra.

Decompose the manager

Get the internal submanager of a NewPolka manager.

No internal parameters for now...

Get the polyhedra kind from PPLite manager.

Policy manager

Get the widening specification from PPLite manager.

Return true iff the argument manager is a box manager

Return true iff the argument manager is a disjunction manager

Return true iff the argument manager is an octagon manager

Return true iff the argument manager is a polka manager

Return true iff the argument manager is a polkagrid manager

Type conversions

Return true iff the argument manager is a ppl manager

Return true iff the argument manager is a PPLite manager

Make a box manager generic

Make a disjunction manager generic

Make an octagon manager generic

Makes a polka manager generic

Makes a polkagrid manager generic

Make a ppl manager generic

Make a PPLite manager generic

Set the polyhedra kind for PPLite manager.

Set the widening specification for PPLite manager.

Instanciate the type of a box manager.

Instanciate the type of a disjunction manager.

Instanciate the type of an octagon manager.

Instanciate the type of a polka manager.

Instanciate the type of a polkagrid manager.

Instanciate the type of a ppl manager.

Instantiate the type of a PPLite manager.

Meet of 2 abstract values.

Meet of 2 abstract values.

Meet of a non empty array of abstract values.

Meet of a non empty array of abstract values.

Meet of an abstract value with an array of linear constraints.

Meet of an abstract value with an array of linear constraints.

Meet of an abstract value with an array of tree expressions constraints.

Meet of an abstract value with an array of tree expression constraints.

Return true if the variable is present in the environment.

Minimize the size of the representation of the value.

In case of sparse representation, remove zero coefficients

Minimize the size of the representation of the value.

In case of sparse representation, remove zero coefficients

Remove from the environment of the abstract value and from the abstract value itself variables that are unconstrained in it.

Standard narrowing.

Negation

Negation

Negation

Combines Linexpr0.make and Linexpr0.set_array (see below)

Make a box value generic

Make a box value generic

Make a box value generic

Abstract an hypercube.

Abstract an hypercube.

Make a disjunction value generic

Make a disjunction value generic

General constructor (actually the most efficient)

General constructor (actually the most efficient

Create a scalar of type Float with the given value

Create a scalar of type Mpqf from resp.

Approximate a set of generators to an abstract value, with best precision.

depreciated

Create a scalar of type Float with the value multiplied by infinity (resulting in minus infinity, zero, or infinity

Conversion

Conversion

Combines Linexpr0.make and Linexpr0.set_list (see below)

Abstraction of lists of strings representing constraints to abstract values, on the abstract domain defined by the given manager.

Safe conversion from and to Mpfr.t.

Create an interval from resp.

Create a scalar of type Mpfrf with the given value

Safe conversion from and to Mpq.t.

Safe conversion from and to Mpz.t.

Make an oct value generic

Make an oct value generic

Makes a polka value generic

Makes a polka value generic

Makes a polkagrid value generic

Makes a polkagrid value generic

Make a ppl value generic

Make a ppl value generic

Make a PPLite value generic

Make a PPLite value generic

Build an interval from a lower and an upper bound

Constructor

Abstract a conjunction of constraints

Abstract a conjunction of constraints

perm_compose perm1 perm2 composes the 2 permutations perm1 and perm2 (in this order).

Invert a permutation

Algorithms.

Print as a set of constraints

Print the tree expression constraint

Print an abstract tree expression

Print the generator

Print the linear constraint

Print the linear expression

Printing

Printing function

Print as a set of constraints

Print a constraint

Print an abstract tree expression, using a function converting from dimensions to names

Print a generator

Print a constraint

Print a linear expression, using a function converting from dimensions to names

Printing

Print an interval, under the format [inf,sup]

Print a coefficient

General use

Printing functions

Print a tree expression

Print a tree expression, using a function converting from dimensions to names

Convert interval to scalar if possible

Remove from an environment a set of variables.

Renaming in an environment a set of variables.

Parallel renaming of the environment of the abstract value.

Similar to previous function, but returns also the permutation on dimensions induced by the renaming.

Create an interval coefficient of type Float with the given value

Create a scalar coefficient of type Mpqf.t from resp.

Create an interval coefficient of type Mpfr with the given value

Does the abstract value satisfy the constraint dim in interval?

Does the abstract value satisfy the constraint dim in interval ?

Does the abstract value satisfy the linear constraint ?

Does the abstract value satisfy the linear constraint ?

Does the abstract value satisfy the tree expression constraint ?

Does the abstract value satisfy the tree expression constraint ?

Set simultaneously a number of coefficients, as set_list.

Set simultaneously a number of coefficients, as set_list.

Set simultaneously a number of coefficients, as set_list.

Set simultaneously a number of coefficients, as set_list.

Fill the interval with top (resp.

Set the coefficient of the variable in the underlying linear expression

Set the coefficient of the variable in the underlying linear expression

Set the coefficient of the variable

Set the coefficient corresponding to the dimension

Set the constant of the underlying linear expression

Set the constant

Set the constant

Set / get the global manager used for deserialization

Set the options for the function.

Fill the interval with the given lower and upper bouunds

Set simultaneously a number of coefficients.

Set simultaneously a number of coefficients.

Set simultaneously a number of coefficients.

Set simultaneously a number of coefficients.

Set the constraint type

Set the generator type

Set the constraint type

Initialisation of abstract type operations in C library

Return the sign of the coefficient, which may be a negative value, zero or a positive value.

Return the abstract size of a value

Return the size of the environment

Return the abstract size of a value

Call sprintf with the given format string and arguments.

Convert a constraint type to a string (=,>=, or >)

Convert a constraint type to a string (=,>=, or >)

Convert a constraint type to a string (=,>=, or >)

Convert a generator type to a string (LIN,RAY, or VTX)

Convert a constraint type to a string (=,>=, or >)

As MPFR's strtofr, but returns a pair (r,i) where r is the usual ternary result, and i is the index in the string of the first not-read character.

Parallel substitution of an array of dimensions by an array of same size of linear expressions

Parallel substitution of an array of dimensions by an array of same size of linear expressions

Assignement/Substitution of a single dimension by a single expression

Assignement/Substitution of a single dimension by a single expression

Parallel substitution of an array of dimensions by an array of same size of tree expressions

Parallel substitution of an array of dimensions by an array of same size of tree expressions

Side-effect version of the previous functions

Side-effect version of the previous functions

Conversion from lexing buffers to resp.

Conversion from lists of strings to array of tree constraints.

Conversion from lexing buffers to resp.

Instanciate the type of a box value.

Instanciate the type of a box value.

Instanciate the type of a box value.

Convert the abstract value to an hypercube .

Convert the abstract value to an hypercube.

Instanciate the type of a disjunction value.

Instanciate the type of a disjunction value.

General destructor

General destructor

Convert the abstract value to a set of generators that defines it.

Convert the abstract value to a set of generators that defines it.

Convert the abstract value to a conjunction of linear constraints.

Convert the abstract value to a conjunction of linear constraints.

Instanciate the type of an oct value.

Instanciate the type of an oct value.

Instanciate the type of a polka value.

Instanciate the type of a polka value.

Instanciate the type of a polkagrid value.

Instanciate the type of a polkagrid value.

Instanciate the type of a ppl value.

Instanciate the type of a ppl value.

Instantiate the type of a PPLite value.

Instantiate the type of a PPLite value.

Conversion to string

Conversion to string, using string_of_double, Mpqf.to_string or Mpfr.to_string

Convert the abstract value to a conjunction of tree expression constraints.

Create a top (universe) value defined on the given environment

Create a top (universe) value with the given number of integer and real variables

Return the type of variables in the environment.

Unification of 2 abstract values on their least common environment

Side-effect version

Return the variable corresponding to the given dimension in the environment.

Return the (lexicographically ordered) sets of integer and real variables in the environment

Widening.

Widening.

Widening with scalar thresholds.