1 files changed, 154 insertions, 0 deletions
diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h
new file mode 100644
index 000000000..8466c5444
--- /dev/null
+++ b/src/theory/ite_simplifier.h
@@ -0,0 +1,154 @@
+/*********************                                                        */
+/*! \file ite_simplifier.h
+ ** \verbatim
+ ** Original author: barrett
+ ** Major contributors: 
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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/substitutions.h"
+#include "theory/rewriter.h"
+#include "theory/substitutions.h"
+#include "theory/shared_terms_database.h"
+#include "theory/term_registration_visitor.h"
+#include "theory/valuation.h"
+#include "util/options.h"
+#include "util/stats.h"
+#include "util/hash.h"
+#include "util/cache.h"
+#include "util/ite_removal.h"
+
+namespace CVC4 {
+
+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;
+
+  NodeMap d_simpConstCache;
+  Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
+  Node d_simpVarInt;
+  Node d_simpVarReal;
+  Node getSimpVar(TypeNode t);
+  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() {}
+
+};
+
+}
+
+#endif