* 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.

7 files changed, 69 insertions, 46 deletions

diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc
index 09a69e212..982731b34 100644
--- a/test/regress/regress0/error.cvc
+++ b/test/regress/regress0/error.cvc
@@ -1,4 +1,4 @@
 % EXPECT-ERROR: CVC4 Error:
-% EXPECT-ERROR: Parse Error: Parser Error: error.cvc:3.9: Symbol BOOL not declared
+% EXPECT-ERROR: Parse Error: error.cvc:3.9: Symbol BOOL not declared
 p : BOOL;
 % EXIT: 1
diff --git a/test/regress/run_regression b/test/regress/run_regression
index 65ab6c31a..439c8e6c9 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -77,7 +77,17 @@ else
   echo "$expected_error" >"$experrfile"
 fi
 
-("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile"
+cvc4dir=`dirname "$cvc4"`
+cvc4dirfull=`cd "$cvc4dir" && pwd`
+if [ -z "$cvc4dirfull" ]; then
+  error "getting directory of \`$cvc4 !?"
+fi
+cvc4base=`basename "$cvc4"`
+cvc4full="$cvc4dirfull/$cvc4base"
+( cd `dirname "$benchmark"`;
+  "$cvc4full" --segv-nospin `basename "$benchmark"`;
+  echo $? >"$exitstatusfile"
+) > "$outfile" 2> "$errfile"
 
 diffs=`diff -u "$expoutfile" "$outfile"`
 diffexit=$?
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index eb728c62c..e87c8d708 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -70,7 +70,8 @@ public:
   typedef expr::Attribute<MyDataAttributeId, MyData*, MyDataCleanupFunction> MyDataAttribute;
 
   void testDeallocation() {
-    Node* node = new Node(d_nodeManager->mkVar());
+    Type* booleanType = d_nodeManager->booleanType();
+    Node* node = new Node(d_nodeManager->mkVar(booleanType));
     MyData* data;
     MyData* data1;
     MyDataAttribute attr;
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 64c768a13..e0d9d6bf4 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -60,6 +60,7 @@ class AttributeWhite : public CxxTest::TestSuite {
   Context* d_ctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
+  Type* d_booleanType;
 
 public:
 
@@ -67,6 +68,8 @@ public:
     d_ctxt = new Context;
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
+
+    d_booleanType = d_nm->booleanType();
   }
 
   void tearDown() {
@@ -150,9 +153,9 @@ public:
 
     //Debug.on("boolattr");
 
-    Node a = d_nm->mkVar();
-    Node b = d_nm->mkVar();
-    Node c = d_nm->mkVar();
+    Node a = d_nm->mkVar(d_booleanType);
+    Node b = d_nm->mkVar(d_booleanType);
+    Node c = d_nm->mkVar(d_booleanType);
 
     Debug("boolattr", "get flag 1 on a (should be F)\n");
     TS_ASSERT(! a.getAttribute(TestFlag1cd()));
@@ -280,10 +283,10 @@ public:
 
     //Debug.on("boolattr");
 
-    Node a = d_nm->mkVar();
-    Node b = d_nm->mkVar();
-    Node c = d_nm->mkVar();
-    Node unnamed = d_nm->mkVar();
+    Node a = d_nm->mkVar(d_booleanType);
+    Node b = d_nm->mkVar(d_booleanType);
+    Node c = d_nm->mkVar(d_booleanType);
+    Node unnamed = d_nm->mkVar(d_booleanType);
 
     a.setAttribute(VarNameAttr(), "a");
     b.setAttribute(VarNameAttr(), "b");
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
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index 2a7b3623e..eec6949f0 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -37,6 +37,7 @@ private:
   Context* d_ctxt;
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
+  Type* d_booleanType;
 
 public:
 
@@ -44,7 +45,9 @@ public:
     d_ctxt = new Context;
     d_nm = new NodeManager(d_ctxt);
     d_scope = new NodeManagerScope(d_nm);
+
     specKind = PLUS;
+    d_booleanType = d_nm->booleanType();
   }
 
   void tearDown() {
@@ -209,9 +212,9 @@ public:
 
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nm->mkVar();
-    Node y = d_nm->mkVar();
-    Node z = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node y = d_nm->mkVar(d_booleanType);
+    Node z = d_nm->mkVar(d_booleanType);
     b << x << y << z << AND;
 
     {
@@ -460,9 +463,9 @@ public:
   }
 
   void testAppend() {
-    Node x = d_nm->mkVar();
-    Node y = d_nm->mkVar();
-    Node z = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node y = d_nm->mkVar(d_booleanType);
+    Node z = d_nm->mkVar(d_booleanType);
     Node m = d_nm->mkNode(AND, y, z, x);
     Node n = d_nm->mkNode(OR, d_nm->mkNode(NOT, x), y, z);
     Node o = d_nm->mkNode(XOR, y, x);
@@ -587,12 +590,12 @@ public:
   }
 
   void testConvenienceBuilders() {
-    Node a = d_nm->mkVar();
-    Node b = d_nm->mkVar();
-    Node c = d_nm->mkVar();
-    Node d = d_nm->mkVar();
-    Node e = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    Node a = d_nm->mkVar(d_booleanType);
+    Node b = d_nm->mkVar(d_booleanType);
+    Node c = d_nm->mkVar(d_booleanType);
+    Node d = d_nm->mkVar(d_booleanType);
+    Node e = d_nm->mkVar(d_booleanType);
+    Node f = d_nm->mkVar(d_booleanType);
 
     Node m = a && b;
     Node n = a && b || c;
diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h
index a204d79b7..369be5a16 100644
--- a/test/unit/theory/theory_uf_white.h
+++ b/test/unit/theory/theory_uf_white.h
@@ -31,7 +31,6 @@ using namespace CVC4::context;
 
 using namespace std;
 
-
 /**
  * Very basic OutputChannel for testing simple Theory Behaviour.
  * Stores a call sequence for the output channel
@@ -95,6 +94,8 @@ class TheoryUFWhite : public CxxTest::TestSuite {
 
   TheoryUF* d_euf;
 
+  Type* d_booleanType;
+
 public:
 
   TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {}
@@ -105,6 +106,8 @@ public:
     d_scope = new NodeManagerScope(d_nm);
     d_outputChannel.clear();
     d_euf = new TheoryUF(d_ctxt, d_outputChannel);
+
+    d_booleanType = d_nm->booleanType();
   }
 
   void tearDown() {
@@ -116,8 +119,8 @@ public:
   }
 
   void testPushPopChain() {
-    Node x = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node f = d_nm->mkVar(d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -171,8 +174,8 @@ public:
 
   /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */
   void testSimpleChain() {
-    Node x = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node f = d_nm->mkVar(d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -196,7 +199,7 @@ public:
 
   /* test that !(x == x) is inconsistent */
   void testSelfInconsistent() {
-    Node x = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
     Node x_neq_x = (x.eqNode(x)).notNode();
 
     d_euf->assertFact(x_neq_x);
@@ -209,7 +212,7 @@ public:
 
   /* test that (x == x) is consistent */
   void testSelfConsistent() {
-    Node x = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
     Node x_eq_x = x.eqNode(x);
 
     d_euf->assertFact(x_eq_x);
@@ -225,8 +228,8 @@ public:
       f(x) != x
      } is inconsistent */
   void testChain() {
-    Node x = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node f = d_nm->mkVar(d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
@@ -256,7 +259,7 @@ public:
 
 
   void testPushPopA() {
-    Node x = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
     Node x_eq_x = x.eqNode(x);
 
     d_ctxt->push();
@@ -267,8 +270,8 @@ public:
   }
 
   void testPushPopB() {
-    Node x = d_nm->mkVar();
-    Node f = d_nm->mkVar();
+    Node x = d_nm->mkVar(d_booleanType);
+    Node f = d_nm->mkVar(d_booleanType);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_x_eq_x = f_x.eqNode(x);