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 "gatefinder.h"
24 #include "time_mem.h"
25 #include "solver.h"
26 #include "occsimplifier.h"
27 #include "subsumestrengthen.h"
28 #include "clauseallocator.h"
29 #include <array>
30 #include <utility>
31 #include "sqlstats.h"
32
33 using namespace CMSat;
34 using std::cout;
35 using std::endl;
36
GateFinder(OccSimplifier * _simplifier,Solver * _solver)37 GateFinder::GateFinder(OccSimplifier *_simplifier, Solver *_solver) :
38 numDotPrinted(0)
39 , simplifier(_simplifier)
40 , solver(_solver)
41 , seen(_solver->seen)
42 , seen2(_solver->seen2)
43 , toClear(solver->toClear)
44 {
45 sizeSortedOcc.resize(solver->conf.maxGateBasedClReduceSize+1);
46 }
47
doAll()48 bool GateFinder::doAll()
49 {
50 runStats.clear();
51 orGates.clear();
52
53 assert(solver->watches.get_smudged_list().empty());
54 find_or_gates_and_update_stats();
55 if (!all_simplifications_with_gates())
56 goto end;
57
58 if (solver->conf.doPrintGateDot) {
59 print_graphviz_dot();
60 }
61
62 end:
63 solver->clean_occur_from_idx_types_only_smudged();
64 if (solver->conf.verbosity) {
65 if (solver->conf.verbosity >= 3) {
66 runStats.print(solver->nVars());
67 }
68 }
69 globalStats += runStats;
70
71 orGates.clear();
72 orGates.shrink_to_fit();
73 solver->sumSearchStats.num_gates_found_last = orGates.size();
74
75 return solver->okay();
76 }
77
find_or_gates_and_update_stats()78 void GateFinder::find_or_gates_and_update_stats()
79 {
80 assert(solver->ok);
81
82 double myTime = cpuTime();
83 const int64_t orig_numMaxGateFinder =
84 solver->conf.gatefinder_time_limitM*100LL*1000LL
85 *solver->conf.global_timeout_multiplier;
86 numMaxGateFinder = orig_numMaxGateFinder;
87 simplifier->limit_to_decrease = &numMaxGateFinder;
88
89 find_or_gates();
90
91 for(const auto orgate: orGates) {
92 if (orgate.red) {
93 runStats.learntGatesSize += 2;
94 runStats.numRed++;
95 } else {
96 runStats.irredGatesSize += 2;
97 runStats.numIrred++;
98 }
99 }
100 const double time_used = cpuTime() - myTime;
101 const bool time_out = (numMaxGateFinder <= 0);
102 const double time_remain = float_div(numMaxGateFinder, orig_numMaxGateFinder);
103 runStats.findGateTime = time_used;
104 runStats.find_gate_timeout = time_out;
105 if (solver->sqlStats) {
106 solver->sqlStats->time_passed(
107 solver
108 , "gate find"
109 , time_used
110 , time_out
111 , time_remain
112 );
113 }
114
115 if (solver->conf.verbosity) {
116 cout << "c [occ-gates] found"
117 << " irred:" << runStats.numIrred
118 << " avg-s: " << std::fixed << std::setprecision(1)
119 << float_div(runStats.irredGatesSize, runStats.numIrred)
120 << " red: " << runStats.numRed
121 /*<< " avg-s: " << std::fixed << std::setprecision(1)
122 << float_div(learntGatesSize, numRed)*/
123 << solver->conf.print_times(time_used, time_out, time_remain)
124 << endl;
125 }
126 }
127
shorten_with_all_or_gates()128 bool GateFinder::shorten_with_all_or_gates()
129 {
130 const double myTime = cpuTime();
131 const int64_t orig_numMaxShortenWithGates =
132 solver->conf.shorten_with_gates_time_limitM*1000LL*1000LL
133 *solver->conf.global_timeout_multiplier;
134
135 numMaxShortenWithGates = orig_numMaxShortenWithGates;
136 simplifier->limit_to_decrease = &numMaxShortenWithGates;
137
138 //Go through each gate, see if we can do something with it
139 simplifier->cl_to_free_later.clear();
140 for (const OrGate& gate: orGates) {
141 if (numMaxShortenWithGates < 0
142 || solver->must_interrupt_asap()
143 ) {
144 break;
145 }
146
147 if (!shortenWithOrGate(gate))
148 break;
149 }
150 solver->clean_occur_from_removed_clauses();
151 simplifier->free_clauses_to_free();
152
153 const double time_used = cpuTime() - myTime;
154 const bool time_out = (numMaxShortenWithGates <= 0);
155 const double time_remain = float_div(numMaxShortenWithGates, orig_numMaxShortenWithGates);
156 runStats.orBasedTime = time_used;
157 runStats.or_based_timeout = time_out;
158 if (solver->sqlStats) {
159 solver->sqlStats->time_passed(
160 solver
161 , "gate shorten cl"
162 , time_used
163 , time_out
164 , time_remain
165 );
166 }
167
168 if (solver->conf.verbosity) {
169 cout << "c [occ-gates] shorten"
170 << " cl: " << std::setw(5) << runStats.orGateUseful
171 << " l-rem: " << std::setw(6) << runStats.litsRem
172 << solver->conf.print_times(time_used, time_out, time_remain)
173 << endl;
174 }
175
176 return solver->okay();
177 }
178
remove_clauses_with_all_or_gates()179 bool GateFinder::remove_clauses_with_all_or_gates()
180 {
181 const int64_t orig_numMaxClRemWithGates =
182 solver->conf.remove_cl_with_gates_time_limitM*1000LL*1000LL
183 *solver->conf.global_timeout_multiplier;
184
185 numMaxClRemWithGates = orig_numMaxClRemWithGates;
186 simplifier->limit_to_decrease = &numMaxClRemWithGates;
187 const double myTime = cpuTime();
188
189 //Go through each gate, see if we can do something with it
190 for (const OrGate& gate: orGates) {
191 if (numMaxClRemWithGates < 0
192 || solver->must_interrupt_asap()
193 ) {
194 break;
195 }
196
197 if (!remove_clauses_using_and_gate(gate, true, false))
198 break;
199
200 if (!remove_clauses_using_and_gate_tri(gate, true, false))
201 break;
202 }
203 const double time_used = cpuTime() - myTime;
204 const bool time_out = (numMaxClRemWithGates <= 0);
205 const double time_remain = float_div(numMaxClRemWithGates, orig_numMaxClRemWithGates);
206 runStats.andBasedTime = time_used;
207 runStats.and_based_timeout = time_out;
208 if (solver->sqlStats) {
209 solver->sqlStats->time_passed(
210 solver
211 , "gate rem cl"
212 , time_used
213 , time_out
214 , time_remain
215 );
216 }
217
218 if (solver->conf.verbosity) {
219 cout << "c [occ-gates] rem"
220 << " cl: " << runStats.andGateUseful
221 << " avg s: " << std::setprecision(1)
222 << float_div(runStats.clauseSizeRem, runStats.andGateUseful)
223 << solver->conf.print_times(time_used, time_out, time_remain)
224 << endl;
225 }
226
227 return solver->okay();
228 }
229
all_simplifications_with_gates()230 bool GateFinder::all_simplifications_with_gates()
231 {
232 assert(solver->ok);
233
234 //OR gate treatment
235 if (solver->conf.doShortenWithOrGates) {
236 if (!shorten_with_all_or_gates()) {
237 return false;
238 }
239 }
240
241 //AND gate treatment
242 if (solver->conf.doRemClWithAndGates) {
243 if (!remove_clauses_with_all_or_gates()) {
244 return false;
245 }
246 }
247
248 //EQ gate treatment
249 if (solver->conf.doFindEqLitsWithGates) {
250 const double myTime = cpuTime();
251 runStats.varReplaced += findEqOrGates();
252
253 const double time_used = cpuTime() - myTime;
254 runStats.varReplaceTime += time_used;
255 if (solver->sqlStats) {
256 solver->sqlStats->time_passed_min(
257 solver
258 , "gate eq-var"
259 , time_used
260 );
261 }
262
263 if (solver->conf.verbosity) {
264 cout << "c [occ-gates] eqlit"
265 << " v-rep: " << std::setw(3) << runStats.varReplaced
266 << solver->conf.print_times(time_used)
267 << endl;
268 }
269
270 if (!solver->ok)
271 return false;
272 }
273
274 return solver->okay();
275 }
276
findEqOrGates()277 size_t GateFinder::findEqOrGates()
278 {
279 assert(solver->ok);
280 size_t foundRep = 0;
281 vector<OrGate> gates = orGates;
282 std::sort(gates.begin(), gates.end(), GateCompareForEq());
283
284 vector<Lit> tmp(2);
285 for (uint32_t i = 1; i < gates.size(); i++) {
286 const OrGate& gate1 = gates[i-1];
287 const OrGate& gate2 = gates[i];
288
289 if (gate1.lit1 == gate2.lit1
290 && gate1.lit2 == gate2.lit2
291 && gate1.rhs.var() != gate2.rhs.var()
292 ) {
293 foundRep++;
294 tmp[0] = gate1.rhs.unsign();
295 tmp[1] = gate2.rhs.unsign();
296 const bool RHS = gate1.rhs.sign() ^ gate2.rhs.sign();
297 if (!solver->add_xor_clause_inter(tmp, RHS, false))
298 return foundRep;
299 }
300 }
301
302 return foundRep;
303 }
304
find_or_gates()305 void GateFinder::find_or_gates()
306 {
307 if (solver->nVars() < 1)
308 return;
309
310 const size_t offs = solver->mtrand.randInt(solver->nVars()*2-1);
311 for(size_t i = 0
312 ; i < solver->nVars()*2
313 && *simplifier->limit_to_decrease > 0
314 && !solver->must_interrupt_asap()
315 ; i++
316 ) {
317 const size_t at = (offs + i) % (solver->nVars()*2);
318 const Lit lit = Lit::toLit(at);
319 find_or_gates_in_sweep_mode(lit);
320 find_or_gates_in_sweep_mode(~lit);
321 }
322 }
323
find_or_gates_in_sweep_mode(const Lit lit)324 void GateFinder::find_or_gates_in_sweep_mode(const Lit lit)
325 {
326 assert(toClear.empty());
327 watch_subarray_const ws = solver->watches[lit];
328 *simplifier->limit_to_decrease -= ws.size();
329 for(const Watched w: ws) {
330 if (w.isBin() && !w.red()) {
331 seen[(~w.lit2()).toInt()] = 1;
332 toClear.push_back(~w.lit2());
333 }
334 }
335
336 *simplifier->limit_to_decrease -= toClear.size();
337 for(const Lit toclear: toClear) {
338 seen[toclear.toInt()] = 0;
339 }
340 toClear.clear();
341 }
342
343
add_gate_if_not_already_inside(const Lit rhs,const Lit lit1,const Lit lit2)344 void GateFinder::add_gate_if_not_already_inside(
345 const Lit rhs
346 , const Lit lit1
347 , const Lit lit2
348 ) {
349 OrGate gate(rhs, lit1, lit2, false);
350 for (Watched ws: solver->watches[gate.rhs]) {
351 if (ws.isIdx()
352 && orGates[ws.get_idx()] == gate
353 ) {
354 return;
355 }
356 }
357 link_in_gate(gate);
358 }
359
link_in_gate(const OrGate & gate)360 void GateFinder::link_in_gate(const OrGate& gate)
361 {
362 const size_t at = orGates.size();
363 orGates.push_back(gate);
364 solver->watches[gate.rhs].push(Watched(at));
365 solver->watches.smudge(gate.rhs);
366 }
367
shortenWithOrGate(const OrGate & gate)368 bool GateFinder::shortenWithOrGate(const OrGate& gate)
369 {
370 assert(solver->ok);
371
372 //Find clauses that potentially could be shortened
373 subs.clear();
374 simplifier->sub_str->find_subsumed(
375 std::numeric_limits< uint32_t >::max()
376 , gate.getLits()
377 , calcAbstraction(gate.getLits())
378 , subs
379 );
380
381 for (size_t i = 0; i < subs.size(); i++) {
382 ClOffset offset = subs[i];
383 Clause& cl = *solver->cl_alloc.ptr(offset);
384
385 //Don't shorten irred clauses with red gates
386 // -- potential loss if e.g. red clause is removed later
387 if ((!cl.red() && gate.red))
388 continue;
389
390 runStats.orGateUseful++;
391
392 //Go through clause, check if RHS (rhs) is inside the clause
393 //If it is, we have two possibilities:
394 //1) a = b V c , clause: a V b V c V d
395 //2) a = b V c , clause: -a V b V c V d
396 //But we will simply ignore this. One of these clauses can be strengthened
397 //the other subsumed. But let's ignore these, subsumption/strenghtening will take care of this
398 bool rhsInside = false;
399 for (Lit lit: cl) {
400 if (gate.rhs.var() == lit.var()) {
401 rhsInside = true;
402 break;
403 }
404 }
405 if (rhsInside)
406 continue;
407
408 if (solver->conf.verbosity >= 6) {
409 cout << "OR gate-based cl-shortening" << endl;
410 cout << "Gate used: " << gate << endl;
411 cout << "orig Clause: " << cl<< endl;
412 }
413
414 //Set up future clause's lits
415 vector<Lit> lits;
416 for (const Lit lit: cl) {
417 bool inGate = false;
418 for (Lit lit2: gate.getLits()) {
419 if (lit == lit2) {
420 inGate = true;
421 runStats.litsRem++;
422 break;
423 }
424 }
425
426 if (!inGate)
427 lits.push_back(lit);
428 }
429 if (!rhsInside) {
430 lits.push_back(gate.rhs);
431 runStats.litsRem--;
432 }
433
434 //Future clause's stat
435 const bool red = cl.red();
436 const ClauseStats stats = cl.stats;
437
438 //Free the old clause and allocate new one
439 (*solver->drat) << deldelay << cl << fin;
440 simplifier->unlink_clause(offset, false, false, true);
441 Clause* cl2 = solver->add_clause_int(lits, red, stats, false);
442 (*solver->drat) << findelay;
443 if (!solver->ok)
444 return false;
445
446 //If the clause is implicit, it's already linked in, ignore
447 if (cl2 == NULL)
448 continue;
449
450 simplifier->linkInClause(*cl2);
451 ClOffset offset2 = solver->cl_alloc.get_offset(cl2);
452 simplifier->clauses.push_back(offset2);
453
454 if (solver->conf.verbosity >= 6) {
455 cout << "new clause after gate: " << lits << endl;
456 cout << "-----------" << endl;
457 }
458 }
459
460 return true;
461 }
462
set_seen2_and_abstraction(const Clause & cl,cl_abst_type & abstraction)463 void GateFinder::set_seen2_and_abstraction(
464 const Clause& cl
465 , cl_abst_type& abstraction
466 ) {
467 *simplifier->limit_to_decrease -= cl.size();
468 for (const Lit lit: cl) {
469 if (!seen2[lit.toInt()]) {
470 seen2[lit.toInt()] = true;
471 seen2Set.push_back(lit.toInt());
472 }
473 abstraction |= abst_var(lit.var());
474 }
475 }
476
calc_sorted_occ_and_set_seen2(const OrGate & gate,uint32_t & maxSize,uint32_t & minSize,const bool only_irred)477 cl_abst_type GateFinder::calc_sorted_occ_and_set_seen2(
478 const OrGate& gate
479 , uint32_t& maxSize
480 , uint32_t& minSize
481 , const bool only_irred
482 ) {
483 assert(seen2Set.empty());
484 cl_abst_type abstraction = 0;
485 for (vector<ClOffset>& certain_size_occ: sizeSortedOcc)
486 certain_size_occ.clear();
487
488 watch_subarray_const csOther = solver->watches[~(gate.lit2)];
489 *simplifier->limit_to_decrease -= csOther.size();
490 for (const Watched ws: csOther) {
491 if (!ws.isClause())
492 continue;
493
494 const ClOffset offset = ws.get_offset();
495 const Clause& cl = *solver->cl_alloc.ptr(offset);
496 if (cl.red() && only_irred)
497 continue;
498
499 //We might be contracting 2 irred clauses based on a learnt gate
500 //would lead to UNSAT->SAT
501 if (!cl.red() && gate.red)
502 continue;
503
504 //Clause too long, skip
505 if (cl.size() > solver->conf.maxGateBasedClReduceSize)
506 continue;
507
508 maxSize = std::max(maxSize, cl.size());
509 minSize = std::min(minSize, cl.size());
510 sizeSortedOcc[cl.size()].push_back(offset);
511 set_seen2_and_abstraction(cl, abstraction);
512 }
513
514 return abstraction;
515 }
516
set_seen2_tri(const OrGate & gate,const bool only_irred)517 void GateFinder::set_seen2_tri(
518 const OrGate& gate
519 , const bool only_irred
520 ) {
521 assert(seen2Set.empty());
522 watch_subarray_const csOther = solver->watches[~(gate.lit2)];
523 *simplifier->limit_to_decrease -= csOther.size();
524 for (const Watched ws: csOther) {
525 if (!ws.isTri())
526 continue;
527
528 if (ws.red() && only_irred)
529 continue;
530
531 //We might be contracting 2 irred clauses based on a learnt gate
532 //would lead to UNSAT->SAT
533 if (!ws.red() && gate.red)
534 continue;
535
536 const Lit lits[2] = {ws.lit2(), ws.lit3()};
537 for (size_t i = 0; i < 2; i++) {
538 const Lit lit = lits[i];
539 if (!seen2[lit.toInt()]) {
540 seen2[lit.toInt()] = 1;
541 seen2Set.push_back(lit.toInt());
542 }
543 }
544 }
545 }
546
calc_abst_and_set_seen(const Clause & cl,const OrGate & gate)547 cl_abst_type GateFinder::calc_abst_and_set_seen(
548 const Clause& cl
549 , const OrGate& gate
550 ) {
551 cl_abst_type abst = 0;
552 for (const Lit lit: cl) {
553 //lit1 doesn't count into abstraction
554 if (lit == ~(gate.lit1))
555 continue;
556
557 seen[lit.toInt()] = 1;
558 abst |= abst_var(lit.var());
559 }
560 abst |= abst_var((~(gate.lit2)).var());
561
562 return abst;
563 }
564
check_seen_and_gate_against_cl(const Clause & this_cl,const OrGate & gate)565 bool GateFinder::check_seen_and_gate_against_cl(
566 const Clause& this_cl
567 , const OrGate& gate
568 ) {
569 *(simplifier->limit_to_decrease) -= this_cl.size();
570 for (const Lit lit: this_cl) {
571
572 //We know this is inside, skip
573 if (lit == ~(gate.lit1))
574 continue;
575
576 //If some weird variable is inside, skip
577 if ( lit.var() == gate.lit2.var()
578 || lit.var() == gate.rhs.var()
579 //A lit is inside this clause isn't inside the others
580 || !seen2[lit.toInt()]
581 ) {
582 return false;
583 }
584 }
585 return true;
586 }
587
check_seen_and_gate_against_lit(const Lit lit,const OrGate & gate)588 bool GateFinder::check_seen_and_gate_against_lit(
589 const Lit lit
590 , const OrGate& gate
591 ) {
592 //If some weird variable is inside, skip
593 if ( lit.var() == gate.lit2.var()
594 || lit.var() == gate.rhs.var()
595 //A lit is inside this clause isn't inside the others
596 || !seen2[lit.toInt()]
597 ) {
598 return false;
599 }
600
601 return true;
602 }
603
find_pair_for_and_gate_reduction(const Watched & ws,const size_t minSize,const size_t maxSize,const cl_abst_type general_abst,const OrGate & gate,const bool only_irred)604 ClOffset GateFinder::find_pair_for_and_gate_reduction(
605 const Watched& ws
606 , const size_t minSize
607 , const size_t maxSize
608 , const cl_abst_type general_abst
609 , const OrGate& gate
610 , const bool only_irred
611 ) {
612 //Only long clauses
613 if (!ws.isClause())
614 return CL_OFFSET_MAX;
615
616 const ClOffset this_cl_offs = ws.get_offset();
617 Clause& this_cl = *solver->cl_alloc.ptr(this_cl_offs);
618 if ((ws.getAbst() | general_abst) != general_abst
619 || (this_cl.red() && only_irred)
620 || (!this_cl.red() && gate.red)
621 || this_cl.size() > solver->conf.maxGateBasedClReduceSize
622 || this_cl.size() > maxSize //Size must be smaller or equal to maxSize
623 || this_cl.size() < minSize //Size must be larger or equal than minsize
624 || sizeSortedOcc[this_cl.size()].empty()) //this bracket for sizeSortedOcc must be non-empty
625 {
626 //cout << "Not even possible, this clause cannot match any other" << endl;
627 return CL_OFFSET_MAX;
628 }
629
630 if (!check_seen_and_gate_against_cl(this_cl, gate))
631 return CL_OFFSET_MAX;
632
633
634 const cl_abst_type this_cl_abst = calc_abst_and_set_seen(this_cl, gate);
635 const ClOffset other_cl_offs = findAndGateOtherCl(
636 sizeSortedOcc[this_cl.size()] //in this occur list that contains clauses of specific size
637 , ~(gate.lit2) //this is the LIT that is meant to be in the clause
638 , this_cl_abst //clause MUST match this abst
639 , gate.red
640 , only_irred
641 );
642
643 //Clear 'seen' from bits set
644 *(simplifier->limit_to_decrease) -= this_cl.size();
645 for (const Lit lit: this_cl) {
646 seen[lit.toInt()] = 0;
647 }
648
649 return other_cl_offs;
650 }
651
find_pair_for_and_gate_reduction_tri(const Watched & ws,const OrGate & gate,const bool only_irred,Watched & found_pair)652 bool GateFinder::find_pair_for_and_gate_reduction_tri(
653 const Watched& ws
654 , const OrGate& gate
655 , const bool only_irred
656 , Watched& found_pair
657 ) {
658 //Only long clauses
659 if (!ws.isTri())
660 return false;
661
662 if (ws.red() && only_irred) {
663 //cout << "Not even possible, this clause cannot match any other" << endl;
664 return false;
665 }
666
667 //Check that we are not removing irred info based on learnt gate
668 if (!ws.red() && gate.red)
669 return false;
670
671 if (!check_seen_and_gate_against_lit(ws.lit2(), gate)
672 || !check_seen_and_gate_against_lit(ws.lit3(), gate))
673 {
674 return false;
675 }
676
677 seen[ws.lit2().toInt()] = 1;
678 seen[ws.lit3().toInt()] = 1;
679 const bool ret = findAndGateOtherCl_tri(
680 solver->watches[~(gate.lit2)]
681 , gate.red
682 , only_irred
683 , found_pair
684 );
685
686 seen[ws.lit2().toInt()] = 0;
687 seen[ws.lit3().toInt()] = 0;
688
689 return ret;
690 }
691
remove_clauses_using_and_gate(const OrGate & gate,const bool really_remove,const bool only_irred)692 bool GateFinder::remove_clauses_using_and_gate(
693 const OrGate& gate
694 , const bool really_remove
695 , const bool only_irred
696 ) {
697 assert(clToUnlink.empty());
698 if (solver->watches[~(gate.lit1)].empty()
699 || solver->watches[~(gate.lit2)].empty()
700 ) {
701 return solver->okay();
702 }
703
704 uint32_t maxSize = 0;
705 uint32_t minSize = std::numeric_limits<uint32_t>::max();
706 cl_abst_type general_abst = calc_sorted_occ_and_set_seen2(gate, maxSize, minSize, only_irred);
707 general_abst |= abst_var(gate.lit1.var());
708 if (maxSize == 0)
709 return solver->okay();
710
711 watch_subarray cs = solver->watches[~(gate.lit1)];
712 *simplifier->limit_to_decrease -= cs.size();
713 for (const Watched ws: cs) {
714 if (*simplifier->limit_to_decrease < 0)
715 break;
716
717 const ClOffset other_cl_offs = find_pair_for_and_gate_reduction(
718 ws, minSize, maxSize, general_abst, gate, only_irred
719 );
720
721 if (really_remove
722 && other_cl_offs != CL_OFFSET_MAX
723 ) {
724 const ClOffset this_cl_offs = ws.get_offset();
725 assert(other_cl_offs != this_cl_offs);
726 clToUnlink.insert(other_cl_offs);
727 clToUnlink.insert(this_cl_offs);
728 treatAndGateClause(other_cl_offs, gate, this_cl_offs);
729 }
730
731 if (!solver->ok)
732 return false;
733 }
734
735 //Clear from seen2 bits that have been set
736 *(simplifier->limit_to_decrease) -= seen2Set.size();
737 for(const size_t at: seen2Set) {
738 seen2[at] = 0;
739 }
740 seen2Set.clear();
741
742 //Now that all is computed, remove those that need removal
743 for(const ClOffset offset: clToUnlink) {
744 simplifier->unlink_clause(offset);
745 }
746 clToUnlink.clear();
747
748 return solver->okay();
749 }
750
remove_clauses_using_and_gate_tri(const OrGate & gate,const bool really_remove,const bool only_irred)751 bool GateFinder::remove_clauses_using_and_gate_tri(
752 const OrGate& gate
753 , const bool really_remove
754 , const bool only_irred
755 ) {
756 if (solver->watches[~(gate.lit1)].empty()
757 || solver->watches[~(gate.lit2)].empty()
758 ) {
759 return solver->okay();
760 }
761 tri_to_unlink.clear();
762
763 set_seen2_tri(gate, only_irred);
764 watch_subarray_const cs = solver->watches[~(gate.lit1)];
765 *simplifier->limit_to_decrease -= cs.size();
766 for (const Watched ws: cs) {
767 if (*simplifier->limit_to_decrease < 0)
768 break;
769
770 Watched other_ws;
771 const bool found_pair = find_pair_for_and_gate_reduction_tri(
772 ws, gate, only_irred, other_ws
773 );
774
775 if (really_remove && found_pair) {
776 runStats.andGateUseful++;
777 runStats.clauseSizeRem += 3;
778
779 tri_to_unlink.insert(TriToUnlink(ws.lit2(), ws.lit3(), ws.red()));
780 solver->detach_tri_clause(~(gate.lit2), other_ws.lit2(), other_ws.lit3(), other_ws.red());
781 vector<Lit> lits = {~(gate.rhs), ws.lit2(), ws.lit3()};
782 solver->add_clause_int(
783 lits
784 , ws.red() && other_ws.red()
785 , ClauseStats()
786 , false //don't attach/propagate
787 );
788 if (!solver->ok)
789 return false;
790 }
791 }
792
793 //Clear from seen2 bits that have been set
794 *(simplifier->limit_to_decrease) -= seen2Set.size();
795 for(const size_t at: seen2Set) {
796 seen2[at] = false;
797 }
798 seen2Set.clear();
799
800 for(const TriToUnlink tri: tri_to_unlink) {
801 solver->detach_tri_clause(~(gate.lit1), tri.lit2, tri.lit3, tri.red);
802 }
803 tri_to_unlink.clear();
804
805 return solver->okay();
806 }
807
treatAndGateClause(const ClOffset other_cl_offset,const OrGate & gate,const ClOffset this_cl_offset)808 void GateFinder::treatAndGateClause(
809 const ClOffset other_cl_offset
810 , const OrGate& gate
811 , const ClOffset this_cl_offset
812 ) {
813 //Update stats
814 runStats.andGateUseful++;
815 const Clause& this_cl = *solver->cl_alloc.ptr(this_cl_offset);
816 runStats.clauseSizeRem += this_cl.size();
817
818 if (solver->conf.verbosity >= 6) {
819 cout << "AND gate-based cl rem" << endl;
820 cout << "clause 1: " << this_cl << endl;
821 //cout << "clause 2: " << *clauses[other_cl_offset.index] << endl;
822 cout << "gate : " << gate << endl;
823 }
824
825 //Put into 'lits' the literals of the clause
826 vector<Lit> lits;
827 *simplifier->limit_to_decrease -= this_cl.size()*2;
828 for (const Lit lit: this_cl) {
829 if (lit != ~(gate.lit1)) {
830 lits.push_back(lit);
831 assert(lit.var() != gate.rhs.var());
832 assert(lit.var() != gate.lit1.var());
833 assert(lit.var() != gate.lit2.var());
834 }
835 }
836 lits.push_back(~(gate.rhs));
837
838 //Calculate learnt & glue
839 const Clause& other_cl = *solver->cl_alloc.ptr(other_cl_offset);
840 const bool red = other_cl.red() && this_cl.red();
841 ClauseStats stats = ClauseStats::combineStats(this_cl.stats, other_cl.stats);
842
843 if (solver->conf.verbosity >= 6) {
844 cout << "gate new clause:" << lits << endl;
845 cout << "-----------" << endl;
846 }
847
848 //Create clause (but don't attach)
849 Clause* clNew = solver->add_clause_int(lits, red, stats, false);
850
851 //Link in clause properly (not regular attach)
852 if (clNew != NULL) {
853 simplifier->linkInClause(*clNew);
854 ClOffset offsetNew = solver->cl_alloc.get_offset(clNew);
855 simplifier->clauses.push_back(offsetNew);
856 }
857 }
858
findAndGateOtherCl(const vector<ClOffset> & this_sizeSortedOcc,const Lit otherLit,const cl_abst_type abst,const bool gate_is_red,const bool only_irred)859 ClOffset GateFinder::findAndGateOtherCl(
860 const vector<ClOffset>& this_sizeSortedOcc
861 , const Lit otherLit
862 , const cl_abst_type abst
863 , const bool gate_is_red
864 , const bool only_irred
865 ) {
866 *(simplifier->limit_to_decrease) -= this_sizeSortedOcc.size();
867 for (const ClOffset offset: this_sizeSortedOcc) {
868 const Clause& cl = *solver->cl_alloc.ptr(offset);
869 if (cl.red() && only_irred)
870 continue;
871
872 if (!cl.red() && gate_is_red)
873 continue;
874
875 //abstraction must match
876 if (cl.abst != abst)
877 continue;
878
879 *(simplifier->limit_to_decrease) -= cl.size()/2+5;
880 for (const Lit lit: cl) {
881 //we skip the other lit in the gate
882 if (lit == otherLit)
883 continue;
884
885 //Seen is perfectly correct, everything must match
886 if (!seen[lit.toInt()])
887 goto next;
888
889 }
890 return offset;
891 next:;
892 }
893
894 return CL_OFFSET_MAX;
895 }
896
findAndGateOtherCl_tri(watch_subarray_const ws_list,const bool gate_is_red,const bool only_irred,Watched & ret)897 bool GateFinder::findAndGateOtherCl_tri(
898 watch_subarray_const ws_list
899 , const bool gate_is_red
900 , const bool only_irred
901 , Watched& ret
902 ) {
903 *(simplifier->limit_to_decrease) -= ws_list.size();
904 for (const Watched& ws: ws_list) {
905 if (!ws.isTri())
906 continue;
907
908 if (ws.red() && only_irred)
909 continue;
910
911 if (!ws.red() && gate_is_red)
912 continue;
913
914 if (seen[ws.lit2().toInt()]
915 && seen[ws.lit3().toInt()]
916 ) {
917 ret = ws;
918 return true;
919 }
920 }
921
922 return false;
923 }
924
print_graphviz_dot2()925 void GateFinder::print_graphviz_dot2()
926 {
927 std::stringstream ss;
928 ss << "Gates" << (numDotPrinted++) << ".dot";
929 std::string filenename = ss.str();
930 std::ofstream file(filenename.c_str(), std::ios::out);
931 file << "digraph G {" << endl;
932 vector<bool> gateUsed;
933 gateUsed.resize(orGates.size(), false);
934 size_t index = 0;
935 for (const OrGate orGate: orGates) {
936 index++;
937 for (const Lit lit: orGate.getLits()) {
938 for (Watched ws: solver->watches[lit]) {
939 if (!ws.isIdx()) {
940 continue;
941 }
942 uint32_t at = ws.get_idx();
943
944 //The same one, skip
945 if (at == index)
946 continue;
947
948 file << "Gate" << at;
949 gateUsed[at] = true;
950 file << " -> ";
951
952 file << "Gate" << index;
953 gateUsed[index] = true;
954
955 file << "[arrowsize=\"0.4\"];" << endl;
956 }
957
958 /*vector<uint32_t>& occ2 = gateOccEq[(~*it2).toInt()];
959 for (vector<uint32_t>::const_iterator it3 = occ2.begin(), end3 = occ2.end(); it3 != end3; it3++) {
960 if (*it3 == index) continue;
961
962 file << "Gate" << *it3;
963 gateUsed[*it3] = true;
964 file << " -> ";
965
966 file << "Gate" << index;
967 gateUsed[index] = true;
968
969 file << "[style = \"dotted\", arrowsize=\"0.4\"];" << endl;
970 }*/
971 }
972 }
973
974 index = 0;
975 for (const OrGate orGate: orGates) {
976 index++;
977
978 if (gateUsed[index]) {
979 file << "Gate" << index << " [ shape=\"point\"";
980 file << ", size = 0.8";
981 file << ", style=\"filled\"";
982 if (orGate.red)
983 file << ", color=\"darkseagreen4\"";
984 else
985 file << ", color=\"darkseagreen\"";
986
987 file << "];" << endl;
988 }
989 }
990
991 file << "}" << endl;
992 file.close();
993 cout << "c Printed gate structure to file " << filenename << endl;
994 }
995
print_graphviz_dot()996 void GateFinder::print_graphviz_dot()
997 {
998 print_graphviz_dot2();
999 }
1000
operator +=(const Stats & other)1001 GateFinder::Stats& GateFinder::Stats::operator+=(const Stats& other)
1002 {
1003 findGateTime += other.findGateTime;
1004 find_gate_timeout += other.find_gate_timeout;
1005 orBasedTime += other.orBasedTime;
1006 or_based_timeout += other.or_based_timeout;
1007 varReplaceTime += other.varReplaceTime;
1008 andBasedTime += other.andBasedTime;
1009 and_based_timeout += other.and_based_timeout;
1010 erTime += other.erTime;
1011
1012 //OR-gate
1013 orGateUseful += other.orGateUseful;
1014 numLongCls += other.numLongCls;
1015 numLongClsLits += other.numLongClsLits;
1016 litsRem += other.litsRem;
1017 varReplaced += other.varReplaced;
1018
1019 //And-gate
1020 andGateUseful += other.andGateUseful;
1021 clauseSizeRem += other.clauseSizeRem;
1022
1023 //ER
1024 numERVars += other.numERVars;
1025
1026 //Gates
1027 learntGatesSize += other.learntGatesSize;
1028 numRed += other.numRed;
1029 irredGatesSize += other.irredGatesSize;
1030 numIrred += other.numIrred;
1031
1032 return *this;
1033 }
1034
print(const size_t nVars) const1035 void GateFinder::Stats::print(const size_t nVars) const
1036 {
1037 cout << "c -------- GATE FINDING ----------" << endl;
1038 print_stats_line("c time"
1039 , total_time()
1040 );
1041
1042 print_stats_line("c find gate time"
1043 , findGateTime
1044 , stats_line_percent(findGateTime, total_time())
1045 , "% time"
1046 );
1047
1048 print_stats_line("c gate-based cl-sh time"
1049 , orBasedTime
1050 , stats_line_percent(orBasedTime, total_time())
1051 , "% time"
1052 );
1053
1054 print_stats_line("c gate-based cl-rem time"
1055 , andBasedTime
1056 , stats_line_percent(andBasedTime, total_time())
1057 , "% time"
1058 );
1059
1060 print_stats_line("c gate-based varrep time"
1061 , varReplaceTime
1062 , stats_line_percent(varReplaceTime, total_time())
1063 , "% time"
1064 );
1065
1066 print_stats_line("c gatefinder cl-short"
1067 , orGateUseful
1068 , stats_line_percent(orGateUseful, numLongCls)
1069 , "% long cls"
1070 );
1071
1072 print_stats_line("c gatefinder lits-rem"
1073 , litsRem
1074 , stats_line_percent(litsRem, numLongClsLits)
1075 , "% long cls lits"
1076 );
1077
1078 print_stats_line("c gatefinder cl-rem"
1079 , andGateUseful
1080 , stats_line_percent(andGateUseful, numLongCls)
1081 , "% long cls"
1082 );
1083
1084 print_stats_line("c gatefinder cl-rem's lits"
1085 , clauseSizeRem
1086 , stats_line_percent(clauseSizeRem, numLongClsLits)
1087 , "% long cls lits"
1088 );
1089
1090 print_stats_line("c gatefinder var-rep"
1091 , varReplaced
1092 , stats_line_percent(varReplaced, nVars)
1093 , "% vars"
1094 );
1095
1096 cout << "c -------- GATE FINDING END ----------" << endl;
1097 }
1098
1099