projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ba34ba8) | patch
Split higher-order term database (#7045)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 24 Aug 2021 20:54:31 +0000 (15:54 -0500)
committerGitHub <noreply@github.com>
Tue, 24 Aug 2021 20:54:31 +0000 (17:54 -0300)
commit9a4deadddfd3d4489ba15f65f0e3dab72b2fcccc
treec86ed005257bc1d951bfa30141b8dcde1039324ftree
parentba34ba8fc1edc62702f6b6ffcd247d13ba7f8271commit | 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.
src/CMakeLists.txt diff | blob | history
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/theory/quantifiers/ematching/ho_trigger.cpp diff | blob | history
src/theory/quantifiers/ho_term_database.cpp [new file with mode: 0644] blob
src/theory/quantifiers/ho_term_database.h [new file with mode: 0644] blob
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers/term_registry.cpp diff | blob | history