diff options
| author |  tabarbe <unknown> | 2010-08-26 23:37:01 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-26 23:37:01 +0000 |
| commit | 47171ab9f9d31dab0d5e0a4c3c95c763452e9295 (patch) | |
| tree | 402d453ee1c63dff1a04d03eabfc2bef32eed4ed /Source/AIFramework/CommonFunctionSymbols.cs | |
| parent | 8b0392fe672ce820ba07af673fe9177babdee00b (diff) | |
Boogie: Renaming the AIFramework sources in preparation for committal of my port of the project
Diffstat (limited to 'Source/AIFramework/CommonFunctionSymbols.cs')
| -rw-r--r-- | Source/AIFramework/CommonFunctionSymbols.cs | 927 |
1 files changed, 927 insertions, 0 deletions
diff --git a/Source/AIFramework/CommonFunctionSymbols.cs b/Source/AIFramework/CommonFunctionSymbols.cs new file mode 100644 index 00000000..bc59df97 --- /dev/null +++ b/Source/AIFramework/CommonFunctionSymbols.cs @@ -0,0 +1,927 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.AbstractInterpretationFramework
+{
+ using Microsoft.Contracts;
+ using System.Collections;
+ 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;
+
+ public FunctionSymbol(AIType! typ)
+ : this("FunctionSymbol", typ)
+ {
+ }
+
+ internal FunctionSymbol(string! display, AIType! typ)
+ {
+ this.display = display;
+ this.typ = typ;
+ // base();
+ }
+
+ public AIType! AIType { get { return typ; } }
+
+ [NoDefaultContract]
+ [Pure]
+ public override string! ToString()
+ {
+ 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((!)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((!)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 { return (!) this.ToString(); } }
+
+ public NamedSymbol(string! symbol, AIType! typ)
+ : base(symbol, typ)
+ {
+ }
+
+ [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 { return valtype; } }
+
+ private static readonly FunctionType[]! funtypeCache = new FunctionType[5];
+ public static FunctionType! FunctionType(int inParameterCount)
+ requires 0 <= inParameterCount;
+ // ensures 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 {
+ if (binreltype == null) {
+ binreltype = new FunctionType(Type, Type, Prop.Type);
+ }
+ return binreltype;
+ }
+ }
+
+ [Once] private static FunctionSymbol! _eq;
+ public static FunctionSymbol! Eq {
+ get {
+ if (_eq == null) {
+ _eq = new FunctionSymbol("=", BinrelType);
+ }
+ return _eq;
+ }
+ }
+ [Once] private static FunctionSymbol! _neq;
+ public static FunctionSymbol! Neq {
+ get {
+ if (_neq == null) {
+ _neq = new FunctionSymbol("!=", BinrelType);
+ }
+ return _neq;
+ }
+ }
+ [Once] private static FunctionSymbol! _subtype;
+ public static FunctionSymbol! Subtype {
+ get {
+ if (_subtype == null) {
+ _subtype = new FunctionSymbol("<:", BinrelType);
+ }
+ return _subtype;
+ }
+ }
+
+ [Once] private static AIType! typeof_type;
+ private static AIType! TypeofType {
+ get {
+ if (typeof_type == null) {
+ typeof_type = new FunctionType(Ref.Type, Type);
+ }
+ return typeof_type;
+ }
+ }
+ [Once] private static FunctionSymbol! _typeof;
+ public static FunctionSymbol! Typeof {
+ get {
+ 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 AIType! Type { get { 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 { return _negate; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Add { get { return _add; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Sub { get { return _sub; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mul { get { return _mul; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Div { get { return _div; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mod { get { return _mod; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtMost { get { return _atmost; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Less { get { return _less; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Greater { get { return _greater; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtLeast { get { return _atleast; } }
+
+ public static IntSymbol! Const(BigNum x)
+ {
+ // 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 AIType! Type { get { return doubletype; } }
+
+ public static DoubleSymbol! Const(double x)
+ {
+ // 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 AIType! Type { get { 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 { return _negate; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Add { get { return _add; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Sub { get { return _sub; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mul { get { return _mul; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Div { get { return _div; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mod { get { return _mod; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtMost { get { return _atmost; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Less { get { return _less; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Greater { get { return _greater; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtLeast { get { return _atleast; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Extract { get { return _extract; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Concat { get { return _concat; } }
+
+ public static BvSymbol! Const(BigNum x, int y)
+ {
+ // 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 AIType! Type { get { return reftype; } }
+
+ private static readonly FunctionSymbol! _null = new FunctionSymbol("null", Type);
+
+ public static FunctionSymbol! Null { get { 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 AIType! Type { get { 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 AIType! Type { get { return fieldnametype; } }
+
+ private static readonly FunctionSymbol! _allocated = new FunctionSymbol("$allocated", FieldName.Type);
+ public static FunctionSymbol! Allocated { get { return _allocated; } }
+
+ /// <summary>
+ /// Is this a boolean field that monotonically goes from false to true?
+ /// </summary>
+ public static bool IsBooleanMonotonicallyWeakening(IFunctionSymbol! f)
+ {
+ 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 AIType! Type { get { 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 { 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 { 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 { 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 { 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 { 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 { get { 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 { get { return type1; } }
+// public AIType! Type2 { get { 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();
+ public static AIType! Type { get { 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 { return _false; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! True { get { return _true; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Not { get { return _not; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! And { [Pure] get { return _and; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Or { get { return _or; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Implies { get { return _implies; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Exists { get { return _exists; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Forall { get { return _forall; } }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Lambda { get { 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)
+ {
+ 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)
+ {
+ IExpr! result = factory.True;
+ foreach (IExpr! conjunct in exprs)
+ {
+ result = SimplifiedAnd(factory, result, conjunct);
+ }
+ return result;
+ }
+
+ public static IExpr! SimplifiedOr(IPropExprFactory! factory, IExpr! e0, IExpr! e1)
+ {
+ 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)
+ {
+ IExpr! result = factory.False;
+ foreach (IExpr! disj in exprs)
+ {
+ 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)
+ ensures forall{ IExpr sub in result; 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)
+ ensures forall{ IExpr sub in result; sub is IFunApp ==> !((IFunApp) sub).FunctionSymbol.Equals(Prop.Or) };
+ {
+ return BreakJuncts(e, Prop.Or);
+ }
+
+ private static IList/*<IExpr!>*/! BreakJuncts(IExpr! e, IFunctionSymbol! sym)
+ ensures forall{ IExpr sub in result; 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)
+ {
+ 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>
+ 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);*/;
+ }
+
+ /// <summary>
+ /// Like IPropExprFactory, but also with quantifiers.
+ /// </summary>
+ 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);*/;
+ }
+
+ /// <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>
+ 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);*/;
+ }
+
+ /// <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>
+ 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);*/ }
+ }
+
+ /// <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>
+ public interface IIntExprFactory : IValueExprFactory
+ {
+ IFunApp! Const(BigNum i) /*ensures result.FunctionSymbol.Equals(new IntSymbol(i));*/;
+ }
+
+ /// <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>
+ 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);*/;
+ }
+
+ /// <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>
+ 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);*/;
+ }
+
+}
|