- Main Page
- Classes
- Files

- File List
- File Members

# pfa.h

Go to the documentation of this file.

    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))); // fix this
    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 }