From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/AIFramework/CommonFunctionSymbols.cs | 2464 +++++++++++++-------------- 1 file changed, 1232 insertions(+), 1232 deletions(-) (limited to 'Source/AIFramework/CommonFunctionSymbols.cs') diff --git a/Source/AIFramework/CommonFunctionSymbols.cs b/Source/AIFramework/CommonFunctionSymbols.cs index 6f7a9f93..6a287810 100644 --- a/Source/AIFramework/CommonFunctionSymbols.cs +++ b/Source/AIFramework/CommonFunctionSymbols.cs @@ -1,1232 +1,1232 @@ -//----------------------------------------------------------------------------- -// -// 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; - - /// - /// A basic class for function symbols. - /// - 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() != null); return typ; } } - - [NoDefaultContract] - [Pure] - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != null); - return display; - } - - } - - /// - /// A class for integer constants. - /// - public class IntSymbol : FunctionSymbol - { - public readonly BigNum Value; - - /// - /// The intention is that this constructor be called only from the Int.Const method. - /// - 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(); - } - } - - /// - /// A class for bitvector constants. - /// - public class BvSymbol : FunctionSymbol - { - public readonly BigNum Value; - public readonly int Bits; - - /// - /// The intention is that this constructor be called only from the Int.Const method. - /// - 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; - - /// - /// The intention is that this constructor be called only from the Double.Const method. - /// - 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(); - } - } - - /// - /// Function symbol based on a string. Uses the string equality for determining equality - /// of symbol. - /// - public class NamedSymbol : FunctionSymbol - { - public string/*!*/ Value { [NoDefaultContract] get { Contract.Ensures(Contract.Result() != 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 ---------------------------------- - - /// - /// A class with the equality symbol and the ValueType.Type. - /// - public class Value : AIType - { - private static readonly AIType/*!*/ valtype = new Value(); - public static AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != 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() != 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; - - private static AIType/*!*/ BinrelType { - get { - Contract.Ensures(Contract.Result() != 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() != null); - if (_eq == null) { - _eq = new FunctionSymbol("=", BinrelType); - } - return _eq; - } - } - [Once] - private static FunctionSymbol/*!*/ _neq; - public static FunctionSymbol/*!*/ Neq { - get { - Contract.Ensures(Contract.Result() != null); - if (_neq == null) { - _neq = new FunctionSymbol("!=", BinrelType); - } - return _neq; - } - } - [Once] - private static FunctionSymbol/*!*/ _subtype; - public static FunctionSymbol/*!*/ Subtype { - get { - Contract.Ensures(Contract.Result() != 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() != 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() != null); - if (_typeof == null) { - _typeof = new FunctionSymbol("typeof", TypeofType); - } - return _typeof; - } - } - - /// - /// Value should not be instantiated from the outside, except perhaps in - /// subclasses. - /// - protected Value() { } - - } - - public class Int : Value - { - private static readonly AIType/*!*/ inttype = new Int(); - public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != 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() != null); return _negate; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Add { get { Contract.Ensures(Contract.Result() != null); return _add; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Sub { get { Contract.Ensures(Contract.Result() != null); return _sub; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Mul { get { Contract.Ensures(Contract.Result() != null); return _mul; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Div { get { Contract.Ensures(Contract.Result() != null); return _div; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Mod { get { Contract.Ensures(Contract.Result() != null); return _mod; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ AtMost { get { Contract.Ensures(Contract.Result() != null); return _atmost; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Less { get { Contract.Ensures(Contract.Result() != null); return _less; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Greater { get { Contract.Ensures(Contract.Result() != null); return _greater; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ AtLeast { get { Contract.Ensures(Contract.Result() != null); return _atleast; } } - - public static IntSymbol/*!*/ Const(BigNum x) { - Contract.Ensures(Contract.Result() != null); - // We could cache things here, but for now we don't. - return new IntSymbol(x); - } - - /// - /// Int should not be instantiated from the outside, except perhaps in - /// subclasses. - /// - private Int() { } - } - - public class Double : Value - { - private static readonly AIType/*!*/ doubletype = new Double(); - public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != null); return doubletype; } } - - public static DoubleSymbol/*!*/ Const(double x) { - Contract.Ensures(Contract.Result() != null); - // We could cache things here, but for now we don't. - return new DoubleSymbol(x); - } - - /// - /// Double should not be instantiated from the outside, except perhaps in - /// subclasses. - /// - private Double() { } - } - - public class Bv : Value - { - private static readonly AIType/*!*/ bvtype = new Bv(); - public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != 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() != null); return _negate; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Add { get { Contract.Ensures(Contract.Result() != null); return _add; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Sub { get { Contract.Ensures(Contract.Result() != null); return _sub; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Mul { get { Contract.Ensures(Contract.Result() != null); return _mul; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Div { get { Contract.Ensures(Contract.Result() != null); return _div; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Mod { get { Contract.Ensures(Contract.Result() != null); return _mod; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ AtMost { get { Contract.Ensures(Contract.Result() != null); return _atmost; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Less { get { Contract.Ensures(Contract.Result() != null); return _less; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Greater { get { Contract.Ensures(Contract.Result() != null); return _greater; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ AtLeast { get { Contract.Ensures(Contract.Result() != null); return _atleast; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Extract { get { Contract.Ensures(Contract.Result() != null); return _extract; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Concat { get { Contract.Ensures(Contract.Result() != null); return _concat; } } - - public static BvSymbol/*!*/ Const(BigNum x, int y) { - Contract.Ensures(Contract.Result() != null); - // We could cache things here, but for now we don't. - return new BvSymbol(x, y); - } - - /// - /// Int should not be instantiated from the outside, except perhaps in - /// subclasses. - /// - private Bv() { } - } - - public class Ref : Value - { - private static readonly AIType/*!*/ reftype = new Ref(); - public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != null); return reftype; } } - - private static readonly FunctionSymbol/*!*/ _null = new FunctionSymbol("null", Type); - - public static FunctionSymbol/*!*/ Null { get { Contract.Ensures(Contract.Result() != null); return _null; } } - - /// - /// Ref should not be instantiated from the outside, except perhaps in - /// subclasses. - /// - private Ref() { } - } - - public class HeapStructure : Value - { - private static readonly AIType/*!*/ reftype = new HeapStructure(); - public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != null); return reftype; } } - - - - /// - /// HeapStructure should not be instantiated from the outside, except perhaps in - /// subclasses. - /// - private HeapStructure() { } - } - - public class FieldName : Value - { - private static readonly AIType/*!*/ fieldnametype = new FieldName(); - public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != null); return fieldnametype; } } - - private static readonly FunctionSymbol/*!*/ _allocated = new FunctionSymbol("$allocated", FieldName.Type); - public static FunctionSymbol/*!*/ Allocated { get { Contract.Ensures(Contract.Result() != null); return _allocated; } } - - /// - /// Is this a boolean field that monotonically goes from false to true? - /// - public static bool IsBooleanMonotonicallyWeakening(IFunctionSymbol/*!*/ f) { - Contract.Requires(f != null); - return f.Equals(Allocated); - } - - /// - /// FieldName should not be instantiated from the outside, except perhaps in - /// subclasses. - /// - private FieldName() { } - } - - public class Heap : Value - { - private static readonly AIType/*!*/ heaptype = new Heap(); - public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != 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() != 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() != 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() != 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() != 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() != null); return _unsupportedHeapOp; } } - - /// - /// Heap should not be instantiated from the outside, except perhaps in - /// subclasses. - /// - private Heap() { } - } - - // public class List : Value - // { - // private static IDictionary/**/! 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/**/! 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/**/! 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; } } - // - // /// - // /// List should not be instantiated from the outside. - // /// - // 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; } } - // - // /// - // /// Pair should not be instantiated from the outside, except by subclasses. - // /// - // protected Pair(AIType! type1, AIType! type2) - // { - // this.type1 = type1; - // this.type2 = type2; - // } - // } - - //-------------------------- Propositions --------------------------- - - - /// - /// A class with global propositional symbols and the Prop.Type. - /// - public sealed class Prop : AIType - { - private static readonly AIType/*!*/ proptype = new Prop(); - - public static AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != 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() != null); return _false; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ True { get { Contract.Ensures(Contract.Result() != null); return _true; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Not { get { Contract.Ensures(Contract.Result() != null); return _not; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ And { [Pure] get { Contract.Ensures(Contract.Result() != null); return _and; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Or { get { Contract.Ensures(Contract.Result() != null); return _or; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Implies { get { Contract.Ensures(Contract.Result() != null); return _implies; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Exists { get { Contract.Ensures(Contract.Result() != null); return _exists; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Forall { get { Contract.Ensures(Contract.Result() != null); return _forall; } } - [Pure] - [Reads(ReadsAttribute.Reads.Nothing)] - public static FunctionSymbol/*!*/ Lambda { get { Contract.Ensures(Contract.Result() != null); return _lambda; } } - - - /// - /// Prop should not be instantiated from the outside. - /// - 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() != 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/**//*!*/ exprs) { - Contract.Requires(exprs != null); - Contract.Requires(factory != null); - Contract.Ensures(Contract.Result() != 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() != 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/**//*!*/ exprs) { - Contract.Requires(exprs != null); - Contract.Requires(factory != null); - Contract.Ensures(Contract.Result() != 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; - } - - - - /// - /// Break top-level conjuncts into a list of sub-expressions. - /// - /// The expression to examine. - /// A list of conjuncts. - internal static IList/**//*!*/ BreakConjuncts(IExpr/*!*/ e) { - Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.ForAll(0, Contract.Result().Count, i => { - var sub = Contract.Result()[i]; - return !(sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(Prop.And); - })); - return BreakJuncts(e, Prop.And); - } - - /// - /// Break top-level disjuncts into a list of sub-expressions. - /// - /// The expression to examine. - /// A list of conjuncts. - internal static IList/**//*!*/ BreakDisjuncts(IExpr/*!*/ e) { - Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.ForAll(0, Contract.Result().Count, i => { - var sub = Contract.Result()[i]; - return !(sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(Prop.Or); - })); - return BreakJuncts(e, Prop.Or); - } - - private static IList/**//*!*/ BreakJuncts(IExpr/*!*/ e, IFunctionSymbol/*!*/ sym) { - Contract.Requires(sym != null); - Contract.Requires(e != null); - Contract.Ensures(Contract.Result() != null); - Contract.Ensures(Contract.ForAll(0, Contract.Result().Count, i => { - var sub = Contract.Result()[i]; - return (sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(sym); - })); - ArrayList/**//*!*/ 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; - } - } - - /// - /// A callback to produce a function body given the bound variable. - /// - /// The bound variable to use. - /// The function body. - public delegate IExpr/*!*/ FunctionBody(IVariable/*!*/ var); - - /// - /// 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. - /// - /// - [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() != null); - throw new System.NotImplementedException(); - } - - IFunApp IPropExprFactory.False { - - get { Contract.Ensures(Contract.Result() != null); throw new System.NotImplementedException(); } - } - - IFunApp IPropExprFactory.True { - get { Contract.Ensures(Contract.Result() != null); throw new System.NotImplementedException(); } - } - - IFunApp IPropExprFactory.Not(IExpr p) { - Contract.Requires(p != null); - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - - IFunApp IPropExprFactory.And(IExpr p, IExpr q) { - Contract.Requires(p != null); - Contract.Requires(q != null); - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - - IFunApp IPropExprFactory.Or(IExpr p, IExpr q) { - Contract.Requires(p != null); - Contract.Requires(q != null); - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - - - - #endregion - } - - /// - /// 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. - /// - /// - [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() != null); - throw new System.NotImplementedException(); - } - - IFunApp IValueExprFactory.Neq(IExpr e0, IExpr e1) { - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - - #endregion - } - - /// - /// 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. - /// - /// - [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() != null); - throw new System.NotImplementedException(); - } - - IFunApp INullnessFactory.Neq(IExpr e0, IExpr e1) { - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - - IFunApp INullnessFactory.Null { - get { - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - } - - #endregion - } - - /// - /// 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. - /// - /// - [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() != 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 - } - - /// - /// 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. - /// - /// - [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);*/; - /// - /// If "var" is null, returns an expression representing r. - /// Otherwise, returns an expression representing r*var. - /// - 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() != null); - throw new System.NotImplementedException(); - } - - IFunApp ILinearExprFactory.Add(IExpr e0, IExpr e1) { - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - - IExpr ILinearExprFactory.Term(Rational r, IVariable var) { - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - - IFunApp ILinearExprFactory.False { - get { Contract.Ensures(Contract.Result() != null); throw new System.NotImplementedException(); } - } - - IFunApp ILinearExprFactory.True { - get { Contract.Ensures(Contract.Result() != null); throw new System.NotImplementedException(); } - } - - IFunApp ILinearExprFactory.And(IExpr p, IExpr q) { - Contract.Requires(p != null); - Contract.Requires(q != null); - Contract.Ensures(Contract.Result() != 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 - } - - /// - /// 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. - /// - /// - [ContractClass(typeof(ITypeExprFactoryContracts))] - public interface ITypeExprFactory - { - /// - /// Returns an expression denoting the top of the type hierarchy. - /// - IExpr/*!*/ RootType { get; } - - /// - /// Returns true iff "t" denotes a type constant. - /// - [Pure] - bool IsTypeConstant(IExpr/*!*/ t); - - /// - /// Returns true iff t0 and t1 are types such that t0 and t1 are equal. - /// - [Pure] - bool IsTypeEqual(IExpr/*!*/ t0, IExpr/*!*/ t1); - - /// - /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1. - /// - [Pure] - bool IsSubType(IExpr/*!*/ t0, IExpr/*!*/ t1); - - /// - /// Returns the most derived supertype of both "t0" and "t1". A precondition is - /// that "t0" and "t1" both represent types. - /// - 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() != 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() != null); - throw new System.NotImplementedException(); - } - - IFunApp ITypeExprFactory.IsExactlyA(IExpr e, IExpr type) { - Contract.Requires(e != null); - Contract.Requires(type != null); - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - - IFunApp ITypeExprFactory.IsA(IExpr e, IExpr type) { - Contract.Requires(e != null); - Contract.Requires(type != null); - Contract.Ensures(Contract.Result() != null); - throw new System.NotImplementedException(); - } - - #endregion - } -} +//----------------------------------------------------------------------------- +// +// 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; + + /// + /// A basic class for function symbols. + /// + 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() != null); return typ; } } + + [NoDefaultContract] + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != null); + return display; + } + + } + + /// + /// A class for integer constants. + /// + public class IntSymbol : FunctionSymbol + { + public readonly BigNum Value; + + /// + /// The intention is that this constructor be called only from the Int.Const method. + /// + 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(); + } + } + + /// + /// A class for bitvector constants. + /// + public class BvSymbol : FunctionSymbol + { + public readonly BigNum Value; + public readonly int Bits; + + /// + /// The intention is that this constructor be called only from the Int.Const method. + /// + 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; + + /// + /// The intention is that this constructor be called only from the Double.Const method. + /// + 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(); + } + } + + /// + /// Function symbol based on a string. Uses the string equality for determining equality + /// of symbol. + /// + public class NamedSymbol : FunctionSymbol + { + public string/*!*/ Value { [NoDefaultContract] get { Contract.Ensures(Contract.Result() != 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 ---------------------------------- + + /// + /// A class with the equality symbol and the ValueType.Type. + /// + public class Value : AIType + { + private static readonly AIType/*!*/ valtype = new Value(); + public static AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != 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() != 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; + + private static AIType/*!*/ BinrelType { + get { + Contract.Ensures(Contract.Result() != 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() != null); + if (_eq == null) { + _eq = new FunctionSymbol("=", BinrelType); + } + return _eq; + } + } + [Once] + private static FunctionSymbol/*!*/ _neq; + public static FunctionSymbol/*!*/ Neq { + get { + Contract.Ensures(Contract.Result() != null); + if (_neq == null) { + _neq = new FunctionSymbol("!=", BinrelType); + } + return _neq; + } + } + [Once] + private static FunctionSymbol/*!*/ _subtype; + public static FunctionSymbol/*!*/ Subtype { + get { + Contract.Ensures(Contract.Result() != 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() != 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() != null); + if (_typeof == null) { + _typeof = new FunctionSymbol("typeof", TypeofType); + } + return _typeof; + } + } + + /// + /// Value should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + protected Value() { } + + } + + public class Int : Value + { + private static readonly AIType/*!*/ inttype = new Int(); + public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != 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() != null); return _negate; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Add { get { Contract.Ensures(Contract.Result() != null); return _add; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Sub { get { Contract.Ensures(Contract.Result() != null); return _sub; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Mul { get { Contract.Ensures(Contract.Result() != null); return _mul; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Div { get { Contract.Ensures(Contract.Result() != null); return _div; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Mod { get { Contract.Ensures(Contract.Result() != null); return _mod; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ AtMost { get { Contract.Ensures(Contract.Result() != null); return _atmost; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Less { get { Contract.Ensures(Contract.Result() != null); return _less; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Greater { get { Contract.Ensures(Contract.Result() != null); return _greater; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ AtLeast { get { Contract.Ensures(Contract.Result() != null); return _atleast; } } + + public static IntSymbol/*!*/ Const(BigNum x) { + Contract.Ensures(Contract.Result() != null); + // We could cache things here, but for now we don't. + return new IntSymbol(x); + } + + /// + /// Int should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Int() { } + } + + public class Double : Value + { + private static readonly AIType/*!*/ doubletype = new Double(); + public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != null); return doubletype; } } + + public static DoubleSymbol/*!*/ Const(double x) { + Contract.Ensures(Contract.Result() != null); + // We could cache things here, but for now we don't. + return new DoubleSymbol(x); + } + + /// + /// Double should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Double() { } + } + + public class Bv : Value + { + private static readonly AIType/*!*/ bvtype = new Bv(); + public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != 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() != null); return _negate; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Add { get { Contract.Ensures(Contract.Result() != null); return _add; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Sub { get { Contract.Ensures(Contract.Result() != null); return _sub; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Mul { get { Contract.Ensures(Contract.Result() != null); return _mul; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Div { get { Contract.Ensures(Contract.Result() != null); return _div; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Mod { get { Contract.Ensures(Contract.Result() != null); return _mod; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ AtMost { get { Contract.Ensures(Contract.Result() != null); return _atmost; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Less { get { Contract.Ensures(Contract.Result() != null); return _less; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Greater { get { Contract.Ensures(Contract.Result() != null); return _greater; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ AtLeast { get { Contract.Ensures(Contract.Result() != null); return _atleast; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Extract { get { Contract.Ensures(Contract.Result() != null); return _extract; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Concat { get { Contract.Ensures(Contract.Result() != null); return _concat; } } + + public static BvSymbol/*!*/ Const(BigNum x, int y) { + Contract.Ensures(Contract.Result() != null); + // We could cache things here, but for now we don't. + return new BvSymbol(x, y); + } + + /// + /// Int should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Bv() { } + } + + public class Ref : Value + { + private static readonly AIType/*!*/ reftype = new Ref(); + public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != null); return reftype; } } + + private static readonly FunctionSymbol/*!*/ _null = new FunctionSymbol("null", Type); + + public static FunctionSymbol/*!*/ Null { get { Contract.Ensures(Contract.Result() != null); return _null; } } + + /// + /// Ref should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Ref() { } + } + + public class HeapStructure : Value + { + private static readonly AIType/*!*/ reftype = new HeapStructure(); + public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != null); return reftype; } } + + + + /// + /// HeapStructure should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private HeapStructure() { } + } + + public class FieldName : Value + { + private static readonly AIType/*!*/ fieldnametype = new FieldName(); + public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != null); return fieldnametype; } } + + private static readonly FunctionSymbol/*!*/ _allocated = new FunctionSymbol("$allocated", FieldName.Type); + public static FunctionSymbol/*!*/ Allocated { get { Contract.Ensures(Contract.Result() != null); return _allocated; } } + + /// + /// Is this a boolean field that monotonically goes from false to true? + /// + public static bool IsBooleanMonotonicallyWeakening(IFunctionSymbol/*!*/ f) { + Contract.Requires(f != null); + return f.Equals(Allocated); + } + + /// + /// FieldName should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private FieldName() { } + } + + public class Heap : Value + { + private static readonly AIType/*!*/ heaptype = new Heap(); + public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != 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() != 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() != 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() != 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() != 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() != null); return _unsupportedHeapOp; } } + + /// + /// Heap should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Heap() { } + } + + // public class List : Value + // { + // private static IDictionary/**/! 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/**/! 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/**/! 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; } } + // + // /// + // /// List should not be instantiated from the outside. + // /// + // 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; } } + // + // /// + // /// Pair should not be instantiated from the outside, except by subclasses. + // /// + // protected Pair(AIType! type1, AIType! type2) + // { + // this.type1 = type1; + // this.type2 = type2; + // } + // } + + //-------------------------- Propositions --------------------------- + + + /// + /// A class with global propositional symbols and the Prop.Type. + /// + public sealed class Prop : AIType + { + private static readonly AIType/*!*/ proptype = new Prop(); + + public static AIType/*!*/ Type { get { Contract.Ensures(Contract.Result() != 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() != null); return _false; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ True { get { Contract.Ensures(Contract.Result() != null); return _true; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Not { get { Contract.Ensures(Contract.Result() != null); return _not; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ And { [Pure] get { Contract.Ensures(Contract.Result() != null); return _and; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Or { get { Contract.Ensures(Contract.Result() != null); return _or; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Implies { get { Contract.Ensures(Contract.Result() != null); return _implies; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Exists { get { Contract.Ensures(Contract.Result() != null); return _exists; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Forall { get { Contract.Ensures(Contract.Result() != null); return _forall; } } + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] + public static FunctionSymbol/*!*/ Lambda { get { Contract.Ensures(Contract.Result() != null); return _lambda; } } + + + /// + /// Prop should not be instantiated from the outside. + /// + 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() != 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/**//*!*/ exprs) { + Contract.Requires(exprs != null); + Contract.Requires(factory != null); + Contract.Ensures(Contract.Result() != 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() != 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/**//*!*/ exprs) { + Contract.Requires(exprs != null); + Contract.Requires(factory != null); + Contract.Ensures(Contract.Result() != 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; + } + + + + /// + /// Break top-level conjuncts into a list of sub-expressions. + /// + /// The expression to examine. + /// A list of conjuncts. + internal static IList/**//*!*/ BreakConjuncts(IExpr/*!*/ e) { + Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.ForAll(0, Contract.Result().Count, i => { + var sub = Contract.Result()[i]; + return !(sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(Prop.And); + })); + return BreakJuncts(e, Prop.And); + } + + /// + /// Break top-level disjuncts into a list of sub-expressions. + /// + /// The expression to examine. + /// A list of conjuncts. + internal static IList/**//*!*/ BreakDisjuncts(IExpr/*!*/ e) { + Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.ForAll(0, Contract.Result().Count, i => { + var sub = Contract.Result()[i]; + return !(sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(Prop.Or); + })); + return BreakJuncts(e, Prop.Or); + } + + private static IList/**//*!*/ BreakJuncts(IExpr/*!*/ e, IFunctionSymbol/*!*/ sym) { + Contract.Requires(sym != null); + Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.ForAll(0, Contract.Result().Count, i => { + var sub = Contract.Result()[i]; + return (sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(sym); + })); + ArrayList/**//*!*/ 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; + } + } + + /// + /// A callback to produce a function body given the bound variable. + /// + /// The bound variable to use. + /// The function body. + public delegate IExpr/*!*/ FunctionBody(IVariable/*!*/ var); + + /// + /// 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. + /// + /// + [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() != null); + throw new System.NotImplementedException(); + } + + IFunApp IPropExprFactory.False { + + get { Contract.Ensures(Contract.Result() != null); throw new System.NotImplementedException(); } + } + + IFunApp IPropExprFactory.True { + get { Contract.Ensures(Contract.Result() != null); throw new System.NotImplementedException(); } + } + + IFunApp IPropExprFactory.Not(IExpr p) { + Contract.Requires(p != null); + Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); + } + + IFunApp IPropExprFactory.And(IExpr p, IExpr q) { + Contract.Requires(p != null); + Contract.Requires(q != null); + Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); + } + + IFunApp IPropExprFactory.Or(IExpr p, IExpr q) { + Contract.Requires(p != null); + Contract.Requires(q != null); + Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); + } + + + + #endregion + } + + /// + /// 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. + /// + /// + [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() != null); + throw new System.NotImplementedException(); + } + + IFunApp IValueExprFactory.Neq(IExpr e0, IExpr e1) { + Contract.Requires(e0 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); + } + + #endregion + } + + /// + /// 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. + /// + /// + [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() != null); + throw new System.NotImplementedException(); + } + + IFunApp INullnessFactory.Neq(IExpr e0, IExpr e1) { + Contract.Requires(e0 != null); + Contract.Requires(e1 != null); + Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); + } + + IFunApp INullnessFactory.Null { + get { + Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); + } + } + + #endregion + } + + /// + /// 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. + /// + /// + [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() != 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 + } + + /// + /// 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. + /// + /// + [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);*/; + /// + /// If "var" is null, returns an expression representing r. + /// Otherwise, returns an expression representing r*var. + /// + 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() != null); + throw new System.NotImplementedException(); + } + + IFunApp ILinearExprFactory.Add(IExpr e0, IExpr e1) { + Contract.Requires(e0 != null); + Contract.Requires(e1 != null); Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); + } + + IExpr ILinearExprFactory.Term(Rational r, IVariable var) { + Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); + } + + IFunApp ILinearExprFactory.False { + get { Contract.Ensures(Contract.Result() != null); throw new System.NotImplementedException(); } + } + + IFunApp ILinearExprFactory.True { + get { Contract.Ensures(Contract.Result() != null); throw new System.NotImplementedException(); } + } + + IFunApp ILinearExprFactory.And(IExpr p, IExpr q) { + Contract.Requires(p != null); + Contract.Requires(q != null); + Contract.Ensures(Contract.Result() != 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 + } + + /// + /// 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. + /// + /// + [ContractClass(typeof(ITypeExprFactoryContracts))] + public interface ITypeExprFactory + { + /// + /// Returns an expression denoting the top of the type hierarchy. + /// + IExpr/*!*/ RootType { get; } + + /// + /// Returns true iff "t" denotes a type constant. + /// + [Pure] + bool IsTypeConstant(IExpr/*!*/ t); + + /// + /// Returns true iff t0 and t1 are types such that t0 and t1 are equal. + /// + [Pure] + bool IsTypeEqual(IExpr/*!*/ t0, IExpr/*!*/ t1); + + /// + /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1. + /// + [Pure] + bool IsSubType(IExpr/*!*/ t0, IExpr/*!*/ t1); + + /// + /// Returns the most derived supertype of both "t0" and "t1". A precondition is + /// that "t0" and "t1" both represent types. + /// + 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() != 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() != null); + throw new System.NotImplementedException(); + } + + IFunApp ITypeExprFactory.IsExactlyA(IExpr e, IExpr type) { + Contract.Requires(e != null); + Contract.Requires(type != null); + Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); + } + + IFunApp ITypeExprFactory.IsA(IExpr e, IExpr type) { + Contract.Requires(e != null); + Contract.Requires(type != null); + Contract.Ensures(Contract.Result() != null); + throw new System.NotImplementedException(); + } + + #endregion + } +} -- cgit v1.2.3