diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-03-16 10:56:01 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-16 10:56:01 -0700 |
commit | d6890791897ddebf1212d3e3147bf7aeb2415b27 (patch) | |
tree | 51c69ba48a7550b6a7660e2488b4b39cbedba539 /src/util | |
parent | 0d3ea6f2dcaf80d386c7765ee8a708c18e3ed574 (diff) |
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>
Diffstat (limited to 'src/util')
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 */ |