public abstract class LDT extends java.lang.Object implements Named
Modifier and Type | Field and Description |
---|---|
private Namespace<Operator> |
functions
the namespace of functions this LDT feels responsible for
|
private Name |
name |
private Sort |
sort
the main sort associated with the LDT
|
Modifier | Constructor and Description |
---|---|
protected |
LDT(Name name,
Sort targetSort,
TermServices services) |
protected |
LDT(Name name,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
protected Function |
addFunction(Function f)
adds a function to the LDT
|
protected Function |
addFunction(TermServices services,
java.lang.String funcName)
looks up a function in the namespace and adds it to the LDT
|
protected SortDependingFunction |
addSortDependingFunction(TermServices services,
java.lang.String kind) |
boolean |
containsFunction(Function op) |
protected Namespace<Operator> |
functions()
returns the basic functions of the model
|
abstract Function |
getFunctionFor(Operator op,
Services services,
ExecutionContext ec)
returns the function symbol for the given operation
|
static java.util.Map<Name,LDT> |
getNewLDTInstances(Services s) |
abstract Type |
getType(Term t) |
abstract boolean |
hasLiteralFunction(Function f) |
abstract 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
|
abstract 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
|
abstract 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
|
Name |
name()
returns the name of this element
|
Sort |
targetSort()
Returns the sort associated with the LDT.
|
java.lang.String |
toString() |
abstract Term |
translateLiteral(Literal lit,
Services services)
translates a given literal to its logic counterpart
|
abstract Expression |
translateTerm(Term t,
ExtList children,
Services services)
Is called whenever
hasLiteralFunction() returns true. |
private final Name name
private final Sort sort
protected LDT(Name name, TermServices services)
protected LDT(Name name, Sort targetSort, TermServices services)
protected final Function addFunction(Function f)
protected final Function addFunction(TermServices services, java.lang.String funcName)
funcName
- the String with the name of the function to look upprotected final SortDependingFunction addSortDependingFunction(TermServices services, java.lang.String kind)
protected final Namespace<Operator> functions()
public final Name name()
Named
public final java.lang.String toString()
toString
in class java.lang.Object
public final Sort targetSort()
public boolean containsFunction(Function op)
public abstract boolean isResponsible(Operator op, Term[] subs, Services services, ExecutionContext ec)
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 abstract boolean isResponsible(Operator op, Term left, Term right, Services services, ExecutionContext ec)
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 abstract boolean isResponsible(Operator op, Term sub, TermServices services, ExecutionContext ec)
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 abstract Term translateLiteral(Literal lit, Services services)
lit
- the Literal to be translatedpublic abstract Function getFunctionFor(Operator op, Services services, ExecutionContext ec)
public abstract boolean hasLiteralFunction(Function f)
public abstract Expression translateTerm(Term t, ExtList children, Services services)
hasLiteralFunction()
returns true.