#66 Adding callback mechanisms for saturation

Author: woortwij

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

@@ -2185,6 +2185,34 @@ public static interface ContinuousStatsCallback {
         public void continuous(int usedBddNodes, long opMiss);
     }
 
+    /** Saturation callback with simple information. */
+    @FunctionalInterface
+    public static interface SaturationSimpleCallback {
+        /**
+         * The callback function that is invoked after every transition application performed by saturation.
+         *
+         * @param transition The index of the transition that was applied.
+         */
+        public void accept(int transition);
+    }
+
+    /**
+     * Saturation callback with debug information, notably the BDDs before and after applying a transition.
+     *
+     * @param <T> The BDD representation type.
+     */
+    @FunctionalInterface
+    public static interface SaturationDebugCallback<T> {
+        /**
+         * The callback function that is invoked after every transition application performed by saturation.
+         *
+         * @param transition The index of the transition that was applied.
+         * @param before The BDD to which the transition was applied.
+         * @param after The resulting BDD after applying the transition.
+         */
+        public void accept(int transition, T before, T after);
+    }
+
     /** The registered garbage collection statistics callbacks, or {@code null} if none registered. */
     protected List<GCStatsCallback> gcCallbacks = null;
 
@@ -2293,6 +2321,23 @@ public void registerContinuousStatsCallback(ContinuousStatsCallback callback) {
         continuousCallbacks.add(callback);
     }
 
+    /**
+     * Sets the callback function that is invoked after every transition application performed by saturation.
+     *
+     * @param callback The non-{@code null} callback function.
+     */
+    public abstract void setSaturationCallback(SaturationSimpleCallback callback);
+
+    /**
+     * Sets the callback function that is invoked after every transition application performed by saturation.
+     *
+     * @param callback The non-{@code null} callback function.
+     */
+    public abstract void setSaturationCallback(SaturationDebugCallback<BDD> callback);
+
+    /** Unsets the saturation callback function. */
+    public abstract void unsetSaturationCallback();
+
     /**
      * Unregister a garbage collection statistics callback.
      *

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

@@ -132,6 +132,29 @@ public abstract class BDDFactoryIntImpl extends BDDFactory {
 
     protected abstract void printTable_impl(/* bdd */int v);
 
+    protected abstract void setSaturationCallback_impl(SaturationDebugCallback<Integer> callback);
+
+    @Override
+    public void setSaturationCallback(SaturationSimpleCallback callback) {
+        setSaturationCallback_impl((transition, before, after) -> callback.accept(transition));
+    }
+
+    @Override
+    public void setSaturationCallback(SaturationDebugCallback<BDD> callback) {
+        setSaturationCallback_impl((transition, before, after) -> {
+            BDD beforeBdd = makeBDD(before);
+            BDD afterBdd = makeBDD(after);
+            callback.accept(transition, beforeBdd, afterBdd);
+            beforeBdd.free();
+            afterBdd.free();
+        });
+    }
+
+    @Override
+    public void unsetSaturationCallback() {
+        setSaturationCallback_impl(null);
+    }
+
     public class IntBDD extends BDD {
         protected /* bdd */int v;
 

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

@@ -50,6 +50,15 @@ public class JFactory extends BDDFactoryIntImpl {
 
     static final boolean SWAPCOUNT = false;
 
+    /** The default saturation callback function that does nothing. */
+    private static final SaturationDebugCallback<Integer> DEFAULT_SATURATION_CALLBACK = (t, b, a) -> { };
+
+    /**
+     * The non-{@code null} saturation callback function that is invoked after every transition application performed by
+     * saturation.
+     */
+    private SaturationDebugCallback<Integer> saturationCallback = DEFAULT_SATURATION_CALLBACK;
+
     private JFactory() {
     }
 
@@ -4061,7 +4070,9 @@ int saturationForward_rec(int states, int[] relations, int[] vars, int instance,
 
                 for (int i = current; i < next; i++) {
                     PUSHREF(result);
+                    int prevResult = result;
                     result = relnextUnion_rec(result, relations[i], result, vars[i]);
+                    saturationCallback.accept(i, prevResult, result);
                     POPREF(1);
                 }
 
@@ -4229,7 +4240,9 @@ int boundedSaturationForward_rec(int states, int bound, int[] relations, int[] v
 
                 for (int i = current; i < next; i++) {
                     PUSHREF(result);
+                    int prevResult = result;
                     result = or_rec(PUSHREF(relnextIntersection_rec(result, relations[i], bound, vars[i])), result);
+                    saturationCallback.accept(i, prevResult, result);
                     POPREF(2);
                 }
 
@@ -4369,7 +4382,9 @@ int saturationBackward_rec(int states, int[] relations, int[] vars, int instance
 
                 for (int i = current; i < next; i++) {
                     PUSHREF(result);
+                    int prevResult = result;
                     result = relprevUnion_rec(relations[i], result, result, vars[i]);
+                    saturationCallback.accept(i, prevResult, result);
                     POPREF(1);
                 }
 
@@ -4537,7 +4552,9 @@ int boundedSaturationBackward_rec(int states, int bound, int[] relations, int[]
 
                 for (int i = current; i < next; i++) {
                     PUSHREF(result);
+                    int prevResult = result;
                     result = or_rec(PUSHREF(relprevIntersection_rec(relations[i], result, bound, vars[i])), result);
+                    saturationCallback.accept(i, prevResult, result);
                     POPREF(2);
                 }
 
@@ -4560,6 +4577,11 @@ int boundedSaturationBackward_rec(int states, int bound, int[] relations, int[]
         return result;
     }
 
+    @Override
+    protected void setSaturationCallback_impl(SaturationDebugCallback<Integer> callback) {
+        saturationCallback = callback == null ? DEFAULT_SATURATION_CALLBACK : callback;
+    }
+
     int relprod_rec(int l, int r) {
         BddCacheDataI entry;
         int res;