diff options
| author |  qadeer <unknown> | 2014-12-18 14:04:37 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-12-18 14:04:37 -0800 |
| commit | 86cb1bc74ca8b0242131145ce9d4cbab085c02fd (patch) | |
| tree | 2e714b1801e6057351a103217979bc1eea5da670 /Source/VCExpr | |
| parent | 75b7f29830013051c14990d515d4948cdf917148 (diff) | |
more work on reducing call stack consumption
Diffstat (limited to 'Source/VCExpr')
| -rw-r--r-- | Source/VCExpr/TermFormulaFlattening.cs | 6 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasure.cs | 6 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTVisitors.cs | 13 |
3 files changed, 20 insertions, 5 deletions
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<List<VCExprLetBinding>>())) ////////////////////////////////////////////////////////////////////////////
+ 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<VCExpr>() != 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<VCExpr>() != 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<VCExpr/*!*/>/*!*/ newSubExprs = new List<VCExpr/*!*/>();
@@ -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) {
|