projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f7dcb48) | patch
Add pool instantiation strategy (#6308)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 13 Apr 2021 21:33:07 +0000 (16:33 -0500)
committerGitHub <noreply@github.com>
Tue, 13 Apr 2021 21:33:07 +0000 (21:33 +0000)
commit1c0d2738941e948d67c696e0c96e3463da9807d2
tree31e929bc26f3b01518b339ed0c9bef562bc6983ctree
parentf7dcb4875bba33b7712732a874581639681926f8commit | diff
Add pool instantiation strategy (#6308)

Adds an instantiation strategy based on user-provided pool annotations.

The next PR will connect this to quantifiers engine.
src/CMakeLists.txt diff | blob | history
src/options/quantifiers_options.toml diff | blob | history
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
src/theory/quantifiers/inst_strategy_pool.cpp [new file with mode: 0644] blob
src/theory/quantifiers/inst_strategy_pool.h [new file with mode: 0644] blob
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/quantifiers_modules.cpp diff | blob | history
src/theory/quantifiers/quantifiers_modules.h diff | blob | history
src/theory/quantifiers/term_tuple_enumerator.cpp diff | blob | history
src/theory/quantifiers/term_tuple_enumerator.h diff | blob | history