diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-21 13:52:34 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-21 13:57:50 -0500 |
commit | 761c1e709a5c3a8013d1da19ca7083cc8e9b2ed3 (patch) | |
tree | a56da902cfe38e260fc5cb8a59f11bacfeeecfdf /src/expr | |
parent | f156fc77b30142dcf33d15bdd04c11056281c3ba (diff) |
portfolio: fix export of emptyset
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 5 |
2 files changed, 6 insertions, 1 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} |