more work on reducing call stack consumption

4 files changed, 68 insertions, 51 deletions

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 5cd40896..f431c3d5 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -211,57 +211,59 @@ namespace Microsoft.Boogie.SMTLib
 

     public bool Visit(VCExprNAry node, LineariserOptions options)

     {

-      VCExprOp op = node.Op;

-      Contract.Assert(op != null);

-      

-      if (op.Equals(VCExpressionGenerator.ImpliesOp))

-      {

-          // handle this operator without recursion

-          VCExprNAry iter = node;

-          List<VCExpr> conjuncts = new List<VCExpr>();

-          VCExpr next = null;

-          do

-          {

-              conjuncts.Add(iter[0]);

-              next = iter[1];

-              iter = next as VCExprNAry;

-              if (iter == null) break;

-          }

-          while (iter.Op.Equals(VCExpressionGenerator.ImpliesOp));

+        VCExprOp op = node.Op;

+        Contract.Assert(op != null);

 

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

-          if (conjuncts.Count == 1)

-          {

-              Linearise(conjuncts[0], options);

-          }

-          else {

-            wr.Write("(and");

-            foreach (var e in conjuncts)

+        var booleanOps = new HashSet<VCExprOp>();

+        booleanOps.Add(VCExpressionGenerator.NotOp);

+        booleanOps.Add(VCExpressionGenerator.ImpliesOp);

+        booleanOps.Add(VCExpressionGenerator.AndOp);

+        booleanOps.Add(VCExpressionGenerator.OrOp);

+        if (booleanOps.Contains(op))

+        {

+            Stack<VCExpr> exprs = new Stack<VCExpr>();

+            exprs.Push(node);

+            while (exprs.Count > 0)

             {

+                VCExpr expr = exprs.Pop();

+                if (expr == null)

+                {

+                    wr.Write(")");

+                    continue;

+                }

                 wr.Write(" ");

-                Linearise(e, options);

+                VCExprNAry naryExpr = expr as VCExprNAry;

+                if (naryExpr == null || !booleanOps.Contains(naryExpr.Op))

+                {

+                    Linearise(expr, options);

+                    continue;

+                }

+                else if (naryExpr.Op.Equals(VCExpressionGenerator.NotOp))

+                {

+                    wr.Write("(not");

+                }

+                else if (naryExpr.Op.Equals(VCExpressionGenerator.ImpliesOp))

+                {

+                    wr.Write("(=>");

+                }

+                else if (naryExpr.Op.Equals(VCExpressionGenerator.AndOp))

+                {

+                    wr.Write("(and");

+                }

+                else 

+                {

+                    System.Diagnostics.Debug.Assert(naryExpr.Op.Equals(VCExpressionGenerator.OrOp));

+                    wr.Write("(or");

+                }

+                exprs.Push(null);

+                for (int i = naryExpr.Arity - 1; i >= 0; i--)

+                {

+                    exprs.Push(naryExpr[i]);

+                }

             }

-            wr.Write(")");

-          }

-          wr.Write(" ");

-          Linearise(next, options);

-          wr.Write(")");

-          return true;

-      }

-

-      if (op.Equals(VCExpressionGenerator.AndOp) ||

-           op.Equals(VCExpressionGenerator.OrOp)) {

-        // handle these operators without recursion

-        wr.Write("({0}", op.Equals(VCExpressionGenerator.AndOp) ? "and" : "or");

-        foreach (var ch in node.UniformArguments) {

-          wr.Write("\n");

-          Linearise(ch, options);

+            return true;

         }

-        wr.Write(")");

-        return true;

-      }

-

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

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

     }

 

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

diff --git a/Source/VCExpr/TermFormulaFlattening.cs b/Source/VCExpr/TermFormulaFlattening.cs
index 9198d753..7815413f 100644
--- a/Source/VCExpr/TermFormulaFlattening.cs
+++ b/Source/VCExpr/TermFormulaFlattening.cs
@@ -155,6 +155,12 @@ Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprLetBinding>>()))
 

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

 

+    public override bool AvoidVisit(VCExprNAry node, FlattenerState arg)

+    {

+        return node.Op.Equals(VCExpressionGenerator.AndOp) ||

+               node.Op.Equals(VCExpressionGenerator.OrOp);

+    }

+

     public override VCExpr Visit(VCExprNAry node, FlattenerState state){

 Contract.Requires(node != null);

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

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index 628ebdf1..2326ba7a 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1087,6 +1087,12 @@ namespace Microsoft.Boogie.TypeErasure {
 

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

 

+    public override bool AvoidVisit(VCExprNAry node, VariableBindings arg)

+    {

+        return node.Op.Equals(VCExpressionGenerator.AndOp) ||

+               node.Op.Equals(VCExpressionGenerator.OrOp);

+    }

+

     public override VCExpr Visit(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires(bindings != null);

       Contract.Requires(node != null);

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index c9d4f1c3..ad0c270d 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -859,11 +859,14 @@ namespace Microsoft.Boogie.VCExprAST {
         NAryExprTodoStack.Push(exprTodo[i]);

     }

 

+    public virtual bool AvoidVisit(VCExprNAry node, Arg arg)

+    {

+        return true;

+    }

+

     public virtual VCExpr Visit(VCExprNAry node, Arg arg) {

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

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

-      VCExprOp/*!*/ op = node.Op;

-      Contract.Assert(op != null);

       int initialStackSize = NAryExprTodoStack.Count;

       int initialResultStackSize = NAryExprResultStack.Count;

 

@@ -874,10 +877,10 @@ namespace Microsoft.Boogie.VCExprAST {
         Contract.Assert(subExpr != null);

 

         if (Object.ReferenceEquals(subExpr, CombineResultsMarker)) {

-          //

           // assemble a result

           VCExprNAry/*!*/ originalExpr = (VCExprNAry)NAryExprTodoStack.Pop();

           Contract.Assert(originalExpr != null);

+          VCExprOp/*!*/ op = originalExpr.Op;

           bool changed = false;

           List<VCExpr/*!*/>/*!*/ newSubExprs = new List<VCExpr/*!*/>();

 

@@ -893,8 +896,8 @@ namespace Microsoft.Boogie.VCExprAST {
           //

         } else {

           //

-          VCExprNAry narySubExpr = subExpr as VCExprNAry;

-          if (narySubExpr != null && narySubExpr.Op.Equals(op) &&

+            VCExprNAry narySubExpr = subExpr as VCExprNAry;

+          if (narySubExpr != null && this.AvoidVisit(narySubExpr, arg) &&

             // as in VCExprNAryUniformOpEnumerator, all expressions with

             // type parameters are allowed to be inspected more closely

               narySubExpr.TypeParamArity == 0) {