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, 12 insertions, 0 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 */