summaryrefslogtreecommitdiff
path: root/src/expr/expr_template.h
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2013-12-06 19:05:35 -0500
committerKshitij Bansal <kshitij@cs.nyu.edu>2013-12-07 03:01:37 -0500
commit6ea2b0056a34131dbaf27ec1570dc631208f8ca6 (patch)
tree4c68ca9fa72cf381f18e63127cf1e5593883bfe1 /src/expr/expr_template.h
parent75216dadbf77ca6800383018e12491e337912f3f (diff)
fix bug 542
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r--src/expr/expr_template.h5
1 files changed, 2 insertions, 3 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index ace14a10b..756145bda 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -81,7 +81,7 @@ namespace expr {
class CVC4_PUBLIC ExprDag;
class CVC4_PUBLIC ExprSetLanguage;
- NodeTemplate<true> exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags);
+ class ExportPrivate;
}/* CVC4::expr namespace */
/**
@@ -591,8 +591,7 @@ private:
friend class TypeCheckingException;
friend class expr::pickle::Pickler;
friend class prop::TheoryProxy;
- friend NodeTemplate<true> expr::exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags);
-
+ friend class expr::ExportPrivate;
friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
template <bool ref_count> friend class NodeTemplate;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback