Line data Source code
1 : /* Derivation and subsumption rules for constraints.
2 : Copyright (C) 2013-2023 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 1542 : 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 :
63 1426 : clause (tree t)
64 1426 : {
65 1426 : m_terms.push_back (t);
66 1426 : if (TREE_CODE (t) == ATOMIC_CONSTR)
67 403 : m_set.add (t);
68 :
69 1426 : m_current = m_terms.begin ();
70 1426 : }
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 :
76 116 : clause (clause const& c)
77 116 : : m_terms (c.m_terms), m_set (c.m_set), m_current (m_terms.begin ())
78 : {
79 116 : std::advance (m_current, std::distance (c.begin (), c.current ()));
80 116 : }
81 :
82 : /* Returns true when all terms are atoms. */
83 :
84 272564 : bool done () const
85 : {
86 272564 : return m_current == end ();
87 : }
88 :
89 : /* Advance to the next term. */
90 :
91 44454 : void advance ()
92 : {
93 0 : gcc_assert (!done ());
94 44454 : ++m_current;
95 44454 : }
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 :
104 182231 : std::pair<iterator, bool> replace (iterator iter, tree t)
105 : {
106 182231 : gcc_assert (TREE_CODE (*iter) != ATOMIC_CONSTR);
107 182231 : if (TREE_CODE (t) == ATOMIC_CONSTR)
108 : {
109 88856 : if (m_set.add (t))
110 69790 : return std::make_pair (m_terms.erase (iter), true);
111 : }
112 112441 : *iter = t;
113 112441 : 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 :
123 181999 : std::pair<iterator, bool> insert (iterator iter, tree t)
124 : {
125 181999 : if (TREE_CODE (t) == ATOMIC_CONSTR)
126 : {
127 94281 : if (m_set.add (t))
128 69296 : return std::make_pair (iter, false);
129 : }
130 112703 : 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 :
137 232 : void replace (tree t)
138 : {
139 232 : m_current = replace (m_current, t).first;
140 232 : }
141 :
142 : /* Replace the current term with T1 and T2, in that order. */
143 :
144 181999 : 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 181999 : std::pair<iterator, bool> rep = replace (m_current, t1);
150 181999 : if (rep.second)
151 69790 : m_current = rep.first;
152 : else
153 112209 : ++rep.first;
154 :
155 : /* Insert the t2. Make this the current term if we erased
156 : the prior term. */
157 181999 : std::pair<iterator, bool> ins = insert (rep.first, t2);
158 181999 : if (rep.second && ins.second)
159 18361 : m_current = ins.first;
160 181999 : }
161 :
162 : /* Returns true if the clause contains the term T. */
163 :
164 65951 : bool contains (tree t)
165 : {
166 65951 : gcc_assert (TREE_CODE (t) == ATOMIC_CONSTR);
167 65951 : return m_set.contains (t);
168 : }
169 :
170 :
171 : /* Returns an iterator to the first clause in the formula. */
172 :
173 0 : iterator begin ()
174 : {
175 0 : return m_terms.begin ();
176 : }
177 :
178 : /* Returns an iterator to the first clause in the formula. */
179 :
180 116 : const_iterator begin () const
181 : {
182 116 : return m_terms.begin ();
183 : }
184 :
185 : /* Returns an iterator past the last clause in the formula. */
186 :
187 0 : iterator end ()
188 : {
189 0 : return m_terms.end ();
190 : }
191 :
192 : /* Returns an iterator past the last clause in the formula. */
193 :
194 272564 : const_iterator end () const
195 : {
196 44454 : return m_terms.end ();
197 : }
198 :
199 : /* Returns the current iterator. */
200 :
201 226685 : const_iterator current () const
202 : {
203 116 : 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 1426 : 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 :
224 1426 : formula (tree t)
225 1426 : {
226 1426 : m_clauses.emplace_back (t);
227 1426 : m_current = m_clauses.begin ();
228 1426 : }
229 :
230 : /* Returns true when all clauses are atomic. */
231 3881 : bool done () const
232 : {
233 3881 : return m_current == end ();
234 : }
235 :
236 : /* Advance to the next term. */
237 1541 : void advance ()
238 : {
239 0 : gcc_assert (!done ());
240 1541 : ++m_current;
241 1541 : }
242 :
243 : /* Insert a copy of clause into the formula. This corresponds
244 : to a distribution of one logical operation over the other. */
245 :
246 116 : clause& branch ()
247 : {
248 0 : gcc_assert (!done ());
249 116 : return *m_clauses.insert (std::next (m_current), *m_current);
250 : }
251 :
252 : /* Returns the position of the current clause. */
253 :
254 : iterator current ()
255 : {
256 : return m_current;
257 : }
258 :
259 : /* Returns an iterator to the first clause in the formula. */
260 :
261 0 : iterator begin ()
262 : {
263 0 : return m_clauses.begin ();
264 : }
265 :
266 : /* Returns an iterator to the first clause in the formula. */
267 :
268 : const_iterator begin () const
269 : {
270 : return m_clauses.begin ();
271 : }
272 :
273 : /* Returns an iterator past the last clause in the formula. */
274 :
275 0 : iterator end ()
276 : {
277 0 : return m_clauses.end ();
278 : }
279 :
280 : /* Returns an iterator past the last clause in the formula. */
281 :
282 3881 : const_iterator end () const
283 : {
284 1657 : return m_clauses.end ();
285 : }
286 :
287 : /* Remove the specified clause from the formula. */
288 :
289 798 : void erase (iterator i)
290 : {
291 798 : gcc_assert (i != m_current);
292 798 : m_clauses.erase (i);
293 798 : }
294 :
295 : std::list<clause> m_clauses; /* The list of clauses. */
296 : iterator m_current; /* The current clause. */
297 : };
298 :
299 : void
300 0 : debug (clause& c)
301 : {
302 0 : for (clause::iterator i = c.begin(); i != c.end(); ++i)
303 0 : verbatim (" # %E", *i);
304 0 : }
305 :
306 : void
307 0 : debug (formula& f)
308 : {
309 0 : for (formula::iterator i = f.begin(); i != f.end(); ++i)
310 : {
311 : /* Format punctuators via %s to avoid -Wformat-diag. */
312 0 : verbatim ("%s", "(((");
313 0 : debug (*i);
314 0 : verbatim ("%s", ")))");
315 : }
316 0 : }
317 :
318 : /* The logical rules used to analyze a logical formula. The
319 : "left" and "right" refer to the position of formula in a
320 : sequent (as in sequent calculus). */
321 :
322 : enum rules
323 : {
324 : left, right
325 : };
326 :
327 : /* Distribution counting. */
328 :
329 : static inline bool
330 1092783 : disjunction_p (tree t)
331 : {
332 1092783 : return TREE_CODE (t) == DISJ_CONSTR;
333 : }
334 :
335 : static inline bool
336 : conjunction_p (tree t)
337 : {
338 : return TREE_CODE (t) == CONJ_CONSTR;
339 : }
340 :
341 : static inline bool
342 731374 : atomic_p (tree t)
343 : {
344 731374 : return TREE_CODE (t) == ATOMIC_CONSTR;
345 : }
346 :
347 : /* Recursively count the number of clauses produced when converting T
348 : to DNF. Returns a pair containing the number of clauses and a bool
349 : value signifying that the tree would be rewritten as a result of
350 : distributing. In general, a conjunction for which this flag is set
351 : is considered a disjunction for the purpose of counting. */
352 :
353 : static std::pair<int, bool>
354 365686 : dnf_size_r (tree t)
355 : {
356 365686 : if (atomic_p (t))
357 : /* Atomic constraints produce no clauses. */
358 183556 : return std::make_pair (0, false);
359 :
360 : /* For compound constraints, recursively count clauses and unpack
361 : the results. */
362 182130 : tree lhs = TREE_OPERAND (t, 0);
363 182130 : tree rhs = TREE_OPERAND (t, 1);
364 182130 : std::pair<int, bool> p1 = dnf_size_r (lhs);
365 182130 : std::pair<int, bool> p2 = dnf_size_r (rhs);
366 182130 : int n1 = p1.first, n2 = p2.first;
367 182130 : bool d1 = p1.second, d2 = p2.second;
368 :
369 182130 : if (disjunction_p (t))
370 : {
371 : /* Matches constraints of the form P \/ Q. Disjunctions contribute
372 : linearly to the number of constraints. When both P and Q are
373 : disjunctions, clauses are added. When only one of P and Q
374 : is a disjunction, an additional clause is produced. When neither
375 : P nor Q are disjunctions, two clauses are produced. */
376 116 : if (disjunction_p (lhs))
377 : {
378 0 : if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
379 : /* Both P and Q are disjunctions. */
380 0 : return std::make_pair (n1 + n2, d1 | d2);
381 : else
382 : /* Only LHS is a disjunction. */
383 0 : return std::make_pair (1 + n1 + n2, d1 | d2);
384 : gcc_unreachable ();
385 : }
386 116 : if (conjunction_p (lhs))
387 : {
388 116 : if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
389 : /* Both P and Q are disjunctions. */
390 0 : return std::make_pair (n1 + n2, d1 | d2);
391 116 : if (disjunction_p (rhs)
392 116 : || (conjunction_p (rhs) && d1 != d2)
393 232 : || (atomic_p (rhs) && d1))
394 : /* Either LHS or RHS is a disjunction. */
395 0 : return std::make_pair (1 + n1 + n2, d1 | d2);
396 : else
397 : /* Neither LHS nor RHS is a disjunction. */
398 116 : return std::make_pair (2, false);
399 : }
400 0 : if (atomic_p (lhs))
401 : {
402 0 : if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
403 : /* Only RHS is a disjunction. */
404 0 : return std::make_pair (1 + n1 + n2, d1 | d2);
405 : else
406 : /* Neither LHS nor RHS is a disjunction. */
407 0 : return std::make_pair (2, false);
408 : }
409 : }
410 : else /* conjunction_p (t) */
411 : {
412 : /* Matches constraints of the form P /\ Q, possibly resulting
413 : in the distribution of one side over the other. When both
414 : P and Q are disjunctions, the number of clauses are multiplied.
415 : When only one of P and Q is a disjunction, the number of
416 : clauses are added. Otherwise, neither side is a disjunction and
417 : no clauses are created. */
418 182014 : if (disjunction_p (lhs))
419 : {
420 0 : if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
421 : /* Both P and Q are disjunctions. */
422 0 : return std::make_pair (n1 * n2, true);
423 : else
424 : /* Only LHS is a disjunction. */
425 0 : return std::make_pair (n1 + n2, true);
426 : gcc_unreachable ();
427 : }
428 182014 : if (conjunction_p (lhs))
429 : {
430 93150 : if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
431 : /* Both P and Q are disjunctions. */
432 0 : return std::make_pair (n1 * n2, true);
433 93150 : if (disjunction_p (rhs)
434 93035 : || (conjunction_p (rhs) && d1 != d2)
435 186185 : || (atomic_p (rhs) && d1))
436 : /* Either LHS or RHS is a disjunction. */
437 115 : return std::make_pair (n1 + n2, true);
438 : else
439 : /* Neither LHS nor RHS is a disjunction. */
440 93035 : return std::make_pair (0, false);
441 : }
442 88864 : if (atomic_p (lhs))
443 : {
444 88864 : if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
445 : /* Only RHS is a disjunction. */
446 0 : return std::make_pair (n1 + n2, true);
447 : else
448 : /* Neither LHS nor RHS is a disjunction. */
449 88864 : return std::make_pair (0, false);
450 : }
451 : }
452 0 : gcc_unreachable ();
453 : }
454 :
455 : /* Recursively count the number of clauses produced when converting T
456 : to CNF. Returns a pair containing the number of clauses and a bool
457 : value signifying that the tree would be rewritten as a result of
458 : distributing. In general, a disjunction for which this flag is set
459 : is considered a conjunction for the purpose of counting. */
460 :
461 : static std::pair<int, bool>
462 365688 : cnf_size_r (tree t)
463 : {
464 365688 : if (atomic_p (t))
465 : /* Atomic constraints produce no clauses. */
466 183557 : return std::make_pair (0, false);
467 :
468 : /* For compound constraints, recursively count clauses and unpack
469 : the results. */
470 182131 : tree lhs = TREE_OPERAND (t, 0);
471 182131 : tree rhs = TREE_OPERAND (t, 1);
472 182131 : std::pair<int, bool> p1 = cnf_size_r (lhs);
473 182131 : std::pair<int, bool> p2 = cnf_size_r (rhs);
474 182131 : int n1 = p1.first, n2 = p2.first;
475 182131 : bool d1 = p1.second, d2 = p2.second;
476 :
477 182131 : if (disjunction_p (t))
478 : {
479 : /* Matches constraints of the form P \/ Q, possibly resulting
480 : in the distribution of one side over the other. When both
481 : P and Q are conjunctions, the number of clauses are multiplied.
482 : When only one of P and Q is a conjunction, the number of
483 : clauses are added. Otherwise, neither side is a conjunction and
484 : no clauses are created. */
485 116 : if (disjunction_p (lhs))
486 : {
487 0 : if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
488 : /* Both P and Q are conjunctions. */
489 0 : return std::make_pair (n1 * n2, true);
490 0 : if ((disjunction_p (rhs) && d1 != d2)
491 0 : || conjunction_p (rhs)
492 0 : || (atomic_p (rhs) && d1))
493 : /* Either LHS or RHS is a conjunction. */
494 0 : return std::make_pair (n1 + n2, true);
495 : else
496 : /* Neither LHS nor RHS is a conjunction. */
497 0 : return std::make_pair (0, false);
498 : }
499 116 : if (conjunction_p (lhs))
500 : {
501 116 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
502 : /* Both LHS and RHS are conjunctions. */
503 116 : return std::make_pair (n1 * n2, true);
504 : else
505 : /* Only LHS is a conjunction. */
506 0 : return std::make_pair (n1 + n2, true);
507 : }
508 0 : if (atomic_p (lhs))
509 : {
510 0 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
511 : /* Only RHS is a disjunction. */
512 0 : return std::make_pair (n1 + n2, true);
513 : else
514 : /* Neither LHS nor RHS is a disjunction. */
515 0 : return std::make_pair (0, false);
516 : }
517 : }
518 : else /* conjunction_p (t) */
519 : {
520 : /* Matches constraints of the form P /\ Q. Conjunctions contribute
521 : linearly to the number of constraints. When both P and Q are
522 : conjunctions, clauses are added. When only one of P and Q
523 : is a conjunction, an additional clause is produced. When neither
524 : P nor Q are conjunctions, two clauses are produced. */
525 182015 : if (disjunction_p (lhs))
526 : {
527 0 : if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
528 : /* Both P and Q are conjunctions. */
529 0 : return std::make_pair (n1 + n2, d1 | d2);
530 0 : if ((disjunction_p (rhs) && d1 != d2)
531 0 : || conjunction_p (rhs)
532 0 : || (atomic_p (rhs) && d1))
533 : /* Either LHS or RHS is a conjunction. */
534 0 : return std::make_pair (1 + n1 + n2, d1 | d2);
535 : else
536 : /* Neither LHS nor RHS is a conjunction. */
537 0 : return std::make_pair (2, false);
538 : }
539 182015 : if (conjunction_p (lhs))
540 : {
541 93150 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
542 : /* Both LHS and RHS are conjunctions. */
543 69242 : return std::make_pair (n1 + n2, d1 | d2);
544 : else
545 : /* Only LHS is a conjunction. */
546 23908 : return std::make_pair (1 + n1 + n2, d1 | d2);
547 : }
548 88865 : if (atomic_p (lhs))
549 : {
550 88865 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
551 : /* Only RHS is a disjunction. */
552 18483 : return std::make_pair (1 + n1 + n2, d1 | d2);
553 : else
554 : /* Neither LHS nor RHS is a disjunction. */
555 70382 : return std::make_pair (2, false);
556 : }
557 : }
558 0 : gcc_unreachable ();
559 : }
560 :
561 : /* Count the number conjunctive clauses that would be created
562 : when rewriting T to DNF. */
563 :
564 : static int
565 1426 : dnf_size (tree t)
566 : {
567 0 : std::pair<int, bool> result = dnf_size_r (t);
568 1426 : return result.first == 0 ? 1 : result.first;
569 : }
570 :
571 :
572 : /* Count the number disjunctive clauses that would be created
573 : when rewriting T to CNF. */
574 :
575 : static int
576 1426 : cnf_size (tree t)
577 : {
578 0 : std::pair<int, bool> result = cnf_size_r (t);
579 1426 : return result.first == 0 ? 1 : result.first;
580 : }
581 :
582 :
583 : /* A left-conjunction is replaced by its operands. */
584 :
585 : void
586 181999 : replace_term (clause& c, tree t)
587 : {
588 181999 : tree t1 = TREE_OPERAND (t, 0);
589 181999 : tree t2 = TREE_OPERAND (t, 1);
590 181999 : return c.replace (t1, t2);
591 : }
592 :
593 : /* Create a new clause in the formula by copying the current
594 : clause. In the current clause, the term at CI is replaced
595 : by the first operand, and in the new clause, it is replaced
596 : by the second. */
597 :
598 : void
599 116 : branch_clause (formula& f, clause& c1, tree t)
600 : {
601 116 : tree t1 = TREE_OPERAND (t, 0);
602 116 : tree t2 = TREE_OPERAND (t, 1);
603 116 : clause& c2 = f.branch ();
604 116 : c1.replace (t1);
605 116 : c2.replace (t2);
606 116 : }
607 :
608 : /* Decompose t1 /\ t2 according to the rules R. */
609 :
610 : inline void
611 181999 : decompose_conjuntion (formula& f, clause& c, tree t, rules r)
612 : {
613 181999 : if (r == left)
614 181999 : replace_term (c, t);
615 : else
616 0 : branch_clause (f, c, t);
617 181999 : }
618 :
619 : /* Decompose t1 \/ t2 according to the rules R. */
620 :
621 : inline void
622 116 : decompose_disjunction (formula& f, clause& c, tree t, rules r)
623 : {
624 116 : if (r == right)
625 0 : replace_term (c, t);
626 : else
627 116 : branch_clause (f, c, t);
628 116 : }
629 :
630 : /* An atomic constraint is already decomposed. */
631 : inline void
632 44454 : decompose_atom (clause& c)
633 : {
634 44454 : c.advance ();
635 44454 : }
636 :
637 : /* Decompose a term of clause C (in formula F) according to the
638 : logical rules R. */
639 :
640 : void
641 226569 : decompose_term (formula& f, clause& c, tree t, rules r)
642 : {
643 226569 : switch (TREE_CODE (t))
644 : {
645 181999 : case CONJ_CONSTR:
646 181999 : return decompose_conjuntion (f, c, t, r);
647 116 : case DISJ_CONSTR:
648 116 : return decompose_disjunction (f, c, t, r);
649 44454 : default:
650 44454 : return decompose_atom (c);
651 : }
652 : }
653 :
654 : /* Decompose C (in F) using the logical rules R until it
655 : is comprised of only atomic constraints. */
656 :
657 : void
658 1541 : decompose_clause (formula& f, clause& c, rules r)
659 : {
660 228110 : while (!c.done ())
661 226569 : decompose_term (f, c, *c.current (), r);
662 1541 : f.advance ();
663 1541 : }
664 :
665 : static bool derive_proof (clause&, tree, rules);
666 :
667 : /* Derive a proof of both operands of T. */
668 :
669 : static bool
670 67038 : derive_proof_for_both_operands (clause& c, tree t, rules r)
671 : {
672 67038 : if (!derive_proof (c, TREE_OPERAND (t, 0), r))
673 : return false;
674 64294 : return derive_proof (c, TREE_OPERAND (t, 1), r);
675 : }
676 :
677 : /* Derive a proof of either operand of T. */
678 :
679 : static bool
680 116 : derive_proof_for_either_operand (clause& c, tree t, rules r)
681 : {
682 116 : if (derive_proof (c, TREE_OPERAND (t, 0), r))
683 : return true;
684 116 : return derive_proof (c, TREE_OPERAND (t, 1), r);
685 : }
686 :
687 : /* Derive a proof of the atomic constraint T in clause C. */
688 :
689 : static bool
690 65951 : derive_atomic_proof (clause& c, tree t)
691 : {
692 0 : return c.contains (t);
693 : }
694 :
695 : /* Derive a proof of T from the terms in C. */
696 :
697 : static bool
698 133105 : derive_proof (clause& c, tree t, rules r)
699 : {
700 133105 : switch (TREE_CODE (t))
701 : {
702 67038 : case CONJ_CONSTR:
703 67038 : if (r == left)
704 67038 : return derive_proof_for_both_operands (c, t, r);
705 : else
706 0 : return derive_proof_for_either_operand (c, t, r);
707 116 : case DISJ_CONSTR:
708 116 : if (r == left)
709 116 : return derive_proof_for_either_operand (c, t, r);
710 : else
711 0 : return derive_proof_for_both_operands (c, t, r);
712 65951 : default:
713 65951 : return derive_atomic_proof (c, t);
714 : }
715 : }
716 :
717 : /* Key/value pair for caching subsumption results. This associates a pair of
718 : constraints with a boolean value indicating the result. */
719 :
720 : struct GTY((for_user)) subsumption_entry
721 : {
722 : tree lhs;
723 : tree rhs;
724 : bool result;
725 : };
726 :
727 : /* Hashing function and equality for constraint entries. */
728 :
729 : struct subsumption_hasher : ggc_ptr_hash<subsumption_entry>
730 : {
731 9392 : static hashval_t hash (subsumption_entry *e)
732 : {
733 9392 : hashval_t val = 0;
734 9392 : val = iterative_hash_constraint (e->lhs, val);
735 9392 : val = iterative_hash_constraint (e->rhs, val);
736 9392 : return val;
737 : }
738 :
739 6721 : static bool equal (subsumption_entry *e1, subsumption_entry *e2)
740 : {
741 6721 : if (!constraints_equivalent_p (e1->lhs, e2->lhs))
742 : return false;
743 2125 : if (!constraints_equivalent_p (e1->rhs, e2->rhs))
744 : return false;
745 : return true;
746 : }
747 : };
748 :
749 : /* Caches the results of subsumes_non_null(t1, t1). */
750 :
751 : static GTY ((deletable)) hash_table<subsumption_hasher> *subsumption_cache;
752 :
753 : /* Search for a previously cached subsumption result. */
754 :
755 : static bool*
756 3405 : lookup_subsumption (tree t1, tree t2)
757 : {
758 3405 : if (!subsumption_cache)
759 : return NULL;
760 3046 : subsumption_entry elt = { t1, t2, false };
761 3046 : subsumption_entry* found = subsumption_cache->find (&elt);
762 3046 : if (found)
763 1979 : return &found->result;
764 : else
765 : return 0;
766 : }
767 :
768 : /* Save a subsumption result. */
769 :
770 : static bool
771 1426 : save_subsumption (tree t1, tree t2, bool result)
772 : {
773 1426 : if (!subsumption_cache)
774 359 : subsumption_cache = hash_table<subsumption_hasher>::create_ggc(31);
775 1426 : subsumption_entry elt = {t1, t2, result};
776 1426 : subsumption_entry** slot = subsumption_cache->find_slot (&elt, INSERT);
777 1426 : subsumption_entry* entry = ggc_alloc<subsumption_entry> ();
778 1426 : *entry = elt;
779 1426 : *slot = entry;
780 1426 : return result;
781 : }
782 :
783 :
784 : /* Returns true if the LEFT constraint subsume the RIGHT constraints.
785 : This is done by deriving a proof of the conclusions on the RIGHT
786 : from the assumptions on the LEFT assumptions. */
787 :
788 : static bool
789 3405 : subsumes_constraints_nonnull (tree lhs, tree rhs)
790 : {
791 3405 : auto_timevar time (TV_CONSTRAINT_SUB);
792 :
793 3405 : if (bool *b = lookup_subsumption(lhs, rhs))
794 1979 : return *b;
795 :
796 1426 : tree x, y;
797 1426 : rules r;
798 4278 : if (dnf_size (lhs) <= cnf_size (rhs))
799 : /* When LHS looks simpler than RHS, we'll determine subsumption by
800 : decomposing LHS into its disjunctive normal form and checking that
801 : each (conjunctive) clause in the decomposed LHS implies RHS. */
802 : x = lhs, y = rhs, r = left;
803 : else
804 : /* Otherwise, we'll determine subsumption by decomposing RHS into its
805 : conjunctive normal form and checking that each (disjunctive) clause
806 : in the decomposed RHS implies LHS. */
807 0 : x = rhs, y = lhs, r = right;
808 :
809 : /* Decompose X into a list of sequents according to R, and recursively
810 : check for implication of Y. */
811 1426 : bool result = true;
812 1426 : formula f (x);
813 3650 : while (!f.done ())
814 : {
815 1541 : auto i = f.current ();
816 1541 : decompose_clause (f, *i, r);
817 1541 : if (!derive_proof (*i, y, r))
818 : {
819 : result = false;
820 1426 : break;
821 : }
822 798 : f.erase (i);
823 : }
824 :
825 1426 : return save_subsumption (lhs, rhs, result);
826 3405 : }
827 :
828 : /* Returns true if the LEFT constraints subsume the RIGHT
829 : constraints. */
830 :
831 : bool
832 246953 : subsumes (tree lhs, tree rhs)
833 : {
834 246953 : if (lhs == rhs)
835 : return true;
836 105619 : if (!lhs || lhs == error_mark_node)
837 : return false;
838 54512 : if (!rhs || rhs == error_mark_node)
839 : return true;
840 3405 : return subsumes_constraints_nonnull (lhs, rhs);
841 : }
842 :
843 : #include "gt-cp-logic.h"
|
