POJ--3295

た入场券 2022-07-15 13:54 112阅读 0赞

Tautology

<table> 
 <tbody> 
 <tr> 
 <td>Time Limit:&nbsp;1000MS</td> 
 <td>&nbsp;</td> 
 <td>Memory Limit:&nbsp;65536K</td> 
 </tr> 
 <tr> 
 <td>Total Submissions:&nbsp;12192</td> 
 <td>&nbsp;</td> 
 <td>Accepted:&nbsp;4660</td> 
 </tr> 
 </tbody> 
</table>

Description

WFF 'N PROOF is a logic game played with dice. Each die has six faces representing some subset of the possible symbols K, A, N, C, E, p, q, r, s, t. A Well-formed formula (WFF) is any string of these symbols obeying the following rules:

*  p, q, r, s, and t are WFFs
 *  if *w* is a WFF, N*w* is a WFF
 *  if *w* and *x* are WFFs, K*wx*, A*wx*, C*wx*, and E*wx* are WFFs.

The meaning of a WFF is defined as follows:

*  p, q, r, s, and t are logical variables that may take on the value 0 (false) or 1 (true).
 *  K, A, N, C, E mean *and, or, not, implies,* and *equals* as defined in the truth table below.

<table> 
 <tbody> 
 <tr> 
 <td> Definitions of K, A, N, C, and E </td> 
 </tr> 
 </tbody> 
</table>

A *tautology* is a WFF that has value 1 (true) regardless of the values of its variables. For example, *ApNp* is a tautology because it is true regardless of the value of *p*. On the other hand, *ApNq* is not, because it has the value 0 for *p=0, q=1*.

You must determine whether or not a WFF is a tautology.

Input

Input consists of several test cases. Each test case is a single line containing a WFF with no more than 100 symbols. A line containing 0 follows the last case.

Output

For each test case, output a line containing *tautology* or *not* as appropriate.

Sample Input

ApNp
    ApNq
    0

Sample Output

tautology
    not

Source

[Waterloo Local Contest][], 2006.9.30

#include<stack>
 #include<iostream>
 #include<cstdio>
 #include<cstdlib>
 #include<cstring>
 using namespace std;
 int pp, qq, rr, tt, ss;
 
 stack<int>Q;
 bool num(char st)
 {
 
 	switch (st)
 	{
 	case'p':
 	{
 		Q.push(pp);
 		return true;
 	}
 	case'q':
 	{
 		Q.push(qq);
 		return true;
 	}
 	case'r':
 	{
 		Q.push(rr);
 		return true;
 	}
 	case's':
 	{
 		Q.push(ss);
 		return true;
 
 	}
 	case't':
 	{
 		Q.push(tt);
 		return true;
 	}
 
 	}
 	return false;
 }
 
 void oper(char st)
 {
 
 	switch (st)
 	{
 	case'K':
 	{
 		int m = Q.top();
 		Q.pop();
 		int v = Q.top();
 		Q.pop();
 		Q.push(m && v);
 		break;
 	}
 	case'A':
 	{
 		int m = Q.top();
 		Q.pop();
 		int v = Q.top();
 		Q.pop();
 		Q.push(m || v);
 		break;
 	}
 	case'N':
 	{
 		int m = Q.top();
 		Q.pop();
 
 		Q.push(!m);
 		break;
 	}
 	case'C':
 	{
 		int m = Q.top();
 		Q.pop();
 		int v = Q.top();
 		Q.pop();
 		Q.push((!m) || v);
 		break;
 	}
 	case'E':
 	{
 		int m = Q.top();
 		Q.pop();
 		int v = Q.top();
 		Q.pop();
 		Q.push(m == v);
 		break;
 	}
 	}
 
 	return ;
 }
 
 int main()
 {
 	char wff[210];
 	bool flag;
 	while (cin >> wff && wff[0] != '0')
 	{
 		flag = true;
 
 		int len = strlen(wff);
 		for (pp = 0; pp <= 1; pp++)
 		{
 			for (qq = 0; qq <= 1; qq++)
 			{
 				for (rr = 0; rr <= 1; rr++)
 				{
 					for (ss = 0; ss <= 1; ss++)
 					{
 						for (tt = 0; tt <= 1; tt++)
 						{
 
 							for (int i = len - 1; i >= 0; i--)
 							{
 								if (!num(wff[i]))
 								{
 									oper(wff[i]);
 								}
 							}
 							int ans = Q.top();
 							Q.pop();
 							if (!ans)
 							{
 								flag = false;
 								break;
 							}
 						}
 						if (!flag)
 						{
 							break;
 						}
 					}
 					if (!flag)
 					{
 						break;
 					}
 				}
 				if (!flag)
 				{
 					break;
 				}
 			}
 			if (!flag)
 			{
 				break;
 			}
 		}
 
 		if (flag)
 		{
 			cout << "tautology" << endl;
 		}
 		else
 		{
 			cout << "not" << endl;
 		}
 
 
 	}
 
 
 	return 0;
 
 }

[Waterloo Local Contest]: http://poj.org/searchproblem?field=source&key=Waterloo+Local+Contest