portfolio merge

1 files changed, 12 insertions, 0 deletions

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);