From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 2 Sep 2021 18:21:56 +0000 (-0700)
Subject: Driver & Options cleanup (#7109)
X-Git-Tag: cvc5-1.0.0~1288
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b88b3cb5d93e4a2639d4ad647389953656e4c9ea;p=cvc5.git

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.
---

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<api::Solver>& 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 <iosfwd>
 #include <string>
 
-#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 <stdio.h>
-#include <unistd.h>
-
-#include <cstdlib>
-#include <cstring>
-#include <fstream>
 #include <iostream>
 
 #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<api::Solver> solver;
+  std::unique_ptr<api::Solver> solver = std::make_unique<api::Solver>();
   try
   {
-    solver = std::make_unique<api::Solver>();
     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 <cstdint>
 
 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 <module>_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 <sstream>
 
 #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"