jtp.fol
Class SubstUtils

java.lang.Object
  |
  +--jtp.fol.SubstUtils

public class SubstUtils

extends Object

Utility methods for use with instances of Substitutable and its subclasses.

Constructor Summary

SubstUtils()

Method Summary

static SubstitutableList	createList(Collection args) Returns instance of SubstitutableList that contains elements of Collection args.
static Clause	deReferenceClause(Clause cl) Returns a Clause based on cl in which Variables in its literals' arguments have been replaced by the values that they are bound to.
static Literal	deReferenceLiteral(Literal inputLiteral) Returns a Literal based on inputLiteral in which Variables in its arguments have been replaced by the values that they are bound to.
static CNFSentence	deReferenceSentence(CNFSentence s) Returns a CNFSentence based on s in which Variables in its clauses' literals' arguments have been replaced by the values that they are bound to.
static String	print(Object o) Printing method for sentences.
static String	printClause(Clause cl) Printing method for Clauses.
static String	printCNFSentence(CNFSentence s) Printing method for CNFSentences.
static String	printLiteral(Literal lit) Printing method for Literals.
static String	printSymbol(Symbol sym) Printing method for Symbols.
static CNFSentence	replaceVariables(CNFSentence s) Replaces all Variables in a sentence.
static Object	replaceVariables(Unifyable u) Replaces all Variables in a Unifyable.
protected static Object	substitute(Object o, Map m) If Object o is a key in mapping m, returns value that o is mapped to.
static Literal	substituteLiteral(Literal l, Map m) Uses mapping m to substitute arguments of Literal l that are (or contain) keys of mapping with values in mapping.
static void	unbindStack(List stack, int sz) Unbinds each variable in stack.
static boolean	unify(Object o1, Object o2, List varStack) Attempts to make two Objects equal by unifying them if either Object is a Unifyable.
static boolean	variableIndependentEquals(CNFSentence s1, CNFSentence s2) Determines if two sentences are identical even though they contain different free variables.
static int	variableIndependentHashCode(CNFSentence s) Hash code function for sentences that returns same value for arguments that are variableIndependentEquals.
static Map	variableStackToMap(List varStack, Map m) Given a List of Variables, returns a Map in which the keys are the Variables and the values are the Variables' dereferenced values.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

SubstUtils

public SubstUtils()

Method Detail

substitute

protected static Object substitute(Object o,
                                   Map m)

If Object o is a key in mapping m, returns value that o is mapped to. If o is a Substitutable, returns substitution of o using m. Otherwise, returns o.

Parameters:

o - Object to be substituted

m - substitution mapping

Returns:

substituted object

substituteLiteral

public static Literal substituteLiteral(Literal l,
                                        Map m)

Uses mapping m to substitute arguments of Literal l that are (or contain) keys of mapping with values in mapping. Returns substituted Literal.

Parameters:

l - Literal whose arguments are to be substituted

m - substitution mapping

Returns:

substituted Literal

createList

public static final SubstitutableList createList(Collection args)

Returns instance of SubstitutableList that contains elements of Collection args. Order of elements in returned list is same as order in which they are returned by args iterator.

Parameters:

args - a Collection of elements

Returns:

a SubstitutableList that contains same elements as args

unbindStack

public static final void unbindStack(List stack,
                                     int sz)

Unbinds each variable in stack. Assumes that all elements of stack are Variables.

Parameters:

stack - List of Variables

sz - length of stack

print

public static String print(Object o)

Printing method for sentences.

Parameters:

o - a Literal, Clause, or CNFSentence, or an Object or String that is a Literal argument

Returns:

String representation of o

printClause

public static final String printClause(Clause cl)

Printing method for Clauses.

Parameters:

cl - a Clause

Returns:

String representation of cl

printLiteral

public static final String printLiteral(Literal lit)

Printing method for Literals.

Parameters:

lit - a Literal

Returns:

String representation of lit

printCNFSentence

public static final String printCNFSentence(CNFSentence s)

Printing method for CNFSentences.

Parameters:

s - a CNFSentence

Returns:

String representation of s

printSymbol

public static final String printSymbol(Symbol sym)

Printing method for Symbols.

Parameters:

sym - a Symbol

Returns:

String representation of sym

deReferenceLiteral

public static final Literal deReferenceLiteral(Literal inputLiteral)

Returns a Literal based on inputLiteral in which Variables in its arguments have been replaced by the values that they are bound to.

Parameters:

inputLiteral - a Literal optionally containing Unifyable arguments

Returns:

Literal in which Variables in arguments have been replaced by their bound values. If no Variables needed dereferencing, returns inputLiteral.

See Also:

Variable

deReferenceClause

public static final Clause deReferenceClause(Clause cl)

Returns a Clause based on cl in which Variables in its literals' arguments have been replaced by the values that they are bound to.

Parameters:

cl - a Clause

Returns:

a Clause in which Variables have been replaced by their bound values. If no Variables needed dereferencing, returns cl.

See Also:

Variable

deReferenceSentence

public static final CNFSentence deReferenceSentence(CNFSentence s)

Returns a CNFSentence based on s in which Variables in its clauses' literals' arguments have been replaced by the values that they are bound to.

Parameters:

s - a CNFSentence

Returns:

a CNFSentence in which Variables have been replaced by their bound values. If no Variables needed dereferencing, returns s.

See Also:

Variable

variableStackToMap

public static Map variableStackToMap(List varStack,
                                     Map m)

Given a List of Variables, returns a Map in which the keys are the Variables and the values are the Variables' dereferenced values. If m is provided, uses and returns it. Otherwise, creates an ArrayMap or TreeMap depending on the size of varStack.

This method is useful for for generating bindings for Proofs.

Parameters:

varStack - a List of Variables

m - the Map that the Variables and their values will be put in

Returns:

a Map containing the Variables in varStack and their values

replaceVariables

public static Object replaceVariables(Unifyable u)

Replaces all Variables in a Unifyable. Unbound Variables are replaced by new Variables with same names; bound Variables are replaced by their values.

Parameters:

u - a Unifyable that is to have its Variables replaced

Returns:

a Unifyable based on u with Variables replaced as described above

replaceVariables

public static CNFSentence replaceVariables(CNFSentence s)

Replaces all Variables in a sentence. Unbound Variables are replaced by new Variables with same names; bound Variables are replaced by their values.

Parameters:

s - a CNFSentence that is to have its Variables replaced

Returns:

a CNFSentence based s with Variables replaced as described above

unify

public static boolean unify(Object o1,
                            Object o2,
                            List varStack)

Attempts to make two Objects equal by unifying them if either Object is a Unifyable. If neither Object is a Unifyable, they can be unified if they are equal.

Parameters:

o1 - Object to unify

o2 - Object to unify

varStack - List in which Variables that are bound during this unification will be placed

Returns:

true if unifcation succeeded; false otherwise

variableIndependentEquals

public static boolean variableIndependentEquals(CNFSentence s1,
                                                CNFSentence s2)

Determines if two sentences are identical even though they contain different free variables. For example, (p ?x ?y) and (p ?w ?z) would be considered identical, but (p A ?x) and (p B ?x) are not identical.

Parameters:

s1 - CNFSentence for comparison

s2 - CNFSentence for comparison

Returns:

true if sentences are equal independent of free variables; false otherwise

variableIndependentHashCode

public static int variableIndependentHashCode(CNFSentence s)

Hash code function for sentences that returns same value for arguments that are variableIndependentEquals.

Parameters:

s - CNFSentence whose hash code is to be computed

Returns:

hash code of sentence