net.sourceforge.czt.rules.unification

Class Unifier

java.lang.Object

net.sourceforge.czt.rules.unification.Unifier

public class Unifier
extends Object

Unification of ASTs.

The unify methods in this class assume that all the jokers in both ASTs implement the Joker interface. They also assume that, if a joker gets bound to a term, automatically all jokers of the same type and with the same name get bound to that term. The ProverFactory should be used to ensure these properties.

Author:

Petra Malik

Field Summary

Fields

Modifier and Type	Field and Description
static int	maxDepth_ Unifications deeper than this fail! This is a convenient way of detecting infinite loops in the unification algorithms.
static int	printDepth_ Unifications deeper than this are printed.

Constructor Summary

Constructors

Constructor and Description
Unifier()

Method Summary

Modifier and Type	Method and Description
Set<net.sourceforge.czt.zpatt.ast.Binding>	getBindings()
UnificationException	getCause()
void	provideCause(boolean value)
boolean	unify(Object o1, Object o2)
boolean	unify(net.sourceforge.czt.base.ast.Term term1, net.sourceforge.czt.base.ast.Term term2) Unifies two terms (with occurs check).

Methods inherited from class java.lang.Object

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

Field Detail

printDepth_

public static int printDepth_

Unifications deeper than this are printed. Set it to -1 if you never want to print them.

maxDepth_

public static int maxDepth_

Unifications deeper than this fail! This is a convenient way of detecting infinite loops in the unification algorithms. Set it to -1 to turn off this feature.

Constructor Detail

Unifier

public Unifier()

Method Detail

getBindings

public Set<net.sourceforge.czt.zpatt.ast.Binding> getBindings()

getCause

public UnificationException getCause()

provideCause

public void provideCause(boolean value)

unify

public boolean unify(Object o1,
                     Object o2)

unify

public boolean unify(net.sourceforge.czt.base.ast.Term term1,
                     net.sourceforge.czt.base.ast.Term term2)

Unifies two terms (with occurs check).

Parameters:

term1 - the first term.

term2 - the second term.

Returns:

true if both terms unify, false otherwise.