diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 12:27:40 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-19 12:27:40 -0600 |
| commit | f172b30bfe18a24416fd61f4aa5ce3dea583296e (patch) | |
| tree | 3c27f17b24e6095ce7ad4b5ec3f50e407412d378 /src/expr/CMakeLists.txt | |
| parent | 3654512dd8b341c5725e550d438b23508493b991 (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.
Diffstat (limited to 'src/expr/CMakeLists.txt')
| -rw-r--r-- | src/expr/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index fb3df5327..430303f6b 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -112,6 +112,8 @@ libcvc4_add_sources( record.h sequence.cpp sequence.h + subs.cpp + subs.h sygus_datatype.cpp sygus_datatype.h uninterpreted_constant.cpp |