Browse Source

Add utility methods JDD.FindMinOver and JDD.FindMaxOver.

accumulation-v4.7
Dave Parker 7 years ago
parent
commit
4fd6dfa7c7
  1. 28
      prism/src/jdd/JDD.java

28
prism/src/jdd/JDD.java

@ -954,6 +954,20 @@ public class JDD
return rv; return rv;
} }
/**
* Returns the minimum terminal in the part of
* dd that overlaps with filter.
* If filter is empty, returns +infinity.
* <br>[ REFS: <i>none</i>, DEREFS: <i>filter</i> ]
*/
public static double FindMinOver(JDDNode dd, JDDNode filter)
{
JDDNode filtered = JDD.ITE(filter, dd.copy(), JDD.PlusInfinity());
double rv = FindMin(filtered);
JDD.Deref(filtered);
return rv;
}
/** /**
* returns maximum terminal in dd * returns maximum terminal in dd
* <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ] * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
@ -977,6 +991,20 @@ public class JDD
return rv; return rv;
} }
/**
* Returns the maximum terminal in the part of
* dd that overlaps with filter.
* If filter is empty, returns -infinity.
* <br>[ REFS: <i>none</i>, DEREFS: <i>filter</i> ]
*/
public static double FindMaxOver(JDDNode dd, JDDNode filter)
{
JDDNode filtered = JDD.ITE(filter, dd.copy(), JDD.MinusInfinity());
double rv = FindMax(filtered);
JDD.Deref(filtered);
return rv;
}
/** /**
* returns dd restricted to first non-zero path (cube) * returns dd restricted to first non-zero path (cube)
* <br>[ REFS: <i>result</i>, DEREFS: dd ] * <br>[ REFS: <i>result</i>, DEREFS: dd ]

Loading…
Cancel
Save