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

diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h
deleted file mode 100644
index 07fa0dedb..000000000
--- a/src/theory/ite_simplifier.h
+++ /dev/null
@@ -1,165 +0,0 @@
-/*********************                                                        */
-/*! \file ite_simplifier.h
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Simplifications for ITE expressions
- **
- ** This module implements preprocessing phases designed to simplify ITE
- ** expressions.  Based on:
- ** Kim, Somenzi, Jin.  Efficient Term-ITE Conversion for SMT.  FMCAD 2009.
- ** Burch, Jerry.  Techniques for Verifying Superscalar Microprocessors.  DAC '96
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__ITE_SIMPLIFIER_H
-#define __CVC4__ITE_SIMPLIFIER_H
-
-#include <deque>
-#include <vector>
-#include <utility>
-
-#include "expr/node.h"
-#include "expr/command.h"
-#include "prop/prop_engine.h"
-#include "context/cdhashset.h"
-#include "theory/theory.h"
-#include "theory/rewriter.h"
-#include "theory/shared_terms_database.h"
-#include "theory/term_registration_visitor.h"
-#include "theory/valuation.h"
-#include "util/statistics_registry.h"
-#include "util/hash.h"
-#include "util/cache.h"
-#include "util/ite_removal.h"
-
-namespace CVC4 {
-namespace theory {
-
-class ITESimplifier {
-  Node d_true;
-  Node d_false;
-
-  std::hash_map<Node, bool, NodeHashFunction> d_containsTermITECache;
-  bool containsTermITE(TNode e);
-
-  std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache;
-  bool leavesAreConst(TNode e, theory::TheoryId tid);
-  bool leavesAreConst(TNode e)
-    { return leavesAreConst(e, theory::Theory::theoryOf(e)); }
-
-  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
-  typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
-
-  typedef std::pair<Node, Node> NodePair;
-  struct NodePairHashFunction {
-    size_t operator () (const NodePair& pair) const {
-      size_t hash = 0;
-      hash = 0x9e3779b9 + NodeHashFunction().operator()(pair.first);
-      hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2);
-      return hash;
-    }
-  };/* struct ITESimplifier::NodePairHashFunction */
-
-  typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap;
-
-
-  NodePairMap d_simpConstCache;
-  Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
-  std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
-  Node getSimpVar(TypeNode t);
-
-  NodeMap d_simpContextCache;
-  Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
-
-  Node simpITEAtom(TNode atom);
-
-  NodeMap d_simpITECache;
-
-public:
-  Node simpITE(TNode assertion);
-
-private:
-
-  class CareSetPtr;
-  class CareSetPtrVal {
-    friend class ITESimplifier::CareSetPtr;
-    ITESimplifier& d_iteSimplifier;
-    unsigned d_refCount;
-    std::set<Node> d_careSet;
-    CareSetPtrVal(ITESimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {}
-  };
-
-  std::vector<CareSetPtrVal*> d_usedSets;
-  void careSetPtrGC(CareSetPtrVal* val) {
-    d_usedSets.push_back(val);
-  }
-
-  class CareSetPtr {
-    CareSetPtrVal* d_val;
-    CareSetPtr(CareSetPtrVal* val) : d_val(val) {}
-  public:
-    CareSetPtr() : d_val(NULL) {}
-    CareSetPtr(const CareSetPtr& cs) {
-      d_val = cs.d_val;
-      if (d_val != NULL) {
-        ++(d_val->d_refCount);
-      }
-    }
-    ~CareSetPtr() {
-      if (d_val != NULL && (--(d_val->d_refCount) == 0)) {
-        d_val->d_iteSimplifier.careSetPtrGC(d_val);
-      }
-    }
-    CareSetPtr& operator=(const CareSetPtr& cs) {
-      if (d_val != cs.d_val) {
-        if (d_val != NULL && (--(d_val->d_refCount) == 0)) {
-          d_val->d_iteSimplifier.careSetPtrGC(d_val);
-        }
-        d_val = cs.d_val;
-        if (d_val != NULL) {
-          ++(d_val->d_refCount);
-        }
-      }
-      return *this;
-    }
-    std::set<Node>& getCareSet() { return d_val->d_careSet; }
-    static CareSetPtr mkNew(ITESimplifier& simp) {
-      CareSetPtrVal* val = new CareSetPtrVal(simp);
-      return CareSetPtr(val);
-    }
-    static CareSetPtr recycle(CareSetPtrVal* val) {
-      Assert(val != NULL && val->d_refCount == 0);
-      val->d_refCount = 1;
-      return CareSetPtr(val);
-    }
-  };
-
-  CareSetPtr getNewSet();
-
-  typedef std::map<TNode, CareSetPtr> CareMap;
-  void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet);
-  Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
-
-public:
-  Node simplifyWithCare(TNode e);
-
-  ITESimplifier() {
-    d_true = NodeManager::currentNM()->mkConst<bool>(true);
-    d_false = NodeManager::currentNM()->mkConst<bool>(false);
-  }
-  ~ITESimplifier() {}
-
-};
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif