store the BDD factory in the BDD

src/main/java/org/logicng/bdds/BDD.java

@@ -28,6 +28,16 @@
 
 package org.logicng.bdds;
 
+import org.logicng.datastructures.Assignment;
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.Variable;
+
+import java.math.BigDecimal;
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.List;
+import java.util.Objects;
+
 /**
  * The internal representation of a BDD.
  * @version 1.2
@@ -36,13 +46,16 @@
 public final class BDD {
 
   private final int index;
+  private final BDDFactory factory;
 
   /**
    * Constructs a new BDD with a given index.
-   * @param index the index
+   * @param index   the index
+   * @param factory the factory of this BDD
    */
-  public BDD(int index) {
+  public BDD(int index, final BDDFactory factory) {
     this.index = index;
+    this.factory = factory;
   }
 
   /**
@@ -53,14 +66,99 @@ public int index() {
     return this.index;
   }
 
+  /**
+   * Returns the factory of this BDD.
+   * @return the factory of this BDD
+   */
+  public BDDFactory factory() {
+    return this.factory;
+  }
+
+  /**
+   * Returns {@code true} if this BDD is a tautology, {@code false} otherwise.
+   * @return {@code true} if this BDD is a tautology, {@code false} otherwise
+   */
+  public boolean isTautology() {
+    return this.factory.isTautology(this);
+  }
+
+  /**
+   * Returns {@code true} if this BDD is a contradiction, {@code false} otherwise.
+   * @return {@code true} if this BDD is a contradiction, {@code false} otherwise
+   */
+  public boolean isContradiction() {
+    return this.factory.isContradiction(this);
+  }
+
+  /**
+   * Returns the model count of this BDD.
+   * @return the model count
+   */
+  public BigDecimal modelCount() {
+    return this.factory.modelCount(this);
+  }
+
+  /**
+   * Returns the model count of this BDD with a given number of unimportant variables.
+   * @param unimportantVars the number of unimportant variables
+   * @return the model count
+   */
+  public BigDecimal modelCount(int unimportantVars) {
+    return this.factory.modelCount(this, unimportantVars);
+  }
+
+  /**
+   * Enumerates all models of this BDD.
+   * @return the list of all models
+   */
+  public List<Assignment> enumerateAllModels() {
+    return enumerateAllModels((Collection<Variable>) null);
+  }
+
+  /**
+   * Enumerates all models of this BDD wrt. a given set of variables.
+   * @param variables the variables
+   * @return the list of all models
+   */
+  public List<Assignment> enumerateAllModels(final Variable[] variables) {
+    return this.enumerateAllModels(Arrays.asList(variables));
+  }
+
+  /**
+   * Enumerates all models of this BDD wrt. a given set of variables.
+   * @param variables the variables
+   * @return the list of all models
+   */
+  public List<Assignment> enumerateAllModels(final Collection<Variable> variables) {
+    return this.factory.enumerateAllModels(this, variables);
+  }
+
+  /**
+   * Returns a CNF formula for this BDD.
+   * @return the CNF for the formula represented by this BDD
+   */
+  public Formula cnf() {
+    return this.factory.cnf(this);
+  }
+
+  /**
+   * Returns a DNF formula for a this BDD.
+   * @return the DNF for the formula represented by this BDD
+   */
+  public Formula dnf() {
+    return this.factory.dnf(this);
+  }
+
   @Override
   public int hashCode() {
-    return index;
+    return Objects.hash(index, factory);
   }
 
   @Override
   public boolean equals(final Object other) {
-    return this == other || other instanceof BDD && this.index == ((BDD) other).index;
+    return this == other || other instanceof BDD
+            && this.index == ((BDD) other).index
+            && Objects.equals(this.factory, ((BDD) other).factory);
   }
 
   @Override

src/main/java/org/logicng/bdds/jbuddy/JBuddyFactory.java

@@ -109,7 +109,7 @@ public JBuddyFactory(int numNodes, int cacheSize, final FormulaFactory f) {
 
   @Override
   public BDD build(final Formula formula) {
-    return new BDD(buildRec(formula));
+    return new BDD(buildRec(formula), this);
   }
 
   /**

src/main/java/org/logicng/bdds/simple/BDDFactoryClassical.java

@@ -95,7 +95,7 @@ public BDDNode bddForFormula(final Formula formula) {
 
   @Override
   public BDD build(final Formula formula) {
-    return new BDD(this.build(formula, 0));
+    return new BDD(this.build(formula, 0), this);
   }
 
   @Override

src/main/java/org/logicng/bdds/simple/BDDFactoryComplementaryEdges.java

@@ -94,7 +94,7 @@ public BDDFactoryComplementaryEdges(final FormulaFactory f) {
 
   @Override
   public BDD build(final Formula f) {
-    return new BDD(buildRec(f));
+    return new BDD(buildRec(f), this);
   }
 
   @Override

src/test/java/org/logicng/bdds/simple/BDDFactoryTest.java

@@ -50,7 +50,7 @@ public void test1() throws ParserException {
     final PropositionalParser p = new PropositionalParser(f);
     final Formula f1 = p.parse("a & b | ~c");
     final BDDFactoryClassical bdd = new BDDFactoryClassical(f, f1.variables());
-    Assert.assertEquals(bdd.build(f1), new BDD(bdd.buildWithApply(f1)));
+    Assert.assertEquals(bdd.build(f1), new BDD(bdd.buildWithApply(f1), bdd));
   }