//---------------------------------------------------------------------------

#include "Kernel/stdafx.h"

using namespace std;

#pragma hdrstop
#include "Kernel/kernelincludes.h"
#include "Tautology.h"

//#define DEBUG

//---------------------------------------------------------------------------


/**
*  Implementations of tautology detection tool classes
*
*  author:    Bc. Jan Schindler
*  project:   DP, CVUT, FEL, 2009
*/



/////////////  tautology detector  ///////////////////////////////////////////////////

/**
* interface metod for communication with kernel
* accept PLA
*/
int TautologyDetector::isPLAtautology(PLA* pla){
    cover = new Cover();
	cover->loadPLA(pla);
	int result = tautology();
    return result;
}

/**
* interface metod for communication with kernel
* accept SoPLA
*/
int TautologyDetector::isSoPLAtautology(SoPLA* sopla){
    cover = new Cover();
	cover->loadSoPLA(sopla);
	return tautology();
}

/**
* special cases detection
*/
int Cover::specialCases(){
	// 1) row of 2's
	if(containsRowOf2s()){
		return 1;
	}
	// 2) column of 0's or 1's
	if(containsColumnOf0sOr1s()){
		return 0;
	}
	// 3) deficient vertex count
	if(containsDeficientVertexCount()){
		return 0;
	}
	// truth table if <= 7 inputs or no 2's
	if(countVariables <= 7){
		return isCoverByTruthTable();
	}
	return -1;
}


/**
* realization of main recursive loop
*/
int TautologyDetector::tautology(){

	int t = cover->specialCases();
	if(t != -1){
        delete cover;
		return t;
	}

	// UNATE_REDUCTION
	if(t == -1){
		int numberOfUnatesColumns = cover->detectUnateColumns();
		// if there are unates columns
		if(numberOfUnatesColumns > 0){
			Cover* unateReductant = cover->unateReduction(numberOfUnatesColumns);
			if(unateReductant == NULL){
				return 0;
			}
			delete cover;
			cover = unateReductant;
			t = tautology();
		}
	}
	if(t != -1){ 
		return t;
	}	
	// most binate variable
	int j = cover->binateSelect();
	
	// COMPONENT_REDUCTION
	// only sufficiently sparse matrixes are checked for components
	if(cover->count01InColumn[0][j] < (cover->countTerms / 6)){
		vector<Cover*> queueTau = cover->findComponents();
		if(!queueTau.empty()){
            //delete cover;
			int size = queueTau.size();
			for(int i = 0; i < size; i++){
				Cover* component = queueTau.back();
				queueTau.pop_back();
				delete cover;
				cover = component;
				tautology();
				if (t == 1){
                   return 1;      
                }
			}
			return 0;
		}
	}
	if(t != -1){
		return t;
	}
	
	Cover *cof0 = cover->createCofactor(j, '0');
	Cover *cof1 = cover->createCofactor(j, '1');
	delete cover;
    
    // less DC first -> bigger chance not to be tautology
    if(cof0->getTotalDCnumber() <= cof1->getTotalDCnumber()){
		// question answered by recursive call to cofactors
		cover = cof0;
		if(tautology() == 0){
			return 0;
		}
		cover = cof1;
		if(tautology() == 0){
			return 0;
		}
    } else {
        // question answered by recursive call to cofactors
		cover = cof1;
		if(tautology() == 0){
			return 0;
		}
		cover = cof0;
		if(tautology() == 0){
			return 0;
		}      
    } 
	return 1;
}

/**
* init convertion of PLA to Cover
*/
void Cover::loadPLA(PLA* pla){
	list<Term>::iterator ti;
	TermList *data = pla->GetData();

	countVariables = pla->GetInputs();
	countTerms = data->size();

	if (pla->GetType().f){
		
	} else {
		throw IOException( "PLA is not 'f' type " );
	}

	// init of matrix
	matrix = new char*[countTerms];
	for (int i = 0; i < countTerms; ++i){
		matrix[i] = new char[countVariables];
	}
	initSupportFields();
	// load from PLA
	unsigned int i = 0;
	for ( ti = data->begin(); ti != data->end(); ti++ ){
		string term = (*ti).GetIM();
		strncpy(matrix[i], term.c_str(), term.length());
		i++;
	}

    // data tranfer + saving data info to support fields
	for(int ind = 0; ind < countTerms; ind++){
		for(int j = 0; j < countVariables; j++){
			switch(matrix[ind][j]){
				case '0':
					count01InColumn[0][j]++;
					break;

				case '1':
					count01InColumn[1][j]++;
					break;

				case '-':
					count2InRow[ind]++;
					totalDCnumber++;
					break;

				default:
					// error input value
					break;
			}
		}
	}
}

/**
* init convertion of SoPLA to Cover
*/
void Cover::loadSoPLA(SoPLA* sopla){
	list<SoTerm>::iterator soti;
	SoTermList *sodata = sopla->GetData();

	countVariables = sopla->GetInputs();
	countTerms = sodata->size();

	// init of matrix
	matrix = new char*[countTerms];
	for (int i = 0; i < countTerms; ++i){
		matrix[i] = new char[countVariables];
	}
	initSupportFields();
	// load from SoPLA
	unsigned int i = 0;
	for ( soti = sodata->begin(); soti != sodata->end(); soti++ ){
		string term = (*soti).GetIM();
		strncpy(matrix[i], term.c_str(), term.length());
		i++;
	}
    // data transfer + saving data to support fields
	for(int ind = 0; ind < countTerms; ind++){
		for(int j = 0; j < countVariables; j++){
			switch(matrix[ind][j]){
				case '0':
					count01InColumn[0][j]++;
					break;

				case '1':
					count01InColumn[1][j]++;
					break;

				case '-':
					count2InRow[ind]++;
					totalDCnumber++;
					break;

				default:
					// error input value
					break;
			}
		}
	}
}

/**
* destructor of cover
*/
Cover::~Cover(){		
	destroyFields();
}

/**
* dealocation of dynamic arrays
*/
void Cover::destroyFields(){
	// delete matrix
	for (int i = 0; i < countTerms; ++i){
		delete []matrix[i];
	}
	delete []matrix;

	// delete count01InColumn
	for (int i = 0; i < 2; ++i){
		delete []count01InColumn[i];
	}
	delete []count01InColumn;

	// delete other 1D fields
	delete []configuration;
	delete []indexesOfUnatesColumns;
	delete []indexesOfUnatesRows;
	delete []selectedRows;          
	delete []selectedColumns;       
	delete []totalComponentedRows;  
	delete []selectedRowIndexes;    
	delete []selectedColumnsIndexes;
	delete []count2InRow;
}

/**
* loading directly from given file
*/
void Cover::loadFromFile(const char *fn){
	ifstream inputStream;
	inputStream.open(fn);
	if (!inputStream.is_open()) throw IOException( "Cannot open file: " + string(fn) );

	inputStream >> countVariables;
	inputStream >> countTerms;
	// init of matrix
	matrix = new char*[countTerms];
	for (int i = 0; i < countTerms; ++i){
		matrix[i] = new char[countVariables];
	}
	// nacteni ze souboru
	for (int i = 0; i < countTerms; i++){
		for (int j = 0; j < countVariables; j++){
			inputStream >> matrix[i][j];
		}
	}
	initSupportFields();
}

/**
* alocating of support arrays
*/
void Cover::initSupportFields(){
    // allocate fields
	configuration = new char[countVariables];

	count01InColumn = new int*[2];
	for (int i = 0; i < 2; ++i){
		count01InColumn[i] = new int[countVariables];
	}
	
	count2InRow = new int[countTerms];
	indexesOfUnatesColumns = new int[countVariables];
	indexesOfUnatesRows = new int[countTerms];
	selectedRows = new int[countTerms];
	selectedColumns = new int[countVariables];
	totalComponentedRows = new int[countTerms];
	selectedRowIndexes = new int[countTerms];
	selectedColumnsIndexes = new int[countVariables];

	// reset	
	for (int i = 0; i < countVariables; i++){
		count01InColumn[0][i] = 0;	
		count01InColumn[1][i] = 0;
	}

	for (int i = 0; i < countTerms; i++){
		count2InRow[i] = 0;
	}
	totalDCnumber = 0;
}

/**
* write curent cover on screen
*/
void Cover::write(){
	for (int i = 0; i < countTerms; i++){
		for (int j = 0; j < countVariables; j++){
			cout << matrix[i][j] << " ";
		}
		cout << endl;
	}
}

/**
* write current configuration on screen
*/
void Cover::writeConfiguration(){
	for (int i = 0; i < countVariables; i++){
		cout << configuration[i];
	}
	//cout << endl;
}

/**
* is current configuration TRUE
*/
bool Cover::isConfigurationTrue(){
	bool isTermTrue = true;
	int numberOfPassedTerms = 0;
	for (int i = 0; i < countTerms; i++){
		isTermTrue = true;
		for (int j = 0; j < countVariables; j++){
			if(matrix[i][j] != '-'){
				if(configuration[j] != matrix[i][j]){
					isTermTrue = false;
					break;
				}
			}
		}
		if(isTermTrue){
			return ++numberOfPassedTerms;	
		}
	}
	return numberOfPassedTerms;
}

/**
* recursive appling of brute force to answer tautology question
*/
void Cover::searchTruthTable(int index){
	index++;	
	if(index < countVariables){
		configuration[index] = '0';	
		searchTruthTable(index);
		configuration[index] = '1';
		searchTruthTable(index);
	} else {
		//writeConfiguration();
		bool jeKonfPravda = isConfigurationTrue();
		if(!jeKonfPravda){
			isCover = false;
			return;
		}
	}
}

/**
* init of brute force call
*/
bool Cover::isCoverByTruthTable(){
	isCover = true;
	for (int i = 0; i < countVariables; i++){
		configuration[i] = '0';
	}
	searchTruthTable(-1);
	return isCover;
}

/**
* is there any full cube
*/
bool Cover::containsRowOf2s(){
	for (int i = 0; i < countTerms; i++){
		if(count2InRow[i] == countVariables){
			return true;
		}
	}
	return false;
}

/**
* is there any collumn of 1 or 0
*/
bool Cover::containsColumnOf0sOr1s(){
	for (int j = 0; j < countVariables; j++){
		if(count01InColumn[0][j] == countTerms || count01InColumn[1][j] == countTerms){
			return true;
		}	
	}
	return false;
}

/**
* is sum 2^k (k-count of 2 in cube) < 2^n (n-count of cubes)
*/
bool Cover::containsDeficientVertexCount(){
    char* grid = new char[countVariables + 1];
    for (int i = 0; i < countVariables + 1; i++){
        grid[i] = '0';        
    } 
    int maxIndex = 0;
    int index = 0;

	for (int i = 0; i < countTerms; i++){
        index = count2InRow[i];
        while(grid[index] != '0'){
             grid[index] = '0';
             index++;
             if(index > countVariables){ 
                 delete []grid;  
                 return false;         
             }                                   
        }
        grid[index] = '1';
        if(index > maxIndex){
            maxIndex = index;
        }
	}
	if(maxIndex < countVariables){
        delete []grid;
        return true;            
    } else {
        delete []grid;
        return false;            
    }  
}

/**
* searching for most binate variable
*/
int Cover::binateSelect(){
	int maxPairs01 = 0;
	int mostBinateJ = 0;
	for (int i = 0; i < countVariables; i++){	
		if(min(count01InColumn[0][i], count01InColumn[1][i]) > maxPairs01){
			maxPairs01 = min(count01InColumn[0][i], count01InColumn[1][i]);
			mostBinateJ = i;
		}
	}
	return mostBinateJ;
}

/**
* creates cofactor of given variable and flag (1 - variable, 0 - its negation)
*/
Cover* Cover::createCofactor(int mostBinateJ, char flag){
	Cover *cofactor = new Cover();
	int numberOf0inJthColumn = 0;
	int numberOf1inJthColumn = 0;
	int numberOf2inJthColumn = 0;
	for(int i = 0; i < countTerms; i++){
		switch(matrix[i][mostBinateJ]){
			case '0': numberOf0inJthColumn++;
				break;
			case '1': numberOf1inJthColumn++;
				break;
			case '-': numberOf2inJthColumn++;
				break;
			default: cout << "chyba cof" << endl;
				break;
		}
	}
	int numberOfVariablesInCofactor = countVariables - 1;
	int numberOfTermsInCofactor = 0;
	if(flag == '0'){
		numberOfTermsInCofactor = numberOf0inJthColumn + numberOf2inJthColumn;
	}
	if(flag == '1'){
		numberOfTermsInCofactor = numberOf1inJthColumn + numberOf2inJthColumn;
	}
	cofactor->countVariables = numberOfVariablesInCofactor;
	cofactor->countTerms = numberOfTermsInCofactor;
	cofactor->matrix = new char*[numberOfTermsInCofactor];
	for (int i = 0; i < numberOfTermsInCofactor; ++i){
		cofactor->matrix[i] = new char[numberOfVariablesInCofactor];
	}
	cofactor->initSupportFields();

	// copy values to cofactor
	int CofactorTermIndex = 0;
	int CofactorVariableIndex = 0;
	// data transfer and saving data info to support fields
	for (int i = 0; i < countTerms; i++){
		//najde radek ktery je treba zkopirovat
		if(matrix[i][mostBinateJ] == flag || matrix[i][mostBinateJ] == '-'){
			for(int j = 0; j < countVariables; j++){
				if(j != mostBinateJ){
					cofactor->matrix[CofactorTermIndex][CofactorVariableIndex]	= matrix[i][j];
					switch (matrix[i][j]){
						case '0':
							cofactor->count01InColumn[0][CofactorVariableIndex]++;
							break;
						
						case '1':
							cofactor->count01InColumn[1][CofactorVariableIndex]++;
							break;
						
						case '-':
							cofactor->count2InRow[CofactorTermIndex]++;
							cofactor->totalDCnumber++;
							break;
						
						default:
							// error input
							break;
					}
					CofactorVariableIndex++;
				} 
			}
			CofactorVariableIndex = 0;
			CofactorTermIndex++;
		}	
	}
	return cofactor;
}


/**
* is given column unate
*/
bool Cover::isColumnUnate(int columnIndex){
	if(count01InColumn[0][columnIndex] == 0 || count01InColumn[1][columnIndex] == 0){
		return true;
	}
	return false;
}

/**
* select and mark unate columns, return their count
*/
int Cover::detectUnateColumns(){
	// unates columns index reset
	for(int i = 0; i < countVariables; i++){
		indexesOfUnatesColumns[i] = -1;
	}

	int numberOfUnateColumns = 0;
	int indexOfUnateColumns = 0;
	for(int i = 0; i < countVariables; i++){
		if(isColumnUnate(i)){
			numberOfUnateColumns++;
			indexesOfUnatesColumns[indexOfUnateColumns] = i;
			indexOfUnateColumns++;
		}
	}
	return numberOfUnateColumns;
}

/**
* creates unates reductant
*/
Cover* Cover::unateReduction(int numberOfUnateColumns){
	// reset of indexes of rows for unate reduction detection
	for(int i = 0; i < countTerms; i++){
		indexesOfUnatesRows[i] = -1;
	}

	int numberOf2sPerUnateRow = 0;
	int indexOfUnateRows = 0;
	for (int i = 0; i < countTerms; i++){
		for (int j = 0; j < numberOfUnateColumns; j++){
			if(matrix[i][indexesOfUnatesColumns[j]] == '-'){
				numberOf2sPerUnateRow++;	
			}	
		}
		if(numberOf2sPerUnateRow == numberOfUnateColumns){
			indexesOfUnatesRows[indexOfUnateRows] = i;
			indexOfUnateRows++;
		}
		numberOf2sPerUnateRow = 0;
	}
	
	if(indexOfUnateRows == 0){
		return NULL;
	}

	Cover* unateReductant = new Cover();
	unateReductant->countVariables = countVariables - numberOfUnateColumns;
	unateReductant->countTerms = indexOfUnateRows;


	unateReductant->matrix = new char*[unateReductant->countTerms];
	for (int i = 0; i < unateReductant->countTerms; ++i){
		unateReductant->matrix[i] = new char[unateReductant->countVariables];
	}
	unateReductant->initSupportFields();

	int indexOfUnateColumns = 0;
	// data transfer and saving data info to support fields
	for (int i = 0; i < unateReductant->countTerms; i++){
		for (int j = 0; j < countVariables; j++){
			if(indexesOfUnatesColumns[indexOfUnateColumns] != j){
				unateReductant->matrix[i][j-indexOfUnateColumns] = matrix[indexesOfUnatesRows[i]][j];
				switch (matrix[indexesOfUnatesRows[i]][j]){
						case '0':
							unateReductant->count01InColumn[0][j-indexOfUnateColumns]++;
							break;

						case '1':
							unateReductant->count01InColumn[1][j-indexOfUnateColumns]++;
							break;

						case '-':
							unateReductant->count2InRow[i]++;
							unateReductant->totalDCnumber++;
							break;

						default:
							// error input
							break;
				}
			} else {
				indexOfUnateColumns++;
			}
		}
		indexOfUnateColumns = 0;
	}

	return unateReductant; 
}

/**
* searching and creating components
*/
vector<Cover*> Cover::findComponents(){
	for(int i = 0; i < countTerms; i++){
		totalComponentedRows[i] = -1;
	}
	vector<Cover*> queueTau;
	int sumOfComponentsRows = 0;
	int rowToBeSearchedForComponent = 0;
	while(sumOfComponentsRows < countTerms){
		for(int i = 0; i < countTerms; i++){
			if(totalComponentedRows[i] == -1){
				rowToBeSearchedForComponent = i;
				break;
			}	
		}
		Cover* component = findComponentWithRow(rowToBeSearchedForComponent);
		if(component == NULL){
			return queueTau;
		} else {
			sumOfComponentsRows += component->countTerms;
			queueTau.push_back(component);
		}
	}
	return queueTau;
}

/**
* find smallest non-trivial component of given row
*/
Cover* Cover::findComponentWithRow(int rowIndex){
	vector<int> stack;
	stack.push_back(rowIndex);

	int componentRows = 0;
	int componentColumns = 0;
	for(int i = 0; i < countTerms; i++){
		selectedRows[i] = -1;
		selectedRowIndexes[i] = -1;
	}
	for(int i = 0; i < countVariables; i++){
		selectedColumns[i] = -1;
		selectedColumnsIndexes[i] = -1;
	}
	/*
	for all rows in queue we mark and search all non marked columns
	and we add to queue all non marked rows, where in column is not DC
	*/
	while(!stack.empty()){
		int exploringRow = stack.back();
		stack.pop_back();
		selectedRows[exploringRow] = 1;
		totalComponentedRows[exploringRow] = 1;
		selectedRowIndexes[componentRows] = exploringRow;
		componentRows++;
		for (int j = 0; j < countVariables; j++){
			if(matrix[exploringRow][j] != '-' && selectedColumns[j] == -1){
				selectedColumns[j] = 1;
				selectedColumnsIndexes[componentColumns] = j;
				componentColumns++;
				for (int i = 0; i < countTerms; i++){
					if(matrix[i][j] != '-' && selectedRows[i] == -1){
						stack.push_back(i); 
						selectedRows[i] = 1;
					}
				}
			}	
		}
	}

	if(componentRows == countTerms){
		// there only ONE component - The original matrix
		return NULL;
	}

	Cover* component = new Cover();
	component->countVariables = componentColumns;
	component->countTerms = componentRows;
	component->matrix = new char*[component->countTerms];
	for (int i = 0; i < component->countTerms; ++i){
		component->matrix[i] = new char[component->countVariables];
	}
	component->initSupportFields();
	int indexColumns = 0;
	int indexRows = 0;
	// data transfer and saving data info to support field
	for (int i = 0; i < component->countTerms; i++){
		for (int j = 0; j < component->countVariables; j++){
			component->matrix[i][j] = matrix[selectedRowIndexes[i]][selectedColumnsIndexes[j]];	
			switch (matrix[selectedRowIndexes[i]][selectedColumnsIndexes[j]]){
						case '0':
							component->count01InColumn[0][j]++;
							break;

						case '1':
							component->count01InColumn[1][j]++;
							break;

						case '-':
							component->count2InRow[i]++;
							component->totalDCnumber++;
							break;

						default:
							// error input
							break;
			}
		}
	}

	return component;
}

/**
* how many DC there are in the cover
*/
int Cover::getTotalDCnumber(){
    return totalDCnumber;
}

 
