diff options
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 | 48 |
3 files changed, 49 insertions, 11 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 02220057..ad0c270d 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -288,14 +288,15 @@ namespace Microsoft.Boogie.VCExprAST { node.Op == VCExpressionGenerator.ImpliesOp)) {
Contract.Assert(node.Op != null);
VCExprOp op = node.Op;
-
- IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
- enumerator.MoveNext(); // skip the node itself
-
+ HashSet<VCExprOp> ops = new HashSet<VCExprOp>();
+ ops.Add(VCExpressionGenerator.AndOp);
+ ops.Add(VCExpressionGenerator.OrOp);
+ ops.Add(VCExpressionGenerator.ImpliesOp);
+ IEnumerator enumerator = new VCExprNAryMultiUniformOpEnumerator(node, ops);
while (enumerator.MoveNext()) {
- VCExpr/*!*/ expr = cce.NonNull((VCExpr/*!*/)enumerator.Current);
+ VCExpr expr = cce.NonNull((VCExpr)enumerator.Current);
VCExprNAry naryExpr = expr as VCExprNAry;
- if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ if (naryExpr == null || !ops.Contains(naryExpr.Op)) {
expr.Accept(this, arg);
} else {
StandardResult(expr, arg);
@@ -433,6 +434,28 @@ namespace Microsoft.Boogie.VCExprAST { }
}
+ public class VCExprNAryMultiUniformOpEnumerator : VCExprNAryEnumerator
+ {
+ private readonly HashSet<VCExprOp> Ops;
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(Ops != null);
+ }
+
+ public VCExprNAryMultiUniformOpEnumerator(VCExprNAry completeExpr, HashSet<VCExprOp> ops)
+ : base(completeExpr)
+ {
+ Contract.Requires(completeExpr != null);
+
+ this.Ops = ops;
+ }
+ protected override bool Descend(VCExprNAry expr)
+ {
+ return Ops.Contains(expr.Op) && expr.TypeParamArity == 0;
+ }
+ }
+
//////////////////////////////////////////////////////////////////////////////
// Visitor that knows about the variables bound at each location in a VCExpr
@@ -836,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;
@@ -851,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/*!*/>();
@@ -870,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) {
|