#include "IEngine.h"

int main() { // main program. Handles menu and response.
	int menuResponse;

	do{
		proveItAll();							// Rule list maintenance
		reOrderRules();		
		printMenu();							// Menu work
		getMenuResponse(menuResponse, 0, 4);
		switch(menuResponse)
		{
		case 1:	getNewRule(); break;
		case 2: printRules(); break;
		case 3: removeARule(); break;
		case 4: proveSomething(); break;
		default:break;
		}
	}while(menuResponse != 0);
	return 0;
}

void printMenu() { // Prints menu
	cout << "Make your selection!" << endl;
	cout << "1) Add rule to list" << endl;
	cout << "2) Print rules" << endl;
	cout << "3) Remove a rule" << endl;
	cout << "4) Prove something" << endl;
	cout << "0) QUIT!" << endl;
}

void getMenuResponse(int &menuResponse, int L, int H) { // Gets input for menu
	menuResponse = L-1;
	while(menuResponse < L || menuResponse > H)
	{
		menuResponse = L;
		cin >> menuResponse;
	}
}

void getNewRule() { // Looping function allows user to add to rulesGiven
	char c[20];
	int j;
	for(j=0;j<20;j++)
		c[j] = NULL;
//	system("cls");
	do{
		proveItAll();							// Rule list maintenance
		reOrderRules();	
		printRules();							// Format printing
		cout << "Please format the following way : ABD>E   ==  A ^ B ^ D -> E" << endl;
		cout << "\'0\' exits " << endl;
		cin >> c;								// Rule input
		if(c[0] == '0')							// Loop break statement
			return;

//		system("cls");
		switch(checkForProperInput(c))			// Check for what type of flaw (or none)
		{
		case 1: cout << "Found an improper character. Must be a->z or A->Z\n"; break;
		case 2: cout << "Found too many characters after the >. There can only be one. (Highlander).\n"; break;
		case 0:
		default:									// Input OK. Adding the rule.
			Rule* newRule = new Rule(c);			// Create the rule
			if(!checkForContradictions(newRule))	// Check for contraditions and duplicates
				if(!checkForDuplicate(newRule))
					rulesGiven.push_back(newRule);	// Add rule
			break;
		}
		cout << c << "\n\n";
	}while(1);
}

void removeARule() { // Allows user to remove a single rule from rulesGiven
//	system("cls");
	vector <Rule*> temp;
	int index,j;
	printRules();								// Prints rules
	cout << "Please enter the index of the one you want to remove" << endl;
	cin >> index;
	index -= 1;

	if(index > rulesGiven.size() || index < 0)	// Checks for valid input
		return;

	for(j=0; j<rulesGiven.size(); j++)			// Moves all given rules to temporary vector
		temp.push_back(rulesGiven[j]);
	rulesGiven.clear();							// Clears all rules
	rules.clear();
	for(j=0; j<temp.size(); j++)				// Moves all rules (except index) to given list
		if(j != index)
			rulesGiven.push_back(temp[j]);
}

void printRules() { // Prints both lists of rules
	int j=0;
	cout << "List Of All Current Rules" << endl;
	cout << "GIVEN:" << endl;
	while(j < rulesGiven.size())				// Prints given list
	{
		cout << j+1 << ") ";
		rulesGiven[j++]->print();
	}
	cout << endl << endl;
	cout << "INFERRED:" << endl;
	j=0;
	while(j < rules.size())						// Prints inferred list
		rules[j++]->print();
	cout << endl << endl;
}

int proove(char C) { // Proving function. Pass a char to be proved.

 	int j=0,i=isCharTrue(C);			// Test if char is true, false, or maybe 
	int proven = 2;
	int nOfRuleMatches = 0;

	if(i == 1)							// if char == true
	{
//		cout << "Proving " << C << " TRUE " << endl;
		addTruth(C);
		return 1;
	}
	else if(i == 0)						// if char == false
	{
//		cout << "Proving " << C << " FALSE " << endl;
		addTruth(conjugate(C));
		return 0;
	}

	for(j=0; j<rules.size(); j++)		// if char == maybe
	{
		if(rules[j]->right == C)		// for every rule that matches char on right side
		{
			nOfRuleMatches++;
			for(i=0; i<rules[j]->left.size(); i++) // Prove everything on left of rule
			{
				if(!alreadyTryingToProve(rules[j]->left[i]))
				{
					tryingToProve.push_back(C);
					proven = proove(rules[j]->left[i]);
					removeFromTrying(C);
				}
				else
					proven = 2;
			}

			if(proven==1 && nOfRuleMatches>0)			// If rule is proven
			{
				Rule *newRule = new Rule(C);		// Create new rule for char
				if(!checkForContradictions(newRule))// Make sure rule doesn't contradict anything
				{
					addTruth(C);					// Add rule
					removeFromTrying(C);
					return 1;
				}
				else
					return 0;
			}
		}
	}
//	cout << "Proving " << C << proven << endl;
	if(proven == 0)
		addTruth(conjugate(C));
	return proven;
}

void proveSomething() { // Proves what char the user inputs
//	system("cls");
	char C;
	cout << "What char do you want to prove? " << endl;
	cin >> C;
	int i = isCharTrue(C);								// Try and prove a char
	if(i==1)
		cout << C << " is TRUE!\n\n" << endl;			// Cases of proof
	else if(i==0)
		cout << C << " is FALSE!\n\n" << endl;
	else
		cout << C << " is MAYBE!\n\n" << endl;
}

void proveItAll() { // Called whenever rulesGiven changes. Generates inferred rules.
	int j,change = 1;
	rules.clear();
	for(j=0; j<rulesGiven.size(); j++)
		rules.push_back(rulesGiven[j]); // Puts all of given rules into inferred rules

	while(change != 0)					// change of # of inferred rules
	{
		change = rules.size();
		for(j=0; j<rules.size(); j++)	// for every rule
			proove(rules[j]->right);	// prove the right hand side
		change -= rules.size();
	}
}

void addTruth(char C) { // Adds a truth of char and a false of conjugate to inferred.
	addATruth(C);
	addAFalse(conjugate(C));
}

void addATruth(char C) {			// Adds a truth of char
	Rule *r = new Rule(C);
	if(!checkForDuplicate(r))
		rules.push_back(r);
}

void addAFalse(char C) {			// Adds a false of char
	Rule *r = new Rule(C,1);
	if(!checkForDuplicate(r))
		rules.push_back(r);
}

// Checks new rule to see if there is a contradiction in existing rules.
bool checkForContradictions(Rule* newRule) {
	int j;
	char nL = newRule->left[0];
	char nR = newRule->right;
	char oL, oR;
	for(j=0; j<rules.size(); j++)			// For every rule
	{
		oL = rules[j]->left[0];				// Check to see if it matches any other rule
		oR = rules[j]->right;				// in a contradictory way...
											// just trust me...it works  :)
		if((nR == oR) && ( nL == T || nL == F) && ( oL == T || oL == F) && (oL != nL))
			return true;
		
		oR = conjugate(oR);	
		if((nR == oR) && ( nL == T || nL == F) && ( oL == T || oL == F) && (oL == nL))
			return true;
	}
	return false;
}

void reOrderRules() { // Puts truths, then falses, then general rules.
	vector<Rule*> temp;
	int j;
	
	// Reorders inferred rules.	
	for(j=0; j<rules.size(); j++)			// Stores all rules
		temp.push_back(rules[j]);
	rules.clear();	
	for(j=0; j<temp.size(); j++)			// Adds truths
		if(temp[j]->left[0] == T)
			rules.push_back(temp[j]);
	for(j=0; j<temp.size(); j++)			// Adds falses
		if(temp[j]->left[0] == F)
			rules.push_back(temp[j]);
	for(j=0; j<temp.size(); j++)			// Adds general rules
		if(temp[j]->left[0] != T && temp[j]->left[0] != F)
			rules.push_back(temp[j]);

	// Reorders given rules.
	temp.clear();
	for(j=0; j<rulesGiven.size(); j++)		// Stores rules
		temp.push_back(rulesGiven[j]);
	rulesGiven.clear();
	for(j=0; j<temp.size(); j++)			// Adds truths
		if(temp[j]->left[0] == T)
			rulesGiven.push_back(temp[j]);
	for(j=0; j<temp.size(); j++)			// Adds falses
		if(temp[j]->left[0] == F)
			rulesGiven.push_back(temp[j]);
	for(j=0; j<temp.size(); j++)			// Adds general rules
		if(temp[j]->left[0] != T && temp[j]->left[0] != F)
			rulesGiven.push_back(temp[j]);
}

bool alreadyTryingToProve(char C) { // Used for integrity. Disallows looping in recursion proving.
	int j;
	for(j=0; j<tryingToProve.size(); j++)
		if(tryingToProve[j] == C)
			return true;
	return false;
}

void removeFromTrying(char C) { // Removes C from list of chars already being proven.
	vector<char> temp;
	int j;
	for(j=0; j<tryingToProve.size(); j++)	// Store all chars trying
		temp.push_back(tryingToProve[j]);

	tryingToProve.clear();

	for(j=0; j<temp.size(); j++)			// Put all chars except C back
		if(temp[j] != C)
			tryingToProve.push_back(temp[j]);
}

bool checkForDuplicate(Rule *r) { // Checks to see if rule already exists in list.
	int j;
	for(j=0; j<rules.size(); j++)
		if(*rules[j] == *r)
			return true;
	return false;
}

int isCharTrue(char C) { // Checks inferred list to see if char is already proved.
	int j;
	for(j=0; j<rules.size(); j++)
	{
		if(rules[j]->right == C && rules[j]->left[0] == T)
			return 1;
		if(rules[j]->right == C && rules[j]->left[0] == F)
			return 0;
		if(rules[j]->right == conjugate(C) && rules[j]->left[0] == T)
			return 0;
		if(rules[j]->right == conjugate(C) && rules[j]->left[0] == F)
			return 1;
	}
	return 2;
}

char conjugate(char C) { // Returns conjugate of char
	char D;
	if((int)C >= 65 && (int)C <= 90)		// Change from capital to lower
		D = C + 32;
	else if((int)C >= 97 && (int)C <= 122)	// Change from lower to capital
		D = C - 32;
	return D;
}

int checkForProperInput(char *c) { // Checks the user input for flaws
	int j, count=0;
	bool arrowFound = false;
	for(j=0; c[j] != NULL; j++) // For every character in the string
	{
		if(arrowFound)			// When the arrow has been found, count all following chars
			count++;
		if( !(c[j]>=65 && c[j]<=90) && !(c[j]>=97 && c[j]<=122) && c[j]!='>')
			return 1;			// If char is not a->z or A->Z or '>' return problem
		if(c[j] == '>' && !arrowFound)
			arrowFound = true;	// Flags the '>' for counting purposes.
		if(count > 1)			// Returns problem if > 1 chars after the '>'
			return 2;
	}
	return 0;					// Returns no problem
}