From 3f233b1978e10dcb553662f27ec8a4f250c89071 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 2 Sep 2021 17:42:00 -0700
Subject: [PATCH] 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).
---
 src/options/arrays_options.toml    | 2 +-
 src/options/bv_options.toml        | 2 +-
 src/options/datatypes_options.toml | 2 +-
 src/options/fp_options.toml        | 2 +-
 src/options/mkoptions.py           | 4 ++++
 src/options/smt_options.toml       | 2 +-
 6 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml
index 173a421ec..9892b3fad 100644
--- 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 576dd4103..2457645d1 100644
--- 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 24f7fdb39..60cdcc335 100644
--- 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 be40b49e2..2ed61effe 100644
--- 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 1adc2094d..51a353597 100644
--- 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 e461b803a..40a37fa7b 100644
--- 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"
-- 
2.30.2