Recursive walking of Exprs doesn't play nice when the depth of the AST is high.

Reduce depth of AST whenever possible (e.g., use a binary tree instead of a
linear list of terms)

1 files changed, 17 insertions, 0 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 792262d3..d8cb623b 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -394,6 +394,23 @@ namespace Microsoft.Boogie {
       args.Add(subexpr);

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

     }

+

+    public static Expr BinaryTreeAnd(List<Expr> terms)

+    {

+        return BinaryTreeAnd(terms, 0, terms.Count - 1);

+    }

+

+    private static Expr BinaryTreeAnd(List<Expr> terms, int start, int end)

+    {

+        if (start > end)

+            return Expr.True;

+        if (start == end)

+            return terms[start];

+        if (start + 1 == end)

+            return Expr.And(terms[start], terms[start + 1]);

+        var mid = (start + end) / 2;

+        return Expr.And(BinaryTreeAnd(terms, start, mid), BinaryTreeAnd(terms, mid + 1, end));

+    }

   }

   [ContractClassFor(typeof(Expr))]

   public abstract class ExprContracts : Expr {