<!--  // Hide this just in case this file is read as HTML

// *****************************************************************
// Globals
// *****************************************************************

// used to fix problem with reloading a page
// see tableauRefresh() for more comments
var lastSavedTableauReloadBug = null;

// *****************************************************************
// TABLEAU.JS
// Requires logic.js
//
// Tableau object - collection of assertions and goals
// *****************************************************************

// Tableau constants
var ASSERTION = 1;
var GOAL = 2;

// currently we have 3 selection states that rotate around:
// none, select for group 1, and select for group 2
var NUM_SELECTION_STATES = 3;

// default selection background color is null (none)
var SELECTION_COLORS = new Array(null, "aquamarine", "lightpink");

// rules
// text here is used to display the rule
var RULE_GIVEN = "Given";
var RULE_REWRITE = "Rewrite";
var RULE_SPLIT = "Split";
var RULE_RESOLUTION = "Resolution";
var RULE_EQUIVALENCE = "Equivalence";
var RULE_EQUALITY = "Equality";	
var RULE_SKOLEMIZATION = "Skolemize";

// used to help export rules
var EXPORT_TABLEAU_DATA = "exportTableau";

// *****************************************************************
// TableauRow
// *****************************************************************

function TableauRow(tableau, type, expr, rule, rowNum)
{
	// This class is used internally by Tableau
	// Rows are static. Once created, nothing about them should ever change

	// type is either ASSERTION or GOAL
	// expr and rule are TreeNodes
	// rule can be null

	// members
	this.tableau = tableau;
	this.type = type;
	this.expr = expr;
	this.rule = rule;
	this.rowNum = rowNum;

	this.numLayers = 0;	// number of layers used by this row

	// enter the individual nodes into the tableau
	// note that this has to occur before we generate the HTML
	expr.traverse(enterNode, tableau);
	expr.row = this;		// link back to this row

	if (rule)
	{
		enterNode(rule, tableau);
		rule.row = this;
	}

	this.generateHTML = tableauRowGenerateHTML;

	// html string to display this row
	this.html = "";
	this.generateHTML();
}

function enterNode(node, tableau)
{
	// called from the constructor for TableauRow
	// assign the node a unique nodeId and enter it into tableau
	var nodeId = tableau.nodes.length;
	node.nodeId = nodeId;
	tableau.nodes[nodeId] = node;

	resetNode(node);

	// set default selection for nodes
	node.selectState = 0;
}

function resetNode(node)
{
	// get rid of the layer data
	node.layerIds = new Array(); 	// layers associated with this node
	node.polarityLayerId = -1;	// layer for the polarity
}

// *****************************************************************
// Tableau
// *****************************************************************

function Tableau()
{
	this.showPolarities = true;

	this.rows = new Array();	// this is an array of TableauRows
    	this.name = "Tableau";

	// every node and every subnode is put into this array
	// and is indexed by nodeId stored in the TreeNodes
	this.nodes = new Array();

	this.selected = emptySelectionArray();
	this.numLayers = 0;	// number of layers used so far
	this.window = null;	// note that this window could be closed
	this.lastSelected = null;	// used internally by selection routines

	// method to be overridden
	this.nodeSelected = tableauNodeSelected;

	// public methods
	this.setName = tableauSetName;
	this.undo = tableauUndo;
	this.refresh = tableauRefresh;
	this.destroy = tableauDestroy;
	this.regenerateHTML = tableauRegenerateHTML;
	this.getSelectedNode = tableauGetSelectedNode;
	this.deselectAll = tableauDeselectAll;
	this.importData = tableauImport;
	this.exportData = tableauExport;
	this.applyRule = tableauApplyRule;

	// internal methods //

	// miscellaneous
	this.getNode = tableauGetNode;
	this.getRowFromNode = tableauGetRowFromNode;
	this.getRelativeRow = tableauGetRelativeRow;

	// rules
	this.addRow = tableauAddRow;
	this.addGiven = tableauAddGiven;
	this.doResolution = tableauDoResolution;
	this.doRewrite = tableauDoRewrite;
	this.doSplit = tableauDoSplit;
	this.doSkolemization = tableauDoSkolemization;
	this.doEquivalenceOrEquality = tableauDoEquivalenceOrEquality;
	this.addAppropriateRow = tableauAddAppropriateRow;

	// human interface
	this.saveSelections = tableauSaveSelections;
	this.setSelections = tableauSetSelections;
	this.updateSelectionArray = tableauUpdateSelectionArray;
	this.setSelectionState = tableauSetSelectionState;
	this.restoreAllSelections = tableauRestoreAllSelections;
	this.restoreSelectionState = tableauRestoreSelectionState;
	this.doClick = tableauDoMouseClick;
	this.doMouseOver = tableauDoMouseOver;
	this.doMouseOut = tableauDoMouseOut;
	this.doRuleClick = tableauDoRuleMouseClick;
	this.doRuleMouseOver = tableauDoRuleMouseOver;
	this.doRuleMouseOut = tableauDoRuleMouseOut;
}

function tableauSetName(name, refresh)
{
	this.name = name;

	if (refresh)
		this.refresh();
}

function tableauUndo(refresh)
{
	// undo removes the row(s) added by the last rule
	if (this.rows.length > 0)
	{
		var i = this.rows.length - 1;

		// remove all rows starting from the bottom until 
		// we find a row that has a rule
		while (i >= 0)
		{
			var lastRow = this.rows[i];

			this.numLayers -= lastRow.numLayers;

			// remove from this.nodes all nodes after the last row
			this.nodes.length = lastRow.expr.nodeId;
			this.rows.length--;

			if (lastRow.rule)
				break;		// found a row with a rule
			else
				i--;
		}

		if (refresh)
			this.refresh();
	}
}

function tableauDestroy()
{
	if ((this.window) && (!this.window.closed))
		this.window.close();

	this.window = null;
}

function tableauAddRow(type, expr, rule)
{
	// all logic expressions are simplified before being added
	// and polarities are calculated

	// type should be either ASSERTION or GOAL
	if ((type != ASSERTION) && (type != GOAL))
	{
		alert("Error in tableauAddRow. type == " + type);
		return;
	}

	expr = logicSimplify(expr);

	// initial polarities
	if (type == ASSERTION)
		expr.polarity = NEGATIVE;
	else
		expr.polarity = POSITIVE;

	calcPolarities(expr);

	var rowNum = this.rows.length;

	// add the row
	this.rows[this.rows.length] = new TableauRow(this, type, expr, rule, rowNum);
}

function tableauRegenerateHTML()
{
	// this needs to be called to regenerate HTML for the tableau
	// when for some reason the output should be changed, this should be called

	this.numLayers = 0;

	for (var i = 0; i < this.rows.length; i++)
		this.rows[i].generateHTML();

	// call refresh if the tableau window is opened
	if (this.window && !this.window.closed)
		this.refresh();
}

function getAbsoluteRowNum(thisRow, relativeRowNum)
{
	// convert from a relative row number to an absolute row number
	return (thisRow - relativeRowNum + 1);
}


function tableauGetRelativeRow(relativeRow)
{
	// The relative row is >= 1 and is relative to the next row in the tableau
	// We use relative rows to allow us to insert rows in front of the node's row.
	// without changing the node's relative row.
	// This is necessary to allow the joining of tableaux together.

	return (this.rows[getAbsoluteRowNum(this.rows.length-1, relativeRow)]);
}

function tableauGetNode(relativeRow, position)
{
	// returns a node given a relative row and a position array
	return (this.getRelativeRow(relativeRow).expr.getNode(position));
}

function tableauGetRowFromNode(node)
{
	// returns the relative row that node is in
	var row = node.getTreeTop().row.rowNum;
	var nextRow = this.rows.length;

	return (nextRow - row);
}

// *****************************************************************
// Printing functions to display the tableau
// Dynamic HTML just wasn't dynamic enough for me to figure out
// how to display expressions in a good way. In particular, nesting
// blocks of <DIV> or <SPAN> seemed to be a good way to go but
// would not work. There were many quirks in Netscape.
// Nesting almost anything doesn't work right. I gave up trying to
// work with dynamic borders to show selection.
// This solution just uses unnested <A> tags and shows that various subexpressions
// are selected by changing the background color.
// *****************************************************************

function tableauWindowUnload()
{
	// reload bug. see comment below
	if (window.opener && !window.opener.closed)
		window.opener.lastSavedTableauReloadBug = tableau;
}

function tableauWindowLoad()
{
	// reload bug. see comment below
	if (!window.tableau)
	{
		if (window.opener && !window.opener.closed)
			window.tableau = window.opener.lastSavedTableauReloadBug;

		if (!window.tableau || window.tableau.window != window)
		{
			alert ("Sorry, no tableau was found. This window is now closing.");
			window.close();
		}
		else
			window.tableau.refresh();		// refresh ourselves
	}
}

function tableauRefresh()
{
	// if the window is still opened then just use it
	// otherwise open a new window
	if (!this.window || this.window.closed)
	{
		// try to find a window that does not already 
		// belong to another tableau window
		var basename = "logic_tableau";
		var index = 1;

		while (true)
		{
			this.window = window.open("", basename+index, "height=640,width=480,resizable,scrollbars,menubar");

			if (this.window && !this.window.tableau)
			{
				// not a tableau window, just use this one
				break;
			}
			index++;
		}
	}

	with (this.window.document)
	{
		open();

		// Give the other window access to this tableau
		// this has to be after the document open()
		this.window.tableau = this;

		writeln("<HTML><HEAD><TITLE>" + this.name + "</TITLE>");

		// style sheet specifications
		// position:relative makes them dynamically editable
		writeln("<STYLE TYPE='text/css'>A {position:relative;color:black;text-decoration:none;}" +
			".NORMALTEXT {position:relative} " + 
			".POLARITY {position:relative;visibility:hide} </STYLE></HEAD>");

		// include JavaScript functions to be used there
		// also allow us to use document.layers on IE where it is actually document.all
		writeln("<SCRIPT>" + doShowSelectionState + 
			"if (!document.layers) document.layers = document.all;<\/SCRIPT>");

		// Netscape has the problem that when a document is reloaded
		// it loses all the JavaScript data it previouly contains
		// the tableau window requires the tableau object to work properly
		// this is a hack that saves the tableau in window.opener when the page is unloaded
		// if after this, we get a load event and tableau is not defined
		// we use the saved object to refresh ourselves
		// note that even worse is the fact that this code must be directly entered
		// into the onLoad() and onUnload() event handlers since it seems that
		// everything between <SCRIPT> is also lost during reload. yes stupid.

		// also, during resize, selections are not being redrawn for some reason

		writeln("<BODY onUnload='" + tableauWindowUnload.toString() + " tableauWindowUnload();'" +
			" onLoad='" + tableauWindowLoad.toString() + " tableauWindowLoad();'" +
			" onResize=tableau.restoreAllSelections()>");

		writeln("<H1>" + this.name + "</H1><TABLE WIDTH=100%>");
	
		// write header
		writeln("<TR><TH WIDTH=40%>Assertions</TH><TH WIDTH=40%>Goals</TH><TH>Rules</TH></TR>")

		var i;
		for (i = 0; i < this.rows.length; i++)
		{
			writeln(this.rows[i].html);
		}

		writeln("</TABLE>");
		writeln("</BODY></HTML>");
		close();
	}

	this.restoreAllSelections();
}

function tableauRowGenerateHTML()
{
	// creates the HTML string that wil be used to display this row

	if (this.html != "")
	{
		// we are regenerating html
		// toss away all the old data in the nodes
		this.expr.traverse(resetNode);
		if (this.rule)
			resetNode(this.rule);
		this.numLayers = 0;
	}

	this.html = "";

	this.html += "<TR>";

	// whether to add polarities to all the nodes
	var polarity = (this.tableau.showPolarities) ? addPolarity : null;

	if (this.type == ASSERTION)
	{
		this.html += "<TD>";

		// Selecting the row number selects whole expression
		// but we don't want row number to be selected along with everything
		// have row numbers start at 1 instead of 0
		generateLayer(this.expr, (this.rowNum + 1) + ". ", this, true);

		// generate HTML for the rest of the expression
		logicUnparse(this.expr, generateLayer, polarity, this)
		this.html += "</TD><TD></TD>";
	}
	else
	{
		this.html += "<TD></TD><TD>";
		generateLayer(this.expr, (this.rowNum + 1) + ". ", this, true);
		logicUnparse(this.expr, generateLayer, polarity, this)
		this.html += "</TD>";
	}

	this.html += "<TD>";

	// generate HTML for the rule
	if (this.rule)
	{
		generateRuleLayer(this.rule, getRuleHTML(this.rule), this);
	}
	this.html += "</TD></TR>";
}

function getRuleHTML(rule)
{
	// return html for the given rule
	if (rule.value == RULE_GIVEN)
		return (rule.value);
	else if ((rule.value == RULE_REWRITE) || (rule.value == RULE_SPLIT) || (rule.value == RULE_SKOLEMIZATION))
		return (rule.value + " " + getAbsoluteRowNum(rule.row.rowNum, rule.children[0].value));
	else
	{
		// resolution, equivalence, or equality
		// format for all three are the same
		return (rule.value + " " + getAbsoluteRowNum(rule.row.rowNum, rule.children[0].value) +
			", " + getAbsoluteRowNum(rule.row.rowNum, rule.children[2].value) +
			"<BR>" + rule.unifier);
	}
}

function addPolarity(node, row)
{
	if (node.polarity)
	{
		// share polarity layers to save some space
		// can share when our last child has the same polarity
		if ((node.children.length > 0) &&
			(node.children[node.children.length-1].polarity == node.polarity))
		{
			node.polarityLayerId = node.children[node.children.length-1].polarityLayerId;
		}
		else
		{
			row.html += "<SPAN CLASS=POLARITY><SUP><SMALL>" + node.polarity + "</SMALL></SUP></SPAN>";
			// create a layer here
			node.polarityLayerId = row.tableau.numLayers;

			row.numLayers++;
			row.tableau.numLayers++;
		}
	}
}

function generateRuleLayer(rule, text, row)
{
	// generate a layer for a rule
	// various nodes can be selected when mouse goes over rule, etc.

	var id = rule.nodeId;

	row.numLayers++
	row.tableau.numLayers++;

	row.html += "<A HREF=#" +
		" onClick='return(tableau.doRuleClick(" + id + ", arguments[0]))'" +
		" onMouseOver='tableau.doRuleMouseOver(" + id + ", arguments[0])'" +
		" onMouseOut='tableau.doRuleMouseOut(" + id + ", arguments[0])'>" + 
		text + "</A>\n";
}

function generateLayer(node, text, row, dontSelect)
{
	// if node is null then just add text to the end of row's html
	// else generate the html for a layer of text with the associated node

	// the optional fourth argument says not to include the new layer
	// in the layers that will be selected when node is selected

	if (node)
	{
		var id = node.nodeId;

		if (!dontSelect)
			node.layerIds[node.layerIds.length] = row.tableau.numLayers;

		row.numLayers++
		row.tableau.numLayers++;

		// arguments[0] is the event object when the event handler is called
		row.html += "<A HREF=#" +
			" onClick='return(tableau.doClick(" + id + ", arguments[0]))'" +
			" onMouseOver='tableau.doMouseOver(" + id + ", arguments[0])'" +
			" onMouseOut='tableau.doMouseOut(" + id + ", arguments[0])'>" + 
			text + "</A>\n";
	}
	else
		row.html += text;
}

// *****************************************************************
// Event Handlers called by user interaction with the tableau
// and for dealing with selections
// *****************************************************************

function tableauNodeSelected(node)
{
	// called when a node is selected
	// override to do something useful
}

function tableauDeselectAll()
{
	// have to copy selected to a new array since
	// this.selected will change as we deselect nodes
	var selected = new Array();

	for (var i = 0; i < NUM_SELECTION_STATES - 1; i++)
		arraycopy(this.selected[i], 0, selected, selected.length);

	// now deselect everything
	for (var i = 0; i < selected.length; i++)
		this.setSelectionState(selected[i], 0, true);

	// shouldn't happen but it does on internet explorer
	for (var i = 0; i < NUM_SELECTION_STATES - 1; i++)
		assert(this.selected[i].length == 0, "tableauDeselectAll", "unknown condition");
}

function tableauSaveSelections()
{
	// returns a copy of the selected array
	var newArray = new Array();
	for (var i = 0; i < NUM_SELECTION_STATES - 1; i++)
	{
		newArray[i] = new Array();
		for (var j = 0; j < this.selected[i].length; j++)
			newArray[i][j] = this.selected[i][j];
	}
	return (newArray);
}

function tableauSetSelections(selections, permanent)
{
	// given an array of selections (like this.selected)
	// will do the selections in there with
	// permanent deciding whether the changes are permanent
	if (!selections)
		return;

	for (var i = 0; i < selections.length; i++)
	{
		for (var j = 0; j < selections[i].length; j++)
		{
			this.setSelectionState(selections[i][j], i+1, permanent);
		}
	}
}

function tableauGetSelectedNode()
{
	// if exactly one node is selected, return that node
	// otherwise returns null

	var node = null;

	for (var i = 0; i < NUM_SELECTION_STATES - 1; i++)
	{
		if ((this.selected[i].length == 1) && (!node))
			node = this.selected[i][0];	// first selected node seen
		else if (this.selected[i].length != 0)
			return (null);		// more than one node selected
	}

	return (node);
}

function tableauDoRuleMouseOver(id, event)
{
	var rule = this.nodes[id];
	this.setSelections(rule.selections, false);
}

function tableauDoRuleMouseOut(id, event)
{
	var rule = this.nodes[id];

	if (!rule.selections)
		return;		// some rules don't have selections

	for (var i = 0; i < rule.selections.length; i++)
	{
		for (var j = 0; j < rule.selections[i].length; j++)
		{
			this.restoreSelectionState(rule.selections[i][j]);
		}
	}
}

function tableauDoRuleMouseClick(id, event)
{
	var rule = this.nodes[id];
	this.setSelections(rule.selections, true);
	return (false);
}

function tableauDoMouseOver(id, event)
{
	// when the mouse moves over an expression
	// it highlights to show how it would be selected
	// if the mouse was clicked over it

	var node = this.nodes[id];
	this.setSelectionState(node, nextSelectionState(node.selectState, false), false);
}

function tableauDoMouseOut(id, event)
{
	// reset it to what it should be

	var node = this.nodes[id];

	// restore the state for the whole tree rooted at node
	this.restoreSelectionState(node);

	this.lastSelected = null;
}

function tableauDoMouseClick(id, event)
{
	// click middle button to clear the selection
	// control click to extend selection (doesn't set state)
	// if shift is down then colors rotate the other way
	// otherwise set to next state

	// if lastSelected is set, then we pretend that node was
	// clicked regardless of which node was actually clicked
	var node = this.lastSelected ? this.lastSelected : this.nodes[id];

	// Microsoft IE doesn't support event objects
	var reverse = event && ((event.modifiers & Event.SHIFT_MASK) != 0);

	if (event && event.which == 2)	// second mouse button
		this.setSelectionState(node, 0, true);
	else
	{
		if (event && ((event.modifiers & Event.CONTROL_MASK) != 0))
		{
			if (!node.parent)
				return (false);		// can't go any higher

			// shift is down
			// same as if mouse went over this node's parent
			this.setSelectionState(node.parent, nextSelectionState(node.parent.selectState, reverse), false);

			// need to save this node
			// since mouse isn't actually over node's parent
			this.lastSelected = node.parent;
		}
		else	// normal click
		{
			this.setSelectionState(node, nextSelectionState(node.selectState, reverse), true);
		}
	}

	// return false to cancel the action of the <A> tag
	return (false);
}

function tableauUpdateSelectionArray(node, newState)
{
	var array;

	if (node.selectState != 0)
	{
		// remove old state from array
		array = this.selected[node.selectState-1];

		for (var i = 0; i < array.length; i++)
		{
			if (array[i] == node)
			{
				if (i != array.length - 1)
				{
					// move the last element into here
					array[i] = array[array.length-1];
				}
				// else it's the last element and we'll just shrink the array

				// now shrink the array
				array.length--;

				break;
			}
		}
	}

	// now add new state
	if (newState != 0)
	{
		array = this.selected[newState-1];
		array[array.length] = node;
	}
}

function tableauSetSelectionState(node, state, permanent)
{
	// sets the state stored in the given node
	// and all children (overriding whatever state they have)
	// and updates the display
	// if permanent then update the state stored in the node
	// otherwise only update the display

	// the node's parent state must either be the same or none
	// if it is the same, we shouldn't need to do anything
	// if it is none, we can proceed. otherwise we need
	// to go up and reset the state of the parent
	var parent = node.parent;
	if (parent)
	{
		if ((parent.selectState != state) && (parent.selectState != 0))
		{
			// can't have this node disagree with its parent
			// set parent (and parent's parent, etc) to no selection
			while (parent.parent && (parent.parent.selectState != 0))
				parent = parent.parent;

			this.setSelectionState(parent, 0, permanent);
		}
	}

	// now we can update this node

	// update state stored in node
	if (permanent)
	{
		// update arrays
		this.updateSelectionArray(node, state);

		// update value stored in all nodes rooted at node
		node.traverse(doSetSelectionState, state);

		this.nodeSelected(node);
	}

	// update the displayed state of the node
	node.traverse(this.window.doShowSelectionState, getColorForState(state));
}

function tableauRestoreSelectionState(node)
{
	// restore state of node and everything below node
	// also goes up and restores whatever is necessary to
	// maintain consistency

	var state = node.selectState;

	// find the highest node that has the same state as us
	// and make sure that it showing what we think it should be
	while ((node.parent) && (node.parent.selectState == state))
		node = node.parent;

	node.traverse(doRestoreSelectionState, this);
}

function tableauRestoreAllSelections()
{
	if (!this.window || this.window.closed)
		return;		// don't do anything if the window isn't there

	for (var i = 0; i < this.rows.length; i++)
	{
		this.restoreSelectionState(this.rows[i].expr);
	}
}

function nextSelectionState(state, reverse)
{
	// if reverse, goes the opposite direction
	if (reverse)
		return ((state - 1 + NUM_SELECTION_STATES) % NUM_SELECTION_STATES);
	else
		return ((state + 1) % NUM_SELECTION_STATES);
}

function getColorForState(state)
{
	return (SELECTION_COLORS[state]);
}

function doSetSelectionState(node, state)
{
	node.selectState = state;
}

function doRestoreSelectionState(node, tableau)
{
	tableau.window.doShowSelectionState(node, getColorForState(node.selectState));
}

function doShowSelectionState(node, color)
{
	// This is written into the *TABLEAU WINDOW* and called in that context

	// This needs to be in the tableau window since
	// we're trying to make it update the tableau document
	// and this is simpler than passing in another argument to traverse()

	// show or hide the polarity
	// show the polarity if color is not null
	// that is, there is some type of selection with this node
	// only show our polarity if parent doesn't have polarity showing
	// to avoid clutter in the tableau
	if (node.polarityLayerId >= 0)
	{
		var visible = color ? "show" : "hide";
		
		if (node.parent && 
			(document.layers[node.parent.polarityLayerId].visibility == "show") &&
			(node.parent.polarityLayerId != node.polarityLayerId))
		{
			visible = "hide";
		}
		
		document.layers[node.polarityLayerId].visibility = visible;
	    
	}

	for (var i = 0; i < node.layerIds.length; i++)
		document.layers[node.layerIds[i]].bgColor = color;
}

// *****************************************************************
// Rules
// applyRule() is the entry point for all rules
// *****************************************************************

function tableauApplyRule(whatRule, refresh, arg1, arg2, arg3)
{
	// applyRule() takes the rule to use, whether or not to refresh
	// after applying the rule and also some optional arguments
	// If the rule was successful, a node representing the rule is returned
	// otherwise null is returned
	// If the rule is successful, then the tableau is updated
	// If refresh is true, then the tableau is refreshed if the tableau is changed

	// arg1 (type), arg2 (expr), and arg3 (auto skolemize) are used for RULE_GIVEN 
	// and arg1 (which rewrite) is used for RULE_REWRITE

	var rule = null;

	if (whatRule == RULE_GIVEN)
	{
		rule = this.addGiven(arg1, arg2);
		if (rule && arg3 && false)
		{
alert('temp');

			// automatically skolemize the last row added
			var lastRow = this.rows[this.rows.length-1];
			this.doSkolemization(lastRow.rowNum, lastRow.expr.getNodePosition());
		}
	}
	else if ((whatRule == RULE_REWRITE) || (whatRule == RULE_SPLIT) || (whatRule == RULE_SKOLEMIZATION))
	{
		var node = this.getSelectedNode();

		if (!node) // none or more than one selected
		{
			alert("To apply this rule, exactly one expression must be selected.");
			return (null);
		}

		var position = node.getNodePosition();
		var row = this.getRowFromNode(node);

		if (whatRule == RULE_REWRITE)
			rule = this.doRewrite(row, position, arg1);
		else if (whatRule == RULE_SPLIT)
		{
			if (node.parent)
				alert("You can only split top level expressions.");
			else
				rule = this.doSplit(row);
		}
		else
		{
			if (isQuantifierFree(node))
				alert("You must select an expression containing at least one quantifier with strict force.");
			else
				rule = this.doSkolemization(row, position);
		}
	}
	else
	{
		// rule that is applied to two rows (can be the same)
		// but each row can have multiple selections

		var group1 = new Array();
		var group2 = new Array();
		var row1;
		var row2;
		var thisRow;
		var thisGroup;
		var testRow;
		var i, j;
		var node;
		var followsPolarityStrategy = false;
		var uselessPolarity = POSITIVE;

		if ((this.selected[0].length == 0) || (this.selected[1].length == 0))
		{
			alert("There must be at least one expression selected in each group.");
			return (null);
		}

		// loop for group1 and group 2
		for (j = 0; j < 2; j++)
		{
			thisRow = -1;
			thisGroup = new Array();
			for (i = 0; i < this.selected[j].length; i++)
			{
				node = this.selected[j][i];
				testRow = this.getRowFromNode(node);

				if (thisRow == -1)
					thisRow = testRow;
				else if (thisRow != testRow)
				{
					alert("All expressions selected in one group must come from the same row.");
					return (null);
				}

				if (!isQuantifierFree(node) || !isFreeSubexpression(node))
				{
					alert("All selected expressions must be free and quantifier free.");
					return (null);
				}

				thisGroup[i] = node.getNodePosition();

				// check if in accordance with polarity strategy also
				// polarity strategy states for these rules that at least one
				// node must have some polarity (doesn't have to be strict)
				// so uselessPolarity is the only polarity that would allow a
				// node to violate the polarity strategy
				//
				// for equivalence and equality (non-resolution)
				// we actually need to the polarity of the parent
				if (((whatRule == RULE_RESOLUTION) && (node.polarity != uselessPolarity)) ||
					(node.parent && (node.parent.polarity != uselessPolarity)))
					followsPolarityStrategy = true;
			}

			if (whatRule == RULE_RESOLUTION)
			{
				if (!followsPolarityStrategy)
				{
					alert("Warning: At least one expression to be replaced by " +
						"false should have negative polarity\n" +
						"and one expression to be replaced by true should " +
						 "have positive polarity.");

					// set this to true so that only give above error once
					followsPolarityStrategy = true;
				}
				else
				{
					// have to check two groups for resolution
					uselessPolarity = NEGATIVE;
					followsPolarityStrategy = false;
				}

			}
			else
			{
				if (!followsPolarityStrategy)
					alert("Warning: At least one expression to be replaced by " +
						"false should have negative polarity.");

				// only care about the first time, only one condition
				followsPolarityStrategy = true;
			}

			if (j == 0)
			{
				row1 = thisRow;
				group1 = thisGroup;
			}
			else
			{
				row2 = thisRow;
				group2 = thisGroup;
			}
		}

		if (whatRule == RULE_RESOLUTION)
			rule = this.doResolution(row1, group1, row2, group2);
		else if ((whatRule == RULE_EQUIVALENCE) || (whatRule == RULE_EQUALITY))
			rule = this.doEquivalenceOrEquality(whatRule, row1, group1, row2, group2);
		else
			assert(0, "tableauApplyRule", "unknown rule");
	}

	if (rule)
	{
		if (refresh)
			this.refresh();

		// all rules except adding givens require some form of selection
		// deselect everything after successful application of the rule
		if (whatRule != RULE_GIVEN)
			this.deselectAll();
	}

	return (rule);
}

function tableauAddGiven(type, str)
{
	// parse given string
	var expr = logicParse(str);

	if (!expr)
		return (null);

	// create rule node
	var rule = new TreeNode(RULE_GIVEN, new TreeNode(type), new TreeNode(str));

	this.addRow(type, expr, rule);

	return (rule);
}

function tableauDoRewrite(row, position, num)
{
	// rewriting rules are identified by number as indices
	// into array returned by getPossibleRewrites()

	var node = this.getNode(row, position);
	var top = node.getTreeTop();

	var rewrites = getPossibleRewrites(node);

	if (rewrites.length <= num)
		return (null);

	var rule = new TreeNode(RULE_REWRITE, new TreeNode(row), new TreeNode(position), new TreeNode(num));

	var newnode = top.clone();

	// do the rewrite
	newnode.getNode(position).replaceWith(rewrites[num]);

	// the type of the rewritten expression is the same as the original
	this.addRow(top.row.type, newnode, rule);

	// enter node to be selected when mouse goes over rule
	rule.selections = emptySelectionArray();
	rule.selections[0][0] = node;

	return (rule);
}

function tableauDoSplit(row)
{
	var node = this.getRelativeRow(row).expr;

	// three types of split - AND, OR, and IF
	var token = node.value;
	var type = node.row.type;	// ASSERTION or GOAL
	if (!(((token == AND) && (type == ASSERTION)) ||
		((token == OR) && (type == GOAL)) ||
		((token == IF) && (type == GOAL))))
	{
		alert ("This rule can not be applied.");
		return (null);
	}

	var rule = new TreeNode(RULE_SPLIT, new TreeNode(row));

	// note that second row added has a null rule
	// rule is only associated with one row
	if (token == AND)
	{
		this.addRow(ASSERTION, node.children[0].clone(), rule);
		this.addRow(ASSERTION, node.children[1].clone(), null);
	}
	else if (token == OR)
	{
		this.addRow(GOAL, node.children[0].clone(), rule);
		this.addRow(GOAL, node.children[1].clone(), null);
	}
	else if (token == IF)
	{
		this.addRow(ASSERTION, node.children[0].clone(), rule);
		this.addRow(GOAL, node.children[1].clone(), null);
	}

	rule.selections = emptySelectionArray();
	rule.selections[0][0] = node;

	return (rule);
}

function tableauDoSkolemization(row, position)
{
	// remove all quantifiers of strict force in the given node
	// if no quantifiers are removed, then a new row is not added
	var node = this.getNode(row, position);
	var top = node.getTreeTop();

	var newtop = top.clone();	// have to clone from the top
	var newnode = newtop.getNode(position);

	// need polarities to calculate quantifier forces
	newtop.polarity = top.polarity;
	calcPolarities(newtop);

	newnode = doSkolemize(newnode);

	if (treeEqual(newnode, node))
	{
		alert("No quantifiers were eliminated.");
		return (null);		// no change
	}
	else
	{
		var rule = new TreeNode(RULE_SKOLEMIZATION, new TreeNode(row), new TreeNode(position));
		rule.selections = emptySelectionArray();
		rule.selections[0][0] = node;

		this.addRow(top.row.type, newtop, rule);

		return (rule);
	}
}

function tableauDoResolution(falseRowNum, falseGroup, trueRowNum, trueGroup)
{
	// falseRow and trueRow are relative row numbers.
	// falseGroup and trueGroup are arrays of node positions.

	var falseRow = this.getRelativeRow(falseRowNum);
	var trueRow = this.getRelativeRow(trueRowNum);

	var originalGroup1Nodes = getAllNodes(falseRow.expr, falseGroup);
	var originalGroup2Nodes = getAllNodes(trueRow.expr, trueGroup);

	// rename common free variables
	var falseBefore = falseRow.expr.clone()
	var trueBefore = trueRow.expr.clone()

	renameCommonFreeVariables(falseBefore, trueBefore);

	var falseNodes = getAllNodes(falseBefore, falseGroup);
	var trueNodes = getAllNodes(trueBefore, trueGroup);

	// get most general unifier of all nodes in both groups
	var allnodes = new Array();
	arraycopy(falseNodes, 0, allnodes, 0);
	arraycopy(trueNodes, 0, allnodes, allnodes.length);

	var unifier = getMostGeneralUnifier(allnodes);

	if (!unifier)
	{
		alert("The expressions are not unifiable.");
		return (null);
	}

	// get unified expression. apply to any node - should be same
	var unifiedExpr = unifier.applyTo(falseNodes[0]);

	// now do the substitutions
	var replaceFalse = new Substitution();
	var replaceTrue = new Substitution();

	// both are total substitutions
	replaceFalse.addPair(unifiedExpr, new TreeNode(FALSE));
	replaceTrue.addPair(unifiedExpr, new TreeNode(TRUE));

	var falseAfter = replaceFalse.applyTo(unifier.applyTo(falseBefore, true), true);
	var trueAfter = replaceTrue.applyTo(unifier.applyTo(trueBefore, true), true);

	var rule = new TreeNode(RULE_RESOLUTION, new TreeNode(falseRowNum), new TreeNode(falseGroup),
					new TreeNode(trueRowNum), new TreeNode(trueGroup));

	rule.unifier = unifier;		// save this so that it can be displayed along with the rule

	this.addAppropriateRow(falseRow.type, falseAfter, trueRow.type, trueAfter, rule);

	rule.selections = emptySelectionArray();
	rule.selections[0] = originalGroup1Nodes;
	rule.selections[1] = originalGroup2Nodes;

	return (rule);
}

function tableauDoEquivalenceOrEquality(whatRule, row1Num, group1, row2Num, group2)
{
	// the equivalence and equality rules are basically the same except one
	// deals with equivalence of proprositions and the other with equality of terms
	// the application of the rules however are identical

	// row1 contains the equivalence (or equality)  expression P <-> Q to be replaced by false
	// row2 contains P and will be replaced by Q
	// nodes selected in group1 will be in the P group along with those in group2

	var row1 = this.getRelativeRow(row1Num);
	var row2 = this.getRelativeRow(row2Num);

	var originalGroup1Nodes = getAllNodes(row1.expr, group1);
	var originalGroup2Nodes = getAllNodes(row2.expr, group2);

	// rename common free variables
	var row1Before = row1.expr.clone()
	var row2Before = row2.expr.clone()

	renameCommonFreeVariables(row1Before, row2Before);

	var group1Nodes = getAllNodes(row1Before, group1);
	var group2Nodes = getAllNodes(row2Before, group2);

	var Pnodes = new Array();
	var Qnodes = new Array();

	// check the applicability of this rule
	// all group1 nodes' parent must be have a value of IFF (or EQUAL)
	var whatSymbol = (whatRule == RULE_EQUIVALENCE) ? IFF : EQUAL;
	var rulename = (whatRule == RULE_EQUIVALENCE) ? "equivalence" : "equality";

	for (var i = 0; i < group1Nodes.length; i++)
	{
		if (!group1Nodes[i].parent || (group1Nodes[i].parent.value != whatSymbol))
		{
			if (group1Nodes[i].value == whatSymbol)
				alert("Please select either the left side or the right side of the " +
					rulename + " expression.");
			else
				alert("All expressions in group one must be part of an " +
					rulename + " expression.");
			return (null);
		}
		Pnodes[i] = group1Nodes[i];

		// Q node is the other child of the IFF or EQUAL (our parent)
		Qnodes[i] = group1Nodes[i].parent.children[group1Nodes[i].childNum == 0 ? 1 : 0];
	}

	var unifier = null; 

	// put group 2 into P group
	arraycopy(group2Nodes, 0, Pnodes, Pnodes.length);

	unifier = getMostGeneralSeparateUnifier(Pnodes, Qnodes);
	if (!unifier)
	{
		alert("The expressions are not unifiable.");
		return (null);
	}

	// get unified expressions
	var unifiedP = unifier.applyTo(Pnodes[0]);
	var unifiedQ = unifier.applyTo(Qnodes[0]);

	if (treeEqual(unifiedP, unifiedQ))
		alert("Warning: The expression on either side of the " + rulename + " are identical after unification.");

	// do the substitutions
	var replaceIffOrEqual = new Substitution();
	var replaceByQ = new Substitution();

	// substitute for both the right and left versions so both p <-> q and q <-> p
	// will be replaced by false
	replaceIffOrEqual.addPair(new TreeNode(whatSymbol, unifiedP, unifiedQ), new TreeNode(FALSE));
	replaceIffOrEqual.addPair(new TreeNode(whatSymbol, unifiedQ, unifiedP), new TreeNode(FALSE));

	// total substitution here
	var row1After = replaceIffOrEqual.applyTo(unifier.applyTo(row1Before, true), true);

	// this is a partial substitution
	// only those nodes specified by user are replaced

	replaceByQ.addPair(unifiedP, unifiedQ);

	var row2After = unifier.applyTo(row2Before, true);
	var node;
	for (var i = 0; i < group2.length; i++)
	{
		// use substitution here instead of just replacing by unifiedQ
		// to make sure the substitution is done safely
		node = row2After.getNode(group2[i]);
		node.replaceWith(replaceByQ.applyTo(node, true));
	}

	var rule = new TreeNode(whatRule, new TreeNode(row1Num), new TreeNode(group1), new TreeNode(row2Num), new TreeNode(group2));

	rule.unifier = unifier;		// save this so that it can be displayed along with the rule

	this.addAppropriateRow(row1.type, row1After, row2.type, row2After, rule);

	rule.selections = emptySelectionArray();
	rule.selections[0] = originalGroup1Nodes;
	rule.selections[1] = originalGroup2Nodes;

	return (rule);
}

function tableauAddAppropriateRow(type1, expr1, type2, expr2, rule)
{
	// for resolution, equivalence, and equality
	// add the right row into the tableau based on the types of input
	// since each of these rules has 4 forms - AA, AG, GA, and GG

	if ((type1 == ASSERTION) && (type2 == ASSERTION))	// AA
		this.addRow(ASSERTION, new TreeNode(OR, expr1, expr2), rule);
	else if (type1 == ASSERTION)		// AG
		this.addRow(GOAL, new TreeNode(AND, new TreeNode(NOT, expr1), expr2), rule);
	else if (type2 == ASSERTION)		// GA
		this.addRow(GOAL, new TreeNode(AND, expr1, new TreeNode(NOT, expr2)), rule);
	else					// GG
		this.addRow(GOAL, new TreeNode(AND, expr1, expr2), rule);
}

// *****************************************************************
// Import/Export
// These functions allow you to save the state of the tableau and
// restore it later.
// tableauExport() will return a string of JavaScript code that when
// evaluated will assign to EXPORT_TABLEAU_DATA the tableau data.
// when this data is passed back into tableauImport(), the data
// will be used to recreate the tableau.
// Note that this was created so that tableau does not have to be
// empty to import data. This can be used to append tableaux, for example.
// *****************************************************************

function tableauExport()
{
	// function to export all rules
	// exports the rule node along with all its children
	// the value of children nodes can be numbers, strings, or arrays of these things

	var data = EXPORT_TABLEAU_DATA + '=new Array();';
	var rule;
	var ruleNum = 0;
	var arrays = '';	// arrays are handled separately
	var value;

	// only use double quotes in the string returned
	for (var i = 0; i < tableau.rows.length; i++)
	{
		rule = tableau.rows[i].rule;

		if (!rule)
			continue;

		data += EXPORT_TABLEAU_DATA + '[' + ruleNum + ']=new Array("' + rule.value + '"';

		for (var j = 0; j < rule.children.length; j++)
		{
			data += ',';

			value  = rule.children[j].value;

			if (value.substring)
			{
				// add quotes around strings and escape it
				data += '"' + escape(value) + '"';
			}
			else if (isArray(value))
			{
				// assign to the right element all the data for the array
				// all arrays will be initialized at the end
				// it's j+1 since first element is for rule.value (the name of the rule)
				arrays += exportArray(EXPORT_TABLEAU_DATA + '[' + ruleNum + '][' + (j+1) + ']', value);

				data += '0';	// temporary - expect it to be overriden
			}
			else	// number
				data += value;
		}
		data += '); ';

		ruleNum++;
	}

	data += arrays;		// initialize all array elements

	return (data);
}

function exportArray(variable, array)
{
	// array should be an array of numbers or nested arrays of numbers
	// return string that when evaluated will assign to variable
	// the same value as the passed in array

	var str = variable + '=new Array(';

	if ((array.length == 1) && (!isArray(array[0])))
	{
		// problem is that JavaScript can treat new Array(0)
		// as declaring an array of 0 elements instead of an array with one element of 0
		str += '); ';
		str += variable + '[0]=' + array[0] + '; ';
		return (str);
	}

	var nested = '';

	for (var i = 0; i < array.length; i++)
	{
		if (i != 0)
			str += ',';

		if (isArray(array[i]))
		{
			nested += exportArray(variable + "[" + i + "]", array[i]);
			str += '0';
		}
		else
			str += array[i];	// not an array
	}

	str += '); ';
	str += nested;

	return (str);
}

function tableauImport(data, refresh)
{
	var ruleType;
	var rule;

	for (var i = 0; i < data.length; i++)
	{
		ruleType = data[i][0];

		if (ruleType == RULE_GIVEN)
			rule = this.addGiven(data[i][1], unescape(data[i][2]));
		else if (ruleType == RULE_REWRITE)
			rule = this.doRewrite(data[i][1], data[i][2], data[i][3]);
		else if (ruleType == RULE_SPLIT)
			rule = this.doSplit(data[i][1]);
		else if (ruleType == RULE_SKOLEMIZATION)
			rule = this.doSkolemization(data[i][1], data[i][2]);
		else if (ruleType == RULE_RESOLUTION)
			rule = this.doResolution(data[i][1], data[i][2], data[i][3], data[i][4]);
		else if ((ruleType == RULE_EQUIVALENCE) || (ruleType == RULE_EQUALITY))
			rule = this.doEquivalenceOrEquality(ruleType, data[i][1], data[i][2], data[i][3], data[i][4]);
	}

	if (refresh)
		this.refresh();
}

// *****************************************************************
// Miscellaneous
// *****************************************************************

function emptySelectionArray()
{
	// returns an empty array that can be used for the selected array
	var array = new Array();
	for (var i = 0; i < NUM_SELECTION_STATES - 1; i++)
		array[i] = new Array();
	return (array);
}

function getAllNodes(top, positions)
{
	// given an array of node positions, will
	// return an array of nodes
	var nodes = new Array();
	for (var i = 0; i < positions.length; i++)
		nodes[i] = top.getNode(positions[i]);

	return (nodes);
}

// Stop hiding -->