#include <stdio.h>
#include <string.h>   /* for all the new-fangled string functions */
#include <stdlib.h>     /* malloc, free, rand */


const int Fsize=50;
int no_edges;
int no_nodes;
int i;
const int cases=10;


int evalAtomic(char *nm, int edges[no_edges][2], int size, int V[3]);
int flip(int i);
int evalBin(char *nm, int edges[no_edges][2], int size, int V[3]);
int evalExist(char *nm, int edges[no_edges][2], int size, int V[3]);
int evalUni(char *nm, int edges[no_edges][2], int size, int V[3]);
int varToNum(char *nm);

int parse(char *g){
        /* return 1 if atomic, 2 if  neg, 3 if binary, 4 if exists, 5 if for all, ow 0*/
        char *temp = g;
        switch (*g) {
        case 'X':
                //Atomic
                temp++;
                if(!(*temp=='[')) {
                        return 0;
                }
                temp++;
                if(!(*temp=='x' || *temp=='y' || *temp=='z')) {
                        return 0;
                }
                temp++;
                if(!(*temp=='x' || *temp=='y' || *temp=='z')) {
                        return 0;
                }
                temp++;
                if(!(*temp==']')) {
                        return 0;
                }
                return 1;
                break;
        case '-':
                //Negated
                temp++;
                if(*temp != '\n') {
                        if(parse(temp)!=0) {
                                return 2;
                        }
                }
                break;
        case '(':
                //Binary connective
                temp++;
                if(*temp!='\n') {
                        if(parse(temp)!=0) {
                                // find the > v or ^
                                while(*temp!='^' && *temp != '>' && *temp != 'v') {
                                        temp++;
                                        if(*temp == ')' || *temp == '\n') {
                                                return 0;
                                        }
                                }
                                //binary connector here
                                temp++;
                                if(parse(temp)!=0) {
                                        //find the end bracket
                                        while(*temp!=')') {
                                                temp++;
                                                if(*temp=='\n') {
                                                        return 0;
                                                }
                                        }
                                        //valid here
                                        return 3;
                                }
                        }
                }
                break;
        case 'E':
                // Existential
                temp++;
                if(*temp != '\n') {
                        if(*temp == 'x' || *temp == 'y' || *temp == 'z') {
                                temp++;
                                if(*temp != '\n') {
                                        if(parse(temp)!=0) {
                                                return 4;
                                        }
                                }
                        }
                }
                break;
        case 'A':
                //Universal
                temp++;
                if(*temp!='\n') {
                        if((*temp=='x' || *temp=='y' || *temp=='z')) {
                                temp++;
                                if(parse(temp)!=0) {
                                        return 5;
                                }
                        }
                }
                break;
        default:
                return 0;
        }
        return 0;
}

int eval(char *nm, int edges[no_edges][2], int size, int V[3]){
        /* returns 1 if formla nm evaluates to true in graph with 'size' nodes, no_edges edges, edges stored in 'edges', variable assignment V.  Otherwise returns 0.*/
        switch(parse(nm)) {
        case 1:
                //Atomic
                nm +=2;
                return evalAtomic(nm, edges, size, V);
        case 2:
                //Negated
                nm++;
                return flip( eval(nm, edges, size, V));
        case 3:
                //Binary Connective
                nm++;
                return evalBin(nm, edges, size, V);
        case 4:
                //Existential
                nm++;
                return evalExist(nm, edges, size, V);
        case 5:
                //Universal
                nm++;
                return evalUni(nm, edges, size, V);
        }
        return 0;
}

int evalAtomic(char *nm, int edges[no_edges][2], int size, int V[3] ){
        int firstNode = -1;
        int secondNode = -1;

        firstNode = varToNum(nm);
        secondNode = varToNum(++nm);

        if(firstNode == -1 || secondNode ==-1) {
                return 0;
        }
        for(i = 0; i<no_edges; i++) {
                if( edges[i][0]==V[firstNode]  ) {
                        if(edges[i][1]==V[secondNode]) {
                                return 1;
                        }
                }
        }
        return 0;
}

int flip(int i){
        if(i==0) {
                return 1;
        }else{
                return 0;
        }
}

int evalBin(char *nm, int edges[no_edges][2], int size, int V[3]){
        int firstPart;
        int secondPart;
        char binCon;

        firstPart = eval(nm, edges, size, V);

        while(*nm!='^' && *nm != '>' && *nm != 'v') {
                nm++;
        }
        binCon = *(nm++);

        secondPart = eval(nm, edges, size, V);
        switch(binCon) {
        case 'v':
                //OR
                return (firstPart || secondPart);
        case '^':
                //AND
                return (firstPart && secondPart);
        case '>':
                //IMPLIES
                return ((!firstPart) || secondPart);
        }
        return 0;
}

int evalExist(char *nm, int edges[no_edges][2], int size, int V[3] ){
        int boundVar = varToNum(nm);
        int i;
        nm++;
        for(i = 0; i<no_edges; i++) {
                V[boundVar] = i;
                if(eval( nm, edges, size, V)==1) {
                        return 1;
                }
        }
        return 0;
}

int evalUni(char *nm, int edges[no_edges][2], int size, int V[3]  ){
        int boundVar = varToNum(nm);
        int i;
        nm++;
        for(i = 0; i<size; i++) {
                V[boundVar] = i;
                if(eval( nm, edges, size, V)==0) {
                        return 0;
                }
        }
        return 1;
}

int varToNum(char *nm){
        if(*nm == 'x') {
                return 0;
        } else if(*nm == 'y') {
                return 1;
        } else if(*nm == 'z' ) {
                return 2;
        }
        return -1;
}

int main()
{
  char *name=malloc(Fsize); /*create space for the formula*/
  FILE *fp, *fpout;

  /* reads from input.txt, writes to output.txt*/
 if ((  fp=fopen("input.txt","r"))==NULL){printf("Error opening file");exit(1);}
  if ((  fpout=fopen("output.txt","w"))==NULL){printf("Error opening file");exit(1);}

  int j;
  for(j=0;j<cases;j++)
    {
      fscanf(fp, "%s %d %d",name,&no_nodes,&no_edges);/*read number of nodes, number of edges*/
      int edges[no_edges][2];  /*Store edges in 2D array*/
      for(i=0;i<no_edges;i++)	 fscanf(fp, "%d%d", &edges[i][0], &edges[i][1]);/*read all the edges*/

      /*Assign variables x, y, z to nodes */
      int W[3];
      /*Store variable values in array
	value of x in V[0]
	value of y in V[1]
	value of z in V[2] */
      for(i=0;i<3;i++)  fscanf(fp, "%d", &W[i]);
      int p=parse(name);
      switch(p)
	{case 0:fprintf(fpout,"%s is not a formula.  ", name);break;
	case 1: fprintf(fpout,"%s is an atomic formula.  ",name);break;
	case 2: fprintf(fpout,"%s is a negated formula.  ",name);break;
	case 3: fprintf(fpout,"%s is a binary connective formula.  ", name);break;
	case 4: fprintf(fpout,"%s is an existential formula.  ",name);break;
	case 5: fprintf(fpout,"%s is a universal formula.  ",name);break;
	default: fprintf(fpout,"%s is not a formula.  ",name);break;
	}

      /*Now check if formula is true in the graph with given variable assignment. */
      if (parse(name)!=0){
	if (eval(name, edges, no_nodes,  W)==1)	fprintf(fpout,"The formula %s is true in G under W\n", name);
	else fprintf(fpout,"The formula %s is false in G under W\n", name);
      }
    }



  fclose(fp);
  fclose(fpout);
  free(name);
  return(0);
}