From 5a0fbf6cb94c2ea84a9a848170dc24b4be038c73 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 16 Jun 2021 22:33:22 +0200 Subject: [PATCH] [buddy] introduce a bdd_satoneshortest() function * src/bddop.c, src/bddx.h: Introduce this function. * src/bddtest.cxx: Add some short tests. --- buddy/src/bddop.c | 151 ++++++++++++++++++++++++++++++++++++++++++ buddy/src/bddtest.cxx | 55 +++++++++++++++ buddy/src/bddx.h | 9 +++ 3 files changed, 215 insertions(+) diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index 59ac03fe3..a05152c6d 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -61,6 +61,8 @@ #define CACHEID_SUPPORT 0x6 #define CACHEID_IMPLIES 0x7 #define CACHEID_COMMON 0x8 +#define CACHEID_SHORTDIST 0x9 +#define CACHEID_SHORTBDD 0xA /* Hash value modifiers for replace/compose */ #define CACHEID_REPLACE 0x0 @@ -182,6 +184,8 @@ static int varset2svartable(BDD); #define PATHCOUHASH(r) (r) #define SUPPORTHASH(r) (PAIR(r,CACHEID_SUPPORT)) #define APPEXHASH(l,r,op) (PAIR(l,r)) +#define SHORTDISTHASH(l,rev) (TRIPLE(l,rev,CACHEID_SHORTDIST)) +#define SHORTBDDHASH(l,rev) (TRIPLE(l,rev,CACHEID_SHORTBDD)) #ifndef M_LN2 #define M_LN2 0.69314718055994530942 @@ -3078,6 +3082,153 @@ static BDD satoneset_rec(BDD r, BDD var) } +/* Compute the smallest distance associated to a satisfying path of f, + but without actually building the corresponding cube. This is done + by computing the distance recursively for all sub BDDs, and storing + those in a hashtable, with the intention of sharing that across + all calls of bdd_satoneshortest with the same weights. + + The hash table used for cache stores triples of the form (bdd, rev, + dist) where dist is the distance for bdd, and rev is incremented + everytime bdd_satoneshortest is called with a different set of + weights. One should therefore check that rev from the cache lookup + matches the current rev stored in shortest_rev. bdd_satoneshortest + is in charge of incrementing shortest_rev. + */ +static unsigned wlow_ref = 0; +static unsigned whigh_ref = 0; +static unsigned wdc_ref = 0; +static int shortest_rev = 0; + +/* This computes the shortest distance, recursively. + Populating the cache. */ +static unsigned satoneshortest_rec(BDD f) +{ + if (ISONE(f)) + return 0; + if (ISZERO(f)) + return -1U; + int rev = shortest_rev; + BddCacheData *entry = BddCache_lookup(&misccache, SHORTDISTHASH(f,rev)); + if (entry->i.a == f + && entry->i.b == rev + && entry->i.c == CACHEID_SHORTDIST) + { +#ifdef CACHESTATS + bddcachestats.opHit++; +#endif + return (unsigned) entry->i.res; + } +#ifdef CACHESTATS + bddcachestats.opMiss++; +#endif + + int lv_next = LEVEL(f) + 1; + int low = LOW(f); + int lv_low = LEVEL(low); + unsigned dist_low = satoneshortest_rec(low); + if (dist_low != -1U) + dist_low += wlow_ref + wdc_ref * (lv_low - lv_next); + int high = HIGH(f); + int lv_high = LEVEL(high); + unsigned dist_high = satoneshortest_rec(high); + if (dist_high != -1U) + dist_high += whigh_ref + wdc_ref * (lv_high - lv_next); + + if (dist_high < dist_low) + dist_low = dist_high; + + entry->i.a = f; + entry->i.b = rev; + entry->i.c = CACHEID_SHORTDIST; + entry->i.res = (int) dist_low; + return dist_low; +} + +/* This computes the BDD for the shortest distance, recursively. + It calls satoneshortest_rec again, but this should be fast thanks to + the cache. +*/ +static bdd bdd_satoneshortest_rec(BDD f) +{ + if (ISONE(f)) + return bddtrue; + if (ISZERO(f)) + return bddfalse; + + int rev = shortest_rev; + BddCacheData *entry = BddCache_lookup(&misccache, SHORTBDDHASH(f,rev)); + if (entry->i.a == f + && entry->i.b == rev + && entry->i.c == CACHEID_SHORTDIST) + { +#ifdef CACHESTATS + bddcachestats.opHit++; +#endif + return entry->i.res; + } +#ifdef CACHESTATS + bddcachestats.opMiss++; +#endif + + int lv = LEVEL(f); + int lv_next = lv + 1; + int low = LOW(f); + int lv_low = LEVEL(low); + unsigned dist_low = satoneshortest_rec(low); + if (dist_low != -1U) + dist_low += wlow_ref + wdc_ref * (lv_low - lv_next); + + int high = HIGH(f); + int lv_high = LEVEL(high); + unsigned dist_high = satoneshortest_rec(high); + if (dist_high != -1U) + dist_high += whigh_ref + wdc_ref * (lv_high - lv_next); + + bdd res; + if (dist_high < dist_low) + { + res = bdd_satoneshortest_rec(high); + res = PUSHREF(bdd_makenode(lv, 0, res)); + } + else + { + res = bdd_satoneshortest_rec(low); + res = PUSHREF(bdd_makenode(lv, res, 0)); + } + + entry->i.a = f; + entry->i.b = rev; + entry->i.c = CACHEID_SHORTBDD; + entry->i.res = res; + return res; +} + +/* + return a conjunction representing a satisfying path of f, chosen + among all satisfying paths to minimize the sum of weights given for + positive variables (whigh), negative variables (wlow), and don't care + variables (wdc = Weight of Don't Care). +*/ +BDD bdd_satoneshortest(BDD f, unsigned wlow, unsigned whigh, unsigned wdc) +{ + if (wlow != wlow_ref || whigh != whigh_ref || wdc != wdc_ref) + { + wlow_ref = wlow; + whigh_ref = whigh; + wdc_ref = wdc; + ++shortest_rev; + } + bdd_disable_reorder(); + INITREF; + bdd res = bdd_satoneshortest_rec(f); + bdd_enable_reorder(); + checkresize(); + return res; +} + + + /*=== EXACTLY ONE SATISFYING VARIABLE ASSIGNMENT =======================*/ /* diff --git a/buddy/src/bddtest.cxx b/buddy/src/bddtest.cxx index 78b6bd064..bb07934bf 100644 --- a/buddy/src/bddtest.cxx +++ b/buddy/src/bddtest.cxx @@ -96,6 +96,60 @@ void testBvecIte() ERROR("Bit 2 failed."); } +void testShortest() +{ + cout << "Testing bdd_satoneshortest()\n"; + + bdd a = bdd_ithvar(0); + bdd b = bdd_ithvar(1); + bdd c = bdd_ithvar(2); + bdd d = bdd_ithvar(3); + + bdd cube1 = a&c&!d; + bdd cube2 = a&!c&d; + bdd cube3 = !a&b&c&!d; + bdd cube4 = !a&!b&d; + + bdd f = cube1 | cube2 | cube3 | cube4 ; + + // avoid don't care at all cost, prefer negative + bdd res = bdd_satoneshortest(f, 0, 1, 4); + if (res != cube3) + ERROR("shortest 0 1 4 failed"); + + // avoid don't care at all cost, prefer positive + res = bdd_satoneshortest(f, 1, 0, 4); + if (res != cube3) + ERROR("shortest 1 0 4 failed"); + + // avoid negative at all cost, prefer positive + res = bdd_satoneshortest(f, 4, 0, 1); + if (res != cube2) + ERROR("shortest 4 0 1 failed"); + + // avoid negative at all cost, prefer don't care + res = bdd_satoneshortest(f, 4, 1, 0); + if (res != cube2) + ERROR("shortest 4 1 0 failed"); + + // avoid positive at all cost, prefer don't care + res = bdd_satoneshortest(f, 1, 4, 0); + if (res != cube4) + ERROR("shortest 1 4 0 failed"); + + // avoid positive at all cost, prefer negative + res = bdd_satoneshortest(f, 0, 4, 1); + if (res != cube4) + ERROR("shortest 0 4 1 failed"); + + res = bdd_satoneshortest(bddfalse, 1, 2, 3); + if (res != bddfalse) + ERROR("shortest bddfalse failed"); + + res = bdd_satoneshortest(bddtrue, 1, 2, 3); + if (res != bddtrue) + ERROR("shortest bddtrue failed"); +} int main(int ac, char** av) { @@ -105,6 +159,7 @@ int main(int ac, char** av) testSupport(); testBvecIte(); + testShortest(); bdd_done(); return 0; diff --git a/buddy/src/bddx.h b/buddy/src/bddx.h index c3f8da2fe..174c5713b 100644 --- a/buddy/src/bddx.h +++ b/buddy/src/bddx.h @@ -379,6 +379,7 @@ BUDDY_API BDD bdd_support(BDD); BUDDY_API BDD bdd_satone(BDD); BUDDY_API BDD bdd_satoneset(BDD, BDD, BDD); BUDDY_API BDD bdd_fullsatone(BDD); +BUDDY_API BDD bdd_satoneshortest(BDD, unsigned, unsigned, unsigned); BUDDY_API BDD bdd_satprefix(BDD *); BUDDY_API void bdd_allsat(BDD r, bddallsathandler handler); BUDDY_API double bdd_satcount(BDD); @@ -635,6 +636,8 @@ protected: friend bdd bdd_satone(const bdd &); friend bdd bdd_satoneset(const bdd &, const bdd &, const bdd &); friend bdd bdd_fullsatone(const bdd &); + friend bdd bdd_satoneshortest(const bdd &, + unsigned, unsigned, unsigned); friend bdd bdd_satprefix(bdd &); friend void bdd_allsat(const bdd &r, bddallsathandler handler); friend void bdd_allsat(const bdd &r, bddallsathandler_old handler); @@ -867,6 +870,12 @@ inline bdd bdd_satoneset(const bdd &r, const bdd &var, const bdd &pol) inline bdd bdd_fullsatone(const bdd &r) { return bdd_fullsatone(r.root); } +inline bdd bdd_satoneshortest(const bdd &r, unsigned wlow, + unsigned whigh, unsigned wdc) +{ + return bdd_satoneshortest(r.root, wlow, whigh, wdc); +} + inline bdd bdd_satprefix(bdd &r) { int ro = r.root; bdd res = bdd_satprefix(&ro); r = bdd(ro); return res; }