#include "logic.h"
#include "gate.h"

namespace sat_atpg {

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

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

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

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

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

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


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

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


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

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

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

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

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

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



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

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

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

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

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

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

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

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

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

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


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



Cnf::Cnf(const Cnf& cnf):c(cnf.c),delete_vars(true)
{ 
 vars=new My_Array<My_Var*>(cnf.vars->length());
 for(int i=0; i< cnf.clauses.length(); i++)
   clauses.insert(new My_Clause((cnf.clauses)[i]));
 for(int i=0; i< cnf.vars->length(); i++)
   vars->insert(new My_Var((*cnf.vars)[i]));
 binary_clause_count = cnf.binary_clause_count;
}

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

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


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

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

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

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

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


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

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


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

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

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

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


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


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


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

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



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



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