diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-23 16:01:13 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-05 15:17:37 -0400 |
commit | b3a4670710d3ffdc99879a1d27f37cf775af18eb (patch) | |
tree | afb6554dcf95cdd324384478a51e01c5d63c106b /src/expr/node_manager.h | |
parent | c2972fc63ca6d49ffeaf0e8a9a39cad733790cd7 (diff) |
Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a segfault in smt2 printer
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 913b8befb..f44c7e78b 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -79,8 +79,8 @@ public: virtual void nmNotifyNewSortConstructor(TypeNode tn) { } virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort) { } virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { } - virtual void nmNotifyNewVar(TNode n, bool isGlobal) { } - virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, bool isGlobal) { } + virtual void nmNotifyNewVar(TNode n, uint32_t flags) { } + virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { } };/* class NodeManagerListener */ class NodeManager { @@ -90,8 +90,8 @@ class NodeManager { friend class expr::TypeChecker; // friends so they can access mkVar() here, which is private - friend Expr ExprManager::mkVar(const std::string&, Type, bool isGlobal); - friend Expr ExprManager::mkVar(Type, bool isGlobal); + friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags); + friend Expr ExprManager::mkVar(Type, uint32_t flags); // friend so it can access NodeManager's d_listeners and notify clients friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&); @@ -309,12 +309,12 @@ class NodeManager { * version of this is private to avoid internal uses of mkVar() from * within CVC4. Such uses should employ mkSkolem() instead. */ - Node mkVar(const std::string& name, const TypeNode& type, bool isGlobal = false); - Node* mkVarPtr(const std::string& name, const TypeNode& type, bool isGlobal = false); + Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); + Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); /** Create a variable with the given type. */ - Node mkVar(const TypeNode& type, bool isGlobal = false); - Node* mkVarPtr(const TypeNode& type, bool isGlobal = false); + Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); + Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE); public: @@ -1532,27 +1532,27 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, } -inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, bool isGlobal) { +inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type, uint32_t flags) { Node n = NodeBuilder<0>(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); setAttribute(n, expr::VarNameAttr(), name); - setAttribute(n, expr::GlobalVarAttr(), isGlobal); + setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(n, isGlobal); + (*i)->nmNotifyNewVar(n, flags); } return n; } inline Node* NodeManager::mkVarPtr(const std::string& name, - const TypeNode& type, bool isGlobal) { + const TypeNode& type, uint32_t flags) { Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); setAttribute(*n, expr::VarNameAttr(), name); - setAttribute(*n, expr::GlobalVarAttr(), isGlobal); + setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(*n, isGlobal); + (*i)->nmNotifyNewVar(*n, flags); } return n; } @@ -1570,24 +1570,24 @@ inline Node* NodeManager::mkBoundVarPtr(const std::string& name, return n; } -inline Node NodeManager::mkVar(const TypeNode& type, bool isGlobal) { +inline Node NodeManager::mkVar(const TypeNode& type, uint32_t flags) { Node n = NodeBuilder<0>(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); - setAttribute(n, expr::GlobalVarAttr(), isGlobal); + setAttribute(n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(n, isGlobal); + (*i)->nmNotifyNewVar(n, flags); } return n; } -inline Node* NodeManager::mkVarPtr(const TypeNode& type, bool isGlobal) { +inline Node* NodeManager::mkVarPtr(const TypeNode& type, uint32_t flags) { Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); - setAttribute(*n, expr::GlobalVarAttr(), isGlobal); + setAttribute(*n, expr::GlobalVarAttr(), flags & ExprManager::VAR_FLAG_GLOBAL); for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(*n, isGlobal); + (*i)->nmNotifyNewVar(*n, flags); } return n; } |