Merge from nonclausal-simplification-v2 branch:

* Preprocessing-time, non-clausal, Boolean simplification round to
  support "quasi-non-linear rewrites" as discussed at last few meetings.

* --simplification=none is the default for now, but we'll probably
  change that to --simplification=incremental.  --simplification=batch
  is also a possibility.  See --simplification=help for details.

* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.

13 files changed, 538 insertions, 52 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 27b9e42d2..20806464d 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -51,6 +51,8 @@ libutil_la_SOURCES = \
 	subrange_bound.h \
 	cardinality.h \
 	cardinality.cpp \
+	cache.h \
+	utility.h \
 	trans_closure.h \
 	trans_closure.cpp \
 	boolean_simplification.h \
diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp
index a154f342f..92534bfd4 100644
--- a/src/util/boolean_simplification.cpp
+++ b/src/util/boolean_simplification.cpp
@@ -20,7 +20,7 @@
 
 namespace CVC4 {
 
-void
+bool
 BooleanSimplification::push_back_associative_commute_recursive
     (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
     throw(AssertionException) {
@@ -28,17 +28,40 @@ BooleanSimplification::push_back_associative_commute_recursive
   for(; i != end; ++i){
     Node child = *i;
     if(child.getKind() == k){
-      push_back_associative_commute_recursive(child, buffer, k, notK, negateNode);
+      if(! push_back_associative_commute_recursive(child, buffer, k, notK, negateNode)) {
+        return false;
+      }
     }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){
-      push_back_associative_commute_recursive(child, buffer, notK, k, !negateNode);
+      if(! push_back_associative_commute_recursive(child[0], buffer, notK, k, !negateNode)) {
+        return false;
+      }
     }else{
       if(negateNode){
-        buffer.push_back(negate(child));
+        if(child.getMetaKind() == kind::metakind::CONSTANT) {
+          if((k == kind::AND && child.getConst<bool>()) ||
+             (k == kind::OR && !child.getConst<bool>())) {
+            buffer.clear();
+            buffer.push_back(negate(child));
+            return false;
+          }
+        } else {
+          buffer.push_back(negate(child));
+        }
       }else{
-        buffer.push_back(child);
+        if(child.getMetaKind() == kind::metakind::CONSTANT) {
+          if((k == kind::OR && child.getConst<bool>()) ||
+             (k == kind::AND && !child.getConst<bool>())) {
+            buffer.clear();
+            buffer.push_back(child);
+            return false;
+          }
+        } else {
+          buffer.push_back(child);
+        }
       }
     }
   }
+  return true;
 }/* BooleanSimplification::push_back_associative_commute_recursive() */
 
 }/* CVC4 namespace */
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
index e938a2b38..c2da8af5b 100644
--- a/src/util/boolean_simplification.h
+++ b/src/util/boolean_simplification.h
@@ -39,9 +39,9 @@ class BooleanSimplification {
   BooleanSimplification() CVC4_UNUSED;
   BooleanSimplification(const BooleanSimplification&) CVC4_UNUSED;
 
-  static void push_back_associative_commute_recursive
+  static bool push_back_associative_commute_recursive
     (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
-    throw(AssertionException);
+    throw(AssertionException) CVC4_WARN_UNUSED_RESULT;
 
 public:
 
@@ -80,6 +80,10 @@ public:
 
     removeDuplicates(buffer);
 
+    if(buffer.size() == 1) {
+      return buffer[0];
+    }
+
     NodeBuilder<> nb(kind::AND);
     nb.append(buffer);
     return nb;
@@ -100,6 +104,11 @@ public:
 
     removeDuplicates(buffer);
 
+    Assert(buffer.size() > 0);
+    if(buffer.size() == 1) {
+      return buffer[0];
+    }
+
     NodeBuilder<> nb(kind::OR);
     nb.append(buffer);
     return nb;
@@ -138,10 +147,14 @@ public:
    * @param k the kind to collapse (should equal the kind of node n)
    * @param notK the "negation" of kind k (e.g. OR's negation is AND),
    * or kind::UNDEFINED_KIND if none.
+   * @param negateChildren true if the children of the resulting node
+   * (that is, the elements in buffer) should all be negated; you want
+   * this if e.g. you're simplifying the (OR...) in (NOT (OR...)),
+   * intending to make the result an AND.
    */
   static inline void
   push_back_associative_commute(Node n, std::vector<Node>& buffer,
-                                Kind k, Kind notK)
+                                Kind k, Kind notK, bool negateChildren = false)
       throw(AssertionException) {
     AssertArgument(buffer.empty(), buffer);
     AssertArgument(!n.isNull(), n);
@@ -150,7 +163,13 @@ public:
     AssertArgument(n.getKind() == k, n,
                    "expected node to have kind %s", kindToString(k).c_str());
 
-    push_back_associative_commute_recursive(n, buffer, k, notK, false);
+    bool b CVC4_UNUSED =
+      push_back_associative_commute_recursive(n, buffer, k, notK, false);
+
+    if(buffer.size() == 0) {
+      // all the TRUEs for an AND (resp FALSEs for an OR) were simplified away
+      buffer.push_back(NodeManager::currentNM()->mkConst(k == kind::AND ? true : false));
+    }
   }/* push_back_associative_commute() */
 
   /**
@@ -168,6 +187,9 @@ public:
       base = base[0];
       polarity = !polarity;
     }
+    if(n.getMetaKind() == kind::metakind::CONSTANT) {
+      return NodeManager::currentNM()->mkConst(!n.getConst<bool>());
+    }
     if(polarity){
       return base.notNode();
     }else{
@@ -175,6 +197,26 @@ public:
     }
   }
 
+  /**
+   * Simplify an OR, AND, or IMPLIES.  This function is the identity
+   * for all other kinds.
+   */
+  inline static Node simplify(TNode n) throw(AssertionException) {
+    switch(n.getKind()) {
+    case kind::AND:
+      return simplifyConflict(n);
+
+    case kind::OR:
+      return simplifyClause(n);
+
+    case kind::IMPLIES:
+      return simplifyHornClause(n);
+
+    default:
+      return n;
+    }
+  }
+
 };/* class BooleanSimplification */
 
 }/* CVC4 namespace */
diff --git a/src/util/cache.h b/src/util/cache.h
new file mode 100644
index 000000000..08c624d99
--- /dev/null
+++ b/src/util/cache.h
@@ -0,0 +1,129 @@
+/*********************                                                        */
+/*! \file cache.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A generic Cache<> template class for use by functions that
+ ** walk the Node DAG and want to cache results for sub-DAGs
+ **
+ ** A generic Cache<> template class for use by functions that walk
+ ** the Node DAG and want to cache results for sub-DAGs.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CACHE_H
+#define __CVC4__CACHE_H
+
+#include <utility>
+#include <functional>
+
+namespace CVC4 {
+
+/**
+ * A generic implementation of a cache for functions that walk the
+ * Node DAG performing a computation and want to cache some or all
+ * computations.
+ */
+template <class T, class U, class Hasher = std::hash<T> >
+class Cache {
+  typedef std::hash_map<T, U, Hasher> Map;
+  Map d_map;
+  std::vector<T> d_current;
+  typename Map::iterator d_result;
+
+  // disallow copy/assignment
+  Cache(const Cache&) CVC4_UNUSED;
+  Cache& operator=(const Cache&) CVC4_UNUSED;
+
+public:
+
+  typedef T key_type;
+  typedef U value_type;
+  typedef Hasher hash_function;
+
+  /**
+   * Makes it easy and error-free to use a Cache<> in a function.
+   */
+  class Scope {
+    Cache& d_cache;
+    bool d_fired;
+
+  public:
+    Scope(Cache<T, U, Hasher>& cache, const T& elt) throw(AssertionException) :
+      d_cache(cache),
+      d_fired(d_cache.computing(elt)) {
+    }
+
+    ~Scope() {
+      if(!d_fired) {
+        d_cache();// pop stack
+      }
+    }
+
+    operator bool() throw() {
+      return d_fired;
+    }
+
+    const U& get() throw(AssertionException) {
+      Assert(d_fired, "nothing in cache");
+      return d_cache.get();
+    }
+
+    U& operator()(U& computed) throw(AssertionException) {
+      Assert(!d_fired, "can only cache a computation once");
+      d_fired = true;
+      return d_cache(computed);
+    }
+    const U& operator()(const U& computed) throw(AssertionException) {
+      Assert(!d_fired, "can only cache a computation once");
+      d_fired = true;
+      return d_cache(computed);
+    }
+  };/* class Cache::Scope */
+
+  Cache() {}
+
+  bool computing(const T& elt) {
+    d_result = d_map.find(elt);
+    bool found = (d_result != d_map.end());
+    if(!found) {
+      d_current.push_back(elt);
+    }
+    return found;
+  }
+
+  const U& get() {
+    Assert(d_result != d_map.end());
+    return (*d_result).second;
+  }
+
+  // cache nothing (just pop)
+  void operator()() {
+    d_current.pop_back();
+  }
+
+  U& operator()(U& result) {
+    d_map.insert(d_current.back(), result);
+    d_current.pop_back();
+    return result;
+  }
+  const U& operator()(const U& result) {
+    d_map.insert(std::make_pair(d_current.back(), result));
+    d_current.pop_back();
+    return result;
+  }
+};/* class Cache<> */
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CACHE_H */
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 2a3f69fd6..ab52e7f93 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -109,7 +109,7 @@ void Datatype::addConstructor(const Constructor& c) {
 
 Cardinality Datatype::getCardinality() const throw(AssertionException) {
   CheckArgument(isResolved(), this, "this datatype is not yet resolved");
-  RecursionBreaker<const Datatype*> breaker(__PRETTY_FUNCTION__, this);
+  RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
   if(breaker.isRecursion()) {
     return Cardinality::INTEGERS;
   }
@@ -159,7 +159,7 @@ bool Datatype::isWellFounded() const throw(AssertionException) {
     return self.getAttribute(DatatypeWellFoundedAttr());
   }
 
-  RecursionBreaker<const Datatype*> breaker(__PRETTY_FUNCTION__, this);
+  RecursionBreaker<const Datatype*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
   if(breaker.isRecursion()) {
     // This *path* is cyclic, so may not be well-founded.  The
     // datatype itself might still be well-founded, though (we'll find
@@ -518,7 +518,7 @@ bool Datatype::Constructor::isWellFounded() const throw(AssertionException) {
     return self.getAttribute(DatatypeWellFoundedAttr());
   }
 
-  RecursionBreaker<const Datatype::Constructor*> breaker(__PRETTY_FUNCTION__, this);
+  RecursionBreaker<const Datatype::Constructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
   if(breaker.isRecursion()) {
     // This *path* is cyclic, sso may not be well-founded.  The
     // constructor itself might still be well-founded, though (we'll
@@ -563,7 +563,7 @@ Expr Datatype::Constructor::mkGroundTerm() const throw(AssertionException) {
     return groundTerm;
   }
 
-  RecursionBreaker<const Datatype::Constructor*> breaker(__PRETTY_FUNCTION__, this);
+  RecursionBreaker<const Datatype::Constructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
   if(breaker.isRecursion()) {
     // Recursive path, we should skip and go to the next constructor;
     // see lengthy comments in Datatype::mkGroundTerm().
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 75da1405f..7d9ae6f39 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -427,6 +427,24 @@ struct CVC4_PUBLIC DatatypeHashStrategy {
   }
 };/* struct DatatypeHashStrategy */
 
+/**
+ * A hash function for Datatypes.  Needed to store them in hash sets
+ * and hash maps.
+ */
+struct CVC4_PUBLIC DatatypeHashFunction {
+  inline size_t operator()(const Datatype& dt) const {
+    return StringHashFunction()(dt.getName());
+  }
+  inline size_t operator()(const Datatype* dt) const {
+    return StringHashFunction()(dt->getName());
+  }
+  inline size_t operator()(const Datatype::Constructor& dtc) const {
+    return StringHashFunction()(dtc.getName());
+  }
+  inline size_t operator()(const Datatype::Constructor* dtc) const {
+    return StringHashFunction()(dtc->getName());
+  }
+};/* struct DatatypeHashFunction */
 
 // FUNCTION DECLARATIONS FOR OUTPUT STREAMS
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 1329a443a..dbe0f6804 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -69,6 +69,8 @@ Options::Options() :
   memoryMap(false),
   strictParsing(false),
   lazyDefinitionExpansion(false),
+  simplificationMode(INCREMENTAL_MODE),
+  simplificationStyle(NO_SIMPLIFICATION_STYLE),
   interactive(false),
   interactiveSetByUser(false),
   segvNoSpin(false),
@@ -83,7 +85,7 @@ Options::Options() :
   rewriteArithEqualities(false),
   arithPropagation(false),
   satRandomFreq(0.0),
-  satRandomSeed(91648253), //Minisat's default value
+  satRandomSeed(91648253),// Minisat's default value
   pivotRule(MINIMUM)
 {
 }
@@ -102,10 +104,10 @@ static const string optionsDescription = "\
    --no-checking          disable ALL semantic checks, including type checks\n\
    --no-theory-registration disable theory reg (not safe for some theories)\n\
    --strict-parsing       fail on non-conformant inputs (SMT2 only)\n\
-   --verbose | -v         increase verbosity (repeatable)\n\
-   --quiet | -q           decrease verbosity (repeatable)\n\
-   --trace | -t           tracing for something (e.g. --trace pushpop)\n\
-   --debug | -d           debugging for something (e.g. --debug arith), implies -t\n\
+   --verbose | -v         increase verbosity (may be repeated)\n\
+   --quiet | -q           decrease verbosity (may be repeated)\n\
+   --trace | -t           trace something (e.g. -t pushpop), can repeat\n\
+   --debug | -d           debug something (e.g. -d arith), can repeat\n\
    --stats                give statistics on exit\n\
    --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
    --print-expr-types     print types with variables when printing exprs\n\
@@ -115,8 +117,9 @@ static const string optionsDescription = "\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
    --lazy-definition-expansion expand define-fun lazily\n\
-   --replay file          replay decisions from file\n\
-   --replay-log file      log decisions and propagations to file\n\
+   --simplification=MODE  choose simplification mode, see --simplification=help\n\
+   --replay=file          replay decisions from file\n\
+   --replay-log=file      log decisions and propagations to file\n\
    --pivot-rule=RULE      change the pivot rule (see --pivot-rule help)\n\
    --random-freq=P        sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\
    --random-seed=S        sets the random seed for the sat solver\n\
@@ -132,14 +135,42 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt2 | smtlib2 SMT-LIB format 2.0\n\
 ";
 
+static const string simplificationHelp = "\
+Simplification modes currently supported by the --simplification option:\n\
+\n\
+batch\n\
++ save up all ASSERTions; run nonclausal simplification and clausal\n\
+  (MiniSat) propagation for all of them only after reaching a querying command\n\
+  (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
+\n\
+incremental (default)\n\
++ run nonclausal simplification and clausal propagation at each ASSERT\n\
+  (and at CHECKSAT/QUERY/SUBTYPE)\n\
+\n\
+incremental-lazy-sat\n\
++ run nonclausal simplification at each ASSERT, but delay clausification of\n\
+  ASSERT until reaching a CHECKSAT/QUERY/SUBTYPE, then clausify them all\n\
+\n\
+You can also specify the level of aggressiveness for the simplification\n\
+(by repeating the --simplification option):\n\
+\n\
+toplevel (default)\n\
++ apply toplevel simplifications (things known true/false at outer level\n\
+  only)\n\
+\n\
+aggressive\n\
++ do aggressive, local simplification across the entire formula\n\
+\n\
+none\n\
++ do not perform nonclausal simplification\n\
+";
+
 string Options::getDescription() const {
   return optionsDescription;
 }
 
 void Options::printUsage(const std::string msg, std::ostream& out) {
   out << msg << optionsDescription << endl << flush;
-  // printf(usage + options.getDescription(), options.binary_name.c_str());
-  //     printf(usage, binary_name.c_str());
 }
 
 void Options::printLanguageHelp(std::ostream& out) {
@@ -155,7 +186,7 @@ void Options::printLanguageHelp(std::ostream& out) {
  * any collision.
  */
 enum OptionValue {
-  SMTCOMP = 256, /* no clash with char options */
+  SMTCOMP = 256, /* avoid clashing with char options */
   STATS,
   SEGV_NOSPIN,
   PARSE_ONLY,
@@ -168,6 +199,7 @@ enum OptionValue {
   PRINT_EXPR_TYPES,
   UF_THEORY,
   LAZY_DEFINITION_EXPANSION,
+  SIMPLIFICATION_MODE,
   INTERACTIVE,
   NO_INTERACTIVE,
   PRODUCE_MODELS,
@@ -231,6 +263,7 @@ static struct option cmdlineOptions[] = {
   { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
   { "uf"         , required_argument, NULL, UF_THEORY   },
   { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
+  { "simplification", required_argument, NULL, SIMPLIFICATION_MODE },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { "produce-models", no_argument   , NULL, PRODUCE_MODELS },
@@ -397,8 +430,8 @@ throw(OptionException) {
           uf_implementation = Options::MORGAN;
         } else if(!strcmp(optarg, "help")) {
           printf("UF implementations available:\n");
-          printf("tim\n");
-          printf("morgan\n");
+          printf("  tim\n");
+          printf("  morgan\n");
           exit(1);
         } else {
           throw OptionException(string("unknown option for --uf: `") +
@@ -411,6 +444,28 @@ throw(OptionException) {
       lazyDefinitionExpansion = true;
       break;
 
+    case SIMPLIFICATION_MODE:
+      if(!strcmp(optarg, "batch")) {
+        simplificationMode = BATCH_MODE;
+      } else if(!strcmp(optarg, "incremental")) {
+        simplificationMode = INCREMENTAL_MODE;
+      } else if(!strcmp(optarg, "incremental-lazy-sat")) {
+        simplificationMode = INCREMENTAL_LAZY_SAT_MODE;
+      } else if(!strcmp(optarg, "aggressive")) {
+        simplificationStyle = AGGRESSIVE_SIMPLIFICATION_STYLE;
+      } else if(!strcmp(optarg, "toplevel")) {
+        simplificationStyle = TOPLEVEL_SIMPLIFICATION_STYLE;
+      } else if(!strcmp(optarg, "none")) {
+        simplificationStyle = NO_SIMPLIFICATION_STYLE;
+      } else if(!strcmp(optarg, "help")) {
+        puts(simplificationHelp.c_str());
+        exit(1);
+      } else {
+        throw OptionException(string("unknown option for --simplification: `") +
+                              optarg + "'.  Try --simplification help.");
+      }
+      break;
+
     case INTERACTIVE:
       interactive = true;
       interactiveSetByUser = true;
@@ -545,14 +600,12 @@ throw(OptionException) {
       printf("tls        : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
       exit(0);
 
-    case '?':
-      throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
-
     case ':':
       throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
 
+    case '?':
     default:
-      throw OptionException(string("can't understand option:") + argv[optind - 1] + "'");
+      throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
     }
 
   }
diff --git a/src/util/options.h b/src/util/options.h
index be432e5a7..d9d9c8567 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -34,7 +34,7 @@ namespace CVC4 {
 class ExprStream;
 
 /** Class representing an option-parsing exception. */
-class OptionException : public CVC4::Exception {
+class CVC4_PUBLIC OptionException : public CVC4::Exception {
 public:
     OptionException(const std::string& s) throw() :
       CVC4::Exception("Error in option parsing: " + s) {
@@ -104,6 +104,25 @@ struct CVC4_PUBLIC Options {
   /** Should we expand function definitions lazily? */
   bool lazyDefinitionExpansion;
 
+  /** Enumeration of simplification modes (when to simplify). */
+  typedef enum {
+    BATCH_MODE,
+    INCREMENTAL_MODE,
+    INCREMENTAL_LAZY_SAT_MODE
+  } SimplificationMode;
+  /** When to perform nonclausal simplifications. */
+  SimplificationMode simplificationMode;
+
+  /** Enumeration of simplification styles (how much to simplify). */
+  typedef enum {
+    AGGRESSIVE_SIMPLIFICATION_STYLE,
+    TOPLEVEL_SIMPLIFICATION_STYLE,
+    NO_SIMPLIFICATION_STYLE
+  } SimplificationStyle;
+
+  /** Style of nonclausal simplifications to perform. */
+  SimplificationStyle simplificationStyle;
+
   /** Whether we're in interactive mode or not */
   bool interactive;
 
@@ -188,6 +207,9 @@ struct CVC4_PUBLIC Options {
 };/* struct Options */
 
 inline std::ostream& operator<<(std::ostream& out,
+                                Options::UfImplementation uf) CVC4_PUBLIC;
+
+inline std::ostream& operator<<(std::ostream& out,
                                 Options::UfImplementation uf) {
   switch(uf) {
   case Options::TIM:
@@ -203,7 +225,28 @@ inline std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
-std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule);
+inline std::ostream& operator<<(std::ostream& out,
+                                Options::SimplificationMode mode) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out,
+                                Options::SimplificationMode mode) {
+  switch(mode) {
+  case Options::BATCH_MODE:
+    out << "BATCH_MODE";
+    break;
+  case Options::INCREMENTAL_MODE:
+    out << "INCREMENTAL_MODE";
+    break;
+  case Options::INCREMENTAL_LAZY_SAT_MODE:
+    out << "INCREMENTAL_LAZY_SAT_MODE";
+    break;
+  default:
+    out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]";
+  }
+
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) CVC4_PUBLIC;
 
 }/* CVC4 namespace */
 
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 88628481f..29de4c360 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -31,6 +31,9 @@ ostream null_os(&null_sb);
 
 NullC nullCvc4Stream CVC4_PUBLIC;
 
+const std::string CVC4ostream::s_tab = "  ";
+const int CVC4ostream::s_indentIosIndex = ios_base::xalloc();
+
 DebugC DebugChannel CVC4_PUBLIC (&cout);
 WarningC WarningChannel CVC4_PUBLIC (&cerr);
 MessageC MessageChannel CVC4_PUBLIC (&cout);
diff --git a/src/util/output.h b/src/util/output.h
index b0e210c17..6d0f27f2a 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -21,6 +21,7 @@
 #ifndef __CVC4__OUTPUT_H
 #define __CVC4__OUTPUT_H
 
+#include <ios>
 #include <iostream>
 #include <string>
 #include <cstdio>
@@ -59,20 +60,42 @@ extern null_streambuf null_sb;
 extern std::ostream null_os CVC4_PUBLIC;
 
 class CVC4_PUBLIC CVC4ostream {
+  static const std::string s_tab;
+  static const int s_indentIosIndex;
+
+  /** The underlying ostream */
   std::ostream* d_os;
-  // Current indentation
-  unsigned d_indent;
+  /** Are we in the first column? */
+  bool d_firstColumn;
 
-  std::ostream& (*d_endl)(std::ostream&);
+  /** The endl manipulator (why do we need to keep this?) */
+  std::ostream& (*const d_endl)(std::ostream&);
 
 public:
-  CVC4ostream() : d_os(NULL) {}
-  explicit CVC4ostream(std::ostream* os) : d_os(os), d_indent(0) {
-    d_endl = &std::endl;
+  CVC4ostream() :
+    d_os(NULL),
+    d_firstColumn(false),
+    d_endl(&std::endl) {
+  }
+  explicit CVC4ostream(std::ostream* os) :
+    d_os(os),
+    d_firstColumn(true),
+    d_endl(&std::endl) {
   }
 
-  void pushIndent() { d_indent ++; }
-  void popIndent()  { if (d_indent > 0) -- d_indent; }
+  void pushIndent() {
+    if(d_os != NULL) {
+      ++d_os->iword(s_indentIosIndex);
+    }
+  }
+  void popIndent() {
+    if(d_os != NULL) {
+      long& indent = d_os->iword(s_indentIosIndex);
+      if(indent > 0) {
+        --indent;
+      }
+    }
+  }
 
   CVC4ostream& flush() {
     if(d_os != NULL) {
@@ -87,6 +110,13 @@ public:
   template <class T>
   CVC4ostream& operator<<(T const& t) {
     if(d_os != NULL) {
+      if(d_firstColumn) {
+        d_firstColumn = false;
+        long indent = d_os->iword(s_indentIosIndex);
+        for(long i = 0; i < indent; ++ i) {
+          d_os = &(*d_os << s_tab);
+        }
+      }
       d_os = &(*d_os << t);
     }
     return *this;
@@ -97,10 +127,8 @@ public:
     if(d_os != NULL) {
       d_os = &(*d_os << pf);
 
-      if (pf == d_endl) {
-        for (unsigned i = 0; i < d_indent; ++ i) {
-          d_os = &(*d_os << '\t');
-        }
+      if(pf == d_endl) {
+        d_firstColumn = true;
       }
     }
     return *this;
@@ -452,6 +480,27 @@ public:
 
 extern NullC nullCvc4Stream CVC4_PUBLIC;
 
+/**
+ * Pushes an indentation level on construction, pop on destruction.
+ * Useful for tracing recursive functions especially, but also can be
+ * used for clearly separating different phases of an algorithm,
+ * or iterations of a loop, or... etc.
+ */
+class IndentedScope {
+  CVC4ostream d_out;
+public:
+  inline IndentedScope(CVC4ostream out);
+  inline ~IndentedScope();
+};/* class IndentedScope */
+
+#ifdef CVC4_DEBUG
+inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; }
+inline IndentedScope::~IndentedScope() { d_out << pop; }
+#else /* CVC4_DEBUG */
+inline IndentedScope::IndentedScope(CVC4ostream out) {}
+inline IndentedScope::~IndentedScope() {}
+#endif /* CVC4_DEBUG */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__OUTPUT_H */
diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h
index 6f82eec5c..6573e9b64 100644
--- a/src/util/recursion_breaker.h
+++ b/src/util/recursion_breaker.h
@@ -79,10 +79,9 @@
 
 namespace CVC4 {
 
-template <class T>
+template <class T, class Hasher = std::hash<T> >
 class RecursionBreaker {
-  //typedef std::hash_set<T> Set;
-  typedef std::set<T> Set;
+  typedef std::hash_set<T, Hasher> Set;
   typedef std::map<std::string, Set> Map;
   static CVC4_THREADLOCAL(Map*) s_maps;
 
@@ -92,6 +91,7 @@ class RecursionBreaker {
   bool d_recursion;
 
 public:
+  /** Mark that item has been seen for tag. */
   RecursionBreaker(std::string tag, const T& item) :
     d_tag(tag),
     d_item(item) {
@@ -107,6 +107,7 @@ public:
     }
   }
 
+  /** Clean up the seen trail. */
   ~RecursionBreaker() {
     Assert(s_maps->find(d_tag) != s_maps->end());
     if(!d_recursion) {
@@ -119,14 +120,15 @@ public:
     }
   }
 
+  /** Return true iff recursion has been detected. */
   bool isRecursion() const throw() {
     return d_recursion;
   }
 
 };/* class RecursionBreaker<T> */
 
-template <class T>
-CVC4_THREADLOCAL(typename RecursionBreaker<T>::Map*) RecursionBreaker<T>::s_maps;
+template <class T, class Hasher>
+CVC4_THREADLOCAL(typename RecursionBreaker<T, Hasher>::Map*) RecursionBreaker<T, Hasher>::s_maps;
 
 }/* CVC4 namespace */
 
diff --git a/src/util/tls.h.in b/src/util/tls.h.in
index c2892d11c..fc0b6932b 100644
--- a/src/util/tls.h.in
+++ b/src/util/tls.h.in
@@ -26,13 +26,17 @@
 
 #line 28 "@srcdir@/tls.h.in"
 
+// A bit obnoxious: we have to take varargs to support multi-argument
+// template types in the threadlocals.
+// E.g. "CVC4_THREADLOCAL(hash_set<type, hasher>*)" fails otherwise,
+// due to the embedded comma.
 #if @CVC4_TLS_SUPPORTED@
-#  define CVC4_THREADLOCAL(__type) @CVC4_TLS@ __type
-#  define CVC4_THREADLOCAL_PUBLIC(__type) @CVC4_TLS@ CVC4_PUBLIC __type
+#  define CVC4_THREADLOCAL(__type...) @CVC4_TLS@ __type
+#  define CVC4_THREADLOCAL_PUBLIC(__type...) @CVC4_TLS@ CVC4_PUBLIC __type
 #else
 #  include <pthread.h>
-#  define CVC4_THREADLOCAL(__type) ::CVC4::ThreadLocal< __type >
-#  define CVC4_THREADLOCAL_PUBLIC(__type) CVC4_PUBLIC ::CVC4::ThreadLocal< __type >
+#  define CVC4_THREADLOCAL(__type...) ::CVC4::ThreadLocal< __type >
+#  define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC ::CVC4::ThreadLocal< __type >
 
 namespace CVC4 {
 
@@ -76,6 +80,49 @@ public:
 };/* class ThreadLocalImpl<T, true> */
 
 template <class T>
+class ThreadLocalImpl<T*, true> {
+  pthread_key_t d_key;
+
+  static void cleanup(void*) {
+  }
+
+public:
+  ThreadLocalImpl() {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+  }
+
+  ThreadLocalImpl(const T* t) {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
+  }
+
+  ThreadLocalImpl(const ThreadLocalImpl& tl) {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl))));
+  }
+
+  ThreadLocalImpl& operator=(const T* t) {
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
+    return *this;
+  }
+  ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) {
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl))));
+    return *this;
+  }
+
+  operator T*() const {
+    return static_cast<T*>(pthread_getspecific(d_key));
+  }
+
+  T operator*() {
+    return *static_cast<T*>(pthread_getspecific(d_key));
+  }
+  T* operator->() {
+    return static_cast<T*>(pthread_getspecific(d_key));
+  }
+};/* class ThreadLocalImpl<T*, true> */
+
+template <class T>
 class ThreadLocalImpl<T, false> {
 };/* class ThreadLocalImpl<T, false> */
 
diff --git a/src/util/utility.h b/src/util/utility.h
new file mode 100644
index 000000000..9aa4c1158
--- /dev/null
+++ b/src/util/utility.h
@@ -0,0 +1,75 @@
+/*********************                                                        */
+/*! \file utility.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Some standard STL-related utility functions for CVC4
+ **
+ ** Some standard STL-related utility functions for CVC4.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__UTILITY_H
+#define __CVC4__UTILITY_H
+
+#include <utility>
+#include <functional>
+
+namespace CVC4 {
+
+
+/**
+ * Like std::equal_to<>, but tests equality between the first element
+ * of a pair and an element.
+ */
+template <class T, class U>
+struct first_equal_to : std::binary_function<std::pair<T, U>, T, bool> {
+  bool operator()(const std::pair<T, U>& pr, const T& x) const {
+    return pr.first == x;
+  }
+};/* struct first_equal_to<T> */
+
+
+/**
+ * Like std::equal_to<>, but tests equality between the second element
+ * of a pair and an element.
+ */
+template <class T, class U>
+struct second_equal_to : std::binary_function<std::pair<T, U>, U, bool> {
+  bool operator()(const std::pair<T, U>& pr, const U& x) const {
+    return pr.second == x;
+  }
+};/* struct first_equal_to<T> */
+
+
+/**
+ * Using std::find_if(), finds the first iterator in [first,last)
+ * range that satisfies predicate.  If none, return last; otherwise,
+ * search for a second one.  If there IS a second one, return last,
+ * otherwise return the first (and unique) iterator satisfying pred().
+ */
+template <class InputIterator, class Predicate>
+inline InputIterator find_if_unique(InputIterator first, InputIterator last, Predicate pred) {
+  InputIterator match = std::find_if(first, last, pred);
+  if(match == last) {
+    return last;
+  }
+
+  InputIterator match2 = match;
+  match2 = std::find_if(++match2, last, pred);
+  return (match2 == last) ? match : last;
+}
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UTILITY_H */