#include "nodes.h"
#include "sTable.h"
#include "tNode.h"

#include <sstream>
#include <fstream>

//#define EXPAND
//#define DEBUG

#define S_NOT 0
#define S_AND 1
#define S_OR 2
#define S_NAND 3
#define S_NOR 4
#define S_XOR 5
#define S_XNOR 6
#define S_ASSIGN 7
#define S_LEAF 10

#define S_FALSE 0
#define S_TRUE 1
#define S_DONTCARE 2


static int index;
static int origindex;
static int choice;
static int opt;
static unsigned int literals;
static string varname = "sig";

static unsigned int actnum = 0;

#ifdef DEBUG
static int tlimit = 10000000;
#endif

#ifndef DEBUG
static int tlimit = 10;
#endif

static string OpTypes[]={"not","and","or","nand","nor","xor","xnor","<="};

static string blifKeywords[]={".names"};



//******************************************************************

unsigned int getnum()
{
	return actnum++;
}

bool checkoutput(ostream * output)
{
	 string out_path = "";
	 
	 if ( output->fail() )
	 {
	 	delete output;
	 	cout<<"Enter legal output file path :";
	 	cin>>out_path;
	 	output = new ofstream(&out_path[0]);
	 	cout<<endl;
	 }
	 
	 if ( output->fail() )
	 {
	 	delete output;
	 	cout<<"Cannot open output file"<<endl;
	 	return 0;
	 }
	 
	 return 1;
}

//meri cas vypoctu
void checktime()
{
    if (measure)
    {	
   	 gt2 = clock();
	     if ((difftime(gt2, gt1)/CLOCKS_PER_SEC)>tlimit)
	     {
	    	int option = 2;
	    	cout<<"Timer exceeded, continue?"<<endl;
	    	cout<<"1. Yes"<<endl;
	    	cout<<"2. No"<<endl;
	    	cout<<"Choice:";
	    	cin>>option;
	    	if (option == 2)
	    	{
	    		cout<<"Terminating"<<endl;
	    		exit(0);
	    	}
	    	measure = false;
	     } 
    }
}


//minimalizace formule
Node * minimalization(Node * ptr)
{
	//return ptr;
	
	choice = 1;
	unsigned int j;
	treeArray->terms = 0;

	tRoot = new tNode();
	
	symbTable = treeArray->symbNames;
	symbTable->refresh();
		
	if ( ptr->equals(1) )
	{
		if ( !ptr->findOp(S_OR) ) tRoot->add(symbTable);
	}
	else
	{
		if (ptr != NULL) delete ptr;
		delete tRoot;
		return new VectNode(0,1);
	}
	
	//t1 = clock();
	
	/*if (expand)
	{
		for (j=0;j<treeArray->symbNames->count;j++)
	 	{
		 checktime();
		 tRoot->expand(1);
		 tRoot = tRoot->switchroot();
		 //tRoot->print(cout);
		 //cout<<endl;
	 	}
	
	 }*/

	 for (j=0;j<(treeArray->symbNames->count);j++)
	 {
	 	 tRoot->reduce(1);
	 	 tRoot = tRoot->switchroot();
	 }

	 	 
	 //t2 = clock();
	 
	 //cout<<"Operation took:"<<difftime(t2, t1)/CLOCKS_PER_SEC<<" seconds"<<endl; 
	
	 if (ptr != NULL) delete ptr;
	 ptr = tRoot->transform(NULL,NULL,0);
	 delete tRoot;
	 return ptr;
}

//zapis stromu do souboru
void printvhdl(ostream * output, bool printvals)
{
		int i = 0;
		int vhdltype = 1;
		literals = 0;
		choice = 3;
		
		if (!checkoutput(output)) return;
		
		cout<<"How to save:"<<endl;
		cout<<"1. Complete VHDL"<<endl;
		cout<<"2. Pseudo-VHDL"<<endl;
		cout<<"Choice:";
		if (!autoprint) cin>>vhdltype;
		else
		{
			cout<<opt;
		}
		
		cout<<"What to save:"<<endl;
		cout<<"1. Save all"<<endl;
		cout<<"2. Save added only"<<endl;
		cout<<"Choice:";
		opt = 1;
		if (!autoprint) cin>>opt;
		else
		{
			opt = 2;
			cout<<opt;
		}
		
		if (opt == 2) i = treeArray->outvars - added_formulas;		 
		 
		 if (vhdltype == 2)
		 {
			 if (!treeArray->symbNames->empty())
			 {
			 	*output<<"variable";
			 	treeArray->symbNames->printnamescomma(output);
			 	*output<<";"<<endl;
			 }
		 }
		 
		 for (int j = i; j<treeArray->outvars; j++)
		 {
			 elem = treeArray->find(j);
			 if (elem == NULL) continue;
			 if (elem->root == NULL) continue;
			 literals = literals + elem->root->countLiterals();
		 }
		 
		 if (vhdltype == 2) *output<<"-- literals: "<<literals<<endl;
		 
		 if (vhdltype == 1)
		 {
			 *output<<"library IEEE;"<<endl;
			 *output<<"use IEEE.Std_Logic_1164.all;"<<endl;
			 *output<<"use work.define.all;"<<endl<<endl;
			 *output<<"entity "<<"ent "<<"is"<<endl;
			 *output<<"port "<<"("<<endl;
			 treeArray->symbNames->printnamescomma(output);
			 *output<<": in std_logic;"<<endl;
			 
			 for (int j = i; j<treeArray->outvars; j++)
			 {
				 elem = treeArray->find(j);
				 if (elem == NULL) continue;
				 *output<<" "<<elem->name;
				 if (j+1 != treeArray->outvars) *output<<",";
			 }
			 
			 *output<<": out std_logic);"<<endl;
			 *output<<"end "<<"ent"<<";"<<endl<<endl;
			 
			 *output<<"architecture "<<"dataflow "<<"of "<<"ent "<<"is"<<endl;
			 *output<<"begin"<<endl;
		 }
		 
		 for (;i<treeArray->outvars;i++)
		 {
		 	elem = treeArray->find(i);
		 	if (elem == NULL) continue;
		 	root = elem->root;
		 	if (root == NULL) continue;
		 	symbTable = treeArray->symbNames;
		 	symbTable->refresh();
		   	
		   	*output<<elem->name;
			*output<<" <= ";
		 	root->print(*output);
		   	*output<<";";
		   	
		   	//posledni operace byla test splnitelnosti 	
		   	if (printvals)
		   	{
		   	 	*output<<" --";
		   	 	g_output = output;
		   	 		
		   	 	if ( root->equals(1) )
		   	 	{
		   	 		if ( !root->findOp(S_OR) ) 
		   	 		{
		   	 			*output<<" |"; 
		   	 			symbTable->print(g_output);
		   	 		} 
		   	 	}
		   	 	else { *output<<" N"; }
		   	 	//printbits (root->eval(),32,*output); 
		   	 		
		   	 }
		   	 	
		   	 *output<<endl;
		  }
		  
		  if (vhdltype == 1) *output<<"end "<<"dataflow;"<<endl;
		  
		  cout<<"Data saved";
		  cout<<endl;
}

//ulozeni jako PLA
void printpla(ostream& out)
{
	 choice = 2;
	 literals = 0;
	 index = 0;
	 
	 if (!checkoutput(&out)) return;
	 
	 cout<<"What to save:"<<endl;
	 cout<<"1. Save all"<<endl;
	 cout<<"2. Save added only"<<endl;
	 cout<<"Choice:";
	 opt = 1;
	 #ifndef DEBUG
	 if (!autoprint) cin>>opt;
	 else
	 {
		 opt = 2;
		 cout<<opt;
	 }
     #endif
	 cout<<endl;
	 
	 out<<".i"<<" "<<treeArray->invars<<endl;
	 	
	 if (opt == 2)
	 {
	 	index = treeArray->outvars - added_formulas;
	 	out<<".o"<<" "<<added_formulas<<endl;
	 }
	 else
	 {
	 	out<<".o"<<" "<<treeArray->outvars<<endl;
	 }
	 
	 
	 if (treeArray->namedi)
	 {
	 	out<<".ilb";
	 	treeArray->symbNames->printnames(&out);
	 	out<<endl;
	 }
	 if (treeArray->namedo)
	 {
	 	out<<".ob";
	 	for (int i=index;i<treeArray->outvars;i++)
	 	{
	 		elem = treeArray->find(i);
	 		if (elem == NULL) continue;
	 		out<<" "<<elem->name;
	 	}
	 	out<<endl;
	 }
	 
	 treeArray->terms = 0;
	 for (int i = index; i<treeArray->outvars; i++)
	 {
		 elem = treeArray->find(i);
		 if (elem == NULL) continue;
		 treeArray->terms += elem->terms;
		 if (elem->root == NULL) continue;
		 literals = literals + elem->root->countLiterals();
	 }
	 
	 out<<".p"<<" "<<treeArray->terms<<endl;
	 out<<"# literals: "<<literals<<endl;
	 
	 origindex = index;
	 
	 for (; index<treeArray->outvars; index++)
 	 {
	 	elem = treeArray->find(index);
	 	if (elem == NULL) continue;
	 	root = elem->root;
	 	if (root == NULL) continue;
	 	symbTable = treeArray->symbNames;
	 	symbTable->refresh();
	   	
	   	g_output = &out; 		
	   	 	if ( root->equals(1) )
	   	 	{
	   	 		if ( !root->findOp(S_OR) ) 
	   	 		{
	   	 				symbTable->printvals(g_output);
    					*g_output<<" ";
    					for (int i = origindex;i<treeArray->outvars;i++)
    					{
    						if (i == index) *g_output<<S_TRUE;
    						else *g_output<<S_FALSE;
    					}
    					*g_output<<endl;
	   	 		} 
	   	 	}
	 
 	 }
	 
	 cout<<"Data saved";
	 cout<<endl;
}


//ulozeni jako BLIF
void printblif(ostream& out)
{
	 choice = 4;
	 index = 0;
	 
	 if (!checkoutput(&out)) return;
		 
	 cout<<"What to save:"<<endl;
	 cout<<"1. Save all"<<endl;
	 cout<<"2. Save added only"<<endl;
	 cout<<"Choice:";
	 opt = 1;
	 #ifndef DEBUG
	 if (!autoprint) cin>>opt;
	 else
	 {
		 opt = 2;
		 cout<<opt;
	 }
     #endif
	 cout<<endl;
	  	
	 if (opt == 2)
	 {
	 	index = treeArray->outvars - added_formulas;
	 }
	 
	 out<<".model";
	 out<<" blif";
	 out<<endl;

	 out<<".inputs";
	 treeArray->symbNames->printnames(&out);
	 out<<endl;
	 
	 out<<".outputs";
	 for (int i = index;i<treeArray->outvars;i++)
	 {
	 	elem = treeArray->find(i);
	 	if (elem == NULL) continue;
	 	out<<" "<<elem->name;
	 }
	 out<<endl;
	 	 
	 origindex = index;
	 
	 for (; index<treeArray->outvars; index++)
 	 {
	 	elem = treeArray->find(index);
	 	if (elem == NULL) continue;
	 	root = elem->root;
	 	if (root == NULL) continue;
	 	symbTable = treeArray->symbNames;
	 	symbTable->refresh();
	   	
	   	g_output = &out;
	   	
	   	root->printmulti(out);
	 
 	 }
	 
	 out<<".end";
	 out<<endl;
	 
	 cout<<"Data saved";
	 cout<<endl;
}



//vypsani cisla po bitech
void printbits (unsigned int val, int lng, ostream& out)
{

	for (int i = lng-1; i >= 0; i--)
	{
		out << (((val) >> i) & 1);
	}
}



/*=======================================*/
	
	void Node::createSTable() {return;}
	
	//vrati true pokud je nalezen typ uzlu dany parametrem
	bool Node::findOp (int pType) {return false;}
	
	//vrati true pokud je formule spnitelna a odhodnoti promenne hodnotou parametru
	bool Node::equals (unsigned int val) {return false;}
	
	//zkontroluje semantiku stromu
	bool Node::checkLength (int& g_Length) {return true;}
	
	//vytvori kopii stromu
	//Node * Node::copy()=0;
	
	//test zda strom osahuje jine typy uzlu nez ten dany parametrem
	bool Node::containsOp (int num) {return false;}
	
	//test zda je formule v DNF
	bool Node::isdnf(bool bl) {return true;}
	
	//vyhodnoceni stromu
	unsigned int Node::eval() {return ( 0 ); }
	
	//spocita pocet literalu ve vyrazu
	unsigned int Node::countLiterals() {return ( 0 ); }
	
	//vrati typ daneho uzlu
	//int Node::gettype ()=0;
	
	/*======================================================================*/
	//vsechny nasledujici metody vrati ukazatel na novy strom a stary zrusi
		
	//zjednoduseni vyrazu
	Node * Node::simplify() {return this;}
	
	//forma pro realizaci pomoci nandu
	Node * Node::nandForm() {return this;}
	
	//forma pro realizaci pomoci noru
	Node * Node::norForm() {return this;}
	
	//eliminace dane operace z vyssich hladin stromu - efekt: uprava na NDF nebo NKF
	Node * Node::elimOp(int opType) {return this;}
	
	//eliminace NOT z vyssich hladin stromu - efekt: NOT je pouze pred listy 
	Node * Node::elimNot() {return this;}
	
	//"roznasobeni" praveho podstromu danym podstromem, vstupem je ukazatel na dany podstrom
	// a typ pozadovane operace
	Node * Node::applyLR( Node * lop ,unsigned char& pType ) {return this;}
	
	//negovani stromu
	Node * Node::negate() {return this;}
	
	//uprava daneho stromu do formy kdy obsahuje pouze operatory AND,OR,NOT
	Node * Node::AndOrNot() {return this;}
	
	//zapis stromu do souboru
	//void Node::print(ostream& out)=0;
		
	Node * Node::minimize() {return this;}
	
	Node * Node::cofactor(int num, bool val) {return this;}
	
	Node::~Node() { }


/*===================================*/

	//
    UNode::UNode ( Node * Ch, int T) : Child ( Ch ), Type(T) {}
    
    bool UNode::isdnf(bool bl)
    {
    	if (Child->gettype() == S_LEAF ) return true;
    	return false;
    }
    
    //
    bool UNode::findOp (int pType) {return Child->findOp(pType); }
    
    //
    bool UNode::equals(unsigned int val)
    {
    	switch (Type)
    	{
    		
    		case S_NOT:
    		{
    			return ( Child->equals(~val)  );
    		} 
    	
    		default: return false;
    	}
    }
    
    //
    bool UNode::checkLength(int& g_Length)
    {
    	return Child->checkLength(g_Length);
    }
   
    Node * UNode::AndOrNot()
    {
    	Child = Child->AndOrNot();
    	return this;
    }
    
    //
    Node * UNode::copy()
    {
    	switch (Type)
    	{
    		case S_NOT:
    		{
    			return ( new UNode (Child->copy(),S_NOT) );
    		}
    		default: return NULL;
    	}
    }
    
    //
    bool UNode::containsOp (int num)
    {
    	return Child->containsOp(num);
    }
    
    
    void UNode::createSTable()
    {
    	Child->createSTable();
    	return;
    }
    
    //
    Node * UNode::simplify()
    {
    	Node * ret;
    	UNode * ptr;
    	
    	switch (Type)
    	{
    		case S_NOT:
    		{
    			if ( Child->gettype() == S_NOT )
    			{
    				ptr = dynamic_cast<UNode*>(Child);
    				if (ptr!= NULL)
    				{
	    				ret = ptr->Child;
	    				ptr->Child = NULL;
	    				ret = ret->simplify();
	    				delete this;
	    				return ret;
    				}
	    				
    			}
    			
    			Child = Child->simplify();
    			return this;
    		}
    		default: return this;
    	}
    	
    }
    
    
    //
    Node * UNode::nandForm ()
    {
    	BNode * ptr;
    	
    	switch (Type)
    	{
    		case S_NOT:
    		{
    			if ( Child->gettype() == S_AND )
    			{
    				ptr = dynamic_cast<BNode*>(Child);
    				if (ptr!=NULL)
    				{
	    				ptr->Left = ptr->Left->nandForm();
	    				ptr->Right = ptr->Right->nandForm();
	    				return this;
	    			}  
    			}
    			
    			Child = Child->nandForm();
    			return this;
    		}
    		default: return this;
    	}
    }
    
    //
    Node * UNode::norForm ()
    {
    	BNode * ptr;
    	
    	switch (Type)
    	{
    		case S_NOT:
    		{
    			if ( Child->gettype() == S_OR )
    			{
    				ptr = dynamic_cast<BNode*>(Child);
    				if (ptr!=NULL)
    				{
	    				ptr->Left = ptr->Left->norForm();
	    				ptr->Right = ptr->Right->norForm();
	    				return this;
	    			}  
    			}
    			
    			Child = Child->norForm();
    			return this;
    		}
    		default: return this;
    	}
    }
    
    //
    Node * UNode::applyLR( Node * lop, unsigned char& pType)
    {
    	Child = Child->applyLR(lop,pType);
    	return this;
    }
    
    //
    Node * UNode::elimOp(int opType)
    {
    	Child = Child->elimOp(opType);
    	return this;
    } 
    
    //
    Node * UNode::elimNot()
    {
    	Node * ret;
    	
    	switch (Type)
    	{
    		case S_NOT:
    		{
    			if ( Child->gettype() != S_LEAF )
    			{
    				ret = Child->negate();
    				ret = ret->elimNot();
    				Child = NULL;
    				delete this;
    				return ret;
    			}
    			
    			return this;
    		}
    		
    		default: return this;
    	}
    }
    
    //
    Node * UNode::negate()
    {	
    	Node * ret;
    	
    	switch (Type)
    	{
    		case S_NOT:
    		{
    			ret = Child;
    			Child = NULL;
    			delete this;
    			return ret;
    		}
    		
    		default: return this;
    	}
    }
    
    //
     void UNode::print(ostream& out)
	{
		bool printp = !(Child->gettype()==S_LEAF);
		out<<OpTypes[Type]<<" ";
		
		if (printp) out<<"( ";
		Child->print(out);
		if (printp) out<<" )";
	}
     
     string UNode::printmulti(ostream& out)
    {
    	string istr = Child->printmulti(out);
    	 
    	stringstream ss;
    	string ostr;
    	unsigned int num;
    	
    	num = getnum();
		ss<<num; 
		ss>>ostr;
		ostr = varname + ostr;
		
		if (elem->root == this) ostr = elem->name;
		
		out<<blifKeywords[0]<<" "<<istr<<" "<<ostr<<endl;
    	
    	switch (Type)
    	{
    		case S_NOT:
    		{
    			out<<S_FALSE<<" "<<S_TRUE<<endl;
    			break;
    		}
    	
    	}
    	
    	return ostr;
    }
    
    //
     unsigned int UNode::eval ()
	{
		switch (Type)
		{
			case S_NOT: return (  ~Child->eval() );
			default: return (0);
		}
	} 
    
    //
     int UNode::gettype() { return Type; }
     
     Node * UNode::minimize()
     {
     	Node * ptr = this;
     	if (Child->gettype() == S_LEAF) return ptr;
     	if (!ptr->isdnf(true))
     	{
     		Child = Child->minimize();
     		ptr = ptr->elimOp(S_AND);
     	}
     	ptr = minimalization(ptr);
     	return ptr;
     }
    
     Node * UNode::cofactor(int num, bool val)
     {
    	 Child = Child->cofactor(num, val);
    	 return this;
     }
     
     unsigned int UNode::countLiterals()
     {
    	 return Child->countLiterals();
     }
     
    //
     UNode::~UNode ( )  { delete Child; } 



/*===================================================*/
//=====================================================

	
    BNode::BNode ( Node * L, Node * R, int T ) : Left (L), Right (R), Type(T) {}
    
    bool BNode::isdnf( bool bl )
    {
    	switch (Type)
    	{
    		case S_OR:
    		{
    			if ( bl == false) return false;
    			return ( Left->isdnf(bl) && Right->isdnf(bl) );
    		}
    		
    		case S_AND: 
    		{
    			bl = false;
    			return ( Left->isdnf(bl) && Right->isdnf(bl) );
    		}
    		
    		default: return false;
    	}
    	
    }
    
    bool BNode::findOp (int pType)
    {
    	if (Type == pType) {return true ;}
    	else 
    	{
    		return ( Left->findOp(pType) || Right->findOp(pType) );
    	}
    }
    
    bool BNode::equals(unsigned int val)
    {
    	bool Lval, Rval;
    	
    	switch (Type)
    	{
    		
    		case S_AND:
    		{
    			return ( Left->equals(val) && Right->equals(val) );
    		}
    		
    		case S_OR:
    		{
    			symbTable->refresh();
    			Lval = Left->equals(val);
    			if (Lval && (Left->gettype()!= S_OR))
    			{
    				switch (choice) 
    				{
	    				case 1:
	    				{
	    					tRoot->add(symbTable);
	    					break;
	    				}
	    				case 2:
	    				{
	    					symbTable->printvals(g_output);
	    					*g_output<<" ";
	    					for (int i = origindex ;i<treeArray->outvars;i++)
	    					{
	    						if (i == index) *g_output<<S_TRUE;
	    						else *g_output<<S_FALSE;
	    					}
	    					*g_output<<endl;
	    					break;
	    				}
	    				case 3:
	    				{
		    				*g_output<<" |";
		    				symbTable->print(g_output);
		    				break;
		    			}
	    				case 4:
	    				{
	    					symbTable->printvals(g_output);
	    					*g_output<<" ";
	    					*g_output<<S_TRUE;
	    					*g_output<<endl;
	    					break;
	    				}
	    				default: break;
    				}
    			}
    			
    			symbTable->refresh();
    			Rval = Right->equals(val);
    			if (Rval && (Right->gettype()!= S_OR) )
    			{
    				switch(choice)
    				{
    					case 1:
    					{
    						tRoot->add(symbTable);
    						break;
    					}
    				
    					case 2:
	    				{
	    					symbTable->printvals(g_output);
	    					*g_output<<" ";
	    					for (int i = origindex ;i<treeArray->outvars;i++)
	    					{
	    						if (i == index) *g_output<<S_TRUE;
	    						else *g_output<<S_FALSE;
	    					}
	    					*g_output<<endl;
	    					break;
	    				}
    					case 3:
	    				{
		    				*g_output<<" |";
		    				symbTable->print(g_output);
		    				break;
		    			}
	    				case 4:
	    				{
	    					symbTable->printvals(g_output);
	    					*g_output<<" ";
	    					*g_output<<S_TRUE;
	    					*g_output<<endl;
	    					break;
	    				}
    					default: break;
    				}
    			}
    			return ( Lval || Rval );
    		} 
    		
    		case S_ASSIGN:
    		{
    			return ( Right->equals(val) );
    		} 
    	
    		default: return false;
    	}
    }
    
    bool BNode::checkLength(int& g_Length)
    {
    	return ( Left->checkLength(g_Length) && Right->checkLength(g_Length) );
    }
    
     Node * BNode::copy()
    {
    	Node * Lval,*Rval;
    		
    	Rval = Right->copy();
    	Lval = Left->copy();
    	
    	return ( new BNode (Lval,Rval,Type) );
    	
    }
    
    
    void BNode::createSTable()
    {
    	Left->createSTable();
    	Right->createSTable();
    	return;
    }
    
    Node * BNode::simplify()
    {
    	switch (Type)
		{	
			default: { Left=Left->simplify(); Right=Right->simplify(); return this; }
		}
    }
    
    Node * BNode::nandForm ()
    {
 
			    switch (Type)
			    	{
			    		case S_AND:
			    		{
			    			Left = Left->nandForm();
    						Right = Right->nandForm();
			    			return new UNode (new UNode (this,S_NOT),S_NOT); 
			    		}
			    		case S_OR:
			    		{
			    			Type = S_AND;
			    			Left = new UNode (Left,S_NOT);
			    			Right = new UNode (Right,S_NOT);
    						Left = Left->nandForm();
    						Right = Right->nandForm();
			    			return new UNode (this,S_NOT);
			    		}
			    		
			    		case S_ASSIGN:
			    		{
			    			Right = Right->nandForm();
			    			return this;
			    		}
			    		
			    		default: return this;
			    	}
    		
    }
    
    //
    Node * BNode::norForm ()
    {
 
			    switch (Type)
			    	{
			    		case S_OR:
			    		{
			    			Left = Left->norForm();
    						Right = Right->norForm();
			    			return new UNode (new UNode (this,S_NOT),S_NOT); 
			    		}
			    		case S_AND:
			    		{
			    			Type = S_OR;
			    			Left = new UNode (Left,S_NOT);
			    			Right = new UNode (Right,S_NOT);
    						Left = Left->norForm();
    						Right = Right->norForm();
			    			return new UNode (this,S_NOT);
			    		}
			    		
			    		case S_ASSIGN:
			    		{
			    			Right = Right->norForm();
			    			return this;
			    		}
			    		
			    		default: return this;
			    	}
    		
    }
    
    
     Node * BNode::AndOrNot()
    {
    	Node * newLeft, * newRight, * negLeft, * negRight;
    	Left = Left->AndOrNot();
    	Right = Right->AndOrNot();
    	
    	switch (Type)
    	{
    		case S_AND:
    		case S_OR:
    		{
    			return this;
    		}
    		
    		case S_NAND:
    		{
    			Type = S_AND;
    			return ( new UNode (this,S_NOT) );
    		}
    		
    		case S_NOR:
    		{
    			Type = S_OR;
    			return ( new UNode (this,S_NOT) );
    		}
    		
    		case S_XOR:
    		case S_XNOR:
    		{
    			int oldType = Type;
    			Type = S_OR;
    			negLeft = new UNode (Left->copy(),S_NOT);
    			negRight = new UNode (Right->copy(),S_NOT);
    			
    			newLeft = new BNode (Left,negRight,S_AND);
    			newRight = new BNode (negLeft,Right,S_AND);
    			Left = newLeft;
    			Right = newRight;
    			
    			if (oldType == S_XOR) {return this;}
    			return ( new UNode (this,S_NOT) );
    			
    		}
    	
    		case S_ASSIGN:
    		{
    			Right = Right->AndOrNot();
    			return this;
    		}
    		
    		default: return this;
    		
    	}
    }
    
    
     bool BNode::containsOp (int num)
    {
    	if (Type == num)
    	{return ( Left->containsOp(num) || Right->containsOp(num) );}
    	
    	return true;
    }
    
    
     Node * BNode::applyLR( Node * lop, unsigned char& pType)
    {
    	if (pType == Type)
    	{
    		Left = Left->applyLR(lop,pType);
	    	Right = Right->applyLR(lop,pType);
	    	return this;
    	}
    	
    	else
    	{
    		Left = new BNode (lop->copy(),Left,pType);
	    	Right = new BNode (lop->copy(),Right,pType);  			
	    	return this;
    	}
    	
    } 
    
    
     Node * BNode::elimOp(int opType)
    {
    	
    	checktime(); //pak zapnout
    	Node * ret;
    	
    		if (Type == opType)
    		{
    			if ( !Right->containsOp(opType) ) 
    			{
    				if ( !Left->containsOp(opType) )
    				{ return this; }
    				
    				ret = Left;
    				Left = Right;
    				Right = ret;
    				
    				return ( this->elimOp(opType) );
    			}
   
    			else 
    			{
    				ret = Right->applyLR(Left,Type);
    				ret = ret->elimOp(opType);
    				
    				Right = NULL;
    				//Left = NULL; //levy se kopiroval-smazat
    				delete this;
    				return ret;
    			}
   
    		}
    		
    		else
    		{
    			Left = Left->elimOp(opType);
    			Right = Right->elimOp(opType);
    			return this;
    		}
   
    } 
    
    
     Node * BNode::elimNot()
    {
    	Left = Left->elimNot();
    	Right = Right->elimNot();
    	return this;	
    }
    
    
     Node * BNode::negate()
    {
    	switch (Type)
		{
			case S_AND:
			{ Type=2; Left=Left->negate(); Right=Right->negate(); return this; }
			
			case S_OR:
			{ Type=1; Left=Left->negate(); Right=Right->negate(); return this; }
			
			case S_NAND:
			{ Type=S_AND; return this; }
			
			case S_NOR:
			{ Type=S_OR; return this; }
			
			case S_XOR:
			{ Type=S_XNOR; return this; }
			
			case S_XNOR:
			{ Type=S_XOR; return this; }
			
			case S_ASSIGN:
			{ Right=Right->negate(); return this; }
			
			default: return this;
		}
    }
    
    
     void BNode::print(ostream& out)
	{
		int LType = Left->gettype();
		int RType = Right->gettype();
		
		//radsi zachovat zavorky, aby byla videt struktura stromu
		bool printlp = (!(LType==S_LEAF));//!( (LType==S_LEAF) || (LType==Type) );
		bool printrp = (!(RType==S_LEAF));//!( (RType==S_LEAF) || (RType==Type) );
		
		if (printlp) out<<"( ";
		Left->print(out);
		if (printlp) out<<" )";
		out<<" "<<OpTypes[Type]<<" ";
		if (printrp) out<<"( ";
		Right->print(out);
		if (printrp) out<<" )";
	}
	
     string BNode::printmulti(ostream& out)
    {
    	string istr1 = Left->printmulti(out);
    	string istr2 = Right->printmulti(out);
    	 
    	stringstream ss;
    	string ostr;
    	unsigned int num;
    	
    	num = getnum();
		ss<<num; 
		ss>>ostr;
		ostr = varname + ostr;
		
		if (elem->root == this) ostr = elem->name;
		
		out<<blifKeywords[0]<<" "<<istr1<<" "<<istr2<<" "<<ostr<<endl;
    	
    	switch (Type)
    	{
    		case S_AND:
    		{
    			out<<S_TRUE<<S_TRUE<<" "<<S_TRUE<<endl;
    			break;
    		}
    		
    		case S_OR:
    		{
    			out<<S_TRUE<<"-"<<" "<<S_TRUE<<endl;
    			out<<"-"<<S_TRUE<<" "<<S_TRUE<<endl;
    			break;
    		}
    		
    		case S_NAND:
    		{
    			out<<S_FALSE<<"-"<<" "<<S_TRUE<<endl;
    			out<<"-"<<S_FALSE<<" "<<S_TRUE<<endl;
    			break;
    		}
    		
    		case S_NOR:
    		{
    			out<<S_FALSE<<S_FALSE<<" "<<S_TRUE<<endl;
    			break;
    		}
    		
    		case S_XOR:
    		{
    			out<<S_TRUE<<S_FALSE<<" "<<S_TRUE<<endl;
    			out<<S_FALSE<<S_TRUE<<" "<<S_TRUE<<endl;
    			break;
    		}
    		
    		case S_XNOR:
    		{
    			out<<S_FALSE<<S_FALSE<<" "<<S_TRUE<<endl;
    			out<<S_TRUE<<S_TRUE<<" "<<S_TRUE<<endl;
    			break;
    		}
    	
    	}
    	
    	return ostr;
    }
		
	 unsigned int BNode::eval ()
	{
		unsigned int Lval,Rval;
		Lval=Left->eval();
		Rval=Right->eval();
				
		switch (Type)
		{
			case S_AND: return ( Lval & Rval );
			case S_OR: return ( Lval | Rval );
			case S_NAND: return ~( Lval & Rval );
			case S_NOR: return ~( Lval | Rval );
			case S_XOR: return ( Lval ^ Rval );
			case S_XNOR: return ~( Lval ^ Rval );
			case S_ASSIGN: return ( Rval );
			default: return (0);
		}
	} 
	
	 int BNode::gettype() { return Type; }
	 
     Node * BNode::minimize()
     {
     	Node * ptr = this;
     	if (!ptr->isdnf(true))
     	{
	     	Left = Left->minimize();
	     	Right = Right->minimize();
	     	ptr = ptr->elimOp(S_AND);
     	}
     	//ptr->print(cout);
     	//cout<<endl;
     	ptr = minimalization(ptr);
     	//ptr->print(cout);
     	//cout<<endl<<endl;
     	return ptr;
     }
     
     Node * BNode::cofactor(int num, bool val)
     {
    	 Left = Left->cofactor(num, val);
    	 Right = Right->cofactor(num, val);
    	 return this;
     }
     
     unsigned int BNode::countLiterals()
     {
    	 return ( Left->countLiterals() + Right->countLiterals() );
     }
	
     BNode::~BNode ( )  { delete Left; delete Right; }

/*======================================================*/

   
   IdentNode::IdentNode ( string& Id ) : Name ( Id ) {}
   
   bool IdentNode::equals(unsigned int val)
   {
   		Symbol * act_symb = symbTable->getPtr(Name);
   		if (act_symb == NULL) return false;
   		
   		if ( !act_symb->valid )
   		{
   			symbTable->setValue(Name,val);
   			return true;
   		}
   		
   		unsigned int identVal = act_symb->value;
   		if ( identVal == val ) return true;
   		
   		return false;
   }
   
    Node * IdentNode::copy()
   {
   		return (new IdentNode (Name) );
   }
   
   
    Node * IdentNode::negate()
   {
   		return ( new UNode (this , S_NOT) );	
   }
   
   
    void IdentNode::print (ostream& out)
	{
		out<<Name;
	}
    
    string IdentNode::printmulti(ostream& out)
    {
    	if (elem->root == this)
    	{
    		out<<blifKeywords[0]<<" "<<Name<<" "<<elem->name<<endl;
    		out<<S_TRUE<<" "<<S_TRUE<<endl; 
    	}
    	
    	return Name;
    }
   
   
    unsigned int IdentNode::eval ()
    {
    	Symbol * act_symb = symbTable->getPtr(Name);
    	if (act_symb == NULL) return 0;
    	return ( act_symb->value );
    }
    
    
     int IdentNode::gettype() { return S_LEAF; }
     
     void IdentNode::createSTable()
     {
     	symbTable->add(Name);
     	return;
     }
     
     Node * IdentNode::cofactor(int num, bool val)
     {
    	 Symbol * smb;
    	 Node * ptr;
    	 smb = treeArray->symbNames->find(num);
    	 if (smb == NULL) return this;
    	 if (smb->name != Name) return this;
    	 
    	 ptr = new VectNode(val,1);
    	 delete this;
    	 return ptr;
  
     }
     
     unsigned int IdentNode::countLiterals()
     {
    	 return (1);
     }
          

/*=====================================================================*/

   VectNode::VectNode ( unsigned int V , int L ) : Value ( V ), Length ( L )
   {
	   if (V == 0) Value = ~1;
   }
   
   bool VectNode::equals(unsigned int val)
    {
	    //cout<<"val:"<<val<<endl;
	   	//cout<<"Value:"<<Value<<endl;
    	if (val == Value) return true;
    	return false; 
    }
   
   bool VectNode::checkLength(int& g_Length)
   {
   		return (Length == g_Length); 
   }
   
   int VectNode::length()
   {
   		return Length;
   }
   
   
    Node * VectNode::copy()
   {
   		return (new VectNode (Value,Length) );
   }
   
   
    Node * VectNode::negate()
   {
   		return ( new UNode (this , S_NOT) );
   }
    
    void VectNode::print(ostream& out)
    {	
		out<<char(34);
		printbits(Value,Length,out);
		out<<char(34);
    }
    
    string VectNode::printmulti(ostream& out)
    {
    	return "";
    }
   
    unsigned int VectNode::eval ()
    {
    	return ( Value );
    }
    
     int VectNode::gettype() { return S_LEAF; }
