[PPL-devel] join-like operation

[Piotr Mardziel]

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