GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/candidate_generator.cpp Lines: 172 179 96.1 %
Date: 2021-03-22 Branches: 339 794 42.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file candidate_generator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implementation of theory uf candidate generator class
13
 **/
14
15
#include "theory/quantifiers/ematching/candidate_generator.h"
16
#include "expr/dtype.h"
17
#include "expr/dtype_cons.h"
18
#include "options/quantifiers_options.h"
19
#include "smt/smt_engine.h"
20
#include "smt/smt_engine_scope.h"
21
#include "theory/quantifiers/inst_match.h"
22
#include "theory/quantifiers/instantiate.h"
23
#include "theory/quantifiers/quantifiers_state.h"
24
#include "theory/quantifiers/term_database.h"
25
#include "theory/quantifiers/term_util.h"
26
#include "theory/quantifiers_engine.h"
27
28
using namespace CVC4::kind;
29
30
namespace CVC4 {
31
namespace theory {
32
namespace inst {
33
34
3860620
bool CandidateGenerator::isLegalCandidate( Node n ){
35
3860620
  return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
36
}
37
38
32595
CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
39
    : CandidateGenerator(qe),
40
      d_term_iter(-1),
41
      d_term_iter_limit(0),
42
32595
      d_mode(cand_term_none)
43
{
44
32595
  d_op = qe->getTermDatabase()->getMatchOperator( pat );
45
32595
  Assert(!d_op.isNull());
46
32595
}
47
48
585844
void CandidateGeneratorQE::reset(Node eqc) { resetForOperator(eqc, d_op); }
49
50
587761
void CandidateGeneratorQE::resetForOperator(Node eqc, Node op)
51
{
52
587761
  d_term_iter = 0;
53
587761
  d_eqc = eqc;
54
587761
  d_op = op;
55
587761
  d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms(d_op);
56
587761
  if( eqc.isNull() ){
57
116120
    d_mode = cand_term_db;
58
  }else{
59
471641
    if( isExcludedEqc( eqc ) ){
60
      d_mode = cand_term_none;
61
    }else{
62
471641
      eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
63
471641
      if( ee->hasTerm( eqc ) ){
64
471641
        TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, op);
65
471641
        if( tat ){
66
          //create an equivalence class iterator in eq class eqc
67
438046
          Node rep = ee->getRepresentative( eqc );
68
219023
          d_eqc_iter = eq::EqClassIterator( rep, ee );
69
219023
          d_mode = cand_term_eqc;
70
        }else{
71
252618
          d_mode = cand_term_none;
72
        }
73
      }else{
74
        //the only match is this term itself
75
        d_mode = cand_term_ident;
76
      }
77
    }
78
  }
79
587761
}
80
995061
bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) {
81
995061
  if( n.hasOperator() ){
82
724112
    if( isLegalCandidate( n ) ){
83
393782
      return d_qe->getTermDatabase()->getMatchOperator( n )==d_op;
84
    }
85
  }
86
601279
  return false;
87
}
88
89
3442595
Node CandidateGeneratorQE::getNextCandidate(){
90
3442595
  return getNextCandidateInternal();
91
}
92
93
3448218
Node CandidateGeneratorQE::getNextCandidateInternal()
94
{
95
3448218
  if( d_mode==cand_term_db ){
96
2751281
    quantifiers::QuantifiersState& qs = d_qe->getState();
97
2751281
    Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl;
98
    //get next candidate term in the uf term database
99
3667989
    while( d_term_iter<d_term_iter_limit ){
100
3593254
      Node n = d_qe->getTermDatabase()->getGroundTerm( d_op, d_term_iter );
101
3134900
      d_term_iter++;
102
3134900
      if( isLegalCandidate( n ) ){
103
2697423
        if( d_qe->getTermDatabase()->hasTermCurrent( n ) ){
104
2697423
          if( d_exclude_eqc.empty() ){
105
2607402
            return n;
106
          }else{
107
110898
            Node r = qs.getRepresentative(n);
108
90021
            if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){
109
69144
              Debug("cand-gen-qe") << "...returning " << n << std::endl;
110
69144
              return n;
111
            }
112
          }
113
        }
114
      }
115
    }
116
696937
  }else if( d_mode==cand_term_eqc ){
117
441942
    Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl;
118
1776208
    while( !d_eqc_iter.isFinished() ){
119
1662194
      Node n = *d_eqc_iter;
120
995061
      ++d_eqc_iter;
121
995061
      if( isLegalOpCandidate( n ) ){
122
327928
        Debug("cand-gen-qe") << "...returning " << n << std::endl;
123
327928
        return n;
124
      }
125
    }
126
254995
  }else if( d_mode==cand_term_ident ){
127
2377
    Debug("cand-gen-qe") << "...get next candidate identity" << std::endl;
128
2377
    if (!d_eqc.isNull())
129
    {
130
1669
      Node n = d_eqc;
131
1568
      d_eqc = Node::null();
132
1568
      if( isLegalOpCandidate( n ) ){
133
1467
        return n;
134
      }
135
    }
136
  }
137
442277
  return Node::null();
138
}
139
140
7
CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) :
141
7
CandidateGenerator( qe ), d_match_pattern( mpat ){
142
7
  Assert(d_match_pattern.getKind() == EQUAL);
143
7
  d_match_pattern_type = d_match_pattern[0].getType();
144
7
}
145
146
34
void CandidateGeneratorQELitDeq::reset( Node eqc ){
147
34
  eq::EqualityEngine* ee = d_qe->getState().getEqualityEngine();
148
68
  Node falset = NodeManager::currentNM()->mkConst(false);
149
34
  d_eqc_false = eq::EqClassIterator(falset, ee);
150
34
}
151
152
112
Node CandidateGeneratorQELitDeq::getNextCandidate(){
153
  //get next candidate term in equivalence class
154
169
  while( !d_eqc_false.isFinished() ){
155
154
    Node n = (*d_eqc_false);
156
97
    ++d_eqc_false;
157
97
    if( n.getKind()==d_match_pattern.getKind() ){
158
252
      if (n[0].getType().isComparableTo(d_match_pattern_type)
159
252
          && isLegalCandidate(n))
160
      {
161
        //found an iff or equality, try to match it
162
        //DO_THIS: cache to avoid redundancies?
163
        //DO_THIS: do we need to try the symmetric equality for n?  or will it also exist in the eq class of false?
164
40
        return n;
165
      }
166
    }
167
  }
168
15
  return Node::null();
169
}
170
171
172
71
CandidateGeneratorQEAll::CandidateGeneratorQEAll( QuantifiersEngine* qe, Node mpat ) :
173
71
  CandidateGenerator( qe ), d_match_pattern( mpat ){
174
71
  d_match_pattern_type = mpat.getType();
175
71
  Assert(mpat.getKind() == INST_CONSTANT);
176
71
  d_f = quantifiers::TermUtil::getInstConstAttr( mpat );
177
71
  d_index = mpat.getAttribute(InstVarNumAttribute());
178
71
  d_firstTime = false;
179
71
}
180
181
177
void CandidateGeneratorQEAll::reset( Node eqc ) {
182
177
  d_eq = eq::EqClassesIterator(d_qe->getState().getEqualityEngine());
183
177
  d_firstTime = true;
184
177
}
185
186
279
Node CandidateGeneratorQEAll::getNextCandidate() {
187
279
  quantifiers::TermDb* tdb = d_qe->getTermDatabase();
188
4659
  while( !d_eq.isFinished() ){
189
4556
    TNode n = (*d_eq);
190
2366
    ++d_eq;
191
2366
    if( n.getType().isComparableTo( d_match_pattern_type ) ){
192
176
      TNode nh = tdb->getEligibleTermInEqc(n);
193
176
      if( !nh.isNull() ){
194
176
        if (options::instMaxLevel() != -1)
195
        {
196
          nh = d_qe->getInternalRepresentative( nh, d_f, d_index );
197
          //don't consider this if already the instantiation is ineligible
198
          if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f))
199
          {
200
            nh = Node::null();
201
          }
202
        }
203
176
        if( !nh.isNull() ){
204
176
          d_firstTime = false;
205
          //an equivalence class with the same type as the pattern, return it
206
176
          return nh;
207
        }
208
      }
209
    }
210
  }
211
103
  if( d_firstTime ){
212
    //must return something
213
24
    d_firstTime = false;
214
24
    return d_qe->getInstantiate()->getTermForType(d_match_pattern_type);
215
  }
216
79
  return Node::null();
217
}
218
219
2210
CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(
220
2210
    QuantifiersEngine* qe, Node mpat)
221
2210
    : CandidateGeneratorQE(qe, mpat)
222
{
223
2210
  Assert(mpat.getKind() == APPLY_CONSTRUCTOR);
224
2210
  d_mpat_type = mpat.getType();
225
2210
}
226
227
2376
void CandidateGeneratorConsExpand::reset(Node eqc)
228
{
229
2376
  d_term_iter = 0;
230
2376
  if (eqc.isNull())
231
  {
232
808
    d_mode = cand_term_db;
233
  }
234
  else
235
  {
236
1568
    d_eqc = eqc;
237
1568
    d_mode = cand_term_ident;
238
1568
    Assert(d_eqc.getType() == d_mpat_type);
239
  }
240
2376
}
241
242
3185
Node CandidateGeneratorConsExpand::getNextCandidate()
243
{
244
  // get the next term from the base class
245
6370
  Node curr = getNextCandidateInternal();
246
3185
  if (curr.isNull() || (curr.hasOperator() && curr.getOperator() == d_op))
247
  {
248
2679
    return curr;
249
  }
250
  // expand it
251
506
  NodeManager* nm = NodeManager::currentNM();
252
1012
  std::vector<Node> children;
253
506
  const DType& dt = d_mpat_type.getDType();
254
506
  Assert(dt.getNumConstructors() == 1);
255
506
  children.push_back(d_op);
256
1550
  for (unsigned i = 0, nargs = dt[0].getNumArgs(); i < nargs; i++)
257
  {
258
    Node sel = nm->mkNode(
259
2088
        APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(d_mpat_type, i), curr);
260
1044
    children.push_back(sel);
261
  }
262
506
  return nm->mkNode(APPLY_CONSTRUCTOR, children);
263
}
264
265
1568
bool CandidateGeneratorConsExpand::isLegalOpCandidate(Node n)
266
{
267
1568
  return isLegalCandidate(n);
268
}
269
270
159
CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersEngine* qe,
271
159
                                                       Node mpat)
272
159
    : CandidateGeneratorQE(qe, mpat)
273
{
274
159
  Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl;
275
159
  Assert(mpat.getKind() == APPLY_SELECTOR);
276
318
  Node mpatExp = smt::currentSmtEngine()->expandDefinitions(mpat, false);
277
159
  Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
278
159
  if (mpatExp.getKind() == ITE)
279
  {
280
115
    Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL);
281
115
    Assert(mpatExp[2].getKind() == APPLY_UF);
282
115
    d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp[1]);
283
115
    d_ufOp = qe->getTermDatabase()->getMatchOperator(mpatExp[2]);
284
  }
285
44
  else if (mpatExp.getKind() == APPLY_SELECTOR_TOTAL)
286
  {
287
    // corner case of datatype with one constructor
288
44
    d_selOp = qe->getTermDatabase()->getMatchOperator(mpatExp);
289
  }
290
  else
291
  {
292
    // corner case of a wrongly applied selector as a trigger
293
    Assert(mpatExp.getKind() == APPLY_UF);
294
    d_ufOp = qe->getTermDatabase()->getMatchOperator(mpatExp);
295
  }
296
159
  Assert(d_selOp != d_ufOp);
297
159
}
298
299
1133
void CandidateGeneratorSelector::reset(Node eqc)
300
{
301
1133
  Trace("sel-trigger-debug") << "Reset in eqc=" << eqc << std::endl;
302
  // start with d_selOp, if it exists
303
1133
  resetForOperator(eqc, !d_selOp.isNull()? d_selOp : d_ufOp);
304
1133
}
305
306
2438
Node CandidateGeneratorSelector::getNextCandidate()
307
{
308
4876
  Node nextc = getNextCandidateInternal();
309
2438
  if (!nextc.isNull())
310
  {
311
881
    Trace("sel-trigger-debug") << "...next candidate is " << nextc << std::endl;
312
881
    return nextc;
313
  }
314
1557
  else if (d_op == d_selOp)
315
  {
316
795
    if (d_ufOp.isNull())
317
    {
318
      // corner case: selector cannot be wrongly applied (1-cons case)
319
11
      d_op = Node::null();
320
    }
321
    else
322
    {
323
      // finished correctly applied selectors, now try incorrectly applied ones
324
784
      resetForOperator(d_eqc, d_ufOp);
325
784
      return getNextCandidate();
326
    }
327
  }
328
773
  Trace("sel-trigger-debug") << "...finished" << std::endl;
329
  // no more candidates
330
773
  return Node::null();
331
}
332
333
}  // namespace inst
334
}  // namespace theory
335
26676
}  // namespace CVC4