Array theory: implement weakly equivalent arrays

This implements Christ and Hoenicke's Weakly Equivalent Arrays
(https://arxiv.org/pdf/1405.6939.pdf) with in-place depth-first path
enumeration.

Co-authored-by: Michael Tautschnig <tautschn@amazon.com>

Author: kroening