de.uka.ilkd.key.rule

Class IfFormulaInstSeq

java.lang.Object

de.uka.ilkd.key.rule.IfFormulaInstSeq

All Implemented Interfaces:

IfFormulaInstantiation

public class IfFormulaInstSeq
extends java.lang.Object
implements IfFormulaInstantiation

Instantiation of an if-formula that is a formula of an existing sequent.

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	antec
private SequentFormula	cf
private PosInOccurrence	pioCache
private Sequent	seq Sequent and formula

Constructor Summary

Constructors

Constructor and Description
IfFormulaInstSeq(Sequent p_seq, boolean antec, SequentFormula p_cf)
IfFormulaInstSeq(Sequent seq, int formulaNr)

Method Summary

Modifier and Type	Method and Description
static ImmutableList<IfFormulaInstantiation>	createList(Sequent p_s, boolean antec, Services services)
private static ImmutableList<IfFormulaInstantiation>	createListHelp(Sequent p_s, boolean antec) Create a list with all formulas of a given semisequent
boolean	equals(java.lang.Object p_obj)
SequentFormula	getConstrainedFormula()
int	hashCode()
boolean	inAntec()
PosInOccurrence	toPosInOccurrence()
java.lang.String	toString()
java.lang.String	toString(Services services)

Methods inherited from class java.lang.Object

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

Field Detail

seq

private final Sequent seq

Sequent and formula

antec

private final boolean antec

cf

private final SequentFormula cf

pioCache

private volatile PosInOccurrence pioCache

Constructor Detail

IfFormulaInstSeq

public IfFormulaInstSeq(Sequent p_seq,
                        boolean antec,
                        SequentFormula p_cf)

IfFormulaInstSeq

public IfFormulaInstSeq(Sequent seq,
                        int formulaNr)

Method Detail

getConstrainedFormula

public SequentFormula getConstrainedFormula()

Specified by:

getConstrainedFormula in interface IfFormulaInstantiation

Returns:

the cf this is pointing to

createListHelp

private static ImmutableList<IfFormulaInstantiation> createListHelp(Sequent p_s,
                                                                    boolean antec)

Create a list with all formulas of a given semisequent

createList

public static ImmutableList<IfFormulaInstantiation> createList(Sequent p_s,
                                                               boolean antec,
                                                               Services services)

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

toString

public java.lang.String toString(Services services)

Specified by:

toString in interface IfFormulaInstantiation

equals

public boolean equals(java.lang.Object p_obj)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

inAntec

public boolean inAntec()

toPosInOccurrence

public PosInOccurrence toPosInOccurrence()