src/theory/quantifiers/instantiate.cpp

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