| java.lang.Object de.uka.ilkd.key.rule.soundness.AbstractSkolemBuilder
All known Subclasses: de.uka.ilkd.key.rule.soundness.ProgramVariableSkolemBuilder, de.uka.ilkd.key.rule.soundness.LabelSkolemBuilder, de.uka.ilkd.key.rule.soundness.ContextSkolemBuilder, de.uka.ilkd.key.rule.soundness.AbstractPVPrefixSkolemBuilder, de.uka.ilkd.key.rule.soundness.TypeInfoBuilder, de.uka.ilkd.key.rule.soundness.LogicVariableSkolemBuilder, de.uka.ilkd.key.rule.soundness.SVPartitioningBuilder,
AbstractSkolemBuilder | abstract public class AbstractSkolemBuilder implements SkolemBuilder(Code) | | Abstract superclass of all skolem builders
|
addInstantiation | protected void addInstantiation(SchemaVariable p_sv, Term p_term)(Code) | | Add an instantiation to the SVInstantiations object
|
addInstantiation | protected void addInstantiation(SchemaVariable p_sv, ProgramElement p_pe, int p_instantiationType)(Code) | | Add an instantiation to the SVInstantiations object
|
createTypeCandidates | protected IteratorOfKeYJavaType createTypeCandidates()(Code) | | Types that should be considered for untyped schema
variables. Currently only primitive types and the object type
are returned
|
createUniqueName | static Name createUniqueName(String baseName)(Code) | | HACK: Create a new and unique identifier
|
createUniqueName | static Name createUniqueName(Name baseName)(Code) | | HACK: Create a new and unique identifier
|
getOriginalFormula | protected Term getOriginalFormula()(Code) | | The formula for which skolem symbols are to be created
|
getOriginalSkolemSet | protected SkolemSet getOriginalSkolemSet()(Code) | | The object that is to be enriched by further skolem symbols
|
|
|