/** 
* 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. 
 */

// OLD ORIGINAL COMPARATIOR - good for sets , 432
// 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 (y == bddfalse) return false;
//     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))); // fix this
//                else if ((bdd_low(x) == bddfalse) | (bdd_low(x) == bddtrue) | (bdd_high(x) == bddfalse) | (bdd_high(x) == bddtrue) )
//                        return true;
//                else 
//                        return false;
//                     
//             }
//           }     
//    }
//   else 
//   {
//    return false;
//   }
//   
//  }
//};


// BEST SO FAR, FOR BAGS
// 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 if ( ( ( (bdd_high(x) == bddfalse) |  (bdd_high(x) == bddtrue)))   &  ((bdd_high(y) != bddfalse) & (bdd_high(y) != bddtrue)))
//													return true;
//					else
//             return false;
//    }
//   else
//							return false;
//      
//		}
//};


// 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) 
//    { 
//       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)
//  //   return true;
//  //else if (((x==bddfalse) | (x==bddtrue) ) & ((y!=bddfalse) | (y!=bddtrue) ))
//  //   return true;
//  //else if ((x != bddfalse) & (y != bddfalse) & (x != bddtrue) & (y != bddtrue))
//  //     return (bdd_var(x) < bdd_var(y));
//  //else if (bdd_pathcount(x) <= bdd_pathcount(y))
//		//		return true;
//		//else
//		//		return false;
//		//cout << "x then y" << endl;
//		//bdd_printdot(x);
//		//bdd_printdot(y);
//
//  if (((x==bddfalse) | (x==bddtrue) ) & ((y!=bddfalse) | (y!=bddtrue) ))
//		   return true;
//  else if ((x != bddfalse) & (y != bddfalse) & (x != bddtrue) & (y != bddtrue))
//									 if ((bdd_var(x) < bdd_var(y))) return true;
//          else if ((( x & y  ) == y))
//																			if ((( x & y  ) == x))
//																			    return false;
//																			else
//                       return true;
//									//else if (lessbdd(bdd_high(x), bdd_high(y))) return true;
//									//	else if  ((bdd_var(x) != bdd_var(y)))
//									//					{
//									//							if (bdd_pathcount(x) < bdd_pathcount(y)) return true;
//									//							if (bdd_nodecount(x) < bdd_nodecount(y)) return true;
//									//					}
//									// else
//									//				 {
//									//							if (bdd_pathcount(x) < bdd_pathcount(y)) return true;
//									//							if (bdd_nodecount(x) < bdd_nodecount(y)) return true;
//									set of bdds//					}
//									else
//														{
//																//if (bdd_pathcount(x) < bdd_pathcount(y)) return true; -- long !
//																if ((bdd_nodecount(x) < bdd_nodecount(y))) // | (bdd_nodecount(x) > bdd_nodecount(y)))
//																			return true;
//
//														}       
//													
//  else return false;      
//		}
//};



// 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) return true;
//    else return false; 
//     
//		}
//};

//long rankBdd(bdd const x) - limited by the data type size
//{
//  long rank, numOfNodes, sumOfNodeNumLabels;
//  numOfNodes = 100000 * bdd_nodecount (x);
//  //cout << "number of nodes= " << numOfNodes << endl;
//  sumOfNodeNumLabels = 10000;
//  if (x == bddfalse) return 0;
//  else
//  { 
//      if (model == 0 )
//         for (int i = 1; i <= levels; i++)  
//              {
//                if (existsInSet(bdd_ithvar(i), x))
//                   sumOfNodeNumLabels = sumOfNodeNumLabels + i;
//                //cout << "nodenumlabels = " << sumOfNodeNumLabels  << endl; 
//              }
//      else if (model==1)
//              for (int i = 1; i <= levels; i++) 
//                  {  
//                     if ( (getOcc(bdd_ithvar(i), x)>0) )
//                         {
//                           sumOfNodeNumLabels = sumOfNodeNumLabels + i  + getOcc(bdd_ithvar(i), x);
//                         }
//
//                  }
//
//
//      else // other models
//           cout << "Other Models are not implemented." << endl;
//  }
//  //bdd_printdot(x);
//  //cout << "rank of bdd = " << (numOfNodes + (sumOfNodeNumLabels) ) << endl;
//  return (numOfNodes + (sumOfNodeNumLabels) );
//
//}



// ranking bdds , returning arrays. Works with less_bdd of rank array version. 
void rankBdd(int rank[], bdd const x)
{
  //cout << "in rank: levels = " << levels << endl;
  //int* rank = new int[levels]; // new
  for (int i = 1; i <= levels; i++)
      rank[i] = 0;

  if ((x == bddfalse) or (x == bddtrue)) ; //return rank;
  else
  { 
      if (model == 0 )
         for (int i = 1; i <= levels; i++)  
              {
                if (existsInSet(bdd_ithvar(i), x))
                   rank[i] = 1;
                else
                   rank[i] = 0;
                //cout << "rank of node at i = " << i << " is "<< rank[i]  << endl; 
              }
      else if (model==1)
              for (int i = 1; i <= levels; i++) 
                  {  
                     if ( (getOcc(bdd_ithvar(i), x)>0) )
                         {
                           rank[i] = getOcc(bdd_ithvar(i), x);
                         }
                     else
                         rank[i] = 0;
                     //cout << "rank of node at i = " << i << " is "<< rank[i]  << endl; 

                  }


      else // other models
           cout << "Other Models are not implemented." << endl;
  }
  //cout << "rank of current bdd: " << (numOfNodes + sumOfNodeNumLabels + bdd_var(x)) << endl;
  //cout << " ---- " << endl;
  //return rank;

}



//long double rankBdd(bdd const x)
//{
// 
//  long max_occ = powr(2,occ_bitsize);
//  long double ranking = 0;
//  if (x == bddfalse) return 0;
//  else
//  { 
//      if (model == 0 )
//         for (int i = 1; i <= levels; i++)  
//              {
//                if (existsInSet(bdd_ithvar(i), x))
//                   ranking = ranking + powr(2,(i-1));
//              }
//      else if (model==1)
//              for (int i = 1; i <= levels; i++) 
//                  {  
//                     if ( (getOcc(bdd_ithvar(i), x)>0) )
//                         {
//                           ranking = ranking + ( getOcc(bdd_ithvar(i), x) * powr(max_occ,i-1) );
//                         }
//
//                  }y
//
//
//      else // other models
//           cout << "Other Models are not implemented." << endl;
//  }
//  //cout << "rank of current bdd: " << ranking << endl;
//  return ranking;
//
//}




// 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 (model == 0)
//        {
//          if (setIsMember(x,y) &&  x!=y) return true;
//          else
//             {
//               if ((x!=y)>0) return true;
//               else return false;
//             } 
//          
//        }
//     else
//       {
//          if (setIsMember(x,y) &&  x!=y) return true;
//          else
//             {
//               if ((x!=y)>0) return true;
//               else return false; 
//             } 
//
//       }
//     
//		}
//};


// this compmarator works with rank bdd as array of ranks of x and y. This will not work with large specs (works with ess, not robots), memory problems. It will also duplicate for the case of w.

 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  
    {
     int rankX[levels];
     int rankY[levels];
     //cout << "levels: " << levels <<  endl; 
     bool less = false;
     if ((x==bddfalse) and (y!=bddfalse)) return true;
     else if ((x==bddfalse) and (y==bddfalse)) return false;
     else if ((x!=bddfalse) and (y==bddfalse)) return false;
     else if ((x!=bddfalse) and (y!=bddfalse))
      {
         //int* rankX = rankBdd(x);
         //int* rankY = rankBdd(y);
        rankBdd(rankX,x);
        rankBdd(rankY,y);

        //cout << "-------------------" << endl; 
        //bdd_printdot(x);
        //cout << "rank x= " << rankBdd(x) << endl;
        //cout << "+++++" << endl; 
        //bdd_printdot(y);
        //cout << "rank y= " << rankBdd(y) << endl;
        //cout << "----------------" << endl;
        for (int i=1; i<=levels; i++)
            {
              //cout << "at i = " << i << "  rankX = " << rankX[i] << "  and rankY = " << rankY[i] << endl;
              if (rankX[i] < rankY[i])
                 {
                   //cout << "LESS at i= " << i << "   r(x) = " <<  rankX[i] << "   r(y)= " << rankY[i] << endl;
                   less =  true;
                   break;
                 }
              else if (rankX[i] == rankY[i])
                 {
                   //cout << "EQUAL at i= " << i << "   r(x) = " <<  rankX[i] << "   r(y)= " << rankY[i] << endl;
                   continue;
                 }
              else // >
                 {
                   //cout << "GREATER at i= " << i << "   r(x) = " <<  rankX[i] << "   r(y)= " << rankY[i] << endl;
                   less = false;
                   break;
                 } 
                       
                
            }
        //delete[] rankX;
       //delete[] rankY; 
      }
     else less = false;
   //if (x!=y) return true;
   //else return false;

     return less; 
    }
};

// data type less bdd
//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==bddfalse) and (y!=bddfalse)) return true;
//     else if ((x==bddfalse) and (y==bddfalse)) return false;
//     else if ((x!=bddfalse) and (y==bddfalse)) return false;
//     else if ((x!=bddfalse) and (y!=bddfalse))
//      {
//
//        //cout << "-------------------" << endl; 
//        //bdd_printdot(x);
//        //cout << "rank x= " << rankBdd(x) << endl;
//        //cout << "+++++" << endl; 
//        //bdd_printdot(y);
//        //cout << "rank y= " << rankBdd(y) << endl;
//        for (int i=1; i<=levels; i++)
//            {
//              //cout << "at i = " << i << "  rankX = " << rankX[i] << "  and rankY = " << rankY[i] << endl;
//              if (rankBdd(x) < rankBdd(y))
//                 return true;
//                       
//                
//            }
//     }
//     else return false;
//    }
//};


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).
*/ 
FAMILY DOT(FAMILY const &f1, FAMILY const &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; //malabbad
	//cout << "\033[1;31mbold red text\033[0m\n"<< endl;;
   return F1.size();
}
void SIZE(FAMILY F1)
{
	cout << size(F1) << endl;
}

int sizeInternal(FAMILY F1)
{
   return F1.size();
}



bool isEqual (FAMILY f1, FAMILY f2)
{ bool equal = false;
  FAMILY::iterator iF1,iF2;

  if (sizeInternal(f1) != sizeInternal(f2))
      equal = false;
  else if ((sizeInternal(f1) == 0) &  (sizeInternal(f2) == 0))
     equal = true;
  else if ((sizeInternal(f1) == 0) |  (sizeInternal(f2) == 0))
     equal = false;
  else // ((sizeInternal(f1) >  0) &  (sizeInternal(f2) > 0))
     {
       for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
          {  if (model ==0)
             for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
          							if (find(f2.begin(), f2.end(),*iF1) !=f2.end() )
                    {
                      equal = true;
                    }
                 else
       									    {
       										     equal = false;
                      break;
       									    }

             else if (model == 1)
                     {
                       for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
                           if (bagEqualOcc(*iF1,*iF2) == true)
                              equal = equal | true;
                           else
                               {
                                equal = equal | false;
                               } 
                        
                     }
             else
                     {
                      cout << "Sorry, other models are not implemented." << endl;
                  
                     } 
          }
       // the other way around
       for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
          {  if (model ==0)
             for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
          							if (find(f1.begin(), f1.end(),*iF2) !=f1.end() )
                    {
                      equal = true;
                    }
                 else
       									    {
       										     equal = false;
                      break;
       									    }

             else if (model == 1)
                     {
                       for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
                           if (bagEqualOcc(*iF1,*iF2) == true)
                              equal = equal | true;
                           else
                               {
                                equal = equal | false;
                               } 
                        
                     }
             else
                     {
                      cout << "Sorry, other models are not implemented." << endl;
                  
                     } 
          }

     }
  // if (equal == true)
  //    cout << "isEqual? Yes." << endl;
  // else
  //    cout << "isEqual? No." << endl;
}
void ISEQUAL (FAMILY f1, FAMILY f2)
{
	if (isEqual(f1,f2) == true)
      cout << "Yes" << endl;
   else
      cout << "No" << endl;
}

bool isEqualInternal (FAMILY f1, FAMILY f2)
{ bool equal = false;
  FAMILY::iterator iF1,iF2;

  if (sizeInternal(f1) != sizeInternal(f2))
      equal = false;
  else if ((sizeInternal(f1) == 0) &  (sizeInternal(f2) == 0))
     equal = true;
  else if ((sizeInternal(f1) == 0) |  (sizeInternal(f2) == 0))
     equal = false;
  else // ((sizeInternal(f1) >  0) &  (sizeInternal(f2) > 0))
     {
       for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
          {  if (model ==0)
             for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
          							if (find(f2.begin(), f2.end(),*iF1) !=f2.end() )
                    {
                      equal = true;
                    }
                 else
       									    {
       										     equal = false;
                      break;
       									    }

             else if (model == 1)
                     {
                       for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
                           if (bagEqualOcc(*iF1,*iF2) == true)
                              equal = equal | true;
                           else
                               {
                                equal = equal | false;
                               } 
                        
                     }
             else
                     {
                      cout << "Sorry, other models are not implemented." << endl;
                  
                     } 
          }
       // the other way around
       for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
          {  if (model ==0)
             for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
          							if (find(f1.begin(), f1.end(),*iF2) !=f1.end() )
                    {
                      equal = true;
                    }
                 else
       									    {
       										     equal = false;
                      break;
       									    }

             else if (model == 1)
                     {
                       for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
                           if (bagEqualOcc(*iF1,*iF2) == true)
                              equal = equal | true;
                           else
                               {
                                equal = equal | false;
                               } 
                        
                     }
             else
                     {
                      cout << "Sorry, other models are not implemented." << endl;
                  
                     } 
          }

     }
  return equal;
}

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;
}

/**
* 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.  
*/ 
//FAMILY PLUS(FAMILY const &f1, FAMILY const &f2)
//{
//			FAMILY::iterator iF1, iF2;
//   FAMILY family_result;
//   //insert_iterator<set<bdd, less_bdd > >  res_ins(family_result, family_result.begin());
//   set_union(f1.begin(), f1.end(), f2.begin(), f2.end(),  inserter(family_result, family_result.end()), less_bdd());
//   //set_union(f1.begin(), f1.end(), f2.begin(), f2.end(), res_ins, less_bdd());
//   //cout << "size of f1 =" << f1.size() << endl;
//   //cout << "size of f2 =" << f2.size() << endl;
//   //for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
//   //  {
//   //    family_result.insert(*iF1);
//   //  }
//   //cout << " contents of f1 " << endl;
////  for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
////    {
////      //bdd_printdot(*iF1);
////        family_result.insert(*iF1);
////    }
//////cout << " contents of f2 " << endl;
////  for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
////    {
////      //bdd_printdot(*iF2);
////        family_result.insert(*iF2);
////    }
//   //iF1 = f1.end();
//   //iF2 = f2.end();
//   //iF1++;
//   //iF2+1;
//   //family_result.insert(f1.begin(),f1.end()); //good ones ~~ fastest
//	  //family_result.insert(f2.begin(), f2.end());
//   //merge(f1.begin(), f1.end(), f2.begin(), f2.end(), insert_iterator(family_result, family_result.end()), less_bdd());
//   //family_result.insert(f2.upper_bound());
//  //for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
//  //  {
//  //   family_result.insert(*iF2);
//  // }
// 		//cout <<"inside PLUS"<< endl;
// 		//for (iF1 = family_result.begin(); iF1 != family_result.end(); iF1++ )
//  	//    bdd_printdot(*iF1);
//   //family_result = f1;
////  iF1 = f1.begin();
////  iF2 = f2.begin();
////  while (iF1 != f1.end())
////  {  cout << "rankBDD F1 " << rankBdd(*iF1) << endl;
////    while (iF2 != f2.end())
////    { cout << "rankBDD F2 " << rankBdd(*iF2) << endl;
////      if (*iF1 == *iF2)
////         {
////            family_result.insert(*iF1);
////            iF1++;
////            iF2++;
////         }
////      else if (rankBdd(*iF1) < rankBdd(*iF2))
////         {  
////            family_result.insert(*iF1);
////            iF1++;
////         }
////      else // (rankBdd(*iF1) > rankBdd(*iF2))
////         {   
////            family_result.insert(*iF2);
////            iF2++;
////         }
////    }
////    family_result.insert(*iF1);
////    iF1++;
////
////  }
//// while (iF2 != f2.end())
//// {
////    family_result.insert(*iF2);
////    iF2++;
//// }
//
////family_result = family_result.insert(f2.begin(),f2.end())
//return family_result; 
//}


FAMILY PLUS(FAMILY const &f1, FAMILY const &f2)
{       FAMILY::iterator iF1, iF2;
        FAMILY family_result, temp_result;
  for (iF1 = f1.begin(); iF1 != f1.end(); iF1++)
   family_result.insert(*iF1);
  for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
   {
       bool eqlflag=0;
      for (iF1 =   f1.begin(); iF1 != f1.end(); iF1++ )
      {
       if (model == 0 )
        {
         if(*iF1 == *iF2)
         {
        //     cout<<" equle"<<endl;
             eqlflag=1;
             break;
          }
         }
      else if (model==1)
        {bool bageqlflag=1;
         for (int k = 1; k <= levels; k++) 
          {  
               if ( (getOcc(bdd_ithvar(k), (*iF1))) != (getOcc(bdd_ithvar(k), (*iF2))))
               {
               bageqlflag=0;
               break;
                }
          }
          if(bageqlflag==1)
          {
            //  cout<<" equle"<<endl;
              eqlflag=1;
              break;
           }
         }    
    }
    if(eqlflag!=1) family_result.insert(*iF2);
}
 
   return family_result; 
}



void listCommonality(FAMILY f){
					bdd tempIntersection;
     FAMILY common;
     FAMILY::iterator iF1,iF2;

     if (sizeInternal(f) == 0)
        tempIntersection = bddfalse;
     else // (sizeInternal(f) >  0) 
     {
        if (model == 0)
        {
            for (int i = 1; i <=levels; i++)
                tempIntersection = (tempIntersection | bdd_ithvar(i));

            //bdd_printdot(tempIntersection);

            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);
         }
         else if (model == 1)
         {  
            for (int i = 1; i <=levels; i++)
            {
                tempIntersection = (tempIntersection | setOcc(i,powr(2,occ_bitsize)-1, bdd_ithvar(i)));
            }
            //bdd_printdot(tempIntersection);
            for (iF1 = f.begin(); iF1 != f.end(); iF1++ ) 
               for (iF2 = f.begin(); iF2 != f.end(); iF2++ )
               {
                   tempIntersection = bagIntersection(tempIntersection,bagIntersection(*iF1,*iF2));
               }
            common.insert(tempIntersection);

         }
         else
         {
           common.insert(bddfalse);
           cout << "This function is not implemented for other models" << endl;
         }
     }
					listProducts(common);
	}


//bool isSubFamily(FAMILY f1, FAMILY f2)
//{
//   FAMILY::iterator iF1, iF2;
// 		//return includes(f2.begin(),f2.end(),f1.begin(),f1.end(), less_bdd());
//   //if (includes(f2.begin(),f2.end(),f1.begin(),f1.end(), less_bdd())) cout << "Second includes First !" << endl;
//   //else cout << "Second does not include First !" << endl;
//   bool found = false;
//
//
//			for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ )
//   {  if (model ==0)
//      for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
//   							if (find(f2.begin(), f2.end(),*iF1) !=f2.end() )
//             {
//               found = true;
//             }
//          else
//									    {
//										     found = false;
//               break;
//									    }
//      else if (model == 1)
//              {
//                for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ )
//                    if (bagNumOccLess(*iF1,*iF2) == true)
//                       found = found | true;
//                    else
//                        {
//                         found = found | false;
//                        } 
//                 
//              }
//      else
//              {
//               cout << "Sorry, other models are not implemented." << endl;
//           
//              } 
//   }
//  if (found == true)
//     cout << "is SubFamily? Yes." << endl;
//  else
//     cout << "is SubFamily? No." << endl;
//     
//  return found;
// 
//}

bool isSubFamily(FAMILY f1, FAMILY f2)
{
   bool found = false;
   if (isEqualInternal(PLUS(f1,f2),f2))
      found = true;

   //if (found == true)
   //   cout << "is SubFamily? Yes." << endl;
   //else
   //   cout << "is SubFamily? No." << endl;
}
void ISSUBFAMILY(FAMILY f1, FAMILY f2)
{
	if (isSubFamily(f1,f2) == true)
      cout << "Yes" << endl;
   else
      cout << "No" << endl;
}

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 = true;
    bool internalFlag, occFlag;
    FAMILY allFeatures;
    FAMILY::iterator iF1,iF2;
    int levels;
    levels = number_of_vars-occ_bitsize;
				//if (F1 == F2)  flag = true;
    if (model==0)
    {
       
      for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ ) // k
          { internalFlag = false;  
            for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ ) // j
                {  
                   internalFlag = internalFlag | existsInSet(*iF2 , *iF1);
                   //cout << " second divides first "  << existsInSet(*iF2,*iF1) << endl;
                   if (internalFlag == true) break;
                }
                flag = flag & internalFlag;
                if (flag == false) break;
          }

    }
    else if (model==1)
    {
      
      for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ ) // k
          { internalFlag = false;  
            for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ ) // j
                {  
                   internalFlag = internalFlag | existsInSet(bag2set(*iF2) , bag2set(*iF1));
                   //cout << " second divides first "  << existsInSet(bag2set(*iF2) , bag2set(*iF1)) << endl;
                   if (internalFlag == true) break;
                }
                flag = flag & internalFlag;
                if (flag == false) break;
          }
      // now check the occurances. The occurances in the first should be greater than or equal to the occurances in the second
      if (flag == true )
      {  //cout << "as sets, it refines, now checking occurances " << endl;
         for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ ) // o2
          {
             for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ ) // o
                 { internalFlag = false;
                   for (int i = 1; i <= levels; i++)
                       {  occFlag = true;
                          if (getOcc(bdd_ithvar(i),*iF1) < getOcc(bdd_ithvar(i),*iF2))
                             {
                                occFlag = false;
                                break;
                             }

                       }
                   internalFlag = internalFlag | occFlag;

                   if (internalFlag == true)
                     {
                      break;
                     }
                 }
             flag = flag & internalFlag ;
             if (flag == false)
                break;
          }
      }
      
    }
    else
    {
      cout << "the other models are not implemented yet.";
    }
        

	//		 if (flag == true )
    //   cout <<"refines? Yes."  << endl;
    //else
    //    cout <<"refines? No."  << endl;
    return flag;
}

void REFINES(FAMILY f1, FAMILY f2)
{
	if (refines(f1,f2) == true )
       cout <<"Yes"  << endl;
    else
        cout <<"No"  << endl;
}

bool refinesInternal(FAMILY f1, FAMILY f2)
{
    bool flag = true;
    bool internalFlag, occFlag;
    FAMILY allFeatures;
    FAMILY::iterator iF1,iF2;
    int levels;
    levels = number_of_vars-occ_bitsize;
				//if (F1 == F2)  flag = true;
    if (model==0)
    {
       
      for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ ) // k
          { internalFlag = false;  
            for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ ) // j
                {  
                   internalFlag = internalFlag | existsInSet(*iF2 , *iF1);
                   //cout << " second divides first "  << existsInSet(*iF2,*iF1) << endl;
                   if (internalFlag == true) break;
                }
                flag = flag & internalFlag;
                if (flag == false) break;
          }

    }
    else if (model==1)
    {
      
      for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ ) // k
          { internalFlag = false;  
            for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ ) // j
                {  
                   internalFlag = internalFlag | existsInSet(bag2set(*iF2) , bag2set(*iF1));
                   //cout << " second divides first "  << existsInSet(bag2set(*iF2) , bag2set(*iF1)) << endl;
                   if (internalFlag == true) break;
                }
                flag = flag & internalFlag;
                if (flag == false) break;
          }
      // now check the occurances. The occurances in the first should be greater than or equal to the occurances in the second
      if (flag == true )
      {  //cout << "as sets, it refines, now checking occurances " << endl;
         for (iF1 = f1.begin(); iF1 != f1.end(); iF1++ ) // o2
          {
             for (iF2 = f2.begin(); iF2 != f2.end(); iF2++ ) // o
                 { internalFlag = false;
                   for (int i = 1; i <= levels; i++)
                       {  occFlag = true;
                          if (getOcc(bdd_ithvar(i),*iF1) < getOcc(bdd_ithvar(i),*iF2))
                             {
                                occFlag = false;
                                break;
                             }

                       }
                   internalFlag = internalFlag | occFlag;

                   if (internalFlag == true)
                     {
                      break;
                     }
                 }
             flag = flag & internalFlag ;
             if (flag == false)
                break;
          }
      }
      
    }
    else
    {
      cout << "the other models are not implemented yet.";
    }
        

			 
    return flag;
}

// The old refines using power set, this works for set model. For bag model, the nested loops !!!!

//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 ((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;
//}

//FAMILY APPLYCONSTRAINT (FAMILY const &p, FAMILY &a, FAMILY &b)
FAMILY APPLYCONSTRAINT (FAMILY const &p, FAMILY const &a, FAMILY const &b) // added const to a and b 
{
 bdd bdd_result;
 FAMILY family_result, curr_p, curr_p2,curr_a, curr_b;
 FAMILY::iterator iP, iP2,iA,iB;

 //if (sizeInternal(p) == 1)
 //{ 
   for (iP = p.begin(); iP != p.end(); iP++ )
   {    
        curr_p.insert(*iP);
        //for (iA = a.begin(); iA != a.end(); iA++ )
        // {
        //   curr_a.insert(*iA);
           //for (iB = b.begin(); iB != b.end(); iB++ )
           //{
           //  curr_a.insert(*iB);
             if (not(refinesInternal(curr_p,a)) or (refinesInternal(curr_p,b)))
               {
                  family_result.insert(*iP);
               }
             curr_p.erase(*iP);     
           //}
        //}
        
   }
//}
//else if (sizeInternal(p) > 1)
//{
//   for (iP = p.begin(); iP != p.end(); iP++ )
//   {   curr_p.insert(*iP);
//       for (iP2 = p.begin(); iP2 != p.end(); iP2++ )
//       {   curr_p2.insert(*iP2); 
//             if ( (not(refinesInternal(curr_p,a)) or (refinesInternal(curr_p,b))) and (not(refinesInternal(curr_p2,a)) or (refinesInternal(curr_p2,b))) )
//             {
//                  family_result.insert(*iP);
//                  family_result.insert(*iP2);
//               }
//       }
//    }
//}
  
//else
//    ;
    
return family_result;
}
