octagon_issue.cpp

#include <iostream>
#include <opt_oct.h>

int main() {
  elina_manager_t* man = opt_oct_manager_alloc();

  elina_interval_t** itv1 = (elina_interval_t**) malloc(2 *
      sizeof(elina_interval_t*));

  itv1[0] = elina_interval_alloc();
  itv1[1] = elina_interval_alloc();
  elina_interval_set_double(itv1[0], -1.0, 1.0);
  elina_interval_set_double(itv1[1], -1.0, 1.0);

  elina_abstract0_t* z = elina_abstract0_of_box(man, 0, 2, itv1);
   
  std::cout << "Input" << std::endl;
  elina_lincons0_array_t arr = elina_abstract0_to_lincons_array(man, z);
  elina_lincons0_array_fprint(stdout, &arr, NULL);
  elina_lincons0_array_clear(&arr);
  std::cout << std::endl;

  elina_dim_t dims[2];
  elina_linexpr0_t** update = (elina_linexpr0_t**) malloc(2 * sizeof(elina_linexpr0_t*));
  dims[0] = 0;
  dims[1] = 1;
  update[0] = elina_linexpr0_alloc(ELINA_LINEXPR_SPARSE, 2);
  update[1] = elina_linexpr0_alloc(ELINA_LINEXPR_SPARSE, 2);
  // Identity
  elina_linexpr0_set_coeff_scalar_double(update[0], 0, 1.0);
  elina_linexpr0_set_coeff_scalar_double(update[0], 1, 0.0);
  elina_linexpr0_set_coeff_scalar_double(update[1], 0, 0.0);
  elina_linexpr0_set_coeff_scalar_double(update[1], 1, 1.0);
  elina_linexpr0_set_cst_scalar_double(update[0], 0.0);
  elina_linexpr0_set_cst_scalar_double(update[1], 0.0);

  std::cout << "Transformation:" << std::endl;
  elina_linexpr0_fprint(stdout, update[0], NULL);
  std::cout << std::endl;
  elina_linexpr0_fprint(stdout, update[1], NULL);
  std::cout << std::endl << std::endl;

  elina_abstract0_t* z2 = elina_abstract0_assign_linexpr_array(man, false, z, dims, update, 2, NULL);
  std::cout << "After affine transformation" << std::endl;
  arr = elina_abstract0_to_lincons_array(man, z2);
  elina_lincons0_array_fprint(stdout, &arr, NULL);
  elina_lincons0_array_clear(&arr);
  std::cout << std::endl;

  elina_abstract0_free(man, z2);
  elina_abstract0_free(man, z);
  elina_interval_free(itv1[0]);
  elina_interval_free(itv1[1]);
  free(itv1);
 
  elina_manager_free(man);
  
  return 0;
}