Tautology POJ - 3295

题目链接：https://vjudge.net/problem/POJ-3295

题意： p , q , r , s , t p,q,r,s,t p,q,r,s,t都是公式里的变量， K , A , N , C , E K,A,N,C,E K,A,N,C,E是运算符。分别代表 a n d , o r , n o t , i m p l i e s , e q u a l and,or,not,implies,equal and,or,not,implies,equal运算。运算符真值表如下。

p , q , r , s , t p,q,r,s,t p,q,r,s,t是公式
如果 w w w是公式,则 N w Nw Nw也是公式
如果 w , x w,x w,x是公式，则 K w x , A w x , C w x , E w x Kwx,Awx,Cwx,Ewx Kwx,Awx,Cwx,Ewx也是公式。
如果一个公式的逻辑值恒为1，这称这个公式为 t a u t o l o g y tautology tautology。

问题：现在给你一个公式，请你判断它是不是 t a u t o l o g y tautology tautology.

思路：构造法，用栈模拟这个运算过程，算法步骤具体如下：
枚举p,q,r,s,t的取值，复杂度 2 5 2^5 25。

对于每一种取值，从字符串尾部向前遍历，遇到一个字符，如果是遍历，则入栈。如果是运算符，则根据具体的运算符规则操作。（如果是双目运算符，将头两个元素出栈，并作相关运算，将结果压入栈；单目出栈一个，做运算，将结果压入栈）
这样运算到最后栈顶的元素就是运算结果。(你也许需要定义’T’,'F’来在栈中表示1和0)
那么每一种结果都为真，则为 t a u t o l o g y tautology tautology。否则 n o t not not

具体见代码：

#include<iostream>
#include<stack>
#include<cmath>
using namespace std;
//栈模拟运算。
stack<char>stk;
bool is_var(char c){
	if(c=='p'||c=='q'||c=='r'||c=='s'||c=='t'||c=='T'||c=='F'){
		return true;
	}
	else return false;
}
int bit[7];
int getvalue(char c){
	int res;
	if(c=='p')res=bit[1];
	else if(c=='q')res=bit[2];
	else if(c=='r')res=bit[3];
	else if(c=='s')res=bit[4];
	else if(c=='t')res=bit[5];
	else if(c=='T')res=1;
	else if(c=='F')res=0;
	return res;
}
int N(int x){
	int res=1-x;
	return res;
}
int C(int w,int x){
	int res;
	if(w==1&&x==1)res=1;
	else if(w==1&&x==0)res=0;
	else if(w==0&&x==1)res=1;
	else if(w==0&&x==0)res=1;
	return res;
}
int main(){
	string s;
	while(cin>>s){
		if(s=="0")break;
		int i,h;
		int flag=1;
		for(h=0;h<=pow(2,5)-1;h++)
		{
			while(!stk.empty())stk.pop();
			//to bit
			int tem=5;
			int hh=h;
			while(1){
				bit[tem]=hh&1;
				tem--;
				hh>>=1;
				if(tem==0)break;
			}
			//pqrst
//			p=bit[1];
//			q=bit[2];
//			r=bit[3];
//			s=bit[4];
//			t=bit[5];
			int len=s.size();
			for(i=len-1;i>=0;i--){
				//is variable 
				if(is_var(s[i])){
					stk.push(s[i]);
				}//is operator
				else{
					if(s[i]=='K'){
						char w=stk.top();
						stk.pop();
						char x=stk.top();
						stk.pop();
						int w1,x1;
						w1=getvalue(w);
						x1=getvalue(x);
						int ans=w1&x1;
						if(ans)stk.push('T');
						else stk.push('F'); 
					}
					if(s[i]=='A'){
						char w=stk.top();
						stk.pop();
						char x=stk.top();
						stk.pop();
						int w1,x1;
						w1=getvalue(w);
						x1=getvalue(x);
						int ans=w1|x1;
						if(ans)stk.push('T');
						else stk.push('F'); 
					}
					if(s[i]=='N'){
						char w=stk.top();
						stk.pop();
						int w1=getvalue(w);
						int ans=N(w1);
						if(ans)stk.push('T');
						else stk.push('F'); 
					}
					if(s[i]=='C'){
						char w=stk.top();
						stk.pop();
						char x=stk.top();
						stk.pop();
						int w1,x1;
						w1=getvalue(w);
						x1=getvalue(x);
						int ans=C(w1,x1);
						if(ans)stk.push('T');
						else stk.push('F'); 
					}
					if(s[i]=='E'){
						char w=stk.top();
						stk.pop();
						char x=stk.top();
						stk.pop();
						int w1,x1;
						w1=getvalue(w);
						x1=getvalue(x);
						int ans=(w1==x1);
						if(ans)stk.push('T');
						else stk.push('F'); 
					}
				}
			}
			//stk.top();
			int w=stk.top();
			int ans=getvalue(w);
			if(ans==0){
				flag=0;
				break;
			}
		}
		if(flag)cout<<"tautology\n";
		else cout<<"not\n";
	}
	return 0;
}