Some minor changes after reviewing the portfolio "unified driver" commit.

(this commit was certified error- and warning-free by the test-and-commit script.)

12 files changed, 83 insertions, 80 deletions

diff --git a/src/expr/command.h b/src/expr/command.h
index 3c919c374..70e71a111 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -50,13 +50,12 @@ std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
 
-class ExportToUnsupportedException : public Exception {
+class CVC4_PUBLIC ExportToUnsupportedException : public Exception {
 public:
   ExportToUnsupportedException() throw() :
     Exception("exportTo unsupported for command") {
   }
-};/* class NoMoreValuesException */
-
+};/* class ExportToUnsupportedException */
 
 /** The status an SMT benchmark can have */
 enum BenchmarkStatus {
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 4009bc610..08c3a2b1e 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -137,9 +137,11 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
         } else if(n.getKind() == kind::VARIABLE) {
           to_e = to->mkVar(name, type);// FIXME thread safety
         } else if(n.getKind() == kind::SKOLEM) {
-          Assert(false, "Skolem exporting not yet supported properly.");
-          // to fix this, get the node manager and do the appropriate
-          to_e = to->mkVar(name, type);// FIXME thread safety
+          // skolems are only available at the Node level (not the Expr level)
+          TypeNode typeNode = TypeNode::fromType(type);
+          NodeManager* to_nm = NodeManager::fromExprManager(to);
+          Node n = to_nm->mkSkolem(name, typeNode);// FIXME thread safety
+          to_e = n.toExpr();
         } else {
           Unhandled();
         }
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 9b0200231..2a1ce0d55 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -20,8 +20,10 @@ pcvc4_SOURCES = \
 	portfolio.cpp \
 	portfolio.h \
 	portfolio_util.cpp \
-	command_executer.cpp \
-	command_executer_portfolio.cpp \
+	command_executor.cpp \
+	command_executor_portfolio.cpp \
+	command_executor.h \
+	command_executor_portfolio.h \
 	driver_unified.cpp
 pcvc4_LDADD = \
 	libmain.a \
@@ -42,7 +44,7 @@ endif
 
 cvc4_SOURCES = \
 	main.cpp \
-	command_executer.cpp \
+	command_executor.cpp \
 	driver_unified.cpp
 cvc4_LDADD = \
 	libmain.a \
diff --git a/src/main/command_executer.cpp b/src/main/command_executor.cpp
index 039ab664c..1bffd5e35 100644
--- a/src/main/command_executer.cpp
+++ b/src/main/command_executor.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file command_executer.cpp
+/*! \file command_executor.cpp
  ** \verbatim
  ** Original author: kshitij
  ** Major contributors: none
- ** Minor contributors (to current version): 
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -16,7 +16,7 @@
 
 #include <iostream>
 
-#include "main/command_executer.h"
+#include "main/command_executor.h"
 #include "expr/command.h"
 
 #include "main/main.h"
@@ -25,7 +25,7 @@ namespace CVC4 {
 namespace main {
 
 
-CommandExecuter::CommandExecuter(ExprManager &exprMgr, Options &options):
+CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options):
   d_exprMgr(exprMgr),
   d_smtEngine(SmtEngine(&exprMgr)),
   d_options(options) {
@@ -36,7 +36,7 @@ CommandExecuter::CommandExecuter(ExprManager &exprMgr, Options &options):
   main::pStatistics->registerStat_(d_exprMgr.getStatisticsRegistry());
 }
 
-bool CommandExecuter::doCommand(Command* cmd)
+bool CommandExecutor::doCommand(Command* cmd)
 {
   if( d_options[options::parseOnly] ) {
     return true;
@@ -63,7 +63,7 @@ bool CommandExecuter::doCommand(Command* cmd)
   }
 }
 
-bool CommandExecuter::doCommandSingleton(Command *cmd)
+bool CommandExecutor::doCommandSingleton(Command *cmd)
 {
   bool status = true;
   if(d_options[options::verbosity] >= 0) {
@@ -74,7 +74,7 @@ bool CommandExecuter::doCommandSingleton(Command *cmd)
   return status;
 }
 
-std::string CommandExecuter::getSmtEngineStatus()
+std::string CommandExecutor::getSmtEngineStatus()
 {
   return d_smtEngine.getInfo("status").getValue();
 }
diff --git a/src/main/command_executer.h b/src/main/command_executor.h
index 245857c04..273225e69 100644
--- a/src/main/command_executer.h
+++ b/src/main/command_executor.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file command_executer.cpp
+/*! \file command_executor.h
  ** \verbatim
  ** Original author: kshitij
- ** Major contributors: mdeters
- ** Minor contributors (to current version): 
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -14,17 +14,16 @@
  ** \brief An additional layer between commands and invoking them.
  **/
 
-#ifndef __CVC4__COMMAND_EXECUTER_H
-#define __CVC4__COMMAND_EXECUTER_H
+#ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H
+#define __CVC4__MAIN__COMMAND_EXECUTOR_H
 
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
 
 namespace CVC4 {
-
 namespace main {
 
-class CommandExecuter {
+class CommandExecutor {
 
 protected:
   ExprManager& d_exprMgr;
@@ -36,9 +35,9 @@ public:
   // used), the portfolio command executer currently parses them
   // during initalization, creating thread-specific options and
   // storing them
-  CommandExecuter(ExprManager &exprMgr, Options &options);
+  CommandExecutor(ExprManager &exprMgr, Options &options);
 
-  ~CommandExecuter() {}
+  ~CommandExecutor() {}
 
   /**
    * Executes a command. Recursively handles if cmd is a command
@@ -54,16 +53,15 @@ protected:
   virtual bool doCommandSingleton(CVC4::Command* cmd);
 
 private:
-  CommandExecuter();
+  CommandExecutor();
 
-};
+};/* class CommandExecutor */
 
 bool smtEngineInvoke(SmtEngine* smt,
                      Command* cmd,
                      std::ostream *out);
 
+}/* CVC4::main namespace */
+}/* CVC4 namespace */
 
-}/*main namespace*/
-}/*CVC4 namespace*/
-
-#endif  /* __CVC4__COMMAND_EXECUTER_H */
+#endif  /* __CVC4__MAIN__COMMAND_EXECUTOR_H */
diff --git a/src/main/command_executer_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 85180c9a9..045cac8f1 100644
--- a/src/main/command_executer_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file command_executer_portfolio.cpp
+/*! \file command_executor_portfolio.cpp
  ** \verbatim
  ** Original author: kshitij
- ** Major contributors: mdeters, taking
- ** Minor contributors (to current version): 
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -24,7 +24,7 @@
 
 #include "expr/command.h"
 #include "expr/pickler.h"
-#include "main/command_executer_portfolio.h"
+#include "main/command_executor_portfolio.h"
 #include "main/main.h"
 #include "main/options.h"
 #include "main/portfolio.h"
@@ -36,9 +36,9 @@ using namespace std;
 namespace CVC4 {
 namespace main {
 
-CommandExecuterPortfolio::CommandExecuterPortfolio
+CommandExecutorPortfolio::CommandExecutorPortfolio
 (ExprManager &exprMgr, Options &options, vector<Options>& tOpts):
-  CommandExecuter(exprMgr, options),
+  CommandExecutor(exprMgr, options),
   d_numThreads(options[options::threads]),
   d_smts(),
   d_seq(new CommandSequence()),
@@ -85,7 +85,7 @@ CommandExecuterPortfolio::CommandExecuterPortfolio
 
 }
 
-CommandExecuterPortfolio::~CommandExecuterPortfolio()
+CommandExecutorPortfolio::~CommandExecutorPortfolio()
 {
   Assert(d_seq != NULL);
   delete d_seq;
@@ -101,7 +101,7 @@ CommandExecuterPortfolio::~CommandExecuterPortfolio()
   d_smts.clear();
 }
 
-void CommandExecuterPortfolio::lemmaSharingInit()
+void CommandExecutorPortfolio::lemmaSharingInit()
 {
   /* Sharing channels */
   Assert(d_channelsIn.size() == 0);
@@ -154,7 +154,7 @@ void CommandExecuterPortfolio::lemmaSharingInit()
   }
 }
 
-void CommandExecuterPortfolio::lemmaSharingCleanup()
+void CommandExecutorPortfolio::lemmaSharingCleanup()
 {
   Assert(d_numThreads == d_options[options::threads]);
 
@@ -182,7 +182,7 @@ void CommandExecuterPortfolio::lemmaSharingCleanup()
 
 }
 
-bool CommandExecuterPortfolio::doCommandSingleton(Command* cmd)
+bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 {
   /**
    * save the command and if check sat or query command, run a
@@ -203,7 +203,7 @@ bool CommandExecuterPortfolio::doCommandSingleton(Command* cmd)
   
   if(mode == 0) {
     d_seq->addCommand(cmd->clone());
-    return CommandExecuter::doCommandSingleton(cmd);
+    return CommandExecutor::doCommandSingleton(cmd);
   } else if(mode == 1) {               // portfolio
     d_seq->addCommand(cmd->clone());
 
@@ -228,7 +228,7 @@ bool CommandExecuterPortfolio::doCommandSingleton(Command* cmd)
       try {
         seqs[i] = d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) );
       }catch(ExportToUnsupportedException& e){
-        return CommandExecuter::doCommandSingleton(cmd);
+        return CommandExecutor::doCommandSingleton(cmd);
       }
     }
 
@@ -305,7 +305,7 @@ bool CommandExecuterPortfolio::doCommandSingleton(Command* cmd)
 
 }
 
-std::string CommandExecuterPortfolio::getSmtEngineStatus()
+std::string CommandExecutorPortfolio::getSmtEngineStatus()
 {
   return d_smts[d_lastWinner]->getInfo("status").getValue();
 }
diff --git a/src/main/command_executer_portfolio.h b/src/main/command_executor_portfolio.h
index db9db6509..cc0a77698 100644
--- a/src/main/command_executer_portfolio.h
+++ b/src/main/command_executor_portfolio.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file command_executer_portfolio.h
+/*! \file command_executor_portfolio.h
  ** \verbatim
  ** Original author: kshitij
  ** Major contributors: none
- ** Minor contributors (to current version): 
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -17,10 +17,10 @@
  ** threads.
  **/
 
-#ifndef __CVC4__COMMAND_EXECUTER_PORTFOLIO_H
-#define __CVC4__COMMAND_EXECUTER_PORTFOLIO_H
+#ifndef __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H
+#define __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H
 
-#include "main/command_executer.h"
+#include "main/command_executor.h"
 #include "main/portfolio_util.h"
 
 namespace CVC4 {
@@ -29,7 +29,7 @@ class CommandSequence;
 
 namespace main {
 
-class CommandExecuterPortfolio : public CommandExecuter {
+class CommandExecutorPortfolio : public CommandExecutor {
 
   // These shall be created/deleted during initalization
   std::vector<ExprManager*> d_exprMgrs;
@@ -48,22 +48,22 @@ class CommandExecuterPortfolio : public CommandExecuter {
   std::vector<std::ostringstream*> d_ostringstreams;
 
 public:
-  CommandExecuterPortfolio(ExprManager &exprMgr,
+  CommandExecutorPortfolio(ExprManager &exprMgr,
                            Options &options,
                            std::vector<Options>& tOpts);
 
-  ~CommandExecuterPortfolio();
+  ~CommandExecutorPortfolio();
 
   std::string getSmtEngineStatus();
 protected:
   bool doCommandSingleton(Command* cmd);
 private:
-  CommandExecuterPortfolio();
+  CommandExecutorPortfolio();
   void lemmaSharingInit();
   void lemmaSharingCleanup();
-};
+};/* class CommandExecutorPortfolio */
 
-}/*main namespace*/
-}/*CVC4 namespace*/
+}/* CVC4::main namespace */
+}/* CVC4 namespace */
 
-#endif  /* __CVC4__COMMAND_EXECUTER_PORTFOLIO_H */
+#endif  /* __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H */
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 061e34223..f91f951c6 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -35,9 +35,9 @@
 #include "util/Assert.h"
 #include "util/configuration.h"
 #include "options/options.h"
-#include "main/command_executer.h"
+#include "main/command_executor.h"
 # ifdef PORTFOLIO_BUILD
-#    include "main/command_executer_portfolio.h"
+#    include "main/command_executor_portfolio.h"
 # endif
 #include "main/options.h"
 #include "smt/options.h"
@@ -226,11 +226,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   ExprManager exprMgr(threadOpts[0]);
 # endif
 
-  CommandExecuter* cmdExecuter = 
+  CommandExecutor* cmdExecutor = 
 # ifndef PORTFOLIO_BUILD
-    new CommandExecuter(exprMgr, opts);
+    new CommandExecutor(exprMgr, opts);
 # else
-    new CommandExecuterPortfolio(exprMgr, opts, threadOpts);
+    new CommandExecutorPortfolio(exprMgr, opts, threadOpts);
 #endif
 
   // Create the SmtEngine
@@ -280,7 +280,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       replayParser->useDeclarationsFrom(shell.getParser());
     }
     while((cmd = shell.readCommand())) {
-      status = cmdExecuter->doCommand(cmd) && status;
+      status = cmdExecutor->doCommand(cmd) && status;
       delete cmd;
     }
   } else {
@@ -304,7 +304,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
         break;
       }
-      status = cmdExecuter->doCommand(cmd);
+      status = cmdExecutor->doCommand(cmd);
       delete cmd;
     }
     // Remove the parser
@@ -320,7 +320,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   int returnValue;
   string result = "unknown";
   if(status) {
-    result = cmdExecuter->getSmtEngineStatus();
+    result = cmdExecutor->getSmtEngineStatus();
 
     if(result == "sat") {
       returnValue = 10;
diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp
index bad532d30..b208b2479 100644
--- a/src/main/portfolio_util.cpp
+++ b/src/main/portfolio_util.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include <vector>
+#include <unistd.h>
 #include "options/options.h"
 #include "main/options.h"
 #include "prop/options.h"
diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
index eed993b9f..1955a29a7 100644
--- a/src/main/portfolio_util.h
+++ b/src/main/portfolio_util.h
@@ -14,8 +14,8 @@
  ** \brief Code relevant only for portfolio builds
  **/
 
-#ifndef __CVC4_PORTFOLIO_UTIL_H
-#define __CVC4_PORTFOLIO_UTIL_H
+#ifndef __CVC4__PORTFOLIO_UTIL_H
+#define __CVC4__PORTFOLIO_UTIL_H
 
 #include <queue>
 
@@ -37,7 +37,7 @@ public:
   T pop() { return T(); }
   bool empty() { return true; }
   bool full() { return false; }
-};
+};/* class EmptySharedChannel */
 
 class PortfolioLemmaOutputChannel : public LemmaOutputChannel {
 private:
@@ -202,8 +202,8 @@ void sharingManager(unsigned numThreads,
   }
 
   Trace("sharing") << "sharing: Interrupted, exiting." << std::endl;
-}
+}/* sharingManager() */
 
-}/*CVC4 namespace*/
+}/* CVC4 namespace */
 
-#endif   /* __CVC4_PORTFOLIO_UTIL_H */
+#endif   /* __CVC4__PORTFOLIO_UTIL_H */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 281645317..a82e1b735 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -272,8 +272,6 @@ bool PropEngine::isRunning() const {
 void PropEngine::interrupt() throw(ModalException) {
   if(! d_inCheckSat) {
     return;
-    throw ModalException("SAT solver is not currently solving anything; "
-                         "cannot interrupt it");
   }
 
   d_interrupted = true;
diff --git a/src/util/channel.h b/src/util/channel.h
index eae7a4f11..4a07f265d 100644
--- a/src/util/channel.h
+++ b/src/util/channel.h
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_public.h"
+
 #ifndef __CVC4__CHANNEL_H
 #define __CVC4__CHANNEL_H
 
@@ -31,12 +33,13 @@
 namespace CVC4 {
 
 template <typename T>
-class SharedChannel {
+class CVC4_PUBLIC SharedChannel {
 private:
   int d_maxsize;                // just call it size?
 public:
   SharedChannel() {}
   SharedChannel(int maxsize) : d_maxsize(maxsize) {}
+  virtual ~SharedChannel() {}
 
   /* Tries to add element and returns true if successful */
   virtual bool push(const T&) = 0;
@@ -59,7 +62,7 @@ http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.h
 and is covered by the Boost Software License, version 1.0.
 */
 template <typename T>
-class SynchronizedSharedChannel : public SharedChannel<T> {
+class CVC4_PUBLIC SynchronizedSharedChannel : public SharedChannel<T> {
 public:
   typedef boost::circular_buffer<T> container_type;
   typedef typename container_type::size_type size_type;
@@ -108,6 +111,6 @@ private:
   boost::condition m_not_full;
 };/* class SynchronizedSharedChannel<T> */
 
-}
+}/* CVC4 namespace */
 
 #endif /* __CVC4__CHANNEL_H */