diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-24 15:54:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-24 17:54:31 -0300 |
| commit | 9a4deadddfd3d4489ba15f65f0e3dab72b2fcccc (patch) | |
| tree | c86ed005257bc1d951bfa30141b8dcde1039324f /src/CMakeLists.txt | |
| parent | ba34ba8fc1edc62702f6b6ffcd247d13ba7f8271 (diff) | |
Split higher-order term database (#7045)
This splits higher-order term database as a derived class of term database, thus separating higher-order specific things out of our core term database.
This eliminates many of the references to the deprecated option uf-ho.
This is work towards eliminating that option.
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 f5af58aeb..306420a2c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -803,6 +803,8 @@ libcvc5_add_sources( theory/quantifiers/fmf/model_engine.h theory/quantifiers/fun_def_evaluator.cpp theory/quantifiers/fun_def_evaluator.h + theory/quantifiers/ho_term_database.cpp + theory/quantifiers/ho_term_database.h theory/quantifiers/index_trie.cpp theory/quantifiers/index_trie.h theory/quantifiers/inst_match.cpp |