summaryrefslogtreecommitdiff
path: root/src/expr/expr_template.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r--src/expr/expr_template.cpp91
1 files changed, 54 insertions, 37 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 998f58d0c..3ed72e03e 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -156,13 +156,20 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v
class ExportPrivate {
private:
typedef std::unordered_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache;
- ExprManager* from;
- ExprManager* to;
- ExprManagerMapCollection& vmap;
- uint32_t flags;
- ExportCache exportCache;
-public:
- ExportPrivate(ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags) : from(from), to(to), vmap(vmap), flags(flags) {}
+ ExprManager* d_from;
+ ExprManager* d_to;
+ ExprManagerMapCollection& d_vmap;
+ uint32_t d_flags;
+ ExportCache d_exportCache;
+
+ public:
+ ExportPrivate(ExprManager* from,
+ ExprManager* to,
+ ExprManagerMapCollection& vmap,
+ uint32_t flags)
+ : d_from(from), d_to(to), d_vmap(vmap), d_flags(flags)
+ {
+ }
Node exportInternal(TNode n) {
if(n.isNull()) return Node::null();
@@ -173,17 +180,18 @@ 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));
+ Type type = d_from->exportType(
+ n.getConst< ::CVC4::EmptySet>().getType(), d_to, d_vmap);
+ return d_to->mkConst(::CVC4::EmptySet(type));
}
- return exportConstant(n, NodeManager::fromExprManager(to), vmap);
+ return exportConstant(n, NodeManager::fromExprManager(d_to), d_vmap);
} else if(n.getMetaKind() == metakind::NULLARY_OPERATOR ){
- Expr from_e(from, new Node(n));
- Type type = from->exportType(from_e.getType(), to, vmap);
- return to->mkNullaryOperator(type, n.getKind()); // FIXME thread safety
+ Expr from_e(d_from, new Node(n));
+ Type type = d_from->exportType(from_e.getType(), d_to, d_vmap);
+ return d_to->mkNullaryOperator(type, n.getKind()); // FIXME thread safety
} else if(n.getMetaKind() == metakind::VARIABLE) {
- Expr from_e(from, new Node(n));
- Expr& to_e = vmap.d_typeMap[from_e];
+ Expr from_e(d_from, new Node(n));
+ Expr& to_e = d_vmap.d_typeMap[from_e];
if(! to_e.isNull()) {
Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl;
return to_e.getNode();
@@ -191,20 +199,20 @@ public:
// construct new variable in other manager:
// to_e is a ref, so this inserts from_e -> to_e
std::string name;
- Type type = from->exportType(from_e.getType(), to, vmap);
+ Type type = d_from->exportType(from_e.getType(), d_to, d_vmap);
if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) {
if (n.getKind() == kind::BOUND_VARIABLE)
{
// bound vars are only available at the Node level (not the Expr
// level)
TypeNode typeNode = TypeNode::fromType(type);
- NodeManager* to_nm = NodeManager::fromExprManager(to);
- Node n = to_nm->mkBoundVar(name, typeNode); // FIXME thread safety
+ NodeManager* to_nm = NodeManager::fromExprManager(d_to);
+ Node nn = to_nm->mkBoundVar(name, typeNode); // FIXME thread safety
// Make sure that the correct `NodeManager` is in scope while
// converting the node to an expression.
NodeManagerScope to_nms(to_nm);
- to_e = n.toExpr();
+ to_e = nn.toExpr();
} else if(n.getKind() == kind::VARIABLE) {
bool isGlobal;
Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal);
@@ -212,17 +220,24 @@ public:
// Temporarily set the node manager to nullptr; this gets around
// a check that mkVar isn't called internally
NodeManagerScope nullScope(nullptr);
- to_e = to->mkVar(name, type, isGlobal ? ExprManager::VAR_FLAG_GLOBAL : flags);// FIXME thread safety
+ to_e = d_to->mkVar(name,
+ type,
+ isGlobal ? ExprManager::VAR_FLAG_GLOBAL
+ : d_flags); // FIXME thread safety
} else if(n.getKind() == kind::SKOLEM) {
// skolems are only available at the Node level (not the Expr level)
TypeNode typeNode = TypeNode::fromType(type);
- NodeManager* to_nm = NodeManager::fromExprManager(to);
- Node n = to_nm->mkSkolem(name, typeNode, "is a skolem variable imported from another ExprManager");// FIXME thread safety
+ NodeManager* to_nm = NodeManager::fromExprManager(d_to);
+ Node nn =
+ to_nm->mkSkolem(name,
+ typeNode,
+ "is a skolem variable imported from another "
+ "ExprManager"); // FIXME thread safety
// Make sure that the correct `NodeManager` is in scope while
// converting the node to an expression.
NodeManagerScope to_nms(to_nm);
- to_e = n.toExpr();
+ to_e = nn.toExpr();
} else {
Unhandled();
}
@@ -234,38 +249,39 @@ public:
// bound vars are only available at the Node level (not the Expr
// level)
TypeNode typeNode = TypeNode::fromType(type);
- NodeManager* to_nm = NodeManager::fromExprManager(to);
- Node n = to_nm->mkBoundVar(typeNode); // FIXME thread safety
+ NodeManager* to_nm = NodeManager::fromExprManager(d_to);
+ Node nn = to_nm->mkBoundVar(typeNode); // FIXME thread safety
// Make sure that the correct `NodeManager` is in scope while
// converting the node to an expression.
NodeManagerScope to_nms(to_nm);
- to_e = n.toExpr();
+ to_e = nn.toExpr();
}
else
{
// Temporarily set the node manager to nullptr; this gets around
// a check that mkVar isn't called internally
NodeManagerScope nullScope(nullptr);
- to_e = to->mkVar(type); // FIXME thread safety
+ to_e = d_to->mkVar(type); // FIXME thread safety
}
Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl;
}
uint64_t to_int = (uint64_t)(to_e.getNode().d_nv);
uint64_t from_int = (uint64_t)(from_e.getNode().d_nv);
- vmap.d_from[to_int] = from_int;
- vmap.d_to[from_int] = to_int;
- vmap.d_typeMap[to_e] = from_e;// insert other direction too
+ d_vmap.d_from[to_int] = from_int;
+ d_vmap.d_to[from_int] = to_int;
+ d_vmap.d_typeMap[to_e] = from_e; // insert other direction too
// Make sure that the expressions are associated with the correct
// `ExprManager`s.
- Assert(from_e.getExprManager() == from);
- Assert(to_e.getExprManager() == to);
+ Assert(from_e.getExprManager() == d_from);
+ Assert(to_e.getExprManager() == d_to);
return Node::fromExpr(to_e);
}
} else {
- if(exportCache.find(n) != exportCache.end()) {
- return exportCache[n];
+ if (d_exportCache.find(n) != d_exportCache.end())
+ {
+ return d_exportCache[n];
}
std::vector<Node> children;
@@ -286,16 +302,17 @@ public:
// `n` belongs to the `from` ExprManager, so begin ExprManagerScope
// after printing `n`
- ExprManagerScope ems(*to);
+ ExprManagerScope ems(*d_to);
for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) {
Debug("export") << " child: " << *i << std::endl;
}
}
// FIXME thread safety
- Node ret = NodeManager::fromExprManager(to)->mkNode(n.getKind(), children);
+ Node ret =
+ NodeManager::fromExprManager(d_to)->mkNode(n.getKind(), children);
- exportCache[n] = ret;
+ d_exportCache[n] = ret;
return ret;
}
}/* exportInternal() */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback