net.sourceforge.czt.animation.eval.flatpred

Class Bounds

java.lang.Object

net.sourceforge.czt.animation.eval.flatpred.Bounds

public class Bounds
extends Object

Maintains lower and upper bounds for integer variables. This is a helper class for the range-inference pass of ZLive, which deduces lower and upper bounds for integer variables, based on the semantics of each FlatPred operator. It also stores information about variables that will bind to sets, since this can help when deducing bounds of the elements of those sets. Finally, it records some alias names for structures such as tuples and bindings. For example, from an equality like t=(a,c,d), we record the facts: t.1=a, t.2=c, t.3=d.

It records information about whether new bounds information has recently (since the last call to startAnalysis) been added. The implementation may even record which variables have recently changed, so that clients can decide whether or not it is worth re-analyzing a given FlatPred. TODO: the record of which variables have changed is not currently used. Before it is used, it needs to be updated so that it changes when aliases are added.

The constructor and the startAnalysis method both take a 'parent' object as a parameter, so that these bounds objects can be built into a tree, where each node of the tree stores the bounds information for a local scope such as within a quantifier, or within a disjunction. The startAnalysis method copies bounds information from the parent into the child, but additional bounds information added to the child does not flow back to the parent.

This class also counts the number of bounds deductions that it has detected (see the getDeductions method). Child Bounds objects typically add their deduction count to their parent, so that the count at the root of the Bounds tree gives the total number of deductions that have been made in the current pass. The general idea is to continue making passes until no further deductions are made in a pass, which shows that a fix-point has been reached.

Author:

marku

Field Summary

Fields

Modifier and Type	Field and Description
protected int	deductions_ The number of bounds deductions in this scope (and child scopes).
protected Bounds	parent_

Constructor Summary

Constructors

Constructor and Description
Bounds(Bounds parent) Create a fresh Bounds object with no bounds values.

Method Summary

Modifier and Type	Method and Description
void	addAlias(net.sourceforge.czt.z.ast.ZName var1, net.sourceforge.czt.z.ast.ZName var2) Add another alias for var.
void	addConst(net.sourceforge.czt.z.ast.ZName name, net.sourceforge.czt.z.ast.Expr value) Add name=value to the bounds information.
void	addDeductions(int count) Increment the deductions counter by count.
boolean	addLower(net.sourceforge.czt.z.ast.ZName var0, BigInteger lower) Adds another lower bound for var.
void	addStructureArg(net.sourceforge.czt.z.ast.ZName var, Object argPos, net.sourceforge.czt.z.ast.ZName argName) Record the fact that var is a structure, and the name of one of its arguments (subcomponents).
boolean	addUpper(net.sourceforge.czt.z.ast.ZName var0, BigInteger upper) Adds another upper bound for var.
boolean	anyBoundsChanged(Collection<net.sourceforge.czt.z.ast.ZName> vars) True iff the bounds of any name in vars have changed.
boolean	boundsChanged() True iff some tighter bounds information has been deduced (or inherited from a parent) in this inference pass.
boolean	boundsChanged(net.sourceforge.czt.z.ast.ZName key) True iff the bounds of key have changed in this pass.
void	endAnalysis() This should be called at the end of each bounds inference pass.
Set<net.sourceforge.czt.z.ast.ZName>	getAliases(net.sourceforge.czt.z.ast.ZName var) Returns a list of all known aliases for var.
Set<net.sourceforge.czt.z.ast.ZName>	getAliasKeys() Returns the keys that have alias information.
protected net.sourceforge.czt.z.ast.ZName	getBestAlias(net.sourceforge.czt.z.ast.ZName var) Returns the ZName that has the bounds information attached to it.
int	getDeductions() The number of bounds deductions in this scope (and child scopes).
EvalSet	getEvalSet(net.sourceforge.czt.z.ast.ZName var0) Get the EvalSet for var, if known.
Set<net.sourceforge.czt.z.ast.ZName>	getEvalSetKeys() Returns the keys that have set information.
BigInteger	getLower(net.sourceforge.czt.z.ast.ZName var) Get the optional lower bound for var.
Set<net.sourceforge.czt.z.ast.ZName>	getLowerKeys() Returns the keys that have lower bounds.
RangeSet	getRange(net.sourceforge.czt.z.ast.ZName var0) Returns the lower and/or upper bounds of an integer variable (if known), or null otherwise.
Map<Object,net.sourceforge.czt.z.ast.ZName>	getStructure(net.sourceforge.czt.z.ast.ZName var) Returns information about the argument names of a structure such as a tuple or binding.
Set<net.sourceforge.czt.z.ast.ZName>	getStructureKeys() Returns the names that are known to be structures (tuples/bindings).
BigInteger	getUpper(net.sourceforge.czt.z.ast.ZName var) Get the optional upper bound for var.
Set<net.sourceforge.czt.z.ast.ZName>	getUpperKeys() Returns the keys that have upper bounds.
boolean	includesZero(net.sourceforge.czt.z.ast.ZName name) True iff the set of possible values for name includes 0.
boolean	isAliased(net.sourceforge.czt.z.ast.ZName var, net.sourceforge.czt.z.ast.ZName other) True iff var and other are known to be aliased.
static boolean	isBetterLowerBound(BigInteger lo1, BigInteger lo2) True iff lo1 is a better (tighter) lower bound than lo2.
static boolean	isBetterUpperBound(BigInteger lo1, BigInteger lo2) True iff lo1 is a better (tighter) upper bound than lo2.
static <V> String	printMap(Map<net.sourceforge.czt.z.ast.ZName,V> map) A alternative version of Map<ZName,???>.toString() that prints the names in a non-unicode way.
boolean	setEvalSet(net.sourceforge.czt.z.ast.ZName var0, EvalSet set) Set the EvalSet for var.
void	startAnalysis() Resets the deductions counter and marks all vars as not-yet-changed.
void	startAnalysis(Bounds parent) This is similar to startAnalysis with no parameters, but it also updates the local bounds information from the parent.
String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

parent_

protected Bounds parent_

deductions_

protected int deductions_

The number of bounds deductions in this scope (and child scopes).

Constructor Detail

Bounds

public Bounds(Bounds parent)

Create a fresh Bounds object with no bounds values.

Parameters:

parent - Optional parent to inherit bounds from.

Method Detail

startAnalysis

public void startAnalysis(Bounds parent)

This is similar to startAnalysis with no parameters, but it also updates the local bounds information from the parent. More precisely, it compares the new parent bounds with the current bounds of this object, adds any new information and remembers which variables have changed. Then it resets the deduction count to zero. The same parent must be passed as a parameter each time this method is called, and it must be the same as the parent passed to the constructor.

This method should be used in preference to startAnalysis() whenever bounds inference starts on a Bounds object that is within a nested scope, such as a quantifiers or disjunction. The idea is that bounds information from the parent should flow down into the child, but not in the reverse direction (though a few inferBounds methods like in FlatOr may choose to propagate some common bounds information back up to the parent).

Parameters:

parent - Bounds information from an outer scope.

startAnalysis

public void startAnalysis()

Resets the deductions counter and marks all vars as not-yet-changed. This is usually done at the beginning of each bounds inference pass.

endAnalysis

public void endAnalysis()

This should be called at the end of each bounds inference pass. It propagates the deduction count up to the parent (if any). Note that startAnalysis/endAnalysis calls should always occur in pairs and should be properly nested. That is, the startAnalysis/endAnalysis calls of any child Bounds objects should all occur in between the startAnalysis and endAnalysis calls of their parent.

getDeductions

public int getDeductions()

The number of bounds deductions in this scope (and child scopes).

addDeductions

public void addDeductions(int count)

Increment the deductions counter by count. This is typically used to tell a parent how many deductions a child Bounds object has just made.

boundsChanged

public boolean boundsChanged()

True iff some tighter bounds information has been deduced (or inherited from a parent) in this inference pass.

Returns:

true if new/tighter bounds are available.

boundsChanged

public boolean boundsChanged(net.sourceforge.czt.z.ast.ZName key)

True iff the bounds of key have changed in this pass.

anyBoundsChanged

public boolean anyBoundsChanged(Collection<net.sourceforge.czt.z.ast.ZName> vars)

True iff the bounds of any name in vars have changed.

getLowerKeys

public Set<net.sourceforge.czt.z.ast.ZName> getLowerKeys()

Returns the keys that have lower bounds.

getUpperKeys

public Set<net.sourceforge.czt.z.ast.ZName> getUpperKeys()

Returns the keys that have upper bounds.

getEvalSetKeys

public Set<net.sourceforge.czt.z.ast.ZName> getEvalSetKeys()

Returns the keys that have set information.

toString

public String toString()

Overrides:

toString in class Object

printMap

public static <V> String printMap(Map<net.sourceforge.czt.z.ast.ZName,V> map)

A alternative version of Map<ZName,???>.toString() that prints the names in a non-unicode way.

addConst

public void addConst(net.sourceforge.czt.z.ast.ZName name,
                     net.sourceforge.czt.z.ast.Expr value)

Add name=value to the bounds information.

getEvalSet

public EvalSet getEvalSet(net.sourceforge.czt.z.ast.ZName var0)

Get the EvalSet for var, if known.

Parameters:

var - The name of an integer variable.

Returns:

The EvalSet (null means unknown).

setEvalSet

public boolean setEvalSet(net.sourceforge.czt.z.ast.ZName var0,
                          EvalSet set)

Set the EvalSet for var. This increments the deduction counter if there was previously no EvalSet information for key, or if any of the attributes of the EvalSet have decreased.

Parameters:

var - The name of an integer variable.

set - A non-null EvalSet (usually a FuzzySet).

isBetterLowerBound

public static boolean isBetterLowerBound(BigInteger lo1,
                                         BigInteger lo2)

True iff lo1 is a better (tighter) lower bound than lo2.

Parameters:

lo1 - Optional new lower bound

lo2 - Optional old lower bound

Returns:

true if lo1 > lo2 or if lo1 is non-null and lo2 is null.

isBetterUpperBound

public static boolean isBetterUpperBound(BigInteger lo1,
                                         BigInteger lo2)

True iff lo1 is a better (tighter) upper bound than lo2.

Parameters:

lo1 - Optional new upper bound

lo2 - Optional old upper bound

Returns:

true if lo1 < lo2 or if lo1 is non-null and lo2 is null.

getLower

public BigInteger getLower(net.sourceforge.czt.z.ast.ZName var)

Get the optional lower bound for var.

Parameters:

var - The name of an integer variable.

Returns:

The lower bound (null means -infinity).

getUpper

public BigInteger getUpper(net.sourceforge.czt.z.ast.ZName var)

Get the optional upper bound for var.

Parameters:

var - The name of an integer variable.

Returns:

The upper bound (null means -infinity).

getRange

public RangeSet getRange(net.sourceforge.czt.z.ast.ZName var0)

Returns the lower and/or upper bounds of an integer variable (if known), or null otherwise.

addLower

public boolean addLower(net.sourceforge.czt.z.ast.ZName var0,
                        BigInteger lower)

Adds another lower bound for var. The new lower bound is ignored if it is weaker than any existing lower bound, otherwise it supercedes the old bound (and the deduction count is incremented). That is, new bounds are intersected with the old bounds.

Parameters:

var - The name of an integer variable.

lower - The lower bound (must be non-null).

Returns:

true iff the bound has changed (ie. is tighter).

addUpper

public boolean addUpper(net.sourceforge.czt.z.ast.ZName var0,
                        BigInteger upper)

Adds another upper bound for var. The new upper bound is ignored if it is weaker than any existing upper bound, otherwise it supercedes the old bound (and the deduction count is incremented). That is, new bounds are intersected with the old bounds.

Parameters:

var - The name of an integer variable.

upper - The upper bound (must be non-null).

Returns:

true iff the bound has changed (ie. is tighter).

getAliasKeys

public Set<net.sourceforge.czt.z.ast.ZName> getAliasKeys()

Returns the keys that have alias information.

getAliases

public Set<net.sourceforge.czt.z.ast.ZName> getAliases(net.sourceforge.czt.z.ast.ZName var)

Returns a list of all known aliases for var. The resulting list will contain ZName, TupleExpr and BindExpr objects. For example: getAliases(x) == [ x, y, z ] means that x = y = z.

Parameters:

var -

Returns:

A list of aliases, which should be treated as read-only.

getBestAlias

protected net.sourceforge.czt.z.ast.ZName getBestAlias(net.sourceforge.czt.z.ast.ZName var)

Returns the ZName that has the bounds information attached to it. If var is aliased with other objects, then the bounds information is always attached to the first object in the LinkedHashSet, which will always be a ZName.

isAliased

public boolean isAliased(net.sourceforge.czt.z.ast.ZName var,
                         net.sourceforge.czt.z.ast.ZName other)

True iff var and other are known to be aliased.

addAlias

public void addAlias(net.sourceforge.czt.z.ast.ZName var1,
                     net.sourceforge.czt.z.ast.ZName var2)

Add another alias for var. The alias object must be a ZName, TupleExpr (which contains only ZName objects), or BindExpr object (which contains only ZName objects after each ==).

Parameters:

var1 -

var2 -

getStructureKeys

public Set<net.sourceforge.czt.z.ast.ZName> getStructureKeys()

Returns the names that are known to be structures (tuples/bindings).

getStructure

public Map<Object,net.sourceforge.czt.z.ast.ZName> getStructure(net.sourceforge.czt.z.ast.ZName var)

Returns information about the argument names of a structure such as a tuple or binding. This will return null if var is not known to be a structure.

Parameters:

var - The name of the whole structure

Returns:

A map from argument positions to the names at those positions

addStructureArg

public void addStructureArg(net.sourceforge.czt.z.ast.ZName var,
                            Object argPos,
                            net.sourceforge.czt.z.ast.ZName argName)

Record the fact that var is a structure, and the name of one of its arguments (subcomponents). See the docs for the structure_ field for examples.

Parameters:

var - The name of the whole structure.

argPos - An Integer for tuples, or a ZName for bindings.

argName - The name of the argument.

includesZero

public boolean includesZero(net.sourceforge.czt.z.ast.ZName name)

True iff the set of possible values for name includes 0. More precisely, it is false if the lower bound of name is greater than zero, or the upper bound is less than zero.

Parameters:

name - The name of an integer variable

Returns: