+/********************* */
+/*! \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 */