// file:    LogicTree.java
// author:  Robert Keller
// purpose: A class for representing syntax trees for logic expressions

/**
 * A LogicTree represents the syntax of a propositional logic expression.
 * It includes provisions for checking whether the tree is a tautology.
 * Here we use the Boole-Shannon expansion technique, implemented as an
 * "object-oriented" method which virtually substitutes values for variables.
 */

abstract class LogicTree
{
/**
 * C0 is a tree for the constant 0 (false).
 */

static LogicTree C0 = new False();


/**
 * C1 is a tree for the constant 1 (true).
 */

static LogicTree C1 = new True();


/**
 * additionalIndentation determines how much additional Indentation there
 * is at each level of the tree when it is converted to a String.
 */

static String additionalIndentation = " ";


/**
 * Convert the tree to a String representation.
 */

public String toString()
  {
  StringBuffer buffer = new StringBuffer();  
  toStringBuffer("", buffer);
  return buffer.toString();
  }


/**
 * Put the tree's representation into a StringBuffer.
 */

abstract public void toStringBuffer(String indentation, StringBuffer buffer);



/**
 * Tell whether this tree is a failure.
 */

public boolean isFailure()
  {
  return this instanceof Failure;
  }


/**
 * pseudo-constructor for an "iff" tree
 */

public static LogicTree iff(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  return new Iff(leftSubtree, rightSubtree);
  }


/**
 * pseudo-constructor for an "implies" tree
 */

public static LogicTree implies(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  return new Implies(leftSubtree, rightSubtree);
  }


/**
 * pseudo-constructor for an "or" tree
 */

public static LogicTree or(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  return new Or(leftSubtree, rightSubtree);
  }


/**
 * pseudo-constructor for an "and" tree
 */

public static LogicTree and(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  return new And(leftSubtree, rightSubtree);
  }


/**
 * pseudo-constructor for a "not" tree
 */

public static LogicTree not(LogicTree subtree)
  {
  return new Not(subtree);
  }


/**
 * pseudo-constructor for a logical variable
 */

public static LogicTree var(char name)
  {
  return new Var(name);
  }


/**
 * pseudo-constructor for a failure
 */

public static LogicTree failure(String cause)
  {
  return new Failure(cause);
  }


/**
 * Get an unbound variable from this tree, returing null if there is none.
 */

abstract Var getVar();


/**
 * Bind the variable to the indicated boolean value.
 */

abstract void bind(Var var, boolean value);


/**
 * Unbind the variable.
 */

abstract void unbind(Var var);


/**
 * Evaluate the tree.  This should only be called if the tree has no
 * unbound variables.  It is meaningless otherwise.
 */

abstract boolean eval();


/**
 * Check whether the tree is a tautology or not.
 */

boolean isTautology()
  {
  Var var = getVar();		// Get an unbound variable, if any.
  if( var == null )
    {
    return eval();		// If no variable, determine by direct evaluation.
    }
  else
    {
    bind(var, false);		// Try the expression, substituting false for var.
    boolean V0 = isTautology();

    if( !V0 )
      {
      unbind(var);		// E0 is not a tautology
      return false;
      }

    bind(var, true);		// E0 is a tautology
    boolean V1 = isTautology();	// Try the expression, substituting true for var.
    unbind(var);

    return V1;
    }
  }
}


/**
 * a logic tree with a generic binary operator
 */

class BinaryTree extends LogicTree
{
/**
 * the operator
 */

String op;

/**
 * the left subtree of this tree
 */

LogicTree leftSubtree;


/**
 * the right subtree of this tree
 */

LogicTree rightSubtree;


/**
 * Construct a logic tree with a generic binary operator.
 */

BinaryTree(String op, LogicTree leftSubtree, LogicTree rightSubtree)
  {
  this.op           = op;
  this.leftSubtree  = leftSubtree;
  this.rightSubtree = rightSubtree;
  }


/**
 * Get an unbound variable from this tree, returing null if there is none.
 */

Var getVar()
  {
  Var leftVar = leftSubtree.getVar();
  if( leftVar == null )
    {
    return rightSubtree.getVar();
    }
  return leftVar;
  }


/**
 * Bind the variable to the indicated boolean value.
 */

void bind(Var var, boolean value)
  {
  leftSubtree.bind(var, value);
  rightSubtree.bind(var, value);
  }


/**
 * Unbind the variable.
 */

void unbind(Var var)
  {
  leftSubtree.unbind(var);
  rightSubtree.unbind(var);
  }


/**
 * Evaluate the tree.  This method is intended to be over-ridden
 * in derived trees.
 */

boolean eval()
  {
  return false;
  }

public void toStringBuffer(String indentation, StringBuffer buffer)
  {
  buffer.append(indentation);
  buffer.append(op);
  buffer.append("\n"); 
  leftSubtree.toStringBuffer(indentation + additionalIndentation, buffer);
  rightSubtree.toStringBuffer(indentation + additionalIndentation, buffer);
  }
}


/**
 * a logic tree with a generic unary operator
 */

class UnaryTree extends LogicTree
{
/**
 * the operator
 */

String op;


/**
 * the one subtree of this tree
 */

LogicTree subtree;


/**
 * Construct a logic tree with a generic unary operator.
 */

UnaryTree(String op, LogicTree subtree)
  {
  this.op       = op;
  this.subtree  = subtree;
  }


/**
 * Get an unbound variable from this tree, returing null if there is none.
 */

Var getVar()
  {
  return subtree.getVar();
  }


/**
 * Bind the variable to the indicated boolean value.
 */

void bind(Var var, boolean value)
  {
  subtree.bind(var, value);
  }


/**
 * Unbind the variable.
 */

void unbind(Var var)
  {
  subtree.unbind(var);
  }


/**
 * Evaluate the tree.  This method is intended to be over-ridden
 * in derived trees.
 */

boolean eval()
  {
  return false;
  }


public void toStringBuffer(String indentation, StringBuffer buffer)
  {
  buffer.append(indentation);
  buffer.append(op);
  buffer.append("\n"); 
  subtree.toStringBuffer(indentation + additionalIndentation, buffer);
  }
}


/**
 * a LogicTree tree that is a leaf, either a constant or variable
 */

class Unit extends LogicTree
{
/**
 * the representation of this leaf as a string
 */

String value;


/**
 * construct a leaf
 */

Unit(String value)
  {
  this.value = value;
  }


/**
 * Get an unbound variable from this tree, returing null if there is none.
 * This method serves as a default and will be over-ridden in selected
 * derived classes.
 */

Var getVar()
  {
  return null;
  }


/**
 * Bind the variable to the indicated boolean value.
 * This method will be over-ridden in selected derived classes.
 */

void bind(Var var, boolean value)
  {
  }


/**
 * Unbind the variable.
 * This method will be over-ridden in selected derived classes.
 */

void unbind(Var var)
  {
  }


/**
 * Evaluate the tree.  This method is intended to be over-ridden
 * in derived trees.
 */

boolean eval()
  {
  return false;
  }


public void toStringBuffer(String indentation, StringBuffer buffer)
  {
  buffer.append(indentation);
  buffer.append(value);
  buffer.append("\n"); 
  }
}



/**
 * a LogicTree tree representing the result of illegal input
 */

class Failure extends LogicTree
{
/**
 * description of the cause of failure
 */

String cause;

String residual;


/**
 * Construct a failure indicator from a cause.
 */

Failure(String cause)
  {
  this(cause, null);
  }


/**
 * Construct a failure indicator from a cause and a residual input.
 */

Failure(String cause, String residual)
  {
  this.cause    = cause;
  this.residual = residual;
  }


/**
 * dummy method
 */

Var getVar()
  {
  return null;
  }


/**
 * dummy method
 */

void bind(Var var, boolean value)
  {
  }


/**
 * dummy method
 */

void unbind(Var var)
  {
  }


/**
 * dummy method
 */

boolean eval()
  {
  return false;
  }

public void toStringBuffer(String indentation, StringBuffer buffer)
  {
  buffer.append(indentation);
  buffer.append("*** error: " + cause);
  buffer.append("\n"); 

  if( buffer != null )
    {
    buffer.append("*** starting at: "); 
    buffer.append(residual);
    buffer.append("\n"); 
    }
  }


/**
 * Return a String indicating the cause of failure.
 */

public String getCause()
  {
  return cause;
  }


/**
 * Return a String indicating the residual input after a failure.
 */

public String getResidual()
  {
  return residual;
  }
}


/**
 * a LogicTree tree with an "=" operator and two subtrees
 */

class Iff extends BinaryTree
{
Iff(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  super("=", leftSubtree, rightSubtree);
  }


/**
 * Evaluate the tree.  This should only be called if the tree has no
 * unbound variable.  It is meaningless otherwise.
 * The result is true iff the results of evaluating the two sub-trees 
 * are equal.
 */

boolean eval()
  {
  return leftSubtree.eval() == rightSubtree.eval();
  }

}


/**
 * a LogicTree tree with an ">" operator and two subtrees
 */

class Implies extends BinaryTree
{
Implies(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  super(">", leftSubtree, rightSubtree);
  }


/**
 * Evaluate the tree.  This should only be called if the tree has no
 * unbound variable.  It is meaningless otherwise.
 * The result is true iff the result of evaluating the first sub-tree
 * is false, or the result of evaluating the second sub-tree is true.
 * This is the definition of the "implies" operator.
 */

boolean eval()
  {
  return !leftSubtree.eval() || rightSubtree.eval();
  }
}


/**
 * a LogicTree tree with a "+" operator and two subtrees
 */

class Or extends BinaryTree
{
Or(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  super("+", leftSubtree, rightSubtree);
  }


/**
 * Evaluate the tree.  This should only be called if the tree has no
 * unbound variable.  It is meaningless otherwise.
 * The result is true iff the result of evaluating either sub-tree
 * is true.
 * This is the definition of the "or" operator.
 */

boolean eval()
  {
  return leftSubtree.eval() || rightSubtree.eval();
  }
}


/**
 * a LogicTree tree with a "*" operator and two subtrees
 */

class And extends BinaryTree
{
And(LogicTree leftSubtree, LogicTree rightSubtree)
  {
  super("*", leftSubtree, rightSubtree);
  }


/**
 * Evaluate the tree.  This should only be called if the tree has no
 * unbound variable.  It is meaningless otherwise.
 * The result is true iff the result of evaluating both sub-trees
 * is true.
 * This is the definition of the "and" operator.
 */

boolean eval()
  {
  return leftSubtree.eval() && rightSubtree.eval();
  }
}


/**
 * a LogicTree tree with a "'" operator and one subtrees
 */

class Not extends UnaryTree
{
Not(LogicTree subtree)
  {
  super("'", subtree);
  }


/**
 * Evaluate the tree.  This should only be called if the tree has no
 * unbound variable.  It is meaningless otherwise.
 * The result is true iff the result of evaluating the sub-tree
 * is false.
 * This is the definition of the "not" operator.
 */

boolean eval()
  {
  return !subtree.eval();
  }
}



/**
 * a LogicTree tree for the constant 0 (false)
 */

class False extends Unit
{
False()
  {
  super("0");
  }


/**
 * Evaluate the tree.  The result is always false.
 */

boolean eval()
  {
  return false;
  }
}


/**
 * a LogicTree tree for the constant 1 (true)
 */

class True extends Unit
{
True()
  {
  super("1");
  }


/**
 * Evaluate the tree.  The result is always true.
 */

boolean eval()
  {
  return true;
  }
}


/**
 * a LogicTree tree for a variable with a given name
 */

class Var extends Unit
{
/**
 * the name of this variable
 */

char name;


/**
 * the logic value to which this variable is bound, if it is bound
 */

boolean logicValue;


/**
 * indication of whether this variable is bound
 */

boolean hasLogicValue;


/**
 * Construct a Var with a given name.
 */

Var(char name)
  {
  super("" + name);
  this.name = name;
  hasLogicValue = false;
  }


/**
 * Get this variable as an unbound variable if it is unbound.
 * If not, return null to so indicate.
 */

Var getVar()
  {
  if( hasLogicValue )
    return null;

  return this;
  }


/**
 * Bind the value of this variable to the indicated logicValue.
 */

void bind(Var var, boolean logicValue)
  {
  if( name == var.name )
    {
    this.logicValue = logicValue;
    this.hasLogicValue = true;
    }
  }


/**
 * Unbind the logical value of this variable.
 */

void unbind(Var var)
  {
  if( name == var.name )
    {
    this.hasLogicValue = false;
    }
  }

/**
 * Evaluate the tree consisting of this variable.
 * This should only be called if the variable is bound.
 * It is meaningless otherwise.
 */

boolean eval()
  {
  if( hasLogicValue )
    return logicValue;

  throw new UnboundVariableException("unbound variable " + value);
  }
}


/**
 * This class is used only to check against coding errors.
 * eval() should only be called when every variable in a tree is bound.
 * This exception will be thrown if eval() is called on a tree containing
 * an unbound variable.
 */

class UnboundVariableException extends RuntimeException
{
String message;

UnboundVariableException(String message)
  {
  this.message = message;
  }

public String toString()
  {
  return message;
  }  
}