diff options
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r-- | src/expr/expr_template.cpp | 82 |
1 files changed, 81 insertions, 1 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 3c376f632..c510ce381 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -19,8 +19,10 @@ #include "expr/expr.h" #include "expr/node.h" #include "expr/expr_manager_scope.h" +#include "expr/variable_type_map.h" #include "util/Assert.h" +#include <vector> #include <iterator> #include <utility> @@ -30,7 +32,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 34 "${template}" +#line 36 "${template}" using namespace CVC4::kind; using namespace std; @@ -105,6 +107,72 @@ ExprManager* Expr::getExprManager() const { return d_exprManager; } +namespace expr { + +static Node exportConstant(TNode n, NodeManager* to); + +Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) { + if(n.getMetaKind() == kind::metakind::CONSTANT) { + return exportConstant(n, NodeManager::fromExprManager(to)); + } else if(n.getMetaKind() == kind::metakind::VARIABLE) { + Expr from_e(from, new Node(n)); + Expr& to_e = vmap.d_typeMap[from_e]; + if(! to_e.isNull()) { +Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl; + return to_e.getNode(); + } else { + // 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); + if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) { + to_e = to->mkVar(name, type);// FIXME thread safety +Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl; + } else { + to_e = 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 + return Node::fromExpr(to_e); + } + } else { + std::vector<Node> children; +Debug("export") << "n: " << n << std::endl; + if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { +Debug("export") << "+ parameterized, op is " << n.getOperator() << std::endl; + children.reserve(n.getNumChildren() + 1); + children.push_back(exportInternal(n.getOperator(), from, to, vmap)); + } else { + children.reserve(n.getNumChildren()); + } + for(TNode::iterator i = n.begin(), i_end = n.end(); i != i_end; ++i) { +Debug("export") << "+ child: " << *i << std::endl; + children.push_back(exportInternal(*i, from, to, vmap)); + } + if(Debug.isOn("export")) { + ExprManagerScope ems(*to); + Debug("export") << "children for export from " << n << std::endl; + for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) { + Debug("export") << " child: " << *i << std::endl; + } + } + return NodeManager::fromExprManager(to)->mkNode(n.getKind(), children);// FIXME thread safety + } +}/* exportInternal() */ + +}/* CVC4::expr namespace */ + +Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + Assert(d_exprManager != exprManager, + "No sense in cloning an Expr in the same ExprManager"); + ExprManagerScope ems(*this); + return Expr(exprManager, new Node(expr::exportInternal(*d_node, d_exprManager, exprManager, variableMap))); +} + Expr& Expr::operator=(const Expr& e) { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); @@ -449,4 +517,16 @@ void Expr::debugPrint() { ${getConst_implementations} +namespace expr { + +static Node exportConstant(TNode n, NodeManager* to) { + Assert(n.getMetaKind() == kind::metakind::CONSTANT); + switch(n.getKind()) { +${exportConstant_cases} + + default: Unhandled(n.getKind()); + } +}/* exportConstant() */ + +}/* CVC4::expr namespace */ }/* CVC4 namespace */ |