Abstract1

java.lang.Object
- apron.Abstract1

All Implemented Interfaces:

java.lang.Cloneable
```
public class Abstract1
extends java.lang.Object
implements java.lang.Cloneable
```
Class of level 1 numerical abstract values.
A level 1 numerical abstract value object represents a set of points in an environment.
An Abstract1 is implemented as a pair containing an Abstract0 and an Environment, manipulated in conjunction. Direct access to the fields is prohibited, to avoid desynchronizing them.

Field Summary

Fields
Modifier and Type Field and Description

protected Abstract0 abs
Level 0 abstract element.

protected Environment env
Environment.

Fields
Modifier and Type	Field and Description
`protected Abstract0`	`abs` Level 0 abstract element.
`protected Environment`	`env` Environment.

Constructor Summary

Constructors
Constructor and Description
`Abstract1(Manager man, Abstract1 a)` Creates a copy of the abstract element a.
`Abstract1(Manager man, Environment e)` Creates a new universal abstract element.
`Abstract1(Manager man, Environment e, boolean empty)` Creates a new universal or empty abstract element.
`Abstract1(Manager man, Environment e, java.lang.String[] vars, Interval[] box)`
`Abstract1(Manager man, Environment e, Var[] vars, Interval[] box)` Creates a new abstract element from a box.
`Abstract1(Manager man, Lincons1[] c)` Creates a new abstract element from a set of constraints.
`Abstract1(Manager man, Tcons1[] c)` Creates a new abstract element from a set of constraints.

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`void`	`addRay(Manager man, Generator1 r)` Replaces this with (an over-approximation of) this with one ray added.
`void`	`addRay(Manager man, Generator1[] ar)` Replaces this with (an over-approximation of) this with some rays added.
`Abstract1`	`addRayCopy(Manager man, Generator1 r)` Returns a new abstract element that contains (an over-approximation of) this with one ray added.
`Abstract1`	`addRayCopy(Manager man, Generator1[] ar)` Returns a new abstract element that contains (an over-approximation of) this with some rays added.
`void`	`approximate(Manager man, int algorithm)` Tries to simplify the representation of the element, maybe at the expense of precision.
`void`	`assign(Manager man, java.lang.String[] var, Linexpr1[] ar, Abstract1 dest)`
`void`	`assign(Manager man, java.lang.String[] var, Texpr1Intern[] ar, Abstract1 dest)`
`void`	`assign(Manager man, java.lang.String var, Linexpr1 expr, Abstract1 dest)`
`void`	`assign(Manager man, java.lang.String var, Texpr1Intern expr, Abstract1 dest)`
`void`	`assign(Manager man, Var[] var, Linexpr1[] ar, Abstract1 dest)` Replaces this with (an over-approximation of) this after assigning ar[i] to var[i], in parallel.
`void`	`assign(Manager man, Var[] var, Texpr1Intern[] ar, Abstract1 dest)` Replaces this with (an over-approximation of) this after assigning ar[i] to var[i], in parallel.
`void`	`assign(Manager man, Var var, Linexpr1 expr, Abstract1 dest)` Replaces this with (an over-approximation of) this after assigning expr to var.
`void`	`assign(Manager man, Var var, Texpr1Intern expr, Abstract1 dest)` Replaces this with (an over-approximation of) this after assigning expr to var.
`Abstract1`	`assignCopy(Manager man, java.lang.String[] var, Texpr1Intern[] ar, Abstract1 dest)`
`Abstract1`	`assignCopy(Manager man, java.lang.String var, Linexpr1 expr, Abstract1 dest)`
`Abstract1`	`assignCopy(Manager man, java.lang.String var, Texpr1Intern expr, Abstract1 dest)`
`Abstract1`	`assignCopy(Manager man, Var[] var, Linexpr1[] ar, Abstract1 dest)` Returns a new element containing (an over-approximation of) this after assigning ar[i] to var[i], in parallel.
`Abstract1`	`assignCopy(Manager man, Var[] var, Texpr1Intern[] ar, Abstract1 dest)` Returns a new element containing (an over-approximation of) this after assigning ar[i] to var[i], in parallel.
`Abstract1`	`assignCopy(Manager man, Var var, Linexpr1 expr, Abstract1 dest)` Returns a new element containing (an over-approximation of) this after assigning expr to var.
`Abstract1`	`assignCopy(Manager man, Var var, Texpr1Intern expr, Abstract1 dest)` Returns a new element containing (an over-approximation of) this after assigning expr to var.
`void`	`canonicalize(Manager man)` Tries to put the element in canonical form.
`void`	`changeEnvironment(Manager man, Environment e, boolean project)` Changes the environment into e.
`Abstract1`	`changeEnvironmentCopy(Manager man, Environment e, boolean project)` Returns a copy of this with new environment e.
`void`	`closure(Manager man)` Replaces this with (an over-approximation of) its topological closure.
`Abstract1`	`closureCopy(Manager man)` Returns a new element which is (an over-approximation of) the topological closure of this.
`static Abstract1`	`deserialize(Manager man, Environment e, byte[] buf)` Restores an abstract element from a byte array.
`void`	`expand(Manager man, java.lang.String org, java.lang.String[] dst)`
`void`	`expand(Manager man, Var org, Var[] dst)` Duplicates the variable org as dst[0] ... dst[dst.length-1].
`Abstract1`	`expandCopy(Manager man, java.lang.String org, java.lang.String[] dst)`
`Abstract1`	`expandCopy(Manager man, Var org, Var[] dst)` Returns a new element where variable org is duplicated as dst[0] ... dst[dst.length-1].
`void`	`fold(Manager man, java.lang.String[] var)`
`void`	`fold(Manager man, Var[] var)` Folds all variables var[i] into variable var[0].
`Abstract1`	`foldCopy(Manager man, java.lang.String[] var)`
`Abstract1`	`foldCopy(Manager man, Var[] var)` Returns a new element where all the variables var[i] are folded into the variable var[0].
`void`	`forget(Manager man, java.lang.String[] var, boolean project)`
`void`	`forget(Manager man, java.lang.String var, boolean project)`
`void`	`forget(Manager man, Var[] var, boolean project)` Replaces this with (an over-approximation of) this after forgetting the value of the variables in var.
`void`	`forget(Manager man, Var var, boolean project)` Replaces this with (an over-approximation of) this after forgetting the value of the variable var.
`Abstract1`	`forgetCopy(Manager man, java.lang.String[] var, boolean project)`
`Abstract1`	`forgetCopy(Manager man, java.lang.String var, boolean project)`
`Abstract1`	`forgetCopy(Manager man, Var[] var, boolean project)` Returns a new element containing (an over-approximation of) this after forgetting the value of the variables in var.
`Abstract1`	`forgetCopy(Manager man, Var var, boolean project)` Returns a new element containing (an over-approximation of) this after forgetting the value of the variable var.
`Abstract0`	`getAbstract0(Manager man)` Returns a copy of the Abstract0 underlying this.
`Abstract0`	`getAbstract0Ref()` Returns a (read-only) reference to the Abstract0 underlying this.
`Interval`	`getBound(Manager man, Linexpr1 e)` Returns (an over-approximation of) the set of values e can take on this.
`Interval`	`getBound(Manager man, java.lang.String var)`
`Interval`	`getBound(Manager man, Texpr1Intern e)` Returns (an over-approximation of) the set of values e can take on this.
`Interval`	`getBound(Manager man, Var var)` Returns (an over-approximation of) the set of values the variable var can take on this.
`Manager`	`getCreationManager()` Returns the Manager which was used to create the the abstract element.
`Environment`	`getEnvironment()` Returns the environment of the abstract element.
`int`	`getSize(Manager man)` Returns the size in memory of the abstract element.
`int`	`hashCode(Manager man)` Returns a hash of the element value.
`boolean`	`isBottom(Manager man)` Whether the element is definitely empty (true) or maybe not empty (false).
`boolean`	`isDimensionUnconstrained(Manager man, java.lang.String var)`
`boolean`	`isDimensionUnconstrained(Manager man, Var var)` Whether the variable var is definitely unbounded in this (true) or may be bounded (false).
`boolean`	`isEqual(Manager man, Abstract1 x)` Whether this is definitely equal to x (true) or maybe not equal (false).
`boolean`	`isIncluded(Manager man, Abstract1 x)` Whether this is definitely included in x (true) or maybe not included (false).
`boolean`	`isTop(Manager man)` Whether the element is definitely universal (true) or maybe not universal (false).
`void`	`join(Manager man, Abstract1 op)` Replaces this with (an over-approximation of) the set-union of this and op.
`static Abstract1`	`join(Manager man, Abstract1[] ar)` Returns a new abstract element that contains (an over-approximation of) the set-union of the elements in ar.
`Abstract1`	`joinCopy(Manager man, Abstract1 op)` Returns a new abstract element that contains (an over-approximation of) the set-union of this and op.
`void`	`meet(Manager man, Abstract1 op)` Replaces this with (an over-approximation of) the set-intersection of this and op.
`static Abstract1`	`meet(Manager man, Abstract1[] ar)` Returns a new abstract element that contains (an over-approximation of) the set-intersection of the elements in ar.
`void`	`meet(Manager man, Lincons1 c)` Replaces this with (an over-approximation of) the set-intersection of this with the constraint c.
`void`	`meet(Manager man, Lincons1[] ar)` Replaces this with (an over-approximation of) the set-intersection of this with the constraints in ar.
`void`	`meet(Manager man, Tcons1 c)` Replaces this with (an over-approximation of) the set-intersection of this with the constraint c.
`void`	`meet(Manager man, Tcons1[] ar)` Replaces this with (an over-approximation of) the set-intersection of this with the constraints in ar.
`Abstract1`	`meetCopy(Manager man, Abstract1 op)` Returns a new abstract element that contains (an over-approximation of) the set-intersection of this and op.
`Abstract1`	`meetCopy(Manager man, Lincons1 c)` Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraint cr.
`Abstract1`	`meetCopy(Manager man, Lincons1[] ar)` Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraints in ar.
`Abstract1`	`meetCopy(Manager man, Tcons1 c)` Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraint in c.
`Abstract1`	`meetCopy(Manager man, Tcons1[] ar)` Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraints in ar.
`void`	`minimize(Manager man)` Tries to minimize the memory representation of the element.
`void`	`minimizeEnvironment(Manager man)` Removes all unconstrained variables.
`Abstract1`	`minimizeEnvironmentCopy(Manager man)` Returns a copy of this with all unconstrained variables removed.
`void`	`rename(Manager man, java.lang.String[] org, java.lang.String[] dst)`
`void`	`rename(Manager man, Var[] org, Var[] dst)` Renames variable org[i] as dst[i].
`Abstract1`	`renameCopy(Manager man, java.lang.String[] org, java.lang.String[] dst)`
`Abstract1`	`renameCopy(Manager man, Var[] org, Var[] dst)` Returns a copy of this with variable org[i] renamed as dst[i].
`boolean`	`satisfy(Manager man, Lincons1 c)` Whether this definitely satisfies the constraint c (true) or maybe does not satisfy it (false).
`boolean`	`satisfy(Manager man, java.lang.String var, Interval i)`
`boolean`	`satisfy(Manager man, Tcons1 c)` Whether this definitely satisfies the constraint c (true) or maybe does not satisfy it (false).
`boolean`	`satisfy(Manager man, Var var, Interval i)` Whether the projection of this on variable var is definitely included in the interval i (true) or maybe is not included (false).
`byte[]`	`serialize(Manager man)` Converts the abstract element to a byte array.
`void`	`substitute(Manager man, java.lang.String[] var, Linexpr1[] ar, Abstract1 dest)`
`void`	`substitute(Manager man, java.lang.String[] var, Texpr1Intern[] ar, Abstract1 dest)`
`void`	`substitute(Manager man, java.lang.String var, Linexpr1 expr, Abstract1 dest)`
`void`	`substitute(Manager man, java.lang.String var, Texpr1Intern expr, Abstract1 dest)`
`void`	`substitute(Manager man, Var[] var, Linexpr1[] ar, Abstract1 dest)` Replaces this with (an over-approximation of) this after substituting var[i] with ar[i], in parallel.
`void`	`substitute(Manager man, Var[] var, Texpr1Intern[] ar, Abstract1 dest)` Replaces this with (an over-approximation of) this after substituting var[i] with ar[i], in parallel.
`void`	`substitute(Manager man, Var var, Linexpr1 expr, Abstract1 dest)` Replaces this with (an over-approximation of) this after substituting var with expr.
`void`	`substitute(Manager man, Var var, Texpr1Intern expr, Abstract1 dest)` Replaces this with (an over-approximation of) this after substituting var with expr.
`Abstract1`	`substituteCopy(Manager man, java.lang.String[] var, Texpr1Intern[] ar, Abstract1 dest)`
`Abstract1`	`substituteCopy(Manager man, java.lang.String var, Linexpr1 expr, Abstract1 dest)`
`Abstract1`	`substituteCopy(Manager man, java.lang.String var, Texpr1Intern expr, Abstract1 dest)`
`Abstract1`	`substituteCopy(Manager man, Var[] var, Linexpr1[] ar, Abstract1 dest)` Returns a new element containing (an over-approximation of) this after substituting var[i] with ar[i], in parallel.
`Abstract1`	`substituteCopy(Manager man, Var[] var, Texpr1Intern[] ar, Abstract1 dest)` Returns a new element containing (an over-approximation of) this after substituting var[i] with ar[i], in parallel.
`Abstract1`	`substituteCopy(Manager man, Var var, Linexpr1 expr, Abstract1 dest)` Returns a new element containing (an over-approximation of) this after substituting var with expr.
`Abstract1`	`substituteCopy(Manager man, Var var, Texpr1Intern expr, Abstract1 dest)` Returns a new element containing (an over-approximation of) this after substituting var with expr.
`Interval[]`	`toBox(Manager man)` Returns a box describing (an over-approximation of) this.
`Generator1[]`	`toGenerator(Manager man)` Returns a set of generators describing (an over-approximation of) this.
`Lincons1[]`	`toLincons(Manager man)` Returns a set of linear constraints describing (an over-approximation of) this.
`java.lang.String`	`toString()` Returns a String representation of the element as a list of constraints.
`java.lang.String`	`toString(Manager man)` Returns a String representation of the element as a list of constraints.
`Tcons1[]`	`toTcons(Manager man)` Returns a set of constraints describing (an over-approximation of) this.
`void`	`unify(Manager man, Abstract1 op)` Replaces this with the meet of this and op on their least common environment.
`Abstract1`	`unifyCopy(Manager man, Abstract1 op)` Returns the meet of this and op on their least common environment.
`Abstract1`	`widening(Manager man, Abstract1 op)` Returns a new element equal to this widened with op.
`Abstract1`	`wideningThreshold(Manager man, Abstract1 op, Lincons1[] c)` Returns a new element equal to this widened with op, with thresholds constraints set c.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

abs
```
protected Abstract0 abs
```
Level 0 abstract element.

env
```
protected Environment env
```
Environment.

Constructor Detail

Abstract1

public Abstract1(Manager man,
                 Abstract1 a)
          throws ApronException

Creates a copy of the abstract element a.

Throws:: ApronException

Abstract1

public Abstract1(Manager man,
                 Environment e)
          throws ApronException

Creates a new universal abstract element.

Throws:: ApronException

Abstract1

public Abstract1(Manager man,
                 Environment e,
                 boolean empty)
          throws ApronException

Creates a new universal or empty abstract element.

Throws:: ApronException

Abstract1
```
public Abstract1(Manager man,
                 Environment e,
                 Var[] vars,
                 Interval[] box)
          throws ApronException
```
Creates a new abstract element from a box.
The element is such that vars[i] is in interval box[i]. Variables not in vars have interval [-oo,+oo].
All variables from vars must be exist in the environment e.
vars and box must have the same length.

Throws:

ApronException

Abstract1

public Abstract1(Manager man,
                 Environment e,
                 java.lang.String[] vars,
                 Interval[] box)
          throws ApronException

Throws:: ApronException

Abstract1
```
public Abstract1(Manager man,
                 Lincons1[] c)
          throws ApronException
```
Creates a new abstract element from a set of constraints.
All constraints must have the same environment.
The array must not be empty (to get an environment).

Throws:

ApronException

Abstract1
```
public Abstract1(Manager man,
                 Tcons1[] c)
          throws ApronException
```
Creates a new abstract element from a set of constraints.
All constraints must have the same environment.
The array must not be empty (to get an environment).

Throws:

ApronException

Method Detail

getSize
```
public int getSize(Manager man)
            throws ApronException
```
Returns the size in memory of the abstract element.
The unit is domain-specific.

Throws:

ApronException

hashCode

public int hashCode(Manager man)
             throws ApronException

Returns a hash of the element value.

Throws:: ApronException

getEnvironment
```
public Environment getEnvironment()
```
Returns the environment of the abstract element.

getAbstract0

public Abstract0 getAbstract0(Manager man)
                       throws ApronException

Returns a copy of the Abstract0 underlying this.

Throws:: ApronException

getAbstract0Ref
```
public Abstract0 getAbstract0Ref()
```
Returns a (read-only) reference to the Abstract0 underlying this.
Warning: it is dangerous to add, remove, or permute dimensions as it may desynchrnonize the Abstract0 dimensions form the environment.

getCreationManager
```
public Manager getCreationManager()
```
Returns the Manager which was used to create the the abstract element.

toString
```
public java.lang.String toString()
```
Returns a String representation of the element as a list of constraints.
This method uses the Manager that was used to create this.

Overrides:

toString in class java.lang.Object

toString
```
public java.lang.String toString(Manager man)
```
Returns a String representation of the element as a list of constraints.

getBound

public Interval getBound(Manager man,
                         Linexpr1 e)
                  throws ApronException

Returns (an over-approximation of) the set of values e can take on this.

this and e must have the same environment.

Throws:: ApronException

getBound

public Interval getBound(Manager man,
                         Texpr1Intern e)
                  throws ApronException

Returns (an over-approximation of) the set of values e can take on this.

this and e must have the same environment.

Throws:: ApronException

getBound

public Interval getBound(Manager man,
                         java.lang.String var)
                  throws ApronException

Throws:: ApronException

getBound

public Interval getBound(Manager man,
                         Var var)
                  throws ApronException

Returns (an over-approximation of) the set of values the variable var can take on this.

Throws:: ApronException

toLincons
```
public Lincons1[] toLincons(Manager man)
                     throws ApronException
```
Returns a set of linear constraints describing (an over-approximation of) this.

Throws:

ApronException

toTcons
```
public Tcons1[] toTcons(Manager man)
                 throws ApronException
```
Returns a set of constraints describing (an over-approximation of) this.

Throws:

ApronException

toBox
```
public Interval[] toBox(Manager man)
                 throws ApronException
```
Returns a box describing (an over-approximation of) this.
The variable order in the returned array is that of the environment, i.e., getEnvironment().getVars().

Throws:

ApronException

toGenerator
```
public Generator1[] toGenerator(Manager man)
                         throws ApronException
```
Returns a set of generators describing (an over-approximation of) this.

Throws:

ApronException

isBottom
```
public boolean isBottom(Manager man)
                 throws ApronException
```
Whether the element is definitely empty (true) or maybe not empty (false).
If Manager.wasExact() returns true, then false indicates that the element is definitely empty.

Throws:

ApronException

isTop
```
public boolean isTop(Manager man)
              throws ApronException
```
Whether the element is definitely universal (true) or maybe not universal (false).
If Manager.wasExact() returns true, then false indicates that the element is definitely not universal.

Throws:

ApronException

isIncluded
```
public boolean isIncluded(Manager man,
                          Abstract1 x)
                   throws ApronException
```
Whether this is definitely included in x (true) or maybe not included (false).
If Manager.wasExact() returns true, then false indicates that this is definitely not included in x.
this and x must have the same environment.

Throws:

ApronException

isEqual
```
public boolean isEqual(Manager man,
                       Abstract1 x)
                throws ApronException
```
Whether this is definitely equal to x (true) or maybe not equal (false).
If Manager.wasExact() returns true, then false indicates that this is definitely not equal to x.
this and x must have the same environment.

Throws:

ApronException

satisfy
```
public boolean satisfy(Manager man,
                       Lincons1 c)
                throws ApronException
```
Whether this definitely satisfies the constraint c (true) or maybe does not satisfy it (false).
If Manager.wasExact() returns true, then false indicates that this definitely does not satisfy c.
this and c must have the same environment.

Throws:

ApronException

satisfy
```
public boolean satisfy(Manager man,
                       Tcons1 c)
                throws ApronException
```
Whether this definitely satisfies the constraint c (true) or maybe does not satisfy it (false).
If Manager.wasExact() returns true, then false indicates that this definitely does not satisfy c.
this and c must have the same environment.

Throws:

ApronException

satisfy

public boolean satisfy(Manager man,
                       java.lang.String var,
                       Interval i)
                throws ApronException

Throws:: ApronException

satisfy
```
public boolean satisfy(Manager man,
                       Var var,
                       Interval i)
                throws ApronException
```
Whether the projection of this on variable var is definitely included in the interval i (true) or maybe is not included (false).
If Manager.wasExact() returns true, then false indicates that it is definitely not included.

Throws:

ApronException

isDimensionUnconstrained

public boolean isDimensionUnconstrained(Manager man,
                                        java.lang.String var)
                                 throws ApronException

Throws:: ApronException

isDimensionUnconstrained
```
public boolean isDimensionUnconstrained(Manager man,
                                        Var var)
                                 throws ApronException
```
Whether the variable var is definitely unbounded in this (true) or may be bounded (false).
If Manager.wasExact() returns true, then false indicates that the dimension is definitely bounded.

Throws:

ApronException

minimize
```
public void minimize(Manager man)
              throws ApronException
```
Tries to minimize the memory representation of the element.
Use this to gain memory space. However, this may cause subsequent operations to be less efficients as cached information may be discarded.

Throws:

ApronException

canonicalize
```
public void canonicalize(Manager man)
                  throws ApronException
```
Tries to put the element in canonical form.
The notion of canonical form is not fully defined yet.

Throws:

ApronException

approximate
```
public void approximate(Manager man,
                        int algorithm)
                 throws ApronException
```
Tries to simplify the representation of the element, maybe at the expense of precision.
The algorithm argument indicates how aggressive the simplification should be. Its interpretation is domain-dependant.

Throws:

ApronException

meetCopy
```
public Abstract1 meetCopy(Manager man,
                          Abstract1 op)
                   throws ApronException
```
Returns a new abstract element that contains (an over-approximation of) the set-intersection of this and op.
this and op are not modified.
this and op must have the same environment.

Throws:

ApronException

meet
```
public static Abstract1 meet(Manager man,
                             Abstract1[] ar)
                      throws ApronException
```
Returns a new abstract element that contains (an over-approximation of) the set-intersection of the elements in ar.
The elements of ar are not modified.
The array must not be empty.
All array elements must have the same environment.

Throws:

ApronException

meet
```
public void meet(Manager man,
                 Abstract1 op)
          throws ApronException
```
Replaces this with (an over-approximation of) the set-intersection of this and op.
op is not modified.
this and op must have the same environment.

Throws:

ApronException

joinCopy
```
public Abstract1 joinCopy(Manager man,
                          Abstract1 op)
                   throws ApronException
```
Returns a new abstract element that contains (an over-approximation of) the set-union of this and op.
this and op are not modified.
this and op must have the same environment.

Throws:

ApronException

join
```
public static Abstract1 join(Manager man,
                             Abstract1[] ar)
                      throws ApronException
```
Returns a new abstract element that contains (an over-approximation of) the set-union of the elements in ar.
The elements of ar are not modified.
The array must not be empty.
All array elements must have the same environment.

Throws:

ApronException

join
```
public void join(Manager man,
                 Abstract1 op)
          throws ApronException
```
Replaces this with (an over-approximation of) the set-union of this and op.
op is not modified.
this and op must have the same environment.

Throws:

ApronException

meetCopy
```
public Abstract1 meetCopy(Manager man,
                          Lincons1[] ar)
                   throws ApronException
```
Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraints in ar.
this is not changed.
this and all array elements must have the same environment.

Throws:

ApronException

meetCopy
```
public Abstract1 meetCopy(Manager man,
                          Tcons1[] ar)
                   throws ApronException
```
Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraints in ar.
this is not changed.
this and all array elements must have the same environment.

Throws:

ApronException

meet
```
public void meet(Manager man,
                 Lincons1[] ar)
          throws ApronException
```
Replaces this with (an over-approximation of) the set-intersection of this with the constraints in ar.
this and all array elements must have the same environment.

Throws:

ApronException

meet
```
public void meet(Manager man,
                 Tcons1[] ar)
          throws ApronException
```
Replaces this with (an over-approximation of) the set-intersection of this with the constraints in ar.
this and all array elements must have the same environment.

Throws:

ApronException

meetCopy
```
public Abstract1 meetCopy(Manager man,
                          Lincons1 c)
                   throws ApronException
```
Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraint cr.
this is not changed.
this and c must have the same environment.

Throws:

ApronException

meetCopy
```
public Abstract1 meetCopy(Manager man,
                          Tcons1 c)
                   throws ApronException
```
Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraint in c.
this is not changed.
this and c must have the same environment.

Throws:

ApronException

meet
```
public void meet(Manager man,
                 Lincons1 c)
          throws ApronException
```
Replaces this with (an over-approximation of) the set-intersection of this with the constraint c.
this and c must have the same environment.

Throws:

ApronException

meet
```
public void meet(Manager man,
                 Tcons1 c)
          throws ApronException
```
Replaces this with (an over-approximation of) the set-intersection of this with the constraint c.
this and c must have the same environment.

Throws:

ApronException

addRayCopy
```
public Abstract1 addRayCopy(Manager man,
                            Generator1[] ar)
                     throws ApronException
```
Returns a new abstract element that contains (an over-approximation of) this with some rays added.
this is not changed.
ar can only contain ray and lines, not vertices.
this and all array elements must have the same environment.

Throws:

ApronException

addRay
```
public void addRay(Manager man,
                   Generator1[] ar)
            throws ApronException
```
Replaces this with (an over-approximation of) this with some rays added.
ar can only contain ray and lines, not vertices.
this and all array elements must have the same environment.

Throws:

ApronException

addRayCopy
```
public Abstract1 addRayCopy(Manager man,
                            Generator1 r)
                     throws ApronException
```
Returns a new abstract element that contains (an over-approximation of) this with one ray added.
this is not changed.
this and r must have the same environment.

Throws:

ApronException

addRay
```
public void addRay(Manager man,
                   Generator1 r)
            throws ApronException
```
Replaces this with (an over-approximation of) this with one ray added.
this and r must have the same environment.

Throws:

ApronException

assign

public void assign(Manager man,
                   java.lang.String[] var,
                   Linexpr1[] ar,
                   Abstract1 dest)
            throws ApronException

Throws:: ApronException

assign
```
public void assign(Manager man,
                   Var[] var,
                   Linexpr1[] ar,
                   Abstract1 dest)
            throws ApronException
```
Replaces this with (an over-approximation of) this after assigning ar[i] to var[i], in parallel.
The result is intersected with dest, if dest is not null.
this, dest, and the array must have the same environment.

Throws:

ApronException

assignCopy

public Abstract1 assignCopy(Manager man,
                            Var[] var,
                            Linexpr1[] ar,
                            Abstract1 dest)
                     throws ApronException

Returns a new element containing (an over-approximation of) this after assigning ar[i] to var[i], in parallel.

this is not modified.

The result is intersected with dest, if dest is not null.

this, dest, and the array must have the same environment.

Throws:: ApronException

assign

public void assign(Manager man,
                   java.lang.String[] var,
                   Texpr1Intern[] ar,
                   Abstract1 dest)
            throws ApronException

Throws:: ApronException

assign

public void assign(Manager man,
                   Var[] var,
                   Texpr1Intern[] ar,
                   Abstract1 dest)
            throws ApronException

Replaces this with (an over-approximation of) this after assigning ar[i] to var[i], in parallel.

The result is intersected with dest, if dest is not null.

this, dest, and the array must have the same environment.

Throws:: ApronException

assignCopy

public Abstract1 assignCopy(Manager man,
                            java.lang.String[] var,
                            Texpr1Intern[] ar,
                            Abstract1 dest)
                     throws ApronException

Throws:: ApronException

assignCopy

public Abstract1 assignCopy(Manager man,
                            Var[] var,
                            Texpr1Intern[] ar,
                            Abstract1 dest)
                     throws ApronException

Returns a new element containing (an over-approximation of) this after assigning ar[i] to var[i], in parallel.

this is not modified.

The result is intersected with dest, if dest is not null.

this, dest, and the array must have the same environment.

Throws:: ApronException

substitute

public void substitute(Manager man,
                       java.lang.String[] var,
                       Linexpr1[] ar,
                       Abstract1 dest)
                throws ApronException

Throws:: ApronException

substitute

public void substitute(Manager man,
                       Var[] var,
                       Linexpr1[] ar,
                       Abstract1 dest)
                throws ApronException

Replaces this with (an over-approximation of) this after substituting var[i] with ar[i], in parallel.

The result is intersected with dest, if dest is not null.

this, dest, and the array must have the same environment.

Throws:: ApronException

substituteCopy

public Abstract1 substituteCopy(Manager man,
                                Var[] var,
                                Linexpr1[] ar,
                                Abstract1 dest)
                         throws ApronException

Returns a new element containing (an over-approximation of) this after substituting var[i] with ar[i], in parallel.

this is not modified.

The result is intersected with dest, if dest is not null.

this, dest, and the array must have the same environment.

Throws:: ApronException

substitute

public void substitute(Manager man,
                       java.lang.String[] var,
                       Texpr1Intern[] ar,
                       Abstract1 dest)
                throws ApronException

Throws:: ApronException

substitute

public void substitute(Manager man,
                       Var[] var,
                       Texpr1Intern[] ar,
                       Abstract1 dest)
                throws ApronException

Replaces this with (an over-approximation of) this after substituting var[i] with ar[i], in parallel.

The result is intersected with dest, if dest is not null.

this, dest, and the array must have the same environment.

Throws:: ApronException

substituteCopy

public Abstract1 substituteCopy(Manager man,
                                java.lang.String[] var,
                                Texpr1Intern[] ar,
                                Abstract1 dest)
                         throws ApronException

Throws:: ApronException

substituteCopy

public Abstract1 substituteCopy(Manager man,
                                Var[] var,
                                Texpr1Intern[] ar,
                                Abstract1 dest)
                         throws ApronException

Returns a new element containing (an over-approximation of) this after substituting var[i] with ar[i], in parallel.

this is not modified.

The result is intersected with dest, if dest is not null.

this, dest, and the array must have the same environment.

Throws:: ApronException

assign

public void assign(Manager man,
                   java.lang.String var,
                   Linexpr1 expr,
                   Abstract1 dest)
            throws ApronException

Throws:: ApronException

assign

public void assign(Manager man,
                   Var var,
                   Linexpr1 expr,
                   Abstract1 dest)
            throws ApronException

Replaces this with (an over-approximation of) this after assigning expr to var.

The result is intersected with dest, if dest is not null.

this, dest, and expr must have the same environment.

Throws:: ApronException

assignCopy

public Abstract1 assignCopy(Manager man,
                            java.lang.String var,
                            Linexpr1 expr,
                            Abstract1 dest)
                     throws ApronException

Throws:: ApronException

assignCopy

public Abstract1 assignCopy(Manager man,
                            Var var,
                            Linexpr1 expr,
                            Abstract1 dest)
                     throws ApronException

Returns a new element containing (an over-approximation of) this after assigning expr to var.

this is not modified.

The result is intersected with dest, if dest is not null.

this, dest, and expr must have the same environment.

Throws:: ApronException

assign

public void assign(Manager man,
                   java.lang.String var,
                   Texpr1Intern expr,
                   Abstract1 dest)
            throws ApronException

Throws:: ApronException

assign

public void assign(Manager man,
                   Var var,
                   Texpr1Intern expr,
                   Abstract1 dest)
            throws ApronException

Replaces this with (an over-approximation of) this after assigning expr to var.

The result is intersected with dest, if dest is not null.

this, dest, and expr must have the same environment.

Throws:: ApronException

assignCopy

public Abstract1 assignCopy(Manager man,
                            java.lang.String var,
                            Texpr1Intern expr,
                            Abstract1 dest)
                     throws ApronException

Throws:: ApronException

assignCopy

public Abstract1 assignCopy(Manager man,
                            Var var,
                            Texpr1Intern expr,
                            Abstract1 dest)
                     throws ApronException

Returns a new element containing (an over-approximation of) this after assigning expr to var.

this is not modified.

The result is intersected with dest, if dest is not null.

this, dest, and expr must have the same environment.

Throws:: ApronException

substitute

public void substitute(Manager man,
                       java.lang.String var,
                       Linexpr1 expr,
                       Abstract1 dest)
                throws ApronException

Throws:: ApronException

substitute

public void substitute(Manager man,
                       Var var,
                       Linexpr1 expr,
                       Abstract1 dest)
                throws ApronException

Replaces this with (an over-approximation of) this after substituting var with expr.

The result is intersected with dest, if dest is not null.

this, dest, and expr must have the same environment.

Throws:: ApronException

substituteCopy

public Abstract1 substituteCopy(Manager man,
                                java.lang.String var,
                                Linexpr1 expr,
                                Abstract1 dest)
                         throws ApronException

Throws:: ApronException

substituteCopy

public Abstract1 substituteCopy(Manager man,
                                Var var,
                                Linexpr1 expr,
                                Abstract1 dest)
                         throws ApronException

Returns a new element containing (an over-approximation of) this after substituting var with expr.

this is not modified.

The result is intersected with dest, if dest is not null.

this, dest, and expr must have the same environment.

Throws:: ApronException

substitute

public void substitute(Manager man,
                       java.lang.String var,
                       Texpr1Intern expr,
                       Abstract1 dest)
                throws ApronException

Throws:: ApronException

substitute

public void substitute(Manager man,
                       Var var,
                       Texpr1Intern expr,
                       Abstract1 dest)
                throws ApronException

Replaces this with (an over-approximation of) this after substituting var with expr.

The result is intersected with dest, if dest is not null.

this, dest, and expr must have the same environment.

Throws:: ApronException

substituteCopy

public Abstract1 substituteCopy(Manager man,
                                java.lang.String var,
                                Texpr1Intern expr,
                                Abstract1 dest)
                         throws ApronException

Throws:: ApronException

substituteCopy

public Abstract1 substituteCopy(Manager man,
                                Var var,
                                Texpr1Intern expr,
                                Abstract1 dest)
                         throws ApronException

Returns a new element containing (an over-approximation of) this after substituting var with expr.

this is not modified.

The result is intersected with dest, if dest is not null.

this, dest, and expr must have the same environment.

Throws:: ApronException

forgetCopy

public Abstract1 forgetCopy(Manager man,
                            java.lang.String[] var,
                            boolean project)
                     throws ApronException

Throws:: ApronException

forgetCopy
```
public Abstract1 forgetCopy(Manager man,
                            Var[] var,
                            boolean project)
                     throws ApronException
```
Returns a new element containing (an over-approximation of) this after forgetting the value of the variables in var.
this is not modified.
If project is true, the variables are set to 0. Otherwise, they are set to [-oo,+oo].

Throws:

ApronException

forget

public void forget(Manager man,
                   java.lang.String[] var,
                   boolean project)
            throws ApronException

Throws:: ApronException

forget
```
public void forget(Manager man,
                   Var[] var,
                   boolean project)
            throws ApronException
```
Replaces this with (an over-approximation of) this after forgetting the value of the variables in var.
If project is true, the variables are set to 0. Otherwise, they are set to [-oo,+oo].

Throws:

ApronException

forgetCopy

public Abstract1 forgetCopy(Manager man,
                            java.lang.String var,
                            boolean project)
                     throws ApronException

Throws:: ApronException

forgetCopy

public Abstract1 forgetCopy(Manager man,
                            Var var,
                            boolean project)
                     throws ApronException

Returns a new element containing (an over-approximation of) this after forgetting the value of the variable var.

this is not modified.

Throws:: ApronException

forget

public void forget(Manager man,
                   java.lang.String var,
                   boolean project)
            throws ApronException

Throws:: ApronException

forget

public void forget(Manager man,
                   Var var,
                   boolean project)
            throws ApronException

Replaces this with (an over-approximation of) this after forgetting the value of the variable var.

Throws:: ApronException

changeEnvironmentCopy
```
public Abstract1 changeEnvironmentCopy(Manager man,
                                       Environment e,
                                       boolean project)
                                throws ApronException
```
Returns a copy of this with new environment e.
Variables in this and not in e are removed, while variables in e and not in this are created.
project indicates whether added variables are set to 0 (true) or [-oo,+oo] (false).
this and e must have compatible environments.
this is not modified.

Throws:

ApronException

changeEnvironment
```
public void changeEnvironment(Manager man,
                              Environment e,
                              boolean project)
                       throws ApronException
```
Changes the environment into e.
Variables in this and not in e are removed, while variables in e and not in this are created.
project indicates whether added variables are set to 0 (true) or [-oo,+oo] (false).
this and e must have compatible environments.

Throws:

ApronException

minimizeEnvironmentCopy
```
public Abstract1 minimizeEnvironmentCopy(Manager man)
                                  throws ApronException
```
Returns a copy of this with all unconstrained variables removed.
this is not modified.

Throws:

ApronException

minimizeEnvironment

public void minimizeEnvironment(Manager man)
                         throws ApronException

Removes all unconstrained variables.

Throws:: ApronException

renameCopy

public Abstract1 renameCopy(Manager man,
                            java.lang.String[] org,
                            java.lang.String[] dst)
                     throws ApronException

Throws:: ApronException

renameCopy

public Abstract1 renameCopy(Manager man,
                            Var[] org,
                            Var[] dst)
                     throws ApronException

Returns a copy of this with variable org[i] renamed as dst[i].

org and dst must have the same size.

this is not modified.

Throws:: ApronException

rename

public void rename(Manager man,
                   java.lang.String[] org,
                   java.lang.String[] dst)
            throws ApronException

Throws:: ApronException

rename

public void rename(Manager man,
                   Var[] org,
                   Var[] dst)
            throws ApronException

Renames variable org[i] as dst[i].

org and dst must have the same size.

Throws:: ApronException

unifyCopy

public Abstract1 unifyCopy(Manager man,
                           Abstract1 op)
                    throws ApronException

Returns the meet of this and op on their least common environment.

Throws:: ApronException

unify

public void unify(Manager man,
                  Abstract1 op)
           throws ApronException

Replaces this with the meet of this and op on their least common environment.

Throws:: ApronException

expandCopy

public Abstract1 expandCopy(Manager man,
                            java.lang.String org,
                            java.lang.String[] dst)
                     throws ApronException

Throws:: ApronException

expandCopy

public Abstract1 expandCopy(Manager man,
                            Var org,
                            Var[] dst)
                     throws ApronException

Returns a new element where variable org is duplicated as dst[0] ... dst[dst.length-1].

this is not modified.

Throws:: ApronException

expand

public void expand(Manager man,
                   java.lang.String org,
                   java.lang.String[] dst)
            throws ApronException

Throws:: ApronException

expand

public void expand(Manager man,
                   Var org,
                   Var[] dst)
            throws ApronException

Duplicates the variable org as dst[0] ... dst[dst.length-1].

Throws:: ApronException

foldCopy

public Abstract1 foldCopy(Manager man,
                          java.lang.String[] var)
                   throws ApronException

Throws:: ApronException

foldCopy
```
public Abstract1 foldCopy(Manager man,
                          Var[] var)
                   throws ApronException
```
Returns a new element where all the variables var[i] are folded into the variable var[0].
The array must contain either only integer-valued or real-valued variables.
this is not modified.

Throws:

ApronException

fold

public void fold(Manager man,
                 java.lang.String[] var)
          throws ApronException

Throws:: ApronException

fold
```
public void fold(Manager man,
                 Var[] var)
          throws ApronException
```
Folds all variables var[i] into variable var[0].
The array must contain either only integer-valued or real-valued variables.

Throws:

ApronException

widening

public Abstract1 widening(Manager man,
                          Abstract1 op)
                   throws ApronException

Returns a new element equal to this widened with op.

this and op are not modified.

this and op must have the same environment.

Throws:: ApronException

wideningThreshold

public Abstract1 wideningThreshold(Manager man,
                                   Abstract1 op,
                                   Lincons1[] c)
                            throws ApronException

Returns a new element equal to this widened with op, with thresholds constraints set c.

this and op are not modified.

this, op, and c must have the same environment.

Throws:: ApronException

closureCopy
```
public Abstract1 closureCopy(Manager man)
                      throws ApronException
```
Returns a new element which is (an over-approximation of) the topological closure of this.
this is not modified.

Throws:

ApronException

closure
```
public void closure(Manager man)
             throws ApronException
```
Replaces this with (an over-approximation of) its topological closure.

Throws:

ApronException

serialize
```
public byte[] serialize(Manager man)
                 throws ApronException
```
Converts the abstract element to a byte array.
The byte array can be stored to and retrieved from disk, or sent through a network. However, the sending and receiving parties must use compatible managers and identical environments.

Throws:

ApronException

deserialize

public static Abstract1 deserialize(Manager man,
                                    Environment e,
                                    byte[] buf)
                             throws ApronException

Restores an abstract element from a byte array.

The specified manager must be compatible with that used during the serialize(apron.Manager) call. The environments must be identical.

Throws:: ApronException

Class Abstract1

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

abs

env

Constructor Detail

Abstract1

Abstract1

Abstract1

Abstract1

Abstract1

Abstract1

Abstract1

Method Detail

getSize

hashCode

getEnvironment

getAbstract0

getAbstract0Ref

getCreationManager

toString

toString

getBound

getBound

getBound

getBound

toLincons

toTcons

toBox

toGenerator

isBottom

isTop

isIncluded

isEqual

satisfy

satisfy

satisfy

satisfy

isDimensionUnconstrained

isDimensionUnconstrained

minimize

canonicalize

approximate

meetCopy

meet

meet

joinCopy

join

join

meetCopy

meetCopy

meet

meet

meetCopy

meetCopy

meet

meet

addRayCopy

addRay

addRayCopy

addRay

assign

assign

assignCopy

assign

assign

assignCopy

assignCopy

substitute

substitute

substituteCopy

substitute

substitute

substituteCopy

substituteCopy

assign

assign