#include "BDD.h"
#include "PLAtab.h"
#include <cmath>
#include <fstream>

unsigned int pairF(unsigned int i, unsigned int j);
int  operaceOR(Node * u1, Node * u2);
int operaceAND(Node * u1, Node * u2);
int operaceXOR(Node * u1, Node * u2);

/******************************************************************************/
/* --- konstruktor BDD --- */
/* --- vytvari terminalni uzly 0 a 1 --- */

BDD::BDD(int var) {
        varCt = var;
        root = NULL;
        zeroT = new Term(TERM_VAR_ID,0);
        oneT  = new Term(TERM_VAR_ID,1);
        arrayLevel = NULL;

}
/******************************************************************************/
/* --- kopirujici konstruktor BDD --- */
/* --- pouziva Mapu_uzlu m_u --- */
/* --- alokuje pamet pro pole urovni arrayLevel --- */
/* --- vyuziva funkci rec_copy, ktera vrati koren noveho BDD --- */

BDD :: BDD(BDD & src){
 Mapa_uzlu m_u;
 varCt = src.varCt;
 zeroT = new Term(TERM_VAR_ID,0);
 oneT  = new Term(TERM_VAR_ID,1);
 arrayLevel = new NodeList[varCt];
 root = rec_copy(src.root,this,&m_u);

}

/******************************************************************************/
/* --- pretizeny operator prirazeni pro BDD --- */
/* --- smaze vsechny uzly vcetne terminalu a vytvori nove BDD --- */
/* --- vola se del_nodes ktera smaze vsechny uzly v BDD --- */

BDD BDD::operator=(BDD  &src){

Mapa_uzlu m_u;

delete oneT;
delete zeroT;
del_nodes();
delete [] arrayLevel;
/* --- uklizeno --- */

varCt = src.varCt;
zeroT = new Term(TERM_VAR_ID, 0);
oneT  = new Term(TERM_VAR_ID, 1);
arrayLevel = new NodeList[src.varCt];
root = rec_copy(src.root, this, &m_u);

return *this;
}
/******************************************************************************/
/* --- funkce pro nacteni BDD z uplne pravdivostni tabulky predstavovane zde polem tt --- */

BDD::BDD(int *tt,int n) {

        zeroT = new Term(TERM_VAR_ID,0);
        oneT = new Term(TERM_VAR_ID,1);
        arrayLevel = new NodeList[n];

        Node **array;
        //int number_node;
        varCt = n;
        int number_vertices = (int)pow((double)2,n+1);
        array = new Node*[number_vertices];

        //koren
        array[0] = new Node(0);
        arrayLevel[0].push_back(array[0]);
        // promena(uroven) 2 az n
        for(int i=1;i<n;i++) {
                for(int j=0;j<pow((double)2,i);j++) {
                        array[(int)pow((double)2,i)+j-1] = new Node(i);
                        arrayLevel[i].push_back(array[(int)pow((double)2,i)+j-1]);
                }
        }

        // terminalni uroven
        for(int j=0;j<pow((double)2,n);j++) {
                if(tt[j]==0) array[(int)pow((double)2,n)+j-1] = zeroT;
                        else array[(int)pow((double)2,n)+j-1] = oneT;
        }

        // vytvoreni stromu
        for(int i=0;i<n;i++) {
                for(int j=0;j<pow((double)2,i);j++) {
                        array[(int)pow((double)2,i)+j-1]->Low = array[2*((int)pow((double)2,i)+j)-1];
                        array[2*((int)pow((double)2,i)+j)-1]->parentList.push_back(array[(int)pow((double)2,i)+j-1]);

                        array[(int)pow((double)2,i)+j-1]->High = array[2*((int)pow((double)2,i)+j)];
                        array[2*((int)pow((double)2,i)+j)]->parentList.push_back(array[(int)pow((double)2,i)+j-1]);
                }
        }


        root=array[0];
        root->parentList.push_back(array[0]);

}
/******************************************************************************/
/* --- destruktor BDD --- */
/* --- pro smazani vsech uzlu se vola del_nodes --- */

     BDD :: ~BDD(){
if(arrayLevel!=NULL)
  {
   del_nodes();
   delete [] arrayLevel;
   delete oneT;
   delete zeroT;
  }
}

/******************************************************************************/
/* --- funkce ktera smaze vsechny uzly z jednotlivych urovni v arrayLevel --- */
/* --- tim padem vsechny uzly BDD --- */

void  BDD :: del_nodes(){
 NodeList::iterator it;
  for(int i=0; i<varCt; i++)
     for(it = (arrayLevel[i]).begin();it!=(arrayLevel[i]).end();it++)
          {delete *it;}

}

/******************************************************************************/
/* --- funkce pro vytvoreni kopie BDD predstavovaneho uzlem-korenem src --- */
/* --- postupne uklada uzly do BDD diagram --- */
/* --- pouziva mapu uzlu mapa --- */

Node * rec_copy(Node * src,BDD * diagram, Mapa_uzlu * mapa){
  Node * TmpA, * TmpB, * u;
  Mapa_uzlu :: iterator p;
  if(src->isTerminal()) if(src->getValue()==1) return diagram->oneT;
                        else return diagram->zeroT;

  p = mapa->find(src->Low);
  if(p!=mapa->end()) { // src->Low je uz v mape, do TmpA vlozim hodnotu z mapy
                       TmpA = p->second;
                     }
     else {// src->Low neni jeste v mape, TmpA vypocitam
           TmpA = rec_copy(src->Low,diagram,mapa);
          }
   //obdobne TmpB
  p = mapa->find(src->High);
  if(p!=mapa->end()) TmpB = p->second;
   else TmpB = rec_copy(src->High,diagram,mapa);

// vytvorim novy uzel vysledneho BDD
  u = new Node(src->varId,TmpA,TmpB);
// a nezapomenu ho vlozit do mapy
  mapa->insert(pair<Node*,Node*>(src,u));

//pokud to nejsou terminaly, tak do jejich listu parentu vlozim ten novy uzel
  if(!TmpA->isTerminal())TmpA->parentList.push_back(u);
  if(!TmpB->isTerminal())TmpB->parentList.push_back(u);
//vlozim uzel do prislusneho seznamu urovni
  diagram->arrayLevel[u->varId].push_back(u);
//vratim novy uzel
  return u;
}
/******************************************************************************/
/* --- funkce pro kopirovani BDD bez vytvareni noveho BDD(melka kopie) --- */
/* --- sam sebe znici a privlastni si uzly a celkovou strukturu BDD src --- */

   void BDD :: copy_bdd(BDD & src){
 if(arrayLevel!=NULL) {
                        del_nodes();
                        delete [] arrayLevel;
                      }
 delete oneT;
 delete zeroT;
//uklizeno

 tab = src.tab;
 varCt = src.varCt;
 root = src.root;
 arrayLevel = src.arrayLevel;
 oneT = src.oneT;
 zeroT = src.zeroT;

src.arrayLevel = NULL;


}

/******************************************************************************/
/* --- funkce pro nacteni BDD ze souboru source --- */

string BDD::nacti(char * source){
char znak, * in_var, * out_var;
int output_var_number,ilb_flag = 0,ob_flag=0;
int terms = 0;
string str;
PLAtab hlavniM;


ifstream  src ( source );
  if ( src . fail () )
     {
      src . close ();
      cout << "soubor nenalezen";
      exit(1);
     }

//nacteni poctu vstupnich promennych
src >> znak;
if(znak != '.') throw "chyba pri cteni souboru";
src >> znak;
if(znak != 'i') throw "chyba pri cteni souboru";
src >> varCt;

//nacteni poctu vystupnich promennych
src >> znak;
if(znak != '.') throw "chyba pri cteni souboru";
src >> znak;
if(znak != 'o') throw "chyba pri cteni souboru";
src >> output_var_number;

src >> znak;
while(znak=='.'){
  src >> znak;
  // nacteni poctu termu - muze chybet
  if(znak=='p') { src >> terms; src >> znak; }
  if(znak=='i') {
                 src >> znak;
                 if(znak=='l') src >> znak;
                   else throw "chyba pri cteni souboru";
                 if(znak=='b') {
                                // nacteni nazvu vstupnich promennych
                                ilb_flag = 1;
                                in_var = new char[varCt];
                                for(int i=0; i<varCt; i++) {
                                                             src >> in_var[i];

                                                            }
                               src >> znak;// tecka

                               }
                    else throw "chyba pri cteni souboru";
                 }

  if(znak=='o') {
                 src >> znak;
                 if(znak=='b') {
                                ob_flag = 1;
                                out_var = new char[output_var_number];
                                for(int i=0; i<output_var_number; i++) {
                                                                        // nacteni nazvu vystupnich promennych
                                                                        src >> out_var[i];

                                                                       }
                               src >> znak;
                               }
                    else throw "chyba pri cteni souboru";
                }

}

if(ilb_flag) {
              if(ob_flag) str+=out_var[0];
                else str+= "f()";
              str+=" = ";
             }

BDD vysl(varCt),tmp(varCt);

tmp.arrayLevel = new NodeList[varCt];

if(terms){
           hlavniM = PLAtab(1,varCt);
           for(int i=0; i<terms; i++)
            {
             // nacitani po radcich PLA souboru
             arrayLevel = new NodeList[varCt];
             for(int j=0; j<varCt; j++)
                {
                  if(znak=='-') {
                                 hlavniM[0][j] = -1;
                                }

                    else {
                           hlavniM[0][j] = znak-'0';
                           if(ilb_flag) str+=in_var[j];
                           if(znak == '0' && ilb_flag) str+="'";
                         }
                  src >> znak;
               }
              // v hlavniM je ulozen jeden term ze souboru
              hlavniM.bdd_z_termu(this);



             if(i==0) {
                        vysl.copy_bdd(*this);// vysl = *this;
                        zeroT = new Term(TERM_VAR_ID,0);
                        oneT = new Term(TERM_VAR_ID,1);
                       }
                  else  {
                         // udelam OR stavajiciho BDD a nove nacteneho
                         vysl.applyOR(*this,tmp);
                         vysl.copy_bdd(tmp);//vysl = tmp;
                         tmp.oneT = new Term(TERM_VAR_ID,1);
                         tmp.zeroT = new Term(TERM_VAR_ID,0);
                         del_nodes();
                         delete [] arrayLevel;
                         arrayLevel = NULL;
                        }
            cout << ".";
            src >> znak;
            if(ilb_flag)
               if(i!=terms-1)str += " + ";

            }

           delete tmp.oneT;
           delete tmp.zeroT;
           (*this).copy_bdd(vysl);
           tmp.arrayLevel = NULL;
           vysl.arrayLevel = NULL;

         }
  else {
        // to stejne, jenom nevim kolik bude termu
        int i = 0;
        hlavniM = PLAtab(1,varCt);
        while(1){
        arrayLevel = new NodeList[varCt];
        for(int j=0; j<varCt; j++)
                {
                  if(znak=='-') hlavniM[0][j] = -1;
                    else {
                           hlavniM[0][j] = znak-'0';
                           if(ilb_flag) str+=in_var[j];
                           if(znak == '0' && ilb_flag) str+="'";
                         }
                  src >> znak;
                }

       hlavniM.bdd_z_termu(this);
       if(i==0) {
                 vysl.copy_bdd(*this);// vysl = *this;
                 zeroT = new Term(TERM_VAR_ID,0);
                 oneT = new Term(TERM_VAR_ID,1);
                 i++;
                }
          else  {
                 vysl.applyOR(*this,tmp);
                 vysl.copy_bdd(tmp);//vysl = tmp;
                 tmp.oneT = new Term(TERM_VAR_ID,1);
                 tmp.zeroT = new Term(TERM_VAR_ID,0);
                 del_nodes();
                 delete [] arrayLevel;
                 arrayLevel = NULL;
                }

       src >> znak;



       if(src.eof()|| znak=='.') break;

       if(ilb_flag) str += " + ";

      }

       delete tmp.oneT;
       delete tmp.zeroT;
       (*this).copy_bdd(vysl);
       tmp.arrayLevel = NULL;
       vysl.arrayLevel = NULL;

      }

if(znak=='.') {
               src >> znak;
               if(znak!='e') throw "chyba pri cteni souboru";
              }

if(ilb_flag)
cout << "nacetl jsem funkci : " << str << endl;

src . close ();

if(ilb_flag) delete in_var;
if(ob_flag)delete out_var;

if(ilb_flag) return str;
  else return "";
}
/******************************************************************************/
/* --- funkce na redukci BDD --- */
/* --- vyuziva mapy uzlu typu Mapa --- */
/* --- dedundantni uzly maze --- */

void BDD::reduce(){
NodeList::iterator it,it2,it3;
Mapa :: iterator p;
Node * pomNode;
tab.clear();
for(int i=varCt-1;i>0;i--)
  {
    for(it = (arrayLevel[i]).begin();it!=(arrayLevel[i]).end();)
      {

        if((*it)->Low->nodeId == (*it)->High->nodeId)
          {
            //iteruj pres vsechny parenty
            for(it2 = (*it)->parentList.begin(); it2!=(*it)->parentList.end();++it2)
              {
               (*it2)->bypass((*it),(*it)->Low);
              }

           pomNode = *it;
           it = (arrayLevel[i]).erase(it);
           delete pomNode;
           continue;
          }


Mkey pom((*it)->varId,(*it)->Low->nodeId,(*it)->High->nodeId);

        p = tab.find(pom);

        if(p!=tab.end()) //je v tabulce
           {
          //iteruj pres vsechny parenty
             for(it2 = (*it)->parentList.begin();it2!=(*it)->parentList.end();++it2)
              {
                (*it2)->bypass(*it,p->second);
              }
            pomNode = *it;
            it = (arrayLevel[i]).erase(it);
            delete pomNode;
          }

            else //neni v tabulce
               {
                 //tab.insert(pair<Mkey,Node*>(pom,*it));
                 tab.insert(pair<const Mkey, Node*>(pom,*it));
                 ++it;
               }

      }
  }

  if(root->Low->nodeId == root->High->nodeId)
    {
      pomNode = root;
      root = root->Low;

      (arrayLevel[0]).erase((arrayLevel[0]).begin());
      //(arrayLevel[0]).push_front(root);

      delete pomNode;
    }

}

/******************************************************************************/
/* --- funkce apply pro operaci OR mezi dvemi BDD --- */
/* --- vysledne BDD vznikle ze dvou zdrojovych this a sec, je ulozeno ve vysl --- */
/* --- vyuziva se mapa uzlu typu Mapa_apply --- */
/* --- predpoklada ze vysl ma alokovane jen terminaly, jinak vse vytvari sam --- */
/* --- vola se rekurzivni funkce applyOP s prislusnym ukazatelem na funkci, ktera vraci koren vysledneho BDD --- */

void BDD::applyOR(BDD & sec,BDD & vysl){

  Mapa_apply map;
  vysl.tab.clear();
  vysl.arrayLevel = new NodeList[varCt];
  vysl.root = applyOp(root,sec.root,vysl,&map,operaceOR);

}

/******************************************************************************/
/* --- funkce apply pro operaci AND mezi dvemi BDD --- */
/* --- vysledne BDD vznikle ze dvou zdrojovych this a sec, je ulozeno ve vysl --- */
/* --- vyuziva se mapa uzlu typu Mapa_apply --- */
/* --- predpoklada ze vysl ma alokovane jen terminaly, jinak vse vytvari sam --- */
/* --- vola se rekurzivni funkce applyOp s prislusnzm ukazatelem na funkci, ktera vraci koren vysledneho BDD --- */

void BDD::applyAND(BDD & sec,BDD & vysl){

  Mapa_apply map;
  vysl.tab.clear();
  vysl.arrayLevel = new NodeList[varCt];
  vysl.root = applyOp(root,sec.root,vysl,&map,operaceAND);

}
/******************************************************************************/
/* --- funkce apply pro operaci XOR mezi dvemi BDD --- */
/* --- vysledne BDD vznikle ze dvou zdrojovych this a sec, je ulozeno ve vysl --- */
/* --- vyuziva se mapa uzlu typu Mapa_apply --- */
/* --- predpoklada ze vysl ma alokovane jen terminaly, jinak vse vytvari sam --- */
/* --- vola se rekurzivni funkce applyOp s prislusnzm ukazatelem na funkci, ktera vraci koren vysledneho BDD --- */

void BDD::applyXOR(BDD & sec,BDD & vysl){

  Mapa_apply map;
  vysl.tab.clear();
  vysl.arrayLevel = new NodeList[varCt];
  vysl.root = applyOp(root,sec.root,vysl,&map,operaceXOR);

}


/******************************************************************************/
/* --- rekurzivni funkce pro operaci applyOR mezi dvema BDD --- */
/* --- parametry jsou koreny/uzly dvou BDD --- */
/* --- vysledne BDD diagram a mapa pro optimalizaci map --- */

   Node * applyOp(Node * u1, Node * u2, BDD & diagram, Mapa_apply * map,int (*func_op)(Node *,Node *)){

Node * u, *TmpA, *TmpB;
Mapa :: iterator p_tab;
Mapa_apply :: iterator p;

pair_of_nodes p_nodes(u1,u2);
p = map->find(p_nodes);

// pokud uz jsem pocital funkci applyOp pro uzly u1 a u2,
// nepocitam ji znovu, ale rovnou vratim vysledek, ktery je ulozen v mape
if(p!=map->end()) return p->second;


// oba uzly jsou terminaly
 if(u1->isTerminal() && u2->isTerminal())
   {
     if(func_op(u1,u2)==1) return diagram.oneT;
      else return diagram.zeroT;

   }
// oba uzly jsou neterminaly a odpovidaji stejne promenne
    else if(u1->varId == u2->varId)
         {
           TmpA = applyOp(u1->Low,u2->Low,diagram,map,operaceOR);
           TmpB = applyOp(u1->High,u2->High,diagram,map,operaceOR);
           if(TmpA->getId() == TmpB->getId()) return TmpA;
           //podivej se do tabulky uzlu jestli ten uzel, ktery chci vytvaret tam uz neni
           Mkey pom(u1->varId,TmpA->getId(),TmpB->getId());

      p_tab = diagram.tab.find(pom);

       if(p_tab!=diagram.tab.end()) //je v tabulce
          {
           return p_tab->second;
          }
         else  { u = new Node(u1->varId,TmpA,TmpB); diagram.tab.insert(pair<const Mkey,Node*>(pom,u));}

           if(!TmpA->isTerminal())TmpA->parentList.push_back(u);
           if(!TmpB->isTerminal())TmpB->parentList.push_back(u);
         }

    // oba uzly jsou neterminaly, ale promenna odpovidajici u1 je vyse ve strome
    else if(u1->varId < u2->varId)
         {
           if(u1->isTerminal())
             {
               TmpA = applyOp(u1,u2->Low,diagram,map,operaceOR);
               TmpB = applyOp(u1,u2->High,diagram,map,operaceOR);
               if(TmpA->getId() == TmpB->getId()) return TmpA;
               //podivej se do tabulky uzlu jestli ten uzel, ktery chci vytvaret tam uz neni
               Mkey pom(u2->varId,TmpA->getId(),TmpB->getId());
               p_tab = diagram.tab.find(pom);
               if(p_tab!=diagram.tab.end()) //je v tabulce
                  {
                    return p_tab->second;
                  }
                  else {u = new Node(u2->varId,TmpA,TmpB);diagram.tab.insert(pair<const Mkey,Node*>(pom,u));}
               if(!TmpA->isTerminal())TmpA->parentList.push_back(u);
               if(!TmpB->isTerminal())TmpB->parentList.push_back(u);
             }

            else {
                  TmpA = applyOp(u1->Low,u2,diagram,map,operaceOR);
                  TmpB = applyOp(u1->High,u2,diagram,map,operaceOR);
                  if(TmpA->getId() == TmpB->getId()) return TmpA;
                  //podivej se do tabulky uzlu jestli ten uzel, ktery chci vytvaret tam uz neni
                  Mkey pom(u1->varId,TmpA->getId(),TmpB->getId());
                  p_tab = diagram.tab.find(pom);
                  if(p_tab!=diagram.tab.end()) //je v tabulce
                     {
                      return p_tab->second;

                      }
                      else {u = new Node(u1->varId,TmpA,TmpB);diagram.tab.insert(pair<const Mkey,Node*>(pom,u));}
                  if(!TmpA->isTerminal())TmpA->parentList.push_back(u);
                  if(!TmpB->isTerminal())TmpB->parentList.push_back(u);
                 }
         }

    // oba uzly jsou neterminaly, ale promenna odpovidajici u2 je vyse ve strome
    else if(u1->varId > u2->varId)
         {
           if(u2->isTerminal())
              {
                TmpA = applyOp(u1->Low,u2,diagram,map,operaceOR);
                TmpB = applyOp(u1->High,u2,diagram,map,operaceOR);
                if(TmpA->getId() == TmpB->getId()) return TmpA;
                //podivej se do tabulky uzlu jestli ten uzel, ktery chci vytvaret tam uz neni
                Mkey pom(u1->varId,TmpA->getId(),TmpB->getId());
                p_tab = diagram.tab.find(pom);
                if(p_tab!=diagram.tab.end()) //je v tabulce
                  {
                    return p_tab->second;

                  }
                  else {u = new Node(u1->varId,TmpA,TmpB);diagram.tab.insert(pair<const Mkey,Node*>(pom,u));}
                if(!TmpA->isTerminal())TmpA->parentList.push_back(u);
                if(!TmpB->isTerminal())TmpB->parentList.push_back(u);
              }
           else {
                 TmpA = applyOp(u1,u2->Low,diagram,map,operaceOR);
                 TmpB = applyOp(u1,u2->High,diagram,map,operaceOR);
                 if(TmpA->getId() == TmpB->getId()) return TmpA;
                 //podivej se do tabulky uzlu jestli ten uzel, ktery chci vytvaret tam uz neni
                 Mkey pom(u2->varId,TmpA->getId(),TmpB->getId());
                 p_tab = diagram.tab.find(pom);
                 if(p_tab!=diagram.tab.end()) //je v tabulce
                    {

                      return p_tab->second;
                    }
                    else {u = new Node(u2->varId,TmpA,TmpB);diagram.tab.insert(pair<const Mkey,Node*>(pom,u));}
                 if(!TmpA->isTerminal())TmpA->parentList.push_back(u);
                 if(!TmpB->isTerminal())TmpB->parentList.push_back(u);
                }
         }
  diagram.arrayLevel[u->varId].push_back(u);
  map->insert(pair<pair_of_nodes,Node*>(p_nodes,u));

  return u;

}

/******************************************************************************/
/* --- funkce pro zjisteni, zda dane BDD predstavuje tautologii --- */

bool BDD::isTautology(){
// obecne by tu melo byt reduce(), ale ja uz redukovane BDD mam
// aby to nespomalovalo, nevolam reduce

 return (root->getValue()==1);

}
/******************************************************************************/
/* --- funkce pro vypis uzlu v jednotlivych urovnich --- */
/* --- pouziva sablonu funkce pro vypis kontejneru --- */

void BDD::vypisLevely(ostream& out)const{
  for(int i=0;i<varCt;i++)
     printCont<NodeList::iterator>((arrayLevel[i]).begin(),(arrayLevel[i]).end(),out);
}

/******************************************************************************/
/* --- pretizeny operator pro vystup BDD do proudu --- */
/* --- vola se funkce pro vypys levelu a vypisuji se i terminaly --- */

ostream& operator<<(ostream & out,const BDD & dia){
 out << "***************************************" << endl;
 out << "Korenem je uzel:" << *dia.root;
 out << "***************************************" << endl;
 dia.vypisLevely(out);
 out << *dia.oneT << endl;
 out << *dia.zeroT << endl;
 return out;

}


/******************************************************************************/
/* --- funkce pro vypis BDD do souboru --- */

void   BDD :: print_to_file(char * dst){
  ofstream  dest ( dst );
  if ( dest . fail () )
     {
      dest . close ();
      cout << "soubor nelze vytvorit";
      exit(1);
     }

  dest << *this;

  }

/******************************************************************************/
/* --- funkce pro vypocet poctu vnitrnich uzlu --- */

float   BDD :: count_nodes(){
  float vysl=0;

  for(int i=0; i<varCt; i++) vysl += arrayLevel[i].size();

  return vysl;

  }

/******************************************************************************/
/* --- logicka funkce pro OR dvou terminalu --- */
int operaceOR(Node * u1, Node * u2){

  if(u1->getValue()==1 || u2->getValue()==1) return 1;
  else return 0;

}
/******************************************************************************/
/* --- logicka funkce pro AND dvou terminalu --- */

int operaceAND(Node * u1, Node * u2){

  if(u1->getValue()==1 && u2->getValue()==1) return 1;
  else return 0;

}
/******************************************************************************/
/* --- logicka funkce pro XOR dvou terminalu --- */

int operaceXOR(Node * u1, Node * u2){

  if(u1->getValue()!=u2->getValue()) return 1;
  else return 0;

}

