Hello PPL developers;
I'm finding myself in need of a particular join-like operation but I'm having trouble finding the necessary operations in PPL to make it work. I figure that the need for this operation would be common especially when implementing inter-procedural program analyses so I'm suspicious that I'm just missing the right terminology for it. Let me explain this operation:
The setup has two polyhedra that model two sets of program variables with some variables shared but some variables not shared. For example:
polyhedron A has the constraint x ≤ y, w = 1 polyhedron B has the constraint y ≤ z, w = 2
Note that each of those two only has 3 space dimensions but the are not intended to represent the same 3 variables, hence I gave them names to distinguish them. Thus we see that y and w is shared between the two polyhedra, whereas x or z are only represented in A or B respectively.
Want I need is to join these two (thus requiring to first expand their dimensions to include all 4 dimensions) such that the result is a polyhedron C that "effectively" joins shared dimensions but preserves constraints over unshared dimensions, in this case I would like outcome C to have constraints x ≤ y ≤ z, 1 ≤ w ≤ 2 .
The problem is that to expand each input polyhedron to 4 dimensions, one either has to embed or project and then follow it up with either join or meet. The join doesn't handle the x,y,z portion of this problem correctly whereas meet doesn't handle the w portion correctly.
More technical, I need an operation over A, B to return a C with
γ(A) ⊆ { π_{x,y,w} (e) | e ∈ γ(C) } γ(B) ⊆ { π_{y,z,w} (e) | e ∈ γ(C) }
Where γ is concretization, and π_{...}(e) is a projection of a tuple e to a subset of its dimensions. Top trivially satisfies this requirement but the polyhedron {x ≤ y ≤ z, 1 ≤ w ≤ 2} also satisfies it and does so much more precisely (is minimal in terms of a concretized subset relation).
Am I missing something obvious here? Any help would be greatly appreciated.
Best, Piotr (Peter) Mardziel