projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 13cf418) | patch
Make sygus more robust to unknown responses in solution verification (#5199)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 5 Oct 2020 19:30:02 +0000 (14:30 -0500)
committerGitHub <noreply@github.com>
Mon, 5 Oct 2020 19:30:02 +0000 (14:30 -0500)
commit111a197b4d9179a92b0509aded6463d47e036cc0
tree7107acd35c38640b65d539935f79c8db4be7b197tree
parent13cf41801f8f2bac538cb45d53ae7427916041a7commit | diff
Make sygus more robust to unknown responses in solution verification (#5199)

This makes it so that an "unknown" response in a CEGIS verification step causes the sygus solver to exclude the current solution and mark incomplete. Previously, the sygus solver was non-terminating in such cases, trying the same solution continously.

This also removes the option "sygusVerifySubcall", as this option should always be used. It also makes --nl-ext-tplanes enabled by default when sygus is enabled.
src/options/arith_options.toml diff | blob | history
src/options/quantifiers_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history