Further improvements to test coverage.

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

@@ -256,6 +256,23 @@ public void testLargeModularTotalizerAMK() {
     }
   }
 
+  @Test
+  public void testToString(){
+    String expected = "CCConfig{\n" +
+            "amoEncoder=BEST\n" +
+            "amkEncoder=TOTALIZER\n" +
+            "alkEncoder=TOTALIZER\n" +
+            "exkEncoder=BEST\n" +
+            "bimanderGroupSize=SQRT\n" +
+            "bimanderFixedGroupSize=3\n" +
+            "nestingGroupSize=4\n" +
+            "productRecursiveBound=20\n" +
+            "commanderGroupSize=3\n" +
+            "}\n";
+    Assert.assertEquals(expected, encoders[0].config().toString());
+    Assert.assertEquals(expected, encoders[0].toString());
+  }
+
   @Ignore
   @Test
   public void testVeryLargeModularTotalizerAMK() {

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

@@ -196,8 +196,11 @@ public void testAtomicFormula() {
   }
 
   @Test
-  public void testContains() {
+  public void testContains() throws ParserException {
     Assert.assertTrue(F.AND3.containsVariable(F.f.variable("x")));
     Assert.assertFalse(F.AND3.containsVariable(F.f.variable("a")));
+    PropositionalParser parser = new PropositionalParser(F.f);
+    Formula contAnd = parser.parse("a & b & (c | (d & e))");
+    Assert.assertTrue(contAnd.containsNode(parser.parse("d & e")));
   }
 }

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

@@ -7,6 +7,9 @@
 import org.logicng.formulas.cache.TransformationCacheEntry;
 import org.logicng.transformations.AIGTransformation;
 
+import java.util.Arrays;
+import java.util.List;
+
 /**
  * Unit tests for the package formulas.cache.
  */
@@ -29,4 +32,22 @@ public void testDescription(){
     Assert.assertEquals("FunctionCacheEntry{description=sub-formulas}", FunctionCacheEntry.SUBFORMULAS.description());
   }
 
+  @Test
+  public void testValues(){
+    List<TransformationCacheEntry> valuesTrans = Arrays.asList(TransformationCacheEntry.values());
+    Assert.assertTrue(valuesTrans.size() == 9);
+    Assert.assertTrue(valuesTrans.contains(TransformationCacheEntry.valueOf("FACTORIZED_DNF")));
+    Assert.assertTrue(valuesTrans.contains(TransformationCacheEntry.valueOf("PLAISTED_GREENBAUM_NEG")));
+
+    List<PredicateCacheEntry> valuesPred = Arrays.asList(PredicateCacheEntry.values());
+    Assert.assertTrue(valuesPred.size() == 5);
+    Assert.assertTrue(valuesPred.contains(PredicateCacheEntry.valueOf("IS_DNF")));
+    Assert.assertTrue(valuesPred.contains(PredicateCacheEntry.valueOf("IS_SAT")));
+
+    List<FunctionCacheEntry> valuesFunc = Arrays.asList(FunctionCacheEntry.values());
+    Assert.assertTrue(valuesFunc.size() == 3);
+    Assert.assertTrue(valuesFunc.contains(FunctionCacheEntry.valueOf("LITPROFILE")));
+    Assert.assertTrue(valuesFunc.contains(FunctionCacheEntry.valueOf("SUBFORMULAS")));
+  }
+
 }

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

@@ -187,8 +187,11 @@ public void testAtomicFormula() {
   }
 
   @Test
-  public void testContains() {
+  public void testContains() throws ParserException {
     Assert.assertTrue(F.OR1.containsVariable(F.f.variable("x")));
     Assert.assertFalse(F.OR1.containsVariable(F.f.variable("a")));
+    PropositionalParser parser = new PropositionalParser(F.f);
+    Formula contAnd = parser.parse("a | b | (c & (d | e))");
+    Assert.assertTrue(contAnd.containsNode(parser.parse("d | e")));
   }
 }

src/test/java/org/logicng/predicates/CNFPredicateTest.java

@@ -59,4 +59,9 @@ public void test() {
     Assert.assertFalse(F.NOT2.holds(cnfPredicate));
     Assert.assertFalse(F.f.and(F.OR1, F.EQ1).holds(cnfPredicate));
   }
+
+  @Test
+  public void testToString(){
+    Assert.assertEquals("CNFPredicate", cnfPredicate.toString());
+  }
 }

src/test/java/org/logicng/predicates/DNFPredicateTest.java

@@ -59,4 +59,9 @@ public void test() {
     Assert.assertFalse(F.NOT2.holds(dnfPredicate));
     Assert.assertFalse(F.f.or(F.AND1, F.EQ1).holds(dnfPredicate));
   }
+
+  @Test
+  public void testToString(){
+    Assert.assertEquals("DNFPredicate", dnfPredicate.toString());
+  }
 }

src/test/java/org/logicng/solvers/maxsat/PartialMaxSATTest.java

@@ -161,6 +161,7 @@ public void testTimeoutHandler() throws IOException {
     readCNF(solver, "tests/partialmaxsat/c1355_F176gat-1278gat@1.wcnf");
     MaxSATHandler handler = new TimeoutMaxSATHandler(1000);
     Assert.assertEquals(MaxSAT.MaxSATResult.UNDEF, solver.solve(handler));
+    Assert.assertTrue(handler.lowerBoundApproximation()<33);
 
     solver = MaxSATSolver.wbo(new MaxSATConfig.Builder().verbosity(SOME).output(logStream).build());
     readCNF(solver, "tests/partialmaxsat/c1355_F1229gat@1.wcnf");

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

@@ -89,12 +89,14 @@ public void testAssume() throws ParserException {
       Assert.assertEquals(TRUE, s.sat(f.variable("d")));
       Assert.assertEquals(TRUE, s.sat(f.variable("e")));
       Assert.assertEquals(TRUE, s.sat(f.variable("f")));
+      Assert.assertEquals(TRUE, s.sat(f.variable("g")));
       Assert.assertEquals(FALSE, s.sat(f.variable("a")));
       Assert.assertEquals(FALSE, s.sat(f.literal("b", false)));
       Assert.assertEquals(FALSE, s.sat(f.literal("c", false)));
       Assert.assertEquals(FALSE, s.sat(f.literal("d", false)));
       Assert.assertEquals(FALSE, s.sat(f.literal("e", false)));
       Assert.assertEquals(FALSE, s.sat(f.literal("f", false)));
+      Assert.assertEquals(TRUE, s.sat(f.literal("g", false)));
       Assert.assertEquals(TRUE, s.sat(assumptions1));
       Assert.assertEquals(TRUE, s.sat(assumptions2));
       Assert.assertEquals(TRUE, s.sat(assumptions3));

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

@@ -32,24 +32,23 @@
 import org.junit.Test;
 import org.logicng.datastructures.Assignment;
 import org.logicng.datastructures.Tristate;
-import org.logicng.formulas.F;
-import org.logicng.formulas.Formula;
-import org.logicng.formulas.FormulaFactory;
-import org.logicng.formulas.Literal;
-import org.logicng.formulas.Variable;
+import org.logicng.formulas.*;
 import org.logicng.handlers.NumberOfModelsHandler;
+import org.logicng.handlers.SATHandler;
 import org.logicng.handlers.TimeoutSATHandler;
 import org.logicng.io.parsers.ParserException;
 import org.logicng.io.parsers.PropositionalParser;
 import org.logicng.propositions.StandardProposition;
 import org.logicng.solvers.CleaneLing;
 import org.logicng.solvers.MiniSat;
 import org.logicng.solvers.SATSolver;
+import org.logicng.solvers.SolverState;
 
 import java.io.BufferedReader;
 import java.io.File;
 import java.io.FileReader;
 import java.io.IOException;
+import java.text.Normalizer;
 import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
@@ -63,6 +62,7 @@
 
 /**
  * Unit tests for the SAT solvers.
+ *
  * @version 1.1
  * @since 1.0
  */
@@ -72,6 +72,7 @@ public class SATTest {
   private final SATSolver[] solvers;
   private final PigeonHoleGenerator pg;
   private final PropositionalParser parser;
+  private final String[] testStrings;
 
   public SATTest() {
     this.f = new FormulaFactory();
@@ -87,6 +88,16 @@ public SATTest() {
     this.solvers[5] = CleaneLing.minimalistic(f);
     this.solvers[6] = CleaneLing.full(f, new CleaneLingConfig.Builder().plain(true).glueUpdate(true).gluered(true).build());
     this.solvers[7] = CleaneLing.full(f);
+
+    this.testStrings = new String[8];
+    this.testStrings[0] = "MiniSat{result=UNDEF, incremental=true}";
+    this.testStrings[1] = "MiniSat{result=UNDEF, incremental=false}";
+    this.testStrings[2] = "MiniSat{result=UNDEF, incremental=false}";
+    this.testStrings[3] = "MiniSat{result=UNDEF, incremental=true}";
+    this.testStrings[4] = "MiniSat{result=UNDEF, incremental=false}";
+    this.testStrings[5] = "CleaneLing{result=UNDEF, idx2name={}}";
+    this.testStrings[6] = "CleaneLing{result=UNDEF, idx2name={}}";
+    this.testStrings[7] = "CleaneLing{result=UNDEF, idx2name={}}";
   }
 
   @Test
@@ -95,6 +106,7 @@ public void testTrue() {
       s.add(F.TRUE);
       Assert.assertEquals(TRUE, s.sat());
       Assert.assertEquals(0, s.model().size());
+      Assert.assertTrue(s.toString().contains("{result=TRUE"));
       s.reset();
     }
   }
@@ -219,6 +231,42 @@ public void testCC1() throws InterruptedException {
     }
   }
 
+  @Test
+  public void testPBC() {
+    for (SATSolver s : this.solvers) {
+      List<Literal> lits = new ArrayList<>();
+      List<Integer> coeffs = new ArrayList<>();
+      Variable[] vars = new Variable[5];
+      for (int i = 0; i < 5; i++) {
+        lits.add(f.literal("x" + i, i % 2 == 0));
+        vars[i] = f.variable("x" + i);
+        coeffs.add(i + 1);
+      }
+      s.add(f.pbc(CType.GE, 10, lits, coeffs));
+      Assert.assertEquals(Tristate.TRUE, s.sat());
+      s.reset();
+    }
+  }
+
+  @Test
+  public void testWithRelaxation() throws ParserException {
+    PropositionalParser parser = new PropositionalParser(f);
+    Formula one = parser.parse("a & b & (c | ~d)");
+    Formula two = parser.parse("~a | ~c");
+
+    for (SATSolver s : this.solvers) {
+      s.add(one);
+      s.addWithRelaxation(f.variable("d"), two);
+      Assert.assertEquals(Tristate.TRUE, s.sat());
+      try {
+        Assert.assertEquals(2, s.enumerateAllModels().size());
+      }catch (Exception e){
+        Assert.assertTrue(e instanceof UnsupportedOperationException);
+      }
+      s.reset();
+    }
+  }
+
   @Test(expected = UnsupportedOperationException.class)
   public void testIllegalEnumeration() {
     final SATSolver s = this.solvers[7];
@@ -441,4 +489,73 @@ public void testNumberOfModelHandler() {
   public void testIllegalHandler() {
     new NumberOfModelsHandler(0);
   }
+
+  @Test(expected = IllegalArgumentException.class)
+  public void testAddNonCCAsCC(){
+    MiniSat solver = MiniSat.miniSat(f);
+    solver.addIncrementalCC((PBConstraint) F.PBC3);
+  }
+
+  @Test(expected = IllegalStateException.class)
+  public void testModelBeforeSolving(){
+    MiniSat solver = MiniSat.miniSat(f);
+    solver.model();
+  }
+
+  @Test(expected = IllegalArgumentException.class)
+  public void testCLAddNonCCAsCC(){
+    CleaneLing solver = CleaneLing.minimalistic(f, new CleaneLingConfig.Builder().gluered(true).build());
+    solver.addIncrementalCC((PBConstraint) F.PBC3);
+  }
+
+  @Test(expected = IllegalStateException.class)
+  public void testCLModelBeforeSolving(){
+    CleaneLing solver = CleaneLing.minimalistic(f);
+    solver.model();
+  }
+
+  @Test(expected = UnsupportedOperationException.class)
+  public void testCLSatWithLit(){
+    CleaneLing solver = CleaneLing.minimalistic(f);
+    solver.add(F.AND1);
+    solver.sat(new TimeoutSATHandler(10000), F.A);
+  }
+
+  @Test(expected = UnsupportedOperationException.class)
+  public void testCLSaveState(){
+    CleaneLing solver = CleaneLing.minimalistic(f);
+    solver.add(F.AND1);
+    solver.saveState();
+  }
+
+  @Test(expected = UnsupportedOperationException.class)
+  public void testCLLoadState(){
+    CleaneLing solver = CleaneLing.minimalistic(f);
+    solver.add(F.AND1);
+    solver.loadState(new SolverState(27, new int[3]));
+  }
+
+  @Test(expected = UnsupportedOperationException.class)
+  public void testCLSatWithLitCollection(){
+    CleaneLing solver = CleaneLing.minimalistic(f);
+    solver.add(F.AND1);
+    List<Literal> lits = new ArrayList<>();
+    lits.add(F.A);
+    lits.add(F.B);
+    solver.sat(new TimeoutSATHandler(10000), lits);
+  }
+
+  @Test(expected = UnsupportedOperationException.class)
+  public void testCLEnumerateWithWrongConfig(){
+    CleaneLing solver = CleaneLing.full(f,new CleaneLingConfig.Builder().plain(false).build());
+    solver.add(F.AND1);
+    solver.enumerateAllModels();
+  }
+
+  @Test
+  public void testToString() {
+    for (int i = 0; i < this.solvers.length; i++) {
+      Assert.assertEquals(this.testStrings[i], this.solvers[i].toString());
+    }
+  }
 }

src/test/java/org/logicng/transformations/AIGTest.java

@@ -147,5 +147,6 @@ public void testPBC(){
   @Test
   public void testToString(){
     Assert.assertEquals("AIGTransformation", aigTrans.toString());
+    Assert.assertEquals("AIGPredicate", aigPred.toString());
   }
 }

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

@@ -37,6 +37,7 @@
 
 /**
  * Unit tests for the class {@link CNFEncoder}.
+ *
  * @version 1.1
  * @since 1.1
  */
@@ -154,4 +155,25 @@ public void testAdvancedEncoder() throws ParserException {
     Assert.assertEquals(p.parse("(z1 | z2) & z3 & z4 & (~@RESERVED_CNF_2 | z1) & (~@RESERVED_CNF_2 | z5) & (~@RESERVED_CNF_2 | ~z6) & (~@RESERVED_CNF_2 | ~z7) & (@RESERVED_CNF_2 | ~z1 | ~z5 | z6 | z7) & (@RESERVED_CNF_2 | z8 | z9)"), encoder3.encode(phi3));
   }
 
+  @Test
+  public void testToString() {
+    String expected = "CNFConfig{\n" +
+            "algorithm=TSEITIN\n" +
+            "fallbackAlgorithmForAdvancedEncoding=PLAISTED_GREENBAUM\n" +
+            "distributedBoundary=-1\n" +
+            "createdClauseBoundary=1000\n" +
+            "atomBoundary=12\n" +
+            "}\n";
+    FormulaFactory f = new FormulaFactory();
+    CNFConfig config = new CNFConfig.Builder().algorithm(CNFConfig.Algorithm.TSEITIN).fallbackAlgorithmForAdvancedEncoding(CNFConfig.Algorithm.PLAISTED_GREENBAUM).build();
+    CNFEncoder encoder = new CNFEncoder(f, config);
+    Assert.assertEquals(expected, config.toString());
+    Assert.assertEquals(expected, encoder.toString());
+  }
+
+  @Test(expected = IllegalArgumentException.class)
+  public void testWrongFallbackForConfig() {
+    CNFConfig config = new CNFConfig.Builder().fallbackAlgorithmForAdvancedEncoding(CNFConfig.Algorithm.FACTORIZATION).build();
+  }
+
 }

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

@@ -127,6 +127,11 @@ public void testCC() throws ParserException {
     Assert.assertEquals(p.parse("(d | @RESERVED_CC_1 | @RESERVED_CC_4) & (~@RESERVED_CC_3 | @RESERVED_CC_1 | @RESERVED_CC_4) & (~@RESERVED_CC_3 | d | @RESERVED_CC_4) & (~@RESERVED_CC_4 | @RESERVED_CC_0) & (~@RESERVED_CC_2 | @RESERVED_CC_0) & (~@RESERVED_CC_4 | ~@RESERVED_CC_2) & (c | @RESERVED_CC_3 | @RESERVED_CC_5) & (b | @RESERVED_CC_3 | @RESERVED_CC_5) & (b | c | @RESERVED_CC_5) & (~@RESERVED_CC_5 | @RESERVED_CC_2) & ~@RESERVED_CC_0"), p.parse("~(1 * b + 1 * c + 1 * d <= 1)").cnf());
   }
 
+  @Test
+  public void testToString(){
+    Assert.assertEquals("CNFFactorization", cnf.toString());
+  }
+
   private static class TestFactorizationHandler implements FactorizationHandler {
 
     private int distCount = 0;

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

@@ -203,6 +203,11 @@ public void testFactorization() throws ParserException {
     Assert.assertEquals(f4.variables().size(), f4.transform(pgf).variables().size());
   }
 
+  @Test
+  public void testToString(){
+    Assert.assertEquals("PlaistedGreenbaumTransformation{boundary=0}", pg.toString());
+  }
+
   private boolean equivalentModels(final Formula f1, final Formula f2, final SortedSet<Variable> vars) {
     final SATSolver s = MiniSat.miniSat(f1.factory());
     s.add(f1);

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

@@ -46,6 +46,7 @@
 
 /**
  * Unit Tests for {@link TseitinTransformation}.
+ *
  * @version 1.1
  * @since 1.0
  */
@@ -152,6 +153,11 @@ public void testCC() throws ParserException {
     Assert.assertEquals(p.parse("(d | @RESERVED_CC_1 | @RESERVED_CC_4) & (~@RESERVED_CC_3 | @RESERVED_CC_1 | @RESERVED_CC_4) & (~@RESERVED_CC_3 | d | @RESERVED_CC_4) & (~@RESERVED_CC_4 | @RESERVED_CC_0) & (~@RESERVED_CC_2 | @RESERVED_CC_0) & (~@RESERVED_CC_4 | ~@RESERVED_CC_2) & (c | @RESERVED_CC_3 | @RESERVED_CC_5) & (b | @RESERVED_CC_3 | @RESERVED_CC_5) & (b | c | @RESERVED_CC_5) & (~@RESERVED_CC_5 | @RESERVED_CC_2) & ~@RESERVED_CC_0"), p.parse("~(1 * b + 1 * c + 1 * d <= 1)").transform(ts));
   }
 
+  @Test
+  public void testToString() {
+    Assert.assertEquals("TseitinTransformation{boundary=0}", ts.toString());
+  }
+
   private boolean equivalentModels(final Formula f1, final Formula f2, final SortedSet<Variable> vars) {
     final SATSolver s = MiniSat.miniSat(f1.factory());
     s.add(f1);