Add support for arrays in Yices2

[daniel-raffler]

Hello,
in this PR we add support for arrays to the Yices2 backend. Yices has supported arrays for a while, however, the implementation is a bit non-standard. Instead of the usual array operations from SMTLIB we have to use function terms:

• Const become (lambda (x::T) c) where T is the index type and c the default element
• Select becomes regular function application
• Store become function update where we "fix" the function for a single value

Array types from SMTLIB then map to (curried) function types in Yices2

There can be some confusion between UF terms and arrays as both are just function terms in Yices2. We work around issue this by explicitly keeping track of all our UF declarations in the FormulaCreator and assume all other function terms must be arrays

[kfriedberger]

The implementation looks good at first view.

Does it work with existing Yices2 bindings or do we need an update?
I saw the other PR. I am just wondering, whether we can merge this first.

[daniel-raffler]

The implementation looks good at first view.

Does it work with existing Yices2 bindings or do we need an update? I saw the other PR. I am just wondering, whether we can merge this first.

Hello Karlheinz,
thanks for the quick review! Arrays will work with the current version of Yices, so we could merge this before the update

[kfriedberger]

Can be merged

[daniel-raffler]

Thanks for merging! I think we still need to update javasmt-yices2 before the next release? However, this can be done after we've updated to yices 2.7.0