Removed AIFramework from Boogie -- use native trivial or native interval-based abstract interpretation instead.

Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie.
Command-line option '/logInfer' has been dropped.

10 files changed, 14 insertions, 1115 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 9df982d9..b64a9e5e 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -11,56 +11,40 @@ namespace Microsoft.Boogie.AbstractInterpretation {
   using System.Diagnostics.Contracts;

   using System.Collections;

   using System.Collections.Generic;

-  using AI = Microsoft.AbstractInterpretationFramework;

 

   public class CallSite {

     public readonly Implementation/*!*/ Impl;

     public readonly Block/*!*/ Block;

     public readonly int Statement; // invariant: Block[Statement] is CallCmd

-    public readonly AI.Lattice.Element/*!*/ KnownBeforeCall;

     public readonly ProcedureSummaryEntry/*!*/ SummaryEntry;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(Impl != null);

       Contract.Invariant(Block != null);

-      Contract.Invariant(KnownBeforeCall != null);

       Contract.Invariant(SummaryEntry != null);

     }

 

 

-    public CallSite(Implementation impl, Block b, int stmt, AI.Lattice.Element e, ProcedureSummaryEntry summaryEntry) {

+    public CallSite(Implementation impl, Block b, int stmt, ProcedureSummaryEntry summaryEntry) {

       Contract.Requires(summaryEntry != null);

-      Contract.Requires(e != null);

       Contract.Requires(b != null);

       Contract.Requires(impl != null);

       this.Impl = impl;

       this.Block = b;

       this.Statement = stmt;

-      this.KnownBeforeCall = e;

       this.SummaryEntry = summaryEntry;

     }

   }

 

   public class ProcedureSummaryEntry {

-    public AI.Lattice/*!*/ Lattice;

-    public AI.Lattice.Element/*!*/ OnEntry;

-    public AI.Lattice.Element/*!*/ OnExit;

     public HashSet<CallSite>/*!*/ ReturnPoints; // whenever OnExit changes, we start analysis again at all the ReturnPoints

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(Lattice != null);

-      Contract.Invariant(OnEntry != null);

-      Contract.Invariant(OnExit != null);

       Contract.Invariant(ReturnPoints != null);

     }

 

 

-    public ProcedureSummaryEntry(AI.Lattice lattice, AI.Lattice.Element onEntry) {

-      Contract.Requires(onEntry != null);

-      Contract.Requires(lattice != null);

-      this.Lattice = lattice;

-      this.OnEntry = onEntry;

-      this.OnExit = lattice.Bottom;

+    public ProcedureSummaryEntry() {

       this.ReturnPoints = new HashSet<CallSite>();

       // base();

     }

@@ -93,7 +77,6 @@ namespace Microsoft.Boogie {
   using System.Collections.Generic;

   using System.Diagnostics.Contracts;

   using Microsoft.Boogie.AbstractInterpretation;

-  using AI = Microsoft.AbstractInterpretationFramework;

   using Graphing;

   using Set = GSet<object>;

 

@@ -349,12 +332,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public void InstrumentWithInvariants() {

-      foreach (Declaration d in this.TopLevelDeclarations) {

-        d.InstrumentWithInvariants();

-      }

-    }

-

     /// <summary>

     /// Reset the abstract stated computed before

     /// </summary>

@@ -1045,14 +1022,6 @@ namespace Microsoft.Boogie {
     }

 

     /// <summary>

-    /// This method inserts the abstract-interpretation-inferred invariants

-    /// as assume (or possibly assert) statements in the statement sequences of

-    /// each block.

-    /// </summary>

-    public virtual void InstrumentWithInvariants() {

-    }

-

-    /// <summary>

     /// Reset the abstract stated computed before

     /// </summary>

     public virtual void ResetAbstractInterpretationState() { /* does nothing */

@@ -1388,7 +1357,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public abstract class Variable : NamedDeclaration, AI.IVariable {

+  public abstract class Variable : NamedDeclaration {

     public TypedIdent/*!*/ TypedIdent;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -1446,11 +1415,6 @@ namespace Microsoft.Boogie {
       TypecheckAttributes(tc);

       this.TypedIdent.Typecheck(tc);

     }

-    [Pure]

-    public object DoVisit(AI.ExprVisitor visitor) {

-      //Contract.Requires(visitor != null);

-      return visitor.VisitVariable(this);

-    }

   }

 

   public class VariableComparer : IComparer {

@@ -2354,12 +2318,6 @@ namespace Microsoft.Boogie {
         for (int s = 0; s < this.Summary.Count; s++) {

           ProcedureSummaryEntry/*!*/ entry = cce.NonNull(this.Summary[s]);

           stream.Write(level + 1, "// ");

-          Expr e;

-          e = (Expr)entry.Lattice.ToPredicate(entry.OnEntry);

-          e.Emit(stream);

-          stream.Write("   ==>   ");

-          e = (Expr)entry.Lattice.ToPredicate(entry.OnExit);

-          e.Emit(stream);

           stream.WriteLine();

         }

       }

@@ -2862,53 +2820,6 @@ namespace Microsoft.Boogie {
     }

 

     /// <summary>

-    /// Instrument the blocks with the inferred invariants

-    /// </summary>

-    public override void InstrumentWithInvariants() {

-      foreach (Block b in this.Blocks) {

-        if (b.Lattice != null) {

-          Contract.Assert(b.PreInvariant != null);      /* If the pre-abstract state is null, then something is wrong */

-          Contract.Assert(b.PostInvariant != null);      /* If the post-state is null, then something is wrong */

-

-          bool instrumentEntry;

-          bool instrumentExit;

-          switch (CommandLineOptions.Clo.InstrumentInfer) {

-            case CommandLineOptions.InstrumentationPlaces.Everywhere:

-              instrumentEntry = true;

-              instrumentExit = true;

-              break;

-            case CommandLineOptions.InstrumentationPlaces.LoopHeaders:

-              instrumentEntry = b.widenBlock;

-              instrumentExit = false;

-              break;

-            default: {

-                Contract.Assert(false);

-                throw new cce.UnreachableException();

-              } // unexpected InstrumentationPlaces value

-          }

-

-          if (instrumentEntry || instrumentExit) {

-            CmdSeq newCommands = new CmdSeq();

-            if (instrumentEntry) {

-              Expr inv = (Expr)b.Lattice.ToPredicate(b.PreInvariant); /*b.PreInvariantBuckets.GetDisjunction(b.Lattice);*/

-              var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);

-              PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv, kv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv, kv);

-              newCommands.Add(cmd);

-            }

-            newCommands.AddRange(b.Cmds);

-            if (instrumentExit) {

-              Expr inv = (Expr)b.Lattice.ToPredicate(b.PostInvariant);

-              var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);

-              PredicateCmd cmd = CommandLineOptions.Clo.InstrumentWithAsserts ? (PredicateCmd)new AssertCmd(Token.NoToken, inv, kv) : (PredicateCmd)new AssumeCmd(Token.NoToken, inv, kv);

-              newCommands.Add(cmd);

-            }

-            b.Cmds = newCommands;

-          }

-        }

-      }

-    }

-

-    /// <summary>

     /// Return a collection of blocks that are reachable from the block passed as a parameter.

     /// The block must be defined in the current implementation

     /// </summary>

@@ -3148,113 +3059,6 @@ namespace Microsoft.Boogie {
     }

   }

 

-  /// <summary>

-  /// Conceptually, a LatticeElementList is a infinite array indexed from 0,

-  /// where some finite number of elements have a non-null value.  All elements

-  /// have type Lattice.Element.

-  ///

-  /// The Count property returns the first index above all non-null values.

-  ///

-  /// The [i] getter returns the element at position i, which may be null.  The

-  /// index i is not allowed to be negative.

-  /// The [i] setter sets the element at position i.  As a side effect, this

-  /// operation may increase Count.  The index i is not allowed to be negative.

-  /// The right-hand value of the setter is not allowed to be null; that is,

-  /// null can occur in the list only as an "unused" element.

-  /// </summary>

-  public class LatticeElementList : ArrayList {

-    public new /*Maybe null*/ AI.Lattice.Element this[int i] {

-      get {

-        if (i < Count) {

-          return (AI.Lattice.Element)base[i];

-        } else {

-          return null;

-        }

-      }

-      set {

-        System.Diagnostics.Debug.Assert(value != null);

-        while (Count <= i) {

-          Add(null);

-        }

-        base[i] = value;

-      }

-    }

-    /// <summary>

-    /// Returns the disjunction of (the expression formed from) the

-    /// non-null lattice elements in the list.  The expressions are

-    /// formed according to the given "lattice", which is assumed to

-    /// be the lattice of the lattice elements stored in the list.

-    /// </summary>

-    /// <param name="lattice"></param>

-    /// <returns></returns>

-    public Expr GetDisjunction(AI.Lattice lattice) {

-      Contract.Requires(lattice != null);

-      Expr disjunction = null;

-      foreach (AI.Lattice.Element el in this) {

-        if (el != null) {

-          Expr e = (Expr)lattice.ToPredicate(el);

-          if (disjunction == null) {

-            disjunction = e;

-          } else {

-            disjunction = Expr.Or(disjunction, e);

-          }

-        }

-      }

-      if (disjunction == null) {

-        return Expr.False;

-      } else {

-        return disjunction;

-      }

-    }

-  }

-

-  public abstract class BoogieFactory {

-    public static Expr IExpr2Expr(AI.IExpr e) {

-      Contract.Requires(e != null);

-      Contract.Ensures(Contract.Result<Expr>() != null);

-      Variable v = e as Variable;

-      if (v != null) {

-        return new IdentifierExpr(Token.NoToken, v);

-      } else if (e is AI.IVariable) { // but not a Variable

-        return new AIVariableExpr(Token.NoToken, (AI.IVariable)e);

-      } else if (e is IdentifierExpr.ConstantFunApp) {

-        return ((IdentifierExpr.ConstantFunApp)e).IdentifierExpr;

-      } else if (e is QuantifierExpr.AIQuantifier) {

-        return ((QuantifierExpr.AIQuantifier)e).arg.RealQuantifier;

-      } else {

-        return (Expr)e;

-      }

-    }

-    public static ExprSeq IExprArray2ExprSeq(IList/*<AI.IExpr!>*/ a) {

-      Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<ExprSeq>() != null);

-      Expr[] e = new Expr[a.Count];

-      int i = 0;

-      foreach (AI.IExpr/*!*/ aei in a) {

-        Contract.Assert(aei != null);

-        e[i] = IExpr2Expr(aei);

-        i++;

-      }

-      return new ExprSeq(e);

-    }

-

-    // Convert a Boogie type into an AIType if possible.  This should be

-    // extended when AIFramework gets more types.

-    public static AI.AIType Type2AIType(Type t) {

-      Contract.Requires(t != null);

-      Contract.Ensures(Contract.Result<AI.AIType>() != null);

-      //      if (t.IsRef)

-      //        return AI.Ref.Type;

-      //      else

-      if (t.IsInt)

-        return AI.Int.Type;

-      //      else if (t.IsName)               PR: how to handle this case?

-      //        return AI.FieldName.Type;

-      else

-        return AI.Value.Type;

-    }

-  }

-

   #region Generic Sequences

   //---------------------------------------------------------------------

   // Generic Sequences

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index c6b66585..607848ed 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -13,7 +13,6 @@ namespace Microsoft.Boogie {
   using System.Diagnostics;

   using System.Collections.Generic;

   using Microsoft.Boogie.AbstractInterpretation;

-  using AI = Microsoft.AbstractInterpretationFramework;

   using System.Diagnostics.Contracts;

   using Set = GSet<object>;

 

@@ -818,13 +817,6 @@ namespace Microsoft.Boogie {
     public bool widenBlock;

     public int iterations;         // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not

 

-    // Block-specific invariants...

-    public AI.Lattice Lattice;    // The lattice used for the analysis of this block

-    public AI.Lattice.Element PreInvariant;   // The initial abstract states for this block

-    public AI.Lattice.Element PostInvariant;  // The exit abstract states for this block

-    // KRML: We want to include the following invariant, but at the moment, doing so causes a run-time error (something about committed):

-    //invariant ;

-

     // VC generation and SCC computation

     public BlockSeq/*!*/ Predecessors;

 

@@ -837,7 +829,6 @@ namespace Microsoft.Boogie {
       Contract.Invariant(Label != null);

       Contract.Invariant(Cmds != null);

       Contract.Invariant(cce.NonNullElements(liveVarsBefore, true));

-      Contract.Invariant((PreInvariant != null) == (PostInvariant != null));

     }

 

     public bool IsLive(Variable v) {

@@ -860,8 +851,6 @@ namespace Microsoft.Boogie {
       this.Label = label;

       this.Cmds = cmds;

       this.TransferCmd = transferCmd;

-      this.PreInvariant = null;

-      this.PostInvariant = null;

       this.Predecessors = new BlockSeq();

       this.liveVarsBefore = null;

       this.TraversingStatus = VisitState.ToVisit;

@@ -920,9 +909,6 @@ namespace Microsoft.Boogie {
       //      this.currentlyTraversed = false;

       this.TraversingStatus = VisitState.ToVisit;

       this.iterations = 0;

-      this.Lattice = null;

-      this.PreInvariant = null;

-      this.PostInvariant = null;

     }

 

     [Pure]

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index e274fcc3..f2ed5790 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -13,8 +13,6 @@ namespace Microsoft.Boogie {
   using System.Diagnostics;

   using System.Collections.Generic;

   using Microsoft.Boogie.AbstractInterpretation;

-  using AI = Microsoft.AbstractInterpretationFramework;

-  using Microsoft.AbstractInterpretationFramework;//DANGER: Added?

   using System.Diagnostics.Contracts;

   using Microsoft.Basetypes;

 

@@ -379,21 +377,6 @@ namespace Microsoft.Boogie {
       args.Add(subexpr);

       return new NAryExpr(x, new TypeCoercion(x, type), args);

     }

-

-

-    /// <summary>

-    /// This property returns a representation for the expression suitable for use

-    /// by the AIFramework.  Usually, the property just returns "this", but not

-    /// every Expr is an AI.IExpr (besides, AI.IExpr is to be thought of as an

-    /// abstract interface--any class that implements AI.IExpr is supposed to

-    /// implement some proper subinterface of AI.IExpr).

-    /// The converse operations of this property are found in AbsInt\ExprFactories.ssc.

-    /// </summary>

-    public abstract AI.IExpr/*!*/ IExpr {

-      [Peer]

-      get;

-    }

-

   }

   [ContractClassFor(typeof(Expr))]

   public abstract class ExprContracts : Expr {

@@ -415,16 +398,9 @@ namespace Microsoft.Boogie {
         throw new NotImplementedException();

       }

     }

-    public override Microsoft.AbstractInterpretationFramework.IExpr IExpr {

-      get {

-        Contract.Ensures(Contract.Result<Microsoft.AbstractInterpretationFramework.IExpr>() != null);

-

-        throw new NotImplementedException();

-      }

-    }

   }

 

-  public class LiteralExpr : Expr, AI.IFunApp {

+  public class LiteralExpr : Expr {

     public readonly object/*!*/ Val;  // false, true, a BigNum, or a BvConst

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -532,12 +508,6 @@ namespace Microsoft.Boogie {
         return Val is bool && ((bool)Val) == true;

       }

     }

-    public override AI.IExpr/*!*/ IExpr {

-      get {

-        Contract.Ensures(Contract.Result<AI.IExpr>() != null);

-        return this;

-      }

-    }

 

     // should be eliminated after converting everything to BigNums

     private int asInt {

@@ -572,64 +542,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public AI.IFunctionSymbol/*!*/ FunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-

-        if (Val is bool) {

-          if ((bool)Val) {

-            return AI.Prop.True;

-          } else {

-            return AI.Prop.False;

-          }

-        } else if (Val is BigNum) {

-          return AI.Int.Const((BigNum)Val);

-        } else if (Val is BvConst) {

-          return AI.Bv.Const(((BvConst)Val).Value, ((BvConst)Val).Bits);

-        } else {

-          {

-            Contract.Assert(false);

-            throw new cce.UnreachableException();

-          } // like, where did this value come from?!

-        }

-      }

-    }

-    public IList/*<AI.IExpr!>*//*!*/ Arguments {

-      get {

-        Contract.Ensures(Contract.Result<IList>() != null);

-

-        return ArrayList.ReadOnly(new AI.IExpr[0]);

-      }

-    }

-    public Microsoft.AbstractInterpretationFramework.IFunApp CloneWithArguments(IList/*<AI.IExpr!>*/ args) {

-      //Contract.Requires(args != null);

-      Contract.Ensures(Contract.Result<Microsoft.AbstractInterpretationFramework.IFunApp>() != null);

-      Contract.Assert(args.Count == 0);

-      return this;

-    }

-    public AI.AIType/*!*/ AIType {

-      get {

-        Contract.Requires(AIType != null);

-        if (Val is bool) {

-          return AI.Prop.Type;

-        } else if (Val is BigNum) {

-          return AI.Int.Type;

-        } else if (Val is BvConst) {

-          return AI.Bv.Type;

-        } else {

-          {

-            Contract.Assert(false);

-            throw new cce.UnreachableException();

-          } // like, where did this value come from?!

-        }

-      }

-    }

-    [Pure]

-    public object DoVisit(AI.ExprVisitor visitor) {

-      //Contract.Requires(visitor != null);

-      return visitor.VisitFunApp(this);

-    }

-

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

       Contract.Ensures(Contract.Result<Absy>() != null);

@@ -688,86 +600,6 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public class AIVariableExpr : Expr {

-

-    public string Name;     // identifier symbol

-    public AI.IVariable/*!*/ Decl;   // identifier declaration

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(Decl != null);

-    }

-

-

-    /// <summary>

-    /// Creates an unresolved identifier expression.

-    /// </summary>

-    /// <param name="tok"></param>

-    /// <param name="name"></param>

-    public AIVariableExpr(IToken/*!*/ tok, AI.IVariable/*!*/ var)

-      : base(tok) {

-      Contract.Requires(tok != null);

-      Contract.Requires(var != null);

-      Name = var.ToString();

-      Decl = var;

-    }

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]

-    public override bool Equals(object obj) {

-      if (obj == null)

-        return false;

-      if (!(obj is AIVariableExpr))

-        return false;

-

-      AIVariableExpr other = (AIVariableExpr)obj;

-      return object.Equals(this.Name, other.Name) && object.Equals(this.Decl, other.Decl);

-    }

-    [Pure]

-    public override int GetHashCode() {

-      int h = this.Name == null ? 0 : this.Name.GetHashCode();

-      h ^= this.Decl == null ? 0 : this.Decl.GetHashCode();

-      return h;

-    }

-    public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

-      //Contract.Requires(stream != null);

-      if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

-        stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h" + this.Decl.GetHashCode());

-      }

-      stream.Write(this, "{0}", this.Name);

-    }

-    public override void Resolve(ResolutionContext rc) {

-      //Contract.Requires(rc != null);

-    }

-    public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {

-      //Contract.Requires(freeVars != null);

-      if (Decl is Variable) {

-        freeVars.Add((Variable)Decl);

-      }

-    }

-    public override void Typecheck(TypecheckingContext tc) {

-      //Contract.Requires(tc != null);

-      throw new System.NotImplementedException();

-    }

-    public override Type/*!*/ ShallowType {

-      get {

-        Contract.Ensures(Contract.Result<Type>() != null);

-        throw new System.NotImplementedException();

-      }

-    }

-    public override AI.IExpr/*!*/ IExpr {

-      get {

-        Contract.Ensures(Contract.Result<AI.IExpr>() != null);

-

-        return Decl;

-      }

-    }

-

-    public override Absy StdDispatch(StandardVisitor visitor) {

-      //Contract.Requires(visitor != null);

-      Contract.Ensures(Contract.Result<Absy>() != null);

-      return visitor.VisitAIVariableExpr(this);

-    }

-  }

-

   public class IdentifierExpr : Expr {

     public string/*!*/ Name;    // identifier symbol

     public Variable Decl;   // identifier declaration

@@ -894,12 +726,11 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public sealed class ConstantFunApp : AI.IFunApp {

+    public sealed class ConstantFunApp {

       private IdentifierExpr/*!*/ identifierExpr;

       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(identifierExpr != null);

-        Contract.Invariant(symbol != null);

         Contract.Invariant(emptyArgs != null);

       }

 

@@ -910,14 +741,6 @@ namespace Microsoft.Boogie {
         }

       }

 

-      private AI.IFunctionSymbol/*!*/ symbol;

-      public AI.IFunctionSymbol/*!*/ FunctionSymbol {

-        get {

-          Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-          return symbol;

-        }

-      }

-

       private static IList/*!*/ emptyArgs = ArrayList.ReadOnly(cce.NonNull((IList/*!*/)new ArrayList()));

       public IList/*!*/ Arguments {

         get {

@@ -926,44 +749,14 @@ namespace Microsoft.Boogie {
         }

       }

 

-      public AI.IFunApp CloneWithArguments(IList newargs) {

-        //Contract.Requires(newargs != null);

-        Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

-        return this;

-      }

-

-      [Pure]

-      public object DoVisit(AI.ExprVisitor visitor) {

-        //Contract.Requires(visitor != null);

-        return visitor.VisitFunApp(this);

-      }

-

       public ConstantFunApp(IdentifierExpr ie, Constant c) {

         Contract.Requires(c != null);

         Contract.Requires(ie != null);

         this.identifierExpr = ie;

-        this.symbol =

-            new AI.NamedSymbol(c.TypedIdent.Name, BoogieFactory.Type2AIType(c.TypedIdent.Type));

         // base();

       }

 

     }

-    private AI.IExpr iexprCache = null;

-    public override AI.IExpr/*!*/ IExpr {

-      get {

-        Contract.Ensures(Contract.Result<IExpr>() != null);

-

-        if (iexprCache == null) {

-          if (Decl is Constant)

-            iexprCache = new ConstantFunApp(this, (Constant)Decl);

-          else {

-            Contract.Assume(this.Decl != null);

-            iexprCache = Decl;

-          }

-        }

-        return iexprCache;

-      }

-    }

 

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

@@ -972,7 +765,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public class OldExpr : Expr, AI.IFunApp // HACK

+  public class OldExpr : Expr

   {

     public Expr/*!*/ Expr;

     [ContractInvariantMethod]

@@ -1030,67 +823,6 @@ namespace Microsoft.Boogie {
         return Expr.ShallowType;

       }

     }

-    public override AI.IExpr/*!*/ IExpr {

-      get {

-        Contract.Ensures(Contract.Result<IExpr>() != null);

-

-        // Put back these lines when "HACK" removed

-        //            // An Old expression has no AI.IExpr representation

-        //           {Contract.Assert(false);throw new cce.UnreachableException();}

-        return this;  // HACK

-      }

-    }

-    [Pure]

-    public object DoVisit(AI.ExprVisitor visitor) {

-      //Contract.Requires(visitor != null);

-      return visitor.VisitFunApp(this);

-    }

-    public AI.IFunApp CloneWithArguments(IList/*<IExpr!>*/ args) {

-      //Contract.Requires(args != null);

-      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

-      Contract.Assume(args.Count == 1);

-      AI.IExpr/*!*/ iexpr = (AI.IExpr)cce.NonNull(args[0]);

-      return new OldExpr(Token.NoToken, BoogieFactory.IExpr2Expr(iexpr));

-    }

-    private IList/*?*/ argCache = null;

-    public IList/*<IExpr!*//*!*/ Arguments {

-

-      get {

-        Contract.Ensures(Contract.Result<IList>() != null);

-

-        if (argCache == null) {

-          IList l = new ArrayList(1);

-          l.Add(Expr.IExpr);

-          argCache = ArrayList.ReadOnly(l);

-        }

-        return argCache;

-      }

-    }

-    private sealed class OldFunctionSymbol : AI.IFunctionSymbol {

-      private static readonly AI.AIType/*!*/ aitype = new AI.FunctionType(AI.Value.Type, AI.Value.Type);

-

-      public AI.AIType/*!*/ AIType {

-        get {

-          Contract.Ensures(Contract.Result<AIType>() != null);

-          return aitype;

-        }

-      }

-      private OldFunctionSymbol() {

-      }

-      internal static readonly OldFunctionSymbol/*!*/ Sym = new OldFunctionSymbol();

-

-      [Pure]

-      public override string ToString() {

-        Contract.Ensures(Contract.Result<string>() != null);

-        return "old";

-      }

-    }

-    public AI.IFunctionSymbol/*!*/ FunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-        return OldFunctionSymbol.Sym;

-      }

-    }

 

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

@@ -1198,10 +930,6 @@ namespace Microsoft.Boogie {
     /// </summary>

     Type/*!*/ ShallowType(ExprSeq/*!*/ args);

 

-    AI.IFunctionSymbol/*!*/ AIFunctionSymbol {

-      get;

-    }

-

     T Dispatch<T>(IAppliableVisitor<T>/*!*/ visitor);

   }

   [ContractClassFor(typeof(IAppliable))]

@@ -1250,13 +978,6 @@ namespace Microsoft.Boogie {
       throw new NotImplementedException();

     }

 

-    public IFunctionSymbol AIFunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-        throw new NotImplementedException();

-      }

-    }

-

     public T Dispatch<T>(IAppliableVisitor<T> visitor) {

       Contract.Requires(visitor != null);

       throw new NotImplementedException();

@@ -1334,19 +1055,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-

-        switch (this.op) {

-          case Opcode.Not:

-            return AI.Prop.Not;

-        }

-        System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString());

-        throw new Exception();

-      }

-    }

-

     public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

       //Contract.Requires(stream != null);

       //Contract.Requires(args != null);

@@ -1537,50 +1245,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-

-        switch (this.op) {

-

-          case Opcode.Add:

-            return AI.Int.Add;

-          case Opcode.Sub:

-            return AI.Int.Sub;

-          case Opcode.Mul:

-            return AI.Int.Mul;

-          case Opcode.Div:

-            return AI.Int.Div;

-          case Opcode.Mod:

-            return AI.Int.Mod;

-          case Opcode.Eq:

-            return AI.Value.Eq;

-          case Opcode.Neq:

-            return AI.Value.Neq;

-          case Opcode.Gt:

-            return AI.Int.Greater;

-          case Opcode.Ge:

-            return AI.Int.AtLeast;

-          case Opcode.Lt:

-            return AI.Int.Less;

-          case Opcode.Le:

-            return AI.Int.AtMost;

-          case Opcode.And:

-            return AI.Prop.And;

-          case Opcode.Or:

-            return AI.Prop.Or;

-          case Opcode.Imp:

-            return AI.Prop.Implies;

-          case Opcode.Iff:

-            return AI.Value.Eq;

-          case Opcode.Subtype:

-            return AI.Value.Subtype;

-        }

-        System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString());

-        throw new Exception();

-      }

-    }

-

     public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

       //Contract.Requires(stream != null);

       //Contract.Requires(args != null);

@@ -1917,7 +1581,7 @@ namespace Microsoft.Boogie {
 

   }

 

-  public class FunctionCall : IAppliable, AI.IFunctionSymbol {

+  public class FunctionCall : IAppliable {

     private IdentifierExpr/*!*/ name;

     public Function Func;

     public FunctionCall(IdentifierExpr name) {

@@ -1940,25 +1604,6 @@ namespace Microsoft.Boogie {
       Contract.Invariant(name != null);

     }

 

-    public FunctionCall createUnresolvedCopy()

-    {

-        return new FunctionCall(new IdentifierExpr(name.tok, name.Name, name.Type));

-    }

-

-    public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-

-        if (name.Name == "$typeof") {

-          return AI.Value.Typeof;

-        } else if (name.Name == "$allocated") {

-          return AI.FieldName.Allocated;

-        } else {

-          return this;

-        }

-      }

-    }

-

     [Pure]

     public override string ToString() {

       Contract.Ensures(Contract.Result<string>() != null);

@@ -1977,15 +1622,6 @@ namespace Microsoft.Boogie {
       return Func.GetHashCode();

     }

 

-    public AI.AIType/*!*/ AIType {

-      get {

-        Contract.Ensures(Contract.Result<AIType>() != null);

-

-        Contract.Assume(this.Func != null);

-        return AI.Value.FunctionType(this.Func.InParams.Length);

-      }

-    }

-

     virtual public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {

       //Contract.Requires(stream != null);

       //Contract.Requires(args != null);

@@ -2139,16 +1775,6 @@ namespace Microsoft.Boogie {
       return this.Type;

     }

 

-    public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-

-        // not really clear what should be returned here ...

-        // should the operation be completely invisible for the abstract interpretation?

-        return AI.Heap.UnsupportedHeapOp;

-      }

-    }

-

     public T Dispatch<T>(IAppliableVisitor<T> visitor) {

       //Contract.Requires(visitor != null);

       return visitor.Visit(this);

@@ -2156,7 +1782,7 @@ namespace Microsoft.Boogie {
 

   }

 

-  public class NAryExpr : Expr, AI.IFunApp {

+  public class NAryExpr : Expr {

     [Additive]

     [Peer]

     public IAppliable/*!*/ Fun;

@@ -2264,44 +1890,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public override AI.IExpr/*!*/ IExpr {

-      get {

-        Contract.Ensures(Contract.Result<IExpr>() != null);

-

-        return this;

-      }

-    }

-    public AI.IFunctionSymbol/*!*/ FunctionSymbol {

-      get {

-

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-

-        return Fun.AIFunctionSymbol;

-      }

-    }

-    public IList/*<AI.IExpr!>*//*!*/ Arguments {

-      get {

-        Contract.Ensures(Contract.Result<IList>() != null);

-

-        AI.IExpr[] a = new AI.IExpr[Args.Length];

-        for (int i = 0; i < Args.Length; i++) {

-          a[i] = cce.NonNull(Args[i]).IExpr;

-        }

-        return ArrayList.ReadOnly(a);

-      }

-    }

-    public AI.IFunApp CloneWithArguments(IList/*<AI.IExpr!>*/ args) {

-      //Contract.Requires(args != null);

-      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

-      return new NAryExpr(this.tok, this.Fun, BoogieFactory.IExprArray2ExprSeq(args));

-    }

-

-    [Pure]

-    public object DoVisit(AI.ExprVisitor visitor) {

-      //Contract.Requires(visitor != null);

-      return visitor.VisitFunApp(this);

-    }

-

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

       Contract.Ensures(Contract.Result<Absy>() != null);

@@ -2309,7 +1897,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public class MapSelect : IAppliable, AI.IFunctionSymbol {

+  public class MapSelect : IAppliable {

 

     public readonly int Arity;

     private readonly IToken/*!*/ tok;

@@ -2484,40 +2072,13 @@ namespace Microsoft.Boogie {
       return Type.InferValueType(mapType.TypeParameters, mapType.Arguments, mapType.Result, actualArgTypes);

     }

 

-    public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-

-        switch (Arity) {

-          case 1:

-            return AI.Heap.Select1;

-          case 2:

-            return AI.Heap.Select2;

-          default:

-            // Maps with Arity arguments are not fully supported yet

-            return AI.Heap.UnsupportedHeapOp;

-        }

-      }

-    }

-

-    public AI.AIType/*!*/ AIType {

-      [Rep]

-      [ResultNotNewlyAllocated]

-      get {

-        Contract.Ensures(Contract.Result<AIType>() != null);

-

-        return AI.Prop.Type;     // THAT is a type? PR: no idea whether this makes sense,

-        // but it is the type of select1

-      }

-    }

-

     public T Dispatch<T>(IAppliableVisitor<T> visitor) {

       //Contract.Requires(visitor != null);

       return visitor.Visit(this);

     }

   }

 

-  public class MapStore : IAppliable, AI.IFunctionSymbol {

+  public class MapStore : IAppliable {

 

     public readonly int Arity;

     public readonly IToken/*!*/ tok;

@@ -2631,32 +2192,6 @@ namespace Microsoft.Boogie {
       return cce.NonNull(args[0]).ShallowType;

     }

 

-    public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-

-        switch (Arity) {

-          case 1:

-            return AI.Heap.Update1;

-          case 2:

-            return AI.Heap.Update2;

-          default:

-            // Maps with Arity arguments are not fully supported yet

-            return AI.Heap.UnsupportedHeapOp;

-        }

-      }

-    }

-

-    public AI.AIType/*!*/ AIType {

-      [Rep]

-      [ResultNotNewlyAllocated]

-      get {

-        Contract.Ensures(Contract.Result<AIType>() != null);

-

-        return AI.Heap.Type;

-      }

-    }

-

     public T Dispatch<T>(IAppliableVisitor<T> visitor) {

       //Contract.Requires(visitor != null);

       return visitor.Visit(this);

@@ -2664,7 +2199,7 @@ namespace Microsoft.Boogie {
   }

 

 

-  public class IfThenElse : IAppliable, AI.IFunctionSymbol {

+  public class IfThenElse : IAppliable {

 

     public IToken/*!*/ tok;

     [ContractInvariantMethod]

@@ -2758,23 +2293,6 @@ namespace Microsoft.Boogie {
       return cce.NonNull(args[1]).ShallowType;

     }

 

-    public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-        return this;

-      }

-    }

-

-    public AI.AIType/*!*/ AIType {

-      [Rep]

-      [ResultNotNewlyAllocated]

-      get {

-        Contract.Ensures(Contract.Result<AIType>() != null);

-

-        return AI.Value.FunctionType(3);

-      }

-    }

-

     public T Dispatch<T>(IAppliableVisitor<T> visitor) {

       //Contract.Requires(visitor != null);

       return visitor.Visit(this);

@@ -2783,7 +2301,7 @@ namespace Microsoft.Boogie {
 

 

 

-  public class CodeExpr : Expr, AI.IUnknown {

+  public class CodeExpr : Expr {

     public VariableSeq/*!*/ LocVars;

     [Rep]

     public List<Block/*!*/>/*!*/ Blocks;

@@ -2802,18 +2320,6 @@ namespace Microsoft.Boogie {
       Blocks = blocks;

     }

 

-    public override AI.IExpr/*!*/ IExpr {

-      get {

-        Contract.Ensures(Contract.Result<IExpr>() != null);

-        return this;

-      }

-    }

-    [Pure]

-    public object DoVisit(AI.ExprVisitor visitor) {

-      //Contract.Requires(visitor != null);

-      return this;

-    }

-

     public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {

       //Contract.Requires(freeVars != null);

       // Treat a BlockEexpr as if it has no free variables at all

@@ -2894,7 +2400,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public class BvExtractExpr : Expr, AI.IFunApp {

+  public class BvExtractExpr : Expr {

     public /*readonly--except in StandardVisitor*/ Expr/*!*/ Bitvector;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -2987,56 +2493,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public override AI.IExpr/*!*/ IExpr {

-      get {

-        Contract.Ensures(Contract.Result<IExpr>() != null);

-

-        return this;

-      }

-    }

-    public AI.IFunctionSymbol/*!*/ FunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-

-        return AI.Bv.Extract;

-      }

-    }

-    public IList/*<AI.IExpr!>*//*!*/ Arguments {

-      get {

-        Contract.Ensures(Contract.Result<IList>() != null);

-

-        AI.IExpr[] a = new AI.IExpr[3];

-        a[0] = Bitvector.IExpr;

-        a[1] = new LiteralExpr(Token.NoToken, BigNum.FromInt(End));

-        a[2] = new LiteralExpr(Token.NoToken, BigNum.FromInt(Start));

-        return ArrayList.ReadOnly(a);

-      }

-    }

-    public AI.IFunApp CloneWithArguments(IList/*<AI.IExpr!>*/ args) {

-      //Contract.Requires(args != null);

-      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

-      AI.IFunApp retFun;

-

-      if (args.Count == 3) {

-        retFun = new BvExtractExpr(this.tok,

-                                 BoogieFactory.IExpr2Expr(cce.NonNull((AI.IExpr)args[0])),

-                                 cce.NonNull((LiteralExpr/*!*/)args[1]).asBigNum.ToIntSafe,

-                                 cce.NonNull((LiteralExpr/*!*/)args[2]).asBigNum.ToIntSafe);

-      } else {

-        {

-          Contract.Assert(false);

-          throw new cce.UnreachableException();

-        }   // If we are something wrong is happended

-      }

-      return retFun;

-    }

-

-    [Pure]

-    public object DoVisit(AI.ExprVisitor visitor) {

-      //Contract.Requires(visitor != null);

-      return visitor.VisitFunApp(this);

-    }

-

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

       Contract.Ensures(Contract.Result<Absy>() != null);

@@ -3044,7 +2500,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public class BvConcatExpr : Expr, AI.IFunApp {

+  public class BvConcatExpr : Expr {

     public /*readonly--except in StandardVisitor*/ Expr/*!*/ E0, E1;

     [ContractInvariantMethod]

     void ObjectInvariant() {

@@ -3137,53 +2593,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public override AI.IExpr/*!*/ IExpr {

-      get {

-        Contract.Ensures(Contract.Result<IExpr>() != null);

-

-        return this;

-      }

-    }

-    public AI.IFunctionSymbol/*!*/ FunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);

-        return AI.Bv.Concat;

-      }

-    }

-    public IList/*<AI.IExpr!>*//*!*/ Arguments {

-      get {

-        Contract.Ensures(Contract.Result<IList>() != null);

-

-        AI.IExpr[] a = new AI.IExpr[2];

-        a[0] = E0.IExpr;

-        a[1] = E1.IExpr;

-        return ArrayList.ReadOnly(a);

-      }

-    }

-    public AI.IFunApp CloneWithArguments(IList/*<AI.IExpr!>*/ args) {

-      //Contract.Requires(args != null);

-      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

-      AI.IFunApp/*!*/ retFun;

-

-      if (args.Count == 2) {

-        retFun = new BvConcatExpr(this.tok,

-                               BoogieFactory.IExpr2Expr(cce.NonNull((AI.IExpr/*!*/)args[0])),

-                               BoogieFactory.IExpr2Expr(cce.NonNull((AI.IExpr/*!*/)args[1])));

-      } else {

-        {

-          Contract.Assert(false);

-          throw new cce.UnreachableException();

-        }   // If we are something wrong is happended

-      }

-      return retFun;

-    }

-

-    [Pure]

-    public object DoVisit(AI.ExprVisitor visitor) {

-      //Contract.Requires(visitor != null);

-      return visitor.VisitFunApp(this);

-    }

-

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

       Contract.Ensures(Contract.Result<Absy>() != null);

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index 3f798fd2..05fdb7e4 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -13,7 +13,6 @@ namespace Microsoft.Boogie {
   using System.Diagnostics;

   using System.Collections.Generic;

   using Microsoft.Boogie.AbstractInterpretation;

-  using AI = Microsoft.AbstractInterpretationFramework;

   using System.Diagnostics.Contracts;

   using Microsoft.Basetypes;

 

@@ -38,24 +37,11 @@ namespace Microsoft.Boogie {
     public BinderExprContracts():base(null,null,null,null,null){

   }

 

-    public override Microsoft.AbstractInterpretationFramework.IFunctionSymbol FunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<AI.IFunctionSymbol>() != null);

-        throw new NotImplementedException();

-      }

-    }

-

     public override Type ShallowType {

       get {

         throw new NotImplementedException();

       }

     }

-

-    public override Microsoft.AbstractInterpretationFramework.IExpr IExpr {

-      get {

-        throw new NotImplementedException();

-      }

-    }

   }

   [ContractClass(typeof(BinderExprContracts))]

   public abstract class BinderExpr : Expr {

@@ -217,211 +203,6 @@ namespace Microsoft.Boogie {
       }

       return unmentionedParameters;

     }

-

-

-    public abstract AI.IFunctionSymbol/*!*/ FunctionSymbol {

-      get;

-    }

-

-    internal sealed class AIQuantifier : AI.IFunApp {

-      internal readonly AIFunctionRep/*!*/ arg;

-      [ContractInvariantMethod]

-      void ObjectInvariant() {

-        Contract.Invariant(arg != null);

-      }

-

-      internal AIQuantifier(BinderExpr/*!*/ realQuantifier, int dummyIndex)

-        : this(new AIFunctionRep(realQuantifier, dummyIndex)) {

-        Contract.Requires(realQuantifier != null);

-      }

-      [Pure]

-      [Reads(ReadsAttribute.Reads.Nothing)]

-      public override bool Equals(object obj) {

-        if (obj == null)

-          return false;

-        if (!(obj is AIQuantifier))

-          return false;

-

-        AIQuantifier other = (AIQuantifier)obj;

-        return object.Equals(this.arg, other.arg);

-      }

-      [Pure]

-      public override int GetHashCode() {

-        return this.arg.GetHashCode();

-      }

-

-      private AIQuantifier(AIFunctionRep arg) {

-        Contract.Requires(arg != null);

-        this.arg = arg;

-        // base();

-      }

-

-      [Pure]

-      public object DoVisit(AI.ExprVisitor visitor) {

-        //Contract.Requires(visitor != null);

-        return visitor.VisitFunApp(this);

-      }

-

-      public AI.IFunctionSymbol/*!*/ FunctionSymbol {

-        get {

-          Contract.Ensures(Contract.Result<AI.IFunctionSymbol>() != null);

-          return arg.RealQuantifier.FunctionSymbol;

-        }

-      }

-

-      private IList/*?*/ argCache = null;

-      public IList/*<IExpr!>*//*!*/ Arguments {

-

-        get {

-          Contract.Ensures(Contract.Result<IList>() != null);

-

-          if (argCache == null) {

-            IList a = new ArrayList(1);

-            a.Add(arg);

-            argCache = ArrayList.ReadOnly(a);

-          }

-          return argCache;

-        }

-      }

-

-      public AI.IFunApp CloneWithArguments(IList/*<IExpr!>*/ args) {

-        //Contract.Requires(args != null);

-        Contract.Ensures(Contract.Result<AI.IFunApp>() != null);

-        Contract.Assume(args.Count == 1);

-

-        AIFunctionRep rep = args[0] as AIFunctionRep;

-        if (rep != null)

-          return new AIQuantifier(rep);

-        else

-          throw new System.NotImplementedException();

-      }

-

-      [Pure]

-      public override string ToString() {

-        Contract.Ensures(Contract.Result<string>() != null);

-        return string.Format("{0}({1})", FunctionSymbol, arg);

-      }

-    }

-

-    internal sealed class AIFunctionRep : AI.IFunction {

-      internal readonly BinderExpr/*!*/ RealQuantifier;

-      [ContractInvariantMethod]

-      void ObjectInvariant() {

-        Contract.Invariant(RealQuantifier != null);

-      }

-

-      private readonly int dummyIndex;

-

-      internal AIFunctionRep(BinderExpr realQuantifier, int dummyIndex) {

-        Contract.Requires(realQuantifier != null);

-        this.RealQuantifier = realQuantifier;

-        this.dummyIndex = dummyIndex;

-        Contract.Assert(realQuantifier.TypeParameters.Length == 0); // PR: don't know how to handle this yet

-        // base();

-      }

-      [Pure]

-      [Reads(ReadsAttribute.Reads.Nothing)]

-      public override bool Equals(object obj) {

-        if (obj == null)

-          return false;

-        if (!(obj is AIFunctionRep))

-          return false;

-

-        AIFunctionRep other = (AIFunctionRep)obj;

-        return object.Equals(this.RealQuantifier, other.RealQuantifier) && this.dummyIndex == other.dummyIndex;

-      }

-      [Pure]

-      public override int GetHashCode() {

-        return this.RealQuantifier.GetHashCode() ^ dummyIndex;

-      }

-

-      [Pure]

-      public object DoVisit(AI.ExprVisitor visitor) {

-        //Contract.Requires(visitor != null);

-        return visitor.VisitFunction(this);

-      }

-

-      public AI.IVariable/*!*/ Param {

-

-        get {

-          Contract.Ensures(Contract.Result<AI.IVariable>() != null);

-          return cce.NonNull(RealQuantifier.Dummies[dummyIndex]);

-        }

-      }

-      public AI.AIType/*!*/ ParamType {

-        get {

-          Contract.Ensures(Contract.Result<AI.AIType>() != null);

-          throw new System.NotImplementedException();

-        }

-      }

-

-      // We lazily convert to 1 dummy per quantifier representation for AIFramework

-      private AI.IExpr/*?*/ bodyCache = null;

-      public AI.IExpr/*!*/ Body {

-        get {

-          Contract.Ensures(Contract.Result<AI.IExpr>() != null);

-

-          if (bodyCache == null) {

-            int dummyi = dummyIndex;

-            int dummylen = RealQuantifier.Dummies.Length;

-            Contract.Assume(dummylen > dummyi);

-

-            // return the actual body if there are no more dummies

-            if (dummyi + 1 == dummylen)

-              bodyCache = RealQuantifier.Body.IExpr;

-            else {

-              AIQuantifier innerquant = new AIQuantifier(RealQuantifier, dummyi + 1);

-              bodyCache = innerquant;

-            }

-          }

-          return bodyCache;

-        }

-      }

-      public AI.IFunction CloneWithBody(AI.IExpr body) {

-        //Contract.Requires(body != null);

-        Contract.Ensures(Contract.Result<AI.IFunction>() != null);

-        BinderExpr realquant;

-

-        AIQuantifier innerquant = body as AIQuantifier;

-        if (innerquant == null) {

-          // new quantifier body, clone the real quantifier

-          realquant = (BinderExpr)RealQuantifier.Clone();

-          realquant.Body = BoogieFactory.IExpr2Expr(body);

-        } else {

-          if (innerquant.arg.dummyIndex > 0) {

-            realquant = innerquant.arg.RealQuantifier;

-          } else {

-            realquant = (BinderExpr)RealQuantifier.Clone();

-            VariableSeq/*!*/ newdummies = new VariableSeq();

-            newdummies.Add(Param);

-            newdummies.AddRange(innerquant.arg.RealQuantifier.Dummies);

-            realquant.Dummies = newdummies;

-            realquant.Body = innerquant.arg.RealQuantifier.Body;

-          }

-        }

-

-        return new AIFunctionRep(realquant, dummyIndex);

-      }

-      [Pure]

-      public override string ToString() {

-        Contract.Ensures(Contract.Result<string>() != null);

-        return string.Format("\\{0} :: {1}", Param, Body);

-      }

-    }

-

-    private AI.IExpr aiexprCache = null;

-    public override AI.IExpr/*!*/ IExpr {

-      get {

-        Contract.Ensures(Contract.Result<AI.IExpr>() != null);

-

-        if (TypeParameters.Length > 0)

-          return new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "anon", Type.Bool));

-        if (aiexprCache == null) {

-          aiexprCache = new AIQuantifier(this, 0);

-        }

-        return aiexprCache;

-      }

-    }

   }

 

   public class QKeyValue : Absy {

@@ -678,13 +459,6 @@ namespace Microsoft.Boogie {
       Contract.Requires(dummies.Length + typeParams.Length > 0);

       //:base(tok, typeParams, dummies, null, null, body); // here for aesthetic reasons

     }

-    public override AI.IFunctionSymbol/*!*/ FunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<AI.IFunctionSymbol>() != null);

-

-        return AI.Prop.Forall;

-      }

-    }

 

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

@@ -726,13 +500,6 @@ namespace Microsoft.Boogie {
       Contract.Requires(dummies.Length > 0);

       //:base(tok, new TypeVariableSeq(), dummies, null, null, body); // here for aesthetic reasons

     }

-    public override AI.IFunctionSymbol/*!*/ FunctionSymbol {

-      get {

-        Contract.Ensures(Contract.Result<AI.IFunctionSymbol>() != null);

-

-        return AI.Prop.Exists;

-      }

-    }

 

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

@@ -1006,15 +773,6 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public override AI.IFunctionSymbol/*!*/ FunctionSymbol {

-

-      get {

-        Contract.Ensures(Contract.Result<AI.IFunctionSymbol>() != null);

-

-        return AI.Prop.Lambda;

-      }

-    }

-

     public override Absy StdDispatch(StandardVisitor visitor) {

       //Contract.Requires(visitor != null);

       Contract.Ensures(Contract.Result<Absy>() != null);

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index a22ece7d..706d6298 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -13,7 +13,6 @@ namespace Microsoft.Boogie {
   using System.Diagnostics;

   using System.Collections.Generic;

   using Microsoft.Boogie.AbstractInterpretation;

-  using AI = Microsoft.AbstractInterpretationFramework;

   using System.Diagnostics.Contracts;

 

   //=====================================================================

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 9c721703..a2ad40f6 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -12,7 +12,6 @@ using System.Text;
 using Microsoft.Boogie;

 using Microsoft.Basetypes;

 using Bpl = Microsoft.Boogie;

-using AI = Microsoft.AbstractInterpretationFramework;

 

 

 COMPILER BoogiePL

@@ -115,7 +114,6 @@ private class BvBounds : Expr {
     {Contract.Assert(false);throw new cce.UnreachableException();}

   }

   public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }

-  public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } }

 }

 

 /*--------------------------------------------------------------------------*/

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 73fa8946..55f15454 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -609,26 +609,9 @@ namespace Microsoft.Boogie {
     }

 

     public class AiFlags {

-      public bool Intervals = false;

-      public bool Constant = false;

-      public bool DynamicType = false;

-      public bool Nullness = false;

-      public bool Polyhedra = false;

       public bool J_Trivial = false;

       public bool J_Intervals = false;

       public bool DebugStatistics = false;

-

-      public bool AnySet {

-        get {

-          return Intervals

-              || Constant

-              || DynamicType

-              || Nullness

-              || Polyhedra

-              || J_Trivial

-              || J_Intervals;

-        }

-      }

     }

     public AiFlags/*!*/ Ai = new AiFlags();

 

@@ -639,26 +622,6 @@ namespace Microsoft.Boogie {
           if (ps.ConfirmArgumentCount(1)) {

             foreach (char c in cce.NonNull(args[ps.i])) {

               switch (c) {

-                case 'i':

-                  Ai.Intervals = true;

-                  UseAbstractInterpretation = true;

-                  break;

-                case 'c':

-                  Ai.Constant = true;

-                  UseAbstractInterpretation = true;

-                  break;

-                case 'd':

-                  Ai.DynamicType = true;

-                  UseAbstractInterpretation = true;

-                  break;

-                case 'n':

-                  Ai.Nullness = true;

-                  UseAbstractInterpretation = true;

-                  break;

-                case 'p':

-                  Ai.Polyhedra = true;

-                  UseAbstractInterpretation = true;

-                  break;

                 case 't':

                   Ai.J_Trivial = true;

                   UseAbstractInterpretation = true;

@@ -697,12 +660,6 @@ namespace Microsoft.Boogie {
           }

           return true;

 

-        case "logInfer":

-          if (ps.ConfirmArgumentCount(0)) {

-            Microsoft.AbstractInterpretationFramework.Lattice.LogSwitch = true;

-          }

-          return true;

-

         case "break":

         case "launch":

           if (ps.ConfirmArgumentCount(0)) {

@@ -1502,7 +1459,6 @@ namespace Microsoft.Boogie {
                 perform interprocedural inference (deprecated, not supported)

   /contractInfer

                 perform procedure contract inference

-  /logInfer     print debug output during inference

   /instrumentInfer

                 h - instrument inferred invariants only at beginning of

                     loop headers (default)

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index 9a24b6b2..3a2f421a 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -172,10 +172,6 @@
     <Compile Include="Xml.cs" />

   </ItemGroup>

   <ItemGroup>

-    <ProjectReference Include="..\AIFramework\AIFramework.csproj">

-      <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>

-      <Name>AIFramework</Name>

-    </ProjectReference>

     <ProjectReference Include="..\Basetypes\Basetypes.csproj">

       <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 69f505bc..e95bccda 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -6,7 +6,6 @@ using System.Text;
 using Microsoft.Boogie;

 using Microsoft.Basetypes;

 using Bpl = Microsoft.Boogie;

-using AI = Microsoft.AbstractInterpretationFramework;

 

 

 

@@ -134,7 +133,6 @@ private class BvBounds : Expr {
     {Contract.Assert(false);throw new cce.UnreachableException();}

   }

   public override void ComputeFreeVariables(GSet<object>/*!*/ freeVars) {Contract.Requires(freeVars != null); {Contract.Assert(false);throw new cce.UnreachableException();} }

-  public override AI.IExpr/*!*/ IExpr { get { Contract.Ensures(Contract.Result<AI.IExpr>()!=null); {Contract.Assert(false);throw new cce.UnreachableException();} } }

 }

 

 /*--------------------------------------------------------------------------*/

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 9bbeada1..66eee658 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -63,11 +63,6 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Absy>() != null);

       return node.StdDispatch(this);

     }

-    public virtual AIVariableExpr VisitAIVariableExpr(AIVariableExpr node) {

-      Contract.Requires(node != null);

-      Contract.Ensures(Contract.Result<AIVariableExpr>() != null);

-      return node;

-    }

     public virtual Cmd VisitAssertCmd(AssertCmd node) {

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<Cmd>() != null);