https://gcc.gnu.org/bugzilla/show_bug.cgi?id=100828
--- Comment #4 from CVS Commits <cvs-commit at gcc dot gnu.org> --- The releases/gcc-11 branch has been updated by Patrick Palka <ppa...@gcc.gnu.org>: https://gcc.gnu.org/g:90f3dd128bc709a76c52b5ae29b40903acb26f20 commit r11-8851-g90f3dd128bc709a76c52b5ae29b40903acb26f20 Author: Patrick Palka <ppa...@redhat.com> Date: Mon Aug 2 09:59:56 2021 -0400 c++: Improve memory usage of subsumption [PR100828] Constraint subsumption is implemented in two steps. The first step computes the disjunctive (or conjunctive) normal form of one of the constraints, and the second step verifies that each clause in the decomposed form implies the other constraint. Performing these two steps separately is problematic because in the first step the DNF/CNF can be exponentially larger than the original constraint, and by computing it ahead of time we'd have to keep all of it in memory. This patch fixes this exponential blowup in memory usage by interleaving the two steps, so that as soon as we decompose one clause we check implication for it. In turn, memory usage during subsumption is now worst case linear in the size of the constraints rather than exponential, and so we can safely remove the hard limit of 16 clauses without introducing runaway memory usage on some inputs. (Note the _time_ complexity of subsumption is still exponential in the worst case.) In order for this to work we need to make formula::branch() insert the copy of the current clause directly after the current clause rather than at the end of the list, so that we fully decompose a clause shortly after creating it. Otherwise we'd end up accumulating exponentially many (partially decomposed) clauses in memory anyway. PR c++/100828 gcc/cp/ChangeLog: * logic.cc (formula::formula): Use emplace_back instead of push_back. (formula::branch): Insert a copy of m_current directly after m_current instead of at the end of the list. (formula::erase): Define. (decompose_formula): Remove. (decompose_antecedents): Remove. (decompose_consequents): Remove. (derive_proofs): Remove. (max_problem_size): Remove. (diagnose_constraint_size): Remove. (subsumes_constraints_nonnull): Rewrite directly in terms of decompose_clause and derive_proof, interleaving decomposition with implication checking. Remove limit on constraint complexity. Use formula::erase to free the current clause before moving on to the next one. (cherry picked from commit f48c3cd2e3f9cd9e3c329eb2d3185bd26e7c7607)
