model

Class NotSolutionNode

java.lang.Object

model.AbstractSolutionNode

model.NotSolutionNode

public class NotSolutionNode
extends AbstractSolutionNode

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

Author:

Alexandre Camus

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	solutionFlag
private AbstractSolutionNode	tailSolutionNode

Fields inherited from class model.AbstractSolutionNode

nodesCreated

Constructor Summary

Constructors

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

Method Summary

Methods

Modifier and Type	Method and Description
protected AbstractSolutionNode	getTailSolutionNode() Gets the solution node of the not clause's tail.
SubstitutionSet	nextSolution() Creates the next solution for the negative clause of the node.
protected void	reset(SubstitutionSet newParentSolution, RuleSet newRuleSet) Resets the subtree to the new state of the database and resets all the counters that prevent from infinite evaluation of the node.

Methods inherited from class model.AbstractSolutionNode

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

Methods inherited from class java.lang.Object

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

Field Detail

tailSolutionNode

private AbstractSolutionNode tailSolutionNode

solutionFlag

private boolean solutionFlag

Constructor Detail

NotSolutionNode

public NotSolutionNode(Not clause,
               RuleSet rules,
               SubstitutionSet parentSolution,
               AbstractSolutionNode parentNode)

Constructor of the class.

Parameters:

clause - the negative 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.

parentNode - the parent node in the tree of proof.

Method Detail

reset

protected void reset(SubstitutionSet newParentSolution,
         RuleSet newRuleSet)

Resets the subtree to the new state of the database and resets all the counters that prevent from infinite evaluation of the node.

Overrides:

reset in class AbstractSolutionNode

Parameters:

newParentSolution - the new parent solution of the subtree.

newRuleSet - the new state of the database.

See Also:

AbstractSolutionNode.reset(model.SubstitutionSet, model.RuleSet)

getTailSolutionNode

protected AbstractSolutionNode getTailSolutionNode()

Gets the solution node of the not clause's tail.

This is based on the representation of an not clause. See Not class for more details.

Returns:

a AbstractSolutionNode representing the solution node of the tail.

nextSolution

public SubstitutionSet nextSolution()

Creates the next solution for the negative clause 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()