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.

6 files changed, 272 insertions, 33 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index d300b27de..f416f84bb 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -279,6 +279,28 @@ void DefineNamedFunctionCommand::toStream(std::ostream& out) const {
   out << " )";
 }
 
+/* class Simplify */
+
+SimplifyCommand::SimplifyCommand(Expr term) :
+  d_term(term) {
+}
+
+void SimplifyCommand::invoke(SmtEngine* smtEngine) {
+  d_result = smtEngine->simplify(d_term);
+}
+
+Expr SimplifyCommand::getResult() const {
+  return d_result;
+}
+
+void SimplifyCommand::printResult(std::ostream& out) const {
+  out << d_result << endl;
+}
+
+void SimplifyCommand::toStream(std::ostream& out) const {
+  out << "Simplify( << " << d_term << " >> )";
+}
+
 /* class GetValueCommand */
 
 GetValueCommand::GetValueCommand(Expr term) :
diff --git a/src/expr/command.h b/src/expr/command.h
index 17736ed77..d0b72c3dd 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -164,6 +164,19 @@ public:
   void toStream(std::ostream& out) const;
 };/* class QueryCommand */
 
+// this is TRANSFORM in the CVC presentation language
+class CVC4_PUBLIC SimplifyCommand : public Command {
+protected:
+  Expr d_term;
+  Expr d_result;
+public:
+  SimplifyCommand(Expr term);
+  void invoke(SmtEngine* smtEngine);
+  Expr getResult() const;
+  void printResult(std::ostream& out) const;
+  void toStream(std::ostream& out) const;
+};/* class SimplifyCommand */
+
 class CVC4_PUBLIC GetValueCommand : public Command {
 protected:
   Expr d_term;
diff --git a/src/expr/node.h b/src/expr/node.h
index a40b3fce5..9351293f8 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -11,7 +11,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Reference-counted encapsulation of a pointer to node information.
+ ** \brief Reference-counted encapsulation of a pointer to node information
  **
  ** Reference-counted encapsulation of a pointer to node information.
  **/
@@ -29,7 +29,7 @@
 #include <iostream>
 #include <stdint.h>
 
-#include "type.h"
+#include "expr/type.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/expr.h"
@@ -38,6 +38,8 @@
 #include "util/output.h"
 #include "util/exception.h"
 #include "util/language.h"
+#include "util/utility.h"
+#include "util/hash.h"
 
 namespace CVC4 {
 
@@ -156,6 +158,16 @@ namespace kind {
 template <bool ref_count>
 class NodeTemplate {
 
+  // for hash_maps, hash_sets..
+  template <bool ref_count1>
+  struct HashFunction {
+    size_t operator()(CVC4::NodeTemplate<ref_count1> node) const {
+      return (size_t) node.getId();
+    }
+  };/* struct HashFunction */
+
+  typedef HashFunction<false> TNodeHashFunction;
+
   /**
    * The NodeValue has access to the private constructors, so that the
    * iterators can can create new nodes.
@@ -209,6 +221,30 @@ class NodeTemplate {
     }
   }
 
+  /**
+   * Cache-aware, recursive version of substitute() used by the public
+   * member function with a similar signature.
+   */
+  Node substitute(TNode node, TNode replacement,
+                  std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+
+  /**
+   * Cache-aware, recursive version of substitute() used by the public
+   * member function with a similar signature.
+   */
+  template <class Iterator1, class Iterator2>
+  Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd,
+                  Iterator2 replacementsBegin, Iterator2 replacementsEnd,
+                  std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+
+  /**
+   * Cache-aware, recursive version of substitute() used by the public
+   * member function with a similar signature.
+   */
+  template <class Iterator>
+  Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd,
+                  std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
+
 public:
 
   /** Default constructor, makes a null expression. */
@@ -444,7 +480,7 @@ public:
    * type checking is not requested, getType() will do the minimum
    * amount of checking required to return a valid result.
    *
-   * @param check whether we should check the type as we compute it 
+   * @param check whether we should check the type as we compute it
    * (default: false)
    */
   TypeNode getType(bool check = false) const
@@ -456,7 +492,9 @@ public:
   Node substitute(TNode node, TNode replacement) const;
 
   /**
-   * Simultaneous substitution of Nodes.
+   * Simultaneous substitution of Nodes.  Elements in the Iterator1
+   * range will be replaced by their corresponding element in the
+   * Iterator2 range.  Both ranges should have the same size.
    */
   template <class Iterator1, class Iterator2>
   Node substitute(Iterator1 nodesBegin,
@@ -465,6 +503,14 @@ public:
                   Iterator2 replacementsEnd) const;
 
   /**
+   * Simultaneous substitution of Nodes.  Iterators should be over
+   * pairs (x,y) for the rewrites [x->y].
+   */
+  template <class Iterator>
+  Node substitute(Iterator substitutionsBegin,
+                  Iterator substitutionsEnd) const;
+
+  /**
    * Returns the kind of this node.
    * @return the kind
    */
@@ -1146,39 +1192,81 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const
 }
 
 template <bool ref_count>
-Node NodeTemplate<ref_count>::substitute(TNode node,
-                                         TNode replacement) const {
+inline Node
+NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
+  std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+  return substitute(node, replacement, cache);
+}
+
+template <bool ref_count>
+Node
+NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
+                                    std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+  // in cache?
+  typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  if(i != cache.end()) {
+    return (*i).second;
+  }
+
+  // otherwise compute
   NodeBuilder<> nb(getKind());
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     // push the operator
     nb << getOperator();
   }
-  for(TNode::const_iterator i = begin(),
+  for(const_iterator i = begin(),
         iend = end();
       i != iend;
       ++i) {
     if(*i == node) {
       nb << replacement;
     } else {
-      (*i).substitute(node, replacement);
+      (*i).substitute(node, replacement, cache);
     }
   }
+
+  // put in cache
   Node n = nb;
+  cache[*this] = n;
   return n;
 }
 
 template <bool ref_count>
 template <class Iterator1, class Iterator2>
-Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
-                                         Iterator1 nodesEnd,
-                                         Iterator2 replacementsBegin,
-                                         Iterator2 replacementsEnd) const {
+inline Node
+NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
+                                    Iterator1 nodesEnd,
+                                    Iterator2 replacementsBegin,
+                                    Iterator2 replacementsEnd) const {
+  std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+  return substitute(nodesBegin, nodesEnd,
+                    replacementsBegin, replacementsEnd, cache);
+}
+
+template <bool ref_count>
+template <class Iterator1, class Iterator2>
+Node
+NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
+                                    Iterator1 nodesEnd,
+                                    Iterator2 replacementsBegin,
+                                    Iterator2 replacementsEnd,
+                                    std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+  // in cache?
+  typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  if(i != cache.end()) {
+    return (*i).second;
+  }
+
+  // otherwise compute
   Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin,
           "Substitution iterator ranges must be equal size" );
   Iterator1 j = find(nodesBegin, nodesEnd, *this);
   if(j != nodesEnd) {
-    return *(replacementsBegin + (j - nodesBegin));
+    Node n = *(replacementsBegin + (j - nodesBegin));
+    cache[*this] = n;
+    return n;
   } else if(getNumChildren() == 0) {
+    cache[*this] = *this;
     return *this;
   } else {
     NodeBuilder<> nb(getKind());
@@ -1186,14 +1274,65 @@ Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
       // push the operator
       nb << getOperator();
     }
-    for(TNode::const_iterator i = begin(),
+    for(const_iterator i = begin(),
           iend = end();
         i != iend;
         ++i) {
       nb << (*i).substitute(nodesBegin, nodesEnd,
-                            replacementsBegin, replacementsEnd);
+                            replacementsBegin, replacementsEnd,
+                            cache);
+    }
+    Node n = nb;
+    cache[*this] = n;
+    return n;
+  }
+}
+
+template <bool ref_count>
+template <class Iterator>
+inline Node
+NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
+                                    Iterator substitutionsEnd) const {
+  std::hash_map<TNode, TNode, TNodeHashFunction> cache;
+  return substitute(substitutionsBegin, substitutionsEnd, cache);
+}
+
+template <bool ref_count>
+template <class Iterator>
+Node
+NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
+                                    Iterator substitutionsEnd,
+                                    std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
+  // in cache?
+  typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
+  if(i != cache.end()) {
+    return (*i).second;
+  }
+
+  // otherwise compute
+  Iterator j = find_if(substitutionsBegin, substitutionsEnd,
+                       bind2nd(first_equal_to<typename Iterator::value_type::first_type, typename Iterator::value_type::second_type>(), *this));
+  if(j != substitutionsEnd) {
+    Node n = (*j).second;
+    cache[*this] = n;
+    return n;
+  } else if(getNumChildren() == 0) {
+    cache[*this] = *this;
+    return *this;
+  } else {
+    NodeBuilder<> nb(getKind());
+    if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+      // push the operator
+      nb << getOperator();
+    }
+    for(const_iterator i = begin(),
+          iend = end();
+        i != iend;
+        ++i) {
+      nb << (*i).substitute(substitutionsBegin, substitutionsEnd, cache);
     }
     Node n = nb;
+    cache[*this] = n;
     return n;
   }
 }
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 68655aed9..cc7e89bc8 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1244,7 +1244,7 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
      enabled and the current node isn't a variable or constant */
   if( d_nm->getOptions()->earlyTypeChecking ) {
     kind::MetaKind mk = n.getMetaKind();
-    if( mk != kind::metakind::VARIABLE 
+    if( mk != kind::metakind::VARIABLE
         && mk != kind::metakind::CONSTANT ) {
       d_nm->getType(n, true);
     }
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 7b0adaa95..a6ca39015 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -28,7 +28,15 @@ namespace CVC4 {
 TypeNode TypeNode::s_null( &expr::NodeValue::s_null );
 
 TypeNode TypeNode::substitute(const TypeNode& type,
-                              const TypeNode& replacement) const {
+                              const TypeNode& replacement,
+                              std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const {
+  // in cache?
+  std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+  if(i != cache.end()) {
+    return (*i).second;
+  }
+
+  // otherwise compute
   NodeBuilder<> nb(getKind());
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     // push the operator
@@ -44,7 +52,11 @@ TypeNode TypeNode::substitute(const TypeNode& type,
       (*i).substitute(type, replacement);
     }
   }
-  return nb.constructTypeNode();
+
+  // put in cache
+  TypeNode tn = nb.constructTypeNode();
+  cache[*this] = tn;
+  return tn;
 }
 
 Cardinality TypeNode::getCardinality() const {
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index b9fea939e..7f6ebd471 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -48,6 +48,17 @@ namespace expr {
  */
 class TypeNode {
 
+public:
+
+  // for hash_maps, hash_sets..
+  struct HashFunction {
+    size_t operator()(TypeNode node) const {
+      return (size_t) node.getId();
+    }
+  };/* struct HashFunction */
+
+private:
+
   /**
    * The NodeValue has access to the private constructors, so that the
    * iterators can can create new types.
@@ -79,6 +90,22 @@ class TypeNode {
    */
   void assignNodeValue(expr::NodeValue* ev);
 
+  /**
+   * Cache-aware, recursive version of substitute() used by the public
+   * member function with a similar signature.
+   */
+  TypeNode substitute(const TypeNode& type, const TypeNode& replacement,
+                      std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const;
+
+  /**
+   * Cache-aware, recursive version of substitute() used by the public
+   * member function with a similar signature.
+   */
+  template <class Iterator1, class Iterator2>
+  TypeNode substitute(Iterator1 typesBegin, Iterator1 typesEnd,
+                      Iterator2 replacementsBegin, Iterator2 replacementsEnd,
+                      std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const;
+
 public:
 
   /** Default constructor, makes a null expression. */
@@ -114,16 +141,16 @@ public:
   /**
    * Substitution of TypeNodes.
    */
-  TypeNode substitute(const TypeNode& type, const TypeNode& replacement) const;
+  inline TypeNode
+  substitute(const TypeNode& type, const TypeNode& replacement) const;
 
   /**
    * Simultaneous substitution of TypeNodes.
    */
   template <class Iterator1, class Iterator2>
-  TypeNode substitute(Iterator1 typesBegin,
-                      Iterator1 typesEnd,
-                      Iterator2 replacementsBegin,
-                      Iterator2 replacementsEnd) const;
+  inline TypeNode
+  substitute(Iterator1 typesBegin, Iterator1 typesEnd,
+             Iterator2 replacementsBegin, Iterator2 replacementsEnd) const;
 
   /**
    * Structural comparison operator for expressions.
@@ -504,12 +531,7 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
   return out;
 }
 
-// for hash_maps, hash_sets..
-struct TypeNodeHashFunction {
-  size_t operator()(TypeNode node) const {
-    return (size_t) node.getId();
-  }
-};/* struct TypeNodeHashFunction */
+typedef TypeNode::HashFunction TypeNodeHashFunction;
 
 }/* CVC4 namespace */
 
@@ -527,17 +549,46 @@ inline TypeNode TypeNode::fromType(const Type& t) {
   return NodeManager::fromType(t);
 }
 
+inline TypeNode
+TypeNode::substitute(const TypeNode& type,
+                     const TypeNode& replacement) const {
+  std::hash_map<TypeNode, TypeNode, HashFunction> cache;
+  return substitute(type, replacement, cache);
+}
+
+template <class Iterator1, class Iterator2>
+inline TypeNode
+TypeNode::substitute(Iterator1 typesBegin,
+                     Iterator1 typesEnd,
+                     Iterator2 replacementsBegin,
+                     Iterator2 replacementsEnd) const {
+  std::hash_map<TypeNode, TypeNode, HashFunction> cache;
+  return substitute(typesBegin, typesEnd,
+                    replacementsBegin, replacementsEnd, cache);
+}
+
 template <class Iterator1, class Iterator2>
 TypeNode TypeNode::substitute(Iterator1 typesBegin,
                               Iterator1 typesEnd,
                               Iterator2 replacementsBegin,
-                              Iterator2 replacementsEnd) const {
+                              Iterator2 replacementsEnd,
+                              std::hash_map<TypeNode, TypeNode, HashFunction>& cache) const {
+  // in cache?
+  std::hash_map<TypeNode, TypeNode, HashFunction>::const_iterator i = cache.find(*this);
+  if(i != cache.end()) {
+    return (*i).second;
+  }
+
+  // otherwise compute
   Assert( typesEnd - typesBegin == replacementsEnd - replacementsBegin,
           "Substitution iterator ranges must be equal size" );
   Iterator1 j = find(typesBegin, typesEnd, *this);
   if(j != typesEnd) {
-    return *(replacementsBegin + (j - typesBegin));
+    TypeNode tn = *(replacementsBegin + (j - typesBegin));
+    cache[*this] = tn;
+    return tn;
   } else if(getNumChildren() == 0) {
+    cache[*this] = *this;
     return *this;
   } else {
     NodeBuilder<> nb(getKind());
@@ -550,9 +601,11 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin,
         i != iend;
         ++i) {
       nb << (*i).substitute(typesBegin, typesEnd,
-                            replacementsBegin, replacementsEnd);
+                            replacementsBegin, replacementsEnd, cache);
     }
-    return nb.constructTypeNode();
+    TypeNode tn = nb.constructTypeNode();
+    cache[*this] = tn;
+    return tn;
   }
 }