diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index a91d4e29b2b..1eeba60e2b4 100644 --- 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& 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 index 76dae03940d..2dbaa0e9546 100644 --- 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 index f6dcfb09f4b..f1ed6b9b91d 100644 --- 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 index e1a0c68df34..b5ac62848f1 100644 --- 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 index 81934e13fa4..128968b115e 100644 --- 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,