All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
private TacletGoalTemplate |
createAxiomGoalTemplate(Term goalTerm) |
private OpReplacer |
createOpReplacer(ImmutableList<ProgramVariable> programVars,
ImmutableList<SchemaVariable> schemaVars,
TermServices services) |
private TacletGenerator.TermAndBoundVarPair |
createSchemaTerm(Term term,
ImmutableList<ProgramVariable> programVars,
ImmutableList<SchemaVariable> schemaVars,
TermServices services) |
private TacletGenerator.TermAndBoundVarPair |
createSchemaTerm(Term term,
TermServices services,
Pair<ProgramVariable,SchemaVariable>... varPairs) |
private SchemaVariable |
createSchemaVariable(ProgramVariable programVar) |
private ImmutableList<SchemaVariable> |
createSchemaVariables(ImmutableList<ProgramVariable> programVars) |
private void |
functionalRepresentsAddSatisfiabilityBranch(IObserverFunction target,
TermServices services,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
ImmutableList<SchemaVariable> paramSVs,
TacletGenerator.TermAndBoundVarPair schemaRepresents,
RewriteTacletBuilder<? extends RewriteTaclet> tacletBuilder) |
private Term |
functionalRepresentsSatisfiability(IObserverFunction target,
TermServices services,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
ImmutableList<SchemaVariable> paramSVs,
TacletGenerator.TermAndBoundVarPair schemaRepresents,
RewriteTacletBuilder<? extends RewriteTaclet> tacletBuilder) |
Taclet |
generateAxiomTaclet(Name tacletName,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
KeYJavaType kjt,
RuleSet ruleSet,
TermServices services)
Returns a no-find taclet to the passed axiom.
|
ImmutableSet<Taclet> |
generateContractAxiomTaclets(Name name,
Term originalPre,
Term originalPost,
Term originalMby,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> originalParamVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiabilityGuard,
TermServices services) |
ImmutableSet<Taclet> |
generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
private SequentFormula |
generateGuard(KeYJavaType kjt,
IObserverFunction target,
TermServices services,
SchemaVariable selfSV,
java.util.List<SchemaVariable> heapSVs,
ImmutableList<SchemaVariable> paramSVs,
Term schemaAxiom,
RewriteTacletBuilder<? extends RewriteTaclet> tacletBuilder,
boolean addGuard) |
private ImmutableSet<Taclet> |
generateModelMethodExecutionTaclets(Name name,
KeYJavaType kjt,
IObserverFunction target,
Services services) |
ImmutableSet<Taclet> |
generatePartialInvTaclet(Name name,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
SchemaVariable eqSV,
Term term,
KeYJavaType kjt,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean isStatic,
boolean eqVersion,
Services services) |
Taclet |
generateRelationalRepresentsTaclet(Name tacletName,
Term originalAxiom,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
boolean satisfiabilityGuard,
TermServices services) |
Taclet |
generateRewriteTaclet(Name tacletName,
Term originalFind,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
RuleSet ruleSet,
TermServices services) |
static TacletGenerator |
getInstance() |
private Pair<Term,ImmutableSet<Taclet>> |
limitTerm(Term t,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
private Term |
prepareExactInstanceGuard(KeYJavaType kjt,
IObserverFunction target,
TermServices services,
SchemaVariable selfSV) |
private Term |
prepareSatisfiabilityGuard(IObserverFunction target,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
ImmutableList<SchemaVariable> paramSVs,
Term schemaAxiom,
RewriteTacletBuilder<? extends RewriteTaclet> tacletBuilder,
TermServices services) |
private TacletGenerator.TermAndBoundVarPair |
replaceBoundLogicVars(Term t,
TermServices services)
Replaces any bound logical variables in t with schema variables
(necessary for proof saving/loading, if t occurs as part of a taclet).
|
private TacletGenerator.TermAndBoundVarPair |
replaceBoundLVsWithSVsHelper(Term t,
TermServices services) |