#include <cstdlib>
#include <iostream>
#include <math.h>
#include <vector>
#include "Rule.h"
using namespace std;

#define T '*'
#define F '#'

/* Numbers only used for return val of isCharTrue(C)
0 == false
1 == true
2 == maybe
*/

// Prints menu
void printMenu();
// Gets input for menu
void getMenuResponse(int&,int,int);
// Looping function allows user to add to rulesGiven
void getNewRule();
// Allows user to remove a single rule from rulesGiven
void removeARule();
// Prints both lists of rules
void printRules();

// Proving function. Pass a char to be proved.
int proove(char);
// Proves what char the user inputs
void proveSomething();
// Called whenever rulesGiven changes. Generates inferred rules.
void proveItAll();

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

// Checks new rule to see if there is a contradiction in existing rules.
bool checkForContradictions(Rule*);
// Puts truths, then falses, then general rules.
void reOrderRules();

// Used for integrity. Disallows looping in recursion proving.
bool alreadyTryingToProve(char);
// Removes char from list of chars already being proven.
void removeFromTrying(char);

// Checks to see if rule already exists in list.
bool checkForDuplicate(Rule*);
// Checks inferred list to see if char is already proved.
int isCharTrue(char);
// Returns conjugate of char
char conjugate(char);
// Checks the user input for flaws
int checkForProperInput(char*);

vector <Rule*> rules;
vector <Rule*> rulesGiven;
vector <char> tryingToProve;