public class StructurallyEquivalentHeap extends AbstractSyntacticHeap implements SyntacticHeap {
	private final SyntacticHeap parent;
	/**
	 * @param parent
	 */
	public StructurallyEquivalentHeap(SyntacticHeap parent) {
		this.parent = parent;
		//
		for(int i=0;i<parent.size();i++) {
			// dummy
			syntacticItems.add(parent.getSyntacticItem(i));
		}
	}

	@Override
	public SyntacticHeap getParent() {
		return parent;
	}

	@Override
	public <T extends SyntacticItem> T allocate(T item) {
		return allocate(item,new IdentityHashMap<>());
	}

	private <T extends SyntacticItem> T allocate(T item, Map<SyntacticItem,SyntacticItem> map) {
		//
		SyntacticHeap parent = item.getHeap();
		T allocated = (T) map.get(item);
		if(allocated != null) {
			return allocated;
		} else if (parent == this || parent == this.parent) {
			// Item already allocated to this heap, hence return its existing
			// address.
			return item;
		} else {
			// We need to recursively descend into children of this item
			// allocating them all to this heap.
			SyntacticItem[] children = item.getAll();
			// Initially, this will alias children. In the event of a child
			// which is actually updated, then this will refer to a new
			// array. That will be the signal that we need to create a new
			// item to return.
			SyntacticItem[] nChildren = new SyntacticItem[item.size()];
			if (children != null) {
				for (int i = 0; i != children.length; ++i) {
					SyntacticItem child = children[i];
					// Check for null, since we don't want to try and
					// substitute into null.
					if (child != null) {
						// Perform the substitution in the given child
						nChildren[i] = allocate(child, map);
					}
				}
			}
			T nItem = (T) item.clone(nChildren);
			// Look for any structural equivalents that exist
			// already in this heap. If we find one, then we can
			// just return the directly.
			T equivalent = (T) findStructuralEquivalent(nItem, item.getClass());
			//
			if (equivalent == null) {
				// Allocate the item (or its clone) into this heap.
				int index = syntacticItems.size();
				syntacticItems.add(nItem);
				nItem.allocate(this, index);
			} else {
				nItem = equivalent;
			}
			map.put(item,nItem);
			return nItem;
		}
	}

	/**
	 * Look for a structurally equivalent node in the current heap, assuming
	 * that all children are already allocated (and, hence, for which the
	 * invariant is already true).
	 *
	 * @param opcode
	 * @param data
	 * @param children
	 * @return
	 */
	private SyntacticItem findStructuralEquivalent(SyntacticItem item, Class<?> clazz) {
		for (int i = 0; i != syntacticItems.size(); ++i) {
			SyntacticItem candidate = getSyntacticItem(i);
			if(candidate.getClass() == clazz && item.equals(candidate)) {
				return candidate;
			}
		}
		return null;
	}

	private boolean haveIdenticalChildren(SyntacticItem[] left, SyntacticItem[] right) {
		if (left == null || right == null) {
			return left == right;
		} else if (left.length != right.length) {
			return false;
		} else if(left.getClass().equals(right.getClass())){
			for (int j = 0; j != left.length; ++j) {
				if (left[j] != right[j]) {
					return false;
				}
			}
			return true;
		} else {
			return false;
		}
	}
} public class WyalFile extends AbstractCompilationUnit<WyalFile> {

	// =========================================================================
	// Content Type
	// =========================================================================

	public static final Content.Type<WyalFile> ContentType = new Content.Type<WyalFile>() {
		public Path.Entry<WyalFile> accept(Path.Entry<?> e) {
			if (e.contentType() == this) {
				return (Path.Entry<WyalFile>) e;
			}
			return null;
		}

		@Override
		public WyalFile read(Path.Entry<WyalFile> e, InputStream input) throws IOException {
			WyalFileLexer wlexer = new WyalFileLexer(e);
			WyalFileParser wfr = new WyalFileParser(new WyalFile(e), wlexer.scan());
			return wfr.read();
		}

		@Override
		public void write(OutputStream output, WyalFile module) throws IOException {
			new WyalFilePrinter(output).write(module);
		}

		@Override
		public String toString() {
			return "Content-Type: wyal";
		}

		@Override
		public String getSuffix() {
			return "wyal";
		}
	};

	public static final Content.Type<WyalFile> BinaryContentType = new Content.Type<WyalFile>() {
		public Path.Entry<WyalFile> accept(Path.Entry<?> e) {
			if (e.contentType() == this) {
				return (Path.Entry<WyalFile>) e;
			}
			return null;
		}

		@Override
		public WyalFile read(Path.Entry<WyalFile> e, InputStream input) throws IOException {
			throw new RuntimeException("Implement me!");
		}

		@Override
		public void write(OutputStream output, WyalFile module) throws IOException {
			// FIXME: this is screwed
			//throw new RuntimeException("Implement me!");
		}

		@Override
		public String toString() {
			return "Content-Type: wycs";
		}

		@Override
		public String getSuffix() {
			return "wycs";
		}
	};

	// =========================================================================
	// Item Kinds
	// =========================================================================
	// DECLARATIONS: 00010000 (16) -- 00011111 (31)
	public static final int DECL_mask = 0b00010000;
	public static final int DECL_linecomment = DECL_mask + 0;
	public static final int DECL_blkcomment = DECL_mask + 1;
	public static final int DECL_import = DECL_mask + 2;
	public static final int DECL_assert = DECL_mask + 3;
	public static final int DECL_type = DECL_mask + 4;
	public static final int DECL_fun = DECL_mask + 5;
	public static final int DECL_macro = DECL_mask + 6;
	// ERRORS
	public static final int ERR_verify = DECL_mask + 7;
	// TYPES: 00100000 (32) -- 00111111 (63)
	public static final int TYPE_mask = 0b000100000;
	public static final int TYPE_void = TYPE_mask + 0;
	public static final int TYPE_any = TYPE_mask + 1;
	public static final int TYPE_null = TYPE_mask + 2;
	public static final int TYPE_bool = TYPE_mask + 3;
	public static final int TYPE_int = TYPE_mask + 4;
	public static final int TYPE_nom = TYPE_mask + 5;
	public static final int TYPE_ref = TYPE_mask + 6;
	public static final int TYPE_arr = TYPE_mask + 8;
	public static final int TYPE_rec = TYPE_mask + 9;
	public static final int TYPE_fun = TYPE_mask + 10;
	public static final int TYPE_meth = TYPE_mask + 11;
	public static final int TYPE_property = TYPE_mask + 12;
	public static final int TYPE_inv = TYPE_mask + 13;
	public static final int TYPE_or = TYPE_mask + 14;
	public static final int TYPE_and = TYPE_mask + 15;
	public static final int TYPE_not = TYPE_mask + 16;
	public static final int TYPE_byte = TYPE_mask + 17;
	// STATEMENTS: 01000000 (64) -- 001011111 (95)
	public static final int STMT_mask = 0b01000000;
	public static final int STMT_block = STMT_mask + 0;
	public static final int STMT_vardecl = STMT_mask + 1;
	public static final int STMT_ifthen = STMT_mask + 2;
	public static final int STMT_caseof = STMT_mask + 3;
	public static final int STMT_exists = STMT_mask + 4;
	public static final int STMT_forall = STMT_mask + 5;
	// EXPRESSIONS: 01100000 (96) -- 10011111 (159)
	public static final int EXPR_mask = 0b01100000;
	public static final int EXPR_varcopy = EXPR_mask + 0;
	public static final int EXPR_varmove = EXPR_mask + 1;
	public static final int EXPR_staticvar = EXPR_mask + 2;
	public static final int EXPR_const = EXPR_mask + 3;
	public static final int EXPR_cast = EXPR_mask + 4;
	public static final int EXPR_invoke = EXPR_mask + 5;
	public static final int EXPR_qualifiedinvoke = EXPR_mask + 6;
	public static final int EXPR_indirectinvoke = EXPR_mask + 7;
	// LOGICAL
	public static final int EXPR_not = EXPR_mask + 8;
	public static final int EXPR_and = EXPR_mask + 9;
	public static final int EXPR_or = EXPR_mask + 10;
	public static final int EXPR_implies = EXPR_mask + 11;
	public static final int EXPR_iff = EXPR_mask + 12;
	public static final int EXPR_exists = EXPR_mask + 13;
	public static final int EXPR_forall = EXPR_mask + 14;
	// COMPARATORS
	public static final int EXPR_eq = EXPR_mask + 16;
	public static final int EXPR_neq = EXPR_mask + 17;
	public static final int EXPR_lt = EXPR_mask + 18;
	public static final int EXPR_lteq = EXPR_mask + 19;
	public static final int EXPR_gt = EXPR_mask + 20;
	public static final int EXPR_gteq = EXPR_mask + 21;
	public static final int EXPR_is = EXPR_mask + 22;
	// ARITHMETIC
	public static final int EXPR_neg = EXPR_mask + 24;
	public static final int EXPR_add = EXPR_mask + 25;
	public static final int EXPR_sub = EXPR_mask + 26;
	public static final int EXPR_mul = EXPR_mask + 27;
	public static final int EXPR_div = EXPR_mask + 28;
	public static final int EXPR_rem = EXPR_mask + 29;
	// BITWISE
	public static final int EXPR_bitwisenot = EXPR_mask + 32;
	public static final int EXPR_bitwiseand = EXPR_mask + 33;
	public static final int EXPR_bitwiseor = EXPR_mask + 34;
	public static final int EXPR_bitwisexor = EXPR_mask + 35;
	public static final int EXPR_bitwiseshl = EXPR_mask + 36;
	public static final int EXPR_bitwiseshr = EXPR_mask + 37;
	// REFERENCES
	public static final int EXPR_deref = EXPR_mask + 40;
	public static final int EXPR_new = EXPR_mask + 41;
	public static final int EXPR_qualifiedlambda = EXPR_mask + 42;
	public static final int EXPR_lambda = EXPR_mask + 43;
	// RECORDS
	public static final int EXPR_recfield = EXPR_mask + 48;
	public static final int EXPR_recupdt = EXPR_mask + 49;
	public static final int EXPR_recinit = EXPR_mask + 50;
	// ARRAYS
	public static final int EXPR_arridx = EXPR_mask + 56;
	public static final int EXPR_arrlen = EXPR_mask + 57;
	public static final int EXPR_arrupdt = EXPR_mask + 58;
	public static final int EXPR_arrgen = EXPR_mask + 59;
	public static final int EXPR_arrinit = EXPR_mask + 60;
	public static final int EXPR_arrrange = EXPR_mask + 61;

	// =========================================================================
	// Constructors
	// =========================================================================

	public WyalFile(Path.Entry<WyalFile> entry) {
		super(entry);
	}

	@Override
	public Path.Entry<WyalFile> getEntry() {
		return entry;
	}

	@Override
	public SyntacticHeap getParent() {
		return null;
	}

	// ============================================================
	// Fundamental Items
	// ============================================================


	// ============================================================
	// Declarations
	// ============================================================
	public static interface Declaration extends CompilationUnit.Declaration {

		public static class Assert extends AbstractSyntacticItem implements Declaration {
			private String message;
			private SyntacticItem context;

			public Assert(Stmt.Block body, String message, SyntacticItem context) {
				super(DECL_assert, body);
				this.message = message;
				this.context = context;
			}

			public Stmt.Block getBody() {
				return (Stmt.Block) get(0);
			}

			public SyntacticItem getContext() {
				return context;
			}

			public String getMessage() {
				return message;
			}

			@Override
			public Assert clone(SyntacticItem[] operands) {
				return new Assert((Stmt.Block) operands[0], message, context);
			}

			@Override
			public String toString() {
				return "assert " + getBody();
			}
		}

		public static interface Named extends Declaration {

			public Name getName();

			public Tuple<VariableDeclaration> getParameters();

			public static abstract class FunctionOrMacro extends AbstractSyntacticItem implements Named {
				public FunctionOrMacro(Name name, Tuple<VariableDeclaration> parameters, Stmt.Block body) {
					super(DECL_macro, name, parameters, body);
				}

				public FunctionOrMacro(Name name, Tuple<VariableDeclaration> parameters,
						Tuple<VariableDeclaration> returns) {
					super(DECL_fun, name, parameters, returns);
				}

				@Override
				public Name getName() {
					return (Name) get(0);
				}

				@Override
				public Tuple<VariableDeclaration> getParameters() {
					return (Tuple) get(1);
				}

				public abstract WyalFile.Type.FunctionOrMethodOrProperty getSignatureType();
			}

			// ============================================================
			// Function Declaration
			// ============================================================
			public static class Function extends FunctionOrMacro {

				public Function(Name name, VariableDeclaration[] parameters, VariableDeclaration[] returns) {
					super(name, new Tuple(parameters), new Tuple(returns));
				}

				public Function(Name name, Tuple<VariableDeclaration> parameters,
						Tuple<VariableDeclaration> returns) {
					super(name, parameters, returns);
				}

				public Tuple<VariableDeclaration> getReturns() {
					return (Tuple<VariableDeclaration>) get(2);
				}

				@Override
				public WyalFile.Type.Function getSignatureType() {
					return new WyalFile.Type.Function(projectTypes(getParameters()), projectTypes(getReturns()));
				}

				@Override
				public Function clone(SyntacticItem[] operands) {
					return new Function((Name) operands[0], (Tuple) operands[1], (Tuple) operands[2]);
				}
			}

			// ============================================================
			// Macro Declaration
			// ============================================================
			public static class Macro extends FunctionOrMacro {
				public Macro(Name name, VariableDeclaration[] parameters, Stmt.Block body) {
					super(name, new Tuple<>(parameters), body);
				}

				private Macro(Name name, Tuple<VariableDeclaration> parameters, Stmt.Block body) {
					super(name, parameters, body);
				}

				public Stmt.Block getBody() {
					return (Stmt.Block) get(2);
				}

				@Override
				public WyalFile.Type.Property getSignatureType() {
					return new WyalFile.Type.Property(projectTypes(getParameters()));
				}

				@Override
				public Macro clone(SyntacticItem[] operands) {
					return new Macro((Name) operands[0], (Tuple<VariableDeclaration>) operands[1],
							(Stmt.Block) operands[2]);
				}
			}

			// ============================================================
			// Type Declaration
			// ============================================================
			public static class Type extends AbstractSyntacticItem implements Named {

				public Type(Name name, VariableDeclaration vardecl, Stmt.Block... invariant) {
					super(DECL_type, name, vardecl, new Tuple(invariant));
				}

				private Type(Name name, VariableDeclaration vardecl, Tuple<Stmt.Block> invariant) {
					super(DECL_type, name, vardecl, invariant);
				}

				@Override
				public Name getName() {
					return (Name) get(0);
				}

				public VariableDeclaration getVariableDeclaration() {
					return (VariableDeclaration) get(1);
				}

				public Tuple<Stmt.Block> getInvariant() {
					return (Tuple) get(2);
				}

				@Override
				public Type clone(SyntacticItem[] operands) {
					return new Type((Name) operands[0], (VariableDeclaration) operands[1], (Tuple) operands[2]);
				}

				@Override
				public Tuple<VariableDeclaration> getParameters() {
					return new Tuple<>(getVariableDeclaration());
				}
			}
		}
	}

	// ============================================================
	// Types
	// ============================================================
	public static interface Type extends SyntacticItem {

		public static final Any Any = new Any();
		public static final Void Void = new Void();
		public static final Bool Bool = new Bool();
		public static final Int Int = new Int();
		public static final Null Null = new Null();

		public interface Primitive extends Type {

		}

		public static abstract class Atom extends AbstractSyntacticItem implements Type {
			public Atom(int opcode) {
				super(opcode);
			}

			public Atom(int opcode, SyntacticItem item) {
				super(opcode, item);
			}

			public Atom(int opcode, SyntacticItem first, SyntacticItem second) {
				super(opcode, first, second);
			}

			public Atom(int opcode, SyntacticItem[] items) {
				super(opcode, items);
			}
		}

		/**
		 * The type <code>any</code> represents the type whose variables may hold
		 * any possible value. <b>NOTE:</b> the any type is top in the type lattice.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Any extends Atom implements Primitive {
			public Any() {
				super(TYPE_any);
			}

			@Override
			public Any clone(SyntacticItem[] operands) {
				return new Any();
			}

			@Override
			public String toString() {
				return "any";
			}
		}

		/**
		 * A void type represents the type whose variables cannot exist! That is,
		 * they cannot hold any possible value. Void is used to represent the return
		 * type of a function which does not return anything. However, it is also
		 * used to represent the element type of an empty list of set. <b>NOTE:</b>
		 * the void type is a subtype of everything; that is, it is bottom in the
		 * type lattice.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Void extends Atom implements Primitive {
			public Void() {
				super(TYPE_void);
			}

			@Override
			public Void clone(SyntacticItem[] operands) {
				return new Void();
			}

			@Override
			public String toString() {
				return "void";
			}
		}

		/**
		 * The null type is a special type which should be used to show the absence
		 * of something. It is distinct from void, since variables can hold the
		 * special <code>null</code> value (where as there is no special "void"
		 * value). With all of the problems surrounding <code>null</code> and
		 * <code>NullPointerException</code>s in languages like Java and C, it may
		 * seem that this type should be avoided. However, it remains a very useful
		 * abstraction to have around and, in Whiley, it is treated in a completely
		 * safe manner (unlike e.g. Java).
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Null extends Atom implements Primitive {
			public Null() {
				super(TYPE_null);
			}

			@Override
			public Null clone(SyntacticItem[] operands) {
				return new Null();
			}

			@Override
			public String toString() {
				return "null";
			}
		}

		/**
		 * Represents the set of boolean values (i.e. true and false)
		 * @author David J. Pearce
		 *
		 */
		public static class Bool extends Atom implements Primitive {
			public Bool() {
				super(TYPE_bool);
			}

			@Override
			public Bool clone(SyntacticItem[] operands) {
				return new Bool();
			}

			@Override
			public String toString() {
				return "bool";
			}
		}

		/**
		 * Represents a sequence of 8 bits. Note that, unlike many languages, there
		 * is no representation associated with a byte. For example, to extract an
		 * integer value from a byte, it must be explicitly decoded according to
		 * some representation (e.g. two's compliment) using an auxillary function
		 * (e.g. <code>Byte.toInt()</code>).
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Byte extends Atom implements Primitive {
			public Byte() {
				super(TYPE_byte);
			}

			@Override
			public Null clone(SyntacticItem[] operands) {
				return new Null();
			}

			@Override
			public String toString() {
				return "byte";
			}
		}

		/**
		 * Represents the set of (unbound) integer values. Since integer types in
		 * Whiley are unbounded, there is no equivalent to Java's
		 * <code>MIN_VALUE</code> and <code>MAX_VALUE</code> for <code>int</code>
		 * types.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Int extends Atom implements Primitive {
			public Int() {
				super(TYPE_int);
			}

			@Override
			public Int clone(SyntacticItem[] operands) {
				return new Int();
			}

			@Override
			public String toString() {
				return "int";
			}
		}

		/**
		 * Represents a list type, which is of the form:
		 *
		 * <pre>
		 * ArrayType ::= Type '[' ']'
		 * </pre>
		 *
		 * @return
		 */
		public static class Array extends Atom {
			public Array(Type element) {
				super(TYPE_arr, element);
			}

			public Type getElement() {
				return (Type) get(0);
			}

			@Override
			public Array clone(SyntacticItem[] operands) {
				return new Array((Type) operands[0]);
			}

			@Override
			public String toString() {
				return "(" + getElement() + ")[]";
			}
		}

		/**
		 * Parse a reference type, which is of the form:
		 *
		 * <pre>
		 * ReferenceType ::= '&' Type
		 * </pre>
		 *
		 * @return
		 */
		public static class Reference extends Atom {
			public Reference(Type element, Identifier lifetime) {
				super(TYPE_ref, element, lifetime);
			}

			public Type getElement() {
				return (Type) get(0);
			}
			public Identifier getLifetime() {
				return (Identifier) get(1);
			}

			@Override
			public Reference clone(SyntacticItem[] operands) {
				return new Reference((Type) operands[0], (Identifier) operands[1]);
			}

			@Override
			public String toString() {
				Identifier lifetime = getLifetime();
				if (lifetime != null) {
					return "&(" + getElement() + ")";
				} else {
					return "&" + lifetime + ":(" + getElement() + ")";
				}
			}
		}

		/**
		 * Represents record type, which is of the form:
		 *
		 * <pre>
		 * RecordType ::= '{' Type Identifier (',' Type Identifier)* [ ',' "..." ] '}'
		 * </pre>
		 *
		 * @return
		 */
		public static class Record extends Atom {
			public Record(boolean isOpen, FieldDeclaration[] fields) {
				super(TYPE_rec, ArrayUtils.append(SyntacticItem.class, new Value.Bool(isOpen), fields));
			}

			private Record(SyntacticItem[] operands) {
				super(TYPE_rec, operands);
			}

			public boolean isOpen() {
				Value.Bool flag = (Value.Bool) get(0);
				return flag.get();
			}

			public FieldDeclaration[] getFields() {
				// FIXME: this should be packed as a Tuple and return a Tuple
				SyntacticItem[] operands = getAll();
				FieldDeclaration[] fields = new FieldDeclaration[size() - 1];
				System.arraycopy(operands, 1, fields, 0, fields.length);
				return fields;
			}

			@Override
			public Record clone(SyntacticItem[] operands) {
				return new Record(operands);
			}

			@Override
			public String toString() {
				String r = "{";
				FieldDeclaration[] fields = getFields();
				for (int i = 0; i != fields.length; ++i) {
					if (i != 0) {
						r += ",";
					}
					FieldDeclaration field = fields[i];
					r += field.getType() + " " + field.getVariableName();
				}
				if (isOpen()) {
					if (fields.length > 0) {
						r += ", ...";
					} else {
						r += "...";
					}
				}
				return r + "}";
			}
		}

		/**
		 * Represents a nominal type, which is of the form:
		 *
		 * <pre>
		 * NominalType ::= Identifier ('.' Identifier)*
		 * </pre>
		 *
		 * A nominal type specifies the name of a type defined elsewhere. In some
		 * cases, this type can be expanded (or "inlined"). However, visibility
		 * modifiers can prevent this and, thus, give rise to true nominal types.
		 *
		 * @return
		 */
		public static class Nominal extends AbstractSyntacticItem implements Type {
			public Nominal(Name name) {
				super(TYPE_nom, name);
			}

			public Name getName() {
				return (Name) get(0);
			}

			@Override
			public Nominal clone(SyntacticItem[] operands) {
				return new Nominal((Name) operands[0]);
			}

			@Override
			public String toString() {
				return getName().toString();
			}
		}

		/**
		 * Parse a negation type, which is of the form:
		 *
		 * <pre>
		 * ReferenceType ::= '!' Type
		 * </pre>
		 *
		 * @return
		 */
		public static class Negation extends AbstractSyntacticItem implements Type {
			public Negation(Type element) {
				super(TYPE_not, element);
			}

			public Type getElement() {
				return (Type) get(0);
			}

			@Override
			public Negation clone(SyntacticItem[] operands) {
				return new Negation((Type) operands[0]);
			}

			@Override
			public String toString() {
				return "!(" + getElement() + ")";
			}
		}

		public abstract static class UnionOrIntersection extends AbstractSyntacticItem implements Type {
			public UnionOrIntersection(int kind, Type[] types) {
				super(kind, types);
			}

			@Override
			public Type get(int i) {
				return (Type) super.get(i);
			}

			@Override
			public Type[] getAll() {
				return (Type[]) super.getAll();
			}
		}

		/**
		 * Represents a union type, which is of the form:
		 *
		 * <pre>
		 * UnionType ::= IntersectionType ('|' IntersectionType)*
		 * </pre>
		 *
		 * Union types are used to compose types together. For example, the type
		 * <code>int|null</code> represents the type which is either an
		 * <code>int</code> or <code>null</code>.
		 *
		 * @return
		 */
		public static class Union extends UnionOrIntersection {
			public Union(Type[] types) {
				super(TYPE_or, types);
			}

			@Override
			public Union clone(SyntacticItem[] operands) {
				return new Union(ArrayUtils.toArray(Type.class,operands));
			}

			@Override
			public String toString() {
				String r = "";
				for (int i = 0; i != size(); ++i) {
					if (i != 0) {
						r += "|";
					}
					r += get(i);
				}
				return "(" + r + ")";
			}
		}

		/**
		 * Represents an intersection type, which is of the form:
		 *
		 * <pre>
		 * IntersectionType ::= BaseType ('&' BaseType)*
		 * </pre>
		 *
		 * Intersection types are used to unify types together. For example, the
		 * type <code>{int x, int y}&MyType</code> represents the type which is both
		 * an instanceof of <code>{int x, int y}</code> and an instance of
		 * <code>MyType</code>.
		 *
		 * @return
		 */
		public static class Intersection extends UnionOrIntersection {
			public Intersection(Type[] types) {
				super(TYPE_and, types);
			}

			@Override
			public Intersection clone(SyntacticItem[] operands) {
				return new Intersection(ArrayUtils.toArray(Type.class, operands));
			}

			@Override
			public String toString() {
				String r = "";
				for (int i = 0; i != size(); ++i) {
					if (i != 0) {
						r += "&";
					}
					r += get(i);
				}
				return "(" + r + ")";
			}
		}

		public static abstract class FunctionOrMacroOrInvariant extends Atom implements Type {
			public FunctionOrMacroOrInvariant(int opcode, Tuple<Type> parameters, Tuple<Type> returns) {
				super(opcode, parameters, returns);
			}
			public FunctionOrMacroOrInvariant(int opcode, SyntacticItem[] items) {
				super(opcode, items);
			}
			public Tuple<Type> getParameters() {
				return (Tuple<Type>) get(0);
			}

			public Tuple<Type> getReturns() {
				return (Tuple<Type>) get(1);
			}

			@Override
			public String toString() {
				return getParameters() + "->" + getReturns();
			}
		}

		public static abstract class FunctionOrMethodOrProperty extends FunctionOrMacroOrInvariant {
			public FunctionOrMethodOrProperty(int opcode, Tuple<Type> parameters, Tuple<Type> returns) {
				super(opcode, parameters, returns);
			}
			public FunctionOrMethodOrProperty(int opcode, SyntacticItem[] operands) {
				super(opcode, operands);
			}
		}

		public static class Function extends FunctionOrMethodOrProperty implements Type {
			public Function(Type[] parameters, Type[] returns) {
				super(TYPE_fun, new Tuple(parameters), new Tuple(returns));
			}
			public Function(Tuple<Type> parameters, Tuple<Type> returns) {
				super(TYPE_fun, parameters, returns);
			}

			@Override
			public Function clone(SyntacticItem[] operands) {
				return new Function((Tuple<Type>) operands[0], (Tuple<Type>) operands[1]);
			}

			@Override
			public String toString() {
				return "function" + super.toString();
			}
		}

		public static class Method extends FunctionOrMethodOrProperty implements Type {

			public Method(Tuple<Type> parameters, Tuple<Type> returns, Tuple<Identifier> contextLifetimes,
					Tuple<Identifier> lifetimeParameters) {
				super(TYPE_meth,
						new SyntacticItem[] { parameters, returns, contextLifetimes, lifetimeParameters });
			}

			@Override
			public Method clone(SyntacticItem[] operands) {
				return new Method((Tuple<Type>) operands[0], (Tuple<Type>) operands[1],
						(Tuple<Identifier>) operands[2], (Tuple<Identifier>) operands[3]);
			}

			public Tuple<Identifier> getContextLifetimes() {
				return (Tuple<Identifier>) get(2);
			}

			public Tuple<Identifier> getLifetimeParameters() {
				return (Tuple<Identifier>) get(3);
			}

			@Override
			public String toString() {
				return "method" + super.toString();
			}
		}

		public static class Property extends FunctionOrMethodOrProperty implements Type {
			public Property(Tuple<Type> parameters) {
				super(TYPE_property, parameters, new Tuple<>(new Type.Bool()));
			}

			private Property(Tuple<Type> parameters, Tuple<Type> returns) {
				super(TYPE_property, parameters, returns);
			}

			@Override
			public Property clone(SyntacticItem[] operands) {
				return new Property((Tuple<Type>) operands[0], (Tuple<Type>) operands[1]);
			}

			@Override
			public String toString() {
				return "macro" + super.toString();
			}
		}

		public static class Invariant extends FunctionOrMacroOrInvariant implements Type {
			public Invariant(Tuple<Type> parameters) {
				super(TYPE_inv, parameters, new Tuple<Type>(new Bool()));
			}

			private Invariant(Tuple<Type> parameters, Tuple<Type> returns) {
				super(TYPE_inv, parameters, returns);
			}

			@Override
			public Invariant clone(SyntacticItem[] operands) {
				return new Invariant((Tuple<Type>) operands[0], (Tuple<Type>) operands[1]);
			}

			@Override
			public String toString() {
				return "invariant" + super.toString();
			}
		}
	}

	// ============================================================
	// Variable Declaration
	// ============================================================

	public static class VariableDeclaration extends AbstractSyntacticItem {
		public VariableDeclaration(Type type, Identifier name) {
			super(STMT_vardecl, type, name);
		}

		public Type getType() {
			return (Type) get(0);
		}

		public Identifier getVariableName() {
			return (Identifier) get(1);
		}

		@Override
		public boolean equals(Object o) {
			// The reason for this is that we want to treat variable
			// declarations specially. The only way that two variable
			// declarations can be considered equal is if they are the same.
			return o == this;
		}

		@Override
		public VariableDeclaration clone(SyntacticItem[] operands) {
			return new VariableDeclaration((Type) operands[0], (Identifier) operands[1]);
		}
	}

	public static class FieldDeclaration extends AbstractSyntacticItem {
		public FieldDeclaration(Type type, Identifier name) {
			super(STMT_vardecl, type, name);
		}

		public Type getType() {
			return (Type) get(0);
		}

		public Identifier getVariableName() {
			return (Identifier) get(1);
		}

		@Override
		public FieldDeclaration clone(SyntacticItem[] operands) {
			return new FieldDeclaration((Type) operands[0], (Identifier) operands[1]);
		}
	}

	// ============================================================
	// Stmt
	// ============================================================

	public interface Stmt extends SyntacticItem {

		public static class Block extends AbstractSyntacticItem implements Stmt {
			public Block(Stmt... stmts) {
				super(STMT_block, stmts);
			}

			@Override
			public Stmt get(int i) {
				return (Stmt) super.get(i);
			}

			@Override
			public Stmt[] getAll() {
				return (Stmt[]) super.getAll();
			}

			@Override
			public Block clone(SyntacticItem[] operands) {
				return new Block(ArrayUtils.toArray(Stmt.class, operands));
			}
		}

		public static abstract class Quantifier extends AbstractSyntacticItem implements Stmt {
			public Quantifier(int opcode, VariableDeclaration[] parameters, Block body) {
				super(opcode, new Tuple<>(parameters), body);
			}

			public Quantifier(int opcode, Tuple<VariableDeclaration> parameters, Block body) {
				super(opcode, parameters, body);
			}

			public Tuple<VariableDeclaration> getParameters() {
				return (Tuple<VariableDeclaration>) get(0);
			}

			public Block getBody() {
				return (Block) get(1);
			}

			@Override
			public abstract Quantifier clone(SyntacticItem[] operands);
		}

		/**
		 * Represents an unbounded universally quantified expression of the form
		 * "<code>forall(T v1, ... T vn): block</code>" where
		 * <code>T1 v1</code> ... <code>Tn vn</code> are the <i>quantified
		 * variable declarations</i> and <code>block</code> is the body
		 * consisting of a statement block
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class UniversalQuantifier extends Quantifier {
			public UniversalQuantifier(VariableDeclaration[] parameters, Block body) {
				super(STMT_forall, new Tuple<>(parameters), body);
			}

			public UniversalQuantifier(Tuple<VariableDeclaration> parameters, Block body) {
				super(STMT_forall, parameters, body);
			}

			@Override
			public Quantifier clone(SyntacticItem[] operands) {
				return new UniversalQuantifier((Tuple<VariableDeclaration>) operands[0],
						(Block) operands[1]);
			}
		}

		/**
		 * Represents an unbounded existentially quantified expression of the
		 * form "<code>some(T v1, ... T vn): block</code>" where
		 * <code>T1 v1</code> ... <code>Tn vn</code> are the <i>quantified
		 * variable declarations</i> and <code>block</code> is the body
		 * consisting of a statement block.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class ExistentialQuantifier extends Quantifier {
			public ExistentialQuantifier(VariableDeclaration[] parameters, Block body) {
				super(STMT_exists, new Tuple<>(parameters), body);
			}

			public ExistentialQuantifier(Tuple<VariableDeclaration> parameters, Block body) {
				super(STMT_exists, parameters, body);
			}

			@Override
			public Quantifier clone(SyntacticItem[] operands) {
				return new ExistentialQuantifier((Tuple<VariableDeclaration>) operands[0], (Block) operands[1]);
			}
		}

		public static class IfThen extends AbstractSyntacticItem implements Stmt {
			public IfThen(Block ifBlock, Block thenBlock) {
				super(STMT_ifthen, ifBlock, thenBlock);
			}

			public Block getIfBody() {
				return (Block) get(0);
			}

			public Block getThenBody() {
				return (Block) get(1);
			}

			@Override
			public IfThen clone(SyntacticItem[] operands) {
				return new IfThen((Block) operands[0], (Block) operands[1]);
			}
		}

		public static class CaseOf extends AbstractSyntacticItem implements Stmt {
			public CaseOf(Block... cases) {
				super(STMT_caseof, cases);
			}

			@Override
			public Block get(int i) {
				return (Block) super.get(i);
			}

			@Override
			public Block[] getAll() {
				return (Block[]) super.getAll();
			}

			@Override
			public CaseOf clone(SyntacticItem[] operands) {
				return new CaseOf(ArrayUtils.toArray(Block.class, operands));
			}
		}
	}

	public interface Expr extends Stmt {

		// =========================================================================
		// General Expressions
		// =========================================================================

		/**
		 * Represents a cast expression of the form "<code>(T) e</code>" where
		 * <code>T</code> is the <i>cast type</i> and <code>e</code> the
		 * <i>casted expression</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Cast extends AbstractSyntacticItem implements Expr {
			public Cast(Type type, Expr rhs) {
				super(EXPR_cast, type, rhs);
			}

			public Type getCastType() {
				return (Type) super.get(0);
			}

			public Expr getCastedExpr() {
				return (Expr) super.get(1);
			}

			@Override
			public Cast clone(SyntacticItem[] operands) {
				return new Cast((Type) operands[0], (Expr) operands[1]);
			}

			@Override
			public String toString() {
				return "(" + getCastType() + ") " + getCastedExpr();
			}
		}

		/**
		 * Represents the use of a constant within some expression. For example,
		 * in <code>x + 1</code> the expression <code>1</code> is a constant
		 * expression.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Constant extends AbstractSyntacticItem implements Expr {
			public Constant(Value value) {
				super(EXPR_const, value);
			}

			public Value getValue() {
				return (Value) get(0);
			}

			@Override
			public Constant clone(SyntacticItem[] operands) {
				return new Constant((Value) operands[0]);
			}

			@Override
			public String toString() {
				return getValue().toString();
			}
		}

		/**
		 * Represents a <i>type test expression</i> of the form
		 * "<code>e is T</code>" where <code>e</code> is the <i>test
		 * expression</i> and <code>T</code> is the <i>test type</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Is extends AbstractSyntacticItem implements Expr {
			public Is(Expr lhs, Type rhs) {
				super(EXPR_is, lhs, rhs);
			}

			public Expr getTestExpr() {
				return (Expr) get(0);
			}

			public Type getTestType() {
				return (Type) get(1);
			}

			@Override
			public Is clone(SyntacticItem[] operands) {
				return new Is((Expr) operands[0], (Type) operands[1]);
			}

			@Override
			public String toString() {
				return getTestExpr() + " is " + getTestType();
			}
		}

		/**
		 * Represents an invocation of the form "<code>x.y.f(e1,..en)</code>".
		 * Here, <code>x.y.f</code> constitute a <i>partially-</i> or
		 * <i>fully-qualified name</i> and <code>e1</code> ... <code>en</code>
		 * are the <i>argument expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Invoke extends AbstractSyntacticItem implements Expr {

			public Invoke(Type.FunctionOrMacroOrInvariant type, Name name, Integer selector, Expr[] arguments) {
				super(EXPR_invoke, new SyntacticItem[] { type, name,
						selector != null ? new Value.Int(selector) : null, new Tuple<>(arguments) });
			}

			public Invoke(Type.FunctionOrMacroOrInvariant type, Name name, Value.Int selector, Tuple<Expr> arguments) {
				super(EXPR_invoke, new SyntacticItem[] { type, name, selector, arguments });
			}

			public Type.FunctionOrMacroOrInvariant getSignatureType() {
				return (Type.FunctionOrMacroOrInvariant) get(0);
			}

			public void setSignatureType(Type.FunctionOrMacroOrInvariant type) {
				this.setOperand(0, type);
			}

			public Name getName() {
				return (Name) get(1);
			}

			public Value.Int getSelector() {
				return (Value.Int) get(2);
			}

			public Tuple<Expr> getArguments() {
				return (Tuple) get(3);
			}

			@Override
			public Invoke clone(SyntacticItem[] operands) {
				return new Invoke((Type.FunctionOrMacroOrInvariant) operands[0], (Name) operands[1],
						(Value.Int) operands[2], (Tuple) operands[3]);
			}

			@Override
			public String toString() {
				String r = getName().toString();
				r += getArguments();
				r += "#" + getSelector();
				return r;
			}
		}

		/**
		 * Represents an abstract operator expression over one or more
		 * <i>operand expressions</i>. For example. in <code>arr[i+1]</code> the
		 * expression <code>i+1</code> is an operator expression.
		 *
		 * @author David J. Pearce
		 *
		 */
		public abstract static class Operator extends AbstractSyntacticItem implements Expr {
			public Operator(int opcode, Expr... operands) {
				super(opcode, operands);
			}

			@Override
			public Expr get(int i) {
				return (Expr) super.get(i);
			}

			@Override
			public Expr[] getAll() {
				return (Expr[]) super.getAll();
			}

			@Override
			public abstract Expr clone(SyntacticItem[] operands);
		}

		/**
		 * Represents an abstract quantified expression of the form
		 * "<code>forall(T v1, ... T vn).e</code>" or
		 * "<code>exists(T v1, ... T vn).e</code>" where <code>T1 v1</code> ...
		 * <code>Tn vn</code> are the <i>quantified variable declarations</i>
		 * and <code>e</code> is the body.
		 *
		 * @author David J. Pearce
		 *
		 */
		public abstract static class Quantifier extends AbstractSyntacticItem implements Expr {
			public Quantifier(int opcode, VariableDeclaration[] parameters, Expr body) {
				super(opcode, new Tuple<>(parameters), body);
			}

			public Quantifier(int opcode, Tuple<VariableDeclaration> parameters, Expr body) {
				super(opcode, parameters, body);
			}

			public Tuple<VariableDeclaration> getParameters() {
				return (Tuple<VariableDeclaration>) get(0);
			}

			public Expr getBody() {
				return (Expr) get(1);
			}

			@Override
			public abstract Expr clone(SyntacticItem[] operands);
		}

		/**
		 * Represents an unbounded universally quantified expression of the form
		 * "<code>forall(T v1, ... T vn).e</code>" where <code>T1 v1</code> ...
		 * <code>Tn vn</code> are the <i>quantified variable declarations</i>
		 * and <code>e</code> is the body.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class UniversalQuantifier extends Quantifier {
			public UniversalQuantifier(VariableDeclaration[] parameters, Expr body) {
				super(EXPR_forall, new Tuple<>(parameters), body);
			}

			public UniversalQuantifier(Tuple<VariableDeclaration> parameters, Expr body) {
				super(EXPR_forall, parameters, body);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				return new UniversalQuantifier((Tuple<VariableDeclaration>) operands[0],
						(Expr) operands[1]);
			}

			@Override
			public String toString() {
				String r = "forall";
				r += getParameters();
				r += ".";
				r += getBody();
				return r;
			}
		}

		/**
		 * Represents an unbounded existentially quantified expression of the
		 * form "<code>some(T v1, ... T vn).e</code>" where <code>T1 v1</code>
		 * ... <code>Tn vn</code> are the <i>quantified variable
		 * declarations</i> and <code>e</code> is the body.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class ExistentialQuantifier extends Quantifier {
			public ExistentialQuantifier(VariableDeclaration[] parameters, Expr body) {
				super(EXPR_exists, new Tuple<>(parameters), body);
			}

			public ExistentialQuantifier(Tuple<VariableDeclaration> parameters, Expr body) {
				super(EXPR_exists, parameters, body);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				return new ExistentialQuantifier((Tuple<VariableDeclaration>) operands[0], (Expr) operands[1]);
			}

			@Override
			public String toString() {
				String r = "exists";
				r += getParameters();
				r += ".";
				r += getBody();
				return r;
			}
		}

		/**
		 * Represents a use of some variable within an expression. For example,
		 * in <code>x + 1</code> the expression <code>x</code> is a variable
		 * access expression. Every variable access is associated with a
		 * <i>variable declaration</i> that unique identifies which variable is
		 * being accessed.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class VariableAccess extends AbstractSyntacticItem implements Expr {
			public VariableAccess(VariableDeclaration decl) {
				super(EXPR_varcopy, decl);
			}

			public VariableDeclaration getVariableDeclaration() {
				return (VariableDeclaration) get(0);
			}

			@Override
			public VariableAccess clone(SyntacticItem[] operands) {
				return new VariableAccess((VariableDeclaration) operands[0]);
			}

			@Override
			public String toString() {
				return getVariableDeclaration().getVariableName().toString();
			}
		}


		public abstract static class InfixOperator extends Operator {
			public InfixOperator(int opcode, Expr... operands) {
				super(opcode, operands);
			}

			@Override
			public String toString() {
				String str = getOperatorString();
				String r = "";
				for (int i = 0; i != size(); ++i) {
					if (i != 0) {
						r += str;
					}
					r += get(i);
				}
				return r;
			}

			protected abstract String getOperatorString();
		}

		// =========================================================================
		// Logical Expressions
		// =========================================================================
		/**
		 * Represents a <i>logical conjunction</i> of the form
		 * "<code>e1 && .. && en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class LogicalAnd extends InfixOperator {
			public LogicalAnd(Expr... operands) {
				super(EXPR_and, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if(operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new LogicalAnd(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " && ";
			}
		}

		/**
		 * Represents a <i>logical disjunction</i> of the form
		 * "<code>e1 || .. || en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class LogicalOr extends InfixOperator {
			public LogicalOr(Expr... operands) {
				super(EXPR_or, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if(operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new LogicalOr(ArrayUtils.toArray(Expr.class, operands));
			}


			@Override
			protected String getOperatorString() {
				return " && ";
			}
		}

		/**
		 * Represents a <i>logical implication</i> of the form
		 * "<code>e1 ==> ... ==> en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class LogicalImplication extends InfixOperator {
			public LogicalImplication(Expr... operands) {
				super(EXPR_implies, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if(operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new LogicalImplication(ArrayUtils.toArray(Expr.class, operands));
			}


			@Override
			protected String getOperatorString() {
				return " ==> ";
			}
		}

		/**
		 * Represents a <i>logical biconditional</i> of the form
		 * "<code>e1 <==> ... <==> en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class LogicalIff extends InfixOperator {
			public LogicalIff(Expr... operands) {
				super(EXPR_iff, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if(operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new LogicalIff(ArrayUtils.toArray(Expr.class, operands));
			}


			@Override
			protected String getOperatorString() {
				return " <==> ";
			}
		}

		/**
		 * Represents a <i>logical negation</i> of the form "<code>!e</code>"
		 * where <code>e</code> is the <i>operand expression</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class LogicalNot extends Operator {
			public LogicalNot(Expr operand) {
				super(EXPR_not, operand);
			}

			public Expr getOperand() {
				return get(0);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if(operands.length != 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new LogicalNot((Expr) operands[0]);
			}
		}

		// =========================================================================
		// Comparator Expressions
		// =========================================================================

		/**
		 * Represents an equality expression of the form
		 * "<code>e1 == ... == en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Equal extends InfixOperator {
			public Equal(Expr... operands) {
				super(EXPR_eq, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if(operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new Equal(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			public String getOperatorString() {
				return " == ";
			}
		}

		/**
		 * Represents an unequality expression of the form
		 * "<code>e1 != ... != en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class NotEqual extends InfixOperator {
			public NotEqual(Expr... operands) {
				super(EXPR_neq, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if(operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new NotEqual(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " != ";
			}
		}

		/**
		 * Represents a strict <i>inequality expression</i> of the form
		 * "<code>e1 < ... < en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class LessThan extends InfixOperator {
			public LessThan(Expr... operands) {
				super(EXPR_lt, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new LessThan(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " < ";
			}
		}

		/**
		 * Represents a non-strict <i>inequality expression</i> of the form
		 * "<code>e1 <= ... <= en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class LessThanOrEqual extends InfixOperator {
			public LessThanOrEqual(Expr... operands) {
				super(EXPR_lteq, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new LessThanOrEqual(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " <= ";
			}
		}

		/**
		 * Represents a strict <i>inequality expression</i> of the form
		 * "<code>e1 > ... > en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class GreaterThan extends InfixOperator {
			public GreaterThan(Expr... operands) {
				super(EXPR_gt, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new GreaterThan(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " > ";
			}
		}

		/**
		 * Represents a non-strict <i>inequality expression</i> of the form
		 * "<code>e1 >= ... >= en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class GreaterThanOrEqual extends InfixOperator {
			public GreaterThanOrEqual(Expr... operands) {
				super(EXPR_gteq, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new GreaterThanOrEqual(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " >= ";
			}
		}

		// =========================================================================
		// Arithmetic Expressions
		// =========================================================================

		/**
		 * Represents an arithmetic <i>addition expression</i> of the form
		 * "<code>e1 + ... + en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Addition extends InfixOperator {
			public Addition(Expr... operands) {
				super(EXPR_add, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new Addition(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " + ";
			}
		}

		/**
		 * Represents an arithmetic <i>subtraction expression</i> of the form
		 * "<code>e1 - ... - en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Subtraction extends InfixOperator {
			public Subtraction(Expr... operands) {
				super(EXPR_sub, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new Subtraction(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " - ";
			}
		}

		/**
		 * Represents an arithmetic <i>multiplication expression</i> of the form
		 * "<code>e1 * ... * en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Multiplication extends InfixOperator {
			public Multiplication(Expr... operands) {
				super(EXPR_mul, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new Multiplication(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " * ";
			}
		}

		/**
		 * Represents an arithmetic <i>division expression</i> of the form
		 * "<code>e1 / ... / en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Division extends InfixOperator {
			public Division(Expr... operands) {
				super(EXPR_div, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new Division(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " / ";
			}
		}

		/**
		 * Represents an arithmetic <i>remainder expression</i> of the form
		 * "<code>e1 / ... / en</code>" where <code>e1</code> ...
		 * <code>en</code> are the <i>operand expressions</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Remainder extends InfixOperator {
			public Remainder(Expr... operands) {
				super(EXPR_rem, operands);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length <= 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new Remainder(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			protected String getOperatorString() {
				return " % ";
			}
		}

		/**
		 * Represents an arithmetic <i>negation expression</i> of the form
		 * "<code>-e</code>" where <code>e</code> is the <i>operand
		 * expression</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class Negation extends Operator {
			public Negation(Expr operand) {
				super(EXPR_neg, operand);
			}

			public Expr getOperand() {
				return get(0);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length != 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new Negation((Expr) operands[0]);
			}


			@Override
			public String toString() {
				return "-" + getOperand();
			}
		}

		// =========================================================================
		// Reference Expressions
		// =========================================================================
		public static class Dereference extends Operator {
			public Dereference(Expr operand) {
				super(EXPR_deref, operand);
			}

			public Expr getOperand() {
				return get(0);
			}

			@Override
			public Expr clone(SyntacticItem[] operands) {
				if (operands.length != 1) {
					throw new IllegalArgumentException("invalid number of operands");
				}
				return new Dereference((Expr) operands[0]);
			}

			@Override
			public String toString() {
				return "*" + getOperand();
			}
		}

		// =========================================================================
		// Array Expressions
		// =========================================================================

		/**
		 * Represents an <i>array access expression</i> of the form
		 * "<code>arr[e]</code>" where <code>arr</code> is the <i>source
		 * array</i> and <code>e</code> the <i>subscript expression</i>. This
		 * returns the value held in the element determined by <code>e</code>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class ArrayAccess extends Expr.Operator {
			public ArrayAccess(Expr src, Expr index) {
				super(EXPR_arridx, src, index);
			}

			public Expr getSource() {
				return get(0);
			}

			public Expr getSubscript() {
				return get(1);
			}

			@Override
			public ArrayAccess clone(SyntacticItem[] operands) {
				return new ArrayAccess((Expr) operands[0], (Expr) operands[1]);
			}
		}

		/**
		 * Represents an <i>array update expression</i> of the form
		 * "<code>arr[e1:=e2]</code>" where <code>arr</code> is the <i>source
		 * array</i>, <code>e1</code> the <i>subscript expression</i> and
		 * <code>e2</code> is the value expression. This returns a new array
		 * which is equivalent to <code>arr</code> but where the element
		 * determined by <code>e1</code> has the value resulting from
		 * <code>e2</code>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class ArrayUpdate extends Expr.Operator {
			public ArrayUpdate(Expr src, Expr index, Expr value) {
				super(EXPR_arrupdt, src, index, value);
			}

			public Expr getSource() {
				return get(0);
			}

			public Expr getSubscript() {
				return get(1);
			}

			public Expr getValue() {
				return get(2);
			}

			@Override
			public ArrayUpdate clone(SyntacticItem[] operands) {
				return new ArrayUpdate((Expr) operands[0], (Expr) operands[1], (Expr) operands[2]);
			}

			@Override
			public String toString() {
				return getSource() + "[" + getSubscript() + ":=" + getValue() + "]";
			}
		}

		/**
		 * Represents an <i>array initialiser expression</i> of the form
		 * "<code>[e1,...,en]</code>" where <code>e1</code> ... <code>en</code>
		 * are the <i>initialiser expressions</i>. Thus returns a new array made
		 * up from those values resulting from the initialiser expressions.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class ArrayInitialiser extends Expr.Operator {
			public ArrayInitialiser(Expr... elements) {
				super(EXPR_arrinit, elements);
			}

			@Override
			public ArrayInitialiser clone(SyntacticItem[] operands) {
				return new ArrayInitialiser(ArrayUtils.toArray(Expr.class, operands));
			}

			@Override
			public String toString() {
				return Arrays.toString(getAll());
			}
		}

		/**
		 * Represents an <i>array generator expression</i> of the form
		 * "<code>[e1;e2]</code>" where <code>e1</code> is the <i>element
		 * expression</i> and <code>e2</code> is the <i>length expression</i>.
		 * This returns a new array whose length is determined by
		 * <code>e2</code> and where every element has contains the value
		 * determined by <code>e1</code>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class ArrayGenerator extends Expr.Operator {
			public ArrayGenerator(Expr value, Expr length) {
				super(EXPR_arrgen, value, length);
			}

			public Expr getValue() {
				return get(0);
			}

			public Expr getLength() {
				return get(1);
			}

			@Override
			public ArrayGenerator clone(SyntacticItem[] operands) {
				return new ArrayGenerator((Expr) operands[0], (Expr) operands[1]);
			}
		}

		/**
		 * Represents an <i>array length expression</i> of the form
		 * "<code>|arr|</code>" where <code>arr</code> is the <i>source
		 * array</i>. This simply returns the length of array <code>arr</code>.
		 * <code>e</code>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class ArrayLength extends Expr.Operator {
			public ArrayLength(Expr src) {
				super(EXPR_arrlen, src);
			}

			public Expr getSource() {
				return get(0);
			}

			@Override
			public ArrayLength clone(SyntacticItem[] operands) {
				return new ArrayLength((Expr) operands[0]);
			}

			@Override
			public String toString() {
				return "|" + getSource() + "|";
			}
		}

		// =========================================================================
		// Record Expressions
		// =========================================================================

		/**
		 * Represents a <i>record access expression</i> of the form
		 * "<code>rec.f</code>" where <code>rec</code> is the <i>source record</i>
		 * and <code>f</code> is the <i>field</i>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class RecordAccess extends AbstractSyntacticItem implements Expr {
			public RecordAccess(Expr lhs, Identifier rhs) {
				super(EXPR_recfield, lhs, rhs);
			}

			public Expr getSource() {
				return (Expr) get(0);
			}

			public Identifier getField() {
				return (Identifier) get(1);
			}

			@Override
			public RecordAccess clone(SyntacticItem[] operands) {
				return new RecordAccess((Expr) operands[0], (Identifier) operands[1]);
			}

			@Override
			public String toString() {
				return getSource() + "." + getField();
			}
		}

		/**
		 * Represents a <i>record initialiser</i> expression of the form
		 * <code>{ f1: e1, ..., fn: en }</code> where <code>f1: e1</code> ...
		 * <code>fn: en</code> are <i>field initialisers</code>. This returns a
		 * new record where each field holds the value resulting from its
		 * corresponding expression.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class RecordInitialiser extends AbstractSyntacticItem implements Expr {
			public RecordInitialiser(Pair<Identifier, Expr>... fields) {
				super(EXPR_recinit, fields);
			}

			public Pair<Identifier, Expr>[] getFields() {
				return ArrayUtils.toArray(Pair.class, getAll());
			}

			@Override
			public RecordInitialiser clone(SyntacticItem[] operands) {
				return new RecordInitialiser(ArrayUtils.toArray(Pair.class, operands));
			}
		}

		/**
		 * Represents a <i>record update expression</i> of the form
		 * "<code>rec[f:=e]</code>" where <code>rec</code> is the <i>source
		 * record</i>, <code>f</code> is the <i>field</i> and <code>e</code> is
		 * the <i>value expression</i>. This returns a new record which is
		 * equivalent to <code>rec</code> but where the element in field
		 * <code>f</code> has the value resulting from <code>e</code>.
		 *
		 * @author David J. Pearce
		 *
		 */
		public static class RecordUpdate extends AbstractSyntacticItem implements Expr {
			public RecordUpdate(Expr lhs, Identifier mhs, Expr rhs) {
				super(EXPR_recupdt, lhs, mhs, rhs);
			}

			public Expr getSource() {
				return (Expr) get(0);
			}

			public Identifier getField() {
				return (Identifier) get(1);
			}

			public Expr getValue() {
				return (Expr) get(2);
			}

			@Override
			public RecordUpdate clone(SyntacticItem[] operands) {
				return new RecordUpdate((Expr) operands[0], (Identifier) operands[1], (Expr) operands[2]);
			}

			@Override
			public String toString() {
				return getSource() + "{" + getField() + ":=" + getValue() + "}";
			}
		}
	}

	// ============================================================
	// Attributes
	// ============================================================
	public interface Attribute {
//		public class Proof implements wybs.lang.Attribute {
//			private final wytp.proof.Proof proof;
//
//			public Proof(wytp.proof.Proof proof) {
//				this.proof = proof;
//			}
//
//			public wytp.proof.Proof getProof() {
//				return proof;
//			}
//		}
	}
	// ===========================================================
	// Errors
	// ===========================================================
	public static class VerificationError extends AbstractSyntacticItem {

		public VerificationError(Declaration.Assert parent) {
			super(ERR_verify, parent);
		}

		@Override
		public SyntacticItem clone(SyntacticItem[] operands) {
			return new VerificationError((Declaration.Assert) operands[0]);
		}

	}

	// ===========================================================
	// Misc
	// ===========================================================
	public static Tuple<Type> projectTypes(Tuple<VariableDeclaration> decls) {
		Type[] types = new Type[decls.size()];
		for (int i = 0; i != types.length; ++i) {
			types[i] = decls.get(i).getType();
		}
		return new Tuple<>(types);
	}

	// ===========================================================
	// DEBUGGING SUPPORT
	// ===========================================================

	public static void println(Proof.Delta delta) {
		print(delta);
		System.out.println();
	}

	public static void print(Proof.Delta delta) {
		Proof.Delta.Set additions = delta.getAdditions();
		Proof.Delta.Set removals = delta.getRemovals();
		for (int i = 0; i != additions.size(); ++i) {
			if (i != 0) {
				System.out.print(", ");
			}
			System.out.print("+");
			print(additions.get(i));
		}
		for (int i = 0; i != removals.size(); ++i) {
			if (i != 0 || additions.size() > 0) {
				System.out.print(", ");
			}
			System.out.print("-");
			print(removals.get(i));
		}
	}

	public static void println(SyntacticItem... items) {
		print(items);
		System.out.println();
	}

	public static void print(SyntacticItem... items) {
		PrintWriter out = new PrintWriter(System.out);
		WyalFilePrinter printer = new WyalFilePrinter(out);
		for (int i = 0; i != items.length; ++i) {
			if (i != 0) {
				out.print(", ");
			}
			SyntacticItem item = items[i];
			if (item instanceof WyalFile.Expr) {
				printer.writeExpression((Expr) item);
			} else if (item instanceof WyalFile.Stmt) {
				printer.writeStatement((Stmt) item, 0);
			} else if (item instanceof WyalFile.Type) {
				printer.writeType((Type) item);
			} else if (item instanceof WyalFile.VariableDeclaration) {
				printer.writeVariableDeclaration((WyalFile.VariableDeclaration) item);
			} else if (item instanceof WyalFile.Tuple) {
				WyalFile.Tuple tuple = (WyalFile.Tuple) item;
				out.print("(");
				for (int j = 0; j != tuple.size(); ++j) {
					if (j != 0) {
						out.print(",");
					}
					out.flush();
					print(tuple.get(j));
				}
				out.print(")");
			} else if (item == null) {
				out.print("null");
			} else {
				out.print(item);
			}
		}
		out.flush();
	}
} public interface NameResolver {

	/**
	 * <p>
	 * Resolve a given name which occurs at some position in a compilation unit
	 * into exactly one named declaration. Depending on the context, we may be
	 * looking for a specific kind of declaration. For example, for a variable
	 * declaration, we may be looking for the corresponding type declaration.
	 * </p>
	 * <p>
	 * Observe that this method is expecting to find <b>exactly</b> one
	 * corresponding declaration. If it find no such matches or if it finds more
	 * than one match, then a corresponding error will be reported.
	 * </p>
	 * <p>
	 * Resolution is determined by the context in which a given name is used.
	 * For example, what imports are active in the enclosing file, as in the
	 * following:
	 * </p>
	 *
	 * <pre>
	 * import std.*
	 *
	 * type nat is integer.uint
	 * </pre>
	 *
	 * <p>
	 * In resolving the name <code>integer.uint</code>, the resolver will
	 * examine the package <code>std</code> to see whether a compilation unit
	 * named "integer" exists. If so, it will then resolve the name
	 * <code>integer.uint</code> to <code>std.integer.uint</code>.
	 * </p>
	 *
	 * @param name
	 *            The name to be resolved in the given context.
	 * @param kind
	 *            The kind of declaration we are looking for, which can simply
	 *            be <code>Declaration.Named</code> in the case we are looking
	 *            for any kind of declaration.
	 * @return
	 */
	public <T extends Declaration> T resolveExactly(Name name, Class<T> kind) throws ResolutionError;

	/**
	 * <p>
	 * Resolve a given name which occurs at some position in a compilation unit
	 * into one or more named declarations. Depending on the context, we may be
	 * looking for a specific kind of declaration. For example, for a function
	 * invocation expression, we are looking for the corresponding function
	 * declaration.
	 * </p>
	 * <p>
	 * Resolution is determined by the context in which a given name is used.
	 * For example, what imports are active in the enclosing file, as in the
	 * following:
	 * </p>
	 *
	 * <pre>
	 * import std.*
	 *
	 * type nat is integer.uint
	 * </pre>
	 *
	 * <p>
	 * In resolving the name <code>integer.uint</code>, the resolver will
	 * examine the package <code>std</code> to see whether a compilation unit
	 * named "integer" exists. If so, it will then resolve the name
	 * <code>integer.uint</code> to <code>std.integer.uint</code>.
	 * </p>
	 *
	 * @param name
	 *            The name to be resolved in the given context.
	 * @param kind
	 *            The kind of declaration we are looking for, which can simply
	 *            be <code>Declaration.Named</code> in the case we are looking
	 *            for any kind of declaration.
	 * @return
	 */
	public <T extends Declaration> List<T> resolveAll(Name name, Class<T> kind) throws ResolutionError;

	/**
	 * A resolution error occurs when a given name cannot be successfully
	 * resolved. Such errors are typically propagated out of the current
	 * processing method to some kind of generic handler (e.g. for reporting
	 * errors).
	 *
	 * @author David J. Pearce
	 *
	 */
	public static class ResolutionError extends Exception {
		/**
		 *
		 */
		private static final long serialVersionUID = 1L;
		private final Name name;

		public ResolutionError(Name name, String message) {
			super(message);
			if (name == null) {
				throw new IllegalArgumentException("name is null");
			}
			this.name = name;
		}

		/**
		 * Get the name being resolved that lead to this error.
		 *
		 * @return
		 */
		public Name getName() {
			return name;
		}
	}

	/**
	 * This error is reported in the case that no matching name can be
	 * identified.
	 *
	 * @author David J. Pearce
	 *
	 */
	public static class NameNotFoundError extends ResolutionError {
		/**
		 *
		 */
		private static final long serialVersionUID = 1L;

		public NameNotFoundError(Name name) {
			super(name, "name \"" + name + "\" not found");
		}
	}

	/**
	 * This error is reported in the case that exactly one match was sought, but
	 * more than one match was found.
	 *
	 * @author David J. Pearce
	 *
	 */
	public static class AmbiguousNameError extends ResolutionError {
		/**
		 *
		 */
		private static final long serialVersionUID = 1L;

		public AmbiguousNameError(Name name) {
			super(name, "name \"" + name + "\" is ambiguous");
		}
	}
} public static class AmbiguousNameError extends ResolutionError {
	/**
	 *
	 */
	private static final long serialVersionUID = 1L;

	public AmbiguousNameError(Name name) {
		super(name, "name \"" + name + "\" is ambiguous");
	}
} public static class NameNotFoundError extends ResolutionError {
	/**
	 *
	 */
	private static final long serialVersionUID = 1L;

	public NameNotFoundError(Name name) {
		super(name, "name \"" + name + "\" not found");
	}
} public static class ResolutionError extends Exception {
	/**
	 *
	 */
	private static final long serialVersionUID = 1L;
	private final Name name;

	public ResolutionError(Name name, String message) {
		super(message);
		if (name == null) {
			throw new IllegalArgumentException("name is null");
		}
		this.name = name;
	}

	/**
	 * Get the name being resolved that lead to this error.
	 *
	 * @return
	 */
	public Name getName() {
		return name;
	}
} public interface Formula extends Expr {

	@Override
	public Formula clone(SyntacticItem[] children);

	public static class Truth extends Expr.Constant implements Formula {

		public Truth(boolean value) {
			super(new Value.Bool(value));
		}

		public Truth(Value.Bool value) {
			super(value);
		}

		public boolean holds() {
			return getValue().get();
		}

		@Override
		public Value.Bool getValue() {
			return (Value.Bool) super.getValue();
		}

		@Override
		public Truth clone(SyntacticItem[] children) {
			return new Truth((Value.Bool) children[0]);
		}
	}

	public static class Conjunct extends Expr.Operator implements Formula {

		public Conjunct(Formula... operands) {
			super(WyalFile.EXPR_and, operands);
		}

		@Override
		public Formula get(int i) {
			return (Formula) super.get(i);
		}

		@Override
		public Formula[] getAll() {
			return (Formula[]) super.getAll();
		}

		@Override
		public Conjunct clone(SyntacticItem[] children) {
			return new Conjunct(ArrayUtils.toArray(Formula.class, children));
		}

		@Override
		public String toString() {
			String r = "";
			for (int i = 0; i != size(); ++i) {
				if (i != 0) {
					r += " && ";
				}
				r += get(i);
			}
			return r;
		}
	}

	public static class Disjunct extends Expr.Operator implements Formula {

		public Disjunct(Formula... operands) {
			super(WyalFile.EXPR_or, operands);
		}

		@Override
		public Formula get(int i) {
			return (Formula) super.get(i);
		}

		@Override
		public Formula[] getAll() {
			return (Formula[]) super.getAll();
		}

		@Override
		public Disjunct clone(SyntacticItem[] children) {
			return new Disjunct(ArrayUtils.toArray(Formula.class, children));
		}

		@Override
		public String toString() {
			String r = "";
			for (int i = 0; i != size(); ++i) {
				if (i != 0) {
					r += " || ";
				}
				r += get(i);
			}
			return r;
		}
	}

	public static class Quantifier extends Expr.Quantifier implements Formula {
		public Quantifier(boolean sign, VariableDeclaration parameter, Formula body) {
			super(sign ? WyalFile.EXPR_forall : WyalFile.EXPR_exists, new Tuple<>(parameter), body);
		}

		public Quantifier(boolean sign, VariableDeclaration[] parameters, Formula body) {
			super(sign ? WyalFile.EXPR_forall : WyalFile.EXPR_exists,
					new Tuple<>(parameters), body);
		}

		public Quantifier(boolean sign, Tuple<VariableDeclaration> parameters, Formula body) {
			super(sign ? WyalFile.EXPR_forall : WyalFile.EXPR_exists, parameters, body);
		}

		public boolean getSign() {
			return getOpcode() == WyalFile.EXPR_forall;
		}

		@Override
		public Tuple<VariableDeclaration> getParameters() {
			return (Tuple<VariableDeclaration>) get(0);
		}

		@Override
		public Formula getBody() {
			return (Formula) get(1);
		}

		@Override
		public Formula.Quantifier clone(SyntacticItem[] children) {
			return new Formula.Quantifier(getSign(), (Tuple) children[0], (Formula) children[1]);
		}
	}

	public interface Equation extends Formula {
		@Override
		public Expr get(int i);

		@Override
		public Expr[] getAll();
	}

	public interface ArithmeticEquation extends Equation {
		@Override
		public Expr get(int i);

		@Override
		public Expr[] getAll();
	}

	public static class Inequality extends Expr.GreaterThanOrEqual implements ArithmeticEquation {

		public Inequality(Expr lhs, Expr rhs) {
			super(lhs, rhs);
		}

		@Override
		public Inequality clone(SyntacticItem[] children) {
			return new Inequality((Expr) children[0],(Expr) children[1]);
		}
	}

	public static class Equality extends Expr.Operator implements Equation {
		public Equality(boolean sign, Expr lhs, Expr rhs) {
			super(sign ? WyalFile.EXPR_eq : WyalFile.EXPR_neq, lhs, rhs);
		}

		public Equality(boolean sign, Expr[] arr) {
			super(sign ? WyalFile.EXPR_eq : WyalFile.EXPR_neq, arr);
		}

		public boolean getSign() {
			return getOpcode() == WyalFile.EXPR_eq;
		}

		@Override
		public Equality clone(SyntacticItem[] children) {
			return new Equality(getSign(),(Expr) children[0],(Expr) children[1]);
		}

		@Override
		public String toString() {
			String str = getSign() ? " == " : " != ";
			String r = "";
			for (int i = 0; i != size(); ++i) {
				if (i != 0) {
					r += str;
				}
				r += get(i);
			}
			return r;
		}
	}

	public static class ArithmeticEquality extends Equality implements ArithmeticEquation {
		public ArithmeticEquality(boolean sign, Expr lhs, Expr rhs) {
			super(sign, lhs, rhs);
		}

		@Override
		public ArithmeticEquality clone(SyntacticItem[] children) {
			return new ArithmeticEquality(getSign(),(Expr) children[0],(Expr) children[1]);
		}
	}

	public static class Invoke extends Expr.Invoke implements Formula {
		private boolean sign;

		public Invoke(boolean sign, Type.FunctionOrMacroOrInvariant type, Name name, Integer selector,
				Expr... arguments) {
			super(type, name, selector == null ? null : selector, arguments);
			this.sign = sign;
		}

		public Invoke(boolean sign, Type.FunctionOrMacroOrInvariant type, Name name, Value.Int selector,
				Tuple<Expr> arguments) {
			super(type, name, selector, arguments);
			this.sign = sign;
		}

		public boolean getSign() {
			return sign;
		}

		@Override
		public byte[] getData() {
			return new byte[sign?1:0];
		}

		@Override
		public boolean equals(Object o) {
			// FIXME: the need for this method is something of a hack.
			if(o instanceof Formula.Invoke) {
				Formula.Invoke i = (Formula.Invoke) o;
				return sign == i.sign && super.equals(o);
			} else if(o instanceof Expr.Invoke && !sign) {
				return false;
			} else {
				return super.equals(o);
			}
		}

		@Override
		public Formula.Invoke clone(SyntacticItem[] children) {
			return new Formula.Invoke(sign,(Type.FunctionOrMacroOrInvariant) children[0], (Name) children[1],
					(Value.Int) children[2], (Tuple) children[3]);
		}
	}

	public static class Is extends Expr.Is implements Formula {
		public Is(Expr lhs, Type rhs) {
			super(lhs,rhs);
		}

		@Override
		public Formula.Is clone(SyntacticItem[] children) {
			return new Formula.Is((Expr) children[0],(Type) children[1]);
		}
	}
} public interface Proof {

	/**
	 * Get the assertion to which this proof applies.
	 *
	 * @return
	 */
	public Declaration.Assert getAssertion();

	/**
	 * Determine whether or not the proof is complete. That is, whether or not
	 * the proof demonstrates that the given assertion is correct.
	 *
	 * @return
	 */
	public boolean isComplete();

	/**
	 * Determine the number of steps in this proof.
	 *
	 * @return
	 */
	public int size();

	/**
	 * Get the ith step in this proof.
	 *
	 * @param ith
	 * @return
	 */
	public State getState(int ith);

	/**
	 * Get the heap in which this proof is operating within.
	 *
	 * @return
	 */
	public SyntacticHeap getHeap();

	/**
	 * A proof branch considered of one or more states which were derived from
	 * an existing state using a given rule.
	 *
	 * @author David J. Peare
	 *
	 */
	public interface State {
		/**
		 * Get the enclosing proof for this step. Every step must be associated
		 * with a proof, and all connected steps must be in the same proof.
		 *
		 * @return
		 */
		Proof getProof();

		/**
		 * Get the parent (i.e. before) state for this step. This is
		 * <code>null</code> if this state represents the root of the proof.
		 *
		 * @return
		 */
		State getParent();

		/**
		 * Determine whether a truth is already known or not. Truths which are
		 * already known do not need to be reintroduced.
		 *
		 * @param truth
		 * @return
		 */
		boolean isKnown(Formula truth);

		/**
		 * Get the delta between this state and its parent.
		 *
		 * @return
		 */
		Delta getDelta();

		/**
		 * Get the delta between this state and an ancestor.
		 *
		 * @return
		 */
		Delta getDelta(State ancestor);

		/**
		 * Get the name of the rule used for this step.
		 *
		 * @return
		 */
		Rule getRule();

		/**
		 * Get the typing environment at this state in a given proof. The type
		 * environment gives the current type for all declared variables. The
		 * environment is not static as the type of a given variable can be
		 * refined at any given state as more facts become known.
		 *
		 * @return
		 */
		TypeInferer.Environment getTypeEnvironment();

		/**
		 * Get the formulae on which this step depends
		 *
		 * @return
		 */
		List<Formula> getDependencies();

		/**
		 * Get the number of child steps originating from this step
		 *
		 * @return
		 */
		int numberOfChildren();

		/**
		 * Get the child state resulting from this step
		 *
		 * @return
		 */
		State getChild(int ith);

		void applyBypass(State bypass);

		/**
		 * Apply a simple proof step which splits a given disjunct into several
		 * sub-states.
		 *
		 * @param disjunct
		 * @return
		 */
		State[] split(Formula.Disjunct disjunct);

		/**
		 * Subsume a given truth by a replacement.
		 *
		 * @param rule
		 * @param truth
		 * @param replacement
		 * @param dependencies
		 * @return
		 */
		State subsume(Proof.Rule rule, Formula truth, Formula replacement, Formula... dependencies);

		/**
		 * Infer a new fact from one or more existing facts.
		 *
		 * @param rule
		 * @param truth
		 * @param dependencies
		 * @return
		 */
		State infer(Proof.Rule rule, Formula truth, Formula... dependencies);

		/**
		 * Refine the type of a given variable in this state. That is, make the
		 * type more precise at this point.
		 *
		 * @param rule
		 *            The rule which is causing this particular refinement.
		 * @param variable
		 *            The variable whose type is being refined.
		 * @param type
		 *            The type which this variable is refined with.
		 * @param dependencies
		 *            The immediate dependencies needed to establish this
		 *            refinement.
		 *
		 * @return
		 */
		State refine(Proof.Rule rule, WyalFile.VariableDeclaration variable, WyalFile.Type type, Formula... dependencies);

		/**
		 * Ensure a given formula is properly allocated into this state.
		 *
		 * @param f
		 * @return
		 */
		Formula allocate(Formula f);
	}

	/**
	 * A proof delta represents a set of truths which have been introduced
	 * during one or more proof steps.
	 *
	 * @author David J. Pearce
	 *
	 */
	interface Delta {

		/**
		 * Check whether or not a given formula is in the additions set
		 *
		 * @param truth
		 * @return
		 */
		public boolean isAddition(Formula truth);

		/**
		 * Check whether or not a given formula is in the removals set
		 *
		 * @param truth
		 * @return
		 */
		public boolean isRemoval(Formula truth);

		/**
		 * Get the set of truths added to this delta
		 *
		 * @return
		 */
		public Set getAdditions();

		/**
		 * Get the set of truths removed from this delta
		 *
		 * @return
		 */
		public Set getRemovals();

		/**
		 * Add a new formula to this delta
		 *
		 * @param truth
		 * @return
		 */
		public Delta add(Formula truth);

		/**
		 * Remove a truth from this delta (e.g. because it has been processed).
		 *
		 * @param truth
		 * @return
		 */
		public Delta remove(Formula truth);

		/**
		 * Apply a given delta on top of this one.
		 *
		 * @param delta
		 * @return
		 */
		public Delta apply(Delta delta);

		/**
		 * A set of truths in a delta, either representing those added or those
		 * removed.
		 *
		 * @author David J. Pearce
		 *
		 */
		public interface Set {
			/**
			 * Determine the number of truths in this set
			 *
			 * @return
			 */
			public int size();

			/**
			 * Check whether the given formula is contained within this set or
			 * not.
			 *
			 * @param truth
			 * @return
			 */
			public boolean contains(Formula truth);

			/**
			 * Get the ith truth in this set
			 *
			 * @param ith
			 * @return
			 */
			public Formula get(int ith);

			/**
			 * Add a truth to this set.
			 *
			 * @param truth
			 * @return
			 */
			public Set add(Formula truth);

			/**
			 * Remove a formula from this set
			 *
			 * @param truth
			 * @return
			 */
			public Set remove(Formula truth);

			/**
			 * Union two sets together
			 *
			 * @param other
			 * @return
			 */
			public Set union(Proof.Delta.Set other);

			/**
			 * Remove the elements of one set from this
			 *
			 * @param other
			 * @return
			 */
			public Set remove(Proof.Delta.Set other);
		}
	}

	/**
	 * A proof rule represents the transformation of a given proof according to
	 * some logical inference.
	 *
	 * @author David J. Pearce
	 *
	 */
	interface Rule {
		/**
		 * Get the name of this rule
		 * @return
		 */
		public String getName();
	}

	interface LinearRule extends Rule {
		/**
		 * Apply a given rule to a given state, producing one potentially
		 * updated state. If the rule does not apply or produces no additional
		 * information, then the original state is returned untouched.
		 *
		 * @param current
		 *            The current state of truth. That is, everything which is
		 *            known to be true at this point.
		 * @param head
		 *            The current tip of the proof branch. This maybe some
		 *            distance in the future from the current state, and
		 *            identifies truths which have yet to be processed.
		 * @return One or more states representing the remaining states to be
		 *         discharged
		 */
		State apply(State current, State head) throws ResolutionError;
	}

	interface NonLinearRule extends Rule {
		/**
		 * Apply a given rule to a given state, producing one (or more)
		 * potentially updated states. If the rule does not apply or produces no
		 * additional information, then the original state is returned
		 * untouched.
		 *
		 * @param current
		 *            The current state of truth. That is, everything which is
		 *            known to be true at this point.
		 * @param head
		 *            The current tip of the proof branch. This maybe some
		 *            distance in the future from the current state, and
		 *            identifies truths which have yet to be processed.
		 * @return One or more states representing the remaining states to be
		 *         discharged
		 */
		State[] apply(State current, State head) throws ResolutionError;
	}
} public class ProofPrinter {
	private final PrintWriter out;
	private int width = 120;
	private boolean fullDelta = false;

	public ProofPrinter(OutputStream writer) {
		this(new OutputStreamWriter(writer));
	}

	public ProofPrinter(Writer writer) {
		this.out = new PrintWriter(writer);
	}

	public ProofPrinter(PrintWriter writer) {
		this.out = writer;
	}

	public ProofPrinter setWidth(int width) {
		this.width = width;
		return this;
	}

	public ProofPrinter setShowAll(boolean flag) {
		this.fullDelta = flag;
		return this;
	}

	public void flush() {
		out.flush();
	}

	public void print(Proof p) {
		print(0, p.getState(0));
	}

	private static final char BOX_TOP='\u2500';
	private static final char BOX_BOTTOM='\u2500';
	private static final char BOX_SPLIT='\u2500';
	private static final char BOX_LEFTSIDE='\u2502';
	private static final char BOX_TOPLEFTCORNER='\u250c';
	private static final char BOX_TOPRIGHTCORNER='\u2510';
	private static final char BOX_BOTTOMLEFTCORNER='\u2514';
	private static final char BOX_BOTTOMRIGHTCORNER='\u2518';
	private static final char BOX_SPLITLEFT='\u251c';
	private static final char BOX_SPLITRIGHT='\u2524';

	public void print(int depth, Proof.State step) {
		printBoxContents(depth,step);
		// now print any children
		if(step.numberOfChildren() == 0) {
			// do nothing
		} else if(step.numberOfChildren() == 1) {
			print(depth,step.getChild(0));
		} else {
			printOpenBox(depth);
			for(int i=0;i!=step.numberOfChildren();++i) {
				print(depth+1,step.getChild(i));
				if((i+1) != step.numberOfChildren()) {
					printSplitBox(depth);
				}
			}
			printCloseBox(depth);
		}
	}

	public void printBoxContents(int depth, Proof.State step) {
		String[] lines = toLines(step);
		String title = title(step);
		int lineWidth = width - depth;
		lineWidth = depth == 0 ? lineWidth : lineWidth-1;
		for(int i=0;i!=lines.length;++i) {
			String t;
			if(i == 0) {
				t = title;
			} else {
				t = "";
			}
			tab(depth);
			out.print(pad(lines[i],t,lineWidth));
			if(depth > 0) {
				out.print(BOX_LEFTSIDE);
			}
			out.println();
		}
	}
	public void tab(int indent) {
		if(indent > 0) {
			for (int i = 0; i < (indent-1); ++i) {
				out.print(BOX_LEFTSIDE);
			}
			out.print(BOX_LEFTSIDE);
		}
	}


	private String pad(String left, String right, int width) {
		if(width <= 0) {
			return "";
		} else {
			if(right.length() > width) {
				right = right.substring(0, width);
			}
			width -= right.length();
			if(left.length() > width) {
				left = left.substring(0, width);
			} else {
				while(left.length() < width) {
					left = left + " ";
				}
			}
			return left + right;
		}
	}

	private String[] toLines(Proof.State s) {
		Proof.Delta delta = s.getDelta();
		Proof.Delta.Set additions = delta.getAdditions();
		Proof.Delta.Set removals = delta.getRemovals();
		if(fullDelta) {
			// Full delta (usually for debugging)
			String[] lines = new String[additions.size()+removals.size()];
			for(int i=0;i<removals.size();++i) {
				lines[i] = "-" + toLine(removals.get(i));
			}
			for(int i=0;i<additions.size();++i) {
				lines[i+removals.size()] = "+" + toLine(additions.get(i));
			}
			return lines;
		} else {
			// Half delta
			String[] lines = new String[additions.size()];
			for(int i=0;i!=lines.length;++i) {
				lines[i] = toLine(additions.get(i));
			}
			return lines;
		}
	}

	private String title(Proof.State step) {
		String title = " (";
		if(step.getRule() != null) {
			title += step.getRule().getName();
			title += " ";
		}
		List<Formula> deps = step.getDependencies();
		for(int j=0;j<deps.size();++j) {
			if(j != 0) {
				title += ",";
			}
			title = title + deps.get(j).getIndex();
		}
		return title + ") ";
	}

	private String toLine(WyalFile.Expr e) {
		ByteArrayOutputStream out = new ByteArrayOutputStream();
		PrintWriter pw = new PrintWriter(out);
		WyalFilePrinter printer = new WyalFilePrinter(pw);
		pw.print(" " + e.getIndex() + ". ");
		printer.writeExpression(e);
		printer.flush();
		return new String(out.toByteArray());
	}


	private void printOpenBox(int depth) {
		printBoxLine(depth,BOX_TOPLEFTCORNER,BOX_TOP,BOX_TOPRIGHTCORNER);
	}

	private void printCloseBox(int depth) {
		printBoxLine(depth,BOX_BOTTOMLEFTCORNER,BOX_BOTTOM,BOX_BOTTOMRIGHTCORNER);
	}

	private void printSplitBox(int depth) {
		printBoxLine(depth,BOX_SPLITLEFT,BOX_SPLIT,BOX_SPLITRIGHT);
	}

	private void printBoxLine(int depth, char lc, char mc, char rc) {
		tab(depth);
		int boxWidth = this.width - depth;
		out.print(lc);
		for(int i=1;i<(boxWidth-1);i++) {
			out.print(mc);
		}
		if(depth != 0) {
			out.print(BOX_SPLITRIGHT);
		} else {
			out.print(rc);
		}
		out.println();
	}
} public class CongruenceClosure extends AbstractClosureRule implements Proof.LinearRule {

	public CongruenceClosure(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "Eq-S";
	}

	@Override
	public State apply(Proof.Delta.Set existingTruths, Proof.State head, Formula newTruth) throws ResolutionError {
		//
		ArrayList<Formula> dependencies = new ArrayList<>();
		Formula constructed = (Formula) construct(existingTruths, head, newTruth, newTruth, dependencies);
		if(constructed != newTruth && !constructed.equals(newTruth)) {
			Formula[] deps = dependencies.toArray(new Formula[dependencies.size()]);
			// NOTE: we need to allocated the constructed item here so that we
			// can use it within the substituteAgainstEquality() function below
			// if it's an equality.
			constructed = head.allocate(constructed);
			head = head.subsume(this, newTruth, constructed, deps);
		}
		// If the construct truth is still an equality then we need to apply
		// that through all existing terms.
		if (constructed instanceof Formula.Equality && ((Formula.Equality) constructed).getSign()) {
			head = substituteAgainstEquality(existingTruths, head, (Formula.Equality) constructed);
		}
		//
		return head;
	}

	private Proof.State substituteAgainstEquality(Proof.Delta.Set existingTruths, Proof.State head, Formula.Equality newTruth) throws ResolutionError {
		//
		if (newTruth.getSign()) {
			head = applyEqualityTypeAxiom(head, newTruth);
			//
			Assignment assignment = rearrangeToAssignment(newTruth);
			if (assignment != null) {
				return applyAssignment(assignment,existingTruths,head);
			}
		}
		return head;
	}

	private State applyEqualityTypeAxiom(Proof.State state, Formula.Equality newTruth) throws ResolutionError {
		Expr lhs = newTruth.get(0);
		Expr rhs = newTruth.get(1);
		Type lhsT = types.inferType(state.getTypeEnvironment(),lhs);
		Type rhsT = types.inferType(state.getTypeEnvironment(),rhs);
		if(lhsT == null || rhsT == null) {
			// Defer processing of this equality
			return state;
		} else {
			Type intersection = new Type.Intersection(new Type[]{lhsT,rhsT});
			//
			boolean left = types.isRawSubtype(lhsT, rhsT);
			boolean right = types.isRawSubtype(rhsT, lhsT);
			Formula axiom;
			if (left && right) {
				// In this case, the types are equivalent so we don't need to do
				// anything.
				return state;
			} else if (left) {
				// In this case, the type of rhs is contained within that of lhs.
				// Therefore, that type must be the type for lhs.
				axiom = new Formula.Is(lhs, rhsT);
			} else if (right) {
				// In this case, the type of lhs is contained within that of rhs.
				// Therefore, that type must be the type for rhs.
				axiom = new Formula.Is(rhs, lhsT);
			} else if (types.isRawSubtype(new Type.Void(), intersection)) {
				// In this case, no possible intersection exists between the lhs and
				// rhs. Therefore, we're done as this equality cannot ever be true.
				return state.subsume(this, newTruth, new Formula.Truth(false));
			} else {
				// In this case, neither type is contained within the other.
				// Therefore, their intersection must be the type for both.
				axiom = new Formula.Conjunct(new Formula.Is(lhs, intersection), new Formula.Is(rhs, intersection));
			}
			// FIXME: I think it makes sense here to try and propagate the type
			// information upwards. Otherwise, we can get stuck with a non-variable
			// on the left-hand side.
			return state.infer(this,simp.simplify(axiom),newTruth);
		}
	}

	private State applyAssignment(Assignment assignment, Proof.Delta.Set existingTruths, Proof.State head) throws ResolutionError {
		Formula newTruth = assignment.getDependency();
		//
		for (int i = 0; i != existingTruths.size(); ++i) {
			Formula existingTruth = existingTruths.get(i);
			//
			Formula updatedTruth = (Formula) substitute(assignment.getLeftHandSide(), assignment.getRightHandSide(),
					existingTruth);
			//
			if (existingTruth != updatedTruth) {
				// The following is needed because substitution can
				// produce a different looking term which, after
				// simplification, is the same. To avoid this, we
				// need to avoid "recursive substitutions" somehow.
				if (!existingTruth.equals(updatedTruth)) {
					head = head.subsume(this, existingTruth, updatedTruth, newTruth);
				}
			}
		}
		//
		return head;
	}

	/**
	 * Rearrange an equality into two parts. The left-hand side (lhs)
	 * substituted through existing truths and replaced by the right-hand side
	 * (rhs). For example, in the equality <code>x+1 == y</code>, we may
	 * determine the lhs as <code>x</code> and the rhs as <code>y - 1</code>. A
	 * lexicographic ordering of terms is used to select the candidate for
	 * substitution, versus the rest.
	 *
	 * @param equality
	 *            --- The equality being rearranged
	 * @return
	 */
	public static Assignment rearrangeToAssignment(Formula.Equality equality) {
		if (equality instanceof Formula.ArithmeticEquality) {
			// Arithmetic equalities are a special case because we can actually
			// rearrange them.
			Formula.ArithmeticEquality e = (Formula.ArithmeticEquality) equality;
			Arithmetic.Polynomial lhs = Arithmetic.asPolynomial(e.get(0));
			Arithmetic.Polynomial rhs = Arithmetic.asPolynomial(e.get(1));
			Arithmetic.Polynomial diff = lhs.subtract(rhs);
			Polynomial.Term candidate = selectCandidateForSubstitution(diff);
			if(candidate == null) {
				return null;
			}
			Arithmetic.Polynomial bound = diff.subtract(candidate);
			if(candidate.getCoefficient().compareTo(BigInteger.ZERO) < 0) {
				candidate = candidate.negate();
			} else {
				bound = bound.negate();
			}
			if(candidate.getAtoms().length > 1) {
				syntaxError("Need support for non-linear arithmetic", equality);
			} else if(candidate.getCoefficient().compareTo(BigInteger.ONE) != 0) {
				syntaxError("Need support for reasoning about rationals", equality);
			}
			return new Assignment(candidate.toExpression(),bound.toExpression(),equality);
		} else {
			// For non-arithmetic equalities, we can't rearrange them.
			// Therefore, there are relatively few options.
			Expr lhs = equality.get(0);
			Expr rhs = equality.get(1);
			//
			Expr candidate = min(lhs,rhs);
			Expr bound;
			if(candidate == null || hasRecursiveReference(lhs,rhs)) {
				return null;
			} else {
				bound = max(lhs,rhs);
			}
			return new Assignment(candidate,bound,equality);
		}
	}

	/**
	 * Examine all terms in a polynomial to see whether any is a candidate for
	 * substitution or not. If one or more are found, then the least candidate
	 * is returned.
	 *
	 * @param p
	 * @return
	 */
	public static Polynomial.Term selectCandidateForSubstitution(Polynomial p) {
		Polynomial.Term candidate = null;
		for (int i = 0; i != p.size(); ++i) {
			Polynomial.Term term = p.getTerm(i);
			if (term.getAtoms().length > 0 && !hasRecursiveReference(term, p)) {
				candidate = selectCandidate(candidate,term);
			}
		}
		return candidate;
	}

	/**
	 * Given two candidate terms, select the best option.
	 *
	 * @param lhs
	 * @param rhs
	 * @return
	 */
	private static Polynomial.Term selectCandidate(Polynomial.Term lhs, Polynomial.Term rhs) {
		if (lhs == null) {
			return rhs;
		} else if (rhs == null) {
			return lhs;
		} else if (lessThan(lhs, rhs)) {
			return lhs;
		} else {
			return rhs;
		}
	}

	private static boolean lessThan(Polynomial.Term lhs, Polynomial.Term rhs) {
		Expr[] lhs_atoms = lhs.getAtoms();
		Expr[] rhs_atoms = rhs.getAtoms();
		// FIXME: this is *clearly* a hack
		long lhs_coeff = Math.abs(lhs.getCoefficient().longValue());
		long rhs_coeff = Math.abs(rhs.getCoefficient().longValue());
		//
		int lengthDifference = lhs_atoms.length - rhs_atoms.length;
		if (lengthDifference < 0) {
			return true;
		} else if (lengthDifference > 0) {
			return false;
		} else if(lhs_coeff == 1 && rhs_coeff != 1) {
			return true;
		} else if(lhs_coeff != 1 && rhs_coeff == 1) {
			return false;
		} else if(lhs_coeff != rhs_coeff) {
			return lhs_coeff < rhs_coeff;
		} else {
			for (int i = 0; i != lhs_atoms.length; ++i) {
				if (lessThan(lhs_atoms[i], rhs_atoms[i])) {
					return true;
				}
			}
			return false;
		}
	}

//	private static boolean lessThan(Expr lhs, Expr rhs) {
//		return lhs.getIndex() < rhs.getIndex();
//	}

	private static boolean lessThan(Expr lhs, Expr rhs) {
		return lhs.compareTo(rhs) < 0;
	}

	public static Expr min(Expr lhs, Expr rhs) {
		// First, prefer variables as these are always more useful.
		if(isVariable(lhs) && isVariable(rhs)) {
			if(lessThan(lhs,rhs)) {
				return lhs;
			} else {
				return rhs;
			}
		} else if(isVariable(lhs)) {
			return lhs;
		} else if(isVariable(rhs)) {
			return rhs;
		}
		// Second, take whatever has lowest index
		if(lessThan(lhs,rhs)) {
			return lhs;
		} else {
			return rhs;
		}
	}

	public static Expr max(Expr lhs, Expr rhs) {
		Expr r = min(lhs,rhs);
		//
		if(r == lhs) {
			return rhs;
		} else if(r == rhs) {
			return lhs;
		} else {
			return null;
		}
	}

	private static boolean isVariable(Expr e) {
		switch(e.getOpcode()) {
		case EXPR_varcopy:
		case EXPR_arridx:
		case EXPR_recfield:
		case EXPR_invoke:
		case EXPR_arrlen:
			return true;
		default:
			return false;
		}
	}

	/**
	 * Check whether a given polynomial contains a recursive reference to a
	 * given term. A recursive reference is simply an occurrence of the term as
	 * some component of a constructor contained within. For example, in
	 * <code>x</code> has a recursive reference in <code>x + y + f(x)</code>,
	 * whereas <code>y</code> does not.
	 *
	 * @param term
	 *            --- The term which we are checking to see whether it has a
	 *            recursive reference or not.
	 * @param poly
	 *            --- The polynomial within which we are looking for the
	 *            recursive reference.
	 * @return
	 */
	private static boolean hasRecursiveReference(Polynomial.Term term, Polynomial poly) {
		Expr[] atoms = term.getAtoms();
		//
		for (int i = 0; i != poly.size(); ++i) {
			Polynomial.Term t = poly.getTerm(i);
			// The polynomial is expected to contain the given term we're
			// looking for and, obviously, we don't want to use that when
			// looking for a recursive reference (since that would always be
			// true).
			if (t != term) {
				Expr[] t_atoms = t.getAtoms();
				for (int j = 0; j != atoms.length; ++j) {
					Expr atom = atoms[j];
					for (int k = 0; k != t_atoms.length; ++k) {
						if (isParentOf(t_atoms[k], atom)) {
							return true;
						}
					}
				}
			}
		}
		//
		return false;
	}

	/**
	 * Check whether the rhs contains a recursive reference to the lhs.
	 * @param lhs
	 * @param rhs
	 * @return
	 */
	private static boolean hasRecursiveReference(Expr lhs, Expr rhs) {
		return isParentOf(rhs,lhs);
	}

	/**
	 * Check whether a given expression is a parent of a given child. Or, put
	 * another way, whether the given parent contains the given child.
	 *
	 * @param parent
	 * @param child
	 * @return
	 */
	private static boolean isParentOf(SyntacticItem parent, Expr child) {
		if (parent.equals(child)) {
			return true;
		} else {
			for (int i = 0; i != parent.size(); ++i) {
				SyntacticItem pChild = parent.get(i);
				if (pChild != null && isParentOf(pChild, child)) {
					return true;
				}
			}
			return false;
		}
	}

	public static class Assignment {
		private final Expr lhs;
		private final Expr rhs;
		private final Formula dependency;

		public Assignment(Expr lhs, Expr rhs, Formula dep) {
			this.lhs = lhs;
			this.rhs = rhs;
			this.dependency = dep;
		}

		public Expr getLeftHandSide() {
			return lhs;
		}

		public Expr getRightHandSide() {
			return rhs;
		}

		public Formula getDependency() {
			return dependency;
		}
	}


	/**
	 * When generating an entirely new term within a given rule (i.e. one
	 * that has not been previously seen in the proof), we need to check
	 * whether it is the subject of some existing assignment or not.
	 *
	 * @param newTerm
	 * @return
	 */
	public SyntacticItem construct(Proof.Delta.Set existingTruths, Proof.State head, SyntacticItem term, Formula newTruth, List<Formula> dependencies) {
		SyntacticItem[] children = term.getAll();
		SyntacticItem[] nChildren = children;
		if(children != null) {
			for (int i = 0; i != children.length; ++i) {
				SyntacticItem child = children[i];
				SyntacticItem nChild;
				if (child instanceof Expr) {
					nChild = construct(existingTruths, head, child, newTruth, dependencies);
				} else if (child instanceof Tuple) {
					nChild = construct(existingTruths, head, child, newTruth, dependencies);
				} else {
					nChild = child;
				}
				if (child != nChild && nChildren == children) {
					// Clone the new children array to avoid interfering
					// with original item.
					nChildren = Arrays.copyOf(children, children.length);
				}
				nChildren[i] = nChild;
			}
		}
		if (nChildren != children) {
			// At least one child was changed, therefore clone the original
			// item with the new children.
			term = term.clone(nChildren);
		}
		if(term instanceof Expr) {
			return localConstruct(existingTruths, head,(Expr) term, newTruth, dependencies);
		} else {
			return term;
		}
	}

	public Expr localConstruct(Proof.Delta.Set existingTruths, Proof.State head, Expr term, Formula newTruth, List<Formula> dependencies) {
		Assignment assignment = lookupAssignment(existingTruths, head, term, newTruth);
		if (assignment != null) {
			dependencies.add(assignment.dependency);
			return assignment.getRightHandSide();
		} else {
			return term;
		}
	}

	private Assignment lookupAssignment(Proof.Delta.Set existingTruths, Proof.State head, Expr term, Formula newTruth) {
		//
		for (int i = existingTruths.size() - 1; i >= 0; --i) {
			Formula existingTruth = existingTruths.get(i);
			//
			if (existingTruth instanceof Formula.Equality) {
				Formula.Equality eq = (Formula.Equality) existingTruth;
				if (eq.getSign()) {
					CongruenceClosure.Assignment assign = rearrangeToAssignment(eq);
					// FIXME: this is essentially pretty broken. Need to find a
					// much better way to handle congruence closure.
					if (assign != null && assign.getLeftHandSide().equals(term)) {
						return assign;
					}
				}
			}
		}
		return null;
	}
} public class EqualityCaseAnalysis extends AbstractProofRule implements Proof.LinearRule {

	public EqualityCaseAnalysis(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "Neq-C";
	}

	@Override
	public State apply(State state, Formula truth) throws ResolutionError {
		if (truth instanceof Formula.ArithmeticEquality) {
			Formula.ArithmeticEquality eq = (Formula.ArithmeticEquality) truth;
			if (!eq.getSign()) {
				Expr lhs = eq.get(0);
				Expr rhs = eq.get(1);
				// For an arithmetic equality of the form x != y, we return a
				// disjunction of the form (x < y) || (x > y). This is not
				// necessarily the most efficient thing to do. However, for our
				// purposes, this works well enough for now.
				Inequality lt = Formulae.lessThan(lhs, rhs);
				Inequality gt = Formulae.lessThan(rhs, lhs);
				Formula disjunct = new Formula.Disjunct(lt, gt);
				return state.subsume(this, truth, disjunct);
			}
		} else if (truth instanceof Formula.Equality) {
			Formula.Equality eq = (Formula.Equality) truth;
			Expr lhs = eq.get(0);
			Expr rhs = eq.get(1);
			Type lhsT = types.inferType(state.getTypeEnvironment(), lhs);
			Type rhsT = types.inferType(state.getTypeEnvironment(), rhs);
			if (lhsT != null && rhsT != null) {
				Type intersection = new Type.Intersection(new Type[]{lhsT, rhsT});
				//
				if (types.isRawSubtype(new Type.Void(), intersection)) {
					// In this case, no possible intersection exists between the
					// lhs and rhs. Therefore, we're done as this equality
					// cannot ever be true.
					return state.subsume(this, truth, new Formula.Truth(true));
				} else if (types.isRawSubtype(new Type.Bool(), lhsT) && types.isRawSubtype(new Type.Bool(), rhsT)) {
					return expandBooleanEquality(eq, state);
				}
			} else {
				// NOTE: it is possible to get here in some situations. This can
				// happen as a result of type test which has not yet been
				// properly processed.
			}
		}

		return state;
	}

	private State expandBooleanEquality(Formula.Equality eq, Proof.State state) throws ResolutionError {
		Expr lhs = eq.get(0);
		Expr rhs = eq.get(1);
		//
		Formula lhs_f = Formulae.toFormula(lhs, types);
		Formula rhs_f = Formulae.toFormula(rhs, types);
		//
		// FIXME: I have a feeling we can do better here. Especially, in the
		// case of an equality I don't think we want to do anything. In the case
		// of an inequality (e.g. x==y), I think we want to generate an equality
		// (x == !y) or similar.
		//
		if(eq.getSign()) {
			Formula l = new Conjunct(lhs_f, rhs_f);
			Formula r = new Conjunct(Formulae.invert(lhs_f), Formulae.invert(rhs_f));
			Formula disjunct = new Formula.Disjunct(l, r);
			return state.subsume(this, eq, disjunct);
		} else {
			Formula l = new Conjunct(Formulae.invert(lhs_f),rhs_f);
			Formula r = new Conjunct(lhs_f,Formulae.invert(rhs_f));
			Formula disjunct = new Formula.Disjunct(l, r);
			// NOTE: at the moment, we can't do a subsume here because we can
			// end up losing critical information.
			return state.infer(this, simp.simplify(disjunct), eq);
		}
	}
} public class Simplification extends AbstractProofRule implements Proof.LinearRule {

	private final static Formula TRUE = new Formula.Truth(true);
	private final static Formula FALSE = new Formula.Truth(false);

	public Simplification(TypeSystem types) {
		super(null,types);
	}

	@Override
	public String getName() {
		return "Simp";
	}


	@Override
	public State apply(State head, Formula truth) throws ResolutionError {
		Formula simplifiedTruth = simplify(truth);
		if(!simplifiedTruth.equals(truth)) {
			// FIXME: useful optimisation would be to support pointer equality
			// for the above test.
			head = head.subsume(this, truth, simplifiedTruth);
		}
		return head;
	}

	/**
	 * Recursively simplify a given formula by applying the "standard"
	 * simplifications for each kind. If no simplification is performed, this
	 * returns the original object in tact.
	 *
	 * @param f
	 * @return
	 * @throws AmbiguousNameError
	 * @throws NameNotFoundError
	 */
	public Formula simplify(Formula f) throws ResolutionError {
		switch (f.getOpcode()) {
		case EXPR_const:
			return f;
		case EXPR_and:
			return simplifyConjunct((Formula.Conjunct) f);
		case EXPR_or:
			return simplifyDisjunct((Formula.Disjunct) f);
		case EXPR_exists:
		case EXPR_forall: {
			return simplifyQuantifier((Formula.Quantifier) f);
		}
		case EXPR_eq:
		case EXPR_neq: {
			if (f instanceof ArithmeticEquality) {
				return simplifyArithmeticEquality((Formula.ArithmeticEquality) f);
			} else {
				return simplifyEquality((Formula.Equality) f);
			}
		}
		case EXPR_lt:
		case EXPR_gteq: {
			return simplifyInequality((Formula.Inequality) f);
		}
		case EXPR_invoke: {
			return simplifyInvoke((Formula.Invoke) f);
		}
		case EXPR_is: {
			return simplifyIs((Formula.Is) f);
		}
		default:
			throw new IllegalArgumentException("invalid formula opcode: " + f.getOpcode());
		}
	}

	public Formula simplifyConjunct(Conjunct conjunct) throws ResolutionError {
		Formula[] children = conjunct.getAll();
		Formula[] nChildren = simplify(children);
		// Check whether contains false
		if (ArrayUtils.firstIndexOf(nChildren, FALSE) >= 0) {
			// Any conjunct containing false equals false
			return new Formula.Truth(false);
		}
		// Expand any nested conjuncts
		nChildren = inlineNestedConjuncts(nChildren);
		// Remove any duplicate types
		nChildren = ArrayUtils.removeDuplicates(nChildren);
		// Remove all occurrences of true
		nChildren = ArrayUtils.removeAll(nChildren, TRUE);
		//
		if(nChildren.length == 0) {
			return new Formula.Truth(true);
		} else if(nChildren.length == 1) {
			return nChildren[0];
		} else if(children == nChildren) {
			return conjunct;
		} else {
			return new Formula.Conjunct(nChildren);
		}
	}

	public Formula simplifyDisjunct(Disjunct disjunct) throws ResolutionError {
		Formula[] children = disjunct.getAll();
		Formula[] nChildren = simplify(children);
		// Check whether contains true
		if (ArrayUtils.firstIndexOf(nChildren, TRUE) >= 0) {
			// Any disjunct containing true equals true
			return new Formula.Truth(true);
		}
		// Expand any nested disjuncts
		nChildren = inlineNestedDisjuncts(nChildren);
		// Remove any duplicate types
		nChildren = ArrayUtils.removeDuplicates(nChildren);
		// Remove all occurrences of false
		nChildren = ArrayUtils.removeAll(nChildren, FALSE);
		//
		if(nChildren.length == 0) {
			return new Formula.Truth(false);
		} else if(nChildren.length == 1) {
			return nChildren[0];
		} else if(children == nChildren) {
			return disjunct;
		} else {
			return new Formula.Disjunct(nChildren);
		}
	}

	public Formula[] simplify(Formula[] children) throws ResolutionError {
		Formula[] nChildren = children;
		for (int i = 0; i != nChildren.length; ++i) {
			Formula child = children[i];
			Formula nChild = simplify(child);
			if (child != nChild && children == nChildren) {
				nChildren = Arrays.copyOf(children, children.length);
			}
			nChildren[i] = nChild;
		}
		return nChildren;
	}

	/**
	 * Simplify a quantified formula. In essence, if the body is a truth value
	 * then that is returned. For example, <code>forall x.true</code> is simply
	 * <code>true</code>.
	 *
	 * @param quantifier
	 * @return
	 * @throws AmbiguousNameError
	 * @throws NameNotFoundError
	 */
	public Formula simplifyQuantifier(Quantifier quantifier) throws ResolutionError {
		Formula body = quantifier.getBody();
		Formula nBody = simplify(body);
		if (nBody instanceof Truth) {
			return nBody;
		} else if (nBody != body) {
			return new Quantifier(quantifier.getSign(), quantifier.getParameters(), nBody);
		} else {
			return quantifier;
		}
	}

	/**
	 * Simplify an inequality by canceling, evaluating and/or balancing:
	 * <ol>
	 * <li><b>Canceling</b> is the process of removing commons terms from both
	 * sides. For example, in <code>x+y < x</code> we can cancel <code>x</code>
	 * to give <code>y < 0</code>.</li>
	 * <li><b>Evaluating</b> is the process of reducing a constant inequality to
	 * either <code>true</code> or <code>false</code>. For example,
	 * <code>0 < 1</code> reduces to <code>true</code> whilst
	 * <code>1 >= 0</code> reduces to <code>false</code>.</li>
	 * <li><b>Balancing</b> is the process of eliminating negative terms and
	 * factorising. For example, <code>-x < 1</code> is balanced to
	 * <code>0 < 1 + x</code>. Likewise, <code>2*x < 6*y</code> is factorised to
	 * <code>x < 3*y</code>.</li>
	 * </ol>
	 *
	 * @param ieq
	 * @return
	 * @throws AmbiguousNameError
	 * @throws NameNotFoundError
	 */
	public Formula simplifyInequality(Inequality ieq) throws ResolutionError {
		Expr lhs = ieq.get(0);
		Expr rhs = ieq.get(1);
		Expr nLhs = simplifyExpression(lhs);
		Expr nRhs = simplifyExpression(rhs);
		Pair<Expr, Expr> bs = normaliseBounds(nLhs, nRhs);
		nLhs = bs.getFirst();
		nRhs = bs.getSecond();
		//
		if (nLhs instanceof Expr.Constant && nRhs instanceof Expr.Constant) {
			Value.Int lhs_v = (Value.Int) ((Expr.Constant) nLhs).getValue();
			Value.Int rhs_v = (Value.Int) ((Expr.Constant) nRhs).getValue();
			return evaluateInequality(ieq.getOpcode(), lhs_v, rhs_v);
		} else if (nLhs.equals(nRhs)) {
			return new Formula.Truth(true);
		} else if(lhs.equals(nLhs) && rhs.equals(nRhs)) {
			return ieq;
		} else {
			return new Inequality(bs.getFirst(), bs.getSecond());
		}
	}

	/**
	 * Simplify an arithmetic equality by canceling, evaluating and/or
	 * balancing:
	 * <ol>
	 * <li><b>Canceling</b> is the process of removing commons terms from both
	 * sides. For example, in <code>x+y == x</code> we can cancel <code>x</code>
	 * to give <code>y == 0</code>.</li>
	 * <li><b>Evaluating</b> is the process of reducing a constant inequality to
	 * either <code>true</code> or <code>false</code>. For example,
	 * <code>0 == 0</code> reduces to <code>true</code> whilst
	 * <code>1 == 0</code> reduces to <code>false</code>.</li>
	 * <li><b>Balancing</b> is the process of eliminating negative terms and
	 * factorising. For example, <code>-x == 1</code> is balanced to
	 * <code>0 == 1 + x</code>. Likewise, <code>2*x == 6*y</code> is factorised
	 * to <code>x == 3*y</code>.</li>
	 * </ol>
	 *
	 * @param ieq
	 * @return
	 * @throws AmbiguousNameError
	 * @throws NameNotFoundError
	 */
	public Formula simplifyArithmeticEquality(ArithmeticEquality eq) throws ResolutionError {
		Expr lhs = eq.get(0);
		Expr rhs = eq.get(1);
		Expr nLhs = simplifyExpression(lhs);
		Expr nRhs = simplifyExpression(rhs);
		Pair<Expr, Expr> bs = normaliseBounds(nLhs, nRhs);
		nLhs = bs.getFirst();
		nRhs = bs.getSecond();
		if (nLhs instanceof Expr.Constant && nRhs instanceof Expr.Constant) {
			Value lhs_v = ((Expr.Constant) nLhs).getValue();
			Value rhs_v = ((Expr.Constant) nRhs).getValue();
			return evaluateEquality(eq.getOpcode(), lhs_v, rhs_v);
		} else if (nLhs.equals(nRhs)) {
			return new Formula.Truth(eq.getSign());
		}
		Arithmetic.Polynomial difference = Arithmetic.asPolynomial(nLhs).subtract(Arithmetic.asPolynomial(nRhs));
		if(difference.isConstant()) {
			BigInteger constant = difference.toConstant();
			return new Formula.Truth(constant.equals(BigInteger.ZERO));
		}
		// Handle orientation
		if(nLhs.compareTo(nRhs) > 0) {
			Expr tmp = nLhs;
			nLhs = nRhs;
			nRhs = tmp;
		}
		if(nLhs.equals(lhs) && nRhs.equals(rhs)) {
			// FIXME: above could be more efficient
			return eq;
		} else {
			return new ArithmeticEquality(eq.getSign(), nLhs, nRhs);
		}
	}

	/**
	 * Simplify a non-arithmetic equality by attempting to evaluate it. For
	 * example, <code>true == false</code> reduces to <code>false</code>. In the
	 * case that neither side is a constant, then the original equality is
	 * returned.
	 *
	 * @param eq
	 * @return
	 * @throws AmbiguousNameError
	 * @throws NameNotFoundError
	 */
	public Formula simplifyEquality(Equality eq) throws ResolutionError {
		Expr lhs = eq.get(0);
		Expr rhs = eq.get(1);
		Expr nLhs = simplifyExpression(lhs);
		Expr nRhs = simplifyExpression(rhs);
		if (nLhs instanceof Expr.Constant && nRhs instanceof Expr.Constant) {
			Value lhs_v = ((Expr.Constant) nLhs).getValue();
			Value rhs_v = ((Expr.Constant) nRhs).getValue();
			return evaluateEquality(eq.getOpcode(), lhs_v, rhs_v);
		} else if (nLhs.equals(nRhs)) {
			return new Formula.Truth(eq.getSign());
		}
		// Handle orientation
		if(nLhs.compareTo(nRhs) > 0) {
			Expr tmp = nLhs;
			nLhs = nRhs;
			nRhs = tmp;
		}
		// Now decide whether need to create a new equality or not.
		if(nLhs == lhs && nRhs == rhs) {
			return eq;
		} else {
			return new Equality(eq.getSign(),nLhs,nRhs);
		}
	}

	public Formula simplifyInvoke(Invoke ivk) throws ResolutionError {
		Tuple<Expr> args = ivk.getArguments();
		Expr[] nChildren = new Expr[args.size()];
		boolean changed = false;
		for (int i = 0; i != args.size(); ++i) {
			Expr child = args.get(i);
			Expr nChild = simplifyExpression(child);
			//
			changed |= (child != nChild);
			nChildren[i] = nChild;
		}
		if(!changed) {
			return ivk;
		} else {
			Tuple<Expr> nArgs = new Tuple<>(nChildren);
			return new Invoke(ivk.getSign(),ivk.getSignatureType(),ivk.getName(),ivk.getSelector(),nArgs);
		}
	}

	public Formula simplifyIs(Formula.Is e) throws ResolutionError {
		Expr lhs = e.getTestExpr();
		Expr nLhs = simplifyExpression(lhs);
		if(lhs != nLhs) {
			return new Formula.Is(nLhs, e.getTestType());
		} else {
			return e;
		}
	}


	public Expr[] simplifyExpressions(Expr[] children) throws ResolutionError {
		Expr[] nChildren = children;
		for (int i = 0; i != children.length; ++i) {
			Expr child = children[i];
			Expr nChild = simplifyExpression(child);
			if (child != nChild && children == nChildren) {
				nChildren = Arrays.copyOf(children, children.length);
			}
			nChildren[i] = nChild;
		}
		return nChildren;
	}

	/**
	 * Convert an arbitrary expression to an atom.
	 *
	 * @param e
	 * @return
	 * @throws AmbiguousNameError
	 * @throws NameNotFoundError
	 */
	public Expr simplifyExpression(Expr e) throws ResolutionError {
		switch (e.getOpcode()) {
		case EXPR_varcopy:
			return e;
		case EXPR_const:
			return simplifyConstant((Expr.Constant) e);
		case EXPR_invoke:
			return simplifyInvoke((Expr.Invoke) e);
		case EXPR_arridx:
			return simplifyArrayIndex((Expr.Operator) e);
		case EXPR_arrupdt:
			return simplifyArrayUpdate((Expr.Operator) e);
		case EXPR_arrlen:
			return simplifyArrayLength((Expr.Operator)e);
		case EXPR_arrinit:
		case EXPR_arrgen:
		case EXPR_div: // temporary for now
		case EXPR_rem: // temporary for now
			return simplifyNonArithmetic((Expr.Operator) e);
		case EXPR_neg:
		case EXPR_add:
		case EXPR_mul:
		case EXPR_sub:
			return simplifyArithmetic((Expr.Operator) e);
		case EXPR_recinit:
			return simplifyRecordInitialiser((Expr.RecordInitialiser) e);
		case EXPR_recfield:
			return simplifyRecordAccess((Expr.RecordAccess) e);
		case EXPR_recupdt:
			return simplifyRecordUpdate((Expr.RecordUpdate) e);
		case EXPR_deref:
			return simplifyDereference((Expr.Dereference) e);
		case EXPR_not:
		case EXPR_and:
		case EXPR_or:
		case EXPR_exists:
		case EXPR_forall:
		case EXPR_eq:
		case EXPR_neq:
		case EXPR_lt:
		case EXPR_lteq:
		case EXPR_gt:
		case EXPR_gteq:
		case EXPR_is:
			if(e instanceof Formula) {
				return simplify((Formula) e);
			} else {
				// We need toFormula here because of the potential for arbitrarily
				// nested expressions to contain these constructs.
				return simplify(Formulae.toFormula(e,types));
			}
		default:
			throw new IllegalArgumentException("cannot convert expression to atom: " + e.getClass().getName());
		}
	}

	public Expr simplifyConstant(Expr.Constant e) {
		Value val = e.getValue();
		if (val instanceof Value.Bool) {
			Value.Bool b = (Value.Bool) val;
			return new Formula.Truth(b.get());
		} else {
			return e;
		}
	}

	public Expr simplifyRecordInitialiser(Expr.RecordInitialiser e) throws ResolutionError {
		Pair<Identifier,Expr>[] fields = e.getFields();
		Pair<Identifier,Expr>[] nFields = fields;
		for(int i=0;i!=fields.length;++i) {
			Expr ith = fields[i].getSecond();
			Expr nIth = simplifyExpression(ith);
			if(ith != nIth && fields == nFields) {
				nFields = Arrays.copyOf(fields, fields.length);
			}
			if(ith != nIth) {
				nFields[i] = new Pair<>(fields[i].getFirst(),nIth);
			}
		}
		if(fields == nFields) {
			return e;
		} else {
			return new Expr.RecordInitialiser(nFields);
		}
	}

	public Expr simplifyRecordAccess(Expr.RecordAccess e) throws ResolutionError {
		Expr source = e.getSource();
		Expr nSource = simplifyExpression(source);
		if(nSource instanceof Expr.RecordInitialiser) {
			Expr.RecordInitialiser ri = (Expr.RecordInitialiser) nSource;
			Pair<Identifier, Expr>[] fields = ri.getFields();
			for(int i=0;i!=fields.length;++i) {
				Pair<Identifier, Expr> field = fields[i];
				if(e.getField().equals(field.getFirst())) {
					return field.getSecond();
				}
			}
		} else if(nSource instanceof Expr.RecordUpdate) {
			Expr.RecordUpdate r = (Expr.RecordUpdate) nSource;
			if(e.getField().equals(r.getField())) {
				return r.getValue();
			} else {
				return new Expr.RecordAccess(r.getSource(), e.getField());
			}
		}
		//
		if(source == nSource) {
			return e;
		} else {
			return new Expr.RecordAccess(nSource, e.getField());
		}
	}

	public Expr simplifyRecordUpdate(Expr.RecordUpdate e) throws ResolutionError {
		Expr source = e.getSource();
		Expr value = e.getValue();
		Expr nSource = simplifyExpression(source);
		Expr nValue = simplifyExpression(value);
		//
		if(nSource instanceof Expr.RecordInitialiser) {
			Expr.RecordInitialiser ri = (Expr.RecordInitialiser) nSource;
			Pair<Identifier, Expr>[] oldFields = ri.getFields();
			Pair<Identifier, Expr>[] newFields = Arrays.copyOf(oldFields, oldFields.length);
			for(int i=0;i!=oldFields.length;++i) {
				Pair<Identifier, Expr> field = oldFields[i];
				if(e.getField().equals(field.getFirst())) {
					newFields[i] = new Pair<>(field.getFirst(),nValue);
				}
			}
			return new Expr.RecordInitialiser(newFields);
		}
		//
		if(source == nSource && value == nValue) {
			return e;
		} else {
			return new Expr.RecordUpdate(nSource, e.getField(), nValue);
		}
	}

	public Expr simplifyDereference(Expr.Dereference e) throws ResolutionError {
		Expr source = e.getOperand();
		Expr nSource = simplifyExpression(source);
		if (source == nSource) {
			return e;
		} else {
			return new Expr.Dereference(nSource);
		}
	}

	public Expr simplifyInvoke(Expr.Invoke ivk) throws ResolutionError {
		Tuple<Expr> args = ivk.getArguments();
		Expr[] nChildren = new Expr[args.size()];
		boolean changed = false;
		for (int i = 0; i != args.size(); ++i) {
			Expr child = args.get(i);
			Expr nChild = simplifyExpression(child);
			//
			changed |= (child != nChild);
			nChildren[i] = nChild;
		}
		if(!changed) {
			return ivk;
		} else {
			Tuple<Expr> nArgs = new Tuple<>(nChildren);
			return new Expr.Invoke(ivk.getSignatureType(),ivk.getName(),ivk.getSelector(),nArgs);
		}
	}

	public Expr simplifyArrayIndex(Expr.Operator e) throws ResolutionError {
		Expr source = e.get(0);
		Expr index = e.get(1);
		Expr nSource = simplifyExpression(source);
		Expr nIndex = simplifyExpression(index);
		//
		if (nSource instanceof Expr.Operator && nIndex instanceof Expr.Constant) {
			// We may have a constant index value into a constant array
			Expr.Operator arr = (Expr.Operator) nSource;
			if (arr.getOpcode() == EXPR_arrinit) {
				// We definitely have a constant index value into a constant
				// array
				BigInteger i = ((Value.Int) ((Expr.Constant) nIndex).getValue()).get();
				if (i.compareTo(BigInteger.ZERO) >= 0 && i.compareTo(BigInteger.valueOf(arr.size())) < 0) {
					// The constant index is within bounds
					return arr.get(i.intValue());
				}
			}
		}
		if(nSource.getOpcode() == EXPR_arrgen) {
			return (Expr) nSource.get(0);
		}
		// If we get here, then no simplification of the array access expression
		// was possible.
		if (source == nSource && index == nIndex) {
			return e;
		} else {
			return new Expr.ArrayAccess(nSource, nIndex);
		}
	}

	public Expr simplifyArrayUpdate(Expr.Operator e) throws ResolutionError {
		Expr source = e.get(0);
		Expr index = e.get(1);
		Expr value = e.get(2);
		Expr nSource = simplifyExpression(source);
		Expr nIndex = simplifyExpression(index);
		Expr nValue = simplifyExpression(value);
		//
		if(nIndex instanceof Expr.Constant && nSource.getOpcode() == EXPR_arrinit) {
			Expr.Operator src = (Expr.Operator) nSource;
			BigInteger b = ((Value.Int) ((Expr.Constant) nIndex).getValue()).get();
			if(b.compareTo(BigInteger.ZERO) >= 0 && b.compareTo(BigInteger.valueOf(nSource.size())) < 0) {
				int idx = b.intValue();
				Expr[] nChildren = Arrays.copyOf(src.getAll(),src.size());
				nChildren[idx] = nValue;
				return src.clone(nChildren);
			}
		}
		if (source == nSource && index == nIndex && value == nValue) {
			return e;
		} else {
			return new Expr.ArrayUpdate(nSource, nIndex, nValue);
		}
	}

	public Expr simplifyArrayLength(Expr.Operator e) throws ResolutionError {
		Expr r = simplifyNonArithmetic(e);
		if (r instanceof Expr.Operator) {
			Expr src = (Expr) r.get(0);
			if (src.getOpcode() == EXPR_arrinit) {
				return new Expr.Constant(new Value.Int(src.size()));
			} else if (src.getOpcode() == EXPR_arrgen) {
				return (Expr) src.get(1);
			} else if (src.getOpcode() == EXPR_arrupdt) {
				return simplifyArrayLength(new Expr.ArrayLength((Expr) src.get(0)));
			}
		}
		return r;
	}

	public Expr simplifyNonArithmetic(Expr.Operator e) throws ResolutionError {
		Expr[] children = e.getAll();
		Expr[] nChildren = simplifyExpressions(children);

		if (nChildren == children) {
			return e;
		} else {
			// FIXME: there are further simplifications that can be performed
			// here. For example, taking the field of a constant record;
			// likewise, taking a constant index into a constant array. Although
			// unlikely, they can arise through the use of e.g. configuration
			// constants, etc.
			return e.clone(nChildren);
		}
	}

	public Expr simplifyArithmetic(Expr.Operator e) throws ResolutionError {
		Expr[] children = e.getAll();
		Polynomial result = Arithmetic.asPolynomial(simplifyExpression(children[0]));
		switch (e.getOpcode()) {
		case EXPR_add: {
			for (int i = 1; i != children.length; ++i) {
				result = result.add(Arithmetic.asPolynomial(simplifyExpression(children[i])));
			}
			break;
		}
		case EXPR_sub: {
			for (int i = 1; i != children.length; ++i) {
				result = result.subtract(Arithmetic.asPolynomial(simplifyExpression(children[i])));
			}
			break;
		}
		case EXPR_mul: {
			for (int i = 1; i != children.length; ++i) {
				result = result.multiply(Arithmetic.asPolynomial(simplifyExpression(children[i])));
			}
			break;
		}
		case EXPR_neg: {
			result = result.negate();
			break;
		}
		default:
			throw new IllegalArgumentException("Unknown arithmetic opcode encountered");
		}
		return result.toExpression();
	}

	// ========================================================================
	// Equalities / Inequalities
	// ========================================================================

	/**
	 * Evaluate a given inequality whose bounds are known to be constant integer
	 * values. For example, <code>1 < 0</code> evaluates to <code>false</code>,
	 * etc.
	 *
	 * @param opcode
	 * @param lhs
	 * @param rhs
	 * @return
	 */
	public Formula.Truth evaluateInequality(int opcode, Value.Int lhs, Value.Int rhs) {
		boolean result;
		switch (opcode) {
		case EXPR_lt:
			result = lhs.compareTo(rhs) < 0;
			break;
		case EXPR_lteq:
			result = lhs.compareTo(rhs) <= 0;
			break;
		case EXPR_gt:
			result = lhs.compareTo(rhs) > 0;
			break;
		case EXPR_gteq:
			result = lhs.compareTo(rhs) >= 0;
			break;
		default:
			throw new IllegalArgumentException("Invalid inequality opcode: " + opcode);
		}
		return new Formula.Truth(result);
	}

	/**
	 * Evaluate a given equality whose bounds are known to be constant values of
	 * some sort. For example, <code>true == false</code> evaluates to
	 * <code>false</code>, etc.
	 *
	 * @param opcode
	 * @param lhs
	 * @param rhs
	 * @return
	 */
	public Formula.Truth evaluateEquality(int opcode, Value lhs, Value rhs) {
		boolean result;
		switch (opcode) {
		case EXPR_eq:
			result = lhs.equals(rhs);
			break;
		case EXPR_neq:
			result = !(lhs.equals(rhs));
			break;
		default:
			throw new IllegalArgumentException("Invalid equality opcode: " + opcode);
		}
		return new Formula.Truth(result);
	}

	/**
	 * Normalise bounds of an equation to be positive. For example, consider the
	 * inequality <code>x < y - z</code>. In this case, the right-hand side is
	 * not simplifyd because it contains a negative term. The simplifyd
	 * version of this inequality would be <code>x + z < y</code>.
	 *
	 * @param lhs
	 * @param rhs
	 * @return
	 */
	public Pair<Expr, Expr> normaliseBounds(Expr lhs, Expr rhs) {
		Polynomial left = Arithmetic.asPolynomial(lhs);
		Polynomial right = Arithmetic.asPolynomial(rhs);
		Polynomial bound = left.subtract(right).factorise();
		//
		Polynomial pos = filter(bound, true);
		Polynomial neg = filter(bound, false);
		return new Pair<>(pos.toExpression(), neg.toExpression());
	}

	public Polynomial filter(Polynomial p, boolean sign) {
		Polynomial result = Polynomial.ZERO;
		for (int i = 0; i != p.size(); ++i) {
			Polynomial.Term term = p.getTerm(i);
			BigInteger coefficient = term.getCoefficient();
			int c = coefficient.compareTo(BigInteger.ZERO);
			if (sign && c >= 0) {
				result = result.add(term);
			} else if (!sign && c < 0) {
				result = result.subtract(term);
			}
		}
		return result;
	}


	private Formula[] inlineNestedDisjuncts(Formula[] children) {
		Formula[] nChildren = children;
		for(int i=0;i!=nChildren.length;++i) {
			Formula child = nChildren[i];
			if(child instanceof Formula.Disjunct) {
				// We found a nested disjunct!
				Formula.Disjunct disjunct = (Formula.Disjunct) child;
				Formula[] nested = disjunct.getAll();
				// Inline the nested disjunct's operands
				nChildren = inlineNestedArray(nChildren,i,nested);
				// Can safely skip all elements in nested since disjunct already
				// in simplified form by construction.
				i += (nested.length - 1);
			}
		}
		return nChildren;
	}

	private Formula[] inlineNestedConjuncts(Formula[] children) {
		Formula[] nChildren = children;
		for (int i = 0; i != nChildren.length; ++i) {
			Formula child = nChildren[i];
			if (child instanceof Formula.Conjunct) {
				// We found a nested conjunct!
				Formula.Conjunct conjunct = (Formula.Conjunct) child;
				Formula[] nested = conjunct.getAll();
				// Inline the nested conjunct's operands
				nChildren = inlineNestedArray(nChildren, i, nested);
				// Can safely skip all elements in nested since conjunct already
				// in simplified form by construction.
				i += (nested.length - 1);
			}
		}
		return nChildren;
	}

	public <T> Formula[] inlineNestedArray(Formula[] parent, int index, Formula[] child) {
		Formula[] types = new Formula[parent.length + child.length - 1];
		System.arraycopy(parent, 0, types, 0, index);
		System.arraycopy(child, 0, types, index, child.length);
		System.arraycopy(parent, index + 1, types, index + child.length, parent.length - (index + 1));
		return types;
	}
} public class InequalityIntroduction extends AbstractClosureRule implements Proof.LinearRule {
	public InequalityIntroduction(Simplification simp,TypeSystem types) {
		super(simp,types);
	}

	@Override
	public String getName() {
		return "Ieq-I";
	}

	@Override
	public State apply(Proof.Delta.Set existingTruths, Proof.State state, Formula newTruth) throws ResolutionError {
		if(newTruth instanceof Formula.Inequality) {
			Formula.Inequality inequality = (Formula.Inequality) newTruth;
			// At this point, we have an inequality which potentially could be
			// closed with one or more other inequalities. Therefore, we need to
			// look back through the history to determine any inequalities which
			// are currently "active".
			for(int i=0;i!=existingTruths.size();++i) {
				Formula existingTruth = existingTruths.get(i);
				if(existingTruth instanceof Formula.Inequality) {
					state = closeOver(inequality,(Formula.Inequality)existingTruth,state);
				}
			}
		}
		// No change in the normal case
		return state;
	}

	private State closeOver(Formula.Inequality ith, Formula.Inequality jth, State state) throws ResolutionError {
		//
		Formula inferred = closeOver(ith, jth);
		if (inferred != null) {
			inferred = simp.simplify(inferred);
			state = state.infer(this, inferred, ith, jth);
		}
		inferred = closeOver(jth, ith);
		if (inferred != null) {
			inferred = simp.simplify(inferred);
			state = state.infer(this, inferred, ith, jth);
		}
		return state;
	}


	/**
	 * <p>
	 * Close over two inequalities. This may or may not produce a new inequality
	 * as a result. For example, closing over <code>3 < x</code> and
	 * <code>x < y</code> gives <code>3 < y</code>. Observe that, for this
	 * operation to succeed, there must exist a term common to both
	 * inequalities. In the case that multiple candidate terms exist, then the
	 * lexiographically least is selected.
	 * </p>
	 * <p>
	 * This operation always closes in the same direction. If ith is "p1 >= p2"
	 * and jth is "p3 >= p4" then it attempts to generate the inequality of the
	 * form "p1 >= p4", but never of the form "p4 >= p1". In otherwords, the ith
	 * inequality always provides the lower bound and the jth inequality always
	 * provides the upper bound.
	 * </p>
	 *
	 * <b>NOTE:</b> this currently assumes that the inequalities are balanced.
	 *
	 * @param ith
	 * @param jth
	 * @return
	 */
	public Formula closeOver(Formula.Inequality ith, Formula.Inequality jth) throws ResolutionError {
		Polynomial ithLowerBound = extractBound(false, ith);
		Polynomial ithUpperBound = extractBound(true, ith);
		Polynomial jthLowerBound = extractBound(false, jth);
		Polynomial jthUpperBound = extractBound(true, jth);
		// A language with destructuring would be nice here
		Pair<Polynomial.Term, Polynomial.Term> candidates = selectCandidateTerm(ithLowerBound, jthUpperBound);
		//
		if (candidates == null) {
			// No matching candidates were found for this orientation.
			return null;
		} else {
			Polynomial.Term ithCandidate = candidates.first();
			Polynomial.Term jthCandidate = candidates.second();
			Polynomial ithUpper = rearrangeForUpperBound(ithLowerBound, ithUpperBound, ithCandidate);
			Polynomial jthLower = rearrangeForLowerBound(jthLowerBound, jthUpperBound, jthCandidate);
			ithUpper = ithUpper.multiply(jthCandidate.getCoefficient());
			jthLower = jthLower.multiply(ithCandidate.getCoefficient());
			// 2 < 2x, 3x < 3
			//
			if (ithUpper.equals(jthLower)) {
				Polynomial.Term candidate = ithCandidate.multiply(jthCandidate.getCoefficient());
				return new Formula.ArithmeticEquality(true, candidate.toExpression(), ithUpper.toExpression());
			} else {
				return Formulae.greaterOrEqual(ithUpper.toExpression(),jthLower.toExpression());
			}
		}
	}

	/**
	 * Extract a given bound from the inequality. Here, true is upper and false
	 * is lower.
	 *
	 * @param sign
	 * @param inequality
	 * @return
	 */
	private static Polynomial extractBound(boolean sign, Formula.Inequality inequality) {
		int i = sign ? 0 : 1;
		return Arithmetic.asPolynomial(inequality.get(i));
	}

	/**
	 * <p>
	 * Determine a suitable term (if one exists) for rearranging the two
	 * inequalities. A candidate term must be common to both and involve at
	 * least one variable, and should appear on opposite sides of the
	 * inequalities. The selected candidate then has the lowest ordering of any
	 * possible term. For example, consider these two options:
	 * </p>
	 *
	 * <pre>
	 * x < y + z
	 * x + y > z
	 * </pre>
	 *
	 * <p>
	 * For these two equations, the candidate terms are <code>x</code> and
	 * <code>z</code>. Since <code>y</code> is an upper bound on both, it is not
	 * considered. Then, <code>x</code> is selected as the actual term for
	 * rearranging since it is lexiographically lower than <code>z</code>.
	 * </p>
	 *
	 * @param ith
	 * @param jth
	 * @return
	 */
	private static Pair<Polynomial.Term, Polynomial.Term> selectCandidateTerm(Polynomial lower, Polynomial upper) {
		for (int i = 0; i != lower.size(); ++i) {
			Polynomial.Term ith = lower.getTerm(i);
			Expr[] ithAtoms = ith.getAtoms();
			if (ithAtoms.length > 0) {
				for (int j = 0; j != upper.size(); ++j) {
					Polynomial.Term jth = upper.getTerm(j);
					Expr[] jthAtoms = jth.getAtoms();
					if (Arrays.equals(ithAtoms, jthAtoms)) {
						return new Pair<>(ith,jth);
					}
				}
			}
		}
		//
		return null;
	}

	/**
	 * Rearrange a given equation such that the given term appears on the
	 * right-hand side, and everything else is moved on to the left side. For
	 * example, consider rearranging these for <code>x</code>:
	 *
	 * <pre>
	 * 1 < x + y
	 * </pre>
	 *
	 * The resulting polynomial represents the "left-hand side" which (in this
	 * case) is 1-y. Thus, the rearranged inequality would be 1 - y < x.
	 *
	 * @param lhs
	 *            The "left-hand side" of the equation.
	 * @param rhs
	 *            The "right-hand side" of the equation.
	 * @param term
	 *            the given term being rearranged for.
	 */
	private static Polynomial rearrangeForLowerBound(Polynomial lhs, Polynomial rhs, Polynomial.Term term) {
		rhs = rhs.subtract(term);
		return lhs.add(rhs.negate());
	}

	/**
	 * Rearrange a given equation such that the given term appears on the
	 * left-hand side, and everything else is moved on to the right side. For
	 * example, consider rearranging these for <code>x</code>:
	 *
	 * <pre>
	 * x + y < 1
	 * </pre>
	 *
	 * The resulting polynomial represents the "right-hand side" which (in this
	 * case) is 1-y. Thus, the rearranged inequality would be x < 1 - y.
	 *
	 * @param lhs
	 *            The "left-hand side" of the equation.
	 * @param rhs
	 *            The "right-hand side" of the equation.
	 * @param term
	 *            the given term being rearranged for.
	 */
	private static Polynomial rearrangeForUpperBound(Polynomial lhs, Polynomial rhs, Polynomial.Term term) {
		lhs = lhs.subtract(term);
		return rhs.add(lhs.negate());
	}
} public class ArrayEqualityCaseAnalysis extends AbstractProofRule implements Proof.LinearRule {
	private int skolem = 0;

	public ArrayEqualityCaseAnalysis(Simplification simplify, TypeSystem types) {
		super(simplify, types);
	}

	@Override
	public String getName() {
		return "Aeq-C";
	}

	@Override
	public State apply(State state, Formula truth) throws ResolutionError {
		if (truth instanceof Formula.Equality) {
			Formula.Equality eq = (Formula.Equality) truth;
			Expr lhs = eq.get(0);
			Expr rhs = eq.get(1);
			Type lhsT = types.inferType(state.getTypeEnvironment(), lhs);
			Type rhsT = types.inferType(state.getTypeEnvironment(), rhs);
			if (lhsT != null && rhsT != null) {
				Type.Array lhsArray = types.extractReadableArray(lhsT);
				Type.Array rhsArray = types.extractReadableArray(rhsT);
				if (lhsArray != null && rhsArray != null) {
					return expandArrayEquality(eq, state);
				}
			} else {
				// NOTE: it is possible to get here in some situations. This can
				// happen as a result of type test which has not yet been
				// properly processed.
			}
		}

		return state;
	}

	private State expandArrayEquality(Formula.Equality eq, Proof.State state) throws ResolutionError {
		Expr lhs = eq.get(0);
		Expr rhs = eq.get(1);
		if (lhs.getOpcode() == WyalFile.EXPR_arrinit && rhs.getOpcode() == WyalFile.EXPR_arrinit) {
			return expandArrayInitialiserInitialiserEquality(eq, (Expr.Operator) lhs, (Expr.Operator) rhs, state);
		} else if (lhs.getOpcode() == WyalFile.EXPR_arrgen && rhs.getOpcode() == WyalFile.EXPR_arrinit) {
			return expandArrayGeneratorInitialiserEquality(eq, (Expr.Operator) lhs, (Expr.Operator) rhs, state);
		} else if (lhs.getOpcode() == WyalFile.EXPR_arrinit && rhs.getOpcode() == WyalFile.EXPR_arrgen) {
			return expandArrayGeneratorInitialiserEquality(eq, (Expr.Operator) rhs, (Expr.Operator) lhs, state);
		} else if (lhs.getOpcode() == WyalFile.EXPR_arrgen && rhs.getOpcode() == WyalFile.EXPR_arrgen) {
			return expandArrayGeneratorGeneratorEquality(eq, (Expr.Operator) lhs, (Expr.Operator) rhs, state);
		} else if (!eq.getSign() && lhs.getOpcode() == WyalFile.EXPR_arrinit) {
			return expandArrayInitialiserNonEquality(eq, (Expr.Operator) lhs, rhs, state);
		} else if (!eq.getSign() && rhs.getOpcode() == WyalFile.EXPR_arrinit) {
			return expandArrayInitialiserNonEquality(eq, (Expr.Operator) rhs, lhs, state);
		} else if (!eq.getSign()) {
			return expandArrayArrayNonEquality(eq, lhs, rhs, state);
		}
		return state;
	}

	private State expandArrayInitialiserInitialiserEquality(Formula.Equality eq, Expr.Operator lhs, Expr.Operator rhs,
			Proof.State state) throws ResolutionError {
		if (lhs.size() != rhs.size()) {
			return state.subsume(this, new Formula.Truth(!eq.getSign()), eq);
		} else {
			Expr[] lhsOperands = lhs.getAll();
			Expr[] rhsOperands = rhs.getAll();
			Formula[] clauses = new Formula[lhsOperands.length];
			for (int i = 0; i != lhsOperands.length; ++i) {
				Expr lhsOperand = lhsOperands[i];
				Expr rhsOperand = rhsOperands[i];
				clauses[i] = Formulae.toFormula(equal(eq.getSign(), lhsOperand, rhsOperand), types);
			}
			//
			Formula f = eq.getSign() ? new Formula.Conjunct(clauses) : new Formula.Disjunct(clauses);
			return state.subsume(this, eq, f);
		}
	}

	private State expandArrayGeneratorInitialiserEquality(Formula.Equality eq, Expr.Operator lhs, Expr.Operator rhs,
			Proof.State state) throws ResolutionError {
		Expr lhsValue = lhs.get(0);
		Expr lhsSize = lhs.get(1);
		Expr rhsSize = new Expr.Constant(new Value.Int(rhs.size()));
		Expr[] rhsOperands = rhs.getAll();
		Formula[] clauses = new Formula[rhsOperands.length + 1];
		for (int i = 0; i != rhsOperands.length; ++i) {
			Expr rhsOperand = rhsOperands[i];
			clauses[i] = Formulae.toFormula(equal(eq.getSign(), lhsValue, rhsOperand), types);
		}
		clauses[rhsOperands.length] = Formulae.toFormula(equal(eq.getSign(), lhsSize, rhsSize), types);
		//
		Formula f = eq.getSign() ? new Formula.Conjunct(clauses) : new Formula.Disjunct(clauses);
		return state.subsume(this, eq, f);
	}

	private State expandArrayGeneratorGeneratorEquality(Formula.Equality eq, Expr.Operator lhs, Expr.Operator rhs,
			Proof.State state) throws ResolutionError {
		Expr lhsValue = lhs.get(0);
		Expr lhsSize = lhs.get(1);
		Expr rhsValue = rhs.get(0);
		Expr rhsSize = rhs.get(1);
		Formula c1 = Formulae.toFormula(equal(eq.getSign(), lhsSize, rhsSize), types);
		Formula c2 = Formulae.toFormula(equal(eq.getSign(), lhsValue, rhsValue), types);
		//
		Formula f = eq.getSign() ? new Formula.Conjunct(c1, c2) : new Formula.Disjunct(c1, c2);
		return state.subsume(this, eq, f);
	}

	private State expandArrayInitialiserNonEquality(Formula.Equality eq, Expr.Operator lhs, Expr rhs, Proof.State state)
			throws ResolutionError {
		Expr lhsSize = new Expr.Constant(new Value.Int(lhs.size()));
		Expr rhsSize = new Expr.ArrayLength(rhs);
		Expr[] lhsOperands = lhs.getAll();
		Formula[] clauses = new Formula[lhsOperands.length + 1];
		for (int i = 0; i != lhsOperands.length; ++i) {
			Expr index = new Expr.Constant(new Value.Int(i));
			Expr lhsOperand = lhsOperands[i];
			Expr rhsOperand = new Expr.ArrayAccess(rhs, index);
			clauses[i] = Formulae.toFormula(new Expr.NotEqual(lhsOperand, rhsOperand), types);
		}
		clauses[lhsOperands.length] = Formulae.toFormula(new Expr.NotEqual(lhsSize, rhsSize), types);
		Formula f = new Formula.Disjunct(clauses);
		return state.subsume(this, eq, f);
	}

	private State expandArrayArrayNonEquality(Formula.Equality eq, Expr lhs, Expr rhs, Proof.State state)
			throws ResolutionError {
		WyalFile.VariableDeclaration var = new WyalFile.VariableDeclaration(new Type.Int(),
				new Identifier("i:" + skolem++));
		Expr va = new Expr.VariableAccess(var);
		Expr lhsAccess = new Expr.ArrayAccess(lhs, va);
		Expr rhsAccess = new Expr.ArrayAccess(rhs, va);
		Formula body = notEquals(state, lhsAccess, rhsAccess, types);
		Expr lhsLen = new Expr.ArrayLength(lhs);
		Expr rhsLen = new Expr.ArrayLength(rhs);
		// The following axiom simply states that the length of every array
		// type is greater than or equal to zero.
		Formula axiom = new ArithmeticEquality(false, lhsLen, rhsLen);
		axiom = Formulae.or(axiom, new Quantifier(false, var, body));
		//
		return state.subsume(this, eq, axiom);
	}

	private static Formula notEquals(State state, Expr lhs, Expr rhs, TypeSystem types) throws ResolutionError {
		Type lhs_t = types.inferType(state.getTypeEnvironment(), lhs);
		Type rhs_t = types.inferType(state.getTypeEnvironment(), rhs);
		if (types.isRawSubtype(new Type.Int(), lhs_t) || types.isRawSubtype(new Type.Int(), rhs_t)) {
			return new ArithmeticEquality(false, lhs, rhs);
		} else {
			return new Formula.Equality(false, lhs, rhs);
		}
	}

	private static Expr equal(boolean sign, Expr lhs, Expr rhs) {
		if (sign) {
			return new Expr.Equal(lhs, rhs);
		} else {
			return new Expr.NotEqual(lhs, rhs);
		}
	}
} public class ArrayIndexAxiom extends AbstractClosureRule implements Proof.LinearRule {


	public ArrayIndexAxiom(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "ArrIdx-I";
	}

	@Override
	public State apply(Proof.Delta.Set existingTruths, Proof.State head, Formula truth) throws ResolutionError {
		head = attemptInstantiationByArrayAccess(truth,existingTruths,head);
		head = attemptInstantiationByEquation(truth,existingTruths,head);
		return head;
	}

	public State attemptInstantiationByEquation(Formula truth, Proof.Delta.Set existingTruths, Proof.State state) throws ResolutionError {
		for (int j = 0; j != existingTruths.size(); ++j) {
			Formula existing = existingTruths.get(j);
			List<Expr.Operator> matches = extractDefinedTerms(existing,WyalFile.EXPR_arridx);
			state = attemptInstantiation(existing,matches,truth,state);
		}
		return state;
	}

	public State attemptInstantiationByArrayAccess(Formula truth, Proof.Delta.Set existingTruths, Proof.State state) throws ResolutionError {
		List<Expr.Operator> matches = extractDefinedTerms(truth,WyalFile.EXPR_arridx);
		// At this point, we have one or more array access expressions which
		// potentially could be introduce some useful facts. Therefore, we need to look
		// back through the history to determine any cases where this can be applied.
		for (int j = 0; j != existingTruths.size(); ++j) {
			Formula existingTruth = existingTruths.get(j);
			state = attemptInstantiation(truth,matches,existingTruth,state);
		}
		return state;
	}

	public State attemptInstantiation(Formula source, List<Expr.Operator> matches, Formula target, Proof.State state) throws ResolutionError {
		//
		for (int i = 0; i != matches.size(); ++i) {
			Expr.Operator match = matches.get(i);
			Expr index = match.get(1);
			// NOTE: we must call construct here since we are creating a new
			// term from scratch.
			Expr length = new Expr.ArrayLength(match.get(0));
			// Now, try to match!
			if (target instanceof Formula.Inequality) {
				Formula.Inequality ieq = (Formula.Inequality) target;
				//
				if(match(ieq.get(1), index, Match.NONNEGATIVE)) {
					// A[i] ~ e && 0 >= i+1
					state = instantiateIndexAxiom(index,state,target,source);
				}
				//
				if (match(ieq.get(0), index, Match.NEGATIVE)
						&& match(ieq.get(1), length, Match.NONNEGATIVE)) {
					// A[i] ~ e && i-1 >= |A|+1 ==> i < |A|
					state = instantiateLengthAxiom(index, length, state, target, source);
				}
			} else if(target instanceof Formula.ArithmeticEquality) {
				Formula.ArithmeticEquality ieq = (Formula.ArithmeticEquality) target;
				// A[i] ~ e && |A| == c ==> i < |A|
				if (match(ieq.get(0), length, Match.NONNEGATIVE)
						|| match(ieq.get(1), length, Match.NONNEGATIVE)) {
					// A[i] ~ e && 0 >= i+1
					state = instantiateLengthAxiom(index,length,state,target,source);
				}
			}

		}
		return state;
	}

	private State instantiateIndexAxiom(Expr index, Proof.State state, Formula... dependencies) throws ResolutionError {
		Expr zero = new Expr.Constant(new WyalFile.Value.Int(0));
		Formula axiom = Formulae.greaterOrEqual(index, zero);
		axiom = simp.simplify(axiom);
		return state.infer(this, axiom, dependencies);
	}

	private State instantiateLengthAxiom(Expr index, Expr length, Proof.State state, Formula... dependencies) throws ResolutionError {
		Formula axiom = Formulae.lessThan(index, length);
		return state.infer(this, axiom, dependencies);
	}


	private enum Match {
		EXACT,
		NONNEGATIVE, // >= 0
		NEGATIVE  // < 0
	}

	private boolean match(Expr attempt, Expr ground, Match kind) {
		if (kind == Match.EXACT) {
			return attempt.equals(ground);
		}
		//
		Arithmetic.Polynomial lhs = Arithmetic.asPolynomial(attempt);
		Arithmetic.Polynomial rhs = Arithmetic.asPolynomial(ground);
		Arithmetic.Polynomial difference = lhs.subtract(rhs);
		if (difference.isConstant()) {
			BigInteger diff = difference.toConstant();
			if (kind == Match.NONNEGATIVE) {
				return diff.compareTo(BigInteger.ZERO) >= 0;
			} else {
				return diff.compareTo(BigInteger.ZERO) < 0;
			}
		} else {
			return false;
		}
	}
} public class ArrayIndexCaseAnalysis extends AbstractProofRule implements Proof.LinearRule {

	public ArrayIndexCaseAnalysis(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "ArrInd-C";
	}

	@Override
	public State apply(State state, Formula truth) throws ResolutionError {
		List<Expr.Operator> matches = extractDefinedTerms(truth,WyalFile.EXPR_arridx);
		if (matches.size() > 0) {
			for(int i=0;i!=matches.size();++i) {
				Expr.Operator match = matches.get(i);
				Formula[] cases = generateCaseAnalysis(match, truth, state);
				if(cases.length > 0) {
					Formula disjunct = new Formula.Disjunct(cases);
					state = state.subsume(this, truth, disjunct);
				}
			}
		}
		return state;
	}

	private Formula[] generateCaseAnalysis(Expr.Operator split, Formula truth, Proof.State state) {
		Formula[] result;
		switch (split.getOpcode()) {
		case WyalFile.EXPR_arridx: {
			Expr src = split.get(0);
			Expr j = split.get(1);
			if (src.getOpcode() == WyalFile.EXPR_arrupdt) {
				// xs[i:=v][j]
				Expr xs = (Expr) src.get(0);
				Expr i = (Expr) src.get(1);
				Expr v = (Expr) src.get(2);
				result = new Formula[2];
				Formula case1 = (Formula) substitute(split, v, truth);
				// NOTE: we must call construct here since we are creating a new
				// term from scratch.
				WyalFile.Expr arridx = new Expr.ArrayAccess(xs, j);
				Formula case2 = (Formula) substitute(split, arridx, truth);
				result[0] = Formulae.and(new Formula.ArithmeticEquality(true, i, j), case1);
				result[1] = Formulae.and(new Formula.ArithmeticEquality(false, i, j), case2);
				break;
			} else if (src.getOpcode() == WyalFile.EXPR_arrinit) {
				// [a,b,c][j] >= 0
				result = new Formula[src.size()];
				for (int i = 0; i != src.size(); ++i) {
					// a >= 0 && j == 0
					Expr ith = new Expr.Constant(new WyalFile.Value.Int(i));
					Formula lhs = (Formula) substitute(split, src.get(i), truth);
					Formula rhs = new Formula.ArithmeticEquality(true, j, ith);
					result[i] = Formulae.and(lhs, rhs);
				}
				break;
			}
		}
		default:
			// NOTE: we can arrive here if we extracted a defined term that
			// didn't meet our criteria above.
			return new Formula[0];
		}
		return result;
	}
} public class ArrayLengthAxiom extends AbstractProofRule implements Proof.LinearRule {

	public ArrayLengthAxiom(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "ArrLen-I";
	}

	@Override
	public State apply(Proof.State state, Formula truth) throws ResolutionError {
		// FIXME: there is a bug here because we might not find an array length
		// expression; rather we might find only the representative from its
		// equivalence class.
		if (truth instanceof Formula.Inequality) {
			Formula.Inequality inequality = (Formula.Inequality) truth;
			List<WyalFile.Expr> matches = findMatches(inequality.get(1));
			for (int i = 0; i != matches.size(); ++i) {
				WyalFile.Expr match = matches.get(i);
				Expr len = match;
				Expr zero = new Expr.Constant(new WyalFile.Value.Int(0));
				Formula axiom = Formulae.greaterOrEqual(len, zero);
				state = state.infer(this, simp.simplify(axiom), inequality);
			}
			return state;
		}
		// No change in the normal case
		return state;
	}

	/**
	 * <p>
	 * Find matches which can be used to instantiate the axiom. A match is
	 * simply an occurrence of an array length expression in a given polynomial.
	 * The is that it has to be on the positive side of an inequality. For
	 * example, "|xs|" matches in "0 < |xs|". In contrast, "|xs|" does not match
	 * in "|xs| > 0". The reason for this simply that the instantiated axiom
	 * cannot benefit the latter case.
	 * </p>
	 *
	 * @param poly
	 * @return
	 */
	private List<WyalFile.Expr> findMatches(Expr poly) {
		if (poly instanceof Expr.Operator) {
			ArrayList<WyalFile.Expr> matches = new ArrayList<>();
			Expr.Operator op = (Expr.Operator) poly;
			switch (op.getOpcode()) {
			case WyalFile.EXPR_arrlen:
				matches.add(poly);
				break;
			case WyalFile.EXPR_add:
			case WyalFile.EXPR_sub:
			case WyalFile.EXPR_mul:
			case WyalFile.EXPR_div:
			case WyalFile.EXPR_rem:
				for (int i = 0; i != poly.size(); ++i) {
					Expr term = op.get(i);
					matches.addAll(findMatches(term));
				}
			}
			return matches;
		} else {
			return Collections.EMPTY_LIST;
		}
	}
} public class FunctionCallAxiom extends AbstractProofRule implements Proof.LinearRule {

	public FunctionCallAxiom(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "FunCall-I";
	}

	@Override
	public State apply(State state, Formula truth) throws ResolutionError {
		List<Expr.Invoke> matches = extractDefinedTerms(truth,WyalFile.EXPR_invoke);
		if (matches.size() > 0) {
			for (int i = 0; i != matches.size(); ++i) {
				Expr.Invoke ivk = matches.get(i);
				// Determine the type declaration in question
				Type.FunctionOrMacroOrInvariant af = ivk.getSignatureType();
				if(af instanceof Type.Function) {
					state = applySpecificationInstantiation(state, truth, matches.get(i));
				}
			}
		}
		return state;
	}

	/**
	 * Instantiate the specification of a given (defined) function invocation.
	 *
	 * @param state
	 * @param truth
	 * @param ivk
	 * @return
	 */
	private State applySpecificationInstantiation(Proof.State state, Formula truth, Expr.Invoke ivk) throws ResolutionError {
		// FIXME: this resolution should have already been performed
		// elsewhere
		Declaration.Named.Function decl = resolve(ivk);
		if (decl != null) {
			// FIXME: there are bugs in the procedure before when new
			// terms are introduced, but not taken to the representative of
			// their equivalence class.
			//
			// Calculate the precondition
			Formula precondition = expandFunctionPrecondition(decl, ivk.getArguments());
			//
			if (precondition != null) {
				state = state.infer(this, simp.simplify(precondition), truth);
			}
			// Calculate the postcondition
			Formula postcondition = expandFunctionPostcondition(decl, ivk);
			//
			if (postcondition != null) {
				state = state.infer(this, postcondition, truth);
			}
		}
		return state;
	}

	private Formula expandFunctionPrecondition(Declaration.Named.Function decl, Tuple<Expr> arguments) throws ResolutionError {
		Formula precondition = null;
		Tuple<VariableDeclaration> parameters = decl.getParameters();
		for (int i = 0; i != parameters.size(); ++i) {
			VariableDeclaration parameter = parameters.get(i);
			Expr argument = arguments.get(i);
			Formula clause = types.extractInvariant(parameter.getType(), argument);
			precondition = or(precondition, clause);
		}
		return precondition;
	}

	private Formula expandFunctionPostcondition(Declaration.Named.Function decl, Expr.Invoke ivk) throws ResolutionError {
		Tuple<VariableDeclaration> returns = decl.getReturns();
		Value.Int selector = ivk.getSelector();
		int index = selector == null ? 0 : selector.get().intValue();
		VariableDeclaration parameter = returns.get(index);
		return types.extractInvariant(parameter.getType(), ivk);
	}

	private Formula or(Formula lhs, Formula rhs) {
		if(lhs == null) {
			return rhs;
		} else if(rhs == null) {
			return lhs;
		} else {
			return new Formula.Disjunct(lhs,rhs);
		}
	}

	private Declaration.Named.Function resolve(Expr.Invoke ivk) throws ResolutionError {
		Type.FunctionOrMacroOrInvariant signature = ivk.getSignatureType();
		List<Declaration.Named.Function> candidates = types.resolveAll(ivk.getName(),Declaration.Named.Function.class);
		for(int i=0;i!=candidates.size();++i) {
			Declaration.Named.Function fun = candidates.get(i);
			if(fun.getSignatureType().equals(signature)) {
				return fun;
			}
		}
		//
		// Should really be impossible to get here
		throw new NameNotFoundError(ivk.getName());
	}

} public class MacroExpansion extends AbstractProofRule implements Proof.LinearRule {

	public MacroExpansion(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "Macro-I";
	}

	@Override
	public State apply(Proof.State state, Formula truth) throws ResolutionError {
		Formula expanded = expandFormula(state, truth);
		if(expanded != truth) {
			state = state.subsume(this, truth, expanded);
		}
		return state;
	}

	private Formula expandFormula(Proof.State state, Formula formula) throws ResolutionError {
		if (formula instanceof Formula.Invoke) {
			Formula.Invoke ivk = (Formula.Invoke) formula;
			// Determine the type declaration in question
			Type.FunctionOrMacroOrInvariant af = ivk.getSignatureType();
			if(af instanceof Type.Function) {
				// We ignore function macros here
				return null;
			}
			// Resolve the declaration corresponding to this invocation
			Declaration.Named decl = resolve(ivk);
			//
			Formula invariant = extractDeclarationInvariant(state, decl, ivk.getArguments());
			if (invariant != null) {
				if (!ivk.getSign()) {
					invariant = Formulae.invert(invariant);
				}
				// Update the state
				return invariant;
			}
		} else if(formula instanceof Formula.Quantifier) {
			Formula.Quantifier quantifier = (Formula.Quantifier) formula;
			if(quantifier.getSign()) {
				// There's no point going into existentials since they will be
				// expanded anyway,
				Formula body = expandFormula(state, quantifier.getBody());
				if(body != quantifier.getBody()) {
					return new Formula.Quantifier(true, quantifier.getParameters(), body);
				}
			}
		} else if(formula instanceof Formula.Disjunct) {
			Formula.Disjunct disjunct = (Formula.Disjunct) formula;
			Formula[] children = disjunct.getAll();
			Formula[] nChildren = expandFormula(state, children);
			if(nChildren != children) {
				return new Formula.Disjunct(nChildren);
			}
		} else if(formula instanceof Formula.Conjunct) {
			Formula.Conjunct disjunct = (Formula.Conjunct) formula;
			Formula[] children = disjunct.getAll();
			Formula[] nChildren = expandFormula(state, children);
			if(nChildren != children) {
				return new Formula.Conjunct(nChildren);
			}
		}
		return formula;
	}

	private Formula[] expandFormula(Proof.State state, Formula... children) throws ResolutionError {
		Formula[] nChildren = children;
		for(int i=0;i!=children.length;++i) {
			Formula child = nChildren[i];
			Formula nChild = expandFormula(state, child);
			if(child != nChild && nChildren == children) {
				nChildren = Arrays.copyOf(children, children.length);
			}
			nChildren[i] = nChild;
		}
		return nChildren;
	}

	private Formula extractDeclarationInvariant(Proof.State state, Declaration.Named decl, Tuple<Expr> arguments) throws ResolutionError {
		if (decl instanceof Declaration.Named.Type) {
			// This is a type invariant macro call. In such case, we
			// need to first determine what the invariant actually is.
			Declaration.Named.Type td = (Declaration.Named.Type) decl;
			// Expand the corresponding type invariant
			return expandTypeInvariant(state, td, arguments.get(0));
		} else if (decl instanceof Declaration.Named.Macro) {
			Declaration.Named.Macro md = (Declaration.Named.Macro) decl;
			// Expand the macro body with appropriate substitutions
			return expandMacroBody(state, md, arguments);
		} else {
			// Functions are ignored
			return null;
		}
	}

	private Formula expandMacroBody(Proof.State state, Declaration.Named.Macro md, Tuple<Expr> arguments) throws ResolutionError {
		Tuple<VariableDeclaration> parameters = md.getParameters();
		// Initialise the map with the identity for parameters to ensure they
		// are preserved as is, and can then be substituted.
		Map<SyntacticItem, SyntacticItem> map = new IdentityHashMap<>();
		for (int i = 0; i != parameters.size(); ++i) {
			map.put(parameters.get(i), parameters.get(i));
		}
		// Clone is required at this point to ensure that any variable
		// declarations are distinguished appropriately.
		WyalFile.Stmt.Block block = SyntacticHeaps.cloneOnly(md.getBody(), map, WyalFile.VariableDeclaration.class);
		Formula body = Formulae.toFormula(block, types);
		for (int i = 0; i != arguments.size(); ++i) {
			// At this point, we must substitute the parameter name used in
			// the type declaration for the name used as the invocation
			// argument.
			Expr.VariableAccess parameter = new Expr.VariableAccess(parameters.get(i));
			body = (Formula) substitute(parameter, arguments.get(i), body);
		}
		return body;
	}

	private Formula expandTypeInvariant(Proof.State state, Declaration.Named.Type td, Expr argument) throws ResolutionError {
		// Extract only the explicit invariants given using where clauses.
		Tuple<Block> invariant = td.getInvariant();
		Formula result = types.extractInvariant(td.getVariableDeclaration().getType(), argument);
		for (int i = 0; i != invariant.size(); ++i) {
			// Convert the invariant clause into a formula
			Formula ith = Formulae.toFormula(invariant.get(i), types);
			//
			result = result == null ? ith : new Formula.Conjunct(result, ith);
		}
		if (result == null) {
			return null;
		} else {
			// At this point, we must substitute the variable name used in
			// the type declaration for the name used as the invocation
			// argument.

			// FIXME: this is only necessary for the invariant itself, not the
			// extracted type invariant.

			Expr.VariableAccess parameter = new Expr.VariableAccess(td.getVariableDeclaration());
			result = (Formula) substitute(parameter, argument, result);
			return result;
		}
	}

	private Declaration.Named resolve(Expr.Invoke ivk) throws ResolutionError {
		if (ivk.getSignatureType() instanceof Type.Property) {
			List<Declaration.Named.Macro> candidates = types.resolveAll(ivk.getName(), Declaration.Named.Macro.class);
			Type.FunctionOrMacroOrInvariant signature = ivk.getSignatureType();
			for (int i = 0; i != candidates.size(); ++i) {
				Declaration.Named.Macro macro = candidates.get(i);
				if (macro.getSignatureType().equals(signature)) {
					return macro;
				}
			}
			//
			// Should really be impossible to get here
			throw new NameNotFoundError(ivk.getName());
		} else {
			return types.resolveExactly(ivk.getName(), Declaration.Named.Type.class);
		}
	}
} public class AndElimination extends AbstractProofRule implements Proof.LinearRule {

	public AndElimination(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "And-E";
	}

	@Override
	public State apply(Proof.State head, Formula truth) {
		if (truth instanceof Formula.Conjunct) {
			Formula.Conjunct conjunct = (Formula.Conjunct) truth;
			for(int i=0;i!=conjunct.size();++i) {
				head = head.subsume(this, conjunct, conjunct.get(i));
			}
			return head;
		} else {
			// No change in the normal case
			return head;
		}
	}

} public class OrElimination implements Proof.NonLinearRule {

	@Override
	public String getName() {
		return "Or-E";
	}

	@Override
	public Proof.State[] apply(Proof.State current, Proof.State head) throws ResolutionError {
		Proof.Delta.Set additions = current.getDelta().getAdditions();
		if(additions.size() > 1) {
			throw new IllegalArgumentException("should be impossible to get here");
		} else if(additions.size() != 0) {
			Proof.Delta delta = head.getDelta(current);
			Formula truth = additions.get(0);
			if(!delta.isRemoval(truth)) {
				// Truth not yet subsumed by existing rule
				return apply(head, truth);
			}
		}
		return new Proof.State[]{head};
	}

	public Proof.State[] apply(Proof.State state, Formula truth) {
		if(truth instanceof Formula.Disjunct) {
			Formula.Disjunct disjunct = (Formula.Disjunct) truth;
			Formula[] cases = disjunct.getAll();
			Proof.State[] result = new Proof.State[cases.length];
			for (int i = 0; i != cases.length; ++i) {
				result[i] = state.subsume(this,disjunct,cases[i]);
			}
			return result;
		} else {
			// No change in the normal case
			return new Proof.State[]{state};
		}
	}
} public class ExhaustiveQuantifierInstantiation extends AbstractClosureRule implements Proof.LinearRule {

	public ExhaustiveQuantifierInstantiation(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "Forall-I";
	}

	@Override
	public State apply(Proof.Delta.Set existingTruths, Proof.State state, Formula newTruth) throws ResolutionError {
		if (newTruth instanceof Formula.ArithmeticEquation) {
			Formula.ArithmeticEquation ground = (Formula.ArithmeticEquation) newTruth;
			return instantiateQuantifiers(existingTruths, ground, state);
		} else if (newTruth instanceof Formula.Quantifier) {
			Formula.Quantifier quantifier = (Formula.Quantifier) newTruth;
			return instantiateQuantifiers(existingTruths, quantifier, state);
		}
		// No change in the normal case
		return state;
	}

	/**
	 * Attempt to match a given quantifier against any appropriate ground terms.
	 * This may fail if no suitable bindings can be found.
	 *
	 * @param quantifier
	 * @param state
	 * @return
	 */
	private State instantiateQuantifiers(Proof.Delta.Set existingTruths, Formula.Quantifier quantifier, State state) throws ResolutionError {
		if (quantifier.getSign()) {
			// At this point, we have a quantifier which has not been seen
			// before (for example, it was hiding inside a macro invocation
			// somewhere). Therefore, we need to search the history looking for
			// suitable opportunities to instantiate it.
			for (int i = 0; i != existingTruths.size(); ++i) {
				Formula existingTruth = existingTruths.get(i);
				if (existingTruth instanceof Formula.ArithmeticEquation) {
					Formula.ArithmeticEquation ground = (Formula.ArithmeticEquation) existingTruth;
					// Yes, this is a universal quantifier
					state = applyQuantifierInstantiation(quantifier, ground, state);
				} else {
					// FIXME: we need to handle Assignment here
				}
			}
		}
		//
		return state;
	}

	/**
	 * Attempt to match a given ground term against any active quantifiers in an
	 * effort to instantiate them one or more times. This may fail if no
	 * suitable bindings can be found.
	 *
	 * @param groundTerm
	 * @param state
	 * @return
	 */
	private State instantiateQuantifiers(Proof.Delta.Set existingTruths, Formula.ArithmeticEquation groundTerm, State state) throws ResolutionError {
		// At this point, we have an equality or inequality which potentially
		// could be used to instantiate one or more existing (universal)
		// quantifiers. Therefore, we need to look back through the history to
		// determine any cases where this can be applied.
		for (int i = 0; i != existingTruths.size(); ++i) {
			Formula existingTruth = existingTruths.get(i);
			if (existingTruth instanceof Formula.Quantifier) {
				Formula.Quantifier qf = (Formula.Quantifier) existingTruth;
				if (qf.getSign()) {
					// Yes, this is a universal quantifier
					state = applyQuantifierInstantiation(qf, groundTerm, state);
				}
			}
		}
		//
		return state;
	}

	private State applyQuantifierInstantiation(Formula.Quantifier quantifier, Formula.Equation groundTerm, State state)
			throws ResolutionError {
		// FIXME: I believe there is a bug here in the (unlikely?) situation
		// that we can in fact match *multiple* variables in the same quantifier
		// against the same ground term.
		Tuple<VariableDeclaration> parameters = quantifier.getParameters();
		for (int i = 0; i != parameters.size(); ++i) {
			VariableDeclaration variable = parameters.get(i);
			state = attemptQuantifierInstantiation(quantifier, variable, groundTerm, state);
		}
		return state;
	}

	/**
	 * Attempt to instantiate a given variable of a universal quantifier. This
	 * searches a given ground term for appropriate bindings for the variable in
	 * question. If any are found, then the quantifier is instantiated
	 * separately for each.
	 *
	 * @param quantifier
	 *            --- The universal quantifier to be instantiated.
	 * @param variable
	 *            --- The quantified variable declared in the universal
	 *            quantifier to be instantiated.
	 * @param groundTerm
	 *            --- The term with which we will attempt to bind the quantified
	 *            variable against, thereby producing appropriate bindings for
	 *            the instantiation (or not, if none exist).
	 * @param state
	 *            --- The state in which the instantiated quantifier will be
	 *            asserted.
	 * @return
	 */
	private State attemptQuantifierInstantiation(Formula.Quantifier quantifier, VariableDeclaration variable,
			Formula.Equation groundTerm, State state) throws ResolutionError {
		// Exhaustively instantiate this variable with all possible ground
		// terms.
		List<Expr> grounds = bind(state, variable, quantifier.getBody(), groundTerm);
		//
		for (int i = 0; i != grounds.size(); ++i) {
			Expr ground = grounds.get(i);
			// NOTE: we don't bother checking the type of the term being
			// instantiated here. That's because (at the moment) this is only
			// matching integer terms anyway. In the future, if we relax this,
			// then we might need a different approach.
			state = instantiateQuantifier(quantifier, variable, groundTerm, ground, state);
		}
		return state;
	}

	/**
	 * <p>
	 * Instantiate the body of a universal quantifier using a binding for a
	 * given quantified variable. For example, instantiating
	 * <code>forall(int i).(xs[i] >= 0)</code> with the binding <code>i=1</code>
	 * would produce the ground term <code>xs[1] >= 0</code>.
	 * </p>
	 * <p>
	 * Note that this procedure does not always eliminate the quantifier itself.
	 * For example, instantiating <code>forall(int i, int j).(xs[i] >= j)</code>
	 * with the binding <code>i=1</code> would produce the quantified term
	 * <code>forall(int j).(xs[1] >= j)</code>.
	 * </p>
	 *
	 * @param quantifier
	 *            --- The universal quantifier to be instantiated.
	 * @param variable
	 *            --- The quantified variable declared in the universal
	 *            quantifier to be instantiated.
	 * @param binding
	 *            --- The binding to be used to instantiated the quantified
	 *            variable with. In other words, all occurences of the
	 *            quantified variable are replaced with this expression.
	 * @param state
	 *            --- The state in which the instantiated quantifier will be
	 *            asserted.
	 * @return
	 */
	private State instantiateQuantifier(Formula.Quantifier quantifier, VariableDeclaration variable,
			Formula.Equation groundTerm, Expr binding, State state) throws ResolutionError {
		Tuple<VariableDeclaration> parameters = quantifier.getParameters();
		// Substitute body through for the binding obtained the given parameter
		Formula grounded = quantifier.getBody();
		Expr access = new Expr.VariableAccess(variable);
		grounded = (Formula) substitute(access, binding, grounded);
		// Expand any type invariant associated with this variable
		Formula invariant = types.extractInvariant(variable.getType(), new Expr.VariableAccess(variable));
		// Add type invariants (if appropriate)
		if (invariant != null) {
			grounded = new Disjunct(Formulae.invert(invariant), grounded);
		}
		// Determine whether quantified variables still exist.
		if (parameters.size() > 1) {
			// This does not represent a complete instantiation of this
			// quantifier. Therefore, we need to retain all quantified variables
			// except that which was instantiated.
			VariableDeclaration[] stripped = stripInstantiatedParameter(parameters, variable);
			// Re-quantify remaining variables
			grounded = new Formula.Quantifier(true, stripped, grounded);
		}
		// Finally, assert the newly instantiated quantifier in the current
		// state.
		grounded = simp.simplify(grounded);
		return state.infer(this, grounded, quantifier, groundTerm);
	}

	/**
	 * Remove a given parameter declaration from an array of parameter
	 * declarations, producing an array of length exactly one less than the
	 * original.
	 *
	 * @param parameters
	 * @param variable
	 * @return
	 */
	private VariableDeclaration[] stripInstantiatedParameter(Tuple<VariableDeclaration> parameters,
			VariableDeclaration variable) {
		VariableDeclaration[] result = new VariableDeclaration[parameters.size() - 1];
		for (int i = 0, j = 0; i != parameters.size(); ++i) {
			VariableDeclaration parameter = parameters.get(i);
			if (parameter != variable) {
				result[j++] = parameter;
			}
		}
		return result;
	}

	/**
	 * Match a given term quantified over a given variable against a ground
	 * term. For example, if "i" is a quantified variable then we might try
	 * matching "A[i] < 0" against "0 < A[1]". In this case, our list of matches
	 * would contain just "1". Observe that the key here is that the matches are
	 * occurring on opposite "sides" of the equation. This is important for
	 * being "goal driven" in that we are looking for potential contradictions.
	 *
	 * @param variable
	 * @return
	 */
	private List<Expr> bind(Proof.State state, VariableDeclaration variable, Formula quantified, Formula.Equation ground) throws ResolutionError {
		ArrayList<Expr> result = new ArrayList<>();
		//
		if (quantified instanceof Formula.Inequality && ground instanceof Formula.Inequality) {
			//
			Formula.Inequality ieq = (Formula.Inequality) quantified;
			// Positive (Quantified) versus Negative (Ground)
			List<Expr> posNegMatches = bind(state, variable, ieq.get(0), ground.get(1), Match.NEGATIVE);
			// Negative (Quantified) versus Positive (Ground)
			List<Expr> negPosMatches = bind(state, variable, ieq.get(1), ground.get(0), Match.POSITIVE);
			//
			result.addAll(posNegMatches);
			result.addAll(negPosMatches);
		} else if (quantified instanceof Formula.Equation) {
			Formula.Equation ieq = (Formula.Equation) quantified;
			Match leftSign = getSign(ieq,ground,0);
			Match rightSign = getSign(ieq,ground,1);
			List<Expr> posPosMatches = bind(state, variable, ieq.get(0), ground.get(0), leftSign);
			List<Expr> posNegMatches = bind(state, variable, ieq.get(0), ground.get(1), rightSign);
			List<Expr> negPosMatches = bind(state, variable, ieq.get(1), ground.get(0), leftSign);
			List<Expr> negNegMatches = bind(state, variable, ieq.get(1), ground.get(1), rightSign);
			//
			result.addAll(posPosMatches);
			result.addAll(posNegMatches);
			result.addAll(negPosMatches);
			result.addAll(negNegMatches);
		} else if (quantified instanceof Formula.Conjunct) {
			Formula.Conjunct c = (Formula.Conjunct) quantified;
			for (int i = 0; i != c.size(); ++i) {
				result.addAll(bind(state, variable, c.get(i), ground));
			}
		} else if (quantified instanceof Formula.Disjunct) {
			Formula.Disjunct c = (Formula.Disjunct) quantified;
			for (int i = 0; i != c.size(); ++i) {
				result.addAll(bind(state, variable, c.get(i), ground));
			}
		}
		return result;
	}

	private Match getSign(Formula.Equation quantified, Formula.Equation ground, int operand) {
		if (quantified instanceof Formula.Equality && ground instanceof Formula.Equality) {
			return Match.EXACT;
		} else if (operand == 0) {
			return Match.POSITIVE;
		} else {
			return Match.NEGATIVE;
		}
	}

	private enum Match {
		EXACT,
		POSITIVE, // >= 0
		NEGATIVE  // <= 0
	}

	/**
	 * <p>
	 * Here, we have a quantified expression (e.g. A[k]) and a ground expression
	 * (e.g. A[0]). Our goal is to "guess" an appropriate instantiation of k
	 * which gives A[0]. Instead of trying to be too clever (e.g. some kind of
	 * matching), we're going to take a more "exhaustive" approach. That is,
	 * given some set of ground terms, we're just going to substitute *every*
	 * ground term for the quantified variable and see whether the result is a
	 * match. There are lots of reasons why this turns out to be quite a good
	 * idea.
	 * </p>
	 * <p>
	 * The important question is from where we derive our set of ground terms to
	 * try. If this set is too small, we may not be able to figure out what we
	 * need. For example, consider matching A[k-1] against A[0]. The ground term
	 * we need is -1 here.
	 * </p>
	 *
	 * @param variable
	 * @param quantified
	 * @param ground
	 * @return
	 */
	private List<Expr> bind(Proof.State state, VariableDeclaration variable, Expr quantified, Expr ground, Match kind) throws ResolutionError {
		//
		if (containsTrigger(quantified,variable)) {
			Expr access = new Expr.VariableAccess(variable);
			List<Expr> candidates = determineGroundTerms(ground, new ArrayList<>());
			List<Expr> result = new ArrayList<>();
			for (int i = 0; i != candidates.size(); ++i) {
				Expr candidate = candidates.get(i);
				Expr attempt = (Expr) substitute(access, candidate, quantified);
				// Attempt the match
				if (match(attempt,ground,kind)) {
					// Awesome, we made a correct guess!!!
					result.add(candidate);
				}
			}
			return result;
		} else {
			return Collections.EMPTY_LIST;
		}
	}

	private boolean match(Expr attempt, Expr ground, Match kind) {
		//
		Arithmetic.Polynomial lhs = Arithmetic.asPolynomial(attempt);
		Arithmetic.Polynomial rhs = Arithmetic.asPolynomial(ground);
		Arithmetic.Polynomial difference = lhs.subtract(rhs);
		if (difference.isConstant()) {
			BigInteger diff = difference.toConstant();
			if(kind == Match.EXACT) {
				return diff.compareTo(BigInteger.ZERO) == 0;
			} else if (kind == Match.POSITIVE) {
				return diff.compareTo(BigInteger.ZERO) >= 0;
			} else {
				return diff.compareTo(BigInteger.ZERO) <= 0;
			}
		} else {
			return false;
		}
	}

	private List<Expr> determineGroundTerms(Expr e, List<Expr> grounds) {
		for (int i = 0; i != e.size(); ++i) {
			SyntacticItem child = e.get(i);
			if (child instanceof Expr) {
				determineGroundTerms((Expr) child, grounds);
			} else if(child instanceof WyalFile.Tuple) {
				// FIXME: this can occur for the parameters of a function
				// invocation. Perhaps not ideal actually.
				Tuple<?> t = (Tuple<?>) child;
				for(SyntacticItem p : t.getAll()) {
					if (p instanceof Expr) {
						determineGroundTerms((Expr) p, grounds);
					}
				}
			}
		}
		grounds.add(e);
		return grounds;
	}

	/**
	 * Determine whether a given expression contains a "trigger" or not. That
	 * is, a special term which we are using to signal that an instantiation
	 * makes sense.
	 *
	 * @param ground
	 * @return
	 */
	private boolean containsTrigger(Expr e, VariableDeclaration variable) {
		if(isTrigger(e, variable)) {
			return true;
		} else {
			for (int i = 0; i != e.size(); ++i) {
				SyntacticItem child = e.get(i);
				if (child instanceof Expr) {
					if(containsTrigger((Expr) child, variable)) {
						return true;
					}
				} else if(child instanceof WyalFile.Tuple) {
					// FIXME: this can occur for the parameters of a function
					// invocation. Perhaps not ideal actually.
					Tuple<?> t = (Tuple<?>) child;
					for(SyntacticItem p : t.getAll()) {
						if (p instanceof Expr) {
							if(containsTrigger((Expr) p, variable)) {
								return true;
							}
						}
					}
				}
			}
			return false;
		}
	}

	private boolean isTrigger(Expr e, VariableDeclaration variable) {
		if(e.getOpcode() == WyalFile.EXPR_arridx) {
			Expr.Operator arridx = (Expr.Operator) e;
			// Check whether the index includes the quantified variable or not.
			return containsQuantifiedVariable(arridx.get(1),variable);
		}
		return false;
	}

	/**
	 * Determine whether a given expression contains the quantified variable or
	 * not.
	 *
	 * @param e
	 *            --- expression we are checking to see whether it's quantified.
	 * @param variable
	 *            --- the quantified variable we are looking for.
	 * @return
	 */
	private boolean containsQuantifiedVariable(Expr e, VariableDeclaration variable) {
		if(isQuantifiedVariableAccess(e,variable)) {
			return true;
		} else {
			for (int i = 0; i != e.size(); ++i) {
				SyntacticItem child = e.get(i);
				if (child instanceof Expr) {
					if(containsQuantifiedVariable((Expr) child, variable)) {
						return true;
					}
				} else if(child instanceof WyalFile.Tuple) {
					// FIXME: this can occur for the parameters of a function
					// invocation. Perhaps not ideal actually.
					Tuple<?> t = (Tuple<?>) child;
					for(SyntacticItem p : t.getAll()) {
						if (p instanceof Expr) {
							if(containsQuantifiedVariable((Expr) p, variable)) {
								return true;
							}
						}
					}
				}
			}
			return false;
		}
	}

	private boolean isQuantifiedVariableAccess(Expr e, VariableDeclaration variable) {
		if(e instanceof Expr.VariableAccess) {
			Expr.VariableAccess va = (Expr.VariableAccess) e;
			return va.getVariableDeclaration().equals(variable);
		}
		return false;
	}
} public class ExistentialElimination extends AbstractProofRule implements Proof.LinearRule {

	public ExistentialElimination(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "Exists-E";
	}

	@Override
	public State apply(Proof.State head, Formula truth) throws ResolutionError {
		if(truth instanceof Formula.Quantifier) {
			Formula.Quantifier qf = (Formula.Quantifier) truth;
			if(!qf.getSign()) {
				Formula body = qf.getBody();
				// Expand any type invariants
				Formula invariant = expandTypeInvariants(qf.getParameters(),types);
				// Add type invariants (if appropriate)
				if (invariant != null) {
					body = new Conjunct(invariant, body);
				}
				head = head.subsume(this, qf, body);
			}
		}
		// No change in the normal case
		return head;
	}

	/**
	 * For a given sequence of variable declarations expand their type
	 * invariants as appropriate. This expansion is done lazily, in that it
	 * produces invocations to the type invariants themselves. Such invocations
	 * must then be separately expanded (like macros) later on. As an example,
	 * consider this:
	 *
	 * <pre>
	 * type nat is (int x) where x >= 0
	 *
	 * assert:
	 *     forall(nat x):
	 *         x >= 0
	 * </pre>
	 *
	 * The type invariant given for <code>x</code> in the quantifier will be
	 * expanded, to give then body <code>nat(x) ==> x >= 0</code>. The call
	 * <code>nat(x)</code> will later be expanded during theorem proving to
	 * <code>x >= 0</code>. The reason this is done lazily is to properly
	 * support recursive types and their invariants.
	 *
	 * @param declarations
	 * @param types
	 * @return
	 * @throws ResolutionError
	 */
	protected Formula expandTypeInvariants(Tuple<VariableDeclaration> declarations, TypeSystem types)
			throws ResolutionError {
		Formula result = null;
		for (int i = 0; i != declarations.size(); ++i) {
			VariableDeclaration variable = declarations.get(i);
			Formula invariant = types.extractInvariant(variable.getType(), new Expr.VariableAccess(variable));
			// FIXME: need to perform appropriate variable substitution here?
			if (invariant != null && result == null) {
				result = invariant;
			} else if (invariant != null) {
				result = new Conjunct(result, invariant);
			}
		}
		return result;
	}
} public class RecordEqualityCaseAnalysis extends AbstractProofRule implements Proof.LinearRule {

	public RecordEqualityCaseAnalysis(Simplification simplify, TypeSystem types) {
		super(simplify, types);
	}

	@Override
	public String getName() {
		return "Req-C";
	}

	@Override
	public State apply(State state, Formula truth) throws ResolutionError {
		if (truth instanceof Formula.Equality) {
			Formula.Equality eq = (Formula.Equality) truth;
			Expr lhs = eq.get(0);
			Expr rhs = eq.get(1);
			Type lhsT = types.inferType(state.getTypeEnvironment(), lhs);
			Type rhsT = types.inferType(state.getTypeEnvironment(), rhs);
			if (lhsT != null && rhsT != null) {
				Type.Record lhsRecord = types.extractReadableRecord(lhsT);
				Type.Record rhsRecord = types.extractReadableRecord(rhsT);
				if (lhsRecord != null && rhsRecord != null) {
					return expandRecordEquality(eq, state);
				}
			} else {
				// NOTE: it is possible to get here in some situations. This can
				// happen as a result of type test which has not yet been
				// properly processed.
			}
		}

		return state;
	}

	private State expandRecordEquality(Formula.Equality eq, Proof.State state) throws ResolutionError {
		Expr lhs = eq.get(0);
		Expr rhs = eq.get(1);
		if (eq.getSign()) {
			// Equality
			if (lhs instanceof Expr.RecordInitialiser && rhs instanceof Expr.RecordInitialiser) {
				return expandRecordInitialiserEquality(eq, (Expr.RecordInitialiser) lhs, (Expr.RecordInitialiser) rhs,
						state);
			}
		} else {
			// Non-Equality
			return expandRecordNonEquality(eq, lhs, rhs, state);
		}
		return state;
	}

	private State expandRecordNonEquality(Formula.Equality eq, Expr lhs, Expr rhs, Proof.State state)
			throws ResolutionError {
		Type lhs_t = types.inferType(state.getTypeEnvironment(), lhs);
		Type.Record lhs_r = types.extractReadableRecord(lhs_t);
		FieldDeclaration[] fields = lhs_r.getFields();
		Formula[] clauses = new Formula[fields.length];
		for (int i = 0; i != fields.length; ++i) {
			Expr lf = new Expr.RecordAccess(lhs, fields[i].getVariableName());
			Expr rf = new Expr.RecordAccess(rhs, fields[i].getVariableName());
			clauses[i] = Formulae.toFormula(new Expr.NotEqual(lf, rf), types);
		}
		// FIXME: what to do for open records?
		Formula disjunct = new Formula.Disjunct(clauses);
		return state.subsume(this, eq, disjunct);
	}

	private State expandRecordInitialiserEquality(Formula.Equality eq, Expr.RecordInitialiser lhs,
			Expr.RecordInitialiser rhs, Proof.State state) throws ResolutionError {
		if (lhs.size() != rhs.size()) {
			// FIXME: for open records this could be possible
			return state.infer(this, new Formula.Truth(false), eq);
		} else {
			Pair<Identifier, Expr>[] lhsFields = lhs.getFields();
			Pair<Identifier, Expr>[] rhsFields = rhs.getFields();
			Formula[] clauses = new Formula[lhsFields.length];
			for (int i = 0; i != lhsFields.length; ++i) {
				Pair<Identifier, Expr> lhsField = lhsFields[i];
				Pair<Identifier, Expr> rhsField = rhsFields[i];
				if (!lhsField.getFirst().equals(rhsField.getFirst())) {
					// FIXME: could do more here --- esp to handle out-of-order
					// field declarations.
					return state.infer(this, new Formula.Truth(false), eq);
				}
				Expr lf = lhsField.getSecond();
				Expr rf = rhsField.getSecond();
				// NOTE: don't need to call construct here, since generating a
				// formula.
				clauses[i] = Formulae.toFormula(new Expr.Equal(lf, rf), types);
			}
			Formula disjunct = new Formula.Conjunct(clauses);
			return state.subsume(this, eq, disjunct);
		}
	}
} public class TypeTestClosure extends AbstractClosureRule implements Proof.LinearRule {

	public TypeTestClosure(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "Is-I";
	}

	@Override
	public State apply(Proof.Delta.Set existingTruths, Proof.State head, Formula newTruth) throws ResolutionError {
		if (newTruth instanceof Formula.Is) {
			Formula.Is test = (Formula.Is) newTruth;
			head = apply(existingTruths, test, head);
		}
		return head;
	}

	/**
	 * Effect the given type test by retyping the variable in question. The type
	 * test is made redundant at this point.
	 *
	 * @param typeTest
	 * @param state
	 * @param dependencies
	 * @return
	 */
	private State apply(Proof.Delta.Set existingTruths, Formula.Is typeTest, Proof.State state) throws ResolutionError {
		Expr lhs = typeTest.getTestExpr();
		Type lhsT = types.inferType(state.getTypeEnvironment(), lhs);
		Type rhsT = typeTest.getTestType();
		if (lhsT != null) {
			// NOTE #84: We must simplify here. Otherwise, it's possible that
			// using new Type.Intersection could potentially lead to unbounded
			// growth of the overall type.
			Type intersection = types.simplify(new Type.Intersection(new Type[]{lhsT, rhsT}));
			//
			if (types.isRawSubtype(new Type.Void(), intersection)) {
				// No possible intersection exists between the types in
				// question. Therefore, the test cannot be true.
				return state.subsume(this, typeTest, new Formula.Truth(false));
			} else {
				// At this point, it seems that the type test cannot be
				// eliminated. The next thing is to assert any type invariants
				// which now hold as a result of this test holding.
				Formula invariant = types.extractInvariant(intersection, lhs);
				// Assume extracted type invariant (if one exists)
				if (invariant != null) {
					state = state.infer(this, invariant, typeTest);
				}
				// In the case of a variable being retyped, we now need to go
				// through a properly effect that by retyping all truths which
				// use that variable. This may allow some of those truths to now
				// type themselves correctly.
				if (lhs instanceof Expr.VariableAccess) {
					state = retypeVariable(existingTruths, typeTest, intersection, state);
				} else {
					List<Formula.Is> matches = findMatches(existingTruths, typeTest, state);
					if (matches.size() > 1) {
						state = closeOver(matches, state);
					}
				}
			}
		}
		return state;
	}

	private Proof.State retypeVariable(Proof.Delta.Set existingTruths, Formula.Is typeTest, Type refinement,
			Proof.State state) throws ResolutionError {
		Expr.VariableAccess variable = (Expr.VariableAccess) typeTest.get(0);
		VariableDeclaration declaration = variable.getVariableDeclaration();
		TypeInferer.Environment environment = state.getTypeEnvironment();
		// Check whether or not the type has actually changed in some sense
		WyalFile.Type type = environment.getType(declaration);
		if (types.isRawSubtype(type, refinement) && !types.isRawSubtype(refinement, type)) {
			state = state.refine(this, declaration, refinement, typeTest);
		}
		//
		// FIXME: any formula which uses the given variable should be
		// reconsidered? For example, that fact may have been ignored thus far
		// because the type returned in a given situation was null.
		//
		return state;
	}

	/**
	 * Find the complete set of matching type tests. A type test is matching if
	 * it refers to the same left-hand side. For example, if we are matching
	 * <code>(x is int)</code> against <code>(y is int) && (x is !int)</code>,
	 * then this will return <code>x is !int</code>.
	 *
	 * @param lhs
	 * @param state
	 * @return
	 */
	private List<Formula.Is> findMatches(Proof.Delta.Set existingTruths, Formula.Is lhs, Proof.State state) {
		//
		List<Formula.Is> matches = new ArrayList<>();
		//
		for (int i = 0; i != existingTruths.size(); ++i) {
			Formula existing = existingTruths.get(i);
			if (existing != lhs && existing instanceof Formula.Is) {
				Formula.Is rhs = (Formula.Is) existing;
				if (lhs.getTestExpr().equals(rhs.getTestExpr())) {
					matches.add(rhs);
				}
			}
		}
		//
		return matches;
	}

	private State closeOver(List<Formula.Is> matches, Proof.State state) throws ResolutionError {
		Formula.Is first = matches.get(0);
		Type[] bounds = project(matches);
		// NOTE #84: We must simplify here. Otherwise, it's possible that
		// using new Type.Intersection could potentially lead to unbounded
		// growth of the overall type.
		Type type = types.simplify(new Type.Intersection(bounds));
		Formula test = new Formula.Is(first.getTestExpr(), type);
		//
		for (int i = 0; i != matches.size(); ++i) {
			state = state.subsume(this, matches.get(i), test);
		}
		//
		return state;
	}

	/**
	 * Extract the type from each matching type test.
	 *
	 * @param matches
	 * @return
	 */
	private Type[] project(List<Formula.Is> matches) {
		Type[] bounds = new Type[matches.size()];
		//
		for (int i = 0; i != matches.size(); ++i) {
			Formula.Is match = matches.get(i);
			bounds[i] = match.getTestType();
		}
		//
		return bounds;
	}
} public class TypeTestNormalisation extends AbstractClosureRule implements Proof.LinearRule {

	public TypeTestNormalisation(Simplification simplify,TypeSystem types) {
		super(simplify,types);
	}

	@Override
	public String getName() {
		return "Is-N";
	}

	@Override
	public State apply(Proof.Delta.Set existingTruths, Proof.State head, Formula newTruth) throws ResolutionError {
		if (newTruth instanceof Formula.Is) {
			Formula.Is test = (Formula.Is) newTruth;
			// Attempt to normalise this type test by expanding record accesses.
			Formula.Is normalisedTest = normalise(test);
			// Check whether or not we managed to expand it.
			if (normalisedTest != test) {
				// Yes, we succeeded in normalising this test ... therefore, we
				// subsume the original test and replace it with the
				// generalisation.
				head = head.subsume(this, test, normalisedTest);
			}
		}
		return head;
	}

	/**
	 * Normalise a given type test of the form <code>p.x is T</code> to
	 * <code>p is {T x, ...}</code>.
	 *
	 * @param test
	 *            The test to be normalised
	 * @return
	 * @throws ResolutionError
	 */
	private Formula.Is normalise(Formula.Is test) throws ResolutionError {
		Expr lhs = test.getTestExpr();
		if (lhs instanceof Expr.RecordAccess) {
			Expr.RecordAccess ra = (Expr.RecordAccess) lhs;
			Type type = test.getTestType();
			// Type lhsT = types.inferType(state.getTypeEnvironment(), lhs);
			// if(lhsT instanceof Type.Record) {
			// Type.Record rec = (Type.Record) lhsT;
			// // FIXME: could potentially perform an extraction here.
			// FieldDeclaration[] fields = rec.getFields();
			// FieldDeclaration[] nFields = Arrays.copyOf(fields,fields.length);
			//
			// }
			FieldDeclaration[] fields = new FieldDeclaration[1];
			fields[0] = new FieldDeclaration(type, ra.getField());
			return normalise(new Formula.Is(ra.getSource(), new Type.Record(true, fields)));
		} else {
			return test;
		}
	}
} public class DeltaProof extends AbstractProof<DeltaProof.State> {

	public DeltaProof(Assert assertion, SyntacticHeap heap, Formula axiom) {
		super(assertion,heap);
		// Initialise the proof with the root state
		states.add(new State(this, axiom));
	}

	public static class State extends AbstractState<State> {
		/**
		 * The set of all known truths, including those which are subsumed.
		 * Always a superset of activeTruths.
		 */
		private final BitSet truths;

		private final Delta delta;

		private final TypeInferer.Environment environment;

		public State(DeltaProof proof, Formula axiom) {
			super(proof, null, null);
			this.truths = new BitSet();
			this.delta = new FastDelta(new FastDelta.Set(axiom), FastDelta.EMPTY_SET);
			this.environment = new StdTypeEnvironment();
			truths.set(axiom.getIndex());
		}

		private State(State state, Proof.Rule rule, FastDelta delta, Formula... dependencies) {
			super((DeltaProof) state.getProof(), state, rule, dependencies);
			this.truths = (BitSet) state.truths.clone();
			this.environment = state.getTypeEnvironment();
			this.delta = delta;
			state.children.add(this);
			// Update our state of the world
			FastDelta.Set additions = delta.getAdditions();
			//
			for (int i = 0; i != additions.size(); ++i) {
				truths.set(additions.get(i).getIndex());
			}
		}

		private State(State state, TypeInferer.Environment environment,  Proof.Rule rule, Formula... dependencies) {
			super((DeltaProof) state.getProof(), state, rule, dependencies);
			this.truths = (BitSet) state.truths.clone();
			this.environment = environment;
			this.delta = FastDelta.EMPTY_DELTA;
			state.children.add(this);
		}

		/**
		 * Return the list of formulae introduced by this step.
		 *
		 * @return
		 */
		@Override
		public Delta getDelta() {
			return delta;
		}

		/**
		 * Return the list of formulae introduced by this step.
		 *
		 * @return
		 */
		@Override
		public Proof.Delta getDelta(Proof.State ancestor) {
			if(this == ancestor) {
				return FastDelta.EMPTY_DELTA;
			} else if(parent == null) {
				// At this point, we must be the root node. In which case, we
				// just return what we have.
				return delta;
			} else {
				return parent.getDelta(ancestor).apply(delta);
			}
		}

		/**
		 * Determine whether a given truth is known or not.
		 *
		 * @param truth
		 * @return
		 */
		@Override
		public boolean isKnown(Formula truth) {
			return truths.get(truth.getIndex());
		}

		@Override
		public Environment getTypeEnvironment() {
			return environment;
		}

		/**
		 * Subume one formula with one or more formulae. This implication is
		 * that latter "cover" the former. The former is no longer active,
		 * though it remains a known truth. The new formula are active.
		 *
		 * @param from
		 * @param to
		 */
		@Override
		public State subsume(Proof.Rule rule, Formula from, Formula to, Formula... deps) {
			FastDelta.Set removals = FastDelta.EMPTY_SET.add(from);
			FastDelta.Set additions = FastDelta.EMPTY_SET;
			// Check whether target already known
			to = allocate(to);
			final int toIndex = to.getIndex();
			if (!truths.get(toIndex)) {
				additions = additions.add(to);
			}
			FastDelta nDelta = new FastDelta(additions, removals);
			// Register this state
			return proof.register(new State(this, rule, nDelta, ArrayUtils.append(from, deps)));
		}

		@Override
		public State infer(Proof.Rule rule, Formula truth, Formula... dependencies) {
			//
			truth = allocate(truth);
			final int index = truth.getIndex();
			if(!truths.get(index)) {
				FastDelta delta = new FastDelta(new FastDelta.Set(truth), FastDelta.EMPTY_SET);
				return proof.register(new State(this,rule,delta,dependencies));
			} else {
				return this;
			}
		}

		@Override
		public State[] split(Formula.Disjunct disjunct) {
			Formula[] cases = disjunct.getAll();
			State[] result = new State[cases.length];
			for (int i = 0; i != cases.length; ++i) {
				result[i] = this.subsume(null,disjunct,cases[i]);
			}
			return result;
		}

		@Override
		public wytp.proof.Proof.State refine(Rule rule, VariableDeclaration variable, Type type,
				Formula... dependencies) {
			Type old = environment.getType(variable);
			if(old.equals(type)) {
				// nothing has changed.
				return this;
			} else {
				TypeInferer.Environment env = environment.refineType(variable, type);
				return proof.register(new State(this,env,rule,dependencies));
			}
		}

		@Override
		public Formula allocate(Formula truth) {
			return proof.getHeap().allocate(truth);
		}
	}
} public class Formulae {

	// ========================================================================
	// Conversions
	// ========================================================================

	/**
	 * <p>
	 * Take a tree of statements and expressions, and return a formula. This is
	 * the first part of the process in discharging a given assertion. The
	 * purpose of a formula is just to provide a more "structured" form of the
	 * logical expression. The interface Formula also provides useful functions
	 * form manipulating formulae.
	 * </p>
	 * <p>
	 * Observe that after this conversion the resulting formula is not
	 * necessarily in simplified form. For example, conjuncts may contain nested
	 * conjuncts or equations may be unbalanced.
	 * </p>
	 *
	 * @param stmt
	 *            The statement being converted into a formula
	 * @param types
	 *            The type system is required for the translation, as some
	 *            aspects depend upon the types of expressions involved.
	 * @return
	 * @throws AmbiguousNameError
	 * @throws NameNotFoundError
	 */
	public static Formula toFormula(WyalFile.Stmt stmt, TypeSystem types) throws ResolutionError {
		switch (stmt.getOpcode()) {
		case WyalFile.STMT_block: {
			WyalFile.Stmt.Block b = (WyalFile.Stmt.Block) stmt;
			Formula[] operands = toFormulae(b.getAll(), types);
			return new Formula.Conjunct(operands);
		}
		case WyalFile.STMT_caseof: {
			WyalFile.Stmt.CaseOf b = (WyalFile.Stmt.CaseOf) stmt;
			Formula[] operands = toFormulae(b.getAll(), types);
			return new Formula.Disjunct(operands);
		}
		case WyalFile.STMT_ifthen: {
			WyalFile.Stmt.IfThen it = (WyalFile.Stmt.IfThen) stmt;
			Formula lhs = toFormula(it.getIfBody(), types);
			Formula rhs = toFormula(it.getThenBody(), types);
			return new Formula.Disjunct(invert(lhs), rhs);
		}
		case WyalFile.STMT_forall: {
			Stmt.Quantifier q = (WyalFile.Stmt.Quantifier) stmt;
			// Convert body of quantifier
			Formula body = toFormula(q.getBody(), types);
			// Done
			return new Formula.Quantifier(true, q.getParameters(), body);
		}
		case WyalFile.STMT_exists: {
			Stmt.Quantifier q = (WyalFile.Stmt.Quantifier) stmt;
			// Convert body of quantifier
			Formula body = toFormula(q.getBody(), types);
			// Done
			return new Formula.Quantifier(false, q.getParameters(), body);
		}
		case WyalFile.EXPR_forall: {
			Expr.Quantifier q = (WyalFile.Expr.Quantifier) stmt;
			// Convert body of quantifier
			Formula body = toFormula(q.getBody(), types);
			// Done
			return new Formula.Quantifier(true, q.getParameters(), body);
		}
		case WyalFile.EXPR_exists: {
			Expr.Quantifier q = (WyalFile.Expr.Quantifier) stmt;
			// Convert body of quantifier
			Formula body = toFormula(q.getBody(), types);
			// Done
			return new Formula.Quantifier(false, q.getParameters(), body);
		}
		case WyalFile.EXPR_and: {
			Expr.Operator b = (Expr.Operator) stmt;
			Formula[] operands = toFormulae(b.getAll(), types);
			return new Formula.Conjunct(operands);
		}
		case WyalFile.EXPR_or: {
			Expr.Operator b = (Expr.Operator) stmt;
			Formula[] operands = toFormulae(b.getAll(), types);
			return new Formula.Disjunct(operands);
		}
		case WyalFile.EXPR_implies: {
			WyalFile.Expr.Operator it = (Expr.Operator) stmt;
			Formula lhs = toFormula(it.get(0), types);
			Formula rhs = toFormula(it.get(1), types);
			return new Formula.Disjunct(invert(lhs), rhs);
		}
		case WyalFile.EXPR_iff: {
			WyalFile.Expr.Operator it = (Expr.Operator) stmt;
			Formula lhs = toFormula(it.get(0), types);
			Formula rhs = toFormula(it.get(1), types);
			Formula a1 = new Formula.Conjunct(lhs,rhs);
			Formula a2 = new Formula.Conjunct(invert(lhs),invert(rhs));
			return new Formula.Disjunct(a1, a2);
		}
		case WyalFile.EXPR_eq: {
			Expr.Operator operator = (Expr.Operator) stmt;
			Expr lhs = operator.get(0);
			Expr rhs = operator.get(1);
			Type lhs_t = types.inferType(new StdTypeEnvironment(),lhs);
			Type rhs_t = types.inferType(new StdTypeEnvironment(),rhs);
			if (types.isRawSubtype(new Type.Int(), lhs_t) && types.isRawSubtype(new Type.Int(), rhs_t)) {
				// Force arithmetic equality
				return new Formula.ArithmeticEquality(true, lhs, rhs);
			} else {
				return new Formula.Equality(true, lhs, rhs);
			}
		}
		case WyalFile.EXPR_neq: {
			Expr.Operator operator = (Expr.Operator) stmt;
			Expr lhs = operator.get(0);
			Expr rhs = operator.get(1);
			Type lhs_t = types.inferType(new StdTypeEnvironment(),lhs);
			Type rhs_t = types.inferType(new StdTypeEnvironment(),rhs);
			if (types.isRawSubtype(new Type.Int(), lhs_t) && types.isRawSubtype(new Type.Int(), rhs_t)) {
				// Force arithmetic equality
				return new Formula.ArithmeticEquality(false, lhs, rhs);
			} else {
				return new Formula.Equality(false, lhs, rhs);
			}
		}
		case WyalFile.EXPR_lt: {
			Expr.Operator operator = (Expr.Operator) stmt;
			Expr lhs = operator.get(0);
			Expr rhs = operator.get(1);
			return lessThan(lhs,rhs);
		}
		case WyalFile.EXPR_lteq: {
			Expr.Operator operator = (Expr.Operator) stmt;
			Expr lhs = operator.get(0);
			Expr rhs = operator.get(1);
			return greaterOrEqual(rhs,lhs);
		}
		case WyalFile.EXPR_gt: {
			Expr.Operator operator = (Expr.Operator) stmt;
			Expr lhs = operator.get(0);
			Expr rhs = operator.get(1);
			// lhs > rhs ==> lhs+1 >= rhs
			return lessThan(rhs,lhs);
		}
		case WyalFile.EXPR_gteq: {
			Expr.Operator operator = (Expr.Operator) stmt;
			Expr lhs = operator.get(0);
			Expr rhs = operator.get(1);
			return greaterOrEqual(lhs,rhs);
		}
		case WyalFile.EXPR_not: {
			Expr.Operator operator = (Expr.Operator) stmt;
			Formula f = toFormula(operator.get(0), types);
			return invert(f);
		}
		case WyalFile.EXPR_const: {
			Expr.Constant c = (Expr.Constant) stmt;
			Value.Bool b = (Value.Bool) c.getValue();
			return new Formula.Truth(b);
		}
		case WyalFile.EXPR_invoke: {
			Expr.Invoke ivk = (Expr.Invoke) stmt;
			if(ivk.getSignatureType() instanceof Type.Function) {
				Expr TRUE = new Formula.Truth(new Value.Bool(true));
				return new Formula.Equality(true, ivk, TRUE);
			} else {
				return new Formula.Invoke(true, ivk.getSignatureType(), ivk.getName(), ivk.getSelector(), ivk.getArguments());
			}
		}
		case WyalFile.EXPR_is: {
			Expr.Is operator = (Expr.Is) stmt;
			Expr lhs = operator.getTestExpr();
			Type lhs_t = types.inferType(new StdTypeEnvironment(),lhs);
			if(lhs_t != null && types.isRawSubtype(new Type.Bool(), lhs_t)) {
				lhs = toFormula(lhs,types);
			}
			return new Formula.Is(lhs,operator.getTestType());
		}
		default:
			if (stmt instanceof WyalFile.Expr) {
				Expr expr = (WyalFile.Expr) stmt;
				Expr TRUE = new Formula.Truth(new Value.Bool(true));
				return new Formula.Equality(true, expr, TRUE);
			} else {
				throw new IllegalArgumentException("unknown statement encountered: " + stmt.getOpcode());
			}
		}
	}

	/**
	 * Convert an array of statements into an array of (equivalent) formulae.
	 *
	 * @param stmts
	 * @return
	 * @throws AmbiguousNameError
	 * @throws NameNotFoundError
	 */
	public static Formula[] toFormulae(Stmt[] stmts, TypeSystem types) throws ResolutionError {
		Formula[] exprs = new Formula[stmts.length];
		for (int i = 0; i != exprs.length; ++i) {
			exprs[i] = toFormula(stmts[i], types);
		}
		return exprs;
	}

	public static Formula.Inequality lessThan(Expr lhs, Expr rhs) {
		// lhs < rhs ===> rhs >= (lhs+1)
		Expr one = new Expr.Constant(new Value.Int(1));
		Expr lhsP1 = new Expr.Addition(lhs, one);
		return new Formula.Inequality(rhs, lhsP1);
	}

	public static Formula.Inequality greaterOrEqual(Expr lhs, Expr rhs) {
		return new Formula.Inequality(lhs, rhs);
	}

	public static Formula implies(Formula lhs, Formula rhs) {
		return new Formula.Disjunct(invert(lhs),rhs);
	}

	public static Formula and(Formula lhs, Formula rhs) {
		return new Formula.Conjunct(lhs,rhs);
	}

	public static Formula or(Formula lhs, Formula rhs) {
		return new Formula.Disjunct(lhs,rhs);
	}

	// ========================================================================
	// Inversion
	// ========================================================================

	/**
	 * Logically invert a given formula. This pushes through all inversions as
	 * far as possible. For example, <code>!(x == 0 && y < x)</code> becomes
	 * <code>x != 0 || y >= x</code>. This method is useful (amongst other
	 * things) for beginning a proof-by-contradiction. In such a proof, we first
	 * invert the formula in question and then establish that this reduces to a
	 * contradiction.
	 *
	 * @param f
	 * @return
	 */
	public static Formula invert(Formula f) {
		switch (f.getOpcode()) {
		case WyalFile.EXPR_const: {
			Formula.Truth truth = (Formula.Truth) f;
			return new Formula.Truth(!truth.holds());
		}
		case WyalFile.EXPR_and: {
			Formula.Conjunct c = (Formula.Conjunct) f;
			return new Disjunct(invert(c.getAll()));
		}
		case WyalFile.EXPR_or: {
			Formula.Disjunct c = (Formula.Disjunct) f;
			return new Conjunct(invert(c.getAll()));
		}
		case WyalFile.EXPR_exists:
		case WyalFile.EXPR_forall: {
			Formula.Quantifier q = (Formula.Quantifier) f;
			// FIXME: it's perhaps a little strange that we invert the body
			// here?
			return new Formula.Quantifier(!q.getSign(), q.getParameters(), invert(q.getBody()));
		}
		case WyalFile.EXPR_eq:
		case WyalFile.EXPR_neq: {
			if (f instanceof ArithmeticEquality) {
				ArithmeticEquality e = (ArithmeticEquality) f;
				return new ArithmeticEquality(!e.getSign(), e.get(0), e.get(1));
			} else {
				Equality e = (Equality) f;
				return new Equality(!e.getSign(), e.get(0), e.get(1));
			}
		}
		case WyalFile.EXPR_gteq: {
			// !(lhs >= rhs) => lhs < rhs
			Inequality e = (Inequality) f;
			Expr lhs = e.get(0);
			Expr rhs = e.get(1);
			return lessThan(lhs,rhs);
		}
		case WyalFile.EXPR_invoke: {
			Invoke e = (Invoke) f;
			return new Formula.Invoke(!e.getSign(),e.getSignatureType(),e.getName(),e.getSelector(),e.getArguments());
		}
		case WyalFile.EXPR_is: {
			Formula.Is c = (Formula.Is) f;
			// FIXME: could simplify the type here I think
			return new Is(c.getTestExpr(), new Type.Negation(c.getTestType()));
		}
		default:
			throw new IllegalArgumentException("invalid formula opcode: " + f.getOpcode());
		}
	}

	private static Formula[] invert(Formula[] children) {
		Formula[] nChildren = new Formula[children.length];
		for (int i = 0; i != children.length; ++i) {
			nChildren[i] = invert(children[i]);
		}
		return nChildren;
	}
	// ========================================================================
	// Simplifications
	// ========================================================================

} public class TypeSystem {
	/**
	 * The "null" environment provides a simple environment which simply falls
	 * back to using the declared type for a given variable.
	 */
	public  final static TypeInferer.Environment NULL_ENVIRONMENT = new StdTypeEnvironment();
	//
	private final NameResolver resolver;
	private final SubtypeOperator coerciveSubtypeOperator;
	private final TypeExtractor<Type.Record,Object> readableRecordExtractor;
	private final TypeExtractor<Type.Array,Object> readableArrayExtractor;
	private final TypeExtractor<Type.Reference,Object> readableReferenceExtractor;
	private final TypeInvariantExtractor typeInvariantExtractor;
	private final TypeInferer typeInfererence;
	private final TypeRewriter typeSimplifier;

	public TypeSystem(Build.Project project) {
		this.resolver = new WyalFileResolver(project);
		this.coerciveSubtypeOperator = new CoerciveSubtypeOperator(resolver);
		this.readableRecordExtractor = new ReadableRecordExtractor(resolver,this);
		this.readableArrayExtractor = new ReadableArrayExtractor(resolver,this);
		this.readableReferenceExtractor = new ReadableReferenceExtractor(resolver,this);
		this.typeInvariantExtractor = new TypeInvariantExtractor(resolver);
		this.typeInfererence = new StdTypeInfererence(this);
		this.typeSimplifier = new StdTypeRewriter();
	}

	/**
	 * <p>
	 * Determine whether one type is a <i>raw subtype</i> of another.
	 * Specifically, whether the raw type of <code>rhs</code> is a subtype of
	 * <code>lhs</code>'s raw type (i.e.
	 * "<code>&lfloor;lhs&rfloor; :> &lfloor;rhs&rfloor;</code>"). The raw type
	 * is that which ignores any type invariants involved. Thus, one must be
	 * careful when interpreting the meaning of this operation. Specifically,
	 * "<code>&lfloor;lhs&rfloor; :> &lfloor;rhs&rfloor;</code>" <b>does not
	 * imply</b> that "<code>lhs :> rhs</code>" holds. However, if
	 * "<code>&lfloor;lhs&rfloor; :> &lfloor;rhs&rfloor;</code>" does not hold,
	 * then it <b>does follow</b> that "<code>lhs :> rhs</code>" also does not
	 * hold.
	 * </p>
	 *
	 * <p>
	 * Depending on the exact language of types involved, this can be a
	 * surprisingly complex operation. For example, in the presence of
	 * <i>union</i>, <i>intersection</i> and <i>negation</i> types, the subtype
	 * algorithm is surprisingly intricate.
	 * </p>
	 *
	 * @param lhs
	 *            The candidate "supertype". That is, lhs's raw type may be a
	 *            supertype of <code>rhs</code>'s raw type.
	 * @param rhs
	 *            The candidate "subtype". That is, rhs's raw type may be a
	 *            subtype of <code>lhs</code>'s raw type.
	 * @return
	 * @throws ResolutionError
	 *             Occurs when a nominal type is encountered whose name cannot
	 *             be resolved properly. For example, it resolves to more than
	 *             one possible matching declaration, or it cannot be resolved
	 *             to a corresponding type declaration.
	 */
	public boolean isRawSubtype(Type lhs, Type rhs) throws ResolutionError {
		return coerciveSubtypeOperator.isSubtype(lhs,rhs) != SubtypeOperator.Result.False;
	}

	/**
	 * For a given type, extract its effective record type. For example, the
	 * type <code>({int x, int y}|{int x, int z})</code> has effective record
	 * type <code>{int x, ...}</code>. The following illustrates some more
	 * cases:
	 *
	 * <pre>
	 * {int x, int y} | null    ==> null
	 * {int x, int y} | {int x} ==> null
	 * {int x, int y} | {int x, bool y} ==> {int x, int|bool y}
	 * {int x, int y} & null    ==> null
	 * {int x, int y} & {int x} ==> null
	 * {int x, int y} & {int x, int|bool y} ==> {int x, int y}
	 * </pre>
	 *
	 * @param type
	 * @return
	 * @throws ResolutionError
	 */
	public Type.Record extractReadableRecord(Type type) throws ResolutionError {
		return readableRecordExtractor.extract(type,null);
	}

	/**
	 * Extract the readable array type from a given type. For example, the type
	 * <code>(int[])|(bool[])</code> has a readable array type of
	 * <code>(int|bool)[]</code>.
	 *
	 * @param type
	 * @return
	 * @throws ResolutionError
	 */
	public Type.Array extractReadableArray(Type type) throws ResolutionError {
		return readableArrayExtractor.extract(type,null);
	}

	/**
	 * Extract the readable reference type from a given type. This is relatively
	 * straightforward. For example, <code>&int</code> is extracted as
	 * <code>&int</code>. However, <code>(&int)|(&bool)</code> is not extracted
	 * as as <code>&(int|bool)</code>.
	 *
	 * @param type
	 * @return
	 * @throws ResolutionError
	 */
	public Type.Reference extractReadableReference(Type type) throws ResolutionError {
		return readableReferenceExtractor.extract(type,null);
	}

	/**
	 * Extracting the invariant (if any) from a given type. For example,
	 * consider the following type declaration:
	 *
	 * <pre>
	 * type nat is (int x) where x >= 0
	 * </pre>
	 *
	 * Then, extracting the invariant from type <code>nat</code> gives
	 * <code>x >= 0</code>. Likewise, extracting the invariant from the type
	 * <code>bool|int</code> gives the invariant
	 * <code>(x is int) ==> (x >= 0)</code>. Finally, extracting the invariant
	 * from the type <code>nat[]</code> gives the invariant
	 * <code>forall(int i).(0 <= i
	 * && i < |xs| ==> xs[i] >= 0)</code>.
	 *
	 *
	 */
	public Formula extractInvariant(Type type, Expr root) throws ResolutionError {
		return typeInvariantExtractor.extract(type,root);
	}

	// ========================================================================
	// Inference
	// ========================================================================

	/**
	 * Get the type inferred for a given expression in a given environment.
	 *
	 * @param environment
	 * @param expression
	 * @return
	 * @throws ResolutionError
	 *             Occurs when a particular named type cannot be resolved.
	 */
	public Type inferType(TypeInferer.Environment environment, Expr expression) throws ResolutionError {
		return typeInfererence.getInferredType(environment, expression);
	}

	// ========================================================================
	// Resolution
	// ========================================================================

	public <T extends Declaration.Named> T resolveExactly(Name name, Class<T> kind)
			throws ResolutionError {
		return resolver.resolveExactly(name,kind);
	}

	public <T extends Declaration.Named> List<T> resolveAll(Name name, Class<T> kind)
			throws ResolutionError {
		return resolver.resolveAll(name,kind);
	}

	// ========================================================================
	// Simplification
	// ========================================================================

	public Type simplify(Type type) {
		return typeSimplifier.rewrite(type);
	}
}
import java.util.BitSet;
import wyal.heap.StructurallyEquivalentHeap;
import wyal.lang.WyalFile;
import wyal.util.NameResolver;
import wyal.util.NameResolver.AmbiguousNameError;
import wyal.util.NameResolver.NameNotFoundError;
import wyal.util.NameResolver.ResolutionError;
import wybs.lang.SyntacticException;
import wybs.lang.SyntacticHeap;
import wybs.lang.SyntacticItem;
import wytp.proof.Formula;
import wytp.proof.Proof;
import wytp.proof.io.ProofPrinter;
import wytp.proof.rules.CongruenceClosure;
import wytp.proof.rules.EqualityCaseAnalysis;
import wytp.proof.rules.Simplification;
import wytp.proof.rules.arithmetic.InequalityIntroduction;
import wytp.proof.rules.array.ArrayEqualityCaseAnalysis;
import wytp.proof.rules.array.ArrayIndexAxiom;
import wytp.proof.rules.array.ArrayIndexCaseAnalysis;
import wytp.proof.rules.array.ArrayLengthAxiom;
import wytp.proof.rules.function.FunctionCallAxiom;
import wytp.proof.rules.function.MacroExpansion;
import wytp.proof.rules.logic.AndElimination;
import wytp.proof.rules.logic.OrElimination;
import wytp.proof.rules.quantifier.ExhaustiveQuantifierInstantiation;
import wytp.proof.rules.quantifier.ExistentialElimination;
import wytp.proof.rules.record.RecordEqualityCaseAnalysis;
import wytp.proof.rules.type.TypeTestClosure;
import wytp.proof.rules.type.TypeTestNormalisation;
import wytp.proof.util.DeltaProof;
import wytp.proof.util.Formulae;
import wytp.types.TypeSystem;
// Copyright 2011 The Whiley Project Developers
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//    http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
package wytp.provers;



public class AutomatedTheoremProver {

	/**
	 * The type system encapsulates the core algorithms for type simplification
	 * and subtyping testing.
	 */
	private final TypeSystem types;

	/**
	 * Determines the maximum size of a proof.
	 */
	private int maxProofSize = 5000;

	/**
	 * Debugging option which prints the proof to the console. This should
	 * eventually be deprecated in favour of a more formal mechanism for
	 * extracting and examining the proof.
	 */
	private boolean printProof = false;

	/**
	 * Set the width for displaying proofs
	 */
	private int proofWidth = 80;

	/**
	 * The list of proof rules which can be applied by this theorem prover.
	 */
	private Proof.Rule[] rules;

	public void setPrintProof(boolean flag) {
		this.printProof = flag;
	}

	public void setProofLimit(int size) {
		this.maxProofSize = size;
	}

	public void setProofWidth(int width) {
		this.proofWidth= width;
	}

	public AutomatedTheoremProver(TypeSystem typeSystem) {
		this.types = typeSystem;
		//
		Simplification simplify = new Simplification(types);
		//
		this.rules = new Proof.Rule[] {
				simplify,
				new CongruenceClosure(simplify,types),
				new InequalityIntroduction(simplify,types),
				new AndElimination(simplify,types),
				new ExistentialElimination(simplify,types),
				new MacroExpansion(simplify,types),
				new TypeTestNormalisation(simplify,types),
				new TypeTestClosure(simplify,types),
				new ArrayLengthAxiom(simplify,types),
				new ArrayIndexAxiom(simplify,types),
				new ArrayIndexCaseAnalysis(simplify,types),
				new FunctionCallAxiom(simplify,types),
				new EqualityCaseAnalysis(simplify,types),
				new RecordEqualityCaseAnalysis(simplify,types),
				new ArrayEqualityCaseAnalysis(simplify,types),
				new OrElimination(),
				new ExhaustiveQuantifierInstantiation(simplify,types) };
	}

	public void check(WyalFile source) {
		for (int i = 0; i != source.size(); ++i) {
			SyntacticItem item = source.getSyntacticItem(i);
			if (item instanceof WyalFile.Declaration.Assert) {
				WyalFile.Declaration.Assert ast = (WyalFile.Declaration.Assert) item;
				try {
					if (!check(ast)) {
						String msg = ast.getMessage();
						msg = msg != null ? msg : "assertion failure";
						throw new SyntacticException(msg,null, ast);
					}
				} catch (NameResolver.ResolutionError e) {