net.sourceforge.czt.animation.eval.flatpred

Class FlatPredList

java.lang.Object

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

net.sourceforge.czt.animation.eval.flatpred.FlatPredList

Direct Known Subclasses:

FlatNot

public class FlatPredList
extends FlatPred

Manages a list of FlatPred predicates. Provides methods for adding declarations and predicates to the list, doing mode analysis of the list, and evaluating the list (giving a series of updated environments).

Here is a typical use of FlatPredList:

  // Stage 1: Setup.
  predlist = new FlatPredList(zlive_instance);
  // now add decls, predicates, expressions etc.
  ZName resultName = predlist.addExpr(expr);
  Envir env0 = new Envir(); // empty environment

  // Stage 2: Optimisation.
  predlist.inferBounds(new Bounds()); // does some static analysis
  // Ask the FlatPredList to optimise itself for efficient
  // evaluation, given the inputs in env0 (none in this case).
  Mode m = predlist.chooseMode(env0);
  if (m == null)
    throw new EvalException("Cannot find mode to evaluate " + expr);
  predlist.setMode(m);

  // Stage 3: Evaluation.
  predlist.startEvaluation();
  while (predlist.nextEvaluation())
      // lookup the result and do something with it.
      System.out.println(predlist.getEnvir().lookup(resultName));
  

Field Summary

Fields

Modifier and Type	Field and Description
protected Set<net.sourceforge.czt.z.ast.ZName>	boundVars_ Records the bound variables in this list (Ignoring the tmp vars produced by Flatten).
static boolean	optimize_ Evaluation is left-to-right if this is false, or smallest-mode-first if it is true.
protected List<FlatPred>	predlist_ This stores the list of FlatPreds used in the current evaluation.

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

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

Constructor Summary

Constructors

Constructor and Description
FlatPredList(ZLive newZLive) Creates an empty FlatPred list.

Method Summary

Modifier and Type	Method and Description
void	add(FlatPred flat) Add one FlatPred to the FlatPred list.
void	addDecl(net.sourceforge.czt.z.ast.Decl decl) Adds one declaration to the FlatPred list predList_.
void	addExistsPred(net.sourceforge.czt.z.ast.Pred pred) This is similar to addPred, but it flattens out any existential quantifiers within pred.
void	addExistsSchText(net.sourceforge.czt.z.ast.ZSchText stext) Same as addSchText, but uses addExistsPred to add the predicate part.
net.sourceforge.czt.z.ast.ZName	addExpr(net.sourceforge.czt.z.ast.Expr expr) Adds one expression to the FlatPred list.
void	addPred(net.sourceforge.czt.z.ast.Pred pred) Adds one predicate to the FlatPred list.
void	addSchText(net.sourceforge.czt.z.ast.ZSchText stext) Adds a whole schema text to the FlatPred list.
Set<net.sourceforge.czt.z.ast.ZName>	boundVars() Returns the bound variables of this FlatPredList, ignoring any temporary variables.
ModeList	chooseMode(Envir env0) Optimises the list and chooses a mode.
Set<net.sourceforge.czt.z.ast.ZName>	freeVars() Returns the free variables of all the FlatPreds.
List<net.sourceforge.czt.z.ast.ZName>	getArgs() Get the list of variables that this predicate directly depends upon.
protected net.sourceforge.czt.z.util.Factory	getFactory()
Envir	getOutputEnvir() The output environment of this FlatPred list.
boolean	inferBounds(Bounds bnds) Infer bounds for any integer variables.
boolean	inferBoundsFixPoint(Bounds bnds) Equivalent to inferBoundsFixPoint(bnds, 5).
boolean	inferBoundsFixPoint(Bounds bnds, int maxPasses) Infer bounds for any integer variables.
Iterator<FlatPred>	iterator() An iterator over the FlatPreds in this list.
void	makeBound(net.sourceforge.czt.z.ast.ZName name) Clients can use this to mark some names as being local to (bound by) this FlatPred list.
void	makeFree(net.sourceforge.czt.z.ast.ZName name) Clients can use this to say that the given variable is actually a free variable of this FlatPredList.
boolean	nextEvaluation() Returns the next solution from this list of FlatPreds.
void	setMode(Mode mode) Set the mode that will be used to evaluate this list.
int	size() Returns the number of FlatPreds in this list.
void	startEvaluation() Starts a fresh evaluation.
String	toString() This prints each FlatPred on a separate line.

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

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

Methods inherited from class java.lang.Object

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

Field Detail

optimize_

public static final boolean optimize_

Evaluation is left-to-right if this is false, or smallest-mode-first if it is true.

See Also:

Constant Field Values

predlist_

protected List<FlatPred> predlist_

This stores the list of FlatPreds used in the current evaluation.

boundVars_

protected Set<net.sourceforge.czt.z.ast.ZName> boundVars_

Records the bound variables in this list (Ignoring the tmp vars produced by Flatten). It is set up as Declarations are added.

Constructor Detail

FlatPredList

public FlatPredList(ZLive newZLive)

Creates an empty FlatPred list.

Method Detail

size

public int size()

Returns the number of FlatPreds in this list.

iterator

public Iterator<FlatPred> iterator()

An iterator over the FlatPreds in this list. This should be used as a read-only iterator.

Returns:

the iterator

boundVars

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

Returns the bound variables of this FlatPredList, ignoring any temporary variables.

freeVars

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

Returns the free variables of all the FlatPreds. This must not be called until after all addPred/Expr calls have been done. The first time it is called, it calculates the free variables as the union of the free variables of all the FlatPreds in the list, minus the boundvars. It also sets the args list to contain these same variables.

Overrides:

freeVars in class FlatPred

getArgs

public List<net.sourceforge.czt.z.ast.ZName> getArgs()

Description copied from class: FlatPred

Get the list of variables that this predicate directly depends upon. This usually contains the same variables as the freeVars set, but this list may contain duplicates. This should be treated as a read-only list.

Overrides:

getArgs in class FlatPred

add

public void add(FlatPred flat)

Add one FlatPred to the FlatPred list. This is a low-level method, and addDecl or addPred should usually be used in preference to this method. This method should be called before chooseMode or freeVars are called.

Parameters:

flat - the FlatPred to add.

makeBound

public void makeBound(net.sourceforge.czt.z.ast.ZName name)

Clients can use this to mark some names as being local to (bound by) this FlatPred list.

Parameters:

name -

makeFree

public void makeFree(net.sourceforge.czt.z.ast.ZName name)

Clients can use this to say that the given variable is actually a free variable of this FlatPredList. If it was in the set of bound variables, this also removes it from that set.

addSchText

public void addSchText(net.sourceforge.czt.z.ast.ZSchText stext)

Adds a whole schema text to the FlatPred list. This method should be called before chooseMode or freeVars are called.

Parameters:

stext -

addExistsSchText

public void addExistsSchText(net.sourceforge.czt.z.ast.ZSchText stext)

Same as addSchText, but uses addExistsPred to add the predicate part. This should only be used within existential quantifier situations, such as set comprehensions and exists quantifiers.

Parameters:

stext -

addDecl

public void addDecl(net.sourceforge.czt.z.ast.Decl decl)

Adds one declaration to the FlatPred list predList_. A VarDecl, x,y:T, is converted into x \in T \land y \in T. (More precisely, into: tmp=T; x \in tmp; y \in tmp). A ConstDecl, x==E, is converted into x \in {E}. A schema inclusion [D|P], is added recursively using addSchText. TODO: it would be nice to use addExistsSchText sometimes, when we are adding declarations within an exists etc. This method should be called before chooseMode or freeVars are called.

Parameters:

decl - May declare several variables.

addPred

public void addPred(net.sourceforge.czt.z.ast.Pred pred)

Adds one predicate to the FlatPred list. This method should be called before chooseMode or freeVars are called.

Parameters:

pred - The Pred to flatten and add.

addExistsPred

public void addExistsPred(net.sourceforge.czt.z.ast.Pred pred)

This is similar to addPred, but it flattens out any existential quantifiers within pred. That is, it merges the declarations from within the exists with those outside it. So you should only call this method from a context where this is sound, such as within an exists or within a set comprehension whose result expression is filled in. It also flattens nested exists and exists within one branch of a conjunction.

Note that this method would not be sound for a predicate like

   (exists x:0..20 @ x < 10) and (exists x:0..20 @ x > 10),
  

because the flattened result would unify the two x's, and the resulting predicate would be false, rather than true. However, such inputs should never occur, since CZT ASTs always use a different ID for each variable with a different scope, even for sibling scopes.

Parameters:

pred -

addExpr

public net.sourceforge.czt.z.ast.ZName addExpr(net.sourceforge.czt.z.ast.Expr expr)

Adds one expression to the FlatPred list. This method should be called before chooseMode or freeVars are called. Returns the 'result' name that will be bound to the result of the expression after evaluation. That is, after chooseMode, startEvaluation and nextEvaluation have been called, then getOutputEnvir().lookup(result) can be called to get the value of the evaluated expression.

The result name is not necessarily free or bound -- this depends upon how the name was declared. So it is the caller's responsibility to make it free if this is desired.

Parameters:

expr - The Expr to flatten and add.

Returns:

The result name.

inferBounds

public boolean inferBounds(Bounds bnds)

Infer bounds for any integer variables. See FlatPred.inferBounds(Bounds bnds);

This does upto inferPasses_ passes over all the predicates in the list (it stops if a fixed point is found earlier).

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

inferBoundsFixPoint

public boolean inferBoundsFixPoint(Bounds bnds)

Equivalent to inferBoundsFixPoint(bnds, 5). That is, this does a default (maximum) number of static inference iterations.

inferBoundsFixPoint

public boolean inferBoundsFixPoint(Bounds bnds,
                                   int maxPasses)

Infer bounds for any integer variables. See FlatPred.inferBounds(Bounds bnds);

This does upto maxPasses passes over all the predicates in the list. TODO: stop earlier than maxPasses if a fixed point is reached. That is, if the bounds are not getting any tighter after a pass.

Parameters:

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

maxPasses - The maximum number of iterations done. Must be > 0.

Returns:

true iff a fix point has been reached.

chooseMode

public ModeList chooseMode(Envir env0)

Optimises the list and chooses a mode. Note that inferBounds must be done before this, since it may narrow the search space of chooseMode.

Specified by:

chooseMode in class FlatPred

Returns:

The Mode object, with statistics and an updated environment.

setMode

public void setMode(Mode mode)

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

Overrides:

setMode in class FlatPred

Parameters:

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

startEvaluation

public void startEvaluation()

Starts a fresh evaluation.

Overrides:

startEvaluation in class FlatPred

getOutputEnvir

public Envir getOutputEnvir()

The output environment of this FlatPred list. This is only valid after startEvaluation.

nextEvaluation

public boolean nextEvaluation()

Returns the next solution from this list of FlatPreds. This implements chronological backtracking, like Prolog. If it returns true, the output environment, available via getOutputEnvir(), will contain updated values for any bound variables defined within this FlatPredList. Note that the empty list of FlatPreds will return true once.

Specified by:

nextEvaluation in class FlatPred

Returns:

true iff a new solution was found.

getFactory

protected net.sourceforge.czt.z.util.Factory getFactory()

toString

public String toString()

This prints each FlatPred on a separate line. If a FlatPred within the list is displayed on multiple lines, it indents those lines, to preserve the nested indentation structure.

Overrides:

toString in class FlatPred