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

// *****************************************************************
// LOGIC.JS
// Requires Parser.js, Stack.js, Tree.js, and misc.js
//
// some entry points:
// logicParse(str): returns a Tree representing the logic expression or null
// treeNodeToString(node): convert a node back to a string
// logicSimplify(node): simplify the logic expression given
// *****************************************************************

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

var logicParser = null; // setupLogicParser() will initialize this

var symbolTable = new Array();	// All identifiers and their types go into here

var possibleRewrites = new Array();
var simplifications = new Array();

// *****************************************************************
// Constants
// *****************************************************************

// used for automatically generating new identifiers
var NEW_VARIABLE_PREFIX = 'x';
var NEW_FUNCTION_PREFIX = 'f';
var NEW_CONSTANT_PREFIX = 'c';

// quantifier force
var UNIVERSAL_FORCE = 'A';
var EXISTENTIAL_FORCE = 'E';
var BOTH_FORCES = 'AE';

// Polarities
var POSITIVE = "+";
var NEGATIVE = "-";
var BOTH = "+/-";

// Tokens returned by lexer
// Not particularly important what these are

var T_VAR = "VARIABLE";
var T_FUNCTION = "FUNCTION";
var T_PREDICATE = "PREDICATE";

// so we can simplify the grammar and the parsing
// we group all logical binary operators and quantifiers
var T_BINARY_OP = "BINARY_OP";	
var T_QUANTIFIER = "QUANTIFIER";

var T_NOT = "NOT";
var T_EQUAL = "EQUAL";	// note this isn't a logical binary operator
var T_TRUE = "TRUE";
var T_FALSE = "FALSE";
var T_FORALL = "FORALL";
var T_EXISTS = "EXISTS";
var T_IF = "IMPLIES";
var T_IFF = "IFF";
var T_AND = "AND";
var T_OR = "OR";

// create standard tokens so we can just reuse these
var NOT = new Token(T_NOT, null);
var AND = new Token(T_AND, null);
var OR = new Token(T_OR, null);
var IF = new Token(T_IF, null);
var IFF = new Token(T_IFF, null);
var TRUE = new Token(T_TRUE, null);
var FALSE = new Token(T_FALSE, null);
var FORALL = new Token(T_FORALL, null);
var EXISTS = new Token(T_EXISTS, null);
var EQUAL = new Token(T_EQUAL, null);

// This is used is 'schemas'. Can be used in place of any expression
var PLACEHOLDER = "PLACEHOLDER";
var nextPlaceholderId = 0;	// used to generate unique placeholders

// This is an array of all the special symbols that can be returned by the lexer
var SYMBOLS = new Array(T_TRUE, T_FALSE, T_NOT, T_AND, T_OR, T_IF,
			T_IFF, T_FORALL, T_EXISTS, T_EQUAL);


// Variables that affect the lexical analysis
// Define an array with the special names to simplify lookup
// assign SYMBOL_ARRAY[str] to a token type to be returned
// (i.e. SYMBOL_ARRAY["and"] = T_AND;
var SYMBOL_ARRAY = new Array();

// OUTPUT_SYMBOLS[token] is string to output to represent the token
var OUTPUT_SYMBOLS = new Array();

// These are the actual tokens returned by lex to help simplify parsing
// The value of the token is the real token seen
var LEX_AND = new Token(T_BINARY_OP, AND);
var LEX_OR = new Token(T_BINARY_OP, OR);
var LEX_IF = new Token(T_BINARY_OP, IF);
var LEX_IFF = new Token(T_BINARY_OP, IFF);
var LEX_FORALL = new Token(T_QUANTIFIER, FORALL);
var LEX_EXISTS = new Token(T_QUANTIFIER, EXISTS);

// what the lexer actually returns for each token type
var LEX_TOKENS = new Array();
LEX_TOKENS[T_NOT] = NOT;
LEX_TOKENS[T_AND] = LEX_AND;
LEX_TOKENS[T_OR] = LEX_OR;
LEX_TOKENS[T_IF] = LEX_IF;
LEX_TOKENS[T_IFF] = LEX_IFF;
LEX_TOKENS[T_EQUAL] = EQUAL;
LEX_TOKENS[T_TRUE] = TRUE;
LEX_TOKENS[T_FALSE] = FALSE;
LEX_TOKENS[T_FORALL] = LEX_FORALL;
LEX_TOKENS[T_EXISTS] = LEX_EXISTS;


// lexer tells the type of identifiers 
// by first letters
// if it starts with a, b, c, f, g, or h it is a function
// if it starts with u, v, w, x, y, or z it is a variable
// everything else is taken to be a predicate symbol
//
// This can be overridden by prepending an identifier with one of the following
// $ for variables, @ for function, and ? for predicates
// Thus $p is a variable named p even though it would normally have
// been treated as a predicate 

var LEX_IDENTIFIER_OVERRIDE = new Array();
LEX_IDENTIFIER_OVERRIDE["$"] = T_VAR;
LEX_IDENTIFIER_OVERRIDE["@"] = T_FUNCTION;
LEX_IDENTIFIER_OVERRIDE["?"] = T_PREDICATE;

// possible letters, numbers, and other things that are allowed in identifiers
var IDENTIFIER_ALPHABET = "'_ABCDEFGHIJKLMNOPQRSTUVWYXZ0123456789";

// characters that indicate the end of non-identifiers
var SYMBOL_BOUNDARY = IDENTIFIER_ALPHABET + " ()";

// *****************************************************************
// Semantic analysis
// *****************************************************************

function defineIdentifier(type, name, mustMatch)
{
	// define identifier of name to be of type
	// where type is one of T_VAR, T_FUNCTION, T_PREDICATE
	// returns a token
	// if name is already in the symbol table of the right type
	// then it returns the token in the symbol table
	// otherwise if name is defined to be a different type and mustMatch,
	// a parseError occurs and false is returned
	// if !mustMatch then the passed in type is ignored when an existing
	// token is found

	var token;

	if (symbolTable[name])
	{
		// check that previous definition of name had same type
		token = symbolTable[name];

		if (mustMatch && (token.type != type))
		{
			parseError("Redefinition of " + name + " as a " + type +
				". Previously was a " + token.type + ".");
			return (false);
		}

		// else we return token
	}
	else
	{
		// not defined before
		token = new Token(type, name);
		symbolTable[name] = token;
	}

	return (token);
}

function checkArity(token, numTerms)
{
	// check that the arity for predicates or functions is consistent
	// have to check directly with null since arity could be equal to 0
	if (token.arity == null)
		token.arity = numTerms;		// first time to see this function/predicate
	else if (token.arity != numTerms)
	{
		parseError(token.value + " previously had " + token.arity + " argument(s).");
		return (false);
	}
	return (true);
}

// *****************************************************************
// Lexical analyzer
//
// Symbols are delimited by space
// In addition, strings of letters (and numbers) are delimited
// by non-letters and non-numbers (and quote) while
// strings of non-letters are delimited by letters (and spaces)
// Basically, letters are grouped with letters and everything
// else is grouped together
//
// Determines the type an identifier is by the first letter
// This can be overridden with an override symbol preceding the identifier
// that tells the lexer what the identifier should be treated as
// *****************************************************************

function LogicLexer(str)
{
	this.str = str;
	this.nextIdentifier = null;	// override the type of the next identifier with this

	this.nextToken = logicLexNextToken;
}

function logicLexNextToken()
{
	// returns one token from the string
	// returns false if error occurs
	// returns null if no more input (str == "")

	var token;
	var pos = 0;      // location of end of token
	var ch;           // temporary character holder

	this.str = trim(this.str);  // remove leading and trailing spaces

	if (this.str == "")
		return (null);      // no more input

	ch = this.str.charAt(pos);   // get the first character

	if (IDENTIFIER_ALPHABET.indexOf(ch.toUpperCase()) != -1)
	{
		// identifier or keyword

		while (IDENTIFIER_ALPHABET.indexOf(ch.toUpperCase()) != -1)
		{
			// increment pos and find next character

			pos++;
			if (pos >= this.str.length)
				break;      // reached end of string
			else
				ch = this.str.charAt(pos);   // continue testing
		}

		tokenVal = this.str.substring(0, pos);

		// determine the type of the token
		if (this.nextIdentifier)
		{
			// the type of this identifier has been specified
			token = defineIdentifier(LEX_IDENTIFIER_OVERRIDE[this.nextIdentifier], tokenVal, true);
			this.nextIdentifier = null;	// reset this
		}
		else if (SYMBOL_ARRAY[tokenVal])	// check if it is a special symbol
			token = LEX_TOKENS[SYMBOL_ARRAY[tokenVal]];
		else
		{
			// determine what it is by first character
			ch = tokenVal.charAt(0).toUpperCase();

			// constants as defined by Manna, Waldinger are
			// treated as functions (really functions with no arguments)
			if ((ch <= 'C') || ((ch >= 'F') && (ch <= 'H')))
				token = defineIdentifier(T_FUNCTION, tokenVal, false);
			else if (ch >= 'U')
				token = defineIdentifier(T_VAR, tokenVal, false);
			else
				token = defineIdentifier(T_PREDICATE, tokenVal, false);
		}
	}
	else	// not an identifier
	{
		if (this.nextIdentifier)
		{
			// expected an identifier, but didn't get one
			parseError("Expected identifier after '" + this.nextIdentifier + "'");
			return (false); 
		}

		// we find the next boundary space, letter, or parenthesis
		do 
		{
			// increment pos and find next character
			pos++;
			if (pos >= this.str.length)
				break;      // reached end of string
			else
				ch = this.str.charAt(pos);   // continue testing
		}
		while (SYMBOL_BOUNDARY.indexOf(ch.toUpperCase()) == -1);

		tokenVal = this.str.substring(0, pos);

		if (SYMBOL_ARRAY[tokenVal])
		{
			token = LEX_TOKENS[SYMBOL_ARRAY[tokenVal]];
		}
		else
		{
			// check if one of the "identifier type overrides"
			if (LEX_IDENTIFIER_OVERRIDE[tokenVal])
			{
				this.nextIdentifier = tokenVal;

				this.str = this.str.substring(pos);	// prepare for next call
				return (this.nextToken());		// return the next identifier (hopefully)
			}

			// can't be an identifier and isn't is a special symbol
			// so maybe it belongs by itself
			// return the first character by itself
			// reset pos so we get the rest next time
			token = new Token(this.str.charAt(0), null);
			pos = 1;
		}
	}

	// remove from the string everything that we have already seen
	this.str = this.str.substring(pos);  // everythi ang else

	return (token);
}

// *****************************************************************
// Parser for logic expressions
// *****************************************************************
//
// This parser will return a tree representing the input expression
//
// *****************************************************************
// All binary operators have left to right associativity with
// all equal precedence
// quantifiers and NOT have higher precendence than binary operators
//
// This is a LL(1) parser for the following grammar:
//
// SENTENCE -> ATOMIC | SENTENCE binary_op ATOMIC
// ATOMIC  -> ( SENTENCE ) | not ATOMIC | PROPOSITION | ( quantifier variable ) ATOMIC
//
// After removing left recursion/left factoring from these productions
// and the rest of the grammar follows. The numbers identify each production
//
// Production 13: TERM -> constant has been removed.
//
// SENTENCE -> ATOMIC OPT_BINARY ~1~
// OPT_BINARY -> $empty$ ~2~ | binary_op ATOMIC OPT_BINARY ~3~
// ATOMIC  -> ( ATOMIC' ~4~ | not ATOMIC ~5~ | PROPOSITION ~6~
// ATOMIC' -> SENTENCE ) ~7~ | quantifier OPT_PREDICATE TERMLIST ) ATOMIC ~8~
// PROPOSITION -> true ~9~ | false ~10~ | predicate OPT_TERMLIST ~11~ | TERM equal TERM ~12~
// TERM -> variable ~14~ | FUNCTION ~15~
// FUNCTION -> function OPT_TERMLIST ~16
// OPT_TERMLIST -> $empty$ ~17~ | ( TERMLIST ) ~18~
// TERMLIST -> $empty ~19~ | TERM MORETERMS ~20~
// MORETERMS -> $empty ~21~ | , TERM MORETERMS ~22~
// OPT_PREDICATE -> $empty ~23~ | predicate ~24~
//
// First(SENTENCE) = ( not true false predicate variable function
// First(OPT_BINARY) = $empty binary_op
// First(ATOMIC) = ( not true false predicate variable function
// First(ATOMIC') = ( not true false predicate variable function quantifier
// First(PROPOSITION) = true false predicate variable function
// First(TERM) =  variable function
// First(FUNCTION) = function
// First(OPT_TERMLIST) = $empty (
// First(TERMLIST) = $empty variable function
// First(MORETERMS) = $empty ,
// First(OPT_PREDICATE) = $empty predicate
//
// Follow(SENTENCE) = $ )
// Follow(OPT_BINARY) = $ )
// Follow(ATOMIC) = $ ) binary_op
// Follow(ATOMIC') = $ ) binary_op
// Follow(PROPOSITION) = $ ) binary_op
// Follow(TERM) = equal $ ) binary_op ,
// Follow(FUNCTION) = equal $ ) binary_op ,
// Follow(OPT_TERMLIST) = equal $ ) binary_op ,
// Follow(TERMLIST) = )
// Follow(MORETERMS) = )
// Follow(OPT_PREDICATE) = variable function )
//
// From this we get the following parse table ($ is end of input):
// 
//	t  f  variable  function  (  )  ,  binary_op  not  predicate  equal  quantifier  $
// SEN  1  1  1         1         1                   1    1         
// BIN                               2     3                                             2
// ATOM 6  6  6         6         4                   5    6                    
// ATOM'7  7  7         7         7                   7    7                 8   
// PROP 9  10 12        12                                 11                    
// TERM       14        15
// FUNC                 16
// OPTT                           18 17 17 17                         17                 17
// LIST       20        20           19
// MORE                              21 22
// OPTP       23        23           23                    24
//
// *****************************************************************

function setupLogicParser()
{
	// setup the parser to parse logical expressions

	// the second part of these parse nodes are not important
	var sentence = new ParseNode(NONTERMINAL, "SENTENCE");
	var opt_binary = new ParseNode(NONTERMINAL, "OPT_BINARY");
	var atomic = new ParseNode(NONTERMINAL, "ATOMIC");
	var atomic2 = new ParseNode(NONTERMINAL, "ATOMIC'");
	var prop = new ParseNode(NONTERMINAL, "PROPOSITION");
	var term = new ParseNode(NONTERMINAL, "TERM");
	var func = new ParseNode(NONTERMINAL, "FUNCTION");
	var opt_termlist = new ParseNode(NONTERMINAL, "OPT_TERMLIST");
	var termlist = new ParseNode(NONTERMINAL, "TERMLIST");
	var moreterms = new ParseNode(NONTERMINAL, "MORETERMS");
	var opt_predicate = new ParseNode(NONTERMINAL, "OPT_PREDICATE");

	var true_node = new ParseNode(TERMINAL, T_TRUE);
	var false_node = new ParseNode(TERMINAL, T_FALSE);
	var variable_node = new ParseNode(TERMINAL, T_VAR);
	var function_node = new ParseNode(TERMINAL, T_FUNCTION);
	var lparen = new ParseNode(TERMINAL, "(");
	var rparen = new ParseNode(TERMINAL, ")");
	var comma = new ParseNode(TERMINAL, ",");
	var binary_op = new ParseNode(TERMINAL, T_BINARY_OP);
	var not_node = new ParseNode(TERMINAL, T_NOT);
	var predicate = new ParseNode(TERMINAL, T_PREDICATE);
	var equal = new ParseNode(TERMINAL, T_EQUAL);
	var quantifier = new ParseNode(TERMINAL, T_QUANTIFIER);

	var use_prev = new ParseNode(ACTION, usePrevTokenFunc);

	// create the parse table
	var parseTable = new Array();

	parseTable[sentence] = new Array();
	parseTable[sentence][T_TRUE] = parseTable[sentence][T_FALSE] = 
		parseTable[sentence][T_VAR] = parseTable[sentence][T_FUNCTION] =
		parseTable[sentence][T_NOT] = parseTable[sentence][T_PREDICATE] = 
		parseTable[sentence]["("] = new Array(atomic, opt_binary);

	parseTable[opt_binary] = new Array();
	parseTable[opt_binary][")"] = parseTable[opt_binary][PARSE_END_INPUT] = new Array();
	parseTable[opt_binary][T_BINARY_OP] = new Array(binary_op, atomic, new ParseNode(ACTION, binaryFunc), opt_binary);

	parseTable[atomic] = new Array();
	parseTable[atomic]["("] = new Array(lparen, atomic2);
	parseTable[atomic][T_NOT] = new Array(not_node, atomic, new ParseNode(ACTION, notFunc));
	parseTable[atomic][T_TRUE] = parseTable[atomic][T_FALSE] = 
		parseTable[atomic][T_VAR] = parseTable[atomic][T_FUNCTION] = 
		parseTable[atomic][T_PREDICATE] = new Array(prop);

	parseTable[atomic2] = new Array();
	parseTable[atomic2][T_TRUE] = parseTable[atomic2][T_FALSE] = 
		parseTable[atomic2][T_VAR] = parseTable[atomic2][T_FUNCTION] =
		parseTable[atomic2][T_NOT] = parseTable[atomic2][T_PREDICATE] = 
		parseTable[atomic2]["("] = new Array(sentence, rparen);
	parseTable[atomic2][T_QUANTIFIER] = new Array(quantifier, opt_predicate, termlist, rparen, atomic, new ParseNode(ACTION, quantifierFunc));

	parseTable[prop] = new Array();
	parseTable[prop][T_TRUE] = new Array(true_node, use_prev);
	parseTable[prop][T_FALSE] = new Array(false_node, use_prev);
	parseTable[prop][T_PREDICATE] = new Array(predicate, opt_termlist, new ParseNode(ACTION, predOrFuncFunc));
	parseTable[prop][T_VAR] = parseTable[prop][T_FUNCTION] = 
		new Array(term, equal, term, new ParseNode(ACTION, equalFunc));

	parseTable[term] = new Array();
	parseTable[term][T_VAR] = new Array(variable_node, use_prev);
	parseTable[term][T_FUNCTION] = new Array(func);

	parseTable[func] = new Array();
	parseTable[func][T_FUNCTION] = new Array(function_node, opt_termlist, new ParseNode(ACTION, predOrFuncFunc));

	parseTable[opt_termlist] = new Array();
	parseTable[opt_termlist][")"] = parseTable[opt_termlist][","] = 
		parseTable[opt_termlist][T_BINARY_OP] = parseTable[opt_termlist][T_EQUAL] = 
		parseTable[opt_termlist][PARSE_END_INPUT] = new Array();
	parseTable[opt_termlist]["("] = new Array(lparen, termlist, rparen);

	var add_term = new ParseNode(ACTION, addTermFunc);

	parseTable[termlist] = new Array();
	parseTable[termlist][")"] = new Array();
	parseTable[termlist][T_VAR] = parseTable[termlist][T_FUNCTION] = new Array(term, add_term, moreterms);

	parseTable[moreterms] = new Array();
	parseTable[moreterms][")"] = new Array();
	parseTable[moreterms][","] = new Array(comma, term, add_term, moreterms);

	parseTable[opt_predicate] = new Array();
	parseTable[opt_predicate][T_VAR] = parseTable[opt_predicate][T_FUNCTION] = 
		parseTable[opt_predicate][")"] = new Array();
	parseTable[opt_predicate][T_PREDICATE] = new Array(predicate, use_prev);

	logicParser = new Parser(new ParseTable(parseTable, sentence), parseError, null, endLogicParse);
}

function parseError(errorMsg)
{
	alert (errorMsg);
}

function endLogicParse(parseTree)
{
	// what we care about is actually the attribute
	// which contains a TreeNode not the whole parseTree
	return (parseTree.attribute);
}

// *****************************************************************
// Parsing Functions
// *****************************************************************

// For all these functions, "this" refers to the ParseNode that we're at.
// Fill the attribute field with a TreeNode 
// This basically converts everything to TreeNodes (essentially getting rid
// of excess nodes like nonterminals)

function usePrevTokenFunc()
{
	// for all productions of the form
	// NONTERMINAL->terminal
	this.attribute = new TreeNode(this.getRelativeSibling(-1).token);

	return (true);
}

function notFunc()
{
	// ATOMIC->not ATOMIC
	this.attribute = new TreeNode(NOT, this.getRelativeSibling(-1).attribute);
	return (true);
}

function quantifierFunc()
{
	// first child is the quantified variable 
	// second is the quantified expression

	// ATOMIC' -> quantifier OPT_PREDICATE termlist ) ATOMIC

	// only allow quantification of variables
	// have to check termlist now

	var terms = this.getRelativeSibling(-3).attribute;
	var expr = this.getRelativeSibling(-1).attribute;	// quantified expression
	var quantifier = this.getRelativeSibling(-5).token.value;
	var predicate = this.getRelativeSibling(-4).attribute;

	if (!terms)
	{
		this.attribute = expr;

		parseError("Warning: nothing is being quantified. Ignoring quantifier.");
		return (true);
	}

	// relativized quantifiers - predicate must be unary
	if (predicate)
	{
		if (!checkArity(predicate.value, 1))
		{
			parseError("Predicates in relativized quantifiers must be unary.");
			return (false);
		}

		// (forall p x1, x2) is (forall x1, x2)(if p(x1) and p(x2) then ...)
		// (exists p x1, x2) is (exists x1, x2)(p(x1) and p(x2) and ...)

		var array = new Array();	// create array of p(x1), p(x2), etc
		for (var i = 0; i < terms.length - 1; i++)
			array[i] = new TreeNode(predicate.value, term);

		expr = new TreeNode((quantifier == FORALL ? IF : AND),
				naryToBinary(AND, array), expr);
	}

	// go backwards so (forall x,y) is treated as (forall x)(forall y)
	for (var i = terms.length - 1; i >= 0; i--)
	{
		if (terms[i].value.type != T_VAR)
		{
			parseError("Warning: only variables may be quantified. Ignoring term.");
		}
		else
		{
			expr = new TreeNode(quantifier, terms[i], expr);
		}
	}

	this.attribute = expr;

	return (true);
}

function binaryFunc()
{
	// OPT_BINARY -> binary_op ATOMIC
	// the first operand is whatever came right before the OPT_BINARY

	var operand2 = this.getRelativeSibling(-1);
	var operator = this.getRelativeSibling(-2);
	var operand1 = this.parent.getRelativeSibling(-1);

	// real binary operator is in the value of the token returned by the lexer
	this.attribute = new TreeNode(operator.token.value, operand1.attribute, operand2.attribute);
	return (true);
}

function equalFunc()
{
	// PROPOSITION->term equal term

	this.attribute = new TreeNode(EQUAL, 
		this.getRelativeSibling(-3).attribute, this.getRelativeSibling(-1).attribute);
	return (true);
}

function predOrFuncFunc()
{
	var terms = this.getRelativeSibling(-1).attribute;
	if (!terms)
		terms = new Array();
	var numTerms = terms.length;
	var token = this.getRelativeSibling(-2).token;		// function or predicate
	var root = new TreeNode(token);

	if (!checkArity(token, numTerms))
		return (false);

	// terms are added as children of the function or predicate
	// so a function with n arguments has n children

	for (var i = 0; i < numTerms; i++)
		root.addChild(terms[i]);

	this.attribute = root;

	return (true);
}

function addTermFunc()
{
	// TERMLIST->term this_func moreterms
	// or MORETERMS-> , term this_func moreterms

	// attribute type of the parent of this function is an array of terms

	if (!this.parent.attribute)
		this.parent.attribute = new Array();

	this.attribute = this.parent.attribute;

	this.attribute[this.attribute.length] = this.getRelativeSibling(-1).attribute;

	// pass the array down
	this.getRelativeSibling(1).attribute = this.attribute;

	return (true);
}

// *****************************************************************
// Simplifications
// These are listed on p. 38-41 of Manna and Waldinger
// *****************************************************************

function setupSimplifications()
{
	var F = getPlaceholder();
	var G = getPlaceholder();
	var trueNode = new TreeNode(TRUE);
	var falseNode = new TreeNode(FALSE);
	var notF = new TreeNode(NOT, F);
	var notG = new TreeNode(NOT, G);

	// all simplifications only go one way (no need for fourth argument)

	// true-false simplifications
	addEquivalentSchemas(simplifications, new TreeNode(NOT, trueNode), falseNode);
	addEquivalentSchemas(simplifications, new TreeNode(NOT, falseNode), trueNode);

	addEquivalentSchemas(simplifications, new TreeNode(AND, F, trueNode), F);
	addEquivalentSchemas(simplifications, new TreeNode(AND, trueNode, F), F);
	addEquivalentSchemas(simplifications, new TreeNode(AND, F, falseNode), falseNode);
	addEquivalentSchemas(simplifications, new TreeNode(AND, falseNode, F), falseNode);

	addEquivalentSchemas(simplifications, new TreeNode(OR, F, trueNode), trueNode);
	addEquivalentSchemas(simplifications, new TreeNode(OR, trueNode, F), trueNode);
	addEquivalentSchemas(simplifications, new TreeNode(OR, F, falseNode), F);
	addEquivalentSchemas(simplifications, new TreeNode(OR, falseNode, F), F);

	addEquivalentSchemas(simplifications, new TreeNode(IF, trueNode, G), G);
	addEquivalentSchemas(simplifications, new TreeNode(IF, falseNode, G), trueNode);
	addEquivalentSchemas(simplifications, new TreeNode(IF, F, trueNode), trueNode);
	addEquivalentSchemas(simplifications, new TreeNode(IF, F, falseNode), notF);

	addEquivalentSchemas(simplifications, new TreeNode(IFF, F, trueNode), F);
	addEquivalentSchemas(simplifications, new TreeNode(IFF, trueNode, F), F);
	addEquivalentSchemas(simplifications, new TreeNode(IFF, F, falseNode), notF);
	addEquivalentSchemas(simplifications, new TreeNode(IFF, falseNode, F), notF);

	// other simplifications
	addEquivalentSchemas(simplifications, new TreeNode(NOT, notF), F);
	addEquivalentSchemas(simplifications,
		new TreeNode(NOT, new TreeNode(AND, notF, notG)), new TreeNode(OR, F, G));
	addEquivalentSchemas(simplifications,
		new TreeNode(NOT, new TreeNode(OR, notF, notG)), new TreeNode(AND, F, G));
	addEquivalentSchemas(simplifications,
		new TreeNode(NOT, new TreeNode(IF, F, notG)), new TreeNode(AND, F, G));
	addEquivalentSchemas(simplifications,
		new TreeNode(NOT, new TreeNode(IFF, notF, G)), new TreeNode(IFF, F, G));
	addEquivalentSchemas(simplifications,
		new TreeNode(NOT, new TreeNode(IFF, F, notG)), new TreeNode(IFF, F, G));

	addEquivalentSchemas(simplifications, new TreeNode(AND, F, F), F);
	addEquivalentSchemas(simplifications, new TreeNode(AND, F, notF), falseNode);
	addEquivalentSchemas(simplifications, new TreeNode(AND, notF, F), falseNode);

	addEquivalentSchemas(simplifications, new TreeNode(OR, F, F), F);
	addEquivalentSchemas(simplifications, new TreeNode(OR, F, notF), trueNode);
	addEquivalentSchemas(simplifications, new TreeNode(OR, notF, F), trueNode);

	addEquivalentSchemas(simplifications, new TreeNode(IF, F, F), trueNode);
	addEquivalentSchemas(simplifications, new TreeNode(IF, notF, F), F);
	addEquivalentSchemas(simplifications, new TreeNode(IF, F, notF), notF);
	addEquivalentSchemas(simplifications,
		new TreeNode(IF, notG, notF), new TreeNode(IF, F, G));

	addEquivalentSchemas(simplifications, new TreeNode(IFF, F, F), trueNode);
	addEquivalentSchemas(simplifications, new TreeNode(IFF, F, notF), falseNode);
	addEquivalentSchemas(simplifications, new TreeNode(IFF, notF, F), falseNode);

	// quantifiers
	// F represents the variable
	// these are only applied if the variable does not occur free in G
	addEquivalentSchemas(simplifications, 
		new TreeNode(FORALL, F, G), G, false, simplifyCheckQuantifedVariableIsFree);
	addEquivalentSchemas(simplifications,
		new TreeNode(EXISTS, F, G), G, false, simplifyCheckQuantifedVariableIsFree);
}

function simplifyCheckQuantifedVariableIsFree(node, replacement)
{
	if (!variableOccursFree(getQuantifiedVariable(node), replacement))
		return (replacement);		// ok to remove quantifier
	else
		return (null);
}

function logicSimplify(node)
{
	// simplify node as much as possible and return a new simplified node
	var newnode = new TreeNode(node.value);

	// first simplify all the children
	for (var i = 0; i < node.children.length; i++)
	{
		newnode.addChild(logicSimplify(node.children[i]));
	}

	// now simplify this node until it can't be simplified
	while (true)
	{
		var simplified = findMatchingSchemas(simplifications, newnode);

		// should only be either 0 or 1 element in the simplified array
		// only one way to simplify any given expression
		if (simplified.length == 0)
			return (newnode);
		else
			newnode = simplified[0];	// just take first simplification
	}
}

// *****************************************************************
// Rewritings
// p. 68 of Manna and Waldinger
// *****************************************************************

function setupRewriteRules()
{
	var F = getPlaceholder();
	var G = getPlaceholder();
	var H = getPlaceholder();
	var x = getPlaceholder();	// quantified variables
	var y = getPlaceholder();

	// all rewrites can go both way (thus the 'true')
	// note however that some of them have false since for instance
	// commutativity 'F and G' and 'G and F' are identical

	// negation
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(NOT, new TreeNode(AND, F, G)), 
		new TreeNode(OR, new TreeNode(NOT, F), new TreeNode(NOT, G)), true);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(NOT, new TreeNode(OR, F, G)), 
		new TreeNode(AND, new TreeNode(NOT, F), new TreeNode(NOT, G)), true);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(NOT, new TreeNode(IF, F, G)), 
		new TreeNode(AND, F, new TreeNode(NOT, G)), true);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(NOT, new TreeNode(IFF, F, G)), 
		new TreeNode(IFF, F, new TreeNode(NOT, G)), true);

	// elimination
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(IF, F, G), new TreeNode(OR, new TreeNode(NOT, F), G), true);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(IFF, F, G), 
		new TreeNode(AND, new TreeNode(IF, F, G), new TreeNode(IF, G, F)), true);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(IFF, F, G), 
		new TreeNode(OR, 
			new TreeNode(AND, F, G),
			new TreeNode(AND, new TreeNode(NOT, F), new TreeNode(NOT, G))), true);

	// commutativity
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(AND, F, G), new TreeNode(AND, G, F), false);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(OR, F, G), new TreeNode(OR, G, F), false);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(IFF, F, G), new TreeNode(IFF, G, F), false);

	// associativity
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(AND, new TreeNode(AND, F, G), H), 
		new TreeNode(AND, F, new TreeNode(AND, G, H)), true);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(OR, new TreeNode(OR, F, G), H), 
		new TreeNode(OR, F, new TreeNode(OR, G, H)), true);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(IFF, new TreeNode(IFF, F, G), H), 
		new TreeNode(IFF, F, new TreeNode(IFF, G, H)), true);

	// distributivity
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(AND, F, new TreeNode(OR, G, H)),
		new TreeNode(OR, new TreeNode(AND, F, G), new TreeNode(AND, F, H)), true);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(OR, F, new TreeNode(AND, G, H)),
		new TreeNode(AND, new TreeNode(OR, F, G), new TreeNode(OR, F, H)), true);

	// quantifiers
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(FORALL, x, new TreeNode(FORALL, y, F)),
		new TreeNode(FORALL, y, new TreeNode(FORALL, x, F)), false);
	addEquivalentSchemas(possibleRewrites, 
		new TreeNode(EXISTS, x, new TreeNode(EXISTS, y, F)),
		new TreeNode(EXISTS, y, new TreeNode(EXISTS, x, F)), false);
	addEquivalentSchemas(possibleRewrites,
		new TreeNode(NOT, new TreeNode(FORALL, x, F)),
		new TreeNode(EXISTS, x, new TreeNode(NOT, F)), true);
	addEquivalentSchemas(possibleRewrites,
		new TreeNode(NOT, new TreeNode(EXISTS, x, F)),
		new TreeNode(FORALL, x, new TreeNode(NOT, F)), true);
	addEquivalentSchemas(possibleRewrites,
		new TreeNode(FORALL, x, new TreeNode(AND, F, G)),
		new TreeNode(AND, new TreeNode(FORALL, x, F), new TreeNode(FORALL, x, G)), true);
	addEquivalentSchemas(possibleRewrites,
		new TreeNode(EXISTS, x, new TreeNode(OR, F, G)),
		new TreeNode(OR, new TreeNode(EXISTS, x, F), new TreeNode(EXISTS, x, G)), true);
	addEquivalentSchemas(possibleRewrites,
		new TreeNode(EXISTS, x, new TreeNode(IF, F, G)),
		new TreeNode(IF, new TreeNode(FORALL, x, F), new TreeNode(EXISTS, x, G)), true);
}

function getPossibleRewrites(node)
{
	// returns an array of nodes, each of which can be used to rewrite the given node
	// also saves the information in the node for next time this is called

	if (!node.rewrites)
		node.rewrites = findMatchingSchemas(possibleRewrites, node);

	return (node.rewrites);
}

// *****************************************************************
// Polarity
// *****************************************************************

function calcPolarities(node)
{
	// calculate all polarities for everything rooted at node
	// assumes node currently already has an initial polarity
	node.traverse(doCalcPolarities);

	return (node);
}

function doCalcPolarities(node)
{
	// calculate polarities for the children of node
	// given node's polarity

	// can't do anything if we don't have a polarity
	if (!node.polarity)
		return;

	var token = node.value;

	if (token == NOT)
		node.children[0].polarity = oppositePolarity(node.polarity);
	else if ((token == AND) || (token == OR))
		node.children[0].polarity = node.children[1].polarity = node.polarity;
	else if (token == IF)
	{
		node.children[0].polarity = oppositePolarity(node.polarity);
		node.children[1].polarity = node.polarity;
	}
	else if (token == IFF)
		node.children[0].polarity = node.children[1].polarity = BOTH;
	else if (isQuantifier(node))
		node.children[1].polarity = node.polarity;

	return (node);
}

function oppositePolarity(polarity)
{
	if (polarity == POSITIVE)
		return (NEGATIVE);
	else if (polarity == NEGATIVE)
		return (POSITIVE);
	else
		return (BOTH);
}

// *****************************************************************
// Schemas
// A schema is simply a tree that contains PLACEHOLDERS
// *****************************************************************

function getPlaceholder()
{
	// return a new unique placeholder
	return (new TreeNode(new Token(PLACEHOLDER, nextPlaceholderId++)));
}

function matchSchema(schema, node, substitution)
{
	// matches a tree with a schema
	// returns a substitution that replaces for all the PLACEHOLDERS in schema
	// the actual values in node
	// returns null if node doesn't fit the given schema
	// third argument is optional

	var schemaToken = schema.value;
	var nodeToken = node.value;

	if (!substitution)
		substitution = new Substitution();

	if (schemaToken.type == PLACEHOLDER)
	{
		// must not already be in the substitution with something different
		var inSub = substitution.contains(schema);

		if (inSub)
		{
			if (!treeEqual(inSub, node))
				return (null);
			// else leave substitution as it is
		}
		else
			substitution.addPair(schema, node);
 		return (substitution);
	}
	else if (schemaToken != nodeToken)
		return (null);
	else if (schema.children.length != node.children.length)
		return (null);

	// try children
	var tryMatch;
	for (var i = 0; i < schema.children.length; i++)
	{
		tryMatch = matchSchema(schema.children[i], node.children[i], substitution);
		if (!tryMatch)
			return (null);
	}

	return (substitution);
}


function addEquivalentSchemas(schemaList, schema1, schema2, addReverse, func)
{
	// schema1 and schema2 should be equivalent sentence schema
	// schemaList is an array
	// will add to the list that schema1 is equivalent to schema2
	// if addReverse then it will also add that schema2 is equivalent to schema1
	// if func is given, then func() will be called when something matches
	// schema1. The value returned from func will be used instead of schema2.
	// see findMatchingSchemas()

	var token1 = schema1.value;
	if (!schemaList[token1])
		schemaList[token1] = new Array();

	var array = new Array();
	array[0] = schema1;
	array[1] = schema2;
	if (func)
		array[2] = func;
	schemaList[token1][schemaList[token1].length] = array;

	if (addReverse)
		addEquivalentSchemas(schemaList, schema2, schema1, false);
}

function findMatchingSchemas(schemaList, node)
{
	// goes through schemaList and finds schema that match node
	// for each matching schema, finds the schema that is equivalent to it
	// return an array of nodes that is equivalent to the given node
	var token = node.value;
	var array = new Array();
	var lookupArray = schemaList[token];

	if (!lookupArray)
		return (array);		// empty array

	var match;
	for (var i = 0; i < lookupArray.length; i++)
	{
		match = matchSchema(lookupArray[i][0], node);

		if (match)
		{
			// replace placeholders in the equivalent schema
			var replacement = match.applyTo(lookupArray[i][1]);

			// check if a function was given to be called
			// call with two arguments. the original node, and a possible replacement
			if (lookupArray[i][2])
				replacement = lookupArray[i][2](node, replacement);

			if (replacement)
				array[array.length] = replacement;
		}
	}

	return (array);
}

// *****************************************************************
// Unifiers
// *****************************************************************

function getUnifier(expr1, expr2)
{
	// returns a Substitution that unifies expr1 and expr2
	// or null if the two are not unifiable

	var unifier = new Substitution();
	var totalUnifier = new Substitution();
	var token1;
	var token2;

	token1 = expr1.value;
	token2 = expr2.value;

	if (token1 != token2)
	{
		if (token1.type == token2.type)
		{
			// same type
			if (token1.type == T_VAR)
			{
				unifier.addPair(expr1, expr2);
			}
			else
			{
				// FUNCTION or PREDICATE
				// have to be the same symbol
				return (null);
			}
		}
		else
		{
			// one must be a variable if two tokens have different types
			if ((token1.type != T_VAR) && (token2.type != T_VAR))
				return (null);

			// the occurs-check
			// the variable to be substituted can't be in the other expression
			if (token1.type == T_VAR)
			{
				if (expr2.find(token1))
					return (null);		// found - not good
				else
					unifier.addPair(expr1, expr2);
			}
			else	// token2.type == T_VAR
			{
				if (expr1.find(token2))
					return (null);
				else
					unifier.addPair(expr2, expr1);
			}
		}

		expr1 = unifier.applyTo(expr1);
		expr2 = unifier.applyTo(expr2);

		totalUnifier = totalUnifier.compose(unifier);
	}

	// after above, expr1.value == expr2.value

	// unify children

	if (expr1.children.length != expr2.children.length)
		return (null);

	for (var i = 0; i < expr1.children.length; i++)
	{
		unifier = getUnifier(expr1.children[i], expr2.children[i]);
		if (!unifier)
			return (null);

		expr1 = unifier.applyTo(expr1);
		expr2 = unifier.applyTo(expr2);
		totalUnifier = totalUnifier.compose(unifier);
	}

	return (totalUnifier);
}

function getMostGeneralUnifier(nodes, startUnifier)
{
	// pass in array of nodes to unify
	// returns a unifier that unifies all expressions or null
	// optional second argument is a unifier that is first applied to all the nodes

	var unifier = new Substitution();
	var mgu = startUnifier ? startUnifier : new Substitution();	// most general unifier

	for (var i = 1; i < nodes.length; i++)
	{
		unifier = getUnifier(mgu.applyTo(nodes[i-1]), mgu.applyTo(nodes[i]));

		if (!unifier)
			return (null);
		else
			mgu = mgu.compose(unifier);
	}

	return (mgu);
}

function getMostGeneralSeparateUnifier(group1, group2)
{
	// pass in two arrays of nodes
	// returns a unifier that unifies both group1 and group2
	// but after unification the two groups may still be distinct from each other

	var mgsu = getMostGeneralUnifier(group1);

	if (!mgsu)
		return (null);

	return (getMostGeneralUnifier(group2, mgsu));
}

// *****************************************************************
// Substitution
// *****************************************************************

function Substitution()
{
	// list of replacement pairs F <- G

	this.pairs = new Array();
	this.applyTo = applySubstitution;
	this.contains = substitutionContains;
	this.addPair = addSubstitutionPair;
	this.compose = composeSubstitution;
	this.toString = substitutionToString;
}

function substitutionContains(F)
{
	// check if substitution contains a substitution for F
	// and returns what would be substituted for F
	// else return null
	for (var i = 0; i < this.pairs.length; i++)
	{
		if (treeEqual(F, this.pairs[i][0]))
			return (this.pairs[i][1]);
	}
	return (null);
}

function addSubstitutionPair(F, G)
{
	// replace occurrences of F with G
	// add this pair to the substitution
	// this returns false if F is already in the substitution
	// or if F == G
	// and returns true otherwise

	if (this.contains(F))
		return (false);

	if (treeEqual(F, G))
		return (false);

	this.pairs[this.pairs.length] = new Array(F, G);	// ok substitution
}


function applySubstitution(expr, safe)
{
	// apply this substitution to the expr
	// performs a total substitution returning a new node
	// if safe, then a total safe substitution is performed
	// that is, only free occurrences are replaced
	// and if a variable is to be captured, rename the bound variable

	var i;

	// can't substitute if it isn't free
	if (!safe || isFreeSubexpression(expr))
	{
		// try to find a substitution for this node
		for (i = 0; i < this.pairs.length; i++)
		{
			if (treeEqual(expr, this.pairs[i][0]))
			{
				var replacement = this.pairs[i][1].clone();
				if (safe)
				{
					// avoid capturing
					var tempnode = expr.parent;

					while (tempnode)
					{
						// if the variable is free it will be captured
						if (isQuantifier(tempnode) && 
							(variableOccursFree(getQuantifiedVariable(tempnode), replacement)))
						{
							renameBoundVariables(tempnode);
						}
						tempnode = tempnode.parent;
					}
				}
				return (replacement);
			}
		}
	}

	var newnode = expr.clone();

	// apply substitutions to the children of this new node

	for (i = 0; i < newnode.children.length; i++)
	{
		newnode.children[i].replaceWith(this.applyTo(newnode.children[i]), safe);
	}

	return (newnode);
}

function composeSubstitution(sub2)
{
	// return the composition of this and sub2
	// that is returns a composition that when applied to an expression
	// is equivalent to first applying this composition followed by sub2
	// note this composition is not commutative

	var newSub = new Substitution();

	var i;
	for (i = 0; i < this.pairs.length; i++)
	{
		// result of pairs in this substitution
		// by first applying this substitution followed by sub2
		newSub.addPair(this.pairs[i][0], sub2.applyTo(this.pairs[i][1]));
	}

	for (i = 0; i < sub2.pairs.length; i++)
	{
		// and then result of just applying substitutions in sub2
		newSub.addPair(sub2.pairs[i][0], sub2.pairs[i][1]);
	}

	return (newSub);
}

function substitutionToString()
{
	var str = "{";
	var first = true;
	var i;
	for (i = 0; i < this.pairs.length; i++)
	{
		if (!first)
			str += ", ";
		else
			first = false;

		str += this.pairs[i][0] + " <- " + this.pairs[i][1];
	}
	str += "}";

	return (str);
}

// *****************************************************************
// Functions to deal with quantifiers
// *****************************************************************

function eliminateUniversalForceQuantifier(node)
{
	// node should be a quantifier with universal force
	// this quantifier will be eliminated by the skolemization rules

	var quantifiers = getAllSurroundingQuantifiers(node);

	// these are the arguments to the new function symbol to be used
	// free variables and all variables bound by quantifiers of existential
	// force go into here
	var args = new Array();

	var freeVars = findFreeVariables(node.getTreeTop());
	var variable;

	for (i in freeVars)	// i is the variable name (i.e. "x")
		args[args.length] = freeVars[i][0].value;	// need variable token

	for (var i = 0; i < quantifiers.length; i++)
	{
		if (getQuantifierForce(quantifiers[i]) == EXISTENTIAL_FORCE)
		{
			variable = getQuantifiedVariable(quantifiers[i]);

			if (freeVars[variable])
			{
				// also a free variable - rename
				// and get new variable
				variable = renameBoundVariables(quantifiers[i]).value;
			}

			// add to arg list
			args[args.length] = variable;
		}
	}

	var replacement;
	if (args.length == 0)
		replacement = new TreeNode(getNewConstant());
	else
	{
		replacement = new TreeNode(getNewFunction());

		for (var i = 0; i < args.length; i++)
		{
			replacement.addChild(new TreeNode(args[i]));
		}
	}

	renameBoundVariables(node, replacement);

	// now we drop the quantifier
	node.replaceWith(node.children[1]);
	return (doSkolemize(node));	
}

function eliminateExistentialForceQuantifier(node)
{
	// node is a quantifier of existential force
	// will try to be eliminated

	var renamed = false;
	var variable = getQuantifiedVariable(node);

	var quantifiers = getAllSurroundingQuantifiers(node);

	for (var i = 0; i < quantifiers.length; i++)
	{
		// must not be in the scope of any quantifier of universal force
		// otherwise we just leave this quantifier
		if (getQuantifierForce(quantifiers[i]) == UNIVERSAL_FORCE)
		{
			doSkolemize(node.children[1]);
			return (node);
		}

		if (!renamed &&
			(getQuantifiedVariable(quantifiers[i]) == variable))
		{
			// have to rename our variable
			renameBoundVariables(node);
			renamed = true;
		}

	}

	// if the quantified variable occurs free
	// in the top level expression, then we also need to
	// rename since we are going to just drop the quantifier
	if (!renamed)
	{
		if (variableOccursFree(variable, node.getTreeTop()))
		{
			renameBoundVariables(node);
			renamed = true;
		}
	}

	// now we drop the quantifier
	node.replaceWith(node.children[1]);
	return (doSkolemize(node));
}

function doSkolemize(node)
{
	// remove quantifiers with strict force from node
	// return node after removal of quantifiers
	// quantifiers are removed in place
	// so tree structure of node will be preserved
	// although the nodes themselves won't be preserved

	if (isQuantifier(node))
	{
		var force = getQuantifierForce(node);

		if (force == BOTH_FORCES)
		{
			// can't get rid of this
			// and any quantifier under here will also have both forces
			return (node);
		}
		else
		{
			if (force == UNIVERSAL_FORCE)
				node = eliminateUniversalForceQuantifier(node);
			else if (force == EXISTENTIAL_FORCE)
				node = eliminateExistentialForceQuantifier(node);
		}
	}
	else
	{
		for (var i = 0; i < node.children.length; i++)
		{
			node.children[i].replaceWith(doSkolemize(node.children[i]));
		}
	}

	return (node);
}

function isQuantifierFree(node)
{
	// returns true if node doesn't contain any quantifiers
	return (!node.find(FORALL) && !node.find(EXISTS));
}

function getSurroundingQuantifier(node)
{
	// finds the first quantifier that has node in its scope
	// or null if none
	var parent = node.parent;
	while (parent)
	{
		if (isQuantifier(parent))
			return (parent);
		parent = parent.parent;
	}
	return (null);
}

function getAllSurroundingQuantifiers(node)
{
	// returns an array of all quantifiers surrounding node
	var array = new Array();
	var quantifier = node;

	while (quantifier)
	{
		quantifier = getSurroundingQuantifier(node);

		if (!quantifier)
			break;

		array[array.length] = quantifier;

		node = node.parent;
	}
	return (array);
}

function isFreeSubexpression(node)
{
	// returns true if node does not contain any variable that is bound
	// by a quantifier surrounding this node
	var variable;
	var quantifiers = getAllSurroundingQuantifiers(node);

	for (var i = 0; i < quantifiers.length; i++)
	{
		variable = quantifiers[i].chlidren[0].value;

		// this variable must not occur free from node down
		// otherwise it would be bound to this quantifier
		if (variableOccursFree(variable, node))
		{
			return (false);
		}
	}
	return (true);
}

function findFreeVariables(node, free, bound)
{
	// return an array of all variables free in node
	// with all the occurrences (nodes) of that free variable
	// (i.e. returnVal["x"] is an array of nodes that have x as a free variable)
	// all arguments after the first are optional and used internally

	if (!free)
		free = new Array();
	if (!bound)
		bound = new Array();

	var token = node.value;

	if (token.type == T_VAR)
	{
		// check if it is bound in this scope
		var find = arrayfind(bound, token.value);
		if (find == -1)
		{
			var array = free[token.value];
			if (!array)
			{
				array = free[token.value] = new Array();
			}
			array[array.length] = node;
		}
	}
	else if (isQuantifier(node))
	{
		// add a bound variable in this scope
		bound[bound.length] = getQuantifiedVariable(node).value;

		findFreeVariables(node.children[1], free, bound);

		// now remove it
		bound.length--;
	}
	else
	{
		for (var i = 0; i < node.children.length; i++)
			findFreeVariables(node.children[i], free, bound);
	}

	return (free);
}

function variableOccursFree(variable, node)
{
	// returns true if there is at least one occurrence of variable
	// that is not bound to any quantifier in node

	var freeVars = findFreeVariables(node);

	return (freeVars[variable.value] != null);
}

function findBoundNodes(node)
{
	// node should be a quantifier
	// will return an array of variable nodes that are bound by this quantifier

	assert(isQuantifier(node), "findBoundNodes", "invalid node");

	// nodes that are bound by this quantifier have this variable free
	// when you remove this quantifier
	var variable = getQuantifiedVariable(node);
	var freeVars = findFreeVariables(node.children[1]);
	return (freeVars[variable.value]);
}

function renameBoundVariables(node, replacement)
{
	// node should be a quantifier
	// will rename the quantified variable and all places
	// that the variable is bound in node 
	// if replacement is not given, then a new variable name will be used
	// returns the replacement node
	var boundNodes = findBoundNodes(node);

	if (!replacement)
		replacement = new TreeNode(getNewVariable());

	node.children[0].replaceWith(replacement.clone());

	for (var i = 0; i < boundNodes.length; i++)
		boundNodes[i].replaceWith(replacement.clone());

	return (replacement);
}

function renameFreeVariable(variableName, node)
{
	// rename all free occurrences of variable in node to a new variable name

	var freeVars = findFreeVariables(node);
	var array = freeVars[variableName];

	if (array)
	{
		var newVar = getNewVariable();
		for (var i = 0; i < array.length; i++)
		{
			array[i].value = newVar;
		}
	}
}

function renameCommonFreeVariables(node1, node2)
{
	// renames all the free variables in node2 that also occur in node1
	var free1 = findFreeVariables(node1);

	for (var i in free1)
	{
		renameFreeVariable(i, node2);
	}
}

function getQuantifierForce(node)
{
	assert(isQuantifier(node) && node.polarity, "getQuantifierForce", "invalid node");

	var token = node.value;

	if (node.polarity == BOTH)
		return (BOTH_FORCES);
	else if (node.polarity == POSITIVE)
	{
		if (token == FORALL)
			return (UNIVERSAL_FORCE);
		else
			return (EXISTENTIAL_FORCE);
	}
	else
	{
		if (token == FORALL)
			return (EXISTENTIAL_FORCE);
		else
			return (UNIVERSAL_FORCE);

	}
}

function getQuantifiedVariable(node)
{
	// returns the variable token that represents the quantified variable
	assert(isQuantifier(node), "getQuantifiedVariable", "invalid node");
	return (node.children[0].value);
}

// *****************************************************************
// Utilities
// *****************************************************************

function isQuantifier(node)
{
	return ((node.value == FORALL) || (node.value == EXISTS));
}

function isUnary(node)
{
	return ((node.value == NOT) || isQuantifier(node));
}

function isLogicalBinary(node)
{
	// note this doesn't include EQUAL
	return ((node.value == AND) || (node.value == OR) || 
		(node.value == IF) || (node.value == IFF));
}

function getUnusedIdentifier(type, prefix)
{
	// returns a token of the given type that is not currently
	// in the symbol table by adding numbers to the end of prefix
	var num = 1;
	while (true)
	{
		var name = prefix + num++;
		if (!symbolTable[name])
			return (defineIdentifier(type, name, true));
	}
}

function getNewVariable()
{
	return (getUnusedIdentifier(T_VAR, NEW_VARIABLE_PREFIX));
}

function getNewFunction()
{
	return (getUnusedIdentifier(T_FUNCTION, NEW_FUNCTION_PREFIX));
}

function getNewConstant()
{
	return (getUnusedIdentifier(T_FUNCTION, NEW_CONSTANT_PREFIX));
}

function naryToBinary(operator, array)
{
	// operator should be a binary operator
	// array is an array of TreeNodes
	// will return a new node with all of the elements of the array
	// combined using operator
	// so if operator == AND, will return array[0] AND array[1] AND array[2] ...

	if (array.length == 0)
		return (null);
	else if (array.length == 1)
		return (array[0]);

	var newnode = new TreeNode(operator, array[0], array[1]);
	for (var i = 2; i < array.length; i++)
	{
		newnode = new TreeNode(operator, newnode, array[i]);
	}
	return (newnode);
}

// *****************************************************************
// logicUnparse(): generic function to convert a TreeNode to a string
// *****************************************************************

function logicUnparse(node, func, afterFunc, param, insertComma)
{
	// converts node to a string
	// for each subexpression of node, calls func(node, str, param)
	// where str is part of the string representation of node
	// note that node can be null for strings that aren't intrinsically part of any node
	// afterFunc(node, param) is called at the end of the processing of every node
	//
	// insertComma is optional argument only used by this function to insert commas in termlists

	var token = node.value;
	var type = token.type;

	// check if we should insert a comma
	if (insertComma)
		func(null, ",", param);

	if ((token == TRUE) || (token == FALSE))
		func(node, OUTPUT_SYMBOLS[token.type], param);
	else if ((type == T_PREDICATE) || (type == T_VAR) || (type == T_FUNCTION))
	{
		var text;
		var hasArguments = ((type != T_VAR) && (node.children.length != 0))

		if (hasArguments)
			text = token.value + "(";
		else
			text = token.value;

		func(node, text, param);

		// put in arguments if any for predicates and functions
		if (hasArguments)
		{
			// insert a comma before all but the first argument
			logicUnparse(node.children[0], func, afterFunc, param);
			for (var i = 1; i < node.children.length; i++)
				logicUnparse(node.children[i], func, afterFunc, param, true);

			func(node, ")", param);	// closing paren
		}
	}
	else if (token == NOT)
	{
		func(node, OUTPUT_SYMBOLS[token.type], param);
		logicUnparse(node.children[0], func, afterFunc, param);
	}
	else if ((token == FORALL) || (token == EXISTS))
	{
		// collapse many of same quantifiers into one
		// (forall x)(forall y) should be output as (forall x,y)
		var variables = getQuantifiedVariable(node).value
		var expr = node.children[1];	// quantified expression

		while (expr.value == token)
		{
			// same type of quantifier
			variables += "," + getQuantifiedVariable(expr).value;
			expr = expr.children[1];
		}
		func(node, "(" + OUTPUT_SYMBOLS[token.type] + " " + variables + ")", param);
		logicUnparse(expr, func, afterFunc, param);
	}
	else if (node.children.length == 2)
	{
		// binary operator (EQUAL is also handled in here)

		// check if we need parenthesis around this expression
		var needParens = false;

		// only three precedences in our grammar and everything is left to right associative
		if (node.parent)
		{
			// don't need parenthesis if we're at the top
			if (isUnary(node.parent))
				needParens = true;	// unary higher precedence than binary
			else if (isLogicalBinary(node.parent))
			{
				// need to check associativity
				// if we're the left child, everything is ok
				// otherwise we need parenthesis
				if (node.childNum != 0)
					needParens = true;	// not left child
			}
			// else we don't need parenthesis
		}

		if (needParens)
			func(node, "(", param);

		logicUnparse(node.children[0], func, afterFunc, param);
		func(node, OUTPUT_SYMBOLS[token.type], param);
		logicUnparse(node.children[1], func, afterFunc, param);

		if (needParens)
			func(node, ")", param);
	}
	else if (type == PLACEHOLDER)
		func(null, PLACEHOLDER + token.value, param);

	if (afterFunc)
		afterFunc(node, param);
}

// *****************************************************************
// treeNodeToString(): returns a string representation of a node
// 	overrides the toString method of TreeNode
// *****************************************************************

function doNodeToString(node, str, stringWrapper)
{
	if (!node)
		stringWrapper.value += str;
	else if (isLogicalBinary(node))
		stringWrapper.value += " " + str + " ";
	else if (isUnary(node))
		stringWrapper.value += str + " ";
	else
		stringWrapper.value += str;
}

function treeNodeToString()
{
	// use an object wrapper since we want to change the string
	// and so need it to be passed by reference
	var str = new ObjectWrapper("");
	logicUnparse(this, doNodeToString, null, str);

	return (str.value);
}

// *****************************************************************
// logicParse(str): an entry point
// *****************************************************************

function logicParse(str)
{
	return (logicParser.parse(new LogicLexer(str)));
}

// *****************************************************************
// Initialization
// *****************************************************************

function initializeLogicSystem()
{
	setupLogicParser();
	setupSimplifications();
	setupRewriteRules();
}

initializeLogicSystem();

// Stop hiding -->