1 /******************************************
2 Copyright (c) 2016, Mate Soos
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to deal
6 in the Software without restriction, including without limitation the rights
7 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 THE SOFTWARE.
21 ***********************************************/
22
23 #include "sqlitestats.h"
24 #include "solvertypes.h"
25 #include "solver.h"
26 #include "time_mem.h"
27 #include <sstream>
28 #include "varreplacer.h"
29 #include "occsimplifier.h"
30 #include <string>
31 #include <cmath>
32 #include <time.h>
33 #include "constants.h"
34 #include "reducedb.h"
35 #include "sql_tablestructure.h"
36 #include "varreplacer.h"
37
38 #define bind_null_or_double(stmt,bindat,stucture,func) \
39 { \
40 if (stucture.num_data_elements() == 0) {\
41 sqlite3_bind_null(stmt, bindat); \
42 } else { \
43 sqlite3_bind_double(stmt, bindat, stucture.func()); \
44 }\
45 bindat++; \
46 }
47
48 #define bind_null_or_int(stmt,bindat,stucture,func) \
49 { \
50 if (stucture.num_data_elements() == 0) {\
51 sqlite3_bind_null(stmt, bindat); \
52 } else { \
53 sqlite3_bind_int(stmt, bindat, stucture.func()); \
54 }\
55 bindat++; \
56 }
57
58 #define bind_null_or_int64(stmt,bindat,stucture,func) \
59 { \
60 if (stucture.num_data_elements() == 0) {\
61 sqlite3_bind_null(stmt, bindat); \
62 } else { \
63 sqlite3_bind_int64(stmt, bindat, stucture.func()); \
64 }\
65 bindat++; \
66 }
67
68 using std::cout;
69 using std::cerr;
70 using std::endl;
71 using std::string;
72 using namespace CMSat;
73
rst_dat_type_to_str(rst_dat_type type)74 const char* rst_dat_type_to_str(rst_dat_type type) {
75 static const char* const norm ="restart_norm";
76 static const char* const var ="restart_var";
77 static const char* const cl ="restart_cl";
78 if (type == rst_dat_type::norm) {
79 return norm;
80 } else if (type == rst_dat_type::var) {
81 return var;
82 } else if (type == rst_dat_type::cl) {
83 return cl;
84 } else {
85 assert(false);
86 }
87 assert(false);
88 exit(-1);
89 }
90
SQLiteStats(std::string _filename)91 SQLiteStats::SQLiteStats(std::string _filename) :
92 filename(_filename)
93 {
94 }
95
get_columns(const char * tablename)96 vector<string> SQLiteStats::get_columns(const char* tablename)
97 {
98 vector<string> ret;
99
100 std::stringstream q;
101 q << "pragma table_info(" << tablename << ");";
102
103 sqlite3_stmt *stmt;
104 if (sqlite3_prepare_v2(db, q.str().c_str(), -1, &stmt, NULL)) {
105 cerr << "ERROR: Couln't create table structure for SQLite: "
106 << sqlite3_errmsg(db)
107 << endl;
108 std::exit(-1);
109 }
110
111 sqlite3_bind_int(stmt, 1, 16);
112 int rc;
113 while ( (rc = sqlite3_step(stmt)) == SQLITE_ROW) {
114 ret.push_back(string((const char*)sqlite3_column_text(stmt, 1)));
115 }
116 sqlite3_finalize(stmt);
117
118 return ret;
119 }
120
del_prepared_stmt(sqlite3_stmt * stmt)121 void SQLiteStats::del_prepared_stmt(sqlite3_stmt* stmt)
122 {
123 if (stmt == NULL) {
124 return;
125 }
126
127 int ret = sqlite3_finalize(stmt);
128 if (ret != SQLITE_OK) {
129 cout << "Error closing prepared statement" << endl;
130 std::exit(-1);
131 }
132 }
133
134
~SQLiteStats()135 SQLiteStats::~SQLiteStats()
136 {
137 if (!setup_ok)
138 return;
139
140 //Free all the prepared statements
141 del_prepared_stmt(stmtRst);
142 del_prepared_stmt(stmtVarRst);
143 del_prepared_stmt(stmtClRst);
144 del_prepared_stmt(stmtFeat);
145 del_prepared_stmt(stmtReduceDB);
146 del_prepared_stmt(stmtTimePassed);
147 del_prepared_stmt(stmtMemUsed);
148 del_prepared_stmt(stmt_clause_stats);
149 del_prepared_stmt(stmt_delete_cl);
150 del_prepared_stmt(stmt_var_data_picktime);
151 del_prepared_stmt(stmt_var_data_fintime);
152 del_prepared_stmt(stmt_dec_var_clid);
153 del_prepared_stmt(stmt_var_dist);
154
155 //Close clonnection
156 sqlite3_close(db);
157 }
158
setup(const Solver * solver)159 bool SQLiteStats::setup(const Solver* solver)
160 {
161 setup_ok = connectServer(solver);
162 if (!setup_ok) {
163 return false;
164 }
165
166 //TODO check if data is in any table
167 if (sqlite3_exec(db, cmsat_tablestructure_sql, NULL, NULL, NULL)) {
168 cerr << "ERROR: Couln't create table structure for SQLite: "
169 << sqlite3_errmsg(db)
170 << endl;
171 std::exit(-1);
172 }
173
174 add_solverrun(solver);
175 addStartupData();
176 init("timepassed", &stmtTimePassed);
177 init("memused", &stmtMemUsed);
178 init("satzilla_features", &stmtFeat);
179 init("clause_stats", &stmt_clause_stats);
180 init("restart", &stmtRst);
181 init("restart_dat_for_var", &stmtVarRst);
182 init("restart_dat_for_cl", &stmtClRst);
183 init("reduceDB", &stmtReduceDB);
184 #ifdef STATS_NEEDED
185 init("var_data_fintime", &stmt_var_data_fintime);
186 init("var_data_picktime", &stmt_var_data_picktime);
187 init("dec_var_clid", &stmt_dec_var_clid);
188 init("cl_last_in_solver", &stmt_delete_cl);
189 init("var_dist", &stmt_var_dist);
190 #endif
191
192 return true;
193 }
194
195
file_exists(const std::string & name)196 bool file_exists (const std::string& name) {
197 std::ifstream f(name.c_str());
198 return f.good();
199 }
200
201
connectServer(const Solver * solver)202 bool SQLiteStats::connectServer(const Solver* solver)
203 {
204 if (file_exists(filename) && !solver->conf.sql_overwrite_file) {
205 cout << "ERROR -- the database already exists: " << filename << endl;
206 cout << "ERROR -- We cannot store more than one run in the same database"
207 << endl
208 << "Exiting." << endl;
209 exit(-1);
210 }
211
212 int rc = sqlite3_open(filename.c_str(), &db);
213 if(rc) {
214 cout << "c Cannot open sqlite database: " << sqlite3_errmsg(db) << endl;
215 sqlite3_close(db);
216 return false;
217 }
218
219 if (sqlite3_exec(db, "PRAGMA synchronous = OFF", NULL, NULL, NULL)) {
220 cerr << "ERROR: Problem setting pragma synchronous = OFF to SQLite DB" << endl;
221 cerr << "c " << sqlite3_errmsg(db) << endl;
222 std::exit(-1);
223 }
224
225 if (sqlite3_exec(db, "PRAGMA journal_mode = MEMORY", NULL, NULL, NULL)) {
226 cerr << "ERROR: Problem setting pragma journal_mode = MEMORY to SQLite DB" << endl;
227 cerr << "c " << sqlite3_errmsg(db) << endl;
228 std::exit(-1);
229 }
230
231
232 if (solver->conf.verbosity) {
233 cout << "c writing to SQLite file: " << filename << endl;
234 }
235
236 return true;
237 }
238
begin_transaction()239 void SQLiteStats::begin_transaction()
240 {
241 if (sqlite3_exec(db, "BEGIN TRANSACTION", NULL, NULL, NULL)) {
242 cerr << "ERROR: Beginning SQLITE transaction" << endl;
243 cerr << "c " << sqlite3_errmsg(db) << endl;
244 std::exit(-1);
245 }
246 }
247
end_transaction()248 void SQLiteStats::end_transaction()
249 {
250 if (sqlite3_exec(db, "END TRANSACTION", NULL, NULL, NULL)) {
251 cerr << "ERROR: Beginning SQLITE transaction" << endl;
252 cerr << "c " << sqlite3_errmsg(db) << endl;
253 std::exit(-1);
254 }
255 }
256
add_solverrun(const Solver * solver)257 bool SQLiteStats::add_solverrun(const Solver* solver)
258 {
259 std::stringstream ss;
260 ss
261 << "INSERT INTO solverRun (`runtime`, `gitrev`) values ("
262 << time(NULL)
263 << ", '" << solver->get_version_sha1() << "'"
264 << ");";
265
266 //Inserting element into solverruns to get unique ID
267 const int rc = sqlite3_exec(db, ss.str().c_str(), NULL, NULL, NULL);
268 if (rc) {
269 if (solver->getConf().verbosity >= 6) {
270 cerr << "c ERROR Couldn't insert into table 'solverruns'" << endl;
271 cerr << "c " << sqlite3_errmsg(db) << endl;
272 }
273
274 return false;
275 }
276
277 return true;
278 }
279
add_tag(const std::pair<string,string> & tag)280 void SQLiteStats::add_tag(const std::pair<string, string>& tag)
281 {
282 std::stringstream ss;
283 ss
284 << "INSERT INTO `tags` (`name`, `val`) VALUES("
285 << "'" << tag.first << "'"
286 << ", '" << tag.second << "'"
287 << ");";
288
289 //Inserting element into solverruns to get unique ID
290 if (sqlite3_exec(db, ss.str().c_str(), NULL, NULL, NULL)) {
291 cerr << "SQLite: ERROR Couldn't insert into table 'tags'" << endl;
292 assert(false);
293 std::exit(-1);
294 }
295 }
296
addStartupData()297 void SQLiteStats::addStartupData()
298 {
299 std::stringstream ss;
300 ss
301 << "INSERT INTO `startup` (`startTime`) VALUES ("
302 << "datetime('now')"
303 << ");";
304
305 if (sqlite3_exec(db, ss.str().c_str(), NULL, NULL, NULL)) {
306 cerr << "ERROR Couldn't insert into table 'startup' : "
307 << sqlite3_errmsg(db) << endl;
308
309 std::exit(-1);
310 }
311 }
312
finishup(const lbool status)313 void SQLiteStats::finishup(const lbool status)
314 {
315 std::stringstream ss;
316 ss
317 << "INSERT INTO `finishup` (`endTime`, `status`) VALUES ("
318 << "datetime('now') , "
319 << "'" << status << "'"
320 << ");";
321
322 if (sqlite3_exec(db, ss.str().c_str(), NULL, NULL, NULL)) {
323 cerr << "ERROR Couldn't insert into table 'finishup'" << endl;
324 std::exit(-1);
325 }
326 }
327
writeQuestionMarks(size_t num,std::stringstream & ss)328 void SQLiteStats::writeQuestionMarks(
329 size_t num
330 , std::stringstream& ss
331 ) {
332 ss << "(";
333 for(size_t i = 0
334 ; i < num
335 ; i++
336 ) {
337 if (i < num-1)
338 ss << "?,";
339 else
340 ss << "?";
341 }
342 ss << ")";
343 }
344
run_sqlite_step(sqlite3_stmt * stmt,const char * name)345 void SQLiteStats::run_sqlite_step(sqlite3_stmt* stmt, const char* name)
346 {
347 int rc = sqlite3_step(stmt);
348 if (rc != SQLITE_DONE) {
349 cout
350 << "ERROR: while executing '" << name << "' SQLite prepared statement"
351 << endl;
352
353 cout << "Error from sqlite: "
354 << sqlite3_errmsg(db)
355 << endl;
356 cout << "Error code from sqlite: " << rc << endl;
357 std::exit(-1);
358 }
359
360 if (sqlite3_reset(stmt)) {
361 cerr << "Error calling sqlite3_reset on cl_last_in_solver" << endl;
362 std::exit(-1);
363 }
364
365 if (sqlite3_clear_bindings(stmt)) {
366 cerr << "Error calling sqlite3_clear_bindings on '"
367 << name << "'" << endl;
368 std::exit(-1);
369 }
370 }
371
372
init(const char * name,sqlite3_stmt ** stmt)373 void SQLiteStats::init(const char* name, sqlite3_stmt** stmt)
374 {
375 vector<string> cols = get_columns(name);
376 const size_t numElems = cols.size();
377
378 std::stringstream ss;
379 ss << "insert into `" << name << "` (";
380 for(uint32_t i = 0; i < cols.size(); i++) {
381 if (i > 0) {
382 ss << ", ";
383 }
384 ss << "`" << cols[i] << "`";
385 }
386 ss << ") values ";
387 writeQuestionMarks(
388 numElems
389 , ss
390 );
391 ss << ";";
392
393 //Prepare the statement
394 if (sqlite3_prepare(db, ss.str().c_str(), -1, stmt, NULL)) {
395 cerr << "ERROR in sqlite_stmt_prepare(), INSERT failed"
396 << endl
397 << sqlite3_errmsg(db)
398 << endl
399 << "Query was: " << ss.str()
400 << endl;
401 std::exit(-1);
402 }
403 }
404
mem_used(const Solver * solver,const string & name,double given_time,uint64_t mem_used_mb)405 void SQLiteStats::mem_used(
406 const Solver* solver
407 , const string& name
408 , double given_time
409 , uint64_t mem_used_mb
410 ) {
411 int bindAt = 1;
412 //Position
413 sqlite3_bind_int64(stmtMemUsed, bindAt++, solver->get_solve_stats().num_simplify);
414 sqlite3_bind_int64(stmtMemUsed, bindAt++, solver->sumConflicts);
415 sqlite3_bind_double(stmtMemUsed, bindAt++, given_time);
416 //memory stats
417 sqlite3_bind_text(stmtMemUsed, bindAt++, name.c_str(), -1, NULL);
418 sqlite3_bind_int(stmtMemUsed, bindAt++, mem_used_mb);
419
420 run_sqlite_step(stmtMemUsed, "memused");
421 }
422
time_passed(const Solver * solver,const string & name,double time_passed,bool time_out,double percent_time_remain)423 void SQLiteStats::time_passed(
424 const Solver* solver
425 , const string& name
426 , double time_passed
427 , bool time_out
428 , double percent_time_remain
429 ) {
430
431 int bindAt = 1;
432 sqlite3_bind_int64(stmtTimePassed, bindAt++, solver->get_solve_stats().num_simplify);
433 sqlite3_bind_int64(stmtTimePassed, bindAt++, solver->sumConflicts);
434 sqlite3_bind_double(stmtTimePassed, bindAt++, cpuTime());
435 sqlite3_bind_text(stmtTimePassed, bindAt++, name.c_str(), -1, NULL);
436 sqlite3_bind_double(stmtTimePassed, bindAt++, time_passed);
437 sqlite3_bind_int(stmtTimePassed, bindAt++, time_out);
438 sqlite3_bind_double(stmtTimePassed, bindAt++, percent_time_remain);
439
440 run_sqlite_step(stmtTimePassed, "timepassed");
441 }
442
time_passed_min(const Solver * solver,const string & name,double time_passed)443 void SQLiteStats::time_passed_min(
444 const Solver* solver
445 , const string& name
446 , double time_passed
447 ) {
448 int bindAt = 1;
449 sqlite3_bind_int64(stmtTimePassed, bindAt++, solver->get_solve_stats().num_simplify);
450 sqlite3_bind_int64(stmtTimePassed, bindAt++, solver->sumConflicts);
451 sqlite3_bind_double(stmtTimePassed, bindAt++, cpuTime());
452 sqlite3_bind_text(stmtTimePassed, bindAt++, name.c_str(), -1, NULL);
453 sqlite3_bind_double(stmtTimePassed, bindAt++, time_passed);
454 sqlite3_bind_null(stmtTimePassed, bindAt++);
455 sqlite3_bind_null(stmtTimePassed, bindAt++);
456
457 run_sqlite_step(stmtTimePassed, "time_passed_min");
458 }
459
satzilla_features(const Solver * solver,const Searcher * search,const SatZillaFeatures & satzilla_feat)460 void SQLiteStats::satzilla_features(
461 const Solver* solver
462 , const Searcher* search
463 , const SatZillaFeatures& satzilla_feat
464 ) {
465 int bindAt = 1;
466 sqlite3_bind_int64(stmtFeat, bindAt++, solver->get_solve_stats().num_simplify);
467 sqlite3_bind_int64(stmtFeat, bindAt++, search->sumRestarts());
468 sqlite3_bind_int64(stmtFeat, bindAt++, solver->sumConflicts);
469 sqlite3_bind_int(stmtFeat, bindAt++, solver->latest_satzilla_feature_calc);
470
471 sqlite3_bind_int64(stmtFeat, bindAt++, (uint64_t)satzilla_feat.numVars);
472 sqlite3_bind_int64(stmtFeat, bindAt++, (uint64_t)satzilla_feat.numClauses);
473 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.var_cl_ratio);
474
475 //Clause distribution
476 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.binary);
477 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.horn);
478 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.horn_mean);
479 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.horn_std);
480 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.horn_min);
481 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.horn_max);
482 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.horn_spread);
483
484 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.vcg_var_mean);
485 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.vcg_var_std);
486 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.vcg_var_min);
487 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.vcg_var_max);
488 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.vcg_var_spread);
489
490 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.vcg_cls_mean);
491 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.vcg_cls_std);
492 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.vcg_cls_min);
493 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.vcg_cls_max);
494 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.vcg_cls_spread);
495
496 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.pnr_var_mean);
497 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.pnr_var_std);
498 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.pnr_var_min);
499 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.pnr_var_max);
500 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.pnr_var_spread);
501
502 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.pnr_cls_mean);
503 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.pnr_cls_std);
504 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.pnr_cls_min);
505 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.pnr_cls_max);
506 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.pnr_cls_spread);
507
508 //Conflict clauses
509 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.avg_confl_size);
510 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.confl_size_min);
511 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.confl_size_max);
512 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.avg_confl_glue);
513 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.confl_glue_min);
514 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.confl_glue_max);
515 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.avg_num_resolutions);
516 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.num_resolutions_min);
517 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.num_resolutions_max);
518 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.learnt_bins_per_confl);
519
520 //Search
521 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.avg_branch_depth);
522 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.branch_depth_min);
523 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.branch_depth_max);
524 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.avg_trail_depth_delta);
525 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.trail_depth_delta_min);
526 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.trail_depth_delta_max);
527 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.avg_branch_depth_delta);
528 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.props_per_confl);
529 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.confl_per_restart);
530 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.decisions_per_conflict);
531
532 //red stats
533 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.red_cl_distrib.glue_distr_mean);
534 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.red_cl_distrib.glue_distr_var);
535 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.red_cl_distrib.size_distr_mean);
536 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.red_cl_distrib.size_distr_var);
537 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.red_cl_distrib.activity_distr_mean);
538 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.red_cl_distrib.activity_distr_var);
539
540 //irred stats
541 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.irred_cl_distrib.glue_distr_mean);
542 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.irred_cl_distrib.glue_distr_var);
543 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.irred_cl_distrib.size_distr_mean);
544 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.irred_cl_distrib.size_distr_var);
545 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.irred_cl_distrib.activity_distr_mean);
546 sqlite3_bind_double(stmtFeat, bindAt++, satzilla_feat.irred_cl_distrib.activity_distr_var);
547
548 run_sqlite_step(stmtFeat, "satzilla_features");
549 }
550
551 #ifdef STATS_NEEDED
restart(const uint32_t restartID,const Restart rest_type,const PropStats & thisPropStats,const SearchStats & thisStats,const Solver * solver,const Searcher * search,const rst_dat_type type,const int64_t clauseID)552 void SQLiteStats::restart(
553 const uint32_t restartID
554 , const Restart rest_type
555 , const PropStats& thisPropStats
556 , const SearchStats& thisStats
557 , const Solver* solver
558 , const Searcher* search
559 , const rst_dat_type type
560 , const int64_t clauseID
561 ) {
562 sqlite3_stmt* stmt;
563 if (type == rst_dat_type::norm) {
564 stmt = stmtRst;
565 } else if (type == rst_dat_type::var) {
566 stmt = stmtVarRst;
567 } else if (type == rst_dat_type::cl) {
568 stmt = stmtClRst;
569 } else {
570 assert(false);
571 }
572
573 const SearchHist& searchHist = search->getHistory();
574 const BinTriStats& binTri = solver->getBinTriStats();
575
576 int bindAt = 1;
577 sqlite3_bind_int64(stmt, bindAt++, restartID);
578 if (clauseID == -1) {
579 sqlite3_bind_null(stmt, bindAt++);
580 } else {
581 sqlite3_bind_int64(stmt, bindAt++, clauseID);
582 }
583 sqlite3_bind_int64(stmt, bindAt++, solver->get_solve_stats().num_simplify);
584 sqlite3_bind_int64(stmt, bindAt++, search->sumRestarts());
585 sqlite3_bind_int64(stmt, bindAt++, solver->sumConflicts);
586 sqlite3_bind_int(stmt, bindAt++, searchHist.num_conflicts_this_restart);
587 sqlite3_bind_int(stmt, bindAt++, solver->latest_satzilla_feature_calc);
588 sqlite3_bind_double(stmt, bindAt++, cpuTime());
589
590
591 sqlite3_bind_int64(stmt, bindAt++, binTri.irredBins);
592 sqlite3_bind_int64(stmt, bindAt++, solver->get_num_long_irred_cls());
593 sqlite3_bind_int64(stmt, bindAt++, binTri.redBins);
594 sqlite3_bind_int64(stmt, bindAt++, solver->get_num_long_red_cls());
595
596 sqlite3_bind_int64(stmt, bindAt++, solver->litStats.irredLits);
597 sqlite3_bind_int64(stmt, bindAt++, solver->litStats.redLits);
598
599 //Conflict stats
600 bind_null_or_double(stmt, bindAt, searchHist.glueHist.getLongtTerm(),avg);
601 sqlite3_bind_double(stmt, bindAt++, std:: sqrt(searchHist.glueHist.getLongtTerm().var()));
602 bind_null_or_double(stmt, bindAt, searchHist.glueHist.getLongtTerm(),getMin);
603 bind_null_or_double(stmt, bindAt, searchHist.glueHist.getLongtTerm(),getMax);
604
605 bind_null_or_double(stmt, bindAt, searchHist.conflSizeHist, avg);
606 sqlite3_bind_double(stmt, bindAt++, std:: sqrt(searchHist.conflSizeHist.var()));
607 bind_null_or_double(stmt, bindAt, searchHist.conflSizeHist,getMin);
608 bind_null_or_double(stmt, bindAt, searchHist.conflSizeHist,getMax);
609
610 bind_null_or_double(stmt, bindAt, searchHist.numResolutionsHist, avg);
611 sqlite3_bind_double(stmt, bindAt++, std:: sqrt(searchHist.numResolutionsHist.var()));
612 bind_null_or_double(stmt, bindAt, searchHist.numResolutionsHist,getMin);
613 bind_null_or_double(stmt, bindAt, searchHist.numResolutionsHist,getMax);
614
615 //Search stats
616 bind_null_or_double(stmt, bindAt, searchHist.branchDepthHist,avg);
617 sqlite3_bind_double(stmt, bindAt++, std:: sqrt(searchHist.branchDepthHist.var()));
618 bind_null_or_double(stmt, bindAt, searchHist.branchDepthHist,getMin);
619 bind_null_or_double(stmt, bindAt, searchHist.branchDepthHist,getMax);
620
621 bind_null_or_double(stmt, bindAt, searchHist.branchDepthDeltaHist,avg);
622 sqlite3_bind_double(stmt, bindAt++, std:: sqrt(searchHist.branchDepthDeltaHist.var()));
623 bind_null_or_double(stmt, bindAt, searchHist.branchDepthDeltaHist,getMin);
624 bind_null_or_double(stmt, bindAt, searchHist.branchDepthDeltaHist,getMax);
625
626 bind_null_or_double(stmt, bindAt, searchHist.trailDepthHist.getLongtTerm(),avg);
627 sqlite3_bind_double(stmt, bindAt++, std:: sqrt(searchHist.trailDepthHist.getLongtTerm().var()));
628 bind_null_or_double(stmt, bindAt, searchHist.trailDepthHist.getLongtTerm(),getMin);
629 bind_null_or_double(stmt, bindAt, searchHist.trailDepthHist.getLongtTerm(),getMax);
630
631 bind_null_or_double(stmt, bindAt, searchHist.trailDepthDeltaHist,avg);
632 sqlite3_bind_double(stmt, bindAt++, std:: sqrt(searchHist.trailDepthDeltaHist.var()));
633 bind_null_or_double(stmt, bindAt, searchHist.trailDepthDeltaHist,getMin);
634 bind_null_or_double(stmt, bindAt, searchHist.trailDepthDeltaHist,getMax);
635
636 //Prop
637 sqlite3_bind_int64(stmt, bindAt++, thisPropStats.propsBinIrred);
638 sqlite3_bind_int64(stmt, bindAt++, thisPropStats.propsBinRed);
639 sqlite3_bind_int64(stmt, bindAt++, thisPropStats.propsLongIrred);
640 sqlite3_bind_int64(stmt, bindAt++, thisPropStats.propsLongRed);
641
642 //Confl
643 sqlite3_bind_int64(stmt, bindAt++, thisStats.conflStats.conflsBinIrred);
644 sqlite3_bind_int64(stmt, bindAt++, thisStats.conflStats.conflsBinRed);
645 sqlite3_bind_int64(stmt, bindAt++, thisStats.conflStats.conflsLongIrred);
646 sqlite3_bind_int64(stmt, bindAt++, thisStats.conflStats.conflsLongRed);
647
648 //Red
649 sqlite3_bind_int64(stmt, bindAt++, thisStats.learntUnits);
650 sqlite3_bind_int64(stmt, bindAt++, thisStats.learntBins);
651 sqlite3_bind_int64(stmt, bindAt++, thisStats.learntLongs);
652
653 //Resolv stats
654 sqlite3_bind_int64(stmt, bindAt++, thisStats.resolvs.binIrred);
655 sqlite3_bind_int64(stmt, bindAt++, thisStats.resolvs.binRed);
656 sqlite3_bind_int64(stmt, bindAt++, thisStats.resolvs.longIrred);
657 sqlite3_bind_int64(stmt, bindAt++, thisStats.resolvs.longRed);
658
659
660 //Var stats
661 sqlite3_bind_int64(stmt, bindAt++, thisPropStats.propagations);
662 sqlite3_bind_int64(stmt, bindAt++, thisStats.decisions);
663
664 sqlite3_bind_int64(stmt, bindAt++, thisPropStats.varFlipped);
665 sqlite3_bind_int64(stmt, bindAt++, thisPropStats.varSetPos);
666 sqlite3_bind_int64(stmt, bindAt++, thisPropStats.varSetNeg);
667 sqlite3_bind_int64(stmt, bindAt++, solver->get_num_free_vars());
668 sqlite3_bind_int64(stmt, bindAt++, solver->varReplacer->get_num_replaced_vars());
669 sqlite3_bind_int64(stmt, bindAt++, solver->get_num_vars_elimed());
670 sqlite3_bind_int64(stmt, bindAt++, search->getTrailSize());
671
672 //strategy
673 sqlite3_bind_int(stmt, bindAt++, branch_type_to_int(solver->branch_strategy));
674 sqlite3_bind_int(stmt, bindAt++, restart_type_to_int(rest_type));
675
676 run_sqlite_step(stmt, rst_dat_type_to_str(type));
677 }
678
reduceDB(const Solver * solver,const bool locked,const Clause * cl,const string & cur_restart_type,const uint32_t act_ranking_top_10,const uint32_t act_ranking,const uint32_t tot_cls_in_db)679 void SQLiteStats::reduceDB(
680 const Solver* solver
681 , const bool locked
682 , const Clause* cl
683 , const string& cur_restart_type
684 , const uint32_t act_ranking_top_10
685 , const uint32_t act_ranking
686 , const uint32_t tot_cls_in_db
687 ) {
688 assert(cl->stats.dump_no != std::numeric_limits<uint16_t>::max());
689
690 int bindAt = 1;
691 sqlite3_bind_int64(stmtReduceDB, bindAt++, solver->get_solve_stats().num_simplify);
692 sqlite3_bind_int64(stmtReduceDB, bindAt++, solver->sumRestarts());
693 sqlite3_bind_int64(stmtReduceDB, bindAt++, solver->sumConflicts);
694 sqlite3_bind_int64(stmtReduceDB, bindAt++, solver->latest_satzilla_feature_calc);
695 sqlite3_bind_text(stmtReduceDB, bindAt++, cur_restart_type.c_str(), -1, NULL);
696 sqlite3_bind_double(stmtReduceDB, bindAt++, cpuTime());
697
698 //data
699 sqlite3_bind_int64(stmtReduceDB, bindAt++, cl->stats.ID);
700 sqlite3_bind_int64(stmtReduceDB, bindAt++, cl->stats.dump_no);
701 sqlite3_bind_int64(stmtReduceDB, bindAt++, cl->stats.conflicts_made);
702 sqlite3_bind_int64(stmtReduceDB, bindAt++, cl->stats.propagations_made);
703 sqlite3_bind_int64(stmtReduceDB, bindAt++, cl->stats.sum_propagations_made);
704 sqlite3_bind_int64(stmtReduceDB, bindAt++, cl->stats.clause_looked_at);
705 sqlite3_bind_int64(stmtReduceDB, bindAt++, cl->stats.used_for_uip_creation);
706
707 int64_t last_touched_diff = solver->sumConflicts-cl->stats.last_touched;
708 sqlite3_bind_int64(stmtReduceDB, bindAt++, last_touched_diff);
709
710 sqlite3_bind_double(stmtReduceDB, bindAt++, (double)cl->stats.activity/(double)solver->get_cla_inc());
711 sqlite3_bind_int(stmtReduceDB, bindAt++, locked);
712 sqlite3_bind_int(stmtReduceDB, bindAt++, cl->used_in_xor());
713 sqlite3_bind_int(stmtReduceDB, bindAt++, cl->stats.glue);
714 sqlite3_bind_int(stmtReduceDB, bindAt++, cl->size());
715 sqlite3_bind_int(stmtReduceDB, bindAt++, cl->stats.ttl);
716 sqlite3_bind_int(stmtReduceDB, bindAt++, cl->is_ternary_resolvent);
717 sqlite3_bind_int(stmtReduceDB, bindAt++, act_ranking_top_10);
718 sqlite3_bind_int(stmtReduceDB, bindAt++, act_ranking);
719 sqlite3_bind_int(stmtReduceDB, bindAt++, tot_cls_in_db);
720 sqlite3_bind_int(stmtReduceDB, bindAt++, cl->stats.sum_uip1_used);
721
722 run_sqlite_step(stmtReduceDB, "reduceDB");
723 }
724
dump_clause_stats(const Solver * solver,uint64_t clid,const uint64_t restartID,uint32_t orig_glue,uint32_t glue_before_minim,uint32_t backtrack_level,uint32_t size,AtecedentData<uint16_t> antec_data,size_t decision_level,size_t trail_depth,uint64_t conflicts_this_restart,const std::string & restart_type,const SearchHist & hist,const bool is_decision)725 void SQLiteStats::dump_clause_stats(
726 const Solver* solver
727 , uint64_t clid
728 , const uint64_t restartID
729 , uint32_t orig_glue
730 , uint32_t glue_before_minim
731 , uint32_t backtrack_level
732 , uint32_t size
733 , AtecedentData<uint16_t> antec_data
734 , size_t decision_level
735 , size_t trail_depth
736 , uint64_t conflicts_this_restart
737 , const std::string& restart_type
738 , const SearchHist& hist
739 , const bool is_decision
740 ) {
741 uint32_t num_overlap_literals = antec_data.sum_size()-(antec_data.num()-1)-size;
742
743 int bindAt = 1;
744 sqlite3_bind_int64(stmt_clause_stats, bindAt++, solver->get_solve_stats().num_simplify);
745 sqlite3_bind_int64(stmt_clause_stats, bindAt++, solver->sumRestarts());
746 if (solver->sumRestarts() == 0) {
747 sqlite3_bind_int64(stmt_clause_stats, bindAt++, 0);
748 } else {
749 sqlite3_bind_int64(stmt_clause_stats, bindAt++, solver->sumRestarts()-1);
750 }
751 sqlite3_bind_int64 (stmt_clause_stats, bindAt++, solver->sumConflicts);
752 sqlite3_bind_int (stmt_clause_stats, bindAt++, solver->latest_satzilla_feature_calc);
753 sqlite3_bind_int64 (stmt_clause_stats, bindAt++, clid);
754 sqlite3_bind_int (stmt_clause_stats, bindAt++, restartID);
755
756 sqlite3_bind_int (stmt_clause_stats, bindAt++, orig_glue);
757 sqlite3_bind_int (stmt_clause_stats, bindAt++, glue_before_minim);
758 sqlite3_bind_int (stmt_clause_stats, bindAt++, size);
759 sqlite3_bind_int64 (stmt_clause_stats, bindAt++, conflicts_this_restart);
760 sqlite3_bind_int (stmt_clause_stats, bindAt++, num_overlap_literals);
761 sqlite3_bind_int (stmt_clause_stats, bindAt++, antec_data.num());
762 sqlite3_bind_int (stmt_clause_stats, bindAt++, antec_data.sum_size());
763 sqlite3_bind_int (stmt_clause_stats, bindAt++, is_decision);
764
765 sqlite3_bind_int (stmt_clause_stats, bindAt++, backtrack_level);
766 sqlite3_bind_int64 (stmt_clause_stats, bindAt++, decision_level);
767 sqlite3_bind_int64 (stmt_clause_stats, bindAt++, hist.branchDepthHistQueue.prev(1));
768 sqlite3_bind_int64 (stmt_clause_stats, bindAt++, hist.branchDepthHistQueue.prev(2));
769 sqlite3_bind_int64 (stmt_clause_stats, bindAt++, trail_depth);
770 sqlite3_bind_text (stmt_clause_stats, bindAt++, restart_type.c_str(), -1, NULL);
771
772 sqlite3_bind_int (stmt_clause_stats, bindAt++, antec_data.binIrred);
773 sqlite3_bind_int (stmt_clause_stats, bindAt++, antec_data.binRed);
774 sqlite3_bind_int (stmt_clause_stats, bindAt++, antec_data.longIrred);
775 sqlite3_bind_int (stmt_clause_stats, bindAt++, antec_data.longRed);
776
777 bind_null_or_double(stmt_clause_stats, bindAt, antec_data.glue_long_reds,avg);
778 bind_null_or_double(stmt_clause_stats, bindAt, antec_data.glue_long_reds,avg);
779 bind_null_or_double(stmt_clause_stats, bindAt, antec_data.glue_long_reds,var);
780 bind_null_or_int (stmt_clause_stats, bindAt, antec_data.glue_long_reds,getMin);
781 bind_null_or_int (stmt_clause_stats, bindAt, antec_data.glue_long_reds,getMax);
782
783 bind_null_or_double(stmt_clause_stats, bindAt, antec_data.age_long_reds,avg);
784 bind_null_or_double(stmt_clause_stats, bindAt, antec_data.age_long_reds,var);
785 bind_null_or_int64 (stmt_clause_stats, bindAt, antec_data.age_long_reds,getMin);
786 bind_null_or_int64 (stmt_clause_stats, bindAt, antec_data.age_long_reds,getMax);
787
788 bind_null_or_double(stmt_clause_stats, bindAt, hist.decisionLevelHistLT,avg);
789 bind_null_or_double(stmt_clause_stats, bindAt, hist.backtrackLevelHistLT,avg);
790 bind_null_or_double(stmt_clause_stats, bindAt, hist.trailDepthHistLT,avg);
791 bind_null_or_double(stmt_clause_stats, bindAt, hist.conflSizeHistLT,avg);
792 bind_null_or_double(stmt_clause_stats, bindAt, hist.glueHistLT,avg);
793 bind_null_or_double(stmt_clause_stats, bindAt, hist.numResolutionsHistLT,avg);
794
795 bind_null_or_double(stmt_clause_stats, bindAt, hist.antec_data_sum_sizeHistLT,avg);
796 bind_null_or_double(stmt_clause_stats, bindAt, hist.overlapHistLT,avg);
797
798 sqlite3_bind_double(stmt_clause_stats, bindAt++, hist.branchDepthHistQueue.avg_nocheck());
799 sqlite3_bind_double(stmt_clause_stats, bindAt++, hist.trailDepthHist.avg_nocheck());
800 sqlite3_bind_double(stmt_clause_stats, bindAt++, hist.trailDepthHistLonger.avg_nocheck());
801 bind_null_or_double(stmt_clause_stats, bindAt, hist.numResolutionsHist,avg);
802 bind_null_or_double(stmt_clause_stats, bindAt, hist.conflSizeHist,avg);
803 bind_null_or_double(stmt_clause_stats, bindAt, hist.trailDepthDeltaHist,avg);
804 sqlite3_bind_double(stmt_clause_stats, bindAt++, hist.backtrackLevelHist.avg_nocheck());
805 sqlite3_bind_double(stmt_clause_stats, bindAt++, hist.glueHist.avg_nocheck());
806 bind_null_or_double(stmt_clause_stats, bindAt, hist.glueHist.getLongtTerm(),avg);
807
808 run_sqlite_step(stmt_clause_stats, "dump_clause_stats");
809 }
810
811 #ifdef STATS_NEEDED_BRANCH
var_data_fintime(const Solver * solver,const uint32_t var,const VarData & vardata,const double rel_activity)812 void SQLiteStats::var_data_fintime(
813 const Solver* solver
814 , const uint32_t var
815 , const VarData& vardata
816 , const double rel_activity
817 ) {
818 int bindAt = 1;
819 sqlite3_bind_int (stmt_var_data_fintime, bindAt++, var);
820 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, vardata.sumConflicts_at_picktime);
821
822 sqlite3_bind_double (stmt_var_data_fintime, bindAt++, rel_activity);
823
824 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, vardata.inside_conflict_clause);
825 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, vardata.inside_conflict_clause_antecedents);
826 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, vardata.inside_conflict_clause_glue);
827
828 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, solver->sumDecisions);
829 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, solver->sumConflicts);
830 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, solver->sumPropagations);
831 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, solver->sumAntecedents);
832 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, solver->sumAntecedentsLits);
833 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, solver->sumConflictClauseLits);
834 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, solver->sumDecisionBasedCl);
835 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, solver->sumClLBD);
836 sqlite3_bind_int64 (stmt_var_data_fintime, bindAt++, solver->sumClSize);
837
838 run_sqlite_step(stmt_var_data_fintime, "var_data_fintime");
839 }
840
var_data_picktime(const Solver * solver,const uint32_t var,const VarData & vardata,const double rel_activity)841 void SQLiteStats::var_data_picktime(
842 const Solver* solver
843 , const uint32_t var
844 , const VarData& vardata
845 , const double rel_activity
846 ) {
847 int bindAt = 1;
848 sqlite3_bind_int (stmt_var_data_picktime, bindAt++, var);
849 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.level);
850 sqlite3_bind_double(stmt_var_data_picktime, bindAt++, rel_activity);
851 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->latest_vardist_feature_calc);
852
853 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.inside_conflict_clause);
854 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.inside_conflict_clause_antecedents);
855 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.inside_conflict_clause_glue);
856
857 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.inside_conflict_clause_during);
858 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.inside_conflict_clause_antecedents_during);
859 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.inside_conflict_clause_glue_during);
860
861
862 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.num_decided);
863 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.num_decided_pos);
864 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.num_propagated);
865 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.num_propagated_pos);
866
867 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumConflicts-vardata.last_seen_in_1uip);
868 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumConflicts-vardata.last_decided_on);
869 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumConflicts-vardata.last_propagated);
870 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumConflicts-vardata.last_canceled);
871
872
873 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumDecisions);
874 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumConflicts);
875 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumPropagations);
876 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumAntecedents);
877 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumAntecedentsLits);
878 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumConflictClauseLits);
879 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumDecisionBasedCl);
880 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumClLBD);
881 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumClSize);
882
883 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.sumConflicts_below_during);
884 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.sumDecisions_below_during);
885 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.sumPropagations_below_during);
886 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.sumAntecedents_below_during);
887 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.sumAntecedentsLits_below_during);
888 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.sumConflictClauseLits_below_during);
889 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.sumDecisionBasedCl_below_during);
890 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.sumClLBD_below_during);
891 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, vardata.sumClSize_below_during);
892
893 sqlite3_bind_int64 (stmt_var_data_picktime, bindAt++, solver->sumConflicts-vardata.last_flipped);
894
895 run_sqlite_step(stmt_var_data_picktime, "var_data_picktime");
896 }
897
var_dist(const uint32_t var,const VarData2 & data,const Solver * solver)898 void SQLiteStats::var_dist(
899 const uint32_t var
900 , const VarData2& data
901 , const Solver* solver
902 ) {
903 int bindAt = 1;
904 sqlite3_bind_int(stmt_var_dist, bindAt++, var);
905 sqlite3_bind_int64(stmt_var_dist, bindAt++, solver->latest_vardist_feature_calc);
906 sqlite3_bind_int64(stmt_var_dist, bindAt++, solver->sumConflicts);
907
908 sqlite3_bind_int64(stmt_var_dist, bindAt++, solver->longIrredCls.size());
909 uint32_t num = 0;
910 for(auto& x: solver->longRedCls) {
911 num+=x.size();
912 }
913 sqlite3_bind_int64(stmt_var_dist, bindAt++, num);
914 sqlite3_bind_int64(stmt_var_dist, bindAt++, solver->binTri.irredBins);
915 sqlite3_bind_int64(stmt_var_dist, bindAt++, solver->binTri.redBins);
916
917
918 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.red.num_times_in_bin_clause);
919 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.red.num_times_in_long_clause);
920 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.red.satisfies_cl);
921 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.red.falsifies_cl);
922 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.red.tot_num_lit_of_bin_it_appears_in);
923 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.red.tot_num_lit_of_long_cls_it_appears_in);
924 sqlite3_bind_double(stmt_var_dist, bindAt++, data.red.sum_var_act_of_cls);
925
926 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.irred.num_times_in_bin_clause);
927 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.irred.num_times_in_long_clause);
928 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.irred.satisfies_cl);
929 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.irred.falsifies_cl);
930 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.irred.tot_num_lit_of_bin_it_appears_in);
931 sqlite3_bind_int64(stmt_var_dist, bindAt++, data.irred.tot_num_lit_of_long_cls_it_appears_in);
932 sqlite3_bind_double(stmt_var_dist, bindAt++, data.irred.sum_var_act_of_cls);
933
934 sqlite3_bind_double(stmt_var_dist, bindAt++, data.tot_act_long_red_cls);
935
936 run_sqlite_step(stmt_var_dist, "var_dist");
937 }
938
dec_var_clid(const uint32_t var,const uint64_t sumConflicts_at_picktime,const uint64_t clid)939 void SQLiteStats::dec_var_clid(
940 const uint32_t var
941 , const uint64_t sumConflicts_at_picktime
942 , const uint64_t clid
943 ) {
944 assert(clid != 0);
945
946 int bindAt = 1;
947 sqlite3_bind_int(stmt_dec_var_clid, bindAt++, var);
948 sqlite3_bind_int64(stmt_dec_var_clid, bindAt++, sumConflicts_at_picktime);
949 sqlite3_bind_int64(stmt_dec_var_clid, bindAt++, clid);
950
951 run_sqlite_step(stmt_dec_var_clid, "dec_var_clid");
952 }
953 #endif
954
cl_last_in_solver(const Solver * solver,const uint64_t clid)955 void SQLiteStats::cl_last_in_solver(
956 const Solver* solver
957 , const uint64_t clid)
958 {
959 assert(clid != 0);
960
961 int bindAt = 1;
962 sqlite3_bind_int64(stmt_delete_cl, bindAt++, solver->sumConflicts);
963 sqlite3_bind_int64(stmt_delete_cl, bindAt++, clid);
964
965 run_sqlite_step(stmt_delete_cl, "cl_last_in_solver");
966 }
967
968 #endif
969