diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-27 14:47:38 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-27 14:47:38 -0700 |
| commit | 764cd110aa83468a8f57b2dd8980f71ebee0a7af (patch) | |
| tree | d6fcbe50f7d85883dc1953365400afd8dba57b17 /Source | |
| parent | 7b4af4309de9ae134eac20af13a87f1036733e0d (diff) | |
Boogie: removed unreachable or unused code
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/AIFramework/CommonFunctionSymbols.cs | 2209 | ||||
| -rw-r--r-- | Source/AbsInt/AbstractInterpretation.cs | 10 | ||||
| -rw-r--r-- | Source/AbsInt/ExprFactories.cs | 47 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 2 |
4 files changed, 1083 insertions, 1185 deletions
diff --git a/Source/AIFramework/CommonFunctionSymbols.cs b/Source/AIFramework/CommonFunctionSymbols.cs index d8e4497f..6f7a9f93 100644 --- a/Source/AIFramework/CommonFunctionSymbols.cs +++ b/Source/AIFramework/CommonFunctionSymbols.cs @@ -5,1287 +5,1228 @@ //-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework
{
- using System.Diagnostics.Contracts;
- using System.Collections;
+ using System.Diagnostics.Contracts;
+ using System.Collections;
using System.Collections.Generic;
- //using Microsoft.SpecSharp.Collections;
- using Microsoft.Basetypes;
+ //using Microsoft.SpecSharp.Collections;
+ using Microsoft.Basetypes;
+
+ /// <summary>
+ /// A basic class for function symbols.
+ /// </summary>
+ public class FunctionSymbol : IFunctionSymbol
+ {
+ private readonly string/*!*/ display;
+ private readonly AIType/*!*/ typ;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(display != null);
+ Contract.Invariant(typ != null);
+ }
- /// <summary>
- /// A basic class for function symbols.
- /// </summary>
- public class FunctionSymbol : IFunctionSymbol
- {
- private readonly string/*!*/ display;
- private readonly AIType/*!*/ typ;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(display != null);
- Contract.Invariant(typ != null);
-}
+ public FunctionSymbol(AIType/*!*/ typ)
+ : this("FunctionSymbol", typ) {
+ Contract.Requires(typ != null);
+ }
- 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();
+ }
- internal FunctionSymbol(string/*!*/ display, AIType/*!*/ typ){
-Contract.Requires(typ != null);
-Contract.Requires(display != null);
- this.display = display;
- this.typ = typ;
- // base();
- }
+ public AIType/*!*/ AIType { get { Contract.Ensures(Contract.Result<AIType>() != null); return typ; } }
- public AIType/*!*/ AIType { get {Contract.Ensures(Contract.Result<AIType>() != null); return typ; } }
+ [NoDefaultContract]
+ [Pure]
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return display;
+ }
- [NoDefaultContract]
- [Pure]
- public override string/*!*/ ToString() {
-Contract.Ensures(Contract.Result<string>() != null);
- return display;
- }
+ }
+
+ /// <summary>
+ /// A class for integer constants.
+ /// </summary>
+ public class IntSymbol : FunctionSymbol
+ {
+ public readonly BigNum Value;
- }
-
/// <summary>
- /// A class for integer constants.
+ /// The intention is that this constructor be called only from the Int.Const method.
/// </summary>
- public class IntSymbol : FunctionSymbol
- {
- public readonly BigNum Value;
-
- /// <summary>
- /// The intention is that this constructor be called only from the Int.Const method.
- /// </summary>
- internal IntSymbol(BigNum x)
- : base(cce.NonNull(x.ToString()), Int.Type)
- {
- this.Value = x;
- }
+ 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();
- }
+ [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>
- /// A class for bitvector constants.
+ /// The intention is that this constructor be called only from the Int.Const method.
/// </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;
- }
- }
+ internal BvSymbol(BigNum x, int y)
+ : base(x + "bv" + y, Bv.Type) {
+ this.Value = x;
+ this.Bits = y;
}
- public class DoubleSymbol : FunctionSymbol
- {
- public readonly double Value;
-
- /// <summary>
- /// The intention is that this constructor be called only from the Double.Const method.
- /// </summary>
- internal DoubleSymbol(double x)
- : base(cce.NonNull(x.ToString()), Double.Type)
- {
- this.Value = x;
- }
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object other)
- {
- DoubleSymbol dsym = other as DoubleSymbol;
- return dsym != null && dsym.Value == this.Value;
- }
+ [Pure]
+ [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()
- {
- return Value.GetHashCode();
- }
+ [Pure]
+ public override int GetHashCode() {
+ unchecked {
+ return Value.GetHashCode() ^ Bits;
+ }
}
+ }
+
+ public class DoubleSymbol : FunctionSymbol
+ {
+ public readonly double Value;
/// <summary>
- /// Function symbol based on a string. Uses the string equality for determining equality
- /// of symbol.
+ /// The intention is that this constructor be called only from the Double.Const method.
/// </summary>
- public class NamedSymbol : FunctionSymbol
- {
- public string/*!*/ Value { [NoDefaultContract] get {Contract.Ensures(Contract.Result<string>() != null); return cce.NonNull(this.ToString()); } }
-
- public NamedSymbol(string/*!*/ symbol, AIType/*!*/ typ)
- : base(symbol, typ){
-Contract.Requires(typ != null);
-Contract.Requires(symbol != null);
- }
+ internal DoubleSymbol(double x)
+ : base(cce.NonNull(x.ToString()), Double.Type) {
+ this.Value = x;
+ }
- [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);
- }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object other) {
+ DoubleSymbol dsym = other as DoubleSymbol;
+ return dsym != null && dsym.Value == this.Value;
+ }
- [NoDefaultContract]
- [Pure]
- public override int GetHashCode()
- {
- return Value.GetHashCode();
- }
+ [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.
- //
+ /// <summary>
+ /// Function symbol based on a string. Uses the string equality for determining equality
+ /// of symbol.
+ /// </summary>
+ public class NamedSymbol : FunctionSymbol
+ {
+ public string/*!*/ Value { [NoDefaultContract] get { Contract.Ensures(Contract.Result<string>() != null); return cce.NonNull(this.ToString()); } }
+
+ public NamedSymbol(string/*!*/ symbol, AIType/*!*/ typ)
+ : base(symbol, typ) {
+ Contract.Requires(typ != null);
+ Contract.Requires(symbol != null);
+ }
- //-------------------------- Terms ----------------------------------
+ [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);
+ }
- /// <summary>
- /// A class with the equality symbol and the ValueType.Type.
- /// </summary>
- public class Value : AIType
- {
- private static readonly AIType/*!*/ valtype = new Value();
- public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return valtype; } }
-
- private static readonly FunctionType[]/*!*/ funtypeCache = new FunctionType[5];
- public static FunctionType/*!*/ FunctionType(int inParameterCount) {
-Contract.Requires((0 <= inParameterCount));
-Contract.Ensures(Contract.Result<FunctionType>() != null);
- // Contract.Ensures(Contract.Result<>().Arity == inParameterCount);
- FunctionType result;
- if (inParameterCount < funtypeCache.Length) {
- result = funtypeCache[inParameterCount];
- if (result != null) {
- return result;
- }
- }
- AIType[] signature = new AIType[1 + inParameterCount];
- for (int i = 0; i < signature.Length; i++) {
- signature[i] = valtype;
- }
- result = new FunctionType(signature);
- if (inParameterCount < funtypeCache.Length) {
- funtypeCache[inParameterCount] = result;
- }
- return result;
+ [NoDefaultContract]
+ [Pure]
+ public override int GetHashCode() {
+ return Value.GetHashCode();
+ }
+ }
+
+ //
+ // In the following, the classes like Value and Prop serve two
+ // roles. The primary role is to be the base types for AIType.
+ // The only objects of these classes are the representative
+ // objects that denote an AIType, which are given by the
+ // "Type" property. Subtypes in the AIType language are
+ // encoded by subclassing. This yields some "higher-orderness"
+ // for checking subtyping in the AIType language, by using
+ // the Spec#/C# subclassing checks.
+ //
+ // The other role is simply as a module for collecting like function
+ // symbols.
+ //
+
+ //-------------------------- Terms ----------------------------------
+
+ /// <summary>
+ /// A class with the equality symbol and the ValueType.Type.
+ /// </summary>
+ public class Value : AIType
+ {
+ private static readonly AIType/*!*/ valtype = new Value();
+ public static AIType/*!*/ Type { get { Contract.Ensures(Contract.Result<AIType>() != null); return valtype; } }
+
+ private static readonly FunctionType[]/*!*/ funtypeCache = new FunctionType[5];
+ public static FunctionType/*!*/ FunctionType(int inParameterCount) {
+ Contract.Requires((0 <= inParameterCount));
+ Contract.Ensures(Contract.Result<FunctionType>() != null);
+ // Contract.Ensures(Contract.Result<>().Arity == inParameterCount);
+ FunctionType result;
+ if (inParameterCount < funtypeCache.Length) {
+ result = funtypeCache[inParameterCount];
+ if (result != null) {
+ return result;
}
+ }
+ AIType[] signature = new AIType[1 + inParameterCount];
+ for (int i = 0; i < signature.Length; i++) {
+ signature[i] = valtype;
+ }
+ result = new FunctionType(signature);
+ if (inParameterCount < funtypeCache.Length) {
+ funtypeCache[inParameterCount] = result;
+ }
+ return result;
+ }
- [Once] private static AIType/*!*/ binreltype;
+ [Once]
+ private static AIType/*!*/ binreltype;
- private static AIType/*!*/ BinrelType {
- get {Contract.Ensures(Contract.Result<AIType>() != null);
- if (binreltype == null) {
- binreltype = new FunctionType(Type, Type, Prop.Type);
- }
- return binreltype;
- }
+ private static AIType/*!*/ BinrelType {
+ get {
+ Contract.Ensures(Contract.Result<AIType>() != null);
+ if (binreltype == null) {
+ binreltype = new FunctionType(Type, Type, Prop.Type);
}
+ return binreltype;
+ }
+ }
- [Once] private static FunctionSymbol/*!*/ _eq;
- public static FunctionSymbol/*!*/ Eq {
- get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
- if (_eq == null) {
- _eq = new FunctionSymbol("=", BinrelType);
- }
- return _eq;
- }
+ [Once]
+ private static FunctionSymbol/*!*/ _eq;
+ public static FunctionSymbol/*!*/ Eq {
+ get {
+ Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
+ if (_eq == null) {
+ _eq = new FunctionSymbol("=", BinrelType);
}
- [Once] private static FunctionSymbol/*!*/ _neq;
- public static FunctionSymbol/*!*/ Neq {
- get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
- if (_neq == null) {
- _neq = new FunctionSymbol("!=", BinrelType);
- }
- return _neq;
- }
+ return _eq;
+ }
+ }
+ [Once]
+ private static FunctionSymbol/*!*/ _neq;
+ public static FunctionSymbol/*!*/ Neq {
+ get {
+ Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
+ if (_neq == null) {
+ _neq = new FunctionSymbol("!=", BinrelType);
}
- [Once] private static FunctionSymbol/*!*/ _subtype;
- public static FunctionSymbol/*!*/ Subtype {
- get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
- if (_subtype == null) {
- _subtype = new FunctionSymbol("<:", BinrelType);
- }
- return _subtype;
- }
+ return _neq;
+ }
+ }
+ [Once]
+ private static FunctionSymbol/*!*/ _subtype;
+ public static FunctionSymbol/*!*/ Subtype {
+ get {
+ Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
+ if (_subtype == null) {
+ _subtype = new FunctionSymbol("<:", BinrelType);
}
+ return _subtype;
+ }
+ }
- [Once] private static AIType/*!*/ typeof_type;
- private static AIType/*!*/ TypeofType {
- get {Contract.Ensures(Contract.Result<AIType>() != null);
- if (typeof_type == null) {
- typeof_type = new FunctionType(Ref.Type, Type);
- }
- return typeof_type;
- }
+ [Once]
+ private static AIType/*!*/ typeof_type;
+ private static AIType/*!*/ TypeofType {
+ get {
+ Contract.Ensures(Contract.Result<AIType>() != null);
+ if (typeof_type == null) {
+ typeof_type = new FunctionType(Ref.Type, Type);
}
- [Once] private static FunctionSymbol/*!*/ _typeof;
- public static FunctionSymbol/*!*/ Typeof {
- get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
- if (_typeof == null) {
- _typeof = new FunctionSymbol("typeof", TypeofType);
- }
- return _typeof;
- }
- }
-
- /// <summary>
- /// Value should not be instantiated from the outside, except perhaps in
- /// subclasses.
- /// </summary>
- protected Value() { }
-
- }
-
- public class Int : Value
- {
- private static readonly AIType/*!*/ inttype = new Int();
- public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return inttype; } }
-
- private static readonly AIType/*!*/ unaryinttype = new FunctionType(Type, Type);
- private static readonly AIType/*!*/ bininttype = new FunctionType(Type, Type, Type);
- private static readonly AIType/*!*/ relationtype = new FunctionType(Type, Type, Prop.Type);
-
- private static readonly FunctionSymbol/*!*/ _negate = new FunctionSymbol("~", unaryinttype);
- private static readonly FunctionSymbol/*!*/ _add = new FunctionSymbol("+", bininttype);
- private static readonly FunctionSymbol/*!*/ _sub = new FunctionSymbol("-", bininttype);
- private static readonly FunctionSymbol/*!*/ _mul = new FunctionSymbol("*", bininttype);
- private static readonly FunctionSymbol/*!*/ _div = new FunctionSymbol("/", bininttype);
- private static readonly FunctionSymbol/*!*/ _mod = new FunctionSymbol("%", bininttype);
- private static readonly FunctionSymbol/*!*/ _atmost = new FunctionSymbol("<=", relationtype);
- private static readonly FunctionSymbol/*!*/ _less = new FunctionSymbol("<", relationtype);
- private static readonly FunctionSymbol/*!*/ _greater = new FunctionSymbol(">", relationtype);
- private static readonly FunctionSymbol/*!*/ _atleast = new FunctionSymbol(">=", relationtype);
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Negate { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _negate; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Add { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _add; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Sub { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _sub; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Mul { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _mul; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Div { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _div; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Mod { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _mod; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ AtMost { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atmost; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Less { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _less; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Greater { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _greater; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ AtLeast { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atleast; } }
-
- public static IntSymbol/*!*/ Const(BigNum x) {
-Contract.Ensures(Contract.Result<IntSymbol>() != null);
- // We could cache things here, but for now we don't.
- return new IntSymbol(x);
+ return typeof_type;
+ }
+ }
+ [Once]
+ private static FunctionSymbol/*!*/ _typeof;
+ public static FunctionSymbol/*!*/ Typeof {
+ get {
+ Contract.Ensures(Contract.Result<FunctionSymbol>() != null);
+ if (_typeof == null) {
+ _typeof = new FunctionSymbol("typeof", TypeofType);
}
+ return _typeof;
+ }
+ }
- /// <summary>
- /// Int should not be instantiated from the outside, except perhaps in
- /// subclasses.
- /// </summary>
- private Int() { }
- }
-
- public class Double : Value
- {
- private static readonly AIType/*!*/ doubletype = new Double();
- public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return doubletype; } }
-
- public static DoubleSymbol/*!*/ Const(double x) {
-Contract.Ensures(Contract.Result<DoubleSymbol>() != null);
- // We could cache things here, but for now we don't.
- return new DoubleSymbol(x);
- }
+ /// <summary>
+ /// Value should not be instantiated from the outside, except perhaps in
+ /// subclasses.
+ /// </summary>
+ protected Value() { }
- /// <summary>
- /// Double should not be instantiated from the outside, except perhaps in
- /// subclasses.
- /// </summary>
- private Double() { }
- }
-
- public class Bv : Value
- {
- private static readonly AIType/*!*/ bvtype = new Bv();
- public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return bvtype; } }
-
- private static readonly AIType/*!*/ unaryinttype = new FunctionType(Type, Type);
- private static readonly AIType/*!*/ bininttype = new FunctionType(Type, Type, Type);
- private static readonly AIType/*!*/ relationtype = new FunctionType(Type, Type, Prop.Type);
-
- private static readonly FunctionSymbol/*!*/ _negate = new FunctionSymbol("~", unaryinttype);
- private static readonly FunctionSymbol/*!*/ _add = new FunctionSymbol("+", bininttype);
- private static readonly FunctionSymbol/*!*/ _sub = new FunctionSymbol("-", bininttype);
- private static readonly FunctionSymbol/*!*/ _mul = new FunctionSymbol("*", bininttype);
- private static readonly FunctionSymbol/*!*/ _div = new FunctionSymbol("/", bininttype);
- private static readonly FunctionSymbol/*!*/ _mod = new FunctionSymbol("%", bininttype);
- private static readonly FunctionSymbol/*!*/ _concat = new FunctionSymbol("$concat", bininttype);
- private static readonly FunctionSymbol/*!*/ _extract = new FunctionSymbol("$extract", unaryinttype);
- private static readonly FunctionSymbol/*!*/ _atmost = new FunctionSymbol("<=", relationtype);
- private static readonly FunctionSymbol/*!*/ _less = new FunctionSymbol("<", relationtype);
- private static readonly FunctionSymbol/*!*/ _greater = new FunctionSymbol(">", relationtype);
- private static readonly FunctionSymbol/*!*/ _atleast = new FunctionSymbol(">=", relationtype);
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Negate { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _negate; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Add { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _add; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Sub { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _sub; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Mul { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _mul; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Div { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _div; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Mod { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null);return _mod; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ AtMost { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atmost; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Less { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _less; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Greater { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _greater; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ AtLeast { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atleast; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Extract { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _extract; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Concat { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _concat; } }
-
- public static BvSymbol/*!*/ Const(BigNum x, int y) {
-Contract.Ensures(Contract.Result<BvSymbol>() != null);
- // We could cache things here, but for now we don't.
- return new BvSymbol(x, y);
- }
+ }
- /// <summary>
- /// Int should not be instantiated from the outside, except perhaps in
- /// subclasses.
- /// </summary>
- private Bv() { }
+ public class Int : Value
+ {
+ private static readonly AIType/*!*/ inttype = new Int();
+ public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result<AIType>() != null); return inttype; } }
+
+ private static readonly AIType/*!*/ unaryinttype = new FunctionType(Type, Type);
+ private static readonly AIType/*!*/ bininttype = new FunctionType(Type, Type, Type);
+ private static readonly AIType/*!*/ relationtype = new FunctionType(Type, Type, Prop.Type);
+
+ private static readonly FunctionSymbol/*!*/ _negate = new FunctionSymbol("~", unaryinttype);
+ private static readonly FunctionSymbol/*!*/ _add = new FunctionSymbol("+", bininttype);
+ private static readonly FunctionSymbol/*!*/ _sub = new FunctionSymbol("-", bininttype);
+ private static readonly FunctionSymbol/*!*/ _mul = new FunctionSymbol("*", bininttype);
+ private static readonly FunctionSymbol/*!*/ _div = new FunctionSymbol("/", bininttype);
+ private static readonly FunctionSymbol/*!*/ _mod = new FunctionSymbol("%", bininttype);
+ private static readonly FunctionSymbol/*!*/ _atmost = new FunctionSymbol("<=", relationtype);
+ private static readonly FunctionSymbol/*!*/ _less = new FunctionSymbol("<", relationtype);
+ private static readonly FunctionSymbol/*!*/ _greater = new FunctionSymbol(">", relationtype);
+ private static readonly FunctionSymbol/*!*/ _atleast = new FunctionSymbol(">=", relationtype);
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Negate { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _negate; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Add { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _add; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Sub { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _sub; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Mul { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _mul; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Div { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _div; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Mod { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _mod; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ AtMost { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atmost; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Less { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _less; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Greater { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _greater; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ AtLeast { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atleast; } }
+
+ public static IntSymbol/*!*/ Const(BigNum x) {
+ Contract.Ensures(Contract.Result<IntSymbol>() != null);
+ // We could cache things here, but for now we don't.
+ return new IntSymbol(x);
}
- public class Ref : Value
- {
- private static readonly AIType/*!*/ reftype = new Ref();
- public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return reftype; } }
-
- private static readonly FunctionSymbol/*!*/ _null = new FunctionSymbol("null", Type);
+ /// <summary>
+ /// Int should not be instantiated from the outside, except perhaps in
+ /// subclasses.
+ /// </summary>
+ private Int() { }
+ }
- public static FunctionSymbol/*!*/ Null { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _null; } }
+ public class Double : Value
+ {
+ private static readonly AIType/*!*/ doubletype = new Double();
+ public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result<AIType>() != null); return doubletype; } }
- /// <summary>
- /// Ref should not be instantiated from the outside, except perhaps in
- /// subclasses.
- /// </summary>
- private Ref() { }
+ public static DoubleSymbol/*!*/ Const(double x) {
+ Contract.Ensures(Contract.Result<DoubleSymbol>() != null);
+ // We could cache things here, but for now we don't.
+ return new DoubleSymbol(x);
}
- public class HeapStructure : Value
- {
- private static readonly AIType/*!*/ reftype = new HeapStructure();
- public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return reftype; } }
-
-
+ /// <summary>
+ /// Double should not be instantiated from the outside, except perhaps in
+ /// subclasses.
+ /// </summary>
+ private Double() { }
+ }
- /// <summary>
- /// HeapStructure should not be instantiated from the outside, except perhaps in
- /// subclasses.
- /// </summary>
- private HeapStructure() { }
+ public class Bv : Value
+ {
+ private static readonly AIType/*!*/ bvtype = new Bv();
+ public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result<AIType>() != null); return bvtype; } }
+
+ private static readonly AIType/*!*/ unaryinttype = new FunctionType(Type, Type);
+ private static readonly AIType/*!*/ bininttype = new FunctionType(Type, Type, Type);
+ private static readonly AIType/*!*/ relationtype = new FunctionType(Type, Type, Prop.Type);
+
+ private static readonly FunctionSymbol/*!*/ _negate = new FunctionSymbol("~", unaryinttype);
+ private static readonly FunctionSymbol/*!*/ _add = new FunctionSymbol("+", bininttype);
+ private static readonly FunctionSymbol/*!*/ _sub = new FunctionSymbol("-", bininttype);
+ private static readonly FunctionSymbol/*!*/ _mul = new FunctionSymbol("*", bininttype);
+ private static readonly FunctionSymbol/*!*/ _div = new FunctionSymbol("/", bininttype);
+ private static readonly FunctionSymbol/*!*/ _mod = new FunctionSymbol("%", bininttype);
+ private static readonly FunctionSymbol/*!*/ _concat = new FunctionSymbol("$concat", bininttype);
+ private static readonly FunctionSymbol/*!*/ _extract = new FunctionSymbol("$extract", unaryinttype);
+ private static readonly FunctionSymbol/*!*/ _atmost = new FunctionSymbol("<=", relationtype);
+ private static readonly FunctionSymbol/*!*/ _less = new FunctionSymbol("<", relationtype);
+ private static readonly FunctionSymbol/*!*/ _greater = new FunctionSymbol(">", relationtype);
+ private static readonly FunctionSymbol/*!*/ _atleast = new FunctionSymbol(">=", relationtype);
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Negate { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _negate; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Add { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _add; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Sub { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _sub; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Mul { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _mul; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Div { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _div; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Mod { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _mod; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ AtMost { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atmost; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Less { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _less; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Greater { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _greater; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ AtLeast { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _atleast; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Extract { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _extract; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Concat { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _concat; } }
+
+ public static BvSymbol/*!*/ Const(BigNum x, int y) {
+ Contract.Ensures(Contract.Result<BvSymbol>() != null);
+ // We could cache things here, but for now we don't.
+ return new BvSymbol(x, y);
}
- public class FieldName : Value
- {
- private static readonly AIType/*!*/ fieldnametype = new FieldName();
- public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return fieldnametype; } }
+ /// <summary>
+ /// Int should not be instantiated from the outside, except perhaps in
+ /// subclasses.
+ /// </summary>
+ private Bv() { }
+ }
- private static readonly FunctionSymbol/*!*/ _allocated = new FunctionSymbol("$allocated", FieldName.Type);
- public static FunctionSymbol/*!*/ Allocated { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _allocated; } }
+ public class Ref : Value
+ {
+ private static readonly AIType/*!*/ reftype = new Ref();
+ public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result<AIType>() != null); return reftype; } }
- /// <summary>
- /// Is this a boolean field that monotonically goes from false to true?
- /// </summary>
- public static bool IsBooleanMonotonicallyWeakening(IFunctionSymbol/*!*/ f){
-Contract.Requires(f != null);
- return f.Equals(Allocated);
- }
+ private static readonly FunctionSymbol/*!*/ _null = new FunctionSymbol("null", Type);
- /// <summary>
- /// FieldName should not be instantiated from the outside, except perhaps in
- /// subclasses.
- /// </summary>
- private FieldName() { }
- }
-
- public class Heap : Value
- {
- private static readonly AIType/*!*/ heaptype = new Heap();
- public static new AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return heaptype; } }
-
- // the types in the following, select1, select2, are hard-coded;
- // these types may not always be appropriate
- private static readonly FunctionSymbol/*!*/ _select1 = new FunctionSymbol("sel1",
- // Heap x FieldName -> Prop
- new FunctionType(Type, FieldName.Type, Prop.Type)
- );
- public static FunctionSymbol/*!*/ Select1 { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _select1; } }
-
- private static readonly FunctionSymbol/*!*/ _select2 = new FunctionSymbol("sel2",
- // Heap x Ref x FieldName -> Value
- new FunctionType(Type, Ref.Type, FieldName.Type, Value.Type)
- );
- public static FunctionSymbol/*!*/ Select2 { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _select2; } }
-
- // the types in the following, store1, store2, are hard-coded;
- // these types may not always be appropriate
- private static readonly FunctionSymbol/*!*/ _update1 = new FunctionSymbol("upd1",
- // Heap x FieldName x Value -> Heap
- new FunctionType(Type, FieldName.Type, Value.Type, Type)
- );
- public static FunctionSymbol/*!*/ Update1 { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _update1; } }
-
- private static readonly FunctionSymbol/*!*/ _update2 = new FunctionSymbol("upd2",
- // Heap x Ref x FieldName x Value -> Heap
- new FunctionType(Type, Ref.Type, FieldName.Type, Value.Type, Type)
- );
- public static FunctionSymbol/*!*/ Update2 { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _update2; } }
-
- private static readonly FunctionSymbol/*!*/ _unsupportedHeapOp =
- new FunctionSymbol("UnsupportedHeapOp",
- // Heap x FieldName -> Prop
- new FunctionType(Type, FieldName.Type, Prop.Type)
- );
- public static FunctionSymbol/*!*/ UnsupportedHeapOp { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _unsupportedHeapOp; } }
-
- /// <summary>
- /// Heap should not be instantiated from the outside, except perhaps in
- /// subclasses.
- /// </summary>
- private Heap() { }
- }
-
-// public class List : Value
-// {
-// private static IDictionary/*<AIType!,AIType!>*/! lists = new Hashtable();
-// public static AIType! Type(AIType! typeParameter)
-// {
-// if (lists.Contains(typeParameter))
-// return lists[typeParameter];
-// else
-// {
-// AIType! result = new List(typeParameter);
-// lists[typeParameter] = result;
-// return result;
-// }
-// }
-//
-// private static IDictionary/*<AIType!,AIType!>*/! nils = new Hashtable();
-// public static FunctionSymbol! Nil(AIType! typeParameter)
-// {
-// if (nils.Contains(typeParameter))
-// return nils[typeParameter];
-// else
-// {
-// FunctionSymbol! result = new FunctionSymbol(Type(typeParameter));
-// nils[typeParameter] = result;
-// return result;
-// }
-// }
-//
-// private static IDictionary/*<AIType!,AIType!>*/! cons = new Hashtable();
-// public static FunctionSymbol! Cons(AIType! typeParameter)
-// {
-// if (cons.Contains(typeParameter))
-// return cons[typeParameter];
-// else
-// {
-// FunctionSymbol! result = new FunctionSymbol(
-// new FunctionType(typeParameter, Type(typeParameter), Type(typeParameter))
-// );
-// cons[typeParameter] = result;
-// return result;
-// }
-// }
-//
-// private AIType! typeParameter;
-// public AIType(TypeParameter/*!*/ ){
-//Contract.Requires( != null);
- //return typeParameter; } }
-//
-// /// <summary>
-// /// List should not be instantiated from the outside.
-// /// </summary>
-// private List(AIType! typeParameter)
-// {
-// this.typeParameter = typeParameter;
-// }
-// }
-//
-// public class Pair : Value
-// {
-// private static IDictionary! pairs = new Hashtable();
-// public static AIType! Type(AIType! type1, AIType! type2)
-// {
-// Microsoft.AbstractInterpretationFramework.Collections.Pair typpair
-// = new Microsoft.AbstractInterpretationFramework.Collections.Pair(type1, type2);
-//
-// if (pairs.Contains(typpair))
-// return pairs[typpair];
-// else
-// {
-// AIType! result = new Pair(type1, type2);
-// pairs[typpair] = result;
-// return result;
-// }
-// }
-//
-// private static IDictionary! constructs = new Hashtable();
-// public static FunctionSymbol! Pair(AIType! type1, AIType! type2)
-// {
-// Microsoft.AbstractInterpretationFramework.Collections.Pair typpair
-// = new Microsoft.AbstractInterpretationFramework.Collections.Pair(type1, type2);
-//
-// if (constructs.Contains(typpair))
-// return constructs[typpair];
-// else
-// {
-// FunctionSymbol! result = new FunctionSymbol(
-// new FunctionType(type1, type2, Type(type1, type2))
-// );
-// constructs[typpair] = result;
-// return result;
-// }
-// }
-//
-// protected AIType! type1;
-// protected AIType! type2;
-//
-// public AIType(Type1/*!*/ ){
-//Contract.Requires( != null);
-// return type1; } }
-// public AIType(Type2/*!*/ ){
-//Contract.Requires( != null);
-// return type2; } }
-//
-// /// <summary>
-// /// Pair should not be instantiated from the outside, except by subclasses.
-// /// </summary>
-// protected Pair(AIType! type1, AIType! type2)
-// {
-// this.type1 = type1;
-// this.type2 = type2;
-// }
-// }
+ public static FunctionSymbol/*!*/ Null { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _null; } }
+
+ /// <summary>
+ /// Ref should not be instantiated from the outside, except perhaps in
+ /// subclasses.
+ /// </summary>
+ private Ref() { }
+ }
+
+ public class HeapStructure : Value
+ {
+ private static readonly AIType/*!*/ reftype = new HeapStructure();
+ public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result<AIType>() != null); return reftype; } }
- //-------------------------- Propositions ---------------------------
/// <summary>
- /// A class with global propositional symbols and the Prop.Type.
+ /// HeapStructure should not be instantiated from the outside, except perhaps in
+ /// subclasses.
/// </summary>
- public sealed class Prop : AIType
- {
- private static readonly AIType/*!*/ proptype = new Prop();
-
- public static AIType/*!*/ Type { get {Contract.Ensures(Contract.Result<AIType>() != null); return proptype; } }
-
- private static readonly AIType/*!*/ unaryproptype = new FunctionType(Type, Type);
- private static readonly AIType/*!*/ binproptype = new FunctionType(Type, Type, Type);
- private static readonly AIType/*!*/ quantifiertype =
- new FunctionType(new FunctionType(Value.Type, Type), Type);
-
- private static readonly FunctionSymbol/*!*/ _false = new FunctionSymbol("false", Type);
- private static readonly FunctionSymbol/*!*/ _true = new FunctionSymbol("true", Type);
- private static readonly FunctionSymbol/*!*/ _not = new FunctionSymbol("!", unaryproptype);
- private static readonly FunctionSymbol/*!*/ _and = new FunctionSymbol("/\\", binproptype);
- private static readonly FunctionSymbol/*!*/ _or = new FunctionSymbol("\\/", binproptype);
- private static readonly FunctionSymbol/*!*/ _implies = new FunctionSymbol("==>", binproptype);
- private static readonly FunctionSymbol/*!*/ _exists = new FunctionSymbol("Exists", quantifiertype);
- private static readonly FunctionSymbol/*!*/ _forall = new FunctionSymbol("Forall", quantifiertype);
- private static readonly FunctionSymbol/*!*/ _lambda = new FunctionSymbol("Lambda", quantifiertype);
-
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ False { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _false; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ True { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _true; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Not { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _not; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ And { [Pure] get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _and; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Or { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _or; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Implies { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _implies; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Exists { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _exists; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Forall { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _forall; } }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol/*!*/ Lambda { get {Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _lambda; } }
-
-
- /// <summary>
- /// Prop should not be instantiated from the outside.
- /// </summary>
- private Prop() { }
-
-
-
- //
- // Utility Methods
- //
-
- public static IExpr/*!*/ SimplifiedAnd(IPropExprFactory/*!*/ factory, IExpr/*!*/ e0, IExpr/*!*/ e1){
-Contract.Requires(e1 != null);
-Contract.Requires(e0 != null);
-Contract.Requires(factory != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
- IFunApp fun0 = e0 as IFunApp;
- if (fun0 != null)
- {
- if (fun0.FunctionSymbol.Equals(Prop.True))
- {
- return e1;
- }
- else if (fun0.FunctionSymbol.Equals(Prop.False))
- {
- return e0;
- }
- }
-
- IFunApp fun1 = e1 as IFunApp;
- if (fun1 != null)
- {
- if (fun1.FunctionSymbol.Equals(Prop.True))
- {
- return e0;
- }
- else if (fun1.FunctionSymbol.Equals(Prop.False))
- {
- return e1;
- }
- }
-
- return factory.And(e0, e1);
- }
-
- public static IExpr/*!*/ SimplifiedAnd(IPropExprFactory/*!*/ factory, IEnumerable/*<IExpr!>*//*!*/ exprs){
-Contract.Requires(exprs != null);
-Contract.Requires(factory != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
-IExpr/*!*/ result = factory.True;
-Contract.Assert(result != null);
- foreach(IExpr/*!*/ conjunct in exprs){
-Contract.Assert(conjunct != null);
- result = SimplifiedAnd(factory, result, conjunct);
- }
- return result;
- }
+ private HeapStructure() { }
+ }
- public static IExpr/*!*/ SimplifiedOr(IPropExprFactory/*!*/ factory, IExpr/*!*/ e0, IExpr/*!*/ e1){
-Contract.Requires(e1 != null);
-Contract.Requires(e0 != null);
-Contract.Requires(factory != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
- IFunApp fun0 = e0 as IFunApp;
- if (fun0 != null)
- {
- if (fun0.FunctionSymbol.Equals(Prop.False))
- {
- return e1;
- }
- else if (fun0.FunctionSymbol.Equals(Prop.True))
- {
- return e0;
- }
- }
-
- IFunApp fun1 = e1 as IFunApp;
- if (fun1 != null)
- {
- if (fun1.FunctionSymbol.Equals(Prop.False))
- {
- return e0;
- }
- else if (fun1.FunctionSymbol.Equals(Prop.True))
- {
- return e1;
- }
- }
-
- return factory.Or(e0, e1);
- }
-
- public static IExpr/*!*/ SimplifiedOr(IPropExprFactory/*!*/ factory, IEnumerable/*<IExpr!>*//*!*/ exprs){
-Contract.Requires(exprs != null);
-Contract.Requires(factory != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
-IExpr/*!*/ result = factory.False;
-Contract.Assert(result != null);
- foreach(IExpr/*!*/ disj in exprs){
-Contract.Assert(disj != null);
- result = SimplifiedOr(factory, result, disj);
- }
- return result;
- }
+ public class FieldName : Value
+ {
+ private static readonly AIType/*!*/ fieldnametype = new FieldName();
+ public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result<AIType>() != null); return fieldnametype; } }
+ private static readonly FunctionSymbol/*!*/ _allocated = new FunctionSymbol("$allocated", FieldName.Type);
+ public static FunctionSymbol/*!*/ Allocated { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _allocated; } }
+ /// <summary>
+ /// Is this a boolean field that monotonically goes from false to true?
+ /// </summary>
+ public static bool IsBooleanMonotonicallyWeakening(IFunctionSymbol/*!*/ f) {
+ Contract.Requires(f != null);
+ return f.Equals(Allocated);
+ }
- /// <summary>
- /// Break top-level conjuncts into a list of sub-expressions.
- /// </summary>
- /// <param name="e">The expression to examine.</param>
- /// <returns>A list of conjuncts.</returns>
- internal static IList/*<IExpr!>*//*!*/ BreakConjuncts(IExpr/*!*/ e){
-Contract.Requires(e != null);
- Contract.Ensures(Contract.Result<IList>() != null);
- Contract.Ensures(Contract.ForAll(0, Contract.Result<IList>().Count, i => {
- var sub = Contract.Result<IList>()[i];
- return !(sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(Prop.And);
- }));
- return BreakJuncts(e, Prop.And);
- }
+ /// <summary>
+ /// FieldName should not be instantiated from the outside, except perhaps in
+ /// subclasses.
+ /// </summary>
+ private FieldName() { }
+ }
- /// <summary>
- /// Break top-level disjuncts into a list of sub-expressions.
- /// </summary>
- /// <param name="e">The expression to examine.</param>
- /// <returns>A list of conjuncts.</returns>
- internal static IList/*<IExpr!>*//*!*/ BreakDisjuncts(IExpr/*!*/ e){
-Contract.Requires(e != null);
- Contract.Ensures(Contract.Result<IList>() != null);
- Contract.Ensures(Contract.ForAll(0, Contract.Result<IList>().Count, i => {
- var sub = Contract.Result<IList>()[i];
- return !(sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(Prop.Or);
- }));
- return BreakJuncts(e, Prop.Or);
- }
-
- private static IList/*<IExpr!>*//*!*/ BreakJuncts(IExpr/*!*/ e, IFunctionSymbol/*!*/ sym){
-Contract.Requires(sym != null);
-Contract.Requires(e != null);
- Contract.Ensures(Contract.Result<IList>() != null);
- Contract.Ensures(Contract.ForAll(0, Contract.Result<IList>().Count, i => {
- var sub = Contract.Result<IList>()[i];
- return (sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(sym);
- }));
- ArrayList/*<IExpr!>*//*!*/ result = new ArrayList();
-
- IFunApp f = e as IFunApp;
- if (f != null)
- {
- // If it is a sym, go down into sub-expressions.
- if (f.FunctionSymbol.Equals(sym))
- {
- foreach(IExpr/*!*/ arg in f.Arguments){
-Contract.Assert(arg != null);
- result.AddRange(BreakJuncts(arg,sym));
- }
- }
- // Otherwise, stop.
- else
- {
- result.Add(e);
- }
- }
- else
- {
- result.Add(e);
- }
-
- return result;
- }
- }
+ public class Heap : Value
+ {
+ private static readonly AIType/*!*/ heaptype = new Heap();
+ public static new AIType/*!*/ Type { get { Contract.Ensures(Contract.Result<AIType>() != null); return heaptype; } }
+
+ // the types in the following, select1, select2, are hard-coded;
+ // these types may not always be appropriate
+ private static readonly FunctionSymbol/*!*/ _select1 = new FunctionSymbol("sel1",
+ // Heap x FieldName -> Prop
+ new FunctionType(Type, FieldName.Type, Prop.Type)
+ );
+ public static FunctionSymbol/*!*/ Select1 { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _select1; } }
+
+ private static readonly FunctionSymbol/*!*/ _select2 = new FunctionSymbol("sel2",
+ // Heap x Ref x FieldName -> Value
+ new FunctionType(Type, Ref.Type, FieldName.Type, Value.Type)
+ );
+ public static FunctionSymbol/*!*/ Select2 { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _select2; } }
+
+ // the types in the following, store1, store2, are hard-coded;
+ // these types may not always be appropriate
+ private static readonly FunctionSymbol/*!*/ _update1 = new FunctionSymbol("upd1",
+ // Heap x FieldName x Value -> Heap
+ new FunctionType(Type, FieldName.Type, Value.Type, Type)
+ );
+ public static FunctionSymbol/*!*/ Update1 { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _update1; } }
+
+ private static readonly FunctionSymbol/*!*/ _update2 = new FunctionSymbol("upd2",
+ // Heap x Ref x FieldName x Value -> Heap
+ new FunctionType(Type, Ref.Type, FieldName.Type, Value.Type, Type)
+ );
+ public static FunctionSymbol/*!*/ Update2 { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _update2; } }
+
+ private static readonly FunctionSymbol/*!*/ _unsupportedHeapOp =
+ new FunctionSymbol("UnsupportedHeapOp",
+ // Heap x FieldName -> Prop
+ new FunctionType(Type, FieldName.Type, Prop.Type)
+ );
+ public static FunctionSymbol/*!*/ UnsupportedHeapOp { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _unsupportedHeapOp; } }
/// <summary>
- /// A callback to produce a function body given the bound variable.
+ /// Heap should not be instantiated from the outside, except perhaps in
+ /// subclasses.
/// </summary>
- /// <param name="var">The bound variable to use.</param>
- /// <returns>The function body.</returns>
- public delegate IExpr/*!*/ FunctionBody(IVariable/*!*/ var);
+ private Heap() { }
+ }
+
+ // public class List : Value
+ // {
+ // private static IDictionary/*<AIType!,AIType!>*/! lists = new Hashtable();
+ // public static AIType! Type(AIType! typeParameter)
+ // {
+ // if (lists.Contains(typeParameter))
+ // return lists[typeParameter];
+ // else
+ // {
+ // AIType! result = new List(typeParameter);
+ // lists[typeParameter] = result;
+ // return result;
+ // }
+ // }
+ //
+ // private static IDictionary/*<AIType!,AIType!>*/! nils = new Hashtable();
+ // public static FunctionSymbol! Nil(AIType! typeParameter)
+ // {
+ // if (nils.Contains(typeParameter))
+ // return nils[typeParameter];
+ // else
+ // {
+ // FunctionSymbol! result = new FunctionSymbol(Type(typeParameter));
+ // nils[typeParameter] = result;
+ // return result;
+ // }
+ // }
+ //
+ // private static IDictionary/*<AIType!,AIType!>*/! cons = new Hashtable();
+ // public static FunctionSymbol! Cons(AIType! typeParameter)
+ // {
+ // if (cons.Contains(typeParameter))
+ // return cons[typeParameter];
+ // else
+ // {
+ // FunctionSymbol! result = new FunctionSymbol(
+ // new FunctionType(typeParameter, Type(typeParameter), Type(typeParameter))
+ // );
+ // cons[typeParameter] = result;
+ // return result;
+ // }
+ // }
+ //
+ // private AIType! typeParameter;
+ // public AIType(TypeParameter/*!*/ ){
+ //Contract.Requires( != null);
+ //return typeParameter; } }
+ //
+ // /// <summary>
+ // /// List should not be instantiated from the outside.
+ // /// </summary>
+ // private List(AIType! typeParameter)
+ // {
+ // this.typeParameter = typeParameter;
+ // }
+ // }
+ //
+ // public class Pair : Value
+ // {
+ // private static IDictionary! pairs = new Hashtable();
+ // public static AIType! Type(AIType! type1, AIType! type2)
+ // {
+ // Microsoft.AbstractInterpretationFramework.Collections.Pair typpair
+ // = new Microsoft.AbstractInterpretationFramework.Collections.Pair(type1, type2);
+ //
+ // if (pairs.Contains(typpair))
+ // return pairs[typpair];
+ // else
+ // {
+ // AIType! result = new Pair(type1, type2);
+ // pairs[typpair] = result;
+ // return result;
+ // }
+ // }
+ //
+ // private static IDictionary! constructs = new Hashtable();
+ // public static FunctionSymbol! Pair(AIType! type1, AIType! type2)
+ // {
+ // Microsoft.AbstractInterpretationFramework.Collections.Pair typpair
+ // = new Microsoft.AbstractInterpretationFramework.Collections.Pair(type1, type2);
+ //
+ // if (constructs.Contains(typpair))
+ // return constructs[typpair];
+ // else
+ // {
+ // FunctionSymbol! result = new FunctionSymbol(
+ // new FunctionType(type1, type2, Type(type1, type2))
+ // );
+ // constructs[typpair] = result;
+ // return result;
+ // }
+ // }
+ //
+ // protected AIType! type1;
+ // protected AIType! type2;
+ //
+ // public AIType(Type1/*!*/ ){
+ //Contract.Requires( != null);
+ // return type1; } }
+ // public AIType(Type2/*!*/ ){
+ //Contract.Requires( != null);
+ // return type2; } }
+ //
+ // /// <summary>
+ // /// Pair should not be instantiated from the outside, except by subclasses.
+ // /// </summary>
+ // protected Pair(AIType! type1, AIType! type2)
+ // {
+ // this.type1 = type1;
+ // this.type2 = type2;
+ // }
+ // }
+
+ //-------------------------- Propositions ---------------------------
+
+
+ /// <summary>
+ /// A class with global propositional symbols and the Prop.Type.
+ /// </summary>
+ public sealed class Prop : AIType
+ {
+ private static readonly AIType/*!*/ proptype = new Prop();
+
+ public static AIType/*!*/ Type { get { Contract.Ensures(Contract.Result<AIType>() != null); return proptype; } }
+
+ private static readonly AIType/*!*/ unaryproptype = new FunctionType(Type, Type);
+ private static readonly AIType/*!*/ binproptype = new FunctionType(Type, Type, Type);
+ private static readonly AIType/*!*/ quantifiertype =
+ new FunctionType(new FunctionType(Value.Type, Type), Type);
+
+ private static readonly FunctionSymbol/*!*/ _false = new FunctionSymbol("false", Type);
+ private static readonly FunctionSymbol/*!*/ _true = new FunctionSymbol("true", Type);
+ private static readonly FunctionSymbol/*!*/ _not = new FunctionSymbol("!", unaryproptype);
+ private static readonly FunctionSymbol/*!*/ _and = new FunctionSymbol("/\\", binproptype);
+ private static readonly FunctionSymbol/*!*/ _or = new FunctionSymbol("\\/", binproptype);
+ private static readonly FunctionSymbol/*!*/ _implies = new FunctionSymbol("==>", binproptype);
+ private static readonly FunctionSymbol/*!*/ _exists = new FunctionSymbol("Exists", quantifiertype);
+ private static readonly FunctionSymbol/*!*/ _forall = new FunctionSymbol("Forall", quantifiertype);
+ private static readonly FunctionSymbol/*!*/ _lambda = new FunctionSymbol("Lambda", quantifiertype);
+
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ False { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _false; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ True { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _true; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Not { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _not; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ And { [Pure] get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _and; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Or { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _or; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Implies { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _implies; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Exists { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _exists; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Forall { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _forall; } }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public static FunctionSymbol/*!*/ Lambda { get { Contract.Ensures(Contract.Result<FunctionSymbol>() != null); return _lambda; } }
+
/// <summary>
- /// 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.
+ /// Prop should not be instantiated from the outside.
/// </summary>
- ///
- [ContractClass(typeof(IPropExprFactoryContracts))]
- public interface IPropExprFactory
- {
- IFunApp/*!*/ False { get /*ensures result.FunctionSymbol.Equals(Prop.False);*/; }
- IFunApp/*!*/ True { get /*ensures result.FunctionSymbol.Equals(Prop.True);*/; }
-
- IFunApp/*!*/ Not(IExpr/*!*/ p) /*ensures result.FunctionSymbol.Equals(Prop.Not);*/;
-
- IFunApp/*!*/ And(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.And);*/;
- IFunApp/*!*/ Or(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.Or);*/;
-
- IFunApp/*!*/ Implies(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.Implies);*/;
- }
- [ContractClassFor(typeof(IPropExprFactory))]
- public abstract class IPropExprFactoryContracts:IPropExprFactory{
- #region IPropExprFactory Members
- IFunApp IPropExprFactory.Implies(IExpr p, IExpr q)
- {
- Contract.Requires(p != null);
- Contract.Requires(q != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
+ private Prop() { }
+
+
+
+ //
+ // Utility Methods
+ //
+
+ public static IExpr/*!*/ SimplifiedAnd(IPropExprFactory/*!*/ factory, IExpr/*!*/ e0, IExpr/*!*/ e1) {
+ Contract.Requires(e1 != null);
+ Contract.Requires(e0 != null);
+ Contract.Requires(factory != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ IFunApp fun0 = e0 as IFunApp;
+ if (fun0 != null) {
+ if (fun0.FunctionSymbol.Equals(Prop.True)) {
+ return e1;
+ } else if (fun0.FunctionSymbol.Equals(Prop.False)) {
+ return e0;
+ }
+ }
+
+ IFunApp fun1 = e1 as IFunApp;
+ if (fun1 != null) {
+ if (fun1.FunctionSymbol.Equals(Prop.True)) {
+ return e0;
+ } else if (fun1.FunctionSymbol.Equals(Prop.False)) {
+ return e1;
+ }
+ }
+
+ return factory.And(e0, e1);
}
-IFunApp IPropExprFactory.False
-{
-
- get { Contract.Ensures(Contract.Result<IFunApp>() != null);throw new System.NotImplementedException(); }
-}
+ public static IExpr/*!*/ SimplifiedAnd(IPropExprFactory/*!*/ factory, IEnumerable/*<IExpr!>*//*!*/ exprs) {
+ Contract.Requires(exprs != null);
+ Contract.Requires(factory != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ IExpr/*!*/ result = factory.True;
+ Contract.Assert(result != null);
+ foreach (IExpr/*!*/ conjunct in exprs) {
+ Contract.Assert(conjunct != null);
+ result = SimplifiedAnd(factory, result, conjunct);
+ }
+ return result;
+ }
-IFunApp IPropExprFactory.True
-{
- get {Contract.Ensures(Contract.Result<IFunApp>() != null); throw new System.NotImplementedException(); }
-}
+ public static IExpr/*!*/ SimplifiedOr(IPropExprFactory/*!*/ factory, IExpr/*!*/ e0, IExpr/*!*/ e1) {
+ Contract.Requires(e1 != null);
+ Contract.Requires(e0 != null);
+ Contract.Requires(factory != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ IFunApp fun0 = e0 as IFunApp;
+ if (fun0 != null) {
+ if (fun0.FunctionSymbol.Equals(Prop.False)) {
+ return e1;
+ } else if (fun0.FunctionSymbol.Equals(Prop.True)) {
+ return e0;
+ }
+ }
-IFunApp IPropExprFactory.Not(IExpr p)
-{
- Contract.Requires(p != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ 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;
+ }
+ }
-IFunApp IPropExprFactory.And(IExpr p, IExpr q)
-{
- Contract.Requires(p != null);
- Contract.Requires(q != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ return factory.Or(e0, e1);
+ }
-IFunApp IPropExprFactory.Or(IExpr p, IExpr q)
-{Contract.Requires(p != null);
- Contract.Requires(q != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ public static IExpr/*!*/ SimplifiedOr(IPropExprFactory/*!*/ factory, IEnumerable/*<IExpr!>*//*!*/ exprs) {
+ Contract.Requires(exprs != null);
+ Contract.Requires(factory != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ IExpr/*!*/ result = factory.False;
+ Contract.Assert(result != null);
+ foreach (IExpr/*!*/ disj in exprs) {
+ Contract.Assert(disj != null);
+ result = SimplifiedOr(factory, result, disj);
+ }
+ return result;
+ }
-#endregion
-}
-
/// <summary>
- /// Like IPropExprFactory, but also with quantifiers.
+ /// Break top-level conjuncts into a list of sub-expressions.
/// </summary>
- ///
- [ContractClass(typeof(IQuantPropExprFactoryContracts))]
- public interface IQuantPropExprFactory : IPropExprFactory {
- /// <summary>
- /// Produce an existential given the lambda-expression.
- /// </summary>
- /// <param name="p">The lambda-expression.</param>
- /// <returns>The existential.</returns>
- IFunApp/*!*/ Exists(IFunction/*!*/ p) /*ensures result.FunctionSymbol.Equals(Prop.Exists);*/;
- IFunApp/*!*/ Forall(IFunction/*!*/ p) /*ensures result.FunctionSymbol.Equals(Prop.Forall);*/;
-
- /// <summary>
- /// Produce an existential given a callback that can produce a function body given the
- /// bound variable to use. The implementer of this method is responsible for generating
- /// a fresh new variable to pass to the FunctionBody callback to use as the bound variable.
- /// </summary>
- /// <param name="body">The function body callback.</param>
- /// <returns>The existential.</returns>
- IFunApp/*!*/ Exists(AIType paramType, FunctionBody/*!*/ body) /*ensures result.FunctionSymbol.Equals(Prop.Exists);*/;
- IFunApp/*!*/ Forall(AIType paramType, FunctionBody/*!*/ body) /*ensures result.FunctionSymbol.Equals(Prop.Forall);*/;
- }
- [ContractClassFor(typeof(IQuantPropExprFactory))]
- public abstract class IQuantPropExprFactoryContracts:IQuantPropExprFactory{
- #region IQuantPropExprFactory Members
-
-IFunApp IQuantPropExprFactory.Exists(IFunction p)
-{
- Contract.Requires(p != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ /// <param name="e">The expression to examine.</param>
+ /// <returns>A list of conjuncts.</returns>
+ internal static IList/*<IExpr!>*//*!*/ BreakConjuncts(IExpr/*!*/ e) {
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<IList>() != null);
+ Contract.Ensures(Contract.ForAll(0, Contract.Result<IList>().Count, i => {
+ var sub = Contract.Result<IList>()[i];
+ return !(sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(Prop.And);
+ }));
+ return BreakJuncts(e, Prop.And);
+ }
-IFunApp IQuantPropExprFactory.Forall(IFunction p)
-{Contract.Requires(p != null);Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ /// <summary>
+ /// Break top-level disjuncts into a list of sub-expressions.
+ /// </summary>
+ /// <param name="e">The expression to examine.</param>
+ /// <returns>A list of conjuncts.</returns>
+ internal static IList/*<IExpr!>*//*!*/ BreakDisjuncts(IExpr/*!*/ e) {
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<IList>() != null);
+ Contract.Ensures(Contract.ForAll(0, Contract.Result<IList>().Count, i => {
+ var sub = Contract.Result<IList>()[i];
+ return !(sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(Prop.Or);
+ }));
+ return BreakJuncts(e, Prop.Or);
+ }
-IFunApp IQuantPropExprFactory.Exists(AIType paramType, FunctionBody body)
-{Contract.Requires(body != null);Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ private static IList/*<IExpr!>*//*!*/ BreakJuncts(IExpr/*!*/ e, IFunctionSymbol/*!*/ sym) {
+ Contract.Requires(sym != null);
+ Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<IList>() != null);
+ Contract.Ensures(Contract.ForAll(0, Contract.Result<IList>().Count, i => {
+ var sub = Contract.Result<IList>()[i];
+ return (sub is IFunApp) || !((IFunApp)sub).FunctionSymbol.Equals(sym);
+ }));
+ ArrayList/*<IExpr!>*//*!*/ result = new ArrayList();
+
+ IFunApp f = e as IFunApp;
+ if (f != null) {
+ // If it is a sym, go down into sub-expressions.
+ if (f.FunctionSymbol.Equals(sym)) {
+ foreach (IExpr/*!*/ arg in f.Arguments) {
+ Contract.Assert(arg != null);
+ result.AddRange(BreakJuncts(arg, sym));
+ }
+ }
+ // Otherwise, stop.
+ else {
+ result.Add(e);
+ }
+ } else {
+ result.Add(e);
+ }
-IFunApp IQuantPropExprFactory.Forall(AIType paramType, FunctionBody body)
-{Contract.Requires(body != null);Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ return result;
+ }
+ }
-#endregion
+ /// <summary>
+ /// A callback to produce a function body given the bound variable.
+ /// </summary>
+ /// <param name="var">The bound variable to use.</param>
+ /// <returns>The function body.</returns>
+ public delegate IExpr/*!*/ FunctionBody(IVariable/*!*/ var);
+
+ /// <summary>
+ /// An interface for constructing propositional expressions.
+ ///
+ /// This interface should be implemented by the client. An implementation of
+ /// of this class should generally be used as a singleton object.
+ /// </summary>
+ ///
+ [ContractClass(typeof(IPropExprFactoryContracts))]
+ public interface IPropExprFactory
+ {
+ IFunApp/*!*/ False { get /*ensures result.FunctionSymbol.Equals(Prop.False);*/; }
+ IFunApp/*!*/ True { get /*ensures result.FunctionSymbol.Equals(Prop.True);*/; }
+
+ IFunApp/*!*/ Not(IExpr/*!*/ p) /*ensures result.FunctionSymbol.Equals(Prop.Not);*/;
+
+ IFunApp/*!*/ And(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.And);*/;
+ IFunApp/*!*/ Or(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.Or);*/;
+
+ IFunApp/*!*/ Implies(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.Implies);*/;
+ }
+ [ContractClassFor(typeof(IPropExprFactory))]
+ public abstract class IPropExprFactoryContracts : IPropExprFactory
+ {
+ #region IPropExprFactory Members
+ IFunApp IPropExprFactory.Implies(IExpr p, IExpr q) {
+ Contract.Requires(p != null);
+ Contract.Requires(q != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-#region IPropExprFactory Members
+ IFunApp IPropExprFactory.False {
-IFunApp IPropExprFactory.False
-{
- get { throw new System.NotImplementedException(); }
-}
+ get { Contract.Ensures(Contract.Result<IFunApp>() != null); throw new System.NotImplementedException(); }
+ }
-IFunApp IPropExprFactory.True
-{
- get { throw new System.NotImplementedException(); }
-}
+ IFunApp IPropExprFactory.True {
+ get { Contract.Ensures(Contract.Result<IFunApp>() != null); throw new System.NotImplementedException(); }
+ }
-IFunApp IPropExprFactory.Not(IExpr p)
-{
- throw new System.NotImplementedException();
-}
+ IFunApp IPropExprFactory.Not(IExpr p) {
+ Contract.Requires(p != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-IFunApp IPropExprFactory.And(IExpr p, IExpr q)
-{
- throw new System.NotImplementedException();
-}
+ IFunApp IPropExprFactory.And(IExpr p, IExpr q) {
+ Contract.Requires(p != null);
+ Contract.Requires(q != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-IFunApp IPropExprFactory.Or(IExpr p, IExpr q)
-{
- throw new System.NotImplementedException();
-}
+ IFunApp IPropExprFactory.Or(IExpr p, IExpr q) {
+ Contract.Requires(p != null);
+ Contract.Requires(q != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-IFunApp IPropExprFactory.Implies(IExpr p, IExpr q)
-{
- throw new System.NotImplementedException();
-}
-#endregion
-}
- /// <summary>
- /// An interface for constructing value expressions.
- ///
- /// This interface should be implemented by the client. An implementation of
- /// of this class should generally be used as a singleton object.
- /// </summary>
- ///
+ #endregion
+ }
+
+ /// <summary>
+ /// An interface for constructing value expressions.
+ ///
+ /// This interface should be implemented by the client. An implementation of
+ /// of this class should generally be used as a singleton object.
+ /// </summary>
+ ///
[ContractClass(typeof(IValueExprFactoryContracts))]
- public interface IValueExprFactory
- {
- IFunApp/*!*/ Eq (IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Eq);*/;
- IFunApp/*!*/ Neq(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Neq);*/;
- }
+ 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
+ public abstract class IValueExprFactoryContracts : IValueExprFactory
+ {
+ #region IValueExprFactory Members
-IFunApp IValueExprFactory.Eq(IExpr e0, IExpr e1)
-{
- Contract.Requires(e0 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ IFunApp IValueExprFactory.Eq(IExpr e0, IExpr e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-IFunApp IValueExprFactory.Neq(IExpr e0, IExpr e1)
-{
- Contract.Requires(e0 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ IFunApp IValueExprFactory.Neq(IExpr e0, IExpr e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-#endregion
-}
+ #endregion
+ }
- /// <summary>
- /// An interface for constructing value expressions having to with null.
- ///
- /// This interface should be implemented by the client. An implementation of
- /// of this class should generally be used as a singleton object.
- /// </summary>
- ///
+ /// <summary>
+ /// An interface for constructing value expressions having to with null.
+ ///
+ /// This interface should be implemented by the client. An implementation of
+ /// of this class should generally be used as a singleton object.
+ /// </summary>
+ ///
[ContractClass(typeof(INullnessFactoryContracts))]
- public interface INullnessFactory
- {
- IFunApp/*!*/ Eq(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Eq);*/;
- IFunApp/*!*/ Neq(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Neq);*/;
- IFunApp/*!*/ Null { get; /*ensures result.FunctionSymbol.Equals(Ref.Null);*/ }
- }
+ 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
+ public abstract class INullnessFactoryContracts : INullnessFactory
+ {
+ #region INullnessFactory Members
-IFunApp INullnessFactory.Eq(IExpr e0, IExpr e1)
-{
- Contract.Requires(e0 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ IFunApp INullnessFactory.Eq(IExpr e0, IExpr e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-IFunApp INullnessFactory.Neq(IExpr e0, IExpr e1)
-{
- Contract.Requires(e0 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ IFunApp INullnessFactory.Neq(IExpr e0, IExpr e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-IFunApp INullnessFactory.Null
-{
- get {
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException(); }
-}
+ IFunApp INullnessFactory.Null {
+ get {
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
+ }
-#endregion
-}
+ #endregion
+ }
- /// <summary>
- /// An interface for constructing integer expressions.
- ///
- /// This interface should be implemented by the client. An implementation of
- /// of this class should generally be used as a singleton object.
- /// </summary>
- ///
+ /// <summary>
+ /// An interface for constructing integer expressions.
+ ///
+ /// This interface should be implemented by the client. An implementation of
+ /// of this class should generally be used as a singleton object.
+ /// </summary>
+ ///
[ContractClass(typeof(IIntExprFactoryContracts))]
- public interface IIntExprFactory : IValueExprFactory
- {
- IFunApp/*!*/ Const(BigNum i) /*ensures result.FunctionSymbol.Equals(new IntSymbol(i));*/;
- }
+ 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
+ public abstract class IIntExprFactoryContracts : IIntExprFactory
+ {
- IFunApp IIntExprFactory.Const(BigNum i) {
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
- }
+ #region IIntExprFactory Members
- #endregion
+ IFunApp IIntExprFactory.Const(BigNum i) {
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
- #region IValueExprFactory Members
+ #endregion
- IFunApp IValueExprFactory.Eq(IExpr e0, IExpr e1) {
- throw new System.NotImplementedException();
- }
+ #region IValueExprFactory Members
- IFunApp IValueExprFactory.Neq(IExpr e0, IExpr e1) {
- throw new System.NotImplementedException();
- }
+ IFunApp IValueExprFactory.Eq(IExpr e0, IExpr e1) {
+ throw new System.NotImplementedException();
+ }
- #endregion
+ IFunApp IValueExprFactory.Neq(IExpr e0, IExpr e1) {
+ throw new System.NotImplementedException();
}
+ #endregion
+ }
+
+ /// <summary>
+ /// An interface for constructing linear integer expressions.
+ ///
+ /// This interface should be implemented by the client. An implementation of
+ /// of this class should generally be used as a singleton object.
+ /// </summary>
+ ///
+ [ContractClass(typeof(ILinearExprFactoryContracts))]
+ public interface ILinearExprFactory : IIntExprFactory
+ {
+ IFunApp/*!*/ AtMost(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.AtMost);*/;
+ IFunApp/*!*/ Add(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Add);*/;
/// <summary>
- /// 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.
+ /// If "var" is null, returns an expression representing r.
+ /// Otherwise, returns an expression representing r*var.
/// </summary>
- ///
- [ContractClass(typeof(ILinearExprFactoryContracts))]
- public interface ILinearExprFactory : IIntExprFactory
- {
- IFunApp/*!*/ AtMost(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.AtMost);*/;
- IFunApp/*!*/ Add(IExpr/*!*/ e0, IExpr/*!*/ e1) /*ensures result.FunctionSymbol.Equals(Value.Add);*/;
- /// <summary>
- /// If "var" is null, returns an expression representing r.
- /// Otherwise, returns an expression representing r*var.
- /// </summary>
- IExpr/*!*/ Term(Microsoft.Basetypes.Rational r, IVariable var);
-
- IFunApp/*!*/ False { get /*ensures result.FunctionSymbol.Equals(Prop.False);*/; }
- IFunApp/*!*/ True { get /*ensures result.FunctionSymbol.Equals(Prop.True);*/; }
- IFunApp/*!*/ And(IExpr/*!*/ p, IExpr/*!*/ q) /*ensures result.FunctionSymbol.Equals(Prop.And);*/;
- }
+ 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{
+ public abstract class ILinearExprFactoryContracts : ILinearExprFactory
+ {
- #region ILinearExprFactory Members
+ #region ILinearExprFactory Members
-IFunApp ILinearExprFactory.AtMost(IExpr e0, IExpr e1)
-{
- Contract.Requires(e0 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ IFunApp ILinearExprFactory.AtMost(IExpr e0, IExpr e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-IFunApp ILinearExprFactory.Add(IExpr e0, IExpr e1)
-{
- Contract.Requires(e0 != null);
- Contract.Requires(e1 != null);Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ IFunApp ILinearExprFactory.Add(IExpr e0, IExpr e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null); Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-IExpr ILinearExprFactory.Term(Rational r, IVariable var)
-{
- Contract.Ensures(Contract.Result<IExpr>() != null);
- throw new System.NotImplementedException();
-}
+ IExpr ILinearExprFactory.Term(Rational r, IVariable var) {
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ throw new System.NotImplementedException();
+ }
-IFunApp ILinearExprFactory.False
-{
- get {Contract.Ensures(Contract.Result<IFunApp>() != null); throw new System.NotImplementedException(); }
-}
+ IFunApp ILinearExprFactory.False {
+ get { Contract.Ensures(Contract.Result<IFunApp>() != null); throw new System.NotImplementedException(); }
+ }
-IFunApp ILinearExprFactory.True
-{
- get { Contract.Ensures(Contract.Result<IFunApp>() != null);throw new System.NotImplementedException(); }
-}
+ IFunApp ILinearExprFactory.True {
+ get { Contract.Ensures(Contract.Result<IFunApp>() != null); throw new System.NotImplementedException(); }
+ }
-IFunApp ILinearExprFactory.And(IExpr p, IExpr q)
-{
- Contract.Requires(p != null);
- Contract.Requires(q != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ IFunApp ILinearExprFactory.And(IExpr p, IExpr q) {
+ Contract.Requires(p != null);
+ Contract.Requires(q != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-#endregion
+ #endregion
-#region IIntExprFactory Members
+ #region IIntExprFactory Members
-IFunApp IIntExprFactory.Const(BigNum i) {
- throw new System.NotImplementedException();
-}
+ IFunApp IIntExprFactory.Const(BigNum i) {
+ throw new System.NotImplementedException();
+ }
-#endregion
+ #endregion
-#region IValueExprFactory Members
+ #region IValueExprFactory Members
-IFunApp IValueExprFactory.Eq(IExpr e0, IExpr e1) {
- throw new System.NotImplementedException();
-}
+ IFunApp IValueExprFactory.Eq(IExpr e0, IExpr e1) {
+ throw new System.NotImplementedException();
+ }
-IFunApp IValueExprFactory.Neq(IExpr e0, IExpr e1) {
- throw new System.NotImplementedException();
-}
+ IFunApp IValueExprFactory.Neq(IExpr e0, IExpr e1) {
+ throw new System.NotImplementedException();
+ }
-#endregion
+ #endregion
}
+ /// <summary>
+ /// An interface for constructing type expressions and performing some type operations.
+ /// The types are assumed to be arranged in a rooted tree.
+ ///
+ /// This interface should be implemented by the client. An implementation of
+ /// of this class should generally be used as a singleton object.
+ /// </summary>
+ ///
+ [ContractClass(typeof(ITypeExprFactoryContracts))]
+ public interface ITypeExprFactory
+ {
/// <summary>
- /// 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.
+ /// Returns an expression denoting the top of the type hierarchy.
/// </summary>
- ///
- [ContractClass(typeof(ITypeExprFactoryContracts))]
- public interface ITypeExprFactory
- {
- /// <summary>
- /// Returns an expression denoting the top of the type hierarchy.
- /// </summary>
- IExpr/*!*/ RootType { get; }
-
- /// <summary>
- /// Returns true iff "t" denotes a type constant.
- /// </summary>
- [Pure]
- bool IsTypeConstant(IExpr/*!*/ t);
-
- /// <summary>
- /// Returns true iff t0 and t1 are types such that t0 and t1 are equal.
- /// </summary>
- [Pure]
- bool IsTypeEqual(IExpr/*!*/ t0, IExpr/*!*/ t1);
-
- /// <summary>
- /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.
- /// </summary>
- [Pure]
- bool IsSubType(IExpr/*!*/ t0, IExpr/*!*/ t1);
-
- /// <summary>
- /// Returns the most derived supertype of both "t0" and "t1". A precondition is
- /// that "t0" and "t1" both represent types.
- /// </summary>
- IExpr/*!*/ JoinTypes(IExpr/*!*/ t0, IExpr/*!*/ t1);
-
- IFunApp/*!*/ IsExactlyA(IExpr/*!*/ e, IExpr/*!*/ type) /*requires IsTypeConstant(type); ensures result.FunctionSymbol.Equals(Value.Eq);*/;
- IFunApp/*!*/ IsA(IExpr/*!*/ e, IExpr/*!*/ type) /*requires IsTypeConstant(type); ensures result.FunctionSymbol.Equals(Value.Subtype);*/;
- }
+ IExpr/*!*/ RootType { get; }
+
+ /// <summary>
+ /// Returns true iff "t" denotes a type constant.
+ /// </summary>
+ [Pure]
+ bool IsTypeConstant(IExpr/*!*/ t);
+
+ /// <summary>
+ /// Returns true iff t0 and t1 are types such that t0 and t1 are equal.
+ /// </summary>
+ [Pure]
+ bool IsTypeEqual(IExpr/*!*/ t0, IExpr/*!*/ t1);
+
+ /// <summary>
+ /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1.
+ /// </summary>
+ [Pure]
+ bool IsSubType(IExpr/*!*/ t0, IExpr/*!*/ t1);
+
+ /// <summary>
+ /// Returns the most derived supertype of both "t0" and "t1". A precondition is
+ /// that "t0" and "t1" both represent types.
+ /// </summary>
+ IExpr/*!*/ JoinTypes(IExpr/*!*/ t0, IExpr/*!*/ t1);
+
+ IFunApp/*!*/ IsExactlyA(IExpr/*!*/ e, IExpr/*!*/ type) /*requires IsTypeConstant(type); ensures result.FunctionSymbol.Equals(Value.Eq);*/;
+ IFunApp/*!*/ IsA(IExpr/*!*/ e, IExpr/*!*/ type) /*requires IsTypeConstant(type); ensures result.FunctionSymbol.Equals(Value.Subtype);*/;
+ }
[ContractClassFor(typeof(ITypeExprFactory))]
- public abstract class ITypeExprFactoryContracts:ITypeExprFactory{
+ public abstract class ITypeExprFactoryContracts : ITypeExprFactory
+ {
- #region ITypeExprFactory Members
+ #region ITypeExprFactory Members
-IExpr ITypeExprFactory.RootType
-{
- get {Contract.Ensures(Contract.Result<IExpr>() != null); throw new System.NotImplementedException(); }
-}
+ IExpr ITypeExprFactory.RootType {
+ get { Contract.Ensures(Contract.Result<IExpr>() != null); throw new System.NotImplementedException(); }
+ }
-bool ITypeExprFactory.IsTypeConstant(IExpr t)
-{
- Contract.Requires(t != null);
- throw new System.NotImplementedException();
-}
+ bool ITypeExprFactory.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.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();
-}
+ bool ITypeExprFactory.IsSubType(IExpr t0, IExpr t1) {
+ Contract.Requires(t0 != null);
+ Contract.Requires(t1 != null);
+ throw new System.NotImplementedException();
+ }
-IExpr ITypeExprFactory.JoinTypes(IExpr t0, IExpr t1)
-{
- Contract.Requires(t0 != null);
- Contract.Requires(t1 != null);
- Contract.Ensures(Contract.Result<IExpr>() != null);
- throw new System.NotImplementedException();
-}
+ IExpr ITypeExprFactory.JoinTypes(IExpr t0, IExpr t1) {
+ Contract.Requires(t0 != null);
+ Contract.Requires(t1 != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ throw new System.NotImplementedException();
+ }
-IFunApp ITypeExprFactory.IsExactlyA(IExpr e, IExpr type)
-{
- Contract.Requires(e != null);
- Contract.Requires(type != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ IFunApp ITypeExprFactory.IsExactlyA(IExpr e, IExpr type) {
+ Contract.Requires(e != null);
+ Contract.Requires(type != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-IFunApp ITypeExprFactory.IsA(IExpr e, IExpr type)
-{
- Contract.Requires(e != null);
- Contract.Requires(type != null);
- Contract.Ensures(Contract.Result<IFunApp>() != null);
- throw new System.NotImplementedException();
-}
+ IFunApp ITypeExprFactory.IsA(IExpr e, IExpr type) {
+ Contract.Requires(e != null);
+ Contract.Requires(type != null);
+ Contract.Ensures(Contract.Result<IFunApp>() != null);
+ throw new System.NotImplementedException();
+ }
-#endregion
+ #endregion
+ }
}
-}
\ No newline at end of file diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs index 698141bb..a5847594 100644 --- a/Source/AbsInt/AbstractInterpretation.cs +++ b/Source/AbsInt/AbstractInterpretation.cs @@ -686,7 +686,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { static public AbstractAlgebra BuildIntervalsAbstractDomain() {
Contract.Ensures(Contract.Result<AbstractAlgebra>() != null);
- AI.IQuantPropExprFactory propfactory = new BoogiePropFactory();
+ AI.IPropExprFactory propfactory = new BoogiePropFactory();
AI.ILinearExprFactory linearfactory = new BoogieLinearFactory();
AI.IValueExprFactory valuefactory = new BoogieValueFactory();
IComparer variableComparer = new VariableComparer();
@@ -709,7 +709,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { AI.Lattice returnLattice;
- AI.IQuantPropExprFactory propfactory = new BoogiePropFactory();
+ AI.IPropExprFactory propfactory = new BoogiePropFactory();
AI.ILinearExprFactory linearfactory = new BoogieLinearFactory();
AI.IIntExprFactory intfactory = new BoogieIntFactory();
AI.IValueExprFactory valuefactory = new BoogieValueFactory();
@@ -772,7 +772,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { [Peer]
private AI.Lattice lattice;
[Peer]
- private AI.IQuantPropExprFactory propFactory;
+ private AI.IPropExprFactory propFactory;
[Peer]
private AI.ILinearExprFactory linearFactory;
[Peer]
@@ -797,7 +797,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { }
}
- public AI.IQuantPropExprFactory PropositionFactory {
+ public AI.IPropExprFactory PropositionFactory {
get {
return this.propFactory;
}
@@ -835,7 +835,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { [Captured]
public AbstractAlgebra(AI.Lattice lattice,
- AI.IQuantPropExprFactory propFactory,
+ AI.IPropExprFactory propFactory,
AI.ILinearExprFactory linearFactory,
AI.IIntExprFactory intFactory,
AI.IValueExprFactory valueFactory,
diff --git a/Source/AbsInt/ExprFactories.cs b/Source/AbsInt/ExprFactories.cs index 34564cac..9b1ea0a0 100644 --- a/Source/AbsInt/ExprFactories.cs +++ b/Source/AbsInt/ExprFactories.cs @@ -10,7 +10,8 @@ using Microsoft.Basetypes; namespace Microsoft.Boogie.AbstractInterpretation {
- public class BoogiePropFactory : BoogieFactory, AI.IQuantPropExprFactory {
+ public class BoogiePropFactory : BoogieFactory, AI.IPropExprFactory
+ {
public AI.IFunApp False {
get {
Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
@@ -61,17 +62,6 @@ namespace Microsoft.Boogie.AbstractInterpretation { return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;
}
- public AI.IFunApp Exists(AI.AIType paramType, AI.FunctionBody bodygen) {
- //Contract.Requires(bodygen != null);
- Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
-
- // generate a fresh new variable
- Variable var = FreshBoundVariable(paramType);
- Contract.Assert(var != null);
- Expr expr = IExpr2Expr(bodygen(var));
- Contract.Assert(expr != null);
- return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;
- }
public AI.IFunApp Forall(AI.IFunction p) {
//Contract.Requires(p != null);
@@ -79,39 +69,6 @@ namespace Microsoft.Boogie.AbstractInterpretation { return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;
}
- public AI.IFunApp Forall(AI.AIType paramType, AI.FunctionBody bodygen) {
- //Contract.Requires(bodygen != null);
- Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
-
- // generate a fresh new variable
- Variable var = FreshBoundVariable(paramType);
- Contract.Assert(var != null);
- Expr expr = IExpr2Expr(bodygen(var));
- Contract.Assert(expr != null);
- return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;
- }
-
- private static int freshVarNum = 0;
- private static Variable FreshBoundVariable(AI.AIType paramType) {
- Contract.Ensures(Contract.Result<Variable>() != null);
-
- // TODO: Should use the AI.AIType given in Exists and Forall to determine what Boogie type
- // to make this new variable? For now, we use Type.Any.
- Type t = Type.Int;
- Contract.Assert(t != null);
- /*
- if (paramType is AI.Ref)
- t = Type.Ref;
- else if (paramType is AI.FieldName)
- t = Type.Name;
- else
- System.Console.WriteLine("*** unsupported type in AI {0}", paramType); */
- Contract.Assert(false);
- throw new cce.UnreachableException();
- TypedIdent id = new TypedIdent(Token.NoToken, "propfactory_freshvar" + freshVarNum, t);
- freshVarNum++;
- return new BoundVariable(Token.NoToken, id);
- }
}
public class BoogieValueFactory : BoogieFactory, AI.IValueExprFactory {
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index a9c41efb..0b40c86e 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -761,7 +761,7 @@ namespace Microsoft.Boogie { Graph<Block> g = ProcessLoops(impl);
CreateProceduresForLoops(impl, g, loopImpls, fullMap);
}
- catch (IrreducibleLoopException e)
+ catch (IrreducibleLoopException)
{
System.Diagnostics.Debug.Assert(!fullMap.ContainsKey(impl.Name));
fullMap[impl.Name] = null;
|