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

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