Commit 5e509d9d authored by Daniel Le Berre's avatar Daniel Le Berre

Encapsulated fields of SolverStats to please SonarQube.

Need however to check if it does not impact efficiency.
parent ed68390b
......@@ -58,7 +58,7 @@ class Glucose2LCDS<D extends DataStructureFactory> extends GlucoseLCDS<D> {
if (from.getActivity() > 2.0) {
int nblevel = computeLBD(from);
if (nblevel < from.getActivity()) {
solver.stats.updateLBD++;
solver.stats.incUpdateLBD();
from.setActivity(nblevel);
}
}
......
......@@ -67,7 +67,7 @@ class GlucoseLCDS<D extends DataStructureFactory> implements
solver.out
.log(this.solver.getLogPrefix()
+ "cleaning " + (learnedConstrs.size() - j) //$NON-NLS-1$
+ " clauses out of " + learnedConstrs.size() + " with flag " + this.flag + "/" + solver.stats.conflicts); //$NON-NLS-1$ //$NON-NLS-2$
+ " clauses out of " + learnedConstrs.size() + " with flag " + this.flag + "/" + solver.stats.getConflicts()); //$NON-NLS-1$ //$NON-NLS-2$
// out.flush();
}
solver.learnts.shrinkTo(j);
......
......@@ -386,13 +386,13 @@ public class Solver<D extends DataStructureFactory>
this.learnts.push(c);
c.setLearnt();
c.register();
this.stats.learnedclauses++;
this.stats.incLearnedclauses();
switch (c.size()) {
case 2:
this.stats.learnedbinaryclauses++;
this.stats.incLearnedbinaryclauses();
break;
case 3:
this.stats.learnedternaryclauses++;
this.stats.incLearnedternaryclauses();
break;
default:
// do nothing
......@@ -886,7 +886,7 @@ public class Solver<D extends DataStructureFactory>
}
}
conflictToReduce.shrink(i - j);
this.stats.reducedliterals += i - j;
this.stats.incReducedliterals(i - j);
}
private final IVecInt analyzetoclear = new VecInt();
......@@ -908,7 +908,7 @@ public class Solver<D extends DataStructureFactory>
}
}
conflictToReduce.shrink(i - j);
this.stats.reducedliterals += i - j;
this.stats.incReducedliterals(i - j);
}
// Check if 'p' can be removed.' min_level' is used to abort early if
......@@ -972,7 +972,7 @@ public class Solver<D extends DataStructureFactory>
}
}
conflictToReduce.shrink(i - j);
this.stats.reducedliterals += i - j;
this.stats.incReducedliterals(i - j);
}
// Check if 'p' can be removed.' min_level' is used to abort early if
......@@ -1079,7 +1079,7 @@ public class Solver<D extends DataStructureFactory>
// ltrail.size() changes due to propagation
// cannot cache that value.
while (this.qhead < ltrail.size()) {
lstats.propagations++;
lstats.incPropagations();
int p = ltrail.get(this.qhead++);
lslistener.propagating(toDimacs(p));
lorder.assignLiteral(p);
......@@ -1101,7 +1101,7 @@ public class Solver<D extends DataStructureFactory>
this.voc.watches(p).moveTo(lwatched);
final int size = lwatched.size();
for (int i = 0; i < size; i++) {
this.stats.inspects++;
this.stats.incInspects();
// try shortcut
// shortcut = shortcuts.get(i);
// if (shortcut != ILits.UNDEFINED && voc.isSatisfied(shortcut))
......@@ -1130,7 +1130,7 @@ public class Solver<D extends DataStructureFactory>
int p = toDimacs(constr.get(0));
this.slistener.adding(p);
if (constr.size() == 1) {
this.stats.learnedliterals++;
this.stats.incLearnedliterals();
this.slistener.learnUnit(p);
} else {
this.learner.learns(constr);
......@@ -1206,7 +1206,7 @@ public class Solver<D extends DataStructureFactory>
private Lbool search(IVecInt assumps) {
assert this.rootLevel == decisionLevel();
this.stats.starts++;
this.stats.incStarts();
int backjumpLevel;
// varDecay = 1 / params.varDecay;
......@@ -1222,7 +1222,7 @@ public class Solver<D extends DataStructureFactory>
if (confl == null) {
// No conflict found
if (decisionLevel() == 0 && this.isDBSimplificationAllowed) {
this.stats.rootSimplifications++;
this.stats.incRootSimplifications();
boolean ret = simplifyDB();
assert ret;
}
......@@ -1263,7 +1263,7 @@ public class Solver<D extends DataStructureFactory>
}
if (this.sharedConflict == null) {
// New variable decision
this.stats.decisions++;
this.stats.incDecisions();
int p = this.order.select();
if (p == ILits.UNDEFINED) {
// check (expensive) if all the constraints are not
......@@ -1300,7 +1300,7 @@ public class Solver<D extends DataStructureFactory>
}
if (confl != null) {
// conflict found
this.stats.conflicts++;
this.stats.incConflicts();
this.slistener.conflictFound(confl, decisionLevel(),
this.trail.size());
this.conflictCount.newConflict();
......@@ -1494,7 +1494,7 @@ public class Solver<D extends DataStructureFactory>
}
protected final void reduceDB() {
this.stats.reduceddb++;
this.stats.incReduceddb();
this.slistener.cleaning();
this.learnedConstraintsDeletionStrategy.reduce(this.learnts);
}
......@@ -1820,7 +1820,7 @@ public class Solver<D extends DataStructureFactory>
&& this.lastConflictMeansUnsat) {
int before = this.trail.size();
unitClauseProvider.provideUnitClauses(this);
this.stats.importedUnits += this.trail.size() - before;
this.stats.incImportedUnits(this.trail.size() - before);
status = search(assumps);
if (status == Lbool.UNDEFINED) {
this.restarter.onRestart();
......@@ -2024,7 +2024,7 @@ public class Solver<D extends DataStructureFactory>
this.stats.printStat(out, prefix);
double cputime = (System.currentTimeMillis() - this.timebegin) / 1000;
out.println(prefix + "speed (assignments/second)\t: " //$NON-NLS-1$
+ this.stats.propagations / cputime);
+ this.stats.getPropagations() / cputime);
this.order.printStat(out, prefix);
printLearntClausesInfos(out, prefix);
}
......
......@@ -44,39 +44,39 @@ import java.util.Map;
public class SolverStats implements Serializable {
private static final long serialVersionUID = 1L;
public int starts;
private int starts;
public long decisions;
private long decisions;
public long propagations;
private long propagations;
public long inspects;
private long inspects;
public long conflicts;
private long conflicts;
public long learnedliterals;
private long learnedliterals;
public long learnedbinaryclauses;
private long learnedbinaryclauses;
public long learnedternaryclauses;
private long learnedternaryclauses;
public long learnedclauses;
private long learnedclauses;
public long ignoredclauses;
private long ignoredclauses;
public long rootSimplifications;
private long rootSimplifications;
public long reducedliterals;
private long reducedliterals;
public long changedreason;
private long changedreason;
public int reduceddb;
private int reduceddb;
public int shortcuts;
private int shortcuts;
public long updateLBD;
private long updateLBD;
public int importedUnits;
private int importedUnits;
public void reset() {
this.starts = 0;
......@@ -99,7 +99,7 @@ public class SolverStats implements Serializable {
}
public void printStat(PrintWriter out, String prefix) {
out.println(prefix + "starts\t\t: " + this.starts);
out.println(prefix + "starts\t\t: " + this.getStarts());
out.println(prefix + "conflicts\t\t: " + this.conflicts);
out.println(prefix + "decisions\t\t: " + this.decisions);
out.println(prefix + "propagations\t\t: " + this.propagations);
......@@ -112,8 +112,8 @@ public class SolverStats implements Serializable {
+ this.learnedternaryclauses);
out.println(prefix + "learnt constraints\t: " + this.learnedclauses);
out.println(prefix + "ignored constraints\t: " + this.ignoredclauses);
out.println(prefix + "root simplifications\t: "
+ this.rootSimplifications);
out.println(
prefix + "root simplifications\t: " + this.rootSimplifications);
out.println(prefix + "removed literals (reason simplification)\t: "
+ this.reducedliterals);
out.println(prefix + "reason swapping (by a shorter reason)\t: "
......@@ -121,8 +121,7 @@ public class SolverStats implements Serializable {
out.println(prefix + "Calls to reduceDB\t: " + this.reduceddb);
out.println(prefix + "Number of update (reduction) of LBD\t: "
+ this.updateLBD);
out.println(prefix + "Imported unit clauses\t: "
+ this.importedUnits);
out.println(prefix + "Imported unit clauses\t: " + this.importedUnits);
}
public Map<String, Number> toMap() {
......@@ -138,4 +137,140 @@ public class SolverStats implements Serializable {
}
return map;
}
public int getStarts() {
return starts;
}
public void incStarts() {
this.starts++;
}
public long getDecisions() {
return decisions;
}
public void incDecisions() {
this.decisions++;
}
public long getPropagations() {
return propagations;
}
public void incPropagations() {
this.propagations++;
}
public long getInspects() {
return inspects;
}
public void incInspects() {
this.inspects++;
}
public long getConflicts() {
return conflicts;
}
public void incConflicts() {
this.conflicts++;
}
public long getLearnedliterals() {
return learnedliterals;
}
public void incLearnedliterals() {
this.learnedliterals++;
}
public long getLearnedbinaryclauses() {
return learnedbinaryclauses;
}
public void incLearnedbinaryclauses() {
this.learnedbinaryclauses++;
}
public long getLearnedternaryclauses() {
return learnedternaryclauses;
}
public void incLearnedternaryclauses() {
this.learnedternaryclauses++;
}
public long getLearnedclauses() {
return learnedclauses;
}
public void incLearnedclauses() {
this.learnedclauses++;
}
public long getIgnoredclauses() {
return ignoredclauses;
}
public void incIgnoredclauses() {
this.ignoredclauses++;
}
public long getRootSimplifications() {
return rootSimplifications;
}
public void incRootSimplifications() {
this.rootSimplifications++;
}
public long getReducedliterals() {
return reducedliterals;
}
public void incReducedliterals(int increment) {
this.reducedliterals += increment;
}
public long getChangedreason() {
return changedreason;
}
public void incChangedreason() {
this.changedreason++;
}
public int getReduceddb() {
return reduceddb;
}
public void incReduceddb() {
this.reduceddb++;
}
public int getShortcuts() {
return shortcuts;
}
public void incShortcuts() {
this.shortcuts++;
}
public long getUpdateLBD() {
return updateLBD;
}
public void incUpdateLBD() {
this.updateLBD++;
}
public int getImportedUnits() {
return importedUnits;
}
public void incImportedUnits(int increment) {
this.importedUnits += increment;
}
}
......@@ -53,8 +53,8 @@ import org.sat4j.specs.Propagatable;
* @author leberre
*
*/
public class WatcherBasedPrimeImplicantStrategy implements
PrimeImplicantStrategy, MandatoryLiteralListener {
public class WatcherBasedPrimeImplicantStrategy
implements PrimeImplicantStrategy, MandatoryLiteralListener {
private int[] prime;
......@@ -125,14 +125,14 @@ public class WatcherBasedPrimeImplicantStrategy implements
}
long end = System.currentTimeMillis();
if (solver.isVerbose()) {
System.out
.printf("%s prime implicant computation statistics BRESIL (reverse = %b)%n",
solver.getLogPrefix(), this.comparator != null);
System.out
.printf("%s implied: %d, decision: %d, removed %d (+%d), propagated %d, time(ms):%d %n",
solver.getLogPrefix(), solver.implied.size(),
solver.decisions.size(), removed, posremoved,
propagated, end - begin);
System.out.printf(
"%s prime implicant computation statistics BRESIL (reverse = %b)%n",
solver.getLogPrefix(), this.comparator != null);
System.out.printf(
"%s implied: %d, decision: %d, removed %d (+%d), propagated %d, time(ms):%d %n",
solver.getLogPrefix(), solver.implied.size(),
solver.decisions.size(), removed, posremoved, propagated,
end - begin);
}
return implicant;
}
......@@ -145,7 +145,7 @@ public class WatcherBasedPrimeImplicantStrategy implements
solver.voc.watches(p).moveTo(lwatched);
final int size = lwatched.size();
for (int i = 0; i < size; i++) {
solver.stats.inspects++;
solver.stats.incInspects();
lwatched.get(i).propagatePI(this, p);
}
return null;
......
......@@ -75,7 +75,7 @@ public abstract class LimitedLearning<D extends DataStructureFactory>
this.all.learns(constr);
} else {
this.none.learns(constr);
this.stats.ignoredclauses++;
this.stats.incIgnoredclauses();
}
}
......
......@@ -76,11 +76,11 @@ public class EMARestarts implements RestartStrategy {
}
public boolean shouldRestart() {
return this.stats.conflicts > limit && fast / 125 > slow / 100;
return this.stats.getConflicts() > limit && fast / 125 > slow / 100;
}
public void onRestart() {
limit = this.stats.conflicts + 50;
limit = this.stats.getConflicts() + 50;
}
public void onBackjumpToRootLevel() {
......
......@@ -77,7 +77,7 @@ public class Glucose21Restarts implements RestartStrategy {
// was
// ... trailLevel > 1.4 * bufferTrail.average()
// uses now only integers to avoid rounding issues
if (stats.conflicts > 10000 && bufferTrail.isFull()
if (stats.getConflicts() > 10000 && bufferTrail.isFull()
&& trailLevel * 5L > 7L * bufferTrail.average()) {
bufferLBD.clear();
}
......@@ -97,7 +97,7 @@ public class Glucose21Restarts implements RestartStrategy {
// ... && bufferLBD.average() * 0.8 > sumOfAllLBD / stats.conflicts
// uses now only integers to avoid rounding issues
return bufferLBD.isFull()
&& bufferLBD.average() * stats.conflicts * 4L > sumOfAllLBD * 5L;
&& bufferLBD.average() * stats.getConflicts() * 4L > sumOfAllLBD * 5L;
}
public void onRestart() {
......
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