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/quantifiers/quantifiers_attributes.cpp | |
| 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/quantifiers/quantifiers_attributes.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
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() ){ |