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 /test/unit/expr/attribute_black.h | |
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 'test/unit/expr/attribute_black.h')
-rw-r--r-- | test/unit/expr/attribute_black.h | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index 93fbe049a..02de21635 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -74,7 +74,7 @@ public: void testDeallocation() { TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); MyData* data; MyData* data1; MyDataAttribute attr; @@ -92,7 +92,7 @@ public: typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute; void testInts(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); const uint64_t val = 63489; uint64_t data0 = 0; uint64_t data1 = 0; @@ -120,9 +120,9 @@ public: typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute; void testTNodes(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); - Node val(d_nodeManager->mkSkolem(booleanType)); + Node val(d_nodeManager->mkSkolem("b", booleanType)); TNode data0; TNode data1; @@ -155,7 +155,7 @@ public: typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute; void testPtrs(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); Foo* val = new Foo(63489); Foo* data0 = NULL; @@ -186,7 +186,7 @@ public: typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute; void testConstPtrs(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); const Foo* val = new Foo(63489); const Foo* data0 = NULL; @@ -216,7 +216,7 @@ public: typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute; void testStrings(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); std::string val("63489"); std::string data0; @@ -245,7 +245,7 @@ public: typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute; void testBools(){ TypeNode booleanType = d_nodeManager->booleanType(); - Node* node = new Node(d_nodeManager->mkSkolem(booleanType)); + Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType)); bool val = true; bool data0 = false; |