diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/CMakeLists.txt | 7 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 9 | ||||
-rw-r--r-- | src/main/main.h | 1 | ||||
-rw-r--r-- | src/main/options.h | 64 | ||||
-rw-r--r-- | src/main/options_template.cpp | 287 |
5 files changed, 362 insertions, 6 deletions
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 029397832..27086d3fb 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -19,17 +19,22 @@ set(libmain_src_files interactive_shell.cpp interactive_shell.h main.h + options.h signal_handlers.cpp signal_handlers.h time_limit.cpp time_limit.h ) +set(libmain_gen_src_files + ${CMAKE_CURRENT_BINARY_DIR}/options.cpp +) +set_source_files_properties(${libmain_gen_src_files} PROPERTIES GENERATED TRUE) #-----------------------------------------------------------------------------# # Build object library since we will use the object files for cvc5-bin and # main-test library. -add_library(main OBJECT ${libmain_src_files}) +add_library(main OBJECT ${libmain_src_files} ${libmain_gen_src_files}) target_compile_definitions(main PRIVATE -D__BUILDING_CVC5DRIVER) if(ENABLE_SHARED) set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON) diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 93d458c32..9ceed82f7 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -31,6 +31,7 @@ #include "main/command_executor.h" #include "main/interactive_shell.h" #include "main/main.h" +#include "main/options.h" #include "main/signal_handlers.h" #include "main/time_limit.h" #include "options/base_options.h" @@ -89,9 +90,9 @@ void printUsage(const Options& opts, bool full) { << endl << "cvc5 options:" << endl; if(full) { - options::printUsage(ss.str(), *opts.base.out); + main::printUsage(ss.str(), *opts.base.out); } else { - options::printShortUsage(ss.str(), *opts.base.out); + main::printShortUsage(ss.str(), *opts.base.out); } } @@ -109,7 +110,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver) Options* opts = &pExecutor->getOptions(); // Parse the options - std::vector<string> filenames = options::parse(*opts, argc, argv, progName); + std::vector<string> filenames = main::parse(*solver, argc, argv, progName); auto limit = install_time_limit(*opts); @@ -120,7 +121,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver) } else if (opts->base.languageHelp) { - options::printLanguageHelp(*opts->base.out); + main::printLanguageHelp(*opts->base.out); exit(1); } else if (opts->driver.version) diff --git a/src/main/main.h b/src/main/main.h index e76836600..5643588e1 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -65,6 +65,5 @@ extern bool segvSpin; /** Actual cvc5 driver functions **/ int runCvc5(int argc, char* argv[], std::unique_ptr<cvc5::api::Solver>&); -void printUsage(const cvc5::Options&, bool full = false); #endif /* CVC5__MAIN__MAIN_H */ diff --git a/src/main/options.h b/src/main/options.h new file mode 100644 index 000000000..a2c26273b --- /dev/null +++ b/src/main/options.h @@ -0,0 +1,64 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Options utilities used in the driver. + */ + +#ifndef CVC5__MAIN__OPTIONS_H +#define CVC5__MAIN__OPTIONS_H + +#include <iosfwd> +#include <string> +#include <vector> + +#include "api/cpp/cvc5.h" + +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" + */ +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); + +/** Print help for the --lang command line option */ +void printLanguageHelp(std::ostream& os); + +/** + * Initialize the Options object options based on the given + * command-line arguments given in argc and argv. The return value + * is what's left of the command line (that is, the non-option + * arguments). + * + * This function uses getopt_long() and is not thread safe. + * + * Throws OptionException on failures. + * + * Preconditions: options and argv must be non-null. + */ +std::vector<std::string> parse(api::Solver& solver, + int argc, + char* argv[], + std::string& binaryName); + +} // namespace cvc5::options + +#endif diff --git a/src/main/options_template.cpp b/src/main/options_template.cpp new file mode 100644 index 000000000..87a5fc158 --- /dev/null +++ b/src/main/options_template.cpp @@ -0,0 +1,287 @@ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Gereon Kremer, Andrew Reynolds + * + * 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. + * **************************************************************************** + * + * Options utilities used in the driver. + */ + +#include "main/options.h" + +#if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__) +// force use of optreset; mingw32 croaks on argv-switching otherwise +#include "base/cvc5config.h" +#define _BSD_SOURCE +#undef HAVE_DECL_OPTRESET +#define HAVE_DECL_OPTRESET 1 +#define CVC5_IS_NOT_REALLY_BSD +#endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */ + +#ifdef __MINGW64__ +extern int optreset; +#endif /* __MINGW64__ */ + +#include <getopt.h> + +// clean up +#ifdef CVC5_IS_NOT_REALLY_BSD +# undef _BSD_SOURCE +#endif /* CVC5_IS_NOT_REALLY_BSD */ + +#include "base/check.h" +#include "base/output.h" +#include "options/didyoumean.h" +#include "options/option_exception.h" + +#include <cstring> +#include <iostream> +#include <limits> + +namespace cvc5::main { + +// clang-format off +static const std::string commonOptionsDescription = + "Most commonly-used cvc5 options:\n" +${help_common}$ + ; + +static const std::string additionalOptionsDescription = + "Additional cvc5 options:\n" +${help_others}$; + +static const std::string optionsFootnote = "\n\ +[*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ + sense of the option.\n\ +"; + +static const std::string languageDescription = + "\ +Languages currently supported as arguments to the -L / --lang option:\n\ + auto attempt to automatically determine language\n\ + cvc | presentation | pl CVC presentation language\n\ + smt | smtlib | smt2 |\n\ + smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ + tptp TPTP format (cnf, fof and tff)\n\ + sygus | sygus2 SyGuS version 2.0\n\ +\n\ +Languages currently supported as arguments to the --output-lang option:\n\ + auto match output language to input language\n\ + cvc | presentation | pl CVC presentation language\n\ + smt | smtlib | smt2 |\n\ + smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ + tptp TPTP format\n\ + ast internal format (simple syntax trees)\n\ +"; +// clang-format on + +void printUsage(const std::string& msg, std::ostream& os) { + os << msg << "\n" << commonOptionsDescription << "\n\n" << additionalOptionsDescription << std::endl + << optionsFootnote << std::endl << std::flush; +} + +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 << std::flush; +} + +void printLanguageHelp(std::ostream& os) { + os << languageDescription << std::flush; +} + +/** + * This is a table of long options. By policy, each short option + * should have an equivalent long option (but the reverse isn't the + * case), so this table should thus contain all command-line options. + * + * Each option in this array has four elements: + * + * 1. the long option string + * 2. argument behavior for the option: + * no_argument - no argument permitted + * required_argument - an argument is expected + * optional_argument - an argument is permitted but not required + * 3. this is a pointer to an int which is set to the 4th entry of the + * array if the option is present; or NULL, in which case + * getopt_long() returns the 4th entry + * 4. the return value for getopt_long() when this long option (or the + * value to set the 3rd entry to; see #3) + */ +// clang-format off +static struct option cmdlineOptions[] = { + ${cmdline_options}$ + {nullptr, no_argument, nullptr, '\0'} +}; +// clang-format on + +std::string suggestCommandLineOptions(const std::string& optionName) +{ + DidYouMean didYouMean; + + const char* opt; + for(size_t i = 0; (opt = cmdlineOptions[i].name) != nullptr; ++i) { + didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); + } + + return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); +} + +void parseInternal(api::Solver& solver, int argc, + char* argv[], + std::vector<std::string>& nonoptions) +{ + Assert(argv != nullptr); + if(Debug.isOn("options")) { + Debug("options") << "starting a new parseInternal with " + << argc << " arguments" << std::endl; + for( int i = 0; i < argc ; i++ ){ + Assert(argv[i] != NULL); + Debug("options") << " argv[" << i << "] = " << argv[i] << std::endl; + } + } + + // Reset getopt(), in the case of multiple calls to parse(). + // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0. + optind = 0; +#if HAVE_DECL_OPTRESET + optreset = 1; // on BSD getopt() (e.g. Mac OS), might need this +#endif /* HAVE_DECL_OPTRESET */ + + // We must parse the binary name, which is manually ignored below. Setting + // this to 1 leads to incorrect behavior on some platforms. + int main_optind = 0; + int old_optind; + + + while(true) { // Repeat Forever + + optopt = 0; + + optind = main_optind; + old_optind = main_optind; + + // If we encounter an element that is not at zero and does not start + // with a "-", this is a non-option. We consume this element as a + // non-option. + if (main_optind > 0 && main_optind < argc && + argv[main_optind][0] != '-') { + Debug("options") << "enqueueing " << argv[main_optind] + << " as a non-option." << std::endl; + nonoptions.push_back(argv[main_optind]); + ++main_optind; + continue; + } + + + Debug("options") << "[ before, main_optind == " << main_optind << " ]" + << std::endl; + Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; + Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]" + << std::endl; + // clang-format off + int c = getopt_long(argc, argv, + "+:${options_short}$", + cmdlineOptions, NULL); + // clang-format on + + main_optind = optind; + + Debug("options") << "[ got " << int(c) << " (" << char(c) << ") ]" + << "[ next option will be at pos: " << optind << " ]" + << std::endl; + + // The initial getopt_long call should always determine that argv[0] + // is not an option and returns -1. We always manually advance beyond + // this element. + if ( old_optind == 0 && c == -1 ) { + Assert(main_optind > 0); + continue; + } + + if ( c == -1 ) { + if(Debug.isOn("options")) { + Debug("options") << "done with option parsing" << std::endl; + for(int index = optind; index < argc; ++index) { + Debug("options") << "remaining " << argv[index] << std::endl; + } + } + break; + } + + std::string option = argv[old_optind == 0 ? 1 : old_optind]; + std::string optionarg = (optarg == nullptr) ? "" : optarg; + + Debug("preemptGetopt") << "processing option " << c + << " (`" << char(c) << "'), " << option << std::endl; + + // clang-format off + switch(c) + { + ${options_handler}$ + + case ':' : + // This can be a long or short option, and the way to get at the + // name of it is different. + throw OptionException(std::string("option `") + option + + "' missing its required argument"); + + case '?': + default: + throw OptionException(std::string("can't understand option `") + option + + "'" + suggestCommandLineOptions(option)); + } + } + // clang-format on + + Debug("options") << "got " << nonoptions.size() + << " non-option arguments." << std::endl; +} + +/** + * Parse argc/argv and put the result into a cvc5::Options. + * The return value is what's left of the command line (that is, the + * non-option arguments). + * + * Throws OptionException on failures. + */ +std::vector<std::string> parse( + api::Solver& solver, int argc, char* argv[], std::string& binaryName) +{ + Assert(argv != nullptr); + + const char *progName = argv[0]; + + // To debug options parsing, you may prefer to simply uncomment this + // and recompile. Debug flags have not been parsed yet so these have + // not been set. + //DebugChannel.on("options"); + + Debug("options") << "argv == " << argv << std::endl; + + // Find the base name of the program. + const char *x = strrchr(progName, '/'); + if(x != nullptr) { + progName = x + 1; + } + binaryName = std::string(progName); + + std::vector<std::string> nonoptions; + parseInternal(solver, argc, argv, nonoptions); + if (Debug.isOn("options")){ + for (const auto& no: nonoptions){ + Debug("options") << "nonoptions " << no << std::endl; + } + } + + return nonoptions; +} + +} // namespace cvc5::options |