Added more test coverage.

src/test/java/org/logicng/datastructures/AssignmentTest.java

@@ -31,12 +31,16 @@
 import org.junit.Assert;
 import org.junit.Test;
 import org.logicng.formulas.F;
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Literal;
 import org.logicng.io.parsers.ParserException;
 import org.logicng.io.parsers.PropositionalParser;
 
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Collections;
+import java.util.List;
 
 /**
  * Unit tests for the class {@link Assignment}.
@@ -155,6 +159,8 @@ public void testFastEvaluable() {
     Assert.assertEquals(F.f.and(F.A, F.NX, F.NB, F.Y), ass.formula(F.f));
     ass = new Assignment(Arrays.asList(F.A, F.NX), true);
     Assert.assertTrue(ass.fastEvaluable());
+    ass.convertToFastEvaluable();
+    Assert.assertTrue(ass.fastEvaluable());
   }
 
   @Test
@@ -189,6 +195,22 @@ public void testEquals() {
     Assert.assertNotEquals(ass, F.TRUE);
   }
 
+  @Test
+  public void testBlockingClause(){
+    Assignment ass = new Assignment();
+    ass.addLiteral(F.A);
+    ass.addLiteral(F.B);
+    ass.addLiteral(F.NX);
+    ass.addLiteral(F.NY);
+    List<Literal> lits = new ArrayList<>();
+    lits.add(F.A);
+    lits.add(F.X);
+    lits.add(F.C);
+    Formula bc = ass.blockingClause(F.f, lits);
+    Assert.assertTrue(!bc.containsVariable(F.C));
+    Assert.assertEquals("~a | x",bc.toString());
+  }
+
   @Test
   public void testToString() {
     Assert.assertEquals("Assignment{pos=[], neg=[]}", new Assignment().toString());

src/test/java/org/logicng/solvers/datastructures/LNGHeapTest.java

@@ -0,0 +1,27 @@
+package org.logicng.solvers.datastructures;
+
+import org.junit.Assert;
+import org.junit.Test;
+import org.logicng.collections.LNGIntVector;
+import org.logicng.formulas.FormulaFactory;
+import org.logicng.solvers.MiniSat;
+import org.logicng.solvers.sat.MiniCard;
+import org.logicng.solvers.sat.MiniSatStyleSolver;
+
+/**
+ * Unit tests for the class {@link LNGHeap}.
+ */
+public class LNGHeapTest {
+
+  @Test
+  public void test(){
+    MiniSatStyleSolver solver = new MiniCard();
+    LNGHeap heap = new LNGHeap(solver);
+    Assert.assertTrue(heap.empty());
+    heap.insert(5);
+    Assert.assertTrue(heap.toString().contains("5"));
+    Assert.assertEquals(1,heap.size());
+    heap.clear();
+    Assert.assertTrue(heap.empty());
+  }
+}

src/test/java/org/logicng/solvers/datastructures/TestToStrings.java

@@ -135,6 +135,9 @@ public void testMSClause() {
     clause.setSeen(true);
     final String expected = "MSClause{activity=0.0, learnt=true, szWithoutSelectors=0, seen=true, lbd=42, canBeDel=true, oneWatched=false, isAtMost=false, atMostWatchers=-1, lits=[1, 2, 3]}";
     Assert.assertEquals(expected, clause.toString());
+    Assert.assertTrue(clause.equals(clause));
+    Assert.assertEquals(clause.hashCode(),clause.hashCode());
+    Assert.assertFalse(clause.equals("Test"));
   }
 
   @Test
@@ -180,6 +183,7 @@ public void testMSWatcher() {
     final MSWatcher watcher = new MSWatcher(clause, 2);
     final String expected = "MSWatcher{clause=MSClause{activity=0.0, learnt=true, szWithoutSelectors=0, seen=false, lbd=0, canBeDel=true, oneWatched=false, isAtMost=false, atMostWatchers=-1, lits=[1, 2, 3]}, blocker=2}";
     Assert.assertEquals(expected, watcher.toString());
+    Assert.assertEquals(watcher.hashCode(),watcher.hashCode());
   }
 
 }

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

@@ -31,6 +31,9 @@
 import org.junit.Assert;
 import org.junit.Test;
 import org.logicng.formulas.F;
+import org.logicng.formulas.Formula;
+import org.logicng.formulas.PBConstraint;
+import org.logicng.formulas.cache.TransformationCacheEntry;
 import org.logicng.io.parsers.ParserException;
 import org.logicng.io.parsers.PropositionalParser;
 import org.logicng.predicates.AIGPredicate;
@@ -80,6 +83,14 @@ public void testBinaryOperators() throws ParserException {
     Assert.assertFalse(F.IMP3.holds(aigPred));
     Assert.assertFalse(F.EQ1.holds(aigPred));
     Assert.assertFalse(F.EQ2.holds(aigPred));
+    Formula impl = p.parse("m => n");
+    impl.transform(aigTrans, false);
+    Formula aigIMPL = impl.transformationCacheEntry(TransformationCacheEntry.AIG);
+    Assert.assertNull(aigIMPL);
+    Formula equi = p.parse("m <=> n");
+    equi.transform(aigTrans, false);
+    Formula aigEQUI = impl.transformationCacheEntry(TransformationCacheEntry.AIG);
+    Assert.assertNull(aigEQUI);
   }
 
   @Test
@@ -100,6 +111,14 @@ public void testNAryOperators() throws ParserException {
     Assert.assertFalse(p.parse("~(a | b) & c & ~(x & ~y) & (w => z)").holds(aigPred));
     Assert.assertFalse(p.parse("~(a & b) | c | ~(x | ~y)").holds(aigPred));
     Assert.assertFalse(p.parse("a | b | (~x & ~y)").holds(aigPred));
+    Formula or = p.parse("m | n | o");
+    or.transform(aigTrans,false);
+    Formula aigOR = or.transformationCacheEntry(TransformationCacheEntry.AIG);
+    Assert.assertNull(aigOR);
+    Formula and = p.parse("m & n & o");
+    and.transform(aigTrans,false);
+    Formula aigAND = and.transformationCacheEntry(TransformationCacheEntry.AIG);
+    Assert.assertNull(aigAND);
   }
 
   @Test
@@ -114,5 +133,19 @@ public void testNot() throws ParserException {
     Assert.assertEquals(p.parse("~(a & b & ~x & ~y)"), p.parse("~(a & b & ~x & ~y)").transform(aigTrans));
     Assert.assertEquals(p.parse("~a & ~b & x & y"), p.parse("~(a | b | ~x | ~y)").transform(aigTrans));
     Assert.assertEquals(p.parse("~a & ~b & x & y"), p.parse("~(a | b | ~x | ~y)").transform(aigTrans)); // test caching
+    Formula not = p.parse("~(m | n)");
+    not.transform(aigTrans,false);
+    Formula aig = not.transformationCacheEntry(TransformationCacheEntry.AIG);
+    Assert.assertNull(aig);
+  }
+
+  @Test
+  public void testPBC(){
+    Assert.assertTrue(F.PBC1.transform(aigTrans).holds(aigPred));
+  }
+
+  @Test
+  public void testToString(){
+    Assert.assertEquals("AIGTransformation", aigTrans.toString());
   }
 }