zdd/lib/SAPPOROBDD/include/ZBDD.h

   1 /*********************************************
   2  * ZBDD+ Manipulator (SAPPORO-1.58) - Header *
   3  * (C) Shin-ichi MINATO  (Nov. 22, 2013)     *
   4  *********************************************/
   5
   6 class ZBDD;
   7 class ZBDDV;
   8
   9 #ifndef _ZBDD_
  10 #define _ZBDD_
  11
  12 #include "BDD.h"
  13
  14 class SeqBDD;
  15
  16 class ZBDD
  17 {
  18   bddword _zbdd;
  19
  20 public:
  21   ZBDD(void) { _zbdd = bddempty; }
  22   ZBDD(int v) { _zbdd = (v==0)? bddempty:(v>0)? bddsingle:bddnull; }
  23   ZBDD(const ZBDD& f) { _zbdd = bddcopy(f._zbdd); }
  24
  25   ~ZBDD(void) { bddfree(_zbdd); }
  26
  27   ZBDD& operator=(const ZBDD& f) {
  28     if(_zbdd != f._zbdd) { bddfree(_zbdd); _zbdd = bddcopy(f._zbdd); }
  29     return *this;
  30   }
  31
  32   ZBDD& operator&=(const ZBDD& f)
  33     { ZBDD h; h._zbdd = bddintersec(_zbdd, f._zbdd); return *this = h; }
  34
  35   ZBDD& operator+=(const ZBDD& f)
  36     { ZBDD h; h._zbdd = bddunion(_zbdd, f._zbdd); return *this = h; }
  37
  38   ZBDD& operator-=(const ZBDD& f)
  39     { ZBDD h; h._zbdd = bddsubtract(_zbdd, f._zbdd); return *this = h; }
  40
  41   ZBDD& operator<<=(int s)
  42     { ZBDD h; h._zbdd = bddlshift(_zbdd, s); return *this = h; }
  43
  44   ZBDD& operator>>=(int s)
  45     { ZBDD h; h._zbdd = bddrshift(_zbdd, s); return *this = h; }
  46
  47   ZBDD& operator*=(const ZBDD&);
  48   ZBDD& operator/=(const ZBDD&);
  49   ZBDD& operator%=(const ZBDD&);
  50
  51   ZBDD operator<<(int s) const
  52     { ZBDD h; h._zbdd = bddlshift(_zbdd, s); return h; }
  53
  54   ZBDD operator>>(int s) const
  55     { ZBDD h; h._zbdd = bddrshift(_zbdd, s); return h; }
  56
  57   int Top(void) const { return bddtop(_zbdd); }
  58
  59   ZBDD OffSet(int v) const
  60     { ZBDD h; h._zbdd = bddoffset(_zbdd, v); return h; }
  61
  62   ZBDD OnSet(int v) const
  63     { ZBDD h; h._zbdd = bddonset(_zbdd, v); return h; }
  64
  65   ZBDD OnSet0(int v) const
  66     { ZBDD h; h._zbdd = bddonset0(_zbdd, v); return h; }
  67
  68   ZBDD Change(int v) const
  69     { ZBDD h; h._zbdd = bddchange(_zbdd, v); return h; }
  70
  71   bddword GetID(void) const { return _zbdd; }
  72   bddword Size(void) const { return bddsize(_zbdd); }
  73   bddword Card(void) const { return bddcard(_zbdd); }
  74   bddword Lit(void) const { return bddlit(_zbdd); }
  75   bddword Len(void) const { return bddlen(_zbdd); }
  76
  77   void Export(FILE *strm = stdout) const;
  78   void XPrint(void) const;
  79   void Print(void) const;
  80   void PrintPla(void) const;
  81
  82   ZBDD Swap(int, int) const;
  83   ZBDD Restrict(const ZBDD&) const;
  84   ZBDD Permit(const ZBDD&) const;
  85   ZBDD PermitSym(int) const;
  86   ZBDD Support(void) const
  87     { ZBDD h; h._zbdd = bddsupport(_zbdd); return h; }
  88   ZBDD Always(void) const;
  89
  90   int SymChk(int, int) const;
  91   ZBDD SymGrp(void) const;
  92   ZBDD SymGrpNaive(void) const;
  93
  94   ZBDD SymSet(int) const;
  95   int ImplyChk(int, int) const;
  96   int CoImplyChk(int, int) const;
  97   ZBDD ImplySet(int) const;
  98   ZBDD CoImplySet(int) const;
  99
 100   int IsPoly(void) const;
 101   ZBDD Divisor(void) const;
 102
 103   ZBDD ZLev(int lev, int last = 0) const;
 104   void SetZSkip(void) const;
 105   ZBDD Intersec(const ZBDD&) const;
 106
 107   friend ZBDD ZBDD_ID(bddword);
 108
 109   //friend class SeqBDD;
 110 };
 111
 112 extern ZBDD operator*(const ZBDD&, const ZBDD&);
 113 extern ZBDD operator/(const ZBDD&, const ZBDD&);
 114 extern ZBDD ZBDD_Meet(const ZBDD&, const ZBDD&);
 115 extern ZBDD ZBDD_Random(int, int density = 50);
 116 extern ZBDD ZBDD_Import(FILE *strm = stdin);
 117
 118 extern ZBDD ZBDD_LCM_A(char *, int);
 119 extern ZBDD ZBDD_LCM_C(char *, int);
 120 extern ZBDD ZBDD_LCM_M(char *, int);
 121
 122 inline ZBDD ZBDD_ID(bddword zbdd)
 123   { ZBDD h; h._zbdd = zbdd; return h; }
 124
 125 inline ZBDD BDD_CacheZBDD(char op, bddword fx, bddword gx)
 126   { return ZBDD_ID(bddcopy(bddrcache(op, fx, gx))); }
 127
 128 inline ZBDD operator&(const ZBDD& f, const ZBDD& g)
 129   { return ZBDD_ID(bddintersec(f.GetID(), g.GetID())); }
 130
 131 inline ZBDD operator+(const ZBDD& f, const ZBDD& g)
 132   { return ZBDD_ID(bddunion(f.GetID(), g.GetID())); }
 133
 134 inline ZBDD operator-(const ZBDD& f, const ZBDD& g)
 135   { return ZBDD_ID(bddsubtract(f.GetID(), g.GetID())); }
 136
 137 inline ZBDD operator%(const ZBDD& f, const ZBDD& p)
 138   { return f - (f/p) * p; }
 139
 140 inline int operator==(const ZBDD& f, const ZBDD& g)
 141   { return f.GetID() == g.GetID(); }
 142
 143 inline int operator!=(const ZBDD& f, const ZBDD& g)
 144   { return !(f == g); }
 145
 146 inline ZBDD& ZBDD::operator*=(const ZBDD& f)
 147   { return *this = *this * f; }
 148
 149 inline ZBDD& ZBDD::operator/=(const ZBDD& f)
 150   { return *this = *this / f; }
 151
 152 inline ZBDD& ZBDD::operator%=(const ZBDD& f)
 153   { return *this = *this % f; }
 154
 155
 156 class ZBDDV
 157 {
 158   ZBDD _zbdd;
 159
 160 public:
 161   ZBDDV(void) { _zbdd = 0; }
 162   ZBDDV(const ZBDDV& fv) { _zbdd = fv._zbdd; }
 163   ZBDDV(const ZBDD& f, int location = 0);
 164   ~ZBDDV(void) { }
 165
 166   ZBDDV& operator=(const ZBDDV& fv) { _zbdd = fv._zbdd; return *this; }
 167   ZBDDV& operator&=(const ZBDDV& fv) { _zbdd &= fv._zbdd; return *this; }
 168   ZBDDV& operator+=(const ZBDDV& fv) { _zbdd += fv._zbdd; return *this; }
 169   ZBDDV& operator-=(const ZBDDV& fv) { _zbdd -= fv._zbdd; return *this; }
 170   ZBDDV& operator<<=(int);
 171   ZBDDV& operator>>=(int);
 172
 173   ZBDDV operator<<(int) const;
 174   ZBDDV operator>>(int) const;
 175
 176   ZBDDV OffSet(int) const;
 177   ZBDDV OnSet(int) const;
 178   ZBDDV OnSet0(int) const;
 179   ZBDDV Change(int) const;
 180   ZBDDV Swap(int, int) const;
 181
 182   int Top(void) const;
 183   int Last(void) const;
 184   ZBDDV Mask(int start, int length = 1) const;
 185   ZBDD GetZBDD(int) const;
 186
 187   ZBDD GetMetaZBDD(void) const { return _zbdd; }
 188   bddword Size(void) const;
 189   void Print(void) const;
 190   void Export(FILE *strm = stdout) const;
 191   int PrintPla(void) const;
 192   void XPrint(void) const;
 193
 194   friend ZBDDV operator&(const ZBDDV&, const ZBDDV&);
 195   friend ZBDDV operator+(const ZBDDV&, const ZBDDV&);
 196   friend ZBDDV operator-(const ZBDDV&, const ZBDDV&);
 197 };
 198
 199 extern ZBDDV ZBDDV_Import(FILE *strm = stdin);
 200
 201 inline ZBDDV operator&(const ZBDDV& fv, const ZBDDV& gv)
 202   { ZBDDV hv; hv._zbdd = fv._zbdd & gv._zbdd; return hv; }
 203 inline ZBDDV operator+(const ZBDDV& fv, const ZBDDV& gv)
 204   { ZBDDV hv; hv._zbdd = fv._zbdd + gv._zbdd; return hv; }
 205 inline ZBDDV operator-(const ZBDDV& fv, const ZBDDV& gv)
 206   { ZBDDV hv; hv._zbdd = fv._zbdd - gv._zbdd; return hv; }
 207 inline int operator==(const ZBDDV& fv, const ZBDDV& gv)
 208   {  return fv.GetMetaZBDD() == gv.GetMetaZBDD(); }
 209 inline int operator!=(const ZBDDV& fv, const ZBDDV& gv)
 210   {  return !(fv == gv); }
 211
 212 inline ZBDDV& ZBDDV::operator<<=(int s)
 213   { return *this = *this << s; }
 214
 215 inline ZBDDV& ZBDDV::operator>>=(int s)
 216   { return *this = *this >> s; }
 217
 218 class ZBDD_Hash;
 219 class ZBDD_Hash
 220 {
 221   struct ZBDD_Entry
 222   {
 223     ZBDD _key;
 224     void* _ptr;
 225     ZBDD_Entry(void){ _key = -1; }
 226   };
 227
 228   bddword _amount;
 229   bddword _hashSize;
 230   ZBDD_Entry* _wheel;
 231
 232   ZBDD_Entry* GetEntry(ZBDD);
 233   void Enlarge(void);
 234 public:
 235   ZBDD_Hash(void);
 236   ~ZBDD_Hash(void);
 237   void Clear(void);
 238   void Enter(ZBDD, void *);
 239   void* Refer(ZBDD);
 240   bddword Amount(void);
 241 };
 242
 243 #endif // _ZBDD_