diff options
81 files changed, 599 insertions, 510 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index dc244917d..c06c360ac 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -40,6 +40,8 @@ set(CMAKE_C_STANDARD 99) set(CMAKE_CXX_STANDARD 17) set(CMAKE_CXX_EXTENSIONS OFF) set(CMAKE_CXX_STANDARD_REQUIRED ON) +set(CMAKE_CXX_VISIBILITY_PRESET hidden) +set(CMAKE_VISIBILITY_INLINES_HIDDEN 1) # Generate compile_commands.json, which can be used for various code completion # plugins. @@ -292,6 +294,12 @@ if(ENABLE_SHARED) message(WARNING "Disabling static binary since shared build is enabled.") endif() + # Set visibility to default if unit tests are enabled + if(ENABLE_UNIT_TESTING) + set(CMAKE_CXX_VISIBILITY_PRESET default) + set(CMAKE_VISIBILITY_INLINES_HIDDEN 0) + endif() + # Embed the installation prefix as an RPATH in the executable such that the # linker can find our libraries (such as libcvc4parser) when executing the # cvc4 binary. This is for example useful when installing CVC4 with a custom diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake index b01c2bb23..50907a561 100644 --- a/cmake/ConfigDebug.cmake +++ b/cmake/ConfigDebug.cmake @@ -27,3 +27,7 @@ cvc4_set_option(ENABLE_DUMPING ON) cvc4_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=optional cvc4_set_option(ENABLE_UNIT_TESTING ON) + +# Reset visibility for debug builds (https://github.com/CVC4/CVC4/issues/324) +set(CMAKE_CXX_VISIBILITY_PRESET default) +set(CMAKE_VISIBILITY_INLINES_HIDDEN 0) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 042969884..e8dd5d0aa 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1089,6 +1089,9 @@ target_include_directories(cvc4 $<INSTALL_INTERFACE:include> ) +include(GenerateExportHeader) +generate_export_header(cvc4) + install(TARGETS cvc4 EXPORT cvc4-targets LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} @@ -1178,7 +1181,7 @@ install(FILES DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/api) install(FILES - include/cvc4_public.h + ${CMAKE_CURRENT_BINARY_DIR}/cvc4_export.h DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/) diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 5a1a75024..8e7971e68 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -14,7 +14,7 @@ ** The CVC4 C++ API. **/ -#include "cvc4_public.h" +#include "cvc4_export.h" #ifndef CVC4__API__CVC4CPP_H #define CVC4__API__CVC4CPP_H @@ -79,7 +79,7 @@ struct Statistics; /* Exception */ /* -------------------------------------------------------------------------- */ -class CVC4_PUBLIC CVC4ApiException : public std::exception +class CVC4_EXPORT CVC4ApiException : public std::exception { public: CVC4ApiException(const std::string& str) : d_msg(str) {} @@ -91,7 +91,7 @@ class CVC4_PUBLIC CVC4ApiException : public std::exception std::string d_msg; }; -class CVC4_PUBLIC CVC4ApiRecoverableException : public CVC4ApiException +class CVC4_EXPORT CVC4ApiRecoverableException : public CVC4ApiException { public: CVC4ApiRecoverableException(const std::string& str) : CVC4ApiException(str) {} @@ -108,7 +108,7 @@ class CVC4_PUBLIC CVC4ApiRecoverableException : public CVC4ApiException /** * Encapsulation of a three-valued solver result, with explanations. */ -class CVC4_PUBLIC Result +class CVC4_EXPORT Result { friend class Solver; @@ -217,7 +217,7 @@ class CVC4_PUBLIC Result * @param r the result to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_EXPORT; /** * Serialize an UnknownExplanation to given stream. @@ -226,7 +226,7 @@ std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; * @return the output stream */ std::ostream& operator<<(std::ostream& out, - enum Result::UnknownExplanation e) CVC4_PUBLIC; + enum Result::UnknownExplanation e) CVC4_EXPORT; /* -------------------------------------------------------------------------- */ /* Sort */ @@ -237,7 +237,7 @@ class Datatype; /** * The sort of a CVC4 term. */ -class CVC4_PUBLIC Sort +class CVC4_EXPORT Sort { friend class CVC4::DatatypeDeclarationCommand; friend class CVC4::DeclareFunctionCommand; @@ -745,12 +745,12 @@ class CVC4_PUBLIC Sort * @param s the sort to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Sort& s) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const Sort& s) CVC4_EXPORT; /** * Hash function for Sorts. */ -struct CVC4_PUBLIC SortHashFunction +struct CVC4_EXPORT SortHashFunction { size_t operator()(const Sort& s) const; }; @@ -764,7 +764,7 @@ struct CVC4_PUBLIC SortHashFunction * An operator is a term that represents certain operators, instantiated * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT. */ -class CVC4_PUBLIC Op +class CVC4_EXPORT Op { friend class Solver; friend class Term; @@ -887,7 +887,7 @@ class CVC4_PUBLIC Op /** * A CVC4 Term. */ -class CVC4_PUBLIC Term +class CVC4_EXPORT Term { friend class CVC4::AssertCommand; friend class CVC4::BlockModelValuesCommand; @@ -1294,7 +1294,7 @@ class CVC4_PUBLIC Term /** * Hash function for Terms. */ -struct CVC4_PUBLIC TermHashFunction +struct CVC4_EXPORT TermHashFunction { size_t operator()(const Term& t) const; }; @@ -1305,7 +1305,7 @@ struct CVC4_PUBLIC TermHashFunction * @param t the term to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_EXPORT; /** * Serialize a vector of terms to given stream. @@ -1314,7 +1314,7 @@ std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_PUBLIC; * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const std::vector<Term>& vector) CVC4_PUBLIC; + const std::vector<Term>& vector) CVC4_EXPORT; /** * Serialize a set of terms to the given stream. @@ -1323,7 +1323,7 @@ std::ostream& operator<<(std::ostream& out, * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const std::set<Term>& set) CVC4_PUBLIC; + const std::set<Term>& set) CVC4_EXPORT; /** * Serialize an unordered_set of terms to the given stream. @@ -1334,7 +1334,7 @@ std::ostream& operator<<(std::ostream& out, */ std::ostream& operator<<(std::ostream& out, const std::unordered_set<Term, TermHashFunction>& - unordered_set) CVC4_PUBLIC; + unordered_set) CVC4_EXPORT; /** * Serialize a map of terms to the given stream. @@ -1345,7 +1345,7 @@ std::ostream& operator<<(std::ostream& out, */ template <typename V> std::ostream& operator<<(std::ostream& out, - const std::map<Term, V>& map) CVC4_PUBLIC; + const std::map<Term, V>& map) CVC4_EXPORT; /** * Serialize an unordered_map of terms to the given stream. @@ -1357,7 +1357,7 @@ std::ostream& operator<<(std::ostream& out, template <typename V> std::ostream& operator<<(std::ostream& out, const std::unordered_map<Term, V, TermHashFunction>& - unordered_map) CVC4_PUBLIC; + unordered_map) CVC4_EXPORT; /** * Serialize an operator to given stream. @@ -1365,12 +1365,12 @@ std::ostream& operator<<(std::ostream& out, * @param t the operator to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Op& t) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const Op& t) CVC4_EXPORT; /** * Hash function for Ops. */ -struct CVC4_PUBLIC OpHashFunction +struct CVC4_EXPORT OpHashFunction { size_t operator()(const Op& t) const; }; @@ -1385,7 +1385,7 @@ class DatatypeIterator; /** * A CVC4 datatype constructor declaration. */ -class CVC4_PUBLIC DatatypeConstructorDecl +class CVC4_EXPORT DatatypeConstructorDecl { friend class DatatypeDecl; friend class Solver; @@ -1455,7 +1455,7 @@ class Solver; /** * A CVC4 datatype declaration. */ -class CVC4_PUBLIC DatatypeDecl +class CVC4_EXPORT DatatypeDecl { friend class DatatypeConstructorArg; friend class Solver; @@ -1559,7 +1559,7 @@ class CVC4_PUBLIC DatatypeDecl /** * A CVC4 datatype selector. */ -class CVC4_PUBLIC DatatypeSelector +class CVC4_EXPORT DatatypeSelector { friend class DatatypeConstructor; friend class Solver; @@ -1628,7 +1628,7 @@ class CVC4_PUBLIC DatatypeSelector /** * A CVC4 datatype constructor. */ -class CVC4_PUBLIC DatatypeConstructor +class CVC4_EXPORT DatatypeConstructor { friend class Datatype; friend class Solver; @@ -1854,7 +1854,7 @@ class CVC4_PUBLIC DatatypeConstructor /* * A CVC4 datatype. */ -class CVC4_PUBLIC Datatype +class CVC4_EXPORT Datatype { friend class Solver; friend class Sort; @@ -2079,7 +2079,7 @@ class CVC4_PUBLIC Datatype * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const DatatypeDecl& dtdecl) CVC4_PUBLIC; + const DatatypeDecl& dtdecl) CVC4_EXPORT; /** * Serialize a datatype constructor declaration to given stream. @@ -2088,7 +2088,7 @@ std::ostream& operator<<(std::ostream& out, * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const DatatypeConstructorDecl& ctordecl) CVC4_PUBLIC; + const DatatypeConstructorDecl& ctordecl) CVC4_EXPORT; /** * Serialize a vector of datatype constructor declarations to given stream. @@ -2106,7 +2106,7 @@ std::ostream& operator<<(std::ostream& out, * @param dtdecl the datatype to be serialized to given stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_EXPORT; /** * Serialize a datatype constructor to given stream. @@ -2115,7 +2115,7 @@ std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_PUBLIC; * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const DatatypeConstructor& ctor) CVC4_PUBLIC; + const DatatypeConstructor& ctor) CVC4_EXPORT; /** * Serialize a datatype selector to given stream. @@ -2124,7 +2124,7 @@ std::ostream& operator<<(std::ostream& out, * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const DatatypeSelector& stor) CVC4_PUBLIC; + const DatatypeSelector& stor) CVC4_EXPORT; /* -------------------------------------------------------------------------- */ /* Grammar */ @@ -2133,7 +2133,7 @@ std::ostream& operator<<(std::ostream& out, /** * A Sygus Grammar. */ -class CVC4_PUBLIC Grammar +class CVC4_EXPORT Grammar { friend class CVC4::GetAbductCommand; friend class CVC4::GetInterpolCommand; @@ -2272,7 +2272,7 @@ class CVC4_PUBLIC Grammar * @param g the grammar to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_EXPORT; /* -------------------------------------------------------------------------- */ /* Rounding Mode for Floating Points */ @@ -2281,7 +2281,7 @@ std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_PUBLIC; /** * A CVC4 floating point rounding mode. */ -enum CVC4_PUBLIC RoundingMode +enum CVC4_EXPORT RoundingMode { ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE, @@ -2293,7 +2293,7 @@ enum CVC4_PUBLIC RoundingMode /** * Hash function for RoundingModes. */ -struct CVC4_PUBLIC RoundingModeHashFunction +struct CVC4_EXPORT RoundingModeHashFunction { inline size_t operator()(const RoundingMode& rm) const; }; @@ -2305,7 +2305,7 @@ struct CVC4_PUBLIC RoundingModeHashFunction /* * A CVC4 solver. */ -class CVC4_PUBLIC Solver +class CVC4_EXPORT Solver { friend class Datatype; friend class DatatypeDecl; diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 62154a078..c98667da7 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -14,7 +14,7 @@ ** The term kinds of the CVC4 C++ API. **/ -#include "cvc4_public.h" +#include "cvc4_export.h" #ifndef CVC4__API__CVC4CPPKIND_H #define CVC4__API__CVC4CPPKIND_H @@ -35,7 +35,7 @@ namespace api { * checks for validity). The size of this type depends on the size of * CVC4::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h). */ -enum CVC4_PUBLIC Kind : int32_t +enum CVC4_EXPORT Kind : int32_t { /** * Internal kind. @@ -2849,7 +2849,7 @@ enum CVC4_PUBLIC Kind : int32_t * @param k the kind * @return the string representation of kind k */ -std::string kindToString(Kind k) CVC4_PUBLIC; +std::string kindToString(Kind k) CVC4_EXPORT; /** * Serialize a kind to given stream. @@ -2857,12 +2857,12 @@ std::string kindToString(Kind k) CVC4_PUBLIC; * @param k the kind to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, Kind k) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, Kind k) CVC4_EXPORT; /** * Hash function for Kinds. */ -struct CVC4_PUBLIC KindHashFunction +struct CVC4_EXPORT KindHashFunction { size_t operator()(Kind k) const; }; diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index e6a0c71c5..b400c14e5 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -49,10 +49,15 @@ add_library(pycvc4 target_link_libraries(pycvc4 cvc4 ${PYTHON_LIBRARIES}) # Disable -Werror and other warnings for code generated by Cython. +# Note: Visibility is reset to default here since otherwise the PyInit_... +# function will not be exported correctly +# (https://github.com/cython/cython/issues/3380). set_target_properties(pycvc4 PROPERTIES COMPILE_FLAGS - "-Wno-error -Wno-shadow -Wno-implicit-fallthrough") + "-Wno-error -Wno-shadow -Wno-implicit-fallthrough" + CXX_VISIBILITY_PRESET default + VISIBILITY_INLINES_HIDDEN 0) python_extension_module(pycvc4) diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py index f93b14a85..c19364559 100644 --- a/src/api/python/genkinds.py +++ b/src/api/python/genkinds.py @@ -38,7 +38,7 @@ US = '_' NL = '\n' #################### Enum Declarations ################ -ENUM_START = 'enum CVC4_PUBLIC Kind' +ENUM_START = 'enum CVC4_EXPORT Kind' ENUM_END = CCB+SC ################ Comments and Macro Tokens ############ diff --git a/src/base/check.h b/src/base/check.h index 434d38ede..70c5c9016 100644 --- a/src/base/check.h +++ b/src/base/check.h @@ -38,6 +38,7 @@ #include <ostream> #include "base/exception.h" +#include "cvc4_export.h" // Define CVC4_NO_RETURN macro replacement for [[noreturn]]. #if defined(SWIG) @@ -91,7 +92,7 @@ namespace CVC4 { // Class that provides an ostream and whose destructor aborts! Direct usage of // this class is discouraged. -class FatalStream +class CVC4_EXPORT FatalStream { public: FatalStream(const char* function, const char* file, int line); diff --git a/src/base/configuration.h b/src/base/configuration.h index 792694378..aab136374 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -23,13 +23,16 @@ #include <string> +#include "cvc4_export.h" + namespace CVC4 { /** * Represents the (static) configuration of CVC4. */ -class CVC4_PUBLIC Configuration { -private: +class CVC4_EXPORT Configuration +{ + private: /** Private default ctor: Disallow construction of this class */ Configuration(); @@ -136,7 +139,7 @@ public: static std::string getCompiler(); static std::string getCompiledDateTime(); -};/* class Configuration */ +}; /* class Configuration */ }/* CVC4 namespace */ diff --git a/src/base/exception.h b/src/base/exception.h index f2b1b919e..d9bf83f44 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -23,9 +23,12 @@ #include <iosfwd> #include <string> +#include "cvc4_export.h" + namespace CVC4 { -class CVC4_PUBLIC Exception : public std::exception { +class Exception : public std::exception +{ protected: std::string d_msg; @@ -66,10 +69,11 @@ class CVC4_PUBLIC Exception : public std::exception { */ virtual void toStream(std::ostream& os) const { os << d_msg; } -};/* class Exception */ +}; /* class Exception */ -class CVC4_PUBLIC IllegalArgumentException : public Exception { -protected: +class CVC4_EXPORT IllegalArgumentException : public Exception +{ + protected: IllegalArgumentException() : Exception() {} void construct(const char* header, const char* extra, @@ -104,34 +108,34 @@ public: */ static std::string formatVariadic(); static std::string formatVariadic(const char* format, ...); -};/* class IllegalArgumentException */ +}; /* class IllegalArgumentException */ -inline std::ostream& operator<<(std::ostream& os, - const Exception& e) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& os, const Exception& e); inline std::ostream& operator<<(std::ostream& os, const Exception& e) { e.toStream(os); return os; } -template <class T> inline void CheckArgument(bool cond, const T& arg, - const char* tail) CVC4_PUBLIC; +template <class T> +inline void CheckArgument(bool cond, const T& arg, const char* tail); template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED, const char* tail CVC4_UNUSED) { if(__builtin_expect( ( !cond ), false )) { \ throw ::CVC4::IllegalArgumentException("", "", tail); \ } \ } -template <class T> inline void CheckArgument(bool cond, const T& arg) - CVC4_PUBLIC; +template <class T> +inline void CheckArgument(bool cond, const T& arg); template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED) { if(__builtin_expect( ( !cond ), false )) { \ throw ::CVC4::IllegalArgumentException("", "", ""); \ } \ } -class CVC4_PUBLIC LastExceptionBuffer { -public: +class CVC4_EXPORT LastExceptionBuffer +{ + public: LastExceptionBuffer(); ~LastExceptionBuffer(); diff --git a/src/base/listener.h b/src/base/listener.h index fa31920e8..4205aca01 100644 --- a/src/base/listener.h +++ b/src/base/listener.h @@ -27,8 +27,9 @@ namespace CVC4 { * * The interface provides a notify() function. */ -class CVC4_PUBLIC Listener { -public: +class Listener +{ + public: Listener(); virtual ~Listener(); diff --git a/src/base/modal_exception.h b/src/base/modal_exception.h index 41aedc7c0..bfd5c9469 100644 --- a/src/base/modal_exception.h +++ b/src/base/modal_exception.h @@ -26,8 +26,9 @@ namespace CVC4 { -class CVC4_PUBLIC ModalException : public CVC4::Exception { -public: +class ModalException : public CVC4::Exception +{ + public: ModalException() : Exception("Feature used while operating in " "incorrect state") { @@ -40,7 +41,7 @@ public: ModalException(const char* msg) : Exception(msg) { } -};/* class ModalException */ +}; /* class ModalException */ /** * Special case of ModalException that allows the execution of the solver to @@ -49,7 +50,8 @@ public: * TODO(#1108): This exception should not be needed anymore in future versions * of the public API. */ -class CVC4_PUBLIC RecoverableModalException : public CVC4::ModalException { +class RecoverableModalException : public CVC4::ModalException +{ public: RecoverableModalException(const std::string& msg) : ModalException(msg) {} diff --git a/src/base/output.cpp b/src/base/output.cpp index 1e6bbed98..93ebf2a70 100644 --- a/src/base/output.cpp +++ b/src/base/output.cpp @@ -27,18 +27,18 @@ namespace CVC4 { null_streambuf null_sb; ostream null_os(&null_sb); -NullC nullCvc4Stream CVC4_PUBLIC; +NullC nullCvc4Stream; const std::string CVC4ostream::s_tab = " "; const int CVC4ostream::s_indentIosIndex = ios_base::xalloc(); -DebugC DebugChannel CVC4_PUBLIC (&cout); -WarningC WarningChannel CVC4_PUBLIC (&cerr); -MessageC MessageChannel CVC4_PUBLIC (&cout); -NoticeC NoticeChannel CVC4_PUBLIC (&null_os); -ChatC ChatChannel CVC4_PUBLIC (&null_os); -TraceC TraceChannel CVC4_PUBLIC (&cout); +DebugC DebugChannel(&cout); +WarningC WarningChannel(&cerr); +MessageC MessageChannel(&cout); +NoticeC NoticeChannel(&null_os); +ChatC ChatChannel(&null_os); +TraceC TraceChannel(&cout); std::ostream DumpOutC::dump_cout(cout.rdbuf());// copy cout stream buffer -DumpOutC DumpOutChannel CVC4_PUBLIC (&DumpOutC::dump_cout); +DumpOutC DumpOutChannel(&DumpOutC::dump_cout); }/* CVC4 namespace */ diff --git a/src/base/output.h b/src/base/output.h index ae874fb5b..5791d6f8f 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -19,17 +19,20 @@ #ifndef CVC4__OUTPUT_H #define CVC4__OUTPUT_H +#include <cstdio> #include <ios> #include <iostream> -#include <string> -#include <cstdio> #include <set> +#include <string> #include <utility> +#include "cvc4_export.h" + namespace CVC4 { template <class T, class U> -std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, + const std::pair<T, U>& p) CVC4_EXPORT; template <class T, class U> std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) { @@ -43,21 +46,23 @@ std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) { * attached to a null_streambuf instance so that output is directed to * the bit bucket. */ -class CVC4_PUBLIC null_streambuf : public std::streambuf { -public: +class null_streambuf : public std::streambuf +{ + public: /* Overriding overflow() just ensures that EOF isn't returned on the * stream. Perhaps this is not so critical, but recommended; this * way the output stream looks like it's functioning, in a non-error * state. */ int overflow(int c) override { return c; } -};/* class null_streambuf */ +}; /* class null_streambuf */ /** A null stream-buffer singleton */ extern null_streambuf null_sb; /** A null output stream singleton */ -extern std::ostream null_os CVC4_PUBLIC; +extern std::ostream null_os CVC4_EXPORT; -class CVC4_PUBLIC CVC4ostream { +class CVC4_EXPORT CVC4ostream +{ static const std::string s_tab; static const int s_indentIosIndex; @@ -111,7 +116,7 @@ public: std::ostream* getStreamPointer() const { return d_os; } template <class T> - CVC4ostream& operator<<(T const& t) CVC4_PUBLIC; + CVC4ostream& operator<<(T const& t) CVC4_EXPORT; // support manipulators, endl, etc.. CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) { @@ -139,7 +144,7 @@ public: CVC4ostream& operator<<(CVC4ostream& (*pf)(CVC4ostream&)) { return pf(*this); } -};/* class CVC4ostream */ +}; /* class CVC4ostream */ inline CVC4ostream& push(CVC4ostream& stream) { stream.pushIndent(); @@ -171,17 +176,19 @@ CVC4ostream& CVC4ostream::operator<<(T const& t) { * builds. None of these should ever be called in such builds, but we * offer this to the compiler so it doesn't complain. */ -class CVC4_PUBLIC NullC { -public: - operator bool() const { return false; } - operator CVC4ostream() const { return CVC4ostream(); } - operator std::ostream&() const { return null_os; } -};/* class NullC */ +class NullC +{ + public: + operator bool() const { return false; } + operator CVC4ostream() const { return CVC4ostream(); } + operator std::ostream&() const { return null_os; } +}; /* class NullC */ -extern NullC nullCvc4Stream CVC4_PUBLIC; +extern NullC nullCvc4Stream CVC4_EXPORT; /** The debug output class */ -class CVC4_PUBLIC DebugC { +class DebugC +{ std::set<std::string> d_tags; std::ostream* d_os; @@ -217,10 +224,11 @@ public: std::ostream& setStream(std::ostream* os) { d_os = os; return *os; } std::ostream& getStream() const { return *d_os; } std::ostream* getStreamPointer() const { return d_os; } -};/* class DebugC */ +}; /* class DebugC */ /** The warning output class */ -class CVC4_PUBLIC WarningC { +class WarningC +{ std::set<std::pair<std::string, size_t> > d_alreadyWarned; std::ostream* d_os; @@ -251,10 +259,11 @@ public: return true; } -};/* class WarningC */ +}; /* class WarningC */ /** The message output class */ -class CVC4_PUBLIC MessageC { +class MessageC +{ std::ostream* d_os; public: @@ -267,10 +276,11 @@ public: std::ostream* getStreamPointer() const { return d_os; } bool isOn() const { return d_os != &null_os; } -};/* class MessageC */ +}; /* class MessageC */ /** The notice output class */ -class CVC4_PUBLIC NoticeC { +class NoticeC +{ std::ostream* d_os; public: @@ -283,10 +293,11 @@ public: std::ostream* getStreamPointer() const { return d_os; } bool isOn() const { return d_os != &null_os; } -};/* class NoticeC */ +}; /* class NoticeC */ /** The chat output class */ -class CVC4_PUBLIC ChatC { +class ChatC +{ std::ostream* d_os; public: @@ -299,10 +310,11 @@ public: std::ostream* getStreamPointer() const { return d_os; } bool isOn() const { return d_os != &null_os; } -};/* class ChatC */ +}; /* class ChatC */ /** The trace output class */ -class CVC4_PUBLIC TraceC { +class TraceC +{ std::ostream* d_os; std::set<std::string> d_tags; @@ -339,10 +351,11 @@ public: std::ostream& getStream() const { return *d_os; } std::ostream* getStreamPointer() const { return d_os; } -};/* class TraceC */ +}; /* class TraceC */ /** The dump output class */ -class CVC4_PUBLIC DumpOutC { +class DumpOutC +{ std::set<std::string> d_tags; std::ostream* d_os; @@ -380,22 +393,22 @@ public: std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() const { return *d_os; } std::ostream* getStreamPointer() const { return d_os; } -};/* class DumpOutC */ +}; /* class DumpOutC */ /** The debug output singleton */ -extern DebugC DebugChannel CVC4_PUBLIC; +extern DebugC DebugChannel CVC4_EXPORT; /** The warning output singleton */ -extern WarningC WarningChannel CVC4_PUBLIC; +extern WarningC WarningChannel CVC4_EXPORT; /** The message output singleton */ -extern MessageC MessageChannel CVC4_PUBLIC; +extern MessageC MessageChannel CVC4_EXPORT; /** The notice output singleton */ -extern NoticeC NoticeChannel CVC4_PUBLIC; +extern NoticeC NoticeChannel CVC4_EXPORT; /** The chat output singleton */ -extern ChatC ChatChannel CVC4_PUBLIC; +extern ChatC ChatChannel CVC4_EXPORT; /** The trace output singleton */ -extern TraceC TraceChannel CVC4_PUBLIC; +extern TraceC TraceChannel CVC4_EXPORT; /** The dump output singleton */ -extern DumpOutC DumpOutChannel CVC4_PUBLIC; +extern DumpOutC DumpOutChannel CVC4_EXPORT; #ifdef CVC4_MUZZLE @@ -451,7 +464,8 @@ public: #if defined(CVC4_DEBUG) && defined(CVC4_TRACING) -class CVC4_PUBLIC ScopedDebug { +class ScopedDebug +{ std::string d_tag; bool d_oldSetting; @@ -474,20 +488,22 @@ public: Debug.off(d_tag); } } -};/* class ScopedDebug */ +}; /* class ScopedDebug */ #else /* CVC4_DEBUG && CVC4_TRACING */ -class CVC4_PUBLIC ScopedDebug { -public: +class ScopedDebug +{ + public: ScopedDebug(std::string tag, bool newSetting = true) {} -};/* class ScopedDebug */ +}; /* class ScopedDebug */ #endif /* CVC4_DEBUG && CVC4_TRACING */ #ifdef CVC4_TRACING -class CVC4_PUBLIC ScopedTrace { +class ScopedTrace +{ std::string d_tag; bool d_oldSetting; @@ -510,14 +526,15 @@ public: Trace.off(d_tag); } } -};/* class ScopedTrace */ +}; /* class ScopedTrace */ #else /* CVC4_TRACING */ -class CVC4_PUBLIC ScopedTrace { -public: +class ScopedTrace +{ + public: ScopedTrace(std::string tag, bool newSetting = true) {} -};/* class ScopedTrace */ +}; /* class ScopedTrace */ #endif /* CVC4_TRACING */ @@ -527,12 +544,13 @@ public: * used for clearly separating different phases of an algorithm, * or iterations of a loop, or... etc. */ -class CVC4_PUBLIC IndentedScope { +class IndentedScope +{ CVC4ostream d_out; public: inline IndentedScope(CVC4ostream out); inline ~IndentedScope(); -};/* class IndentedScope */ +}; /* class IndentedScope */ #if defined(CVC4_DEBUG) && defined(CVC4_TRACING) inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; } diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h index b47b19d5f..dac967668 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -32,7 +32,8 @@ class NodeTemplate; typedef NodeTemplate<true> Node; class TypeNode; -class CVC4_PUBLIC ArrayStoreAll { +class ArrayStoreAll +{ public: /** * @throws IllegalArgumentException if `type` is not an array or if `expr` is @@ -59,13 +60,13 @@ class CVC4_PUBLIC ArrayStoreAll { std::unique_ptr<Node> d_value; }; /* class ArrayStoreAll */ -std::ostream& operator<<(std::ostream& out, - const ArrayStoreAll& asa) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const ArrayStoreAll& asa); /** * Hash function for the ArrayStoreAll constants. */ -struct CVC4_PUBLIC ArrayStoreAllHashFunction { +struct ArrayStoreAllHashFunction +{ size_t operator()(const ArrayStoreAll& asa) const; }; /* struct ArrayStoreAllHashFunction */ diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h index 9bf9b131a..66f376b18 100644 --- a/src/expr/ascription_type.h +++ b/src/expr/ascription_type.h @@ -33,7 +33,8 @@ class TypeNode; * AscriptionType payload. (Essentially, all of this is a way to * coerce a Type into the expression tree.) */ -class CVC4_PUBLIC AscriptionType { +class AscriptionType +{ public: AscriptionType(TypeNode t); ~AscriptionType(); @@ -46,17 +47,18 @@ class CVC4_PUBLIC AscriptionType { private: /** The type */ std::unique_ptr<TypeNode> d_type; -};/* class AscriptionType */ +}; /* class AscriptionType */ /** * A hash function for type ascription operators. */ -struct CVC4_PUBLIC AscriptionTypeHashFunction { +struct AscriptionTypeHashFunction +{ size_t operator()(const AscriptionType& at) const; -};/* struct AscriptionTypeHashFunction */ +}; /* struct AscriptionTypeHashFunction */ /** An output routine for AscriptionTypes */ -std::ostream& operator<<(std::ostream& out, AscriptionType at) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, AscriptionType at); }/* CVC4 namespace */ diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h index 32656b08c..6020759fb 100644 --- a/src/expr/datatype_index.h +++ b/src/expr/datatype_index.h @@ -22,7 +22,7 @@ namespace CVC4 { /* stores an index to Datatype residing in NodeManager */ -class CVC4_PUBLIC DatatypeIndexConstant +class DatatypeIndexConstant { public: DatatypeIndexConstant(unsigned index); @@ -57,10 +57,9 @@ class CVC4_PUBLIC DatatypeIndexConstant const unsigned d_index; }; /* class DatatypeIndexConstant */ -std::ostream& operator<<(std::ostream& out, - const DatatypeIndexConstant& dic) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic); -struct CVC4_PUBLIC DatatypeIndexConstantHashFunction +struct DatatypeIndexConstantHashFunction { size_t operator()(const DatatypeIndexConstant& dic) const; }; /* struct DatatypeIndexConstantHashFunction */ diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h index b7d348335..e9763108e 100644 --- a/src/expr/emptybag.h +++ b/src/expr/emptybag.h @@ -24,7 +24,7 @@ namespace CVC4 { class TypeNode; -class CVC4_PUBLIC EmptyBag +class EmptyBag { public: /** @@ -51,9 +51,9 @@ class CVC4_PUBLIC EmptyBag std::unique_ptr<TypeNode> d_type; }; /* class EmptyBag */ -std::ostream& operator<<(std::ostream& out, const EmptyBag& es) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const EmptyBag& es); -struct CVC4_PUBLIC EmptyBagHashFunction +struct EmptyBagHashFunction { size_t operator()(const EmptyBag& es) const; }; /* struct EmptyBagHashFunction */ diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h index 8bc0929e5..1c441e519 100644 --- a/src/expr/emptyset.h +++ b/src/expr/emptyset.h @@ -27,7 +27,7 @@ namespace CVC4 { class TypeNode; -class CVC4_PUBLIC EmptySet +class EmptySet { public: /** @@ -53,9 +53,9 @@ class CVC4_PUBLIC EmptySet std::unique_ptr<TypeNode> d_type; }; /* class EmptySet */ -std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const EmptySet& es); -struct CVC4_PUBLIC EmptySetHashFunction +struct EmptySetHashFunction { size_t operator()(const EmptySet& es) const; }; /* struct EmptySetHashFunction */ diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h index 5e29ce303..5306e2a2b 100644 --- a/src/expr/expr_iomanip.h +++ b/src/expr/expr_iomanip.h @@ -43,9 +43,9 @@ namespace expr { * allocated word in ios_base), and serves also as the manipulator * itself (as above). */ -class CVC4_PUBLIC ExprSetDepth { -public: - +class ExprSetDepth +{ + public: /** * Construct a ExprSetDepth with the given depth. */ @@ -89,13 +89,14 @@ public: * When this manipulator is used, the depth is stored here. */ long d_depth; -};/* class ExprSetDepth */ +}; /* class ExprSetDepth */ /** * IOStream manipulator to print expressions as a dag (or not). */ -class CVC4_PUBLIC ExprDag { -public: +class ExprDag +{ + public: /** * Construct a ExprDag with the given setting (dagification on or off). */ @@ -146,7 +147,7 @@ public: * When this manipulator is used, the setting is stored here. */ size_t d_dag; -};/* class ExprDag */ +}; /* class ExprDag */ /** * Sets the default dag setting when pretty-printing a Expr to an ostream. @@ -157,7 +158,7 @@ public: * * The setting stays permanently (until set again) with the stream. */ -std::ostream& operator<<(std::ostream& out, ExprDag d) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, ExprDag d); /** * Sets the default depth when pretty-printing a Expr to an ostream. @@ -168,7 +169,7 @@ std::ostream& operator<<(std::ostream& out, ExprDag d) CVC4_PUBLIC; * * The depth stays permanently (until set again) with the stream. */ -std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, ExprSetDepth sd); }/* namespace CVC4::expr */ diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 6d08279cc..ccb7656a9 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -27,13 +27,13 @@ namespace CVC4 { namespace kind { -enum CVC4_PUBLIC Kind_t { - UNDEFINED_KIND = -1, /**< undefined */ - NULL_EXPR, /**< Null kind */ -${kind_decls} - LAST_KIND /**< marks the upper-bound of this enumeration */ +enum Kind_t +{ + UNDEFINED_KIND = -1, /**< undefined */ + NULL_EXPR, /**< Null kind */ + ${kind_decls} LAST_KIND /**< marks the upper-bound of this enumeration */ -};/* enum Kind_t */ +}; /* enum Kind_t */ }/* CVC4::kind namespace */ @@ -61,14 +61,14 @@ const char* toString(CVC4::Kind k); * @param k The kind to write to the stream * @return The stream */ -std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, CVC4::Kind); /** Returns true if the given kind is associative. This is used by ExprManager to * decide whether it's safe to modify big expressions by changing the grouping of * the arguments. */ /* TODO: This could be generated. */ -bool isAssociative(::CVC4::Kind k) CVC4_PUBLIC; -std::string kindToString(::CVC4::Kind k) CVC4_PUBLIC; +bool isAssociative(::CVC4::Kind k); +std::string kindToString(::CVC4::Kind k); struct KindHashFunction { inline size_t operator()(::CVC4::Kind k) const { @@ -81,10 +81,9 @@ struct KindHashFunction { /** * The enumeration for the built-in atomic types. */ -enum CVC4_PUBLIC TypeConstant +enum TypeConstant { - ${type_constant_list} - LAST_TYPE + ${type_constant_list} LAST_TYPE }; /* enum TypeConstant */ /** @@ -100,9 +99,9 @@ std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant); namespace theory { -::CVC4::theory::TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC; +::CVC4::theory::TheoryId kindToTheoryId(::CVC4::Kind k); ::CVC4::theory::TheoryId typeConstantToTheoryId( - ::CVC4::TypeConstant typeConstant) CVC4_PUBLIC; + ::CVC4::TypeConstant typeConstant); }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/expr/record.h b/src/expr/record.h index cccbf625a..a9201fca3 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -34,7 +34,8 @@ class TypeNode; namespace CVC4 { // operators for record update -class CVC4_PUBLIC RecordUpdate { +class RecordUpdate +{ std::string d_field; public: @@ -42,15 +43,16 @@ class CVC4_PUBLIC RecordUpdate { std::string getField() const { return d_field; } bool operator==(const RecordUpdate& t) const { return d_field == t.d_field; } bool operator!=(const RecordUpdate& t) const { return d_field != t.d_field; } -};/* class RecordUpdate */ +}; /* class RecordUpdate */ -struct CVC4_PUBLIC RecordUpdateHashFunction { +struct RecordUpdateHashFunction +{ inline size_t operator()(const RecordUpdate& t) const { return std::hash<std::string>()(t.getField()); } -};/* struct RecordUpdateHashFunction */ +}; /* struct RecordUpdateHashFunction */ -std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, const RecordUpdate& t); using Record = std::vector<std::pair<std::string, TypeNode>>; diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 36f3b46bd..40ea44b34 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -22,6 +22,7 @@ #include <string> #include "api/cvc4cpp.h" +#include "cvc4_export.h" #include "expr/symbol_table.h" namespace CVC4 { @@ -34,7 +35,7 @@ namespace CVC4 { * Like SymbolTable, this class currently lives in src/expr/ since it uses * context-dependent data structures. */ -class CVC4_PUBLIC SymbolManager +class CVC4_EXPORT SymbolManager { public: SymbolManager(api::Solver* s); diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index cdfe3a6a3..297917120 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -24,6 +24,7 @@ #include <vector> #include "base/exception.h" +#include "cvc4_export.h" namespace CVC4 { @@ -33,14 +34,17 @@ class Sort; class Term; } // namespace api -class CVC4_PUBLIC ScopeException : public Exception {}; +class CVC4_EXPORT ScopeException : public Exception +{ +}; /** * A convenience class for handling scoped declarations. Implements the usual * nested scoping rules for declarations, with separate bindings for expressions * and types. */ -class CVC4_PUBLIC SymbolTable { +class CVC4_EXPORT SymbolTable +{ public: /** Create a symbol table. */ SymbolTable(); diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h index 93a9fc1c6..e7c0f9830 100644 --- a/src/expr/uninterpreted_constant.h +++ b/src/expr/uninterpreted_constant.h @@ -55,7 +55,7 @@ std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc); /** * Hash function for the BitVector constants. */ -struct CVC4_PUBLIC UninterpretedConstantHashFunction +struct UninterpretedConstantHashFunction { size_t operator()(const UninterpretedConstant& uc) const; }; /* struct UninterpretedConstantHashFunction */ diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index 9f6dbd753..8dd164120 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -22,16 +22,6 @@ #include <stddef.h> #include <stdint.h> -#if defined _WIN32 || defined __CYGWIN__ -# define CVC4_PUBLIC -#else /* !( defined _WIN32 || defined __CYGWIN__ ) */ -# if __GNUC__ >= 4 -# define CVC4_PUBLIC __attribute__ ((__visibility__("default"))) -# else /* !( __GNUC__ >= 4 ) */ -# define CVC4_PUBLIC -# endif /* __GNUC__ >= 4 */ -#endif /* defined _WIN32 || defined __CYGWIN__ */ - // CVC4_UNUSED is to mark something (e.g. local variable, function) // as being _possibly_ unused, so that the compiler generates no // warning about it. This might be the case for e.g. a variable @@ -42,14 +32,12 @@ # define CVC4_NORETURN __attribute__ ((__noreturn__)) # define CVC4_CONST_FUNCTION __attribute__ ((__const__)) # define CVC4_PURE_FUNCTION __attribute__ ((__pure__)) -# define CVC4_DEPRECATED __attribute__ ((__deprecated__)) # define CVC4_WARN_UNUSED_RESULT __attribute__ ((__warn_unused_result__)) #else /* ! __GNUC__ */ # define CVC4_UNUSED # define CVC4_NORETURN # define CVC4_CONST_FUNCTION # define CVC4_PURE_FUNCTION -# define CVC4_DEPRECATED # define CVC4_WARN_UNUSED_RESULT #endif /* __GNUC__ */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 88f23ec36..001da12db 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -36,7 +36,6 @@ #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "parser/parser_exception.h" #include "smt/command.h" #include "util/result.h" #include "util/statistics_registry.h" @@ -203,7 +202,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { bool status = true; if(opts.getInteractive() && inputFromStdin) { if(opts.getTearDownIncremental() > 0) { - throw OptionException( + throw Exception( "--tear-down-incremental doesn't work in interactive mode"); } if(!opts.wasSetByUserIncrementalSolving()) { diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 3739e2251..b3c54f580 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -37,7 +37,7 @@ namespace parser { class SymbolManager; -class CVC4_PUBLIC InteractiveShell +class InteractiveShell { const Options& d_options; std::istream& d_in; 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 */ diff --git a/src/parser/input.h b/src/parser/input.h index 10c53156e..f6be43028 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -19,12 +19,14 @@ #ifndef CVC4__PARSER__INPUT_H #define CVC4__PARSER__INPUT_H -#include <iostream> #include <stdio.h> + +#include <iostream> #include <string> #include <vector> #include "api/cvc4cpp.h" +#include "cvc4_export.h" #include "options/language.h" #include "parser/parser_exception.h" @@ -34,14 +36,15 @@ class Command; namespace parser { -class CVC4_PUBLIC InputStreamException : public Exception { +class InputStreamException : public Exception +{ public: InputStreamException(const std::string& msg); }; /** Wrapper around an input stream. */ -class CVC4_PUBLIC InputStream { - +class InputStream +{ /** The name of this input stream. */ std::string d_name; @@ -66,7 +69,7 @@ class CVC4_PUBLIC InputStream { /** Get the name of this input stream. */ const std::string getName() const; -};/* class InputStream */ +}; /* class InputStream */ class Parser; @@ -76,7 +79,8 @@ class Parser; * for the given input language and attach it to an input source of the * appropriate type. */ -class CVC4_PUBLIC Input { +class CVC4_EXPORT Input +{ friend class Parser; // for parseError, parseCommand, parseExpr friend class ParserBuilder; @@ -170,7 +174,7 @@ class CVC4_PUBLIC Input { /** Set the Parser object for this input. */ virtual void setParser(Parser& parser) = 0; -};/* class Input */ +}; /* class Input */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h index 762be1e36..e5de7c998 100644 --- a/src/parser/parse_op.h +++ b/src/parser/parse_op.h @@ -55,7 +55,7 @@ namespace CVC4 { * interpret this operator by converting the next parsed constant of type T2 to * an Array of type (Array T1 T2) over that constant. */ -struct CVC4_PUBLIC ParseOp +struct ParseOp { ParseOp(api::Kind k = api::NULL_EXPR) : d_kind(k) {} /** The kind associated with the parsed operator, if it exists */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 7789fd148..c2fad6656 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -24,6 +24,7 @@ #include <string> #include "api/cvc4cpp.h" +#include "cvc4_export.h" #include "expr/kind.h" #include "expr/symbol_manager.h" #include "expr/symbol_table.h" @@ -56,7 +57,7 @@ enum DeclarationCheck { * Returns a string representation of the given object (for * debugging). */ -inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check); inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) { switch(check) { case CHECK_NONE: @@ -84,7 +85,7 @@ enum SymbolType { * Returns a string representation of the given object (for * debugging). */ -inline std::ostream& operator<<(std::ostream& out, SymbolType type) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, SymbolType type); inline std::ostream& operator<<(std::ostream& out, SymbolType type) { switch(type) { case SYM_VARIABLE: @@ -101,7 +102,8 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) { * name of the file, line number and column information, and in-scope * declarations. */ -class CVC4_PUBLIC Parser { +class CVC4_EXPORT Parser +{ friend class ParserBuilder; private: @@ -769,7 +771,7 @@ public: * c1, c2, c3 are digits from 0 to 7. */ std::vector<unsigned> processAdHocStringEsc(const std::string& s); -};/* class Parser */ +}; /* class Parser */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 178bbc2d9..c5de761b8 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -21,6 +21,7 @@ #include <string> +#include "cvc4_export.h" #include "options/language.h" #include "parser/input.h" @@ -42,7 +43,8 @@ class Parser; * called any number of times on an instance and will generate a fresh * parser each time. */ -class CVC4_PUBLIC ParserBuilder { +class CVC4_EXPORT ParserBuilder +{ enum InputType { FILE_INPUT, LINE_BUFFERED_STREAM_INPUT, @@ -184,7 +186,7 @@ class CVC4_PUBLIC ParserBuilder { /** Set the parser to use the given logic string. */ ParserBuilder& withForcedLogic(const std::string& logic); -};/* class ParserBuilder */ +}; /* class ParserBuilder */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 4c6341d43..8b6bd3b50 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -24,11 +24,13 @@ #include <sstream> #include "base/exception.h" +#include "cvc4_export.h" namespace CVC4 { namespace parser { -class CVC4_PUBLIC ParserException : public Exception { +class CVC4_EXPORT ParserException : public Exception +{ public: // Constructors ParserException() : d_filename(), d_line(0), d_column(0) {} @@ -74,9 +76,10 @@ class CVC4_PUBLIC ParserException : public Exception { std::string d_filename; unsigned long d_line; unsigned long d_column; -};/* class ParserException */ +}; /* class ParserException */ -class CVC4_PUBLIC ParserEndOfFileException : public ParserException { +class ParserEndOfFileException : public ParserException +{ public: // Constructors same as ParserException's @@ -94,7 +97,7 @@ class CVC4_PUBLIC ParserEndOfFileException : public ParserException { { } -};/* class ParserEndOfFileException */ +}; /* class ParserEndOfFileException */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index b3ed72a4c..df2f9b967 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -140,7 +140,7 @@ public: CVC4::context::UserContext* userContext, ProofNodeManager* pnm, bool enableIncremental = false); - CVC4_PUBLIC virtual ~Solver(); + virtual ~Solver(); // Problem specification: // diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 5e348c1e7..f553746e6 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -47,7 +47,7 @@ class SimpSolver : public Solver { CVC4::context::UserContext* userContext, ProofNodeManager* pnm, bool enableIncremental = false); - CVC4_PUBLIC ~SimpSolver(); + ~SimpSolver(); // Problem specification: // diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index decf83634..d0810324a 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -63,7 +63,7 @@ class PropEngine /** * Destructor. */ - CVC4_PUBLIC ~PropEngine(); + ~PropEngine(); /** * Finish initialize. Call this after construction just before we are diff --git a/src/smt/command.h b/src/smt/command.h index f880cfc98..78e7c4071 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -28,6 +28,7 @@ #include <vector> #include "api/cvc4cpp.h" +#include "cvc4_export.h" #include "util/sexpr.h" namespace CVC4 { @@ -52,12 +53,12 @@ class Model; * @param sexpr the symbolic expression to convert * @return the symbolic expression as string */ -std::string sexprToString(api::Term sexpr); +std::string sexprToString(api::Term sexpr) CVC4_EXPORT; -std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command&) CVC4_EXPORT; +std::ostream& operator<<(std::ostream&, const Command*) CVC4_EXPORT; +std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_EXPORT; +std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC4_EXPORT; /** The status an SMT benchmark can have */ enum BenchmarkStatus @@ -70,7 +71,7 @@ enum BenchmarkStatus SMT_UNKNOWN }; /* enum BenchmarkStatus */ -std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) CVC4_EXPORT; /** * IOStream manipulator to print success messages or not. @@ -84,7 +85,7 @@ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) CVC4_PUBLIC; * prints a success message (in a manner appropriate for the current * output language). */ -class CVC4_PUBLIC CommandPrintSuccess +class CVC4_EXPORT CommandPrintSuccess { public: /** Construct a CommandPrintSuccess with the given setting. */ @@ -118,9 +119,9 @@ class CVC4_PUBLIC CommandPrintSuccess * The depth stays permanently (until set again) with the stream. */ std::ostream& operator<<(std::ostream& out, - CommandPrintSuccess cps) CVC4_PUBLIC; + CommandPrintSuccess cps) CVC4_EXPORT; -class CVC4_PUBLIC CommandStatus +class CVC4_EXPORT CommandStatus { protected: // shouldn't construct a CommandStatus (use a derived class) @@ -133,7 +134,7 @@ class CVC4_PUBLIC CommandStatus virtual CommandStatus& clone() const = 0; }; /* class CommandStatus */ -class CVC4_PUBLIC CommandSuccess : public CommandStatus +class CVC4_EXPORT CommandSuccess : public CommandStatus { static const CommandSuccess* s_instance; @@ -145,7 +146,7 @@ class CVC4_PUBLIC CommandSuccess : public CommandStatus } }; /* class CommandSuccess */ -class CVC4_PUBLIC CommandInterrupted : public CommandStatus +class CVC4_EXPORT CommandInterrupted : public CommandStatus { static const CommandInterrupted* s_instance; @@ -157,7 +158,7 @@ class CVC4_PUBLIC CommandInterrupted : public CommandStatus } }; /* class CommandInterrupted */ -class CVC4_PUBLIC CommandUnsupported : public CommandStatus +class CVC4_EXPORT CommandUnsupported : public CommandStatus { public: CommandStatus& clone() const override @@ -166,7 +167,7 @@ class CVC4_PUBLIC CommandUnsupported : public CommandStatus } }; /* class CommandSuccess */ -class CVC4_PUBLIC CommandFailure : public CommandStatus +class CVC4_EXPORT CommandFailure : public CommandStatus { std::string d_message; @@ -182,7 +183,7 @@ class CVC4_PUBLIC CommandFailure : public CommandStatus * for an unsat core in a place that is not immediately preceded by an * unsat/valid response. */ -class CVC4_PUBLIC CommandRecoverableFailure : public CommandStatus +class CVC4_EXPORT CommandRecoverableFailure : public CommandStatus { std::string d_message; @@ -195,7 +196,7 @@ class CVC4_PUBLIC CommandRecoverableFailure : public CommandStatus std::string getMessage() const { return d_message; } }; /* class CommandRecoverableFailure */ -class CVC4_PUBLIC Command +class CVC4_EXPORT Command { public: typedef CommandPrintSuccess printsuccess; @@ -282,7 +283,7 @@ class CVC4_PUBLIC Command * EmptyCommands are the residue of a command after the parser handles * them (and there's nothing left to do). */ -class CVC4_PUBLIC EmptyCommand : public Command +class CVC4_EXPORT EmptyCommand : public Command { public: EmptyCommand(std::string name = ""); @@ -300,7 +301,7 @@ class CVC4_PUBLIC EmptyCommand : public Command std::string d_name; }; /* class EmptyCommand */ -class CVC4_PUBLIC EchoCommand : public Command +class CVC4_EXPORT EchoCommand : public Command { public: EchoCommand(std::string output = ""); @@ -324,7 +325,7 @@ class CVC4_PUBLIC EchoCommand : public Command std::string d_output; }; /* class EchoCommand */ -class CVC4_PUBLIC AssertCommand : public Command +class CVC4_EXPORT AssertCommand : public Command { protected: api::Term d_term; @@ -346,7 +347,7 @@ class CVC4_PUBLIC AssertCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class AssertCommand */ -class CVC4_PUBLIC PushCommand : public Command +class CVC4_EXPORT PushCommand : public Command { public: void invoke(api::Solver* solver, SymbolManager* sm) override; @@ -359,7 +360,7 @@ class CVC4_PUBLIC PushCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class PushCommand */ -class CVC4_PUBLIC PopCommand : public Command +class CVC4_EXPORT PopCommand : public Command { public: void invoke(api::Solver* solver, SymbolManager* sm) override; @@ -372,7 +373,7 @@ class CVC4_PUBLIC PopCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class PopCommand */ -class CVC4_PUBLIC DeclarationDefinitionCommand : public Command +class CVC4_EXPORT DeclarationDefinitionCommand : public Command { protected: std::string d_symbol; @@ -384,7 +385,7 @@ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command std::string getSymbol() const; }; /* class DeclarationDefinitionCommand */ -class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand +class CVC4_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand { protected: api::Term d_func; @@ -405,7 +406,7 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareFunctionCommand */ -class CVC4_PUBLIC DeclareSortCommand : public DeclarationDefinitionCommand +class CVC4_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand { protected: size_t d_arity; @@ -427,7 +428,7 @@ class CVC4_PUBLIC DeclareSortCommand : public DeclarationDefinitionCommand OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareSortCommand */ -class CVC4_PUBLIC DefineSortCommand : public DeclarationDefinitionCommand +class CVC4_EXPORT DefineSortCommand : public DeclarationDefinitionCommand { protected: std::vector<api::Sort> d_params; @@ -452,7 +453,7 @@ class CVC4_PUBLIC DefineSortCommand : public DeclarationDefinitionCommand OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DefineSortCommand */ -class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand +class CVC4_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand { public: DefineFunctionCommand(const std::string& id, @@ -497,7 +498,7 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand * This command will assert a set of quantified formulas that specify * the (mutually recursive) function definitions provided to it. */ -class CVC4_PUBLIC DefineFunctionRecCommand : public Command +class CVC4_EXPORT DefineFunctionRecCommand : public Command { public: DefineFunctionRecCommand(api::Term func, @@ -542,7 +543,7 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command * (declare-heap (T U)) * where T is the location sort and U is the data sort. */ -class CVC4_PUBLIC DeclareHeapCommand : public Command +class CVC4_EXPORT DeclareHeapCommand : public Command { public: DeclareHeapCommand(api::Sort locSort, api::Sort dataSort); @@ -568,7 +569,7 @@ class CVC4_PUBLIC DeclareHeapCommand : public Command * The command when an attribute is set by a user. In SMT-LIBv2 this is done * via the syntax (! expr :attr) */ -class CVC4_PUBLIC SetUserAttributeCommand : public Command +class CVC4_EXPORT SetUserAttributeCommand : public Command { public: SetUserAttributeCommand(const std::string& attr, api::Term term); @@ -604,7 +605,7 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command * The command when parsing check-sat. * This command will check satisfiability of the input formula. */ -class CVC4_PUBLIC CheckSatCommand : public Command +class CVC4_EXPORT CheckSatCommand : public Command { public: CheckSatCommand(); @@ -632,7 +633,7 @@ class CVC4_PUBLIC CheckSatCommand : public Command * This command will assume a set of formulas and check satisfiability of the * input formula under these assumptions. */ -class CVC4_PUBLIC CheckSatAssumingCommand : public Command +class CVC4_EXPORT CheckSatAssumingCommand : public Command { public: CheckSatAssumingCommand(api::Term term); @@ -655,7 +656,7 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command api::Result d_result; }; /* class CheckSatAssumingCommand */ -class CVC4_PUBLIC QueryCommand : public Command +class CVC4_EXPORT QueryCommand : public Command { protected: api::Term d_term; @@ -681,7 +682,7 @@ class CVC4_PUBLIC QueryCommand : public Command /* ------------------- sygus commands ------------------ */ /** Declares a sygus universal variable */ -class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand +class CVC4_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand { public: DeclareSygusVarCommand(const std::string& id, api::Term var, api::Sort sort); @@ -718,7 +719,7 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand * This command is also used for the special case in which we are declaring an * invariant-to-synthesize */ -class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand +class CVC4_EXPORT SynthFunCommand : public DeclarationDefinitionCommand { public: SynthFunCommand(const std::string& id, @@ -769,7 +770,7 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand }; /** Declares a sygus constraint */ -class CVC4_PUBLIC SygusConstraintCommand : public Command +class CVC4_EXPORT SygusConstraintCommand : public Command { public: SygusConstraintCommand(const api::Term& t); @@ -807,7 +808,7 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command * than the precondition, not weaker than the postcondition and inductive * w.r.t. the transition relation. */ -class CVC4_PUBLIC SygusInvConstraintCommand : public Command +class CVC4_EXPORT SygusInvConstraintCommand : public Command { public: SygusInvConstraintCommand(const std::vector<api::Term>& predicates); @@ -843,7 +844,7 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command }; /** Declares a synthesis conjecture */ -class CVC4_PUBLIC CheckSynthCommand : public Command +class CVC4_EXPORT CheckSynthCommand : public Command { public: CheckSynthCommand(){}; @@ -881,7 +882,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command /* ------------------- sygus commands ------------------ */ // this is TRANSFORM in the CVC presentation language -class CVC4_PUBLIC SimplifyCommand : public Command +class CVC4_EXPORT SimplifyCommand : public Command { protected: api::Term d_term; @@ -903,7 +904,7 @@ class CVC4_PUBLIC SimplifyCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SimplifyCommand */ -class CVC4_PUBLIC GetValueCommand : public Command +class CVC4_EXPORT GetValueCommand : public Command { protected: std::vector<api::Term> d_terms; @@ -926,7 +927,7 @@ class CVC4_PUBLIC GetValueCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetValueCommand */ -class CVC4_PUBLIC GetAssignmentCommand : public Command +class CVC4_EXPORT GetAssignmentCommand : public Command { protected: SExpr d_result; @@ -946,7 +947,7 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetAssignmentCommand */ -class CVC4_PUBLIC GetModelCommand : public Command +class CVC4_EXPORT GetModelCommand : public Command { public: GetModelCommand(); @@ -968,7 +969,7 @@ class CVC4_PUBLIC GetModelCommand : public Command }; /* class GetModelCommand */ /** The command to block models. */ -class CVC4_PUBLIC BlockModelCommand : public Command +class CVC4_EXPORT BlockModelCommand : public Command { public: BlockModelCommand(); @@ -984,7 +985,7 @@ class CVC4_PUBLIC BlockModelCommand : public Command }; /* class BlockModelCommand */ /** The command to block model values. */ -class CVC4_PUBLIC BlockModelValuesCommand : public Command +class CVC4_EXPORT BlockModelValuesCommand : public Command { public: BlockModelValuesCommand(const std::vector<api::Term>& terms); @@ -1004,7 +1005,7 @@ class CVC4_PUBLIC BlockModelValuesCommand : public Command std::vector<api::Term> d_terms; }; /* class BlockModelValuesCommand */ -class CVC4_PUBLIC GetProofCommand : public Command +class CVC4_EXPORT GetProofCommand : public Command { public: GetProofCommand(); @@ -1026,7 +1027,7 @@ class CVC4_PUBLIC GetProofCommand : public Command std::string d_result; }; /* class GetProofCommand */ -class CVC4_PUBLIC GetInstantiationsCommand : public Command +class CVC4_EXPORT GetInstantiationsCommand : public Command { public: GetInstantiationsCommand(); @@ -1045,7 +1046,7 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command api::Solver* d_solver; }; /* class GetInstantiationsCommand */ -class CVC4_PUBLIC GetSynthSolutionCommand : public Command +class CVC4_EXPORT GetSynthSolutionCommand : public Command { public: GetSynthSolutionCommand(); @@ -1073,7 +1074,7 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command * find a predicate P, then the output response of this command is: (define-fun * s () Bool P) */ -class CVC4_PUBLIC GetInterpolCommand : public Command +class CVC4_EXPORT GetInterpolCommand : public Command { public: GetInterpolCommand(const std::string& name, api::Term conj); @@ -1123,7 +1124,7 @@ class CVC4_PUBLIC GetInterpolCommand : public Command * A grammar G can be optionally provided to indicate the syntactic restrictions * on the possible solutions returned. */ -class CVC4_PUBLIC GetAbductCommand : public Command +class CVC4_EXPORT GetAbductCommand : public Command { public: GetAbductCommand(const std::string& name, api::Term conj); @@ -1162,7 +1163,7 @@ class CVC4_PUBLIC GetAbductCommand : public Command api::Term d_result; }; /* class GetAbductCommand */ -class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command +class CVC4_EXPORT GetQuantifierEliminationCommand : public Command { protected: api::Term d_term; @@ -1188,7 +1189,7 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetQuantifierEliminationCommand */ -class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command +class CVC4_EXPORT GetUnsatAssumptionsCommand : public Command { public: GetUnsatAssumptionsCommand(); @@ -1207,7 +1208,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command std::vector<api::Term> d_result; }; /* class GetUnsatAssumptionsCommand */ -class CVC4_PUBLIC GetUnsatCoreCommand : public Command +class CVC4_EXPORT GetUnsatCoreCommand : public Command { public: GetUnsatCoreCommand(); @@ -1231,7 +1232,7 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command std::vector<api::Term> d_result; }; /* class GetUnsatCoreCommand */ -class CVC4_PUBLIC GetAssertionsCommand : public Command +class CVC4_EXPORT GetAssertionsCommand : public Command { protected: std::string d_result; @@ -1251,7 +1252,7 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetAssertionsCommand */ -class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command +class CVC4_EXPORT SetBenchmarkStatusCommand : public Command { protected: BenchmarkStatus d_status; @@ -1271,7 +1272,7 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetBenchmarkStatusCommand */ -class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command +class CVC4_EXPORT SetBenchmarkLogicCommand : public Command { protected: std::string d_logic; @@ -1290,7 +1291,7 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetBenchmarkLogicCommand */ -class CVC4_PUBLIC SetInfoCommand : public Command +class CVC4_EXPORT SetInfoCommand : public Command { protected: std::string d_flag; @@ -1312,7 +1313,7 @@ class CVC4_PUBLIC SetInfoCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetInfoCommand */ -class CVC4_PUBLIC GetInfoCommand : public Command +class CVC4_EXPORT GetInfoCommand : public Command { protected: std::string d_flag; @@ -1335,7 +1336,7 @@ class CVC4_PUBLIC GetInfoCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetInfoCommand */ -class CVC4_PUBLIC SetOptionCommand : public Command +class CVC4_EXPORT SetOptionCommand : public Command { protected: std::string d_flag; @@ -1357,7 +1358,7 @@ class CVC4_PUBLIC SetOptionCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetOptionCommand */ -class CVC4_PUBLIC GetOptionCommand : public Command +class CVC4_EXPORT GetOptionCommand : public Command { protected: std::string d_flag; @@ -1380,7 +1381,7 @@ class CVC4_PUBLIC GetOptionCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetOptionCommand */ -class CVC4_PUBLIC DatatypeDeclarationCommand : public Command +class CVC4_EXPORT DatatypeDeclarationCommand : public Command { private: std::vector<api::Sort> d_datatypes; @@ -1400,7 +1401,7 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DatatypeDeclarationCommand */ -class CVC4_PUBLIC ResetCommand : public Command +class CVC4_EXPORT ResetCommand : public Command { public: ResetCommand() {} @@ -1414,7 +1415,7 @@ class CVC4_PUBLIC ResetCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class ResetCommand */ -class CVC4_PUBLIC ResetAssertionsCommand : public Command +class CVC4_EXPORT ResetAssertionsCommand : public Command { public: ResetAssertionsCommand() {} @@ -1428,7 +1429,7 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class ResetAssertionsCommand */ -class CVC4_PUBLIC QuitCommand : public Command +class CVC4_EXPORT QuitCommand : public Command { public: QuitCommand() {} @@ -1442,7 +1443,7 @@ class CVC4_PUBLIC QuitCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class QuitCommand */ -class CVC4_PUBLIC CommentCommand : public Command +class CVC4_EXPORT CommentCommand : public Command { std::string d_comment; @@ -1461,7 +1462,7 @@ class CVC4_PUBLIC CommentCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class CommentCommand */ -class CVC4_PUBLIC CommandSequence : public Command +class CVC4_EXPORT CommandSequence : public Command { protected: /** All the commands to be executed (in sequence) */ @@ -1499,7 +1500,7 @@ class CVC4_PUBLIC CommandSequence : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class CommandSequence */ -class CVC4_PUBLIC DeclarationSequence : public CommandSequence +class CVC4_EXPORT DeclarationSequence : public CommandSequence { void toStream( std::ostream& out, diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index d58dda1ce..bb0bff1d7 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -55,7 +55,7 @@ CVC4dumpstream& CVC4dumpstream::operator<<(const NodeCommand& nc) #endif /* CVC4_DUMPING && !CVC4_MUZZLE */ -DumpC DumpChannel CVC4_PUBLIC; +DumpC DumpChannel; std::ostream& DumpC::setStream(std::ostream* os) { ::CVC4::DumpOutChannel.setStream(os); diff --git a/src/smt/dump.h b/src/smt/dump.h index d1cb37035..d8c2e5b4e 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -28,7 +28,7 @@ class NodeCommand; #if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) -class CVC4_PUBLIC CVC4dumpstream +class CVC4dumpstream { public: CVC4dumpstream() : d_os(nullptr) {} @@ -53,7 +53,7 @@ class CVC4_PUBLIC CVC4dumpstream * Dummy implementation of the dump stream when dumping is disabled or the * build is muzzled. */ -class CVC4_PUBLIC CVC4dumpstream +class CVC4dumpstream { public: CVC4dumpstream() {} @@ -65,7 +65,7 @@ class CVC4_PUBLIC CVC4dumpstream #endif /* CVC4_DUMPING && !CVC4_MUZZLE */ /** The dump class */ -class CVC4_PUBLIC DumpC +class DumpC { public: CVC4dumpstream operator()(const char* tag) { @@ -108,7 +108,7 @@ class CVC4_PUBLIC DumpC };/* class DumpC */ /** The dump singleton */ -extern DumpC DumpChannel CVC4_PUBLIC; +extern DumpC DumpChannel; #define Dump ::CVC4::DumpChannel diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h index c3eadb517..bb1d274ae 100644 --- a/src/smt/logic_exception.h +++ b/src/smt/logic_exception.h @@ -26,7 +26,8 @@ namespace CVC4 { -class CVC4_PUBLIC LogicException : public CVC4::Exception { +class LogicException : public CVC4::Exception +{ public: LogicException() : Exception("Feature used while operating in " @@ -40,7 +41,7 @@ class CVC4_PUBLIC LogicException : public CVC4::Exception { LogicException(const char* msg) : Exception(msg) { } -};/* class LogicException */ +}; /* class LogicException */ }/* CVC4 namespace */ diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index f69bd1502..6117b9df5 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -33,7 +33,7 @@ namespace smt { * * Represents whether an objective should be minimized or maximized */ -enum CVC4_PUBLIC ObjectiveType +enum ObjectiveType { OBJECTIVE_MINIMIZE, OBJECTIVE_MAXIMIZE, @@ -46,7 +46,7 @@ enum CVC4_PUBLIC ObjectiveType * Represents the result of a checkopt query * (unimplemented) OPT_OPTIMAL: if value was found */ -enum CVC4_PUBLIC OptResult +enum OptResult { // the original set of assertions has result UNKNOWN OPT_UNKNOWN, diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 56f3ffbb8..744320950 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -25,6 +25,7 @@ #include <vector> #include "context/cdhashmap_forward.h" +#include "cvc4_export.h" #include "options/options.h" #include "smt/output_manager.h" #include "smt/smt_mode.h" @@ -122,7 +123,7 @@ namespace theory { /* -------------------------------------------------------------------------- */ -class CVC4_PUBLIC SmtEngine +class CVC4_EXPORT SmtEngine { friend class ::CVC4::api::Solver; friend class ::CVC4::smt::SmtEngineState; @@ -246,7 +247,7 @@ class CVC4_PUBLIC SmtEngine * to a state where its options were prior to parsing but after e.g. * reading command line options. */ - void notifyStartParsing(std::string filename); + void notifyStartParsing(std::string filename) CVC4_EXPORT; /** return the input name (if any) */ const std::string& getFilename() const; 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. 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 */ |