From e5044d89c715ac6c0d41a731b58a9c672d2d524e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 5 Sep 2013 20:59:18 -0400 Subject: [PATCH] Fix declare-datatypes dumping bug (bug 385). --- src/expr/expr_manager_template.cpp | 4 ++-- src/expr/expr_manager_template.h | 8 +++++++- src/expr/node_manager.h | 24 +++++++++++++----------- src/parser/cvc/Cvc.g | 6 +++--- src/parser/parser.cpp | 6 +++--- src/parser/parser.h | 3 ++- src/smt/smt_engine.cpp | 6 ++++-- src/smt/smt_engine.h | 2 +- 8 files changed, 35 insertions(+), 24 deletions(-) diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index a838d6d30..d87c498e6 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -718,9 +718,9 @@ TesterType ExprManager::mkTesterType(Type domain) const { return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode))); } -SortType ExprManager::mkSort(const std::string& name) const { +SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const { NodeManagerScope nms(d_nodeManager); - return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)))); + return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name, flags)))); } SortConstructorType ExprManager::mkSortConstructor(const std::string& name, diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 58c0bbae3..3f0ec2f9c 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -430,8 +430,14 @@ public: /** Make a type representing a tester with the given parameterization. */ TesterType mkTesterType(Type domain) const; + /** Bits for use in mkSort() flags. */ + enum { + SORT_FLAG_NONE = 0, + SORT_FLAG_PLACEHOLDER = 1 + };/* enum */ + /** Make a new sort with the given name. */ - SortType mkSort(const std::string& name) const; + SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const; /** Make a sort constructor from a name and arity. */ SortConstructorType mkSortConstructor(const std::string& name, diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 7c84f3f15..a65655501 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -75,9 +75,9 @@ typedef expr::Attribute DatatypeRecordA class NodeManagerListener { public: virtual ~NodeManagerListener() { } - virtual void nmNotifyNewSort(TypeNode tn) { } + virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { } virtual void nmNotifyNewSortConstructor(TypeNode tn) { } - virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort) { } + virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { } virtual void nmNotifyNewDatatypes(const std::vector& datatypes) { } virtual void nmNotifyNewVar(TNode n, uint32_t flags) { } virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { } @@ -778,14 +778,15 @@ public: inline TypeNode mkTesterType(TypeNode domain); /** Make a new (anonymous) sort of arity 0. */ - inline TypeNode mkSort(); + inline TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE); /** Make a new sort with the given name of arity 0. */ - inline TypeNode mkSort(const std::string& name); + inline TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE); /** Make a new sort by parameterizing the given sort constructor. */ inline TypeNode mkSort(TypeNode constructor, - const std::vector& children); + const std::vector& children, + uint32_t flags = ExprManager::SORT_FLAG_NONE); /** Make a new sort with the given name and arity. */ inline TypeNode mkSortConstructor(const std::string& name, size_t arity); @@ -1220,31 +1221,32 @@ inline bool NodeManager::hasOperator(Kind k) { } } -inline TypeNode NodeManager::mkSort() { +inline TypeNode NodeManager::mkSort(uint32_t flags) { NodeBuilder<1> nb(this, kind::SORT_TYPE); Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); nb << sortTag; TypeNode tn = nb.constructTypeNode(); for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSort(tn); + (*i)->nmNotifyNewSort(tn, flags); } return tn; } -inline TypeNode NodeManager::mkSort(const std::string& name) { +inline TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) { NodeBuilder<1> nb(this, kind::SORT_TYPE); Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); nb << sortTag; TypeNode tn = nb.constructTypeNode(); setAttribute(tn, expr::VarNameAttr(), name); for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSort(tn); + (*i)->nmNotifyNewSort(tn, flags); } return tn; } inline TypeNode NodeManager::mkSort(TypeNode constructor, - const std::vector& children) { + const std::vector& children, + uint32_t flags) { Assert(constructor.getKind() == kind::SORT_TYPE && constructor.getNumChildren() == 0, "expected a sort constructor"); @@ -1262,7 +1264,7 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor, TypeNode type = nb.constructTypeNode(); setAttribute(type, expr::VarNameAttr(), name); for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyInstantiateSortConstructor(constructor, type); + (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags); } return type; } diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index cbdee9c74..03d1e7a8a 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1951,15 +1951,15 @@ datatypeDef[std::vector& datatypes] * below. */ : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); } ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] { - t = PARSER_STATE->mkSort(id2); + t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER); params.push_back( t ); } ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] { - t = PARSER_STATE->mkSort(id2); + t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER); params.push_back( t ); } )* RBRACKET )? - { datatypes.push_back(Datatype(id,params)); + { datatypes.push_back(Datatype(id, params)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 42ca27caf..5d9b6c7ae 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -231,9 +231,9 @@ Parser::defineParameterizedType(const std::string& name, } SortType -Parser::mkSort(const std::string& name) { +Parser::mkSort(const std::string& name, uint32_t flags) { Debug("parser") << "newSort(" << name << ")" << std::endl; - Type type = d_exprManager->mkSort(name); + Type type = d_exprManager->mkSort(name, flags); defineType(name, type); return type; } @@ -248,7 +248,7 @@ Parser::mkSortConstructor(const std::string& name, size_t arity) { } SortType Parser::mkUnresolvedType(const std::string& name) { - SortType unresolved = mkSort(name); + SortType unresolved = mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER); d_unresolved.insert(unresolved); return unresolved; } diff --git a/src/parser/parser.h b/src/parser/parser.h index d07756cf4..b6ba482b7 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -411,7 +411,8 @@ public: /** * Creates a new sort with the given name. */ - SortType mkSort(const std::string& name); + SortType mkSort(const std::string& name, + uint32_t flags = ExprManager::SORT_FLAG_NONE); /** * Creates a new sort constructor with the given name and arity. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 810715885..987220cc7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -419,11 +419,13 @@ public: d_smt.d_nodeManager->unsubscribeEvents(this); } - void nmNotifyNewSort(TypeNode tn) { + void nmNotifyNewSort(TypeNode tn, uint32_t flags) { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn.toType()); - d_smt.addToModelCommandAndDump(c); + if((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) { + d_smt.addToModelCommandAndDump(c, flags); + } } void nmNotifyNewSortConstructor(TypeNode tn) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1da8d26da..3531f92e7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -336,7 +336,7 @@ class CVC4_PUBLIC SmtEngine { * Add to Model command. This is used for recording a command * that should be reported during a get-model call. */ - void addToModelCommandAndDump(const Command& c, uint32_t flags = ExprManager::VAR_FLAG_NONE, bool userVisible = true, const char* dumpTag = "declarations"); + void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations"); /** * Get the model (only if immediately preceded by a SAT -- 2.30.2