Evaluator.java

package edu.udel.cis.vsl.tass.semantics.impl;

import java.util.HashMap;
import java.util.Map;
import java.util.Scanner;

import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicException;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicFactoryIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.CellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.LiteralCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.ModelCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.SharedCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.ArrayValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.FunctionValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.PrimitiveValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.RecordValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.ReferenceValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.ValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ArrayElementReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ArrayValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.RecordElementReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.RecordValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.VariableReferenceValueIF;
import edu.udel.cis.vsl.tass.model.IF.FunctionIF;
import edu.udel.cis.vsl.tass.model.IF.ModelFactoryIF;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ArrayLiteralTypeIF;
import edu.udel.cis.vsl.tass.model.IF.expression.BinaryExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.BoundExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.DereferenceExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.EvaluatedFunctionExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.IfThenElseExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.LHSExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.LiteralExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.LiteralTypeIF;
import edu.udel.cis.vsl.tass.model.IF.expression.NotEmptyExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.NotFullExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ObjectLiteralExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ProcessReferenceExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.RecordLiteralTypeIF;
import edu.udel.cis.vsl.tass.model.IF.expression.RecordNavigationExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.SizeOfExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.UnaryExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.VariableExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF.ExpressionKind;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.model.IF.scope.LocalScopeIF;
import edu.udel.cis.vsl.tass.model.IF.scope.ScopeIF.ScopeKind;
import edu.udel.cis.vsl.tass.model.IF.type.ArrayTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.FunctionTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.PointerTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.RecordTypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF.TypeKind;
import edu.udel.cis.vsl.tass.model.IF.variable.BoundVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.FormalVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.LocalVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.ProcessVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.SharedVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.VariableIF;
import edu.udel.cis.vsl.tass.number.IF.IntegerNumberIF;
import edu.udel.cis.vsl.tass.number.IF.NumberFactoryIF;
import edu.udel.cis.vsl.tass.number.IF.NumberIF;
import edu.udel.cis.vsl.tass.semantics.IF.EnvironmentIF;
import edu.udel.cis.vsl.tass.semantics.IF.EvaluatorIF;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionException;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem;
import edu.udel.cis.vsl.tass.semantics.IF.LogIF;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.Certainty;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.ErrorKind;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicConstantIF;
import edu.udel.cis.vsl.tass.util.Sourceable;
import edu.udel.cis.vsl.tass.util.TASSInternalException;
import edu.udel.cis.vsl.tass.util.TernaryResult.ResultType;

/**
 * An Evaluator is used to evaluate expressions in a MiniMP model.
 */
public class Evaluator implements EvaluatorIF {

	private ModelFactoryIF modelFactory;

	private DynamicFactoryIF dynamicFactory;

	private LogIF log;

	private NumberFactoryIF numberFactory;

	private int bufferSize;

	private ValueIF zero, zeroReal, one, trueValue;

	private ValueTypeIF integerType, realType;

	/** If true, will not allow reads of output variables */
	private boolean checkAccess = true;

	public Evaluator(DynamicFactoryIF dynamicFactory, int bufferSize, LogIF log) {
		assert dynamicFactory != null;
		assert log != null;
		this.dynamicFactory = dynamicFactory;
		this.modelFactory = dynamicFactory.modelFactory();
		this.numberFactory = dynamicFactory.numberFactory();
		this.bufferSize = bufferSize;
		this.log = log;
		trueValue = dynamicFactory.trueValue();
		integerType = dynamicFactory.integerType();
		realType = dynamicFactory.realType();
		zero = dynamicFactory.zero();
		one = dynamicFactory.symbolicValue(numberFactory.oneInteger());
		zeroReal = dynamicFactory.symbolicValue(numberFactory.zeroRational());
	}

	public RunConfiguration configuration() {
		return dynamicFactory.configuration();
	}

	public ModelFactoryIF modelFactory() {
		return modelFactory;
	}

	public DynamicFactoryIF dynamicFactory() {
		return dynamicFactory;
	}

	public LogIF log() {
		return log;
	}

	public ModelCellIF cell(EnvironmentIF environment, VariableIF variable) {
		switch (variable.scope().kind()) {
		case MODEL:
			return dynamicFactory.sharedCell((SharedVariableIF) variable);
		case PROCESS:
			return dynamicFactory.processCell((ProcessVariableIF) variable);
		case LOCAL:
			LocalVariableIF localVariable = (LocalVariableIF) variable;
			LocalScopeIF variableScope = localVariable.scope();
			FunctionIF variableFunction = variableScope.function();
			ProcessIF process = variableFunction.process();
			LocationIF location = environment.location(process);
			LocalScopeIF locationScope = location.scope();
			int stackSize = environment.stackSize(process);

			assert modelFactory.isDescendantOf(locationScope, variableScope);
			return dynamicFactory.localCell(localVariable, stackSize - 1);
		default:
			throw new IllegalArgumentException(
					"TASS Internal error: No dynamic variable for variable "
							+ variable);
		}
	}

	/**
	 * Returns a reference to a variable v.
	 * 
	 * For a variable of array type, this returns a reference to an array.
	 * 
	 * @throws ExecutionException
	 * */
	private ReferenceValueIF variableReferenceValue(EnvironmentIF environment,
			VariableExpressionIF expression) throws ExecutionException {
		VariableIF variable = expression.variable();
		TypeIF type = variable.type();
		ModelCellIF dynamicVariable = cell(environment, variable);

		if (type.kind() == TypeKind.ARRAY) {
			if (variable instanceof FormalVariableIF) {
				return (ReferenceValueIF) environment.valueOf(dynamicVariable);
			} else {
				ValueIF arrayValue = environment.valueOf(dynamicVariable);
				ArrayValueTypeIF arrayDynamicType = (ArrayValueTypeIF) arrayValue
						.valueType();
				ReferenceValueTypeIF referenceDynamicType = dynamicFactory
						.referenceValueType(arrayDynamicType);

				// assert referenceDynamicType.isCommitted();
				return dynamicFactory.referenceValue(dynamicVariable,
						referenceDynamicType);
			}
		} else {
			return dynamicFactory.referenceValue(dynamicVariable,
					dynamicFactory.referenceValueType(variableValueType(
							environment, variable)));
		}
	}

	private ReferenceValueIF objectLiteralReferenceValue(
			EnvironmentIF environment, ObjectLiteralExpressionIF expression)
			throws ExecutionException {
		CellIF cell = dynamicFactory.literalCell(expression);
		ValueTypeIF incompleteValueType = valueType(environment, expression
				.type());
		ValueTypeIF completeValueType = completeValueType(environment,
				incompleteValueType, expression.literalType());
		ReferenceValueTypeIF referenceType = dynamicFactory
				.referenceValueType(completeValueType);

		return dynamicFactory.referenceValue(cell, referenceType);
	}

	/**
	 * Given expression of form e[i], returns a reference to the i-th element of
	 * the array defined by e. For example, if a is declared int[N] a, and the
	 * expression is "a[i]", this will return a reference to the i-th element of
	 * a.
	 * 
	 * @throws ExecutionProblem
	 * 
	 */
	private ReferenceValueIF arrayElementReferenceValue(
			EnvironmentIF environment, BinaryExpressionIF expression)
			throws ExecutionProblem {
		ValueIF assumption = environment.getAssumption();
		LHSExpressionIF arrayExpression = (LHSExpressionIF) expression.left();
		ExpressionIF indexExpression = expression.right();
		ReferenceValueIF oldReference, newReference;
		ValueIF extent, indexValue;

		assert expression.kind() == ExpressionKind.SUBSCRIPT;
		oldReference = referenceValue(environment, arrayExpression);
		extent = evaluateLength(environment, oldReference, expression);
		indexValue = evaluate(environment, indexExpression);
		try {
			ValueIF claim = dynamicFactory.not(assumption, dynamicFactory
					.lessThan(assumption, indexValue, zero));
			ResultType truth = dynamicFactory.valid(assumption, claim);

			if (truth != ResultType.YES) {
				String message;
				Certainty certainty;
				ExecutionException error;

				if (truth == ResultType.MAYBE) {
					message = "Cannot prove array index is non-negative:";
					certainty = Certainty.MAYBE;
				} else { /* true == ResultType.NO */
					message = "It is possible for the array index to be negative:";
					certainty = Certainty.PROVEABLE;
				}
				message += "\n  array expression : " + arrayExpression
						+ "\n  index expression : " + indexExpression
						+ "\n       index value : " + indexValue
						+ "\n    path condition : " + assumption;
				error = new ExecutionException(expression,
						ErrorKind.OUT_OF_BOUNDS, certainty, message);
				log.report(error);
				environment.addAssumption(claim);
			}
			claim = dynamicFactory.lessThanOrEquals(assumption, indexValue,
					extent);
			truth = dynamicFactory.valid(assumption, claim);
			if (truth != ResultType.YES) {
				String message;
				Certainty certainty;
				ExecutionException error;

				if (truth == ResultType.MAYBE) {
					message = "Cannot prove array index is within bounds:";
					certainty = Certainty.MAYBE;
				} else { /* true == ResultType.NO */
					message = "It is possible for the array index to be out of bounds:";
					certainty = Certainty.PROVEABLE;
				}
				message += "\n  array expression : " + arrayExpression
						+ "\n  index expression : " + indexExpression
						+ "\n       index value : " + indexValue
						+ "\n      array extent : " + extent
						+ "\n    path condition : " + assumption;
				error = new ExecutionException(expression,
						ErrorKind.OUT_OF_BOUNDS, certainty, message);
				log.report(error);
				environment.addAssumption(claim);
			}
		} catch (DynamicException e) {
			throw new ExecutionException(expression, e, Certainty.NONE);
		}
		newReference = dynamicFactory.arrayElementReference(oldReference,
				indexValue);
		return newReference;
	}

	private ReferenceValueIF recordElementReferenceValue(
			EnvironmentIF environment, RecordNavigationExpressionIF expression)
			throws ExecutionException {
		LHSExpressionIF recordExpression = expression.recordExpression();
		ReferenceValueIF recordReference = referenceValue(environment,
				recordExpression);
		int fieldIndex = expression.fieldIndex();
		ReferenceValueIF newReference = dynamicFactory.recordElementReference(
				recordReference, fieldIndex);

		return newReference;
	}

	/**
	 * This takes any left-hand side expression and returns a reference value to
	 * the object in memory determined by that expression.
	 * 
	 * LHS possibilities: variable, a[i], r.f, *p
	 * 
	 * @throws ExecutionException
	 */
	public ReferenceValueIF referenceValue(EnvironmentIF environment,
			LHSExpressionIF expression) throws ExecutionException {
		ExpressionKind expressionKind;

		if (expression == null)
			throw new RuntimeException("null expression");
		expressionKind = expression.kind();
		switch (expressionKind) {
		case VARIABLE:
			return variableReferenceValue(environment,
					(VariableExpressionIF) expression);
		case SUBSCRIPT:
			try {
				return arrayElementReferenceValue(environment,
						(BinaryExpressionIF) expression);
			} catch (ExecutionException error) {
				throw error;
			} catch (ExecutionProblem problem) {
				throw new ExecutionException(expression, problem);
			}
		case NAVIGATE:
			return recordElementReferenceValue(environment,
					(RecordNavigationExpressionIF) expression);
		case DEREFERENCE:
			return (ReferenceValueIF) evaluate(environment,
					((DereferenceExpressionIF) expression).expression());
		case PROCESS_REF:
			return variableReferenceValue(environment, variableExpression(
					environment, (ProcessReferenceExpressionIF) expression));
		case LITERAL:
			return objectLiteralReferenceValue(environment,
					(ObjectLiteralExpressionIF) expression);
		default:
			throw new ExecutionException(expression, ErrorKind.INTERNAL,
					Certainty.NONE,
					"Expected reference expression (Evaluator.referenceValue)");
		}
	}

	/**
	 * Evaluate an expression while ignoring checks for accessing input/output
	 * variables. A little bit of a hack.
	 * 
	 * @throws ExecutionException
	 */
	public ValueIF evaluateOverride(EnvironmentIF environment,
			ExpressionIF expression) throws ExecutionException {
		checkAccess = false;
		ValueIF result = evaluate(environment, expression);
		checkAccess = true;
		return result;
	}

	/**
	 * Takes any expression and returns the symbolic value of that expression in
	 * the given environment. This is a "right-hand side" evaluation.
	 * 
	 * @throws ExecutionException
	 * @throws DynamicException
	 */
	public ValueIF evaluate(EnvironmentIF environment, ExpressionIF expression)
			throws ExecutionException {
		ExpressionKind kind;
		ValueIF result;

		assert expression != null;
		assert environment != null;
		kind = expression.kind();
		try {
			if (expression instanceof BinaryExpressionIF) {
				result = evaluateBinary(environment,
						(BinaryExpressionIF) expression, kind);
			} else if (expression instanceof UnaryExpressionIF) {
				result = evaluateUnary(environment,
						(UnaryExpressionIF) expression, kind);
			} else {
				switch (kind) {
				case NOT_EMPTY:
					result = evaluateNotEmpty(environment,
							(NotEmptyExpressionIF) expression);
					break;
				case NOT_FULL:
					result = evaluateNotFull(environment,
							(NotFullExpressionIF) expression);
					break;
				case LITERAL:
					result = evaluateLiteral(environment,
							(LiteralExpressionIF) expression);
					break;
				case VARIABLE:
					result = evaluateVariable(environment,
							(VariableExpressionIF) expression);
					break;
				case IF_THEN_ELSE:
					result = evaluateIfThenElse(environment,
							(IfThenElseExpressionIF) expression);
					break;
				case FUNCTION:
					result = evaluateEvaluatedFunction(environment,
							(EvaluatedFunctionExpressionIF) expression);
					break;
				case NAVIGATE:
					result = evaluateNavigate(environment,
							(RecordNavigationExpressionIF) expression);
					break;
				case SIZEOF:
					result = evaluateSizeOf(environment,
							(SizeOfExpressionIF) expression);
					break;
				case FORALL:
					result = evaluateForall(environment,
							(BoundExpressionIF) expression);
					break;
				case EXISTS:
					result = evaluateExists(environment,
							(BoundExpressionIF) expression);
					break;
				case LAMBDA:
					result = evaluateLambda(environment,
							(BoundExpressionIF) expression);
					break;
				case PROCESS_REF:
					result = evaluateProcessReference(environment,
							(ProcessReferenceExpressionIF) expression);
					break;
				default:
					throw new ExecutionException(expression,
							ErrorKind.INTERNAL, Certainty.NONE,
							"Unknown expression type");
				}
			}
		} catch (ExecutionException error) {
			throw error;
		} catch (ExecutionProblem problem) {
			throw new ExecutionException(expression, problem);
		}
		return result;
	}

	private ValueIF evaluateProcessReference(EnvironmentIF environment,
			ProcessReferenceExpressionIF expression) throws ExecutionException {
		return evaluateVariable(environment, variableExpression(environment,
				expression));
	}

	/**
	 * This will get a local variable if that variable is in the outer-most
	 * scope. Need to think of some way to dis-ambiguate variables in nested
	 * scopes.
	 */
	private VariableExpressionIF variableExpression(EnvironmentIF environment,
			ProcessReferenceExpressionIF expression) throws ExecutionException {
		ModelIF model = expression.model();
		ValueIF pidValue = evaluate(environment, expression.pid());
		int pid;
		VariableIF variable;

		pid = ((IntegerNumberIF) dynamicFactory.numericValue(environment
				.getAssumption(), pidValue)).intValue();
		// Check for local variables given by name@function
		if (expression.variableName().contains("@")) {
			Scanner sc = new Scanner(expression.variableName());
			
			sc.useDelimiter("@");
			
			String shortName = sc.next();
			String functionName = sc.next();
			
			sc.close();
			variable = model.process(pid).scope()
					.functionWithName(functionName).outermostScope()
					.variableWithName(shortName);
		} else {
			variable = model.process(pid).scope().variableWithName(
					expression.variableName());
		}
		return modelFactory.variableExpression(variable);
	}

	// TODO: if function has restriction on input (such as lambda expression),
	// check that point satisfies the restriction.

	private ValueIF evaluateEvaluatedFunction(EnvironmentIF environment,
			EvaluatedFunctionExpressionIF expression) throws ExecutionException {
		int numParameters = expression.function().numFormals();
		ValueTypeIF parameterTypes[] = new ValueTypeIF[numParameters];
		ValueIF point[] = new ValueIF[numParameters];

		for (int i = 0; i < expression.function().numFormals(); i++) {
			point[i] = evaluate(environment, expression.getArgument(i));
			parameterTypes[i] = point[i].valueType();
		}
		try {
			ValueIF function = dynamicFactory.function(environment
					.getAssumption(), expression.function(), parameterTypes,
					valueType(environment, expression.function().returnType()));

			return dynamicFactory.apply(environment.getAssumption(), function,
					point);
		} catch (DynamicException error) {
			throw new ExecutionException(expression, error, Certainty.NONE);
		}
	}

	private ValueIF evaluateBinary(EnvironmentIF environment,
			BinaryExpressionIF binaryExpression, ExpressionKind kind)
			throws ExecutionProblem {
		if (kind == ExpressionKind.SUBSCRIPT) {
			return evaluateSubscript(environment,
					(LHSExpressionIF) binaryExpression);
		} else if (kind == ExpressionKind.AND) {
			// short circuit evaluation is done in special way...
			return evaluateAnd(environment, binaryExpression.left(),
					binaryExpression.right());
		} else if (kind == ExpressionKind.OR) {
			return evaluateOr(environment, binaryExpression.left(),
					binaryExpression.right());
		} else {
			ValueIF left = evaluate(environment, binaryExpression.left());
			ValueIF right = evaluate(environment, binaryExpression.right());

			switch (kind) {
			case ADD:
				return evaluateAdd(environment, left, right);
			case MULTIPLY:
				return evaluateMultiply(environment, left, right);
			case DIVIDE:
				return evaluateDivide(environment, binaryExpression, left,
						right);
			case SUBTRACT:
				return evaluateSubtract(environment, left, right);
			case MODULO:
				return evaluateModulo(environment, binaryExpression, left,
						right);
			case EQUALS:
				return evaluateEquals(environment, left, right);
			case LESS_THAN:
				return evaluateLessThan(environment, left, right);
			case LEQ:
				return evaluateLessThanOrEquals(environment, left, right);
			case POINTER_ADD:
				return evaluatePointerAdd(environment, (ReferenceValueIF) left,
						right, binaryExpression);
			case ARRAY_LAMBDA:
				return evaluateArrayLambda(environment, left, right);
			default:
				throw new ExecutionException(binaryExpression,
						ErrorKind.INTERNAL, Certainty.NONE,
						"Unknown binary operator: " + kind);
			}
		}
	}

	private ValueIF evaluateUnary(EnvironmentIF environment,
			UnaryExpressionIF unary, ExpressionKind kind)
			throws ExecutionException {
		ExpressionIF argument = unary.expression();

		try {
			if (kind == ExpressionKind.ADDRESS_OF) {
				return referenceValue(environment, (LHSExpressionIF) argument);
			} else {
				ValueIF argumentValue = evaluate(environment, argument);

				switch (kind) {
				case NOT:
					return evaluateNot(environment, argumentValue);
				case NEGATIVE:
					return evaluateNegative(environment, argumentValue);
				case LENGTH:
					return evaluateLength(environment, argumentValue, unary);
				case DEREFERENCE:
					return dereference(environment,
							(ReferenceValueIF) argumentValue, unary);
				case CAST:
					return evaluateCast(environment, unary.type(),
							argumentValue);
				default:
					throw new ExecutionException(unary, ErrorKind.INTERNAL,
							Certainty.NONE, "Unknown unary expression kind: "
									+ kind);
				}
			}
		} catch (ExecutionException error) {
			throw error;
		} catch (ExecutionProblem problem) {
			throw new ExecutionException(unary, problem);
		}
	}

	private ValueIF evaluateNavigate(EnvironmentIF environment,
			RecordNavigationExpressionIF navigateExpression)
			throws ExecutionException {
		RecordValueIF recordValue = (RecordValueIF) evaluate(environment,
				navigateExpression.recordExpression());
		int fieldIndex = navigateExpression.fieldIndex();

		return dynamicFactory.recordRead(environment.getAssumption(),
				recordValue, fieldIndex);
	}

	private ReferenceValueIF evaluateVariablePointerAdd(
			EnvironmentIF environment, VariableReferenceValueIF reference,
			ValueIF intValue, Sourceable sourceable) throws ExecutionException {
		try {
			ValueIF assumption = environment.getAssumption();
			ValueIF offset = reference.offset();
			ValueIF newOffset = dynamicFactory
					.add(assumption, offset, intValue);
			VariableReferenceValueIF newReference;

			ValueIF claim = dynamicFactory.lessThanOrEquals(assumption, zero,
					newOffset);
			ResultType truth = dynamicFactory.valid(assumption, claim);

			if (truth != ResultType.YES) {
				String message;
				Certainty certainty;

				if (truth == ResultType.MAYBE) {
					message = "Cannot prove that pointer addition results in non-negative offset:";
					certainty = Certainty.MAYBE;
				} else { /* truth == ResultType.NO */
					message = "Pointer addition can result in a negative offset:";
					certainty = Certainty.PROVEABLE;
				}
				message += "\n  original reference : " + reference
						+ "\n     original offset : " + offset
						+ "\n           increment : " + intValue
						+ "\n    resulting offset : " + newOffset
						+ "\n      path condition : " + assumption + "\n";
				log.report(new ExecutionException(sourceable,
						ErrorKind.OUT_OF_BOUNDS, certainty, message));
				environment.addAssumption(claim);
			}
			claim = dynamicFactory.lessThanOrEquals(assumption, newOffset, one);
			truth = dynamicFactory.valid(assumption, claim);
			if (truth != ResultType.YES) {
				String message;
				Certainty certainty;

				if (truth == ResultType.MAYBE) {
					message = "Cannot prove that result of pointer addition is within bounds:";
					certainty = Certainty.MAYBE;
				} else { /* truth == ResultType.NO */
					message = "Result of pointer addition can be out of bounds:";
					certainty = Certainty.PROVEABLE;
				}
				message += "\n  original reference : " + reference
						+ "\n     original offset : " + offset
						+ "\n           increment : " + intValue
						+ "\n    resulting offset : " + newOffset
						+ "\n      path condition : " + assumption + "\n";
				log.report(new ExecutionException(sourceable,
						ErrorKind.OUT_OF_BOUNDS, certainty, message));
				environment.addAssumption(claim);
			}
			newReference = dynamicFactory.referenceValue(reference.variable(),
					reference.valueType(), newOffset);
			return newReference;
		} catch (DynamicException error) {
			throw new ExecutionException(sourceable, error, Certainty.NONE);
		} catch (ExecutionProblem problem) {
			throw new ExecutionException(sourceable, problem);
		}
	}

	/**
	 * As in C, allow a pointer right after the last array element; throw
	 * exception if you ever try to dereference it.
	 */
	private ReferenceValueIF evaluateArrayElementPointerAdd(
			EnvironmentIF environment, ArrayElementReferenceValueIF reference,
			ValueIF intValue, Sourceable sourceable) throws ExecutionException {
		ValueIF assumption = environment.getAssumption();
		ReferenceValueIF parent = reference.parent(); // reference to array
		ValueIF index = reference.index(); // value of integer type

		// need to compare the base type of reference.valueType() with
		// value type of the array elements themselves.

		// the type of the array:
		ArrayValueTypeIF valueType = (ArrayValueTypeIF) parent.valueType()
				.baseType();

		if (valueType.dimension() > 1) {
			throw new ExecutionException(sourceable, ErrorKind.POINTER,
					Certainty.NONE,
					"Cannot perform pointer addition on ragged array: "
							+ reference);
		}

		// the number of elements in the array:
		ValueIF extent = valueType.extent();

		// the type of an element of the array:
		ValueTypeIF elementType = valueType.baseType();

		// the type referenced by "reference":
		ValueTypeIF referencedType = reference.valueType().baseType();

		ValueIF newIndex;
		ArrayElementReferenceValueIF newReference;

		try {
			if (elementType != null && elementType.equals(referencedType)) {
				newIndex = dynamicFactory.add(assumption, index, intValue);
			} else if (elementType != null) {
				// need to get sizeof(elementType) and sizeof(referencedType)
				ValueIF sizeofElementType = sizeof(environment, elementType);
				ValueIF sizeofReferencedType = sizeof(environment,
						referencedType);
				ValueIF numerator = dynamicFactory.multiply(assumption,
						sizeofReferencedType, intValue);

				newIndex = dynamicFactory.add(assumption, index, dynamicFactory
						.intDivide(assumption, numerator, sizeofElementType));

				ValueIF claim = dynamicFactory.equals(assumption, zero,
						dynamicFactory.modulo(assumption, numerator,
								sizeofElementType));
				ResultType truth = dynamicFactory.valid(assumption, claim);

				if (truth != ResultType.YES) {
					String message;
					Certainty certainty;

					if (truth == ResultType.MAYBE) {
						message = "Cannot prove that pointer into array is aligned with array element:";
						certainty = Certainty.MAYBE;
					} else {
						message = "It is possible for pointer into array to not be aligned with array element:";
						certainty = Certainty.PROVEABLE;
					}
					message += "\n  original reference : " + reference
							+ "\n   element type : " + elementType
							+ "\n   element type size: " + sizeofElementType
							+ "\n    increment value : " + intValue
							+ "\n    incrementing type : " + referencedType
							+ "\n   sizeof incrementing type : "
							+ sizeofReferencedType + "\n    byte increment : "
							+ numerator + "\n";
					message += "Expected the byte increment to be a multiple of element type size.";
					log.report(new ExecutionException(sourceable,
							ErrorKind.POINTER, certainty, message));
					environment.addAssumption(claim);
				}
			} else {
				throw new ExecutionProblem(ErrorKind.POINTER,
						Certainty.PROVEABLE,
						"Unable to perform pointer arithmetic: array of void type");
			}

			ValueIF claim = dynamicFactory.lessThanOrEquals(assumption,
					newIndex, extent);
			ResultType truth = dynamicFactory.valid(assumption, claim);

			if (truth != ResultType.YES) {
				String message;
				Certainty certainty;

				if (truth == ResultType.MAYBE) {
					message = "Cannot prove that result of pointer addition is within bounds:";
					certainty = Certainty.MAYBE;
				} else {
					message = "Result of pointer addition can extend beyond object bounds:";
					certainty = Certainty.PROVEABLE;
				}
				message += "\n          reference : " + reference
						+ "\n  integer increment : " + intValue
						+ "\n    resulting index : " + newIndex
						+ "\n       array extent : " + extent
						+ "\n              query : "
						+ dynamicFactory.lessThan(assumption, newIndex, extent)
						+ "\n    path condition = " + assumption;
				log.report(new ExecutionException(sourceable,
						ErrorKind.OUT_OF_BOUNDS, certainty, message));
				environment.addAssumption(claim);
			}
			newReference = dynamicFactory.arrayElementReference(parent,
					newIndex);
			return newReference;
		} catch (DynamicException error) {
			throw new ExecutionException(sourceable, error, Certainty.NONE);
		} catch (ExecutionProblem error) {
			throw new ExecutionException(sourceable, error);
		}
	}

	public ReferenceValueIF evaluatePointerAdd(EnvironmentIF environment,
			ReferenceValueIF reference, ValueIF intValue, Sourceable sourceable)
			throws ExecutionException {
		if (reference.isNull()) {
			throw new ExecutionException(sourceable, ErrorKind.POINTER,
					Certainty.PROVEABLE,
					"Attempt to apply pointer addition to a NULL pointer value:");
		} else if (reference instanceof ArrayElementReferenceValueIF) {
			return evaluateArrayElementPointerAdd(environment,
					(ArrayElementReferenceValueIF) reference, intValue,
					sourceable);
		} else if (reference instanceof VariableReferenceValueIF) {
			return evaluateVariablePointerAdd(environment,
					(VariableReferenceValueIF) reference, intValue, sourceable);
		} else {
			throw new ExecutionException(
					sourceable,
					ErrorKind.POINTER,
					Certainty.NONE,
					"Unsupported pointer arithmetic: TASS only supports pointer arithmetic"
							+ "\nfor a pointer to a variable or to an array element");
		}
	}

	// ideally, would like dereference to return two things: the value and
	// a boolean field to tell whether the value returned is "inside" the
	// referenced object, so that modifications to it will be reflected in
	// the original object.

	public ValueIF dereference(EnvironmentIF environment,
			ReferenceValueIF reference, Sourceable element)
			throws ExecutionException {
		ValueIF assumption;

		if (reference == null)
			throw new NullPointerException("null reference");
		if (environment == null)
			throw new NullPointerException("null environment");
		assumption = environment.getAssumption();

		ReferenceValueTypeIF referenceValueType = reference.valueType();
		ValueTypeIF referencedType = referenceValueType.baseType();
		ValueIF result;

		if (reference.isNull()) {
			throw new ExecutionException(element, ErrorKind.DEREFERENCE,
					Certainty.PROVEABLE,
					"Attempt to dereference a null pointer value:"
							+ "\n type : " + reference.valueType());
		} else if (reference instanceof VariableReferenceValueIF) {
			CellIF cell = ((VariableReferenceValueIF) reference).variable();

			if (checkAccess && cell instanceof SharedCellIF) {
				SharedVariableIF variable = ((SharedCellIF) cell).variable();

				if (variable.isOutput()
						&& variable.type().kind() != TypeKind.ARRAY) {
					throw new ExecutionException(element,
							ErrorKind.OUTPUT_READ, Certainty.MAYBE,
							"Attempt to read output variable through dereference: "
									+ variable);
				}
			}
			if (cell instanceof ModelCellIF) {
				result = environment.valueOf((ModelCellIF) cell);
			} else {
				LiteralCellIF literalCell = (LiteralCellIF) cell;
				ObjectLiteralExpressionIF literalExpression = literalCell
						.expression();

				result = evaluateLiteral(environment, literalExpression);
			}
		} else if (reference instanceof ArrayElementReferenceValueIF) {
			ArrayValueIF arrayValue = (ArrayValueIF) dereference(environment,
					reference.parent(), element);
			ValueIF index = ((ArrayElementReferenceValueIF) reference).index();
			ValueIF extent = arrayValue.valueType().extent();

			if (checkAccess) {
				// is this a scalar cell of an output array?
				VariableReferenceValueIF variableReference = reference
						.variableReference();
				CellIF cell = variableReference.variable();

				if (cell instanceof SharedCellIF) {
					SharedVariableIF variable = ((SharedCellIF) cell)
							.variable();

					if (variable.isOutput()
							&& variable.type().kind() == TypeKind.ARRAY
							&& ((ArrayTypeIF) variable.type()).elementType()
									.kind() != TypeKind.ARRAY) {
						throw new ExecutionException(element,
								ErrorKind.OUTPUT_READ, Certainty.MAYBE,
								"Attempt to read output variable through dereference");
					}
				}
			}
			try {
				ValueIF claim = dynamicFactory.lessThan(assumption, index,
						extent);
				ResultType truth = dynamicFactory.valid(assumption, claim);
				ExecutionException error;

				if (truth != ResultType.YES) {
					String message;
					Certainty certainty;

					if (truth == ResultType.MAYBE) {
						message = "Unable to prove that array element reference is within bounds:";
						certainty = Certainty.MAYBE;
					} else {
						message = "Array element reference can extend beyond last element of array:";
						certainty = Certainty.PROVEABLE;
					}
					message += "\n          reference : " + reference
							+ "\n              index : " + index
							+ "\n       array extent : " + extent
							+ "\n              query : " + claim
							+ "\n     path condition : " + assumption;
					error = new ExecutionException(element,
							ErrorKind.OUT_OF_BOUNDS, certainty, message);
					log.report(error);
					environment.addAssumption(claim);
				}
				result = dynamicFactory
						.arrayRead(assumption, arrayValue, index);
			} catch (DynamicException e) {
				throw new ExecutionException(element, e, Certainty.NONE);
			} catch (ExecutionProblem problem) {
				throw new ExecutionException(element, problem);
			}
		} else if (reference instanceof RecordElementReferenceValueIF) {
			RecordValueIF recordValue = (RecordValueIF) dereference(
					environment, reference.parent(), element);
			int fieldIndex = ((RecordElementReferenceValueIF) reference)
					.fieldIndex();

			result = dynamicFactory.recordRead(assumption, recordValue,
					fieldIndex);
		} else {
			throw new ExecutionException(element, ErrorKind.INTERNAL,
					Certainty.NONE, "Unknown reference value:\n" + reference);
		}
		if (!result.valueType().equals(referencedType)) {
			throw new ExecutionException(element, ErrorKind.DEREFERENCE,
					Certainty.MAYBE,
					"Dereferencing error: pointer type does not match value type:\n"
							+ "referenced type: " + referencedType + "\n"
							+ "value type: " + result.valueType());
		}
		return result;
	}

	private ValueIF evaluateSubscript(EnvironmentIF environment,
			LHSExpressionIF subscriptExpression) throws ExecutionException {
		try {
			return dereference(environment, referenceValue(environment,
					subscriptExpression), subscriptExpression);
		} catch (ExecutionProblem e) {
			throw new ExecutionException(subscriptExpression, e);
		}
	}

	private ValueIF evaluateAdd(EnvironmentIF environment, ValueIF left,
			ValueIF right) throws ExecutionProblem {
		try {
			return dynamicFactory.add(environment.getAssumption(), left, right);
		} catch (DynamicException error) {
			throw new ExecutionProblem(error, Certainty.NONE);
		}
	}

	private ValueIF evaluateSubtract(EnvironmentIF environment, ValueIF left,
			ValueIF right) throws ExecutionProblem {
		try {
			return dynamicFactory.subtract(environment.getAssumption(), left,
					right);
		} catch (DynamicException error) {
			throw new ExecutionProblem(error, Certainty.NONE);
		}
	}

	private ValueIF evaluateMultiply(EnvironmentIF environment, ValueIF left,
			ValueIF right) {
		return dynamicFactory
				.multiply(environment.getAssumption(), left, right);
	}

	// need to cast integer values to real in mixed expressions. or do
	// statically?
	private ValueIF evaluateDivide(EnvironmentIF environment,
			BinaryExpressionIF expression, ValueIF numerator,
			ValueIF denominator) throws ExecutionException {
		ValueIF assumption = environment.getAssumption();
		ValueIF theZero = (denominator.valueType().equals(integerType) ? zero
				: zeroReal);

		try {
			ValueIF claim = dynamicFactory.not(assumption, dynamicFactory
					.equals(assumption, denominator, theZero));
			ResultType truth = dynamicFactory.valid(assumption, claim);

			if (truth != ResultType.YES) {
				String message;
				Certainty certainty;
				ExecutionException error;

				if (truth == ResultType.MAYBE) {
					message = "Cannot prove that denominator in division is non-zero:";
					certainty = Certainty.MAYBE;
				} else {
					message = "Denominator in division can be zero:";
					certainty = Certainty.PROVEABLE;
				}
				message += "\n" + denominator;
				error = new ExecutionException(expression,
						ErrorKind.DIVISION_BY_ZERO, certainty, message);
				environment.addAssumption(claim);
				if (dynamicFactory.nsat(environment.getAssumption()))
					throw error;
				log.report(error);
			}
			if (expression.type().kind() == TypeKind.INTEGER) {
				// this is integer division, which is hard.
				// this is stricter than necessary, but for now we treat
				// integer division with negative denominator to be illegal:

				ValueIF intClaim = dynamicFactory.not(assumption,
						dynamicFactory.lessThan(assumption, denominator,
								theZero));
				ResultType intTruth = dynamicFactory
						.valid(assumption, intClaim);

				if (intTruth != ResultType.YES) {
					String intMessage;
					Certainty intCertainty;
					ExecutionException intError;

					if (intTruth == ResultType.MAYBE) {
						intMessage = "Cannot prove that denominator in integer division is positive."
								+ "\nInteger division with negative denominator is strongly discouraged:";
						intCertainty = Certainty.MAYBE;
					} else {
						intMessage = "It is possible for the denominator of the integer division operation "
								+ "\nto be negative.  This is strongly discouraged:";
						intCertainty = Certainty.PROVEABLE;
					}
					intMessage += "\n  denominator    : " + denominator
							+ "\n  path condition : " + assumption;
					intError = new ExecutionException(expression,
							ErrorKind.INT_DIVISION, intCertainty, intMessage);
					environment.addAssumption(intClaim);
					if (dynamicFactory.nsat(environment.getAssumption()))
						throw intError;
					log.report(intError);
				}

				IntegerNumberIF numeratorInt = (IntegerNumberIF) dynamicFactory
						.numericValue(assumption, numerator);

				if (numeratorInt != null) {
					IntegerNumberIF denominatorInt = (IntegerNumberIF) dynamicFactory
							.numericValue(assumption, denominator);

					if (denominatorInt != null)
						return dynamicFactory.symbolicValue(numberFactory
								.divide(numeratorInt, denominatorInt));
				}
				return dynamicFactory.intDivide(assumption, numerator,
						denominator);
			}
			return dynamicFactory.divide(assumption, numerator, denominator);
		} catch (DynamicException error) {
			throw new ExecutionException(expression, error, Certainty.NONE);
		} catch (ExecutionProblem problem) {
			throw new ExecutionException(expression, problem);
		}
	}

	private ValueIF evaluateModulo(EnvironmentIF environment,
			BinaryExpressionIF expression, ValueIF left, ValueIF right)
			throws ExecutionException {
		ValueIF numerator = left;
		ValueIF denominator = right;
		ValueIF assumption = environment.getAssumption();

		try {
			ValueIF claim = dynamicFactory.not(assumption, dynamicFactory
					.equals(assumption, denominator, zero));
			ResultType truth = dynamicFactory.valid(assumption, claim);

			if (truth != ResultType.YES) {
				String message;
				Certainty certainty;
				ExecutionException error;

				if (truth == ResultType.MAYBE) {
					message = "Cannot prove that denominator in modulus is non-zero:";
					certainty = Certainty.MAYBE;
				} else {
					message = "Denominator in modulus can be zero:";
					certainty = Certainty.PROVEABLE;
				}
				message += "\n" + denominator;
				error = new ExecutionException(expression,
						ErrorKind.DIVISION_BY_ZERO, certainty, message);
				environment.addAssumption(claim);
				if (dynamicFactory.nsat(environment.getAssumption()))
					throw error;
				log.report(error);
			}
			return dynamicFactory.modulo(assumption, numerator, denominator);
		} catch (DynamicException error) {
			throw new ExecutionException(expression, error, Certainty.NONE);
		} catch (ExecutionProblem problem) {
			throw new ExecutionException(expression, problem);
		}
	}

	private ProcessIF process(EnvironmentIF environment, ModelIF model,
			ExpressionIF expression) throws ExecutionException {
		if (expression.kind() == ExpressionKind.ANY) {
			return null;
		} else {
			ValueIF assumption = environment.getAssumption();
			ValueIF value = evaluate(environment, expression);
			IntegerNumberIF number = (IntegerNumberIF) dynamicFactory
					.numericValue(assumption, value);
			int pid;

			if (number == null)
				throw new ExecutionException(expression, ErrorKind.INTERNAL,
						Certainty.NONE,
						"Expected integer concrete value from expression");
			pid = number.intValue();
			if (pid < 0 || pid >= model.numProcs())
				throw new ExecutionException(expression, ErrorKind.INVALID_PID,
						Certainty.PROVEABLE, "Illegal value for process id:\n"
								+ pid + "\nModel " + model.name() + " has "
								+ model.numProcs() + " process(es).");
			return model.process(pid);
		}
	}

	private ValueIF tagValue(EnvironmentIF environment, ExpressionIF expression)
			throws ExecutionException {
		if (expression.kind() == ExpressionKind.ANY) {
			return null;
		} else {
			return evaluate(environment, expression);
		}
	}

	private ValueIF evaluateNotEmpty(EnvironmentIF environment,
			NotEmptyExpressionIF expression) throws ExecutionException {
		ModelIF model = expression.model();
		ExpressionIF destinationExpression = expression.destination();
		ExpressionIF sourceExpression = expression.source();
		ExpressionIF tagExpression = expression.tag();
		ProcessIF destinationProcess = process(environment, model,
				destinationExpression);
		ProcessIF sourceProcess = process(environment, model, sourceExpression);
		ValueIF tagValue = tagValue(environment, tagExpression);
		boolean result;

		if (destinationProcess == null)
			throw new ExecutionException(expression, ErrorKind.COMMUNICATION,
					Certainty.NONE,
					"Destination process cannot be determined:\n" + expression);
		try {
			result = environment.hasMessage(sourceProcess, destinationProcess,
					tagValue);
		} catch (ExecutionProblem error) {
			throw new ExecutionException(expression, error);
		}
		return dynamicFactory.symbolicValue(result);
	}

	// what if expression evaluates to MPI_PROC_NULL?
	private ValueIF evaluateNotFull(EnvironmentIF environment,
			NotFullExpressionIF expression) {
		int numMessages = environment.numMessages(expression.model());
		boolean result = numMessages < bufferSize;

		return dynamicFactory.symbolicValue(result);
	}

	/**
	 * Short-circuit evaluatin of AND. Evaluate left, then evaluate right under
	 * assumption that left is true. Example: a>0 && b/a<7 should evaluate
	 * without throwing a divide by 0 exception.
	 * 
	 * @throws ExecutionProblem
	 */
	private ValueIF evaluateAnd(EnvironmentIF environment, ExpressionIF left,
			ExpressionIF right) throws ExecutionProblem {
		ValueIF assumption = environment.getAssumption();
		ValueIF value1 = evaluate(environment, left);
		ValueIF value2, result;

		environment.setAssumption(dynamicFactory.and(trueValue, assumption,
				value1));
		value2 = evaluate(environment, right);
		result = dynamicFactory.and(assumption, value1, value2);
		environment.setAssumption(assumption);
		return result;
	}

	// TODO: use local environments...

	private ValueIF evaluateOr(EnvironmentIF environment, ExpressionIF left,
			ExpressionIF right) throws ExecutionProblem {
		ValueIF assumption = environment.getAssumption();
		ValueIF value1 = evaluate(environment, left);
		ValueIF value2, result;

		try {
			environment.setAssumption(dynamicFactory.and(trueValue, assumption,
					dynamicFactory.not(trueValue, value1)));
			// TODO: problem: if the following statement modifies the
			// assumption the modification will be lost.
			// Solution: detect this and set assumption to false, abandoning
			// recovery attempt?
			value2 = evaluate(environment, right);
			result = dynamicFactory.or(assumption, value1, value2);
			environment.setAssumption(assumption);

			return result;
		} catch (DynamicException e) {
			throw new ExecutionProblem(e, Certainty.NONE);
		}
	}

	private ValueIF evaluateNot(EnvironmentIF environment, ValueIF value)
			throws ExecutionProblem {
		try {
			return dynamicFactory.not(environment.getAssumption(), value);
		} catch (DynamicException e) {
			throw new ExecutionProblem(e, Certainty.NONE);
		}
	}

	private ValueIF evaluateEquals(EnvironmentIF environment, ValueIF left,
			ValueIF right) throws ExecutionProblem {
		try {
			return dynamicFactory.equals(environment.getAssumption(), left,
					right);
		} catch (DynamicException e) {
			throw new ExecutionProblem(e, Certainty.NONE);
		}
	}

	private ValueIF evaluateLessThan(EnvironmentIF environment, ValueIF left,
			ValueIF right) throws ExecutionProblem {
		try {
			return dynamicFactory.lessThan(environment.getAssumption(), left,
					right);
		} catch (DynamicException e) {
			throw new ExecutionProblem(e, Certainty.NONE);
		}
	}

	private ValueIF evaluateLessThanOrEquals(EnvironmentIF environment,
			ValueIF left, ValueIF right) throws ExecutionProblem {
		try {
			return dynamicFactory.lessThanOrEquals(environment.getAssumption(),
					left, right);
		} catch (DynamicException e) {
			throw new ExecutionProblem(e, Certainty.NONE);
		}
	}

	// can you put this into dynamic factory?
	// need to figure out dynamic type of literal but should be possible.
	// should be independent of environment. can also be cached.

	// alternative: everyplace in which you try to get value of literal
	// cell from environment, instead send here.???

	// does it depend on whether being used for initializer or in expression?
	// should be able to get dynamic type of variable if initializer

	private ValueIF evaluateLiteral(EnvironmentIF environment,
			LiteralExpressionIF expression) throws ExecutionException {
		ValueIF result = null; // (ValueIF) expression.dynamicValue();

		// if (result != null)
		// return result;
		

		Object value = expression.value();

		if (value == null) {
			// NULL pointer value
			result = dynamicFactory
					.nullReferenceValue((ReferenceValueTypeIF) valueType(
							environment, expression.type()));
		} else if (value instanceof Boolean) {
			result = dynamicFactory.symbolicValue((Boolean) value);
		} else if (value instanceof Character) {
			result = dynamicFactory.symbolicValue((Character) value);
		} else if (value instanceof NumberIF) {
			result = dynamicFactory.symbolicValue((NumberIF) value);
		} else if (expression instanceof ObjectLiteralExpressionIF) {
			ValueTypeIF valueType = valueType(environment, expression.type());

			result = evaluateObjectLiteral(environment,
					(ObjectLiteralExpressionIF) expression, valueType);
		} else {
			throw new ExecutionException(expression, ErrorKind.INTERNAL,
					Certainty.NONE, "Unknown literal value: " + value);
		}
		// expression.setDynamicValue(result);
		return result;
	}

	/**
	 * Given a value type that may have some array extents null, and some others
	 * not null, evaluate the literal expression to produce a value type that is
	 * complete (no non-null extents) and agrees with the given partial value
	 * type on everything that was non-null.
	 */
	public ValueIF evaluateObjectLiteral(EnvironmentIF environment,
			ObjectLiteralExpressionIF expression, ValueTypeIF partialValueType)
			throws ExecutionException {
		LiteralTypeIF literalType = expression.literalType();
		ValueTypeIF valueType = completeValueType(environment,
				partialValueType, literalType);

		return evaluateObjectLiteralComplete(environment, expression, valueType);
	}

	/** Value type may not contain ragged array types. */
	private ValueIF evaluateObjectLiteralComplete(EnvironmentIF environment,
			ObjectLiteralExpressionIF expression, ValueTypeIF valueType)
			throws ExecutionException {
		if (valueType instanceof ArrayValueTypeIF) {
			ArrayValueTypeIF arrayValueType = (ArrayValueTypeIF) valueType;

			assert arrayValueType.dimension() == 1;

			ValueTypeIF elementValueType = arrayValueType.baseType();
			ObjectLiteralExpressionIF object = (ObjectLiteralExpressionIF) expression;
			ExpressionIF[] elementExpressions = object.value();
			int numElements = elementExpressions.length;
			ValueIF[] elementValues = new ValueIF[numElements];

			for (int i = 0; i < numElements; i++) {
				ExpressionIF elementExpression = elementExpressions[i];

				if (elementExpression == null)
					continue; // actually in C, init to "0"
				if (elementExpression instanceof ObjectLiteralExpressionIF) {
					elementValues[i] = evaluateObjectLiteralComplete(
							environment,
							(ObjectLiteralExpressionIF) elementExpression,
							elementValueType);
				} else {
					elementValues[i] = evaluate(environment, elementExpression);
				}
			}
			return dynamicFactory.arrayValue(arrayValueType, elementValues);
		} else if (valueType instanceof RecordValueTypeIF) {
			RecordValueTypeIF recordValueType = (RecordValueTypeIF) valueType;
			ObjectLiteralExpressionIF object = (ObjectLiteralExpressionIF) expression;
			ExpressionIF[] elementExpressions = object.value();
			int numElements = elementExpressions.length;
			int numFields = recordValueType.type().numFields();
			ValueIF[] elementValues = new ValueIF[numFields];

			for (int i = 0; i < numElements; i++) {
				ExpressionIF elementExpression = elementExpressions[i];

				if (elementExpression == null)
					continue; // actually in C, init to "0"
				if (elementExpression instanceof ObjectLiteralExpressionIF) {
					elementValues[i] = evaluateObjectLiteralComplete(
							environment,
							(ObjectLiteralExpressionIF) elementExpression,
							recordValueType.fieldType(i));
				} else {
					elementValues[i] = evaluate(environment, elementExpression);
				}
			}
			for (int i = numElements; i < numFields; i++) {
				elementValues[i] = null;
			}
			return dynamicFactory.recordValue(recordValueType, elementValues);
		} else {
			throw new RuntimeException("Unknown literal kind.");
		}
	}

	/**
	 * Given a value type that may not be complete (i.e., some array extents may
	 * be null), complete it using the data provided in the literal type.
	 * 
	 * The value type may not contain any ragged array type.
	 */
	private ValueTypeIF completeValueType(EnvironmentIF environment,
			ValueTypeIF partialValueType, LiteralTypeIF literalType)
			throws ExecutionException {
		if (partialValueType instanceof ArrayValueTypeIF) {
			ArrayValueTypeIF arrayValueType = (ArrayValueTypeIF) partialValueType;
			ArrayLiteralTypeIF arrayLiteralType = (ArrayLiteralTypeIF) literalType;
			LiteralTypeIF elementLiteralType = arrayLiteralType
					.elementLiteralType();
			int literalExtent = arrayLiteralType.extent();
			ValueIF extent = arrayValueType.extent();
			ValueTypeIF elementValueType = arrayValueType.baseType();

			assert arrayValueType.dimension() == 1;
			elementValueType = completeValueType(environment, elementValueType,
					elementLiteralType);
			if (extent == null) {
				extent = dynamicFactory.symbolicValue(literalExtent);
			} else {
				// check that extent >= literalExtent
			}
			arrayValueType = dynamicFactory.arrayValueType(elementValueType,
					extent);
			return arrayValueType;
		} else if (partialValueType instanceof RecordValueTypeIF) {
			RecordLiteralTypeIF recordLiteralType = (RecordLiteralTypeIF) literalType;
			LiteralTypeIF[] fieldLiteralTypes = recordLiteralType
					.fieldLiteralTypes();
			int numFields = fieldLiteralTypes.length;
			RecordValueTypeIF recordValueType = (RecordValueTypeIF) partialValueType;
			ValueTypeIF[] newFieldValueTypes = new ValueTypeIF[numFields];

			for (int i = 0; i < numFields; i++) {
				newFieldValueTypes[i] = completeValueType(environment,
						recordValueType.fieldType(i), fieldLiteralTypes[i]);
			}
			recordValueType = dynamicFactory.recordValueType(recordValueType
					.type(), newFieldValueTypes);
			return recordValueType;
		} else {
			return partialValueType;
		}
	}

	private ValueIF evaluateNegative(EnvironmentIF environment, ValueIF value)
			throws ExecutionProblem {
		try {
			return dynamicFactory.negative(environment.getAssumption(), value);
		} catch (DynamicException e) {
			throw new ExecutionProblem(e, Certainty.NONE);
		}
	}

	// TODO: need to evalute bound variable but specifying value type...

	/**
	 * Returns the value associated to a variable.
	 * 
	 * For a variable of array type, this returns an array value. If the
	 * variable is a formal parameter, the environment associates to it a
	 * reference to a variable, so it is dereferenced and the result returned.
	 * Otherwise, the environment associates to it a variable value and that is
	 * returned.
	 */
	private ValueIF evaluateVariable(EnvironmentIF environment,
			VariableExpressionIF expression) throws ExecutionException {
		VariableIF variable = expression.variable();

		if (variable.scope().kind() == ScopeKind.BOUND) {
			try {
				return dynamicFactory
						.valueOfBoundVariable((BoundVariableIF) variable);
			} catch (DynamicException e) {
				throw new ExecutionException(expression, e, Certainty.NONE);
			}
		}

		ModelCellIF cell = cell(environment, variable);
		ValueIF value = environment.valueOf(cell);

		if (checkAccess && variable instanceof SharedVariableIF
				&& (((SharedVariableIF) variable).isOutput())) {
			throw new ExecutionException(expression, ErrorKind.OUTPUT_READ,
					Certainty.MAYBE, "Attempt to read output variable");
		}
		if (variable.type().kind() == TypeKind.ARRAY
				&& variable instanceof FormalVariableIF) {
			try {
				value = dereference(environment, (ReferenceValueIF) value,
						expression);
			} catch (ExecutionProblem e) {
				throw new ExecutionException(expression, e);
			}
		}
		if (value == null || dynamicFactory.isUndefined(value)) {
			throw new ExecutionException(expression, ErrorKind.UNDEFINED_VALUE,
					Certainty.PROVEABLE, "Variable is undefined: " + variable);
		}
		return value;
	}

	private ValueIF evaluateLength(EnvironmentIF environment, ValueIF value,
			Sourceable element) throws ExecutionProblem {
		ValueTypeIF valueType;
		ValueIF extent;
		ValueIF arrayValue;
		// it is OK to get the length of an output variable array
		boolean holdAccessFlag = checkAccess;

		checkAccess = false;
		if (!(value instanceof ReferenceValueIF))
			throw new RuntimeException("Expected array reference value:\n"
					+ value);
		arrayValue = dereference(environment, (ReferenceValueIF) value, element);
		valueType = arrayValue.valueType();
		if (!(valueType instanceof ArrayValueTypeIF))
			throw new RuntimeException(
					"Expected referenced type to be array:\n" + valueType);
		extent = ((ArrayValueTypeIF) valueType).extent();
		checkAccess = holdAccessFlag;
		return extent;
	}

	private ValueIF evaluateIfThenElse(EnvironmentIF environment,
			IfThenElseExpressionIF expression) throws ExecutionException {
		ExpressionIF condition = expression.condition();
		ExpressionIF trueExpression = expression.trueValue();
		ExpressionIF falseExpression = expression.falseValue();
		ValueIF assumption = environment.getAssumption();
		ValueIF conditionValue = evaluate(environment, condition);

		try {
			if (dynamicFactory.isValid(assumption, conditionValue))
				return evaluate(environment, trueExpression);
			if (dynamicFactory.isValid(assumption, dynamicFactory.not(
					assumption, conditionValue)))
				return evaluate(environment, falseExpression);
			return dynamicFactory.ifThenElse(assumption, conditionValue,
					evaluate(environment, trueExpression), evaluate(
							environment, falseExpression));
		} catch (DynamicException e) {
			throw new ExecutionException(expression, e, Certainty.NONE);
		}
	}

	private ValueIF evaluateCast(EnvironmentIF environment, TypeIF newType,
			ValueIF value) throws ExecutionProblem {
		ValueTypeIF oldValueType = value.valueType();
		ValueTypeIF newValueType = valueType(environment, newType);

		if (newType.kind() == TypeKind.RATIONAL) {

			if (oldValueType instanceof PrimitiveValueTypeIF) {
				if (((PrimitiveValueTypeIF) oldValueType).type().kind() == TypeKind.INTEGER) {
					try {
						return dynamicFactory.cast(realType, value);
					} catch (DynamicException e) {
						throw new ExecutionProblem(e, Certainty.NONE);
					}
				}
			}
		} else if (newValueType instanceof ReferenceValueTypeIF
				&& oldValueType instanceof ReferenceValueTypeIF) {
			if (((ReferenceValueIF) value).isNull()) {
				return dynamicFactory
						.nullReferenceValue((ReferenceValueTypeIF) newValueType);
			} else if (value instanceof VariableReferenceValueIF) {
				return dynamicFactory.referenceValue(
						((VariableReferenceValueIF) value).variable(),
						(ReferenceValueTypeIF) newValueType,
						((VariableReferenceValueIF) value).offset());
			} else if (value instanceof ArrayElementReferenceValueIF) {
				ArrayElementReferenceValueIF old = (ArrayElementReferenceValueIF) value;

				return dynamicFactory.arrayElementReference(old.parent(), old
						.index(), (ReferenceValueTypeIF) newValueType);

			} else if (value instanceof RecordElementReferenceValueIF) {
				RecordElementReferenceValueIF old = (RecordElementReferenceValueIF) value;

				return dynamicFactory.recordElementReference(old.parent(), old
						.fieldIndex(), (ReferenceValueTypeIF) newValueType);
			} else {
				throw new RuntimeException(
						"TASS internal error: unknown reference type: "
								+ oldValueType);
			}
		}
		throw new ExecutionProblem(ErrorKind.INVALID_CAST, Certainty.MAYBE,
				"TASS does not support casting " + value + " to " + newType);
	}

	private ValueIF evaluateSizeOf(EnvironmentIF environment,
			SizeOfExpressionIF expression) throws ExecutionException {
		TypeIF type = expression.typeArgument();
		ValueTypeIF valueType = valueType(environment, type);

		try {
			ValueIF result = sizeof(environment, valueType);

			return result;
		} catch (DynamicException e) {
			throw new ExecutionException(expression, e, Certainty.NONE);
		} catch (ExecutionProblem e) {
			throw new ExecutionException(expression, e);
		}
	}

	/* Type to ValueType conversion... */

	/**
	 * Translates a type to corresponding dynamic type. Array extents are left
	 * unspecified.
	 * 
	 * @throws ExecutionException
	 */
	ValueTypeIF valueType(EnvironmentIF environment, TypeIF type)
			throws ExecutionException {
		Map<TypeIF, ValueTypeIF> map = new HashMap<TypeIF, ValueTypeIF>();
		ValueTypeIF result = valueType(environment, type, map);

		// return dynamicFactory.commit(result);
		return result;
	}

	/**
	 * Determine the dynamic type associated to a variable in a given
	 * environment. For a variable of array type, the array dimension
	 * expressions are evaluated and checked to be non-negative.
	 * 
	 * For a variable of array type, the dynamic type will have the form
	 * reference-to-T, where T is a dynamic array type. T will then have the
	 * form array of length N of B, where B is the dyanmic type of the elements,
	 * and N is a value which may or may not be null.
	 * 
	 * If this is a formal parameter array variable, as in f(int[] a), then the
	 * lengths in the dynamic type will all be null. Otherwise, it is a proper
	 * local or global variable that is declared with dimension expressions;
	 * these will be evaluated, checked to be non-negative, and incorporated
	 * into T.
	 * 
	 * @throws ExecutionException
	 */

	// TODO: generalize for ragged...get unique name of variable
	// need to know if input variable or not.

	ValueTypeIF variableValueType(EnvironmentIF environment, VariableIF variable)
			throws ExecutionException {
		TypeIF type = variable.type();

		if (type.kind() == TypeKind.ARRAY) {
			ExpressionIF[] dimensionExpressions = variable
					.dimensionExpressions();

			if (dimensionExpressions == null) { // formal parameter
				assert (variable instanceof FormalVariableIF);
				return dynamicFactory.referenceValueType(valueType(environment,
						type));
			} else {
				return arrayValueType(environment, (ArrayTypeIF) type,
						dimensionExpressions);
			}
		} else {
			return valueType(environment, type);
		}
	}

	/**
	 * Translates a type to corresponding dynamic type. Array extents are left
	 * unspecified.
	 * 
	 * @throws ExecutionException
	 */
	private ValueTypeIF valueType(EnvironmentIF environment, TypeIF type,
			Map<TypeIF, ValueTypeIF> map) throws ExecutionException {
		switch (type.kind()) {
		case BOOLEAN:
			return dynamicFactory.booleanType();
		case INTEGER:
			return dynamicFactory.integerType();
		case RATIONAL:
			return dynamicFactory.realType();
		case CHAR:
			return dynamicFactory.characterType();
		default: {
			ValueTypeIF result = map.get(type);

			if (result != null)
				return result;
			switch (type.kind()) {
			case POINTER:
				result = referenceValueType(environment, (PointerTypeIF) type,
						map);
				break;
			case RECORD:
				result = recordValueType(environment, (RecordTypeIF) type, map);
				break;
			case ARRAY:
				result = arrayValueType(environment, (ArrayTypeIF) type, map);
				break;
			case FUNCTION:
				result = functionValueType(environment, (FunctionTypeIF) type,
						map);
				break;
			default:
				throw new IllegalArgumentException("Unknown type: " + type);
			}
			return result;
		}
		}
	}

	private RecordValueTypeIF recordValueType(EnvironmentIF environment,
			RecordTypeIF recordType, Map<TypeIF, ValueTypeIF> map)
			throws ExecutionException {
		int numFields = recordType.numFields();
		ValueTypeIF[] fieldTypes = new ValueTypeIF[numFields];
		RecordValueTypeIF result;

		for (int i = 0; i < numFields; i++) {
			TypeIF type = recordType.fieldType(i);

			if (type.kind() == TypeKind.ARRAY) {
				fieldTypes[i] = arrayValueType(environment, (ArrayTypeIF) type,
						recordType.dimensionExpressions(i), map);
			} else {
				fieldTypes[i] = valueType(environment, type, map);
			}
		}
		result = dynamicFactory.recordValueType(recordType, fieldTypes);
		map.put(recordType, result);
		// for (int i = 0; i < numFields; i++) {
		// TypeIF type = recordType.fieldType(i);
		//
		// if (type.kind() == TypeKind.POINTER) {
		// TypeIF baseType = ((PointerTypeIF) type).baseType();
		// ValueTypeIF baseValueType = valueType(environment, baseType,
		// map);
		//
		// dynamicFactory.complete((ReferenceValueTypeIF) fieldTypes[i],
		// baseValueType);
		// }
		// }
		return result;
	}

	private FunctionValueTypeIF functionValueType(EnvironmentIF environment,
			FunctionTypeIF functionType, Map<TypeIF, ValueTypeIF> map)
			throws ExecutionException {
		TypeIF[] inputTypes = functionType.inputTypes();
		int numInputs = inputTypes.length;
		TypeIF returnType = functionType.outputType();
		ValueTypeIF[] inputValueTypes = new ValueTypeIF[numInputs];
		ValueTypeIF returnValueType;
		FunctionValueTypeIF result;

		for (int i = 0; i < numInputs; i++) {
			inputValueTypes[i] = valueType(environment, inputTypes[i], map);
		}
		returnValueType = valueType(environment, returnType, map);
		result = dynamicFactory.functionValueType(inputValueTypes,
				returnValueType);
		map.put(functionType, result);
		// for (int i = 0; i < numInputs; i++) {
		// if (inputTypes[i].kind() == TypeKind.POINTER) {
		// TypeIF baseType = ((PointerTypeIF) inputTypes[i]).baseType();
		// ValueTypeIF baseValueType = valueType(environment, baseType,
		// map);
		//
		// dynamicFactory.complete(
		// (ReferenceValueTypeIF) inputValueTypes[i],
		// baseValueType);
		// }
		// }
		// if (returnType.kind() == TypeKind.POINTER) {
		// TypeIF baseType = ((PointerTypeIF) returnType).baseType();
		// ValueTypeIF baseValueType = valueType(environment, baseType, map);
		//
		// dynamicFactory.complete((ReferenceValueTypeIF) returnValueType,
		// baseValueType);
		// }
		return result;
	}

	private ReferenceValueTypeIF referenceValueType(EnvironmentIF environment,
			PointerTypeIF type, Map<TypeIF, ValueTypeIF> map)
			throws ExecutionException {
		TypeIF baseType = type.baseType();
		ReferenceValueTypeIF result;

		if (baseType.kind() == TypeKind.VOID) {
			result = dynamicFactory.voidPointerType();
		} else {
			ValueTypeIF baseValueType;

			result = dynamicFactory.newIncompleteReferenceValueType();
			map.put(type, result);
			baseValueType = valueType(environment, baseType, map);
			dynamicFactory.complete(result, baseValueType);
		}
		return result;
	}

	/**
	 * Uses null extent for array.
	 * 
	 * @throws ExecutionException
	 */
	private ArrayValueTypeIF arrayValueType(EnvironmentIF environment,
			ArrayTypeIF arrayType, Map<TypeIF, ValueTypeIF> map)
			throws ExecutionException {
		ValueTypeIF elementValueType = valueType(environment, arrayType
				.elementType(), map);
		ArrayValueTypeIF result = dynamicFactory.arrayValueType(
				elementValueType, (ValueIF) null);

		map.put(arrayType, result);
		return result;
	}

	/**
	 * Evaluates the dimension expressions in given environment and returns
	 * array of dimension values. If any entries are null, the corresponding
	 * entries are null in the result.
	 */
	private ValueIF[] dimensions(EnvironmentIF environment,
			ExpressionIF[] dimensionExpressions) throws ExecutionException {
		int dimension = dimensionExpressions.length;
		ValueIF[] dimensions = new ValueIF[dimension];

		for (int i = 0; i < dimension; i++) {
			ExpressionIF expression = dimensionExpressions[i];

			if (expression == null)
				continue;

			ValueIF extent = evaluate(environment, expression);
			ValueIF assumption = environment.getAssumption();

			if (extent.valueType().isInteger())
				try {
					ValueIF claim = dynamicFactory.not(assumption,
							dynamicFactory.lessThan(assumption, extent,
									dynamicFactory.zero()));
					ResultType truth = dynamicFactory.valid(assumption, claim);

					if (truth != ResultType.YES) {
						String message;
						Certainty certainty;
						ExecutionException error;

						if (truth == ResultType.MAYBE) {
							message = "Cannot prove that extent " + i
									+ " of array is nonnegative:";
							certainty = Certainty.MAYBE;
						} else {
							message = "Extent " + i
									+ " of array can be negative:";
							certainty = Certainty.PROVEABLE;
						}
						message += "\n  extent expression  : " + expression
								+ "\n        extent value : " + extent
								+ "\n      path condition : " + assumption;
						error = new ExecutionException(expression,
								ErrorKind.ARRAY_DECLARATION, certainty, message);
						log.report(error);
						environment.addAssumption(claim);
					}
				} catch (DynamicException e) {
					throw new ExecutionException(expression, e, Certainty.NONE);
				} catch (ExecutionProblem problem) {
					throw new ExecutionException(expression, problem);
				}
			dimensions[i] = extent;
		}
		return dimensions;
	}

	private ArrayValueTypeIF arrayValueType(EnvironmentIF environment,
			ArrayTypeIF arrayType, ExpressionIF[] dimensionExpressions)
			throws ExecutionException {
		ArrayValueTypeIF result = arrayValueType(environment, arrayType,
				dimensionExpressions, new HashMap<TypeIF, ValueTypeIF>());

		// result = (ArrayValueTypeIF) dynamicFactory.commit(result);
		return result;
	}

	/**
	 * Given array type and array of dimension expressions, evaluates those
	 * expressions to get array dimensions and returns corresponding rectangular
	 * dynamic array type.
	 * 
	 * @throws ExecutionException
	 */
	private ArrayValueTypeIF arrayValueType(EnvironmentIF environment,
			ArrayTypeIF arrayType, ExpressionIF[] dimensionExpressions,
			Map<TypeIF, ValueTypeIF> map) throws ExecutionException {
		ValueIF[] dimensions = dimensions(environment, dimensionExpressions);
		ValueTypeIF baseValueType = valueType(environment,
				arrayType.baseType(), map);

		ArrayValueTypeIF result = dynamicFactory.rectangularArrayValueType(
				baseValueType, dimensions);

		map.put(arrayType, result);
		return result;
	}

	public ValueIF sizeof(EnvironmentIF environment, ValueTypeIF valueType)
			throws DynamicException, ExecutionProblem {
		ValueIF result = dynamicFactory.sizeof(valueType);
		ValueIF assumption = environment.getAssumption();

		environment.addAssumption(dynamicFactory.lessThan(assumption, zero,
				result));
		return result;
	}

	private ValueIF evaluateForall(EnvironmentIF environment,
			BoundExpressionIF expression) throws ExecutionException {
		try {
			BoundVariableIF boundVariable = expression.boundVariable();
			SymbolicConstantIF symbolicConstant = dynamicFactory
					.symbolicConstantForBoundVariable(boundVariable);
			ValueIF boundConstraint = evaluate(environment, expression
					.boundRestriction());
			ValueIF assumption = environment.getAssumption();

			// TODO: need to evaluate assuming the boundConstraint holds...
			// temporarily add to assumption boundConstraint, or
			// make predicate ((!boundConstraint)||predicate)

			environment.setAssumption(dynamicFactory.and(trueValue, assumption,
					boundConstraint));

			ValueIF predicate = evaluate(environment, expression.expression());

			environment.setAssumption(assumption);

			return dynamicFactory.forall(assumption, symbolicConstant,
					boundConstraint, predicate);
		} catch (DynamicException e) {
			throw new ExecutionException(expression, e, Certainty.NONE);
		}
	}

	private ValueIF evaluateExists(EnvironmentIF environment,
			BoundExpressionIF expression) throws ExecutionException {
		try {
			ValueIF assumption = environment.getAssumption();

			return dynamicFactory.exists(assumption,
					expression.boundVariable(), evaluate(environment,
							expression.boundRestriction()), evaluate(
							environment, expression.expression()));
		} catch (DynamicException e) {
			throw new ExecutionException(expression, e, Certainty.NONE);
		}
	}

	private ValueIF evaluateLambda(EnvironmentIF environment,
			BoundExpressionIF lambda) throws ExecutionException {
		BoundVariableIF variable = lambda.boundVariable();
		ExpressionIF expression = lambda.expression();
		ValueTypeIF domainValueType = variableValueType(environment, variable);
		ValueIF lambdaAssumption = evaluate(environment, lambda
				.boundRestriction());
		ValueIF assumption = environment.getAssumption();
		ValueIF tempAssumption = dynamicFactory.and(trueValue, assumption,
				lambdaAssumption);

		environment.setAssumption(tempAssumption);

		ValueIF expressionValue = evaluate(environment, expression);

		// TODO: check assumption has not changed. if it has, go to false.

		environment.setAssumption(assumption);

		ValueIF result = dynamicFactory.lambda(assumption, domainValueType,
				dynamicFactory.symbolicConstantForBoundVariable(variable),
				expressionValue);

		return result;
	}

	public ArrayValueIF evaluateArrayLambda(EnvironmentIF environment,
			ValueIF extent, ValueIF function) throws ExecutionProblem {
		ValueIF assumption = environment.getAssumption();
		ValueTypeIF typeOfFunction = function.valueType();

		if (!extent.valueType().isInteger()) {
			throw new TASSInternalException(
					"Extent argument to array lambda must have integer type: "
							+ extent);
		}
		if (!(typeOfFunction instanceof FunctionValueTypeIF)) {
			throw new TASSInternalException(
					"Argument to evaluateArrayLambda not function: " + function);
		}

		FunctionValueTypeIF functionType = (FunctionValueTypeIF) typeOfFunction;
		ValueTypeIF elementType = functionType.returnType();

		if (functionType.numArguments() != 1) {
			throw new TASSInternalException(
					"Array lambda requires function of one variable: "
							+ function);
		}

		ValueTypeIF inputType = functionType.argumentType(0);

		if (!inputType.isInteger()) {
			throw new TASSInternalException(
					"Array lambda requires function from integers: " + function);
		}

		ArrayValueTypeIF arrayValueType = dynamicFactory.arrayValueType(
				elementType, extent);

		return dynamicFactory.arrayLambda(assumption, arrayValueType, function);
	}
}