diff options
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 2 | ||||
| -rw-r--r-- | src/expr/expr_template.cpp | 5 | ||||
| -rw-r--r-- | src/expr/node.h | 6 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 | ||||
| -rw-r--r-- | test/system/Makefile.am | 4 |
5 files changed, 14 insertions, 7 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/expr/node.h b/src/expr/node.h index e7c51f0e2..9ada7879c 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1376,7 +1376,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, NodeBuilder<> nb(getKind()); if(getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator - nb << getOperator(); + nb << getOperator().substitute(nodesBegin, nodesEnd, + replacementsBegin, replacementsEnd, + cache); } for(const_iterator i = begin(), iend = end(); @@ -1427,7 +1429,7 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin, NodeBuilder<> nb(getKind()); if(getMetaKind() == kind::metakind::PARAMETERIZED) { // push the operator - nb << getOperator(); + nb << getOperator().substitute(substitutionsBegin, substitutionsEnd, cache); } for(const_iterator i = begin(), iend = end(); 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()); } } diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 0306afa68..6d278409e 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -85,8 +85,8 @@ LIBADD += \ @abs_top_builddir@/src/libcvc4.la # WHEN SYSTEM TESTS ARE ADDED, BUILD LIKE THIS: -$(filter-out %.class.lo,$(TESTS:%=%.lo)): %.lo: %.cpp - $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@ $+ +$(filter-out %.class.lo,$(TESTS:%=%.lo)): %.lo: %.cpp $(LIBADD) + $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@ $< $(filter-out %.class,$(TESTS)): %: %.lo $(LIBADD) $(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $(LIBS) $< CVC4JavaTest.class: CVC4JavaTest.java @abs_top_builddir@/src/bindings/CVC4.jar @abs_top_builddir@/src/bindings/java/libcvc4jni.la |