Package | Description |
---|---|
de.uka.ilkd.key.core | |
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.nparser.builder | |
de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
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 |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.label | |
de.uka.ilkd.key.rule.match.vm.instructions | |
de.uka.ilkd.key.rule.tacletbuilder | |
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.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.taclettranslation.assumptions | |
de.uka.ilkd.key.taclettranslation.lemma |
Modifier and Type | Method and Description |
---|---|
Namespace<QuantifiableVariable> |
KeYMediator.var_ns()
returns the variable namespace
|
Modifier and Type | Field and Description |
---|---|
protected QuantifiableVariable |
ClashFreeSubst.v |
Modifier and Type | Field and Description |
---|---|
protected ImmutableSet<QuantifiableVariable> |
ClashFreeSubst.svars |
Modifier and Type | Method and Description |
---|---|
protected QuantifiableVariable |
ClashFreeSubst.getVariable() |
protected QuantifiableVariable |
ClashFreeSubst.newVarFor(QuantifiableVariable var,
ImmutableSet<QuantifiableVariable> usedVars)
returns a new variable that has a name derived from that of
var , that is different from any of the names of
variables in usedVars . |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<QuantifiableVariable> |
TermImpl.boundVars() |
ImmutableArray<QuantifiableVariable> |
Term.boundVars()
The logical variables bound by the top level operator.
|
ImmutableSet<QuantifiableVariable> |
TermImpl.freeVars() |
ImmutableSet<QuantifiableVariable> |
Term.freeVars()
The set of free quantifiable variables occurring in this term.
|
ImmutableSet<QuantifiableVariable> |
BoundVarsVisitor.getBoundVariables()
returns all the bound variables that have been stored
|
protected static ImmutableArray<QuantifiableVariable> |
ClashFreeSubst.getSingleArray(ImmutableArray<QuantifiableVariable>[] bv) |
ImmutableArray<QuantifiableVariable> |
BoundVariableTools.unifyBoundVariables(ImmutableArray<QuantifiableVariable>[] boundVarsPerSub,
Term[] subs,
int subtermsBegin,
int subtermsEnd,
TermServices services)
Ensure that for the subterms with indexes [
subtermsBegin ,
subtermsEnd ) the same variables are bound. |
Namespace<QuantifiableVariable> |
NamespaceSet.variables() |
ImmutableSet<QuantifiableVariable> |
ClashFreeSubst.VariableCollectVisitor.vars()
the set of all occurring variables.
|
ImmutableArray<QuantifiableVariable> |
TermImpl.varsBoundHere(int n) |
ImmutableArray<QuantifiableVariable> |
Term.varsBoundHere(int n)
The logical variables bound by the top level operator for the nth
subterm.
|
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.all(QuantifiableVariable qv,
Term t) |
RenameTable |
RenameTable.assign(QuantifiableVariable n1,
QuantifiableVariable n2)
assigns both QuantifiableVariable objects the same abstract name
|
Term |
TermBuilder.bprod(QuantifiableVariable qv,
Term a,
Term b,
Term t,
Services services)
Constructs a bounded product comprehension expression.
|
Term |
TermBuilder.bsum(QuantifiableVariable qv,
Term a,
Term b,
Term t) |
boolean |
RenameTable.contains(QuantifiableVariable n)
returns true iff the given variable is mapped to an abstract name.
|
boolean |
RenameTable.containsLocally(QuantifiableVariable n)
does nearly the same as
RenameTable.contains(QuantifiableVariable) but performs
the test only on the local table |
Term |
TermBuilder.ex(QuantifiableVariable qv,
Term t) |
Term |
TermBuilder.ifEx(QuantifiableVariable qv,
Term cond,
Term _then,
Term _else)
Construct a term with the \ifEx operator.
|
Term |
TermBuilder.infiniteUnion(QuantifiableVariable[] qvs,
Term s) |
Term |
TermBuilder.infiniteUnion(QuantifiableVariable[] qvs,
Term guard,
Term s) |
protected QuantifiableVariable |
ClashFreeSubst.newVarFor(QuantifiableVariable var,
ImmutableSet<QuantifiableVariable> usedVars)
returns a new variable that has a name derived from that of
var , that is different from any of the names of
variables in usedVars . |
boolean |
BoundVariableTools.resolveCollisions(ImmutableArray<QuantifiableVariable> oldVars,
QuantifiableVariable[] newVars,
ImmutableSet<QuantifiableVariable> criticalVars)
Replace all variables of
oldVars that also turn up in
criticalPairs with new variables (currently just with the
same name). |
boolean |
RenameTable.sameAbstractName(QuantifiableVariable n1,
QuantifiableVariable n2)
tests if both QuantifiableVariables are assigned to the same abstract
name (locally or by the parent)
|
Term |
TermBuilder.seqDef(QuantifiableVariable qv,
Term a,
Term b,
Term t) |
Term |
TermBuilder.setComprehension(QuantifiableVariable[] qvs,
Term o,
Term f) |
Term |
TermBuilder.setComprehension(QuantifiableVariable[] qvs,
Term guard,
Term o,
Term f) |
Term |
TermBuilder.subst(QuantifiableVariable substVar,
Term substTerm,
Term origTerm) |
Term |
TermBuilder.subst(SubstOp op,
QuantifiableVariable substVar,
Term substTerm,
Term origTerm)
Creates a substitution term
|
boolean |
Sequent.varIsBound(QuantifiableVariable v)
returns true iff the given variable is bound in a formula of a SequentFormula
in this sequent.
|
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.all(java.lang.Iterable<QuantifiableVariable> qvs,
Term t) |
boolean |
BoundVariableTools.consistentVariableArrays(ImmutableArray<QuantifiableVariable> ar0,
ImmutableArray<QuantifiableVariable> ar1) |
boolean |
BoundVariableTools.consistentVariableArrays(ImmutableArray<QuantifiableVariable> ar0,
ImmutableArray<QuantifiableVariable> ar1) |
Term |
TermFactory.createTerm(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock) |
Term |
TermFactory.createTerm(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
ImmutableArray<TermLabel> labels)
Master method for term creation.
|
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
TermLabel label) |
boolean |
BoundVariableTools.equalsModRenaming(ImmutableArray<QuantifiableVariable> vars0,
Term term0,
ImmutableArray<QuantifiableVariable> vars1,
Term term1,
TermServices services) |
boolean |
BoundVariableTools.equalsModRenaming(ImmutableArray<QuantifiableVariable> vars0,
Term term0,
ImmutableArray<QuantifiableVariable> vars1,
Term term1,
TermServices services) |
Term |
TermBuilder.ex(java.lang.Iterable<QuantifiableVariable> qvs,
Term t) |
Term |
TermBuilder.func(Function f,
Term[] s,
ImmutableArray<QuantifiableVariable> boundVars) |
Term |
TermBuilder.ifEx(ImmutableList<QuantifiableVariable> qvs,
Term cond,
Term _then,
Term _else)
Construct a term with the \ifEx operator.
|
Term |
TermBuilder.max(ImmutableList<? extends QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
minimum operator
|
Term |
TermBuilder.min(ImmutableList<? extends QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
minimum operator
|
protected QuantifiableVariable |
ClashFreeSubst.newVarFor(QuantifiableVariable var,
ImmutableSet<QuantifiableVariable> usedVars)
returns a new variable that has a name derived from that of
var , that is different from any of the names of
variables in usedVars . |
Term |
TermBuilder.prod(ImmutableList<QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
General (unbounded) product
|
Term[] |
BoundVariableTools.renameVariables(Term[] originalTerms,
ImmutableArray<QuantifiableVariable> oldBoundVars,
ImmutableArray<QuantifiableVariable> newBoundVars,
TermServices services) |
Term[] |
BoundVariableTools.renameVariables(Term[] originalTerms,
ImmutableArray<QuantifiableVariable> oldBoundVars,
ImmutableArray<QuantifiableVariable> newBoundVars,
TermServices services) |
Term |
BoundVariableTools.renameVariables(Term originalTerm,
ImmutableArray<QuantifiableVariable> oldBoundVars,
ImmutableArray<QuantifiableVariable> newBoundVars,
TermServices services)
Compare the arrays
oldBoundVars and
newBoundVars component-wise, and in case of differences
substitute variables from the former array with the ones of the latter
array (in originalTerm ) |
Term |
BoundVariableTools.renameVariables(Term originalTerm,
ImmutableArray<QuantifiableVariable> oldBoundVars,
ImmutableArray<QuantifiableVariable> newBoundVars,
TermServices services)
Compare the arrays
oldBoundVars and
newBoundVars component-wise, and in case of differences
substitute variables from the former array with the ones of the latter
array (in originalTerm ) |
boolean |
BoundVariableTools.resolveCollisions(ImmutableArray<QuantifiableVariable> oldVars,
QuantifiableVariable[] newVars,
ImmutableSet<QuantifiableVariable> criticalVars)
Replace all variables of
oldVars that also turn up in
criticalPairs with new variables (currently just with the
same name). |
boolean |
BoundVariableTools.resolveCollisions(ImmutableArray<QuantifiableVariable> oldVars,
QuantifiableVariable[] newVars,
ImmutableSet<QuantifiableVariable> criticalVars)
Replace all variables of
oldVars that also turn up in
criticalPairs with new variables (currently just with the
same name). |
boolean |
BoundVariableTools.resolveCollisions(Term originalTerm,
ImmutableSet<QuantifiableVariable> criticalVars,
ImmutableArray<QuantifiableVariable>[] newBoundVars,
Term[] newSubs,
TermServices services)
Ensure that none of the variables
criticalVars is bound by
the top-level operator of t (by bound renaming). |
void |
NamespaceSet.setVariables(Namespace<QuantifiableVariable> varNS) |
protected boolean |
ClashFreeSubst.subTermChanges(ImmutableArray<QuantifiableVariable> boundVars,
Term subTerm)
returns true if
subTerm bound by
boundVars would change under application of this
substitution. |
Term |
TermBuilder.sum(ImmutableList<QuantifiableVariable> qvs,
Term range,
Term t)
General (unbounded) sum
|
Constructor and Description |
---|
ClashFreeSubst(QuantifiableVariable v,
Term s,
TermBuilder tb) |
WaryClashFreeSubst(QuantifiableVariable v,
Term s,
TermBuilder tb) |
Constructor and Description |
---|
NamespaceSet(Namespace<QuantifiableVariable> varNS,
Namespace<Function> funcNS,
Namespace<Sort> sortNS,
Namespace<RuleSet> ruleSetNS,
Namespace<Choice> choiceNS,
Namespace<IProgramVariable> programVarNS) |
RenameTable(RenameTable parent,
ImmutableMap<QuantifiableVariable,java.lang.Integer> localTable,
int newMax) |
TermImpl(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock)
Constructs a term for the given operator, with the given sub terms,
bounded variables and (if applicable) the code block on this term.
|
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. |
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
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. |
protected void |
TermLabelManager.performUpdater(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableList<TermLabelUpdate> updater,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
TermLabelUpdate instances. |
Modifier and Type | Class and Description |
---|---|
class |
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
class |
VariableSV
Schema variable that is instantiated with logical variables.
|
Modifier and Type | Method and Description |
---|---|
QuantifiableVariable |
ExpressionBuilder.visitOne_bound_variable(KeYParser.One_bound_variableContext ctx) |
Modifier and Type | Method and Description |
---|---|
protected Namespace<QuantifiableVariable> |
DefaultBuilder.variables() |
java.util.List<QuantifiableVariable> |
ExpressionBuilder.visitBound_variables(KeYParser.Bound_variablesContext ctx) |
Modifier and Type | Method and Description |
---|---|
protected void |
DefaultBuilder.unbindVars(Namespace<QuantifiableVariable> orig) |
Modifier and Type | Method and Description |
---|---|
Term |
DefaultTermParser.parse(java.io.Reader in,
Sort sort,
Services services,
Namespace<QuantifiableVariable> var_ns,
Namespace<Function> func_ns,
Namespace<Sort> sort_ns,
Namespace<IProgramVariable> progVar_ns,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a term with the
specified namespaces.
|
Modifier and Type | Method and Description |
---|---|
void |
LogicPrinter.printSubstTerm(java.lang.String l,
QuantifiableVariable v,
Term t,
int ass2,
java.lang.String r,
Term phi,
int ass3)
Print a substitution term.
|
Modifier and Type | Method and Description |
---|---|
void |
LogicPrinter.printQuantifierTerm(java.lang.String name,
ImmutableArray<QuantifiableVariable> vars,
Term phi,
int ass)
Print a quantified term.
|
Modifier and Type | Method and Description |
---|---|
ImmutableArray<QuantifiableVariable> |
OpReplacer.replace(ImmutableArray<QuantifiableVariable> vars)
Replaces in an ImmutableArray
|
Modifier and Type | Method and Description |
---|---|
ImmutableArray<QuantifiableVariable> |
OpReplacer.replace(ImmutableArray<QuantifiableVariable> vars)
Replaces in an ImmutableArray
|
Constructor and Description |
---|
PrefixTermTacletAppIndexCacheImpl(ImmutableList<QuantifiableVariable> prefix,
java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache) |
Modifier and Type | Method and Description |
---|---|
Namespace<QuantifiableVariable> |
InitConfig.varNS()
returns the variable namespace of this initial configuration
|
Modifier and Type | Method and Description |
---|---|
static Term |
IntermediateProofReplayer.parseTerm(java.lang.String value,
Proof proof,
Namespace<QuantifiableVariable> varNS,
Namespace<IProgramVariable> progVarNS,
Namespace<Function> functNS)
Parses a given term in String representation.
|
Modifier and Type | Method and Description |
---|---|
protected static ImmutableSet<QuantifiableVariable> |
TacletApp.boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
protected static ImmutableSet<QuantifiableVariable> |
TacletApp.boundAtOccurrenceSet(TacletPrefix prefix,
SVInstantiations instantiations,
PosInOccurrence pos)
collects all bound variables above the occurrence of the schemavariable
whose prefix is given
|
protected static ImmutableSet<QuantifiableVariable> |
TacletApp.collectBoundVarsAbove(PosInOccurrence pos)
collects all bound vars that are bound above the subterm described by the
given term position information
|
protected ImmutableSet<QuantifiableVariable> |
NoPosTacletApp.contextVars(SchemaVariable sv) |
protected ImmutableSet<QuantifiableVariable> |
PosTacletApp.contextVars(SchemaVariable sv) |
protected abstract ImmutableSet<QuantifiableVariable> |
TacletApp.contextVars(SchemaVariable sv) |
Namespace<QuantifiableVariable> |
TacletApp.extendVarNamespaceForSV(Namespace<QuantifiableVariable> var_ns,
SchemaVariable sv)
creates a new variable namespace by adding names of the instantiations of
the schema variables in the context of the given schema variable and (if
the TacletApp's prefix has the context flag set) by adding names of the
logic variables of the context.
|
ImmutableSet<QuantifiableVariable> |
Taclet.getBoundVariables()
computes and returns all variables that occur bound in the taclet
including the taclets defined in addrules sections.
|
protected abstract ImmutableSet<QuantifiableVariable> |
Taclet.getBoundVariablesHelper()
collects bound variables in taclet entities others than goal templates
|
protected ImmutableSet<QuantifiableVariable> |
FindTaclet.getBoundVariablesHelper()
returns the variables that occur bound in the find part
|
protected ImmutableSet<QuantifiableVariable> |
NoFindTaclet.getBoundVariablesHelper()
the empty set as a no find taclet has no other entities where
variables cann occur bound than in the goal templates
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
MatchConditions.addRenaming(QuantifiableVariable q1,
QuantifiableVariable q2) |
Modifier and Type | Method and Description |
---|---|
Namespace<QuantifiableVariable> |
TacletApp.extendVarNamespaceForSV(Namespace<QuantifiableVariable> var_ns,
SchemaVariable sv)
creates a new variable namespace by adding names of the instantiations of
the schema variables in the context of the given schema variable and (if
the TacletApp's prefix has the context flag set) by adding names of the
logic variables of the context.
|
Modifier and Type | Method and Description |
---|---|
boolean |
ChildTermLabelPolicy.addLabel(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,
Term childTerm,
TermLabel label)
|
boolean |
ChildTermLabelPolicy.isRuleApplicationSupported(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)
Decides if the currently active
Rule application is supported or not. |
TermLabel |
OriginTermLabelPolicy.keepLabel(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,
TermLabel label) |
TermLabel |
TermLabelPolicy.keepLabel(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,
TermLabel label)
|
TermLabel |
PerpetualTermLabelPolicy.keepLabel(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,
TermLabel label) |
TermLabel |
StayOnOperatorTermLabelPolicy.keepLabel(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,
TermLabel label)
|
TermLabel |
StayOnFormulaTermLabelPolicy.keepLabel(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,
TermLabel label)
|
void |
TermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
FormulaTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
LoopBodyTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
BlockContractValidityTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
SymbolicExecutionTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
void |
LoopInvariantNormalBehaviorTermLabelUpdate.updateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
java.util.Set<TermLabel> labels)
|
Modifier and Type | Method and Description |
---|---|
static MatchInstruction |
Instruction.matchAndBindVariables(ImmutableArray<QuantifiableVariable> boundVars) |
static MatchInstruction |
Instruction.unbindVariables(ImmutableArray<QuantifiableVariable> boundVars) |
Constructor and Description |
---|
BindVariablesInstruction(ImmutableArray<QuantifiableVariable> boundVars) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<QuantifiableVariable> |
AntecSuccTacletGoalTemplate.getBoundVariables()
rertieves and returns all variables that are bound in the
goal template
|
ImmutableSet<QuantifiableVariable> |
RewriteTacletGoalTemplate.getBoundVariables()
rertieves and returns all variables that are bound in the
goal template
|
ImmutableSet<QuantifiableVariable> |
TacletGoalTemplate.getBoundVariables()
retrieves and returns all variables that are bound in the
goal template
|
Modifier and Type | Method and Description |
---|---|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateTerm(Term term,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services)
Translates the given term into input syntax and adds the resulting
string to the StringBuffer sb.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateUnknown(Term term,
java.util.Vector<QuantifiableVariable> quantifiedVars,
Services services)
Takes care of sequent tree parts that were not matched in
translate(term, skolemization).
|
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.createSeqDef(SLExpression a,
SLExpression b,
SLExpression t,
KeYJavaType declsType,
ImmutableList<? extends QuantifiableVariable> declVars) |
protected Term |
JmlTermFactory.typerestrict(KeYJavaType kjt,
boolean nullable,
java.lang.Iterable<? extends QuantifiableVariable> qvs)
Provide restriction terms for the declared KeYJavaType
Note that these restrictions only apply to the JML to DL translation.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<QuantifiableVariable> |
TriggersSet.getUniQuantifiedVariables() |
ImmutableMap<QuantifiableVariable,Term> |
Substitution.getVarMap() |
Modifier and Type | Method and Description |
---|---|
Term |
Substitution.getSubstitutedTerm(QuantifiableVariable var) |
boolean |
QuanEliminationAnalyser.isEliminableVariableAllPaths(QuantifiableVariable var,
Term matrix,
boolean ex)
The variable
var is eliminable on all
conjunctive/disjunctive paths through matrix (depending on
whether ex is true/false) |
boolean |
QuanEliminationAnalyser.isEliminableVariableSomePaths(QuantifiableVariable var,
Term matrix,
boolean ex)
The variable
var is either eliminable or does not occur on
all conjunctive/disjunctive paths through matrix
(depending on whether ex is true/false) |
Modifier and Type | Method and Description |
---|---|
boolean |
Substitution.isTotalOn(ImmutableSet<QuantifiableVariable> vars) |
Constructor and Description |
---|
Substitution(ImmutableMap<QuantifiableVariable,Term> map) |
Modifier and Type | Method and Description |
---|---|
void |
DefaultTacletSetTranslation.eventQuantifiedVariable(QuantifiableVariable var) |
void |
TranslationListener.eventQuantifiedVariable(QuantifiableVariable var)
Called when the translator finds a term that has a quantified variable.
|
Modifier and Type | Method and Description |
---|---|
void |
UserDefinedSymbols.addVariable(QuantifiableVariable symbol) |
Copyright © 2003-2019 The KeY-Project.