(Refactor) Instantiate utility (#1387)

1 files changed, 821 insertions, 0 deletions

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
new file mode 100644
index 000000000..e04217b16
--- /dev/null
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -0,0 +1,821 @@
+/*********************                                                        */
+/*! \file instantiate.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of instantiate
+ **/
+
+#include "theory/quantifiers/instantiate.h"
+
+#include "options/quantifiers_options.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/inst_strategy_cbqi.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+Instantiate::Instantiate(QuantifiersEngine* qe, context::UserContext* u)
+    : d_qe(qe),
+      d_term_db(nullptr),
+      d_term_util(nullptr),
+      d_total_inst_count_debug(0),
+      d_c_inst_match_trie_dom(u)
+{
+}
+
+Instantiate::~Instantiate()
+{
+  for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+  {
+    delete t.second;
+  }
+  d_c_inst_match_trie.clear();
+}
+
+bool Instantiate::reset(Theory::Effort e)
+{
+  if (!d_recorded_inst.empty())
+  {
+    Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size()
+                                << " instantiations..." << std::endl;
+    // remove explicitly recorded instantiations
+    for (std::pair<Node, std::vector<Node> >& r : d_recorded_inst)
+    {
+      removeInstantiationInternal(r.first, r.second);
+    }
+    d_recorded_inst.clear();
+  }
+  d_term_db = d_qe->getTermDatabase();
+  d_term_util = d_qe->getTermUtil();
+  return true;
+}
+
+void Instantiate::registerQuantifier(Node q) {}
+bool Instantiate::checkComplete()
+{
+  if (!d_recorded_inst.empty())
+  {
+    Trace("quant-engine-debug")
+        << "Set incomplete due to recorded instantiations." << std::endl;
+    return false;
+  }
+  return true;
+}
+
+void Instantiate::addNotify(InstantiationNotify* in)
+{
+  d_inst_notify.push_back(in);
+}
+
+void Instantiate::notifyFlushLemmas()
+{
+  for (InstantiationNotify*& in : d_inst_notify)
+  {
+    in->filterInstantiations();
+  }
+}
+
+bool Instantiate::addInstantiation(
+    Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts)
+{
+  Assert(q[0].getNumChildren() == m.d_vals.size());
+  return addInstantiation(q, m.d_vals, mkRep, modEq, doVts);
+}
+
+bool Instantiate::addInstantiation(
+    Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts)
+{
+  // For resource-limiting (also does a time check).
+  d_qe->getOutputChannel().safePoint(options::quantifierStep());
+  Assert(!d_qe->inConflict());
+  Assert(terms.size() == q[0].getNumChildren());
+  Assert(d_term_db != nullptr);
+  Assert(d_term_util != nullptr);
+  Trace("inst-add-debug") << "For quantified formula " << q
+                          << ", add instantiation: " << std::endl;
+  for (unsigned i = 0, size = terms.size(); i < size; i++)
+  {
+    Trace("inst-add-debug") << "  " << q[0][i];
+    Trace("inst-add-debug2") << " -> " << terms[i];
+    TypeNode tn = q[0][i].getType();
+    if (terms[i].isNull())
+    {
+      terms[i] = getTermForType(tn);
+    }
+    if (mkRep)
+    {
+      // pick the best possible representative for instantiation, based on past
+      // use and simplicity of term
+      terms[i] = d_qe->getInternalRepresentative(terms[i], q, i);
+    }
+    else
+    {
+      // ensure the type is correct
+      terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn);
+    }
+    Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
+    if (terms[i].isNull())
+    {
+      Trace("inst-add-debug")
+          << " --> Failed to make term vector, due to term/type restrictions."
+          << std::endl;
+      return false;
+    }
+#ifdef CVC4_ASSERTIONS
+    bool bad_inst = false;
+    if (quantifiers::TermUtil::containsUninterpretedConstant(terms[i]))
+    {
+      Trace("inst") << "***& inst contains uninterpreted constant : "
+                    << terms[i] << std::endl;
+      bad_inst = true;
+    }
+    else if (!terms[i].getType().isSubtypeOf(q[0][i].getType()))
+    {
+      Trace("inst") << "***& inst bad type : " << terms[i] << " "
+                    << terms[i].getType() << "/" << q[0][i].getType()
+                    << std::endl;
+      bad_inst = true;
+    }
+    else if (options::cbqi())
+    {
+      Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
+      if (!icf.isNull())
+      {
+        if (icf == q)
+        {
+          Trace("inst") << "***& inst contains inst constant attr : "
+                        << terms[i] << std::endl;
+          bad_inst = true;
+        }
+        else if (quantifiers::TermUtil::containsTerms(
+                     terms[i], d_term_util->d_inst_constants[q]))
+        {
+          Trace("inst") << "***& inst contains inst constants : " << terms[i]
+                        << std::endl;
+          bad_inst = true;
+        }
+      }
+    }
+    // this assertion is critical to soundness
+    if (bad_inst)
+    {
+      Trace("inst") << "***& Bad Instantiate " << q << " with " << std::endl;
+      for (unsigned j = 0; j < terms.size(); j++)
+      {
+        Trace("inst") << "   " << terms[j] << std::endl;
+      }
+      Assert(false);
+    }
+#endif
+  }
+
+  // Note we check for entailment before checking for term vector duplication.
+  // Although checking for term vector duplication is a faster check, it is
+  // included automatically with recordInstantiationInternal, hence we prefer
+  // two checks instead of three. In experiments, it is 1% slower or so to call
+  // existsInstantiation here.
+  // Alternatively, we could return an (index, trie node) in the call to
+  // existsInstantiation here, where this would return the node in the trie
+  // where we determined that there is definitely no duplication, and then
+  // continue from that point in recordInstantiation below. However, for
+  // simplicity, we do not pursue this option (as it would likely only
+  // lead to very small gains).
+
+  // check for positive entailment
+  if (options::instNoEntail())
+  {
+    // should check consistency of equality engine
+    // (if not aborting on utility's reset)
+    std::map<TNode, TNode> subs;
+    for (unsigned i = 0, size = terms.size(); i < size; i++)
+    {
+      subs[q[0][i]] = terms[i];
+    }
+    if (d_term_db->isEntailed(q[1], subs, false, true))
+    {
+      Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
+      ++(d_statistics.d_inst_duplicate_ent);
+      return false;
+    }
+  }
+
+  // check based on instantiation level
+  if (options::instMaxLevel() != -1 || options::lteRestrictInstClosure())
+  {
+    for (Node& t : terms)
+    {
+      if (!d_term_db->isTermEligibleForInstantiation(t, q, true))
+      {
+        return false;
+      }
+    }
+  }
+
+  // record the instantiation
+  bool recorded = recordInstantiationInternal(q, terms, modEq);
+  if (!recorded)
+  {
+    Trace("inst-add-debug") << " --> Already exists (no record)." << std::endl;
+    ++(d_statistics.d_inst_duplicate_eq);
+    return false;
+  }
+
+  // construct the instantiation
+  Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
+  Assert(d_term_util->d_vars[q].size() == terms.size());
+  // get the instantiation
+  Node body = getInstantiation(q, d_term_util->d_vars[q], terms, doVts);
+  Node orig_body = body;
+  if (options::cbqiNestedQE())
+  {
+    InstStrategyCbqi* icbqi = d_qe->getInstStrategyCbqi();
+    if (icbqi)
+    {
+      body = icbqi->doNestedQE(q, terms, body, doVts);
+    }
+  }
+  body = quantifiers::QuantifiersRewriter::preprocess(body, true);
+  Trace("inst-debug") << "...preprocess to " << body << std::endl;
+
+  // construct the lemma
+  Trace("inst-assert") << "(assert " << body << ")" << std::endl;
+
+  if (d_qe->usingModelEqualityEngine() && options::instNoModelTrue())
+  {
+    Node val_body = d_qe->getModel()->getValue(body);
+    if (val_body.isConst() && val_body.getConst<bool>())
+    {
+      Trace("inst-add-debug") << " --> True in model." << std::endl;
+      ++(d_statistics.d_inst_duplicate_model_true);
+      return false;
+    }
+  }
+
+  Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body);
+
+  // get relevancy conditions
+  if (options::instRelevantCond())
+  {
+    std::vector<Node> rlv_cond;
+    for (Node& t : terms)
+    {
+      quantifiers::TermUtil::getRelevancyCondition(t, rlv_cond);
+    }
+    if (!rlv_cond.empty())
+    {
+      rlv_cond.push_back(lem);
+      lem = NodeManager::currentNM()->mkNode(kind::OR, rlv_cond);
+    }
+  }
+
+  lem = Rewriter::rewrite(lem);
+
+  // check for lemma duplication
+  if (!d_qe->addLemma(lem, true, false))
+  {
+    Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
+    ++(d_statistics.d_inst_duplicate);
+    return false;
+  }
+
+  d_total_inst_debug[q]++;
+  d_temp_inst_debug[q]++;
+  d_total_inst_count_debug++;
+  if (Trace.isOn("inst"))
+  {
+    Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
+    for (unsigned i = 0, size = terms.size(); i < size; i++)
+    {
+      if (Trace.isOn("inst"))
+      {
+        Trace("inst") << "   " << terms[i];
+        if (Trace.isOn("inst-debug"))
+        {
+          Trace("inst-debug") << ", type=" << terms[i].getType()
+                              << ", var_type=" << q[0][i].getType();
+        }
+        Trace("inst") << std::endl;
+      }
+    }
+  }
+  if (options::instMaxLevel() != -1)
+  {
+    if (doVts)
+    {
+      // virtual term substitution/instantiation level features are
+      // incompatible
+      Assert(false);
+    }
+    else
+    {
+      uint64_t maxInstLevel = 0;
+      for (const Node& tc : terms)
+      {
+        if (tc.hasAttribute(InstLevelAttribute())
+            && tc.getAttribute(InstLevelAttribute()) > maxInstLevel)
+        {
+          maxInstLevel = tc.getAttribute(InstLevelAttribute());
+        }
+      }
+      QuantAttributes::setInstantiationLevelAttr(
+          orig_body, q[1], maxInstLevel + 1);
+    }
+  }
+  QuantifiersModule::QEffort elevel = d_qe->getCurrentQEffort();
+  if (elevel > QuantifiersModule::QEFFORT_CONFLICT
+      && elevel < QuantifiersModule::QEFFORT_NONE
+      && !d_inst_notify.empty())
+  {
+    // notify listeners
+    for (InstantiationNotify*& in : d_inst_notify)
+    {
+      if (!in->notifyInstantiation(elevel, q, lem, terms, body))
+      {
+        Trace("inst-add-debug") << "...we are in conflict." << std::endl;
+        d_qe->setConflict();
+        Assert(d_qe->getNumLemmasWaiting() > 0);
+        break;
+      }
+    }
+  }
+  if (options::trackInstLemmas())
+  {
+    bool recorded;
+    if (options::incrementalSolving())
+    {
+      recorded = d_c_inst_match_trie[q]->recordInstLemma(q, terms, lem);
+    }
+    else
+    {
+      recorded = d_inst_match_trie[q].recordInstLemma(q, terms, lem);
+    }
+    Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl;
+    Assert(recorded);
+  }
+  Trace("inst-add-debug") << " --> Success." << std::endl;
+  ++(d_statistics.d_instantiations);
+  return true;
+}
+
+bool Instantiate::removeInstantiation(Node q,
+                                      Node lem,
+                                      std::vector<Node>& terms)
+{
+  // lem must occur in d_waiting_lemmas
+  if (d_qe->removeLemma(lem))
+  {
+    return removeInstantiationInternal(q, terms);
+  }
+  return false;
+}
+
+bool Instantiate::recordInstantiation(Node q,
+                                      std::vector<Node>& terms,
+                                      bool modEq,
+                                      bool addedLem)
+{
+  return recordInstantiationInternal(q, terms, modEq, addedLem);
+}
+
+bool Instantiate::existsInstantiation(Node q,
+                                      std::vector<Node>& terms,
+                                      bool modEq)
+{
+  if (options::incrementalSolving())
+  {
+    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
+        d_c_inst_match_trie.find(q);
+    if (it != d_c_inst_match_trie.end())
+    {
+      return it->second->existsInstMatch(
+          d_qe, q, terms, d_qe->getUserContext(), modEq);
+    }
+  }
+  else
+  {
+    std::map<Node, inst::InstMatchTrie>::iterator it =
+        d_inst_match_trie.find(q);
+    if (it != d_inst_match_trie.end())
+    {
+      return it->second.existsInstMatch(d_qe, q, terms, modEq);
+    }
+  }
+  return false;
+}
+
+Node Instantiate::getInstantiation(Node q,
+                                   std::vector<Node>& vars,
+                                   std::vector<Node>& terms,
+                                   bool doVts)
+{
+  Node body;
+  Assert(vars.size() == terms.size());
+  Assert(q[0].getNumChildren() == vars.size());
+  // TODO (#1386) : optimize this
+  body = q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
+  if (doVts)
+  {
+    // do virtual term substitution
+    body = Rewriter::rewrite(body);
+    Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
+    Node body_r = d_term_util->rewriteVtsSymbols(body);
+    Trace("quant-vts-debug") << "            ...result: " << body_r
+                             << std::endl;
+    body = body_r;
+  }
+  return body;
+}
+
+Node Instantiate::getInstantiation(Node q, InstMatch& m, bool doVts)
+{
+  Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end());
+  Assert(m.d_vals.size() == q[0].getNumChildren());
+  return getInstantiation(q, d_term_util->d_vars[q], m.d_vals, doVts);
+}
+
+Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
+{
+  Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end());
+  return getInstantiation(q, d_term_util->d_vars[q], terms, doVts);
+}
+
+bool Instantiate::recordInstantiationInternal(Node q,
+                                              std::vector<Node>& terms,
+                                              bool modEq,
+                                              bool addedLem)
+{
+  if (!addedLem)
+  {
+    // record the instantiation for deletion later
+    d_recorded_inst.push_back(std::pair<Node, std::vector<Node> >(q, terms));
+  }
+  if (options::incrementalSolving())
+  {
+    Trace("inst-add-debug")
+        << "Adding into context-dependent inst trie, modEq = " << modEq
+        << std::endl;
+    inst::CDInstMatchTrie* imt;
+    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
+        d_c_inst_match_trie.find(q);
+    if (it != d_c_inst_match_trie.end())
+    {
+      imt = it->second;
+    }
+    else
+    {
+      imt = new inst::CDInstMatchTrie(d_qe->getUserContext());
+      d_c_inst_match_trie[q] = imt;
+    }
+    d_c_inst_match_trie_dom.insert(q);
+    return imt->addInstMatch(d_qe, q, terms, d_qe->getUserContext(), modEq);
+  }
+  Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
+  return d_inst_match_trie[q].addInstMatch(d_qe, q, terms, modEq);
+}
+
+bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)
+{
+  if (options::incrementalSolving())
+  {
+    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
+        d_c_inst_match_trie.find(q);
+    if (it != d_c_inst_match_trie.end())
+    {
+      return it->second->removeInstMatch(q, terms);
+    }
+    return false;
+  }
+  return d_inst_match_trie[q].removeInstMatch(q, terms);
+}
+
+Node Instantiate::getTermForType(TypeNode tn)
+{
+  if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+  {
+    return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
+  }
+  return d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
+}
+
+bool Instantiate::printInstantiations(std::ostream& out)
+{
+  bool useUnsatCore = false;
+  std::vector<Node> active_lemmas;
+  if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas))
+  {
+    useUnsatCore = true;
+  }
+  bool printed = false;
+  if (options::incrementalSolving())
+  {
+    for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+    {
+      bool firstTime = true;
+      t.second->print(out, t.first, firstTime, useUnsatCore, active_lemmas);
+      if (!firstTime)
+      {
+        out << ")" << std::endl;
+      }
+      printed = printed || !firstTime;
+    }
+  }
+  else
+  {
+    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+    {
+      bool firstTime = true;
+      t.second.print(out, t.first, firstTime, useUnsatCore, active_lemmas);
+      if (!firstTime)
+      {
+        out << ")" << std::endl;
+      }
+      printed = printed || !firstTime;
+    }
+  }
+  return printed;
+}
+
+void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
+{
+  if (options::incrementalSolving())
+  {
+    for (context::CDHashSet<Node, NodeHashFunction>::const_iterator it =
+             d_c_inst_match_trie_dom.begin();
+         it != d_c_inst_match_trie_dom.end();
+         ++it)
+    {
+      qs.push_back(*it);
+    }
+  }
+  else
+  {
+    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+    {
+      qs.push_back(t.first);
+    }
+  }
+}
+
+bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas)
+{
+  // only if unsat core available
+  if (options::proof())
+  {
+    if (!ProofManager::currentPM()->unsatCoreAvailable())
+    {
+      return false;
+    }
+  }
+
+  Trace("inst-unsat-core") << "Get instantiations in unsat core..."
+                           << std::endl;
+  ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS,
+                                                  active_lemmas);
+  if (Trace.isOn("inst-unsat-core"))
+  {
+    Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: "
+                             << std::endl;
+    for (const Node& lem : active_lemmas)
+    {
+      Trace("inst-unsat-core") << "  " << lem << std::endl;
+    }
+    Trace("inst-unsat-core") << std::endl;
+  }
+  return true;
+}
+
+bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
+                                     std::map<Node, Node>& weak_imp)
+{
+  if (getUnsatCoreLemmas(active_lemmas))
+  {
+    for (unsigned i = 0, size = active_lemmas.size(); i < size; ++i)
+    {
+      Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(
+          active_lemmas[i]);
+      if (n != active_lemmas[i])
+      {
+        Trace("inst-unsat-core") << "  weaken : " << active_lemmas[i] << " -> "
+                                 << n << std::endl;
+      }
+      weak_imp[active_lemmas[i]] = n;
+    }
+    return true;
+  }
+  return false;
+}
+
+void Instantiate::getInstantiationTermVectors(
+    Node q, std::vector<std::vector<Node> >& tvecs)
+{
+  std::vector<Node> lemmas;
+  getInstantiations(q, lemmas);
+  std::map<Node, Node> quant;
+  std::map<Node, std::vector<Node> > tvec;
+  getExplanationForInstLemmas(lemmas, quant, tvec);
+  for (std::pair<const Node, std::vector<Node> >& t : tvec)
+  {
+    tvecs.push_back(t.second);
+  }
+}
+
+void Instantiate::getInstantiationTermVectors(
+    std::map<Node, std::vector<std::vector<Node> > >& insts)
+{
+  if (options::incrementalSolving())
+  {
+    for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+    {
+      getInstantiationTermVectors(t.first, insts[t.first]);
+    }
+  }
+  else
+  {
+    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+    {
+      getInstantiationTermVectors(t.first, insts[t.first]);
+    }
+  }
+}
+
+void Instantiate::getExplanationForInstLemmas(
+    const std::vector<Node>& lems,
+    std::map<Node, Node>& quant,
+    std::map<Node, std::vector<Node> >& tvec)
+{
+  if (options::trackInstLemmas())
+  {
+    if (options::incrementalSolving())
+    {
+      for (std::pair<const Node, inst::CDInstMatchTrie*>& t :
+           d_c_inst_match_trie)
+      {
+        t.second->getExplanationForInstLemmas(t.first, lems, quant, tvec);
+      }
+    }
+    else
+    {
+      for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+      {
+        t.second.getExplanationForInstLemmas(t.first, lems, quant, tvec);
+      }
+    }
+#ifdef CVC4_ASSERTIONS
+    for (unsigned j = 0; j < lems.size(); j++)
+    {
+      Assert(quant.find(lems[j]) != quant.end());
+      Assert(tvec.find(lems[j]) != tvec.end());
+    }
+#endif
+  }
+  Assert(false);
+}
+
+void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts)
+{
+  bool useUnsatCore = false;
+  std::vector<Node> active_lemmas;
+  if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas))
+  {
+    useUnsatCore = true;
+  }
+
+  if (options::incrementalSolving())
+  {
+    for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+    {
+      t.second->getInstantiations(
+          insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas);
+    }
+  }
+  else
+  {
+    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+    {
+      t.second.getInstantiations(
+          insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas);
+    }
+  }
+}
+
+void Instantiate::getInstantiations(Node q, std::vector<Node>& insts)
+{
+  if (options::incrementalSolving())
+  {
+    std::map<Node, inst::CDInstMatchTrie*>::iterator it =
+        d_c_inst_match_trie.find(q);
+    if (it != d_c_inst_match_trie.end())
+    {
+      std::vector<Node> active_lemmas;
+      it->second->getInstantiations(
+          insts, it->first, d_qe, false, active_lemmas);
+    }
+  }
+  else
+  {
+    std::map<Node, inst::InstMatchTrie>::iterator it =
+        d_inst_match_trie.find(q);
+    if (it != d_inst_match_trie.end())
+    {
+      std::vector<Node> active_lemmas;
+      it->second.getInstantiations(
+          insts, it->first, d_qe, false, active_lemmas);
+    }
+  }
+}
+
+Node Instantiate::getInstantiatedConjunction(Node q)
+{
+  Assert(q.getKind() == FORALL);
+  std::vector<Node> insts;
+  getInstantiations(q, insts);
+  if (insts.empty())
+  {
+    return NodeManager::currentNM()->mkConst(true);
+  }
+  Node ret;
+  if (insts.size() == 1)
+  {
+    ret = insts[0];
+  }
+  else
+  {
+    ret = NodeManager::currentNM()->mkNode(kind::AND, insts);
+  }
+  // have to remove q
+  // may want to do this in a better way
+  TNode tq = q;
+  TNode tt = NodeManager::currentNM()->mkConst(true);
+  ret = ret.substitute(tq, tt);
+  return ret;
+}
+
+void Instantiate::debugPrint()
+{
+  // debug information
+  if (Trace.isOn("inst-per-quant-round"))
+  {
+    for (std::pair<const Node, int>& i : d_temp_inst_debug)
+    {
+      Trace("inst-per-quant-round") << " * " << i.second << " for " << i.first
+                                    << std::endl;
+      d_temp_inst_debug[i.first] = 0;
+    }
+  }
+}
+
+void Instantiate::debugPrintModel()
+{
+  if (Trace.isOn("inst-per-quant"))
+  {
+    for (std::pair<const Node, int>& i : d_total_inst_debug)
+    {
+      Trace("inst-per-quant") << " * " << i.second << " for " << i.first
+                              << std::endl;
+    }
+  }
+}
+
+Instantiate::Statistics::Statistics()
+    : d_instantiations("Instantiate::Instantiations_Total", 0),
+      d_inst_duplicate("Instantiate::Duplicate_Inst", 0),
+      d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0),
+      d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0),
+      d_inst_duplicate_model_true("Instantiate::Duplicate_Inst_Model_True", 0)
+{
+  smtStatisticsRegistry()->registerStat(&d_instantiations);
+  smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
+  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
+  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
+  smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true);
+}
+
+Instantiate::Statistics::~Statistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_instantiations);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
+  smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true);
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */