| java.lang.Object de.uka.ilkd.key.logic.ldt.ADT de.uka.ilkd.key.logic.ldt.LDT de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT de.uka.ilkd.key.logic.ldt.ByteLDT
Methods inherited from de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT | public Function getArithAddition()(Code)(Java Doc) public Function getArithDivision()(Code)(Java Doc) public Function getArithJavaIntAddition()(Code)(Java Doc) public Function getArithModulo()(Code)(Java Doc) public Function getArithMultiplication()(Code)(Java Doc) public Function getArithSubstraction()(Code)(Java Doc) public Function getCharSymbol()(Code)(Java Doc) public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services serv, ExecutionContext ec)(Code)(Java Doc) public Function getGreaterOrEquals()(Code)(Java Doc) public Function getGreaterThan()(Code)(Java Doc) abstract public Function getInBoundsPredicate()(Code)(Java Doc) public Function getJDivision()(Code)(Java Doc) public Function getJModulo()(Code)(Java Doc) public Function getJavaAddInt()(Code)(Java Doc) public Function getJavaAddLong()(Code)(Java Doc) public Function getJavaBitwiseAndInt()(Code)(Java Doc) public Function getJavaBitwiseAndLong()(Code)(Java Doc) public Function getJavaBitwiseNegation()(Code)(Java Doc) public Function getJavaBitwiseOrInt()(Code)(Java Doc) public Function getJavaBitwiseOrLong()(Code)(Java Doc) public Function getJavaBitwiseXOrInt()(Code)(Java Doc) public Function getJavaBitwiseXOrLong()(Code)(Java Doc) public Function getJavaCastByte()(Code)(Java Doc) public Function getJavaCastChar()(Code)(Java Doc) public Function getJavaCastInt()(Code)(Java Doc) public Function getJavaCastLong()(Code)(Java Doc) public Function getJavaCastShort()(Code)(Java Doc) public Function getJavaDivInt()(Code)(Java Doc) public Function getJavaDivLong()(Code)(Java Doc) public Function getJavaMod()(Code)(Java Doc) public Function getJavaMulInt()(Code)(Java Doc) public Function getJavaMulLong()(Code)(Java Doc) public Function getJavaShiftLeftInt()(Code)(Java Doc) public Function getJavaShiftLeftLong()(Code)(Java Doc) public Function getJavaShiftRightInt()(Code)(Java Doc) public Function getJavaShiftRightLong()(Code)(Java Doc) public Function getJavaSubInt()(Code)(Java Doc) public Function getJavaSubLong()(Code)(Java Doc) public Function getJavaUnaryMinusInt()(Code)(Java Doc) public Function getJavaUnaryMinusLong()(Code)(Java Doc) public Function getJavaUnsignedShiftRightInt()(Code)(Java Doc) public Function getJavaUnsignedShiftRightLong()(Code)(Java Doc) public Function getLessOrEquals()(Code)(Java Doc) public Function getLessThan()(Code)(Java Doc) public Function getModuloLong()(Code)(Java Doc) public Function getNegativeNumberSign()(Code)(Java Doc) public Function getNegativeSign()(Code)(Java Doc) public Function getNumberLiteralFor(int number)(Code)(Java Doc) public Function getNumberSymbol()(Code)(Java Doc) public Function getNumberTerminator()(Code)(Java Doc) public boolean hasLiteralFunction(Function f)(Code)(Java Doc) public boolean isResponsible(Operator op, Term[] subs, Services services, ExecutionContext ec)(Code)(Java Doc) public boolean isResponsible(Operator op, Term left, Term right, Services services, ExecutionContext ec)(Code)(Java Doc) public boolean isResponsible(Operator op, Term sub, Services services, ExecutionContext ec)(Code)(Java Doc) public Term translateLiteral(Literal lit)(Code)(Java Doc) public Expression translateTerm(Term t, ExtList children)(Code)(Java Doc)
|
Methods inherited from de.uka.ilkd.key.logic.ldt.LDT | public Function addFunction(Function f)(Code)(Java Doc) public Function addFunction(Namespace funcNS, String funcName)(Code)(Java Doc) public boolean containsFunction(Function op)(Code)(Java Doc) public Namespace functions()(Code)(Java Doc) public String getFile()(Code)(Java Doc) abstract public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services serv, ExecutionContext ec)(Code)(Java Doc) public KeYJavaType getKeYJavaType(Type t)(Code)(Java Doc) abstract public boolean hasLiteralFunction(Function f)(Code)(Java Doc) abstract public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term[] subs, Services services, ExecutionContext ec)(Code)(Java Doc) abstract public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term left, Term right, Services services, ExecutionContext ec)(Code)(Java Doc) abstract public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term sub, Services services, ExecutionContext ec)(Code)(Java Doc) public Type javaType()(Code)(Java Doc) public SetOfTaclet rules()(Code)(Java Doc) public Sort targetSort()(Code)(Java Doc) public String toString()(Code)(Java Doc) abstract public Term translateLiteral(Literal lit)(Code)(Java Doc) abstract public Expression translateTerm(Term t, ExtList children)(Code)(Java Doc)
|
|
|