Commit a829c090 authored by Daniel Le Berre's avatar Daniel Le Berre

Make explicit call to IConflict.setDecisionLevel()

parent b4a97f9e
Pipeline #3234 failed with stages
in 45 minutes and 15 seconds
...@@ -574,6 +574,11 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -574,6 +574,11 @@ public class ConflictMap extends MapPb implements IConflict {
return isImplyingLiteral(slack, dl); return isImplyingLiteral(slack, dl);
} }
public void setDecisionLevel(int dl) {
assert dl <= this.currentLevel;
this.currentLevel = dl;
}
/** /**
* tests if the conflict is unsatisfiable * tests if the conflict is unsatisfiable
* *
...@@ -586,7 +591,8 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -586,7 +591,8 @@ public class ConflictMap extends MapPb implements IConflict {
// given the slack already computed, tests if a literal could be implied at // given the slack already computed, tests if a literal could be implied at
// a particular level // a particular level
// uses the byLevel data structure to parse each literal by decision level // uses the byLevel data structure to parse each literal by decision level
private boolean isImplyingLiteral(BigInteger slack, int currentDecisionLevel) { private boolean isImplyingLiteral(BigInteger slack,
int currentDecisionLevel) {
// unassigned literals are tried first // unassigned literals are tried first
int unassigned = levelToIndex(-1); int unassigned = levelToIndex(-1);
int lit; int lit;
......
...@@ -54,6 +54,8 @@ public interface IConflict extends IDataStructurePB { ...@@ -54,6 +54,8 @@ public interface IConflict extends IDataStructurePB {
boolean isAssertive(int dl); boolean isAssertive(int dl);
void setDecisionLevel(int dl);
boolean isUnsat(); boolean isUnsat();
/** /**
......
...@@ -54,6 +54,7 @@ public class PostProcessToCard implements IPostProcess { ...@@ -54,6 +54,7 @@ public class PostProcessToCard implements IPostProcess {
&& (!conflictMap.degree.equals(BigInteger.ONE))) { && (!conflictMap.degree.equals(BigInteger.ONE))) {
int lit, litLevel, ilit; int lit, litLevel, ilit;
BigInteger coefLit; BigInteger coefLit;
conflictMap.setDecisionLevel(dl);
if (conflictMap.assertiveLiteral != -1) { if (conflictMap.assertiveLiteral != -1) {
conflictMap.assertiveLiteral = this.chooseAssertiveLiteral(dl, conflictMap.assertiveLiteral = this.chooseAssertiveLiteral(dl,
conflictMap); conflictMap);
......
...@@ -51,6 +51,7 @@ public class PostProcessToClause implements IPostProcess { ...@@ -51,6 +51,7 @@ public class PostProcessToClause implements IPostProcess {
if (conflictMap.isAssertive(dl) if (conflictMap.isAssertive(dl)
&& (!conflictMap.degree.equals(BigInteger.ONE))) { && (!conflictMap.degree.equals(BigInteger.ONE))) {
int litLevel, ilit; int litLevel, ilit;
conflictMap.setDecisionLevel(dl);
if (conflictMap.assertiveLiteral != -1) { if (conflictMap.assertiveLiteral != -1) {
conflictMap.assertiveLiteral = this.chooseAssertiveLiteral(dl, conflictMap.assertiveLiteral = this.chooseAssertiveLiteral(dl,
conflictMap); conflictMap);
......
...@@ -144,6 +144,7 @@ public class PBSolverCP extends PBSolver { ...@@ -144,6 +144,7 @@ public class PBSolverCP extends PBSolver {
} }
PBConstr constraint = (PBConstr) this.voc.getReason(litImplied); PBConstr constraint = (PBConstr) this.voc.getReason(litImplied);
// result of the resolution is in the conflict (confl) // result of the resolution is in the conflict (confl)
confl.setDecisionLevel(currentLevel);
confl.resolve(constraint, litImplied, this); confl.resolve(constraint, litImplied, this);
updateNumberOfReductions(confl); updateNumberOfReductions(confl);
assert confl.slackConflict().signum() < 0; assert confl.slackConflict().signum() < 0;
...@@ -171,6 +172,7 @@ public class PBSolverCP extends PBSolver { ...@@ -171,6 +172,7 @@ public class PBSolverCP extends PBSolver {
|| decisionLevel() == 0 || confl.isUnsat(); || decisionLevel() == 0 || confl.isUnsat();
assert currentLevel == decisionLevel(); assert currentLevel == decisionLevel();
confl.setDecisionLevel(currentLevel);
confl.undoOne(this.trail.last()); confl.undoOne(this.trail.last());
undoOne(); undoOne();
this.qhead = this.trail.size(); this.qhead = this.trail.size();
......
...@@ -182,6 +182,7 @@ public class InprocCardConstrLearningSolver extends PBSolverCP { ...@@ -182,6 +182,7 @@ public class InprocCardConstrLearningSolver extends PBSolverCP {
constraint = (PBConstr) extendedConstr; constraint = (PBConstr) extendedConstr;
} }
// result of the resolution is in the conflict (confl) // result of the resolution is in the conflict (confl)
confl.setDecisionLevel(currentLevel);
confl.resolve(constraint, litImplied, this); confl.resolve(constraint, litImplied, this);
updateNumberOfReductions(confl); updateNumberOfReductions(confl);
assert confl.slackConflict().signum() < 0; assert confl.slackConflict().signum() < 0;
...@@ -210,6 +211,7 @@ public class InprocCardConstrLearningSolver extends PBSolverCP { ...@@ -210,6 +211,7 @@ public class InprocCardConstrLearningSolver extends PBSolverCP {
|| decisionLevel() == 0; || decisionLevel() == 0;
assert currentLevel == decisionLevel(); assert currentLevel == decisionLevel();
confl.setDecisionLevel(currentLevel);
undoOne(); undoOne();
this.qhead = this.trail.size(); this.qhead = this.trail.size();
updateNumberOfReducedLearnedConstraints(confl); updateNumberOfReducedLearnedConstraints(confl);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment