Adding static_fact_manager

1 files changed, 119 insertions, 0 deletions

diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h
new file mode 100644
index 000000000..d2dfc5f2d
--- /dev/null
+++ b/src/theory/arrays/static_fact_manager.h
@@ -0,0 +1,119 @@
+/*********************                                                        */
+/*! \file static_fact_manager.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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 Path-compressing, backtrackable union-find using an undo
+ ** stack. Refactored from the UF union-find.
+ **
+ ** Path-compressing, backtrackable union-find using an undo stack
+ ** rather than storing items in a CDMap<>.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
+#define __CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
+
+#include <utility>
+#include <vector>
+#include <ext/hash_map>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+  class StaticFactManager {
+  /** Our underlying map type. */
+  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> MapType;
+
+  /**
+   * Our map of Nodes to their canonical representatives.
+   * If a Node is not present in the map, it is its own
+   * representative.
+   */
+  MapType d_map;
+  std::vector<Node> d_diseq;
+
+public:
+  StaticFactManager() {}
+  ~StaticFactManager() throw() { }
+
+  /**
+   * Return a Node's union-find representative, doing path compression.
+   */
+  inline TNode find(TNode n);
+
+  /**
+   * Return a Node's union-find representative, NOT doing path compression.
+   * This is useful for Assert() statements, debug checking, and similar
+   * things that you do NOT want to mutate the structure.
+   */
+  inline TNode debugFind(TNode n) const;
+
+  /**
+   * Set the canonical representative of n to newParent.  They should BOTH
+   * be their own canonical representatives on entry to this funciton.
+   */
+  inline void setCanon(TNode n, TNode newParent);
+
+  bool areEq(TNode a, TNode b);
+  bool areDiseq(TNode a, TNode b);
+  void addDiseq(TNode eq);
+  void addEq(TNode eq);
+
+};/* class StaticFactManager<> */
+
+inline TNode StaticFactManager::debugFind(TNode n) const {
+  typename MapType::const_iterator i = d_map.find(n);
+  if(i == d_map.end()) {
+    return n;
+  } else {
+    return debugFind((*i).second);
+  }
+}
+
+inline TNode StaticFactManager::find(TNode n) {
+  Trace("arraysuf") << "arraysUF find of " << n << std::endl;
+  typename MapType::iterator i = d_map.find(n);
+  if(i == d_map.end()) {
+    Trace("arraysuf") << "arraysUF   it is rep" << std::endl;
+    return n;
+  } else {
+    Trace("arraysuf") << "arraysUF   not rep: par is " << (*i).second << std::endl;
+    std::pair<TNode, TNode> pr = *i;
+    // our iterator is invalidated by the recursive call to find(),
+    // since it mutates the map
+    TNode p = find(pr.second);
+    if(p == pr.second) {
+      return p;
+    }
+    pr.second = p;
+    d_map.insert(pr);
+    return p;
+  }
+}
+
+inline void StaticFactManager::setCanon(TNode n, TNode newParent) {
+  Assert(d_map.find(n) == d_map.end());
+  Assert(d_map.find(newParent) == d_map.end());
+  if(n != newParent) {
+    d_map[n] = newParent;
+  }
+}
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /*__CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */