Remove implementation-dependent functions from EncodingResult

booleworks · Dec 16, 2024 · bdc2198 · bdc2198
1 parent 1128139
commit bdc2198
Show file tree

Hide file tree

Showing 14 changed files with 136 additions and 148 deletions.
diff --git a/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResult.java b/core/src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResult.java
@@ -5,15 +5,10 @@
 package com.booleworks.logicng.datastructures.encodingresult;
 
 import com.booleworks.logicng.collections.LngVector;
-import com.booleworks.logicng.formulas.Formula;
 import com.booleworks.logicng.formulas.FormulaFactory;
 import com.booleworks.logicng.formulas.InternalAuxVarType;
 import com.booleworks.logicng.formulas.Literal;
 import com.booleworks.logicng.formulas.Variable;
-import com.booleworks.logicng.propositions.Proposition;
-import com.booleworks.logicng.solvers.sat.LngCoreSolver;
-
-import java.util.List;
 
 /**
  * The result of an encoding.
@@ -87,34 +82,4 @@ default Variable newCnfVariable() {
      * @return the {@link FormulaFactory}
      */
     FormulaFactory getFactory();
-
-    /**
-     * Returns the result. The result might not be complete if the encoding
-     * result materialize its input as formulas on the formula factory only
-     * partially. E.g. the encoding result for a SAT Solver does not materialize
-     * any formulas.
-     * @return the result
-     */
-    List<Formula> getResult();
-
-    /**
-     * Constructs a new result which stores the result in a formula.
-     * @param f the formula factory
-     * @return the result
-     */
-    static EncodingResultFF forFormulaFactory(final FormulaFactory f) {
-        return new EncodingResultFF(f);
-    }
-
-    /**
-     * Constructs a new result which adds the result directly to a given solver.
-     * @param solver      the solver
-     * @param proposition the original proposition of the cardinality constraint
-     * @return the result
-     */
-    static EncodingResultSolver forSatSolver(final FormulaFactory f, final LngCoreSolver solver,
-                                             final Proposition proposition) {
-        return new EncodingResultSolver(f, solver, proposition);
-    }
-
 }
diff --git a/.../src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultFF.java b/.../src/main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultFF.java
@@ -23,7 +23,7 @@ public final class EncodingResultFF implements EncodingResult {
      * {@link FormulaFactory}.
      * @param f the formula factory
      */
-    EncodingResultFF(final FormulaFactory f) {
+    public EncodingResultFF(final FormulaFactory f) {
         this.f = f;
         result = new ArrayList<>();
     }
@@ -47,7 +47,6 @@ public Variable newVariable(final String auxType) {
         return f.newAuxVariable(auxType);
     }
 
-    @Override
     public List<Formula> getResult() {
         return result;
     }

diff --git a/.../main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultSolver.java b/.../main/java/com/booleworks/logicng/datastructures/encodingresult/EncodingResultSolver.java
@@ -2,16 +2,12 @@
 
 import com.booleworks.logicng.collections.LngIntVector;
 import com.booleworks.logicng.collections.LngVector;
-import com.booleworks.logicng.formulas.Formula;
 import com.booleworks.logicng.formulas.FormulaFactory;
 import com.booleworks.logicng.formulas.Literal;
 import com.booleworks.logicng.formulas.Variable;
 import com.booleworks.logicng.propositions.Proposition;
 import com.booleworks.logicng.solvers.sat.LngCoreSolver;
 
-import java.util.ArrayList;
-import java.util.List;
-
 /**
  * An encoding result that writes the encoding directly to a solver.
  */
@@ -25,7 +21,7 @@ public final class EncodingResultSolver implements EncodingResult {
      * @param solver      the solver instance
      * @param proposition the original proposition
      */
-    EncodingResultSolver(final FormulaFactory f, final LngCoreSolver solver, final Proposition proposition) {
+    public EncodingResultSolver(final FormulaFactory f, final LngCoreSolver solver, final Proposition proposition) {
         this.f = f;
         this.solver = solver;
         this.proposition = proposition;
@@ -77,11 +73,6 @@ public FormulaFactory getFactory() {
         return f;
     }
 
-    @Override
-    public List<Formula> getResult() {
-        return new ArrayList<>();
-    }
-
     /**
      * Returns the original proposition.
      * @return the original proposition

diff --git a/core/src/main/java/com/booleworks/logicng/encodings/CcEncoder.java b/core/src/main/java/com/booleworks/logicng/encodings/CcEncoder.java
@@ -65,7 +65,7 @@ public static List<Formula> encode(final FormulaFactory f, final CardinalityCons
      */
     public static List<Formula> encode(final FormulaFactory f, final CardinalityConstraint cc,
                                        final EncoderConfig config) {
-        final EncodingResultFF result = EncodingResult.forFormulaFactory(f);
+        final EncodingResultFF result = new EncodingResultFF(f);
         encodeConstraint(cc, result, config);
         return Collections.unmodifiableList(result.getResult());
     }
@@ -95,10 +95,10 @@ public static void encode(final CardinalityConstraint cc, final EncodingResult r
      * @param cc the cardinality constraint
      * @return the encoding of the constraint and the incremental data
      */
-    public static Pair<List<Formula>, CcIncrementalData> encodeIncremental(final FormulaFactory f,
-                                                                           final CardinalityConstraint cc) {
-        final EncodingResultFF result = EncodingResult.forFormulaFactory(f);
-        final CcIncrementalData incData = encodeIncremental(cc, result);
+    public static Pair<List<Formula>, CcIncrementalData<EncodingResultFF>> encodeIncremental(final FormulaFactory f,
+                                                                                             final CardinalityConstraint cc) {
+        final EncodingResultFF result = new EncodingResultFF(f);
+        final CcIncrementalData<EncodingResultFF> incData = encodeIncremental(cc, result);
         return new Pair<>(Collections.unmodifiableList(result.getResult()), incData);
     }
 
@@ -109,10 +109,10 @@ public static Pair<List<Formula>, CcIncrementalData> encodeIncremental(final For
      * @param config the configuration for the encoder
      * @return the encoding of the constraint and the incremental data
      */
-    public static Pair<List<Formula>, CcIncrementalData>
+    public static Pair<List<Formula>, CcIncrementalData<EncodingResultFF>>
     encodeIncremental(final FormulaFactory f, final CardinalityConstraint cc, final EncoderConfig config) {
-        final EncodingResultFF result = EncodingResult.forFormulaFactory(f);
-        final CcIncrementalData incData = encodeIncremental(cc, result, config);
+        final EncodingResultFF result = new EncodingResultFF(f);
+        final CcIncrementalData<EncodingResultFF> incData = encodeIncremental(cc, result, config);
         return new Pair<>(Collections.unmodifiableList(result.getResult()), incData);
     }
 
@@ -122,7 +122,8 @@ public static Pair<List<Formula>, CcIncrementalData> encodeIncremental(final For
      * @param result the result of the encoding
      * @return the incremental data
      */
-    public static CcIncrementalData encodeIncremental(final CardinalityConstraint cc, final EncodingResult result) {
+    public static <T extends EncodingResult> CcIncrementalData<T> encodeIncremental(final CardinalityConstraint cc,
+                                                                                    final T result) {
         return encodeIncrementalConstraint(cc, result, null);
     }
 
@@ -133,14 +134,14 @@ public static CcIncrementalData encodeIncremental(final CardinalityConstraint cc
      * @param config the configuration for the encoder
      * @return the incremental data
      */
-    public static CcIncrementalData encodeIncremental(final CardinalityConstraint cc, final EncodingResult result,
-                                                      final EncoderConfig config) {
+    public static <T extends EncodingResult> CcIncrementalData<T> encodeIncremental(final CardinalityConstraint cc,
+                                                                                    final T result,
+                                                                                    final EncoderConfig config) {
         return encodeIncrementalConstraint(cc, result, config);
     }
 
-    protected static CcIncrementalData encodeIncrementalConstraint(final CardinalityConstraint cc,
-                                                                   final EncodingResult result,
-                                                                   final EncoderConfig initConfig) {
+    protected static <T extends EncodingResult> CcIncrementalData<T> encodeIncrementalConstraint(
+            final CardinalityConstraint cc, final T result, final EncoderConfig initConfig) {
         final var config = initConfig != null ? initConfig
                                               : (EncoderConfig) result.getFactory()
                                                       .configurationFor(ConfigurationType.ENCODER);
@@ -279,8 +280,10 @@ protected static void amk(final EncodingResult result, final EncoderConfig confi
         }
     }
 
-    protected static CcIncrementalData amkIncremental(final EncodingResult result, final EncoderConfig config,
-                                                      final Variable[] vars, final int rhs) {
+    protected static <T extends EncodingResult> CcIncrementalData<T> amkIncremental(final T result,
+                                                                                    final EncoderConfig config,
+                                                                                    final Variable[] vars,
+                                                                                    final int rhs) {
         if (rhs < 0) {
             throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs);
         }
@@ -344,8 +347,10 @@ protected static void alk(final EncodingResult result, final EncoderConfig confi
         }
     }
 
-    protected static CcIncrementalData alkIncremental(final EncodingResult result, final EncoderConfig config,
-                                                      final Variable[] vars, final int rhs) {
+    protected static <T extends EncodingResult> CcIncrementalData<T> alkIncremental(final T result,
+                                                                                    final EncoderConfig config,
+                                                                                    final Variable[] vars,
+                                                                                    final int rhs) {
         if (rhs < 0) {
             throw new IllegalArgumentException("Invalid right hand side of cardinality constraint: " + rhs);
         }

diff --git a/core/src/main/java/com/booleworks/logicng/encodings/CcIncrementalData.java b/core/src/main/java/com/booleworks/logicng/encodings/CcIncrementalData.java
@@ -28,12 +28,9 @@
 
 import com.booleworks.logicng.collections.LngVector;
 import com.booleworks.logicng.datastructures.encodingresult.EncodingResult;
-import com.booleworks.logicng.formulas.Formula;
 import com.booleworks.logicng.formulas.FormulaFactory;
 import com.booleworks.logicng.formulas.Literal;
 
-import java.util.List;
-
 /**
  * Incremental data for an at-most-k cardinality constraint. When an at-most-k
  * cardinality constraint is constructed, it is possible to save incremental
@@ -42,8 +39,8 @@
  * @version 3.0.0
  * @since 1.1
  */
-public final class CcIncrementalData {
-    private final EncodingResult result;
+public final class CcIncrementalData<T extends EncodingResult> {
+    private final T result;
     private final EncoderConfig.AmkEncoder amkEncoder;
     private final EncoderConfig.AlkEncoder alkEncoder;
     private final LngVector<? extends Literal> vector1;
@@ -62,7 +59,7 @@ public final class CcIncrementalData {
      * @param vector2    the second internal vector
      * @param mod        the modulo value
      */
-    public CcIncrementalData(final EncodingResult result, final EncoderConfig.AmkEncoder amkEncoder, final int rhs,
+    public CcIncrementalData(final T result, final EncoderConfig.AmkEncoder amkEncoder, final int rhs,
                              final LngVector<? extends Literal> vector1, final LngVector<? extends Literal> vector2,
                              final int mod) {
         this.result = result;
@@ -82,7 +79,7 @@ public CcIncrementalData(final EncodingResult result, final EncoderConfig.AmkEnc
      * @param rhs     the current right-hand-side
      * @param vector1 the first internal vector
      */
-    public CcIncrementalData(final EncodingResult result, final EncoderConfig.AmkEncoder encoder, final int rhs,
+    public CcIncrementalData(final T result, final EncoderConfig.AmkEncoder encoder, final int rhs,
                              final LngVector<? extends Literal> vector1) {
         this(result, encoder, rhs, vector1, null, -1);
     }
@@ -98,7 +95,7 @@ public CcIncrementalData(final EncodingResult result, final EncoderConfig.AmkEnc
      * @param vector2    the second internal vector
      * @param mod        the modulo value
      */
-    public CcIncrementalData(final EncodingResult result, final EncoderConfig.AlkEncoder alkEncoder, final int rhs,
+    public CcIncrementalData(final T result, final EncoderConfig.AlkEncoder alkEncoder, final int rhs,
                              final int nVars,
                              final LngVector<? extends Literal> vector1, final LngVector<? extends Literal> vector2,
                              final int mod) {
@@ -122,20 +119,17 @@ public CcIncrementalData(final EncodingResult result, final EncoderConfig.AlkEnc
      * @param nVars      the number of variables
      * @param vector1    the first internal vector
      */
-    public CcIncrementalData(final EncodingResult result, final EncoderConfig.AlkEncoder alkEncoder, final int rhs,
+    public CcIncrementalData(final T result, final EncoderConfig.AlkEncoder alkEncoder, final int rhs,
                              final int nVars, final LngVector<? extends Literal> vector1) {
         this(result, alkEncoder, rhs, nVars, vector1, null, -1);
     }
 
     /**
-     * Tightens the upper bound of an at-most-k constraint and returns the
-     * resulting formula.
+     * Tightens the upper bound of an at-most-k constraint.
      * @param rhs the new upperBound
-     * @return the incremental encoding of the new upper bound
      */
-    public List<Formula> newUpperBound(final int rhs) {
+    public void newUpperBound(final int rhs) {
         computeUbConstraint(result, rhs);
-        return result.getResult();
     }
 
     /**
@@ -201,14 +195,11 @@ private void computeUbConstraint(final EncodingResult result, final int rhs) {
     }
 
     /**
-     * Tightens the lower bound of an at-least-k constraint and returns the
-     * resulting formula.
+     * Tightens the lower bound of an at-least-k constraint.
      * @param rhs the new upperBound
-     * @return the incremental encoding of the new lower bound
      */
-    public List<Formula> newLowerBound(final int rhs) {
+    public void newLowerBound(final int rhs) {
         computeLbConstraint(result, rhs);
-        return result.getResult();
     }
 
     /**
@@ -283,6 +274,14 @@ public int getCurrentRhs() {
         return currentRhs;
     }
 
+    /**
+     * Returns the {@link EncodingResult} that is used as the target for the encodings.
+     * @return the {@link EncodingResult} that is used as the target for the encodings
+     */
+    public T getEncodingResult() {
+        return result;
+    }
+
     @Override
     public String toString() {
         return "CcIncrementalData{" +

diff --git a/core/src/main/java/com/booleworks/logicng/encodings/PbEncoder.java b/core/src/main/java/com/booleworks/logicng/encodings/PbEncoder.java
@@ -39,7 +39,7 @@ private PbEncoder() {
      * @return the CNF encoding of the pseudo-Boolean constraint
      */
     public static List<Formula> encode(final FormulaFactory f, final PbConstraint constraint) {
-        final EncodingResultFF result = EncodingResult.forFormulaFactory(f);
+        final EncodingResultFF result = new EncodingResultFF(f);
         encode(constraint, result, null);
         return Collections.unmodifiableList(result.getResult());
     }
@@ -62,7 +62,7 @@ public static void encode(final PbConstraint constraint, final EncodingResult re
      */
     public static List<Formula> encode(final FormulaFactory f, final PbConstraint constraint,
                                        final EncoderConfig config) {
-        final EncodingResult result = EncodingResult.forFormulaFactory(f);
+        final EncodingResultFF result = new EncodingResultFF(f);
         encode(constraint, result, config);
         return Collections.unmodifiableList(result.getResult());
     }

diff --git a/core/src/main/java/com/booleworks/logicng/encodings/cc/CcCardinalityNetwork.java b/core/src/main/java/com/booleworks/logicng/encodings/cc/CcCardinalityNetwork.java
@@ -65,8 +65,9 @@ public static void amk(final EncodingResult result, final Variable[] vars, final
         }
     }
 
-    public static CcIncrementalData amkForIncremental(final EncodingResult result, final Variable[] vars,
-                                                      final int rhs) {
+    public static <T extends EncodingResult> CcIncrementalData<T> amkForIncremental(final T result,
+                                                                                    final Variable[] vars,
+                                                                                    final int rhs) {
         final FormulaFactory f = result.getFactory();
         final LngVector<Literal> input = new LngVector<>();
         final LngVector<Literal> output = new LngVector<>();
@@ -76,7 +77,7 @@ public static CcIncrementalData amkForIncremental(final EncodingResult result, f
         CcSorting.sort(f, rhs + 1, input, result, output, CcSorting.ImplicationDirection.INPUT_TO_OUTPUT);
         assert output.size() > rhs;
         result.addClause(output.get(rhs).negate(f));
-        return new CcIncrementalData(result, EncoderConfig.AmkEncoder.CARDINALITY_NETWORK, rhs, output);
+        return new CcIncrementalData<>(result, EncoderConfig.AmkEncoder.CARDINALITY_NETWORK, rhs, output);
     }
 
     public static void alk(final EncodingResult result, final Variable[] vars, final int rhs) {
@@ -103,8 +104,9 @@ public static void alk(final EncodingResult result, final Variable[] vars, final
         }
     }
 
-    public static CcIncrementalData alkForIncremental(final EncodingResult result, final Variable[] vars,
-                                                      final int rhs) {
+    public static <T extends EncodingResult> CcIncrementalData<T> alkForIncremental(final T result,
+                                                                                    final Variable[] vars,
+                                                                                    final int rhs) {
         final FormulaFactory f = result.getFactory();
         final LngVector<Literal> input = new LngVector<>();
         final LngVector<Literal> output = new LngVector<>();
@@ -115,7 +117,7 @@ public static CcIncrementalData alkForIncremental(final EncodingResult result, f
         CcSorting.sort(f, newRhs + 1, input, result, output, CcSorting.ImplicationDirection.INPUT_TO_OUTPUT);
         assert output.size() > newRhs;
         result.addClause(output.get(newRhs).negate(f));
-        return new CcIncrementalData(result, EncoderConfig.AlkEncoder.CARDINALITY_NETWORK, rhs, vars.length, output);
+        return new CcIncrementalData<>(result, EncoderConfig.AlkEncoder.CARDINALITY_NETWORK, rhs, vars.length, output);
     }
 
     public static void exk(final EncodingResult result, final Variable[] vars, final int rhs) {