diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 14:11:14 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 14:11:14 -0400 |
commit | c28d0a243dbfd4295f785a017890251bd2670ce8 (patch) | |
tree | 58b7c8ef04cc14563129017d9c2c8717f400825d /src/expr | |
parent | 6f6703473ccc66b3d2bdefed688602f93d33cd8f (diff) | |
parent | ca423e291b1f7d67e1a325bb6d98663d6c0690c7 (diff) |
Merge pull request #25 from kbansal/sets
Sets
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.cpp | 20 | ||||
-rw-r--r-- | src/expr/node_manager.h | 13 |
2 files changed, 11 insertions, 22 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) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 15c49efd8..f533d3ab9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -424,12 +424,11 @@ public: /** * 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 prefix the name of the new skolem variable is the prefix + * appended with the Node ID. This way a family of skolem variables + * can be made with unique identifiers, used in dump, tracing, and + * debugging output. Use SKOLEM_EXECT_NAME flag if you don't want + * Node ID appended and use prefix as the name. * * @param type the type of the skolem variable to create * @@ -440,7 +439,7 @@ public: * @param flags an optional mask of bits from SkolemFlags to control * mkSkolem() behavior */ - Node mkSkolem(const std::string& name, const TypeNode& type, + Node mkSkolem(const std::string& prefix, const TypeNode& type, const std::string& comment = "", int flags = SKOLEM_DEFAULT); /** Create a instantiation constant with the given type. */ |