This PR adds a generic unit test for api::Solver::setOption(). It iterates over all options and calls setOption() with somewhat cleverly chosen values according to getOptionInfo().
While building this, it occurred to me that calling std::exit() in an option handler is weird (for example for version) and we should do this in the driver instead. This PR also refactors this issue, moving all calls to std::exit() from the option handlers into the driver.
} // 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
// 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
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
";
// 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
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]]
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]]
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]]
#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"
// 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;
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
{
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(
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
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());
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");
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
/******************************* 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.*/
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
--- /dev/null
+; COMMAND-LINE: --input-agnuage
+; ERROR-SCRUBBER: grep -o "--[a-zA-Z-]+"
+; ERROR-EXPECT: --input-language
+; EXIT: 1
\ No newline at end of file
--- /dev/null
+; COMMAND-LINE: --help
+; SCRUBBER: grep -o "usage: cvc5"
+; EXPECT: usage: cvc5
+; EXIT: 1
\ No newline at end of file
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)
--- /dev/null
+###############################################################################
+# 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)
--- /dev/null
+/******************************************************************************
+ * 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
projects / cvc5.git / commitdiff