public class AssumptionGenerator extends java.lang.Object implements TacletTranslator
Modifier and Type | Field and Description |
---|---|
protected de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions |
conditions |
protected java.util.Collection<TranslationListener> |
listener |
protected java.util.HashMap<java.lang.String,LogicVariable> |
usedVariables |
Constructor and Description |
---|
AssumptionGenerator(Services services) |
Modifier and Type | Method and Description |
---|---|
void |
addListener(TranslationListener list) |
protected Term |
changeTerm(Term term)
Override this method if you want to change the term, i.e.
|
static void |
checkTable(byte[][] referenceTable,
Sort[] instTable,
Sort[] genericTable,
de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions conditions,
Services services)
Checks the referenceTable whether there are rows that are not
allowed.
|
static java.util.HashSet<GenericSort> |
collectGenerics(Term term) |
protected static java.lang.String |
eliminateSpecialChars(java.lang.String name)
eliminates all special chars.
|
static byte[][] |
generateReferenceTable(int objectCount,
int bucketCount)
Creates an array containing objectCount^bucketCount rows.
|
LogicVariable |
getInstantiationOfLogicVar(Sort instantiation,
LogicVariable lv) |
LogicVariable |
getLogicVariable(Name name,
Sort sort)
Returns a new logic variable with the given name and sort.
|
static boolean |
isAbstractOrInterface(Sort sort,
Services services) |
static boolean |
isReferenceSort(Sort sort,
Services services) |
protected static Term |
quantifyTerm(Term term,
TermServices services)
Quantifies a term, i.d.
|
void |
removeListener(TranslationListener list) |
TacletFormula |
translate(Taclet t,
ImmutableSet<Sort> sorts,
int maxGeneric) |
protected java.util.HashMap<java.lang.String,LogicVariable> usedVariables
protected java.util.Collection<TranslationListener> listener
protected de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions conditions
public AssumptionGenerator(Services services)
public TacletFormula translate(Taclet t, ImmutableSet<Sort> sorts, int maxGeneric) throws IllegalTacletException
IllegalTacletException
public LogicVariable getInstantiationOfLogicVar(Sort instantiation, LogicVariable lv)
public static java.util.HashSet<GenericSort> collectGenerics(Term term)
public static byte[][] generateReferenceTable(int objectCount, int bucketCount)
objectCount
different objects into
bucketCount
buckets.objects= 2
and bucket =3
the method
returns:objectCount
- the number of objects.bucketCount
- the number of buckets.public static void checkTable(byte[][] referenceTable, Sort[] instTable, Sort[] genericTable, de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions conditions, Services services)
protected static Term quantifyTerm(Term term, TermServices services) throws IllegalTacletException
term
- the term to be quantify.services
- TODOIllegalTacletException
public LogicVariable getLogicVariable(Name name, Sort sort)
name
- name of the logic variable.sort
- sort of the logic variable.protected static java.lang.String eliminateSpecialChars(java.lang.String name)
protected Term changeTerm(Term term)
rebuildTerm
.term
- the term to be changed.public void addListener(TranslationListener list)
public void removeListener(TranslationListener list)
Copyright © 2003-2019 The KeY-Project.