Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
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.nparser.builder | |
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.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.label | |
de.uka.ilkd.key.rule.match.legacy | |
de.uka.ilkd.key.rule.match.vm.instructions | |
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.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.smt.newsmt2 | |
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.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.model.impl | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.taclettranslation.lemma |
Modifier and Type | Method and Description |
---|---|
LRUCache<Operator,java.lang.Integer> |
ServiceCaches.getIntroductionTimeCache() |
Modifier and Type | Method and Description |
---|---|
protected Namespace<Operator> |
LDT.functions()
returns the basic functions of the model
|
Modifier and Type | Method and Description |
---|---|
Sort |
HeapLDT.getSortOfSelect(Operator op)
If the passed operator is an instance of "select", this method returns
the sort of the function (identical to its return type); otherwise,
returns null.
|
boolean |
HeapLDT.isSelectOp(Operator op) |
Modifier and Type | Interface and Description |
---|---|
interface |
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
Modifier and Type | Method and Description |
---|---|
Operator |
TermImpl.op() |
Operator |
Term.op()
The top operator (e.g., in "A and B" this is "and", in f(x,y) it is "f").
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<Operator> |
OpCollector.ops() |
Modifier and Type | Method and Description |
---|---|
boolean |
OpCollector.contains(Operator op) |
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,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator junctor,
java.util.List<Term> terms)
Reduce the given list of terms into a one term by using the operator.
|
Term |
TermFactory.createTerm(Operator op,
Term... subs) |
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) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
TermLabel label) |
Term |
TermFactory.createTerm(Operator op,
Term sub,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term sub1,
Term sub2,
ImmutableArray<TermLabel> labels) |
Constructor and Description |
---|
TermCreationException(Operator op,
Term failed) |
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 |
---|---|
static boolean |
OriginTermLabel.canAddLabel(Operator op,
Services services)
Determines whether an
OriginTermLabel can be added to a term with the specified
operator. |
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 | Interface and Description |
---|---|
interface |
IObserverFunction |
interface |
IProgramMethod |
interface |
IProgramVariable |
interface |
ParsableVariable
This interface represents the variables that can be recognized
by one of the parsers.
|
interface |
QuantifiableVariable
This interface represents the variables that can be bound
(by quantifiers or other binding operators).
|
interface |
SchemaVariable
This interface represents the root of a schema variable hierarchy to be
express termstructures that match on logical terms.
|
interface |
SortedOperator
Operator with well-defined argument and result sorts.
|
interface |
TermTransformer
TermTransformer perform complex term transformation which cannot be
(efficiently or at all) described by taclets.
|
interface |
UpdateableOperator
Operators implementing this interface may stand for
locations as well.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractSortedOperator
Abstract sorted operator class offering some common functionality.
|
class |
AbstractSV
Abstract base class for schema variables.
|
class |
AbstractTermTransformer
Abstract class factoring out commonalities of typical term transformer implementations.
|
class |
ElementaryUpdate
Class of operators for elementary updates, i.e., updates of the form
"x := t".
|
class |
Equality
This class defines the equality operator "=".
|
class |
FormulaSV
A schema variable that is used as placeholder for formulas.
|
class |
Function
Objects of this class represent function and predicate symbols.
|
class |
IfExThenElse
This singleton class implements a conditional operator
"\ifEx iv; (phi) \then (t1) \else (t2)", where iv is an integer logic
variable, phi is a formula, and where t1 and t2 are terms with the same sort.
|
class |
IfThenElse
This singleton class implements a general conditional operator
\if (phi) \then (t1) \else (t2).
|
class |
Junctor
Class of junctor operators, i.e., operators connecting
a given number of formula to create another formula.
|
class |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
class |
LogicVariable
The objects of this class represent logical variables,
used e.g.
|
class |
Modality
This class is used to represent a dynamic logic modality like
diamond and box (but also extensions of DL like
preserves and throughout are possible in the future).
|
class |
ModalOperatorSV
Schema variable matching modal operators.
|
class |
ObserverFunction
Objects of this class represent "observer" function or predicate symbols.
|
class |
ProgramConstant
This class represents currently only static final fields initialised with
a compile time constant.
|
class |
ProgramMethod
The program method represents a (pure) method in the logic.
|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
class |
ProgramVariable
The objects of this class represent program variables and program
constants (resulting from static final declarations in programs; TODO: it is
weird that constants are a special case of variables).
|
class |
Quantifier
The two objects of this class represent the universal and the existential
quantifier, respectively.
|
class |
SkolemTermSV
Schema variable that is instantiated with fresh Skolem constants.
|
class |
SortDependingFunction
The objects of this class represent families of function symbols, where
each family contains an instantiation of a template symbol for a particular
sort.
|
class |
SubstOp
Standard first-order substitution operator, resolving clashes but not
preventing (usually unsound) substitution of non-rigid terms across modal
operators.
|
class |
TermLabelSV
A schema variable which matches term labels
|
class |
TermSV
A schema variable that is used as placeholder for terms.
|
class |
Transformer
Functions with a restricted/special rule set only applicable for the top level
of the term transformer and not directly for its arguments, prohibiting any rule
applications to sub arguments as well as applications from outside such as update applications.
|
class |
UpdateApplication
Singleton class defining a binary operator {u}t that applies updates u to
terms, formulas, or other updates t.
|
class |
UpdateJunctor
Class of update junctor operators, i.e., operators connecting
a given number of updates to create another update.
|
class |
UpdateSV
A schema variable that is used as placeholder for updates.
|
class |
VariableSV
Schema variable that is instantiated with logical variables.
|
class |
WarySubstOp |
Modifier and Type | Method and Description |
---|---|
abstract Operator |
ProgramVariable.rename(Name name)
Returns an equivalent variable with the new name.
|
Operator |
ProgramConstant.rename(Name name) |
Modifier and Type | Method and Description |
---|---|
protected Operator |
DefaultBuilder.lookupVarfuncId(org.antlr.v4.runtime.ParserRuleContext ctx,
java.lang.String varfuncName,
java.lang.String sortName,
Sort sort)
looks up a function, (program) variable or static query of the
given name varfunc_id and the argument terms args in the namespaces
and java info.
|
Operator |
TacletPBuilder.visitVarId(KeYParser.VarIdContext ctx) |
Modifier and Type | Method and Description |
---|---|
Term |
ExpressionBuilder.createAttributeTerm(Term prefix,
Operator attribute,
org.antlr.v4.runtime.ParserRuleContext ctx) |
Modifier and Type | Method and Description |
---|---|
Operator |
OpReplacer.replace(Operator op)
Replaces in an operator.
|
Modifier and Type | Method and Description |
---|---|
java.util.Map<Operator,Term> |
OpReplacer.replace(java.util.Map<Operator,Term> myMap)
Replaces in a map from Operator to Term.
|
Modifier and Type | Method and Description |
---|---|
Operator |
OpReplacer.replace(Operator op)
Replaces in an operator.
|
static Term |
OpReplacer.replace(Operator toReplace,
Operator with,
Term in,
TermFactory tf)
Replace an operator.
|
static Term |
OpReplacer.replace(Operator toReplace,
Operator with,
Term in,
TermFactory tf,
Proof proof)
Replace an operator.
|
Modifier and Type | Method and Description |
---|---|
java.util.Map<Operator,Term> |
OpReplacer.replace(java.util.Map<Operator,Term> myMap)
Replaces in a map from Operator to Term.
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.add(ModalOperatorSV sv,
Operator op,
Services services) |
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 | Class and Description |
---|---|
class |
ElementMatcher<T extends Operator> |
Modifier and Type | Class and Description |
---|---|
class |
Instruction<OP extends Operator>
enum encoding the instructions of the matching vm
|
class |
MatchOpIdentityInstruction<T extends Operator>
The match instruction reports a success if the top level operator of the term to be matched is the same(identical) operator
like the one for which this instruction has been instantiated
|
Modifier and Type | Field and Description |
---|---|
protected OP |
Instruction.op |
Modifier and Type | Method and Description |
---|---|
static Instruction<Operator> |
Instruction.matchOp(Operator op) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
MatchProgramSVInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOperatorInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
MatchConditions |
MatchOpIdentityInstruction.match(Operator instantiationCandidate,
MatchConditions matchConditions,
Services services) |
static Instruction<Operator> |
Instruction.matchOp(Operator op) |
Modifier and Type | Class and Description |
---|---|
class |
AddCast |
class |
ArrayBaseInstanceOf
Creates an Type::instance(..) term for the component type of the
array.
|
class |
ConstantValue
Replace a program variable that is a compile-time constant with the
value of the initializer
|
class |
CreateBeforeLoopUpdate
Initializes the "before loop" update needed for the assignable clause.
|
class |
CreateFrameCond
Creates the frame condition (aka "assignable clause") for the given loop.
|
class |
CreateHeapAnonUpdate
Creates the anonymizing update for the heap.
|
class |
CreateLocalAnonUpdate
Expects a loop body and creates the anonymizing update
out_1:=anon_1||...||out_n:=anon_n , where anon_1, ..., anon_n are
the written variables in the loop body visible to the outside. |
class |
CreateWellformedCond
Creates the wellformedness condition for the given anonymizing heap terms if
they apply for the current profile and modality type.
|
class |
EnumConstantValue
resolve a program variable to an integer literal.
|
class |
ExpandQueriesMetaConstruct
Uses the class
QueryExpand in order to insert query expansions in the term that the
meta construct is applied on. |
class |
IntroAtPreDefsOp |
class |
MemberPVToField |
class |
ObserverEqualityMetaConstruct
This meta contruct allows one to prove equality (equivalence) of two
observer terms if they belong to the same observer function symbol.
|
Modifier and Type | Class and Description |
---|---|
class |
DivideLCRMonomials
Metaoperator for computing the result of dividing one monomial by another
|
class |
DivideMonomials
Metaoperator for computing the result of dividing one monomial by another
|
class |
MetaAdd |
class |
MetaArithBitMaskOp |
class |
MetaBinaryAnd |
class |
MetaBinaryOr |
class |
MetaBinaryXOr |
class |
MetaDiv |
class |
MetaEqual |
class |
MetaGeq |
class |
MetaGreater |
class |
MetaLeq |
class |
MetaLess |
class |
MetaMul |
class |
MetaPow
Computes the pow function for literals.
|
class |
MetaShift |
class |
MetaShiftLeft |
class |
MetaShiftRight |
class |
MetaSub |
Modifier and Type | Method and Description |
---|---|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateFunc(Operator o,
java.util.ArrayList<java.lang.StringBuffer> sub)
translate a function.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateVariable(Operator op) |
Modifier and Type | Method and Description |
---|---|
boolean |
DefinedSymbolsHandler.canHandle(Operator op) |
boolean |
SeqDefHandler.canHandle(Operator op) |
boolean |
CastingFunctionsHandler.canHandle(Operator op) |
boolean |
QuantifierHandler.canHandle(Operator op) |
boolean |
LogicalVariableHandler.canHandle(Operator op) |
boolean |
SMTHandler.canHandle(Operator op)
Query if this handler can translate an operator.
|
boolean |
BooleanConnectiveHandler.canHandle(Operator op) |
boolean |
UninterpretedSymbolsHandler.canHandle(Operator op) |
boolean |
PolymorphicHandler.canHandle(Operator op) |
boolean |
InstanceOfHandler.canHandle(Operator op) |
boolean |
IntegerOpHandler.canHandle(Operator op) |
boolean |
FieldConstantHandler.canHandle(Operator op) |
boolean |
UpdateHandler.canHandle(Operator op) |
boolean |
SumProdHandler.canHandle(Operator op) |
boolean |
NumberConstantsHandler.canHandle(Operator op) |
boolean |
CastHandler.canHandle(Operator op) |
Modifier and Type | Method and Description |
---|---|
protected static TermFeature |
StaticFeatureCollection.op(Operator op) |
protected static TermFeature |
StaticFeatureCollection.opSub(Operator op,
TermFeature sub0) |
protected static TermFeature |
StaticFeatureCollection.opSub(Operator op,
TermFeature sub0,
TermFeature sub1) |
protected static ProjectionToTerm |
StaticFeatureCollection.opTerm(Operator op,
ProjectionToTerm subTerm) |
protected static ProjectionToTerm |
StaticFeatureCollection.opTerm(Operator op,
ProjectionToTerm[] subTerms) |
protected static ProjectionToTerm |
StaticFeatureCollection.opTerm(Operator op,
ProjectionToTerm subTerm0,
ProjectionToTerm subTerm1) |
Modifier and Type | Method and Description |
---|---|
static Feature |
DirectlyBelowSymbolFeature.create(Operator badSymbol) |
static Feature |
DirectlyBelowSymbolFeature.create(Operator badSymbol,
int index) |
protected int |
AbstractMonomialSmallerThanFeature.introductionTime(Operator op,
Goal goal) |
protected abstract boolean |
DirectlyBelowFeature.isBadSymbol(Operator op) |
protected boolean |
DirectlyBelowSymbolFeature.isBadSymbol(Operator op) |
Modifier and Type | Class and Description |
---|---|
class |
Metavariable
Deprecated.
|
Modifier and Type | Method and Description |
---|---|
static TermFeature |
OperatorTF.create(Operator op) |
Modifier and Type | Method and Description |
---|---|
static TermFeature |
OperatorClassTF.create(java.lang.Class<? extends Operator> op) |
Modifier and Type | Method and Description |
---|---|
static ProjectionToTerm |
TermConstructionProjection.create(Operator op,
ProjectionToTerm[] subTerms) |
Modifier and Type | Method and Description |
---|---|
static boolean |
TruthValueTracingUtil.isIfThenElseFormula(Operator operator,
ImmutableArray<Term> subs)
|
static boolean |
TruthValueTracingUtil.isLogicOperator(Operator operator,
ImmutableArray<Term> subs)
|
static boolean |
TruthValueTracingUtil.isPredicate(Operator operator)
Checks if the given
Operator is a predicate. |
Modifier and Type | Method and Description |
---|---|
protected void |
ExecutionVariable.groupGoalsByValue(ImmutableList<Goal> goals,
Operator operator,
Term siteProofSelectTerm,
Term siteProofCondition,
java.util.Map<Term,java.util.List<Goal>> valueMap,
java.util.List<Goal> unknownValues,
Services services)
Groups all
Goal s which provides the same value. |
protected ExecutionValue[] |
ExecutionVariable.instantiateValuesFromSideProof(InitConfig initConfig,
Services services,
TermBuilder tb,
ApplyStrategyInfo info,
Operator resultOperator,
Term siteProofSelectTerm,
Term siteProofCondition)
Analyzes the side proof defined by the
ApplyStrategyInfo
and creates ExecutionValue s from it. |
Modifier and Type | Method and Description |
---|---|
Operator |
SymbolicExecutionUtil.SiteProofVariableValueInput.getOperator()
Returns the
Operator which is the predicate that contains the value interested in. |
Modifier and Type | Method and Description |
---|---|
static java.util.Set<Operator> |
SymbolicExecutionSideProofUtil.extractRelevantThings(Services services,
Sequent sequentToProve)
|
Modifier and Type | Method and Description |
---|---|
static java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
SymbolicExecutionSideProofUtil.computeResultsAndConditions(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Operator operator,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term and conditions. |
static Term |
SymbolicExecutionSideProofUtil.extractOperatorTerm(ApplyStrategyInfo info,
Operator operator)
Extracts the operator term for the formula with the given
Operator
from the site proof result (ApplyStrategyInfo ). |
static Term |
SymbolicExecutionSideProofUtil.extractOperatorTerm(Goal goal,
Operator operator)
|
static Term |
SymbolicExecutionSideProofUtil.extractOperatorTerm(Node node,
Operator operator)
|
static Term |
SymbolicExecutionSideProofUtil.extractOperatorValue(Goal goal,
Operator operator)
|
static Term |
SymbolicExecutionSideProofUtil.extractOperatorValue(Node node,
Operator operator)
|
static boolean |
SymbolicExecutionUtil.isBaseHeap(Operator op,
HeapLDT heapLDT)
Checks if the given
Operator is the base heap. |
static boolean |
SymbolicExecutionUtil.isBoolean(Services services,
Operator op)
Checks if the given
Operator is a boolean. |
static boolean |
SymbolicExecutionUtil.isHeap(Operator op,
HeapLDT heapLDT)
Checks if the given
Operator is a heap. |
static boolean |
SymbolicExecutionUtil.isNumber(Operator op)
Checks if the given
Operator is a number. |
Modifier and Type | Method and Description |
---|---|
static boolean |
SymbolicExecutionSideProofUtil.containsIrrelevantThings(Services services,
SequentFormula sf,
java.util.Set<Operator> relevantThings)
Checks if the given
SequentFormula contains irrelevant things
(things which are not contained in the relevantThingsToProve and are no Java types) |
static boolean |
SymbolicExecutionSideProofUtil.isIrrelevantCondition(Services services,
Sequent initialSequent,
java.util.Set<Operator> relevantThingsInSequentToProve,
SequentFormula sf)
Checks if the given
SequentFormula is a relevant condition. |
Constructor and Description |
---|
SiteProofVariableValueInput(Sequent sequentToProve,
Operator operator)
Constructor.
|
Constructor and Description |
---|
ContainsIrrelevantThingsVisitor(Services services,
java.util.Set<Operator> relevantThings)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected Operator |
GenericRemovingLemmaGenerator.replaceOp(Operator op,
TermServices services)
Sometimes operators must be replaced during lemma generation.
|
Modifier and Type | Method and Description |
---|---|
protected Operator |
GenericRemovingLemmaGenerator.replaceOp(Operator op,
TermServices services)
Sometimes operators must be replaced during lemma generation.
|
Copyright © 2003-2019 The KeY-Project.