#ifndef LOGIC_H
#define LOGIC_H

#include <iostream>

#include "stack.h"

using namespace std;

namespace sat_atpg {

class Circuit;

class l_type
{
	public:
	unsigned value :2;
		l_type() {value = (unsigned) 1;}
		l_type ( unsigned _value ) :value ( _value ) {}
		l_type ( bool _value ) {if ( _value ) value=3; else value=0;}

		l_type& operator = ( const l_type& _l );
		bool operator == ( const l_type& _l );
		bool operator != ( const l_type& _l );
		l_type& operator & ( const l_type& _l );
		l_type& operator | ( const l_type& _l );
		l_type& operator ^ ( const l_type& _l );
		l_type& operator + ( const l_type& _l );	
                void print(ostream & stream);
};

ostream& operator << ( ostream& stream,l_type& l );
l_type& operator ~ ( const l_type& l );

const l_type l_true(( unsigned ) 3 );
const l_type l_false( ( unsigned ) 0 );
const l_type l_dc( ( unsigned ) 1 );
const l_type l_cd( ( unsigned ) 2 );



class Cnf;

class My_Var
{
	public:
		bool input;
		bool faulty; //true iff in faulty part of Circuit
		l_type value;  //value from Sat solver
		int gate_index; //index in Circuit
		My_Var ( int _gate_index,bool _faulty, bool _input ) :input ( _input ) ,faulty ( _faulty ),value ( l_dc ),gate_index( _gate_index ){}
		My_Var() :input ( false ),faulty ( false ),value ( l_dc ),gate_index ( -1 ){}
		My_Var ( const My_Var& v );
		My_Var ( const My_Var* v );
		~My_Var(){};
	void flip() { value = ( value==l_true ) ?l_false:l_true;}
};


class My_Clause
{
	private:
		int *vars;
		bool *weights;
		int max_count;
		int var_count;

		void print_var ( ostream &stream, int index, Cnf &cnf );

	public:


		My_Clause ( int _max_count );
		My_Clause ( const My_Clause& m );
		My_Clause ( My_Clause* m );
		~My_Clause() { delete [] vars; delete [] weights; }
		void print ( ostream &stream,Cnf &cnf );
		void print_integers ( ostream &stream );
		void add_var ( int var, bool weight );
		int get_var_count() { return var_count; }
		bool polarity ( int index ) { return weights[index]; }
		int var ( int index ) {return vars[index]; }
		bool satisfied ( Cnf &cnf );
		void remove_var ( int index );
		bool is_binary() {return var_count==2; };
    void to_dimacs(ofstream &f);
};

class Cnf
{
	private:
		My_Array<My_Clause*> clauses;
		My_Array<My_Var*> *vars;
		Circuit& c;
		int binary_clause_count;
		bool delete_vars;
		bool to_expand();

	public:

		Cnf ( Circuit &_c );
		Cnf ( const Cnf& cnf );
		~Cnf();
		Cnf& operator = ( const Cnf& cnf );
		void add_clause ( My_Clause *c );
		void remove_clause ( int index );
		void print ( ostream &stream );
		void print_integers ( ostream &stream );
		void print ( ostream &stream, int index );
		int get_var_count() { return vars->length();}
		int get_clause_count() { return clauses.length();}
		int get_binary_clause_count() {return binary_clause_count;}; 
//int set_var_count(int _count) { var_count=_count; }
		int newVar ( int _index,bool _faulty );
		My_Array<My_Clause*>& get_clauses() {return clauses;}
		My_Clause* get_clause ( int index ) {return clauses[index];}
		My_Var* get_var ( int index ) { return (*vars)[index];}
		void init_vars_dc();
		bool satisfied();
		bool satisfy();
		Cnf* expand_dc();
		void set_value ( int index, l_type value )
		{
			(*vars)[index]->value=value;
		}
		void set_input ( int index, bool input=true )
		{
			(*vars)[index]->input=input;
		}
		l_type bool_to_l_type ( bool b )
		{
			return b?l_true:l_false;
		}
		void compute_counts();
    My_Array<My_Var*>* export_vars();
    My_Array<My_Var*>* copy_vars();
    My_Array<My_Var*>& get_vars() {return (*vars);}	
    void to_dimacs(ofstream &f);

};
	

class Test_Vector
{
	private:
		My_Vector<l_type> *in_vector;
		My_Vector<l_type> *out_vector;
		My_Vector<l_type> *fault_vector;
	public:
                ~Test_Vector(); 
		Test_Vector ( Circuit &circuit, Cnf &cnf );
		Test_Vector ( Circuit &circuit );
		Test_Vector ( My_Vector<l_type> *input=0, My_Vector<l_type> *output=0, My_Vector<l_type> *fault=0);
		int get_input_count();
		int get_output_count();
		My_Vector<l_type>* get_output_vector();
		My_Vector<l_type>* get_input_vector();
		My_Vector<l_type>* get_fault_output_vector();
		ostream& operator <<(ostream &stream);
		Test_Vector* operator + (const Test_Vector& t_v);
		bool operator ^ (const Test_Vector& t_v);		
                void print(ostream &stream,bool in_=true, bool out_=false, bool fault_=false);  
    bool tests_fault();
    int count_dc_inputs();
		// converts all dc to the value
		void dc_convert(const l_type &l);
};

} 
#endif








