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>

28 files changed, 199 insertions, 181 deletions

diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h
index 44f2277fe..5d28d355a 100644
--- a/src/util/abstract_value.h
+++ b/src/util/abstract_value.h
@@ -24,7 +24,8 @@
 
 namespace CVC4 {
 
-class CVC4_PUBLIC AbstractValue {
+class AbstractValue
+{
   const Integer d_index;
 
  public:
@@ -46,17 +47,18 @@ class CVC4_PUBLIC AbstractValue {
   }
   bool operator>(const AbstractValue& val) const { return !(*this <= val); }
   bool operator>=(const AbstractValue& val) const { return !(*this < val); }
-};/* class AbstractValue */
+}; /* class AbstractValue */
 
-std::ostream& operator<<(std::ostream& out, const AbstractValue& val) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const AbstractValue& val);
 
 /**
  * Hash function for the BitVector constants.
  */
-struct CVC4_PUBLIC AbstractValueHashFunction {
+struct AbstractValueHashFunction
+{
   inline size_t operator()(const AbstractValue& val) const {
     return IntegerHashFunction()(val.getIndex());
   }
-};/* struct AbstractValueHashFunction */
+}; /* struct AbstractValueHashFunction */
 
 }/* CVC4 namespace */
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 5da7667b0..ab6d8b030 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -27,7 +27,7 @@
 
 namespace CVC4 {
 
-class CVC4_PUBLIC BitVector
+class BitVector
 {
  public:
   BitVector(unsigned size, const Integer& val)
@@ -282,7 +282,7 @@ class CVC4_PUBLIC BitVector
  * operation maps bit-vectors to bit-vector of size <code>high - low + 1</code>
  * by taking the bits at indices <code>high ... low</code>
  */
-struct CVC4_PUBLIC BitVectorExtract
+struct BitVectorExtract
 {
   /** The high bit of the range for this extract */
   unsigned d_high;
@@ -300,7 +300,7 @@ struct CVC4_PUBLIC BitVectorExtract
 /**
  * The structure representing the extraction of one Boolean bit.
  */
-struct CVC4_PUBLIC BitVectorBitOf
+struct BitVectorBitOf
 {
   /** The index of the bit */
   unsigned d_bitIndex;
@@ -312,21 +312,21 @@ struct CVC4_PUBLIC BitVectorBitOf
   }
 }; /* struct BitVectorBitOf */
 
-struct CVC4_PUBLIC BitVectorSize
+struct BitVectorSize
 {
   unsigned d_size;
   BitVectorSize(unsigned size) : d_size(size) {}
   operator unsigned() const { return d_size; }
 }; /* struct BitVectorSize */
 
-struct CVC4_PUBLIC BitVectorRepeat
+struct BitVectorRepeat
 {
   unsigned d_repeatAmount;
   BitVectorRepeat(unsigned repeatAmount) : d_repeatAmount(repeatAmount) {}
   operator unsigned() const { return d_repeatAmount; }
 }; /* struct BitVectorRepeat */
 
-struct CVC4_PUBLIC BitVectorZeroExtend
+struct BitVectorZeroExtend
 {
   unsigned d_zeroExtendAmount;
   BitVectorZeroExtend(unsigned zeroExtendAmount)
@@ -336,7 +336,7 @@ struct CVC4_PUBLIC BitVectorZeroExtend
   operator unsigned() const { return d_zeroExtendAmount; }
 }; /* struct BitVectorZeroExtend */
 
-struct CVC4_PUBLIC BitVectorSignExtend
+struct BitVectorSignExtend
 {
   unsigned d_signExtendAmount;
   BitVectorSignExtend(unsigned signExtendAmount)
@@ -346,7 +346,7 @@ struct CVC4_PUBLIC BitVectorSignExtend
   operator unsigned() const { return d_signExtendAmount; }
 }; /* struct BitVectorSignExtend */
 
-struct CVC4_PUBLIC BitVectorRotateLeft
+struct BitVectorRotateLeft
 {
   unsigned d_rotateLeftAmount;
   BitVectorRotateLeft(unsigned rotateLeftAmount)
@@ -356,7 +356,7 @@ struct CVC4_PUBLIC BitVectorRotateLeft
   operator unsigned() const { return d_rotateLeftAmount; }
 }; /* struct BitVectorRotateLeft */
 
-struct CVC4_PUBLIC BitVectorRotateRight
+struct BitVectorRotateRight
 {
   unsigned d_rotateRightAmount;
   BitVectorRotateRight(unsigned rotateRightAmount)
@@ -366,7 +366,7 @@ struct CVC4_PUBLIC BitVectorRotateRight
   operator unsigned() const { return d_rotateRightAmount; }
 }; /* struct BitVectorRotateRight */
 
-struct CVC4_PUBLIC IntToBitVector
+struct IntToBitVector
 {
   unsigned d_size;
   IntToBitVector(unsigned size) : d_size(size) {}
@@ -380,7 +380,7 @@ struct CVC4_PUBLIC IntToBitVector
 /*
  * Hash function for the BitVector constants.
  */
-struct CVC4_PUBLIC BitVectorHashFunction
+struct BitVectorHashFunction
 {
   inline size_t operator()(const BitVector& bv) const { return bv.hash(); }
 }; /* struct BitVectorHashFunction */
@@ -388,7 +388,7 @@ struct CVC4_PUBLIC BitVectorHashFunction
 /**
  * Hash function for the BitVectorExtract objects.
  */
-struct CVC4_PUBLIC BitVectorExtractHashFunction
+struct BitVectorExtractHashFunction
 {
   size_t operator()(const BitVectorExtract& extract) const
   {
@@ -401,13 +401,13 @@ struct CVC4_PUBLIC BitVectorExtractHashFunction
 /**
  * Hash function for the BitVectorBitOf objects.
  */
-struct CVC4_PUBLIC BitVectorBitOfHashFunction
+struct BitVectorBitOfHashFunction
 {
   size_t operator()(const BitVectorBitOf& b) const { return b.d_bitIndex; }
 }; /* struct BitVectorBitOfHashFunction */
 
 template <typename T>
-struct CVC4_PUBLIC UnsignedHashFunction
+struct UnsignedHashFunction
 {
   inline size_t operator()(const T& x) const { return (size_t)x; }
 }; /* struct UnsignedHashFunction */
@@ -416,29 +416,25 @@ struct CVC4_PUBLIC UnsignedHashFunction
  ** Output stream
  * ----------------------------------------------------------------------- */
 
-inline std::ostream& operator<<(std::ostream& os,
-                                const BitVector& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const BitVector& bv);
 inline std::ostream& operator<<(std::ostream& os, const BitVector& bv)
 {
   return os << bv.toString();
 }
 
-inline std::ostream& operator<<(std::ostream& os,
-                                const BitVectorExtract& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv);
 inline std::ostream& operator<<(std::ostream& os, const BitVectorExtract& bv)
 {
   return os << "[" << bv.d_high << ":" << bv.d_low << "]";
 }
 
-inline std::ostream& operator<<(std::ostream& os,
-                                const BitVectorBitOf& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv);
 inline std::ostream& operator<<(std::ostream& os, const BitVectorBitOf& bv)
 {
   return os << "[" << bv.d_bitIndex << "]";
 }
 
-inline std::ostream& operator<<(std::ostream& os,
-                                const IntToBitVector& bv) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv);
 inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv)
 {
   return os << "[" << bv.d_size << "]";
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 5f7d70406..6c48b44a8 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -30,7 +30,8 @@ namespace CVC4 {
  * Representation for a Beth number, used only to construct
  * Cardinality objects.
  */
-class CVC4_PUBLIC CardinalityBeth {
+class CardinalityBeth
+{
   Integer d_index;
 
  public:
@@ -43,7 +44,8 @@ class CVC4_PUBLIC CardinalityBeth {
 /**
  * Representation for an unknown cardinality.
  */
-class CVC4_PUBLIC CardinalityUnknown {
+class CardinalityUnknown
+{
  public:
   CardinalityUnknown() {}
   ~CardinalityUnknown() {}
@@ -54,7 +56,8 @@ class CVC4_PUBLIC CardinalityUnknown {
  * arbitrary-precision integer for finite cardinalities, and we
  * distinguish infinite cardinalities represented as Beth numbers.
  */
-class CVC4_PUBLIC Cardinality {
+class Cardinality
+{
   /** Cardinality of the integers */
   static const Integer s_intCard;
 
@@ -90,7 +93,8 @@ class CVC4_PUBLIC Cardinality {
   static const Cardinality UNKNOWN_CARD;
 
   /** Used as a result code for Cardinality::compare(). */
-  enum CVC4_PUBLIC CardinalityComparison {
+  enum CardinalityComparison
+  {
     LESS,
     EQUAL,
     GREATER,
@@ -216,10 +220,10 @@ class CVC4_PUBLIC Cardinality {
 }; /* class Cardinality */
 
 /** Print an element of the InfiniteCardinality enumeration. */
-std::ostream& operator<<(std::ostream& out, CardinalityBeth b) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, CardinalityBeth b);
 
 /** Print a cardinality in a human-readable fashion. */
-std::ostream& operator<<(std::ostream& out, const Cardinality& c) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const Cardinality& c);
 
 } /* CVC4 namespace */
 
diff --git a/src/util/divisible.h b/src/util/divisible.h
index 3d7a2e937..2de81c52b 100644
--- a/src/util/divisible.h
+++ b/src/util/divisible.h
@@ -31,7 +31,8 @@ namespace CVC4 {
 /**
  * The structure representing the divisibility-by-k predicate.
  */
-struct CVC4_PUBLIC Divisible {
+struct Divisible
+{
   const Integer k;
 
   Divisible(const Integer& n);
@@ -43,18 +44,19 @@ struct CVC4_PUBLIC Divisible {
   bool operator!=(const Divisible& d) const {
     return !(*this == d);
   }
-};/* struct Divisible */
+}; /* struct Divisible */
 
 /**
  * Hash function for the Divisible objects.
  */
-struct CVC4_PUBLIC DivisibleHashFunction {
+struct DivisibleHashFunction
+{
   size_t operator()(const Divisible& d) const {
     return d.k.hash();
   }
-};/* struct DivisibleHashFunction */
+}; /* struct DivisibleHashFunction */
 
-inline std::ostream& operator <<(std::ostream& os, const Divisible& d) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const Divisible& d);
 inline std::ostream& operator <<(std::ostream& os, const Divisible& d) {
   return os << "divisible-by-" << d.k;
 }
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index 10d1352a4..758d51bc5 100644
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -35,7 +35,7 @@ namespace CVC4 {
 
 class FloatingPointLiteral;
 
-class CVC4_PUBLIC FloatingPoint
+class FloatingPoint
 {
  public:
   /**
@@ -274,7 +274,7 @@ class CVC4_PUBLIC FloatingPoint
 /**
  * Hash function for floating-point values.
  */
-struct CVC4_PUBLIC FloatingPointHashFunction
+struct FloatingPointHashFunction
 {
   size_t operator()(const FloatingPoint& fp) const
   {
@@ -290,7 +290,7 @@ struct CVC4_PUBLIC FloatingPointHashFunction
 /**
  * The parameter type for the conversions to floating point.
  */
-class CVC4_PUBLIC FloatingPointConvertSort
+class FloatingPointConvertSort
 {
  public:
   /** Constructors. */
@@ -309,7 +309,7 @@ class CVC4_PUBLIC FloatingPointConvertSort
 
 /** Hash function for conversion sorts. */
 template <uint32_t key>
-struct CVC4_PUBLIC FloatingPointConvertSortHashFunction
+struct FloatingPointConvertSortHashFunction
 {
   inline size_t operator()(const FloatingPointConvertSort& fpcs) const
   {
@@ -328,8 +328,7 @@ struct CVC4_PUBLIC FloatingPointConvertSortHashFunction
  * sign, the following exponent width bits the exponent, and the remaining bits
  * the significand).
  */
-class CVC4_PUBLIC FloatingPointToFPIEEEBitVector
-    : public FloatingPointConvertSort
+class FloatingPointToFPIEEEBitVector : public FloatingPointConvertSort
 {
  public:
   /** Constructors. */
@@ -347,8 +346,7 @@ class CVC4_PUBLIC FloatingPointToFPIEEEBitVector
  * Conversion from floating-point to another floating-point (of possibly
  * different size).
  */
-class CVC4_PUBLIC FloatingPointToFPFloatingPoint
-    : public FloatingPointConvertSort
+class FloatingPointToFPFloatingPoint : public FloatingPointConvertSort
 {
  public:
   /** Constructors. */
@@ -365,7 +363,7 @@ class CVC4_PUBLIC FloatingPointToFPFloatingPoint
 /**
  * Conversion from floating-point to Real.
  */
-class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort
+class FloatingPointToFPReal : public FloatingPointConvertSort
 {
  public:
   /** Constructors. */
@@ -382,8 +380,7 @@ class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort
 /**
  * Conversion from floating-point to signed bit-vector value.
  */
-class CVC4_PUBLIC FloatingPointToFPSignedBitVector
-    : public FloatingPointConvertSort
+class FloatingPointToFPSignedBitVector : public FloatingPointConvertSort
 {
  public:
   /** Constructors. */
@@ -400,8 +397,7 @@ class CVC4_PUBLIC FloatingPointToFPSignedBitVector
 /**
  * Conversion from floating-point to unsigned bit-vector value.
  */
-class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector
-    : public FloatingPointConvertSort
+class FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort
 {
  public:
   /** Constructors. */
@@ -415,7 +411,7 @@ class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector
   }
 };
 
-class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort
+class FloatingPointToFPGeneric : public FloatingPointConvertSort
 {
  public:
   /** Constructors. */
@@ -432,7 +428,7 @@ class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort
 /**
  * Base type for floating-point to bit-vector conversion.
  */
-class CVC4_PUBLIC FloatingPointToBV
+class FloatingPointToBV
 {
  public:
   /** Constructors. */
@@ -450,7 +446,7 @@ class CVC4_PUBLIC FloatingPointToBV
 /**
  * Conversion from floating-point to unsigned bit-vector value.
  */
-class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV
+class FloatingPointToUBV : public FloatingPointToBV
 {
  public:
   FloatingPointToUBV(uint32_t _s) : FloatingPointToBV(_s) {}
@@ -460,7 +456,7 @@ class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV
 /**
  * Conversion from floating-point to signed bit-vector value.
  */
-class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV
+class FloatingPointToSBV : public FloatingPointToBV
 {
  public:
   FloatingPointToSBV(uint32_t _s) : FloatingPointToBV(_s) {}
@@ -470,7 +466,7 @@ class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV
 /**
  * Conversion from floating-point to unsigned bit-vector value (total version).
  */
-class CVC4_PUBLIC FloatingPointToUBVTotal : public FloatingPointToBV
+class FloatingPointToUBVTotal : public FloatingPointToBV
 {
  public:
   FloatingPointToUBVTotal(uint32_t _s) : FloatingPointToBV(_s) {}
@@ -482,7 +478,7 @@ class CVC4_PUBLIC FloatingPointToUBVTotal : public FloatingPointToBV
 /**
  * Conversion from floating-point to signed bit-vector value (total version).
  */
-class CVC4_PUBLIC FloatingPointToSBVTotal : public FloatingPointToBV
+class FloatingPointToSBVTotal : public FloatingPointToBV
 {
  public:
   FloatingPointToSBVTotal(uint32_t _s) : FloatingPointToBV(_s) {}
@@ -495,7 +491,7 @@ class CVC4_PUBLIC FloatingPointToSBVTotal : public FloatingPointToBV
  * Hash function for floating-point to bit-vector conversions.
  */
 template <uint32_t key>
-struct CVC4_PUBLIC FloatingPointToBVHashFunction
+struct FloatingPointToBVHashFunction
 {
   inline size_t operator()(const FloatingPointToBV& fptbv) const
   {
@@ -509,15 +505,14 @@ struct CVC4_PUBLIC FloatingPointToBVHashFunction
  * FloatingPointLiteral in a sensible way. Use FloatingPoint instead. */
 
 /** Output stream operator overloading for floating-point values. */
-std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& os, const FloatingPoint& fp);
 
 /** Output stream operator overloading for floating-point formats. */
-std::ostream& operator<<(std::ostream& os,
-                         const FloatingPointSize& fps) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps);
 
 /** Output stream operator overloading for floating-point conversion sorts. */
 std::ostream& operator<<(std::ostream& os,
-                         const FloatingPointConvertSort& fpcs) CVC4_PUBLIC;
+                         const FloatingPointConvertSort& fpcs);
 
 }  // namespace CVC4
 
diff --git a/src/util/floatingpoint_size.h b/src/util/floatingpoint_size.h
index d241ef93e..be00e0987 100644
--- a/src/util/floatingpoint_size.h
+++ b/src/util/floatingpoint_size.h
@@ -19,15 +19,15 @@
 namespace CVC4 {
 
 // Inline these!
-inline bool CVC4_PUBLIC validExponentSize(uint32_t e) { return e >= 2; }
-inline bool CVC4_PUBLIC validSignificandSize(uint32_t s) { return s >= 2; }
+inline bool validExponentSize(uint32_t e) { return e >= 2; }
+inline bool validSignificandSize(uint32_t s) { return s >= 2; }
 
 /**
  * Floating point sorts are parameterised by two constants > 1 giving the
  * width (in bits) of the exponent and significand (including the hidden bit).
  * So, IEEE-754 single precision, a.k.a. float, is described as 8 24.
  */
-class CVC4_PUBLIC FloatingPointSize
+class FloatingPointSize
 {
  public:
   /** Constructors. */
@@ -79,7 +79,7 @@ class CVC4_PUBLIC FloatingPointSize
 /**
  * Hash function for floating point formats.
  */
-struct CVC4_PUBLIC FloatingPointSizeHashFunction
+struct FloatingPointSizeHashFunction
 {
   static inline size_t ROLL(size_t X, size_t N)
   {
diff --git a/src/util/iand.h b/src/util/iand.h
index 064867169..e5f1a5af7 100644
--- a/src/util/iand.h
+++ b/src/util/iand.h
@@ -24,7 +24,7 @@
 
 namespace CVC4 {
 
-struct CVC4_PUBLIC IntAnd
+struct IntAnd
 {
   unsigned d_size;
   IntAnd(unsigned size) : d_size(size) {}
@@ -35,7 +35,7 @@ struct CVC4_PUBLIC IntAnd
  ** Output stream
  * ----------------------------------------------------------------------- */
 
-inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia);
 inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia)
 {
   return os << "[" << ia.d_size << "]";
diff --git a/src/util/indexed_root_predicate.h b/src/util/indexed_root_predicate.h
index 1c9491078..3c36a6a97 100644
--- a/src/util/indexed_root_predicate.h
+++ b/src/util/indexed_root_predicate.h
@@ -40,7 +40,7 @@ namespace CVC4 {
  *  IRP_1(x = 0, x*x-2)  <=>  x = -sqrt(2)
  *  IRP_1(x = 0, x*x-y), y=3  <=>  x = -sqrt(3)
  */
-struct CVC4_PUBLIC IndexedRootPredicate
+struct IndexedRootPredicate
 {
   /** The index of the root */
   std::uint64_t d_index;
@@ -54,14 +54,14 @@ struct CVC4_PUBLIC IndexedRootPredicate
 }; /* struct IndexedRootPredicate */
 
 inline std::ostream& operator<<(std::ostream& os,
-                                const IndexedRootPredicate& irp) CVC4_PUBLIC;
+                                const IndexedRootPredicate& irp);
 inline std::ostream& operator<<(std::ostream& os,
                                 const IndexedRootPredicate& irp)
 {
   return os << "k=" << irp.d_index;
 }
 
-struct CVC4_PUBLIC IndexedRootPredicateHashFunction
+struct IndexedRootPredicateHashFunction
 {
   std::size_t operator()(const IndexedRootPredicate& irp) const
   {
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 3a6da7b9e..1687bc776 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -31,12 +31,13 @@
 #include <string>
 
 #include "base/exception.h"
+#include "cvc4_export.h"  // remove when Cvc language support is removed
 
 namespace CVC4 {
 
 class Rational;
 
-class CVC4_PUBLIC Integer
+class CVC4_EXPORT Integer
 {
   friend class CVC4::Rational;
 
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 4215189a0..9cd230d35 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -25,11 +25,13 @@
 #include <iosfwd>
 #include <string>
 
+#include "cvc4_export.h"  // remove when Cvc language support is removed
+
 namespace CVC4 {
 
 class Rational;
 
-class CVC4_PUBLIC Integer
+class CVC4_EXPORT Integer
 {
   friend class CVC4::Rational;
 
diff --git a/src/util/maybe.h b/src/util/maybe.h
index febcbe401..a74a42a17 100644
--- a/src/util/maybe.h
+++ b/src/util/maybe.h
@@ -34,7 +34,7 @@
 namespace CVC4 {
 
 template <class T>
-class CVC4_PUBLIC Maybe
+class Maybe
 {
  public:
   Maybe() : d_just(false), d_value(){}
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 6d83a5a0f..bd48ad851 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -33,6 +33,7 @@
 #include <string>
 
 #include "base/exception.h"
+#include "cvc4_export.h"  // remove when Cvc language support is removed
 #include "util/integer.h"
 #include "util/maybe.h"
 
@@ -53,7 +54,7 @@ namespace CVC4 {
  ** in danger of invoking the char* constructor, from whence you will segfault.
  **/
 
-class CVC4_PUBLIC Rational
+class CVC4_EXPORT Rational
 {
  public:
   /**
@@ -338,7 +339,7 @@ struct RationalHashFunction
   inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); }
 }; /* struct RationalHashFunction */
 
-CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
+std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT;
 
 }  // namespace CVC4
 
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 54a81c856..490211001 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -24,6 +24,7 @@
 
 #include <string>
 
+#include "cvc4_export.h"  // remove when Cvc language support is removed
 #include "util/gmp_util.h"
 #include "util/integer.h"
 #include "util/maybe.h"
@@ -45,7 +46,7 @@ namespace CVC4 {
  ** in danger of invoking the char* constructor, from whence you will segfault.
  **/
 
-class CVC4_PUBLIC Rational
+class CVC4_EXPORT Rational
 {
  public:
   /**
@@ -328,7 +329,7 @@ struct RationalHashFunction
   inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); }
 }; /* struct RationalHashFunction */
 
-CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
+std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT;
 
 }  // namespace CVC4
 
diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h
index 01c0ca343..ef5ff16f1 100644
--- a/src/util/real_algebraic_number_poly_imp.h
+++ b/src/util/real_algebraic_number_poly_imp.h
@@ -40,7 +40,7 @@ namespace CVC4 {
  * Note that the interval representation uses dyadic rationals (denominators are
  * only powers of two).
  */
-class CVC4_PUBLIC RealAlgebraicNumber
+class RealAlgebraicNumber
 {
  public:
   /** Construct as zero. */
@@ -103,57 +103,50 @@ class CVC4_PUBLIC RealAlgebraicNumber
 }; /* class RealAlgebraicNumber */
 
 /** Stream a real algebraic number to an output stream. */
-CVC4_PUBLIC std::ostream& operator<<(std::ostream& os,
-                                     const RealAlgebraicNumber& ran);
+std::ostream& operator<<(std::ostream& os, const RealAlgebraicNumber& ran);
 
 /** Compare two real algebraic numbers. */
-CVC4_PUBLIC bool operator==(const RealAlgebraicNumber& lhs,
-                            const RealAlgebraicNumber& rhs);
+bool operator==(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
 /** Compare two real algebraic numbers. */
-CVC4_PUBLIC bool operator!=(const RealAlgebraicNumber& lhs,
-                            const RealAlgebraicNumber& rhs);
+bool operator!=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
 /** Compare two real algebraic numbers. */
-CVC4_PUBLIC bool operator<(const RealAlgebraicNumber& lhs,
-                           const RealAlgebraicNumber& rhs);
+bool operator<(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
 /** Compare two real algebraic numbers. */
-CVC4_PUBLIC bool operator<=(const RealAlgebraicNumber& lhs,
-                            const RealAlgebraicNumber& rhs);
+bool operator<=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
 /** Compare two real algebraic numbers. */
-CVC4_PUBLIC bool operator>(const RealAlgebraicNumber& lhs,
-                           const RealAlgebraicNumber& rhs);
+bool operator>(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
 /** Compare two real algebraic numbers. */
-CVC4_PUBLIC bool operator>=(const RealAlgebraicNumber& lhs,
-                            const RealAlgebraicNumber& rhs);
+bool operator>=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs);
 
 /** Add two real algebraic numbers. */
-CVC4_PUBLIC RealAlgebraicNumber operator+(const RealAlgebraicNumber& lhs,
-                                          const RealAlgebraicNumber& rhs);
+RealAlgebraicNumber operator+(const RealAlgebraicNumber& lhs,
+                              const RealAlgebraicNumber& rhs);
 /** Subtract two real algebraic numbers. */
-CVC4_PUBLIC RealAlgebraicNumber operator-(const RealAlgebraicNumber& lhs,
-                                          const RealAlgebraicNumber& rhs);
+RealAlgebraicNumber operator-(const RealAlgebraicNumber& lhs,
+                              const RealAlgebraicNumber& rhs);
 /** Negate a real algebraic number. */
-CVC4_PUBLIC RealAlgebraicNumber operator-(const RealAlgebraicNumber& ran);
+RealAlgebraicNumber operator-(const RealAlgebraicNumber& ran);
 /** Multiply two real algebraic numbers. */
-CVC4_PUBLIC RealAlgebraicNumber operator*(const RealAlgebraicNumber& lhs,
-                                          const RealAlgebraicNumber& rhs);
+RealAlgebraicNumber operator*(const RealAlgebraicNumber& lhs,
+                              const RealAlgebraicNumber& rhs);
 
 /** Add and assign two real algebraic numbers. */
-CVC4_PUBLIC RealAlgebraicNumber& operator+=(RealAlgebraicNumber& lhs,
-                                            const RealAlgebraicNumber& rhs);
+RealAlgebraicNumber& operator+=(RealAlgebraicNumber& lhs,
+                                const RealAlgebraicNumber& rhs);
 /** Subtract and assign two real algebraic numbers. */
-CVC4_PUBLIC RealAlgebraicNumber& operator-=(RealAlgebraicNumber& lhs,
-                                            const RealAlgebraicNumber& rhs);
+RealAlgebraicNumber& operator-=(RealAlgebraicNumber& lhs,
+                                const RealAlgebraicNumber& rhs);
 /** Multiply and assign two real algebraic numbers. */
-CVC4_PUBLIC RealAlgebraicNumber& operator*=(RealAlgebraicNumber& lhs,
-                                            const RealAlgebraicNumber& rhs);
+RealAlgebraicNumber& operator*=(RealAlgebraicNumber& lhs,
+                                const RealAlgebraicNumber& rhs);
 
 /** Compute the sign of a real algebraic number. */
-CVC4_PUBLIC int sgn(const RealAlgebraicNumber& ran);
+int sgn(const RealAlgebraicNumber& ran);
 
 /** Check whether a real algebraic number is zero. */
-CVC4_PUBLIC bool isZero(const RealAlgebraicNumber& ran);
+bool isZero(const RealAlgebraicNumber& ran);
 /** Check whether a real algebraic number is one. */
-CVC4_PUBLIC bool isOne(const RealAlgebraicNumber& ran);
+bool isOne(const RealAlgebraicNumber& ran);
 
 }  // namespace CVC4
 
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 94addf171..b08065a25 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -21,7 +21,7 @@
 
 namespace CVC4 {
 
-struct CVC4_PUBLIC RegExpRepeat
+struct RegExpRepeat
 {
   RegExpRepeat(uint32_t repeatAmount);
 
@@ -30,7 +30,7 @@ struct CVC4_PUBLIC RegExpRepeat
   uint32_t d_repeatAmount;
 };
 
-struct CVC4_PUBLIC RegExpLoop
+struct RegExpLoop
 {
   RegExpLoop(uint32_t l, uint32_t h);
 
@@ -48,7 +48,7 @@ struct CVC4_PUBLIC RegExpLoop
 /*
  * Hash function for the RegExpRepeat constants.
  */
-struct CVC4_PUBLIC RegExpRepeatHashFunction
+struct RegExpRepeatHashFunction
 {
   size_t operator()(const RegExpRepeat& r) const;
 };
@@ -56,7 +56,7 @@ struct CVC4_PUBLIC RegExpRepeatHashFunction
 /**
  * Hash function for the RegExpLoop objects.
  */
-struct CVC4_PUBLIC RegExpLoopHashFunction
+struct RegExpLoopHashFunction
 {
   size_t operator()(const RegExpLoop& r) const;
 };
@@ -65,9 +65,9 @@ struct CVC4_PUBLIC RegExpLoopHashFunction
  ** Output stream
  * ----------------------------------------------------------------------- */
 
-std::ostream& operator<<(std::ostream& os, const RegExpRepeat& bv) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& os, const RegExpRepeat& bv);
 
-std::ostream& operator<<(std::ostream& os, const RegExpLoop& bv) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& os, const RegExpLoop& bv);
 
 }  // namespace CVC4
 
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index d9c30bc7f..a8a7edb75 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -35,7 +35,7 @@ class StatisticsRegistry;
 /**
  * This class implements a easy to use wall clock timer based on std::chrono.
  */
-class CVC4_PUBLIC WallClockTimer
+class WallClockTimer
 {
   /**
    * The underlying clock that is used.
@@ -71,7 +71,7 @@ class CVC4_PUBLIC WallClockTimer
  * time limits. The available resources are listed in ResourceManager::Resource
  * and their individual costs are configured via command line options.
  */
-class CVC4_PUBLIC ResourceManager
+class ResourceManager
 {
  public:
   /** Types of resources. */
diff --git a/src/util/result.h b/src/util/result.h
index f325e2496..b5c5451ea 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -28,12 +28,13 @@ namespace CVC4 {
 
 class Result;
 
-std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const Result& r);
 
 /**
  * Three-valued SMT result, with optional explanation.
  */
-class CVC4_PUBLIC Result {
+class Result
+{
  public:
   enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 };
 
@@ -149,17 +150,15 @@ class CVC4_PUBLIC Result {
 
 inline bool Result::operator!=(const Result& r) const { return !(*this == r); }
 
-std::ostream& operator<<(std::ostream& out, enum Result::Sat s) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& out,
-                         enum Result::Entailment e) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& out,
-                         enum Result::UnknownExplanation e) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, enum Result::Sat s);
+std::ostream& operator<<(std::ostream& out, enum Result::Entailment e);
+std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e);
 
-bool operator==(enum Result::Sat s, const Result& r) CVC4_PUBLIC;
-bool operator==(enum Result::Entailment e, const Result& r) CVC4_PUBLIC;
+bool operator==(enum Result::Sat s, const Result& r);
+bool operator==(enum Result::Entailment e, const Result& r);
 
-bool operator!=(enum Result::Sat s, const Result& r) CVC4_PUBLIC;
-bool operator!=(enum Result::Entailment e, const Result& r) CVC4_PUBLIC;
+bool operator!=(enum Result::Sat s, const Result& r);
+bool operator!=(enum Result::Entailment e, const Result& r);
 
 } /* CVC4 namespace */
 
diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h
index 8c87df606..485bbf847 100644
--- a/src/util/roundingmode.h
+++ b/src/util/roundingmode.h
@@ -25,7 +25,7 @@ namespace CVC4 {
 /**
  * A concrete instance of the rounding mode sort
  */
-enum CVC4_PUBLIC RoundingMode
+enum RoundingMode
 {
   ROUND_NEAREST_TIES_TO_EVEN = FE_TONEAREST,
   ROUND_TOWARD_POSITIVE = FE_UPWARD,
@@ -40,7 +40,7 @@ enum CVC4_PUBLIC RoundingMode
 /**
  * Hash function for rounding mode values.
  */
-struct CVC4_PUBLIC RoundingModeHashFunction
+struct RoundingModeHashFunction
 {
   inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); }
 }; /* struct RoundingModeHashFunction */
diff --git a/src/util/safe_print.h b/src/util/safe_print.h
index cb3f46721..dd66ed41b 100644
--- a/src/util/safe_print.h
+++ b/src/util/safe_print.h
@@ -42,6 +42,8 @@
 #include <cstring>
 #include <string>
 
+#include "cvc4_export.h"
+
 namespace CVC4 {
 
 /**
@@ -49,7 +51,8 @@ namespace CVC4 {
  * signal handler.
  */
 template <size_t N>
-void CVC4_PUBLIC safe_print(int fd, const char (&msg)[N]) {
+void CVC4_EXPORT safe_print(int fd, const char (&msg)[N])
+{
   ssize_t nb = N - 1;
   if (write(fd, msg, nb) != nb) {
     abort();
@@ -92,7 +95,7 @@ auto toStringImpl(const T& obj, int) -> decltype(toString(obj))
  * @param obj The object to print
  */
 template <typename T>
-void CVC4_PUBLIC safe_print(int fd, const T& obj)
+void CVC4_EXPORT safe_print(int fd, const T& obj)
 {
   const char* s =
       toStringImpl(obj, /* prefer the method that uses `toString()` */ 0);
@@ -104,25 +107,25 @@ void CVC4_PUBLIC safe_print(int fd, const T& obj)
 }
 
 template <>
-void CVC4_PUBLIC safe_print(int fd, const std::string& msg);
+void CVC4_EXPORT safe_print(int fd, const std::string& msg);
 template <>
-void CVC4_PUBLIC safe_print(int fd, const int64_t& _i);
+void CVC4_EXPORT safe_print(int fd, const int64_t& _i);
 template <>
-void CVC4_PUBLIC safe_print(int fd, const int32_t& i);
+void CVC4_EXPORT safe_print(int fd, const int32_t& i);
 template <>
-void CVC4_PUBLIC safe_print(int fd, const uint64_t& _i);
+void CVC4_EXPORT safe_print(int fd, const uint64_t& _i);
 template <>
-void CVC4_PUBLIC safe_print(int fd, const uint32_t& i);
+void CVC4_EXPORT safe_print(int fd, const uint32_t& i);
 template <>
-void CVC4_PUBLIC safe_print(int fd, const double& _d);
+void CVC4_EXPORT safe_print(int fd, const double& _d);
 template <>
-void CVC4_PUBLIC safe_print(int fd, const float& f);
+void CVC4_EXPORT safe_print(int fd, const float& f);
 template <>
-void CVC4_PUBLIC safe_print(int fd, const bool& b);
+void CVC4_EXPORT safe_print(int fd, const bool& b);
 template <>
-void CVC4_PUBLIC safe_print(int fd, void* const& addr);
+void CVC4_EXPORT safe_print(int fd, void* const& addr);
 template <>
-void CVC4_PUBLIC safe_print(int fd, const timespec& t);
+void CVC4_EXPORT safe_print(int fd, const timespec& t);
 
 /** Prints an integer in hexadecimal. Safe to use in a signal handler. */
 void safe_print_hex(int fd, uint64_t i);
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 9e4ac0837..aabbf473d 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -30,13 +30,15 @@
 #include <string>
 #include <vector>
 
+#include "cvc4_export.h"
 #include "options/language.h"
 #include "util/integer.h"
 #include "util/rational.h"
 
 namespace CVC4 {
 
-class CVC4_PUBLIC SExprKeyword {
+class SExprKeyword
+{
  public:
   SExprKeyword(const std::string& s) : d_str(s) {}
   const std::string& getString() const { return d_str; }
@@ -49,7 +51,8 @@ class CVC4_PUBLIC SExprKeyword {
  * A simple S-expression. An S-expression is either an atom with a
  * string value, or a list of other S-expressions.
  */
-class CVC4_PUBLIC SExpr {
+class CVC4_EXPORT SExpr
+{
  public:
   typedef SExprKeyword Keyword;
 
@@ -231,12 +234,13 @@ class CVC4_PUBLIC SExpr {
 }; /* class SExpr */
 
 /** Prints an SExpr. */
-std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_EXPORT;
 
 /**
  * IOStream manipulator to pretty-print SExprs.
  */
-class CVC4_PUBLIC PrettySExprs {
+class CVC4_EXPORT PrettySExprs
+{
   /**
    * The allocated index in ios_base for our setting.
    */
diff --git a/src/util/statistics.h b/src/util/statistics.h
index ce8f4711f..7b5400aaf 100644
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -26,15 +26,16 @@
 #include <string>
 #include <utility>
 
+#include "cvc4_export.h"
 #include "util/sexpr.h"
 
 namespace CVC4 {
 
 class Stat;
 
-class CVC4_PUBLIC StatisticsBase {
-protected:
-
+class CVC4_EXPORT StatisticsBase
+{
+ protected:
   /** A helper class for comparing two statistics */
   struct StatCmp {
     bool operator()(const Stat* s1, const Stat* s2) const;
@@ -54,7 +55,9 @@ public:
 
   virtual ~StatisticsBase() { }
 
-  class CVC4_PUBLIC iterator : public std::iterator< std::input_iterator_tag, std::pair<std::string, SExpr> > {
+  class iterator : public std::iterator<std::input_iterator_tag,
+                                        std::pair<std::string, SExpr> >
+  {
     StatSet::iterator d_it;
 
     iterator(StatSet::iterator it) : d_it(it) { }
@@ -69,7 +72,7 @@ public:
     iterator operator++(int) { iterator old = *this; ++d_it; return old; }
     bool operator==(const iterator& i) const { return d_it == i.d_it; }
     bool operator!=(const iterator& i) const { return d_it != i.d_it; }
-  };/* class StatisticsBase::iterator */
+  }; /* class StatisticsBase::iterator */
 
   /** An iterator type over a set of statistics. */
   typedef iterator const_iterator;
@@ -97,9 +100,10 @@ public:
    */
   const_iterator end() const;
 
-};/* class StatisticsBase */
+}; /* class StatisticsBase */
 
-class CVC4_PUBLIC Statistics : public StatisticsBase {
+class Statistics : public StatisticsBase
+{
   void clear();
   void copyFrom(const StatisticsBase&);
 
@@ -121,7 +125,7 @@ public:
   Statistics& operator=(const StatisticsBase& stats);
   Statistics& operator=(const Statistics& stats);
 
-};/* class Statistics */
+}; /* class Statistics */
 
 }/* CVC4 namespace */
 
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 7382bafa3..a55aec282 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -16,14 +16,14 @@
  ** classes.
  **
  ** This file is somewhat unique in that it is a "cvc4_private_library.h"
- ** header. Because of this, most classes need to be marked as CVC4_PUBLIC.
- ** This is because CVC4_PUBLIC is connected to the visibility of the linkage
+ ** header. Because of this, most classes need to be marked as CVC4_EXPORT.
+ ** This is because CVC4_EXPORT is connected to the visibility of the linkage
  ** in the object files for the class. It does not dictate what headers are
  ** installed.
  ** Because the StatisticsRegistry and associated classes are built into
  ** libutil, which is used by libcvc4, and then later used by the libmain
  ** without referring to libutil as well. Thus the without marking these as
- ** CVC4_PUBLIC the symbols would be external in libutil, internal in libcvc4,
+ ** CVC4_EXPORT the symbols would be external in libutil, internal in libcvc4,
  ** and not be visible to libmain and linking would fail.
  ** You can debug this using "nm" on the .so and .o files in the builds/
  ** directory. See
@@ -31,7 +31,6 @@
  ** for a longer discussion on symbol visibility.
  **/
 
-
 /**
  * On the design of the statistics:
  * 
@@ -98,9 +97,10 @@
 #endif
 
 #include "base/exception.h"
+#include "cvc4_export.h"
 #include "util/safe_print.h"
-#include "util/stats_base.h"
 #include "util/statistics.h"
+#include "util/stats_base.h"
 
 namespace CVC4 {
 
@@ -142,9 +142,9 @@ public:
  * The main statistics registry.  This registry maintains the list of
  * currently active statistics and is able to "flush" them all.
  */
-class CVC4_PUBLIC StatisticsRegistry : public StatisticsBase {
-private:
-
+class CVC4_EXPORT StatisticsRegistry : public StatisticsBase
+{
+ private:
   /** Private copy constructor undefined (no copy permitted). */
   StatisticsRegistry(const StatisticsRegistry&) = delete;
 
@@ -177,15 +177,16 @@ public:
   /** Unregister a new statistic */
   void unregisterStat(Stat* s);
 
-};/* class StatisticsRegistry */
+}; /* class StatisticsRegistry */
 
 /**
  * Resource-acquisition-is-initialization idiom for statistics
  * registry.  Useful for stack-based statistics (like in the driver).
  * This RAII class only does registration and unregistration.
  */
-class CVC4_PUBLIC RegisterStatistic {
-public:
+class CVC4_EXPORT RegisterStatistic
+{
+ public:
   RegisterStatistic(StatisticsRegistry* reg, Stat* stat);
   ~RegisterStatistic();
 
@@ -193,7 +194,7 @@ private:
   StatisticsRegistry* d_reg;
   Stat* d_stat;
 
-};/* class RegisterStatistic */
+}; /* class RegisterStatistic */
 
 }/* CVC4 namespace */
 
diff --git a/src/util/stats_base.h b/src/util/stats_base.h
index c9ff2131f..24a2ca560 100644
--- a/src/util/stats_base.h
+++ b/src/util/stats_base.h
@@ -23,6 +23,7 @@
 #include <sstream>
 #include <string>
 
+#include "cvc4_export.h"
 #include "util/safe_print.h"
 #include "util/sexpr.h"
 #include "util/stats_utils.h"
@@ -43,7 +44,7 @@ namespace CVC4 {
  * Derived classes must implement these function and pass their name to
  * the base class constructor.
  */
-class Stat
+class CVC4_EXPORT Stat
 {
  public:
   /**
diff --git a/src/util/stats_timer.h b/src/util/stats_timer.h
index a2dfd626a..36e254795 100644
--- a/src/util/stats_timer.h
+++ b/src/util/stats_timer.h
@@ -21,6 +21,7 @@
 
 #include <chrono>
 
+#include "cvc4_export.h"
 #include "util/stats_base.h"
 
 namespace CVC4 {
@@ -33,7 +34,7 @@ struct duration : public std::chrono::nanoseconds
 }  // namespace timer_stat_detail
 
 template <>
-void CVC4_PUBLIC safe_print(int fd, const timer_stat_detail::duration& t);
+void CVC4_EXPORT safe_print(int fd, const timer_stat_detail::duration& t);
 
 class CodeTimer;
 
@@ -42,7 +43,7 @@ class CodeTimer;
  * arbitrarily, like a stopwatch; the value of the statistic at the
  * end is the accumulated time over all (start,stop) pairs.
  */
-class CVC4_PUBLIC TimerStat : public BackedStat<timer_stat_detail::duration>
+class CVC4_EXPORT TimerStat : public BackedStat<timer_stat_detail::duration>
 {
  public:
   typedef CVC4::CodeTimer CodeTimer;
diff --git a/src/util/stats_utils.h b/src/util/stats_utils.h
index df692af1f..b38f7b641 100644
--- a/src/util/stats_utils.h
+++ b/src/util/stats_utils.h
@@ -21,6 +21,8 @@
 
 #include <iosfwd>
 
+#include "cvc4_export.h"
+
 namespace CVC4 {
 
 namespace timer_stat_detail {
@@ -28,7 +30,7 @@ struct duration;
 }
 
 std::ostream& operator<<(std::ostream& os,
-                         const timer_stat_detail::duration& dur) CVC4_PUBLIC;
+                         const timer_stat_detail::duration& dur) CVC4_EXPORT;
 
 }  // namespace CVC4
 
diff --git a/src/util/string.h b/src/util/string.h
index 83967f3c6..6c620587a 100644
--- a/src/util/string.h
+++ b/src/util/string.h
@@ -30,7 +30,8 @@ namespace CVC4 {
  * This data structure is the domain of values for the string type. It can also
  * be used as a generic utility for representing strings.
  */
-class CVC4_PUBLIC String {
+class String
+{
  public:
   /**
    * This is the cardinality of the alphabet that is representable by this
@@ -262,7 +263,8 @@ class CVC4_PUBLIC String {
 
 namespace strings {
 
-struct CVC4_PUBLIC StringHashFunction {
+struct StringHashFunction
+{
   size_t operator()(const ::CVC4::String& s) const {
     return std::hash<std::string>()(s.toString());
   }
@@ -270,7 +272,7 @@ struct CVC4_PUBLIC StringHashFunction {
 
 }  // namespace strings
 
-std::ostream& operator<<(std::ostream& os, const String& s) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& os, const String& s);
 
 }  // namespace CVC4
 
diff --git a/src/util/tuple.h b/src/util/tuple.h
index b3c50b358..d77d7bf97 100644
--- a/src/util/tuple.h
+++ b/src/util/tuple.h
@@ -25,7 +25,8 @@
 
 namespace CVC4 {
 
-class CVC4_PUBLIC TupleUpdate {
+class TupleUpdate
+{
   unsigned d_index;
 
  public:
@@ -33,15 +34,16 @@ class CVC4_PUBLIC TupleUpdate {
   unsigned getIndex() const { return d_index; }
   bool operator==(const TupleUpdate& t) const { return d_index == t.d_index; }
   bool operator!=(const TupleUpdate& t) const { return d_index != t.d_index; }
-};/* class TupleUpdate */
+}; /* class TupleUpdate */
 
-struct CVC4_PUBLIC TupleUpdateHashFunction {
+struct TupleUpdateHashFunction
+{
   inline size_t operator()(const TupleUpdate& t) const {
     return t.getIndex();
   }
-};/* struct TupleUpdateHashFunction */
+}; /* struct TupleUpdateHashFunction */
 
-std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, const TupleUpdate& t);
 
 inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) {
   return out << "[" << t.getIndex() << "]";
diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h
index 3f6205232..29c22409c 100644
--- a/src/util/unsafe_interrupt_exception.h
+++ b/src/util/unsafe_interrupt_exception.h
@@ -19,11 +19,13 @@
 #define CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
 
 #include "base/exception.h"
+#include "cvc4_export.h"
 
 namespace CVC4 {
 
-class CVC4_PUBLIC UnsafeInterruptException : public CVC4::Exception {
-public:
+class CVC4_EXPORT UnsafeInterruptException : public CVC4::Exception
+{
+ public:
   UnsafeInterruptException() :
     Exception("Interrupted in unsafe state due to "
               "time/resource limit.") {
@@ -36,7 +38,7 @@ public:
   UnsafeInterruptException(const char* msg) :
     Exception(msg) {
   }
-};/* class UnsafeInterruptException */
+}; /* class UnsafeInterruptException */
 
 }/* CVC4 namespace */