<commit_before>/* ********************************************************************** */
/* pk_widening.c: widening  */
/* ********************************************************************** */

/* This file is part of the APRON Library, released under LGPL license.  Please
   read the COPYING file packaged in the distribution */

#include "pk_config.h"
#include "pk_vector.h"
#include "pk_bit.h"
#include "pk_satmat.h"
#include "pk_matrix.h"
#include "pk_cherni.h"
#include "pk.h"
#include "pk_representation.h"
#include "pk_user.h"
#include "pk_constructor.h"
#include "pk_test.h"

#include "mf_qsort.h"

typedef struct satmat_row_t {
  bitstring_t* p; 
    /* pointing somewhere in the field pinit of an underlying satmat_t object */
  int index;
} satmat_row_t;


static satmat_row_t* esatmat_of_satmat(satmat_t* sat)
{
  size_t i;
  satmat_row_t* tab;

  tab = malloc(sat->nbrows * sizeof(satmat_row_t));
  for (i=0; i<sat->nbrows; i++){
    tab[i].p = sat->p[i];
    tab[i].index = i;
  }
  return tab;
}

/* Row sorting.

We use here the insertion sort. 
The array tab is supposed to be of size sat->nbrows.
*/
static void esatmat_isort_rows(satmat_row_t* tab, satmat_t* sat)
{
  size_t i,j;

  for (i=1; i<sat->nbrows; i++){
    satmat_row_t row = tab[i];
    j = i;
    while (j > 0 && bitstring_cmp(tab[j-1].p, row.p, sat->nbcolumns) > 0){
      tab[j] = tab[j-1];
      j--;
    }
    tab[j] = row;
  }
}

/* Row sorting.

We use here the quick sort. */
typedef struct qsort_man_t {
  size_t size;
} qsort_man_t;
static int qsort_rows_compar(void* qsort_man, const void* p1, const void* p2)
{
  qsort_man_t* qm = (qsort_man_t*)qsort_man;
  return (bitstring_cmp( ((satmat_row_t*)p1)->p,
			 ((satmat_row_t*)p2)->p,
			 qm->size));
}

static void esatmat_sort_rows(satmat_row_t* tab, satmat_t* sat)
{
  if (sat->nbrows>=6){
    qsort_man_t qsort_man;
    qsort_man.size = sat->nbcolumns;
    qsort2(tab,
	  (size_t)sat->nbrows, sizeof(satmat_row_t),
	   qsort_rows_compar, &qsort_man);
  }
  else {
    esatmat_isort_rows(tab,sat);
  }
}

/* Membership test.

The following function tests if the given row belongs to the sorted saturation
matrix. If it is the case, it returns its rank in the saturation
matrix. Otherwise, it returns -1 */

typedef struct bsearch_man_t {
  bitstring_t* satline;
  satmat_row_t* tab;
  size_t size;
} bsearch_man_t;

static bool bsearch2(bsearch_man_t* man, size_t low, size_t high)
{
  if (high - low <= 4){
    size_t i;
    int res=-1;
    for (i=low; i<high; i++){
      int cmp = bitstring_cmp(man->tab[i].p, man->satline, man->size);
      if (cmp==0){
	res=i; break;
      }
      else if (cmp>0) break;
    }
    return res;
  }
  else {
    size_t mid = low+(high-low)/2;
    int cmp = bitstring_cmp(man->tab[mid].p,man->satline,man->size);
    if (cmp<0)
      return (bsearch2(man,mid+1,high));
    else if (cmp>0)
      return (bsearch2(man,low,mid));
    else
      return mid;
  }
}

static
int esatmat_index_in_sorted_rows(bitstring_t* satline, 
				 satmat_row_t* tab, 
				 satmat_t* sat)
{
  bsearch_man_t man;
  man.satline = satline;
  man.tab = tab;
  man.size = sat->nbcolumns;
  return bsearch2(&man,0,sat->nbrows);
}

/* This function defines the standard widening operator.  The resulting
   polyhedron has no frame matrix, unless pa is empty. */
pk_t* pk_widening(ap_manager_t* man, pk_t* pa, pk_t* pb)
{
  pk_internal_t* pk = pk_init_from_manager(man,AP_FUNID_WIDENING);
  bool widening_affine = pk->funopt->algorithm<=0;
  poly_chernikova2(man,pa,"of the first argument");
  if (pk->exn){
    pk->exn = AP_EXC_NONE;
    man->result.flag_best = man->result.flag_exact = false;
    return pk_top(man,pa->intdim,pa->realdim);
  }
  poly_chernikova2(man,pb,"of the second argument");
  if (pk->exn){
    pk->exn = AP_EXC_NONE;
    man->result.flag_best = man->result.flag_exact = false;
    return pk_top(man,pa->intdim,pa->realdim);
  }
  if (!pa->C && !pa->F) /* pa is empty */
    return pk_copy(man,pb);
  else {
    size_t sat_nbcols;
    size_t nbrows,i;
    int index;
    pk_t* po;
    bitstring_t* bitstringp;
    satmat_row_t* tab;
 
    /* copy saturation pa->satF, and sort it */
    poly_obtain_satF(pa);
    tab = esatmat_of_satmat(pa->satF);
    esatmat_sort_rows(tab,pa->satF);
    sat_nbcols = pa->satF->nbcolumns;

    po = poly_alloc(pa->intdim,pa->realdim);
<commit_msg>In widening, added assert(inclusion check).<commit_after>/* ********************************************************************** */
/* pk_widening.c: widening  */
/* ********************************************************************** */

/* This file is part of the APRON Library, released under LGPL license.  Please
   read the COPYING file packaged in the distribution */

#include "pk_config.h"
#include "pk_vector.h"
#include "pk_bit.h"
#include "pk_satmat.h"
#include "pk_matrix.h"
#include "pk_cherni.h"
#include "pk.h"
#include "pk_representation.h"
#include "pk_user.h"
#include "pk_constructor.h"
#include "pk_test.h"

#include "mf_qsort.h"

typedef struct satmat_row_t {
  bitstring_t* p; 
    /* pointing somewhere in the field pinit of an underlying satmat_t object */
  int index;
} satmat_row_t;


static satmat_row_t* esatmat_of_satmat(satmat_t* sat)
{
  size_t i;
  satmat_row_t* tab;

  tab = malloc(sat->nbrows * sizeof(satmat_row_t));
  for (i=0; i<sat->nbrows; i++){
    tab[i].p = sat->p[i];
    tab[i].index = i;
  }
  return tab;
}

/* Row sorting.

We use here the insertion sort. 
The array tab is supposed to be of size sat->nbrows.
*/
static void esatmat_isort_rows(satmat_row_t* tab, satmat_t* sat)
{
  size_t i,j;

  for (i=1; i<sat->nbrows; i++){
    satmat_row_t row = tab[i];
    j = i;
    while (j > 0 && bitstring_cmp(tab[j-1].p, row.p, sat->nbcolumns) > 0){
      tab[j] = tab[j-1];
      j--;
    }
    tab[j] = row;
  }
}

/* Row sorting.

We use here the quick sort. */
typedef struct qsort_man_t {
  size_t size;
} qsort_man_t;
static int qsort_rows_compar(void* qsort_man, const void* p1, const void* p2)
{
  qsort_man_t* qm = (qsort_man_t*)qsort_man;
  return (bitstring_cmp( ((satmat_row_t*)p1)->p,
			 ((satmat_row_t*)p2)->p,
			 qm->size));
}

static void esatmat_sort_rows(satmat_row_t* tab, satmat_t* sat)
{
  if (sat->nbrows>=6){
    qsort_man_t qsort_man;
    qsort_man.size = sat->nbcolumns;
    qsort2(tab,
	  (size_t)sat->nbrows, sizeof(satmat_row_t),
	   qsort_rows_compar, &qsort_man);
  }
  else {
    esatmat_isort_rows(tab,sat);
  }
}

/* Membership test.

The following function tests if the given row belongs to the sorted saturation
matrix. If it is the case, it returns its rank in the saturation
matrix. Otherwise, it returns -1 */

typedef struct bsearch_man_t {
  bitstring_t* satline;
  satmat_row_t* tab;
  size_t size;
} bsearch_man_t;

static bool bsearch2(bsearch_man_t* man, size_t low, size_t high)
{
  if (high - low <= 4){
    size_t i;
    int res=-1;
    for (i=low; i<high; i++){
      int cmp = bitstring_cmp(man->tab[i].p, man->satline, man->size);
      if (cmp==0){
	res=i; break;
      }
      else if (cmp>0) break;
    }
    return res;
  }
  else {
    size_t mid = low+(high-low)/2;
    int cmp = bitstring_cmp(man->tab[mid].p,man->satline,man->size);
    if (cmp<0)
      return (bsearch2(man,mid+1,high));
    else if (cmp>0)
      return (bsearch2(man,low,mid));
    else
      return mid;
  }
}

static
int esatmat_index_in_sorted_rows(bitstring_t* satline, 
				 satmat_row_t* tab, 
				 satmat_t* sat)
{
  bsearch_man_t man;
  man.satline = satline;
  man.tab = tab;
  man.size = sat->nbcolumns;
  return bsearch2(&man,0,sat->nbrows);
}

/* This function defines the standard widening operator.  The resulting
   polyhedron has no frame matrix, unless pa is empty. */
pk_t* pk_widening(ap_manager_t* man, pk_t* pa, pk_t* pb)
{
  pk_internal_t* pk = pk_init_from_manager(man,AP_FUNID_WIDENING);
  bool widening_affine = pk->funopt->algorithm<=0;
  poly_chernikova2(man,pa,"of the first argument");
  if (pk->exn){
    pk->exn = AP_EXC_NONE;
    man->result.flag_best = man->result.flag_exact = false;
    return pk_top(man,pa->intdim,pa->realdim);
  }
  poly_chernikova2(man,pb,"of the second argument");
  if (pk->exn){
    pk->exn = AP_EXC_NONE;
    man->result.flag_best = man->result.flag_exact = false;
    return pk_top(man,pa->intdim,pa->realdim);
  }
  assert(pk_is_leq(man,pa,pb));
  if (!pa->C && !pa->F) /* pa is empty */
    return pk_copy(man,pb);
  else {
    size_t sat_nbcols;
    size_t nbrows,i;
    int index;
    pk_t* po;
    bitstring_t* bitstringp;
    satmat_row_t* tab;
 
    /* copy saturation pa->satF, and sort it */
    poly_obtain_satF(pa);
    tab = esatmat_of_satmat(pa->satF);
    esatmat_sort_rows(tab,pa->satF);
    sat_nbcols = pa->satF->nbcolumns;

    po = poly_alloc(pa->intdim,pa->realdim);

{'fraction_non_alphanumeric': 0.1695859872611465, 'fraction_numerical': 0.0065969062784349405, 'mean_word_length': 3.591644908616188, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 99, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5358514', 'n_tokens_mistral': 3605, 'n_tokens_neox': 3489, 'n_words': 791}