diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-09 22:18:58 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-09 20:18:58 -0700 |
| commit | 0e09af0be57ec4df28869e4383a40d847c0a6b5a (patch) | |
| tree | 659be92f761f174f6690bd16d1d2e6b0f2301999 /src/options/quantifiers_options.toml | |
| parent | 3ebc297e6ff589f7b98519cd2aa23963a4e06652 (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.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 1101f70c5..926eacaae 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1032,12 +1032,12 @@ header = "options/quantifiers_options.h" help = "attempt to preprocess arbitrary inputs to sygus conjectures" [[option]] - name = "ceGuidedInst" + name = "sygus" category = "regular" - long = "cegqi" + long = "sygus" type = "bool" default = "false" - help = "counterexample-guided quantifier instantiation for sygus" + help = "use sygus solver (default is true for sygus inputs)" [[option]] name = "cegqiSingleInvMode" |