Adjust special variable counters when importing formulas

logic-ng · Dec 7, 2018 · 8cc8a21 · 8cc8a21
1 parent f4cf868
commit 8cc8a21
Show file tree

Hide file tree

Showing 3 changed files with 55 additions and 1 deletion.
diff --git a/pom.xml b/pom.xml
@@ -155,6 +155,7 @@
       <plugin>
         <groupId>org.apache.maven.plugins</groupId>
         <artifactId>maven-surefire-plugin</artifactId>
+        <version>2.22.0</version>
         <configuration>
           <useSystemClassLoader>false</useSystemClassLoader>
         </configuration>

diff --git a/src/main/java/org/logicng/formulas/FormulaFactory.java b/src/main/java/org/logicng/formulas/FormulaFactory.java
@@ -998,7 +998,32 @@ public Formula importFormula(final Formula formula) {
     if (this.importer == null) {
       this.importer = new FormulaFactoryImporter(this);
     }
-    return formula.transform(this.importer);
+    final Formula imported = formula.transform(this.importer);
+    adjustCounters(imported);
+    return imported;
+  }
+
+  private void adjustCounters(Formula formula) {
+    for (Variable variable : formula.variables()) {
+      if (variable.name().startsWith(CC_PREFIX)) {
+        String[] tokens = variable.name().split("_");
+        int counter = Integer.parseInt(tokens[tokens.length - 1]);
+        if (this.ccCounter < counter)
+          this.ccCounter = counter + 1;
+      }
+      if (variable.name().startsWith(CNF_PREFIX)) {
+        String[] tokens = variable.name().split("_");
+        int counter = Integer.parseInt(tokens[tokens.length - 1]);
+        if (this.cnfCounter < counter)
+          this.cnfCounter = counter + 1;
+      }
+      if (variable.name().startsWith(PB_PREFIX)) {
+        String[] tokens = variable.name().split("_");
+        int counter = Integer.parseInt(tokens[tokens.length - 1]);
+        if (this.pbCounter < counter)
+          this.pbCounter = counter + 1;
+      }
+    }
   }
 
   /**

diff --git a/src/test/java/org/logicng/transformations/FormulaFactoryImporterTest.java b/src/test/java/org/logicng/transformations/FormulaFactoryImporterTest.java
@@ -33,6 +33,9 @@
 import org.logicng.formulas.F;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
+import org.logicng.io.parsers.ParserException;
+import org.logicng.io.parsers.PseudoBooleanParser;
+import org.logicng.transformations.cnf.TseitinTransformation;
 
 import static org.assertj.core.api.Assertions.assertThat;
 import static org.logicng.formulas.F.*;
@@ -215,6 +218,31 @@ public void testPBC() {
     assertThat(this.g.statistics().equivalences()).isEqualTo(0);
   }
 
+  @Test
+  public void testAdjustCounters() throws ParserException {
+    final FormulaFactory f = new FormulaFactory("Factory");
+    final PseudoBooleanParser p = new PseudoBooleanParser(f);
+    final Formula cc = p.parse("A + B + C + D + E <= 2").cnf();
+    final Formula pbc = p.parse("2*A + -2*B + 3*C + D + 2*E <= 3").cnf();
+    final Formula cnf = p.parse("A & B & C | C & D & ~A").transform(new TseitinTransformation(0));
+
+    final FormulaFactory g = new FormulaFactory();
+    g.newCNFVariable();
+    g.newCNFVariable();
+    g.newCCVariable();
+    g.newCCVariable();
+    g.newCCVariable();
+    g.newPBVariable();
+    g.newPBVariable();
+    g.newPBVariable();
+    g.importFormula(cc);
+    g.importFormula(pbc);
+    g.importFormula(cnf);
+    assertThat(g.statistics().cnfCounter()).isEqualTo(2);
+    assertThat(g.statistics().ccCounter()).isEqualTo(13);
+    assertThat(g.statistics().pbCounter()).isEqualTo(25);
+  }
+
   /**
    * Imports the given formula in the new formula factory.
    * @param formula the formula to import