1 #include "internal.hpp"
2
3 namespace CaDiCaL {
4
5 /*------------------------------------------------------------------------*/
6
7 // This implements an inprocessing version of blocked clause elimination and
8 // is assumed to be triggered just before bounded variable elimination. It
9 // has a separate 'block' flag while variable elimination uses 'elim'.
10 // Thus it only tries to block clauses on a literal which was removed in an
11 // irredundant clause in negated form before and has not been tried to use
12 // as blocking literal since then.
13
14 /*------------------------------------------------------------------------*/
15
operator ()(unsigned a,unsigned b)16 inline bool block_more_occs_size::operator () (unsigned a, unsigned b) {
17 size_t s = internal->noccs (-internal->u2i (a));
18 size_t t = internal->noccs (-internal->u2i (b));
19 if (s > t) return true;
20 if (s < t) return false;
21 s = internal->noccs (internal->u2i (a));
22 t = internal->noccs (internal->u2i (b));
23 if (s > t) return true;
24 if (s < t) return false;
25 return a > b;
26 }
27
28 /*------------------------------------------------------------------------*/
29
30 // Determine whether 'c' is blocked on 'lit', by first marking all its
31 // literals and then checking all resolvents with negative clauses (with
32 // '-lit') are tautological. We use a move-to-front scheme for both the
33 // occurrence list of negative clauses (with '-lit') and then for literals
34 // within each such clause. The clause move-to-front scheme has the goal to
35 // find non-tautological clauses faster in the future, while the literal
36 // move-to-front scheme has the goal to faster find the matching literal,
37 // which makes the resolvent tautological (again in the future).
38
is_blocked_clause(Clause * c,int lit)39 bool Internal::is_blocked_clause (Clause * c, int lit) {
40
41 LOG (c, "trying to block on %d", lit);
42
43 assert (c->size >= opts.blockminclslim);
44 assert (c->size <= opts.blockmaxclslim);
45 assert (active (lit));
46 assert (!val (lit));
47 assert (!c->garbage);
48 assert (!c->redundant);
49 assert (!level);
50
51 mark (c); // First mark all literals in 'c'.
52
53 Occs & os = occs (-lit);
54 LOG ("resolving against at most %zd clauses with %d", os.size (), -lit);
55
56 bool res = true; // Result is true if all resolvents tautological.
57
58 // Can not use 'auto' here since we update 'os' during traversal.
59 //
60 const auto end_of_os = os.end ();
61 auto i = os.begin ();
62
63 Clause * prev_d = 0; // Previous non-tautological clause.
64
65 for (; i != end_of_os; i++)
66 {
67 // Move the first clause with non-tautological resolvent to the front of
68 // the occurrence list to improve finding it faster later.
69 //
70 Clause * d = *i;
71
72 assert (!d->garbage);
73 assert (!d->redundant);
74 assert (d->size <= opts.blockmaxclslim);
75
76 *i = prev_d; // Move previous non-tautological clause
77 prev_d = d; // backwards but remember clause at this position.
78
79 LOG (d, "resolving on %d against", lit);
80 stats.blockres++;
81
82 int prev_other = 0; // Previous non-tautological literal.
83
84 // No 'auto' since we update literals of 'd' during traversal.
85 //
86 const const_literal_iterator end_of_d = d->end ();
87 literal_iterator l;
88
89 for (l = d->begin (); l != end_of_d; l++)
90 {
91 // Same move-to-front mechanism for literals within a clause. It
92 // moves the first negatively marked literal to the front to find it
93 // faster in the future.
94 //
95 const int other = *l;
96 *l = prev_other;
97 prev_other = other;
98 if (other == -lit) continue;
99 assert (other != lit);
100 assert (active (other));
101 assert (!val (other));
102 if (marked (other) < 0) {
103 LOG ("found tautological literal %d", other);
104 d->literals[0] = other; // Move to front of 'd'.
105 break;
106 }
107 }
108
109 if (l == end_of_d)
110 {
111 LOG ("no tautological literal found");
112 //
113 // Since we did not find a tautological literal we restore the old
114 // order of literals in the clause.
115 //
116 const const_literal_iterator begin_of_d = d->begin ();
117 while (l-- != begin_of_d) {
118 const int other = *l;
119 *l = prev_other;
120 prev_other = other;
121 }
122 res = false; // Now 'd' is a witness that 'c' is not blocked.
123 os[0] = d; // Move it to the front of the occurrence list.
124 break;
125 }
126 }
127 unmark (c); // ... all literals of the candidate clause.
128
129 // If all resolvents are tautological and thus the clause is blocked we
130 // restore the old order of clauses in the occurrence list of '-lit'.
131 //
132 if (res) {
133 assert (i == end_of_os);
134 const auto boc = os.begin ();
135 while (i != boc) {
136 Clause * d = *--i;
137 *i = prev_d;
138 prev_d = d;
139 }
140 }
141
142 return res;
143 }
144
145 /*------------------------------------------------------------------------*/
146
block_schedule(Blocker & blocker)147 void Internal::block_schedule (Blocker & blocker)
148 {
149 // Set skip flags for all literals in too large clauses.
150 //
151 for (const auto & c : clauses) {
152
153 if (c->garbage) continue;
154 if (c->redundant) continue;
155 if (c->size <= opts.blockmaxclslim) continue;
156
157 for (const auto & lit : *c)
158 mark_skip (-lit);
159 }
160
161 // Connect all literal occurrences in irredundant clauses.
162 //
163 for (const auto & c : clauses) {
164
165 if (c->garbage) continue;
166 if (c->redundant) continue;
167
168 for (const auto & lit : *c) {
169 assert (active (lit));
170 assert (!val (lit));
171 occs (lit).push_back (c);
172 }
173 }
174
175 // We establish the invariant that 'noccs' gives the number of actual
176 // occurrences of 'lit' in non-garbage clauses, while 'occs' might still
177 // refer to garbage clauses, thus 'noccs (lit) <= occs (lit).size ()'. It
178 // is expensive to remove references to garbage clauses from 'occs' during
179 // blocked clause elimination, but decrementing 'noccs' is cheap.
180
181 for (int idx = 1; idx <= max_var; idx++) {
182 if (!active (idx)) continue;
183 assert (!val (idx));
184 for (int sign = -1; sign <= 1; sign += 2) {
185 const int lit = sign * idx;
186 Occs & os = occs (lit);
187 noccs (lit) = os.size ();
188 }
189 }
190
191 // Now we fill the schedule (priority queue) of candidate literals to be
192 // tried as blocking literals. It is probably slightly faster to do this
193 // in one go after all occurrences have been determined, instead of
194 // filling the priority queue during pushing occurrences. Filling the
195 // schedule can not be fused with the previous loop (easily) since we
196 // first have to initialize 'noccs' for both 'lit' and '-lit'.
197
198 int skipped = 0;
199
200 for (int idx = 1; idx <= max_var; idx++) {
201 if (!active (idx)) continue;
202 if (frozen (idx)) { skipped += 2; continue; }
203 assert (!val (idx));
204 for (int sign = -1; sign <= 1; sign += 2) {
205 const int lit = sign * idx;
206 if (marked_skip (lit)) { skipped++; continue; }
207 if (!marked_block (lit)) continue;
208 unmark_block (lit);
209 LOG ("scheduling %d with %" PRId64 " positive and %" PRId64 " negative occurrences",
210 lit, noccs (lit), noccs (-lit));
211 blocker.schedule.push_back (vlit (lit));
212 }
213 }
214
215 PHASE ("block", stats.blockings,
216 "scheduled %zd candidate literals %.2f%% (%d skipped %.2f%%)",
217 blocker.schedule.size (),
218 percent (blocker.schedule.size (), 2.0*active ()),
219 skipped, percent (skipped, 2.0*active ()));
220 }
221
222 /*------------------------------------------------------------------------*/
223
224 // A literal is pure if it only occurs positive. Then all clauses in which
225 // it occurs are blocked on it. This special case can be implemented faster
226 // than trying to block literals with at least one negative occurrence and
227 // is thus handled separately. It also allows to avoid pushing blocked
228 // clauses onto the extension stack.
229
block_pure_literal(Blocker & blocker,int lit)230 void Internal::block_pure_literal (Blocker & blocker, int lit)
231 {
232 if (frozen (lit)) return;
233 assert (active (lit));
234
235 Occs & pos = occs (lit);
236 Occs & nos = occs (-lit);
237
238 assert (!noccs (-lit));
239 #ifndef NDEBUG
240 for (const auto & c : nos) assert (c->garbage);
241 #endif
242 stats.blockpurelits++;
243 LOG ("found pure literal %d", lit);
244
245 int64_t pured = 0;
246
247 for (const auto & c : pos) {
248 if (c->garbage) continue;
249 assert (!c->redundant);
250 LOG (c, "pure literal %d in", lit);
251 blocker.reschedule.push_back (c);
252 external->push_clause_on_extension_stack (c, lit);
253 stats.blockpured++;
254 mark_garbage (c);
255 pured++;
256 }
257
258 erase_vector (pos);
259 erase_vector (nos);
260
261 mark_pure (lit);
262 stats.blockpured++;
263 LOG ("blocking %" PRId64 " clauses on pure literal %d", pured, lit);
264 }
265
266 /*------------------------------------------------------------------------*/
267
268 // If there is only one negative clause with '-lit' it is faster to mark it
269 // instead of marking all the positive clauses with 'lit' one after the
270 // other and then resolving against the negative clause.
271
272 void
block_literal_with_one_negative_occ(Blocker & blocker,int lit)273 Internal::block_literal_with_one_negative_occ (Blocker & blocker, int lit)
274 {
275 assert (active (lit));
276 assert (!frozen (lit));
277 assert (noccs (lit) > 0);
278 assert (noccs (-lit) == 1);
279
280 Occs & nos = occs (-lit);
281 assert (nos.size () >= 1);
282
283 Clause * d = 0;
284 for (const auto & c : nos) {
285 if (c->garbage) continue;
286 assert (!d);
287 d = c;
288 #ifndef NDEBUG
289 break;
290 #endif
291 }
292 assert (d);
293 nos.resize (1);
294 nos[0] = d;
295
296 if (d && d->size > opts.blockmaxclslim) {
297 LOG (d, "skipped common antecedent");
298 return;
299 }
300
301 assert (!d->garbage);
302 assert (!d->redundant);
303 assert (d->size <= opts.blockmaxclslim);
304
305 LOG (d, "common antecedent", lit);
306 mark (d);
307
308 int64_t blocked = 0, skipped = 0;
309
310 Occs & pos = occs (lit);
311
312 // Again no 'auto' since 'pos' is update during traversal.
313 //
314 const auto eop = pos.end ();
315 auto j = pos.begin (), i = j;
316
317 for (; i != eop; i++)
318 {
319 Clause * c = *j++ = *i;
320
321 if (c->garbage) { j--; continue; }
322 if (c->size > opts.blockmaxclslim) { skipped++; continue; }
323 if (c->size < opts.blockminclslim) { skipped++; continue; }
324
325 LOG (c, "trying to block on %d", lit);
326
327 // We use the same literal move-to-front strategy as in
328 // 'is_blocked_clause'. See there for more explanations.
329
330 int prev_other = 0; // Previous non-tautological literal.
331
332 // No 'auto' since literals of 'c' are updated during traversal.
333 //
334 const const_literal_iterator end_of_c = c->end ();
335 literal_iterator l;
336
337 for (l = c->begin (); l != end_of_c; l++)
338 {
339 const int other = *l;
340 *l = prev_other;
341 prev_other = other;
342 if (other == lit) continue;
343 assert (other != -lit);
344 assert (active (other));
345 assert (!val (other));
346 if (marked (other) < 0) {
347 LOG ("found tautological literal %d", other);
348 c->literals[0] = other; // Move to front of 'c'.
349 break;
350 }
351 }
352
353 if (l == end_of_c) {
354 LOG ("no tautological literal found");
355
356 // Restore old literal order in the clause because.
357
358 const const_literal_iterator begin_of_c = c->begin ();
359 while (l-- != begin_of_c) {
360 const int other = *l;
361 *l = prev_other;
362 prev_other = other;
363 }
364
365 continue; // ... with next candidate 'c' in 'pos'.
366 }
367
368 blocked++;
369 LOG (c, "blocked");
370 external->push_clause_on_extension_stack (c, lit);
371 blocker.reschedule.push_back (c);
372 mark_garbage (c);
373 j--;
374 }
375 if (j == pos.begin ()) erase_vector (pos);
376 else pos.resize (j - pos.begin ());
377
378 stats.blocked += blocked;
379 LOG ("blocked %" PRId64 " clauses on %d (skipped %" PRId64 ")", blocked, lit, skipped);
380
381 unmark (d);
382 }
383
384 /*------------------------------------------------------------------------*/
385
386 // Determine the set of candidate clauses with 'lit', which are checked to
387 // be blocked by 'lit'. Filter out too large and small clauses and which do
388 // not have any negated other literal in any of the clauses with '-lit'.
389
block_candidates(Blocker & blocker,int lit)390 size_t Internal::block_candidates (Blocker & blocker, int lit) {
391
392 assert (blocker.candidates.empty ());
393
394 Occs & pos = occs (lit); // Positive occurrences of 'lit'.
395 Occs & nos = occs (-lit);
396
397 assert ((size_t) noccs (lit) <= pos.size ());
398 assert ((size_t) noccs (-lit) == nos.size ()); // Already flushed.
399
400 // Mark all literals in clauses with '-lit'. Note that 'mark2' uses
401 // separate bits for 'lit' and '-lit'.
402 //
403 for (const auto & c : nos) mark2 (c);
404
405 const auto eop = pos.end ();
406 auto j = pos.begin (), i = j;
407
408 for (; i != eop; i++)
409 {
410 Clause * c = *j++ = *i;
411 if (c->garbage) { j--; continue; }
412 assert (!c->redundant);
413 if (c->size > opts.blockmaxclslim) continue;
414 if (c->size < opts.blockminclslim) continue;
415 const const_literal_iterator eoc = c->end ();
416 const_literal_iterator l;
417 for (l = c->begin (); l != eoc; l++) {
418 const int other = *l;
419 if (other == lit) continue;
420 assert (other != -lit);
421 assert (active (other));
422 assert (!val (other));
423 if (marked2 (-other)) break;
424 }
425 if (l != eoc) blocker.candidates.push_back (c);
426 }
427 if (j == pos.begin ()) erase_vector (pos);
428 else pos.resize (j - pos.begin ());
429
430 assert (pos.size () == (size_t) noccs (lit)); // Now also flushed.
431
432 for (const auto & c : nos) unmark (c);
433
434 return blocker.candidates.size ();
435 }
436
437 /*------------------------------------------------------------------------*/
438
439 // Try to find a clause with '-lit' which does not have any literal in
440 // clauses with 'lit'. If such a clause exists no candidate clause can be
441 // blocked on 'lit' since all candidates would produce a non-tautological
442 // resolvent with that clause.
443
block_impossible(Blocker & blocker,int lit)444 Clause * Internal::block_impossible (Blocker & blocker, int lit)
445 {
446 assert (noccs (-lit) > 1);
447 assert (blocker.candidates.size () > 1);
448
449 for (const auto & c : blocker.candidates) mark2 (c);
450
451 Occs & nos = occs (-lit);
452 Clause * res = 0;
453
454 for (const auto & c : nos) {
455 assert (!c->garbage);
456 assert (!c->redundant);
457 assert (c->size <= opts.blockmaxclslim);
458 const const_literal_iterator eoc = c->end ();
459 const_literal_iterator l;
460 for (l = c->begin (); l != eoc; l++) {
461 const int other = *l;
462 if (other == -lit) continue;
463 assert (other != lit);
464 assert (active (other));
465 assert (!val (other));
466 if (marked2 (-other)) break;
467 }
468 if (l == eoc) res = c;
469 }
470
471 for (const auto & c : blocker.candidates) unmark (c);
472
473 if (res) {
474 LOG (res, "common non-tautological resolvent producing");
475 blocker.candidates.clear ();
476 }
477
478 return res;
479 }
480
481 /*------------------------------------------------------------------------*/
482
483 // In the general case we have at least two negative occurrences.
484
block_literal_with_at_least_two_negative_occs(Blocker & blocker,int lit)485 void Internal::block_literal_with_at_least_two_negative_occs (
486 Blocker & blocker,
487 int lit)
488 {
489 assert (active (lit));
490 assert (!frozen (lit));
491 assert (noccs (lit) > 0);
492 assert (noccs (-lit) > 1);
493
494 Occs & nos = occs (-lit);
495 assert ((size_t) noccs (-lit) <= nos.size ());
496
497 int max_size = 0;
498
499 // Flush all garbage clauses in occurrence list 'nos' of '-lit' and
500 // determine the maximum size of negative clauses (with '-lit').
501 //
502 const auto eon = nos.end ();
503 auto j = nos.begin (), i = j;
504 for (; i != eon; i++)
505 {
506 Clause * c = *j++ = *i;
507 if (c->garbage) j--;
508 else if (c->size > max_size) max_size = c->size;
509 }
510 if (j == nos.begin ()) erase_vector (nos);
511 else nos.resize (j - nos.begin ());
512
513 assert (nos.size () == (size_t) noccs (-lit));
514 assert (nos.size () > 1);
515
516 // If the maximum size of a negative clause (with '-lit') exceeds the
517 // maximum clause size limit ignore this candidate literal.
518 //
519 if (max_size > opts.blockmaxclslim) {
520 LOG ("maximum size %d of clauses with %d exceeds clause size limit %d",
521 max_size, -lit, opts.blockmaxclslim);
522 return;
523 }
524
525 LOG ("maximum size %d of clauses with %d", max_size, -lit);
526
527 // We filter candidate clauses with positive occurrence of 'lit' in
528 // 'blocker.candidates' and return if no candidate clause remains.
529 // Candidates should be small enough and should have at least one literal
530 // which occurs negated in one of the clauses with '-lit'.
531 //
532 size_t candidates = block_candidates (blocker, lit);
533 if (!candidates) {
534 LOG ("no candidate clauses found");
535 return;
536 }
537
538 LOG ("found %zd candidate clauses", candidates);
539
540 // We further search for a clause with '-lit' that has no literal
541 // negated in any of the candidate clauses (except 'lit'). If such a
542 // clause exists, we know that none of the candidates is blocked.
543 //
544 if (candidates > 1 && block_impossible (blocker, lit)) {
545 LOG ("impossible to block any candidate clause on %d", lit);
546 assert (blocker.candidates.empty ());
547 return;
548 }
549
550 LOG ("trying to block %zd clauses out of %" PRId64 " with literal %d",
551 candidates, noccs (lit), lit);
552
553 int64_t blocked = 0;
554
555 // Go over all remaining candidates and try to block them on 'lit'.
556 //
557 for (const auto & c : blocker.candidates) {
558 assert (!c->garbage);
559 assert (!c->redundant);
560 if (!is_blocked_clause (c, lit)) continue;
561 blocked++;
562 LOG (c, "blocked");
563 external->push_clause_on_extension_stack (c, lit);
564 blocker.reschedule.push_back (c);
565 mark_garbage (c);
566 }
567
568 LOG ("blocked %" PRId64 " clauses on %d out of %zd candidates in %zd occurrences",
569 blocked, lit, blocker.candidates.size (), occs (lit).size ());
570
571 blocker.candidates.clear ();
572 stats.blocked += blocked;
573 if (blocked) flush_occs (lit);
574 }
575
576 /*------------------------------------------------------------------------*/
577
578 // Reschedule literals in a clause (except 'lit') which was blocked.
579
580 void
block_reschedule_clause(Blocker & blocker,int lit,Clause * c)581 Internal::block_reschedule_clause (Blocker & blocker, int lit, Clause * c)
582 {
583 #ifdef NDEBUG
584 (void) lit;
585 #endif
586 assert (c->garbage);
587
588 for (const auto & other : *c) {
589
590 int64_t & n = noccs (other);
591 assert (n > 0);
592 n--;
593
594 LOG ("updating %d with %" PRId64 " positive and %" PRId64 " negative occurrences",
595 other, noccs (other), noccs (-other));
596
597 if (blocker.schedule.contains (vlit (-other)))
598 blocker.schedule.update (vlit (-other));
599 else if (active (other) &&
600 !frozen (other) &&
601 !marked_skip (-other)) {
602 LOG ("rescheduling to block clauses on %d", -other);
603 blocker.schedule.push_back (vlit (-other));
604 }
605
606 if (blocker.schedule.contains (vlit (other))) {
607 assert (other != lit);
608 blocker.schedule.update (vlit (other));
609 }
610 }
611 }
612
613 // Reschedule all literals in clauses blocked by 'lit' (except 'lit').
614
block_reschedule(Blocker & blocker,int lit)615 void Internal::block_reschedule (Blocker & blocker, int lit)
616 {
617 while (!blocker.reschedule.empty ()) {
618 Clause * c = blocker.reschedule.back ();
619 blocker.reschedule.pop_back ();
620 block_reschedule_clause (blocker, lit, c);
621 }
622 }
623
624 /*------------------------------------------------------------------------*/
625
block_literal(Blocker & blocker,int lit)626 void Internal::block_literal (Blocker & blocker, int lit)
627 {
628 assert (!marked_skip (lit));
629
630 if (!active (lit)) return; // Pure literal '-lit'.
631 if (frozen (lit)) return;
632
633 assert (!val (lit));
634
635 // If the maximum number of a negative clauses (with '-lit') exceeds the
636 // occurrence limit ignore this candidate literal.
637 //
638 if (noccs (-lit) > opts.blockocclim) return;
639
640 LOG ("blocking literal candidate %d "
641 "with %" PRId64 " positive and %" PRId64 " negative occurrences",
642 lit, noccs (lit), noccs (-lit));
643
644 stats.blockcands++;
645
646 assert (blocker.reschedule.empty ());
647 assert (blocker.candidates.empty ());
648
649 if (!noccs (-lit)) block_pure_literal (blocker, lit);
650 else if (!noccs (lit)) {
651 // Rare situation, where the clause length limit was hit for 'lit' and
652 // '-lit' is skipped and then it becomes pure. Can be ignored.
653 assert (frozen (lit) || marked_skip (-lit));
654 } else if (noccs (-lit) == 1)
655 block_literal_with_one_negative_occ (blocker, lit);
656 else
657 block_literal_with_at_least_two_negative_occs (blocker, lit);
658
659 // Done with blocked clause elimination on this literal and we do not
660 // have to try blocked clause elimination on it again until irredundant
661 // clauses with its negation are removed.
662 //
663 assert (!frozen (lit)); // just to be sure ...
664 unmark_block (lit);
665 }
666
667 /*------------------------------------------------------------------------*/
668
block()669 bool Internal::block () {
670
671 if (!opts.block) return false;
672 if (unsat || terminating () || !stats.current.irredundant) return false;
673
674 assert (opts.simplify);
675
676 if (propagated < trail.size ()) {
677 LOG ("need to propagate %zd units first", trail.size () - propagated);
678 init_watches ();
679 connect_watches ();
680 if (!propagate ()) {
681 LOG ("propagating units results in empty clause");
682 learn_empty_clause ();
683 assert (unsat);
684 }
685 disconnect_watches ();
686 reset_watches ();
687 if (unsat) return false;
688 }
689
690 START_SIMPLIFIER (block, BLOCK);
691
692 stats.blockings++;
693
694 LOG ("block-%" PRId64 "", stats.blockings);
695
696 assert (!level);
697 assert (!watching ());
698 assert (!occurring ());
699
700 mark_satisfied_clauses_as_garbage ();
701
702 init_occs (); // Occurrence lists for all literals.
703 init_noccs (); // Number of occurrences to avoid flushing garbage clauses.
704
705 Blocker blocker (this);
706 block_schedule (blocker);
707
708 int64_t blocked = stats.blocked;
709 int64_t resolutions = stats.blockres;
710 int64_t purelits = stats.blockpurelits;
711 int64_t pured = stats.blockpured;
712
713 while (!terminating () &&
714 !blocker.schedule.empty ()) {
715 int lit = u2i (blocker.schedule.front ());
716 blocker.schedule.pop_front ();
717 block_literal (blocker, lit);
718 block_reschedule (blocker, lit);
719 }
720
721 blocker.erase ();
722 reset_noccs ();
723 reset_occs ();
724
725 resolutions = stats.blockres - resolutions;
726 blocked = stats.blocked - blocked;
727
728 PHASE ("block", stats.blockings,
729 "blocked %" PRId64 " clauses in %" PRId64 " resolutions",
730 blocked, resolutions);
731
732 pured = stats.blockpured - pured;
733 purelits = stats.blockpurelits - purelits;
734
735 if (pured)
736 mark_redundant_clauses_with_eliminated_variables_as_garbage ();
737
738 if (purelits)
739 PHASE ("block", stats.blockings,
740 "found %" PRId64 " pure literals in %" PRId64 " clauses",
741 purelits, pured);
742 else
743 PHASE ("block", stats.blockings,
744 "no pure literals found");
745
746 report ('b', !opts.reportall && !blocked);
747
748 STOP_SIMPLIFIER (block, BLOCK);
749
750 return blocked;
751 }
752
753 }
754