Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.prover | |
de.uka.ilkd.key.prover.impl | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
org.key_project.ui.interactionlog | |
org.key_project.ui.interactionlog.model |
Modifier and Type | Method and Description |
---|---|
void |
InteractionListener.runAutoMode(java.util.List<Node> initialGoals,
Proof proof,
ApplyStrategyInfo info) |
Modifier and Type | Method and Description |
---|---|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
Goal goal)
starts a proof search for a given goals using the given strategy settings
instead the ones configures in the proof
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals)
starts a proof search for a set of goals using the given strategy settings
instead the ones configures in the proof
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout,
boolean stopAtFirstNonCloseableGoal)
This entry point to the proof may provide inconsistent data.
|
ApplyStrategyInfo |
ProverCore.start(Proof proof,
ImmutableList<Goal> goals,
StrategySettings stratSet)
starts a proof search for a set of goals using the given strategy settings
instead the ones configures in the proof
|
Modifier and Type | Method and Description |
---|---|
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
Goal goal) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals,
int maxSteps,
long timeout,
boolean stopAtFirstNonCloseableGoal) |
ApplyStrategyInfo |
ApplyStrategy.start(Proof proof,
ImmutableList<Goal> goals,
StrategySettings stratSet) |
Modifier and Type | Method and Description |
---|---|
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 |
---|---|
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve)
Starts a site proof for the given
Sequent . |
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption)
Starts a site proof for the given
Sequent . |
static ApplyStrategyInfo |
SymbolicExecutionSideProofUtil.startSideProof(Proof proof,
ProofStarter starter,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption)
Starts a site proof.
|
Modifier and Type | Method and Description |
---|---|
static void |
SymbolicExecutionSideProofUtil.disposeOrStore(java.lang.String description,
ApplyStrategyInfo info)
|
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 ). |
Modifier and Type | Method and Description |
---|---|
ApplyStrategyInfo |
ProofStarter.start()
starts proof attempt
|
ApplyStrategyInfo |
ProofStarter.start(ImmutableList<Goal> goals)
starts proof attempt
|
Modifier and Type | Method and Description |
---|---|
void |
InteractionRecorder.runAutoMode(java.util.List<Node> initialGoals,
Proof proof,
ApplyStrategyInfo info) |
Modifier and Type | Method and Description |
---|---|
ApplyStrategyInfo |
AutoModeInteraction.getInfo() |
Modifier and Type | Method and Description |
---|---|
void |
AutoModeInteraction.setInfo(ApplyStrategyInfo info) |
Constructor and Description |
---|
AutoModeInteraction(java.util.List<Node> initialNodes,
ApplyStrategyInfo info) |
Copyright © 2003-2019 The KeY-Project.