Merge pull request #53 from wytseoortwijn/relprev_and_relnext

#52 Contribute BDD operations `relnext` and `relprev` and their restricted variants

Author: dhendriks

src/main/java/com/github/javabdd/BDD.java

@@ -586,6 +586,60 @@ public BDD relprod(BDD that, BDDVarSet var) {
      */
     public abstract BDD satOne(BDDVarSet var, boolean pol);
 
+    /**
+     * Computes the BDD that represents the set of successor states from {@code states}, i.e., the ones reachable by
+     * taking one forward step from states in {@code states}, where this BDD is the (partial) transition relation to
+     * consider. It is assumed that old-state and new-state BDD variables are interleaved in this transition relation,
+     * starting with the old-state variable, i.e., each old-state variable comes directly before its corresponding
+     * new-state variable.
+     *
+     * @param states The BDD representing the set of states.
+     * @param vars The BDD representing the set of variables that are relevant to consider for determining successor
+     * states. This variable set <i>must</i> include all variables that occur in the transition relation BDD. Moreover,
+     * for every new-state variable that is in {@code vars}, {@code relnext} considers the corresponding old-state
+     * variable to be relevant as well, regardless of whether it's included in {@code vars} or not.
+     * @return The BDD representing the set of successor states from {@code states}.
+     */
+    public abstract BDD relnext(BDD states, BDDVarSet vars);
+
+    /**
+     * Computes {@code and(relnext(states, vars), restriction)} as a single BDD operation.
+     *
+     * @param states The BDD representing the set of states.
+     * @param restriction The BDD representing the restriction to apply to the BDD representing the successor states.
+     * @param vars The BDD representing the set of relevant variables to consider. See {@link #relnext(BDD, BDDVarSet)
+     * relnext} for further details.
+     * @return The BDD representing the restricted set of successor states from {@code states}.
+     */
+    public abstract BDD relnextRestricted(BDD states, BDD restriction, BDDVarSet vars);
+
+    /**
+     * Computes the BDD that represents the set of predecessor states from {@code states}, i.e., the ones reachable by
+     * taking one backward step from states in {@code states}, where this BDD is the (partial) transition relation to
+     * consider. It is assumed that old-state and new-state BDD variables are interleaved in this transition relation,
+     * starting with the old-state variable, i.e., each old-state variable comes directly before its corresponding
+     * new-state variable.
+     *
+     * @param states The BDD representing the set of states.
+     * @param vars The BDD representing the set of variables that are relevant to consider for determining predecessor
+     * states. This variable set <i>must</i> include all variables that occur in the transition relation BDD. Moreover,
+     * for every new-state variable that is in {@code vars}, {@code relprev} considers the corresponding old-state
+     * variable to be relevant as well, regardless of whether it's included in {@code vars} or not.
+     * @return The BDD representing the set of predecessor states from {@code states}.
+     */
+    public abstract BDD relprev(BDD states, BDDVarSet vars);
+
+    /**
+     * Computes {@code and(relprev(states, vars), restriction)} as a single BDD operation.
+     *
+     * @param states The BDD representing the set of states.
+     * @param restriction The BDD representing the restriction to apply to the BDD representing the predecessor states.
+     * @param vars The BDD representing the set of relevant variables to consider. See {@link #relprev(BDD, BDDVarSet)
+     * relprev} for further details.
+     * @return The BDD representing the restricted set of predecessor states from {@code states}.
+     */
+    public abstract BDD relprevRestricted(BDD states, BDD restriction, BDDVarSet vars);
+
     /**
      * Finds all satisfying variable assignments.
      *

src/main/java/com/github/javabdd/BDDFactoryIntImpl.java

@@ -86,6 +86,16 @@ public abstract class BDDFactoryIntImpl extends BDDFactory {
 
     protected abstract /* bdd */int veccompose_impl(/* bdd */int v, BDDPairing p);
 
+    protected abstract /* bdd */int relnext_impl(/* bdd */int states, /* bdd */int relation, /* bdd */int vars);
+
+    protected abstract /* bdd */int relnextRestricted_impl(/* bdd */int states, /* bdd */int relation,
+            /* bdd */int restriction, /* bdd */int vars);
+
+    protected abstract /* bdd */int relprev_impl(/* bdd */int relation, /* bdd */int states, /* bdd */int vars);
+
+    protected abstract /* bdd */int relprevRestricted_impl(/* bdd */int relation, /* bdd */int states,
+            /* bdd */int restriction, /* bdd */int vars);
+
     protected abstract int nodeCount_impl(/* bdd */int v);
 
     protected abstract double pathCount_impl(/* bdd */int v);
@@ -325,6 +335,26 @@ public BDD veccompose(BDDPairing pair) {
         public BDDVarSet toVarSet() {
             return makeBDDVarSet(v);
         }
+
+        @Override
+        public BDD relnext(BDD states, BDDVarSet vars) {
+            return makeBDD(relnext_impl(unwrap(states), v, unwrap(vars)));
+        }
+
+        @Override
+        public BDD relnextRestricted(BDD states, BDD restriction, BDDVarSet vars) {
+            return makeBDD(relnextRestricted_impl(unwrap(states), v, unwrap(restriction), unwrap(vars)));
+        }
+
+        @Override
+        public BDD relprev(BDD states, BDDVarSet vars) {
+            return makeBDD(relprev_impl(v, unwrap(states), unwrap(vars)));
+        }
+
+        @Override
+        public BDD relprevRestricted(BDD states, BDD restriction, BDDVarSet vars) {
+            return makeBDD(relprevRestricted_impl(v, unwrap(states), unwrap(restriction), unwrap(vars)));
+        }
     }
 
     public class IntBDDWithFinalizer extends IntBDD {