diff --git a/pom.xml b/pom.xml index 4b12f96c..088c09cb 100644 --- a/pom.xml +++ b/pom.xml @@ -3,7 +3,7 @@ + xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 https://maven.apache.org/maven-v4_0_0.xsd"> 4.0.0 com.booleworks logicng-core @@ -12,7 +12,7 @@ LogicNG The Next Generation Logic Library - http://www.logicng.org + https://www.logicng.org @@ -48,13 +48,12 @@ 11 - 4.13.1 5.10.1 3.24.2 5.2.0 - 4.13.1 + 3.0.1 0.8.11 4.3.0 3.13.0 @@ -80,19 +79,16 @@ - + - org.antlr - antlr4-maven-plugin - ${version.antlr-plugin} - - src/main/antlr - target/generated-sources/antlr/com/booleworks/logicng/io/parsers - + org.codehaus.mojo + javacc-maven-plugin + ${version.javacc} + javacc - antlr4 + javacc @@ -234,7 +230,7 @@ ${version.coveralls} - target/generated-sources/antlr + target/generated-sources/parser @@ -255,13 +251,6 @@ - - - org.antlr - antlr4-runtime - ${version.antlr} - - org.junit.jupiter diff --git a/src/main/antlr/LogicNGPropositional.g4 b/src/main/antlr/LogicNGPropositional.g4 deleted file mode 100644 index bf5fa1b5..00000000 --- a/src/main/antlr/LogicNGPropositional.g4 +++ /dev/null @@ -1,95 +0,0 @@ -// SPDX-License-Identifier: Apache-2.0 and MIT -// Copyright 2015-2023 Christoph Zengler -// Copyright 2023-20xx BooleWorks GmbH - -grammar LogicNGPropositional; - -options { - superClass = ParserWithFormula; -} - -@header { - package com.booleworks.logicng.io.parsers; - - import java.util.LinkedHashSet; - import com.booleworks.logicng.formulas.*; -} - -@parser::members { - public Formula getParsedFormula() { - return formula().f; - } -} - -formula returns [Formula f] - : EOF {$f = f.verum();} - | equiv EOF {$f = $equiv.f;}; - -constant returns [Formula f] - : TRUE {$f = f.verum();} - | FALSE {$f = f.falsum();}; - -comparison returns [Formula f] - : e = add EQ n = NUMBER {$f = f.pbc(CType.EQ, Integer.parseInt($n.text), $e.literals, $e.coeffs);} - | e = add LE n = NUMBER {$f = f.pbc(CType.LE, Integer.parseInt($n.text), $e.literals, $e.coeffs);} - | e = add LT n = NUMBER {$f = f.pbc(CType.LT, Integer.parseInt($n.text), $e.literals, $e.coeffs);} - | e = add GE n = NUMBER {$f = f.pbc(CType.GE, Integer.parseInt($n.text), $e.literals, $e.coeffs);} - | e = add GT n = NUMBER {$f = f.pbc(CType.GT, Integer.parseInt($n.text), $e.literals, $e.coeffs);}; - -simp returns [Formula f] - : NUMBER {$f = ($NUMBER.text.startsWith("~") ? f.literal($NUMBER.text.substring(1, $NUMBER.text.length()), false) : f.literal($NUMBER.text, true));} - | LITERAL {$f = ($LITERAL.text.startsWith("~") ? f.literal($LITERAL.text.substring(1, $LITERAL.text.length()), false) : f.literal($LITERAL.text, true));} - | constant {$f = $constant.f;} - | comparison {$f = $comparison.f;} - | LBR equiv RBR {$f = $equiv.f;}; - -lit returns [Formula f] - : NOT a = lit {$f = f.not($a.f);} - | simp {$f = $simp.f;}; - -conj returns [Formula f] -@init{LinkedHashSet literals = new LinkedHashSet<>(); } - : a = lit {literals.add($a.f);} (AND b = lit {literals.add($b.f);})* {$f = f.and(literals);}; - -disj returns [Formula f] -@init{LinkedHashSet conjunctions = new LinkedHashSet<>();} - : a = conj {conjunctions.add($a.f);} (OR b = conj {conjunctions.add($b.f);})* {$f = f.or(conjunctions);}; - -impl returns [Formula f] -@init{Formula[] operands = new Formula[2];} - : a = disj {operands[0] =$a.f;} (IMPL b = impl {operands[1] = $b.f;})? {$f = operands[1] == null ? operands[0] : f.implication(operands[0], operands[1]);}; - -equiv returns [Formula f] -@init{Formula[] operands = new Formula[2];} - : a = impl {operands[0] =$a.f;} (EQUIV b = equiv {operands[1] = $b.f;})? {$f = operands[1] == null ? operands[0] : f.equivalence(operands[0], operands[1]);}; - -mul returns [Literal l, int c] - : LITERAL {$l = ($LITERAL.text.startsWith("~") ? f.literal($LITERAL.text.substring(1, $LITERAL.text.length()), false) : f.literal($LITERAL.text, true)); $c = 1;} - | NUMBER {$l = f.literal($NUMBER.text, true); $c = 1;} - | NUMBER MUL LITERAL {$l = ($LITERAL.text.startsWith("~") ? f.literal($LITERAL.text.substring(1, $LITERAL.text.length()), false) : f.literal($LITERAL.text, true)); $c = Integer.parseInt($NUMBER.text);} - | num = NUMBER MUL lt = NUMBER {$l = f.literal($lt.text, true); $c = Integer.parseInt($num.text);}; - -add returns [List literals, List coeffs] -@init{$literals = new ArrayList<>(); $coeffs = new ArrayList<>();} - : m1 = mul {$literals.add($m1.l); $coeffs.add($m1.c);} (ADD m2 = mul {$literals.add($m2.l); $coeffs.add($ADD.text.equals("+") ? $m2.c : -$m2.c);})*; - - -NUMBER : [\-]?[0-9]+; -LITERAL : [~]?[A-Za-z0-9_@#][A-Za-z0-9_#]*; -TRUE : '$true'; -FALSE : '$false'; -LBR : '('; -RBR : ')'; -NOT : '~'; -AND : '&'; -OR : '|'; -IMPL : '=>'; -EQUIV : '<=>'; -MUL : '*'; -ADD : [+-]; -EQ : '='; -LE : '<='; -LT : '<'; -GE : '>='; -GT : '>'; -WS : [ \t\r\n]+ -> skip; diff --git a/src/main/java/com/booleworks/logicng/datastructures/ubtrees/UBTree.java b/src/main/java/com/booleworks/logicng/datastructures/ubtrees/UBTree.java index 76aaf03e..2a21f443 100644 --- a/src/main/java/com/booleworks/logicng/datastructures/ubtrees/UBTree.java +++ b/src/main/java/com/booleworks/logicng/datastructures/ubtrees/UBTree.java @@ -17,7 +17,7 @@ * A data structure for storing sets with efficient sub- and superset queries. * C.f. `A New Method to Index and Query Sets`, Hoffmann and Koehler, 1999 * @param the type of the elements (must be comparable) - * @version 2.0.0 + * @version 3.0.0 * @since 1.5.0 */ public final class UBTree> { @@ -38,11 +38,7 @@ public void addSet(final SortedSet set) { SortedMap> nodes = rootNodes; UBNode node = null; for (final T element : set) { - node = nodes.get(element); - if (node == null) { - node = new UBNode<>(element); - nodes.put(element, node); - } + node = nodes.computeIfAbsent(element, UBNode::new); nodes = node.children(); } if (node != null) { @@ -54,7 +50,7 @@ public void addSet(final SortedSet set) { * Returns the first subset of a given set in this UBTree. * @param set the set to search for * @return the first subset which is found for the given set or {@code null} - * if there is none + * if there is none */ public SortedSet firstSubset(final SortedSet set) { if (rootNodes.isEmpty() || set == null || set.isEmpty()) { @@ -138,7 +134,7 @@ private void allSubsets(final SortedSet set, final SortedMap> fo private void allSupersets(final SortedSet set, final SortedMap> forest, final Set> supersets) { - final Set> nodes = getAllNodesContainingElementsLessThan(set, forest, set.first()); + final Set> nodes = getAllNodesContainingElementsLessThan(forest, set.first()); for (final UBNode node : nodes) { allSupersets(set, node.children(), supersets); } @@ -172,8 +168,7 @@ private Set> getAllNodesContainingElements(final SortedSet set, fin return nodes; } - private Set> getAllNodesContainingElementsLessThan(final SortedSet set, - final SortedMap> forest, + private Set> getAllNodesContainingElementsLessThan(final SortedMap> forest, final T element) { final Set> nodes = new LinkedHashSet<>(); for (final UBNode node : forest.values()) { diff --git a/src/main/java/com/booleworks/logicng/explanations/drup/DRUPTrim.java b/src/main/java/com/booleworks/logicng/explanations/drup/DRUPTrim.java index 674c249a..8230368a 100644 --- a/src/main/java/com/booleworks/logicng/explanations/drup/DRUPTrim.java +++ b/src/main/java/com/booleworks/logicng/explanations/drup/DRUPTrim.java @@ -72,7 +72,7 @@ private static int index(final int lit) { * @param originalProblem the clauses of the original problem * @param proof the clauses of the proof * @return the result of the DRUP execution from which the UNSAT core can be - * generated + * generated */ public DRUPResult compute(final LNGVector originalProblem, final LNGVector proof) { final DRUPResult result = new DRUPResult(); @@ -95,8 +95,6 @@ private static class Solver { private final LNGVector core; private final boolean delete; private LNGIntVector DB; - private int nVars; - private int nClauses; private int[] falseStack; private int[] reason; private int[] internalFalse; @@ -108,7 +106,6 @@ private static class Solver { private int count; private int adlemmas; private int lemmas; - private int time; private Solver(final LNGVector originalProblem, final LNGVector proof) { this.originalProblem = originalProblem; @@ -300,10 +297,10 @@ int matchClause(final LNGIntVector clauselist, final int[] _marks, final int mar * Parses the input and returns {@code true} if further processing is * required and {@code false} if the formula is trivially UNSAT. * @return {@code true} if further processing is required and - * {@code false} if the formula is trivially UNSAT + * {@code false} if the formula is trivially UNSAT */ private boolean parse() { - nVars = 0; + int nVars = 0; for (final LNGIntVector vector : originalProblem) { for (int i = 0; i < vector.size(); i++) { if (Math.abs(vector.get(i)) > nVars) { @@ -311,7 +308,7 @@ private boolean parse() { } } } - nClauses = originalProblem.size(); + final int nClauses = originalProblem.size(); boolean del = false; int nZeros = nClauses; @@ -426,7 +423,7 @@ private LNGVector verify() { final int endPtr = lemmas; int checked = adlemmas; final LNGIntVector buffer = new LNGIntVector(); - time = DB.get(lemmasPtr - 1); + int time; boolean gotoPostProcess = false; if (processedPtr < assignedPtr) { diff --git a/src/main/java/com/booleworks/logicng/formulas/FormulaFactory.java b/src/main/java/com/booleworks/logicng/formulas/FormulaFactory.java index 14d68a89..843ea520 100644 --- a/src/main/java/com/booleworks/logicng/formulas/FormulaFactory.java +++ b/src/main/java/com/booleworks/logicng/formulas/FormulaFactory.java @@ -12,7 +12,9 @@ import com.booleworks.logicng.formulas.implementation.noncaching.NonCachingFormulaFactory; import com.booleworks.logicng.formulas.printer.FormulaStringRepresentation; import com.booleworks.logicng.functions.SubNodeFunction; +import com.booleworks.logicng.io.parsers.FormulaParser; import com.booleworks.logicng.io.parsers.ParserException; +import com.booleworks.logicng.io.parsers.PropositionalParser; import com.booleworks.logicng.solvers.functions.modelenumeration.ModelEnumerationConfig; import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATConfig; import com.booleworks.logicng.solvers.sat.SATSolverConfig; @@ -49,6 +51,7 @@ */ public abstract class FormulaFactory { + protected FormulaParser parser; protected final String name; protected final FormulaStringRepresentation stringRepresentation; protected final FormulaFactoryConfig.FormulaMergeStrategy formulaMergeStrategy; @@ -93,7 +96,8 @@ protected FormulaFactory(final FormulaFactoryConfig config) { auxVarCounters = new ConcurrentHashMap<>(); clear(); subformulaFunction = new SubNodeFunction(this); - auxVarPrefix = "@AUX_" + this.name + "_"; + auxVarPrefix = "@AUX_" + name + "_"; + parser = new PropositionalParser(this); readOnly = false; } @@ -723,7 +727,7 @@ private Formula constructCCUnsafe(final CType comparator, final int rhs, * @param coefficients the coefficients or {@code null} if there are no * coefficients to test * @return {@code true} if the given pseudo-Boolean constraint is a - * cardinality constraint, otherwise {@code false} + * cardinality constraint, otherwise {@code false} */ private static boolean isCC(final CType comparator, final int rhs, final Collection literals, final List coefficients) { @@ -752,7 +756,7 @@ private static boolean isCC(final CType comparator, final int rhs, final Collect * @param comparator the comparator * @param rhs the right-hand side * @return {@code true} if the trivial case is a tautology, {@code false} if - * the trivial case is a contradiction + * the trivial case is a contradiction */ private static boolean evaluateTrivialPBConstraint(final CType comparator, final int rhs) { switch (comparator) { @@ -909,13 +913,28 @@ public long numberOfNodes(final Formula formula) { return formula.apply(subformulaFunction).size(); } + /** + * Sets a formula parser for this factory. By default, this will be the + * included JavaCC-based formula parser. But you could replace with an + * ANTLR-based parser or your application-specific parser. + * @param parser the formula parser + */ + public void setParser(final FormulaParser parser) { + this.parser = parser; + } + /** * Parses a given string to a formula using a pseudo boolean parser. * @param string a string representing the formula * @return the formula * @throws ParserException if the parser throws an exception */ - public abstract Formula parse(final String string) throws ParserException; + public Formula parse(final String string) throws ParserException { + if (readOnly) { + throwReadOnlyException(); + } + return parser.parse(string); + } /** * Adds a given formula to a list of operands. If the formula is the neutral @@ -966,7 +985,7 @@ private byte addFormulaAnd(final LinkedHashSet ops, final Formula formu * @param formulas the list of formulas * @param formula the formula * @return {@code true} if a given list of formulas contains a given - * formula, {@code false} otherwise + * formula, {@code false} otherwise */ private boolean containsComplement(final LinkedHashSet formulas, final Formula formula) { if (!simplifyComplementaryOperands) { @@ -981,7 +1000,7 @@ private boolean containsComplement(final LinkedHashSet formulas, final * otherwise {@code null} is returned. * @param formula the formula * @return the negated formula if the negation exists in the cache, - * otherwise {@code null} + * otherwise {@code null} */ protected abstract Formula negateOrNull(final Formula formula); diff --git a/src/main/java/com/booleworks/logicng/formulas/implementation/cached/CachingFormulaFactory.java b/src/main/java/com/booleworks/logicng/formulas/implementation/cached/CachingFormulaFactory.java index 95836353..c5539d47 100644 --- a/src/main/java/com/booleworks/logicng/formulas/implementation/cached/CachingFormulaFactory.java +++ b/src/main/java/com/booleworks/logicng/formulas/implementation/cached/CachingFormulaFactory.java @@ -23,8 +23,6 @@ import com.booleworks.logicng.formulas.PBConstraint; import com.booleworks.logicng.formulas.Variable; import com.booleworks.logicng.formulas.cache.CacheEntry; -import com.booleworks.logicng.io.parsers.ParserException; -import com.booleworks.logicng.io.parsers.PropositionalParser; import com.booleworks.logicng.util.Pair; import java.util.HashMap; @@ -35,7 +33,6 @@ public class CachingFormulaFactory extends FormulaFactory { - private final PropositionalParser parser; Map posLiterals; Map negLiterals; Map nots; @@ -71,7 +68,6 @@ public CachingFormulaFactory(final FormulaFactoryConfig config) { super(config); cFalse = new LngCachedFalse(this); cTrue = new LngCachedTrue(this); - parser = new PropositionalParser(this); clear(); } @@ -438,14 +434,6 @@ public void clear() { pbEncodingCache = new HashMap<>(); } - @Override - public Formula parse(final String string) throws ParserException { - if (readOnly) { - throwReadOnlyException(); - } - return parser.parse(string); - } - /** * Returns the statistics for this formula factory. * @return the statistics for this formula factory @@ -731,7 +719,7 @@ public int ccs() { * Returns the number of generated cardinality constraint auxiliary * variables. * @return the number of generated cardinality constraint auxiliary - * variables + * variables */ public int ccCounter() { return ccCounter; diff --git a/src/main/java/com/booleworks/logicng/formulas/implementation/noncaching/NonCachingFormulaFactory.java b/src/main/java/com/booleworks/logicng/formulas/implementation/noncaching/NonCachingFormulaFactory.java index 35e1ef1d..4d28fb74 100644 --- a/src/main/java/com/booleworks/logicng/formulas/implementation/noncaching/NonCachingFormulaFactory.java +++ b/src/main/java/com/booleworks/logicng/formulas/implementation/noncaching/NonCachingFormulaFactory.java @@ -10,8 +10,6 @@ import com.booleworks.logicng.formulas.FormulaFactoryConfig; import com.booleworks.logicng.formulas.Literal; import com.booleworks.logicng.formulas.Variable; -import com.booleworks.logicng.io.parsers.ParserException; -import com.booleworks.logicng.io.parsers.PropositionalParser; import java.util.HashMap; import java.util.LinkedHashSet; @@ -161,14 +159,6 @@ protected Formula negateOrNull(final Formula formula) { return formula.negate(this); } - @Override - public Formula parse(final String string) throws ParserException { - if (readOnly) { - throwReadOnlyException(); - } - return new PropositionalParser(this).parse(string); - } - @Override public void clear() { super.clear(); diff --git a/src/main/java/com/booleworks/logicng/formulas/printer/SortedStringRepresentation.java b/src/main/java/com/booleworks/logicng/formulas/printer/SortedStringRepresentation.java index 95bbcda5..4be252f9 100644 --- a/src/main/java/com/booleworks/logicng/formulas/printer/SortedStringRepresentation.java +++ b/src/main/java/com/booleworks/logicng/formulas/printer/SortedStringRepresentation.java @@ -93,7 +93,7 @@ public SortedStringRepresentation(final FormulaFactory f, final List v * Returns the sorted string representation of the given formula. * @param formula the formula * @return the sorted string representation of the formula with regard to - * the variable ordering + * the variable ordering */ @Override public String toInnerString(final Formula formula) { @@ -194,7 +194,7 @@ protected String pbLhs(final List operands, final List coeffic sb.append(sortedOperands.get(i)).append(add); } } - if (sortedOperands.size() > 0) { + if (!sortedOperands.isEmpty()) { if (sortedCoefficients.get(sortedOperands.size() - 1) != 1) { sb.append(sortedCoefficients.get(sortedOperands.size() - 1)).append(mul) .append(sortedOperands.get(sortedOperands.size() - 1)); @@ -243,12 +243,12 @@ static class FormulaComparator implements Comparator { * @param formula1 the first formula * @param formula2 the second formula * @return -1 iff formula1 < formula2 (when for the first time a - * variable of the ordering appears in formula1 but not - * formula2) 0 iff formula1 = formula2 (when all variables of - * the ordering appear (or not appear) in both formula1 and - * formula2) 1 iff formula1 > formula2 (when for the first - * time a variable of the ordering appears in formula2 but not - * formula1) + * variable of the ordering appears in formula1 but not + * formula2) 0 iff formula1 = formula2 (when all variables of + * the ordering appear (or not appear) in both formula1 and + * formula2) 1 iff formula1 > formula2 (when for the first + * time a variable of the ordering appears in formula2 but not + * formula1) */ @Override public int compare(final Formula formula1, final Formula formula2) { diff --git a/src/main/java/com/booleworks/logicng/handlers/TimeoutHandler.java b/src/main/java/com/booleworks/logicng/handlers/TimeoutHandler.java index a43870da..242592c8 100644 --- a/src/main/java/com/booleworks/logicng/handlers/TimeoutHandler.java +++ b/src/main/java/com/booleworks/logicng/handlers/TimeoutHandler.java @@ -14,7 +14,7 @@ */ public class TimeoutHandler implements ComputationHandler { - protected long timeout; + protected final long timeout; protected final TimerType type; protected long designatedEnd; @@ -69,7 +69,7 @@ public boolean shouldResume(final LNGEvent event) { /** * Tests if the current time exceeds the timeout limit. * @return {@code true} if the current time exceeds the timeout limit, - * otherwise {@code false} + * otherwise {@code false} */ private boolean timeLimitExceeded() { return designatedEnd > 0 && System.currentTimeMillis() >= designatedEnd; diff --git a/src/main/java/com/booleworks/logicng/io/graphical/GraphicalNode.java b/src/main/java/com/booleworks/logicng/io/graphical/GraphicalNode.java index 5b288bd9..8c493ee4 100644 --- a/src/main/java/com/booleworks/logicng/io/graphical/GraphicalNode.java +++ b/src/main/java/com/booleworks/logicng/io/graphical/GraphicalNode.java @@ -45,7 +45,7 @@ public GraphicalNode(final String id, final String label, final boolean terminal /** * Returns the id of this node. - * @return the if of this node + * @return the id of this node */ public String getId() { return id; diff --git a/src/main/java/com/booleworks/logicng/io/parsers/FormulaParser.java b/src/main/java/com/booleworks/logicng/io/parsers/FormulaParser.java index effba5e6..57014ade 100644 --- a/src/main/java/com/booleworks/logicng/io/parsers/FormulaParser.java +++ b/src/main/java/com/booleworks/logicng/io/parsers/FormulaParser.java @@ -1,79 +1,23 @@ -// SPDX-License-Identifier: Apache-2.0 and MIT -// Copyright 2015-2023 Christoph Zengler -// Copyright 2023-20xx BooleWorks GmbH - package com.booleworks.logicng.io.parsers; import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; -import org.antlr.v4.runtime.BailErrorStrategy; -import org.antlr.v4.runtime.CharStream; -import org.antlr.v4.runtime.CharStreams; -import org.antlr.v4.runtime.CommonTokenStream; -import org.antlr.v4.runtime.Lexer; -import org.antlr.v4.runtime.misc.ParseCancellationException; -import java.io.IOException; import java.io.InputStream; /** - * Super class for a formula parser. - * @version 1.2 - * @since 1.2 + * Interface for formula parsers. + * @version 3.0.0 + * @since 3.0.0 */ -public abstract class FormulaParser { - - private final FormulaFactory f; - private Lexer lexer; - private ParserWithFormula parser; - - /** - * Constructor. - * @param f the formula factory - */ - protected FormulaParser(final FormulaFactory f) { - this.f = f; - } - - /** - * Sets the internal lexer and the parser. - * @param lexer the lexer - * @param parser the parser - */ - protected void setLexerAndParser(final Lexer lexer, final ParserWithFormula parser) { - this.lexer = lexer; - this.parser = parser; - this.parser.setFormulaFactory(f); - this.lexer.removeErrorListeners(); - this.parser.removeErrorListeners(); - this.parser.setErrorHandler(new BailErrorStrategy()); - this.parser.setBuildParseTree(false); - } - +public interface FormulaParser { /** * Parses and returns a given input stream. - * @param inputStream an input stream + * @param inStream an input stream * @return the {@link Formula} representation of this stream * @throws ParserException if there was a problem with the input stream */ - public Formula parse(final InputStream inputStream) throws ParserException { - if (inputStream == null) { - return f.verum(); - } - try { - final CharStream input = CharStreams.fromStream(inputStream); - lexer.setInputStream(input); - final CommonTokenStream tokens = new CommonTokenStream(lexer); - parser.setInputStream(tokens); - return parser.getParsedFormula(); - } catch (final IOException e) { - throw new ParserException("IO exception when parsing the formula", e); - } catch (final ParseCancellationException e) { - throw new ParserException("Parse cancellation exception when parsing the formula", e); - } catch (final LexerException e) { - throw new ParserException("Lexer exception when parsing the formula.", e); - } - } + Formula parse(final InputStream inStream) throws ParserException; /** * Parses and returns a given string. @@ -81,28 +25,11 @@ public Formula parse(final InputStream inputStream) throws ParserException { * @return the {@link Formula} representation of this string * @throws ParserException if the string was not a valid formula */ - public Formula parse(final String in) throws ParserException { - if (in == null || in.isEmpty()) { - return f.verum(); - } - try { - final CharStream input = CharStreams.fromString(in); - lexer.setInputStream(input); - final CommonTokenStream tokens = new CommonTokenStream(lexer); - parser.setInputStream(tokens); - return parser.getParsedFormula(); - } catch (final ParseCancellationException e) { - throw new ParserException("Parse cancellation exception when parsing the formula", e); - } catch (final LexerException e) { - throw new ParserException("Lexer exception when parsing the formula.", e); - } - } + Formula parse(final String in) throws ParserException; /** * Returns the factory of this parser. * @return the factory of this parser */ - public FormulaFactory factory() { - return f; - } + FormulaFactory factory(); } diff --git a/src/main/java/com/booleworks/logicng/io/parsers/LexerException.java b/src/main/java/com/booleworks/logicng/io/parsers/LexerException.java deleted file mode 100644 index 92ea6e90..00000000 --- a/src/main/java/com/booleworks/logicng/io/parsers/LexerException.java +++ /dev/null @@ -1,21 +0,0 @@ -// SPDX-License-Identifier: Apache-2.0 and MIT -// Copyright 2015-2023 Christoph Zengler -// Copyright 2023-20xx BooleWorks GmbH - -package com.booleworks.logicng.io.parsers; - -/** - * A lexer exception for the lexers. - * @version 1.0 - * @since 1.0 - */ -public final class LexerException extends RuntimeException { - - /** - * Constructs a new lexer exception with a given message. - * @param message the message - */ - public LexerException(final String message) { - super(message); - } -} diff --git a/src/main/java/com/booleworks/logicng/io/parsers/ParserException.java b/src/main/java/com/booleworks/logicng/io/parsers/ParserException.java index 786156bf..50230f11 100644 --- a/src/main/java/com/booleworks/logicng/io/parsers/ParserException.java +++ b/src/main/java/com/booleworks/logicng/io/parsers/ParserException.java @@ -17,7 +17,7 @@ public final class ParserException extends Exception { * @param message the message * @param exception the inner exception */ - public ParserException(final String message, final Exception exception) { + public ParserException(final String message, final Throwable exception) { super(message, exception); } } diff --git a/src/main/java/com/booleworks/logicng/io/parsers/ParserWithFormula.java b/src/main/java/com/booleworks/logicng/io/parsers/ParserWithFormula.java deleted file mode 100644 index d9b82c74..00000000 --- a/src/main/java/com/booleworks/logicng/io/parsers/ParserWithFormula.java +++ /dev/null @@ -1,43 +0,0 @@ -// SPDX-License-Identifier: Apache-2.0 and MIT -// Copyright 2015-2023 Christoph Zengler -// Copyright 2023-20xx BooleWorks GmbH - -package com.booleworks.logicng.io.parsers; - -import com.booleworks.logicng.formulas.Formula; -import com.booleworks.logicng.formulas.FormulaFactory; -import org.antlr.v4.runtime.Parser; -import org.antlr.v4.runtime.TokenStream; - -/** - * Abstract super class for parsers which have a formula factory and return a - * formula. - * @version 1.4.0 - * @since 1.4.0 - */ -public abstract class ParserWithFormula extends Parser { - - protected FormulaFactory f; - - /** - * Constructor. - * @param input the token stream (e.g. a lexer) for the parser - */ - public ParserWithFormula(final TokenStream input) { - super(input); - } - - /** - * Sets the LogicNG formula factory for this parser - * @param f the LogicNG formula factory - */ - public void setFormulaFactory(final FormulaFactory f) { - this.f = f; - } - - /** - * Returns the parsed formula. - * @return the parsed formula - */ - public abstract Formula getParsedFormula(); -} diff --git a/src/main/java/com/booleworks/logicng/io/parsers/PropositionalLexer.java b/src/main/java/com/booleworks/logicng/io/parsers/PropositionalLexer.java deleted file mode 100644 index 908b9b26..00000000 --- a/src/main/java/com/booleworks/logicng/io/parsers/PropositionalLexer.java +++ /dev/null @@ -1,29 +0,0 @@ -// SPDX-License-Identifier: Apache-2.0 and MIT -// Copyright 2015-2023 Christoph Zengler -// Copyright 2023-20xx BooleWorks GmbH - -package com.booleworks.logicng.io.parsers; - -import org.antlr.v4.runtime.CharStream; -import org.antlr.v4.runtime.LexerNoViableAltException; - -/** - * A lexer for propositional (including pseudo-Boolean) formulas. - * @version 1.0 - * @since 1.0 - */ -public final class PropositionalLexer extends LogicNGPropositionalLexer { - - /** - * Constructs a new pseudo boolean lexer. - * @param inputStream the input stream - */ - public PropositionalLexer(final CharStream inputStream) { - super(inputStream); - } - - @Override - public void recover(final LexerNoViableAltException exception) { - throw new LexerException(exception.getMessage()); - } -} diff --git a/src/main/java/com/booleworks/logicng/io/parsers/PropositionalParser.java b/src/main/java/com/booleworks/logicng/io/parsers/PropositionalParser.java index f4b35f28..9d25bb84 100644 --- a/src/main/java/com/booleworks/logicng/io/parsers/PropositionalParser.java +++ b/src/main/java/com/booleworks/logicng/io/parsers/PropositionalParser.java @@ -4,8 +4,14 @@ package com.booleworks.logicng.io.parsers; +import com.booleworks.logicng.formulas.Formula; import com.booleworks.logicng.formulas.FormulaFactory; -import org.antlr.v4.runtime.CommonTokenStream; +import com.booleworks.logicng.io.parsers.javacc.BooleanFormulaParser; +import com.booleworks.logicng.io.parsers.javacc.ParseException; +import com.booleworks.logicng.io.parsers.javacc.TokenMgrError; + +import java.io.InputStream; +import java.io.StringReader; /** * A parser for propositional (including pseudo-Boolean) formulas. @@ -44,17 +50,51 @@ * @version 2.4.1 * @since 1.0 */ -public final class PropositionalParser extends FormulaParser { +public final class PropositionalParser implements FormulaParser { + + private final BooleanFormulaParser parser; /** * Constructs a new parser for pseudo boolean formulas. * @param f the formula factory */ public PropositionalParser(final FormulaFactory f) { - super(f); - final PropositionalLexer lexer = new PropositionalLexer(null); - final CommonTokenStream tokens = new CommonTokenStream(lexer); - final ParserWithFormula parser = new LogicNGPropositionalParser(tokens); - setLexerAndParser(lexer, parser); + parser = new BooleanFormulaParser(new StringReader("")); + parser.setFactory(f); + } + + @Override + public Formula parse(final InputStream inStream) throws ParserException { + if (inStream == null) { + return parser.getFactory().verum(); + } + try { + parser.ReInit(inStream); + return parser.formula(); + } catch (final TokenMgrError e) { + throw new ParserException("lexer error", e); + } catch (final ParseException e) { + throw new ParserException("parser error", e); + } + } + + @Override + public Formula parse(final String input) throws ParserException { + if (input == null || input.isBlank()) { + return parser.getFactory().verum(); + } + try { + parser.ReInit(new StringReader(input)); + return parser.formula(); + } catch (final TokenMgrError e) { + throw new ParserException("lexer error", e); + } catch (final ParseException e) { + throw new ParserException("parser error", e); + } + } + + @Override + public FormulaFactory factory() { + return parser.getFactory(); } } diff --git a/src/main/java/com/booleworks/logicng/io/readers/FormulaReader.java b/src/main/java/com/booleworks/logicng/io/readers/FormulaReader.java index 79c02f5a..66d924e4 100644 --- a/src/main/java/com/booleworks/logicng/io/readers/FormulaReader.java +++ b/src/main/java/com/booleworks/logicng/io/readers/FormulaReader.java @@ -14,13 +14,11 @@ import java.io.File; import java.io.FileReader; import java.io.IOException; -import java.util.LinkedHashSet; +import java.util.ArrayList; +import java.util.List; /** - * A reader for formulas. - *

- * Reads a formula from an input file. If the file has more than one line, the - * lines will be co-joined. + * A reader for formula files. * @version 3.0.0 * @since 1.2 */ @@ -34,46 +32,106 @@ private FormulaReader() { } /** - * Reads a given file and returns the contained propositional formula. + * Reads a given file and returns the contained formulas as a formula conjunction. * @param f the formula factory * @param fileName the file name * @return the parsed formula * @throws IOException if there was a problem reading the file * @throws ParserException if there was a problem parsing the formula */ - public static Formula readPropositionalFormula(final FormulaFactory f, final String fileName) - throws IOException, ParserException { - return read(new File(fileName), new PropositionalParser(f)); + public static Formula readFormula(final FormulaFactory f, final String fileName) throws IOException, ParserException { + return readFormula(new PropositionalParser(f), new File(fileName)); } /** - * Reads a given file and returns the contained propositional formula. + * Reads a given file and returns the contained formulas as a formula conjunction. * @param f the formula factory * @param file the file * @return the parsed formula * @throws IOException if there was a problem reading the file * @throws ParserException if there was a problem parsing the formula */ - public static Formula readPropositionalFormula(final FormulaFactory f, final File file) - throws IOException, ParserException { - return read(file, new PropositionalParser(f)); + public static Formula readFormula(final FormulaFactory f, final File file) throws IOException, ParserException { + return readFormula(new PropositionalParser(f), file); } /** - * Internal read function. - * @param file the file + * Reads a given file and returns the contained formulas. + * @param f the formula factory + * @param fileName the file name + * @return the parsed formulas + * @throws IOException if there was a problem reading the file + * @throws ParserException if there was a problem parsing the formula + */ + public static List readFormulas(final FormulaFactory f, final String fileName) throws IOException, ParserException { + return readFormulas(new PropositionalParser(f), new File(fileName)); + } + + /** + * Reads a given file and returns the contained formulas. + * @param f the formula factory + * @param file the file + * @return the parsed formulas + * @throws IOException if there was a problem reading the file + * @throws ParserException if there was a problem parsing the formula + */ + public static List readFormulas(final FormulaFactory f, final File file) throws IOException, ParserException { + return readFormulas(new PropositionalParser(f), file); + } + + /** + * Reads a given file and returns the contained formulas as a formula conjunction. + * @param parser the parser + * @param fileName the file name + * @return the parsed formula + * @throws IOException if there was a problem reading the file + * @throws ParserException if there was a problem parsing the formulas + */ + public static Formula readFormula(final FormulaParser parser, final String fileName) throws IOException, ParserException { + return parser.factory().and(readFormulas(parser, fileName)); + } + + /** + * Reads a given file and returns the contained formulas as a formula conjunction. * @param parser the parser + * @param file the file * @return the parsed formula * @throws IOException if there was a problem reading the file - * @throws ParserException if there was a problem parsing the formula + * @throws ParserException if there was a problem parsing the formulas */ - private static Formula read(final File file, final FormulaParser parser) throws IOException, ParserException { + public static Formula readFormula(final FormulaParser parser, final File file) throws IOException, ParserException { + return parser.factory().and(readFormulas(parser, file)); + } + + /** + * Reads a given file and returns the contained formulas. + * @param parser the parser + * @param fileName the file name + * @return the parsed formulas + * @throws IOException if there was a problem reading the file + * @throws ParserException if there was a problem parsing the formulas + */ + public static List readFormulas(final FormulaParser parser, final String fileName) + throws IOException, ParserException { + return readFormulas(parser, new File(fileName)); + } + + /** + * Reads a given file and returns the contained formulas. + * @param parser the parser + * @param file the file + * @return the parsed formulas + * @throws IOException if there was a problem reading the file + * @throws ParserException if there was a problem parsing the formulas + */ + public static List readFormulas(final FormulaParser parser, final File file) + throws IOException, ParserException { + final List formulas = new ArrayList<>(); try (final BufferedReader br = new BufferedReader(new FileReader(file))) { - final LinkedHashSet ops = new LinkedHashSet<>(); while (br.ready()) { - ops.add(parser.parse(br.readLine())); + formulas.add(parser.parse(br.readLine())); } - return parser.factory().and(ops); } + return formulas; } } diff --git a/src/main/java/com/booleworks/logicng/io/writers/FormulaDimacsFileWriter.java b/src/main/java/com/booleworks/logicng/io/writers/FormulaDimacsFileWriter.java index 56fa7e24..2bbcd759 100644 --- a/src/main/java/com/booleworks/logicng/io/writers/FormulaDimacsFileWriter.java +++ b/src/main/java/com/booleworks/logicng/io/writers/FormulaDimacsFileWriter.java @@ -69,7 +69,7 @@ public static void write(final String fileName, final Formula formula, final boo throw new IllegalArgumentException("Cannot write a non-CNF formula to dimacs. Convert to CNF first."); } final List parts = new ArrayList<>(); - if (formula.type().equals(FType.LITERAL) || formula.type().equals(FType.OR)) { + if (formula.type() == FType.LITERAL || formula.type() == FType.OR) { parts.add(formula); } else { for (final Formula part : formula) { @@ -77,7 +77,7 @@ public static void write(final String fileName, final Formula formula, final boo } } final StringBuilder sb = new StringBuilder("p cnf "); - final int partsSize = formula.type().equals(FType.FALSE) ? 1 : parts.size(); + final int partsSize = formula.type() == FType.FALSE ? 1 : parts.size(); sb.append(var2id.size()).append(" ").append(partsSize).append(System.lineSeparator()); for (final Formula part : parts) { diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDCache.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDCache.java index c984050a..b51e5182 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDCache.java +++ b/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDCache.java @@ -34,12 +34,12 @@ /** * BDD Cache. - * @version 2.0.0 + * @version 3.0.0 * @since 1.4.0 */ public class BDDCache { private final BDDPrime prime; - protected BDDCacheEntry[] table; + private BDDCacheEntry[] table; /** * Constructs a new BDD cache of a given size (number of entries in the @@ -82,7 +82,7 @@ protected void reset() { * @param hash the hash value. * @return the respective entry in the cache */ - protected BDDCacheEntry lookup(final int hash) { + BDDCacheEntry lookup(final int hash) { return table[Math.abs(hash % table.length)]; } } diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java index c19e73d7..e957376e 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java +++ b/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java @@ -88,7 +88,7 @@ protected enum Operand { protected final SortedMap var2idx; protected final SortedMap idx2var; - protected BDDReordering reordering; + protected final BDDReordering reordering; protected int[] nodes; // All the bdd nodes protected int[] vars; // Set of defined BDD variables diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java index e13bba9d..188bd803 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java +++ b/src/main/java/com/booleworks/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java @@ -153,9 +153,7 @@ public void reorder(final BDDReorderingMethod method) { reorderMethod = method; bddreorderTimes = 1; top = new BDDTree(-1); - if (reorderInit() < 0) { - return; - } + reorderInit(); usednumBefore = k.nodesize - k.freenum; top.setFirst(0); top.setLast(k.varnum - 1); @@ -729,7 +727,6 @@ protected int siftTestCmp(final BDDSizePair a, final BDDSizePair b) { return Integer.compare(a.val, b.val); } - // === Random reordering (mostly for debugging and test ) ============= protected BDDTree reorderRandom(final BDDTree t) { BDDTree thisTree; @@ -950,7 +947,6 @@ protected int reorderMakenode(final int var, final int low, final int high) { final int hash; int res; - // Note: We know that low,high has a refcou greater than zero, so there // is no need to add reference *recursively* // Check whether childs are equal @@ -1090,7 +1086,7 @@ protected void reorderAuto() { bddreorderTimes--; } - protected int reorderInit() { + protected void reorderInit() { levels = new LevelData[k.varnum]; for (int n = 0; n < k.varnum; n++) { levels[n] = new LevelData(); @@ -1100,17 +1096,14 @@ protected int reorderInit() { } // First mark and recursive refcou. all roots and childs. Also do some // setup here for both setLevellookup and reorder_gbc - if (markRoots() < 0) { - return -1; - } + markRoots(); // Initialize the hash tables reorderSetLevellookup(); // Garbage collect and rehash to new scheme reorderGbc(); - return 0; } - protected int markRoots() { + protected void markRoots() { final int[] dep = new int[k.varnum]; extRootSize = 0; for (int n = 2; n < k.nodesize; n++) { @@ -1142,7 +1135,6 @@ protected int markRoots() { } k.setHash(0, 0); k.setHash(1, 0); - return 0; } protected void reorderGbc() { diff --git a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfSatSolver.java b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfSatSolver.java index 21bace0b..fa972591 100644 --- a/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfSatSolver.java +++ b/src/main/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfSatSolver.java @@ -22,7 +22,7 @@ public interface DnnfSatSolver { * Returns the factory of the solver * @return the factory */ - public FormulaFactory f(); + FormulaFactory f(); /** * Adds a formula to the solver. The formula is first converted to CNF. @@ -56,7 +56,7 @@ public interface DnnfSatSolver { * Returns {@code true} if the current decision level was previously * selected as backtrack level. * @return {@code true} if the current decision level was previously - * selected as backtrack level, otherwise {@code false} + * selected as backtrack level, otherwise {@code false} */ boolean atAssertionLevel(); diff --git a/src/main/java/com/booleworks/logicng/predicates/ContainsPBCPredicate.java b/src/main/java/com/booleworks/logicng/predicates/ContainsPBCPredicate.java index be049281..1ddbc59a 100644 --- a/src/main/java/com/booleworks/logicng/predicates/ContainsPBCPredicate.java +++ b/src/main/java/com/booleworks/logicng/predicates/ContainsPBCPredicate.java @@ -10,7 +10,7 @@ import com.booleworks.logicng.formulas.Not; /** - * Predicate to test if a formula contains any subformula that is a + * Predicate to test if a formula contains any sub-formula that is a * pseudo-Boolean constraint. * @version 3.0.0 * @since 2.0.0 diff --git a/src/main/java/com/booleworks/logicng/solvers/datastructures/LNGHeap.java b/src/main/java/com/booleworks/logicng/solvers/datastructures/LNGHeap.java index 8923906b..2f3ee0f7 100644 --- a/src/main/java/com/booleworks/logicng/solvers/datastructures/LNGHeap.java +++ b/src/main/java/com/booleworks/logicng/solvers/datastructures/LNGHeap.java @@ -201,7 +201,7 @@ public void clear() { } /** - * Bubbles a element at a given position up. + * Bubbles an element at a given position up. * @param pos the position */ private void percolateUp(final int pos) { @@ -219,7 +219,7 @@ private void percolateUp(final int pos) { } /** - * Bubbles a element at a given position down. + * Bubbles an element at a given position down. * @param pos the position */ private void percolateDown(final int pos) { diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MSU3.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MSU3.java index 7fdb42f8..9c0f2f56 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MSU3.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MSU3.java @@ -174,7 +174,7 @@ protected LNGResult none(final ComputationHandler handler) protected LNGResult iterative(final ComputationHandler handler) { if (encoder.cardEncoding() != CardinalityEncoding.TOTALIZER) { throw new IllegalStateException( - "Error: Currently algorithm MSU3 with iterative encoding only supports the totalizer encoding."); + "Error: Currently algorithm MSU3 with iterative encoding only supports the totalizer encoding."); } nbInitialVariables = nVars(); final LNGIntVector objFunction = new LNGIntVector(); diff --git a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSAT.java b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSAT.java index 5a698182..40e4819a 100644 --- a/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSAT.java +++ b/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSAT.java @@ -75,7 +75,7 @@ public enum ProblemType { final LNGVector hardClauses; final LNGIntVector orderWeights; protected Verbosity verbosity; - int hardWeight; + final int hardWeight; ProblemType problemType; int nbVars; int nbInitialVariables; @@ -443,9 +443,9 @@ public int computeCostModel(final LNGBooleanVector currentModel, final int weigh /** * Tests if the MaxSAT formula has lexicographical optimization criterion. - * @param cache is indicates whether the result should be cached. + * @param cache indicates whether the result should be cached. * @return {@code true} if the formula has lexicographical optimization - * criterion + * criterion */ public boolean isBMO(final boolean cache) { assert orderWeights.size() == 0; @@ -493,7 +493,7 @@ public Stats stats() { * @param lowerBound the new lower bound * @param handler the computation handler * @return the event if the handler canceled the computation, otherwise - * {@code null} + * {@code null} */ LNGEvent foundLowerBound(final int lowerBound, final ComputationHandler handler) { final MaxSatNewLowerBoundEvent event = new MaxSatNewLowerBoundEvent(lowerBound); @@ -507,7 +507,7 @@ LNGEvent foundLowerBound(final int lowerBound, final ComputationHandler handler) * @param upperBound the new upper bound * @param handler the computation handler * @return the event if the handler canceled the computation, otherwise - * {@code null} + * {@code null} */ LNGEvent foundUpperBound(final int upperBound, final ComputationHandler handler) { final MaxSatNewUpperBoundEvent event = new MaxSatNewUpperBoundEvent(upperBound); diff --git a/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java b/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java index 3851e748..bca7c427 100644 --- a/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java +++ b/src/main/java/com/booleworks/logicng/solvers/sat/LNGCoreSolver.java @@ -328,7 +328,7 @@ protected Tristate value(final int lit) { * @param x the first variable * @param y the second variable * @return {@code true} if the first variable's activity is larger than the - * second one's + * second one's */ public boolean lt(final int x, final int y) { return vars.get(x).activity() > vars.get(y).activity(); @@ -391,13 +391,11 @@ public int newVar(final boolean sign, final boolean dvar) { * Adds a unit clause to the solver. * @param lit the unit clause's literal * @param proposition a proposition (if required for proof tracing) - * @return {@code true} if the clause was added successfully, {@code false} - * otherwise */ - public boolean addClause(final int lit, final Proposition proposition) { + public void addClause(final int lit, final Proposition proposition) { final LNGIntVector unit = new LNGIntVector(1); unit.push(lit); - return addClause(unit, proposition); + addClause(unit, proposition); } /** @@ -405,7 +403,7 @@ public boolean addClause(final int lit, final Proposition proposition) { * @param ps the literals of the clause * @param proposition a proposition (if required for proof tracing) * @return {@code true} if the clause was added successfully, {@code false} - * otherwise + * otherwise * @throws IllegalStateException if a {@link SATCall} is currently running * on this solver */ @@ -563,7 +561,7 @@ public LNGBooleanVector model() { * Returns {@code false} if this solver is known to be in a conflicting * state, otherwise {@code true}. * @return {@code false} if this solver is known to be in a conflicting - * state, otherwise {@code true} + * state, otherwise {@code true} */ public boolean ok() { return ok; @@ -888,7 +886,7 @@ protected void removeClause(final LNGClause c) { /** * Performs unit propagation. * @return the conflicting clause if a conflict arose during unit - * propagation or {@code null} if there was none + * propagation or {@code null} if there was none */ protected LNGClause propagate() { LNGClause confl = null; @@ -989,7 +987,7 @@ protected LNGClause propagate() { * @param abstractLevels an abstraction of levels * @param analyzeToClear helper vector * @return {@code true} if a given literal is redundant in the current - * conflict analysis + * conflict analysis */ protected boolean litRedundant(final int p, final int abstractLevels, final LNGIntVector analyzeToClear) { final LNGIntVector analyzeStack = new LNGIntVector(); @@ -1155,9 +1153,9 @@ public LNGVector pgProof() { /** * The main search procedure of the CDCL algorithm. * @return a {@link Tristate} representing the result. {@code FALSE} if the - * formula is UNSAT, {@code TRUE} if the formula is SAT, and - * {@code UNDEF} if the state is not known yet (restart) or the - * handler canceled the computation + * formula is UNSAT, {@code TRUE} if the formula is SAT, and + * {@code UNDEF} if the state is not known yet (restart) or the + * handler canceled the computation */ protected LNGResult search(final ComputationHandler handler) { if (!ok) { @@ -1623,7 +1621,7 @@ public List convertInternalModel(final LNGBooleanVector internalModel, * Returns {@code true} if a {@link SATCall} is currently using this solver, * otherwise {@code false}. * @return {@code true} if a {@link SATCall} is currently using this solver, - * otherwise {@code false} + * otherwise {@code false} */ public boolean inSatCall() { return inSatCall; @@ -1746,7 +1744,7 @@ public LNGResult computeBackbone(final Collection variables, * @param type backbone type * @param handler the handler * @return the backbone projected to the relevant variables or {@code null} - * if the computation was canceled by the handler + * if the computation was canceled by the handler */ public LNGResult computeBackbone(final Collection variables, final BackboneType type, final ComputationHandler handler) { @@ -1935,7 +1933,7 @@ protected Backbone buildBackbone(final Collection variables, final Bac * satisfiable before. * @param var variable index to test * @return {@code true} if the variable is a unit propagated literal on - * level 0, otherwise {@code false} + * level 0, otherwise {@code false} */ protected boolean isUPZeroLit(final int var) { return vars.get(var).level() == 0; diff --git a/src/main/java/com/booleworks/logicng/solvers/sat/SATCall.java b/src/main/java/com/booleworks/logicng/solvers/sat/SATCall.java index edec44cf..46d28902 100644 --- a/src/main/java/com/booleworks/logicng/solvers/sat/SATCall.java +++ b/src/main/java/com/booleworks/logicng/solvers/sat/SATCall.java @@ -4,7 +4,6 @@ import com.booleworks.logicng.collections.LNGIntVector; import com.booleworks.logicng.collections.LNGVector; -import com.booleworks.logicng.datastructures.Assignment; import com.booleworks.logicng.datastructures.Model; import com.booleworks.logicng.explanations.UNSATCore; import com.booleworks.logicng.formulas.FType; @@ -25,7 +24,7 @@ * Encapsulates the data used for a single SAT call to a {@link SATSolver}. *

* A SAT Solver is stateful and features like assumptions, selection order, - * handler etc require manual housekeeping. This class aims to facilitate the + * handler etc. require manual housekeeping. This class aims to facilitate the * interaction with the SAT solver. *

* There can never be more than one SAT call for the same SAT solver. You @@ -117,7 +116,7 @@ public LNGResult getSatResult() { * If the formula is UNSAT, {@code null} will be returned. * @param variables the set of variables * @return a model of the current formula or {@code null} if the SAT call - * was unsatisfiable + * was unsatisfiable * @throws IllegalArgumentException if the given variables are {@code null} */ public Model model(final Collection variables) { diff --git a/src/main/java/com/booleworks/logicng/transformations/CacheableAndCancelableFormulaTransformation.java b/src/main/java/com/booleworks/logicng/transformations/CacheableAndCancelableFormulaTransformation.java index f21ba46b..f9a0665a 100644 --- a/src/main/java/com/booleworks/logicng/transformations/CacheableAndCancelableFormulaTransformation.java +++ b/src/main/java/com/booleworks/logicng/transformations/CacheableAndCancelableFormulaTransformation.java @@ -18,7 +18,7 @@ * by a handler. This cache is usually changed by the transformation. Formulas * from a caching formula factory provide their cache via the factory, formulas * from a non-caching formula factory can be given their own cache per - * transformation. A cacheable and an cancelable formula transformation with a + * transformation. A cacheable and a cancelable formula transformation with a * provided cache or handler is not thread-safe. * @version 3.0.0 * @since 3.0.0 diff --git a/src/main/java/com/booleworks/logicng/transformations/Subsumption.java b/src/main/java/com/booleworks/logicng/transformations/Subsumption.java index 70055ad5..9f26a64d 100644 --- a/src/main/java/com/booleworks/logicng/transformations/Subsumption.java +++ b/src/main/java/com/booleworks/logicng/transformations/Subsumption.java @@ -44,7 +44,6 @@ public Subsumption(final FormulaFactory f) { * @return the UBTree with the operands and deleted subsumed operands */ protected UBTree generateSubsumedUBTree(final Formula formula) { - //noinspection OptionalGetWithoutIsPresent return generateSubsumedUBTree(formula, NopHandler.get()).getResult(); } diff --git a/src/main/java/com/booleworks/logicng/transformations/simplification/AdvancedSimplifierConfig.java b/src/main/java/com/booleworks/logicng/transformations/simplification/AdvancedSimplifierConfig.java index 20c728cb..305bace9 100644 --- a/src/main/java/com/booleworks/logicng/transformations/simplification/AdvancedSimplifierConfig.java +++ b/src/main/java/com/booleworks/logicng/transformations/simplification/AdvancedSimplifierConfig.java @@ -15,11 +15,11 @@ public class AdvancedSimplifierConfig extends Configuration { - boolean restrictBackbone; - boolean factorOut; - boolean simplifyNegations; - boolean useRatingFunction; - RatingFunction ratingFunction; + final boolean restrictBackbone; + final boolean factorOut; + final boolean simplifyNegations; + final boolean useRatingFunction; + final RatingFunction ratingFunction; @Override public String toString() { diff --git a/src/main/java/com/booleworks/logicng/util/FormulaRandomizerConfig.java b/src/main/java/com/booleworks/logicng/util/FormulaRandomizerConfig.java index 8d21dd36..117ada29 100644 --- a/src/main/java/com/booleworks/logicng/util/FormulaRandomizerConfig.java +++ b/src/main/java/com/booleworks/logicng/util/FormulaRandomizerConfig.java @@ -435,7 +435,7 @@ public Builder maximumOperandsPbc(final int maximumOperandsPbc) { /** * Sets the maximum absolute value of a coefficient in a pseudo boolean - * constraint. Whether the coefficient is positive or negative is + * constraint. Whether the coefficient is positive or negative * depends on {@link #weightPbcCoeffPositive} and * {@link #weightPbcCoeffNegative}. * @param maximumCoefficientPbc the maximum absolute value of a diff --git a/src/main/java/module-info.java b/src/main/java/module-info.java index adce3de1..163da8b1 100644 --- a/src/main/java/module-info.java +++ b/src/main/java/module-info.java @@ -1,7 +1,4 @@ module logicng { - requires org.antlr.antlr4.runtime; - requires java.xml; - exports com.booleworks.logicng.backbones; exports com.booleworks.logicng.encodings; diff --git a/src/main/javacc/BooleanParser.jj b/src/main/javacc/BooleanParser.jj new file mode 100644 index 00000000..422ef3bc --- /dev/null +++ b/src/main/javacc/BooleanParser.jj @@ -0,0 +1,170 @@ +// SPDX-License-Identifier: Apache-2.0 and MIT +// Copyright 2023-20xx BooleWorks GmbH + +//noinspection UnreachableCode +options { + STATIC = false; +} + +PARSER_BEGIN(BooleanFormulaParser) +package com.booleworks.logicng.io.parsers.javacc; + +import com.booleworks.logicng.formulas.*; +import com.booleworks.logicng.util.Pair; + +import java.util.ArrayList; +import java.util.LinkedHashSet; +import java.util.List; + +public class BooleanFormulaParser { + + private FormulaFactory f; + + public void setFactory(final FormulaFactory f) { + this.f = f; + } + + public FormulaFactory getFactory() { + return this.f; + } +} + +PARSER_END(BooleanFormulaParser) + +SKIP : { " " | "\t" | "\n" | "\r" } + +TOKEN : +{ + + | < LITERAL : (["~"])? (["A"-"Z", "a"-"z", "0"-"9", "_", "@", "#"])+ > + | + | + | + | + | + | + | + | "> + | "> + | + | + | + | ="> + | "> +} + +Formula formula() : { Formula formula; } +{ + ( { formula = f.verum(); } + | formula = equiv() + ) + { return formula;} +} + +Formula equiv() : { + Formula left; + Formula right = null; +} +{ + left = impl() ( right = equiv() )? { return right == null ? left : f.equivalence(left, right); } +} + +Formula impl() : { + Formula left; + Formula right = null; +} +{ + left = disj() ( right = impl())? { return right == null ? left : f.implication(left, right); } +} + +Formula disj() : { + Formula a, b; + LinkedHashSet conjs = new LinkedHashSet<>(); +} +{ + a = conj() { conjs.add(a); } ( b = conj() { conjs.add(b); })* { return f.or(conjs); } +} + +Formula conj() : { + Formula a, b; + LinkedHashSet lits = new LinkedHashSet<>(); +} +{ + a = lit() { lits.add(a); } ( b = lit() { lits.add(b); })* { return f.and(lits); } +} + +Formula lit() : { Formula formula, op; } +{ + ( op = lit() { formula = f.not(op); } + | formula = simp() + ) + { return formula; } +} + +Formula simp() : { Formula formula; } +{ + ( formula = comparison() + | formula = constant() + | formula = equiv() + ) + { return formula; } +} + +Formula comparison() : { + Formula formula; + Pair, List> e; + CType c; + Token t; +} +{ + ( LOOKAHEAD(2) e = add() c = comperator() t = {formula = f.pbc(c, Integer.parseInt(t.image), e.first(), e.second()); } + | t = { formula = (t.image.startsWith("~") ? f.literal(t.image.substring(1), false) : f.literal(t.image, true)); } + | t = { formula = (t.image.startsWith("~") ? f.literal(t.image.substring(1), false) : f.literal(t.image, true)); } + ) + { return formula; } +} + +CType comperator() : { + +} +{ + { return CType.EQ; } + | { return CType.LE; } + | { return CType.LT; } + | { return CType.GE; } + | { return CType.GT; } +} + +Pair, List> add() : { + Pair m1, m2; + List lits = new ArrayList<>(); + List coeffs = new ArrayList<>(); + Token a; +} +{ + m1 = mul() { lits.add(m1.first()); coeffs.add(m1.second()); } (a = m2 = mul() { lits.add(m2.first()); coeffs.add (a.image.equals("+") ? m2.second() : -m2.second()); })* + { return new Pair<>(lits, coeffs); } +} + +Pair mul() : { + Token n, l; + Literal lit; + int c = 1; +} +{ + ( LOOKAHEAD(3) n = l = {lit = (l.image.startsWith("~") ? f.literal(l.image.substring(1), false) : f .literal(l.image, true)); c = Integer.parseInt(n.image); } + | LOOKAHEAD(3) n = l = {lit = f.literal(l.image, true); c = Integer.parseInt(n.image); } + | l = { lit = (l.image.startsWith("~") ? f.literal(l.image.substring(1), false) : f.literal (l.image, true) ); } + | n = { lit = f.literal(n.image, true); } + ) + { return new Pair<>(lit, c); } +} + +Formula constant() : {} +{ + { return f.verum(); } + | { return f.falsum(); } +} + diff --git a/src/test/java/com/booleworks/logicng/backbones/BackboneGenerationTest.java b/src/test/java/com/booleworks/logicng/backbones/BackboneGenerationTest.java index 9fe06c65..930effef 100644 --- a/src/test/java/com/booleworks/logicng/backbones/BackboneGenerationTest.java +++ b/src/test/java/com/booleworks/logicng/backbones/BackboneGenerationTest.java @@ -194,7 +194,7 @@ public void testSimpleBackbones() { public void testSmallFormulas() throws IOException, ParserException { final FormulaFactory f = FormulaFactory.caching(); final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/small_formulas.txt"); final SATSolver solver = SATSolver.newSolver(f); solver.add(formula); final Backbone backbone = solver.execute(BackboneFunction.builder().variables(formula.variables(f)).build()); @@ -205,7 +205,7 @@ public void testSmallFormulas() throws IOException, ParserException { public void testLargeFormula() throws IOException, ParserException { final FormulaFactory f = FormulaFactory.caching(); final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/large_formula.txt"); final SATSolver solver = SATSolver.newSolver(f); solver.add(formula); final Backbone backbone = solver.execute(BackboneFunction.builder().variables(formula.variables(f)).build()); diff --git a/src/test/java/com/booleworks/logicng/explanations/smus/SmusComputationTest.java b/src/test/java/com/booleworks/logicng/explanations/smus/SmusComputationTest.java index fd42891e..47f16dd7 100644 --- a/src/test/java/com/booleworks/logicng/explanations/smus/SmusComputationTest.java +++ b/src/test/java/com/booleworks/logicng/explanations/smus/SmusComputationTest.java @@ -230,7 +230,7 @@ public void testTimeoutHandlerLarge() throws ParserException, IOException { new TimeoutHandler(System.currentTimeMillis() + 1L, FIXED_END) ); final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/large_formula.txt"); final List formulas = formula.stream().collect(Collectors.toList()); for (final TimeoutHandler handler : handlers) { testHandler(handler, formulas, true); diff --git a/src/test/java/com/booleworks/logicng/functions/MinimumPrimeImplicantTest.java b/src/test/java/com/booleworks/logicng/functions/MinimumPrimeImplicantTest.java index 1d544599..6e0f9938 100644 --- a/src/test/java/com/booleworks/logicng/functions/MinimumPrimeImplicantTest.java +++ b/src/test/java/com/booleworks/logicng/functions/MinimumPrimeImplicantTest.java @@ -91,7 +91,7 @@ public void testSmallExamples() throws ParserException { @Test public void testMiddleExamples() throws IOException, ParserException { - final Formula parsed = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/formula1.txt"); + final Formula parsed = FormulaReader.readFormula(f, "src/test/resources/formulas/formula1.txt"); for (final Formula formula : parsed) { isPrimeImplicant(formula, formula.apply(new MinimumPrimeImplicantFunction(f))); } @@ -100,7 +100,7 @@ public void testMiddleExamples() throws IOException, ParserException { @Test public void testLargeExamples() throws IOException, ParserException { final Formula parsed = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/small_formulas.txt"); for (final Formula formula : parsed) { isPrimeImplicant(formula, formula.apply(new MinimumPrimeImplicantFunction(f))); } diff --git a/src/test/java/com/booleworks/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java b/src/test/java/com/booleworks/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java index eec0a3a6..f9715949 100644 --- a/src/test/java/com/booleworks/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java +++ b/src/test/java/com/booleworks/logicng/graphs/algorithms/ConnectedComponentsComputerTest.java @@ -63,7 +63,7 @@ public void graph30Test() throws IOException { } @Test - public void graph60Test() throws IOException { + public void graph50Test() throws IOException { final Graph g = GraphTest.getLongGraph("50"); for (long i = 0; i < 60; i++) { g.node(i); @@ -100,7 +100,7 @@ public void graph60Test() throws IOException { public void testFormulaSplit() throws IOException, ParserException { final FormulaFactory f = FormulaFactory.caching(); f.putConfiguration(EncoderConfig.builder().amoEncoding(EncoderConfig.AMO_ENCODER.PURE).build()); - final Formula parsed = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/formula1.txt"); + final Formula parsed = FormulaReader.readFormula(f, "src/test/resources/formulas/formula1.txt"); final List formulas = new ArrayList<>(); final List originalFormulas = new ArrayList<>(); for (final Formula formula : parsed) { diff --git a/src/test/java/com/booleworks/logicng/graphs/generators/ConstraintGraphGeneratorTest.java b/src/test/java/com/booleworks/logicng/graphs/generators/ConstraintGraphGeneratorTest.java index 2354dabd..0dcbabad 100644 --- a/src/test/java/com/booleworks/logicng/graphs/generators/ConstraintGraphGeneratorTest.java +++ b/src/test/java/com/booleworks/logicng/graphs/generators/ConstraintGraphGeneratorTest.java @@ -86,10 +86,10 @@ public void testCnf() throws ParserException { expected.connect(d, a); expected.connect(d, e); assertThat(ConstraintGraphGenerator.generateFromFormulas(f, - p.parse("a | ~b | c"), - p.parse("d | ~a"), - p.parse("d + e = 1"), - p.parse("g")).toString()) + p.parse("a | ~b | c"), + p.parse("d | ~a"), + p.parse("d + e = 1"), + p.parse("g")).toString()) .isEqualTo(expected.toString()); } @@ -97,7 +97,7 @@ public void testCnf() throws ParserException { public void testRealExample() throws IOException, ParserException { final FormulaFactory f = FormulaFactory.caching(); f.putConfiguration(EncoderConfig.builder().amoEncoding(EncoderConfig.AMO_ENCODER.PURE).build()); - final Formula parsed = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/formula1.txt"); + final Formula parsed = FormulaReader.readFormula(f, "src/test/resources/formulas/formula1.txt"); final List formulas = new ArrayList<>(); for (final Formula formula : parsed) { if (formula instanceof PBConstraint) { diff --git a/src/test/java/com/booleworks/logicng/io/FormulaWriterReaderTest.java b/src/test/java/com/booleworks/logicng/io/FormulaWriterReaderTest.java index 7191aab7..129bf18f 100644 --- a/src/test/java/com/booleworks/logicng/io/FormulaWriterReaderTest.java +++ b/src/test/java/com/booleworks/logicng/io/FormulaWriterReaderTest.java @@ -33,8 +33,8 @@ public void testSimpleFormulaOneLine() throws ParserException, IOException { final FormulaFactory f = FormulaFactory.caching(); final Formula p1 = new PropositionalParser(f).parse("A & B & ~(C | (D => ~E))"); FormulaWriter.write(file, p1, false); - final Formula p2 = FormulaReader.readPropositionalFormula(f, fileName); - final Formula p3 = FormulaReader.readPropositionalFormula(f, file); + final Formula p2 = FormulaReader.readFormula(f, fileName); + final Formula p3 = FormulaReader.readFormula(f, file); assertThat(p2).isEqualTo(p1); assertThat(p3).isEqualTo(p1); try (final BufferedReader reader = new BufferedReader(new FileReader(fileName))) { @@ -55,7 +55,7 @@ public void testSimpleFormulaMultiLine() throws ParserException, IOException { final FormulaFactory f = FormulaFactory.caching(); final Formula p1 = new PropositionalParser(f).parse("A & B & ~(C | (D => ~E))"); FormulaWriter.write(fileName, p1, true); - final Formula p2 = FormulaReader.readPropositionalFormula(f, fileName); + final Formula p2 = FormulaReader.readFormula(f, fileName); assertThat(p2).isEqualTo(p1); try (final BufferedReader reader = new BufferedReader(new FileReader(fileName))) { int count = 0; @@ -75,8 +75,8 @@ public void testPBFormulaOneLine() throws ParserException, IOException { final FormulaFactory f = FormulaFactory.caching(); final Formula p1 = new PropositionalParser(f).parse("A & B & ~(C | (D => ~E)) & (2*y + 3*y >= 4) & (x <= 1)"); FormulaWriter.write(fileName, p1, false); - final Formula p2 = FormulaReader.readPropositionalFormula(f, fileName); - final Formula p3 = FormulaReader.readPropositionalFormula(f, file); + final Formula p2 = FormulaReader.readFormula(f, fileName); + final Formula p3 = FormulaReader.readFormula(f, file); assertThat(p2).isEqualTo(p1); assertThat(p3).isEqualTo(p1); try (final BufferedReader reader = new BufferedReader(new FileReader(fileName))) { @@ -97,7 +97,7 @@ public void testPBFormulaMultiLine() throws ParserException, IOException { final FormulaFactory f = FormulaFactory.caching(); final Formula p1 = new PropositionalParser(f).parse("A & B & ~(C | (D => ~E)) & (2*y + 3*y >= 4) & (x <= 1)"); FormulaWriter.write(fileName, p1, true); - final Formula p2 = FormulaReader.readPropositionalFormula(f, fileName); + final Formula p2 = FormulaReader.readFormula(f, fileName); assertThat(p2).isEqualTo(p1); try (final BufferedReader reader = new BufferedReader(new FileReader(fileName))) { int count = 0; @@ -118,7 +118,7 @@ public void testSimpleFormulaOneLineFormatter() throws ParserException, IOExcept final Formula p1 = new PropositionalParser(f).parse("A & B & ~(C | (D => ~E))"); FormulaWriter.write(fileName, p1, false, new UTF8StringRepresentation()); try (final BufferedReader reader = - new BufferedReader(new InputStreamReader(new FileInputStream(fileName), StandardCharsets.UTF_8))) { + new BufferedReader(new InputStreamReader(new FileInputStream(fileName), StandardCharsets.UTF_8))) { assertThat(reader.readLine()).isEqualTo("A ∧ B ∧ ¬(C ∨ (D ⇒ ¬E))"); } Files.deleteIfExists(file.toPath()); @@ -132,7 +132,7 @@ public void testSimpleFormulaMultiLineFormatter() throws ParserException, IOExce final Formula p1 = new PropositionalParser(f).parse("A & B & ~(C | (D => ~E))"); FormulaWriter.write(fileName, p1, true, new UTF8StringRepresentation()); try (final BufferedReader reader = - new BufferedReader(new InputStreamReader(new FileInputStream(fileName), StandardCharsets.UTF_8))) { + new BufferedReader(new InputStreamReader(new FileInputStream(fileName), StandardCharsets.UTF_8))) { assertThat(reader.readLine()).isEqualTo("A"); assertThat(reader.readLine()).isEqualTo("B"); assertThat(reader.readLine()).isEqualTo("¬(C ∨ (D ⇒ ¬E))"); diff --git a/src/test/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java b/src/test/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java index f48ffe15..7820522a 100644 --- a/src/test/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java +++ b/src/test/java/com/booleworks/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java @@ -108,7 +108,7 @@ public void testDnnfProperties() throws ParserException { public void testDnnfEvents() throws ParserException, IOException { final FormulaFactory f = FormulaFactory.caching(); f.putConfiguration(EncoderConfig.builder().amoEncoding(EncoderConfig.AMO_ENCODER.PURE).build()); - final Formula parsed = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/formula1.txt"); + final Formula parsed = FormulaReader.readFormula(f, "src/test/resources/formulas/formula1.txt"); final DnnfComputationHandler handler = new DnnfComputationHandler(); final LNGResult dnnf = DnnfFactory.compile(f, parsed, handler); assertThat(dnnf.isSuccess()).isTrue(); @@ -132,7 +132,7 @@ public void testDnnfEvents() throws ParserException, IOException { public void testLargeFormula() throws IOException, ParserException { final FormulaFactory f = FormulaFactory.caching(); f.putConfiguration(EncoderConfig.builder().amoEncoding(EncoderConfig.AMO_ENCODER.PURE).build()); - final Formula parsed = FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/formula1.txt"); + final Formula parsed = FormulaReader.readFormula(f, "src/test/resources/formulas/formula1.txt"); Dnnf dnnf = DnnfFactory.compile(f, parsed); final BigInteger dnnfCount = dnnf.execute(new DnnfModelCountFunction(f)); final List formulas = new ArrayList<>(); diff --git a/src/test/java/com/booleworks/logicng/primecomputation/PrimeCompilerTest.java b/src/test/java/com/booleworks/logicng/primecomputation/PrimeCompilerTest.java index 9b0ebc44..f952c758 100644 --- a/src/test/java/com/booleworks/logicng/primecomputation/PrimeCompilerTest.java +++ b/src/test/java/com/booleworks/logicng/primecomputation/PrimeCompilerTest.java @@ -150,7 +150,7 @@ public void testTimeoutHandlerLarge() throws ParserException, IOException { new TimeoutHandler(System.currentTimeMillis() + 1L, FIXED_END) ); final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/large_formula.txt"); for (final TimeoutHandler handler : handlers) { testHandler(handler, formula, compiler.first(), compiler.second(), true); } diff --git a/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicantReductionTest.java b/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicantReductionTest.java index 392d05e3..df8f9343 100644 --- a/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicantReductionTest.java +++ b/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicantReductionTest.java @@ -67,7 +67,7 @@ public void testSimple(final FormulaContext _c) throws ParserException { @MethodSource("contexts") public void testFormula1(final FormulaContext _c) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(_c.f, "src/test/resources/formulas/formula1.txt"); + FormulaReader.readFormula(_c.f, "src/test/resources/formulas/formula1.txt"); testFormula(formula); } @@ -75,7 +75,7 @@ public void testFormula1(final FormulaContext _c) throws IOException, ParserExce @MethodSource("contexts") public void testSimplifyFormulas(final FormulaContext _c) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(_c.f, "src/test/resources/formulas/simplify_formulas.txt"); + FormulaReader.readFormula(_c.f, "src/test/resources/formulas/simplify_formulas.txt"); testFormula(formula); } @@ -84,7 +84,7 @@ public void testSimplifyFormulas(final FormulaContext _c) throws IOException, Pa @LongRunningTag public void testLargeFormula(final FormulaContext _c) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(_c.f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(_c.f, "src/test/resources/formulas/large_formula.txt"); testFormula(formula); } @@ -119,7 +119,7 @@ public void testRandom() { @Test public void testCancellationPoints() throws ParserException, IOException { - final Formula formula = FormulaReader.readPropositionalFormula(FormulaFactory.nonCaching(), + final Formula formula = FormulaReader.readFormula(FormulaFactory.nonCaching(), "src/test/resources/formulas/large_formula.txt"); for (int numStarts = 0; numStarts < 20; numStarts++) { final ComputationHandler handler = new BoundedSatHandler(numStarts); diff --git a/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicateReductionTest.java b/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicateReductionTest.java index ec2e46e8..3816030b 100644 --- a/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicateReductionTest.java +++ b/src/test/java/com/booleworks/logicng/primecomputation/PrimeImplicateReductionTest.java @@ -58,7 +58,7 @@ public void testPrimeImplicateNaive(final FormulaContext _c) throws ParserExcept @MethodSource("contexts") public void testFormula1(final FormulaContext _c) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(_c.f, "src/test/resources/formulas/formula1.txt"); + FormulaReader.readFormula(_c.f, "src/test/resources/formulas/formula1.txt"); testFormula(formula); } @@ -66,7 +66,7 @@ public void testFormula1(final FormulaContext _c) throws IOException, ParserExce @MethodSource("contexts") public void testSimplifyFormulas(final FormulaContext _c) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(_c.f, "src/test/resources/formulas/simplify_formulas.txt"); + FormulaReader.readFormula(_c.f, "src/test/resources/formulas/simplify_formulas.txt"); testFormula(formula); } @@ -74,7 +74,7 @@ public void testSimplifyFormulas(final FormulaContext _c) throws IOException, Pa @MethodSource("contexts") public void testLargeFormula(final FormulaContext _c) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(_c.f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(_c.f, "src/test/resources/formulas/large_formula.txt"); testFormula(formula); } @@ -108,7 +108,7 @@ public void testRandom() { @Test public void testCancellationPoints() throws ParserException, IOException { - final Formula formula = FormulaReader.readPropositionalFormula(FormulaFactory.nonCaching(), + final Formula formula = FormulaReader.readFormula(FormulaFactory.nonCaching(), "src/test/resources/formulas/large_formula.txt"); for (int numStarts = 0; numStarts < 20; numStarts++) { final ComputationHandler handler = new BoundedSatHandler(numStarts); diff --git a/src/test/java/com/booleworks/logicng/solvers/functions/BackboneFunctionTest.java b/src/test/java/com/booleworks/logicng/solvers/functions/BackboneFunctionTest.java index 81d7846a..3356d6d1 100644 --- a/src/test/java/com/booleworks/logicng/solvers/functions/BackboneFunctionTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/functions/BackboneFunctionTest.java @@ -39,7 +39,6 @@ @SuppressWarnings("unused") public class BackboneFunctionTest { - public static List solvers() { final FormulaFactory f = FormulaFactory.caching(); return SolverTestSet.solverTestSetForParameterizedTests(Set.of(USE_AT_MOST_CLAUSES, CNF_METHOD), f); @@ -103,7 +102,7 @@ public void testSimpleFormulasWithBuilderUsage(final SATSolver solver, final Str final FormulaFactory f = solver.factory(); solver.add(f.parse("(a => c | d) & (b => d | ~e) & (a | b)")); Backbone backbone = solver.execute(BackboneFunction.builder().variables( - f.variable("a"), f.variable("b"), f.variable("c"), f.variable("d"), f.variable("e"), f.variable("f")) + f.variable("a"), f.variable("b"), f.variable("c"), f.variable("d"), f.variable("e"), f.variable("f")) .build()); assertThat(backbone.isSat()).isTrue(); assertThat(backbone.getCompleteBackbone(f)).isEmpty(); @@ -124,7 +123,7 @@ public void testRealFormulaIncremental1(final SATSolver solver, final String sol throws IOException, ParserException { final FormulaFactory f = solver.factory(); final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/large_formula.txt"); solver.add(formula); final List expectedBackbones = new ArrayList<>(); final BufferedReader reader = @@ -168,7 +167,7 @@ public void testRealFormulaIncremental2(final SATSolver solver, final String sol throws IOException, ParserException { final FormulaFactory f = solver.factory(); final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/small_formulas.txt"); solver.add(formula); final List expectedBackbones = new ArrayList<>(); final BufferedReader reader = @@ -212,7 +211,7 @@ public void testRealFormulaIncrementalDecremental1(final SATSolver solver, final throws IOException, ParserException { final FormulaFactory f = solver.factory(); final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/large_formula.txt"); solver.add(formula); final SolverState state = solver.saveState(); final List expectedBackbones = new ArrayList<>(); @@ -267,7 +266,7 @@ public void testRealFormulaIncrementalDecremental2(final SATSolver solver, final throws IOException, ParserException { final FormulaFactory f = solver.factory(); final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/small_formulas.txt"); solver.add(formula); final SolverState state = solver.saveState(); final List expectedBackbones = new ArrayList<>(); diff --git a/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java b/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java index 55d8b7c1..81beec4a 100644 --- a/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java @@ -292,7 +292,7 @@ public void testLargeFormulaMinimize(final Function s final String solverDescription) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/large_formula.txt"); final List variables = randomSubset(formula.variables(f), 300); final LNGResult minimumModel = optimize(Collections.singleton(formula), variables, Collections.emptyList(), false, solver.apply(f), NopHandler.get()); @@ -306,7 +306,7 @@ public void testLargeFormulaMaximize(final Function s final String solverDescription) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/large_formula.txt"); final LNGResult maximumModel = optimize(Collections.singleton(formula), formula.variables(f), Collections.emptyList(), true, solver.apply(f), NopHandler.get()); testMaximumModel(formula, maximumModel, formula.variables(f)); @@ -319,7 +319,7 @@ public void testLargerFormulaMinimize(final Function final String solverDescription) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/small_formulas.txt"); final LNGResult minimumModel = optimize(Collections.singleton(formula), formula.variables(f), Collections.emptyList(), false, solver.apply(f), NopHandler.get()); testMinimumModel(formula, minimumModel, formula.variables(f)); @@ -332,7 +332,7 @@ public void testLargerFormulaMaximize(final Function final String solverDescription) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/small_formulas.txt"); final List variables = randomSubset(formula.variables(f), 300); final LNGResult maximumModel = optimize(Collections.singleton(formula), variables, Collections.emptyList(), true, solver.apply(f), NopHandler.get()); @@ -375,7 +375,7 @@ public void testTimeoutOptimizationHandler(final Function maximumModel = optimize(Collections.singleton(formula), formula.variables(f), Collections.emptyList(), true, solver.apply(f), handlerMax); diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java index e379d867..42ece5a8 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java @@ -182,7 +182,7 @@ public void testWMSU3BMO() throws IOException { } @Test - public void testLineaerSUBMO() throws IOException { + public void testLinearSUBMO() throws IOException { final MaxSATConfig[] configs = new MaxSATConfig[2]; configs[0] = MaxSATConfig.builder().cardinality(MaxSATConfig.CardinalityEncoding.TOTALIZER).bmo(true) .verbosity(MaxSATConfig.Verbosity.SOME).output(logStream).build(); diff --git a/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java b/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java index 1ae9a4bf..83dbd64f 100644 --- a/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/sat/SATCallTest.java @@ -131,7 +131,7 @@ public void testDisallowNullVariablesInModel() { @Test public void testHandler() throws IOException, ParserException { final SATSolver solver = SATSolver.newSolver(f, SATSolverConfig.builder().proofGeneration(true).build()); - solver.add(FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/small_formulas.txt")); + solver.add(FormulaReader.readFormula(f, "src/test/resources/formulas/small_formulas.txt")); try (final SATCall satCall = solver.satCall().handler(new MaxConflictsHandler(0)).solve()) { assertThat(satCall.getSatResult().isSuccess()).isFalse(); diff --git a/src/test/java/com/booleworks/logicng/transformations/cnf/CNFSubsumptionTest.java b/src/test/java/com/booleworks/logicng/transformations/cnf/CNFSubsumptionTest.java index d849b507..5f82ef26 100644 --- a/src/test/java/com/booleworks/logicng/transformations/cnf/CNFSubsumptionTest.java +++ b/src/test/java/com/booleworks/logicng/transformations/cnf/CNFSubsumptionTest.java @@ -75,7 +75,7 @@ public void testNotInCNF() { public void testEvenLargerFormula() throws IOException, ParserException { final FormulaFactory f = FormulaFactory.caching(); final Formula formula = - FormulaReader.readPropositionalFormula(f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(f, "src/test/resources/formulas/large_formula.txt"); final Formula cnf = formula.transform(new CNFFactorization(f)); final Formula subsumed = cnf.transform(new CNFSubsumption(f)); assertThat(f.equivalence(cnf, subsumed).holds(new TautologyPredicate(f))).isTrue(); diff --git a/src/test/java/com/booleworks/logicng/transformations/cnf/CnfMethodComparisonTest.java b/src/test/java/com/booleworks/logicng/transformations/cnf/CnfMethodComparisonTest.java index ae032d07..bdc05efa 100644 --- a/src/test/java/com/booleworks/logicng/transformations/cnf/CnfMethodComparisonTest.java +++ b/src/test/java/com/booleworks/logicng/transformations/cnf/CnfMethodComparisonTest.java @@ -88,7 +88,7 @@ private Backbone computeBackbone(final String fileName, final CNFConfig cnfConfi throws IOException, ParserException { final FormulaFactory f = FormulaFactory.caching(); f.putConfiguration(cnfConfig); - final Formula formula = FormulaReader.readPropositionalFormula(f, fileName); + final Formula formula = FormulaReader.readFormula(f, fileName); final SATSolver solver = SATSolver.newSolver(f, SATSolverConfig.builder().cnfMethod(cnfMethod).build()); solver.add(formula); return solver.backbone(formula.variables(f)); @@ -113,7 +113,7 @@ private Map computeBackbonePerVariable(final String fileName // final long start = System.currentTimeMillis(); final FormulaFactory f = FormulaFactory.caching(); f.putConfiguration(cnfConfig); - final Formula formula = FormulaReader.readPropositionalFormula(f, fileName); + final Formula formula = FormulaReader.readFormula(f, fileName); final SATSolver solver = SATSolver.newSolver(f, SATSolverConfig.builder().cnfMethod(cnfMethod).build()); solver.add(formula); final SolverState solverState = solver.saveState(); diff --git a/src/test/java/com/booleworks/logicng/transformations/dnf/DNFSubsumptionTest.java b/src/test/java/com/booleworks/logicng/transformations/dnf/DNFSubsumptionTest.java index ed6b41ab..b821aa67 100644 --- a/src/test/java/com/booleworks/logicng/transformations/dnf/DNFSubsumptionTest.java +++ b/src/test/java/com/booleworks/logicng/transformations/dnf/DNFSubsumptionTest.java @@ -64,7 +64,7 @@ public void testLargeDNFSubsumption(final FormulaContext _c) throws ParserExcept @LongRunningTag public void testEvenLargerFormulas(final FormulaContext _c) throws IOException, ParserException { final Formula formula = - FormulaReader.readPropositionalFormula(_c.f, "src/test/resources/formulas/small_formulas.txt"); + FormulaReader.readFormula(_c.f, "src/test/resources/formulas/small_formulas.txt"); int count = 10; // test only first 10 formulas for (final Formula op : formula) { if (count == 0) { diff --git a/src/test/java/com/booleworks/logicng/transformations/simplification/AdvancedSimplifierTest.java b/src/test/java/com/booleworks/logicng/transformations/simplification/AdvancedSimplifierTest.java index 71f646a9..57b8b79a 100644 --- a/src/test/java/com/booleworks/logicng/transformations/simplification/AdvancedSimplifierTest.java +++ b/src/test/java/com/booleworks/logicng/transformations/simplification/AdvancedSimplifierTest.java @@ -84,7 +84,7 @@ public void testTimeoutHandlerLarge(final FormulaContext _c) throws ParserExcept new TimeoutHandler(System.currentTimeMillis() + 1L, TimeoutHandler.TimerType.FIXED_END) ); final Formula formula = - FormulaReader.readPropositionalFormula(_c.f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(_c.f, "src/test/resources/formulas/large_formula.txt"); for (final TimeoutHandler handler : handlers) { testHandler(handler, formula, true); } diff --git a/src/test/java/com/booleworks/logicng/transformations/simplification/QuineMcCluskeyTest.java b/src/test/java/com/booleworks/logicng/transformations/simplification/QuineMcCluskeyTest.java index 6b40856b..2cce8c59 100644 --- a/src/test/java/com/booleworks/logicng/transformations/simplification/QuineMcCluskeyTest.java +++ b/src/test/java/com/booleworks/logicng/transformations/simplification/QuineMcCluskeyTest.java @@ -78,7 +78,7 @@ public void testLarge1(final FormulaContext _c) throws ParserException { @MethodSource("contexts") public void testLarge2(final FormulaContext _c) throws ParserException, IOException { final Formula formula = - FormulaReader.readPropositionalFormula(_c.f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(_c.f, "src/test/resources/formulas/large_formula.txt"); final SATSolver solver = SATSolver.newSolver(_c.f); solver.add(formula); final List models = solver.enumerateAllModels(Arrays.asList( @@ -106,7 +106,7 @@ public void testLarge2(final FormulaContext _c) throws ParserException, IOExcept @MethodSource("contexts") public void testLarge3(final FormulaContext _c) throws ParserException, IOException { final Formula formula = - FormulaReader.readPropositionalFormula(_c.f, "src/test/resources/formulas/large_formula.txt"); + FormulaReader.readFormula(_c.f, "src/test/resources/formulas/large_formula.txt"); final SATSolver solver = SATSolver.newSolver(_c.f); solver.add(formula); final List models = solver.enumerateAllModels(Arrays.asList(