#include "gate.h"
#include "macros.h"

namespace sat_atpg {

Fault_List::Fault_List() 
{
 head = new Fault_Head(tail = new Fault_Tail(0));
 tail->prev=head;
 count = 0;
}


void Fault_List::print_all(ostream& stream)
{
 Fault_Item * f= head;
 while (f!=tail)
   {
    f->print(stream);
    f=f->next;
   }
 }
void Fault::print(ostream& stream) {
        stream << from->get_name();
        if (to != 0) 
          stream << "->" << to->get_name();
        if (kind) 
           stream << " /1" << endl;
        else 
           stream << " /0" << endl;       
}

void Gate::active_path(Cnf &cnf)
{
 int var_active = get_var_active(cnf);
 My_Clause* newClause;
 if (output.length()>0)
   {
    newClause = new My_Clause(output.length()+1);
    newClause->add_var(var_active,false); 
    for(int i=0; i<output.length();i++)
      newClause->add_var(output[i]->get_var_active(cnf),true);
    cnf.add_clause(newClause);
   }
    newClause = new My_Clause(3);
    newClause->add_var(var_active,false);
    newClause->add_var(get_var(cnf),true);
    newClause->add_var(get_var_faulty(cnf),true);
    cnf.add_clause(newClause);
    
    newClause = new My_Clause(3);
    newClause->add_var(var_active,false);
    newClause->add_var(get_var(cnf),false);
    newClause->add_var(get_var_faulty(cnf),false);
    cnf.add_clause(newClause);
                 
}

My_Array<Gate*> &Gate::get_outputs()
{
 return output;
}

My_Array<Gate*> &Gate::get_inputs()
{
 return input;
}
  
void Gate::add_output(Gate *g)
{
     output.insert(g);
     output_ones.insert(0);
     output_zeros.insert(0);		
}  



void Gate::forwards(My_Stack<Gate> &s, My_Stack<Gate> &b)
{
 if (output.length()==0)
   {
    if (state==FORWARDS)
      this->set_state(BOTH);
    else
      this->set_state(FAULTYBACK);                      
    b.push(this);
   } 
 else
   for(int i=0; i<output.length();i++)
     if (output[i]->get_state() == WHITE)
        { 
         output[i]->set_state(FORWARDS);
         s.push(output[i]);
        }  
}

void Gate::backwards(My_Stack<Gate> &s,Cnf &c,bool active_vars)
{
 for(int i=0; i<input.length();i++) 
   {
    switch (input[i]->get_state()) {
      case WHITE:s.push(input[i]);input[i]->set_state(BACKWARDS);break;
      case FORWARDS:s.push(input[i]);input[i]->set_state(BOTH);break;
      case BACKWARDS: break;
      case BOTH: break; 
      case FAULTY: s.push(input[i]);input[i]->set_state(FAULTYBACK);break;
      case FAULTYBACK:break;	
    }
   }
 this->to_cnf(c);
 this->to_cnf_faulty(c,active_vars);    
}

Gate::~Gate()
{
}

bool Gate::var_exists()
{
 return var>-1;
}

int Gate::get_var(Cnf &cnf)
{
 if (!var_exists())
   var = cnf.newVar(index,false);
 return var;
}

          
int Gate::get_var_faulty(Cnf &cnf)
{
 if (var_faulty<0)
   var_faulty = cnf.newVar(index,true);
 return var_faulty;
}

int Gate::get_var_active(Cnf &cnf)
{
 if (var_active<0)
   var_active = cnf.newVar(-index,false);
 return var_active;
}

int Gate::get_var_active()
{
 return var_active;
}

void Gate::init_faults_eq(Fault_List& f)
{
 if (output.length()==0)
   {
    permanent_one = f.add_fault(this,0,true);
    permanent_zero = f.add_fault(this,0,false);
   }  
 else if (output.length()==1)
   {
    if (!(output[0]->sensitive_input(true)))
      {
       permanent_one = f.add_fault(this,0,true);
      }
    if (!(output[0]->sensitive_input(false)))       
      {
       permanent_zero = f.add_fault(this,0,false);  
      }
   }  
 else
   {	  
    for(int i=0;i<output.length();i++)
    {
     if (!output[i]->sensitive_input(true))         
       {
        output_ones[i]=f.add_fault(this,output[i],true);
	
       }
     if (!output[i]->sensitive_input(false))         
       {
        output_zeros[i]=f.add_fault(this,output[i],false); 
       }
    }
    permanent_one = f.add_fault(this,0,true);	
    permanent_zero = f.add_fault(this,0,false);  	
  }
}

void Gate::set_faulty(Gate *g, bool _fault)
{
 this->state = FAULTY;
 for(int i=0; i<input.length();i++)
   {
    if (input[i]==g)
      {
       faulty = i;
       fault = _fault;
       break;
      }
  } 
}

void N_naryGate::to_cnf(Cnf &cnf)
{
 int *input_vars = new int[input.length()];
 for(int i=0; i<input.length(); i++)
   input_vars[i] = input[i]->get_var(cnf);
 to_cnf(cnf,input_vars,input.length(),this->get_var(cnf));
 delete []input_vars;  
}

void N_naryGate::to_cnf_faulty(Cnf &cnf, bool active_vars)
{
int *input_vars = new int[input.length()];
switch (state)  {
 case BOTH: for (int i=0;i<input.length();i++)
              input_vars[i] = input_backwards(i,cnf); 
            this->to_cnf(cnf,input_vars,input.length(),get_var_faulty(cnf));
	    if (active_vars)
     		{	
      		this->active_path(cnf);
     		} 
            break;
            
 case FAULTYBACK:{ 
   My_Clause *c = new My_Clause(1);
   c->add_var(input[faulty]->get_var_faulty(cnf),fault);
   cnf.add_clause(c);
   if (active_vars)
     {	
      this->active_path(cnf);
     }   
   for (int i=0;i<input.length();i++)
     if (i == faulty)
       input_vars[i] = input[i]->get_var_faulty(cnf);
     else
       input_vars[i] = input_backwards(i,cnf);
    this->to_cnf(cnf,input_vars,input.length(),get_var_faulty(cnf));  
   }break;
 case BACKWARDS: break;
}
delete [] input_vars;
}

void BinaryXor::to_cnf(Cnf &cnf,int a,int b, int c)
{
 //( a or b or -c) and (a or -b or c) and (-a or b or c) and (-a or -b or -c)
 
 //( a or b or -c)
 My_Clause* clause = new My_Clause(3);
 clause->add_var(a,true);
 clause->add_var(b,true);
 clause->add_var(c,false);
 cnf.add_clause(clause);
 
 //(a or -b or c)
 clause = new My_Clause(3);
 clause->add_var(a,true);
 clause->add_var(b,false);
 clause->add_var(c,true);
 cnf.add_clause(clause);

 //(-a or b or c)
 clause = new My_Clause(3);
 clause->add_var(a,false);
 clause->add_var(b,true);
 clause->add_var(c,true);
 cnf.add_clause(clause);

 //(-a or -b or -c)
 clause = new My_Clause(3);
 clause->add_var(a,false);
 clause->add_var(b,false);
 clause->add_var(c,false);
 cnf.add_clause(clause);
}

void BinaryXor::count_dc_inputs(Cnf &cnf)
{
 dc_true_count = 0;
 dc_false_count = 0;
}	 



void Not::to_cnf(Cnf &cnf)
{
 //( a or b) and (-a or -b)
  int a = this->input[0]->get_var(cnf);   
  int b = this->get_var(cnf); 
  to_cnf(cnf, a, b);
}

void Not::count_dc_inputs(Cnf &cnf)
{
 dc_true_count = 0;
 dc_false_count = 0;
}


void Not::to_cnf(Cnf &cnf, int a, int b)
{
  //( a or b) and (-a or -b)
 //(a or b)
 My_Clause* clause = new My_Clause(2);
 clause->add_var(a,true);
 clause->add_var(b,true);
 cnf.add_clause(clause);

 //(-a or -b)
 clause = new My_Clause(2);
 clause->add_var(a,false);
 clause->add_var(b,false);
 cnf.add_clause(clause);
}

void Not::to_cnf_faulty(Cnf &cnf,bool active_vars)
{
switch (state) {
 case FAULTYBACK: {My_Clause *c = new My_Clause(1);
                  c->add_var(this->input[0]->get_var_faulty(cnf),fault); 
                  cnf.add_clause(c);
                   if (active_vars)
     			{	
      			 this->active_path(cnf);
     			} 
                  } 
		 this->to_cnf(cnf,input[0]->get_var_faulty(cnf),this->get_var_faulty(cnf)); 
                   
		  break;
 case BOTH: this->to_cnf(cnf,input_backwards(0,cnf),this->get_var_faulty(cnf));
             if (active_vars)
     		{	
      		this->active_path(cnf);
     		} 
            break;
 case BACKWARDS:break;
}  
}

void Buffer::to_cnf(Cnf &cnf)
{

 //( a or b) and (-a or -b)
  int a = this->input[0]->get_var(cnf);   
  int b = this->get_var(cnf); 
  to_cnf(cnf, a, b);
 
}


void Buffer::to_cnf(Cnf &cnf,int a,int b)
{
    // (a or -b) and (-a or b)
   //(a or -b)
   My_Clause* clause = new My_Clause(2);
   clause->add_var(a,true);
   clause->add_var(b,false);
   cnf.add_clause(clause);

   //(-a or b)
   clause = new My_Clause(2);
   clause->add_var(a,false);
   clause->add_var(b,true);
   cnf.add_clause(clause);
}

void Buffer::to_cnf_faulty(Cnf &cnf,bool active_vars)
{
 switch (state) {
 case FAULTYBACK: { My_Clause *c = new My_Clause(1);
                    c->add_var(this->input[0]->get_var_faulty(cnf),fault); 
                    cnf.add_clause(c);
                     if (active_vars)
     			{	
      			this->active_path(cnf);
     			} 
                    this->to_cnf(cnf,input[0]->get_var_faulty(cnf),this->get_var_faulty(cnf));   
                    break;}
 case BOTH: this->to_cnf(cnf,input[0]->get_var_faulty(cnf),this->get_var_faulty(cnf));
             if (active_vars)
     		{	
      		 this->active_path(cnf);
     		}  
	     break;
 case BACKWARDS:break;
   }
}

void Buffer::count_dc_inputs(Cnf &cnf)
{
 dc_true_count = 0;
 dc_false_count = 0;
}  

void BinaryXor::to_cnf(Cnf &cnf)
{
  int a = this->input[0]->get_var(cnf);   
  int b = this->input[1]->get_var(cnf);
  int c = this->get_var(cnf); 
  to_cnf(cnf, a, b,c);
}
 
void BinaryXor::to_cnf_faulty(Cnf& cnf,bool active_vars)
{
 switch (state) {
 case FAULTYBACK: { My_Clause *c = new My_Clause(1);
                    c->add_var(this->input[faulty]->get_var_faulty(cnf),fault); 
                    cnf.add_clause(c);
			if (active_vars)
     			{	
      			this->active_path(cnf);
     			}
		    if (faulty==0)
	  		this->to_cnf(cnf,input[0]->get_var_faulty(cnf),input_backwards(1,cnf),this->get_var_faulty(cnf));
 		    else
			this->to_cnf(cnf,input_backwards(0,cnf),input[1]->get_var_faulty(cnf),this->get_var_faulty(cnf)); 
		   break;}
 case BOTH: this->to_cnf(cnf,input_backwards(0,cnf),input_backwards(1,cnf),this->get_var_faulty(cnf));
             if (active_vars)
     		{	
      		this->active_path(cnf);
     		}  
	    break;
 case BACKWARDS:break;
   }
}   



void N_naryAnd::to_cnf(Cnf &cnf,int *input_vars,int length,int result)
{
 My_Clause* clause = new My_Clause(length+1);
 for(int i=0;i<length;i++)
   clause->add_var(input_vars[i],false);  
 clause->add_var(result,true);
 cnf.add_clause(clause);

 for(int i=0;i<length;i++)
   {
    clause = new My_Clause(2);
    clause->add_var(input_vars[i],true);
    clause->add_var(result,false);
    cnf.add_clause(clause);
   }
}

void N_naryGate::count_dc_inputs(Cnf &cnf)
{
    dc_true_count = 0;
    dc_false_count = 0;

if (this->can_change_inputs(cnf))//
  {
   if (differs(cnf))
     return;
   if (fault)
     {
      for(int i=0;i<faulty;i++)
        count_dc_input(input[i],cnf);
      for(int i=faulty+1;i<input.length();i++)
        count_dc_input(input[i],cnf);
      }
   else
     {
       for (int i=0; i<input.length();i++)
         {
          count_dc_input(input[i],cnf);
         }
     }
   this->change_dc_count();        
  }
}

void N_naryGate::count_dc_input(Gate *g,Cnf &cnf)   
{
 if (g->var_active_exists())
    {
      if (g->differs(cnf))
         return;
    }                
l_type l= cnf.get_var(g->get_var())->value;

if (l == l_true)  
   {
     dc_true_count++;
   }
else if (l==l_false) 
        {
          dc_false_count++;
        }
} 

bool N_naryAnd::can_change_inputs(Cnf &cnf)
{
 return (cnf.get_var(var)->value == l_false);
}
bool N_naryNand::can_change_inputs(Cnf &cnf)
{
 return (cnf.get_var(var)->value == l_true);
}
bool N_naryOr::can_change_inputs(Cnf &cnf)
{
 return (cnf.get_var(var)->value == l_true);
}
bool N_naryNor::can_change_inputs(Cnf &cnf)
{
 return (cnf.get_var(var)->value == l_false);
}

void N_naryAnd::change_dc_count()
{
  if (dc_false_count>0)
     --dc_false_count;
}

void N_naryNand::change_dc_count()
{
  if (dc_false_count>0)
     --dc_false_count;
}
void N_naryOr::change_dc_count()
{
  if (dc_true_count>0)
     --dc_true_count;
}
void N_naryNor::change_dc_count()
{
  if (dc_true_count>0)
     --dc_true_count;
}


void N_naryNand::to_cnf(Cnf &cnf,int *input_vars,int length,int result)
{
 My_Clause* clause = new My_Clause(length+1);
 for(int i=0;i<length;i++)
   clause->add_var(input_vars[i],false);  
 clause->add_var(result,false);
 cnf.add_clause(clause);

 for(int i=0;i<length;i++)
   {
    clause = new My_Clause(2);
    clause->add_var(input_vars[i],true);
    clause->add_var(result,true);
    cnf.add_clause(clause);
   }
}

void N_naryOr::to_cnf(Cnf &cnf,int *input_vars,int length,int result)
{
 My_Clause* clause = new My_Clause(length+1);
 for(int i=0;i<length;i++)
   clause->add_var(input_vars[i],true);  
 clause->add_var(result,false);
 cnf.add_clause(clause);

 for(int i=0;i<length;i++)
   {
    clause = new My_Clause(2);
    clause->add_var(input_vars[i],false);
    clause->add_var(result,true);
    cnf.add_clause(clause);
   }
}

void N_naryNor::to_cnf(Cnf &cnf,int *input_vars,int length,int result)
{
 My_Clause* clause = new My_Clause(length+1);
 for(int i=0;i<length;i++)
   clause->add_var(input_vars[i],true);  
 clause->add_var(result,true);
 cnf.add_clause(clause);

 for(int i=0;i<length;i++)
   {
    clause = new My_Clause(2);
    clause->add_var(input_vars[i],false);
    clause->add_var(result,false);
    cnf.add_clause(clause);
   }
}

void Input::print(std::ostream &stream)
{
 stream << "Input: " << this->name << endl;
}

Circuit::Circuit():faults(0),gates(0),outputs(0),a_outputs(0),gate_max(0),index_gate(0),output_count(0), gate_count(0),cnf(0),total_faults(0),covered_faults(0){}

int Circuit::read_circuit(Parser &parser)
{
 faults = new Fault_List();
 My_Queue<Gate_token>& inputs = parser.get_inputs();
 My_Queue<Gate_token>& inners = parser.get_gates();
 My_Queue<Gate_token>& out = parser.get_outputs();
 
 index_gate = inputs.get_count();
 gate_max = index_gate + inners.get_count();
 gates  = new pGate[gate_max];
 outputs = new pGate[out.get_count()];
 while (!inputs.is_empty())
    {
     Gate *g=new Input(inputs.top()->name);
     			
     this->add_gate(g);
     delete inputs.top();	
     inputs.pop();
    }
 while (!inners.is_empty())
   {
    Gate_token *t = inners.top();
    pGate *p = new pGate[t->input_count];
    bool found = true;
    for(int i=0; i< t->input_count; i++)
      {
	p[i]=find_gate(t->inputs[i]);
	if (p[i]==0)
	  {
	   found=false;	
	   break;
	  }	  	
      }										 
    if (found)   
      {
       Gate *newGate;		
       if (t->input_count == 1)
          {
           switch(t->kind)
            {
             case NOT : newGate = new Not(t->name, p[0]);break; 
             case BUFF : newGate = new Buffer(t->name, p[0]);break;
             default: cout << "error: "; t->output(cerr); cout << "wrong gate type" << endl; return -1;
		    
            }
           }
       else if (t->kind == XOR)
         {
          if (t->input_count == 2)
            {
             newGate = new BinaryXor(t->name, p[0], p[1]);
            }
          else
            {
             cerr << "error: "; t->output(cerr); cout << "wrong gate type" << endl; return -1;
            }
         }
       else
          {
           switch(t->kind)
              {
               case AND : newGate = new N_naryAnd(t->name, p ,t->input_count ); 
               break;
               case NAND : newGate = new N_naryNand(t->name, p , t->input_count); break;
	           case OR : newGate = new N_naryOr(t->name, p , t->input_count); break; 
               case NOR : newGate = new N_naryNor(t->name, p , t->input_count); break;
               default: cerr << "error: "; t->output(cerr); cout << "wrong gate type" << endl; return -1;
              }
          }
     this->add_gate(newGate);
     for (int i=0; i< t->input_count;i++)
     p[i]->add_output(newGate);
     inners.pop();
     delete t;	
    }
   else
    inners.first_to_end();
   delete []p;	
  }
 while (!out.is_empty())
    {
     Gate *g = find_gate(out.top()->name); 
     this->add_gate_output(g);
     delete out.top(); 
     out.pop();
    }
 //this -> print(cout);
 return 0;
}

Gate* Circuit::find_gate(string name)
{ 
 std::map<string,Gate*>::iterator iter = gate_map.find(name);
  	if( iter == gate_map.end() ) 
	   {
	 	return 0;
	   }		
	return iter->second;
}

void Circuit::read_faults(Parser &p)
{
 My_Queue<Fault_token>& queue = p.get_faults();
 while (!queue.is_empty())
   {
    Fault_token* ft = queue.top();
    queue.pop();
    Gate* from = find_gate(ft->from);
    if (from==0)
      {
       cerr << "Fault " << ft->from;
       if (ft->to!="")
         cerr << " -> " << ft->to; 
       if (ft->polarity)
         cerr << " /1 ";
       else
         cerr << " /0 ";		       
       cerr <<"refers to nonexistent gate: "<< ft->from << endl;
       exit(-1);
      }
    Gate* to = 0;	
    if (ft->to!="")
      {      
       to = find_gate(ft->to);
       if (to==0)
         {
       	  cerr << "Fault " << ft->from;
       	  if (ft->to!="")
            cerr << " -> " << ft->to;        
          if (ft->polarity)
         	cerr << " /1 ";
          else
         	cerr << " /0 ";	 
          cerr<<" refers to nonexistent gate: "<< ft->to << endl;
          exit(-1);
      	 }
      }
    from->add_fault(faults->add_fault(from,to,ft->polarity));
   }
 total_faults = faults->get_count();  
} 


void Circuit::add_gate(Gate *p)
{
 gates[gate_count]=p;
 p->set_index(gate_count++);
 gate_map[p->get_name()]=p;
}
void Circuit::print(ostream &stream)
{
 for(int i=0; i<gate_count;i++)
   gates[i]->print(stream);
} 
void Circuit::init()
{
for (int i=0; i<gate_count;i++)
  gates[i]->init();
if (a_outputs!=0)
  delete a_outputs;
};

void Circuit::init_faults(bool ch_p)
{
 if (ch_p)
   {
     for (int i=gate_count;i>=index_gate;i--)
	gates[i]->fanout_faults(*faults);	
     for (int i=index_gate-1; i>=0;i--)
       ((Input*)(gates[i]))->input_chp_faults(*faults);  
   }	 
else	
  {
   for (int i=gate_count-1; i>=0; i--)
     {
      gates[i]->init_faults_eq(*faults);
     }
  } 
total_faults = faults->get_count();
}

void Circuit::print_faults(ostream &stream)
{
 if (faults != 0)
     faults->print_all(stream);
} 

Cnf* Circuit::fault_to_cnf(Fault &f, bool active_vars)
{
 init();
 //cout << "Resolving: ";
 //cout << "Result:" << endl;
 Cnf* cnf = new Cnf(*this);
 My_Clause *newClause;
 My_Stack<Gate> s_forward;
 My_Stack<Gate> s_backward;
 if (f.from->get_output_count()==0)
   {
     newClause = new My_Clause(1);
     newClause->add_var(f.from->get_var_active(*cnf),true);
     s_backward.push(f.from);		
   }	
else
  {
    if (f.to == 0)
     {
      newClause = new My_Clause(f.from->get_output_count());     
      My_Array<Gate*> &g = f.from->get_outputs();
      for(int i=0;i<g.length();i++)
       {
        g[i]->set_faulty(f.from,f.kind);
        newClause->add_var(g[i]->get_var_active(*cnf),true);
        s_forward.push(g[i]);       
       }   
     }
   else
   {
    f.to->set_faulty(f.from,f.kind);
    s_forward.push(f.to);
    newClause = new My_Clause(1);
    newClause->add_var(f.to->get_var_active(*cnf),true);
   }
  }
 //Setting gate in front of fault to oposite value (for s_a_0 true...)
  cnf->add_clause(newClause);
  newClause = new My_Clause(1);
  newClause->add_var(f.from->get_var(*cnf),not f.kind);
  cnf->add_clause(newClause); 
//DFS 
 while (!s_forward.is_empty()) 
   {
    Gate *g=s_forward.top();
    s_forward.pop();	
    g->forwards(s_forward,s_backward);
   }
 int active_outputs = s_backward.get_count();
 this->a_outputs = new My_Array<Gate*>(active_outputs);
 newClause = new My_Clause(active_outputs);
 Gate *g = s_backward.first();
 do {
     if (!active_vars)
       {
        g->active_path(*cnf);
       }	
     a_outputs->insert(g);
     newClause->add_var(g->get_var_active(*cnf),true);
     g = s_backward.next();
    }
 while (g!=0);
 
cnf->add_clause(newClause);	
while (!s_backward.is_empty()) 
   {
    Gate *g=s_backward.top();
    s_backward.pop();	
    g->backwards(s_backward,*cnf,active_vars);
   }
return cnf;
}   

void Circuit::print_inputs(ostream& stream,Cnf &cnf)
{
 for (int i=0;i<index_gate;i++)
   {
    if (gates[i]->var_exists())
      {
       l_type out = cnf.get_var(gates[i]->get_var())->value;
       stream << out;
      }
    else     
      stream << "x";      
   }
} 

void Circuit::print_outputs(ostream& stream,Cnf &cnf)
{
 for (int i=0;i<output_count;i++)
   {
    if (outputs[i]->var_exists())
       { 
        l_type out = (cnf.get_var(outputs[i]->get_var())->value);
        stream << out;
       }
    else
       stream << "x";
   }
} 



  

/*!
    \fn Circuit::get_inputs()
 */
My_Array<int> *Circuit::get_inputs()
{
    My_Array<int>  *array= new My_Array<int>(index_gate);
    for(int i=0;i<index_gate;i++)
      {
        if (gates[i]->var_exists())
          array->insert(gates[i]->get_var());
      }
  return array;
}


/*!
    \fn Circuit::find_dc()
 */
void Circuit::find_dc(Cnf &cnf)
{
 bool active_output = false;
 for(int i=gate_count-1; i>=0;i--)
   {	
    if (gates[i]->var_exists())
     {
      if (cnf.get_var(gates[i]->get_var())->value==l_dc)
        continue;
      if (gates[i]->var_active_exists())
        {
	 	  	
         if (cnf.get_var(gates[i]->get_var_active())->value != l_true)     
           { 
	    gates[i]->dc_outputs(cnf);
            if (cnf.get_var(gates[i]->get_var())->value!=l_dc)
              gates[i]->count_dc_inputs(cnf);
	    		     
           }
	 else
	   {
	    if (gates[i]->get_output_count()==0)
              {
                if (active_output)
                  {
	 	   cnf.set_value(gates[i]->get_var(),l_dc);
	          }
	       else
		 {
  		  active_output = true;
	 	 }
	      }				
	   }
        }
      else
        {
	 gates[i]->dc_outputs(cnf);
	 if (cnf.get_var(gates[i]->get_var())->value!=l_dc)	
	   gates[i]->count_dc_inputs(cnf);
        }
      }
  }
}

void Circuit::add_active_vars(Cnf &cnf)
{
My_Stack<Gate> stack;	
for (int i=0;i<a_outputs->length();i++)
{
 Gate *h= (*a_outputs)[i]; 
  if (h->differs(cnf) && (!h->var_active_exists()))	
    {
	stack.push(h);
    }	
  while (!stack.is_empty())
      {
	Gate *g = stack.top();
	stack.pop();
	cnf.set_value(g->get_var_active(cnf),true);
        My_Array<Gate*> g_inputs = g->get_inputs();
	   for(int i =0; i<g_inputs.length();i++)
	     {
	      if (g->differs(cnf))
	        {
			stack.push(g_inputs[i]);
	        }						 		
     	     }	
      } 
}
}

/*!
    \fn Gate::var_active_exists()
 */
bool Gate::var_active_exists()
{
    return var_active>-1;
}




/*!
    \fn Gate::dc_outputs()
 */
void Gate::dc_outputs(Cnf &cnf)
{
 bool dc = true;
 for(int i=0;i<output.length();i++)
   {
    if (!output[i]->is_dc_input(cnf,cnf.get_var(var)->value))
      {
        dc = false;
        break;
      }
   }
 if (dc)
   {
     if ((cnf.get_var(var)->value)==l_true)
       for(int i=0;i<output.length();i++)
   	 output[i]->dec_dc_true_count(cnf);
     else
       for(int i=0;i<output.length();i++)
         output[i]->dec_dc_false_count(cnf);
     cnf.set_value(var,l_dc);
   }
}





/*!
    \fn Gate::is_dc_input(Cnf &cnf, l_type in)
 */
bool Gate::is_dc_input(Cnf &cnf, l_type in)
{
 if (!var_exists())
   return true;
 if (cnf.get_var(var)->value == l_dc)
   return true;
 if (var_active_exists())
   {
    if (cnf.get_var(var_active)->value==l_true)
      return false;
   }
 if (in == l_true)
   {
    return (dc_true_count>0);
   }
 return (dc_false_count>0);   
}





/*!
    \fn Gate::dec_dc_true_count(Cnf &cnf)
 */
void Gate::dec_dc_true_count(Cnf &cnf)
{
  if (var_exists())  
    {
      if (cnf.get_var(var)->value != l_dc)
       {
        dc_true_count--;
       }
    }
}

void Gate::dec_dc_false_count(Cnf &cnf)
{
  if (var_exists())  
    {
     if (cnf.get_var(var)->value != l_dc)
       {
        dc_false_count--;
       }
    }
}


void Input::count_dc_inputs(Cnf &cnf)
{
 dc_false_count = 0;
 dc_true_count = 0;
}


/*!
    \fn Circuit::inputs_to_vector(Cnf &cnf)
 */
My_Vector<l_type>* Circuit::inputs_to_vector(Cnf &cnf)
{
 My_Vector<l_type> *m_v = new My_Vector<l_type>(index_gate,l_true);
 for(int i=0; i<index_gate; i++)
   (*m_v)[i] = gates[i]->var_exists() ? cnf.get_var(gates[i]->get_var())->value : l_dc; 
 return m_v;
}

My_Vector<l_type>* Circuit::outputs_to_vector(Cnf &cnf)
{
 My_Vector<l_type> *m_v = new My_Vector<l_type>(output_count,l_true);
  for(int i=0 ; i<output_count; i++)
    {
     (*m_v)[i] = outputs[i]->var_exists() ? cnf.get_var(outputs[i]->get_var())->value : l_dc;
   }	 
 return m_v;
}

My_Vector<l_type>* Circuit::fault_outputs_to_vector(Cnf &cnf)
{
 My_Vector<l_type> *m_v = new My_Vector<l_type>(output_count,l_true);
  for(int i=0 ; i<output_count; i++)
  {
   (*m_v)[i] = outputs[i]->var_faulty_exists() ? cnf.get_var(outputs[i]->get_var_faulty())->value : l_dc;
 } 
 return m_v;
}

void Fault_List::remove_Fault() { 
delete top();
count--;
                }  

Fault_List::~Fault_List() { while (!is_empty()) remove_Fault();
			    delete head; delete tail;}

/*!
    \fn Gate::var_faulty_exists()
 */
bool Gate::var_faulty_exists()
{
    return var_faulty>-1;
}


/*!
    \fn Gate::get_var_faulty()
 */
int Gate::get_var_faulty()
{
   return var_faulty;
}



/*!
    \fn Fault_List::add_fault(Gate *_from,Gate *_to, bool _kind)
 */
Fault* Fault_List::add_fault(Gate *_from,Gate *_to, bool _kind)
{
    ++count;
    Fault *f = new Fault(_from,_to,_kind,head->next,head);
    head->next->prev = f;
    head->next = f;
    return f;	
}


/*!
    \fn Fault_Head::print(ostream &stream)
 */
void Fault_Head::print(ostream &stream)
{
  //stream << "Faults:";

}

void Fault_Tail::print(ostream &stream)
{
}


/*!
    \fn Fault_List::top()
 */
Fault* Fault_List::top()
{
   if (head->next!=tail)
     return (Fault*) head->next;
   else
     return 0;  
}


/*!
    \fn Circuit::remove_risky()
 */
void Circuit::remove_risky(My_Array<My_Var*> &vars)
{
 My_Stack<Gate> active_gates;
 Fault *f = faults->top();
 if (f->to==0)
   {
    active_gates.push(f->from);
    covered_faults--;   
   }
 else
   { 
    active_gates.push(f->to);
    f->from->delete_fault(f);
   }
while (!active_gates.is_empty())
   {
    Gate *g=active_gates.top();
    active_gates.pop();
    //cout << "Exploring: " << g->get_name() << endl; 			
    covered_faults = covered_faults+g->remove_risky(vars,active_gates);
   }    
}


void Circuit::remove_dominance(My_Array<My_Var*> &vars)
{
 Fault *f = faults->top();
 if (f->to == 0)
   {
    if	(f->from->get_output_count()==1) //no brench
      {
       covered_faults = covered_faults + f->from->get_outputs()[0]->remove_dominance(vars);	
      }
   }  
else
   { 
    covered_faults = covered_faults + f->to->remove_dominance(vars);
   }
delete f;    
}

int Gate::remove_dominance(My_Array<My_Var*> &vars)
{
 l_type value = vars[var]->value;
 int count = 0;
 if (output.length()==1)
   {
    count = output[0]->remove_dominance(vars);
   }
 if (value==l_true)
   {
    if (permanent_zero!=0)
      {
        delete permanent_zero;
        permanent_zero=0;
        count++;
      }
   }    	
 else
   {
    if (permanent_one!=0)
      {
        delete permanent_one;
        permanent_one=0;
        count++;
      }
   }
 return count;
}
/*!
    \fn Gate::add_fault(Fault *f)
 */
void Gate::add_fault(Fault *f)
{
 if (f->to==0)
   {
    if (f->kind)
      {
	permanent_one = f;
      }
    else
	{	
         permanent_zero = f;
	}      
   }
else
   {
     for(int i=0;i<output.length();i++)
       if (output[i]==f->to)
	  {
	   if (f->kind)
   	     output_ones[i]=f;
 	   else			
	     output_zeros[i]=f;
	   break;
	  }
	}			
}


/*!
    \fn Gate::remove_covered_faults(Cnf &cnf,My_Stack<Gates*> &m_s)
 */
int Gate::remove_risky(My_Array<My_Var*> &vars,My_Stack<Gate> &m_s)
{

 int active_inputs = 0;
 for (int i=0;i<input.length();i++)
    {
     if (input[i]->differs(vars))
	{
	  active_inputs++;
	  if (active_inputs>1)
            {
	     return 0;
            }	 
	}
    }
 int count = 0;	 		
 l_type var_value=vars[var]->value;
 if (var_value==l_true)
   {
    if (permanent_zero!=0)
      {
        delete permanent_zero;
        permanent_zero=0;
	count++;
      } 
   } 
else
   {
     if (permanent_one!=0)
       {
        delete permanent_one;
        permanent_one=0;
	count++;
       }
   } 
if (output.length()==1)
  {
	if (output[0]->var_active_exists() && (vars[output[0]->get_var_active()]->value==l_true) && (output[0]->get_state()!=VISITED))
	  {
	   output[0]->set_state(VISITED);	
	   m_s.push(output[0]);
	  }	
  }
else if (output.length()>1)
    {
     for (int i=0;i<output.length();i++)
       {
	if (vars[output[i]->get_var_active()]->value==l_true)
   	  {
           if (output[i]->get_state()!=VISITED)
             {
              output[0]->set_state(VISITED);	
	      m_s.push(output[0]);
	     }
	   if (var_value==l_true)
              {
                if (output_zeros[i]!=0)
     	         {
                  delete output_zeros[i];
                  output_zeros[i]=0;
		  count++;	
                  }  
              }            
          else
              {
                if (output_ones[i]!=0)
     	         {
                  delete output_ones[i];
                  output_ones[i]=0;
		  count++;
                  }  
              }
         }
     }
   }
 return count;
}    


/*!
    \fn Gate::delete_fault(Fault *f)
 */
void Gate::delete_fault(Fault *f)
{ 
 for(int i=0;i<output.length();i++)
      if (output[i]==f->to)
        {
         if (f->kind)
           {
            if (output_ones[i]!=0) 
              {
		delete output_ones[i];
            	output_ones[i]=0;
	      }	
            }
         else
           {
	    if (output_zeros[i]!=0)
              {	
               delete output_zeros[i];
               output_zeros[i]=0;
	      }	
 	   }
       }
}


Circuit::~Circuit () {
		delete faults;
                for (int i=0;i<gate_max;i++)
                   delete gates[i];
		delete []gates;
		delete []outputs;
		if (a_outputs!=0) delete a_outputs;	
}



/*!
    \fn Input::input_chp_faults(Fault_List &faults)
 */
void Input::input_chp_faults(Fault_List &faults)
{
   this->fanout_faults(faults);		
   permanent_one = faults.add_fault(this,0,true);
   permanent_zero = faults.add_fault(this,0,false);
   
}


/*!
    \fn Gate::fanout_faults(Fault_List &faults)
 */
void Gate::fanout_faults(Fault_List &faults)
{ 

if (output.length()>1)
     for (int i=0;i<output.length();i++)
        {
	 output_ones[i]=faults.add_fault(this,output[i],true);
	 output_zeros[i]=faults.add_fault(this,output[i],false);
        }
  
}


/*!
    \fn Circuit::fault_to_string()
 */
string Circuit::fault_to_string()
{
    return faults->top()->to_string();
}

string Circuit::fault_to_dimacs_string()
{
    return faults->top()->to_dimacs_string();
}


/*!
    \fn Fault::to_string()
 */
string Fault::to_dimacs_string()
{
 if (to==0)
   return from->get_name()+(kind?"_1":"_0");
 else
   return from->get_name()+"_"+to->get_name()+(kind?"_1":"_0");
}

string Fault::to_string()
{
 if (to==0)
   return from->get_name()+(kind?" /1":" /0");
 else
   return from->get_name()+"->"+to->get_name()+(kind?" /1":" /0");
} 


/*!
    \fn Circuit::add_gate_output1()
 */
void Circuit::add_gate_output(Gate *g)
{
 outputs[output_count++]=g;
}

/*!
    \fn Fault_List::get_count()
 */
int Fault_List::get_count()
{
  return count;
}

bool Gate::differs(Cnf& cnf)
{
 return (var_exists() && var_faulty_exists() && (cnf.get_var(var)->value != cnf.get_var(var_faulty)->value));
}

bool Gate::differs(My_Array<My_Var*> &vars)
{
 return (var_exists() && var_faulty_exists() && (vars[var]->value != vars[var_faulty]->value));
}


void BinaryXor::simulate()
{

 sim_value = input[0]->get_sim_value() ^ input[1]->get_sim_value();
 if ((state == FAULTY) || (state==FAULTYBACK))
   {
    l_type &l = *new l_type(fault);    
    if (faulty==0)
      sim_fault = l ^ input[1]->get_sim_fault();
    else
      sim_fault = input[0]->get_sim_fault() ^ l;
   }   
 else
   sim_fault = input[0]->get_sim_fault() ^ input[1]->get_sim_fault(); 
}
void N_naryAnd::simulate()
{
 sim_value = input[0]->get_sim_value();  
 for(int i=1; i<input.length();i++)
   sim_value = sim_value & input[i]->get_sim_value();
 sim_fault = l_true;
 if ((state == FAULTY) || (state==FAULTYBACK))
   {
    l_type &l = *new l_type(fault); 
    for(int i=0;i<faulty;i++)
      sim_fault = sim_fault & input[i]->get_sim_fault();
    sim_fault = sim_fault & l;
    for(int i=faulty+1;i<input.length();i++)
      sim_fault = sim_fault & input[i]->get_sim_fault();
   }
 else
   {   
    for(int i=0;i<input.length();i++)
      sim_fault = sim_fault & input[i]->get_sim_fault();
   }        
}
void N_naryNand::simulate()
{
   sim_value = input[0]->get_sim_value();  
 for(int i=1; i<input.length();i++)
   sim_value = sim_value & input[i]->get_sim_value();
 sim_fault = l_true;
 if ((state == FAULTY) || (state==FAULTYBACK))
   {
    l_type &l = *new l_type(fault);  
    for(int i=0;i<faulty;i++)
      sim_fault = sim_fault & input[i]->get_sim_fault();
    sim_fault = sim_fault & l;
    for(int i=faulty+1;i<input.length();i++)
      sim_fault = sim_fault & input[i]->get_sim_fault();
   }
 else
   {   
    for(int i=0;i<input.length();i++)
      sim_fault = sim_fault & input[i]->get_sim_fault();
   }        
 sim_value = ~sim_value;
 sim_fault = ~sim_fault;
}
void N_naryOr::simulate()
{
   sim_value = input[0]->get_sim_value();  
 for(int i=1; i<input.length();i++)
   sim_value = sim_value | input[i]->get_sim_value();
 sim_fault = l_false;
 if ((state == FAULTY) || (state==FAULTYBACK))
   {
    l_type &l = *new l_type(fault); 
    for(int i=0;i<faulty;i++)
      sim_fault = sim_fault | input[i]->get_sim_fault();
    sim_fault = sim_fault | l;
    for(int i=faulty+1;i<input.length();i++)
      sim_fault = sim_fault | input[i]->get_sim_fault();
   }
 else
   {   
    for(int i=0;i<input.length();i++)
      sim_fault = sim_fault | input[i]->get_sim_fault();
   }        
}
void N_naryNor::simulate()
{
   sim_value = input[0]->get_sim_value();  
 for(int i=1; i<input.length();i++)
   sim_value = sim_value | input[i]->get_sim_value();
 sim_fault = l_false;
 if ((state == FAULTY) || (state==FAULTYBACK))
   {
    l_type &l = *new l_type(fault);  
    for(int i=0;i<faulty;i++)
      sim_fault = sim_fault | input[i]->get_sim_fault();
    sim_fault = sim_fault | l;
    for(int i=faulty+1;i<input.length();i++)
      sim_fault = sim_fault | input[i]->get_sim_fault();
   }
 else
   {   
    for(int i=0;i<input.length();i++)
      sim_fault = sim_fault | input[i]->get_sim_fault();
   } 
 sim_value = ~sim_value;
 sim_fault = ~sim_fault;
}
void Buffer::simulate()
{
   sim_value = input[0]->get_sim_value();
   sim_fault = input[0]->get_sim_fault();   
}
void Not::simulate()
{
   sim_value = ~input[0]->get_sim_value();
   sim_fault = ~input[0]->get_sim_fault();   
}
  
void Circuit::simulate(Cnf &cnf)
{
 cout << "Simulating" << endl;
 for (int i=0;i<index_gate;i++)
   {
    gates[i]->set_sim_value(cnf);
     l_type l = gates[i]->get_sim_value();
     l_type l2 = gates[i]->get_sim_fault();	
      cout << gates[i]->get_name() << ": "<< l << " " << l2 <<" "<< gates[i]->get_state() << endl;	
   }
 cout << "Gates:" << endl;
 for (int i=index_gate;i<gate_max;i++)
  {
   gates[i]->simulate();
   l_type l = gates[i]->get_sim_value();
   l_type l2 = gates[i]->get_sim_fault();
    cout << gates[i]->get_name() << ": "<< l << " " << l2 <<" "<< gates[i]->get_state() << endl;
  
  }
 cout << "End of simulating" << endl;
}

void Gate::set_sim_value(Cnf &cnf)
{
if (var>0)
  sim_value = cnf.get_var(var)->value;
else
  sim_value = l_dc;
sim_fault = sim_value;
}     

/*!
    \fn Gate::print_dc_counts()
 */
void Gate::print_dc_counts(ostream &stream)
{
  stream << " " << dc_true_count << " " << dc_false_count;
}

void Circuit::cnf_dc(Cnf &cnf) 
{
 My_Array<l_type> backup(index_gate);
 int i,j;	
 for(i=0;i<index_gate;i++)
   if (gates[i]->var_exists())
     {
        int i_var = gates[i]->get_var(); 
	backup[i]=cnf.get_var(i_var)->value;
      	cnf.set_value(i_var,l_dc);
     }
 do
 {
   int count = cnf.get_clause_count();	
   for (i=0;i<cnf.get_clause_count();)
     {
      My_Clause *k = cnf.get_clause(i);
      bool removed = false;		
      for (j=0;j<k->get_var_count();)
	 {
	  if (cnf.get_var(k->var(j))->value == k->polarity(j))
	    {
	     cnf.remove_clause(i);
	     removed = true;
	     break;		
	    }
          else if (cnf.get_var(k->var(j))->value == (!k->polarity(j)))
		{
		 k->remove_var(j);
		}
	  else j++;
	 }
     if (removed)
	continue;	 	
     if (k->get_var_count()==0)
	{
	 cnf.remove_clause(i);
	 continue;
	}
     if	(k->get_var_count()==1)
	{
	  int g_index = cnf.get_var(k->var(0))->gate_index;	
	  cnf.set_value(k->var(0),backup[g_index]);
	  cnf.remove_clause(i);	
	  continue;
	}
     ++i;					 				 	
    }
  if (count == cnf.get_clause_count())
    {
     int chosen = this->choose_variable(cnf,backup);
     cnf.set_value(chosen,backup[cnf.get_var(chosen)->gate_index]);	
    } //if
   } //do				
while (cnf.get_clause_count()>0);
}

int Circuit::choose_variable(Cnf &cnf,My_Array<l_type> &backup) 
{     
     map<int,int> good;
     map<int,int> bad;	
     map<int, int>::iterator iter;
     map<int, int>::iterator iter_temp; 
     for (int i=0;i<cnf.get_clause_count();i++)
	{
     	 My_Clause *m= cnf.get_clause(i);
	 for (int j=0;j<m->get_var_count();j++)
	   {
	     int var_j=m->var(j);
	     if (backup[cnf.get_var(var_j)->gate_index] == m->polarity(j))
		{
		  iter = good.find(var_j);
        	  if( iter != good.end() ) 
                     {
			good[var_j]++;
                     }
		  else
                     {
			good[var_j]=1;
		     }
		}
	      else
		{
		  iter = bad.find(var_j);
        	  if( iter != bad.end() ) 
                     {
			bad[var_j]++;
                     }
		  else
                     {
			bad[var_j]=1;
		     } 
           	}
	   } 
        }
     int max = 0;
     int max_var = -1;
     for (iter = bad.begin(); iter!=bad.end(); iter++)
	{
	  iter_temp = good.find(iter->first);
          if (iter_temp == good.end())
	    {
	      int index = cnf.get_var(iter->first)->gate_index;			
	      backup[index] = ~backup[index];
            }
         good[iter->first]=iter->second;
        }	 
     for (iter = good.begin(); iter!=good.end(); iter++)
	{
         if (iter->second>max)
           {
	    max = iter->second;
	    max_var = iter->first;
           }
	} //for
return max_var;
}		


void Circuit::copy_input_vars(Cnf &dest,Cnf &source)
{
 for (int i=0; i< index_gate; i++)
   {
	if (gates[i]->var_exists())
	   {
	    dest.set_value(gates[i]->get_var(),source.get_var(gates[i]->get_var())->value);
	   }
   }
}							


}
