de.uka.ilkd.key.symbolic_execution.util

Class SymbolicExecutionSideProofUtil.ContainsIrrelevantThingsVisitor

java.lang.Object

de.uka.ilkd.key.logic.DefaultVisitor

de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil.ContainsIrrelevantThingsVisitor

All Implemented Interfaces:

Visitor

Enclosing class:

SymbolicExecutionSideProofUtil

protected static class SymbolicExecutionSideProofUtil.ContainsIrrelevantThingsVisitor
extends DefaultVisitor

Utility class used by QuerySideProofRule#containsIrrelevantThings(Services, SequentFormula, Set).

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
(package private) boolean	containsIrrelevantThings The result.
private java.util.Set<Operator>	relevantThings The relevant things.
private Services	services The Services to use.

Constructor Summary

Constructors

Constructor and Description
ContainsIrrelevantThingsVisitor(Services services, java.util.Set<Operator> relevantThings) Constructor.

Method Summary

Modifier and Type	Method and Description
boolean	isContainsIrrelevantThings() Returns the result.
void	visit(Term visited) the entry method for the visitor pattern

Methods inherited from class de.uka.ilkd.key.logic.DefaultVisitor

subtreeEntered, subtreeLeft, visitSubtree

Methods inherited from class java.lang.Object

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

Field Detail

services

private Services services

The Services to use.

relevantThings

private java.util.Set<Operator> relevantThings

The relevant things.

containsIrrelevantThings

boolean containsIrrelevantThings

The result.

Constructor Detail

ContainsIrrelevantThingsVisitor

public ContainsIrrelevantThingsVisitor(Services services,
                                       java.util.Set<Operator> relevantThings)

Constructor.

Parameters:

services - The Services to use.

relevantThings - The relevant things.

Method Detail

visit

public void visit(Term visited)

the entry method for the visitor pattern

Parameters:

visited - the Term to be visited

isContainsIrrelevantThings

public boolean isContainsIrrelevantThings()

Returns the result.

Returns:

The SequentFormula contains irrelevant things, false the SequentFormula contains no irrelevant things.