From b88b3cb5d93e4a2639d4ad647389953656e4c9ea Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 2 Sep 2021 11:21:56 -0700 Subject: [PATCH] Driver & Options cleanup (#7109) This PR does some cleanup in the driver and the options. It removes the now obsolete public attribute that allowed using the options in the driver, and removes a bunch of includes from the driver that are no longer necessary. --- src/main/command_executor.h | 1 - src/main/driver_unified.cpp | 1 - src/main/interactive_shell.h | 5 ---- src/main/main.cpp | 43 +++++++++------------------------ src/main/time_limit.h | 2 +- src/options/base_options.toml | 1 - src/options/main_options.toml | 1 - src/options/mkoptions.py | 8 +----- src/options/module_template.h | 2 +- src/options/parser_options.toml | 1 - test/api/smt2_compliance.cpp | 2 -- 11 files changed, 14 insertions(+), 53 deletions(-) diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 1e8d848a4..a9897f53e 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -21,7 +21,6 @@ #include "api/cpp/cvc5.h" #include "expr/symbol_manager.h" -#include "options/options.h" namespace cvc5 { diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 6c991ce29..28b786437 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -180,7 +180,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) int returnValue = 0; { - // pass filename to solver (options & statistics) solver->setInfo("filename", filenameStr); // Parse and execute commands until we are done diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index d4736470f..bf05a1ec7 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -19,14 +19,9 @@ #include #include -#include "options/language.h" -#include "options/options.h" -#include "util/unsafe_interrupt_exception.h" - namespace cvc5 { class Command; -class Options; namespace api { class Solver; diff --git a/src/main/main.cpp b/src/main/main.cpp index bbc0b6ece..141b0c46c 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -14,46 +14,23 @@ */ #include "main/main.h" -#include -#include - -#include -#include -#include #include #include "api/cpp/cvc5.h" #include "base/configuration.h" -#include "base/output.h" #include "main/command_executor.h" -#include "main/interactive_shell.h" -#include "options/base_options.h" -#include "options/language.h" #include "options/option_exception.h" -#include "options/options.h" -#include "parser/parser.h" -#include "parser/parser_builder.h" -#include "parser/parser_exception.h" -#include "util/result.h" -using namespace std; using namespace cvc5; -using namespace cvc5::main; -using namespace cvc5::language; /** - * cvc5's main() routine is just an exception-safe wrapper around cvc5. - * Please don't construct anything here. Even if the constructor is - * inside the try { }, an exception during destruction can cause - * problems. That's why main() wraps runCvc5() in the first place. - * Put everything in runCvc5(). + * cvc5's main() routine is just an exception-safe wrapper around runCvc5. */ int main(int argc, char* argv[]) { - std::unique_ptr solver; + std::unique_ptr solver = std::make_unique(); try { - solver = std::make_unique(); return runCvc5(argc, argv, solver); } catch (cvc5::api::CVC5ApiOptionException& e) @@ -61,18 +38,20 @@ int main(int argc, char* argv[]) #ifdef CVC5_COMPETITION_MODE solver->getDriverOptions().out() << "unknown" << std::endl; #endif - cerr << "(error \"" << e.getMessage() << "\")" << endl - << endl - << "Please use --help to get help on command-line options." << endl; + std::cerr << "(error \"" << e.getMessage() << "\")" << std::endl + << std::endl + << "Please use --help to get help on command-line options." + << std::endl; } catch (OptionException& e) { #ifdef CVC5_COMPETITION_MODE solver->getDriverOptions().out() << "unknown" << std::endl; #endif - cerr << "(error \"" << e.getMessage() << "\")" << endl - << endl - << "Please use --help to get help on command-line options." << endl; + std::cerr << "(error \"" << e.getMessage() << "\")" << std::endl + << std::endl + << "Please use --help to get help on command-line options." + << std::endl; } catch (Exception& e) { @@ -92,7 +71,7 @@ int main(int argc, char* argv[]) if (solver->getOptionInfo("stats").boolValue() && main::pExecutor != nullptr) { - pExecutor->printStatistics(solver->getDriverOptions().err()); + main::pExecutor->printStatistics(solver->getDriverOptions().err()); } } exit(1); diff --git a/src/main/time_limit.h b/src/main/time_limit.h index de0a28a26..6c9a1920f 100644 --- a/src/main/time_limit.h +++ b/src/main/time_limit.h @@ -16,7 +16,7 @@ #ifndef CVC5__MAIN__TIME_LIMIT_H #define CVC5__MAIN__TIME_LIMIT_H -#include "options/options.h" +#include namespace cvc5 { namespace main { diff --git a/src/options/base_options.toml b/src/options/base_options.toml index adc2d8456..e3035e0d6 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -1,6 +1,5 @@ id = "BASE" name = "Base" -public = true [[option]] name = "in" diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 41d6766e8..fc03de167 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -1,6 +1,5 @@ id = "DRIVER" name = "Driver" -public = true [[option]] name = "version" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 289fa95db..62e70214d 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -50,7 +50,7 @@ import toml ### Allowed attributes for module/option MODULE_ATTR_REQ = ['id', 'name'] -MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option', 'public'] +MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option'] OPTION_ATTR_REQ = ['category', 'type'] OPTION_ATTR_ALL = OPTION_ATTR_REQ + [ @@ -608,13 +608,7 @@ def codegen_module(module, dst_dir, tpls): help=help_mode_format(option), long=option.long.split('=')[0])) - if module.public: - visibility_include = '#include "cvc5_public.h"' - else: - visibility_include = '#include "cvc5_private.h"' - data = { - 'visibility_include': visibility_include, 'id_cap': module.id_cap, 'id': module.id, 'includes': '\n'.join(sorted(list(includes))), diff --git a/src/options/module_template.h b/src/options/module_template.h index 3a8e2a981..0d830e109 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -16,7 +16,7 @@ * expands this template and generates a _options.h file. */ -${visibility_include}$ +#include "cvc5_private.h" #ifndef CVC5__OPTIONS__${id_cap}$_H #define CVC5__OPTIONS__${id_cap}$_H diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index f19b903a6..6fc683368 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -1,6 +1,5 @@ id = "PARSER" name = "Parser" -public = true [[option]] name = "strictParsing" diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 888f722a7..d7ce1bfc1 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -18,9 +18,7 @@ #include #include "api/cpp/cvc5.h" -#include "options/base_options.h" #include "options/options.h" -#include "options/options_public.h" #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" -- 2.30.2