Using NullObject for tautological PB constraints.

org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/IDataStructurePB.java

@@ -31,11 +31,91 @@ package org.sat4j.pb.constraints.pb;
 
 import java.math.BigInteger;
 
+import org.sat4j.minisat.core.ILits;
 import org.sat4j.minisat.core.VarActivityListener;
 import org.sat4j.specs.IVec;
 import org.sat4j.specs.IVecInt;
 
 public interface IDataStructurePB {
+
+    IDataStructurePB TAUTOLOGY = new IDataStructurePB() {
+
+        @Override
+        public int size() {
+            return 0;
+        }
+
+        @Override
+        public BigInteger saturation() {
+            return BigInteger.ZERO;
+        }
+
+        @Override
+        public int reduceCoeffsByPower2() {
+            return 0;
+        }
+
+        @Override
+        public boolean isLongSufficient() {
+            return true;
+        }
+
+        @Override
+        public boolean isCardinality() {
+            return true;
+        }
+
+        @Override
+        public BigInteger getDegree() {
+            return BigInteger.ZERO;
+        }
+
+        @Override
+        public BigInteger getCardDegree() {
+            return BigInteger.ZERO;
+        }
+
+        @Override
+        public int getAssertiveLiteral() {
+            return ILits.UNDEFINED;
+        }
+
+        @Override
+        public BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
+                BigInteger degreeCons, BigInteger coefMult) {
+            throw new UnsupportedOperationException();
+        }
+
+        @Override
+        public BigInteger cuttingPlane(int[] lits, BigInteger[] reducedCoefs,
+                BigInteger deg) {
+            throw new UnsupportedOperationException();
+        }
+
+        @Override
+        public BigInteger cuttingPlane(PBConstr cpb, BigInteger degreeCons,
+                BigInteger[] reducedCoefs, BigInteger coefMult,
+                VarActivityListener val) {
+            throw new UnsupportedOperationException();
+        }
+
+        @Override
+        public BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,
+                BigInteger[] reducedCoefs, VarActivityListener val) {
+            throw new UnsupportedOperationException();
+        }
+
+        @Override
+        public void buildConstraintFromMapPb(int[] resLits,
+                BigInteger[] resCoefs) {
+        }
+
+        @Override
+        public void buildConstraintFromConflict(IVecInt resLits,
+                IVec<BigInteger> resCoefs) {
+        }
+    };
+
     BigInteger saturation();
 
     BigInteger cuttingPlane(PBConstr cpb, BigInteger deg,

org.sat4j.pb/src/main/java/org/sat4j/pb/constraints/pb/Pseudos.java

@@ -51,8 +51,8 @@ public abstract class Pseudos {
         ps.copyTo(lits);
         BigInteger[] bc = new BigInteger[bigCoefs.size()];
         bigCoefs.copyTo(bc);
-        BigInteger bigDegree = Pseudos.niceCheckedParametersForCompetition(
-                lits, bc, moreThan, bigDeg);
+        BigInteger bigDegree = Pseudos.niceCheckedParametersForCompetition(lits,
+                bc, moreThan, bigDeg);
 
         IDataStructurePB mpb = new MapPb(voc.nVars() * 2 + 2);
         if (bigDegree.signum() > 0) {
@@ -100,12 +100,12 @@ public abstract class Pseudos {
             ILits voc) throws ContradictionException {
         // Ajouter les simplifications quand la structure sera d?finitive
         if (ps.size() == 0) {
-            if (moreThan && bigDeg.signum() > 0 || !moreThan
-                    && bigDeg.signum() < 0) {
+            if (moreThan && bigDeg.signum() > 0
+                    || !moreThan && bigDeg.signum() < 0) {
                 throw new ContradictionException("Creating Empty clause ?");
             }
             // ignoring tautological constraint
-            return null;
+            return IDataStructurePB.TAUTOLOGY;
         }
         if (ps.size() != bigCoefs.size()) {
             throw new IllegalArgumentException(
@@ -121,8 +121,8 @@ public abstract class Pseudos {
             throws ContradictionException {
         // Ajouter les simplifications quand la structure sera d?finitive
         if (ps.length == 0) {
-            if (moreThan && bigDeg.signum() > 0 || !moreThan
-                    && bigDeg.signum() < 0) {
+            if (moreThan && bigDeg.signum() > 0
+                    || !moreThan && bigDeg.signum() < 0) {
                 throw new ContradictionException("Creating Empty clause ?");
             }
             // ignoring tautological constraint
@@ -149,7 +149,8 @@ public abstract class Pseudos {
         return BigInteger.valueOf(i);
     }
 
-    public static ObjectiveFunction normalizeObjective(ObjectiveFunction initial) {
+    public static ObjectiveFunction normalizeObjective(
+            ObjectiveFunction initial) {
         IVec<BigInteger> initCoeffs = initial.getCoeffs();
         IVecInt initLits = initial.getVars();
         assert initCoeffs.size() == initLits.size();