de.uni_freiburg.informatik.ultimate.logic

Class TermTransformer.BuildQuantifier

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.TermTransformer.BuildQuantifier

All Implemented Interfaces:

NonRecursive.Walker

Enclosing class:

TermTransformer

protected static class TermTransformer.BuildQuantifier
extends java.lang.Object
implements NonRecursive.Walker

Collect the sub term of a quantified formula and build the converted formula. The converted sub formula is expected to be on the converted stack. It stores the converted quantifier on the converted stack and in the cache.

Constructor Summary

Constructors

Constructor and Description
BuildQuantifier(QuantifiedFormula term)

Method Summary

Modifier and Type	Method and Description
java.lang.String	toString()
void	walk(NonRecursive engine) Do one step of the recursive algorithm.

Methods inherited from class java.lang.Object

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

Constructor Detail

BuildQuantifier

public BuildQuantifier(QuantifiedFormula term)

Method Detail

walk

public void walk(NonRecursive engine)

Description copied from interface: NonRecursive.Walker

Do one step of the recursive algorithm. This may enqueue new walkers that do the remaining steps.

Specified by:

walk in interface NonRecursive.Walker

Parameters:

engine - The non recursive engine where new walkers can be enqueued.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object