From: Gereon Kremer Date: Thu, 2 Dec 2021 00:30:09 +0000 (-0800) Subject: Add unit tests for api::Solver::setOption() (#7708) X-Git-Tag: cvc5-1.0.0~738 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6afc21a16e740d4fb4a16cdbd9a6ff745c7ce00c;p=cvc5.git Add unit tests for api::Solver::setOption() (#7708) 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. --- 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 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& solver) { // Initialize the signal handlers @@ -92,15 +72,24 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) // Parse the options std::vector 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& tags) +void printTags(const std::vector& 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 +#include + +#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 +struct overloaded : Ts... +{ + using Ts::operator()...; +}; +template +overloaded(Ts...) -> overloaded; + +TEST_F(TestBlackOptions, set) +{ + const std::set 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& v) { + d_solver.setOption(name, "false"); + d_solver.setOption(name, "true"); + }, + [this, &name](const OptionInfo::ValueInfo& v) { + d_solver.setOption(name, "foo"); + }, + [this, &name](const OptionInfo::NumberInfo& v) { + std::pair range{ + std::numeric_limits::min(), + std::numeric_limits::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& v) { + std::pair range{ + std::numeric_limits::min(), + std::numeric_limits::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& v) { + std::pair range{ + std::numeric_limits::min(), + std::numeric_limits::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