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

source code of gcc/cp/logic.cc