1 files changed, 80 insertions, 15 deletions

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 53e9c6832..d40a2c13d 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -37,7 +37,7 @@ 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_total_inst_debug(u),
       d_c_inst_match_trie_dom(u)
 {
 }
@@ -264,9 +264,8 @@ bool Instantiate::addInstantiation(
     return false;
   }
 
-  d_total_inst_debug[q]++;
+  d_total_inst_debug[q] = d_total_inst_debug[q] + 1;
   d_temp_inst_debug[q]++;
-  d_total_inst_count_debug++;
   if (Trace.isOn("inst"))
   {
     Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
@@ -466,6 +465,16 @@ Node Instantiate::getTermForType(TypeNode tn)
 
 bool Instantiate::printInstantiations(std::ostream& out)
 {
+  if (options::printInstMode() == options::PrintInstMode::NUM)
+  {
+    return printInstantiationsNum(out);
+  }
+  Assert(options::printInstMode() == options::PrintInstMode::LIST);
+  return printInstantiationsList(out);
+}
+
+bool Instantiate::printInstantiationsList(std::ostream& out)
+{
   bool useUnsatCore = false;
   std::vector<Node> active_lemmas;
   if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas))
@@ -473,35 +482,89 @@ bool Instantiate::printInstantiations(std::ostream& out)
     useUnsatCore = true;
   }
   bool printed = false;
+  bool isFull = options::printInstFull();
   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)
+      std::stringstream qout;
+      if (!printQuant(t.first, qout, isFull))
+      {
+        continue;
+      }
+      std::stringstream sout;
+      t.second->print(sout, t.first, useUnsatCore, active_lemmas);
+      if (!sout.str().empty())
       {
+        out << "(instantiations " << qout.str() << std::endl;
+        out << sout.str();
         out << ")" << std::endl;
+        printed = true;
       }
-      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)
+      std::stringstream qout;
+      if (!printQuant(t.first, qout, isFull))
+      {
+        continue;
+      }
+      std::stringstream sout;
+      t.second.print(sout, t.first, useUnsatCore, active_lemmas);
+      if (!sout.str().empty())
       {
+        out << "(instantiations " << qout.str() << std::endl;
+        out << sout.str();
         out << ")" << std::endl;
+        printed = true;
       }
-      printed = printed || !firstTime;
     }
   }
+  out << std::endl;
   return printed;
 }
 
+bool Instantiate::printInstantiationsNum(std::ostream& out)
+{
+  if (d_total_inst_debug.empty())
+  {
+    return false;
+  }
+  bool isFull = options::printInstFull();
+  for (NodeUIntMap::iterator it = d_total_inst_debug.begin();
+       it != d_total_inst_debug.end();
+       ++it)
+  {
+    std::stringstream ss;
+    if (printQuant((*it).first, ss, isFull))
+    {
+      out << "(num-instantiations " << ss.str() << " " << (*it).second << ")"
+          << std::endl;
+    }
+  }
+  return true;
+}
+
+bool Instantiate::printQuant(Node q, std::ostream& out, bool isFull)
+{
+  if (isFull)
+  {
+    out << q;
+    return true;
+  }
+  quantifiers::QuantAttributes* qa = d_qe->getQuantAttributes();
+  Node name = qa->getQuantName(q);
+  if (name.isNull())
+  {
+    return false;
+  }
+  out << name;
+  return true;
+}
+
 void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
 {
   if (options::incrementalSolving())
@@ -726,7 +789,7 @@ void Instantiate::debugPrint()
   // debug information
   if (Trace.isOn("inst-per-quant-round"))
   {
-    for (std::pair<const Node, int>& i : d_temp_inst_debug)
+    for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
     {
       Trace("inst-per-quant-round") << " * " << i.second << " for " << i.first
                                     << std::endl;
@@ -739,10 +802,12 @@ void Instantiate::debugPrintModel()
 {
   if (Trace.isOn("inst-per-quant"))
   {
-    for (std::pair<const Node, int>& i : d_total_inst_debug)
+    for (NodeUIntMap::iterator it = d_total_inst_debug.begin();
+         it != d_total_inst_debug.end();
+         ++it)
     {
-      Trace("inst-per-quant") << " * " << i.second << " for " << i.first
-                              << std::endl;
+      Trace("inst-per-quant")
+          << " * " << (*it).second << " for " << (*it).first << std::endl;
     }
   }
 }