#ifndef GATE_H
#define GATE_H

#define WHITE 0
#define FORWARDS 1
#define BACKWARDS 2
//#define FAULTY 3
//////////////
const int FAULTY=50;
/////////////
#define BOTH 4
#define FAULTYBACK 5
#define VISITED 6

#include "logic.h"
#include "stack.h"
#include "parser.h"


#include <iostream>
#include <string>
#include <map>


namespace sat_atpg {

class Gate;
class Gate_element;

class Fault_Item {
public:
Fault_Item *prev,*next;
virtual~Fault_Item(){};
Fault_Item(Fault_Item *_next,Fault_Item* _prev):prev(_prev),next(_next){}
virtual void print(ostream &stream)=0;
};


class Fault_Head:public Fault_Item{
public:
 Fault_Head(Fault_Item *item):Fault_Item(item,0) {}
    virtual void print(ostream &stream);
};


class Fault_Tail:public Fault_Item{
public:
 Fault_Tail(Fault_Item *item):Fault_Item(0,item) {}
 virtual void print(ostream &stream);
};

class Fault:public Fault_Item {
	public:
		Gate *from,*to;	
		bool kind;
		Fault ( Gate *_from, Gate *_to,bool _kind,Fault_Item* _next, Fault_Item *_prev ) : Fault_Item(_next,_prev),from ( _from ),to ( _to ),kind ( _kind ){};
		void print_all ( ostream& stream );
		void print ( ostream& stream );
                ~Fault() {
                                  
			//cout<< "Delete: ";print(cout);
			remove();};
		void remove() {
			prev->next=next;
			next->prev=prev;
			}		;
    string to_string();
    string to_dimacs_string();	
};

class Fault_List 
{
public:        

 Fault_List();
 ~Fault_List(); 

 Fault_Head *head;
 Fault_Tail *tail;
 int count;	

 bool is_empty() {return head->next==tail;}
 Fault* add_fault(Gate *_from,Gate *_to, bool _kind);
 void remove_Fault(); 
                  	;
 void print_all(ostream &stream);
    Fault* top();
    int get_count();
};

typedef Gate* pGate;
typedef Fault* pFault;

class Gate_element
{
	public:
		Gate* data;
		Gate_element *next;
};


class Gate
{
	protected:

		
		string name;   		//name from ISCAS file
		int index;     		//index in array of gates
		int state;     		//state for algorithm visiting nodes
		My_Array<Gate*> output;  	//Array of outputs
		My_Array<Gate*> input;       //Array of inputs
		int faulty;		//index of faulty input
		bool fault;		//if is some input faulty
		int var;		//name of var for MiniSat
		int var_faulty;		//name of var for MiniSat - in circuit with fault
		int var_active;  //name of var for MinisSat - active path var
		l_type sim_value; //variable for simulation of non-faulty circuit
		l_type sim_fault; //variable for simulation of faulty circuit
		int dc_true_count;
		int dc_false_count;
		Fault *permanent_zero;
		Fault *permanent_one;
		My_Array<Fault*> output_zeros;
		My_Array<Fault*> output_ones;	
		int input_backwards ( int index, Cnf &cnf )
		{
			if ( ( input[index]->get_state() ==BOTH ) || ( input[index]->get_state() ==FAULTYBACK ) )
				return  input[index]->get_var_faulty ( cnf );
			else
				return  input[index]->get_var ( cnf );
		}

	public:
		Gate ( string _name ) : name ( _name ),
				index(0),
				state ( WHITE ),
				output ( 1 ),
				input ( 2 ),
				faulty ( -1 ),
				fault (false),
				var ( -1 ),
				var_faulty ( -1 ),
				var_active ( -1 ),
				sim_value (l_dc),
				sim_fault (l_dc),
				dc_true_count(0),
				dc_false_count(0),
				permanent_zero (0),
				permanent_one (0),
				output_zeros(1),
				output_ones(1)	
	{}
		virtual ~Gate();
		void init_faults_eq ( Fault_List& f );
		//Gate_element* get_outputs() { return output;}
		void forwards ( My_Stack<Gate> &s, My_Stack<Gate> &back );
		void backwards ( My_Stack<Gate> &s,Cnf &cnf, bool active_vars);
		virtual void to_cnf ( Cnf &cnf ) =0;
		virtual void to_cnf_faulty ( Cnf &cnf,bool active_vars ) =0;
		string get_name() {return this->name;}
		int get_index() {return this->index;}
		void set_index ( int _index ) {this->index = _index;}
		int get_state() {return state;}
		int get_var ( Cnf &cnf );
		int get_var_faulty ( Cnf &cnf );
		int get_var_active ();
		int get_var_active ( Cnf &cnf );
		void init() {state = WHITE;var=-1;
var_faulty=-1;
var_active=-1;
sim_value=l_dc;
sim_fault=l_dc;
fault=false;
faulty=-1;
dc_false_count = 0;
dc_false_count = 0;}
		void set_state ( int _state ) {state=_state;}
		virtual void print ( ostream &stream ) = 0;
		void set_faulty ( Gate *g,bool _fault );
		int get_var() {return var;}
		virtual bool sensitive_input ( bool polarity ) = 0;
		void active_path ( Cnf &cnf );
		int get_output_count() { return output.length(); }
		bool var_exists();
		void add_output ( Gate *g );
		My_Array<Gate*> &get_outputs();
		My_Array<Gate*> &get_inputs();
		bool var_active_exists();
		void dc_outputs ( Cnf &cnf );
		virtual void count_dc_inputs ( Cnf &cnf ) =0;
		virtual bool is_dc_input ( Cnf &cnf, l_type in );
		void dec_dc_true_count ( Cnf &cnf );
		void dec_dc_false_count ( Cnf &cnf );
		bool var_faulty_exists();
		int get_var_faulty();
    void add_fault(Fault *f);
    int remove_risky(My_Array<My_Var*> &vars,My_Stack<Gate> &m_s);
    int remove_dominance(My_Array<My_Var*> &vars);		
    void delete_fault(Fault *f);
    void fanout_faults(Fault_List &faults);
    bool differs(Cnf &cnf);
    bool differs(My_Array<My_Var*> &vars);

		virtual void simulate() =0;
		l_type get_sim_value() {return sim_value;}
		l_type get_sim_fault() {return sim_fault;}
		void set_sim_value ( l_type _sim_value ) {sim_value = _sim_value; sim_fault=sim_value; }
		void set_sim_value ( Cnf &cnf );
    void print_dc_counts(ostream &stream);
};

class Input: public Gate
{
	public:
		Input ( string _name ) : Gate ( _name ) {};
		virtual void print ( ostream &stream );
		virtual void to_cnf ( Cnf &cnf ) {};
		virtual void to_cnf_faulty ( Cnf &cnf, bool ative_vars ) {};
		virtual bool sensitive_input ( bool polarity ) {return false;}
		virtual void count_dc_inputs ( Cnf &cnf );
    void input_chp_faults(Fault_List &faults);

    virtual void simulate() {}	
};

class BinaryXor : public Gate
{
	public:
		BinaryXor ( string _name, Gate *_input1, Gate *_input2 ) : Gate ( _name )
		{
			input.insert ( _input1 );
			input.insert ( _input2 );
		}

		virtual void to_cnf ( Cnf &cnf,int a,int b, int c );
		virtual void to_cnf ( Cnf &cnf );
		virtual void to_cnf_faulty ( Cnf& cnf, bool active_vars );

		virtual void print ( ostream& stream )
		{
			stream << name << " = XOR(" << input[0]->get_name() <<","<<input[1]->get_name() <<")"<< endl;
		}
		virtual bool sensitive_input ( bool polarity ) {return false;}
		virtual void count_dc_inputs ( Cnf &cnf );

		virtual void simulate();
};

class Not: public Gate
{
	public:
		// konstruktor - naplni hodnoty name, in
		Not ( string _name, Gate *_input ) : Gate ( _name ) { input.insert ( _input );}
		virtual void to_cnf ( Cnf &cnf );
		virtual void to_cnf_faulty ( Cnf &cnf, bool active_vars);
		void to_cnf ( Cnf &cnf, int a, int b );
		virtual void print ( ostream& stream )
		{
			stream << name << " = NOT(" << input[0]->get_name() <<")" << endl;
		}
		virtual bool sensitive_input ( bool polarity ) {return true;}
		virtual void count_dc_inputs ( Cnf &cnf );
		virtual void simulate();
};

class Buffer: public Gate
{
	public:
		// konstruktor - naplni hodnoty name, in
		Buffer ( string _name, Gate *_input ) : Gate ( _name ) { input.insert ( _input );}

		virtual void to_cnf ( Cnf &cnf );
		void to_cnf ( Cnf& cnf,int a, int b );
		virtual void to_cnf_faulty ( Cnf &cnf, bool active_vars);
		virtual void print ( ostream& stream )
		{
			stream << name << " = BUFFER (" << input[0]->get_name() <<")" << endl;
		}
		virtual bool sensitive_input ( bool polarity ) {return true;}
		virtual void count_dc_inputs ( Cnf &cnf );
		virtual void simulate();
};


class N_naryGate : public Gate
{
	protected:
		virtual void to_cnf ( Cnf &cnf );
		virtual void to_cnf_faulty ( Cnf &cnf, bool active_vars );
		virtual void to_cnf ( Cnf &cnf,int *vars,int length,int result ) =0;
		virtual bool can_change_inputs(Cnf &cnf)=0;
		virtual void change_dc_count()=0;
		void count_dc_input(Gate *g, Cnf &cnf);
		void print_inputs ( ostream& stream )
		{
			for ( int i=0; i<input.length()-1; i++ )
				stream << input[i]->get_name() << " ,";
			stream << input[input.length()-1]->get_name() << ")" << endl;
		}


	public:
		N_naryGate ( string _name, pGate* _input, int _input_count ) : Gate ( _name )
		{
			for ( int i=0; i<_input_count;i++ )
				input.insert ( _input[i] );
		}
	virtual void count_dc_inputs(Cnf &cnf);
};

class N_naryNand : public N_naryGate
{
    protected:
             virtual bool can_change_inputs(Cnf &cnf);
             virtual void change_dc_count();  
      
	public:

		N_naryNand ( string _name, pGate* _inputs, int _input_count ) : N_naryGate ( _name,_inputs,_input_count ) {}
		virtual void to_cnf ( Cnf &cnf,int *input_vars,int length,int result );
		virtual void print ( ostream& stream )
		{
			stream << name << " = NAND(";
			this->print_inputs ( stream );
		}
		virtual bool sensitive_input ( bool polarity ) {return !polarity;}
		
		virtual void simulate();
};

class N_naryAnd : public N_naryGate
{
     protected:
             virtual bool can_change_inputs(Cnf &cnf);
             virtual void change_dc_count();  
	public:
		N_naryAnd ( string _name, pGate* _inputs, int _input_count ) : N_naryGate ( _name,_inputs,_input_count ) {}
		virtual void to_cnf ( Cnf &cnf,int *input_vars,int length,int result );
		virtual void print ( ostream& stream )
		{
			stream << name << " = AND(";
			this->print_inputs ( stream );
		}
		virtual bool sensitive_input ( bool polarity ) {return !polarity;}
	
		virtual void simulate();	
};

class N_naryNor : public N_naryGate
{
 protected:
             virtual bool can_change_inputs(Cnf &cnf);
             virtual void change_dc_count();  
	public:
		N_naryNor ( string _name, pGate* _inputs, int _input_count ) : N_naryGate ( _name,_inputs,_input_count ) {}
		virtual void to_cnf ( Cnf &cnf,int *input_vars,int length,int result );
		virtual void print ( ostream& stream )
		{
			stream << name << " = NOR(";
			this->print_inputs ( stream );
		}
		virtual bool sensitive_input ( bool polarity ) {return polarity;}
		
		virtual void simulate();
};

class N_naryOr : public N_naryGate
{
    protected:
             virtual bool can_change_inputs(Cnf &cnf);
             virtual void change_dc_count();  
	public:
		N_naryOr ( string _name, pGate* _inputs, int _input_count ) : N_naryGate ( _name,_inputs,_input_count ) {}
		virtual void to_cnf ( Cnf &cnf,int *input_vars,int length,int result );
		virtual void print ( ostream& stream )
		{
			stream << name << " = OR(";
			this->print_inputs ( stream );
		}
		virtual bool sensitive_input ( bool polarity ) {return polarity;}

		virtual void simulate();		
};

class Circuit
{
///	private:
public:
		Fault_List *faults;
		pGate *gates;
		pGate *outputs;
		My_Array<Gate*> *a_outputs; 	
		int gate_max,
		index_gate,
		output_count,
		gate_count;
		Cnf *cnf;
		Gate* find_gate ( string name );
		std::map<string,Gate*> gate_map;
		int total_faults;	
		int covered_faults;
	
/////////////////////////////////////////////////////////
		Circuit ();
                ~Circuit(); 
		string int_to_name ( int index ) {return gates[index]->get_name();}
		void add_gate ( Gate *p );
		void print ( ostream &stream );
		void init();
		// returns true, if var and var_faulty differs
		bool differs();
		
		////////////////////////////////////////////////////////////////////////
        void printMY(); ////////////////////////////////////////////////////////
        Fault* retFault(); // vraci poruchu implicitne top
		void createAdd(int f,int t,int v); // podle indexu a typu poruchz vztvori a prida poruchu
		Fault* createRet(int f,int t,int v); // podle indexu from, to a tzpu poruchz vztvori poruchu
		string shiftStr(string original,ofstream *file_test_out); // provede posun vektoru o 1vlevo - prvni bit yprava nahradi Dont care napr 10011 -> 0011-
		string shiftStrX(string original,char newCh,ofstream *file_test_out);
		string shiftStrR(string original,ofstream *file_test_out);
		////////////////////////////////////////////////////////////////////////
		
		void read_faults ( Parser &p );
		void print_faults ( ostream &stream );
		Cnf* fault_to_cnf (Fault &f, bool active_vars);
		Cnf* fault_to_cnf(int f,int t,int k, bool active_vars);
		Cnf* fault_to_cnf(bool active_vars) {return fault_to_cnf (  *(faults->top()),active_vars );}
		bool has_fault() {return !faults->is_empty();}
		void remove_fault(){delete faults->top();}	
		int get_gate_count() { return gate_count;}
		int get_input_count() { return index_gate; }
		int get_output_count() { return output_count; }
		void print_inputs ( ostream &stream,Cnf &cnf );
		void print_outputs ( ostream& stream,Cnf &cnf );
		void print_fault ( ostream &stream ) {faults->top()->print( stream );}
		My_Array<int> *get_inputs();
		void find_dc ( Cnf &cnf );
		void cnf_dc(Cnf &cnf); 
		My_Vector<l_type>* inputs_to_vector ( Cnf &cnf );
		My_Vector<l_type>* outputs_to_vector ( Cnf &cnf );
		My_Vector<l_type>* fault_outputs_to_vector ( Cnf &cnf );
		My_Vector<l_type>* inputs_to_vector();
		My_Vector<l_type>* outputs_to_vector();
		My_Vector<l_type>* fault_outputs_to_vector();
    void remove_risky(My_Array<My_Var*> &vars);
    void remove_dominance(My_Array<My_Var*> &vars);	
    void init_faults(bool ch_p);
    string fault_to_string();
    string fault_to_dimacs_string();	
    void add_gate_output(Gate *g);
    int read_circuit(Parser &parser);
    int choose_variable(Cnf &cnf,My_Array<l_type> &backup);
     void copy_input_vars(Cnf &dest,Cnf &source);		
	int get_total_faults() const
	{
		return total_faults;
	}

	int get_covered_faults() const
	{
		return covered_faults;
	}
	
	void simulate ( Cnf& cnf );
	void add_active_vars(Cnf &cnf);
	
};
}
#endif
