Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
de.uka.ilkd.key.control.instantiation_model | |
de.uka.ilkd.key.gui.join | |
de.uka.ilkd.key.gui.nodeviews | |
de.uka.ilkd.key.gui.testgen |
This package contains the graphical user interface of the test generation backend.
|
de.uka.ilkd.key.informationflow.proof | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.macros.scripts |
Proof script commands are a simple proof automation facility.
|
de.uka.ilkd.key.nparser | |
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.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.proof.join | |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.executor.javadl | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
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.smt.counterexample | |
de.uka.ilkd.key.smt.newsmt2 | |
de.uka.ilkd.key.smt.testgen | |
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.rule | |
de.uka.ilkd.key.symbolic_execution.slicing | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.taclettranslation | |
de.uka.ilkd.key.testgen | |
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 |
---|---|
Sequent |
ProjectedNode.getSequent()
Return the sequent of a proof node
|
Modifier and Type | Method and Description |
---|---|
java.util.List<VariableAssignments> |
Matcher.matchPattern(java.lang.String pattern,
Sequent currentSeq,
VariableAssignments assignments)
Matches a sequent against a sequent pattern (a schematic sequent) returns a list of Nodes containing matching
results from where the information about instantiated schema variables can be extracted.
|
java.util.List<VariableAssignments> |
ScriptApi.matchPattern(java.lang.String pattern,
Sequent currentSeq,
VariableAssignments assignments)
Matches a sequent against a sequent pattern (a schematic sequent) returns a list of Nodes containing matching
results from where the information about instantiated schema variables can be extracted.
|
Constructor and Description |
---|
TacletInstantiationModel(TacletApp app,
Sequent seq,
NamespaceSet nss,
AbbrevMap scm,
Goal goal)
Create new data model for the apply Taclet dialog wrapping a combo box model
and a table model.
|
Modifier and Type | Method and Description |
---|---|
void |
SequentViewer.setSequent(Sequent sequent,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected Sequent |
InsertHiddenTacletMenuItem.checkTaclet(Taclet t)
determines the sequent with the formulas to be added
or null if the given taclet is not thought to be displayed
by this component
|
protected Sequent |
InsertSystemInvariantTacletMenuItem.checkTaclet(Taclet t)
determines the sequent with the formulas to be added
or null if the given taclet is not thought to be displayed
by this component
|
protected abstract Sequent |
InsertionTacletBrowserMenuItem.checkTaclet(Taclet t) |
Modifier and Type | Method and Description |
---|---|
protected Proof |
CounterExampleAction.MainWindowCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
Constructor and Description |
---|
InfFlowProof(java.lang.String name,
Sequent sequent,
java.lang.String header,
TacletIndex rules,
BuiltInRuleIndex builtInRules,
InitConfig initConfig) |
Modifier and Type | Field and Description |
---|---|
static Sequent |
Sequent.EMPTY_SEQUENT |
Modifier and Type | Method and Description |
---|---|
static Sequent |
Sequent.createAnteSequent(Semisequent ante)
creates a new Sequent with empty succedent
|
static Sequent |
Sequent.createSequent(Semisequent ante,
Semisequent succ)
creates a new Sequent
|
static Sequent |
Sequent.createSuccSequent(Semisequent succ)
creates a new Sequent with empty antecedent
|
Sequent |
SequentChangeInfo.getOriginalSequent() |
Sequent |
SequentChangeInfo.sequent()
returns the resulting sequent
|
Modifier and Type | Method and Description |
---|---|
static SequentChangeInfo |
SequentChangeInfo.createSequentChangeInfo(boolean antec,
SemisequentChangeInfo semiCI,
Sequent result,
Sequent original)
creates a new sequent change info whose semisequent described by the
value of the selector antec (true selects antecedent; false selects
succedent) has changed.
|
static SequentChangeInfo |
SequentChangeInfo.createSequentChangeInfo(PosInOccurrence pos,
SemisequentChangeInfo semiCI,
Sequent result,
Sequent original)
creates a new sequent change info whose semisequent described by position
pos has changed.
|
static SequentChangeInfo |
SequentChangeInfo.createSequentChangeInfo(SemisequentChangeInfo anteCI,
SemisequentChangeInfo sucCI,
Sequent result,
Sequent original)
creates a new sequent change info whose semisequents have changed.
|
static PosInOccurrence |
PosInOccurrence.findInSequent(Sequent seq,
int formulaNumber,
PosInTerm pos) |
void |
BoundVarsVisitor.visit(Sequent visited)
visits a sequent
|
Modifier and Type | Method and Description |
---|---|
static SequentChangeInfo |
OriginTermLabel.removeOriginLabels(Sequent seq,
Services services)
Removes all
OriginTermLabel from the specified sequent. |
Modifier and Type | Method and Description |
---|---|
Sequent |
JavascriptCommand.JavascriptInterface.getSelectedGoal() |
Sequent |
EngineState.toSequent(java.lang.String sequent) |
Modifier and Type | Method and Description |
---|---|
static PosInOccurrence |
MacroCommand.extractMatchingPio(Sequent sequent,
java.lang.String matchRegEx,
Services services)
TODO
|
Modifier and Type | Method and Description |
---|---|
Sequent |
KeyIO.parseSequence(org.antlr.v4.runtime.CharStream stream)
Given an input stream, this function returns a sequent if parsable.
|
Modifier and Type | Method and Description |
---|---|
Sequent |
ExpressionBuilder.visitSeq(KeYParser.SeqContext ctx) |
Sequent |
ExpressionBuilder.visitSeqEOF(KeYParser.SeqEOFContext ctx) |
Modifier and Type | Method and Description |
---|---|
Sequent |
DefaultTermParser.parseSeq(java.io.Reader in,
Services services,
NamespaceSet nss,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a sequent with the
specified namespaces.
|
Modifier and Type | Method and Description |
---|---|
Sequent |
SequentPrintFilter.getOriginalSequent() |
Modifier and Type | Method and Description |
---|---|
void |
LogicPrinter.printSequent(Sequent seq)
Pretty-print a sequent.
|
void |
LogicPrinter.printSequent(Sequent seq,
boolean finalbreak) |
protected void |
LogicPrinter.printTextSequent(Sequent seq,
java.lang.String text,
boolean frontbreak) |
static java.lang.String |
LogicPrinter.quickPrintSequent(Sequent s,
Services services)
Converts a sequent to a string.
|
void |
SequentPrintFilter.setSequent(Sequent s)
sets the (original) sequent of this filter
|
Modifier and Type | Method and Description |
---|---|
Sequent |
Goal.sequent()
returns the sequent of the node
|
Sequent |
Node.sequent()
returns the sequent of this node
|
Modifier and Type | Method and Description |
---|---|
SemisequentTacletAppIndex |
SemisequentTacletAppIndex.addTaclets(RuleFilter filter,
Sequent s,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
Create an index that additionally contains the taclets that are selected
by
filter |
SequentChangeInfo |
ProgVarReplacer.replace(Sequent s)
replaces in a sequent
|
void |
Node.setSequent(Sequent seq)
sets the sequent at this node
|
Constructor and Description |
---|
Node(Proof proof,
Sequent seq)
creates a node with the given contents
|
Node(Proof proof,
Sequent seq,
Node parent)
creates a node with the given contents, the given collection of children (all
elements must be of class Node) and the given parent node.
|
Proof(java.lang.String name,
Sequent sequent,
java.lang.String header,
TacletIndex rules,
BuiltInRuleIndex builtInRules,
InitConfig initConfig) |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
OutputStreamProofSaver.posInOccurrence2Proof(Sequent seq,
PosInOccurrence pos) |
Modifier and Type | Method and Description |
---|---|
Sequent |
ProspectivePartner.getSequent(int index) |
Modifier and Type | Method and Description |
---|---|
Sequent |
Taclet.TacletLabelHint.getSequent()
Returns the optional
Sequent of the add or replace part of the taclet. |
Sequent |
Taclet.ifSequent()
returns the if-sequence of the application part of the Taclet.
|
Sequent |
TacletApplPart.ifSequent()
returns the if-sequent of the application part of a Taclet
|
Modifier and Type | Method and Description |
---|---|
void |
BoundUniquenessChecker.addAll(Sequent seq)
adds all formulas in the sequent to the list of terms to
include in the uniqueness check
|
static ImmutableList<IfFormulaInstantiation> |
IfFormulaInstSeq.createList(Sequent p_s,
boolean antec,
Services services) |
ImmutableList<TacletApp> |
TacletApp.findIfFormulaInstantiations(Sequent p_seq,
Services p_services)
Find all possible instantiations of the if sequent formulas within the
sequent "p_seq".
|
static java.util.List<PosInOccurrence> |
UseDependencyContractRule.getSteps(java.util.List<LocationVariable> heapContext,
PosInOccurrence pos,
Sequent seq,
Services services) |
PosInOccurrence |
UseDependencyContractApp.step(Sequent seq,
TermServices services) |
void |
TacletSchemaVariableCollector.visit(Sequent seq)
goes through the given sequent an collects all vars found
|
void |
SVNameCorrespondenceCollector.visit(Sequent seq)
collects all correspondences in a sequent
|
Constructor and Description |
---|
BoundUniquenessChecker(Sequent seq) |
BoundUniquenessChecker(Term t,
Sequent seq) |
IfFormulaInstSeq(Sequent p_seq,
boolean antec,
SequentFormula p_cf) |
IfFormulaInstSeq(Sequent seq,
int formulaNr) |
TacletApplPart(Sequent ifseq,
ImmutableList<NewVarcond> varsNew,
ImmutableList<NotFreeIn> varsNotFreeIn,
ImmutableList<NewDependingOn> varsNewDependingOn,
ImmutableList<VariableCondition> variableConditions)
constructs a new TacletApplPart object with the given Sequent,
a list of variables that are new, a list of variable pairs that
represent the NotFreeIn relation and a list of additional
generic variable conditions.
|
TacletLabelHint(Taclet.TacletLabelHint.TacletOperation tacletOperation,
Sequent sequent)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
protected void |
RewriteTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
SuccTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
NoFindTacletExecutor.applyAdd(TermLabelState termLabelState,
Sequent add,
SequentChangeInfo currentSequent,
Services services,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp)
adds the sequent of the add part of the Taclet to the goal sequent
|
Modifier and Type | Method and Description |
---|---|
Term |
WhileInvariantTransformer.transform(TermLabelState termLabelState,
Rule rule,
RuleApp ruleApp,
Goal goal,
Sequent applicationSequent,
PosInOccurrence applicationPos,
Term initialPost,
Term invariantFramingTermination,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Modifier and Type | Field and Description |
---|---|
protected Sequent |
TacletBuilder.ifseq |
Modifier and Type | Method and Description |
---|---|
Sequent |
TacletBuilder.ifSequent() |
Sequent |
AntecSuccTacletGoalTemplate.replaceWith()
a Taclet may replace a Sequent by another.
|
Sequent |
TacletGoalTemplate.sequent()
a Taclet may add a new Sequent as Goal.
|
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.setIfSequent(Sequent seq)
sets the ifseq of the Taclet to be built
|
Constructor and Description |
---|
AntecSuccTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Sequent replacewith) |
AntecSuccTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Sequent replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
RewriteTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Term replacewith) |
RewriteTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Term replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
TacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules)
creates new Goaldescription
same effect as
new TacletGoalTemplate(addedSeq,
addedRules,
SetAsListOf. |
TacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
ImmutableSet<SchemaVariable> addedProgVars)
creates new Goaldescription
|
Modifier and Type | Method and Description |
---|---|
Sequent |
SMTProblem.getSequent() |
Modifier and Type | Method and Description |
---|---|
static Term |
SMTProblem.sequentToTerm(Sequent s,
Services services) |
java.lang.StringBuffer |
SMTObjTranslator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings) |
java.lang.StringBuffer |
AbstractSMTTranslator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings) |
java.lang.CharSequence |
SMTTranslator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings)
Translates a problem into the given syntax.
|
Constructor and Description |
---|
AbstractSMTTranslator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
SimplifyTranslator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
SmtLib2Translator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
SmtLibTranslator(Sequent sequent,
Services services,
AbstractSMTTranslator.Configuration config)
Just a constructor which starts the conversion to Simplify syntax.
|
SMTProblem(Sequent s,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected Sequent |
AbstractCounterExampleGenerator.createNewSequent(Sequent oldSequent)
|
Modifier and Type | Method and Description |
---|---|
protected Sequent |
AbstractCounterExampleGenerator.createNewSequent(Sequent oldSequent)
|
protected abstract Proof |
AbstractCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
protected Proof |
AbstractSideProofCounterExampleGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent,
java.lang.String proofName)
Creates a new
Proof . |
void |
AbstractCounterExampleGenerator.searchCounterExample(UserInterfaceControl ui,
Proof oldProof,
Sequent oldSequent)
Searches a counter example for the given
Sequent . |
Modifier and Type | Method and Description |
---|---|
java.lang.CharSequence |
ModularSMTLib2Translator.translateProblem(Sequent sequent,
Services services,
SMTSettings settings) |
Modifier and Type | Method and Description |
---|---|
protected Proof |
AbstractTestGenerator.createProof(UserInterfaceControl ui,
Proof oldProof,
java.lang.String newName,
Sequent newSequent) |
Modifier and Type | Method and Description |
---|---|
protected Sequent |
IsInRangeProvable.toSequent(ImmutableSet<Term> axioms,
Term toProve)
creates the sequent
axioms ==> toProve |
Modifier and Type | Method and Description |
---|---|
protected boolean |
IsInRangeProvable.isProvable(Sequent seq,
Services services)
checks if the sequent is provable
|
Modifier and Type | Method and Description |
---|---|
protected Sequent |
SymbolicLayoutExtractor.createSequentForEquivalenceClassComputation()
Creates a
Sequent which is used to compute equivalence classes. |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractUpdateExtractor.collectLocationsFromUpdates(Sequent sequent,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
java.util.Set<Term> updateCreatedObjectsToFill,
java.util.Set<Term> updateValueObjectsToFill,
java.util.Set<Term> objectsToIgnore)
|
protected java.util.Set<Term> |
SymbolicLayoutExtractor.collectObjectsFromSequent(Sequent sequent,
java.util.Set<Term> objectsToIgnore)
Collects all objects which are used in the conditions of the
Sequent . |
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
AbstractUpdateExtractor.extractLocationsFromSequent(Sequent sequent,
java.util.Set<Term> objectsToIgnore)
|
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. |
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
AbstractSideProofRule.computeResultsAndConditions(Services services,
Goal goal,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Function newPredicate)
Starts the side proof and extracts the result
Term and conditions. |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractSlicer.analyzeSequent(Services services,
Sequent sequent,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the given
Sequent for equalities specified by top level formulas. |
Modifier and Type | Method and Description |
---|---|
static Sequent |
SymbolicExecutionSideProofUtil.computeGeneralSequentToProve(Sequent goalSequent,
SequentFormula currentSF)
Computes a general
Sequent to prove in a side proof which
contains all SequentFormula of the original Sequent
except the given current SequentFormula and those which
contains modalities and queries. |
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term newSuccedent)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
boolean addResultLabel)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
PosInOccurrence pio,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
Term additionalAntecedent,
Term newSuccedent,
boolean addResultLabel)
|
static Sequent |
SymbolicExecutionUtil.createSequentToProveWithNewSuccedent(Node node,
Term additionalAntecedent,
Term newSuccedent,
ImmutableList<Term> updates,
boolean addResultLabel)
|
Sequent |
SymbolicExecutionUtil.SiteProofVariableValueInput.getSequentToProve()
Returns the sequent to prove.
|
protected static Sequent |
SymbolicExecutionUtil.labelSkolemConstants(Sequent sequent,
java.util.Set<Term> constantsToLabel,
TermFactory factory)
Labels all specified skolem equalities with the
SymbolicExecutionUtil.RESULT_LABEL . |
Modifier and Type | Method and Description |
---|---|
static Sequent |
SymbolicExecutionSideProofUtil.computeGeneralSequentToProve(Sequent goalSequent,
SequentFormula currentSF)
Computes a general
Sequent to prove in a side proof which
contains all SequentFormula of the original Sequent
except the given current SequentFormula and those which
contains modalities and queries. |
static java.util.List<Pair<Term,Node>> |
SymbolicExecutionSideProofUtil.computeResults(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
TermLabel label,
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 . |
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 ProofStarter |
SymbolicExecutionSideProofUtil.createSideProof(ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String proofName)
Creates a new
ProofStarter which contains a new site proof
of the given Proof . |
static java.util.Set<Operator> |
SymbolicExecutionSideProofUtil.extractRelevantThings(Services services,
Sequent sequentToProve)
|
static PosInOccurrence |
SymbolicExecutionUtil.findModalityWithMaxSymbolicExecutionLabelId(Sequent sequent)
Searches the modality
PosInOccurrence with the maximal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Sequent . |
static PosInOccurrence |
SymbolicExecutionUtil.findModalityWithMinSymbolicExecutionLabelId(Sequent sequent)
Searches the modality
PosInOccurrence with the minimal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Sequent . |
static boolean |
SymbolicExecutionSideProofUtil.isIrrelevantCondition(Services services,
Sequent initialSequent,
java.util.Set<Operator> relevantThingsInSequentToProve,
SequentFormula sf)
Checks if the given
SequentFormula is a relevant condition. |
protected static Sequent |
SymbolicExecutionUtil.labelSkolemConstants(Sequent sequent,
java.util.Set<Term> constantsToLabel,
TermFactory factory)
Labels all specified skolem equalities with the
SymbolicExecutionUtil.RESULT_LABEL . |
static Term |
SymbolicExecutionUtil.posInOccurrenceInOtherNode(Sequent original,
PosInOccurrence pio,
Sequent toApplyOn)
Returns the
Term described by the given PosInOccurrence of the original Sequent
in the Sequent to apply on. |
static PosInOccurrence |
SymbolicExecutionUtil.posInOccurrenceToOtherSequent(Sequent original,
PosInOccurrence pio,
Sequent toApplyTo)
Returns the
PosInOccurrence described by the given PosInOccurrence of the original Sequent
in the Sequent to apply too. |
static Term |
SymbolicExecutionUtil.replaceSkolemConstants(Sequent sequent,
Term term,
Services services)
Replaces all skolem constants in the given
Term . |
static Term |
SymbolicExecutionUtil.sequentToImplication(Sequent sequent,
Services services)
Converts the given
Sequent into an implication. |
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 . |
Constructor and Description |
---|
SiteProofVariableValueInput(Sequent sequentToProve,
Operator operator)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
TacletVisitor.visit(Sequent seq) |
Modifier and Type | Method and Description |
---|---|
Term |
ModelGenerator.sequentToTerm(Sequent s) |
Modifier and Type | Method and Description |
---|---|
static ProofStarter |
SideProofUtil.createSideProof(ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String proofName)
Creates a new
ProofStarter which contains a new site proof
of the given Proof . |
void |
ProofStarter.init(Sequent sequentToProve,
ProofEnvironment env,
java.lang.String proofName)
creates a new proof object for sequentToProve and registers it in the given environment
|
Constructor and Description |
---|
UserProvidedInput(Sequent seq,
ProofEnvironment env) |
UserProvidedInput(Sequent seq,
ProofEnvironment env,
java.lang.String proofName) |
Modifier and Type | Method and Description |
---|---|
static java.util.HashSet<LocationVariable> |
MergeRuleUtils.getLocationVariablesHashSet(Sequent sequent,
Services services)
Returns all program variables in the given sequent.
|
static boolean |
MergeRuleUtils.isProvable(Sequent toProve,
Services services,
int timeout)
Tries to prove the given formula without splitting and returns whether
the prove could be closed.
|
static boolean |
MergeRuleUtils.isProvableWithSplitting(Sequent toProve,
Services services,
int timeout)
Tries to prove the given formula with splitting and returns whether the
prove could be closed.
|
Copyright © 2003-2019 The KeY-Project.