Significant revision to theory/arith. The new draft has a lot of small bug fixes and organizational changes. The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.

1 files changed, 19 insertions, 7 deletions

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index f231b701c..619f60a6c 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -555,19 +555,31 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
  */
 template <class T>
 inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
+  bool anyRequireClearing = false;
+  typedef AttributeTraits<T, false> traits_t;
+  typedef AttrHash<T> hash_t;
   for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
-    typedef AttributeTraits<T, false> traits_t;
-    typedef AttrHash<T> hash_t;
     if(traits_t::cleanup[id] != NULL) {
-      typename hash_t::iterator it = table.begin();
-      typename hash_t::iterator it_end = table.end();
-      while (it != it_end) {
+      anyRequireClearing = true;
+    }
+  }
+
+  if(anyRequireClearing){
+    typename hash_t::iterator it = table.begin();
+    typename hash_t::iterator it_end = table.end();
+
+    while (it != it_end){
+      uint64_t id = (*it).first.first;
+      Debug("attrgc") << "id " << id
+                      << " node_value: " << ((*it).first.second)
+                      << std::endl;
+      if(traits_t::cleanup[id] != NULL) {
         traits_t::cleanup[id]((*it).second);
-        ++ it;
       }
+      ++it;
     }
-    table.clear();
   }
+  table.clear();
 }