From c21ca8353370eb44aa6318e6ee4bffee64197fd8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 27 Apr 2011 00:49:02 +0000
Subject: cleaned up some of the hacks in the datatypes theory solver, working
 on using Transitive Closure to detect cycles, added rewrite rule for
 disinguished ground terms

---
 src/util/trans_closure.cpp | 12 ++++++++++++
 src/util/trans_closure.h   | 22 +++++++++++++++++++++-
 2 files changed, 33 insertions(+), 1 deletion(-)

(limited to 'src/util')

diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp
index 092dfb358..a31dc3378 100644
--- a/src/util/trans_closure.cpp
+++ b/src/util/trans_closure.cpp
@@ -89,5 +89,17 @@ void TransitiveClosure::debugPrintMatrix()
   }      
 }
 
+unsigned TransitiveClosureNode::d_counter = 0;
+
+unsigned TransitiveClosureNode::getId( Node i ){
+  std::map< Node, unsigned >::iterator it = nodeMap.find( i );
+  if( it==nodeMap.end() ){
+    nodeMap[i] = d_counter;
+    d_counter++;
+    return d_counter-1;
+  }
+  return it->second;
+}
+
 
 }/* CVC4 namespace */
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
index 56951d531..4d811d0c9 100644
--- a/src/util/trans_closure.h
+++ b/src/util/trans_closure.h
@@ -20,6 +20,8 @@
 #define __CVC4__UTIL__TRANSITIVE_CLOSURE_H
 
 #include "context/context.h"
+#include "expr/node.h"
+#include <map>
 
 namespace CVC4 {
 
@@ -105,13 +107,31 @@ class TransitiveClosure {
 
 public:
   TransitiveClosure(context::Context* context) : d_context(context) {}
-  ~TransitiveClosure();
+  virtual ~TransitiveClosure();
 
   /* Add an edge from node i to node j.  Return false if successful, true if this edge would create a cycle */
   bool addEdge(unsigned i, unsigned j);
   void debugPrintMatrix();
 };
 
+/**
+ * Transitive closure module for nodes in CVC4.
+ *
+ */
+class TransitiveClosureNode : public TransitiveClosure{
+  static unsigned d_counter;
+  std::map< Node, unsigned > nodeMap;
+  unsigned getId( Node i );
+public:
+  TransitiveClosureNode(context::Context* context) : TransitiveClosure(context) {}
+  ~TransitiveClosureNode(){}
+
+  /* Add an edge from node i to node j.  Return false if successful, true if this edge would create a cycle */
+  bool addEdgeNode(Node i, Node j) {
+    return addEdge( getId( i ), getId( j ) );
+  }
+};
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__UTIL__TRANSITIVE_CLOSURE_H */
-- 
cgit v1.2.3