Added parser setter to formula factory

booleworks · May 4, 2024 · 17c6e09 · 17c6e09
1 parent 248545e
commit 17c6e09
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 29 deletions.
diff --git 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<? extends Literal> literals,
                                 final List<Integer> 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<Formula> 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<Formula> formulas, final Formula formula) {
         if (!simplifyComplementaryOperands) {
@@ -981,7 +1000,7 @@ private boolean containsComplement(final LinkedHashSet<Formula> 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/...ain/java/com/booleworks/logicng/formulas/implementation/cached/CachingFormulaFactory.java b/...ain/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<String, Variable> posLiterals;
     Map<String, Literal> negLiterals;
     Map<Formula, Not> 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/...a/com/booleworks/logicng/formulas/implementation/noncaching/NonCachingFormulaFactory.java b/...a/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();