| This class represents the translation rule for ArrayOps.
Thereby the array access represented by the ArrayOp is translated into an SMT-LIB
UninterpretedFuncTerm, if the array is of Sort INT or OBJECT. If it is of
boolean Sort, it is translated into an SMT-LIB UninterpretedPredFormula.
The created functions or predicates consist of two arguments: their first argument represents the
accessed array itself, and the second argument specifies the index to be accessed
author:
akuwertz
version:
1.3, 12/13/2006 (Minor fixes for AUFLIA support) |
