Branch data Line data Source code
1 : : /* Derivation and subsumption rules for constraints.
2 : : Copyright (C) 2013-2025 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 : 31352 : 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 : 25071 : clause (tree t)
64 : 25071 : {
65 : 25071 : m_terms.push_back (t);
66 : 25071 : if (TREE_CODE (t) == ATOMIC_CONSTR)
67 : 6564 : m_set.add (t);
68 : :
69 : 25071 : m_current = m_terms.begin ();
70 : 25071 : }
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 : 6281 : clause (clause const& c)
77 : 6281 : : m_terms (c.m_terms), m_set (c.m_set), m_current (m_terms.begin ())
78 : : {
79 : 6281 : std::advance (m_current, std::distance (c.begin (), c.current ()));
80 : 6281 : }
81 : :
82 : : /* Returns true when all terms are atoms. */
83 : :
84 : 4672529 : bool done () const
85 : : {
86 : 4672529 : return m_current == end ();
87 : : }
88 : :
89 : : /* Advance to the next term. */
90 : :
91 : 878711 : void advance ()
92 : : {
93 : 0 : gcc_assert (!done ());
94 : 878711 : ++m_current;
95 : 878711 : }
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 : 2890038 : std::pair<iterator, bool> replace (iterator iter, tree t)
105 : : {
106 : 2890038 : gcc_assert (TREE_CODE (*iter) != ATOMIC_CONSTR);
107 : 2890038 : if (TREE_CODE (t) == ATOMIC_CONSTR)
108 : : {
109 : 1417944 : if (m_set.add (t))
110 : 1028384 : return std::make_pair (m_terms.erase (iter), true);
111 : : }
112 : 1861654 : *iter = t;
113 : 1861654 : 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 : 2877476 : std::pair<iterator, bool> insert (iterator iter, tree t)
123 : : {
124 : 2877476 : if (TREE_CODE (t) == ATOMIC_CONSTR)
125 : : {
126 : 1484318 : if (m_set.add (t))
127 : 1001731 : return std::make_pair (iter, false);
128 : : }
129 : 1875745 : 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 : 12562 : void replace (tree t)
137 : : {
138 : 12562 : m_current = replace (m_current, t).first;
139 : 12562 : }
140 : :
141 : : /* Replace the current term with T1 and T2, in that order. */
142 : :
143 : 2877476 : 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 : 2877476 : std::pair<iterator, bool> rep = replace (m_current, t1);
149 : 2877476 : if (rep.second)
150 : 1028384 : m_current = rep.first;
151 : : else
152 : 1849092 : ++rep.first;
153 : :
154 : : /* Insert the t2. Make this the current term if we erased
155 : : the prior term. */
156 : 2877476 : std::pair<iterator, bool> ins = insert (rep.first, t2);
157 : 2877476 : if (rep.second && ins.second)
158 : 280574 : m_current = ins.first;
159 : 2877476 : }
160 : :
161 : : /* Returns true if the clause contains the term T. */
162 : :
163 : 717666 : bool contains (tree t)
164 : : {
165 : 717666 : gcc_assert (TREE_CODE (t) == ATOMIC_CONSTR);
166 : 717666 : 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 : 6281 : const_iterator begin () const
180 : : {
181 : 6281 : 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 : 4672529 : const_iterator end () const
194 : : {
195 : 878711 : return m_terms.end ();
196 : : }
197 : :
198 : : /* Returns the current iterator. */
199 : :
200 : 3768749 : const_iterator current () const
201 : : {
202 : 6281 : 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 : 50142 : 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 : 25071 : formula (tree t)
224 : 25071 : {
225 : 25071 : m_clauses.emplace_back (t);
226 : 25071 : m_current = m_clauses.begin ();
227 : 25071 : }
228 : :
229 : : /* Returns true when all clauses are atomic. */
230 : 81426 : bool done () const
231 : : {
232 : 81426 : return m_current == end ();
233 : : }
234 : :
235 : : /* Advance to the next term. */
236 : 31350 : void advance ()
237 : : {
238 : 0 : gcc_assert (!done ());
239 : 31350 : ++m_current;
240 : 31350 : }
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 : 6281 : clause& branch ()
246 : : {
247 : 0 : gcc_assert (!done ());
248 : 12562 : 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 : 81426 : const_iterator end () const
282 : : {
283 : 37631 : return m_clauses.end ();
284 : : }
285 : :
286 : : /* Remove the specified clause from the formula. */
287 : :
288 : 18724 : void erase (iterator i)
289 : : {
290 : 18724 : gcc_assert (i != m_current);
291 : 18724 : m_clauses.erase (i);
292 : 18724 : }
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 : 17302758 : disjunction_p (tree t)
330 : : {
331 : 17302758 : 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 : 11585314 : atomic_p (tree t)
342 : : {
343 : 11585314 : 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 : 5792645 : dnf_size_r (tree t)
354 : : {
355 : 5792645 : if (atomic_p (t))
356 : : /* Atomic constraints produce no clauses. */
357 : 2908858 : return std::make_pair (0, false);
358 : :
359 : : /* For compound constraints, recursively count clauses and unpack
360 : : the results. */
361 : 2883787 : tree lhs = TREE_OPERAND (t, 0);
362 : 2883787 : tree rhs = TREE_OPERAND (t, 1);
363 : 2883787 : auto p1 = dnf_size_r (lhs);
364 : 2883787 : auto p2 = dnf_size_r (rhs);
365 : 2883787 : HOST_WIDE_INT n1 = p1.first, n2 = p2.first;
366 : 2883787 : bool d1 = p1.second, d2 = p2.second;
367 : :
368 : 2883787 : 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 : 6281 : 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 : 6281 : if (conjunction_p (lhs))
387 : : {
388 : 6281 : if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
389 : : /* Both P and Q are disjunctions. */
390 : 2093 : return std::make_pair (add_sat_hwi (n1, n2), d1 | d2);
391 : 4188 : if (disjunction_p (rhs)
392 : 4188 : || (conjunction_p (rhs) && d1 != d2)
393 : 8376 : || (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 : 4188 : return std::make_pair (2, false);
400 : : }
401 : 0 : if (atomic_p (lhs))
402 : : {
403 : 0 : 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 : 0 : 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 : 2877506 : 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 : 2877506 : if (conjunction_p (lhs))
431 : : {
432 : 1461639 : 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 : 1461639 : if (disjunction_p (rhs)
436 : 1457453 : || (conjunction_p (rhs) && d1 != d2)
437 : 2919092 : || (atomic_p (rhs) && d1))
438 : : /* Either LHS or RHS is a disjunction. */
439 : 4186 : return std::make_pair (add_sat_hwi (n1, n2), true);
440 : : else
441 : : /* Neither LHS nor RHS is a disjunction. */
442 : 1457453 : return std::make_pair (0, false);
443 : : }
444 : 1415867 : if (atomic_p (lhs))
445 : : {
446 : 1415867 : if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
447 : : /* Only RHS is a disjunction. */
448 : 2093 : return std::make_pair (n1 + n2, true);
449 : : else
450 : : /* Neither LHS nor RHS is a disjunction. */
451 : 1413774 : 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 : 5792669 : cnf_size_r (tree t)
465 : : {
466 : 5792669 : if (atomic_p (t))
467 : : /* Atomic constraints produce no clauses. */
468 : 2908870 : return std::make_pair (0, false);
469 : :
470 : : /* For compound constraints, recursively count clauses and unpack
471 : : the results. */
472 : 2883799 : tree lhs = TREE_OPERAND (t, 0);
473 : 2883799 : tree rhs = TREE_OPERAND (t, 1);
474 : 2883799 : auto p1 = cnf_size_r (lhs);
475 : 2883799 : auto p2 = cnf_size_r (rhs);
476 : 2883799 : HOST_WIDE_INT n1 = p1.first, n2 = p2.first;
477 : 2883799 : bool d1 = p1.second, d2 = p2.second;
478 : :
479 : 2883799 : 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 : 6290 : 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 : 6290 : if (conjunction_p (lhs))
502 : : {
503 : 6281 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
504 : : /* Both LHS and RHS are conjunctions. */
505 : 4188 : return std::make_pair (mul_sat_hwi (n1, n2), true);
506 : : else
507 : : /* Only LHS is a conjunction. */
508 : 2093 : return std::make_pair (add_sat_hwi (n1, n2), true);
509 : : }
510 : 9 : if (atomic_p (lhs))
511 : : {
512 : 9 : 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 : 9 : 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 : 2877509 : 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 : 2877509 : if (conjunction_p (lhs))
543 : : {
544 : 1461639 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
545 : : /* Both LHS and RHS are conjunctions. */
546 : 1091767 : return std::make_pair (add_sat_hwi (n1, n2), d1 | d2);
547 : : else
548 : : /* Only LHS is a conjunction. */
549 : 369872 : return std::make_pair (add_sat_hwi (1, add_sat_hwi (n1, n2)),
550 : 739744 : d1 | d2);
551 : : }
552 : 1415870 : if (atomic_p (lhs))
553 : : {
554 : 1415870 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
555 : : /* Only RHS is a disjunction. */
556 : 301405 : return std::make_pair (add_sat_hwi (1, add_sat_hwi (n1, n2)),
557 : 602810 : d1 | d2);
558 : : else
559 : : /* Neither LHS nor RHS is a disjunction. */
560 : 1114465 : 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 : 25071 : dnf_size (tree t)
571 : : {
572 : 0 : auto result = dnf_size_r (t);
573 : 25071 : 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 : 25071 : cnf_size (tree t)
582 : : {
583 : 0 : auto result = cnf_size_r (t);
584 : 25071 : return result.first == 0 ? 1 : result.first;
585 : : }
586 : :
587 : :
588 : : /* A left-conjunction is replaced by its operands. */
589 : :
590 : : void
591 : 2877476 : replace_term (clause& c, tree t)
592 : : {
593 : 2877476 : tree t1 = TREE_OPERAND (t, 0);
594 : 2877476 : tree t2 = TREE_OPERAND (t, 1);
595 : 2877476 : 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 : 6281 : branch_clause (formula& f, clause& c1, tree t)
605 : : {
606 : 6281 : tree t1 = TREE_OPERAND (t, 0);
607 : 6281 : tree t2 = TREE_OPERAND (t, 1);
608 : 6281 : clause& c2 = f.branch ();
609 : 6281 : c1.replace (t1);
610 : 6281 : c2.replace (t2);
611 : 6281 : }
612 : :
613 : : /* Decompose t1 /\ t2 according to the rules R. */
614 : :
615 : : inline void
616 : 2877476 : decompose_conjuntion (formula& f, clause& c, tree t, rules r)
617 : : {
618 : 2877476 : if (r == left)
619 : 2877476 : replace_term (c, t);
620 : : else
621 : 0 : branch_clause (f, c, t);
622 : 2877476 : }
623 : :
624 : : /* Decompose t1 \/ t2 according to the rules R. */
625 : :
626 : : inline void
627 : 6281 : decompose_disjunction (formula& f, clause& c, tree t, rules r)
628 : : {
629 : 6281 : if (r == right)
630 : 0 : replace_term (c, t);
631 : : else
632 : 6281 : branch_clause (f, c, t);
633 : 6281 : }
634 : :
635 : : /* An atomic constraint is already decomposed. */
636 : : inline void
637 : 878711 : decompose_atom (clause& c)
638 : : {
639 : 878711 : c.advance ();
640 : 878711 : }
641 : :
642 : : /* Decompose a term of clause C (in formula F) according to the
643 : : logical rules R. */
644 : :
645 : : void
646 : 3762468 : decompose_term (formula& f, clause& c, tree t, rules r)
647 : : {
648 : 3762468 : switch (TREE_CODE (t))
649 : : {
650 : 2877476 : case CONJ_CONSTR:
651 : 2877476 : return decompose_conjuntion (f, c, t, r);
652 : 6281 : case DISJ_CONSTR:
653 : 6281 : return decompose_disjunction (f, c, t, r);
654 : 878711 : default:
655 : 878711 : 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 : 31350 : decompose_clause (formula& f, clause& c, rules r)
664 : : {
665 : 3793818 : while (!c.done ())
666 : 3762468 : decompose_term (f, c, *c.current (), r);
667 : 31350 : f.advance ();
668 : 31350 : }
669 : :
670 : : static bool derive_proof (clause&, tree, rules);
671 : :
672 : : /* Derive a proof of both operands of T. */
673 : :
674 : : static bool
675 : 732843 : derive_proof_for_both_operands (clause& c, tree t, rules r)
676 : : {
677 : 732843 : if (!derive_proof (c, TREE_OPERAND (t, 0), r))
678 : : return false;
679 : 683331 : 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 : 2994 : derive_proof_for_either_operand (clause& c, tree t, rules r)
686 : : {
687 : 2994 : if (derive_proof (c, TREE_OPERAND (t, 0), r))
688 : : return true;
689 : 2985 : 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 : 717666 : 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 : 1453503 : derive_proof (clause& c, tree t, rules r)
704 : : {
705 : 1453503 : switch (TREE_CODE (t))
706 : : {
707 : 732843 : case CONJ_CONSTR:
708 : 732843 : if (r == left)
709 : 732843 : return derive_proof_for_both_operands (c, t, r);
710 : : else
711 : 0 : return derive_proof_for_either_operand (c, t, r);
712 : 2994 : case DISJ_CONSTR:
713 : 2994 : if (r == left)
714 : 2994 : return derive_proof_for_either_operand (c, t, r);
715 : : else
716 : 0 : return derive_proof_for_both_operands (c, t, r);
717 : 717666 : default:
718 : 717666 : 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 : 104636 : static hashval_t hash (subsumption_entry *e)
737 : : {
738 : 104636 : hashval_t val = 0;
739 : 104636 : val = iterative_hash_constraint (e->lhs, val);
740 : 104636 : val = iterative_hash_constraint (e->rhs, val);
741 : 104636 : return val;
742 : : }
743 : :
744 : 62967 : static bool equal (subsumption_entry *e1, subsumption_entry *e2)
745 : : {
746 : 62967 : if (!constraints_equivalent_p (e1->lhs, e2->lhs))
747 : : return false;
748 : 11094 : 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 : 34487 : lookup_subsumption (tree t1, tree t2)
762 : : {
763 : 34487 : if (!subsumption_cache)
764 : : return NULL;
765 : 28540 : subsumption_entry elt = { t1, t2, false };
766 : 28540 : subsumption_entry* found = subsumption_cache->find (&elt);
767 : 28540 : if (found)
768 : 9416 : return &found->result;
769 : : else
770 : : return 0;
771 : : }
772 : :
773 : : /* Save a subsumption result. */
774 : :
775 : : static bool
776 : 25071 : save_subsumption (tree t1, tree t2, bool result)
777 : : {
778 : 25071 : if (!subsumption_cache)
779 : 5947 : subsumption_cache = hash_table<subsumption_hasher>::create_ggc (31);
780 : 25071 : subsumption_entry elt = {t1, t2, result};
781 : 25071 : subsumption_entry** slot = subsumption_cache->find_slot (&elt, INSERT);
782 : 25071 : subsumption_entry* entry = ggc_alloc<subsumption_entry> ();
783 : 25071 : *entry = elt;
784 : 25071 : *slot = entry;
785 : 25071 : 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 : 34487 : subsumes_constraints_nonnull (tree lhs, tree rhs)
795 : : {
796 : 34487 : auto_timevar time (TV_CONSTRAINT_SUB);
797 : :
798 : 34487 : if (bool *b = lookup_subsumption (lhs, rhs))
799 : 9416 : return *b;
800 : :
801 : 25071 : tree x, y;
802 : 25071 : rules r;
803 : 75213 : 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 : 25071 : bool result = true;
817 : 25071 : formula f (x);
818 : 68866 : while (!f.done ())
819 : : {
820 : 31350 : auto i = f.current ();
821 : 31350 : decompose_clause (f, *i, r);
822 : 31350 : if (!derive_proof (*i, y, r))
823 : : {
824 : : result = false;
825 : 25071 : break;
826 : : }
827 : 18724 : f.erase (i);
828 : : }
829 : :
830 : 25071 : return save_subsumption (lhs, rhs, result);
831 : 34487 : }
832 : :
833 : : /* Returns true if the LEFT constraints subsume the RIGHT
834 : : constraints. */
835 : :
836 : : bool
837 : 4865724 : subsumes (tree lhs, tree rhs)
838 : : {
839 : 4865724 : if (lhs == rhs)
840 : : return true;
841 : 619664 : if (!lhs || lhs == error_mark_node)
842 : : return false;
843 : 327067 : if (!rhs || rhs == error_mark_node)
844 : : return true;
845 : 34487 : return subsumes_constraints_nonnull (lhs, rhs);
846 : : }
847 : :
848 : : #include "gt-cp-logic.h"
|
