From: Morgan Deters Date: Fri, 1 Apr 2011 21:35:50 +0000 (+0000) Subject: minor bugfixes (fixes broken dynamic-library build from last night) X-Git-Tag: cvc5-1.0.0~8621 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b50c1d3c0c72c0a2e07dabf8206c62b0dd6803d;p=cvc5.git minor bugfixes (fixes broken dynamic-library build from last night) --- diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 99cd26297..4253fafa3 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -147,7 +147,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { SatLiteral CnfStream::getLiteral(TNode node) { TranslationCache::iterator find = d_translationCache.find(node); - Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: ", node.toString().c_str()); + Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: %s", node.toString().c_str()); SatLiteral literal = find->second.literal; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; diff --git a/src/util/stats.h b/src/util/stats.h index 53acc9b1b..526d70681 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -42,7 +42,7 @@ namespace CVC4 { # define __CVC4_USE_STATISTICS false #endif -class ExprManager; +class CVC4_PUBLIC ExprManager; class CVC4_PUBLIC Stat; @@ -186,7 +186,7 @@ inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, * std::ostream& operator<<(std::ostream&, const T&) */ template -class ReadOnlyDataStat : public Stat { +class CVC4_PUBLIC ReadOnlyDataStat : public Stat { public: /** The "payload" type of this data statistic (that is, T). */ typedef T payload_t; @@ -228,7 +228,7 @@ public: * std::ostream& operator<<(std::ostream&, const T&) */ template -class DataStat : public ReadOnlyDataStat { +class CVC4_PUBLIC DataStat : public ReadOnlyDataStat { public: /** Construct a data statistic with the given name. */ @@ -258,7 +258,7 @@ public: * Template class T must have an assignment operator=(). */ template -class ReferenceStat : public DataStat { +class CVC4_PUBLIC ReferenceStat : public DataStat { private: /** The referenced data cell */ const T* d_data; @@ -308,7 +308,7 @@ public: * Template class T must have an operator=() and a copy constructor. */ template -class BackedStat : public DataStat { +class CVC4_PUBLIC BackedStat : public DataStat { protected: /** The internally-kept statistic value */ T d_data; @@ -361,7 +361,7 @@ public: * giving it a globally unique name. */ template -class WrappedStat : public ReadOnlyDataStat { +class CVC4_PUBLIC WrappedStat : public ReadOnlyDataStat { typedef typename Stat::payload_t T; const ReadOnlyDataStat& d_stat; @@ -399,7 +399,7 @@ public: * This doesn't functionally differ from its base class BackedStat, * except for adding convenience functions for dealing with integers. */ -class IntStat : public BackedStat { +class CVC4_PUBLIC IntStat : public BackedStat { public: /** @@ -458,7 +458,7 @@ public: * running count, so should generally be avoided. Call addEntry() to add * an entry to the average calculation. */ -class AverageStat : public BackedStat { +class CVC4_PUBLIC AverageStat : public BackedStat { private: /** * The number of accumulations of the running average that we @@ -485,7 +485,7 @@ public: };/* class AverageStat */ template -class ListStat : public Stat{ +class CVC4_PUBLIC ListStat : public Stat{ private: typedef std::vector List; List d_list; @@ -638,7 +638,7 @@ inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) { * arbitrarily, like a stopwatch; the value of the statistic at the * end is the accumulated time over all (start,stop) pairs. */ -class TimerStat : public BackedStat< ::timespec > { +class CVC4_PUBLIC TimerStat : public BackedStat< ::timespec > { // strange: timespec isn't placed in 'std' namespace ?! /** The last start time of this timer */ @@ -746,7 +746,7 @@ public: * registration/unregistration. This RAII class only does * registration and unregistration. */ -class RegisterStatistic { +class CVC4_PUBLIC RegisterStatistic { ExprManager* d_em; Stat* d_stat; public: