From: Morgan Deters <mdeters@gmail.com>
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 T>
-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 T>
-class DataStat : public ReadOnlyDataStat<T> {
+class CVC4_PUBLIC DataStat : public ReadOnlyDataStat<T> {
 public:
 
   /** Construct a data statistic with the given name. */
@@ -258,7 +258,7 @@ public:
  * Template class T must have an assignment operator=().
  */
 template <class T>
-class ReferenceStat : public DataStat<T> {
+class CVC4_PUBLIC ReferenceStat : public DataStat<T> {
 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 T>
-class BackedStat : public DataStat<T> {
+class CVC4_PUBLIC BackedStat : public DataStat<T> {
 protected:
   /** The internally-kept statistic value */
   T d_data;
@@ -361,7 +361,7 @@ public:
  * giving it a globally unique name.
  */
 template <class Stat>
-class WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
+class CVC4_PUBLIC WrappedStat : public ReadOnlyDataStat<typename Stat::payload_t> {
   typedef typename Stat::payload_t T;
 
   const ReadOnlyDataStat<T>& d_stat;
@@ -399,7 +399,7 @@ public:
  * This doesn't functionally differ from its base class BackedStat<int64_t>,
  * except for adding convenience functions for dealing with integers.
  */
-class IntStat : public BackedStat<int64_t> {
+class CVC4_PUBLIC IntStat : public BackedStat<int64_t> {
 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<double> {
+class CVC4_PUBLIC AverageStat : public BackedStat<double> {
 private:
   /**
    * The number of accumulations of the running average that we
@@ -485,7 +485,7 @@ public:
 };/* class AverageStat */
 
 template <class T>
-class ListStat : public Stat{
+class CVC4_PUBLIC ListStat : public Stat{
 private:
   typedef std::vector<T> 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: