blog
Class NonRandomFunction

java.lang.Object
  blog.Function
      blog.NonRandomFunction

public class NonRandomFunction
extends Function

Represents the symbol for a non-random function, whose value for the given tuple of arguments is constant over worlds. Non-random functions do not have dependency statement like the random functions do. Instead, the function symbol's interpretation is given by an object that implements the FunctionInterp interface.

See Also:

Function

Nested Class Summary

Nested classes/interfaces inherited from class blog.Function

Function.Sig

Constructor Summary

NonRandomFunction(java.lang.String fname, java.util.List arg_types, Type ret_type)

NonRandomFunction(java.lang.String fname, java.util.List arg_types, Type ret_type, java.lang.Class interpClass, java.util.List interpParams)

NonRandomFunction(java.lang.String fname, java.util.List arg_types, Type ret_type, FunctionInterp interp)

NonRandomFunction(java.lang.String fname, Type ret_type)
Creates a non-random constant with the given name and type.

Method Summary

boolean	checkTypesAndScope(Model model) Returns true if the dependency statement or interpretation statement for this function (if any) satisfies type and scope constraints.
int	compile(java.util.LinkedHashSet callStack) Constructs this function's interpretation, if it hasn't been constructed already.
java.lang.Class	getInterpClass() Returns the FunctionInterp implementation used for this function's interpretation, or null if this function's interpretation class has not been set.
FunctionInterp	getInterpretation() Returns the interpretation of this function, or null if this function's interpretation has not been set or constructed yet.
java.util.Set	getInverseArgs(java.lang.Object[] args, int argIndex, java.lang.Object value) Returns the set of values for argument argIndex that, in combination with the given values for the other arguments, yield the given function value.
java.util.Set	getInverseTuples(java.lang.Object value) Returns the set of argument tuples that yield the given value, or null if this set cannot be computed easily.
java.lang.Object	getValue()
java.lang.Object	getValue(java.lang.Object[] args)
java.lang.Object	getValueInContext(java.lang.Object[] args, EvalContext context, boolean stable) Returns the value of this function applied to the given tuple of arguments in the given context.
java.lang.Object	getValueSingleArg(java.lang.Object arg)
void	print(java.io.PrintStream s) Prints a description of this NonRandomFunction to the given stream.
void	setConstantInterp(java.lang.Object value) Sets the interpretation of this function to be a ConstantInterp with the given value.
void	setInterpretation(java.lang.Class interpClass, java.util.List interpParams) Sets the interpretation of this function to be an instance of the given class, constructed with the given parameters.
void	setInterpretation(FunctionInterp interp) Sets the interpretation of this function.

Methods inherited from class blog.Function

appliesTo, domainIterator, domainIterator, getArgTypes, getCreationIndex, getDefaultValue, getName, getRetType, getSig, getValue, getValue, getValue, getValueSingleArg, isTimeIndexed, overlapsWith, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

NonRandomFunction

public NonRandomFunction(java.lang.String fname,
                         Type ret_type)

Creates a non-random constant with the given name and type.

NonRandomFunction

public NonRandomFunction(java.lang.String fname,
                         java.util.List arg_types,
                         Type ret_type)

NonRandomFunction

public NonRandomFunction(java.lang.String fname,
                         java.util.List arg_types,
                         Type ret_type,
                         java.lang.Class interpClass,
                         java.util.List interpParams)

Parameters:

fname - the name of this non-random function

arg_types - List of Type objects for function arguments

ret_type - return type of this function

interpClass - implementation of FunctionInterp used for the function's interpretation

interpParams - List of ArgSpec objects whose denotations are passed to the interpetation's constructor. These must be non-random and must contain no free variables.

NonRandomFunction

public NonRandomFunction(java.lang.String fname,
                         java.util.List arg_types,
                         Type ret_type,
                         FunctionInterp interp)

Method Detail

setInterpretation

public void setInterpretation(FunctionInterp interp)

Sets the interpretation of this function.

setInterpretation

public void setInterpretation(java.lang.Class interpClass,
                              java.util.List interpParams)

Sets the interpretation of this function to be an instance of the given class, constructed with the given parameters.

setConstantInterp

public void setConstantInterp(java.lang.Object value)

Sets the interpretation of this function to be a ConstantInterp with the given value.

getInterpretation

public FunctionInterp getInterpretation()

Returns the interpretation of this function, or null if this function's interpretation has not been set or constructed yet.

getInterpClass

public java.lang.Class getInterpClass()

Returns the FunctionInterp implementation used for this function's interpretation, or null if this function's interpretation class has not been set.

getValue

public java.lang.Object getValue()

getValue

public java.lang.Object getValue(java.lang.Object[] args)

getValueSingleArg

public java.lang.Object getValueSingleArg(java.lang.Object arg)

getInverseTuples

public java.util.Set getInverseTuples(java.lang.Object value)

Returns the set of argument tuples that yield the given value, or null if this set cannot be computed easily.

Returns:

unmodifiable Set of List

getInverseArgs

public java.util.Set getInverseArgs(java.lang.Object[] args,
                                    int argIndex,
                                    java.lang.Object value)

Returns the set of values for argument argIndex that, in combination with the given values for the other arguments, yield the given function value. If this set cannot be computed straightforwardly, returns null.

Parameters:

args - tuple of arguments; the entry at argIndex is ignored

getValueInContext

public java.lang.Object getValueInContext(java.lang.Object[] args,
                                          EvalContext context,
                                          boolean stable)

Description copied from class: Function

Returns the value of this function applied to the given tuple of arguments in the given context. If the partial world in the given context is not complete enough to determine the function value, this method returns null.

Specified by:

getValueInContext in class Function

stable - if true, the caller guarantees that the args array will not be modified

checkTypesAndScope

public boolean checkTypesAndScope(Model model)

Description copied from class: Function

Returns true if the dependency statement or interpretation statement for this function (if any) satisfies type and scope constraints. If there is a type or scope error, prints a message to standard error and returns false.

This default implementation just returns true.

Overrides:

checkTypesAndScope in class Function

compile

public int compile(java.util.LinkedHashSet callStack)

Constructs this function's interpretation, if it hasn't been constructed already. If this function is already in the call stack, prints an error message saying that there is a cyclic dependency among the non-random functions.

Overrides:

compile in class Function

Parameters:

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

print

public void print(java.io.PrintStream s)

Prints a description of this NonRandomFunction to the given stream.