de.uni_freiburg.informatik.ultimate.logic

Class CheckClosedTerm

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.NonRecursive

de.uni_freiburg.informatik.ultimate.logic.CheckClosedTerm

public class CheckClosedTerm
extends NonRecursive

Class to check if a term is closed. It is closed if it does not contain a free variable. Use it as follows:

new CheckClosedTerm().isClosed()

You can check multiple terms with one instance and it will cache results between checks.

Author:

Jochen Hoenicke

Nested Class Summary

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

NonRecursive.Walker

Constructor Summary

Constructors

Constructor and Description
CheckClosedTerm() The default constructor.

Method Summary

Modifier and Type	Method and Description
boolean	isClosed(Term t) Check if term t is closed.

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

CheckClosedTerm

public CheckClosedTerm()

The default constructor.

Method Detail

isClosed

public boolean isClosed(Term t)

Check if term t is closed. I.e., it contains no free term variable.

Parameters:

t - the term that is checked.

Returns:

true if the term is closed; false otherwise.