From 2a96d7de381aa565a6eacf724848c0e7839c7cf6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 23 Jul 2019 08:54:13 -0500 Subject: [PATCH] Fix help messages (#3096) --- src/options/options_handler.cpp | 17 ++++++++++------- 1 file 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\ -- 2.30.2