projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: aaf0877) | patch
Enable CDCAC solver for selected quantified logics (#7571)
authorGereon Kremer <nafur42@gmail.com>
Thu, 4 Nov 2021 17:59:14 +0000 (10:59 -0700)
committerGitHub <noreply@github.com>
Thu, 4 Nov 2021 17:59:14 +0000 (17:59 +0000)
commit622865024f83cefee01f56271ba2dfae4984d0d0
tree22cb7434de40d4251b369fe4ea7ae015971f3392tree
parentaaf0877baf437395f915b8a12457a72b77fc39cecommit | diff
Enable CDCAC solver for selected quantified logics (#7571)

This PR enables the CDCAC solver for quantified logics with reals, but no integers. Also, it disables SyGuS if no integers are used. The regression is a benchmark that is only solved with this new configuration.
src/smt/set_defaults.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/nl/nra-cad-performance.smt2 [new file with mode: 0644] blob