JuliaReach
Analyzing high-dimensional properties in low dimensions
When checking a property with BFFPSV, we implicitly assume that the property is defined in the dimensions of the analyzed blocks. We have some way to project a property up-front, but this just creates a lazy set of type LinearMap, and for those we do not have a working subset check at the moment.
https://github.com/JuliaReach/LazySets.jl/issues/1209 in LazySets is supposed to provide a concrete projection for these cases. After that is done, we should adapt our code here to use this feature.
#524 proposed a workaround, but instead we went for a partial solution in #525.
Suppose that the property is a halfspace H0 in n=48 dimensions. The we from the output of projection_map we know the variables that are being computed, say proj = [25]. Then we can create a new halfspace H in dimension m = length(proj) such that H.a = H0.a[25] and H.b = H0.b.
