| This class represents the translation rule for AttributeOps.
Thereby the attribute represented by the AttributeOp has to be a
ProgramVariable. If this attribute is of Sort INT or OBJECT, it will be
translated into an SMT-LIB UninterpretedFuncTerm. If it is of Sort FORMULA,
it will be translated into an SMT-LIB UninterpretedPredFormula.
The name of the uninterpreted function or predicate respectively is created out of the name of
the attribute and an id unique to the AttributeOp to be translated. It further consists
of a prefix indicating that it is a translation of an AttributeOp and a suffix that
allows to quickly distinguish functions from predicates
author:
akuwertz
version:
1.5, 12/13/2006 (Minor fixes for AUFLIA support) | 