timespec printing bug

diff --git a/src/main/options b/src/main/options
index 8733011f7a2e456598affd00ce3b3415fc14fc8e..943f46b61eff24ea8717a74aabbe430bf80989d4 100644 (file)
--- 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 610023b70387e480c4b86cffff50c7479d33d30e..b2857216de94a9e2d08bbb23bf636839deed8ce9 100644 (file)
--- 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 8246bfdd23c0aafdcf957e2e04f8dfee0353b7ef..be4a719792a4ab28fe3e8297d0c9aa4fdfae6f36 100644 (file)
--- 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 {