* Addressed issues brought up in Chris's review of Morgan's

  NodeManager (bug #65).  Better documentation, etc.

* As part of this, removed NodeManager::mkVar() (which created a
  variable of unknown type).  This requires changes to lots of unit
  tests, which were using this function.

* Performed some review of parser code (my code review #73).

  + I changed the way exceptions were caught and rethrown in
    src/parser/input.cpp.

  + ParserExceptions weren't being properly constructed (d_line and
    d_column weren't intiialized and could contain junk, leading to
    weird error messages).  Fixed.

* Fix to the current working directory used by run_regression script.
  Makes exceptional output easier to match against (in expected error
  output).

* (configure.ac) Ensure that CFLAGS has -fexceptions in it, in case we
  compile any C code and don't use the C++ compiler.

1 files changed, 15 insertions, 12 deletions

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index d420c6e26..9e199aa9a 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -36,6 +36,7 @@ private:
   Context* d_ctxt;
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
+  Type* d_booleanType;
 
 public:
 
@@ -43,6 +44,8 @@ public:
     d_ctxt = new Context;
     d_nodeManager = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nodeManager);
+
+    d_booleanType = d_nodeManager->booleanType();
   }
 
   void tearDown() {
@@ -94,12 +97,12 @@ public:
   void testOperatorEquals() {
     Node a, b, c;
 
-    b = d_nodeManager->mkVar();
+    b = d_nodeManager->mkVar(d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkVar();
+    Node d = d_nodeManager->mkVar(d_booleanType);
 
     TS_ASSERT(a==a);
     TS_ASSERT(a==b);
@@ -134,12 +137,12 @@ public:
 
     Node a, b, c;
 
-    b = d_nodeManager->mkVar();
+    b = d_nodeManager->mkVar(d_booleanType);
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkVar();
+    Node d = d_nodeManager->mkVar(d_booleanType);
 
     /*structed assuming operator == works */
     TS_ASSERT(iff(a!=a, !(a==a)));
@@ -196,7 +199,7 @@ public:
   /*tests:   Node& operator=(const Node&); */
   void testOperatorAssign() {
     Node a, b;
-    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar());
+    Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar(d_booleanType));
 
     b = c;
     TS_ASSERT(b==c);
@@ -317,8 +320,8 @@ public:
   void testIteNode() {
     /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 
-    Node a = d_nodeManager->mkVar();
-    Node b = d_nodeManager->mkVar();
+    Node a = d_nodeManager->mkVar(d_booleanType);
+    Node b = d_nodeManager->mkVar(d_booleanType);
 
     Node cnd = d_nodeManager->mkNode(PLUS, a, b);
     Node thenBranch = d_nodeManager->mkConst(true);
@@ -380,8 +383,8 @@ public:
   void testGetKind() {
     /*inline Kind getKind() const; */
 
-    Node a = d_nodeManager->mkVar();
-    Node b = d_nodeManager->mkVar();
+    Node a = d_nodeManager->mkVar(d_booleanType);
+    Node b = d_nodeManager->mkVar(d_booleanType);
 
     Node n = d_nodeManager->mkNode(NOT, a);
     TS_ASSERT(NOT == n.getKind());
@@ -463,9 +466,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nodeManager->mkVar();
-    Node y = d_nodeManager->mkVar();
-    Node z = d_nodeManager->mkVar();
+    Node x = d_nodeManager->mkVar(d_booleanType);
+    Node y = d_nodeManager->mkVar(d_booleanType);
+    Node z = d_nodeManager->mkVar(d_booleanType);
     Node n = b << x << y << z << kind::AND;
 
     { // iterator