From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Wed, 15 Jul 2009 21:03:41 +0000 Subject: Initial set of files. --- Source/AIFramework/CommonFunctionSymbols.ssc | 926 +++++++++++++++++++++++++++ 1 file changed, 926 insertions(+) create mode 100644 Source/AIFramework/CommonFunctionSymbols.ssc (limited to 'Source/AIFramework/CommonFunctionSymbols.ssc') diff --git a/Source/AIFramework/CommonFunctionSymbols.ssc b/Source/AIFramework/CommonFunctionSymbols.ssc new file mode 100644 index 00000000..4e38fbcb --- /dev/null +++ b/Source/AIFramework/CommonFunctionSymbols.ssc @@ -0,0 +1,926 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +namespace Microsoft.AbstractInterpretationFramework +{ + using Microsoft.Contracts; + using System.Collections; + using Microsoft.SpecSharp.Collections; + using Microsoft.Basetypes; + + /// + /// A basic class for function symbols. + /// + public class FunctionSymbol : IFunctionSymbol + { + private readonly string! display; + private readonly AIType! typ; + + public FunctionSymbol(AIType! typ) + : this("FunctionSymbol", typ) + { + } + + internal FunctionSymbol(string! display, AIType! typ) + { + this.display = display; + this.typ = typ; + // base(); + } + +// public AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return typ; } } + public AIType! AIType { [Pure][Reads(ReadsAttribute.Reads.Owned)] get { return typ; } } + + [NoDefaultContract] + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override string! ToString() + { + return display; + } + + } + + /// + /// A class for integer constants. + /// + public class IntSymbol : FunctionSymbol + { + public readonly BigNum Value; + + /// + /// The intention is that this constructor be called only from the Int.Const method. + /// + internal IntSymbol(BigNum x) + : base((!)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][Reads(ReadsAttribute.Reads.Owned)] + public override int GetHashCode() + { + return Value.GetHashCode(); + } + } + + /// + /// A class for bitvector constants. + /// + public class BvSymbol : FunctionSymbol + { + public readonly BigNum Value; + public readonly int Bits; + + /// + /// The intention is that this constructor be called only from the Int.Const method. + /// + internal BvSymbol(BigNum x, int y) + : base(x + "bv" + y, Bv.Type) + { + this.Value = x; + this.Bits = y; + } + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) + { + BvSymbol isym = other as BvSymbol; + return isym != null && isym.Value == this.Value && isym.Bits == this.Bits; + } + + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override int GetHashCode() + { + unchecked { + return Value.GetHashCode() ^ Bits; + } + } + } + + public class DoubleSymbol : FunctionSymbol + { + public readonly double Value; + + /// + /// The intention is that this constructor be called only from the Double.Const method. + /// + internal DoubleSymbol(double x) + : base((!)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.Owned)] + public override int GetHashCode() + { + return Value.GetHashCode(); + } + } + + /// + /// Function symbol based on a string. Uses the string equality for determining equality + /// of symbol. + /// + public class NamedSymbol : FunctionSymbol + { + public string! Value { [NoDefaultContract] get { return (!) this.ToString(); } } + + public NamedSymbol(string! symbol, AIType! typ) + : base(symbol, typ) + { + } + + [NoDefaultContract] + [Pure][Reads(ReadsAttribute.Reads.Nothing)] + public override bool Equals(object other) + { + NamedSymbol nsym = other as NamedSymbol; + return nsym != null && this.Value.Equals(nsym.Value); + } + + [NoDefaultContract] + [Pure][Reads(ReadsAttribute.Reads.Owned)] + public override int GetHashCode() + { + return Value.GetHashCode(); + } + } + + // + // In the following, the classes like Value and Prop serve two + // roles. The primary role is to be the base types for AIType. + // The only objects of these classes are the representative + // objects that denote an AIType, which are given by the + // "Type" property. Subtypes in the AIType language are + // encoded by subclassing. This yields some "higher-orderness" + // for checking subtyping in the AIType language, by using + // the Spec#/C# subclassing checks. + // + // The other role is simply as a module for collecting like function + // symbols. + // + + //-------------------------- Terms ---------------------------------- + + /// + /// A class with the equality symbol and the ValueType.Type. + /// + public class Value : AIType + { + private static readonly AIType! valtype = new Value(); + public static AIType! Type { get { return valtype; } } + + private static readonly FunctionType[]! funtypeCache = new FunctionType[5]; + public static FunctionType! FunctionType(int inParameterCount) + requires 0 <= inParameterCount; + // ensures result.Arity == inParameterCount; + { + FunctionType result; + if (inParameterCount < funtypeCache.Length) { + result = funtypeCache[inParameterCount]; + if (result != null) { + return result; + } + } + AIType[] signature = new AIType[1 + inParameterCount]; + for (int i = 0; i < signature.Length; i++) { + signature[i] = valtype; + } + result = new FunctionType(signature); + if (inParameterCount < funtypeCache.Length) { + funtypeCache[inParameterCount] = result; + } + return result; + } + + [Once] private static AIType! binreltype; + private static AIType! BinrelType { + get { + if (binreltype == null) { + binreltype = new FunctionType(Type, Type, Prop.Type); + } + return binreltype; + } + } + + [Once] private static FunctionSymbol! _eq; + public static FunctionSymbol! Eq { + get { + if (_eq == null) { + _eq = new FunctionSymbol("=", BinrelType); + } + return _eq; + } + } + [Once] private static FunctionSymbol! _neq; + public static FunctionSymbol! Neq { + get { + if (_neq == null) { + _neq = new FunctionSymbol("!=", BinrelType); + } + return _neq; + } + } + [Once] private static FunctionSymbol! _subtype; + public static FunctionSymbol! Subtype { + get { + if (_subtype == null) { + _subtype = new FunctionSymbol("<:", BinrelType); + } + return _subtype; + } + } + + [Once] private static AIType! typeof_type; + private static AIType! TypeofType { + get { + if (typeof_type == null) { + typeof_type = new FunctionType(Ref.Type, Type); + } + return typeof_type; + } + } + [Once] private static FunctionSymbol! _typeof; + public static FunctionSymbol! Typeof { + get { + if (_typeof == null) { + _typeof = new FunctionSymbol("typeof", TypeofType); + } + return _typeof; + } + } + + /// + /// Value should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + protected Value() { } + + } + + public class Int : Value + { + private static readonly AIType! inttype = new Int(); + public static AIType! Type { get { return inttype; } } + + private static readonly AIType! unaryinttype = new FunctionType(Type, Type); + private static readonly AIType! bininttype = new FunctionType(Type, Type, Type); + private static readonly AIType! relationtype = new FunctionType(Type, Type, Prop.Type); + + private static readonly FunctionSymbol! _negate = new FunctionSymbol("~", unaryinttype); + private static readonly FunctionSymbol! _add = new FunctionSymbol("+", bininttype); + private static readonly FunctionSymbol! _sub = new FunctionSymbol("-", bininttype); + private static readonly FunctionSymbol! _mul = new FunctionSymbol("*", bininttype); + private static readonly FunctionSymbol! _div = new FunctionSymbol("/", bininttype); + private static readonly FunctionSymbol! _mod = new FunctionSymbol("%", bininttype); + private static readonly FunctionSymbol! _atmost = new FunctionSymbol("<=", relationtype); + private static readonly FunctionSymbol! _less = new FunctionSymbol("<", relationtype); + private static readonly FunctionSymbol! _greater = new FunctionSymbol(">", relationtype); + private static readonly FunctionSymbol! _atleast = new FunctionSymbol(">=", relationtype); + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Negate { get { return _negate; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Add { get { return _add; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Sub { get { return _sub; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mul { get { return _mul; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Div { get { return _div; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mod { get { return _mod; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtMost { get { return _atmost; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Less { get { return _less; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Greater { get { return _greater; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtLeast { get { return _atleast; } } + + public static IntSymbol! Const(BigNum x) + { + // We could cache things here, but for now we don't. + return new IntSymbol(x); + } + + /// + /// Int should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Int() { } + } + + public class Double : Value + { + private static readonly AIType! doubletype = new Double(); + public static AIType! Type { get { return doubletype; } } + + public static DoubleSymbol! Const(double x) + { + // We could cache things here, but for now we don't. + return new DoubleSymbol(x); + } + + /// + /// Double should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Double() { } + } + + public class Bv : Value + { + private static readonly AIType! bvtype = new Bv(); + public static AIType! Type { get { return bvtype; } } + + private static readonly AIType! unaryinttype = new FunctionType(Type, Type); + private static readonly AIType! bininttype = new FunctionType(Type, Type, Type); + private static readonly AIType! relationtype = new FunctionType(Type, Type, Prop.Type); + + private static readonly FunctionSymbol! _negate = new FunctionSymbol("~", unaryinttype); + private static readonly FunctionSymbol! _add = new FunctionSymbol("+", bininttype); + private static readonly FunctionSymbol! _sub = new FunctionSymbol("-", bininttype); + private static readonly FunctionSymbol! _mul = new FunctionSymbol("*", bininttype); + private static readonly FunctionSymbol! _div = new FunctionSymbol("/", bininttype); + private static readonly FunctionSymbol! _mod = new FunctionSymbol("%", bininttype); + private static readonly FunctionSymbol! _concat = new FunctionSymbol("$concat", bininttype); + private static readonly FunctionSymbol! _extract = new FunctionSymbol("$extract", unaryinttype); + private static readonly FunctionSymbol! _atmost = new FunctionSymbol("<=", relationtype); + private static readonly FunctionSymbol! _less = new FunctionSymbol("<", relationtype); + private static readonly FunctionSymbol! _greater = new FunctionSymbol(">", relationtype); + private static readonly FunctionSymbol! _atleast = new FunctionSymbol(">=", relationtype); + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Negate { get { return _negate; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Add { get { return _add; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Sub { get { return _sub; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mul { get { return _mul; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Div { get { return _div; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Mod { get { return _mod; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtMost { get { return _atmost; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Less { get { return _less; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Greater { get { return _greater; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! AtLeast { get { return _atleast; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Extract { get { return _extract; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Concat { get { return _concat; } } + + public static BvSymbol! Const(BigNum x, int y) + { + // We could cache things here, but for now we don't. + return new BvSymbol(x, y); + } + + /// + /// Int should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Bv() { } + } + + public class Ref : Value + { + private static readonly AIType! reftype = new Ref(); + public static AIType! Type { get { return reftype; } } + + private static readonly FunctionSymbol! _null = new FunctionSymbol("null", Type); + + public static FunctionSymbol! Null { get { return _null; } } + + /// + /// Ref should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Ref() { } + } + + public class HeapStructure : Value + { + private static readonly AIType! reftype = new HeapStructure(); + public static AIType! Type { get { return reftype; } } + + + + /// + /// HeapStructure should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private HeapStructure() { } + } + + public class FieldName : Value + { + private static readonly AIType! fieldnametype = new FieldName(); + public static AIType! Type { get { return fieldnametype; } } + + private static readonly FunctionSymbol! _allocated = new FunctionSymbol("$allocated", FieldName.Type); + public static FunctionSymbol! Allocated { get { return _allocated; } } + + /// + /// Is this a boolean field that monotonically goes from false to true? + /// + public static bool IsBooleanMonotonicallyWeakening(IFunctionSymbol! f) + { + return f.Equals(Allocated); + } + + /// + /// FieldName should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private FieldName() { } + } + + public class Heap : Value + { + private static readonly AIType! heaptype = new Heap(); + public static AIType! Type { get { return heaptype; } } + + // the types in the following, select1, select2, are hard-coded; + // these types may not always be appropriate + private static readonly FunctionSymbol! _select1 = new FunctionSymbol("sel1", + // Heap x FieldName -> Prop + new FunctionType(Type, FieldName.Type, Prop.Type) + ); + public static FunctionSymbol! Select1 { get { return _select1; } } + + private static readonly FunctionSymbol! _select2 = new FunctionSymbol("sel2", + // Heap x Ref x FieldName -> Value + new FunctionType(Type, Ref.Type, FieldName.Type, Value.Type) + ); + public static FunctionSymbol! Select2 { get { return _select2; } } + + // the types in the following, store1, store2, are hard-coded; + // these types may not always be appropriate + private static readonly FunctionSymbol! _update1 = new FunctionSymbol("upd1", + // Heap x FieldName x Value -> Heap + new FunctionType(Type, FieldName.Type, Value.Type, Type) + ); + public static FunctionSymbol! Update1 { get { return _update1; } } + + private static readonly FunctionSymbol! _update2 = new FunctionSymbol("upd2", + // Heap x Ref x FieldName x Value -> Heap + new FunctionType(Type, Ref.Type, FieldName.Type, Value.Type, Type) + ); + public static FunctionSymbol! Update2 { get { return _update2; } } + + private static readonly FunctionSymbol! _unsupportedHeapOp = + new FunctionSymbol("UnsupportedHeapOp", + // Heap x FieldName -> Prop + new FunctionType(Type, FieldName.Type, Prop.Type) + ); + public static FunctionSymbol! UnsupportedHeapOp { get { return _unsupportedHeapOp; } } + + /// + /// Heap should not be instantiated from the outside, except perhaps in + /// subclasses. + /// + private Heap() { } + } + +// public class List : Value +// { +// private static IDictionary/**/! lists = new Hashtable(); +// public static AIType! Type(AIType! typeParameter) +// { +// if (lists.Contains(typeParameter)) +// return lists[typeParameter]; +// else +// { +// AIType! result = new List(typeParameter); +// lists[typeParameter] = result; +// return result; +// } +// } +// +// private static IDictionary/**/! nils = new Hashtable(); +// public static FunctionSymbol! Nil(AIType! typeParameter) +// { +// if (nils.Contains(typeParameter)) +// return nils[typeParameter]; +// else +// { +// FunctionSymbol! result = new FunctionSymbol(Type(typeParameter)); +// nils[typeParameter] = result; +// return result; +// } +// } +// +// private static IDictionary/**/! cons = new Hashtable(); +// public static FunctionSymbol! Cons(AIType! typeParameter) +// { +// if (cons.Contains(typeParameter)) +// return cons[typeParameter]; +// else +// { +// FunctionSymbol! result = new FunctionSymbol( +// new FunctionType(typeParameter, Type(typeParameter), Type(typeParameter)) +// ); +// cons[typeParameter] = result; +// return result; +// } +// } +// +// private AIType! typeParameter; +// public AIType! TypeParameter { get { return typeParameter; } } +// +// /// +// /// List should not be instantiated from the outside. +// /// +// private List(AIType! typeParameter) +// { +// this.typeParameter = typeParameter; +// } +// } +// +// public class Pair : Value +// { +// private static IDictionary! pairs = new Hashtable(); +// public static AIType! Type(AIType! type1, AIType! type2) +// { +// Microsoft.AbstractInterpretationFramework.Collections.Pair typpair +// = new Microsoft.AbstractInterpretationFramework.Collections.Pair(type1, type2); +// +// if (pairs.Contains(typpair)) +// return pairs[typpair]; +// else +// { +// AIType! result = new Pair(type1, type2); +// pairs[typpair] = result; +// return result; +// } +// } +// +// private static IDictionary! constructs = new Hashtable(); +// public static FunctionSymbol! Pair(AIType! type1, AIType! type2) +// { +// Microsoft.AbstractInterpretationFramework.Collections.Pair typpair +// = new Microsoft.AbstractInterpretationFramework.Collections.Pair(type1, type2); +// +// if (constructs.Contains(typpair)) +// return constructs[typpair]; +// else +// { +// FunctionSymbol! result = new FunctionSymbol( +// new FunctionType(type1, type2, Type(type1, type2)) +// ); +// constructs[typpair] = result; +// return result; +// } +// } +// +// protected AIType! type1; +// protected AIType! type2; +// +// public AIType! Type1 { get { return type1; } } +// public AIType! Type2 { get { return type2; } } +// +// /// +// /// Pair should not be instantiated from the outside, except by subclasses. +// /// +// protected Pair(AIType! type1, AIType! type2) +// { +// this.type1 = type1; +// this.type2 = type2; +// } +// } + + //-------------------------- Propositions --------------------------- + + + /// + /// A class with global propositional symbols and the Prop.Type. + /// + public sealed class Prop : AIType + { + private static readonly AIType! proptype = new Prop(); + public static AIType! Type { get { 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); + + + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! False { get { return _false; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! True { get { return _true; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Not { get { return _not; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! And { [Pure] get { return _and; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Or { get { return _or; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Implies { get { return _implies; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Exists { get { return _exists; } } + [Pure][Reads(ReadsAttribute.Reads.Nothing)] public static FunctionSymbol! Forall { get { return _forall; } } + + + /// + /// Prop should not be instantiated from the outside. + /// + private Prop() { } + + + + // + // Utility Methods + // + + public static IExpr! SimplifiedAnd(IPropExprFactory! factory, IExpr! e0, IExpr! e1) + { + IFunApp fun0 = e0 as IFunApp; + if (fun0 != null) + { + if (fun0.FunctionSymbol.Equals(Prop.True)) + { + return e1; + } + else if (fun0.FunctionSymbol.Equals(Prop.False)) + { + return e0; + } + } + + IFunApp fun1 = e1 as IFunApp; + if (fun1 != null) + { + if (fun1.FunctionSymbol.Equals(Prop.True)) + { + return e0; + } + else if (fun1.FunctionSymbol.Equals(Prop.False)) + { + return e1; + } + } + + return factory.And(e0, e1); + } + + public static IExpr! SimplifiedAnd(IPropExprFactory! factory, IEnumerable/**/! exprs) + { + IExpr! result = factory.True; + foreach (IExpr! conjunct in exprs) + { + result = SimplifiedAnd(factory, result, conjunct); + } + return result; + } + + public static IExpr! SimplifiedOr(IPropExprFactory! factory, IExpr! e0, IExpr! e1) + { + IFunApp fun0 = e0 as IFunApp; + if (fun0 != null) + { + if (fun0.FunctionSymbol.Equals(Prop.False)) + { + return e1; + } + else if (fun0.FunctionSymbol.Equals(Prop.True)) + { + return e0; + } + } + + IFunApp fun1 = e1 as IFunApp; + if (fun1 != null) + { + if (fun1.FunctionSymbol.Equals(Prop.False)) + { + return e0; + } + else if (fun1.FunctionSymbol.Equals(Prop.True)) + { + return e1; + } + } + + return factory.Or(e0, e1); + } + + public static IExpr! SimplifiedOr(IPropExprFactory! factory, IEnumerable/**/! exprs) + { + IExpr! result = factory.False; + foreach (IExpr! disj in exprs) + { + result = SimplifiedOr(factory, result, disj); + } + return result; + } + + + + /// + /// Break top-level conjuncts into a list of sub-expressions. + /// + /// The expression to examine. + /// A list of conjuncts. + internal static IList/**/! BreakConjuncts(IExpr! e) + ensures forall{ IExpr sub in result; sub is IFunApp ==> !((IFunApp) sub).FunctionSymbol.Equals(Prop.And) }; + { + return BreakJuncts(e, Prop.And); + } + + /// + /// Break top-level disjuncts into a list of sub-expressions. + /// + /// The expression to examine. + /// A list of conjuncts. + internal static IList/**/! BreakDisjuncts(IExpr! e) + ensures forall{ IExpr sub in result; sub is IFunApp ==> !((IFunApp) sub).FunctionSymbol.Equals(Prop.Or) }; + { + return BreakJuncts(e, Prop.Or); + } + + private static IList/**/! BreakJuncts(IExpr! e, IFunctionSymbol! sym) + ensures forall{ IExpr sub in result; sub is IFunApp ==> !((IFunApp) sub).FunctionSymbol.Equals(sym) }; + { + ArrayList/**/! result = new ArrayList(); + + IFunApp f = e as IFunApp; + if (f != null) + { + // If it is a sym, go down into sub-expressions. + if (f.FunctionSymbol.Equals(sym)) + { + foreach (IExpr! arg in f.Arguments) + { + result.AddRange(BreakJuncts(arg,sym)); + } + } + // Otherwise, stop. + else + { + result.Add(e); + } + } + else + { + result.Add(e); + } + + return result; + } + } + + /// + /// A callback to produce a function body given the bound variable. + /// + /// The bound variable to use. + /// The function body. + public delegate IExpr! FunctionBody(IVariable! var); + + /// + /// An interface for constructing propositional expressions. + /// + /// This interface should be implemented by the client. An implementation of + /// of this class should generally be used as a singleton object. + /// + 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);*/; + } + + /// + /// Like IPropExprFactory, but also with quantifiers. + /// + public interface IQuantPropExprFactory : IPropExprFactory { + /// + /// Produce an existential given the lambda-expression. + /// + /// The lambda-expression. + /// The existential. + IFunApp! Exists(IFunction! p) /*ensures result.FunctionSymbol.Equals(Prop.Exists);*/; + IFunApp! Forall(IFunction! p) /*ensures result.FunctionSymbol.Equals(Prop.Forall);*/; + + /// + /// 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. + /// + /// The function body callback. + /// The existential. + IFunApp! Exists(AIType paramType, FunctionBody! body) /*ensures result.FunctionSymbol.Equals(Prop.Exists);*/; + IFunApp! Forall(AIType paramType, FunctionBody! body) /*ensures result.FunctionSymbol.Equals(Prop.Forall);*/; + } + + /// + /// 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. + /// + 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);*/; + } + + /// + /// 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. + /// + 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);*/ } + } + + /// + /// 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. + /// + public interface IIntExprFactory : IValueExprFactory + { + IFunApp! Const(BigNum i) /*ensures result.FunctionSymbol.Equals(new IntSymbol(i));*/; + } + + /// + /// 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. + /// + public interface ILinearExprFactory : IIntExprFactory + { + IFunApp! AtMost(IExpr! e0, IExpr! e1) /*ensures result.FunctionSymbol.Equals(Value.AtMost);*/; + IFunApp! Add(IExpr! e0, IExpr! e1) /*ensures result.FunctionSymbol.Equals(Value.Add);*/; + /// + /// If "var" is null, returns an expression representing r. + /// Otherwise, returns an expression representing r*var. + /// + IExpr! Term(Microsoft.Basetypes.Rational r, IVariable var); + + IFunApp! False { get /*ensures result.FunctionSymbol.Equals(Prop.False);*/; } + IFunApp! True { get /*ensures result.FunctionSymbol.Equals(Prop.True);*/; } + IFunApp! And(IExpr! p, IExpr! q) /*ensures result.FunctionSymbol.Equals(Prop.And);*/; + } + + /// + /// 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. + /// + public interface ITypeExprFactory + { + /// + /// Returns an expression denoting the top of the type hierarchy. + /// + IExpr! RootType { get; } + + /// + /// Returns true iff "t" denotes a type constant. + /// + [Pure][Reads(ReadsAttribute.Reads.Owned)] + bool IsTypeConstant(IExpr! t); + + /// + /// Returns true iff t0 and t1 are types such that t0 and t1 are equal. + /// + [Pure][Reads(ReadsAttribute.Reads.Owned)] + bool IsTypeEqual(IExpr! t0, IExpr! t1); + + /// + /// Returns true iff t0 and t1 are types such that t0 is a subtype of t1. + /// + [Pure][Reads(ReadsAttribute.Reads.Owned)] + bool IsSubType(IExpr! t0, IExpr! t1); + + /// + /// Returns the most derived supertype of both "t0" and "t1". A precondition is + /// that "t0" and "t1" both represent types. + /// + IExpr! JoinTypes(IExpr! t0, IExpr! t1); + + IFunApp! IsExactlyA(IExpr! e, IExpr! type) /*requires IsTypeConstant(type); ensures result.FunctionSymbol.Equals(Value.Eq);*/; + IFunApp! IsA(IExpr! e, IExpr! type) /*requires IsTypeConstant(type); ensures result.FunctionSymbol.Equals(Value.Subtype);*/; + } + +} -- cgit v1.2.3