A bag of unrelated fixes to bring trunk more in-line with recent
authorMorgan Deters <mdeters@gmail.com>
Sat, 27 Feb 2010 23:43:24 +0000 (23:43 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sat, 27 Feb 2010 23:43:24 +0000 (23:43 +0000)
commit0eb82499822544f96877f317bbbcd4cb7c644614
tree7abbd631cb9c5e065883f9eb8babccc62a9fbb00
parente56c41f47d43103a6e8bf744e12229ed6e5a8f19
A bag of unrelated fixes to bring trunk more in-line with recent
policy discussion (no dead code, no unimplemented unit tests...), and
other fixes:

* src/expr/node_builder.h: uncomment AndNodeBuilder, OrNodeBuilder,
  PlusNodeBuilder, and MultNodeBuilder.  (These had been dead code for
  awhile.)

* src/expr/node_value.cpp: toString() is much more reasonable now,
  printing S-exprs and using variable names (instead of printing raw
  pointer values).  Next, we'll want to define a pretty-printing
  theory interface and perhaps hook this up to that.

* test/unit/expr/node_black.h: implement testIterator(),
  testToString(), and testToStream().

* test/unit/expr/node_builder_black.h: implement testIterator() and
  testAppend(), and add some code to avoid the warnings on clear() for
  unused NodeBuilders.

* src/expr/node_builder.h: redefine "iterator" to be over Nodes rather
  than over NodeValues.  Doesn't make sense to expose the underlying
  NodeValues.  This shouldn't affect anyone, no one was using
  NodeBuilder iterators.

* fix some comments in source code
src/expr/node_builder.h
src/expr/node_value.cpp
src/expr/node_value.h
src/smt/smt_engine.h
src/theory/arith/kinds
src/theory/theoryof_table_epilogue.h
src/theory/theoryof_table_middle.h
src/theory/theoryof_table_prologue.h
test/unit/expr/node_black.h
test/unit/expr/node_builder_black.h