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

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