diff options
Diffstat (limited to 'Source/VCExpr/VCExprASTVisitors.cs')
| -rw-r--r-- | Source/VCExpr/VCExprASTVisitors.cs | 35 |
1 files changed, 29 insertions, 6 deletions
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 02220057..c9d4f1c3 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
|