projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 11752f5) | patch
Implement internal support for (definitional) satisfiability modulo oracles (#8618)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 14 Apr 2022 22:53:28 +0000 (17:53 -0500)
committerGitHub <noreply@github.com>
Thu, 14 Apr 2022 22:53:28 +0000 (17:53 -0500)
commit2c8f7a72fbd01c06e717a02a34d610e39cc20042
tree181a0f5c0dd108590e8b2c55a46fcad649921b45tree
parent11752f52825ff7f077a25bcb6350bbc9d9c1ba55commit | diff
Implement internal support for (definitional) satisfiability modulo oracles (#8618)

Adds implementation of OracleEngine, which adds lemmas of the form (= (f c) d) on demand for I/O pairs (c,d) from oracle calls.
src/expr/oracle_caller.cpp diff | blob | history
src/expr/oracle_caller.h diff | blob | history
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
src/theory/quantifiers/oracle_engine.cpp diff | blob | history
src/theory/quantifiers/oracle_engine.h diff | blob | history