From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 23 Jul 2019 13:54:13 +0000 (-0500)
Subject: Fix help messages (#3096)
X-Git-Tag: cvc5-1.0.0~4082
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2a96d7de381aa565a6eacf724848c0e7839c7cf6;p=cvc5.git

Fix help messages (#3096)
---

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\