blog
Class TupleSetSpec

java.lang.Object
  blog.ArgSpec
      blog.TupleSetSpec

public class TupleSetSpec
extends ArgSpec

Represents an argument - set consisting of implicitly specified tuples. The components of each tuple are assumed to be Terms. The general form of the i-th component of a tuple is specified by the object in the i-th position of terms. The tuple is evaluated for each assignment of values to vars that makes the formula cond true.

Field Summary

Fields inherited from class blog.ArgSpec

location

Constructor Summary

TupleSetSpec(java.util.List termList, java.util.List varTypeList, java.util.List varList, Formula cond)

TupleSetSpec(Term[] terms, LogicalVar[] vars, Formula cond)

Method Summary

boolean	checkTypesAndScope(Model model, java.util.Map scope) Returns true if, within the given scope, all the variables used in this ArgSpec are in scope and all type constraints are satisfied.
int	compile(java.util.LinkedHashSet callStack) Initializes ObjGenGraph objects for the possible bindings to the variables in this TupleSetSpec.
boolean	containsRandomSymbol() Returns true if this ArgSpec contains any random function symbols or any type symbols (any type might have a number statement, and thus could be random).
boolean	equals(java.lang.Object o) Two tuple set specifications are equivalent if they have the same tuple of terms, variable type list, variable list, and condition.
java.lang.Object	evaluate(EvalContext context) Returns the value of this argument specification in the given context, or null if the partial world in this context is not complete enough to evaluate this ArgSpec.
Formula	getCond()
java.util.Set	getFreeVars() Returns the logical variables that occur free in this expression.
Term[]	getGenericTuple()
LogicalVar[]	getParams()
java.util.Collection	getSubExprs() Returns the proper sub-expressions of this ArgSpec.
ArgSpec	getSubstResult(Substitution subst, java.util.Set<LogicalVar> boundVars) Returns the result of applying the substitution subst to this expression, excluding the logical variables in boundVars.
int	hashCode()
java.lang.String	toString() Returns a string of the form {t1, ..., tK for T1 v1, ..., TN vN : cond} where t1, ..., tK are the terms, T1, ..., TN are the variable types, v1, ..., vN are the variables, and cond is the condition.

Methods inherited from class blog.ArgSpec

evaluate, evaluate, getLocation, getSubstResult, getValueIfNonRandom, getVariable, isDetermined, isNumeric, setLocation

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

TupleSetSpec

public TupleSetSpec(java.util.List termList,
                    java.util.List varTypeList,
                    java.util.List varList,
                    Formula cond)

Parameters:

termList - List of Term objects denoting elements of tuples

varTypeList - List of Type objects representing types of the variables. Some of these types may be null, but then the main program should exit before the compilation phase.

varList - List of String objects serving as names of variables

cond - Formula that each tuple of objects bound to the variables must satisfy

TupleSetSpec

public TupleSetSpec(Term[] terms,
                    LogicalVar[] vars,
                    Formula cond)

Method Detail

getGenericTuple

public Term[] getGenericTuple()

getParams

public LogicalVar[] getParams()

getCond

public Formula getCond()

evaluate

public java.lang.Object evaluate(EvalContext context)

Returns the value of this argument specification in the given context, or null if the partial world in this context is not complete enough to evaluate this ArgSpec.

This method first enumerates the assignments that satisfy the first disjunct, then those that satisfy the second but not the first, etc. If the VarValuesIterator for the first disjunct returns infinitely many values, this process will never invoke the VarValuesIterators for the remaining disjuncts. But there's no such thing as short-circuit evaluation for TupleSetSpecs anyway: we always return the whole set.

Specified by:

evaluate in class ArgSpec

containsRandomSymbol

public boolean containsRandomSymbol()

Description copied from class: ArgSpec

Returns true if this ArgSpec contains any random function symbols or any type symbols (any type might have a number statement, and thus could be random).

Specified by:

containsRandomSymbol in class ArgSpec

checkTypesAndScope

public boolean checkTypesAndScope(Model model,
                                  java.util.Map scope)

Description copied from class: ArgSpec

Returns true if, within the given scope, all the variables used in this ArgSpec are in scope and all type constraints are satisfied. If there is a type or scope error, prints an appropriate message to standard error and returns false.

Specified by:

checkTypesAndScope in class ArgSpec

scope - a Map from variable names (Strings) to LogicalVar objects

compile

public int compile(java.util.LinkedHashSet callStack)

Initializes ObjGenGraph objects for the possible bindings to the variables in this TupleSetSpec.

Overrides:

compile in class ArgSpec

Parameters:

callStack - Set of objects whose compile methods are parents of this method invocation. Ordered by invocation order. Used to detect cycles.

getSubExprs

public java.util.Collection getSubExprs()

Description copied from class: ArgSpec

Returns the proper sub-expressions of this ArgSpec. This is an empty collection if this ArgSpec has no proper sub-expressions.

This default implementation returns an empty collection.

Overrides:

getSubExprs in class ArgSpec

Returns:

unmodifiable Collection of ArgSpec

getFreeVars

public java.util.Set getFreeVars()

Description copied from class: ArgSpec

Returns the logical variables that occur free in this expression. If this expression was loaded from a file, then this method should be called only after checkTypesAndScope, which converts SymbolTerms to LogicalVars.

The default implementation returns the union of the sets of free variables in this expression's sub-expressions.

Overrides:

getFreeVars in class ArgSpec

Returns:

unmodifiable Set of LogicalVar

getSubstResult

public ArgSpec getSubstResult(Substitution subst,
                              java.util.Set<LogicalVar> boundVars)

Description copied from class: ArgSpec

Returns the result of applying the substitution subst to this expression, excluding the logical variables in boundVars. This method is used for recursive calls. The set boundVars should contain those variables that are bound in the syntax tree between this sub-expression and the top-level expression to which the substitution is being applied.

Specified by:

getSubstResult in class ArgSpec

equals

public boolean equals(java.lang.Object o)

Two tuple set specifications are equivalent if they have the same tuple of terms, variable type list, variable list, and condition. There are various ways to construct a tuple set specification that is equivalent to a given specification (rename the variables, reorder the variables and types, etc.), but we do not consider those variations equal to the given specification.

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toString

public java.lang.String toString()

Returns a string of the form

{t1, ..., tK for T1 v1, ..., TN vN : cond}

where t1, ..., tK are the terms, T1, ..., TN are the variable types, v1, ..., vN are the variables, and cond is the condition.

Overrides:

toString in class java.lang.Object