Fixes to documentation / fixes for MacOS

diff --git a/configure.ac b/configure.ac
index 53790a090e4a27119c14eb6980b3b4cb22b8834f..d44dc362087f2d8bbf6c3aa7a2ecf7310310be26 100644 (file)
--- 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 ba29b6c347f95d07447fa82d962dd9c063f56fea..8d089901b8f0a043ee45a86b0c5629a8064d5bf3 100644 (file)
--- 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 2d87fefc23949112b45f43a768767806297a08e0..fa1da4cb187243e911cb86a47b202fdfb8942cd3 100644 (file)
--- 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 26cdb2cdbe219db3d22dd28922f5ecaf4c2118db..6f8d0264220f36dd60fe15097bf530e06f30895f 100644 (file)
--- 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 268829105737c5b6616a5ff6f1effc1ccf7a2efb..05159407c975d71f0705c5305e737cb23a9b3301 100644 (file)
--- 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 bb69e7c827e34529e32a373d086da695a6208ac4..e77d256dcfbe82fc86bcb9f2ad0aca21830f63de 100644 (file)
--- 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> */