diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 18:18:07 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 18:18:07 -0400 |
commit | 004678b6386e66cfa6a079215a3644efca59cdf7 (patch) | |
tree | af7e8ba930b15ffc2ba901f35704c82abeb81e0e /src/expr | |
parent | c28d0a243dbfd4295f785a017890251bd2670ce8 (diff) |
nodemanager robust skolem numbering
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.cpp | 8 | ||||
-rw-r--r-- | src/expr/node_manager.h | 13 |
2 files changed, 16 insertions, 5 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index ecd3df084..4c61550b9 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -89,7 +89,8 @@ NodeManager::NodeManager(context::Context* ctxt, d_exprManager(exprManager), d_nodeUnderDeletion(NULL), d_inReclaimZombies(false), - d_abstractValueCount(0) { + d_abstractValueCount(0), + d_skolemCounter(0) { init(); } @@ -103,7 +104,8 @@ NodeManager::NodeManager(context::Context* ctxt, d_exprManager(exprManager), d_nodeUnderDeletion(NULL), d_inReclaimZombies(false), - d_abstractValueCount(0) { + d_abstractValueCount(0), + d_skolemCounter(0) { init(); } @@ -310,7 +312,7 @@ Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, cons setAttribute(n, TypeCheckedAttr(), true); if((flags & SKOLEM_EXACT_NAME) == 0) { stringstream name; - name << prefix << '_' << n.getId(); + name << prefix << '_' << ++d_skolemCounter; setAttribute(n, expr::VarNameAttr(), name.str()); } else { setAttribute(n, expr::VarNameAttr(), prefix); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f533d3ab9..f75ed9559 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -164,6 +164,15 @@ class NodeManager { unsigned d_abstractValueCount; /** + * A counter used to produce unique skolem names. + * + * Note that it is NOT incremented when skolems are created using + * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced + * by this node manager. + */ + unsigned d_skolemCounter; + + /** * 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 @@ -425,10 +434,10 @@ public: * Create a skolem constant with the given name, type, and comment. * * @param prefix the name of the new skolem variable is the prefix - * appended with the Node ID. This way a family of skolem variables + * appended with a unique 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. + * a unique ID appended and use prefix as the name. * * @param type the type of the skolem variable to create * |