de.uka.ilkd.key.taclettranslation.assumptions

Class AssumptionGenerator

java.lang.Object

de.uka.ilkd.key.taclettranslation.assumptions.AssumptionGenerator

All Implemented Interfaces:

VariablePool, TacletTranslator

public class AssumptionGenerator
extends java.lang.Object
implements TacletTranslator, VariablePool

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
AssumptionGenerator(Services services)

Method Summary

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)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

usedVariables

protected java.util.HashMap<java.lang.String,LogicVariable> usedVariables

listener

protected java.util.Collection<TranslationListener> listener

conditions

protected TacletConditions conditions

services

private Services services

genericTranslator

private GenericTranslator genericTranslator

Constructor Detail

AssumptionGenerator

public AssumptionGenerator(Services services)

Method Detail

translate

public TacletFormula translate(Taclet t,
                               ImmutableSet<Sort> sorts,
                               int maxGeneric)
                        throws IllegalTacletException

Throws:

IllegalTacletException

rebuildTerm

private Term rebuildTerm(Term term)

Use this method to rebuild the given term. The method splits the term in its single components and assemblies them. After every splitting step the method calls changeTerm. This mechanism can be used to exchange subterms.

Parameters:

term - the term to rebuild.

Returns:

returns the new term.

print

private void print(Term term)

getInstantiationOfLogicVar

public LogicVariable getInstantiationOfLogicVar(Sort instantiation,
                                                LogicVariable lv)

Specified by:

getInstantiationOfLogicVar in interface VariablePool

isAbstractOrInterface

public static boolean isAbstractOrInterface(Sort sort,
                                            Services services)

isReferenceSort

public static boolean isReferenceSort(Sort sort,
                                      Services services)

collectGenerics

public static java.util.HashSet<GenericSort> collectGenerics(Term term)

collectGenerics

private static void collectGenerics(Term term,
                                    java.util.HashSet<GenericSort> genericSorts)

generateReferenceTable

public static byte[][] generateReferenceTable(int objectCount,
                                              int bucketCount)

Creates an array containing objectCount^bucketCount rows. Each of this rows has bucketCount columns. The method enumerates all possible variations of putting objectCount different objects into bucketCount buckets.
Example
For objects= 2 and bucket =3 the method returns:
000
001
010
011
100
101
110
111

Parameters:

objectCount - the number of objects.

bucketCount - the number of buckets.

Returns:

an array of dimension objectCount^bucketCount x bucketCount

checkTable

public static void checkTable(byte[][] referenceTable,
                              Sort[] instTable,
                              Sort[] genericTable,
                              TacletConditions conditions,
                              Services services)

Checks the referenceTable whether there are rows that are not allowed. For example: the notSame-Condition is hurted.

quantifyTerm

protected static Term quantifyTerm(Term term,
                                   TermServices services)
                            throws IllegalTacletException

Quantifies a term, i.d. every free variable is bounded by a allquantor.

Parameters:

term - the term to be quantify.

services - TODO

Returns:

the quantified term.

Throws:

IllegalTacletException

getLogicVariable

public LogicVariable getLogicVariable(Name name,
                                      Sort sort)

Returns a new logic variable with the given name and sort. If already a logic variable exists with the same name and sort this variable is returned instead of a new logic variable.

Specified by:

getLogicVariable in interface VariablePool

Parameters:

name - name of the logic variable.

sort - sort of the logic variable.

Returns:

logic variable with the given name and sort.

eliminateSpecialChars

protected static java.lang.String eliminateSpecialChars(java.lang.String name)

eliminates all special chars.

removeIllegalChars

private static java.lang.StringBuffer removeIllegalChars(java.lang.StringBuffer template,
                                                         java.util.ArrayList<java.lang.String> toReplace,
                                                         java.util.ArrayList<java.lang.String> replacement)

changeTerm

protected Term changeTerm(Term term)

Override this method if you want to change the term, i.e. exchanging schema variables for logic variables. See rebuildTerm.

Parameters:

term - the term to be changed.

Returns:

the new term.

addListener

public void addListener(TranslationListener list)

removeListener

public void removeListener(TranslationListener list)