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>

5 files changed, 10 insertions, 8 deletions

diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h
index 3021c5a53..e8610e7db 100644
--- a/src/theory/bags/make_bag_op.h
+++ b/src/theory/bags/make_bag_op.h
@@ -52,7 +52,7 @@ std::ostream& operator<<(std::ostream& out, const MakeBagOp& op);
 /**
  * Hash function for the MakeBagOpHashFunction objects.
  */
-struct CVC4_PUBLIC MakeBagOpHashFunction
+struct MakeBagOpHashFunction
 {
   size_t operator()(const MakeBagOp& op) const;
 }; /* struct MakeBagOpHashFunction */
diff --git a/src/theory/datatypes/tuple_project_op.h b/src/theory/datatypes/tuple_project_op.h
index 045f05cc2..361cf4f60 100644
--- a/src/theory/datatypes/tuple_project_op.h
+++ b/src/theory/datatypes/tuple_project_op.h
@@ -48,7 +48,7 @@ std::ostream& operator<<(std::ostream& out, const TupleProjectOp& op);
 /**
  * Hash function for the TupleProjectOpHashFunction objects.
  */
-struct CVC4_PUBLIC TupleProjectOpHashFunction
+struct TupleProjectOpHashFunction
 {
   size_t operator()(const TupleProjectOp& op) const;
 }; /* struct TupleProjectOpHashFunction */
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index fe6d1cf62..72913a0c2 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -24,6 +24,7 @@
 #include <string>
 #include <vector>
 
+#include "cvc4_export.h"
 #include "theory/theory_id.h"
 
 namespace CVC4 {
@@ -43,7 +44,8 @@ namespace CVC4 {
  * (e.g., for communicating to the SmtEngine which theories should be used,
  * rather than having to provide an SMT-LIB string).
  */
-class CVC4_PUBLIC LogicInfo {
+class CVC4_EXPORT LogicInfo
+{
   mutable std::string d_logicString; /**< an SMT-LIB-like logic string */
   std::vector<bool> d_theories; /**< set of active theories */
   size_t d_sharingTheories; /**< count of theories that need sharing */
@@ -285,9 +287,9 @@ public:
     return *this <= other || *this >= other;
   }
 
-};/* class LogicInfo */
+}; /* class LogicInfo */
 
-std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const LogicInfo& logic);
 
 }/* CVC4 namespace */
 
diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h
index fd70598da..7d7bb85b6 100644
--- a/src/theory/sets/singleton_op.h
+++ b/src/theory/sets/singleton_op.h
@@ -53,7 +53,7 @@ std::ostream& operator<<(std::ostream& out, const SingletonOp& op);
 /**
  * Hash function for the SingletonHashFunction objects.
  */
-struct CVC4_PUBLIC SingletonOpHashFunction
+struct SingletonOpHashFunction
 {
   size_t operator()(const SingletonOp& op) const;
 }; /* struct SingletonOpHashFunction */
diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h
index 1833f1cac..cca3bf2d6 100644
--- a/src/theory/theory_id.h
+++ b/src/theory/theory_id.h
@@ -52,11 +52,11 @@ enum TheoryId
 const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
 const TheoryId THEORY_SAT_SOLVER = THEORY_LAST;
 
-TheoryId& operator++(TheoryId& id) CVC4_PUBLIC;
+TheoryId& operator++(TheoryId& id);
 
 std::ostream& operator<<(std::ostream& out, TheoryId theoryId);
 
-std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC;
+std::string getStatsPrefix(TheoryId theoryId);
 
 /**
  * A set of theories. Utilities for TheoryIdSet can be found below.