diff options
Diffstat (limited to 'src/expr/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 20 |
1 files changed, 5 insertions, 15 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 22c47da59..ecd3df084 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -304,26 +304,16 @@ TypeNode NodeManager::getType(TNode n, bool check) 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) { |