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 "comphandler.h"
24 #include "compfinder.h"
25 #include "varreplacer.h"
26 #include "solver.h"
27 #include "varupdatehelper.h"
28 #include "watchalgos.h"
29 #include "clauseallocator.h"
30 #include "clausecleaner.h"
31 #include <iostream>
32 #include <cassert>
33 #include <iomanip>
34 #include "cryptominisat5/cryptominisat.h"
35 #include "sqlstats.h"
36
37 using namespace CMSat;
38 using std::make_pair;
39 using std::cout;
40 using std::endl;
41
42 //#define VERBOSE_DEBUG
43
CompHandler(Solver * _solver)44 CompHandler::CompHandler(Solver* _solver) :
45 solver(_solver)
46 , compFinder(NULL)
47 {
48 }
49
~CompHandler()50 CompHandler::~CompHandler()
51 {
52 if (compFinder != NULL) {
53 delete compFinder;
54 }
55 }
56
new_var(const uint32_t orig_outer)57 void CompHandler::new_var(const uint32_t orig_outer)
58 {
59 if (orig_outer == std::numeric_limits<uint32_t>::max()) {
60 savedState.push_back(l_Undef);
61 }
62 assert(savedState.size() == solver->nVarsOuter());
63 }
64
new_vars(size_t n)65 void CompHandler::new_vars(size_t n)
66 {
67 savedState.insert(savedState.end(), n, l_Undef);
68 assert(savedState.size() == solver->nVarsOuter());
69 }
70
save_on_var_memory()71 void CompHandler::save_on_var_memory()
72 {
73 }
74
mem_used() const75 size_t CompHandler::mem_used() const
76 {
77 size_t mem = 0;
78 mem += savedState.capacity()*sizeof(lbool);
79 mem += useless.capacity()*sizeof(uint32_t);
80 mem += smallsolver_to_bigsolver.capacity()*sizeof(uint32_t);
81 mem += bigsolver_to_smallsolver.capacity()*sizeof(uint32_t);
82
83 return mem;
84 }
85
createRenumbering(const vector<uint32_t> & vars)86 void CompHandler::createRenumbering(const vector<uint32_t>& vars)
87 {
88 smallsolver_to_bigsolver.resize(vars.size());
89 bigsolver_to_smallsolver.resize(solver->nVars());
90
91 for(size_t i = 0, size = vars.size()
92 ; i < size
93 ; ++i
94 ) {
95 bigsolver_to_smallsolver[vars[i]] = i;
96 smallsolver_to_bigsolver[i] = vars[i];
97 }
98 }
99
assumpsInsideComponent(const vector<uint32_t> & vars)100 bool CompHandler::assumpsInsideComponent(const vector<uint32_t>& vars)
101 {
102 for(uint32_t var: vars) {
103 if (solver->var_inside_assumptions(var) != l_Undef) {
104 return true;
105 }
106 }
107
108 return false;
109 }
110
get_component_sizes() const111 vector<pair<uint32_t, uint32_t> > CompHandler::get_component_sizes() const
112 {
113 vector<pair<uint32_t, uint32_t> > sizes;
114 map<uint32_t, vector<uint32_t> > reverseTable = compFinder->getReverseTable();
115
116 for (map<uint32_t, vector<uint32_t> >::iterator
117 it = reverseTable.begin()
118 ; it != reverseTable.end()
119 ; ++it
120 ) {
121 sizes.push_back(make_pair(
122 it->first //Comp number
123 , (uint32_t)it->second.size() //Size of the table
124 ));
125 }
126
127 //Sort according to smallest size first
128 std::sort(sizes.begin(), sizes.end(), sort_pred());
129 assert(sizes.size() > 1);
130
131 return sizes;
132 }
133
handle()134 bool CompHandler::handle()
135 {
136 assert(solver->conf.sampling_vars == NULL && "Cannot handle components when sampling vars is set");
137 assert(solver->okay());
138 double myTime = cpuTime();
139
140 delete compFinder;
141 compFinder = new CompFinder(solver);
142 compFinder->find_components();
143 if (compFinder->getTimedOut()) {
144 delete compFinder;
145 compFinder = NULL;
146 return solver->okay();
147 }
148
149 const uint32_t num_comps = compFinder->getNumComps();
150
151 //If there is only one big comp, we can't do anything
152 if (num_comps <= 1) {
153 if (solver->conf.verbosity >= 3) {
154 cout
155 << "c [comp] Only one component, not handling it separately"
156 << endl;
157 }
158
159 delete compFinder;
160 compFinder = NULL;
161 return solver->okay();
162 }
163
164
165 solver->removed_xorclauses_clash_vars.clear();
166 solver->xorclauses.clear();
167 solver->xorclauses_unused.clear();
168 #ifdef USE_GAUSS
169 solver->clear_gauss_matrices();
170 #endif
171 map<uint32_t, vector<uint32_t> > reverseTable = compFinder->getReverseTable();
172 assert(num_comps == compFinder->getReverseTable().size());
173 vector<pair<uint32_t, uint32_t> > sizes = get_component_sizes();
174
175 size_t num_comps_solved = 0;
176 size_t vars_solved = 0;
177 for (uint32_t it = 0; it < sizes.size()-1; ++it) {
178 const uint32_t comp = sizes[it].first;
179 vector<uint32_t>& vars = reverseTable[comp];
180 const bool ok = try_to_solve_component(it, comp, vars, num_comps);
181 if (!ok) {
182 break;
183 }
184 num_comps_solved++;
185 vars_solved += vars.size();
186 }
187
188 if (!solver->okay()) {
189 delete compFinder;
190 compFinder = NULL;
191
192 return solver->okay();
193 }
194
195 const double time_used = cpuTime() - myTime;
196 if (solver->conf.verbosity >= 1) {
197 cout
198 << "c [comp] Coming back to original instance, solved "
199 << num_comps_solved << " component(s), "
200 << vars_solved << " vars"
201 << solver->conf.print_times(time_used)
202 << endl;
203 }
204
205 if (solver->sqlStats) {
206 solver->sqlStats->time_passed_min(
207 solver
208 , "comphandler"
209 , time_used
210 );
211 }
212
213 check_local_vardata_sanity();
214
215 delete compFinder;
216 compFinder = NULL;
217 return solver->okay();
218 }
219
try_to_solve_component(const uint32_t comp_at,const uint32_t comp,const vector<uint32_t> & vars_orig,const size_t num_comps)220 bool CompHandler::try_to_solve_component(
221 const uint32_t comp_at
222 , const uint32_t comp
223 , const vector<uint32_t>& vars_orig
224 , const size_t num_comps
225 ) {
226 for(const uint32_t var: vars_orig) {
227 assert(solver->value(var) == l_Undef);
228 }
229
230 if (vars_orig.size() > 100ULL*1000ULL*
231 solver->conf.var_and_mem_out_mult
232 ) {
233 //There too many variables -- don't create a sub-solver
234 //I'm afraid that we will memory-out
235
236 return true;
237 }
238
239 //Components with assumptions should not be removed
240 if (assumpsInsideComponent(vars_orig))
241 return true;
242
243 return solve_component(comp_at, comp, vars_orig, num_comps);
244 }
245
solve_component(const uint32_t comp_at,const uint32_t comp,const vector<uint32_t> & vars_orig,const size_t num_comps)246 bool CompHandler::solve_component(
247 const uint32_t comp_at
248 , const uint32_t comp
249 , const vector<uint32_t>& vars_orig
250 , const size_t num_comps
251 ) {
252 assert(! (solver->drat->enabled() || solver->conf.simulate_drat) );
253 vector<uint32_t> vars(vars_orig);
254 components_solved++;
255
256 //Sort and renumber
257 std::sort(vars.begin(), vars.end());
258 createRenumbering(vars);
259
260 if (solver->conf.verbosity && num_comps < 20) {
261 cout
262 << "c [comp] Solving component " << comp_at
263 << " num vars: " << vars.size()
264 << " ======================================="
265 << endl;
266 }
267
268 //Set up new solver
269 SolverConf conf = configureNewSolver(vars.size());
270 SATSolver newSolver(
271 (void*)&conf
272 , solver->get_must_interrupt_inter_asap_ptr()
273 );
274 moveVariablesBetweenSolvers(&newSolver, vars, comp);
275
276 //Move clauses over
277 moveClausesImplicit(&newSolver, comp, vars);
278 moveClausesLong(solver->longIrredCls, &newSolver, comp);
279 for(auto& lredcls: solver->longRedCls) {
280 moveClausesLong(lredcls, &newSolver, comp);
281 }
282
283 const lbool status = newSolver.solve();
284 //Out of time
285 if (status == l_Undef) {
286 if (solver->conf.verbosity) {
287 cout
288 << "c [comp] subcomponent returned l_Undef -- timeout or interrupt."
289 << endl;
290 }
291 readdRemovedClauses();
292 return false;
293 }
294
295 if (status == l_False) {
296 solver->ok = false;
297 if (solver->conf.verbosity) {
298 cout
299 << "c [comp] The component is UNSAT -> problem is UNSAT"
300 << endl;
301 }
302 return false;
303 }
304
305 check_solution_is_unassigned_in_main_solver(&newSolver, vars);
306 save_solution_to_savedstate(&newSolver, vars, comp);
307 move_decision_level_zero_vars_here(&newSolver);
308
309 if (solver->conf.verbosity && num_comps < 20) {
310 cout
311 << "c [comp] component " << comp_at
312 << " ======================================="
313 << endl;
314 }
315 return true;
316 }
317
check_local_vardata_sanity()318 void CompHandler::check_local_vardata_sanity()
319 {
320 //Checking that all variables that are not in the remaining comp have
321 //correct 'removed' flags, and none have been assigned
322
323 size_t num_vars_removed_check = 0;
324 for (uint32_t outerVar = 0; outerVar < solver->nVarsOuter(); ++outerVar) {
325 const uint32_t interVar = solver->map_outer_to_inter(outerVar);
326 if (savedState[outerVar] != l_Undef) {
327 assert(solver->varData[interVar].removed == Removed::decomposed);
328 assert(solver->value(interVar) == l_Undef || solver->varData[interVar].level == 0);
329 }
330
331 if (solver->varData[interVar].removed == Removed::decomposed) {
332 num_vars_removed_check++;
333 }
334 }
335
336 assert(num_vars_removed == num_vars_removed_check);
337 }
338
check_solution_is_unassigned_in_main_solver(const SATSolver * newSolver,const vector<uint32_t> & vars)339 void CompHandler::check_solution_is_unassigned_in_main_solver(
340 const SATSolver* newSolver
341 , const vector<uint32_t>& vars
342 ) {
343 for (size_t i = 0; i < vars.size(); ++i) {
344 uint32_t var = vars[i];
345 if (newSolver->get_model()[upd_bigsolver_to_smallsolver(var)] != l_Undef) {
346 assert(solver->value(var) == l_Undef);
347 }
348 }
349 }
350
save_solution_to_savedstate(const SATSolver * newSolver,const vector<uint32_t> & vars,const uint32_t comp)351 void CompHandler::save_solution_to_savedstate(
352 const SATSolver* newSolver
353 , const vector<uint32_t>& vars
354 , const uint32_t comp
355 ) {
356 assert(savedState.size() == solver->nVarsOuter());
357 for (size_t i = 0; i < vars.size(); ++i) {
358 uint32_t var = vars[i];
359 uint32_t outerVar = solver->map_inter_to_outer(var);
360 if (newSolver->get_model()[upd_bigsolver_to_smallsolver(var)] != l_Undef) {
361 assert(savedState[outerVar] == l_Undef);
362 assert(compFinder->getVarComp(var) == comp);
363
364 savedState[outerVar] = newSolver->get_model()[upd_bigsolver_to_smallsolver(var)];
365 }
366 }
367 }
368
move_decision_level_zero_vars_here(const SATSolver * newSolver)369 void CompHandler::move_decision_level_zero_vars_here(
370 const SATSolver* newSolver
371 ) {
372 const vector<Lit> zero_assigned = newSolver->get_zero_assigned_lits();
373 for (Lit lit: zero_assigned) {
374 assert(lit.var() < newSolver->nVars());
375 assert(lit.var() < smallsolver_to_bigsolver.size());
376 lit = Lit(smallsolver_to_bigsolver[lit.var()], lit.sign());
377 assert(solver->value(lit) == l_Undef);
378
379 assert(solver->varData[lit.var()].removed == Removed::decomposed);
380 solver->varData[lit.var()].removed = Removed::none;
381 solver->set_decision_var(lit.var());
382 num_vars_removed--;
383
384 const uint32_t outer = solver->map_inter_to_outer(lit.var());
385 savedState[outer] = l_Undef;
386 solver->enqueue(lit);
387
388 //These vars are not meant to be in the orig solver
389 //so they cannot cause UNSAT
390 solver->ok = (solver->propagate<false>().isNULL());
391 assert(solver->ok);
392 }
393 }
394
395
configureNewSolver(const size_t numVars) const396 SolverConf CompHandler::configureNewSolver(
397 const size_t numVars
398 ) const {
399 SolverConf conf(solver->conf);
400 conf.origSeed = solver->mtrand.randInt();
401 conf.sampling_vars = NULL;
402 if (numVars < 60) {
403 conf.do_simplify_problem = false;
404 conf.doIntreeProbe = false;
405 conf.do_hyperbin_and_transred = false;
406 conf.verbosity = std::min(solver->conf.verbosity, 0);
407 }
408
409 //To small, don't clogger up the screen
410 if (numVars < 20 && solver->conf.verbosity < 3) {
411 conf.verbosity = 0;
412 }
413
414 //Don't recurse
415 conf.doCompHandler = false;
416
417 return conf;
418 }
419
420 /**
421 @brief Moves the variables to the new solver
422
423 This implies making the right variables decision in the new solver,
424 and making it non-decision in the old solver.
425 */
moveVariablesBetweenSolvers(SATSolver * newSolver,const vector<uint32_t> & vars,const uint32_t comp)426 void CompHandler::moveVariablesBetweenSolvers(
427 SATSolver* newSolver
428 , const vector<uint32_t>& vars
429 , const uint32_t comp
430 ) {
431 for(const uint32_t var: vars) {
432 newSolver->new_var();
433 assert(compFinder->getVarComp(var) == comp);
434 assert(solver->value(var) == l_Undef);
435
436 assert(solver->varData[var].removed == Removed::none);
437 solver->varData[var].removed = Removed::decomposed;
438 num_vars_removed++;
439 }
440 }
441
moveClausesLong(vector<ClOffset> & cs,SATSolver * newSolver,const uint32_t comp)442 void CompHandler::moveClausesLong(
443 vector<ClOffset>& cs
444 , SATSolver* newSolver
445 , const uint32_t comp
446 ) {
447 vector<Lit> tmp;
448
449 vector<ClOffset>::iterator i, j, end;
450 for (i = j = cs.begin(), end = cs.end()
451 ; i != end
452 ; ++i
453 ) {
454 Clause& cl = *solver->cl_alloc.ptr(*i);
455
456 //Irred, different comp
457 if (!cl.red()) {
458 if (compFinder->getVarComp(cl[0].var()) != comp) {
459 //different comp, move along
460 *j++ = *i;
461 continue;
462 }
463 }
464
465 if (cl.red()) {
466 //Check which comp(s) it belongs to
467 bool thisComp = false;
468 bool otherComp = false;
469 for (Lit* l = cl.begin(), *end2 = cl.end(); l != end2; ++l) {
470 if (compFinder->getVarComp(l->var()) == comp)
471 thisComp = true;
472
473 if (compFinder->getVarComp(l->var()) != comp)
474 otherComp = true;
475 }
476
477 //In both comps, remove it
478 if (thisComp && otherComp) {
479 solver->detachClause(cl);
480 solver->free_cl(&cl);
481 continue;
482 }
483
484 //In one comp, but not this one
485 if (!thisComp) {
486 //different comp, move along
487 *j++ = *i;
488 continue;
489 }
490 assert(thisComp && !otherComp);
491 }
492
493 //Let's move it to the other solver!
494 #ifdef VERBOSE_DEBUG
495 cout << "clause in this comp:" << cl << endl;
496 #endif
497
498 //Create temporary space 'tmp' and copy to backup
499 tmp.resize(cl.size());
500 for (size_t i2 = 0; i2 < cl.size(); ++i2) {
501 tmp[i2] = upd_bigsolver_to_smallsolver(cl[i2]);
502 }
503
504 //Add 'tmp' to the new solver
505 if (cl.red()) {
506 #if defined(STATS_NEEDED) || defined(FINAL_PREDICTOR)
507 cl.stats.introduced_at_conflict = 0;
508 #endif
509 //newSolver->addRedClause(tmp, cl.stats);
510 } else {
511 saveClause(cl);
512 newSolver->add_clause(tmp);
513 }
514
515 //Remove from here
516 solver->detachClause(cl);
517 solver->free_cl(&cl);
518 }
519 cs.resize(cs.size() - (i-j));
520 }
521
remove_bin_except_for_lit1(const Lit lit,const Lit lit2)522 void CompHandler::remove_bin_except_for_lit1(const Lit lit, const Lit lit2)
523 {
524 removeWBin(solver->watches, lit2, lit, true);
525
526 //Update stats
527 solver->binTri.redBins--;
528 }
529
move_binary_clause(SATSolver * newSolver,const uint32_t comp,Watched * i,const Lit lit)530 void CompHandler::move_binary_clause(
531 SATSolver* newSolver
532 , const uint32_t comp
533 , Watched *i
534 , const Lit lit
535 ) {
536 const Lit lit2 = i->lit2();
537
538 //Unless redundant, cannot be in 2 comps at once
539 assert((compFinder->getVarComp(lit.var()) == comp
540 && compFinder->getVarComp(lit2.var()) == comp
541 ) || i->red()
542 );
543
544 //If it's redundant and the lits are in different comps, remove it.
545 if (compFinder->getVarComp(lit.var()) != comp
546 || compFinder->getVarComp(lit2.var()) != comp
547 ) {
548 //Can only be redundant, otherwise it would be in the same
549 //component
550 assert(i->red());
551
552 //The way we go through this, it's definitely going to be
553 //lit2 that's in the other component
554 assert(compFinder->getVarComp(lit2.var()) != comp);
555
556 remove_bin_except_for_lit1(lit, lit2);
557 return;
558 }
559
560 //don't add the same clause twice
561 if (lit < lit2) {
562
563 //Add clause
564 tmp_lits = {upd_bigsolver_to_smallsolver(lit), upd_bigsolver_to_smallsolver(lit2)};
565 assert(compFinder->getVarComp(lit.var()) == comp);
566 assert(compFinder->getVarComp(lit2.var()) == comp);
567
568 //Add new clause
569 if (i->red()) {
570 //newSolver->addRedClause(tmp_lits);
571 numRemovedHalfRed++;
572 } else {
573 //Save backup
574 saveClause(vector<Lit>{lit, lit2});
575
576 newSolver->add_clause(tmp_lits);
577 numRemovedHalfIrred++;
578 }
579 } else {
580
581 //Just remove, already added above
582 if (i->red()) {
583 numRemovedHalfRed++;
584 } else {
585 numRemovedHalfIrred++;
586 }
587 }
588 }
589
moveClausesImplicit(SATSolver * newSolver,const uint32_t comp,const vector<uint32_t> & vars)590 void CompHandler::moveClausesImplicit(
591 SATSolver* newSolver
592 , const uint32_t comp
593 , const vector<uint32_t>& vars
594 ) {
595 numRemovedHalfIrred = 0;
596 numRemovedHalfRed = 0;
597
598 for(const uint32_t var: vars) {
599 for(unsigned sign = 0; sign < 2; ++sign) {
600 const Lit lit = Lit(var, sign);
601 watch_subarray ws = solver->watches[lit];
602
603 //If empty, nothing to to, skip
604 if (ws.empty()) {
605 continue;
606 }
607
608 Watched *i = ws.begin();
609 Watched *j = i;
610 for (Watched *end2 = ws.end()
611 ; i != end2
612 ; ++i
613 ) {
614 //At least one variable inside comp
615 if (i->isBin()
616 && (compFinder->getVarComp(lit.var()) == comp
617 || compFinder->getVarComp(i->lit2().var()) == comp
618 )
619 ) {
620 move_binary_clause(newSolver, comp, i, lit);
621 continue;
622 }
623 *j++ = *i;
624 }
625 ws.shrink_(i-j);
626 }}
627
628 assert(numRemovedHalfIrred % 2 == 0);
629 solver->binTri.irredBins -= numRemovedHalfIrred/2;
630
631 assert(numRemovedHalfRed % 2 == 0);
632 solver->binTri.redBins -= numRemovedHalfRed/2;
633 }
634
addSavedState(vector<lbool> & solution)635 void CompHandler::addSavedState(vector<lbool>& solution)
636 {
637 //Enqueue them. They may need to be extended, so enqueue is needed
638 //manipulating "model" may not be good enough
639 assert(savedState.size() == solver->nVarsOuter());
640 assert(solution.size() == solver->nVarsOuter());
641 for (size_t var = 0; var < savedState.size(); ++var) {
642 if (savedState[var] != l_Undef) {
643 const uint32_t interVar = solver->map_outer_to_inter(var);
644 assert(solver->varData[interVar].removed == Removed::decomposed);
645
646 const lbool val = savedState[var];
647 assert(solution[var] == l_Undef);
648 solution[var] = val;
649 //cout << "Solution to var " << var + 1 << " has been added: " << val << endl;
650
651 solver->varData[interVar].polarity = (val == l_True);
652 }
653 }
654 }
655
656 template<class T>
saveClause(const T & lits)657 void CompHandler::saveClause(const T& lits)
658 {
659 //Update variable number to 'outer' number. This means we will not have
660 //to update the variables every time the internal variable numbering changes
661 for (const Lit lit : lits ) {
662 removedClauses.lits.push_back(
663 solver->map_inter_to_outer(lit)
664 );
665 }
666 removedClauses.sizes.push_back(lits.size());
667 }
668
readdRemovedClauses()669 void CompHandler::readdRemovedClauses()
670 {
671 assert(solver->okay());
672 double myTime = cpuTime();
673
674 //Avoid recursion, clear 'removed' status
675 for(size_t outer = 0; outer < solver->nVarsOuter(); ++outer) {
676 const uint32_t inter = solver->map_outer_to_inter(outer);
677 VarData& dat = solver->varData[inter];
678 if (dat.removed == Removed::decomposed) {
679 dat.removed = Removed::none;
680 num_vars_removed--;
681 }
682 }
683
684 //Clear saved state
685 for(lbool& val: savedState) {
686 val = l_Undef;
687 }
688
689 vector<Lit> tmp;
690 size_t at = 0;
691 for (uint32_t sz: removedClauses.sizes) {
692
693 //addClause() needs *outer* literals, so just do that
694 tmp.clear();
695 for(size_t i = at; i < at + sz; ++i) {
696 tmp.push_back(removedClauses.lits[i]);
697 }
698 if (solver->conf.verbosity >= 6) {
699 cout << "c [comp] Adding back component clause " << tmp << endl;
700 }
701
702 //Add the clause to the system
703 solver->addClause(tmp);
704 assert(solver->okay());
705
706 //Move 'at' along
707 at += sz;
708 }
709
710 //The variables have been added back thanks to addClause()
711 //-> set them decision
712 for(size_t outer = 0; outer < solver->nVarsOuter(); ++outer) {
713 const uint32_t inter = solver->map_outer_to_inter(outer);
714 VarData& dat = solver->varData[inter];
715 if (dat.removed == Removed::none
716 && solver->value(inter) == l_Undef
717 ) {
718 solver->set_decision_var(inter);
719 }
720 }
721
722 //Explain what we just did
723 const double time_used = cpuTime() - myTime;
724 if (solver->conf.verbosity) {
725 cout
726 << "c [comp] re-added components. Lits: "
727 << removedClauses.lits.size()
728 << " cls:" << removedClauses.sizes.size()
729 << solver->conf.print_times(time_used)
730 << endl;
731 }
732 if (solver->sqlStats) {
733 solver->sqlStats->time_passed_min(
734 solver
735 , "comp re-adding"
736 , time_used
737 );
738 }
739
740 //Clear added data
741 removedClauses.lits.clear();
742 removedClauses.sizes.clear();
743 }
744
dump_removed_clauses(std::ostream * outfile) const745 uint32_t CompHandler::dump_removed_clauses(std::ostream* outfile) const
746 {
747 if (outfile == NULL)
748 return removedClauses.sizes.size();
749
750 uint32_t num_cls = 0;
751 vector<Lit> tmp;
752 size_t at = 0;
753 for (uint32_t size :removedClauses.sizes) {
754 tmp.clear();
755 for(size_t i = at; i < at + size; ++i) {
756 tmp.push_back(removedClauses.lits[i]);
757 }
758 std::sort(tmp.begin(), tmp.end());
759 *outfile << tmp << " 0" << endl;
760 num_cls ++;
761
762 //Move 'at' along
763 at += size;
764 }
765 return num_cls;
766 }
767