net.sourceforge.czt.animation.eval.flatpred

Class FlatRangeSet

java.lang.Object

net.sourceforge.czt.animation.eval.flatpred.FlatPred

net.sourceforge.czt.animation.eval.flatpred.FlatRangeSet

public class FlatRangeSet
extends FlatPred

Author:

Mark Utting FlatRangeSet(a,b,s) implements a..b = s. However, the a and b bounds are both optional, which allows these objects to represent the set of naturals and the set of integers etc.

Field Summary

Fields

Modifier and Type	Field and Description
protected Bounds	bounds_ The most recent variable bounds information.
protected net.sourceforge.czt.z.util.Factory	factory_

Fields inherited from class net.sourceforge.czt.animation.eval.flatpred.FlatPred

args_, evalMode_, freeVars_, INDENT, LOG, printer_, solutionsReturned_

Constructor Summary

Constructors

Constructor and Description
FlatRangeSet(net.sourceforge.czt.z.ast.ZName lowerBound, net.sourceforge.czt.z.ast.ZName upperBound, net.sourceforge.czt.z.ast.ZName set) Creates a FlatRangeSet object, with optional bounds.

Method Summary

Modifier and Type	Method and Description
<R> R	accept(net.sourceforge.czt.util.Visitor<R> visitor) Calls visitor.visitPred (preferably) or visitor.visitTerm.
Mode	chooseMode(Envir env) Chooses the mode in which the predicate can be evaluated.
static int	getAverageClosedRange()
BigInteger	getBound(int which)
boolean	inferBounds(Bounds bnds) Saves the Bounds information for later use.
boolean	nextEvaluation() Does the actual evaluation
static void	setAverageClosedRange(int size) Sets the average expected size of a closed range a..b.
static void	setAverageClosedRange(String str) A convenience method for setting the average expected size of a closed range a..b.
String	toString() A default implementation of toString.

Methods inherited from class net.sourceforge.czt.animation.eval.flatpred.FlatPred

freeVars, getArgs, getEnvir, getLastArg, getMode, indent, modeAllDefined, modeCollection, modeFunction, modeOneOutput, printArg, printBinOp, printLastArg, printName, printQuant, setMode, startEvaluation

Methods inherited from class java.lang.Object

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

Field Detail

factory_

protected net.sourceforge.czt.z.util.Factory factory_

bounds_

protected Bounds bounds_

The most recent variable bounds information.

Constructor Detail

FlatRangeSet

public FlatRangeSet(net.sourceforge.czt.z.ast.ZName lowerBound,
                    net.sourceforge.czt.z.ast.ZName upperBound,
                    net.sourceforge.czt.z.ast.ZName set)

Creates a FlatRangeSet object, with optional bounds.

Parameters:

lowerBound - a lower bound expression, or null for no bound.

upperBound - an upper bound expression, or null for no bound.

set - the name of the resulting set of integers.

Method Detail

getAverageClosedRange

public static int getAverageClosedRange()

Returns:

the average expected size of a closed range a..b

setAverageClosedRange

public static void setAverageClosedRange(int size)

Sets the average expected size of a closed range a..b. This is used to guess the best evaluation order during mode analysis.

Parameters:

averageClosedRange - should be 2..1000000000.

setAverageClosedRange

public static void setAverageClosedRange(String str)

A convenience method for setting the average expected size of a closed range a..b.

Parameters:

str - An integer in string form.

inferBounds

public boolean inferBounds(Bounds bnds)

Saves the Bounds information for later use. Note that we cannot deduce any constraints on a or b from a..b. Not even a<=b, because the b

Overrides:

inferBounds in class FlatPred

Parameters:

bnds - The database of lower and upper bounds for integer variables.

Returns:

true iff the bnds database has been changed.

The default implementation infers nothing and returns false.

getBound

public BigInteger getBound(int which)

chooseMode

public Mode chooseMode(Envir env)

Chooses the mode in which the predicate can be evaluated.

Specified by:

chooseMode in class FlatPred

Returns:

The Mode object, with statistics and an updated environment.

nextEvaluation

public boolean nextEvaluation()

Does the actual evaluation

Specified by:

nextEvaluation in class FlatPred

Returns:

true iff another solution has been found.

toString

public String toString()

Description copied from class: FlatPred

A default implementation of toString. This returns "FlatXXX(args[0], args[1], ...)".

Overrides:

toString in class FlatPred

accept

public <R> R accept(net.sourceforge.czt.util.Visitor<R> visitor)

Description copied from class: FlatPred

Calls visitor.visitPred (preferably) or visitor.visitTerm. Subclasses that correspond to particular kinds of Pred should override this to call more specific visitXXX methods (and should call super to handle the remaining cases).

Overrides:

accept in class FlatPred