public class AssumptionGenerator extends java.lang.Object implements TacletTranslator, VariablePool
Modifier and Type | Field and Description |
---|---|
protected TacletConditions |
conditions |
private GenericTranslator |
genericTranslator |
protected java.util.Collection<TranslationListener> |
listener |
private Services |
services |
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. exchanging
schema variables for logic variables.
|
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 java.util.HashSet<GenericSort> |
collectGenerics(Term term) |
private static void |
collectGenerics(Term term,
java.util.HashSet<GenericSort> genericSorts) |
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) |
private void |
print(Term term) |
protected static Term |
quantifyTerm(Term term,
TermServices services)
Quantifies a term, i.d. every free variable is bounded by a
allquantor.
|
private Term |
rebuildTerm(Term term)
Use this method to rebuild the given term.
|
private static java.lang.StringBuffer |
removeIllegalChars(java.lang.StringBuffer template,
java.util.ArrayList<java.lang.String> toReplace,
java.util.ArrayList<java.lang.String> replacement) |
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 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 java.util.HashSet<GenericSort> collectGenerics(Term term)
private static void collectGenerics(Term term, java.util.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 java.lang.String eliminateSpecialChars(java.lang.String name)
private static java.lang.StringBuffer removeIllegalChars(java.lang.StringBuffer template, java.util.ArrayList<java.lang.String> toReplace, java.util.ArrayList<java.lang.String> replacement)
protected Term changeTerm(Term term)
rebuildTerm
.term
- the term to be changed.public void addListener(TranslationListener list)
public void removeListener(TranslationListener list)