* Attribute infrastructure -- static design. Documentation is coming.

  See test/unit/expr/node_white.h for use examples, including how to
  define new attribute kinds.

Also:

* fixes to test infrastructure
* minor changes to code formatting throughout
* attribute tests in test/unit/expr/node_white.h
* fixes to NodeManagerScope ordering
* use NodeValue::getKind() to properly deal with UNDEFINED_KIND
  (removing compiler warning)
* ExprManager: add proper NodeManagerScope to public-facing member
  functions
* store variable names and types in attributes
* SoftNode is a placeholder, not a real implementation

1 files changed, 25 insertions, 25 deletions

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index fd2cf3332..0693b48db 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -39,7 +39,7 @@ public:
     d_scope = new NodeManagerScope(d_nm);
   }
 
-  void tearDown(){
+  void tearDown() {
     delete d_nm;
     delete d_scope;
   }
@@ -55,7 +55,7 @@ public:
     Node::null();
   }
 
-  void testIsNull(){
+  void testIsNull() {
     /* bool isNull() const; */
 
     Node a = Node::null();
@@ -73,7 +73,7 @@ public:
     Node e(Node::null());
   }
 
-  void testDestructor(){
+  void testDestructor() {
     /* No access to internals ?
      * Makes sense to only test that this is crash free.
      */
@@ -84,7 +84,7 @@ public:
   }
 
   /*tests:  bool operator==(const Node& e) const  */
-  void testOperatorEquals(){
+  void testOperatorEquals() {
     Node a, b, c;
     
     b = d_nm->mkVar();
@@ -122,7 +122,7 @@ public:
   }
 
   /* operator!= */
-  void testOperatorNotEquals(){
+  void testOperatorNotEquals() {
 
 
     Node a, b, c;
@@ -157,7 +157,7 @@ public:
 
   }
 
-  void testOperatorSquare(){  
+  void testOperatorSquare() {  
     /*Node operator[](int i) const */
 
     //Basic bounds check on a node w/out children
@@ -183,7 +183,7 @@ public:
   }
 
   /*tests:   Node& operator=(const Node&); */
-  void testOperatorAssign(){
+  void testOperatorAssign() {
     Node a, b;
     Node c = d_nm->mkNode(NOT);
     
@@ -197,7 +197,7 @@ public:
     TS_ASSERT(a==c);
   }
   
-  void testOperatorLessThan(){
+  void testOperatorLessThan() {
     /* We don't have access to the ids so we can't test the implementation
      * in the black box tests. 
      */
@@ -232,13 +232,13 @@ public:
     std::vector<Node> chain;
     int N = 500;
     Node curr = d_nm->mkNode(NULL_EXPR);
-    for(int i=0;i<N;i++){
+    for(int i=0;i<N;i++) {
       chain.push_back(curr);
       curr = d_nm->mkNode(AND,curr);
     }
     
-    for(int i=0;i<N;i++){
-      for(int j=i+1;j<N;j++){
+    for(int i=0;i<N;i++) {
+      for(int j=i+1;j<N;j++) {
 	Node chain_i = chain[i];
 	Node chain_j = chain[j];
 	TS_ASSERT(chain_i<chain_j);
@@ -247,7 +247,7 @@ public:
     
   }
 
-  void testHash(){
+  void testHash() {
     /* Not sure how to test this except survial... */
     Node a = d_nm->mkNode(ITE);
     Node b = d_nm->mkNode(ITE);
@@ -257,7 +257,7 @@ public:
 
   
 
-  void testEqExpr(){
+  void testEqExpr() {
     /*Node eqExpr(const Node& right) const;*/
 
     Node left = d_nm->mkNode(TRUE);
@@ -272,7 +272,7 @@ public:
     TS_ASSERT(eq[1] == right);
   }
 
-  void testNotExpr(){
+  void testNotExpr() {
     /*  Node notExpr() const;*/
 
     Node child = d_nm->mkNode(TRUE);
@@ -284,7 +284,7 @@ public:
     TS_ASSERT(parent[0] == child);
     
   }
-  void testAndExpr(){
+  void testAndExpr() {
     /*Node andExpr(const Node& right) const;*/
     
     Node left = d_nm->mkNode(TRUE);
@@ -300,7 +300,7 @@ public:
     
   }
 
-  void testOrExpr(){
+  void testOrExpr() {
     /*Node orExpr(const Node& right) const;*/
      
     Node left = d_nm->mkNode(TRUE);
@@ -316,7 +316,7 @@ public:
 
   }
 
-  void testIteExpr(){
+  void testIteExpr() {
     /*Node iteExpr(const Node& thenpart, const Node& elsepart) const;*/
 
     Node cnd = d_nm->mkNode(PLUS);
@@ -333,7 +333,7 @@ public:
     TS_ASSERT(*(++(++ite.begin())) == elseBranch);
   }
 
-  void testIffExpr(){
+  void testIffExpr() {
     /*  Node iffExpr(const Node& right) const; */
      
     Node left = d_nm->mkNode(TRUE);
@@ -349,7 +349,7 @@ public:
   }
 
   
-  void testImpExpr(){
+  void testImpExpr() {
     /* Node impExpr(const Node& right) const; */
     Node left = d_nm->mkNode(TRUE);
     Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
@@ -363,7 +363,7 @@ public:
     TS_ASSERT(*(++eq.begin()) == right);
   }
 
-  void testXorExpr(){
+  void testXorExpr() {
     /*Node xorExpr(const Node& right) const;*/
     Node left = d_nm->mkNode(TRUE);
     Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
@@ -377,26 +377,26 @@ public:
     TS_ASSERT(*(++eq.begin()) == right);
   }
 
-  void testPlusExpr(){
+  void testPlusExpr() {
     /*Node plusExpr(const Node& right) const;*/
     TS_WARN( "TODO: No implementation to test." );
   }
 
-  void testUMinusExpr(){
+  void testUMinusExpr() {
     /*Node uMinusExpr() const;*/
     TS_WARN( "TODO: No implementation to test." );
   }
-  void testMultExpr(){
+  void testMultExpr() {
     /*  Node multExpr(const Node& right) const;*/
     TS_WARN( "TODO: No implementation to test." );    
   }
 
-  void testKindSingleton(Kind k){
+  void testKindSingleton(Kind k) {
     Node n = d_nm->mkNode(k);
     TS_ASSERT(k == n.getKind());
   }
 
-  void testGetKind(){
+  void testGetKind() {
     /*inline Kind getKind() const; */
 
     testKindSingleton(NOT);