diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-29 06:59:21 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-11-29 06:59:21 +0000 |
commit | 8f6b53a5328e34ed3f22c67aad6a5ab73bb6fa8b (patch) | |
tree | 277d4cefb81445d0f3975382f053d224437c6118 /src/expr/expr_template.cpp | |
parent | ff6ac38127fbb03e6c11a210b6b16d647b8785ea (diff) |
Hack to support global variables for CVC language extended to export mechanism.
- Adds GlobalVarAttr node attribute
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r-- | src/expr/expr_template.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index ed643b830..a3204f00f 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -138,12 +138,15 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) { // temporarily set the node manager to NULL; this gets around // a check that mkVar isn't called internally - NodeManagerScope nullScope(NULL); if(n.getKind() == kind::BOUND_VAR_LIST || n.getKind() == kind::BOUND_VARIABLE) { + NodeManagerScope nullScope(NULL); to_e = to->mkBoundVar(name, type);// FIXME thread safety } else if(n.getKind() == kind::VARIABLE) { - to_e = to->mkVar(name, type);// FIXME thread safety + bool isGlobal; + Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal); + NodeManagerScope nullScope(NULL); + to_e = to->mkVar(name, type, isGlobal);// 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); |