Fixed bugs. Improved Documentation. Improved test coverage.

src/main/java/org/logicng/cardinalityconstraints/CCEncoder.java

@@ -293,8 +293,10 @@ private List<Formula> amo(final EncodingResult result, final Variable... vars) {
    * @param vars   the variables of the constraint
    */
   private void exo(final EncodingResult result, final Variable... vars) {
-    if (vars.length == 0)
+    if (vars.length == 0) {
+      result.addClause();
       return;
+    }
     if (vars.length == 1) {
       result.addClause(vars[0]);
       return;

src/main/java/org/logicng/collections/LNGDoubleVector.java

@@ -163,7 +163,8 @@ public void pop() {
    * @param newSize the new size
    */
   public void shrinkTo(int newSize) {
-    this.size = newSize;
+    if (newSize < this.size)
+      this.size = newSize;
   }
 
   /**

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

@@ -105,7 +105,6 @@ public void remove() {
         maxWeight = c;
       if (c != 1) {
         cc = false;
-        break;
       }
     }
     for (final Literal lit : literals)
@@ -215,7 +214,8 @@ public Formula normalize() {
   }
 
   /**
-   * Internal helper for normalization of a <= constraint.
+   * Internal helper for normalization of a <= constraint. Can also be used for >= constraints by multiplying the right
+   * side and the coefficients with -1.
    * @param ps  the literals
    * @param cs  the coefficients
    * @param rhs the right-hand side

src/main/java/org/logicng/io/writers/FormulaDotFileWriter.java

@@ -55,7 +55,7 @@ public final class FormulaDotFileWriter {
    * Private constructor.
    */
   private FormulaDotFileWriter() {
-    throw new AssertionError();
+    // Intentionally left empty.
   }
 
   /**
@@ -178,9 +178,4 @@ private static void generateNaryDotString(final NAryOperator formula, final Stri
     for (final Formula operand : formula)
       sb.append("  id").append(id).append(" -> id").append(ids.get(operand)).append(";\n");
   }
-
-  @Override
-  public String toString() {
-    return this.getClass().getSimpleName();
-  }
 }

src/main/java/org/logicng/predicates/satisfiability/SATPredicate.java

@@ -77,7 +77,7 @@ public boolean test(final Formula formula, boolean cache) {
     else if (formula.type() == FType.TRUE || formula.type() == FType.LITERAL)
       result = true;
     else if (formula.holds(dnfPredicate))
-      result = formula != factory.falsum();
+      result = true;
     else {
       this.solver.add(formula);
       result = solver.sat() == Tristate.TRUE;

src/main/java/org/logicng/propositions/StandardProposition.java

@@ -43,15 +43,15 @@
 public final class StandardProposition extends Proposition {
 
   private final ImmutableFormulaList formulas;
-  private final String decription;
+  private final String description;
 
   /**
    * Constructs a new proposition for a single formulas.
    * @param formula the formulas
    */
   public StandardProposition(final Formula formula) {
     this.formulas = new ImmutableFormulaList(FType.AND, formula);
-    this.decription = "";
+    this.description = "";
   }
 
   /**
@@ -61,7 +61,7 @@ public StandardProposition(final Formula formula) {
    */
   public StandardProposition(final String description, final Formula formula) {
     this.formulas = new ImmutableFormulaList(FType.AND, formula);
-    this.decription = description;
+    this.description = description == null ? "" : description;
   }
 
   /**
@@ -71,7 +71,7 @@ public StandardProposition(final String description, final Formula formula) {
    */
   public StandardProposition(final String description, final Collection<? extends Formula> formulas) {
     this.formulas = new ImmutableFormulaList(FType.AND, formulas);
-    this.decription = description;
+    this.description = description == null ? "" : description;
   }
 
   /**
@@ -81,7 +81,7 @@ public StandardProposition(final String description, final Collection<? extends
    */
   public StandardProposition(final String description, final Formula... formulas) {
     this.formulas = new ImmutableFormulaList(FType.AND, formulas);
-    this.decription = description;
+    this.description = description == null ? "" : description;
   }
 
   /**
@@ -91,7 +91,7 @@ public StandardProposition(final String description, final Formula... formulas)
    */
   public StandardProposition(final String description, final ImmutableFormulaList formulas) {
     this.formulas = new ImmutableFormulaList(FType.AND, formulas);
-    this.decription = description;
+    this.description = description == null ? "" : description;
   }
 
   @Override
@@ -104,12 +104,12 @@ public ImmutableFormulaList formulas() {
    * @return the bagpack of this proposition
    */
   public String description() {
-    return this.decription == null ? "" : this.decription;
+    return this.description;
   }
 
   @Override
   public int hashCode() {
-    return Objects.hash(this.formulas, this.decription);
+    return Objects.hash(this.formulas, this.description);
   }
 
   @Override
@@ -118,13 +118,13 @@ public boolean equals(final Object other) {
       return true;
     if (other instanceof StandardProposition) {
       final StandardProposition o = (StandardProposition) other;
-      return Objects.equals(this.formulas, o.formulas) && Objects.equals(this.decription, o.decription);
+      return Objects.equals(this.formulas, o.formulas) && Objects.equals(this.description, o.description);
     }
     return false;
   }
 
   @Override
   public String toString() {
-    return String.format("StandardProposition{formulas=%s, description=%s}", this.formulas, this.decription);
+    return String.format("StandardProposition{formulas=%s, description=%s}", this.formulas, this.description);
   }
 }

src/main/java/org/logicng/pseudobooleans/PBEncoder.java

@@ -114,7 +114,7 @@ public ImmutableFormulaList encode(final PBConstraint constraint) {
       case PBC:
         final PBConstraint pbc = (PBConstraint) normalized;
         if (pbc.isCC())
-          return this.ccEncoder.encode(constraint);
+          return this.ccEncoder.encode(pbc);
         return new ImmutableFormulaList(FType.AND, this.encode(pbc.operands(), pbc.coefficients(), pbc.rhs()));
       case AND:
         final List<Formula> list = new LinkedList<>();

src/main/java/org/logicng/transformations/cnf/CNFFactorization.java

@@ -89,12 +89,14 @@ public Formula apply(final Formula formula, boolean cache) {
             return null;
           nops.add(this.apply(op, cache));
         }
-        final Iterator<Formula> it = nops.iterator();
-        cached = it.next();
-        while (it.hasNext()) {
-          if (!this.proceed)
-            return null;
-          cached = this.distribute(cached, it.next());
+        if (proceed) {
+          final Iterator<Formula> it = nops.iterator();
+          cached = it.next();
+          while (it.hasNext()) {
+            if (!this.proceed)
+              return null;
+            cached = this.distribute(cached, it.next());
+          }
         }
         break;
       case AND:
@@ -104,7 +106,8 @@ public Formula apply(final Formula formula, boolean cache) {
             return null;
           nops.add(this.apply(op, cache));
         }
-        cached = formula.factory().and(nops);
+        if (proceed)
+          cached = formula.factory().and(nops);
         break;
       case PBC:
         cached = formula.nnf();

src/main/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformation.java

@@ -117,10 +117,6 @@ private Formula computePosPolarity(final Formula formula, final Literal fixedPGV
     final FormulaFactory f = formula.factory();
     final Formula pgVar = fixedPGVar != null ? fixedPGVar : pgVariable(formula);
     switch (formula.type()) {
-      case NOT:
-        result = f.or(pgVar.negate(), pgVariable(((Not) formula).operand()).negate());
-        formula.setTransformationCacheEntry(PLAISTED_GREENBAUM_POS, result);
-        return result;
       case AND:
         List<Formula> nops = new ArrayList<>();
         for (final Formula op : formula)

src/main/java/org/logicng/transformations/dnf/DNFFactorization.java

@@ -90,7 +90,8 @@ public Formula apply(final Formula formula, boolean cache) {
             return null;
           nops.add(this.apply(op, cache));
         }
-        cached = formula.factory().or(nops);
+        if (proceed)
+          cached = formula.factory().or(nops);
         break;
       case AND:
         nops = new LinkedHashSet<>();
@@ -99,12 +100,14 @@ public Formula apply(final Formula formula, boolean cache) {
             return null;
           nops.add(this.apply(op, cache));
         }
-        final Iterator<Formula> it = nops.iterator();
-        cached = it.next();
-        while (it.hasNext()) {
-          if (!this.proceed)
-            return null;
-          cached = this.distribute(cached, it.next());
+        if (proceed) {
+          final Iterator<Formula> it = nops.iterator();
+          cached = it.next();
+          while (it.hasNext()) {
+            if (!this.proceed)
+              return null;
+            cached = this.distribute(cached, it.next());
+          }
         }
         break;
       default:

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

@@ -83,7 +83,7 @@ public void testEXO0() {
     final FormulaFactory f = new FormulaFactory();
     final PBConstraint cc = f.exo();
     for (final CCConfig config : this.configs)
-      Assert.assertTrue(new CCEncoder(f, config).encode(cc).empty());
+      Assert.assertEquals(f.falsum(), new CCEncoder(f, config).encode(cc).formula(f).cnf());
     Assert.assertTrue(f.newCCVariable().name().endsWith("_0"));
   }
 

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

@@ -0,0 +1,32 @@
+package org.logicng.formulas;
+
+import org.junit.Assert;
+import org.junit.Test;
+import org.logicng.formulas.cache.FunctionCacheEntry;
+import org.logicng.formulas.cache.PredicateCacheEntry;
+import org.logicng.formulas.cache.TransformationCacheEntry;
+import org.logicng.transformations.AIGTransformation;
+
+/**
+ * Unit tests for the package formulas.cache.
+ */
+public class CacheTest {
+
+  @Test
+  public void testDescription(){
+    Assert.assertEquals("TransformationCacheEntry{description=and-inverter graph}", TransformationCacheEntry.AIG.description());
+    Assert.assertEquals("TransformationCacheEntry{description=negation normal form}", TransformationCacheEntry.NNF.description());
+    Assert.assertEquals("TransformationCacheEntry{description=Plaisted & Greenbaum conjunctive normal form (positive polarity)}", TransformationCacheEntry.PLAISTED_GREENBAUM_POS.description());
+    Assert.assertEquals("TransformationCacheEntry{description=Tseitin conjunctive normal form}", TransformationCacheEntry.TSEITIN.description());
+    Assert.assertEquals("TransformationCacheEntry{description=factorized conjunctive normal form}", TransformationCacheEntry.FACTORIZED_CNF.description());
+
+    Assert.assertEquals("PredicateCacheEntry{description=and-inverter graph}", PredicateCacheEntry.IS_AIG.description());
+    Assert.assertEquals("PredicateCacheEntry{description=tautology}", PredicateCacheEntry.IS_TAUTOLOGY.description());
+    Assert.assertEquals("PredicateCacheEntry{description=conjunctive normal form}", PredicateCacheEntry.IS_CNF.description());
+
+    Assert.assertEquals("FunctionCacheEntry{description=literal profile}", FunctionCacheEntry.LITPROFILE.description());
+    Assert.assertEquals("FunctionCacheEntry{description=variable profile}", FunctionCacheEntry.VARPROFILE.description());
+    Assert.assertEquals("FunctionCacheEntry{description=sub-formulas}", FunctionCacheEntry.SUBFORMULAS.description());
+  }
+
+}

src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java

@@ -164,16 +164,16 @@ public void testSpecialCases(){
     }
   }
 
-
-  public void showBug(){
+  @Test
+  public void testCCNormalized(){
     List<Literal> lits = new ArrayList<>();
     lits.add(f.literal("m", true));
     lits.add(f.literal("n", true));
     List<Integer> coeffs2 = new ArrayList<>();
     coeffs2.add(2);
     coeffs2.add(2);
     PBConstraint normCC = f.pbc(CType.LE, 2, lits, coeffs2);
-    System.out.println(encoders[0].encode(normCC).toString());
+    Assert.assertEquals("AND[~m | ~n]", encoders[0].encode(normCC).toString());
   }
 
 //  @Ignore //TODO