DynamicFactory.java

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

import java.io.PrintWriter;
import java.util.Collection;
import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.Vector;

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.DynamicException.DynamicErrorKind;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicFactoryIF;
import edu.udel.cis.vsl.tass.dynamic.IF.ValueSubstituterIF;
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.ProcessCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.SharedCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.simplify.DynamicSimplifierIF;
import edu.udel.cis.vsl.tass.dynamic.IF.simplify.MorphicSimplifierCacheIF;
import edu.udel.cis.vsl.tass.dynamic.IF.simplify.MorphicSimplifierIF;
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.MessageIF;
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.simplify.ArraySimplifier;
import edu.udel.cis.vsl.tass.dynamic.impl.simplify.DynamicSimplifier;
import edu.udel.cis.vsl.tass.dynamic.impl.simplify.ReferenceSimplifier;
import edu.udel.cis.vsl.tass.dynamic.impl.simplify.SetSimplifier;
import edu.udel.cis.vsl.tass.dynamic.impl.simplify.SimpleCache;
import edu.udel.cis.vsl.tass.dynamic.impl.simplify.SimplifyCache;
import edu.udel.cis.vsl.tass.dynamic.impl.simplify.SubstitutionSimplifier;
import edu.udel.cis.vsl.tass.dynamic.impl.simplify.VectorSimplifier;
import edu.udel.cis.vsl.tass.dynamic.impl.type.ValueTypeFactory;
import edu.udel.cis.vsl.tass.dynamic.impl.value.ArrayValue;
import edu.udel.cis.vsl.tass.dynamic.impl.value.MessageFactory;
import edu.udel.cis.vsl.tass.dynamic.impl.value.SymbolicValue;
import edu.udel.cis.vsl.tass.dynamic.impl.value.UndefinedValue;
import edu.udel.cis.vsl.tass.dynamic.impl.value.ValueExplorer;
import edu.udel.cis.vsl.tass.dynamic.impl.value.ValueFactory;
import edu.udel.cis.vsl.tass.dynamic.impl.value.ValueSubstituter;
import edu.udel.cis.vsl.tass.dynamic.impl.value.VectorValue;
import edu.udel.cis.vsl.tass.model.IF.AbstractFunctionIF;
import edu.udel.cis.vsl.tass.model.IF.ModelFactoryIF;
import edu.udel.cis.vsl.tass.model.IF.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ObjectLiteralExpressionIF;
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.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.morph.Morphic;
import edu.udel.cis.vsl.tass.morph.MorphicArray;
import edu.udel.cis.vsl.tass.morph.MorphicArrayFactory;
import edu.udel.cis.vsl.tass.morph.MorphicFactoryIF;
import edu.udel.cis.vsl.tass.morph.MorphicList;
import edu.udel.cis.vsl.tass.morph.MorphicListFactory;
import edu.udel.cis.vsl.tass.morph.MorphicSet;
import edu.udel.cis.vsl.tass.morph.MorphicSetFactory;
import edu.udel.cis.vsl.tass.morph.MorphicVector;
import edu.udel.cis.vsl.tass.morph.MorphicVectorFactory;
import edu.udel.cis.vsl.tass.number.IF.IntegerNumberIF;
import edu.udel.cis.vsl.tass.number.IF.IntervalIF;
import edu.udel.cis.vsl.tass.number.IF.NumberFactoryIF;
import edu.udel.cis.vsl.tass.number.IF.NumberIF;
import edu.udel.cis.vsl.tass.prove.IF.TheoremProverException;
import edu.udel.cis.vsl.tass.prove.IF.TheoremProverIF;
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.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.SymbolicArrayTypeIF;
import edu.udel.cis.vsl.tass.symbolic.IF.type.SymbolicCompleteArrayTypeIF;
import edu.udel.cis.vsl.tass.symbolic.IF.type.SymbolicFunctionTypeIF;
import edu.udel.cis.vsl.tass.symbolic.IF.type.SymbolicTypeIF;
import edu.udel.cis.vsl.tass.symbolic.IF.type.SymbolicTypeIF.SymbolicTypeKind;
import edu.udel.cis.vsl.tass.util.TASSInternalException;
import edu.udel.cis.vsl.tass.util.TernaryResult.ResultType;

public class DynamicFactory implements DynamicFactoryIF {

	private static int factoryCount = 0;

	public static int QUANTIFIER_EXPANSION_THRESHOLD = 200;

	private SymbolicTypeIF booleanSymbolicTypeIF, integerSymbolicTypeIF,
			realSymbolicTypeIF;

	private ValueTypeIF booleanValueType, characterValueType, integerValueType,
			realValueType;

	private CellFactory cellFactory;

	private RunConfiguration configuration;

	Map<ArrayValueTypeIF, SymbolicExpressionIF> emptyArrayCache = new HashMap<ArrayValueTypeIF, SymbolicExpressionIF>();

	private ValueExplorer explorer;

	private ValueIF falseValue, trueValue, zero, one;

	private int id;

	private MessageFactory messageFactory;

	private MorphicSimplifierIF<MessageIF> messageSimplifier;

	private MorphicVectorFactory<MessageIF> messageVectorFactory;

	private MorphicSimplifierIF<MorphicVector<MessageIF>> messageVectorSimplifier;

	private ModelFactoryIF modelFactory;

	private DynamicSimplifierIF noAssumptionSimplifier;

	private NumberFactoryIF numberFactory;

	private int numValidCalls = 0;

	private IntegerNumberIF ONE;

	private PrintWriter out;

	private TheoremProverIF prover;

	private IntegerNumberIF quantifierExpansionThreshold;

	private Map<Query, ResultType> queryCache = new LinkedHashMap<Query, ResultType>();

	private boolean showQueries;

	private Map<ValueIF, DynamicSimplifierIF> simplifierCache = new HashMap<ValueIF, DynamicSimplifierIF>();

	private SymbolicSimplifierFactoryIF simplifierFactory;

	private boolean simplify;

	private MorphicSimplifierCacheIF simplifyCache = new SimplifyCache();

	private ValueIF sizeofFunction;

	private SymbolicExpressionIF trueExpression, falseExpression;

	private ValueTypeFactory typeFactory;

	private SymbolicUniverseIF universe;

	private boolean useConcreteArrays;

	private MorphicArrayFactory<ValueIF> valueArrayFactory;

	private MorphicSimplifierIF<MorphicArray<ValueIF>> valueArraySimplifier;

	private ValueFactory valueFactory;

	private MorphicSimplifierIF<ValueIF> valueSimplifier;

	private MorphicVectorFactory<ValueIF> valueVectorFactory;

	private MorphicSimplifierIF<MorphicVector<ValueIF>> valueVectorSimplifier;

	private ReferenceValueTypeIF voidPointerType;

	public DynamicFactory(ModelFactoryIF modelFactory,
			SymbolicSimplifierFactoryIF simplifierFactory,
			TheoremProverIF prover, RunConfiguration configuration) {
		this.configuration = configuration;
		this.out = configuration.out();
		this.showQueries = configuration.showQueries()
				|| configuration.verbose();
		this.simplify = configuration.simplify();
		this.numberFactory = modelFactory.numberFactory();
		ONE = numberFactory.oneInteger();
		this.prover = prover;
		this.simplifierFactory = simplifierFactory;
		id = factoryCount;
		factoryCount++;
		universe = prover.universe();
		if (configuration.verbose()) {
			configuration.out().println("Creating dynamic factory " + id);
			configuration.out().flush();
		}
		this.trueExpression = universe.concreteExpression(true);
		this.falseExpression = universe.concreteExpression(false);
		useConcreteArrays = configuration.useConcreteArrays();
		this.modelFactory = modelFactory;
		this.typeFactory = new ValueTypeFactory(modelFactory, universe);
		this.cellFactory = new CellFactory();
		this.valueFactory = new ValueFactory(typeFactory, cellFactory,
				universe, simplifierFactory);
		this.valueArrayFactory = new MorphicArrayFactory<ValueIF>(valueFactory);
		this.valueVectorFactory = valueFactory.valueVectorFactory();
		typeFactory.setValueFactory(valueFactory);
		this.messageFactory = new MessageFactory(valueFactory);
		this.messageVectorFactory = new MorphicVectorFactory<MessageIF>(
				messageFactory);
		booleanSymbolicTypeIF = universe.booleanType();
		integerSymbolicTypeIF = universe.integerType();
		realSymbolicTypeIF = universe.realType();
		booleanValueType = typeFactory.booleanType();
		characterValueType = typeFactory.characterType();
		integerValueType = typeFactory.integerType();
		realValueType = typeFactory.realType();
		voidPointerType = typeFactory.voidPointerType();
		trueValue = canonic(valueFactory.symbolicValue(trueExpression,
				trueExpression, booleanValueType));
		falseValue = canonic(valueFactory.symbolicValue(trueExpression,
				falseExpression, booleanValueType));
		zero = symbolicValue(0);
		one = symbolicValue(1);
		try {
			sizeofFunction = function(trueValue,
					modelFactory.sizeofAbstractFunction(),
					new ValueTypeIF[] { integerValueType }, integerValueType);
		} catch (DynamicException e) {
			throw new TASSInternalException(e.toString());
		}
		this.explorer = new ValueExplorer(universe);
		this.valueSimplifier = new MorphicSimplifierIF<ValueIF>() {
			@Override
			public ValueIF simplify(DynamicSimplifierIF dynamicSimplifier,
					ValueIF value) throws DynamicException {
				return dynamicSimplifier.simplify(value);
			}
		};
		this.valueArraySimplifier = newArraySimplifier(valueArrayFactory,
				valueSimplifier);
		this.valueVectorSimplifier = newVectorSimplifier(valueVectorFactory,
				valueSimplifier);
		this.messageSimplifier = new MorphicSimplifierIF<MessageIF>() {
			@Override
			public MessageIF simplify(DynamicSimplifierIF dynamicSimplifier,
					MessageIF message) throws DynamicException {
				return dynamicSimplifier.simplify(message);
			}
		};
		this.messageVectorSimplifier = newVectorSimplifier(
				messageVectorFactory, messageSimplifier);
		this.noAssumptionSimplifier = new DynamicSimplifier(this, trueValue,
				simplifyCache);
		simplifierCache.put(trueValue, noAssumptionSimplifier);
		this.quantifierExpansionThreshold = numberFactory
				.integer(QUANTIFIER_EXPANSION_THRESHOLD);
	}

	@Override
	public ValueIF add(ValueIF assumption, ValueIF left, ValueIF right) {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.add(arg1, arg2);
		ValueTypeIF valueType = (left.valueType().equals(integerValueType)
				&& right.valueType().equals(integerValueType) ? integerValueType
				: realValueType);

		return valueFactory.value(predicate, result, valueType);
	}

	/** Appends element to vector, incrementing size by 1. */
	@Override
	public VectorValue add(VectorValueIF vector, ValueIF element)
			throws DynamicException {
		if (!vector.valueType().elementType().equals(element.valueType())) {
			throw new DynamicException(DynamicErrorKind.INTERNAL,
					"Attempt to add element to vector of incompatible type:\n"
							+ "  vector type: " + vector.valueType()
							+ "\n  element: " + element + " ("
							+ element.valueType() + ")");
		}
		return valueFactory.add(vector, element);
	}

	@Override
	public ValueIF and(ValueIF assumption, ValueIF left, ValueIF right) {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.and(arg1, arg2);

		return valueFactory.value(predicate, result, booleanValueType);
	}

	@Override
	public ArrayElementReferenceValueIF arrayElementReference(
			ReferenceValueIF arrayReference, ValueIF index) {
		return valueFactory.arrayElementReferenceValue(trueExpression,
				arrayReference, 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.
	 */
	@Override
	public ArrayElementReferenceValueIF arrayElementReference(
			ReferenceValueIF arrayReference, ValueIF index,
			ReferenceValueTypeIF referenceType) {
		return valueFactory.arrayElementReferenceValue(arrayReference, index,
				referenceType);
	}

	@Override
	public ValueIF arrayRead(ValueIF assumption, ArrayValueIF array,
			ValueIF index) {
		return valueFactory.arrayRead(valueFactory.symExpression(assumption),
				array, index);
	}

	@Override
	public ArrayValueIF arrayValue(ArrayValueTypeIF valueType,
			ValueIF[] elementArray) {
		return arrayValue("E", valueType, elementArray);
	}

	@Override
	public ArrayValueIF arrayValue(String name, ArrayValueTypeIF valueType,
			MorphicVector<ValueIF> elements) {
		SymbolicTypeIF type = typeFactory.symType(valueType);

		return valueFactory.arrayValue(universe
				.symbolicConstantExpression(universe
						.getOrCreateSymbolicConstant(name, type)), elements,
				valueType);
	}

	@Override
	public ArrayValueIF arrayValue(String name, ArrayValueTypeIF valueType,
			ValueIF[] elementArray) {
		SymbolicTypeIF type = typeFactory.symType(valueType);
		MorphicVector<ValueIF> elementVector = valueVectorFactory
				.newVector(elementArray.length);

		for (int i = 0; i < elementArray.length; i++) {
			elementVector.set(i, elementArray[i]);
		}
		return valueFactory.arrayValue(universe
				.symbolicConstantExpression(universe
						.getOrCreateSymbolicConstant(name, type)),
				elementVector, valueType);
	}

	@Override
	public ArrayValueTypeIF arrayValueType(ValueTypeIF baseType,
			ValueIF lengthVector) {
		return typeFactory.arrayValueType(baseType, lengthVector);
	}

	@Override
	public ArrayValueTypeIF rectangularArrayValueType(ValueTypeIF baseType,
			ValueIF[] dimensions) {
		return typeFactory.rectangularArrayValueType(baseType, dimensions);
	}

	@Override
	public ArrayValueIF arrayWrite(ValueIF assumption, ArrayValueIF array,
			ValueIF index, ValueIF value) {
		ArrayValue arrayValue = (ArrayValue) array;

		if (useConcreteArrays) {
			IntegerNumberIF indexNumber = (IntegerNumberIF) numericValue(
					assumption, index);

			if (indexNumber != null)
				return valueFactory.setArrayElement(arrayValue,
						indexNumber.intValue(), value);
		}
		return arrayWriteSymbolic(assumption, array, index, value);
	}

	private ArrayValueIF arrayWriteSymbolic(ValueIF assumption,
			ArrayValueIF array, ValueIF index, ValueIF value) {
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF symArray = valueFactory.symExpression(array);
		SymbolicExpressionIF symIndex = valueFactory.symExpression(index);
		SymbolicExpressionIF symValue = valueFactory.symExpression(value);
		SymbolicExpressionIF symResult = universe.arrayWrite(symArray,
				symIndex, symValue);
		ValueTypeIF arrayType = array.valueType();

		return (ArrayValueIF) valueFactory.symbolicValue(predicate, symResult,
				arrayType);
	}

	@Override
	public ValueTypeIF booleanType() {
		return booleanValueType;
	}

	@Override
	public Boolean booleanValue(ValueIF assumption, ValueIF value) {
		if (value instanceof SymbolicValue) {
			SymbolicExpressionIF symValue = ((SymbolicValue) value)
					.getSymbolicExpression();
			Boolean booleanValue = universe.extractBoolean(symValue);

			if (booleanValue != null) {
				return booleanValue;
			} else {
				SymbolicExpressionIF predicate = valueFactory
						.symExpression(assumption);
				SymbolicSimplifierIF simplifier = simplifierFactory
						.simplifier(predicate);

				symValue = simplifier.simplify(symValue);
				booleanValue = universe.extractBoolean(symValue);
				if (booleanValue != null)
					return booleanValue;
			}
		}
		return null;
	}

	@Override
	public MessageIF canonic(MessageIF message) {
		return messageFactory.canonic(message);
	}

	@Override
	public ValueIF canonic(ValueIF value) {
		return valueFactory.canonic(value);
	}

	@Override
	public ValueTypeIF canonic(ValueTypeIF valueType) {
		return typeFactory.canonic(valueType);
	}

	@Override
	public ValueIF cast(ValueTypeIF newType, ValueIF oldValue)
			throws DynamicException {
		ValueTypeIF oldType = oldValue.valueType();

		if (newType instanceof PrimitiveValueTypeIF
				&& ((PrimitiveValueTypeIF) newType).type().kind() == TypeKind.RATIONAL) {
			if (oldType instanceof PrimitiveValueTypeIF
					&& ((PrimitiveValueTypeIF) oldType).type().kind() == TypeKind.INTEGER) {
				return valueFactory.symbolicValue(trueExpression, universe
						.castToReal(valueFactory.symExpression(oldValue)),
						newType);
			} else if (oldType instanceof PrimitiveValueTypeIF
					&& ((PrimitiveValueTypeIF) oldType).type().kind() == TypeKind.RATIONAL) {
				return oldValue;
			}
		}
		throw new DynamicException(DynamicErrorKind.INVALID_CAST,
				"TASS internal error: cannot cast " + oldValue + " to "
						+ newType);
	}

	@Override
	public ValueTypeIF characterType() {
		return characterValueType;
	}

	@Override
	public Character characterValue(ValueIF assumption, ValueIF value) {
		if (value instanceof SymbolicValue) {
			SymbolicExpressionIF symValue = ((SymbolicValue) value)
					.getSymbolicExpression();
			NumberIF characterValue = universe.extractNumber(symValue);

			if (characterValue != null) {
				return (char) Integer.parseInt(characterValue.atomString());
			} else {
				SymbolicExpressionIF predicate = valueFactory
						.symExpression(assumption);
				SymbolicSimplifierIF simplifier = simplifierFactory
						.simplifier(predicate);

				symValue = simplifier.simplify(symValue);
				characterValue = universe.extractNumber(symValue);
				if (characterValue != null)
					return (char) Integer.parseInt(characterValue.atomString());
			}
		}
		return null;
	}

	private ValueIF compatibleArrayTypes(ValueIF assumption,
			ArrayValueTypeIF type1, ArrayValueTypeIF type2) {
		if (type1.dimension() != type2.dimension())
			return falseValue;

		ValueIF result = equals(assumption, type1.lengthVector(),
				type2.lengthVector());

		result = and(assumption, result,
				compatibleTypes(assumption, type1.baseType(), type2.baseType()));
		return result;
	}

	private ValueIF compatibleRecordTypes(ValueIF assumption,
			RecordValueTypeIF type1, RecordValueTypeIF type2) {
		RecordTypeIF recordType1 = type1.type();
		RecordTypeIF recordType2 = type2.type();
		int numFields1 = recordType1.numFields();
		int numFields2 = recordType2.numFields();

		if (numFields1 != numFields2)
			return falseValue;

		ValueIF result = trueValue;

		for (int i = 0; i < numFields1; i++) {
			result = and(
					assumption,
					result,
					compatibleTypes(assumption, type1.fieldType(i),
							type2.fieldType(i)));
		}
		return result;
	}

	private ValueIF compatibleTypes(ValueIF assumption, ValueTypeIF type1,
			ValueTypeIF type2) {
		if (type1.equals(type2))
			return trueValue;
		if (type1 instanceof ArrayValueTypeIF
				&& type2 instanceof ArrayValueTypeIF) {
			return compatibleArrayTypes(assumption, (ArrayValueTypeIF) type1,
					(ArrayValueTypeIF) type2);
		}
		if (type1 instanceof RecordValueTypeIF
				&& type2 instanceof RecordValueTypeIF) {
			return compatibleRecordTypes(assumption, (RecordValueTypeIF) type1,
					(RecordValueTypeIF) type2);
		}
		return falseValue;
	}

	@Override
	public void complete(ReferenceValueTypeIF incompleteValueType,
			ValueTypeIF baseType) {
		typeFactory.complete(incompleteValueType, baseType);
	}

	public Object concreteValue(ValueIF assumption, ValueIF value) {
		ValueTypeIF valueType = value.valueType();

		if (booleanValueType.equals(valueType)) {
			return booleanValue(assumption, value);
		} else if (integerValueType.equals(valueType)
				|| realValueType.equals(valueType)) {
			return numericValue(assumption, value);
		} else if (characterValueType.equals(valueType)) {
			return characterValue(assumption, value);
		}
		return null;
	}

	@Override
	public RunConfiguration configuration() {
		return configuration;
	}

	/**
	 * Converts a symbolic expression into a ValueIF
	 */
	private ValueIF convertSymExpr(SymbolicExpressionIF symExpr,
			ValueTypeIF valueType) {
		return valueFactory.symbolicValue(trueExpression, symExpr, valueType);
	}

	/**
	 * The following is for division of two reals only. This is not integer
	 * division.
	 */
	@Override
	public ValueIF divide(ValueIF assumption, ValueIF left, ValueIF right) {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.divide(arg1, arg2);

		assert left.valueType() == realValueType;
		assert right.valueType() == realValueType;
		return valueFactory.value(predicate, result, realValueType);
	}

	@Override
	public ValueIF divides(ValueIF assumption, ValueIF left, ValueIF right) {
		return equals(assumption, zero, modulo(assumption, right, left));
	}

	@Override
	public ValueTypeIF elementType(ValueIF assumption,
			ArrayValueTypeIF arrayValueType, ValueIF index) {
		return valueFactory.elementType(valueFactory.symExpression(assumption),
				arrayValueType, index);
	}

	/**
	 * Returns vector of length 0 with given vector type.
	 */
	@Override
	public VectorValue emptyVectorValue(VectorValueTypeIF vectorValueType) {
		return valueFactory.emptyVector(vectorValueType);
	}

	// THINK ABOUT THIS:
	// add method which will return pair: the ValueIF, as before,
	// but also another thing explaining the sub-components which are not
	// equal. (1) index vector into thing, (2) sub-thing #1, (3) sub-thing #2.
	// reference into something...

	@Override
	public ValueIF equals(ValueIF assumption, ValueIF left, ValueIF right) {
		return equals(assumption, left, right, 0);
	}

	/**
	 * Returns boolean value representing "left==right". The scope count is
	 * needed when the arguments are arrays. Then this is tranlated into an
	 * expression of the form "forall i ....". The scope count is then
	 * incremented by 1. It is used to name the bound variable i.
	 * 
	 * @throws DynamicException
	 */
	private ValueIF equals(ValueIF assumption, ValueIF left, ValueIF right,
			int scopeCount) {
		ValueTypeIF leftType = left.valueType();
		ValueTypeIF rightType = right.valueType();

		if (isUndefined(left) || isUndefined(right))
			return falseValue;
		if (left.equals(right))
			return trueValue;

		ValueIF typeCompatibility = compatibleTypes(assumption, leftType,
				rightType);

		if (typeCompatibility.equals(falseValue))
			return falseValue;

		ValueIF result;
		Object leftConcreteValue = concreteValue(assumption, left);
		Object rightConcreteValue;

		if (leftConcreteValue != null
				&& (rightConcreteValue = concreteValue(assumption, right)) != null) {
			result = symbolicValue(leftConcreteValue.equals(rightConcreteValue));
		} else if (left instanceof ArrayValueIF) {
			result = equalsArrayPrefix(assumption,
					((ArrayValueTypeIF) leftType).extent(),
					(ArrayValueIF) left, (ArrayValueIF) right, scopeCount);
		} else if (left instanceof VectorValueIF) {
			result = equalsVector(assumption, (VectorValueIF) left,
					(VectorValueIF) right, scopeCount);
		} else if (left instanceof RecordValueIF) {
			RecordValueTypeIF recordValueType = (RecordValueTypeIF) leftType;
			int numFields = recordValueType.type().numFields();

			if (numFields == 0) {
				result = trueValue;
			} else {
				RecordValueIF leftRecord = (RecordValueIF) left;
				RecordValueIF rightRecord = (RecordValueIF) right;

				result = equals(assumption,
						recordRead(assumption, leftRecord, 0),
						recordRead(assumption, rightRecord, 0), scopeCount);
				for (int i = 1; i < numFields; i++) {
					result = and(
							assumption,
							result,
							equals(assumption,
									recordRead(assumption, leftRecord, i),
									recordRead(assumption, rightRecord, i),
									scopeCount));
				}
			}
		} else if (left instanceof ReferenceValueIF
				&& ((ReferenceValueIF) left).isNull()) {
			if (right instanceof ReferenceValueIF
					&& ((ReferenceValueIF) right).isNull())
				result = trueValue;
			else
				result = falseValue;
		} else if (right instanceof ReferenceValueIF
				&& ((ReferenceValueIF) right).isNull()) {
			result = falseValue;
		} else if (left instanceof VariableReferenceValueIF) {
			VariableReferenceValueIF leftRef = (VariableReferenceValueIF) left;
			VariableReferenceValueIF rightRef = (VariableReferenceValueIF) right;

			if (!(leftRef.variable().equals(rightRef.variable())))
				result = falseValue;
			else
				result = equals(assumption, leftRef.offset(),
						rightRef.offset(), scopeCount);
		} else if (left instanceof RecordElementReferenceValueIF) {
			RecordElementReferenceValueIF leftRef = (RecordElementReferenceValueIF) left;
			RecordElementReferenceValueIF rightRef = (RecordElementReferenceValueIF) right;

			if (leftRef.fieldIndex() != rightRef.fieldIndex())
				result = falseValue;
			else
				result = equals(assumption, leftRef.parent(),
						rightRef.parent(), scopeCount);
		} else if (left instanceof ArrayElementReferenceValueIF) {
			ArrayElementReferenceValueIF leftRef = (ArrayElementReferenceValueIF) left;
			ArrayElementReferenceValueIF rightRef = (ArrayElementReferenceValueIF) right;

			result = and(
					assumption,
					equals(assumption, leftRef.parent(), rightRef.parent(),
							scopeCount),
					equals(assumption, leftRef.index(), rightRef.index(),
							scopeCount));
		} else {
			result = equalsSymbolic(assumption, left, right, scopeCount);
		}
		if (result.equals(falseValue))
			return falseValue;
		return and(assumption, typeCompatibility, result);
	}

	/**
	 * Compares two array prefixes for equality, i.e., elements of indices less
	 * than length.
	 * 
	 * @throws DynamicException
	 */
	private ValueIF equalsArrayPrefix(ValueIF assumption, ValueIF length,
			ArrayValueIF array1, ArrayValueIF array2, int scopeCount) {
		IntegerNumberIF numElements = (IntegerNumberIF) concreteValue(
				assumption, length);

		if (numElements != null) {
			if (numElements.signum() == 0) {
				return trueValue;
			} else {
				ValueIF conjunction = equals(assumption,
						arrayRead(assumption, array1, zero),
						arrayRead(assumption, array2, zero), scopeCount);

				for (IntegerNumberIF i = ONE; numberFactory.compare(
						numElements, i) > 0 && !falseValue.equals(conjunction); i = numberFactory
						.add(i, ONE)) {
					ValueIF index = symbolicValue(i);

					conjunction = and(
							assumption,
							conjunction,
							equals(assumption,
									arrayRead(assumption, array1, index),
									arrayRead(assumption, array2, index),
									scopeCount));
				}
				return conjunction;
			}
		} else {
			SymbolicConstantIF boundVariable = getScopeVariable(scopeCount);
			ValueIF index = valueFactory.symbolicValue(
					universe.symbolicConstantExpression(boundVariable),
					integerValueType);
			ValueIF boundExpression = and(assumption,
					lessThanOrEquals(assumption, zero, index),
					lessThan(assumption, index, length));
			ValueIF elementComparison = equals(assumption,
					arrayRead(assumption, array1, index),
					arrayRead(assumption, array2, index), scopeCount + 1);
			ValueIF forall = forall(assumption, boundVariable, boundExpression,
					elementComparison);

			return forall;
		}
	}

	/**
	 * These symbolic constants are used when construction an expression of the
	 * from a==b for array values a and b. They are used as indices, as in
	 * forall i (in ...) a[i]=b[i]. There is an array because these can be
	 * nested in scopes.
	 */
	private Vector<SymbolicConstantIF> scopeVariables = new Vector<SymbolicConstantIF>();

	/** Get or create the scopeVariable symbolic constant. They are cached. */
	private SymbolicConstantIF getScopeVariable(int scope) {
		if (scope >= scopeVariables.size()) {
			scopeVariables.setSize(scope + 1);
		}

		SymbolicConstantIF result = scopeVariables.get(scope);

		if (result == null) {
			result = universe.getOrCreateSymbolicConstant("I" + scope,
					integerSymbolicTypeIF);
			scopeVariables.set(scope, result);
		}
		return result;
	}

	private ValueIF equalsSymbolic(ValueIF assumption, ValueIF left,
			ValueIF right, int scopeCount) {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.equals(arg1, arg2);

		return valueFactory.value(predicate, result, booleanValueType);
	}

	private ValueIF equalsVector(ValueIF assumption, VectorValueIF vector1,
			VectorValueIF vector2, int scopeCount) {
		int size = vector1.size();

		if (size != vector2.size())
			return falseValue;
		if (size == 0)
			return trueValue;

		try {
			ValueIF result = equals(assumption, vector1.get(0), vector2.get(0),
					scopeCount);

			for (int i = 1; i < size && !falseValue.equals(result); i++) {
				result = and(
						assumption,
						result,
						equals(assumption, vector1.get(i), vector2.get(i),
								scopeCount));
			}
			return result;
		} catch (DynamicException e) {
			throw new TASSInternalException(
					"Should not happen: vectors have equal positive length.");
		}
	}

	@Override
	public ValueIF apply(ValueIF assumption, ValueIF function, ValueIF[] point) {
		SymbolicExpressionIF[] expressions = new SymbolicExpressionIF[point.length];
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);

		for (int i = 0; i < point.length; i++) {
			expressions[i] = valueFactory.symExpression(point[i]);
		}

		SymbolicExpressionIF expr = universe.apply(
				valueFactory.symExpression(function), expressions);

		return valueFactory.value(predicate, expr, valueType(expr.type()));
	}

	@Override
	public ValueIF exists(ValueIF assumption, BoundVariableIF variable,
			ValueIF boundExpression, ValueIF expression)
			throws DynamicException {
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicConstantIF var = symbolicConstantForBoundVariable(variable);
		ValueIF expr = (boundExpression == null ? expression : implies(
				assumption, boundExpression, expression));

		return valueFactory.value(predicate,
				universe.exists(var, valueFactory.symExpression(expr)),
				booleanValueType);
	}

	@Override
	public ValueIF falseValue() {
		return falseValue;
	}

	public ValueIF findModel(ValueIF context) throws DynamicException {
		// TODO remove this print statement
		System.out.println("\nPath Condition: " + context);
		SymbolicExpressionIF symExpAssumption = null;
		System.out
				.println("SymbolicConstants: " + universe.symbolicConstants());
		// convert ValueIF context to a symbolic expression
		symExpAssumption = valueFactory.symExpression(context);

		if (symExpAssumption != null) {
			// get the model from cvc3
			Map<SymbolicConstantIF, SymbolicExpressionIF> map;
			try {
				map = prover.findModel(symExpAssumption);
			} catch (TheoremProverException e) {
				throw new DynamicException(
						DynamicException.DynamicErrorKind.PROVER,
						e.getMessage());
			}
			if (map != null) {
				Set<Entry<SymbolicConstantIF, SymbolicExpressionIF>> entrySet = map
						.entrySet();
				// create an iterator to walk through each entry in the map
				Iterator<Entry<SymbolicConstantIF, SymbolicExpressionIF>> iter = entrySet
						.iterator();
				ValueIF assumption = null;
				while (iter.hasNext()) {
					Map.Entry<SymbolicConstantIF, SymbolicExpressionIF> entry = (Map.Entry<SymbolicConstantIF, SymbolicExpressionIF>) iter
							.next();
					// convert the symbolic constant to a value
					ValueIF constant = symbolicConstant(entry.getKey().name(),
							valueType(entry.getKey().type()));
					ValueIF term;
					// set the constant to its value
					term = equals(
							trueValue(),
							constant,
							convertSymExpr(entry.getValue(),
									constant.valueType()));
					if (assumption == null) {
						assumption = term;
					} else {
						// and the new term with the others
						assumption = and(trueValue(), assumption, term);
					}
				}
				return assumption;
			}
		}
		return null;
	}

	public ValueIF forall(ValueIF assumption, SymbolicConstantIF var,
			ValueIF boundExpression, ValueIF expression) {
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);

		if (boundExpression != null && var.type().isInteger()) {
			IntervalIF interval = this.getInterval(assumption, var,
					boundExpression);

			if (interval != null && !interval.strictLower()
					&& !interval.strictUpper()) {
				IntegerNumberIF low = (IntegerNumberIF) interval.lower();
				IntegerNumberIF high = (IntegerNumberIF) interval.upper();
				IntegerNumberIF deltaNumber = numberFactory.subtract(high, low);

				if (deltaNumber.signum() < 0)
					return trueValue; // vacuous

				IntegerNumberIF difference = numberFactory.subtract(
						quantifierExpansionThreshold, deltaNumber);

				if (difference.signum() >= 0) {
					int delta = deltaNumber.intValue();
					ValueIF result = null;

					for (int i = 0; i <= delta; i++) {
						// substitute concrete value for occurrences of
						// bound variable in expression...
						ValueIF loopValue = symbolicValue(low);
						ValueSubstituterIF substituter = ValueSubstituter
								.valueSubstituterFromSymbolicConstantValue(
										valueFactory, var, loopValue);
						ValueIF simplifiedExpression = substituter
								.substitute(expression);

						if (i == 0) {
							result = simplifiedExpression;
						} else {
							result = and(assumption, result,
									simplifiedExpression);
						}
						if (i < delta)
							low = numberFactory.add(low, ONE);
					}
					return result;
				}
			}
		}

		ValueIF expr = (boundExpression == null ? expression : implies(
				assumption, boundExpression, expression));

		return valueFactory.value(predicate,
				universe.forall(var, valueFactory.symExpression(expr)),
				booleanValueType);
	}

	public ValueIF forall(ValueIF assumption, BoundVariableIF variable,
			ValueIF boundExpression, ValueIF expression) {
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicConstantIF var = symbolicConstantForBoundVariable(variable);

		if (boundExpression != null
				&& variable.type().kind() == TypeKind.INTEGER) {
			IntervalIF interval = this.getInterval(assumption, variable,
					boundExpression);

			if (interval != null && !interval.strictLower()
					&& !interval.strictUpper()) {
				IntegerNumberIF low = (IntegerNumberIF) interval.lower();
				IntegerNumberIF high = (IntegerNumberIF) interval.upper();
				IntegerNumberIF deltaNumber = numberFactory.subtract(high, low);

				if (deltaNumber.signum() < 0)
					return trueValue; // vacuous

				IntegerNumberIF difference = numberFactory.subtract(
						quantifierExpansionThreshold, deltaNumber);

				if (difference.signum() >= 0) {
					int delta = deltaNumber.intValue();
					ValueIF result = null;

					for (int i = 0; i <= delta; i++) {
						// substitute concrete value for occurrences of
						// bound variable in expression...
						ValueIF loopValue = symbolicValue(low);
						ValueSubstituterIF substituter = ValueSubstituter
								.valueSubstituterFromSymbolicConstantValue(
										valueFactory, var, loopValue);
						ValueIF simplifiedExpression = substituter
								.substitute(expression);

						if (i == 0) {
							result = simplifiedExpression;
						} else {
							result = and(assumption, result,
									simplifiedExpression);
						}
						if (i < delta)
							low = numberFactory.add(low, ONE);
					}
					return result;
				}
			}
		}

		ValueIF expr = (boundExpression == null ? expression : implies(
				assumption, boundExpression, expression));

		return valueFactory.value(predicate,
				universe.forall(var, valueFactory.symExpression(expr)),
				booleanValueType);
	}

	@Override
	public ValueIF function(ValueIF assumption, AbstractFunctionIF f,
			ValueTypeIF[] parameterTypes, ValueTypeIF returnType)
			throws DynamicException {

		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicTypeIF functionType;
		SymbolicTypeIF inputTypes[] = new SymbolicTypeIF[f.numFormals()];
		SymbolicTypeIF outputType = typeFactory.symType(returnType);
		for (int i = 0; i < f.numFormals(); i++) {
			inputTypes[i] = typeFactory.symType(parameterTypes[i]);
		}
		functionType = universe.functionType(inputTypes, outputType);
		SymbolicConstantIF fConstant = universe.getOrCreateSymbolicConstant(
				f.name(), functionType);
		return valueFactory.value(predicate,
				universe.symbolicConstantExpression(fConstant),
				valueType(functionType));
	}

	@Override
	public FunctionValueTypeIF functionValueType(ValueTypeIF[] inputTypes,
			ValueTypeIF outputType) {
		return typeFactory.functionValueType(outputType, inputTypes);
	}

	/**
	 * Returns the element of the vector at the given index. Assumes, but does
	 * not check, that the index is within range.
	 */
	@Override
	public ValueIF get(VectorValueIF vector, int index) throws DynamicException {
		return vector.get(index);
	}

	public IntervalIF getInterval(ValueIF assumption,
			SymbolicConstantIF symbolicConstant, ValueIF constraint) {
		try {
			DynamicSimplifierIF simplifier1 = simplifier(assumption);
			DynamicSimplifierIF simplifier2;

			constraint = simplifier1.simplify(constraint);
			simplifier2 = simplifier(constraint);
			return simplifier2.assumptionAsInterval(symbolicConstant);
		} catch (DynamicException e) {
			throw new TASSInternalException(e.toString());
		}
	}

	@Override
	public IntervalIF getInterval(ValueIF assumption, BoundVariableIF variable,
			ValueIF constraint) {
		try {
			SymbolicConstantIF symbolicConstant = symbolicConstantForBoundVariable(variable);
			DynamicSimplifierIF simplifier1 = simplifier(assumption);
			DynamicSimplifierIF simplifier2;

			constraint = simplifier1.simplify(constraint);
			simplifier2 = simplifier(constraint);
			return simplifier2.assumptionAsInterval(symbolicConstant);
		} catch (DynamicException e) {
			throw new TASSInternalException(e.toString());
		}
	}

	@Override
	public Map<SharedVariableIF, CellIF> getSharedVariableCells(
			Collection<SharedVariableIF> variables) {
		Map<SharedVariableIF, CellIF> map = new HashMap<SharedVariableIF, CellIF>();
		for (SharedVariableIF variable : variables) {
			map.put(variable, sharedCell(variable));
		}
		return map;
	}

	@Override
	public HeapCellIF heapCell(ProcessIF process, int heapIndex) {
		return cellFactory.dynamicHeapVariable(process, heapIndex);
	}

	@Override
	public ValueIF ifThenElse(ValueIF assumption, ValueIF condition,
			ValueIF trueValue, ValueIF falseValue) throws DynamicException {
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);

		return valueFactory.value(predicate, universe.cond(
				valueFactory.symExpression(condition),
				valueFactory.symExpression(trueValue),
				valueFactory.symExpression(falseValue)), trueValue.valueType());
	}

	@Override
	public ValueIF implies(ValueIF assumption, ValueIF left, ValueIF right) {
		return or(assumption, not(assumption, left), right);
	}

	@Override
	public ValueIF intDivide(ValueIF assumption, ValueIF left, ValueIF right)
			throws DynamicException {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.divide(arg1, arg2);

		assert left.valueType() == integerValueType;
		assert right.valueType() == integerValueType;
		return valueFactory.value(predicate, result, integerValueType);
	}

	@Override
	public ValueTypeIF integerType() {
		return integerValueType;
	}

	@Override
	public boolean isUndefined(ValueIF value) {
		return value instanceof UndefinedValue;
	}

	/** Assuming the assumption is satisfiable,.... */
	@Override
	public boolean isValid(ValueIF assumption, ValueIF predicate)
			throws DynamicException {
		return valid(assumption, predicate) == ResultType.YES;
	}

	@Override
	public ValueIF lessThan(ValueIF assumption, ValueIF left, ValueIF right) {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.lessThan(arg1, arg2);

		return valueFactory.value(predicate, result, booleanValueType);
	}

	@Override
	public ValueIF lessThanOrEquals(ValueIF assumption, ValueIF left,
			ValueIF right) {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.lessThanEquals(arg1, arg2);

		return valueFactory.value(predicate, result, booleanValueType);
	}

	@Override
	public LiteralCellIF literalCell(ObjectLiteralExpressionIF expression) {
		return cellFactory.literalCell(expression);
	}

	@Override
	public LocalCellIF localCell(LocalVariableIF variable, int stackIndex) {
		return cellFactory.dynamicLocalVariable(variable, stackIndex);
	}

	@Override
	public MessageIF message(ProcessIF source, ProcessIF destination,
			ValueIF tag, ValueIF data) {
		return messageFactory.message(source, destination, tag, data);
	}

	@Override
	public MorphicFactoryIF<MessageIF> messageFactory() {
		return messageFactory;
	}

	@Override
	public MorphicSimplifierIF<MessageIF> messageSimplifier() {
		return messageSimplifier;
	}

	@Override
	public MorphicVectorFactory<MessageIF> messageVectorFactory() {
		return messageVectorFactory;
	}

	@Override
	public MorphicSimplifierIF<MorphicVector<MessageIF>> messageVectorSimplifier() {
		return messageVectorSimplifier;
	}

	@Override
	public ModelFactoryIF modelFactory() {
		return modelFactory;
	}

	@Override
	public ValueIF modulo(ValueIF assumption, ValueIF left, ValueIF right) {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.modulo(arg1, arg2);

		return valueFactory.value(predicate, result, integerValueType);
	}

	@Override
	public ValueIF multiply(ValueIF assumption, ValueIF left, ValueIF right) {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.multiply(arg1, arg2);
		ValueTypeIF valueType = (left.valueType().equals(integerValueType)
				&& right.valueType().equals(integerValueType) ? integerValueType
				: realValueType);

		return valueFactory.value(predicate, result, valueType);
	}

	@Override
	public ValueIF negative(ValueIF assumption, ValueIF arg) {
		Object concreteValue = concreteValue(assumption, arg);

		if (concreteValue != null) {
			if (concreteValue instanceof NumberIF) {
				return symbolicValue(numberFactory
						.negate((NumberIF) concreteValue));
			}
			throw new TASSInternalException("Unknown concrete value type: "
					+ concreteValue);
		}

		SymbolicExpressionIF arg1 = valueFactory.symExpression(arg);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.minus(arg1);
		ValueTypeIF valueType = valueType(result.type());

		return valueFactory.value(predicate, result, valueType);
	}

	@Override
	public <T extends Morphic> MorphicSimplifierIF<MorphicArray<T>> newArraySimplifier(
			MorphicArrayFactory<T> arrayFactory,
			MorphicSimplifierIF<? super T> elementSimplifier) {
		return new ArraySimplifier<T>(arrayFactory, elementSimplifier);
	}

	@Override
	public ReferenceValueTypeIF newIncompleteReferenceValueType() {
		return typeFactory.newIncompleteReferenceValueType();
	}

	@Override
	public <T extends Morphic> MorphicSimplifierIF<MorphicList<T>> newListSimplifier(
			MorphicListFactory<T> listFactory,
			MorphicSimplifierIF<? super T> elementSimplifier) {
		// TODO: to be implemented
		// return new ListSimplifier<T>(store, listFactory, elementSimplifier);
		return null;
	}

	@Override
	public <T extends Morphic> MorphicSimplifierIF<MorphicSet<T>> newSetSimplifier(
			MorphicSetFactory<T> setFactory,
			MorphicSimplifierIF<? super T> elementSimplifier) {
		return new SetSimplifier<T>(setFactory, elementSimplifier);
	}

	@Override
	public MorphicSimplifierCacheIF newSimpleCache() {
		return new SimpleCache();
	}

	@Override
	public <T extends Morphic> MorphicSimplifierIF<MorphicVector<T>> newVectorSimplifier(
			MorphicVectorFactory<T> vectorFactory,
			MorphicSimplifierIF<? super T> elementSimplifier) {
		return new VectorSimplifier<T>(vectorFactory, elementSimplifier);
	}

	@Override
	public DynamicSimplifierIF noAssumptionSimplifier() {
		return noAssumptionSimplifier;
	}

	@Override
	public ValueIF not(ValueIF assumption, ValueIF arg) {
		if (trueValue.equals(arg))
			return falseValue;
		if (falseValue.equals(arg))
			return trueValue;

		SymbolicExpressionIF arg1 = valueFactory.symExpression(arg);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.not(arg1);

		return valueFactory.value(predicate, result, booleanValueType);
	}

	/**
	 * Conservative estimate to "not satisfiable": if this method returns true,
	 * then the predicate is definitely not satisfiable. If it returns false,
	 * anything is possible.
	 * 
	 * @throws DynamicException
	 *             if something goes wrong in the theorem prover
	 */
	@Override
	public boolean nsat(ValueIF predicate) throws DynamicException {
		return isValid(trueValue, not(trueValue, predicate));
	}

	@Override
	public ReferenceValueIF nullReferenceValue(
			ReferenceValueTypeIF referenceType) {
		return valueFactory.nullReferenceValue(referenceType);
	}

	@Override
	public NumberFactoryIF numberFactory() {
		return numberFactory;
	}

	// these could also be cached...
	@Override
	public NumberIF numericValue(ValueIF assumption, ValueIF value) {
		return valueFactory.numericValue(
				valueFactory.symExpression(assumption), value);
	}

	@Override
	public int numMessages() {
		return messageFactory.numStored();
	}

	@Override
	public int numProverValidCalls() {
		return prover.numInternalValidCalls();
	}

	@Override
	public int numQueries() {
		return queryCache.size();
	}

	@Override
	public int numValues() {
		return valueFactory.numStored();
	}

	@Override
	public ValueIF one() {
		return one;
	}

	@Override
	public ValueIF or(ValueIF assumption, ValueIF left, ValueIF right) {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.or(arg1, arg2);

		return valueFactory.value(predicate, result, booleanValueType);
	}

	@Override
	public ProcessCellIF processCell(ProcessVariableIF variable) {
		return cellFactory.processCell(variable);
	}

	@Override
	public TheoremProverIF prover() {
		return prover;
	}

	@Override
	public Set<VariableReferenceValueIF> reachableVariableReferences(
			ValueIF value, Collection<ValueIF> seenValues) {
		return valueFactory.reachableVariableReferences(value, seenValues);
	}

	@Override
	public ValueTypeIF realType() {
		return realValueType;
	}

	@Override
	public RecordElementReferenceValueIF recordElementReference(
			ReferenceValueIF recordReference, int fieldIndex) {
		return valueFactory.recordElementReferenceValue(recordReference,
				fieldIndex);
	}

	@Override
	public RecordElementReferenceValueIF recordElementReference(
			ReferenceValueIF recordReference, int fieldIndex,
			ReferenceValueTypeIF referenceType) {
		return valueFactory.recordElementReferenceValue(recordReference,
				fieldIndex, referenceType);
	}

	@Override
	public ValueIF recordRead(ValueIF assumption, RecordValueIF record,
			int fieldIndex) {
		return record.element(fieldIndex);
	}

	@Override
	public RecordValueIF recordValue(RecordValueTypeIF recordType,
			ValueIF[] fieldValues) {
		return valueFactory.recordValue(fieldValues, recordType);
	}

	@Override
	public RecordValueIF recordValue(ValueIF assumption,
			RecordValueTypeIF recordType, ValueIF[] fieldValues) {
		return valueFactory.recordValue(fieldValues, recordType);
	}

	@Override
	public RecordValueTypeIF recordValueType(RecordTypeIF recordType,
			ValueTypeIF[] fieldTypes) {
		return typeFactory.recordValueType(recordType, fieldTypes);
	}

	@Override
	public RecordValueIF recordWrite(ValueIF assumption, RecordValueIF record,
			int fieldIndex, ValueIF newValue) {
		return valueFactory.setRecordElement(record, fieldIndex, newValue);
	}

	@Override
	public DynamicSimplifierIF referenceSimplifier(
			ValueSubstituterIF substituter, MorphicSimplifierCacheIF cache) {
		return new ReferenceSimplifier(substituter, this, cache);
	}

	@Override
	public VariableReferenceValueIF referenceValue(CellIF variable,
			ReferenceValueTypeIF referenceType) {
		return valueFactory.variableReferenceValue(variable, referenceType,
				zero);
	}

	@Override
	public VariableReferenceValueIF referenceValue(CellIF variable,
			ReferenceValueTypeIF referenceType, ValueIF offset) {
		return valueFactory.variableReferenceValue(variable, referenceType,
				offset);
	}

	@Override
	public ReferenceValueTypeIF referenceValueType(ValueTypeIF type) {
		return typeFactory.referenceValueType(type);
	}

	/**
	 * Removes element at given position in the vector. The length of the vector
	 * is decreased by one and the elements at greater positions are shifted
	 * down.
	 * 
	 * @throws DynamicException
	 *             if index<0 or index>=vector.size()
	 */
	@Override
	public VectorValue removeElementAt(VectorValueIF vector, int index)
			throws DynamicException {
		return valueFactory.removeElementAt(vector, index);
	}

	/**
	 * Returns vector which is same as given one, except that the element at
	 * position index has been set to the given value. The method assumes, but
	 * does not check, that index is within range, i.e., that 0<=index<size,
	 * where size is the size of the vector. The size of the vector is
	 * unchanged.
	 */
	@Override
	public VectorValue set(VectorValueIF vector, int index, ValueIF value)
			throws DynamicException {
		return valueFactory.setExtend(vector, index, value);
	}

	@Override
	public SharedCellIF sharedCell(SharedVariableIF variable) {
		return cellFactory.sharedCell(variable);
	}

	@Override
	public void shutdown() {
		if (configuration.verbose()) {
			configuration.out().println("Destroying dynamic factory " + id);
			configuration.out().flush();
		}
		universe = null;
		booleanSymbolicTypeIF = null;
		booleanValueType = null;
		characterValueType = null;
		configuration = null;
		falseValue = null;
		integerSymbolicTypeIF = null;
		integerValueType = null;
		modelFactory = null;
		one = null;
		realSymbolicTypeIF = null;
		realValueType = null;
		trueValue = null;
		typeFactory = null;
		valueFactory = null;
		cellFactory = null;
		zero = null;
		queryCache = null;
	}

	@Override
	public DynamicSimplifierIF simplifier(ValueIF assumption)
			throws DynamicException {
		try {
			return simplifier(assumption, simplifyCache);
		} catch (DynamicException e) {
			throw new TASSInternalException(e.toString());
		}
	}

	@Override
	public DynamicSimplifierIF simplifier(ValueIF assumption,
			MorphicSimplifierCacheIF cache) throws DynamicException {
		assumption = canonic(assumption);
		// TODO: experimental optimization: reduce assumption to canonical
		// form first.
		assumption = noAssumptionSimplifier.simplify(assumption);

		DynamicSimplifierIF simplifier = simplifierCache.get(assumption);

		if (simplifier != null)
			return simplifier;
		simplifier = new DynamicSimplifier(this, assumption, cache);
		simplifierCache.put(assumption, simplifier);
		return simplifier;
	}

	public DynamicSimplifierIF simplifier(ValueSubstituterIF substituter,
			MorphicSimplifierCacheIF cache) {
		return new SubstitutionSimplifier(substituter, this, cache);
	}

	public SymbolicSimplifierFactoryIF simplifierFactory() {
		return simplifierFactory;
	}

	@Override
	public MorphicSimplifierCacheIF simplifyCache() {
		return simplifyCache;
	}

	@Override
	public MessageIF simplifyMessage(DynamicSimplifierIF dynamicSimplifier,
			MessageIF message) throws DynamicException {
		return messageSimplifier.simplify(dynamicSimplifier, message);
	}

	@Override
	public MorphicVector<MessageIF> simplifyMessageVector(
			DynamicSimplifierIF dynamicSimplifier,
			MorphicVector<MessageIF> messageVector) throws DynamicException {
		return messageVectorSimplifier.simplify(dynamicSimplifier,
				messageVector);
	}

	@Override
	public ValueIF simplifyValue(DynamicSimplifierIF dynamicSimplifier,
			ValueIF value) throws DynamicException {
		return valueSimplifier.simplify(dynamicSimplifier, value);
	}

	@Override
	public MorphicArray<ValueIF> simplifyValueArray(
			DynamicSimplifierIF dynamicSimplifier,
			MorphicArray<ValueIF> valueArray) throws DynamicException {
		return valueArraySimplifier.simplify(dynamicSimplifier, valueArray);
	}

	@Override
	public MorphicVector<ValueIF> simplifyValueVector(
			DynamicSimplifierIF dynamicSimplifier,
			MorphicVector<ValueIF> valueVector) throws DynamicException {
		return valueVectorSimplifier.simplify(dynamicSimplifier, valueVector);
	}

	@Override
	public int size(VectorValueIF vector) {
		return vector.size();
	}

	@Override
	public ValueIF sizeof(ValueTypeIF valueType) throws DynamicException {
		valueType = typeFactory.canonic(valueType);
		if (valueType instanceof ArrayValueTypeIF) {
			ArrayValueTypeIF arrayValueType = (ArrayValueTypeIF) valueType;
			ValueIF extent = arrayValueType.extent();
			int dimension = arrayValueType.dimension();
			ValueTypeIF baseType = arrayValueType.baseType();

			if (extent == null) {
				throw new DynamicException(DynamicErrorKind.SIZEOF,
						"Cannot take sizeof array of unspecified extent: "
								+ valueType);
			}
			if (dimension > 1) {
				throw new DynamicException(DynamicErrorKind.SIZEOF,
						"Cannot take sizeof ragged array: " + valueType);
			}
			return multiply(trueValue, extent, sizeof(baseType));
		} else if (valueType instanceof PrimitiveValueTypeIF
				&& ((PrimitiveValueTypeIF) valueType).type().kind() == TypeIF.TypeKind.CHAR) {
			return symbolicValue(1);
		} else if (valueType instanceof PrimitiveValueTypeIF
				|| valueType instanceof RecordValueTypeIF
				|| valueType instanceof ReferenceValueTypeIF) {
			int typeId = valueType.canonicalId();

			assert typeId >= 0;

			ValueIF typeIdValue = symbolicValue(typeId);
			ValueIF result = apply(trueValue, sizeofFunction,
					new ValueIF[] { typeIdValue });

			return result;

		} else {
			throw new DynamicException(DynamicErrorKind.SIZEOF,
					"Cannot take sizeof type: " + valueType);
		}
	}

	@Override
	public ValueIF subtract(ValueIF assumption, ValueIF left, ValueIF right) {
		SymbolicExpressionIF arg1 = valueFactory.symExpression(left);
		SymbolicExpressionIF arg2 = valueFactory.symExpression(right);
		SymbolicExpressionIF predicate = valueFactory.symExpression(assumption);
		SymbolicExpressionIF result = universe.subtract(arg1, arg2);
		ValueTypeIF valueType = (left.valueType().equals(integerValueType)
				&& right.valueType().equals(integerValueType) ? integerValueType
				: realValueType);

		return valueFactory.value(predicate, result, valueType);

	}

	@Override
	public ValueIF symbolicConstant(String name, ValueTypeIF type) {
		return valueFactory.symbolicValue(trueExpression, universe
				.symbolicConstantExpression(universe
						.getOrCreateSymbolicConstant(name,
								typeFactory.symType(type))), type);
	}

	private SymbolicConstantIF symbolicConstantForBoundVariable(
			BoundVariableIF variable, SymbolicTypeIF type) {
		SymbolicConstantIF var = universe.getOrCreateSymbolicConstant("B"
				+ variable.boundVariableId(), type);

		return var;
	}

	public SymbolicConstantIF symbolicConstantForBoundVariable(
			BoundVariableIF variable) {
		TypeIF type = variable.type();
		SymbolicTypeIF symType;

		switch (type.kind()) {
		case BOOLEAN:
			symType = booleanSymbolicTypeIF;
			break;
		case INTEGER:
			symType = integerSymbolicTypeIF;
			break;
		case RATIONAL:
			symType = realSymbolicTypeIF;
			break;
		default:
			throw new TASSInternalException(
					"Quantified variables must have primitive type");
		}
		return symbolicConstantForBoundVariable(variable, symType);
	}

	/**
	 * Returns the set of symbolic constants occurring within any value in a set
	 * of values. Includes those symbolic constants that might be reachable from
	 * the value types as well.
	 */
	@Override
	public Collection<SymbolicConstantIF> symbolicConstants(
			Collection<ValueIF> valueSet) {
		return explorer.symbolicConstants(valueSet);
	}

	public SymbolicUniverseIF symbolicUniverse() {
		return universe;
	}

	@Override
	public ValueIF symbolicValue(boolean value) {
		return (value ? trueValue : falseValue);
	}

	@Override
	public ValueIF symbolicValue(char value) {
		return valueFactory.characterValue(universe
				.concreteExpression((int) value));
	}

	@Override
	public ValueIF symbolicValue(int value) {
		return valueFactory.symbolicValue(trueExpression,
				universe.concreteExpression(value), integerValueType);
	}

	@Override
	public ValueIF symbolicValue(NumberIF value) {
		ValueTypeIF type = (value instanceof IntegerNumberIF ? integerValueType
				: realValueType);
		SymbolicExpressionIF expression = universe.concreteExpression(value);

		return valueFactory.symbolicValue(trueExpression, expression, type);
	}

	@Override
	public String toString() {
		return "Dynamic Factory " + id;
	}

	@Override
	public ValueIF trueValue() {
		return trueValue;
	}

	@Override
	public ValueIF undefinedValue(ValueTypeIF scalarType) {
		return valueFactory.undefinedValue(scalarType);
	}

	@Override
	public SymbolicUniverseIF universe() {
		return universe;
	}

	@Override
	public ResultType valid(ValueIF assumption, ValueIF predicate)
			throws DynamicException {
		ResultType result;
		int callID = ++numValidCalls;

		if (showQueries) {
			out.println();
			out.println("Query assumption " + callID + ": " + assumption);
			out.println("Query predicate  " + callID + ": " + predicate);
			out.flush();
		}
		if (trueValue.equals(predicate) || falseValue.equals(assumption)) {
			result = ResultType.YES;
		} else if (trueValue.equals(assumption) && falseValue.equals(predicate)) {
			result = ResultType.NO;
		} else {
			DynamicSimplifierIF simplifier;
			Query query;

			assumption = canonic(assumption);
			predicate = canonic(predicate);
			if (simplify) {
				simplifier = simplifier(assumption, simplifyCache);
				assumption = simplifier.newAssumption(); // constants stripped
				predicate = simplifier.simplify(predicate); // constants
				// stripped
			}
			query = new Query(assumption, predicate);
			result = queryCache.get(query);
			if (result == null) {
				if (falseValue.equals(predicate)) {
					// if exists x.assumption(x) return false else return true,
					// i.e. return valid(!assumption(x))
					result = valid(trueValue, not(trueValue, assumption));
				} else {
					if (trueValue.equals(predicate))
						result = ResultType.YES;
					else if (falseValue.equals(predicate))
						result = ResultType.NO;
					else {
						SymbolicExpressionIF symAssumption = valueFactory
								.symExpression(assumption);
						SymbolicExpressionIF symPredicate = valueFactory
								.symExpression(symAssumption, predicate);

						result = prover.valid(symAssumption, symPredicate);
					}
				}
				queryCache.put(query, result);
			}
		}
		if (showQueries) {
			out.println("Query result     " + callID + ": " + result);
			out.flush();
		}
		return result;
	}

	@Override
	public MorphicArrayFactory<ValueIF> valueArrayFactory() {
		return valueArrayFactory;
	}

	@Override
	public MorphicSimplifierIF<MorphicArray<ValueIF>> valueArraySimplifier() {
		return valueArraySimplifier;
	}

	@Override
	public MorphicFactoryIF<ValueIF> valueFactory() {
		return valueFactory;
	}

	public ValueIF valueOfBoundVariable(BoundVariableIF variable,
			ValueTypeIF type) {
		SymbolicTypeIF symType = typeFactory.symType(type);
		SymbolicConstantIF symbolicConstant = this
				.symbolicConstantForBoundVariable(variable, symType);
		SymbolicExpressionIF symbolicExpression = universe
				.symbolicConstantExpression(symbolicConstant);
		ValueIF result = valueFactory.value(symbolicExpression, type);

		return result;
	}

	@Override
	public ValueIF valueOfBoundVariable(BoundVariableIF variable) {
		TypeIF type = variable.type();
		SymbolicTypeIF symType;
		SymbolicConstantIF var;
		SymbolicExpressionIF expression;
		ValueTypeIF valueType;

		switch (type.kind()) {
		case BOOLEAN:
			symType = booleanSymbolicTypeIF;
			valueType = booleanValueType;
			break;
		case INTEGER:
			symType = integerSymbolicTypeIF;
			valueType = integerValueType;
			break;
		case RATIONAL:
			symType = realSymbolicTypeIF;
			valueType = realValueType;
			break;
		default:
			throw new TASSInternalException(
					"Quantified variables must have primitive type");
		}
		var = symbolicConstantForBoundVariable(variable, symType);
		expression = universe.symbolicConstantExpression(var);
		return valueFactory.value(expression, valueType);
	}

	@Override
	public MorphicSimplifierIF<ValueIF> valueSimplifier() {
		return valueSimplifier;
	}

	/**
	 * A value substituter is specified by a map from values to values. The map
	 * is then extended to a map on all values by looking for any sub-tree in
	 * the tree defining a value that matches one of the values in the domain of
	 * the map.
	 */
	@Override
	public ValueSubstituterIF valueSubstituter(Map<ValueIF, ValueIF> valueMap)
			throws DynamicException {
		return new ValueSubstituter(valueFactory, valueMap);
	}

	@Override
	public ValueSubstituterIF valueSubstituterFromSymbolicConstantMap(
			Map<SymbolicConstantIF, SymbolicConstantIF> symbolicConstantMap) {
		return ValueSubstituter.valueSubstituterFromSymbolicConstantMap(
				valueFactory, symbolicConstantMap);
	}

	@Override
	public ValueSubstituterIF valueSubstituterFromTreeMap(
			Map<TreeExpressionIF, TreeExpressionIF> treeMap) {
		return ValueSubstituter.valueSubstituterFromTreeMap(valueFactory,
				treeMap);
	}

	private ValueTypeIF valueType(SymbolicTypeIF symType) {
		SymbolicTypeKind kind = symType.kind();

		switch (kind) {
		case BOOLEAN:
			return booleanValueType;
		case INTEGER:
			return integerValueType;
		case REAL:
			return realValueType;
		case ARRAY:
			SymbolicArrayTypeIF arrayType = (SymbolicArrayTypeIF) symType;
			SymbolicExpressionIF extent = null;

			if (arrayType instanceof SymbolicCompleteArrayTypeIF)
				extent = ((SymbolicCompleteArrayTypeIF) arrayType).extent();
			return typeFactory.arrayValueType(
					valueType(arrayType.elementType()), valueFactory
							.symbolicValue(trueExpression, extent,
									typeFactory.integerType()));
		case FUNCTION:
			SymbolicFunctionTypeIF functionType = (SymbolicFunctionTypeIF) symType;
			ValueTypeIF returnType = valueType(functionType.outputType());
			ValueTypeIF[] argumentTypes = new ValueTypeIF[functionType
					.numInputs()];
			for (int i = 0; i < functionType.numInputs(); i++) {
				argumentTypes[i] = valueType(functionType.inputType(i));
			}
			return typeFactory.functionValueType(returnType, argumentTypes);

		default:
			throw new TASSInternalException(
					"Unknown symbolic expression type kind: " + kind);
		}
	}

	@Override
	public MorphicFactoryIF<ValueTypeIF> valueTypeFactory() {
		return valueFactory.typeFactory();
	}

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

	@Override
	public MorphicSimplifierIF<MorphicVector<ValueIF>> valueVectorSimplifier() {
		return valueVectorSimplifier;
	}

	@Override
	public VectorElementReferenceValueIF vectorElementReference(
			ReferenceValueIF vectorReference, int index) {
		return valueFactory.vectorElementReferenceValue(vectorReference, index);
	}

	@Override
	public VectorElementReferenceValueIF vectorElementReference(
			ReferenceValueIF vectorReference, int index,
			ReferenceValueTypeIF referenceType) {
		return valueFactory.vectorElementReferenceValue(vectorReference, index,
				referenceType);
	}

	@Override
	public VectorValueTypeIF vectorValueType(ValueTypeIF elementType) {
		return typeFactory.vectorValueType(elementType);
	}

	@Override
	public ReferenceValueTypeIF voidPointerType() {
		return voidPointerType;
	}

	@Override
	public ValueIF zero() {
		return zero;
	}

	@Override
	public ArrayValueIF arrayLambda(ValueIF assumption,
			ArrayValueTypeIF arrayValueType, ValueIF function) {
		ArrayValueIF result;
		SymbolicCompleteArrayTypeIF arraySymbolicType = (SymbolicCompleteArrayTypeIF) typeFactory
				.symType(arrayValueType);
		SymbolicExpressionIF symbolicFunction = valueFactory
				.symExpression(function);
		SymbolicExpressionIF origin = universe.arrayLambda(arraySymbolicType,
				symbolicFunction);

		result = valueFactory.arrayValue(origin, arrayValueType);
		return result;
	}

	@Override
	public ValueIF lambda(ValueIF assumption, ValueTypeIF domainValueType,
			SymbolicConstantIF symbolicConstant, ValueIF expression) {
		SymbolicExpressionIF symExpression = valueFactory
				.symExpression(expression);
		SymbolicExpressionIF symLambda = universe.lambda(symbolicConstant,
				symExpression);
		FunctionValueTypeIF functionType = typeFactory.functionValueType(
				expression.valueType(), new ValueTypeIF[] { domainValueType });
		SymbolicExpressionIF symAssumption = valueFactory
				.symExpression(assumption);
		ValueIF result = valueFactory.symbolicValue(symAssumption, symLambda,
				functionType);

		return result;
	}

	@Override
	public ValueIF valueOfSymbolicConstant(SymbolicConstantIF symbolicConstant,
			ValueTypeIF valueType) {
		return valueFactory.symbolicValue(
				universe.symbolicConstantExpression(symbolicConstant),
				valueType);
	}

	@Override
	public ValueIF string(String string) {
		char[] array = string.toCharArray();
		int numChars = array.length;
		ValueIF lengthValue = symbolicValue(numChars);
		ArrayValueTypeIF valueType = arrayValueType(characterValueType,
				lengthValue);
		ValueIF[] valueArray = new ValueIF[numChars];

		for (int i = 0; i < numChars; i++)
			valueArray[i] = symbolicValue(array[i]);
		return arrayValue(valueType, valueArray);
	}
}