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

diff --git a/src/util/nary_builder.cpp b/src/util/nary_builder.cpp
new file mode 100644
index 000000000..004dd3382
--- /dev/null
+++ b/src/util/nary_builder.cpp
@@ -0,0 +1,183 @@
+
+#include "util/nary_builder.h"
+#include "expr/metakind.h"
+using namespace std;
+
+namespace CVC4 {
+namespace util {
+
+Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children){
+  if(children.size() == 0){
+    return zeroArity(kind);
+  }else if(children.size() == 1){
+    return children[0];
+  }else{
+    const unsigned int max = kind::metakind::getUpperBoundForKind(kind);
+    const unsigned int min = kind::metakind::getLowerBoundForKind(kind);
+
+    Assert(min <= children.size());
+
+    unsigned int numChildren = children.size();
+    NodeManager* nm = NodeManager::currentNM();
+    if( numChildren <= max ) {
+      return nm->mkNode(kind,children);
+    }
+
+    typedef std::vector<Node>::const_iterator const_iterator;
+    const_iterator it = children.begin() ;
+    const_iterator end = children.end() ;
+
+    /* The new top-level children and the children of each sub node */
+    std::vector<Node> newChildren;
+    std::vector<Node> subChildren;
+
+    while( it != end && numChildren > max ) {
+      /* Grab the next max children and make a node for them. */
+      for(const_iterator next = it + max; it != next; ++it, --numChildren ) {
+        subChildren.push_back(*it);
+      }
+      Node subNode = nm->mkNode(kind,subChildren);
+      newChildren.push_back(subNode);
+      subChildren.clear();
+    }
+
+    /* If there's children left, "top off" the Expr. */
+    if(numChildren > 0) {
+      /* If the leftovers are too few, just copy them into newChildren;
+       * otherwise make a new sub-node  */
+      if(numChildren < min) {
+        for(; it != end; ++it) {
+          newChildren.push_back(*it);
+        }
+      } else {
+        for(; it != end; ++it) {
+          subChildren.push_back(*it);
+        }
+        Node subNode = nm->mkNode(kind, subChildren);
+        newChildren.push_back(subNode);
+      }
+    }
+
+    /* It's inconceivable we could have enough children for this to fail
+     * (more than 2^32, in most cases?). */
+    AlwaysAssert( newChildren.size() <= max,
+                  "Too many new children in mkAssociative" );
+
+    /* It would be really weird if this happened (it would require
+     * min > 2, for one thing), but let's make sure. */
+    AlwaysAssert( newChildren.size() >= min,
+                  "Too few new children in mkAssociative" );
+
+    return nm->mkNode(kind,newChildren);
+  }
+}
+
+Node NaryBuilder::zeroArity(Kind k){
+  using namespace kind;
+  NodeManager* nm = NodeManager::currentNM();
+  switch(k){
+  case AND:
+    return nm->mkConst(true);
+  case OR:
+    return nm->mkConst(false);
+  case PLUS:
+    return nm->mkConst(Rational(0));
+  case MULT:
+    return nm->mkConst(Rational(1));
+  default:
+    return Node::null();
+  }
+}
+
+
+RePairAssocCommutativeOperators::RePairAssocCommutativeOperators()
+  : d_cache()
+{}
+RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){}
+size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); }
+void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); }
+
+bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){
+  using namespace kind;
+  switch(k){
+  case BITVECTOR_CONCAT:
+  case BITVECTOR_AND:
+  case BITVECTOR_OR:
+  case BITVECTOR_XOR:
+  case BITVECTOR_MULT:
+  case BITVECTOR_PLUS:
+  case DISTINCT:
+  case PLUS:
+  case MULT:
+  case AND:
+  case OR:
+    return true;
+  default:
+    return false;
+  }
+}
+
+Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){
+  if(d_cache.find(n) != d_cache.end()){
+    return d_cache[n];
+  }
+  Node result =
+    isAssociateCommutative(n.getKind()) ?
+    case_assoccomm(n) : case_other(n);
+
+  d_cache[n] = result;
+  return result;
+}
+
+Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){
+  Kind k = n.getKind();
+  Assert(isAssociateCommutative(k));
+  Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
+  unsigned N = n.getNumChildren();
+  Assert(N >= 2);
+
+
+  Node last = rePairAssocCommutativeOperators( n[N-1]);
+  Node nextToLast = rePairAssocCommutativeOperators(n[N-2]);
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node last2 = nm->mkNode(k, nextToLast, last);
+
+  if(N <= 2){
+    return last2;
+  } else{
+    Assert(N > 2);
+    Node prevRound = last2;
+    for(unsigned prevPos = N-2; prevPos > 0; --prevPos){
+      unsigned currPos = prevPos-1;
+      Node curr = rePairAssocCommutativeOperators(n[currPos]);
+      Node round = nm->mkNode(k, curr, prevRound);
+      prevRound = round;
+    }
+    return prevRound;
+  }
+}
+
+Node RePairAssocCommutativeOperators::case_other(TNode n){
+  if(n.isConst() || n.isVar()){
+    return n;
+  }
+
+  NodeBuilder<> nb(n.getKind());
+
+  if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    nb << n.getOperator();
+  }
+
+  // Remove the ITEs from the children
+  for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) {
+    Node newChild = rePairAssocCommutativeOperators(*i);
+    nb << newChild;
+  }
+
+  Node result = (Node)nb;
+  return result;
+}
+
+}/* util namespace */
+}/* CVC4 namespace */