From 761c1e709a5c3a8013d1da19ca7083cc8e9b2ed3 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 21 Feb 2014 13:52:34 -0500
Subject: [PATCH] portfolio: fix export of emptyset

---
 src/expr/expr_manager_template.cpp | 2 +-
 src/expr/expr_template.cpp         | 5 +++++
 src/smt/smt_engine.cpp             | 4 ++--
 3 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 41f69e587..c733e37ea 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -934,7 +934,7 @@ 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;
+  Debug("export") << "type: " << n << " " << n.getId() << std::endl;
   if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
     throw ExportUnsupportedException
       ("export of types belonging to theory of DATATYPES kinds unsupported");
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index f7e5498dd..60f34867c 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -135,6 +135,10 @@ public:
     }
 
     if(n.getMetaKind() == metakind::CONSTANT) {
+      if(n.getKind() == kind::EMPTYSET) {
+        Type type = from->exportType(n.getConst< ::CVC4::EmptySet >().getType(), to, vmap);
+        return to->mkConst(::CVC4::EmptySet(type));
+      }
       return exportConstant(n, NodeManager::fromExprManager(to));
     } else if(n.isVar()) {
       Expr from_e(from, new Node(n));
@@ -572,6 +576,7 @@ namespace expr {
 
 static Node exportConstant(TNode n, NodeManager* to) {
   Assert(n.isConst());
+  Debug("export") << "constant: " << n << std::endl;
   switch(n.getKind()) {
 ${exportConstant_cases}
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4ab8cb548..9abd6e165 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1439,9 +1439,9 @@ void SmtEngine::defineFunction(Expr func,
       stringstream ss;
       ss << "Declared type of defined constant does not match its definition\n"
          << "The constant   : " << func << "\n"
-         << "Declared type  : " << funcType << "\n"
+         << "Declared type  : " << funcType << " " << Type::getTypeNode(funcType)->getId() << "\n"
          << "The definition : " << formula << "\n"
-         << "Definition type: " << formulaType;
+         << "Definition type: " << formulaType << " " << Type::getTypeNode(formulaType)->getId();
       throw TypeCheckingException(func, ss.str());
     }
   }
-- 
2.30.2