options: Add -H/--help-regular option to list regular options.

mpreiner · Aug 8, 2023 · 9d189c5 · 9d189c5
1 parent e2dae2a
commit 9d189c5
Show file tree

Hide file tree

Showing 5 changed files with 41 additions and 7 deletions.
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
@@ -76,6 +76,11 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<cvc5::Solver>& solver)
     printUsage(progName, dopts.out());
     exit(1);
   }
+  else if (solver->getOptionInfo("help-regular").boolValue())
+  {
+    printUsage(progName, dopts.out(), true);
+    exit(1);
+  }
   for (const auto& name : {"show-config",
                            "copyright",
                            "show-trace-tags",

diff --git a/src/main/options.h b/src/main/options.h
@@ -28,7 +28,9 @@ namespace cvc5::main {
  * Print overall command-line option usage message to the given output stream
  * with binary being the command to run cvc5.
  */
-void printUsage(const std::string& binary, std::ostream& os);
+void printUsage(const std::string& binary,
+                std::ostream& os,
+                bool printRegular = false);
 
 /**
  * Initialize the Options object options based on the given

diff --git a/src/main/options_template.cpp b/src/main/options_template.cpp
@@ -59,13 +59,18 @@ R"FOOBAR(Additional cvc5 options:
 ${help_others}$
 )FOOBAR";
 
+static const std::string regularOptionsDescription =
+R"FOOBAR(Regular cvc5 options:
+${help_regular}$
+)FOOBAR";
+
 static const std::string optionsFootnote = "\n\
 [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\
     sense of the option.\n\
 ";
 // clang-format on
 
-void printUsage(const std::string& binary, std::ostream& os)
+void printUsage(const std::string& binary, std::ostream& os, bool printRegular)
 {
   os << "usage: " << binary << " [options] [input-file]" << std::endl
      << std::endl
@@ -75,9 +80,17 @@ void printUsage(const std::string& binary, std::ostream& os)
      << std::endl
      << "cvc5 options:" << std::endl
      << commonOptionsDescription << std::endl
-     << std::endl
-     << additionalOptionsDescription << std::endl
-     << optionsFootnote << std::endl;
+     << std::endl;
+
+  if (printRegular)
+  {
+    os << regularOptionsDescription << std::endl;
+  }
+  else
+  {
+    os << additionalOptionsDescription << std::endl;
+  }
+  os << optionsFootnote << std::endl;
 }
 
 /**

diff --git a/src/options/main_options.toml b/src/options/main_options.toml
@@ -22,6 +22,16 @@ name   = "Driver"
   alternate  = false
   help       = "full command line reference"
 
+[[option]]
+  name       = "helpRegular"
+  category   = "common"
+  long       = "help-regular"
+  short      = "H"
+  type       = "bool"
+  default    = "false"
+  alternate  = false
+  help       = "regular command line reference"
+
 [[option]]
   name       = "showConfiguration"
   category   = "common"

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
@@ -716,6 +716,7 @@ def _cli_help_wrap(help_msg, opts):
 def generate_cli_help(modules):
     """Generate the output for --help."""
     common = []
+    regular = []
     others = []
     for module in modules:
         if not module.options:
@@ -738,7 +739,9 @@ def generate_cli_help(modules):
                     common.extend(res)
                 else:
                     others.extend(res)
-    return '\n'.join(common), '\n'.join(others)
+                    if option.category == 'regular':
+                        regular.extend(res)
+    return '\n'.join(common), '\n'.join(others), '\n'.join(regular)
 
 
 ################################################################################
@@ -961,7 +964,7 @@ def codegen_module(module, dst_dir, tpls):
 def codegen_all_modules(modules, src_dir, build_dir, dst_dir, tpls):
     """Generate code for all option modules."""
     short, cmdline_opts, parseinternal = generate_parsing(modules)
-    help_common, help_others = generate_cli_help(modules)
+    help_common, help_others, help_regular = generate_cli_help(modules)
 
     if os.path.isdir('{}/docs/'.format(build_dir)):
         write_file('{}/docs/'.format(build_dir), 'options_generated.rst',
@@ -997,6 +1000,7 @@ def codegen_all_modules(modules, src_dir, build_dir, dst_dir, tpls):
         # main/options.cpp
         'help_common': help_common,
         'help_others': help_others,
+        'help_regular': help_regular,
         'cmdoptions_long': cmdline_opts,
         'cmdoptions_short': short,
         'parseinternal_impl': parseinternal,