GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/instantiate.cpp Lines: 257 335 76.7 %
Date: 2021-03-22 Branches: 492 1364 36.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file instantiate.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, 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 instantiate
13
 **/
14
15
#include "theory/quantifiers/instantiate.h"
16
17
#include "expr/lazy_proof.h"
18
#include "expr/node_algorithm.h"
19
#include "expr/proof_node_manager.h"
20
#include "options/printer_options.h"
21
#include "options/quantifiers_options.h"
22
#include "options/smt_options.h"
23
#include "proof/proof_manager.h"
24
#include "smt/logic_exception.h"
25
#include "smt/smt_statistics_registry.h"
26
#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
27
#include "theory/quantifiers/first_order_model.h"
28
#include "theory/quantifiers/quantifiers_attributes.h"
29
#include "theory/quantifiers/quantifiers_rewriter.h"
30
#include "theory/quantifiers/term_database.h"
31
#include "theory/quantifiers/term_enumeration.h"
32
#include "theory/quantifiers/term_util.h"
33
#include "theory/quantifiers_engine.h"
34
#include "theory/rewriter.h"
35
36
using namespace CVC4::kind;
37
using namespace CVC4::context;
38
39
namespace CVC4 {
40
namespace theory {
41
namespace quantifiers {
42
43
8995
Instantiate::Instantiate(QuantifiersEngine* qe,
44
                         QuantifiersState& qs,
45
                         QuantifiersInferenceManager& qim,
46
                         QuantifiersRegistry& qr,
47
8995
                         ProofNodeManager* pnm)
48
    : d_qe(qe),
49
      d_qstate(qs),
50
      d_qim(qim),
51
      d_qreg(qr),
52
      d_pnm(pnm),
53
      d_term_db(nullptr),
54
8995
      d_total_inst_debug(qs.getUserContext()),
55
8995
      d_c_inst_match_trie_dom(qs.getUserContext()),
56
26985
      d_pfInst(pnm ? new CDProof(pnm) : nullptr)
57
{
58
8995
}
59
60
26976
Instantiate::~Instantiate()
61
{
62
9607
  for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
63
  {
64
615
    delete t.second;
65
  }
66
8992
  d_c_inst_match_trie.clear();
67
17984
}
68
69
28251
bool Instantiate::reset(Theory::Effort e)
70
{
71
28251
  if (!d_recorded_inst.empty())
72
  {
73
    Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size()
74
                                << " instantiations..." << std::endl;
75
    // remove explicitly recorded instantiations
76
    for (std::pair<Node, std::vector<Node> >& r : d_recorded_inst)
77
    {
78
      removeInstantiationInternal(r.first, r.second);
79
    }
80
    d_recorded_inst.clear();
81
  }
82
28251
  d_term_db = d_qe->getTermDatabase();
83
28251
  return true;
84
}
85
86
23481
void Instantiate::registerQuantifier(Node q) {}
87
3612
bool Instantiate::checkComplete()
88
{
89
3612
  if (!d_recorded_inst.empty())
90
  {
91
2
    Trace("quant-engine-debug")
92
1
        << "Set incomplete due to recorded instantiations." << std::endl;
93
1
    return false;
94
  }
95
3611
  return true;
96
}
97
98
5975
void Instantiate::addRewriter(InstantiationRewriter* ir)
99
{
100
5975
  d_instRewrite.push_back(ir);
101
5975
}
102
103
219589
bool Instantiate::addInstantiation(Node q,
104
                                   std::vector<Node>& terms,
105
                                   InferenceId id,
106
                                   bool mkRep,
107
                                   bool modEq,
108
                                   bool doVts)
109
{
110
  // For resource-limiting (also does a time check).
111
219589
  d_qim.safePoint(ResourceManager::Resource::QuantifierStep);
112
219589
  Assert(!d_qstate.isInConflict());
113
219589
  Assert(terms.size() == q[0].getNumChildren());
114
219589
  Assert(d_term_db != nullptr);
115
439178
  Trace("inst-add-debug") << "For quantified formula " << q
116
219589
                          << ", add instantiation: " << std::endl;
117
849708
  for (unsigned i = 0, size = terms.size(); i < size; i++)
118
  {
119
630119
    Trace("inst-add-debug") << "  " << q[0][i];
120
630119
    Trace("inst-add-debug2") << " -> " << terms[i];
121
1260238
    TypeNode tn = q[0][i].getType();
122
630119
    if (terms[i].isNull())
123
    {
124
2264
      terms[i] = getTermForType(tn);
125
    }
126
    // Ensure the type is correct, this for instance ensures that real terms
127
    // are cast to integers for { x -> t } where x has type Int and t has
128
    // type Real.
129
630119
    terms[i] = ensureType(terms[i], tn);
130
630119
    if (mkRep)
131
    {
132
      // pick the best possible representative for instantiation, based on past
133
      // use and simplicity of term
134
71001
      terms[i] = d_qe->getInternalRepresentative(terms[i], q, i);
135
    }
136
630119
    Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
137
630119
    if (terms[i].isNull())
138
    {
139
      Trace("inst-add-debug")
140
          << " --> Failed to make term vector, due to term/type restrictions."
141
          << std::endl;
142
      return false;
143
    }
144
#ifdef CVC4_ASSERTIONS
145
630119
    bool bad_inst = false;
146
630119
    if (TermUtil::containsUninterpretedConstant(terms[i]))
147
    {
148
      Trace("inst") << "***& inst contains uninterpreted constant : "
149
                    << terms[i] << std::endl;
150
      bad_inst = true;
151
    }
152
630119
    else if (!terms[i].getType().isSubtypeOf(q[0][i].getType()))
153
    {
154
      Trace("inst") << "***& inst bad type : " << terms[i] << " "
155
                    << terms[i].getType() << "/" << q[0][i].getType()
156
                    << std::endl;
157
      bad_inst = true;
158
    }
159
630119
    else if (options::cegqi())
160
    {
161
1246424
      Node icf = TermUtil::getInstConstAttr(terms[i]);
162
623212
      if (!icf.isNull())
163
      {
164
82
        if (icf == q)
165
        {
166
          Trace("inst") << "***& inst contains inst constant attr : "
167
                        << terms[i] << std::endl;
168
          bad_inst = true;
169
        }
170
82
        else if (expr::hasSubterm(terms[i], d_qreg.d_inst_constants[q]))
171
        {
172
          Trace("inst") << "***& inst contains inst constants : " << terms[i]
173
                        << std::endl;
174
          bad_inst = true;
175
        }
176
      }
177
    }
178
    // this assertion is critical to soundness
179
630119
    if (bad_inst)
180
    {
181
      Trace("inst") << "***& Bad Instantiate " << q << " with " << std::endl;
182
      for (unsigned j = 0; j < terms.size(); j++)
183
      {
184
        Trace("inst") << "   " << terms[j] << std::endl;
185
      }
186
      Assert(false);
187
    }
188
#endif
189
  }
190
191
  // Note we check for entailment before checking for term vector duplication.
192
  // Although checking for term vector duplication is a faster check, it is
193
  // included automatically with recordInstantiationInternal, hence we prefer
194
  // two checks instead of three. In experiments, it is 1% slower or so to call
195
  // existsInstantiation here.
196
  // Alternatively, we could return an (index, trie node) in the call to
197
  // existsInstantiation here, where this would return the node in the trie
198
  // where we determined that there is definitely no duplication, and then
199
  // continue from that point in recordInstantiation below. However, for
200
  // simplicity, we do not pursue this option (as it would likely only
201
  // lead to very small gains).
202
203
  // check for positive entailment
204
219589
  if (options::instNoEntail())
205
  {
206
    // should check consistency of equality engine
207
    // (if not aborting on utility's reset)
208
293674
    std::map<TNode, TNode> subs;
209
834507
    for (unsigned i = 0, size = terms.size(); i < size; i++)
210
    {
211
618080
      subs[q[0][i]] = terms[i];
212
    }
213
216427
    if (d_term_db->isEntailed(q[1], subs, false, true))
214
    {
215
139180
      Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
216
139180
      ++(d_statistics.d_inst_duplicate_ent);
217
139180
      return false;
218
    }
219
  }
220
221
  // check based on instantiation level
222
80409
  if (options::instMaxLevel() != -1)
223
  {
224
963
    for (Node& t : terms)
225
    {
226
678
      if (!d_term_db->isTermEligibleForInstantiation(t, q))
227
      {
228
        return false;
229
      }
230
    }
231
  }
232
233
  // record the instantiation
234
80409
  bool recorded = recordInstantiationInternal(q, terms, modEq);
235
80409
  if (!recorded)
236
  {
237
42504
    Trace("inst-add-debug") << " --> Already exists (no record)." << std::endl;
238
42504
    ++(d_statistics.d_inst_duplicate_eq);
239
42504
    return false;
240
  }
241
242
  // Set up a proof if proofs are enabled. This proof stores a proof of
243
  // the instantiation body with q as a free assumption.
244
75810
  std::shared_ptr<LazyCDProof> pfTmp;
245
37905
  if (isProofEnabled())
246
  {
247
17320
    pfTmp.reset(new LazyCDProof(
248
8660
        d_pnm, nullptr, nullptr, "Instantiate::LazyCDProof::tmp"));
249
  }
250
251
  // construct the instantiation
252
37905
  Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
253
37905
  Assert(d_qreg.d_vars[q].size() == terms.size());
254
  // get the instantiation
255
75810
  Node body = getInstantiation(q, d_qreg.d_vars[q], terms, doVts, pfTmp.get());
256
75810
  Node orig_body = body;
257
  // now preprocess, storing the trust node for the rewrite
258
75810
  TrustNode tpBody = QuantifiersRewriter::preprocess(body, true);
259
37905
  if (!tpBody.isNull())
260
  {
261
    Assert(tpBody.getKind() == TrustNodeKind::REWRITE);
262
    body = tpBody.getNode();
263
    // do a tranformation step
264
    if (pfTmp != nullptr)
265
    {
266
      //              ----------------- from preprocess
267
      // orig_body    orig_body = body
268
      // ------------------------------ EQ_RESOLVE
269
      // body
270
      Node proven = tpBody.getProven();
271
      // add the transformation proof, or THEORY_PREPROCESS if none provided
272
      pfTmp->addLazyStep(proven,
273
                         tpBody.getGenerator(),
274
                         PfRule::THEORY_PREPROCESS,
275
                         true,
276
                         "Instantiate::getInstantiation:qpreprocess");
277
      pfTmp->addStep(body, PfRule::EQ_RESOLVE, {orig_body, proven}, {});
278
    }
279
  }
280
37905
  Trace("inst-debug") << "...preprocess to " << body << std::endl;
281
282
  // construct the lemma
283
37905
  Trace("inst-assert") << "(assert " << body << ")" << std::endl;
284
285
  // construct the instantiation, and rewrite the lemma
286
75810
  Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, q, body);
287
288
  // If proofs are enabled, construct the proof, which is of the form:
289
  // ... free assumption q ...
290
  // ------------------------- from pfTmp
291
  // body
292
  // ------------------------- SCOPE
293
  // (=> q body)
294
  // -------------------------- MACRO_SR_PRED_ELIM
295
  // lem
296
37905
  bool hasProof = false;
297
37905
  if (isProofEnabled())
298
  {
299
    // make the proof of body
300
17320
    std::shared_ptr<ProofNode> pfn = pfTmp->getProofFor(body);
301
    // make the scope proof to get (=> q body)
302
17320
    std::vector<Node> assumps;
303
8660
    assumps.push_back(q);
304
17320
    std::shared_ptr<ProofNode> pfns = d_pnm->mkScope({pfn}, assumps);
305
8660
    Assert(assumps.size() == 1 && assumps[0] == q);
306
    // store in the main proof
307
8660
    d_pfInst->addProof(pfns);
308
17320
    Node prevLem = lem;
309
8660
    lem = Rewriter::rewrite(lem);
310
8660
    if (prevLem != lem)
311
    {
312
4198
      d_pfInst->addStep(lem, PfRule::MACRO_SR_PRED_ELIM, {prevLem}, {});
313
    }
314
8660
    hasProof = true;
315
  }
316
  else
317
  {
318
29245
    lem = Rewriter::rewrite(lem);
319
  }
320
321
  // added lemma, which checks for lemma duplication
322
37905
  bool addedLem = false;
323
37905
  if (hasProof)
324
  {
325
    // use proof generator
326
8660
    addedLem =
327
17320
        d_qim.addPendingLemma(lem, id, LemmaProperty::NONE, d_pfInst.get());
328
  }
329
  else
330
  {
331
29245
    addedLem = d_qim.addPendingLemma(lem, id);
332
  }
333
334
37905
  if (!addedLem)
335
  {
336
951
    Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
337
951
    ++(d_statistics.d_inst_duplicate);
338
951
    return false;
339
  }
340
341
36954
  d_total_inst_debug[q] = d_total_inst_debug[q] + 1;
342
36954
  d_temp_inst_debug[q]++;
343
36954
  if (Trace.isOn("inst"))
344
  {
345
    Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
346
    for (unsigned i = 0, size = terms.size(); i < size; i++)
347
    {
348
      if (Trace.isOn("inst"))
349
      {
350
        Trace("inst") << "   " << terms[i];
351
        if (Trace.isOn("inst-debug"))
352
        {
353
          Trace("inst-debug") << ", type=" << terms[i].getType()
354
                              << ", var_type=" << q[0][i].getType();
355
        }
356
        Trace("inst") << std::endl;
357
      }
358
    }
359
  }
360
36954
  if (options::instMaxLevel() != -1)
361
  {
362
268
    if (doVts)
363
    {
364
      // virtual term substitution/instantiation level features are
365
      // incompatible
366
      std::stringstream ss;
367
      ss << "Cannot combine instantiation strategies that require virtual term "
368
            "substitution with those that restrict instantiation levels";
369
      throw LogicException(ss.str());
370
    }
371
    else
372
    {
373
268
      uint64_t maxInstLevel = 0;
374
921
      for (const Node& tc : terms)
375
      {
376
1306
        if (tc.hasAttribute(InstLevelAttribute())
377
653
            && tc.getAttribute(InstLevelAttribute()) > maxInstLevel)
378
        {
379
          maxInstLevel = tc.getAttribute(InstLevelAttribute());
380
        }
381
      }
382
268
      QuantAttributes::setInstantiationLevelAttr(
383
          orig_body, q[1], maxInstLevel + 1);
384
    }
385
  }
386
36954
  Trace("inst-add-debug") << " --> Success." << std::endl;
387
36954
  ++(d_statistics.d_instantiations);
388
36954
  return true;
389
}
390
391
8973
bool Instantiate::addInstantiationExpFail(Node q,
392
                                          std::vector<Node>& terms,
393
                                          std::vector<bool>& failMask,
394
                                          InferenceId id,
395
                                          bool mkRep,
396
                                          bool modEq,
397
                                          bool doVts,
398
                                          bool expFull)
399
{
400
8973
  if (addInstantiation(q, terms, id, mkRep, modEq, doVts))
401
  {
402
1163
    return true;
403
  }
404
7810
  size_t tsize = terms.size();
405
7810
  failMask.resize(tsize, true);
406
7810
  if (tsize == 1)
407
  {
408
    // will never succeed with 1 variable
409
3625
    return false;
410
  }
411
4185
  Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl;
412
  // set up information for below
413
4185
  std::vector<Node>& vars = d_qreg.d_vars[q];
414
4185
  Assert(tsize == vars.size());
415
8370
  std::map<TNode, TNode> subs;
416
21320
  for (size_t i = 0; i < tsize; i++)
417
  {
418
17135
    subs[vars[i]] = terms[i];
419
  }
420
  // get the instantiation body
421
8370
  Node ibody = getInstantiation(q, vars, terms, doVts);
422
4185
  ibody = Rewriter::rewrite(ibody);
423
21215
  for (size_t i = 0; i < tsize; i++)
424
  {
425
    // process consecutively in reverse order, which is important since we use
426
    // the fail mask for incrementing in a lexicographic order
427
17135
    size_t ii = (tsize - 1) - i;
428
    // replace with the identity substitution
429
34165
    Node prev = terms[ii];
430
17135
    terms[ii] = vars[ii];
431
17135
    subs.erase(vars[ii]);
432
17135
    if (subs.empty())
433
    {
434
      // will never succeed with empty substitution
435
105
      break;
436
    }
437
17030
    Trace("inst-exp-fail") << "- revert " << ii << std::endl;
438
    // check whether we are still redundant
439
17030
    bool success = false;
440
    // check entailment, only if option is set
441
17030
    if (options::instNoEntail())
442
    {
443
17030
      Trace("inst-exp-fail") << "  check entailment" << std::endl;
444
17030
      success = d_term_db->isEntailed(q[1], subs, false, true);
445
17030
      Trace("inst-exp-fail") << "  entailed: " << success << std::endl;
446
    }
447
    // check whether the instantiation rewrites to the same thing
448
17030
    if (!success)
449
    {
450
29130
      Node ibodyc = getInstantiation(q, vars, terms, doVts);
451
14565
      ibodyc = Rewriter::rewrite(ibodyc);
452
14565
      success = (ibodyc == ibody);
453
14565
      Trace("inst-exp-fail") << "  rewrite invariant: " << success << std::endl;
454
    }
455
17030
    if (success)
456
    {
457
      // if we still fail, we are not critical
458
2695
      failMask[ii] = false;
459
    }
460
    else
461
    {
462
14335
      subs[vars[ii]] = prev;
463
14335
      terms[ii] = prev;
464
      // not necessary to proceed if expFull is false
465
14335
      if (!expFull)
466
      {
467
        break;
468
      }
469
    }
470
  }
471
4185
  if (Trace.isOn("inst-exp-fail"))
472
  {
473
    Trace("inst-exp-fail") << "Fail mask: ";
474
    for (bool b : failMask)
475
    {
476
      Trace("inst-exp-fail") << (b ? 1 : 0);
477
    }
478
    Trace("inst-exp-fail") << std::endl;
479
  }
480
4185
  return false;
481
}
482
483
1
bool Instantiate::recordInstantiation(Node q,
484
                                      std::vector<Node>& terms,
485
                                      bool modEq,
486
                                      bool addedLem)
487
{
488
1
  return recordInstantiationInternal(q, terms, modEq, addedLem);
489
}
490
491
bool Instantiate::existsInstantiation(Node q,
492
                                      std::vector<Node>& terms,
493
                                      bool modEq)
494
{
495
  if (options::incrementalSolving())
496
  {
497
    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
498
        d_c_inst_match_trie.find(q);
499
    if (it != d_c_inst_match_trie.end())
500
    {
501
      return it->second->existsInstMatch(d_qstate, q, terms, modEq);
502
    }
503
  }
504
  else
505
  {
506
    std::map<Node, inst::InstMatchTrie>::iterator it =
507
        d_inst_match_trie.find(q);
508
    if (it != d_inst_match_trie.end())
509
    {
510
      return it->second.existsInstMatch(d_qstate, q, terms, modEq);
511
    }
512
  }
513
  return false;
514
}
515
516
244132
Node Instantiate::getInstantiation(Node q,
517
                                   std::vector<Node>& vars,
518
                                   std::vector<Node>& terms,
519
                                   bool doVts,
520
                                   LazyCDProof* pf)
521
{
522
244132
  Assert(vars.size() == terms.size());
523
244132
  Assert(q[0].getNumChildren() == vars.size());
524
  // Notice that this could be optimized, but no significant performance
525
  // improvements were observed with alternative implementations (see #1386).
526
  Node body =
527
244132
      q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
528
529
  // store the proof of the instantiated body, with (open) assumption q
530
244132
  if (pf != nullptr)
531
  {
532
8660
    pf->addStep(body, PfRule::INSTANTIATE, {q}, terms);
533
  }
534
535
  // run rewriters to rewrite the instantiation in sequence.
536
482721
  for (InstantiationRewriter*& ir : d_instRewrite)
537
  {
538
477178
    TrustNode trn = ir->rewriteInstantiation(q, terms, body, doVts);
539
238589
    if (!trn.isNull())
540
    {
541
134
      Node newBody = trn.getNode();
542
      // if using proofs, we store a preprocess + transformation step.
543
67
      if (pf != nullptr)
544
      {
545
32
        Node proven = trn.getProven();
546
16
        pf->addLazyStep(proven,
547
                        trn.getGenerator(),
548
                        PfRule::THEORY_PREPROCESS,
549
                        true,
550
                        "Instantiate::getInstantiation:rewrite_inst");
551
16
        pf->addStep(newBody, PfRule::EQ_RESOLVE, {body, proven}, {});
552
      }
553
67
      body = newBody;
554
    }
555
  }
556
244132
  return body;
557
}
558
559
186971
Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
560
{
561
186971
  Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
562
186971
  return getInstantiation(q, d_qreg.d_vars[q], terms, doVts);
563
}
564
565
80410
bool Instantiate::recordInstantiationInternal(Node q,
566
                                              std::vector<Node>& terms,
567
                                              bool modEq,
568
                                              bool addedLem)
569
{
570
80410
  if (!addedLem)
571
  {
572
    // record the instantiation for deletion later
573
1
    d_recorded_inst.push_back(std::pair<Node, std::vector<Node> >(q, terms));
574
  }
575
80410
  if (options::incrementalSolving())
576
  {
577
8688
    Trace("inst-add-debug")
578
4344
        << "Adding into context-dependent inst trie, modEq = " << modEq
579
4344
        << std::endl;
580
    inst::CDInstMatchTrie* imt;
581
    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
582
4344
        d_c_inst_match_trie.find(q);
583
4344
    if (it != d_c_inst_match_trie.end())
584
    {
585
3729
      imt = it->second;
586
    }
587
    else
588
    {
589
615
      imt = new inst::CDInstMatchTrie(d_qstate.getUserContext());
590
615
      d_c_inst_match_trie[q] = imt;
591
    }
592
4344
    d_c_inst_match_trie_dom.insert(q);
593
4344
    return imt->addInstMatch(d_qstate, q, terms, modEq);
594
  }
595
76066
  Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
596
76066
  return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms, modEq);
597
}
598
599
bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)
600
{
601
  if (options::incrementalSolving())
602
  {
603
    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
604
        d_c_inst_match_trie.find(q);
605
    if (it != d_c_inst_match_trie.end())
606
    {
607
      return it->second->removeInstMatch(q, terms);
608
    }
609
    return false;
610
  }
611
  return d_inst_match_trie[q].removeInstMatch(q, terms);
612
}
613
614
2288
Node Instantiate::getTermForType(TypeNode tn)
615
{
616
2288
  if (tn.isClosedEnumerable())
617
  {
618
108
    return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
619
  }
620
2180
  return d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
621
}
622
623
88
void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
624
{
625
88
  if (options::incrementalSolving())
626
  {
627
    for (context::CDHashSet<Node, NodeHashFunction>::const_iterator it =
628
4
             d_c_inst_match_trie_dom.begin();
629
4
         it != d_c_inst_match_trie_dom.end();
630
         ++it)
631
    {
632
      qs.push_back(*it);
633
    }
634
  }
635
  else
636
  {
637
163
    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
638
    {
639
79
      qs.push_back(t.first);
640
    }
641
  }
642
88
}
643
644
87
void Instantiate::getInstantiationTermVectors(
645
    Node q, std::vector<std::vector<Node> >& tvecs)
646
{
647
648
87
  if (options::incrementalSolving())
649
  {
650
    std::map<Node, inst::CDInstMatchTrie*>::const_iterator it =
651
2
        d_c_inst_match_trie.find(q);
652
2
    if (it != d_c_inst_match_trie.end())
653
    {
654
2
      it->second->getInstantiations(q, tvecs);
655
    }
656
  }
657
  else
658
  {
659
    std::map<Node, inst::InstMatchTrie>::const_iterator it =
660
85
        d_inst_match_trie.find(q);
661
85
    if (it != d_inst_match_trie.end())
662
    {
663
85
      it->second.getInstantiations(q, tvecs);
664
    }
665
  }
666
87
}
667
668
6
void Instantiate::getInstantiationTermVectors(
669
    std::map<Node, std::vector<std::vector<Node> > >& insts)
670
{
671
6
  if (options::incrementalSolving())
672
  {
673
4
    for (const auto& t : d_c_inst_match_trie)
674
    {
675
2
      getInstantiationTermVectors(t.first, insts[t.first]);
676
    }
677
  }
678
  else
679
  {
680
10
    for (const auto& t : d_inst_match_trie)
681
    {
682
6
      getInstantiationTermVectors(t.first, insts[t.first]);
683
    }
684
  }
685
6
}
686
687
75810
bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
688
689
2
void Instantiate::debugPrint(std::ostream& out)
690
{
691
  // debug information
692
2
  if (Trace.isOn("inst-per-quant-round"))
693
  {
694
    for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
695
    {
696
      Trace("inst-per-quant-round") << " * " << i.second << " for " << i.first
697
                                    << std::endl;
698
      d_temp_inst_debug[i.first] = 0;
699
    }
700
  }
701
12612
  if (options::debugInst())
702
  {
703
2
    bool req = !options::printInstFull();
704
6
    for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
705
    {
706
8
      Node name;
707
4
      if (!d_qe->getNameForQuant(i.first, name, req))
708
      {
709
        continue;
710
      }
711
8
      out << "(num-instantiations " << name << " " << i.second << ")"
712
4
          << std::endl;
713
    }
714
  }
715
2
}
716
717
5822
void Instantiate::debugPrintModel()
718
{
719
5822
  if (Trace.isOn("inst-per-quant"))
720
  {
721
    for (NodeUIntMap::iterator it = d_total_inst_debug.begin();
722
         it != d_total_inst_debug.end();
723
         ++it)
724
    {
725
      Trace("inst-per-quant")
726
          << " * " << (*it).second << " for " << (*it).first << std::endl;
727
    }
728
  }
729
5822
}
730
731
630119
Node Instantiate::ensureType(Node n, TypeNode tn)
732
{
733
630119
  Trace("inst-add-debug2") << "Ensure " << n << " : " << tn << std::endl;
734
1260238
  TypeNode ntn = n.getType();
735
630119
  Assert(ntn.isComparableTo(tn));
736
630119
  if (ntn.isSubtypeOf(tn))
737
  {
738
630109
    return n;
739
  }
740
10
  if (tn.isInteger())
741
  {
742
10
    return NodeManager::currentNM()->mkNode(TO_INTEGER, n);
743
  }
744
  return Node::null();
745
}
746
747
8995
Instantiate::Statistics::Statistics()
748
    : d_instantiations("Instantiate::Instantiations_Total", 0),
749
      d_inst_duplicate("Instantiate::Duplicate_Inst", 0),
750
      d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0),
751
8995
      d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0)
752
{
753
8995
  smtStatisticsRegistry()->registerStat(&d_instantiations);
754
8995
  smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
755
8995
  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
756
8995
  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
757
8995
}
758
759
17984
Instantiate::Statistics::~Statistics()
760
{
761
8992
  smtStatisticsRegistry()->unregisterStat(&d_instantiations);
762
8992
  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
763
8992
  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
764
8992
  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
765
8992
}
766
767
} /* CVC4::theory::quantifiers namespace */
768
} /* CVC4::theory namespace */
769
39286
} /* CVC4 namespace */