ValueFactory.java

package edu.udel.cis.vsl.tass.dynamic.impl.value;

import java.io.PrintWriter;
import java.util.Collection;
import java.util.LinkedHashSet;
import java.util.Set;

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.cell.CellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.HeapCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.LiteralCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.LocalCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.ModelCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.ProcessCellIF;
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.type.VectorValueTypeIF;
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.dynamic.IF.value.VectorElementReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.VectorValueIF;
import edu.udel.cis.vsl.tass.dynamic.impl.cell.CellFactory;
import edu.udel.cis.vsl.tass.dynamic.impl.type.ValueType;
import edu.udel.cis.vsl.tass.dynamic.impl.type.ValueTypeFactory;
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.scope.LocalScopeIF;
import edu.udel.cis.vsl.tass.model.IF.type.RecordTypeIF;
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.morph.Morphic;
import edu.udel.cis.vsl.tass.morph.MorphicFactory;
import edu.udel.cis.vsl.tass.morph.MorphicFactoryIF;
import edu.udel.cis.vsl.tass.morph.MorphicVector;
import edu.udel.cis.vsl.tass.morph.MorphicVectorFactory;
import edu.udel.cis.vsl.tass.number.Numbers;
import edu.udel.cis.vsl.tass.number.IF.IntegerNumberIF;
import edu.udel.cis.vsl.tass.number.IF.NumberIF;
import edu.udel.cis.vsl.tass.simplify.IF.SymbolicSimplifierFactoryIF;
import edu.udel.cis.vsl.tass.simplify.IF.SymbolicSimplifierIF;
import edu.udel.cis.vsl.tass.symbolic.Symbolics;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicConstantIF;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicExpressionIF;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicUniverseIF;
import edu.udel.cis.vsl.tass.symbolic.IF.tree.TreeExpressionIF;
import edu.udel.cis.vsl.tass.symbolic.IF.type.SymbolicTupleTypeIF;
import edu.udel.cis.vsl.tass.symbolic.IF.type.SymbolicTypeIF;
import edu.udel.cis.vsl.tass.util.TASSInternalException;

/**
 * A factory used to produce values. Used by the Dynamic Factory for all value
 * creation tasks.
 */
public class ValueFactory extends MorphicFactory<ValueIF> {

	/*
	 * The following are the possible values for the "kind" field in a variable
	 * reference tuple.
	 */
	private final static int NULL = 0;
	private final static int SHARED = 1;
	private final static int PROCESS = 2;
	private final static int HEAP = 3;
	private final static int LOCAL = 4;
	private final static int LITERAL = 5;

	private RunConfiguration configuration;

	private ValueTypeIF integerType;

	private ModelFactoryIF modelFactory;

	private SymbolicExpressionIF navigatorBase;

	/** See ValueTypeFactory.referenceSymbolicTypeIF */
	private SymbolicTupleTypeIF referenceSymbolicType;

	private SymbolicExpressionIF symTrue, symZero, symOne;

	private SymbolicUniverseIF treeUniverse;

	private ValueTypeFactory typeFactory;

	private SymbolicUniverseIF universe;

	private MorphicVectorFactory<ValueIF> valueVectorFactory;

	private CellFactory cellFactory;

	/** See ValueTypeFactory.variableReferenceSymbolicTypeIF */
	private SymbolicTupleTypeIF variableReferenceSymbolicType;

	private ValueIF zero;

	private SymbolicSimplifierFactoryIF simplifierFactory;

	public ValueFactory(ValueTypeFactory typeFactory, CellFactory cellFactory,
			SymbolicUniverseIF universe,
			SymbolicSimplifierFactoryIF simplifierFactory) {
		this.typeFactory = typeFactory;
		this.cellFactory = cellFactory;
		this.universe = universe;
		this.simplifierFactory = simplifierFactory;
		this.configuration = universe.configuration();
		this.treeUniverse = Symbolics.newStandardUniverse(configuration,
				Numbers.REAL_FACTORY, universe);
		variableReferenceSymbolicType = typeFactory
				.variableReferenceSymbolicType();
		referenceSymbolicType = typeFactory.referenceSymbolicTypeIF();
		navigatorBase = universe.symbolicConstantExpression(universe
				.newSymbolicConstant("__TASS_navigatorBase__",
						universe.arrayType(universe.integerType())));
		symTrue = universe.concreteExpression(true);
		symZero = universe.zeroInt();
		symOne = universe.oneInt();
		modelFactory = typeFactory.modelFactory();
		integerType = typeFactory.integerType();
		valueVectorFactory = new MorphicVectorFactory<ValueIF>(this);
		zero = value(symZero, integerType);
	}

	public VectorValue add(VectorValueIF vector, ValueIF element) {
		VectorValue theVector = mutable(vector);

		theVector.add(element);
		return theVector;
	}

	/**
	 * Returns a reference to an element of an array. The type of the reference
	 * is just "pointer to elementType of array".
	 */
	public ArrayElementReferenceValue arrayElementReferenceValue(
			SymbolicExpressionIF assumption, ReferenceValueIF parent,
			ValueIF index) {
		ValueTypeIF elementType = elementType(assumption,
				(ArrayValueTypeIF) parent.valueType().baseType(), index);
		ReferenceValueTypeIF resultType = typeFactory
				.referenceValueType(elementType);

		return arrayElementReferenceValue(parent, index, resultType);
	}

	public ArrayElementReferenceValue arrayElementReferenceValue(
			ReferenceValueIF parent, ValueIF index) {
		return arrayElementReferenceValue(symTrue, parent, index);
	}

	/**
	 * A general way to create a reference to an array element AND specify the
	 * type of that reference. The type of the reference is allowed to be
	 * different from "reference to the element type of the array" because of
	 * casting of pointer types.
	 */
	public ArrayElementReferenceValue arrayElementReferenceValue(
			ReferenceValueIF parent, ValueIF index,
			ReferenceValueTypeIF referenceType) {
		ArrayElementReferenceValue result = new ArrayElementReferenceValue(
				parent, index, referenceType);

		return result;
	}

	public ArrayValue arrayValue(SymbolicExpressionIF origin,
			ArrayValueTypeIF valueType) {
		ArrayValue newValue = new ArrayValue(origin,
				valueVectorFactory.newVector(), valueType);

		return newValue;
	}

	public ArrayValue arrayValue(SymbolicExpressionIF origin,
			MorphicVector<ValueIF> elements, ArrayValueTypeIF valueType) {
		ArrayValue newValue = new ArrayValue(origin, elements, valueType);

		return newValue;
	}

	@Override
	protected void canonicalizeChildren(ValueIF value) {
		((Value) value).canonicalizeChildren(this, typeFactory);
	}

	public ValueIF characterValue(SymbolicExpressionIF expression) {
		Character character = null;
		NumberIF number = universe.extractNumber(expression);
		Value newValue;

		if (number instanceof IntegerNumberIF) {
			character = (char) ((IntegerNumberIF) number).intValue();
		}
		newValue = new CharacterValue(expression, typeFactory.characterType(),
				character);

		return newValue;
	}

	/**
	 * Finds all references embedded in a symbolic expression, adds them to the
	 * set references.
	 */
	private void computeReachable(SymbolicExpressionIF expression,
			Set<VariableReferenceValueIF> references) {
		computeReachableTree(universe.tree(expression), references);

	}

	private void computeReachable(ValueIF value,
			Collection<ValueIF> seenValues,
			Set<VariableReferenceValueIF> references) {
		if (seenValues.contains(value))
			return;
		seenValues.add(value);
		if (!value.valueType().containsReferences())
			return;
		if (value instanceof UndefinedValue) {
			return;
		} else if (value instanceof ReferenceValueIF) {
			if (value instanceof NullReferenceValue) {
				return;
			} else if (value instanceof VariableReferenceValueIF) {
				references.add((VariableReferenceValueIF) value);
			} else if (value instanceof ArrayElementReferenceValueIF) {
				computeReachable(
						((ArrayElementReferenceValueIF) value)
								.variableReference(),
						seenValues, references);
			} else if (value instanceof RecordElementReferenceValueIF) {
				computeReachable(
						((RecordElementReferenceValueIF) value)
								.variableReference(),
						seenValues, references);
			} else if (value instanceof VectorElementReferenceValueIF) {
				computeReachable(
						((VectorElementReferenceValueIF) value)
								.variableReference(),
						seenValues, references);
			} else {
				throw new TASSInternalException("Unknown type of reference: "
						+ value);
			}
		} else if (value instanceof ArrayValue) {
			ArrayValue array = (ArrayValue) value;
			SymbolicExpressionIF origin = array.origin();

			computeReachable(origin, references);
			for (ValueIF element : array.elements())
				if (element != null)
					computeReachable(element, seenValues, references);
		} else if (value instanceof RecordValue) {
			RecordValue record = (RecordValue) value;
			int numElements = record.numElements();

			for (int i = 0; i < numElements; i++)
				computeReachable(record.element(i), seenValues, references);
		} else if (value instanceof SymbolicValue) {
			SymbolicExpressionIF expression = ((SymbolicValue) value)
					.getSymbolicExpression();

			computeReachable(expression, references);
		} else if (value instanceof VectorValue) {
			for (ValueIF element : (VectorValue) value)
				if (element != null)
					computeReachable(element, seenValues, references);
		} else {
			throw new TASSInternalException("Unknown type of vaue: " + value);
		}

	}

	private void computeReachableTree(TreeExpressionIF tree,
			Set<VariableReferenceValueIF> references) {
		SymbolicTypeIF type = tree.type();

		if (type.equals(variableReferenceSymbolicType)) {
			SymbolicExpressionIF tuple = universe.canonicalize(tree);
			VariableReferenceValueIF reference = variableReferenceValue(
					symTrue, tuple);

			references.add(reference);
		} else {
			int numChildren = tree.numArguments();

			for (int i = 0; i < numChildren; i++)
				computeReachableTree(tree.argument(i), references);
		}
	}

	public VectorValue emptyVector(VectorValueTypeIF vectorValueType) {
		return vectorValue(0, vectorValueType);
	}

	private boolean isNullReference(SymbolicExpressionIF assumption,
			SymbolicExpressionIF variableReferenceTuple) {
		Integer kind = readIntField(assumption, variableReferenceTuple, 0);

		return kind != null && kind == NULL;
	}

	private VectorValue mutable(VectorValueIF vector) {
		VectorValue theVector = (VectorValue) vector;
		MorphicVector<ValueIF> data = theVector.data();

		if (data.isCommitted()) {
			data = valueVectorFactory.newVector(data);
			if (theVector.isCommitted()) {
				theVector = new VectorValue(data, vector.valueType());
			} else {
				theVector.setData(data);
			}
		}
		return theVector;
	}

	public NullReferenceValue nullReferenceValue(
			ReferenceValueTypeIF referenceType) {
		NullReferenceValue x = new NullReferenceValue(referenceType);

		return x;
	}

	public void printValues(PrintWriter out) {
		out.println("Values: ");
		for (Morphic value : store())
			out.println("  " + ((ValueIF) value).typedString());
		out.println();
		out.flush();
	}

	/**
	 * Given a value V and a set S of "seen" values, this method returns the set
	 * of all variable reference values that are reachable from V in zero or
	 * more steps by a path that does not go through S. In addition, this method
	 * adds to S values reachable from value by a path of 0 or more steps that
	 * does not go through S.
	 * 
	 * By "path" we mean a path in the directed graph in which the nodes are
	 * values and there is an edge from v1 to v2 if v2 "is a component of" v1.
	 * The "is a component of" relation is defined in case by case basis
	 * (depending on the kind of expression), but is pretty obvious.
	 */
	public Set<VariableReferenceValueIF> reachableVariableReferences(
			ValueIF value, Collection<ValueIF> seenValues) {
		Set<VariableReferenceValueIF> result = new LinkedHashSet<VariableReferenceValueIF>();

		computeReachable(value, seenValues, result);
		return result;
	}

	private Integer readIntField(SymbolicExpressionIF assumption,
			SymbolicExpressionIF tuple, int index) {
		SymbolicExpressionIF component = universe.tupleRead(tuple, index);
		IntegerNumberIF result = (IntegerNumberIF) universe
				.extractNumber(component);

		if (result == null)
			return null;
		return result.intValue();

	}

	public RecordElementReferenceValue recordElementReferenceValue(
			ReferenceValueIF parent, int fieldIndex) {
		ValueTypeIF elementType = ((RecordValueTypeIF) parent.valueType()
				.baseType()).fieldType(fieldIndex);
		ReferenceValueTypeIF resultType = typeFactory
				.referenceValueType(elementType);

		return recordElementReferenceValue(parent, fieldIndex, resultType);
	}

	public RecordElementReferenceValue recordElementReferenceValue(
			ReferenceValueIF parent, int fieldIndex,
			ReferenceValueTypeIF referenceType) {
		RecordElementReferenceValue result = new RecordElementReferenceValue(
				parent, fieldIndex, referenceType);

		return result;
	}

	private RecordValueIF recordValue(SymbolicExpressionIF assumption,
			SymbolicExpressionIF symExpression,
			RecordValueTypeIF recordDynamicType) {
		RecordTypeIF recordType = recordDynamicType.type();
		int numFields = recordType.numFields();
		ValueIF[] elements = new ValueIF[numFields];
		RecordValue result;

		for (int i = 0; i < numFields; i++) {
			SymbolicExpressionIF symElement = universe.tupleRead(symExpression,
					i);
			ValueTypeIF fieldType = recordDynamicType.fieldType(i);

			elements[i] = value(assumption, symElement, fieldType);
		}
		result = recordValue(elements, recordDynamicType);
		result.commit();
		if (result.getSymbolicExpression() == null)
			result.setSymbolicExpression(symExpression); // why not?
		return result;
	}

	public RecordValue recordValue(ValueIF[] elements,
			RecordValueTypeIF recordType) {
		RecordValue x = new RecordValue(elements, recordType);

		return x;
	}

	/**
	 * Returns null if fields in tuple are not concrete enough.
	 * 
	 */
	private ReferenceValueIF referenceValue(SymbolicExpressionIF assumption,
			SymbolicExpressionIF tuple) {
		SymbolicExpressionIF variableReferenceTuple = universe.tupleRead(tuple,
				0);

		if (isNullReference(assumption, variableReferenceTuple)) {
			Integer dynamicTypeId = readIntField(assumption,
					variableReferenceTuple, 6);
			ReferenceValueTypeIF referenceType = (ReferenceValueTypeIF) typeFactory
					.dynamicType(dynamicTypeId);

			return nullReferenceValue(referenceType);
		}

		VariableReferenceValueIF variableReference = variableReferenceValue(
				assumption, variableReferenceTuple);

		if (variableReference == null)
			return null;

		int numNavigators;

		{
			Integer tmp = readIntField(assumption, tuple, 1);

			if (tmp == null)
				return null;
			numNavigators = tmp;
		}

		SymbolicExpressionIF navigators = universe.tupleRead(tuple, 2);
		ReferenceValueIF result = variableReference;

		for (int i = 0; i < numNavigators; i++) {
			ReferenceValueTypeIF dynamicType = result.valueType();
			ValueTypeIF baseType = dynamicType.baseType();
			SymbolicExpressionIF index = universe.concreteExpression(i);
			SymbolicExpressionIF navigator = universe.arrayRead(navigators,
					index);

			if (baseType instanceof RecordValueTypeIF) {
				int fieldIndex = ((IntegerNumberIF) universe
						.extractNumber(navigator)).intValue();
				result = recordElementReferenceValue(result, fieldIndex);
			} else if (baseType instanceof ArrayValueTypeIF) {
				result = arrayElementReferenceValue(assumption, result,
						symbolicValue(assumption, navigator, integerType));
			} else {
				throw new TASSInternalException(
						"Unknown kind of structured datatype: " + baseType);
			}
		}
		return result;
	}

	public VectorValue removeElementAt(VectorValueIF vector, int position)
			throws DynamicException {
		VectorValue theVector = mutable(vector);

		theVector.removeElementAt(position);
		return theVector;
	}

	/**
	 * Sets an array element to the given value. The array may or may not be
	 * committed. If committed, a new array value is created.
	 */
	public ArrayValue setArrayElement(ArrayValue array, int index, ValueIF value) {
		MorphicVector<ValueIF> elements = array.elements();

		if (!elements.isCommitted()) {
			elements.setExtend(index, value);
		} else {
			elements = valueVectorFactory.newVector(elements);
			elements.setExtend(index, value);
			if (!array.isCommitted()) {
				array.setElements(elements);
			} else {
				array = arrayValue(array.origin(), elements, array.valueType());
			}
		}
		return array;
	}

	public VectorValue setExtend(VectorValueIF vector, int index, ValueIF value) {
		VectorValue theVector = mutable(vector);

		theVector.setExtend(index, value);
		return theVector;
	}

	public RecordValue setRecordElement(RecordValueIF record, int index,
			ValueIF value) {
		if (record.isCommitted()) {
			ValueIF[] oldElements = ((RecordValue) record).elements();
			int numElements = oldElements.length;
			ValueIF[] newElements = new ValueIF[numElements];

			for (int i = 0; i < index; i++)
				newElements[i] = oldElements[i];
			newElements[index] = value;
			for (int i = index + 1; i < numElements; i++)
				newElements[i] = oldElements[i];
			return recordValue(newElements, record.valueType());
		} else {
			record.setElement(index, value);
			return (RecordValue) record;
		}
	}

	public VectorValue setSize(VectorValueIF vector, int newSize) {
		VectorValue theVector = mutable(vector);

		theVector.setSize(newSize);
		return theVector;
	}

	public Value symbolicValue(SymbolicExpressionIF expression,
			ValueTypeIF valueType) {
		return symbolicValue(symTrue, expression, valueType);
	}

	public Value symbolicValue(SymbolicExpressionIF assumption,
			SymbolicExpressionIF expression, ValueTypeIF valueType) {
		Value newValue;

		assert expression != null;
		assert valueType != null;
		if (valueType instanceof ArrayValueTypeIF) {
			SymbolicExpressionIF originExpression = universe
					.getArrayOrigin(expression);
			SymbolicExpressionIF[] elementExpressions = universe
					.getArrayElements(expression);
			int numElements = elementExpressions.length;
			MorphicVector<ValueIF> elements = valueVectorFactory
					.newVector(numElements);

			ArrayValueTypeIF arrayValueType = (ArrayValueTypeIF) valueType;
			int dimension = arrayValueType.dimension();
			ValueTypeIF baseType = arrayValueType.baseType();

			if (dimension == 1) {
				for (int i = 0; i < numElements; i++) {
					SymbolicExpressionIF elementExpression = elementExpressions[i];

					if (elementExpression != null)
						elements.set(
								i,
								symbolicValue(assumption, elementExpression,
										baseType));
				}
			} else {
				for (int i = 0; i < numElements; i++) {
					SymbolicExpressionIF elementExpression = elementExpressions[i];
					ValueTypeIF elementType = elementType(assumption,
							arrayValueType, intValue(i));

					if (elementExpression != null)
						elements.set(
								i,
								symbolicValue(assumption, elementExpression,
										elementType));
				}
			}
			newValue = new ArrayValue(originExpression, elements,
					(ArrayValueTypeIF) valueType);
			// TODO: instead of this, get the origin and elements from the
			// symbolic array and use them here...trying it now....

			// TODO: add similar clause for function, lambda, array
			// lambda,...????

		} else {
			newValue = new SymbolicValue(expression, valueType);
		}

		return newValue;
	}

	private ValueIF intValue(int n) {
		return new SymbolicValue(universe.concreteExpression(n),
				this.integerType);
	}

	/**
	 * Returns a symbolic representation of an array value.
	 */
	private SymbolicExpressionIF symExpression(SymbolicExpressionIF assumption,
			ArrayValue array) {
		SymbolicExpressionIF symExpression = array.getSymbolicExpression();

		if (symExpression == null) {
			MorphicVector<ValueIF> elements = array.elements();
			int numElements = elements.size();

			if (numElements == 0) {
				return array.origin();
			}

			SymbolicExpressionIF[] elementExpressions = new SymbolicExpressionIF[numElements];

			for (int i = 0; i < numElements; i++) {
				ValueIF element = elements.get(i);
				if (element != null) {
					SymbolicExpressionIF symElement = symExpression(assumption,
							element);

					elementExpressions[i] = symElement;
				}
			}
			symExpression = universe.arrayExpression(array.origin(),
					elementExpressions);
			array.commit(); // in order to cache symExpression, need this
			array.setSymbolicExpression(symExpression);
		}
		return symExpression;
	}

	/**
	 * Returns a symbolic representation of a record value.
	 */
	private SymbolicExpressionIF symExpression(SymbolicExpressionIF assumption,
			RecordValue record) {
		SymbolicExpressionIF symExpression;

		RecordValueTypeIF recordDynamicType = record.valueType();
		SymbolicTupleTypeIF symRecordType = (SymbolicTupleTypeIF) typeFactory
				.symType(recordDynamicType);
		RecordTypeIF recordType = recordDynamicType.type();
		int numFields = recordType.numFields();
		SymbolicExpressionIF[] symElements = new SymbolicExpressionIF[numFields];

		for (int i = 0; i < numFields; i++) {
			symElements[i] = symExpression(assumption, record.element(i));
		}
		symExpression = universe.tupleExpression(symRecordType, symElements);
		return symExpression;
	}

	/**
	 * Returns a symbolic representation of a reference value.
	 */
	private SymbolicExpressionIF symExpression(SymbolicExpressionIF assumption,
			ReferenceValue reference) {
		SymbolicExpressionIF symExpression;

		SymbolicExpressionIF symVariableReference;
		SymbolicExpressionIF numNavigators;
		SymbolicExpressionIF navigators;

		if (reference instanceof NullReferenceValue) {
			int dynamicTypeId = typeFactory.canonic(
					(ValueType) reference.valueType()).canonicalId();
			SymbolicExpressionIF[] tupleElements = new SymbolicExpressionIF[] {
					universe.concreteExpression(NULL),
					universe.concreteExpression(-1),
					universe.concreteExpression(-1),
					universe.concreteExpression(-1),
					universe.concreteExpression(-1),
					universe.concreteExpression(-1),
					universe.concreteExpression(-1),
					universe.concreteExpression(dynamicTypeId) };
			symVariableReference = universe.tupleExpression(
					variableReferenceSymbolicType, tupleElements);
			numNavigators = symZero;
			navigators = navigatorBase;
		} else if (reference instanceof VariableReferenceValueIF) {
			int dynamicTypeId = typeFactory.canonic(
					(ValueType) reference.valueType()).canonicalId();
			VariableReferenceValueIF variableReference = (VariableReferenceValueIF) reference;
			CellIF dynamicVariable = variableReference.variable();
			int kind, processId, functionId, stackPosition, scopeId, variableId, modelId;

			if (dynamicVariable instanceof ModelCellIF) {
				modelId = ((ModelCellIF) dynamicVariable).model().id();
			} else {
				modelId = -1;
			}
			switch (dynamicVariable.scope()) {
			case SHARED: {
				processId = -1;
				variableId = ((SharedCellIF) dynamicVariable)
						.sharedVariableId();
				functionId = -1;
				stackPosition = -1;
				scopeId = -1;
				kind = SHARED;
				break;
			}
			case PROCESS: {
				ProcessVariableIF variable = ((ProcessCellIF) dynamicVariable)
						.variable();

				processId = variable.scope().process().pid();
				variableId = variable.idInScope();
				functionId = -1;
				stackPosition = -1;
				scopeId = -1;
				kind = PROCESS;
				break;
			}
			case LOCAL: {
				LocalCellIF localVariable = (LocalCellIF) dynamicVariable;
				LocalVariableIF variable = localVariable.variable();
				LocalScopeIF scope = variable.scope();
				FunctionIF function = scope.function();

				kind = LOCAL;
				scopeId = scope.localId();
				variableId = localVariable.localID();
				functionId = function.idInScope();
				stackPosition = localVariable.stackIndex();
				processId = function.process().pid();
				break;
			}
			case HEAP: {
				HeapCellIF heapVariable = (HeapCellIF) dynamicVariable;

				kind = HEAP;
				variableId = heapVariable.heapIndex();
				functionId = -1;
				stackPosition = -1;
				scopeId = -1;
				processId = heapVariable.process().pid();
				break;
			}
			case LITERAL: {
				kind = LITERAL;
				variableId = (((LiteralCellIF) dynamicVariable).expression()
						.objectLiteralID());
				functionId = -1;
				stackPosition = -1;
				processId = -1;
				scopeId = -1;
			}
			default:
				throw new TASSInternalException("Unknown dynamic scope: "
						+ dynamicVariable.scope());
			}
			SymbolicExpressionIF[] tupleElements = new SymbolicExpressionIF[] {
					universe.concreteExpression(kind),
					universe.concreteExpression(modelId),
					universe.concreteExpression(processId),
					universe.concreteExpression(functionId),
					universe.concreteExpression(stackPosition),
					universe.concreteExpression(scopeId),
					universe.concreteExpression(variableId),
					universe.concreteExpression(dynamicTypeId) };
			symVariableReference = universe.tupleExpression(
					variableReferenceSymbolicType, tupleElements);
			numNavigators = symZero;
			navigators = navigatorBase;
		} else { // parent not null
			ReferenceValueIF parent = reference.parent();
			SymbolicExpressionIF parentExpression = symExpression(assumption,
					parent);
			SymbolicExpressionIF parentNumNavigators = universe.tupleRead(
					parentExpression, 1);
			SymbolicExpressionIF parentNavigators = universe.tupleRead(
					parentExpression, 2);
			SymbolicExpressionIF newNavigator;

			symVariableReference = universe.tupleRead(parentExpression, 0);
			numNavigators = universe.add(parentNumNavigators, symOne);
			if (reference instanceof ArrayElementReferenceValueIF) {
				newNavigator = ((SymbolicValue) ((ArrayElementReferenceValueIF) reference)
						.index()).getSymbolicExpression();
			} else if (reference instanceof RecordElementReferenceValueIF) {
				newNavigator = universe
						.concreteExpression(((RecordElementReferenceValueIF) reference)
								.fieldIndex());
			} else {
				throw new TASSInternalException("Unknown reference kind:\n"
						+ reference);
			}
			navigators = universe.arrayWrite(parentNavigators,
					parentNumNavigators, newNavigator);
		}
		symExpression = universe.tupleExpression(referenceSymbolicType,
				new SymbolicExpressionIF[] { symVariableReference,
						numNavigators, navigators });
		return symExpression;
	}

	/** Returns a symbolic representation of a value. */
	// would it better to insist that the value is canonic before this is
	// called?
	public SymbolicExpressionIF symExpression(SymbolicExpressionIF assumption,
			ValueIF value) {
		value = (Value) canonic(value);

		SymbolicExpressionIF symbolicExpression = ((Value) value)
				.getSymbolicExpression();

		if (symbolicExpression == null) {
			if (value instanceof ReferenceValue) {
				symbolicExpression = symExpression(assumption,
						(ReferenceValue) value);
			} else if (value instanceof RecordValue) {
				symbolicExpression = symExpression(assumption,
						(RecordValue) value);
			} else if (value instanceof ArrayValue) {
				symbolicExpression = symExpression(assumption,
						(ArrayValue) value);
			} else if (value instanceof VectorValue) {
				symbolicExpression = symExpression(assumption,
						(VectorValue) value);
			} else {
				// should not be able to happen
				throw new TASSInternalException(
						"Unable to extract symbolic expression from value:\n"
								+ value);
			}
			((Value) value).setSymbolicExpression(symbolicExpression);
		}
		return symbolicExpression;
	}

	/**
	 * Returns symbolic representation of a vector. The vector is represented as
	 * tuple (size,a), where size is a concrete integer symbolic expression (the
	 * size of the vector), and a is a symbolic array containing the elements of
	 * the vector. The array has as its origin a symbolic constant named "EMPTY"
	 * (there exists one for each type).
	 */
	private SymbolicExpressionIF symExpression(SymbolicExpressionIF assumption,
			VectorValue vector) {
		VectorValueTypeIF valueType = vector.valueType();
		SymbolicTupleTypeIF symType = (SymbolicTupleTypeIF) typeFactory
				.symType(valueType);
		SymbolicConstantIF symbolicConstant = universe
				.getOrCreateSymbolicConstant("EMPTY", symType);
		SymbolicExpressionIF origin = universe
				.symbolicConstantExpression(symbolicConstant);
		int numElements = vector.size();
		SymbolicExpressionIF sizeSymExpression = universe
				.concreteExpression(numElements);
		SymbolicExpressionIF[] elements = new SymbolicExpressionIF[numElements];
		SymbolicExpressionIF symArray, result;

		try {
			for (int i = 0; i < numElements; i++)
				elements[i] = symExpression(vector.get(i));
		} catch (DynamicException e) {
			throw new TASSInternalException(
					"Should not happen as i is in bounds:\n" + e);
		}
		symArray = universe.arrayExpression(origin, elements);
		result = universe.tupleExpression(symType, new SymbolicExpressionIF[] {
				sizeSymExpression, symArray });
		return result;
	}

	public SymbolicExpressionIF symExpression(ValueIF value) {
		return symExpression(symTrue, value);
	}

	public SymbolicExpressionIF symTrue() {
		return symTrue;
	}

	public SymbolicUniverseIF treeUniverse() {
		return treeUniverse;
	}

	public MorphicFactoryIF<ValueTypeIF> typeFactory() {
		return typeFactory;
	}

	public ValueIF undefinedValue(ValueTypeIF type) {
		ValueType theType = (ValueType) type;
		ValueIF result = theType.getUndefinedValue();

		if (result == null) {
			result = canonic(new UndefinedValue(type));

			if (theType.isCommitted())
				theType.setUndefinedValue(result);
		}
		return result;
	}

	// WANT: all ReferenceValues "reachable" from a set of value.
	// two kinds of reach: values which are components of other values
	// de-referenceing , which requires the state.
	// value package is good at first kind, ModelEnvironment at second kind.

	// two different kinds of edges: value and dereference
	// here are all values you haven't seen before
	// loop through these and dereference any that are references, add cells to
	// set
	// pass these new values back to value factory, repeat until no new.

	// Graph: nodes are values. Two kinds of edges. Do DFS.

	// parent edge: a reference value has a parent; this is a value edge.

	public SymbolicUniverseIF universe() {
		return universe;
	}

	/**
	 * Returns the instance of ValueIF corresponding to a symbolic expression.
	 * The value type must also be specified.
	 */
	public ValueIF value(SymbolicExpressionIF assumption,
			SymbolicExpressionIF symExpression, ValueTypeIF dynamicType) {
		ValueIF result;

		if (dynamicType.isChar()) {
			result = characterValue(symExpression);
		} else if (dynamicType instanceof PrimitiveValueTypeIF
				|| dynamicType instanceof ArrayValueTypeIF
				|| dynamicType instanceof FunctionValueTypeIF) {
			result = symbolicValue(assumption, symExpression, dynamicType);
		} else if (dynamicType instanceof ReferenceValueTypeIF) {
			result = referenceValue(assumption, symExpression);
			if (result == null)
				result = undefinedValue(dynamicType);
		} else if (dynamicType instanceof RecordValueTypeIF) {
			result = recordValue(assumption, symExpression,
					(RecordValueTypeIF) dynamicType);
		} else {
			throw new TASSInternalException("Unknown dynamic type: "
					+ dynamicType);
		}
		return result;
	}

	public ValueIF value(SymbolicExpressionIF symExpression,
			ValueTypeIF dynamicType) {
		return value(symTrue, symExpression, dynamicType);
	}

	public MorphicVectorFactory<ValueIF> valueVectorFactory() {
		return valueVectorFactory;
	}

	public VariableReferenceValue variableReferenceValue(CellIF variable,
			ReferenceValueTypeIF type, ValueIF offset) {
		VariableReferenceValue x = new VariableReferenceValue(variable, type,
				offset);

		return x;
	}

	/**
	 * Will return null if tuple can not be concretized.
	 * 
	 * <ol>
	 * <li>0. kind
	 * <li>1. modelId
	 * <li>2. processId
	 * <li>3. functionId
	 * <li>4. stackPosition
	 * <li>5. scopeId
	 * <li>6. variableId
	 * <li>7. referenceTypeId
	 * <ol>
	 * 
	 * */
	private VariableReferenceValueIF variableReferenceValue(
			SymbolicExpressionIF assumption, SymbolicExpressionIF tuple) {
		int kind, modelId, variableId, dynamicTypeId;

		{
			Integer tmp = readIntField(assumption, tuple, 0);

			if (tmp == null)
				return null;
			kind = tmp;
		}
		{
			Integer tmp = readIntField(assumption, tuple, 1);

			if (tmp == null)
				return null;
			modelId = tmp;
		}
		{
			Integer tmp = readIntField(assumption, tuple, 6);

			if (tmp == null)
				return null;
			variableId = tmp;
		}
		{
			Integer tmp = readIntField(assumption, tuple, 7);

			if (tmp == null)
				return null;
			dynamicTypeId = tmp;
		}

		ReferenceValueTypeIF referenceType = (ReferenceValueTypeIF) typeFactory
				.dynamicType(dynamicTypeId);
		ModelIF model = modelFactory.getModel(modelId);
		CellIF dynamicVariable;
		VariableReferenceValueIF reference;

		if (kind == SHARED) {
			dynamicVariable = cellFactory.sharedCell(model.scope()
					.variableWithId(variableId));
		} else {
			int processId = readIntField(assumption, tuple, 2);
			ProcessIF process = model.process(processId);

			if (kind == PROCESS) {
				dynamicVariable = cellFactory.processCell(process.scope()
						.variableWithId(variableId));
			} else if (kind == LOCAL) {
				int functionId = readIntField(assumption, tuple, 3);
				int stackPosition = readIntField(assumption, tuple, 4);
				int scopeId = readIntField(assumption, tuple, 5);
				FunctionIF function = process.scope()
						.functionWithId(functionId);
				LocalScopeIF scope = function.scope(scopeId);
				LocalVariableIF local = scope.variableWithId(variableId);

				dynamicVariable = cellFactory.dynamicLocalVariable(local,
						stackPosition);
			} else if (kind == HEAP) {
				dynamicVariable = cellFactory.dynamicHeapVariable(process,
						variableId);
			} else {
				throw new TASSInternalException("Unknown variable kind code: "
						+ kind);
			}
		}
		reference = variableReferenceValue(dynamicVariable, referenceType, zero);
		return reference;
	}

	public VectorElementReferenceValue vectorElementReferenceValue(
			ReferenceValueIF parent, int index) {
		ValueTypeIF elementType = ((VectorValueTypeIF) parent.valueType()
				.baseType()).elementType();
		ReferenceValueTypeIF resultType = typeFactory
				.referenceValueType(elementType);

		return vectorElementReferenceValue(parent, index, resultType);
	}

	public VectorElementReferenceValue vectorElementReferenceValue(
			ReferenceValueIF parent, int index,
			ReferenceValueTypeIF referenceType) {
		VectorElementReferenceValue result = new VectorElementReferenceValue(
				parent, index, referenceType);

		return result;
	}

	public VectorValue vectorValue(MorphicVector<ValueIF> data,
			VectorValueTypeIF vectorValueType) {
		VectorValue newValue = new VectorValue(data, vectorValueType);

		return newValue;
	}

	public VectorValue vectorValue(int size, VectorValueTypeIF vectorValueType) {
		return vectorValue(valueVectorFactory.newVector(size), vectorValueType);
	}

	public NumberIF numericValue(SymbolicExpressionIF assumption, ValueIF value) {
		if (value instanceof SymbolicValue) {
			SymbolicExpressionIF symValue = ((SymbolicValue) value)
					.getSymbolicExpression();
			NumberIF number = universe.extractNumber(symValue);

			if (number != null) {
				return number;
			} else {
				SymbolicSimplifierIF simplifier = simplifierFactory
						.simplifier(assumption);

				symValue = simplifier.simplify(symValue);
				number = universe.extractNumber(symValue);
				if (number != null)
					return number;
			}
		}
		return null;
	}

	public ValueIF arrayRead(SymbolicExpressionIF assumption,
			ArrayValueIF array, ValueIF index) {
		ArrayValue arrayValue = (ArrayValue) array;

		IntegerNumberIF indexNumber = (IntegerNumberIF) numericValue(
				assumption, index);

		if (indexNumber != null) {
			int indexInt = indexNumber.intValue();
			MorphicVector<ValueIF> elements = arrayValue.elements();

			if (indexInt < elements.size() && elements.get(indexInt) != null)
				return elements.get(indexInt);
			else {
				SymbolicExpressionIF origin = arrayValue.origin();
				SymbolicExpressionIF symIndex = symExpression(index);
				SymbolicExpressionIF symResult = universe.arrayRead(origin,
						symIndex);
				ValueTypeIF elementType = elementType(assumption,
						array.valueType(), index);

				return value(assumption, symResult, elementType);
			}
		}
		return arrayReadSymbolic(assumption, arrayValue, index);
	}

	private ValueIF arrayReadSymbolic(SymbolicExpressionIF assumption,
			ArrayValueIF array, ValueIF index) {
		SymbolicExpressionIF symArray = symExpression(array);
		SymbolicExpressionIF symIndex = symExpression(index);
		SymbolicExpressionIF symResult = universe.arrayRead(symArray, symIndex);
		ValueTypeIF elementType = elementType(assumption, array.valueType(),
				index);

		return value(assumption, symResult, elementType);
	}

	/**
	 * Given R=(d,T,L), d>=1, and integer i, define
	 * <ul>
	 * <li>elementType(R,i) = T, if d=1
	 * <li>elementType(R,i) = (d-1,T,L[i]), if d>1.
	 * </ul>
	 */
	public ValueTypeIF elementType(SymbolicExpressionIF assumption,
			ArrayValueTypeIF arrayValueType, ValueIF index) {
		int dimension = arrayValueType.dimension();
		ValueTypeIF baseType = arrayValueType.baseType();

		if (dimension == 1) {
			return baseType;
		} else {
			ArrayValueIF lengths = (ArrayValueIF) arrayValueType.lengthVector();
			ValueIF elementLengths = arrayRead(assumption, lengths, index);

			return typeFactory.arrayValueType(baseType, elementLengths);
		}
	}

	// array value that is not instanceof ArrayValue
	// symbolic value....ok .... origin....
	public ArrayValue arrayLambda(ValueIF lambdaValue) {
		// TODO
		return null;
	}

	public Value lambdaValue() {
		// TODO
		return null;
	}
}