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, 38 insertions, 0 deletions

diff --git a/src/util/nary_builder.h b/src/util/nary_builder.h
new file mode 100644
index 000000000..ceaa44e77
--- /dev/null
+++ b/src/util/nary_builder.h
@@ -0,0 +1,38 @@
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4{
+namespace util {
+
+class NaryBuilder {
+public:
+  static Node mkAssoc(Kind k, const std::vector<Node>& children);
+  static Node zeroArity(Kind k);
+};/* class NaryBuilder */
+
+class RePairAssocCommutativeOperators {
+public:
+  RePairAssocCommutativeOperators();
+  ~RePairAssocCommutativeOperators();
+
+  Node rePairAssocCommutativeOperators(TNode n);
+
+  static bool isAssociateCommutative(Kind k);
+
+  size_t size() const;
+  void clear();
+private:
+  Node case_assoccomm(TNode n);
+  Node case_other(TNode n);
+
+  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  NodeMap d_cache;
+};/* class RePairAssocCommutativeOperators */
+
+}/* util namespace */
+}/* CVC4 namespace */