#include <iostream>
#include "minisat2Solver.h"
#include "minisatDcSolver.h"
#include "gate.h"
#include "stdafx.h"
#include "ainclude\Atpg.h"
#include "ainclude\Simulation.h"
#include "ainclude\Fault.h"
#include <stdio.h>

#include <map>
#include <ctime>




static inline double cpuTime(void) {
    return (double)clock() / CLOCKS_PER_SEC; }



#define NO_CONVERSION 2
#define CONVERT_TO_ONE 1
#define CONVERT_TO_ZERO 0

using namespace atalantadll;
//using namespace sat_atpg;



//prints values of simulation, for debugging only
void print_result ( ostream &stream, Circuit &c, Cnf &cnf)
{
	c.print_inputs ( stream,cnf );
	stream << " ";
	c.print_outputs ( stream,cnf );
}



//chooses vector with maximum count of DC
int choose_vector(My_Array<Test_Vector*> &vectors)
{
 int index=0;
 int best_dc= vectors[0]->count_dc_inputs();
    for (int i=1;i<vectors.length();i++)
      {
       int dc_count = vectors[i]->count_dc_inputs();
       if (dc_count>best_dc)
          {
	   index = i;
           best_dc = dc_count;
         }
     }
 return index;
}

//adds vector to result, tryes to unite with another one
void add_vector_to_result(My_Array<Test_Vector*> &result,Test_Vector *vector)
{
 int index_result=-1;
 int best = -1;
 int temp_count; 
 Test_Vector *best_t_v=0;
  for(int i=0; i<result.length();i++)
      if (!((*vector) ^ *(result[i])))   //vectors are compatible   	
        {					
         Test_Vector *t_v;			
	 t_v = ((*vector) + (*(result[i])));	// X = Y u Z
         temp_count = t_v->count_dc_inputs();   //counts DC
         if (temp_count>best)			//has more DC thne previous best solution
	   {
             delete best_t_v;
	     best_t_v = t_v;
	     best = temp_count;
	     index_result = i;	
	   }
         else
           delete t_v;				
	}
 if (best>-1)				//compatible vector found
   {
    delete result[index_result];	
    result[index_result] = best_t_v; 
    delete vector;
   }	
 else					//if no compatible vector, adds vector to list	
   {
    result.insert(vector);
  }
}    


//simple help
void help()
{
 cout<<"sat_atpg [options] [-n] bench_file_name "<< endl;
 cout<<"Options:"<<endl<<endl;
 cout<<"-h	displays this short help"<<endl<<endl;
 cout<<"-n <FILE>	specifies file in .bench format"<<endl;
 cout<<"-t <FILE>	specifies output file with patterns"<<endl;
 cout<<"-f <FILE>	specifies input file with faults"<<endl;
 cout<<"-F <FILE>	specifies output file with faults"<<endl;
 cout<<"-P <FILE>	specifies output for report"<<endl;
 cout<<"-U <FILE>	prints not covered faults"<<endl;
 cout<<"-d <FILE/DIR>	exports cnf forms of faults to FILE (one fault solved) or DIR/*.cnf (more faults to solved), no ATG is performed"<<endl;  
 cout<< endl <<"-A	for each fault computes all test vectors, no compaction"<<endl;
 cout<<"-D <n>	for each fault computes n test vectors, no compaction"<<endl; 
 cout<<"-e <0,1,2>	expand to dont cares: 0-none (default), 1-cnf, 2-structural"<<endl;
 cout<<"-N	dont make compaction"<<endl;
 cout<<"-r <0,1,2>	Fault reduction: 0-only ekvivalence, 1-also dominance (default), 2-risky (bad coverage)"<<endl;
 cout<<"-a	appends one line of values to report file instead of rewrite file with full report"<<endl; 
 cout<<"-ch     doesnt use eqivalence but Checkpoints theorem for fault init"<<endl;
 cout<<"-W <0,1,2,3>	vektor format: 0-no, 1-inputs, 2-outputs 3-numbered list for -A or -D mode "<<endl;
 cout<<"-s 	switch to dc_solver"<<endl;
 cout<<"-l 	prints Inputs"<<endl;
 cout<<"-V 	dont use active vars"<<endl;	 
} 						


//compaction over all vectors, doesnt work yet
void compact(My_Array<Test_Vector*> &result)
{
 int best_i,best_j, best_dc, dc_count;   	
 do
   {
    best_i = -1;
    best_j = -1;
    best_dc = -1;
    Test_Vector *best_vector=0;
    Test_Vector *t_v;						
    for(int i=0;i<result.length()-1;i++)
       for(int j=i+1;j<result.length();j++)
	  {
	    if (!(*(result[i])^ *(result[j])))
		{
		  t_v = ((*(result[i])) + (*(result[j])));
		  dc_count = t_v->count_dc_inputs();
		  if (dc_count>best_dc)
		    {
		     best_dc = dc_count;
		     best_i = i;
		     best_j = j;
		     best_vector = t_v;	
		    }							
		}
	  }
   if (best_dc>-1)
     {
	result[best_i]=best_vector;
	result.remove(best_j);
     }
   }				
 while (best_dc > -1);
}







int main ( int argc, char *argv[] )
{
//*********** file streams
	ifstream file_bench_in; 		//input files with circuit in ISCAS format
	ifstream file_faults_in; 		//input file with list of faults (Atalanta format)
	ofstream file_faults_out;		//output file for faults
	ofstream file_patterns_out;		//output file for test patterns
	ofstream file_report_out;		//output file for report
	ofstream file_export_out;		//output file for dimacs
	ofstream file_redundant_out;		//output file for redundant faults	
	ofstream mapVec;		//
	ofstream file_test_out;
//*********** parameters
	bool in_bench_set = false;	//bench file was given
	bool in_out_set = false;	
	bool in_faults_set = false; 	//list of faults was given
	bool out_faults_set = false;	//output file for faults was given
	bool out_patterns_set = false;	//output file for patterns was given
	bool out_report_set = false;	//output file for reprot was given	
	bool out_redundant_set = false; //output file fo redundant faults was given
   	bool export_to_dimacs = false;	//export SAt instances to dimacs format
    /////////////////////////
    bool compress = false;	// atpg compression set - použijeme kompresy?
	char* benchName;        // jmeno benchmarku - obvodu
	char* patName;
	char* streamOut;
	int from,to,typ;        // indexy chyby - from, to a druh chyby type - potrebujili vytvorit chybu
	int vecCount=0;           // pocet vektoru nutnzch k pokryti
	int undetectedVec=0;
	int coveredTmp=0;       // kolik poruch pokryla aktualni simulace
	int bitCount=0;         // pocet bitu ktere jsem uz vzsunul
	 string inputSet;
	 string newV;
	 Sat_Solver *satM;
     Test_Vector *current=0;
	 My_Vector<l_type> *ivector;
     int shiftCount=0; //hlida kolikrat doslo k vzsunuti - pokud jsem vzsunul vsechnz bitz musi tam bzt nesplnitelny sat -> vzhodim poruchu = undetected
     clock_t startatpg,endatpg; // mereni casu
	 Cnf* cnf;

	 int sortEnable=0;   // povoleni razeni - nerazeno(0), max->min(1), min->max(2)
	 int DCenable=0;     // povoleni pridavani DC(1)
	 int presimEnable=0; // povoleni presimulace(1)

	 //////// temp heuristika ///
     int clTmp=0;
	 int varTmp=0;
     int inptmp=0;
     int fltI=0;
	 int tmpBit=0;
	 int dcTest; // testovano DC
	 int dcSet;  // kolik jsem jich nastavil na DC
	 ////////////////////////////
	 

    /////////////////////////  	
	int expand_mode = 0;		//expand dontcares in test vectors 
	//bool debug = false;		//print another info
	bool all_iter=false; 		//for each fault find all vectors
	bool print_circuit=false;       //print circuit
   	bool diagnostic_mode=false;     //for each fault prints some vectors  
    	bool compaction=true;		//compaction
	bool simple_compaction = true;  //simple compaction = when inserts to array of vectors, tries to unite with another
        bool use_checkpoints = false;   //doesn't use gate-after-gate faults generation using ekvivalence but Checkpoint theorem instead; 
	int remove_covered=1; 		//0-no_remove, 1-remove dominate, 2-remove_risky (experimental:))
 	bool single_fault=true; 	//to determine, if dimacs output will be to file or directory 
        bool use_dc_solver = false;	//using DC solver
	bool report_append = false;	//report in special format in one line is appen d to file, suitable for komplex tests
	bool use_active_vars = true;	//generate active vars during conversion to Cnf
	int report=-1; 			
	string dimacs_path;		//path to diamacs file
	int output_mode = 0;		//if output is print	
        int convert_dc = NO_CONVERSION; //no conversion at the end 
	int n = 1; 			//number of vectors for each fault
//*********** results
	My_Array<Test_Vector*> result;	//result - array of Vectors
	bool satisfied;			//controls if current Cnf is satisfiable

//*********** objects
	Parser p;			//very simple parser for parsing Circuit and faults (doesnt use Grammar)
	Circuit *c;			//basic object of ATPG generator
    Sat_Solver *s;			//sat_solver

//*********** statistics
	int total_vectors_count=0;	
	int bad_faults=0;		//redundant faults, they are really bad :)
  	int total_var_count=0;
	int total_clauses_count=0;
	int total_binary_clauses_count=0;
	int max_clauses_count=0;
	int max_vars_count=0;
	double ratio = 0; 
	double min_ratio = -1;
	double max_ratio = 0;
	int dc_count=0;

//*************************************************************************************************************
// Parsing arguments
//*************************************************************************************************************
if (argc==1)
  {
   help();
   exit(0);
  } 
  
  
for ( int i = 1; i < argc; i++ ){
   if ( strcmp ( argv[i],"-h" ) == 0 ){
	  help();
	  exit(0);	
	}
    if ((i==argc-1) && (!in_bench_set)){   
		file_bench_in.open(argv[i]);
		benchName=argv[i];
		if(!file_bench_in.is_open()){
	  	  	cerr << "Cant open bench file: " << argv[i] << endl;
			return -1;
		} 	
		in_bench_set=true; 
    }else
		if ( strcmp ( argv[i],"-n" ) == 0 ){
		  if ( i+1<argc ){
             file_bench_in.open(argv[++i]);
			 benchName=argv[i];
			 if (!file_bench_in.is_open()){
				cerr << "Cant open bench file: " << argv[i] << endl;	
			   	return -1;
			 }		
			 in_bench_set = true;			
		   }else{
			  cerr << "Name of bench file after -n expected." << endl;
			  return -1;
		   }
		}
		////////////////////////////////////////////
		else if ( strcmp ( argv[i],"-W" ) == 0 ){
		  if ( i+1<argc ){
              i++; 
		      fltI = atoi ( argv[i] );
		        
          }else{
		     cerr << "Output mode after -W expected." << endl;
		     return -1;
		  }
                        	
		}	
		///////////////////////////////////////////////
		
        ////////////////////////////////////////////
		// povoleni DC
		else if ( strcmp ( argv[i],"-DC" ) == 0 ){
			DCenable=1;
		}
		// presimulace enable
        else if ( strcmp ( argv[i],"-PS" ) == 0 ){
			presimEnable=1;
		}
		// sort enable
		else if ( strcmp ( argv[i],"-S" ) == 0 ){
		  if ( i+1<argc ){
              i++; 
		      sortEnable = atoi ( argv[i] );
          }else{
		     cerr << "Output mode after -S expected." << endl;
		     return -1;
		  }
                        	
		}	


		///////////////////////////////////////////////
		else
		if ( strcmp ( argv[i],"-t" ) == 0 ){
		  if ( i+1<argc ){
			 file_test_out.open (argv[++i], fstream::out | fstream::app );
			 streamOut=argv[i];
			 if (!file_test_out.is_open()){
				cerr << "Cant open bench file: " << argv[i] << endl;	
			   	return -1;
			 }		
			 in_out_set = true;			
		   }else{
			  cerr << "Name of output file after -t expected." << endl;
			  return -1;
		   }
		}


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



		else {
		    cerr << "Unknown argument: " << argv[i] << endl;
		    return -1;
		}				
}

if (!in_bench_set){
   cerr << "Bench file not specified"  << endl;	
   return -1;
}	

if (!in_out_set){
   cerr << "Output file not specified"  << endl;	
   return -1;
}	


//double parse_arguments = cpuTime();

//*************************************************************************************************************
// Parsing file with bench
//*************************************************************************************************************
	
    if (p.parse_bench ( file_bench_in )!=0){
	  cerr << "Wrong .bench file, could not be parsed" <<endl;
	  return -1;
		
	}
    file_bench_in.close();	

	
//*************************************************************************************************************
// Creating circuit structure and initialising Faults
//*************************************************************************************************************
	c= new Circuit();
	if (c->read_circuit( p )!=0){
	  cerr << "Wrong bench file" << endl;
	  return -1;
	}	

cout << " SETUP FINISHED " << endl;

//////////////////////////////////////////////////////////
/****** atalanta init *************/

  Atalanta *simulation=new Atalanta();
  simulation->simulationSet(benchName);
  string minTest;
  
  bitCount =c->get_input_count()-1;
  tmpBit=c->get_input_count()-1;


  cout <<"prvni : " << fltI <<endl;
  ///////////////////////////////////
  startatpg=clock();
  //////////// inicialiyace debug souboru ////
  patName=benchName;
  patName[0]='_';
  file_patterns_out.open (patName , fstream::out | fstream::app );
	 if(!file_patterns_out.is_open() ){
		cerr << "Cant open file with patterns: "<<  endl;	
	  	return -1;
	 }	

 
  cout <<"fault size : " << simulation->hopeFaultList.size() <<endl;


  // inicializace - mapuju indexy!!!!!
  for(int i=0;i<c->gate_count;i++){
	  for(int j=0;j<c->gate_count;j++){
  	    if(simulation->net[j]->symbol->symbol.compare(c->int_to_name(i))==0){
           simulation->net[j]->index = i;
		   //cout << c.int_to_name(i) << " - index - " << i <<endl;
		}
	 }
  }
	
 cout << "mapping finished ..." <<endl;

///  OHODNOCENI A ROVNANI 
 int inpCount;

 if(sortEnable==1 || sortEnable==2){
   for(int i=0;i<simulation->hopeFaultList.size();i++){
      simulation->setFltIndex(i);
      from = simulation->findex->Findex;
      to   = simulation->findex->Tindex;
      typ  = simulation->findex->Typ;
      inpCount=0;

	  cnf = c->fault_to_cnf(from,to,typ,use_active_vars);
	
	   for(int k=0;k<cnf->get_var_count();k++){
         if((*cnf->vars)[k]->input==1)inpCount++;
	   }

	   //simulation->setPrice(i,cnf->get_var_count());
	   if(sortEnable==1){
	      simulation->setPrice(i,inpCount);
	   }else if(sortEnable==2){
          simulation->setPrice(i,6000-inpCount);
	   }
     delete cnf;
   }
 
   simulation->maxSort();
   if(sortEnable==1){
	 cout<<"Razeni seznamu poruch ENABLED(MAX -> MIN)"<<endl;
   }else if(sortEnable==2){
     cout<<"Razeni seznamu poruch ENABLED(MIN -> MAX)"<<endl;
   }

 }else{
   cout << "Razeni seznamu poruch - DISABLED"<<endl;
 }
 
 if(presimEnable==1)cout <<"Presimultion ENABLED" << endl;
 else cout <<"Presimultion DISABLED" << endl; 
 
 if(DCenable==1)cout <<"DC adding - ENABLED" << endl;
 else cout <<"DC adding - DISABLED" << endl; 
 


dcTest=0;
dcSet=0;
int shiftStr=0;
int pc;
int fSx=simulation->hopeFaultList.size();
srand(time(0));

 
 //exit(0);
//////////////////////////////////////////////

/************************************/
 ////////////////////////////////////////////////////////////
 while(simulation->hopeFaultList.size()>0){ //c.has_fault() )		//vyskocim breakem kdyz atalante dojdou chzbz
	

    satisfied = true; //if cnf representing fault can be satisfied
   
   if(vecCount==0){ // na zacatku vyberu prvni index a vyresim sat ...
       simulation->setFltIndex(fltI);
       
       from = simulation->findex->Findex;
       to   = simulation->findex->Tindex;
       typ  = simulation->findex->Typ;
      
	   vecCount++;
       // vytvoreni poruchy z indexu
	   cnf = c->fault_to_cnf(from,to,typ,use_active_vars);
	   
     	
       // reseni satu
       satM = new minisat2::Minisat_Solver();
       satisfied = satM->set_cnf(*cnf);

       if(satM->has_preprocess())satisfied=satM->preprocess();
       if(satisfied)satisfied=satM->solve();
       if(satisfied){ 
	      satM->assign_solution(*cnf);
	      ivector= c->inputs_to_vector(*cnf);
		  minTest.resize(ivector->length());
          for(int i=0; i<ivector->length(); i++){
	         if((*ivector)[i]==l_false)minTest[i]='0';
             if((*ivector)[i]==l_true)minTest[i]='1';
	         if((*ivector)[i]==l_dc){
				 minTest[i]='-';
	         }
          }
	      delete ivector;
		  

////// kdyz je prvni bit DC nahradim abzch yvetsil pocet poruch co vektor detekuje
		  //simulace prvniho vektoru
		  if(minTest[0]=='-'){
			int max01=simulation->simulationVctX(minTest);
			simulation->resetFL();
			minTest[0]=='1';
            int pom1=simulation->simulationVctX(minTest);
            simulation->resetFL();
			minTest[0]=='0';
            int pom0=simulation->simulationVctX(minTest);
            simulation->resetFL();

            if(pom0!=0 && pom0>pom1){
			   if(pom0>max01){
                  minTest[0]=='0';
			   }else{
                  minTest[0]='-'; // nahradim cimkoli nezmeni se to
			   }
			}else{
  			   if(pom1!=0 && pom1>pom0){
				 if(pom1>max01){
                    minTest[0]=='1'; 
				 }else{
                    minTest[0]='-'; // nahradim cimkoli nezmeni se to
				 }
		  	  }
		    }
		  }
//////////////////////////////////////////////

       coveredTmp+=simulation->simulationVct(minTest);
	   //cout << minTest <<"     * "<< coveredTmp <<"/"<<simulation->hopeFaultList.size()<< endl;
	   //file_patterns_out << minTest << endl;
	   // cout << minTest <<endl;
   	   bitCount++;
	   tmpBit++;
	   vecCount++;
     }
     delete cnf;
     delete  satM;
	 ////////////////////////////////////////////// 
	 // pokud je prvni resena porucha redundantni uknocim a je treba vzbrat jinou
	 if(!satisfied){
	   cout <<"Prvni zpracovavana porucha je NEDETEKOVATELNA - zvolte jinou"<<endl;
	   exit(0);
	 }
     ////////////////////////
  
    shiftStr=0; 

   }else{


	   //file_test_out
     minTest=c->shiftStr(minTest,&file_test_out);  // vysunuju bity vlevo
     // minTest=c->shiftStrR(minTest,&file_test_out); // vysunuju bity vpravo
     //if(((int)(rand() / (double) 2))%2)minTest=c->shiftStrX(minTest,'0',&file_test_out);
     //else minTest=c->shiftStrX(minTest,'1',&file_test_out);
	 shiftStr++;
	 tmpBit++;
     pc=0;

///////////////////////////////////////////////////////
	// povoluju presimulaci
	if(presimEnable==1){ 
	   pc= simulation->simulationVctX(minTest); 
	   if(pc!=0){	
          ////// kdyz je prvni bit DC nahradim abzch yvetsil pocet poruch co vektor detekuje
          //simulace prvniho vektoru
		  if(minTest[0]=='-'){
		    int max01=simulation->simulationVctX(minTest);
		    simulation->resetFL();
		    minTest[0]=='1';
            int pom1=simulation->simulationVctX(minTest);
            simulation->resetFL();
		    minTest[0]=='0';
            int pom0=simulation->simulationVctX(minTest);
            simulation->resetFL();

            if(pom0!=0 && pom0>pom1){
		       if(pom0>max01){
                  minTest[0]=='0';
		       }else{
                  minTest[0]='-'; // nahradim cimkoli nezmeni se to
		       }
		    }else{
  		       if(pom1!=0 && pom1>pom0){
		         if(pom1>max01){
                    minTest[0]=='1'; 
		         }else{
                    minTest[0]='-'; // nahradim cimkoli nezmeni se to
		         }
		       }
		    }
		 }
         /////////////////////////////////////////////
	     coveredTmp+=simulation->simulationVct(minTest);
		 shiftStr=0;
		 vecCount++;
	     //cout << minTest <<"    *--- "<< pc <<"/"<<simulation->hopeFaultList.size()<<" - "<< tmpBit<<endl;vecCount++;
	   }
	 }
/////////////////////////////////////////////////////////////////////////////////////	
	   if(pc==0){
            shiftStr=0;   
	        for(int indeX=0;indeX<simulation->hopeFaultList.size();indeX++){ //projdu poruchz a ykusim sat pro urcitz vektor

		        // beru postupne poruchy a testuju jestli jsou splnitelne pro posunuty test vector
		        simulation->setFltIndex(indeX);
                from = simulation->findex->Findex;
                to   = simulation->findex->Tindex;
                typ  = simulation->findex->Typ;
      
	   	        cnf = c->fault_to_cnf(from,to,typ,use_active_vars);

		         // nastavim v cnf promenne podle testovaciho vektoru z minula
		         inputSet=cnf->setInputs(minTest);//,*c);    
                 // reseni satu
                 satM = new minisat2::Minisat_Solver();
                 satisfied = satM->set_cnf(*cnf);
                 if(satM->has_preprocess() && inputSet[0]!='u')satisfied=satM->preprocess();
                 if(satisfied && inputSet[0]!='u')satisfied=satM->solve();
                 if(satisfied && inputSet[0]!='u'){ 
	                satM->assign_solution(*cnf);
			        ivector= c->inputs_to_vector(*cnf);
                    newV.resize(ivector->length());
                    for(int i=0; i<ivector->length(); i++){
			 	       if(inputSet[i]=='-' && minTest[i]=='-'){
	                       if((*ivector)[i]==l_false )newV[i]='0';
                           if((*ivector)[i]==l_true  )newV[i]='1';
						   if((*ivector)[i]==l_dc ){
							   newV[i]='-';
                               //if(((int)(rand() / (double) 2))%2)newV[i]='0';
	                           //else newV[i]='1';
						   }
				       }else{
				 	       newV[i]=minTest[i];
				       }
                    }
			
	                ////////////////////////////////////////////////////////////
					// pridavam DC do vektoru
					if(DCenable==1){
			  		  newV=cnf->setDCInputs(newV,minTest,from,to,typ);
			          dcTest+=cnf->dcTest;
			          dcSet+=cnf->dcSet;
					}
			        //cout << "t/dc : " <<dcTest <<"/"<<dcSet<<endl;
                    /////////////////////////////////////////////////////////////////////////////
			        delete ivector;
		         }else satisfied=false;

 		         delete  satM;
		         delete cnf;		
	       
		         if(satisfied ){ // jestlize je pro nejakou poruchu a dane nastaveni splnitelna pak odsimuluj nastaveni a prerus hledani
			        int jjk=0;
                    
  					////// kdyz je prvni bit DC nahradim abzch yvetsil pocet poruch co vektor detekuje
          		    //simulace prvniho vektoru
		            if(minTest[0]=='-'){
			          int max01=simulation->simulationVctX(minTest);
			          simulation->resetFL();
			          minTest[0]=='1';
                      int pom1=simulation->simulationVctX(minTest);
                      simulation->resetFL();
			          minTest[0]=='0';
                      int pom0=simulation->simulationVctX(minTest);
                      simulation->resetFL();

                      if(pom0!=0 && pom0>pom1){
			            if(pom0>max01){
                          minTest[0]=='0';
			            }else{
                          minTest[0]='-'; // nahradim cimkoli nezmeni se to
			            }
		       	      }else{
  			            if(pom1!=0 && pom1>pom0){
				          if(pom1>max01){
                             minTest[0]=='1'; 
				          }else{
                             minTest[0]='-'; // nahradim cimkoli nezmeni se to
				          }
		  	           }
		              }
		          }
                  //////////////////////////////////////////////

                  ///////////////////////////////////////////////
   		          jjk=simulation->simulationVct(newV);
			      coveredTmp+=jjk;
				  if(vecCount%10==0)cout << "fault list size : "<< simulation->hopeFaultList.size()<<endl;
				  //cout << newV <<"     * "<< jjk << "/"<<simulation->hopeFaultList.size()<<" - "<< tmpBit<<endl;
				  //file_patterns_out << newV <<"     * "<< jjk << endl;
			      bitCount++;
			      ////////////////////////////////////////////////
	              vecCount++;
                  shiftCount=0;
                  minTest=newV;
 
			      if(jjk==0 && pc==0){
			        cout<<"je tam 0poruch pokrzto!!!!"<<endl;
				    exit(0);
			      }else{
                   //  file_patterns_out << jjk << " poruch -> " << newV << endl;
			      }

        		   break;
		    }else{
		         shiftCount++;
			 
                   // jestlize jsem vzsunul vsechnz bity a nejde stale splnit = je nesplnitelna -> odmazu
		           if(shiftCount>=c->get_input_count()*simulation->hopeFaultList.size()){
			          cout << "zbyle poruchy jsou redundantni?? "<<endl;
				      bitCount=bitCount - c->get_input_count();
				      tmpBit=tmpBit-c->get_input_count();
                      endatpg=clock();
				      cout <<"...vysunuto : "<<bitCount<<"/"<<tmpBit<< "doba reseni : " << (endatpg-startatpg)/CLOCKS_PER_SEC << " sekund  ; dctest/dcset"<< dcTest<<"/"<<dcSet <<","<<simulation->hopeFaultList.size()<<","<<vecCount<<endl;
                      file_patterns_out << fltI <<","<<tmpBit<<","<<simulation->hopeFaultList.size()<<","<<vecCount<<","<< dcTest<<","<<dcSet<<","<<(endatpg-startatpg)/CLOCKS_PER_SEC<<","<<endl;
                      // file_patterns_out << fltI <<","<<bitCount<<","<<simulation->hopeFaultList.size()<<","<<vecCount<<","<<(endatpg-startatpg)/CLOCKS_PER_SEC<<","<<endl;
				      delete c;
                      delete simulation;
					  file_test_out.close();
				      file_patterns_out.close();
				      return 0;
			       }
		        }
        }/// konec for???
    
	   }//konec if PC
  
   } // konec if ???

   // cout <<"vzsunuto bitu : "<< bitCount <<" ; zbyva : "<< simulation->hopeFaultList.size() << " ; pokryto : "<< coveredTmp <<" , from : "<<from<<" ,to : "<<to <<" ,typ : "<<typ<<endl;
   //cout <<"vysunuto : "<<bitCount<<"/"<<tmpBit<< "doba reseni : " << (endatpg-startatpg)/CLOCKS_PER_SEC << " sekund  ; dctest/dcset"<< dcTest<<"/"<<dcSet <<endl;
   // file_patterns_out << fltI <<","<<bitCount<<","<<simulation->hopeFaultList.size()<<","<< dcTest<<","<<dcSet<<","<<(endatpg-startatpg)/CLOCKS_PER_SEC<<","<<endl;

   if(simulation->hopeFaultList.size()>0)continue;// break;
 
} // konec while


endatpg=clock();
//for(int j=0;j<newV.length();j++)file_test_out << newV[j];


cout <<"vysunuto : "<<bitCount<<"/"<<tmpBit<< "doba reseni : " << (endatpg-startatpg)/CLOCKS_PER_SEC << " sekund  ; dctest/dcset"<< dcTest<<"/"<<dcSet <<","<<simulation->hopeFaultList.size()<<endl;
//file_patterns_out << fltI <<","<<bitCount<<","<<simulation->hopeFaultList.size()<<","<< dcTest<<","<<dcSet<<","<<(endatpg-startatpg)/CLOCKS_PER_SEC<<","<<endl;
//file_patterns_out << fltI <<","<<bitCount<<","<<simulation->hopeFaultList.size()<<","<<vecCount<<","<<(endatpg-startatpg)/CLOCKS_PER_SEC<<","<<endl;
file_patterns_out << fltI <<","<<tmpBit<<","<<simulation->hopeFaultList.size()<<","<<vecCount<<","<< dcTest<<","<<dcSet<<","<<(endatpg-startatpg)/CLOCKS_PER_SEC<<","<<endl;


delete simulation;
delete c;
file_test_out.close();
file_patterns_out.close();
return 0;    
};






 /////////////////////////////////////////////////////
   //maximaliyace poruch
 //////////////////////////////////////////////////////
	/*	  int max01=simulation->simulationVctX(minTest);
		  //cout <<"max 01 : "<< max01<<endl;
		  int pom0=0;
		  int pom1=0;
		  simulation->resetFL();
		  for(int kl=0;kl<minTest.length();kl++){ 
			 if(minTest[kl]=='-'){
                minTest[kl]='1';
				pom1=simulation->simulationVctX(minTest);
				//cout << "pom1 " << kl <<" : " << pom1<<endl;
				simulation->resetFL();
				minTest[kl]='0';
				pom0=simulation->simulationVctX(minTest);
				//cout << "pom0 " << kl <<" : " << pom0 <<endl;;
                simulation->resetFL();
				if(pom0!=0 && pom0>pom1){
					if(pom0>max01){
                       max01=pom0;
					}else{
                       minTest[kl]='-';
					}

				}else{
					if(pom1!=0 && pom1>pom0){
					  if(pom1>max01){
                         max01=pom1;
					  }else{
                         minTest[kl]='-';
					  }
					}
				}



			 }
		  }
       
		 // cout <<"max 01 -1 : "<< max01<<endl;
*/
////////////////////////////////////////////////////



