From 21387d6484b454970cec70f38d2314cef9ffdde2 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 30 Mar 2022 01:51:42 -0700 Subject: [PATCH] Move cvc5::internal::main to cvc5::main. (#8454) --- src/api/cpp/cvc5.h | 10 +++++----- src/main/command_executor.cpp | 6 ++---- src/main/command_executor.h | 3 --- src/main/driver_unified.cpp | 14 ++++++-------- src/main/main.cpp | 8 ++++---- src/main/main.h | 8 +++----- src/main/options.h | 4 ++-- src/main/options_template.cpp | 6 ++++-- src/main/signal_handlers.cpp | 7 +++---- src/main/signal_handlers.h | 6 ++---- src/main/time_limit.cpp | 13 ++++++------- src/main/time_limit.h | 6 ++---- 12 files changed, 39 insertions(+), 52 deletions(-) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index cf55b0589..24107281f 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -36,6 +36,10 @@ namespace cvc5 { class Command; +namespace main { +class CommandExecutor; +} // namespace main + namespace internal { #ifndef DOXYGEN_SKIP @@ -56,10 +60,6 @@ class Rational; class Result; class SynthResult; class StatisticsRegistry; - -namespace main { -class CommandExecutor; -} // namespace main } // namespace internal class Solver; @@ -3047,7 +3047,7 @@ class CVC5_EXPORT Solver friend class Grammar; friend class Op; friend class cvc5::Command; - friend class internal::main::CommandExecutor; + friend class main::CommandExecutor; friend class Sort; friend class Term; diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index f6206e84e..801375db1 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -29,8 +29,7 @@ #include "smt/command.h" #include "smt/solver_engine.h" -namespace cvc5::internal { -namespace main { +namespace cvc5::main { // Function to cancel any (externally-imposed) limit on CPU time. // This is used for competitions while a solution (proof or model) @@ -220,5 +219,4 @@ void CommandExecutor::flushOutputStreams() { d_solver->getDriverOptions().err() << std::flush; } -} // namespace main -} // namespace cvc5::internal +} // namespace cvc5::main diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 9ee3cb4e1..1b02d6a66 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -26,8 +26,6 @@ namespace cvc5 { class Command; -namespace internal { - namespace main { class CommandExecutor @@ -113,7 +111,6 @@ bool solverInvoke(cvc5::Solver* solver, std::ostream& out); } // namespace main -} // namespace internal } // namespace cvc5 #endif /* CVC5__MAIN__COMMAND_EXECUTOR_H */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 51420dd21..c19295b49 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -42,10 +42,9 @@ using namespace std; using namespace cvc5::internal; using namespace cvc5::parser; -using namespace cvc5::internal::main; +using namespace cvc5::main; -namespace cvc5::internal { -namespace main { +namespace cvc5::main { /** Full argv[0] */ const char* progPath; @@ -54,10 +53,9 @@ const char* progPath; std::string progName; /** A pointer to the CommandExecutor (the signal handlers need it) */ -std::unique_ptr pExecutor; +std::unique_ptr pExecutor; -} // namespace main -} // namespace cvc5::internal +} // namespace cvc5::main int runCvc5(int argc, char* argv[], std::unique_ptr& solver) { @@ -71,10 +69,10 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) cvc5::DriverOptions dopts = solver->getDriverOptions(); // Parse the options - std::vector filenames = main::parse(*solver, argc, argv, progName); + std::vector filenames = parse(*solver, argc, argv, progName); if (solver->getOptionInfo("help").boolValue()) { - main::printUsage(progName, dopts.out()); + printUsage(progName, dopts.out()); exit(1); } for (const auto& name : {"show-config", diff --git a/src/main/main.cpp b/src/main/main.cpp index 9910bc7ef..a11fa20c8 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -22,6 +22,7 @@ #include "options/option_exception.h" using namespace cvc5::internal; +using namespace cvc5::main; /** * cvc5's main() routine is just an exception-safe wrapper around runCvc5. @@ -68,13 +69,12 @@ int main(int argc, char* argv[]) solver->getDriverOptions().err() << "(error \"" << e << "\")" << std::endl; } - if (solver->getOptionInfo("stats").boolValue() - && main::pExecutor != nullptr) + if (solver->getOptionInfo("stats").boolValue() && pExecutor != nullptr) { - main::pExecutor->printStatistics(solver->getDriverOptions().err()); + pExecutor->printStatistics(solver->getDriverOptions().err()); } } // Make sure that the command executor is destroyed before the node manager. - main::pExecutor.reset(); + pExecutor.reset(); exit(1); } diff --git a/src/main/main.h b/src/main/main.h index ef1a6003f..4d4c5f5fb 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -22,8 +22,7 @@ #ifndef CVC5__MAIN__MAIN_H #define CVC5__MAIN__MAIN_H -namespace cvc5::internal { -namespace main { +namespace cvc5::main { class CommandExecutor; @@ -34,7 +33,7 @@ extern const char* progPath; extern std::string progName; /** A reference for use by the signal handlers to print statistics */ -extern std::unique_ptr pExecutor; +extern std::unique_ptr pExecutor; /** * If true, will not spin on segfault even when CVC5_DEBUG is on. @@ -43,8 +42,7 @@ extern std::unique_ptr pExecutor; */ extern bool segvSpin; -} // namespace main -} // namespace cvc5::internal +} // namespace cvc5::main /** Actual cvc5 driver functions **/ int runCvc5(int argc, char* argv[], std::unique_ptr&); diff --git a/src/main/options.h b/src/main/options.h index 7c496bdfc..6a5636349 100644 --- a/src/main/options.h +++ b/src/main/options.h @@ -22,7 +22,7 @@ #include "api/cpp/cvc5.h" -namespace cvc5::internal::main { +namespace cvc5::main { /** * Print overall command-line option usage message to the given output stream @@ -47,6 +47,6 @@ std::vector parse(cvc5::Solver& solver, char* argv[], std::string& binaryName); -} // namespace cvc5::internal::options +} // namespace cvc5::main #endif diff --git a/src/main/options_template.cpp b/src/main/options_template.cpp index dbd71b1c1..ac49a911c 100644 --- a/src/main/options_template.cpp +++ b/src/main/options_template.cpp @@ -44,7 +44,9 @@ extern int optreset; #include #include -namespace cvc5::internal::main { +namespace cvc5::main { + +using namespace cvc5::internal; // clang-format off static const std::string commonOptionsDescription = @@ -277,4 +279,4 @@ std::vector parse(cvc5::Solver& solver, return nonoptions; } -} // namespace cvc5::internal::options +} // namespace cvc5::main diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp index a531da839..5aaa9801e 100644 --- a/src/main/signal_handlers.cpp +++ b/src/main/signal_handlers.cpp @@ -41,8 +41,8 @@ using cvc5::internal::Exception; using namespace std; -namespace cvc5::internal { -namespace main { +namespace cvc5::main { +using namespace cvc5::internal; /** * If true, will not spin on segfault even when CVC5_DEBUG is on. @@ -344,5 +344,4 @@ void cleanup() noexcept } } // namespace signal_handlers -} // namespace main -} // namespace cvc5::internal +} // namespace cvc5::main diff --git a/src/main/signal_handlers.h b/src/main/signal_handlers.h index 5394dec15..875ad242b 100644 --- a/src/main/signal_handlers.h +++ b/src/main/signal_handlers.h @@ -16,8 +16,7 @@ #ifndef CVC5__MAIN__SIGNAL_HANDLERS_H #define CVC5__MAIN__SIGNAL_HANDLERS_H -namespace cvc5::internal { -namespace main { +namespace cvc5::main { namespace signal_handlers { /** @@ -39,7 +38,6 @@ void install(); void cleanup(); } // namespace signal_handlers -} // namespace main -} // namespace cvc5::internal +} // namespace cvc5::main #endif /* CVC5__MAIN__SIGNAL_HANDLERS_H */ diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp index b557729ee..93f9d2a41 100644 --- a/src/main/time_limit.cpp +++ b/src/main/time_limit.cpp @@ -58,8 +58,7 @@ #include "base/exception.h" #include "signal_handlers.h" -namespace cvc5::internal { -namespace main { +namespace cvc5::main { #if HAVE_SETITIMER TimeLimit::~TimeLimit() {} @@ -92,8 +91,8 @@ TimeLimit install_time_limit(uint64_t ms) sigemptyset(&sact.sa_mask); if (sigaction(SIGALRM, &sact, NULL)) { - throw Exception(std::string("sigaction(SIGALRM) failure: ") - + strerror(errno)); + throw internal::Exception(std::string("sigaction(SIGALRM) failure: ") + + strerror(errno)); } // Check https://linux.die.net/man/2/setitimer @@ -108,7 +107,8 @@ TimeLimit install_time_limit(uint64_t ms) // Argument 3: old timer configuration, we don't want to know if (setitimer(ITIMER_REAL, &timerspec, nullptr)) { - throw Exception(std::string("timer_settime() failure: ") + strerror(errno)); + throw internal::Exception(std::string("timer_settime() failure: ") + + strerror(errno)); } #else abort_timer_flag.store(false); @@ -131,5 +131,4 @@ TimeLimit install_time_limit(uint64_t ms) return TimeLimit(); } -} // namespace main -} // namespace cvc5::internal +} // namespace cvc5::main diff --git a/src/main/time_limit.h b/src/main/time_limit.h index 74686823e..e693e6431 100644 --- a/src/main/time_limit.h +++ b/src/main/time_limit.h @@ -18,8 +18,7 @@ #include -namespace cvc5::internal { -namespace main { +namespace cvc5::main { /** * This class makes sure that the main thread signals back to the time @@ -45,7 +44,6 @@ struct TimeLimit */ TimeLimit install_time_limit(uint64_t ms); -} // namespace main -} // namespace cvc5::internal +} // namespace cvc5::main #endif /* CVC5__MAIN__TIME_LIMIT_H */ -- 2.30.2