/*  This is a partial solution to program-3:
	    a Propositional Logic checker
	   					2/15/2007
	///////////////////////////////////////////////////////////////
	    The definition of the following functions have been left out
	    on purpose for you to complete for this program:
	    1. int wff: finalTest()
	       This function checks to see the given wff (with an antecedent
	       and a consequent without any operators left) is valid.
	       It is valid if and only if a predicate symbol appears in
	       both the antecedent and the consequent.
	    2. int wff: validTest()
	       This recursive function checks to see the current wff is valid
	       by repeatedly eliminating an operator appearing in either its
	       antecedent or its consequent and calling itself subsequently.
	*/
	#include 
	#include 
	#include 	// For I/O Manipulators 
	#include 	// For exit(1)
	#include 	// For NULL
	#include 	// For string operations
	typedef char Exp[80];
	class ExpNode
	{
	  friend class List;
	  friend class wff;
	  Exp	Node;
	  int length;
	  ExpNode* Link;
	// Member functions, all private.
	  void strip();
	  ExpNode ();
	  ExpNode (Exp form);
	  ExpNode* PartCopy (int from, int to);
	  int findImp (int& start);
	  int findOr  (int& start);
	  int findAnd (int& start);
	  int findNot (int& start);
	};
	class List
	{
	  friend class wff;
	  friend main();	// Make private member functions available
				// to main().
	  ExpNode* firstExp;
	// Member functions, all private.
	  ExpNode* copyList();
	  void  remove (ExpNode* useless);
	  void insert  (ExpNode* added);
	  int findOp (ExpNode*& nod, int& where);
	  List();
	  List (ExpNode* first);
	  void Initial (Exp form);
	};
	class wff
	{ 
	  friend main();	// To make private components of this class
				// available to main()
	  List anti;
  	  List conseq;
  	  wff();	// A default constructor is mandatory if the following
			// dynamic declaration is used:
			// wff* pwwf = new wff;
	  wff* Copy();
	  int found (ExpNode*, ExpNode*);
	  int validTest();
	  int finalTest();
	};
	/////////////////////////////////////////////////
	  ExpNode::ExpNode()
	    {
		Link = NULL;
		length = 0;
		Node[0] = '\0';
	    }
	  ExpNode::ExpNode (Exp form)
	    {	strcpy(Node, form);
		Link = NULL;
		length = strlen (form);
		Node[length] = '\0';
	    }	// End of Constructor ExpNode (Exp form)
	/////////////////////////////////////////////////
	ExpNode* ExpNode:: PartCopy (int from, int to)
       	{  ExpNode* newnode = new ExpNode;
	   for (int k=from; k<=to; k++)
		newnode->Node [k-from] = Node[k];
	   newnode->Node [to-from+1] = '\0';
	   newnode->length = to-from+1;
	   newnode->Link = NULL;	//Just in case.

	   return newnode;
	}	// End of function PartCopy()					
	///////////////////////////////////////////////////	
	void ExpNode::strip()
	{ // strip all outermost pairs of parentheses and move resulting
	  // expression to the leftmost positions.
	  int level, k;
	  while (Node[0] == ' ')
		{
		for (k=1; k<=length; k++)
		  Node[k-1] = Node[k];
		length--;
		}
	  while (Node[length-1] == ' ')	//Check for trailing blanks.
		length--;
	  Node[length] = '\0';		// String terminator.
	  ///////////////////////////////////////////////////
	  int done = 0;
	  if (length <= 1) done=1;
	  while (Node[0]=='(' && Node[length-1] == ')' && !done)
		{
		level=0;
		for (k=0; k' has to be treated as left-associative, and so
	  // the rightmost one needs to be found
	  int level=0;
	  for (int k=length-1; k>1; k--)
	    {	start = k-1;
		if (Node[k] == '(') level++;
		if (Node[k] == ')') level--;
		if (!level && Node[k-1]=='-' && Node[k]=='>')
			return 1;	// The '->' has been found at the
					// topmost level.
	    }
	  return 0;
	}	// End of function findImp()
	//////////////////////////////////////////////////
	int ExpNode:: findOr (int& start)
	{
	  int level=0;
	  for (start=0; start<=length-2; start++)
	    {	if (Node[start] == '(') level++;
		if (Node[start] == ')') level--;
		if (!level && Node[start]=='O' && Node[start+1]=='R')
			return 2;
	    }
	  return 0;
	}
	///////////////////////////////////////////////////////
	int ExpNode:: findAnd (int& start)
	{
	  int level=0;
	  for (start=0; start<= length-3; start++)
	    {	if (Node[start]=='(') level++;
		if (Node[start]==')') level--;
		if (!level && Node[start]=='A' && Node[start+1]=='N'
		           && Node[start+2]=='D')  return 3;
	    }
	  return 0;
	}	// End of function findAnd()
	////////////////////////////////////////////////////////
	int ExpNode:: findNot (int& start)
	{
	  int level=0;
	  for (start=0; start<= length-3; start++)
	    {	if (Node[start] == '(') level++;
		if (Node[start] == ')') level--;
		if (!level && Node[start]=='N' && Node[start+1]=='O'
			   && Node[start+2]=='T')  return 4;
	    }
	  return 0;
	}
	////////////////////////////////////////////////////////
	List:: List()
	{ 	firstExp = NULL; 
	}	// Empty list initialization.
	//	End of the default constructor List()
	///////////////////////////////////////////////////////
	List::List (ExpNode* first)
	// This constructor simply initializes a list so that
	// the given node (first) is its first node.
	{	firstExp = first;
	}
	///////////////////////////////////////////////////////
	void List:: Initial (Exp form)
	{	ExpNode* newnode = new ExpNode(form);
		firstExp = newnode;
	}	//End of function Initial()
	//////////////////////////////////////////////////////
	ExpNode* List:: copyList()
	{	ExpNode* first = new ExpNode;	
		// The following declaration does not work for above:
		// ExpNode* first;	//Due to 'first->Node' being used.
		if (!firstExp)	// Empty list to copy.
			return NULL;
		else	// List not empty yet.
		{  strcpy (first->Node, firstExp->Node);
		   first->length = strlen (first->Node);
		   List tail (firstExp->Link);
		   first->Link = tail.copyList();
		   return first;
		}
	}	//End of function copyList()
	/////////////////////////////////////////////////////
	void List:: insert (ExpNode* added)
	{   if (firstExp)
		{
		added->Link = firstExp->Link;	//Insert right after the 
						//first node.
		firstExp->Link = added;
		}
	    else	// The first node is empty 
		{
		firstExp = added;
		firstExp->Link = NULL;
		}
	}	// End of function insert()
	///////////////////////////////////////////////////////
	void List:: remove (ExpNode* useless)
	{	ExpNode* current, *pred=NULL;
		current = firstExp;
		while (current != useless && current)
		  {	pred=current;
			current = current->Link;
		  }
		if (!current)
		  {	cout << "ERROR:::IN REMOVAL\n\n";
			exit(1);
		  }
		else	{
			if (!pred)	//Then it is first node to go.
				firstExp = firstExp->Link;
			else 	pred->Link = useless->Link;
			}
	}	// End of function remove()
	/////////////////////////////////////////////////////////////
	int List::findOp (ExpNode*& nod, int& where)
	{  //	Finds an operator to be eliminated along with the containing
	   //	node (Conjunct or Disjunct) and the starting position of it.
		ExpNode* current;
		nod = firstExp;	//First node to test.
		while (nod)
		  {	nod->strip();
			if (nod->findImp(where))
				return 1;	// '->' has been found.
			else if (nod->findOr(where))
				return 2;
			else if (nod->findAnd(where))
				return 3;
			else if (nod->findNot(where))
				return 4;
			else nod=nod->Link;
		  }
		return 0;	// No operator has been found.
	}	// End of function findOp()
	///////////////////////////////////////////////////////
  	wff::wff()
	{
		/* next two initalization cause a syntax error
		   as 'anti' nor 'conseq' has not been defined yet.
		anti.List();
		conseq.List();
		*/
    		List an, con;	// Get an empty list for both.
		anti = an;
		conseq = con;
   	}	// End of constructor wff()
	///////////////////////////////////////////////////////
	wff* wff:: Copy()
	{	// Following static declaration does not work due to
		// subsequently use of its purported component although
		// absence of an explicit default constructor does not
		// cause a syntax error unlike: 
				// wff* newone = new wff;
		wff* newone = new wff;
		(newone->anti).firstExp = anti.copyList();
		(newone->conseq).firstExp = conseq.copyList();
		return newone;
	}
	////////////////////////////////////////////////////////
	int wff:: found (ExpNode* target, ExpNode* listnode)
	{	ExpNode* current, *pred;
		if (!listnode) return 0; // List is already empty.
		current = listnode;
		target->strip();
		while (current)
		{	current->strip();
			if (!strcmp(current->Node, target->Node))
				return 1;
			else	current = current->Link;
		}
		return 0;
	}	// End of function found()
	////////////////////////////////////////////////////////
	int wff:: finalTest()
	// Both antecedent and consequent have no operator.
	//////////////////////////////////////////////////
	int wff::validTest()
	/////////////////////////////////////////////////
	// The definition is left out.	/////////////////
	/////////////////////////////////////////////////
	int main()
	{
	  Exp formula;
	  int inputCount=0;
	  int result;
	  while (cin.getline (formula,79))
		{
		inputCount++;
		cout << "INPUT FORMULA IS:::" << formula << endl;
		wff *inputt = new wff;
		(inputt->conseq).Initial (formula);
		if (result=inputt->validTest())
			cout << "   VALID.  \n\n";
		else    cout << "   INVALID.\n\n";
		}
	  cout << "MY PROGRAM STOPS AFTER PROCESSING " << setw(4) 
		<< inputCount << " INPUT FORMULAS.\n\n";
	  return 0;