Browse Source

JDD: add multi-operand And and Or methods (convenience wrappers around binary And / Or)

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11221 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 10 years ago
parent
commit
8aa10e320d
  1. 50
      prism/src/jdd/JDD.java

50
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.
* <br>
* Returns JDD.Constant(0) for empty argument list
* <br>[ REFS: <i>result</i>, DEREFS: <i>all arguments</i> ]
*/
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.
* <br>
* Returns JDD.Constant(1) for empty argument list
* <br>[ REFS: <i>result</i>, DEREFS: <i>all arguments</i> ]
*/
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
* <br>[ REFS: <i>result</i>, DEREFS: dd1, dd2 ]

Loading…
Cancel
Save