Commit 3c644600 authored by Daniel Le Berre's avatar Daniel Le Berre

More encapsulation of statistics fields.

parent 5e509d9d
Pipeline #3346 passed with stages
in 46 minutes and 46 seconds
...@@ -303,9 +303,9 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -303,9 +303,9 @@ public class ConflictMap extends MapPb implements IConflict {
if (this.weightedLits.get(nLitImplied).negate() if (this.weightedLits.get(nLitImplied).negate()
.compareTo(slackConflict()) > 0) { .compareTo(slackConflict()) > 0) {
if (this.endingSkipping) if (this.endingSkipping)
stats.numberOfEndingSkipping++; stats.incNumberOfEndingSkipping();
else else
stats.numberOfInternalSkipping++; stats.incNumberOfInternalSkipping();
// no resolution // no resolution
// undo operation should be anticipated // undo operation should be anticipated
...@@ -322,7 +322,7 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -322,7 +322,7 @@ public class ConflictMap extends MapPb implements IConflict {
} }
stats.numberOfDerivationSteps++; stats.incNumberOfDerivationSteps();
assert slackConflict().signum() < 0; assert slackConflict().signum() < 0;
assert this.degree.signum() >= 0; assert this.degree.signum() >= 0;
...@@ -383,9 +383,9 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -383,9 +383,9 @@ public class ConflictMap extends MapPb implements IConflict {
for (int i = 0; i < cpb.size(); i++) { for (int i = 0; i < cpb.size(); i++) {
if (coefsCons[i].signum() != 0) { if (coefsCons[i].signum() != 0) {
if (this.voc.isUnassigned(cpb.get(i))) { if (this.voc.isUnassigned(cpb.get(i))) {
this.stats.numberOfRemainingUnassigned++; this.stats.incNumberOfRemainingUnassigned();
} else { } else {
this.stats.numberOfRemainingAssigned++; this.stats.incNumberOfRemainingAssigned();
} }
} }
} }
......
...@@ -44,7 +44,7 @@ public class ConflictMapReduceByGCD extends ConflictMap { ...@@ -44,7 +44,7 @@ public class ConflictMapReduceByGCD extends ConflictMap {
void divideCoefs() { void divideCoefs() {
int gcd = reduceCoeffsByGCD(); int gcd = reduceCoeffsByGCD();
if (gcd > 1) { if (gcd > 1) {
stats.numberOfReductionsByGCD++; stats.incNumberOfReductionsByGCD();
} }
} }
......
...@@ -44,9 +44,8 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap { ...@@ -44,9 +44,8 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap {
void divideCoefs() { void divideCoefs() {
int nbBits = reduceCoeffsByPower2(); int nbBits = reduceCoeffsByPower2();
if (nbBits > 0) { if (nbBits > 0) {
stats.numberOfReductionsByPower2++; stats.incNumberOfReductionsByPower2();
stats.numberOfRightShiftsForCoeffs = stats.numberOfRightShiftsForCoeffs stats.incNumberOfRightShiftsForCoeffs(nbBits);
+ nbBits;
} }
} }
......
...@@ -108,9 +108,9 @@ public class ConflictMapRounding extends ConflictMap { ...@@ -108,9 +108,9 @@ public class ConflictMapRounding extends ConflictMap {
tprime = saturation(abc, tprime, xyz); tprime = saturation(abc, tprime, xyz);
this.coefMultCons = this.weightedLits.get(x ^ 1); this.coefMultCons = this.weightedLits.get(x ^ 1);
this.coefMult = BigInteger.ONE; this.coefMult = BigInteger.ONE;
this.stats.numberOfRoundingOperations++; this.stats.incNumberOfRoundingOperations();
if (easyRounding) { if (easyRounding) {
this.stats.numberOfEasyRoundingOperations++; this.stats.incNumberOfEasyRoundingOperations();
} }
return tprime; return tprime;
} }
......
...@@ -44,9 +44,8 @@ public class PostProcessDivideBy2 implements IPostProcess { ...@@ -44,9 +44,8 @@ public class PostProcessDivideBy2 implements IPostProcess {
public void postProcess(int dl, ConflictMap conflictMap) { public void postProcess(int dl, ConflictMap conflictMap) {
int nbBits = conflictMap.reduceCoeffsByPower2(); int nbBits = conflictMap.reduceCoeffsByPower2();
if (nbBits > 0) { if (nbBits > 0) {
conflictMap.stats.numberOfReductionsByPower2++; conflictMap.stats.incNumberOfReductionsByPower2();
conflictMap.stats.numberOfRightShiftsForCoeffs = conflictMap.stats.numberOfRightShiftsForCoeffs conflictMap.stats.incNumberOfRightShiftsForCoeffs(nbBits);
+ nbBits;
} }
} }
......
...@@ -15,7 +15,7 @@ public class PostProcessDivideByGCD implements IPostProcess { ...@@ -15,7 +15,7 @@ public class PostProcessDivideByGCD implements IPostProcess {
public void postProcess(int dl, ConflictMap conflictMap) { public void postProcess(int dl, ConflictMap conflictMap) {
int gcd = conflictMap.reduceCoeffsByGCD(); int gcd = conflictMap.reduceCoeffsByGCD();
if (gcd > 1) { if (gcd > 1) {
conflictMap.stats.numberOfReductionsByGCD++; conflictMap.stats.incNumberOfReductionsByGCD();
} }
} }
......
...@@ -270,7 +270,7 @@ public abstract class PBSolver extends Solver<PBDataStructureFactory> implements ...@@ -270,7 +270,7 @@ public abstract class PBSolver extends Solver<PBDataStructureFactory> implements
System.out System.out
.println(getLogPrefix() .println(getLogPrefix()
+ "cleaning " + (learnedConstrs.size() - j) //$NON-NLS-1$ + "cleaning " + (learnedConstrs.size() - j) //$NON-NLS-1$
+ " clauses out of " + learnedConstrs.size() + "/" + PBSolver.this.stats.conflicts); //$NON-NLS-1$ //$NON-NLS-2$ + " clauses out of " + learnedConstrs.size() + "/" + PBSolver.this.stats.getConflicts()); //$NON-NLS-1$ //$NON-NLS-2$
System.out.flush(); System.out.flush();
} }
PBSolver.this.learnts.shrinkTo(j); PBSolver.this.learnts.shrinkTo(j);
......
...@@ -71,14 +71,14 @@ public class PBSolverCautious extends PBSolverCP { ...@@ -71,14 +71,14 @@ public class PBSolverCautious extends PBSolverCP {
@Override @Override
protected void updateNumberOfReductions(IConflict confl) { protected void updateNumberOfReductions(IConflict confl) {
this.stats.numberOfReductions += ((ConflictMapSwitchToClause) confl) this.stats.incNumberOfReductions(
.getNumberOfReductions(); ((ConflictMapSwitchToClause) confl).getNumberOfReductions());
} }
@Override @Override
protected void updateNumberOfReducedLearnedConstraints(IConflict confl) { protected void updateNumberOfReducedLearnedConstraints(IConflict confl) {
if (((ConflictMapSwitchToClause) confl).hasBeenReduced()) { if (((ConflictMapSwitchToClause) confl).hasBeenReduced()) {
this.stats.numberOfLearnedConstraintsReduced++; this.stats.incNumberOfLearnedConstraintsReduced();
} }
} }
......
...@@ -37,8 +37,8 @@ import org.sat4j.minisat.core.SearchParams; ...@@ -37,8 +37,8 @@ import org.sat4j.minisat.core.SearchParams;
public class PBSolverResCP extends PBSolverCP { public class PBSolverResCP extends PBSolverCP {
/** /**
* *
*/ */
private static final long serialVersionUID = 1L; private static final long serialVersionUID = 1L;
public static final long MAXCONFLICTS = 100000L; public static final long MAXCONFLICTS = 100000L;
...@@ -70,16 +70,16 @@ public class PBSolverResCP extends PBSolverCP { ...@@ -70,16 +70,16 @@ public class PBSolverResCP extends PBSolverCP {
@Override @Override
boolean someCriteria() { boolean someCriteria() {
if (this.stats.conflicts == this.bound) { if (this.stats.getConflicts() == this.bound) {
this.setSimplifier(NO_SIMPLIFICATION); this.setSimplifier(NO_SIMPLIFICATION);
this.reduceDB(); this.reduceDB();
this.stats.numberOfCP++; this.stats.incNumberOfCP();
return true; return true;
} else if (this.stats.conflicts > this.bound) { } else if (this.stats.getConflicts() > this.bound) {
this.stats.numberOfCP++; this.stats.incNumberOfCP();
return true; return true;
} else { } else {
this.stats.numberOfResolution++; this.stats.incNumberOfResolution();
return false; return false;
} }
} }
......
...@@ -40,33 +40,33 @@ public class PBSolverStats extends SolverStats { ...@@ -40,33 +40,33 @@ public class PBSolverStats extends SolverStats {
*/ */
private static final long serialVersionUID = 1L; private static final long serialVersionUID = 1L;
public long numberOfReductions; private long numberOfReductions;
public long numberOfReductionsByPower2; private long numberOfReductionsByPower2;
public long numberOfRightShiftsForCoeffs; private long numberOfRightShiftsForCoeffs;
public long numberOfReductionsByGCD; private long numberOfReductionsByGCD;
public long numberOfLearnedConstraintsReduced; private long numberOfLearnedConstraintsReduced;
public long numberOfResolution; private long numberOfResolution;
public long numberOfCP; private long numberOfCP;
public long numberOfRoundingOperations; private long numberOfRoundingOperations;
public long numberOfEasyRoundingOperations; private long numberOfEasyRoundingOperations;
public long numberOfEndingSkipping; private long numberOfEndingSkipping;
public long numberOfInternalSkipping; private long numberOfInternalSkipping;
public long numberOfDerivationSteps; private long numberOfDerivationSteps;
public long numberOfRemainingUnassigned; private long numberOfRemainingUnassigned;
public long numberOfRemainingAssigned; private long numberOfRemainingAssigned;
@Override @Override
public void reset() { public void reset() {
...@@ -91,7 +91,7 @@ public class PBSolverStats extends SolverStats { ...@@ -91,7 +91,7 @@ public class PBSolverStats extends SolverStats {
super.printStat(out, prefix); super.printStat(out, prefix);
out.println( out.println(
prefix + "number of reductions to clauses (during analyze)\t: " prefix + "number of reductions to clauses (during analyze)\t: "
+ this.numberOfReductions); + this.getNumberOfReductions());
out.println(prefix out.println(prefix
+ "number of learned constraints concerned by reduction\t: " + "number of learned constraints concerned by reduction\t: "
+ this.numberOfLearnedConstraintsReduced); + this.numberOfLearnedConstraintsReduced);
...@@ -106,7 +106,7 @@ public class PBSolverStats extends SolverStats { ...@@ -106,7 +106,7 @@ public class PBSolverStats extends SolverStats {
+ this.numberOfEasyRoundingOperations); + this.numberOfEasyRoundingOperations);
out.println(prefix out.println(prefix
+ "number of reductions of the coefficients by power 2 \t: " + "number of reductions of the coefficients by power 2 \t: "
+ this.numberOfReductionsByPower2); + this.getNumberOfReductionsByPower2());
out.println( out.println(
prefix + "number of right shift for reduction by power 2 \t: " prefix + "number of right shift for reduction by power 2 \t: "
+ this.numberOfRightShiftsForCoeffs); + this.numberOfRightShiftsForCoeffs);
...@@ -118,7 +118,7 @@ public class PBSolverStats extends SolverStats { ...@@ -118,7 +118,7 @@ public class PBSolverStats extends SolverStats {
out.println(prefix + "number of internal skipping \t: " out.println(prefix + "number of internal skipping \t: "
+ this.numberOfInternalSkipping); + this.numberOfInternalSkipping);
out.println(prefix + "number of derivation steps \t: " out.println(prefix + "number of derivation steps \t: "
+ this.numberOfDerivationSteps); + this.getNumberOfDerivationSteps());
out.println(prefix + "number of skipped derivation steps \t: " out.println(prefix + "number of skipped derivation steps \t: "
+ (this.numberOfInternalSkipping + (this.numberOfInternalSkipping
+ this.numberOfEndingSkipping)); + this.numberOfEndingSkipping));
...@@ -128,4 +128,116 @@ public class PBSolverStats extends SolverStats { ...@@ -128,4 +128,116 @@ public class PBSolverStats extends SolverStats {
+ this.numberOfRemainingAssigned); + this.numberOfRemainingAssigned);
} }
public long getNumberOfReductions() {
return numberOfReductions;
}
public void incNumberOfReductions(long increment) {
this.numberOfReductions += increment;
}
public long getNumberOfReductionsByPower2() {
return numberOfReductionsByPower2;
}
public void incNumberOfReductionsByPower2() {
this.numberOfReductionsByPower2++;
}
public long getNumberOfRightShiftsForCoeffs() {
return numberOfRightShiftsForCoeffs;
}
public void incNumberOfRightShiftsForCoeffs(int increment) {
this.numberOfRightShiftsForCoeffs += increment;
}
public long getNumberOfReductionsByGCD() {
return numberOfReductionsByGCD;
}
public void incNumberOfReductionsByGCD() {
this.numberOfReductionsByGCD++;
}
public long getNumberOfLearnedConstraintsReduced() {
return numberOfLearnedConstraintsReduced;
}
public void incNumberOfLearnedConstraintsReduced() {
this.numberOfLearnedConstraintsReduced++;
}
public long getNumberOfResolution() {
return numberOfResolution;
}
public void incNumberOfResolution() {
this.numberOfResolution++;
}
public long getNumberOfCP() {
return numberOfCP;
}
public void incNumberOfCP() {
this.numberOfCP++;
}
public long getNumberOfRoundingOperations() {
return numberOfRoundingOperations;
}
public void incNumberOfRoundingOperations() {
this.numberOfRoundingOperations++;
}
public long getNumberOfEasyRoundingOperations() {
return numberOfEasyRoundingOperations;
}
public void incNumberOfEasyRoundingOperations() {
this.numberOfEasyRoundingOperations++;
}
public long getNumberOfEndingSkipping() {
return numberOfEndingSkipping;
}
public void incNumberOfEndingSkipping() {
this.numberOfEndingSkipping++;
}
public long getNumberOfInternalSkipping() {
return numberOfInternalSkipping;
}
public void incNumberOfInternalSkipping() {
this.numberOfInternalSkipping++;
}
public long getNumberOfDerivationSteps() {
return numberOfDerivationSteps;
}
public void incNumberOfDerivationSteps() {
this.numberOfDerivationSteps++;
}
public long getNumberOfRemainingUnassigned() {
return numberOfRemainingUnassigned;
}
public void incNumberOfRemainingUnassigned() {
this.numberOfRemainingUnassigned++;
}
public long getNumberOfRemainingAssigned() {
return numberOfRemainingAssigned;
}
public void incNumberOfRemainingAssigned() {
this.numberOfRemainingAssigned++;
}
} }
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