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

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.