diff options
| -rw-r--r-- | src/main/options | 3 | ||||
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 8 | ||||
| -rw-r--r-- | src/util/statistics_registry.h | 4 |
3 files changed, 13 insertions, 2 deletions
diff --git a/src/main/options b/src/main/options index 8733011f7..943f46b61 100644 --- a/src/main/options +++ b/src/main/options @@ -53,4 +53,7 @@ undocumented-alias --segv-nospin = --no-segv-spin expert-option waitToJoin --wait-to-join bool :default true wait for other threads to join before quitting +expert-option periodicStatsInterval --periodic-stats int :default 0 + print total time we have been running every N decisions + endmodule diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 610023b70..b2857216d 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/minisat.h" #include "prop/options.h" #include "util/output.h" +#include "util/periodic_statistics.h" #include "expr/command.h" #include "proof/proof_manager.h" #include "proof/sat_proof.h" @@ -478,6 +479,13 @@ Lit Solver::pickBranchLit() { Lit nextLit; + // Every so-many-decisions print the total time + if(options::periodicStatsInterval() && decisions % options::periodicStatsInterval() == 0) { + PeriodicStatistic::print("sat::decisions", decisions); + PeriodicStatistic::print("sat::conflicts", conflicts); + PeriodicStatistic::print("sat::propagations", propagations); + } + #ifdef CVC4_REPLAY nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision()); diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 8246bfdd2..be4a71979 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -694,7 +694,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) { CheckArgument(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec, a); CheckArgument(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec, b); a.tv_sec -= b.tv_sec; - long nsec = a.tv_nsec - b.tv_nsec; + long nsec = long(a.tv_nsec) - long(b.tv_nsec); if(nsec < 0) { nsec += nsec_per_sec; --a.tv_sec; @@ -762,7 +762,7 @@ inline bool operator>=(const timespec& a, const timespec& b) { inline std::ostream& operator<<(std::ostream& os, const timespec& t) { // assumes t.tv_nsec is in range return os << t.tv_sec << "." - << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec; + << std::setfill('0') << std::setw(9) << std::right << t.tv_nsec; } namespace CVC4 { |