00001
00012 struct less_bdd : public binary_function<bdd, bdd, bool>
00013 {
00014 bool operator()(const bdd x, const bdd y) const { return lessbdd(x,y); }
00015
00016 bool lessbdd (const bdd x, const bdd y) const
00017 {
00018 if (x!=y)
00019 {
00020 if (x == bddfalse) return true;
00021 else if (y == bddfalse) return false;
00022 else if (( x & y ) == y) return true;
00023 else
00024 {
00025 if (bdd_var(x) < bdd_var(y)) return true;
00026 else
00027 {
00028 if ((bdd_low(x) != bddfalse) & (bdd_low(x) != bddtrue) & (bdd_high(x) != bddfalse) & (bdd_high(x) != bddtrue)
00029 & (bdd_low(y) != bddfalse) & (bdd_low(y) != bddtrue) & (bdd_high(y) != bddfalse) & (bdd_high(y) != bddtrue) )
00030 return (lessbdd(bdd_low(x), bdd_low(y)) & lessbdd(bdd_high(x), bdd_high(y)));
00031 else if ((bdd_low(x) == bddfalse) | (bdd_low(x) == bddtrue) | (bdd_high(x) == bddfalse) | (bdd_high(x) == bddtrue) )
00032 return true;
00033 else
00034 return false;
00035
00036 }
00037 }
00038 }
00039 else
00040 {
00041 return false;
00042 }
00043
00044 }
00045 };
00046
00047
00048 typedef set<bdd, less_bdd> FAMILY;
00049
00050
00055 inline FAMILY DOT(FAMILY f1, FAMILY f2)
00056 {
00057 bdd bdd_result;
00058 FAMILY family_result;
00059 FAMILY::iterator iF1,iF2;
00060 if (f1.empty() | f2.empty() ) return family_result;
00061 else
00062 {
00063 for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
00064 for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
00065 {
00066 if (model ==0) family_result.insert(setUnion(*iF1,*iF2));
00067 else family_result.insert(bagUnion(*iF1,*iF2));
00068 }
00069 return family_result;
00070 }
00071 return family_result;
00072 }
00073
00078 inline FAMILY PLUS(FAMILY f1, FAMILY f2)
00079 {
00080 FAMILY::iterator iF;
00081 FAMILY family_result;
00082 set_union(f1.begin(), f1.end(), f2.begin(), f2.end(), inserter(family_result, family_result.begin()), less_bdd());
00083 return family_result;
00084 }