| Message ID | 20210719220529.2446563-1-ppalka@redhat.com |
|---|---|
| State | New |
| Headers | show |
| Series | c++: Improve memory usage of subsumption [PR100828] | expand |
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> { };
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); >
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); > > >
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); >>> >> >
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); > > > > > > > > > > >
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); >>>>> >>>> >>> >> >> >
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);