diff --git a/stats.h b/stats.h index c7bfcaae271981f14e167eda722d93800ab6858c..5803bc2027b63ba6f0c213f7bb96dac785d44e05 100755 --- a/stats.h +++ b/stats.h @@ -114,6 +114,7 @@ typedef enum { LDD_PROJECT_MINUS_CACHED, LDD_NODES_CREATED, LDD_NODES_REUSED, + LDD_FIRE_CACHED, LLMSSET_LOOKUP, diff --git a/sylvan_int.h b/sylvan_int.h index 61ea5707c1b5d3110a26a89a30ca558b447ee6ed..008541b5f5b09a46f85696f0dbc61238b6a611b0 100755 --- a/sylvan_int.h +++ b/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); diff --git a/sylvan_seq.c b/sylvan_seq.c index ceaa9469a0a7c0deacc1d848867a2435653045cb..d10dddfb1b0bcf863e08d7e5ac2a546be8645392 100755 --- a/sylvan_seq.c +++ b/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; }