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, 56 insertions, 6 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 84bbbc179..93b3f0d7e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -35,6 +35,11 @@
 #include "util/node_visitor.h"
 #include "util/ite_removal.h"
 
+//#include "theory/ite_simplifier.h"
+//#include "theory/ite_compressor.h"
+#include "theory/ite_utilities.h"
+#include "theory/unconstrained_simplifier.h"
+
 #include "theory/model.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/theory_quantifiers.h"
@@ -122,7 +127,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms),
-  d_unconstrainedSimp(context, logicInfo),
+  d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)),
   d_bvToBoolPreprocessor()
 {
   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
@@ -140,7 +145,9 @@ TheoryEngine::TheoryEngine(context::Context* context,
   StatisticsRegistry::registerStat(&d_combineTheoriesTime);
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
-  PROOF (ProofManager::currentPM()->initTheoryProof(); ); 
+  PROOF (ProofManager::currentPM()->initTheoryProof(); );
+
+  d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
 }
 
 TheoryEngine::~TheoryEngine() {
@@ -161,6 +168,10 @@ TheoryEngine::~TheoryEngine() {
   delete d_masterEqualityEngine;
 
   StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
+
+  delete d_unconstrainedSimp;
+
+  delete d_iteUtilities;
 }
 
 void TheoryEngine::interrupt() throw(ModalException) {
@@ -1401,9 +1412,48 @@ void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<N
 
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
-  Node result = d_iteSimplifier.simpITE(assertion);
-  result = d_iteSimplifier.simplifyWithCare(Rewriter::rewrite(result));
-  result = Rewriter::rewrite(result);
+  if(!d_iteRemover.containsTermITE(assertion)){
+    return assertion;
+  }else{
+
+    Node result = d_iteUtilities->simpITE(assertion);
+    Node res_rewritten = Rewriter::rewrite(result);
+
+    if(options::simplifyWithCareEnabled()){
+      Chat() << "starting simplifyWithCare()" << endl;
+      Node postSimpWithCare = d_iteUtilities->simplifyWithCare(res_rewritten);
+      Chat() << "ending simplifyWithCare()"
+             << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
+      result = Rewriter::rewrite(postSimpWithCare);
+    }else{
+      result = res_rewritten;
+    }
+
+    return result;
+  }
+}
+
+bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
+  bool result = true;
+  if(d_iteUtilities->simpIteDidALotOfWorkHeuristic()){
+    if(options::compressItes()){
+      result = d_iteUtilities->compress(assertions);
+    }
+
+    if(result){
+      // if false, don't bother to reclaim memory here.
+      NodeManager* nm = NodeManager::currentNM();
+      if(nm->poolSize() >= options::zombieHuntThreshold()){
+        Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl;
+        Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
+        d_iteUtilities->clear();
+        Rewriter::garbageCollect();
+        d_iteRemover.garbageCollect();
+        nm->reclaimZombiesUntil(options::zombieHuntThreshold());
+        Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
+      }
+    }
+  }
   return result;
 }
 
@@ -1481,7 +1531,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
 
 void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
 {
-  d_unconstrainedSimp.processAssertions(assertions);
+  d_unconstrainedSimp->processAssertions(assertions);
 }