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

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index cf55b0589f1dcb41ffce21ba5bba278e36f18392..24107281f73d7ba916953b81377cd7df54aaf181 100644 (file)
--- 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 f6206e84e21a08f3ad8e022559c56c7cbefe3dc3..801375db1a6205c5c5c375f27eb79d8e5f2cc40f 100644 (file)
--- 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 9ee3cb4e12d7b975d073f8f48884a57582609f5c..1b02d6a66e2140ac84039766a1f6589e54e2e361 100644 (file)
--- 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 51420dd21276e24a5d873c6766ff739f11d3e9fc..c19295b497e662136098d2f40dd97cf1f3498024 100644 (file)
--- 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 9910bc7efa2e9534af50f79abf5b5007374e235e..a11fa20c8b4110ba17efb1c3520c386e6b01829b 100644 (file)
--- 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 ef1a6003f38afea7f11a5e70ef6695e5d7463034..4d4c5f5fb24114b245fb2f85d512ec9bf159c169 100644 (file)
--- 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 7c496bdfcede73aa6d5e8387d705a8892c341c2d..6a5636349b60f6fce6ca23c819b593ac76313376 100644 (file)
--- 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 dbd71b1c12be8b7e1af0f1331f10424e79afbdb3..ac49a911c7c02909f5586cacfa04c2bf5cfceb89 100644 (file)
--- 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 a531da83991bf8180a29bad0cfc0409b01719262..5aaa9801e3f2403188e7182c910edf1c9eecd7b0 100644 (file)
--- 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 5394dec154f256b15de643a981790a81ea497e62..875ad242b7670a2b998529aef1ac8b15f4251f23 100644 (file)
--- 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 b557729ee816c8a819085d756e006e88e20ea6b1..93f9d2a413f626578fcfbfb2693455a660f409bf 100644 (file)
--- 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 74686823efe51baa4cd31c2e2761941d5bb43a88..e693e6431ed34daf4b9f996db4a2839492162d67 100644 (file)
--- 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 */