diff options
Diffstat (limited to 'gcc/cp/logic.cc')
| -rw-r--r-- | gcc/cp/logic.cc | 1183 |
1 files changed, 605 insertions, 578 deletions
diff --git a/gcc/cp/logic.cc b/gcc/cp/logic.cc index 13cc321..2d4abaf 100644 --- a/gcc/cp/logic.cc +++ b/gcc/cp/logic.cc @@ -47,729 +47,736 @@ along with GCC; see the file COPYING3. If not see #include "toplev.h" #include "type-utils.h" -namespace { +/* Hash functions for atomic constrains. */ -// Helper algorithms - -template<typename I> -inline I -next (I iter) +struct constraint_hash : default_hash_traits<tree> { - return ++iter; -} + static hashval_t hash (tree t) + { + return hash_atomic_constraint (t); + } -template<typename I, typename P> -inline bool -any_p (I first, I last, P pred) -{ - while (first != last) - { - if (pred(*first)) - return true; - ++first; - } - return false; -} + static bool equal (tree t1, tree t2) + { + return atomic_constraints_identical_p (t1, t2); + } +}; -bool prove_implication (tree, tree); +/* A conjunctive or disjunctive clause. -/*--------------------------------------------------------------------------- - Proof state ----------------------------------------------------------------------------*/ + Each clause maintains an iterator that refers to the current + term, which is used in the linear decomposition of a formula + into CNF or DNF. */ -struct term_entry +struct clause { - tree t; -}; + typedef std::list<tree>::iterator iterator; + typedef std::list<tree>::const_iterator const_iterator; -/* Hashing function and equality for constraint entries. */ + /* Initialize a clause with an initial term. */ -struct term_hasher : ggc_ptr_hash<term_entry> -{ - static hashval_t hash (term_entry *e) + clause (tree t) { - return iterative_hash_template_arg (e->t, 0); + m_terms.push_back (t); + if (TREE_CODE (t) == ATOMIC_CONSTR) + m_set.add (t); + + m_current = m_terms.begin (); } - static bool equal (term_entry *e1, term_entry *e2) + /* Create a copy of the current term. The current + iterator is set to point to the same position in the + copied list of terms. */ + + clause (clause const& c) + : m_terms (c.m_terms), m_set (c.m_set), m_current (m_terms.begin ()) { - return cp_tree_equal (e1->t, e2->t); + std::advance (m_current, std::distance (c.begin (), c.current ())); } -}; -/* A term list is a list of atomic constraints. It is used - to maintain the lists of assumptions and conclusions in a - proof goal. + /* Returns true when all terms are atoms. */ - Each term list maintains an iterator that refers to the current - term. This can be used by various tactics to support iteration - and stateful manipulation of the list. */ -class term_list -{ -public: - typedef std::list<tree>::iterator iterator; + bool done () const + { + return m_current == end (); + } - term_list (); - term_list (tree); + /* Advance to the next term. */ - bool includes (tree); - iterator insert (iterator, tree); - iterator push_back (tree); - iterator erase (iterator); - iterator replace (iterator, tree); - iterator replace (iterator, tree, tree); + void advance () + { + gcc_assert (!done ()); + ++m_current; + } - iterator begin() { return seq.begin(); } - iterator end() { return seq.end(); } + /* Replaces the current term at position ITER with T. If + T is an atomic constraint that already appears in the + clause, remove but do not replace ITER. Returns a pair + containing an iterator to the replace object or past + the erased object and a boolean value which is true if + an object was erased. */ - std::list<tree> seq; - hash_table<term_hasher> tab; -}; + std::pair<iterator, bool> replace (iterator iter, tree t) + { + gcc_assert (TREE_CODE (*iter) != ATOMIC_CONSTR); + if (TREE_CODE (t) == ATOMIC_CONSTR) + { + if (m_set.add (t)) + return std::make_pair (m_terms.erase (iter), true); + } + *iter = t; + return std::make_pair (iter, false); + } -inline -term_list::term_list () - : seq(), tab (11) -{ -} + /* Inserts T before ITER in the list of terms. If T has + already is an atomic constraint that already appears in + the clause, no action is taken, and the current iterator + is returned. Returns a pair of an iterator to the inserted + object or ITER if no insertion occurred and a boolean + value which is true if an object was inserted. */ -/* Initialize a term list with an initial term. */ + std::pair<iterator, bool> insert (iterator iter, tree t) + { + if (TREE_CODE (t) == ATOMIC_CONSTR) + { + if (m_set.add (t)) + return std::make_pair (iter, false); + } + return std::make_pair (m_terms.insert (iter, t), true); + } -inline -term_list::term_list (tree t) - : seq (), tab (11) -{ - push_back (t); -} + /* Replaces the current term with T. In the case where the + current term is erased (because T is redundant), update + the position of the current term to the next term. */ -/* Returns true if T is the in the tree. */ + void replace (tree t) + { + m_current = replace (m_current, t).first; + } -inline bool -term_list::includes (tree t) -{ - term_entry ent = {t}; - return tab.find (&ent); -} + /* Replace the current term with T1 and T2, in that order. */ -/* Append a term to the list. */ -inline term_list::iterator -term_list::push_back (tree t) -{ - return insert (end(), t); -} + void replace (tree t1, tree t2) + { + /* Replace the current term with t1. Ensure that iter points + to the term before which t2 will be inserted. Update the + current term as needed. */ + std::pair<iterator, bool> rep = replace (m_current, t1); + if (rep.second) + m_current = rep.first; + else + ++rep.first; -/* Insert a new (unseen) term T into the list before the proposition - indicated by ITER. Returns the iterator to the newly inserted - element. */ + /* Insert the t2. Make this the current term if we erased + the prior term. */ + std::pair<iterator, bool> ins = insert (rep.first, t2); + if (rep.second && ins.second) + m_current = ins.first; + } -term_list::iterator -term_list::insert (iterator iter, tree t) -{ - gcc_assert (!includes (t)); - iter = seq.insert (iter, t); - term_entry ent = {t}; - term_entry** slot = tab.find_slot (&ent, INSERT); - term_entry* ptr = ggc_alloc<term_entry> (); - *ptr = ent; - *slot = ptr; - return iter; -} + /* Returns true if the clause contains the term T. */ -/* Remove an existing term from the list. Returns an iterator referring - to the element after the removed term. This may be end(). */ + bool contains (tree t) + { + gcc_assert (TREE_CODE (t) == ATOMIC_CONSTR); + return m_set.contains (t); + } -term_list::iterator -term_list::erase (iterator iter) -{ - gcc_assert (includes (*iter)); - term_entry ent = {*iter}; - tab.remove_elt (&ent); - iter = seq.erase (iter); - return iter; -} -/* Replace the given term with that specified. If the term has - been previously seen, do not insert the term. Returns the - first iterator past the current term. */ + /* Returns an iterator to the first clause in the formula. */ -term_list::iterator -term_list::replace (iterator iter, tree t) -{ - iter = erase (iter); - if (!includes (t)) - insert (iter, t); - return iter; -} + iterator begin () + { + return m_terms.begin (); + } + /* Returns an iterator to the first clause in the formula. */ -/* Replace the term at the given position by the supplied T1 - followed by t2. This is used in certain logical operators to - load a list of assumptions or conclusions. */ + const_iterator begin () const + { + return m_terms.begin (); + } -term_list::iterator -term_list::replace (iterator iter, tree t1, tree t2) -{ - iter = erase (iter); - if (!includes (t1)) - insert (iter, t1); - if (!includes (t2)) - insert (iter, t2); - return iter; -} + /* Returns an iterator past the last clause in the formula. */ + + iterator end () + { + return m_terms.end (); + } -/* A goal (or subgoal) models a sequent of the form - 'A |- C' where A and C are lists of assumptions and - conclusions written as propositions in the constraint - language (i.e., lists of trees). */ + /* Returns an iterator past the last clause in the formula. */ -class proof_goal -{ -public: - term_list assumptions; - term_list conclusions; + const_iterator end () const + { + return m_terms.end (); + } + + /* Returns the current iterator. */ + + const_iterator current () const + { + return m_current; + } + + std::list<tree> m_terms; /* The list of terms. */ + hash_set<tree, false, constraint_hash> m_set; /* The set of atomic constraints. */ + iterator m_current; /* The current term. */ }; + /* A proof state owns a list of goals and tracks the current sub-goal. The class also provides facilities for managing subgoals and constructing term lists. */ -class proof_state : public std::list<proof_goal> +struct formula { -public: - proof_state (); + typedef std::list<clause>::iterator iterator; + typedef std::list<clause>::const_iterator const_iterator; - iterator branch (iterator i); - iterator discharge (iterator i); -}; + /* Construct a formula with an initial formula in a + single clause. */ -/* Initialize the state with a single empty goal, and set that goal - as the current subgoal. */ - -inline -proof_state::proof_state () - : std::list<proof_goal> (1) -{ } + formula (tree t) + { + /* This should call emplace_back(). There's a an extra copy being + invoked by using push_back(). */ + m_clauses.push_back (t); + m_current = m_clauses.begin (); + } + /* Returns true when all clauses are atomic. */ + bool done () const + { + return m_current == end (); + } -/* Branch the current goal by creating a new subgoal, returning a - reference to the new object. This does not update the current goal. */ + /* Advance to the next term. */ + void advance () + { + gcc_assert (!done ()); + ++m_current; + } -inline proof_state::iterator -proof_state::branch (iterator i) -{ - gcc_assert (i != end()); - proof_goal& g = *i; - return insert (++i, g); -} + /* Insert a copy of clause into the formula. This corresponds + to a distribution of one logical operation over the other. */ -/* Discharge the current goal, setting it equal to the - next non-satisfied goal. */ + clause& branch () + { + gcc_assert (!done ()); + m_clauses.push_back (*m_current); + return m_clauses.back (); + } -inline proof_state::iterator -proof_state::discharge (iterator i) -{ - gcc_assert (i != end()); - return erase (i); -} + /* Returns the position of the current clause. */ + iterator current () + { + return m_current; + } -/*--------------------------------------------------------------------------- - Debugging ----------------------------------------------------------------------------*/ + /* Returns an iterator to the first clause in the formula. */ -// void -// debug (term_list& ts) -// { -// for (term_list::iterator i = ts.begin(); i != ts.end(); ++i) -// verbatim (" # %E", *i); -// } -// -// void -// debug (proof_goal& g) -// { -// debug (g.assumptions); -// verbatim (" |-"); -// debug (g.conclusions); -// } + iterator begin () + { + return m_clauses.begin (); + } -/*--------------------------------------------------------------------------- - Atomicity of constraints ----------------------------------------------------------------------------*/ + /* Returns an iterator to the first clause in the formula. */ -/* Returns true if T is not an atomic constraint. */ + const_iterator begin () const + { + return m_clauses.begin (); + } -bool -non_atomic_constraint_p (tree t) -{ - switch (TREE_CODE (t)) - { - case PRED_CONSTR: - case EXPR_CONSTR: - case TYPE_CONSTR: - case ICONV_CONSTR: - case DEDUCT_CONSTR: - case EXCEPT_CONSTR: - /* A pack expansion isn't atomic, but it can't decompose to prove an - atom, so it shouldn't cause analyze_atom to return undecided. */ - case EXPR_PACK_EXPANSION: - return false; - case CHECK_CONSTR: - case PARM_CONSTR: - case CONJ_CONSTR: - case DISJ_CONSTR: - return true; - default: - gcc_unreachable (); - } -} + /* Returns an iterator past the last clause in the formula. */ -/* Returns true if any constraints in T are not atomic. */ + iterator end () + { + return m_clauses.end (); + } -bool -any_non_atomic_constraints_p (term_list& t) -{ - return any_p (t.begin(), t.end(), non_atomic_constraint_p); -} + /* Returns an iterator past the last clause in the formula. */ -/*--------------------------------------------------------------------------- - Proof validations ----------------------------------------------------------------------------*/ + const_iterator end () const + { + return m_clauses.end (); + } -enum proof_result -{ - invalid, - valid, - undecided + std::list<clause> m_clauses; /* The list of clauses. */ + iterator m_current; /* The current clause. */ }; -proof_result check_term (term_list&, tree); - - -proof_result -analyze_atom (term_list& ts, tree t) +void +debug (clause& c) { - /* FIXME: Hook into special cases, if any. */ - /* - term_list::iterator iter = ts.begin(); - term_list::iterator end = ts.end(); - while (iter != end) - { - ++iter; - } - */ - - if (non_atomic_constraint_p (t)) - return undecided; - if (any_non_atomic_constraints_p (ts)) - return undecided; - return invalid; + for (clause::iterator i = c.begin(); i != c.end(); ++i) + verbatim (" # %E", *i); } -/* Search for a pack expansion in the list of assumptions that would - make this expansion valid. */ - -proof_result -analyze_pack (term_list& ts, tree t) +void +debug (formula& f) { - tree c1 = normalize_expression (PACK_EXPANSION_PATTERN (t)); - term_list::iterator iter = ts.begin(); - term_list::iterator end = ts.end(); - while (iter != end) + for (formula::iterator i = f.begin(); i != f.end(); ++i) { - if (TREE_CODE (*iter) == TREE_CODE (t)) - { - tree c2 = normalize_expression (PACK_EXPANSION_PATTERN (*iter)); - if (prove_implication (c2, c1)) - return valid; - else - return invalid; - } - ++iter; + verbatim ("((("); + debug (*i); + verbatim (")))"); } - return invalid; } -/* Search for concept checks in TS that we know subsume T. */ +/* The logical rules used to analyze a logical formula. The + "left" and "right" refer to the position of formula in a + sequent (as in sequent calculus). */ -proof_result -search_known_subsumptions (term_list& ts, tree t) +enum rules { - for (term_list::iterator i = ts.begin(); i != ts.end(); ++i) - if (TREE_CODE (*i) == CHECK_CONSTR) - { - if (bool* b = lookup_subsumption_result (*i, t)) - return *b ? valid : invalid; - } - return undecided; -} + left, right +}; -/* Determine if the terms in TS provide sufficient support for proving - the proposition T. If any term in TS is a concept check that is known - to subsume T, then the proof is valid. Otherwise, we have to expand T - and continue searching for support. */ +/* Distribution counting. */ -proof_result -analyze_check (term_list& ts, tree t) +static inline bool +disjunction_p (tree t) { - proof_result r = search_known_subsumptions (ts, t); - if (r != undecided) - return r; - - tree tmpl = CHECK_CONSTR_CONCEPT (t); - tree args = CHECK_CONSTR_ARGS (t); - tree c = expand_concept (tmpl, args); - return check_term (ts, c); + return TREE_CODE (t) == DISJ_CONSTR; } -/* Recursively check constraints of the parameterized constraint. */ - -proof_result -analyze_parameterized (term_list& ts, tree t) +static inline bool +conjunction_p (tree t) { - return check_term (ts, PARM_CONSTR_OPERAND (t)); + return TREE_CODE (t) == CONJ_CONSTR; } -proof_result -analyze_conjunction (term_list& ts, tree t) +static inline bool +atomic_p (tree t) { - proof_result r = check_term (ts, TREE_OPERAND (t, 0)); - if (r == invalid || r == undecided) - return r; - return check_term (ts, TREE_OPERAND (t, 1)); + return TREE_CODE (t) == ATOMIC_CONSTR; } -proof_result -analyze_disjunction (term_list& ts, tree t) -{ - proof_result r = check_term (ts, TREE_OPERAND (t, 0)); - if (r == valid) - return r; - return check_term (ts, TREE_OPERAND (t, 1)); -} +/* Recursively count the number of clauses produced when converting T + to DNF. Returns a pair containing the number of clauses and a bool + value signifying that the the tree would be rewritten as a result of + distributing. In general, a conjunction for which this flag is set + is considered a disjunction for the purpose of counting. */ -proof_result -analyze_term (term_list& ts, tree t) +static std::pair<int, bool> +dnf_size_r (tree t) { - switch (TREE_CODE (t)) - { - case CHECK_CONSTR: - return analyze_check (ts, t); + if (atomic_p (t)) + /* Atomic constraints produce no clauses. */ + return std::make_pair (0, false); - case PARM_CONSTR: - return analyze_parameterized (ts, t); + /* For compound constraints, recursively count clauses and unpack + the results. */ + tree lhs = TREE_OPERAND (t, 0); + tree rhs = TREE_OPERAND (t, 1); + std::pair<int, bool> p1 = dnf_size_r (lhs); + std::pair<int, bool> p2 = dnf_size_r (rhs); + int n1 = p1.first, n2 = p2.first; + bool d1 = p1.second, d2 = p2.second; - case CONJ_CONSTR: - return analyze_conjunction (ts, t); - case DISJ_CONSTR: - return analyze_disjunction (ts, t); - - case PRED_CONSTR: - case EXPR_CONSTR: - case TYPE_CONSTR: - case ICONV_CONSTR: - case DEDUCT_CONSTR: - case EXCEPT_CONSTR: - return analyze_atom (ts, t); - - case EXPR_PACK_EXPANSION: - return analyze_pack (ts, t); - - case ERROR_MARK: - /* Encountering an error anywhere in a constraint invalidates - the proof, since the constraint is ill-formed. */ - return invalid; - default: - gcc_unreachable (); + if (disjunction_p (t)) + { + /* Matches constraints of the form P \/ Q. Disjunctions contribute + linearly to the number of constraints. When both P and Q are + disjunctions, clauses are added. When only one of P and Q + is a disjunction, an additional clause is produced. When neither + P nor Q are disjunctions, two clauses are produced. */ + if (disjunction_p (lhs)) + { + if (disjunction_p (rhs) || (conjunction_p (rhs) && d2)) + /* Both P and Q are disjunctions. */ + return std::make_pair (n1 + n2, d1 | d2); + else + /* Only LHS is a disjunction. */ + return std::make_pair (1 + n1 + n2, d1 | d2); + gcc_unreachable (); + } + if (conjunction_p (lhs)) + { + if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2)) + /* Both P and Q are disjunctions. */ + return std::make_pair (n1 + n2, d1 | d2); + if (disjunction_p (rhs) + || (conjunction_p (rhs) && d1 != d2) + || (atomic_p (rhs) && d1)) + /* Either LHS or RHS is a disjunction. */ + return std::make_pair (1 + n1 + n2, d1 | d2); + else + /* Neither LHS nor RHS is a disjunction. */ + return std::make_pair (2, false); + } + if (atomic_p (lhs)) + { + if (disjunction_p (rhs) || (conjunction_p (rhs) && d2)) + /* Only RHS is a disjunction. */ + return std::make_pair (1 + n1 + n2, d1 | d2); + else + /* Neither LHS nor RHS is a disjunction. */ + return std::make_pair (2, false); + } + } + else /* conjunction_p (t) */ + { + /* Matches constraints of the form P /\ Q, possibly resulting + in the distribution of one side over the other. When both + P and Q are disjunctions, the number of clauses are multiplied. + When only one of P and Q is a disjunction, the the number of + clauses are added. Otherwise, neither side is a disjunction and + no clauses are created. */ + if (disjunction_p (lhs)) + { + if (disjunction_p (rhs) || (conjunction_p (rhs) && d2)) + /* Both P and Q are disjunctions. */ + return std::make_pair (n1 * n2, true); + else + /* Only LHS is a disjunction. */ + return std::make_pair (n1 + n2, true); + gcc_unreachable (); + } + if (conjunction_p (lhs)) + { + if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2)) + /* Both P and Q are disjunctions. */ + return std::make_pair (n1 * n2, true); + if (disjunction_p (rhs) + || (conjunction_p (rhs) && d1 != d2) + || (atomic_p (rhs) && d1)) + /* Either LHS or RHS is a disjunction. */ + return std::make_pair (n1 + n2, true); + else + /* Neither LHS nor RHS is a disjunction. */ + return std::make_pair (0, false); + } + if (atomic_p (lhs)) + { + if (disjunction_p (rhs) || (conjunction_p (rhs) && d2)) + /* Only RHS is a disjunction. */ + return std::make_pair (n1 + n2, true); + else + /* Neither LHS nor RHS is a disjunction. */ + return std::make_pair (0, false); + } } + gcc_unreachable (); } -/* Check if a single term can be proven from a set of assumptions. - If the proof is not valid, then it is incomplete when either - the given term is non-atomic or any term in the list of assumptions - is not-atomic. */ +/* Recursively count the number of clauses produced when converting T + to CNF. Returns a pair containing the number of clauses and a bool + value signifying that the the tree would be rewritten as a result of + distributing. In general, a disjunction for which this flag is set + is considered a conjunction for the purpose of counting. */ -proof_result -check_term (term_list& ts, tree t) +static std::pair<int, bool> +cnf_size_r (tree t) { - /* Try the easy way; search for an equivalent term. */ - if (ts.includes (t)) - return valid; + if (atomic_p (t)) + /* Atomic constraints produce no clauses. */ + return std::make_pair (0, false); - /* The hard way; actually consider what the term means. */ - return analyze_term (ts, t); -} + /* For compound constraints, recursively count clauses and unpack + the results. */ + tree lhs = TREE_OPERAND (t, 0); + tree rhs = TREE_OPERAND (t, 1); + std::pair<int, bool> p1 = cnf_size_r (lhs); + std::pair<int, bool> p2 = cnf_size_r (rhs); + int n1 = p1.first, n2 = p2.first; + bool d1 = p1.second, d2 = p2.second; -/* Check to see if any term is proven by the assumptions in the - proof goal. The proof is valid if the proof of any term is valid. - If validity cannot be determined, but any particular - check was undecided, then this goal is undecided. */ - -proof_result -check_goal (proof_goal& g) -{ - term_list::iterator iter = g.conclusions.begin (); - term_list::iterator end = g.conclusions.end (); - bool incomplete = false; - while (iter != end) + if (disjunction_p (t)) { - proof_result r = check_term (g.assumptions, *iter); - if (r == valid) - return r; - if (r == undecided) - incomplete = true; - ++iter; + /* Matches constraints of the form P \/ Q, possibly resulting + in the distribution of one side over the other. When both + P and Q are conjunctions, the number of clauses are multiplied. + When only one of P and Q is a conjunction, the the number of + clauses are added. Otherwise, neither side is a conjunction and + no clauses are created. */ + if (disjunction_p (lhs)) + { + if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1)) + /* Both P and Q are conjunctions. */ + return std::make_pair (n1 * n2, true); + if ((disjunction_p (rhs) && d1 != d2) + || conjunction_p (rhs) + || (atomic_p (rhs) && d1)) + /* Either LHS or RHS is a conjunction. */ + return std::make_pair (n1 + n2, true); + else + /* Neither LHS nor RHS is a conjunction. */ + return std::make_pair (0, false); + gcc_unreachable (); + } + if (conjunction_p (lhs)) + { + if ((disjunction_p (rhs) && d2) || conjunction_p (rhs)) + /* Both LHS and RHS are conjunctions. */ + return std::make_pair (n1 * n2, true); + else + /* Only LHS is a conjunction. */ + return std::make_pair (n1 + n2, true); + } + if (atomic_p (lhs)) + { + if ((disjunction_p (rhs) && d2) || conjunction_p (rhs)) + /* Only RHS is a disjunction. */ + return std::make_pair (n1 + n2, true); + else + /* Neither LHS nor RHS is a disjunction. */ + return std::make_pair (0, false); + } } - - /* Was the proof complete? */ - if (incomplete) - return undecided; - else - return invalid; -} - -/* Check if the the proof is valid. This is the case when all - goals can be discharged. If any goal is invalid, then the - entire proof is invalid. Otherwise, the proof is undecided. */ - -proof_result -check_proof (proof_state& p) -{ - proof_state::iterator iter = p.begin(); - proof_state::iterator end = p.end(); - while (iter != end) + else /* conjunction_p (t) */ { - proof_result r = check_goal (*iter); - if (r == invalid) - return r; - if (r == valid) - iter = p.discharge (iter); - else - ++iter; + /* Matches constraints of the form P /\ Q. Conjunctions contribute + linearly to the number of constraints. When both P and Q are + conjunctions, clauses are added. When only one of P and Q + is a conjunction, an additional clause is produced. When neither + P nor Q are conjunctions, two clauses are produced. */ + if (disjunction_p (lhs)) + { + if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1)) + /* Both P and Q are conjunctions. */ + return std::make_pair (n1 + n2, d1 | d2); + if ((disjunction_p (rhs) && d1 != d2) + || conjunction_p (rhs) + || (atomic_p (rhs) && d1)) + /* Either LHS or RHS is a conjunction. */ + return std::make_pair (1 + n1 + n2, d1 | d2); + else + /* Neither LHS nor RHS is a conjunction. */ + return std::make_pair (2, false); + gcc_unreachable (); + } + if (conjunction_p (lhs)) + { + if ((disjunction_p (rhs) && d2) || conjunction_p (rhs)) + /* Both LHS and RHS are conjunctions. */ + return std::make_pair (n1 + n2, d1 | d2); + else + /* Only LHS is a conjunction. */ + return std::make_pair (1 + n1 + n2, d1 | d2); + } + if (atomic_p (lhs)) + { + if ((disjunction_p (rhs) && d2) || conjunction_p (rhs)) + /* Only RHS is a disjunction. */ + return std::make_pair (1 + n1 + n2, d1 | d2); + else + /* Neither LHS nor RHS is a disjunction. */ + return std::make_pair (2, false); + } } - - /* If all goals are discharged, then the proof is valid. */ - if (p.empty()) - return valid; - else - return undecided; + gcc_unreachable (); } -/*--------------------------------------------------------------------------- - Left logical rules ----------------------------------------------------------------------------*/ +/* Count the number conjunctive clauses that would be created + when rewriting T to DNF. */ -term_list::iterator -load_check_assumption (term_list& ts, term_list::iterator i) +static int +dnf_size (tree t) { - tree decl = CHECK_CONSTR_CONCEPT (*i); - tree tmpl = DECL_TI_TEMPLATE (decl); - tree args = CHECK_CONSTR_ARGS (*i); - return ts.replace(i, expand_concept (tmpl, args)); + std::pair<int, bool> result = dnf_size_r (t); + return result.first == 0 ? 1 : result.first; } -term_list::iterator -load_parameterized_assumption (term_list& ts, term_list::iterator i) -{ - return ts.replace(i, PARM_CONSTR_OPERAND(*i)); -} -term_list::iterator -load_conjunction_assumption (term_list& ts, term_list::iterator i) +/* Count the number disjunctive clauses that would be created + when rewriting T to CNF. */ + +static int +cnf_size (tree t) { - tree t1 = TREE_OPERAND (*i, 0); - tree t2 = TREE_OPERAND (*i, 1); - return ts.replace(i, t1, t2); + std::pair<int, bool> result = cnf_size_r (t); + return result.first == 0 ? 1 : result.first; } -/* Examine the terms in the list, and apply left-logical rules to move - terms into the set of assumptions. */ + +/* A left-conjunction is replaced by its operands. */ void -load_assumptions (proof_goal& g) +replace_term (clause& c, tree t) { - term_list::iterator iter = g.assumptions.begin(); - term_list::iterator end = g.assumptions.end(); - while (iter != end) - { - switch (TREE_CODE (*iter)) - { - case CHECK_CONSTR: - iter = load_check_assumption (g.assumptions, iter); - break; - case PARM_CONSTR: - iter = load_parameterized_assumption (g.assumptions, iter); - break; - case CONJ_CONSTR: - iter = load_conjunction_assumption (g.assumptions, iter); - break; - default: - ++iter; - break; - } - } + tree t1 = TREE_OPERAND (t, 0); + tree t2 = TREE_OPERAND (t, 1); + return c.replace (t1, t2); } -/* In each subgoal, load constraints into the assumption set. */ +/* Create a new clause in the formula by copying the current + clause. In the current clause, the term at CI is replaced + by the first operand, and in the new clause, it is replaced + by the second. */ void -load_assumptions(proof_state& p) +branch_clause (formula& f, clause& c1, tree t) { - proof_state::iterator iter = p.begin(); - while (iter != p.end()) - { - load_assumptions (*iter); - ++iter; - } + tree t1 = TREE_OPERAND (t, 0); + tree t2 = TREE_OPERAND (t, 1); + clause& c2 = f.branch (); + c1.replace (t1); + c2.replace (t2); } -void -explode_disjunction (proof_state& p, proof_state::iterator gi, term_list::iterator ti1) -{ - tree t1 = TREE_OPERAND (*ti1, 0); - tree t2 = TREE_OPERAND (*ti1, 1); +/* Decompose t1 /\ t2 according to the rules R. */ - /* Erase the current term from the goal. */ - proof_goal& g1 = *gi; - proof_goal& g2 = *p.branch (gi); +inline void +decompose_conjuntion (formula& f, clause& c, tree t, rules r) +{ + if (r == left) + replace_term (c, t); + else + branch_clause (f, c, t); +} - /* Get an iterator to the equivalent position in th enew goal. */ - int n = std::distance (g1.assumptions.begin (), ti1); - term_list::iterator ti2 = g2.assumptions.begin (); - std::advance (ti2, n); +/* Decompose t1 \/ t2 according to the rules R. */ - /* Replace the disjunction in both branches. */ - g1.assumptions.replace (ti1, t1); - g2.assumptions.replace (ti2, t2); +inline void +decompose_disjunction (formula& f, clause& c, tree t, rules r) +{ + if (r == right) + replace_term (c, t); + else + branch_clause (f, c, t); } +/* An atomic constraint is already decomposed. */ +inline void +decompose_atom (clause& c) +{ + c.advance (); +} -/* Search the assumptions of the goal for the first disjunction. */ +/* Decompose a term of clause C (in formula F) according to the + logical rules R. */ -bool -explode_goal (proof_state& p, proof_state::iterator gi) +void +decompose_term (formula& f, clause& c, tree t, rules r) { - term_list& ts = gi->assumptions; - term_list::iterator ti = ts.begin(); - term_list::iterator end = ts.end(); - while (ti != end) + switch (TREE_CODE (t)) { - if (TREE_CODE (*ti) == DISJ_CONSTR) - { - explode_disjunction (p, gi, ti); - return true; - } - else ++ti; + case CONJ_CONSTR: + return decompose_conjuntion (f, c, t, r); + case DISJ_CONSTR: + return decompose_disjunction (f, c, t, r); + default: + return decompose_atom (c); } - return false; } -/* Search for the first goal with a disjunction, and then branch - creating a clone of that subgoal. */ +/* Decompose C (in F) using the logical rules R until it + is comprised of only atomic constraints. */ void -explode_assumptions (proof_state& p) +decompose_clause (formula& f, clause& c, rules r) { - proof_state::iterator iter = p.begin(); - proof_state::iterator end = p.end(); - while (iter != end) - { - if (explode_goal (p, iter)) - return; - ++iter; - } + while (!c.done ()) + decompose_term (f, c, *c.current (), 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. */ -/*--------------------------------------------------------------------------- - Right logical rules ----------------------------------------------------------------------------*/ - -term_list::iterator -load_disjunction_conclusion (term_list& g, term_list::iterator i) +void +decompose_formula (formula& f, rules r) { - tree t1 = TREE_OPERAND (*i, 0); - tree t2 = TREE_OPERAND (*i, 1); - return g.replace(i, t1, t2); + while (!f.done ()) + decompose_clause (f, *f.current (), r); } -/* Apply logical rules to the right hand side. This will load the - conclusion set with all tpp-level disjunctions. */ +/* Fully decomposing T into a list of sequents, each comprised of + a list of atomic constraints, as if T were an antecedent. */ -void -load_conclusions (proof_goal& g) +static formula +decompose_antecedents (tree t) { - term_list::iterator iter = g.conclusions.begin(); - term_list::iterator end = g.conclusions.end(); - while (iter != end) - { - if (TREE_CODE (*iter) == DISJ_CONSTR) - iter = load_disjunction_conclusion (g.conclusions, iter); - else - ++iter; - } + formula f (t); + decompose_formula (f, left); + return f; } -void -load_conclusions (proof_state& p) +/* 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) { - proof_state::iterator iter = p.begin(); - while (iter != p.end()) - { - load_conclusions (*iter); - ++iter; - } + formula f (t); + decompose_formula (f, right); + return f; } +static bool derive_proof (clause&, tree, rules); -/*--------------------------------------------------------------------------- - High-level proof tactics ----------------------------------------------------------------------------*/ +/* Derive a proof of both operands of T. */ -/* Given two constraints A and C, try to derive a proof that - A implies C. */ +static bool +derive_proof_for_both_operands (clause& c, tree t, rules r) +{ + if (!derive_proof (c, TREE_OPERAND (t, 0), r)) + return false; + return derive_proof (c, TREE_OPERAND (t, 1), r); +} -bool -prove_implication (tree a, tree c) +/* Derive a proof of either operand of T. */ + +static bool +derive_proof_for_either_operand (clause& c, tree t, rules r) { - /* Quick accept. */ - if (cp_tree_equal (a, c)) + if (derive_proof (c, TREE_OPERAND (t, 0), r)) return true; + return derive_proof (c, TREE_OPERAND (t, 1), r); +} - /* Build the initial proof state. */ - proof_state proof; - proof_goal& goal = proof.front(); - goal.assumptions.push_back(a); - goal.conclusions.push_back(c); - - /* Perform an initial right-expansion in the off-chance that the right - hand side contains disjunctions. */ - load_conclusions (proof); +/* Derive a proof of the atomic constraint T in clause C. */ - int step_max = 1 << 10; - int step_count = 0; /* FIXME: We shouldn't have this. */ - std::size_t branch_limit = 1024; /* FIXME: This needs to be configurable. */ - while (step_count < step_max && proof.size() < branch_limit) - { - /* Determine if we can prove that the assumptions entail the - conclusions. If so, we're done. */ - load_assumptions (proof); +static bool +derive_atomic_proof (clause& c, tree t) +{ + return c.contains (t); +} - /* Can we solve the proof based on this? */ - proof_result r = check_proof (proof); - if (r != undecided) - return r == valid; +/* Derive a proof of T from the terms in C. */ - /* If not, then we need to dig into disjunctions. */ - explode_assumptions (proof); +static bool +derive_proof (clause& c, tree t, rules r) +{ + switch (TREE_CODE (t)) + { + case CONJ_CONSTR: + if (r == left) + return derive_proof_for_both_operands (c, t, r); + else + return derive_proof_for_either_operand (c, t, r); + case DISJ_CONSTR: + if (r == left) + return derive_proof_for_either_operand (c, t, r); + else + return derive_proof_for_both_operands (c, t, r); + default: + return derive_atomic_proof (c, t); + } +} - ++step_count; - } +/* Derive a proof of T from disjunctive clauses in F. */ - if (step_count == step_max) - error ("subsumption failed to resolve"); +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; +} - if (proof.size() == branch_limit) - error ("exceeded maximum number of branches"); +/* 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; } @@ -777,31 +784,51 @@ prove_implication (tree a, tree c) This is done by deriving a proof of the conclusions on the RIGHT from the assumptions on the LEFT assumptions. */ -bool -subsumes_constraints_nonnull (tree left, tree right) +static bool +subsumes_constraints_nonnull (tree lhs, tree rhs) { - gcc_assert (check_constraint_info (left)); - gcc_assert (check_constraint_info (right)); - auto_timevar time (TV_CONSTRAINT_SUB); - tree a = CI_ASSOCIATED_CONSTRAINTS (left); - tree c = CI_ASSOCIATED_CONSTRAINTS (right); - return prove_implication (a, c); -} -} /* namespace */ + 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 the implication using the larger. Note that for + constraints that are largely comprised of conjunctions the + it will usually be the case that n1 <= n2. */ + if (n1 <= n2) + { + formula dnf = decompose_antecedents (lhs); + return derive_proofs (dnf, rhs, left); + } + else + { + formula cnf = decompose_consequents (rhs); + return derive_proofs (cnf, lhs, right); + } +} /* Returns true if the LEFT constraints subsume the RIGHT constraints. */ bool -subsumes (tree left, tree right) +subsumes (tree lhs, tree rhs) { - if (left == right) + if (lhs == rhs) return true; - if (!left) + if (!lhs || lhs == error_mark_node) return false; - if (!right) + if (!rhs || rhs == error_mark_node) return true; - return subsumes_constraints_nonnull (left, right); + return subsumes_constraints_nonnull (lhs, rhs); } |