Add VCExprNAry.UniformArguments property to return arguments of nested And/Or nodes.

1 files changed, 13 insertions, 0 deletions

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 74505150..49440ff0 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -915,6 +915,19 @@ namespace Microsoft.Boogie.VCExprAST {
     internal static readonly List<Type/*!*/>/*!*/ EMPTY_TYPE_LIST = new List<Type/*!*/>();

     internal static readonly List<VCExpr/*!*/>/*!*/ EMPTY_VCEXPR_LIST = new List<VCExpr/*!*/>();

 

+    public IEnumerable<VCExpr> UniformArguments

+    {

+      get

+      {

+        var enumerator = new VCExprNAryUniformOpEnumerator(this);

+        while (enumerator.MoveNext()) {

+          VCExprNAry naryExpr = enumerator.Current as VCExprNAry;

+          if (naryExpr == null || !naryExpr.Op.Equals(this.Op)) {

+            yield return (VCExpr)enumerator.Current;

+          }

+        }

+      }

+    }

   }

 

   // We give specialised implementations for nullary, unary and binary expressions