Package apron

Class Abstract0

java.lang.Object

apron.Abstract0

All Implemented Interfaces:

Cloneable

public class Abstract0
extends Object
implements Cloneable

Class of level 0 numerical abstract values.

A level 0 numerical abstract value object represents a set of points in Z^n * R^m, for some n and m.

All abstract element methods are applied within a given Manager that indicates which numerical abstract domain instance is used. Most often, which Manager is used is specified as an argument. It must be a Manager compatible (i.e., from the same factory, and constructed using the same parameters) with the one the Abstract0 arguments were created with. A few functions (such as finalize, toString) cannot take a Manager argument. They are applied implicitly with the Manager used when creating the object.

An Abstract0 object encapsulates an ap_abstract0_t Apron object allocated in the C heap.

Constructor Summary

Constructors

Constructor	Description
Abstract0(Manager man, int intdim, int realdim)	Creates a new universal abstract element.
Abstract0(Manager man, int intdim, int realdim, boolean empty)	Creates a new universal or empty abstract element.
Abstract0(Manager man, int intdim, int realdim, Interval[] box)	Creates a new abstract element from a box.
Abstract0(Manager man, int intdim, int realdim, Lincons0[] c)	Creates a new abstract element from a set of constraints.
Abstract0(Manager man, int intdim, int realdim, Tcons0[] c)	Creates a new abstract element from a set of constraints.
Abstract0(Manager man, Abstract0 a)	Creates a copy of the abstract element a.

Method Summary

Modifier and Type	Method	Description
void	addDimensions(Manager man, Dimchange d, boolean project)	Adds some dimensions to this.
Abstract0	addDimensionsCopy(Manager man, Dimchange d, boolean project)	Returns a new element containing this after adding some dimensions.
void	addRay(Manager man, Generator0 r)	Replaces this with (an over-approximation of) this with one ray added.
void	addRay(Manager man, Generator0[] ar)	Replaces this with (an over-approximation of) this with some rays added.
Abstract0	addRayCopy(Manager man, Generator0 r)	Returns a new abstract element that contains (an over-approximation of) this with one ray added.
Abstract0	addRayCopy(Manager man, Generator0[] 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, int[] dim, Linexpr0[] ar, Abstract0 dest)	Replaces this with (an over-approximation of) this after assigning ar[i] to dim[i], in parallel.
void	assign(Manager man, int[] dim, Texpr0Intern[] ar, Abstract0 dest)	Replaces this with (an over-approximation of) this after assigning ar[i] to dim[i], in parallel.
void	assign(Manager man, int dim, Linexpr0 expr, Abstract0 dest)	Replaces this with (an over-approximation of) this after assigning expr to dim.
void	assign(Manager man, int dim, Texpr0Intern expr, Abstract0 dest)	Replaces this with (an over-approximation of) this after assigning expr to dim.
Abstract0	assignCopy(Manager man, int[] dim, Linexpr0[] ar, Abstract0 dest)	Returns a new element containing (an over-approximation of) this after assigning ar[i] to dim[i], in parallel.
Abstract0	assignCopy(Manager man, int[] dim, Texpr0Intern[] ar, Abstract0 dest)	Returns a new element containing (an over-approximation of) this after assigning ar[i] to dim[i], in parallel.
Abstract0	assignCopy(Manager man, int dim, Linexpr0 expr, Abstract0 dest)	Returns a new element containing (an over-approximation of) this after assigning expr to dim.
Abstract0	assignCopy(Manager man, int dim, Texpr0Intern expr, Abstract0 dest)	Returns a new element containing (an over-approximation of) this after assigning expr to dim.
void	canonicalize(Manager man)	Tries to put the element in canonical form.
void	closure(Manager man)	Replaces this with (an over-approximation of) its topological closure.
Abstract0	closureCopy(Manager man)	Returns a new element which is (an over-approximation of) the topological closure of this.
static Abstract0	deserialize(Manager man, byte[] buf)	Restores an abstract element from a byte array.
void	expand(Manager man, int dim, int n)	Duplicates n times the variable dim in this.
Abstract0	expandCopy(Manager man, int dim, int n)	Returns a new element where variable dim is duplicated n times.
void	fold(Manager man, int[] dim)	Folds all dimensions from dim[] into dimension dim[0].
Abstract0	foldCopy(Manager man, int[] dim)	Returns a new element where all dimensions from dim[] are folded into dimension dim[0].
void	forget(Manager man, int[] dim, boolean project)	Replaces this with (an over-approximation of) this after forgetting the value of the variables in dim.
void	forget(Manager man, int dim, boolean project)	Replaces this with (an over-approximation of) this after forgetting the value of the variable dim.
Abstract0	forgetCopy(Manager man, int[] dim, boolean project)	Returns a new element containing (an over-approximation of) this after forgetting the value of the variables in dim.
Abstract0	forgetCopy(Manager man, int dim, boolean project)	Returns a new element containing (an over-approximation of) this after forgetting the value of the variable dim.
Interval	getBound(Manager man, int dim)	Returns (an over-approximation of) the set of values the variable dim can take on this.
Interval	getBound(Manager man, Linexpr0 e)	Returns (an over-approximation of) the set of values e can take on this.
Interval	getBound(Manager man, Texpr0Intern e)	Returns (an over-approximation of) the set of values e can take on this.
Manager	getCreationManager()	Returns the Manager which was used to create the the abstract element.
Dimension	getDimension(Manager man)	Returns the number of integer-valued and real-valued dimensions in the 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, int dim)	Whether the dimension dim is definitely unbounded in this (true) or may be bounded (false).
boolean	isEqual(Manager man, Abstract0 x)	Whether this is definitely equal to x (true) or maybe not equal (false).
boolean	isIncluded(Manager man, Abstract0 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, Abstract0 op)	Replaces this with (an over-approximation of) the set-union of this and op.
static Abstract0	join(Manager man, Abstract0[] ar)	Returns a new abstract element that contains (an over-approximation of) the set-union of the elements in ar.
Abstract0	joinCopy(Manager man, Abstract0 op)	Returns a new abstract element that contains (an over-approximation of) the set-union of this and op.
void	meet(Manager man, Abstract0 op)	Replaces this with (an over-approximation of) the set-intersection of this and op.
static Abstract0	meet(Manager man, Abstract0[] ar)	Returns a new abstract element that contains (an over-approximation of) the set-intersection of the elements in ar.
void	meet(Manager man, Lincons0 c)	Replaces this with (an over-approximation of) the set-intersection of this with the constraint c.
void	meet(Manager man, Lincons0[] ar)	Replaces this with (an over-approximation of) the set-intersection of this with the constraints in ar.
void	meet(Manager man, Tcons0 c)	Replaces this with (an over-approximation of) the set-intersection of this with the constraint c.
void	meet(Manager man, Tcons0[] ar)	Replaces this with (an over-approximation of) the set-intersection of this with the constraints in ar.
Abstract0	meetCopy(Manager man, Abstract0 op)	Returns a new abstract element that contains (an over-approximation of) the set-intersection of this and op.
Abstract0	meetCopy(Manager man, Lincons0 c)	Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraint cr.
Abstract0	meetCopy(Manager man, Lincons0[] ar)	Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraints in ar.
Abstract0	meetCopy(Manager man, Tcons0 c)	Returns a new abstract element that contains (an over-approximation of) the set-intersection of this with the constraint in c.
Abstract0	meetCopy(Manager man, Tcons0[] 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	permuteDimensions(Manager man, Dimperm p)	Permutes some dimensions to this.
Abstract0	permuteDimensionsCopy(Manager man, Dimperm p)	Returns a new element containing this after permuting some dimensions.
void	removeDimensions(Manager man, Dimchange d)	Removes some dimensions from this.
Abstract0	removeDimensionsCopy(Manager man, Dimchange d)	Returns a new element containing this after removing some dimensions.
boolean	satisfy(Manager man, int dim, Interval i)	Whether the projection of this on dimension dim is definitely included in the interval i (true) or maybe is not included (false).
boolean	satisfy(Manager man, Lincons0 c)	Whether this definitely satisfies the constraint c (true) or maybe does not satisfy it (false).
boolean	satisfy(Manager man, Tcons0 c)	Whether this definitely satisfies the constraint c (true) or maybe does not satisfy it (false).
byte[]	serialize(Manager man)	Converts the abstract element to a byte array.
void	substitute(Manager man, int[] dim, Linexpr0[] ar, Abstract0 dest)	Replaces this with (an over-approximation of) this after substituting dim[i] with ar[i], in parallel.
void	substitute(Manager man, int[] dim, Texpr0Intern[] ar, Abstract0 dest)	Replaces this with (an over-approximation of) this after substituting dim[i] with ar[i], in parallel.
void	substitute(Manager man, int dim, Linexpr0 expr, Abstract0 dest)	Replaces this with (an over-approximation of) this after substituting dim with expr.
void	substitute(Manager man, int dim, Texpr0Intern expr, Abstract0 dest)	Replaces this with (an over-approximation of) this after substituting dim with expr.
Abstract0	substituteCopy(Manager man, int[] dim, Linexpr0[] ar, Abstract0 dest)	Returns a new element containing (an over-approximation of) this after substituting dim[i] with ar[i], in parallel.
Abstract0	substituteCopy(Manager man, int[] dim, Texpr0Intern[] ar, Abstract0 dest)	Returns a new element containing (an over-approximation of) this after substituting dim[i] with ar[i], in parallel.
Abstract0	substituteCopy(Manager man, int dim, Linexpr0 expr, Abstract0 dest)	Returns a new element containing (an over-approximation of) this after substituting dim with expr.
Abstract0	substituteCopy(Manager man, int dim, Texpr0Intern expr, Abstract0 dest)	Returns a new element containing (an over-approximation of) this after substituting dim with expr.
Interval[]	toBox(Manager man)	Returns a box describing (an over-approximation of) this.
Generator0[]	toGenerator(Manager man)	Returns a set of generators describing (an over-approximation of) this.
Lincons0[]	toLincons(Manager man)	Returns a set of linear constraints describing (an over-approximation of) this.
String	toString()	Returns a String representation of the element as a list of constraints.
String	toString(Manager man)	Returns a String representation of the element as a list of constraints.
String	toString(Manager man, Var[] names)	Returns a String representation of the element as a list of constraints.
String	toString(Manager man, String[] names)
Tcons0[]	toTcons(Manager man)	Returns a set of constraints describing (an over-approximation of) this.
Abstract0	widening(Manager man, Abstract0 op)	Returns a new element equal to this widened with op.
Abstract0	wideningThreshold(Manager man, Abstract0 op, Lincons0[] 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

Constructor Details

Abstract0

public Abstract0(Manager man,
 Abstract0 a)
          throws ApronException

Creates a copy of the abstract element a.

Throws:

ApronException

Abstract0

public Abstract0(Manager man,
 int intdim,
 int realdim)
          throws ApronException

Creates a new universal abstract element.

The element has intdim integer-valued dimensions, followed by realdim real-valued dimensions.

It is initialized to the full space: Z^intdim * R^realdim.

Throws:

ApronException

Abstract0

public Abstract0(Manager man,
 int intdim,
 int realdim,
 boolean empty)
          throws ApronException

Creates a new universal or empty abstract element.

The element has intdim integer-valued dimensions, followed by realdim real-valued dimensions.

It is initialized to the full space if empty is false, and to the empty space if empty is true.

Throws:

ApronException

Abstract0

public Abstract0(Manager man,
 int intdim,
 int realdim,
 Interval[] box)
          throws ApronException

Creates a new abstract element from a box.

The element has intdim integer-valued dimensions, followed by realdim real-valued dimensions.

box must contain intdim+realdim intervals.

The constructed element is the Cartesian product of the intervals.

Throws:

ApronException

Abstract0

public Abstract0(Manager man,
 int intdim,
 int realdim,
 Lincons0[] c)
          throws ApronException

Creates a new abstract element from a set of constraints.

The element has intdim integer-valued dimensions, followed by realdim real-valued dimensions.

The constructed element is (an over-approximation of) the set of points satisfying all constraints.

Throws:

ApronException

Abstract0

public Abstract0(Manager man,
 int intdim,
 int realdim,
 Tcons0[] c)
          throws ApronException

Creates a new abstract element from a set of constraints.

The element has intdim integer-valued dimensions, followed by realdim real-valued dimensions.

The constructed element is (an over-approximation of) the set of points satisfying all constraints.

Throws:

ApronException

Method Details

getSize

public int getSize(Manager man)
            throws ApronException

Returns the size in memory of the abstract element.

The memory unit is domain-specific.

Throws:

ApronException

hashCode

public int hashCode(Manager man)
             throws ApronException

Returns a hash of the element value.

Throws:

ApronException

getDimension

public Dimension getDimension(Manager man)
                       throws ApronException

Returns the number of integer-valued and real-valued dimensions in the element.

Throws:

ApronException

getCreationManager

public Manager getCreationManager()

Returns the Manager which was used to create the the abstract element.

toString

public 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 Object

toString

public String toString(Manager man)

Returns a String representation of the element as a list of constraints.

Dimension i is denoted as xi.

toString

public String toString(Manager man,
 String[] names)

toString

public String toString(Manager man,
 Var[] names)

Returns a String representation of the element as a list of constraints.

Dimension i as denoted by names[i].

getBound

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

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

Throws:

ApronException

getBound

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

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

Throws:

ApronException

getBound

public Interval getBound(Manager man,
 int dim)
                  throws ApronException

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

Throws:

ApronException

toLincons

public Lincons0[] toLincons(Manager man)
                     throws ApronException

Returns a set of linear constraints describing (an over-approximation of) this.

Throws:

ApronException

toTcons

public Tcons0[] 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.

Throws:

ApronException

toGenerator

public Generator0[] 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 not 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,
 Abstract0 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.

Throws:

ApronException

isEqual

public boolean isEqual(Manager man,
 Abstract0 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.

Throws:

ApronException

satisfy

public boolean satisfy(Manager man,
 Lincons0 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.

Throws:

ApronException

satisfy

public boolean satisfy(Manager man,
 Tcons0 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.

Throws:

ApronException

satisfy

public boolean satisfy(Manager man,
 int dim,
 Interval i)
                throws ApronException

Whether the projection of this on dimension dim 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,
 int dim)
                                 throws ApronException

Whether the dimension dim 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 Abstract0 meetCopy(Manager man,
 Abstract0 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.

Throws:

ApronException

meet

public static Abstract0 meet(Manager man,
 Abstract0[] 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.

Throws:

ApronException

meet

public void meet(Manager man,
 Abstract0 op)
          throws ApronException

Replaces this with (an over-approximation of) the set-intersection of this and op.

op is not modified.

Throws:

ApronException

joinCopy

public Abstract0 joinCopy(Manager man,
 Abstract0 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.

Throws:

ApronException

join

public static Abstract0 join(Manager man,
 Abstract0[] 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.

Throws:

ApronException

join

public void join(Manager man,
 Abstract0 op)
          throws ApronException

Replaces this with (an over-approximation of) the set-union of this and op.

op is not modified.

Throws:

ApronException

meetCopy

public Abstract0 meetCopy(Manager man,
 Lincons0[] 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.

Throws:

ApronException

meetCopy

public Abstract0 meetCopy(Manager man,
 Tcons0[] 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.

Throws:

ApronException

meet

public void meet(Manager man,
 Lincons0[] ar)
          throws ApronException

Replaces this with (an over-approximation of) the set-intersection of this with the constraints in ar.

Throws:

ApronException

meet

public void meet(Manager man,
 Tcons0[] ar)
          throws ApronException

Replaces this with (an over-approximation of) the set-intersection of this with the constraints in ar.

Throws:

ApronException

meetCopy

public Abstract0 meetCopy(Manager man,
 Lincons0 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.

Throws:

ApronException

meetCopy

public Abstract0 meetCopy(Manager man,
 Tcons0 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.

Throws:

ApronException

meet

public void meet(Manager man,
 Lincons0 c)
          throws ApronException

Replaces this with (an over-approximation of) the set-intersection of this with the constraint c.

Throws:

ApronException

meet

public void meet(Manager man,
 Tcons0 c)
          throws ApronException

Replaces this with (an over-approximation of) the set-intersection of this with the constraint c.

Throws:

ApronException

addRayCopy

public Abstract0 addRayCopy(Manager man,
 Generator0[] 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.

Throws:

ApronException

addRay

public void addRay(Manager man,
 Generator0[] ar)
            throws ApronException

Replaces this with (an over-approximation of) this with some rays added.

ar can only contain ray and lines, not vertices.

Throws:

ApronException

addRayCopy

public Abstract0 addRayCopy(Manager man,
 Generator0 r)
                     throws ApronException

Returns a new abstract element that contains (an over-approximation of) this with one ray added.

this is not changed.

Throws:

ApronException

addRay

public void addRay(Manager man,
 Generator0 r)
            throws ApronException

Replaces this with (an over-approximation of) this with one ray added.

Throws:

ApronException

assign

public void assign(Manager man,
 int[] dim,
 Linexpr0[] ar,
 Abstract0 dest)
            throws ApronException

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

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

Throws:

ApronException

assignCopy

public Abstract0 assignCopy(Manager man,
 int[] dim,
 Linexpr0[] ar,
 Abstract0 dest)
                     throws ApronException

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

this is not modified.

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

Throws:

ApronException

assign

public void assign(Manager man,
 int[] dim,
 Texpr0Intern[] ar,
 Abstract0 dest)
            throws ApronException

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

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

Throws:

ApronException

assignCopy

public Abstract0 assignCopy(Manager man,
 int[] dim,
 Texpr0Intern[] ar,
 Abstract0 dest)
                     throws ApronException

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

this is not modified.

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

Throws:

ApronException

substitute

public void substitute(Manager man,
 int[] dim,
 Linexpr0[] ar,
 Abstract0 dest)
                throws ApronException

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

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

Throws:

ApronException

substituteCopy

public Abstract0 substituteCopy(Manager man,
 int[] dim,
 Linexpr0[] ar,
 Abstract0 dest)
                         throws ApronException

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

this is not modified.

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

Throws:

ApronException

substitute

public void substitute(Manager man,
 int[] dim,
 Texpr0Intern[] ar,
 Abstract0 dest)
                throws ApronException

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

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

Throws:

ApronException

substituteCopy

public Abstract0 substituteCopy(Manager man,
 int[] dim,
 Texpr0Intern[] ar,
 Abstract0 dest)
                         throws ApronException

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

this is not modified.

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

Throws:

ApronException

assign

public void assign(Manager man,
 int dim,
 Linexpr0 expr,
 Abstract0 dest)
            throws ApronException

Replaces this with (an over-approximation of) this after assigning expr to dim. The result is intersected with dest, if dest is not null.

Throws:

ApronException

assignCopy

public Abstract0 assignCopy(Manager man,
 int dim,
 Linexpr0 expr,
 Abstract0 dest)
                     throws ApronException

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

this is not modified.

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

Throws:

ApronException

assign

public void assign(Manager man,
 int dim,
 Texpr0Intern expr,
 Abstract0 dest)
            throws ApronException

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

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

Throws:

ApronException

assignCopy

public Abstract0 assignCopy(Manager man,
 int dim,
 Texpr0Intern expr,
 Abstract0 dest)
                     throws ApronException

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

this is not modified.

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

Throws:

ApronException

substitute

public void substitute(Manager man,
 int dim,
 Linexpr0 expr,
 Abstract0 dest)
                throws ApronException

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

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

Throws:

ApronException

substituteCopy

public Abstract0 substituteCopy(Manager man,
 int dim,
 Linexpr0 expr,
 Abstract0 dest)
                         throws ApronException

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

this is not modified.

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

Throws:

ApronException

substitute

public void substitute(Manager man,
 int dim,
 Texpr0Intern expr,
 Abstract0 dest)
                throws ApronException

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

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

Throws:

ApronException

substituteCopy

public Abstract0 substituteCopy(Manager man,
 int dim,
 Texpr0Intern expr,
 Abstract0 dest)
                         throws ApronException

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

this is not modified.

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

Throws:

ApronException

forgetCopy

public Abstract0 forgetCopy(Manager man,
 int[] dim,
 boolean project)
                     throws ApronException

Returns a new element containing (an over-approximation of) this after forgetting the value of the variables in dim.

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,
 int[] dim,
 boolean project)
            throws ApronException

Replaces this with (an over-approximation of) this after forgetting the value of the variables in dim.

If project is true, the variables are set to 0. Otherwise, they are set to [-oo,+oo].

Throws:

ApronException

forgetCopy

public Abstract0 forgetCopy(Manager man,
 int dim,
 boolean project)
                     throws ApronException

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

this is not modified.

Throws:

ApronException

forget

public void forget(Manager man,
 int dim,
 boolean project)
            throws ApronException

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

Throws:

ApronException

addDimensionsCopy

public Abstract0 addDimensionsCopy(Manager man,
 Dimchange d,
 boolean project)
                            throws ApronException

Returns a new element containing this after adding some dimensions.

this is not modified.

If project is true, the added variables are set to 0. Otherwise, they are set to set to [-oo,+oo].

Throws:

ApronException

addDimensions

public void addDimensions(Manager man,
 Dimchange d,
 boolean project)
                   throws ApronException

Adds some dimensions to this.

If project is true, the added variables are set to 0. Otherwise, they are set to set to [-oo,+oo].

Throws:

ApronException

removeDimensionsCopy

public Abstract0 removeDimensionsCopy(Manager man,
 Dimchange d)
                               throws ApronException

Returns a new element containing this after removing some dimensions.

this is not modified.

Throws:

ApronException

removeDimensions

public void removeDimensions(Manager man,
 Dimchange d)
                      throws ApronException

Removes some dimensions from this.

Throws:

ApronException

permuteDimensionsCopy

public Abstract0 permuteDimensionsCopy(Manager man,
 Dimperm p)
                                throws ApronException

Returns a new element containing this after permuting some dimensions.

this is not modified.

Throws:

ApronException

permuteDimensions

public void permuteDimensions(Manager man,
 Dimperm p)
                       throws ApronException

Permutes some dimensions to this.

Throws:

ApronException

expandCopy

public Abstract0 expandCopy(Manager man,
 int dim,
 int n)
                     throws ApronException

Returns a new element where variable dim is duplicated n times.

If the duplicated dimension is integer (resp. float), copies are appended after all integer (resp. float) variables.

this is not modified.

Throws:

ApronException

expand

public void expand(Manager man,
 int dim,
 int n)
            throws ApronException

Duplicates n times the variable dim in this.

If the duplicated dimension is integer (resp. float), copies are appended after all integer (resp. float) variables.

Throws:

ApronException

foldCopy

public Abstract0 foldCopy(Manager man,
 int[] dim)
                   throws ApronException

Returns a new element where all dimensions from dim[] are folded into dimension dim[0].

The array must be sorted and contain either only integer-valued or real-valued variables.

this is not modified.

Throws:

ApronException

fold

public void fold(Manager man,
 int[] dim)
          throws ApronException

Folds all dimensions from dim[] into dimension dim[0].

The array must be sorted and contain either only integer-valued or real-valued variables.

The array must be sorted.

Throws:

ApronException

widening

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

Returns a new element equal to this widened with op.

this and op are not modified.

Throws:

ApronException

wideningThreshold

public Abstract0 wideningThreshold(Manager man,
 Abstract0 op,
 Lincons0[] c)
                            throws ApronException

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

this and op are not modified.

Throws:

ApronException

closureCopy

public Abstract0 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.

Throws:

ApronException

deserialize

public static Abstract0 deserialize(Manager man,
 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.

Throws:

ApronException