diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index 565c9c31..00095268 100644 --- a/prism/src/jdd/JDD.java +++ b/prism/src/jdd/JDD.java @@ -380,6 +380,30 @@ public class JDD } return ptrToNode(DD_Or(dd1.ptr(), dd2.ptr())); } + + /** + * Multi-operand Or (0/1-MTBDD disjunction) operation. + * Operands are processed from left-to-right. + *
+ * Returns JDD.Constant(0) for empty argument list + *
[ REFS: result, DEREFS: all arguments ] + */ + public static JDDNode Or(JDDNode... nodes) + { + if (nodes.length == 0) + return JDD.Constant(0); + + JDDNode result = nodes[0]; + for (int i = 1; i < nodes.length; i++) { + // note: Java overloading rules ensure that fixed arity + // methods take precedence. So, for two-operand Or, + // the Or(JDDNode,JDDNode) method above is called and we don't + // run into an infinite recursion + result = Or(result, nodes[i]); + } + + return result; + } /** * and of dd1, dd2 @@ -394,7 +418,31 @@ public class JDD return ptrToNode(DD_And(dd1.ptr(), dd2.ptr())); } - + + /** + * Multi-operand And (0/1-MTBDD conjunction) operation. + * Operands are processed from left-to-right. + *
+ * Returns JDD.Constant(1) for empty argument list + *
[ REFS: result, DEREFS: all arguments ] + */ + public static JDDNode And(JDDNode... nodes) + { + if (nodes.length == 0) + return JDD.Constant(1); + + JDDNode result = nodes[0]; + for (int i = 1; i < nodes.length; i++) { + // note: Java overloading rules ensure that fixed arity + // methods take precedence. So, for two-operand And, + // the And(JDDNode,JDDNode) method above is called and we don't + // run into an infinite recursion + result = And(result, nodes[i]); + } + + return result; + } + /** * xor of dd1, dd2 *
[ REFS: result, DEREFS: dd1, dd2 ]