de.uni_freiburg.informatik.ultimate.logic

Class TermEquivalence

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.NonRecursive

de.uni_freiburg.informatik.ultimate.logic.TermEquivalence

public class TermEquivalence
extends NonRecursive

This class checks if two terms are syntactically equivalent modulo renaming of variables. E. g., (let ((x 0)) x) is equivalent to (let ((y 0)) y), but not to 0 or (let ((y 0)) 0).

Author:

Juergen Christ

Nested Class Summary

Nested classes/interfaces inherited from class de.uni_freiburg.informatik.ultimate.logic.NonRecursive

NonRecursive.TermWalker, NonRecursive.Walker

Constructor Summary

Constructors

Constructor and Description
TermEquivalence()

Method Summary

Modifier and Type	Method and Description
boolean	equal(Term lhs, Term rhs) Returns true if the terms are equivalent.

Methods inherited from class de.uni_freiburg.informatik.ultimate.logic.NonRecursive

enqueueWalker, reset, run, run, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

TermEquivalence

public TermEquivalence()

Method Detail

equal

public boolean equal(Term lhs,
                     Term rhs)

Returns true if the terms are equivalent.

Parameters:

lhs - the left hand side term.

rhs - the right hand side term.

Returns:

true if the terms are equivalent modulo variable renaming.