public class TacletGenerator
extends java.lang.Object
public static TacletGenerator getInstance()
public Taclet generateAxiomTaclet(Name tacletName, Term originalAxiom, ImmutableList<ProgramVariable> programVars, KeYJavaType kjt, RuleSet ruleSet, TermServices services)
public Taclet generateRewriteTaclet(Name tacletName, Term originalFind, Term originalAxiom, ImmutableList<ProgramVariable> programVars, RuleSet ruleSet, TermServices services)
public 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)
public 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)
public 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)
public 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)
Copyright © 2003-2019 The KeY-Project.