Modifier and Type | Field and Description |
---|---|
private Function |
clContains |
private Function |
clEndsWith |
private Function |
clHashCode |
private Function |
clIndexOfChar |
private Function |
clIndexOfCl |
private Function |
clLastIndexOfChar |
private Function |
clLastIndexOfCl |
private Function |
clRemoveZeros |
private Function |
clReplace |
private Function |
clStartsWith |
private Function |
clTranslateInt |
static Name |
NAME |
static Name |
STRINGCONTENT_NAME |
static Name |
STRINGPOOL_NAME |
Constructor and Description |
---|
CharListLDT(TermServices services) |
Modifier and Type | Method and Description |
---|---|
Function |
getClContains() |
Function |
getClEndsWith() |
Function |
getClHashCode() |
Function |
getClIndexOfChar() |
Function |
getClIndexOfCl() |
Function |
getClLastIndexOfChar() |
Function |
getClLastIndexOfCl() |
Function |
getClRemoveZeros() |
Function |
getClReplace() |
Function |
getClStartsWith() |
Function |
getClTranslateInt() |
Function |
getFunctionFor(Operator op,
Services serv,
ExecutionContext ec)
returns the function symbol for the given operation
|
Type |
getType(Term t) |
boolean |
hasLiteralFunction(Function f) |
boolean |
isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given java
operator and the logic subterms
|
boolean |
isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
unary java operator and the logic subterms
|
boolean |
isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
binary java operator and the logic subterms
|
private java.lang.StringBuffer |
printlastfirst(Term t) |
private java.lang.String |
translateCharTerm(Term t) |
Term |
translateLiteral(Literal lit,
Services services)
translates a given literal to its logic counterpart
|
Expression |
translateTerm(Term t,
ExtList children,
Services services)
Is called whenever
hasLiteralFunction() returns true. |
addFunction, addFunction, addSortDependingFunction, containsFunction, functions, getNewLDTInstances, name, targetSort, toString
public static final Name NAME
public static final Name STRINGPOOL_NAME
public static final Name STRINGCONTENT_NAME
private final Function clIndexOfChar
private final Function clIndexOfCl
private final Function clLastIndexOfChar
private final Function clLastIndexOfCl
private final Function clReplace
private final Function clTranslateInt
private final Function clRemoveZeros
private final Function clHashCode
private final Function clStartsWith
private final Function clEndsWith
private final Function clContains
public CharListLDT(TermServices services)
private java.lang.String translateCharTerm(Term t)
private java.lang.StringBuffer printlastfirst(Term t)
public Function getClIndexOfChar()
public Function getClIndexOfCl()
public Function getClLastIndexOfChar()
public Function getClLastIndexOfCl()
public Function getClReplace()
public Function getClTranslateInt()
public Function getClRemoveZeros()
public Function getClHashCode()
public Function getClStartsWith()
public Function getClEndsWith()
public Function getClContains()
public boolean isResponsible(Operator op, Term[] subs, Services services, ExecutionContext ec)
LDT
isResponsible
in class LDT
op
- the de.uka.ilkd.key.java.expression.Operator to
translatesubs
- the logic subterms of the java operatorservices
- the Servicesec
- the ExecutionContext in which the expression is evaluatedpublic boolean isResponsible(Operator op, Term left, Term right, Services services, ExecutionContext ec)
LDT
isResponsible
in class LDT
op
- the de.uka.ilkd.key.java.expression.Operator to
translateleft
- the left subterm of the java operatorright
- the right subterm of the java operatorservices
- the Servicesec
- the ExecutionContext in which the expression is evaluatedpublic boolean isResponsible(Operator op, Term sub, TermServices services, ExecutionContext ec)
LDT
isResponsible
in class LDT
op
- the de.uka.ilkd.key.java.expression.Operator to
translatesub
- the logic subterms of the java operatorservices
- the Servicesec
- the ExecutionContext in which the expression is evaluatedpublic Term translateLiteral(Literal lit, Services services)
LDT
translateLiteral
in class LDT
lit
- the Literal to be translatedpublic Function getFunctionFor(Operator op, Services serv, ExecutionContext ec)
LDT
getFunctionFor
in class LDT
public boolean hasLiteralFunction(Function f)
hasLiteralFunction
in class LDT
public Expression translateTerm(Term t, ExtList children, Services services)
LDT
hasLiteralFunction()
returns true.translateTerm
in class LDT