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