Optimizations for datatypes theory. There seems to be a bug in trans_closure, currently implemented a work around.

4 files changed, 36 insertions, 17 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 96e8692f5..8db91da69 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -107,6 +107,7 @@ void Datatype::resolve(ExprManager* em,
     Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
   }
   d_self = self;
+  //d_card = getCardinality();
 }
 
 void Datatype::addConstructor(const DatatypeConstructor& c) {
@@ -125,6 +126,10 @@ Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
     c += (*i).getCardinality();
   }
+  //if( d_card!=c ){
+    //std::cout << "Bad card " << std::endl;
+  //}
+
   return c;
 }
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index c46c10c97..01558fd30 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -404,6 +404,7 @@ private:
   std::vector<DatatypeConstructor> d_constructors;
   bool d_resolved;
   Type d_self;
+  Cardinality d_card;
 
   /**
    * Datatypes refer to themselves, recursively, and we have a
@@ -616,7 +617,8 @@ inline Datatype::Datatype(std::string name) :
   d_params(),
   d_constructors(),
   d_resolved(false),
-  d_self() {
+  d_self(),
+  d_card(1) {
 }
 
 inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
@@ -624,7 +626,8 @@ inline Datatype::Datatype(std::string name, const std::vector<Type>& params) :
   d_params(params),
   d_constructors(),
   d_resolved(false),
-  d_self() {
+  d_self(),
+  d_card(1) {
 }
 
 inline std::string Datatype::getName() const throw() {
diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp
index 90b069485..970d2542e 100644
--- a/src/util/trans_closure.cpp
+++ b/src/util/trans_closure.cpp
@@ -37,16 +37,22 @@ TransitiveClosure::~TransitiveClosure() {
 
 bool TransitiveClosure::addEdge(unsigned i, unsigned j)
 {
+  Debug("trans-closure") << "Add edge " << i << " -> " << j << std::endl;
   // Check for loops
   Assert(i != j, "Cannot add self-loop");
-  if (adjMatrix.size() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) {
+  if (adjIndex.get() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) {
     return true;
   }
 
   // Grow matrix if necessary
   unsigned maxSize = ((i > j) ? i : j) + 1;
-  while (maxSize > adjMatrix.size()) {
-    adjMatrix.push_back(NULL);
+  while (maxSize > adjIndex.get()) {
+    if( maxSize > adjMatrix.size() ){
+      adjMatrix.push_back(NULL);
+    }else if( adjMatrix[adjIndex.get()]!=NULL ){
+      adjMatrix[adjIndex.get()]->clear();
+    }
+    adjIndex.set( adjIndex.get() + 1 );
   }
 
   // Add edge from i to j and everything j can reach
@@ -60,7 +66,7 @@ bool TransitiveClosure::addEdge(unsigned i, unsigned j)
 
   // Add edges from everything that can reach i to j and everything that j can reach
   unsigned k;
-  for (k = 0; k < adjMatrix.size(); ++k) {
+  for (k = 0; k < adjIndex.get(); ++k) {
     if (adjMatrix[k] != NULL && adjMatrix[k]->read(i)) {
       adjMatrix[k]->write(j);
       if (adjMatrix[j] != NULL) {
@@ -74,7 +80,7 @@ bool TransitiveClosure::addEdge(unsigned i, unsigned j)
 
 bool TransitiveClosure::isConnected(unsigned i, unsigned j)
 {
-  if( i>=adjMatrix.size() || j>adjMatrix.size() ){
+  if( i>=adjIndex.get() || j>adjIndex.get() ){//adjMatrix.size() ){
     return false;
   }else{
     return adjMatrix[i] != NULL && adjMatrix[i]->read(j);
@@ -84,15 +90,15 @@ bool TransitiveClosure::isConnected(unsigned i, unsigned j)
 void TransitiveClosure::debugPrintMatrix()
 {
   unsigned i,j;
-  for (i = 0; i < adjMatrix.size(); ++i) {
-    for (j = 0; j < adjMatrix.size(); ++j) {
+  for (i = 0; i < adjIndex.get(); ++i) {
+    for (j = 0; j < adjIndex.get(); ++j) {
       if (adjMatrix[i] != NULL && adjMatrix[i]->read(j)) {
         Debug("trans-closure") << "1 ";
       }
       else Debug("trans-closure") << "0 ";
     }
     Debug("trans-closure") << endl;
-  }      
+  }
 }
 
 unsigned TransitiveClosureNode::getId( Node i ){
@@ -108,10 +114,14 @@ unsigned TransitiveClosureNode::getId( Node i ){
 
 void TransitiveClosureNode::debugPrint(){
   for( int i=0; i<(int)currEdges.size(); i++ ){
-    Debug("trans-closure") << "currEdges[ " << i << " ] = " 
+    Debug("trans-closure") << "currEdges[ " << i << " ] = "
                            << currEdges[i].first << " -> " << currEdges[i].second;
+    int id1 = getId( currEdges[i].first );
+    int id2 = getId( currEdges[i].second );
+    Debug("trans-closure") << " { " << id1 << " -> " << id2 << " } ";
     Debug("trans-closure") << std::endl;
   }
+  debugPrintMatrix();
 }
 
 
diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h
index ce846637d..14e7ab95f 100644
--- a/src/util/trans_closure.h
+++ b/src/util/trans_closure.h
@@ -57,17 +57,17 @@ protected:
   CDBV* next() { return d_next; }
 
 public:
-  CDBV(context::Context* context) : 
+  CDBV(context::Context* context) :
     ContextObj(context), d_data(0), d_next(NULL)
   {}
 
-  ~CDBV() { 
+  ~CDBV() {
     if (d_next != NULL) {
       d_next->deleteSelf();
     }
     destroy();
   }
-
+  void clear() { d_data = 0; if( d_next ) d_next->clear(); }
   bool read(unsigned index) {
     if (index < 64) return (d_data & (uint64_t(1) << index)) != 0;
     else if (d_next == NULL) return false;
@@ -88,7 +88,7 @@ public:
       makeCurrent();
       d_next = new(true) CDBV(getContext());
       d_next->write(index - 64);
-    }      
+    }
   }
 
   void merge(CDBV* pcdbv) {
@@ -108,9 +108,10 @@ public:
 class TransitiveClosure {
   context::Context* d_context;
   std::vector<CDBV* > adjMatrix;
+  context::CDO<unsigned> adjIndex;
 
 public:
-  TransitiveClosure(context::Context* context) : d_context(context) {}
+  TransitiveClosure(context::Context* context) : d_context(context), adjIndex(context,0) {}
   virtual ~TransitiveClosure();
 
   /* Add an edge from node i to node j.  Return false if successful, true if this edge would create a cycle */
@@ -130,7 +131,7 @@ class TransitiveClosureNode : public TransitiveClosure{
   //for debugging
   context::CDList< std::pair< Node, Node > > currEdges;
 public:
-  TransitiveClosureNode(context::Context* context) : 
+  TransitiveClosureNode(context::Context* context) :
     TransitiveClosure(context), d_counter( context, 0 ), nodeMap( context ), currEdges(context) {}
   ~TransitiveClosureNode(){}