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