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, 13 insertions, 10 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 53ff4d167..e5b2ad8d2 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -37,12 +37,8 @@
 #include "options/options.h"
 #include "smt/options.h"
 #include "util/statistics_registry.h"
-#include "util/hash.h"
-#include "util/cache.h"
 #include "util/cvc4_assert.h"
 #include "util/sort_inference.h"
-#include "theory/ite_simplifier.h"
-#include "theory/unconstrained_simplifier.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/bv/bv_to_bool.h"
 #include "theory/atom_requests.h"
@@ -77,18 +73,19 @@ struct NodeTheoryPairHashFunction {
 
 
 
-
+/* Forward Declarations Block */
 namespace theory {
   class TheoryModel;
   class TheoryEngineModelBuilder;
+  class ITEUtilities;
 
   namespace eq {
     class EqualityEngine;
   }
 }/* CVC4::theory namespace */
-
-
 class DecisionEngine;
+class RemoveITE;
+class UnconstrainedSimplifier;
 
 /**
  * This is essentially an abstraction for a collection of theories.  A
@@ -771,11 +768,14 @@ private:
   /** Dump the assertions to the dump */
   void dumpAssertions(const char* tag);
 
-  /** For preprocessing pass simplifying ITEs */
-  theory::ITESimplifier d_iteSimplifier;
+  /**
+   * A collection of ite preprocessing passes.
+   */
+  theory::ITEUtilities* d_iteUtilities;
+
 
   /** For preprocessing pass simplifying unconstrained expressions */
-  UnconstrainedSimplifier d_unconstrainedSimp;
+  UnconstrainedSimplifier* d_unconstrainedSimp;
 
   /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
   theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; 
@@ -783,6 +783,9 @@ public:
 
   void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); 
   Node ppSimpITE(TNode assertion);
+  /** Returns false if an assertion simplified to false. */
+  bool donePPSimpITE(std::vector<Node>& assertions);
+
   void ppUnconstrainedSimp(std::vector<Node>& assertions);
 
   SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }