Implement Array-{Read-Write}-Elimination simplifications

[Robbepop]

Stevia should handle complex array expressions and thus be able to word-level simplify those together with array abstraction refinement.

To be implemented are:

1. Array-Read-Elimination: Eliminates ArrayRead expressions by replacing them with appropriate equi-satisfiable local- and root expressions.
2. Array-Write-Elimination: Eliminates ArrayWrite expressions by replacing them with appropriate equisatisfiable local- and root expressions.

Both simplifications require refinement expressions on the root scope of the input expression which can be refined by lazy insertion similar to how STP handles them via its array abstraction refinement.