From 4aecb261e60bf3e2de0d6a59af8d3a55b608c273 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 22 Feb 2012 15:30:51 +0000
Subject: [PATCH] Fixes to documentation / fixes for MacOS

---
 configure.ac                      |  2 +-
 src/expr/command.cpp              |  4 ++++
 src/expr/command.h                | 11 +++++++----
 src/theory/arith/simplex.cpp      |  2 +-
 src/theory/arith/theory_arith.cpp |  5 ++++-
 src/util/tls.h.in                 |  2 +-
 6 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/configure.ac b/configure.ac
index 53790a090..d44dc3620 100644
--- a/configure.ac
+++ b/configure.ac
@@ -876,7 +876,7 @@ if test $cvc4_has_threads = maybe; then
   fi
 fi
 if test $cvc4_has_threads = no -a $cvc4_must_have_threads = yes; then
-  AC_MSG_ERROR([user gave --with-threads but could not build with threads; maybe boost threading library is missing?])
+  AC_MSG_ERROR([user gave --with-portfolio but could not build with threads; maybe boost threading library is missing?])
 fi
 
 # Whether to build compatibility library
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index ba29b6c34..8d089901b 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -74,6 +74,10 @@ ostream& operator<<(ostream& out, const CommandStatus* s) throw() {
 Command::Command() throw() : d_commandStatus(NULL) {
 }
 
+Command::Command(const Command& cmd) {
+  d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone();
+}
+
 Command::~Command() throw() {
   if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) {
     delete d_commandStatus;
diff --git a/src/expr/command.h b/src/expr/command.h
index 2d87fefc2..fa1da4cb1 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -158,30 +158,31 @@ public:
   virtual ~CommandStatus() throw() {}
   void toStream(std::ostream& out,
                 OutputLanguage language = language::output::LANG_AST) const throw();
+  virtual CommandStatus& clone() const = 0;
 };/* class CommandStatus */
 
 class CVC4_PUBLIC CommandSuccess : public CommandStatus {
   static const CommandSuccess* s_instance;
 public:
   static const CommandSuccess* instance() throw() { return s_instance; }
+  CommandStatus& clone() const { return const_cast<CommandSuccess&>(*this); }
 };/* class CommandSuccess */
 
 class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
+public:
+  CommandStatus& clone() const { return *new CommandUnsupported(*this); }
 };/* class CommandSuccess */
 
 class CVC4_PUBLIC CommandFailure : public CommandStatus {
   std::string d_message;
 public:
   CommandFailure(std::string message) throw() : d_message(message) {}
+  CommandFailure& clone() const { return *new CommandFailure(*this); }
   ~CommandFailure() throw() {}
   std::string getMessage() const throw() { return d_message; }
 };/* class CommandFailure */
 
 class CVC4_PUBLIC Command {
-  // intentionally not permitted
-  Command(const Command&) CVC4_UNDEFINED;
-  Command& operator=(const Command&) CVC4_UNDEFINED;
-
 protected:
   /**
    * This field contains a command status if the command has been
@@ -197,6 +198,8 @@ public:
   typedef CommandPrintSuccess printsuccess;
 
   Command() throw();
+  Command(const Command& cmd);
+
   virtual ~Command() throw();
 
   virtual void invoke(SmtEngine* smtEngine) throw() = 0;
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 26cdb2cdb..6f8d02642 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -621,7 +621,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   }
 
   static CVC4_THREADLOCAL(unsigned int) instance = 0;
-  ++instance;
+  instance = instance + 1;
   Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() "
                                          << instance << endl;
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 268829105..05159407c 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1224,7 +1224,10 @@ void TheoryArith::presolve(){
   if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); }
 
   static CVC4_THREADLOCAL(unsigned) callCount = 0;
-  Debug("arith::presolve") << "TheoryArith::presolve #" << (callCount++) << endl;
+  if(Debug.isOn("arith::presolve")) {
+    Debug("arith::presolve") << "TheoryArith::presolve #" << callCount << endl;
+    callCount = callCount + 1;
+  }
 
   d_learner.clear();
   check(FULL_EFFORT);
diff --git a/src/util/tls.h.in b/src/util/tls.h.in
index bb69e7c82..e77d256dc 100644
--- a/src/util/tls.h.in
+++ b/src/util/tls.h.in
@@ -75,7 +75,7 @@ public:
   }
 
   operator T() const {
-    return static_cast<T>(pthread_getspecific(d_key));
+    return static_cast<T>(reinterpret_cast<size_t>(pthread_getspecific(d_key)));
   }
 };/* class ThreadLocalImpl<T, true> */
 
-- 
2.30.2