Include the importer functionality directly in the formula factory

src/main/java/org/logicng/formulas/FormulaFactory.java

@@ -36,6 +36,7 @@
 import org.logicng.io.parsers.ParserException;
 import org.logicng.io.parsers.PseudoBooleanParser;
 import org.logicng.pseudobooleans.PBEncoder;
+import org.logicng.transformations.FormulaFactoryImporter;
 import org.logicng.transformations.cnf.CNFEncoder;
 import org.logicng.util.Pair;
 
@@ -108,6 +109,7 @@ public class FormulaFactory {
   int pbCounter;
   int cnfCounter;
   private boolean cnfCheck;
+  private FormulaFactoryImporter importer;
 
   /**
    * Constructor for a new formula factory.
@@ -977,6 +979,19 @@ private void addFormulaAnd(final LinkedHashSet<Formula> ops, final Formula f) {
     }
   }
 
+  /**
+   * Imports a formula from another formula factory into this factory and returns it.  If the current factory of the
+   * formula is already this formula factory, the same instance will be returned.
+   * @param formula the formula to import
+   * @return the imported formula on this factory
+   */
+  public Formula importFormula(final Formula formula) {
+    if (this.importer == null) {
+      this.importer = new FormulaFactoryImporter(this);
+    }
+    return formula.transform(importer);
+  }
+
   /**
    * Returns a string representation of a formula with this factories string representation
    * @param formula the formula

src/test/java/org/logicng/formulas/FormulaFactoryTest.java

@@ -32,13 +32,17 @@
 import org.junit.Test;
 import org.logicng.configurations.Configuration;
 import org.logicng.configurations.ConfigurationType;
+import org.logicng.io.parsers.ParserException;
+import org.logicng.io.parsers.PropositionalParser;
 import org.logicng.solvers.maxsat.algorithms.MaxSATConfig;
 import org.logicng.solvers.sat.GlucoseConfig;
 import org.logicng.solvers.sat.MiniSatConfig;
 
 import java.util.ArrayList;
 import java.util.List;
 
+import static org.assertj.core.api.Assertions.assertThat;
+
 /**
  * Test some basic formula factory functionality.
  * @version 1.1
@@ -145,4 +149,26 @@ public void testCNF() {
     Assert.assertEquals(cnf, cnf.cnf());
     Assert.assertNotEquals(nCnf, nCnf.cnf());
   }
+
+  @Test
+  public void testImportFormula() throws ParserException {
+    final FormulaFactory f = new FormulaFactory("Factory F");
+    final FormulaFactory g = new FormulaFactory("Factory G");
+    final PropositionalParser pf = new PropositionalParser(f);
+    final String formula = "x1 & x2 & ~x3 => (x4 | (x5 <=> ~x1))";
+    final Formula ff = pf.parse(formula);
+    final Formula fg = g.importFormula(ff);
+    assertThat(fg).isEqualTo(ff);
+    assertThat(ff.factory()).isSameAs(f);
+    assertThat(fg.factory()).isSameAs(g);
+    assertThat(f.statistics()).isEqualToComparingOnlyGivenFields (g.statistics(), "positiveLiterals",
+            "negativeLiterals", "negations", "implications", "equivalences", "conjunctions2", "conjunctions3",
+            "conjunctions4", "conjunctionsN", "disjunctions2", "disjunctions3", "disjunctions4");
+    for (Literal litF : ff.literals()) {
+      assertThat(litF.factory()).isSameAs(f);
+    }
+    for (Literal litG : fg.literals()) {
+      assertThat(litG.factory()).isSameAs(g);
+    }
+  }
 }