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