diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-23 08:54:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-23 08:54:13 -0500 |
| commit | 2a96d7de381aa565a6eacf724848c0e7839c7cf6 (patch) | |
| tree | fd5ff8da60c7a8d3ff0b43d1d18940b70500dc35 /src/options | |
| parent | 5b494f33f146677386385fc7d055f95d9aae08d5 (diff) | |
Fix help messages (#3096)
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/options_handler.cpp | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index b145da639..b7684c556 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -219,7 +219,7 @@ ErrorSelectionRule OptionsHandler::stringToErrorSelectionRule( // theory/quantifiers/options_handlers.h const std::string OptionsHandler::s_instWhenHelp = "\ -Modes currently supported by the --inst-when option:\n\ +Instantiation modes currently supported by the --inst-when option:\n\ \n\ full-last-call (default)\n\ + Alternate running instantiation rounds at full effort and last\n\ @@ -349,7 +349,8 @@ min-s-all \n\ \n\ "; const std::string OptionsHandler::s_triggerActiveSelModeHelp = "\ -Trigger active selection modes currently supported by the --trigger-sel option:\n\ +Trigger active selection modes currently supported by the \ +--trigger-active-sel option:\n\ \n\ all \n\ + Make all triggers active. \n\ @@ -399,7 +400,8 @@ none \n\ "; const std::string OptionsHandler::s_termDbModeHelp = "\ -Modes for term database, supported by --term-db-mode:\n\ +Modes for terms included in the quantifiers term database, supported by\ +--term-db-mode:\n\ \n\ all \n\ + Quantifiers module considers all ground terms.\n\ @@ -425,7 +427,8 @@ all \n\ const std::string OptionsHandler::s_cbqiBvIneqModeHelp = "\ -Modes for single invocation techniques, supported by --cbqi-bv-ineq:\n\ +Modes for handling bit-vector inequalities in counterexample-guided\ +instantiation, supported by --cbqi-bv-ineq:\n\ \n\ eq-slack (default) \n\ + Solve for the inequality using the slack value in the model, e.g.,\ @@ -1587,7 +1590,7 @@ table\n\ "; const std::string OptionsHandler::s_instFormatHelp = "\ -Inst format modes currently supported by the --model-format option:\n\ +Inst format modes currently supported by the --inst-format option:\n\ \n\ default \n\ + Print instantiations as a list in the output language format.\n\ @@ -1711,7 +1714,7 @@ SimplificationMode OptionsHandler::stringToSimplificationMode( const std::string OptionsHandler::s_modelCoresHelp = "\ -Model cores modes currently supported by the --simplification option:\n\ +Model cores modes currently supported by the --model-cores option:\n\ \n\ none (default) \n\ + do not compute model cores\n\ @@ -1756,7 +1759,7 @@ ModelCoresMode OptionsHandler::stringToModelCoresMode(std::string option, const std::string OptionsHandler::s_sygusSolutionOutModeHelp = "\ -Modes for finite model finding bound minimization, supported by --sygus-out:\n\ +Modes for sygus solution output, supported by --sygus-out:\n\ \n\ status \n\ + Print only status for check-synth calls.\n\ |