confl.updateSlack() is now called inside confl.setDecisionLevel()

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

@@ -576,6 +576,8 @@ public class ConflictMap extends MapPb implements IConflict {
 
     public void setDecisionLevel(int dl) {
         assert dl <= this.currentLevel;
+        if (dl < this.currentLevel)
+            this.updateSlack(dl);
         this.currentLevel = dl;
     }
 

org.sat4j.pb/src/main/java/org/sat4j/pb/core/PBSolverCP.java

@@ -137,6 +137,7 @@ public class PBSolverCP extends PBSolver {
         int litImplied = this.trail.last();
         int currentLevel = this.voc.getLevel(litImplied);
         IConflict confl = chooseConflict((PBConstr) myconfl, currentLevel);
+        confl.setDecisionLevel(currentLevel);
         assert confl.slackConflict().signum() < 0;
         while (!confl.isUnsat() && !confl.isAssertive(currentLevel)) {
             if (!this.undertimeout) {
@@ -144,7 +145,6 @@ public class PBSolverCP extends PBSolver {
             }
             PBConstr constraint = (PBConstr) this.voc.getReason(litImplied);
             // result of the resolution is in the conflict (confl)
-            confl.setDecisionLevel(currentLevel);
             confl.resolve(constraint, litImplied, this);
             updateNumberOfReductions(confl);
             assert confl.slackConflict().signum() < 0;
@@ -160,10 +160,10 @@ public class PBSolverCP extends PBSolver {
             if (this.voc.getLevel(litImplied) != currentLevel) {
                 this.trailLim.pop();
                 slistener.backtracking(LiteralsUtils.toDimacs(litImplied));
-                confl.updateSlack(this.voc.getLevel(litImplied));
             }
             assert this.voc.getLevel(litImplied) <= currentLevel;
             currentLevel = this.voc.getLevel(litImplied);
+            confl.setDecisionLevel(currentLevel);
             assert confl.slackIsCorrect(currentLevel);
             assert currentLevel == decisionLevel();
             assert litImplied > 1;
@@ -212,8 +212,8 @@ public class PBSolverCP extends PBSolver {
                 + this.getClass().getName() + ")\n"
                 + (this.noRemove ? ""
                         : prefix + " - Removing satisfied literals at a higher level before CP \n")
-                + (this.skipAllow ? prefix
-                        + " - Skipping as much as possible cutting planes during analysis conflict- Jan Elffers's algorithm \n"
+                + (this.skipAllow
+                        ? prefix + " - Skipping as much as possible cutting planes during analysis conflict- Jan Elffers's algorithm \n"
                         : "")
                 + prefix + " - " + autoDivisionStrategy + "\n" + prefix + " - "
                 + postprocess + "\n" + prefix + " - " + conflictFactory + "\n"

org.sat4j.pb/src/main/java/org/sat4j/pb/tools/InprocCardConstrLearningSolver.java

@@ -168,6 +168,7 @@ public class InprocCardConstrLearningSolver extends PBSolverCP {
         int litImplied = this.trail.last();
         int currentLevel = this.voc.getLevel(litImplied);
         IConflict confl = chooseConflict((PBConstr) myconfl, currentLevel);
+        confl.setDecisionLevel(currentLevel);
         assert confl.slackConflict().signum() < 0;
         while (!confl.isAssertive(currentLevel)) {
             if (!this.undertimeout) {
@@ -182,7 +183,6 @@ public class InprocCardConstrLearningSolver extends PBSolverCP {
                 constraint = (PBConstr) extendedConstr;
             }
             // result of the resolution is in the conflict (confl)
-            confl.setDecisionLevel(currentLevel);
             confl.resolve(constraint, litImplied, this);
             updateNumberOfReductions(confl);
             assert confl.slackConflict().signum() < 0;
@@ -199,10 +199,10 @@ public class InprocCardConstrLearningSolver extends PBSolverCP {
             if (this.voc.getLevel(litImplied) != currentLevel) {
                 this.trailLim.pop();
                 slistener.backtracking(LiteralsUtils.toDimacs(litImplied));
-                confl.updateSlack(this.voc.getLevel(litImplied));
             }
             assert this.voc.getLevel(litImplied) <= currentLevel;
             currentLevel = this.voc.getLevel(litImplied);
+            confl.setDecisionLevel(currentLevel);
             assert confl.slackIsCorrect(currentLevel);
             assert currentLevel == decisionLevel();
             assert litImplied > 1;