BDDFactory: cache BDDPairings (#8302)

* BDDFactory: cache BDDPairings

Add a getPair method that computes a BDDPairing that maps variables to variables. The BDDPairing is cached to improve cache performance of BDD#replace(BDDPairing), BDD#replaceWith(BDDPairing), etc. Without caching, two equivalent pairings will have different IDs, and JFactory's replacecache will not share their work.

Caveat: BDDPairings are mutable, and mutating cached pairings is not safe. We should clean up the API to guard against that. (We currently never mutate a pairing after creating it).

projects/batfish-common-protocol/src/main/java/org/batfish/common/bdd/BDDUtils.java

@@ -42,14 +42,18 @@ public static BDDPairing swapPairing(BDD[] bv1, BDD[] bv2) {
     checkArgument(bv1.length > 0, "Cannot build swapPairing for empty bitvectors");
     checkArgument(bv1.length == bv2.length, "Bitvector lengths must be equal");
 
-    BDDFactory factory = bv1[0].getFactory();
-    BDDPairing pairing = factory.makePair();
-
-    for (int i = 0; i < bv1.length; i++) {
-      pairing.set(bv1[i].var(), bv2[i].var());
-      pairing.set(bv2[i].var(), bv1[i].var());
+    int l = bv1.length;
+    BDD[] oldvars = new BDD[l * 2];
+    BDD[] newvars = new BDD[l * 2];
+    for (int i = 0; i < l; i++) {
+      // forward
+      oldvars[i] = bv1[i];
+      newvars[i] = bv2[i];
+      // reverse
+      oldvars[l + i] = bv2[i];
+      newvars[l + i] = bv1[i];
     }
 
-    return pairing;
+    return bv1[0].getFactory().getPair(oldvars, newvars);
   }
 }

projects/bdd/BUILD

@@ -11,6 +11,7 @@ java_library(
     deps = [
         "@maven//:com_carrotsearch_hppc",
         "@maven//:com_google_code_findbugs_jsr305",
+        "@maven//:com_google_guava_guava",
         "@maven//:org_apache_logging_log4j_log4j_api",
     ],
 )

projects/bdd/pom.xml

@@ -128,7 +128,6 @@
     <dependency>
       <groupId>com.google.guava</groupId>
       <artifactId>guava</artifactId>
-      <scope>test</scope>
     </dependency>
 
     <dependency>

projects/bdd/src/main/java/net/sf/javabdd/BDDFactory.java

@@ -28,14 +28,20 @@
  */
 package net.sf.javabdd;
 
+import static com.google.common.base.Preconditions.checkArgument;
+
+import com.google.common.base.Objects;
 import java.lang.reflect.InvocationTargetException;
 import java.lang.reflect.Method;
 import java.math.BigInteger;
 import java.security.AccessControlException;
 import java.util.Arrays;
 import java.util.Collection;
+import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 import java.util.StringTokenizer;
+import javax.annotation.Nullable;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
@@ -569,6 +575,73 @@ public BDDPairing makePair(BDDDomain oldvar, BDDDomain newvar) {
     return p;
   }
 
+  private static final class PairCacheKey {
+    private final BDD[] _oldvars;
+    private final BDD[] _newvars;
+
+    private PairCacheKey(BDD[] oldvars, BDD[] newvars) {
+      _oldvars = oldvars;
+      _newvars = newvars;
+    }
+
+    @Override
+    public boolean equals(Object o) {
+      if (this == o) {
+        return true;
+      }
+      if (!(o instanceof PairCacheKey)) {
+        return false;
+      }
+      PairCacheKey that = (PairCacheKey) o;
+      return Arrays.equals(_oldvars, that._oldvars) && Arrays.equals(_newvars, that._newvars);
+    }
+
+    @Override
+    public int hashCode() {
+      return Objects.hashCode(Arrays.hashCode(_oldvars), Arrays.hashCode(_newvars));
+    }
+  }
+
+  /** Copy the input array of BDDs (the array and each individual {@link BDD} is copied). */
+  private static BDD[] copy(BDD[] bdds) {
+    BDD[] result = new BDD[bdds.length];
+    for (int i = 0; i < bdds.length; i++) {
+      result[i] = bdds[i].id();
+    }
+    return result;
+  }
+
+  private Map<PairCacheKey, BDDPairing> _pairCache = null; // lazy init
+
+  /**
+   * Compute a {@link BDDPairing} mapping {@code oldvars} to {@code newvars}. The returned pairing
+   * is cached to improve cache performance of {@link BDD#replace(BDDPairing)}, {@link
+   * BDD#replaceWith(BDDPairing)}, etc. Without caching, two equivalent pairings will have different
+   * IDs, and the cache will not share their work.
+   *
+   * <p>The returned {@link BDDPairing} must not be mutated -- it is unsafe to call {@link
+   * BDDPairing#set} or {@link BDDPairing#reset()}.
+   */
+  public BDDPairing getPair(BDD[] oldvars, BDD[] newvars) {
+    checkArgument(
+        oldvars.length == newvars.length, "getPair: oldvars and newvars must have the same length");
+    if (_pairCache == null) {
+      _pairCache = new HashMap<>();
+    }
+    @Nullable BDDPairing pair = _pairCache.get(new PairCacheKey(oldvars, newvars));
+    if (pair != null) {
+      return pair;
+    }
+    pair = makePair();
+    for (int i = 0; i < oldvars.length; i++) {
+      pair.set(oldvars[i].var(), newvars[i].var());
+    }
+    _pairCache.put(
+        new PairCacheKey(copy(oldvars), copy(newvars)), // defensive copy
+        pair);
+    return pair;
+  }
+
   /**
    * Duplicate a BDD variable.
    *