From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 30 Mar 2022 08:51:42 +0000 (-0700)
Subject: Move cvc5::internal::main to cvc5::main. (#8454)
X-Git-Tag: cvc5-1.0.0~125
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=21387d6484b454970cec70f38d2314cef9ffdde2;p=cvc5.git

Move cvc5::internal::main to cvc5::main. (#8454)
---

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<cvc5::internal::main::CommandExecutor> pExecutor;
+std::unique_ptr<CommandExecutor> pExecutor;
 
-}  // namespace main
-}  // namespace cvc5::internal
+}  // namespace cvc5::main
 
 int runCvc5(int argc, char* argv[], std::unique_ptr<cvc5::Solver>& solver)
 {
@@ -71,10 +69,10 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<cvc5::Solver>& solver)
   cvc5::DriverOptions dopts = solver->getDriverOptions();
 
   // Parse the options
-  std::vector<string> filenames = main::parse(*solver, argc, argv, progName);
+  std::vector<string> 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<cvc5::internal::main::CommandExecutor> pExecutor;
+extern std::unique_ptr<CommandExecutor> pExecutor;
 
 /**
  * If true, will not spin on segfault even when CVC5_DEBUG is on.
@@ -43,8 +42,7 @@ extern std::unique_ptr<cvc5::internal::main::CommandExecutor> 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<cvc5::Solver>&);
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<std::string> 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 <iostream>
 #include <limits>
 
-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<std::string> 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 <cstdint>
 
-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 */