diff --git a/core/pom.xml b/core/pom.xml index 7e68e86c..3622ad87 100644 --- a/core/pom.xml +++ b/core/pom.xml @@ -46,24 +46,6 @@ - - - org.antlr - antlr4-maven-plugin - ${version.antlr-plugin} - - src/main/antlr - target/generated-sources/antlr/org/logicng/io/parsers - - - - - antlr4 - - - - - org.apache.maven.plugins maven-compiler-plugin @@ -197,18 +179,96 @@ -Xmx2g + + + + org.antlr + antlr4-maven-plugin + ${version.antlr-plugin} + + ../parser/src/main/antlr + target/generated-test-sources/antlr/org/logicng/io/parsers + + + + generate-test-sources + + antlr4 + + + + + + + org.apache.maven.plugins + maven-resources-plugin + ${version.resources-plugin} + + + copy-parser-classes + process-test-sources + + copy-resources + + + target/generated-test-sources/antlr/org/logicng/io/parsers + + + ../parser/src/main/java/org/logicng/io/parsers + false + + + + + + copy-reader-classes + process-test-sources + + copy-resources + + + target/generated-test-sources/antlr/org/logicng/io/readers + + + ../parser/src/main/java/org/logicng/io/readers + false + + + + + + + + org.codehaus.mojo + build-helper-maven-plugin + ${version.build-helper-plugin} + + + add-parser-sources + generate-test-sources + + add-test-source + + + + target/generated-test-sources/antlr + + + + + - + org.antlr antlr4-runtime ${version.antlr} + test - org.junit.jupiter junit-jupiter diff --git a/core/src/main/java/org/logicng/formulas/FormulaFactory.java b/core/src/main/java/org/logicng/formulas/FormulaFactory.java index 58e77ab5..2a082926 100644 --- a/core/src/main/java/org/logicng/formulas/FormulaFactory.java +++ b/core/src/main/java/org/logicng/formulas/FormulaFactory.java @@ -45,8 +45,6 @@ import org.logicng.formulas.cache.CacheEntry; import org.logicng.formulas.printer.FormulaStringRepresentation; import org.logicng.functions.SubNodeFunction; -import org.logicng.io.parsers.ParserException; -import org.logicng.io.parsers.PseudoBooleanParser; import org.logicng.pseudobooleans.PBConfig; import org.logicng.pseudobooleans.PBEncoder; import org.logicng.solvers.maxsat.algorithms.MaxSATConfig; @@ -103,7 +101,6 @@ public class FormulaFactory { private final SubNodeFunction subformulaFunction; private final PBEncoder pbEncoder; private final CNFEncoder cnfEncoder; - private final PseudoBooleanParser parser; Map posLiterals; Map negLiterals; Set generatedVariables; @@ -155,7 +152,6 @@ public FormulaFactory(final FormulaFactoryConfig config) { this.cnfPrefix = CNF_PREFIX; } this.pbEncoder = new PBEncoder(this); - this.parser = new PseudoBooleanParser(this); } /** @@ -1400,16 +1396,6 @@ public long numberOfNodes(final Formula formula) { return formula.apply(this.subformulaFunction).size(); } - /** - * Parses a given string to a formula using a pseudo boolean parser. - * @param string a string representing the formula - * @return the formula - * @throws ParserException if the parser throws an exception - */ - public Formula parse(final String string) throws ParserException { - return this.parser.parse(string); - } - /** * Adds a given formula to a list of operands. If the formula is the neutral element for the respective n-ary * operation it will be skipped. If a complementary formula is already present in the list of operands or the diff --git a/core/src/test/java/org/logicng/TestWithExampleFormulas.java b/core/src/test/java/org/logicng/TestWithExampleFormulas.java index b6c1fe5f..fb953713 100644 --- a/core/src/test/java/org/logicng/TestWithExampleFormulas.java +++ b/core/src/test/java/org/logicng/TestWithExampleFormulas.java @@ -34,6 +34,8 @@ 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.PseudoBooleanParser; public abstract class TestWithExampleFormulas { protected final FormulaFactory f = new FormulaFactory(); @@ -89,4 +91,12 @@ public abstract class TestWithExampleFormulas { protected final Formula PBC3 = this.f.pbc(CType.GE, 2, this.literals, this.coefficients); protected final Formula PBC4 = this.f.pbc(CType.LT, 2, this.literals, this.coefficients); protected final Formula PBC5 = this.f.pbc(CType.LE, 2, this.literals, this.coefficients); + + public static Formula parse(final FormulaFactory f, final String formula) { + try { + return new PseudoBooleanParser(f).parse(formula); + } catch (final ParserException e) { + throw new RuntimeException(e); + } + } } diff --git a/core/src/test/java/org/logicng/datastructures/AssignmentTest.java b/core/src/test/java/org/logicng/datastructures/AssignmentTest.java index 39600551..10121152 100644 --- a/core/src/test/java/org/logicng/datastructures/AssignmentTest.java +++ b/core/src/test/java/org/logicng/datastructures/AssignmentTest.java @@ -207,7 +207,7 @@ public void testEquals() { } @Test - public void testBlockingClause() throws ParserException { + public void testBlockingClause() { final Assignment ass = new Assignment(); ass.addLiteral(this.A); ass.addLiteral(this.B); @@ -215,14 +215,14 @@ public void testBlockingClause() throws ParserException { ass.addLiteral(this.NY); final Formula bc01 = ass.blockingClause(this.f); assertThat(bc01.containsVariable(this.C)).isFalse(); - assertThat(bc01).isEqualTo(this.f.parse("~a | ~b | x | y")); + assertThat(bc01).isEqualTo(parse(this.f, "~a | ~b | x | y")); final Formula bc02 = ass.blockingClause(this.f, null); assertThat(bc02.containsVariable(this.C)).isFalse(); - assertThat(bc02).isEqualTo(this.f.parse("~a | ~b | x | y")); + assertThat(bc02).isEqualTo(parse(this.f, "~a | ~b | x | y")); final List lits = Arrays.asList(this.A, this.X, this.C); final Formula bcProjected = ass.blockingClause(this.f, lits); assertThat(bcProjected.containsVariable(this.C)).isFalse(); - assertThat(bcProjected).isEqualTo(this.f.parse("~a | x")); + assertThat(bcProjected).isEqualTo(parse(this.f, "~a | x")); } @Test diff --git a/core/src/test/java/org/logicng/explanations/drup/DRUPTest.java b/core/src/test/java/org/logicng/explanations/drup/DRUPTest.java index 1c573032..018b4569 100644 --- a/core/src/test/java/org/logicng/explanations/drup/DRUPTest.java +++ b/core/src/test/java/org/logicng/explanations/drup/DRUPTest.java @@ -29,6 +29,7 @@ package org.logicng.explanations.drup; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import static org.logicng.datastructures.Tristate.FALSE; import static org.logicng.datastructures.Tristate.TRUE; @@ -40,7 +41,6 @@ import org.logicng.explanations.UNSATCore; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.io.readers.DimacsReader; import org.logicng.propositions.ExtendedProposition; import org.logicng.propositions.Proposition; @@ -145,16 +145,16 @@ public void testUnsatCoresAimTestset() throws IOException { } @Test - public void testPropositionHandling() throws ParserException { + public void testPropositionHandling() { final List propositions = new ArrayList<>(); - propositions.add(new StandardProposition("P1", this.f.parse("((a & b) => c) & ((a & b) => d)"))); - propositions.add(new StandardProposition("P2", this.f.parse("(c & d) <=> ~e"))); - propositions.add(new StandardProposition("P3", this.f.parse("~e => f | g"))); - propositions.add(new StandardProposition("P4", this.f.parse("(f => ~a) & (g => ~b) & p & q"))); - propositions.add(new StandardProposition("P5", this.f.parse("a => b"))); - propositions.add(new StandardProposition("P6", this.f.parse("a"))); - propositions.add(new StandardProposition("P7", this.f.parse("g | h"))); - propositions.add(new StandardProposition("P8", this.f.parse("(x => ~y | z) & (z | w)"))); + propositions.add(new StandardProposition("P1", parse(this.f, "((a & b) => c) & ((a & b) => d)"))); + propositions.add(new StandardProposition("P2", parse(this.f, "(c & d) <=> ~e"))); + propositions.add(new StandardProposition("P3", parse(this.f, "~e => f | g"))); + propositions.add(new StandardProposition("P4", parse(this.f, "(f => ~a) & (g => ~b) & p & q"))); + propositions.add(new StandardProposition("P5", parse(this.f, "a => b"))); + propositions.add(new StandardProposition("P6", parse(this.f, "a"))); + propositions.add(new StandardProposition("P7", parse(this.f, "g | h"))); + propositions.add(new StandardProposition("P8", parse(this.f, "(x => ~y | z) & (z | w)"))); for (final SATSolver solver : this.solvers) { solver.addPropositions(propositions); @@ -167,19 +167,19 @@ public void testPropositionHandling() throws ParserException { } @Test - public void testPropositionIncDec() throws ParserException { + public void testPropositionIncDec() { final SATSolver solver = this.solvers[0]; - final StandardProposition p1 = new StandardProposition("P1", this.f.parse("((a & b) => c) & ((a & b) => d)")); - final StandardProposition p2 = new StandardProposition("P2", this.f.parse("(c & d) <=> ~e")); - final StandardProposition p3 = new StandardProposition("P3", this.f.parse("~e => f | g")); - final StandardProposition p4 = new StandardProposition("P4", this.f.parse("(f => ~a) & (g => ~b) & p & q")); - final StandardProposition p5 = new StandardProposition("P5", this.f.parse("a => b")); - final StandardProposition p6 = new StandardProposition("P6", this.f.parse("a")); - final StandardProposition p7 = new StandardProposition("P7", this.f.parse("g | h")); - final StandardProposition p8 = new StandardProposition("P8", this.f.parse("(x => ~y | z) & (z | w)")); - final StandardProposition p9 = new StandardProposition("P9", this.f.parse("a & b")); - final StandardProposition p10 = new StandardProposition("P10", this.f.parse("(p => q) & p")); - final StandardProposition p11 = new StandardProposition("P11", this.f.parse("a & ~q")); + final StandardProposition p1 = new StandardProposition("P1", parse(this.f, "((a & b) => c) & ((a & b) => d)")); + final StandardProposition p2 = new StandardProposition("P2", parse(this.f, "(c & d) <=> ~e")); + final StandardProposition p3 = new StandardProposition("P3", parse(this.f, "~e => f | g")); + final StandardProposition p4 = new StandardProposition("P4", parse(this.f, "(f => ~a) & (g => ~b) & p & q")); + final StandardProposition p5 = new StandardProposition("P5", parse(this.f, "a => b")); + final StandardProposition p6 = new StandardProposition("P6", parse(this.f, "a")); + final StandardProposition p7 = new StandardProposition("P7", parse(this.f, "g | h")); + final StandardProposition p8 = new StandardProposition("P8", parse(this.f, "(x => ~y | z) & (z | w)")); + final StandardProposition p9 = new StandardProposition("P9", parse(this.f, "a & b")); + final StandardProposition p10 = new StandardProposition("P10", parse(this.f, "(p => q) & p")); + final StandardProposition p11 = new StandardProposition("P11", parse(this.f, "a & ~q")); solver.addPropositions(p1, p2, p3, p4); final SolverState state1 = solver.saveState(); @@ -218,10 +218,10 @@ public void testPropositionIncDec() throws ParserException { } @Test - public void testTrivialCasesPropositions() throws ParserException { + public void testTrivialCasesPropositions() { for (final SATSolver solver : this.solvers) { assertSolverSat(solver); - final StandardProposition p1 = new StandardProposition("P1", this.f.parse("$false")); + final StandardProposition p1 = new StandardProposition("P1", parse(this.f, "$false")); solver.add(p1); assertSolverUnsat(solver); UNSATCore unsatCore = solver.unsatCore(); @@ -229,10 +229,10 @@ public void testTrivialCasesPropositions() throws ParserException { solver.reset(); assertSolverSat(solver); - final StandardProposition p2 = new StandardProposition("P2", this.f.parse("a")); + final StandardProposition p2 = new StandardProposition("P2", parse(this.f, "a")); solver.add(p2); assertSolverSat(solver); - final StandardProposition p3 = new StandardProposition("P3", this.f.parse("~a")); + final StandardProposition p3 = new StandardProposition("P3", parse(this.f, "~a")); solver.add(p3); assertSolverUnsat(solver); unsatCore = solver.unsatCore(); @@ -241,15 +241,15 @@ public void testTrivialCasesPropositions() throws ParserException { } @Test - public void testCoreAndAssumptions() throws ParserException { + public void testCoreAndAssumptions() { final FormulaFactory f = new FormulaFactory(); final SATSolver[] solvers = new SATSolver[]{ MiniSat.miniSat(f, MiniSatConfig.builder().proofGeneration(true).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build()), MiniSat.glucose(f, MiniSatConfig.builder().proofGeneration(true).incremental(false).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build(), GlucoseConfig.builder().build()) }; for (final SATSolver solver : solvers) { - final StandardProposition p1 = new StandardProposition(f.parse("A => B")); - final StandardProposition p2 = new StandardProposition(f.parse("A & B => G")); + final StandardProposition p1 = new StandardProposition(parse(f, "A => B")); + final StandardProposition p2 = new StandardProposition(parse(f, "A & B => G")); final StandardProposition p3 = new StandardProposition(f.or(f.literal("X", false), f.literal("A", true))); final StandardProposition p4 = new StandardProposition(f.or(f.literal("X", false), f.literal("G", false))); final StandardProposition p5 = new StandardProposition(f.literal("G", false)); @@ -271,28 +271,28 @@ public void testCoreAndAssumptions() throws ParserException { } @Test - public void testCoreAndAssumptions2() throws ParserException { + public void testCoreAndAssumptions2() { final FormulaFactory f = new FormulaFactory(); final SATSolver[] solvers = new SATSolver[]{ MiniSat.miniSat(f, MiniSatConfig.builder().proofGeneration(true).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build()), MiniSat.glucose(f, MiniSatConfig.builder().proofGeneration(true).incremental(false).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build(), GlucoseConfig.builder().build()) }; for (final SATSolver solver : solvers) { - solver.add(f.parse("~C => D")); - solver.add(f.parse("C => D")); - solver.add(f.parse("D => B | A")); - solver.add(f.parse("B => X")); - solver.add(f.parse("B => ~X")); + solver.add(parse(f, "~C => D")); + solver.add(parse(f, "C => D")); + solver.add(parse(f, "D => B | A")); + solver.add(parse(f, "B => X")); + solver.add(parse(f, "B => ~X")); solver.sat(f.literal("A", false)); - solver.add(f.parse("~A")); + solver.add(parse(f, "~A")); solver.sat(); assertThat(solver.unsatCore()).isNotNull(); } } @Test - public void testCoreAndAssumptions3() throws ParserException { + public void testCoreAndAssumptions3() { // Unit test for DRUP issue which led to java.lang.ArrayIndexOutOfBoundsException: -1 final FormulaFactory f = new FormulaFactory(); final SATSolver[] solvers = new SATSolver[]{ @@ -300,21 +300,21 @@ public void testCoreAndAssumptions3() throws ParserException { MiniSat.glucose(f, MiniSatConfig.builder().proofGeneration(true).incremental(false).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build(), GlucoseConfig.builder().build()) }; for (final SATSolver solver : solvers) { - solver.add(f.parse("X => Y")); - solver.add(f.parse("X => Z")); - solver.add(f.parse("C => E")); - solver.add(f.parse("D => ~F")); - solver.add(f.parse("B => M")); - solver.add(f.parse("D => N")); - solver.add(f.parse("G => O")); - solver.add(f.parse("A => B")); - solver.add(f.parse("T1 <=> A & K & ~B & ~C")); - solver.add(f.parse("T2 <=> A & B & C & K")); - solver.add(f.parse("T1 + T2 = 1")); + solver.add(parse(f, "X => Y")); + solver.add(parse(f, "X => Z")); + solver.add(parse(f, "C => E")); + solver.add(parse(f, "D => ~F")); + solver.add(parse(f, "B => M")); + solver.add(parse(f, "D => N")); + solver.add(parse(f, "G => O")); + solver.add(parse(f, "A => B")); + solver.add(parse(f, "T1 <=> A & K & ~B & ~C")); + solver.add(parse(f, "T2 <=> A & B & C & K")); + solver.add(parse(f, "T1 + T2 = 1")); solver.sat(); // required for DRUP issue - solver.add(f.parse("Y => ~X & D")); - solver.add(f.parse("X")); + solver.add(parse(f, "Y => ~X & D")); + solver.add(parse(f, "X")); solver.sat(); assertThat(solver.unsatCore()).isNotNull(); @@ -322,35 +322,35 @@ public void testCoreAndAssumptions3() throws ParserException { } @Test - public void testCoreAndAssumptions4() throws ParserException { + public void testCoreAndAssumptions4() { final SATSolver[] solvers = new SATSolver[]{ MiniSat.miniSat(this.f, MiniSatConfig.builder().proofGeneration(true).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build()), MiniSat.glucose(this.f, MiniSatConfig.builder().proofGeneration(true).incremental(false).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build(), GlucoseConfig.builder().build()) }; for (final SATSolver solver : solvers) { - solver.add(this.f.parse("~X1")); + solver.add(parse(this.f, "~X1")); solver.sat(this.f.variable("X1")); // caused the bug solver.add(this.f.variable("A1")); - solver.add(this.f.parse("A1 => A2")); - solver.add(this.f.parse("R & A2 => A3")); - solver.add(this.f.parse("L & A2 => A3")); - solver.add(this.f.parse("R & A3 => A4")); - solver.add(this.f.parse("L & A3 => A4")); - solver.add(this.f.parse("~A4")); - solver.add(this.f.parse("L | R")); + solver.add(parse(this.f, "A1 => A2")); + solver.add(parse(this.f, "R & A2 => A3")); + solver.add(parse(this.f, "L & A2 => A3")); + solver.add(parse(this.f, "R & A3 => A4")); + solver.add(parse(this.f, "L & A3 => A4")); + solver.add(parse(this.f, "~A4")); + solver.add(parse(this.f, "L | R")); solver.sat(); assertThat(solver.unsatCore()).isNotNull(); } } @Test - public void testWithCcPropositions() throws ParserException { + public void testWithCcPropositions() { final FormulaFactory f = new FormulaFactory(); final SATSolver solver = MiniSat.miniSat(f, MiniSatConfig.builder().proofGeneration(true).cnfMethod(MiniSatConfig.CNFMethod.PG_ON_SOLVER).build()); - final ExtendedProposition p1 = new ExtendedProposition<>(new StringBackpack("CC"), f.parse("A + B + C <= 1")); - final StandardProposition p2 = new StandardProposition(f.parse("A")); - final StandardProposition p3 = new StandardProposition(f.parse("B")); - final StandardProposition p4 = new StandardProposition(f.parse("X & Y")); + final ExtendedProposition p1 = new ExtendedProposition<>(new StringBackpack("CC"), parse(f, "A + B + C <= 1")); + final StandardProposition p2 = new StandardProposition(parse(f, "A")); + final StandardProposition p3 = new StandardProposition(parse(f, "B")); + final StandardProposition p4 = new StandardProposition(parse(f, "X & Y")); solver.add(p1); solver.add(p2); solver.add(p3); @@ -360,20 +360,20 @@ public void testWithCcPropositions() throws ParserException { } @Test - public void testWithSpecialUnitCaseMiniSat() throws ParserException { + public void testWithSpecialUnitCaseMiniSat() { final FormulaFactory f = new FormulaFactory(); final SATSolver solver = MiniSat.miniSat(f, MiniSatConfig.builder().proofGeneration(true).build()); - final StandardProposition p1 = new StandardProposition(f.parse("a => b")); - final StandardProposition p2 = new StandardProposition(f.parse("a => c | d")); - final StandardProposition p3 = new StandardProposition(f.parse("b => c | d")); - final StandardProposition p4 = new StandardProposition(f.parse("e | f | g | h => i")); - final StandardProposition p5 = new StandardProposition(f.parse("~j => k | j")); - final StandardProposition p6 = new StandardProposition(f.parse("b => ~(e | f)")); - final StandardProposition p7 = new StandardProposition(f.parse("c => ~j")); - final StandardProposition p8 = new StandardProposition(f.parse("l | m => ~i")); - final StandardProposition p9 = new StandardProposition(f.parse("j => (f + g + h = 1)")); - final StandardProposition p10 = new StandardProposition(f.parse("d => (l + m + e + f = 1)")); - final StandardProposition p11 = new StandardProposition(f.parse("~k")); + final StandardProposition p1 = new StandardProposition(parse(f, "a => b")); + final StandardProposition p2 = new StandardProposition(parse(f, "a => c | d")); + final StandardProposition p3 = new StandardProposition(parse(f, "b => c | d")); + final StandardProposition p4 = new StandardProposition(parse(f, "e | f | g | h => i")); + final StandardProposition p5 = new StandardProposition(parse(f, "~j => k | j")); + final StandardProposition p6 = new StandardProposition(parse(f, "b => ~(e | f)")); + final StandardProposition p7 = new StandardProposition(parse(f, "c => ~j")); + final StandardProposition p8 = new StandardProposition(parse(f, "l | m => ~i")); + final StandardProposition p9 = new StandardProposition(parse(f, "j => (f + g + h = 1)")); + final StandardProposition p10 = new StandardProposition(parse(f, "d => (l + m + e + f = 1)")); + final StandardProposition p11 = new StandardProposition(parse(f, "~k")); solver.addPropositions(p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11); assertThat(solver.sat()).isEqualTo(TRUE); solver.add(f.variable("a")); @@ -382,20 +382,20 @@ public void testWithSpecialUnitCaseMiniSat() throws ParserException { } @Test - public void testWithSpecialUnitCaseGlucose() throws ParserException { + public void testWithSpecialUnitCaseGlucose() { final FormulaFactory f = new FormulaFactory(); final SATSolver solver = MiniSat.glucose(f, MiniSatConfig.builder().proofGeneration(true).incremental(false).build(), GlucoseConfig.builder().build()); - final StandardProposition p1 = new StandardProposition(f.parse("a => b")); - final StandardProposition p2 = new StandardProposition(f.parse("a => c | d")); - final StandardProposition p3 = new StandardProposition(f.parse("b => c | d")); - final StandardProposition p4 = new StandardProposition(f.parse("e | f | g | h => i")); - final StandardProposition p5 = new StandardProposition(f.parse("~j => k | j")); - final StandardProposition p6 = new StandardProposition(f.parse("b => ~(e | f)")); - final StandardProposition p7 = new StandardProposition(f.parse("c => ~j")); - final StandardProposition p8 = new StandardProposition(f.parse("l | m => ~i")); - final StandardProposition p9 = new StandardProposition(f.parse("j => (f + g + h = 1)")); - final StandardProposition p10 = new StandardProposition(f.parse("d => (l + m + e + f = 1)")); - final StandardProposition p11 = new StandardProposition(f.parse("~k")); + final StandardProposition p1 = new StandardProposition(parse(f, "a => b")); + final StandardProposition p2 = new StandardProposition(parse(f, "a => c | d")); + final StandardProposition p3 = new StandardProposition(parse(f, "b => c | d")); + final StandardProposition p4 = new StandardProposition(parse(f, "e | f | g | h => i")); + final StandardProposition p5 = new StandardProposition(parse(f, "~j => k | j")); + final StandardProposition p6 = new StandardProposition(parse(f, "b => ~(e | f)")); + final StandardProposition p7 = new StandardProposition(parse(f, "c => ~j")); + final StandardProposition p8 = new StandardProposition(parse(f, "l | m => ~i")); + final StandardProposition p9 = new StandardProposition(parse(f, "j => (f + g + h = 1)")); + final StandardProposition p10 = new StandardProposition(parse(f, "d => (l + m + e + f = 1)")); + final StandardProposition p11 = new StandardProposition(parse(f, "~k")); solver.addPropositions(p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11); assertThat(solver.sat()).isEqualTo(TRUE); solver.add(f.variable("a")); diff --git a/core/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java b/core/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java index d2553b85..e160bd82 100644 --- a/core/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java +++ b/core/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java @@ -55,185 +55,185 @@ public class SmusComputationTest extends TestWithExampleFormulas { @Test - public void testFromPaper() throws ParserException { + public void testFromPaper() { final List input = Arrays.asList( - this.f.parse("~s"), - this.f.parse("s|~p"), - this.f.parse("p"), - this.f.parse("~p|m"), - this.f.parse("~m|n"), - this.f.parse("~n"), - this.f.parse("~m|l"), - this.f.parse("~l") + parse(this.f, "~s"), + parse(this.f, "s|~p"), + parse(this.f, "p"), + parse(this.f, "~p|m"), + parse(this.f, "~m|n"), + parse(this.f, "~n"), + parse(this.f, "~m|l"), + parse(this.f, "~l") ); final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f); - assertThat(result).containsExactlyInAnyOrder(this.f.parse("~s"), this.f.parse("s|~p"), this.f.parse("p")); + assertThat(result).containsExactlyInAnyOrder(parse(this.f, "~s"), parse(this.f, "s|~p"), parse(this.f, "p")); } @Test - public void testWithAdditionalConstraint() throws ParserException { + public void testWithAdditionalConstraint() { final List input = Arrays.asList( - this.f.parse("~s"), - this.f.parse("s|~p"), - this.f.parse("p"), - this.f.parse("~p|m"), - this.f.parse("~m|n"), - this.f.parse("~n"), - this.f.parse("~m|l"), - this.f.parse("~l") + parse(this.f, "~s"), + parse(this.f, "s|~p"), + parse(this.f, "p"), + parse(this.f, "~p|m"), + parse(this.f, "~m|n"), + parse(this.f, "~n"), + parse(this.f, "~m|l"), + parse(this.f, "~l") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(this.f.parse("n|l")), this.f); - assertThat(result).containsExactlyInAnyOrder(this.f.parse("~n"), this.f.parse("~l")); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f); + assertThat(result).containsExactlyInAnyOrder(parse(this.f, "~n"), parse(this.f, "~l")); } @Test - public void testSatisfiable() throws ParserException { + public void testSatisfiable() { final List input = Arrays.asList( - this.f.parse("~s"), - this.f.parse("s|~p"), - this.f.parse("~p|m"), - this.f.parse("~m|n"), - this.f.parse("~n"), - this.f.parse("~m|l") + parse(this.f, "~s"), + parse(this.f, "s|~p"), + parse(this.f, "~p|m"), + parse(this.f, "~m|n"), + parse(this.f, "~n"), + parse(this.f, "~m|l") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(this.f.parse("n|l")), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f); assertThat(result).isNull(); } @Test - public void testUnsatisfiableAdditionalConstraints() throws ParserException { + public void testUnsatisfiableAdditionalConstraints() { final List input = Arrays.asList( - this.f.parse("~s"), - this.f.parse("s|~p"), - this.f.parse("~p|m"), - this.f.parse("~m|n"), - this.f.parse("~n|s") + parse(this.f, "~s"), + parse(this.f, "s|~p"), + parse(this.f, "~p|m"), + parse(this.f, "~m|n"), + parse(this.f, "~n|s") ); - final List result = SmusComputation.computeSmusForFormulas(input, Arrays.asList(this.f.parse("~a&b"), this.f.parse("a|~b")), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Arrays.asList(parse(this.f, "~a&b"), parse(this.f, "a|~b")), this.f); assertThat(result).isEmpty(); } @Test - public void testTrivialUnsatFormula() throws ParserException { + public void testTrivialUnsatFormula() { final List input = Arrays.asList( - this.f.parse("~s"), - this.f.parse("s|~p"), - this.f.parse("p"), - this.f.parse("~p|m"), - this.f.parse("~m|n"), - this.f.parse("~n"), - this.f.parse("~m|l"), - this.f.parse("~l"), - this.f.parse("a&~a") + parse(this.f, "~s"), + parse(this.f, "s|~p"), + parse(this.f, "p"), + parse(this.f, "~p|m"), + parse(this.f, "~m|n"), + parse(this.f, "~n"), + parse(this.f, "~m|l"), + parse(this.f, "~l"), + parse(this.f, "a&~a") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(this.f.parse("n|l")), this.f); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f); assertThat(result).containsExactly(this.f.falsum()); } @Test - public void testUnsatFormula() throws ParserException { + public void testUnsatFormula() { final List input = Arrays.asList( - this.f.parse("~s"), - this.f.parse("s|~p"), - this.f.parse("p"), - this.f.parse("~p|m"), - this.f.parse("~m|n"), - this.f.parse("~n"), - this.f.parse("~m|l"), - this.f.parse("~l"), - this.f.parse("(a<=>b)&(~a<=>b)") + parse(this.f, "~s"), + parse(this.f, "s|~p"), + parse(this.f, "p"), + parse(this.f, "~p|m"), + parse(this.f, "~m|n"), + parse(this.f, "~n"), + parse(this.f, "~m|l"), + parse(this.f, "~l"), + parse(this.f, "(a<=>b)&(~a<=>b)") ); - final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(this.f.parse("n|l")), this.f); - assertThat(result).containsExactly(this.f.parse("(a<=>b)&(~a<=>b)")); + final List result = SmusComputation.computeSmusForFormulas(input, Collections.singletonList(parse(this.f, "n|l")), this.f); + assertThat(result).containsExactly(parse(this.f, "(a<=>b)&(~a<=>b)")); } @Test - public void testShorterConflict() throws ParserException { + public void testShorterConflict() { final List input = Arrays.asList( - this.f.parse("~s"), - this.f.parse("s|~p"), - this.f.parse("p"), - this.f.parse("p&~s"), - this.f.parse("~p|m"), - this.f.parse("~m|n"), - this.f.parse("~n"), - this.f.parse("~m|l"), - this.f.parse("~l") + parse(this.f, "~s"), + parse(this.f, "s|~p"), + parse(this.f, "p"), + parse(this.f, "p&~s"), + parse(this.f, "~p|m"), + parse(this.f, "~m|n"), + parse(this.f, "~n"), + parse(this.f, "~m|l"), + parse(this.f, "~l") ); final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f); - assertThat(result).containsExactlyInAnyOrder(this.f.parse("s|~p"), this.f.parse("p&~s")); + assertThat(result).containsExactlyInAnyOrder(parse(this.f, "s|~p"), parse(this.f, "p&~s")); } @Test - public void testCompleteConflict() throws ParserException { + public void testCompleteConflict() { final List input = Arrays.asList( - this.f.parse("~s"), - this.f.parse("s|~p"), - this.f.parse("p|~m"), - this.f.parse("m|~n"), - this.f.parse("n|~l"), - this.f.parse("l|s") + parse(this.f, "~s"), + parse(this.f, "s|~p"), + parse(this.f, "p|~m"), + parse(this.f, "m|~n"), + parse(this.f, "n|~l"), + parse(this.f, "l|s") ); final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f); assertThat(result).containsExactlyInAnyOrderElementsOf(input); } @Test - public void testLongConflictWithShortcut() throws ParserException { + public void testLongConflictWithShortcut() { final List input = Arrays.asList( - this.f.parse("~s"), - this.f.parse("s|~p"), - this.f.parse("p|~m"), - this.f.parse("m|~n"), - this.f.parse("n|~l"), - this.f.parse("l|s"), - this.f.parse("n|s") + parse(this.f, "~s"), + parse(this.f, "s|~p"), + parse(this.f, "p|~m"), + parse(this.f, "m|~n"), + parse(this.f, "n|~l"), + parse(this.f, "l|s"), + parse(this.f, "n|s") ); final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f); - assertThat(result).containsExactlyInAnyOrder(this.f.parse("~s"), - this.f.parse("s|~p"), - this.f.parse("p|~m"), - this.f.parse("m|~n"), - this.f.parse("n|s")); + assertThat(result).containsExactlyInAnyOrder(parse(this.f, "~s"), + parse(this.f, "s|~p"), + parse(this.f, "p|~m"), + parse(this.f, "m|~n"), + parse(this.f, "n|s")); } @Test - public void testManyConflicts() throws ParserException { + public void testManyConflicts() { final List input = Arrays.asList( - this.f.parse("a"), - this.f.parse("~a|b"), - this.f.parse("~b|c"), - this.f.parse("~c|~a"), - this.f.parse("a1"), - this.f.parse("~a1|b1"), - this.f.parse("~b1|c1"), - this.f.parse("~c1|~a1"), - this.f.parse("a2"), - this.f.parse("~a2|b2"), - this.f.parse("~b2|c2"), - this.f.parse("~c2|~a2"), - this.f.parse("a3"), - this.f.parse("~a3|b3"), - this.f.parse("~b3|c3"), - this.f.parse("~c3|~a3"), - this.f.parse("a1|a2|a3|a4|b1|x|y"), - this.f.parse("x&~y"), - this.f.parse("x=>y") + parse(this.f, "a"), + parse(this.f, "~a|b"), + parse(this.f, "~b|c"), + parse(this.f, "~c|~a"), + parse(this.f, "a1"), + parse(this.f, "~a1|b1"), + parse(this.f, "~b1|c1"), + parse(this.f, "~c1|~a1"), + parse(this.f, "a2"), + parse(this.f, "~a2|b2"), + parse(this.f, "~b2|c2"), + parse(this.f, "~c2|~a2"), + parse(this.f, "a3"), + parse(this.f, "~a3|b3"), + parse(this.f, "~b3|c3"), + parse(this.f, "~c3|~a3"), + parse(this.f, "a1|a2|a3|a4|b1|x|y"), + parse(this.f, "x&~y"), + parse(this.f, "x=>y") ); final List result = SmusComputation.computeSmusForFormulas(input, Collections.emptyList(), this.f); - assertThat(result).containsExactlyInAnyOrder(this.f.parse("x&~y"), this.f.parse("x=>y")); + assertThat(result).containsExactlyInAnyOrder(parse(this.f, "x&~y"), parse(this.f, "x=>y")); } @Test - public void testTimeoutHandlerSmall() throws ParserException { + public void testTimeoutHandlerSmall() { final List handlers = Arrays.asList( new TimeoutOptimizationHandler(5_000L, TimeoutHandler.TimerType.SINGLE_TIMEOUT), new TimeoutOptimizationHandler(5_000L, TimeoutHandler.TimerType.RESTARTING_TIMEOUT), new TimeoutOptimizationHandler(System.currentTimeMillis() + 5_000L, TimeoutHandler.TimerType.FIXED_END) ); final List formulas = Arrays.asList( - this.f.parse("a"), - this.f.parse("~a") + parse(this.f, "a"), + parse(this.f, "~a") ); for (final TimeoutOptimizationHandler handler : handlers) { testHandler(handler, formulas, false); @@ -241,7 +241,7 @@ public void testTimeoutHandlerSmall() throws ParserException { } @Test - public void testTimeoutHandlerLarge() throws ParserException, IOException { + public void testTimeoutHandlerLarge() throws IOException, ParserException { final List handlers = Arrays.asList( new TimeoutOptimizationHandler(1L, TimeoutHandler.TimerType.SINGLE_TIMEOUT), new TimeoutOptimizationHandler(1L, TimeoutHandler.TimerType.RESTARTING_TIMEOUT), @@ -266,22 +266,22 @@ public void testCancellationPoints() throws IOException { } @Test - public void testMinimumHittingSetCancelled() throws ParserException { + public void testMinimumHittingSetCancelled() { final OptimizationHandler handler = new BoundedOptimizationHandler(-1, 0); final List formulas = Arrays.asList( - this.f.parse("a"), - this.f.parse("~a") + parse(this.f, "a"), + parse(this.f, "~a") ); testHandler(handler, formulas, true); } @Test - public void testHSolverCancelled() throws ParserException { + public void testHSolverCancelled() { final OptimizationHandler handler = new BoundedOptimizationHandler(-1, 3); final List formulas = Arrays.asList( - this.f.parse("a"), - this.f.parse("~a"), - this.f.parse("c") + parse(this.f, "a"), + parse(this.f, "~a"), + parse(this.f, "c") ); testHandler(handler, formulas, true); } diff --git a/core/src/test/java/org/logicng/formulas/ExtendedFormulaFactoryTest.java b/core/src/test/java/org/logicng/formulas/ExtendedFormulaFactoryTest.java index 2eb41501..a25b678e 100644 --- a/core/src/test/java/org/logicng/formulas/ExtendedFormulaFactoryTest.java +++ b/core/src/test/java/org/logicng/formulas/ExtendedFormulaFactoryTest.java @@ -31,6 +31,7 @@ import static org.assertj.core.api.Assertions.assertThat; import static org.assertj.core.api.Assertions.assertThatThrownBy; import static org.assertj.core.data.MapEntry.entry; +import static org.logicng.TestWithExampleFormulas.parse; import org.assertj.core.api.SoftAssertions; import org.junit.jupiter.api.Test; @@ -38,7 +39,6 @@ import org.logicng.datastructures.Tristate; import org.logicng.formulas.cache.PredicateCacheEntry; import org.logicng.formulas.cache.TransformationCacheEntry; -import org.logicng.io.parsers.ParserException; import org.logicng.testutils.PigeonHoleGenerator; import org.logicng.transformations.cnf.CNFFactorization; import org.logicng.transformations.cnf.PlaistedGreenbaumTransformation; @@ -133,7 +133,7 @@ public void testLoad01() { } @Test - public void testLoad02() throws ParserException { + public void testLoad02() { final SoftAssertions softly = new SoftAssertions(); final ExtendedFormulaFactory eff = new ExtendedFormulaFactory(); final Variable a = eff.variable("A"); @@ -151,7 +151,7 @@ public void testLoad02() throws ParserException { final Or or3 = (Or) eff.or(a, b, c); final Or or4 = (Or) eff.or(a, b, c, d); final Or or5 = (Or) eff.or(a, b, c, d, e); - eff.parse("A | B & C").transform(new PlaistedGreenbaumTransformation(0)); + parse(eff, "A | B & C").transform(new PlaistedGreenbaumTransformation(0)); softly.assertThat(eff.posLiterals).containsValue(b); softly.assertThat(eff.ands2).containsValue(and); softly.assertThat(eff.ands3).containsValue(and3); diff --git a/core/src/test/java/org/logicng/formulas/FormulaFactoryTest.java b/core/src/test/java/org/logicng/formulas/FormulaFactoryTest.java index 5649f5d3..80a62dd1 100644 --- a/core/src/test/java/org/logicng/formulas/FormulaFactoryTest.java +++ b/core/src/test/java/org/logicng/formulas/FormulaFactoryTest.java @@ -30,11 +30,11 @@ import static org.assertj.core.api.Assertions.assertThat; import static org.assertj.core.api.Assertions.assertThatThrownBy; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.logicng.configurations.Configuration; import org.logicng.configurations.ConfigurationType; -import org.logicng.io.parsers.ParserException; import org.logicng.io.parsers.PropositionalParser; import org.logicng.solvers.maxsat.algorithms.MaxSATConfig; import org.logicng.solvers.sat.GlucoseConfig; @@ -170,12 +170,12 @@ public void testCNF() { } @Test - public void testImportFormula() throws ParserException { + public void testImportFormula() { final FormulaFactory f = new FormulaFactory(FormulaFactoryConfig.builder().name("Factory F").build()); final FormulaFactory g = new FormulaFactory(FormulaFactoryConfig.builder().name("Factory G").build()); final PropositionalParser pf = new PropositionalParser(f); final String formula = "x1 & x2 & ~x3 => (x4 | (x5 <=> ~x1))"; - final Formula ff = pf.parse(formula); + final Formula ff = parse(f, formula); final Formula fg = g.importFormula(ff); assertThat(fg).isEqualTo(ff); assertThat(ff.factory()).isSameAs(f); diff --git a/core/src/test/java/org/logicng/formulas/FormulaFactoryWithoutContradictionCheckTest.java b/core/src/test/java/org/logicng/formulas/FormulaFactoryWithoutContradictionCheckTest.java index 95b50d42..ed34e39a 100644 --- a/core/src/test/java/org/logicng/formulas/FormulaFactoryWithoutContradictionCheckTest.java +++ b/core/src/test/java/org/logicng/formulas/FormulaFactoryWithoutContradictionCheckTest.java @@ -29,11 +29,11 @@ package org.logicng.formulas; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.logicng.datastructures.Assignment; import org.logicng.datastructures.Tristate; -import org.logicng.io.parsers.ParserException; import org.logicng.predicates.NNFPredicate; import org.logicng.predicates.satisfiability.ContingencyPredicate; import org.logicng.predicates.satisfiability.ContradictionPredicate; @@ -55,33 +55,33 @@ public class FormulaFactoryWithoutContradictionCheckTest { private final Formula contradiction = this.f.and(this.a, this.f.literal("A", false)); @Test - public void testSimpleFormulas() throws ParserException { - assertThat(this.f.parse("$true").toString()).isEqualTo("$true"); - assertThat(this.f.parse("$false").toString()).isEqualTo("$false"); - assertThat(this.f.parse("A").toString()).isEqualTo("A"); - assertThat(this.f.parse("~A").toString()).isEqualTo("~A"); - assertThat(this.f.parse("A & A & B").toString()).isEqualTo("A & B"); - assertThat(this.f.parse("A | A | B").toString()).isEqualTo("A | B"); - assertThat(this.f.parse("A => A & B").toString()).isEqualTo("A => A & B"); - assertThat(this.f.parse("A <=> A & B").toString()).isEqualTo("A <=> A & B"); + public void testSimpleFormulas() { + assertThat(parse(this.f, "$true").toString()).isEqualTo("$true"); + assertThat(parse(this.f, "$false").toString()).isEqualTo("$false"); + assertThat(parse(this.f, "A").toString()).isEqualTo("A"); + assertThat(parse(this.f, "~A").toString()).isEqualTo("~A"); + assertThat(parse(this.f, "A & A & B").toString()).isEqualTo("A & B"); + assertThat(parse(this.f, "A | A | B").toString()).isEqualTo("A | B"); + assertThat(parse(this.f, "A => A & B").toString()).isEqualTo("A => A & B"); + assertThat(parse(this.f, "A <=> A & B").toString()).isEqualTo("A <=> A & B"); } @Test - public void testContradictions() throws ParserException { - assertThat(this.f.parse("A & ~A").toString()).isEqualTo("A & ~A"); - assertThat(this.f.parse("~A & A").toString()).isEqualTo("A & ~A"); - assertThat(this.f.parse("~A & A & A & ~A & A & A & ~A").toString()).isEqualTo("A & ~A"); - assertThat(this.f.parse("(A | B) & ~(A | B)").toString()).isEqualTo("(A | B) & ~(A | B)"); - assertThat(this.f.parse("(A | B) & ~(B | A)").toString()).isEqualTo("(A | B) & ~(A | B)"); + public void testContradictions() { + assertThat(parse(this.f, "A & ~A").toString()).isEqualTo("A & ~A"); + assertThat(parse(this.f, "~A & A").toString()).isEqualTo("A & ~A"); + assertThat(parse(this.f, "~A & A & A & ~A & A & A & ~A").toString()).isEqualTo("A & ~A"); + assertThat(parse(this.f, "(A | B) & ~(A | B)").toString()).isEqualTo("(A | B) & ~(A | B)"); + assertThat(parse(this.f, "(A | B) & ~(B | A)").toString()).isEqualTo("(A | B) & ~(A | B)"); } @Test - public void testTautologies() throws ParserException { - assertThat(this.f.parse("A | ~A").toString()).isEqualTo("A | ~A"); - assertThat(this.f.parse("~A | A").toString()).isEqualTo("A | ~A"); - assertThat(this.f.parse("~A | A | A | ~A | A | A | ~A").toString()).isEqualTo("A | ~A"); - assertThat(this.f.parse("(A & B) | ~(A & B)").toString()).isEqualTo("A & B | ~(A & B)"); - assertThat(this.f.parse("(A & B) | ~(B & A)").toString()).isEqualTo("A & B | ~(A & B)"); + public void testTautologies() { + assertThat(parse(this.f, "A | ~A").toString()).isEqualTo("A | ~A"); + assertThat(parse(this.f, "~A | A").toString()).isEqualTo("A | ~A"); + assertThat(parse(this.f, "~A | A | A | ~A | A | A | ~A").toString()).isEqualTo("A | ~A"); + assertThat(parse(this.f, "(A & B) | ~(A & B)").toString()).isEqualTo("A & B | ~(A & B)"); + assertThat(parse(this.f, "(A & B) | ~(B & A)").toString()).isEqualTo("A & B | ~(A & B)"); } @Test @@ -159,15 +159,15 @@ public void testPredicates() { } @Test - public void testSatSolverWithTautologies() throws ParserException { + public void testSatSolverWithTautologies() { final SATSolver solver = MiniSat.miniSat(this.f); - solver.add(this.f.parse("A")); - solver.add(this.f.parse("A => B")); - solver.add(this.f.parse("C | ~C")); + solver.add(parse(this.f, "A")); + solver.add(parse(this.f, "A => B")); + solver.add(parse(this.f, "C | ~C")); List models = solver.enumerateAllModels(); assertThat(models).hasSize(2); models.forEach(m -> assertThat(m.literals()).containsAnyOf(this.f.literal("C", true), this.f.literal("C", false))); - solver.add(this.f.parse("D | ~D")); + solver.add(parse(this.f, "D | ~D")); models = solver.enumerateAllModels(); assertThat(models).hasSize(4); models.forEach(m -> assertThat(m.literals()).containsAnyOf(this.f.literal("C", true), this.f.literal("C", false), @@ -175,24 +175,24 @@ public void testSatSolverWithTautologies() throws ParserException { } @Test - public void testSatSolverWithContradictions() throws ParserException { + public void testSatSolverWithContradictions() { final SATSolver solver = MiniSat.miniSat(this.f); - solver.add(this.f.parse("A")); - solver.add(this.f.parse("A => B")); - solver.add(this.f.parse("C | ~C")); + solver.add(parse(this.f, "A")); + solver.add(parse(this.f, "A => B")); + solver.add(parse(this.f, "C | ~C")); final List models = solver.enumerateAllModels(); assertThat(models).hasSize(2); models.forEach(m -> assertThat(m.literals()).containsAnyOf(this.f.literal("C", true), this.f.literal("C", false))); - solver.add(this.f.parse("D & ~D")); + solver.add(parse(this.f, "D & ~D")); assertThat(solver.sat()).isEqualTo(Tristate.FALSE); } @Test - public void testSubsumption() throws ParserException { + public void testSubsumption() { assertThat(this.tautology.substitute(this.a, this.notA)).isEqualTo(this.tautology); assertThat(this.contradiction.substitute(this.a, this.notA)).isEqualTo(this.contradiction); - assertThat(this.tautology.substitute(this.a, this.f.variable("B"))).isEqualTo(this.f.parse("B | ~B")); - assertThat(this.contradiction.substitute(this.a, this.f.variable("B"))).isEqualTo(this.f.parse("B & ~B")); + assertThat(this.tautology.substitute(this.a, this.f.variable("B"))).isEqualTo(parse(this.f, "B | ~B")); + assertThat(this.contradiction.substitute(this.a, this.f.variable("B"))).isEqualTo(parse(this.f, "B & ~B")); } @Test diff --git a/core/src/test/java/org/logicng/formulas/FormulaTest.java b/core/src/test/java/org/logicng/formulas/FormulaTest.java index 45830955..3c87b552 100644 --- a/core/src/test/java/org/logicng/formulas/FormulaTest.java +++ b/core/src/test/java/org/logicng/formulas/FormulaTest.java @@ -29,6 +29,7 @@ package org.logicng.formulas; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import static org.logicng.formulas.cache.PredicateCacheEntry.IS_CNF; import static org.logicng.formulas.cache.PredicateCacheEntry.IS_DNF; import static org.logicng.formulas.cache.TransformationCacheEntry.FACTORIZED_CNF; @@ -36,7 +37,6 @@ import org.junit.jupiter.api.Test; import org.logicng.datastructures.Tristate; import org.logicng.formulas.cache.CacheEntry; -import org.logicng.io.parsers.ParserException; import org.logicng.transformations.cnf.BDDCNFTransformation; import java.util.Arrays; @@ -119,10 +119,10 @@ public void testCType() { } @Test - public void testIsSatisfiable() throws ParserException { + public void testIsSatisfiable() { final FormulaFactory f = new FormulaFactory(); - final Formula f1 = f.parse("(a | b) & (c | ~d)"); - final Formula f2 = f.parse("~a & ~b & (a | b)"); + final Formula f1 = parse(f, "(a | b) & (c | ~d)"); + final Formula f2 = parse(f, "~a & ~b & (a | b)"); assertThat(f.falsum().isSatisfiable()).isFalse(); assertThat(f.verum().isSatisfiable()).isTrue(); assertThat(f1.isSatisfiable()).isTrue(); @@ -130,10 +130,10 @@ public void testIsSatisfiable() throws ParserException { } @Test - public void testIsTautology() throws ParserException { + public void testIsTautology() { final FormulaFactory f = new FormulaFactory(); - final Formula f1 = f.parse("(a | b) & (c | ~d)"); - final Formula f2 = f.parse("(a & b) | (~a & b) | (a & ~b) | (~a & ~b)"); + final Formula f1 = parse(f, "(a | b) & (c | ~d)"); + final Formula f2 = parse(f, "(a & b) | (~a & b) | (a & ~b) | (~a & ~b)"); assertThat(f.falsum().isTautology()).isFalse(); assertThat(f.verum().isTautology()).isTrue(); assertThat(f1.isTautology()).isFalse(); @@ -141,10 +141,10 @@ public void testIsTautology() throws ParserException { } @Test - public void testIsContradiction() throws ParserException { + public void testIsContradiction() { final FormulaFactory f = new FormulaFactory(); - final Formula f1 = f.parse("(a | b) & (c | ~d)"); - final Formula f2 = f.parse("~a & ~b & (a | b)"); + final Formula f1 = parse(f, "(a | b) & (c | ~d)"); + final Formula f2 = parse(f, "~a & ~b & (a | b)"); assertThat(f.falsum().isContradiction()).isTrue(); assertThat(f.verum().isContradiction()).isFalse(); assertThat(f1.isContradiction()).isFalse(); @@ -152,11 +152,11 @@ public void testIsContradiction() throws ParserException { } @Test - public void testImplies() throws ParserException { + public void testImplies() { final FormulaFactory f = new FormulaFactory(); - final Formula f1 = f.parse("(a | b) & (c | ~d)"); - final Formula f2 = f.parse("(a | b) & (c | ~d) & (e | ~f)"); - final Formula f3 = f.parse("(a | b) & (c | d)"); + final Formula f1 = parse(f, "(a | b) & (c | ~d)"); + final Formula f2 = parse(f, "(a | b) & (c | ~d) & (e | ~f)"); + final Formula f3 = parse(f, "(a | b) & (c | d)"); assertThat(f1.implies(f2)).isFalse(); assertThat(f2.implies(f1)).isTrue(); assertThat(f1.implies(f3)).isFalse(); @@ -165,11 +165,11 @@ public void testImplies() throws ParserException { } @Test - public void testIsImpliedBy() throws ParserException { + public void testIsImpliedBy() { final FormulaFactory f = new FormulaFactory(); - final Formula f1 = f.parse("(a | b) & (c | ~d)"); - final Formula f2 = f.parse("(a | b) & (c | ~d) & (e | ~f)"); - final Formula f3 = f.parse("(a | b) & (c | d)"); + final Formula f1 = parse(f, "(a | b) & (c | ~d)"); + final Formula f2 = parse(f, "(a | b) & (c | ~d) & (e | ~f)"); + final Formula f3 = parse(f, "(a | b) & (c | d)"); assertThat(f1.isImpliedBy(f2)).isTrue(); assertThat(f2.isImpliedBy(f1)).isFalse(); assertThat(f1.isImpliedBy(f3)).isFalse(); @@ -178,11 +178,11 @@ public void testIsImpliedBy() throws ParserException { } @Test - public void testIsEquivalentTo() throws ParserException { + public void testIsEquivalentTo() { final FormulaFactory f = new FormulaFactory(); - final Formula f1 = f.parse("(a | b) & (c | ~d)"); - final Formula f2 = f.parse("(a | b) & (c | ~d) & (e | ~f)"); - final Formula f3 = f.parse("(a & c) | (a & ~d) | (b & c) | (b & ~d)"); + final Formula f1 = parse(f, "(a | b) & (c | ~d)"); + final Formula f2 = parse(f, "(a | b) & (c | ~d) & (e | ~f)"); + final Formula f3 = parse(f, "(a & c) | (a & ~d) | (b & c) | (b & ~d)"); assertThat(f1.isEquivalentTo(f2)).isFalse(); assertThat(f2.isEquivalentTo(f1)).isFalse(); assertThat(f1.isEquivalentTo(f3)).isTrue(); diff --git a/core/src/test/java/org/logicng/functions/FormulaDepthFunctionTest.java b/core/src/test/java/org/logicng/functions/FormulaDepthFunctionTest.java index 7110a076..7f9f235a 100644 --- a/core/src/test/java/org/logicng/functions/FormulaDepthFunctionTest.java +++ b/core/src/test/java/org/logicng/functions/FormulaDepthFunctionTest.java @@ -36,7 +36,6 @@ import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Variable; import org.logicng.formulas.cache.FunctionCacheEntry; -import org.logicng.io.parsers.ParserException; /** * Unit Tests for the class {@link FormulaDepthFunction}. @@ -89,9 +88,9 @@ public void testDeeperFormulas() { } @Test - public void testCache() throws ParserException { + public void testCache() { final FormulaFactory f = new FormulaFactory(); - final Formula formula = f.parse("A & B | C"); + final Formula formula = parse(f, "A & B | C"); assertThat(formula.functionCacheEntry(FunctionCacheEntry.DEPTH)).isNull(); assertThat(formula.apply(FormulaDepthFunction.get())).isEqualTo(2); assertThat(formula.functionCacheEntry(FunctionCacheEntry.DEPTH)).isEqualTo(2); diff --git a/core/src/test/java/org/logicng/functions/MinimumPrimeImplicantTest.java b/core/src/test/java/org/logicng/functions/MinimumPrimeImplicantTest.java index b507671d..75e791a5 100644 --- a/core/src/test/java/org/logicng/functions/MinimumPrimeImplicantTest.java +++ b/core/src/test/java/org/logicng/functions/MinimumPrimeImplicantTest.java @@ -29,6 +29,7 @@ package org.logicng.functions; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.logicng.cardinalityconstraints.CCConfig; @@ -57,65 +58,65 @@ public MinimumPrimeImplicantTest() { } @Test - public void testSimpleCases() throws ParserException { - Formula formula = this.f.parse("a"); + public void testSimpleCases() { + Formula formula = parse(this.f, "a"); SortedSet pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(1); isPrimeImplicant(formula, pi); - formula = this.f.parse("a | b | c"); + formula = parse(this.f, "a | b | c"); pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(1); isPrimeImplicant(formula, pi); - formula = this.f.parse("a & b & (~a|~b)"); + formula = parse(this.f, "a & b & (~a|~b)"); pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).isNull(); - formula = this.f.parse("a & b & c"); + formula = parse(this.f, "a & b & c"); pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(3); isPrimeImplicant(formula, pi); - formula = this.f.parse("a | b | ~c => e & d & f"); + formula = parse(this.f, "a | b | ~c => e & d & f"); pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(3); isPrimeImplicant(formula, pi); - formula = this.f.parse("a | b | ~c <=> e & d & f"); + formula = parse(this.f, "a | b | ~c <=> e & d & f"); pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(4); isPrimeImplicant(formula, pi); - formula = this.f.parse("(a | b | ~c <=> e & d & f) | (a | b | ~c => e & d & f)"); + formula = parse(this.f, "(a | b | ~c <=> e & d & f) | (a | b | ~c => e & d & f)"); pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(3); isPrimeImplicant(formula, pi); - formula = this.f.parse("(a | b | ~c <=> e & d & f) | (a | b | ~c => e & d & f) | (a & b)"); + formula = parse(this.f, "(a | b | ~c <=> e & d & f) | (a | b | ~c => e & d & f) | (a & b)"); pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(2); isPrimeImplicant(formula, pi); - formula = this.f.parse("(a | b | ~c <=> e & d & f) | (a | b | ~c => e & d & f) | (a & b) | (f => g)"); + formula = parse(this.f, "(a | b | ~c <=> e & d & f) | (a | b | ~c => e & d & f) | (a & b) | (f => g)"); pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(1); isPrimeImplicant(formula, pi); } @Test - public void testSmallExamples() throws ParserException { - Formula formula = this.f.parse("(~(v17 | v18) | ~v1494 & (v17 | v18)) & ~v687 => v686"); + public void testSmallExamples() { + Formula formula = parse(this.f, "(~(v17 | v18) | ~v1494 & (v17 | v18)) & ~v687 => v686"); SortedSet pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(1); isPrimeImplicant(formula, pi); - formula = this.f.parse("(~(v17 | v18) | ~v1494 & (v17 | v18)) & v687 => ~v686"); + formula = parse(this.f, "(~(v17 | v18) | ~v1494 & (v17 | v18)) & v687 => ~v686"); pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(1); isPrimeImplicant(formula, pi); - formula = this.f.parse("v173 + v174 + v451 + v258 + v317 + v259 + v452 + v453 + v175 + v176 + v177 + v178 + v179 + v180 + v181 + v182 + v183 + v102 + v103 + v104 + v105 = 1"); + formula = parse(this.f, "v173 + v174 + v451 + v258 + v317 + v259 + v452 + v453 + v175 + v176 + v177 + v178 + v179 + v180 + v181 + v182 + v183 + v102 + v103 + v104 + v105 = 1"); pi = formula.apply(MinimumPrimeImplicantFunction.get()); assertThat(pi).hasSize(21); isPrimeImplicant(formula, pi); diff --git a/core/src/test/java/org/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java b/core/src/test/java/org/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java index e4a48007..3b4246a6 100644 --- a/core/src/test/java/org/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java +++ b/core/src/test/java/org/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java @@ -155,8 +155,7 @@ public void testFormulaSplit() throws IOException, ParserException { @Test public void testFormulaSplitIllegal() { final FormulaFactory f = new FormulaFactory(); - @SuppressWarnings("deprecation") - final Graph graph = ConstraintGraphGenerator.generateFromCnf(f.variable("B")); + @SuppressWarnings("deprecation") 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/core/src/test/java/org/logicng/graphs/io/conditions/ContainsCondition.java b/core/src/test/java/org/logicng/graphs/io/conditions/ContainsCondition.java index 52c2c317..1f18d818 100644 --- a/core/src/test/java/org/logicng/graphs/io/conditions/ContainsCondition.java +++ b/core/src/test/java/org/logicng/graphs/io/conditions/ContainsCondition.java @@ -33,7 +33,7 @@ import java.util.List; /** - * A condition needed for AssertJ-Assertions for {@link org.logicng.graphs.io.GraphDotFileWriterTest} and {@link org.logicng.graphs.io.GraphDimacsFileWriterTest}. + * A condition needed for AssertJ-Assertions for {@link org.logicng.graphs.io.GraphDimacsFileWriterTest}. * @version 1.2 * @since 1.2 */ diff --git a/core/src/test/java/org/logicng/handlers/TimeoutBDDHandlerTest.java b/core/src/test/java/org/logicng/handlers/TimeoutBDDHandlerTest.java index 57b2bcd7..920f6e46 100644 --- a/core/src/test/java/org/logicng/handlers/TimeoutBDDHandlerTest.java +++ b/core/src/test/java/org/logicng/handlers/TimeoutBDDHandlerTest.java @@ -1,6 +1,7 @@ package org.logicng.handlers; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import static org.mockito.Mockito.atLeast; import static org.mockito.Mockito.times; import static org.mockito.Mockito.verify; @@ -11,7 +12,6 @@ import org.junit.jupiter.api.extension.ExtendWith; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.knowledgecompilation.bdds.BDD; import org.logicng.knowledgecompilation.bdds.BDDFactory; import org.logicng.knowledgecompilation.bdds.jbuddy.BDDKernel; @@ -45,8 +45,8 @@ public void testNewRefAdded() throws InterruptedException { } @Test - public void testThatMethodsAreCalled() throws ParserException { - final Formula formula = f.parse("(A => ~B) & ((A & C) | (D & ~C)) & (A | Y | X)"); + public void testThatMethodsAreCalled() { + final Formula formula = parse(this.f, "(A => ~B) & ((A & C) | (D & ~C)) & (A | Y | X)"); final VariableOrderingProvider provider = VariableOrdering.BFS.provider(); final BDDKernel kernel = new BDDKernel(this.f, provider.getOrder(formula), 100, 100); final TimeoutBDDHandler handler = Mockito.mock(TimeoutBDDHandler.class); @@ -58,8 +58,8 @@ public void testThatMethodsAreCalled() throws ParserException { } @Test - public void testThatNewRefAddedHandledProperly() throws ParserException { - final Formula formula = f.parse("(A => ~B) & ((A & C) | ~(D & ~C)) & (A | Y | X)"); + public void testThatNewRefAddedHandledProperly() { + final Formula formula = parse(this.f, "(A => ~B) & ((A & C) | ~(D & ~C)) & (A | Y | X)"); final VariableOrderingProvider provider = VariableOrdering.BFS.provider(); final BDDKernel kernel = new BDDKernel(this.f, provider.getOrder(formula), 100, 100); final TimeoutBDDHandler handler = Mockito.mock(TimeoutBDDHandler.class); @@ -76,7 +76,7 @@ public void testThatNewRefAddedHandledProperly() throws ParserException { @Test public void testTimeoutHandlerSingleTimeout() { - final Formula formula = pg.generate(10); + final Formula formula = this.pg.generate(10); final VariableOrderingProvider provider = VariableOrdering.BFS.provider(); final BDDKernel kernel = new BDDKernel(this.f, provider.getOrder(formula), 100, 100); final TimeoutBDDHandler handler = new TimeoutBDDHandler(100L); @@ -89,7 +89,7 @@ public void testTimeoutHandlerSingleTimeout() { @Test public void testTimeoutHandlerFixedEnd() { - final Formula formula = pg.generate(10); + final Formula formula = this.pg.generate(10); final VariableOrderingProvider provider = VariableOrdering.BFS.provider(); final BDDKernel kernel = new BDDKernel(this.f, provider.getOrder(formula), 100, 100); final TimeoutBDDHandler handler = new TimeoutBDDHandler(System.currentTimeMillis() + 100L, TimeoutHandler.TimerType.FIXED_END); diff --git a/core/src/test/java/org/logicng/handlers/TimeoutMaxSATHandlerTest.java b/core/src/test/java/org/logicng/handlers/TimeoutMaxSATHandlerTest.java index 8724e6c1..2d26f0d4 100644 --- a/core/src/test/java/org/logicng/handlers/TimeoutMaxSATHandlerTest.java +++ b/core/src/test/java/org/logicng/handlers/TimeoutMaxSATHandlerTest.java @@ -1,6 +1,7 @@ package org.logicng.handlers; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import static org.mockito.ArgumentMatchers.any; import static org.mockito.ArgumentMatchers.anyInt; import static org.mockito.Mockito.atLeast; @@ -15,7 +16,6 @@ import org.logicng.datastructures.Assignment; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.io.readers.DimacsReader; import org.logicng.solvers.MaxSATSolver; import org.logicng.solvers.maxsat.algorithms.MaxSAT; @@ -67,12 +67,12 @@ public void testTimeoutForUpperBound() throws InterruptedException { } @Test - public void testThatMethodsAreCalled() throws ParserException { + public void testThatMethodsAreCalled() { for (final MaxSATSolver solver : this.solvers) { final int weight = solver.isWeighted() ? 2 : 1; - solver.addHardFormula(this.f.parse("A&B")); - solver.addSoftFormula(this.f.parse("~A"), weight); - solver.addSoftFormula(this.f.parse("~B"), weight); + solver.addHardFormula(parse(this.f, "A&B")); + solver.addSoftFormula(parse(this.f, "~A"), weight); + solver.addSoftFormula(parse(this.f, "~B"), weight); final TimeoutMaxSATHandler handler = Mockito.mock(TimeoutMaxSATHandler.class); solver.solve(handler); diff --git a/core/src/test/java/org/logicng/handlers/TimeoutModelEnumerationHandlerTest.java b/core/src/test/java/org/logicng/handlers/TimeoutModelEnumerationHandlerTest.java index b02d2f9a..22072b5c 100644 --- a/core/src/test/java/org/logicng/handlers/TimeoutModelEnumerationHandlerTest.java +++ b/core/src/test/java/org/logicng/handlers/TimeoutModelEnumerationHandlerTest.java @@ -1,6 +1,7 @@ package org.logicng.handlers; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import static org.mockito.ArgumentMatchers.any; import static org.mockito.Mockito.lenient; import static org.mockito.Mockito.times; @@ -13,7 +14,6 @@ import org.logicng.datastructures.Assignment; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; import org.logicng.solvers.functions.ModelEnumerationFunction; @@ -36,7 +36,7 @@ class TimeoutModelEnumerationHandlerTest { @BeforeEach public void init() { this.f = new FormulaFactory(); - this.pg = new PigeonHoleGenerator(f); + this.pg = new PigeonHoleGenerator(this.f); this.solvers = new SATSolver[8]; this.solvers[0] = MiniSat.miniSat(this.f, MiniSatConfig.builder().incremental(true).build()); this.solvers[1] = MiniSat.miniSat(this.f, MiniSatConfig.builder().incremental(false).build()); @@ -59,8 +59,8 @@ public void testFoundModel() throws InterruptedException { } @Test - public void testThatMethodsAreCalled() throws ParserException { - final Formula formula = f.parse("A & B | C"); + public void testThatMethodsAreCalled() { + final Formula formula = parse(this.f, "A & B | C"); for (final SATSolver solver : this.solvers) { solver.add(formula); final TimeoutModelEnumerationHandler handler = Mockito.mock(TimeoutModelEnumerationHandler.class); @@ -75,7 +75,7 @@ public void testThatMethodsAreCalled() throws ParserException { @Test public void testThatSatHandlerIsHandledProperly() { - final Formula formula = pg.generate(10).negate(); + final Formula formula = this.pg.generate(10).negate(); for (final SATSolver solver : this.solvers) { solver.add(formula); final TimeoutSATHandler satHandler = Mockito.mock(TimeoutSATHandler.class); @@ -99,7 +99,7 @@ public void testThatSatHandlerIsHandledProperly() { @Test public void testTimeoutHandlerSingleTimeout() { - final Formula formula = pg.generate(10).negate(); + final Formula formula = this.pg.generate(10).negate(); for (final SATSolver solver : this.solvers) { solver.add(formula); final TimeoutModelEnumerationHandler handler = new TimeoutModelEnumerationHandler(100L); @@ -114,7 +114,7 @@ public void testTimeoutHandlerSingleTimeout() { @Test public void testTimeoutHandlerFixedEnd() { - final Formula formula = pg.generate(10).negate(); + final Formula formula = this.pg.generate(10).negate(); for (final SATSolver solver : this.solvers) { solver.add(formula); final TimeoutModelEnumerationHandler handler = new TimeoutModelEnumerationHandler(System.currentTimeMillis() + 100L, TimeoutHandler.TimerType.FIXED_END); diff --git a/core/src/test/java/org/logicng/handlers/TimeoutOptimizationHandlerTest.java b/core/src/test/java/org/logicng/handlers/TimeoutOptimizationHandlerTest.java index e6d5bfda..2161b0fe 100644 --- a/core/src/test/java/org/logicng/handlers/TimeoutOptimizationHandlerTest.java +++ b/core/src/test/java/org/logicng/handlers/TimeoutOptimizationHandlerTest.java @@ -1,6 +1,7 @@ package org.logicng.handlers; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import static org.mockito.Mockito.atLeast; import static org.mockito.Mockito.times; import static org.mockito.Mockito.verify; @@ -11,7 +12,6 @@ import org.logicng.datastructures.Assignment; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.io.readers.DimacsReader; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; @@ -56,8 +56,8 @@ public void testTimeoutFoundBetterBound() throws InterruptedException { } @Test - public void testThatMethodsAreCalled() throws ParserException { - final Formula formula = f.parse("a & b & (~a => b)"); + public void testThatMethodsAreCalled() { + final Formula formula = parse(this.f, "a & b & (~a => b)"); for (final SATSolver solver : this.solvers) { solver.add(formula); final TimeoutOptimizationHandler handler = Mockito.mock(TimeoutOptimizationHandler.class); diff --git a/core/src/test/java/org/logicng/handlers/TimeoutSATHandlerTest.java b/core/src/test/java/org/logicng/handlers/TimeoutSATHandlerTest.java index 0964d201..31425d69 100644 --- a/core/src/test/java/org/logicng/handlers/TimeoutSATHandlerTest.java +++ b/core/src/test/java/org/logicng/handlers/TimeoutSATHandlerTest.java @@ -1,6 +1,7 @@ package org.logicng.handlers; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import static org.mockito.Mockito.atLeast; import static org.mockito.Mockito.times; import static org.mockito.Mockito.verify; @@ -11,7 +12,6 @@ import org.junit.jupiter.api.extension.ExtendWith; import org.logicng.datastructures.Tristate; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; import org.logicng.solvers.sat.GlucoseConfig; @@ -55,9 +55,9 @@ public void testDetectedConflict() throws InterruptedException { } @Test - public void testThatMethodsAreCalled() throws ParserException { + public void testThatMethodsAreCalled() { for (final SATSolver solver : this.solvers) { - solver.add(this.f.parse("(x => y) & (~x => y) & (y => z) & (z => ~y)")); + solver.add(parse(this.f, "(x => y) & (~x => y) & (y => z) & (z => ~y)")); final TimeoutSATHandler handler = Mockito.mock(TimeoutSATHandler.class); solver.sat(handler); @@ -71,7 +71,7 @@ public void testThatMethodsAreCalled() throws ParserException { @Test public void testThatDetectedConflictIsHandledProperly() { for (final SATSolver solver : this.solvers) { - solver.add(pg.generate(10)); + solver.add(this.pg.generate(10)); final TimeoutSATHandler handler = Mockito.mock(TimeoutSATHandler.class); final AtomicInteger count = new AtomicInteger(0); when(handler.detectedConflict()).then(invocationOnMock -> count.addAndGet(1) < 5); @@ -89,7 +89,7 @@ public void testThatDetectedConflictIsHandledProperly() { @Test public void testTimeoutHandlerSingleTimeout() { for (final SATSolver solver : this.solvers) { - solver.add(pg.generate(10)); + solver.add(this.pg.generate(10)); final TimeoutSATHandler handler = new TimeoutSATHandler(100L); final Tristate result = solver.sat(handler); @@ -102,7 +102,7 @@ public void testTimeoutHandlerSingleTimeout() { @Test public void testTimeoutHandlerFixedEnd() { for (final SATSolver solver : this.solvers) { - solver.add(pg.generate(10)); + solver.add(this.pg.generate(10)); final TimeoutSATHandler handler = new TimeoutSATHandler(System.currentTimeMillis() + 100L, TimeoutHandler.TimerType.FIXED_END); final Tristate result = solver.sat(handler); diff --git a/core/src/test/java/org/logicng/io/FormulaWriterReaderTest.java b/core/src/test/java/org/logicng/io/FormulaWriterReaderTest.java index 96aee91e..ad98e38c 100644 --- a/core/src/test/java/org/logicng/io/FormulaWriterReaderTest.java +++ b/core/src/test/java/org/logicng/io/FormulaWriterReaderTest.java @@ -57,7 +57,7 @@ public class FormulaWriterReaderTest { @Test - public void testSimpleFormulaOneLine() throws ParserException, IOException { + public void testSimpleFormulaOneLine() throws IOException, ParserException { final String fileName = "src/test/resources/writers/temp/simple_formula1.txt"; final File file = new File(fileName); final FormulaFactory f = new FormulaFactory(); @@ -79,7 +79,7 @@ public void testSimpleFormulaOneLine() throws ParserException, IOException { } @Test - public void testSimpleFormulaMultiLine() throws ParserException, IOException { + public void testSimpleFormulaMultiLine() throws IOException, ParserException { final String fileName = "src/test/resources/writers/temp/simple_formula2.txt"; final File file = new File(fileName); final FormulaFactory f = new FormulaFactory(); @@ -99,7 +99,7 @@ public void testSimpleFormulaMultiLine() throws ParserException, IOException { } @Test - public void testPBFormulaOneLine() throws ParserException, IOException { + public void testPBFormulaOneLine() throws IOException, ParserException { final String fileName = "src/test/resources/writers/temp/simple_formula3.txt"; final File file = new File(fileName); final FormulaFactory f = new FormulaFactory(); @@ -121,7 +121,7 @@ public void testPBFormulaOneLine() throws ParserException, IOException { } @Test - public void testPBFormulaMultiLine() throws ParserException, IOException { + public void testPBFormulaMultiLine() throws IOException, ParserException { final String fileName = "src/test/resources/writers/temp/simple_formula4.txt"; final File file = new File(fileName); final FormulaFactory f = new FormulaFactory(); @@ -141,7 +141,7 @@ public void testPBFormulaMultiLine() throws ParserException, IOException { } @Test - public void testSimpleFormulaOneLineFormatter() throws ParserException, IOException { + public void testSimpleFormulaOneLineFormatter() throws IOException, ParserException { final String fileName = "src/test/resources/writers/temp/simple_formula5.txt"; final File file = new File(fileName); final FormulaFactory f = new FormulaFactory(); @@ -154,7 +154,7 @@ public void testSimpleFormulaOneLineFormatter() throws ParserException, IOExcept } @Test - public void testSimpleFormulaMultiLineFormatter() throws ParserException, IOException { + public void testSimpleFormulaMultiLineFormatter() throws IOException, ParserException { final String fileName = "src/test/resources/writers/temp/simple_formula6.txt"; final File file = new File(fileName); final FormulaFactory f = new FormulaFactory(); diff --git a/core/src/test/java/org/logicng/io/graphical/generators/BddGraphicalGeneratorTest.java b/core/src/test/java/org/logicng/io/graphical/generators/BddGraphicalGeneratorTest.java index ee4edb98..e739a487 100644 --- a/core/src/test/java/org/logicng/io/graphical/generators/BddGraphicalGeneratorTest.java +++ b/core/src/test/java/org/logicng/io/graphical/generators/BddGraphicalGeneratorTest.java @@ -84,7 +84,7 @@ public void testFormulas() throws IOException, ParserException { } @Test - public void testFixedStyle() throws ParserException, IOException { + public void testFixedStyle() throws IOException, ParserException { final FormulaFactory f = new FormulaFactory(); final PropositionalParser p = new PropositionalParser(f); final List ordering = Arrays.asList(f.variable("A"), f.variable("B"), f.variable("C"), f.variable("D")); @@ -104,7 +104,7 @@ public void testFixedStyle() throws ParserException, IOException { } @Test - public void testDynamic() throws ParserException, IOException { + public void testDynamic() throws IOException, ParserException { final FormulaFactory f = new FormulaFactory(); final PropositionalParser p = new PropositionalParser(f); final List ordering = Arrays.asList(f.variable("A"), f.variable("B"), f.variable("C"), f.variable("D")); diff --git a/core/src/test/java/org/logicng/io/graphical/generators/FormulaAstGraphicalGeneratorTest.java b/core/src/test/java/org/logicng/io/graphical/generators/FormulaAstGraphicalGeneratorTest.java index 664ab322..771f5a15 100644 --- a/core/src/test/java/org/logicng/io/graphical/generators/FormulaAstGraphicalGeneratorTest.java +++ b/core/src/test/java/org/logicng/io/graphical/generators/FormulaAstGraphicalGeneratorTest.java @@ -100,7 +100,7 @@ public void testFormulas() throws IOException, ParserException { } @Test - public void testDuplicateFormulaParts() throws ParserException, IOException { + public void testDuplicateFormulaParts() throws IOException, ParserException { final Formula f6 = this.p.parse("(a & b) | (c & ~(a & b))"); testFiles("f6", f6, FormulaAstGraphicalGenerator.builder().build()); final Formula f7 = this.p.parse("(c & d) | (a & b) | ((c & d) <=> (a & b))"); @@ -108,7 +108,7 @@ public void testDuplicateFormulaParts() throws ParserException, IOException { } @Test - public void testFixedStyle() throws ParserException, IOException { + public void testFixedStyle() throws IOException, ParserException { final Formula f8 = this.p.parse("(A <=> B & (~A | C | X)) => a + b + c <= 2"); final FormulaAstGraphicalGenerator generator = FormulaAstGraphicalGenerator.builder() .backgroundColor("#020202") @@ -120,7 +120,7 @@ public void testFixedStyle() throws ParserException, IOException { } @Test - public void testDynamicStyle() throws ParserException, IOException { + public void testDynamicStyle() throws IOException, ParserException { final Formula f9 = this.p.parse("(A <=> B & (~A | C | X)) => a + b + c <= 2 & (~a | d => X & ~B)"); final GraphicalNodeStyle style1 = GraphicalNodeStyle.rectangle(GRAY_DARK, GRAY_DARK, GRAY_LIGHT); @@ -149,7 +149,7 @@ public void testDynamicStyle() throws ParserException, IOException { } @Test - public void testEdgeMapper() throws ParserException, IOException { + public void testEdgeMapper() throws IOException, ParserException { final Formula f10 = this.p.parse("(A <=> B & (~A | C | X)) => a + b + c <= 2 & (~a | d => X & ~B)"); final GraphicalEdgeStyle style1 = GraphicalEdgeStyle.dotted(GRAY_DARK); @@ -172,7 +172,7 @@ public void testEdgeMapper() throws ParserException, IOException { } @Test - public void testWithLabelMapper() throws ParserException, IOException { + public void testWithLabelMapper() throws IOException, ParserException { final Formula f8 = this.p.parse("(A <=> B & (~A | C | X)) => a + b + c <= 2"); final FormulaAstGraphicalGenerator generator = FormulaAstGraphicalGenerator.builder() .backgroundColor("#020202") diff --git a/core/src/test/java/org/logicng/io/graphical/generators/FormulaDagGraphicalGeneratorTest.java b/core/src/test/java/org/logicng/io/graphical/generators/FormulaDagGraphicalGeneratorTest.java index 4166755a..790f9072 100644 --- a/core/src/test/java/org/logicng/io/graphical/generators/FormulaDagGraphicalGeneratorTest.java +++ b/core/src/test/java/org/logicng/io/graphical/generators/FormulaDagGraphicalGeneratorTest.java @@ -100,7 +100,7 @@ public void testFormulas() throws IOException, ParserException { } @Test - public void testDuplicateFormulaParts() throws ParserException, IOException { + public void testDuplicateFormulaParts() throws IOException, ParserException { final Formula f6 = this.p.parse("(a & b) | (c & ~(a & b))"); testFiles("f6", f6, FormulaDagGraphicalGenerator.builder().build()); final Formula f7 = this.p.parse("(c & d) | (a & b) | ((c & d) <=> (a & b))"); @@ -108,7 +108,7 @@ public void testDuplicateFormulaParts() throws ParserException, IOException { } @Test - public void testFixedStyle() throws ParserException, IOException { + public void testFixedStyle() throws IOException, ParserException { final Formula f8 = this.p.parse("(A <=> B & (~A | C | X)) => a + b + c <= 2"); final FormulaDagGraphicalGenerator generator = FormulaDagGraphicalGenerator.builder() .backgroundColor("#020202") @@ -120,7 +120,7 @@ public void testFixedStyle() throws ParserException, IOException { } @Test - public void testDynamicStyle() throws ParserException, IOException { + public void testDynamicStyle() throws IOException, ParserException { final Formula f9 = this.p.parse("(A <=> B & (~A | C | X)) => a + b + c <= 2 & (~a | d => X & ~B)"); final GraphicalNodeStyle style1 = GraphicalNodeStyle.rectangle(GRAY_DARK, GRAY_DARK, GRAY_LIGHT); @@ -149,7 +149,7 @@ public void testDynamicStyle() throws ParserException, IOException { } @Test - public void testEdgeMapper() throws ParserException, IOException { + public void testEdgeMapper() throws IOException, ParserException { final Formula f10 = this.p.parse("(A <=> B & (~A | C | X)) => a + b + c <= 2 & (~a | d => X & ~B)"); final GraphicalEdgeStyle style1 = GraphicalEdgeStyle.dotted(GRAY_DARK); diff --git a/core/src/test/java/org/logicng/io/writers/FormulaDimacsFileWriterTest.java b/core/src/test/java/org/logicng/io/writers/FormulaDimacsFileWriterTest.java index 5316bfce..927ba190 100644 --- a/core/src/test/java/org/logicng/io/writers/FormulaDimacsFileWriterTest.java +++ b/core/src/test/java/org/logicng/io/writers/FormulaDimacsFileWriterTest.java @@ -90,7 +90,7 @@ public void testFormulas() throws IOException, ParserException { } @Test - public void testDuplicateFormulaParts() throws ParserException, IOException { + public void testDuplicateFormulaParts() throws IOException, ParserException { final Formula f6 = this.encoder.encode(this.p.parse("(a & b) | (c & ~(a & b))")); testFiles("f6", f6); final Formula f7 = this.encoder.encode(this.p.parse("(c & d) | (a & b) | ((c & d) <=> (a & b))")); diff --git a/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDConstructionTests.java b/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDConstructionTests.java index 5f7baa42..9ba6cc5f 100644 --- a/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDConstructionTests.java +++ b/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDConstructionTests.java @@ -29,13 +29,13 @@ package org.logicng.knowledgecompilation.bdds; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Variable; -import org.logicng.io.parsers.ParserException; import org.logicng.knowledgecompilation.bdds.jbuddy.BDDKernel; import java.util.List; @@ -56,12 +56,12 @@ public class BDDConstructionTests { BDD secondBdd; @BeforeEach - public void init() throws ParserException { + public void init() { this.f = new FormulaFactory(); this.variables = this.f.variables("a", "b", "c", "d", "e", "f", "g"); this.kernel = new BDDKernel(this.f, this.variables, 1000, 10000); - this.initFormula = this.f.parse("(a & b) => (c | d & ~e)"); - this.secondFormula = this.f.parse("(g & f) <=> (c | ~a | ~d)"); + this.initFormula = parse(this.f, "(a & b) => (c | d & ~e)"); + this.secondFormula = parse(this.f, "(g & f) <=> (c | ~a | ~d)"); this.initBdd = BDDFactory.build(this.initFormula, this.kernel); this.secondBdd = BDDFactory.build(this.secondFormula, this.kernel); } diff --git a/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDOperationsTest.java b/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDOperationsTest.java index 11a1b0b7..a19ae29c 100644 --- a/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDOperationsTest.java +++ b/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDOperationsTest.java @@ -29,6 +29,7 @@ package org.logicng.knowledgecompilation.bdds; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; @@ -87,7 +88,7 @@ public void init() throws ParserException { } @Test - public void testToFormula() throws ParserException { + public void testToFormula() { assertThat(this.bddVerum.toFormula()).isEqualTo(this.f.verum()); assertThat(this.bddFalsum.toFormula()).isEqualTo(this.f.falsum()); assertThat(this.bddPosLit.toFormula()).isEqualTo(this.f.literal("A", true)); @@ -101,12 +102,12 @@ public void testToFormula() throws ParserException { } @Test - public void testToFormulaStyles() throws ParserException { - final BDD bdd = BDDFactory.build(this.f.parse("~A | ~B | ~C"), this.kernel); - final Formula expFollowPathsToTrue = this.f.parse("~A | A & (~B | B & ~C)"); + public void testToFormulaStyles() { + final BDD bdd = BDDFactory.build(parse(this.f, "~A | ~B | ~C"), this.kernel); + final Formula expFollowPathsToTrue = parse(this.f, "~A | A & (~B | B & ~C)"); assertThat(bdd.toFormula()).isEqualTo(expFollowPathsToTrue); assertThat(bdd.toFormula(true)).isEqualTo(expFollowPathsToTrue); - assertThat(bdd.toFormula(false)).isEqualTo(this.f.parse("~(A & B & C)")); + assertThat(bdd.toFormula(false)).isEqualTo(parse(this.f, "~(A & B & C)")); } @RandomTag @@ -329,8 +330,8 @@ public void testVariableProfile() { assertThat(this.bddAnd.variableProfile()).containsExactly(a1, b1, c1); } - private void compareFormula(final BDD bdd, final String formula) throws ParserException { - compareFormula(bdd, bdd.kernel.factory().parse(formula)); + private void compareFormula(final BDD bdd, final String formula) { + compareFormula(bdd, parse(bdd.kernel.factory(), formula)); } private void compareFormula(final BDD bdd, final Formula compareFormula) { diff --git a/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java b/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java index 858f8f6d..f27986b6 100644 --- a/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java +++ b/core/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java @@ -37,7 +37,6 @@ import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Variable; -import org.logicng.io.parsers.ParserException; import org.logicng.knowledgecompilation.bdds.datastructures.BDDConstant; import org.logicng.knowledgecompilation.bdds.datastructures.BDDInnerNode; import org.logicng.knowledgecompilation.bdds.functions.LngBDDFunction; @@ -84,7 +83,7 @@ public void testExceptionalBehavior() { assertThatThrownBy(() -> { final BDDKernel kernel = new BDDKernel(this.f, Arrays.asList(this.A, this.B), 100, 100); final BDDReordering reordering = new BDDReordering(kernel); - final Formula formula = this.f.parse("a | b"); + final Formula formula = parse(this.f, "a | b"); BDDFactory.build(formula, kernel); reordering.swapVariables(0, 2); }).isInstanceOf(IllegalArgumentException.class) @@ -92,7 +91,7 @@ public void testExceptionalBehavior() { assertThatThrownBy(() -> { final BDDKernel kernel = new BDDKernel(this.f, Arrays.asList(this.A, this.B), 100, 100); final BDDReordering reordering = new BDDReordering(kernel); - final Formula formula = this.f.parse("a | b"); + final Formula formula = parse(this.f, "a | b"); BDDFactory.build(formula, kernel); reordering.swapVariables(3, 0); }).isInstanceOf(IllegalArgumentException.class) @@ -100,9 +99,9 @@ public void testExceptionalBehavior() { } @Test - public void testSwapping() throws ParserException { + public void testSwapping() { final BDDKernel kernel = new BDDKernel(this.f, Arrays.asList(this.A, this.B, this.C), 100, 100); - final Formula formula = this.f.parse("a | b | c"); + final Formula formula = parse(this.f, "a | b | c"); final BDD bdd = BDDFactory.build(formula, kernel); assertThat(bdd.getVariableOrder()).containsExactly(this.A, this.B, this.C); kernel.swapVariables(this.A, this.B); @@ -126,10 +125,10 @@ public void testSwapping() throws ParserException { } @Test - public void testSwappingMultipleBdds() throws ParserException { + public void testSwappingMultipleBdds() { final BDDKernel kernel = new BDDKernel(this.f, Arrays.asList(this.A, this.B, this.C), 100, 100); - final Formula formula1 = this.f.parse("a | b | c"); - final Formula formula2 = this.f.parse("a & b"); + final Formula formula1 = parse(this.f, "a | b | c"); + final Formula formula2 = parse(this.f, "a & b"); final BDD bdd1 = BDDFactory.build(formula1, kernel); final BDD bdd2 = BDDFactory.build(formula2, kernel); assertThat(bdd1.getVariableOrder()).containsExactly(this.A, this.B, this.C); @@ -146,11 +145,11 @@ public void testSwappingMultipleBdds() throws ParserException { } @Test - public void testReorderingAndFormulaGeneration() throws ParserException { + public void testReorderingAndFormulaGeneration() { final List order = this.f.variables("a", "b", "c", "d", "e", "f"); - final Formula formula1 = this.f.parse("a & b <=> (~c | d) & f"); - final Formula formula2 = this.f.parse("a => c & ~d | e | f"); - final Formula formula3 = this.f.parse("a => b <=> (~a | d) & c | f"); + final Formula formula1 = parse(this.f, "a & b <=> (~c | d) & f"); + final Formula formula2 = parse(this.f, "a => c & ~d | e | f"); + final Formula formula3 = parse(this.f, "a => b <=> (~a | d) & c | f"); for (final BDDReorderingMethod method : REORDER_METHODS) { final BDDKernel kernel = new BDDKernel(this.f, order, 100, 100); @@ -167,32 +166,32 @@ public void testReorderingAndFormulaGeneration() throws ParserException { } @Test - public void testSwappingAndFormulaGeneration() throws ParserException { + public void testSwappingAndFormulaGeneration() { final List order = this.f.variables("a", "b", "c", "d", "e", "f"); - final Formula formula1 = this.f.parse("a | b | c"); - final Formula formula2 = this.f.parse("a => b & ~c | ~d"); - final Formula formula3 = this.f.parse("a & b <=> (~c | d) & f"); + final Formula formula1 = parse(this.f, "a | b | c"); + final Formula formula2 = parse(this.f, "a => b & ~c | ~d"); + final Formula formula3 = parse(this.f, "a & b <=> (~c | d) & f"); final BDDKernel kernel = new BDDKernel(this.f, order, 100, 100); final BDD bdd1 = BDDFactory.build(formula1, kernel); final BDD bdd2 = BDDFactory.build(formula2, kernel); - assertThat(bdd1.toFormula()).isEqualTo(this.f.parse("~a & (~b & c | b) | a")); - assertThat(bdd2.toFormula()).isEqualTo(this.f.parse("~a | a & (~b & ~d | b & (~c | c & ~d))")); + assertThat(bdd1.toFormula()).isEqualTo(parse(this.f, "~a & (~b & c | b) | a")); + assertThat(bdd2.toFormula()).isEqualTo(parse(this.f, "~a | a & (~b & ~d | b & (~c | c & ~d))")); kernel.swapVariables(this.f.variable("a"), this.f.variable("b")); // also affects bdd2 and upcoming bdd3 - assertThat(bdd1.toFormula()).isEqualTo(this.f.parse("~b & (~a & c | a) | b")); - assertThat(bdd2.toFormula()).isEqualTo(this.f.parse("~b & (~a | a & ~d) | b & (~a | a & (~c | c & ~d))")); + assertThat(bdd1.toFormula()).isEqualTo(parse(this.f, "~b & (~a & c | a) | b")); + assertThat(bdd2.toFormula()).isEqualTo(parse(this.f, "~b & (~a | a & ~d) | b & (~a | a & (~c | c & ~d))")); final BDD bdd3 = BDDFactory.build(formula3, kernel); - assertThat(bdd3.toFormula()).isEqualTo(this.f.parse("~b & (~c & ~f | c & (~d | d & ~f)) | b & (~a & (~c & ~f | c & (~d | d & ~f)) | a & (~c & f | c & d & f))")); + assertThat(bdd3.toFormula()).isEqualTo(parse(this.f, "~b & (~c & ~f | c & (~d | d & ~f)) | b & (~a & (~c & ~f | c & (~d | d & ~f)) | a & (~c & f | c & d & f))")); kernel.swapVariables(this.f.variable("a"), this.f.variable("d")); - assertThat(bdd1.toFormula()).isEqualTo(this.f.parse("~b & (~c & a | c) | b")); - assertThat(bdd2.toFormula()).isEqualTo(this.f.parse("~b & (~d | d & ~a) | b & (~d | d & (~c | c & ~a))")); - assertThat(bdd3.toFormula()).isEqualTo(this.f.parse("~b & (~d & (~c & ~f | c) | d & ~f) | b & (~d & (~c & (~a & ~f | a & f) | ~a & c) | d & (~a & ~f | a & f))")); + assertThat(bdd1.toFormula()).isEqualTo(parse(this.f, "~b & (~c & a | c) | b")); + assertThat(bdd2.toFormula()).isEqualTo(parse(this.f, "~b & (~d | d & ~a) | b & (~d | d & (~c | c & ~a))")); + assertThat(bdd3.toFormula()).isEqualTo(parse(this.f, "~b & (~d & (~c & ~f | c) | d & ~f) | b & (~d & (~c & (~a & ~f | a & f) | ~a & c) | d & (~a & ~f | a & f))")); } @Test diff --git a/core/src/test/java/org/logicng/knowledgecompilation/bdds/FormulaBDDTest.java b/core/src/test/java/org/logicng/knowledgecompilation/bdds/FormulaBDDTest.java index dd0d5c31..efb97a39 100644 --- a/core/src/test/java/org/logicng/knowledgecompilation/bdds/FormulaBDDTest.java +++ b/core/src/test/java/org/logicng/knowledgecompilation/bdds/FormulaBDDTest.java @@ -29,6 +29,7 @@ package org.logicng.knowledgecompilation.bdds; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.logicng.datastructures.Assignment; @@ -89,9 +90,9 @@ public void testBDDGeneration() throws ParserException { } @Test - public void testNonNnfs() throws ParserException { + public void testNonNnfs() { final FormulaFactory f = new FormulaFactory(); - assertThat(f.parse("A + 2*B - C = 1").bdd()).isNotNull(); - assertThat(f.parse("(A & B & C | D & E & F) & (A - 2*B -D <= 0) | (C + 3*D - F > 0)").bdd()).isNotNull(); + assertThat(parse(f, "A + 2*B - C = 1").bdd()).isNotNull(); + assertThat(parse(f, "(A & B & C | D & E & F) & (A - 2*B -D <= 0) | (C + 3*D - F > 0)").bdd()).isNotNull(); } } diff --git a/core/src/test/java/org/logicng/knowledgecompilation/bdds/LargeBDDTest.java b/core/src/test/java/org/logicng/knowledgecompilation/bdds/LargeBDDTest.java index 3bf2fc56..c76eebed 100644 --- a/core/src/test/java/org/logicng/knowledgecompilation/bdds/LargeBDDTest.java +++ b/core/src/test/java/org/logicng/knowledgecompilation/bdds/LargeBDDTest.java @@ -29,13 +29,13 @@ package org.logicng.knowledgecompilation.bdds; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.logicng.formulas.Formula; 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.testutils.NQueensGenerator; import org.logicng.testutils.PigeonHoleGenerator; @@ -142,9 +142,9 @@ public void testNumberOfNodesHandlerLarge() { } @Test - public void testNumberOfNodesHandler() throws ParserException { + public void testNumberOfNodesHandler() { final FormulaFactory f = new FormulaFactory(); - final Formula formula = f.parse("A <=> ~(B => C & F & G & ~H | A & D & ~E)"); + final Formula formula = parse(f, "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); diff --git a/core/src/test/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNodeTest.java b/core/src/test/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNodeTest.java index 48029cc5..4d50f0e1 100644 --- a/core/src/test/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNodeTest.java +++ b/core/src/test/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNodeTest.java @@ -32,7 +32,6 @@ import org.junit.jupiter.api.Test; import org.logicng.TestWithExampleFormulas; -import org.logicng.io.parsers.ParserException; /** * Unit tests for {@link DTreeNode}. @@ -42,8 +41,8 @@ public class DTreeNodeTest extends TestWithExampleFormulas { @Test - public void testToString() throws ParserException { - final DTreeNode node = new DTreeNode(new DTreeLeaf(1, this.f.parse("a | b")), new DTreeLeaf(2, this.f.parse("c | d"))); + public void testToString() { + final DTreeNode node = new DTreeNode(new DTreeLeaf(1, parse(this.f, "a | b")), new DTreeLeaf(2, parse(this.f, "c | d"))); assertThat(node.toString()).isEqualTo("DTreeNode: [DTreeLeaf: 1, a | b, DTreeLeaf: 2, c | d]"); } } diff --git a/core/src/test/java/org/logicng/modelcounting/ModelCounterTest.java b/core/src/test/java/org/logicng/modelcounting/ModelCounterTest.java index f74ef892..178f6dcb 100644 --- a/core/src/test/java/org/logicng/modelcounting/ModelCounterTest.java +++ b/core/src/test/java/org/logicng/modelcounting/ModelCounterTest.java @@ -42,7 +42,6 @@ import org.logicng.formulas.PBConstraint; import org.logicng.formulas.Variable; import org.logicng.handlers.DnnfCompilationHandler; -import org.logicng.io.parsers.ParserException; import org.logicng.io.readers.DimacsReader; import org.logicng.knowledgecompilation.bdds.orderings.VariableOrdering; import org.logicng.solvers.MiniSat; @@ -77,7 +76,7 @@ private SortedSet vars(final String... vars) { @Test public void testWrongArgument() { assertThrows(IllegalArgumentException.class, () -> - ModelCounter.count(Collections.singletonList(this.f.parse("a & b")), new TreeSet<>(Collections.singletonList(this.A)))); + ModelCounter.count(Collections.singletonList(parse(this.f, "a & b")), new TreeSet<>(Collections.singletonList(this.A)))); } @Test @@ -94,40 +93,40 @@ public void testConstants() { } @Test - public void testSimple() throws ParserException { - final Formula formula01 = this.f.parse("(~v1 => ~v0) | ~v1 | v0"); + public void testSimple() { + final Formula formula01 = parse(this.f, "(~v1 => ~v0) | ~v1 | v0"); assertThat(ModelCounter.count(Collections.singletonList(formula01), formula01.variables())).isEqualTo(BigInteger.valueOf(4)); - final List formulas02 = Arrays.asList(this.f.parse("(a & b) | ~b"), this.f.parse("a")); + final List formulas02 = Arrays.asList(parse(this.f, "(a & b) | ~b"), parse(this.f, "a")); assertThat(ModelCounter.count(formulas02, FormulaHelper.variables(formulas02))).isEqualTo(BigInteger.valueOf(2)); - final List formulas03 = Arrays.asList(this.f.parse("a & b & c"), this.f.parse("c & d")); + final List formulas03 = Arrays.asList(parse(this.f, "a & b & c"), parse(this.f, "c & d")); assertThat(ModelCounter.count(formulas03, FormulaHelper.variables(formulas03))).isEqualTo(BigInteger.valueOf(1)); } @Test - public void testAmoAndExo() throws ParserException { - final List formulas01 = Arrays.asList(this.f.parse("a & b"), this.f.parse("a + b + c + d <= 1")); + public void testAmoAndExo() { + final List formulas01 = Arrays.asList(parse(this.f, "a & b"), parse(this.f, "a + b + c + d <= 1")); assertThat(ModelCounter.count(formulas01, FormulaHelper.variables(formulas01))).isEqualTo(BigInteger.valueOf(0)); - final List formulas02 = Arrays.asList(this.f.parse("a & b & (a + b + c + d <= 1)"), this.f.parse("a | b")); + final List formulas02 = Arrays.asList(parse(this.f, "a & b & (a + b + c + d <= 1)"), parse(this.f, "a | b")); assertThat(ModelCounter.count(formulas02, FormulaHelper.variables(formulas02))).isEqualTo(BigInteger.valueOf(0)); - final List formulas03 = Arrays.asList(this.f.parse("a & (a + b + c + d <= 1)"), this.f.parse("a | b")); + final List formulas03 = Arrays.asList(parse(this.f, "a & (a + b + c + d <= 1)"), parse(this.f, "a | b")); assertThat(ModelCounter.count(formulas03, FormulaHelper.variables(formulas03))).isEqualTo(BigInteger.valueOf(1)); - final List formulas04 = Arrays.asList(this.f.parse("a & (a + b + c + d = 1)"), this.f.parse("a | b")); + final List formulas04 = Arrays.asList(parse(this.f, "a & (a + b + c + d = 1)"), parse(this.f, "a | b")); assertThat(ModelCounter.count(formulas04, FormulaHelper.variables(formulas04))).isEqualTo(BigInteger.valueOf(1)); } @Test - public void testNonAmoAndExo() throws ParserException { - final List formulas01 = Arrays.asList(this.f.parse("a & b"), this.f.parse("a + b + c + d = 2")); + public void testNonAmoAndExo() { + final List formulas01 = Arrays.asList(parse(this.f, "a & b"), parse(this.f, "a + b + c + d = 2")); assertThatThrownBy(() -> ModelCounter.count(formulas01, FormulaHelper.variables(formulas01))) .isInstanceOf(UnsupportedOperationException.class) .hasMessage("Pure encoding for a PBC of type other than AMO or EXO is currently not supported."); - final List formulas02 = Arrays.asList(this.f.parse("a & b"), this.f.parse("c | a & (b + c + d <= 4)")); + final List formulas02 = Arrays.asList(parse(this.f, "a & b"), parse(this.f, "c | a & (b + c + d <= 4)")); assertThatThrownBy(() -> ModelCounter.count(formulas02, FormulaHelper.variables(formulas02))) .isInstanceOf(UnsupportedOperationException.class) .hasMessage("Pure encoding for a PBC of type other than AMO or EXO is currently not supported."); diff --git a/core/src/test/java/org/logicng/predicates/ContainsPBCPredicateTest.java b/core/src/test/java/org/logicng/predicates/ContainsPBCPredicateTest.java index 1ac622e9..076c37ba 100644 --- a/core/src/test/java/org/logicng/predicates/ContainsPBCPredicateTest.java +++ b/core/src/test/java/org/logicng/predicates/ContainsPBCPredicateTest.java @@ -35,7 +35,6 @@ import org.logicng.TestWithExampleFormulas; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.util.FormulaRandomizer; import org.logicng.util.FormulaRandomizerConfig; @@ -61,26 +60,26 @@ public void testLiterals() { } @Test - public void testNot() throws ParserException { - assertThat(this.f.parse("~a").holds(this.predicate)).isFalse(); - assertThat(this.f.parse("~(a | b)").holds(this.predicate)).isFalse(); + public void testNot() { + assertThat(parse(this.f, "~a").holds(this.predicate)).isFalse(); + assertThat(parse(this.f, "~(a | b)").holds(this.predicate)).isFalse(); - assertThat(this.f.parse("~(a | (a + b = 3))").holds(this.predicate)).isTrue(); - assertThat(this.f.parse("~(a & ~(a + b = 3))").holds(this.predicate)).isTrue(); + assertThat(parse(this.f, "~(a | (a + b = 3))").holds(this.predicate)).isTrue(); + assertThat(parse(this.f, "~(a & ~(a + b = 3))").holds(this.predicate)).isTrue(); } @Test - public void testMixed() throws ParserException { - assertThat(this.f.parse("a => b").holds(this.predicate)).isFalse(); - assertThat(this.f.parse("a <=> b").holds(this.predicate)).isFalse(); - assertThat(this.f.parse("a => (b | c & ~(e | d))").holds(this.predicate)).isFalse(); - assertThat(this.f.parse("a <=> (b | c & ~(e | d))").holds(this.predicate)).isFalse(); + public void testMixed() { + assertThat(parse(this.f, "a => b").holds(this.predicate)).isFalse(); + assertThat(parse(this.f, "a <=> b").holds(this.predicate)).isFalse(); + assertThat(parse(this.f, "a => (b | c & ~(e | d))").holds(this.predicate)).isFalse(); + assertThat(parse(this.f, "a <=> (b | c & ~(e | d))").holds(this.predicate)).isFalse(); - assertThat(this.f.parse("a => (3*a + ~b <= 4)").holds(this.predicate)).isTrue(); - assertThat(this.f.parse("(3*a + ~b <= 4) <=> b").holds(this.predicate)).isTrue(); - assertThat(this.f.parse("a => (b | c & (3*a + ~b <= 4) & ~(e | d))").holds(this.predicate)).isTrue(); - assertThat(this.f.parse("a <=> (b | c & ~(e | (3*a + ~b <= 4) | d))").holds(this.predicate)).isTrue(); - assertThat(this.f.parse("3*a + ~b <= 4").holds(this.predicate)).isTrue(); + assertThat(parse(this.f, "a => (3*a + ~b <= 4)").holds(this.predicate)).isTrue(); + assertThat(parse(this.f, "(3*a + ~b <= 4) <=> b").holds(this.predicate)).isTrue(); + assertThat(parse(this.f, "a => (b | c & (3*a + ~b <= 4) & ~(e | d))").holds(this.predicate)).isTrue(); + assertThat(parse(this.f, "a <=> (b | c & ~(e | (3*a + ~b <= 4) | d))").holds(this.predicate)).isTrue(); + assertThat(parse(this.f, "3*a + ~b <= 4").holds(this.predicate)).isTrue(); } @Test diff --git a/core/src/test/java/org/logicng/predicates/EvaluatesToConstantPredicateTest.java b/core/src/test/java/org/logicng/predicates/EvaluatesToConstantPredicateTest.java index 098e8a7d..30f588fe 100644 --- a/core/src/test/java/org/logicng/predicates/EvaluatesToConstantPredicateTest.java +++ b/core/src/test/java/org/logicng/predicates/EvaluatesToConstantPredicateTest.java @@ -42,7 +42,6 @@ import org.logicng.formulas.Literal; import org.logicng.formulas.PBConstraint; import org.logicng.formulas.Variable; -import org.logicng.io.parsers.ParserException; import org.logicng.util.FormulaCornerCases; import org.logicng.util.FormulaRandomizer; import org.logicng.util.FormulaRandomizerConfig; @@ -123,166 +122,166 @@ public void testLiteralsToFalse() { } @Test - public void testNotToFalse() throws ParserException { - assertThat(this.f.parse("~~a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~~a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~~a").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~~~a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~~~a").holds(this.aToFalse)).isTrue(); - assertThat(this.f.parse("~~~a").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("~(a & b)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~(a & b)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~(a & b)").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~(~a & b)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~(~a & b)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~(~a & b)").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~(a & ~b)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~(a & ~b)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~(a & ~b)").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("~(~a & ~b)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~(~a & ~b)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~(~a & ~b)").holds(this.aNotBToFalse)).isFalse(); + public void testNotToFalse() { + assertThat(parse(this.f, "~~a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~~a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~~a").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~~~a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~~~a").holds(this.aToFalse)).isTrue(); + assertThat(parse(this.f, "~~~a").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "~(a & b)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~(a & b)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~(a & b)").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~(~a & b)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~(~a & b)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~(~a & b)").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~(a & ~b)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~(a & ~b)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~(a & ~b)").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "~(~a & ~b)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~(~a & ~b)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~(~a & ~b)").holds(this.aNotBToFalse)).isFalse(); } @Test - public void testAndToFalse() throws ParserException { - assertThat(this.f.parse("a & ~a").holds(this.emptyToFalse)).isTrue(); - assertThat(this.f.parse("a & ~a").holds(this.aToFalse)).isTrue(); - assertThat(this.f.parse("a & ~a").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("a & b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a & b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a & b").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("~a & b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a & b").holds(this.aToFalse)).isTrue(); - assertThat(this.f.parse("~a & b").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("a & ~b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a & ~b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a & ~b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~a & ~b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a & ~b").holds(this.aToFalse)).isTrue(); - assertThat(this.f.parse("~a & ~b").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("~a & ~b & c & ~d").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a & ~b & c & ~d").holds(this.aToFalse)).isTrue(); - assertThat(this.f.parse("~a & ~b & c & ~d").holds(this.aNotBToFalse)).isTrue(); + public void testAndToFalse() { + assertThat(parse(this.f, "a & ~a").holds(this.emptyToFalse)).isTrue(); + assertThat(parse(this.f, "a & ~a").holds(this.aToFalse)).isTrue(); + assertThat(parse(this.f, "a & ~a").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "a & b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a & b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a & b").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "~a & b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a & b").holds(this.aToFalse)).isTrue(); + assertThat(parse(this.f, "~a & b").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "a & ~b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a & ~b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a & ~b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~a & ~b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a & ~b").holds(this.aToFalse)).isTrue(); + assertThat(parse(this.f, "~a & ~b").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "~a & ~b & c & ~d").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a & ~b & c & ~d").holds(this.aToFalse)).isTrue(); + assertThat(parse(this.f, "~a & ~b & c & ~d").holds(this.aNotBToFalse)).isTrue(); } @Test - public void testOrToFalse() throws ParserException { - assertThat(this.f.parse("a | b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a | b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a | b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~a | b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a | b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~a | b").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("a | ~b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a | ~b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a | ~b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~a | ~b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a | ~b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~a | ~b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~a | ~b | c | ~d").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a | ~b | c | ~d").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~a | ~b | c | ~d").holds(this.aNotBToFalse)).isFalse(); + public void testOrToFalse() { + assertThat(parse(this.f, "a | b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a | b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a | b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~a | b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a | b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~a | b").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "a | ~b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a | ~b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a | ~b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~a | ~b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a | ~b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~a | ~b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~a | ~b | c | ~d").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a | ~b | c | ~d").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~a | ~b | c | ~d").holds(this.aNotBToFalse)).isFalse(); } @Test - public void testImplicationToFalse() throws ParserException { - assertThat(this.f.parse("a => a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a => a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a => a").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("b => b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("b => b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("b => b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("a => b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a => b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a => b").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("~a => b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a => b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~a => b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("a => ~b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a => ~b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a => ~b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~a => ~b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a => ~b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~a => ~b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("b => a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("b => a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("b => a").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~b => a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~b => a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~b => a").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("b => ~a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("b => ~a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("b => ~a").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~b => ~a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~b => ~a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~b => ~a").holds(this.aNotBToFalse)).isTrue(); + public void testImplicationToFalse() { + assertThat(parse(this.f, "a => a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a => a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a => a").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "b => b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "b => b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "b => b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "a => b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a => b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a => b").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "~a => b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a => b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~a => b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "a => ~b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a => ~b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a => ~b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~a => ~b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a => ~b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~a => ~b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "b => a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "b => a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "b => a").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~b => a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~b => a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~b => a").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "b => ~a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "b => ~a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "b => ~a").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~b => ~a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~b => ~a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~b => ~a").holds(this.aNotBToFalse)).isTrue(); } @Test - public void testEquivalenceToFalse() throws ParserException { - assertThat(this.f.parse("a <=> a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a <=> a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a <=> a").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("b <=> b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("b <=> b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("b <=> b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("a <=> b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a <=> b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a <=> b").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("~a <=> b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a <=> b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~a <=> b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("a <=> ~b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a <=> ~b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a <=> ~b").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~a <=> ~b").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a <=> ~b").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~a <=> ~b").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("b <=> a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("b <=> a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("b <=> a").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("~b <=> a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~b <=> a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~b <=> a").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("b <=> ~a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("b <=> ~a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("b <=> ~a").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("~b <=> ~a").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~b <=> ~a").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("~b <=> ~a").holds(this.aNotBToFalse)).isTrue(); + public void testEquivalenceToFalse() { + assertThat(parse(this.f, "a <=> a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a <=> a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a <=> a").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "b <=> b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "b <=> b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "b <=> b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "a <=> b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a <=> b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a <=> b").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "~a <=> b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a <=> b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~a <=> b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "a <=> ~b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a <=> ~b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a <=> ~b").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~a <=> ~b").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a <=> ~b").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~a <=> ~b").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "b <=> a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "b <=> a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "b <=> a").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "~b <=> a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~b <=> a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~b <=> a").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "b <=> ~a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "b <=> ~a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "b <=> ~a").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "~b <=> ~a").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~b <=> ~a").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "~b <=> ~a").holds(this.aNotBToFalse)).isTrue(); } @Test @@ -307,50 +306,50 @@ public void testPBCToFalse() { } @Test - public void testMixedToFalse() throws ParserException { - assertThat(this.f.parse("~a & (a | ~b)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a & (a | ~b)").holds(this.aToFalse)).isTrue(); - assertThat(this.f.parse("~a & (a | ~b)").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("~b & (b | ~a)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~b & (b | ~a)").holds(this.aToFalse)).isTrue(); - assertThat(this.f.parse("~b & (b | ~a)").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("~a & (a | ~b) & c & (a => b | e)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a & (a | ~b) & c & (a => b | e)").holds(this.aToFalse)).isTrue(); - assertThat(this.f.parse("~a & (a | ~b) & c & (a => b | e)").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("~a & ~(a | ~b) & c & (a => b | e)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("~a & ~(a | ~b) & c & (a => b | e)").holds(this.aToFalse)).isTrue(); - assertThat(this.f.parse("~a & ~(a | ~b) & c & (a => b | e)").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("a & (a | ~b) & c & (a => b | e)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a => b | e)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a => b | e)").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & c & (a => ~b | e)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a => ~b | e)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a => ~b | e)").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & (a => b | e)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a => b | e)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a => b | e)").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & c & (a <=> ~b | e)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a <=> ~b | e)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a <=> ~b | e)").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & (a <=> b | e)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a <=> b | e)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a <=> b | e)").holds(this.aNotBToFalse)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & (a <=> b)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a <=> b)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a <=> b)").holds(this.aNotBToFalse)).isTrue(); - - assertThat(this.f.parse("a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.emptyToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.aToFalse)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.aNotBToFalse)).isTrue(); + public void testMixedToFalse() { + assertThat(parse(this.f, "~a & (a | ~b)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a & (a | ~b)").holds(this.aToFalse)).isTrue(); + assertThat(parse(this.f, "~a & (a | ~b)").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "~b & (b | ~a)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~b & (b | ~a)").holds(this.aToFalse)).isTrue(); + assertThat(parse(this.f, "~b & (b | ~a)").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "~a & (a | ~b) & c & (a => b | e)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a & (a | ~b) & c & (a => b | e)").holds(this.aToFalse)).isTrue(); + assertThat(parse(this.f, "~a & (a | ~b) & c & (a => b | e)").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "~a & ~(a | ~b) & c & (a => b | e)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "~a & ~(a | ~b) & c & (a => b | e)").holds(this.aToFalse)).isTrue(); + assertThat(parse(this.f, "~a & ~(a | ~b) & c & (a => b | e)").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "a & (a | ~b) & c & (a => b | e)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a => b | e)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a => b | e)").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & c & (a => ~b | e)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a => ~b | e)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a => ~b | e)").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & (a => b | e)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a => b | e)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a => b | e)").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & c & (a <=> ~b | e)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a <=> ~b | e)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a <=> ~b | e)").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b | e)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b | e)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b | e)").holds(this.aNotBToFalse)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b)").holds(this.aNotBToFalse)).isTrue(); + + assertThat(parse(this.f, "a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.emptyToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.aToFalse)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.aNotBToFalse)).isTrue(); } @Test @@ -384,166 +383,166 @@ public void testLiteralsToTrue() { } @Test - public void testNotToTrue() throws ParserException { - assertThat(this.f.parse("~~a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~~a").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("~~a").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~~~a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~~~a").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~~~a").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~(a & b)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~(a & b)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~(a & b)").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~(~a & b)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~(~a & b)").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("~(~a & b)").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~(a & ~b)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~(a & ~b)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~(a & ~b)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~(~a & ~b)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~(~a & ~b)").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("~(~a & ~b)").holds(this.aNotBToTrue)).isTrue(); + public void testNotToTrue() { + assertThat(parse(this.f, "~~a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~~a").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "~~a").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~~~a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~~~a").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~~~a").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~(a & b)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~(a & b)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~(a & b)").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~(~a & b)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~(~a & b)").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "~(~a & b)").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~(a & ~b)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~(a & ~b)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~(a & ~b)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~(~a & ~b)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~(~a & ~b)").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "~(~a & ~b)").holds(this.aNotBToTrue)).isTrue(); } @Test - public void testAndToTrue() throws ParserException { - assertThat(this.f.parse("a & ~a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a & ~a").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a & ~a").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("a & b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a & b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a & b").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~a & b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a & b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a & b").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("a & ~b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a & ~b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a & ~b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~a & ~b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a & ~b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a & ~b").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~a & ~b & c & ~d").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a & ~b & c & ~d").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a & ~b & c & ~d").holds(this.aNotBToTrue)).isFalse(); + public void testAndToTrue() { + assertThat(parse(this.f, "a & ~a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a & ~a").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a & ~a").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "a & b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a & b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a & b").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~a & b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a & b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a & b").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "a & ~b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a & ~b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a & ~b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~a & ~b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a & ~b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a & ~b").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~a & ~b & c & ~d").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a & ~b & c & ~d").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a & ~b & c & ~d").holds(this.aNotBToTrue)).isFalse(); } @Test - public void testOrToTrue() throws ParserException { - assertThat(this.f.parse("a | b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a | b").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("a | b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~a | b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a | b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a | b").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("a | ~b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a | ~b").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("a | ~b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~a | ~b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a | ~b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a | ~b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~a | ~b | c | ~d").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a | ~b | c | ~d").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a | ~b | c | ~d").holds(this.aNotBToTrue)).isTrue(); + public void testOrToTrue() { + assertThat(parse(this.f, "a | b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a | b").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "a | b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~a | b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a | b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a | b").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "a | ~b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a | ~b").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "a | ~b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~a | ~b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a | ~b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a | ~b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~a | ~b | c | ~d").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a | ~b | c | ~d").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a | ~b | c | ~d").holds(this.aNotBToTrue)).isTrue(); } @Test - public void testImplicationToTrue() throws ParserException { - assertThat(this.f.parse("a => a").holds(this.emptyToTrue)).isTrue(); - assertThat(this.f.parse("a => a").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("a => a").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("b => b").holds(this.emptyToTrue)).isTrue(); - assertThat(this.f.parse("b => b").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("b => b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("a => b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a => b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a => b").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~a => b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a => b").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("~a => b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("a => ~b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a => ~b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a => ~b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~a => ~b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a => ~b").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("~a => ~b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("b => a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("b => a").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("b => a").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~b => a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~b => a").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("~b => a").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("b => ~a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("b => ~a").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("b => ~a").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~b => ~a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~b => ~a").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~b => ~a").holds(this.aNotBToTrue)).isFalse(); + public void testImplicationToTrue() { + assertThat(parse(this.f, "a => a").holds(this.emptyToTrue)).isTrue(); + assertThat(parse(this.f, "a => a").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "a => a").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "b => b").holds(this.emptyToTrue)).isTrue(); + assertThat(parse(this.f, "b => b").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "b => b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "a => b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a => b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a => b").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~a => b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a => b").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "~a => b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "a => ~b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a => ~b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a => ~b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~a => ~b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a => ~b").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "~a => ~b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "b => a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "b => a").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "b => a").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~b => a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~b => a").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "~b => a").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "b => ~a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "b => ~a").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "b => ~a").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~b => ~a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~b => ~a").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~b => ~a").holds(this.aNotBToTrue)).isFalse(); } @Test - public void testEquivalenceToTrue() throws ParserException { - assertThat(this.f.parse("a <=> a").holds(this.emptyToTrue)).isTrue(); - assertThat(this.f.parse("a <=> a").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("a <=> a").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("b <=> b").holds(this.emptyToTrue)).isTrue(); - assertThat(this.f.parse("b <=> b").holds(this.aToTrue)).isTrue(); - assertThat(this.f.parse("b <=> b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("a <=> b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a <=> b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a <=> b").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~a <=> b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a <=> b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a <=> b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("a <=> ~b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a <=> ~b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a <=> ~b").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~a <=> ~b").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a <=> ~b").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a <=> ~b").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("b <=> a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("b <=> a").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("b <=> a").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~b <=> a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~b <=> a").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~b <=> a").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("b <=> ~a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("b <=> ~a").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("b <=> ~a").holds(this.aNotBToTrue)).isTrue(); - - assertThat(this.f.parse("~b <=> ~a").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~b <=> ~a").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~b <=> ~a").holds(this.aNotBToTrue)).isFalse(); + public void testEquivalenceToTrue() { + assertThat(parse(this.f, "a <=> a").holds(this.emptyToTrue)).isTrue(); + assertThat(parse(this.f, "a <=> a").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "a <=> a").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "b <=> b").holds(this.emptyToTrue)).isTrue(); + assertThat(parse(this.f, "b <=> b").holds(this.aToTrue)).isTrue(); + assertThat(parse(this.f, "b <=> b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "a <=> b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a <=> b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a <=> b").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~a <=> b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a <=> b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a <=> b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "a <=> ~b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a <=> ~b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a <=> ~b").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~a <=> ~b").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a <=> ~b").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a <=> ~b").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "b <=> a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "b <=> a").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "b <=> a").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~b <=> a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~b <=> a").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~b <=> a").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "b <=> ~a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "b <=> ~a").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "b <=> ~a").holds(this.aNotBToTrue)).isTrue(); + + assertThat(parse(this.f, "~b <=> ~a").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~b <=> ~a").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~b <=> ~a").holds(this.aNotBToTrue)).isFalse(); } @Test @@ -568,58 +567,58 @@ public void testPBCToTrue() { } @Test - public void testMixedToTrue() throws ParserException { - assertThat(this.f.parse("~a & (a | ~b)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a & (a | ~b)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a & (a | ~b)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~b & (b | ~a)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~b & (b | ~a)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~b & (b | ~a)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~a & (a | ~b)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a & (a | ~b)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a & (a | ~b)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~b & (b | ~a)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~b & (b | ~a)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~b & (b | ~a)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~a & (a | ~b) & c & (a => b | e)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a & (a | ~b) & c & (a => b | e)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a & (a | ~b) & c & (a => b | e)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("~a & ~(a | ~b) & c & (a => b | e)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("~a & ~(a | ~b) & c & (a => b | e)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("~a & ~(a | ~b) & c & (a => b | e)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & c & (a => b | e)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a => b | e)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a => b | e)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & c & (a => ~b | e)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a => ~b | e)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a => ~b | e)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & (a => b | e)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a => b | e)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a => b | e)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & c & (a <=> ~b | e)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a <=> ~b | e)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & c & (a <=> ~b | e)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & (a <=> b | e)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a <=> b | e)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a <=> b | e)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & (a <=> b)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a <=> b)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (a <=> b)").holds(this.aNotBToTrue)).isFalse(); - - assertThat(this.f.parse("a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.emptyToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.aToTrue)).isFalse(); - assertThat(this.f.parse("a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.aNotBToTrue)).isFalse(); + public void testMixedToTrue() { + assertThat(parse(this.f, "~a & (a | ~b)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a & (a | ~b)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a & (a | ~b)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~b & (b | ~a)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~b & (b | ~a)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~b & (b | ~a)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~a & (a | ~b)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a & (a | ~b)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a & (a | ~b)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~b & (b | ~a)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~b & (b | ~a)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~b & (b | ~a)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~a & (a | ~b) & c & (a => b | e)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a & (a | ~b) & c & (a => b | e)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a & (a | ~b) & c & (a => b | e)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "~a & ~(a | ~b) & c & (a => b | e)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "~a & ~(a | ~b) & c & (a => b | e)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "~a & ~(a | ~b) & c & (a => b | e)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & c & (a => b | e)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a => b | e)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a => b | e)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & c & (a => ~b | e)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a => ~b | e)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a => ~b | e)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & (a => b | e)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a => b | e)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a => b | e)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & c & (a <=> ~b | e)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a <=> ~b | e)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & c & (a <=> ~b | e)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b | e)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b | e)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b | e)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (a <=> b)").holds(this.aNotBToTrue)).isFalse(); + + assertThat(parse(this.f, "a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.emptyToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.aToTrue)).isFalse(); + assertThat(parse(this.f, "a & (a | ~b) & (3 * a + 2 * b > 4)").holds(this.aNotBToTrue)).isFalse(); } @Test diff --git a/core/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java b/core/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java index 6005b473..061cacf7 100644 --- a/core/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java +++ b/core/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java @@ -29,7 +29,6 @@ package org.logicng.primecomputation; import static org.assertj.core.api.Assertions.assertThat; -import static org.assertj.core.api.Assertions.fail; import org.junit.jupiter.api.Test; import org.logicng.RandomTag; @@ -116,20 +115,16 @@ public void testOriginalFormulas() throws IOException { Files.lines(Paths.get("src/test/resources/formulas/simplify_formulas.txt")) .filter(s -> !s.isEmpty()) .forEach(s -> { - try { - final Formula formula = this.f.parse(s); - final PrimeResult resultImplicantsMin = PrimeCompiler.getWithMinimization().compute(formula, PrimeResult.CoverageType.IMPLICANTS_COMPLETE); - verify(resultImplicantsMin, formula); - final PrimeResult resultImplicatesMin = PrimeCompiler.getWithMinimization().compute(formula, PrimeResult.CoverageType.IMPLICATES_COMPLETE); - verify(resultImplicatesMin, formula); - } catch (final ParserException e) { - fail(e.toString()); - } + final Formula formula = parse(this.f, s); + final PrimeResult resultImplicantsMin = PrimeCompiler.getWithMinimization().compute(formula, PrimeResult.CoverageType.IMPLICANTS_COMPLETE); + verify(resultImplicantsMin, formula); + final PrimeResult resultImplicatesMin = PrimeCompiler.getWithMinimization().compute(formula, PrimeResult.CoverageType.IMPLICATES_COMPLETE); + verify(resultImplicatesMin, formula); }); } @Test - public void testTimeoutHandlerSmall() throws ParserException { + public void testTimeoutHandlerSmall() { final List> compilers = Arrays.asList( new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICANTS_COMPLETE), new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICATES_COMPLETE), @@ -141,7 +136,7 @@ public void testTimeoutHandlerSmall() throws ParserException { new TimeoutOptimizationHandler(5_000L, TimeoutHandler.TimerType.RESTARTING_TIMEOUT), new TimeoutOptimizationHandler(System.currentTimeMillis() + 5_000L, TimeoutHandler.TimerType.FIXED_END) ); - final Formula formula = this.f.parse("a & b | ~c & a"); + final Formula formula = parse(this.f, "a & b | ~c & a"); for (final TimeoutOptimizationHandler handler : handlers) { testHandler(handler, formula, compiler.first(), compiler.second(), false); } @@ -149,7 +144,7 @@ public void testTimeoutHandlerSmall() throws ParserException { } @Test - public void testTimeoutHandlerLarge() throws ParserException, IOException { + public void testTimeoutHandlerLarge() throws IOException, ParserException { final List> compilers = Arrays.asList( new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICANTS_COMPLETE), new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICATES_COMPLETE), @@ -169,8 +164,8 @@ public void testTimeoutHandlerLarge() throws ParserException, IOException { } @Test - public void testCancellationPoints() throws IOException, ParserException { - final Formula formula = this.f.parse(Files.readAllLines(Paths.get("src/test/resources/formulas/simplify_formulas.txt")).get(0)); + public void testCancellationPoints() throws IOException { + final Formula formula = parse(this.f, Files.readAllLines(Paths.get("src/test/resources/formulas/simplify_formulas.txt")).get(0)); final List> compilers = Arrays.asList( new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICANTS_COMPLETE), new Pair<>(PrimeCompiler.getWithMaximization(), PrimeResult.CoverageType.IMPLICATES_COMPLETE), diff --git a/core/src/test/java/org/logicng/primecomputation/PrimeImplicantReductionTest.java b/core/src/test/java/org/logicng/primecomputation/PrimeImplicantReductionTest.java index cc5636ff..a71af686 100644 --- a/core/src/test/java/org/logicng/primecomputation/PrimeImplicantReductionTest.java +++ b/core/src/test/java/org/logicng/primecomputation/PrimeImplicantReductionTest.java @@ -62,23 +62,23 @@ public class PrimeImplicantReductionTest extends TestWithExampleFormulas { @Test - public void testSimple() throws ParserException { + public void testSimple() { final NaivePrimeReduction naiveTautology = new NaivePrimeReduction(this.f.verum()); assertThat(naiveTautology.reduceImplicant(new TreeSet<>(Arrays.asList(this.A, this.B)))).isEmpty(); - final NaivePrimeReduction naive01 = new NaivePrimeReduction(this.f.parse("a&b|c&d")); + final NaivePrimeReduction naive01 = new NaivePrimeReduction(parse(this.f, "a&b|c&d")); assertThat(naive01.reduceImplicant(new TreeSet<>(Arrays.asList(this.A, this.B, this.C, this.D.negate())))) .containsExactlyInAnyOrder(this.A, this.B); assertThat(naive01.reduceImplicant(new TreeSet<>(Arrays.asList(this.A.negate(), this.B, this.C, this.D)))) .containsExactlyInAnyOrder(this.C, this.D); - final NaivePrimeReduction naive02 = new NaivePrimeReduction(this.f.parse("a|b|~a&~b")); + final NaivePrimeReduction naive02 = new NaivePrimeReduction(parse(this.f, "a|b|~a&~b")); assertThat(naive02.reduceImplicant(new TreeSet<>(Arrays.asList(this.A.negate(), this.B)))) .containsExactlyInAnyOrder(); assertThat(naive02.reduceImplicant(new TreeSet<>(Arrays.asList(this.A.negate(), this.B)))) .containsExactlyInAnyOrder(); - final NaivePrimeReduction naive03 = new NaivePrimeReduction(this.f.parse("(a => b) | b | c")); + final NaivePrimeReduction naive03 = new NaivePrimeReduction(parse(this.f, "(a => b) | b | c")); assertThat(naive03.reduceImplicant(new TreeSet<>(Arrays.asList(this.A, this.B, this.C.negate())))) .containsExactlyInAnyOrder(this.B); assertThat(naive03.reduceImplicant(new TreeSet<>(Arrays.asList(this.A, this.B.negate(), this.C)))) @@ -104,10 +104,10 @@ public void testLargeFormula() throws IOException, ParserException { } @Test - public void testSmallFormulas() throws IOException, ParserException { + public void testSmallFormulas() throws IOException { final List lines = Files.readAllLines(Paths.get("src/test/resources/formulas/small_formulas.txt")); for (final String line : lines) { - testFormula(this.f.parse(line)); + testFormula(parse(this.f, line)); } } @@ -130,7 +130,7 @@ public void testRandom() { } @Test - public void testCancellationPoints() throws ParserException, IOException { + public void testCancellationPoints() throws IOException, ParserException { final Formula formula = FormulaReader.readPseudoBooleanFormula("src/test/resources/formulas/large_formula.txt", this.f); for (int numStarts = 0; numStarts < 20; numStarts++) { final SATHandler handler = new BoundedSatHandler(numStarts); diff --git a/core/src/test/java/org/logicng/primecomputation/PrimeImplicateReductionTest.java b/core/src/test/java/org/logicng/primecomputation/PrimeImplicateReductionTest.java index 70889a11..f3f4bcd7 100644 --- a/core/src/test/java/org/logicng/primecomputation/PrimeImplicateReductionTest.java +++ b/core/src/test/java/org/logicng/primecomputation/PrimeImplicateReductionTest.java @@ -63,16 +63,16 @@ public class PrimeImplicateReductionTest extends TestWithExampleFormulas { @Test - public void testPrimeImplicateNaive() throws ParserException { - final NaivePrimeReduction naive01 = new NaivePrimeReduction(this.f.parse("a&b")); + public void testPrimeImplicateNaive() { + final NaivePrimeReduction naive01 = new NaivePrimeReduction(parse(this.f, "a&b")); assertThat(naive01.reduceImplicate(new TreeSet<>(Arrays.asList(this.A, this.B)))) .containsAnyOf(this.A, this.B).hasSize(1); - final NaivePrimeReduction naive02 = new NaivePrimeReduction(this.f.parse("(a => b) | b | c")); + final NaivePrimeReduction naive02 = new NaivePrimeReduction(parse(this.f, "(a => b) | b | c")); assertThat(naive02.reduceImplicate(new TreeSet<>(Arrays.asList(this.A.negate(), this.B, this.C)))) .containsExactly(this.A.negate(), this.B, this.C); - final NaivePrimeReduction naive03 = new NaivePrimeReduction(this.f.parse("(a => b) & b & c")); + final NaivePrimeReduction naive03 = new NaivePrimeReduction(parse(this.f, "(a => b) & b & c")); assertThat(naive03.reduceImplicate(new TreeSet<>(Arrays.asList(this.B, this.C)))) .containsAnyOf(this.B, this.C).hasSize(1); } @@ -96,10 +96,10 @@ public void testLargeFormula() throws IOException, ParserException { } @Test - public void testSmallFormulas() throws IOException, ParserException { + public void testSmallFormulas() throws IOException { final List lines = Files.readAllLines(Paths.get("src/test/resources/formulas/small_formulas.txt")); for (final String line : lines) { - testFormula(this.f.parse(line)); + testFormula(parse(this.f, line)); } } @@ -122,7 +122,7 @@ public void testRandom() { } @Test - public void testCancellationPoints() throws ParserException, IOException { + public void testCancellationPoints() throws IOException, ParserException { final Formula formula = FormulaReader.readPseudoBooleanFormula("src/test/resources/formulas/large_formula.txt", this.f); for (int numStarts = 0; numStarts < 20; numStarts++) { final SATHandler handler = new BoundedSatHandler(numStarts); diff --git a/core/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java b/core/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java index d6ca75d8..aa44a5ba 100644 --- a/core/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java +++ b/core/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java @@ -28,6 +28,7 @@ package org.logicng.pseudobooleans; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.logicng.LogicNGTest; @@ -39,7 +40,6 @@ import org.logicng.formulas.Literal; import org.logicng.formulas.PBConstraint; import org.logicng.formulas.Variable; -import org.logicng.io.parsers.ParserException; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; @@ -163,7 +163,7 @@ public void testSpecialCases() { } @Test - public void testCCNormalized() throws ParserException { + public void testCCNormalized() { final List lits = new ArrayList<>(); lits.add(this.f.literal("m", true)); lits.add(this.f.literal("n", true)); @@ -171,7 +171,7 @@ public void testCCNormalized() throws ParserException { coeffs2.add(2); coeffs2.add(2); final PBConstraint normCC = (PBConstraint) this.f.pbc(CType.LE, 2, lits, coeffs2); - assertThat(this.encoders[0].encode(normCC)).containsExactly(this.f.parse("~m | ~n")); + assertThat(this.encoders[0].encode(normCC)).containsExactly(parse(this.f, "~m | ~n")); } @Test diff --git a/core/src/test/java/org/logicng/solvers/ModelTest.java b/core/src/test/java/org/logicng/solvers/ModelTest.java index b3b4099d..4648e421 100644 --- a/core/src/test/java/org/logicng/solvers/ModelTest.java +++ b/core/src/test/java/org/logicng/solvers/ModelTest.java @@ -30,6 +30,7 @@ import static org.assertj.core.api.Assertions.assertThat; import static org.assertj.core.api.Assertions.assertThatThrownBy; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.params.ParameterizedTest; import org.junit.jupiter.params.provider.MethodSource; @@ -38,7 +39,6 @@ import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Variable; -import org.logicng.io.parsers.ParserException; import org.logicng.solvers.functions.ModelEnumerationFunction; import org.logicng.solvers.sat.GlucoseConfig; import org.logicng.solvers.sat.MiniSatConfig; @@ -83,17 +83,17 @@ public static Collection solvers() { @ParameterizedTest @MethodSource("solvers") - public void testNoModel(final SATSolver solver) throws ParserException { + public void testNoModel(final SATSolver solver) { solver.reset(); solver.add(f.falsum()); solver.sat(); assertThat(solver.model()).isNull(); solver.reset(); - solver.add(f.parse("A & ~A")); + solver.add(parse(f, "A & ~A")); solver.sat(); assertThat(solver.model()).isNull(); solver.reset(); - solver.add(f.parse("(A => (B & C)) & A & C & (C <=> ~B)")); + solver.add(parse(f, "(A => (B & C)) & A & C & (C <=> ~B)")); solver.sat(); assertThat(solver.model()).isNull(); } @@ -129,9 +129,9 @@ public void testSimpleModel(final SATSolver solver) { @ParameterizedTest @MethodSource("solvers") - public void testCNFFormula(final SATSolver solver) throws ParserException { + public void testCNFFormula(final SATSolver solver) { solver.reset(); - final Formula formula = f.parse("(A|B|C) & (~A|~B|~C) & (A|~B|~C) & (~A|~B|C)"); + final Formula formula = parse(f, "(A|B|C) & (~A|~B|~C) & (A|~B|~C) & (~A|~B|C)"); solver.add(formula); solver.sat(); final Assignment model = solver.model(); @@ -144,9 +144,9 @@ public void testCNFFormula(final SATSolver solver) throws ParserException { @ParameterizedTest @MethodSource("solvers") - public void testCNFWithAuxiliaryVars(final MiniSat solver) throws ParserException { + public void testCNFWithAuxiliaryVars(final MiniSat solver) { solver.reset(); - final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); + final Formula formula = parse(f, "(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); final Formula cnf = formula.transform(new TseitinTransformation(0)); solver.add(cnf); solver.sat(); @@ -171,9 +171,9 @@ public void testCNFWithAuxiliaryVars(final MiniSat solver) throws ParserExceptio @ParameterizedTest @MethodSource("solvers") - public void testCNFWithAuxiliaryVarsRestrictedToOriginal(final SATSolver solver) throws ParserException { + public void testCNFWithAuxiliaryVarsRestrictedToOriginal(final SATSolver solver) { solver.reset(); - final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); + final Formula formula = parse(f, "(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); final Formula cnf = formula.transform(new TseitinTransformation(0)); solver.add(cnf); solver.sat(); @@ -190,9 +190,9 @@ public void testCNFWithAuxiliaryVarsRestrictedToOriginal(final SATSolver solver) @ParameterizedTest @MethodSource("solvers") - public void testNonCNFAllVars(final MiniSat solver) throws ParserException { + public void testNonCNFAllVars(final MiniSat solver) { solver.reset(); - final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); + final Formula formula = parse(f, "(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); solver.add(formula); solver.sat(); final Assignment model = solver.model(); @@ -215,9 +215,9 @@ public void testNonCNFAllVars(final MiniSat solver) throws ParserException { @ParameterizedTest @MethodSource("solvers") - public void testNonCNFOnlyFormulaVars(final SATSolver solver) throws ParserException { + public void testNonCNFOnlyFormulaVars(final SATSolver solver) { solver.reset(); - final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); + final Formula formula = parse(f, "(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); solver.add(formula); solver.sat(); final Assignment model = solver.model(formula.variables()); @@ -233,9 +233,9 @@ public void testNonCNFOnlyFormulaVars(final SATSolver solver) throws ParserExcep @ParameterizedTest @MethodSource("solvers") - public void testNonCNFRestrictedVars(final SATSolver solver) throws ParserException { + public void testNonCNFRestrictedVars(final SATSolver solver) { solver.reset(); - final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); + final Formula formula = parse(f, "(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); final MiniSat miniSat = MiniSat.miniSat(f); miniSat.add(formula); solver.add(formula); @@ -254,9 +254,9 @@ public void testNonCNFRestrictedVars(final SATSolver solver) throws ParserExcept @ParameterizedTest @MethodSource("solvers") - public void testNonCNFRestrictedAndAdditionalVars(final SATSolver solver) throws ParserException { + public void testNonCNFRestrictedAndAdditionalVars(final SATSolver solver) { solver.reset(); - final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); + final Formula formula = parse(f, "(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); final MiniSat miniSat = MiniSat.miniSat(f); miniSat.add(formula); solver.add(formula); @@ -278,9 +278,9 @@ public void testNonCNFRestrictedAndAdditionalVars(final SATSolver solver) throws @ParameterizedTest @MethodSource("solvers") - public void testUnsolvedFormula(final SATSolver solver) throws ParserException { + public void testUnsolvedFormula(final SATSolver solver) { solver.reset(); - final Formula formula = f.parse("(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); + final Formula formula = parse(f, "(A => B & C) & (~A => C & ~D) & (C => (D & E | ~E & B)) & ~F"); solver.add(formula); assertThatThrownBy(solver::model).isInstanceOf(IllegalStateException.class); } diff --git a/core/src/test/java/org/logicng/solvers/functions/BackboneFunctionTest.java b/core/src/test/java/org/logicng/solvers/functions/BackboneFunctionTest.java index 8fff3812..d01bb274 100644 --- a/core/src/test/java/org/logicng/solvers/functions/BackboneFunctionTest.java +++ b/core/src/test/java/org/logicng/solvers/functions/BackboneFunctionTest.java @@ -29,6 +29,7 @@ package org.logicng.solvers.functions; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.junit.jupiter.params.ParameterizedTest; @@ -125,13 +126,13 @@ public void testConstants(final MiniSat solver) { @ParameterizedTest @MethodSource("solvers") - public void testSimpleBackbones(final MiniSat solver) throws ParserException { + public void testSimpleBackbones(final MiniSat solver) { solver.reset(); SolverState state = null; if (solver.underlyingSolver() instanceof MiniSat2Solver) { state = solver.saveState(); } - solver.add(f.parse("a & b & ~c")); + solver.add(parse(f, "a & b & ~c")); Backbone backbone = solver.backbone(v("a b c")); assertThat(backbone.isSat()).isTrue(); assertThat(backbone.getCompleteBackbone()).containsExactly(f.variable("a"), f.variable("b"), f.literal("c", false)); @@ -140,7 +141,7 @@ public void testSimpleBackbones(final MiniSat solver) throws ParserException { } else { solver.reset(); } - solver.add(f.parse("~a & ~b & c")); + solver.add(parse(f, "~a & ~b & c")); backbone = solver.backbone(v("a c")); assertThat(backbone.isSat()).isTrue(); assertThat(backbone.getCompleteBackbone()).containsExactly(f.literal("a", false), f.variable("c")); @@ -148,15 +149,15 @@ public void testSimpleBackbones(final MiniSat solver) throws ParserException { @ParameterizedTest @MethodSource("solvers") - public void testSimpleFormulas(final MiniSat solver) throws ParserException { + public void testSimpleFormulas(final MiniSat solver) { solver.reset(); - solver.add(f.parse("(a => c | d) & (b => d | ~e) & (a | b)")); + solver.add(parse(f, "(a => c | d) & (b => d | ~e) & (a | b)")); Backbone backbone = solver.backbone(v("a b c d e f")); assertThat(backbone.isSat()).isTrue(); assertThat(backbone.getCompleteBackbone()).isEmpty(); - solver.add(f.parse("a => b")); - solver.add(f.parse("b => a")); - solver.add(f.parse("~d")); + solver.add(parse(f, "a => b")); + solver.add(parse(f, "b => a")); + solver.add(parse(f, "~d")); backbone = solver.backbone(v("a b c d e f g h")); assertThat(backbone.isSat()).isTrue(); assertThat(backbone.getCompleteBackbone()).containsExactly(f.variable("a"), f.variable("b"), f.variable("c"), @@ -165,17 +166,17 @@ public void testSimpleFormulas(final MiniSat solver) throws ParserException { @ParameterizedTest @MethodSource("solvers") - public void testSimpleFormulasWithBuilderUsage(final MiniSat solver) throws ParserException { + public void testSimpleFormulasWithBuilderUsage(final MiniSat solver) { solver.reset(); - solver.add(f.parse("(a => c | d) & (b => d | ~e) & (a | b)")); + solver.add(parse(f, "(a => c | d) & (b => d | ~e) & (a | b)")); Backbone backbone = solver.execute(BackboneFunction.builder().variables( f.variable("a"), f.variable("b"), f.variable("c"), f.variable("d"), f.variable("e"), f.variable("f")) .build()); assertThat(backbone.isSat()).isTrue(); assertThat(backbone.getCompleteBackbone()).isEmpty(); - solver.add(f.parse("a => b")); - solver.add(f.parse("b => a")); - solver.add(f.parse("~d")); + solver.add(parse(f, "a => b")); + solver.add(parse(f, "b => a")); + solver.add(parse(f, "~d")); backbone = solver.backbone(v("a b c d e f g h")); assertThat(backbone.isSat()).isTrue(); assertThat(backbone.getCompleteBackbone()).containsExactly(f.variable("a"), f.variable("b"), f.variable("c"), @@ -285,31 +286,31 @@ public void testRealFormulaIncrementalDecremental1(final MiniSat solver) throws assertThat(backbone.isSat()).isTrue(); solver.loadState(state); - solver.add(f.parse("v411 & v385")); + solver.add(parse(f, "v411 & v385")); backbone = solver.backbone(formula.variables()); assertThat(backbone.getCompleteBackbone()).isEqualTo(parseBackbone(expectedBackbones.get(2))); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); - solver.add(f.parse("v411 & v385 & v275")); + solver.add(parse(f, "v411 & v385 & v275")); backbone = solver.backbone(formula.variables()); assertThat(backbone.getCompleteBackbone()).isEqualTo(parseBackbone(expectedBackbones.get(3))); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); - solver.add(f.parse("v411 & v385 & v275 & v188")); + solver.add(parse(f, "v411 & v385 & v275 & v188")); backbone = solver.backbone(formula.variables()); assertThat(backbone.getCompleteBackbone()).isEqualTo(parseBackbone(expectedBackbones.get(4))); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); - solver.add(f.parse("v411 & v385 & v275 & v188 & v103")); + solver.add(parse(f, "v411 & v385 & v275 & v188 & v103")); backbone = solver.backbone(formula.variables()); assertThat(backbone.getCompleteBackbone()).isEqualTo(parseBackbone(expectedBackbones.get(5))); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); - solver.add(f.parse("v411 & v385 & v275 & v188 & v103 & v404")); + solver.add(parse(f, "v411 & v385 & v275 & v188 & v103 & v404")); backbone = solver.backbone(formula.variables()); assertThat(backbone.getCompleteBackbone()).isEmpty(); assertThat(backbone.isSat()).isFalse(); @@ -339,31 +340,31 @@ public void testRealFormulaIncrementalDecremental2(final MiniSat solver) throws assertThat(backbone.isSat()).isTrue(); solver.loadState(state); - solver.add(f.parse("v2609 & v2416")); + solver.add(parse(f, "v2609 & v2416")); backbone = solver.backbone(formula.variables()); assertThat(backbone.getCompleteBackbone()).isEqualTo(parseBackbone(expectedBackbones.get(2))); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); - solver.add(f.parse("v2609 & v2416 & v2048")); + solver.add(parse(f, "v2609 & v2416 & v2048")); backbone = solver.backbone(formula.variables()); assertThat(backbone.getCompleteBackbone()).isEqualTo(parseBackbone(expectedBackbones.get(3))); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); - solver.add(f.parse("v2609 & v2416 & v2048 & v39")); + solver.add(parse(f, "v2609 & v2416 & v2048 & v39")); backbone = solver.backbone(formula.variables()); assertThat(backbone.getCompleteBackbone()).isEqualTo(parseBackbone(expectedBackbones.get(4))); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); - solver.add(f.parse("v2609 & v2416 & v2048 & v39 & v1663")); + solver.add(parse(f, "v2609 & v2416 & v2048 & v39 & v1663")); backbone = solver.backbone(formula.variables()); assertThat(backbone.getCompleteBackbone()).isEqualTo(parseBackbone(expectedBackbones.get(5))); assertThat(backbone.isSat()).isTrue(); solver.loadState(state); - solver.add(f.parse("v2609 & v2416 & v2048 & v39 & v1663 & v2238")); + solver.add(parse(f, "v2609 & v2416 & v2048 & v39 & v1663 & v2238")); backbone = solver.backbone(formula.variables()); assertThat(backbone.getCompleteBackbone()).isEmpty(); assertThat(backbone.isSat()).isFalse(); @@ -371,13 +372,13 @@ public void testRealFormulaIncrementalDecremental2(final MiniSat solver) throws } @Test - public void testMiniCardSpecialCase() throws ParserException { + public void testMiniCardSpecialCase() { final FormulaFactory f = new FormulaFactory(); final SATSolver miniCard = MiniSat.miniCard(f); - miniCard.add(f.parse("v1 + v2 + v3 + v4 + v5 + v6 = 1")); - miniCard.add(f.parse("v1234 + v50 + v60 = 1")); - miniCard.add(f.parse("(v1 => v1234) & (v2 => v1234) & (v3 => v1234) & (v4 => v1234) & (v5 => v50) & (v6 => v60)")); - miniCard.add(f.parse("~v6")); + miniCard.add(parse(f, "v1 + v2 + v3 + v4 + v5 + v6 = 1")); + miniCard.add(parse(f, "v1234 + v50 + v60 = 1")); + miniCard.add(parse(f, "(v1 => v1234) & (v2 => v1234) & (v3 => v1234) & (v4 => v1234) & (v5 => v50) & (v6 => v60)")); + miniCard.add(parse(f, "~v6")); final Backbone backboneMC = miniCard.backbone(Arrays.asList(f.variable("v6"), f.variable("v60"))); assertThat(backboneMC.getNegativeBackbone()).extracting(Variable::name).containsExactlyInAnyOrder("v6", "v60"); } @@ -390,10 +391,10 @@ private SortedSet v(final String s) { return vars; } - private SortedSet parseBackbone(final String string) throws ParserException { + private SortedSet parseBackbone(final String string) { final SortedSet literals = new TreeSet<>(); for (final String lit : string.split(" ")) { - literals.add((Literal) f.parse(lit)); + literals.add((Literal) parse(f, lit)); } return literals; } diff --git a/core/src/test/java/org/logicng/solvers/functions/ModelEnumerationFunctionTest.java b/core/src/test/java/org/logicng/solvers/functions/ModelEnumerationFunctionTest.java index 0e3aa04b..b2c9357f 100644 --- a/core/src/test/java/org/logicng/solvers/functions/ModelEnumerationFunctionTest.java +++ b/core/src/test/java/org/logicng/solvers/functions/ModelEnumerationFunctionTest.java @@ -1,11 +1,11 @@ package org.logicng.solvers.functions; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.logicng.datastructures.Assignment; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; @@ -25,9 +25,9 @@ public ModelEnumerationFunctionTest() { } @Test - public void testModelEnumerationSimple() throws ParserException { + public void testModelEnumerationSimple() { final SATSolver solver = MiniSat.miniSat(this.f); - solver.add(this.f.parse("A & (B | C)")); + solver.add(parse(this.f, "A & (B | C)")); final List models = solver.execute(ModelEnumerationFunction.builder().build()); assertThat(models).containsExactlyInAnyOrder( new Assignment(this.f.variable("A"), this.f.variable("B"), this.f.variable("C")), @@ -37,9 +37,9 @@ public void testModelEnumerationSimple() throws ParserException { } @Test - public void testFastEvaluable() throws ParserException { + public void testFastEvaluable() { final SATSolver solver = MiniSat.miniSat(this.f); - solver.add(this.f.parse("A & (B | C)")); + solver.add(parse(this.f, "A & (B | C)")); List models = solver.execute(ModelEnumerationFunction.builder().build()); assertThat(models).extracting(Assignment::fastEvaluable).containsOnly(false); models = solver.execute(ModelEnumerationFunction.builder().fastEvaluable(false).build()); diff --git a/core/src/test/java/org/logicng/solvers/functions/OptimizationFunctionTest.java b/core/src/test/java/org/logicng/solvers/functions/OptimizationFunctionTest.java index 3f9c2ce9..f35ce60a 100644 --- a/core/src/test/java/org/logicng/solvers/functions/OptimizationFunctionTest.java +++ b/core/src/test/java/org/logicng/solvers/functions/OptimizationFunctionTest.java @@ -30,6 +30,7 @@ import static java.util.stream.Collectors.toCollection; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.junit.jupiter.params.ParameterizedTest; @@ -102,8 +103,8 @@ public static Collection solvers() { @ParameterizedTest @MethodSource("solvers") - public void testUnsatFormula(final SATSolver solver) throws ParserException { - final Formula formula = solver.factory().parse("a & b & (a => ~b)"); + public void testUnsatFormula(final SATSolver solver) { + final Formula formula = parse(solver.factory(), "a & b & (a => ~b)"); final Assignment minimumModel = optimize(Collections.singleton(formula), formula.variables(), Collections.emptyList(), false, solver, null); assertThat(minimumModel).isNull(); final Assignment maximumModel = optimize(Collections.singleton(formula), formula.variables(), Collections.emptyList(), true, solver, null); @@ -112,8 +113,8 @@ public void testUnsatFormula(final SATSolver solver) throws ParserException { @ParameterizedTest @MethodSource("solvers") - public void testSingleModel(final SATSolver solver) throws ParserException { - final Formula formula = solver.factory().parse("~a & ~b & ~c"); + public void testSingleModel(final SATSolver solver) { + final Formula formula = parse(solver.factory(), "~a & ~b & ~c"); final Assignment minimumModel = optimize(Collections.singleton(formula), formula.variables(), Collections.emptyList(), false, solver, null); testMinimumModel(formula, minimumModel, formula.variables()); final Assignment maximumModel = optimize(Collections.singleton(formula), formula.variables(), Collections.emptyList(), true, solver, null); @@ -185,13 +186,13 @@ private static SortedSet randomTargetLiterals(final Random random, fina @ParameterizedTest @MethodSource("solvers") - public void testIncrementalityMinimizeAndMaximize(final MiniSat solver) throws ParserException { + public void testIncrementalityMinimizeAndMaximize(final MiniSat solver) { final FormulaFactory f = solver.factory(); if (!solver.canSaveLoadState()) { return; } solver.reset(); - Formula formula = f.parse("(a|b|c|d|e) & (p|q) & (x|y|z)"); + Formula formula = parse(f, "(a|b|c|d|e) & (p|q) & (x|y|z)"); final SortedSet vars = new TreeSet<>(formula.variables()); solver.add(formula); @@ -200,7 +201,7 @@ public void testIncrementalityMinimizeAndMaximize(final MiniSat solver) throws P assertThat(minimumModel.positiveVariables()).hasSize(3); assertThat(maximumModel.positiveVariables()).hasSize(10); - formula = f.parse("~p"); + formula = parse(f, "~p"); vars.addAll(formula.variables()); solver.add(formula); minimumModel = solver.execute(OptimizationFunction.builder().minimize().literals(vars).build()); @@ -208,7 +209,7 @@ public void testIncrementalityMinimizeAndMaximize(final MiniSat solver) throws P assertThat(minimumModel.positiveVariables()).hasSize(3).contains(f.variable("q")); assertThat(maximumModel.positiveVariables()).hasSize(9).contains(f.variable("q")); - formula = f.parse("(x => n) & (y => m) & (a => ~b & ~c)"); + formula = parse(f, "(x => n) & (y => m) & (a => ~b & ~c)"); vars.addAll(formula.variables()); solver.add(formula); minimumModel = solver.execute(OptimizationFunction.builder().minimize().literals(vars).build()); @@ -218,7 +219,7 @@ public void testIncrementalityMinimizeAndMaximize(final MiniSat solver) throws P .contains(f.variable("q"), f.variable("z")) .doesNotContain(f.variable("a")); - formula = f.parse("(z => v & w) & (m => v) & (b => ~c & ~d & ~e)"); + formula = parse(f, "(z => v & w) & (m => v) & (b => ~c & ~d & ~e)"); vars.addAll(formula.variables()); solver.add(formula); minimumModel = solver.execute(OptimizationFunction.builder().minimize().literals(vars).build()); @@ -228,7 +229,7 @@ public void testIncrementalityMinimizeAndMaximize(final MiniSat solver) throws P .contains(f.variable("q"), f.variable("x"), f.variable("n"), f.variable("v"), f.variable("w")) .doesNotContain(f.variable("b")); - formula = f.parse("~q"); + formula = parse(f, "~q"); vars.addAll(formula.variables()); solver.add(formula); minimumModel = solver.execute(OptimizationFunction.builder().minimize().literals(vars).build()); @@ -239,7 +240,7 @@ public void testIncrementalityMinimizeAndMaximize(final MiniSat solver) throws P @ParameterizedTest @MethodSource("solvers") - public void testAdditionalVariables(final SATSolver solver) throws ParserException { + public void testAdditionalVariables(final SATSolver solver) { final FormulaFactory f = solver.factory(); final Variable a = f.variable("a"); final Literal na = f.literal("a", false); @@ -251,7 +252,7 @@ public void testAdditionalVariables(final SATSolver solver) throws ParserExcepti final Variable y = f.variable("y"); solver.reset(); - final Formula formula = f.parse("(a|b) & (~a => c) & (x|y)"); + final Formula formula = parse(f, "(a|b) & (~a => c) & (x|y)"); final List literalsANBX = Arrays.asList(a, nb, x); final Assignment minimumModel = optimize(Collections.singleton(formula), literalsANBX, Collections.emptyList(), false, solver, null); diff --git a/core/src/test/java/org/logicng/solvers/functions/UnsatCoreFunctionTest.java b/core/src/test/java/org/logicng/solvers/functions/UnsatCoreFunctionTest.java index a7cb24de..454bfb44 100644 --- a/core/src/test/java/org/logicng/solvers/functions/UnsatCoreFunctionTest.java +++ b/core/src/test/java/org/logicng/solvers/functions/UnsatCoreFunctionTest.java @@ -63,7 +63,7 @@ public void testExceptionalBehavior() { .hasMessage("Cannot generate an unsat core before the formula was solved."); assertThatThrownBy(() -> { final SATSolver solver = MiniSat.miniCard(this.f, MiniSatConfig.builder().proofGeneration(true).build()); - solver.add(this.f.parse("A & (A => B) & (B => ~A)")); + solver.add(parse(f, "A & (A => B) & (B => ~A)")); solver.sat(); solver.execute(UnsatCoreFunction.get()); }).isInstanceOf(IllegalStateException.class) diff --git a/core/src/test/java/org/logicng/solvers/maxsat/PartialMaxSATTest.java b/core/src/test/java/org/logicng/solvers/maxsat/PartialMaxSATTest.java index 76c61707..ffd28139 100644 --- a/core/src/test/java/org/logicng/solvers/maxsat/PartialMaxSATTest.java +++ b/core/src/test/java/org/logicng/solvers/maxsat/PartialMaxSATTest.java @@ -38,7 +38,6 @@ import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.handlers.TimeoutMaxSATHandler; -import org.logicng.io.parsers.ParserException; import org.logicng.solvers.MaxSATSolver; import org.logicng.solvers.maxsat.algorithms.MaxSAT; import org.logicng.solvers.maxsat.algorithms.MaxSATConfig; @@ -79,7 +78,7 @@ public PartialMaxSATTest() throws FileNotFoundException { public void testExceptionalBehaviorForMSU3() { assertThatThrownBy(() -> { final MaxSATSolver solver = MaxSATSolver.msu3(this.f); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, 2); solver.solve(); }).isInstanceOf(IllegalStateException.class) @@ -89,7 +88,7 @@ public void testExceptionalBehaviorForMSU3() { .incremental(MaxSATConfig.IncrementalStrategy.ITERATIVE) .cardinality(MaxSATConfig.CardinalityEncoding.MTOTALIZER) .build()); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, 1); solver.solve(); }).isInstanceOf(IllegalStateException.class) @@ -289,13 +288,13 @@ public void testTimeoutHandlerUB() throws IOException { } @Test - public void testNonClauselSoftConstraints() throws ParserException { + public void testNonClauselSoftConstraints() { final MaxSATSolver[] solvers = new MaxSATSolver[2]; solvers[0] = MaxSATSolver.msu3(this.f); solvers[1] = MaxSATSolver.linearUS(this.f); for (final MaxSATSolver solver : solvers) { - solver.addHardFormula(this.f.parse("a & b & c")); - solver.addSoftFormula(this.f.parse("~a & ~b & ~c"), 1); + solver.addHardFormula(parse(this.f, "a & b & c")); + solver.addSoftFormula(parse(this.f, "~a & ~b & ~c"), 1); assertThat(solver.solve()).isEqualTo(MaxSAT.MaxSATResult.OPTIMUM); assertThat(solver.model().literals()).containsExactlyInAnyOrder( this.f.variable("a"), this.f.variable("b"), this.f.variable("c") @@ -305,14 +304,14 @@ public void testNonClauselSoftConstraints() throws ParserException { } @Test - public void testSoftConstraintsCornerCaseVerum() throws ParserException { + public void testSoftConstraintsCornerCaseVerum() { final MaxSATSolver[] solvers = new MaxSATSolver[2]; solvers[0] = MaxSATSolver.msu3(this.f); solvers[1] = MaxSATSolver.linearUS(this.f); for (final MaxSATSolver solver : solvers) { - solver.addHardFormula(this.f.parse("a & b & c")); - solver.addSoftFormula(this.f.parse("$true"), 1); - solver.addSoftFormula(this.f.parse("~a & ~b & ~c"), 1); + solver.addHardFormula(parse(this.f, "a & b & c")); + solver.addSoftFormula(parse(this.f, "$true"), 1); + solver.addSoftFormula(parse(this.f, "~a & ~b & ~c"), 1); assertThat(solver.solve()).isEqualTo(MaxSAT.MaxSATResult.OPTIMUM); assertThat(solver.model().literals()).containsExactlyInAnyOrder( this.f.variable("a"), this.f.variable("b"), this.f.variable("c") @@ -322,14 +321,14 @@ public void testSoftConstraintsCornerCaseVerum() throws ParserException { } @Test - public void testSoftConstraintsCornerCaseFalsum() throws ParserException { + public void testSoftConstraintsCornerCaseFalsum() { final MaxSATSolver[] solvers = new MaxSATSolver[2]; solvers[0] = MaxSATSolver.msu3(this.f); solvers[1] = MaxSATSolver.linearUS(this.f); for (final MaxSATSolver solver : solvers) { - solver.addHardFormula(this.f.parse("a & b & c")); - solver.addSoftFormula(this.f.parse("$false"), 1); - solver.addSoftFormula(this.f.parse("~a & ~b & ~c"), 1); + solver.addHardFormula(parse(this.f, "a & b & c")); + solver.addSoftFormula(parse(this.f, "$false"), 1); + solver.addSoftFormula(parse(this.f, "~a & ~b & ~c"), 1); assertThat(solver.solve()).isEqualTo(MaxSAT.MaxSATResult.OPTIMUM); assertThat(solver.model().literals()).containsExactlyInAnyOrder( this.f.variable("a"), this.f.variable("b"), this.f.variable("c") diff --git a/core/src/test/java/org/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java b/core/src/test/java/org/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java index 5be2ca8e..97679b8c 100644 --- a/core/src/test/java/org/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java +++ b/core/src/test/java/org/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java @@ -40,7 +40,6 @@ import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.handlers.TimeoutMaxSATHandler; -import org.logicng.io.parsers.ParserException; import org.logicng.solvers.MaxSATSolver; import org.logicng.solvers.maxsat.algorithms.MaxSAT; import org.logicng.solvers.maxsat.algorithms.MaxSATConfig; @@ -88,7 +87,7 @@ public PartialWeightedMaxSATTest() throws FileNotFoundException { public void testExceptionalBehaviorForWMSU3() { assertThatThrownBy(() -> { final MaxSATSolver solver = MaxSATSolver.wmsu3(this.f); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, 1); solver.solve(); }).isInstanceOf(IllegalStateException.class) @@ -99,7 +98,7 @@ public void testExceptionalBehaviorForWMSU3() { .incremental(MaxSATConfig.IncrementalStrategy.ITERATIVE) .cardinality(CardinalityEncoding.MTOTALIZER) .build()); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, 2); solver.solve(); }).isInstanceOf(IllegalStateException.class) @@ -309,15 +308,15 @@ public void testTimeoutHandlerLineaerSUBMO() { } @Test - public void testWeightedNonClauselSoftConstraints() throws ParserException { + public void testWeightedNonClauselSoftConstraints() { final MaxSATSolver[] solvers = new MaxSATSolver[4]; solvers[0] = MaxSATSolver.incWBO(this.f); solvers[1] = MaxSATSolver.linearSU(this.f); solvers[2] = MaxSATSolver.wbo(this.f); solvers[3] = MaxSATSolver.wmsu3(this.f); for (final MaxSATSolver solver : solvers) { - solver.addHardFormula(this.f.parse("a & b & c")); - solver.addSoftFormula(this.f.parse("~a & ~b & ~c"), 2); + solver.addHardFormula(parse(this.f, "a & b & c")); + solver.addSoftFormula(parse(this.f, "~a & ~b & ~c"), 2); assertThat(solver.solve()).isEqualTo(MaxSAT.MaxSATResult.OPTIMUM); assertThat(solver.model().literals()).containsExactlyInAnyOrder( this.f.variable("a"), this.f.variable("b"), this.f.variable("c") @@ -328,16 +327,16 @@ public void testWeightedNonClauselSoftConstraints() throws ParserException { } @Test - public void testWeightedSoftConstraintsCornerCaseVerum() throws ParserException { + public void testWeightedSoftConstraintsCornerCaseVerum() { final MaxSATSolver[] solvers = new MaxSATSolver[4]; solvers[0] = MaxSATSolver.incWBO(this.f); solvers[1] = MaxSATSolver.linearSU(this.f); solvers[2] = MaxSATSolver.wbo(this.f); solvers[3] = MaxSATSolver.wmsu3(this.f); for (final MaxSATSolver solver : solvers) { - solver.addHardFormula(this.f.parse("a & b & c")); - solver.addSoftFormula(this.f.parse("$true"), 2); - solver.addSoftFormula(this.f.parse("~a & ~b & ~c"), 3); + solver.addHardFormula(parse(this.f, "a & b & c")); + solver.addSoftFormula(parse(this.f, "$true"), 2); + solver.addSoftFormula(parse(this.f, "~a & ~b & ~c"), 3); assertThat(solver.solve()).isEqualTo(MaxSAT.MaxSATResult.OPTIMUM); assertThat(solver.model().literals()).containsExactlyInAnyOrder( this.f.variable("a"), this.f.variable("b"), this.f.variable("c") @@ -347,16 +346,16 @@ public void testWeightedSoftConstraintsCornerCaseVerum() throws ParserException } @Test - public void testWeightedSoftConstraintsCornerCaseFalsum() throws ParserException { + public void testWeightedSoftConstraintsCornerCaseFalsum() { final MaxSATSolver[] solvers = new MaxSATSolver[4]; solvers[0] = MaxSATSolver.incWBO(this.f); solvers[1] = MaxSATSolver.linearSU(this.f); solvers[2] = MaxSATSolver.wbo(this.f); solvers[3] = MaxSATSolver.wmsu3(this.f); for (final MaxSATSolver solver : solvers) { - solver.addHardFormula(this.f.parse("a & b & c")); - solver.addSoftFormula(this.f.parse("$false"), 2); - solver.addSoftFormula(this.f.parse("~a & ~b & ~c"), 3); + solver.addHardFormula(parse(this.f, "a & b & c")); + solver.addSoftFormula(parse(this.f, "$false"), 2); + solver.addSoftFormula(parse(this.f, "~a & ~b & ~c"), 3); assertThat(solver.solve()).isEqualTo(MaxSAT.MaxSATResult.OPTIMUM); assertThat(solver.model().literals()).containsExactlyInAnyOrder( this.f.variable("a"), this.f.variable("b"), this.f.variable("c") diff --git a/core/src/test/java/org/logicng/solvers/maxsat/PureMaxSATTest.java b/core/src/test/java/org/logicng/solvers/maxsat/PureMaxSATTest.java index f9b12b4f..9f1df46a 100644 --- a/core/src/test/java/org/logicng/solvers/maxsat/PureMaxSATTest.java +++ b/core/src/test/java/org/logicng/solvers/maxsat/PureMaxSATTest.java @@ -78,7 +78,7 @@ public PureMaxSATTest() throws FileNotFoundException { public void testExceptionalBehavior() { assertThatThrownBy(() -> { final MaxSATSolver solver = MaxSATSolver.incWBO(this.f); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, 1); solver.solve(); solver.addHardFormula(this.B); @@ -86,7 +86,7 @@ public void testExceptionalBehavior() { .hasMessage("The MaxSAT solver does currently not support an incremental interface. Reset the solver."); assertThatThrownBy(() -> { final MaxSATSolver solver = MaxSATSolver.incWBO(this.f); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, 1); solver.solve(); solver.addSoftFormula(this.B, 1); @@ -94,20 +94,20 @@ public void testExceptionalBehavior() { .hasMessage("The MaxSAT solver does currently not support an incremental interface. Reset the solver."); assertThatThrownBy(() -> { final MaxSATSolver solver = MaxSATSolver.incWBO(this.f); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, -1); }).isInstanceOf(IllegalArgumentException.class) .hasMessage("The weight of a formula must be > 0"); assertThatThrownBy(() -> { final MaxSATSolver solver = MaxSATSolver.incWBO(this.f); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, 1); solver.result(); }).isInstanceOf(IllegalStateException.class) .hasMessage("Cannot get a result as long as the formula is not solved. Call 'solver' first."); assertThatThrownBy(() -> { final MaxSATSolver solver = MaxSATSolver.incWBO(this.f); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, 1); solver.model(); }).isInstanceOf(IllegalStateException.class) @@ -118,7 +118,7 @@ public void testExceptionalBehavior() { public void testExceptionalBehaviorForLinearUS() { assertThatThrownBy(() -> { final MaxSATSolver solver = MaxSATSolver.linearUS(this.f); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, 3); solver.solve(); }).isInstanceOf(IllegalStateException.class) @@ -128,7 +128,7 @@ public void testExceptionalBehaviorForLinearUS() { .incremental(MaxSATConfig.IncrementalStrategy.ITERATIVE) .cardinality(CardinalityEncoding.MTOTALIZER) .build()); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addSoftFormula(this.A, 1); solver.solve(); }).isInstanceOf(IllegalStateException.class) @@ -136,9 +136,9 @@ public void testExceptionalBehaviorForLinearUS() { } @Test - public void testCornerCase() throws ParserException { + public void testCornerCase() { final MaxSATSolver solver = MaxSATSolver.incWBO(this.f); - solver.addHardFormula(this.f.parse("a | b")); + solver.addHardFormula(parse(this.f, "a | b")); solver.addHardFormula(this.f.verum()); solver.addSoftFormula(this.A, 1); MaxSAT.MaxSATResult result = solver.solve(); diff --git a/core/src/test/java/org/logicng/solvers/sat/MiniSatTest.java b/core/src/test/java/org/logicng/solvers/sat/MiniSatTest.java index 3ad02c14..d590275b 100644 --- a/core/src/test/java/org/logicng/solvers/sat/MiniSatTest.java +++ b/core/src/test/java/org/logicng/solvers/sat/MiniSatTest.java @@ -30,13 +30,13 @@ import static org.assertj.core.api.Assertions.assertThat; import static org.assertj.core.api.Assertions.assertThatThrownBy; +import static org.logicng.TestWithExampleFormulas.parse; import static org.logicng.datastructures.Tristate.FALSE; import static org.logicng.datastructures.Tristate.TRUE; import org.junit.jupiter.api.Test; import org.logicng.collections.LNGIntVector; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; @@ -127,10 +127,10 @@ public void testConfig() { } @Test - public void testAssumptionChecking() throws ParserException { + public void testAssumptionChecking() { final FormulaFactory f = new FormulaFactory(); final SATSolver solver = MiniSat.miniSat(f); - solver.add(f.parse("A & B")); + solver.add(parse(f, "A & B")); assertThat(solver.sat()).isEqualTo(TRUE); assertThat(solver.sat(f.literal("A", true))).isEqualTo(TRUE); assertThat(solver.sat(f.literal("B", true))).isEqualTo(TRUE); diff --git a/core/src/test/java/org/logicng/solvers/sat/SATTest.java b/core/src/test/java/org/logicng/solvers/sat/SATTest.java index d2949650..0e833039 100644 --- a/core/src/test/java/org/logicng/solvers/sat/SATTest.java +++ b/core/src/test/java/org/logicng/solvers/sat/SATTest.java @@ -391,11 +391,11 @@ public void testWithRelaxation() throws ParserException { } @Test - public void testRelaxationFormulas() throws ParserException { + public void testRelaxationFormulas() { for (final SATSolver s : this.solvers) { - s.add(this.f.parse("a & (b | c)")); + s.add(parse(this.f, "a & (b | c)")); assertSolverSat(s); - s.addWithRelaxation(this.f.variable("x"), this.f.parse("~a & ~b")); + s.addWithRelaxation(this.f.variable("x"), parse(this.f, "~a & ~b")); assertSolverSat(s); assertThat(s.model().positiveVariables()).contains(this.f.variable("x")); s.add(this.f.variable("x").negate()); @@ -875,7 +875,7 @@ public void testAddWithoutUnknown() throws ParserException { public void testUPZeroLiteralsForUndefState() { assertThatThrownBy(() -> { final SATSolver solver = MiniSat.miniSat(this.f); - solver.add(this.f.parse("a & b")); + solver.add(parse(this.f, "a & b")); solver.execute(UpZeroLiteralsFunction.get()); }).isInstanceOf(IllegalStateException.class) .hasMessage("Cannot get unit propagated literals on level 0 as long as the formula is not solved. Call 'sat' first."); @@ -969,22 +969,22 @@ public void testFormulaOnSolver() throws ParserException { } @Test - public void testFormulaOnSolverWithContradiction() throws ParserException { + public void testFormulaOnSolverWithContradiction() { for (final SATSolver solver : this.solvers) { if (solver instanceof MiniSat) { solver.add(this.f.variable("A")); solver.add(this.f.variable("B")); - solver.add(this.f.parse("C & (~A | ~B)")); + solver.add(parse(this.f, "C & (~A | ~B)")); assertThat(solver.execute(FormulaOnSolverFunction.get())) .containsExactlyInAnyOrder(this.f.variable("A"), this.f.variable("B"), this.f.variable("C"), this.f.falsum()); solver.reset(); - solver.add(this.f.parse("A <=> B")); - solver.add(this.f.parse("B <=> ~A")); + solver.add(parse(this.f, "A <=> B")); + solver.add(parse(this.f, "B <=> ~A")); assertThat(solver.execute(FormulaOnSolverFunction.get())) - .containsExactlyInAnyOrder(this.f.parse("A | ~B"), this.f.parse("~A | B"), this.f.parse("~B | ~A"), this.f.parse("B | A")); + .containsExactlyInAnyOrder(parse(this.f, "A | ~B"), parse(this.f, "~A | B"), parse(this.f, "~B | ~A"), parse(this.f, "B | A")); solver.sat(); assertThat(solver.execute(FormulaOnSolverFunction.get())) - .containsExactlyInAnyOrder(this.f.parse("A | ~B"), this.f.parse("~A | B"), this.f.parse("~B | ~A"), this.f.parse("B | A"), + .containsExactlyInAnyOrder(parse(this.f, "A | ~B"), parse(this.f, "~A | B"), parse(this.f, "~B | ~A"), parse(this.f, "B | A"), this.f.variable("A"), this.f.variable("B"), this.f.falsum()); } } @@ -1105,9 +1105,9 @@ public void testDimacsFilesWithSelectionOrder() throws IOException { } @Test - public void testModelEnumerationWithAdditionalVariables() throws ParserException { + public void testModelEnumerationWithAdditionalVariables() { final SATSolver solver = MiniSat.miniSat(this.f); - solver.add(this.f.parse("A | B | C | D | E")); + solver.add(parse(this.f, "A | B | C | D | E")); final List models = solver.execute(ModelEnumerationFunction.builder() .variables(Arrays.asList(this.f.variable("A"), this.f.variable("B"))) .additionalVariables(Arrays.asList(this.f.variable("B"), this.f.variable("C"))).build()); diff --git a/core/src/test/java/org/logicng/transformations/LiteralSubstitutionTest.java b/core/src/test/java/org/logicng/transformations/LiteralSubstitutionTest.java index 5955541d..ec994d07 100644 --- a/core/src/test/java/org/logicng/transformations/LiteralSubstitutionTest.java +++ b/core/src/test/java/org/logicng/transformations/LiteralSubstitutionTest.java @@ -29,12 +29,12 @@ package org.logicng.transformations; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Literal; -import org.logicng.io.parsers.ParserException; import java.util.HashMap; import java.util.Map; @@ -60,36 +60,36 @@ public void init() { } @Test - public void testSimpleFormula() throws ParserException { - assertThat(this.f.parse("$true").transform(this.s1)).isEqualTo(this.f.parse("$true")); - assertThat(this.f.parse("$false").transform(this.s1)).isEqualTo(this.f.parse("$false")); + public void testSimpleFormula() { + assertThat(parse(this.f, "$true").transform(this.s1)).isEqualTo(parse(this.f, "$true")); + assertThat(parse(this.f, "$false").transform(this.s1)).isEqualTo(parse(this.f, "$false")); } @Test - public void testLiterals() throws ParserException { - assertThat(this.f.parse("m").transform(this.s1)).isEqualTo(this.f.parse("m")); - assertThat(this.f.parse("~m").transform(this.s1)).isEqualTo(this.f.parse("~m")); - assertThat(this.f.parse("a").transform(this.s1)).isEqualTo(this.f.parse("a_t")); - assertThat(this.f.parse("~a").transform(this.s1)).isEqualTo(this.f.parse("a_f")); - assertThat(this.f.parse("b").transform(this.s1)).isEqualTo(this.f.parse("b")); - assertThat(this.f.parse("~b").transform(this.s1)).isEqualTo(this.f.parse("x")); - assertThat(this.f.parse("c").transform(this.s1)).isEqualTo(this.f.parse("y")); - assertThat(this.f.parse("~c").transform(this.s1)).isEqualTo(this.f.parse("~y")); + public void testLiterals() { + assertThat(parse(this.f, "m").transform(this.s1)).isEqualTo(parse(this.f, "m")); + assertThat(parse(this.f, "~m").transform(this.s1)).isEqualTo(parse(this.f, "~m")); + assertThat(parse(this.f, "a").transform(this.s1)).isEqualTo(parse(this.f, "a_t")); + assertThat(parse(this.f, "~a").transform(this.s1)).isEqualTo(parse(this.f, "a_f")); + assertThat(parse(this.f, "b").transform(this.s1)).isEqualTo(parse(this.f, "b")); + assertThat(parse(this.f, "~b").transform(this.s1)).isEqualTo(parse(this.f, "x")); + assertThat(parse(this.f, "c").transform(this.s1)).isEqualTo(parse(this.f, "y")); + assertThat(parse(this.f, "~c").transform(this.s1)).isEqualTo(parse(this.f, "~y")); } @Test - public void testFormulas() throws ParserException { - assertThat(this.f.parse("~(a & b & ~c & x)").transform(this.s1)).isEqualTo(this.f.parse("~(a_t & b & ~y & x)")); - assertThat(this.f.parse("a & b & ~c & x").transform(this.s1)).isEqualTo(this.f.parse("a_t & b & ~y & x")); - assertThat(this.f.parse("a | b | ~c | x").transform(this.s1)).isEqualTo(this.f.parse("a_t | b | ~y | x")); - assertThat(this.f.parse("(a | b) => (~c | x)").transform(this.s1)).isEqualTo(this.f.parse("(a_t | b) => (~y | x)")); - assertThat(this.f.parse("(a | b) <=> (~c | x)").transform(this.s1)).isEqualTo(this.f.parse("(a_t | b) <=> (~y | x)")); - assertThat(this.f.parse("2*a + 3*~b + -4*~c + x <= 5").transform(this.s1)).isEqualTo(this.f.parse("2*a_t + 3*x + -4*~y + x <= 5")); + public void testFormulas() { + assertThat(parse(this.f, "~(a & b & ~c & x)").transform(this.s1)).isEqualTo(parse(this.f, "~(a_t & b & ~y & x)")); + assertThat(parse(this.f, "a & b & ~c & x").transform(this.s1)).isEqualTo(parse(this.f, "a_t & b & ~y & x")); + assertThat(parse(this.f, "a | b | ~c | x").transform(this.s1)).isEqualTo(parse(this.f, "a_t | b | ~y | x")); + assertThat(parse(this.f, "(a | b) => (~c | x)").transform(this.s1)).isEqualTo(parse(this.f, "(a_t | b) => (~y | x)")); + assertThat(parse(this.f, "(a | b) <=> (~c | x)").transform(this.s1)).isEqualTo(parse(this.f, "(a_t | b) <=> (~y | x)")); + assertThat(parse(this.f, "2*a + 3*~b + -4*~c + x <= 5").transform(this.s1)).isEqualTo(parse(this.f, "2*a_t + 3*x + -4*~y + x <= 5")); } @Test - public void testEmptySubstitution() throws ParserException { - assertThat(this.f.parse("2*a + 3*~b + -4*~c + x <= 5").transform(new LiteralSubstitution())).isEqualTo(this.f.parse("2*a + 3*~b + -4*~c + x <= 5")); + public void testEmptySubstitution() { + assertThat(parse(this.f, "2*a + 3*~b + -4*~c + x <= 5").transform(new LiteralSubstitution())).isEqualTo(parse(this.f, "2*a + 3*~b + -4*~c + x <= 5")); } } diff --git a/core/src/test/java/org/logicng/transformations/PureExpansionTransformationTest.java b/core/src/test/java/org/logicng/transformations/PureExpansionTransformationTest.java index ea2bfcc6..f804d381 100644 --- a/core/src/test/java/org/logicng/transformations/PureExpansionTransformationTest.java +++ b/core/src/test/java/org/logicng/transformations/PureExpansionTransformationTest.java @@ -40,7 +40,6 @@ import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Not; import org.logicng.formulas.PBConstraint; -import org.logicng.io.parsers.ParserException; import org.logicng.modelcounting.ModelCounter; import org.logicng.predicates.satisfiability.TautologyPredicate; import org.logicng.util.FormulaCornerCases; @@ -71,20 +70,20 @@ public void testLiterals() { } @Test - public void testNot() throws ParserException { + public void testNot() { assertThat(this.NOT1.transform(transformation)).isEqualTo(this.NOT1); assertThat(this.NOT2.transform(transformation)).isEqualTo(this.NOT2); - assertThat(this.f.parse("~a").transform(transformation)).isEqualTo(this.f.parse("~a")); - assertThat(this.f.parse("~(a => b)").transform(transformation)).isEqualTo(this.f.parse("~(a => b)")); - assertThat(this.f.parse("~(~(a | b) => ~(x | y))").transform(transformation)).isEqualTo(this.f.parse("~(~(a | b) => ~(x | y))")); - assertThat(this.f.parse("~(a <=> b)").transform(transformation)).isEqualTo(this.f.parse("~(a <=> b)")); - assertThat(this.f.parse("~(a & b & ~x & ~y)").transform(transformation)).isEqualTo(this.f.parse("~(a & b & ~x & ~y)")); - assertThat(this.f.parse("~(a | b | (a + b <= 1) | ~y)").transform(transformation)).isEqualTo(this.f.parse("~(a | b | (~a | ~b) | ~y)")); + assertThat(parse(this.f, "~a").transform(transformation)).isEqualTo(parse(this.f, "~a")); + assertThat(parse(this.f, "~(a => b)").transform(transformation)).isEqualTo(parse(this.f, "~(a => b)")); + assertThat(parse(this.f, "~(~(a | b) => ~(x | y))").transform(transformation)).isEqualTo(parse(this.f, "~(~(a | b) => ~(x | y))")); + assertThat(parse(this.f, "~(a <=> b)").transform(transformation)).isEqualTo(parse(this.f, "~(a <=> b)")); + assertThat(parse(this.f, "~(a & b & ~x & ~y)").transform(transformation)).isEqualTo(parse(this.f, "~(a & b & ~x & ~y)")); + assertThat(parse(this.f, "~(a | b | (a + b <= 1) | ~y)").transform(transformation)).isEqualTo(parse(this.f, "~(a | b | (~a | ~b) | ~y)")); } @Test - public void testBinaryOperators() throws ParserException { + public void testBinaryOperators() { assertThat(this.IMP1.transform(transformation)).isEqualTo(this.IMP1); assertThat(this.IMP2.transform(transformation)).isEqualTo(this.IMP2); assertThat(this.IMP3.transform(transformation)).isEqualTo(this.IMP3); @@ -94,11 +93,11 @@ public void testBinaryOperators() throws ParserException { assertThat(this.EQ3.transform(transformation)).isEqualTo(this.EQ3); assertThat(this.EQ4.transform(transformation)).isEqualTo(this.EQ4); - assertThat(this.f.parse("~(a => (a + b = 1))").transform(transformation)).isEqualTo(this.f.parse("~(a => (a | b) & (~a | ~b))")); + assertThat(parse(this.f, "~(a => (a + b = 1))").transform(transformation)).isEqualTo(parse(this.f, "~(a => (a | b) & (~a | ~b))")); } @Test - public void testNAryOperators() throws ParserException { + public void testNAryOperators() { assertThat(this.AND1.transform(transformation)).isEqualTo(this.AND1); assertThat(this.AND2.transform(transformation)).isEqualTo(this.AND2); assertThat(this.AND3.transform(transformation)).isEqualTo(this.AND3); @@ -106,20 +105,20 @@ public void testNAryOperators() throws ParserException { assertThat(this.OR2.transform(transformation)).isEqualTo(this.OR2); assertThat(this.OR3.transform(transformation)).isEqualTo(this.OR3); - assertThat(this.f.parse("~(a & b) | c | ~(x | ~y)").transform(transformation)).isEqualTo(this.f.parse("~(a & b) | c | ~(x | ~y)")); - assertThat(this.f.parse("~(a | b) & (a + b = 1) & ~(x & ~(z + x = 1))").transform(transformation)) - .isEqualTo(this.f.parse("~(a | b) & ((a | b) & (~a | ~b)) & ~(x & ~((z | x) & (~z | ~x)))")); - assertThat(this.f.parse("a & b & (~x | ~y)").transform(transformation)).isEqualTo(this.f.parse("a & b & (~x | ~y)")); - assertThat(this.f.parse("~(a | b) & c & ~(x & ~y) & (w => z)").transform(transformation)).isEqualTo(this.f.parse("~(a | b) & c & ~(x & ~y) & (w => z)")); - assertThat(this.f.parse("~(a & b) | c | ~(x | ~y)").transform(transformation)).isEqualTo(this.f.parse("~(a & b) | c | ~(x | ~y)")); - assertThat(this.f.parse("a | b | (~x & ~y)").transform(transformation)).isEqualTo(this.f.parse("a | b | (~x & ~y)")); + assertThat(parse(this.f, "~(a & b) | c | ~(x | ~y)").transform(transformation)).isEqualTo(parse(this.f, "~(a & b) | c | ~(x | ~y)")); + assertThat(parse(this.f, "~(a | b) & (a + b = 1) & ~(x & ~(z + x = 1))").transform(transformation)) + .isEqualTo(parse(this.f, "~(a | b) & ((a | b) & (~a | ~b)) & ~(x & ~((z | x) & (~z | ~x)))")); + assertThat(parse(this.f, "a & b & (~x | ~y)").transform(transformation)).isEqualTo(parse(this.f, "a & b & (~x | ~y)")); + assertThat(parse(this.f, "~(a | b) & c & ~(x & ~y) & (w => z)").transform(transformation)).isEqualTo(parse(this.f, "~(a | b) & c & ~(x & ~y) & (w => z)")); + assertThat(parse(this.f, "~(a & b) | c | ~(x | ~y)").transform(transformation)).isEqualTo(parse(this.f, "~(a & b) | c | ~(x | ~y)")); + assertThat(parse(this.f, "a | b | (~x & ~y)").transform(transformation)).isEqualTo(parse(this.f, "a | b | (~x & ~y)")); } @Test - public void testPBCs() throws ParserException { - assertThat(this.f.parse("a + b <= 1").transform(transformation)).isEqualTo(this.f.parse("~a | ~b")); - assertThat(this.f.parse("a + b < 2").transform(transformation)).isEqualTo(this.f.parse("~a | ~b")); - assertThat(this.f.parse("a + b = 1").transform(transformation)).isEqualTo(this.f.parse("(a | b) & (~a | ~b)")); + public void testPBCs() { + assertThat(parse(this.f, "a + b <= 1").transform(transformation)).isEqualTo(parse(this.f, "~a | ~b")); + assertThat(parse(this.f, "a + b < 2").transform(transformation)).isEqualTo(parse(this.f, "~a | ~b")); + assertThat(parse(this.f, "a + b = 1").transform(transformation)).isEqualTo(parse(this.f, "(a | b) & (~a | ~b)")); } @Test diff --git a/core/src/test/java/org/logicng/transformations/cnf/CanonicalCNFEnumerationTest.java b/core/src/test/java/org/logicng/transformations/cnf/CanonicalCNFEnumerationTest.java index c55b48d8..2d97934a 100644 --- a/core/src/test/java/org/logicng/transformations/cnf/CanonicalCNFEnumerationTest.java +++ b/core/src/test/java/org/logicng/transformations/cnf/CanonicalCNFEnumerationTest.java @@ -1,12 +1,12 @@ package org.logicng.transformations.cnf; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.logicng.RandomTag; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.predicates.CNFPredicate; import org.logicng.predicates.satisfiability.TautologyPredicate; import org.logicng.util.FormulaCornerCases; @@ -21,21 +21,21 @@ public class CanonicalCNFEnumerationTest { @Test - public void testSamples() throws ParserException { + public void testSamples() { final FormulaFactory f = new FormulaFactory(); - assertThat(f.falsum().transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("$false")); - assertThat(f.verum().transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("$true")); - assertThat(f.parse("a").transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("a")); - assertThat(f.parse("~a").transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("~a")); - assertThat(f.parse("~a & b").transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("(~a | b) & (~a | ~b) & (a | b)")); - assertThat(f.parse("~a | b").transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("~a | b")); - assertThat(f.parse("a => b").transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("~a | b")); - assertThat(f.parse("a <=> b").transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("(~a | b) & (a | ~b)")); - assertThat(f.parse("a + b = 1").transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("(a | b) & (~a | ~b)")); - assertThat(f.parse("a & (b | ~c)").transform(CanonicalCNFEnumeration.get())) - .isEqualTo(f.parse("(a | b | c) & (a | b | ~c) & (a | ~b | c) & (a | ~b | ~c) & (~a | b | ~c)")); - assertThat(f.parse("a & b & (~a | ~b)").transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("(a | b) & (~a | b) & (~a | ~b) & (a | ~b)")); - assertThat(f.parse("a | b | ~a & ~b").transform(CanonicalCNFEnumeration.get())).isEqualTo(f.parse("$true")); + assertThat(f.falsum().transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "$false")); + assertThat(f.verum().transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "$true")); + assertThat(parse(f, "a").transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "a")); + assertThat(parse(f, "~a").transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "~a")); + assertThat(parse(f, "~a & b").transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "(~a | b) & (~a | ~b) & (a | b)")); + assertThat(parse(f, "~a | b").transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "~a | b")); + assertThat(parse(f, "a => b").transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "~a | b")); + assertThat(parse(f, "a <=> b").transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "(~a | b) & (a | ~b)")); + assertThat(parse(f, "a + b = 1").transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "(a | b) & (~a | ~b)")); + assertThat(parse(f, "a & (b | ~c)").transform(CanonicalCNFEnumeration.get())) + .isEqualTo(parse(f, "(a | b | c) & (a | b | ~c) & (a | ~b | c) & (a | ~b | ~c) & (~a | b | ~c)")); + assertThat(parse(f, "a & b & (~a | ~b)").transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "(a | b) & (~a | b) & (~a | ~b) & (a | ~b)")); + assertThat(parse(f, "a | b | ~a & ~b").transform(CanonicalCNFEnumeration.get())).isEqualTo(parse(f, "$true")); } @Test diff --git a/core/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformationSolverTest.java b/core/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformationSolverTest.java index 550cb9a7..c87a0ccc 100644 --- a/core/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformationSolverTest.java +++ b/core/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformationSolverTest.java @@ -37,7 +37,6 @@ import org.logicng.datastructures.Tristate; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.predicates.satisfiability.SATPredicate; import org.logicng.predicates.satisfiability.TautologyPredicate; import org.logicng.solvers.MiniSat; @@ -118,29 +117,29 @@ private static Formula randomSATFormula(final FormulaRandomizer randomizer, fina } @Test - public void simple() throws ParserException { - computeAndVerify(this.f.parse("(X => (A & B)) | ~(A & B)")); - computeAndVerify(this.f.parse("~((A | (C & D)) & ((X & ~Z) | (H & E)))")); + public void simple() { + computeAndVerify(parse(this.f, "(X => (A & B)) | ~(A & B)")); + computeAndVerify(parse(this.f, "~((A | (C & D)) & ((X & ~Z) | (H & E)))")); - computeAndVerify(this.f.parse("A | (B | ~C) & (D | ~E)")); - computeAndVerify(this.f.parse("A | B & (C | D)")); + computeAndVerify(parse(this.f, "A | (B | ~C) & (D | ~E)")); + computeAndVerify(parse(this.f, "A | B & (C | D)")); - computeAndVerify(this.f.parse("~(A&B)|X")); - computeAndVerify(this.f.parse("~(~(A&B)|X)")); + computeAndVerify(parse(this.f, "~(A&B)|X")); + computeAndVerify(parse(this.f, "~(~(A&B)|X)")); - computeAndVerify(this.f.parse("~(~(A&B)|X)")); - computeAndVerify(this.f.parse("~(A&B=>X)")); + computeAndVerify(parse(this.f, "~(~(A&B)|X)")); + computeAndVerify(parse(this.f, "~(A&B=>X)")); - computeAndVerify(this.f.parse("A&B => X")); - computeAndVerify(this.f.parse("~(A&B=>X)")); + computeAndVerify(parse(this.f, "A&B => X")); + computeAndVerify(parse(this.f, "~(A&B=>X)")); - computeAndVerify(this.f.parse("A&B <=> X")); - computeAndVerify(this.f.parse("~(A&B<=>X)")); + computeAndVerify(parse(this.f, "A&B <=> X")); + computeAndVerify(parse(this.f, "~(A&B<=>X)")); - computeAndVerify(this.f.parse("~(A&B)")); + computeAndVerify(parse(this.f, "~(A&B)")); - computeAndVerify(this.f.parse("A & (B | A => (A <=> ~B))")); - computeAndVerify(this.f.parse("(A => ~A) <=> (B <=> (~A => B))")); + computeAndVerify(parse(this.f, "A & (B | A => (A <=> ~B))")); + computeAndVerify(parse(this.f, "(A => ~A) <=> (B <=> (~A => B))")); } private static void computeAndVerify(final Formula formula) { diff --git a/core/src/test/java/org/logicng/transformations/dnf/CanonicalDNFEnumerationTest.java b/core/src/test/java/org/logicng/transformations/dnf/CanonicalDNFEnumerationTest.java index f5947e6d..a14547df 100644 --- a/core/src/test/java/org/logicng/transformations/dnf/CanonicalDNFEnumerationTest.java +++ b/core/src/test/java/org/logicng/transformations/dnf/CanonicalDNFEnumerationTest.java @@ -1,12 +1,12 @@ package org.logicng.transformations.dnf; import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.TestWithExampleFormulas.parse; import org.junit.jupiter.api.Test; import org.logicng.RandomTag; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.predicates.DNFPredicate; import org.logicng.predicates.satisfiability.ContradictionPredicate; import org.logicng.predicates.satisfiability.TautologyPredicate; @@ -22,20 +22,20 @@ public class CanonicalDNFEnumerationTest { @Test - public void testSamples() throws ParserException { + public void testSamples() { final FormulaFactory f = new FormulaFactory(); - assertThat(f.falsum().transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("$false")); - assertThat(f.verum().transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("$true")); - assertThat(f.parse("a").transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("a")); - assertThat(f.parse("~a").transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("~a")); - assertThat(f.parse("~a & b").transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("~a & b")); - assertThat(f.parse("~a | b").transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("~a & ~b | ~a & b | a & b")); - assertThat(f.parse("a => b").transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("~a & ~b | ~a & b | a & b")); - assertThat(f.parse("a <=> b").transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("a & b | ~a & ~b")); - assertThat(f.parse("a + b = 1").transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("~a & b | a & ~b")); - assertThat(f.parse("a & (b | ~c)").transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("a & b & c | a & b & ~c | a & ~b & ~c")); - assertThat(f.parse("a & b & (~a | ~b)").transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("$false")); - assertThat(f.parse("a | b | ~a & ~b").transform(CanonicalDNFEnumeration.get())).isEqualTo(f.parse("~a & b | a & b | a & ~b | ~a & ~b")); + assertThat(f.falsum().transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "$false")); + assertThat(f.verum().transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "$true")); + assertThat(parse(f, "a").transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "a")); + assertThat(parse(f, "~a").transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "~a")); + assertThat(parse(f, "~a & b").transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "~a & b")); + assertThat(parse(f, "~a | b").transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "~a & ~b | ~a & b | a & b")); + assertThat(parse(f, "a => b").transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "~a & ~b | ~a & b | a & b")); + assertThat(parse(f, "a <=> b").transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "a & b | ~a & ~b")); + assertThat(parse(f, "a + b = 1").transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "~a & b | a & ~b")); + assertThat(parse(f, "a & (b | ~c)").transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "a & b & c | a & b & ~c | a & ~b & ~c")); + assertThat(parse(f, "a & b & (~a | ~b)").transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "$false")); + assertThat(parse(f, "a | b | ~a & ~b").transform(CanonicalDNFEnumeration.get())).isEqualTo(parse(f, "~a & b | a & b | a & ~b | ~a & ~b")); } @Test diff --git a/core/src/test/java/org/logicng/transformations/qmc/QuineMcCluskeyTest.java b/core/src/test/java/org/logicng/transformations/qmc/QuineMcCluskeyTest.java index d7a357f3..184a7e26 100644 --- a/core/src/test/java/org/logicng/transformations/qmc/QuineMcCluskeyTest.java +++ b/core/src/test/java/org/logicng/transformations/qmc/QuineMcCluskeyTest.java @@ -113,7 +113,7 @@ public void testLarge1() throws ParserException { } @Test - public void testLarge2() throws ParserException, IOException { + public void testLarge2() throws IOException, ParserException { final FormulaFactory f = new FormulaFactory(); final Formula formula = FormulaReader.readPseudoBooleanFormula("src/test/resources/formulas/large_formula.txt", f); final SATSolver solver = MiniSat.miniSat(f); @@ -140,7 +140,7 @@ public void testLarge2() throws ParserException, IOException { } @Test - public void testLarge3() throws ParserException, IOException { + public void testLarge3() throws IOException, ParserException { final FormulaFactory f = new FormulaFactory(); final Formula formula = FormulaReader.readPseudoBooleanFormula("src/test/resources/formulas/large_formula.txt", f); final SATSolver solver = MiniSat.miniSat(f); diff --git a/core/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java b/core/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java index fb26a82d..be2b3cad 100644 --- a/core/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java +++ b/core/src/test/java/org/logicng/transformations/simplification/AdvancedSimplifierTest.java @@ -84,20 +84,20 @@ public void testRandomized() { } @Test - public void testTimeoutHandlerSmall() throws ParserException { + public void testTimeoutHandlerSmall() { final List handlers = Arrays.asList( new TimeoutOptimizationHandler(5_000L, TimeoutHandler.TimerType.SINGLE_TIMEOUT), new TimeoutOptimizationHandler(5_000L, TimeoutHandler.TimerType.RESTARTING_TIMEOUT), new TimeoutOptimizationHandler(System.currentTimeMillis() + 5_000L, TimeoutHandler.TimerType.FIXED_END) ); - final Formula formula = this.f.parse("a & b | ~c & a"); + final Formula formula = parse(this.f, "a & b | ~c & a"); for (final TimeoutOptimizationHandler handler : handlers) { testHandler(handler, formula, false); } } @Test - public void testTimeoutHandlerLarge() throws ParserException, IOException { + public void testTimeoutHandlerLarge() throws IOException, ParserException { final List handlers = Arrays.asList( new TimeoutOptimizationHandler(1L, TimeoutHandler.TimerType.SINGLE_TIMEOUT), new TimeoutOptimizationHandler(1L, TimeoutHandler.TimerType.RESTARTING_TIMEOUT), @@ -110,24 +110,24 @@ public void testTimeoutHandlerLarge() throws ParserException, IOException { } @Test - public void testPrimeCompilerIsCancelled() throws ParserException { + public void testPrimeCompilerIsCancelled() { final OptimizationHandler handler = new BoundedOptimizationHandler(-1, 0); - final Formula formula = this.f.parse("a&(b|c)"); + final Formula formula = parse(this.f, "a&(b|c)"); testHandler(handler, formula, true); } @Test - public void testSmusComputationIsCancelled() throws ParserException { + public void testSmusComputationIsCancelled() { final OptimizationHandler handler = new BoundedOptimizationHandler(-1, 5); - final Formula formula = this.f.parse("a&(b|c)"); + final Formula formula = parse(this.f, "a&(b|c)"); testHandler(handler, formula, true); } @LongRunningTag @Test - public void testCancellationPoints() throws ParserException { + public void testCancellationPoints() { final FormulaFactory f = new FormulaFactory(); - final Formula formula = f.parse("~v16 & ~v22 & ~v12 & (~v4 | ~v14) & (~v4 | ~v15) & (v3 | v4) & (v3 | ~v14) & (v3 | ~v15) " + + final Formula formula = parse(f, "~v16 & ~v22 & ~v12 & (~v4 | ~v14) & (~v4 | ~v15) & (v3 | v4) & (v3 | ~v14) & (v3 | ~v15) " + "& (~v20 | ~v8) & (v9 | ~v20) & (~v21 | ~v8) & (v9 | ~v21) & (~v21 | ~v10) & (~v21 | ~v11) & v19"); for (int numOptimizationStarts = 1; numOptimizationStarts < 30; numOptimizationStarts++) { for (int numSatHandlerStarts = 1; numSatHandlerStarts < 500; numSatHandlerStarts++) { diff --git a/core/src/test/java/org/logicng/transformations/simplification/FactorOutSimplificationTest.java b/core/src/test/java/org/logicng/transformations/simplification/FactorOutSimplificationTest.java index 0f53cc5c..cc5711df 100644 --- a/core/src/test/java/org/logicng/transformations/simplification/FactorOutSimplificationTest.java +++ b/core/src/test/java/org/logicng/transformations/simplification/FactorOutSimplificationTest.java @@ -35,7 +35,6 @@ import org.logicng.TestWithExampleFormulas; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.predicates.satisfiability.TautologyPredicate; import org.logicng.util.FormulaCornerCases; import org.logicng.util.FormulaRandomizer; @@ -51,29 +50,29 @@ public class FactorOutSimplificationTest extends TestWithExampleFormulas { private final FactorOutSimplifier factorOut = new FactorOutSimplifier(); @Test - public void testSimple() throws ParserException { + public void testSimple() { assertThat(this.f.falsum().transform(this.factorOut)).isEqualTo(this.f.falsum()); assertThat(this.f.verum().transform(this.factorOut)).isEqualTo(this.f.verum()); assertThat(this.A.transform(this.factorOut)).isEqualTo(this.A); assertThat(this.NA.transform(this.factorOut)).isEqualTo(this.NA); - assertThat(this.f.parse("A&~B&~C&~D").transform(this.factorOut)).isEqualTo(this.f.parse("A&~B&~C&~D")); - assertThat(this.f.parse("~A&~B&~C&~D").transform(this.factorOut)).isEqualTo(this.f.parse("~A&~B&~C&~D")); + assertThat(parse(this.f, "A&~B&~C&~D").transform(this.factorOut)).isEqualTo(parse(this.f, "A&~B&~C&~D")); + assertThat(parse(this.f, "~A&~B&~C&~D").transform(this.factorOut)).isEqualTo(parse(this.f, "~A&~B&~C&~D")); - assertThat(this.f.parse("A|A&B").transform(this.factorOut)).isEqualTo(this.f.parse("A")); - assertThat(this.f.parse("A|A&B|C&D").transform(this.factorOut)).isEqualTo(this.f.parse("A|C&D")); - assertThat(this.f.parse("~(A&(A|B))").transform(this.factorOut)).isEqualTo(this.f.parse("~A")); - assertThat(this.f.parse("A|A&B|C").transform(this.factorOut)).isEqualTo(this.f.parse("A|C")); + assertThat(parse(this.f, "A|A&B").transform(this.factorOut)).isEqualTo(parse(this.f, "A")); + assertThat(parse(this.f, "A|A&B|C&D").transform(this.factorOut)).isEqualTo(parse(this.f, "A|C&D")); + assertThat(parse(this.f, "~(A&(A|B))").transform(this.factorOut)).isEqualTo(parse(this.f, "~A")); + assertThat(parse(this.f, "A|A&B|C").transform(this.factorOut)).isEqualTo(parse(this.f, "A|C")); - assertThat(this.f.parse("A&(A|B)").transform(this.factorOut)).isEqualTo(this.f.parse("A")); - assertThat(this.f.parse("A&(A|B)&(C|D)").transform(this.factorOut)).isEqualTo(this.f.parse("A&(C|D)")); - assertThat(this.f.parse("~(A|A&B)").transform(this.factorOut)).isEqualTo(this.f.parse("~A")); - assertThat(this.f.parse("A&(A|B)&C").transform(this.factorOut)).isEqualTo(this.f.parse("A&C")); + assertThat(parse(this.f, "A&(A|B)").transform(this.factorOut)).isEqualTo(parse(this.f, "A")); + assertThat(parse(this.f, "A&(A|B)&(C|D)").transform(this.factorOut)).isEqualTo(parse(this.f, "A&(C|D)")); + assertThat(parse(this.f, "~(A|A&B)").transform(this.factorOut)).isEqualTo(parse(this.f, "~A")); + assertThat(parse(this.f, "A&(A|B)&C").transform(this.factorOut)).isEqualTo(parse(this.f, "A&C")); - assertThat(this.f.parse("A&X&Y|A&B&C|B&C&D|A&Z").transform(this.factorOut)).isEqualTo(this.f.parse("A&(X&Y|B&C|Z)|B&C&D")); - assertThat(this.f.parse("G&(A&X&Y|A&B&C|B&C&D|A&Z)").transform(this.factorOut)).isEqualTo(this.f.parse("G&(A&(X&Y|B&C|Z)|B&C&D)")); + assertThat(parse(this.f, "A&X&Y|A&B&C|B&C&D|A&Z").transform(this.factorOut)).isEqualTo(parse(this.f, "A&(X&Y|B&C|Z)|B&C&D")); + assertThat(parse(this.f, "G&(A&X&Y|A&B&C|B&C&D|A&Z)").transform(this.factorOut)).isEqualTo(parse(this.f, "G&(A&(X&Y|B&C|Z)|B&C&D)")); - assertThat(this.f.parse("G&(~(A&X&Y)|~(A&B&C))").transform(this.factorOut)).isEqualTo(this.f.parse("G&(~(A&X&Y)|~(A&B&C))")); + assertThat(parse(this.f, "G&(~(A&X&Y)|~(A&B&C))").transform(this.factorOut)).isEqualTo(parse(this.f, "G&(~(A&X&Y)|~(A&B&C))")); } @Test diff --git a/core/src/test/java/org/logicng/transformations/simplification/NegationMinimizerTest.java b/core/src/test/java/org/logicng/transformations/simplification/NegationMinimizerTest.java index 39182431..b41410a3 100644 --- a/core/src/test/java/org/logicng/transformations/simplification/NegationMinimizerTest.java +++ b/core/src/test/java/org/logicng/transformations/simplification/NegationMinimizerTest.java @@ -35,7 +35,6 @@ import org.logicng.TestWithExampleFormulas; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; -import org.logicng.io.parsers.ParserException; import org.logicng.predicates.satisfiability.TautologyPredicate; import org.logicng.util.FormulaCornerCases; import org.logicng.util.FormulaRandomizer; @@ -51,43 +50,43 @@ public class NegationMinimizerTest extends TestWithExampleFormulas { private final NegationSimplifier minimizer = NegationSimplifier.get(); @Test - public void testSimple() throws ParserException { + public void testSimple() { assertThat(this.f.falsum().transform(this.minimizer)).isEqualTo(this.f.falsum()); assertThat(this.f.verum().transform(this.minimizer)).isEqualTo(this.f.verum()); assertThat(this.A.transform(this.minimizer)).isEqualTo(this.A); assertThat(this.NA.transform(this.minimizer)).isEqualTo(this.NA); - assertThat(this.f.parse("A&~B&~C&~D").transform(this.minimizer)).isEqualTo(this.f.parse("A&~B&~C&~D")); - assertThat(this.f.parse("~A&~B&~C&~D").transform(this.minimizer)).isEqualTo(this.f.parse("~(A|B|C|D)")); + assertThat(parse(this.f, "A&~B&~C&~D").transform(this.minimizer)).isEqualTo(parse(this.f, "A&~B&~C&~D")); + assertThat(parse(this.f, "~A&~B&~C&~D").transform(this.minimizer)).isEqualTo(parse(this.f, "~(A|B|C|D)")); - assertThat(this.f.parse("A|~B|~C|~D").transform(this.minimizer)).isEqualTo(this.f.parse("A|~B|~C|~D")); - assertThat(this.f.parse("~A|~B|~C|~D").transform(this.minimizer)).isEqualTo(this.f.parse("~(A&B&C&D)")); + assertThat(parse(this.f, "A|~B|~C|~D").transform(this.minimizer)).isEqualTo(parse(this.f, "A|~B|~C|~D")); + assertThat(parse(this.f, "~A|~B|~C|~D").transform(this.minimizer)).isEqualTo(parse(this.f, "~(A&B&C&D)")); - assertThat(this.f.parse("~A|~B|~C|D|~E|~G").transform(this.minimizer)).isEqualTo(this.f.parse("D|~(A&B&C&E&G)")); - assertThat(this.f.parse("~A&~B&~C&D&~E&~G").transform(this.minimizer)).isEqualTo(this.f.parse("D&~(A|B|C|E|G)")); + assertThat(parse(this.f, "~A|~B|~C|D|~E|~G").transform(this.minimizer)).isEqualTo(parse(this.f, "D|~(A&B&C&E&G)")); + assertThat(parse(this.f, "~A&~B&~C&D&~E&~G").transform(this.minimizer)).isEqualTo(parse(this.f, "D&~(A|B|C|E|G)")); - assertThat(this.f.parse("~A|~B|~E&G|~H&~B&~C|~X").transform(this.minimizer)).isEqualTo(this.f.parse("~E&G|~(A&B&(H|B|C)&X)")); - assertThat(this.f.parse("~(A&B&~(~E&G)&(H|B|C)&X)").transform(this.minimizer)).isEqualTo(this.f.parse("~E&G|~(A&B&(H|B|C)&X)")); + assertThat(parse(this.f, "~A|~B|~E&G|~H&~B&~C|~X").transform(this.minimizer)).isEqualTo(parse(this.f, "~E&G|~(A&B&(H|B|C)&X)")); + assertThat(parse(this.f, "~(A&B&~(~E&G)&(H|B|C)&X)").transform(this.minimizer)).isEqualTo(parse(this.f, "~E&G|~(A&B&(H|B|C)&X)")); - assertThat(this.f.parse("~A|B|(~E&~G&~H&~K)").transform(this.minimizer)).isEqualTo(this.f.parse("~A|B|~(E|G|H|K)")); + assertThat(parse(this.f, "~A|B|(~E&~G&~H&~K)").transform(this.minimizer)).isEqualTo(parse(this.f, "~A|B|~(E|G|H|K)")); - assertThat(this.f.parse("~A|~B").transform(this.minimizer)).isEqualTo(this.f.parse("~A|~B")); - assertThat(this.f.parse("~A|~B|~C").transform(this.minimizer)).isEqualTo(this.f.parse("~A|~B|~C")); - assertThat(this.f.parse("~A|~B|~C|~D").transform(this.minimizer)).isEqualTo(this.f.parse("~(A&B&C&D)")); + assertThat(parse(this.f, "~A|~B").transform(this.minimizer)).isEqualTo(parse(this.f, "~A|~B")); + assertThat(parse(this.f, "~A|~B|~C").transform(this.minimizer)).isEqualTo(parse(this.f, "~A|~B|~C")); + assertThat(parse(this.f, "~A|~B|~C|~D").transform(this.minimizer)).isEqualTo(parse(this.f, "~(A&B&C&D)")); - assertThat(this.f.parse("X&(~A|~B)").transform(this.minimizer)).isEqualTo(this.f.parse("X&~(A&B)")); - assertThat(this.f.parse("X&(~A|~B|~C)").transform(this.minimizer)).isEqualTo(this.f.parse("X&~(A&B&C)")); - assertThat(this.f.parse("X&(~A|~B|~C|~D)").transform(this.minimizer)).isEqualTo(this.f.parse("X&~(A&B&C&D)")); + assertThat(parse(this.f, "X&(~A|~B)").transform(this.minimizer)).isEqualTo(parse(this.f, "X&~(A&B)")); + assertThat(parse(this.f, "X&(~A|~B|~C)").transform(this.minimizer)).isEqualTo(parse(this.f, "X&~(A&B&C)")); + assertThat(parse(this.f, "X&(~A|~B|~C|~D)").transform(this.minimizer)).isEqualTo(parse(this.f, "X&~(A&B&C&D)")); - assertThat(this.f.parse("~A&~B").transform(this.minimizer)).isEqualTo(this.f.parse("~A&~B")); - assertThat(this.f.parse("~A&~B&~C").transform(this.minimizer)).isEqualTo(this.f.parse("~A&~B&~C")); - assertThat(this.f.parse("~A&~B&~C&~D").transform(this.minimizer)).isEqualTo(this.f.parse("~(A|B|C|D)")); + assertThat(parse(this.f, "~A&~B").transform(this.minimizer)).isEqualTo(parse(this.f, "~A&~B")); + assertThat(parse(this.f, "~A&~B&~C").transform(this.minimizer)).isEqualTo(parse(this.f, "~A&~B&~C")); + assertThat(parse(this.f, "~A&~B&~C&~D").transform(this.minimizer)).isEqualTo(parse(this.f, "~(A|B|C|D)")); - assertThat(this.f.parse("X|~A&~B").transform(this.minimizer)).isEqualTo(this.f.parse("X|~A&~B")); - assertThat(this.f.parse("X|~A&~B&~C").transform(this.minimizer)).isEqualTo(this.f.parse("X|~A&~B&~C")); - assertThat(this.f.parse("X|~A&~B&~C&~D").transform(this.minimizer)).isEqualTo(this.f.parse("X|~(A|B|C|D)")); + assertThat(parse(this.f, "X|~A&~B").transform(this.minimizer)).isEqualTo(parse(this.f, "X|~A&~B")); + assertThat(parse(this.f, "X|~A&~B&~C").transform(this.minimizer)).isEqualTo(parse(this.f, "X|~A&~B&~C")); + assertThat(parse(this.f, "X|~A&~B&~C&~D").transform(this.minimizer)).isEqualTo(parse(this.f, "X|~(A|B|C|D)")); - assertThat(this.f.parse("A&(~B|~C|~D|~E|~G|X|Y|H)").transform(this.minimizer)).isEqualTo(this.f.parse("A&(~(B&C&D&E&G)|X|Y|H)")); + assertThat(parse(this.f, "A&(~B|~C|~D|~E|~G|X|Y|H)").transform(this.minimizer)).isEqualTo(parse(this.f, "A&(~(B&C&D&E&G)|X|Y|H)")); } @Test diff --git a/parser/pom.xml b/parser/pom.xml new file mode 100644 index 00000000..c77afeac --- /dev/null +++ b/parser/pom.xml @@ -0,0 +1,309 @@ + + + + + + + + + + + + + + + + + + + + + + + + + 4.0.0 + + + org.logicng + logicng-pom + 2.5.0-SNAPSHOT + + + logicng + bundle + + + + + + org.antlr + antlr4-maven-plugin + ${version.antlr-plugin} + + src/main/antlr + target/generated-sources/antlr/org/logicng/io/parsers + + + + + antlr4 + + + + + + + org.apache.maven.plugins + maven-compiler-plugin + ${version.maven-compiler} + + + + + org.apache.maven.plugins + maven-jar-plugin + ${version.maven-jar} + + true + + + true + true + + + BooleWorks GmbH + logicng + + + + + + + + org.apache.maven.plugins + maven-source-plugin + ${version.maven-source} + + + attach-sources + + jar + + + + + + + + org.apache.maven.plugins + maven-javadoc-plugin + ${version.maven-javadoc} + + + attach-javadocs + + jar + + + + + + + + org.jacoco + jacoco-maven-plugin + ${version.jacoco} + + + **/LogicNGPropositional* + **/LogicNGPseudoBoolean* + + + + + default-prepare-agent + + prepare-agent + + + + default-report + prepare-package + + report + + + + default-check + + check + + + + + BUNDLE + + + + + + + + + + org.apache.felix + maven-bundle-plugin + ${version.osgi-plugin} + true + + + JavaSE-1.8 + + + + + + + org.eluder.coveralls + coveralls-maven-plugin + ${version.coveralls} + + + target/generated-sources/antlr + + + + + + + org.apache.maven.plugins + maven-surefire-plugin + ${version.surefire} + + false + false + -Xmx2g + + + + + + + + + org.logicng + logicng-core + ${project.version} + + + + + org.antlr + antlr4-runtime + ${version.antlr} + + + + + org.junit.jupiter + junit-jupiter + ${version.junit} + test + + + + org.junit.jupiter + junit-jupiter-params + ${version.junit} + test + + + + org.assertj + assertj-core + ${version.assertj} + test + + + + + + sonatype-nexus-snapshot + https://oss.sonatype.org/content/repositories/snapshots + + false + + + true + + + + + + + release + + + + + org.sonatype.plugins + nexus-staging-maven-plugin + ${version.nexus-staging} + true + + ossrh + https://oss.sonatype.org/ + false + + + + + + org.apache.maven.plugins + maven-gpg-plugin + ${version.maven-gpg} + + + sign-artifacts + verify + + sign + + + + + + + + + + all-tests + + + + regular-tests + + true + + + random,longRunning + + + + + long-running-tests + + longRunning + + + + + random-tests + + random + + + + diff --git a/core/src/main/antlr/LogicNGPropositional.g4 b/parser/src/main/antlr/LogicNGPropositional.g4 similarity index 100% rename from core/src/main/antlr/LogicNGPropositional.g4 rename to parser/src/main/antlr/LogicNGPropositional.g4 diff --git a/core/src/main/antlr/LogicNGPseudoBoolean.g4 b/parser/src/main/antlr/LogicNGPseudoBoolean.g4 similarity index 100% rename from core/src/main/antlr/LogicNGPseudoBoolean.g4 rename to parser/src/main/antlr/LogicNGPseudoBoolean.g4 diff --git a/core/src/main/java/org/logicng/io/parsers/FormulaParser.java b/parser/src/main/java/org/logicng/io/parsers/FormulaParser.java similarity index 100% rename from core/src/main/java/org/logicng/io/parsers/FormulaParser.java rename to parser/src/main/java/org/logicng/io/parsers/FormulaParser.java diff --git a/core/src/main/java/org/logicng/io/parsers/LexerException.java b/parser/src/main/java/org/logicng/io/parsers/LexerException.java similarity index 100% rename from core/src/main/java/org/logicng/io/parsers/LexerException.java rename to parser/src/main/java/org/logicng/io/parsers/LexerException.java diff --git a/core/src/main/java/org/logicng/io/parsers/ParserException.java b/parser/src/main/java/org/logicng/io/parsers/ParserException.java similarity index 100% rename from core/src/main/java/org/logicng/io/parsers/ParserException.java rename to parser/src/main/java/org/logicng/io/parsers/ParserException.java diff --git a/core/src/main/java/org/logicng/io/parsers/ParserWithFormula.java b/parser/src/main/java/org/logicng/io/parsers/ParserWithFormula.java similarity index 100% rename from core/src/main/java/org/logicng/io/parsers/ParserWithFormula.java rename to parser/src/main/java/org/logicng/io/parsers/ParserWithFormula.java diff --git a/core/src/main/java/org/logicng/io/parsers/PropositionalLexer.java b/parser/src/main/java/org/logicng/io/parsers/PropositionalLexer.java similarity index 100% rename from core/src/main/java/org/logicng/io/parsers/PropositionalLexer.java rename to parser/src/main/java/org/logicng/io/parsers/PropositionalLexer.java diff --git a/core/src/main/java/org/logicng/io/parsers/PropositionalParser.java b/parser/src/main/java/org/logicng/io/parsers/PropositionalParser.java similarity index 100% rename from core/src/main/java/org/logicng/io/parsers/PropositionalParser.java rename to parser/src/main/java/org/logicng/io/parsers/PropositionalParser.java diff --git a/core/src/main/java/org/logicng/io/parsers/PseudoBooleanLexer.java b/parser/src/main/java/org/logicng/io/parsers/PseudoBooleanLexer.java similarity index 100% rename from core/src/main/java/org/logicng/io/parsers/PseudoBooleanLexer.java rename to parser/src/main/java/org/logicng/io/parsers/PseudoBooleanLexer.java diff --git a/core/src/main/java/org/logicng/io/parsers/PseudoBooleanParser.java b/parser/src/main/java/org/logicng/io/parsers/PseudoBooleanParser.java similarity index 100% rename from core/src/main/java/org/logicng/io/parsers/PseudoBooleanParser.java rename to parser/src/main/java/org/logicng/io/parsers/PseudoBooleanParser.java diff --git a/core/src/main/java/org/logicng/io/readers/FormulaReader.java b/parser/src/main/java/org/logicng/io/readers/FormulaReader.java similarity index 100% rename from core/src/main/java/org/logicng/io/readers/FormulaReader.java rename to parser/src/main/java/org/logicng/io/readers/FormulaReader.java diff --git a/core/src/test/java/org/logicng/io/parsers/PropositionalParserTest.java b/parser/src/test/java/org/logicng/io/parsers/PropositionalParserTest.java similarity index 97% rename from core/src/test/java/org/logicng/io/parsers/PropositionalParserTest.java rename to parser/src/test/java/org/logicng/io/parsers/PropositionalParserTest.java index 331f5f1b..27538bdd 100644 --- a/core/src/test/java/org/logicng/io/parsers/PropositionalParserTest.java +++ b/parser/src/test/java/org/logicng/io/parsers/PropositionalParserTest.java @@ -32,18 +32,15 @@ import static org.assertj.core.api.Assertions.assertThatThrownBy; import org.junit.jupiter.api.Test; -import org.logicng.TestWithExampleFormulas; +import org.logicng.formulas.FormulaFactory; import java.io.ByteArrayInputStream; import java.io.InputStream; import java.nio.charset.StandardCharsets; -/** - * Unit Tests for the class {@link PropositionalParser}. - * @version 2.4.1 - * @since 1.0 - */ -public class PropositionalParserTest extends TestWithExampleFormulas { +public class PropositionalParserTest { + + final FormulaFactory f = new FormulaFactory(); @Test public void testExceptions() throws ParserException { @@ -157,8 +154,8 @@ public void testSkipSymbols() throws ParserException { assertThat(parser.parse("\n")).isEqualTo(this.f.verum()); assertThat(parser.parse("\r")).isEqualTo(this.f.verum()); assertThat(parser.parse(" \r\n\n \t")).isEqualTo(this.f.verum()); - assertThat(parser.parse("a\n&\tb")).isEqualTo(this.AND1); - assertThat(parser.parse(" a\r=>\t\tb")).isEqualTo(this.IMP1); + assertThat(parser.parse("a\n&\tb")).isEqualTo(this.f.and(this.f.variable("a"), this.f.variable("b"))); + assertThat(parser.parse(" a\r=>\t\tb")).isEqualTo(this.f.implication(this.f.variable("a"), this.f.variable("b"))); } @Test diff --git a/core/src/test/java/org/logicng/io/parsers/PseudoBooleanParserTest.java b/parser/src/test/java/org/logicng/io/parsers/PseudoBooleanParserTest.java similarity index 96% rename from core/src/test/java/org/logicng/io/parsers/PseudoBooleanParserTest.java rename to parser/src/test/java/org/logicng/io/parsers/PseudoBooleanParserTest.java index c98547e8..57b017a8 100644 --- a/core/src/test/java/org/logicng/io/parsers/PseudoBooleanParserTest.java +++ b/parser/src/test/java/org/logicng/io/parsers/PseudoBooleanParserTest.java @@ -32,18 +32,16 @@ import static org.assertj.core.api.Assertions.assertThatThrownBy; import org.junit.jupiter.api.Test; -import org.logicng.TestWithExampleFormulas; import org.logicng.formulas.CType; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Literal; -/** - * Unit Tests for the class {@link PseudoBooleanParser}. - * @version 4.4.1 - * @since 1.0 - */ -public class PseudoBooleanParserTest extends TestWithExampleFormulas { +import java.util.Arrays; + +public class PseudoBooleanParserTest { + + final FormulaFactory f = new FormulaFactory(); @Test public void testExceptions() throws ParserException { @@ -174,9 +172,9 @@ public void testSkipSymbols() throws ParserException { assertThat(parser.parse("\n")).isEqualTo(this.f.verum()); assertThat(parser.parse("\r")).isEqualTo(this.f.verum()); assertThat(parser.parse(" \r\n\n \t")).isEqualTo(this.f.verum()); - assertThat(parser.parse("a\n&\tb")).isEqualTo(this.AND1); - assertThat(parser.parse(" a\r=>\t\tb")).isEqualTo(this.IMP1); - assertThat(parser.parse(" 2\n*a\r+\n\n-4*\tb +3*x=2")).isEqualTo(this.PBC1); + assertThat(parser.parse("a\n&\tb")).isEqualTo(this.f.and(this.f.variable("a"), this.f.variable("b"))); + assertThat(parser.parse(" a\r=>\t\tb")).isEqualTo(this.f.implication(this.f.variable("a"), this.f.variable("b"))); + assertThat(parser.parse(" 2\n*a\r+\n\n-4*\tb +3*x=2")).isEqualTo(this.f.pbc(CType.EQ, 2, Arrays.asList(this.f.variable("a"), this.f.variable("b"), this.f.variable("x")), Arrays.asList(2, -4, 3))); } @Test @@ -189,12 +187,6 @@ public void testNumberLiterals() throws ParserException { assertThat(parser.parse("-12 * ~12 + 13 * A + 10 * B <= 25")).isEqualTo(f.pbc(CType.LE, 25, new Literal[]{f.literal("12", false), f.variable("A"), f.variable("B")}, new int[]{-12, 13, 10})); } - @Test - public void testFormulaFactoryParser() throws ParserException { - assertThat(this.f.parse("a & b")).isEqualTo(this.f.and(this.f.variable("a"), this.f.variable("b"))); - assertThat(this.f.parse("2*a + -4*b + 3*x = 2")).isEqualTo(this.PBC1); - } - @Test public void testIllegalVariable1() { assertThatThrownBy(() -> new PseudoBooleanParser(this.f).parse("$$%")).isInstanceOf(ParserException.class); diff --git a/pom.xml b/pom.xml index 4d481387..4a17c45c 100644 --- a/pom.xml +++ b/pom.xml @@ -35,6 +35,7 @@ core + parser @@ -88,5 +89,7 @@ 3.3.0 3.6.3 3.3.0 + 3.3.1 + 1.9.1