Meet/Join with different dims?

[cwright7101]

[Help Request] Is there a way to meet/join/etc with opt_pk_array_t that have dimensions corresponding to different variables?

Say one state has dims corresponding to ["a", "b"] and the other state corresponding to ["c","d"], when doing a join I might expect ["a","b","c","d"] dimensions with corresponding constraints, instead of just the constraints joined from the two states with just 2 variables (since the dims are 0 and 1 for both of the states).

Do I need to keep track if the dim names are different and then change the linconstraints for the different dims before doing the join operation? If so, how would I do this?

[GgnDpSngh]

Hi Christopher,

Both meet/join transformers assume that the inputs have the same dimensionality. Therefore, you would need to create two 4 dimensional polyhedra by mapping "a->x0", "b->x1", "c->x2" and "d->x3". In the first polyhedron, x2 and x3 will be unconstrained while x0 and x1 will be unconstrained in the other.

Let me know if this helps!

P.S.- The join in this case will return top while the meet will return bottom.

Cheers, Gagandeep Singh

[cwright7101]

So, is there an easy way to map new dimensions? Say without having to go through each lincons/coeff and such?

The only idea I had is to do something as below (I don't have resizing of the a yet), but the last loop doesn't work because p.linterm isn't always there, it is sometimes p.coeff. How would I change this or do it differently?:

//loop through all of a, if b doesn't agree, then need to add a dimension map<string, size_t> changePolys(elina_manager_t man, opt_pk_array_t aPoly, map<string, size_t>amap, opt_pk_array_t* bPoly, map<string, size_t>bmap){ size_t sizeDim = amap.size() - 1; map<size_t,size_t> dim2dimMap{}; for (auto avardim : amap) { string avar = avardim.first; size_t adim = avardim.second; auto it = bmap.find(avar) if( it != bmap.end()) { auto bdim = it->second; if (bdim != adim){ dim2dimMap.insert(make_pair(bdim, ++sizeDim)); } } } //exists in b but not a, need to move over still for (auto bvardim : bmap) { string bvar = bvardim.first; size_t bdim = bvardim.second; auto it = bmap.find(avar) if (it == amap.end()) { bDimToDimMap = bDimToDimMap.set(bdim, ++sizeDim); } } // Then loop through the B constraints // change the dims that need to be changed auto bArray = opt_pk_to_lincons_array(man, bpoly); for (int i = 0; i < bArray.size; ++i) { auto bcons = bArray.p[i]; auto bexpr = bcons.linexpr0; auto bexprSize = bexpr->size; auto blinterms = bexpr->p.linterm; for (auto j = 0; j < bexprSize; ++j) { auto blinterm = blinterms[j]; auto dim = blinterm.dim; auto it = bDimToDimMap.find(dim); if (it != bDimToDimMap.end()) { blinterm.dim = it->second; } } }

[GgnDpSngh]

Hi Christopher,

The linear expressions in ELINA are encoded as either sparse or dense. You can check whether an expression is dense or sparse as here: https://github.com/eth-sri/ELINA/blob/fe56503116080eed0a021eae0cf427a170eaefd5/elina_zonotope/elina_box_meetjoin.c#L476

For Sparse expressions, p.linterm stores the indexes of the variables in the expression. For dense expressions,p.linterm=NULL and p.coeff[i] stores the coefficient for the variable x_i.

Let me know if this helps.

Cheers, Gagandeep Singh

[cwright7101]

So the output I get for meet is:

--------meet_test State 0-------- 2 array of constraints of size 2 0: -x0 + 2147483647 >= 0 1: x0 + 2147483647 >= 0 --------meet_test State 1-------- 2 array of constraints of size 2 0: -x1 + 2147483647 >= 0 1: x1 + 2147483647 >= 0 --------meet_test Meet State -------- 4 array of constraints of size 4 0: -x0 + 2147483647 >= 0 1: x0 + 2147483647 >= 0 2: -x1 + 2147483647 >= 0 3: x1 + 2147483647 >= 0 I was a bit confused if you meant this as the bottom from your previous comment?

If I print the lincons for the join, I get:

--------join_test State 0-------- 2 array of constraints of size 2 0: -x0 + 2147483647 >= 0 1: x0 + 2147483647 >= 0 --------join_test State 1-------- 2 array of constraints of size 2 0: -x1 + 2147483647 >= 0 1: x1 + 2147483647 >= 0 --------join_test Join State-------- 0 empty array of constraints

Just double checking these are what I should expect correct?

[GgnDpSngh]

Your output for both is correct, there was a misunderstanding on my part when I considered the meet to return bottom.

Cheers, Gagandeep Singh