public final class MetaDiv extends AbstractTermTransformer
ADD_CAST, ARRAY_BASE_INSTANCE_OF, CONSTANT_VALUE, DIVIDE_LCR_MONOMIALS, DIVIDE_MONOMIALS, ENUM_CONSTANT_VALUE, EXPAND_QUERIES, INTRODUCE_ATPRE_DEFINITIONS, MEMBER_PV_TO_FIELD, META_ADD, META_AND, META_DIV, META_EQ, META_GEQ, META_GREATER, META_LEQ, META_LESS, META_MUL, META_OR, META_POW, META_SHIFTLEFT, META_SHIFTRIGHT, META_SUB, META_XOR, METASORT
Constructor and Description |
---|
MetaDiv() |
Modifier and Type | Method and Description |
---|---|
private boolean |
checkResult(java.math.BigInteger a,
java.math.BigInteger b,
java.math.BigInteger result)
checks whether the result is consistent with the axiom div_axiom
|
Term |
transform(Term term,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
convertToDecimalString, name2metaop
additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort
arity, bindVarsAt, isRigid, name, toString, validTopLevel, whereToBind
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
argSort, argSorts, sort
arity, bindVarsAt, isRigid, sort, validTopLevel
private boolean checkResult(java.math.BigInteger a, java.math.BigInteger b, java.math.BigInteger result)
public Term transform(Term term, SVInstantiations svInst, Services services)