projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9ab7a86) | patch
Integrate oracle checker into quantifiers term registry (#8604)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 14 Apr 2022 13:36:38 +0000 (08:36 -0500)
committerGitHub <noreply@github.com>
Thu, 14 Apr 2022 13:36:38 +0000 (13:36 +0000)
commitefda428a779a73e69fa853967447c82f9876d9c8
tree330557c0753f81635794d62397fccd5b99783091tree
parent9ab7a86c46ebeab243a768a6240c2ecfb0b7464dcommit | diff
Integrate oracle checker into quantifiers term registry (#8604)

Also incorporates into sygus term database. For SyMO, oracle function symbols act analogously to recursive function definitions; the oracle checker is used to rewrite terms in the same contexts as when recursive function definitions are evaluated.
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.h diff | blob | history
src/theory/quantifiers/term_registry.cpp diff | blob | history
src/theory/quantifiers/term_registry.h diff | blob | history