Package apron

Class Abstract1

java.lang.Object

apron.Abstract1

All Implemented Interfaces:

Cloneable

public class Abstract1
extends Object
implements 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	Description
protected Abstract0	abs	Level 0 abstract element.
protected Environment	env	Environment.

Constructor Summary

Constructors

Constructor	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, Var[] vars, Interval[] box)	Creates a new abstract element from a box.
Abstract1(Manager man, Environment e, String[] vars, Interval[] 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

Modifier and Type	Method	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, 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.
void	assign(Manager man, String[] var, Linexpr1[] ar, Abstract1 dest)
void	assign(Manager man, String[] var, Texpr1Intern[] ar, Abstract1 dest)
void	assign(Manager man, String var, Linexpr1 expr, Abstract1 dest)
void	assign(Manager man, 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.
Abstract1	assignCopy(Manager man, String[] var, Texpr1Intern[] ar, Abstract1 dest)
Abstract1	assignCopy(Manager man, String var, Linexpr1 expr, Abstract1 dest)
Abstract1	assignCopy(Manager man, String var, Texpr1Intern expr, Abstract1 dest)
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, Var org, Var[] dst)	Duplicates the variable org as dst[0] ... dst[dst.length-1].
void	expand(Manager man, String org, 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].
Abstract1	expandCopy(Manager man, String org, String[] dst)
void	fold(Manager man, Var[] var)	Folds all variables var[i] into variable var[0].
void	fold(Manager man, 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].
Abstract1	foldCopy(Manager man, String[] var)
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.
void	forget(Manager man, String[] var, boolean project)
void	forget(Manager man, 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.
Abstract1	forgetCopy(Manager man, String[] var, boolean project)
Abstract1	forgetCopy(Manager man, String var, boolean project)
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, 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.
Interval	getBound(Manager man, String var)
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, Var var)	Whether the variable var is definitely unbounded in this (true) or may be bounded (false).
boolean	isDimensionUnconstrained(Manager man, String var)
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, Var[] org, Var[] dst)	Renames variable org[i] as dst[i].
void	rename(Manager man, String[] org, String[] dst)
Abstract1	renameCopy(Manager man, Var[] org, Var[] dst)	Returns a copy of this with variable org[i] renamed as dst[i].
Abstract1	renameCopy(Manager man, String[] org, String[] dst)
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, 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).
boolean	satisfy(Manager man, String var, Interval i)
byte[]	serialize(Manager man)	Converts the abstract element to a byte array.
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.
void	substitute(Manager man, String[] var, Linexpr1[] ar, Abstract1 dest)
void	substitute(Manager man, String[] var, Texpr1Intern[] ar, Abstract1 dest)
void	substitute(Manager man, String var, Linexpr1 expr, Abstract1 dest)
void	substitute(Manager man, 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.
Abstract1	substituteCopy(Manager man, String[] var, Texpr1Intern[] ar, Abstract1 dest)
Abstract1	substituteCopy(Manager man, String var, Linexpr1 expr, Abstract1 dest)
Abstract1	substituteCopy(Manager man, String var, Texpr1Intern expr, Abstract1 dest)
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.
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.
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 Details

abs

protected Abstract0 abs

Level 0 abstract element.

env

protected Environment env

Environment.

Constructor Details

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,
 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 Details

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

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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 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,
 String[] org,
 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,
 String[] org,
 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,
 String org,
 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,
 String org,
 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,
 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,
 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