Class Equality

java.lang.Object
  |
  +--Equality

public class Equality

extends Object

This class implements an equality between two nodes.

Author:

P. URSO

See Also:

Node

Constructor Summary

Equality(Node lhs, Node rhs)
Constructor of the equality node.

Method Summary

Equality	applySubst(Substitution sigma) Applies a substitution to this equality node.
static Map	DEC(RuleTable rules, Node t) Makes the decoupage of a term according to all prefix of top and bottom path.
boolean	equals(Object o) Tests if some other object is "equal to" this one.
void	inductionVariables(Map iv) Extends the map of induction variable with the ones of this equality.
boolean	isNFEqual(RuleTable rules) Tests if this normal form of both sides are equals.
Node	leftSide() Returns the left hand side of the equality.
boolean	lowerThan(Node node) Tests if both sides of this equality are lower than a specified term.
static Node	nf(RuleTable rules, Node term) Returns the normal form of a specified term.
EqualList	patterns(RuleTable rules) Use patterns to split the equality.
Node	rightSide() Returns the right hand side of the equality.
boolean	sidesEqual() Indicates whether this equality is a syntaxic equality.
Equality	split(RuleTable rules) Split the equality.
Equality	toggles() If left (or right) sides is a boolean constant toggles it.
String	toString() Returns a string representation of this equality node.

Methods inherited from class java.lang.Object

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

Constructor Detail

Equality

public Equality(Node lhs,
                Node rhs)

Constructor of the equality node.

Parameters:

lhs - the left hand side of the equality

rhs - the right hand side of the equality

Method Detail

leftSide

public Node leftSide()

Returns the left hand side of the equality.

Returns:

the left hand side of the equality.

rightSide

public Node rightSide()

Returns the right hand side of the equality.

Returns:

the right hand side of the equality.

applySubst

public Equality applySubst(Substitution sigma)

Applies a substitution to this equality node.

Parameters:

sigma - the substitution.

Returns:

a new equality node where the substitution is applied on each side.

sidesEqual

public boolean sidesEqual()

Indicates whether this equality is a syntaxic equality.

Returns:

true if both sides are equal.

inductionVariables

public void inductionVariables(Map iv)

Extends the map of induction variable with the ones of this equality. Variables are mapped with their maximum induction priority. Initial priority of variables is 0.

Parameters:

iv - the map in construction.

toggles

public Equality toggles()

If left (or right) sides is a boolean constant toggles it.

Returns:

a new equality toggled if possible, null otherwise.

lowerThan

public boolean lowerThan(Node node)

Tests if both sides of this equality are lower than a specified term.

Parameters:

node - the term.

nf

public static Node nf(RuleTable rules,
                      Node term)

Returns the normal form of a specified term. Applies simplify rule until no more simplification could be done.

Parameters:

rules - rewrite rules to apply.

term - the node.

Returns:

nf(term).

isNFEqual

public boolean isNFEqual(RuleTable rules)

Tests if this normal form of both sides are equals.

Parameters:

rules - rewrite rules to apply.

Returns:

true if nf(lhs) == nf(rhs)

DEC

public static Map DEC(RuleTable rules,
                      Node t)

Makes the decoupage of a term according to all prefix of top and bottom path. (Monomorphic rewrite system).

Parameters:

rules - rules to normalize complement.

t - term to be split.

Returns:

a map of head part to tail part.

split

public Equality split(RuleTable rules)

Split the equality. Try to find same head or tail part in the both side.

Parameters:

rules - rules to normalize complement.

Returns:

the rest of the both side if splited, null otherwise.

patterns

public EqualList patterns(RuleTable rules)

Use patterns to split the equality. Try to find same left or right patterns in the both sides.

Parameters:

rules - rules to normalize complements.

Returns:

a list of conjectures to prove, null otherwise.

equals

public boolean equals(Object o)

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

Overrides:

equals in class Object

Parameters:

o - the object with which to compare.

Returns:

true if o is an equality and both side are equal.

toString

public String toString()

Returns a string representation of this equality node. The string representation consists of two expression separated by the characters " = ".

Overrides:

toString in class Object

Returns:

a string representation of this node.

See Also:

Node