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

2 files changed, 15 insertions, 2 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index cd952eef9..a272aaafd 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -81,6 +81,12 @@ enum OptionValue {
  *    getopt_long() returns the 4th entry
  * 4. the return value for getopt_long() when this long option (or the
  *    value to set the 3rd entry to; see #3)
+ *
+ * If you add something here, you should add it in src/main/usage.h
+ * also, to document it.
+ *
+ * If you add something that has a short option equivalent, you should
+ * add it to the getopt_long() call in parseOptions().
  */
 static struct option cmdlineOptions[] = {
   // name, has_arg, *flag, val
@@ -91,6 +97,7 @@ static struct option cmdlineOptions[] = {
   { "quiet"      , no_argument      , NULL, 'q'         },
   { "lang"       , required_argument, NULL, 'L'         },
   { "debug"      , required_argument, NULL, 'd'         },
+  { "trace"      , required_argument, NULL, 't'         },
   { "smtcomp"    , no_argument      , NULL, SMTCOMP     },
   { "stats"      , no_argument      , NULL, STATS       },
   { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
@@ -131,7 +138,7 @@ throw(OptionException) {
   // cmdlineOptions specifies all the long-options and the return
   // value for getopt_long() should they be encountered.
   while((c = getopt_long(argc, argv,
-                         "+:hVvqL:d:",
+                         "+:hVvqL:d:t:",
                          cmdlineOptions, NULL)) != -1) {
     switch(c) {
 
@@ -171,8 +178,13 @@ throw(OptionException) {
       fputs(lang_help, stdout);
       exit(1);
 
+    case 't':
+      Trace.on(optarg);
+      break;
+
     case 'd':
       Debug.on(optarg);
+      Trace.on(optarg);
       /* fall-through */
 
     case STATS:
diff --git a/src/main/usage.h b/src/main/usage.h
index 3a609d2ec..c8ca6a179 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -32,7 +32,8 @@ CVC4 options:\n\
    --help | -h     this command line reference\n\
    --verbose | -v  increase verbosity (repeatable)\n\
    --quiet | -q    decrease verbosity (repeatable)\n\
-   --debug | -d    debugging for something (e.g. --debug arith)\n\
+   --trace | -t    tracing for something (e.g. --trace pushpop)\n\
+   --debug | -d    debugging for something (e.g. --debug arith), implies -t\n\
    --smtcomp       competition mode (very quiet)\n\
    --stats         give statistics on exit\n\
    --segv-nospin   (debug builds only) don't spin on segfault waiting for gdb\n\