Merge remote-tracking branch 'origin/testCoverage' into release_1.1

logic-ng · Aug 28, 2016 · 40fd643 · 40fd643
2 parents be9a0bb + 68ee711
commit 40fd643
Show file tree

Hide file tree

Showing 21 changed files with 391 additions and 50 deletions.
diff --git a/README.md b/README.md
@@ -1,4 +1,4 @@
-[![wercker status](https://app.wercker.com/status/24c4765f3a0d79520ad80a1e4c20cfa2/s/master "wercker status")](https://app.wercker.com/project/bykey/24c4765f3a0d79520ad80a1e4c20cfa2) [![Coverage Status](https://coveralls.io/repos/logic-ng/LogicNG/badge.svg?branch=master&service=github)](https://coveralls.io/github/logic-ng/LogicNG?branch=master) ![License](https://img.shields.io/badge/license-Apache%202-blue.svg) ![Version](https://img.shields.io/badge/version-1.0.2-ff69b4.svg)
+[![wercker status](https://app.wercker.com/status/24c4765f3a0d79520ad80a1e4c20cfa2/s/master "wercker status")](https://app.wercker.com/project/bykey/24c4765f3a0d79520ad80a1e4c20cfa2) [![Coverage Status](https://coveralls.io/repos/logic-ng/LogicNG/badge.svg?branch=master&service=github)](https://coveralls.io/github/logic-ng/LogicNG?branch=master) ![License](https://img.shields.io/badge/license-Apache%202-blue.svg) ![Version](https://img.shields.io/badge/version-1.1-ff69b4.svg)
 
 <img src="https://github.com/logic-ng/LogicNG/blob/master/doc/logo/logo_big.png" alt="logo" width="300">
 

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCIncrementalData.java b/src/main/java/org/logicng/cardinalityconstraints/CCIncrementalData.java
@@ -149,8 +149,8 @@ public final class CCIncrementalData {
    */
   public List<Formula> newUpperBound(int rhs) {
     this.result.reset();
-    computeUBConstraint(result, rhs);
-    return result.result();
+    this.computeUBConstraint(this.result, rhs);
+    return this.result.result();
   }
 
   /**
@@ -162,7 +162,7 @@ public List<Formula> newUpperBound(int rhs) {
    * @param rhs the new upperBound
    */
   public void newUpperBoundForSolver(int rhs) {
-    computeUBConstraint(result, rhs);
+    this.computeUBConstraint(this.result, rhs);
   }
 
   private void computeUBConstraint(final EncodingResult result, int rhs) {
@@ -212,8 +212,8 @@ private void computeUBConstraint(final EncodingResult result, int rhs) {
    */
   public List<Formula> newLowerBound(int rhs) {
     this.result.reset();
-    computeLBConstraint(result, rhs);
-    return result.result();
+    this.computeLBConstraint(this.result, rhs);
+    return this.result.result();
   }
 
   /**
@@ -225,7 +225,7 @@ public List<Formula> newLowerBound(int rhs) {
    * @param rhs the new upperBound
    */
   public void newLowerBoundForSolver(int rhs) {
-    computeLBConstraint(result, rhs);
+    this.computeLBConstraint(this.result, rhs);
   }
 
   private void computeLBConstraint(final EncodingResult result, int rhs) {
@@ -240,7 +240,7 @@ private void computeLBConstraint(final EncodingResult result, int rhs) {
           result.addClause(this.vector1.get(i));
         break;
       case MODULAR_TOTALIZER:
-        int newRHS = nVars - rhs;
+        int newRHS = this.nVars - rhs;
         assert this.vector1.size() != 0 || this.vector2.size() != 0;
         int ulimit = (newRHS + 1) / this.mod;
         int llimit = (newRHS + 1) - ulimit * this.mod;
@@ -261,7 +261,7 @@ private void computeLBConstraint(final EncodingResult result, int rhs) {
         }
         break;
       case CARDINALITY_NETWORK:
-        newRHS = nVars - rhs;
+        newRHS = this.nVars - rhs;
         if (this.vector1.size() > newRHS)
           result.addClause(this.vector1.get(newRHS).negate());
         break;
@@ -270,15 +270,23 @@ private void computeLBConstraint(final EncodingResult result, int rhs) {
     }
   }
 
+  /**
+   * Returns the current right hand side of this CCIncrementalData.
+   * @return the current right hand side of this CCIncrementalData.
+   */
+  public int currentRHS() {
+    return this.currentRHS;
+  }
+
   @Override
   public String toString() {
     return "CCIncrementalData{" +
-            ", amkEncoder=" + amkEncoder +
-            ", alkEncoder=" + alkEncoder +
-            ", vector1=" + vector1 +
-            ", vector2=" + vector2 +
-            ", mod=" + mod +
-            ", currentRHS=" + currentRHS +
+            ", amkEncoder=" + this.amkEncoder +
+            ", alkEncoder=" + this.alkEncoder +
+            ", vector1=" + this.vector1 +
+            ", vector2=" + this.vector2 +
+            ", mod=" + this.mod +
+            ", currentRHS=" + this.currentRHS +
             '}';
   }
 }
diff --git a/src/main/java/org/logicng/solvers/SolverState.java b/src/main/java/org/logicng/solvers/SolverState.java
@@ -32,7 +32,7 @@
 
 /**
  * A wrapper class for the internal solver state.
- * @version 1.0.1
+ * @version 1.1
  * @since 1.0
  */
 public final class SolverState {
@@ -41,16 +41,6 @@ public final class SolverState {
 
   private final int[] state;
 
-  /**
-   * Creates a new solver state with a given internal solver state and id -1.
-   * @param state the internal solver state
-   * @deprecated use with explicit id
-   */
-  @Deprecated
-  public SolverState(final int[] state) {
-    this(-1, state);
-  }
-
   /**
    * Creates a new solver state with a given id and internal solver data.
    * @param id    the id

diff --git a/src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java b/src/main/java/org/logicng/solvers/maxsat/algorithms/MaxSAT.java
@@ -441,11 +441,6 @@ protected boolean foundUpperBound(final int upperBound, final Assignment model)
     return handler == null || handler.foundUpperBound(upperBound, model);
   }
 
-  @Override
-  public String toString() {
-    return this.getClass().getSimpleName();
-  }
-
   /**
    * The MaxSAT solver statistics.
    */

diff --git a/src/main/java/org/logicng/solvers/maxsat/encodings/Encoding.java b/src/main/java/org/logicng/solvers/maxsat/encodings/Encoding.java
@@ -180,7 +180,7 @@ void addQuaternaryClause(final MiniSatStyleSolver s, int a, int b, int c, int d)
    * @param d        the fourth literal
    * @param blocking the blocking literal
    */
-  void addQuaternaryClause(final MiniSatStyleSolver s, int a, int b, int c, int d, int blocking) {
+  private void addQuaternaryClause(final MiniSatStyleSolver s, int a, int b, int c, int d, int blocking) {
     assert this.clause.size() == 0;
     assert a != LIT_UNDEF && b != LIT_UNDEF && c != LIT_UNDEF && d != LIT_UNDEF;
     assert var(a) < s.nVars() && var(b) < s.nVars() && var(c) < s.nVars() && var(d) < s.nVars();
@@ -193,9 +193,4 @@ void addQuaternaryClause(final MiniSatStyleSolver s, int a, int b, int c, int d,
     s.addClause(this.clause);
     this.clause.clear();
   }
-
-  @Override
-  public String toString() {
-    return this.getClass().getSimpleName();
-  }
 }
diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java
@@ -39,6 +39,7 @@
 import org.logicng.solvers.MiniSat;
 import org.logicng.solvers.SATSolver;
 
+import java.util.Arrays;
 import java.util.List;
 
 /**
@@ -108,8 +109,19 @@ public void testIllegalCC1() {
 
   @Test
   public void testToString() {
+    FormulaFactory f = new FormulaFactory();
     Assert.assertEquals("TOTALIZER", configs[0].alkEncoder.toString());
     Assert.assertEquals("MODULAR_TOTALIZER", configs[1].alkEncoder.toString());
     Assert.assertEquals("CARDINALITY_NETWORK", configs[2].alkEncoder.toString());
+
+    Assert.assertEquals("CCTotalizer", new CCTotalizer().toString());
+    Assert.assertEquals("CCModularTotalizer", new CCModularTotalizer(f).toString());
+    Assert.assertEquals("CCCardinalityNetworks", new CCCardinalityNetworks().toString());
+
+    Assert.assertEquals("CCALKTotalizer", new CCALKTotalizer().toString());
+    Assert.assertEquals("CCALKModularTotalizer", new CCALKModularTotalizer(f).toString());
+    Assert.assertEquals("CCALKCardinalityNetwork", new CCALKCardinalityNetwork().toString());
+
+    Assert.assertTrue(Arrays.asList(CCConfig.ALK_ENCODER.values()).contains(CCConfig.ALK_ENCODER.valueOf("MODULAR_TOTALIZER")));
   }
 }
diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java
@@ -141,9 +141,16 @@ public void testIllegalCC1() {
 
   @Test
   public void testToString() {
+    FormulaFactory f = new FormulaFactory();
     Assert.assertEquals("TOTALIZER", configs[0].amkEncoder.toString());
     Assert.assertEquals("MODULAR_TOTALIZER", configs[1].amkEncoder.toString());
     Assert.assertEquals("CARDINALITY_NETWORK", configs[2].amkEncoder.toString());
+
+    Assert.assertEquals("CCAMKTotalizer", new CCAMKTotalizer().toString());
+    Assert.assertEquals("CCAMKModularTotalizer", new CCAMKModularTotalizer(f).toString());
+    Assert.assertEquals("CCAMKCardinalityNetwork", new CCAMKCardinalityNetwork().toString());
+
+    Assert.assertTrue(Arrays.asList(CCConfig.AMK_ENCODER.values()).contains(CCConfig.AMK_ENCODER.valueOf("TOTALIZER")));
   }
 
   @Test

diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java
@@ -38,6 +38,7 @@
 import org.logicng.solvers.MiniSat;
 import org.logicng.solvers.SATSolver;
 
+import java.util.Arrays;
 import java.util.List;
 
 import static org.logicng.cardinalityconstraints.CCConfig.AMO_ENCODER.BEST;
@@ -134,6 +135,17 @@ public void testToString() {
     Assert.assertEquals("COMMANDER", configs[5].amoEncoder.toString());
     Assert.assertEquals("BIMANDER", configs[7].amoEncoder.toString());
     Assert.assertEquals("BEST", configs[13].amoEncoder.toString());
+
+    Assert.assertEquals("CCAMOPure", new CCAMOPure().toString());
+    Assert.assertEquals("CCAMOLadder", new CCAMOLadder().toString());
+    Assert.assertEquals("CCAMOProduct", new CCAMOProduct(2).toString());
+    Assert.assertEquals("CCAMOBinary", new CCAMOBinary().toString());
+    Assert.assertEquals("CCAMONested", new CCAMONested(2).toString());
+    Assert.assertEquals("CCAMOCommander", new CCAMOCommander(2).toString());
+    Assert.assertEquals("CCAMOBimander", new CCAMOBimander(2).toString());
+
+    Assert.assertTrue(Arrays.asList(CCConfig.AMO_ENCODER.values()).contains(CCConfig.AMO_ENCODER.valueOf("LADDER")));
+    Assert.assertTrue(Arrays.asList(CCConfig.BIMANDER_GROUP_SIZE.values()).contains(CCConfig.BIMANDER_GROUP_SIZE.valueOf("SQRT")));
   }
 
   private void testAMO(int numLits, final FormulaFactory f, boolean miniCard) {

diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCEXKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCEXKTest.java
@@ -31,13 +31,15 @@
 import org.junit.Assert;
 import org.junit.Test;
 import org.logicng.datastructures.Assignment;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.datastructures.Tristate;
 import org.logicng.formulas.CType;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Variable;
 import org.logicng.solvers.MiniSat;
 import org.logicng.solvers.SATSolver;
 
+import java.util.Arrays;
 import java.util.List;
 
 /**
@@ -103,9 +105,25 @@ public void testIllegalCC1() {
     encoder.encode(f.cc(CType.EQ, -1, problemLits));
   }
 
+  @Test
+  public void testCCEXKTotalizer() {
+    FormulaFactory f = new FormulaFactory();
+    CCEXKTotalizer totalizer = new CCEXKTotalizer();
+    totalizer.build(EncodingResult.resultForFormula(f), new Variable[]{f.variable("A"), f.variable("B"), f.variable("C")}, 2);
+    Assert.assertNull(totalizer.incrementalData());
+    Assert.assertEquals("CCEXKTotalizer", totalizer.toString());
+
+    CCEXKCardinalityNetwork cNetwork = new CCEXKCardinalityNetwork();
+    cNetwork.build(EncodingResult.resultForFormula(f), new Variable[]{f.variable("A"), f.variable("B"), f.variable("C")}, 2);
+    Assert.assertNull(cNetwork.incrementalData());
+    Assert.assertEquals("CCEXKCardinalityNetwork", cNetwork.toString());
+  }
+
   @Test
   public void testToString() {
     Assert.assertEquals("TOTALIZER", configs[0].exkEncoder.toString());
     Assert.assertEquals("CARDINALITY_NETWORK", configs[1].exkEncoder.toString());
+
+    Assert.assertTrue(Arrays.asList(CCConfig.EXK_ENCODER.values()).contains(CCConfig.EXK_ENCODER.valueOf("CARDINALITY_NETWORK")));
   }
 }
diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalFormulaTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalFormulaTest.java
@@ -86,6 +86,7 @@ public void testSimpleIncrementalAMK() {
       Assert.assertEquals(Tristate.TRUE, solver.sat()); // <= 9
       solver.add(incData.newUpperBound(8)); // <= 8
       Assert.assertEquals(Tristate.TRUE, solver.sat());
+      Assert.assertEquals(8, incData.currentRHS());
       solver.add(incData.newUpperBound(7)); // <= 7
       Assert.assertEquals(Tristate.TRUE, solver.sat());
       solver.add(incData.newUpperBound(6)); // <= 6

diff --git a/src/test/java/org/logicng/explanations/unsatcores/MUSConfigTest.java b/src/test/java/org/logicng/explanations/unsatcores/MUSConfigTest.java
@@ -43,9 +43,8 @@ public class MUSConfigTest {
 
   @Test
   public void testMUSConfiguration() {
-    final MUSConfig config = new MUSConfig.Builder().algorithm(MUSConfig.Algorithm.DELETION).build();
+    final MUSConfig config = new MUSConfig.Builder().algorithm(MUSConfig.Algorithm.valueOf("DELETION")).build();
     Assert.assertEquals("MUSConfig{\nalgorithm=DELETION\n}\n", config.toString());
     Assert.assertTrue(Arrays.asList(CNFConfig.Algorithm.values()).contains(CNFConfig.Algorithm.valueOf("TSEITIN")));
   }
-
 }
diff --git a/src/test/java/org/logicng/solvers/datastructures/LNGHeapTest.java b/src/test/java/org/logicng/solvers/datastructures/LNGHeapTest.java
@@ -43,12 +43,17 @@ public class LNGHeapTest {
   @Test
   public void test() {
     MiniSatStyleSolver solver = new MiniCard();
+    solver.newVar(true, true);
+    solver.newVar(true, true);
+    solver.newVar(true, true);
     LNGHeap heap = new LNGHeap(solver);
     Assert.assertTrue(heap.empty());
-    heap.insert(5);
-    Assert.assertEquals(5, heap.get(0));
-    Assert.assertTrue(heap.toString().contains("5"));
-    Assert.assertEquals(1, heap.size());
+    heap.insert(1);
+    heap.insert(2);
+    heap.insert(0);
+    Assert.assertEquals(1, heap.get(0));
+    Assert.assertEquals("LNGHeap{[1, 2], [2, 0], [0, 1]}", heap.toString());
+    Assert.assertEquals(3, heap.size());
     heap.clear();
     Assert.assertTrue(heap.empty());
   }

diff --git a/src/test/java/org/logicng/solvers/maxsat/MaxSATClassTest.java b/src/test/java/org/logicng/solvers/maxsat/MaxSATClassTest.java
@@ -0,0 +1,83 @@
+///////////////////////////////////////////////////////////////////////////
+//                   __                _      _   ________               //
+//                  / /   ____  ____ _(_)____/ | / / ____/               //
+//                 / /   / __ \/ __ `/ / ___/  |/ / / __                 //
+//                / /___/ /_/ / /_/ / / /__/ /|  / /_/ /                 //
+//               /_____/\____/\__, /_/\___/_/ |_/\____/                  //
+//                           /____/                                      //
+//                                                                       //
+//               The Next Generation Logic Library                       //
+//                                                                       //
+///////////////////////////////////////////////////////////////////////////
+//                                                                       //
+//  Copyright 2015-2016 Christoph Zengler                                //
+//                                                                       //
+//  Licensed under the Apache License, Version 2.0 (the "License");      //
+//  you may not use this file except in compliance with the License.     //
+//  You may obtain a copy of the License at                              //
+//                                                                       //
+//  http://www.apache.org/licenses/LICENSE-2.0                           //
+//                                                                       //
+//  Unless required by applicable law or agreed to in writing, software  //
+//  distributed under the License is distributed on an "AS IS" BASIS,    //
+//  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or      //
+//  implied.  See the License for the specific language governing        //
+//  permissions and limitations under the License.                       //
+//                                                                       //
+///////////////////////////////////////////////////////////////////////////
+
+package org.logicng.solvers.maxsat;
+
+import org.junit.Assert;
+import org.junit.Test;
+import org.logicng.solvers.maxsat.algorithms.IncWBO;
+import org.logicng.solvers.maxsat.algorithms.LinearSU;
+import org.logicng.solvers.maxsat.algorithms.LinearUS;
+import org.logicng.solvers.maxsat.algorithms.MSU3;
+import org.logicng.solvers.maxsat.algorithms.MaxSAT;
+import org.logicng.solvers.maxsat.algorithms.MaxSATConfig;
+import org.logicng.solvers.maxsat.algorithms.WBO;
+import org.logicng.solvers.maxsat.algorithms.WMSU3;
+
+import java.util.Arrays;
+
+/**
+ * Unit tests for the package {@link org.logicng.solvers.maxsat}.
+ * @version 1.1
+ * @since 1.1
+ */
+public class MaxSATClassTest {
+
+  @Test
+  public void testMaxSATConfig() {
+    Assert.assertTrue(Arrays.asList(MaxSATConfig.SolverType.values()).contains(MaxSATConfig.SolverType.valueOf("GLUCOSE")));
+    Assert.assertTrue(Arrays.asList(MaxSATConfig.IncrementalStrategy.values()).contains(MaxSATConfig.IncrementalStrategy.valueOf("ITERATIVE")));
+    Assert.assertTrue(Arrays.asList(MaxSATConfig.AMOEncoding.values()).contains(MaxSATConfig.AMOEncoding.valueOf("LADDER")));
+    Assert.assertTrue(Arrays.asList(MaxSATConfig.PBEncoding.values()).contains(MaxSATConfig.PBEncoding.valueOf("SWC")));
+    Assert.assertTrue(Arrays.asList(MaxSATConfig.CardinalityEncoding.values()).contains(MaxSATConfig.CardinalityEncoding.valueOf("TOTALIZER")));
+    Assert.assertTrue(Arrays.asList(MaxSATConfig.WeightStrategy.values()).contains(MaxSATConfig.WeightStrategy.valueOf("DIVERSIFY")));
+    Assert.assertTrue(Arrays.asList(MaxSATConfig.Verbosity.values()).contains(MaxSATConfig.Verbosity.valueOf("SOME")));
+  }
+
+  @Test
+  public void testMaxSATenum() {
+    Assert.assertTrue(Arrays.asList(MaxSAT.ProblemType.values()).contains(MaxSAT.ProblemType.valueOf("UNWEIGHTED")));
+    Assert.assertTrue(Arrays.asList(MaxSAT.MaxSATResult.values()).contains(MaxSAT.MaxSATResult.valueOf("OPTIMUM")));
+  }
+
+  @Test
+  public void testMaxSATtoString() {
+    MaxSAT wmsu3 = new WMSU3();
+    Assert.assertEquals("WMSU3", wmsu3.toString());
+    MaxSAT wbo = new WBO();
+    Assert.assertEquals("WBO", wbo.toString());
+    MaxSAT incWbo = new IncWBO();
+    Assert.assertEquals("IncWBO", incWbo.toString());
+    MaxSAT msu3 = new MSU3();
+    Assert.assertEquals("MSU3", msu3.toString());
+    MaxSAT linearSu = new LinearSU();
+    Assert.assertEquals("LinearSU", linearSu.toString());
+    MaxSAT linearUs = new LinearUS();
+    Assert.assertEquals("LinearUS", linearUs.toString());
+  }
+}