diff options
author | MichalMoskal <unknown> | 2011-02-15 21:38:34 +0000 |
---|---|---|
committer | MichalMoskal <unknown> | 2011-02-15 21:38:34 +0000 |
commit | 1db9296da33686ae51028eea404462342b24ebf8 (patch) | |
tree | 8038efbfd5d5801a324b3f587feff070ee0340c1 /Source/VCExpr/VCExprAST.cs | |
parent | f27cd4a2be87c59d6988feb83533e32a77886e61 (diff) |
Add VCExprNAry.UniformArguments property to return arguments of nested And/Or nodes.
Diffstat (limited to 'Source/VCExpr/VCExprAST.cs')
-rw-r--r-- | Source/VCExpr/VCExprAST.cs | 13 |
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
|