Substantial Changes:

-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default.  This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.

- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.

- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.

- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.

- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.

Minor Changes:

- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.

- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.

-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.

- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)

9 files changed, 108 insertions, 11 deletions

diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 92a21546c..056e68c69 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -26,6 +26,19 @@ namespace CVC4 {
 namespace expr {
 namespace attr {
 
+AttributeManager::AttributeManager(context::Context* ctxt) :
+  d_cdbools(ctxt),
+  d_cdints(ctxt),
+  d_cdtnodes(ctxt),
+  d_cdnodes(ctxt),
+  d_cdstrings(ctxt),
+  d_cdptrs(ctxt),
+  d_inGarbageCollection(false)
+{}
+
+bool AttributeManager::inGarbageCollection() const {
+  return d_inGarbageCollection;
+}
 
 void AttributeManager::debugHook(int debugFlag) {
   /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS!
@@ -36,6 +49,7 @@ void AttributeManager::debugHook(int debugFlag) {
 }
 
 void AttributeManager::deleteAllAttributes(NodeValue* nv) {
+  Assert(!inGarbageCollection());
   d_bools.erase(nv);
   deleteFromTable(d_ints, nv);
   deleteFromTable(d_tnodes, nv);
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 605427190..1e3f25461 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -101,17 +101,14 @@ class AttributeManager {
   template <class T, bool context_dep>
   friend struct getTable;
 
+  bool d_inGarbageCollection;
+
+  void clearDeleteAllAttributesBuffer();
+
 public:
 
   /** Construct an attribute manager. */
-  AttributeManager(context::Context* ctxt) :
-    d_cdbools(ctxt),
-    d_cdints(ctxt),
-    d_cdtnodes(ctxt),
-    d_cdnodes(ctxt),
-    d_cdstrings(ctxt),
-    d_cdptrs(ctxt) {
-  }
+  AttributeManager(context::Context* ctxt);
 
   /**
    * Get a particular attribute on a particular node.
@@ -177,6 +174,10 @@ public:
    */
   void deleteAllAttributes();
 
+  /**
+   * Returns true if a table is currently being deleted.
+   */
+  bool inGarbageCollection() const ;
 
   /**
    * Determines the AttrTableId of an attribute.
@@ -563,6 +564,8 @@ AttributeManager::setAttribute(NodeValue* nv,
 /**
  * Search for the NodeValue in all attribute tables and remove it,
  * calling the cleanup function if one is defined.
+ *
+ * This cannot use nv as anything other than a pointer!
  */
 template <class T>
 inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
@@ -600,6 +603,9 @@ inline void AttributeManager::deleteFromTable(CDAttrHash<T>& table,
  */
 template <class T>
 inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
+  Assert(!d_inGarbageCollection);
+  d_inGarbageCollection = true;
+
   bool anyRequireClearing = false;
   typedef AttributeTraits<T, false> traits_t;
   typedef AttrHash<T> hash_t;
@@ -627,6 +633,8 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
     }
   }
   table.clear();
+  d_inGarbageCollection = false;
+  Assert(!d_inGarbageCollection);
 }
 
 template <class AttrKind>
@@ -639,6 +647,7 @@ AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){
 
 template <class T>
 void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){
+  d_inGarbageCollection = true;
   typedef AttributeTraits<T, false> traits_t;
   typedef AttrHash<T> hash_t;
 
@@ -664,6 +673,7 @@ void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::
       ++it;
     }
   }
+  d_inGarbageCollection = false;
   static const size_t ReconstructShrinkRatio = 8;
   if(initialSize/ReconstructShrinkRatio > table.size()){
     reconstructTable(table);
@@ -672,10 +682,12 @@ void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::
 
 template <class T>
 void AttributeManager::reconstructTable(AttrHash<T>& table){
+  d_inGarbageCollection = true;
   typedef AttrHash<T> hash_t;
   hash_t cpy;
   cpy.insert(table.begin(), table.end());
   cpy.swap(table);
+  d_inGarbageCollection = false;
 }
 
 
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 8c94db3cc..9e7a2596f 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -65,6 +65,7 @@ exportConstant_cases=
 
 typerules=
 construles=
+neverconstrules=
 
 seen_theory=false
 seen_theory_builtin=false
@@ -168,6 +169,12 @@ function construle {
 #line $lineno \"$kf\"
     return $2::computeIsConst(nodeManager, n);
 "
+  neverconstrules="${neverconstrules}
+#line $lineno \"$kf\"
+  case kind::$1:
+#line $lineno \"$kf\"
+    return false;
+"
 }
 
 function sort {
@@ -294,6 +301,7 @@ for var in \
     typechecker_includes \
     typerules \
     construles \
+    neverconstrules \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index b1614f31b..39bbfbc2e 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -73,6 +73,10 @@ bool NodeTemplate<ref_count>::isConst() const {
     Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
     return false;
   default:
+    if(expr::TypeChecker::neverIsConst(NodeManager::currentNM(), *this)){
+      Debug("isConst") << "Node::isConst() returning false, the kind is never const" << std::endl;
+      return false;
+    }
     if(getAttribute(IsConstComputedAttr())) {
       bool bval = getAttribute(IsConstAttr());
       Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index cede6ff1f..9c76a41f3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -134,6 +134,7 @@ NodeManager::~NodeManager() {
     d_operators[i] = Node::null();
   }
 
+  Assert(!d_attrManager->inGarbageCollection() );
   while(!d_zombies.empty()) {
     reclaimZombies();
   }
@@ -161,6 +162,7 @@ NodeManager::~NodeManager() {
 
 void NodeManager::reclaimZombies() {
   // FIXME multithreading
+  Assert(!d_attrManager->inGarbageCollection());
 
   Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n";
 
@@ -435,6 +437,23 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
   return dtt;
 }
 
+void NodeManager::reclaimAllZombies(){
+  reclaimZombiesUntil(0u);
+}
+
+/** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
+void NodeManager::reclaimZombiesUntil(uint32_t k){
+  if(safeToReclaimZombies()){
+    while(poolSize() >= k && !d_zombies.empty()){
+      reclaimZombies();
+    }
+  }
+}
+
+size_t NodeManager::poolSize() const{
+  return d_nodeValuePool.size();
+}
+
 TypeNode NodeManager::mkSort(uint32_t flags) {
   NodeBuilder<1> nb(this, kind::SORT_TYPE);
   Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
@@ -586,6 +605,11 @@ Node NodeManager::mkAbstractValue(const TypeNode& type) {
   return n;
 }
 
+bool NodeManager::safeToReclaimZombies() const{
+  // FIXME multithreading
+  return !d_inReclaimZombies && !d_attrManager->inGarbageCollection();
+}
+
 void NodeManager::deleteAttributes(const std::vector<const expr::attr::AttributeUniqueId*>& ids){
   d_attrManager->deleteAttributes(ids);
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 32c492003..af771bd89 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -229,8 +229,7 @@ class NodeManager {
     }
     d_zombies.insert(nv);// FIXME multithreading
 
-    if(!d_inReclaimZombies) {// FIXME multithreading
-      // for now, collect eagerly.  can add heuristic here later..
+    if(safeToReclaimZombies()) {
       if(d_zombies.size() > 5000) {
         reclaimZombies();
       }
@@ -243,6 +242,11 @@ class NodeManager {
   void reclaimZombies();
 
   /**
+   * It is safe to collect zombies.
+   */
+  bool safeToReclaimZombies() const;
+
+  /**
    * This template gives a mechanism to stack-allocate a NodeValue
    * with enough space for N children (where N is a compile-time
    * constant).  You use it like this:
@@ -860,6 +864,15 @@ public:
    */
   static inline TypeNode fromType(Type t);
 
+  /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
+  void reclaimZombiesUntil(uint32_t k);
+
+  /** Reclaims all zombies (if possible).*/
+  void reclaimAllZombies();
+
+  /** Size of the node pool. */
+  size_t poolSize() const;
+
   /** Deletes a list of attributes from the NM's AttributeManager.*/
   void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
 
@@ -871,7 +884,6 @@ public:
    * any published code!
    */
   void debugHook(int debugFlag);
-
 };/* class NodeManager */
 
 /**
diff --git a/src/expr/options b/src/expr/options
index 223189d1b..cf893a7a5 100644
--- a/src/expr/options
+++ b/src/expr/options
@@ -21,5 +21,8 @@ option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :defaul
 option typeChecking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking
  never type check expressions
 
+option biasedITERemoval --biased-ites bool :default false
+ try the new remove ite pass that is biased against term ites appearing
+
 endmodule
 
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index ac461bb7b..d34a7c7d6 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -34,6 +34,9 @@ public:
   static bool computeIsConst(NodeManager* nodeManager, TNode n)
     throw (AssertionException);
 
+  static bool neverIsConst(NodeManager* nodeManager, TNode n)
+    throw (AssertionException);
+
 };/* class TypeChecker */
 
 }/* CVC4::expr namespace */
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index b2138c9a1..4e476f4d9 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -78,5 +78,22 @@ ${construles}
 
 }/* TypeChecker::computeIsConst */
 
+bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n)
+  throw (AssertionException) {
+
+  Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
+
+  switch(n.getKind()) {
+${neverconstrules}
+
+#line 90 "${template}"
+
+  default:;
+  }
+
+  return true;
+
+}/* TypeChecker::neverIsConst */
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */