Statistics on instantiations per quantified formula. (#4719)

This adds a new print format for instantiations --print-instantiations=num, which prints the total number of instantations of quantified formulas. This count is user-context-dependent, which is in sync with the existing print-instantiation format (list).

It also simplifies and improves printing of Instantiation Tries.

1 files changed, 12 insertions, 1 deletions

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 17c625652..c00d3c579 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -50,8 +50,9 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
     SygusAttribute ca;
     n.setAttribute( ca, true );
   }
-  else if (attr == "quant-name")
+  else if (attr == "qid")
   {
+    // using z3 syntax "qid"
     Trace("quant-attr-debug") << "Set quant-name " << n << std::endl;
     QuantNameAttribute qna;
     n.setAttribute(qna, true);
@@ -303,6 +304,16 @@ bool QuantAttributes::isQuantElimPartial( Node q ) {
   }
 }
 
+Node QuantAttributes::getQuantName(Node q) const
+{
+  std::map<Node, QAttributes>::const_iterator it = d_qattr.find(q);
+  if (it != d_qattr.end())
+  {
+    return it->second.d_name;
+  }
+  return Node::null();
+}
+
 int QuantAttributes::getQuantIdNum( Node q ) {
   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
   if( it!=d_qattr.end() ){