projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3654512) | patch
Add nested quantifier elimination module (#5422)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 19 Nov 2020 18:27:40 +0000 (12:27 -0600)
committerGitHub <noreply@github.com>
Thu, 19 Nov 2020 18:27:40 +0000 (12:27 -0600)
commitf172b30bfe18a24416fd61f4aa5ce3dea583296e
tree3c27f17b24e6095ce7ad4b5ec3f50e407412d378tree
parent3654512dd8b341c5725e550d438b23508493b991commit | diff
Add nested quantifier elimination module (#5422)

This has static utilities for doing nested quantifier elimination and some data structures for maintaining a context-dependent set of quantified formulas that have been processed.

This is work towards CVC4/cvc4-wishues#26, and work reimplementation of the option --ceqgi-nested-qe.
src/CMakeLists.txt diff | blob | history
src/expr/CMakeLists.txt diff | blob | history
src/theory/quantifiers/cegqi/nested_qe.cpp [new file with mode: 0644] blob
src/theory/quantifiers/cegqi/nested_qe.h [new file with mode: 0644] blob