blog
Class ImplicitSetSpec

java.lang.Object
  blog.ArgSpec
      blog.ImplicitSetSpec

public class ImplicitSetSpec
extends ArgSpec

Represents an argument - set with implicit specification of its elements. An ImplicitSetSpec consists of a type type, a variable set_elt, and a formula cond. It evaluates to the set of objects o of type type such that cond is satisfied when set_elt is bound to o.

Field Summary

Fields inherited from class blog.ArgSpec

location

Constructor Summary

ImplicitSetSpec(LogicalVar var, Formula cond)

ImplicitSetSpec(java.lang.String set_elt, Type type, 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 a compiled version of this set specification.
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 implicit set specifications are equal if they have the same type, generic element variable, and condition.
java.lang.Object	evaluate(EvalContext context) Returns the value of this argument specification in the given context.
Formula	getCond()
java.util.Set	getFreeVars() Returns the logical variables that occur free in this expression.
LogicalVar	getGenericSetElt()
protected CompiledSetSpec	getSatisfierSpec() Returns a compiled version of the set represented by this ImplicitSetSpec.
java.util.Set	getSatisfyingSet(PartialWorld w) Returns the set of objects o of type type such that when var is bound to o, the formula cond is satisfied in w.
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.
Type	getType()
int	hashCode()
java.lang.String	toString() Returns a string of the form {Type var : cond} where Type is this implicit set specification's type, var is the generic set element variable, and cond is the membership 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

ImplicitSetSpec

public ImplicitSetSpec(java.lang.String set_elt,
                       Type type,
                       Formula cond)

Parameters:

set_elt - name of variable representing an element of the set

type - type of objects in the set. May be null, but then the main program should exit before the compilation phase.

cond - formula that objects in the set must satisfy

ImplicitSetSpec

public ImplicitSetSpec(LogicalVar var,
                       Formula cond)

Method Detail

getGenericSetElt

public LogicalVar getGenericSetElt()

getType

public Type getType()

getCond

public Formula getCond()

getSatisfyingSet

public java.util.Set getSatisfyingSet(PartialWorld w)

Returns the set of objects o of type type such that when var is bound to o, the formula cond is satisfied in w. This method yields a fatal error if w is not complete enough to define this set.

evaluate

public java.lang.Object evaluate(EvalContext context)

Description copied from class: ArgSpec

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

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 a compiled version of this set specification.

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 implicit set specifications are equal if they have the same type, generic element variable, and condition. Two implicit set specifications that differ only in the choice of generic element variable are equivalent, but we do not consider them equal, just as we do not consider two universally quantified formulas equal if they differ in the quantified variable.

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 {Type var : cond} where Type is this implicit set specification's type, var is the generic set element variable, and cond is the membership condition.

Overrides:

toString in class java.lang.Object

getSatisfierSpec

protected CompiledSetSpec getSatisfierSpec()

Returns a compiled version of the set represented by this ImplicitSetSpec.