#include "logic.h"
#include "gate.h"
//////////////////////////////////////////
#include "minisat2Solver.h"
//////////////////////////////////////////

namespace sat_atpg {
          
///////////////////////////////////////////////////////////////////////////////          
//cudd lib functions
/*DdNode* Cnf::AddTerm(My_Clause* cls){
  int vcnt=cls->get_var_count();
  DdNode *tmp, *var,*fx;
  fx=Cudd_ReadOne(manager);
  Cudd_Ref(fx);

  if(vcnt>1){

    var=Cudd_bddIthVar(manager,cls->var(0)+1);
    if(cls->polarity(0)){
      tmp=Cudd_bddAnd(manager,var,fx);
	  //cout<< cls->var(vcnt-1)+1 <<endl;
    }else{
      tmp=Cudd_bddAnd(manager,Cudd_Not(var),fx);
	  //cout<< "-" <<cls->var(vcnt-1)+1 << endl;
    }
    Cudd_Ref(tmp);
    Cudd_RecursiveDeref(manager,fx);
    fx=tmp;


	for(int i=1; i<vcnt;i++){  
      var=Cudd_bddIthVar(manager,cls->var(i)+1);
	  if(cls->polarity(i)){
	    tmp=Cudd_bddOr(manager,var,fx);
		//cout<< cls->var(i)+1 << " ";
	  }else{
        tmp=Cudd_bddOr(manager,Cudd_Not(var),fx);
		//cout<<"-"<<cls->var(i)+1 << " ";
	  }
	  Cudd_Ref(tmp);
	  Cudd_RecursiveDeref(manager,fx);
      fx=tmp;
	}

  }else{
    
	  if(vcnt!=0){
        var=Cudd_bddIthVar(manager,cls->var(vcnt-1)+1);
        if(cls->polarity(vcnt-1)){
          tmp=Cudd_bddAnd(manager,var,fx);
		  //cout<< cls->var(vcnt-1)+1 <<endl;
        }else{
          tmp=Cudd_bddAnd(manager,Cudd_Not(var),fx);
		  //cout<< "-" <<cls->var(vcnt-1)+1 << endl;
        }
        Cudd_Ref(tmp);
        Cudd_RecursiveDeref(manager,fx);
        fx=tmp;
	  }
  }

 return fx;
}



void Cnf::MakeBDD(Cnf* cnf){
DdNode *tmp;
int clauseCnt=0;

Cudd_EnableGarbageCollection(manager);
switch(Konfig){
  case 0:
    cout << "reordering NONE" << endl;
    break;
  case 1:
    cout << "reordering RANDOM" << endl;
    Cudd_AutodynEnable(manager,CUDD_REORDER_RANDOM);
    break;
  case 2:
    cout << "reordering RANDOM_PIVOT" << endl;
    Cudd_AutodynEnable(manager,CUDD_REORDER_RANDOM_PIVOT);
    break;
  case 3:
    cout << "reordering SIFT" << endl;
    Cudd_AutodynEnable(manager,CUDD_REORDER_SIFT);
    break;
  case 4:
    cout << "reordering SYMM_SIFT" << endl;
    Cudd_AutodynEnable(manager,CUDD_REORDER_SYMM_SIFT);
    break;
  case 5:
    cout << "reordering GROUP_SIFT" << endl;
    Cudd_AutodynEnable(manager,CUDD_REORDER_GROUP_SIFT);
    break;
  case 6:
    cout << "reordering WINDOW2" << endl;
    Cudd_AutodynEnable(manager,CUDD_REORDER_WINDOW2);
    break;
  case 7:
    cout << "reordering ANNEALING" << endl;
    Cudd_AutodynEnable(manager,CUDD_REORDER_ANNEALING);
    break;
  case 8:
    cout << "reordering GENETIC" << endl;
    Cudd_AutodynEnable(manager,CUDD_REORDER_GENETIC);
    break;
  default:
    cout << "Spatne zadany parametr - konfigurace" << endl;
    exit(0);
  }

cout << "clause count :  " << clauses.length() << " ; variable count : "<<  vars->length() <<endl; 
 
while(clauseCnt<clauses.length()){
	//cout << "clause : " << clauseCnt << " velikost bdd : "<< Cudd_DagSize(f) <<endl; 
    Cudd_RecursiveDeref(manager,f1);
	f1=AddTerm(cnf->get_clause(clauseCnt));
    tmp=Cudd_bddAnd(manager,f,f1);
    Cudd_Ref(tmp);
    Cudd_RecursiveDeref(manager,f);
    f=tmp;
 
	  //cout << "velikost BDD : " << Cudd_DagSize(f) <<endl;
      ////////////////////////////////////////////////////////////
      //// **** Kontrola splnitelnosti **** //////////////////////
      if(Cudd_IsConstant(f)){
        cerr << " Funkce neni splnitelna ... !!!!!!! " << endl;
		//SAT=false;
        break;
      }
      ////////////////////////////////////////////////////////////
      clauseCnt++;
   }
}


 
          
 
///////////////////////////////////////////////////////////////////////////////////
//////// ****  VYSTUP - tisteni mintermu **** /////////////////////////////////////
///////////////////////////////////////////////////////////////////////////////////
void Cnf::PrintMinterm( DdManager * dd, DdNode * node , int * list, int in, int termN ){
    DdNode *N,*Nv,*Nnv;
    int	   i,v,index;

    N = Cudd_Regular(node);
    if (cuddIsConstant(N)) {
        if (node != background && node != zero) {
            for (i = 1; i < dd->size; i++) {
                v = list[i];
                if (v == 0) cout << "0";//(void) fprintf(vystup,"0");
                else if (v == 1) cout << "1";//(void) fprintf(vystup,"1");
                else cout << "-"; //fprintf(vystup,"-");
            }
            cout << "  -> 1 "<<endl;//(void) fprintf(vystup," % g\n", cuddV(node));
        }
    } else {
        Nv  = cuddT(N);
        Nnv = cuddE(N);
        if (Cudd_IsComplement(node)) {
            Nv  = Cudd_Not(Nv);
            Nnv = Cudd_Not(Nnv);
        }
        index = N->index;
        list[index] = 0;
        PrintMinterm(dd,Nnv,list,in,termN);
        list[index] = 1;
        PrintMinterm(dd,Nv,list,in,termN);
        list[index] = 2;
    }
    return;

}

int Cnf::Output_Minterm( DdManager *dd, DdNode * node, int in , int termN)
{
    int	i, *list;
    //fprintf(vystup,".i %i\n",in);
    //fprintf(vystup,".o 1\n");

    background = dd->background;
    zero = Cudd_Not(dd->one);
    list = ALLOC(int,dd->size);
    if (list == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    for (i = 0; i < dd->size; i++) list[i] = 2;
    PrintMinterm(dd,node,list,in,termN);
    //fprintf(vystup,".e\n");
    FREE(list);
    return(1);

}


void Cnf::printEssential(){
	Output_Minterm(manager,Cudd_FindEssential(manager,f),vars->length(),clauses.length());
}





/////////////////////////////////////////////////////////////////////////////////////////////
/***************** print mapped ************************************************************/
/*void Cnf::PrintMapped( DdManager * dd, DdNode * node , int * list, int in, int termN,My_Array<int>  * ay,ofstream &f ,int cnt){
     DdNode *N,*Nv,*Nnv;
    int	   i,v,index;


    N = Cudd_Regular(node);
    if (cuddIsConstant(N)) {
        if (node != background && node != zero) {
           for (i = 0; i < cnt; i++) {
			   if(i<ay->length()){
                 v = list[(*ay)[i]+1];
				 if (v == 0) {f<<"0";cout << "0";}//vct[i]=(char)"0";
				 else if (v == 1) {f<<"1"; cout << "1";}// vct[i]=(char)"1";
				 else  {f<<"-";cout << "-";}//vct[i]=(char)"-";
			   }else{
                  f<<"-";
				  cout << "-";
			   }
		   }
		   f << endl;
		   cout <<endl;	
        }
    } else {
        Nv  = cuddT(N);
        Nnv = cuddE(N);
        if (Cudd_IsComplement(node)) {
            Nv  = Cudd_Not(Nv);
            Nnv = Cudd_Not(Nnv);
        }
        index = N->index;
        list[index] = 0;
        PrintMapped(dd,Nnv,list,in,termN,ay,f,cnt);
        list[index] = 1;
        PrintMapped(dd,Nv,list,in,termN,ay,f,cnt);
        list[index] = 2;
    }
    return;

}*/
/*



void Cnf::PrintMapped( DdManager * dd, DdNode * node , int * list, int in, int termN,Circuit &c,ofstream &f ,int cnt){
     DdNode *N,*Nv,*Nnv;
    int	   i,v,index;


    N = Cudd_Regular(node);
    if (cuddIsConstant(N)) {
        if (node != background && node != zero) {
           
            cout <<"G0 : "<< c.gates[0]->get_var()+1 <<endl;
            cout <<"G1 : "<< c.gates[1]->get_var()+1 <<endl;
            cout <<"G2 : "<< c.gates[2]->get_var()+1 <<endl;
            cout <<"G3 : "<< c.gates[3]->get_var()+1 <<endl;
            cout <<"G5 : "<< c.gates[4]->get_var()+1 <<endl;
            cout <<"G6 : "<< c.gates[5]->get_var()+1 <<endl;
            cout <<"G7 : "<< c.gates[6]->get_var()+1 <<endl;
		    for (i = 0; i < cnt; i++) {
			  if(c.gates[i]->get_var()+1!=0){
			     v = list[c.gates[i]->get_var()+1];
			     if (v == 0) {f<<"0";cout << "0";}//vct[i]=(char)"0";
			     else if (v == 1) {f<<"1"; cout << "1";}// vct[i]=(char)"1";
			     else  {f<<"-";cout << "-";}//vct[i]=(char)"-";
			  }else{
                 f<<"-";
			     cout << "-";
			  }
		    }
		   f << endl;
		   cout <<endl;

        }
    } else {
        Nv  = cuddT(N);
        Nnv = cuddE(N);
        if (Cudd_IsComplement(node)) {
            Nv  = Cudd_Not(Nv);
            Nnv = Cudd_Not(Nnv);
        }
        index = N->index;
        list[index] = 0;
        PrintMapped(dd,Nnv,list,in,termN,c,f,cnt);
        list[index] = 1;
        PrintMapped(dd,Nv,list,in,termN,c,f,cnt);
        list[index] = 2;
    }
    return;

}



int Cnf::OutputMapped( DdManager *dd, DdNode * node, int in , int termN,Circuit &c,ofstream &f,int cnt)
{
    int	i, *list;

    background = dd->background;
    zero = Cudd_Not(dd->one);
    list = ALLOC(int,dd->size);
    if (list == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    for (i = 0; i < dd->size; i++) list[i] = 2;
    PrintMapped(dd,node,list,in,termN,c,f,cnt);

    FREE(list);
    return(1);

}



string Cnf::retMapped1( DdManager * dd, DdNode * node , int * list, int in, int termN,Circuit &c,int cnt){
    DdNode *N,*Nv,*Nnv;
    int	   i,v,index; 

    N = Cudd_Regular(node);
    if (cuddIsConstant(N)) {
        if (node != background && node != zero) {
		    for (i = 0; i < cnt; i++) {
			  if(c.gates[i]->get_var()+1!=0){
			     v = list[c.gates[i]->get_var()+1];
				 if (v == 0) {cout << "0";strVec[i]='0';}
				 else if (v == 1) {cout << "1"; strVec[i]='1';}
			     else  {cout << "-"; strVec[i]='-';} // ---
			  }else{
			     cout << "-"; // ---
				 strVec[i]='-'; // ---
			  }
		    }
		   cout <<endl;

        }
    } else {
        Nv  = cuddT(N);
        Nnv = cuddE(N);
        if (Cudd_IsComplement(node)) {
            Nv  = Cudd_Not(Nv);
            Nnv = Cudd_Not(Nnv);
        }
        index = N->index;
        list[index] = 0;
        retMapped1(dd,Nnv,list,in,termN,c,cnt);
        list[index] = 1;
        retMapped1(dd,Nv,list,in,termN,c,cnt);
        list[index] = 2;
    }
    return strVec;

}


string Cnf::retMapped( DdManager *dd, DdNode * node, int in , int termN,Circuit &c,int cnt)
{
    int	i, *list;
	string str;
	strVec.resize(cnt);	

    background = dd->background;
    zero = Cudd_Not(dd->one);
    list = ALLOC(int,dd->size);
    if (list == NULL) {
        dd->errorCode = CUDD_MEMORY_OUT;
        return(0);
    }
    for (i = 0; i < dd->size; i++) list[i] = 2;
    str = retMapped1(dd,node,list,in,termN,c,cnt);
    FREE(list);
    return str;

}


void Cnf::printVec(Circuit &c,ofstream &ff,int cnt){

 OutputMapped(manager,Cudd_FindEssential(manager,f),vars->length(),clauses.length(),c,ff,cnt);
}
      
void Cnf::printVec1(Circuit &c,ofstream &ff,int cnt){

 OutputMapped(manager,Cudd_SubsetCompress(manager,f,Cudd_SupportSize(manager,f),vars->length()),vars->length(),clauses.length(),c,ff,cnt);
}
 
void Cnf::printVec2(Circuit &c,ofstream &ff,int cnt){

 OutputMapped(manager,f,vars->length(),clauses.length(),c,ff,cnt);
}
          

string Cnf::retEssential(Circuit &c,int cnt){    
  return retMapped(manager,Cudd_FindEssential(manager,f),vars->length(),clauses.length(),c,cnt);
}
          
string Cnf::retSubsetCompress(Circuit &c,int cnt){    
  return retMapped(manager,Cudd_SubsetCompress(manager,f,Cudd_SupportSize(manager,f),vars->length()),vars->length(),clauses.length(),c,cnt);
} 
*/



string Cnf::setInputs(string vct){//,Circuit &c){
string sx;

 sx.resize(vct.length());
 for(int o=0;o<vct.length();o++)sx[o]='-';

 for(int i=0; i<clauses.length(); i++){

    for(int j=0; j<clauses[i]->get_var_count();j++){
       	 
		if((*vars)[clauses[i]->var(j)]->input==1){ // kdzy je to input   
			if(vct[(*vars)[clauses[i]->var(j)]->gate_index]=='0'){ // promenna ma byt nastavena na 0
				sx[(*vars)[clauses[i]->var(j)]->gate_index]='0';
				if(clauses[i]->polarity(j)==true) { // ma bzt nastavena 0 ale je jedna - mazu literal 
					
					//delete clauses[i]->var(j);
					/////////////////////////////////////////////
					if(clauses[i]->get_var_count()==1){sx[0]='u';return sx;} // jestlize bz to bzla jedina promenna a je nastavena na - je to unsat
					/////////////////////////////////////////////
					clauses[i]->remove_var(j); //smazani promenne
					if(j!=0)j--;
				}else{
					if(clauses[i]->polarity(j)==false){// jinak kdzy je nastavena souhlasne mayu celej term
						delete clauses[i];
						clauses.remove(i);  
						if(i!=0)i--;
					}
				}	
			} else{///////////////////

			if(vct[(*vars)[clauses[i]->var(j)]->gate_index]=='1'){ // promenna ma bzt nastavena na 1	 
			  sx[(*vars)[clauses[i]->var(j)]->gate_index]='1';
              if(clauses[i]->polarity(j)==false) { // ma bzt nastavena 1 ale je nula - mazu literal 
				//   delete clauses[i]->var(j);
				   ////////////////////////////////////////////
				   if(clauses[i]->get_var_count()==1){sx[0]='u';return sx;}  // jestlize bz to bzla jedina promenna a je nastavena na - je to unsat
				  /////////////////////////////////////////////
				   clauses[i]->remove_var(j); //smazani promenne
				   if(j!=0)j--;
			  }else{
			   	  if(clauses[i]->polarity(j)==true){// jinak kdzy je nastavena souhlasne mayu celej term
					 delete clauses[i];
				 	 clauses.remove(i);  
					 if(i!=0)i--;
				  }
			  }
			}

		}
		}/////////////////
		
	}   

 }

 return sx;
}


string Cnf::setInputs(string vct,string fp1){//,Circuit &c){
string sx;
//cout << "fp start : "<< fp1<<endl;
 sx.resize(vct.length());
 for(int o=0;o<vct.length();o++)sx[o]='-';

 for(int i=0; i<clauses.length(); i++){
    for(int j=0; j<clauses[i]->get_var_count();j++){
         // cout<< (*vars)[clauses[i]->var(j)]->gate_index <<" "<<endl;
		if(((*vars)[clauses[i]->var(j)])->input==1){ // kdzy je to input   
            /// kdyz je to nastaveno tak smazu
			
			//cout<<"hhhhhhhh " <<fp1 <<endl;
			if(fp1[(*vars)[clauses[i]->var(j)]->gate_index]=='2'){
			
			   if(clauses[i]->get_var_count()<=1){
			     sx[0]='u';
                 return sx;
			   }else{
			      clauses[i]->remove_var(j); //smazani promenne
			      if(j!=0)j--;
			   }
			}else{
            ////////////////////////////////////////////////////

			if(vct[(*vars)[clauses[i]->var(j)]->gate_index]=='0'){ // promenna ma byt nastavena na 0
				sx[(*vars)[clauses[i]->var(j)]->gate_index]='0';
				if(clauses[i]->polarity(j)==true) { // ma bzt nastavena 0 ale je jedna - mazu literal 
					if(clauses[i]->get_var_count()==1){sx[0]='u';return sx;}  // jestlize bz to bzla jedina promenna a je nastavena na - je to unsat
					clauses[i]->remove_var(j); //smazani promenne
					if(j!=0)j--;
				}else{
					if(clauses[i]->polarity(j)==false){// jinak kdzy je nastavena souhlasne mayu celej term
						delete clauses[i];
						clauses.remove(i);  
						if(i!=0)i--;
					}
				}	
			} else{///////////////////

			if(vct[(*vars)[clauses[i]->var(j)]->gate_index]=='1'){ // promenna ma bzt nastavena na 1	 
			  sx[(*vars)[clauses[i]->var(j)]->gate_index]='1';
              if(clauses[i]->polarity(j)==false) { // ma bzt nastavena 1 ale je nula - mazu literal 			
				  if(clauses[i]->get_var_count()==1){sx[0]='u';return sx;}  // jestlize bz to bzla jedina promenna a je nastavena na - je to unsat 
				  clauses[i]->remove_var(j); //smazani promenne
				   if(j!=0)j--;
			  }else{
			   	  if(clauses[i]->polarity(j)==true){// jinak kdzy je nastavena souhlasne mayu celej term
					 delete clauses[i];
				 	 clauses.remove(i);  
					 if(i!=0)i--;
				  }
			  }
			}

		}
	
			
	  }/// else k odstranovani stejnejcj	
		}/////////////////
	}   

 }

 return sx;
}





string Cnf::setDCInputs(string vct,string inputsSet,int from,int to,int typ){// vct - vektor ze solveru , inputSet - nastavení vstupů z predchozího vektoru
string flip;
string sx;
Sat_Solver *satX;
bool satcnf=false;
Cnf *cx;


dcTest=0;
dcSet=0;

/*cout<<"*****************************************************"<<endl;
cout <<"vct : "<< vct <<endl;
cout <<"inp : "<< inputsSet <<endl;*/

flip.resize(inputsSet.length());
for(int i=0;i < inputsSet.length();i++)flip[i]='-';

//cx = c.fault_to_cnf(from,to,typ,true);
//sx=cx->setInputs(vct,flip);


//cout<<"set dc start ..."<<endl;

    //for(int i=vct.length()-1;i >=0 ;i--){
	for(int i=0;i < vct.length();i++){
		if(inputsSet[i]=='-' && vct[i]!='-'){
              dcTest++;
              flip[i]='2';
			  // cout << "pred 0 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count()<<endl;
			 // cout<<"set dc - cnf new ..."<<endl;
			  cx = c.fault_to_cnf(from,to,typ,true);
             // cout<<"set dc - cnf new inp set..."<<endl;
			  sx=cx->setInputs(vct,flip);
			 // cout<<"set dc - cnf new ok ..."<<endl;
			 // cout << "po   0 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<<endl; 
			  satcnf=false;
		      satX = new minisat2::Minisat_Solver();
              satcnf = satX->set_cnf(*cx);   
			 ///////// solver part /////
               if(satX->has_preprocess() && sx[0]!='u')satcnf=satX->preprocess();
               if(satcnf && sx[0]!='u')satcnf=satX->solve();
			   if(satcnf && sx[0]!='u'){
				// cout << "flip : "<< i << " 0->1 - satisfied -> '-' " << vct<<endl;
				 vct[i]='-';
				 inputsSet[i]='-';
				 flip[i]='2';
			     dcSet++;
				
			   }else{
                // cout << "flip : "<< i << " 0->1 - unsatisfied -> '0' "<<vct<<endl; 
                 inputsSet[i]= vct[i];
				 flip[i]='-';
				
			   }
              ///////////konec solver part /////////////////
		 delete cx; 
         delete satX; 
		} //konec hlavni if
	
	} // konec for
	



	/*cout <<"flp : "<< flip <<endl;
	cout <<"inp : "<< inputsSet<<endl;
	cout <<"vc1 : "<< vct <<endl;
	cout<<"*****************************************************"<<endl;*/
//delete cx;
return vct;
}





















/*string Cnf::setDCInputs(string vct,string inputsSet,Cnf *c1,int from,int to,int typ){// vct - vektor ze solveru , inputSet - nastavení vstupů z predchozího vektoru
string flip;
Sat_Solver *satX;
bool satcnf=false;
Cnf *cx;

cout<<"*****************************************************"<<endl;
cout <<"vct : "<< vct <<endl;
cout <<"inp : "<< inputsSet <<endl;

flip.resize(inputsSet.length());
for(int i=0;i < inputsSet.length();i++)flip[i]='-';

cx = c.fault_to_cnf(from,to,typ,true);
cx->setInputs(inputsSet,flip);



    
	for(int i=0;i < vct.length();i++){
		if(inputsSet[i]=='-' && vct[i]!='-'){
           satcnf=false;
		   satX = new minisat2::Minisat_Solver();
          
		   if(vct[i]=='0'){
              vct[i]='1';
			  inputsSet[i]='1';
			 // cout << "pred 0 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count()<<endl;
			  cout <<" volam set .." <<endl;
			  cx = c.fault_to_cnf(from,to,typ,true);
			  cx->setInputs(inputsSet,flip);
			 // cout << "po   0 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<<endl;      
              satcnf = satX->set_cnf(*cx);   
			 ///////// solver part /////
               if(satX->has_preprocess())satcnf=satX->preprocess();
               if(satcnf)satcnf=satX->solve();
			   if(satcnf){
				 cout << "flip : "<< i << " 0->1 - satisfied -> '-' "<<endl;
				 vct[i]='-';
				 inputsSet[i]='-';
				 flip[i]='2';
				
			   }else{
                 cout << "flip : "<< i << " 0->1 - unsatisfied -> '0' "<<endl; 
                 vct[i]='0';
				 inputsSet[i]='0';
				
				 //delete cx;
				 cx = c.fault_to_cnf(from,to,typ,true);
				// for(int l=0;l<i;l++)inputsSet[l]=vct[l];
				 cx->setInputs(inputsSet,flip);
				 //cout << "reconstruct   0 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<< " , "<<vct<<endl;      
				 
			   }
              ///////////konec solver part /////////////////
		   }
		   else {


		   if(vct[i]=='1'){
              vct[i]='0';
			  inputsSet[i]='0';
			 // cout << "pred 1 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count()<< endl;
			 // cout <<"vct: "<< vct<<endl;
			 // cout <<"inp: "<<inputsSet<<endl;
			  cout <<" volam set .." <<endl;
			  cx = c.fault_to_cnf(from,to,typ,true);
			  cx->setInputs(inputsSet,flip);
           // cout << "po   1 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count()<<endl; 
              satcnf = satX->set_cnf(*cx);    
              ///////// solver part /////
               if(satX->has_preprocess())satcnf=satX->preprocess();
               if(satcnf)satcnf=satX->solve();
			   if(satcnf){
				 cout << "flip : "<< i << " 1->0 - satisfied -> '-' "<<endl;
				 vct[i]='-';
				 inputsSet[i]='-';
				 flip[i]='2';
								 
			   }else{
                 cout << "flip : "<< i << " 1->0 - unsatisfied -> '1' "<<endl;
                 vct[i]='1';
				 inputsSet[i]='1';
				 
				 //delete cx;
				 cx = c.fault_to_cnf(from,to,typ,true);
				 //for(int l=0;l<i;l++)inputsSet[l]=vct[l];
				 cx->setInputs(inputsSet,flip);
				// cout << "reconstruct   1 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<< " , "<<vct<<endl;      
			   }
              ///////////konec solver part /////////////////
		   }
           
		   }///else


         delete satX; 
		} //konec hlavni if
	
	} // konec for
	







               satcnf=false;
			   cx = c.fault_to_cnf(from,to,typ,true);
		   satX = new minisat2::Minisat_Solver();
              cx->setInputs(inputsSet,flip);
           // cout << "po   1 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count()<<endl; 
              satcnf = satX->set_cnf(*cx);    
              ///////// solver part /////
               if(satX->has_preprocess())satcnf=satX->preprocess();
               if(satcnf)satcnf=satX->solve();
			   if(satcnf){
				 cout << "je splnitelna s danzm nastavenim "<<endl;
				 
								 
			   }else{
                 cout << "neni splnitelna s danzm nastavenim"<<endl;
                // cout << "reconstruct   1 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<< " , "<<vct<<endl;      
			   }
              ///////////konec solver part /////////////////
		   delete satX;






	cout <<"flp : "<< flip <<endl;
	cout <<"flp : "<< inputsSet<<endl;
	cout <<"vc1 : "<< vct <<endl;
	cout<<"*****************************************************"<<endl;
delete cx;
return vct;
}
*/



/*string Cnf::setDCInputs(string vct,string inputsSet,Cnf *c1,int from,int to,int typ){// vct - vektor ze solveru , inputSet - nastavení vstupů z predchozího vektoru
string flip;
Sat_Solver *satX;
bool satcnf=false;
Cnf *cx;
int * dcmask; // nastavuju priynak tem co muzu smazat     

cx = c.fault_to_cnf(from,to,typ,true);
dcmask=new int[cx->get_var_count()];
for(int i=0;i<cx->get_var_count();i++)dcmask[i]=-1;
//cout << "NNNNNNNNNNcnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count() <<endl;
//flip=cx->setInputs(inputsSet,dcmask);
//cout << "NNNNNNNNN111pred 0 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count() <<endl;


//cout <<"********************************************************************"<<endl;
 //  cout <<"inputsSet : " << inputsSet <<endl;
 //  cout <<"vct0      : " << vct <<endl;
	
    
	for(int i=0;i < vct.length();i++){
		if(inputsSet[i]=='-' && vct[i]!='-'){
           satcnf=false;
		   satX = new minisat2::Minisat_Solver();
          
		   if(vct[i]=='0'){
              vct[i]='1';
			  inputsSet[i]='1';
			 // cout << "pred 0 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count()<<endl;
			  flip=cx->setInputs(vct,dcmask);
			 // cout << "po   0 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<<endl;      
              satcnf = satX->set_cnf(*cx);   
			 ///////// solver part /////
               if(satX->has_preprocess())satcnf=satX->preprocess();
               if(satcnf)satcnf=satX->solve();
			   if(satcnf){
				 cout << "flip : "<< i << " 0->1 - satisfied -> '-' "<<endl;
				 vct[i]='-';
				 inputsSet[i]='-';
				 dcmask[i]=1;
			   }else{
                 cout << "flip : "<< i << " 0->1 - unsatisfied -> '0' "<<endl; 
                 vct[i]='0';
				 inputsSet[i]='0';
				 delete cx;
				 delete satX;
				 delete dcmask;
				 return vct;
				 ///////////////////////////
				 cx = c.fault_to_cnf(from,to,typ,true);
				// for(int l=0;l<i;l++)inputsSet[l]=vct[l];
				 flip=cx->setInputs(inputsSet,dcmask);
				 //cout << "reconstruct   0 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<< " , "<<vct<<endl;      
				 
			   }
              ///////////konec solver part /////////////////
		   }
		   else {


		   if(vct[i]=='1'){
              vct[i]='0';
			  inputsSet[i]='0';
			 // cout << "pred 1 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count()<< endl;
			 // cout <<"vct: "<< vct<<endl;
			 // cout <<"inp: "<<inputsSet<<endl;
			  flip=cx->setInputs(vct,dcmask);
           // cout << "po   1 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count()<<endl; 
              satcnf = satX->set_cnf(*cx);    
              ///////// solver part /////
               if(satX->has_preprocess())satcnf=satX->preprocess();
               if(satcnf)satcnf=satX->solve();
			   if(satcnf){
				 cout << "flip : "<< i << " 1->0 - satisfied -> '-' "<<endl;
				 vct[i]='-';
				 inputsSet[i]='-';
				 dcmask[i]=1;
			   }else{
                 cout << "flip : "<< i << " 1->0 - unsatisfied -> '1' "<<endl;
                 vct[i]='1';
				 inputsSet[i]='1';
				 delete cx;
				 delete satX;
				 delete dcmask;
				 return vct;
				 ///////////////////////////
				 cx = c.fault_to_cnf(from,to,typ,true);
				 flip=cx->setInputs(inputsSet,dcmask);
				 cout << "reconstruct   1 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<< " , "<<vct<<endl;      
			   }
              ///////////konec solver part /////////////////
		   }
           
		   }///else


         delete satX; 
		} //konec hlavni if
		/*else{
          if(inputsSet[i]!='-' && vct[i]=='-')vct[i]=inputsSet[i];

		}*/
           

	//} // konec for


/*
delete cx;
delete dcmask;
return vct;
}*/



/*
string Cnf::setDCInputs(string vct,string inputsSet,Cnf *c1,int from,int to,int typ){// vct - vektor ze solveru , inputSet - nastavení vstupů z predchozího vektoru
string flip;
Sat_Solver *satX;
bool satcnf=true;
Cnf *cx;

cx = c.fault_to_cnf(from,to,typ,true);
//cout << "NNNNNNNNNNcnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count() <<endl;
flip=cx->setInputs(inputsSet);
//cout << "NNNNNNNNN111pred 0 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count() <<endl;


//cout <<"********************************************************************"<<endl;
 //   cout <<"inputsSet : " << inputsSet <<endl;
//	cout <<"vct0       : " << vct <<endl;
	
    
	for(int i=0;i < vct.length();i++){
		if(inputsSet[i]=='-' && vct[i]!='-'){
          
		   satX = new minisat2::Minisat_Solver();
          
		   if(vct[i]=='0'){
              vct[i]='1';
			  inputsSet[i]='1';
			  cout << "pred 0 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count() << " , "<<vct<<endl;
			  flip=cx->setInputs(inputsSet);
			  cout << "po   0 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<<endl;      
              satcnf = satX->set_cnf(*cx);   
			 ///////// solver part /////
               if(satX->has_preprocess())satcnf=satX->preprocess();
               if(satcnf)satcnf=satX->solve();
			   if(satcnf){
				 cout << "flip : "<< i << " 0->1 - satisfied -> '-' "<<endl;
				 vct[i]='-';
				 inputsSet[i]='-';
			   }else{
                 cout << "flip : "<< i << " 0->1 - unsatisfied -> '0' "<<endl; 
                 vct[i]='0';
				 inputsSet[i]='0';
				 delete cx;
				 cx = c.fault_to_cnf(from,to,typ,true);
				// for(int l=0;l<i;l++)inputsSet[l]=vct[l];
				 flip=cx->setInputs(inputsSet);
				 cout << "reconstruct   0 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<< " , "<<vct<<endl;      
			   }
              ///////////konec solver part /////////////////
		   }
		   else {


		   if(vct[i]=='1'){
              vct[i]='0';
			  inputsSet[i]='0';
			  cout << "pred 1 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count()<< " , "<<vct<<endl;
			  flip=cx->setInputs(inputsSet);
            cout << "po   1 - cnf " << cx->get_clause_count()<<" - var cnf "<< cx->get_var_count()<<endl; 
              satcnf = satX->set_cnf(*cx);    
              ///////// solver part /////
               if(satX->has_preprocess())satcnf=satX->preprocess();
               if(satcnf)satcnf=satX->solve();
			   if(satcnf){
				 cout << "flip : "<< i << " 1->0 - satisfied -> '-' "<<endl;
				 vct[i]='-';
				 inputsSet[i]='-';
			   }else{
                cout << "flip : "<< i << " 1->0 - unsatisfied -> '1' "<<endl;
                 vct[i]='1';
				 inputsSet[i]='1';
				 delete cx;
				 cx = c.fault_to_cnf(from,to,typ,true);
			
				 flip=cx->setInputs(inputsSet);
				 cout << "reconstruct   1 - cnf "<< cx->get_clause_count()<<" - var cnf  "<< cx->get_var_count()<< " , "<<vct<<endl;      
			   }
              ///////////konec solver part /////////////////
		   }
           
		   }///else


         delete satX; 
		} //konec hlavni if
		else{
          if(inputsSet[i]!='-' && vct[i]=='-')vct[i]=inputsSet[i];

		}
           

	} // konec for



cx = c.fault_to_cnf(from,to,typ,true);
flip=cx->setInputs(inputsSet);
satX = new minisat2::Minisat_Solver();




 //  cout <<"vct1       : " << vct <<endl;
 //  cout <<"is1       : " << inputsSet <<endl;
//   cout <<"********************************************************************"<<endl;
delete cx;
//	return vct;



return inputsSet;
}*/













/////////////////////////////////////////////////////////////////////////////////          
          
          

ostream& operator << (ostream& stream,l_type& l)
{
 if (l==l_dc) 
   stream << "x";
 else if (l==l_true)
   stream << 1;
 else if (l == l_false)  
   stream << 0;
 else
   stream << "Z";  
 return stream;
}

void l_type::print (ostream& stream)
{
 if ((*this)==l_dc) 
   stream << "x";
 else if ((*this)==l_true)
   stream << 1;
 else if ((*this) == l_false)  
   stream << 0;
 else
   stream << "Z";  
}

 l_type& l_type::operator = (const l_type& _l)
{
 value = _l.value;
 return *this;
}

 bool l_type::operator == (const l_type& _l)
{
 return value == _l.value;
}

 bool l_type::operator != (const l_type& _l)
{
 return value != _l.value;
}

 l_type& l_type::operator & (const l_type& _l)
{
 static l_type l;
 l.value = value & _l.value;
 if (l.value ^ 2)
   return l;
 l.value = 1;
 return l;
}
 
 l_type& l_type::operator | (const l_type& _l)
{
 static l_type l;
 l.value = value | _l.value;
 return l;
}


l_type& operator ~ (const l_type& l)
{
 static l_type result;
  if (l.value ^ 1)
     result.value = ~l.value;
  else
     result.value = l.value;
  return result;      
}

l_type& l_type::operator + ( const l_type& _l )
{
 /*l_type* l = new l_type;*/
static l_type l;
 if (value ^ 1)
   l.value = value;
 else
   l.value = _l.value;
 return l;
}
    	


l_type& l_type::operator ^(const l_type& _l)
{

/* l_type* l = new l_type;*/
 static l_type l;
 if ((_l.value == 1) || (value == 1))
    l.value =1;  
 else
    l.value = value ^ _l.value;
 return l;
}

My_Var::My_Var (const My_Var& v)
{
 input=v.input;
 faulty=v.faulty; //true iff in faulty part of Circuit 
 value=v.value;  //value from Sat solver 
 gate_index=v.gate_index; //index in Circuit
}

My_Var::My_Var (const My_Var* v)
{
 input=v->input;
 faulty=v->faulty; //true iff in faulty part of Circuit 
 value=v->value;  //value from Sat solver 
 gate_index=v->gate_index; //index in Circuit
}
void My_Clause::print_var(ostream &stream, int index, Cnf &cnf)
{
 if (!weights[index])
   stream << "not ";
 cnf.print(stream, vars[index]);
}

void My_Clause::print_integers(ostream &stream)
{
 for (int i=0; i<var_count; i++)
   {
    if(!weights[i])
      stream <<"-";
    stream << vars[i] << " ";
   } 
stream << endl;
}      

My_Clause::My_Clause(const My_Clause& m)
{
 max_count = m.var_count;
 var_count = m.var_count;
 vars = new int[var_count];
 weights = new bool[var_count];
 for(int i=0; i<var_count;i++)
   { 
    vars[i] = m.vars[i];
    weights[i]= m.weights[i];
   }
}
My_Clause::My_Clause (My_Clause* m)
{
 max_count = m->var_count;
 var_count = m->var_count;
 vars = new int[var_count];
 weights = new bool[var_count];
 for(int i=0; i<var_count;i++)
   {
    vars[i]=m->vars[i];
    weights[i]=m->weights[i];
   }
} 
 



My_Clause::My_Clause (int _max_count): max_count(_max_count) {
vars = new int[max_count];
weights = new bool[max_count];
var_count = 0;
}

bool My_Clause::satisfied(Cnf &cnf)
{
 bool s=false;
 for(int i=0;i<var_count;i++)
   {
     if (((cnf.get_var(vars[i])->value == l_true) && weights[i]) 
         ||
        ((cnf.get_var(vars[i])->value == l_false) && (!weights[i]))) 
     {
      s=true;
      break;
     }
  }
 return s;
}
    
void My_Clause::print(ostream &stream,Cnf &cnf)
{
if (var_count>0)
 {
  this->print_var(stream,0,cnf);  
  for (int i=1; i<var_count; i++)
     {
       stream << " v ";
       this->print_var(stream,i,cnf);
     }
 stream << endl; 
 }
}

void My_Clause::add_var(int var, bool weight)
{
 vars[var_count]=var;
 weights[var_count++]=weight;
}

void My_Clause::remove_var(int index)
{ 
 var_count--;
 vars[index]=vars[var_count];
 weights[index]=weights[var_count];
}

Cnf::~Cnf()
{
 if (delete_vars)
   {
    for (int i=0;i<vars->length();i++)
     delete (*vars)[i];
    delete vars;
   }
 for (int i=0;i<clauses.length();i++)
     delete clauses[i];

 // cudd functions
 /*Cudd_RecursiveDeref(manager,f); 
 Cudd_RecursiveDeref(manager,f1); 
 Cudd_Quit(manager); */
}

void Cnf::add_clause(My_Clause *c){
 clauses.insert(c);
 if (c->is_binary())
   {
	++binary_clause_count;
   }
}

void Cnf::print(ostream &stream) {
for(int i=0; i<vars->length(); i++)
  {
   print(stream,i);
   stream << ": " << (*vars)[i]->value << endl;
  }
for(int i=0; i<clauses.length();i++)
  clauses[i]->print(stream,(*this));
}

void Cnf::print_integers(ostream &stream) 
{
for (int i=0;i<vars->length();i++)
   {
    stream << i << " ";
    
   }
stream << endl;    
for (int i=0;i<vars->length();i++)
   { 
    stream << (*vars)[i]->value;
   }
 stream << endl;
for(int i=0; i<clauses.length();i++)
   clauses[i]->print_integers(stream);
} 

void Cnf::print(ostream &stream,int index) {
 if ((*vars)[index]->gate_index<0){
   stream << "A_";
   stream << c.int_to_name(-(*vars)[index]->gate_index);
 }else{
   if ((*vars)[index]->faulty) stream << "f_";
  
   stream << c.int_to_name((*vars)[index]->gate_index);
   
 } 
}  


int Cnf::newVar(int _index,bool _faulty)
{
 
 My_Var* v = new My_Var(_index,_faulty,(((_index<c.get_input_count())&&(_index>=0))?true:false));
 vars->insert(v); 
 return vars->length()-1; }


bool Cnf::satisfied()
{
 bool s = true;
 for(int i=0; i<clauses.length(); i++)
   if (!(s= clauses[i]->satisfied(*this)))
      break; 
 return s;
}



Cnf::Cnf(const Cnf& cnf):c(cnf.c),delete_vars(true)
{ 
 vars=new My_Array<My_Var*>(cnf.vars->length());
 for(int i=0; i< cnf.clauses.length(); i++)
   clauses.insert(new My_Clause((cnf.clauses)[i]));
 for(int i=0; i< cnf.vars->length(); i++)
   vars->insert(new My_Var((*cnf.vars)[i]));
 binary_clause_count = cnf.binary_clause_count;
 
 // cudd functions
/* manager = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
 f=Cudd_ReadOne(manager);
 Cudd_Ref(f);
 f1=Cudd_ReadOne(manager);
 Cudd_Ref(f1);
 Konfig=5;*/
}

void Cnf::init_vars_dc()
  {
   for(int i=0; i<vars->length(); i++)
     if (!(*vars)[i]->input)
       (*vars)[i]->value = l_dc;
   for(int i=0; i<clauses.length();)
     {
      bool remove = false;
      for(int j=0;j<clauses[i]->get_var_count();j++)
       if ((*vars)[clauses[i]->var(j)]->gate_index<0)
         {
          remove = true;
          break;
         }
      if (remove)   
        clauses.remove(i);
      else
        i++;
     }      
  }

Cnf::Cnf ( Circuit &_c ) : c ( _c ), delete_vars(true)
{
 vars = new My_Array<My_Var*>;
 binary_clause_count = 0;

 // cudd functions
/* manager = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
 f=Cudd_ReadOne(manager);
 Cudd_Ref(f);
 f1=Cudd_ReadOne(manager);
 Cudd_Ref(f1);
 Konfig=5;
*/
}


void Cnf::remove_clause(int index)
{
 if (clauses[index]->is_binary())
   {
     --binary_clause_count;
   }
 clauses.remove(index);
 
}

Test_Vector::Test_Vector(Circuit &circuit, Cnf &cnf)
{
 in_vector = circuit.inputs_to_vector(cnf);
 out_vector = circuit.outputs_to_vector(cnf);
 fault_vector = circuit.fault_outputs_to_vector(cnf);
}

Test_Vector::Test_Vector ( My_Vector<l_type> *input, My_Vector<l_type> *output, My_Vector<l_type> *fault)
{
 in_vector = input;
 out_vector = output;
 fault_vector = fault;
}
      
int Test_Vector::get_input_count()
{
 return in_vector->length();
}

int Test_Vector::get_output_count()
{
 return out_vector->length();
}
 

/*!
    \fn Test_Vector::get_input_vector()
 */
My_Vector<l_type>* Test_Vector::get_input_vector()
{
    return in_vector;
}


/*!
    \fn Test_Vector::get_output_vector()
 */
My_Vector<l_type>* Test_Vector::get_output_vector()
{
    return out_vector;
}

/*!
    \fn Test_Vector::get_fault_output_vector()
 */
My_Vector<l_type>* Test_Vector::get_fault_output_vector()
{
    return fault_vector;
}


ostream& Test_Vector::operator << (ostream &stream)
{
 for(int i=0; i<in_vector->length(); i++)
    stream << (*in_vector)[i];
stream << " ";
for(int i=0; i<out_vector->length(); i++)
    stream << (*out_vector)[i];
stream << " "; 
for(int i=0; i<fault_vector->length(); i++)
  stream << (*fault_vector)[i];
 return stream;
}

void Test_Vector::print(ostream &stream,bool in_, bool out_, bool fault_)
{
 if (in_)    
 for(int i=0; i<in_vector->length(); i++)
    stream << (*in_vector)[i];
    
 if ((out_vector!=0) && (out_))
   {
 	stream << " ";
 	for(int i=0; i<out_vector->length(); i++)
    		stream << (*out_vector)[i];
   } 		
if ((fault_vector!=0) && (fault_))
   {
		stream << " ";  
          	 for(int i=0; i<fault_vector->length(); i++)
           		stream << (*fault_vector)[i];	
	
   }
}
/*!
    \fn Test_Vector::tests_fault()
 */
bool Test_Vector::tests_fault()
{
for(int i=0;i<out_vector->length();i++)
   if(((*out_vector)[i]!=(*fault_vector)[i]) && ((*out_vector)[i]!=l_dc))
      return true;
return false;	
}

bool Test_Vector::operator ^ (const Test_Vector& t_v)
{
 return *in_vector ^ *t_v.in_vector;
}

Test_Vector* Test_Vector::operator + (const Test_Vector& t_v)
{
 My_Vector<l_type> *input=0;
 My_Vector<l_type> *output=0;
 My_Vector<l_type> *fault=0;
 if ((in_vector!=0) && (t_v.in_vector!=0))
   {
	input = *in_vector + *t_v.in_vector;
   }	
 if ((out_vector!=0) && (t_v.out_vector!=0))
   {
	output = *out_vector + *t_v.out_vector;
   }
 if ((fault_vector!=0) && (t_v.fault_vector!=0))
   {
	fault = *fault_vector +*t_v.fault_vector;	  
   }
 return new Test_Vector(input,output,fault);
}


/*!
    \fn Test_Vector::count_dc_inputs()
 */
int Test_Vector::count_dc_inputs()
{
  int count =0;
  for (int i=0; i<in_vector->length();i++)
    {
	if (((*in_vector)[i]) == l_dc)
           count++;
    }
  return count;    
}


/*!
    \fn Cnf::export_vars()
 */
My_Array<My_Var*>* Cnf::export_vars()
{
   delete_vars = false;
   return vars;
}


/*!
    \fn Cnf::copy_vars()
 */
My_Array<My_Var*>* Cnf::copy_vars()
{
 My_Array<My_Var*> *m_a = new My_Array<My_Var*>(vars->length());
 for (int i=0; i<vars->length();i++)
    m_a->insert(new My_Var((*vars)[i]));
 return m_a;
}

Test_Vector::~Test_Vector()
{
 delete in_vector;
 delete out_vector;
 delete fault_vector;
}



// converts all dc to l (should be l_true or l_false);
void Test_Vector::dc_convert(const l_type &l)
{
 if (in_vector!=0)
   for (int i=0; i<in_vector->length();i++)
     if ((*in_vector)[i]==l_dc)
        {
         (*in_vector)[i]=l;
        }
} 



/*!
    \fn Cnf::to_dimacs(ofstream &f)
 */
void Cnf::to_dimacs(ofstream &f)
{
 f << "c v " << vars->length() << endl;  
 for (int i=0; i< vars->length();i++)
   {
    f << "c " << i+1 <<" ";
    print(f,i);
    f << endl; 
   }    
 f << "p cnf "<<vars->length() <<" "<<clauses.length() <<endl;
    for (int i=0; i<clauses.length(); i++)
	{
	 clauses[i]->to_dimacs(f);
        }
}		
/*!
    \fn My_Clause::to_dimacs(ofstream &f)
 */
void My_Clause::to_dimacs(ofstream &f)
{
 for (int i=0; i<var_count;i++)
    {
     if (!weights[i])
       f<<"-";
     f<<vars[i]+1 << " ";
    }
 f << 0 << endl; 						 
}
}
