Commit e6549155 authored by Romain WALLON's avatar Romain WALLON

Corrects the order of the literals in all kinds of WatchPb

parent ea6d9ba2
Pipeline #4711 failed with stages
in 194 minutes and 39 seconds
......@@ -361,7 +361,7 @@ public abstract class WatchPb
for (j = i + 1; j < to; j++) {
if (this.coefs[j].compareTo(this.coefs[bestIndex]) > 0
|| this.coefs[j].equals(this.coefs[bestIndex])
&& this.lits[j] > this.lits[bestIndex]) {
&& this.lits[j] < this.lits[bestIndex]) {
bestIndex = j;
}
}
......@@ -447,12 +447,12 @@ public abstract class WatchPb
i++;
} while (this.coefs[i].compareTo(pivot) > 0
|| this.coefs[i].equals(pivot)
&& this.lits[i] > litPivot);
&& this.lits[i] < litPivot);
do {
j--;
} while (pivot.compareTo(this.coefs[j]) > 0
|| this.coefs[j].equals(pivot)
&& this.lits[j] < litPivot);
&& this.lits[j] > litPivot);
if (i >= j) {
break;
......
......@@ -388,7 +388,7 @@ public abstract class WatchPbLongCP
for (j = i + 1; j < to; j++) {
if (this.coefs[j] > this.coefs[bestIndex]
|| this.coefs[j] == this.coefs[bestIndex]
&& this.lits[j] > this.lits[bestIndex]) {
&& this.lits[j] < this.lits[bestIndex]) {
bestIndex = j;
}
}
......@@ -474,11 +474,11 @@ public abstract class WatchPbLongCP
do {
i++;
} while (this.coefs[i] > pivot
|| this.coefs[i] == pivot && this.lits[i] > litPivot);
|| this.coefs[i] == pivot && this.lits[i] < litPivot);
do {
j--;
} while (pivot > this.coefs[j]
|| this.coefs[j] == pivot && this.lits[j] < litPivot);
|| this.coefs[j] == pivot && this.lits[j] > litPivot);
if (i >= j) {
break;
......
  • There must be a problem in this code: the build takes ages since those changes. We probably enter an infinite loop in corner cases.

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