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 "reducedb.h"
24 #include "solver.h"
25 #include "solverconf.h"
26 #include "sqlstats.h"
27 #ifdef FINAL_PREDICTOR
28 #include "cl_predictors.h"
29 #endif
30
31 // #define VERBOSE_DEBUG
32
33 #include <functional>
34 #include <cmath>
35
36 using namespace CMSat;
37
38 struct SortRedClsGlue
39 {
SortRedClsGlueSortRedClsGlue40 explicit SortRedClsGlue(ClauseAllocator& _cl_alloc) :
41 cl_alloc(_cl_alloc)
42 {}
43 ClauseAllocator& cl_alloc;
44
operator ()SortRedClsGlue45 bool operator () (const ClOffset xOff, const ClOffset yOff) const
46 {
47 const Clause* x = cl_alloc.ptr(xOff);
48 const Clause* y = cl_alloc.ptr(yOff);
49 return x->stats.glue < y->stats.glue;
50 }
51 };
52
53 struct SortRedClsSize
54 {
SortRedClsSizeSortRedClsSize55 explicit SortRedClsSize(ClauseAllocator& _cl_alloc) :
56 cl_alloc(_cl_alloc)
57 {}
58 ClauseAllocator& cl_alloc;
59
operator ()SortRedClsSize60 bool operator () (const ClOffset xOff, const ClOffset yOff) const
61 {
62 const Clause* x = cl_alloc.ptr(xOff);
63 const Clause* y = cl_alloc.ptr(yOff);
64 return x->size() < y->size();
65 }
66 };
67
68 struct SortRedClsAct
69 {
SortRedClsActSortRedClsAct70 explicit SortRedClsAct(ClauseAllocator& _cl_alloc) :
71 cl_alloc(_cl_alloc)
72 {}
73 ClauseAllocator& cl_alloc;
74
operator ()SortRedClsAct75 bool operator () (const ClOffset xOff, const ClOffset yOff) const
76 {
77 const Clause* x = cl_alloc.ptr(xOff);
78 const Clause* y = cl_alloc.ptr(yOff);
79 return x->stats.activity > y->stats.activity;
80 }
81 };
82 #ifdef FINAL_PREDICTOR
83 struct SortRedClsPredShort
84 {
SortRedClsPredShortSortRedClsPredShort85 explicit SortRedClsPredShort(ClauseAllocator& _cl_alloc) :
86 cl_alloc(_cl_alloc)
87 {}
88 ClauseAllocator& cl_alloc;
89
operator ()SortRedClsPredShort90 bool operator () (const ClOffset xOff, const ClOffset yOff) const
91 {
92 const Clause* x = cl_alloc.ptr(xOff);
93 const Clause* y = cl_alloc.ptr(yOff);
94 return x->stats.pred_short_use > y->stats.pred_short_use;
95 }
96 };
97
98 struct SortRedClsPredLong
99 {
SortRedClsPredLongSortRedClsPredLong100 explicit SortRedClsPredLong(ClauseAllocator& _cl_alloc) :
101 cl_alloc(_cl_alloc)
102 {}
103 ClauseAllocator& cl_alloc;
104
operator ()SortRedClsPredLong105 bool operator () (const ClOffset xOff, const ClOffset yOff) const
106 {
107 const Clause* x = cl_alloc.ptr(xOff);
108 const Clause* y = cl_alloc.ptr(yOff);
109 return x->stats.pred_long_use > y->stats.pred_long_use;
110 }
111 };
112
113 struct SortRedClsPredForever
114 {
SortRedClsPredForeverSortRedClsPredForever115 explicit SortRedClsPredForever(ClauseAllocator& _cl_alloc) :
116 cl_alloc(_cl_alloc)
117 {}
118 ClauseAllocator& cl_alloc;
119
operator ()SortRedClsPredForever120 bool operator () (const ClOffset xOff, const ClOffset yOff) const
121 {
122 const Clause* x = cl_alloc.ptr(xOff);
123 const Clause* y = cl_alloc.ptr(yOff);
124 return x->stats.pred_forever_use > y->stats.pred_forever_use;
125 }
126 };
127 #endif
128
129
ReduceDB(Solver * _solver)130 ReduceDB::ReduceDB(Solver* _solver) :
131 solver(_solver)
132 {
133 }
134
~ReduceDB()135 ReduceDB::~ReduceDB()
136 {
137 #ifdef FINAL_PREDICTOR
138 delete predictors;
139 #endif
140 }
141
sort_red_cls(ClauseClean clean_type)142 void ReduceDB::sort_red_cls(ClauseClean clean_type)
143 {
144 #ifdef VERBOSE_DEBUG
145 cout << "Before sort" << endl;
146 uint64_t i = 0;
147 for(const auto& x: solver->longRedCls[2]) {
148 const ClOffset offset = x;
149 Clause* cl = solver->cl_alloc.ptr(offset);
150 cout << i << " offset: " << offset << " cl->stats.last_touched: " << cl->stats.last_touched
151 << " act:" << std::setprecision(9) << cl->stats.activity
152 << " which_red_array:" << cl->stats.which_red_array << endl
153 << " -- cl:" << *cl << " tern:" << cl->is_ternary_resolvent
154 << endl;
155 }
156 #endif
157
158 switch (clean_type) {
159 case ClauseClean::glue : {
160 std::sort(solver->longRedCls[2].begin(), solver->longRedCls[2].end(), SortRedClsGlue(solver->cl_alloc));
161 break;
162 }
163
164 case ClauseClean::activity : {
165 std::sort(solver->longRedCls[2].begin(), solver->longRedCls[2].end(), SortRedClsAct(solver->cl_alloc));
166 break;
167 }
168
169 default: {
170 assert(false && "Unknown cleaning type");
171 }
172 }
173 }
174
175 //TODO maybe we chould count binary learnt clauses as well into the
176 //kept no. of clauses as other solvers do
handle_lev2()177 void ReduceDB::handle_lev2()
178 {
179 solver->dump_memory_stats_to_sql();
180 size_t orig_size = solver->longRedCls[2].size();
181
182 const double myTime = cpuTime();
183 assert(solver->watches.get_smudged_list().empty());
184
185 //lev2 -- clean
186 int64_t num_to_reduce = solver->longRedCls[2].size();
187 for(unsigned keep_type = 0
188 ; keep_type < sizeof(solver->conf.ratio_keep_clauses)/sizeof(double)
189 ; keep_type++
190 ) {
191 const uint64_t keep_num = (double)num_to_reduce*solver->conf.ratio_keep_clauses[keep_type];
192 if (keep_num == 0) {
193 continue;
194 }
195 sort_red_cls(static_cast<ClauseClean>(keep_type));
196 mark_top_N_clauses(keep_num);
197 }
198 assert(delayed_clause_free.empty());
199 cl_marked = 0;
200 cl_ttl = 0;
201 cl_locked_solver = 0;
202 remove_cl_from_lev2();
203
204 solver->clean_occur_from_removed_clauses_only_smudged();
205 for(ClOffset offset: delayed_clause_free) {
206 solver->free_cl(offset);
207 }
208 delayed_clause_free.clear();
209
210 #ifdef SLOW_DEBUG
211 solver->check_no_removed_or_freed_cl_in_watch();
212 #endif
213
214 if (solver->conf.verbosity >= 2) {
215 cout << "c [DBclean lev2]"
216 << " confl: " << solver->sumConflicts
217 << " orig size: " << orig_size
218 << " marked: " << cl_marked
219 << " ttl:" << cl_ttl
220 << " locked_solver:" << cl_locked_solver
221 << solver->conf.print_times(cpuTime()-myTime)
222 << endl;
223 }
224
225 if (solver->sqlStats) {
226 solver->sqlStats->time_passed_min(
227 solver
228 , "dbclean-lev2"
229 , cpuTime()-myTime
230 );
231 }
232 total_time += cpuTime()-myTime;
233
234 last_reducedb_num_conflicts = solver->sumConflicts;
235 }
236
237 #ifdef STATS_NEEDED
dump_sql_cl_data(const string & cur_rst_type)238 void ReduceDB::dump_sql_cl_data(
239 const string& cur_rst_type
240 ) {
241 double myTime = cpuTime();
242 assert(solver->sqlStats);
243 solver->sqlStats->begin_transaction();
244 uint64_t added_to_db = 0;
245
246 vector<ClOffset> all_learnt;
247 for(uint32_t lev = 0; lev < solver->longRedCls.size(); lev++) {
248 auto& cc = solver->longRedCls[lev];
249 for(const auto& offs: cc) {
250 Clause* cl = solver->cl_alloc.ptr(offs);
251 assert(!cl->getRemoved());
252 assert(cl->red());
253 assert(!cl->freed());
254 all_learnt.push_back(offs);
255 }
256 }
257
258 std::sort(all_learnt.begin(), all_learnt.end(), SortRedClsAct(solver->cl_alloc));
259 for(size_t i = 0; i < all_learnt.size(); i++) {
260 ClOffset offs = all_learnt[i];
261 Clause* cl = solver->cl_alloc.ptr(offs);
262
263 //Only if selected to be dumped
264 if (cl->stats.ID == 0) {
265 continue;
266 }
267
268 const bool locked = solver->clause_locked(*cl, offs);
269 const uint32_t act_ranking_top_10 = std::ceil((double)i/((double)all_learnt.size()/10.0))+1;
270 //cout << "Ranking top 10: " << act_ranking_top_10 << " act: " << cl->stats.activity << endl;
271 solver->sqlStats->reduceDB(
272 solver
273 , locked
274 , cl
275 , cur_rst_type
276 , act_ranking_top_10
277 , i+1
278 , all_learnt.size()
279 );
280 added_to_db++;
281 cl->stats.dump_no++;
282 cl->stats.reset_rdb_stats();
283 }
284 solver->sqlStats->end_transaction();
285
286 if (solver->conf.verbosity) {
287 cout << "c [sql] added to DB " << added_to_db
288 << " dump-ratio: " << solver->conf.dump_individual_cldata_ratio
289 << solver->conf.print_times(cpuTime()-myTime)
290 << endl;
291 }
292 }
293 #endif
294
handle_lev1()295 void ReduceDB::handle_lev1()
296 {
297 #ifdef VERBOSE_DEBUG
298 cout << "c handle_lev1()" << endl;
299 #endif
300
301 uint32_t moved_w0 = 0;
302 uint32_t used_recently = 0;
303 uint32_t non_recent_use = 0;
304 double myTime = cpuTime();
305 size_t orig_size = solver->longRedCls[1].size();
306
307 size_t j = 0;
308 for(size_t i = 0
309 ; i < solver->longRedCls[1].size()
310 ; i++
311 ) {
312 const ClOffset offset = solver->longRedCls[1][i];
313 Clause* cl = solver->cl_alloc.ptr(offset);
314 #ifdef VERBOSE_DEBUG
315 cout << "offset: " << offset << " cl->stats.last_touched: " << cl->stats.last_touched
316 << " act:" << std::setprecision(9) << cl->stats.activity
317 << " which_red_array:" << cl->stats.which_red_array << endl
318 << " -- cl:" << *cl << " tern:" << cl->is_ternary_resolvent
319 << endl;
320 #endif
321
322 assert(!cl->stats.locked_for_data_gen);
323 if (cl->stats.which_red_array == 0) {
324 solver->longRedCls[0].push_back(offset);
325 moved_w0++;
326 } else if (cl->stats.which_red_array == 2) {
327 assert(false && "we should never move up through any other means");
328 } else {
329 uint32_t must_touch = solver->conf.must_touch_lev1_within;
330 if (cl->is_ternary_resolvent) {
331 must_touch *= solver->conf.ternary_keep_mult;
332 }
333 if (!solver->clause_locked(*cl, offset)
334 && cl->stats.last_touched + must_touch < solver->sumConflicts
335 ) {
336 solver->longRedCls[2].push_back(offset);
337 cl->stats.which_red_array = 2;
338
339 //when stats are needed, activities are correctly updated
340 //across all clauses
341 //WARNING this changes the way things behave during STATS relative to non-STATS!
342 #ifndef STATS_NEEDED
343 cl->stats.activity = 0;
344 solver->bump_cl_act<false>(cl);
345 #endif
346 non_recent_use++;
347 } else {
348 solver->longRedCls[1][j++] = offset;
349 used_recently++;
350 }
351 }
352 }
353 solver->longRedCls[1].resize(j);
354
355 if (solver->conf.verbosity >= 2) {
356 cout << "c [DBclean lev1]"
357 << " confl: " << solver->sumConflicts
358 << " orig size: " << orig_size
359 << " used recently: " << used_recently
360 << " not used recently: " << non_recent_use
361 << " moved w0: " << moved_w0
362 << solver->conf.print_times(cpuTime()-myTime)
363 << endl;
364 }
365
366 if (solver->sqlStats) {
367 solver->sqlStats->time_passed_min(
368 solver
369 , "dbclean-lev1"
370 , cpuTime()-myTime
371 );
372 }
373 total_time += cpuTime()-myTime;
374 }
375
376 #ifdef FINAL_PREDICTOR
handle_lev2_predictor()377 void ReduceDB::handle_lev2_predictor()
378 {
379 num_times_lev3_called++;
380 if (predictors == NULL) {
381 predictors = new ClPredictors(solver);
382 predictors->load_models(
383 solver->conf.pred_conf_short,
384 solver->conf.pred_conf_long,
385 solver->conf.pred_conf_forever);
386 }
387
388 assert(delayed_clause_free.empty());
389 uint32_t deleted = 0;
390 uint32_t kept_locked = 0;
391 uint32_t kept_dump_no = 0;
392 double myTime = cpuTime();
393 uint32_t tot_dumpno = 0;
394 size_t origsize = solver->longRedCls[2].size();
395
396 std::sort(solver->longRedCls[2].begin(), solver->longRedCls[2].end(),
397 SortRedClsAct(solver->cl_alloc));
398
399 for(size_t i = 0
400 ; i < solver->longRedCls[2].size()
401 ; i++
402 ) {
403 const ClOffset offset = solver->longRedCls[2][i];
404 Clause* cl = solver->cl_alloc.ptr(offset);
405
406 if (cl->stats.which_red_array == 0) {
407 assert(false);
408 }
409 const uint32_t act_ranking_top_10 = \
410 std::ceil((double)i/((double)solver->longRedCls[2].size()/10.0))+1;
411 double act_ranking_rel = (double)i/(double)solver->longRedCls[2].size();
412
413 cl->stats.pred_short_use = 0;
414 cl->stats.pred_long_use = 0;
415 cl->stats.pred_forever_use= 0;
416 if (cl->stats.dump_no > 0) {
417 assert(cl->stats.last_touched <= (int64_t)solver->sumConflicts);
418 int64_t last_touched_diff =
419 (int64_t)solver->sumConflicts-(int64_t)cl->stats.last_touched;
420 #ifdef EXTENDED_FEATURES
421 assert(cl->stats.rdb1_last_touched <= (int64_t)solver->sumConflicts-10000);
422 int64_t rdb1_last_touched_diff =
423 (int64_t)solver->sumConflicts-10000-(int64_t)cl->stats.rdb1_last_touched;
424 #endif
425
426 predictors->predict(
427 cl,
428 solver->sumConflicts,
429 last_touched_diff,
430 #ifdef EXTENDED_FEATURES
431 rdb1_last_touched_diff,
432 #endif
433 act_ranking_rel,
434 act_ranking_top_10,
435 cl->stats.pred_short_use,
436 cl->stats.pred_long_use,
437 cl->stats.pred_forever_use
438 );
439 }
440 cl->stats.dump_no++;
441 #ifdef EXTENDED_FEATURES
442 cl->stats.rdb1_act_ranking_rel = act_ranking_rel;
443 cl->stats.rdb1_last_touched = cl->stats.last_touched;
444 #endif
445 cl->stats.rdb1_propagations_made = cl->stats.propagations_made;
446 cl->stats.reset_rdb_stats();
447 }
448
449 if (solver->conf.verbosity >= 1) {
450 double predTime = cpuTime() - myTime;
451 cout << "c [DBCL] main predtime: " << predTime << endl;
452 }
453
454
455 uint32_t marked_forever = 0;
456 uint32_t keep_forever = 300 * solver->conf.pred_forever_chunk_mult;
457 std::sort(solver->longRedCls[2].begin(), solver->longRedCls[2].end(),
458 SortRedClsPredForever(solver->cl_alloc));
459 size_t j = 0;
460 for(uint32_t i = 0; i < solver->longRedCls[2].size(); i ++) {
461 const ClOffset offset = solver->longRedCls[2][i];
462 Clause* cl = solver->cl_alloc.ptr(offset);
463 if (i < keep_forever) {
464 marked_forever++;
465 cl->stats.which_red_array = 0;
466 solver->longRedCls[0].push_back(offset);
467 } else {
468 solver->longRedCls[2][j++] =solver->longRedCls[2][i];
469 }
470 }
471 solver->longRedCls[2].resize(j);
472
473
474 uint32_t marked_long = 0;
475 uint32_t keep_long = 2000 * solver->conf.pred_long_chunk_mult;
476 std::sort(solver->longRedCls[2].begin(), solver->longRedCls[2].end(),
477 SortRedClsPredLong(solver->cl_alloc));
478
479 j = 0;
480 for(uint32_t i = 0; i < solver->longRedCls[2].size(); i ++) {
481 const ClOffset offset = solver->longRedCls[2][i];
482 Clause* cl = solver->cl_alloc.ptr(offset);
483 if (i < keep_long) {
484 marked_long++;
485 cl->stats.which_red_array = 1;
486 solver->longRedCls[1].push_back(offset);
487 } else {
488 solver->longRedCls[2][j++] =solver->longRedCls[2][i];
489 }
490 }
491 solver->longRedCls[2].resize(j);
492
493 deleted = 0;
494 uint32_t keep_short = 15000 * solver->conf.pred_short_size_mult;
495 std::sort(solver->longRedCls[2].begin(), solver->longRedCls[2].end(),
496 SortRedClsPredShort(solver->cl_alloc));
497
498 j = 0;
499 for(uint32_t i = 0; i < solver->longRedCls[2].size(); i ++) {
500 const ClOffset offset = solver->longRedCls[2][i];
501 Clause* cl = solver->cl_alloc.ptr(offset);
502 // cout << "Short pred use: " << cl->stats.pred_short_use << endl;
503 tot_dumpno += cl->stats.dump_no-1;
504
505 if (solver->clause_locked(*cl, offset)) {
506 kept_locked++;
507 }
508
509 if (i < keep_short
510 || solver->clause_locked(*cl, offset)
511 || cl->stats.dump_no == 1
512 ) {
513 if (solver->clause_locked(*cl, offset)
514 || cl->stats.dump_no == 1)
515 {
516 keep_short++;
517 }
518 solver->longRedCls[2][j++] =solver->longRedCls[2][i];
519 } else {
520 deleted++;
521 solver->watches.smudge((*cl)[0]);
522 solver->watches.smudge((*cl)[1]);
523 solver->litStats.redLits -= cl->size();
524
525 *solver->drat << del << *cl << fin;
526 cl->setRemoved();
527 delayed_clause_free.push_back(offset);
528 }
529 }
530 solver->longRedCls[2].resize(j);
531
532
533 //Deal with FOREVER once in a while
534 const uint32_t orig_keep_forever = 2000.0*std::sqrt((double)solver->sumConflicts/10000.0) *
535 (double)solver->conf.pred_forever_size_mult;
536 if (num_times_lev3_called % 12 == 11) {
537 //Recalc pred_forever_use
538 std::sort(solver->longRedCls[0].begin(), solver->longRedCls[0].end(),
539 SortRedClsAct(solver->cl_alloc));
540
541 for(size_t i = 0
542 ; i < solver->longRedCls[0].size()
543 ; i++
544 ) {
545 const ClOffset offset = solver->longRedCls[0][i];
546 Clause* cl = solver->cl_alloc.ptr(offset);
547
548 const uint32_t act_ranking_top_10 = \
549 std::ceil((double)i/((double)solver->longRedCls[0].size()/10.0))+1;
550 double act_ranking_rel = (double)i/(double)solver->longRedCls[0].size();
551
552 int64_t last_touched_diff =
553 (int64_t)solver->sumConflicts-(int64_t)cl->stats.last_touched;
554 #ifdef EXTENDED_FEATURES
555 int64_t rdb1_last_touched_diff =
556 (int64_t)solver->sumConflicts-10000-(int64_t)cl->stats.rdb1_last_touched;
557 #endif
558
559 cl->stats.pred_forever_use = predictors->predict(
560 predict_type::forever_pred,
561 cl,
562 solver->sumConflicts,
563 last_touched_diff,
564 #ifdef EXTENDED_FEATURES
565 rdb1_last_touched_diff,
566 #endif
567 act_ranking_rel,
568 act_ranking_top_10);
569 }
570
571 //Clean up FOREVER, move to LONG
572 keep_forever = orig_keep_forever;
573 std::sort(solver->longRedCls[0].begin(), solver->longRedCls[0].end(),
574 SortRedClsPredForever(solver->cl_alloc));
575 j = 0;
576 for(uint32_t i = 0; i < solver->longRedCls[0].size(); i ++) {
577 const ClOffset offset = solver->longRedCls[0][i];
578 Clause* cl = solver->cl_alloc.ptr(offset);
579 if (i < keep_forever) {
580 assert(cl->stats.which_red_array == 0);
581 solver->longRedCls[0][j++] =solver->longRedCls[0][i];
582 } else {
583 solver->longRedCls[1].push_back(offset);
584 cl->stats.which_red_array = 1;
585 }
586 }
587 solver->longRedCls[0].resize(j);
588 }
589
590
591 //Deal with LONG once in a while
592 if (num_times_lev3_called % 5 == 4) {
593 //Recalc pred_long_use
594 std::sort(solver->longRedCls[1].begin(), solver->longRedCls[1].end(),
595 SortRedClsAct(solver->cl_alloc));
596
597 for(size_t i = 0
598 ; i < solver->longRedCls[1].size()
599 ; i++
600 ) {
601 const ClOffset offset = solver->longRedCls[1][i];
602 Clause* cl = solver->cl_alloc.ptr(offset);
603
604 const uint32_t act_ranking_top_10 = \
605 std::ceil((double)i/((double)solver->longRedCls[1].size()/10.0))+1;
606 double act_ranking_rel = (double)i/(double)solver->longRedCls[1].size();
607
608 int64_t last_touched_diff =
609 (int64_t)solver->sumConflicts-(int64_t)cl->stats.last_touched;
610 #ifdef EXTENDED_FEATURES
611 int64_t rdb1_last_touched_diff =
612 (int64_t)solver->sumConflicts-10000-(int64_t)cl->stats.rdb1_last_touched;
613 #endif
614
615 cl->stats.pred_long_use = predictors->predict(
616 predict_type::long_pred,
617 cl,
618 solver->sumConflicts,
619 last_touched_diff,
620 #ifdef EXTENDED_FEATURES
621 rdb1_last_touched_diff,
622 #endif
623 act_ranking_rel,
624 act_ranking_top_10);
625 }
626
627 //Clean up LONG, move to SHORT
628 std::sort(solver->longRedCls[1].begin(), solver->longRedCls[1].end(),
629 SortRedClsPredLong(solver->cl_alloc));
630 keep_long = 15000 * solver->conf.pred_long_size_mult;
631 j = 0;
632 for(uint32_t i = 0; i < solver->longRedCls[1].size(); i ++) {
633 const ClOffset offset = solver->longRedCls[1][i];
634 Clause* cl = solver->cl_alloc.ptr(offset);
635 if (i < keep_long) {
636 assert(cl->stats.which_red_array == 1);
637 solver->longRedCls[1][j++] =solver->longRedCls[1][i];
638 } else {
639 solver->longRedCls[2].push_back(offset);
640 cl->stats.which_red_array = 2;
641 }
642 }
643 solver->longRedCls[1].resize(j);
644 }
645
646
647 //Cleanup
648 solver->clean_occur_from_removed_clauses_only_smudged();
649 for(ClOffset offset: delayed_clause_free) {
650 solver->free_cl(offset);
651 }
652 delayed_clause_free.clear();
653
654 //Stats
655 if (solver->conf.verbosity >= 1) {
656 cout
657 << "c [DBCL pred]"
658 << " del: " << print_value_kilo_mega(deleted)
659 << " short: " << print_value_kilo_mega(solver->longRedCls[2].size())
660 << " long: " << print_value_kilo_mega(solver->longRedCls[1].size())
661 << " forever: " << print_value_kilo_mega(solver->longRedCls[0].size())
662 << endl;
663
664 if (solver->conf.verbosity >= 2) {
665 cout
666 << "c [DBCL pred] lev0: " << solver->longRedCls[0].size() << endl
667 << "c [DBCL pred] lev1: " << solver->longRedCls[1].size() << endl
668 << "c [DBCL pred] lev2: " << solver->longRedCls[2].size() << endl;
669 }
670
671 cout << "c [DBCL pred]"
672 << " avg dumpno: " << std::fixed << std::setprecision(2)
673 << ratio_for_stat(tot_dumpno, origsize)
674 << " dumpno_nonz: " << print_value_kilo_mega(origsize-kept_dump_no)
675 << solver->conf.print_times(cpuTime()-myTime)
676 << endl;
677 }
678
679 if (solver->sqlStats) {
680 solver->sqlStats->time_passed_min(
681 solver
682 , "dbclean-lev1"
683 , cpuTime()-myTime
684 );
685 }
686 total_time += cpuTime()-myTime;
687 }
688 #endif
689
mark_top_N_clauses(const uint64_t keep_num)690 void ReduceDB::mark_top_N_clauses(const uint64_t keep_num)
691 {
692 #ifdef VERBOSE_DEBUG
693 cout << "Marking top N clauses " << keep_num << endl;
694 #endif
695
696 size_t marked = 0;
697 for(size_t i = 0
698 ; i < solver->longRedCls[2].size() && marked < keep_num
699 ; i++
700 ) {
701 const ClOffset offset = solver->longRedCls[2][i];
702 Clause* cl = solver->cl_alloc.ptr(offset);
703 #ifdef VERBOSE_DEBUG
704 cout << "offset: " << offset << " cl->stats.last_touched: " << cl->stats.last_touched
705 << " act:" << std::setprecision(9) << cl->stats.activity
706 << " which_red_array:" << cl->stats.which_red_array << endl
707 << " -- cl:" << *cl << " tern:" << cl->is_ternary_resolvent
708 << endl;
709 #endif
710
711 if (cl->used_in_xor()
712 || cl->stats.ttl > 0
713 || solver->clause_locked(*cl, offset)
714 || cl->stats.which_red_array != 2
715 ) {
716 //no need to mark, skip
717 #ifdef VERBOSE_DEBUG
718 cout << "Not marking Skipping "<< endl;
719 #endif
720 continue;
721 }
722
723 if (!cl->stats.marked_clause) {
724 marked++;
725 cl->stats.marked_clause = true;
726 #ifdef VERBOSE_DEBUG
727 cout << "Not marking Skipping "<< endl;
728 #endif
729 }
730 }
731 }
732
cl_needs_removal(const Clause * cl,const ClOffset offset) const733 bool ReduceDB::cl_needs_removal(const Clause* cl, const ClOffset offset) const
734 {
735 assert(cl->red());
736 return !cl->used_in_xor()
737 && !cl->stats.marked_clause
738 && cl->stats.ttl == 0
739 && !solver->clause_locked(*cl, offset);
740 }
741
remove_cl_from_lev2()742 void ReduceDB::remove_cl_from_lev2() {
743 size_t i, j;
744 for (i = j = 0
745 ; i < solver->longRedCls[2].size()
746 ; i++
747 ) {
748 ClOffset offset = solver->longRedCls[2][i];
749 Clause* cl = solver->cl_alloc.ptr(offset);
750 assert(cl->size() > 2);
751
752 //move to another array
753 if (cl->stats.which_red_array < 2) {
754 cl->stats.marked_clause = 0;
755 solver->longRedCls[cl->stats.which_red_array].push_back(offset);
756 continue;
757 }
758 assert(cl->stats.which_red_array == 2);
759
760 //Check if locked, or marked or ttl-ed
761 if (cl->stats.marked_clause) {
762 cl_marked++;
763 } else if (cl->stats.ttl != 0) {
764 cl_ttl++;
765 } else if (solver->clause_locked(*cl, offset)) {
766 cl_locked_solver++;
767 }
768
769 if (!cl_needs_removal(cl, offset)) {
770 if (cl->stats.ttl > 0) {
771 cl->stats.ttl--;
772 }
773 solver->longRedCls[2][j++] = offset;
774 cl->stats.marked_clause = 0;
775 continue;
776 }
777
778 //Stats Update
779 solver->watches.smudge((*cl)[0]);
780 solver->watches.smudge((*cl)[1]);
781 solver->litStats.redLits -= cl->size();
782
783 *solver->drat << del << *cl << fin;
784 cl->setRemoved();
785 #ifdef VERBOSE_DEBUG
786 cout << "REMOVING offset: " << offset << " cl->stats.last_touched: " << cl->stats.last_touched
787 << " act:" << std::setprecision(9) << cl->stats.activity
788 << " which_red_array:" << cl->stats.which_red_array << endl
789 << " -- cl:" << *cl << " tern:" << cl->is_ternary_resolvent
790 << endl;
791 #endif
792 delayed_clause_free.push_back(offset);
793 }
794 solver->longRedCls[2].resize(j);
795 }
796