//#include <iostream>
#include "minisat2Solver.h"
#include "minisatDcSolver.h"
#include "gate.h"
#include "macros.h"


#include <map>
#ifdef _WIN32
#include <ctime>


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

#include <sys/time.h>
#include <sys/resource.h>
#include <unistd.h>

static inline double cpuTime(void) {
    struct rusage ru;
    getrusage(RUSAGE_SELF, &ru);
    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
#endif

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


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





//this function was created for testing memory leaks in MINISAT, no leaks were found
/*
void test_Simpsolver () 
{
 for (int i=0;i<5000;i++)
   {
    cout << i << endl;
    SimpSolver *simpSolver = new SimpSolver;
    		for ( int j=0; j<10000;j++)
		{
			simpSolver->newVar();
		}
		vec<Lit> lits;
		for ( int j=0;j<10000;j++ )
		{
			lits.clear();
			for ( int k=0; k< 40; k++ )
			{
				lits.push ( ((k % 3)==0  ) ? Lit (((j+k)*53)%10000) : ~Lit (((j+2*k)*13)%10000) );
			}
			if ( !simpSolver->addClause ( lits ) )
			{
				
                   	}
		}
     delete simpSolver;
   }
}
*/

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	
//*********** parameters
	bool in_bench_set = false;	//bench file was given
	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
	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;

//*************************************************************************************************************
// Time 
//*************************************************************************************************************


double   cpu_time = cpuTime();

//*************************************************************************************************************
// 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]);
		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]);
                           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],"-f" ) == 0 )
		{
			if ( i+1<argc )
			{
				file_faults_in.open ( argv[++i] );
				if ( !file_faults_in.is_open() )
				   {
					cerr << "Cant open file with faults: " << argv[i] << endl;	
					return -1;
				   }
				in_faults_set = true;
					
			}
			else 
			{
			   cerr << "Name of file with faults after -f expected." << endl;
			   return -1;
			  }
                }
	else if ( strcmp ( argv[i],"-F" ) == 0 )
		{
			if ( i+1<argc )
			{
				file_faults_out.open ( argv[++i] );
				if ( !file_faults_out.is_open() )
				  {
				   cerr << "Cant open file with faults: " << argv[i] << endl;		
				   return -1;
				  }	
				out_faults_set = true;
					
			}
			else
			{
			   cerr << "Name of file with faults after -F expected." << endl;
			   return -1;
			  }
                }
	else if ( strcmp ( argv[i],"-t" ) == 0 )
		{
			if ( i+1<argc )
			{
				
				file_patterns_out.open ( argv[++i] );
				if ( !file_patterns_out.is_open() )
				  {
					cerr << "Cant open file with patterns: " << argv[i] << endl;	
				  	return -1;
				  }	
				out_patterns_set=true;
			}
			else
			{
			   cerr << "Name of file with patterns after -t expected." << endl;
			   return -1;
			  }
		}
 	else if ( strcmp ( argv[i],"-P" ) == 0 )
		{
			if ( i+1<argc )
			{
			    out_report_set=true;
			    report = ++i;	
			}
			else
			{
			   cerr << "Name of file with report after -P expected." << endl;
			   return -1;
			  }
		}
	else if ( strcmp ( argv[i],"-U" ) == 0 )
		{
			if ( i+1<argc )
			{
				
				file_redundant_out.open ( argv[++i] );
				if ( !file_redundant_out.is_open() )
				  {
					cerr << "Cant open file for redundant files: " << argv[i] << endl;	
				  	return -1;
				  }	
				out_redundant_set=true;
			}
			else
			{
			   cerr << "Name of file for redundant files after -U expected." << endl;
			   return -1;
			  }
		}
		else if ( strcmp ( argv[i],"-W" ) == 0 )
		{
		  if ( i+1<argc )
			{
                	i++; 
		        output_mode = atoi ( argv[i] );
		        if ((output_mode<0)||(output_mode>3))
			  {
                           cerr << "Output mode (-W) out of range (should be 0,1,2,3)" << endl; 	 
			  }
                       }
		  else 
		    {
		     cerr << "Output mode after -W expected." << endl;
		     return -1;
		    }
                        	
		}
		else if ( strcmp ( argv[i],"-D" ) == 0 )
		{
			if ( i+1<argc )
			{
                i++; 
		        n = atoi ( argv[i] );
		        diagnostic_mode=true; 
			}
			else 
			   {
				cerr << "Number of vectors per fault after -D expected." << endl;
			   	return -1;
			   }
			
		}
		else if ( strcmp ( argv[i],"-m" ) == 0 )
		{
			if ( i+1<argc )
			{
                	i++; 
		        convert_dc = atoi ( argv[i] );
		        if ((convert_dc<0) ||  (convert_dc >2))
                          {
			    cerr << "0,1 or 2 after parameter -m expected" << endl;
                            return -1;
                          }
			}
			else
			{
				cerr << "Type of DC conversion after -m expected." << endl;
			   	return -1;
			}
			
			
		}
		else if ( strcmp ( argv[i],"-e" ) == 0 )
		{
			if ( i+1<argc )
			{
                	i++; 
		        expand_mode = atoi ( argv[i] );
		        if ((expand_mode<0) || (expand_mode >2))
                          {
			    cerr << "0,1 or 2 after parameter -e expected" << endl;
                            return -1;
                          }
			}
			else
			{
			   cerr << "Type of expansion after -e expected." << endl;
			   return -1;
			}
		}
		else if ( strcmp ( argv[i],"-s" ) == 0 )
		{
			use_dc_solver = true;
		}
		else if ( strcmp ( argv[i],"-l" ) == 0 )
		{
			print_circuit = true;
		}
		else if ( strcmp ( argv[i],"-A" ) == 0 )
		{
            		all_iter = true;    
			diagnostic_mode=true;
		}
		else if ( strcmp ( argv[i],"-a" ) == 0 )
		{
            		report_append = true;
		}
		else if ( strcmp ( argv[i],"-N" ) == 0 )
		{
            	compaction = false;
		}
		else if ( strcmp ( argv[i],"-c" ) == 0 )
		{
		 simple_compaction = false;
		} 
		else if ( strcmp ( argv[i],"-ch" ) == 0 )
		{
            	  use_checkpoints = true;
		}
		else if ( strcmp ( argv[i],"-V" ) == 0 )
		{
            	  use_active_vars = false;
		}
		else if ( strcmp ( argv[i],"-d" ) == 0 )
		{
            	  export_to_dimacs = true;
	        	if ( i+1<argc )
			{
			 dimacs_path= argv[++i];
			}
			else
			{
			   cerr << "Name of path/file after -d expected." << endl;
			   return -1;
			}
		}
		else if ( strcmp ( argv[i],"-r" ) == 0 )
		{
		  if ( i+1<argc )
			{
                	i++; 
		        remove_covered = atoi ( argv[i] );
		        if ((remove_covered<0) ||  (remove_covered >2))
                          {
			    cerr << "0,1 or 2 after parameter -r expected" << endl;
                            return -1;
                          }
			}
		  else
		    {
			cerr << "Type of fault removing after -r 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;
  }	
//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
//*************************************************************************************************************
	if (c.read_circuit( p )!=0)
	  {
	   cerr << "Wrong bench file" << endl;
	   return -1;
	  }	
			;
        if (print_circuit)
          {
	   c.print(file_report_out);
 	  }			
//double parse_time = cpuTime();
	if ( in_faults_set )
	{
		p.parse_faults (file_faults_in);
		file_faults_in.close();
		c.read_faults ( p );
	}
	else
	  c.init_faults(use_checkpoints);
	if (out_faults_set)
	  {
	   c.print_faults(file_faults_out);
	   file_faults_out.close();
	  }
if (export_to_dimacs)
  {
   if (c.get_total_faults()==1)
     {
       single_fault = true;
       file_export_out.open(dimacs_path.c_str());
       if (!file_export_out.is_open())
          {
           cerr << "Cant open the file " << dimacs_path <<" for export to dimacs" << endl;   
           return -1;          
	  } 
     }
   else
     single_fault = false; 
 }
	
//double fault_time = cpuTime();

//*************************************************************************************************************
// Procesing faults
//*************************************************************************************************************
double total_fault_convert=0;
double total_to_minisat=0;
double total_minisat_solve=0;
double total_fault_process=0;
double total_compact_time=0;

	while ( c.has_fault() )		
	{
double start_fault = cpuTime();
double minisat_solve;
		satisfied = true; //if cnf representing fault can be satisfied
//*************************************************************************************************************
// Converting Fault to cnf
//*************************************************************************************************************
 Cnf* cnf = c.fault_to_cnf(use_active_vars);

 int var_local =  cnf->get_var_count();
 int clause_local = cnf->get_clause_count();	
 double ratio_local = ((double)clause_local)/((double)var_local);
 if (min_ratio < 0)
   {
	min_ratio = ratio_local;
        max_ratio = ratio_local;
   }
 else
   {
    if (min_ratio > ratio_local)
      {
        min_ratio = ratio_local;
      }
    if (max_ratio < ratio_local)
      {
	 max_ratio = ratio_local;
      }
   }
 ratio = ratio + ratio_local;
 if (max_vars_count < var_local)
   {
    max_vars_count = var_local;
   }
 total_var_count = total_var_count + var_local;
 if (max_clauses_count < clause_local)
   {
    max_clauses_count = clause_local;
   }
 total_clauses_count = total_clauses_count + clause_local;
 total_binary_clauses_count = total_binary_clauses_count + cnf->get_binary_clause_count();
 double fault_convert = cpuTime();
//*************************************************************************************************************
// To DIMACS 
//*************************************************************************************************************
if (export_to_dimacs)
  {
   if (!single_fault)
      {
       file_export_out.open((dimacs_path+"/"+c.fault_to_dimacs_string()+".cnf").c_str());
       if (!file_export_out.is_open())
          {
           cerr << "Cant open the file " << dimacs_path+"/"+c.fault_to_dimacs_string()+".cnf" <<" for export to dimacs" << endl;   
           return -1;          
	  }
      } 
   cnf->to_dimacs(file_export_out);
   delete cnf;	
   file_export_out.close();
   c.remove_fault();
   continue;	
  }	
  
//*************************************************************************************************************
// Simplify cnf 
//*************************************************************************************************************

  //cnf->remove_strong_components(); not implemented  

//*************************************************************************************************************
// Using MiniSAT Solver
//*************************************************************************************************************
		if (use_dc_solver)	
		  {
                    s = new minisat_dc::Minisat_Solver();
                  }
                else
                  {
                   s = new minisat2::Minisat_Solver();
		  } 
		satisfied = s->set_cnf(*cnf);
		
double to_minisat = cpuTime();
		
		int iter=1; //computes number of founded vectors for this fault
		Test_Vector *current=0;
		if ( satisfied ) //if no conflict in adding clauses
		{
			do
			{     
                                if (s->has_preprocess()) 
				//if (export_to_dimacs)
				//simpSolver->toDimacs((c->fault_to_string()+".dim").c_str());
                                   satisfied=s->preprocess();
				//simpSolver->toDimacs((c->fault_to_string()+"_simp_"+".dim").c_str());
				//simplifies input
                                if (satisfied) 
				//runs Sat solver
				  satisfied=s->solve();
minisat_solve = cpuTime();
//cout << (satisfied ? "SATISFIABLE\n": "UNSATISFIABLE\n");
//*************************************************************************************************************
// Processing result of MiniSAT
//*************************************************************************************************************
				if ( satisfied )
                                   { 
					{
					 s->assign_solution(*cnf);
					}
					if ((!use_active_vars) && ((expand_mode==2) || (remove_covered==2)))
					  {
					   c.add_active_vars(*cnf);
					  } 
					if ( expand_mode == 2 )
					{
						c.find_dc ( *cnf );		
					}
					else if ( expand_mode == 1 )
					{
					  if ((n>iter) || (all_iter))
					    {
					     Cnf temp = (*cnf);
					     c.cnf_dc(temp);
					     c.copy_input_vars(*cnf,temp);
					    }		
					  else
					    {
						c.cnf_dc(*cnf);
					    }				 		  			 
							
					}
					current = new Test_Vector ( c,*cnf );	
					
					//current->print(cout);cout<<endl;
					//cnf->print(cout);
					//c.simulate(*cnf);
                                       	if (diagnostic_mode) 
					   {
					     result.insert(current);
					     if ((n>iter) || all_iter)		
					        {
						 My_Array<int>* inputs = c.get_inputs();
					     	 My_Clause *newClause = new My_Clause(inputs->length());	
					         for ( int i=0;i<inputs->length();i++ )	
					           {
						    l_type value = cnf->get_var ((*inputs)[i] )->value;
						    if (value!=l_dc )
                                                      {
						       newClause->add_var((*inputs)[i],value==l_true?false:true);	
						      }
						   }	
						 delete inputs;
						 cnf->add_clause(newClause);			
						 if (s->can_add_clause_later())	
  						   satisfied = s->add_clause(*newClause);
                                                 else
  						   {
						    delete s;
						    if (use_dc_solver)	
		  					{
                    					 s = new minisat_dc::Minisat_Solver();
                  					}
                				    else
                  					{
                   					 s = new minisat2::Minisat_Solver();
		  					}	
						   satisfied=s->set_cnf(*cnf);
						  }	 
                                          	}
                     			 
					    }
				}
			}
			while ( satisfied && ( ( iter++ < n ) || all_iter ) );
		}
                else //solver not run
                 {
		  minisat_solve=to_minisat;
                 }	
                    
		 if (diagnostic_mode)
			{	
				if (result.length()==0)
				  {
					bad_faults++;
				  }
				else
				  {
				   total_vectors_count = result.length()+total_vectors_count;
				  }	
                    		if ((out_patterns_set) && (output_mode>0))
				        {
                                          for (int i=result.length()-1;i>=0;i--)
					    { 
					      Test_Vector *current = result[i];
					      dc_count = dc_count + current->count_dc_inputs();
					      if (convert_dc==CONVERT_TO_ONE)
						current->dc_convert(l_true);
				              else if (convert_dc==CONVERT_TO_ZERO)
					   	current->dc_convert(l_false);
                                              if (output_mode==3)   		
					        file_patterns_out << i <<":";
					      current->print(file_patterns_out,true,output_mode==2?true:false);
	                 		      file_patterns_out << endl;
					    }    
                                         }
 		    	        while (result.length()>0)
				  {
				   delete result[0];
				   result.remove(0);
				  }		
		    		c.remove_fault();   
		 	}
		else
		  {
		   if (satisfied)	
			{			
//if (expand){Cnf &heur = cnf->expand_2();}
               /*          if (!vectors[i]->tests_fault()) for testing only
				{ 
				  #if DEBUG > 0
				  if (expand)
				  {						
				  old_vectors[i]->print(*file_output);
				  file_output << endl;
				  }		
				  #endif	
                                  vectors[i]->print(*file_output);
				  (*file_output) << endl;
				} 
			 else*/
			   //int index = choose_vector(vectors);
 			   if (remove_covered==0)
			     {
                               c.remove_fault();
                             }	
                           else if (remove_covered==1)    
			      {	
				c.remove_dominance(cnf->get_vars());
                              }
                           else //remove_covered==2
			      {	
                               c.remove_risky(cnf->get_vars());
                              } 
			   if ((compaction)&&(simple_compaction))
			     {
				double start_compaction = cpuTime();
                   		add_vector_to_result(result,current);
				total_compact_time = total_compact_time + (cpuTime() - start_compaction); 
                 	     }
               		  else
                 	     {
                   		result.insert(current);
                 	     }		
			 ++total_vectors_count;
			}
	            else 
		      {	
	               if (out_redundant_set)
                         {
			  file_redundant_out << c.fault_to_string() << endl; 	
			 }
			c.remove_fault();
			++bad_faults;	
		      }
	 	}	
           	delete s;
           	delete cnf;
//for(int i=0;i<vectors.length();i++)
//  delete vectors[i];
double end_fault = cpuTime();	
total_fault_convert=total_fault_convert+(fault_convert-start_fault);
total_to_minisat = total_to_minisat+(to_minisat-fault_convert);
total_minisat_solve= total_minisat_solve+(minisat_solve-to_minisat);
total_fault_process= total_fault_process +(end_fault-minisat_solve);

}
if ((!(diagnostic_mode)) && (compaction)&&(!simple_compaction))
{
  double start_compaction = cpuTime();	
  compact(result);
  total_compact_time = cpuTime()-start_compaction;	
}
else
  {
	total_fault_process = total_fault_process - total_compact_time;
  }	
if (convert_dc==CONVERT_TO_ONE)
  for (int i=0;i<result.length();i++)	
    result[i]->dc_convert(l_true);
else if (convert_dc==CONVERT_TO_ZERO)
  for (int i=0;i<result.length();i++)	
    result[i]->dc_convert(l_false);
int vector_count;	//vector count afer compaction  	
if (diagnostic_mode)
  {
   vector_count = total_vectors_count;
  }
else	
  {
   vector_count = result.length();
   for (int i=0;i<result.length();i++)
     {
      dc_count = dc_count + result[i]->count_dc_inputs();
     }
  }
if (out_patterns_set)
  {
   if ((output_mode>0) && (!diagnostic_mode)) 
     {
      for (int i=0;i<result.length();i++)
        {  
         result[i]->print(file_patterns_out,true,output_mode==2?true:false);
         delete result[i];
         file_patterns_out << endl;
        }
     }
   file_patterns_out.close();
  }
 if (out_redundant_set)
   {
    file_redundant_out.close();
   }


double total_time = cpuTime() - cpu_time;

if (out_report_set)
  {
   if (report_append)
      file_report_out.open ( argv[report],fstream::app);
   else
      file_report_out.open ( argv[report] );
   if ( !file_report_out.is_open() )
 	{
	 cerr << "Cant open file for report: " << argv[report] << endl;	
	 return -1;
	}
   if (report_append)
     {
      	file_report_out <<  c.get_total_faults()<< "\t"
 			<<  c.get_covered_faults()<< "\t"
			<<  bad_faults << "\t"
			<<  total_vectors_count << "\t"
			<<  vector_count << "\t"
			<< ((vector_count==0)?0:(100*((float)(dc_count))/((float)(vector_count*c.get_input_count())))) << "\t"
 			<< total_time <<"\t"
			<< endl; 
     }
  else
    {	
file_report_out<<"Inputs:						" << c.get_input_count() << endl;
file_report_out<<"Outputs:					" << c.get_output_count()<< endl;
file_report_out<<"Gates:						" << c.get_gate_count()-c.get_input_count()<< endl;

file_report_out<<"Faults:						" << 
c.get_total_faults()<<endl;
file_report_out<<"Faults removed (dominance):			" << c.get_covered_faults()<<endl;
file_report_out<<"Faults not covered:				"<<
bad_faults<<endl;
file_report_out<<"Total vectors:					" << 
total_vectors_count<<endl;
file_report_out<<"Total vectors after compaction			" <<
vector_count << endl;
file_report_out<<"Average dc ratio:				" 
    << ((vector_count==0)?0:(((float)(dc_count))/((float)(vector_count*c.get_input_count()))))<< endl;
file_report_out<<"								" << endl;

file_report_out <<"Total time:					" << total_time <<" s "<< endl; 
//file_report_out <<"Parse arguments:                                        " << parse_arguments-cpu_time << endl;
//file_report_out <<"Parse bench:                                            " << parse_time-parse_arguments<< endl;
//file_report_out <<"Fault init:                                             " << fault_time-parse_time<< endl;
//file_report_out <<"Fault_convert:                                          " << total_fault_convert<<endl;
//file_report_out <<"Convert to minisat:                                     " << total_to_minisat<<endl;
//file_report_out <<"Minisat solving:                                        " << total_minisat_solve<<endl;
//file_report_out <<"Fault process:                                          " << total_fault_process<<endl;
//file_report_out <<"Compaction time:					   " <<total_compact_time<<endl;

file_report_out <<"Average count of clauses in CNF:		" << ((total_vectors_count==0)?0: (((double)total_clauses_count) / (double) total_vectors_count)) << endl;
file_report_out <<"Maximum of clauses in CNF:			"<< max_clauses_count << endl;
file_report_out <<"Average count of variables in CNF:		" << ((total_vectors_count==0)?0: (((double)total_var_count) / ((double) total_vectors_count))) << endl;
file_report_out <<"Maximum of vars in CNF:				"<< max_vars_count << endl;

file_report_out <<"Average count of binary clauses in CNF:		" << ((total_vectors_count==0)?0: (((double)total_binary_clauses_count) / ((double) total_vectors_count))) << endl;
file_report_out <<"Average clauses / vars ratio:			"<< ((total_vectors_count==0)?0: (((double)ratio) / (double) total_vectors_count)) << endl;	 
file_report_out <<"Maximum of clauses / vars ratio:		"<< max_ratio<<endl;
file_report_out <<"Minimum of clauses / vars ratio:		"<< min_ratio<<endl; 
file_report_out.close();
}

}
};





