special CCResult is now a general EncodingResult

logic-ng · Jun 21, 2016 · fc4c704 · fc4c704
1 parent 7eac5fe
commit fc4c704
Show file tree

Hide file tree

Showing 30 changed files with 161 additions and 106 deletions.
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCALKCardinalityNetwork.java b/src/main/java/org/logicng/cardinalityconstraints/CCALKCardinalityNetwork.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -48,7 +49,7 @@ final class CCALKCardinalityNetwork implements CCAtLeastK {
   }
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     cardinalityNetwork.buildALK(result, vars, rhs);
   }
 
@@ -58,7 +59,7 @@ public void build(final CCResult result, final Variable[] vars, int rhs) {
    * @param vars   the variables
    * @param rhs    the right-hand side
    */
-  void buildForIncremental(final CCResult result, final Variable[] vars, int rhs) {
+  void buildForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
     cardinalityNetwork.buildALKForIncremental(result, vars, rhs);
   }
 

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCALKModularTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCALKModularTotalizer.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Variable;
 
@@ -50,7 +51,7 @@ final class CCALKModularTotalizer implements CCAtLeastK {
   }
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     this.totalizer.buildALK(result, vars, rhs);
   }
 

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCALKTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCALKTotalizer.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -48,7 +49,7 @@ final class CCALKTotalizer implements CCAtLeastK {
   }
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     this.totalizer.buildALK(result, vars, rhs);
   }
 

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMKCardinalityNetwork.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMKCardinalityNetwork.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -48,7 +49,7 @@ final class CCAMKCardinalityNetwork implements CCAtMostK {
   }
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     cardinalityNetwork.buildAMK(result, vars, rhs);
   }
 
@@ -63,7 +64,7 @@ public CCIncrementalData incrementalData() {
    * @param vars   the variables
    * @param rhs    the right-hand side
    */
-  void buildForIncremental(final CCResult result, final Variable[] vars, int rhs) {
+  void buildForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
     cardinalityNetwork.buildAMKForIncremental(result, vars, rhs);
   }
 

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMKModularTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMKModularTotalizer.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Variable;
 
@@ -50,7 +51,7 @@ final class CCAMKModularTotalizer implements CCAtMostK {
   }
 
   @Override
-  public void build(final CCResult result, Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, Variable[] vars, int rhs) {
     this.totalizer.buildAMK(result, vars, rhs);
   }
 

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMKTotalizer.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMKTotalizer.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -49,7 +50,7 @@ final class CCAMKTotalizer implements CCAtMostK {
 
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     this.totalizer.buildAMK(result, vars, rhs);
   }
 

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOBimander.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOBimander.java
@@ -52,6 +52,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
@@ -62,7 +63,7 @@
  */
 final class CCAMOBimander implements CCAtMostOne {
 
-  private CCResult result;
+  private EncodingResult result;
   private LNGVector<LNGVector<Literal>> groups;
   private LNGVector<Literal> bits;
   private int numberOfBits;
@@ -80,7 +81,7 @@ final class CCAMOBimander implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     this.result = result;
     this.encodeIntern(new LNGVector<Literal>(vars));

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOBinary.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOBinary.java
@@ -51,6 +51,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -70,7 +71,7 @@ final class CCAMOBinary implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     final int numberOfBits = (int) Math.ceil((Math.log(vars.length) / Math.log(2)));
     final int twoPowNBits = (int) Math.pow(2, numberOfBits);

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOCommander.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOCommander.java
@@ -52,6 +52,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
@@ -62,7 +63,7 @@
  */
 final class CCAMOCommander implements CCAtMostOne {
 
-  private CCResult result;
+  private EncodingResult result;
   private int k;
   private LNGVector<Literal> literals;
   private LNGVector<Literal> nextLiterals;
@@ -80,7 +81,7 @@ final class CCAMOCommander implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     this.result = result;
     this.currentLiterals.clear();

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOLadder.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOLadder.java
@@ -49,6 +49,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -65,7 +66,7 @@ final class CCAMOLadder implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     final Variable[] seqAuxiliary = new Variable[vars.length - 1];
     for (int i = 0; i < vars.length - 1; i++)

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMONested.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMONested.java
@@ -52,6 +52,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
@@ -63,7 +64,7 @@
 final class CCAMONested implements CCAtMostOne {
 
   private int groupSize;
-  private CCResult result;
+  private EncodingResult result;
 
   /**
    * Constructs the nested AMO encoder.
@@ -74,7 +75,7 @@ final class CCAMONested implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     this.result = result;
     this.encodeIntern(new LNGVector<Literal>(vars));

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOProduct.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOProduct.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -37,7 +38,7 @@
  */
 final class CCAMOProduct implements CCAtMostOne {
   private final int recursiveBound;
-  private CCResult result;
+  private EncodingResult result;
 
   /**
    * Constructs the naive AMO encoder.
@@ -47,7 +48,7 @@ final class CCAMOProduct implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     this.result = result;
     this.productRec(vars);

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAMOPure.java b/src/main/java/org/logicng/cardinalityconstraints/CCAMOPure.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -46,7 +47,7 @@ final class CCAMOPure implements CCAtMostOne {
   }
 
   @Override
-  public void build(final CCResult result, final Variable... vars) {
+  public void build(final EncodingResult result, final Variable... vars) {
     result.reset();
     for (int i = 0; i < vars.length; i++)
       for (int j = i + 1; j < vars.length; j++)

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAtLeastK.java b/src/main/java/org/logicng/cardinalityconstraints/CCAtLeastK.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -43,7 +44,7 @@ interface CCAtLeastK {
    * @param rhs    the right hand side {@code k} of the constraint
    * @throws IllegalArgumentException if the right hand side of the cardinality constraint is negative
    */
-  void build(final CCResult result, final Variable[] vars, int rhs);
+  void build(final EncodingResult result, final Variable[] vars, int rhs);
 
   /**
    * Returns the incremental data for the current encoded constraint.

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAtMostK.java b/src/main/java/org/logicng/cardinalityconstraints/CCAtMostK.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -44,7 +45,7 @@ interface CCAtMostK {
    * @param rhs    the right hand side {@code k} of the constraint
    * @throws IllegalArgumentException if the right hand side of the cardinality constraint is negative
    */
-  void build(final CCResult result, final Variable[] vars, int rhs);
+  void build(final EncodingResult result, final Variable[] vars, int rhs);
 
   /**
    * Returns the incremental data for the current encoded constraint.

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCAtMostOne.java b/src/main/java/org/logicng/cardinalityconstraints/CCAtMostOne.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -42,5 +43,5 @@ interface CCAtMostOne {
    * @param result the result for the encoding
    * @param vars   the variables {@code var_1 ... var_n}
    */
-  void build(final CCResult result, final Variable... vars);
+  void build(final EncodingResult result, final Variable... vars);
 }
diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCCardinalityNetworks.java b/src/main/java/org/logicng/cardinalityconstraints/CCCardinalityNetworks.java
@@ -52,6 +52,7 @@
 package org.logicng.cardinalityconstraints;
 
 import org.logicng.collections.LNGVector;
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Literal;
 import org.logicng.formulas.Variable;
 
@@ -76,7 +77,7 @@ final class CCCardinalityNetworks {
     this.sorting = new CCSorting();
   }
 
-  void buildAMK(final CCResult result, final Variable[] vars, int rhs) {
+  void buildAMK(final EncodingResult result, final Variable[] vars, int rhs) {
     result.reset();
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();
@@ -96,7 +97,7 @@ void buildAMK(final CCResult result, final Variable[] vars, int rhs) {
     }
   }
 
-  void buildAMKForIncremental(final CCResult result, final Variable[] vars, int rhs) {
+  void buildAMKForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();
     for (final Variable var : vars)
@@ -107,7 +108,7 @@ void buildAMKForIncremental(final CCResult result, final Variable[] vars, int rh
     this.incData = new CCIncrementalData(result, CCConfig.AMK_ENCODER.CARDINALITY_NETWORK, rhs, output);
   }
 
-  void buildALK(final CCResult result, final Variable[] vars, int rhs) {
+  void buildALK(final EncodingResult result, final Variable[] vars, int rhs) {
     result.reset();
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();
@@ -128,7 +129,7 @@ void buildALK(final CCResult result, final Variable[] vars, int rhs) {
     }
   }
 
-  void buildALKForIncremental(final CCResult result, final Variable[] vars, int rhs) {
+  void buildALKForIncremental(final EncodingResult result, final Variable[] vars, int rhs) {
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();
     for (final Variable var : vars)
@@ -140,7 +141,7 @@ void buildALKForIncremental(final CCResult result, final Variable[] vars, int rh
     this.incData = new CCIncrementalData(result, CCConfig.ALK_ENCODER.CARDINALITY_NETWORK, rhs, vars.length, output);
   }
 
-  void buildEXK(final CCResult result, final Variable[] vars, int rhs) {
+  void buildEXK(final EncodingResult result, final Variable[] vars, int rhs) {
     result.reset();
     final LNGVector<Literal> input = new LNGVector<>();
     final LNGVector<Literal> output = new LNGVector<>();

diff --git a/src/main/java/org/logicng/cardinalityconstraints/CCEXKCardinalityNetwork.java b/src/main/java/org/logicng/cardinalityconstraints/CCEXKCardinalityNetwork.java
@@ -28,6 +28,7 @@
 
 package org.logicng.cardinalityconstraints;
 
+import org.logicng.datastructures.EncodingResult;
 import org.logicng.formulas.Variable;
 
 /**
@@ -48,7 +49,7 @@ final class CCEXKCardinalityNetwork implements CCAtMostK {
   }
 
   @Override
-  public void build(final CCResult result, final Variable[] vars, int rhs) {
+  public void build(final EncodingResult result, final Variable[] vars, int rhs) {
     cardinalityNetwork.buildEXK(result, vars, rhs);
   }