diff --git a/src/main/java/org/logicng/LogicNGVersion.java b/src/main/java/org/logicng/LogicNGVersion.java index 81dc3e75..14f643ab 100644 --- a/src/main/java/org/logicng/LogicNGVersion.java +++ b/src/main/java/org/logicng/LogicNGVersion.java @@ -32,7 +32,7 @@ public static int major() { return major(version()); } - static int major(final String version) { + private static int major(final String version) { try { return Integer.parseInt(version.split("\\.")[0]); } catch (final ArrayIndexOutOfBoundsException | NumberFormatException e) { @@ -48,7 +48,7 @@ public static int minor() { return minor(version()); } - static int minor(final String version) { + private static int minor(final String version) { try { return Integer.parseInt(version.split("\\.")[1]); } catch (final ArrayIndexOutOfBoundsException | NumberFormatException e) { @@ -64,7 +64,7 @@ public static int patch() { return patch(version()); } - static int patch(final String version) { + private static int patch(final String version) { try { return Integer.parseInt(version.split("\\.")[2].split("-")[0]); } catch (final ArrayIndexOutOfBoundsException | NumberFormatException e) { @@ -80,7 +80,7 @@ public static boolean snapshot() { return snapshot(version()); } - static boolean snapshot(final String version) { + private static boolean snapshot(final String version) { return version.contains("-SNAPSHOT"); } } diff --git a/src/test/java/org/logicng/LogicNGVersionTest.java b/src/test/java/org/logicng/LogicNGVersionTest.java index d7980032..86916d88 100644 --- a/src/test/java/org/logicng/LogicNGVersionTest.java +++ b/src/test/java/org/logicng/LogicNGVersionTest.java @@ -1,9 +1,12 @@ package org.logicng; import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.fail; import org.junit.jupiter.api.Test; +import java.lang.reflect.Field; + /** * Unit tests for {@link LogicNGVersion}. * @version 2.0.0 @@ -13,42 +16,72 @@ public class LogicNGVersionTest { @Test public void testMajor() { - assertThat(LogicNGVersion.major("2.0.0")).isEqualTo(2); - assertThat(LogicNGVersion.major("2.0.0-SNAPSHOT")).isEqualTo(2); - assertThat(LogicNGVersion.major("2.1.3")).isEqualTo(2); - assertThat(LogicNGVersion.major("42.7.19")).isEqualTo(42); - assertThat(LogicNGVersion.major("0.0.0")).isEqualTo(0); + setVersion("2.0.0"); + assertThat(LogicNGVersion.major()).isEqualTo(2); + setVersion("2.0.0-SNAPSHOT"); + assertThat(LogicNGVersion.major()).isEqualTo(2); + setVersion("2.1.3"); + assertThat(LogicNGVersion.major()).isEqualTo(2); + setVersion("42.7.19"); + assertThat(LogicNGVersion.major()).isEqualTo(42); + setVersion("0.0.0"); + assertThat(LogicNGVersion.major()).isEqualTo(0); - assertThat(LogicNGVersion.major("A.0.1")).isEqualTo(-1); + setVersion("A.0.1"); + assertThat(LogicNGVersion.major()).isEqualTo(-1); } @Test public void testMinor() { - assertThat(LogicNGVersion.minor("2.0.0")).isEqualTo(0); - assertThat(LogicNGVersion.minor("2.3.0-SNAPSHOT")).isEqualTo(3); - assertThat(LogicNGVersion.minor("2.1.3")).isEqualTo(1); - assertThat(LogicNGVersion.minor("42.7.19")).isEqualTo(7); - assertThat(LogicNGVersion.minor("0.123.0")).isEqualTo(123); + setVersion("2.0.0"); + assertThat(LogicNGVersion.minor()).isEqualTo(0); + setVersion("2.3.0-SNAPSHOT"); + assertThat(LogicNGVersion.minor()).isEqualTo(3); + setVersion("2.1.3"); + assertThat(LogicNGVersion.minor()).isEqualTo(1); + setVersion("42.7.19"); + assertThat(LogicNGVersion.minor()).isEqualTo(7); + setVersion("0.123.0"); + assertThat(LogicNGVersion.minor()).isEqualTo(123); - assertThat(LogicNGVersion.minor("2.A.1")).isEqualTo(-1); + setVersion("2.A.1"); + assertThat(LogicNGVersion.minor()).isEqualTo(-1); } @Test public void testPatch() { - assertThat(LogicNGVersion.patch("2.0.3")).isEqualTo(3); - assertThat(LogicNGVersion.patch("2.3.3-SNAPSHOT")).isEqualTo(3); - assertThat(LogicNGVersion.patch("2.1.0")).isEqualTo(0); - assertThat(LogicNGVersion.patch("42.7.19")).isEqualTo(19); - assertThat(LogicNGVersion.patch("0.123.22")).isEqualTo(22); + setVersion("2.0.3"); + assertThat(LogicNGVersion.patch()).isEqualTo(3); + setVersion("2.3.3-SNAPSHOT"); + assertThat(LogicNGVersion.patch()).isEqualTo(3); + setVersion("2.1.0"); + assertThat(LogicNGVersion.patch()).isEqualTo(0); + setVersion("42.7.19"); + assertThat(LogicNGVersion.patch()).isEqualTo(19); + setVersion("0.123.22"); + assertThat(LogicNGVersion.patch()).isEqualTo(22); - assertThat(LogicNGVersion.patch("2.2.A")).isEqualTo(-1); + setVersion("2.2.A"); + assertThat(LogicNGVersion.patch()).isEqualTo(-1); } @Test public void testSnapshot() { - assertThat(LogicNGVersion.snapshot("2.0.3")).isFalse(); - assertThat(LogicNGVersion.snapshot("2.0.3-SNAPSHOT")).isTrue(); - assertThat(LogicNGVersion.snapshot("2.0.3-HUGO")).isFalse(); + setVersion("2.0.3"); + assertThat(LogicNGVersion.snapshot()).isFalse(); + setVersion("2.0.3-SNAPSHOT"); + assertThat(LogicNGVersion.snapshot()).isTrue(); + setVersion("2.0.3-HUGO"); + assertThat(LogicNGVersion.snapshot()).isFalse(); } + private void setVersion(final String version) { + try { + final Field implVersion = Package.class.getDeclaredField("implVersion"); + implVersion.setAccessible(true); + implVersion.set(LogicNGVersion.class.getPackage(), version); + } catch (final NoSuchFieldException | IllegalAccessException e) { + fail("Failed to initialize test."); + } + } } diff --git a/src/test/java/org/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java b/src/test/java/org/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java index 0bc7cf63..97969f23 100644 --- a/src/test/java/org/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java +++ b/src/test/java/org/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java @@ -29,6 +29,7 @@ package org.logicng.graphs.algorithms; import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; import org.junit.jupiter.api.Test; import org.logicng.cardinalityconstraints.CCConfig; @@ -46,6 +47,7 @@ import java.io.IOException; import java.util.ArrayList; +import java.util.Collections; import java.util.HashSet; import java.util.List; import java.util.Set; @@ -149,4 +151,13 @@ public void testFormulaSplit() throws IOException, ParserException { assertThat(split.get(2)).hasSize(3); assertThat(split.get(3)).hasSize(3); } + + @Test + public void testFormulaSplitIllegal() { + final FormulaFactory f = new FormulaFactory(); + final Graph graph = ConstraintGraphGenerator.generateFromCnf(f.variable("B")); + final Set>> ccs = Collections.singleton(Collections.singleton(graph.node(f.variable("B")))); + assertThatThrownBy(() -> ConnectedComponentsComputation.splitFormulasByComponent(Collections.singletonList(f.variable("A")), ccs)) + .isInstanceOf(IllegalArgumentException.class); + } } diff --git a/src/test/java/org/logicng/knowledgecompilation/bdds/LargeBDDTest.java b/src/test/java/org/logicng/knowledgecompilation/bdds/LargeBDDTest.java index bf32d711..96910f56 100644 --- a/src/test/java/org/logicng/knowledgecompilation/bdds/LargeBDDTest.java +++ b/src/test/java/org/logicng/knowledgecompilation/bdds/LargeBDDTest.java @@ -35,6 +35,7 @@ import org.logicng.formulas.FormulaFactory; import org.logicng.handlers.NumberOfNodesBDDHandler; import org.logicng.handlers.TimeoutBDDHandler; +import org.logicng.io.parsers.ParserException; import org.logicng.knowledgecompilation.bdds.jbuddy.BDDKernel; import org.logicng.predicates.CNFPredicate; import org.logicng.testutils.NQueensGenerator; @@ -140,4 +141,15 @@ public void testNumberOfNodesHandlerLarge() { assertThat(handler.aborted()).isTrue(); assertThat(bdd.index()).isEqualTo(BDDKernel.BDD_ABORT); } + + @Test + public void testNumberOfNodesHandler() throws ParserException { + final FormulaFactory f = new FormulaFactory(); + final Formula formula = f.parse("A <=> ~(B => C & F & G & ~H | A & D & ~E)"); + final BDDKernel kernel = new BDDKernel(f, formula.variables().size(), 10000, 10000); + final NumberOfNodesBDDHandler handler = new NumberOfNodesBDDHandler(5); + final BDD bdd = BDDFactory.build(formula, kernel, handler); + assertThat(handler.aborted()).isTrue(); + assertThat(bdd.index()).isEqualTo(BDDKernel.BDD_ABORT); + } } diff --git a/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java b/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java index 1fd1bbab..6f1d234a 100644 --- a/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java +++ b/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java @@ -83,7 +83,7 @@ public void testLargeFormulas() throws IOException { @Test public void testDnnfProperties() throws ParserException { final DNNF dnnf = new DNNFFactory().compile(this.parser.parse("a | ((b & ~c) | (c & (~d | ~a & b)) & e)")); - assertThat(dnnf.getOriginalVariables()).extracting("name").containsExactlyInAnyOrder("a", "b", "c", "d", "e"); + assertThat(dnnf.getOriginalVariables()).extracting(Variable::name).containsExactlyInAnyOrder("a", "b", "c", "d", "e"); } @Test diff --git a/src/test/java/org/logicng/predicates/CNFPredicateTest.java b/src/test/java/org/logicng/predicates/CNFPredicateTest.java index 91b1a0f9..809d9067 100644 --- a/src/test/java/org/logicng/predicates/CNFPredicateTest.java +++ b/src/test/java/org/logicng/predicates/CNFPredicateTest.java @@ -29,6 +29,8 @@ package org.logicng.predicates; import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; +import static org.logicng.formulas.cache.PredicateCacheEntry.IS_CNF; import org.junit.jupiter.api.Test; import org.logicng.TestWithExampleFormulas; @@ -61,6 +63,12 @@ public void test() { assertThat(this.f.and(this.OR1, this.EQ1).holds(this.cnfPredicate)).isFalse(); } + @Test + public void testIllegalAnd() { + this.AND1.setPredicateCacheEntry(IS_CNF, null); + assertThatThrownBy(() -> this.AND1.holds(this.cnfPredicate)).isInstanceOf(IllegalStateException.class); + } + @Test public void testToString() { assertThat(this.cnfPredicate.toString()).isEqualTo("CNFPredicate"); diff --git a/src/test/java/org/logicng/solvers/maxsat/PureMaxSATTest.java b/src/test/java/org/logicng/solvers/maxsat/PureMaxSATTest.java index 4d43dc7a..f3eccce4 100644 --- a/src/test/java/org/logicng/solvers/maxsat/PureMaxSATTest.java +++ b/src/test/java/org/logicng/solvers/maxsat/PureMaxSATTest.java @@ -40,6 +40,7 @@ import org.logicng.datastructures.Assignment; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Literal; +import org.logicng.formulas.Variable; import org.logicng.io.parsers.ParserException; import org.logicng.io.parsers.PropositionalParser; import org.logicng.solvers.MaxSATSolver; @@ -283,12 +284,11 @@ public void testAssignment() throws ParserException { assertThat(solver.solve()).isEqualTo(OPTIMUM); assertThat(solver.result()).isEqualTo(3); final Assignment model = solver.model(); - System.out.println("model = " + model); assertThat(model.size()).isEqualTo(8); assertThat(model.positiveVariables()).hasSize(1); - assertThat(model.positiveVariables()).extracting("name").containsExactlyInAnyOrder("y"); + assertThat(model.positiveVariables()).extracting(Variable::name).containsExactlyInAnyOrder("y"); assertThat(model.negativeLiterals()).hasSize(7); - assertThat(model.negativeVariables()).extracting("name").containsExactlyInAnyOrder("a", "b", "c", "d", "e", "x", "z"); + assertThat(model.negativeVariables()).extracting(Variable::name).containsExactlyInAnyOrder("a", "b", "c", "d", "e", "x", "z"); } @Test diff --git a/src/test/java/org/logicng/transformations/AIGTest.java b/src/test/java/org/logicng/transformations/AIGTest.java index 20390f1a..d3959aaa 100644 --- a/src/test/java/org/logicng/transformations/AIGTest.java +++ b/src/test/java/org/logicng/transformations/AIGTest.java @@ -106,6 +106,7 @@ public void testNAryOperators() throws ParserException { assertThat(p.parse("~(a & b) | c | ~(x | ~y)").transform(this.aigTrans).holds(this.aigPred)).isTrue(); assertThat(p.parse("a | b | (~x & ~y)").transform(this.aigTrans).holds(this.aigPred)).isTrue(); assertThat(this.AND1.holds(this.aigPred)).isTrue(); + assertThat(this.f.and(this.AND1, this.PBC1).holds(this.aigPred)).isFalse(); assertThat(this.OR1.holds(this.aigPred)).isFalse(); assertThat(p.parse("~(a | b) & c & ~(x & ~y) & (w => z)").holds(this.aigPred)).isFalse(); assertThat(p.parse("~(a & b) | c | ~(x | ~y)").holds(this.aigPred)).isFalse();