diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 8 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 63 | ||||
-rw-r--r-- | src/expr/node_manager.h | 133 | ||||
-rw-r--r-- | src/expr/symbol_table.cpp | 20 |
6 files changed, 170 insertions, 60 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 53ca266f4..8b61e92d3 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -479,8 +479,6 @@ Type DeclareFunctionCommand::getType() const throw() { } void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this; - smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_FUN ); d_commandStatus = CommandSuccess::instance(); } @@ -511,8 +509,6 @@ Type DeclareTypeCommand::getType() const throw() { } void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this; - smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_SORT ); d_commandStatus = CommandSuccess::instance(); } @@ -552,7 +548,6 @@ Type DefineTypeCommand::getType() const throw() { } void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this; d_commandStatus = CommandSuccess::instance(); } @@ -602,7 +597,6 @@ Expr DefineFunctionCommand::getFormula() const throw() { } void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { - //Dump("declarations") << *this; -- done by SmtEngine try { if(!d_func.isNull()) { smtEngine->defineFunction(d_func, d_formals, d_formula); @@ -1275,8 +1269,6 @@ DatatypeDeclarationCommand::getDatatypes() const throw() { } void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { - Dump("declarations") << *this; - smtEngine->addToModelCommand( clone(), Model::COMMAND_DECLARE_DATATYPES ); d_commandStatus = CommandSuccess::instance(); } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 804d3af9a..03f3a04b0 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -646,6 +646,10 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, checkResolvedDatatype(*i); } + for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) { + (*i)->nmNotifyNewDatatypes(dtts); + } + return dtts; } diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 08c3a2b1e..c607ca0a7 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -140,7 +140,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC // skolems are only available at the Node level (not the Expr level) TypeNode typeNode = TypeNode::fromType(type); NodeManager* to_nm = NodeManager::fromExprManager(to); - Node n = to_nm->mkSkolem(name, typeNode);// FIXME thread safety + Node n = to_nm->mkSkolem(name, typeNode, "is a skolem variable imported from another ExprManager");// FIXME thread safety to_e = n.toExpr(); } else { Unhandled(); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index fc2eec774..82242cb1c 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -139,7 +139,7 @@ NodeManager::~NodeManager() { poolRemove( &expr::NodeValue::s_null ); if(Debug.isOn("gc:leaks")) { - Debug("gc:leaks") << "still in pool:" << std::endl; + Debug("gc:leaks") << "still in pool:" << endl; for(NodeValuePool::const_iterator i = d_nodeValuePool.begin(), iend = d_nodeValuePool.end(); i != iend; @@ -147,9 +147,9 @@ NodeManager::~NodeManager() { Debug("gc:leaks") << " " << *i << " id=" << (*i)->d_id << " rc=" << (*i)->d_rc - << " " << **i << std::endl; + << " " << **i << endl; } - Debug("gc:leaks") << ":end:" << std::endl; + Debug("gc:leaks") << ":end:" << endl; } delete d_statisticsRegistry; @@ -183,10 +183,10 @@ void NodeManager::reclaimZombies() { vector<NodeValue*> zombies; zombies.reserve(d_zombies.size()); - std::remove_copy_if(d_zombies.begin(), - d_zombies.end(), - std::back_inserter(zombies), - NodeValueReferenceCountNonZero()); + remove_copy_if(d_zombies.begin(), + d_zombies.end(), + back_inserter(zombies), + NodeValueReferenceCountNonZero()); d_zombies.clear(); for(vector<NodeValue*>::iterator i = zombies.begin(); @@ -200,7 +200,7 @@ void NodeManager::reclaimZombies() { Debug("gc") << "deleting node value " << nv << " [" << nv->d_id << "]: "; nv->printAst(Debug("gc")); - Debug("gc") << std::endl; + Debug("gc") << endl; } // remove from the pool @@ -251,7 +251,7 @@ TypeNode NodeManager::getType(TNode n, bool check) bool hasType = getAttribute(n, TypeAttr(), typeNode); bool needsCheck = check && !getAttribute(n, TypeCheckedAttr()); - Debug("getType") << "getting type for " << n << std::endl; + Debug("getType") << "getting type for " << n << endl; if(needsCheck && !(*d_options)[options::earlyTypeChecking]) { /* Iterate and compute the children bottom up. This avoids stack @@ -295,28 +295,57 @@ TypeNode NodeManager::getType(TNode n, bool check) /* The check should have happened, if we asked for it. */ Assert( !check || getAttribute(n, TypeCheckedAttr()) ); - Debug("getType") << "type of " << n << " is " << typeNode << std::endl; + Debug("getType") << "type of " << n << " is " << typeNode << endl; return typeNode; } +Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type, const std::string& comment, int flags) { + Node n = NodeBuilder<0>(this, kind::SKOLEM); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); + if((flags & SKOLEM_EXACT_NAME) == 0) { + size_t pos = name.find("$$"); + if(pos != string::npos) { + // replace a "$$" with the node ID + stringstream id; + id << n.getId(); + string newName = name; + newName.replace(pos, 2, id.str()); + setAttribute(n, expr::VarNameAttr(), newName); + } else { + stringstream newName; + newName << name << '_' << n.getId(); + setAttribute(n, expr::VarNameAttr(), newName.str()); + } + } else { + setAttribute(n, expr::VarNameAttr(), name); + } + if((flags & SKOLEM_NO_NOTIFY) == 0) { + for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewSkolem(n, comment); + } + } + return n; +} + TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor, TypeNode range) { - std::vector<TypeNode> sorts; - Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl; + vector<TypeNode> sorts; + Debug("datatypes") << "ctor name: " << constructor.getName() << endl; for(DatatypeConstructor::const_iterator i = constructor.begin(); i != constructor.end(); ++i) { TypeNode selectorType = *(*i).getSelector().getType().d_typeNode; - Debug("datatypes") << selectorType << std::endl; + Debug("datatypes") << selectorType << endl; TypeNode sort = selectorType[1]; // should be guaranteed here already, but just in case Assert(!sort.isFunctionLike()); - Debug("datatypes") << "ctor sort: " << sort << std::endl; + Debug("datatypes") << "ctor sort: " << sort << endl; sorts.push_back(sort); } - Debug("datatypes") << "ctor range: " << range << std::endl; + Debug("datatypes") << "ctor range: " << range << endl; CheckArgument(!range.isFunctionLike(), range, "cannot create higher-order function types"); sorts.push_back(range); @@ -335,7 +364,7 @@ TypeNode NodeManager::mkPredicateSubtype(Expr lambda) TypeNode tn = lambdan.getType(); if(! tn.isPredicateLike() || tn.getArgTypes().size() != 1) { - std::stringstream ss; + stringstream ss; ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; throw TypeCheckingExceptionPrivate(lambdan, ss.str()); } @@ -355,7 +384,7 @@ TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness) TypeNode tn = lambdan.getType(); if(! tn.isPredicateLike() || tn.getArgTypes().size() != 1) { - std::stringstream ss; + stringstream ss; ss << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; throw TypeCheckingExceptionPrivate(lambdan, ss.str()); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 27d77a646..893fde64b 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -63,6 +63,21 @@ typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; }/* CVC4::expr namespace */ +/** + * An interface that an interested party can implement and then subscribe + * to NodeManager events via NodeManager::subscribeEvents(this). + */ +class NodeManagerListener { +public: + virtual ~NodeManagerListener() { } + virtual void nmNotifyNewSort(TypeNode tn) { } + 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) { } + virtual void nmNotifyNewSkolem(TNode n, const std::string& comment) { } +};/* class NodeManagerListener */ + class NodeManager { template <unsigned nchild_thresh> friend class CVC4::NodeBuilder; friend class NodeManagerScope; @@ -70,8 +85,11 @@ class NodeManager { friend class expr::TypeChecker; // friends so they can access mkVar() here, which is private - friend Expr ExprManager::mkVar(const std::string& name, Type type); - friend Expr ExprManager::mkVar(Type type); + friend Expr ExprManager::mkVar(const std::string&, Type); + friend Expr ExprManager::mkVar(Type); + + // 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>&); /** Predicate for use with STL algorithms */ struct NodeValueReferenceCountNonZero { @@ -138,6 +156,11 @@ class NodeManager { Node d_operators[kind::LAST_KIND]; /** + * A list of subscribers for NodeManager events. + */ + std::vector<NodeManagerListener*> d_listeners; + + /** * Look up a NodeValue in the pool associated to this NodeManager. * The NodeValue argument need not be a "completely-constructed" * NodeValue. In particular, "non-inlined" constants are permitted @@ -299,6 +322,19 @@ public: return d_statisticsRegistry; } + /** Subscribe to NodeManager events */ + void subscribeEvents(NodeManagerListener* listener) { + Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed"); + d_listeners.push_back(listener); + } + + /** Unsubscribe from NodeManager events */ + void unsubscribeEvents(NodeManagerListener* listener) { + std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener); + Assert(elt != d_listeners.end(), "listener not subscribed"); + d_listeners.erase(elt); + } + // general expression-builders /** Create a node with one child. */ @@ -371,9 +407,39 @@ public: Node mkBoundVar(const TypeNode& type); Node* mkBoundVarPtr(const TypeNode& type); - /** Create a skolem constant with the given type. */ - Node mkSkolem(const TypeNode& type); - Node mkSkolem(const std::string& name, const TypeNode& type); + /** + * Optional flags used to control behavior of NodeManager::mkSkolem(). + * They should be composed with a bitwise OR (e.g., + * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME"). Of course, SKOLEM_DEFAULT + * cannot be composed in such a manner. + */ + enum SkolemFlags { + SKOLEM_DEFAULT = 0, /**< default behavior */ + SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */ + SKOLEM_EXACT_NAME = 2 /**< do not make the name unique by adding the id */ + };/* enum SkolemFlags */ + + /** + * Create a skolem constant with the given name, type, and comment. + * + * @param name the name of the new skolem variable. This name can + * contain the special character sequence "$$", in which case the + * $$ is replaced with the Node ID. That way a family of skolem + * variables can be made with unique identifiers, used in dump, + * tracing, and debugging output. By convention, you should probably + * call mkSkolem() with a custom name appended with "_$$". + * + * @param type the type of the skolem variable to create + * + * @param comment a comment for dumping output; if declarations are + * being dumped, this is included in a comment before the declaration + * and can be quite useful for debugging + * + * @param flags an optional mask of bits from SkolemFlags to control + * mkSkolem() behavior + */ + Node mkSkolem(const std::string& name, const TypeNode& type, + const std::string& comment = "", int flags = SKOLEM_DEFAULT); /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); @@ -1118,13 +1184,23 @@ inline TypeNode NodeManager::mkSort() { NodeBuilder<1> nb(this, kind::SORT_TYPE); Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); nb << sortTag; - return nb.constructTypeNode(); + TypeNode tn = nb.constructTypeNode(); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewSort(tn); + } + return tn; } inline TypeNode NodeManager::mkSort(const std::string& name) { - TypeNode type = mkSort(); - setAttribute(type, expr::VarNameAttr(), name); - return type; + 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<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewSort(tn); + } + return tn; } inline TypeNode NodeManager::mkSort(TypeNode constructor, @@ -1145,6 +1221,9 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor, nb.append(children); TypeNode type = nb.constructTypeNode(); setAttribute(type, expr::VarNameAttr(), name); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyInstantiateSortConstructor(constructor, type); + } return type; } @@ -1157,6 +1236,9 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name, TypeNode type = nb.constructTypeNode(); setAttribute(type, expr::VarNameAttr(), name); setAttribute(type, expr::SortArityAttr(), arity); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewSortConstructor(type); + } return type; } @@ -1368,15 +1450,25 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind, inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { - Node n = mkVar(type); + Node n = NodeBuilder<0>(this, kind::VARIABLE); + setAttribute(n, TypeAttr(), type); + setAttribute(n, TypeCheckedAttr(), true); setAttribute(n, expr::VarNameAttr(), name); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewVar(n); + } return n; } inline Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) { - Node* n = mkVarPtr(type); + Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); + setAttribute(*n, TypeAttr(), type); + setAttribute(*n, TypeCheckedAttr(), true); setAttribute(*n, expr::VarNameAttr(), name); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewVar(*n); + } return n; } @@ -1397,6 +1489,9 @@ inline Node NodeManager::mkVar(const TypeNode& type) { Node n = NodeBuilder<0>(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewVar(n); + } return n; } @@ -1404,6 +1499,9 @@ inline Node* NodeManager::mkVarPtr(const TypeNode& type) { Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr(); setAttribute(*n, TypeAttr(), type); setAttribute(*n, TypeCheckedAttr(), true); + for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { + (*i)->nmNotifyNewVar(*n); + } return n; } @@ -1421,19 +1519,6 @@ inline Node* NodeManager::mkBoundVarPtr(const TypeNode& type) { return n; } -inline Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type) { - Node n = mkSkolem(type); - setAttribute(n, expr::VarNameAttr(), name); - return n; -} - -inline Node NodeManager::mkSkolem(const TypeNode& type) { - Node n = NodeBuilder<0>(this, kind::SKOLEM); - setAttribute(n, TypeAttr(), type); - setAttribute(n, TypeCheckedAttr(), true); - return n; -} - inline Node NodeManager::mkInstConstant(const TypeNode& type) { Node n = NodeBuilder<0>(this, kind::INST_CONSTANT); n.setAttribute(TypeAttr(), type); diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index c9234b5e0..e3bd898ef 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -50,7 +50,7 @@ SymbolTable::~SymbolTable() { } void SymbolTable::bind(const std::string& name, Expr obj, - bool levelZero) throw(AssertionException) { + bool levelZero) throw(AssertionException) { CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj); @@ -58,7 +58,7 @@ void SymbolTable::bind(const std::string& name, Expr obj, } void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj, - bool levelZero) throw(AssertionException) { + bool levelZero) throw(AssertionException) { CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); if(levelZero){ @@ -89,18 +89,18 @@ Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException } void SymbolTable::bindType(const std::string& name, Type t, - bool levelZero) throw() { - if(levelZero){ + bool levelZero) throw() { + if(levelZero) { d_typeMap->insertAtContextLevelZero(name, make_pair(vector<Type>(), t)); - }else{ + } else { d_typeMap->insert(name, make_pair(vector<Type>(), t)); } } void SymbolTable::bindType(const std::string& name, - const std::vector<Type>& params, - Type t, - bool levelZero) throw() { + const std::vector<Type>& params, + Type t, + bool levelZero) throw() { if(Debug.isOn("sort")) { Debug("sort") << "bindType(" << name << ", ["; if(params.size() > 0) { @@ -110,7 +110,7 @@ void SymbolTable::bindType(const std::string& name, } Debug("sort") << "], " << t << ")" << endl; } - if(levelZero){ + if(levelZero) { d_typeMap->insertAtContextLevelZero(name, make_pair(params, t)); } else { d_typeMap->insert(name, make_pair(params, t)); @@ -131,7 +131,7 @@ Type SymbolTable::lookupType(const std::string& name) const throw(AssertionExcep } Type SymbolTable::lookupType(const std::string& name, - const std::vector<Type>& params) const throw(AssertionException) { + const std::vector<Type>& params) const throw(AssertionException) { pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second; Assert(p.first.size() == params.size(), "type constructor arity is wrong: " |