poj3295 http://poj.org/problem?id=3295

//  ：
//5   ( 0||1) 32                            
//       
//k->x&&y
//A->x||y
//N->!x
//implies->(!x)||y
//E->x==y;
#include<iostream>
#include<string.h>
#include<stdio.h>
#include<stack>
using namespace std;
stack<int>  tem;
string test;
char map[6];
int p,q,r,s,t;
int pp,qq,rr,ss,tt;
int judge(char ch)
{
    switch(ch)
    {
    case  'p':
        tem.push(pp);
        return 1;
    case  'q':
        tem.push(qq);
        return 1;
    case 'r':
        tem.push(rr);
        return 1;
    case 's':
        tem.push(ss);
        return 1;
    case 't':
        tem.push(tt);
        return 1;
    }
    return 0;
}
void res(char ch)
{
    int a,b;
    switch(ch)
    {
    case 'K':
        a=tem.top();
        tem.pop();
        b=tem.top();
        tem.pop();
        tem.push(a&&b);
        break;
    case 'A':
        a=tem.top();
        tem.pop();
        b=tem.top();
        tem.pop();
        tem.push(a||b);
        break;
    case 'N':
        a=tem.top();
        tem.pop();
        tem.push(!a);
        break;
    case 'C':
        a=tem.top();
        tem.pop();
        b=tem.top();
        tem.pop();
        tem.push((!a)||b);
        break;
    case 'E':
        a=tem.top();
        tem.pop();
        b=tem.top();
        tem.pop();
        tem.push(a==b);
        break;
    }

}
int main()
{
    int flag;
    while(getline(cin,test))
    {
        if(test[0]=='0') break;
        flag=1;
        p=q=r=s=t=1;
        for(int i=0;i<5;i++)
          map[i]=0;
        for(int i=0; i<test.size(); i++)
        {
            if(test[i]=='p'&&p)
            {
                map[0]=1;
                p=0;
            }
            else if(test[i]=='q'&&q)
            {
                map[1]=1;
                q=0;
            }
            else if(test[i]=='r'&&r)
            {
                map[2]=1;
                r=0;
            }
            else if(test[i]=='s'&&s)
            {
                map[3]=1;
                s=0;
            }
            else if(test[i]=='t'&&t)
            {
                map[4]=1;
                t=0;
            }
        }
       // printf("%d %d %d %d
",q,r,s,t);
        for( pp=p; pp<=1&&flag!=-1; pp++)
            for( qq=q; qq<=1&&flag!=-1; qq++)
                for( rr=r; rr<=1&&flag!=-1; rr++)
                    for( ss=s; ss<=1&&flag!=-1; ss++)
                        for( tt=t; tt<=1&&flag!=-1; tt++)
                        {
                         //   printf("fsdf
");
                            for(int i=test.size()-1; i>=0&&flag!=-1; i--)
                            {
                                if(!judge(test[i]))
                                    res(test[i]);
                            }
                        //  printf("tem=%d
",tem.top());
                            flag=tem.top()-1;
                          //  printf("flag=%d
",flag);
                            tem.pop();
                        }
        if(flag!=-1)
            printf("tautology
");
        else
            printf("not
");
    }
    return 0;
}