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.h | |
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.h')
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 2 |
1 files changed, 2 insertions, 0 deletions
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 */ |