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

Do not set the decisionLevel when calling isAssertive.

parent db90c603
Pipeline #3233 failed with stages
in 12 minutes and 21 seconds
...@@ -567,12 +567,11 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -567,12 +567,11 @@ public class ConflictMap extends MapPb implements IConflict {
public boolean isAssertive(int dl) { public boolean isAssertive(int dl) {
assert dl <= this.currentLevel; assert dl <= this.currentLevel;
this.currentLevel = dl;
BigInteger slack = this.currentSlack.subtract(this.degree); BigInteger slack = this.currentSlack.subtract(this.degree);
if (slack.signum() < 0) { if (slack.signum() < 0) {
return false; return false;
} }
return isImplyingLiteral(slack); return isImplyingLiteral(slack, dl);
} }
/** /**
...@@ -587,7 +586,7 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -587,7 +586,7 @@ 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) { 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;
...@@ -605,7 +604,7 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -605,7 +604,7 @@ public class ConflictMap extends MapPb implements IConflict {
// then we have to look at every literal // then we have to look at every literal
// at a decision level >= currentLevel // at a decision level >= currentLevel
BigInteger tmp; BigInteger tmp;
int level = levelToIndex(this.currentLevel); int level = levelToIndex(currentDecisionLevel);
if (this.byLevel[level] != null) { if (this.byLevel[level] != null) {
for (IteratorInt iterator = this.byLevel[level].iterator(); iterator for (IteratorInt iterator = this.byLevel[level].iterator(); iterator
.hasNext();) { .hasNext();) {
......
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