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/node_manager.h | |
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/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5cf591f9d..2cda23f2d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -52,12 +52,14 @@ class TypeChecker; // TODO: hide this attribute behind a NodeManager interface. namespace attr { struct VarNameTag { }; + struct GlobalVarTag { }; struct SortArityTag { }; struct DatatypeTupleTag { }; struct DatatypeRecordTag { }; }/* CVC4::expr::attr namespace */ typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; +typedef Attribute<attr::GlobalVarTag(), bool> GlobalVarAttr; typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; /** Attribute true for datatype types that are replacements for tuple types */ typedef expr::Attribute<expr::attr::DatatypeTupleTag, TypeNode> DatatypeTupleAttr; @@ -1479,6 +1481,7 @@ inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, bo setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); setAttribute(n, expr::VarNameAttr(), name); + setAttribute(n, expr::GlobalVarAttr(), isGlobal); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { (*i)->nmNotifyNewVar(n, isGlobal); } @@ -1491,6 +1494,7 @@ inline Node* NodeManager::mkVarPtr(const std::string& name, setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); setAttribute(*n, expr::VarNameAttr(), name); + setAttribute(*n, expr::GlobalVarAttr(), isGlobal); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { (*i)->nmNotifyNewVar(*n, isGlobal); } @@ -1514,6 +1518,7 @@ inline Node NodeManager::mkVar(const TypeNode& type, bool isGlobal) { Node n = NodeBuilder<0>(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); + setAttribute(n, expr::GlobalVarAttr(), isGlobal); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { (*i)->nmNotifyNewVar(n, isGlobal); } @@ -1524,6 +1529,7 @@ inline Node* NodeManager::mkVarPtr(const TypeNode& type, bool isGlobal) { Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); + setAttribute(*n, expr::GlobalVarAttr(), isGlobal); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { (*i)->nmNotifyNewVar(*n, isGlobal); } |