[POJ3295]Tautology

Posted 2020-08-21

?????????symbols   determine   min   table   scan   input   name   oss   turn   

[POJ3295]Tautology

????????????

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 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.

??????

For each test case, output a line containing tautology or not as appropriate.

????????????

ApNp
ApNq
0

????????????

tautology
not

?????????????????????

???????????????

??????

?????? p, q, r, s, t ????????????????????????????????????????????????????????????????????????????????????tautology??????????????????not??????

#include <iostream>
#include <cstdio>
#include <algorithm>
#include <cmath>
#include <stack>
#include <vector>
#include <queue>
#include <cstring>
#include <string>
#include <map>
#include <set>
using namespace std;

#define maxn 110
#define maxal 300
char S[maxn];
int ord[maxal];
bool val[10];

struct Info {
	int p, v;
	Info() {}
	Info(int _, int __): p(_), v(__) {}
} ;
Info check(int l) {
	if(islower(S[l])) return Info(l + 1, val[ord[S[l]]]);
	if(S[l] == ???N???) {
		Info t;
		t = check(l + 1);
		return Info(t.p, t.v ^ 1);
	}
	if(S[l] == ???K???) {
		Info t, t2;
		t = check(l + 1);
		t2 = check(t.p);
		return Info(t2.p, t.v & t2.v);
	}
	if(S[l] == ???A???) {
		Info t, t2;
		t = check(l + 1);
		t2 = check(t.p);
		return Info(t2.p, t.v | t2.v);
	}
	if(S[l] == ???C???) {
		Info t, t2;
		t = check(l + 1);
		t2 = check(t.p);
		return Info(t2.p, (t.v && !t2.v) ? 0 : 1);
	}
	if(S[l] == ???E???) {
		Info t, t2;
		t = check(l + 1);
		t2 = check(t.p);
		return Info(t2.p, t.v == t2.v);
	}
	return Info(0, 0);
}

int main() {
	ord[???p???] = 0;
	ord[???q???] = 1;
	ord[???r???] = 2;
	ord[???s???] = 3;
	ord[???t???] = 4;
	while(scanf("%s", S + 1) == 1) {
		int all = (1 << 5) - 1, n = strlen(S + 1);
		if(n == 1 && S[1] == ???0???) break;
		bool ok = 1;
		for(int i = 0; i <= all; i++) {
			for(int j = 0; j < 5; j++)
				val[j] = (i >> j & 1);
			if(!check(1).v){ ok = 0; break; }
		}
		puts(ok ? "tautology" : "not");
	}
	
	return 0;
}