minor refactoring; more unit tests

src/main/java/org/logicng/LogicNGVersion.java

@@ -6,8 +6,7 @@
  * @version 2.0.0
  * @since 2.0.0
  */
-
-public class LogicNGVersion {
+public interface LogicNGVersion {
 
     /**
      * Returns the version string from the POM.

src/main/java/org/logicng/algorithms/SetCover.java

@@ -24,7 +24,14 @@
  * @version 2.0.0
  * @since 2.0.0
  */
-public class SetCover {
+public final class SetCover {
+
+    /**
+     * Private empty constructor.  Class only contains static utility methods.
+     */
+    private SetCover() {
+        // Intentionally left empty
+    }
 
     /**
      * Computes the minimum set cover for the given collection of sets,

src/main/java/org/logicng/algorithms/SmusComputation.java

@@ -30,10 +30,17 @@
  * @version 2.0.0
  * @since 2.0.0
  */
-public class SmusComputation {
+public final class SmusComputation {
 
     private static final String PROPOSITION_SELECTOR = "@PROPOSITION_SEL_";
 
+    /**
+     * Private empty constructor.  Class only contains static utility methods.
+     */
+    private SmusComputation() {
+        // Intentionally left empty
+    }
+
     /**
      * TODO: Adjust input and output?
      * Computes the SMUS for the given list of propositions modulo some additional constraint.

src/main/java/org/logicng/explanations/unsatcores/UNSATCore.java

@@ -39,7 +39,7 @@
  * @version 1.3
  * @since 1.1
  */
-final public class UNSATCore<T extends Proposition> {
+public final class UNSATCore<T extends Proposition> {
 
     private final List<T> propositions;
     private final boolean isMUS;

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

@@ -28,6 +28,9 @@
 
 package org.logicng.formulas;
 
+import static org.logicng.formulas.FType.dual;
+import static org.logicng.formulas.cache.TransformationCacheEntry.NNF;
+
 import org.logicng.datastructures.Assignment;
 import org.logicng.datastructures.Substitution;
 
@@ -38,9 +41,6 @@
 import java.util.SortedSet;
 import java.util.stream.Stream;
 
-import static org.logicng.formulas.FType.dual;
-import static org.logicng.formulas.cache.TransformationCacheEntry.NNF;
-
 /**
  * Boolean negation.
  * @version 2.0.0
@@ -171,7 +171,7 @@ public Formula nnf() {
                     nnf = this.operand.negate().nnf();
                     break;
                 default:
-                    nnf = this;
+                    throw new IllegalStateException("Did not expect formula of type: " + this.operand.type());
             }
             this.transformationCache.put(NNF, nnf);
         }

src/main/java/org/logicng/functions/FormulaDepthFunction.java

@@ -11,7 +11,8 @@
  * @version 2.0
  * @since 2.0
  */
-public class FormulaDepthFunction implements FormulaFunction<Integer> {
+public final class FormulaDepthFunction implements FormulaFunction<Integer> {
+
     @Override
     public Integer apply(final Formula formula, final boolean cache) {
         final Object cached = formula.functionCacheEntry(DEPTH);

src/main/java/org/logicng/functions/MinimumPrimeImplicantFunction.java

@@ -23,7 +23,7 @@
  * @version 2.0.0
  * @since 2.0.0
  */
-public class MinimumPrimeImplicantFunction implements FormulaFunction<SortedSet<Literal>> {
+public final class MinimumPrimeImplicantFunction implements FormulaFunction<SortedSet<Literal>> {
 
     private static final String POS = "_POS";
     private static final String NEG = "_NEG";

src/main/java/org/logicng/predicates/ContainsPBCPredicate.java

@@ -10,7 +10,7 @@
  * @version 2.0.0
  * @since 2.0.0
  */
-public class ContainsPBCPredicate implements FormulaPredicate {
+public final class ContainsPBCPredicate implements FormulaPredicate {
 
     private final static ContainsPBCPredicate INSTANCE = new ContainsPBCPredicate();
 

src/main/java/org/logicng/predicates/EvaluatesToConstantPredicate.java

@@ -40,7 +40,7 @@
  * @version 2.0.0
  * @since 2.0.0
  */
-final public class EvaluatesToConstantPredicate implements FormulaPredicate {
+public final class EvaluatesToConstantPredicate implements FormulaPredicate {
 
     private final boolean evaluatesToTrue;
     private final Map<Variable, Boolean> mapping;

src/main/java/org/logicng/transformations/Anonymizer.java

@@ -12,7 +12,7 @@
  * @version 1.4.0
  * @since 1.4.0
  */
-public class Anonymizer implements FormulaTransformation {
+public final class Anonymizer implements FormulaTransformation {
 
     private final Substitution substitution;
     private final String prefix;

src/main/java/org/logicng/transformations/BackboneSimplifier.java

@@ -44,7 +44,8 @@
  * @version 1.5.0
  * @since 1.5.0
  */
-public class BackboneSimplifier implements FormulaTransformation {
+public final class BackboneSimplifier implements FormulaTransformation {
+
     @Override
     public Formula apply(final Formula formula, final boolean cache) {
         final SATSolver solver = MiniSat.miniSat(formula.factory());

src/main/java/org/logicng/transformations/DistributiveSimplifier.java

@@ -28,6 +28,8 @@
 
 package org.logicng.transformations;
 
+import static org.logicng.formulas.FType.dual;
+
 import org.logicng.formulas.Equivalence;
 import org.logicng.formulas.FType;
 import org.logicng.formulas.Formula;
@@ -42,14 +44,12 @@
 import java.util.Map;
 import java.util.Set;
 
-import static org.logicng.formulas.FType.dual;
-
 /**
  * A formula transformation which performs simplifications by applying the distributive laws.
  * @version 2.0.0
  * @since 1.3
  */
-public class DistributiveSimplifier implements FormulaTransformation {
+public final class DistributiveSimplifier implements FormulaTransformation {
 
     @Override
     public Formula apply(final Formula formula, final boolean cache) {

src/main/java/org/logicng/transformations/LiteralSubstitution.java

@@ -23,7 +23,7 @@
  * @version 2.0.0
  * @since 2.0.0
  */
-public class LiteralSubstitution implements FormulaTransformation {
+public final class LiteralSubstitution implements FormulaTransformation {
 
     private final Map<Literal, Literal> substitution;
 

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

@@ -48,7 +48,7 @@
  * @version 2.0.0
  * @since 1.5.0
  */
-public class CNFSubsumption extends Subsumption implements FormulaTransformation {
+public final class CNFSubsumption extends Subsumption implements FormulaTransformation {
 
     @Override
     public Formula apply(final Formula formula, final boolean cache) {

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

@@ -48,7 +48,7 @@
  * @version 2.0.0
  * @since 1.5.0
  */
-public class DNFSubsumption extends Subsumption implements FormulaTransformation {
+public final class DNFSubsumption extends Subsumption implements FormulaTransformation {
 
     @Override
     public Formula apply(final Formula formula, final boolean cache) {

src/test/java/org/logicng/datastructures/ubtrees/UBNodeTest.java

@@ -0,0 +1,62 @@
+package org.logicng.datastructures.ubtrees;
+
+import static org.assertj.core.api.Assertions.assertThat;
+
+import org.junit.jupiter.api.Test;
+import org.logicng.algorithms.primecomputation.PrimeResult;
+import org.logicng.formulas.F;
+import org.logicng.formulas.Literal;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
+import java.util.SortedSet;
+import java.util.TreeSet;
+
+/**
+ * Unit Tests for the class {@link UBNode}.
+ * @version 2.0.0
+ * @since 2.0.0
+ */
+public class UBNodeTest {
+
+    private final UBNode<Integer> node1;
+    private final UBNode<String> node2;
+
+    public UBNodeTest() {
+        this.node1 = new UBNode<>(1);
+        this.node2 = new UBNode<>("String");
+    }
+
+    @Test
+    public void testHashCode() {
+        assertThat(this.node1.hashCode()).isEqualTo(this.node1.hashCode());
+        assertThat(this.node1.hashCode()).isEqualTo(new UBNode<>(1).hashCode());
+    }
+
+    @Test
+    public void testEquals() {
+        assertThat(this.node1.hashCode()).isEqualTo(this.node1.hashCode());
+        final List<SortedSet<Literal>> primeImplicants = new ArrayList<>();
+        primeImplicants.add(new TreeSet<>(Arrays.asList(F.A, F.NB)));
+        primeImplicants.add(new TreeSet<>(Arrays.asList(F.A, F.C)));
+        final List<SortedSet<Literal>> primeImplicates = new ArrayList<>();
+        primeImplicates.add(new TreeSet<>(Arrays.asList(F.A, F.NB)));
+        final PrimeResult otherResult = new PrimeResult(primeImplicants, primeImplicates, PrimeResult.CoverageType.IMPLICANTS_COMPLETE);
+        assertThat(this.node1.equals(this.node1)).isTrue();
+        assertThat(this.node1.equals(new UBNode<>(1))).isTrue();
+        assertThat(this.node1.equals(this.node2)).isFalse();
+        assertThat(this.node2.equals(this.node1)).isFalse();
+        assertThat(this.node1.equals(null)).isFalse();
+    }
+
+    @Test
+    public void testToString() {
+        assertThat(this.node1.toString()).isEqualTo(
+                "UBNode{" +
+                        "element=1" +
+                        ", children={}" +
+                        ", set=null" +
+                        '}');
+    }
+}

src/test/java/org/logicng/explanations/unsatcores/UNSATCoreTest.java

@@ -63,6 +63,7 @@ public void testEquals() {
         assertThat(new UNSATCore<>(this.props1, false)).isNotEqualTo(this.core1);
         assertThat(new UNSATCore<>(this.props2, true)).isNotEqualTo(this.core1);
         assertThat("String").isNotEqualTo(this.core1);
+        assertThat(this.core1).isNotEqualTo("String");
     }
 
     @Test

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

@@ -123,6 +123,7 @@ public void testEquals() {
         assertThat(F.f.implication(F.AND1, F.OR1)).isEqualTo(F.IMP3);
         assertThat(F.IMP2).isEqualTo(F.IMP2);
         assertThat(F.IMP2).isNotEqualTo(F.IMP1);
+        assertThat(F.IMP2).isNotEqualTo("String");
     }
 
     @Test

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

@@ -101,6 +101,7 @@ public void testEquals() {
         assertThat(F.f.not(F.OR1)).isEqualTo(F.NOT2);
         assertThat(F.NOT1).isEqualTo(F.NOT1);
         assertThat(F.NOT2).isNotEqualTo(F.NOT1);
+        assertThat(F.NOT2).isNotEqualTo("String");
     }
 
     @Test
@@ -120,6 +121,7 @@ public void testHash() {
 
     @Test
     public void testNumberOfAtoms() {
+        assertThat(F.NOT1.numberOfAtoms()).isEqualTo(2);
         assertThat(F.NOT1.numberOfAtoms()).isEqualTo(2);
         assertThat(F.NOT2.numberOfAtoms()).isEqualTo(2);
         assertThat(F.OR1.numberOfAtoms()).isEqualTo(2);

src/test/java/org/logicng/functions/MinimumPrimeImplicantTest.java

@@ -1,5 +1,7 @@
 package org.logicng.functions;
 
+import static org.assertj.core.api.Assertions.assertThat;
+
 import org.junit.jupiter.api.Test;
 import org.logicng.cardinalityconstraints.CCConfig;
 import org.logicng.formulas.Formula;
@@ -13,8 +15,6 @@
 import java.util.SortedSet;
 import java.util.TreeSet;
 
-import static org.assertj.core.api.Assertions.assertThat;
-
 /**
  * Unit Tests for the class {@link MinimumPrimeImplicantFunction}.
  * @version 2.0.0
@@ -40,6 +40,10 @@ public void testSimpleCases() throws ParserException {
         assertThat(pi).hasSize(1);
         isPrimeImplicant(formula, pi);
 
+        formula = this.f.parse("a & b & (~a|~b)");
+        pi = formula.apply(MinimumPrimeImplicantFunction.get());
+        assertThat(pi).isNull();
+
         formula = this.f.parse("a & b & c");
         pi = formula.apply(MinimumPrimeImplicantFunction.get());
         assertThat(pi).hasSize(3);