Commit 09bb8a79 authored by Blomme Anthony's avatar Blomme Anthony
Browse files

veriPB : try to use saturation in the proof only when necessary

parent 504d5caa
Pipeline #15922 passed with stages
in 40 minutes and 40 seconds
......@@ -743,10 +743,10 @@ public class ConflictMap extends MapPb implements IConflict {
protected BigInteger saturation(BigInteger[] coefs, BigInteger degree,
IWatchPb wpb) {
listener.saturateReason();
assert degree.signum() > 0;
BigInteger degreeResult = degree;
boolean isMinimumEqualsToDegree = true;
boolean useSaturation = false;
int comparison;
for (int i = 0; i < coefs.length; i++) {
comparison = coefs[i].compareTo(degree);
......@@ -756,6 +756,9 @@ public class ConflictMap extends MapPb implements IConflict {
.subtract(coefs[i]);
this.possReducedCoefs = this.possReducedCoefs.add(degree);
}
if (!(degree.equals(coefs[i]))) {
useSaturation = true;
}
coefs[i] = degree;
} else if (comparison < 0 && coefs[i].signum() > 0) {
isMinimumEqualsToDegree = false;
......@@ -778,6 +781,9 @@ public class ConflictMap extends MapPb implements IConflict {
}
listener.divideReason(degree);
}
if (useSaturation) {
listener.saturateReason();
}
return degreeResult;
}
......
......@@ -179,12 +179,13 @@ public class MapPb implements IDataStructurePB {
}
public BigInteger saturation() {
listener.saturateConflict();
assert this.degree.signum() > 0;
BigInteger minimum = this.degree;
boolean useSaturation = false;
for (int ind = 0; ind < size(); ind++) {
assert this.weightedLits.getCoef(ind).signum() >= 0;
if (this.degree.compareTo(this.weightedLits.getCoef(ind)) < 0) {
useSaturation = true;
changeCoef(ind, this.degree);
}
assert this.weightedLits.getCoef(ind).signum() >= 0;
......@@ -200,7 +201,9 @@ public class MapPb implements IDataStructurePB {
changeCoef(ind, BigInteger.ONE);
}
}
if (useSaturation) {
listener.saturateConflict();
}
return this.degree;
}
......
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