Move public wrapper functions out of options class (#6600)

This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.

5 files changed, 236 insertions, 282 deletions

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 2107865c0..978c32888 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -30,7 +30,8 @@ libcvc5_add_sources(
   options_handler.cpp
   options_handler.h
   options_listener.h
-  options_public_functions.cpp
+  options_public.cpp
+  options_public.h
   printer_modes.cpp
   printer_modes.h
   set_language.cpp
diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp
new file mode 100644
index 000000000..778056553
--- /dev/null
+++ b/src/options/options_public.cpp
@@ -0,0 +1,155 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Gereon Kremer, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Definitions of public facing interface functions for Options.
+ *
+ * These are all one line wrappers for accessing the internal option data.
+ */
+
+#include "options_public.h"
+
+#include <fstream>
+#include <ostream>
+#include <string>
+#include <vector>
+
+#include "base/listener.h"
+#include "base/modal_exception.h"
+#include "options/base_options.h"
+#include "options/language.h"
+#include "options/main_options.h"
+#include "options/option_exception.h"
+#include "options/options.h"
+#include "options/parser_options.h"
+#include "options/printer_modes.h"
+#include "options/printer_options.h"
+#include "options/resource_manager_options.h"
+#include "options/smt_options.h"
+#include "options/uf_options.h"
+
+namespace cvc5::options {
+
+InputLanguage getInputLanguage(const Options& opts)
+{
+  return opts.base.inputLanguage;
+}
+InstFormatMode getInstFormatMode(const Options& opts)
+{
+  return opts.printer.instFormatMode;
+}
+OutputLanguage getOutputLanguage(const Options& opts)
+{
+  return opts.base.outputLanguage;
+}
+bool getUfHo(const Options& opts) { return opts.uf.ufHo; }
+bool getDumpInstantiations(const Options& opts)
+{
+  return opts.smt.dumpInstantiations;
+}
+bool getDumpModels(const Options& opts) { return opts.smt.dumpModels; }
+bool getDumpProofs(const Options& opts) { return opts.smt.dumpProofs; }
+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;
+}
+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;
+}
+bool getStatistics(const Options& opts) { return opts.base.statistics; }
+bool getStatsEveryQuery(const Options& opts)
+{
+  return opts.base.statisticsEveryQuery;
+}
+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;
+}
+int32_t getVerbosity(const Options& opts) { return opts.base.verbosity; }
+
+std::istream* getIn(const Options& opts) { return opts.base.in; }
+std::ostream* getErr(const Options& opts) { return opts.base.err; }
+std::ostream* getOut(const Options& opts) { return opts.base.out; }
+const std::string& getBinaryName(const Options& opts)
+{
+  return opts.base.binary_name;
+}
+
+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)
+{
+  opts.base.outputLanguage = val;
+}
+
+bool wasSetByUserEarlyExit(const Options& opts)
+{
+  return opts.driver.earlyExit__setByUser;
+}
+bool wasSetByUserForceLogicString(const Options& opts)
+{
+  return opts.parser.forceLogicString__setByUser;
+}
+bool wasSetByUserIncrementalSolving(const Options& opts)
+{
+  return opts.smt.incrementalSolving__setByUser;
+}
+bool wasSetByUserInteractive(const Options& opts)
+{
+  return opts.driver.interactive__setByUser;
+}
+
+}  // namespace cvc5::options
diff --git a/src/options/options_public.h b/src/options/options_public.h
new file mode 100644
index 000000000..a6d93cae7
--- /dev/null
+++ b/src/options/options_public.h
@@ -0,0 +1,79 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Public facing functions for options that need to be accessed from the
+ * outside.
+ *
+ * These are all one line wrappers for accessing the internal option data so
+ * that external code (including parser/ and main/) does not need to include
+ * the option modules (*_options.h).
+ */
+
+#include "cvc5_public.h"
+
+#ifndef CVC5__OPTIONS__OPTIONS_PUBLIC_H
+#define CVC5__OPTIONS__OPTIONS_PUBLIC_H
+
+#include "options/language.h"
+#include "options/options.h"
+#include "options/printer_modes.h"
+
+namespace cvc5::options {
+
+InputLanguage getInputLanguage(const Options& opts) CVC5_EXPORT;
+InstFormatMode getInstFormatMode(const Options& opts) CVC5_EXPORT;
+OutputLanguage getOutputLanguage(const Options& opts) CVC5_EXPORT;
+bool getUfHo(const Options& opts) CVC5_EXPORT;
+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;
+
+std::istream* getIn(const Options& opts) CVC5_EXPORT;
+std::ostream* getErr(const Options& opts) CVC5_EXPORT;
+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;
+
+bool wasSetByUserEarlyExit(const Options& opts) CVC5_EXPORT;
+bool wasSetByUserForceLogicString(const Options& opts) CVC5_EXPORT;
+bool wasSetByUserIncrementalSolving(const Options& opts) CVC5_EXPORT;
+bool wasSetByUserInteractive(const Options& opts) CVC5_EXPORT;
+
+}  // namespace cvc5::options
+
+#endif
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
deleted file mode 100644
index 2789b2d68..000000000
--- a/src/options/options_public_functions.cpp
+++ /dev/null
@@ -1,234 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Tim King, Gereon Kremer, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Definitions of public facing interface functions for Options.
- *
- * These are all 1 line wrappers for Options::get<T>, Options::set<T>, and
- * Options::wasSetByUser<T> for different option types T.
- */
-
-#include <fstream>
-#include <ostream>
-#include <string>
-#include <vector>
-
-#include "base/listener.h"
-#include "base/modal_exception.h"
-#include "options/options.h"
-#include "options/base_options.h"
-#include "options/language.h"
-#include "options/main_options.h"
-#include "options/option_exception.h"
-#include "options/parser_options.h"
-#include "options/printer_modes.h"
-#include "options/printer_options.h"
-#include "options/quantifiers_options.h"
-#include "options/resource_manager_options.h"
-#include "options/smt_options.h"
-#include "options/uf_options.h"
-
-namespace cvc5 {
-
-// Get accessor functions.
-InputLanguage Options::getInputLanguage() const {
-  return (*this)[options::inputLanguage];
-}
-
-options::InstFormatMode Options::getInstFormatMode() const
-{
-  return (*this)[options::instFormatMode];
-}
-
-OutputLanguage Options::getOutputLanguage() const {
-  return (*this)[options::outputLanguage];
-}
-
-bool Options::getUfHo() const { return (*this)[options::ufHo]; }
-
-bool Options::getDumpInstantiations() const{
-  return (*this)[options::dumpInstantiations];
-}
-
-bool Options::getDumpModels() const{
-  return (*this)[options::dumpModels];
-}
-
-bool Options::getDumpProofs() const{
-  return (*this)[options::dumpProofs];
-}
-
-bool Options::getDumpUnsatCores() const{
-  // dump unsat cores full enables dumpUnsatCores
-  return (*this)[options::dumpUnsatCores]
-         || (*this)[options::dumpUnsatCoresFull];
-}
-
-bool Options::getEarlyExit() const{
-  return (*this)[options::earlyExit];
-}
-
-bool Options::getFilesystemAccess() const{
-  return (*this)[options::filesystemAccess];
-}
-
-bool Options::getForceNoLimitCpuWhileDump() const{
-  return (*this)[options::forceNoLimitCpuWhileDump];
-}
-
-bool Options::getHelp() const{
-  return (*this)[options::help];
-}
-
-bool Options::getIncrementalSolving() const{
-  return (*this)[options::incrementalSolving];
-}
-
-bool Options::getInteractive() const{
-  return (*this)[options::interactive];
-}
-
-bool Options::getInteractivePrompt() const{
-  return (*this)[options::interactivePrompt];
-}
-
-bool Options::getLanguageHelp() const{
-  return (*this)[options::languageHelp];
-}
-
-bool Options::getMemoryMap() const{
-  return (*this)[options::memoryMap];
-}
-
-bool Options::getParseOnly() const{
-  return (*this)[options::parseOnly];
-}
-
-bool Options::getProduceModels() const{
-  return (*this)[options::produceModels];
-}
-
-bool Options::getSegvSpin() const{
-  return (*this)[options::segvSpin];
-}
-
-bool Options::getSemanticChecks() const{
-  return (*this)[options::semanticChecks];
-}
-
-bool Options::getStatistics() const{
-  // statsEveryQuery enables stats
-  return (*this)[options::statistics] || (*this)[options::statisticsEveryQuery];
-}
-
-bool Options::getStatsEveryQuery() const{
-  return (*this)[options::statisticsEveryQuery];
-}
-
-bool Options::getStrictParsing() const{
-  return (*this)[options::strictParsing];
-}
-
-int Options::getTearDownIncremental() const{
-  return (*this)[options::tearDownIncremental];
-}
-
-uint64_t Options::getCumulativeTimeLimit() const
-{
-  return (*this)[options::cumulativeMillisecondLimit];
-}
-
-bool Options::getVersion() const{
-  return (*this)[options::version];
-}
-
-const std::string& Options::getForceLogicString() const{
-  return (*this)[options::forceLogicString];
-}
-
-int Options::getVerbosity() const{
-  return (*this)[options::verbosity];
-}
-
-std::istream* Options::getIn() const{
-  return (*this)[options::in];
-}
-
-std::ostream* Options::getErr(){
-  return (*this)[options::err];
-}
-
-std::ostream* Options::getOut(){
-  return (*this)[options::out];
-}
-
-std::ostream* Options::getOutConst() const{
-  // #warning "Remove Options::getOutConst"
-  return (*this)[options::out];
-}
-
-std::string Options::getBinaryName() const{
-  return (*this)[options::binary_name];
-}
-
-std::ostream* Options::currentGetOut() {
-  return current().getOut();
-}
-
-
-// TODO: Document these.
-
-void Options::setInputLanguage(InputLanguage value) {
-  base.inputLanguage = value;
-}
-
-void Options::setInteractive(bool value) {
-  driver.interactive = value;
-}
-
-void Options::setOut(std::ostream* value) {
-  base.out = value;
-}
-
-void Options::setOutputLanguage(OutputLanguage value) {
-  base.outputLanguage = value;
-}
-
-bool Options::wasSetByUserEarlyExit() const {
-  return wasSetByUser(options::earlyExit);
-}
-
-bool Options::wasSetByUserForceLogicString() const {
-  return wasSetByUser(options::forceLogicString);
-}
-
-bool Options::wasSetByUserIncrementalSolving() const {
-  return wasSetByUser(options::incrementalSolving);
-}
-
-bool Options::wasSetByUserInteractive() const {
-  return wasSetByUser(options::interactive);
-}
-
-
-void Options::flushErr() {
-  if(getErr() != NULL) {
-    *(getErr()) << std::flush;
-  }
-}
-
-void Options::flushOut() {
-  if(getOut() != NULL) {
-    *(getOut()) << std::flush;
-  }
-}
-
-}  // namespace cvc5
diff --git a/src/options/options_template.h b/src/options/options_template.h
index 346096169..6e28aad85 100644
--- a/src/options/options_template.h
+++ b/src/options/options_template.h
@@ -136,53 +136,6 @@ public:
    */
   std::string getOption(const std::string& key) const;
 
-  // Get accessor functions.
-  InputLanguage getInputLanguage() const;
-  options::InstFormatMode getInstFormatMode() const;
-  OutputLanguage getOutputLanguage() const;
-  bool getUfHo() const;
-  bool getDumpInstantiations() const;
-  bool getDumpModels() const;
-  bool getDumpProofs() const;
-  bool getDumpUnsatCores() const;
-  bool getEarlyExit() const;
-  bool getFilesystemAccess() const;
-  bool getForceNoLimitCpuWhileDump() const;
-  bool getHelp() const;
-  bool getIncrementalSolving() const;
-  bool getInteractive() const;
-  bool getInteractivePrompt() const;
-  bool getLanguageHelp() const;
-  bool getMemoryMap() const;
-  bool getParseOnly() const;
-  bool getProduceModels() const;
-  bool getSegvSpin() const;
-  bool getSemanticChecks() const;
-  bool getStatistics() const;
-  bool getStatsEveryQuery() const;
-  bool getStrictParsing() const;
-  int getTearDownIncremental() const;
-  uint64_t getCumulativeTimeLimit() const;
-  bool getVersion() const;
-  const std::string& getForceLogicString() const;
-  int getVerbosity() const;
-  std::istream* getIn() const;
-  std::ostream* getErr();
-  std::ostream* getOut();
-  std::ostream* getOutConst() const; // TODO: Remove this.
-  std::string getBinaryName() const;
-
-  // TODO: Document these.
-  void setInputLanguage(InputLanguage);
-  void setInteractive(bool);
-  void setOut(std::ostream*);
-  void setOutputLanguage(OutputLanguage);
-
-  bool wasSetByUserEarlyExit() const;
-  bool wasSetByUserForceLogicString() const;
-  bool wasSetByUserIncrementalSolving() const;
-  bool wasSetByUserInteractive() const;
-
   // Static accessor functions.
   // TODO: Document these.
   static std::ostream* currentGetOut();