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.
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
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)
$<INSTALL_INTERFACE:include>
)
+include(GenerateExportHeader)
+generate_export_header(cvc4)
+
install(TARGETS cvc4
EXPORT cvc4-targets
LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
DESTINATION
${CMAKE_INSTALL_INCLUDEDIR}/cvc4/api)
install(FILES
- include/cvc4_public.h
+ ${CMAKE_CURRENT_BINARY_DIR}/cvc4_export.h
DESTINATION
${CMAKE_INSTALL_INCLUDEDIR}/cvc4/)
** The CVC4 C++ API.
**/
-#include "cvc4_public.h"
+#include "cvc4_export.h"
#ifndef CVC4__API__CVC4CPP_H
#define CVC4__API__CVC4CPP_H
/* Exception */
/* -------------------------------------------------------------------------- */
-class CVC4_PUBLIC CVC4ApiException : public std::exception
+class CVC4_EXPORT CVC4ApiException : public std::exception
{
public:
CVC4ApiException(const std::string& str) : d_msg(str) {}
std::string d_msg;
};
-class CVC4_PUBLIC CVC4ApiRecoverableException : public CVC4ApiException
+class CVC4_EXPORT CVC4ApiRecoverableException : public CVC4ApiException
{
public:
CVC4ApiRecoverableException(const std::string& str) : CVC4ApiException(str) {}
/**
* Encapsulation of a three-valued solver result, with explanations.
*/
-class CVC4_PUBLIC Result
+class CVC4_EXPORT Result
{
friend class Solver;
* @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.
* @return the output stream
*/
std::ostream& operator<<(std::ostream& out,
- enum Result::UnknownExplanation e) CVC4_PUBLIC;
+ enum Result::UnknownExplanation e) CVC4_EXPORT;
/* -------------------------------------------------------------------------- */
/* Sort */
/**
* The sort of a CVC4 term.
*/
-class CVC4_PUBLIC Sort
+class CVC4_EXPORT Sort
{
friend class CVC4::DatatypeDeclarationCommand;
friend class CVC4::DeclareFunctionCommand;
* @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;
};
* 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;
/**
* A CVC4 Term.
*/
-class CVC4_PUBLIC Term
+class CVC4_EXPORT Term
{
friend class CVC4::AssertCommand;
friend class CVC4::BlockModelValuesCommand;
/**
* Hash function for Terms.
*/
-struct CVC4_PUBLIC TermHashFunction
+struct CVC4_EXPORT TermHashFunction
{
size_t operator()(const Term& t) const;
};
* @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.
* @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.
* @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.
*/
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.
*/
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.
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.
* @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;
};
/**
* A CVC4 datatype constructor declaration.
*/
-class CVC4_PUBLIC DatatypeConstructorDecl
+class CVC4_EXPORT DatatypeConstructorDecl
{
friend class DatatypeDecl;
friend class Solver;
/**
* A CVC4 datatype declaration.
*/
-class CVC4_PUBLIC DatatypeDecl
+class CVC4_EXPORT DatatypeDecl
{
friend class DatatypeConstructorArg;
friend class Solver;
/**
* A CVC4 datatype selector.
*/
-class CVC4_PUBLIC DatatypeSelector
+class CVC4_EXPORT DatatypeSelector
{
friend class DatatypeConstructor;
friend class Solver;
/**
* A CVC4 datatype constructor.
*/
-class CVC4_PUBLIC DatatypeConstructor
+class CVC4_EXPORT DatatypeConstructor
{
friend class Datatype;
friend class Solver;
/*
* A CVC4 datatype.
*/
-class CVC4_PUBLIC Datatype
+class CVC4_EXPORT Datatype
{
friend class Solver;
friend class Sort;
* @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.
* @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.
* @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.
* @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.
* @return the output stream
*/
std::ostream& operator<<(std::ostream& out,
- const DatatypeSelector& stor) CVC4_PUBLIC;
+ const DatatypeSelector& stor) CVC4_EXPORT;
/* -------------------------------------------------------------------------- */
/* Grammar */
/**
* A Sygus Grammar.
*/
-class CVC4_PUBLIC Grammar
+class CVC4_EXPORT Grammar
{
friend class CVC4::GetAbductCommand;
friend class CVC4::GetInterpolCommand;
* @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 */
/**
* A CVC4 floating point rounding mode.
*/
-enum CVC4_PUBLIC RoundingMode
+enum CVC4_EXPORT RoundingMode
{
ROUND_NEAREST_TIES_TO_EVEN,
ROUND_TOWARD_POSITIVE,
/**
* Hash function for RoundingModes.
*/
-struct CVC4_PUBLIC RoundingModeHashFunction
+struct CVC4_EXPORT RoundingModeHashFunction
{
inline size_t operator()(const RoundingMode& rm) const;
};
/*
* A CVC4 solver.
*/
-class CVC4_PUBLIC Solver
+class CVC4_EXPORT Solver
{
friend class Datatype;
friend class DatatypeDecl;
** 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
* 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.
* @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.
* @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;
};
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)
NL = '\n'
#################### Enum Declarations ################
-ENUM_START = 'enum CVC4_PUBLIC Kind'
+ENUM_START = 'enum CVC4_EXPORT Kind'
ENUM_END = CCB+SC
################ Comments and Macro Tokens ############
#include <ostream>
#include "base/exception.h"
+#include "cvc4_export.h"
// Define CVC4_NO_RETURN macro replacement for [[noreturn]].
#if defined(SWIG)
// 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);
#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();
static std::string getCompiler();
static std::string getCompiledDateTime();
-};/* class Configuration */
+}; /* class Configuration */
}/* CVC4 namespace */
#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;
*/
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,
*/
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();
*
* The interface provides a notify() function.
*/
-class CVC4_PUBLIC Listener {
-public:
+class Listener
+{
+ public:
Listener();
virtual ~Listener();
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") {
ModalException(const char* msg) :
Exception(msg) {
}
-};/* class ModalException */
+}; /* class ModalException */
/**
* Special case of ModalException that allows the execution of the solver to
* 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) {}
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 */
#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) {
* 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;
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&)) {
CVC4ostream& operator<<(CVC4ostream& (*pf)(CVC4ostream&)) {
return pf(*this);
}
-};/* class CVC4ostream */
+}; /* class CVC4ostream */
inline CVC4ostream& push(CVC4ostream& stream) {
stream.pushIndent();
* 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;
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;
return true;
}
-};/* class WarningC */
+}; /* class WarningC */
/** The message output class */
-class CVC4_PUBLIC MessageC {
+class MessageC
+{
std::ostream* d_os;
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:
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:
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;
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;
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
#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
-class CVC4_PUBLIC ScopedDebug {
+class ScopedDebug
+{
std::string d_tag;
bool d_oldSetting;
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;
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 */
* 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; }
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
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 */
* 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();
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 */
namespace CVC4 {
/* stores an index to Datatype residing in NodeManager */
-class CVC4_PUBLIC DatatypeIndexConstant
+class DatatypeIndexConstant
{
public:
DatatypeIndexConstant(unsigned index);
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 */
class TypeNode;
-class CVC4_PUBLIC EmptyBag
+class EmptyBag
{
public:
/**
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 */
class TypeNode;
-class CVC4_PUBLIC EmptySet
+class EmptySet
{
public:
/**
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 */
* 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.
*/
* 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).
*/
* 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.
*
* 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.
*
* 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 */
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 */
* @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 {
/**
* 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 */
/**
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 */
namespace CVC4 {
// operators for record update
-class CVC4_PUBLIC RecordUpdate {
+class RecordUpdate
+{
std::string d_field;
public:
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>>;
#include <string>
#include "api/cvc4cpp.h"
+#include "cvc4_export.h"
#include "expr/symbol_table.h"
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);
#include <vector>
#include "base/exception.h"
+#include "cvc4_export.h"
namespace CVC4 {
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();
/**
* Hash function for the BitVector constants.
*/
-struct CVC4_PUBLIC UninterpretedConstantHashFunction
+struct UninterpretedConstantHashFunction
{
size_t operator()(const UninterpretedConstant& uc) const;
}; /* struct UninterpretedConstantHashFunction */
#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
# 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__ */
#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"
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()) {
class SymbolManager;
-class CVC4_PUBLIC InteractiveShell
+class InteractiveShell
{
const Options& d_options;
std::istream& d_in;
#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
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:
namespace output {
-enum CVC4_PUBLIC Language
+enum CVC4_EXPORT Language
{
// SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
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;
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 */
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 = \
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}::";
#define CVC4__OPTION_EXCEPTION_H
#include "base/exception.h"
+#include "cvc4_export.h"
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) {}
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") {
UnrecognizedOptionException(const std::string& msg) :
CVC4::OptionException("Unrecognized informational or option key or setting: " + msg) {
}
-};/* class UnrecognizedOptionException */
+}; /* class UnrecognizedOptionException */
}/* CVC4 namespace */
#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"
class OptionsListener;
-class CVC4_PUBLIC Options {
+class CVC4_EXPORT Options
+{
friend api::Solver;
/** The struct that holds all option values. */
options::OptionsHolder* d_holder;
static const unsigned s_preemptAdditional = 6;
public:
- class CVC4_PUBLIC OptionsScope {
+ class OptionsScope
+ {
private:
Options* d_oldOptions;
public:
~OptionsScope(){
Options::s_current = d_oldOptions;
}
- };
+ };
/** Return true if current Options are null */
static inline bool isCurrentNull() {
int argc,
char* argv[],
std::vector<std::string>* nonoptions);
-};/* class Options */
+}; /* class Options */
}/* CVC4 namespace */
/** 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,
} // namespace options
-std::ostream& operator<<(std::ostream& out,
- options::InstFormatMode mode) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, options::InstFormatMode mode);
} // namespace CVC4
#define CVC4__OPTIONS__SET_LANGUAGE_H
#include <iostream>
+
+#include "cvc4_export.h"
#include "options/language.h"
namespace CVC4 {
/**
* 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
* 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.
*
* 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 */
#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"
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;
/** Get the name of this input stream. */
const std::string getName() const;
-};/* class InputStream */
+}; /* class InputStream */
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;
/** Set the Parser object for this input. */
virtual void setParser(Parser& parser) = 0;
-};/* class Input */
+}; /* class Input */
}/* CVC4::parser namespace */
}/* CVC4 namespace */
* 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 */
#include <string>
#include "api/cvc4cpp.h"
+#include "cvc4_export.h"
#include "expr/kind.h"
#include "expr/symbol_manager.h"
#include "expr/symbol_table.h"
* 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:
* 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:
* 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:
* 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 */
#include <string>
+#include "cvc4_export.h"
#include "options/language.h"
#include "parser/input.h"
* 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,
/** Set the parser to use the given logic string. */
ParserBuilder& withForcedLogic(const std::string& logic);
-};/* class ParserBuilder */
+}; /* class ParserBuilder */
}/* CVC4::parser namespace */
}/* CVC4 namespace */
#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) {}
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
{
}
-};/* class ParserEndOfFileException */
+}; /* class ParserEndOfFileException */
}/* CVC4::parser namespace */
}/* CVC4 namespace */
CVC4::context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental = false);
- CVC4_PUBLIC virtual ~Solver();
+ virtual ~Solver();
// Problem specification:
//
CVC4::context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental = false);
- CVC4_PUBLIC ~SimpSolver();
+ ~SimpSolver();
// Problem specification:
//
/**
* Destructor.
*/
- CVC4_PUBLIC ~PropEngine();
+ ~PropEngine();
/**
* Finish initialize. Call this after construction just before we are
#include <vector>
#include "api/cvc4cpp.h"
+#include "cvc4_export.h"
#include "util/sexpr.h"
namespace CVC4 {
* @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
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.
* 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. */
* 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)
virtual CommandStatus& clone() const = 0;
}; /* class CommandStatus */
-class CVC4_PUBLIC CommandSuccess : public CommandStatus
+class CVC4_EXPORT CommandSuccess : public CommandStatus
{
static const CommandSuccess* s_instance;
}
}; /* class CommandSuccess */
-class CVC4_PUBLIC CommandInterrupted : public CommandStatus
+class CVC4_EXPORT CommandInterrupted : public CommandStatus
{
static const CommandInterrupted* s_instance;
}
}; /* class CommandInterrupted */
-class CVC4_PUBLIC CommandUnsupported : public CommandStatus
+class CVC4_EXPORT CommandUnsupported : public CommandStatus
{
public:
CommandStatus& clone() const override
}
}; /* class CommandSuccess */
-class CVC4_PUBLIC CommandFailure : public CommandStatus
+class CVC4_EXPORT CommandFailure : public CommandStatus
{
std::string d_message;
* 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;
std::string getMessage() const { return d_message; }
}; /* class CommandRecoverableFailure */
-class CVC4_PUBLIC Command
+class CVC4_EXPORT Command
{
public:
typedef CommandPrintSuccess printsuccess;
* 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 = "");
std::string d_name;
}; /* class EmptyCommand */
-class CVC4_PUBLIC EchoCommand : public Command
+class CVC4_EXPORT EchoCommand : public Command
{
public:
EchoCommand(std::string output = "");
std::string d_output;
}; /* class EchoCommand */
-class CVC4_PUBLIC AssertCommand : public Command
+class CVC4_EXPORT AssertCommand : public Command
{
protected:
api::Term d_term;
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;
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;
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;
std::string getSymbol() const;
}; /* class DeclarationDefinitionCommand */
-class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand
+class CVC4_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand
{
protected:
api::Term d_func;
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;
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;
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,
* 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,
* (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);
* 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);
* 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();
* 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);
api::Result d_result;
}; /* class CheckSatAssumingCommand */
-class CVC4_PUBLIC QueryCommand : public Command
+class CVC4_EXPORT QueryCommand : public Command
{
protected:
api::Term d_term;
/* ------------------- 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);
* 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,
};
/** Declares a sygus constraint */
-class CVC4_PUBLIC SygusConstraintCommand : public Command
+class CVC4_EXPORT SygusConstraintCommand : public Command
{
public:
SygusConstraintCommand(const api::Term& t);
* 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);
};
/** Declares a synthesis conjecture */
-class CVC4_PUBLIC CheckSynthCommand : public Command
+class CVC4_EXPORT CheckSynthCommand : public Command
{
public:
CheckSynthCommand(){};
/* ------------------- 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;
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;
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;
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetAssignmentCommand */
-class CVC4_PUBLIC GetModelCommand : public Command
+class CVC4_EXPORT GetModelCommand : public Command
{
public:
GetModelCommand();
}; /* class GetModelCommand */
/** The command to block models. */
-class CVC4_PUBLIC BlockModelCommand : public Command
+class CVC4_EXPORT BlockModelCommand : public Command
{
public:
BlockModelCommand();
}; /* 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);
std::vector<api::Term> d_terms;
}; /* class BlockModelValuesCommand */
-class CVC4_PUBLIC GetProofCommand : public Command
+class CVC4_EXPORT GetProofCommand : public Command
{
public:
GetProofCommand();
std::string d_result;
}; /* class GetProofCommand */
-class CVC4_PUBLIC GetInstantiationsCommand : public Command
+class CVC4_EXPORT GetInstantiationsCommand : public Command
{
public:
GetInstantiationsCommand();
api::Solver* d_solver;
}; /* class GetInstantiationsCommand */
-class CVC4_PUBLIC GetSynthSolutionCommand : public Command
+class CVC4_EXPORT GetSynthSolutionCommand : public Command
{
public:
GetSynthSolutionCommand();
* 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);
* 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);
api::Term d_result;
}; /* class GetAbductCommand */
-class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
+class CVC4_EXPORT GetQuantifierEliminationCommand : public Command
{
protected:
api::Term d_term;
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class GetQuantifierEliminationCommand */
-class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
+class CVC4_EXPORT GetUnsatAssumptionsCommand : public Command
{
public:
GetUnsatAssumptionsCommand();
std::vector<api::Term> d_result;
}; /* class GetUnsatAssumptionsCommand */
-class CVC4_PUBLIC GetUnsatCoreCommand : public Command
+class CVC4_EXPORT GetUnsatCoreCommand : public Command
{
public:
GetUnsatCoreCommand();
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;
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;
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;
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;
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;
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;
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;
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;
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class DatatypeDeclarationCommand */
-class CVC4_PUBLIC ResetCommand : public Command
+class CVC4_EXPORT ResetCommand : public Command
{
public:
ResetCommand() {}
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class ResetCommand */
-class CVC4_PUBLIC ResetAssertionsCommand : public Command
+class CVC4_EXPORT ResetAssertionsCommand : public Command
{
public:
ResetAssertionsCommand() {}
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class ResetAssertionsCommand */
-class CVC4_PUBLIC QuitCommand : public Command
+class CVC4_EXPORT QuitCommand : public Command
{
public:
QuitCommand() {}
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;
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) */
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,
#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
-DumpC DumpChannel CVC4_PUBLIC;
+DumpC DumpChannel;
std::ostream& DumpC::setStream(std::ostream* os) {
::CVC4::DumpOutChannel.setStream(os);
#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE)
-class CVC4_PUBLIC CVC4dumpstream
+class CVC4dumpstream
{
public:
CVC4dumpstream() : d_os(nullptr) {}
* Dummy implementation of the dump stream when dumping is disabled or the
* build is muzzled.
*/
-class CVC4_PUBLIC CVC4dumpstream
+class CVC4dumpstream
{
public:
CVC4dumpstream() {}
#endif /* CVC4_DUMPING && !CVC4_MUZZLE */
/** The dump class */
-class CVC4_PUBLIC DumpC
+class DumpC
{
public:
CVC4dumpstream operator()(const char* tag) {
};/* class DumpC */
/** The dump singleton */
-extern DumpC DumpChannel CVC4_PUBLIC;
+extern DumpC DumpChannel;
#define Dump ::CVC4::DumpChannel
namespace CVC4 {
-class CVC4_PUBLIC LogicException : public CVC4::Exception {
+class LogicException : public CVC4::Exception
+{
public:
LogicException() :
Exception("Feature used while operating in "
LogicException(const char* msg) :
Exception(msg) {
}
-};/* class LogicException */
+}; /* class LogicException */
}/* CVC4 namespace */
*
* Represents whether an objective should be minimized or maximized
*/
-enum CVC4_PUBLIC ObjectiveType
+enum ObjectiveType
{
OBJECTIVE_MINIMIZE,
OBJECTIVE_MAXIMIZE,
* 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,
#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"
/* -------------------------------------------------------------------------- */
-class CVC4_PUBLIC SmtEngine
+class CVC4_EXPORT SmtEngine
{
friend class ::CVC4::api::Solver;
friend class ::CVC4::smt::SmtEngineState;
* 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;
/**
* Hash function for the MakeBagOpHashFunction objects.
*/
-struct CVC4_PUBLIC MakeBagOpHashFunction
+struct MakeBagOpHashFunction
{
size_t operator()(const MakeBagOp& op) const;
}; /* struct MakeBagOpHashFunction */
/**
* Hash function for the TupleProjectOpHashFunction objects.
*/
-struct CVC4_PUBLIC TupleProjectOpHashFunction
+struct TupleProjectOpHashFunction
{
size_t operator()(const TupleProjectOp& op) const;
}; /* struct TupleProjectOpHashFunction */
#include <string>
#include <vector>
+#include "cvc4_export.h"
#include "theory/theory_id.h"
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 */
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 */
/**
* Hash function for the SingletonHashFunction objects.
*/
-struct CVC4_PUBLIC SingletonOpHashFunction
+struct SingletonOpHashFunction
{
size_t operator()(const SingletonOp& op) const;
}; /* struct SingletonOpHashFunction */
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.
namespace CVC4 {
-class CVC4_PUBLIC AbstractValue {
+class AbstractValue
+{
const Integer d_index;
public:
}
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 */
namespace CVC4 {
-class CVC4_PUBLIC BitVector
+class BitVector
{
public:
BitVector(unsigned size, const Integer& val)
* 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;
/**
* The structure representing the extraction of one Boolean bit.
*/
-struct CVC4_PUBLIC BitVectorBitOf
+struct BitVectorBitOf
{
/** The index of the bit */
unsigned d_bitIndex;
}
}; /* 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)
operator unsigned() const { return d_zeroExtendAmount; }
}; /* struct BitVectorZeroExtend */
-struct CVC4_PUBLIC BitVectorSignExtend
+struct BitVectorSignExtend
{
unsigned d_signExtendAmount;
BitVectorSignExtend(unsigned signExtendAmount)
operator unsigned() const { return d_signExtendAmount; }
}; /* struct BitVectorSignExtend */
-struct CVC4_PUBLIC BitVectorRotateLeft
+struct BitVectorRotateLeft
{
unsigned d_rotateLeftAmount;
BitVectorRotateLeft(unsigned rotateLeftAmount)
operator unsigned() const { return d_rotateLeftAmount; }
}; /* struct BitVectorRotateLeft */
-struct CVC4_PUBLIC BitVectorRotateRight
+struct BitVectorRotateRight
{
unsigned d_rotateRightAmount;
BitVectorRotateRight(unsigned rotateRightAmount)
operator unsigned() const { return d_rotateRightAmount; }
}; /* struct BitVectorRotateRight */
-struct CVC4_PUBLIC IntToBitVector
+struct IntToBitVector
{
unsigned d_size;
IntToBitVector(unsigned size) : d_size(size) {}
/*
* 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 */
/**
* Hash function for the BitVectorExtract objects.
*/
-struct CVC4_PUBLIC BitVectorExtractHashFunction
+struct BitVectorExtractHashFunction
{
size_t operator()(const BitVectorExtract& extract) const
{
/**
* 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 */
** 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 << "]";
* Representation for a Beth number, used only to construct
* Cardinality objects.
*/
-class CVC4_PUBLIC CardinalityBeth {
+class CardinalityBeth
+{
Integer d_index;
public:
/**
* Representation for an unknown cardinality.
*/
-class CVC4_PUBLIC CardinalityUnknown {
+class CardinalityUnknown
+{
public:
CardinalityUnknown() {}
~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;
static const Cardinality UNKNOWN_CARD;
/** Used as a result code for Cardinality::compare(). */
- enum CVC4_PUBLIC CardinalityComparison {
+ enum CardinalityComparison
+ {
LESS,
EQUAL,
GREATER,
}; /* 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 */
/**
* The structure representing the divisibility-by-k predicate.
*/
-struct CVC4_PUBLIC Divisible {
+struct Divisible
+{
const Integer k;
Divisible(const Integer& n);
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;
}
class FloatingPointLiteral;
-class CVC4_PUBLIC FloatingPoint
+class FloatingPoint
{
public:
/**
/**
* Hash function for floating-point values.
*/
-struct CVC4_PUBLIC FloatingPointHashFunction
+struct FloatingPointHashFunction
{
size_t operator()(const FloatingPoint& fp) const
{
/**
* The parameter type for the conversions to floating point.
*/
-class CVC4_PUBLIC FloatingPointConvertSort
+class FloatingPointConvertSort
{
public:
/** Constructors. */
/** Hash function for conversion sorts. */
template <uint32_t key>
-struct CVC4_PUBLIC FloatingPointConvertSortHashFunction
+struct FloatingPointConvertSortHashFunction
{
inline size_t operator()(const FloatingPointConvertSort& fpcs) const
{
* 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. */
* Conversion from floating-point to another floating-point (of possibly
* different size).
*/
-class CVC4_PUBLIC FloatingPointToFPFloatingPoint
- : public FloatingPointConvertSort
+class FloatingPointToFPFloatingPoint : public FloatingPointConvertSort
{
public:
/** Constructors. */
/**
* Conversion from floating-point to Real.
*/
-class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort
+class FloatingPointToFPReal : public FloatingPointConvertSort
{
public:
/** Constructors. */
/**
* Conversion from floating-point to signed bit-vector value.
*/
-class CVC4_PUBLIC FloatingPointToFPSignedBitVector
- : public FloatingPointConvertSort
+class FloatingPointToFPSignedBitVector : public FloatingPointConvertSort
{
public:
/** Constructors. */
/**
* Conversion from floating-point to unsigned bit-vector value.
*/
-class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector
- : public FloatingPointConvertSort
+class FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort
{
public:
/** Constructors. */
}
};
-class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort
+class FloatingPointToFPGeneric : public FloatingPointConvertSort
{
public:
/** Constructors. */
/**
* Base type for floating-point to bit-vector conversion.
*/
-class CVC4_PUBLIC FloatingPointToBV
+class FloatingPointToBV
{
public:
/** Constructors. */
/**
* 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) {}
/**
* 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) {}
/**
* 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) {}
/**
* 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) {}
* 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
{
* 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
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. */
/**
* Hash function for floating point formats.
*/
-struct CVC4_PUBLIC FloatingPointSizeHashFunction
+struct FloatingPointSizeHashFunction
{
static inline size_t ROLL(size_t X, size_t N)
{
namespace CVC4 {
-struct CVC4_PUBLIC IntAnd
+struct IntAnd
{
unsigned d_size;
IntAnd(unsigned size) : d_size(size) {}
** 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 << "]";
* 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;
}; /* 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
{
#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;
#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;
namespace CVC4 {
template <class T>
-class CVC4_PUBLIC Maybe
+class Maybe
{
public:
Maybe() : d_just(false), d_value(){}
#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"
** in danger of invoking the char* constructor, from whence you will segfault.
**/
-class CVC4_PUBLIC Rational
+class CVC4_EXPORT Rational
{
public:
/**
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
#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"
** in danger of invoking the char* constructor, from whence you will segfault.
**/
-class CVC4_PUBLIC Rational
+class CVC4_EXPORT Rational
{
public:
/**
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
* Note that the interval representation uses dyadic rationals (denominators are
* only powers of two).
*/
-class CVC4_PUBLIC RealAlgebraicNumber
+class RealAlgebraicNumber
{
public:
/** Construct as zero. */
}; /* 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
namespace CVC4 {
-struct CVC4_PUBLIC RegExpRepeat
+struct RegExpRepeat
{
RegExpRepeat(uint32_t repeatAmount);
uint32_t d_repeatAmount;
};
-struct CVC4_PUBLIC RegExpLoop
+struct RegExpLoop
{
RegExpLoop(uint32_t l, uint32_t h);
/*
* Hash function for the RegExpRepeat constants.
*/
-struct CVC4_PUBLIC RegExpRepeatHashFunction
+struct RegExpRepeatHashFunction
{
size_t operator()(const RegExpRepeat& r) const;
};
/**
* Hash function for the RegExpLoop objects.
*/
-struct CVC4_PUBLIC RegExpLoopHashFunction
+struct RegExpLoopHashFunction
{
size_t operator()(const RegExpLoop& r) const;
};
** 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
/**
* 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.
* 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. */
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 };
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 */
/**
* 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,
/**
* 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 */
#include <cstring>
#include <string>
+#include "cvc4_export.h"
+
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();
* @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);
}
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);
#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; }
* 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;
}; /* 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.
*/
#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;
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) { }
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;
*/
const_iterator end() const;
-};/* class StatisticsBase */
+}; /* class StatisticsBase */
-class CVC4_PUBLIC Statistics : public StatisticsBase {
+class Statistics : public StatisticsBase
+{
void clear();
void copyFrom(const StatisticsBase&);
Statistics& operator=(const StatisticsBase& stats);
Statistics& operator=(const Statistics& stats);
-};/* class Statistics */
+}; /* class Statistics */
}/* CVC4 namespace */
** 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
** for a longer discussion on symbol visibility.
**/
-
/**
* On the design of the statistics:
*
#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 {
* 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;
/** 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();
StatisticsRegistry* d_reg;
Stat* d_stat;
-};/* class RegisterStatistic */
+}; /* class RegisterStatistic */
}/* CVC4 namespace */
#include <sstream>
#include <string>
+#include "cvc4_export.h"
#include "util/safe_print.h"
#include "util/sexpr.h"
#include "util/stats_utils.h"
* Derived classes must implement these function and pass their name to
* the base class constructor.
*/
-class Stat
+class CVC4_EXPORT Stat
{
public:
/**
#include <chrono>
+#include "cvc4_export.h"
#include "util/stats_base.h"
namespace CVC4 {
} // 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;
* 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;
#include <iosfwd>
+#include "cvc4_export.h"
+
namespace CVC4 {
namespace timer_stat_detail {
}
std::ostream& operator<<(std::ostream& os,
- const timer_stat_detail::duration& dur) CVC4_PUBLIC;
+ const timer_stat_detail::duration& dur) CVC4_EXPORT;
} // 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
namespace strings {
-struct CVC4_PUBLIC StringHashFunction {
+struct StringHashFunction
+{
size_t operator()(const ::CVC4::String& s) const {
return std::hash<std::string>()(s.toString());
}
} // namespace strings
-std::ostream& operator<<(std::ostream& os, const String& s) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& os, const String& s);
} // namespace CVC4
namespace CVC4 {
-class CVC4_PUBLIC TupleUpdate {
+class TupleUpdate
+{
unsigned d_index;
public:
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() << "]";
#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.") {
UnsafeInterruptException(const char* msg) :
Exception(msg) {
}
-};/* class UnsafeInterruptException */
+}; /* class UnsafeInterruptException */
}/* CVC4 namespace */
projects / cvc5.git / commitdiff