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 | |
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')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 8 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 30 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_manager.h | 40 |
4 files changed, 46 insertions, 34 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 3a2feb624..424ebab11 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -805,20 +805,20 @@ Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) { return t; } -Expr ExprManager::mkVar(const std::string& name, Type type, bool isGlobal) { +Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) { Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem()."); NodeManagerScope nms(d_nodeManager); - Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, isGlobal); + Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags); Debug("nm") << "set " << name << " on " << *n << std::endl; INC_STAT_VAR(type, false); return Expr(this, n); } -Expr ExprManager::mkVar(Type type, bool isGlobal) { +Expr ExprManager::mkVar(Type type, uint32_t flags) { Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code. Please use mkSkolem()."); NodeManagerScope nms(d_nodeManager); INC_STAT_VAR(type, false); - return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, isGlobal)); + return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags)); } Expr ExprManager::mkBoundVar(const std::string& name, Type type) { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 15278dfb6..58c0bbae3 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -468,6 +468,13 @@ public: Type getType(Expr e, bool check = false) throw(TypeCheckingException); + /** Bits for use in mkVar() flags. */ + enum { + VAR_FLAG_NONE = 0, + VAR_FLAG_GLOBAL = 1, + VAR_FLAG_DEFINED = 2 + };/* enum */ + /** * Create a new, fresh variable. This variable is guaranteed to be * distinct from every variable thus far in the ExprManager, even @@ -477,28 +484,33 @@ public: * * @param name a name to associate to the fresh new variable * @param type the type for the new variable - * @param isGlobal whether this variable is to be considered "global" - * or not. Note that this information isn't used by the ExprManager, - * but is passed on to the ExprManager's event subscribers like the - * model-building service; if isGlobal is true, this newly-created - * variable will still available in models generated after an - * intervening pop. + * @param flags - VAR_FLAG_NONE - no flags; + * VAR_FLAG_GLOBAL - whether this variable is to be + * considered "global" or not. Note that this information isn't + * used by the ExprManager, but is passed on to the ExprManager's + * event subscribers like the model-building service; if isGlobal + * is true, this newly-created variable will still available in + * models generated after an intervening pop. + * VAR_FLAG_DEFINED - if this is to be a "defined" symbol, e.g., for + * use with SmtEngine::defineFunction(). This keeps a declaration + * from being emitted in API dumps (since a subsequent definition is + * expected to be dumped instead). */ - Expr mkVar(const std::string& name, Type type, bool isGlobal = false); + Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE); /** * Create a (nameless) new, fresh variable. This variable is guaranteed * to be distinct from every variable thus far in the ExprManager. * * @param type the type for the new variable - * @param isGlobal whether this variable is to be considered "global" + * @param flags - VAR_FLAG_GLOBAL - whether this variable is to be considered "global" * or not. Note that this information isn't used by the ExprManager, * but is passed on to the ExprManager's event subscribers like the * model-building service; if isGlobal is true, this newly-created * variable will still available in models generated after an * intervening pop. */ - Expr mkVar(Type type, bool isGlobal = false); + Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE); /** * Create a new, fresh variable for use in a binder expression diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 7e809ed62..1b1bc7535 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -146,7 +146,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC bool isGlobal; Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal); NodeManagerScope nullScope(NULL); - to_e = to->mkVar(name, type, isGlobal);// FIXME thread safety + to_e = to->mkVar(name, type, isGlobal ? ExprManager::VAR_FLAG_GLOBAL : ExprManager::VAR_FLAG_NONE);// 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); 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; } |