Revert "fixed SATSolver#add: Ensure all variables are added to the internal solver"

This reverts commit 5cdab69.

Author: czengler

src/main/java/org/logicng/solvers/MiniSat.java

@@ -67,7 +67,7 @@
 
 /**
  * Wrapper for the MiniSAT-style SAT solvers.
- * @version 2.4.2
+ * @version 2.4.0
  * @since 1.0
  */
 public class MiniSat extends SATSolver {
@@ -271,18 +271,6 @@ public void add(final Formula formula, final Proposition proposition) {
         } else {
             addFormulaAsCNF(formula, proposition);
         }
-        addAllOriginalVariables(formula);
-    }
-
-    /**
-     * Adds all variables of the given formula to the solver if not already present.
-     * This method can be used to ensure that the internal solver knows the given variables.
-     * @param originalFormula the original formula
-     */
-    private void addAllOriginalVariables(final Formula originalFormula) {
-        for (final Variable var : originalFormula.variables()) {
-            getOrAddIndex(var);
-        }
     }
 
     protected void addFormulaAsCNF(final Formula formula, final Proposition proposition) {

src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java

@@ -46,7 +46,7 @@
 
 /**
  * Unit tests for the at-least-k configs.
- * @version 2.4.2
+ * @version 2.0.0
  * @since 1.0
  */
 public class CCALKTest implements LogicNGTest {
@@ -66,7 +66,7 @@ public void testALK() {
         int counter = 0;
         for (final CCConfig config : this.configs) {
             f.putConfiguration(config);
-            testCC(10, 0, 1024, f);
+            testCC(10, 0, 1, f);
             testCC(10, 1, 1023, f);
             testCC(10, 2, 1013, f);
             testCC(10, 3, 968, f);

src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java

@@ -43,7 +43,7 @@
 
 /**
  * Unit tests for the at-most-k encoders.
- * @version 2.4.2
+ * @version 2.0.0
  * @since 1.0
  */
 public class CCAMKTest implements LogicNGTest {
@@ -73,8 +73,8 @@ public void testAMK() {
             testCC(10, 7, 968, f, false);
             testCC(10, 8, 1013, f, false);
             testCC(10, 9, 1023, f, false);
-            testCC(10, 10, 1024, f, false);
-            testCC(10, 15, 1024, f, false);
+            testCC(10, 10, 1, f, false);
+            testCC(10, 15, 1, f, false);
             assertThat(f.newCCVariable().name()).endsWith("_" + counter++);
         }
     }

src/test/java/org/logicng/solvers/functions/ModelEnumerationFunctionTest.java

@@ -1,24 +1,19 @@
 package org.logicng.solvers.functions;
 
 import static org.assertj.core.api.Assertions.assertThat;
-import static org.logicng.util.FormulaHelper.variables;
 
 import org.junit.jupiter.api.Test;
 import org.logicng.datastructures.Assignment;
-import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
-import org.logicng.formulas.FormulaFactoryConfig;
-import org.logicng.formulas.Variable;
 import org.logicng.io.parsers.ParserException;
 import org.logicng.solvers.MiniSat;
 import org.logicng.solvers.SATSolver;
-import org.logicng.solvers.sat.MiniSatConfig;
 
 import java.util.List;
 
 /**
  * Units tests for {@link ModelEnumerationFunction}.
- * @version 2.4.2
+ * @version 2.3.0
  * @since 2.3.0
  */
 public class ModelEnumerationFunctionTest {
@@ -52,29 +47,4 @@ public void testFastEvaluable() throws ParserException {
         models = solver.execute(ModelEnumerationFunction.builder().fastEvaluable(true).build());
         assertThat(models).extracting(Assignment::fastEvaluable).containsOnly(true);
     }
-
-    @Test
-    public void testVariableRemovedBySimplificationOccursInModels() throws ParserException {
-        final FormulaFactory f = new FormulaFactory(FormulaFactoryConfig.builder().simplifyComplementaryOperands(true).build());
-        final SATSolver solver = MiniSat.miniSat(this.f, MiniSatConfig.builder().cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build());
-        final Variable a = f.variable("A");
-        final Variable b = f.variable("B");
-        final Formula formula = this.f.parse("A & B => A");
-        solver.add(formula); // during NNF conversion, used by the PG transformation, the formula simplifies to verum when added to the solver
-        final List<Assignment> models = solver.execute(ModelEnumerationFunction.builder().variables(formula.variables()).build());
-        assertThat(models).hasSize(4);
-        for (final Assignment model : models) {
-            assertThat(variables(model.literals())).containsExactlyInAnyOrder(a, b);
-        }
-    }
-
-    @Test
-    public void testUnknownVariableNotOccurringInModel() {
-        final SATSolver solver = MiniSat.miniSat(this.f);
-        final Variable a = this.f.variable("A");
-        solver.add(a);
-        final List<Assignment> models = solver.execute(ModelEnumerationFunction.builder().variables(this.f.variables("A", "X")).build());
-        assertThat(models).hasSize(1);
-        assertThat(models.get(0).literals()).containsExactly(a);
-    }
 }

src/test/java/org/logicng/solvers/sat/SATTest.java

@@ -33,7 +33,6 @@
 import static org.logicng.datastructures.Tristate.UNDEF;
 import static org.logicng.solvers.sat.MiniSatConfig.ClauseMinimization.BASIC;
 import static org.logicng.solvers.sat.MiniSatConfig.ClauseMinimization.NONE;
-import static org.logicng.util.FormulaHelper.variables;
 
 import org.junit.jupiter.api.Test;
 import org.logicng.LogicNGTest;
@@ -44,7 +43,6 @@
 import org.logicng.formulas.CType;
 import org.logicng.formulas.Formula;
 import org.logicng.formulas.FormulaFactory;
-import org.logicng.formulas.FormulaFactoryConfig;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 import org.logicng.handlers.ModelEnumerationHandler;
@@ -63,6 +61,7 @@
 import org.logicng.solvers.functions.ModelEnumerationFunction;
 import org.logicng.solvers.functions.UpZeroLiteralsFunction;
 import org.logicng.testutils.PigeonHoleGenerator;
+import org.logicng.util.FormulaHelper;
 
 import java.io.BufferedReader;
 import java.io.File;
@@ -82,7 +81,7 @@
 
 /**
  * Unit tests for the SAT solvers.
- * @version 2.4.1
+ * @version 1.6
  * @since 1.0
  */
 public class SATTest extends TestWithExampleFormulas implements LogicNGTest {
@@ -297,28 +296,6 @@ public void testPartialModel() {
         }
     }
 
-    @Test
-    public void testVariableRemovedBySimplificationOccursInModel() throws ParserException {
-        final FormulaFactory f = new FormulaFactory(FormulaFactoryConfig.builder().simplifyComplementaryOperands(true).build());
-        final SATSolver solver = MiniSat.miniSat(f, MiniSatConfig.builder().cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build());
-        final Variable a = f.variable("A");
-        final Variable b = f.variable("B");
-        final Formula formula = this.f.parse("A & B => A");
-        solver.add(formula); // during NNF conversion, used by the PG transformation, the formula simplifies to verum when added to the solver
-        assertThat(solver.sat()).isEqualTo(Tristate.TRUE);
-        assertThat(solver.knownVariables()).containsExactlyInAnyOrder(a, b);
-        assertThat(variables(solver.model().literals())).containsExactlyInAnyOrder(a, b);
-    }
-
-    @Test
-    public void testUnknownVariableNotOccurringInModel() {
-        final SATSolver solver = MiniSat.miniSat(this.f);
-        final Variable a = this.f.variable("A");
-        solver.add(a);
-        assertThat(solver.sat()).isEqualTo(Tristate.TRUE);
-        assertThat(solver.model(this.f.variables("A", "X")).literals()).containsExactly(a);
-    }
-
     @Test
     public void testModelEnumerationHandler() {
         for (final SATSolver s : this.solvers) {
@@ -364,6 +341,7 @@ public boolean foundModel(final Assignment assignment) {
     }
 
     @Test
+    @SuppressWarnings("deprecation")
     public void testWithRelaxation() throws ParserException {
         final PropositionalParser parser = new PropositionalParser(this.f);
         final Formula one = parser.parse("a & b & (c | ~d)");
@@ -844,6 +822,7 @@ public void testKnownVariables() throws ParserException {
     }
 
     @Test
+    @SuppressWarnings("deprecation")
     public void testAddWithoutUnknown() throws ParserException {
         final PropositionalParser parser = new PropositionalParser(this.f);
         final Formula phi = parser.parse("x1 & (~x2 | x3) & (x4 | ~x5)");
@@ -1107,7 +1086,7 @@ public void testDimacsFilesWithSelectionOrder() throws IOException {
                 if (fileName.endsWith(".cnf")) {
                     readCNF(solver, file);
                     final List<Literal> selectionOrder = new ArrayList<>();
-                    for (final Variable var : variables(solver.execute(FormulaOnSolverFunction.get()))) {
+                    for (final Variable var : FormulaHelper.variables(solver.execute(FormulaOnSolverFunction.get()))) {
                         if (selectionOrder.size() < 10) {
                             selectionOrder.add(var.negate());
                         }

src/test/java/org/logicng/transformations/cnf/BDDCNFTest.java

@@ -42,7 +42,7 @@
 
 /**
  * Unit Tests for {@link BDDCNFTransformation}.
- * @version 2.4.2
+ * @version 2.3.0
  * @since 1.4.0
  */
 public class BDDCNFTest extends TestWithExampleFormulas {
@@ -160,7 +160,7 @@ public void testNot() throws ParserException {
     @Test
     public void testCC() throws ParserException {
         final PseudoBooleanParser p = new PseudoBooleanParser(this.f);
-        final Formula f1 = p.parse("a <=> (1 * b <= 0)");
+        final Formula f1 = p.parse("a <=> (1 * b <= 1)");
         final Formula f2 = p.parse("~(1 * b <= 1)");
         final Formula f3 = p.parse("(1 * b + 1 * c + 1 * d <= 1)");
         final Formula f4 = p.parse("~(1 * b + 1 * c + 1 * d <= 1)");

src/test/java/org/logicng/transformations/dnf/BDDDNFTest.java

@@ -43,7 +43,7 @@
 
 /**
  * Unit Tests for {@link BDDDNFTransformation}.
- * @version 2.4.2
+ * @version 2.3.0
  * @since 2.3.0
  */
 public class BDDDNFTest extends TestWithExampleFormulas {
@@ -162,7 +162,7 @@ public void testNot() throws ParserException {
     @Test
     public void testCC() throws ParserException {
         final PseudoBooleanParser p = new PseudoBooleanParser(this.f);
-        final Formula f1 = p.parse("a <=> (1 * b <= 0)");
+        final Formula f1 = p.parse("a <=> (1 * b <= 1)");
         final Formula f2 = p.parse("~(1 * b <= 1)");
         final Formula f3 = p.parse("(1 * b + 1 * c + 1 * d <= 1)");
         final Formula f4 = p.parse("~(1 * b + 1 * c + 1 * d <= 1)");