Implement simple tracking of instantiation lemmas (#6077)

We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution.

This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination.

Fixes #5899.

6 files changed, 115 insertions, 90 deletions

diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 9a0178cfe..ba11319d3 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -99,21 +99,11 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
       Assert(topq.getKind() == FORALL);
       Trace("smt-qe") << "Get qe based on preprocessed quantified formula "
                       << topq << std::endl;
-      std::vector<std::vector<Node>> insts;
-      qe->getInstantiationTermVectors(topq, insts);
-      std::vector<Node> vars(ne[0].begin(), ne[0].end());
-      std::vector<Node> conjs;
-      // apply the instantiation on the original body
-      for (const std::vector<Node>& inst : insts)
-      {
-        // note we do not convert to witness form here, since we could be
-        // an internal subsolver
-        Subs s;
-        s.add(vars, inst);
-        Node c = s.apply(ne[1].negate());
-        conjs.push_back(c);
-      }
-      ret = nm->mkAnd(conjs);
+      std::vector<Node> insts;
+      qe->getInstantiations(topq, insts);
+      // note we do not convert to witness form here, since we could be
+      // an internal subsolver (SmtEngine::isInternalSubsolver).
+      ret = nm->mkAnd(insts);
       Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl;
       if (q.getKind() == EXISTS)
       {
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 3690cbcac..19821d347 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -473,23 +473,23 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
 
 bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   Assert(!d_curr_quant.isNull());
+  // check if we need virtual term substitution (if used delta or infinity)
+  bool usedVts = d_vtsCache->containsVtsTerm(subs, false);
   Instantiate* inst = d_qim.getInstantiate();
   //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
   if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant))
   {
     d_cbqi_set_quant_inactive = true;
     d_incomplete_check = true;
-    inst->recordInstantiation(d_curr_quant, subs, false, false);
+    inst->recordInstantiation(d_curr_quant, subs, usedVts);
     return true;
   }
-  // check if we need virtual term substitution (if used delta or infinity)
-  bool used_vts = d_vtsCache->containsVtsTerm(subs, false);
-  if (inst->addInstantiation(d_curr_quant,
-                             subs,
-                             InferenceId::QUANTIFIERS_INST_CEGQI,
-                             false,
-                             false,
-                             used_vts))
+  else if (inst->addInstantiation(d_curr_quant,
+                                  subs,
+                                  InferenceId::QUANTIFIERS_INST_CEGQI,
+                                  false,
+                                  false,
+                                  usedVts))
   {
     return true;
   }
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 61c7703ed..b74f4ae0f 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -51,7 +51,7 @@ Instantiate::Instantiate(QuantifiersState& qs,
       d_qreg(qr),
       d_treg(tr),
       d_pnm(pnm),
-      d_total_inst_debug(qs.getUserContext()),
+      d_insts(qs.getUserContext()),
       d_c_inst_match_trie_dom(qs.getUserContext()),
       d_pfInst(pnm ? new CDProof(pnm) : nullptr)
 {
@@ -68,24 +68,16 @@ Instantiate::~Instantiate()
 
 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();
-  }
+  Trace("inst-debug") << "Reset, effort " << e << std::endl;
+  // clear explicitly recorded instantiations
+  d_recordedInst.clear();
   return true;
 }
 
 void Instantiate::registerQuantifier(Node q) {}
 bool Instantiate::checkComplete()
 {
-  if (!d_recorded_inst.empty())
+  if (!d_recordedInst.empty())
   {
     Trace("quant-engine-debug")
         << "Set incomplete due to recorded instantiations." << std::endl;
@@ -337,7 +329,10 @@ bool Instantiate::addInstantiation(Node q,
     return false;
   }
 
-  d_total_inst_debug[q] = d_total_inst_debug[q] + 1;
+  // add to list of instantiations
+  InstLemmaList* ill = getOrMkInstLemmaList(q);
+  ill->d_list.push_back(body);
+  // add to temporary debug statistics (# inst on this round)
   d_temp_inst_debug[q]++;
   if (Trace.isOn("inst"))
   {
@@ -480,12 +475,16 @@ bool Instantiate::addInstantiationExpFail(Node q,
   return false;
 }
 
-bool Instantiate::recordInstantiation(Node q,
+void Instantiate::recordInstantiation(Node q,
                                       std::vector<Node>& terms,
-                                      bool modEq,
-                                      bool addedLem)
+                                      bool doVts)
 {
-  return recordInstantiationInternal(q, terms, modEq, addedLem);
+  Trace("inst-debug") << "Record instantiation for " << q << std::endl;
+  // get the instantiation list, which ensures that q is marked as a quantified
+  // formula we instantiated, despite only recording an instantiation here
+  getOrMkInstLemmaList(q);
+  Node inst = getInstantiation(q, terms, doVts);
+  d_recordedInst[q].push_back(inst);
 }
 
 bool Instantiate::existsInstantiation(Node q,
@@ -562,14 +561,8 @@ Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
 
 bool Instantiate::recordInstantiationInternal(Node q,
                                               std::vector<Node>& terms,
-                                              bool modEq,
-                                              bool addedLem)
+                                              bool modEq)
 {
-  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")
@@ -607,24 +600,13 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)
   return d_inst_match_trie[q].removeInstMatch(q, terms);
 }
 
-void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
+void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) const
 {
-  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 (NodeInstListMap::const_iterator it = d_insts.begin();
+       it != d_insts.end();
+       ++it)
   {
-    for (std::pair<const Node, InstMatchTrie>& t : d_inst_match_trie)
-    {
-      qs.push_back(t.first);
-    }
+    qs.push_back(it->first);
   }
 }
 
@@ -671,6 +653,20 @@ void Instantiate::getInstantiationTermVectors(
   }
 }
 
+void Instantiate::getInstantiations(Node q, std::vector<Node>& insts)
+{
+  Trace("inst-debug") << "get instantiations for " << q << std::endl;
+  InstLemmaList* ill = getOrMkInstLemmaList(q);
+  insts.insert(insts.end(), ill->d_list.begin(), ill->d_list.end());
+  // also include recorded instantations (for qe-partial)
+  std::map<Node, std::vector<Node> >::const_iterator it =
+      d_recordedInst.find(q);
+  if (it != d_recordedInst.end())
+  {
+    insts.insert(insts.end(), it->second.begin(), it->second.end());
+  }
+}
+
 bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
 
 void Instantiate::debugPrint(std::ostream& out)
@@ -705,12 +701,11 @@ void Instantiate::debugPrintModel()
 {
   if (Trace.isOn("inst-per-quant"))
   {
-    for (NodeUIntMap::iterator it = d_total_inst_debug.begin();
-         it != d_total_inst_debug.end();
+    for (NodeInstListMap::iterator it = d_insts.begin(); it != d_insts.end();
          ++it)
     {
-      Trace("inst-per-quant")
-          << " * " << (*it).second << " for " << (*it).first << std::endl;
+      Trace("inst-per-quant") << " * " << (*it).second->d_list.size() << " for "
+                              << (*it).first << std::endl;
     }
   }
 }
@@ -731,6 +726,19 @@ Node Instantiate::ensureType(Node n, TypeNode tn)
   return Node::null();
 }
 
+InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q)
+{
+  NodeInstListMap::iterator it = d_insts.find(q);
+  if (it != d_insts.end())
+  {
+    return it->second.get();
+  }
+  std::shared_ptr<InstLemmaList> ill =
+      std::make_shared<InstLemmaList>(d_qstate.getUserContext());
+  d_insts.insert(q, ill);
+  return ill.get();
+}
+
 Instantiate::Statistics::Statistics()
     : d_instantiations("Instantiate::Instantiations_Total", 0),
       d_inst_duplicate("Instantiate::Duplicate_Inst", 0),
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index be410c2c8..94e16b526 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -69,6 +69,15 @@ class InstantiationRewriter
                                          bool doVts) = 0;
 };
 
+/** Context-dependent list of nodes */
+class InstLemmaList
+{
+ public:
+  InstLemmaList(context::Context* c) : d_list(c) {}
+  /** The list */
+  context::CDList<Node> d_list;
+};
+
 /** Instantiate
  *
  * This class is used for generating instantiation lemmas.  It maintains an
@@ -90,7 +99,8 @@ class InstantiationRewriter
  */
 class Instantiate : public QuantifiersUtil
 {
-  typedef context::CDHashMap<Node, uint32_t, NodeHashFunction> NodeUIntMap;
+  using NodeInstListMap = context::
+      CDHashMap<Node, std::shared_ptr<InstLemmaList>, NodeHashFunction>;
 
  public:
   Instantiate(QuantifiersState& qs,
@@ -187,13 +197,13 @@ class Instantiate : public QuantifiersUtil
                                bool expFull = true);
   /** record instantiation
    *
-   * Explicitly record that q has been instantiated with terms. This is the
-   * same as addInstantiation, but does not enqueue an instantiation lemma.
+   * Explicitly record that q has been instantiated with terms, with virtual
+   * term substitution if doVts is true. This is the same as addInstantiation,
+   * but does not enqueue an instantiation lemma.
    */
-  bool recordInstantiation(Node q,
+  void recordInstantiation(Node q,
                            std::vector<Node>& terms,
-                           bool modEq = false,
-                           bool addedLem = true);
+                           bool doVts = false);
   /** exists instantiation
    *
    * Returns true if and only if the instantiation already was added or
@@ -240,7 +250,7 @@ class Instantiate : public QuantifiersUtil
    * Get the list of quantified formulas that were instantiated in the current
    * user context, store them in qs.
    */
-  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
+  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) const;
   /** get instantiation term vectors
    *
    * Get term vectors corresponding to for all instantiations lemmas added in
@@ -255,6 +265,11 @@ class Instantiate : public QuantifiersUtil
    */
   void getInstantiationTermVectors(
       std::map<Node, std::vector<std::vector<Node> > >& insts);
+  /**
+   * Get instantiations for quantified formula q. If q is (forall ((x T)) (P
+   * x)), this is a list of the form (P t1) ... (P tn) for ground terms ti.
+   */
+  void getInstantiations(Node q, std::vector<Node>& insts);
   //--------------------------------------end user-level interface utilities
 
   /** Are proofs enabled for this object? */
@@ -281,15 +296,12 @@ class Instantiate : public QuantifiersUtil
  private:
   /** record instantiation, return true if it was not a duplicate
    *
-   * addedLem : whether an instantiation lemma was added for the vector we are
-   *            recording. If this is false, we bookkeep the vector.
    * modEq : whether to check for duplication modulo equality in instantiation
    *         tries (for performance),
    */
   bool recordInstantiationInternal(Node q,
                                    std::vector<Node>& terms,
-                                   bool modEq = false,
-                                   bool addedLem = true);
+                                   bool modEq = false);
   /** remove instantiation from the cache */
   bool removeInstantiationInternal(Node q, std::vector<Node>& terms);
   /**
@@ -297,6 +309,8 @@ class Instantiate : public QuantifiersUtil
    * if possible.
    */
   static Node ensureType(Node n, TypeNode tn);
+  /** Get or make the instantiation list for quantified formula q */
+  InstLemmaList* getOrMkInstLemmaList(TNode q);
 
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
@@ -311,8 +325,19 @@ class Instantiate : public QuantifiersUtil
   /** instantiation rewriter classes */
   std::vector<InstantiationRewriter*> d_instRewrite;
 
-  /** statistics for debugging total instantiations per quantifier */
-  NodeUIntMap d_total_inst_debug;
+  /**
+   * The list of all instantiation lemma bodies per quantifier. This is used
+   * for debugging and for quantifier elimination.
+   */
+  NodeInstListMap d_insts;
+  /** explicitly recorded instantiations
+   *
+   * Sometimes an instantiation is recorded internally but not sent out as a
+   * lemma, for instance, for partial quantifier elimination. This is a map
+   * of these instantiations, for each quantified formula. This map is cleared
+   * on presolve, e.g. it is local to a check-sat call.
+   */
+  std::map<Node, std::vector<Node> > d_recordedInst;
   /** statistics for debugging total instantiations per quantifier per round */
   std::map<Node, uint32_t> d_temp_inst_debug;
 
@@ -328,14 +353,6 @@ class Instantiate : public QuantifiersUtil
    * is valid.
    */
   context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom;
-
-  /** explicitly recorded instantiations
-   *
-   * Sometimes an instantiation is recorded internally but not sent out as a
-   * lemma, for instance, for partial quantifier elimination. This is a map
-   * of these instantiations, for each quantified formula.
-   */
-  std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst;
   /**
    * A CDProof storing instantiation steps.
    */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8d8f54768..f1ca0dd9f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -630,6 +630,11 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector
   d_qim.getInstantiate()->getInstantiationTermVectors(insts);
 }
 
+void QuantifiersEngine::getInstantiations(Node q, std::vector<Node>& insts)
+{
+  d_qim.getInstantiate()->getInstantiations(q, insts);
+}
+
 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
   if (d_qmodules->d_synth_e)
   {
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 28f162ddd..d05137e80 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -155,6 +155,11 @@ public:
  void getInstantiationTermVectors(
      std::map<Node, std::vector<std::vector<Node> > >& insts);
  /**
+  * Get instantiations for quantified formula q. If q is (forall ((x T)) (P x)),
+  * this is a list of the form (P t1) ... (P tn) for ground terms ti.
+  */
+ void getInstantiations(Node q, std::vector<Node>& insts);
+ /**
   * Get skolemization vectors, where for each quantified formula that was
   * skolemized, this is the list of skolems that were used to witness the
   * negation of that quantified formula.