From d2fe46136afd9f15825d1095f5db0a53cf4c0bc9 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 6 Apr 2021 21:17:09 +0200 Subject: [PATCH] [buddy] introduce minterm enumeration support * src/bddop.c, src/bddx.h (bdd_ibuildcube2, bdd_first_minterm, bdd_next_minterm): New functions. * src/bddx.h (minterms_of): New class. --- buddy/src/bddop.c | 158 ++++++++++++++++++++++++++++++++++++++++++++++ buddy/src/bddx.h | 126 ++++++++++++++++++++++++++++++++++++ 2 files changed, 284 insertions(+) diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index f5ddbac15..fd8a06104 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -406,6 +406,164 @@ BDD bdd_ibuildcube(int value, int width, int *variables) return result; } +BDD bdd_ibuildcube2(int width, const int *variables) +{ + if (width == 0) + return BDDONE; + + BDD result; + { + int vn = variables[width - 1]; + if (vn >= 0) + result = bdd_ithvar(vn); + else + result = bdd_nithvar(~vn); + } + + for (int z = width - 2 ; z >= 0 ; --z) + { + BDD v; + int vn = variables[z]; + if (vn >= 0) + v = bdd_ithvar(vn); + else + v = bdd_nithvar(~vn); + int lv = LEVEL(v); + if (__likely(LEVEL(result) > lv)) + { + PUSHREF(result); + if (vn >= 0) + result = bdd_makenode(lv, BDDZERO, result); + else + result = bdd_makenode(lv, result, BDDZERO); + POPREF(1); + } + else + { + bdd_addref(result); + BDD tmp = bdd_apply(result, v, bddop_and); + bdd_delref(result); + result = tmp; + } + } + + return result; +} + +mintermEnumerator* bdd_init_minterm(BDD fun, BDD vars) +{ + mintermEnumerator* me = malloc(sizeof(mintermEnumerator)); + if (__unlikely(me == NULL)) + { + bdd_error(BDD_MEMORY); + return NULL; + } + int* varsptr = malloc(sizeof(int)*bddvarnum); + if (__unlikely(varsptr == NULL)) + { + free(me); + bdd_error(BDD_MEMORY); + return NULL; + } + int i = 0; + while (!ISCONST(vars)) + { + varsptr[i++] = bddlevel2var[LEVEL(vars)]; + vars = HIGH(vars); + } + int* stack = malloc(sizeof(int)*i*2); + if (__unlikely(stack == NULL)) + { + free(varsptr); + free(me); + bdd_error(BDD_MEMORY); + return NULL; + } + bdd_addref(fun); + me->vars = varsptr; + me->stacktop = stack; + me->stack = stack; + me->fun = fun; + me->nvars = i; + return me; +} + +void bdd_free_minterm(mintermEnumerator* me) +{ + bdd_delref(me->fun); + free(me->stack); + free(me->vars); + free(me); +} + +static int reset_minterm(mintermEnumerator*me, + BDD sub, int var) +{ + int nvars = me->nvars; + int* vars = me->vars; + int ls = LEVEL(sub); + for (int i = var; i < nvars; ++i) + { + int v = vars[i]; + int neg = v < 0; + if (neg) + v = ~v; + int lv = bddvar2level[v]; + if (ls == lv) /* variable used in fun */ + { + BDD low = LOW(sub); + if (low == BDDZERO) + { + sub = HIGH(sub); + } + else + { + if (HIGH(sub) != BDDZERO) + { + *me->stacktop++ = sub; + *me->stacktop++ = i; + } + v = ~v; + sub = low; + } + ls = LEVEL(sub); + } + else + { + *me->stacktop++ = sub; + *me->stacktop++ = i; + v = ~v; + } + vars[i] = v; + } + return 1; +} + + +int bdd_first_minterm(mintermEnumerator* me) +{ + if (__unlikely(me->fun == BDDZERO)) + return 0; + me->stacktop = me->stack; + return reset_minterm(me, me->fun, 0); +} + +bdd bdd_next_minterm(mintermEnumerator* me) +{ + if (me->stacktop == me->stack) // end of iteration + return 0; + int *vars = me->vars; + // switch polarity of variable of last possible branching + int lastbranch = *--me->stacktop; + BDD lastsub = *--me->stacktop; + int v = ~vars[lastbranch]; + if (LEVEL(lastsub) == bddvar2level[v]) + lastsub = HIGH(lastsub); + vars[lastbranch] = v; + // reset everything below to negative polarity + return reset_minterm(me, lastsub, lastbranch + 1); +} + /*=== NOT ==============================================================*/ diff --git a/buddy/src/bddx.h b/buddy/src/bddx.h index 48018ccec..6ac521939 100644 --- a/buddy/src/bddx.h +++ b/buddy/src/bddx.h @@ -127,6 +127,14 @@ typedef struct s_bddPair struct s_bddPair *next; } bddPair; +typedef struct +{ + int *vars; + int *stacktop; + int *stack; + BDD fun; + int nvars; +} mintermEnumerator; /*=== Status information ===============================================*/ @@ -333,6 +341,11 @@ BUDDY_API void bdd_freepair(bddPair*); BUDDY_API int bdd_setcacheratio(int); BUDDY_API BDD bdd_buildcube(int, int, BDD *); BUDDY_API BDD bdd_ibuildcube(int, int, int *); +BUDDY_API BDD bdd_ibuildcube2(int, const int *); +BUDDY_API mintermEnumerator* bdd_init_minterm(BDD, BDD); +BUDDY_API int bdd_first_minterm(mintermEnumerator*); +BUDDY_API int bdd_next_minterm(mintermEnumerator*); +BUDDY_API void bdd_free_minterm(mintermEnumerator*); BUDDY_API BDD bdd_not(BDD); BUDDY_API BDD bdd_apply(BDD, BDD, int); BUDDY_API BDD bdd_and(BDD, BDD); @@ -583,6 +596,11 @@ protected: friend bdd bdd_from_int(int i); friend bdd bdd_buildcube(int, int, const bdd *); friend bdd bdd_ibuildcubepp(int, int, int *); + friend bdd bdd_ibuildcubepp2(int, const int *); + friend mintermEnumerator* bdd_init_minterm(const bdd&, const bdd&); + friend int bdd_first_mintermpp(mintermEnumerator*); + friend int bdd_next_mintermpp(mintermEnumerator*); + friend void bdd_free_mintermpp(mintermEnumerator*); friend bdd bdd_not(const bdd &); friend bdd bdd_simplify(const bdd &, const bdd &); friend bdd bdd_apply(const bdd &, const bdd &, int); @@ -750,6 +768,21 @@ inline bdd bdd_simplify(const bdd &d, const bdd &b) inline bdd bdd_ibuildcubepp(int v, int w, int *a) { return bdd_ibuildcube(v,w,a); } +inline bdd bdd_ibuildcubepp2(int v, const int *a) +{ return bdd_ibuildcube2(v,a); } + +inline mintermEnumerator* bdd_init_minterm(const bdd& fun, const bdd& vars) +{ return bdd_init_minterm(fun.root, vars.root); } + +inline int bdd_first_mintermpp(mintermEnumerator* me) +{ return bdd_first_minterm(me); } + +inline int bdd_next_mintermpp(mintermEnumerator* me) +{ return bdd_next_minterm(me); } + +inline void bdd_free_mintermpp(mintermEnumerator* me) +{ return bdd_free_minterm(me); } + inline bdd bdd_not(const bdd &r) { return bdd_not(r.root); } @@ -904,6 +937,10 @@ inline int bdd_addvarblock(const bdd &v, int f) #define bdd_nithvar bdd_nithvarpp #define bdd_makeset bdd_makesetpp #define bdd_ibuildcube bdd_ibuildcubepp +#define bdd_ibuildcube2 bdd_ibuildcubepp2 +#define bdd_first_minterm bdd_first_mintermpp +#define bdd_next_minterm bdd_next_mintermpp +#define bdd_free_minterm bdd_free_mintermpp #define bdd_anodecount bdd_anodecountpp /*=== Inline C++ functions =============================================*/ @@ -1060,6 +1097,95 @@ typedef void (*bddstrmhandler)(std::ostream &, int); BUDDY_API bddstrmhandler bdd_strm_hook(bddstrmhandler); +/*=== Minterm enumeration ====*/ + +class minterms_of +{ +public: + class minterm_iterator + { + public: + minterm_iterator(minterms_of* me) + : me_(me) + { + } + + minterm_iterator& operator++(); + void operator++(int); + bool operator==(std::nullptr_t) const; + bool operator!=(std::nullptr_t) const; + bdd operator*() const; + protected: + minterms_of* me_; + }; + + minterms_of(bdd fun, bdd vars) + { + me_ = bdd_init_minterm(fun, vars); + } + + ~minterms_of() + { + bdd_free_minterm(me_); + } + + minterm_iterator begin() + { + done_ = !bdd_first_minterm(me_); + return this; + } + + std::nullptr_t end() const + { + return nullptr; + } + + bool done() const + { + return done_; + } + + bdd operator*() const + { + return bdd_ibuildcube2(me_->nvars, me_->vars); + } + + void operator++() + { + if (!bdd_next_minterm(me_)) + done_ = true; + } + +protected: + mintermEnumerator* me_; + bool done_; +}; + +inline minterms_of::minterm_iterator& +minterms_of::minterm_iterator::operator++() +{ + ++*me_; + return *this; +} + +inline bool +minterms_of::minterm_iterator::operator==(std::nullptr_t) const +{ + return me_->done(); +} + +inline bool +minterms_of::minterm_iterator::operator!=(std::nullptr_t) const +{ + return !me_->done(); +} + +inline bdd +minterms_of::minterm_iterator::operator*() const +{ + return **me_; +} + #endif /* CPLUSPLUS */ #endif /* _BDDX_H */