From d027f24ed72556c240b43c0fa3282927f9344c3e Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 15 Dec 2020 17:16:07 -0600
Subject: [PATCH] Improvements related to quantifiers printing (#5678)

Also fixes a bug where patterns would be printed with the wrong scope (that included the bound variable list).
---
 src/printer/smt2/smt2_printer.cpp                 |  6 ++++--
 src/theory/quantifiers/ematching/trigger.cpp      | 13 ++++++++++---
 src/theory/quantifiers/quantifiers_attributes.cpp |  8 ++++++++
 src/theory/quantifiers/quantifiers_attributes.h   |  2 ++
 4 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 81445d281..1b7143538 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -902,15 +902,17 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::WITNESS:
   {
     out << smtKindString(k, d_variant) << " ";
+    toStream(out, n[0], toDepth, lbind);
+    out << " ";
     if (n.getNumChildren() == 3)
     {
       out << "(! ";
     }
-    out << n[0] << " ";
     toStreamWithLetify(out, n[1], toDepth - 1, lbind);
     if (n.getNumChildren() == 3)
     {
-      out << n[2];
+      out << " ";
+      toStream(out, n[2], toDepth, lbind);
       out << ")";
     }
     out << ")";
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 8d18c62bf..62aa1bcc0 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
@@ -53,9 +54,15 @@ Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
     : d_quantEngine(qe), d_quant(q)
 {
   d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
-  Trace("trigger") << "Trigger for " << q << ": " << std::endl;
-  for( unsigned i=0; i<d_nodes.size(); i++ ){
-    Trace("trigger") << "   " << d_nodes[i] << std::endl;
+  if (Trace.isOn("trigger"))
+  {
+    quantifiers::QuantAttributes* qa = d_quantEngine->getQuantAttributes();
+    Trace("trigger") << "Trigger for " << qa->quantToString(q) << ": "
+                     << std::endl;
+    for (const Node& n : d_nodes)
+    {
+      Trace("trigger") << "   " << n << std::endl;
+    }
   }
   if( d_nodes.size()==1 ){
     if( isSimpleTrigger( d_nodes[0] ) ){
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 6d9c82ac3..15715152b 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -316,6 +316,14 @@ Node QuantAttributes::getQuantName(Node q) const
   return Node::null();
 }
 
+std::string QuantAttributes::quantToString(Node q) const
+{
+  std::stringstream ss;
+  Node name = getQuantName(q);
+  ss << (name.isNull() ? q : name);
+  return ss.str();
+}
+
 int QuantAttributes::getQuantIdNum( Node q ) {
   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
   if( it!=d_qattr.end() ){
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 9fdb127e6..91a0d504f 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -225,6 +225,8 @@ public:
   bool isInternal(Node q) const;
   /** get quant name, which is used for :qid */
   Node getQuantName(Node q) const;
+  /** Print quantified formula q, possibly using its name, if it has one */
+  std::string quantToString(Node q) const;
   /** get (internal) quant id num */
   int getQuantIdNum( Node q );
   /** get (internal)quant id num */
-- 
2.30.2