cmake: Generate cvc4_export.h and set visibility to hidden. (#6139)

The build system (cmake) will automatically generate an export header
cvc4_export.h, which makes sure that the correct export features are
defined depending on the compiler and target platform. The macro CVC4_EXPORT
replaces CVC4_PUBLIC and its usage is reduced by 2/3.

Co-authored-by: Gereon Kremer <nafur42@gmail.com>

6 files changed, 45 insertions, 35 deletions

diff --git a/src/options/language.h b/src/options/language.h
index 9626b3aa2..a8b42fec1 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -22,12 +22,14 @@
 #include <ostream>
 #include <string>
 
+#include "cvc4_export.h"
+
 namespace CVC4 {
 namespace language {
 
 namespace input {
 
-enum CVC4_PUBLIC Language
+enum CVC4_EXPORT Language
 {
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
@@ -59,7 +61,7 @@ enum CVC4_PUBLIC Language
   LANG_MAX
 }; /* enum Language */
 
-inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_EXPORT;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
   switch(lang) {
   case LANG_AUTO:
@@ -85,7 +87,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
 
 namespace output {
 
-enum CVC4_PUBLIC Language
+enum CVC4_EXPORT Language
 {
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
@@ -122,7 +124,7 @@ enum CVC4_PUBLIC Language
   LANG_MAX
 }; /* enum Language */
 
-inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_EXPORT;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
   switch(lang) {
   case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break;
@@ -155,24 +157,24 @@ typedef language::output::Language OutputLanguage;
 namespace language {
 
 /** Is the language a variant of the smtlib version 2 language? */
-bool isInputLang_smt2(InputLanguage lang) CVC4_PUBLIC;
-bool isOutputLang_smt2(OutputLanguage lang) CVC4_PUBLIC;
+bool isInputLang_smt2(InputLanguage lang) CVC4_EXPORT;
+bool isOutputLang_smt2(OutputLanguage lang) CVC4_EXPORT;
 
 /**
   * Is the language smtlib 2.6 or above? If exact=true, then this method returns
   * false if the input language is not exactly SMT-LIB 2.6.
   */
-bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
-bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
+bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_EXPORT;
+bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_EXPORT;
 
 /** Is the language a variant of the SyGuS input language? */
-bool isInputLangSygus(InputLanguage lang) CVC4_PUBLIC;
-bool isOutputLangSygus(OutputLanguage lang) CVC4_PUBLIC;
+bool isInputLangSygus(InputLanguage lang) CVC4_EXPORT;
+bool isOutputLangSygus(OutputLanguage lang) CVC4_EXPORT;
 
-InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC;
-OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC;
-InputLanguage toInputLanguage(std::string language) CVC4_PUBLIC;
-OutputLanguage toOutputLanguage(std::string language) CVC4_PUBLIC;
+InputLanguage toInputLanguage(OutputLanguage language) CVC4_EXPORT;
+OutputLanguage toOutputLanguage(InputLanguage language) CVC4_EXPORT;
+InputLanguage toInputLanguage(std::string language) CVC4_EXPORT;
+OutputLanguage toOutputLanguage(std::string language) CVC4_EXPORT;
 
 }/* CVC4::language namespace */
 }/* CVC4 namespace */
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index f13cf3fc6..4dc8880b1 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -168,23 +168,23 @@ TPL_HOLDER_MACRO_ATTR += "  bool {name}__setByUser__;"
 
 
 TPL_OPTION_STRUCT_RW = \
-"""extern struct CVC4_PUBLIC {name}__option_t
+"""extern struct {name}__option_t
 {{
   typedef {type} type;
   type operator()() const;
   bool wasSetByUser() const;
   void set(const type& v);
   const char* getName() const;
-}} thread_local {name} CVC4_PUBLIC;"""
+}} thread_local {name};"""
 
 TPL_OPTION_STRUCT_RO = \
-"""extern struct CVC4_PUBLIC {name}__option_t
+"""extern struct {name}__option_t
 {{
   typedef {type} type;
   type operator()() const;
   bool wasSetByUser() const;
   const char* getName() const;
-}} thread_local {name} CVC4_PUBLIC;"""
+}} thread_local {name};"""
 
 
 TPL_DECL_SET = \
@@ -258,9 +258,9 @@ enum class {type}
 TPL_DECL_MODE_FUNC = \
 """
 std::ostream&
-operator<<(std::ostream& os, {type} mode) CVC4_PUBLIC;"""
+operator<<(std::ostream& os, {type} mode);"""
 
-TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(" CVC4_PUBLIC;")] + \
+TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(";")] + \
 """
 {{
   os << "{type}::";
diff --git a/src/options/option_exception.h b/src/options/option_exception.h
index 84bde3ce5..11d6b8fd3 100644
--- a/src/options/option_exception.h
+++ b/src/options/option_exception.h
@@ -20,6 +20,7 @@
 #define CVC4__OPTION_EXCEPTION_H
 
 #include "base/exception.h"
+#include "cvc4_export.h"
 
 namespace CVC4 {
 
@@ -29,7 +30,8 @@ namespace CVC4 {
  * name is itself unrecognized, a UnrecognizedOptionException (a derived
  * class, below) should be used instead.
  */
-class CVC4_PUBLIC OptionException : public CVC4::Exception {
+class CVC4_EXPORT OptionException : public CVC4::Exception
+{
  public:
   OptionException(const std::string& s) : CVC4::Exception(s_errPrefix + s) {}
 
@@ -45,13 +47,14 @@ class CVC4_PUBLIC OptionException : public CVC4::Exception {
  private:
   /** The string to be added in front of the actual error message */
   static const std::string s_errPrefix;
-};/* class OptionException */
+}; /* class OptionException */
 
 /**
  * Class representing an exception in option processing due to an
  * unrecognized or unsupported option key.
  */
-class CVC4_PUBLIC UnrecognizedOptionException : public CVC4::OptionException {
+class UnrecognizedOptionException : public CVC4::OptionException
+{
  public:
   UnrecognizedOptionException() :
     CVC4::OptionException("Unrecognized informational or option key or setting") {
@@ -60,7 +63,7 @@ class CVC4_PUBLIC UnrecognizedOptionException : public CVC4::OptionException {
   UnrecognizedOptionException(const std::string& msg) :
     CVC4::OptionException("Unrecognized informational or option key or setting: " + msg) {
   }
-};/* class UnrecognizedOptionException */
+}; /* class UnrecognizedOptionException */
 
 }/* CVC4 namespace */
 
diff --git a/src/options/options.h b/src/options/options.h
index df94be9d9..728e5c7c8 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -26,6 +26,7 @@
 
 #include "base/listener.h"
 #include "base/modal_exception.h"
+#include "cvc4_export.h"
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/printer_modes.h"
@@ -42,7 +43,8 @@ namespace options {
 
 class OptionsListener;
 
-class CVC4_PUBLIC Options {
+class CVC4_EXPORT Options
+{
   friend api::Solver;
   /** The struct that holds all option values. */
   options::OptionsHolder* d_holder;
@@ -80,7 +82,8 @@ class CVC4_PUBLIC Options {
   static const unsigned s_preemptAdditional = 6;
 
 public:
-  class CVC4_PUBLIC OptionsScope {
+ class OptionsScope
+ {
   private:
     Options* d_oldOptions;
   public:
@@ -92,7 +95,7 @@ public:
     ~OptionsScope(){
       Options::s_current = d_oldOptions;
     }
-  };
+ };
 
   /** Return true if current Options are null */
   static inline bool isCurrentNull() {
@@ -301,7 +304,7 @@ public:
                                     int argc,
                                     char* argv[],
                                     std::vector<std::string>* nonoptions);
-};/* class Options */
+}; /* class Options */
 
 }/* CVC4 namespace */
 
diff --git a/src/options/printer_modes.h b/src/options/printer_modes.h
index 09395dd5e..d4cdbd9a4 100644
--- a/src/options/printer_modes.h
+++ b/src/options/printer_modes.h
@@ -27,7 +27,7 @@ namespace options {
 
 /** Enumeration of inst_format modes (how to print models from get-model
  * command). */
-enum class CVC4_PUBLIC InstFormatMode
+enum class InstFormatMode
 {
   /** default mode (print expressions in the output language format) */
   DEFAULT,
@@ -37,8 +37,7 @@ enum class CVC4_PUBLIC InstFormatMode
 
 }  // namespace options
 
-std::ostream& operator<<(std::ostream& out,
-                         options::InstFormatMode mode) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, options::InstFormatMode mode);
 
 }  // namespace CVC4
 
diff --git a/src/options/set_language.h b/src/options/set_language.h
index c41351250..b94bdf1d8 100644
--- a/src/options/set_language.h
+++ b/src/options/set_language.h
@@ -20,6 +20,8 @@
 #define CVC4__OPTIONS__SET_LANGUAGE_H
 
 #include <iostream>
+
+#include "cvc4_export.h"
 #include "options/language.h"
 
 namespace CVC4 {
@@ -28,8 +30,9 @@ namespace language {
 /**
  * IOStream manipulator to set the output language for Exprs.
  */
-class CVC4_PUBLIC SetLanguage {
-public:
+class CVC4_EXPORT SetLanguage
+{
+ public:
   /**
    * Set a language on the output stream for the current stack scope.
    * This makes sure the old language is reset on the stream after
@@ -74,7 +77,7 @@ private:
    * When this manipulator is used, the setting is stored here.
    */
   OutputLanguage d_language;
-};/* class SetLanguage */
+}; /* class SetLanguage */
 
 /**
  * Sets the output language when pretty-printing a Expr to an ostream.
@@ -85,7 +88,7 @@ private:
  *
  * The setting stays permanently (until set again) with the stream.
  */
-std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_EXPORT;
 
 }/* CVC4::language namespace */
 }/* CVC4 namespace */