diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-19 21:21:00 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-19 21:21:00 +0000 |
commit | 46c12d84290f3ed23bd0b435c6e8e5852ab1af39 (patch) | |
tree | 64c2d2175eb814b9187d8cc6ccecbddf90151b2a /src/expr/node_manager.cpp | |
parent | 7a15b2c1fb45f0cc7480466473f344f8b1f5ed94 (diff) |
General subscriber infrastructure for NodeManager, as discussed in the
meeting last week. The SmtEngine now subscribes to NodeManager events,
does appropriate dumping of variable declarations, and notifies the Model
class.
The way to create a skolem is now:
nodeManager->mkSkolem("myvar_$$", TypeNode, "is a variable created by the theory of Foo")
The first argument is the name of the skolem, and the (optional) "$$" is a
placeholder for the node id (to get a unique name). Without a "$$", a "_$$"
is automatically appended to the given name.
The second argument is the type.
The (optional, but recommended) third argument is a comment, used by the
dump infrastructure to indicate what the variable is for / who owns it.
An optional fourth argument (not shown) allows you to specify flags that
control the behavior (e.g., don't do notification, and/or don't make a
unique name). Look at the documentation for details on these.
In particular, the above means you can't just do a mkSkolem(boolType) for
example---you have to specify a name and (hopefully also,
but it's optional) a comment. This leads to easier debugging than the
anonymous skolems before, since we'll be able to track where the skolems
came from.
Much of the Model and Dump stuff, as well as some Command stuff, is cleaned up
by this commit. Some remains to be cleaned up.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 63 |
1 files changed, 46 insertions, 17 deletions
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()); } |