Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.boollattice | |
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
de.uka.ilkd.key.axiom_abstraction.signanalysis | |
de.uka.ilkd.key.control | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.informationflow.macros | |
de.uka.ilkd.key.informationflow.rule | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.abstraction |
This package contains the meta model abstractions as used by the
semantical services.
|
de.uka.ilkd.key.java.expression |
Elements of the Java syntax tree representing expressions.
|
de.uka.ilkd.key.java.expression.literal |
This package contains representations for the various Java literal types.
|
de.uka.ilkd.key.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.logic.sort |
This package contains different kinds and implementations subtyping interface Sort.
|
de.uka.ilkd.key.macros | |
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.io.intermediate | |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.label | |
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.metaconstruct.arith |
contains classes representing the special meta constructs of
Taclet s performing arithmetic operations. |
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.settings | |
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml.pretranslation | |
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.strategy.feature | |
de.uka.ilkd.key.strategy.feature.instantiator | |
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.strategy.termfeature | |
de.uka.ilkd.key.strategy.termProjection | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.rule | |
de.uka.ilkd.key.symbolic_execution.strategy | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.taclettranslation.assumptions | |
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
Name |
Top.name() |
Name |
False.name() |
Name |
True.name() |
Name |
Bottom.name() |
Modifier and Type | Method and Description |
---|---|
Name |
AbstractPredicateAbstractionDomainElement.name() |
Modifier and Type | Method and Description |
---|---|
Name |
Top.name() |
Name |
Geq.name() |
Name |
Neg.name() |
Name |
Zero.name() |
Name |
Pos.name() |
Name |
Bottom.name() |
Name |
Leq.name() |
Modifier and Type | Method and Description |
---|---|
static java.util.List<Name> |
TermLabelVisibilityManager.getSortedTermLabelNames(Profile profile)
Returns a sorted list of all term label names supported by the given
Profile . |
static java.util.List<Name> |
TermLabelVisibilityManager.getSortedTermLabelNames(Proof proof)
Returns a sorted list of all term label names supported by the given
Proof . |
static java.util.List<Name> |
TermLabelVisibilityManager.getSortedTermLabelNames(TermLabelManager manager)
Returns a sorted list of all term TermLabelManager names supported by the given
TermLabelManager . |
Modifier and Type | Method and Description |
---|---|
boolean |
TermLabelVisibilityManager.contains(Name labelName) |
boolean |
TermLabelVisibilityManager.isHidden(Name labelName)
Gives the information whether the term label with the passed name is currently hidden.
|
void |
TermLabelVisibilityManager.setHidden(Name labelName,
boolean hidden)
Sets the state of the term label with the passed name to hidden or not.
|
Modifier and Type | Method and Description |
---|---|
java.util.List<Name> |
MainWindow.getSortedTermLabelNames() |
Modifier and Type | Method and Description |
---|---|
Name |
UseInformationFlowContractMacro.PropExpansionStrategy.name() |
Modifier and Type | Method and Description |
---|---|
static void |
InfFlowContractAppTaclet.register(Name name) |
static boolean |
InfFlowContractAppTaclet.registered(Name name) |
static boolean |
InfFlowContractAppTaclet.unregister(Name name) |
Constructor and Description |
---|
InfFlowContractAppTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
InfFlowContractAppTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
Modifier and Type | Method and Description |
---|---|
void |
Services.addNameProposal(Name proposal) |
Modifier and Type | Method and Description |
---|---|
Name |
PrimitiveType.getCorrespondingLDTName()
Gets the name of the LDT corresponding to this primitive type.
|
Modifier and Type | Method and Description |
---|---|
static PrimitiveType |
PrimitiveType.getPrimitiveTypeByLDT(Name ldtName) |
Modifier and Type | Method and Description |
---|---|
abstract Name |
Literal.getLDTName() |
Modifier and Type | Method and Description |
---|---|
Name |
EmptySeqLiteral.getLDTName() |
Name |
StringLiteral.getLDTName() |
Name |
DoubleLiteral.getLDTName() |
Name |
NullLiteral.getLDTName() |
Name |
EmptySetLiteral.getLDTName() |
Name |
RealLiteral.getLDTName() |
Name |
FloatLiteral.getLDTName() |
Name |
BooleanLiteral.getLDTName() |
Name |
AbstractIntegerLiteral.getLDTName() |
Name |
FreeLiteral.getLDTName() |
Name |
EmptyMapLiteral.getLDTName() |
Modifier and Type | Field and Description |
---|---|
static Name |
HeapLDT.BASE_HEAP_NAME |
static Name |
IntegerLDT.CHAR_ID_NAME |
static Name |
DoubleLDT.NAME |
static Name |
CharListLDT.NAME |
static Name |
FreeLDT.NAME |
static Name |
MapLDT.NAME |
static Name |
RealLDT.NAME |
static Name |
BooleanLDT.NAME |
static Name |
PermissionLDT.NAME |
static Name |
LocSetLDT.NAME |
static Name |
IntegerLDT.NAME |
static Name |
HeapLDT.NAME |
static Name |
FloatLDT.NAME |
static Name |
SeqLDT.NAME |
static Name |
IntegerLDT.NUMBERS_NAME |
static Name |
HeapLDT.PERMISSION_HEAP_NAME |
static Name |
HeapLDT.SAVED_HEAP_NAME |
static Name |
HeapLDT.SELECT_NAME |
static Name |
SeqLDT.SEQGET_NAME |
static Name |
HeapLDT.STORE_NAME |
static Name |
CharListLDT.STRINGCONTENT_NAME |
static Name |
CharListLDT.STRINGPOOL_NAME |
static Name[] |
HeapLDT.VALID_HEAP_NAMES |
Modifier and Type | Method and Description |
---|---|
Name |
LDT.name() |
Modifier and Type | Method and Description |
---|---|
static java.util.Map<Name,LDT> |
LDT.getNewLDTInstances(Services s) |
Modifier and Type | Method and Description |
---|---|
LocationVariable |
HeapLDT.getHeapForName(Name name) |
Constructor and Description |
---|
LDT(Name name,
Sort targetSort,
TermServices services) |
LDT(Name name,
TermServices services) |
Modifier and Type | Class and Description |
---|---|
class |
ProgramElementName |
static class |
VariableNamer.IndProgramElementName
ProgramElementName carrying an additional index
|
Modifier and Type | Method and Description |
---|---|
<T extends Name> |
NamespaceSet.containsAll(java.lang.Iterable<T> names) |
Modifier and Type | Method and Description |
---|---|
static Name |
VariableNamer.getBasename(Name name) |
Name |
Choice.name() |
Name |
Named.name()
returns the name of this element
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<Name> |
Sequent.getOccuringTermLabels() |
Modifier and Type | Method and Description |
---|---|
int |
Name.compareTo(Name o) |
static Name |
VariableNamer.getBasename(Name name) |
TermLabel |
TermImpl.getLabel(Name termLabelName) |
TermLabel |
Term.getLabel(Name termLabelName)
|
Named |
NamespaceSet.lookup(Name name)
looks up if the given name is found in one of the namespaces
and returns the named object or null if no object with the same name
has been found
|
E |
Namespace.lookup(Name name)
looks if a registered object is declared in this namespace, if
negative it asks its parent
|
protected E |
Namespace.lookupLocally(Name name) |
Named |
NamespaceSet.lookupLogicSymbol(Name name)
looks up for the symbol in the namespaces sort, functions and
programVariables
|
void |
Namespace.remove(Name name)
Remove a name from the namespace.
|
Constructor and Description |
---|
Choice(Name name,
java.lang.String category) |
Modifier and Type | Field and Description |
---|---|
static Name |
ParameterlessTermLabel.ANON_HEAP_LABEL_NAME
|
static Name |
ParameterlessTermLabel.IMPLICIT_SPECIFICATION_LABEL_NAME
|
static Name |
ParameterlessTermLabel.LOOP_SCOPE_INDEX_LABEL_NAME
|
static Name |
OriginTermLabel.NAME
Display name for
OriginTermLabel s. |
static Name |
FormulaTermLabel.NAME
The unique name of this label.
|
static Name |
BlockContractValidityTermLabel.NAME
The unique name of this label.
|
static Name |
SymbolicExecutionTermLabel.NAME
The unique name of this label.
|
static Name |
ParameterlessTermLabel.POST_CONDITION_LABEL_NAME
|
static Name |
ParameterlessTermLabel.SELECT_SKOLEM_LABEL_NAME
|
static Name |
ParameterlessTermLabel.SELF_COMPOSITION_LABEL_NAME
|
static Name |
ParameterlessTermLabel.SHORTCUT_EVALUATION_LABEL_NAME
|
static Name |
ParameterlessTermLabel.UNDEFINED_VALUE_LABEL_NAME
|
Modifier and Type | Method and Description |
---|---|
Name |
TermLabelManager.TermLabelConfiguration.getTermLabelName()
|
Name |
ParameterlessTermLabel.name() |
Name |
OriginTermLabel.name() |
Name |
FormulaTermLabel.name()
returns the name of this element
|
Name |
BlockContractValidityTermLabel.name()
returns the name of this element
|
Name |
SymbolicExecutionTermLabel.name()
returns the name of this element
|
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.computeActiveChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicies,
java.util.Map<Name,ChildTermLabelPolicy> ruleIndependentPolicies)
Computes active
ChildTermLabelPolicy instances which have to be executed during the given rule application. |
ImmutableList<Name> |
TermLabelManager.getSupportedTermLabelNames()
|
static ImmutableList<Name> |
TermLabelManager.getSupportedTermLabelNames(Services services)
|
Modifier and Type | Method and Description |
---|---|
static TermLabel |
TermLabelManager.findInnerMostParentLabel(PosInOccurrence pio,
Name termLabelName)
Searches the inner most
TermLabel wit the given Name in the parent hierarchy of the PosInOccurrence . |
java.util.Map<java.lang.Object,java.lang.Object> |
TermLabelState.getLabelState(Name termLabelName)
|
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.computeActiveChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicies,
java.util.Map<Name,ChildTermLabelPolicy> ruleIndependentPolicies)
Computes active
ChildTermLabelPolicy instances which have to be executed during the given rule application. |
protected java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.computeActiveChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicies,
java.util.Map<Name,ChildTermLabelPolicy> ruleIndependentPolicies)
Computes active
ChildTermLabelPolicy instances which have to be executed during the given rule application. |
protected java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.computeActiveChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicies,
java.util.Map<Name,ChildTermLabelPolicy> ruleIndependentPolicies)
Computes active
ChildTermLabelPolicy instances which have to be executed during the given rule application. |
protected void |
TermLabelManager.performChildAndGrandchildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
ChildTermLabelPolicy instances. |
protected void |
TermLabelManager.performDirectChildPolicies(TermServices services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given direct
ChildTermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels,
TermLabel label)
Performs the given
TermLabelPolicy instances. |
Constructor and Description |
---|
ParameterlessTermLabel(Name name)
Instantiates a new simple term label.
|
TermLabelConfiguration(Name termLabelName,
TermLabelFactory<?> factory)
Constructor.
|
TermLabelConfiguration(Name termLabelName,
TermLabelFactory<?> factory,
ImmutableList<TermLabelPolicy> applicationTermPolicies,
ImmutableList<TermLabelPolicy> modalityTermPolicies,
ImmutableList<ChildTermLabelPolicy> directChildTermLabelPolicies,
ImmutableList<ChildTermLabelPolicy> childAndGrandchildTermLabelPolicies,
ImmutableList<TermLabelUpdate> termLabelUpdates,
ImmutableList<TermLabelRefactoring> termLabelRefactorings,
TermLabelMerger termLabelMerger)
Constructor.
|
Modifier and Type | Field and Description |
---|---|
static Name |
Quantifier.ALL_NAME |
static Name |
Quantifier.EX_NAME |
Modifier and Type | Method and Description |
---|---|
Name |
SortDependingFunction.getKind() |
Modifier and Type | Method and Description |
---|---|
static SortDependingFunction |
SortDependingFunction.createFirstInstance(GenericSort sortDependingOn,
Name kind,
Sort sort,
Sort[] argSorts,
boolean unique) |
static FormulaSV |
SchemaVariableFactory.createFormulaSV(Name name) |
static FormulaSV |
SchemaVariableFactory.createFormulaSV(Name name,
boolean rigidness)
creates a SchemaVariable representing a formula
|
static ModalOperatorSV |
SchemaVariableFactory.createModalOperatorSV(Name name,
Sort sort,
ImmutableSet<Modality> modalities)
creates a SchemaVariable representing an operator
|
static SkolemTermSV |
SchemaVariableFactory.createSkolemTermSV(Name name,
Sort s)
creates a SchemaVariable representing a skolem term
|
static TermLabelSV |
SchemaVariableFactory.createTermLabelSV(Name name)
creates a LabelSchemaVariable
|
static TermSV |
SchemaVariableFactory.createTermSV(Name name,
Sort sort) |
static TermSV |
SchemaVariableFactory.createTermSV(Name name,
Sort sort,
boolean rigidness,
boolean strictSV)
creates a SchemaVariable representing a term but not a formula
|
static UpdateSV |
SchemaVariableFactory.createUpdateSV(Name name) |
static VariableSV |
SchemaVariableFactory.createVariableSV(Name name,
Sort sort)
creates a SchemaVariable representing quantified variables
|
static SortDependingFunction |
SortDependingFunction.getFirstInstance(Name kind,
TermServices services) |
static Transformer |
Transformer.getTransformer(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
TermServices services)
Looks up the function namespace for a term transformer with the given
attributes, assuming it to be uniquely defined by its name.
|
Function |
Function.rename(Name newName) |
abstract Operator |
ProgramVariable.rename(Name name)
Returns an equivalent variable with the new name.
|
UpdateableOperator |
LocationVariable.rename(Name name) |
Operator |
ProgramConstant.rename(Name name) |
Constructor and Description |
---|
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
boolean isRigid) |
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean isRigid) |
AbstractSortedOperator(Name name,
Sort[] argSorts,
Sort sort,
boolean isRigid) |
AbstractSortedOperator(Name name,
Sort[] argSorts,
Sort sort,
java.lang.Boolean[] whereToBind,
boolean isRigid) |
AbstractSortedOperator(Name name,
Sort sort,
boolean isRigid) |
AbstractSV(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
boolean isRigid,
boolean isStrict) |
AbstractSV(Name name,
Sort[] argSorts,
Sort sort,
boolean isRigid,
boolean isStrict) |
AbstractSV(Name name,
Sort sort,
boolean isRigid,
boolean isStrict) |
AbstractTermTransformer(Name name,
int arity) |
AbstractTermTransformer(Name name,
int arity,
Sort sort) |
Function(Name name,
Sort sort) |
Function(Name name,
Sort sort,
boolean isSkolemConstant) |
Function(Name name,
Sort sort,
boolean isSkolemConstant,
Sort... argSorts) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique,
boolean isSkolemConstant) |
Function(Name name,
Sort sort,
Sort... argSorts) |
Function(Name name,
Sort sort,
Sort[] argSorts,
java.lang.Boolean[] whereToBind,
boolean unique) |
Function(Name name,
Sort sort,
Sort[] argSorts,
java.lang.Boolean[] whereToBind,
boolean unique,
boolean isSkolemConstant) |
LogicVariable(Name name,
Sort sort) |
SubstOp(Name name) |
TermLabelSV(Name name) |
Transformer(Name name,
Sort argSort) |
Transformer(Name name,
Sort sort,
ImmutableArray<Sort> argSorts) |
Modifier and Type | Field and Description |
---|---|
static Name |
Sort.CAST_NAME
Name of
Sort.getCastSymbol(TermServices) . |
static Name |
Sort.EXACT_INSTANCE_NAME
|
static Name |
Sort.INSTANCE_NAME
|
static Name |
NullSort.NAME |
Modifier and Type | Method and Description |
---|---|
Name |
NullSort.name() |
Name |
AbstractSort.name() |
Modifier and Type | Method and Description |
---|---|
static java.util.Map<Name,ProgramSVSort> |
ProgramSVSort.name2sort() |
Constructor and Description |
---|
AbstractSort(Name name,
ImmutableSet<Sort> ext,
boolean isAbstract) |
GenericSort(Name name) |
GenericSort(Name name,
ImmutableSet<Sort> ext,
ImmutableSet<Sort> oneOf)
creates a generic sort
|
ProgramSVSort(Name name) |
ProxySort(Name name) |
ProxySort(Name name,
ImmutableSet<Sort> ext) |
SortImpl(Name name) |
SortImpl(Name name,
ImmutableSet<Sort> ext) |
SortImpl(Name name,
ImmutableSet<Sort> ext,
boolean isAbstract) |
SortImpl(Name name,
Sort ext) |
Modifier and Type | Method and Description |
---|---|
Name |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy.name() |
Modifier and Type | Method and Description |
---|---|
protected <T> T |
DefaultBuilder.doLookup(Name n,
Namespace... lookups) |
protected Named |
DefaultBuilder.lookup(Name n) |
Modifier and Type | Method and Description |
---|---|
boolean |
VisibleTermLabels.contains(Name name) |
Modifier and Type | Method and Description |
---|---|
Name |
VariableNameProposer.getNewName(Services services,
Name baseName)
Warning: this method is buggy.
|
Name |
NameRecorder.getProposal() |
Name |
Proof.name()
returns the name of the proof.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Name> |
NameRecorder.getProposals() |
Modifier and Type | Method and Description |
---|---|
void |
NameRecorder.addProposal(Name proposal) |
Name |
VariableNameProposer.getNewName(Services services,
Name baseName)
Warning: this method is buggy.
|
NoPosTacletApp |
TacletIndex.lookup(Name name)
returns a NoPosTacletApp whose Taclet has a name that equals the given
name.
|
Modifier and Type | Method and Description |
---|---|
void |
NameRecorder.setProposals(ImmutableList<Name> proposals) |
Modifier and Type | Method and Description |
---|---|
StrategyFactory |
Profile.getStrategyFactory(Name strategyName)
returns the StrategyFactory for strategy
strategyName |
StrategyFactory |
AbstractProfile.getStrategyFactory(Name n) |
Taclet |
InitConfig.lookupActiveTaclet(Name name) |
boolean |
Profile.supportsStrategyFactory(Name strategyName)
returns true if strategy
strategyName may be
used with this profile. |
boolean |
AbstractProfile.supportsStrategyFactory(Name strategy) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Name> |
BuiltInAppIntermediate.getNewNames() |
ImmutableList<Name> |
TacletAppIntermediate.getNewNames() |
abstract ImmutableList<Name> |
AppIntermediate.getNewNames() |
Constructor and Description |
---|
BuiltInAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
java.lang.String contract,
ImmutableList<Pair<java.lang.Integer,PosInTerm>> builtInIfInsts,
ImmutableList<Name> newNames) |
MergeAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
int id,
java.lang.String joinProc,
int nrPartners,
ImmutableList<Name> newNames,
java.lang.String distinguishingFormula,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> predAbstrLatticeType,
java.lang.String abstractionPredicates,
java.lang.String userChoices)
Constructs a new join rule.
|
MergePartnerAppIntermediate(java.lang.String ruleName,
Pair<java.lang.Integer,PosInTerm> pos,
int mergeNodeId,
ImmutableList<Name> newNames)
Constructs a new close-merge-partner intermediate application.
|
TacletAppIntermediate(java.lang.String tacletName,
Pair<java.lang.Integer,PosInTerm> posInfo,
java.util.LinkedList<java.lang.String> insts,
ImmutableList<java.lang.String> ifSeqFormulaList,
ImmutableList<java.lang.String> ifDirectFormulaList,
ImmutableList<Name> newNames)
Constructs a new intermediate taclet application.
|
Modifier and Type | Field and Description |
---|---|
Name |
RuleKey.name |
static Name |
LoopApplyHeadRule.NAME
The rule name.
|
Modifier and Type | Method and Description |
---|---|
Name |
BlockContractExternalRule.name() |
Name |
Taclet.name()
returns the name of the Taclet
|
Name |
QueryExpand.name() |
Name |
Rule.name()
the name of the rule
|
Name |
OneStepSimplifier.name() |
Name |
WhileInvariantRule.name() |
Name |
BlockContractInternalRule.name() |
Name |
LoopContractExternalRule.name() |
Name |
LoopContractInternalRule.name() |
Name |
UseDependencyContractRule.name() |
Name |
LoopApplyHeadRule.name() |
Name |
UseOperationContractRule.name() |
Name |
RuleSet.name()
gets name of the heuristic
|
Name |
LoopScopeInvariantRule.name() |
Modifier and Type | Method and Description |
---|---|
TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
Name name,
Services services) |
Constructor and Description |
---|
AntecTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
NoFindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that represents a rewrite rule.
|
RuleSet(Name name)
creates a heuristic
|
SuccTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent.
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSmbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Taclet (originally known as Schematic Theory Specific Rules)
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
Name name,
Services services) |
ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>> |
SVInstantiations.lookupEntryForSV(Name name) |
java.lang.Object |
SVInstantiations.lookupValue(Name name) |
SchemaVariable |
SVInstantiations.lookupVar(Name name) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<Name> |
OriginTermLabelRefactoring.getSupportedRuleNames() |
ImmutableList<Name> |
RuleSpecificTask.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
FormulaTermLabelUpdate.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
LoopBodyTermLabelUpdate.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
FormulaTermLabelRefactoring.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
BlockContractValidityTermLabelUpdate.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
SymbolicExecutionTermLabelUpdate.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
RemoveInCheckBranchesTermLabelRefactoring.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
ImmutableList<Name> |
LoopInvariantNormalBehaviorTermLabelUpdate.getSupportedRuleNames()
Returns the supported rule
Name s or null or an empty
list if all rules are supported. |
Modifier and Type | Method and Description |
---|---|
protected TermLabel |
FormulaTermLabelUpdate.getTermLabel(java.util.Set<TermLabel> labels,
Name name)
|
Constructor and Description |
---|
RemoveInCheckBranchesTermLabelRefactoring(Name termLabelNameToRemove)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Name |
MergeRule.name() |
Name |
CloseAfterMerge.name() |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Name> |
CloseAfterMergeRuleBuiltInRuleApp.getNewNames() |
java.util.LinkedHashSet<Name> |
MergeProcedure.ValuesMergeResult.getNewNames() |
protected Triple<SymbolicExecutionState,java.util.LinkedHashSet<Name>,java.util.LinkedHashSet<Term>> |
MergeRule.mergeStates(MergeProcedure mergeRule,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term programCounter,
Term distinguishingFormula,
Services services)
Merges two SE states (U1,C1,p) and (U2,C2,p) according to the method
MergeRule#mergeValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services)
. |
Modifier and Type | Method and Description |
---|---|
CloseAfterMergeRuleBuiltInRuleApp |
CloseAfterMerge.createApp(PosInOccurrence pio,
Node thePartnerNode,
Node correspondingMergeNode,
SymbolicExecutionState mergeNodeState,
SymbolicExecutionState partnerState,
Term pc,
java.util.Set<Name> newNames)
Creates a complete CloseAfterMergeBuiltInRuleApp.
|
void |
CloseAfterMergeRuleBuiltInRuleApp.setNewNames(java.util.Set<Name> newNames) |
Constructor and Description |
---|
CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule,
PosInOccurrence pio,
Node thePartnerNode,
Node correspondingMergeNode,
SymbolicExecutionState mergeNodeState,
SymbolicExecutionState partnerState,
Term pc,
java.util.Set<Name> newNames) |
ValuesMergeResult(ImmutableSet<Term> newConstraints,
Term mergeVal,
java.util.LinkedHashSet<Name> newNames,
java.util.LinkedHashSet<Term> sideConditions) |
Modifier and Type | Method and Description |
---|---|
Name |
ProgramTransformer.name()
returns the name of the meta construct
|
Constructor and Description |
---|
ConstructorCall(Name name,
SchemaVariable newObjectSV,
ProgramElement consRef) |
MethodCall(Name name,
ProgramSV ec,
SchemaVariable result,
ProgramElement body)
creates the methodcall-MetaConstruct
|
ProgramTransformer(Name name,
ProgramElement body)
creates a ProgramTransformer
|
Constructor and Description |
---|
MetaArithBitMaskOp(Name name) |
MetaShift(Name name) |
Modifier and Type | Field and Description |
---|---|
protected Name |
TacletBuilder.name |
protected static Name |
TacletBuilder.NONAME |
Modifier and Type | Method and Description |
---|---|
Name |
TacletBuilder.getName()
returns the name of the Taclet to be built
|
Modifier and Type | Method and Description |
---|---|
Taclet |
TacletGenerator.generateAxiomTaclet(Name tacletName,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
KeYJavaType kjt,
RuleSet ruleSet,
TermServices services)
Returns a no-find taclet to the passed axiom.
|
ImmutableSet<Taclet> |
TacletGenerator.generateContractAxiomTaclets(Name name,
Term originalPre,
Term originalPost,
Term originalMby,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> originalParamVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiabilityGuard,
TermServices services) |
ImmutableSet<Taclet> |
TacletGenerator.generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
ImmutableSet<Taclet> |
TacletGenerator.generatePartialInvTaclet(Name name,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
SchemaVariable eqSV,
Term term,
KeYJavaType kjt,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean isStatic,
boolean eqVersion,
Services services) |
Taclet |
TacletGenerator.generateRelationalRepresentsTaclet(Name tacletName,
Term originalAxiom,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
boolean satisfiabilityGuard,
TermServices services) |
Taclet |
TacletGenerator.generateRewriteTaclet(Name tacletName,
Term originalFind,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
RuleSet ruleSet,
TermServices services) |
void |
TacletBuilder.setName(Name name)
sets the name of the Taclet to be built
|
Modifier and Type | Method and Description |
---|---|
Name |
StrategySettings.getStrategy()
Get the name of the active strategy
|
Modifier and Type | Method and Description |
---|---|
void |
StrategySettings.setStrategy(Name name)
Set the name of the active strategy
|
Modifier and Type | Field and Description |
---|---|
static Name |
RuleAppSMT.SMTRule.name |
Modifier and Type | Method and Description |
---|---|
Name |
RuleAppSMT.SMTRule.name() |
Modifier and Type | Method and Description |
---|---|
Name |
WellDefinednessCheck.name() |
Constructor and Description |
---|
TextualJMLDepends(ImmutableList<java.lang.String> mods,
Name[] heaps,
LabeledParserRuleContext depends) |
Modifier and Type | Field and Description |
---|---|
static Name |
JavaCardDLStrategyFactory.NAME
The unique
Name of this StrategyFactory . |
Modifier and Type | Method and Description |
---|---|
Name |
SimpleFilteredStrategy.name() |
Name |
FIFOStrategy.name() |
Name |
FIFOStrategy.Factory.name() |
Name |
JavaCardDLStrategy.name() |
Name |
JavaCardDLStrategyFactory.name() |
Modifier and Type | Method and Description |
---|---|
protected Feature |
AbstractFeatureStrategy.instantiate(Name sv,
ProjectionToTerm value) |
Constructor and Description |
---|
IntroducedSymbolBy(ProjectionToTerm termWithTopLevelOpToCheck,
Name ruleSetName,
Name schemaVar) |
Modifier and Type | Method and Description |
---|---|
static Feature |
InstantiatedSVFeature.create(Name svName) |
Constructor and Description |
---|
InstantiatedSVFeature(Name svName) |
SVNeedsInstantiation(Name svName) |
Modifier and Type | Method and Description |
---|---|
static Feature |
SVInstantiationCP.create(Name svToInstantiate,
ProjectionToTerm value,
BackTrackingManager manager) |
Constructor and Description |
---|
Metavariable(Name name,
Sort sort)
Deprecated.
|
Constructor and Description |
---|
ContainsLabelNameFeature(Name labelName) |
Modifier and Type | Method and Description |
---|---|
static SVInstantiationProjection |
SVInstantiationProjection.create(Name svName,
boolean demandInst) |
Modifier and Type | Method and Description |
---|---|
Name |
TruthValueTracingUtil.BranchResult.getTermLabelName()
|
Modifier and Type | Method and Description |
---|---|
protected static void |
TruthValueTracingUtil.checkForNewMinorIds(Node childNode,
Term term,
Name termLabelName,
PosInOccurrence parentPio,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Checks if new minor IDs are available.
|
protected static void |
TruthValueTracingUtil.checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF,
Term term,
Name termLabelName,
PosInOccurrence parentPio,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Checks if new minor IDs are available in case of
OneStepSimplifier usage. |
TruthValueTracingUtil.TruthValue |
TruthValueTracingUtil.MultiEvaluationResult.evaluate(Name termLabelName,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Computes the final truth value.
|
static TruthValueTracingUtil.TruthValueTracingResult |
TruthValueTracingUtil.evaluate(Node node,
Name termLabelName,
boolean useUnicode,
boolean usePrettyPrinting)
|
protected static void |
TruthValueTracingUtil.evaluateNode(Node evaluationNode,
boolean useUnicode,
boolean usePrettyPrinting,
Node child,
int childIndexOnParent,
Name termLabelName,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> nodeResult,
TruthValueTracingUtil.TruthValueTracingResult result,
Services services)
|
protected static java.util.List<de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil.LabelOccurrence> |
TruthValueTracingUtil.findInvolvedLabels(Sequent sequent,
TacletApp tacletApp,
Name termLabelName)
Computes the occurrences of all involved
FormulaTermLabel s. |
protected static void |
TruthValueTracingUtil.listLabelReplacements(SequentFormula sf,
Name labelName,
java.lang.String labelId,
java.util.List<Term> resultToFill)
Lists all label replacements in the given
SequentFormula . |
protected static void |
TruthValueTracingUtil.updatePredicateResultBasedOnNewMinorIds(Node childNode,
Name termLabelName,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Updates the
PredicateResult s based on minor ID changes if available. |
protected static void |
TruthValueTracingUtil.updatePredicateResultBasedOnNewMinorIdsOSS(PosInOccurrence childPio,
PosInOccurrence parentPio,
Name termLabelName,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Updates the
PredicateResult s based on minor ID changes if
available in case of OneStepSimplifier usage. |
Constructor and Description |
---|
BranchResult(Node leafNode,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results,
Term condition,
java.lang.String conditionString,
Name termLabelName)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
Name |
ModalitySideProofRule.name()
the name of the rule
|
Name |
QuerySideProofRule.name()
the name of the rule
|
Modifier and Type | Field and Description |
---|---|
static Name |
SymbolicExecutionStrategy.name
|
static Name |
SimplifyTermStrategy.name
|
Modifier and Type | Method and Description |
---|---|
Name |
SymbolicExecutionStrategy.name()
returns the name of this element
|
Name |
SymbolicExecutionStrategy.Factory.name()
returns the name of this element
|
Name |
SimplifyTermStrategy.name()
returns the name of this element
|
Name |
SimplifyTermStrategy.Factory.name()
returns the name of this element
|
Modifier and Type | Field and Description |
---|---|
static Name |
SymbolicExecutionUtil.LOOP_BODY_LABEL_NAME
|
static Name |
SymbolicExecutionUtil.LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL_NAME
|
static Name |
SymbolicExecutionUtil.RESULT_LABEL_NAME
Name of
SymbolicExecutionUtil.RESULT_LABEL . |
Modifier and Type | Method and Description |
---|---|
LogicVariable |
AssumptionGenerator.getLogicVariable(Name name,
Sort sort)
Returns a new logic variable with the given name and sort.
|
Modifier and Type | Method and Description |
---|---|
java.util.Map<Name,Sort> |
UserDefinedSymbols.getExtraSorts() |
Modifier and Type | Method and Description |
---|---|
static Name |
MiscTools.toValidTacletName(java.lang.String s) |
static Name |
MiscTools.toValidVariableName(java.lang.String s) |
Modifier and Type | Method and Description |
---|---|
static Pair<Sort,Name> |
MergeRuleUtils.parsePlaceholder(java.lang.String input,
boolean registerInNamespaces,
Services services)
Parses a declaration of the type "<SORT> <NAME>", where
<SORT> must be a sort known to the proof and <NAME> must be a
fresh name.
|
static Pair<Sort,Name> |
MergeRuleUtils.parsePlaceholder(java.lang.String input,
Services services)
Parses a declaration of the type "<SORT> <NAME>", where
<SORT> must be a sort known to the proof and <NAME> must be a
fresh name.
|
Modifier and Type | Method and Description |
---|---|
static void |
MergeRuleUtils.closeMergePartnerGoal(Node mergeNodeParent,
Goal mergePartner,
PosInOccurrence pio,
SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Term pc,
java.util.Set<Name> newNames)
Closes the given partner goal, using the
CloseAfterMerge rule. |
static AbstractionPredicate |
MergeRuleUtils.parsePredicate(java.lang.String input,
java.util.ArrayList<Pair<Sort,Name>> registeredPlaceholders,
NamespaceSet localNamespaces,
Services services)
Parses an abstraction predicate.
|
Copyright © 2003-2019 The KeY-Project.