Adding more information to clause about current restart

Author: msoos

cmsat_tablestructure.sql

@@ -150,6 +150,8 @@ CREATE TABLE `clauseStats` (
   `backtrack_level` int(20) NOT NULL,
   `decision_level` int(20) NOT NULL,
   `trail_depth_level` int(20) NOT NULL,
+  `cur_restart_type` char(20) NOT NULL,
+  `cur_confl_in_restart` int(20) NOT NULL,
 
   `atedecents_binIrred` int(20) NOT NULL,
   `atedecents_binRed` int(20) NOT NULL,

src/searcher.cpp

@@ -1486,6 +1486,8 @@ void Searcher::dump_sql_clause_data(
         , decisionLevel()
         , trail.size()
         , params.conflictsDoneThisRestart
+        , restart_type_to_short_string(params.rest_type)
+        , stats
         , hist
     );
 }

src/sqlitestats.cpp

@@ -944,6 +944,8 @@ void SQLiteStats::init_clause_stats_STMT()
     << " `backtrack_level`,"
     << " `decision_level`,"
     << " `trail_depth_level`,"
+    << " `cur_restart_type` ,"
+    << " `cur_confl_in_restart` ,"
 
     << " `atedecents_binIrred`,"
     << " `atedecents_binRed`,"
@@ -1015,6 +1017,8 @@ void SQLiteStats::dump_clause_stats(
     , size_t decision_level
     , size_t trail_depth
     , uint64_t conflicts_this_restart
+    , const std::string& restart_type
+    , const SearchStats& stats
     , const SearchHist& hist
 ) {
     uint32_t num_overlap_literals = antec_data.sum_size()-(antec_data.num()-1)-size;
@@ -1042,6 +1046,8 @@ void SQLiteStats::dump_clause_stats(
     sqlite3_bind_int(stmt_clause_stats, bindAt++, backtrack_level);
     sqlite3_bind_int64(stmt_clause_stats, bindAt++, decision_level);
     sqlite3_bind_int64(stmt_clause_stats, bindAt++, trail_depth);
+    sqlite3_bind_text(stmt_clause_stats, bindAt++,  restart_type.c_str(), -1, NULL);
+    sqlite3_bind_int64(stmt_clause_stats, bindAt++, stats.conflStats.numConflicts);
 
     sqlite3_bind_int(stmt_clause_stats, bindAt++, antec_data.binIrred);
     sqlite3_bind_int(stmt_clause_stats, bindAt++, antec_data.binRed);

src/sqlitestats.h

@@ -89,6 +89,8 @@ class SQLiteStats: public SQLStats
         , size_t decision_level
         , size_t trail_depth
         , uint64_t conflicts_this_restart
+        , const std::string& rest_type
+        , const SearchStats& stats
         , const SearchHist& hist
     ) override;
 

src/sqlstats.h

@@ -91,6 +91,8 @@ class SQLStats
         , size_t decision_level
         , size_t trail_depth
         , uint64_t conflicts_this_restart
+        , const std::string& rest_type
+        , const SearchStats& stats
         , const SearchHist& hist
     ) = 0;