#include <stdlib.h>
#include <stdlib.h>
#include <bdd.h>
#include <bvec.h>
#include <cmath>
#include <iostream>
#include <bitset>
#include <set>
#include <algorithm>  
#include "ConfigFile.h"
#include "loadme.h"
#include "bag.h"
#include "set.h"
#include "bag.cpp"
#include "set.cpp"
#include "setbag.h"
#include "pfa.h"
#include <iterator>
#include <utility>

using namespace std;



int main()
{


bdd_init(10000,1000);
bdd_setvarnum(1500);
// read configuration from a file.

ConfigFile config("config.inp"); // remember, this is where the values are set.
config.readInto( number_of_vars, "number_of_vars" );
config.readInto( model, "model");
config.readInto( occ_bitsize, "occ_bitsize");
//cout << "number variables is " << number_of_vars << endl;
//cout << "our model is " << model << endl;
//cout << "occ_bitsize is " << occ_bitsize << endl;
levels = number_of_vars - occ_bitsize;

cout << "Greetings  -------------------------------------------------------------  Started"<< endl;
#include "families.h"  // brings all the defined families


bdd zero = bddfalse;

FAMILY zeroSet;
FAMILY oneSet;
oneSet.insert(bddfalse);

FAMILY::iterator iFAMILY;




// TESTING ESS EXAMPLE HERE IN STL CODE:
FAMILY commonality, A, B, C, D, E, F, F1, F2, F3, F4, F5, F6, F7, F8, F9, internet_intranet_enabled_ess, ess_basic_personal_tasks, ess_time_and_attendance_tasks, ess_payroll_and_benifits_tasks, employee_self_service,  ESS; 
FAMILY G, H, I, J, K, L, M, N, O, P;

bdd comm = a1 & b1 & c1 & d1 & e1 & f1;  // commonality from 1 to 6
//bdd a1TEST = a1;
//bdd a1TEST2 = setOcc(1,4, comm);  // for testing the bag model
bdd a1TEST2 = a1;
//cout << "a1TEST1 and then a1TEST2 in main ======" <<endl;
//bdd_printdot(a1TEST);
//bdd_printdot(a1TEST2);

//cout << "the number of occurances of a1 in a1TEST2 is:" << getOcc(a1,a1TEST2)  << endl;
//a1TEST2 = setOcc(2,7,a1TEST2);
//cout << "the number of occurances of b1 in a1TEST2 is:" << getOcc(b1,a1TEST2)  << endl;

commonality.insert(comm);

//setIsMember(a1TEST2,a1TEST2 & b1);
//// to avoid the bdd unkonwn error, I convert sets to bags and see
// our example is DOT(A,B)
a1TEST2 = set2bag(a1);
a1TEST2 = setOcc(1,6,a1TEST2);
//a1TEST2 = setOcc(7,7,a1TEST2);
bdd_printdot(a1TEST2);
cout << "the occurances of a1 in a1TEST2 = " << getOcc(a1,a1TEST2) << endl; 
//cout << "the occurances of g1 in a1TEST2 = " << getOcc(g1,a1TEST2) << endl; 
a1TEST2 = bag2set(a1TEST2);
cout << "bag2set of a1TEST2 = " << endl; 
bdd_printdot(a1TEST2);
//b1 = set2bag(b1);

//A.insert(a1);
A.insert(a1);
B.insert(b1);
B.insert(a1); //remove, just for testing list commonality
C.insert(c1);
D.insert(d1);
E.insert(e1);
F.insert(f1);
G.insert(g1); // 7
H.insert(h1); // 8
I.insert(i1); // 9
J.insert(j1); // 10
K.insert(k1); // 11
L.insert(l1); // 12 
M.insert(m1); // 13
N.insert(n1); // 14
O.insert(o1); // 15
P.insert(p1); // 17

F1 = PLUS(oneSet, G);
F2 = PLUS(oneSet, H);
F3 = PLUS(oneSet, I);
F4 = PLUS(oneSet, J);
F5 = PLUS(oneSet, K);
F6 = PLUS(oneSet, L);
F7 = PLUS(oneSet, M);
F8 = PLUS(oneSet, N);
F9 = PLUS(O,P);


// TESTING SET OCCURANCE AND GET OCCURANCE : BEING

//bdd wow = setOcc(1, 3, a1);
//bdd wew = setOcc(2, 5, comm);

//bdd_printdot(wow);

//bdd bit1 = bdd_ithvar(17);
//bdd bit2 = bdd_ithvar(18);
//bdd bit3 = bdd_ithvar(19);

//bdd wow = setOcc(1,4,comm);
//bdd_printdot(wow);
//cout << "the occurance of a1 in wow = " << getOcc(a1,wow) << endl;



//bdd_printdot(comm);


// TESTING SET OCCURANCE AND GET OCCURANCE : END

//ESS = dot(commonality, dot(F1, dot(F2, dot(F3, dot(F4, dot(F5, dot(F6, dot(F7, dot(F8, F9)))))))));
// Experimenting step by step:
//ESS = dot(commonality,dot(F8,F9));

// ESS = dot(G,plss(oneSet, H)); worked perfect
//cout << "The size of the ESS family is: " << ESS.size() << endl;
//cout << "The contents of the ESS family is: " << endl;
//for (iFAMILY = ESS.begin(); iFAMILY != ESS.end(); iFAMILY++ )  bdd_printdot(*iFAMILY); 
//set_union(s1.begin(), s1.end(), s2.begin(), s2.end(), collect.begin());

// The example from the Haskell prototype:


internet_intranet_enabled_ess = DOT(A, B);

ess_basic_personal_tasks = DOT(C, DOT(D, DOT(E, F)));

ess_time_and_attendance_tasks = DOT(F1, DOT(F2, DOT(PLUS(oneSet, DOT(I, F4)), PLUS(oneSet, DOT(K, F6)))));

ess_payroll_and_benifits_tasks = DOT(F8, PLUS(oneSet, PLUS(O,P)));

employee_self_service = DOT(internet_intranet_enabled_ess, DOT(ess_basic_personal_tasks, DOT(ess_time_and_attendance_tasks, DOT(PLUS(oneSet, M), ess_payroll_and_benifits_tasks))));


cout << "The size of the <employee_self_service> family is: " << employee_self_service.size() << endl;
//cout << "The contents of the ESS family is: " << endl;
//for (iFAMILY = ESS.begin(); iFAMILY != ESS.end(); iFAMILY++ )  bdd_printdot(*iFAMILY); 
cout << "The size of commonality is : " << size(commonality) << endl;
cout << "The size of A is : " << size(A) << endl;
listProducts(A);
cout << "The size of F1 is : " << size(F1) << endl;
listProducts(F1);
cout << "The size of B is : " << size(B) << endl;
listProducts(B);
cout << "listing the commonality in internet_intranet_enabled_ess " << endl;
listCommonality(internet_intranet_enabled_ess);

cout << "A is a subset of B?" << isSubFamily(A,C) << endl;


bdd_done();



}

