Single driver for both sequential and portfolio

A "command executer" layer between parsing commands and invoking them.

New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.

3 files changed, 32 insertions, 5 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index b058292f3..1e4a266a5 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -419,7 +419,9 @@ CommandSequence::const_iterator CommandSequence::begin() const throw() {
 Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
   CommandSequence* seq = new CommandSequence();
   for(iterator i = begin(); i != end(); ++i) {
-    seq->addCommand((*i)->exportTo(exprManager, variableMap));
+    Command* cmd_to_export = *i;
+    Command* cmd = cmd_to_export->exportTo(exprManager, variableMap);
+    seq->addCommand(cmd);
   }
   seq->d_index = d_index;
   return seq;
@@ -1197,8 +1199,12 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
 }
 
 Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  Warning() << "We currently do not support exportTo with Datatypes" << std::endl;
-  return NULL;
+  throw ExportToUnsupportedException();
+  // vector<DatatypeType> params;
+  // transform(d_datatypes.begin(), d_datatypes.end(), back_inserter(params),
+  //           ExportTransformer(exprManager, variableMap));
+  // DatatypeDeclarationCommand* c = new DatatypeDeclarationCommand(params);
+  // return c;
 }
 
 Command* DatatypeDeclarationCommand::clone() const {
diff --git a/src/expr/command.h b/src/expr/command.h
index 0f517e7f2..3c919c374 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -50,6 +50,14 @@ 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 {
+public:
+  ExportToUnsupportedException() throw() :
+    Exception("exportTo unsupported for command") {
+  }
+};/* class NoMoreValuesException */
+
+
 /** The status an SMT benchmark can have */
 enum BenchmarkStatus {
   /** Benchmark is satisfiable */
@@ -233,7 +241,8 @@ public:
    * variableMap for the translation and extending it with any new
    * mappings.
    */
-  virtual Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) = 0;
+  virtual Command* exportTo(ExprManager* exprManager,
+                            ExprManagerMapCollection& variableMap) = 0;
 
   /**
    * Clone this Command (make a shallow copy).
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index a6f9f2cf6..4009bc610 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -131,7 +131,19 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
         // temporarily set the node manager to NULL; this gets around
         // a check that mkVar isn't called internally
         NodeManagerScope nullScope(NULL);
-        to_e = to->mkVar(name, type);// FIXME thread safety
+
+        if(n.getKind() == kind::BOUND_VAR_LIST) {
+          to_e = to->mkBoundVar(name, type);// FIXME thread safety
+        } 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
+        } else {
+          Unhandled();
+        }
+
         Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl;
       } else {
         // temporarily set the node manager to NULL; this gets around