projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2ca4e06) | patch
Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Minor fixes...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 8 May 2014 13:13:05 +0000 (08:13 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 8 May 2014 13:13:05 +0000 (08:13 -0500)
commitce831651caf58c1005fd3ebfdd2b75923d594328
tree8787737dde71b80722bbf39718c38e739596d9fdtree
parent2ca4e063ca007851ebf73ccb2ac6b7c85e73133dcommit | diff
Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers.  Minor fixes to ambqi.  Preparation for CASC proof output.  Add NNF option.
src/theory/quantifiers/ambqi_builder.cpp diff | blob | history
src/theory/quantifiers/inst_match.cpp diff | blob | history
src/theory/quantifiers/inst_match.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history