diff options
-rw-r--r-- | src/expr/node.cpp | 12 | ||||
-rw-r--r-- | src/expr/node.h | 12 |
2 files changed, 24 insertions, 0 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp index b983c81f5..33322588f 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -112,4 +112,16 @@ bool NodeTemplate<ref_count>::isConst() const { template bool NodeTemplate<true>::isConst() const; template bool NodeTemplate<false>::isConst() const; +template class NodeTemplate<true>; +template class NodeTemplate<false>; + }/* CVC4 namespace */ + +namespace std { +template class std::vector<CVC4::NodeTemplate<true>>; +template class std::vector<CVC4::NodeTemplate<false>>; +template class std::unordered_map<CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true>, CVC4::NodeHashFunction>; +template class std::unordered_map<CVC4::NodeTemplate<false>, CVC4::NodeTemplate<false>, CVC4::TNodeHashFunction>; +template class std::map<CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true> >; +template class std::map<CVC4::NodeTemplate<false>, CVC4::NodeTemplate<false> >; +} diff --git a/src/expr/node.h b/src/expr/node.h index 4b12c7ece..8b21c7881 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1507,6 +1507,9 @@ inline Node NodeTemplate<true>::fromExpr(const Expr& e) { return NodeManager::fromExpr(e); } +extern template class NodeTemplate<true>; +extern template class NodeTemplate<false>; + #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used @@ -1568,4 +1571,13 @@ static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& }/* CVC4 namespace */ +namespace std { +extern template class std::vector<CVC4::NodeTemplate<true>>; +extern template class std::vector<CVC4::NodeTemplate<false>>; +extern template class std::unordered_map<CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true>, CVC4::NodeHashFunction>; +extern template class std::unordered_map<CVC4::NodeTemplate<false>, CVC4::NodeTemplate<false>, CVC4::TNodeHashFunction>; +extern template class std::map<CVC4::NodeTemplate<true>, CVC4::NodeTemplate<true> >; +extern template class std::map<CVC4::NodeTemplate<false>, CVC4::NodeTemplate<false> >; +} + #endif /* __CVC4__NODE_H */ |