return typeNode;
}
-Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type, const std::string& comment, int flags) {
+Node NodeManager::mkSkolem(const std::string& prefix, 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());
- }
+ stringstream name;
+ name << prefix << '_' << n.getId();
+ setAttribute(n, expr::VarNameAttr(), name.str());
} else {
- setAttribute(n, expr::VarNameAttr(), name);
+ setAttribute(n, expr::VarNameAttr(), prefix);
}
if((flags & SKOLEM_NO_NOTIFY) == 0) {
for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {