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

2 files changed, 33 insertions, 1 deletions

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 */