Fixing the timing issue correctly this time around

Previous fix was only a half fix. This one should now be correctly displaying the time for the current thread. It was more complicated than I thought I have to admit. Closes #497
msoos · Sep 23, 2018 · 05f2a3f · 05f2a3f
1 parent ffd3153
commit 05f2a3f
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 12 deletions.
diff --git a/src/cryptominisat.cpp b/src/cryptominisat.cpp
@@ -69,6 +69,7 @@ namespace CMSat {
         CMSatPrivateData& operator=(const CMSatPrivateData&) = delete;
 
         vector<Solver*> solvers;
+        vector<double> cpu_times;
         SharedData *shared_data = NULL;
         int which_solved = 0;
         std::atomic<bool>* must_interrupt;
@@ -91,6 +92,7 @@ struct DataForThread
 {
     explicit DataForThread(CMSatPrivateData* data, const vector<Lit>* _assumptions = NULL) :
         solvers(data->solvers)
+        , cpu_times(data->cpu_times)
         , lits_to_add(&(data->cls_lits))
         , vars_to_add(data->vars_to_add)
         , assumptions(_assumptions)
@@ -106,6 +108,7 @@ struct DataForThread
         delete ret;
     }
     vector<Solver*>& solvers;
+    vector<double>& cpu_times;
     vector<Lit> *lits_to_add;
     uint32_t vars_to_add;
     const vector<Lit> *assumptions;
@@ -129,6 +132,7 @@ DLL_PUBLIC SATSolver::SATSolver(
     }
 
     data->solvers.push_back(new Solver((SolverConf*) config, data->must_interrupt));
+    data->cpu_times.push_back(0.0);
 }
 
 DLL_PUBLIC SATSolver::~SATSolver()
@@ -391,6 +395,7 @@ DLL_PUBLIC void SATSolver::set_num_threads(unsigned num)
         SolverConf conf = data->solvers[0]->getConf();
         update_config(conf, i);
         data->solvers.push_back(new Solver(&conf, data->must_interrupt));
+        data->cpu_times.push_back(0.0);
     }
 
     //set shared data
@@ -720,13 +725,13 @@ struct OneThreadCalc
             ret = data_for_thread.solvers[tid]->simplify_with_assumptions(data_for_thread.assumptions);
         }
 
+        data_for_thread.cpu_times[tid] = cpuTime();
         if (print_thread_start_and_finish) {
-            double end_time = cpuTime();
             data_for_thread.update_mutex->lock();
             ios::fmtflags f(cout.flags());
             cout << "c Finished thread " << tid << " with result: " << ret
             << " T-diff: " << std::fixed << std::setprecision(2)
-            << (end_time-start_time)
+            << (data_for_thread.cpu_times[tid]-start_time)
             << endl;
             cout.flags(f);
             data_for_thread.update_mutex->unlock();
@@ -929,7 +934,7 @@ std::string SATSolver::get_text_version_info()
 DLL_PUBLIC void SATSolver::print_stats() const
 {
     double cpu_time_total = cpuTimeTotal();
-    data->solvers[data->which_solved]->print_stats(cpu_time_total);
+    data->solvers[data->which_solved]->print_stats(data->cpu_times[data->which_solved], cpu_time_total);
 }
 
 DLL_PUBLIC void SATSolver::set_drat(std::ostream* os, bool add_ID)

diff --git a/src/solver.cpp b/src/solver.cpp
@@ -2059,9 +2059,8 @@ void Solver::print_prop_confl_stats(
     }
 }
 
-void Solver::print_stats(const double cpu_time_total) const
+void CMSat::Solver::print_stats(const double cpu_time, const double cpu_time_total) const
 {
-    double cpu_time = cpuTime();
     cout << "c ------- FINAL TOTAL SEARCH STATS ---------" << endl;
     if (conf.do_print_times)
     print_stats_line("c UIP search time"
@@ -2149,15 +2148,22 @@ void Solver::print_min_stats(const double cpu_time, const double cpu_time_total)
     } else {
         print_stats_line("c Conflicts in UIP", sumConflicts);
     }
-    if (conf.do_print_times)
-    print_stats_line("c Total time (all threads)", cpu_time_total);
+    print_stats_time(cpu_time, cpu_time_total);
     double vm_usage;
     print_stats_line("c Mem used"
         , (double)memUsedTotal(vm_usage)/(1024UL*1024UL)
         , "MB"
     );
 }
 
+void Solver::print_stats_time(const double cpu_time, const double cpu_time_total) const
+{
+    if (conf.do_print_times) {
+        print_stats_line("c Total time (all threads)", cpu_time_total);
+        print_stats_line("c Total time (this thread)", cpu_time);
+    }
+}
+
 void Solver::print_norm_stats(const double cpu_time, const double cpu_time_total) const
 {
     sumSearchStats.print_short(sumPropStats.propagations, conf.do_print_times);
@@ -2250,8 +2256,7 @@ void Solver::print_norm_stats(const double cpu_time, const double cpu_time_total
         , (double)memUsedTotal(vm_usage)/(1024UL*1024UL)
         , "MB"
     );
-    if (conf.do_print_times)
-    print_stats_line("c Total time (all threads)", cpu_time_total);
+    print_stats_time(cpu_time, cpu_time_total);
 }
 
 void Solver::print_full_restart_stat(const double cpu_time, const double cpu_time_total) const
@@ -2357,8 +2362,7 @@ void Solver::print_full_restart_stat(const double cpu_time, const double cpu_tim
     } else {
         print_stats_line("c Conflicts in UIP", sumConflicts);
     }
-    if (conf.do_print_times)
-    print_stats_line("c Total time (all threads)", cpu_time_total);
+    print_stats_time(cpu_time, cpu_time_total);
     print_mem_stats();
 }
 

diff --git a/src/solver.h b/src/solver.h
@@ -116,7 +116,8 @@ class Solver : public Searcher
         static const char* get_compilation_env();
 
         vector<Lit> get_zero_assigned_lits(const bool backnumber = true, bool only_nvars = false) const;
-        void     print_stats(const double cpu_time_total) const;
+        void     print_stats(const double cpu_time, const double cpu_time_total) const;
+        void     print_stats_time(const double cpu_time, const double cpu_time_total) const;
         void     print_clause_stats() const;
         size_t get_num_free_vars() const;
         size_t get_num_nonfree_vars() const;