Meet/Join with different dims?

[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?

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

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;
      }
    }
  }

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:

ELINA/elina_zonotope/elina_box_meetjoin.c

Line 476 in fe56503

if(expr->discr==ELINA_LINEXPR_SPARSE){

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

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?

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

Cheers,
Gagandeep Singh