projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2fda6c5) | patch
Improvements related to quantifiers printing (#5678)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 15 Dec 2020 23:16:07 +0000 (17:16 -0600)
committerGitHub <noreply@github.com>
Tue, 15 Dec 2020 23:16:07 +0000 (17:16 -0600)
commitd027f24ed72556c240b43c0fa3282927f9344c3e
tree9e33bf117fdbca28227a6a9d0b540031bb942cd9tree
parent2fda6c574c75fcc85f0d828a0af9435154eb1a96commit | 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).
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/quantifiers_attributes.cpp diff | blob | history
src/theory/quantifiers/quantifiers_attributes.h diff | blob | history