net.sourceforge.czt.animation.eval.flatpred

Class FlatForall

java.lang.Object

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

net.sourceforge.czt.animation.eval.flatpred.FlatForall

Direct Known Subclasses:

FlatExists

public class FlatForall
extends FlatPred

Field Summary

Fields

Modifier and Type	Field and Description
protected FlatPredList	body_
protected Bounds	bodyBounds_
protected Mode	bodyMode_ The mode returned by body_
protected static Logger	LOG
protected Bounds	schBounds_
protected Mode	schMode_ The mode returned by schText_
protected FlatPredList	schText_

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

args_, evalMode_, freeVars_, INDENT, printer_, solutionsReturned_

Constructor Summary

Constructors

Constructor and Description
FlatForall(FlatPredList sch, FlatPredList body)

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.
ModeList	chooseMode(Envir env) Chooses the mode in which the predicate can be evaluated.
Set<net.sourceforge.czt.z.ast.ZName>	freeVars() Returns the free variables that appear in the predicate.
boolean	inferBounds(Bounds bnds) This lets bound information flow into the quantifier, but not out.
boolean	nextEvaluation() Generates the next solution that satisfies this predicate.
void	setMode(Mode mode) Set the mode that will be used to evaluate this predicate.
String	toString() A default implementation of toString.

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

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

Methods inherited from class java.lang.Object

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

Field Detail

LOG

protected static final Logger LOG

schText_

protected FlatPredList schText_

body_

protected FlatPredList body_

schBounds_

protected Bounds schBounds_

bodyBounds_

protected Bounds bodyBounds_

schMode_

protected Mode schMode_

The mode returned by schText_

bodyMode_

protected Mode bodyMode_

The mode returned by body_

Constructor Detail

FlatForall

public FlatForall(FlatPredList sch,
                  FlatPredList body)

Method Detail

inferBounds

public boolean inferBounds(Bounds bnds)

This lets bound information flow into the quantifier, but not out. This is because the constraints on the bound variables can be arbitrarily tight, and these should not be allowed to influence the bounds of any free variables. Similarly, bounds information can flow from the bound variables into the body of the quantifier, but not in the reverse direction.

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.

chooseMode

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

freeVars

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

Description copied from class: FlatPred

Returns the free variables that appear in the predicate. The default implementation returns all the variables in args.

Overrides:

freeVars in class FlatPred

setMode

public void setMode(Mode mode)

Description copied from class: FlatPred

Set the mode that will be used to evaluate this predicate.

Overrides:

setMode in class FlatPred

Parameters:

mode - Must be one of the modes returned previously by chooseMode.

nextEvaluation

public boolean nextEvaluation()

Description copied from class: FlatPred

Generates the next solution that satisfies this predicate. This must only be called after startEvaluation().

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