public class AssumptionGenerator extends Object implements TacletTranslator, VariablePool
Modifier and Type | Field and Description |
---|---|
protected TacletConditions |
conditions |
private GenericTranslator |
genericTranslator |
protected Collection<TranslationListener> |
listener |
private Services |
services |
protected HashMap<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,
TacletConditions conditions,
Services services)
Checks the referenceTable whether there are rows that are not
allowed.
|
static HashSet<GenericSort> |
collectGenerics(Term term) |
private static void |
collectGenerics(Term term,
HashSet<GenericSort> genericSorts) |
protected static String |
eliminateSpecialChars(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) |
private void |
print(Term term) |
protected static Term |
quantifyTerm(Term term,
TermServices services)
Quantifies a term, i.d.
|
private Term |
rebuildTerm(Term term)
Use this method to rebuild the given term.
|
private static StringBuffer |
removeIllegalChars(StringBuffer template,
ArrayList<String> toReplace,
ArrayList<String> replacement) |
void |
removeListener(TranslationListener list) |
TacletFormula |
translate(Taclet t,
ImmutableSet<Sort> sorts,
int maxGeneric) |
protected HashMap<String,LogicVariable> usedVariables
protected Collection<TranslationListener> listener
protected TacletConditions conditions
private Services services
private GenericTranslator genericTranslator
public AssumptionGenerator(Services services)
public TacletFormula translate(Taclet t, ImmutableSet<Sort> sorts, int maxGeneric) throws IllegalTacletException
IllegalTacletException
private Term rebuildTerm(Term term)
changeTerm
. This mechanism can be
used to exchange subterms.term
- the term to rebuild.private void print(Term term)
public LogicVariable getInstantiationOfLogicVar(Sort instantiation, LogicVariable lv)
getInstantiationOfLogicVar
in interface VariablePool
public static HashSet<GenericSort> collectGenerics(Term term)
private static void collectGenerics(Term term, HashSet<GenericSort> genericSorts)
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, 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)
getLogicVariable
in interface VariablePool
name
- name of the logic variable.sort
- sort of the logic variable.protected static String eliminateSpecialChars(String name)
private static StringBuffer removeIllegalChars(StringBuffer template, ArrayList<String> toReplace, ArrayList<String> replacement)
protected Term changeTerm(Term term)
rebuildTerm
.term
- the term to be changed.public void addListener(TranslationListener list)
public void removeListener(TranslationListener list)