projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 798524d) | patch
Support nested quantifier elimination for get-qe command (#5490)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 20 Nov 2020 21:19:40 +0000 (15:19 -0600)
committerGitHub <noreply@github.com>
Fri, 20 Nov 2020 21:19:40 +0000 (15:19 -0600)
commit6beb76055b81510ec38a8b50f5ed35d2f5010139
tree87c8b09f26091794943bdaf58c502cc0c29f5a60tree
parent798524d033f69153d4bf6604e08c69a571771ae8commit | diff
Support nested quantifier elimination for get-qe command (#5490)

Uses new nested-qe utility for eliminating nested quantification before doing quantifier elimination.

Fixes CVC4/cvc4-wishues#26

Fixes #5484.
src/smt/quant_elim_solver.cpp diff | blob | history
src/theory/quantifiers/cegqi/nested_qe.cpp diff | blob | history
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/issue5484-qe.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/issue5484b-qe.smt2 [new file with mode: 0644] blob