From d8e2a6ac4b1607bb2ba3746c97587495af9938e7 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Fri, 29 Nov 2013 12:30:16 +0530
Subject: binary tree of ANDs saves stack space

---
 Source/Houdini/AbstractHoudini.cs | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'Source/Houdini')

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index ac5ba95f..6817da88 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -158,8 +158,7 @@ namespace Microsoft.Boogie.Houdini {
                 worklist.Remove(worklist.First());
 
                 var gen = prover.VCExprGen;
-                Expr env = Expr.True;
-
+                var terms = new List<Expr>();
                 foreach (var tup in impl2FuncCalls[impl])
                 {
                     var controlVar = tup.Item2;
@@ -178,9 +177,9 @@ namespace Microsoft.Boogie.Houdini {
                             new Trigger(Token.NoToken, true, new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(controlVar), args) }),
                             term);
                     }
-
-                    env = Expr.And(env, term);
+                    terms.Add(term);
                 }
+                var env = BinaryTreeAnd(terms, 0, terms.Count - 1);
 
                 env.Typecheck(new TypecheckingContext((IErrorSink)null));
                 var envVC = prover.Context.BoogieExprTranslator.Translate(env);
@@ -269,6 +268,18 @@ namespace Microsoft.Boogie.Houdini {
             return overallOutcome;
         }
 
+        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));
+        }
+
         public IEnumerable<Function> GetAssignment()
         {
             var ret = new List<Function>();
-- 
cgit v1.2.3