Add optional debug information for dumping instantiations (#6950)

This complete the implementation of dump-instantiations-debug.

With this option, we can print the source of instantiations. For example:

$ cvc5 regress1/quantifiers/dump-inst-proof.smt2 --dump-instantiations-debug --produce-proofs
unsat
(instantiations (forall ((x Int)) (or (P x) (Q x)))
  (! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (P x) true))))
)
(instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))))
  (! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (S x) false))))
)

14 files changed, 176 insertions, 56 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index bf658dfe0..5431a8348 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -174,7 +174,8 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
       getterCommands.emplace_back(new GetProofCommand());
     }
 
-    if (d_solver->getOptions().driver.dumpInstantiations
+    if ((d_solver->getOptions().driver.dumpInstantiations
+         || d_solver->getOptions().driver.dumpInstantiationsDebug)
         && GetInstantiationsCommand::isEnabled(d_solver.get(), res))
     {
       getterCommands.emplace_back(new GetInstantiationsCommand());
diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index 19bb97f34..869d411bd 100644
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -113,6 +113,14 @@ public = true
   help       = "output instantiations of quantified formulas after every UNSAT/VALID response"
 
 [[option]]
+  name       = "dumpInstantiationsDebug"
+  category   = "regular"
+  long       = "dump-instantiations-debug"
+  type       = "bool"
+  default    = "false"
+  help       = "output instantiations of quantified formulas after every UNSAT/VALID response, with debug information"
+
+[[option]]
   name       = "dumpUnsatCores"
   category   = "regular"
   long       = "dump-unsat-cores"
@@ -134,4 +142,4 @@ public = true
   long       = "force-no-limit-cpu-while-dump"
   type       = "bool"
   default    = "false"
-  help       = "Force no CPU limit when dumping models and proofs"
\ No newline at end of file
+  help       = "Force no CPU limit when dumping models and proofs"
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index b733f62ce..69727e1a2 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -101,14 +101,29 @@ void Printer::toStream(std::ostream& out, const UnsatCore& core) const
 void Printer::toStream(std::ostream& out, const InstantiationList& is) const
 {
   out << "(instantiations " << is.d_quant << std::endl;
-  for (const std::vector<Node>& i : is.d_inst)
+  for (const InstantiationVec& i : is.d_inst)
   {
-    out << "  ( ";
-    for (const Node& n : i)
+    out << "  ";
+    if (i.d_id != theory::InferenceId::UNKNOWN)
+    {
+      out << "(! ";
+    }
+    out << "( ";
+    for (const Node& n : i.d_vec)
     {
       out << n << " ";
     }
-    out << ")" << std::endl;
+    out << ")";
+    if (i.d_id != theory::InferenceId::UNKNOWN)
+    {
+      out << " :source " << i.d_id;
+      if (!i.d_pfArg.isNull())
+      {
+        out << " " << i.d_pfArg;
+      }
+      out << ")";
+    }
+    out << std::endl;
   }
   out << ")" << std::endl;
 }
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index ad9a8f844..66f9fde7c 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -1182,7 +1182,10 @@ bool ProofPostprocessCallback::addToTransChildren(Node eq,
 ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
     ProofNodeManager* pnm)
     : d_ruleCount(smtStatisticsRegistry().registerHistogram<PfRule>(
-        "finalProof::ruleCount")),
+          "finalProof::ruleCount")),
+      d_instRuleIds(
+          smtStatisticsRegistry().registerHistogram<theory::InferenceId>(
+              "finalProof::instRuleId")),
       d_totalRuleCount(
           smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")),
       d_minPedanticLevel(
@@ -1227,6 +1230,20 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
   // record stats for the rule
   d_ruleCount << r;
   ++d_totalRuleCount;
+  // take stats on the instantiations in the proof
+  if (r == PfRule::INSTANTIATE)
+  {
+    Node q = pn->getChildren()[0]->getResult();
+    const std::vector<Node>& args = pn->getArguments();
+    if (args.size() > q[0].getNumChildren())
+    {
+      InferenceId id;
+      if (getInferenceId(args[q[0].getNumChildren()], id))
+      {
+        d_instRuleIds << id;
+      }
+    }
+  }
   return false;
 }
 
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index f9e93fa91..056f77695 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -24,6 +24,7 @@
 
 #include "proof/proof_node_updater.h"
 #include "smt/witness_form.h"
+#include "theory/inference_id.h"
 #include "util/statistics_stats.h"
 
 namespace cvc5 {
@@ -256,6 +257,11 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
  private:
   /** Counts number of postprocessed proof nodes for each kind of proof rule */
   HistogramStat<PfRule> d_ruleCount;
+  /**
+   * Counts number of postprocessed proof nodes of rule INSTANTIATE that were
+   * marked with the given inference id.
+   */
+  HistogramStat<theory::InferenceId> d_instRuleIds;
   /** Total number of postprocessed rule applications */
   IntStat d_totalRuleCount;
   /** The minimum pedantic level of any rule encountered */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 55f3d1c5f..5f3920929 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1561,7 +1561,7 @@ UnsatCore SmtEngine::getUnsatCore() {
 }
 
 void SmtEngine::getRelevantInstantiationTermVectors(
-    std::map<Node, std::vector<std::vector<Node>>>& insts)
+    std::map<Node, InstantiationList>& insts, bool getDebugInfo)
 {
   Assert(d_state->getMode() == SmtMode::UNSAT);
   // generate with new proofs
@@ -1570,7 +1570,7 @@ void SmtEngine::getRelevantInstantiationTermVectors(
   Assert(pe->getProof() != nullptr);
   std::shared_ptr<ProofNode> pfn =
       d_pfManager->getFinalProof(pe->getProof(), *d_asserts);
-  d_ucManager->getRelevantInstantiations(pfn, insts);
+  d_ucManager->getRelevantInstantiations(pfn, insts, getDebugInfo);
 }
 
 std::string SmtEngine::getProof()
@@ -1635,11 +1635,36 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   }
 
   // Second, extract and print the instantiations
-  std::map<Node, std::vector<std::vector<Node>>> insts;
-  getInstantiationTermVectors(insts);
-  for (const std::pair<const Node, std::vector<std::vector<Node>>>& i : insts)
+  std::map<Node, InstantiationList> rinsts;
+  if (d_env->getOptions().smt.produceProofs
+      && (!d_env->getOptions().smt.unsatCores
+          || d_env->getOptions().smt.unsatCoresMode
+                 == options::UnsatCoresMode::FULL_PROOF)
+      && getSmtMode() == SmtMode::UNSAT)
   {
-    if (i.second.empty())
+    // minimize instantiations based on proof manager
+    getRelevantInstantiationTermVectors(rinsts,
+                                        options::dumpInstantiationsDebug());
+  }
+  else
+  {
+    std::map<Node, std::vector<std::vector<Node>>> insts;
+    getInstantiationTermVectors(insts);
+    for (const std::pair<const Node, std::vector<std::vector<Node>>>& i : insts)
+    {
+      // convert to instantiation list
+      Node q = i.first;
+      InstantiationList& ilq = rinsts[q];
+      ilq.initialize(q);
+      for (const std::vector<Node>& ii : i.second)
+      {
+        ilq.d_inst.push_back(InstantiationVec(ii));
+      }
+    }
+  }
+  for (std::pair<const Node, InstantiationList>& i : rinsts)
+  {
+    if (i.second.d_inst.empty())
     {
       // no instantiations, skip
       continue;
@@ -1653,22 +1678,23 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
     // must have a name
     if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::NUM)
     {
-      out << "(num-instantiations " << name << " " << i.second.size() << ")"
-          << std::endl;
+      out << "(num-instantiations " << name << " " << i.second.d_inst.size()
+          << ")" << std::endl;
     }
     else
     {
+      // take the name
+      i.second.d_quant = name;
       Assert(d_env->getOptions().printer.printInstMode
              == options::PrintInstMode::LIST);
-      InstantiationList ilist(name, i.second);
-      out << ilist;
+      out << i.second;
     }
     printed = true;
   }
   // if we did not print anything, we indicate this
   if (!printed)
   {
-    out << "No instantiations" << std::endl;
+    out << "none" << std::endl;
   }
   if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
   {
@@ -1681,21 +1707,10 @@ void SmtEngine::getInstantiationTermVectors(
 {
   SmtScope smts(this);
   finishInit();
-  if (d_env->getOptions().smt.produceProofs
-      && (!d_env->getOptions().smt.unsatCores
-          || d_env->getOptions().smt.unsatCoresMode == options::UnsatCoresMode::FULL_PROOF)
-      && getSmtMode() == SmtMode::UNSAT)
-  {
-    // minimize instantiations based on proof manager
-    getRelevantInstantiationTermVectors(insts);
-  }
-  else
-  {
-    QuantifiersEngine* qe =
-        getAvailableQuantifiersEngine("getInstantiationTermVectors");
-    // otherwise, just get the list of all instantiations
-    qe->getInstantiationTermVectors(insts);
-  }
+  QuantifiersEngine* qe =
+      getAvailableQuantifiersEngine("getInstantiationTermVectors");
+  // get the list of all instantiations
+  qe->getInstantiationTermVectors(insts);
 }
 
 bool SmtEngine::getSynthSolutions(std::map<Node, Node>& solMap)
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 68b1caad0..d00fa0c76 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -46,6 +46,7 @@ class LogicRequest;
 class StatisticsRegistry;
 class Printer;
 class ResourceManager;
+struct InstantiationList;
 
 /* -------------------------------------------------------------------------- */
 
@@ -673,7 +674,7 @@ class CVC5_EXPORT SmtEngine
    * refutation.
    */
   void getRelevantInstantiationTermVectors(
-      std::map<Node, std::vector<std::vector<Node>>>& insts);
+      std::map<Node, InstantiationList>& insts, bool getDebugInfo = false);
   /**
    * Get instantiation term vectors, which maps each instantiated quantified
    * formula to the list of instantiations for that quantified formula. This
diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp
index 22304f9e8..01025e505 100644
--- a/src/smt/unsat_core_manager.cpp
+++ b/src/smt/unsat_core_manager.cpp
@@ -56,12 +56,13 @@ void UnsatCoreManager::getUnsatCore(std::shared_ptr<ProofNode> pfn,
 
 void UnsatCoreManager::getRelevantInstantiations(
     std::shared_ptr<ProofNode> pfn,
-    std::map<Node, std::vector<std::vector<Node>>>& insts)
+    std::map<Node, InstantiationList>& insts,
+    bool getDebugInfo)
 {
   std::unordered_map<ProofNode*, bool> visited;
   std::unordered_map<ProofNode*, bool>::iterator it;
   std::vector<std::shared_ptr<ProofNode>> visit;
-
+  std::map<Node, InstantiationList>::iterator itq;
   std::shared_ptr<ProofNode> cur;
   visit.push_back(pfn);
   do
@@ -82,8 +83,27 @@ void UnsatCoreManager::getRelevantInstantiations(
       Node q = cs[0]->getResult();
       // the instantiation is a prefix of the arguments up to the number of
       // variables
-      insts[q].push_back(
-          {instTerms.begin(), instTerms.begin() + q[0].getNumChildren()});
+      itq = insts.find(q);
+      if (itq == insts.end())
+      {
+        insts[q].initialize(q);
+        itq = insts.find(q);
+      }
+      itq->second.d_inst.push_back(InstantiationVec(
+          {instTerms.begin(), instTerms.begin() + q[0].getNumChildren()}));
+      if (getDebugInfo)
+      {
+        std::vector<Node> extraArgs(instTerms.begin() + q[0].getNumChildren(),
+                                    instTerms.end());
+        if (extraArgs.size() >= 1)
+        {
+          getInferenceId(extraArgs[0], itq->second.d_inst.back().d_id);
+        }
+        if (extraArgs.size() >= 2)
+        {
+          itq->second.d_inst.back().d_pfArg = extraArgs[1];
+        }
+      }
     }
     for (const std::shared_ptr<ProofNode>& cp : cs)
     {
diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h
index e064b83a7..eb71c67ca 100644
--- a/src/smt/unsat_core_manager.h
+++ b/src/smt/unsat_core_manager.h
@@ -21,6 +21,7 @@
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "proof/proof_node.h"
+#include "theory/quantifiers/instantiation_list.h"
 
 namespace cvc5 {
 
@@ -61,9 +62,9 @@ class UnsatCoreManager
    * matrix with each row corresponding to the terms with which the respective
    * quantified formula is instiated.
    */
-  void getRelevantInstantiations(
-      std::shared_ptr<ProofNode> pfn,
-      std::map<Node, std::vector<std::vector<Node>>>& insts);
+  void getRelevantInstantiations(std::shared_ptr<ProofNode> pfn,
+                                 std::map<Node, InstantiationList>& insts,
+                                 bool getDebugInfo = false);
 
 }; /* class UnsatCoreManager */
 
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 8ed30ea98..bf13b75b1 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -16,6 +16,7 @@
 #include "theory/inference_id.h"
 
 #include <iostream>
+#include "proof/proof_checker.h"
 #include "util/rational.h"
 
 namespace cvc5 {
@@ -426,5 +427,16 @@ Node mkInferenceIdNode(InferenceId i)
   return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(i)));
 }
 
+bool getInferenceId(TNode n, InferenceId& i)
+{
+  uint32_t index;
+  if (!ProofRuleChecker::getUInt32(n, index))
+  {
+    return false;
+  }
+  i = static_cast<InferenceId>(index);
+  return true;
+}
+
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index b2bfe3657..e93803170 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -823,6 +823,9 @@ std::ostream& operator<<(std::ostream& out, InferenceId i);
 /** Make node from inference id */
 Node mkInferenceIdNode(InferenceId i);
 
+/** get an inference identifier from a node, return false if we fail */
+bool getInferenceId(TNode n, InferenceId& i);
+
 }  // namespace theory
 }  // namespace cvc5
 
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 3e3249629..63aabbfd6 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -59,7 +59,6 @@ Trigger::Trigger(QuantifiersState& qs,
     Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms);
     d_nodes.push_back(np);
   }
-  d_trNode = NodeManager::currentNM()->mkNode(SEXPR, d_nodes);
   if (Trace.isOn("trigger"))
   {
     QuantAttributes& qa = d_qreg.getQuantAttributes();
@@ -70,18 +69,19 @@ Trigger::Trigger(QuantifiersState& qs,
       Trace("trigger") << "   " << n << std::endl;
     }
   }
+  std::vector<Node> extNodes;
+  for (const Node& nt : d_nodes)
+  {
+    // note we must display the original form, so we go back to bound vars
+    Node ns = d_qreg.substituteInstConstantsToBoundVariables(nt, q);
+    extNodes.push_back(ns);
+  }
+  d_trNode = NodeManager::currentNM()->mkNode(SEXPR, extNodes);
   if (Output.isOn(options::OutputTag::TRIGGER))
   {
     QuantAttributes& qa = d_qreg.getQuantAttributes();
-    Output(options::OutputTag::TRIGGER)
-        << "(trigger " << qa.quantToString(q) << " (";
-    for (size_t i = 0, nnodes = d_nodes.size(); i < nnodes; i++)
-    {
-      // note we must display the original form, so we go back to bound vars
-      Node ns = d_qreg.substituteInstConstantsToBoundVariables(d_nodes[i], q);
-      Output(options::OutputTag::TRIGGER) << (i > 0 ? " " : "") << ns;
-    }
-    Output(options::OutputTag::TRIGGER) << "))" << std::endl;
+    Output(options::OutputTag::TRIGGER) << "(trigger " << qa.quantToString(q)
+                                        << " " << d_trNode << ")" << std::endl;
   }
   QuantifiersStatistics& stats = qs.getStats();
   if( d_nodes.size()==1 ){
diff --git a/src/theory/quantifiers/instantiation_list.cpp b/src/theory/quantifiers/instantiation_list.cpp
index db2e167fb..f4b52619a 100644
--- a/src/theory/quantifiers/instantiation_list.cpp
+++ b/src/theory/quantifiers/instantiation_list.cpp
@@ -20,6 +20,14 @@
 
 namespace cvc5 {
 
+InstantiationVec::InstantiationVec(const std::vector<Node>& vec,
+                                   theory::InferenceId id,
+                                   Node pfArg)
+    : d_vec(vec), d_id(id), d_pfArg(pfArg)
+{
+}
+
+void InstantiationList::initialize(Node q) { d_quant = q; }
 std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist)
 {
   Printer::getPrinter(options::outputLanguage())->toStream(out, ilist);
diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h
index d97383ba0..5e292375a 100644
--- a/src/theory/quantifiers/instantiation_list.h
+++ b/src/theory/quantifiers/instantiation_list.h
@@ -22,20 +22,33 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "theory/inference_id.h"
 
 namespace cvc5 {
 
+struct InstantiationVec
+{
+ public:
+  InstantiationVec(const std::vector<Node>& vec,
+                   theory::InferenceId id = theory::InferenceId::UNKNOWN,
+                   Node pfArg = Node::null());
+  /** The vector of terms */
+  std::vector<Node> d_vec;
+  /** The inference id */
+  theory::InferenceId d_id;
+  /** The proof argument */
+  Node d_pfArg;
+};
+
 /** A list of instantiations for a quantified formula */
 struct InstantiationList
 {
-  InstantiationList(Node q, const std::vector<std::vector<Node> >& inst)
-      : d_quant(q), d_inst(inst)
-  {
-  }
+  /** Initialize */
+  void initialize(Node q);
   /** The quantified formula */
   Node d_quant;
   /** The instantiation list */
-  std::vector<std::vector<Node> > d_inst;
+  std::vector<InstantiationVec> d_inst;
 };
 
 /** Print the instantiation list to stream out */