/** 
* Product Family Algebra Module
* This module contains the functions that correspond to the DOT and PLUS	in Product Family Algebra.
* The module provides the upper set-layer. PFA is a set of sets for the set model and a set of bags in the bag model.
* This utilizes the STL library as a wrapper to the sets(bdds), or bags(bdds) in the lower level. 
*/



/**
 * This is a comparison function that works as an orderering relation between the upper level of sets. The sets of sets or the sets of bags. 
 */


// the best sor far is:

 struct less_bdd : public binary_function<bdd, bdd, bool> 
{
 	bool operator()(const bdd x,  const bdd y) const { return lessbdd(x,y); }

  bool lessbdd (const bdd x, const bdd y) const  
  {  
    if (x!=y) 
    { 
     if ( (x == bddfalse) | (x == bddtrue) ) return true;
     else if ((( x & y  ) == y)) return true;
     else if (bdd_var(x) < bdd_var(y)) return true;
     else if (bdd_var(x) == bdd_var(y) & (bdd_nodecount(x) < bdd_nodecount(y))) return true;
     else if ((bdd_low(x) != bddfalse) & (bdd_low(x) != bddtrue) & (bdd_high(x) != bddfalse) & (bdd_high(x) != bddtrue) 
              & (bdd_low(y) != bddfalse) & (bdd_low(y) != bddtrue) & (bdd_high(y) != bddfalse) & (bdd_high(y) != bddtrue)  )
             {
														 			return (lessbdd(bdd_low(x), bdd_low(y)) & lessbdd(bdd_high(x), bdd_high(y)));
             }
     //else if ( (((bdd_low(x) == bddfalse) | (bdd_low(x) == bddtrue)) & ( (bdd_high(x) == bddfalse) |  (bdd_high(x) == bddtrue)))   & (bdd_low(y) != bddfalse) & (bdd_low(y) != bddtrue) & (bdd_high(y) != bddfalse) & (bdd_high(y) != bddtrue))   return true;
					else
             return true;
    }
   else
							return false;
      
		}
};

// then this

 struct less_bdd : public binary_function<bdd, bdd, bool> 
{
 	bool operator()(const bdd x,  const bdd y) const { return lessbdd(x,y); }

  bool lessbdd (const bdd x, const bdd y) const  
  {  
    if (x!=y) 
    { 
     if (x == bddfalse) return true;
     else if (( x & y  ) == y) return true;
     else if (bdd_var(x) < bdd_var(y)) return true;
     else if ((bdd_low(x) != bddfalse) & (bdd_low(x) != bddtrue) & (bdd_high(x) != bddfalse) & (bdd_high(x) != bddtrue) 
              & (bdd_low(y) != bddfalse) & (bdd_low(y) != bddtrue) & (bdd_high(y) != bddfalse) & (bdd_high(y) != bddtrue)  )
             {
														 			return (lessbdd(bdd_low(x), bdd_low(y)) & lessbdd(bdd_high(x), bdd_high(y)));
             }
     else if ( (((bdd_low(x) == bddfalse) | (bdd_low(x) == bddtrue)) & ( (bdd_high(x) == bddfalse) |  (bdd_high(x) == bddtrue)))   & (bdd_low(y) != bddfalse) & (bdd_low(y) != bddtrue) & (bdd_high(y) != bddfalse) & (bdd_high(y) != bddtrue))
             return true;
     else
             return false;
    }
   else
							return true;
      
		}
};


// struct less_bdd : public binary_function<bdd, bdd, bool> 
//{
// 	bool operator()(const bdd x,  const bdd y) const { return lessbdd(x,y); }
//
//  bool lessbdd (const bdd x, const bdd y) const  
//  {  
//    if (x!=y) 
//    {
//     //out << "node count x = "<< bdd_nodecount(x) << endl;
//     //cout << "node count y = "<< bdd_nodecount(y) << endl;
//     if (bdd_nodecount(x) < bdd_nodecount(y))
//								return true;
//
//					else if (x == bddfalse)
//								return true;
//					else if (( x & y  ) == y)
//								return true;
//					else if ((bdd_low(x) != bddfalse) & (bdd_low(x) != bddtrue) & (bdd_high(x) != bddfalse) & (bdd_high(x) != bddtrue) 
//																		& (bdd_low(y) != bddfalse) & (bdd_low(y) != bddtrue) & (bdd_high(y) != bddfalse) & (bdd_high(y) != bddtrue)  )
//																	{
//                     if (bdd_var(x) < bdd_var(y))
//                        return true;
//																					else
//																					   return (lessbdd(bdd_low(x), bdd_low(y)) & lessbdd(bdd_high(x), bdd_high(y)));
//																	}
//     else
//								return false;
//									
//			}
//   else
//							return true;
//      
//		}
//};

typedef set<bdd, less_bdd> FAMILY;






/**
 * This is the DOT function on the upper level sets. Given two families, f1 and f2, it returns a new family which is the dot of the two orignal families.
*  the function behaves differently if we use the set model or the bag model. In the set model, we utilize the setUnion on sets (bdds) while in the bag model, we ultilize the bagUnion on bags(bdds).
*/ 
inline FAMILY DOT(FAMILY f1, FAMILY f2)
{  
   bdd bdd_result;
   FAMILY family_result;
   FAMILY::iterator iF1,iF2;
   if (f1.empty() | f2.empty()  ) return family_result;
   else 
   { 
		  for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ ) 
			    for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
       { 
         if (model ==0) family_result.insert(setUnion(*iF1,*iF2));  
         else           family_result.insert(bagUnion(*iF1,*iF2)); 
       }
     return family_result;
   }
			return family_result; 
}


int size(FAMILY F1)
{
			cout << F1.size() << endl;
   return F1.size();
}




/**
* This function is the PLUS funtion on the upper level sets. Given two families, f1 and f2, it returns a new family which is the plus of the two original familes.
* The plus is the union of the upper sets.  
*/ 
inline FAMILY PLUS(FAMILY f1, FAMILY f2)
{
			FAMILY::iterator iF1;
   FAMILY family_result;
   set_union(f1.begin(), f1.end(), f2.begin(), f2.end(),  inserter(family_result, family_result.begin()), less_bdd());
 		//cout <<"inside PLUS"<< endl;
 		//for (iF1 = family_result.begin(); iF1 != family_result.end(); iF1++ )
  	//    bdd_printdot(*iF1);
			    
   return family_result; 
}

void listProducts(FAMILY prod){  
     FAMILY::iterator iF1;
     cout << "[ " << endl;
     for (iF1 = prod.begin(); iF1 != prod.end(); iF1++ )
     {
									if (model==0)
												setEnumerate(*iF1);
									else
												bagEnumerate(*iF1);        

			  }
     cout << "]" << endl;
}




void listCommonality(FAMILY f){
					bdd tempIntersection;
     FAMILY common;
     FAMILY::iterator iF1,iF2; 
					
     for (int i = 1; i <=levels; i++)
									tempIntersection = (tempIntersection | bdd_ithvar(i));

					for (iF1 = f.begin(); iF1 != f.end(); iF1++ ) 
								for (iF2 = f.begin(); iF2 != f.end(); iF2++ )
								{ 
  										tempIntersection = setIntersection(tempIntersection,setIntersection(*iF1,*iF2));
 							}
					common.insert(tempIntersection);
					listProducts(common);
	}


bool isSubFamily(FAMILY f1, FAMILY f2)
{
   FAMILY::iterator iF1;
 		//return includes(f2.begin(),f2.end(),f1.begin(),f1.end(), less_bdd());
   bool found = false;
			for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
   {
							if (find(f2.begin(), f2.end(),*iF1) !=f2.end() )
          found = true;
       else
									{
										found = false;
          break;
									}
   }
		cout << "isSubFamily=" << found << endl;
  return found;
 
}



FAMILY powerSet(FAMILY f)
{
  FAMILY head, tail, emptySet;
  FAMILY::iterator iCurr, iF1;
  tail = f;
  emptySet.insert(bddfalse);

  if (f.empty()==true)
     return f;
		else
			{
					iCurr = tail.begin();
					head.insert(*iCurr);
					tail.erase(iCurr);
			}
			return PLUS(emptySet,PLUS(head,PLUS(powerSet(tail),DOT(head,powerSet(tail)))));
		}

bool refines(FAMILY F1, FAMILY F2)
{
    bool flag = false;
    FAMILY allFeatures,powSet, setMember;
    FAMILY::iterator iTer,iFAMILY; // remove iFamily later
				if (F1 == F2)  return true;

				//cout << "levels = " << levels << endl;
				for (int i = 1; i <=levels; i++)
    {
      allFeatures.insert(bdd_ithvar(i));
				}
    powSet = powerSet(allFeatures);
   
				iTer = powSet.begin();
    while ((flag != true) && (iTer!=powSet.end()))
    {
       setMember.insert(*iTer);
       if (isSubFamily(F1,DOT(F2,setMember)))
       {
							  	flag = true;
          break;
       }
       else
          {
										//cout << "ELSEEEE content of setMember of size: " <<  setMember.size() << endl;
										//for (iFAMILY = setMember.begin(); iFAMILY != setMember.end(); iFAMILY++ )
										//{
										//			bdd_printdot(*iFAMILY);
										//
										//}
												setMember.erase(*iTer);
										  iTer++;
          }

    }
    cout <<"refines= " << flag <<endl;
    return flag;
}
