Generate command line options for sphinx docs (#6555)

This PR adds documentation about the command line options to the sphinx documentation. It is mostly a reformatted version of what --help would print.

19 files changed, 128 insertions, 21 deletions

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 078c2ad31..997c6850a 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -74,10 +74,12 @@ add_custom_command(
     OUTPUT
       options.h options.cpp
       ${options_gen_cpp_files} ${options_gen_h_files}
+      ${CMAKE_BINARY_DIR}/docs/options_generated.rst
     COMMAND
       ${PYTHON_EXECUTABLE}
       ${CMAKE_CURRENT_LIST_DIR}/mkoptions.py
       ${CMAKE_CURRENT_LIST_DIR}
+      ${CMAKE_BINARY_DIR}
       ${CMAKE_CURRENT_BINARY_DIR}
       ${abs_toml_files}
     DEPENDS
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index a52f2144e..472657274 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -1,5 +1,5 @@
 id     = "ARITH"
-name   = "Arithmetic theory"
+name   = "Arithmetic Theory"
 
 [[option]]
   name       = "arithUnateLemmaMode"
diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml
index 6017edfd5..4cb6dda1d 100644
--- a/src/options/arrays_options.toml
+++ b/src/options/arrays_options.toml
@@ -1,5 +1,5 @@
 id     = "ARRAYS"
-name   = "Arrays theory"
+name   = "Arrays Theory"
 
 [[option]]
   name       = "arraysOptimizeLinear"
diff --git a/src/options/booleans_options.toml b/src/options/booleans_options.toml
index 52725bb8e..4aa46cfa2 100644
--- a/src/options/booleans_options.toml
+++ b/src/options/booleans_options.toml
@@ -1,3 +1,3 @@
 id     = "BOOLEANS"
-name   = "Boolean theory"
+name   = "Boolean Theory"
 
diff --git a/src/options/builtin_options.toml b/src/options/builtin_options.toml
index b5f2ed593..e4d4296fa 100644
--- a/src/options/builtin_options.toml
+++ b/src/options/builtin_options.toml
@@ -1,3 +1,3 @@
 id     = "BUILTIN"
-name   = "Builtin theory"
+name   = "Builtin Theory"
 
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 6cbf9cf37..e5b96b54a 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -1,5 +1,5 @@
 id     = "BV"
-name   = "Bitvector theory"
+name   = "Bitvector Theory"
 
 [[option]]
   name       = "bvSatSolver"
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 7c6a55095..80dedfb70 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -1,5 +1,5 @@
 id     = "DATATYPES"
-name   = "Datatypes theory"
+name   = "Datatypes Theory"
 
 # How to handle selectors applied to incorrect constructors.  If this option is set,
 # then we do not rewrite such a selector term to an arbitrary ground term.  
diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml
index b3d18aebf..b6f5a5c1b 100644
--- a/src/options/decision_options.toml
+++ b/src/options/decision_options.toml
@@ -1,5 +1,5 @@
 id     = "DECISION"
-name   = "Decision heuristics"
+name   = "Decision Heuristics"
 
 [[option]]
   name       = "decisionMode"
diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index 94a9db05b..ecd0bcf95 100644
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -1,5 +1,5 @@
 id     = "EXPR"
-name   = "Expression package"
+name   = "Expression"
 
 [[option]]
   name       = "defaultExprDepth"
diff --git a/src/options/fp_options.toml b/src/options/fp_options.toml
index d726cec3b..6fd632a7c 100644
--- a/src/options/fp_options.toml
+++ b/src/options/fp_options.toml
@@ -1,5 +1,5 @@
 id     = "FP"
-name   = "Fp"
+name   = "Floating-Point"
 
 [[option]]
   name       = "fpExp"
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 4c3524456..4cc814a61 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -298,6 +298,104 @@ class Option(object):
                 self.long_opt = r[1]
 
 
+class SphinxGenerator:
+    def __init__(self):
+        self.common = []
+        self.others = {}
+
+    def add(self, module, option):
+        if option.category == 'undocumented':
+            return
+        if not option.long and not option.short:
+            return
+        names = []
+        if option.long:
+            if option.long_opt:
+                names.append('--{}={}'.format(option.long_name, option.long_opt))
+            else:
+                names.append('--{}'.format(option.long_name))
+        
+        if option.alias:
+            if option.long_opt:
+                names.extend(['--{}={}'.format(a, option.long_opt) for a in option.alias])
+            else:
+                names.extend(['--{}'.format(a) for a in option.alias])
+
+        if option.short:
+            if option.long_opt:
+                names.append('-{} {}'.format(option.short, option.long_opt))
+            else:
+                names.append('-{}'.format(option.short))
+        
+        modes = None
+        if option.mode:
+            modes = {}
+            for _, data in option.mode.items():
+                assert len(data) == 1
+                data = data[0]
+                modes[data['name']] = data.get('help', '')
+
+        data = {
+            'name': names,
+            'help': option.help,
+            'expert': option.category == 'expert',
+            'alternate': option.type == 'bool' and option.alternate,
+            'help_mode': option.help_mode,
+            'modes': modes,
+        }
+
+        if option.category == 'common':
+            self.common.append(data)
+        else:
+            if module.name not in self.others:
+                self.others[module.name] = []
+            self.others[module.name].append(data)
+    
+    def __render_option(self, res, opt):
+        desc = '``{}``'
+        val = '    {}'
+        if opt['expert']:
+            res.append('.. admonition:: This option is intended for Experts only!')
+            res.append('    ')
+            desc = '    ' + desc
+            val = '    ' + val
+
+        if opt['alternate']:
+            desc += ' (also ``--no-*``)'
+        res.append(desc.format(' | '.join(opt['name'])))
+        res.append(val.format(opt['help']))
+
+        if opt['modes']:
+            print(opt['modes'])
+            res.append(val.format(''))
+            res.append(val.format(opt['help_mode']))
+            res.append(val.format(''))
+            for k, v in opt['modes'].items():
+                res.append(val.format(':{}: {}'.format(k, v)))
+        res.append('    ')
+
+
+    def render(self, dstdir, filename):
+        res = []
+
+        res.append('Most Commonly-Used cvc5 Options')
+        res.append('===============================')
+        for opt in self.common:
+            self.__render_option(res, opt)
+
+        res.append('')
+        res.append('Additional cvc5 Options')
+        res.append('=======================')
+        for module in self.others:
+            res.append('')
+            res.append('{} Module'.format(module))
+            res.append('-' * (len(module) + 8))
+            for opt in self.others[module]:
+                self.__render_option(res, opt)
+
+        write_file(dstdir, filename, '\n'.join(res))
+
+
 def die(msg):
     sys.exit('[error] {}'.format(msg))
 
@@ -626,7 +724,7 @@ def add_getopt_long(long_name, argument_req, getopt_long):
             'required' if argument_req else 'no', value))
 
 
-def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp):
+def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp):
     """
     Generate code for all option modules (options.cpp, options_holder.h).
     """
@@ -645,6 +743,8 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp):
     setoption_handlers = []  # handlers for set-option command
     getoption_handlers = []  # handlers for get-option command
 
+    sphinxgen = SphinxGenerator()
+
     for module in modules:
         headers_module.append(format_include(module.header))
 
@@ -660,6 +760,8 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp):
 
             docgen_option(option, help_common, help_others)
 
+            sphinxgen.add(module, option)
+
             # Generate handler call
             handler = None
             if option.handler:
@@ -885,6 +987,8 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp):
         getoption_handlers='\n'.join(getoption_handlers)
     ))
 
+    if os.path.isdir('{}/docs/'.format(build_dir)):
+        sphinxgen.render('{}/docs/'.format(build_dir), 'options_generated.rst')
 
 def lstrip(prefix, s):
     """
@@ -1010,8 +1114,9 @@ def mkoptions_main():
         die('missing arguments')
 
     src_dir = sys.argv[1]
-    dst_dir = sys.argv[2]
-    filenames = sys.argv[3:]
+    build_dir = sys.argv[2]
+    dst_dir = sys.argv[3]
+    filenames = sys.argv[4:]
 
     # Check if given directories exist.
     for d in [src_dir, dst_dir]:
@@ -1052,7 +1157,7 @@ def mkoptions_main():
         codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp)
 
     # Create options.cpp and options_holder.h in destination directory
-    codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp)
+    codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp)
 
 
 
diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml
index 69dad8d63..26d7a451b 100644
--- a/src/options/prop_options.toml
+++ b/src/options/prop_options.toml
@@ -1,5 +1,5 @@
 id     = "PROP"
-name   = "SAT layer"
+name   = "SAT Layer"
 
 [[option]]
   name       = "satRandomFreq"
diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml
index 88bacce1b..6d5c4d4cf 100644
--- a/src/options/resource_manager_options.toml
+++ b/src/options/resource_manager_options.toml
@@ -1,5 +1,5 @@
 id     = "RESMAN"
-name   = "Resource Manager options"
+name   = "Resource Manager"
 
 [[option]]
   name       = "cumulativeMillisecondLimit"
diff --git a/src/options/sep_options.toml b/src/options/sep_options.toml
index f45e78c98..7185a35df 100644
--- a/src/options/sep_options.toml
+++ b/src/options/sep_options.toml
@@ -1,5 +1,5 @@
 id     = "SEP"
-name   = "Sep"
+name   = "Separation Logic Theory"
 
 [[option]]
   name       = "sepCheckNeg"
diff --git a/src/options/sets_options.toml b/src/options/sets_options.toml
index db9cfa480..dee134ae4 100644
--- a/src/options/sets_options.toml
+++ b/src/options/sets_options.toml
@@ -1,5 +1,5 @@
 id     = "SETS"
-name   = "Sets"
+name   = "Sets Theory"
 
 [[option]]
   name       = "setsProxyLemmas"
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 22d05f6f7..733c2239c 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -1,5 +1,5 @@
 id     = "SMT"
-name   = "SMT layer"
+name   = "SMT Layer"
 
 [[option]]
   name       = "dumpModeString"
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 44c9c191f..958136494 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -1,5 +1,5 @@
 id     = "STRINGS"
-name   = "Strings theory"
+name   = "Strings Theory"
 
 [[option]]
   name       = "stringExp"
diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml
index ec11d17ec..f47907683 100644
--- a/src/options/theory_options.toml
+++ b/src/options/theory_options.toml
@@ -1,5 +1,5 @@
 id     = "THEORY"
-name   = "Theory layer"
+name   = "Theory Layer"
 
 [[option]]
   name       = "theoryOfMode"
diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index 81b119964..058d8be27 100644
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -1,5 +1,5 @@
 id     = "UF"
-name   = "Uninterpreted functions theory"
+name   = "Uninterpreted Functions Theory"
 
 [[option]]
   name       = "ufSymmetryBreaker"