projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3ebc297) | patch
Rename sygus option name (#3977)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 10 Mar 2020 03:18:58 +0000 (22:18 -0500)
committerGitHub <noreply@github.com>
Tue, 10 Mar 2020 03:18:58 +0000 (20:18 -0700)
commit0e09af0be57ec4df28869e4383a40d847c0a6b5a
tree659be92f761f174f6690bd16d1d2e6b0f2301999tree
parent3ebc297e6ff589f7b98519cd2aa23963a4e06652commit | diff
Rename sygus option name (#3977)

This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach).

It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason.
src/options/options.h diff | blob | history
src/options/options_public_functions.cpp diff | blob | history
src/options/quantifiers_options.toml diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
test/regress/regress1/sygus/hd-01-d1-prog.sy diff | blob | history