From 8582330575f48f010f175d9f2da630280f4cdb10 Mon Sep 17 00:00:00 2001
From: abid <chiheb.abid@gmail.com>
Date: Thu, 23 Apr 2020 01:53:15 +0100
Subject: [PATCH] =?UTF-8?q?=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20stats.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20=20s?=
=?UTF-8?q?ylvan=5Fint.h=20=09modifi=C3=A9=C2=A0:=20=20=20=20=20=20=20=20?=
=?UTF-8?q?=20sylvan=5Fseq.c?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
stats.h | 1 +
sylvan_int.h | 3 +++
sylvan_seq.c | 34 ++++++++++------------------------
3 files changed, 14 insertions(+), 24 deletions(-)
diff --git a/stats.h b/stats.h
index c7bfcaa..5803bc2 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 61ea570..008541b 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 ceaa946..d10dddf 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;
}
--
GitLab