aboutsummaryrefslogtreecommitdiff
path: root/gcc/cp/logic.cc
blob: e432c5774971edaea13c5edfc5210d56bd0022d4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
/* Derivation and subsumption rules for constraints.
   Copyright (C) 2013-2022 Free Software Foundation, Inc.
   Contributed by Andrew Sutton (andrew.n.sutton@gmail.com)

This file is part of GCC.

GCC is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 3, or (at your option)
any later version.

GCC is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with GCC; see the file COPYING3.  If not see
<http://www.gnu.org/licenses/>.  */

#include "config.h"
#define INCLUDE_LIST
#include "system.h"
#include "coretypes.h"
#include "tm.h"
#include "timevar.h"
#include "hash-set.h"
#include "machmode.h"
#include "vec.h"
#include "double-int.h"
#include "input.h"
#include "alias.h"
#include "symtab.h"
#include "wide-int.h"
#include "inchash.h"
#include "tree.h"
#include "stringpool.h"
#include "attribs.h"
#include "intl.h"
#include "flags.h"
#include "cp-tree.h"
#include "c-family/c-common.h"
#include "c-family/c-objc.h"
#include "cp-objcp-common.h"
#include "tree-inline.h"
#include "decl.h"
#include "toplev.h"
#include "type-utils.h"

/* A conjunctive or disjunctive clause.

   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 clause
{
  typedef std::list<tree>::iterator iterator;
  typedef std::list<tree>::const_iterator const_iterator;

  /* Initialize a clause with an initial term.  */

  clause (tree t)
  {
    m_terms.push_back (t);
    if (TREE_CODE (t) == ATOMIC_CONSTR)
      m_set.add (t);

    m_current = m_terms.begin ();
  }

  /* 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 ())
  {
    std::advance (m_current, std::distance (c.begin (), c.current ()));
  }

  /* Returns true when all terms are atoms.  */

  bool done () const
  {
    return m_current == end ();
  }

  /* Advance to the next term.  */

  void advance ()
  {
    gcc_assert (!done ());
    ++m_current;
  }

  /* 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::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);
  }

  /* 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.  */

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

  /* 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.  */

  void replace (tree t)
  {
    m_current = replace (m_current, t).first;
  }

  /* Replace the current term with T1 and T2, in that order.  */

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

  /* Returns true if the clause contains the term T.  */

  bool contains (tree t)
  {
    gcc_assert (TREE_CODE (t) == ATOMIC_CONSTR);
    return m_set.contains (t);
  }


  /* Returns an iterator to the first clause in the formula.  */

  iterator begin ()
  {
    return m_terms.begin ();
  }

  /* Returns an iterator to the first clause in the formula.  */

  const_iterator begin () const
  {
    return m_terms.begin ();
  }

  /* Returns an iterator past the last clause in the formula.  */

  iterator end ()
  {
    return m_terms.end ();
  }

  /* Returns an iterator past the last clause in the formula.  */

  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, atom_hasher> 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. */

struct formula
{
  typedef std::list<clause>::iterator iterator;
  typedef std::list<clause>::const_iterator const_iterator;

  /* Construct a formula with an initial formula in a
     single clause.  */

  formula (tree t)
  {
    m_clauses.emplace_back (t);
    m_current = m_clauses.begin ();
  }

  /* Returns true when all clauses are atomic.  */
  bool done () const
  {
    return m_current == end ();
  }

  /* Advance to the next term.  */
  void advance ()
  {
    gcc_assert (!done ());
    ++m_current;
  }

  /* Insert a copy of clause into the formula. This corresponds
     to a distribution of one logical operation over the other.  */

  clause& branch ()
  {
    gcc_assert (!done ());
    return *m_clauses.insert (std::next (m_current), *m_current);
  }

  /* Returns the position of the current clause.  */

  iterator current ()
  {
    return m_current;
  }

  /* Returns an iterator to the first clause in the formula.  */

  iterator begin ()
  {
    return m_clauses.begin ();
  }

  /* Returns an iterator to the first clause in the formula.  */

  const_iterator begin () const
  {
    return m_clauses.begin ();
  }

  /* Returns an iterator past the last clause in the formula.  */

  iterator end ()
  {
    return m_clauses.end ();
  }

  /* Returns an iterator past the last clause in the formula.  */

  const_iterator end () const
  {
    return m_clauses.end ();
  }

  /* Remove the specified clause from the formula.  */

  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.  */
};

void
debug (clause& c)
{
  for (clause::iterator i = c.begin(); i != c.end(); ++i)
    verbatim ("  # %E", *i);
}

void
debug (formula& f)
{
  for (formula::iterator i = f.begin(); i != f.end(); ++i)
    {
      /* Format punctuators via %s to avoid -Wformat-diag.  */
      verbatim ("%s", "(((");
      debug (*i);
      verbatim ("%s", ")))");
    }
}

/* 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).  */

enum rules
{
  left, right
};

/* Distribution counting.  */

static inline bool
disjunction_p (tree t)
{
  return TREE_CODE (t) == DISJ_CONSTR;
}

static inline bool
conjunction_p (tree t)
{
  return TREE_CODE (t) == CONJ_CONSTR;
}

static inline bool
atomic_p (tree t)
{
  return TREE_CODE (t) == ATOMIC_CONSTR;
}

/* 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 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.  */

static std::pair<int, bool>
dnf_size_r (tree t)
{
  if (atomic_p (t))
    /* Atomic constraints produce no clauses.  */
    return std::make_pair (0, false);

  /* 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;

  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 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 ();
}

/* 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 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.  */

static std::pair<int, bool>
cnf_size_r (tree t)
{
  if (atomic_p (t))
    /* Atomic constraints produce no clauses.  */
    return std::make_pair (0, false);

  /* 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;

  if (disjunction_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 conjunctions, the number of clauses are multiplied.
	 When only one of P and Q is a conjunction, 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);
	}
      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);
	}
    }
  else /* conjunction_p (t)  */
    {
      /* 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);
	}
      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);
	}
    }
  gcc_unreachable ();
}

/* Count the number conjunctive clauses that would be created
   when rewriting T to DNF. */

static int
dnf_size (tree t)
{
  std::pair<int, bool> result = dnf_size_r (t);
  return result.first == 0 ? 1 : result.first;
}


/* Count the number disjunctive clauses that would be created
   when rewriting T to CNF. */

static int
cnf_size (tree t)
{
  std::pair<int, bool> result = cnf_size_r (t);
  return result.first == 0 ? 1 : result.first;
}


/* A left-conjunction is replaced by its operands.  */

void
replace_term (clause& c, tree t)
{
  tree t1 = TREE_OPERAND (t, 0);
  tree t2 = TREE_OPERAND (t, 1);
  return c.replace (t1, t2);
}

/* 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
branch_clause (formula& f, clause& c1, tree t)
{
  tree t1 = TREE_OPERAND (t, 0);
  tree t2 = TREE_OPERAND (t, 1);
  clause& c2 = f.branch ();
  c1.replace (t1);
  c2.replace (t2);
}

/* Decompose t1 /\ t2 according to the rules R.  */

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

/* Decompose t1 \/ t2 according to the rules R.  */

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 ();
}

/* Decompose a term of clause C (in formula F) according to the
   logical rules R. */

void
decompose_term (formula& f, clause& c, tree t, rules r)
{
  switch (TREE_CODE (t))
    {
      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);
    }
}

/* Decompose C (in F) using the logical rules R until it
   is comprised of only atomic constraints.  */

void
decompose_clause (formula& f, clause& c, rules r)
{
  while (!c.done ())
    decompose_term (f, c, *c.current (), r);
  f.advance ();
}

static bool derive_proof (clause&, tree, rules);

/* Derive a proof of both operands of T.  */

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

/* Derive a proof of either operand of T.  */

static bool
derive_proof_for_either_operand (clause& c, tree t, rules r)
{
  if (derive_proof (c, TREE_OPERAND (t, 0), r))
    return true;
  return derive_proof (c, TREE_OPERAND (t, 1), r);
}

/* Derive a proof of the atomic constraint T in clause C.  */

static bool
derive_atomic_proof (clause& c, tree t)
{
  return c.contains (t);
}

/* Derive a proof of T from the terms in C.  */

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

/* Key/value pair for caching subsumption results. This associates a pair of
   constraints with a boolean value indicating the result.  */

struct GTY((for_user)) subsumption_entry
{
  tree lhs;
  tree rhs;
  bool result;
};

/* Hashing function and equality for constraint entries.  */

struct subsumption_hasher : ggc_ptr_hash<subsumption_entry>
{
  static hashval_t hash (subsumption_entry *e)
  {
    hashval_t val = 0;
    val = iterative_hash_constraint (e->lhs, val);
    val = iterative_hash_constraint (e->rhs, val);
    return val;
  }

  static bool equal (subsumption_entry *e1, subsumption_entry *e2)
  {
    if (!constraints_equivalent_p (e1->lhs, e2->lhs))
      return false;
    if (!constraints_equivalent_p (e1->rhs, e2->rhs))
      return false;
    return true;
  }
};

/* Caches the results of subsumes_non_null(t1, t1).  */

static GTY ((deletable)) hash_table<subsumption_hasher> *subsumption_cache;

/* Search for a previously cached subsumption result. */

static bool*
lookup_subsumption (tree t1, tree t2)
{
  if (!subsumption_cache)
    return NULL;
  subsumption_entry elt = { t1, t2, false };
  subsumption_entry* found = subsumption_cache->find (&elt);
  if (found)
    return &found->result;
  else
    return 0;
}

/* Save a subsumption result. */

static bool
save_subsumption (tree t1, tree t2, bool result)
{
  if (!subsumption_cache)
    subsumption_cache = hash_table<subsumption_hasher>::create_ggc(31);
  subsumption_entry elt = {t1, t2, result};
  subsumption_entry** slot = subsumption_cache->find_slot (&elt, INSERT);
  subsumption_entry* entry = ggc_alloc<subsumption_entry> ();
  *entry = elt;
  *slot = entry;
  return result;
}


/* Returns true if the LEFT constraint subsume the RIGHT constraints.
   This is done by deriving a proof of the conclusions on the RIGHT
   from the assumptions on the LEFT assumptions.  */

static bool
subsumes_constraints_nonnull (tree lhs, tree rhs)
{
  auto_timevar time (TV_CONSTRAINT_SUB);

  if (bool *b = lookup_subsumption(lhs, rhs))
    return *b;

  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 in the decomposed LHS 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
       in the decomposed RHS 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 ())
    {
      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);
}

/* Returns true if the LEFT constraints subsume the RIGHT
   constraints.  */

bool
subsumes (tree lhs, tree rhs)
{
  if (lhs == rhs)
    return true;
  if (!lhs || lhs == error_mark_node)
    return false;
  if (!rhs || rhs == error_mark_node)
    return true;
  return subsumes_constraints_nonnull (lhs, rhs);
}

#include "gt-cp-logic.h"