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

1 files changed, 20 insertions, 8 deletions

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;
 }