Commit 1bcf9303 authored by Romain WALLON's avatar Romain WALLON
Browse files

Fix the reduction to clause.

parent 1af826fe
Pipeline #6857 passed with stage
in 38 seconds
...@@ -423,7 +423,7 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -423,7 +423,7 @@ public class ConflictMap extends MapPb implements IConflict {
} }
} }
assert slackConflict().signum() < 0; assert slackConflict().signum() < 0;
//assert slackConflict().equals(currentSlack.subtract(degree)); // assert slackConflict().equals(currentSlack.subtract(degree));
// cutting plane // cutting plane
this.degree = cuttingPlane(cpb, degreeCons, coefsCons, this.degree = cuttingPlane(cpb, degreeCons, coefsCons,
...@@ -436,7 +436,7 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -436,7 +436,7 @@ public class ConflictMap extends MapPb implements IConflict {
assert getLevelByLevel(nLitImplied) == -1; assert getLevelByLevel(nLitImplied) == -1;
assert this.degree.signum() > 0; assert this.degree.signum() > 0;
assert slackConflict().signum() < 0; assert slackConflict().signum() < 0;
//assert slackConflict().equals(currentSlack.subtract(degree)); // assert slackConflict().equals(currentSlack.subtract(degree));
// saturation // saturation
this.degree = saturation(); this.degree = saturation();
...@@ -809,6 +809,10 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -809,6 +809,10 @@ public class ConflictMap extends MapPb implements IConflict {
return value; return value;
} }
@Override
public String toString() {
return value.toString();
}
} }
/** /**
...@@ -859,8 +863,7 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -859,8 +863,7 @@ public class ConflictMap extends MapPb implements IConflict {
int at = 0; int at = 0;
for (Integer lvl : levels) { for (Integer lvl : levels) {
s = s.subtract(bylvl.get(lvl).getValue()); s = s.subtract(bylvl.get(lvl).getValue());
for (;; at++) { for (; at < vv_indices.size(); at++) {
assert at < vv_indices.size();
int i = vv_indices.get(at); int i = vv_indices.get(at);
int l = weightedLits.getLit(i); int l = weightedLits.getLit(i);
BigInteger coef = weightedLits.getCoef(i); BigInteger coef = weightedLits.getCoef(i);
...@@ -873,7 +876,6 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -873,7 +876,6 @@ public class ConflictMap extends MapPb implements IConflict {
} }
} }
} }
assert false;
return 0; return 0;
} }
......
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