|
111
|
1 /* Derivation and subsumption rules for constraints.
|
|
145
|
2 Copyright (C) 2013-2020 Free Software Foundation, Inc.
|
|
111
|
3 Contributed by Andrew Sutton (andrew.n.sutton@gmail.com)
|
|
|
4
|
|
|
5 This file is part of GCC.
|
|
|
6
|
|
|
7 GCC is free software; you can redistribute it and/or modify
|
|
|
8 it under the terms of the GNU General Public License as published by
|
|
|
9 the Free Software Foundation; either version 3, or (at your option)
|
|
|
10 any later version.
|
|
|
11
|
|
|
12 GCC is distributed in the hope that it will be useful,
|
|
|
13 but WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
|
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
|
|
15 GNU General Public License for more details.
|
|
|
16
|
|
|
17 You should have received a copy of the GNU General Public License
|
|
|
18 along with GCC; see the file COPYING3. If not see
|
|
|
19 <http://www.gnu.org/licenses/>. */
|
|
|
20
|
|
|
21 #include "config.h"
|
|
|
22 #define INCLUDE_LIST
|
|
|
23 #include "system.h"
|
|
|
24 #include "coretypes.h"
|
|
|
25 #include "tm.h"
|
|
|
26 #include "timevar.h"
|
|
|
27 #include "hash-set.h"
|
|
|
28 #include "machmode.h"
|
|
|
29 #include "vec.h"
|
|
|
30 #include "double-int.h"
|
|
|
31 #include "input.h"
|
|
|
32 #include "alias.h"
|
|
|
33 #include "symtab.h"
|
|
|
34 #include "wide-int.h"
|
|
|
35 #include "inchash.h"
|
|
|
36 #include "tree.h"
|
|
|
37 #include "stringpool.h"
|
|
|
38 #include "attribs.h"
|
|
|
39 #include "intl.h"
|
|
|
40 #include "flags.h"
|
|
|
41 #include "cp-tree.h"
|
|
|
42 #include "c-family/c-common.h"
|
|
|
43 #include "c-family/c-objc.h"
|
|
|
44 #include "cp-objcp-common.h"
|
|
|
45 #include "tree-inline.h"
|
|
|
46 #include "decl.h"
|
|
|
47 #include "toplev.h"
|
|
|
48 #include "type-utils.h"
|
|
|
49
|
|
145
|
50 /* Hash functions for atomic constrains. */
|
|
111
|
51
|
|
145
|
52 struct constraint_hash : default_hash_traits<tree>
|
|
111
|
53 {
|
|
145
|
54 static hashval_t hash (tree t)
|
|
111
|
55 {
|
|
145
|
56 return hash_atomic_constraint (t);
|
|
111
|
57 }
|
|
|
58
|
|
145
|
59 static bool equal (tree t1, tree t2)
|
|
111
|
60 {
|
|
145
|
61 return atomic_constraints_identical_p (t1, t2);
|
|
111
|
62 }
|
|
|
63 };
|
|
|
64
|
|
145
|
65 /* A conjunctive or disjunctive clause.
|
|
111
|
66
|
|
145
|
67 Each clause maintains an iterator that refers to the current
|
|
|
68 term, which is used in the linear decomposition of a formula
|
|
|
69 into CNF or DNF. */
|
|
|
70
|
|
|
71 struct clause
|
|
111
|
72 {
|
|
|
73 typedef std::list<tree>::iterator iterator;
|
|
145
|
74 typedef std::list<tree>::const_iterator const_iterator;
|
|
111
|
75
|
|
145
|
76 /* Initialize a clause with an initial term. */
|
|
|
77
|
|
|
78 clause (tree t)
|
|
|
79 {
|
|
|
80 m_terms.push_back (t);
|
|
|
81 if (TREE_CODE (t) == ATOMIC_CONSTR)
|
|
|
82 m_set.add (t);
|
|
|
83
|
|
|
84 m_current = m_terms.begin ();
|
|
|
85 }
|
|
|
86
|
|
|
87 /* Create a copy of the current term. The current
|
|
|
88 iterator is set to point to the same position in the
|
|
|
89 copied list of terms. */
|
|
|
90
|
|
|
91 clause (clause const& c)
|
|
|
92 : m_terms (c.m_terms), m_set (c.m_set), m_current (m_terms.begin ())
|
|
|
93 {
|
|
|
94 std::advance (m_current, std::distance (c.begin (), c.current ()));
|
|
|
95 }
|
|
|
96
|
|
|
97 /* Returns true when all terms are atoms. */
|
|
|
98
|
|
|
99 bool done () const
|
|
|
100 {
|
|
|
101 return m_current == end ();
|
|
|
102 }
|
|
|
103
|
|
|
104 /* Advance to the next term. */
|
|
|
105
|
|
|
106 void advance ()
|
|
|
107 {
|
|
|
108 gcc_assert (!done ());
|
|
|
109 ++m_current;
|
|
|
110 }
|
|
|
111
|
|
|
112 /* Replaces the current term at position ITER with T. If
|
|
|
113 T is an atomic constraint that already appears in the
|
|
|
114 clause, remove but do not replace ITER. Returns a pair
|
|
|
115 containing an iterator to the replace object or past
|
|
|
116 the erased object and a boolean value which is true if
|
|
|
117 an object was erased. */
|
|
|
118
|
|
|
119 std::pair<iterator, bool> replace (iterator iter, tree t)
|
|
|
120 {
|
|
|
121 gcc_assert (TREE_CODE (*iter) != ATOMIC_CONSTR);
|
|
|
122 if (TREE_CODE (t) == ATOMIC_CONSTR)
|
|
|
123 {
|
|
|
124 if (m_set.add (t))
|
|
|
125 return std::make_pair (m_terms.erase (iter), true);
|
|
|
126 }
|
|
|
127 *iter = t;
|
|
|
128 return std::make_pair (iter, false);
|
|
|
129 }
|
|
|
130
|
|
|
131 /* Inserts T before ITER in the list of terms. If T has
|
|
|
132 already is an atomic constraint that already appears in
|
|
|
133 the clause, no action is taken, and the current iterator
|
|
|
134 is returned. Returns a pair of an iterator to the inserted
|
|
|
135 object or ITER if no insertion occurred and a boolean
|
|
|
136 value which is true if an object was inserted. */
|
|
|
137
|
|
|
138 std::pair<iterator, bool> insert (iterator iter, tree t)
|
|
|
139 {
|
|
|
140 if (TREE_CODE (t) == ATOMIC_CONSTR)
|
|
|
141 {
|
|
|
142 if (m_set.add (t))
|
|
|
143 return std::make_pair (iter, false);
|
|
|
144 }
|
|
|
145 return std::make_pair (m_terms.insert (iter, t), true);
|
|
|
146 }
|
|
111
|
147
|
|
145
|
148 /* Replaces the current term with T. In the case where the
|
|
|
149 current term is erased (because T is redundant), update
|
|
|
150 the position of the current term to the next term. */
|
|
|
151
|
|
|
152 void replace (tree t)
|
|
|
153 {
|
|
|
154 m_current = replace (m_current, t).first;
|
|
|
155 }
|
|
|
156
|
|
|
157 /* Replace the current term with T1 and T2, in that order. */
|
|
|
158
|
|
|
159 void replace (tree t1, tree t2)
|
|
|
160 {
|
|
|
161 /* Replace the current term with t1. Ensure that iter points
|
|
|
162 to the term before which t2 will be inserted. Update the
|
|
|
163 current term as needed. */
|
|
|
164 std::pair<iterator, bool> rep = replace (m_current, t1);
|
|
|
165 if (rep.second)
|
|
|
166 m_current = rep.first;
|
|
|
167 else
|
|
|
168 ++rep.first;
|
|
|
169
|
|
|
170 /* Insert the t2. Make this the current term if we erased
|
|
|
171 the prior term. */
|
|
|
172 std::pair<iterator, bool> ins = insert (rep.first, t2);
|
|
|
173 if (rep.second && ins.second)
|
|
|
174 m_current = ins.first;
|
|
|
175 }
|
|
|
176
|
|
|
177 /* Returns true if the clause contains the term T. */
|
|
|
178
|
|
|
179 bool contains (tree t)
|
|
|
180 {
|
|
|
181 gcc_assert (TREE_CODE (t) == ATOMIC_CONSTR);
|
|
|
182 return m_set.contains (t);
|
|
|
183 }
|
|
|
184
|
|
111
|
185
|
|
145
|
186 /* Returns an iterator to the first clause in the formula. */
|
|
|
187
|
|
|
188 iterator begin ()
|
|
|
189 {
|
|
|
190 return m_terms.begin ();
|
|
|
191 }
|
|
|
192
|
|
|
193 /* Returns an iterator to the first clause in the formula. */
|
|
|
194
|
|
|
195 const_iterator begin () const
|
|
|
196 {
|
|
|
197 return m_terms.begin ();
|
|
|
198 }
|
|
|
199
|
|
|
200 /* Returns an iterator past the last clause in the formula. */
|
|
111
|
201
|
|
145
|
202 iterator end ()
|
|
|
203 {
|
|
|
204 return m_terms.end ();
|
|
|
205 }
|
|
|
206
|
|
|
207 /* Returns an iterator past the last clause in the formula. */
|
|
|
208
|
|
|
209 const_iterator end () const
|
|
|
210 {
|
|
|
211 return m_terms.end ();
|
|
|
212 }
|
|
|
213
|
|
|
214 /* Returns the current iterator. */
|
|
|
215
|
|
|
216 const_iterator current () const
|
|
|
217 {
|
|
|
218 return m_current;
|
|
|
219 }
|
|
|
220
|
|
|
221 std::list<tree> m_terms; /* The list of terms. */
|
|
|
222 hash_set<tree, false, constraint_hash> m_set; /* The set of atomic constraints. */
|
|
|
223 iterator m_current; /* The current term. */
|
|
111
|
224 };
|
|
|
225
|
|
|
226
|
|
|
227 /* A proof state owns a list of goals and tracks the
|
|
|
228 current sub-goal. The class also provides facilities
|
|
|
229 for managing subgoals and constructing term lists. */
|
|
|
230
|
|
145
|
231 struct formula
|
|
111
|
232 {
|
|
145
|
233 typedef std::list<clause>::iterator iterator;
|
|
|
234 typedef std::list<clause>::const_iterator const_iterator;
|
|
111
|
235
|
|
145
|
236 /* Construct a formula with an initial formula in a
|
|
|
237 single clause. */
|
|
111
|
238
|
|
145
|
239 formula (tree t)
|
|
|
240 {
|
|
|
241 /* This should call emplace_back(). There's a an extra copy being
|
|
|
242 invoked by using push_back(). */
|
|
|
243 m_clauses.push_back (t);
|
|
|
244 m_current = m_clauses.begin ();
|
|
|
245 }
|
|
111
|
246
|
|
145
|
247 /* Returns true when all clauses are atomic. */
|
|
|
248 bool done () const
|
|
|
249 {
|
|
|
250 return m_current == end ();
|
|
|
251 }
|
|
111
|
252
|
|
145
|
253 /* Advance to the next term. */
|
|
|
254 void advance ()
|
|
|
255 {
|
|
|
256 gcc_assert (!done ());
|
|
|
257 ++m_current;
|
|
|
258 }
|
|
111
|
259
|
|
145
|
260 /* Insert a copy of clause into the formula. This corresponds
|
|
|
261 to a distribution of one logical operation over the other. */
|
|
111
|
262
|
|
145
|
263 clause& branch ()
|
|
|
264 {
|
|
|
265 gcc_assert (!done ());
|
|
|
266 m_clauses.push_back (*m_current);
|
|
|
267 return m_clauses.back ();
|
|
|
268 }
|
|
|
269
|
|
|
270 /* Returns the position of the current clause. */
|
|
111
|
271
|
|
145
|
272 iterator current ()
|
|
|
273 {
|
|
|
274 return m_current;
|
|
|
275 }
|
|
111
|
276
|
|
145
|
277 /* Returns an iterator to the first clause in the formula. */
|
|
|
278
|
|
|
279 iterator begin ()
|
|
|
280 {
|
|
|
281 return m_clauses.begin ();
|
|
|
282 }
|
|
111
|
283
|
|
145
|
284 /* Returns an iterator to the first clause in the formula. */
|
|
|
285
|
|
|
286 const_iterator begin () const
|
|
|
287 {
|
|
|
288 return m_clauses.begin ();
|
|
|
289 }
|
|
|
290
|
|
|
291 /* Returns an iterator past the last clause in the formula. */
|
|
111
|
292
|
|
145
|
293 iterator end ()
|
|
|
294 {
|
|
|
295 return m_clauses.end ();
|
|
|
296 }
|
|
111
|
297
|
|
145
|
298 /* Returns an iterator past the last clause in the formula. */
|
|
111
|
299
|
|
145
|
300 const_iterator end () const
|
|
|
301 {
|
|
|
302 return m_clauses.end ();
|
|
|
303 }
|
|
111
|
304
|
|
145
|
305 std::list<clause> m_clauses; /* The list of clauses. */
|
|
|
306 iterator m_current; /* The current clause. */
|
|
111
|
307 };
|
|
|
308
|
|
145
|
309 void
|
|
|
310 debug (clause& c)
|
|
111
|
311 {
|
|
145
|
312 for (clause::iterator i = c.begin(); i != c.end(); ++i)
|
|
|
313 verbatim (" # %E", *i);
|
|
111
|
314 }
|
|
|
315
|
|
145
|
316 void
|
|
|
317 debug (formula& f)
|
|
111
|
318 {
|
|
145
|
319 for (formula::iterator i = f.begin(); i != f.end(); ++i)
|
|
111
|
320 {
|
|
145
|
321 verbatim ("(((");
|
|
|
322 debug (*i);
|
|
|
323 verbatim (")))");
|
|
111
|
324 }
|
|
|
325 }
|
|
|
326
|
|
145
|
327 /* The logical rules used to analyze a logical formula. The
|
|
|
328 "left" and "right" refer to the position of formula in a
|
|
|
329 sequent (as in sequent calculus). */
|
|
|
330
|
|
|
331 enum rules
|
|
|
332 {
|
|
|
333 left, right
|
|
|
334 };
|
|
|
335
|
|
|
336 /* Distribution counting. */
|
|
111
|
337
|
|
145
|
338 static inline bool
|
|
|
339 disjunction_p (tree t)
|
|
111
|
340 {
|
|
145
|
341 return TREE_CODE (t) == DISJ_CONSTR;
|
|
|
342 }
|
|
111
|
343
|
|
145
|
344 static inline bool
|
|
|
345 conjunction_p (tree t)
|
|
|
346 {
|
|
|
347 return TREE_CODE (t) == CONJ_CONSTR;
|
|
|
348 }
|
|
|
349
|
|
|
350 static inline bool
|
|
|
351 atomic_p (tree t)
|
|
|
352 {
|
|
|
353 return TREE_CODE (t) == ATOMIC_CONSTR;
|
|
111
|
354 }
|
|
|
355
|
|
145
|
356 /* Recursively count the number of clauses produced when converting T
|
|
|
357 to DNF. Returns a pair containing the number of clauses and a bool
|
|
|
358 value signifying that the the tree would be rewritten as a result of
|
|
|
359 distributing. In general, a conjunction for which this flag is set
|
|
|
360 is considered a disjunction for the purpose of counting. */
|
|
111
|
361
|
|
145
|
362 static std::pair<int, bool>
|
|
|
363 dnf_size_r (tree t)
|
|
111
|
364 {
|
|
145
|
365 if (atomic_p (t))
|
|
|
366 /* Atomic constraints produce no clauses. */
|
|
|
367 return std::make_pair (0, false);
|
|
|
368
|
|
|
369 /* For compound constraints, recursively count clauses and unpack
|
|
|
370 the results. */
|
|
|
371 tree lhs = TREE_OPERAND (t, 0);
|
|
|
372 tree rhs = TREE_OPERAND (t, 1);
|
|
|
373 std::pair<int, bool> p1 = dnf_size_r (lhs);
|
|
|
374 std::pair<int, bool> p2 = dnf_size_r (rhs);
|
|
|
375 int n1 = p1.first, n2 = p2.first;
|
|
|
376 bool d1 = p1.second, d2 = p2.second;
|
|
|
377
|
|
|
378 if (disjunction_p (t))
|
|
111
|
379 {
|
|
145
|
380 /* Matches constraints of the form P \/ Q. Disjunctions contribute
|
|
|
381 linearly to the number of constraints. When both P and Q are
|
|
|
382 disjunctions, clauses are added. When only one of P and Q
|
|
|
383 is a disjunction, an additional clause is produced. When neither
|
|
|
384 P nor Q are disjunctions, two clauses are produced. */
|
|
|
385 if (disjunction_p (lhs))
|
|
|
386 {
|
|
|
387 if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
|
|
|
388 /* Both P and Q are disjunctions. */
|
|
|
389 return std::make_pair (n1 + n2, d1 | d2);
|
|
|
390 else
|
|
|
391 /* Only LHS is a disjunction. */
|
|
|
392 return std::make_pair (1 + n1 + n2, d1 | d2);
|
|
|
393 gcc_unreachable ();
|
|
|
394 }
|
|
|
395 if (conjunction_p (lhs))
|
|
|
396 {
|
|
|
397 if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
|
|
|
398 /* Both P and Q are disjunctions. */
|
|
|
399 return std::make_pair (n1 + n2, d1 | d2);
|
|
|
400 if (disjunction_p (rhs)
|
|
|
401 || (conjunction_p (rhs) && d1 != d2)
|
|
|
402 || (atomic_p (rhs) && d1))
|
|
|
403 /* Either LHS or RHS is a disjunction. */
|
|
|
404 return std::make_pair (1 + n1 + n2, d1 | d2);
|
|
|
405 else
|
|
|
406 /* Neither LHS nor RHS is a disjunction. */
|
|
|
407 return std::make_pair (2, false);
|
|
|
408 }
|
|
|
409 if (atomic_p (lhs))
|
|
|
410 {
|
|
|
411 if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
|
|
|
412 /* Only RHS is a disjunction. */
|
|
|
413 return std::make_pair (1 + n1 + n2, d1 | d2);
|
|
|
414 else
|
|
|
415 /* Neither LHS nor RHS is a disjunction. */
|
|
|
416 return std::make_pair (2, false);
|
|
|
417 }
|
|
111
|
418 }
|
|
145
|
419 else /* conjunction_p (t) */
|
|
|
420 {
|
|
|
421 /* Matches constraints of the form P /\ Q, possibly resulting
|
|
|
422 in the distribution of one side over the other. When both
|
|
|
423 P and Q are disjunctions, the number of clauses are multiplied.
|
|
|
424 When only one of P and Q is a disjunction, the the number of
|
|
|
425 clauses are added. Otherwise, neither side is a disjunction and
|
|
|
426 no clauses are created. */
|
|
|
427 if (disjunction_p (lhs))
|
|
|
428 {
|
|
|
429 if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
|
|
|
430 /* Both P and Q are disjunctions. */
|
|
|
431 return std::make_pair (n1 * n2, true);
|
|
|
432 else
|
|
|
433 /* Only LHS is a disjunction. */
|
|
|
434 return std::make_pair (n1 + n2, true);
|
|
|
435 gcc_unreachable ();
|
|
|
436 }
|
|
|
437 if (conjunction_p (lhs))
|
|
|
438 {
|
|
|
439 if ((disjunction_p (rhs) && d1) || (conjunction_p (rhs) && d1 && d2))
|
|
|
440 /* Both P and Q are disjunctions. */
|
|
|
441 return std::make_pair (n1 * n2, true);
|
|
|
442 if (disjunction_p (rhs)
|
|
|
443 || (conjunction_p (rhs) && d1 != d2)
|
|
|
444 || (atomic_p (rhs) && d1))
|
|
|
445 /* Either LHS or RHS is a disjunction. */
|
|
|
446 return std::make_pair (n1 + n2, true);
|
|
|
447 else
|
|
|
448 /* Neither LHS nor RHS is a disjunction. */
|
|
|
449 return std::make_pair (0, false);
|
|
|
450 }
|
|
|
451 if (atomic_p (lhs))
|
|
|
452 {
|
|
|
453 if (disjunction_p (rhs) || (conjunction_p (rhs) && d2))
|
|
|
454 /* Only RHS is a disjunction. */
|
|
|
455 return std::make_pair (n1 + n2, true);
|
|
|
456 else
|
|
|
457 /* Neither LHS nor RHS is a disjunction. */
|
|
|
458 return std::make_pair (0, false);
|
|
|
459 }
|
|
|
460 }
|
|
|
461 gcc_unreachable ();
|
|
111
|
462 }
|
|
|
463
|
|
145
|
464 /* Recursively count the number of clauses produced when converting T
|
|
|
465 to CNF. Returns a pair containing the number of clauses and a bool
|
|
|
466 value signifying that the the tree would be rewritten as a result of
|
|
|
467 distributing. In general, a disjunction for which this flag is set
|
|
|
468 is considered a conjunction for the purpose of counting. */
|
|
111
|
469
|
|
145
|
470 static std::pair<int, bool>
|
|
|
471 cnf_size_r (tree t)
|
|
111
|
472 {
|
|
145
|
473 if (atomic_p (t))
|
|
|
474 /* Atomic constraints produce no clauses. */
|
|
|
475 return std::make_pair (0, false);
|
|
|
476
|
|
|
477 /* For compound constraints, recursively count clauses and unpack
|
|
|
478 the results. */
|
|
|
479 tree lhs = TREE_OPERAND (t, 0);
|
|
|
480 tree rhs = TREE_OPERAND (t, 1);
|
|
|
481 std::pair<int, bool> p1 = cnf_size_r (lhs);
|
|
|
482 std::pair<int, bool> p2 = cnf_size_r (rhs);
|
|
|
483 int n1 = p1.first, n2 = p2.first;
|
|
|
484 bool d1 = p1.second, d2 = p2.second;
|
|
111
|
485
|
|
145
|
486 if (disjunction_p (t))
|
|
|
487 {
|
|
|
488 /* Matches constraints of the form P \/ Q, possibly resulting
|
|
|
489 in the distribution of one side over the other. When both
|
|
|
490 P and Q are conjunctions, the number of clauses are multiplied.
|
|
|
491 When only one of P and Q is a conjunction, the the number of
|
|
|
492 clauses are added. Otherwise, neither side is a conjunction and
|
|
|
493 no clauses are created. */
|
|
|
494 if (disjunction_p (lhs))
|
|
|
495 {
|
|
|
496 if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
|
|
|
497 /* Both P and Q are conjunctions. */
|
|
|
498 return std::make_pair (n1 * n2, true);
|
|
|
499 if ((disjunction_p (rhs) && d1 != d2)
|
|
|
500 || conjunction_p (rhs)
|
|
|
501 || (atomic_p (rhs) && d1))
|
|
|
502 /* Either LHS or RHS is a conjunction. */
|
|
|
503 return std::make_pair (n1 + n2, true);
|
|
|
504 else
|
|
|
505 /* Neither LHS nor RHS is a conjunction. */
|
|
|
506 return std::make_pair (0, false);
|
|
|
507 gcc_unreachable ();
|
|
|
508 }
|
|
|
509 if (conjunction_p (lhs))
|
|
|
510 {
|
|
|
511 if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
|
|
|
512 /* Both LHS and RHS are conjunctions. */
|
|
|
513 return std::make_pair (n1 * n2, true);
|
|
|
514 else
|
|
|
515 /* Only LHS is a conjunction. */
|
|
|
516 return std::make_pair (n1 + n2, true);
|
|
|
517 }
|
|
|
518 if (atomic_p (lhs))
|
|
|
519 {
|
|
|
520 if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
|
|
|
521 /* Only RHS is a disjunction. */
|
|
|
522 return std::make_pair (n1 + n2, true);
|
|
|
523 else
|
|
|
524 /* Neither LHS nor RHS is a disjunction. */
|
|
|
525 return std::make_pair (0, false);
|
|
|
526 }
|
|
|
527 }
|
|
|
528 else /* conjunction_p (t) */
|
|
|
529 {
|
|
|
530 /* Matches constraints of the form P /\ Q. Conjunctions contribute
|
|
|
531 linearly to the number of constraints. When both P and Q are
|
|
|
532 conjunctions, clauses are added. When only one of P and Q
|
|
|
533 is a conjunction, an additional clause is produced. When neither
|
|
|
534 P nor Q are conjunctions, two clauses are produced. */
|
|
|
535 if (disjunction_p (lhs))
|
|
|
536 {
|
|
|
537 if ((disjunction_p (rhs) && d1 && d2) || (conjunction_p (rhs) && d1))
|
|
|
538 /* Both P and Q are conjunctions. */
|
|
|
539 return std::make_pair (n1 + n2, d1 | d2);
|
|
|
540 if ((disjunction_p (rhs) && d1 != d2)
|
|
|
541 || conjunction_p (rhs)
|
|
|
542 || (atomic_p (rhs) && d1))
|
|
|
543 /* Either LHS or RHS is a conjunction. */
|
|
|
544 return std::make_pair (1 + n1 + n2, d1 | d2);
|
|
|
545 else
|
|
|
546 /* Neither LHS nor RHS is a conjunction. */
|
|
|
547 return std::make_pair (2, false);
|
|
|
548 gcc_unreachable ();
|
|
|
549 }
|
|
|
550 if (conjunction_p (lhs))
|
|
|
551 {
|
|
|
552 if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
|
|
|
553 /* Both LHS and RHS are conjunctions. */
|
|
|
554 return std::make_pair (n1 + n2, d1 | d2);
|
|
|
555 else
|
|
|
556 /* Only LHS is a conjunction. */
|
|
|
557 return std::make_pair (1 + n1 + n2, d1 | d2);
|
|
|
558 }
|
|
|
559 if (atomic_p (lhs))
|
|
|
560 {
|
|
|
561 if ((disjunction_p (rhs) && d2) || conjunction_p (rhs))
|
|
|
562 /* Only RHS is a disjunction. */
|
|
|
563 return std::make_pair (1 + n1 + n2, d1 | d2);
|
|
|
564 else
|
|
|
565 /* Neither LHS nor RHS is a disjunction. */
|
|
|
566 return std::make_pair (2, false);
|
|
|
567 }
|
|
|
568 }
|
|
|
569 gcc_unreachable ();
|
|
111
|
570 }
|
|
|
571
|
|
145
|
572 /* Count the number conjunctive clauses that would be created
|
|
|
573 when rewriting T to DNF. */
|
|
|
574
|
|
|
575 static int
|
|
|
576 dnf_size (tree t)
|
|
111
|
577 {
|
|
145
|
578 std::pair<int, bool> result = dnf_size_r (t);
|
|
|
579 return result.first == 0 ? 1 : result.first;
|
|
111
|
580 }
|
|
|
581
|
|
145
|
582
|
|
|
583 /* Count the number disjunctive clauses that would be created
|
|
|
584 when rewriting T to CNF. */
|
|
|
585
|
|
|
586 static int
|
|
|
587 cnf_size (tree t)
|
|
|
588 {
|
|
|
589 std::pair<int, bool> result = cnf_size_r (t);
|
|
|
590 return result.first == 0 ? 1 : result.first;
|
|
|
591 }
|
|
|
592
|
|
|
593
|
|
|
594 /* A left-conjunction is replaced by its operands. */
|
|
|
595
|
|
|
596 void
|
|
|
597 replace_term (clause& c, tree t)
|
|
|
598 {
|
|
|
599 tree t1 = TREE_OPERAND (t, 0);
|
|
|
600 tree t2 = TREE_OPERAND (t, 1);
|
|
|
601 return c.replace (t1, t2);
|
|
|
602 }
|
|
|
603
|
|
|
604 /* Create a new clause in the formula by copying the current
|
|
|
605 clause. In the current clause, the term at CI is replaced
|
|
|
606 by the first operand, and in the new clause, it is replaced
|
|
|
607 by the second. */
|
|
111
|
608
|
|
|
609 void
|
|
145
|
610 branch_clause (formula& f, clause& c1, tree t)
|
|
111
|
611 {
|
|
145
|
612 tree t1 = TREE_OPERAND (t, 0);
|
|
|
613 tree t2 = TREE_OPERAND (t, 1);
|
|
|
614 clause& c2 = f.branch ();
|
|
|
615 c1.replace (t1);
|
|
|
616 c2.replace (t2);
|
|
|
617 }
|
|
|
618
|
|
|
619 /* Decompose t1 /\ t2 according to the rules R. */
|
|
|
620
|
|
|
621 inline void
|
|
|
622 decompose_conjuntion (formula& f, clause& c, tree t, rules r)
|
|
|
623 {
|
|
|
624 if (r == left)
|
|
|
625 replace_term (c, t);
|
|
|
626 else
|
|
|
627 branch_clause (f, c, t);
|
|
111
|
628 }
|
|
|
629
|
|
145
|
630 /* Decompose t1 \/ t2 according to the rules R. */
|
|
|
631
|
|
|
632 inline void
|
|
|
633 decompose_disjunction (formula& f, clause& c, tree t, rules r)
|
|
|
634 {
|
|
|
635 if (r == right)
|
|
|
636 replace_term (c, t);
|
|
|
637 else
|
|
|
638 branch_clause (f, c, t);
|
|
|
639 }
|
|
|
640
|
|
|
641 /* An atomic constraint is already decomposed. */
|
|
|
642 inline void
|
|
|
643 decompose_atom (clause& c)
|
|
|
644 {
|
|
|
645 c.advance ();
|
|
|
646 }
|
|
|
647
|
|
|
648 /* Decompose a term of clause C (in formula F) according to the
|
|
|
649 logical rules R. */
|
|
111
|
650
|
|
|
651 void
|
|
145
|
652 decompose_term (formula& f, clause& c, tree t, rules r)
|
|
111
|
653 {
|
|
145
|
654 switch (TREE_CODE (t))
|
|
111
|
655 {
|
|
145
|
656 case CONJ_CONSTR:
|
|
|
657 return decompose_conjuntion (f, c, t, r);
|
|
|
658 case DISJ_CONSTR:
|
|
|
659 return decompose_disjunction (f, c, t, r);
|
|
|
660 default:
|
|
|
661 return decompose_atom (c);
|
|
111
|
662 }
|
|
|
663 }
|
|
|
664
|
|
145
|
665 /* Decompose C (in F) using the logical rules R until it
|
|
|
666 is comprised of only atomic constraints. */
|
|
|
667
|
|
111
|
668 void
|
|
145
|
669 decompose_clause (formula& f, clause& c, rules r)
|
|
111
|
670 {
|
|
145
|
671 while (!c.done ())
|
|
|
672 decompose_term (f, c, *c.current (), r);
|
|
|
673 f.advance ();
|
|
|
674 }
|
|
|
675
|
|
|
676 /* Decompose the logical formula F according to the logical
|
|
|
677 rules determined by R. The result is a formula containing
|
|
|
678 clauses that contain only atomic terms. */
|
|
|
679
|
|
|
680 void
|
|
|
681 decompose_formula (formula& f, rules r)
|
|
|
682 {
|
|
|
683 while (!f.done ())
|
|
|
684 decompose_clause (f, *f.current (), r);
|
|
|
685 }
|
|
|
686
|
|
|
687 /* Fully decomposing T into a list of sequents, each comprised of
|
|
|
688 a list of atomic constraints, as if T were an antecedent. */
|
|
111
|
689
|
|
145
|
690 static formula
|
|
|
691 decompose_antecedents (tree t)
|
|
|
692 {
|
|
|
693 formula f (t);
|
|
|
694 decompose_formula (f, left);
|
|
|
695 return f;
|
|
|
696 }
|
|
|
697
|
|
|
698 /* Fully decomposing T into a list of sequents, each comprised of
|
|
|
699 a list of atomic constraints, as if T were a consequent. */
|
|
111
|
700
|
|
145
|
701 static formula
|
|
|
702 decompose_consequents (tree t)
|
|
|
703 {
|
|
|
704 formula f (t);
|
|
|
705 decompose_formula (f, right);
|
|
|
706 return f;
|
|
|
707 }
|
|
111
|
708
|
|
145
|
709 static bool derive_proof (clause&, tree, rules);
|
|
|
710
|
|
|
711 /* Derive a proof of both operands of T. */
|
|
|
712
|
|
|
713 static bool
|
|
|
714 derive_proof_for_both_operands (clause& c, tree t, rules r)
|
|
|
715 {
|
|
|
716 if (!derive_proof (c, TREE_OPERAND (t, 0), r))
|
|
|
717 return false;
|
|
|
718 return derive_proof (c, TREE_OPERAND (t, 1), r);
|
|
111
|
719 }
|
|
|
720
|
|
145
|
721 /* Derive a proof of either operand of T. */
|
|
111
|
722
|
|
145
|
723 static bool
|
|
|
724 derive_proof_for_either_operand (clause& c, tree t, rules r)
|
|
|
725 {
|
|
|
726 if (derive_proof (c, TREE_OPERAND (t, 0), r))
|
|
|
727 return true;
|
|
|
728 return derive_proof (c, TREE_OPERAND (t, 1), r);
|
|
|
729 }
|
|
111
|
730
|
|
145
|
731 /* Derive a proof of the atomic constraint T in clause C. */
|
|
|
732
|
|
|
733 static bool
|
|
|
734 derive_atomic_proof (clause& c, tree t)
|
|
|
735 {
|
|
|
736 return c.contains (t);
|
|
|
737 }
|
|
|
738
|
|
|
739 /* Derive a proof of T from the terms in C. */
|
|
|
740
|
|
|
741 static bool
|
|
|
742 derive_proof (clause& c, tree t, rules r)
|
|
111
|
743 {
|
|
145
|
744 switch (TREE_CODE (t))
|
|
|
745 {
|
|
|
746 case CONJ_CONSTR:
|
|
|
747 if (r == left)
|
|
|
748 return derive_proof_for_both_operands (c, t, r);
|
|
|
749 else
|
|
|
750 return derive_proof_for_either_operand (c, t, r);
|
|
|
751 case DISJ_CONSTR:
|
|
|
752 if (r == left)
|
|
|
753 return derive_proof_for_either_operand (c, t, r);
|
|
|
754 else
|
|
|
755 return derive_proof_for_both_operands (c, t, r);
|
|
|
756 default:
|
|
|
757 return derive_atomic_proof (c, t);
|
|
|
758 }
|
|
|
759 }
|
|
|
760
|
|
|
761 /* Derive a proof of T from disjunctive clauses in F. */
|
|
|
762
|
|
|
763 static bool
|
|
|
764 derive_proofs (formula& f, tree t, rules r)
|
|
|
765 {
|
|
|
766 for (formula::iterator i = f.begin(); i != f.end(); ++i)
|
|
|
767 if (!derive_proof (*i, t, r))
|
|
|
768 return false;
|
|
|
769 return true;
|
|
|
770 }
|
|
|
771
|
|
|
772 /* The largest number of clauses in CNF or DNF we accept as input
|
|
|
773 for subsumption. This an upper bound of 2^16 expressions. */
|
|
|
774 static int max_problem_size = 16;
|
|
|
775
|
|
|
776 static inline bool
|
|
|
777 diagnose_constraint_size (tree t)
|
|
|
778 {
|
|
|
779 error_at (input_location, "%qE exceeds the maximum constraint complexity", t);
|
|
111
|
780 return false;
|
|
|
781 }
|
|
|
782
|
|
145
|
783 /* Key/value pair for caching subsumption results. This associates a pair of
|
|
|
784 constraints with a boolean value indicating the result. */
|
|
111
|
785
|
|
145
|
786 struct GTY((for_user)) subsumption_entry
|
|
111
|
787 {
|
|
145
|
788 tree lhs;
|
|
|
789 tree rhs;
|
|
|
790 bool result;
|
|
|
791 };
|
|
|
792
|
|
|
793 /* Hashing function and equality for constraint entries. */
|
|
111
|
794
|
|
145
|
795 struct subsumption_hasher : ggc_ptr_hash<subsumption_entry>
|
|
|
796 {
|
|
|
797 static hashval_t hash (subsumption_entry *e)
|
|
|
798 {
|
|
|
799 hashval_t val = 0;
|
|
|
800 val = iterative_hash_constraint (e->lhs, val);
|
|
|
801 val = iterative_hash_constraint (e->rhs, val);
|
|
|
802 return val;
|
|
|
803 }
|
|
111
|
804
|
|
145
|
805 static bool equal (subsumption_entry *e1, subsumption_entry *e2)
|
|
|
806 {
|
|
|
807 if (!constraints_equivalent_p (e1->lhs, e2->lhs))
|
|
|
808 return false;
|
|
|
809 if (!constraints_equivalent_p (e1->rhs, e2->rhs))
|
|
|
810 return false;
|
|
|
811 return true;
|
|
|
812 }
|
|
|
813 };
|
|
111
|
814
|
|
145
|
815 /* Caches the results of subsumes_non_null(t1, t1). */
|
|
|
816
|
|
|
817 static GTY ((deletable)) hash_table<subsumption_hasher> *subsumption_cache;
|
|
111
|
818
|
|
145
|
819 /* Search for a previously cached subsumption result. */
|
|
|
820
|
|
|
821 static bool*
|
|
|
822 lookup_subsumption (tree t1, tree t2)
|
|
111
|
823 {
|
|
145
|
824 if (!subsumption_cache)
|
|
|
825 return NULL;
|
|
|
826 subsumption_entry elt = { t1, t2, false };
|
|
|
827 subsumption_entry* found = subsumption_cache->find (&elt);
|
|
|
828 if (found)
|
|
|
829 return &found->result;
|
|
|
830 else
|
|
|
831 return 0;
|
|
111
|
832 }
|
|
|
833
|
|
145
|
834 /* Save a subsumption result. */
|
|
|
835
|
|
|
836 static bool
|
|
|
837 save_subsumption (tree t1, tree t2, bool result)
|
|
111
|
838 {
|
|
145
|
839 if (!subsumption_cache)
|
|
|
840 subsumption_cache = hash_table<subsumption_hasher>::create_ggc(31);
|
|
|
841 subsumption_entry elt = {t1, t2, result};
|
|
|
842 subsumption_entry** slot = subsumption_cache->find_slot (&elt, INSERT);
|
|
|
843 subsumption_entry* entry = ggc_alloc<subsumption_entry> ();
|
|
|
844 *entry = elt;
|
|
|
845 *slot = entry;
|
|
|
846 return result;
|
|
111
|
847 }
|
|
|
848
|
|
|
849
|
|
|
850 /* Returns true if the LEFT constraint subsume the RIGHT constraints.
|
|
|
851 This is done by deriving a proof of the conclusions on the RIGHT
|
|
|
852 from the assumptions on the LEFT assumptions. */
|
|
|
853
|
|
145
|
854 static bool
|
|
|
855 subsumes_constraints_nonnull (tree lhs, tree rhs)
|
|
111
|
856 {
|
|
|
857 auto_timevar time (TV_CONSTRAINT_SUB);
|
|
145
|
858
|
|
|
859 if (bool *b = lookup_subsumption(lhs, rhs))
|
|
|
860 return *b;
|
|
|
861
|
|
|
862 int n1 = dnf_size (lhs);
|
|
|
863 int n2 = cnf_size (rhs);
|
|
|
864
|
|
|
865 /* Make sure we haven't exceeded the largest acceptable problem. */
|
|
|
866 if (std::min (n1, n2) >= max_problem_size)
|
|
|
867 {
|
|
|
868 if (n1 < n2)
|
|
|
869 diagnose_constraint_size (lhs);
|
|
|
870 else
|
|
|
871 diagnose_constraint_size (rhs);
|
|
|
872 return false;
|
|
|
873 }
|
|
|
874
|
|
|
875 /* Decompose the smaller of the two formulas, and recursively
|
|
|
876 check for implication of the larger. */
|
|
|
877 bool result;
|
|
|
878 if (n1 <= n2)
|
|
|
879 {
|
|
|
880 formula dnf = decompose_antecedents (lhs);
|
|
|
881 result = derive_proofs (dnf, rhs, left);
|
|
|
882 }
|
|
|
883 else
|
|
|
884 {
|
|
|
885 formula cnf = decompose_consequents (rhs);
|
|
|
886 result = derive_proofs (cnf, lhs, right);
|
|
|
887 }
|
|
|
888
|
|
|
889 return save_subsumption (lhs, rhs, result);
|
|
111
|
890 }
|
|
|
891
|
|
|
892 /* Returns true if the LEFT constraints subsume the RIGHT
|
|
|
893 constraints. */
|
|
|
894
|
|
|
895 bool
|
|
145
|
896 subsumes (tree lhs, tree rhs)
|
|
111
|
897 {
|
|
145
|
898 if (lhs == rhs)
|
|
111
|
899 return true;
|
|
145
|
900 if (!lhs || lhs == error_mark_node)
|
|
111
|
901 return false;
|
|
145
|
902 if (!rhs || rhs == error_mark_node)
|
|
111
|
903 return true;
|
|
145
|
904 return subsumes_constraints_nonnull (lhs, rhs);
|
|
111
|
905 }
|
|
145
|
906
|
|
|
907 #include "gt-cp-logic.h"
|
