summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/main/driver_unified.cpp37
-rw-r--r--src/main/options.h15
-rw-r--r--src/main/options_template.cpp22
-rw-r--r--src/options/main_options.toml30
-rw-r--r--src/options/options_handler.cpp44
-rw-r--r--src/options/options_handler.h10
-rw-r--r--test/regress/CMakeLists.txt2
-rw-r--r--test/regress/regress0/options/didyoumean.smt24
-rw-r--r--test/regress/regress0/options/help.smt24
-rw-r--r--test/unit/CMakeLists.txt3
-rw-r--r--test/unit/options/CMakeLists.txt17
-rw-r--r--test/unit/options/options_black.cpp168
12 files changed, 270 insertions, 86 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 7b34ab6d3..e576f2e71 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -59,26 +59,6 @@ std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
} // namespace main
} // namespace cvc5
- void printUsage(const api::DriverOptions& dopts, bool full)
- {
- std::stringstream ss;
- ss << "usage: " << progName << " [options] [input-file]" << std::endl
- << std::endl
- << "Without an input file, or with `-', cvc5 reads from standard "
- "input."
- << std::endl
- << std::endl
- << "cvc5 options:" << std::endl;
- if (full)
- {
- main::printUsage(ss.str(), dopts.out());
- }
- else
- {
- main::printShortUsage(ss.str(), dopts.out());
- }
- }
-
int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
{
// Initialize the signal handlers
@@ -92,15 +72,24 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
// Parse the options
std::vector<string> filenames = main::parse(*solver, argc, argv, progName);
-
- auto limit = install_time_limit(solver->getOptionInfo("tlimit").uintValue());
-
if (solver->getOptionInfo("help").boolValue())
{
- printUsage(dopts, true);
+ main::printUsage(progName, dopts.out());
exit(1);
}
+ for (const auto& name : {"show-config",
+ "copyright",
+ "show-debug-tags",
+ "show-trace-tags",
+ "version"})
+ {
+ if (solver->getOptionInfo(name).boolValue())
+ {
+ std::exit(0);
+ }
+ }
+ auto limit = install_time_limit(solver->getOptionInfo("tlimit").uintValue());
segvSpin = solver->getOptionInfo("segv-spin").boolValue();
// If in competition mode, set output stream option to flush immediately
diff --git a/src/main/options.h b/src/main/options.h
index 832abcf9d..d3af4994d 100644
--- a/src/main/options.h
+++ b/src/main/options.h
@@ -25,19 +25,10 @@
namespace cvc5::main {
/**
- * Print overall command-line option usage message, prefixed by
- * "msg"---which could be an error message causing the usage
- * output in the first place, e.g. "no such option --foo"
+ * 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& msg, std::ostream& os);
-
-/**
- * Print command-line option usage message for only the most-commonly
- * used options. The message is prefixed by "msg"---which could be
- * an error message causing the usage output in the first place, e.g.
- * "no such option --foo"
- */
-void printShortUsage(const std::string& msg, std::ostream& os);
+void printUsage(const std::string& binary, std::ostream& os);
/**
* Initialize the Options object options based on the given
diff --git a/src/main/options_template.cpp b/src/main/options_template.cpp
index e0429c5f9..3d0e1ccf9 100644
--- a/src/main/options_template.cpp
+++ b/src/main/options_template.cpp
@@ -63,23 +63,21 @@ static const std::string optionsFootnote = "\n\
";
// clang-format on
-void printUsage(const std::string& msg, std::ostream& os)
+void printUsage(const std::string& binary, std::ostream& os)
{
- os << msg << "\n"
- << commonOptionsDescription << "\n\n"
+ os << "usage: " << binary << " [options] [input-file]" << std::endl
+ << std::endl
+ << "Without an input file, or with `-', cvc5 reads from standard "
+ "input."
+ << std::endl
+ << std::endl
+ << "cvc5 options:" << std::endl
+ << commonOptionsDescription << std::endl
+ << std::endl
<< additionalOptionsDescription << std::endl
<< optionsFootnote << std::endl;
}
-void printShortUsage(const std::string& msg, std::ostream& os)
-{
- os << msg << "\n"
- << commonOptionsDescription << std::endl
- << optionsFootnote << std::endl
- << "For full usage, please use --help." << std::endl
- << std::endl;
-}
-
/**
* This is a table of long options. By policy, each short option
* should have an equivalent long option (but the reverse isn't the
diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index 0e3f63072..10c58016d 100644
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -2,11 +2,13 @@ id = "DRIVER"
name = "Driver"
[[option]]
+ name = "showVersion"
category = "common"
short = "V"
long = "version"
- type = "void"
- handler = "showVersion"
+ type = "bool"
+ predicates = ["showVersion"]
+ alternate = false
help = "identify this cvc5 binary"
[[option]]
@@ -19,17 +21,21 @@ name = "Driver"
help = "full command line reference"
[[option]]
+ name = "showConfiguration"
category = "common"
long = "show-config"
- type = "void"
- handler = "showConfiguration"
+ type = "bool"
+ predicates = ["showConfiguration"]
+ alternate = false
help = "show cvc5 static configuration"
[[option]]
+ name = "showCopyright"
category = "common"
long = "copyright"
- type = "void"
- handler = "showCopyright"
+ type = "bool"
+ predicates = ["showCopyright"]
+ alternate = false
help = "show cvc5 copyright information"
[[option]]
@@ -42,17 +48,21 @@ name = "Driver"
help = "seed for random number generator"
[[option]]
+ name = "showDebugTags"
category = "regular"
long = "show-debug-tags"
- type = "void"
- handler = "showDebugTags"
+ type = "bool"
+ predicates = ["showDebugTags"]
+ alternate = false
help = "show all available tags for debugging"
[[option]]
+ name = "showTraceTags"
category = "regular"
long = "show-trace-tags"
- type = "void"
- handler = "showTraceTags"
+ type = "bool"
+ predicates = ["showTraceTags"]
+ alternate = false
help = "show all available tags for tracing"
[[option]]
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 68d1f2b64..7af82df42 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -33,6 +33,7 @@
#include "options/decision_options.h"
#include "options/io_utils.h"
#include "options/language.h"
+#include "options/main_options.h"
#include "options/option_exception.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
@@ -45,9 +46,9 @@ namespace options {
// helper functions
namespace {
-static void printTags(const std::vector<std::string>& tags)
+void printTags(const std::vector<std::string>& tags)
{
- std::cout << "available tags:";
+ std::cout << "available tags:" << std::endl;
for (const auto& t : tags)
{
std::cout << " " << t << std::endl;
@@ -96,8 +97,7 @@ Languages currently supported as arguments to the --output-lang option:
tptp TPTP format
ast internal format (simple syntax trees)
)FOOBAR" << std::endl;
- std::exit(1);
- return Language::LANG_AUTO;
+ throw OptionException("help is not a valid language");
}
try
@@ -199,12 +199,13 @@ void OptionsHandler::enableTraceTag(const std::string& flag,
{
throw OptionException("trace tags not available in non-tracing builds");
}
- else if(!Configuration::isTraceTag(optarg.c_str()))
+ else if (!Configuration::isTraceTag(optarg))
{
if (optarg == "help")
{
- printTags(Configuration::getTraceTags());
- std::exit(0);
+ d_options->driver.showTraceTags = true;
+ showTraceTags("", true);
+ return;
}
throw OptionException(
@@ -226,13 +227,13 @@ void OptionsHandler::enableDebugTag(const std::string& flag,
throw OptionException("debug tags not available in non-tracing builds");
}
- if (!Configuration::isDebugTag(optarg.c_str())
- && !Configuration::isTraceTag(optarg.c_str()))
+ if (!Configuration::isDebugTag(optarg) && !Configuration::isTraceTag(optarg))
{
if (optarg == "help")
{
- printTags(Configuration::getDebugTags());
- std::exit(0);
+ d_options->driver.showDebugTags = true;
+ showDebugTags("", true);
+ return;
}
throw OptionException(std::string("debug tag ") + optarg
@@ -364,8 +365,9 @@ static void print_config_cond(const char* str, bool cond = false)
print_config(str, cond ? "yes" : "no");
}
-void OptionsHandler::showConfiguration(const std::string& flag)
+void OptionsHandler::showConfiguration(const std::string& flag, bool value)
{
+ if (!value) return;
std::cout << Configuration::about() << std::endl;
print_config("version", Configuration::getVersionString());
@@ -407,24 +409,23 @@ void OptionsHandler::showConfiguration(const std::string& flag)
print_config_cond("kissat", Configuration::isBuiltWithKissat());
print_config_cond("poly", Configuration::isBuiltWithPoly());
print_config_cond("editline", Configuration::isBuiltWithEditline());
-
- std::exit(0);
}
-void OptionsHandler::showCopyright(const std::string& flag)
+void OptionsHandler::showCopyright(const std::string& flag, bool value)
{
+ if (!value) return;
std::cout << Configuration::copyright() << std::endl;
- std::exit(0);
}
-void OptionsHandler::showVersion(const std::string& flag)
+void OptionsHandler::showVersion(const std::string& flag, bool value)
{
+ if (!value) return;
d_options->base.out << Configuration::about() << std::endl;
- std::exit(0);
}
-void OptionsHandler::showDebugTags(const std::string& flag)
+void OptionsHandler::showDebugTags(const std::string& flag, bool value)
{
+ if (!value) return;
if (!Configuration::isDebugBuild())
{
throw OptionException("debug tags not available in non-debug builds");
@@ -434,17 +435,16 @@ void OptionsHandler::showDebugTags(const std::string& flag)
throw OptionException("debug tags not available in non-tracing builds");
}
printTags(Configuration::getDebugTags());
- std::exit(0);
}
-void OptionsHandler::showTraceTags(const std::string& flag)
+void OptionsHandler::showTraceTags(const std::string& flag, bool value)
{
+ if (!value) return;
if (!Configuration::isTracingBuild())
{
throw OptionException("trace tags not available in non-tracing build");
}
printTags(Configuration::getTraceTags());
- std::exit(0);
}
} // namespace options
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 475578c91..6f5016c6c 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -120,15 +120,15 @@ class OptionsHandler
/******************************* main options *******************************/
/** Show the solver build configuration and exit */
- void showConfiguration(const std::string& flag);
+ void showConfiguration(const std::string& flag, bool value);
/** Show copyright information and exit */
- void showCopyright(const std::string& flag);
+ void showCopyright(const std::string& flag, bool value);
/** Show version information and exit */
- void showVersion(const std::string& flag);
+ void showVersion(const std::string& flag, bool value);
/** Show all debug tags and exit */
- void showDebugTags(const std::string& flag);
+ void showDebugTags(const std::string& flag, bool value);
/** Show all trace tags and exit */
- void showTraceTags(const std::string& flag);
+ void showTraceTags(const std::string& flag, bool value);
private:
/** Pointer to the containing Options object.*/
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2478bd276..cf114711a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -780,6 +780,8 @@ set(regress_0_tests
regress0/nl/very-simple-unsat.smt2
regress0/opt-abd-no-use.smt2
regress0/options/ast-and-sexpr.smt2
+ regress0/options/didyoumean.smt2
+ regress0/options/help.smt2
regress0/options/interactive-mode.smt2
regress0/options/set-after-init.smt2
regress0/options/set-and-get-options.smt2
diff --git a/test/regress/regress0/options/didyoumean.smt2 b/test/regress/regress0/options/didyoumean.smt2
new file mode 100644
index 000000000..d95c1bde9
--- /dev/null
+++ b/test/regress/regress0/options/didyoumean.smt2
@@ -0,0 +1,4 @@
+; COMMAND-LINE: --input-agnuage
+; ERROR-SCRUBBER: grep -o "--[a-zA-Z-]+"
+; ERROR-EXPECT: --input-language
+; EXIT: 1 \ No newline at end of file
diff --git a/test/regress/regress0/options/help.smt2 b/test/regress/regress0/options/help.smt2
new file mode 100644
index 000000000..038619c5e
--- /dev/null
+++ b/test/regress/regress0/options/help.smt2
@@ -0,0 +1,4 @@
+; COMMAND-LINE: --help
+; SCRUBBER: grep -o "usage: cvc5"
+; EXPECT: usage: cvc5
+; EXIT: 1 \ No newline at end of file
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 725827abe..0ba29544e 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -97,8 +97,9 @@ add_subdirectory(api)
if(ENABLE_UNIT_TESTING)
add_subdirectory(base)
add_subdirectory(context)
- add_subdirectory(node)
add_subdirectory(main)
+ add_subdirectory(node)
+ add_subdirectory(options)
add_subdirectory(parser)
add_subdirectory(printer)
add_subdirectory(prop)
diff --git a/test/unit/options/CMakeLists.txt b/test/unit/options/CMakeLists.txt
new file mode 100644
index 000000000..da7ac4371
--- /dev/null
+++ b/test/unit/options/CMakeLists.txt
@@ -0,0 +1,17 @@
+###############################################################################
+# Top contributors (to current version):
+# Gereon Kremer
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved. See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# The build system configuration.
+##
+
+# Add unit tests.
+cvc5_add_unit_test_black(options_black options)
diff --git a/test/unit/options/options_black.cpp b/test/unit/options/options_black.cpp
new file mode 100644
index 000000000..1ab4bce23
--- /dev/null
+++ b/test/unit/options/options_black.cpp
@@ -0,0 +1,168 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ * Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Black box testing of the Solver class of the C++ API.
+ */
+
+#include <algorithm>
+#include <limits>
+
+#include "options/option_exception.h"
+#include "options/options_public.h"
+#include "test_api.h"
+
+namespace cvc5 {
+
+using namespace api;
+
+namespace test {
+
+class TestBlackOptions : public TestApi
+{
+};
+
+template <class... Ts>
+struct overloaded : Ts...
+{
+ using Ts::operator()...;
+};
+template <class... Ts>
+overloaded(Ts...) -> overloaded<Ts...>;
+
+TEST_F(TestBlackOptions, set)
+{
+ const std::set<std::string> muted{"copyright",
+ "help",
+ "show-config",
+ "show-debug-tags",
+ "show-trace-tags",
+ "version"};
+ for (const auto& name : options::getNames())
+ {
+ if (muted.count(name))
+ {
+ testing::internal::CaptureStdout();
+ }
+ auto info = d_solver.getOptionInfo(name);
+
+ try
+ {
+ std::visit(
+ overloaded{
+ [this, &name](const OptionInfo::VoidInfo& v) {
+ d_solver.setOption(name, "");
+ },
+ [this, &name](const OptionInfo::ValueInfo<bool>& v) {
+ d_solver.setOption(name, "false");
+ d_solver.setOption(name, "true");
+ },
+ [this, &name](const OptionInfo::ValueInfo<std::string>& v) {
+ d_solver.setOption(name, "foo");
+ },
+ [this, &name](const OptionInfo::NumberInfo<int64_t>& v) {
+ std::pair<int64_t, int64_t> range{
+ std::numeric_limits<int64_t>::min(),
+ std::numeric_limits<int64_t>::max()};
+ if (v.minimum)
+ {
+ EXPECT_THROW(
+ d_solver.setOption(name, std::to_string(*v.minimum - 1)),
+ CVC5ApiOptionException);
+ EXPECT_NO_THROW(
+ d_solver.setOption(name, std::to_string(*v.minimum)));
+ range.first = *v.minimum;
+ }
+ if (v.maximum)
+ {
+ EXPECT_THROW(
+ d_solver.setOption(name, std::to_string(*v.maximum + 1)),
+ CVC5ApiOptionException);
+ EXPECT_NO_THROW(
+ d_solver.setOption(name, std::to_string(*v.maximum)));
+ range.second = *v.maximum;
+ }
+ EXPECT_NO_THROW(d_solver.setOption(
+ name, std::to_string((range.first + range.second) / 2)));
+ },
+ [this, &name](const OptionInfo::NumberInfo<uint64_t>& v) {
+ std::pair<uint64_t, uint64_t> range{
+ std::numeric_limits<uint64_t>::min(),
+ std::numeric_limits<uint64_t>::max()};
+ if (v.minimum)
+ {
+ EXPECT_THROW(
+ d_solver.setOption(name, std::to_string(*v.minimum - 1)),
+ CVC5ApiOptionException);
+ EXPECT_NO_THROW(
+ d_solver.setOption(name, std::to_string(*v.minimum)));
+ range.first = *v.minimum;
+ }
+ if (v.maximum)
+ {
+ EXPECT_THROW(
+ d_solver.setOption(name, std::to_string(*v.maximum + 1)),
+ CVC5ApiOptionException);
+ EXPECT_NO_THROW(
+ d_solver.setOption(name, std::to_string(*v.maximum)));
+ range.second = *v.maximum;
+ }
+ EXPECT_NO_THROW(d_solver.setOption(
+ name, std::to_string((range.first + range.second) / 2)));
+ },
+ [this, &name](const OptionInfo::NumberInfo<double>& v) {
+ std::pair<double, double> range{
+ std::numeric_limits<double>::min(),
+ std::numeric_limits<double>::max()};
+ if (v.minimum)
+ {
+ EXPECT_THROW(
+ d_solver.setOption(name, std::to_string(*v.minimum - 1)),
+ CVC5ApiOptionException);
+ EXPECT_NO_THROW(
+ d_solver.setOption(name, std::to_string(*v.minimum)));
+ range.first = *v.minimum;
+ }
+ if (v.maximum)
+ {
+ EXPECT_THROW(
+ d_solver.setOption(name, std::to_string(*v.maximum + 1)),
+ CVC5ApiOptionException);
+ EXPECT_NO_THROW(
+ d_solver.setOption(name, std::to_string(*v.maximum)));
+ range.second = *v.maximum;
+ }
+ EXPECT_NO_THROW(d_solver.setOption(
+ name, std::to_string((range.first + range.second) / 2)));
+ },
+ [this, &name](const OptionInfo::ModeInfo& v) {
+ EXPECT_THROW(d_solver.setOption(name, "foobarbaz"),
+ CVC5ApiOptionException);
+ for (const auto& m : v.modes)
+ {
+ d_solver.setOption(name, m);
+ }
+ },
+ },
+ info.valueInfo);
+ }
+ catch (const CVC5ApiOptionException&)
+ {
+ }
+ if (muted.count(name))
+ {
+ testing::internal::GetCapturedStdout();
+ }
+ }
+}
+
+} // namespace test
+} // namespace cvc5
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback