* Addressed issues brought up in Chris's review of Morgan's
authorMorgan Deters <mdeters@gmail.com>
Sun, 4 Apr 2010 23:03:52 +0000 (23:03 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sun, 4 Apr 2010 23:03:52 +0000 (23:03 +0000)
commitff53861016427723a7c29e9bbca6f497b4556164
tree4ed798e2f7dfa31283f7d14d44e70c77badf6b75
parent42c58baf0a2a96c1f3bd797d64834d02adfb9a59
* 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.
13 files changed:
configure.ac
src/expr/node_builder.h
src/expr/node_manager.cpp
src/expr/node_manager.h
src/parser/input.cpp
src/parser/parser_exception.h
test/regress/regress0/error.cvc
test/regress/run_regression
test/unit/expr/attribute_black.h
test/unit/expr/attribute_white.h
test/unit/expr/node_black.h
test/unit/expr/node_builder_black.h
test/unit/theory/theory_uf_white.h