#include <iostream>
#include "formula.h"
#include "assignment.h"

using namespace std;


struct node
{
  char symbol;
  formula left;
  formula right;
};


formula new_formula(char symbol, formula left, formula right){
  formula f = new node;
  if (f!=NULL){
    f->symbol = symbol;
    f->left = left;
    f->right = right;
  }
  return f;
}

void delete_formula(formula f){
  if (f!=NULL){
    delete_formula(f->left);
    delete_formula(f->right);
  }
}


void print_formula(formula f){
  if (f!=NULL){
    cout << "(";
    print_formula(f->left);
    cout << f->symbol;
    print_formula(f->right);
    cout << ")";
  }
}

    
formula read_formula(){
  char symbol;
  formula left, right;
  cin >> symbol;
  switch(symbol){
  case '&':
  case '|':
    left = read_formula();
    right = read_formula();
    return new_formula(symbol, left, right);
  case '!':
    left = read_formula();
    return new_formula(symbol, left, NULL);
  default:
    if ((symbol >='a' && symbol <='z') || symbol=='0' || symbol=='1')
      return new_formula(symbol, NULL, NULL);
    else
      return NULL;
  }
}


retval simplify_onestep(formula &f){
  switch (f->symbol){
  case '&':
    if(f->left==NULL || f->right==NULL)
      return FAIL;
    else if(f->left->symbol=='0' || f->right->symbol=='0'){
      delete_formula(f->left);
      delete_formula(f->right);
      f->symbol = '0';
      f->left = NULL;
      f->right = NULL;
    } else if(f->left->symbol=='1'){
      delete f->left;
      formula right = f->right;
      delete f;
      f = right;
    } else if(f->right->symbol=='1'){
      delete f->right;
      formula left = f->left;
      delete f;
      f = left;
    }
    return OK;
  case '|':
    if(f->left==NULL || f->right==NULL)
      return FAIL;
    else if(f->left->symbol=='1' || f->right->symbol=='1'){
      delete_formula(f->left);
      delete_formula(f->right);
      f->symbol = '1';
      f->left = NULL;
      f->right = NULL;
    } else if(f->left->symbol=='0'){
      delete f->left;
      formula right = f->right;
      delete f;
      f = right;
    } else if(f->right->symbol=='0'){
      delete f->right;
      formula left = f->left;
      delete f;
      f = left;
    }
    return OK;
  case '!':
    if(f->left==NULL)
      return FAIL;
    else if(f->left->symbol=='1'){
      delete f->left;
      f->symbol = '0';
    } else if(f->left->symbol=='0'){
      delete f->left;
      f->symbol = '1';
    } 
    return OK;
  default:
    return OK;
  }
}

 
retval simplify(formula &f){
  retval r;
  if(f!=NULL){
    r = simplify(f->left);
    if (r==FAIL)
      return FAIL;
    r = simplify(f->left);
    if (r==FAIL)
      return FAIL;
    return simplify_onestep(f);
  } else
    return OK;
}


  
retval apply_assignment(formula &f, assignment a){
  retval r;
  if(f==NULL)
    return FAIL;
  switch (f->symbol){
  case '&':
  case '|':
    r = apply_assignment(f->left, a);
    if (r==FAIL)
      return FAIL;
    r = apply_assignment(f->right, a);
    if (r==FAIL)
      return FAIL;
    return OK;
    //return simplify_onestep(f);
  case '!':
    r = apply_assignment(f->left, a);
    if (r==FAIL)
      return FAIL;
    return OK;
    //return simplify_onestep(f);
  case '0':
  case '1':
    return OK;
  default:
    if (f->symbol >='a' && f->symbol <='z'){
      bool value;
      r = find(a, f->symbol, value);
      if (r!=FAIL){
	if (value)
	  f->symbol = '1';
	else
	  f->symbol = '0';
      }
      return OK;
    } else
      return FAIL;
  }
}