1 /* Derivation and subsumption rules for constraints.
2 Copyright (C) 2013-2021 Free Software Foundation, Inc.
3 Contributed by Andrew Sutton (andrew.n.sutton@gmail.com)
4
5 This file is part of GCC.
6
7 GCC is free software; you can redistribute it and/or modify
8 it under the terms of the GNU General Public License as published by
9 the Free Software Foundation; either version 3, or (at your option)
10 any later version.
11
12 GCC is distributed in the hope that it will be useful,
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 GNU General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with GCC; see the file COPYING3. If not see
19 <http://www.gnu.org/licenses/>. */
20
21 #include "config.h"
22 #define INCLUDE_LIST
23 #include "system.h"
24 #include "coretypes.h"
25 #include "tm.h"
26 #include "timevar.h"
27 #include "hash-set.h"
28 #include "machmode.h"
29 #include "vec.h"
30 #include "double-int.h"
31 #include "input.h"
32 #include "alias.h"
33 #include "symtab.h"
34 #include "wide-int.h"
35 #include "inchash.h"
36 #include "tree.h"
37 #include "stringpool.h"
38 #include "attribs.h"
39 #include "intl.h"
40 #include "flags.h"
41 #include "cp-tree.h"
42 #include "c-family/c-common.h"
43 #include "c-family/c-objc.h"
44 #include "cp-objcp-common.h"
45 #include "tree-inline.h"
46 #include "decl.h"
47 #include "toplev.h"
48 #include "type-utils.h"
49
50 /* A conjunctive or disjunctive clause.
51
52 Each clause maintains an iterator that refers to the current
53 term, which is used in the linear decomposition of a formula
54 into CNF or DNF. */
55
56 struct clause
57 {
58 typedef std::list<tree>::iterator iterator;
59 typedef std::list<tree>::const_iterator const_iterator;
60
61 /* Initialize a clause with an initial term. */
62
clauseclause63 clause (tree t)
64 {
65 m_terms.push_back (t);
66 if (TREE_CODE (t) == ATOMIC_CONSTR)
67 m_set.add (t);
68
69 m_current = m_terms.begin ();
70 }
71
72 /* Create a copy of the current term. The current
73 iterator is set to point to the same position in the
74 copied list of terms. */
75
clauseclause76 clause (clause const& c)
77 : m_terms (c.m_terms), m_set (c.m_set), m_current (m_terms.begin ())
78 {
79 std::advance (m_current, std::distance (c.begin (), c.current ()));
80 }
81
82 /* Returns true when all terms are atoms. */
83
doneclause84 bool done () const
85 {
86 return m_current == end ();
87 }
88
89 /* Advance to the next term. */
90
advanceclause91 void advance ()
92 {
93 gcc_assert (!done ());
94 ++m_current;
95 }
96
97 /* Replaces the current term at position ITER with T. If
98 T is an atomic constraint that already appears in the
99 clause, remove but do not replace ITER. Returns a pair
100 containing an iterator to the replace object or past
101 the erased object and a boolean value which is true if
102 an object was erased. */
103
replaceclause104 std::pair<iterator, bool> replace (iterator iter, tree t)
105 {
106 gcc_assert (TREE_CODE (*iter) != ATOMIC_CONSTR);
107 if (TREE_CODE (t) == ATOMIC_CONSTR)
108 {
109 if (m_set.add (t))
110 return std::make_pair (m_terms.erase (iter), true);
111 }
112 *iter = t;
113 return std::make_pair (iter, false);
114 }
115
116 /* Inserts T before ITER in the list of terms. If T has
117 already is an atomic constraint that already appears in
118 the clause, no action is taken, and the current iterator
119 is returned. Returns a pair of an iterator to the inserted
120 object or ITER if no insertion occurred and a boolean
121 value which is true if an object was inserted. */
122
insertclause123 std::pair<iterator, bool> insert (iterator iter, tree t)
124 {
125 if (TREE_CODE (t) == ATOMIC_CONSTR)
126 {
127 if (m_set.add (t))
128 return std::make_pair (iter, false);
129 }
130 return std::make_pair (m_terms.insert (iter, t), true);
131 }
132
133 /* Replaces the current term with T. In the case where the
134 current term is erased (because T is redundant), update
135 the position of the current term to the next term. */
136
replaceclause137 void replace (tree t)
138 {
139 m_current = replace (m_current, t).first;
140 }
141
142 /* Replace the current term with T1 and T2, in that order. */
143
replaceclause144 void replace (tree t1, tree t2)
145 {
146 /* Replace the current term with t1. Ensure that iter points
147 to the term before which t2 will be inserted. Update the
148 current term as needed. */
149 std::pair<iterator, bool> rep = replace (m_current, t1);
150 if (rep.second)
151 m_current = rep.first;
152 else
153 ++rep.first;
154
155 /* Insert the t2. Make this the current term if we erased
156 the prior term. */
157 std::pair<iterator, bool> ins = insert (rep.first, t2);
158 if (rep.second && ins.second)
159 m_current = ins.first;
160 }
161
162 /* Returns true if the clause contains the term T. */
163
containsclause164 bool contains (tree t)
165 {
166 gcc_assert (TREE_CODE (t) == ATOMIC_CONSTR);
167 return m_set.contains (t);
168 }
169
170
171 /* Returns an iterator to the first clause in the formula. */
172
beginclause173 iterator begin ()
174 {
175 return m_terms.begin ();
176 }
177
178 /* Returns an iterator to the first clause in the formula. */
179
beginclause180 const_iterator begin () const
181 {
182 return m_terms.begin ();
183 }
184
185 /* Returns an iterator past the last clause in the formula. */
186
endclause187 iterator end ()
188 {
189 return m_terms.end ();
190 }
191
192 /* Returns an iterator past the last clause in the formula. */
193
endclause194 const_iterator end () const
195 {
196 return m_terms.end ();
197 }
198
199 /* Returns the current iterator. */
200
currentclause201 const_iterator current () const
202 {
203 return m_current;
204 }
205
206 std::list<tree> m_terms; /* The list of terms. */
207 hash_set<tree, false, atom_hasher> m_set; /* The set of atomic constraints. */
208 iterator m_current; /* The current term. */
209 };
210
211
212 /* A proof state owns a list of goals and tracks the
213 current sub-goal. The class also provides facilities
214 for managing subgoals and constructing term lists. */
215
216 struct formula
217 {
218 typedef std::list<clause>::iterator iterator;
219 typedef std::list<clause>::const_iterator const_iterator;
220
221 /* Construct a formula with an initial formula in a
222 single clause. */
223
formulaformula224 formula (tree t)
225 {
226 /* This should call emplace_back(). There's an extra copy being
227 invoked by using push_back(). */
228 m_clauses.push_back (t);
229 m_current = m_clauses.begin ();
230 }
231
232 /* Returns true when all clauses are atomic. */
doneformula233 bool done () const
234 {
235 return m_current == end ();
236 }
237
238 /* Advance to the next term. */
advanceformula239 void advance ()
240 {
241 gcc_assert (!done ());
242 ++m_current;
243 }
244
245 /* Insert a copy of clause into the formula. This corresponds
246 to a distribution of one logical operation over the other. */
247
branchformula248 clause& branch ()
249 {
250 gcc_assert (!done ());
251 m_clauses.push_back (*m_current);
252 return m_clauses.back ();
253 }
254
255 /* Returns the position of the current clause. */
256
currentformula257 iterator current ()
258 {
259 return m_current;
260 }
261
262 /* Returns an iterator to the first clause in the formula. */
263
beginformula264 iterator begin ()
265 {
266 return m_clauses.begin ();
267 }
268
269 /* Returns an iterator to the first clause in the formula. */
270
beginformula271 const_iterator begin () const
272 {
273 return m_clauses.begin ();
274 }
275
276 /* Returns an iterator past the last clause in the formula. */
277
endformula278 iterator end ()
279 {
280 return m_clauses.end ();
281 }
282
283 /* Returns an iterator past the last clause in the formula. */
284
endformula285 const_iterator end () const
286 {
287 return m_clauses.end ();
288 }
289
290 std::list<clause> m_clauses; /* The list of clauses. */
291 iterator m_current; /* The current clause. */
292 };
293
294 void
debug(clause & c)295 debug (clause& c)
296 {
297 for (clause::iterator i = c.begin(); i != c.end(); ++i)
298 verbatim (" # %E", *i);
299 }
300
301 void
debug(formula & f)302 debug (formula& f)
303 {
304 for (formula::iterator i = f.begin(); i != f.end(); ++i)
305 {
306 /* Format punctuators via %s to avoid -Wformat-diag. */
307 verbatim ("%s", "(((");
308 debug (*i);
309 verbatim ("%s", ")))");
310 }
311 }
312
313 /* The logical rules used to analyze a logical formula. The
314 "left" and "right" refer to the position of formula in a
315 sequent (as in sequent calculus). */
316
317 enum rules
318 {
319 left, right
320 };
321
322 /* Distribution counting. */
323
324 static inline bool
disjunction_p(tree t)325 disjunction_p (tree t)
326 {
327 return TREE_CODE (t) == DISJ_CONSTR;
328 }
329
330 static inline bool
conjunction_p(tree t)331 conjunction_p (tree t)
332 {
333 return TREE_CODE (t) == CONJ_CONSTR;
334 }
335
336 static inline bool
atomic_p(tree t)337 atomic_p (tree t)
338 {
339 return TREE_CODE (t) == ATOMIC_CONSTR;
340 }
341
342 /* Recursively count the number of clauses produced when converting T
343 to DNF. Returns a pair containing the number of clauses and a bool
344 value signifying that the tree would be rewritten as a result of
345 distributing. In general, a conjunction for which this flag is set
346 is considered a disjunction for the purpose of counting. */
347
348 static std::pair<int, bool>
dnf_size_r(tree t)349 dnf_size_r (tree t)
350 {
351 if (atomic_p (t))
352 /* Atomic constraints produce no clauses. */
353 return std::make_pair (0, false);
354
355 /* For compound constraints, recursively count clauses and unpack
356 the results. */
357 tree lhs = TREE_OPERAND (t, 0);
358 tree rhs = TREE_OPERAND (t, 1);
359 std::pair<int, bool> p1 = dnf_size_r (lhs);
360 std::pair<int, bool> p2 = dnf_size_r (rhs);
361 int n1 = p1.first, n2 = p2.first;
362 bool d1 = p1.second, d2 = p2.second;
363
364 if (disjunction_p (t))
365 {
366 /* Matches constraints of the form P \/ Q. Disjunctions contribute
367 linearly to the number of constraints. When both P and Q are
368 disjunctions, clauses are added. When only one of P and Q
369 is a disjunction, an additional clause is produced. When neither
370 P nor Q are disjunctions, two clauses are produced. */
371 if (disjunction_p (lhs))
372 {
373 if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
374 /* Both P and Q are disjunctions. */
375 return std::make_pair (n1 + n2, d1 | d2);
376 else
377 /* Only LHS is a disjunction. */
378 return std::make_pair (1 + n1 + n2, d1 | d2);
379 gcc_unreachable ();
380 }
381 if (conjunction_p (lhs))
382 {
383 if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
384 /* Both P and Q are disjunctions. */
385 return std::make_pair (n1 + n2, d1 | d2);
386 if (disjunction_p (rhs)
387 || (conjunction_p (rhs) && d1 != d2)
388 || (atomic_p (rhs) && d1))
389 /* Either LHS or RHS is a disjunction. */
390 return std::make_pair (1 + n1 + n2, d1 | d2);
391 else
392 /* Neither LHS nor RHS is a disjunction. */
393 return std::make_pair (2, false);
394 }
395 if (atomic_p (lhs))
396 {
397 if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
398 /* Only RHS is a disjunction. */
399 return std::make_pair (1 + n1 + n2, d1 | d2);
400 else
401 /* Neither LHS nor RHS is a disjunction. */
402 return std::make_pair (2, false);
403 }
404 }
405 else /* conjunction_p (t) */
406 {
407 /* Matches constraints of the form P /\ Q, possibly resulting
408 in the distribution of one side over the other. When both
409 P and Q are disjunctions, the number of clauses are multiplied.
410 When only one of P and Q is a disjunction, the number of
411 clauses are added. Otherwise, neither side is a disjunction and
412 no clauses are created. */
413 if (disjunction_p (lhs))
414 {
415 if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
416 /* Both P and Q are disjunctions. */
417 return std::make_pair (n1 * n2, true);
418 else
419 /* Only LHS is a disjunction. */
420 return std::make_pair (n1 + n2, true);
421 gcc_unreachable ();
422 }
423 if (conjunction_p (lhs))
424 {
425 if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
426 /* Both P and Q are disjunctions. */
427 return std::make_pair (n1 * n2, true);
428 if (disjunction_p (rhs)
429 || (conjunction_p (rhs) && d1 != d2)
430 || (atomic_p (rhs) && d1))
431 /* Either LHS or RHS is a disjunction. */
432 return std::make_pair (n1 + n2, true);
433 else
434 /* Neither LHS nor RHS is a disjunction. */
435 return std::make_pair (0, false);
436 }
437 if (atomic_p (lhs))
438 {
439 if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
440 /* Only RHS is a disjunction. */
441 return std::make_pair (n1 + n2, true);
442 else
443 /* Neither LHS nor RHS is a disjunction. */
444 return std::make_pair (0, false);
445 }
446 }
447 gcc_unreachable ();
448 }
449
450 /* Recursively count the number of clauses produced when converting T
451 to CNF. Returns a pair containing the number of clauses and a bool
452 value signifying that the tree would be rewritten as a result of
453 distributing. In general, a disjunction for which this flag is set
454 is considered a conjunction for the purpose of counting. */
455
456 static std::pair<int, bool>
cnf_size_r(tree t)457 cnf_size_r (tree t)
458 {
459 if (atomic_p (t))
460 /* Atomic constraints produce no clauses. */
461 return std::make_pair (0, false);
462
463 /* For compound constraints, recursively count clauses and unpack
464 the results. */
465 tree lhs = TREE_OPERAND (t, 0);
466 tree rhs = TREE_OPERAND (t, 1);
467 std::pair<int, bool> p1 = cnf_size_r (lhs);
468 std::pair<int, bool> p2 = cnf_size_r (rhs);
469 int n1 = p1.first, n2 = p2.first;
470 bool d1 = p1.second, d2 = p2.second;
471
472 if (disjunction_p (t))
473 {
474 /* Matches constraints of the form P \/ Q, possibly resulting
475 in the distribution of one side over the other. When both
476 P and Q are conjunctions, the number of clauses are multiplied.
477 When only one of P and Q is a conjunction, the number of
478 clauses are added. Otherwise, neither side is a conjunction and
479 no clauses are created. */
480 if (disjunction_p (lhs))
481 {
482 if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
483 /* Both P and Q are conjunctions. */
484 return std::make_pair (n1 * n2, true);
485 if ((disjunction_p (rhs) && d1 != d2)
486 || conjunction_p (rhs)
487 || (atomic_p (rhs) && d1))
488 /* Either LHS or RHS is a conjunction. */
489 return std::make_pair (n1 + n2, true);
490 else
491 /* Neither LHS nor RHS is a conjunction. */
492 return std::make_pair (0, false);
493 gcc_unreachable ();
494 }
495 if (conjunction_p (lhs))
496 {
497 if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
498 /* Both LHS and RHS are conjunctions. */
499 return std::make_pair (n1 * n2, true);
500 else
501 /* Only LHS is a conjunction. */
502 return std::make_pair (n1 + n2, true);
503 }
504 if (atomic_p (lhs))
505 {
506 if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
507 /* Only RHS is a disjunction. */
508 return std::make_pair (n1 + n2, true);
509 else
510 /* Neither LHS nor RHS is a disjunction. */
511 return std::make_pair (0, false);
512 }
513 }
514 else /* conjunction_p (t) */
515 {
516 /* Matches constraints of the form P /\ Q. Conjunctions contribute
517 linearly to the number of constraints. When both P and Q are
518 conjunctions, clauses are added. When only one of P and Q
519 is a conjunction, an additional clause is produced. When neither
520 P nor Q are conjunctions, two clauses are produced. */
521 if (disjunction_p (lhs))
522 {
523 if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
524 /* Both P and Q are conjunctions. */
525 return std::make_pair (n1 + n2, d1 | d2);
526 if ((disjunction_p (rhs) && d1 != d2)
527 || conjunction_p (rhs)
528 || (atomic_p (rhs) && d1))
529 /* Either LHS or RHS is a conjunction. */
530 return std::make_pair (1 + n1 + n2, d1 | d2);
531 else
532 /* Neither LHS nor RHS is a conjunction. */
533 return std::make_pair (2, false);
534 gcc_unreachable ();
535 }
536 if (conjunction_p (lhs))
537 {
538 if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
539 /* Both LHS and RHS are conjunctions. */
540 return std::make_pair (n1 + n2, d1 | d2);
541 else
542 /* Only LHS is a conjunction. */
543 return std::make_pair (1 + n1 + n2, d1 | d2);
544 }
545 if (atomic_p (lhs))
546 {
547 if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
548 /* Only RHS is a disjunction. */
549 return std::make_pair (1 + n1 + n2, d1 | d2);
550 else
551 /* Neither LHS nor RHS is a disjunction. */
552 return std::make_pair (2, false);
553 }
554 }
555 gcc_unreachable ();
556 }
557
558 /* Count the number conjunctive clauses that would be created
559 when rewriting T to DNF. */
560
561 static int
dnf_size(tree t)562 dnf_size (tree t)
563 {
564 std::pair<int, bool> result = dnf_size_r (t);
565 return result.first == 0 ? 1 : result.first;
566 }
567
568
569 /* Count the number disjunctive clauses that would be created
570 when rewriting T to CNF. */
571
572 static int
cnf_size(tree t)573 cnf_size (tree t)
574 {
575 std::pair<int, bool> result = cnf_size_r (t);
576 return result.first == 0 ? 1 : result.first;
577 }
578
579
580 /* A left-conjunction is replaced by its operands. */
581
582 void
replace_term(clause & c,tree t)583 replace_term (clause& c, tree t)
584 {
585 tree t1 = TREE_OPERAND (t, 0);
586 tree t2 = TREE_OPERAND (t, 1);
587 return c.replace (t1, t2);
588 }
589
590 /* Create a new clause in the formula by copying the current
591 clause. In the current clause, the term at CI is replaced
592 by the first operand, and in the new clause, it is replaced
593 by the second. */
594
595 void
branch_clause(formula & f,clause & c1,tree t)596 branch_clause (formula& f, clause& c1, tree t)
597 {
598 tree t1 = TREE_OPERAND (t, 0);
599 tree t2 = TREE_OPERAND (t, 1);
600 clause& c2 = f.branch ();
601 c1.replace (t1);
602 c2.replace (t2);
603 }
604
605 /* Decompose t1 /\ t2 according to the rules R. */
606
607 inline void
decompose_conjuntion(formula & f,clause & c,tree t,rules r)608 decompose_conjuntion (formula& f, clause& c, tree t, rules r)
609 {
610 if (r == left)
611 replace_term (c, t);
612 else
613 branch_clause (f, c, t);
614 }
615
616 /* Decompose t1 \/ t2 according to the rules R. */
617
618 inline void
decompose_disjunction(formula & f,clause & c,tree t,rules r)619 decompose_disjunction (formula& f, clause& c, tree t, rules r)
620 {
621 if (r == right)
622 replace_term (c, t);
623 else
624 branch_clause (f, c, t);
625 }
626
627 /* An atomic constraint is already decomposed. */
628 inline void
decompose_atom(clause & c)629 decompose_atom (clause& c)
630 {
631 c.advance ();
632 }
633
634 /* Decompose a term of clause C (in formula F) according to the
635 logical rules R. */
636
637 void
decompose_term(formula & f,clause & c,tree t,rules r)638 decompose_term (formula& f, clause& c, tree t, rules r)
639 {
640 switch (TREE_CODE (t))
641 {
642 case CONJ_CONSTR:
643 return decompose_conjuntion (f, c, t, r);
644 case DISJ_CONSTR:
645 return decompose_disjunction (f, c, t, r);
646 default:
647 return decompose_atom (c);
648 }
649 }
650
651 /* Decompose C (in F) using the logical rules R until it
652 is comprised of only atomic constraints. */
653
654 void
decompose_clause(formula & f,clause & c,rules r)655 decompose_clause (formula& f, clause& c, rules r)
656 {
657 while (!c.done ())
658 decompose_term (f, c, *c.current (), r);
659 f.advance ();
660 }
661
662 /* Decompose the logical formula F according to the logical
663 rules determined by R. The result is a formula containing
664 clauses that contain only atomic terms. */
665
666 void
decompose_formula(formula & f,rules r)667 decompose_formula (formula& f, rules r)
668 {
669 while (!f.done ())
670 decompose_clause (f, *f.current (), r);
671 }
672
673 /* Fully decomposing T into a list of sequents, each comprised of
674 a list of atomic constraints, as if T were an antecedent. */
675
676 static formula
decompose_antecedents(tree t)677 decompose_antecedents (tree t)
678 {
679 formula f (t);
680 decompose_formula (f, left);
681 return f;
682 }
683
684 /* Fully decomposing T into a list of sequents, each comprised of
685 a list of atomic constraints, as if T were a consequent. */
686
687 static formula
decompose_consequents(tree t)688 decompose_consequents (tree t)
689 {
690 formula f (t);
691 decompose_formula (f, right);
692 return f;
693 }
694
695 static bool derive_proof (clause&, tree, rules);
696
697 /* Derive a proof of both operands of T. */
698
699 static bool
derive_proof_for_both_operands(clause & c,tree t,rules r)700 derive_proof_for_both_operands (clause& c, tree t, rules r)
701 {
702 if (!derive_proof (c, TREE_OPERAND (t, 0), r))
703 return false;
704 return derive_proof (c, TREE_OPERAND (t, 1), r);
705 }
706
707 /* Derive a proof of either operand of T. */
708
709 static bool
derive_proof_for_either_operand(clause & c,tree t,rules r)710 derive_proof_for_either_operand (clause& c, tree t, rules r)
711 {
712 if (derive_proof (c, TREE_OPERAND (t, 0), r))
713 return true;
714 return derive_proof (c, TREE_OPERAND (t, 1), r);
715 }
716
717 /* Derive a proof of the atomic constraint T in clause C. */
718
719 static bool
derive_atomic_proof(clause & c,tree t)720 derive_atomic_proof (clause& c, tree t)
721 {
722 return c.contains (t);
723 }
724
725 /* Derive a proof of T from the terms in C. */
726
727 static bool
derive_proof(clause & c,tree t,rules r)728 derive_proof (clause& c, tree t, rules r)
729 {
730 switch (TREE_CODE (t))
731 {
732 case CONJ_CONSTR:
733 if (r == left)
734 return derive_proof_for_both_operands (c, t, r);
735 else
736 return derive_proof_for_either_operand (c, t, r);
737 case DISJ_CONSTR:
738 if (r == left)
739 return derive_proof_for_either_operand (c, t, r);
740 else
741 return derive_proof_for_both_operands (c, t, r);
742 default:
743 return derive_atomic_proof (c, t);
744 }
745 }
746
747 /* Derive a proof of T from disjunctive clauses in F. */
748
749 static bool
derive_proofs(formula & f,tree t,rules r)750 derive_proofs (formula& f, tree t, rules r)
751 {
752 for (formula::iterator i = f.begin(); i != f.end(); ++i)
753 if (!derive_proof (*i, t, r))
754 return false;
755 return true;
756 }
757
758 /* The largest number of clauses in CNF or DNF we accept as input
759 for subsumption. This an upper bound of 2^16 expressions. */
760 static int max_problem_size = 16;
761
762 static inline bool
diagnose_constraint_size(tree t)763 diagnose_constraint_size (tree t)
764 {
765 error_at (input_location, "%qE exceeds the maximum constraint complexity", t);
766 return false;
767 }
768
769 /* Key/value pair for caching subsumption results. This associates a pair of
770 constraints with a boolean value indicating the result. */
771
772 struct GTY((for_user)) subsumption_entry
773 {
774 tree lhs;
775 tree rhs;
776 bool result;
777 };
778
779 /* Hashing function and equality for constraint entries. */
780
781 struct subsumption_hasher : ggc_ptr_hash<subsumption_entry>
782 {
hashsubsumption_hasher783 static hashval_t hash (subsumption_entry *e)
784 {
785 hashval_t val = 0;
786 val = iterative_hash_constraint (e->lhs, val);
787 val = iterative_hash_constraint (e->rhs, val);
788 return val;
789 }
790
equalsubsumption_hasher791 static bool equal (subsumption_entry *e1, subsumption_entry *e2)
792 {
793 if (!constraints_equivalent_p (e1->lhs, e2->lhs))
794 return false;
795 if (!constraints_equivalent_p (e1->rhs, e2->rhs))
796 return false;
797 return true;
798 }
799 };
800
801 /* Caches the results of subsumes_non_null(t1, t1). */
802
803 static GTY ((deletable)) hash_table<subsumption_hasher> *subsumption_cache;
804
805 /* Search for a previously cached subsumption result. */
806
807 static bool*
lookup_subsumption(tree t1,tree t2)808 lookup_subsumption (tree t1, tree t2)
809 {
810 if (!subsumption_cache)
811 return NULL;
812 subsumption_entry elt = { t1, t2, false };
813 subsumption_entry* found = subsumption_cache->find (&elt);
814 if (found)
815 return &found->result;
816 else
817 return 0;
818 }
819
820 /* Save a subsumption result. */
821
822 static bool
save_subsumption(tree t1,tree t2,bool result)823 save_subsumption (tree t1, tree t2, bool result)
824 {
825 if (!subsumption_cache)
826 subsumption_cache = hash_table<subsumption_hasher>::create_ggc(31);
827 subsumption_entry elt = {t1, t2, result};
828 subsumption_entry** slot = subsumption_cache->find_slot (&elt, INSERT);
829 subsumption_entry* entry = ggc_alloc<subsumption_entry> ();
830 *entry = elt;
831 *slot = entry;
832 return result;
833 }
834
835
836 /* Returns true if the LEFT constraint subsume the RIGHT constraints.
837 This is done by deriving a proof of the conclusions on the RIGHT
838 from the assumptions on the LEFT assumptions. */
839
840 static bool
subsumes_constraints_nonnull(tree lhs,tree rhs)841 subsumes_constraints_nonnull (tree lhs, tree rhs)
842 {
843 auto_timevar time (TV_CONSTRAINT_SUB);
844
845 if (bool *b = lookup_subsumption(lhs, rhs))
846 return *b;
847
848 int n1 = dnf_size (lhs);
849 int n2 = cnf_size (rhs);
850
851 /* Make sure we haven't exceeded the largest acceptable problem. */
852 if (std::min (n1, n2) >= max_problem_size)
853 {
854 if (n1 < n2)
855 diagnose_constraint_size (lhs);
856 else
857 diagnose_constraint_size (rhs);
858 return false;
859 }
860
861 /* Decompose the smaller of the two formulas, and recursively
862 check for implication of the larger. */
863 bool result;
864 if (n1 <= n2)
865 {
866 formula dnf = decompose_antecedents (lhs);
867 result = derive_proofs (dnf, rhs, left);
868 }
869 else
870 {
871 formula cnf = decompose_consequents (rhs);
872 result = derive_proofs (cnf, lhs, right);
873 }
874
875 return save_subsumption (lhs, rhs, result);
876 }
877
878 /* Returns true if the LEFT constraints subsume the RIGHT
879 constraints. */
880
881 bool
subsumes(tree lhs,tree rhs)882 subsumes (tree lhs, tree rhs)
883 {
884 if (lhs == rhs)
885 return true;
886 if (!lhs || lhs == error_mark_node)
887 return false;
888 if (!rhs || rhs == error_mark_node)
889 return true;
890 return subsumes_constraints_nonnull (lhs, rhs);
891 }
892
893 #include "gt-cp-logic.h"
894