Adding static_fact_manager

2 files changed, 291 insertions, 0 deletions

diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp
new file mode 100644
index 000000000..1e135514a
--- /dev/null
+++ b/src/theory/arrays/static_fact_manager.cpp
@@ -0,0 +1,172 @@
+/*********************                                                        */
+/*! \file static_fact_manager.cpp
+ ** \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 <iostream>
+
+#include "theory/arrays/static_fact_manager.h"
+#include "util/Assert.h"
+#include "expr/node.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+bool StaticFactManager::areEq(TNode a, TNode b) {
+  return (find(a) == find(b));
+}
+
+bool StaticFactManager::areDiseq(TNode a, TNode b) {
+  Node af = find(a);
+  Node bf = find(b);
+  Node left, right;
+  unsigned i;
+  for (i = 0; i < d_diseq.size(); ++i) {
+    left = find(d_diseq[i][0]);
+    right = find(d_diseq[i][1]);
+    if ((left == af && right == bf) ||
+        (left == bf && right == af)) {
+      return true;
+    }
+  }
+  return false;
+}
+
+void StaticFactManager::addDiseq(TNode eq) {
+  Assert(eq.getKind() == kind::EQUAL);
+  d_diseq.push_back(eq);
+}
+
+void StaticFactManager::addEq(TNode eq) {
+  Assert(eq.getKind() == kind::EQUAL);
+  Node a = find(eq[0]);
+  Node b = find(eq[1]);
+
+  if( a == b) {
+    return;
+  }
+
+  /*
+   * take care of the congruence closure part
+   */
+
+  // make "a" the one with shorter diseqList
+  // CNodeTNodesMap::iterator deq_ia = d_disequalities.find(a);
+  // CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
+
+  // if(deq_ia != d_disequalities.end()) {
+  //   if(deq_ib == d_disequalities.end() ||
+  //      (*deq_ia).second->size() > (*deq_ib).second->size()) {
+  //     TNode tmp = a;
+  //     a = b;
+  //     b = tmp;
+  //   }
+  // }
+  // a = find(a);
+  // b = find(b);
+
+
+  // b becomes the canon of a
+  setCanon(a, b);
+
+  // deq_ia = d_disequalities.find(a);
+  // map<TNode, TNode> alreadyDiseqs;
+  // if(deq_ia != d_disequalities.end()) {
+  //   /*
+  //    * Collecting the disequalities of b, no need to check for conflicts
+  //    * since the representative of b does not change and we check all the things
+  //    * in a's class when we look at the diseq list of find(a)
+  //    */
+
+  //   CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
+  //   if(deq_ib != d_disequalities.end()) {
+  //     CTNodeListAlloc* deq = (*deq_ib).second;
+  //     for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end(); j++) {
+  //       TNode deqn = *j;
+  //       TNode s = deqn[0];
+  //       TNode t = deqn[1];
+  //       TNode sp = find(s);
+  //       TNode tp = find(t);
+  //       Assert(sp == b || tp == b);
+  //       if(sp == b) {
+  //         alreadyDiseqs[tp] = deqn;
+  //       } else {
+  //         alreadyDiseqs[sp] = deqn;
+  //       }
+  //     }
+  //   }
+
+  //   /*
+  //    * Looking for conflicts in the a disequality list. Note
+  //    * that at this point a and b are already merged. Also has
+  //    * the side effect that it adds them to the list of b (which
+  //    * became the canonical representative)
+  //    */
+
+  //   CTNodeListAlloc* deqa = (*deq_ia).second;
+  //   for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end(); i++) {
+  //     TNode deqn = (*i);
+  //     Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF);
+  //     TNode s = deqn[0];
+  //     TNode t = deqn[1];
+  //     TNode sp = find(s);
+  //     TNode tp = find(t);
+
+  //     if(find(s) == find(t)) {
+  //       d_conflict = deqn;
+  //       return;
+  //     }
+  //     Assert( sp == b || tp == b);
+
+  //     // make sure not to add duplicates
+
+  //     if(sp == b) {
+  //       if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
+  //         appendToDiseqList(b, deqn);
+  //         alreadyDiseqs[tp] = deqn;
+  //       }
+  //     } else {
+  //       if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
+  //         appendToDiseqList(b, deqn);
+  //         alreadyDiseqs[sp] = deqn;
+  //       }
+  //     }
+
+  //   }
+  // }
+
+  // // TODO: check for equality propagations
+  // // a and b are find(a) and find(b) here
+  // checkPropagations(a,b);
+
+  // if(a.getType().isArray()) {
+  //   checkRowLemmas(a,b);
+  //   checkRowLemmas(b,a);
+  //   // note the change in order, merge info adds the list of
+  //   // the 2nd argument to the first
+  //   d_infoMap.mergeInfo(b, a);
+  // }
+}
+
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
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 */