projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0dff5a6) | patch
Add oracle checker utility (#8603)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 12 Apr 2022 18:55:05 +0000 (13:55 -0500)
committerGitHub <noreply@github.com>
Tue, 12 Apr 2022 18:55:05 +0000 (18:55 +0000)
commit571195c8c297192dc3134edf339af2faeaba79ff
tree4211d6ae7e00de38547491ecc8ab0aa52bf2dd71tree
parent0dff5a6cbccb75c2ef1247243c30c0979d3d7617commit | diff
Add oracle checker utility (#8603)

This is a utility that allocates oracle callers for oracle functions on demand and can be used to convert a term containing oracle function symbols into its evaluated form.

It will be used for both SMTO (for checking consistency of oracle interfaces) and SyMO (as part of refinement lemma evaluation in CEGIS).
src/CMakeLists.txt diff | blob | history
src/theory/quantifiers/oracle_checker.cpp [new file with mode: 0644] blob
src/theory/quantifiers/oracle_checker.h [new file with mode: 0644] blob