From 61fcb96a72f6ab60fc3057a7d87fbd3a07a989c4 Mon Sep 17 00:00:00 2001 From: Daniel Le Berre Date: Sun, 11 Nov 2018 12:43:58 +0100 Subject: [PATCH] Encapsulated fields of SolverStats to please SonarQube. Need however to check if it does not impact efficiency. --- .../org/sat4j/minisat/core/Glucose2LCDS.java | 2 +- .../org/sat4j/minisat/core/GlucoseLCDS.java | 2 +- .../java/org/sat4j/minisat/core/Solver.java | 32 ++-- .../org/sat4j/minisat/core/SolverStats.java | 179 +++++++++++++++--- .../WatcherBasedPrimeImplicantStrategy.java | 22 +-- .../minisat/learning/LimitedLearning.java | 2 +- .../sat4j/minisat/restarts/EMARestarts.java | 4 +- .../minisat/restarts/Glucose21Restarts.java | 4 +- 8 files changed, 191 insertions(+), 56 deletions(-) diff --git a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Glucose2LCDS.java b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Glucose2LCDS.java index 766b1588..c14c94cd 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Glucose2LCDS.java +++ b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Glucose2LCDS.java @@ -58,7 +58,7 @@ class Glucose2LCDS extends GlucoseLCDS { if (from.getActivity() > 2.0) { int nblevel = computeLBD(from); if (nblevel < from.getActivity()) { - solver.stats.updateLBD++; + solver.stats.incUpdateLBD(); from.setActivity(nblevel); } } diff --git a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/GlucoseLCDS.java b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/GlucoseLCDS.java index caa91d1e..f460df8f 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/GlucoseLCDS.java +++ b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/GlucoseLCDS.java @@ -67,7 +67,7 @@ class GlucoseLCDS 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); diff --git a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java index d9ca6962..4eef8b75 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java +++ b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/Solver.java @@ -386,13 +386,13 @@ public class Solver 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 } } 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 } } 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 } } 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 // 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 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 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 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 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 } 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 } 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 } 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 && 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 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); } diff --git a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/SolverStats.java b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/SolverStats.java index 7b846a2f..9a956fd1 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/SolverStats.java +++ b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/SolverStats.java @@ -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 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; + } } diff --git a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/WatcherBasedPrimeImplicantStrategy.java b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/WatcherBasedPrimeImplicantStrategy.java index dd996ccc..8e5b9183 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/minisat/core/WatcherBasedPrimeImplicantStrategy.java +++ b/org.sat4j.core/src/main/java/org/sat4j/minisat/core/WatcherBasedPrimeImplicantStrategy.java @@ -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; diff --git a/org.sat4j.core/src/main/java/org/sat4j/minisat/learning/LimitedLearning.java b/org.sat4j.core/src/main/java/org/sat4j/minisat/learning/LimitedLearning.java index 029ff0ee..f1a2bd0d 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/minisat/learning/LimitedLearning.java +++ b/org.sat4j.core/src/main/java/org/sat4j/minisat/learning/LimitedLearning.java @@ -75,7 +75,7 @@ public abstract class LimitedLearning this.all.learns(constr); } else { this.none.learns(constr); - this.stats.ignoredclauses++; + this.stats.incIgnoredclauses(); } } diff --git a/org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/EMARestarts.java b/org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/EMARestarts.java index d2023164..28cfab3e 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/EMARestarts.java +++ b/org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/EMARestarts.java @@ -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() { diff --git a/org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/Glucose21Restarts.java b/org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/Glucose21Restarts.java index 48cb6182..c399aec7 100644 --- a/org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/Glucose21Restarts.java +++ b/org.sat4j.core/src/main/java/org/sat4j/minisat/restarts/Glucose21Restarts.java @@ -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() { -- GitLab