From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Tue, 27 May 2014 18:41:47 +0000 (-0400)
Subject: timespec printing bug
X-Git-Tag: cvc5-1.0.0~6886
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9006b759cfa01c6006196e0716c2d67c760556a6;p=cvc5.git

timespec printing bug
---

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 {