Remove "experimental" options (#7124)

This PR changes all options from experimental to expert and adds a check that only the well-defined option categories are used (common, regular, expert, undocumented).

diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml
index 173a421ec6fb4c3fb2a5869fd78fa72aa534ce5f..9892b3fadbf081456a081fc531e8f84e6d78e295 100644 (file)
--- a/src/options/arrays_options.toml
+++ b/src/options/arrays_options.toml
@@ -67,7 +67,7 @@ name   = "Arrays Theory"
 
 [[option]]
   name       = "arraysExp"
-  category   = "experimental"
+  category   = "expert"
   long       = "arrays-exp"
   type       = "bool"
   default    = "false"

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 576dd41034f84b1a146157c16cbac684a759ab17..2457645d1af9e5e93e3da066df5be8cf7353043d 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -78,7 +78,7 @@ name   = "Bitvector Theory"
 
 [[option]]
   name       = "bitvectorAlgebraicSolver"
-  category   = "experimental"
+  category   = "expert"
   long       = "bv-algebraic-solver"
   type       = "bool"
   default    = "false"

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 24f7fdb3995601bcae157e393211032d3b70c152..60cdcc3358d81670f885793953470e4507c5edf5 100644 (file)
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -23,7 +23,7 @@ name   = "Datatypes Theory"
 
 [[option]]
   name       = "dtPoliteOptimize"
-  category   = "experimental"
+  category   = "expert"
   long       = "dt-polite-optimize"
   type       = "bool"
   default    = "true"

diff --git a/src/options/fp_options.toml b/src/options/fp_options.toml
index be40b49e20264a1e6dcc85673e0618397d0f3038..2ed61effe7b6ec42f731f92f6b1eda1f2cbdcb7f 100644 (file)
--- a/src/options/fp_options.toml
+++ b/src/options/fp_options.toml
@@ -11,7 +11,7 @@ name   = "Floating-Point"
 
 [[option]]
   name       = "fpLazyWb"
-  category   = "experimental"
+  category   = "expert"
   long       = "fp-lazy-wb"
   type       = "bool"
   default    = "false"

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 1adc2094d4f9b997d00a42bb2f3d079048ed71bf..51a3535975e29ec3364c597c0e3fd8093288f102 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -990,6 +990,10 @@ def parse_module(filename, module):
                 perr(filename,
                      'defining handlers for bool options is not allowed',
                      option)
+            if option.category not in CATEGORY_VALUES:
+                perr(filename,
+                     "has invalid category '{}'".format(option.category),
+                     option)
             if option.category != 'undocumented' and not option.help:
                 perr(filename,
                      'help text required for {} options'.format(option.category),

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index e461b803a9629670b1cc547e72b7b566651ed1ab..40a37fa7b80d004e2c2629fd050216350843df22 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -301,7 +301,7 @@ name   = "SMT Layer"
 
 [[option]]
   name       = "earlyIteRemoval"
-  category   = "experimental"
+  category   = "expert"
   long       = "early-ite-removal"
   type       = "bool"
   default    = "false"