//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework
{
    using System.Diagnostics.Contracts;
    using System.Collections;
  using System.Collections.Generic;
    //using Microsoft.SpecSharp.Collections;
	using Microsoft.Basetypes;

    /// <summary>
    ///  A basic class for function symbols.
    /// </summary>
    public class FunctionSymbol : IFunctionSymbol
    {
        private readonly string/*!*/ display;
        private readonly AIType/*!*/ typ;
      [ContractInvariantMethod]
void ObjectInvariant() 
{
    Contract.Invariant(display != null);
        Contract.Invariant(typ != null);
}


        public FunctionSymbol(AIType/*!*/ typ)
        : this("FunctionSymbol", typ)
        {
          Contract.Requires(typ != null);
        }

        internal FunctionSymbol(string/*!*/ display, AIType/*!*/ typ){
Contract.Requires(typ != null);
Contract.Requires(display != null);
            this.display = display;
            this.typ = typ;
            //            base();
        }

        public AIType/*!*/ AIType { get {Contract.Ensures(Contract.Result<AIType>() != null); return typ; } }

        [NoDefaultContract]
        [Pure]
        public override string/*!*/ ToString() {
Contract.Ensures(Contract.Result<string>() != null);
            return display;
        }

    }
    
    /// <summary>
    ///  A class for integer constants.
    /// </summary>
    public class IntSymbol : FunctionSymbol
    {
        public readonly BigNum Value;
        
        /// <summary>
        /// The intention is that this constructor be called only from the Int.Const method.
        /// </summary>
        internal IntSymbol(BigNum x)
        : base(cce.NonNull(x.ToString()), Int.Type)
        {
            this.Value = x;
        }

        [Pure][Reads(ReadsAttribute.Reads.Nothing)]
        public override bool Equals(object other)
        {
            IntSymbol isym = other as IntSymbol;
            return isym != null && isym.Value.Equals(this.Value);
        }
        
        [Pure]
        public override int GetHashCode()
        {
            return Value.GetHashCode();
        }
    }

    /// <summary>
    ///  A class for bitvector constants.
    /// </summary>
    public class BvSymbol : FunctionSymbol
    {
        public readonly BigNum Value;
        public readonly int Bits;
        
        /// <summary>
        /// The intention is that this constructor be called only from the Int.Const method.
        /// </summary>
        internal BvSymbol(BigNum x, int y)
        : base(x + "bv" + y, Bv.Type)
        {
            this.Value = x;
            this.Bits = y;
        }

        [Pure][Reads(ReadsAttribute.Reads.Nothing)]
        public override bool Equals(object other)
        {
            BvSymbol isym = other as BvSymbol;
            return isym != null && isym.Value == this.Value && isym.Bits == this.Bits;
        }
        
        [Pure]
        public override int GetHashCode()
        {
            unchecked {
              return Value.GetHashCode() ^ Bits;
            }
        }
    }

    public class DoubleSymbol : FunctionSymbol
    {
        public readonly double Value;
        
        /// <summary>
        /// The intention is that this constructor be called only from the Double.Const method.
        /// </summary>
        internal DoubleSymbol(double x)
        : base(cce.NonNull(x.ToString()), Double.Type)
        {
            this.Value = x;
        }
        
        [Pure][Reads(ReadsAttribute.Reads.Nothing)]
        public override bool Equals(object other)
        {
            DoubleSymbol dsym = other as DoubleSymbol;
            return dsym != null && dsym.Value == this.Value;
        }

        [Pure]
        public override int GetHashCode()
        {
            return Value.GetHashCode();
        }
    }

    /// <summary>
    ///  Function symbol based on a string.  Uses the string equality for determining equality
    ///  of symbol.
    /// </summary>
    public class NamedSymbol : FunctionSymbol
    {
        public string/*!*/ Value { [NoDefaultContract] get {Contract.Ensures(Contract.Result<string>() != null); return cce.NonNull(this.ToString()); } }

        public NamedSymbol(string/*!*/ symbol, AIType/*!*/ typ)
        : base(symbol, typ){
Contract.Requires(typ != null);
Contract.Requires(symbol != null);
        }

        [NoDefaultContract]
        [Pure][Reads(ReadsAttribute.Reads.Nothing)]
        public override bool Equals(object other)
        {
            NamedSymbol nsym = other as NamedSymbol;
            return nsym != null && this.Value.Equals(nsym.Value);
        }

        [NoDefaultContract]
        [Pure]
        public override int GetHashCode()
        {
            return Value.GetHashCode();
        }
    }

    //
    // In the following, the classes like Value and Prop serve two
    // roles.  The primary role is to be the base types for AIType. 
    // The only objects of these classes are the representative
    // objects that denote an AIType, which are given by the
    // "Type" property.  Subtypes in the AIType language are
    // encoded by subclassing.  This yields some "higher-orderness"
    // for checking subtyping in the AIType language, by using
    // the Spec#/C# subclassing checks.
    //
    // The other role is simply as a module for collecting like function
    // symbols.
    //

    //-------------------------- Terms ----------------------------------

    /// <summary>
    ///  A class with the equality symbol and the ValueType.Type.
    /// </summary>
    public class Value : AIType
    {
        private static readonly AIType/*!*/ valtype = new Value();
        public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return valtype; } }

        private static readonly FunctionType[]/*!*/ funtypeCache = new FunctionType[5];
        public static FunctionType/*!*/ FunctionType(int inParameterCount) {
Contract.Requires((0 <= inParameterCount));
Contract.Ensures(Contract.Result<FunctionType>() != null);
          // Contract.Ensures(Contract.Result<>().Arity == inParameterCount);
            FunctionType result;
            if (inParameterCount < funtypeCache.Length) {
                result = funtypeCache[inParameterCount];
                if (result != null) {
                    return result;
                }
            }
            AIType[] signature = new AIType[1 + inParameterCount];
            for (int i = 0; i < signature.Length; i++) {
                signature[i] = valtype;
            }
            result = new FunctionType(signature);
            if (inParameterCount < funtypeCache.Length) {
                funtypeCache[inParameterCount] = result;
            }
            return result;
        }

        [Once] private static AIType/*!*/ binreltype;
      [ContractInvariantMethod]
void ObjectInvariant() 
{
    Contract.Invariant(binreltype != null);
        Contract.Invariant(_eq != null);
        Contract.Invariant(_neq != null);
        Contract.Invariant(_subtype != null);
        Contract.Invariant(_typeof != null);
}

        private static AIType/*!*/ BinrelType {
          get {Contract.Ensures(Contract.Result<AIType>() != null);
            if (binreltype == null) {
              binreltype = new FunctionType(Type, Type, Prop.Type);
            }
            return binreltype;
          }
        }

        [Once] private static FunctionSymbol/*!*/ _eq;
        public static FunctionSymbol/*!*/ Eq {
          get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
            if (_eq == null) {
              _eq = new FunctionSymbol("=", BinrelType);
            }
            return _eq;
          }
        }
        [Once] private static FunctionSymbol/*!*/ _neq;
        public static FunctionSymbol/*!*/ Neq {
          get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
            if (_neq == null) {
              _neq = new FunctionSymbol("!=", BinrelType);
            }
            return _neq;
          }
        }
        [Once] private static FunctionSymbol/*!*/ _subtype;
        public static FunctionSymbol/*!*/ Subtype {
          get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
            if (_subtype == null) {
              _subtype = new FunctionSymbol("<:", BinrelType);
            }
            return _subtype;
          }
        }

        [Once] private static AIType/*!*/ typeof_type;
        private static AIType/*!*/ TypeofType {
          get {Contract.Ensures(Contract.Result<AIType>() != null);
            if (typeof_type == null) {
              typeof_type = new FunctionType(Ref.Type, Type);
            }
            return typeof_type;
          }
        }
        [Once] private static FunctionSymbol/*!*/ _typeof;
        public static FunctionSymbol/*!*/ Typeof {
          get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
            if (_typeof == null) {
              _typeof = new FunctionSymbol("typeof", TypeofType);
            }
            return _typeof;
          }
        }

        /// <summary>
        /// Value should not be instantiated from the outside, except perhaps in
        /// subclasses.
        /// </summary>
        protected Value() { }
 
    }

    public class Int : Value
    {
        private static readonly AIType/*!*/ inttype = new Int();
        public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return inttype; } }
        
        private static readonly AIType/*!*/ unaryinttype = new FunctionType(Type, Type);
        private static readonly AIType/*!*/ bininttype = new FunctionType(Type, Type, Type);
        private static readonly AIType/*!*/ relationtype = new FunctionType(Type, Type, Prop.Type);

        private static readonly FunctionSymbol/*!*/ _negate = new FunctionSymbol("~", unaryinttype);
        private static readonly FunctionSymbol/*!*/ _add = new FunctionSymbol("+", bininttype);
        private static readonly FunctionSymbol/*!*/ _sub = new FunctionSymbol("-", bininttype);
        private static readonly FunctionSymbol/*!*/ _mul = new FunctionSymbol("*", bininttype);
        private static readonly FunctionSymbol/*!*/ _div = new FunctionSymbol("/", bininttype);
        private static readonly FunctionSymbol/*!*/ _mod = new FunctionSymbol("%", bininttype);
        private static readonly FunctionSymbol/*!*/ _atmost = new FunctionSymbol("<=", relationtype);
        private static readonly FunctionSymbol/*!*/ _less = new FunctionSymbol("<", relationtype);
        private static readonly FunctionSymbol/*!*/ _greater = new FunctionSymbol(">", relationtype);
        private static readonly FunctionSymbol/*!*/ _atleast = new FunctionSymbol(">=", relationtype);

        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Negate { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _negate; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Add { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _add; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Sub { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _sub; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Mul { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _mul; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Div { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _div; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Mod { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _mod; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ AtMost { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atmost; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Less { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _less; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Greater { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _greater; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ AtLeast { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atleast; } }

        public static IntSymbol/*!*/ Const(BigNum x) {
Contract.Ensures(Contract.Result<IntSymbol>() != null);
            // We could cache things here, but for now we don't.
            return new IntSymbol(x);
        }

        /// <summary>
        /// Int should not be instantiated from the outside, except perhaps in
        /// subclasses.
        /// </summary>
        private Int() { }
    }

    public class Double : Value
    {
        private static readonly AIType/*!*/ doubletype = new Double();
        public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return doubletype; } }
        
        public static DoubleSymbol/*!*/ Const(double x) {
Contract.Ensures(Contract.Result<DoubleSymbol>() != null);
            // We could cache things here, but for now we don't.
            return new DoubleSymbol(x);
        }

        /// <summary>
        /// Double should not be instantiated from the outside, except perhaps in
        /// subclasses.
        /// </summary>
        private Double() { }
    }

    public class Bv : Value
    {
        private static readonly AIType/*!*/ bvtype = new Bv();
        public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return bvtype; } }
        
        private static readonly AIType/*!*/ unaryinttype = new FunctionType(Type, Type);
        private static readonly AIType/*!*/ bininttype = new FunctionType(Type, Type, Type);
        private static readonly AIType/*!*/ relationtype = new FunctionType(Type, Type, Prop.Type);

        private static readonly FunctionSymbol/*!*/ _negate = new FunctionSymbol("~", unaryinttype);
        private static readonly FunctionSymbol/*!*/ _add = new FunctionSymbol("+", bininttype);
        private static readonly FunctionSymbol/*!*/ _sub = new FunctionSymbol("-", bininttype);
        private static readonly FunctionSymbol/*!*/ _mul = new FunctionSymbol("*", bininttype);
        private static readonly FunctionSymbol/*!*/ _div = new FunctionSymbol("/", bininttype);
        private static readonly FunctionSymbol/*!*/ _mod = new FunctionSymbol("%", bininttype);
        private static readonly FunctionSymbol/*!*/ _concat = new FunctionSymbol("$concat", bininttype);
        private static readonly FunctionSymbol/*!*/ _extract = new FunctionSymbol("$extract", unaryinttype);
        private static readonly FunctionSymbol/*!*/ _atmost = new FunctionSymbol("<=", relationtype);
        private static readonly FunctionSymbol/*!*/ _less = new FunctionSymbol("<", relationtype);
        private static readonly FunctionSymbol/*!*/ _greater = new FunctionSymbol(">", relationtype);
        private static readonly FunctionSymbol/*!*/ _atleast = new FunctionSymbol(">=", relationtype);

        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Negate { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _negate; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Add { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _add; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Sub { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _sub; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Mul { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _mul; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Div { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _div; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Mod { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null);return _mod; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ AtMost { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atmost; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Less { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _less; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Greater { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _greater; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ AtLeast { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atleast; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Extract { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _extract; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Concat { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _concat; } }

        public static BvSymbol/*!*/ Const(BigNum x, int y) {
Contract.Ensures(Contract.Result<BvSymbol>() != null);
            // We could cache things here, but for now we don't.
            return new BvSymbol(x, y);
        }

        /// <summary>
        /// Int should not be instantiated from the outside, except perhaps in
        /// subclasses.
        /// </summary>
        private Bv() { }
    }

    public class Ref : Value
    {
        private static readonly AIType/*!*/ reftype = new Ref();
        public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return reftype; } }

        private static readonly FunctionSymbol/*!*/ _null = new FunctionSymbol("null", Type);

        public static FunctionSymbol/*!*/ Null { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _null; } }

        /// <summary>
        /// Ref should not be instantiated from the outside, except perhaps in
        /// subclasses.
        /// </summary>
        private Ref() { }
    }

    public class HeapStructure : Value
    {
        private static readonly AIType/*!*/ reftype = new HeapStructure();
        public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return reftype; } }
        


        /// <summary>
        /// HeapStructure should not be instantiated from the outside, except perhaps in
        /// subclasses.
        /// </summary>
        private HeapStructure() { }
    }

    public class FieldName : Value
    {
        private static readonly AIType/*!*/ fieldnametype = new FieldName();
        public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return fieldnametype; } }

        private static readonly FunctionSymbol/*!*/ _allocated = new FunctionSymbol("$allocated", FieldName.Type);
        public static FunctionSymbol/*!*/ Allocated { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _allocated; } }

        /// <summary>
        /// Is this a boolean field that monotonically goes from false to true?
        /// </summary>
        public static bool IsBooleanMonotonicallyWeakening(IFunctionSymbol/*!*/ f){
Contract.Requires(f != null);
            return f.Equals(Allocated);
        }

        /// <summary>
        /// FieldName should not be instantiated from the outside, except perhaps in
        /// subclasses.
        /// </summary>
        private FieldName() { }
    }

    public class Heap : Value
    {
        private static readonly AIType/*!*/ heaptype = new Heap();
        public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return heaptype; } }

        // the types in the following, select1, select2, are hard-coded;
        // these types may not always be appropriate
        private static readonly FunctionSymbol/*!*/ _select1 = new FunctionSymbol("sel1",
            // Heap x FieldName -> Prop
            new FunctionType(Type, FieldName.Type, Prop.Type)
        );
        public static FunctionSymbol/*!*/ Select1 { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _select1; } }

        private static readonly FunctionSymbol/*!*/ _select2 = new FunctionSymbol("sel2",
            // Heap x Ref x FieldName -> Value
            new FunctionType(Type, Ref.Type, FieldName.Type, Value.Type)
        );
        public static FunctionSymbol/*!*/ Select2 { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _select2; } }

        // the types in the following, store1, store2, are hard-coded;
        // these types may not always be appropriate
        private static readonly FunctionSymbol/*!*/ _update1 = new FunctionSymbol("upd1",
            // Heap x FieldName x Value -> Heap
            new FunctionType(Type, FieldName.Type, Value.Type, Type)
        );
        public static FunctionSymbol/*!*/ Update1 { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _update1; } }

        private static readonly FunctionSymbol/*!*/ _update2 = new FunctionSymbol("upd2",
            // Heap x Ref x FieldName x Value -> Heap
            new FunctionType(Type, Ref.Type, FieldName.Type, Value.Type, Type)
        );
        public static FunctionSymbol/*!*/ Update2 { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _update2; } }

        private static readonly FunctionSymbol/*!*/ _unsupportedHeapOp =
            new FunctionSymbol("UnsupportedHeapOp",
            // Heap x FieldName -> Prop
            new FunctionType(Type, FieldName.Type, Prop.Type)
        );
        public static FunctionSymbol/*!*/ UnsupportedHeapOp { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _unsupportedHeapOp; } }

        /// <summary>
        /// Heap should not be instantiated from the outside, except perhaps in
        /// subclasses.
        /// </summary>
        private Heap() { }
    }

//    public class List : Value
//    {
//        private static IDictionary/*<AIType!,AIType!>*/! lists = new Hashtable();
//        public static AIType! Type(AIType! typeParameter)
//        {
//            if (lists.Contains(typeParameter))
//                return lists[typeParameter];
//            else
//            {
//                AIType! result = new List(typeParameter);
//                lists[typeParameter] = result;
//                return result;
//            }
//        }
//
//        private static IDictionary/*<AIType!,AIType!>*/! nils = new Hashtable();
//        public static FunctionSymbol! Nil(AIType! typeParameter)
//        {
//            if (nils.Contains(typeParameter))
//                return nils[typeParameter];
//            else
//            {
//                FunctionSymbol! result = new FunctionSymbol(Type(typeParameter));
//                nils[typeParameter] = result;
//                return result;
//            }
//        }
//
//        private static IDictionary/*<AIType!,AIType!>*/! cons = new Hashtable();
//        public static FunctionSymbol! Cons(AIType! typeParameter)
//        {
//            if (cons.Contains(typeParameter))
//                return cons[typeParameter];
//            else
//            {
//                FunctionSymbol! result = new FunctionSymbol(
//                    new FunctionType(typeParameter, Type(typeParameter), Type(typeParameter))
//                );
//                cons[typeParameter] = result;
//                return result;
//            }
//        }
//
//        private AIType! typeParameter;
//        public AIType(TypeParameter/*!*/ ){
//Contract.Requires( != null);
 //return typeParameter; } }
//
//        /// <summary>
//        /// List should not be instantiated from the outside.
//        /// </summary>
//        private List(AIType! typeParameter)
//        {
//            this.typeParameter = typeParameter;
//        }
//    }
//
//    public class Pair : Value
//    {
//        private static IDictionary! pairs = new Hashtable();
//        public static AIType! Type(AIType! type1, AIType! type2)
//        {
//            Microsoft.AbstractInterpretationFramework.Collections.Pair typpair
//                = new Microsoft.AbstractInterpretationFramework.Collections.Pair(type1, type2);
//
//            if (pairs.Contains(typpair))
//                return pairs[typpair];
//            else
//            {
//                AIType! result = new Pair(type1, type2);
//                pairs[typpair] = result;
//                return result;
//            }
//        }
//
//        private static IDictionary! constructs = new Hashtable();
//        public static FunctionSymbol! Pair(AIType! type1, AIType! type2)
//        {
//            Microsoft.AbstractInterpretationFramework.Collections.Pair typpair
//                = new Microsoft.AbstractInterpretationFramework.Collections.Pair(type1, type2);
//
//            if (constructs.Contains(typpair))
//                return constructs[typpair];
//            else
//            {
//                FunctionSymbol! result = new FunctionSymbol(
//                    new FunctionType(type1, type2, Type(type1, type2))
//                );
//                constructs[typpair] = result;
//                return result;
//            }
//        }
//
//        protected AIType! type1;
//        protected AIType! type2;
//
//        public AIType(Type1/*!*/ ){
//Contract.Requires( != null);
// return type1; } }
//        public AIType(Type2/*!*/ ){
//Contract.Requires( != null);
// return type2; } }
//
//        /// <summary>
//        /// Pair should not be instantiated from the outside, except by subclasses.
//        /// </summary>
//        protected Pair(AIType! type1, AIType! type2)
//        {
//            this.type1 = type1;
//            this.type2 = type2;
//        }
//    }

    //-------------------------- Propositions ---------------------------


    /// <summary>
    ///  A class with global propositional symbols and the Prop.Type.
    /// </summary>
    public sealed class Prop : AIType
    {
        private static readonly AIType/*!*/ proptype = new Prop();
      [ContractInvariantMethod]
void ObjectInvariant() 
{
    Contract.Invariant(proptype != null);
}

        public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return proptype; } }

        private static readonly AIType/*!*/ unaryproptype = new FunctionType(Type, Type);
        private static readonly AIType/*!*/ binproptype = new FunctionType(Type, Type, Type);
        private static readonly AIType/*!*/ quantifiertype =
            new FunctionType(new FunctionType(Value.Type, Type), Type);

        private static readonly FunctionSymbol/*!*/ _false = new FunctionSymbol("false", Type);
        private static readonly FunctionSymbol/*!*/ _true = new FunctionSymbol("true", Type);
        private static readonly FunctionSymbol/*!*/ _not = new FunctionSymbol("!", unaryproptype);
        private static readonly FunctionSymbol/*!*/ _and = new FunctionSymbol("/\\", binproptype);
        private static readonly FunctionSymbol/*!*/ _or = new FunctionSymbol("\\/", binproptype);
        private static readonly FunctionSymbol/*!*/ _implies = new FunctionSymbol("==>", binproptype);
        private static readonly FunctionSymbol/*!*/ _exists = new FunctionSymbol("Exists", quantifiertype);
        private static readonly FunctionSymbol/*!*/ _forall = new FunctionSymbol("Forall", quantifiertype);
        private static readonly FunctionSymbol/*!*/ _lambda = new FunctionSymbol("Lambda", quantifiertype);


        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ False { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _false; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ True { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _true; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Not { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _not; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ And { [Pure] get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _and; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Or { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _or; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Implies { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _implies; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Exists { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _exists; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Forall { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _forall; } }
        [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Lambda { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _lambda; } }


        /// <summary>
        ///  Prop should not be instantiated from the outside.
        /// </summary>
        private Prop() { }



        //
        // Utility Methods
        //
        
        public static IExpr/*!*/ SimplifiedAnd(IPropExprFactory/*!*/ factory, IExpr/*!*/ e0, IExpr/*!*/ e1){
Contract.Requires(e1 != null);
Contract.Requires(e0 != null);
Contract.Requires(factory != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
            IFunApp fun0 = e0 as IFunApp;
            if (fun0 != null)
            {
                if (fun0.FunctionSymbol.Equals(Prop.True))
                {
                    return e1;
                }
                else if (fun0.FunctionSymbol.Equals(Prop.False))
                {
                    return e0;
                }
            }
            
            IFunApp fun1 = e1 as IFunApp;
            if (fun1 != null)
            {
                if (fun1.FunctionSymbol.Equals(Prop.True))
                {
                    return e0;
                }
                else if (fun1.FunctionSymbol.Equals(Prop.False))
                {
                    return e1;
                }
            }
            
            return factory.And(e0, e1);
        }
        
        public static IExpr/*!*/ SimplifiedAnd(IPropExprFactory/*!*/ factory, IEnumerable/*<IExpr!>*//*!*/ exprs){
Contract.Requires(exprs != null);
Contract.Requires(factory != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
IExpr/*!*/ result = factory.True;
Contract.Assert(result != null);
            foreach(IExpr/*!*/ conjunct in exprs){
Contract.Assert(conjunct != null);
                result = SimplifiedAnd(factory, result, conjunct);
            }
            return result;
        }

        public static IExpr/*!*/ SimplifiedOr(IPropExprFactory/*!*/ factory, IExpr/*!*/ e0, IExpr/*!*/ e1){
Contract.Requires(e1 != null);
Contract.Requires(e0 != null);
Contract.Requires(factory != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
            IFunApp fun0 = e0 as IFunApp;
            if (fun0 != null)
            {
                if (fun0.FunctionSymbol.Equals(Prop.False))
                {
                    return e1;
                }
                else if (fun0.FunctionSymbol.Equals(Prop.True))
                {
                    return e0;
                }
            }
            
            IFunApp fun1 = e1 as IFunApp;
            if (fun1 != null)
            {
                if (fun1.FunctionSymbol.Equals(Prop.False))
                {
                    return e0;
                }
                else if (fun1.FunctionSymbol.Equals(Prop.True))
                {
                    return e1;
                }
            }
            
            return factory.Or(e0, e1);
        }
        
        public static IExpr/*!*/ SimplifiedOr(IPropExprFactory/*!*/ factory, IEnumerable/*<IExpr!>*//*!*/ exprs){
Contract.Requires(exprs != null);
Contract.Requires(factory != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
IExpr/*!*/ result = factory.False;
Contract.Assert(result != null);
            foreach(IExpr/*!*/ disj in exprs){
Contract.Assert(disj != null);
                result = SimplifiedOr(factory, result, disj);
            }
            return result;
        }



        /// <summary>
        ///  Break top-level conjuncts into a list of sub-expressions.
        /// </summary>
        /// <param name="e">The expression to examine.</param>
        /// <returns>A list of conjuncts.</returns>
        internal static IList/*<IExpr!>*//*!*/ BreakConjuncts(IExpr/*!*/ e){
Contract.Requires(e != null);
          Contract.Ensures(Contract.Result<IList>() != null);
          Contract.Ensures(Contract.ForAll(0, Contract.Result<IList>().Count, i => {
            var sub = Contract.Result<IList>()[i];
            return !(sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(Prop.And);
          }));
            return BreakJuncts(e, Prop.And);
        }

        /// <summary>
        ///  Break top-level disjuncts into a list of sub-expressions.
        /// </summary>
        /// <param name="e">The expression to examine.</param>
        /// <returns>A list of conjuncts.</returns>
        internal static IList/*<IExpr!>*//*!*/ BreakDisjuncts(IExpr/*!*/ e){
Contract.Requires(e != null);
          Contract.Ensures(Contract.Result<IList>() != null);
          Contract.Ensures(Contract.ForAll(0, Contract.Result<IList>().Count, i => {
            var sub = Contract.Result<IList>()[i];
            return !(sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(Prop.Or);
          }));
            return BreakJuncts(e, Prop.Or);
        }
        
        private static IList/*<IExpr!>*//*!*/ BreakJuncts(IExpr/*!*/ e, IFunctionSymbol/*!*/ sym){
Contract.Requires(sym != null);
Contract.Requires(e != null);
          Contract.Ensures(Contract.Result<IList>() != null);
          Contract.Ensures(Contract.ForAll(0, Contract.Result<IList>().Count, i => {
            var sub = Contract.Result<IList>()[i];
            return (sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(sym);
          }));
            ArrayList/*<IExpr!>*//*!*/ result = new ArrayList();

            IFunApp f = e as IFunApp;
            if (f != null)
            {
                // If it is a sym, go down into sub-expressions.
                if (f.FunctionSymbol.Equals(sym))
                {
                    foreach(IExpr/*!*/ arg in f.Arguments){
Contract.Assert(arg != null);
                        result.AddRange(BreakJuncts(arg,sym));
                    }
                }
                // Otherwise, stop.
                else
                {
                    result.Add(e);
                }
            }
            else
            {
                result.Add(e);
            }

            return result;
        }
    }

    /// <summary>
    /// A callback to produce a function body given the bound variable.
    /// </summary>
    /// <param name="var">The bound variable to use.</param>
    /// <returns>The function body.</returns>
    public delegate IExpr/*!*/ FunctionBody(IVariable/*!*/ var);

    /// <summary>
    ///  An interface for constructing propositional expressions.
    /// 
    ///  This interface should be implemented by the client.  An implementation of
    ///  of this class should generally be used as a singleton object.
    /// </summary>
    /// 
    [ContractClass(typeof(IPropExprFactoryContracts))]
    public interface IPropExprFactory
    {
        IFunApp/*!*/ False { get /*ensures result.FunctionSymbol.Equals(Prop.False);*/; }
        IFunApp/*!*/ True { get /*ensures result.FunctionSymbol.Equals(Prop.True);*/; }

        IFunApp/*!*/ Not(IExpr/*!*/ p) /*ensures result.FunctionSymbol.Equals(Prop.Not);*/;

        IFunApp/*!*/ And(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.And);*/;
        IFunApp/*!*/ Or(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.Or);*/;
        
        IFunApp/*!*/ Implies(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.Implies);*/;
    }
    [ContractClassFor(typeof(IPropExprFactory))]
    public abstract class IPropExprFactoryContracts:IPropExprFactory{
    #region IPropExprFactory Members
    IFunApp  IPropExprFactory.Implies(IExpr p, IExpr q)
    {
      Contract.Requires(p != null);
      Contract.Requires(q != null);
      Contract.Ensures(Contract.Result<IFunApp>() != null);
 	    throw new System.NotImplementedException();
    }

IFunApp  IPropExprFactory.False
{
  
	get { Contract.Ensures(Contract.Result<IFunApp>() != null);throw new System.NotImplementedException(); }
}

IFunApp  IPropExprFactory.True
{
	get {Contract.Ensures(Contract.Result<IFunApp>() != null); throw new System.NotImplementedException(); }
}

IFunApp  IPropExprFactory.Not(IExpr p)
{
  Contract.Requires(p != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  IPropExprFactory.And(IExpr p, IExpr q)
{
  Contract.Requires(p != null);
  Contract.Requires(q != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  IPropExprFactory.Or(IExpr p, IExpr q)
{Contract.Requires(p != null);
  Contract.Requires(q != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}



#endregion
}
    
    /// <summary>
    /// Like IPropExprFactory, but also with quantifiers.
    /// </summary>
    /// 
  [ContractClass(typeof(IQuantPropExprFactoryContracts))]
    public interface IQuantPropExprFactory : IPropExprFactory {
        /// <summary>
        /// Produce an existential given the lambda-expression.
        /// </summary>
        /// <param name="p">The lambda-expression.</param>
        /// <returns>The existential.</returns>
        IFunApp/*!*/ Exists(IFunction/*!*/ p) /*ensures result.FunctionSymbol.Equals(Prop.Exists);*/;
        IFunApp/*!*/ Forall(IFunction/*!*/ p) /*ensures result.FunctionSymbol.Equals(Prop.Forall);*/;

        /// <summary>
        /// Produce an existential given a callback that can produce a function body given the
        /// bound variable to use.  The implementer of this method is responsible for generating
        /// a fresh new variable to pass to the FunctionBody callback to use as the bound variable.
        /// </summary>
        /// <param name="body">The function body callback.</param>
        /// <returns>The existential.</returns>
        IFunApp/*!*/ Exists(AIType paramType, FunctionBody/*!*/ body) /*ensures result.FunctionSymbol.Equals(Prop.Exists);*/;
        IFunApp/*!*/ Forall(AIType paramType, FunctionBody/*!*/ body) /*ensures result.FunctionSymbol.Equals(Prop.Forall);*/;
    }
  [ContractClassFor(typeof(IQuantPropExprFactory))]
  public abstract class IQuantPropExprFactoryContracts:IQuantPropExprFactory{
  #region IQuantPropExprFactory Members

IFunApp  IQuantPropExprFactory.Exists(IFunction p)
{
  Contract.Requires(p != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  IQuantPropExprFactory.Forall(IFunction p)
{Contract.Requires(p != null);Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  IQuantPropExprFactory.Exists(AIType paramType, FunctionBody body)
{Contract.Requires(body != null);Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  IQuantPropExprFactory.Forall(AIType paramType, FunctionBody body)
{Contract.Requires(body != null);Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

#endregion

#region IPropExprFactory Members

IFunApp  IPropExprFactory.False
{
	get { throw new System.NotImplementedException(); }
}

IFunApp  IPropExprFactory.True
{
	get { throw new System.NotImplementedException(); }
}

IFunApp  IPropExprFactory.Not(IExpr p)
{
 	throw new System.NotImplementedException();
}

IFunApp  IPropExprFactory.And(IExpr p, IExpr q)
{
 	throw new System.NotImplementedException();
}

IFunApp  IPropExprFactory.Or(IExpr p, IExpr q)
{
 	throw new System.NotImplementedException();
}

IFunApp  IPropExprFactory.Implies(IExpr p, IExpr q)
{
 	throw new System.NotImplementedException();
}

#endregion
}

    /// <summary>
    ///  An interface for constructing value expressions.
    /// 
    ///  This interface should be implemented by the client.  An implementation of
    ///  of this class should generally be used as a singleton object.
    /// </summary>
    /// 
  [ContractClass(typeof(IValueExprFactoryContracts))]
    public interface IValueExprFactory
    {
        IFunApp/*!*/ Eq (IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Eq);*/;
        IFunApp/*!*/ Neq(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Neq);*/;
    }
  [ContractClassFor(typeof(IValueExprFactory))]
  public abstract class IValueExprFactoryContracts:IValueExprFactory{
  #region IValueExprFactory Members

IFunApp  IValueExprFactory.Eq(IExpr e0, IExpr e1)
{
  Contract.Requires(e0 != null);
  Contract.Requires(e1 != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  IValueExprFactory.Neq(IExpr e0, IExpr e1)
{
  Contract.Requires(e0 != null);
  Contract.Requires(e1 != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

#endregion
}

    /// <summary>
    ///  An interface for constructing value expressions having to with null.
    /// 
    ///  This interface should be implemented by the client.  An implementation of
    ///  of this class should generally be used as a singleton object.
    /// </summary>
    /// 
  [ContractClass(typeof(INullnessFactoryContracts))]
    public interface INullnessFactory
    {
        IFunApp/*!*/ Eq(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Eq);*/;
        IFunApp/*!*/ Neq(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Neq);*/;
        IFunApp/*!*/ Null { get; /*ensures result.FunctionSymbol.Equals(Ref.Null);*/ }
    }
  [ContractClassFor(typeof(INullnessFactory))]
  public abstract class INullnessFactoryContracts:INullnessFactory{
#region INullnessFactory Members

IFunApp  INullnessFactory.Eq(IExpr e0, IExpr e1)
{
  Contract.Requires(e0 != null);
  Contract.Requires(e1 != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  INullnessFactory.Neq(IExpr e0, IExpr e1)
{
  Contract.Requires(e0 != null);
  Contract.Requires(e1 != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  INullnessFactory.Null
{
	get {
  Contract.Ensures(Contract.Result<IFunApp>() != null);
    throw new System.NotImplementedException(); }
}

#endregion
}

    /// <summary>
    ///  An interface for constructing integer expressions.
    /// 
    ///  This interface should be implemented by the client.  An implementation of
    ///  of this class should generally be used as a singleton object.
    /// </summary>
    /// 
  [ContractClass(typeof(IIntExprFactoryContracts))]
    public interface IIntExprFactory : IValueExprFactory
    {
      IFunApp/*!*/ Const(BigNum i) /*ensures result.FunctionSymbol.Equals(new IntSymbol(i));*/;
    }
  [ContractClassFor(typeof(IIntExprFactory))]
    public abstract class IIntExprFactoryContracts : IIntExprFactory {

      #region IIntExprFactory Members

      IFunApp IIntExprFactory.Const(BigNum i) {
        Contract.Ensures(Contract.Result<IFunApp>() != null);
        throw new System.NotImplementedException();
      }

      #endregion

      #region IValueExprFactory Members

      IFunApp IValueExprFactory.Eq(IExpr e0, IExpr e1) {
        throw new System.NotImplementedException();
      }

      IFunApp IValueExprFactory.Neq(IExpr e0, IExpr e1) {
        throw new System.NotImplementedException();
      }

      #endregion
    }

    /// <summary>
    ///  An interface for constructing linear integer expressions.
    /// 
    ///  This interface should be implemented by the client.  An implementation of
    ///  of this class should generally be used as a singleton object.
    /// </summary>
    /// 
  [ContractClass(typeof(ILinearExprFactoryContracts))]
    public interface ILinearExprFactory : IIntExprFactory
    {
        IFunApp/*!*/ AtMost(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.AtMost);*/;
        IFunApp/*!*/ Add(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Add);*/;
        /// <summary>
        /// If "var" is null, returns an expression representing r.
        /// Otherwise, returns an expression representing r*var.
        /// </summary>
        IExpr/*!*/ Term(Microsoft.Basetypes.Rational r, IVariable var);

        IFunApp/*!*/ False { get /*ensures result.FunctionSymbol.Equals(Prop.False);*/; }
        IFunApp/*!*/ True { get /*ensures result.FunctionSymbol.Equals(Prop.True);*/; }
        IFunApp/*!*/ And(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.And);*/;
    }
  [ContractClassFor(typeof(ILinearExprFactory))]
  public abstract class ILinearExprFactoryContracts:ILinearExprFactory{

  #region ILinearExprFactory Members

IFunApp  ILinearExprFactory.AtMost(IExpr e0, IExpr e1)
{
  Contract.Requires(e0 != null);
  Contract.Requires(e1 != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  ILinearExprFactory.Add(IExpr e0, IExpr e1)
{
  Contract.Requires(e0 != null);
  Contract.Requires(e1 != null);Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IExpr  ILinearExprFactory.Term(Rational r, IVariable var)
{
  Contract.Ensures(Contract.Result<IExpr>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  ILinearExprFactory.False
{
	get {Contract.Ensures(Contract.Result<IFunApp>() != null); throw new System.NotImplementedException(); }
}

IFunApp  ILinearExprFactory.True
{
	get { Contract.Ensures(Contract.Result<IFunApp>() != null);throw new System.NotImplementedException(); }
}

IFunApp  ILinearExprFactory.And(IExpr p, IExpr q)
{
  Contract.Requires(p != null);
  Contract.Requires(q != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

#endregion

#region IIntExprFactory Members

IFunApp IIntExprFactory.Const(BigNum i) {
  throw new System.NotImplementedException();
}

#endregion

#region IValueExprFactory Members

IFunApp IValueExprFactory.Eq(IExpr e0, IExpr e1) {
  throw new System.NotImplementedException();
}

IFunApp IValueExprFactory.Neq(IExpr e0, IExpr e1) {
  throw new System.NotImplementedException();
}

#endregion
  }

    /// <summary>
    ///  An interface for constructing type expressions and performing some type operations.
    ///  The types are assumed to be arranged in a rooted tree.
    ///
    ///  This interface should be implemented by the client.  An implementation of
    ///  of this class should generally be used as a singleton object.
    /// </summary>
    /// 
  [ContractClass(typeof(ITypeExprFactoryContracts))]
    public interface ITypeExprFactory
    {
        /// <summary>
        /// Returns an expression denoting the top of the type hierarchy.
        /// </summary>
        IExpr/*!*/ RootType { get; }

        /// <summary>
        /// Returns true iff "t" denotes a type constant.
        /// </summary>
        [Pure]
        bool IsTypeConstant(IExpr/*!*/ t);

        /// <summary>
        /// Returns true iff t0 and t1 are types such that t0 and t1 are equal.
        /// </summary>
        [Pure]
        bool IsTypeEqual(IExpr/*!*/ t0, IExpr/*!*/ t1);

        /// <summary>
        /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.
        /// </summary>
        [Pure]
        bool IsSubType(IExpr/*!*/ t0, IExpr/*!*/ t1);

        /// <summary>
        /// Returns the most derived supertype of both "t0" and "t1".  A precondition is
        /// that "t0" and "t1" both represent types.
        /// </summary>
        IExpr/*!*/ JoinTypes(IExpr/*!*/ t0, IExpr/*!*/ t1);

        IFunApp/*!*/ IsExactlyA(IExpr/*!*/ e, IExpr/*!*/ type) /*requires IsTypeConstant(type); ensures result.FunctionSymbol.Equals(Value.Eq);*/;
        IFunApp/*!*/ IsA(IExpr/*!*/ e, IExpr/*!*/ type) /*requires IsTypeConstant(type); ensures result.FunctionSymbol.Equals(Value.Subtype);*/;
    }
  [ContractClassFor(typeof(ITypeExprFactory))]
  public abstract class ITypeExprFactoryContracts:ITypeExprFactory{

  #region ITypeExprFactory Members

IExpr  ITypeExprFactory.RootType
{
	get {Contract.Ensures(Contract.Result<IExpr>() != null); throw new System.NotImplementedException(); }
}

bool  ITypeExprFactory.IsTypeConstant(IExpr t)
{
  Contract.Requires(t != null);
 	throw new System.NotImplementedException();
}

bool  ITypeExprFactory.IsTypeEqual(IExpr t0, IExpr t1)
{
  Contract.Requires(t0 != null);
  Contract.Requires(t1 != null);
 	throw new System.NotImplementedException();
}

bool  ITypeExprFactory.IsSubType(IExpr t0, IExpr t1)
{
  Contract.Requires(t0 != null);
  Contract.Requires(t1 != null);
 	throw new System.NotImplementedException();
}

IExpr  ITypeExprFactory.JoinTypes(IExpr t0, IExpr t1)
{
  Contract.Requires(t0 != null);
  Contract.Requires(t1 != null);
  Contract.Ensures(Contract.Result<IExpr>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  ITypeExprFactory.IsExactlyA(IExpr e, IExpr type)
{
  Contract.Requires(e != null);
  Contract.Requires(type != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

IFunApp  ITypeExprFactory.IsA(IExpr e, IExpr type)
{
  Contract.Requires(e != null);
  Contract.Requires(type != null);
  Contract.Ensures(Contract.Result<IFunApp>() != null);
 	throw new System.NotImplementedException();
}

#endregion
}
}