model

Class EqualSolutionNode

java.lang.Object

model.AbstractSolutionNode

model.EqualSolutionNode

public class EqualSolutionNode
extends AbstractSolutionNode

This class represents a equality node in the tree of proof. A solution node is a node in a tree of proof.

Author:

Alexandre Camus

Field Summary

Fields inherited from class model.AbstractSolutionNode

nodesCreated

Constructor Summary

Constructors

Constructor and Description
EqualSolutionNode(Equal clause, RuleSet rules, SubstitutionSet parentSolution, AbstractSolutionNode parentNode) Constructor of the class.

Method Summary

Methods

Modifier and Type	Method and Description
SubstitutionSet	nextSolution() Creates the next solution for the equality of the node.

Methods inherited from class model.AbstractSolutionNode

currentRuleCount, getClause, getCurrentRule, getDeepestLeaf, getParentNode, getParentSolution, getRuleSet, hasNextRule, nextRule, reset, setDeepestLeaf

Methods inherited from class java.lang.Object

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

Constructor Detail

EqualSolutionNode

public EqualSolutionNode(Equal clause,
                 RuleSet rules,
                 SubstitutionSet parentSolution,
                 AbstractSolutionNode parentNode)

Constructor of the class.

Parameters:

clause - the equal clause to be proved by this subtree.

rules - the rules representing context of the proof.

parentSolution - the solution of the parent node in the tree of proof.

Method Detail

nextSolution

public SubstitutionSet nextSolution()

Creates the next solution for the equality of the node. If no solution exists, it will create a solution. Otherwise it will get a different solution or return null if there no other different solution.

Specified by:

nextSolution in class AbstractSolutionNode

Returns:

a SubstitutionSet object representing the bindings of the next solution or null if there is no next solution.

See Also:

AbstractSolutionNode.nextSolution()