binary tree of ANDs saves stack space

1 files changed, 15 insertions, 4 deletions

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>();