From 8cc8a212cbd404410b222012901c2c3ddaef09f1 Mon Sep 17 00:00:00 2001
From: Christoph Zengler <christoph.zengler@booleworks.com>
Date: Fri, 7 Dec 2018 15:40:16 +0100
Subject: [PATCH] Adjust special variable counters when importing formulas

---
 pom.xml                                       |  1 +
 .../org/logicng/formulas/FormulaFactory.java  | 27 +++++++++++++++++-
 .../FormulaFactoryImporterTest.java           | 28 +++++++++++++++++++
 3 files changed, 55 insertions(+), 1 deletion(-)

diff --git a/pom.xml b/pom.xml
index 173f4bbf..a832a610 100644
--- 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
index 5b56b135..116d4eb2 100644
--- 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
index dde16ce1..9c39aaf7 100644
--- 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