stats.h

@@ -114,6 +114,7 @@ typedef enum {
     LDD_PROJECT_MINUS_CACHED,
     LDD_NODES_CREATED,
     LDD_NODES_REUSED,
+    LDD_FIRE_CACHED,
 
     LLMSSET_LOOKUP,
 

sylvan_int.h

@@ -80,6 +80,9 @@ static const uint64_t CACHE_MDD_RELPREV             = (27LL<<40);
 static const uint64_t CACHE_MDD_SATCOUNT            = (28LL<<40);
 static const uint64_t CACHE_MDD_SATCOUNTL1          = (29LL<<40);
 static const uint64_t CACHE_MDD_SATCOUNTL2          = (30LL<<40);
+static const uint64_t CACHE_LDD_FIRE                = (31LL<<40);
+static const uint64_t CACHE_LDD_UNION                = (32LL<<40);
+                        
 
 // MTBDD operations
 static const uint64_t CACHE_MTBDD_APPLY             = (40LL<<40);

sylvan_seq.c

@@ -37,8 +37,6 @@
 #include <string.h>
 
 
-
-
 /**
  * MDD node structure
  */
@@ -107,15 +105,10 @@ MDD ldd_makenode(uint32_t value, MDD ifeq, MDD ifneq)
     uint64_t index = llmsset_lookup(nodes, n.a, n.b, &created);
     if (index == 0)
     {
-        /*LACE_ME;
-       sylvan_gc(); // --- MC*/
-
-
         index = llmsset_lookup(nodes, n.a, n.b, &created);
         if (index == 0)
         {
             fprintf(stderr, "MDD Unique table full!\n");
-
             exit(1);
         }
     }
@@ -137,11 +130,7 @@ ldd_make_copynode(MDD ifeq, MDD ifneq)
     uint64_t index = llmsset_lookup(nodes, n.a, n.b, &created);
     if (index == 0)
     {
-        lddmc_refs_push(ifeq);
-        lddmc_refs_push(ifneq);
-        //  LACE_ME;
-        //sylvan_gc();
-        lddmc_refs_pop(1);
+        
 
         index = llmsset_lookup(nodes, n.a, n.b, &created);
         if (index == 0)
@@ -164,7 +153,7 @@ MDD lddmc_union_mono(MDD a, MDD b)
     if (a == lddmc_false) return b;
     if (b == lddmc_false) return a;
     assert(a != lddmc_true && b != lddmc_true); // expecting same length
-
+     
     /* Test gc */
     // LACE_ME;
     // sylvan_gc_test();
@@ -181,10 +170,10 @@ MDD lddmc_union_mono(MDD a, MDD b)
 
     /* Access cache */
     MDD result;
-    /*if (cache_get3(CACHE_MDD_UNION, a, b, 0, &result)) {
-        sylvan_stats_count(LDD_UNION_CACHED);
+    /*if (cache_get3(CACHE_LDD_UNION, a, b, 0,&result)) {        
         return result;
     }*/
+  
 
     /* Get nodes */
     mddnode_t na = GETNODE(a);
@@ -232,8 +221,8 @@ MDD lddmc_union_mono(MDD a, MDD b)
         result = ldd_makenode(nb_value, mddnode_getdown(nb), right);
     }
 
-    /* Write to cache */
-    // if (cache_put3(CACHE_MDD_UNION, a, b, 0, result)) sylvan_stats_count(LDD_UNION_CACHEDPUT);
+    
+    /*cache_put3(CACHE_LDD_UNION, a, b, 0, result);*/
 
     return result;
 }
@@ -291,15 +280,11 @@ MDD lddmc_firing_mono(MDD cmark, MDD minus, MDD plus)
 {
     // for an empty set of source states, or an empty transition relation, return the empty set
     if (cmark == lddmc_true) return lddmc_true;
-    if (minus == lddmc_false) return lddmc_false;
-    if (plus  == lddmc_false) return lddmc_false; // we assume that if meta is finished, then the rest is not in rel
-
-
-    /* Access cache */
+    if (minus == lddmc_false || plus  == lddmc_false) return lddmc_false;
+    
     MDD result;
     MDD _cmark=cmark, _minus=minus, _plus=plus;
-    /*if (cache_get3(CACHE_MDD_RELPROD, cmark, minus, plus, &result)) {
-        sylvan_stats_count(LDD_RELPROD_CACHED);
+  /*  if (cache_get3(CACHE_LDD_FIRE, cmark, minus, plus, &result)) {        
         return result;
     }*/
 
@@ -328,6 +313,7 @@ MDD lddmc_firing_mono(MDD cmark, MDD minus, MDD plus)
         if (cmark == lddmc_false) break;
         n_cmark = GETNODE(cmark);
     }
+    //cache_put3(CACHE_LDD_FIRE, cmark, minus, plus, result);
     return result;
 }