Function prune

factory/variable.cc:261–289

}

void prune (Variable& alpha)
{
  if (alpha.level()==LEVELBASE) return;
  int last_var=-alpha.level();
  if ((last_var <= 0)||(var_names_ext==NULL)) return;
  int i, n = strlen( var_names_ext );
  ASSERT (n+1 >= last_var, "wrong variable");
  if (last_var == 1)
  {
    delete [] var_names_ext;
    delete [] algextensions;
    var_names_ext= 0;
    algextensions= 0;
    alpha= Variable();
    return;
  }
  char * newvarnames = new char [last_var+1];
  for ( i = 0; i < last_var; i++ )
    newvarnames[i] = var_names_ext[i];
  newvarnames[last_var] = 0;
  delete [] var_names_ext;
  var_names_ext = newvarnames;
  ext_entry * newalgext = new ext_entry [last_var];
  for ( i = 0; i < last_var; i++ )
    newalgext[i] = algextensions[i];
  delete [] algextensions;
  algextensions = newalgext;
  alpha= Variable();
}

void prune1 (const Variable& alpha)
{