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).

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 81445d281f25263dfe6d5d123c2ef4f12d24f2f5..1b71435388e0a8dedf44486d7f7b9ebd18a378ad 100644 (file)
--- 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 8d18c62bf23ce91dc4ba0cd4ead5bfe31c1afeb8..62aa1bcc0022c22d8e7db21202643c217d728e34 100644 (file)
--- 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 6d9c82ac3f49a4c8c58971e42c46335fbdaef1df..15715152b8315b6a91d6b77a9adcab12219f916a 100644 (file)
--- 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 9fdb127e6839969cc27d74b1f100b6ffe83d757d..91a0d504f44d1533d0356902390b455b3925b040 100644 (file)
--- 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 */