Class VariableNode

java.lang.Object
  |
  +--Node
        |
        +--VariableNode

public class VariableNode

extends Node

This class implements a variable node.

Author:

P. URSO

See Also:

Variable

Fields inherited from class Node

MAX_PRIORITY, MIN_PRIORITY

Constructor Summary

VariableNode(Variable id)
Constructor of the variable node.

Method Summary

Node	applySubst(Substitution sigma) Applies a substitution to this node.
boolean	equals(Object o) Tests if some other object is "equal to" this node.
int	getNumber(Type t) Returns number of sub term with a specified type of this node.
Type	getType() Returns the type of the node.
void	getVariables(Set vars) Extends the set of variables with this one.
boolean	greaterThan(Node node) Tests if this variable node is greater (in order) than a function call node.
int	hashCode() Returns a hash code for this variable node.
Variable	identifier() Returns the identifier of the variable.
void	inductionVariables(Map iv, int priority) Extends the map of induction variable with the one of this term.
void	makeFilter(Node node, Substitution sigma) Constructs a filter between this variable node and an other node.
Node	simplify(RuleTable rules, Conjecture clause) Applies a rewrite step on this node in a specified conjecture.
String	toString() Returns a string representation of this variable node.

Methods inherited from class Node

bot, botPath, find, getAsPart, getSubterm, isConstant, isConstructorRooted, isGround, nbt, ntp, numAsPart, remplaceSubterm, top, topPath, toStringInfix, withNewVariables

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

VariableNode

public VariableNode(Variable id)

Constructor of the variable node.

Parameters:

id - identifier of the variable.

Method Detail

getType

public Type getType()

Returns the type of the node.

Overrides:

getType in class Node

Returns:

the type of the identifier of the variable.

identifier

public Variable identifier()

Returns the identifier of the variable.

Returns:

the identifier of the variable.

applySubst

public Node applySubst(Substitution sigma)

Applies a substitution to this node.

Overrides:

applySubst in class Node

Parameters:

sigma - the substitution map.

Returns:

the image in substitution if it is a mapped node, the node itself otherwise.

makeFilter

public void makeFilter(Node node,
                       Substitution sigma)
                throws SubstitutionStop

Constructs a filter between this variable node and an other node. If making such a filter is not possible, throws a SubstitutionStop.

Overrides:

makeFilter in class Node

Parameters:

node - the other node.

sigma - the substitution map in construction.

Throws:

SubstitutionStop -

greaterThan

public boolean greaterThan(Node node)

Tests if this variable node is greater (in order) than a function call node.

Overrides:

greaterThan in class Node

Parameters:

node - the other node.

Returns:

true if this variable is a sub-node of the function call node.

simplify

public Node simplify(RuleTable rules,
                     Conjecture clause)

Applies a rewrite step on this node in a specified conjecture. Tries to find in the rewrite rules the defintion of functions apparing in the node. Make one step to normal form.

Parameters:

rules - the table of rewrite rules.

clause - the conjecture where occurs simplifying.

Returns:

null, a variable node could not be simplified.

See Also:

RuleTable

equals

public boolean equals(Object o)

Tests if some other object is "equal to" this node.

Overrides:

equals in class Object

Parameters:

o - the object with which to compare.

Returns:

true if is a variable node and theirs identifier are equal.

inductionVariables

public void inductionVariables(Map iv,
                               int priority)

Extends the map of induction variable with the one of this term. Variables are mapped with their maximum induction priority.

Overrides:

inductionVariables in class Node

Parameters:

iv - the map in construction.

priority - the current priority.

getVariables

public void getVariables(Set vars)

Extends the set of variables with this one.

Overrides:

getVariables in class Node

Parameters:

vars - the set of variables in construction.

getNumber

public int getNumber(Type t)

Returns number of sub term with a specified type of this node.

Overrides:

getNumber in class Node

Parameters:

t - the type.

hashCode

public int hashCode()

Returns a hash code for this variable node. In fact the hashcode of its identifier.

Overrides:

hashCode in class Object

Returns:

a hash code value for this object.

toString

public String toString()

Returns a string representation of this variable node. The string representation consists of the name of identifier.

Overrides:

toString in class Object

Returns:

a string representation of this node.