// Massingill, Berna L.
// With Modifications By:  Oldham, Jeffrey D.
// Sometime
// CS1321

// Tautology checker.

// Input:
//
//   A boolean expression, read from standard input (terminated by
//   EOF), in postfix notation.  Terms are separated by whitespace,
//   and each term is either an operator (&&, ||, !, =>, or ==), a
//   constant (true or false), or a variable name (anything other 
//   than an operator or a constant).
//
//   A boolean expression falls into one of three categories:
//     A tautology (well-formed, and true for all possible assignments
//       of true/false values to variables).
//     Not a tautology (well-formed, but false for at least one
//       assignment of true/false values to variables).
//     Not well-formed.
//
// Output:
//
//   A message to standard output indicating whether the input
//   expression is a tautology, not a tautology, or not well-formed.

#include <iostream>
#include <assert.h>		// has assert()
#include <stdlib.h>		// has EXIT_SUCCESS, EXIT_FAILURE

#include <vector>
#include <string>
#include <map>

// DO NOT DISTRIBUTE.
#include "stack.h"
// end of DO NOT DISTRIBUTE.

typedef vector<string> expr;
typedef pair<bool, bool> twobools;

// An instance of this class represents a boolean expression in
// reverse Polish notation, together with an assignment of values
// to variables.
class ExpressionSubstitution {
public:
  // typedef vector<string> expr;

  ExpressionSubstitution(istream& in) {
    // Read the expression.
    string next;
    while (in >> next)
      e.push_back(next);

    // Prepare initial variable values.
    findVariables();
    noMoreValues = false;
    return;
  }

  // Reset to first assignment of values to variables.
  void reset(void) {
    resetVariables();
    noMoreValues = false;
    return;
  }

  // Obtain the "next" expression generated by assigning values to
  // all variables in the original expression.  Repeated calls to
  // this function cycle through all possible assignments of values
  // to variables, returning true as long as there are more possible
  // assignments, false if all have been used. 
  bool getNext(expr & subst)
  {
    if (noMoreValues)
      return false;

    subst.clear();
    for (expr::const_iterator ePos = e.begin();
	 ePos != e.end();
	 ++ePos)
      if (isKeyword(*ePos))
	subst.push_back(*ePos);
      else 
	{
	  assert(a.find(*ePos) != a.end());
	  subst.push_back((a.find(*ePos))->second ? "true" : "false");
	}
    // Set up for next call.
    noMoreValues = !nextAssignment();
    return true;
  }

  // Determine whether token is a keyword (operator or constant).
  static bool isKeyword(const string & s)
  {
    return (s == "&&" || s == "||" || s == "!" || s == "=>" || 
	    s == "==" ||
	    s == "true" || s == "false");
  }
private:
  expr e;			// expression with variables
  typedef map<string, bool> assignment;
  assignment a;
  bool noMoreValues;

  // Create map from variables in e -- variables are keywords, values
  //   are all initially false.
  void findVariables(void) {
    for (expr::const_iterator ePos = e.begin();
	 ePos != e.end();
	 ++ePos)
      if (!isKeyword(*ePos))
	a[(*ePos)] = false;
    return;
  }

  // Reset map to initial values.
  void resetVariables(void) {
    for (assignment::iterator aPos = a.begin();
	 aPos != a.end();
	 ++aPos)
      aPos->second = false;
  }

  // Generate next assignment.  Treat sequence of values as a binary
  //   number, and add one.  Returns true if there is one (no overflow),
  //   false if not.
  bool nextAssignment(void)
  {
    bool carry = true;
    for (assignment::iterator aPos = a.begin();
	 aPos != a.end() && carry;
	 ++aPos)
      if (aPos->second == false)
	{
	  aPos->second = true;
	  carry = false;
	}
      else
	{
	  aPos->second = false;
	  carry = true;
	}
    return carry == false;
  }
};


// ---- Function prototypes. ----
twobools evaluate(const expr & e);
// DO NOT DISTRIBUTE.
bool doUnaryOp(stack<bool> & s, const string & op);
bool doBinaryOp(stack<bool> & s, const string & op);
// end of DO NOT DISTRIBUTE.

// ---- Main program. ----

int main(void)
{
  cout << "Enter the expression to evaluate "
    "(multiple lines okay, control-D to end):\n";

  ExpressionSubstitution e(cin); // construct expression from input
  twobools evalResult = twobools(true,true);
				// result of evaluating expression --
				//   first bool is well-formedness,
				//   second is expression's value.
  expr eWithValues;

  // Evaluate expression for all possible assignments, stopping
  //   if one returns a false result or a not-well-formed result.
  // (Member function getNext() cycles through possible assignments,
  //   returning false when there are no more.)

  while (evalResult.first && evalResult.second && 
	 e.getNext(eWithValues))
    evalResult = evaluate(eWithValues);
  
  if (!evalResult.first)
    cout << "Input expression is not well-formed.\n";
  else if (!evalResult.second)
    cout << "Input expression is not a tautology.\n";
  else
    cout << "Input expression is a tautology.\n";
  return EXIT_SUCCESS;
}

// ---- Function definitions. ----

// DO NOT DISTRIBUTE.

// Apply unary operator to stack:
// If stack has at least one element, remove top element, apply
//   operator to it, push result onto stack, and return "true"
//   (expression well-formed).
// Otherwise return "false" (expression not well-formed).
bool doUnaryOp(stack<bool> & s, const string & op)
{
  if (s.size() < 1)
    return false;
  bool e1 = s.top();
  s.pop();
  if (op == "!")
      s.push(!e1);
  else
    assert(false);
  return true;
}

// Apply binary operator to stack:
// If stack has at least two elements, remove top two elements,
//   combine with operator, push result onto stack, and return 
//   "true" (expression well-formed).
// Otherwise return "false" (expression not well-formed).
bool doBinaryOp(stack<bool> & s, const string & op)
{
  if (s.size() < 2)
    return false;
  bool e2 = s.top();
  s.pop();
  bool e1 = s.top();
  s.pop();
  if (op == "&&")
    s.push(e1 && e2);
  else if (op == "||")
    s.push(e1 || e2);
  else if (op == "=>")
    s.push(!e1 || e2);
  else if (op == "==")
    s.push(e1 == e2);
  else
    assert(false);
  return true;
}

// Evaluate expression consisting of keywords (operators, "true",
//   "false").  Return value is (well-formed, expression-value).
twobools evaluate(const expr & e)
{
  // Debug print.
#ifdef DEBUG
  cerr << "Evaluating expression:  ";
  for (expr::const_iterator pos = e.begin();
       pos != e.end();
       ++pos)
    cerr << (*pos) << " ";
  cerr << endl;
#endif

  stack<bool> s;
  bool wellFormed = true;
  for (expr::const_iterator ePos = e.begin();
       ePos != e.end() && wellFormed;
       ++ePos)
    {
      assert (ExpressionSubstitution::isKeyword(*ePos));
      if ((*ePos) == "true")
	s.push(true);
      else if ((*ePos) == "false")
	s.push(false);
      else if ((*ePos) == "!")
	wellFormed = doUnaryOp(s, "!");
      else
	wellFormed = doBinaryOp(s, (*ePos));
    }
  wellFormed = wellFormed && (s.size() == 1);
  if (wellFormed)
    return twobools(true, s.top());
  else
    return twobools(false, false);
}

// end of DO NOT DISTRIBUTE.