Support public option modules (#6691)

This PR adds the possibility to make option modules public. As shown on the example of the main driver options, this allows to get rid of the wrappers from options_public.h. We plan to make only very few option modules public (i.e. main and parser).

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 4f82ac1aefc242cb33d885546cad91a7eb7608e8..caa0340bd2e998d0c1b10cd089340316b6cd3a93 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -35,6 +35,7 @@
 #include "main/time_limit.h"
 #include "options/options.h"
 #include "options/options_public.h"
+#include "options/main_options.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -112,7 +113,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
   string progNameStr = options::getBinaryName(opts);
   progName = &progNameStr;
 
-  if (options::getHelp(opts))
+  if (opts.driver.help)
   {
     printUsage(opts, true);
     exit(1);
@@ -122,13 +123,13 @@ int runCvc5(int argc, char* argv[], Options& opts)
     Options::printLanguageHelp(*(options::getOut(opts)));
     exit(1);
   }
-  else if (options::getVersion(opts))
+  else if (opts.driver.version)
   {
     *(options::getOut(opts)) << Configuration::about().c_str() << flush;
     exit(0);
   }
 
-  segvSpin = options::getSegvSpin(opts);
+  segvSpin = opts.driver.segvSpin;
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC5_COMPETITION_MODE
@@ -146,7 +147,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
   // if we're reading from stdin on a TTY, default to interactive mode
   if (!options::wasSetByUserInteractive(opts))
   {
-    options::setInteractive(inputFromStdin && isatty(fileno(stdin)), opts);
+    opts.driver.interactive = inputFromStdin && isatty(fileno(stdin));
   }
 
   // Auto-detect input language by filename extension
@@ -212,9 +213,9 @@ int runCvc5(int argc, char* argv[], Options& opts)
     // Parse and execute commands until we are done
     std::unique_ptr<Command> cmd;
     bool status = true;
-    if (options::getInteractive(opts) && inputFromStdin)
+    if (opts.driver.interactive && inputFromStdin)
     {
-      if (options::getTearDownIncremental(opts) > 0)
+      if (opts.driver.tearDownIncremental > 0)
       {
         throw Exception(
             "--tear-down-incremental doesn't work in interactive mode");
@@ -227,7 +228,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
       }
       InteractiveShell shell(pExecutor->getSolver(),
                              pExecutor->getSymbolManager());
-      if (options::getInteractivePrompt(opts))
+      if (opts.driver.interactivePrompt)
       {
         CVC5Message() << Configuration::getPackageName() << " "
                       << Configuration::getVersionString();
@@ -257,10 +258,10 @@ int runCvc5(int argc, char* argv[], Options& opts)
         }
       }
     }
-    else if (options::getTearDownIncremental(opts) > 0)
+    else if (opts.driver.tearDownIncremental > 0)
     {
       if (!options::getIncrementalSolving(opts)
-          && options::getTearDownIncremental(opts) > 1)
+          && opts.driver.tearDownIncremental > 1)
       {
         // For tear-down-incremental values greater than 1, need incremental
         // on too.
@@ -313,7 +314,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
         }
 
         if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
-          if (needReset >= options::getTearDownIncremental(opts))
+          if (needReset >= opts.driver.tearDownIncremental)
           {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
@@ -342,7 +343,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
           }
         } else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
           allCommands.pop_back(); // fixme leaks cmds here
-          if (needReset >= options::getTearDownIncremental(opts))
+          if (needReset >= opts.driver.tearDownIncremental)
           {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
@@ -371,7 +372,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
           }
         } else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
                   dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
-          if (needReset >= options::getTearDownIncremental(opts))
+          if (needReset >= opts.driver.tearDownIncremental)
           {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
@@ -511,12 +512,12 @@ int runCvc5(int argc, char* argv[], Options& opts)
     pExecutor->flushOutputStreams();
 
 #ifdef CVC5_DEBUG
-    if (options::getEarlyExit(opts) && options::wasSetByUserEarlyExit(opts))
+    if (opts.driver.earlyExit && options::wasSetByUserEarlyExit(opts))
     {
       _exit(returnValue);
     }
 #else  /* CVC5_DEBUG */
-    if (options::getEarlyExit(opts))
+    if (opts.driver.earlyExit)
     {
       _exit(returnValue);
     }

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 9a05394900f926d17fe416e1e5b79505c0d998fc..048c101f08e5ffd78e4821f9c2cc694f3e5ec398 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -41,6 +41,7 @@
 #include "base/output.h"
 #include "expr/symbol_manager.h"
 #include "options/language.h"
+#include "options/main_options.h"
 #include "options/options.h"
 #include "options/options_public.h"
 #include "parser/input.h"
@@ -198,7 +199,7 @@ restart:
   if (d_usingEditline)
   {
 #if HAVE_LIBEDITLINE
-    lineBuf = ::readline(options::getInteractivePrompt(d_options)
+    lineBuf = ::readline(d_options.driver.interactivePrompt
                              ? (line == "" ? "cvc5> " : "... > ")
                              : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
@@ -210,7 +211,7 @@ restart:
   }
   else
   {
-    if (options::getInteractivePrompt(d_options))
+    if (d_options.driver.interactivePrompt)
     {
       if(line == "") {
         d_out << "cvc5> " << flush;
@@ -284,7 +285,7 @@ restart:
       if (d_usingEditline)
       {
 #if HAVE_LIBEDITLINE
-        lineBuf = ::readline(options::getInteractivePrompt(d_options) ? "... > "
+        lineBuf = ::readline(d_options.driver.interactivePrompt ? "... > "
                                                                       : "");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
@@ -295,7 +296,7 @@ restart:
       }
       else
       {
-        if (options::getInteractivePrompt(d_options))
+        if (d_options.driver.interactivePrompt)
         {
           d_out << "... > " << flush;
         }

diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index ccbf2e6aebb01f5d3257dc1d455d777b821bfdb4..0f5dfdcd71ce85f31ca043e3b658c8cd673d7710 100644 (file)
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -1,5 +1,6 @@
 id     = "DRIVER"
 name   = "Driver"
+public = true
 
 [[option]]
   name       = "version"

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index df0ef1a387a3f61fbbcef024d459e5bd21c7b2a9..73de9209bd38ccb56e66b2a6ddbf3ff12429cda0 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -49,7 +49,7 @@ import toml
 ### Allowed attributes for module/option
 
 MODULE_ATTR_REQ = ['id', 'name']
-MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option']
+MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option', 'public']
 
 OPTION_ATTR_REQ = ['category', 'type']
 OPTION_ATTR_ALL = OPTION_ATTR_REQ + [
@@ -615,10 +615,14 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
                     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"'
+
     filename = os.path.splitext(os.path.split(module.header)[1])[0]
     write_file(dst_dir, '{}.h'.format(filename), tpl_module_h.format(
-        filename=filename,
-        header=module.header,
+        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 72249094881c07e30f9273b70545439d8c0066fd..a74d3c49d493a560bd12a850e4d0b9aecda569cc 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.
  */
 
-#include "cvc5_private.h"
+${visibility_include}$
 
 #ifndef CVC5__OPTIONS__${id_cap}$_H
 #define CVC5__OPTIONS__${id_cap}$_H

diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp
index 778056553cd0e50338b9259a34270428c63cad51..f590ba0837029b87cab59ad203bd63276c55f8cd 100644 (file)
--- a/src/options/options_public.cpp
+++ b/src/options/options_public.cpp
@@ -61,7 +61,6 @@ bool getDumpUnsatCores(const Options& opts)
 {
   return opts.smt.dumpUnsatCores || opts.smt.dumpUnsatCoresFull;
 }
-bool getEarlyExit(const Options& opts) { return opts.driver.earlyExit; }
 bool getFilesystemAccess(const Options& opts)
 {
   return opts.parser.filesystemAccess;
@@ -70,21 +69,14 @@ bool getForceNoLimitCpuWhileDump(const Options& opts)
 {
   return opts.smt.forceNoLimitCpuWhileDump;
 }
-bool getHelp(const Options& opts) { return opts.driver.help; }
 bool getIncrementalSolving(const Options& opts)
 {
   return opts.smt.incrementalSolving;
 }
-bool getInteractive(const Options& opts) { return opts.driver.interactive; }
-bool getInteractivePrompt(const Options& opts)
-{
-  return opts.driver.interactivePrompt;
-}
 bool getLanguageHelp(const Options& opts) { return opts.base.languageHelp; }
 bool getMemoryMap(const Options& opts) { return opts.parser.memoryMap; }
 bool getParseOnly(const Options& opts) { return opts.base.parseOnly; }
 bool getProduceModels(const Options& opts) { return opts.smt.produceModels; }
-bool getSegvSpin(const Options& opts) { return opts.driver.segvSpin; }
 bool getSemanticChecks(const Options& opts)
 {
   return opts.parser.semanticChecks;
@@ -98,15 +90,10 @@ bool getStrictParsing(const Options& opts)
 {
   return opts.parser.strictParsing;
 }
-int32_t getTearDownIncremental(const Options& opts)
-{
-  return opts.driver.tearDownIncremental;
-}
 uint64_t getCumulativeTimeLimit(const Options& opts)
 {
   return opts.resman.cumulativeMillisecondLimit;
 }
-bool getVersion(const Options& opts) { return opts.driver.version; }
 const std::string& getForceLogicString(const Options& opts)
 {
   return opts.parser.forceLogicString;
@@ -125,10 +112,6 @@ void setInputLanguage(InputLanguage val, Options& opts)
 {
   opts.base.inputLanguage = val;
 }
-void setInteractive(bool val, Options& opts)
-{
-  opts.driver.interactive = val;
-}
 void setOut(std::ostream* val, Options& opts) { opts.base.out = val; }
 void setOutputLanguage(OutputLanguage val, Options& opts)
 {

diff --git a/src/options/options_public.h b/src/options/options_public.h
index a6d93cae785b60e92742dd1d00affbf2a07195f1..9b549601f7ea1839897757fcaa6bbf7eeced3756 100644 (file)
--- a/src/options/options_public.h
+++ b/src/options/options_public.h
@@ -37,25 +37,18 @@ bool getDumpInstantiations(const Options& opts) CVC5_EXPORT;
 bool getDumpModels(const Options& opts) CVC5_EXPORT;
 bool getDumpProofs(const Options& opts) CVC5_EXPORT;
 bool getDumpUnsatCores(const Options& opts) CVC5_EXPORT;
-bool getEarlyExit(const Options& opts) CVC5_EXPORT;
 bool getFilesystemAccess(const Options& opts) CVC5_EXPORT;
 bool getForceNoLimitCpuWhileDump(const Options& opts) CVC5_EXPORT;
-bool getHelp(const Options& opts) CVC5_EXPORT;
 bool getIncrementalSolving(const Options& opts) CVC5_EXPORT;
-bool getInteractive(const Options& opts) CVC5_EXPORT;
-bool getInteractivePrompt(const Options& opts) CVC5_EXPORT;
 bool getLanguageHelp(const Options& opts) CVC5_EXPORT;
 bool getMemoryMap(const Options& opts) CVC5_EXPORT;
 bool getParseOnly(const Options& opts) CVC5_EXPORT;
 bool getProduceModels(const Options& opts) CVC5_EXPORT;
-bool getSegvSpin(const Options& opts) CVC5_EXPORT;
 bool getSemanticChecks(const Options& opts) CVC5_EXPORT;
 bool getStatistics(const Options& opts) CVC5_EXPORT;
 bool getStatsEveryQuery(const Options& opts) CVC5_EXPORT;
 bool getStrictParsing(const Options& opts) CVC5_EXPORT;
-int32_t getTearDownIncremental(const Options& opts) CVC5_EXPORT;
 uint64_t getCumulativeTimeLimit(const Options& opts) CVC5_EXPORT;
-bool getVersion(const Options& opts) CVC5_EXPORT;
 const std::string& getForceLogicString(const Options& opts) CVC5_EXPORT;
 int32_t getVerbosity(const Options& opts) CVC5_EXPORT;
 
@@ -65,7 +58,6 @@ std::ostream* getOut(const Options& opts) CVC5_EXPORT;
 const std::string& getBinaryName(const Options& opts) CVC5_EXPORT;
 
 void setInputLanguage(InputLanguage val, Options& opts) CVC5_EXPORT;
-void setInteractive(bool val, Options& opts) CVC5_EXPORT;
 void setOut(std::ostream* val, Options& opts) CVC5_EXPORT;
 void setOutputLanguage(OutputLanguage val, Options& opts) CVC5_EXPORT;