jdrew.oo.td
Class Unifier

java.lang.Object
  jdrew.oo.td.Unifier

public class Unifier
extends java.lang.Object

A Unifier is an object that performs two separate functions: it tells whether two clauses literals that occur in Goals/GoalLists clauses can unify, and it builds the resulting Goals/GoalLists after the required substitution, required for the unification, have been applied. In this case a DCTree.Goal and DCTree.GoalList are always used

Field Summary

boolean	down This value is should be set to true if the unification is taking place when travelling down the tree, and false when returning back up.
boolean	unified This value is set to true if unification of the Goal and the first Goal in the subGoalList is successful, false otherwise.

Constructor Summary

Unifier(BackwardReasoner.Goal goal, BackwardReasoner.GoalList subGoalList, int mode)
Constructs a new Unifier for the OO-jDREW top-down module.

Unifier(BackwardReasoner.Goal goal, BackwardReasoner.GoalList subGoalList, int mode, boolean down)
Constructs a new Unifier for the OO-jDREW top-down module.

Method Summary

void	applyToGoal() Used to apply the variable bindings to the current goal.
void	applyToGoalList() Used to apply variable bindings to the sub goal list.

Methods inherited from class java.lang.Object

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

Field Detail

unified

public boolean unified

This value is set to true if unification of the Goal and the first Goal in the subGoalList is successful, false otherwise. It should always be checked to see if it is set to true before calling the applyToGoal() or applyToGoalList() methods, as they will throw a RuntimeException if unification was not successful.

down

public boolean down

This value is should be set to true if the unification is taking place when travelling down the tree, and false when returning back up. This indication is necessary to have proper type unification.

Constructor Detail

Unifier

public Unifier(BackwardReasoner.Goal goal,
               BackwardReasoner.GoalList subGoalList,
               int mode,
               boolean down)

Constructs a new Unifier for the OO-jDREW top-down module.

Parameters:

goal - jDREW.oo.td.DCTree.Goal value - a DCTree.Goal value of the current goal

subGoalList - jDREW.oo.td.DCTree.GoalList value - a DCTree.GoalList value of the current subGoals

mode - int value - an int for the mode - this should be Unifier.DCTREE_MODE

down - boolean value - Tells the unifier if this is going up or down the tree, use for applying type bindings correctly.

Unifier

public Unifier(BackwardReasoner.Goal goal,
               BackwardReasoner.GoalList subGoalList,
               int mode)

Constructs a new Unifier for the OO-jDREW top-down module. This is the same as calling the Unifier(DCTree.Goal goal, DCTree.GoalList subGoalList, int mode, boolean down) constructor with down set to false.

Parameters:

goal - jDREW.oo.td.DCTree.Goal value - a DCTree.Goal value of the current goal

subGoalList - jDREW.oo.td.DCTree.GoalList value - a DCTree.GoalList value of the current subGoals

mode - int value - an int for the mode - this should be Unifier.DCTREE_MODE

Method Detail

applyToGoal

public void applyToGoal()

Used to apply the variable bindings to the current goal. Should only be called if unified is set to true.

applyToGoalList

public void applyToGoalList()

Used to apply variable bindings to the sub goal list. Should only be called if unified is set to true.