Removing a stat and fixing new stat in clause data

Author: msoos

cmsat_tablestructure.sql

@@ -151,7 +151,6 @@ CREATE TABLE `clauseStats` (
   `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

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

src/sqlitestats.cpp

@@ -921,7 +921,7 @@ void SQLiteStats::reduceDB(
 
 void SQLiteStats::init_clause_stats_STMT()
 {
-    const size_t numElems = 48;
+    const size_t numElems = 49;
 
     std::stringstream ss;
     ss << "insert into `clauseStats`"
@@ -945,7 +945,6 @@ void SQLiteStats::init_clause_stats_STMT()
     << " `decision_level`,"
     << " `trail_depth_level`,"
     << " `cur_restart_type` ,"
-    << " `cur_confl_in_restart` ,"
 
     << " `atedecents_binIrred`,"
     << " `atedecents_binRed`,"
@@ -1018,7 +1017,6 @@ void SQLiteStats::dump_clause_stats(
     , 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;
@@ -1047,7 +1045,6 @@ void SQLiteStats::dump_clause_stats(
     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

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

src/sqlstats.h

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