From 86cb1bc74ca8b0242131145ce9d4cbab085c02fd Mon Sep 17 00:00:00 2001 From: qadeer Date: Thu, 18 Dec 2014 14:04:37 -0800 Subject: more work on reducing call stack consumption --- Source/Provers/SMTLib/SMTLibLineariser.cs | 94 ++++++++++++++++--------------- Source/VCExpr/TermFormulaFlattening.cs | 6 ++ Source/VCExpr/TypeErasure.cs | 6 ++ Source/VCExpr/VCExprASTVisitors.cs | 13 +++-- 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 conjuncts = new List(); - 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(); + booleanOps.Add(VCExpressionGenerator.NotOp); + booleanOps.Add(VCExpressionGenerator.ImpliesOp); + booleanOps.Add(VCExpressionGenerator.AndOp); + booleanOps.Add(VCExpressionGenerator.OrOp); + if (booleanOps.Contains(op)) + { + Stack exprs = new Stack(); + 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(OpLineariser, options); + return node.Accept(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>())) //////////////////////////////////////////////////////////////////////////// + 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() != 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() != 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/*!*/ newSubExprs = new List(); @@ -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) { -- cgit v1.2.3