Boogie: Committing new source code for VCExpr

1 files changed, 336 insertions, 165 deletions

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index 30779f22..b8a53b9f 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -8,7 +8,7 @@ using System.Text;
 using System.IO;

 using System.Collections;

 using System.Collections.Generic;

-using Microsoft.Contracts;

+using System.Diagnostics.Contracts;

 using Microsoft.Basetypes;

 using Microsoft.Boogie.VCExprAST;

 

@@ -16,13 +16,25 @@ using Microsoft.Boogie.VCExprAST;
 

 namespace Microsoft.Boogie.VCExprAST

 {

+  [ContractClassFor(typeof(LineariserOptions))]

+  public abstract class LinOptContracts:LineariserOptions{

+    public LinOptContracts() : base(true) {

+    }

+    public override LineariserOptions  SetAsTerm(bool newVal)

+{

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

+  throw new NotImplementedException();

+}

+    

+  }

 

   // Options for the linearisation. Here one can choose, for instance,

   // whether Simplify or Z3 output is to be produced

+  [ContractClass(typeof(LinOptContracts))]

   public abstract class LineariserOptions {

 

     public readonly bool AsTerm;

-    public abstract LineariserOptions! SetAsTerm(bool newVal);

+    public abstract LineariserOptions/*!*/ SetAsTerm(bool newVal);

 

     public abstract bool QuantifierIds { get; }

 

@@ -39,19 +51,29 @@ namespace Microsoft.Boogie.VCExprAST
 

     // variables representing formulas in let-bindings have to be

     // printed in a different way than other variables

-    public virtual List<VCExprVar!>! LetVariables { get {

+    public virtual List<VCExprVar/*!*/>/*!*/ LetVariables { get {Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));

       return EmptyList;

     } }

 

-    public virtual LineariserOptions! AddLetVariable(VCExprVar! furtherVar) {

+    public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar){

+Contract.Requires(furtherVar != null);

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

       return this;

     }

 

-	public virtual LineariserOptions! AddLetVariables(List<VCExprVar!>! furtherVars) {

+	public virtual LineariserOptions AddLetVariables(List<VCExprVar/*!*/>/*!*/ furtherVars){

+Contract.Requires(cce.NonNullElements(furtherVars));

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

       return this;

     }

     

-    private static readonly List<VCExprVar!>! EmptyList = new List<VCExprVar!>();

+    private static readonly List<VCExprVar/*!*/>/*!*/ EmptyList = new List<VCExprVar/*!*/>();

+    [ContractInvariantMethod]

+void ObjectInvarinat() 

+{

+    Contract.Invariant(EmptyList!=null);

+}

+

 

     public bool NativeBv { get {

       return Bitvectors == CommandLineOptions.BvHandling.Z3Native;

@@ -67,14 +89,14 @@ namespace Microsoft.Boogie.VCExprAST
       this.AsTerm = asTerm;

     }

 

-    public static readonly LineariserOptions! SimplifyDefault = new SimplifyOptions (false);

-    internal static readonly LineariserOptions! SimplifyDefaultTerm = new SimplifyOptions (true);

+    public static readonly LineariserOptions SimplifyDefault = new SimplifyOptions (false);

+    internal static readonly LineariserOptions SimplifyDefaultTerm = new SimplifyOptions (true);

 

     ////////////////////////////////////////////////////////////////////////////////////////

 

     private class SimplifyOptions : LineariserOptions {

-      internal SimplifyOptions(bool asTerm) {

-        base(asTerm);

+      internal SimplifyOptions(bool asTerm):base(asTerm) {

+        

       }

       public override bool QuantifierIds { get {

         return false;

@@ -82,7 +104,8 @@ namespace Microsoft.Boogie.VCExprAST
       public override bool UseTypes { get {

         return false;

       } }

-      public override LineariserOptions! SetAsTerm(bool newVal) {

+      public override LineariserOptions SetAsTerm(bool newVal) {

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

         if (newVal)

           return SimplifyDefaultTerm;

         else

@@ -94,14 +117,21 @@ namespace Microsoft.Boogie.VCExprAST
   ////////////////////////////////////////////////////////////////////////////////////////

 

   // Lineariser for expressions. The result (bool) is currently not used for anything

-  public class SimplifyLikeExprLineariser : IVCExprVisitor<bool, LineariserOptions!> {

+  public class SimplifyLikeExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> {

 

-    public static string! ToSimplifyString(VCExpr! e, UniqueNamer! namer) {

+    public static string ToSimplifyString(VCExpr e, UniqueNamer namer){

+Contract.Requires(namer != null);

+Contract.Requires(e != null);

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

       return ToString(e, LineariserOptions.SimplifyDefault, namer);

     }

 

-    public static string! ToString(VCExpr! e, LineariserOptions! options,

-                                   UniqueNamer! namer) {

+    public static string ToString(VCExpr/*!*/ e, LineariserOptions/*!*/ options,UniqueNamer/*!*/ namer) {

+      Contract.Requires(e != null);

+      Contract.Requires(options != null);

+      Contract.Requires(namer != null);

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

+

       StringWriter sw = new StringWriter();

       SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser (sw, namer);

       lin.Linearise(e, options);

@@ -110,32 +140,47 @@ namespace Microsoft.Boogie.VCExprAST
 

     ////////////////////////////////////////////////////////////////////////////////////////

 

-    private readonly TextWriter! wr;

+    [ContractInvariantMethod]

+void ObjectInvariant() 

+{

+    Contract.Invariant(wr!=null);

+      Contract.Invariant(Namer != null);

+}

+

+    private readonly TextWriter/*!*/ wr;

     private SimplifyLikeOpLineariser OpLinObject = null;

-    private IVCExprOpVisitor<bool, LineariserOptions!>! OpLineariser { get {

+    private IVCExprOpVisitor<bool, LineariserOptions/*!*/>/*!*/ OpLineariser { get {Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>()!=null);

       if (OpLinObject == null)

         OpLinObject = new SimplifyLikeOpLineariser (this, wr);

       return OpLinObject;

     } }

 

-    internal readonly UniqueNamer! Namer;

+    internal readonly UniqueNamer Namer;

 

-    public SimplifyLikeExprLineariser(TextWriter! wr, UniqueNamer! namer) {

+    public SimplifyLikeExprLineariser(TextWriter wr, UniqueNamer namer){

+Contract.Requires(namer != null);

+Contract.Requires(wr != null);

       this.wr = wr;

       this.Namer = namer;

     }

 

-    public void Linearise(VCExpr! expr, LineariserOptions! options) {

-      expr.Accept<bool, LineariserOptions!>(this, options);

+    public void Linearise(VCExpr expr, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(expr != null);

+      expr.Accept<bool, LineariserOptions>(this, options);

     }

 

-    public void LineariseAsTerm(VCExpr! expr, LineariserOptions! options) {

+    public void LineariseAsTerm(VCExpr expr, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(expr != null);

       Linearise(expr, options.SetAsTerm(true));

     }

 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public static string! MakeIdPrintable(string! s) {

+    public static string MakeIdPrintable(string s){

+Contract.Requires(s != null);

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

       // make sure that no keywords are used as identifiers

       switch(s) {

       case andName:

@@ -197,14 +242,18 @@ namespace Microsoft.Boogie.VCExprAST
       }

     }

 

-    private static string! TypeToStringHelper(Type! t) {

+    private static string TypeToStringHelper(Type t){

+Contract.Requires(t != null);

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

       System.IO.StringWriter buffer = new System.IO.StringWriter();

       using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

         t.Emit(stream);

       }

       return buffer.ToString();

     }

-    public static string! TypeToString(Type! t) {

+    public static string TypeToString(Type t){

+Contract.Requires(t != null);

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

       if (t.IsBool)

         return "$bool";

       else if (t.IsInt)

@@ -222,30 +271,39 @@ namespace Microsoft.Boogie.VCExprAST
       }

     }

 

-    public static string! BvConcatOpName(VCExprNAry! node)

-      requires node.Op is VCExprBvConcatOp; {

+    public static string BvConcatOpName(VCExprNAry node){

+Contract.Requires(node != null);

+Contract.Requires((node.Op is VCExprBvConcatOp));

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

       int bits1 = node[0].Type.BvBits;

       int bits2 = node[1].Type.BvBits;

       return "$bv" + (bits1 + bits2) + "_concat[" + bits1 + "." + bits2 + "]";

     }

 

-    public static string! BvExtractOpName(VCExprNAry! node)

-      requires node.Op is VCExprBvExtractOp; {

-      VCExprBvExtractOp! op = (VCExprBvExtractOp)node.Op;

+    public static string BvExtractOpName(VCExprNAry node){

+Contract.Requires(node != null);

+Contract.Requires(node.Op is VCExprBvExtractOp);

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

+      VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;

       return "$bv" + node.Type.BvBits + "_extract" + op.Total + "[" + op.Start + ":" + op.End + "]";

     }

 

-    public static string! StoreOpName(VCExprNAry! node)

-      requires node.Op is VCExprStoreOp; {

+    public static string StoreOpName(VCExprNAry node){

+Contract.Requires(node != null);

+Contract.Requires((node.Op is VCExprStoreOp));

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

       return "Store_" + TypeToString(node[0].Type);

     }

 

-    public static string! SelectOpName(VCExprNAry! node)

-      requires node.Op is VCExprSelectOp; {

+    public static string SelectOpName(VCExprNAry node){

+Contract.Requires(node != null);

+Contract.Requires((node.Op is VCExprSelectOp));

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

       return "Select_" + TypeToString(node[0].Type);

     }

     

-    internal void WriteId(string! s) {

+    internal void WriteId(string s){

+Contract.Requires(s != null);

       wr.Write(MakeIdPrintable(s));

     }

 

@@ -254,57 +312,63 @@ namespace Microsoft.Boogie.VCExprAST
     /// <summary>

     /// The name for logical conjunction in Simplify

     /// </summary>

-    internal const string! andName = "AND"; // conjunction

-    internal const string! orName = "OR"; // disjunction

-    internal const string! notName = "NOT"; // negation

-    internal const string! impliesName = "IMPLIES"; // implication

-    internal const string! iffName = "IFF"; // logical equivalence

-    internal const string! eqName = "EQ"; // equality

-    internal const string! neqName = "NEQ"; // inequality

-    internal const string! lessName = "<";

-    internal const string! greaterName = ">";

-    internal const string! atmostName = "<=";

-    internal const string! atleastName = ">=";

-    internal const string! TRUEName = "TRUE"; // nullary predicate that is always true

-    internal const string! FALSEName = "FALSE"; // nullary predicate that is always false

-    internal const string! subtypeName = "<:";

-    internal const string! subtypeArgsName = "<::";

-

-    internal const string! distinctName = "DISTINCT";

+    internal const string andName = "AND"; // conjunction

+    internal const string orName = "OR"; // disjunction

+    internal const string notName = "NOT"; // negation

+    internal const string impliesName = "IMPLIES"; // implication

+    internal const string iffName = "IFF"; // logical equivalence

+    internal const string eqName = "EQ"; // equality

+    internal const string neqName = "NEQ"; // inequality

+    internal const string lessName = "<";

+    internal const string greaterName = ">"; 

+    internal const string atmostName = "<=";

+    internal const string atleastName = ">=";

+    internal const string TRUEName = "TRUE"; // nullary predicate that is always true

+    internal const string FALSEName = "FALSE"; // nullary predicate that is always false

+    internal const string subtypeName = "<:";

+    internal const string subtypeArgsName = "<::";

+

+    internal const string distinctName = "DISTINCT";

     /// <summary>

     /// name of the main inclusion relation

     /// </summary>

-    internal const string! boolTrueName = "|@true|";

-    internal const string! boolFalseName = "|@false|";

-    internal const string! boolAndName = "boolAnd";

-    internal const string! boolOrName = "boolOr";

-    internal const string! boolNotName = "boolNot";

-    internal const string! termEqName = "anyEqual";

-    internal const string! termNeqName = "anyNeq";

-    internal const string! termLessName = "intLess";

-    internal const string! termGreaterName = "intGreater";

-    internal const string! termAtmostName = "intAtMost";

-    internal const string! termAtleastName = "intAtLeast";

-    internal const string! intAddName = "+";

-    internal const string! intAddNameReflect = "Reflect$Add";

-    internal const string! intSubName = "-";

-    internal const string! intMulName = "*";

-    internal const string! intDivName = "/";

-    internal const string! intModName = "%";

-

-    internal void AssertAsTerm(string! x, LineariserOptions! options) {

+    internal const string boolTrueName = "|@true|";

+    internal const string boolFalseName = "|@false|";

+    internal const string boolAndName = "boolAnd";

+    internal const string boolOrName = "boolOr";

+    internal const string boolNotName = "boolNot";

+    internal const string termEqName = "anyEqual";

+    internal const string termNeqName = "anyNeq";

+    internal const string termLessName = "intLess";

+    internal const string termGreaterName = "intGreater";

+    internal const string termAtmostName = "intAtMost";

+    internal const string termAtleastName = "intAtLeast";

+    internal const string intAddName = "+";

+    internal const string intAddNameReflect = "Reflect$Add";

+    internal const string intSubName = "-";

+    internal const string intMulName = "*";

+    internal const string intDivName = "/";

+    internal const string intModName = "%";

+

+    internal void AssertAsTerm(string x, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(x != null);

       if (!options.AsTerm)

         System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!");

     }

 

-    internal void AssertAsFormula(string! x, LineariserOptions! options) {

+    internal void AssertAsFormula(string x, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(x != null);

       if (options.AsTerm)

         System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!");

     }

 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public bool Visit(VCExprLiteral! node, LineariserOptions! options) {

+    public bool Visit(VCExprLiteral node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

       if (options.AsTerm) {

 

         if (node == VCExpressionGenerator.True)

@@ -313,8 +377,10 @@ namespace Microsoft.Boogie.VCExprAST
           wr.Write(options.UseTypes ? FALSEName : boolFalseName);

         else if (node is VCExprIntLit) {

           wr.Write(((VCExprIntLit)node).Val);

-        } else

-          assert false;

+        } else {

+          Contract.Assert(false);

+          throw new cce.UnreachableException();

+        }

 

       } else {

 

@@ -324,8 +390,10 @@ namespace Microsoft.Boogie.VCExprAST
           wr.Write(FALSEName);

         else if (node is VCExprIntLit) {

           System.Diagnostics.Debug.Fail("One should never write IntLit as a predicate!");

-        } else

-          assert false;

+        } else {

+          Contract.Assert(false);

+          throw new cce.UnreachableException();

+        }

 

       }

 

@@ -334,8 +402,11 @@ namespace Microsoft.Boogie.VCExprAST
 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public bool Visit(VCExprNAry! node, LineariserOptions! options) {

-      VCExprOp! op = node.Op;

+    public bool Visit(VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

+      VCExprOp op = node.Op;

+      Contract.Assert(op != null);

 

       if (!options.AsTerm &&

           (op.Equals(VCExpressionGenerator.AndOp) ||

@@ -344,12 +415,13 @@ namespace Microsoft.Boogie.VCExprAST
 

         wr.Write("({0}",

                  op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);

-        IEnumerator! enumerator = new VCExprNAryUniformOpEnumerator (node);

+        IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node);

+        Contract.Assert(enumerator != null);

         while (enumerator.MoveNext()) {

           VCExprNAry naryExpr = enumerator.Current as VCExprNAry;

-          if (naryExpr == null || !naryExpr.Op.Equals(op)) {

+          if (naryExpr == null ||  !naryExpr.Op.Equals(op)) {

             wr.Write(" ");

-            Linearise((VCExpr!)enumerator.Current, options);

+            Linearise(cce.NonNull((VCExpr)enumerator.Current), options);

           }

         }

 

@@ -358,13 +430,16 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

-      return node.Accept<bool, LineariserOptions!>(OpLineariser, options);

+      return node.Accept<bool, LineariserOptions>(OpLineariser, options);

     }

 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public bool Visit(VCExprVar! node, LineariserOptions! options) {

-      string! printedName = Namer.GetName(node, node.Name);

+    public bool Visit(VCExprVar node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

+      string printedName = Namer.GetName(node, node.Name);

+      Contract.Assert(printedName != null);

 

       if (options.AsTerm ||

           // variables for formulas bound in a let-binding are never

@@ -377,7 +452,7 @@ namespace Microsoft.Boogie.VCExprAST
       } else {

         wr.Write("({0} ", eqName);

         WriteId(printedName);

-        wr.Write(" {0})", boolTrueName);

+        wr.Write(" {0})", boolTrueName);        

       }

 

       return true;

@@ -385,19 +460,23 @@ namespace Microsoft.Boogie.VCExprAST
 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public bool Visit(VCExprQuantifier! node, LineariserOptions! options) {

+    public bool Visit(VCExprQuantifier node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

       AssertAsFormula(node.Quan.ToString(), options);

-      assert node.TypeParameters.Count == 0;

+      Contract.Assert(node.TypeParameters.Count == 0);

 

       Namer.PushScope(); try {

 

-      string! kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS";

+      string kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS";

       wr.Write("({0} (", kind);

 

       for (int i = 0; i < node.BoundVars.Count; i++) 

         {

-          VCExprVar! var = node.BoundVars[i];

-          string! printedName = Namer.GetLocalName(var, var.Name);

+          VCExprVar var = node.BoundVars[i];

+        Contract.Assert(var != null);

+          string printedName = Namer.GetLocalName(var, var.Name);

+        Contract.Assert(printedName != null);

           if (i != 0)

             wr.Write(" ");

           WriteId(printedName);

@@ -410,7 +489,8 @@ namespace Microsoft.Boogie.VCExprAST
         

       if (options.QuantifierIds) {

         // only needed for Z3

-        VCQuantifierInfos! infos = node.Infos;

+        VCQuantifierInfos infos = node.Infos;

+        Contract.Assert(infos != null);

         if (infos.qid != null) {

           wr.Write("(QID ");

           wr.Write(infos.qid);

@@ -442,11 +522,14 @@ namespace Microsoft.Boogie.VCExprAST
       }

     }

 

-    private void WriteTriggers(List<VCTrigger!>! triggers, LineariserOptions! options) {

+    private void WriteTriggers(List<VCTrigger/*!*/>/*!*/ triggers, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(cce.NonNullElements(triggers));

       // first, count how many neg/pos triggers there are

       int negTriggers = 0;

       int posTriggers = 0;

-      foreach (VCTrigger! vcTrig in triggers) {

+      foreach (VCTrigger vcTrig in triggers) {

+        Contract.Assert(vcTrig != null);

         if (vcTrig.Pos) {

           posTriggers++;

         } else {

@@ -456,12 +539,13 @@ namespace Microsoft.Boogie.VCExprAST
 

       if (posTriggers > 0) {

         wr.Write("(PATS");

-        foreach (VCTrigger! vcTrig in triggers) {

+        foreach (VCTrigger vcTrig in triggers) {

+          Contract.Assert(vcTrig != null);

           if (vcTrig.Pos) {

             if (vcTrig.Exprs.Count > 1) {

               wr.Write(" (MPAT");

             }

-            foreach (VCExpr! e in vcTrig.Exprs) {

+            foreach (VCExpr e in vcTrig.Exprs) {Contract.Assert(e != null);

               wr.Write(" ");

               LineariseAsTerm(e, options);

             }

@@ -476,10 +560,11 @@ namespace Microsoft.Boogie.VCExprAST
         // will ignore the negative patterns and output a warning. Therefore

         // we never specify both negative and positive triggers

         wr.Write("(NOPATS");

-        foreach (VCTrigger! vcTrig in triggers) {

+        foreach (VCTrigger vcTrig in triggers) {

+          Contract.Assert(vcTrig != null);

           if (!vcTrig.Pos) {

             wr.Write(" ");

-            assert vcTrig.Exprs.Count == 1;

+            Contract.Assert(vcTrig.Exprs.Count == 1);

             LineariseAsTerm(vcTrig.Exprs[0], options);

           }

         }

@@ -490,17 +575,20 @@ namespace Microsoft.Boogie.VCExprAST
 

     /////////////////////////////////////////////////////////////////////////////////////

 

-    public bool Visit(VCExprLet! node, LineariserOptions! options) {

+    public bool Visit(VCExprLet node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

       Namer.PushScope(); try {

 

       wr.Write("(LET (");

 

-      LineariserOptions! optionsWithVars = options.AddLetVariables(node.BoundVars);

+      LineariserOptions optionsWithVars = options.AddLetVariables(node.BoundVars);

+        Contract.Assert(optionsWithVars != null);

 	  

       string s = "(";

-      foreach (VCExprLetBinding! b in node) {

+      foreach (VCExprLetBinding b in node) {Contract.Assert(b != null);

         wr.Write(s);

-        string! printedName = Namer.GetLocalName(b.V, b.V.Name);

+        string printedName = Namer.GetLocalName(b.V, b.V.Name);

 

         bool formula = b.V.Type.IsBool;

         if (formula)

@@ -527,47 +615,66 @@ namespace Microsoft.Boogie.VCExprAST
     /////////////////////////////////////////////////////////////////////////////////////

 

     // Lineariser for operator terms. The result (bool) is currently not used for anything

-    internal class SimplifyLikeOpLineariser : IVCExprOpVisitor<bool, LineariserOptions!> {

-      private readonly SimplifyLikeExprLineariser! ExprLineariser;

-      private readonly TextWriter! wr;

+    internal class SimplifyLikeOpLineariser : IVCExprOpVisitor<bool, LineariserOptions/*!*/> {

+      [ContractInvariantMethod]

+      void ObjectInvariant() {

+        Contract.Invariant(ExprLineariser != null);

+        Contract.Invariant(wr != null);

+      }

 

-      public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser! ExprLineariser, TextWriter! wr) {

+      private readonly SimplifyLikeExprLineariser/*!*/ ExprLineariser;

+      private readonly TextWriter/*!*/ wr;

+

+      public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser ExprLineariser, TextWriter wr){

+Contract.Requires(wr != null);

+Contract.Requires(ExprLineariser != null);

         this.ExprLineariser = ExprLineariser;

         this.wr = wr;

       }

 

       ///////////////////////////////////////////////////////////////////////////////////

 

-      private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,

-                                    LineariserOptions! options,

-                                    bool argsAsTerms) {

+      private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms){

+Contract.Requires(options != null);

+Contract.Requires(op != null);

+Contract.Requires(cce.NonNullElements(args));

         WriteApplication(op, op, args, options, argsAsTerms);

       }

 

-      private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,

-                                    LineariserOptions! options) {

+      private void WriteApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args,LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(op != null);

+Contract.Requires(cce.NonNullElements(args));

         WriteApplication(op, op, args, options, options.AsTerm);

       }

 

-      private void WriteTermApplication(string! op, IEnumerable<VCExpr!>! args,

-                                        LineariserOptions! options) {

+      private void WriteTermApplication(string op, IEnumerable<VCExpr/*!*/>/*!*/ args,LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(op != null);

+Contract.Requires(cce.NonNullElements(args));

         ExprLineariser.AssertAsTerm(op, options);

         WriteApplication(op, op, args, options, options.AsTerm);

       }

 

-      private void WriteApplication(string! termOp, string! predOp,

-                                    IEnumerable<VCExpr!>! args, LineariserOptions! options) {

+      private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(predOp != null);

+Contract.Requires(termOp != null);

+Contract.Requires(cce.NonNullElements(args));

         WriteApplication(termOp, predOp, args, options, options.AsTerm);

       }

 

-      private void WriteApplication(string! termOp, string! predOp,

-                                    IEnumerable<VCExpr!>! args, LineariserOptions! options,

-                                    // change the AsTerm option for the arguments?

-                                    bool argsAsTerms) {

+      private void WriteApplication(string termOp, string predOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options, bool argsAsTerms){

+Contract.Requires(options != null);

+Contract.Requires(predOp != null);

+Contract.Requires(termOp != null);

+Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the arguments?

         wr.Write("({0}", options.AsTerm ? termOp : predOp);

 

-        LineariserOptions! newOptions = options.SetAsTerm(argsAsTerms);

-        foreach (VCExpr! e in args) {

+        LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);

+

+        foreach (VCExpr e in args) {

+          Contract.Assert(e != null);

           wr.Write(" ");

           ExprLineariser.Linearise(e, newOptions);

         }

@@ -578,8 +685,10 @@ namespace Microsoft.Boogie.VCExprAST
       // write an application that can only be a term.

       // if the expression is supposed to be printed as a formula,

       // it is turned into an equation (EQ (f args) |@true|)

-      private void WriteApplicationTermOnly(string! termOp,

-                                            IEnumerable<VCExpr!>! args, LineariserOptions! options) {

+      private void WriteApplicationTermOnly(string termOp, IEnumerable<VCExpr/*!*/>/*!*/ args, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(termOp != null);

+Contract.Requires(cce.NonNullElements(args));

         if (!options.AsTerm)

           // Write: (EQ (f args) |@true|)

           // where "args" are written as terms

@@ -593,22 +702,26 @@ namespace Microsoft.Boogie.VCExprAST
 

       ///////////////////////////////////////////////////////////////////////////////////

       

-      public bool VisitNotOp      (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitNotOp     (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteApplication(boolNotName, notName, node, options);      // arguments can be both terms and formulas

         return true;

       }

 

-      public bool VisitEqOp       (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitEqOp      (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         if (options.AsTerm) {

           // use equality on terms, also if the arguments have type bool

           WriteApplication(termEqName, node, options);

         } else {

           if (node[0].Type.IsBool) {

-            assert node[1].Type.IsBool;

+            Contract.Assert(node[1].Type.IsBool);

             // use equivalence

             WriteApplication(iffName, node, options);

           } else {

-            assert !node[1].Type.IsBool;

+            Contract.Assert(!node[1].Type.IsBool);

             // use equality and write the arguments as terms

             WriteApplication(eqName, node, options, true);

           }

@@ -617,13 +730,15 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

-      public bool VisitNeqOp      (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitNeqOp     (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         if (options.AsTerm) {

           // use equality on terms, also if the arguments have type bool

           WriteApplication(termNeqName, node, options);

         } else {

           if (node[0].Type.IsBool) {

-            assert node[1].Type.IsBool;

+            Contract.Assert(node[1].Type.IsBool);

             // use equivalence and negate the whole thing

             wr.Write("({0} ", notName);

             WriteApplication(iffName, node, options);

@@ -637,19 +752,25 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

-      public bool VisitAndOp      (VCExprNAry! node, LineariserOptions! options) {

-        assert options.AsTerm;

+      public bool VisitAndOp     (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

+        Contract.Assert(options.AsTerm);

         WriteApplication(boolAndName, andName, node, options);        // arguments can be both terms and formulas

         return true;

       }

 

-      public bool VisitOrOp       (VCExprNAry! node, LineariserOptions! options) {

-        assert options.AsTerm;

+      public bool VisitOrOp      (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

+        Contract.Assert(options.AsTerm);

         WriteApplication(boolOrName, orName, node, options);        // arguments can be both terms and formulas

         return true;

       }

 

-      public bool VisitImpliesOp  (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         if (options.AsTerm) {

           wr.Write("({0} ({1} ", boolOrName, boolNotName);

           ExprLineariser.Linearise(node[0], options);

@@ -663,19 +784,22 @@ namespace Microsoft.Boogie.VCExprAST
           ExprLineariser.Linearise(node[0], options);

           wr.Write("))");

         } else {

-          WriteApplication(impliesName, node, options);

+          WriteApplication(impliesName, node, options);          

         }

         return true;

       }

 

-      public bool VisitDistinctOp (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         ExprLineariser.AssertAsFormula(distinctName, options);

         

         if (node.Length < 2) {

           ExprLineariser.Linearise(VCExpressionGenerator.True, options);

         } else {

           wr.Write("({0}", distinctName);

-          foreach (VCExpr! e in node) {

+          foreach (VCExpr e in node) {

+            Contract.Assert(e != null);

             wr.Write(" ");

             ExprLineariser.LineariseAsTerm(e, options);

           }

@@ -685,16 +809,22 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

-      public bool VisitLabelOp    (VCExprNAry! node, LineariserOptions! options) {

-        VCExprLabelOp! op = (VCExprLabelOp)node.Op;

+      public bool VisitLabelOp   (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

+        VCExprLabelOp op = (VCExprLabelOp)node.Op;

+        Contract.Assert(op != null);

         wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));

         ExprLineariser.Linearise(node[0], options); wr.Write(")");

         return true;

       }

 

-      public bool VisitSelectOp   (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitSelectOp  (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         wr.Write("(" + SelectOpName(node));

-        foreach (VCExpr! e in node) {

+        foreach (VCExpr/*!*/ e in node) {

+          Contract.Assert(e != null);

           wr.Write(" ");

           ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));

         }

@@ -702,9 +832,12 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

-      public bool VisitStoreOp    (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitStoreOp   (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         wr.Write("(" + StoreOpName(node));

-        foreach (VCExpr! e in node) {

+        foreach (VCExpr e in node) {

+          Contract.Assert(e != null);

           wr.Write(" ");

           ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));

         }

@@ -712,22 +845,30 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

-      public bool VisitBvOp       (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitBvOp      (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteTermApplication("$make_bv" + node.Type.BvBits, node, options);

         return true;

       }

 

-      public bool VisitBvExtractOp(VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteTermApplication(BvExtractOpName(node), node, options);

         return true;

       }

 

-      public bool VisitBvConcatOp (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitBvConcatOp (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteTermApplication(BvConcatOpName(node), node, options);

         return true;

       }

 

-      public bool VisitIfThenElseOp (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         

         wr.Write("(ITE ");

         ExprLineariser.Linearise(node[0], options.SetAsTerm(false));

@@ -740,7 +881,9 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

-      public bool VisitCustomOp (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitCustomOp(VCExprNAry/*!*/ node, LineariserOptions/*!*/ options) {

+        Contract.Requires(node != null);

+        Contract.Requires(options != null);

         VCExprCustomOp op = (VCExprCustomOp)node.Op;

         wr.Write("({0}", op.Name);

         foreach (VCExpr arg in node) {

@@ -751,7 +894,9 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

-      public bool VisitAddOp            (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitAddOp           (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         if (CommandLineOptions.Clo.ReflectAdd) {

           WriteTermApplication(intAddNameReflect, node, options);

         } else {

@@ -760,61 +905,86 @@ namespace Microsoft.Boogie.VCExprAST
         return true;

       }

 

-      public bool VisitSubOp            (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitSubOp           (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteTermApplication(intSubName, node, options);

         return true;

       }

 

-      public bool VisitMulOp            (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitMulOp           (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteTermApplication(intMulName, node, options);

         return true;

       }

 

-      public bool VisitDivOp            (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitDivOp           (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteTermApplication(intDivName, node, options);

         return true;

       }

 

-      public bool VisitModOp            (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitModOp           (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteTermApplication(intModName, node, options);

         return true;

       }

 

-      public bool VisitLtOp             (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitLtOp            (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteApplication(termLessName, lessName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitLeOp             (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitLeOp            (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteApplication(termAtmostName, atmostName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitGtOp             (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitGtOp            (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteApplication(termGreaterName, greaterName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitGeOp             (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitGeOp            (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteApplication(termAtleastName, atleastName, node, options, true);  // arguments are always terms

         return true;

       }

 

-      public bool VisitSubtypeOp        (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitSubtypeOp       (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteApplication(subtypeName, node, options, true);               // arguments are always terms

         return true;

       }

 

-      public bool VisitSubtype3Op        (VCExprNAry! node, LineariserOptions! options) {

+      public bool VisitSubtype3Op       (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

         WriteApplication(subtypeArgsName, node, options, true);               // arguments are always terms

         return true;

       }

 

-      public bool VisitBoogieFunctionOp (VCExprNAry! node, LineariserOptions! options) {

-        VCExprBoogieFunctionOp! op = (VCExprBoogieFunctionOp)node.Op;

-        string! funcName = op.Func.Name;

-        string? bvzName = op.Func.FindStringAttribute("external");

-        string! printedName = ExprLineariser.Namer.GetName(op.Func, funcName);

+      public bool VisitBoogieFunctionOp (VCExprNAry node, LineariserOptions options){

+Contract.Requires(options != null);

+Contract.Requires(node != null);

+        VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;

+        Contract.Assert(op != null);

+        string funcName = op.Func.Name;

+        Contract.Assert(funcName != null);

+        string bvzName = op.Func.FindStringAttribute("external");

+        string printedName = ExprLineariser.Namer.GetName(op.Func, funcName);

+        Contract.Assert(printedName != null);

         if (bvzName != null) printedName = bvzName;

 

         if (options.UseTypes) {

@@ -824,7 +994,8 @@ namespace Microsoft.Boogie.VCExprAST
           wr.Write("(");

           ExprLineariser.WriteId(printedName);

 

-          foreach (VCExpr! e in node) {

+          foreach (VCExpr e in node) {

+            Contract.Assert(e != null);

             wr.Write(" ");

             ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));

           }