// file:    TautologyChecker.java
// author:  Robert Keller
// purpose: Check logical expressions for being tautologies or not
//          Logical expressions are read one per input line.  An expression
//          is first parsed into a LogicTree, then checked for being a
//          tautology using the isTautology method of class LogicTree.

import java.io.*;

class TautologyChecker
{
/**
 * The main program for the tautology checker.  Most of the work is
 * done in LogicTree.
 */

public static void main(String arg[])
  {
  BufferedReader reader = new BufferedReader(new InputStreamReader(System.in));

  String expressionRead;  // The line of input read

  try
    {
    // Read the next line, continuing the loop only if not end-of-file.

    while( (expressionRead = reader.readLine()) != null )
      {
      // Create a parser for the line read.

      LogicParser parser = new LogicParser(expressionRead);


      // Parse the input.

      LogicTree tree = parser.parse();

      if( tree.isFailure() )
        {
        System.out.println("\nExpression " + expressionRead 
                         + " has an error " + ((Failure)tree).getCause()
                         + " at " + ((Failure)tree).getResidual());
        }
      else
        {
        if( tree.isTautology() )
          {
          System.out.println("\nExpression " + expressionRead 
                           + " is a tautology");
          }
        else
          {
          System.out.println("\nExpression " + expressionRead
                          + " is not a tautology");
          }
        }
      }
    }
  catch( IOException e )
    {
    System.out.println("IOException caught: " + e);
    }
  }
}