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

1 files changed, 21 insertions, 1 deletions

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