portfolio merge

22 files changed, 1389 insertions, 28 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 6a070a88a..6baa4613f 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -28,6 +28,12 @@ libexpr_la_SOURCES = \
 	declaration_scope.cpp \
 	expr_manager_scope.h \
 	node_self_iterator.h \
+	variable_type_map.h \
+	pickle_data.h \
+	pickle_data.cpp \
+	pickler.h \
+	pickler.cpp \
+	node_self_iterator.h \
 	expr_stream.h \
 	kind_map.h
 
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 7d060186a..ba29b6c34 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -126,6 +126,10 @@ void EmptyCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* EmptyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new EmptyCommand(d_name);
+}
+
 /* class AssertCommand */
 
 AssertCommand::AssertCommand(const BoolExpr& e) throw() :
@@ -145,6 +149,10 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new AssertCommand(d_expr.exportTo(exprManager, variableMap));
+}
+
 /* class PushCommand */
 
 void PushCommand::invoke(SmtEngine* smtEngine) throw() {
@@ -156,6 +164,10 @@ void PushCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* PushCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new PushCommand;
+}
+
 /* class PopCommand */
 
 void PopCommand::invoke(SmtEngine* smtEngine) throw() {
@@ -173,6 +185,12 @@ CheckSatCommand::CheckSatCommand() throw() :
   d_expr() {
 }
 
+Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new PopCommand();
+}
+
+/* class CheckSatCommand */
+
 CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() :
   d_expr(expr) {
 }
@@ -202,6 +220,12 @@ void CheckSatCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap));
+  c->d_result = d_result;
+  return c;
+}
+
 /* class QueryCommand */
 
 QueryCommand::QueryCommand(const BoolExpr& e) throw() :
@@ -233,6 +257,12 @@ void QueryCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap));
+  c->d_result = d_result;
+  return c;
+}
+
 /* class QuitCommand */
 
 QuitCommand::QuitCommand() throw() {
@@ -243,6 +273,10 @@ void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* QuitCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new QuitCommand();
+}
+
 /* class CommentCommand */
 
 CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
@@ -257,6 +291,10 @@ void CommentCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* CommentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new CommentCommand(d_comment);
+}
+
 /* class CommandSequence */
 
 CommandSequence::CommandSequence() throw() :
@@ -299,6 +337,15 @@ CommandSequence::const_iterator CommandSequence::begin() const throw() {
   return d_commandSequence.begin();
 }
 
+Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  CommandSequence* seq = new CommandSequence();
+  for(iterator i = begin(); i != end(); ++i) {
+    seq->addCommand((*i)->exportTo(exprManager, variableMap));
+  }
+  seq->d_index = d_index;
+  return seq;
+}
+
 CommandSequence::const_iterator CommandSequence::end() const throw() {
   return d_commandSequence.end();
 }
@@ -338,6 +385,12 @@ void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
 }
 
+Command* DeclareFunctionCommand::exportTo(ExprManager* exprManager,
+                                          ExprManagerMapCollection& variableMap) {
+  return new DeclareFunctionCommand(d_symbol,
+                                    d_type.exportTo(exprManager, variableMap));
+}
+
 /* class DeclareTypeCommand */
 
 DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() :
@@ -358,6 +411,12 @@ void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
 }
 
+Command* DeclareTypeCommand::exportTo(ExprManager* exprManager,
+                                      ExprManagerMapCollection& variableMap) {
+  return new DeclareTypeCommand(d_symbol, d_arity,
+                                d_type.exportTo(exprManager, variableMap));
+}
+
 /* class DefineTypeCommand */
 
 DefineTypeCommand::DefineTypeCommand(const std::string& id,
@@ -388,6 +447,14 @@ void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* DefineTypeCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  vector<Type> params;
+  transform(d_params.begin(), d_params.end(), back_inserter(params),
+            ExportTransformer(exprManager, variableMap));
+  Type type = d_type.exportTo(exprManager, variableMap);
+  return new DefineTypeCommand(d_symbol, params, type);
+}
+
 /* class DefineFunctionCommand */
 
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
@@ -429,6 +496,15 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  Expr func = d_func.exportTo(exprManager, variableMap);
+  vector<Expr> formals;
+  transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
+            ExportTransformer(exprManager, variableMap));
+  Expr formula = d_formula.exportTo(exprManager, variableMap);
+  return new DefineFunctionCommand(d_symbol, func, formals, formula);
+}
+
 /* class DefineNamedFunctionCommand */
 
 DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
@@ -446,6 +522,15 @@ void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* DefineNamedFunctionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  Expr func = d_func.exportTo(exprManager, variableMap);
+  vector<Expr> formals;
+  transform(d_formals.begin(), d_formals.end(), back_inserter(formals),
+            ExportTransformer(exprManager, variableMap));
+  Expr formula = d_formula.exportTo(exprManager, variableMap);
+  return new DefineNamedFunctionCommand(d_symbol, func, formals, formula);
+}
+
 /* class Simplify */
 
 SimplifyCommand::SimplifyCommand(Expr term) throw() :
@@ -473,6 +558,12 @@ void SimplifyCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* SimplifyCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  SimplifyCommand* c = new SimplifyCommand(d_term.exportTo(exprManager, variableMap));
+  c->d_result = d_result.exportTo(exprManager, variableMap);
+  return c;
+}
+
 /* class GetValueCommand */
 
 GetValueCommand::GetValueCommand(Expr term) throw() :
@@ -505,6 +596,12 @@ void GetValueCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetValueCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetValueCommand* c = new GetValueCommand(d_term.exportTo(exprManager, variableMap));
+  c->d_result = d_result.exportTo(exprManager, variableMap);
+  return c;
+}
+
 /* class GetAssignmentCommand */
 
 GetAssignmentCommand::GetAssignmentCommand() throw() {
@@ -531,6 +628,12 @@ void GetAssignmentCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetAssignmentCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetAssignmentCommand* c = new GetAssignmentCommand;
+  c->d_result = d_result;
+  return c;
+}
+
 /* class GetProofCommand */
 
 GetProofCommand::GetProofCommand() throw() {
@@ -557,6 +660,12 @@ void GetProofCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetProofCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetProofCommand* c = new GetProofCommand;
+  c->d_result = d_result;
+  return c;
+}
+
 /* class GetAssertionsCommand */
 
 GetAssertionsCommand::GetAssertionsCommand() throw() {
@@ -586,6 +695,12 @@ void GetAssertionsCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetAssertionsCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetAssertionsCommand* c = new GetAssertionsCommand;
+  c->d_result = d_result;
+  return c;
+}
+
 /* class SetBenchmarkStatusCommand */
 
 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
@@ -608,6 +723,11 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* SetBenchmarkStatusCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  SetBenchmarkStatusCommand* c = new SetBenchmarkStatusCommand(d_status);
+  return c;
+}
+
 /* class SetBenchmarkLogicCommand */
 
 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
@@ -627,6 +747,11 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* SetBenchmarkLogicCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  SetBenchmarkLogicCommand* c = new SetBenchmarkLogicCommand(d_logic);
+  return c;
+}
+
 /* class SetInfoCommand */
 
 SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
@@ -653,6 +778,11 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* SetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  SetInfoCommand* c = new SetInfoCommand(d_flag, d_sexpr);
+  return c;
+}
+
 /* class GetInfoCommand */
 
 GetInfoCommand::GetInfoCommand(std::string flag) throw() :
@@ -688,6 +818,12 @@ void GetInfoCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetInfoCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetInfoCommand* c = new GetInfoCommand(d_flag);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class SetOptionCommand */
 
 SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
@@ -714,6 +850,11 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
+Command* SetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  SetOptionCommand* c = new SetOptionCommand(d_flag, d_sexpr);
+  return c;
+}
+
 /* class GetOptionCommand */
 
 GetOptionCommand::GetOptionCommand(std::string flag) throw() :
@@ -747,6 +888,12 @@ void GetOptionCommand::printResult(std::ostream& out) const throw() {
   }
 }
 
+Command* GetOptionCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  GetOptionCommand* c = new GetOptionCommand(d_flag);
+  c->d_result = d_result;
+  return c;
+}
+
 /* class DatatypeDeclarationCommand */
 
 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
@@ -768,6 +915,11 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
   d_commandStatus = CommandSuccess::instance();
 }
 
+Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  std::cout << "We currently do not support exportTo with Datatypes" << std::endl;
+  exit(1);
+  return NULL;
+}
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out,
                          BenchmarkStatus status) throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index cf8c1b615..2d87fefc2 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -32,6 +32,7 @@
 
 #include "expr/expr.h"
 #include "expr/type.h"
+#include "expr/variable_type_map.h"
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/datatype.h"
@@ -177,6 +178,10 @@ public:
 };/* 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
@@ -210,6 +215,29 @@ public:
 
   virtual void printResult(std::ostream& out) const throw();
 
+  /**
+   * Maps this Command into one for a different ExprManager, using
+   * variableMap for the translation and extending it with any new
+   * mappings.
+   */
+  virtual Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) = 0;
+
+protected:
+  class ExportTransformer {
+    ExprManager* d_exprManager;
+    ExprManagerMapCollection& d_variableMap;
+  public:
+    ExportTransformer(ExprManager* exprManager, ExprManagerMapCollection& variableMap) :
+      d_exprManager(exprManager),
+      d_variableMap(variableMap) {
+    }
+    Expr operator()(Expr e) {
+      return e.exportTo(d_exprManager, d_variableMap);
+    }
+    Type operator()(Type t) {
+      return t.exportTo(d_exprManager, d_variableMap);
+    }
+  };/* class Command::ExportTransformer */
 };/* class Command */
 
 /**
@@ -224,6 +252,7 @@ public:
   ~EmptyCommand() throw() {}
   std::string getName() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class EmptyCommand */
 
 class CVC4_PUBLIC AssertCommand : public Command {
@@ -234,18 +263,21 @@ public:
   ~AssertCommand() throw() {}
   BoolExpr getExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command {
 public:
   ~PushCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class PushCommand */
 
 class CVC4_PUBLIC PopCommand : public Command {
 public:
   ~PopCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class PopCommand */
 
 class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
@@ -265,6 +297,7 @@ public:
   ~DeclareFunctionCommand() throw() {}
   Type getType() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DeclareFunctionCommand */
 
 class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
@@ -277,6 +310,7 @@ public:
   size_t getArity() const throw();
   Type getType() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DeclareTypeCommand */
 
 class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
@@ -290,6 +324,7 @@ public:
   const std::vector<Type>& getParameters() const throw();
   Type getType() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DefineTypeCommand */
 
 class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
@@ -306,6 +341,7 @@ public:
   const std::vector<Expr>& getFormals() const throw();
   Expr getFormula() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DefineFunctionCommand */
 
 /**
@@ -318,6 +354,7 @@ public:
   DefineNamedFunctionCommand(const std::string& id, Expr func,
                              const std::vector<Expr>& formals, Expr formula) throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DefineNamedFunctionCommand */
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -332,6 +369,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   Result getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class CheckSatCommand */
 
 class CVC4_PUBLIC QueryCommand : public Command {
@@ -345,6 +383,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   Result getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class QueryCommand */
 
 // this is TRANSFORM in the CVC presentation language
@@ -359,6 +398,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   Expr getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class SimplifyCommand */
 
 class CVC4_PUBLIC GetValueCommand : public Command {
@@ -372,6 +412,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   Expr getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetValueCommand */
 
 class CVC4_PUBLIC GetAssignmentCommand : public Command {
@@ -383,6 +424,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   SExpr getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetAssignmentCommand */
 
 class CVC4_PUBLIC GetProofCommand : public Command {
@@ -394,6 +436,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   Proof* getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetProofCommand */
 
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
@@ -405,6 +448,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   std::string getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetAssertionsCommand */
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
@@ -415,6 +459,7 @@ public:
   ~SetBenchmarkStatusCommand() throw() {}
   BenchmarkStatus getStatus() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class SetBenchmarkStatusCommand */
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
@@ -425,6 +470,7 @@ public:
   ~SetBenchmarkLogicCommand() throw() {}
   std::string getLogic() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command {
@@ -437,6 +483,7 @@ public:
   std::string getFlag() const throw();
   SExpr getSExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class SetInfoCommand */
 
 class CVC4_PUBLIC GetInfoCommand : public Command {
@@ -450,6 +497,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   std::string getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetInfoCommand */
 
 class CVC4_PUBLIC SetOptionCommand : public Command {
@@ -462,6 +510,7 @@ public:
   std::string getFlag() const throw();
   SExpr getSExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class SetOptionCommand */
 
 class CVC4_PUBLIC GetOptionCommand : public Command {
@@ -475,6 +524,7 @@ public:
   void invoke(SmtEngine* smtEngine) throw();
   std::string getResult() const throw();
   void printResult(std::ostream& out) const throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class GetOptionCommand */
 
 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
@@ -486,6 +536,7 @@ public:
   DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
   const std::vector<DatatypeType>& getDatatypes() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class DatatypeDeclarationCommand */
 
 class CVC4_PUBLIC QuitCommand : public Command {
@@ -493,6 +544,7 @@ public:
   QuitCommand() throw();
   ~QuitCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class QuitCommand */
 
 class CVC4_PUBLIC CommentCommand : public Command {
@@ -502,6 +554,7 @@ public:
   ~CommentCommand() throw() {}
   std::string getComment() const throw();
   void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class CommentCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command {
@@ -528,6 +581,7 @@ public:
   iterator begin() throw();
   iterator end() throw();
 
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
 };/* class CommandSequence */
 
 class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 576d0324d..83a80ed13 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/node_manager.h"
 #include "expr/expr_manager.h"
+#include "expr/variable_type_map.h"
 #include "context/context.h"
 #include "util/options.h"
 #include "util/stats.h"
@@ -30,7 +31,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 34 "${template}"
+#line 35 "${template}"
 
 #ifdef CVC4_STATISTICS_ON
   #define INC_STAT(kind) \
@@ -829,6 +830,52 @@ Context* ExprManager::getContext() const {
   return d_ctxt;
 }
 
+namespace expr {
+
+Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
+
+TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) {
+  Debug("export") << "type: " << n << std::endl;
+  Assert(n.getKind() == kind::SORT_TYPE ||
+         n.getMetaKind() != kind::metakind::PARAMETERIZED,
+         "PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
+  if(n.getKind() == kind::TYPE_CONSTANT) {
+    return to->mkTypeConst(n.getConst<TypeConstant>());
+  } else if(n.getKind() == kind::BITVECTOR_TYPE) {
+    return to->mkBitVectorType(n.getConst<BitVectorSize>());
+  }
+  Type from_t = from->toType(n);
+  Type& to_t = vmap.d_typeMap[from_t];
+  if(! to_t.isNull()) {
+    Debug("export") << "+ mapped `" << from_t << "' to `" << to_t << "'" << std::endl;
+    return *Type::getTypeNode(to_t);
+  }
+  NodeBuilder<> children(to, n.getKind());
+  if(n.getKind() == kind::SORT_TYPE) {
+    Debug("export") << "type: operator: " << n.getOperator() << std::endl;
+    // make a new sort tag in target node manager
+    Node sortTag = NodeBuilder<0>(to, kind::SORT_TAG);
+    children << sortTag;
+  }
+  for(TypeNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
+    Debug("export") << "type: child: " << *i << std::endl;
+    children << exportTypeInternal(*i, from, to, vmap);
+  }
+  TypeNode out = children.constructTypeNode();// FIXME thread safety
+  to_t = to->toType(out);
+  return out;
+}/* exportTypeInternal() */
+
+}/* CVC4::expr namespace */
+
+Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) {
+  Assert(t.d_nodeManager != em->d_nodeManager,
+         "Can't export a Type to the same ExprManager");
+  NodeManagerScope ems(t.d_nodeManager);
+  return Type(em->d_nodeManager,
+              new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));
+}
+
 ${mkConst_implementations}
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 81d30fd1e..eecb40f3e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -42,6 +42,13 @@ class SmtEngine;
 class NodeManager;
 struct Options;
 class IntStat;
+class ExprManagerMapCollection;
+
+namespace expr {
+  namespace pickle {
+    class Pickler;
+  }/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
 
 namespace context {
   class Context;
@@ -404,6 +411,11 @@ public:
   Expr mkVar(const std::string& name, Type type);
   Expr mkVar(Type type);
 
+  /** Export an expr to a different ExprManager */
+  //static Expr exportExpr(const Expr& e, ExprManager* em);
+  /** Export a type to a different ExprManager */
+  static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap);
+
   /** Returns the minimum arity of the given kind. */
   static unsigned minArity(Kind kind);
 
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 3c376f632..c510ce381 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -19,8 +19,10 @@
 #include "expr/expr.h"
 #include "expr/node.h"
 #include "expr/expr_manager_scope.h"
+#include "expr/variable_type_map.h"
 #include "util/Assert.h"
 
+#include <vector>
 #include <iterator>
 #include <utility>
 
@@ -30,7 +32,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 34 "${template}"
+#line 36 "${template}"
 
 using namespace CVC4::kind;
 using namespace std;
@@ -105,6 +107,72 @@ ExprManager* Expr::getExprManager() const {
   return d_exprManager;
 }
 
+namespace expr {
+
+static Node exportConstant(TNode n, NodeManager* to);
+
+Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) {
+  if(n.getMetaKind() == kind::metakind::CONSTANT) {
+    return exportConstant(n, NodeManager::fromExprManager(to));
+  } else if(n.getMetaKind() == kind::metakind::VARIABLE) {
+    Expr from_e(from, new Node(n));
+    Expr& to_e = vmap.d_typeMap[from_e];
+    if(! to_e.isNull()) {
+Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl;
+      return to_e.getNode();
+    } else {
+      // construct new variable in other manager:
+      // to_e is a ref, so this inserts from_e -> to_e
+      std::string name;
+      Type type = from->exportType(from_e.getType(), to, vmap);
+      if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) {
+        to_e = to->mkVar(name, type);// FIXME thread safety
+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 {
+        to_e = to->mkVar(type);// FIXME thread safety
+Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl;
+      }
+      uint64_t to_int = (uint64_t)(to_e.getNode().d_nv);
+      uint64_t from_int = (uint64_t)(from_e.getNode().d_nv);
+      vmap.d_from[to_int] = from_int;
+      vmap.d_to[from_int] = to_int;
+      vmap.d_typeMap[to_e] = from_e;// insert other direction too
+      return Node::fromExpr(to_e);
+    }
+  } else {
+    std::vector<Node> children;
+Debug("export") << "n: " << n << std::endl;
+    if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl;
+      children.reserve(n.getNumChildren() + 1);
+      children.push_back(exportInternal(n.getOperator(), from, to, vmap));
+    } else {
+      children.reserve(n.getNumChildren());
+    }
+    for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
+Debug("export") << "+ child: " << *i << std::endl;
+      children.push_back(exportInternal(*i, from, to, vmap));
+    }
+    if(Debug.isOn("export")) {
+      ExprManagerScope ems(*to);
+      Debug("export") << "children for export from " << n << std::endl;
+      for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) {
+        Debug("export") << "  child: " << *i << std::endl;
+      }
+    }
+    return NodeManager::fromExprManager(to)->mkNode(n.getKind(), children);// FIXME thread safety
+  }
+}/* exportInternal() */
+
+}/* CVC4::expr namespace */
+
+Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  Assert(d_exprManager != exprManager,
+         "No sense in cloning an Expr in the same ExprManager");
+  ExprManagerScope ems(*this);
+  return Expr(exprManager, new Node(expr::exportInternal(*d_node, d_exprManager, exprManager, variableMap)));
+}
+
 Expr& Expr::operator=(const Expr& e) {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
@@ -449,4 +517,16 @@ void Expr::debugPrint() {
 
 ${getConst_implementations}
 
+namespace expr {
+
+static Node exportConstant(TNode n, NodeManager* to) {
+  Assert(n.getMetaKind() == kind::metakind::CONSTANT);
+  switch(n.getKind()) {
+${exportConstant_cases}
+
+  default: Unhandled(n.getKind());
+  }
+}/* exportConstant() */
+
+}/* CVC4::expr namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index b54ec20d4..56396da01 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -49,6 +49,8 @@ namespace CVC4 {
 template <bool ref_count>
 class NodeTemplate;
 
+class NodeManager;
+
 class Expr;
 class ExprManager;
 class SmtEngine;
@@ -56,6 +58,20 @@ class Type;
 class TypeCheckingException;
 class TypeCheckingExceptionPrivate;
 
+namespace expr {
+  namespace pickle {
+    class Pickler;
+  }/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+
+namespace prop {
+  class SatSolver;
+}/* CVC4::prop namespace */
+
+class ExprManagerMapCollection;
+
+struct ExprHashFunction;
+
 namespace smt {
   class SmtEnginePrivate;
 }/* CVC4::smt namespace */
@@ -64,6 +80,8 @@ namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
   class CVC4_PUBLIC ExprPrintTypes;
   class CVC4_PUBLIC ExprSetLanguage;
+
+  NodeTemplate<true> exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
 }/* CVC4::expr namespace */
 
 /**
@@ -437,6 +455,13 @@ public:
   ExprManager* getExprManager() const;
 
   /**
+   * Maps this Expr into one for a different ExprManager, using
+   * variableMap for the translation and extending it with any new
+   * mappings.
+   */
+  Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+
+  /**
    * IOStream manipulator to set the maximum depth of Exprs when
    * pretty-printing.  -1 means print to any depth.  E.g.:
    *
@@ -510,6 +535,10 @@ protected:
   friend class ExprManager;
   friend class NodeManager;
   friend class TypeCheckingException;
+  friend class expr::pickle::Pickler;
+  friend class prop::SatSolver;
+  friend NodeTemplate<true> expr::exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
+
   friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
   template <bool ref_count> friend class NodeTemplate;
 
@@ -828,7 +857,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 832 "${template}"
+#line 861 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 69f7019ab..0cae68ed0 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -60,6 +60,7 @@ getConst_instantiations=
 getConst_implementations=
 mkConst_instantiations=
 mkConst_implementations=
+exportConstant_cases=
 
 seen_theory=false
 seen_theory_builtin=false
@@ -193,6 +194,8 @@ template <> $2 const & Expr::getConst() const {
   return d_node->getConst< $2 >();
 }
 "
+  exportConstant_cases="${exportConstant_cases}
+  case $1: return to->mkConst(n.getConst< $2 >());"
 }
 
 function check_theory_seen {
@@ -244,6 +247,7 @@ for var in \
     getConst_implementations \
     mkConst_instantiations \
     mkConst_implementations \
+    exportConstant_cases \
     typechecker_includes \
     typerules \
     ; do
diff --git a/src/expr/node.h b/src/expr/node.h
index 57b02b05b..37499c3bf 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -49,6 +49,12 @@ namespace CVC4 {
 class TypeNode;
 class NodeManager;
 
+namespace expr {
+  namespace pickle {
+    class PicklerPrivate;
+  }/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+
 template <bool ref_count>
 class NodeTemplate;
 
@@ -177,6 +183,9 @@ class NodeTemplate {
    */
   friend class expr::NodeValue;
 
+  friend class expr::pickle::PicklerPrivate;
+  friend Node expr::exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
+
   /** A convenient null-valued encapsulated pointer */
   static NodeTemplate s_null;
 
@@ -200,6 +209,7 @@ class NodeTemplate {
 
   friend class NodeTemplate<true>;
   friend class NodeTemplate<false>;
+  friend class TypeNode;
   friend class NodeManager;
 
   template <unsigned nchild_thresh>
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index ded7ad8fe..c5d41816e 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -928,7 +928,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
     // reference counts in this case.
     nv->d_nchildren = 0;
     nv->d_kind = d_nv->d_kind;
-    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+    nv->d_id = d_nm->next_id++;// FIXME multithreading
     nv->d_rc = 0;
     setUsed();
     if(Debug.isOn("gc")) {
@@ -1015,7 +1015,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
       }
       nv->d_nchildren = d_inlineNv.d_nchildren;
       nv->d_kind = d_inlineNv.d_kind;
-      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_id = d_nm->next_id++;// FIXME multithreading
       nv->d_rc = 0;
 
       std::copy(d_inlineNv.d_children,
@@ -1069,7 +1069,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
 
       crop();
       expr::NodeValue* nv = d_nv;
-      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_id = d_nm->next_id++;// FIXME multithreading
       d_nv = &d_inlineNv;
       d_nvMaxChildren = nchild_thresh;
       setUsed();
@@ -1118,7 +1118,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
     // reference counts in this case.
     nv->d_nchildren = 0;
     nv->d_kind = d_nv->d_kind;
-    nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+    nv->d_id = d_nm->next_id++;// FIXME multithreading
     nv->d_rc = 0;
     Debug("gc") << "creating node value " << nv
                 << " [" << nv->d_id << "]: " << *nv << "\n";
@@ -1194,7 +1194,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
       }
       nv->d_nchildren = d_inlineNv.d_nchildren;
       nv->d_kind = d_inlineNv.d_kind;
-      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_id = d_nm->next_id++;// FIXME multithreading
       nv->d_rc = 0;
 
       std::copy(d_inlineNv.d_children,
@@ -1248,7 +1248,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
       }
       nv->d_nchildren = d_nv->d_nchildren;
       nv->d_kind = d_nv->d_kind;
-      nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+      nv->d_id = d_nm->next_id++;// FIXME multithreading
       nv->d_rc = 0;
 
       std::copy(d_nv->d_children,
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 2bf0a864a..1d4b7d3d1 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -84,6 +84,7 @@ NodeManager::NodeManager(context::Context* ctxt,
   d_optionsAllocated(new Options()),
   d_options(d_optionsAllocated),
   d_statisticsRegistry(new StatisticsRegistry()),
+  next_id(0),
   d_attrManager(ctxt),
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
@@ -98,6 +99,7 @@ NodeManager::NodeManager(context::Context* ctxt,
   d_optionsAllocated(NULL),
   d_options(&options),
   d_statisticsRegistry(new StatisticsRegistry()),
+  next_id(0),
   d_attrManager(ctxt),
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3646e91c5..e446b7d71 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -88,6 +88,8 @@ class NodeManager {
 
   NodeValuePool d_nodeValuePool;
 
+  size_t next_id;
+
   expr::attr::AttributeManager d_attrManager;
 
   /** The associated ExprManager */
@@ -503,6 +505,60 @@ public:
                            const AttrKind& attr,
                            const typename AttrKind::value_type& value);
 
+  /**
+   * Retrieve an attribute for a TypeNode.
+   *
+   * @param n the type node
+   * @param attr an instance of the attribute kind to retrieve.
+   * @returns the attribute, if set, or a default-constructed
+   * <code>AttrKind::value_type</code> if not.
+   */
+  template <class AttrKind>
+  inline typename AttrKind::value_type
+  getAttribute(TypeNode n, const AttrKind& attr) const;
+
+  /**
+   * Check whether an attribute is set for a TypeNode.
+   *
+   * @param n the type node
+   * @param attr an instance of the attribute kind to check
+   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+   */
+  template <class AttrKind>
+  inline bool hasAttribute(TypeNode n,
+                           const AttrKind& attr) const;
+
+  /**
+   * Check whether an attribute is set for a TypeNode and, if so, retieve
+   * it.
+   *
+   * @param n the type node
+   * @param attr an instance of the attribute kind to check
+   * @param value a reference to an object of the attribute's value type.
+   * <code>value</code> will be set to the value of the attribute, if it is
+   * set for <code>nv</code>; otherwise, it will be set to the default value of
+   * the attribute.
+   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
+   */
+  template <class AttrKind>
+  inline bool getAttribute(TypeNode n,
+                           const AttrKind& attr,
+                           typename AttrKind::value_type& value) const;
+
+  /**
+   * Set an attribute for a type node.  If the node doesn't have the
+   * attribute, this function assigns one.  If the type node has one,
+   * this overwrites it.
+   *
+   * @param n the type node
+   * @param attr an instance of the attribute kind to set
+   * @param value the value of <code>attr</code> for <code>n</code>
+   */
+  template <class AttrKind>
+  inline void setAttribute(TypeNode n,
+                           const AttrKind& attr,
+                           const typename AttrKind::value_type& value);
+
   /** Get the (singleton) type for Booleans. */
   inline TypeNode booleanType();
 
@@ -762,6 +818,32 @@ NodeManager::setAttribute(TNode n, const AttrKind&,
   d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
 }
 
+template <class AttrKind>
+inline typename AttrKind::value_type
+NodeManager::getAttribute(TypeNode n, const AttrKind&) const {
+  return d_attrManager.getAttribute(n.d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::hasAttribute(TypeNode n, const AttrKind&) const {
+  return d_attrManager.hasAttribute(n.d_nv, AttrKind());
+}
+
+template <class AttrKind>
+inline bool
+NodeManager::getAttribute(TypeNode n, const AttrKind&,
+                          typename AttrKind::value_type& ret) const {
+  return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret);
+}
+
+template <class AttrKind>
+inline void
+NodeManager::setAttribute(TypeNode n, const AttrKind&,
+                          const typename AttrKind::value_type& value) {
+  d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
+}
+
 
 /** Get the (singleton) type for booleans. */
 inline TypeNode NodeManager::booleanType() {
@@ -965,7 +1047,7 @@ inline TypeNode NodeManager::mkSort() {
 
 inline TypeNode NodeManager::mkSort(const std::string& name) {
   TypeNode type = mkSort();
-  type.setAttribute(expr::VarNameAttr(), name);
+  setAttribute(type, expr::VarNameAttr(), name);
   return type;
 }
 
@@ -986,7 +1068,7 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor,
   nb << sortTag;
   nb.append(children);
   TypeNode type = nb.constructTypeNode();
-  type.setAttribute(expr::VarNameAttr(), name);
+  setAttribute(type, expr::VarNameAttr(), name);
   return type;
 }
 
@@ -997,8 +1079,8 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name,
   Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
   nb << sortTag;
   TypeNode type = nb.constructTypeNode();
-  type.setAttribute(expr::VarNameAttr(), name);
-  type.setAttribute(expr::SortArityAttr(), arity);
+  setAttribute(type, expr::VarNameAttr(), name);
+  setAttribute(type, expr::SortArityAttr(), arity);
   return type;
 }
 
@@ -1211,37 +1293,37 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
 
 inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
   Node n = mkVar(type);
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(expr::VarNameAttr(), name);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, expr::VarNameAttr(), name);
   return n;
 }
 
 inline Node* NodeManager::mkVarPtr(const std::string& name,
                                    const TypeNode& type) {
   Node* n = mkVarPtr(type);
-  n->setAttribute(TypeAttr(), type);
-  n->setAttribute(expr::VarNameAttr(), name);
+  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, expr::VarNameAttr(), name);
   return n;
 }
 
 inline Node NodeManager::mkVar(const TypeNode& type) {
   Node n = NodeBuilder<0>(this, kind::VARIABLE);
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(TypeCheckedAttr(), true);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, TypeCheckedAttr(), true);
   return n;
 }
 
 inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
-  n->setAttribute(TypeAttr(), type);
-  n->setAttribute(TypeCheckedAttr(), true);
+  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, TypeCheckedAttr(), true);
   return n;
 }
 
 inline Node NodeManager::mkSkolem(const TypeNode& type) {
   Node n = NodeBuilder<0>(this, kind::SKOLEM);
-  n.setAttribute(TypeAttr(), type);
-  n.setAttribute(TypeCheckedAttr(), true);
+  setAttribute(n, TypeAttr(), type);
+  setAttribute(n, TypeCheckedAttr(), true);
   return n;
 }
 
@@ -1282,7 +1364,7 @@ NodeClass NodeManager::mkConstInternal(const T& val) {
 
   nv->d_nchildren = 0;
   nv->d_kind = kind::metakind::ConstantMap<T>::kind;
-  nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+  nv->d_id = next_id++;// FIXME multithreading
   nv->d_rc = 0;
 
   //OwningTheory::mkConst(val);
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 89ac7ffca..970d2e0fc 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -33,8 +33,6 @@ using namespace std;
 namespace CVC4 {
 namespace expr {
 
-size_t NodeValue::next_id = 1;
-
 NodeValue NodeValue::s_null(0);
 
 string NodeValue::toString() const {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 95af57719..e5ecfbc48 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -126,8 +126,6 @@ class NodeValue {
   void inc();
   void dec();
 
-  static size_t next_id;
-
   /**
    * Uninitializing constructor for NodeBuilder's use.
    */
diff --git a/src/expr/pickle_data.cpp b/src/expr/pickle_data.cpp
new file mode 100644
index 000000000..1de8f2cf7
--- /dev/null
+++ b/src/expr/pickle_data.cpp
@@ -0,0 +1,60 @@
+/*********************                                                        */
+/*! \file pickle_data.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: taking, mdeters
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a "pickle" for expressions, CVC4-internal view
+ **
+ ** This is the CVC4-internal view (private data structure) for a
+ ** "pickle" for expressions.  The public-facing view is a "Pickle",
+ ** which just points to a PickleData.  A pickle is a binary
+ ** serialization of an expression that can be converted back into an
+ ** expression in the same or another ExprManager.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/pickle_data.h"
+#include "expr/expr.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/node_value.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/variable_type_map.h"
+#include "util/Assert.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+
+namespace CVC4 {
+namespace expr {
+namespace pickle {
+
+void PickleData::writeToStringStream(std::ostringstream& oss) const {
+  BlockDeque::const_iterator i = d_blocks.begin(), end = d_blocks.end();
+  for(; i != end; ++i) {
+    Block b = *i;
+    Assert(sizeof(b) * 8 == NBITS_BLOCK);
+    oss << b.d_body.d_data << " ";
+  }
+}
+
+std::string PickleData::toString() const {
+  std::ostringstream oss;
+  oss.flags(std::ios::oct | std::ios::showbase);
+  writeToStringStream(oss);
+  return oss.str();
+}
+
+}/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h
new file mode 100644
index 000000000..dab6e56c3
--- /dev/null
+++ b/src/expr/pickle_data.h
@@ -0,0 +1,122 @@
+/*********************                                                        */
+/*! \file pickle_data.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: taking, mdeters
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a "pickle" for expressions, CVC4-internal view
+ **
+ ** This is the CVC4-internal view (private data structure) for a
+ ** "pickle" for expressions.  The public-facing view is a "Pickle",
+ ** which just points to a PickleData.  A pickle is a binary
+ ** serialization of an expression that can be converted back into an
+ ** expression in the same or another ExprManager.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PICKLE_DATA_H
+#define __CVC4__PICKLE_DATA_H
+
+#include <sstream>
+#include <deque>
+#include <stack>
+#include <exception>
+
+#include "expr/expr.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/expr_manager.h"
+#include "expr/variable_type_map.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+
+namespace CVC4 {
+
+class NodeManager;
+
+namespace expr {
+namespace pickle {
+
+const unsigned NBITS_BLOCK = 32;
+const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND;
+const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
+const unsigned NBITS_CONSTBLOCKS = 32;
+
+struct BlockHeader {
+  unsigned d_kind          : NBITS_KIND;
+};/* struct BlockHeader */
+
+struct BlockHeaderOperator {
+  unsigned d_kind          : NBITS_KIND;
+  unsigned d_nchildren     : NBITS_NCHILDREN;
+  unsigned                 : NBITS_BLOCK - (NBITS_KIND + NBITS_NCHILDREN);
+};/* struct BlockHeaderOperator */
+
+struct BlockHeaderConstant {
+  unsigned d_kind          : NBITS_KIND;
+  unsigned d_constblocks   : NBITS_BLOCK - NBITS_KIND;
+};/* struct BlockHeaderConstant */
+
+struct BlockHeaderVariable {
+  unsigned d_kind          : NBITS_KIND;
+  unsigned                 : NBITS_BLOCK - NBITS_KIND;
+};/* struct BlockHeaderVariable */
+
+struct BlockBody  {
+  unsigned d_data          : NBITS_BLOCK;
+};/* struct BlockBody */
+
+union Block {
+  BlockHeader d_header;
+  BlockHeaderConstant d_headerConstant;
+  BlockHeaderOperator d_headerOperator;
+  BlockHeaderVariable d_headerVariable;
+
+  BlockBody d_body;
+};/* union Block */
+
+class PickleData {
+  typedef std::deque<Block> BlockDeque;
+  BlockDeque d_blocks;
+
+public:
+  PickleData& operator<<(Block b) {
+    enqueue(b);
+    return (*this);
+  }
+
+  std::string toString() const;
+
+  void enqueue(Block b) {
+    d_blocks.push_back(b);
+  }
+
+  Block dequeue() {
+    Block b = d_blocks.front();
+    d_blocks.pop_front();
+    return b;
+  }
+
+  bool empty() const { return d_blocks.empty(); }
+  uint32_t size() const { return d_blocks.size(); }
+
+  void swap(PickleData& other){
+    d_blocks.swap(other.d_blocks);
+  }
+
+  void writeToStringStream(std::ostringstream& oss) const;
+};/* class PickleData */
+
+}/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PICKLE_DATA_H */
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
new file mode 100644
index 000000000..f09c552d1
--- /dev/null
+++ b/src/expr/pickler.cpp
@@ -0,0 +1,477 @@
+/*********************                                                        */
+/*! \file pickler.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: taking, mdeters
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a "pickler" for expressions
+ **
+ ** This is a "pickler" for expressions.  It produces a binary
+ ** serialization of an expression that can be converted back
+ ** into an expression in the same or another ExprManager.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/pickler.h"
+#include "expr/pickle_data.h"
+#include "expr/expr.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/node_value.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/variable_type_map.h"
+#include "util/Assert.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
+#include "util/output.h"
+
+namespace CVC4 {
+namespace expr {
+namespace pickle {
+
+class PicklerPrivate {
+public:
+  typedef std::stack<Node> NodeStack;
+  NodeStack d_stack;
+
+  PickleData d_current;
+
+  Pickler& d_pickler;
+
+  NodeManager* const d_nm;
+
+  PicklerPrivate(Pickler& pickler, ExprManager* em) :
+    d_pickler(pickler),
+    d_nm(NodeManager::fromExprManager(em)) {
+  }
+
+  bool atDefaultState(){
+    return d_stack.empty() && d_current.empty();
+  }
+
+  /* Helper functions for toPickle */
+  void toCaseNode(TNode n) throw(AssertionException, PicklingException);
+  void toCaseVariable(TNode n) throw(AssertionException, PicklingException);
+  void toCaseConstant(TNode n);
+  void toCaseOperator(TNode n) throw(AssertionException, PicklingException);
+  void toCaseString(Kind k, const std::string& s);
+
+  /* Helper functions for toPickle */
+  Node fromCaseOperator(Kind k, uint32_t nchildren);
+  Node fromCaseConstant(Kind k, uint32_t nblocks);
+  std::string fromCaseString(uint32_t nblocks);
+  Node fromCaseVariable(Kind k);
+
+};/* class PicklerPrivate */
+
+static Block mkBlockBody4Chars(char a, char b, char c, char d) {
+  Block newBody;
+  newBody.d_body.d_data = (a << 24) | (b << 16) | (c << 8) | d;
+  return newBody;
+}
+
+static char getCharBlockBody(BlockBody body, int i) {
+  Assert(0 <= i && i <= 3);
+
+  switch(i) {
+  case 0: return (body.d_data & 0xff000000) >> 24;
+  case 1: return (body.d_data & 0x00ff0000) >> 16;
+  case 2: return (body.d_data & 0x0000ff00) >> 8;
+  case 3: return (body.d_data & 0x000000ff);
+  default:
+    Unreachable();
+  }
+  return '\0';
+}
+
+static Block mkBlockBody(unsigned data) {
+  Block newBody;
+  newBody.d_body.d_data = data;
+  return newBody;
+}
+
+static Block mkOperatorHeader(Kind k, unsigned numChildren) {
+  Block newHeader;
+  newHeader.d_headerOperator.d_kind = k;
+  newHeader.d_headerOperator.d_nchildren = numChildren;
+  return newHeader;
+}
+
+static Block mkVariableHeader(Kind k) {
+  Block newHeader;
+  newHeader.d_header.d_kind = k;
+  return newHeader;
+}
+
+static Block mkConstantHeader(Kind k, unsigned numBlocks) {
+  Block newHeader;
+  newHeader.d_headerConstant.d_kind = k;
+  newHeader.d_headerConstant.d_constblocks = numBlocks;
+  return newHeader;
+}
+
+Pickler::Pickler(ExprManager* em) :
+  d_private(new PicklerPrivate(*this, em)) {
+}
+
+Pickler::~Pickler() {
+  delete d_private;
+}
+
+void Pickler::toPickle(Expr e, Pickle& p)
+  throw(AssertionException, PicklingException) {
+  Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm);
+  Assert(d_private->atDefaultState());
+
+  try{
+    d_private->d_current.swap(*p.d_data);
+    d_private->toCaseNode(e.getTNode());
+    d_private->d_current.swap(*p.d_data);
+  }catch(PicklingException& pe){
+    d_private->d_current = PickleData();
+    Assert(d_private->atDefaultState());
+    throw pe;
+  }
+
+  Assert(d_private->atDefaultState());
+}
+
+void PicklerPrivate::toCaseNode(TNode n)
+  throw(AssertionException, PicklingException) {
+  Debug("pickler") << "toCaseNode: " << n << std::endl;
+  Kind k = n.getKind();
+  kind::MetaKind m = metaKindOf(k);
+  switch(m) {
+  case kind::metakind::CONSTANT:
+    toCaseConstant(n);
+    break;
+  case kind::metakind::VARIABLE:
+    toCaseVariable(n);
+    break;
+  case kind::metakind::OPERATOR:
+  case kind::metakind::PARAMETERIZED:
+    toCaseOperator(n);
+    break;
+  default:
+    Unhandled(m);
+  }
+}
+
+void PicklerPrivate::toCaseOperator(TNode n)
+  throw(AssertionException, PicklingException) {
+  Kind k = n.getKind();
+  kind::MetaKind m = metaKindOf(k);
+  Assert(m == kind::metakind::PARAMETERIZED || m == kind::metakind::OPERATOR);
+  if(m == kind::metakind::PARAMETERIZED) {
+    toCaseNode(n.getOperator());
+  }
+  for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) {
+    toCaseNode(*i);
+  }
+  d_current << mkOperatorHeader(k, n.getNumChildren());
+}
+
+void PicklerPrivate::toCaseVariable(TNode n)
+  throw(AssertionException, PicklingException) {
+  Kind k = n.getKind();
+  Assert(metaKindOf(k) == kind::metakind::VARIABLE);
+
+  const NodeValue* nv = n.d_nv;
+  uint64_t asInt = reinterpret_cast<uint64_t>(nv);
+  uint64_t mapped = d_pickler.variableToMap(asInt);
+
+  uint32_t firstHalf = mapped >> 32;
+  uint32_t secondHalf = mapped & 0xffffffff;
+
+  d_current << mkVariableHeader(k);
+  d_current << mkBlockBody(firstHalf);
+  d_current << mkBlockBody(secondHalf);
+}
+
+
+void PicklerPrivate::toCaseConstant(TNode n) {
+  Kind k = n.getKind();
+  Assert(metaKindOf(k) == kind::metakind::CONSTANT);
+  switch(k) {
+  case kind::CONST_BOOLEAN:
+    d_current << mkConstantHeader(k, 1);
+    d_current << mkBlockBody(n.getConst<bool>());
+    break;
+  case kind::CONST_INTEGER:
+  case kind::CONST_RATIONAL: {
+    std::string asString;
+    if(k == kind::CONST_INTEGER) {
+      const Integer& i = n.getConst<Integer>();
+      asString = i.toString(16);
+    } else {
+      Assert(k == kind::CONST_RATIONAL);
+      const Rational& q = n.getConst<Rational>();
+      asString = q.toString(16);
+    }
+    toCaseString(k, asString);
+    break;
+  }
+  case kind::BITVECTOR_EXTRACT_OP: {
+    BitVectorExtract bve = n.getConst<BitVectorExtract>();
+    d_current << mkConstantHeader(k, 2);
+    d_current << mkBlockBody(bve.high);
+    d_current << mkBlockBody(bve.low);
+    break;
+  }
+  case kind::CONST_BITVECTOR: {
+    // irritating: we incorporate the size of the string in with the
+    // size of this constant, so it appears as one big constant and
+    // doesn't confuse anybody
+    BitVector bv = n.getConst<BitVector>();
+    std::string asString = bv.getValue().toString(16);
+    d_current << mkConstantHeader(k, 2 + asString.size());
+    d_current << mkBlockBody(bv.getSize());
+    toCaseString(k, asString);
+    break;
+  }
+  default:
+    Unhandled(k);
+  }
+}
+
+void PicklerPrivate::toCaseString(Kind k, const std::string& s) {
+  d_current << mkConstantHeader(k, s.size());
+
+  unsigned size = s.size();
+  unsigned i;
+  for(i = 0; i + 4 <= size; i += 4) {
+    d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], s[i + 3]);
+  }
+  switch(size % 4) {
+  case 0: break;
+  case 1: d_current << mkBlockBody4Chars(s[i + 0], '\0','\0', '\0'); break;
+  case 2: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1], '\0', '\0'); break;
+  case 3: d_current << mkBlockBody4Chars(s[i + 0], s[i + 1],s[i + 2], '\0'); break;
+  default:
+    Unreachable();
+  }
+
+}
+
+void Pickler::debugPickleTest(Expr e) {
+
+  //ExprManager *em = e.getExprManager();
+  //Expr e1 = mkVar("x", makeType());
+  //return ;
+
+  Pickler pickler(e.getExprManager());
+
+  Pickle p;
+  pickler.toPickle(e, p);
+
+  uint32_t size = p.d_data->size();
+  std::string str = p.d_data->toString();
+
+  Expr from = pickler.fromPickle(p);
+  ExprManagerScope ems(e);
+
+  Debug("pickle") << "before: " << e << std::endl;
+  Debug("pickle") << "after: " << from.getNode() << std::endl;
+  Debug("pickle") << "pickle: (oct) "<< size << " " << str.length() << " " << str << std::endl;
+
+  Assert(p.d_data->empty());
+  Assert(e == from);
+}
+
+Expr Pickler::fromPickle(Pickle& p) {
+  Assert(d_private->atDefaultState());
+
+  d_private->d_current.swap(*p.d_data);
+
+  while(!d_private->d_current.empty()) {
+    Block front = d_private->d_current.dequeue();
+
+    Kind k = (Kind)front.d_header.d_kind;
+    kind::MetaKind m = metaKindOf(k);
+
+    Node result = Node::null();
+    switch(m) {
+    case kind::metakind::VARIABLE:
+      result = d_private->fromCaseVariable(k);
+      break;
+    case kind::metakind::CONSTANT:
+      result = d_private->fromCaseConstant(k, front.d_headerConstant.d_constblocks);
+      break;
+    case kind::metakind::OPERATOR:
+    case kind::metakind::PARAMETERIZED:
+      result = d_private->fromCaseOperator(k, front.d_headerOperator.d_nchildren);
+      break;
+    default:
+      Unhandled(m);
+    }
+    Assert(result != Node::null());
+    d_private->d_stack.push(result);
+  }
+
+  Assert(d_private->d_current.empty());
+  Assert(d_private->d_stack.size() == 1);
+  Node res = d_private->d_stack.top();
+  d_private->d_stack.pop();
+
+  Assert(d_private->atDefaultState());
+
+  return d_private->d_nm->toExpr(res);
+}
+
+Node PicklerPrivate::fromCaseVariable(Kind k) {
+  Assert(metaKindOf(k) == kind::metakind::VARIABLE);
+
+  Block firstHalf = d_current.dequeue();
+  Block secondHalf = d_current.dequeue();
+
+  uint64_t asInt = firstHalf.d_body.d_data;
+  asInt = asInt << 32;
+  asInt = asInt | (secondHalf.d_body.d_data);
+
+  uint64_t mapped = d_pickler.variableFromMap(asInt);
+
+  NodeValue* nv = reinterpret_cast<NodeValue*>(mapped);
+  Node fromNodeValue(nv);
+
+  Assert(fromNodeValue.getKind() == k);
+
+  return fromNodeValue;
+}
+
+Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) {
+  switch(k) {
+  case kind::CONST_BOOLEAN: {
+    Assert(constblocks == 1);
+    Block val = d_current.dequeue();
+
+    bool b= val.d_body.d_data;
+    return d_nm->mkConst<bool>(b);
+  }
+  case kind::CONST_INTEGER:
+  case kind::CONST_RATIONAL: {
+    std::string s = fromCaseString(constblocks);
+    if(k == kind::CONST_INTEGER) {
+      Integer i(s, 16);
+      return d_nm->mkConst<Integer>(i);
+    } else {
+      Rational q(s, 16);
+      return d_nm->mkConst<Rational>(q);
+    }
+  }
+  case kind::BITVECTOR_EXTRACT_OP: {
+    Block high = d_current.dequeue();
+    Block low = d_current.dequeue();
+    BitVectorExtract bve(high.d_body.d_data, low.d_body.d_data);
+    return d_nm->mkConst<BitVectorExtract>(bve);
+  }
+  case kind::CONST_BITVECTOR: {
+    unsigned size = d_current.dequeue().d_body.d_data;
+    Block header CVC4_UNUSED = d_current.dequeue();
+    Assert(header.d_headerConstant.d_kind == kind::CONST_BITVECTOR);
+    Assert(header.d_headerConstant.d_constblocks == constblocks - 2);
+    Integer value(fromCaseString(constblocks - 2));
+    BitVector bv(size, value);
+    return d_nm->mkConst(bv);
+  }
+  default:
+    Unhandled(k);
+  }
+}
+
+std::string PicklerPrivate::fromCaseString(uint32_t size) {
+  std::stringstream ss;
+  unsigned i;
+  for(i = 0; i + 4 <= size; i += 4) {
+    Block front = d_current.dequeue();
+    BlockBody body = front.d_body;
+
+    ss << getCharBlockBody(body,0)
+       << getCharBlockBody(body,1)
+       << getCharBlockBody(body,2)
+       << getCharBlockBody(body,3);
+  }
+  Assert(i == size - (size%4) );
+  if(size % 4 != 0) {
+    Block front = d_current.dequeue();
+    BlockBody body = front.d_body;
+    switch(size % 4) {
+    case 1:
+      ss << getCharBlockBody(body,0);
+      break;
+    case 2:
+      ss << getCharBlockBody(body,0)
+         << getCharBlockBody(body,1);
+      break;
+    case 3:
+      ss << getCharBlockBody(body,0)
+         << getCharBlockBody(body,1)
+         << getCharBlockBody(body,2);
+      break;
+    default:
+      Unreachable();
+    }
+  }
+  return ss.str();
+}
+
+Node PicklerPrivate::fromCaseOperator(Kind k, uint32_t nchildren) {
+  kind::MetaKind m = metaKindOf(k);
+  bool parameterized = (m == kind::metakind::PARAMETERIZED);
+  uint32_t npops = nchildren + (parameterized? 1 : 0);
+
+  NodeStack aux;
+  while(npops > 0) {
+    Assert(!d_stack.empty());
+    Node top = d_stack.top();
+    aux.push(top);
+    d_stack.pop();
+    --npops;
+  }
+
+  NodeBuilder<> nb(d_nm, k);
+  while(!aux.empty()) {
+    Node top = aux.top();
+    nb << top;
+    aux.pop();
+  }
+
+  return nb;
+}
+
+Pickle::Pickle() {
+  d_data = new PickleData();
+}
+
+// Just copying the pointer isn't right, we have to copy the
+// underlying data.  Otherwise user-level Pickles will delete the data
+// twice! (once in each thread)
+Pickle::Pickle(const Pickle& p) {
+  d_data = new PickleData(*p.d_data);
+}
+
+Pickle& Pickle::operator = (const Pickle& other) {
+  if (this != &other) {
+    delete d_data;
+    d_data = new PickleData(*other.d_data);
+  }
+  return *this;
+}
+
+
+Pickle::~Pickle() {
+  delete d_data;
+}
+
+}/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
diff --git a/src/expr/pickler.h b/src/expr/pickler.h
new file mode 100644
index 000000000..264ae0e4b
--- /dev/null
+++ b/src/expr/pickler.h
@@ -0,0 +1,139 @@
+/*********************                                                        */
+/*! \file pickle.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: taking, mdeters
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a "pickler" for expressions
+ **
+ ** This is a "pickler" for expressions.  It produces a binary
+ ** serialization of an expression that can be converted back
+ ** into an expression in the same or another ExprManager.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__PICKLER_H
+#define __CVC4__PICKLER_H
+
+#include "expr/variable_type_map.h"
+#include "expr/expr.h"
+#include "util/exception.h"
+
+#include <exception>
+#include <stack>
+
+namespace CVC4 {
+
+class ExprManager;
+
+namespace expr {
+namespace pickle {
+
+class Pickler;
+class PicklerPrivate;
+
+class PickleData;// CVC4-internal representation
+
+class CVC4_PUBLIC Pickle {
+  PickleData* d_data;
+  friend class Pickler;
+  friend class PicklerPrivate;
+public:
+  Pickle();
+  Pickle(const Pickle& p);
+  ~Pickle();
+  Pickle& operator = (const Pickle& other);
+};/* class Pickle */
+
+class CVC4_PUBLIC PicklingException : public Exception {
+public:
+  PicklingException() :
+    Exception("Pickling failed") {
+  }
+};/* class PicklingException */
+
+class CVC4_PUBLIC Pickler {
+  PicklerPrivate* d_private;
+
+  friend class PicklerPrivate;
+
+protected:
+  virtual uint64_t variableToMap(uint64_t x) const
+    throw(AssertionException, PicklingException) {
+    return x;
+  }
+  virtual uint64_t variableFromMap(uint64_t x) const {
+    return x;
+  }
+
+public:
+  Pickler(ExprManager* em);
+  ~Pickler();
+
+  /**
+   * Constructs a new Pickle of the node n.
+   * n must be a node allocated in the node manager specified at initialization
+   * time. The new pickle has variables mapped using the VariableIDMap provided
+   * at initialization.
+   * TODO: Fix comment
+   *
+   * @return the pickle, which should be dispose()'d when you're done with it
+   */
+  void toPickle(Expr e, Pickle& p) throw(AssertionException, PicklingException);
+
+  /**
+   * Constructs a node from a Pickle.
+   * This destroys the contents of the Pickle.
+   * The node is created in the NodeManager getNM();
+   * TODO: Fix comment
+   */
+  Expr fromPickle(Pickle& p);
+
+  static void debugPickleTest(Expr e);
+
+};/* class Pickler */
+
+class MapPickler : public Pickler {
+private:
+  const VarMap& d_toMap;
+  const VarMap& d_fromMap;
+
+public:
+  MapPickler(ExprManager* em, const VarMap& to, const VarMap& from):
+    Pickler(em),
+    d_toMap(to),
+    d_fromMap(from) {
+  }
+
+protected:
+
+  virtual uint64_t variableToMap(uint64_t x) const
+    throw(AssertionException, PicklingException){
+    VarMap::const_iterator i = d_toMap.find(x);
+    if(i != d_toMap.end()){
+      return i->second;
+    }else{
+      throw PicklingException();
+    }
+  }
+
+  virtual uint64_t variableFromMap(uint64_t x) const {
+    VarMap::const_iterator i = d_fromMap.find(x);
+    Assert(i != d_fromMap.end());
+    return i->second;
+  }
+};/* class MapPickler */
+
+}/* CVC4::expr::pickle namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PICKLER_H */
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 7e06a05ae..a901af73a 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -162,6 +162,10 @@ ExprManager* Type::getExprManager() const {
   return d_nodeManager->toExprManager();
 }
 
+Type Type::exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) {
+  return ExprManager::exportType(*this, exprManager, vmap);
+}
+
 void Type::toStream(std::ostream& out) const {
   NodeManagerScope nms(d_nodeManager);
   out << *d_typeNode;
diff --git a/src/expr/type.h b/src/expr/type.h
index 0b50fbd3c..34cc925f6 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -35,6 +35,7 @@ class NodeManager;
 class ExprManager;
 class Expr;
 class TypeNode;
+class ExprManagerMapCollection;
 
 class SmtEngine;
 
@@ -75,6 +76,10 @@ struct CVC4_PUBLIC TypeHashFunction {
  */
 std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
 
+namespace expr {
+  TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
+}/* CVC4::expr namespace */
+
 /**
  * Class encapsulating CVC4 expression types.
  */
@@ -86,6 +91,7 @@ class CVC4_PUBLIC Type {
   friend class TypeNode;
   friend struct TypeHashStrategy;
   friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t);
+  friend TypeNode expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
 
 protected:
 
@@ -166,6 +172,11 @@ public:
   ExprManager* getExprManager() const;
 
   /**
+   * Exports this type into a different ExprManager.
+   */
+  Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap);
+
+  /**
    * Assignment operator.
    * @param t the type to assign to this type
    * @return this type after assignment.
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 553f83276..c7da5ceb7 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -229,6 +229,16 @@ public:
   }
 
   /**
+   * PARAMETERIZED-metakinded types (the SORT_TYPE is one of these)
+   * have an operator.  "Little-p parameterized" types (like Array),
+   * are OPERATORs, not PARAMETERIZEDs.
+   */
+  inline Node getOperator() const {
+    Assert(getMetaKind() == kind::metakind::PARAMETERIZED);
+    return Node(d_nv->getChild(-1));
+  }
+
+  /**
    * Returns the unique id of this node
    *
    * @return the id
diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h
new file mode 100644
index 000000000..a34bec846
--- /dev/null
+++ b/src/expr/variable_type_map.h
@@ -0,0 +1,64 @@
+/*********************                                                        */
+/*! \file variable_type_map.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__VARIABLE_TYPE_MAP_H
+#define __CVC4__VARIABLE_TYPE_MAP_H
+
+#include "expr/expr.h"
+#include "util/hash.h"
+
+namespace CVC4 {
+
+class Expr;
+struct ExprHashFunction;
+class Type;
+struct TypeHashFunction;
+
+class CVC4_PUBLIC VariableTypeMap {
+  /**
+   * A map Expr -> Expr, intended to be used for a mapping of variables
+   * between two ExprManagers.
+   */
+  std::hash_map<Expr, Expr, ExprHashFunction> d_variables;
+
+  /**
+   * A map Type -> Type, intended to be used for a mapping of types
+   * between two ExprManagers.
+   */
+  std::hash_map<Type, Type, TypeHashFunction> d_types;
+
+public:
+  Expr& operator[](Expr e) { return d_variables[e]; }
+  Type& operator[](Type t) { return d_types[t]; }
+
+};/* class VariableTypeMap */
+
+typedef __gnu_cxx::hash_map<uint64_t, uint64_t> VarMap;
+
+struct CVC4_PUBLIC ExprManagerMapCollection {
+  VariableTypeMap d_typeMap;
+  VarMap d_to;
+  VarMap d_from;
+};
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__VARIABLE_MAP_H */