projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 60ad84f) | patch
Add oracle engine to quantifiers engine (#8589)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 11 Apr 2022 21:06:10 +0000 (16:06 -0500)
committerGitHub <noreply@github.com>
Mon, 11 Apr 2022 21:06:10 +0000 (16:06 -0500)
commit8de233dec2e33951e0fcc294af6c835bfc7cb701
tree71a806cc9a1dd3101e62954f51c8df2d5f2c1d4dtree
parent60ad84f41f846c669956205163b0ac4f3641939acommit | diff
Add oracle engine to quantifiers engine (#8589)

This class is the subsolver of quantifiers engine for handling oracles in SMTO. The implementation of this class will be added in followup PRs.

It also contains a utility method for constructing oracle interfaces.
src/CMakeLists.txt diff | blob | history
src/options/quantifiers_options.toml diff | blob | history
src/theory/quantifiers/oracle_engine.cpp [new file with mode: 0644] blob
src/theory/quantifiers/oracle_engine.h [new file with mode: 0644] blob
src/theory/quantifiers/quantifiers_modules.cpp diff | blob | history
src/theory/quantifiers/quantifiers_modules.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history