Merge branch 'improveTestCoverage' into release_1.1

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

@@ -26,7 +26,7 @@
 //                                                                       //
 ///////////////////////////////////////////////////////////////////////////
 
-/**
+/*
  * PBLib       -- Copyright (c) 2012-2013  Peter Steinke
  *
  * Permission is hereby granted, free of charge, to any person obtaining a
@@ -155,6 +155,10 @@ public List<Formula> newUpperBound(int rhs) {
 
   /**
    * Tightens the upper bound of an at-most-k constraint and encodes it on the solver of the result.
+   *
+   * Usage constraints:
+   * -New right hand side must be smaller than current right hand side.
+   * -Cannot be used for at-least-k constraints.
    * @param rhs the new upperBound
    */
   public void newUpperBoundForSolver(int rhs) {
@@ -214,6 +218,10 @@ public List<Formula> newLowerBound(int rhs) {
 
   /**
    * Tightens the lower bound of an at-least-k constraint and encodes it on the solver of the result.
+   *
+   * Usage constraints:
+   * -New right hand side must be greater than current right hand side.
+   * -Cannot be used for at-most-k constraints.
    * @param rhs the new upperBound
    */
   public void newLowerBoundForSolver(int rhs) {

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

@@ -36,7 +36,7 @@
  * In theory one could use the {@link LNGVector} also for doubles.  But Java's auto-boxing comes with such a large
  * performance penalty that for the mission critical data structures of the SAT solvers we use this specialized
  * implementation.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
 public final class LNGDoubleVector {
@@ -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

@@ -103,10 +103,8 @@ public void remove() {
     for (final int c : coefficients) {
       if (c > maxWeight)
         maxWeight = c;
-      if (c != 1) {
+      if (c != 1)
         cc = false;
-        break;
-      }
     }
     for (final Literal lit : literals)
       if (!lit.phase()) {
@@ -215,7 +213,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

@@ -46,7 +46,7 @@
 
 /**
  * A dot file writer for a formula.  Writes the internal data structure of the formula to a dot file.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
 public final class FormulaDotFileWriter {
@@ -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

@@ -41,7 +41,7 @@
 
 /**
  * A SAT solver based SAT predicate.  Indicates whether a formula is satisfiable or not.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
 public final class SATPredicate implements FormulaPredicate {
@@ -70,14 +70,13 @@ public boolean test(final Formula formula, boolean cache) {
     final Tristate cached = formula.predicateCacheEntry(IS_SAT);
     if (cached != Tristate.UNDEF)
       return cached == Tristate.TRUE;
-    final FormulaFactory factory = formula.factory();
     boolean result;
     if (formula.type() == FType.FALSE)
       result = false;
     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

@@ -37,21 +37,21 @@
 
 /**
  * A proposition in LogicNG.  A proposition is a collection of formulas with an additional textual description.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
 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/solvers/SATSolver.java

@@ -47,7 +47,7 @@
 
 /**
  * A generic interface for LogicNG's SAT solvers.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
 public abstract class SATSolver {
@@ -137,8 +137,14 @@ public void add(final Variable relaxationVar, final Collection<? extends Formula
 
   /**
    * Adds a cardinality constraint and returns its incremental data in order to refine the constraint on the solver.
+   *
+   * Usage constraints:
+   * - "<": Cannot be used with right hand side 2, returns null for right hand side 1, but constraint is added to solver.
+   * - "<=": Cannot be used with right hand side 1, returns null for right hand side 0, but constraint is added to solver.
+   * - ">": Returns null for right hand side 0 or number of variables -1, but constraint is added to solver. Adds false to solver for right hand side >= number of variables.
+   * - ">=": Returns null for right hand side 1 or number of variables, but constraint is added to solver. Adds false to solver for right hand side > number of variables.
    * @param cc the cardinality constraint
-   * @return the incremental data of this constraint
+   * @return the incremental data of this constraint, or null if the right hand side of cc is 1
    */
   public abstract CCIncrementalData addIncrementalCC(final PBConstraint cc);
 

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

@@ -42,7 +42,7 @@
 
 /**
  * Transformation of a formula in CNF by factorization.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
 public final class CNFFactorization implements FormulaTransformation {
@@ -100,9 +100,10 @@ public Formula apply(final Formula formula, boolean cache) {
       case AND:
         nops = new LinkedHashSet<>();
         for (final Formula op : formula) {
+          final Formula apply = this.apply(op, cache);
           if (!this.proceed)
             return null;
-          nops.add(this.apply(op, cache));
+          nops.add(apply);
         }
         cached = formula.factory().and(nops);
         break;
@@ -133,8 +134,12 @@ private Formula distribute(final Formula f1, final Formula f2) {
       final FormulaFactory f = f1.factory();
       if (f1.type() == AND || f2.type() == AND) {
         final LinkedHashSet<Formula> nops = new LinkedHashSet<>();
-        for (final Formula op : f1.type() == AND ? f1 : f2)
-          nops.add(this.distribute(op, f1.type() == AND ? f2 : f1));
+        for (final Formula op : f1.type() == AND ? f1 : f2) {
+          final Formula distribute = this.distribute(op, f1.type() == AND ? f2 : f1);
+          if (!this.proceed)
+            return null;
+          nops.add(distribute);
+        }
         return f.and(nops);
       }
       final Formula clause = f.or(f1, f2);

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

@@ -34,7 +34,6 @@
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.FormulaTransformation;
 import org.logicng.formulas.Literal;
-import org.logicng.formulas.Not;
 import org.logicng.predicates.CNFPredicate;
 
 import java.util.ArrayList;
@@ -49,7 +48,7 @@
  * <p>
  * ATTENTION: if you mix formulas from different formula factories this can lead to clashes in the naming of newly
  * introduced variables.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
 public final class PlaistedGreenbaumTransformation implements FormulaTransformation {
@@ -117,10 +116,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

@@ -42,7 +42,7 @@
 
 /**
  * Transformation of a formula in DNF by factorization.
- * @version 1.0
+ * @version 1.1
  * @since 1.0
  */
 public final class DNFFactorization implements FormulaTransformation {
@@ -86,9 +86,10 @@ public Formula apply(final Formula formula, boolean cache) {
       case OR:
         LinkedHashSet<Formula> nops = new LinkedHashSet<>();
         for (final Formula op : formula) {
+          final Formula apply = this.apply(op, cache);
           if (!this.proceed)
             return null;
-          nops.add(this.apply(op, cache));
+          nops.add(apply);
         }
         cached = formula.factory().or(nops);
         break;
@@ -131,8 +132,12 @@ private Formula distribute(final Formula f1, final Formula f2) {
       final FormulaFactory f = f1.factory();
       if (f1.type() == FType.OR || f2.type() == FType.OR) {
         final LinkedHashSet<Formula> nops = new LinkedHashSet<>();
-        for (final Formula op : f1.type() == FType.OR ? f1 : f2)
-          nops.add(this.distribute(op, f1.type() == FType.OR ? f2 : f1));
+        for (final Formula op : f1.type() == FType.OR ? f1 : f2) {
+          final Formula distribute = this.distribute(op, f1.type() == FType.OR ? f2 : f1);
+          if (!this.proceed)
+            return null;
+          nops.add(distribute);
+        }
         return f.or(nops);
       }
       final Formula clause = f.and(f1, f2);

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

@@ -63,6 +63,7 @@ public void testALK() {
     int counter = 0;
     for (final CCConfig config : this.configs) {
       f.putConfiguration(config);
+      testCC(10, 0, 1, f);
       testCC(10, 1, 1023, f);
       testCC(10, 2, 1013, f);
       testCC(10, 3, 968, f);
@@ -104,4 +105,11 @@ public void testIllegalCC1() {
       problemLits[i] = f.variable("v" + i);
     encoder.encode(f.cc(CType.GE, -1, problemLits));
   }
+
+  @Test
+  public void testToString() {
+    Assert.assertEquals("TOTALIZER", configs[0].alkEncoder.toString());
+    Assert.assertEquals("MODULAR_TOTALIZER", configs[1].alkEncoder.toString());
+    Assert.assertEquals("CARDINALITY_NETWORK", configs[2].alkEncoder.toString());
+  }
 }

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

@@ -38,6 +38,7 @@
 import org.logicng.solvers.MiniSat;
 import org.logicng.solvers.SATSolver;
 
+import java.util.Arrays;
 import java.util.List;
 
 /**
@@ -137,4 +138,16 @@ public void testIllegalCC1() {
       problemLits[i] = f.variable("v" + i);
     encoder.encode(f.cc(CType.LE, -1, problemLits));
   }
+
+  @Test
+  public void testToString() {
+    Assert.assertEquals("TOTALIZER", configs[0].amkEncoder.toString());
+    Assert.assertEquals("MODULAR_TOTALIZER", configs[1].amkEncoder.toString());
+    Assert.assertEquals("CARDINALITY_NETWORK", configs[2].amkEncoder.toString());
+  }
+
+  @Test
+  public void testCCSorting() {
+    Assert.assertTrue(Arrays.asList(CCSorting.ImplicationDirection.values()).contains(CCSorting.ImplicationDirection.valueOf("INPUT_TO_OUTPUT")));
+  }
 }