diff options
author | akashlal <unknown> | 2013-11-29 12:30:16 +0530 |
---|---|---|
committer | akashlal <unknown> | 2013-11-29 12:30:16 +0530 |
commit | d8e2a6ac4b1607bb2ba3746c97587495af9938e7 (patch) | |
tree | 816443ea6b1b305e31a3bd4b54bc44849ad4b453 /Source | |
parent | 8c89524279690a8e408ba3e51625ee6da3759c84 (diff) |
binary tree of ANDs saves stack space
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Houdini/AbstractHoudini.cs | 19 |
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>();
|