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 1e8d848a453fab3662c31b60db9a0be4aa3d42c4..a9897f53e358302848a6159ea717016c35c8bf8a 100644 (file)
--- 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 6c991ce29e3c99cf94bdb095e5bd9e92a2befdf8..28b786437d22722a2960db10628d4f798a4b1ca5 100644 (file)
--- 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 d4736470f06ef658b3801cf20d284becf4e910d8..bf05a1ec7c920d6d239c2b42e5ecaa1486cf19ab 100644 (file)
--- 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 bbc0b6ecebf530854c6bfaf134f53bfdfadae407..141b0c46cfc7e4b430facc0c16098c2027645d0c 100644 (file)
--- 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 de0a28a266d4bdd5bc1071865cf2517c1bc7275b..6c9a1920fb688a0327b60f7c74b3f6414237702a 100644 (file)
--- 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 adc2d845624307564ca09ea33636a3d859c5fb7c..e3035e0d63d95fe2b13e67477dea99fbfcd75457 100644 (file)
--- 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 41d6766e8bcf140eb1508a716be91146bddf0cdb..fc03de16721a65b40cfad1ed9eaa2cd29dbc338b 100644 (file)
--- 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 289fa95dbd615beb40cc7c16eccaa809b1a7e1c5..62e70214d21161a87f9c71f40b666f1029eac100 100644 (file)
--- 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 3a8e2a9810cf2623c4bec2015563def156eb65f0..0d830e1093bbe8efc2d10253de0118619a404bf2 100644 (file)
--- 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 f19b903a626b65e93abeaa8840e16ef924d8312b..6fc683368a42a8a78fc19986ef8dcf0dd007793e 100644 (file)
--- 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 888f722a72a84ad8f878638701e3b902967c19c6..d7ce1bfc1782bc6bf55d34e2e4a72e315ceb639d 100644 (file)
--- 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"