projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6e5505c) | patch
Refactor oracles using new std::function backend (#8717)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 4 May 2022 15:03:16 +0000 (10:03 -0500)
committerGitHub <noreply@github.com>
Wed, 4 May 2022 15:03:16 +0000 (15:03 +0000)
commit67d02be826a12349eaf8420ab93495b8cfe5deca
tree2027d2522f28bb85e112b8bf969cd2ca0564e12btree
parent6e5505c92c9586f5e388fd5002e9c7d5f0b666e2commit | diff
Refactor oracles using new std::function backend (#8717)

This also updates several places to be generalized to methods that return a vector of Nodes. Previously we had assumed a use case returning a single node.

After this PR, #8622 will be updated to use the new std::function interface.
src/expr/oracle_caller.cpp diff | blob | history
src/expr/oracle_caller.h diff | blob | history
src/theory/quantifiers/oracle_checker.cpp diff | blob | history
src/theory/quantifiers/oracle_checker.h diff | blob | history
src/theory/quantifiers/oracle_engine.cpp diff | blob | history
src/theory/quantifiers/oracle_engine.h diff | blob | history
src/theory/quantifiers/quantifiers_attributes.cpp diff | blob | history
src/theory/quantifiers/quantifiers_attributes.h diff | blob | history
src/theory/quantifiers/sygus/synth_verify.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history