diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-20 16:40:12 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-20 21:40:12 +0000 |
| commit | cc8ce1bcdf8d6a4b508723063879e891a6cbd8c3 (patch) | |
| tree | fef63c0628404e673eca56947d19411198ba3ce2 /src/CMakeLists.txt | |
| parent | 18ce14653647a93319cc53eec9bc310d3a4c6f57 (diff) | |
Add instantiation pool feature to the API (#6358)
This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b86435eb7..c24ab31ec 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -869,6 +869,8 @@ libcvc4_add_sources( theory/quantifiers/term_database.h theory/quantifiers/term_enumeration.cpp theory/quantifiers/term_enumeration.h + theory/quantifiers/term_pools.cpp + theory/quantifiers/term_pools.h theory/quantifiers/term_registry.cpp theory/quantifiers/term_registry.h theory/quantifiers/term_util.cpp |