#include "graph.h"

#include <iostream>
#include <stack>
#include <sstream>
#include <math.h>
#include <string>
#include <fstream>
using namespace std;

template <class T>
inline std::string To_String (const T& t)
{
std::stringstream ss;
ss << t;
return ss.str();
}

//
// GTerm
//
GTerm::GTerm(string &_inputs, string &_outputs, vector<GVariable*> &variables)
{
	count_on = 0; count_off = 0; count_dc = 0; inputs = _inputs; outputs = _outputs;
	for (unsigned int i=0;i<inputs.length();i++)
	switch (inputs[i])
	{
	case '1':
		count_on++;
		vars_on.push_back(variables[i]);
		break;
	case '0':
		count_off++;
		vars_off.push_back(variables[i]);
		break;
	case '-':
	default:
		count_dc++;
		vars_dc.push_back(variables[i]);
		break;
	}
}	

string GTerm::GetIn() const {return inputs;}
char GTerm::GetIn(const int numinput) const {return inputs[numinput];}
string GTerm::GetOut() const  {return outputs;}
char GTerm::GetOut(const int numoutput) const {return outputs[numoutput];}
void GTerm::SetOut(const int numoutput, char set) {outputs[numoutput] = set;}
int GTerm::GetCount_dc() const {return count_dc;}
list<GVariable*> GTerm::GetVars(char set) const
{
	switch (set)
	{
	case '1': return vars_on;
		break;
	case '0': return vars_off;
		break;
	case '-': return vars_dc;
		break;
	default: 
		throw "wrong set";
	}
}

bool GTerm::Satisfy(const string &_variables) const
{
	if (inputs.length()!=_variables.length()) return false;
	for (unsigned int i=0;i<inputs.length();i++)
		if ((inputs[i]!=_variables[i]) && (inputs[i]!='-')) return false;
	return true;
}

bool GTerm::operator>(const GTerm &druhy) {return (GetCount_dc() > druhy.GetCount_dc());}
bool GTerm::operator<(const GTerm &druhy) {return (GetCount_dc() < druhy.GetCount_dc());}
bool GTerm::operator>=(const GTerm &druhy) {return (GetCount_dc() >= druhy.GetCount_dc());}
bool GTerm::operator<=(const GTerm &druhy) {return (GetCount_dc() <= druhy.GetCount_dc());}
ostream& operator<< (ostream &os, const GTerm &t)
{
	return os << t.GetIn() << " " << t.GetOut() << endl;
}

bool PointerTermCompareLower(GTerm *t1, GTerm *t2){return (*t1 < *t2);}
bool PointerTermCompareHigher(GTerm *t1, GTerm *t2){return (*t1 > *t2);}

bool PointerTermCompare(GTerm *t1, GTerm *t2) {return (t1->GetCount_dc() == t2->GetCount_dc());}
//
// GVariable
//
GVariable::GVariable(int numoutputs, const int counter) : number(counter)
{
	outputs = new Outputs[numoutputs];
	for (int i=0;i<numoutputs;i++)
	{
		outputs[i].count_on = 0; outputs[i].count_off = 0; outputs[i].count_dc = 0;
	}
}
GVariable::~GVariable()
{
	delete [] outputs;
}

int GVariable::GetNum() const {return number;}
void GVariable::AddTermFromPLALine(GTerm *term, const char &relation)
{
	string out = term->GetOut(); //vystupy
	for (unsigned int i=0;i<out.size();i++) //pro vsechny vystupy
	{
		switch (out[i]) //mrkni, zda je to onset, offset nebo dont care
		{
		case '1':
			outputs[i].count_on++; //dalsi onsetovy term pro vystup i
			switch (relation) //do ktereho listu presne patri? 
			{
				case '1':	outputs[i].onset.term_on.push_back(term);	break;
				case '0':	outputs[i].onset.term_off.push_back(term); break;
				case '-':
				default:	outputs[i].onset.term_dc.push_back(term);	break;
			}
			break;
		case '0':
			outputs[i].count_off++; //dalsi offsetovy term pro vystup i
			switch (relation) //do ktereho listu presne patri? 
			{
				case '1':	outputs[i].offset.term_on.push_back(term);	break;
				case '0':	outputs[i].offset.term_off.push_back(term); break;
				case '-':
				default:	outputs[i].offset.term_dc.push_back(term);	break;
			}
			break;
		case '-':
			outputs[i].count_dc++; //dalsi offsetovy term pro vystup i
			switch (relation) //do ktereho listu presne patri? 
			{
				case '1':	outputs[i].dcset.term_on.push_back(term);	break;
				case '0':	outputs[i].dcset.term_off.push_back(term); break;
				case '-':
				default:	outputs[i].dcset.term_dc.push_back(term);	break;
			}
			break;
		}
	}
}

void GVariable::RemoveTerm(GTerm *term, const char &relation)
{
	string out = term->GetOut(); //vystupy
	for (unsigned int i=0;i<out.size();i++) //pro vsechny vystupy
	{
		switch (out[i]) //mrkni, zda je to onset, offset nebo dont care
		{
		case '1':
			outputs[i].count_on--;
			switch (relation)
			{
				case '1':	outputs[i].onset.term_on.remove(term); break;
				case '0':	outputs[i].onset.term_off.remove(term); break;
				case '-':
				default:	outputs[i].onset.term_dc.remove(term);	break;
			}
			break;
		case '0':
			outputs[i].count_off--; 
			switch (relation) 
			{
				case '1':	outputs[i].offset.term_on.remove(term);	break;
				case '0':	outputs[i].offset.term_off.remove(term); break;
				case '-':
				default:	outputs[i].offset.term_dc.remove(term);	break;
			}
			break;
		case '-':
			outputs[i].count_dc--; 
			switch (relation) 
			{
				case '1':	outputs[i].dcset.term_on.remove(term);	break;
				case '0':	outputs[i].dcset.term_off.remove(term); break;
				case '-':
				default:	outputs[i].dcset.term_dc.remove(term);	break;
			}
			break;
		}
	}
}



void GVariable::AddTermOutput(GTerm *term, const char &relation, const int num_output, const char new_output)
{
	switch (new_output) //mrkni, zda je to onset, offset nebo dont care
	{
	case '1':
		outputs[num_output].count_on++;
		switch (relation)
		{
			case '1':	
				outputs[num_output].onset.term_on.push_back(term); 
				break;
			case '0':	
				outputs[num_output].onset.term_off.push_back(term);
				break;
			case '-':
			default:	
				outputs[num_output].onset.term_dc.push_back(term);
				break;
		}
		break;
	case '0':
		outputs[num_output].count_off++; 
		switch (relation) 
		{
			case '1':	
				outputs[num_output].offset.term_on.push_back(term);
				break;
			case '0':	
				outputs[num_output].offset.term_off.push_back(term); 
				break;
			case '-':
			default:	
				outputs[num_output].offset.term_dc.push_back(term);	
				break;
		}
		break;
	case '-':
		outputs[num_output].count_dc++; 
		switch (relation) 
		{
			case '1':	outputs[num_output].dcset.term_on.push_back(term);	break;
			case '0':	outputs[num_output].dcset.term_off.push_back(term); break;
			case '-':
			default:	outputs[num_output].dcset.term_dc.push_back(term);	break;
		}
		break;
	}
}
void GVariable::RemoveTermOutput(GTerm *term, const char &relation, const int num_output, const char old_output)
{
//	string out = term->GetOut(); //vystupy
//	switch (out[num_output]) 
	switch (old_output) //mrkni, zda je to onset, offset nebo dont care
	{
	case '1':
		outputs[num_output].count_on--;
		switch (relation)
		{
			case '1':	outputs[num_output].onset.term_on.remove(term); break;
			case '0':	outputs[num_output].onset.term_off.remove(term); break;
			case '-':
			default:	outputs[num_output].onset.term_dc.remove(term);	break;
		}
		break;
	case '0':
		outputs[num_output].count_off--; 
		switch (relation) 
		{
			case '1':	outputs[num_output].offset.term_on.remove(term);	break;
			case '0':	outputs[num_output].offset.term_off.remove(term); break;
			case '-':
			default:	outputs[num_output].offset.term_dc.remove(term);	break;
		}
		break;
	case '-':
		outputs[num_output].count_dc--; 
		switch (relation) 
		{
			case '1':	outputs[num_output].dcset.term_on.remove(term);	break;
			case '0':	outputs[num_output].dcset.term_off.remove(term); break;
			case '-':
			default:	outputs[num_output].dcset.term_dc.remove(term);	break;
		}
		break;
	}
}
list<GTerm*> GVariable::GetTerms(int output, char set, char list) const
{
	switch (set)
	{
		case '1': 
			switch (list)
			{
				case '1': return outputs[output].onset.term_on; break;
				case '0': return outputs[output].onset.term_off; break;
				case '-': return outputs[output].onset.term_dc; break;
				default: throw "wrong set";
			}
		break;
		case '0':
			switch (list)
			{
				case '1': return outputs[output].offset.term_on; break;
				case '0': return outputs[output].offset.term_off; break;
				case '-': return outputs[output].offset.term_dc; break;
				default: throw "wrong set";
			}
		break;
		case '-':
			switch (list)
			{
				case '1': return outputs[output].dcset.term_on; break;
				case '0': return outputs[output].dcset.term_off; break;
				case '-': return outputs[output].dcset.term_dc; break;
				default: throw "wrong set";
			}
		break;
		default: throw "wrong set";
	}
}
// 
// graf
//
Graph::Graph() {count_terms = -1;}

Graph::~Graph()
{
	for (list<GTerm*>::iterator iter = terms.begin(); iter != terms.end(); iter++)
		delete (*iter);
	delete [] outputs;
	for (int i = 0; i < count_inputs; i++) delete variables[i];
}
// 
// private
//
GTerm* Graph::ConstructFromPLALine(string &_inputs, string &_outputs) //pridava do grafu term podle radku v PLA
{
	if (_inputs.length()!=count_inputs) throw "wrong size of term inputs";
	if (_outputs.length()!=count_outputs) throw "wrong size of term outputs";

	bool del = true;
	for (int i = 0; i < count_outputs; i++) if (_outputs[i] != '~') {del = false; break;}
	if (del) return NULL;

	//zkusime se podivat, jestli uz neni term s temito vstupy definovan
	GTerm* target = NULL;
	int count_on = 0, count_off = 0, count_dc = 0;
	for (int i = 0; i < count_inputs;i++)
	{
		switch (_inputs[i])
		{
		case '1':
			count_on++;
			break;
		case '0':
			count_off++;
			break;
		case '-':
			count_dc++;
			break;
		}
	} //napocitame jednicky, nuly a dontcare ve vstupu
	for (list<GTerm*>::iterator iter = terms.begin(); iter != terms.end(); iter++)
	{
		if ((*iter)->count_dc != count_dc) continue; 
		if ((*iter)->count_on != count_on) continue;
		if ((*iter)->inputs != _inputs) continue;
		else
		{
			target = *iter; //nasli jsme cil
			break;
		}
	}

	if (target != NULL) //term s takovymto vstupem uz existuje
	{
		for (int i = 0; i < count_outputs; i++) //projdeme jeho vystupy
		{
			if (_outputs[i]!='~') //vystup noveho termu na pozici I neni no meaning
			{
				if (target->GetOut(i) =='~') //vystup puvodniho termu na I je no meaning
				{
					target->SetOut(i, _outputs[i]);
					outputs[i].terms_nm.remove(target);
					switch (_outputs[i])
					{
					case '1':
						outputs[i].terms_on.push_back(target);
						break;
					case '0':
						outputs[i].terms_off.push_back(target);
						break;
					case '-':
						outputs[i].terms_dc.push_back(target);
						break;
					default:
						break;
					}
					for (unsigned int q=0;q<_inputs.length();q++)
					{
						variables[q]->AddTermOutput(target, _inputs[q], i, _outputs[i]);
					}
				}
				else //vystup puvodniho neni no meaning!
				{
					if (_outputs[i] != target->GetOut(i)) //throw "There is a conflict between outputs in PLA file.";
					{
						// jeste se muze stat, ze typ je FD a je to konflikt DCsetu s ONsetem
						// to je pak v poradku a prednost ma DCSET
						if (type != fd) throw "Graph: There is a conflict between outputs in PLA file.";
						else
						{
							if (target->GetOut(i)=='1')
							{
								if (_outputs[i] == '-') //zmena z onsetu na dcset
								{
									SetTermOutput(target, i, '-');
								}
								else throw "Graph: There is a conflict between outputs in PLA file.";
							}
							else if (target->GetOut(i) == '-')
							{
								if (_outputs[i] != '1') throw "Graph: There is a conflict between outputs in PLA file.";
							}
							else throw "Graph: There is a conflict between outputs in PLA file.";
						}
					}
				}
			}
		}
		return target;
	}

	GTerm *pom = new GTerm(_inputs, _outputs, variables);
	terms.push_back(pom);
	count_terms++;
	for (int i=0;i<count_outputs;i++)
	{
		switch (_outputs[i])
		{
		case '1':
			outputs[i].terms_on.push_back(pom);
			break;
		case '0':
			outputs[i].terms_off.push_back(pom);
			break;
		case '-':
			outputs[i].terms_dc.push_back(pom);
			break;
		case '~':
			outputs[i].terms_nm.push_back(pom);
			break;
		default:
			break;
		}
	}

	for (unsigned int i=0;i<_inputs.length();i++)
	{
		variables[i]->AddTermFromPLALine(pom,_inputs[i]);
	}
	return pom;
}

void Graph::SetParams(const graphtype &_type, const int &numinputs, const int &numoutputs, const string &_input_names, const string &_output_names)
{
	if (numinputs<=0) throw "inputs must be higher than 0";
	if (numoutputs<=0) throw "inputs must be higher than 0";
	count_terms = 0;
	type = _type;
	count_inputs = numinputs;
	count_outputs = numoutputs;
	outputs = new Outputs[numoutputs];
	for (int i=0;i<numinputs;i++) 
	{
		variables.push_back(new GVariable(numoutputs, i));
	}
	input_names = _input_names;
	output_names = _output_names;
}


void Graph::RemoveTerm(GTerm *term)
{
	string str = term->GetIn();
	for (int i=0;i<count_inputs;i++) variables[i]->RemoveTerm(term,str[i]);
	
	list<GTerm*>::iterator iter;
	str = term->GetOut();
	for (int i=0;i<count_outputs;i++) 
	{
		switch (str[i])
		{
		case '1': 
			outputs[i].terms_on.remove(term);
			break;
		case '0': 
			outputs[i].terms_off.remove(term);
			break;
		case '-': 
			outputs[i].terms_dc.remove(term);
			break;
		case '~':
			outputs[i].terms_nm.remove(term);
			break;
		}
	}

	terms.remove(term);
	count_terms--;
	delete term;
}


void Graph::RemoveTermOutput(GTerm *term, const int num_output)
{
	string str = term->GetOut();
	char old_output = str[num_output];
	
	str = term->GetIn();
	for (int i=0;i<count_inputs;i++) variables[i]->RemoveTermOutput(term,str[i],num_output, old_output);
	
	list<GTerm*>::iterator iter;
	switch (old_output)
	{
	case '1': 
		outputs[num_output].terms_on.remove(term);
		outputs[num_output].terms_nm.push_back(term);
		break;
	case '0': 
		outputs[num_output].terms_off.remove(term);
		outputs[num_output].terms_nm.push_back(term);
		break;
	case '-': 
		outputs[num_output].terms_dc.remove(term);
		outputs[num_output].terms_nm.push_back(term);
		break;
	}
	
	term->SetOut(num_output, '~');
	str = term->GetOut();
	bool del = true;
	for (int i = 0; i < count_outputs; i++) if (str[i] != '~') {del = false; break;}
	if (del) RemoveTerm(term);
}

GTerm* Graph::AddTermOutput(string &t_input, const int &num_output, char new_output)
{
	if (num_output > count_outputs -1) throw "Function AddTerm: output number out of range";
	list<GTerm*> targets;
	GTerm* target = NULL;
	targets = terms;

	int count_on = 0, count_off = 0, count_dc = 0;
	for (int i = 0; i < count_inputs;i++)
	{
		switch (t_input[i])
		{
		case '1':
			count_on++;
			break;
		case '0':
			count_off++;
			break;
		case '-':
			count_dc++;
			break;
		}
	} //napocitame jednicky, nuly a dontcare ve vstupu
	
	for (list<GTerm*>::iterator iter = targets.begin(); iter != targets.end(); iter++)
	{
		if ((*iter)->count_dc != count_dc) continue; 
		if ((*iter)->count_on != count_on) continue;
		if ((*iter)->inputs != t_input) continue;
		else
		{
			target = *iter; //nasli jsme cil
			break;
		}
	}

	if (target != NULL) //term uz existuje
	{
		char old_out = target->GetOut(num_output);
		if (old_out != '~')
		{
			if (old_out != new_output) //KONFLIKT VE VYSTUPECH!!
			{
				if (type != fd) throw "Graph: There is conflict between outputs! ";
				else //fd muze mit konflikt DCSETu s ONSETem
				{
					if (old_out == '-')
					{
						if (new_output == '1') return NULL; //
						else throw "Graph: There is conflict between outputs! ";
					}
					else 
					{
						if (old_out == '1')
						{
							if (new_output == '-') 
							{
								SetTermOutput(target, num_output, new_output);
								return NULL; //prenastaveno na DCSET, ale neni duvod vracet novy objekt
							}
							else throw "Graph: There is conflict between outputs! ";
						}
						else throw "Graph: There is conflict between outputs! ";
					}
				}
			}
			else //existoval vystup uplne stejny jako ten, ktery ukladame
			{
				return NULL;
			}
		}
		else
		{
			outputs[num_output].terms_nm.remove(target);
			target->SetOut(num_output, new_output);
			switch (new_output)
			{
			case '1':
				outputs[num_output].terms_on.push_back(target);
				break;
			case '0':
				outputs[num_output].terms_off.push_back(target);
				break;
			case '-':
				outputs[num_output].terms_dc.push_back(target);
				break;
			default: 
				throw "Function AddTerm: Unacceptable output: {1,0,-} only";
				break;
			}
			for (int q=0;q<count_inputs;q++)
			{
				variables[q]->AddTermOutput(target, t_input[q], num_output, new_output);
			}

			return target; //term uz existoval, jen jsme mu pridali novy vystup, kde ho predtim nemel
		}
	}
	else //zadny neodpovida vystupem, ani tam zadny nema no meaning, musime jej vytvorit
	{
		//tak term nakonec prece jen vubec jeste neexistuje, vytvorime novy
		string str2;
		str2 = ""; 
		for (int i=0;i<count_outputs;i++) str2 += "~"; //vystupy nastav na ~~~~~
		str2[num_output] = new_output; //a ten spravny vystup predelej
		GTerm *retterm = ConstructFromPLALine(t_input, str2); //vytvor term
		return retterm;
	}
}

void Graph::AddTermOutput(GTerm *target, const int &num_output, char new_output)
{
	if (num_output > count_outputs - 1) throw "Graph: Function AddTerm: output number out of range";
	if (target == NULL) throw "Graph: term does not exist";

	if (target->GetOut(num_output) == '~')
	{
		outputs[num_output].terms_nm.remove(target);
		target->SetOut(num_output, new_output);
		switch (new_output)
		{
		case '1':
			outputs[num_output].terms_on.push_back(target);
			break;
		case '0':
			outputs[num_output].terms_off.push_back(target);
			break;
		case '-':
			outputs[num_output].terms_dc.push_back(target);
			break;
		default: 
			throw "Function AddTerm: Unacceptable output: {1,0,-} only";
			break;
		}

		string t_input = target->GetIn();
		for (int q=0;q<count_inputs;q++)
		{
			variables[q]->AddTermOutput(target, t_input[q], num_output, new_output);
		}

		return;
//		return NULL; //term uz existoval, jen jsme mu pridali novy vystup
	}
	else //vystup nebyl v no meaning, jeste muze odpovidat
	{
		if (target->GetOut(num_output) == new_output)
		{
			return; //nasli jsme term, ktery vystupem odpovida, nic se nemeni
		}
		else throw "Graph: there is a conflict between term outputs";
	}
}

void Graph::SetTermOutput(GTerm *term, const int &num_output, char new_output)
{
	if (num_output > count_outputs - 1) throw "Graph: Function AddTerm: output number out of range";
	if (term == NULL) throw "Graph: term does not exist";

	string str = term->GetOut();
	char old_output = str[num_output];
	
	str = term->GetIn();
	for (int i=0;i<count_inputs;i++) 
	{
		variables[i]->RemoveTermOutput(term,str[i],num_output, old_output);
		variables[i]->AddTermOutput(term, str[i], num_output, new_output);
	}
	
	switch (old_output)
	{
	case '1': 
		outputs[num_output].terms_on.remove(term);
		break;
	case '0': 
		outputs[num_output].terms_off.remove(term);
		break;
	case '-': 
		outputs[num_output].terms_dc.remove(term);
		break;
	}
	
	term->SetOut(num_output, new_output);
	switch (new_output)
	{
		case '1':
			outputs[num_output].terms_on.push_back(term);
			break;
		case '0':
			outputs[num_output].terms_off.push_back(term);
			break;
		case '-':
			outputs[num_output].terms_dc.push_back(term);
			break;
		default: 
			throw "Function AddTerm: Unacceptable output: {1,0,-} only";
			break;
	}

	return;
}
//
// 
//
void Graph::Simplification(const int num_output)
{
	struct TermMatch //term pro upravy
	{
		GTerm *t; //ukazatel na term
		GVariable *differentvar; //rozdilna promenna oproti nadrazenemu termu, existuje-li
		TermMatch(GTerm *term) {t = term; differentvar = NULL;}
	};
	list<GTerm*> listtmp, listtmp2;
	list<TermMatch> smallerterms; //mensi a stejne velke termy
	list<GVariable*> listvar;
	GTerm *t;
	char outset;
	bool newhigherinlist = false;

	listtmp = terms; //bereme vsechny termy
	listtmp.sort(PointerTermCompareHigher); //seradime termy od nejvetsiho
	list<GTerm*>::iterator iter = listtmp.begin();

	while (iter != listtmp.end())
	{//projdeme vsechny termy
		smallerterms.clear(); //procistime seznam mensich termu
		t = *iter; //vezmi term
		outset = t->GetOut(num_output);
		if (outset == '~') //termy bez vyznamu preskakuj
		{
			iter++;
			continue;
		}
		list<GTerm*>::iterator it = iter; it++;
		for (it; it!=listtmp.end(); it++)
		{ //jestli dava na vystup totez co prvni term, zarad jej to seznamu
			if (outset == (*it)->GetOut(num_output)) 
			{
				smallerterms.push_back(TermMatch(*it));
			}
		}

		//ted v t je nejvetsi term z nasi skupiny s nejakym vysledkem (1,0,-)
		//a ve smallerterms jsou vsechny mensi (a stejne velke) termy se stejnym vysledkem
		//vysledek je v outset
		/*
			abychom mohli mensi termy kratit
				a) vsude, kde vetsi term nema DC se musi shodovat - v takovem pripade cely mensi term pohltime
				b) vsude, kde vetsi term nema DC se shoduji, az na jednu pozici - v takovem pripade te pozici v mensim termu dame DC
		*/

		listvar = t->GetVars('1'); //promenne, kde tento term ma 1
		for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(num_output, outset, '-'); //termy, ktere tam maji -
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
						break; //done
					}
				}
			}

			listtmp2 = (*variter)->GetTerms(num_output, outset, '0'); //termy, ktere tam maji 0
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ 
					if ((*it) == (*it2).t) //nalezeno
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							(*it2).differentvar = *variter; //zaznamename jej
							break; //done
						}
						else //vice rozdilu, je na case jej smazat
						{
							smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}


		listvar = t->GetVars('0'); //promenne, kde tento term ma 0
				for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(num_output, outset, '-'); //termy, ktere tam maji -
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
						break; //done
					}
				}
			}

			listtmp2 = (*variter)->GetTerms(num_output, outset, '1'); //termy, ktere tam maji 1
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							(*it2).differentvar = *variter; //zaznamename jej
							break; //done
						}
						else //vice rozdilu, je na case jej smazat
						{
							smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}

		//hotovo, ted projdeme vsechny mensi termy, ktere jsme jeste nevyradili
		//v t je nejvetsi term z nasi skupiny s nejakym vysledkem (1,0,-)
		//a ve smallerterms jsou vsechny mensi (a stejne velke) termy se stejnym vysledkem, ktere
		/*
				a) vsude, kde vetsi term nema DC se shoduji - v takovem pripade cely mensi term pohltime
				b) vsude, kde vetsi term nema DC se shoduji, az na jednu pozici - v takovem pripade te pozici v mensim termu dame DC

			tzn.
			a) nemaji zadnou differentvar, cele je muzem pro tento vystup odstranit
			b) maji jednu differentvar, staci mensimu termu nastavit do polarity te promenne dontcare
		*/
		
		list<GTerm*> newterms;
		for (list<TermMatch>::iterator it = smallerterms.begin(); it != smallerterms.end(); it++)
		{
			if ((*it).differentvar == NULL) //term odstranime
			{
				listtmp.remove((*it).t); //odstranime ho z aktualniho listu, co zkracujeme
				RemoveTermOutput((*it).t,num_output); //odstranime jeho vystup ze vsech struktur
			}
			else //vytvorime novy term pro tento jeden vystup, stary smazeme (nahrazeni)
			{
				if (PointerTermCompare((*it).t,t)) //pokud jsou termy stejne velike
					newhigherinlist = true; //mame nove vytvoreny vetsi
				int numvar = (*it).differentvar->GetNum(); //ve ktere promenne se termy lisi
				string str1, str2;
				str1 = ((*it).t)->GetIn(); //puvodni vstupy termu
				str1[numvar] = '-'; //zmenen vstup na doncare
				
				GTerm *retterm = AddTermOutput(str1, num_output, ((*it).t)->GetOut(num_output));
				if (retterm != NULL)
					newterms.push_back(retterm);//pridame novy term do seznamu				
				listtmp.remove((*it).t); //odstranime ho z aktualniho listu, co zkracujeme
				RemoveTermOutput((*it).t,num_output); //odstranime vystup termu ze vsech struktur*/
			}		
		}
		newterms.sort(PointerTermCompareHigher);
		listtmp.merge(newterms,PointerTermCompareHigher);
		if (newhigherinlist) //mame novy vetsi term
		{
			list<GTerm*>::iterator it = iter; //ulozime si to
			bool begin = false;
			while (!PointerTermCompareHigher(*iter, *it))
			{
				if (iter == listtmp.begin())
				{
					begin = true;
					break;
				}
				iter--;
			}
			
			//iter ted ukazuje na posledni z o 1 vetsich termu (ale potrebujeme az na prvni) (nebo na prvni term)
			it = iter; //opet si to ulozime
			while (!PointerTermCompareHigher(*iter, *it))
			{
				if (iter == listtmp.begin())
				{
					begin = true;
					break;
				}
				iter--;
			}
			//iter ted ukazuje na posledni z o 2 vetsich termu (nebo na prvni term)
			if (!begin) iter++;
			//ukazuje na prvni z o 1 vetsich termu, to co potrebujeme
			newhigherinlist = false;
		}
		else iter++; //zadny novy neni, pokracujem
	}
}

void Graph::SimplificationWithDontCares(const int num_output)
{
//nejprve provedeme operaci podobnou Simplification, pouze pozmenenou o to, ze budeme uvazovat dontcares
	struct TermMatch //term pro upravy
	{
		GTerm *t; //ukazatel na term
		GVariable *differentvar; //rozdilna promenna oproti nadrazenemu termu, existuje-li
		TermMatch(GTerm *term) {t = term; differentvar = NULL;}
	};
	list<GTerm*> listtmp, listtmp2, ltmp;
	list<TermMatch> smallerterms; //mensi a stejne velke termy
	list<GVariable*> listvar;
	GTerm *t;
	char outset;
	bool newhigherinlist = false;

	listtmp = outputs[num_output].terms_on; //bereme onset termy
	listtmp.insert(listtmp.end(), outputs[num_output].terms_dc.begin(), outputs[num_output].terms_dc.end());
	//pridame dcset termy
	listtmp.sort(PointerTermCompareHigher); //seradime termy od nejvetsiho
	list<GTerm*>::iterator iter = listtmp.begin();

	while (iter != listtmp.end())
	{//projdeme vsechny termy
		smallerterms.clear(); //procistime seznam mensich termu
		t = *iter; //vezmi term
		outset = t->GetOut(num_output);

		list<GTerm*>::iterator it = iter; it++;
		for (it; it!=listtmp.end(); it++)
		{ //vsechny dalsi termy zarad do seznamu
			smallerterms.push_back(TermMatch(*it));
		}

		//ted v t je nejvetsi term z nasi skupiny s vysledkem {1,-}
		//a ve smallerterms jsou vsechny mensi (a stejne velke) termy
		//vysledek je v outset
		/*
			abychom mohli mensi termy kratit
				a) vsude, kde vetsi term nema DC se musi shodovat - v takovem pripade cely mensi term pohltime
				b) vsude, kde vetsi term nema DC se shoduji, az na jednu pozici - v takovem pripade te pozici v mensim termu dame DC

			!!! - pokud jsme pouzili velky term z DCsetu na kraceni mensiho termu z ONsetu, stava se 
			velky term rovnez ONsetovym termem - !!!
		*/

		listvar = t->GetVars('1'); //promenne, kde tento term ma 1
		for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(num_output, '1', '-'); //termy, ktere tam maji -
			ltmp = (*variter)->GetTerms(num_output, '-', '-');
			listtmp2.insert(listtmp2.end(), ltmp.begin(), ltmp.end()); 
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
						break; //done
					}
				}
			}

			listtmp2 = (*variter)->GetTerms(num_output, '1', '0'); //termy, ktere tam maji 0
			ltmp = (*variter)->GetTerms(num_output, '-', '0');
			listtmp2.insert(listtmp2.end(), ltmp.begin(), ltmp.end()); 
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ 
					if ((*it) == (*it2).t) //nalezeno
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							(*it2).differentvar = *variter; //zaznamename jej
							break; //done
						}
						else //vice rozdilu, je na case jej smazat
						{
							smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}


		listvar = t->GetVars('0'); //promenne, kde tento term ma 0
				for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(num_output, '1', '-'); //termy, ktere tam maji -
			ltmp = (*variter)->GetTerms(num_output, '-', '-');
			listtmp2.insert(listtmp2.end(), ltmp.begin(), ltmp.end()); 
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
						break; //done
					}
				}
			}

			listtmp2 = (*variter)->GetTerms(num_output, '1', '1'); //termy, ktere tam maji 1
			ltmp = (*variter)->GetTerms(num_output, '-', '1'); 
			listtmp2.insert(listtmp2.end(), ltmp.begin(), ltmp.end());
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							(*it2).differentvar = *variter; //zaznamename jej
							break; //done
						}
						else //vice rozdilu, je na case jej smazat
						{
							smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}

		//hotovo, ted projdeme vsechny mensi termy, ktere jsme jeste nevyradili
		//v t je nejvetsi term z nasi skupiny s vysledkem {1,-}
		//a ve smallerterms jsou vsechny mensi (a stejne velke) termy, ktere
		/*
				a) vsude, kde vetsi term nema DC se shoduji - v takovem pripade cely mensi term pohltime
				b) vsude, kde vetsi term nema DC se shoduji, az na jednu pozici - v takovem pripade te pozici v mensim termu dame DC

				pokud vetsi term je z dcsetu a libovolny z mensich je v onsetu, stava se velky term 
				take onsetovym

			tzn.
			a) nemaji zadnou differentvar, cele je muzem pro tento vystup odstranit
			b) maji jednu differentvar, staci mensimu termu nastavit do polarity te promenne dontcare

			pokud ve smallterms existuje cokoliv onsetoveho, prehod velky term na onset
		*/
		
		if (outset == '-') //pokud je hlavni term z dcset
		{
			for (list<TermMatch>::iterator it = smallerterms.begin(); it != smallerterms.end(); it++)
			{
				if ((*it).t->GetOut(num_output) == '1') //a zaroven se v mensich nachazi nejaky z onset
				{
					//udelej z hlavniho termu rovnez onset
					SetTermOutput(t, num_output, '1');
					break;
				}
			}
		}

		list<GTerm*> newterms;
		for (list<TermMatch>::iterator it = smallerterms.begin(); it != smallerterms.end(); it++)
		{
			if ((*it).differentvar == NULL) //term odstranime
			{
				listtmp.remove((*it).t); //odstranime ho z aktualniho listu, co zkracujeme
				RemoveTermOutput((*it).t,num_output); //odstranime jeho vystup ze vsech struktur
			}
			else //vytvorime novy term pro tento jeden vystup, stary smazeme (nahrazeni)
			{
				if (PointerTermCompare((*it).t,t)) //pokud jsou termy stejne velike
					newhigherinlist = true; //mame nove vytvoreny vetsi
				int numvar = (*it).differentvar->GetNum(); //ve ktere promenne se termy lisi
				string str1, str2;
				str1 = ((*it).t)->GetIn(); //puvodni vstupy termu
				str1[numvar] = '-'; //zmenen vstup na doncare
				
				GTerm *retterm = AddTermOutput(str1, num_output, ((*it).t)->GetOut(num_output));
				if (retterm != NULL)
					newterms.push_back(retterm);//pridame novy term do seznamu				
				listtmp.remove((*it).t); //odstranime ho z aktualniho listu, co zkracujeme
				RemoveTermOutput((*it).t,num_output); //odstranime vystup termu ze vsech struktur*/
			}		
		}
		newterms.sort(PointerTermCompareHigher);
		listtmp.merge(newterms,PointerTermCompareHigher);
		if (newhigherinlist) //mame novy vetsi term
		{
			list<GTerm*>::iterator it = iter; //ulozime si to
			bool begin = false;
			while (!PointerTermCompareHigher(*iter, *it))
			{
				if (iter == listtmp.begin())
				{
					begin = true;
					break;
				}
				iter--;
			}
			
			//iter ted ukazuje na posledni z o 1 vetsich termu (ale potrebujeme az na prvni) (nebo na prvni term)
			it = iter; //opet si to ulozime
			while (!PointerTermCompareHigher(*iter, *it))
			{
				if (iter == listtmp.begin())
				{
					begin = true;
					break;
				}
				iter--;
			}
			//iter ted ukazuje na posledni z o 2 vetsich termu (nebo na prvni term)
			if (!begin) iter++;
			//ukazuje na prvni z o 1 vetsich termu, to co potrebujeme
			newhigherinlist = false;
		}
		else iter++; //zadny novy neni, pokracujem
	}
}
void Graph::SimplificationWithDontCares(const int num_output, list<GTerm*> &essentials)
{
//nejprve provedeme operaci podobnou Simplification, pouze pozmenenou o to, ze budeme uvazovat dontcares
	struct TermMatch //term pro upravy
	{
		GTerm *t; //ukazatel na term
		GVariable *differentvar; //rozdilna promenna oproti nadrazenemu termu, existuje-li
		TermMatch(GTerm *term) {t = term; differentvar = NULL;}
	};
	list<GTerm*> listtmp, listtmp2, ltmp;
	list<TermMatch> smallerterms; //mensi a stejne velke termy
	list<GVariable*> listvar;
	GTerm *t;
	char outset;
	bool newhigherinlist = false;

	listtmp = outputs[num_output].terms_on; //bereme onset termy
	listtmp.insert(listtmp.end(), outputs[num_output].terms_dc.begin(), outputs[num_output].terms_dc.end());
	//pridame dcset termy
	listtmp.sort(PointerTermCompareHigher); //seradime termy od nejvetsiho
	list<GTerm*>::iterator iter = listtmp.begin();

	while (iter != listtmp.end())
	{//projdeme vsechny termy
		smallerterms.clear(); //procistime seznam mensich termu
		t = *iter; //vezmi term
		outset = t->GetOut(num_output);

		list<GTerm*>::iterator it = iter; it++;
		for (it; it!=listtmp.end(); it++)
		{ //vsechny dalsi termy zarad do seznamu
			smallerterms.push_back(TermMatch(*it));
		}

		//ted v t je nejvetsi term z nasi skupiny s vysledkem {1,-}
		//a ve smallerterms jsou vsechny mensi (a stejne velke) termy
		//vysledek je v outset
		/*
			abychom mohli mensi termy kratit
				a) vsude, kde vetsi term nema DC se musi shodovat - v takovem pripade cely mensi term pohltime
				b) vsude, kde vetsi term nema DC se shoduji, az na jednu pozici - v takovem pripade te pozici v mensim termu dame DC

			!!! - pokud jsme pouzili velky term z DCsetu na kraceni mensiho termu z ONsetu, stava se 
			velky term rovnez ONsetovym termem - !!!
		*/

		listvar = t->GetVars('1'); //promenne, kde tento term ma 1
		for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(num_output, '1', '-'); //termy, ktere tam maji -
			ltmp = (*variter)->GetTerms(num_output, '-', '-');
			listtmp2.insert(listtmp2.end(), ltmp.begin(), ltmp.end()); 
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
						break; //done
					}
				}
			}

			listtmp2 = (*variter)->GetTerms(num_output, '1', '0'); //termy, ktere tam maji 0
			ltmp = (*variter)->GetTerms(num_output, '-', '0');
			listtmp2.insert(listtmp2.end(), ltmp.begin(), ltmp.end()); 
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ 
					if ((*it) == (*it2).t) //nalezeno
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							(*it2).differentvar = *variter; //zaznamename jej
							break; //done
						}
						else //vice rozdilu, je na case jej smazat
						{
							smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}


		listvar = t->GetVars('0'); //promenne, kde tento term ma 0
				for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(num_output, '1', '-'); //termy, ktere tam maji -
			ltmp = (*variter)->GetTerms(num_output, '-', '-');
			listtmp2.insert(listtmp2.end(), ltmp.begin(), ltmp.end()); 
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
						break; //done
					}
				}
			}

			listtmp2 = (*variter)->GetTerms(num_output, '1', '1'); //termy, ktere tam maji 1
			ltmp = (*variter)->GetTerms(num_output, '-', '1'); 
			listtmp2.insert(listtmp2.end(), ltmp.begin(), ltmp.end());
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							(*it2).differentvar = *variter; //zaznamename jej
							break; //done
						}
						else //vice rozdilu, je na case jej smazat
						{
							smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}

		//hotovo, ted projdeme vsechny mensi termy, ktere jsme jeste nevyradili
		//v t je nejvetsi term z nasi skupiny s vysledkem {1,-}
		//a ve smallerterms jsou vsechny mensi (a stejne velke) termy, ktere
		/*
				a) vsude, kde vetsi term nema DC se shoduji - v takovem pripade cely mensi term pohltime
				b) vsude, kde vetsi term nema DC se shoduji, az na jednu pozici - v takovem pripade te pozici v mensim termu dame DC

				pokud vetsi term je z dcsetu a libovolny z mensich je v onsetu, stava se velky term 
				take onsetovym

			tzn.
			a) nemaji zadnou differentvar, cele je muzem pro tento vystup odstranit
			b) maji jednu differentvar, staci mensimu termu nastavit do polarity te promenne dontcare

			pokud ve smallterms existuje cokoliv onsetoveho, prehod velky term na onset
		*/
		
		if (outset == '-') //pokud je hlavni term z dcset
		{
			for (list<TermMatch>::iterator it = smallerterms.begin(); it != smallerterms.end(); it++)
			{
				if ((*it).t->GetOut(num_output) == '1') //a zaroven se v mensich nachazi nejaky z onset
				{
					//udelej z hlavniho termu rovnez onset
					SetTermOutput(t, num_output, '1');
					break;
				}
			}
		}

		list<GTerm*> newterms;
		for (list<TermMatch>::iterator it = smallerterms.begin(); it != smallerterms.end(); it++)
		{
			if ((*it).differentvar == NULL) //term odstranime
			{				
				listtmp.remove((*it).t); //odstranime ho z aktualniho listu, co zkracujeme
				RemoveTermOutput((*it).t,num_output); //odstranime jeho vystup ze vsech struktur
				essentials.remove((*it).t);
			}
			else //vytvorime novy term pro tento jeden vystup, stary smazeme (nahrazeni)
			{
				if (PointerTermCompare((*it).t,t)) //pokud jsou termy stejne velike
					newhigherinlist = true; //mame nove vytvoreny vetsi
				int numvar = (*it).differentvar->GetNum(); //ve ktere promenne se termy lisi
				string str1, str2;
				str1 = ((*it).t)->GetIn(); //puvodni vstupy termu
				str1[numvar] = '-'; //zmenen vstup na doncare
				
				GTerm* retterm = AddTermOutput(str1, num_output, ((*it).t)->GetOut(num_output));
				if (retterm != NULL)
					newterms.push_back(retterm);//pridame novy term do seznamu
				bool essential = false;
				for (list<GTerm*>::iterator ittt = essentials.begin(); ittt != essentials.end(); ittt++)
				{
					if ((*ittt) == ((*it).t))
					{
						essential = true;
						break;
					}
				}
				if (essential == true)
				{
					essentials.remove((*it).t);
					essentials.push_back(retterm);
				}
				listtmp.remove((*it).t); //odstranime ho z aktualniho listu, co zkracujeme
				RemoveTermOutput((*it).t,num_output); //odstranime vystup termu ze vsech struktur*/
			}		
		}
		newterms.sort(PointerTermCompareHigher);
		listtmp.merge(newterms,PointerTermCompareHigher);
		if (newhigherinlist) //mame novy vetsi term
		{
			list<GTerm*>::iterator it = iter; //ulozime si to
			bool begin = false;
			while (!PointerTermCompareHigher(*iter, *it))
			{
				if (iter == listtmp.begin())
				{
					begin = true;
					break;
				}
				iter--;
			}
			
			//iter ted ukazuje na posledni z o 1 vetsich termu (ale potrebujeme az na prvni) (nebo na prvni term)
			it = iter; //opet si to ulozime
			while (!PointerTermCompareHigher(*iter, *it))
			{
				if (iter == listtmp.begin())
				{
					begin = true;
					break;
				}
				iter--;
			}
			//iter ted ukazuje na posledni z o 2 vetsich termu (nebo na prvni term)
			if (!begin) iter++;
			//ukazuje na prvni z o 1 vetsich termu, to co potrebujeme
			newhigherinlist = false;
		}
		else iter++; //zadny novy neni, pokracujem
	}
}
void Graph::Absorbtion_OrthRespect()
{
	for (int i=0;i<count_outputs;i++) Absorbtion_OrthRespect(i);
}
void Graph::Absorbtion_OrthRespect(const int num_output)
{
	struct TermMatch //term pro upravy
	{
		GTerm *t; //ukazatel na term
		GVariable *differentvar; //rozdilna promenna oproti nadrazenemu termu, existuje-li
		TermMatch(GTerm *term) {t = term; differentvar = NULL;}
	};
	list<GTerm*> listtmp, listtmp2;
	list<TermMatch> smallerterms; //mensi a stejne velke termy
	list<GVariable*> listvar;
	GTerm *t;
	char outset;
	bool newhigherinlist = false;

	listtmp = terms; //bereme vsechny termy
	listtmp.sort(PointerTermCompareHigher); //seradime termy od nejvetsiho
	list<GTerm*>::iterator iter = listtmp.begin();

	while (iter != listtmp.end())
	{//projdeme vsechny termy
		smallerterms.clear(); //procistime seznam mensich termu
		t = *iter; //vezmi term
		outset = t->GetOut(num_output);
		if (outset == '~') //termy bez vyznamu preskakuj
		{
			iter++;
			continue;
		}
		list<GTerm*>::iterator it = iter; it++;
		for (it; it!=listtmp.end(); it++)
		{ //jestli dava na vystup totez co prvni term, zarad jej to seznamu
			if (outset == (*it)->GetOut(num_output)) 
			{
				smallerterms.push_back(TermMatch(*it));
			}
		}

		//ted v t je nejvetsi term z nasi skupiny s nejakym vysledkem (1,0,-)
		//a ve smallerterms jsou vsechny mensi (a stejne velke) termy se stejnym vysledkem
		//vysledek je v outset
		/*
			abychom mohli mensi termy kratit
				a) vsude, kde vetsi term nema DC se musi shodovat - v takovem pripade cely mensi term pohltime
				b) vsude, kde vetsi term nema DC se shoduji, az na jednu pozici - v takovem pripade te pozici v mensim termu dame DC
					ale(!) navic se musi shodovat i tam, kde vetsi term ma DC, jinak bychom porusili ortogonalitu!!
		*/

		listvar = t->GetVars('1'); //promenne, kde tento term ma 1
		for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(num_output, outset, '-'); //termy, ktere tam maji -
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
						break; //done
					}
				}
			}

			listtmp2 = (*variter)->GetTerms(num_output, outset, '0'); //termy, ktere tam maji 0
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ 
					if ((*it) == (*it2).t) //nalezeno
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							(*it2).differentvar = *variter; //zaznamename jej
							break; //done
						}
						else //vice rozdilu, je na case jej smazat
						{
							smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}


		listvar = t->GetVars('0'); //promenne, kde tento term ma 0
				for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(num_output, outset, '-'); //termy, ktere tam maji -
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
						break; //done
					}
				}
			}

			listtmp2 = (*variter)->GetTerms(num_output, outset, '1'); //termy, ktere tam maji 1
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							(*it2).differentvar = *variter; //zaznamename jej
							break; //done
						}
						else //vice rozdilu, je na case jej smazat
						{
							smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}

		listvar = t->GetVars('-'); //promenne, kde tento term ma -
				for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(num_output, outset, '0'); //termy, ktere tam maji -
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							break; //tenhle term bude pohlcen, takze je to jedno
						}
						else //vice rozdilu, je na case jej smazat
						{
							smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}

			listtmp2 = (*variter)->GetTerms(num_output, outset, '1'); //termy, ktere tam maji 1
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = smallerterms.begin(); it2 != smallerterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno, vyskrtni jej
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							break; //tenhle term bude pohlcen, takze je to jedno
						}
						else //vice rozdilu, je na case jej smazat
						{
							smallerterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}
		
		list<GTerm*> newterms;
		for (list<TermMatch>::iterator it = smallerterms.begin(); it != smallerterms.end(); it++)
		{
			if ((*it).differentvar == NULL) //term odstranime
			{
				listtmp.remove((*it).t); //odstranime ho z aktualniho listu, co zkracujeme
				RemoveTermOutput((*it).t,num_output); //odstranime jeho vystup ze vsech struktur
			}
			else //vytvorime novy term pro tento jeden vystup, stary smazeme (nahrazeni)
			{
				if (PointerTermCompare((*it).t,t)) //pokud jsou termy stejne velike
					newhigherinlist = true; //mame nove vytvoreny vetsi
				int numvar = (*it).differentvar->GetNum(); //ve ktere promenne se termy lisi
				string str1, str2;
				str1 = ((*it).t)->GetIn(); //puvodni vstupy termu
				str1[numvar] = '-'; //zmenen vstup na doncare
				
				GTerm* retterm = AddTermOutput(str1, num_output, ((*it).t)->GetOut(num_output));
				if (retterm != NULL)
					newterms.push_back(retterm);//pridame novy term do seznamu				
				listtmp.remove((*it).t); //odstranime ho z aktualniho listu, co zkracujeme
				RemoveTermOutput((*it).t,num_output); //odstranime vystup termu ze vsech struktur*/
			}		
		}
		newterms.sort(PointerTermCompareHigher);
		listtmp.merge(newterms,PointerTermCompareHigher);
		if (newhigherinlist) //mame novy vetsi term
		{
			list<GTerm*>::iterator it = iter; //ulozime si to
			bool begin = false;
			while (!PointerTermCompareHigher(*iter, *it))
			{
				if (iter == listtmp.begin())
				{
					begin = true;
					break;
				}
				iter--;
			}
			
			//iter ted ukazuje na posledni z o 1 vetsich termu (ale potrebujeme az na prvni) (nebo na prvni term)
			it = iter; //opet si to ulozime
			while (!PointerTermCompareHigher(*iter, *it))
			{
				if (iter == listtmp.begin())
				{
					begin = true;
					break;
				}
				iter--;
			}
			//iter ted ukazuje na posledni z o 2 vetsich termu (nebo na prvni term)
			if (!begin) iter++;
			//ukazuje na prvni z o 1 vetsich termu, to co potrebujeme
			newhigherinlist = false;
		}
		else iter++; //zadny novy neni, pokracujem
	}
}
list<GTerm*> Graph::AddTermsRemoveHazardsWithDontCares(const int output, const bool find_essential = false)
{
	struct TermMatch //term pro upravy
	{
		GTerm *t; //ukazatel na term
		GVariable *differentvar; //rozdilna promenna oproti nadrazenemu termu, existuje-li
		list<GVariable*> ones, zeroes; //mista, kam bude treba vlozit 1 a 0, protoze je tam ma nadrizeny term
		TermMatch(GTerm *term) {t = term; differentvar = NULL;}
	};
	list<GTerm*> listtmp, listtmp2;
	list<TermMatch> otherterms; //ostatni termy
	list<GTerm*> essentialterms; // nesporne termy, pokud je ma funkce hledat
	list<string> commonminterms; // termy, co maji spolecny minterm s hlavnim termem (pouzito na nesporne termy)
	list<GVariable*> listvar;
	GTerm *t;
	char outset;

	listtmp = terms; //bereme vsechny termy
	listtmp.sort(PointerTermCompareHigher); //seradime termy od nejvetsiho
	list<GTerm*>::iterator iter = listtmp.begin();

	while (iter != listtmp.end())
	{//projdeme vsechny termy
		commonminterms.clear();
		otherterms.clear(); //procistime seznam mensich termu
		t = *iter; //vezmi term
		outset = t->GetOut(output);
		if (outset == '~') //termy bez vyznamu preskakuj
		{
			iter++;
			continue;
		}
		for (list<GTerm*>::iterator it = listtmp.begin(); it != listtmp.end(); it++)
		{
			if (*iter != *it) otherterms.push_back(TermMatch(*it));
		}

		//ted v t je nejvetsi term z nasi skupiny s vysledkem (1,-)
		//a ve smallerterms jsou vsechny mensi (a stejne velke) termy
		//vysledek je v outset
		/*
				budeme rovnou vytvaret nove termy.... aby ze dvou termu mohl vzniknout jeden novy, tak
				a) termy se nesmi kratit
				b) kde termA nema DC, tam se smi termB								110---
					  neshodovat maximalne jednou (necim jinym nez DC)	0-0-11 je v poradku
																															0-1-11 neni v poradku
				c) najdeme rovnou i takove termy, ktere maji s nasim termem spolecny minterm
		*/

		listvar = t->GetVars('1'); //promenne, kde tento term ma 1
		for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(output, outset, '-'); //termy, ktere tam maji -
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = otherterms.begin(); it2 != otherterms.end(); it2++)
				{ 
					if ((*it) == (*it2).t) //nalezeno
					{
						(*it2).ones.push_back(*variter); //tady bude jednicka, pokud se bude vytvaret novy term
						break; //done
					}
				}
			}
			listtmp2 = (*variter)->GetTerms(output, outset, '0'); //termy, ktere tam maji 0
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = otherterms.begin(); it2 != otherterms.end(); it2++)
				{ 
					if ((*it) == (*it2).t) //nalezeno
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							(*it2).differentvar = *variter; //zaznamename jej
							break; //done
						}
						else //vice rozdilu, je na case jej smazat
						{
							otherterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}

		listvar = t->GetVars('0'); //promenne, kde tento term ma 0
				for (list<GVariable*>::iterator variter = listvar.begin(); variter != listvar.end(); variter++)
		{ //prochazime vsechny tyto variable
			listtmp2 = (*variter)->GetTerms(output, outset, '-'); //termy, ktere tam maji -
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = otherterms.begin(); it2 != otherterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno
					{
						(*it2).zeroes.push_back(*variter); //tady bude nula, jestli se bude vytvaret novy term
						break; //done
					}
				}
			}
			listtmp2 = (*variter)->GetTerms(output, outset, '1'); //termy, ktere tam maji 1
			for (list<GTerm*>::iterator it = listtmp2.begin(); it!=listtmp2.end(); it++)
			{ //projdeme je
				for (list<TermMatch>::iterator it2 = otherterms.begin(); it2 != otherterms.end(); it2++)
				{ //tenhle jeste mame v nasem listu jako pouzitelnej
					if ((*it) == (*it2).t) //nalezeno
					{
						if ((*it2).differentvar == NULL) //prvni rozdil
						{
							(*it2).differentvar = *variter; //zaznamename jej
							break; //done
						}
						else //vice rozdilu, je na case jej smazat
						{
							otherterms.erase(it2); //odstran ze seznamu kandidatu pro minimalizaci
							break; // done
						}
					}
				}
			}
		}

		//hotovo, ted projdeme vsechny mensi termy, ktere jsme jeste nevyradili
		//v t je nejvetsi term z nasi skupiny s vysledkem (1,-)
		//a ve smallerterms jsou vsechny mensi (a stejne velke) termy se stejnym vysledkem, ktere
		/*
				a) vsude, kde vetsi term nema DC, ma mensi term DC nebo shodu, jinak se shoduji - nic se nedeje, ale vyuzijeme tento term pro zjisteni, zda hlavni term je nesporny!
				b) vsude, kde vetsi term nema DC, ma mensi term DC nebo shodu a navic se lisi v jedne pozici - lze vytvorit term, ktery bude pokryvat spolecne stavy

			tzn.
			a) maji zeroes nebo ones, ale zadnou differentvar, zjisti nespornost
			b) maji zeroes nebo ones a jednu differentvar, vytvorime novy term
		*/
		
		string str1, str2;
		list<GTerm*> newterms;
		for (list<TermMatch>::iterator it = otherterms.begin(); it != otherterms.end(); it++)
		{
			if ((!(*it).ones.empty())||(!(*it).zeroes.empty()))
			{
				if ((*it).differentvar != NULL)
				//kde vetsi term nema -, tam ten mensi ma nekde -, ale muze jit vytvorit novy term
				{ //krome tech - maji prave jednu neshodu, vytvorime novy term (uplne novy)
					//v differentvar bude -
					//v ostatnich bude to, co tam ma mensi term
					//jen na nekterych dalsich pozicich budou 0 a 1 podle toho, kde je mel vetsi term
					//nove vytvoreny term nebude nikdy vetsi nez ten vyssi z dvojice

					str1 = ((*it).t)->GetIn(); //puvodni vstupy termu

					str1[(*it).differentvar->GetNum()] = '-'; //promenna ve ktere se termy lisi zmen vstup na -

					for (list<GVariable*>::iterator iii = (*it).ones.begin(); iii != (*it).ones.end(); iii++)
						str1[(*iii)->GetNum()] = '1'; //pridej jednicky
					for (list<GVariable*>::iterator iii = (*it).zeroes.begin(); iii != (*it).zeroes.end(); iii++)
						str1[(*iii)->GetNum()] = '0'; //pridej nuly

					GTerm* retterm = AddTermOutput(str1, output, (*it).t->GetOut(output));
					if (retterm != NULL) 
					{
						commonminterms.push_back(str1);
						newterms.push_back(retterm);//pridame novy term do seznamu	
					}
				}
				else //differentvar == NULL, takze maji spolecny nejaky minterm
				{
					commonminterms.push_back((*it).t->GetIn());
				}
			}
		}
		newterms.sort(PointerTermCompareHigher);
		listtmp.merge(newterms,PointerTermCompareHigher);

		//ted zjistime, jestli hlavni term v *iter je nesporny...
		if ((find_essential) && (!commonminterms.empty()))
		{			
			if ((*iter)->GetCount_dc()>0) 
			{
				string str = (*iter)->GetIn();
				string *newstrs;
				newstrs = new string [commonminterms.size()];
				for (int i=0;i<count_inputs;i++) 
				{
					if (str[i]=='-')
					{
						int counter = 0;
						for (list<string>::iterator it = commonminterms.begin(); it!= commonminterms.end(); it++)
						{
							newstrs[counter] += (*it)[i];
							counter++;
						}
					}
				}
				for (unsigned int i=0;i<commonminterms.size();i++) 
				{
					newstrs[i] += " 1";
				}

				list<string> pla;

				pla.push_back(".i " + To_String((*iter)->count_dc));
				pla.push_back(".o 1");
				pla.push_back(".p " + To_String(commonminterms.size()));
				pla.push_back(".type f");

				for (unsigned int i = 0; i < commonminterms.size(); i++) 
					pla.push_back(newstrs[i]);
				pla.push_back(".e");

				Graph *g = new Graph();
				g->ConstructFromPLALines(pla);
				if (g->BranchAndBoundTautology(0)!="tautology") essentialterms.push_back(*iter);

				delete g;
				delete [] newstrs;
			}
		}
		iter++;
	}
	return essentialterms;
}


//
// main algoritmy
//
string Graph::BruteForceTautology(int output) const
{
	if ((output<0)||(output>count_outputs-1)) throw "wrong number of output";
	string max = "", str="";
	for (int i=0;i<count_inputs;i++) 
	{
		str += "0";
		max += "1";
	}
	list<GTerm*>::iterator iter;
	bool satisfied; //inicializace

	while (str!=max) //prochazime vsechny variace vstupu
	{
		satisfied = false; //neslneno
		for (iter = outputs[output].terms_on.begin(); iter != outputs[output].terms_on.end(); iter++)
		{ //prochazi vsechny termy, co maji z hlediska tohoto vystupu vysledek 1
			satisfied = (*iter)->Satisfy(str);
 			if (satisfied) break;
		}
		if (!satisfied) return str; //jestli zadny nesplnil vstup, vrat vstup
		IncStr(str); //nektery to splnil, zvys o 1
	}
	return "tautology"; //vsechny variace splneny, vrat tautologii
}

string Graph::BranchAndBoundTautology(int output) const
{
	if ((output<0)||(output>count_outputs-1)) throw "wrong number of output";

	//pokud ma funkce nejake offtermy nebo dctermy, nemuze byt o tautologii vubec rec: 
	if (outputs[output].terms_off.size()>0) return (*outputs[output].terms_off.begin())->GetIn();
	if (outputs[output].terms_dc.size()>0) return (*outputs[output].terms_dc.begin())->GetIn();
		
	struct StackElem //prvek na stavovem zasobniku
	{
		GTerm* predecessor; //termu, ktery tento stav nastavoval
		int numvar; //cislo promenne, kterou nastavoval
		list<GTerm*> devalued; //seznam termu, ktere svym rozhodnutim vyradil ze hry (znehodnotil)
	};

	list<GTerm*> valuable; //seznam termu, ktere stale jeste maji vysledek 1 i pres vsechna nase omezeni
	string valuation = ""; //stavova promenna pro aktualni ohodnoceni vsech promennych 
	for (int i=0;i<count_inputs;i++) valuation += '-'; //inicializace
	
	stack<StackElem> st; //zasobnik stavu
	StackElem tmp; //pomocna promenna pro zasobnik
	list<GTerm*> listtmp; //pomocna promenna pro seznam termu
	list<GTerm*>::iterator iter, iter2; //pomocne promenne pro iteraci termy

	for (list<GTerm*>::iterator iter=outputs[output].terms_on.begin();iter != outputs[output].terms_on.end();iter++)
			valuable.push_back(*iter); //do listtmp ukladame vsechny termy

	valuable.sort(PointerTermCompareHigher); //seradi termy podle jejich poctu DC (ty co maji DC nejvetsi jako prvni)	
	/*
		v ramci urychleni vypoctu rozdelime graf (respektive pouze jeho vrcholy-termy) 
		na souvisle podgrafy
			a) tzn pokud cely graf je souvisly, zustane nezmenen
			b)pokud neni souvisly, rozdelime jej na N grafu, ktere budou vsechny souvisle
				pro splneni tautologie pak staci, kdyz kterakoliv souvisla cast je tautologie :-)
	*/

	//to zpusobi, ze jsou vrcholy v grafu serazeny podle stupne (s nejvetsim stupnem jsou prvni) (deg[a]>deg[a+1])

	//bool 
/*	while (!listtmp.empty()) //dokud neni list termu prazdny
	{
		GTerm *termtmp;
		list <GVariable*> varslist;
		varslist.clear(); //clear
		termtmp = *listtmp.begin(); //uchopime prvni term
		listtmp.pop_front(); //odstranime ho z listu
		newlist.push_back(termtmp); //a zaradime ho do noveho listu

		varslist = termtmp->GetVars('1'); //bereme vsechny ONsetove sousedy
		varslist.splice(varslist.end(),termtmp->GetVars('0')); //priradime k nim OFFsetove sousedy
		
		for (list<GVariable*>::iterator it = varslist.begin();it != varslist.end();it++)
		{ //projdi vsechny promenne, co maji s nasim uchopenym termem neco spolecneho
			(*it)->GetTerms('1');
			//for (iter = //najdi je v termech, co tam uz mame
		}
//
	}*/

	while (1) //globalni loop
	{
		bool greedy_end = false; //ukonci hladovou cast algoritmu = false
		while (!greedy_end) //prirazuj hodnoty promennym, dokud muzes (hladovy alg)
		{
			greedy_end = true;
			if (valuable.empty()) return valuation; //zadny term uz nesplnuje nastaveni, neni to tautologie
			else //nejaky jeste splnuje
			{
				GTerm* t = *valuable.begin(); //prvni z nich
				string myvariables = t->GetIn(); //jeho promenne
				for (int i=0;i<count_inputs;i++) //vsechny projdi
				{
					if ((myvariables[i]!='-') && (valuation[i]=='-')) // najdi takovou, na ktere mu zalezi a ktera jeste nebyla nastavena
					{
						tmp.devalued.clear();
						tmp.numvar = i; //uloz zaznam o tom, kterou promennou nyni nastavujeme
						valuation[i] = myvariables[i] == '1' ? '0' : '1'; //nastav ohodnoceni na opacnou polaritu, aby doslo k nesplneni aktualniho termu
						tmp.predecessor = t; //uloz zaznam o tom, ktery term to udelal
						valuable.remove(t);
						
						// najdi termy, ktere toto rozhodnuti vyradi ze hry
						listtmp = variables[i]->GetTerms(output, '1', myvariables[i]); //termy, ktere maji stejnou polaritu u promenne i jako tento term
						for (iter = listtmp.begin(); iter != listtmp.end(); iter++) //vsechny je projdi
						{
							for (iter2 = valuable.begin(); iter2 != valuable.end(); iter2++) //projdi vsechny valuable
							{
								if (*iter == *iter2) //valuable jeste obsahuje tento term
								{
									tmp.devalued.push_back(*iter); //zarad jej do seznamu znehodnocenych pro tento stav
									valuable.remove(*iter); //vyrad je ze seznamu hodnotnych termu
									break;
								}
							}
						} //vsechny termy, co mely byt vyrazeny, jsou vyrazeny
						st.push(tmp); //takto nove definovany stav dej na zasobnik
						greedy_end = false; //je treba provest navrat, tzn opustit vnitrni while(1)
						break; //a znovu zacni prirazovat hodnoty dalsim termum
					} //na teto promenne zrovna nezalezi, jdeme na dalsi
				} //prosli jsme vsechny promenne a na zadne z nich uz nezalezi, tento term to vzdy splnuje
				continue; 
			}
		} //konec vnitrniho while(1)
		
		//pokracovani vnejsi while(1) - backtracking
		bool backtracking_end = false;
		while (!backtracking_end) //backtracking
		{
			//vyjmi stav ze zasobniku
			if (st.empty()) return "tautology"; //zasobnik je uz prazdny, neni kam se vracet? tautologie!
			tmp = st.top(); 
			st.pop(); 

			//proved navrat		
			for (iter=tmp.devalued.begin();iter!=tmp.devalued.end();iter++)
				valuable.push_back(*iter); //vracime zpet znehodnocene termy
			if (tmp.numvar!=-1) valuation[tmp.numvar] = '-'; //vracime zaznam v celkovem hodnoceni
			valuable.push_back(tmp.predecessor);
			//valuable.push_back(tmp.
			tmp.devalued.clear();

			//najdi dalsi novy stav - zmen novou promennou
			string myvariables = tmp.predecessor->GetIn();
			for (int i = tmp.numvar+1; i < count_inputs; i++) //prochazime promenne, ktere jsme jeste nezkouseli
			{
				if ((myvariables[i]!='-')&&(valuation[i]=='-')) // najdi takovou, na ktere mu zalezi a ktera jeste nebyla nastavena
				{
					tmp.numvar = i; //uloz zaznam o tom, kterou promennou nyni nastavujeme
					valuation[i] = myvariables[i]=='1' ? '0' : '1'; //nastav ohodnoceni na opacnou polaritu, aby doslo k nesplneni aktualniho termu
					//uloz zaznam o tom, ktery term to udelal // tmp.predecessor zustava na puvodnim, nemusime jej nastavovat
											
					// najdi termy, ktere toto rozhodnuti vyradi ze hry
					listtmp = variables[i]->GetTerms(output, '1', myvariables[i]);
					for (iter = listtmp.begin(); iter != listtmp.end(); iter++) //vsechny je projdi
					{
						for (iter2 = valuable.begin(); iter2 != valuable.end(); iter2++) //projdi vsechny valuable
						{
							if (*iter == *iter2) //valuable jeste obsahuje tento term
							{
								tmp.devalued.push_back(*iter); //zarad je do seznamu znehodnocenych pro tento stav
								valuable.remove(*iter); //vyrad je ze seznamu hodnotnych termu
								break;
							}
						}
					} //vsechny termy, co mely byt vyrazeny, jsou vyrazeny
					st.push(tmp); //takto nove definovany stav dej na zasobnik
					backtracking_end = true;					
					break; //a znovu zacni prirazovat hodnoty dalsim termum (hladovym alg.)
				} //na teto promenne zrovna nezalezi, jdeme na dalsi
			} //prosli jsme vsechny promenne a na zadne z nich uz nezalezi, tento term to vzdy splnuje
			continue; //pokracujem v backtrackingu
		}
	}
}

list<string> Graph::Complement(int output)
{
	if ((output<0)||(output>count_outputs-1)) throw "wrong number of output";
	if (type == fr) 
	{
		throw "Minimization works only on types F, FD and FDR.";
		return list<string>::list();
	}

	struct StackElem //prvek na stavovem zasobniku
	{
		GTerm* predecessor; //termu, ktery tento stav nastavoval
		int numvar; //cislo promenne, kterou nastavoval
		list<GTerm*> devalued; //seznam termu, ktere svym rozhodnutim vyradil ze hry (znehodnotil)
	};

	list<GTerm*> valuable; //seznam termu, ktere stale jeste maji vysledek 1 i pres vsechna nase omezeni
	string valuation = ""; //stavova promenna pro aktualni ohodnoceni vsech promennych 
	for (int i=0;i<count_inputs;i++) valuation += '-'; //inicializace
	
	stack<StackElem> st; //zasobnik stavu
	StackElem tmp; //pomocna promenna pro zasobnik
	list<GTerm*> listtmp; //pomocna promenna pro seznam termu
	list<GTerm*>::iterator iter, iter2; //pomocne promenne pro iteraci termy

	for (list<GTerm*>::iterator iter=outputs[output].terms_on.begin();iter != outputs[output].terms_on.end();iter++)
			valuable.push_back(*iter); //do listtmp ukladame vsechny onset termy
	for (list<GTerm*>::iterator iter = outputs[output].terms_dc.begin(); iter != outputs[output].terms_dc.end(); iter++)
		valuable.push_back(*iter); //ulozime tam i DCtermy

	valuable.sort(PointerTermCompareLower); //seradi termy podle jejich poctu DC (ty co maji DC nejmensi jako prvni)	
	valuable.reverse();

	list<string> complement;
	while (1) //globalni loop
	{
		bool greedy_end = false; //ukonci hladovou cast algoritmu = false
		while (!greedy_end) //prirazuj hodnoty promennym, dokud muzes (hladovy alg)
		{
			greedy_end = true;
			if (valuable.empty())
			{
				complement.push_back(valuation);
//				return valuation; //zadny term uz nesplnuje nastaveni, neni to tautologie
			}
			else //nejaky jeste splnuje
			{
				GTerm* t = *valuable.begin(); //prvni z nich
				string myvariables = t->GetIn(); //jeho promenne
				for (int i=0;i<count_inputs;i++) //vsechny projdi
				{
					if ((myvariables[i]!='-') && (valuation[i]=='-')) // najdi takovou, na ktere mu zalezi a ktera jeste nebyla nastavena
					{
						tmp.devalued.clear();
						tmp.numvar = i; //uloz zaznam o tom, kterou promennou nyni nastavujeme
						valuation[i] = myvariables[i] == '1' ? '0' : '1'; //nastav ohodnoceni na opacnou polaritu, aby doslo k nesplneni aktualniho termu
						tmp.predecessor = t; //uloz zaznam o tom, ktery term to udelal
						valuable.remove(t);
						
						// najdi termy, ktere toto rozhodnuti vyradi ze hry
						listtmp = variables[i]->GetTerms(output, '1', myvariables[i]); //termy, ktere maji stejnou polaritu u promenne i jako tento term
						for (iter = listtmp.begin(); iter != listtmp.end(); iter++) //vsechny je projdi
						{
							for (iter2 = valuable.begin(); iter2 != valuable.end(); iter2++) //projdi vsechny valuable
							{
								if (*iter == *iter2) //valuable jeste obsahuje tento term
								{
									tmp.devalued.push_back(*iter); //zarad jej do seznamu znehodnocenych pro tento stav
									valuable.remove(*iter); //vyrad je ze seznamu hodnotnych termu
									break;
								}
							}
						} //vsechny termy, co mely byt vyrazeny, jsou vyrazeny
						st.push(tmp); //takto nove definovany stav dej na zasobnik
						greedy_end = false; //je treba provest navrat, tzn opustit vnitrni while(1)
						break; //a znovu zacni prirazovat hodnoty dalsim termum
					} //na teto promenne zrovna nezalezi, jdeme na dalsi
				} //prosli jsme vsechny promenne a na zadne z nich uz nezalezi, tento term to vzdy splnuje
				continue; 
			}
		} //konec vnitrniho while(1)
		
		//pokracovani vnejsi while(1) - backtracking
		bool backtracking_end = false;
		while (!backtracking_end) //backtracking
		{
			//vyjmi stav ze zasobniku
			if (st.empty()) 
			{
				return complement;
			}
			tmp = st.top(); 
			st.pop(); 

			//proved navrat		
			for (iter=tmp.devalued.begin();iter!=tmp.devalued.end();iter++)
				valuable.push_back(*iter); //vracime zpet znehodnocene termy
			if (tmp.numvar!=-1) valuation[tmp.numvar] = '-'; //vracime zaznam v celkovem hodnoceni
			valuable.push_back(tmp.predecessor);
			tmp.devalued.clear();

			//najdi dalsi novy stav - zmen novou promennou
			string myvariables = tmp.predecessor->GetIn();
			for (int i = tmp.numvar+1; i < count_inputs; i++) //prochazime promenne, ktere jsme jeste nezkouseli
			{
				if ((myvariables[i]!='-')&&(valuation[i]=='-')) // najdi takovou, na ktere mu zalezi a ktera jeste nebyla nastavena
				{
					tmp.numvar = i; //uloz zaznam o tom, kterou promennou nyni nastavujeme
					valuation[i] = myvariables[i]=='1' ? '0' : '1'; //nastav ohodnoceni na opacnou polaritu, aby doslo k nesplneni aktualniho termu
					//uloz zaznam o tom, ktery term to udelal // tmp.predecessor zustava na puvodnim, nemusime jej nastavovat
											
					// najdi termy, ktere toto rozhodnuti vyradi ze hry
					listtmp = variables[i]->GetTerms(output, '1', myvariables[i]);
					for (iter = listtmp.begin(); iter != listtmp.end(); iter++) //vsechny je projdi
					{
						for (iter2 = valuable.begin(); iter2 != valuable.end(); iter2++) //projdi vsechny valuable
						{
							if (*iter == *iter2) //valuable jeste obsahuje tento term
							{
								tmp.devalued.push_back(*iter); //zarad je do seznamu znehodnocenych pro tento stav
								valuable.remove(*iter); //vyrad je ze seznamu hodnotnych termu
								break;
							}
						}
					} //vsechny termy, co mely byt vyrazeny, jsou vyrazeny
					st.push(tmp); //takto nove definovany stav dej na zasobnik
					backtracking_end = true;					
					break; //a znovu zacni prirazovat hodnoty dalsim termum (hladovym alg.)
				} //na teto promenne zrovna nezalezi, jdeme na dalsi
			} //prosli jsme vsechny promenne a na zadne z nich uz nezalezi, tento term to vzdy splnuje
			continue; //pokracujem v backtrackingu
		}
	}

}
void Graph::Minimization(const int num_output, const bool deep)
{
	SimplificationWithDontCares(num_output);
	list<GTerm*> essentials;
	if (deep)
	{
		essentials = AddTermsRemoveHazardsWithDontCares(num_output, true);
		SimplificationWithDontCares(num_output, essentials);
	}

	//ted odstranime dontcares, ktere jsou navic a nevyuzite
	list<GTerm*>::iterator iter = outputs[num_output].terms_dc.begin(); 
	while (iter != outputs[num_output].terms_dc.end())
	{
		essentials.remove(*iter);
		RemoveTermOutput(*iter, num_output);
		iter = outputs[num_output].terms_dc.begin();
	}

	//pokud je deep == true, tak plati, ze: 
	//v tuto chvili je zachycen kazdy ONset pøímými implikanty, jiné implikanty neexistují
	//ale ne všechny pøímé implikanty jsou nesporné, nesporne jsou v essentials

	/*
		nesporne implikanty presuneme pryc a ve zbyvajicich hledame nove nesporne implikanty
		zaradime je do mnoziny nespornych a opet overime, jestli nemuzeme nektery ze zbyvajicich odstranit
		opet je presuneme pryc a hledame nove nesporne implikanty
		toto opakujeme, dokud se dari nachazet nesporne implikanty
		kdyz jej po pruchodu nenalezneme, odstranime nejmensi term a pokracujem v hledani
		
	*/

	list<GTerm*> nonessentials;
	nonessentials = outputs[num_output].terms_on;
	for (list<GTerm*>::iterator it = essentials.begin(); it != essentials.end(); it++)
		nonessentials.remove(*it);

	list<GVariable*> listvars;
	list<GTerm*> new_ess;

	bool deletesmallest;
	do
	{
		while (!new_ess.empty())
		{
			//zjisti, zda dany term uz neni nadbytecny
			GTerm *t = *new_ess.begin();
			list<GTerm*> tmp_ess = essentials;

			listvars = t->GetVars('1');//promenne, kde ma term 1
			for (list<GVariable*>::iterator iter = listvars.begin(); iter != listvars.end(); iter++)
			{
				for (list<GTerm*>::iterator ittt = (*iter)->outputs[num_output].onset.term_off.begin(); 
					ittt != (*iter)->outputs[num_output].onset.term_off.end(); ittt++)
				{
					tmp_ess.remove(*ittt);
				}
			}	

			listvars = t->GetVars('0');//promenne, kde ma 0
			for (list<GVariable*>::iterator iter = listvars.begin(); iter != listvars.end(); iter++)
			{
				for (list<GTerm*>::iterator ittt = (*iter)->outputs[num_output].onset.term_on.begin(); 
					ittt != (*iter)->outputs[num_output].onset.term_on.end(); ittt++)
				{
					tmp_ess.remove(*ittt);
				}
			}

			//ted budeme hledat tautologii
			if (!tmp_ess.empty())
			{
				if (t->GetCount_dc()>0) //pokud nema zadne dc, je jasne, ze ho ostatni pokryvaji a je to tautologie
				{
					string str = t->GetIn();
					string *newstrs_ess;
					newstrs_ess = new string[tmp_ess.size()];


					listvars = t->GetVars('-');
					for (list<GVariable*>::iterator iter = listvars.begin(); iter != listvars.end(); iter++)
					{
						int num = (*iter)->number;
						int counter = 0;
						for (list<GTerm*>::iterator ittt = tmp_ess.begin(); ittt!= tmp_ess.end(); ittt++)
						{
							newstrs_ess[counter] += (*ittt)->GetIn(num);
							counter++;
						}
					}
					for (unsigned int i=0;i<tmp_ess.size();i++) 
					{
						newstrs_ess[i] += " 1";
					}

					list<string> pla;

					pla.push_back(".i " + To_String(t->count_dc));
					pla.push_back(".o 1");
					pla.push_back(".p " + To_String(tmp_ess.size()));
					pla.push_back(".type f");

					for (unsigned int i = 0; i < tmp_ess.size(); i++) 
						pla.push_back(newstrs_ess[i]);
					pla.push_back(".e");

					Graph *g = new Graph();
					g->ConstructFromPLALines(pla);
					if (g->BranchAndBoundTautology(0)=="tautology") //nas term uz je redundantni
					{
						nonessentials.remove(t);
						new_ess.remove(t);
						RemoveTermOutput(t, num_output);
						delete g; 
						delete [] newstrs_ess;
						continue;
					}
					delete g; 
					delete [] newstrs_ess;
				}
				else
				{
					nonessentials.remove(t);
					new_ess.remove(t);
					RemoveTermOutput(t, num_output);
					continue;
				}
			}
			essentials.push_back(t);
			nonessentials.remove(t);
			new_ess.remove(t);
		}


		new_ess.clear();
		deletesmallest = true;
		//najdi redundance
		list<GTerm*>::iterator it = nonessentials.begin();
		while (it != nonessentials.end())
		{
			list<GTerm*> tmp_non = nonessentials;
			tmp_non.remove(*it); //odstran sam sebe
			
			listvars = (*it)->GetVars('1');//promenne, kde ma term 1
			for (list<GVariable*>::iterator iter = listvars.begin(); iter != listvars.end(); iter++)
			{
				for (list<GTerm*>::iterator ittt = (*iter)->outputs[num_output].onset.term_off.begin(); 
					ittt != (*iter)->outputs[num_output].onset.term_off.end(); ittt++)
				{
					tmp_non.remove(*ittt);
				}
			}

			listvars = (*it)->GetVars('0');//promenne, kde ma 0
			for (list<GVariable*>::iterator iter = listvars.begin(); iter != listvars.end(); iter++)
			{
				for (list<GTerm*>::iterator ittt = (*iter)->outputs[num_output].onset.term_on.begin(); 
					ittt != (*iter)->outputs[num_output].onset.term_on.end(); ittt++)
				{
					tmp_non.remove(*ittt);
				}
			}

			//ted jsou v tmp_non ty, co by ho mohli definovat
			if (tmp_non.empty())
			{ //je treba jej pridat do essentials
				new_ess.push_back(*it);
				deletesmallest = false;
				it++;
				continue;
			}

			//ted budeme hledat ve zbytcich tautologie
			if (!tmp_non.empty())
			{
				if ((*it)->GetCount_dc()>0) //pokud nema zadne dc, je jasne, ze ho ostatni pokryvaji a je to tautologie
				{
					string str = (*it)->GetIn();
					string *newstrs_non;
					newstrs_non = new string[tmp_non.size()];

					listvars = (*it)->GetVars('-');
					for (list<GVariable*>::iterator iter = listvars.begin(); iter != listvars.end(); iter++)
					{
						int num = (*iter)->number;
						int counter = 0;
						for (list<GTerm*>::iterator ittt = tmp_non.begin(); ittt != tmp_non.end(); ittt++)
						{
							newstrs_non[counter] += (*ittt)->GetIn(num);
							counter++;
						}
					}
					for (unsigned int i = 0; i < tmp_non.size(); i++)
						newstrs_non[i] += " 1";

					list<string> pla;

					pla.clear();

					pla.push_back(".i " + To_String((*it)->count_dc));
					pla.push_back(".o 1");
					pla.push_back(".p " + To_String(tmp_non.size()));
					pla.push_back(".type f");

					for (unsigned int i = 0; i < tmp_non.size(); i++) 
						pla.push_back(newstrs_non[i]);
					pla.push_back(".e");

					Graph *h = new Graph();
					h->ConstructFromPLALines(pla);

					if (h->BranchAndBoundTautology(0)!="tautology") //nas term uz je nesporny
					{
						new_ess.push_back(*it);
						deletesmallest = false;
					}
					delete h;
					delete [] newstrs_non;
				}
			}
			it++;
		}

		//zadny novy nesporny implikant, smaz nejmensi ze zbyvajicich implikantu
		if (deletesmallest && !nonessentials.empty()) 
		{
			nonessentials.sort(PointerTermCompareLower);
			GTerm* t = (*nonessentials.begin());
			nonessentials.erase(nonessentials.begin()); 
			RemoveTermOutput(t, num_output);
		}
	} while (nonessentials.size()>1);
}


void Graph::Orthogonalization(const int num_output, const bool deep)
{
	SimplificationWithDontCares(num_output);
	list<GTerm*> essentials;
	if (deep)
	{
		essentials = AddTermsRemoveHazardsWithDontCares(num_output, true);
		SimplificationWithDontCares(num_output);
	}

	//ted odstranime dontcares, ktere jsou navic a nevyuzite
	list<GTerm*>::iterator iter = outputs[num_output].terms_dc.begin(); 
	while (iter != outputs[num_output].terms_dc.end())
	{
		essentials.remove(*iter);
		RemoveTermOutput(*iter, num_output);
		iter = outputs[num_output].terms_dc.begin();
	}

	//pokud je exact == true, tak plati, ze: 
	//v tuto chvili je zachycen kazdy ONset pøímými implikanty, jiné implikanty neexistují
	//ale ne všechny pøímé implikanty jsou nesporné, nesporne jsou v essentials

	/*
		nejprve overime, jestli nesporne implikanty neobsahuji nejaky jiny implikant, ktery by byl rendundantni... takove odstranime
		pak nesporne implikanty presuneme pryc a ve zbyvajicich hledame nove nesporne implikanty
		zaradime je do mnoziny nespornych a opet overime, jestli nemuzeme nektery ze zbyvajicich odstranit
		opet je presuneme pryc a hledame nove nesporne implikanty
		toto opakujeme, dokud se dari nachazet nesporne implikanty
		kdyz jej po pruchodu nenalezneme, odstranime nejmensi term a pokracujem v hledani
		
		vylepseni - hledej redundantni a nesporne v ramci jednoho cyklu
	*/

	list<GTerm*> nonessentials;
	nonessentials = outputs[num_output].terms_on;
	for (list<GTerm*>::iterator it = essentials.begin(); it != essentials.end(); it++)
		nonessentials.remove(*it);

	//seradime obe rady termu
	essentials.sort(PointerTermCompareHigher);
	nonessentials.sort(PointerTermCompareHigher);

	//udelame si frontu termu, ktere tam budeme vkladat... nesporne napred, pak ostatni
	nonessentials.splice(nonessentials.begin(), essentials);


	list<GTerm*> conflictterms; 
	list<GVariable*> listvars;
	while (!nonessentials.empty())
	{
		GTerm *t = *nonessentials.begin();
		nonessentials.pop_front();
		//zjisti, zda uz neni v essentials neco konfliktniho
		conflictterms = essentials;
		listvars = t->GetVars('1');
		for (list<GVariable*>::iterator iter = listvars.begin(); iter != listvars.end(); iter++)
		{
			for (list<GTerm*>::iterator ittt = (*iter)->outputs[num_output].onset.term_off.begin();
				ittt != (*iter)->outputs[num_output].onset.term_off.end(); ittt++)
			{
				conflictterms.remove(*ittt);
			}
		}

		listvars = t->GetVars('0');
		for (list<GVariable*>::iterator iter = listvars.begin(); iter != listvars.end(); iter++)
		{
			for (list<GTerm*>::iterator ittt = (*iter)->outputs[num_output].onset.term_on.begin(); 
				ittt != (*iter)->outputs[num_output].onset.term_on.end(); ittt++)
			{
				conflictterms.remove(*ittt);
			}
		}

		//ted jsou v conflictterms takove termy, ktere uz jsou ve vysledne skupine a 
		///zaroven maji nejaky spolecny minterm s nasim termem
		if (conflictterms.empty())
		{
			essentials.push_back(t);
			continue;
		}
		else //jsou konfliktni, budeme rozkladat a tvorit nove termy
		{
			/*
				vytvorime novy prostor z dontcare naseho termu a naskladame do nej ty termy, 
				ktere jsou s nim konfliktni... pak nechame na tomto malem prostoru probehnout
				algoritmus pro zjisteni komplementu a tento komplement je tim, co chceme
				nove vlozit do essentials
			*/
			string *cutterms = new string[conflictterms.size()];
			listvars = t->GetVars('-');
			for (list<GVariable*>::iterator iter = listvars.begin(); iter != listvars.end(); iter++)
			{
				int num = (*iter)->number; 
				int counter = 0;
				for (list<GTerm*>::iterator ittt = conflictterms.begin(); 
					ittt != conflictterms.end(); ittt++)
				{
					cutterms[counter] += (*ittt)->GetIn(num);
					counter++;
				}
			}
			for (unsigned int i = 0; i < conflictterms.size(); i++)
				cutterms[i] += " 1";

			list<string> pla;
			pla.push_back(".i " + To_String(t->count_dc));
			pla.push_back(".o 1");
			pla.push_back(".p " + To_String(conflictterms.size()));
			pla.push_back(".type f");

			for (unsigned int i = 0; i < conflictterms.size(); i++) 
				pla.push_back(cutterms[i]);
			pla.push_back(".e");

			Graph *g = new Graph(); 
			g->ConstructFromPLALines(pla);
			Graph *h = g->Complement();
			delete g;
			delete [] cutterms;
			list<string> newcutterms = h->GenerateMatrix();

			string str = t->GetIn();
			list<string> newterms;
			while (!newcutterms.empty())
			{
				string s = newcutterms.front();
				newcutterms.pop_front(); 
				string st = str;
				int counter = 0;
				for (list<GVariable*>::iterator iter = listvars.begin(); iter != listvars.end(); iter++)
				{
					int num = (*iter)->number;
					st[num] = s[counter];
					counter++;
				}
				newterms.push_back(st);
			}

			string out = "";
			for (int j = 0; j < count_outputs; j++) out += "~";
			out[num_output] = '1';			
			for (list<string>::iterator iter = newterms.begin(); iter != newterms.end(); iter++)
			{
				GTerm* retterm = ConstructFromPLALine(*iter, out);
				essentials.push_back(retterm);
			}
			RemoveTermOutput(t, num_output);
		}			
	}
}


// 
// public
//
void Graph::ConstructFromPLALines(std::list<string> &buffer)
{
	if (count_terms != -1) throw "graph reconstruction is not allowed!";
	bool prvni_term = true; //pomocna promenna pro rozpoznani prvniho radku s termy
	int inputs, outputs; //povinne parametry
	inputs = outputs = -1; //pocet vstupu, vystupu a termu
	graphtype type = undefined; //dulezity parametr pro parsovani
	string input_names = "";
	string output_names = "";

	string str, tmp;
	int line = 0;
	while (!buffer.empty())
	{
		line++;
		tmp = *buffer.begin();
		buffer.pop_front();
		Trim(tmp);
		if (tmp=="") continue;
		switch (tmp[0])
		{
		case '#': //obycejny komentar, ignore cely radek
			break;
		case '.':  //definice nejakeho parametru, parsujeme
			str = Separation(tmp);
			if (str==".ilb") input_names = tmp;
			if (str==".ob") output_names = tmp;
			if (str==".i")
			{				
				str = Separation(tmp);
				int pocet = atoi(str.c_str());
				if (pocet>0) 
				{
//					cout << "INPUTS: ";
//					cout << str << endl;
					inputs = pocet;
				}
				else
				{
					string s;
					s = "Parser Error: Number of input variables is not set correctly.\n";
					s += "Line Number: " + line;
					s += "\n";
					throw s;
				}
			}
			
			if (str==".o")
			{
				str = Separation(tmp);
				int pocet = atoi(str.c_str());
				if (pocet>0) 
				{
//					cout << "OUTPUTS: ";
//					cout << str << endl;
					outputs = pocet;
				}
				else
				{
					string s;
					s = "Parser Error: Number of output variables is not set correctly.\n";
					s += "Line Number: " + line;
					s += "\n";
					throw s;
				}
			}

/*			if (str==".p")
			{
				str = Separation(tmp);
				int pocet = atoi(str.c_str());
				if (pocet>0) 
				{
					cout << "TERMS: ";
					cout << str << endl;
					p = pocet;
				}
				else
				{
					cout << "Parser Error: Number of product terms is not set correctly." << endl;
					cout << "Line Number: " << i << endl;
					return false;
				}				
			}*/

			if (str==".type")
			{
				str = Separation(tmp);
				if (str=="f") type = f;
				else if (str=="fd") type = fd;
				else if (str=="fr") type = fr;
				else if (str=="fdr") type = fdr;
				else
				{
					throw "Parser Error: unknown type, this program supports f, fd, fr and fdr only!";
				}
//				cout << "TYPE: ";
//				cout << str << endl;
			}

			continue; //je to parametr, ktery nas nezajima	
		case '1': case '0': case '-': case '~': case '2': case '3': case '4': 
			//nalezen nejaky term, parsujeme
			if (prvni_term)
			{
				if (inputs==-1)
				{
					throw "Parser Error: mandatory field 'number of input variables' is missing";
				}
				if (outputs==-1)
				{
					throw "Parser Error: mandatory field 'number of output variables' is missing";
				}
				if (type==undefined)
				{
//					cout << "TYPE: NOT DEFINED (using default fd)" << endl;
					type = fd;
				}
				SetParams(type, inputs,outputs,input_names,output_names);
				prvni_term = false;
			}
			
			{
				str = Separation(tmp);
				if (str.length()!=inputs)
				{
					string s;
					s = "Parser Error: Incorrect number of inputs in PLA file.\n";
					s += "Line Number: " + line;
					s += "\n";
					throw s;
				}

				string str2 = Separation(tmp);
				if (str2.length()!=outputs)
				{
					string s;
					s = "Parser Error: Incorrect number of outputs PLA file.\n";
					s += "Line Number: " + line;
					s += "\n";
					throw s;
				}

				for (unsigned int q = 0;q<str.length();q++)
				{
					switch (str[q])
					{
					case '~': 
					case '3':
					case '2':
						str[q] = '-';
						break;
					case '4':
						str[q] = '1';
						break;
					}
				}

				for (unsigned int q = 0; q < str2.length(); q++)
				{
					switch (str2[q])
					{
					case '3':
						str2[q]='~';
						break;
					case '2':
					case '-':
						if (type == f) str2[q] = '~'; 
						else if (type == fr) str2[q] = '~';
								 else str2[q] = '-';
						break;
					case '0':
						if (type == f) str2[q] = '~';
						else if (type == fd) str2[q] = '~';
						break;
					case '4':
						str2[q] = '1';
						break;
					}
				}

				ConstructFromPLALine(str, str2);
			}
			break;
		default: 
			//nedefinovany stav, chyba v PLA? 
			string s;
			s = "Parser Error: Incorrect input PLA file.\n";
			s += "Line Number: " + line; s += "\n";
			s += "Line Copy: " + tmp; s += "\n";
			throw s;
		}
	}
}

void Graph::ConstructFromPLAFile(char *filename)
{
	list<string> buffer;
	buffer.clear();
	ifstream f; 
	string s;
	f.open(filename);
	if (!f.is_open())
	{
		throw "Cannot open file: " + string(filename);
	}
	else
	{
		while (!f.eof())
		{
			getline(f, s);
			buffer.push_back(s);
		}
		f.close();
		
		return ConstructFromPLALines(buffer);
	}
}
string Graph::GenerateStreamForPLA()
{
	std::ostringstream stream;
	stream << ".i " << count_inputs << endl;
	if (input_names!="") stream << ".ilb " << input_names << endl;
	stream << ".o " << count_outputs << endl;
	if (output_names!="") stream << ".ob " << output_names << endl;

	stream << ".p " << count_terms << endl;
	stream << ".type ";
	
	switch (type)
	{
	case f: stream << "f"; break;
	case fd: stream << "fd"; break;
	case fr: stream << "fr"; break;
	case fdr: stream << "fdr"; break;
	}

	stream << endl;

	for (list<GTerm*>::iterator iter = terms.begin();iter!=terms.end();iter++)
	{
		stream << (*iter)->GetIn() << " " << (*iter)->GetOut() << endl;
	}
	stream << ".e" << endl;
	return stream.str();
}


list<string> Graph::GenerateMatrix()
{
	list<string> tmp; 
	for (list<GTerm*>::iterator iter = terms.begin();iter!=terms.end();iter++)
	{
		tmp.push_back((*iter)->GetIn());
	}
	return tmp;
}
//
void Graph::Simplification()
{
	for (int i=0;i<count_outputs;i++) Simplification(i);
}
void Graph::SimplificationWithDontCares()
{
	for (int i=0;i<count_outputs;i++) SimplificationWithDontCares(i);
}
string Graph::BruteForceTautology() const
{
	string str;
	str = BruteForceTautology(0);
	for (int i=1;i<count_outputs;i++) str += "\n" + BruteForceTautology(i);
	return str;
}
string Graph::BranchAndBoundTautology() const
{
	string str;
	str = BranchAndBoundTautology(0);
	for (int i=1;i<count_outputs;i++) str += "\n" + BranchAndBoundTautology(i);
	return str;
}
Graph* Graph::Complement()
{
	//complement
	list<string> complement; 
	complement.push_back(".i " + To_String(count_inputs));
		if (input_names!="") complement.push_back(".ilb " + input_names);
	complement.push_back(".o " + To_String(count_outputs));
		if (output_names!="") complement.push_back(".ob " + output_names);
	complement.push_back(".type f");
	complement.push_back("");

	for (int i = 0; i < count_outputs; i++) 
	{
		string out = "";
		for (int j = 0; j < count_outputs; j++) out += "~";
		out[i] = '1';
		list<string> tmp = Complement(i);
		
		for (list<string>::iterator it = tmp.begin(); it != tmp.end(); it++)
			(*it).append(" " + out);
		complement.splice(complement.end(), tmp);
	}

	Graph *g = new Graph();
	g->ConstructFromPLALines(complement);

	return g;
}
void Graph::Minimization(const bool deep)
{
	if (type == fr) 
	{
		throw "Minimization works only on types F, FD and FDR.";
		return;
	}
	
	//odstran OFFSETy, pro minimalizaci nas momentalne nezajimaji
	for (int i=0;i<count_outputs;i++)
	{
		list<GTerm*>::iterator iter = outputs[i].terms_off.begin();
		while (iter !=outputs[i].terms_off.end())
		{
			RemoveTermOutput(*iter, i);
			iter = outputs[i].terms_off.begin();
		}
	}

	for (int i=0;i<count_outputs;i++) Minimization(i, deep);
	type = f;
}
void Graph::Orthogonalization(const bool deep)
{
	if (type == fr) 
	{
		throw "Minimization works only on types F, FD and FDR.";
		return;
	}
	
	//odstran OFFSETy, pro minimalizaci nas momentalne nezajimaji
	for (int i=0;i<count_outputs;i++)
	{
		list<GTerm*>::iterator iter = outputs[i].terms_off.begin();
		while (iter !=outputs[i].terms_off.end())
		{
			RemoveTermOutput(*iter, i);
			iter = outputs[i].terms_off.begin();
		}
	}

	for (int i=0;i<count_outputs;i++) Orthogonalization(i, deep);
	type = f;
	Absorbtion_OrthRespect();
}



//
// pomocne funkce
//
void TrimLeft (string &s, const string &sp) 
{ 
  s = s.erase (0, s.find_first_not_of (sp)); 
}

void TrimRight (string &s, const string &sp)
{ 
  string::size_type pom(s.find_last_not_of (sp));
  if (pom == string::npos) s = "";
  else s = s.erase (s.find_last_not_of (sp) + 1); 
}

void Trim (string &s, const string &sp)
{ 
	TrimLeft(s,sp);
	TrimRight(s,sp);
}

string Separation(string &s, const string &sp)
{
	if (s.empty()) return "";
	string str;
	string::size_type pom(s.find_first_of(sp));
	if (pom == string::npos) 
	{
		str = s;
		s = s.erase();
		return str;
	}
	else
	{
		str = s.substr(0,pom);
		s = s.erase(0, pom);
		TrimLeft(s);
		return str;
	}
}

void IncStr(string &str) //zvetsuje retezec binarniho cisla o 1 (10011 -> 10100)
{
	int pos = (int) str.length() - 1; //pozice posledniho bitu
	while (str[pos]!='0')
	{
		str[pos]='0';
		pos--;
	}
	str[pos] = '1';
}

bool FindMatch(string &a, string &b) 
{
	if (a.length() != b.length()) return false;
	for (unsigned int i=0;i<a.length();i++)
	{
		if ((a[i]!='-') && (b[i]!='-')) return true;
	}
	return false;
}
void MergeMatch(string &a, string &b)
{
	if (a.length() != b.length()) throw "can't merge two strings of different sizes";
	for (unsigned int i=0;i<a.length();i++)
		if (b[i]!='-') a[i] = '1';
	return;
}

