[FEATURE] Add Apalache IR operators for SMT select and store

[rodrigo7491]

The original SMT encoding has the notion of an "in-relation", which underpins how sets are encoded using uninterpreted constants. Keeping this notion while using SMT arrays is counterproductive, since it encompasses both access, select, and update, store, operators. The goal is to add new IR operators to clearly indicate where select and store should be used. See #1093 for a discussion.