diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCIncrementalData.java b/src/main/java/org/logicng/cardinalityconstraints/CCIncrementalData.java index 3e17c7a8..e3f765f5 100644 --- a/src/main/java/org/logicng/cardinalityconstraints/CCIncrementalData.java +++ b/src/main/java/org/logicng/cardinalityconstraints/CCIncrementalData.java @@ -26,7 +26,7 @@ // // /////////////////////////////////////////////////////////////////////////// -/** +/* * PBLib -- Copyright (c) 2012-2013 Peter Steinke * * Permission is hereby granted, free of charge, to any person obtaining a @@ -155,6 +155,10 @@ public List newUpperBound(int rhs) { /** * Tightens the upper bound of an at-most-k constraint and encodes it on the solver of the result. + * + * Usage constraints: + * -New right hand side must be smaller than current right hand side. + * -Cannot be used for at-least-k constraints. * @param rhs the new upperBound */ public void newUpperBoundForSolver(int rhs) { @@ -214,6 +218,10 @@ public List newLowerBound(int rhs) { /** * Tightens the lower bound of an at-least-k constraint and encodes it on the solver of the result. + * + * Usage constraints: + * -New right hand side must be greater than current right hand side. + * -Cannot be used for at-most-k constraints. * @param rhs the new upperBound */ public void newLowerBoundForSolver(int rhs) { diff --git a/src/main/java/org/logicng/collections/LNGDoubleVector.java b/src/main/java/org/logicng/collections/LNGDoubleVector.java index d17b2890..17ad045c 100644 --- a/src/main/java/org/logicng/collections/LNGDoubleVector.java +++ b/src/main/java/org/logicng/collections/LNGDoubleVector.java @@ -36,7 +36,7 @@ * In theory one could use the {@link LNGVector} also for doubles. But Java's auto-boxing comes with such a large * performance penalty that for the mission critical data structures of the SAT solvers we use this specialized * implementation. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public final class LNGDoubleVector { @@ -163,7 +163,8 @@ public void pop() { * @param newSize the new size */ public void shrinkTo(int newSize) { - this.size = newSize; + if (newSize < this.size) + this.size = newSize; } /** diff --git a/src/main/java/org/logicng/formulas/PBConstraint.java b/src/main/java/org/logicng/formulas/PBConstraint.java index f139c1ea..396ce95d 100644 --- a/src/main/java/org/logicng/formulas/PBConstraint.java +++ b/src/main/java/org/logicng/formulas/PBConstraint.java @@ -103,10 +103,8 @@ public void remove() { for (final int c : coefficients) { if (c > maxWeight) maxWeight = c; - if (c != 1) { + if (c != 1) cc = false; - break; - } } for (final Literal lit : literals) if (!lit.phase()) { @@ -215,7 +213,8 @@ public Formula normalize() { } /** - * Internal helper for normalization of a <= constraint. + * Internal helper for normalization of a <= constraint. Can also be used for >= constraints by multiplying the right + * side and the coefficients with -1. * @param ps the literals * @param cs the coefficients * @param rhs the right-hand side diff --git a/src/main/java/org/logicng/io/writers/FormulaDotFileWriter.java b/src/main/java/org/logicng/io/writers/FormulaDotFileWriter.java index 45a80919..c436e26a 100644 --- a/src/main/java/org/logicng/io/writers/FormulaDotFileWriter.java +++ b/src/main/java/org/logicng/io/writers/FormulaDotFileWriter.java @@ -46,7 +46,7 @@ /** * A dot file writer for a formula. Writes the internal data structure of the formula to a dot file. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public final class FormulaDotFileWriter { @@ -55,7 +55,7 @@ public final class FormulaDotFileWriter { * Private constructor. */ private FormulaDotFileWriter() { - throw new AssertionError(); + // Intentionally left empty. } /** @@ -178,9 +178,4 @@ private static void generateNaryDotString(final NAryOperator formula, final Stri for (final Formula operand : formula) sb.append(" id").append(id).append(" -> id").append(ids.get(operand)).append(";\n"); } - - @Override - public String toString() { - return this.getClass().getSimpleName(); - } } diff --git a/src/main/java/org/logicng/predicates/satisfiability/SATPredicate.java b/src/main/java/org/logicng/predicates/satisfiability/SATPredicate.java index f5b933b2..ac15e3b2 100644 --- a/src/main/java/org/logicng/predicates/satisfiability/SATPredicate.java +++ b/src/main/java/org/logicng/predicates/satisfiability/SATPredicate.java @@ -41,7 +41,7 @@ /** * A SAT solver based SAT predicate. Indicates whether a formula is satisfiable or not. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public final class SATPredicate implements FormulaPredicate { @@ -70,14 +70,13 @@ public boolean test(final Formula formula, boolean cache) { final Tristate cached = formula.predicateCacheEntry(IS_SAT); if (cached != Tristate.UNDEF) return cached == Tristate.TRUE; - final FormulaFactory factory = formula.factory(); boolean result; if (formula.type() == FType.FALSE) result = false; else if (formula.type() == FType.TRUE || formula.type() == FType.LITERAL) result = true; else if (formula.holds(dnfPredicate)) - result = formula != factory.falsum(); + result = true; else { this.solver.add(formula); result = solver.sat() == Tristate.TRUE; diff --git a/src/main/java/org/logicng/propositions/StandardProposition.java b/src/main/java/org/logicng/propositions/StandardProposition.java index 03cda7fc..d46312c6 100644 --- a/src/main/java/org/logicng/propositions/StandardProposition.java +++ b/src/main/java/org/logicng/propositions/StandardProposition.java @@ -37,13 +37,13 @@ /** * A proposition in LogicNG. A proposition is a collection of formulas with an additional textual description. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public final class StandardProposition extends Proposition { private final ImmutableFormulaList formulas; - private final String decription; + private final String description; /** * Constructs a new proposition for a single formulas. @@ -51,7 +51,7 @@ public final class StandardProposition extends Proposition { */ public StandardProposition(final Formula formula) { this.formulas = new ImmutableFormulaList(FType.AND, formula); - this.decription = ""; + this.description = ""; } /** @@ -61,7 +61,7 @@ public StandardProposition(final Formula formula) { */ public StandardProposition(final String description, final Formula formula) { this.formulas = new ImmutableFormulaList(FType.AND, formula); - this.decription = description; + this.description = description == null ? "" : description; } /** @@ -71,7 +71,7 @@ public StandardProposition(final String description, final Formula formula) { */ public StandardProposition(final String description, final Collection formulas) { this.formulas = new ImmutableFormulaList(FType.AND, formulas); - this.decription = description; + this.description = description == null ? "" : description; } /** @@ -81,7 +81,7 @@ public StandardProposition(final String description, final Collection list = new LinkedList<>(); diff --git a/src/main/java/org/logicng/solvers/SATSolver.java b/src/main/java/org/logicng/solvers/SATSolver.java index 4df823e5..224dd4ef 100644 --- a/src/main/java/org/logicng/solvers/SATSolver.java +++ b/src/main/java/org/logicng/solvers/SATSolver.java @@ -47,7 +47,7 @@ /** * A generic interface for LogicNG's SAT solvers. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public abstract class SATSolver { @@ -137,8 +137,14 @@ public void add(final Variable relaxationVar, final Collection": Returns null for right hand side 0 or number of variables -1, but constraint is added to solver. Adds false to solver for right hand side >= number of variables. + * - ">=": Returns null for right hand side 1 or number of variables, but constraint is added to solver. Adds false to solver for right hand side > number of variables. * @param cc the cardinality constraint - * @return the incremental data of this constraint + * @return the incremental data of this constraint, or null if the right hand side of cc is 1 */ public abstract CCIncrementalData addIncrementalCC(final PBConstraint cc); diff --git a/src/main/java/org/logicng/transformations/cnf/CNFFactorization.java b/src/main/java/org/logicng/transformations/cnf/CNFFactorization.java index 47d70122..5548c5b6 100644 --- a/src/main/java/org/logicng/transformations/cnf/CNFFactorization.java +++ b/src/main/java/org/logicng/transformations/cnf/CNFFactorization.java @@ -42,7 +42,7 @@ /** * Transformation of a formula in CNF by factorization. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public final class CNFFactorization implements FormulaTransformation { @@ -100,9 +100,10 @@ public Formula apply(final Formula formula, boolean cache) { case AND: nops = new LinkedHashSet<>(); for (final Formula op : formula) { + final Formula apply = this.apply(op, cache); if (!this.proceed) return null; - nops.add(this.apply(op, cache)); + nops.add(apply); } cached = formula.factory().and(nops); break; @@ -133,8 +134,12 @@ private Formula distribute(final Formula f1, final Formula f2) { final FormulaFactory f = f1.factory(); if (f1.type() == AND || f2.type() == AND) { final LinkedHashSet nops = new LinkedHashSet<>(); - for (final Formula op : f1.type() == AND ? f1 : f2) - nops.add(this.distribute(op, f1.type() == AND ? f2 : f1)); + for (final Formula op : f1.type() == AND ? f1 : f2) { + final Formula distribute = this.distribute(op, f1.type() == AND ? f2 : f1); + if (!this.proceed) + return null; + nops.add(distribute); + } return f.and(nops); } final Formula clause = f.or(f1, f2); diff --git a/src/main/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformation.java b/src/main/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformation.java index 17102331..d206d3ba 100644 --- a/src/main/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformation.java +++ b/src/main/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformation.java @@ -34,7 +34,6 @@ import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.FormulaTransformation; import org.logicng.formulas.Literal; -import org.logicng.formulas.Not; import org.logicng.predicates.CNFPredicate; import java.util.ArrayList; @@ -49,7 +48,7 @@ *

* ATTENTION: if you mix formulas from different formula factories this can lead to clashes in the naming of newly * introduced variables. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public final class PlaistedGreenbaumTransformation implements FormulaTransformation { @@ -117,10 +116,6 @@ private Formula computePosPolarity(final Formula formula, final Literal fixedPGV final FormulaFactory f = formula.factory(); final Formula pgVar = fixedPGVar != null ? fixedPGVar : pgVariable(formula); switch (formula.type()) { - case NOT: - result = f.or(pgVar.negate(), pgVariable(((Not) formula).operand()).negate()); - formula.setTransformationCacheEntry(PLAISTED_GREENBAUM_POS, result); - return result; case AND: List nops = new ArrayList<>(); for (final Formula op : formula) diff --git a/src/main/java/org/logicng/transformations/dnf/DNFFactorization.java b/src/main/java/org/logicng/transformations/dnf/DNFFactorization.java index a613c735..f4254a15 100644 --- a/src/main/java/org/logicng/transformations/dnf/DNFFactorization.java +++ b/src/main/java/org/logicng/transformations/dnf/DNFFactorization.java @@ -42,7 +42,7 @@ /** * Transformation of a formula in DNF by factorization. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public final class DNFFactorization implements FormulaTransformation { @@ -86,9 +86,10 @@ public Formula apply(final Formula formula, boolean cache) { case OR: LinkedHashSet nops = new LinkedHashSet<>(); for (final Formula op : formula) { + final Formula apply = this.apply(op, cache); if (!this.proceed) return null; - nops.add(this.apply(op, cache)); + nops.add(apply); } cached = formula.factory().or(nops); break; @@ -131,8 +132,12 @@ private Formula distribute(final Formula f1, final Formula f2) { final FormulaFactory f = f1.factory(); if (f1.type() == FType.OR || f2.type() == FType.OR) { final LinkedHashSet nops = new LinkedHashSet<>(); - for (final Formula op : f1.type() == FType.OR ? f1 : f2) - nops.add(this.distribute(op, f1.type() == FType.OR ? f2 : f1)); + for (final Formula op : f1.type() == FType.OR ? f1 : f2) { + final Formula distribute = this.distribute(op, f1.type() == FType.OR ? f2 : f1); + if (!this.proceed) + return null; + nops.add(distribute); + } return f.or(nops); } final Formula clause = f.and(f1, f2); diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java index 7a0575a4..f506f731 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java @@ -63,6 +63,7 @@ public void testALK() { int counter = 0; for (final CCConfig config : this.configs) { f.putConfiguration(config); + testCC(10, 0, 1, f); testCC(10, 1, 1023, f); testCC(10, 2, 1013, f); testCC(10, 3, 968, f); @@ -104,4 +105,11 @@ public void testIllegalCC1() { problemLits[i] = f.variable("v" + i); encoder.encode(f.cc(CType.GE, -1, problemLits)); } + + @Test + public void testToString() { + Assert.assertEquals("TOTALIZER", configs[0].alkEncoder.toString()); + Assert.assertEquals("MODULAR_TOTALIZER", configs[1].alkEncoder.toString()); + Assert.assertEquals("CARDINALITY_NETWORK", configs[2].alkEncoder.toString()); + } } diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java index 0e63fa6b..63a2685c 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java @@ -38,6 +38,7 @@ import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; +import java.util.Arrays; import java.util.List; /** @@ -137,4 +138,16 @@ public void testIllegalCC1() { problemLits[i] = f.variable("v" + i); encoder.encode(f.cc(CType.LE, -1, problemLits)); } + + @Test + public void testToString() { + Assert.assertEquals("TOTALIZER", configs[0].amkEncoder.toString()); + Assert.assertEquals("MODULAR_TOTALIZER", configs[1].amkEncoder.toString()); + Assert.assertEquals("CARDINALITY_NETWORK", configs[2].amkEncoder.toString()); + } + + @Test + public void testCCSorting() { + Assert.assertTrue(Arrays.asList(CCSorting.ImplicationDirection.values()).contains(CCSorting.ImplicationDirection.valueOf("INPUT_TO_OUTPUT"))); + } } diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java index badd82cf..6de13bf8 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java @@ -62,7 +62,7 @@ public class CCAMOTest { private CCConfig[] configs; public CCAMOTest() { - configs = new CCConfig[11]; + configs = new CCConfig[14]; configs[0] = new CCConfig.Builder().amoEncoding(PURE).build(); configs[1] = new CCConfig.Builder().amoEncoding(LADDER).build(); configs[2] = new CCConfig.Builder().amoEncoding(PRODUCT).build(); @@ -73,7 +73,10 @@ public CCAMOTest() { configs[7] = new CCConfig.Builder().amoEncoding(BIMANDER).bimanderGroupSize(FIXED).build(); configs[8] = new CCConfig.Builder().amoEncoding(BIMANDER).bimanderGroupSize(HALF).build(); configs[9] = new CCConfig.Builder().amoEncoding(BIMANDER).bimanderGroupSize(SQRT).build(); - configs[10] = new CCConfig.Builder().amoEncoding(BEST).build(); + configs[10] = new CCConfig.Builder().amoEncoding(BIMANDER).bimanderGroupSize(FIXED).bimanderFixedGroupSize(2).build(); + configs[11] = new CCConfig.Builder().amoEncoding(NESTED).nestingGroupSize(5).build(); + configs[12] = new CCConfig.Builder().amoEncoding(PRODUCT).productRecursiveBound(10).build(); + configs[13] = new CCConfig.Builder().amoEncoding(BEST).build(); } @Test @@ -121,6 +124,18 @@ public void testAMOKMiniCard() { Assert.assertTrue(f.newCCVariable().name().endsWith("_0")); } + @Test + public void testToString() { + Assert.assertEquals("PURE", configs[0].amoEncoder.toString()); + Assert.assertEquals("LADDER", configs[1].amoEncoder.toString()); + Assert.assertEquals("PRODUCT", configs[2].amoEncoder.toString()); + Assert.assertEquals("BINARY", configs[3].amoEncoder.toString()); + Assert.assertEquals("NESTED", configs[4].amoEncoder.toString()); + Assert.assertEquals("COMMANDER", configs[5].amoEncoder.toString()); + Assert.assertEquals("BIMANDER", configs[7].amoEncoder.toString()); + Assert.assertEquals("BEST", configs[13].amoEncoder.toString()); + } + private void testAMO(int numLits, final FormulaFactory f, boolean miniCard) { final Variable[] problemLits = new Variable[numLits]; for (int i = 0; i < numLits; i++) diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCEXKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCEXKTest.java index 19ec44e9..efe3c9b6 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCEXKTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCEXKTest.java @@ -102,4 +102,10 @@ public void testIllegalCC1() { problemLits[i] = f.variable("v" + i); encoder.encode(f.cc(CType.EQ, -1, problemLits)); } + + @Test + public void testToString() { + Assert.assertEquals("TOTALIZER", configs[0].exkEncoder.toString()); + Assert.assertEquals("CARDINALITY_NETWORK", configs[1].exkEncoder.toString()); + } } diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCEXOTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCEXOTest.java index 984ec627..29134177 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCEXOTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCEXOTest.java @@ -113,6 +113,17 @@ public void testEXOK() { } } + @Test + public void testToString() { + Assert.assertEquals("PURE", configs[0].amoEncoder.toString()); + Assert.assertEquals("LADDER", configs[1].amoEncoder.toString()); + Assert.assertEquals("PRODUCT", configs[2].amoEncoder.toString()); + Assert.assertEquals("BINARY", configs[3].amoEncoder.toString()); + Assert.assertEquals("NESTED", configs[4].amoEncoder.toString()); + Assert.assertEquals("COMMANDER", configs[5].amoEncoder.toString()); + Assert.assertEquals("BIMANDER", configs[7].amoEncoder.toString()); + } + private void testEXO(int numLits, final FormulaFactory f) { final Variable[] problemLits = new Variable[numLits]; for (int i = 0; i < numLits; i++) diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalFormulaTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalFormulaTest.java index 7909df46..c6aaf638 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalFormulaTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalFormulaTest.java @@ -106,6 +106,48 @@ public void testSimpleIncrementalAMK() { } } + @Test + public void testIncrementalData() { + for (final CCEncoder encoder : this.encoders) { + int numLits = 10; + Variable[] vars = new Variable[numLits]; + for (int i = 0; i < numLits; i++) + vars[i] = f.variable("v" + i); + Pair cc = encoder.encodeIncremental(f.cc(CType.LT, 10, vars)); + CCIncrementalData incData = cc.second(); + Assert.assertTrue(incData.toString().contains("currentRHS=9")); + + cc = encoder.encodeIncremental(f.cc(CType.GT, 1, vars)); + incData = cc.second(); + Assert.assertTrue(incData.toString().contains("currentRHS=2")); + + cc = encoder.encodeIncremental(f.cc(CType.LT, 1, vars)); + incData = cc.second(); + Assert.assertNull(incData); + Assert.assertTrue(cc.first().containsFormula(vars[0].negate())); + + cc = encoder.encodeIncremental(f.cc(CType.LE, numLits + 1, vars)); + incData = cc.second(); + Assert.assertNull(incData); + + cc = encoder.encodeIncremental(f.cc(CType.GE, numLits + 1, vars)); + incData = cc.second(); + Assert.assertNull(incData); + + cc = encoder.encodeIncremental(f.cc(CType.GE, numLits, vars)); + incData = cc.second(); + Assert.assertNull(incData); + + cc = encoder.encodeIncremental(f.cc(CType.GE, 0, vars)); + incData = cc.second(); + Assert.assertNull(incData); + + cc = encoder.encodeIncremental(f.cc(CType.GE, 1, vars)); + incData = cc.second(); + Assert.assertNull(incData); + } + } + @Test public void testSimpleIncrementalALK() { for (final CCEncoder encoder : this.encoders) { @@ -214,6 +256,23 @@ public void testLargeModularTotalizerAMK() { } } + @Test + public void testToString() { + String expected = "CCConfig{\n" + + "amoEncoder=BEST\n" + + "amkEncoder=TOTALIZER\n" + + "alkEncoder=TOTALIZER\n" + + "exkEncoder=BEST\n" + + "bimanderGroupSize=SQRT\n" + + "bimanderFixedGroupSize=3\n" + + "nestingGroupSize=4\n" + + "productRecursiveBound=20\n" + + "commanderGroupSize=3\n" + + "}\n"; + Assert.assertEquals(expected, encoders[0].config().toString()); + Assert.assertEquals(expected, encoders[0].toString()); + } + @Ignore @Test public void testVeryLargeModularTotalizerAMK() { diff --git a/src/main/java/org/logicng/explanations/unsatcores/algorithms/NewConstructiveMUS.java b/src/test/java/org/logicng/collections/ImmutableFormulaListTest.java similarity index 54% rename from src/main/java/org/logicng/explanations/unsatcores/algorithms/NewConstructiveMUS.java rename to src/test/java/org/logicng/collections/ImmutableFormulaListTest.java index 0dd27883..2c0ccf75 100644 --- a/src/main/java/org/logicng/explanations/unsatcores/algorithms/NewConstructiveMUS.java +++ b/src/test/java/org/logicng/collections/ImmutableFormulaListTest.java @@ -26,57 +26,28 @@ // // /////////////////////////////////////////////////////////////////////////// -package org.logicng.explanations.unsatcores.algorithms; +package org.logicng.collections; -import org.logicng.datastructures.Assignment; -import org.logicng.datastructures.Tristate; -import org.logicng.explanations.unsatcores.MUSConfig; -import org.logicng.explanations.unsatcores.UNSATCore; +import org.junit.Assert; +import org.junit.Test; +import org.logicng.formulas.FType; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Variable; -import org.logicng.propositions.Proposition; -import org.logicng.solvers.MiniSat; - -import java.util.ArrayList; -import java.util.List; -import java.util.SortedMap; -import java.util.TreeMap; /** - * A new constructive MUS algorithm due to Marques-Silva & Lynce. + * Unit tests for {@link ImmutableFormulaList}. * @version 1.1 * @since 1.1 */ -public final class NewConstructiveMUS extends MUSAlgorithm { +public class ImmutableFormulaListTest { + private FormulaFactory formulaFactory = new FormulaFactory(); + private Variable a = formulaFactory.variable("A"); + private Variable b = formulaFactory.variable("B"); - @Override - public UNSATCore computeMUS(List propositions, final FormulaFactory f, final MUSConfig config) { - final List mus = new ArrayList<>(propositions.size()); - int nrRelaxedProps = propositions.size(); - final MiniSat solver = MiniSat.glucose(f); - final List relexationVars = new ArrayList<>(); - final SortedMap propMapping = new TreeMap<>(); - for (final Proposition prop : propositions) { - final Variable relexationVar = f.variable("@MUS_NC_" + relexationVars.size()); - relexationVars.add(relexationVar); - solver.addWithRelaxation(relexationVar, prop); - propMapping.put(relexationVar, prop); - } - solver.add(f.amo(relexationVars)); - while (nrRelaxedProps > 0) { - final Tristate result = solver.sat(); - if (result == Tristate.TRUE) { - final Assignment model = solver.model(relexationVars); - assert model != null; - final Variable trueVariable = model.negativeVariables().get(0); - solver.add(trueVariable.negate()); - mus.add(propMapping.get(trueVariable)); - nrRelaxedProps--; - relexationVars.remove(trueVariable); - } else { - // UNSAT core required... - } - } - return new UNSATCore(mus, true); + @Test + public void testFormula() { + ImmutableFormulaList ifl = new ImmutableFormulaList(FType.AND, a, b); + Assert.assertEquals(ifl.formula(formulaFactory), ifl.formula(formulaFactory)); //On purpose to check if both ways in method lead to the same result + Assert.assertEquals(formulaFactory.and(a, b), ifl.formula(formulaFactory)); } } diff --git a/src/test/java/org/logicng/collections/LNGBooleanVectorTest.java b/src/test/java/org/logicng/collections/LNGBooleanVectorTest.java index 7a572e5e..8aa04fe5 100644 --- a/src/test/java/org/logicng/collections/LNGBooleanVectorTest.java +++ b/src/test/java/org/logicng/collections/LNGBooleanVectorTest.java @@ -33,7 +33,7 @@ /** * Unit tests for {@link LNGBooleanVector}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class LNGBooleanVectorTest { @@ -125,6 +125,9 @@ public void testVectorShrink() { for (int i = 0; i < 1000; i++) v1.push(i % 2 == 0); Assert.assertFalse(v1.empty()); + int beforeSize = v1.size(); + v1.shrinkTo(v1.size() + 50); + Assert.assertEquals(v1.size(), beforeSize); for (int i = 500; i > 0; i--) { v1.shrinkTo(i); Assert.assertEquals((i - 1) % 2 == 0, v1.back()); diff --git a/src/test/java/org/logicng/collections/LNGByteVectorTest.java b/src/test/java/org/logicng/collections/LNGByteVectorTest.java index fd8b1610..0ded83b4 100644 --- a/src/test/java/org/logicng/collections/LNGByteVectorTest.java +++ b/src/test/java/org/logicng/collections/LNGByteVectorTest.java @@ -33,7 +33,7 @@ /** * Unit tests for {@link LNGByteVector}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class LNGByteVectorTest { @@ -122,6 +122,9 @@ public void testVectorShrink() { for (int i = 0; i < 100; i++) v1.push((byte) i); Assert.assertFalse(v1.empty()); + int beforeSize = v1.size(); + v1.shrinkTo(v1.size() + 50); + Assert.assertEquals(v1.size(), beforeSize); for (int i = 50; i > 0; i--) { v1.shrinkTo(i); Assert.assertEquals((i - 1), v1.back()); diff --git a/src/test/java/org/logicng/collections/LNGDoublePriorityQueueTest.java b/src/test/java/org/logicng/collections/LNGDoublePriorityQueueTest.java index 48d04c8d..c71a527d 100644 --- a/src/test/java/org/logicng/collections/LNGDoublePriorityQueueTest.java +++ b/src/test/java/org/logicng/collections/LNGDoublePriorityQueueTest.java @@ -33,7 +33,7 @@ /** * Unit tests for {@link LNGDoublePriorityQueue}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class LNGDoublePriorityQueueTest { @@ -97,6 +97,8 @@ public void testUpdateAndPriorities() { q1.update(1, 7.0); Assert.assertEquals(5, q1.size()); Assert.assertEquals(1, q1.top()); + q1.update(1, 7.0); + Assert.assertEquals(1, q1.top()); q1.update(1, 2.0); Assert.assertEquals(0, q1.top()); q1.update(4, 8.0); diff --git a/src/test/java/org/logicng/collections/LNGLongVectorTest.java b/src/test/java/org/logicng/collections/LNGLongVectorTest.java index 9b5ae0bb..607eb32f 100644 --- a/src/test/java/org/logicng/collections/LNGLongVectorTest.java +++ b/src/test/java/org/logicng/collections/LNGLongVectorTest.java @@ -33,7 +33,7 @@ /** * Unit tests for {@link LNGLongVector}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class LNGLongVectorTest { @@ -122,6 +122,9 @@ public void testVectorShrink() { for (int i = 0; i < 1000; i++) v1.push(i); Assert.assertFalse(v1.empty()); + int beforeSize = v1.size(); + v1.shrinkTo(v1.size() + 50); + Assert.assertEquals(v1.size(), beforeSize); for (int i = 500; i > 0; i--) { v1.shrinkTo(i); Assert.assertEquals((i - 1), v1.back()); diff --git a/src/test/java/org/logicng/collections/LNGVectorTest.java b/src/test/java/org/logicng/collections/LNGVectorTest.java index aec9af18..4790e529 100644 --- a/src/test/java/org/logicng/collections/LNGVectorTest.java +++ b/src/test/java/org/logicng/collections/LNGVectorTest.java @@ -39,7 +39,7 @@ /** * Unit tests for {@link LNGVector}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class LNGVectorTest { @@ -157,6 +157,9 @@ public void testVectorShrink() { for (int i = 0; i < 1000; i++) v1.push("s" + i); Assert.assertFalse(v1.empty()); + int beforeSize = v1.size(); + v1.shrinkTo(v1.size() + 50); + Assert.assertEquals(v1.size(), beforeSize); for (int i = 500; i > 0; i--) { v1.shrinkTo(i); Assert.assertEquals("s" + (i - 1), v1.back()); diff --git a/src/test/java/org/logicng/configurations/ConfigurationsTest.java b/src/test/java/org/logicng/configurations/ConfigurationsTest.java new file mode 100644 index 00000000..37855325 --- /dev/null +++ b/src/test/java/org/logicng/configurations/ConfigurationsTest.java @@ -0,0 +1,48 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-2016 Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +package org.logicng.configurations; + +import org.junit.Assert; +import org.junit.Test; + +/** + * Unit tests for the package configurations. + * @version 1.1 + * @since 1.1 + */ +public class ConfigurationsTest { + + @Test + public void testValueOf() { + Assert.assertEquals(ConfigurationType.CNF, ConfigurationType.valueOf("CNF")); + Assert.assertEquals(ConfigurationType.GLUCOSE, ConfigurationType.valueOf("GLUCOSE")); + Assert.assertEquals(ConfigurationType.MAXSAT, ConfigurationType.valueOf("MAXSAT")); + Assert.assertEquals(ConfigurationType.CC_ENCODER, ConfigurationType.valueOf("CC_ENCODER")); + } +} diff --git a/src/test/java/org/logicng/datastructures/AssignmentTest.java b/src/test/java/org/logicng/datastructures/AssignmentTest.java index 1256bd11..e73ff2f2 100644 --- a/src/test/java/org/logicng/datastructures/AssignmentTest.java +++ b/src/test/java/org/logicng/datastructures/AssignmentTest.java @@ -31,16 +31,19 @@ import org.junit.Assert; import org.junit.Test; import org.logicng.formulas.F; +import org.logicng.formulas.Formula; import org.logicng.formulas.Literal; import org.logicng.io.parsers.ParserException; import org.logicng.io.parsers.PropositionalParser; +import java.util.ArrayList; import java.util.Arrays; import java.util.Collections; +import java.util.List; /** * Unit tests for the class {@link Assignment}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class AssignmentTest { @@ -139,9 +142,9 @@ public void testFastEvaluable() { Assert.assertFalse(ass.fastEvaluable()); ass.convertToFastEvaluable(); Assert.assertTrue(ass.fastEvaluable()); - Assert.assertEquals(Arrays.asList(F.A), ass.positiveLiterals()); - Assert.assertEquals(Arrays.asList(F.NX), ass.negativeLiterals()); - Assert.assertEquals(Arrays.asList(F.X), ass.negativeVariables()); + Assert.assertEquals(Collections.singletonList(F.A), ass.positiveLiterals()); + Assert.assertEquals(Collections.singletonList(F.NX), ass.negativeLiterals()); + Assert.assertEquals(Collections.singletonList(F.X), ass.negativeVariables()); ass.addLiteral(F.NB); ass.addLiteral(F.Y); Assert.assertEquals(Arrays.asList(F.A, F.Y), ass.positiveLiterals()); @@ -155,6 +158,8 @@ public void testFastEvaluable() { Assert.assertEquals(F.f.and(F.A, F.NX, F.NB, F.Y), ass.formula(F.f)); ass = new Assignment(Arrays.asList(F.A, F.NX), true); Assert.assertTrue(ass.fastEvaluable()); + ass.convertToFastEvaluable(); + Assert.assertTrue(ass.fastEvaluable()); } @Test @@ -189,6 +194,22 @@ public void testEquals() { Assert.assertNotEquals(ass, F.TRUE); } + @Test + public void testBlockingClause() { + Assignment ass = new Assignment(); + ass.addLiteral(F.A); + ass.addLiteral(F.B); + ass.addLiteral(F.NX); + ass.addLiteral(F.NY); + List lits = new ArrayList<>(); + lits.add(F.A); + lits.add(F.X); + lits.add(F.C); + Formula bc = ass.blockingClause(F.f, lits); + Assert.assertTrue(!bc.containsVariable(F.C)); + Assert.assertEquals("~a | x", bc.toString()); + } + @Test public void testToString() { Assert.assertEquals("Assignment{pos=[], neg=[]}", new Assignment().toString()); diff --git a/src/test/java/org/logicng/datastructures/DatastructuresTest.java b/src/test/java/org/logicng/datastructures/DatastructuresTest.java new file mode 100644 index 00000000..705aa204 --- /dev/null +++ b/src/test/java/org/logicng/datastructures/DatastructuresTest.java @@ -0,0 +1,53 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-2016 Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +package org.logicng.datastructures; + +import org.junit.Assert; +import org.junit.Test; + +/** + * Unit tests for the package data structures. + * @version 1.1 + * @since 1.1 + */ +public class DatastructuresTest { + + @Test + public void testTristate() { + Assert.assertEquals(Tristate.TRUE, Tristate.valueOf("TRUE")); + Assert.assertEquals(Tristate.FALSE, Tristate.valueOf("FALSE")); + Assert.assertEquals(Tristate.UNDEF, Tristate.valueOf("UNDEF")); + } + + @Test + public void testEncodingAuxiliaryVariable() { + EncodingAuxiliaryVariable eav = new EncodingAuxiliaryVariable("var", false); + Assert.assertEquals("var", eav.toString()); + } +} diff --git a/src/test/java/org/logicng/explanations/unsatcores/MUSConfigTest.java b/src/test/java/org/logicng/explanations/unsatcores/MUSConfigTest.java index b8eef219..d1ed3986 100644 --- a/src/test/java/org/logicng/explanations/unsatcores/MUSConfigTest.java +++ b/src/test/java/org/logicng/explanations/unsatcores/MUSConfigTest.java @@ -1,7 +1,38 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-2016 Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.explanations.unsatcores; import org.junit.Assert; import org.junit.Test; +import org.logicng.transformations.cnf.CNFConfig; + +import java.util.Arrays; /** * Unit tests for the class {@link MUSConfig}. @@ -14,6 +45,7 @@ public class MUSConfigTest { public void testMUSConfiguration() { final MUSConfig config = new MUSConfig.Builder().algorithm(MUSConfig.Algorithm.DELETION).build(); Assert.assertEquals("MUSConfig{\nalgorithm=DELETION\n}\n", config.toString()); + Assert.assertTrue(Arrays.asList(CNFConfig.Algorithm.values()).contains(CNFConfig.Algorithm.valueOf("TSEITIN"))); } } diff --git a/src/test/java/org/logicng/explanations/unsatcores/MUSGenerationTest.java b/src/test/java/org/logicng/explanations/unsatcores/MUSGenerationTest.java index e1258d5c..d9995f15 100644 --- a/src/test/java/org/logicng/explanations/unsatcores/MUSGenerationTest.java +++ b/src/test/java/org/logicng/explanations/unsatcores/MUSGenerationTest.java @@ -116,6 +116,12 @@ public void testPlainInsertionBasedMUS() throws IOException { testMUS(file2, mus7); } + @Test + public void testToString() { + final MUSGeneration mus = new MUSGeneration(); + Assert.assertEquals("MUSGeneration", mus.toString()); + } + private List generatePGPropositions(int n) { final List result = new ArrayList<>(); final Formula pgf = pg.generate(n); diff --git a/src/test/java/org/logicng/formulas/AndTest.java b/src/test/java/org/logicng/formulas/AndTest.java index 692f6fe7..8ef0e428 100644 --- a/src/test/java/org/logicng/formulas/AndTest.java +++ b/src/test/java/org/logicng/formulas/AndTest.java @@ -39,9 +39,11 @@ import java.util.SortedSet; import java.util.TreeSet; +import static org.logicng.formulas.F.OR1; + /** * Unit Tests for the class {@link And}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class AndTest { @@ -126,11 +128,11 @@ public void testToString() { @Test public void testEquals() { Assert.assertEquals(F.AND1, F.f.and(F.A, F.B)); - Assert.assertEquals(F.AND3, F.f.and(F.OR1, F.OR2)); + Assert.assertEquals(F.AND3, F.f.and(OR1, F.OR2)); Assert.assertEquals(F.AND2, F.AND2); Assert.assertEquals(F.f.and(F.f.or(F.f.variable("a"), F.f.variable("b")), F.f.or(F.f.variable("x"), F.f.literal("y", false))), F.f.and(F.f.or(F.f.literal("y", false), F.f.variable("x")), F.f.or(F.f.variable("b"), F.f.variable("a")))); - Assert.assertEquals(F.f.and(F.A, F.NB, F.OR1, F.NX), F.f.and(F.NX, F.A, F.NB, F.OR1)); + Assert.assertEquals(F.f.and(F.A, F.NB, OR1, F.NX), F.f.and(F.NX, F.A, F.NB, OR1)); Assert.assertNotEquals(F.AND1, null); Assert.assertNotEquals(F.AND1, F.A); Assert.assertNotEquals(F.AND1, F.AND2); @@ -140,10 +142,10 @@ public void testEquals() { @Test public void testEqualsDifferentFormulaFactory() { Assert.assertEquals(F.AND1, F.g.and(F.g.variable("a"), F.g.variable("b"))); - Assert.assertEquals(F.AND3, F.g.and(F.OR1, F.OR2)); + Assert.assertEquals(F.AND3, F.g.and(OR1, F.OR2)); Assert.assertEquals(F.f.and(F.f.or(F.f.variable("a"), F.f.variable("b")), F.f.or(F.f.variable("x"), F.f.literal("y", false))), F.g.and(F.g.or(F.g.literal("y", false), F.g.variable("x")), F.f.or(F.g.variable("b"), F.g.variable("a")))); - Assert.assertEquals(F.f.and(F.A, F.NB, F.OR1, F.NX), F.g.and(F.g.literal("x", false), F.g.variable("a"), F.g.literal("b", false), F.g.or(F.g.variable("x"), F.g.variable("y")))); + Assert.assertEquals(F.f.and(F.A, F.NB, OR1, F.NX), F.g.and(F.g.literal("x", false), F.g.variable("a"), F.g.literal("b", false), F.g.or(F.g.variable("x"), F.g.variable("y")))); Assert.assertNotEquals(F.AND1, F.g.variable("a")); Assert.assertNotEquals(F.AND1, F.g.and(F.g.literal("a", false), F.g.variable("b"))); Assert.assertNotEquals(F.AND1, F.g.and(F.g.variable("a"), F.g.literal("b", false))); @@ -152,7 +154,7 @@ public void testEqualsDifferentFormulaFactory() { @Test public void testHash() { - Formula and = F.f.and(F.OR1, F.OR2); + Formula and = F.f.and(OR1, F.OR2); Assert.assertEquals(F.AND3.hashCode(), and.hashCode()); Assert.assertEquals(F.AND3.hashCode(), and.hashCode()); Assert.assertEquals(F.AND2.hashCode(), F.f.and(F.NA, F.NB).hashCode()); @@ -194,8 +196,11 @@ public void testAtomicFormula() { } @Test - public void testContains() { + public void testContains() throws ParserException { Assert.assertTrue(F.AND3.containsVariable(F.f.variable("x"))); Assert.assertFalse(F.AND3.containsVariable(F.f.variable("a"))); + PropositionalParser parser = new PropositionalParser(F.f); + Formula contAnd = parser.parse("a & b & (c | (d & e))"); + Assert.assertTrue(contAnd.containsNode(parser.parse("d & e"))); } } diff --git a/src/test/java/org/logicng/formulas/CacheTest.java b/src/test/java/org/logicng/formulas/CacheTest.java new file mode 100644 index 00000000..4c892bb9 --- /dev/null +++ b/src/test/java/org/logicng/formulas/CacheTest.java @@ -0,0 +1,82 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-2016 Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +package org.logicng.formulas; + +import org.junit.Assert; +import org.junit.Test; +import org.logicng.formulas.cache.FunctionCacheEntry; +import org.logicng.formulas.cache.PredicateCacheEntry; +import org.logicng.formulas.cache.TransformationCacheEntry; + +import java.util.Arrays; +import java.util.List; + +/** + * Unit tests for the package formulas.cache. + * @version 1.1 + * @since 1.1 + */ +public class CacheTest { + + @Test + public void testDescription() { + Assert.assertEquals("TransformationCacheEntry{description=and-inverter graph}", TransformationCacheEntry.AIG.description()); + Assert.assertEquals("TransformationCacheEntry{description=negation normal form}", TransformationCacheEntry.NNF.description()); + Assert.assertEquals("TransformationCacheEntry{description=Plaisted & Greenbaum conjunctive normal form (positive polarity)}", TransformationCacheEntry.PLAISTED_GREENBAUM_POS.description()); + Assert.assertEquals("TransformationCacheEntry{description=Tseitin conjunctive normal form}", TransformationCacheEntry.TSEITIN.description()); + Assert.assertEquals("TransformationCacheEntry{description=factorized conjunctive normal form}", TransformationCacheEntry.FACTORIZED_CNF.description()); + + Assert.assertEquals("PredicateCacheEntry{description=and-inverter graph}", PredicateCacheEntry.IS_AIG.description()); + Assert.assertEquals("PredicateCacheEntry{description=tautology}", PredicateCacheEntry.IS_TAUTOLOGY.description()); + Assert.assertEquals("PredicateCacheEntry{description=conjunctive normal form}", PredicateCacheEntry.IS_CNF.description()); + + Assert.assertEquals("FunctionCacheEntry{description=literal profile}", FunctionCacheEntry.LITPROFILE.description()); + Assert.assertEquals("FunctionCacheEntry{description=variable profile}", FunctionCacheEntry.VARPROFILE.description()); + Assert.assertEquals("FunctionCacheEntry{description=sub-formulas}", FunctionCacheEntry.SUBFORMULAS.description()); + } + + @Test + public void testValues() { + List valuesTrans = Arrays.asList(TransformationCacheEntry.values()); + Assert.assertTrue(valuesTrans.size() == 9); + Assert.assertTrue(valuesTrans.contains(TransformationCacheEntry.valueOf("FACTORIZED_DNF"))); + Assert.assertTrue(valuesTrans.contains(TransformationCacheEntry.valueOf("PLAISTED_GREENBAUM_NEG"))); + + List valuesPred = Arrays.asList(PredicateCacheEntry.values()); + Assert.assertTrue(valuesPred.size() == 5); + Assert.assertTrue(valuesPred.contains(PredicateCacheEntry.valueOf("IS_DNF"))); + Assert.assertTrue(valuesPred.contains(PredicateCacheEntry.valueOf("IS_SAT"))); + + List valuesFunc = Arrays.asList(FunctionCacheEntry.values()); + Assert.assertTrue(valuesFunc.size() == 3); + Assert.assertTrue(valuesFunc.contains(FunctionCacheEntry.valueOf("LITPROFILE"))); + Assert.assertTrue(valuesFunc.contains(FunctionCacheEntry.valueOf("SUBFORMULAS"))); + } + +} diff --git a/src/test/java/org/logicng/formulas/EquivalenceTest.java b/src/test/java/org/logicng/formulas/EquivalenceTest.java index 211f052d..9f3516e2 100644 --- a/src/test/java/org/logicng/formulas/EquivalenceTest.java +++ b/src/test/java/org/logicng/formulas/EquivalenceTest.java @@ -39,7 +39,7 @@ /** * Unit Tests for the class {@link Equivalence}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class EquivalenceTest { @@ -181,5 +181,7 @@ public void testAtomicFormula() { public void testContains() { Assert.assertTrue(F.EQ4.containsVariable(F.f.variable("a"))); Assert.assertFalse(F.EQ4.containsVariable(F.f.variable("x"))); + Assert.assertTrue(F.EQ4.containsNode(F.IMP1)); + Assert.assertFalse(F.EQ4.containsNode(F.IMP4)); } } diff --git a/src/test/java/org/logicng/formulas/FormulaFactoryTest.java b/src/test/java/org/logicng/formulas/FormulaFactoryTest.java index 89f8e4f2..4ba85d3d 100644 --- a/src/test/java/org/logicng/formulas/FormulaFactoryTest.java +++ b/src/test/java/org/logicng/formulas/FormulaFactoryTest.java @@ -36,9 +36,12 @@ import org.logicng.solvers.sat.GlucoseConfig; import org.logicng.solvers.sat.MiniSatConfig; +import java.util.ArrayList; +import java.util.List; + /** * Test some basic formula factory functionality. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class FormulaFactoryTest { @@ -116,4 +119,30 @@ public void testGeneratedVariables() { Assert.assertEquals("@RESERVED_PB_f_0", pbVar.name()); Assert.assertEquals("@RESERVED_CNF_f_0", cnfVar.name()); } + + @Test + public void testCNF() { + FormulaFactory f = new FormulaFactory(); + Variable a = f.variable("A"); + Variable b = f.variable("B"); + Variable c = f.variable("C"); + Variable d = f.variable("D"); + Formula clause1 = f.or(a, b); + Formula clause2 = f.or(c, d.negate()); + Formula nClause1 = f.implication(a, c); + + List clauses = new ArrayList<>(); + clauses.add(clause1); + clauses.add(clause2); + + List nClauses = new ArrayList<>(); + nClauses.add(clause1); + nClauses.add(clause2); + nClauses.add(nClause1); + + Formula cnf = f.cnf(clauses); + Formula nCnf = f.cnf(nClauses); + Assert.assertEquals(cnf, cnf.cnf()); + Assert.assertNotEquals(nCnf, nCnf.cnf()); + } } diff --git a/src/test/java/org/logicng/formulas/FormulaTest.java b/src/test/java/org/logicng/formulas/FormulaTest.java index f45e16bb..932c7aba 100644 --- a/src/test/java/org/logicng/formulas/FormulaTest.java +++ b/src/test/java/org/logicng/formulas/FormulaTest.java @@ -33,13 +33,15 @@ import org.logicng.datastructures.Tristate; import org.logicng.formulas.cache.CacheEntry; +import java.util.Arrays; + 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; /** * Test some common formula functionality. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class FormulaTest { @@ -83,6 +85,22 @@ public void testFunctionCache() { Assert.assertEquals("key2", formula.functionCacheEntry(MyOwnCacheKey.MYKEY2)); } + @Test + public void testFType() { + Assert.assertEquals(FType.AND, FType.valueOf("AND")); + Assert.assertEquals(FType.NONE, FType.valueOf("NONE")); + Assert.assertTrue(Arrays.asList(FType.values()).contains(FType.valueOf("PBC"))); + Assert.assertEquals(10, FType.values().length); + } + + @Test + public void testCType() { + Assert.assertEquals(CType.EQ, CType.valueOf("EQ")); + Assert.assertEquals(CType.LE, CType.valueOf("LE")); + Assert.assertTrue(Arrays.asList(CType.values()).contains(CType.valueOf("GT"))); + Assert.assertEquals(5, CType.values().length); + } + private enum MyOwnCacheKey implements CacheEntry { MYKEY1("My Key 1"), MYKEY2("My Key 2"); diff --git a/src/test/java/org/logicng/formulas/NotTest.java b/src/test/java/org/logicng/formulas/NotTest.java index c237500f..27dd6216 100644 --- a/src/test/java/org/logicng/formulas/NotTest.java +++ b/src/test/java/org/logicng/formulas/NotTest.java @@ -39,7 +39,7 @@ /** * Unit Tests for the class {@link Not}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class NotTest { @@ -123,6 +123,7 @@ public void testHash() { @Test public void testNumberOfAtoms() { Assert.assertEquals(2, F.NOT1.numberOfAtoms()); + Assert.assertEquals(2, F.NOT2.numberOfAtoms()); Assert.assertEquals(2, F.OR1.numberOfAtoms()); Assert.assertEquals(2, F.OR1.numberOfAtoms()); } diff --git a/src/test/java/org/logicng/formulas/OrTest.java b/src/test/java/org/logicng/formulas/OrTest.java index bcf8d23d..2812ea7a 100644 --- a/src/test/java/org/logicng/formulas/OrTest.java +++ b/src/test/java/org/logicng/formulas/OrTest.java @@ -41,7 +41,7 @@ /** * Unit Tests for the class {@link Or}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class OrTest { @@ -187,8 +187,11 @@ public void testAtomicFormula() { } @Test - public void testContains() { + public void testContains() throws ParserException { Assert.assertTrue(F.OR1.containsVariable(F.f.variable("x"))); Assert.assertFalse(F.OR1.containsVariable(F.f.variable("a"))); + PropositionalParser parser = new PropositionalParser(F.f); + Formula contAnd = parser.parse("a | b | (c & (d | e))"); + Assert.assertTrue(contAnd.containsNode(parser.parse("d | e"))); } } diff --git a/src/test/java/org/logicng/formulas/PBConstraintTest.java b/src/test/java/org/logicng/formulas/PBConstraintTest.java index 9beb5fa9..2076753d 100644 --- a/src/test/java/org/logicng/formulas/PBConstraintTest.java +++ b/src/test/java/org/logicng/formulas/PBConstraintTest.java @@ -42,7 +42,7 @@ /** * Unit Tests for the class {@link PBConstraint}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class PBConstraintTest { @@ -112,18 +112,21 @@ public void testGetters() { Assert.assertEquals(CType.LE, pb1.comparator()); Assert.assertEquals(2, pb1.rhs()); Assert.assertFalse(pb1.isCC()); + Assert.assertEquals(3, pb1.maxWeight()); Assert.assertArrayEquals(lits2, pb2.operands()); Assert.assertArrayEquals(coeffs2, pb2.coefficients()); Assert.assertEquals(CType.LE, pb2.comparator()); Assert.assertEquals(8, pb2.rhs()); Assert.assertFalse(pb2.isCC()); + Assert.assertEquals(7, pb2.maxWeight()); Assert.assertArrayEquals(lits1, cc1.operands()); Assert.assertArrayEquals(coeffsCC1, cc1.coefficients()); Assert.assertEquals(CType.LT, cc1.comparator()); Assert.assertEquals(1, cc1.rhs()); Assert.assertTrue(cc1.isCC()); + Assert.assertEquals(1, cc1.maxWeight()); Assert.assertArrayEquals(litsCC2, cc2.operands()); Assert.assertArrayEquals(coeffsCC2, cc2.coefficients()); @@ -187,6 +190,7 @@ public void testVariables() { final SortedSet lits1 = new TreeSet<>(Collections.singletonList(f.variable("a"))); final SortedSet lits2 = new TreeSet<>(Arrays.asList(f.variable("a"), f.variable("b"), f.variable("c"))); Assert.assertEquals(lits1, pb1.variables()); + Assert.assertEquals(lits1, pb1.variables()); Assert.assertEquals(lits2, pb2.variables()); Assert.assertEquals(lits1, cc1.variables()); Assert.assertEquals(lits2, cc2.variables()); diff --git a/src/test/java/org/logicng/formulas/printer/DefaultStringRepresentationTest.java b/src/test/java/org/logicng/formulas/printer/DefaultStringRepresentationTest.java new file mode 100644 index 00000000..d34088cd --- /dev/null +++ b/src/test/java/org/logicng/formulas/printer/DefaultStringRepresentationTest.java @@ -0,0 +1,72 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-2016 Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +package org.logicng.formulas.printer; + +import org.junit.Assert; +import org.junit.Test; +import org.logicng.formulas.F; + +/** + * Unit tests for {@link DefaultStringRepresentation} + * @version 1.1 + * @since 1.0 + */ +public class DefaultStringRepresentationTest { + private final FormulaStringRepresentation sr = new DefaultStringRepresentation(); + + @Test + public void testDefaultPrinter() { + Assert.assertEquals("$false", F.f.string(F.FALSE, sr)); + Assert.assertEquals("$true", F.f.string(F.TRUE, sr)); + Assert.assertEquals("x", F.f.string(F.X, sr)); + Assert.assertEquals("~a", F.f.string(F.NA, sr)); + Assert.assertEquals("x1", F.f.string(F.f.variable("x1"), sr)); + Assert.assertEquals("x190", F.f.string(F.f.variable("x190"), sr)); + Assert.assertEquals("x234", F.f.string(F.f.variable("x234"), sr)); + Assert.assertEquals("x567", F.f.string(F.f.variable("x567"), sr)); + Assert.assertEquals("abc8", F.f.string(F.f.variable("abc8"), sr)); + Assert.assertEquals("~a => ~b", F.f.string(F.IMP2, sr)); + Assert.assertEquals("a & b => x | y", F.f.string(F.IMP3, sr)); + Assert.assertEquals("a => b <=> ~a => ~b", F.f.string(F.EQ4, sr)); + Assert.assertEquals("(x | y) & (~x | ~y)", F.f.string(F.AND3, sr)); + Assert.assertEquals("a & b & c & x", F.f.string(F.f.and(F.A, F.B, F.C, F.X), sr)); + Assert.assertEquals("a | b | c | x", F.f.string(F.f.or(F.A, F.B, F.C, F.X), sr)); + Assert.assertEquals("2*a + -4*b + 3*x = 2", F.f.string(F.PBC1, sr)); + Assert.assertEquals("2*a + -4*b + 3*x > 2", F.f.string(F.PBC2, sr)); + Assert.assertEquals("2*a + -4*b + 3*x >= 2", F.f.string(F.PBC3, sr)); + Assert.assertEquals("2*a + -4*b + 3*x < 2", F.f.string(F.PBC4, sr)); + Assert.assertEquals("2*a + -4*b + 3*x <= 2", F.f.string(F.PBC5, sr)); + } + + @Test + public void testToString() { + Assert.assertEquals("DefaultStringRepresentation", sr.toString()); + } + +} diff --git a/src/test/java/org/logicng/formulas/printer/LatexStringRepresentationTest.java b/src/test/java/org/logicng/formulas/printer/LatexStringRepresentationTest.java index 5dc448c6..c9b864d8 100644 --- a/src/test/java/org/logicng/formulas/printer/LatexStringRepresentationTest.java +++ b/src/test/java/org/logicng/formulas/printer/LatexStringRepresentationTest.java @@ -31,17 +31,18 @@ import org.junit.Assert; import org.junit.Test; import org.logicng.formulas.F; +import org.logicng.formulas.Variable; /** * Unit tests for {@link LatexStringRepresentation} - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class LatexStringRepresentationTest { private final FormulaStringRepresentation sr = new LatexStringRepresentation(); @Test - public void testUTF8Printer() { + public void testLatexPrinter() { Assert.assertEquals("\\bottom", F.f.string(F.FALSE, sr)); Assert.assertEquals("\\top", F.f.string(F.TRUE, sr)); Assert.assertEquals("x", F.f.string(F.X, sr)); @@ -63,4 +64,11 @@ public void testUTF8Printer() { Assert.assertEquals("2\\cdot a + -4\\cdot b + 3\\cdot x < 2", F.f.string(F.PBC4, sr)); Assert.assertEquals("2\\cdot a + -4\\cdot b + 3\\cdot x \\leq 2", F.f.string(F.PBC5, sr)); } + + @Test + public void testSpecialCases() { + Variable var = F.f.variable("\ntest9t"); + Assert.assertEquals("\ntest9t", F.f.string(var, sr)); + Assert.assertEquals("LatexStringRepresentation", sr.toString()); + } } diff --git a/src/test/java/org/logicng/formulas/printer/UTF8StringRepresentationTest.java b/src/test/java/org/logicng/formulas/printer/UTF8StringRepresentationTest.java index 586df1ed..6956d159 100644 --- a/src/test/java/org/logicng/formulas/printer/UTF8StringRepresentationTest.java +++ b/src/test/java/org/logicng/formulas/printer/UTF8StringRepresentationTest.java @@ -31,10 +31,11 @@ import org.junit.Assert; import org.junit.Test; import org.logicng.formulas.F; +import org.logicng.formulas.Variable; /** * Unit tests for {@link UTF8StringRepresentation} - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class UTF8StringRepresentationTest { @@ -63,4 +64,11 @@ public void testUTF8Printer() { Assert.assertEquals("2a + -4b + 3x < 2", F.f.string(F.PBC4, sr)); Assert.assertEquals("2a + -4b + 3x ≤ 2", F.f.string(F.PBC5, sr)); } + + @Test + public void testSpecialCases() { + Variable var = F.f.variable("\ntest9t"); + Assert.assertEquals("\ntest9t", F.f.string(var, sr)); + Assert.assertEquals("UTF8StringRepresentation", sr.toString()); + } } diff --git a/src/test/java/org/logicng/functions/SubformulaTest.java b/src/test/java/org/logicng/functions/SubformulaTest.java index 8fb1563c..e1618b08 100644 --- a/src/test/java/org/logicng/functions/SubformulaTest.java +++ b/src/test/java/org/logicng/functions/SubformulaTest.java @@ -37,9 +37,11 @@ import java.util.LinkedHashSet; +import static org.logicng.formulas.cache.FunctionCacheEntry.SUBFORMULAS; + /** * Unit tests for {@link SubNodeFunction}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class SubformulaTest { @@ -191,4 +193,12 @@ public void subformulasTest() throws ParserException { expected.add(p.parse("((a & ~b & c) | (d & (~e | c))) & (a => (~x | y) & (x | ~z))")); Assert.assertEquals(expected, f1.apply(new SubNodeFunction())); } + + @Test + public void testNotCache() throws ParserException { + PropositionalParser p = new PropositionalParser(F.f); + final Formula f1 = p.parse("(d | (a & b)) & (c | (a & b)) | (a & b )"); + f1.apply(new SubNodeFunction(), false); + Assert.assertNull(f1.functionCacheEntry(SUBFORMULAS)); + } } diff --git a/src/test/java/org/logicng/io/parsers/PropositionalParserTest.java b/src/test/java/org/logicng/io/parsers/PropositionalParserTest.java index a251477f..9f45f5a5 100644 --- a/src/test/java/org/logicng/io/parsers/PropositionalParserTest.java +++ b/src/test/java/org/logicng/io/parsers/PropositionalParserTest.java @@ -38,11 +38,19 @@ /** * Unit Tests for the class {@link PropositionalParser}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class PropositionalParserTest { + @Test + public void testExceptions() throws ParserException { + PropositionalParser parser = new PropositionalParser(F.f); + Assert.assertEquals(F.f.verum(), parser.parse("")); + String s = null; + Assert.assertEquals(F.f.verum(), parser.parse(s)); + } + @Test public void testParseConstants() throws ParserException { PropositionalParser parser = new PropositionalParser(F.f); diff --git a/src/test/java/org/logicng/io/parsers/PseudoBooleanParserTest.java b/src/test/java/org/logicng/io/parsers/PseudoBooleanParserTest.java index 14ef942e..6499d8dc 100644 --- a/src/test/java/org/logicng/io/parsers/PseudoBooleanParserTest.java +++ b/src/test/java/org/logicng/io/parsers/PseudoBooleanParserTest.java @@ -41,11 +41,18 @@ /** * Unit Tests for the class {@link PseudoBooleanParser}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class PseudoBooleanParserTest { + @Test + public void testExceptions() throws ParserException { + PseudoBooleanParser parser = new PseudoBooleanParser(F.f); + Assert.assertEquals(F.f.verum(), parser.parse("")); + Assert.assertEquals(F.f.verum(), parser.parse((String) null)); + } + @Test public void testParseConstants() throws ParserException { PseudoBooleanParser parser = new PseudoBooleanParser(F.f); diff --git a/src/test/java/org/logicng/io/writers/FormulaDotFileWriterTest.java b/src/test/java/org/logicng/io/writers/FormulaDotFileWriterTest.java index cb9916e9..04994079 100644 --- a/src/test/java/org/logicng/io/writers/FormulaDotFileWriterTest.java +++ b/src/test/java/org/logicng/io/writers/FormulaDotFileWriterTest.java @@ -43,7 +43,7 @@ /** * Unit tests for the {@link FormulaDotFileWriter}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class FormulaDotFileWriterTest { @@ -78,9 +78,17 @@ public void testFormulas() throws IOException, ParserException { testFiles("f5", f5); } + @Test + public void testDuplicateFormulaParts() throws ParserException, IOException { + final Formula f6 = p.parse("(a & b) | (c & ~(a & b))"); + testFiles("f6", f6); + final Formula f7 = p.parse("(c & d) | (a & b) | ((c & d) <=> (a & b))"); + testFiles("f7", f7); + } + private void testFiles(final String fileName, final Formula formula) throws IOException { FormulaDotFileWriter.write("tests/writers/temp/" + fileName + "_t.dot", formula, true); - FormulaDotFileWriter.write("tests/writers/temp/" + fileName + "_f.dot", formula, false); + FormulaDotFileWriter.write("tests/writers/temp/" + fileName + "_f", formula, false); final File expectedT = new File("tests/writers/formulas-dot/" + fileName + "_t.dot"); final File expectedF = new File("tests/writers/formulas-dot/" + fileName + "_f.dot"); final File tempT = new File("tests/writers/temp/" + fileName + "_t.dot"); diff --git a/src/test/java/org/logicng/predicates/CNFPredicateTest.java b/src/test/java/org/logicng/predicates/CNFPredicateTest.java index d3702293..b6e14106 100644 --- a/src/test/java/org/logicng/predicates/CNFPredicateTest.java +++ b/src/test/java/org/logicng/predicates/CNFPredicateTest.java @@ -34,7 +34,7 @@ /** * Unit tests for the cnf predicate. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class CNFPredicateTest { @@ -59,4 +59,9 @@ public void test() { Assert.assertFalse(F.NOT2.holds(cnfPredicate)); Assert.assertFalse(F.f.and(F.OR1, F.EQ1).holds(cnfPredicate)); } + + @Test + public void testToString() { + Assert.assertEquals("CNFPredicate", cnfPredicate.toString()); + } } diff --git a/src/test/java/org/logicng/predicates/DNFPredicateTest.java b/src/test/java/org/logicng/predicates/DNFPredicateTest.java index 4d12a480..cb4797a2 100644 --- a/src/test/java/org/logicng/predicates/DNFPredicateTest.java +++ b/src/test/java/org/logicng/predicates/DNFPredicateTest.java @@ -34,7 +34,7 @@ /** * Unit tests for the dnf predicate. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class DNFPredicateTest { @@ -59,4 +59,9 @@ public void test() { Assert.assertFalse(F.NOT2.holds(dnfPredicate)); Assert.assertFalse(F.f.or(F.AND1, F.EQ1).holds(dnfPredicate)); } + + @Test + public void testToString(){ + Assert.assertEquals("DNFPredicate", dnfPredicate.toString()); + } } diff --git a/src/test/java/org/logicng/predicates/satisfiability/PredicatesTest.java b/src/test/java/org/logicng/predicates/satisfiability/PredicatesTest.java index 810a78a2..62bb2879 100644 --- a/src/test/java/org/logicng/predicates/satisfiability/PredicatesTest.java +++ b/src/test/java/org/logicng/predicates/satisfiability/PredicatesTest.java @@ -30,17 +30,22 @@ import org.junit.Assert; import org.junit.Test; +import org.logicng.datastructures.Tristate; import org.logicng.formulas.F; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.FormulaPredicate; +import org.logicng.formulas.Variable; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; import org.logicng.solvers.sat.PigeonHoleGenerator; +import static org.logicng.formulas.cache.PredicateCacheEntry.IS_SAT; +import static org.logicng.formulas.cache.PredicateCacheEntry.IS_TAUTOLOGY; + /** * Unit tests for the different satisfiability predicates. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class PredicatesTest { @@ -126,6 +131,22 @@ public void testSat() { Assert.assertFalse(new PigeonHoleGenerator(F.f).generate(3).holds(sat)); } + @Test + public void testNotCache() { + final FormulaFactory f = F.f; + final Formula taut = f.or(F.AND1, f.and(F.NA, F.B), f.and(F.A, F.NB), f.and(F.NA, F.NB)); + taut.holds(tau, false); + Assert.assertEquals(Tristate.UNDEF, taut.predicateCacheEntry(IS_TAUTOLOGY)); + + Variable a = f.variable("A"); + Variable b = f.variable("B"); + Variable c = f.variable("C"); + Variable d = f.variable("D"); + final Formula satDNF = f.or(f.and(a, b), f.and(b, c), f.and(d, a)); + Assert.assertTrue(satDNF.holds(sat, false)); + Assert.assertEquals(Tristate.UNDEF, satDNF.predicateCacheEntry(IS_SAT)); + } + @Test public void testToString() { final SATSolver s = MiniSat.miniSat(f); diff --git a/src/test/java/org/logicng/propositions/ExtendedPropositionTest.java b/src/test/java/org/logicng/propositions/ExtendedPropositionTest.java index 0339232e..0ae61c94 100644 --- a/src/test/java/org/logicng/propositions/ExtendedPropositionTest.java +++ b/src/test/java/org/logicng/propositions/ExtendedPropositionTest.java @@ -37,11 +37,12 @@ import org.logicng.io.parsers.PropositionalParser; import java.util.Arrays; +import java.util.Collections; import java.util.Objects; /** * Unit tests for {@link ExtendedProposition}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class ExtendedPropositionTest { @@ -76,6 +77,14 @@ public void testGetters() throws ParserException { Assert.assertEquals("prop4", prop4.bagback().description); } + @Test + public void testFormula() throws ParserException { + FormulaFactory f = new FormulaFactory(); + + Assert.assertEquals(p.parse("a & b"), prop1.formula(f)); + Assert.assertEquals(p.parse("a & b & ~c"), prop3.formula(f)); + } + @Test public void testHashCode() throws ParserException { ExtendedProposition prop11 = new ExtendedProposition<>(new BagPack("prop1"), p.parse("a & b")); @@ -89,7 +98,7 @@ public void testHashCode() throws ParserException { public void testEquals() throws ParserException { ExtendedProposition prop11 = new ExtendedProposition<>(new BagPack("prop1"), p.parse("a & b")); ExtendedProposition prop21 = new ExtendedProposition<>(new BagPack("prop2"), Arrays.asList(p.parse("a & b"), p.parse("~c"))); - ExtendedProposition prop31 = new ExtendedProposition<>(new BagPack("prop3"), Arrays.asList(p.parse("a & b"))); + ExtendedProposition prop31 = new ExtendedProposition<>(new BagPack("prop3"), Collections.singletonList(p.parse("a & b"))); Assert.assertTrue(prop1.equals(prop1)); Assert.assertTrue(prop1.equals(prop11)); Assert.assertTrue(prop2.equals(prop21)); diff --git a/src/test/java/org/logicng/propositions/StandardPropositionTest.java b/src/test/java/org/logicng/propositions/StandardPropositionTest.java index 88696d15..196b44ac 100644 --- a/src/test/java/org/logicng/propositions/StandardPropositionTest.java +++ b/src/test/java/org/logicng/propositions/StandardPropositionTest.java @@ -40,7 +40,7 @@ /** * Unit tests for {@link StandardProposition}. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class StandardPropositionTest { @@ -51,6 +51,7 @@ public class StandardPropositionTest { private final StandardProposition prop3; private final StandardProposition prop4; private final StandardProposition prop5; + private final StandardProposition prop6; public StandardPropositionTest() throws ParserException { FormulaFactory f = new FormulaFactory(); @@ -60,6 +61,7 @@ public StandardPropositionTest() throws ParserException { prop3 = new StandardProposition("prop3", Arrays.asList(p.parse("a & b"), p.parse("~c"))); prop4 = new StandardProposition("prop4", p.parse("a & b"), p.parse("~c")); prop5 = new StandardProposition("prop5", new ImmutableFormulaList(p.parse("a & b"), p.parse("~c"))); + prop6 = new StandardProposition(null, p.parse("a & b")); } @Test @@ -77,6 +79,15 @@ public void testGetters() throws ParserException { Assert.assertEquals("prop3", prop3.description()); Assert.assertEquals("prop4", prop4.description()); Assert.assertEquals("prop5", prop5.description()); + Assert.assertEquals("", prop6.description()); + } + + @Test + public void testFormula() throws ParserException { + FormulaFactory f = new FormulaFactory(); + + Assert.assertEquals(p.parse("a & b"), prop1.formula(f)); + Assert.assertEquals(p.parse("a & b & ~c"), prop3.formula(f)); } @Test diff --git a/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java b/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java index aeed4e8e..5af36b02 100644 --- a/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java +++ b/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java @@ -29,16 +29,22 @@ import org.junit.Assert; import org.junit.Test; +import org.logicng.cardinalityconstraints.CCConfig; import org.logicng.collections.ImmutableFormulaList; +import org.logicng.configurations.ConfigurationType; import org.logicng.datastructures.Assignment; import org.logicng.datastructures.Tristate; import org.logicng.formulas.CType; +import org.logicng.formulas.FType; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Literal; +import org.logicng.formulas.PBConstraint; import org.logicng.formulas.Variable; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; +import java.util.ArrayList; +import java.util.Arrays; import java.util.LinkedList; import java.util.List; @@ -53,8 +59,10 @@ public class PBEncoderTest { private PBEncoder[] encoders; public PBEncoderTest() { - this.encoders = new PBEncoder[1]; + this.encoders = new PBEncoder[3]; this.encoders[0] = new PBEncoder(this.f, new PBConfig.Builder().pbEncoding(PBConfig.PB_ENCODER.SWC).build()); + this.encoders[1] = new PBEncoder(this.f, new PBConfig.Builder().pbEncoding(PBConfig.PB_ENCODER.BINARY_MERGE).binaryMergeUseGAC(false).build(), new CCConfig.Builder().amoEncoding(CCConfig.AMO_ENCODER.NESTED).build()); + this.encoders[2] = new PBEncoder(this.f, null); } @Test @@ -138,4 +146,50 @@ private void testCC(int numLits, int rhs, int expected, final PBEncoder encoder) Assert.assertTrue(model.positiveLiterals().size() <= rhs); } + @Test + public void testNotNullConfig() { + for (final PBEncoder encoder : this.encoders) { + Assert.assertNotNull(encoder.config()); + } + } + + @Test + public void testSpecialCases() { + List lits = new ArrayList<>(); + lits.add(f.literal("m", true)); + lits.add(f.literal("n", true)); + List coeffs = new ArrayList<>(); + coeffs.add(2); + coeffs.add(1); + PBConstraint truePBC = f.pbc(CType.GE, 0, lits, coeffs); + for (final PBEncoder encoder : this.encoders) { + Assert.assertEquals(new ImmutableFormulaList(FType.AND), encoder.encode(truePBC)); + } + } + + @Test + public void testCCNormalized() { + List lits = new ArrayList<>(); + lits.add(f.literal("m", true)); + lits.add(f.literal("n", true)); + List coeffs2 = new ArrayList<>(); + coeffs2.add(2); + coeffs2.add(2); + PBConstraint normCC = f.pbc(CType.LE, 2, lits, coeffs2); + Assert.assertEquals("AND[~m | ~n]", encoders[0].encode(normCC).toString()); + } + + @Test + public void testConfigToString() { + Assert.assertEquals("PBConfig{\n" + + "pbEncoder=SWC\n" + + "binaryMergeUseGAC=true\n" + + "binaryMergeNoSupportForSingleBit=false\n" + + "binaryMergeUseWatchDog=true\n" + + "}\n", encoders[0].config().toString()); + Assert.assertTrue(encoders[0].config().toString().contains("pbEncoder=" + PBConfig.PB_ENCODER.valueOf("SWC"))); + Assert.assertEquals(ConfigurationType.PB_ENCODER, encoders[0].config().type()); + Assert.assertEquals("PBSWC", new PBSWC(f).toString()); + Assert.assertTrue(Arrays.asList(PBConfig.PB_ENCODER.values()).contains(PBConfig.PB_ENCODER.valueOf("ADDER_NETWORKS"))); + } } diff --git a/src/test/java/org/logicng/solvers/datastructures/LNGHeapTest.java b/src/test/java/org/logicng/solvers/datastructures/LNGHeapTest.java new file mode 100644 index 00000000..3bc0f116 --- /dev/null +++ b/src/test/java/org/logicng/solvers/datastructures/LNGHeapTest.java @@ -0,0 +1,55 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-2016 Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +package org.logicng.solvers.datastructures; + +import org.junit.Assert; +import org.junit.Test; +import org.logicng.solvers.sat.MiniCard; +import org.logicng.solvers.sat.MiniSatStyleSolver; + +/** + * Unit tests for the class {@link LNGHeap}. + * @version 1.1 + * @since 1.1 + */ +public class LNGHeapTest { + + @Test + public void test() { + MiniSatStyleSolver solver = new MiniCard(); + LNGHeap heap = new LNGHeap(solver); + Assert.assertTrue(heap.empty()); + heap.insert(5); + Assert.assertEquals(5, heap.get(0)); + Assert.assertTrue(heap.toString().contains("5")); + Assert.assertEquals(1, heap.size()); + heap.clear(); + Assert.assertTrue(heap.empty()); + } +} diff --git a/src/test/java/org/logicng/solvers/datastructures/TestToStrings.java b/src/test/java/org/logicng/solvers/datastructures/SolversDatastructuresTest.java similarity index 93% rename from src/test/java/org/logicng/solvers/datastructures/TestToStrings.java rename to src/test/java/org/logicng/solvers/datastructures/SolversDatastructuresTest.java index 9b90ac6d..c7280578 100644 --- a/src/test/java/org/logicng/solvers/datastructures/TestToStrings.java +++ b/src/test/java/org/logicng/solvers/datastructures/SolversDatastructuresTest.java @@ -33,12 +33,14 @@ import org.logicng.collections.LNGIntVector; import org.logicng.datastructures.Tristate; +import java.util.Arrays; + /** * Unit tests for the toString() methods of the solver data structures. - * @version 1.0 + * @version 1.1 * @since 1.0 */ -public class TestToStrings { +public class SolversDatastructuresTest { @Test public void testCLClause() { @@ -135,6 +137,9 @@ public void testMSClause() { clause.setSeen(true); final String expected = "MSClause{activity=0.0, learnt=true, szWithoutSelectors=0, seen=true, lbd=42, canBeDel=true, oneWatched=false, isAtMost=false, atMostWatchers=-1, lits=[1, 2, 3]}"; Assert.assertEquals(expected, clause.toString()); + Assert.assertTrue(clause.equals(clause)); + Assert.assertEquals(clause.hashCode(), clause.hashCode()); + Assert.assertFalse(clause.equals("Test")); } @Test @@ -180,6 +185,13 @@ public void testMSWatcher() { final MSWatcher watcher = new MSWatcher(clause, 2); final String expected = "MSWatcher{clause=MSClause{activity=0.0, learnt=true, szWithoutSelectors=0, seen=false, lbd=0, canBeDel=true, oneWatched=false, isAtMost=false, atMostWatchers=-1, lits=[1, 2, 3]}, blocker=2}"; Assert.assertEquals(expected, watcher.toString()); + Assert.assertEquals(watcher.hashCode(), watcher.hashCode()); + } + + @Test + public void testCLVarState() { + Assert.assertEquals(CLVar.State.ELIMINATED, CLVar.State.valueOf("ELIMINATED")); + Assert.assertTrue(Arrays.asList(CLVar.State.values()).contains(CLVar.State.valueOf("FREE"))); } } diff --git a/src/test/java/org/logicng/solvers/maxsat/PartialMaxSATTest.java b/src/test/java/org/logicng/solvers/maxsat/PartialMaxSATTest.java index 7846167c..4f9a4343 100644 --- a/src/test/java/org/logicng/solvers/maxsat/PartialMaxSATTest.java +++ b/src/test/java/org/logicng/solvers/maxsat/PartialMaxSATTest.java @@ -50,7 +50,7 @@ /** * Unit tests for the MaxSAT solvers. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class PartialMaxSATTest { @@ -161,6 +161,7 @@ public void testTimeoutHandler() throws IOException { readCNF(solver, "tests/partialmaxsat/c1355_F176gat-1278gat@1.wcnf"); MaxSATHandler handler = new TimeoutMaxSATHandler(1000); Assert.assertEquals(MaxSAT.MaxSATResult.UNDEF, solver.solve(handler)); + Assert.assertTrue(handler.lowerBoundApproximation() < 13); solver = MaxSATSolver.wbo(new MaxSATConfig.Builder().verbosity(SOME).output(logStream).build()); readCNF(solver, "tests/partialmaxsat/c1355_F1229gat@1.wcnf"); @@ -168,6 +169,15 @@ public void testTimeoutHandler() throws IOException { Assert.assertEquals(MaxSAT.MaxSATResult.OPTIMUM, solver.solve(handler)); } + @Test + public void testTimeoutHandlerUB() throws IOException { + MaxSATSolver solver = MaxSATSolver.linearSU(new MaxSATConfig.Builder().verbosity(SOME).output(logStream).build()); + readCNF(solver, "tests/partialmaxsat/c1355_F1229gat@1.wcnf"); + MaxSATHandler handler = new TimeoutMaxSATHandler(5000); + Assert.assertEquals(MaxSAT.MaxSATResult.OPTIMUM, solver.solve(handler)); + Assert.assertEquals(solver.result(), handler.upperBoundApproximation()); + } + private void readCNF(final MaxSATSolver solver, final String fileName) throws IOException { final BufferedReader reader = new BufferedReader(new FileReader(fileName)); int hardWeight = 0; diff --git a/src/test/java/org/logicng/solvers/maxsat/encodings/EncodingsTest.java b/src/test/java/org/logicng/solvers/maxsat/encodings/EncodingsTest.java new file mode 100644 index 00000000..caac01e5 --- /dev/null +++ b/src/test/java/org/logicng/solvers/maxsat/encodings/EncodingsTest.java @@ -0,0 +1,75 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-2016 Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +package org.logicng.solvers.maxsat.encodings; + +import org.junit.Assert; +import org.junit.Test; +import org.logicng.solvers.maxsat.algorithms.MaxSATConfig; + +/** + * Unit test for the package {@link org.logicng.solvers.maxsat.encodings}. + * @version 1.1 + * @since 1.1 + */ +public class EncodingsTest { + + @Test + public void testEncoder() { + Encoder encoder = new Encoder(MaxSATConfig.CardinalityEncoding.TOTALIZER); + Assert.assertEquals("Encoder", encoder.toString()); + } + + @Test + public void testTotalizer() { + Totalizer totalizer = new Totalizer(MaxSATConfig.IncrementalStrategy.ITERATIVE); + Assert.assertEquals(MaxSATConfig.IncrementalStrategy.ITERATIVE, totalizer.incremental()); + Assert.assertEquals("Totalizer", totalizer.toString()); + } + + @Test + public void testModularTotalizer() { + ModularTotalizer mTotalizer = new ModularTotalizer(); + Assert.assertEquals(false, mTotalizer.hasCreatedEncoding()); + Assert.assertEquals("ModularTotalizer", mTotalizer.toString()); + } + + @Test + public void testSequentialWeightCounter() { + SequentialWeightCounter swc = new SequentialWeightCounter(); + Assert.assertEquals(false, swc.hasCreatedEncoding()); + Assert.assertEquals("SequentialWeightCounter", swc.toString()); + } + + @Test + public void testLadder() { + Ladder ladder = new Ladder(); + Assert.assertEquals("Ladder", ladder.toString()); + System.out.println(ladder.toString()); + } +} diff --git a/src/test/java/org/logicng/solvers/sat/AssumeTest.java b/src/test/java/org/logicng/solvers/sat/AssumeTest.java index 2d908807..3e6046ad 100644 --- a/src/test/java/org/logicng/solvers/sat/AssumeTest.java +++ b/src/test/java/org/logicng/solvers/sat/AssumeTest.java @@ -45,14 +45,14 @@ /** * Unit tests for the assume functionality of the MiniSat style SAT solvers. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class AssumeTest { private final FormulaFactory f; private final SATSolver[] solvers; - final PropositionalParser parser; + private final PropositionalParser parser; public AssumeTest() { this.f = new FormulaFactory(); @@ -89,12 +89,14 @@ public void testAssume() throws ParserException { Assert.assertEquals(TRUE, s.sat(f.variable("d"))); Assert.assertEquals(TRUE, s.sat(f.variable("e"))); Assert.assertEquals(TRUE, s.sat(f.variable("f"))); + Assert.assertEquals(TRUE, s.sat(f.variable("g"))); Assert.assertEquals(FALSE, s.sat(f.variable("a"))); Assert.assertEquals(FALSE, s.sat(f.literal("b", false))); Assert.assertEquals(FALSE, s.sat(f.literal("c", false))); Assert.assertEquals(FALSE, s.sat(f.literal("d", false))); Assert.assertEquals(FALSE, s.sat(f.literal("e", false))); Assert.assertEquals(FALSE, s.sat(f.literal("f", false))); + Assert.assertEquals(TRUE, s.sat(f.literal("g", false))); Assert.assertEquals(TRUE, s.sat(assumptions1)); Assert.assertEquals(TRUE, s.sat(assumptions2)); Assert.assertEquals(TRUE, s.sat(assumptions3)); diff --git a/src/test/java/org/logicng/solvers/sat/SATTest.java b/src/test/java/org/logicng/solvers/sat/SATTest.java index 53d10911..7fdaad7f 100644 --- a/src/test/java/org/logicng/solvers/sat/SATTest.java +++ b/src/test/java/org/logicng/solvers/sat/SATTest.java @@ -32,10 +32,12 @@ import org.junit.Test; import org.logicng.datastructures.Assignment; import org.logicng.datastructures.Tristate; +import org.logicng.formulas.CType; import org.logicng.formulas.F; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.Literal; +import org.logicng.formulas.PBConstraint; import org.logicng.formulas.Variable; import org.logicng.handlers.NumberOfModelsHandler; import org.logicng.handlers.TimeoutSATHandler; @@ -45,6 +47,7 @@ import org.logicng.solvers.CleaneLing; import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; +import org.logicng.solvers.SolverState; import java.io.BufferedReader; import java.io.File; @@ -72,6 +75,7 @@ public class SATTest { private final SATSolver[] solvers; private final PigeonHoleGenerator pg; private final PropositionalParser parser; + private final String[] testStrings; public SATTest() { this.f = new FormulaFactory(); @@ -87,6 +91,16 @@ public SATTest() { this.solvers[5] = CleaneLing.minimalistic(f); this.solvers[6] = CleaneLing.full(f, new CleaneLingConfig.Builder().plain(true).glueUpdate(true).gluered(true).build()); this.solvers[7] = CleaneLing.full(f); + + this.testStrings = new String[8]; + this.testStrings[0] = "MiniSat{result=UNDEF, incremental=true}"; + this.testStrings[1] = "MiniSat{result=UNDEF, incremental=false}"; + this.testStrings[2] = "MiniSat{result=UNDEF, incremental=false}"; + this.testStrings[3] = "MiniSat{result=UNDEF, incremental=true}"; + this.testStrings[4] = "MiniSat{result=UNDEF, incremental=false}"; + this.testStrings[5] = "CleaneLing{result=UNDEF, idx2name={}}"; + this.testStrings[6] = "CleaneLing{result=UNDEF, idx2name={}}"; + this.testStrings[7] = "CleaneLing{result=UNDEF, idx2name={}}"; } @Test @@ -95,6 +109,7 @@ public void testTrue() { s.add(F.TRUE); Assert.assertEquals(TRUE, s.sat()); Assert.assertEquals(0, s.model().size()); + Assert.assertTrue(s.toString().contains("{result=TRUE")); s.reset(); } } @@ -219,6 +234,40 @@ public void testCC1() throws InterruptedException { } } + @Test + public void testPBC() { + for (SATSolver s : this.solvers) { + List lits = new ArrayList<>(); + List coeffs = new ArrayList<>(); + for (int i = 0; i < 5; i++) { + lits.add(f.literal("x" + i, i % 2 == 0)); + coeffs.add(i + 1); + } + s.add(f.pbc(CType.GE, 10, lits, coeffs)); + Assert.assertEquals(Tristate.TRUE, s.sat()); + s.reset(); + } + } + + @Test + public void testWithRelaxation() throws ParserException { + PropositionalParser parser = new PropositionalParser(f); + Formula one = parser.parse("a & b & (c | ~d)"); + Formula two = parser.parse("~a | ~c"); + + for (SATSolver s : this.solvers) { + s.add(one); + s.addWithRelaxation(f.variable("d"), two); + Assert.assertEquals(Tristate.TRUE, s.sat()); + try { + Assert.assertEquals(2, s.enumerateAllModels().size()); + } catch (Exception e) { + Assert.assertTrue(e instanceof UnsupportedOperationException); + } + s.reset(); + } + } + @Test(expected = UnsupportedOperationException.class) public void testIllegalEnumeration() { final SATSolver s = this.solvers[7]; @@ -441,4 +490,73 @@ public void testNumberOfModelHandler() { public void testIllegalHandler() { new NumberOfModelsHandler(0); } + + @Test(expected = IllegalArgumentException.class) + public void testAddNonCCAsCC() { + MiniSat solver = MiniSat.miniSat(f); + solver.addIncrementalCC((PBConstraint) F.PBC3); + } + + @Test(expected = IllegalStateException.class) + public void testModelBeforeSolving() { + MiniSat solver = MiniSat.miniSat(f); + solver.model(); + } + + @Test(expected = IllegalArgumentException.class) + public void testCLAddNonCCAsCC() { + CleaneLing solver = CleaneLing.minimalistic(f, new CleaneLingConfig.Builder().gluered(true).build()); + solver.addIncrementalCC((PBConstraint) F.PBC3); + } + + @Test(expected = IllegalStateException.class) + public void testCLModelBeforeSolving() { + CleaneLing solver = CleaneLing.minimalistic(f); + solver.model(); + } + + @Test(expected = UnsupportedOperationException.class) + public void testCLSatWithLit() { + CleaneLing solver = CleaneLing.minimalistic(f); + solver.add(F.AND1); + solver.sat(new TimeoutSATHandler(10000), F.A); + } + + @Test(expected = UnsupportedOperationException.class) + public void testCLSaveState() { + CleaneLing solver = CleaneLing.minimalistic(f); + solver.add(F.AND1); + solver.saveState(); + } + + @Test(expected = UnsupportedOperationException.class) + public void testCLLoadState() { + CleaneLing solver = CleaneLing.minimalistic(f); + solver.add(F.AND1); + solver.loadState(new SolverState(27, new int[3])); + } + + @Test(expected = UnsupportedOperationException.class) + public void testCLSatWithLitCollection() { + CleaneLing solver = CleaneLing.minimalistic(f); + solver.add(F.AND1); + List lits = new ArrayList<>(); + lits.add(F.A); + lits.add(F.B); + solver.sat(new TimeoutSATHandler(10000), lits); + } + + @Test(expected = UnsupportedOperationException.class) + public void testCLEnumerateWithWrongConfig() { + CleaneLing solver = CleaneLing.full(f, new CleaneLingConfig.Builder().plain(false).build()); + solver.add(F.AND1); + solver.enumerateAllModels(); + } + + @Test + public void testToString() { + for (int i = 0; i < this.solvers.length; i++) { + Assert.assertEquals(this.testStrings[i], this.solvers[i].toString()); + } + } } diff --git a/src/test/java/org/logicng/transformations/AIGTest.java b/src/test/java/org/logicng/transformations/AIGTest.java index ea60ebb2..6b23c8a0 100644 --- a/src/test/java/org/logicng/transformations/AIGTest.java +++ b/src/test/java/org/logicng/transformations/AIGTest.java @@ -31,6 +31,8 @@ import org.junit.Assert; import org.junit.Test; import org.logicng.formulas.F; +import org.logicng.formulas.Formula; +import org.logicng.formulas.cache.TransformationCacheEntry; import org.logicng.io.parsers.ParserException; import org.logicng.io.parsers.PropositionalParser; import org.logicng.predicates.AIGPredicate; @@ -38,7 +40,7 @@ /** * Unit Tests for AIG conversion. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class AIGTest { @@ -80,6 +82,14 @@ public void testBinaryOperators() throws ParserException { Assert.assertFalse(F.IMP3.holds(aigPred)); Assert.assertFalse(F.EQ1.holds(aigPred)); Assert.assertFalse(F.EQ2.holds(aigPred)); + Formula impl = p.parse("m => n"); + impl.transform(aigTrans, false); + Formula aigIMPL = impl.transformationCacheEntry(TransformationCacheEntry.AIG); + Assert.assertNull(aigIMPL); + Formula equi = p.parse("m <=> n"); + equi.transform(aigTrans, false); + Formula aigEQUI = impl.transformationCacheEntry(TransformationCacheEntry.AIG); + Assert.assertNull(aigEQUI); } @Test @@ -100,6 +110,14 @@ public void testNAryOperators() throws ParserException { Assert.assertFalse(p.parse("~(a | b) & c & ~(x & ~y) & (w => z)").holds(aigPred)); Assert.assertFalse(p.parse("~(a & b) | c | ~(x | ~y)").holds(aigPred)); Assert.assertFalse(p.parse("a | b | (~x & ~y)").holds(aigPred)); + Formula or = p.parse("m | n | o"); + or.transform(aigTrans, false); + Formula aigOR = or.transformationCacheEntry(TransformationCacheEntry.AIG); + Assert.assertNull(aigOR); + Formula and = p.parse("m & n & o"); + and.transform(aigTrans, false); + Formula aigAND = and.transformationCacheEntry(TransformationCacheEntry.AIG); + Assert.assertNull(aigAND); } @Test @@ -114,5 +132,20 @@ public void testNot() throws ParserException { Assert.assertEquals(p.parse("~(a & b & ~x & ~y)"), p.parse("~(a & b & ~x & ~y)").transform(aigTrans)); Assert.assertEquals(p.parse("~a & ~b & x & y"), p.parse("~(a | b | ~x | ~y)").transform(aigTrans)); Assert.assertEquals(p.parse("~a & ~b & x & y"), p.parse("~(a | b | ~x | ~y)").transform(aigTrans)); // test caching + Formula not = p.parse("~(m | n)"); + not.transform(aigTrans, false); + Formula aig = not.transformationCacheEntry(TransformationCacheEntry.AIG); + Assert.assertNull(aig); + } + + @Test + public void testPBC() { + Assert.assertTrue(F.PBC1.transform(aigTrans).holds(aigPred)); + } + + @Test + public void testToString() { + Assert.assertEquals("AIGTransformation", aigTrans.toString()); + Assert.assertEquals("AIGPredicate", aigPred.toString()); } } diff --git a/src/test/java/org/logicng/transformations/cnf/CNFEncoderTest.java b/src/test/java/org/logicng/transformations/cnf/CNFEncoderTest.java index 3f36ea0f..3b9303b9 100644 --- a/src/test/java/org/logicng/transformations/cnf/CNFEncoderTest.java +++ b/src/test/java/org/logicng/transformations/cnf/CNFEncoderTest.java @@ -154,4 +154,38 @@ public void testAdvancedEncoder() throws ParserException { Assert.assertEquals(p.parse("(z1 | z2) & z3 & z4 & (~@RESERVED_CNF_2 | z1) & (~@RESERVED_CNF_2 | z5) & (~@RESERVED_CNF_2 | ~z6) & (~@RESERVED_CNF_2 | ~z7) & (@RESERVED_CNF_2 | ~z1 | ~z5 | z6 | z7) & (@RESERVED_CNF_2 | z8 | z9)"), encoder3.encode(phi3)); } + @Test + public void testStrings() { + String expected = "CNFConfig{\n" + + "algorithm=TSEITIN\n" + + "fallbackAlgorithmForAdvancedEncoding=PLAISTED_GREENBAUM\n" + + "distributedBoundary=-1\n" + + "createdClauseBoundary=1000\n" + + "atomBoundary=12\n" + + "}\n"; + FormulaFactory f = new FormulaFactory(); + CNFConfig config = new CNFConfig.Builder().algorithm(CNFConfig.Algorithm.TSEITIN).fallbackAlgorithmForAdvancedEncoding(CNFConfig.Algorithm.PLAISTED_GREENBAUM).build(); + CNFEncoder encoder = new CNFEncoder(f, config); + Assert.assertEquals(expected, config.toString()); + Assert.assertEquals(expected, encoder.toString()); + Assert.assertEquals(CNFConfig.Algorithm.TSEITIN, CNFConfig.Algorithm.valueOf("TSEITIN")); + } + + @Test + public void testBugIssueNo4() throws ParserException { + final FormulaFactory f = new FormulaFactory(); + final PropositionalParser parser = new PropositionalParser(f); + final Formula f1 = parser.parse("(x10 & x9 & x3 & x12 | x10 & x9 & x8 | x9 & x8 & x12) & ~x5 & ~x7 & x1 | (x10 & x9 & x3 & x12 | x10 & x9 & x8 | x9 & x8 & x12) & ~(x11 & x3) & ~(x11 & x8) & ~x5 & ~x7 & x0"); + final Formula f2 = parser.parse("x1 & x3 & x4"); + final Formula f3 = parser.parse("(x10 & x9 & x3 & x12 | x10 & x9 & x8 | x9 & x8 & x12) & ~(x11 & x3) & ~(x11 & x8 & x12) & ~x5 & ~x7 & x1 | (x10 & x9 & x3 & x12 | x10 & x9 & x8 | x9 & x8 & x12) & ~(x11 & x3) & ~(x11 & x8) & ~x5 & ~x7 & x0 | x3 & x4 & ~x5 & ~x7 & x1 | x3 & x4 & ~x5 & ~x7 & x0 | x2 & x6 & ~x5 & ~x7 & x0"); + final Formula f4 = parser.parse("(x1 & x3 & x4 | x0 & (x2 & x6 | x3 & x4) | x9 & (x1 & x10 & x8 & ~x12 & x3 | (x1 | x0) & (x12 & (x10 & x3 | x8) | x10 & x8) & ~x11)) & ~x5 & ~x7"); + Assert.assertNotEquals(null, f.not(f.equivalence(f1, f2)).cnf()); + Assert.assertNotEquals(null, f.not(f.equivalence(f3, f4)).cnf()); + } + + @Test(expected = IllegalArgumentException.class) + public void testWrongFallbackForConfig() { + new CNFConfig.Builder().fallbackAlgorithmForAdvancedEncoding(CNFConfig.Algorithm.FACTORIZATION).build(); + } + } diff --git a/src/test/java/org/logicng/transformations/cnf/CNFTest.java b/src/test/java/org/logicng/transformations/cnf/CNFTest.java index 7865942c..52629f04 100644 --- a/src/test/java/org/logicng/transformations/cnf/CNFTest.java +++ b/src/test/java/org/logicng/transformations/cnf/CNFTest.java @@ -127,6 +127,11 @@ public void testCC() throws ParserException { Assert.assertEquals(p.parse("(d | @RESERVED_CC_1 | @RESERVED_CC_4) & (~@RESERVED_CC_3 | @RESERVED_CC_1 | @RESERVED_CC_4) & (~@RESERVED_CC_3 | d | @RESERVED_CC_4) & (~@RESERVED_CC_4 | @RESERVED_CC_0) & (~@RESERVED_CC_2 | @RESERVED_CC_0) & (~@RESERVED_CC_4 | ~@RESERVED_CC_2) & (c | @RESERVED_CC_3 | @RESERVED_CC_5) & (b | @RESERVED_CC_3 | @RESERVED_CC_5) & (b | c | @RESERVED_CC_5) & (~@RESERVED_CC_5 | @RESERVED_CC_2) & ~@RESERVED_CC_0"), p.parse("~(1 * b + 1 * c + 1 * d <= 1)").cnf()); } + @Test + public void testToString() { + Assert.assertEquals("CNFFactorization", cnf.toString()); + } + private static class TestFactorizationHandler implements FactorizationHandler { private int distCount = 0; @@ -145,17 +150,5 @@ public boolean createdClause(final Formula clause) { longestClause = Math.max(clause.numberOfAtoms(), longestClause); return true; } - - private int distCount() { - return this.distCount; - } - - private int clauseCount() { - return this.clauseCount; - } - - private long longestClause() { - return this.longestClause; - } } } diff --git a/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTest.java b/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTest.java index de944ad4..c9117cc2 100644 --- a/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTest.java +++ b/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTest.java @@ -203,6 +203,11 @@ public void testFactorization() throws ParserException { Assert.assertEquals(f4.variables().size(), f4.transform(pgf).variables().size()); } + @Test + public void testToString() { + Assert.assertEquals("PlaistedGreenbaumTransformation{boundary=0}", pg.toString()); + } + private boolean equivalentModels(final Formula f1, final Formula f2, final SortedSet vars) { final SATSolver s = MiniSat.miniSat(f1.factory()); s.add(f1); diff --git a/src/test/java/org/logicng/transformations/cnf/TseitinTest.java b/src/test/java/org/logicng/transformations/cnf/TseitinTest.java index 3773f660..ea7bf02c 100644 --- a/src/test/java/org/logicng/transformations/cnf/TseitinTest.java +++ b/src/test/java/org/logicng/transformations/cnf/TseitinTest.java @@ -152,6 +152,11 @@ public void testCC() throws ParserException { Assert.assertEquals(p.parse("(d | @RESERVED_CC_1 | @RESERVED_CC_4) & (~@RESERVED_CC_3 | @RESERVED_CC_1 | @RESERVED_CC_4) & (~@RESERVED_CC_3 | d | @RESERVED_CC_4) & (~@RESERVED_CC_4 | @RESERVED_CC_0) & (~@RESERVED_CC_2 | @RESERVED_CC_0) & (~@RESERVED_CC_4 | ~@RESERVED_CC_2) & (c | @RESERVED_CC_3 | @RESERVED_CC_5) & (b | @RESERVED_CC_3 | @RESERVED_CC_5) & (b | c | @RESERVED_CC_5) & (~@RESERVED_CC_5 | @RESERVED_CC_2) & ~@RESERVED_CC_0"), p.parse("~(1 * b + 1 * c + 1 * d <= 1)").transform(ts)); } + @Test + public void testToString() { + Assert.assertEquals("TseitinTransformation{boundary=0}", ts.toString()); + } + private boolean equivalentModels(final Formula f1, final Formula f2, final SortedSet vars) { final SATSolver s = MiniSat.miniSat(f1.factory()); s.add(f1); diff --git a/src/test/java/org/logicng/transformations/dnf/DNFTest.java b/src/test/java/org/logicng/transformations/dnf/DNFTest.java index 30d8757a..92342f39 100644 --- a/src/test/java/org/logicng/transformations/dnf/DNFTest.java +++ b/src/test/java/org/logicng/transformations/dnf/DNFTest.java @@ -32,6 +32,7 @@ import org.junit.Test; import org.logicng.formulas.F; import org.logicng.formulas.Formula; +import org.logicng.handlers.FactorizationHandler; import org.logicng.io.parsers.ParserException; import org.logicng.io.parsers.PropositionalParser; import org.logicng.predicates.CNFPredicate; @@ -39,7 +40,7 @@ /** * Unit Tests for DNF conversion. - * @version 1.0 + * @version 1.1 * @since 1.0 */ public class DNFTest { @@ -116,4 +117,33 @@ public void testCDNF() throws ParserException { Assert.assertEquals(cdnf, f.transform(new CanonicalDNFEnumeration())); Assert.assertEquals(F.f.falsum(), F.f.and(F.A, F.NA).transform(new CanonicalDNFEnumeration())); } + + @Test + public void testWithHandler() throws ParserException { + PropositionalParser p = new PropositionalParser(F.f); + Formula formula = p.parse("(~(~(a | b) => ~(x | y))) & ((a | x) => ~(b | y))"); + DNFFactorization factorization = new DNFFactorization(new FactorizationHandler() { + private int dists = 0; + private int clauses = 0; + + @Override + public boolean performedDistribution() { + dists++; + return dists < 100; + } + + @Override + public boolean createdClause(Formula clause) { + clauses++; + return clauses < 5; + } + }); + Assert.assertNull(factorization.apply(formula, false)); + } + + @Test + public void testToString() { + Assert.assertEquals("DNFFactorization", dnfFactorization.toString()); + Assert.assertEquals("CanonicalDNFEnumeration", new CanonicalDNFEnumeration().toString()); + } } diff --git a/tests/writers/formulas-dot/f6_f.dot b/tests/writers/formulas-dot/f6_f.dot new file mode 100644 index 00000000..236179f0 --- /dev/null +++ b/tests/writers/formulas-dot/f6_f.dot @@ -0,0 +1,16 @@ +digraph G { + id0 [shape=box, label="a"]; + id1 [shape=box, label="b"]; + id2 [shape=box, label="c"]; + id3 [label="∧"]; + id3 -> id0; + id3 -> id1; + id4 [label="¬"]; + id4 -> id3; + id5 [label="∧"]; + id5 -> id2; + id5 -> id4; + id6 [label="∨"]; + id6 -> id3; + id6 -> id5; +} diff --git a/tests/writers/formulas-dot/f6_t.dot b/tests/writers/formulas-dot/f6_t.dot new file mode 100644 index 00000000..1aad863b --- /dev/null +++ b/tests/writers/formulas-dot/f6_t.dot @@ -0,0 +1,18 @@ +digraph G { +{ rank = same; + id0 [shape=box, label="a"]; + id1 [shape=box, label="b"]; + id2 [shape=box, label="c"]; +} + id3 [label="∧"]; + id3 -> id0; + id3 -> id1; + id4 [label="¬"]; + id4 -> id3; + id5 [label="∧"]; + id5 -> id2; + id5 -> id4; + id6 [label="∨"]; + id6 -> id3; + id6 -> id5; +} diff --git a/tests/writers/formulas-dot/f7_f.dot b/tests/writers/formulas-dot/f7_f.dot new file mode 100644 index 00000000..ab798e92 --- /dev/null +++ b/tests/writers/formulas-dot/f7_f.dot @@ -0,0 +1,19 @@ +digraph G { + id0 [shape=box, label="a"]; + id1 [shape=box, label="b"]; + id2 [shape=box, label="c"]; + id3 [shape=box, label="d"]; + id4 [label="∧"]; + id4 -> id2; + id4 -> id3; + id5 [label="∧"]; + id5 -> id0; + id5 -> id1; + id6 [label="⇔"]; + id6 -> id4 [label="l"]; + id6 -> id5 [label="r"]; + id7 [label="∨"]; + id7 -> id4; + id7 -> id5; + id7 -> id6; +} diff --git a/tests/writers/formulas-dot/f7_t.dot b/tests/writers/formulas-dot/f7_t.dot new file mode 100644 index 00000000..0ea5f88b --- /dev/null +++ b/tests/writers/formulas-dot/f7_t.dot @@ -0,0 +1,21 @@ +digraph G { +{ rank = same; + id0 [shape=box, label="a"]; + id1 [shape=box, label="b"]; + id2 [shape=box, label="c"]; + id3 [shape=box, label="d"]; +} + id4 [label="∧"]; + id4 -> id2; + id4 -> id3; + id5 [label="∧"]; + id5 -> id0; + id5 -> id1; + id6 [label="⇔"]; + id6 -> id4 [label="l"]; + id6 -> id5 [label="r"]; + id7 [label="∨"]; + id7 -> id4; + id7 -> id5; + id7 -> id6; +}