Remove track instantiations infrastructure (#5883)

This was used in the old method for unsat core tracking for instantiation lemmas, which will soon be subsumed.

This is also work towards eliminating the dependencies on quantifiers engine from Instantiate.

1 files changed, 0 insertions, 175 deletions

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 361796735..9588bba7f 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -383,19 +383,6 @@ bool Instantiate::addInstantiation(
           orig_body, q[1], maxInstLevel + 1);
     }
   }
-  if (options::trackInstLemmas())
-  {
-    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;
@@ -569,55 +556,9 @@ void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
   }
 }
 
-bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas)
-{
-  // only if unsat core available
-  if (options::unsatCores() && !isProofEnabled())
-  {
-    if (!ProofManager::currentPM()->unsatCoreAvailable())
-    {
-      return false;
-    }
-  }
-  else
-  {
-    return false;
-  }
-
-  Trace("inst-unsat-core") << "Get instantiations in unsat core..."
-                           << std::endl;
-  ProofManager::currentPM()->getLemmasInUnsatCore(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;
-}
-
 void Instantiate::getInstantiationTermVectors(
     Node q, std::vector<std::vector<Node> >& tvecs)
 {
-  // if track instantiations is true, we use the instantiation + explanation
-  // methods for doing minimization based on unsat cores.
-  if (options::trackInstLemmas())
-  {
-    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);
-    }
-    return;
-  }
 
   if (options::incrementalSolving())
   {
@@ -658,124 +599,8 @@ void Instantiate::getInstantiationTermVectors(
   }
 }
 
-void Instantiate::getExplanationForInstLemmas(
-    const std::vector<Node>& lems,
-    std::map<Node, Node>& quant,
-    std::map<Node, std::vector<Node> >& tvec)
-{
-  if (!options::trackInstLemmas())
-  {
-    std::stringstream msg;
-    msg << "Cannot get explanation for instantiations when --track-inst-lemmas "
-           "is false.";
-    throw OptionException(msg.str());
-  }
-  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
-}
-
 bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
 
-void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts)
-{
-  if (!options::trackInstLemmas())
-  {
-    std::stringstream msg;
-    msg << "Cannot get instantiations when --track-inst-lemmas is false.";
-    throw OptionException(msg.str());
-  }
-  std::vector<Node> active_lemmas;
-  bool useUnsatCore = getUnsatCoreLemmas(active_lemmas);
-
-  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(std::ostream& out)
 {
   // debug information