de.uka.ilkd.key.logic

Class Sequent.NILSequent

java.lang.Object

de.uka.ilkd.key.logic.Sequent

de.uka.ilkd.key.logic.Sequent.NILSequent

All Implemented Interfaces:

java.lang.Iterable<SequentFormula>

Enclosing class:

Sequent

static class Sequent.NILSequent
extends Sequent

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.logic.Sequent

Sequent.NILSequent, Sequent.SequentIterator

Field Summary

Fields inherited from class de.uka.ilkd.key.logic.Sequent

EMPTY_SEQUENT

Constructor Summary

Constructors

Constructor and Description
NILSequent()

Method Summary

Modifier and Type	Method and Description
boolean	isEmpty() determines if the sequent is empty.
java.util.Iterator<SequentFormula>	iterator() returns iterator about all ConstrainedFormulae of the sequent
boolean	varIsBound(QuantifiableVariable v) returns true iff the given variable is bound in a formula of a SequentFormula in this sequent.

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

addFormula, addFormula, addFormula, addFormula, antecedent, changeFormula, changeFormula, contains, createAnteSequent, createSequent, createSuccSequent, equals, formulaNumberInSequent, getFormulabyNr, getOccuringTermLabels, hashCode, numberInAntec, removeFormula, size, succedent, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Constructor Detail

NILSequent

NILSequent()

Method Detail

isEmpty

public boolean isEmpty()

Description copied from class: Sequent

determines if the sequent is empty.

Overrides:

isEmpty in class Sequent

Returns:

true iff the sequent consists of two instances of Semisequent.EMPTY_SEMISEQUENT

iterator

public java.util.Iterator<SequentFormula> iterator()

Description copied from class: Sequent

returns iterator about all ConstrainedFormulae of the sequent

Specified by:

iterator in interface java.lang.Iterable<SequentFormula>

Overrides:

iterator in class Sequent

Returns:

iterator about all ConstrainedFormulae of the sequent

varIsBound

public boolean varIsBound(QuantifiableVariable v)

Description copied from class: Sequent

returns true iff the given variable is bound in a formula of a SequentFormula in this sequent.

Overrides:

varIsBound in class Sequent

Parameters:

v - the bound variable to search for