POJ 3295 Tautology （构造法）

Tautology Time Limit: 1000MS   Memory Limit: 65536K Total Submissions: 7716   Accepted: 2935 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, Nw is a WFF if w and x are WFFs, Kwx, Awx, Cwx, and Ewx 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. Definitions of K, A, N, C, and E      w  x   Kwx   Awx    Nw   Cwx   Ewx   1  1   1   1    0   1   1   1  0   0   1    0   0   0   0  1   0   1    1   1   0   0  0   0   0    1   1   1 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

题意：K  A  N  C  E 分别代表了不同的运算符，然后用栈模拟即可，，，构造法。。。。。。。。。。。。

#include<iostream>
#include<cstdio>
#include<stack>
#include<cstring>

using namespace std;

const int N=;

char str[N];
int p,q,r,s,t;
stack<int> st;

int isvariables(char ch){
    switch(ch){
        case 'p':st.push(p);return ;
        case 'q':st.push(q);return ;
        case 'r':st.push(r);return ;
        case 's':st.push(s);return ;
        case 't':st.push(t);return ;
    }
    return ;
}

void operators(char op){
    switch(op){
        case 'K':{
            int x=st.top(); st.pop();
            int y=st.top(); st.pop();
            st.push(x && y);
        }break;
        case 'A':{
            int x=st.top(); st.pop();
            int y=st.top(); st.pop();
            st.push(x || y);
        }break;
        case 'N':{
            int x=st.top(); st.pop();
            st.push(!x);
        }break;
        case 'C':{
            int x=st.top(); st.pop();
            int y=st.top(); st.pop();
            st.push((!x) || y);
        }break;
        case 'E':{
            int x=st.top(); st.pop();
            int y=st.top(); st.pop();
            st.push(x==y);
        }break;
    }
}

int main(){

    //freopen("input.txt","r",stdin);

    while(~scanf("%s",str) && str[]!=''){
        int len=strlen(str);
        int flag=;
        for(p=;p<= && flag;p++)
            for(q=;q<= && flag;q++)
                for(r=;r<= && flag;r++)
                    for(s=;s<= && flag;s++)
                        for(t=;t<= && flag;t++){
                            for(int i=len-;i>=;i--)
                                if(!isvariables(str[i]))
                                    operators(str[i]);
                            int last=st.top();
                            st.pop();
                            if(last==)
                                flag=;
                        }
        if(flag)
            printf("tautology\n");
        else
            printf("not\n");
    }
    return ;
}