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

[Patrick Palka <ppalka@redhat.com>]

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> { };