Tautology---poj3295（枚举）

#include<iostream>
#include<stdio.h>
#include<string.h>
#include<string>
#include<vector>
#include<algorithm>
#include<map>
#include<queue>
#include<stack>

using namespace std;

#define met(a, b) memset(a, b, sizeof(a))
#define N 111

typedef long long LL;

int p, q, r, s, t, len;
char str[N];

bool Judge()
{
    stack<int> Sta;
    for(int i=len-1; i>=0; i--)
    {
        int x1, x2;
        if(str[i] == ‘p‘)Sta.push(p);
        else if(str[i] == ‘q‘)Sta.push(q);
        else if(str[i] == ‘r‘)Sta.push(r);
        else if(str[i] == ‘s‘)Sta.push(s);
        else if(str[i] == ‘t‘)Sta.push(t);
        else if(str[i] == ‘K‘)
        {
            x1 = Sta.top();Sta.pop();
            x2 = Sta.top();Sta.pop();
            Sta.push(x1&&x2);
        }
        else if(str[i] == ‘A‘)
        {
            x1 = Sta.top();Sta.pop();
            x2 = Sta.top();Sta.pop();
            Sta.push(x1||x2);
        }
        else if(str[i] == ‘N‘)
        {
            x1 = Sta.top();Sta.pop();
            Sta.push(!x1);
        }
        else if(str[i] == ‘C‘)
        {
            x1 = Sta.top();Sta.pop();
            x2 = Sta.top();Sta.pop();
            Sta.push( !(x1&&!x2) );
        }
        else
        {
            x1 = Sta.top();Sta.pop();
            x2 = Sta.top();Sta.pop();
            Sta.push( x1==x2 );
        }
    }
    return Sta.top()==1;
}

bool solve()
{
    len = strlen(str);

    for(p=0; p<2; p++)
    for(q=0; q<2; q++)
    for(r=0; r<2; r++)
    for(s=0; s<2; s++)
    for(t=0; t<2; t++)
        if(!Judge())
            return false;
    return true;
}

int main()
{
    while(scanf("%s", str), strcmp(str, "0"))
    {
        if(solve())puts("tautology");
        else puts("not");
    }
    return 0;
}