| This class represents the translation rule for ProgramVariables.
A ProgramVariable is translated into a constant. If it is of Sort INT or
OBJECT, it will be translated into an SMT-LIB UninterpretedFuncTerm. If it is of
Sort BOOLEAN, it will be translated into an SMT-LIB UninterpretedPredFormula
The name of the uninterpreted function or predicate respectively is created out of the variable
name and an id unique to the ProgramVariable. It further consists of a prefix
indicating that this is a translation of an ProgramVariable and a suffix that allows to
quickly distinguish functions from predicates and integer functions from object functions
author:
akuwertz
version:
1.3, 03/28/2006 (Minor fixes) | 