public abstract class LDT extends java.lang.Object implements Named
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. |
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.Copyright © 2003-2019 The KeY-Project.