11108:Problem D: Tautology

問題文
http://uva.onlinejudge.org/external/111/11108.html

WFFという文法が与えられる。以下のようなものだ。
1.p,q,r,s,tはWFFである。
2.WFFである文字列をwとおくと、NwはWFFである。
3.WFFである文字列二つをw,xとおくと、Kwx,Awx,Cwx,EwxはWFFである。

1~3の文字列の操作は以下のルールに従う。
{p,q,r,s,t}=true,false
Kwx = w & x, Awx = w | x, Nw = !w
Cwx = !( w == true && x == false ), Ewx = ( w == x )

文字列が一行ずつ与えられる。その文字列に含まれるp,q,r,s,tがどのような値の取り方をしてもWFFが真になるならtautology,一つでも真にならないような値の取り方があるならnotを出力せよ。

構文解析+全探索。構文解析は書いてある通りにやるだけ。あとはビットでp,q,r,s,tそれぞれの値を決めて2^5回構文解析する。

#include<iostream>
#include<string>
#include<algorithm>
#include<cctype>
  
using namespace std;
  
int now,wwf;
string s;
  
bool rec(){
  if(now>=s.size())return true;
  if(isupper(s[now])){
    if(s[now]=='K'){
      now++;
      bool res1=rec();
      now++;
      bool res2=rec();
      return res1&res2;
    }
    else if(s[now]=='A'){
      now++;
      bool res1=rec();
      now++;
      bool res2=rec();
      return res1|res2;
    }
    else if(s[now]=='N'){
      now++;
      return !rec();
    }
    else if(s[now]=='C'){
      now++;
      bool w=rec();
      now++;
      bool x=rec();
      return !(w== true && x==false); 
    }
    else if(s[now]=='E'){
      now++;
      bool w=rec();
      now++;
      bool x=rec();
      return (w==x);
    }
  }
  else {
    if(s[now]=='p')return (wwf>>4)&1;
    if(s[now]=='q')return (wwf>>3)&1;
    if(s[now]=='r')return (wwf>>2)&1;
    if(s[now]=='s')return (wwf>>1)&1;
    if(s[now]=='t')return (wwf>>0)&1;
  }
}
  
int main(void){
  
  while(getline(cin,s)){
    if(s=="0")break;
    for(wwf=0;wwf<(1<<5);wwf++){
      now=0;
      if(!rec()){
    cout << "not" << endl;
    goto end;
      }
    }
    cout << "tautology" << endl;
  end:;
  }
  
  return 0;
}