Introduce intermediate symbolic proposition interface in the symbolic executor

[skeuchel]

The symbolic executor uses the inductively defined symbolic propositions directly, i.e. we have essentially the two monads □(A -> 𝕊) -> 𝕊 and □(A -> SHeap -> 𝕊) -> SHeap -> 𝕊. I think it might be good to introduce an intermediate type class interface for propositions 𝕊 and/or heap propositions SHeap -> 𝕊 that has as methods assert/assume etc, i.e. the interface of our symbolic propositions. Specifically the interfaces should encapsulate everything related to the solver and to heaps in its instances and hide it from the rest of the symbolic executor implementation. The symbolic executor would essentially already look as if it is based on separation logic symbolic propositions directly and does not do any solving itself. Making the switch to symbolic separation logic propositions later should be easy after this. There are other definitions that exhibit the same interface as symbolic propositions, see for example the heuristics for quantifier instantiation implemented in solve_evars / solve_uvars. Hooking a spatial solver into the symbolic executor should also be done in such an instance.