Branch data Line data Source code
1 : : /* Derivation and subsumption rules for constraints.
2 : : Copyright (C) 2013-2024 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 : 30102 : 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 : 24133 : clause (tree t)
64 : 24133 : {
65 : 24133 : m_terms.push_back (t);
66 : 24133 : if (TREE_CODE (t) == ATOMIC_CONSTR)
67 : 6247 : m_set.add (t);
68 : :
69 : 24133 : m_current = m_terms.begin ();
70 : 24133 : }
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 : 5969 : clause (clause const& c)
77 : 5969 : : m_terms (c.m_terms), m_set (c.m_set), m_current (m_terms.begin ())
78 : : {
79 : 5969 : std::advance (m_current, std::distance (c.begin (), c.current ()));
80 : 5969 : }
81 : :
82 : : /* Returns true when all terms are atoms. */
83 : :
84 : 4475025 : bool done () const
85 : : {
86 : 4475025 : return m_current == end ();
87 : : }
88 : :
89 : : /* Advance to the next term. */
90 : :
91 : 847371 : void advance ()
92 : : {
93 : 0 : gcc_assert (!done ());
94 : 847371 : ++m_current;
95 : 847371 : }
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 : 2756152 : std::pair<iterator, bool> replace (iterator iter, tree t)
105 : : {
106 : 2756152 : gcc_assert (TREE_CODE (*iter) != ATOMIC_CONSTR);
107 : 2756152 : if (TREE_CODE (t) == ATOMIC_CONSTR)
108 : : {
109 : 1352799 : if (m_set.add (t))
110 : 977073 : return std::make_pair (m_terms.erase (iter), true);
111 : : }
112 : 1779079 : *iter = t;
113 : 1779079 : 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 : 2744214 : std::pair<iterator, bool> insert (iterator iter, tree t)
123 : : {
124 : 2744214 : if (TREE_CODE (t) == ATOMIC_CONSTR)
125 : : {
126 : 1415268 : if (m_set.add (t))
127 : 949870 : return std::make_pair (iter, false);
128 : : }
129 : 1794344 : 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 : 11938 : void replace (tree t)
137 : : {
138 : 11938 : m_current = replace (m_current, t).first;
139 : 11938 : }
140 : :
141 : : /* Replace the current term with T1 and T2, in that order. */
142 : :
143 : 2744214 : 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 : 2744214 : std::pair<iterator, bool> rep = replace (m_current, t1);
149 : 2744214 : if (rep.second)
150 : 977073 : m_current = rep.first;
151 : : else
152 : 1767141 : ++rep.first;
153 : :
154 : : /* Insert the t2. Make this the current term if we erased
155 : : the prior term. */
156 : 2744214 : std::pair<iterator, bool> ins = insert (rep.first, t2);
157 : 2744214 : if (rep.second && ins.second)
158 : 267893 : m_current = ins.first;
159 : 2744214 : }
160 : :
161 : : /* Returns true if the clause contains the term T. */
162 : :
163 : 699231 : bool contains (tree t)
164 : : {
165 : 699231 : gcc_assert (TREE_CODE (t) == ATOMIC_CONSTR);
166 : 699231 : 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 : 5969 : const_iterator begin () const
180 : : {
181 : 5969 : 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 : 4475025 : const_iterator end () const
194 : : {
195 : 847371 : return m_terms.end ();
196 : : }
197 : :
198 : : /* Returns the current iterator. */
199 : :
200 : 3603523 : const_iterator current () const
201 : : {
202 : 5969 : return m_current;
203 : : }
204 : :
205 : : std::list<tree> m_terms; /* The list of terms. */
206 : : hash_set<tree, false, atom_hasher> 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 : 48266 : 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 : 24133 : formula (tree t)
224 : 24133 : {
225 : 24133 : m_clauses.emplace_back (t);
226 : 24133 : m_current = m_clauses.begin ();
227 : 24133 : }
228 : :
229 : : /* Returns true when all clauses are atomic. */
230 : 78145 : bool done () const
231 : : {
232 : 78145 : return m_current == end ();
233 : : }
234 : :
235 : : /* Advance to the next term. */
236 : 30100 : void advance ()
237 : : {
238 : 0 : gcc_assert (!done ());
239 : 30100 : ++m_current;
240 : 30100 : }
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 : 5969 : clause& branch ()
246 : : {
247 : 0 : gcc_assert (!done ());
248 : 11938 : 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 : 78145 : const_iterator end () const
282 : : {
283 : 36069 : return m_clauses.end ();
284 : : }
285 : :
286 : : /* Remove the specified clause from the formula. */
287 : :
288 : 17943 : void erase (iterator i)
289 : : {
290 : 17943 : gcc_assert (i != m_current);
291 : 17943 : m_clauses.erase (i);
292 : 17943 : }
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 : 16501314 : disjunction_p (tree t)
330 : : {
331 : 16501314 : 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 : 11049142 : atomic_p (tree t)
342 : : {
343 : 11049142 : 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<int, bool>
353 : 5524559 : dnf_size_r (tree t)
354 : : {
355 : 5524559 : if (atomic_p (t))
356 : : /* Atomic constraints produce no clauses. */
357 : 2774346 : return std::make_pair (0, false);
358 : :
359 : : /* For compound constraints, recursively count clauses and unpack
360 : : the results. */
361 : 2750213 : tree lhs = TREE_OPERAND (t, 0);
362 : 2750213 : tree rhs = TREE_OPERAND (t, 1);
363 : 2750213 : std::pair<int, bool> p1 = dnf_size_r (lhs);
364 : 2750213 : std::pair<int, bool> p2 = dnf_size_r (rhs);
365 : 2750213 : int n1 = p1.first, n2 = p2.first;
366 : 2750213 : bool d1 = p1.second, d2 = p2.second;
367 : :
368 : 2750213 : 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 : 5969 : 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 (n1 + n2, d1 | d2);
380 : : else
381 : : /* Only LHS is a disjunction. */
382 : 0 : return std::make_pair (1 + n1 + n2, d1 | d2);
383 : : gcc_unreachable ();
384 : : }
385 : 5969 : if (conjunction_p (lhs))
386 : : {
387 : 5969 : if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
388 : : /* Both P and Q are disjunctions. */
389 : 1989 : return std::make_pair (n1 + n2, d1 | d2);
390 : 3980 : if (disjunction_p (rhs)
391 : 3980 : || (conjunction_p (rhs) && d1 != d2)
392 : 7960 : || (atomic_p (rhs) && d1))
393 : : /* Either LHS or RHS is a disjunction. */
394 : 0 : return std::make_pair (1 + n1 + n2, d1 | d2);
395 : : else
396 : : /* Neither LHS nor RHS is a disjunction. */
397 : 3980 : return std::make_pair (2, false);
398 : : }
399 : 0 : if (atomic_p (lhs))
400 : : {
401 : 0 : if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
402 : : /* Only RHS is a disjunction. */
403 : 0 : return std::make_pair (1 + n1 + n2, d1 | d2);
404 : : else
405 : : /* Neither LHS nor RHS is a disjunction. */
406 : 0 : return std::make_pair (2, false);
407 : : }
408 : : }
409 : : else /* conjunction_p (t) */
410 : : {
411 : : /* Matches constraints of the form P /\ Q, possibly resulting
412 : : in the distribution of one side over the other. When both
413 : : P and Q are disjunctions, the number of clauses are multiplied.
414 : : When only one of P and Q is a disjunction, the number of
415 : : clauses are added. Otherwise, neither side is a disjunction and
416 : : no clauses are created. */
417 : 2744244 : if (disjunction_p (lhs))
418 : : {
419 : 0 : if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
420 : : /* Both P and Q are disjunctions. */
421 : 0 : return std::make_pair (n1 * n2, true);
422 : : else
423 : : /* Only LHS is a disjunction. */
424 : 0 : return std::make_pair (n1 + n2, true);
425 : : gcc_unreachable ();
426 : : }
427 : 2744244 : if (conjunction_p (lhs))
428 : : {
429 : 1393418 : if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
430 : : /* Both P and Q are disjunctions. */
431 : 0 : return std::make_pair (n1 * n2, true);
432 : 1393418 : if (disjunction_p (rhs)
433 : 1389440 : || (conjunction_p (rhs) && d1 != d2)
434 : 2782858 : || (atomic_p (rhs) && d1))
435 : : /* Either LHS or RHS is a disjunction. */
436 : 3978 : return std::make_pair (n1 + n2, true);
437 : : else
438 : : /* Neither LHS nor RHS is a disjunction. */
439 : 1389440 : return std::make_pair (0, false);
440 : : }
441 : 1350826 : if (atomic_p (lhs))
442 : : {
443 : 1350826 : if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
444 : : /* Only RHS is a disjunction. */
445 : 1989 : return std::make_pair (n1 + n2, true);
446 : : else
447 : : /* Neither LHS nor RHS is a disjunction. */
448 : 1348837 : return std::make_pair (0, false);
449 : : }
450 : : }
451 : 0 : gcc_unreachable ();
452 : : }
453 : :
454 : : /* Recursively count the number of clauses produced when converting T
455 : : to CNF. Returns a pair containing the number of clauses and a bool
456 : : value signifying that the tree would be rewritten as a result of
457 : : distributing. In general, a disjunction for which this flag is set
458 : : is considered a conjunction for the purpose of counting. */
459 : :
460 : : static std::pair<int, bool>
461 : 5524583 : cnf_size_r (tree t)
462 : : {
463 : 5524583 : if (atomic_p (t))
464 : : /* Atomic constraints produce no clauses. */
465 : 2774358 : return std::make_pair (0, false);
466 : :
467 : : /* For compound constraints, recursively count clauses and unpack
468 : : the results. */
469 : 2750225 : tree lhs = TREE_OPERAND (t, 0);
470 : 2750225 : tree rhs = TREE_OPERAND (t, 1);
471 : 2750225 : std::pair<int, bool> p1 = cnf_size_r (lhs);
472 : 2750225 : std::pair<int, bool> p2 = cnf_size_r (rhs);
473 : 2750225 : int n1 = p1.first, n2 = p2.first;
474 : 2750225 : bool d1 = p1.second, d2 = p2.second;
475 : :
476 : 2750225 : if (disjunction_p (t))
477 : : {
478 : : /* Matches constraints of the form P \/ Q, possibly resulting
479 : : in the distribution of one side over the other. When both
480 : : P and Q are conjunctions, the number of clauses are multiplied.
481 : : When only one of P and Q is a conjunction, the number of
482 : : clauses are added. Otherwise, neither side is a conjunction and
483 : : no clauses are created. */
484 : 5978 : if (disjunction_p (lhs))
485 : : {
486 : 0 : if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
487 : : /* Both P and Q are conjunctions. */
488 : 0 : return std::make_pair (n1 * n2, true);
489 : 0 : if ((disjunction_p (rhs) && d1 != d2)
490 : 0 : || conjunction_p (rhs)
491 : 0 : || (atomic_p (rhs) && d1))
492 : : /* Either LHS or RHS is a conjunction. */
493 : 0 : return std::make_pair (n1 + n2, true);
494 : : else
495 : : /* Neither LHS nor RHS is a conjunction. */
496 : 0 : return std::make_pair (0, false);
497 : : }
498 : 5978 : if (conjunction_p (lhs))
499 : : {
500 : 5969 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
501 : : /* Both LHS and RHS are conjunctions. */
502 : 3980 : return std::make_pair (n1 * n2, true);
503 : : else
504 : : /* Only LHS is a conjunction. */
505 : 1989 : return std::make_pair (n1 + n2, true);
506 : : }
507 : 9 : if (atomic_p (lhs))
508 : : {
509 : 9 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
510 : : /* Only RHS is a disjunction. */
511 : 0 : return std::make_pair (n1 + n2, true);
512 : : else
513 : : /* Neither LHS nor RHS is a disjunction. */
514 : 9 : return std::make_pair (0, false);
515 : : }
516 : : }
517 : : else /* conjunction_p (t) */
518 : : {
519 : : /* Matches constraints of the form P /\ Q. Conjunctions contribute
520 : : linearly to the number of constraints. When both P and Q are
521 : : conjunctions, clauses are added. When only one of P and Q
522 : : is a conjunction, an additional clause is produced. When neither
523 : : P nor Q are conjunctions, two clauses are produced. */
524 : 2744247 : if (disjunction_p (lhs))
525 : : {
526 : 0 : if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
527 : : /* Both P and Q are conjunctions. */
528 : 0 : return std::make_pair (n1 + n2, d1 | d2);
529 : 0 : if ((disjunction_p (rhs) && d1 != d2)
530 : 0 : || conjunction_p (rhs)
531 : 0 : || (atomic_p (rhs) && d1))
532 : : /* Either LHS or RHS is a conjunction. */
533 : 0 : return std::make_pair (1 + n1 + n2, d1 | d2);
534 : : else
535 : : /* Neither LHS nor RHS is a conjunction. */
536 : 0 : return std::make_pair (2, false);
537 : : }
538 : 2744247 : if (conjunction_p (lhs))
539 : : {
540 : 1393418 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
541 : : /* Both LHS and RHS are conjunctions. */
542 : 1041258 : return std::make_pair (n1 + n2, d1 | d2);
543 : : else
544 : : /* Only LHS is a conjunction. */
545 : 352160 : return std::make_pair (1 + n1 + n2, d1 | d2);
546 : : }
547 : 1350829 : if (atomic_p (lhs))
548 : : {
549 : 1350829 : if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
550 : : /* Only RHS is a disjunction. */
551 : 287702 : return std::make_pair (1 + n1 + n2, d1 | d2);
552 : : else
553 : : /* Neither LHS nor RHS is a disjunction. */
554 : 1063127 : return std::make_pair (2, false);
555 : : }
556 : : }
557 : 0 : gcc_unreachable ();
558 : : }
559 : :
560 : : /* Count the number conjunctive clauses that would be created
561 : : when rewriting T to DNF. */
562 : :
563 : : static int
564 : 24133 : dnf_size (tree t)
565 : : {
566 : 0 : std::pair<int, bool> result = dnf_size_r (t);
567 : 24133 : return result.first == 0 ? 1 : result.first;
568 : : }
569 : :
570 : :
571 : : /* Count the number disjunctive clauses that would be created
572 : : when rewriting T to CNF. */
573 : :
574 : : static int
575 : 24133 : cnf_size (tree t)
576 : : {
577 : 0 : std::pair<int, bool> result = cnf_size_r (t);
578 : 24133 : return result.first == 0 ? 1 : result.first;
579 : : }
580 : :
581 : :
582 : : /* A left-conjunction is replaced by its operands. */
583 : :
584 : : void
585 : 2744214 : replace_term (clause& c, tree t)
586 : : {
587 : 2744214 : tree t1 = TREE_OPERAND (t, 0);
588 : 2744214 : tree t2 = TREE_OPERAND (t, 1);
589 : 2744214 : return c.replace (t1, t2);
590 : : }
591 : :
592 : : /* Create a new clause in the formula by copying the current
593 : : clause. In the current clause, the term at CI is replaced
594 : : by the first operand, and in the new clause, it is replaced
595 : : by the second. */
596 : :
597 : : void
598 : 5969 : branch_clause (formula& f, clause& c1, tree t)
599 : : {
600 : 5969 : tree t1 = TREE_OPERAND (t, 0);
601 : 5969 : tree t2 = TREE_OPERAND (t, 1);
602 : 5969 : clause& c2 = f.branch ();
603 : 5969 : c1.replace (t1);
604 : 5969 : c2.replace (t2);
605 : 5969 : }
606 : :
607 : : /* Decompose t1 /\ t2 according to the rules R. */
608 : :
609 : : inline void
610 : 2744214 : decompose_conjuntion (formula& f, clause& c, tree t, rules r)
611 : : {
612 : 2744214 : if (r == left)
613 : 2744214 : replace_term (c, t);
614 : : else
615 : 0 : branch_clause (f, c, t);
616 : 2744214 : }
617 : :
618 : : /* Decompose t1 \/ t2 according to the rules R. */
619 : :
620 : : inline void
621 : 5969 : decompose_disjunction (formula& f, clause& c, tree t, rules r)
622 : : {
623 : 5969 : if (r == right)
624 : 0 : replace_term (c, t);
625 : : else
626 : 5969 : branch_clause (f, c, t);
627 : 5969 : }
628 : :
629 : : /* An atomic constraint is already decomposed. */
630 : : inline void
631 : 847371 : decompose_atom (clause& c)
632 : : {
633 : 847371 : c.advance ();
634 : 847371 : }
635 : :
636 : : /* Decompose a term of clause C (in formula F) according to the
637 : : logical rules R. */
638 : :
639 : : void
640 : 3597554 : decompose_term (formula& f, clause& c, tree t, rules r)
641 : : {
642 : 3597554 : switch (TREE_CODE (t))
643 : : {
644 : 2744214 : case CONJ_CONSTR:
645 : 2744214 : return decompose_conjuntion (f, c, t, r);
646 : 5969 : case DISJ_CONSTR:
647 : 5969 : return decompose_disjunction (f, c, t, r);
648 : 847371 : default:
649 : 847371 : return decompose_atom (c);
650 : : }
651 : : }
652 : :
653 : : /* Decompose C (in F) using the logical rules R until it
654 : : is comprised of only atomic constraints. */
655 : :
656 : : void
657 : 30100 : decompose_clause (formula& f, clause& c, rules r)
658 : : {
659 : 3627654 : while (!c.done ())
660 : 3597554 : decompose_term (f, c, *c.current (), r);
661 : 30100 : f.advance ();
662 : 30100 : }
663 : :
664 : : static bool derive_proof (clause&, tree, rules);
665 : :
666 : : /* Derive a proof of both operands of T. */
667 : :
668 : : static bool
669 : 713446 : derive_proof_for_both_operands (clause& c, tree t, rules r)
670 : : {
671 : 713446 : if (!derive_proof (c, TREE_OPERAND (t, 0), r))
672 : : return false;
673 : 666265 : return derive_proof (c, TREE_OPERAND (t, 1), r);
674 : : }
675 : :
676 : : /* Derive a proof of either operand of T. */
677 : :
678 : : static bool
679 : 2875 : derive_proof_for_either_operand (clause& c, tree t, rules r)
680 : : {
681 : 2875 : if (derive_proof (c, TREE_OPERAND (t, 0), r))
682 : : return true;
683 : 2866 : return derive_proof (c, TREE_OPERAND (t, 1), r);
684 : : }
685 : :
686 : : /* Derive a proof of the atomic constraint T in clause C. */
687 : :
688 : : static bool
689 : 699231 : derive_atomic_proof (clause& c, tree t)
690 : : {
691 : 0 : return c.contains (t);
692 : : }
693 : :
694 : : /* Derive a proof of T from the terms in C. */
695 : :
696 : : static bool
697 : 1415552 : derive_proof (clause& c, tree t, rules r)
698 : : {
699 : 1415552 : switch (TREE_CODE (t))
700 : : {
701 : 713446 : case CONJ_CONSTR:
702 : 713446 : if (r == left)
703 : 713446 : return derive_proof_for_both_operands (c, t, r);
704 : : else
705 : 0 : return derive_proof_for_either_operand (c, t, r);
706 : 2875 : case DISJ_CONSTR:
707 : 2875 : if (r == left)
708 : 2875 : return derive_proof_for_either_operand (c, t, r);
709 : : else
710 : 0 : return derive_proof_for_both_operands (c, t, r);
711 : 699231 : default:
712 : 699231 : return derive_atomic_proof (c, t);
713 : : }
714 : : }
715 : :
716 : : /* Key/value pair for caching subsumption results. This associates a pair of
717 : : constraints with a boolean value indicating the result. */
718 : :
719 : : struct GTY((for_user)) subsumption_entry
720 : : {
721 : : tree lhs;
722 : : tree rhs;
723 : : bool result;
724 : : };
725 : :
726 : : /* Hashing function and equality for constraint entries. */
727 : :
728 : : struct subsumption_hasher : ggc_ptr_hash<subsumption_entry>
729 : : {
730 : 103328 : static hashval_t hash (subsumption_entry *e)
731 : : {
732 : 103328 : hashval_t val = 0;
733 : 103328 : val = iterative_hash_constraint (e->lhs, val);
734 : 103328 : val = iterative_hash_constraint (e->rhs, val);
735 : 103328 : return val;
736 : : }
737 : :
738 : 63595 : static bool equal (subsumption_entry *e1, subsumption_entry *e2)
739 : : {
740 : 63595 : if (!constraints_equivalent_p (e1->lhs, e2->lhs))
741 : : return false;
742 : 9669 : if (!constraints_equivalent_p (e1->rhs, e2->rhs))
743 : : return false;
744 : : return true;
745 : : }
746 : : };
747 : :
748 : : /* Caches the results of subsumes_constraints_nonnull (t1, t1). */
749 : :
750 : : static GTY ((deletable)) hash_table<subsumption_hasher> *subsumption_cache;
751 : :
752 : : /* Search for a previously cached subsumption result. */
753 : :
754 : : static bool*
755 : 32217 : lookup_subsumption (tree t1, tree t2)
756 : : {
757 : 32217 : if (!subsumption_cache)
758 : : return NULL;
759 : 26533 : subsumption_entry elt = { t1, t2, false };
760 : 26533 : subsumption_entry* found = subsumption_cache->find (&elt);
761 : 26533 : if (found)
762 : 8084 : return &found->result;
763 : : else
764 : : return 0;
765 : : }
766 : :
767 : : /* Save a subsumption result. */
768 : :
769 : : static bool
770 : 24133 : save_subsumption (tree t1, tree t2, bool result)
771 : : {
772 : 24133 : if (!subsumption_cache)
773 : 5684 : subsumption_cache = hash_table<subsumption_hasher>::create_ggc (31);
774 : 24133 : subsumption_entry elt = {t1, t2, result};
775 : 24133 : subsumption_entry** slot = subsumption_cache->find_slot (&elt, INSERT);
776 : 24133 : subsumption_entry* entry = ggc_alloc<subsumption_entry> ();
777 : 24133 : *entry = elt;
778 : 24133 : *slot = entry;
779 : 24133 : return result;
780 : : }
781 : :
782 : :
783 : : /* Returns true if the LEFT constraint subsume the RIGHT constraints.
784 : : This is done by deriving a proof of the conclusions on the RIGHT
785 : : from the assumptions on the LEFT assumptions. */
786 : :
787 : : static bool
788 : 32217 : subsumes_constraints_nonnull (tree lhs, tree rhs)
789 : : {
790 : 32217 : auto_timevar time (TV_CONSTRAINT_SUB);
791 : :
792 : 32217 : if (bool *b = lookup_subsumption (lhs, rhs))
793 : 8084 : return *b;
794 : :
795 : 24133 : tree x, y;
796 : 24133 : rules r;
797 : 72399 : if (dnf_size (lhs) <= cnf_size (rhs))
798 : : /* When LHS looks simpler than RHS, we'll determine subsumption by
799 : : decomposing LHS into its disjunctive normal form and checking that
800 : : each (conjunctive) clause in the decomposed LHS implies RHS. */
801 : : x = lhs, y = rhs, r = left;
802 : : else
803 : : /* Otherwise, we'll determine subsumption by decomposing RHS into its
804 : : conjunctive normal form and checking that each (disjunctive) clause
805 : : in the decomposed RHS implies LHS. */
806 : 0 : x = rhs, y = lhs, r = right;
807 : :
808 : : /* Decompose X into a list of sequents according to R, and recursively
809 : : check for implication of Y. */
810 : 24133 : bool result = true;
811 : 24133 : formula f (x);
812 : 66209 : while (!f.done ())
813 : : {
814 : 30100 : auto i = f.current ();
815 : 30100 : decompose_clause (f, *i, r);
816 : 30100 : if (!derive_proof (*i, y, r))
817 : : {
818 : : result = false;
819 : 24133 : break;
820 : : }
821 : 17943 : f.erase (i);
822 : : }
823 : :
824 : 24133 : return save_subsumption (lhs, rhs, result);
825 : 32217 : }
826 : :
827 : : /* Returns true if the LEFT constraints subsume the RIGHT
828 : : constraints. */
829 : :
830 : : bool
831 : 4746697 : subsumes (tree lhs, tree rhs)
832 : : {
833 : 4746697 : if (lhs == rhs)
834 : : return true;
835 : 592208 : if (!lhs || lhs == error_mark_node)
836 : : return false;
837 : 312203 : if (!rhs || rhs == error_mark_node)
838 : : return true;
839 : 32217 : return subsumes_constraints_nonnull (lhs, rhs);
840 : : }
841 : :
842 : : #include "gt-cp-logic.h"
|
