diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-05-17 17:18:57 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-17 15:18:57 +0000 |
| commit | 63281fbfe093b1d5e375a378bb59761f77256d08 (patch) | |
| tree | ea4e7dc183ddfb23709c92f74b4d35f581ad8d32 /src/options/arith_options.toml | |
| parent | f1a65bef2675495f09603901a7166f20221b0449 (diff) | |
Improve integration of CAD with nl-Ext (#6542)
This PR improves the integration of the CAD solver with the nl-ext solver in a simple way: we simply use a few of the simple linearization lemmas in combination with CAD by default, significantly improving the performance on QF_NRA.
Diffstat (limited to 'src/options/arith_options.toml')
| -rw-r--r-- | src/options/arith_options.toml | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index c472bad3f..3005829e0 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -404,10 +404,20 @@ name = "Arithmetic theory" [[option]] name = "nlExt" category = "regular" - long = "nl-ext" - type = "bool" - default = "true" + long = "nl-ext=MODE" + type = "NlExtMode" + default = "FULL" help = "incremental linearization approach to non-linear" + help_mode = "Modes for the non-linear linearization" +[[option.mode.NONE]] + name = "none" + help = "Disable linearization approach" +[[option.mode.LIGHT]] + name = "light" + help = "Only use a few light-weight lemma schemes" +[[option.mode.FULL]] + name = "full" + help = "Use all lemma schemes" [[option]] name = "nlExtResBound" |