[gcc r12-2658] c++: Improve memory usage of subsumption [PR100828]

[gcc r12-2658] c++: Improve memory usage of subsumption [PR100828]

[Patrick Palka]

https://gcc.gnu.org/g:f48c3cd2e3f9cd9e3c329eb2d3185bd26e7c7607

commit r12-2658-gf48c3cd2e3f9cd9e3c329eb2d3185bd26e7c7607
Author: Patrick Palka <ppalka@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.

Diff:
---
 gcc/cp/logic.cc | 118 +++++++++++++++++---------------------------------------
 1 file changed, 35 insertions(+), 83 deletions(-)

diff --git a/gcc/cp/logic.cc b/gcc/cp/logic.cc
index 142457e408a..9d892b1473b 100644
--- a/gcc/cp/logic.cc
+++ b/gcc/cp/logic.cc
@@ -223,9 +223,7 @@ struct formula
 
   formula (tree t)
   {
-    /* This should call emplace_back(). There's an extra copy being
-       invoked by using push_back().  */
-    m_clauses.push_back (t);
+    m_clauses.emplace_back (t);
     m_current = m_clauses.begin ();
   }
 
@@ -248,8 +246,7 @@ struct formula
   clause& branch ()
   {
     gcc_assert (!done ());
-    m_clauses.push_back (*m_current);
-    return m_clauses.back ();
+    return *m_clauses.insert (std::next (m_current), *m_current);
   }
 
   /* Returns the position of the current clause.  */
@@ -287,6 +284,14 @@ struct formula
     return m_clauses.end ();
   }
 
+  /* Remove the specified clause from the formula.  */
+
+  void erase (iterator i)
+  {
+    gcc_assert (i != m_current);
+    m_clauses.erase (i);
+  }
+
   std::list<clause> m_clauses; /* The list of clauses.  */
   iterator m_current; /* The current clause.  */
 };
@@ -659,39 +664,6 @@ decompose_clause (formula& f, clause& c, rules r)
   f.advance ();
 }
 
-/* Decompose the logical formula F according to the logical
-   rules determined by R.  The result is a formula containing
-   clauses that contain only atomic terms.  */
-
-void
-decompose_formula (formula& f, rules r)
-{
-  while (!f.done ())
-    decompose_clause (f, *f.current (), r);
-}
-
-/* Fully decomposing T into a list of sequents, each comprised of
-   a list of atomic constraints, as if T were an antecedent.  */
-
-static formula
-decompose_antecedents (tree t)
-{
-  formula f (t);
-  decompose_formula (f, left);
-  return f;
-}
-
-/* Fully decomposing T into a list of sequents, each comprised of
-   a list of atomic constraints, as if T were a consequent.  */
-
-static formula
-decompose_consequents (tree t)
-{
-  formula f (t);
-  decompose_formula (f, right);
-  return f;
-}
-
 static bool derive_proof (clause&, tree, rules);
 
 /* Derive a proof of both operands of T.  */
@@ -744,28 +716,6 @@ derive_proof (clause& c, tree t, rules r)
   }
 }
 
-/* Derive a proof of T from disjunctive clauses in F.  */
-
-static bool
-derive_proofs (formula& f, tree t, rules r)
-{
-  for (formula::iterator i = f.begin(); i != f.end(); ++i)
-    if (!derive_proof (*i, t, r))
-      return false;
-  return true;
-}
-
-/* The largest number of clauses in CNF or DNF we accept as input
-   for subsumption. This an upper bound of 2^16 expressions.  */
-static int max_problem_size = 16;
-
-static inline bool
-diagnose_constraint_size (tree t)
-{
-  error_at (input_location, "%qE exceeds the maximum constraint complexity", t);
-  return false;
-}
-
 /* Key/value pair for caching subsumption results. This associates a pair of
    constraints with a boolean value indicating the result.  */
 
@@ -845,31 +795,33 @@ subsumes_constraints_nonnull (tree lhs, tree rhs)
   if (bool *b = lookup_subsumption(lhs, rhs))
     return *b;
 
-  int n1 = dnf_size (lhs);
-  int n2 = cnf_size (rhs);
-
-  /* Make sure we haven't exceeded the largest acceptable problem.  */
-  if (std::min (n1, n2) >= max_problem_size)
-    {
-      if (n1 < n2)
-        diagnose_constraint_size (lhs);
-      else
-	diagnose_constraint_size (rhs);
-      return false;
-    }
-
-  /* Decompose the smaller of the two formulas, and recursively
-     check for implication of the larger.  */
-  bool result;
-  if (n1 <= n2)
-    {
-      formula dnf = decompose_antecedents (lhs);
-      result = derive_proofs (dnf, rhs, left);
-    }
+  tree x, y;
+  rules r;
+  if (dnf_size (lhs) <= cnf_size (rhs))
+    /* When LHS looks simpler than RHS, we'll determine subsumption by
+       decomposing LHS into its disjunctive normal form and checking that
+       each (conjunctive) clause in the decomposed LHS implies RHS.  */
+    x = lhs, y = rhs, r = left;
   else
+    /* Otherwise, we'll determine subsumption by decomposing RHS into its
+       conjunctive normal form and checking that each (disjunctive) clause
+       in the decomposed RHS implies LHS.  */
+    x = rhs, y = lhs, r = right;
+
+  /* Decompose X into a list of sequents according to R, and recursively
+     check for implication of Y.  */
+  bool result = true;
+  formula f (x);
+  while (!f.done ())
     {
-      formula cnf = decompose_consequents (rhs);
-      result = derive_proofs (cnf, lhs, right);
+      auto i = f.current ();
+      decompose_clause (f, *i, r);
+      if (!derive_proof (*i, y, r))
+	{
+	  result = false;
+	  break;
+	}
+      f.erase (i);
     }
 
   return save_subsumption (lhs, rhs, result);