[PATCH] c++: Improve memory usage of subsumption [PR100828]

[PATCH] c++: Improve memory usage of subsumption [PR100828]

[Patrick Palka]

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
disjunctive normal form 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
these 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 formula::branch to prepend 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.

Bootstrapped and regtested on x86_64-pc-linux-gnu, and also tested on
range-v3 and cmcstl2.  Does this look OK for trunk and perhaps 11?

	PR c++/100828

gcc/cp/ChangeLog:

	* logic.cc (formula::formula): Use emplace_back.
	(formula::branch): Insert a copy of m_current in front of
	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.  Use formula::erase to free the
	current clause before moving on to the next one.
---
 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..3f872c11fe2 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.  */
+
+  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 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
+       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);
-- 
2.32.0.264.g75ae10bc75

Re: [PATCH] c++: Improve memory usage of subsumption [PR100828]

[Patrick Palka]

On Mon, 19 Jul 2021, Patrick Palka wrote:

> 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
> disjunctive normal form 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
> these 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 formula::branch to prepend 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.
> 
> Bootstrapped and regtested on x86_64-pc-linux-gnu, and also tested on
> range-v3 and cmcstl2.  Does this look OK for trunk and perhaps 11?

Here's a testcase that demonstrates the exponential improvement, because
the DNF/CNF for the below constraints has around 2^23 clauses.  Before
this patch (but after removing the hard limit of 16 clauses), compile
time and memory usage is 7s/2.4GB.  After this patch, it's 3.5s/25MB.

-- >8 --

template<class T> concept C = true;

template<class T>
requires (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
  || (C<T> && C<T>)
struct k;

template<class T>
requires (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && (C<T> || C<T>)
  && true
struct k<T> { };

Re: [PATCH] c++: Improve memory usage of subsumption [PR100828]

[Jason Merrill]

On 7/19/21 6:05 PM, Patrick Palka wrote:
> 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
> disjunctive normal form 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
> these 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 formula::branch to prepend 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.
> 
> Bootstrapped and regtested on x86_64-pc-linux-gnu, and also tested on
> range-v3 and cmcstl2.  Does this look OK for trunk and perhaps 11?

OK for trunk.

> 	PR c++/100828
> 
> gcc/cp/ChangeLog:
> 
> 	* logic.cc (formula::formula): Use emplace_back.
> 	(formula::branch): Insert a copy of m_current in front of
> 	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.  Use formula::erase to free the
> 	current clause before moving on to the next one.
> ---
>   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..3f872c11fe2 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.  */
> +
> +  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 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
> +       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);
> 

Re: [PATCH] c++: Improve memory usage of subsumption [PR100828]

[Patrick Palka]

On Wed, Jul 28, 2021 at 4:42 PM Jason Merrill <jason@redhat.com> wrote:
>
> On 7/19/21 6:05 PM, Patrick Palka wrote:
> > 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
> > disjunctive normal form 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
> > these 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 formula::branch to prepend 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.
> >
> > Bootstrapped and regtested on x86_64-pc-linux-gnu, and also tested on
> > range-v3 and cmcstl2.  Does this look OK for trunk and perhaps 11?
>
> OK for trunk.

Thanks a lot, patch committed to trunk as r12-2658.  Since this low
complexity limit was introduced in GCC 10, what do you think about
increasing the limit from 16 to say 128 in the 10/11 release branches
as a relatively safe stopgap?

>
> >       PR c++/100828
> >
> > gcc/cp/ChangeLog:
> >
> >       * logic.cc (formula::formula): Use emplace_back.
> >       (formula::branch): Insert a copy of m_current in front of
> >       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.  Use formula::erase to free the
> >       current clause before moving on to the next one.
> > ---
> >   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..3f872c11fe2 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.  */
> > +
> > +  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 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
> > +       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);
> >
>

Re: [PATCH] c++: Improve memory usage of subsumption [PR100828]

[Jason Merrill]

On 8/9/21 5:07 PM, Patrick Palka wrote:
> On Wed, Jul 28, 2021 at 4:42 PM Jason Merrill <jason@redhat.com> wrote:
>>
>> On 7/19/21 6:05 PM, Patrick Palka wrote:
>>> 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
>>> disjunctive normal form 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
>>> these 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 formula::branch to prepend 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.
>>>
>>> Bootstrapped and regtested on x86_64-pc-linux-gnu, and also tested on
>>> range-v3 and cmcstl2.  Does this look OK for trunk and perhaps 11?
>>
>> OK for trunk.
> 
> Thanks a lot, patch committed to trunk as r12-2658.  Since this low
> complexity limit was introduced in GCC 10, what do you think about
> increasing the limit from 16 to say 128 in the 10/11 release branches
> as a relatively safe stopgap?

Now that 11.2 is out, go ahead and apply this patch to the 11 branch.

Won't a limit of 128 in GCC 10 lead to extremely long compile times for 
affected code?  Is that more desirable than an error?

>>>        PR c++/100828
>>>
>>> gcc/cp/ChangeLog:
>>>
>>>        * logic.cc (formula::formula): Use emplace_back.
>>>        (formula::branch): Insert a copy of m_current in front of
>>>        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.  Use formula::erase to free the
>>>        current clause before moving on to the next one.
>>> ---
>>>    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..3f872c11fe2 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.  */
>>> +
>>> +  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 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
>>> +       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);
>>>
>>
> 

Re: [PATCH] c++: Improve memory usage of subsumption [PR100828]

[Patrick Palka]

On Wed, 11 Aug 2021, Jason Merrill wrote:

> On 8/9/21 5:07 PM, Patrick Palka wrote:
> > On Wed, Jul 28, 2021 at 4:42 PM Jason Merrill <jason@redhat.com> wrote:
> > > 
> > > On 7/19/21 6:05 PM, Patrick Palka wrote:
> > > > 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
> > > > disjunctive normal form 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
> > > > these 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 formula::branch to prepend 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.
> > > > 
> > > > Bootstrapped and regtested on x86_64-pc-linux-gnu, and also tested on
> > > > range-v3 and cmcstl2.  Does this look OK for trunk and perhaps 11?
> > > 
> > > OK for trunk.
> > 
> > Thanks a lot, patch committed to trunk as r12-2658.  Since this low
> > complexity limit was introduced in GCC 10, what do you think about
> > increasing the limit from 16 to say 128 in the 10/11 release branches
> > as a relatively safe stopgap?
> 
> Now that 11.2 is out, go ahead and apply this patch to the 11 branch.

Ah great, will do.

> 
> Won't a limit of 128 in GCC 10 lead to extremely long compile times for
> affected code?  Is that more desirable than an error?

Potentially, though I think that'd be the case only if the original
(normalized) constraint is huge to begin with.  The comment for
max_problem_size says

 /* 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;

which implies increasing it to 128 would allow for at most 2^128
expressions (clearly unacceptable), but I'm not sure how this upper
bound was obtained.

FWIW I think another upper bound for the number of expressions in the
CNF/DNF is roughly 'max_problem_size * size_of_original_constraint',
since we allow at most 'max_problem_size' clauses in the decomposed form
and each clause is definitely no larger than the original constraint.
So according to this upper bound the dependence on max_problem_size as
it relates to worst-case compile time/memory usage of subsumption is
linear rather than exponential, contrary to the comment.  In that case
increasing the limit from 16 to 128 doesn't seem to be too bad.

> 
> > > >        PR c++/100828
> > > > 
> > > > gcc/cp/ChangeLog:
> > > > 
> > > >        * logic.cc (formula::formula): Use emplace_back.
> > > >        (formula::branch): Insert a copy of m_current in front of
> > > >        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.  Use formula::erase to free the
> > > >        current clause before moving on to the next one.
> > > > ---
> > > >    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..3f872c11fe2 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.  */
> > > > +
> > > > +  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 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
> > > > +       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);
> > > > 
> > > 
> > 
> 
> 

Re: [PATCH] c++: Improve memory usage of subsumption [PR100828]

[Jason Merrill]

On 8/11/21 10:53 AM, Patrick Palka wrote:
> On Wed, 11 Aug 2021, Jason Merrill wrote:
> 
>> On 8/9/21 5:07 PM, Patrick Palka wrote:
>>> On Wed, Jul 28, 2021 at 4:42 PM Jason Merrill <jason@redhat.com> wrote:
>>>>
>>>> On 7/19/21 6:05 PM, Patrick Palka wrote:
>>>>> 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
>>>>> disjunctive normal form 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
>>>>> these 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 formula::branch to prepend 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.
>>>>>
>>>>> Bootstrapped and regtested on x86_64-pc-linux-gnu, and also tested on
>>>>> range-v3 and cmcstl2.  Does this look OK for trunk and perhaps 11?
>>>>
>>>> OK for trunk.
>>>
>>> Thanks a lot, patch committed to trunk as r12-2658.  Since this low
>>> complexity limit was introduced in GCC 10, what do you think about
>>> increasing the limit from 16 to say 128 in the 10/11 release branches
>>> as a relatively safe stopgap?
>>
>> Now that 11.2 is out, go ahead and apply this patch to the 11 branch.
> 
> Ah great, will do.
> 
>>
>> Won't a limit of 128 in GCC 10 lead to extremely long compile times for
>> affected code?  Is that more desirable than an error?
> 
> Potentially, though I think that'd be the case only if the original
> (normalized) constraint is huge to begin with.  The comment for
> max_problem_size says
> 
>   /* 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;
> 
> which implies increasing it to 128 would allow for at most 2^128
> expressions (clearly unacceptable), but I'm not sure how this upper
> bound was obtained.
> 
> FWIW I think another upper bound for the number of expressions in the
> CNF/DNF is roughly 'max_problem_size * size_of_original_constraint',
> since we allow at most 'max_problem_size' clauses in the decomposed form
> and each clause is definitely no larger than the original constraint.
> So according to this upper bound the dependence on max_problem_size as
> it relates to worst-case compile time/memory usage of subsumption is
> linear rather than exponential, contrary to the comment.  In that case
> increasing the limit from 16 to 128 doesn't seem to be too bad.

Fair, though I would expect anyone writing new concepts code to use GCC 
11.  Up to you.

>>>>>         PR c++/100828
>>>>>
>>>>> gcc/cp/ChangeLog:
>>>>>
>>>>>         * logic.cc (formula::formula): Use emplace_back.
>>>>>         (formula::branch): Insert a copy of m_current in front of
>>>>>         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.  Use formula::erase to free the
>>>>>         current clause before moving on to the next one.
>>>>> ---
>>>>>     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..3f872c11fe2 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.  */
>>>>> +
>>>>> +  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 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
>>>>> +       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);
>>>>>
>>>>
>>>
>>
>>
>