--- /dev/null
+/********************************************\r
+ * BDD+ Manipulator (SAPPORO-1.58) - Header *\r
+ * (C) Shin-ichi MINATO (Nov. 22, 2013) *\r
+ ********************************************/\r
+\r
+class BDD;\r
+class BDDV;\r
+\r
+#ifndef _BDD_\r
+#define _BDD_\r
+\r
+#include <cstdlib>\r
+#include <cstdio>\r
+#include <cstring>\r
+#include <cctype>\r
+#include <iostream>\r
+\r
+#define BDD_CPP\r
+#include "bddc.h"\r
+\r
+using namespace std;\r
+\r
+//--------- Definition of "bddword" type --------\r
+#ifdef B_64\r
+ typedef unsigned long long bddword;\r
+#else\r
+ typedef unsigned int bddword;\r
+#endif\r
+\r
+//--------- External data for BDD ---------\r
+extern const bddword BDD_MaxNode;\r
+extern const int BDD_MaxVar;\r
+\r
+//----- External constant data for BDDV ---------\r
+extern int BDDV_Active;\r
+extern const int BDDV_SysVarTop;\r
+extern const int BDDV_MaxLen;\r
+extern const int BDDV_MaxLenImport;\r
+\r
+//--------- Stack overflow limitter ---------\r
+extern const int BDD_RecurLimit;\r
+extern int BDD_RecurCount;\r
+#define BDD_RECUR_INC \\r
+ {if(++BDD_RecurCount >= BDD_RecurLimit) \\r
+ BDDerr("BDD_RECUR_INC:Stack overflow ", (bddword) BDD_RecurCount);}\r
+#define BDD_RECUR_DEC BDD_RecurCount--\r
+\r
+class BDD\r
+{\r
+ bddword _bdd;\r
+\r
+public:\r
+ BDD(void) { _bdd = bddfalse; }\r
+ BDD(int a) { _bdd = (a==0)? bddfalse:(a>0)? bddtrue:bddnull; }\r
+ BDD(const BDD& f) { _bdd = bddcopy(f._bdd); }\r
+\r
+ ~BDD(void) { bddfree(_bdd); }\r
+\r
+ BDD& operator=(const BDD& f) { \r
+ if(_bdd != f._bdd) { bddfree(_bdd); _bdd = bddcopy(f._bdd); }\r
+ return *this; \r
+ }\r
+\r
+ BDD& operator&=(const BDD& f)\r
+ { BDD h; h._bdd = bddand(_bdd, f._bdd); return *this = h; }\r
+ BDD& operator|=(const BDD& f)\r
+ { BDD h; h._bdd = bddor(_bdd, f._bdd); return *this = h; }\r
+ BDD& operator^=(const BDD& f)\r
+ { BDD h; h._bdd = bddxor(_bdd, f._bdd); return *this = h; }\r
+ BDD& operator<<=(const int s)\r
+ { BDD h; h._bdd = bddlshift(_bdd, s); return *this = h; }\r
+ BDD& operator>>=(const int s)\r
+ { BDD h; h._bdd = bddrshift(_bdd, s); return *this = h; }\r
+\r
+ BDD operator~(void) const { BDD h; h._bdd = bddnot(_bdd); return h; }\r
+ BDD operator<<(int s) const\r
+ { BDD h; h._bdd = bddlshift(_bdd, s); return h; }\r
+ BDD operator>>(int s) const\r
+ { BDD h; h._bdd = bddrshift(_bdd, s); return h; }\r
+\r
+ int Top(void) const { return bddtop(_bdd); }\r
+ BDD At0(int v) const { BDD h; h._bdd = bddat0(_bdd, v); return h; }\r
+ BDD At1(int v) const { BDD h; h._bdd = bddat1(_bdd, v); return h; }\r
+ BDD Cofact(const BDD& f) const\r
+ { BDD h; h._bdd = bddcofactor(_bdd, f._bdd); return h; }\r
+ BDD Univ(const BDD& f) const\r
+ { BDD h; h._bdd = bdduniv(_bdd, f._bdd); return h; }\r
+ BDD Exist(const BDD& f) const\r
+ { BDD h; h._bdd = bddexist(_bdd, f._bdd); return h; }\r
+ BDD Support(void) const\r
+ { BDD h; h._bdd = bddsupport(_bdd); return h; }\r
+\r
+ bddword GetID(void) const {return _bdd; }\r
+ \r
+ bddword Size(void) const;\r
+ void Export(FILE *strm = stdout) const;\r
+ void Print(void) const;\r
+ void XPrint0(void) const;\r
+ void XPrint(void) const;\r
+\r
+ BDD Swap(const int&, const int&) const;\r
+ BDD Smooth(const int&) const;\r
+ BDD Spread(const int&) const;\r
+\r
+ friend BDD BDD_ID(bddword);\r
+};\r
+\r
+//--------- External functions for BDD ---------\r
+extern void BDD_Init(bddword, bddword);\r
+extern int BDD_NewVarOfLev(int);\r
+extern int BDD_VarUsed(void);\r
+extern bddword BDD_Used(void);\r
+extern void BDD_GC(void);\r
+extern BDD BDD_Import(FILE *strm = stdin);\r
+extern BDD BDD_Random(int, int density = 50);\r
+extern void BDDerr(const char *);\r
+extern void BDDerr(const char *, bddword);\r
+extern void BDDerr(const char *, const char *);\r
+\r
+//--------- Inline functions for BDD ---------\r
+inline int BDD_TopLev(void)\r
+ { return BDDV_Active? bddvarused() - BDDV_SysVarTop: bddvarused(); }\r
+\r
+inline int BDD_NewVar(void)\r
+ { return bddnewvaroflev(BDD_TopLev() + 1); }\r
+\r
+inline int BDD_LevOfVar(int v) { return bddlevofvar(v); }\r
+inline int BDD_VarOfLev(int lev) { return bddvaroflev(lev); }\r
+\r
+inline BDD BDD_ID(bddword bdd)\r
+ { BDD h; h._bdd = bdd; return h; }\r
+\r
+inline bddword BDD_CacheInt(unsigned char op, bddword fx, bddword gx)\r
+ { return bddrcache(op, fx, gx); }\r
+\r
+inline BDD BDD_CacheBDD(unsigned char op, bddword fx, bddword gx)\r
+ { return BDD_ID(bddcopy(bddrcache(op, fx, gx))); }\r
+\r
+inline void BDD_CacheEnt(unsigned char op, bddword fx, bddword gx, bddword hx)\r
+ { bddwcache(op, fx, gx, hx); }\r
+\r
+inline BDD BDDvar(int v) { return BDD_ID(bddprime(v)); }\r
+\r
+inline BDD operator&(const BDD& f, const BDD& g) \r
+ { return BDD_ID(bddand(f.GetID(), g.GetID())); }\r
+\r
+inline BDD operator|(const BDD& f, const BDD& g) \r
+ { return BDD_ID(bddor(f.GetID(), g.GetID())); }\r
+\r
+inline BDD operator^(const BDD& f, const BDD& g) \r
+ { return BDD_ID(bddxor(f.GetID(), g.GetID())); }\r
+\r
+inline int operator==(const BDD& f, const BDD& g) \r
+ { return f.GetID() == g.GetID(); }\r
+\r
+inline int operator!=(const BDD& f, const BDD& g) \r
+ { return f.GetID() != g.GetID(); }\r
+\r
+inline int BDD_Imply(const BDD& f, const BDD& g) \r
+ { return bddimply(f.GetID(), g.GetID()); }\r
+\r
+class BDDV\r
+{\r
+ BDD _bdd;\r
+ int _len;\r
+ int _lev;\r
+\r
+ int GetLev(int len) const {\r
+ int lev = 0;\r
+ for(len--; len>0; len>>=1) lev++;\r
+ return lev;\r
+ }\r
+\r
+public:\r
+ BDDV(void) { _bdd = 0; _len = 0; _lev = 0; }\r
+\r
+ BDDV(const BDDV& fv)\r
+ { _bdd = fv._bdd; _len = fv._len; _lev = fv._lev; } \r
+\r
+ BDDV(const BDD& f) {\r
+ int t = f.Top();\r
+ if(t > 0 && BDD_LevOfVar(t) > BDD_TopLev())\r
+ BDDerr("BDDV::BDDV: Invalid top var.", t);\r
+ _bdd = f;\r
+ _len = 1;\r
+ _lev = 0;\r
+ }\r
+\r
+ BDDV(const BDD&, int len);\r
+\r
+ ~BDDV(void) { }\r
+\r
+ BDDV& operator=(const BDDV& fv)\r
+ { _bdd = fv._bdd; _len = fv._len; _lev = fv._lev; return *this; } \r
+\r
+ BDDV& operator&=(const BDDV&);\r
+ BDDV& operator|=(const BDDV&);\r
+ BDDV& operator^=(const BDDV&);\r
+ BDDV& operator<<=(int);\r
+ BDDV& operator>>=(int);\r
+\r
+ BDDV operator~(void) const\r
+ { BDDV h; h._bdd = ~_bdd; h._len = _len; h._lev = _lev; return h; } \r
+ BDDV operator<<(int) const;\r
+ BDDV operator>>(int) const;\r
+\r
+ BDDV At0(int v) const {\r
+ if(v > 0 && BDD_LevOfVar(v) > BDD_TopLev())\r
+ BDDerr("BDDV::At0: Invalid var.", v);\r
+ BDDV hv;\r
+ if((hv._bdd = _bdd.At0(v)) == -1) return BDDV(-1);\r
+ hv._len = _len;\r
+ hv._lev = _lev;\r
+ return hv;\r
+ }\r
+\r
+ BDDV At1(int v) const {\r
+ if(v > 0 && BDD_LevOfVar(v) > BDD_TopLev())\r
+ BDDerr("BDDV::At1: Invalid var.", v);\r
+ BDDV hv;\r
+ if((hv._bdd = _bdd.At1(v)) == -1) return BDDV(-1);\r
+ hv._len = _len;\r
+ hv._lev = _lev;\r
+ return hv;\r
+ }\r
+\r
+ BDDV Cofact(const BDDV&) const;\r
+ BDDV Swap(int, int) const;\r
+ BDDV Spread(int) const;\r
+\r
+ int Top(void) const;\r
+\r
+ bddword Size() const;\r
+ void Export(FILE *strm = stdout) const;\r
+\r
+ BDDV Former(void) const {\r
+ BDDV hv;\r
+ if(_len <= 1) return hv;\r
+ if((hv._bdd = _bdd.At0(_lev)) == -1) return BDDV(-1);\r
+ hv._len = 1 << (_lev - 1);\r
+ hv._lev = _lev - 1;\r
+ return hv;\r
+ }\r
+\r
+ BDDV Latter(void) const {\r
+ BDDV hv;\r
+ if(_len == 0) return hv;\r
+ if(_len == 1) return *this;\r
+ if((hv._bdd = _bdd.At1(_lev)) == -1) return BDDV(-1);\r
+ hv._len = _len - (1 << (_lev - 1));\r
+ hv._lev = GetLev(hv._len);\r
+ return hv;\r
+ }\r
+\r
+ BDDV Part(int, int) const;\r
+ BDD GetBDD(int) const;\r
+\r
+ BDD GetMetaBDD(void) const { return _bdd; }\r
+ int Uniform(void) const\r
+ { return BDD_LevOfVar(_bdd.Top()) <= BDD_TopLev(); }\r
+ int Len(void) const { return _len; }\r
+\r
+ void Print() const;\r
+ void XPrint0() const;\r
+ void XPrint() const;\r
+\r
+ friend BDDV operator&(const BDDV&, const BDDV&);\r
+ friend BDDV operator|(const BDDV&, const BDDV&);\r
+ friend BDDV operator^(const BDDV&, const BDDV&);\r
+ friend BDDV operator||(const BDDV&, const BDDV&);\r
+};\r
+\r
+//----- External functions for BDDV ---------\r
+extern void BDDV_Init(bddword, bddword);\r
+extern int BDDV_NewVarOfLev(int);\r
+extern BDDV operator||(const BDDV&, const BDDV&);\r
+extern BDDV BDDV_Mask1(int, int);\r
+extern BDDV BDDV_Mask2(int, int);\r
+extern BDDV BDDV_Import(FILE *strm = stdin);\r
+\r
+//----- Inline functions for BDDV ---------\r
+inline int BDDV_UserTopLev(void) { return BDD_TopLev(); }\r
+inline int BDDV_NewVar(void) { return BDD_NewVar(); }\r
+inline int BDDV_NewVarOfLev(int lev) {return BDD_NewVarOfLev(lev); }\r
+\r
+inline BDDV operator&(const BDDV& fv, const BDDV& gv) {\r
+ BDDV hv;\r
+ if((hv._bdd = fv._bdd & gv._bdd) == -1) return BDDV(-1);\r
+ if(fv._len != gv._len) BDDerr("BDDV::operator&: Length mismatch");\r
+ hv._len = fv._len;\r
+ hv._lev = fv._lev;\r
+ return hv;\r
+}\r
+\r
+inline BDDV operator|(const BDDV& fv, const BDDV& gv) {\r
+ BDDV hv;\r
+ if((hv._bdd = fv._bdd | gv._bdd) == -1) return BDDV(-1);\r
+ if(fv._len != gv._len) BDDerr("BDDV::operator|: Length mismatch");\r
+ hv._len = fv._len;\r
+ hv._lev = fv._lev;\r
+ return hv;\r
+}\r
+\r
+inline BDDV operator^(const BDDV& fv, const BDDV& gv) {\r
+ BDDV hv;\r
+ if((hv._bdd = fv._bdd ^ gv._bdd) == -1) return BDDV(-1);\r
+ if(fv._len != gv._len) BDDerr("BDDV::operator^: Length mismatch");\r
+ hv._len = fv._len;\r
+ hv._lev = fv._lev;\r
+ return hv;\r
+}\r
+\r
+extern BDDV operator|(const BDDV&, const BDDV&);\r
+extern BDDV operator^(const BDDV&, const BDDV&);\r
+inline int operator==(const BDDV& fv, const BDDV& gv)\r
+\r
+ { return fv.GetMetaBDD() == gv.GetMetaBDD() && fv.Len() == gv.Len(); }\r
+\r
+inline int operator!=(const BDDV& fv, const BDDV& gv)\r
+ { return !(fv == gv); }\r
+\r
+inline int BDDV_Imply(const BDDV& fv, const BDDV& gv) {\r
+ return fv.Len() == gv.Len() \r
+ && BDD_Imply(fv.GetMetaBDD(), gv.GetMetaBDD());\r
+}\r
+\r
+inline BDDV& BDDV::operator&=(const BDDV& fv) { return *this = *this & fv; }\r
+inline BDDV& BDDV::operator|=(const BDDV& fv) { return *this = *this | fv; }\r
+inline BDDV& BDDV::operator^=(const BDDV& fv) { return *this = *this ^ fv; }\r
+inline BDDV& BDDV::operator<<=(int s) { return *this = *this << s; }\r
+inline BDDV& BDDV::operator>>=(int s) { return *this = *this >> s; }\r
+\r
+\r
+class BDD_Hash\r
+{\r
+ struct BDD_Entry\r
+ {\r
+ BDD _key;\r
+ void* _ptr;\r
+ BDD_Entry(void){ _key = -1; }\r
+ };\r
+\r
+ bddword _amount;\r
+ bddword _hashSize;\r
+ BDD_Entry* _wheel;\r
+\r
+ BDD_Entry* GetEntry(BDD);\r
+ void Enlarge(void);\r
+public:\r
+ BDD_Hash(void);\r
+ ~BDD_Hash(void);\r
+ void Clear(void);\r
+ void Enter(BDD, void *);\r
+ void* Refer(BDD);\r
+ bddword Amount(void);\r
+};\r
+\r
+#endif // _BDD_ \r
OSDN Git Service
