* Add some protected ContextObj accessors for ContextObj-derived classes:
authorMorgan Deters <mdeters@gmail.com>
Tue, 6 Apr 2010 06:39:01 +0000 (06:39 +0000)
committerMorgan Deters <mdeters@gmail.com>
Tue, 6 Apr 2010 06:39:01 +0000 (06:39 +0000)
commit4143f662e0c5ef311e98dbd554500b98cd02ecdb
tree79abe3f9393d41450ada658dbd3f0914680048c9
parent6ad21b68e654b940d97caea6d34404d0a6b6e628
* Add some protected ContextObj accessors for ContextObj-derived classes:
  + Context* getContext() -- gets the context
  + ContextMemoryManager* getCMM() -- gets the CMM
  + int getLevel() -- the scope level of the ContextObj's most recent update
  + bool isCurrent() -- true iff the most recent update is the current top level

  In particular, the ContextObj::getCMM() call cleans up by TheoryUF's
  ECData::addPredecessor() function substantially (re: code review bug #64).

* Fix serious bugs in context operations that corrupted the ContextObj
  linked lists.  Closes bug #85.

* Identified a bug in the way objects of the "Link" class are
  allocated; see bug #96.

* Re-enable context white-box tests that ensure proper links in linked
  lists.  Closes bug #86.

* Re-enable CDMap<>::emptyTrash().  Closes bug #87.

* Add a tracing option (-t foo or --trace foo) to the driver to enable
  Trace("foo") output stream.  -d foo implies -t foo.

* Minor clean-up of some TheoryUF code; addition of some documentation
  (re: code review bug #64).

* Address some things that caused Doxygen discomfort.

* Address an issue raised in NodeManager's code review (bug #65).

* Remove an inaccurate comment in Attribute code (re: code review bug #61).
16 files changed:
src/context/cdmap.h
src/context/cdo.h
src/context/context.cpp
src/context/context.h
src/context/context_mm.cpp
src/expr/attribute.cpp
src/expr/attribute.h
src/expr/command.cpp
src/expr/expr_manager_template.cpp
src/expr/node_manager.h
src/main/getopt.cpp
src/main/usage.h
src/theory/uf/ecdata.cpp
src/theory/uf/ecdata.h
src/theory/uf/theory_uf.cpp
test/unit/context/context_white.h