projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 354441c) | patch
Implement internal support for synthesis modulo oracles (#8617)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 14 Apr 2022 19:48:23 +0000 (14:48 -0500)
committerGitHub <noreply@github.com>
Thu, 14 Apr 2022 19:48:23 +0000 (19:48 +0000)
commit85fff4428ceaddd25f5c7caf14abc0544d86a59c
tree8ce1128d8d4261db3de2aa80742f5fc0e74c67e7tree
parent354441c5b1c3d0f4d19d1f92e45df08e1d615b2ccommit | diff
Implement internal support for synthesis modulo oracles (#8617)

SyMO is implemented as a preprocessor for SMT queries in the verification subsolver of SyGuS.
src/theory/quantifiers/sygus/synth_verify.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_verify.h diff | blob | history