diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-15 17:16:07 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-15 17:16:07 -0600 |
| commit | d027f24ed72556c240b43c0fa3282927f9344c3e (patch) | |
| tree | 9e33bf117fdbca28227a6a9d0b540031bb942cd9 /src/theory | |
| parent | 2fda6c574c75fcc85f0d828a0af9435154eb1a96 (diff) | |
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).
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 13 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 2 |
3 files changed, 20 insertions, 3 deletions
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 */ |