/**CFile***********************************************************************

  FileName    [smtUtil.c]

  PackageName [smt]

  Synopsis    [Routines for smt function.]

  Author      [Hyondeuk Kim]

  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]

******************************************************************************/

#ifdef HAVE_LIBGMP

#include "smt.h"

static jmp_buf timeout_env;
static int cusp_timeout;	
static long alarm_lap_time;

smtCls_t *
smt_create_clause(void)
{
  smtCls_t * cls = (smtCls_t *) malloc(sizeof(smtCls_t));

  cls->litArr = sat_array_alloc(8);

  return cls;
}

smtCls_t *
smt_duplicate_clause(smtCls_t * cls)
{
  smtCls_t * new_cls;
  int i, lit;

  new_cls = smt_create_clause();
  
  for(i = 0; i < cls->litArr->size; i++) {
    lit = cls->litArr->space[i];
    new_cls->litArr = sat_array_insert(new_cls->litArr, (long) lit);
  }

  return new_cls;
}

smtFmlType_t
smt_get_ar_symbol(char * str)
{
  smtFmlType_t type;

  if ( ! strcmp(str, "=") )
    type = EQ_c;
  else if ( ! strcmp(str, "<") )
    type = LT_c;
  else if ( ! strcmp(str, ">") )
    type = GT_c;
  else if ( ! strcmp(str, "<=") )
    type = LE_c;
  else if ( ! strcmp(str, ">=") )
    type = GE_c;
  else if ( ! strcmp(str, "+") )
    type = ADD_c;
  else if ( ! strcmp(str, "-") )
    type = SUB_c;
  else if ( ! strcmp(str, "*") )
    type = MUL_c;
  else if ( ! strcmp(str, "~") )
    type = MINUS_c;
  else if ( ! strcmp(str, "/") )
    type = DIV_c;
  else {
#ifndef DISABLE_STATISTICS
    fprintf(stdout, "ERROR: Wrong type: %s\n", str);
#endif
    fprintf(stdout, "unknown\n");
    exit(0);
  }

  return type;
}

smtBvar_t *
smt_create_bool_variable(char * name, smtFml_t * bvfml)
{
  smtBvar_t * bvar = (smtBvar_t *) malloc(sizeof(smtBvar_t));

  if (name) 
    bvar->name = name;
  else
    bvar->name = 0;

  if (bvfml) {
    if (!bvar->name)
      bvar->name = smt_convert_fml_to_string(bvfml);

    bvfml->bvar = bvar;
  }
  
  bvar->id = 0;
  bvar->flag = 0;
  bvar->aig_node = 0;

  return bvar;
}

smtBvar_t *
smt_create_intermediate_bool_variable(smtManager_t * sm, AigEdge_t node)
{
  Aig_Manager_t * bm = sm->bm;
  smtBvar_t * bvar;
  nameType_t * node_name;
  int var_id;

  sm->num_var++;
  var_id = sm->num_var; 

  /* bool var */
  node_name = Aig_NodeReadName(bm, node);
  bvar = smt_create_bool_variable(0,0);
  bvar->name = util_strcat3("AIG_", node_name, "");
  bvar->id = var_id;
  sm->bvarArr = sat_array_insert(sm->bvarArr, (long) bvar);
  sm->id2var = sat_array_insert(sm->id2var, (long) bvar);
  assert(bvar->id == sm->id2var->size-1);

  return bvar;
}

smtNvar_t *
smt_create_numerical_variable(char * name, smtFml_t * nvfml)
{
  smtNvar_t * nvar = (smtNvar_t *) malloc(sizeof(smtNvar_t));

  if (name) 
    nvar->name = name;
  else
    nvar->name = 0;

  if (nvfml) {
    if (!nvar->name)
      nvar->name = smt_convert_fml_to_string(nvfml);

    nvfml->nvar = nvar;
  }
    
  nvar->id = 0;
  nvar->flag = 0;
  nvar->avarArr = 0;

  return nvar;
}

void
smt_create_dl_atom_variable_main(smtManager_t * sm)
{
  smtFml_t * avfml;
  smtAvar_t * avar, * tavar;
  smtNvar_t * nvar, * lnvar, * rnvar;
  st_table * avar_table;
  int id = 1, size = 0;
  int i, j;
  
  sm->avarArr = sat_array_alloc(sm->avfmlArr->size);
  sm->id2var = sat_array_alloc(sm->avarArr->size + sm->bvarArr->size + 1);
  sm->id2var = sat_array_insert(sm->id2var, 0); /* elem starts from idx one */

  if (sm->nvarArr->size) 
    size = 3 * (sm->avfmlArr->size / sm->nvarArr->size + 1);
  
  avar_table = st_init_table(strcmp, st_strhash);
  
  for(i = 0; i < sm->avfmlArr->size; i++) {
    avfml = (smtFml_t *) sm->avfmlArr->space[i];
    avar = smt_create_atom_variable(avfml);

    if ( !(sm->flag & MP_CONST_MASK) ) {
      lnvar = (smtNvar_t *) avar->nvars->space[0];
      rnvar = (smtNvar_t *) avar->nvars->space[1];
      
      if (lnvar == rnvar) { /* bool */
	smt_convert_dl_atom_fml_to_bool_fml(avfml, avar);
	smt_free_atom_members(avar);
	free(avar);
	continue;
      }
    }

    if (st_lookup(avar_table, avar->name, (char **)&(tavar))) { 
      avfml->avar = tavar;
      smt_free_atom_members(avar);
      free(avar);
    } else {
      avfml->avar = avar;
      avar->id = id;
      id++;
      sm->avarArr = sat_array_insert(sm->avarArr, (long) avar);
      st_insert(avar_table, avar->name, (char *) avar); 
      sm->id2var = sat_array_insert(sm->id2var, (long) avar);

      /* generate adjacent avar array */
      for(j = 0; j < avar->nvars->size; j++) {
	nvar = (smtNvar_t *) avar->nvars->space[j];
	if (!nvar->avarArr) nvar->avarArr = sat_array_alloc(size);
	nvar->avarArr = sat_array_insert(nvar->avarArr, (long) avar);
      }

      if (avar->type == EQ_c) {
	if (avar->constant >= 0.0 && avar->constant <= 0.0) 
	  sm->stats->num_eq++;
	else
	  sm->stats->num_ceq++;
      } else {
	sm->stats->num_ineq++;
      }
    }
  }

  st_free_table(avar_table);
}

void
smt_convert_dl_atom_fml_to_bool_fml(smtFml_t * fml, smtAvar_t * avar)
{
  /* atoms are in the form of x - x <= w */

  fml->type = PRED_c;

  if (avar->type == LE_c) {
    if (avar->constant >= 0)
      fml->flag |= TRUE_MASK;
    else 
      fml->flag |= FALSE_MASK;
  } else if (avar->type == LT_c) {
    if (avar->constant > 0)
      fml->flag |= TRUE_MASK;
    else 
      fml->flag |= FALSE_MASK;
  } else if (avar->type == GE_c) {
    if (avar->constant <= 0)
      fml->flag |= TRUE_MASK;
    else 
      fml->flag |= FALSE_MASK;
  } else if (avar->type == GT_c) {
    if (avar->constant < 0)
      fml->flag |= TRUE_MASK;
    else 
      fml->flag |= FALSE_MASK;
  }
    
  return;
}

int
smt_convert_atom_to_leq_form(smtManager_t * sm, smtAvar_t * avar)
{
  smtNvar_t * nvar_a, * nvar_b;
  double * coeffs;
  double coeff, coeff_a, coeff_b;
  int j, k;
  
  /* atom is converted into (nvars <= constant) form */

  coeffs = (double *) malloc(sizeof(double) * (sm->nvarArr->size + 1));
  memset(coeffs, 0, sizeof(double) * (sm->nvarArr->size + 1));
    
  /* check redundant nvar in avar */
  for(j = 0; j < avar->nvars->size-1; j++) {
    nvar_a = (smtNvar_t *) avar->nvars->space[j];
    
    for(k = j+1; k < avar->nvars->size; k++) {
      nvar_b = (smtNvar_t *) avar->nvars->space[k];
      if (nvar_a != nvar_b) continue;
      coeff_a = array_fetch(double, avar->coeffs, j);
      coeff_b = array_fetch(double, avar->coeffs, k);
      coeff_a = coeff_a + coeff_b;
      array_insert(double, avar->coeffs, j, coeff_a);
      array_insert(double, avar->coeffs, k, 0);
    }
  }

  for(j = 0, k = 0; j < avar->coeffs->num; j++) {
    coeff = array_fetch(double, avar->coeffs, j);
    nvar_a = (smtNvar_t *) avar->nvars->space[j];
    
    if (coeff <= 0 && coeff >= 0) { /* redundant nvar exists */
      continue;
    }
    
    if (avar->type == GE_c || avar->type == GT_c) {
      coeff = -coeff;
      array_insert(double, avar->coeffs, k, coeff);
    } else {
      array_insert(double, avar->coeffs, k, coeff);
    }

    coeffs[nvar_a->id] = coeff;

    if (j != k) { /* redundant nvar exists */
      avar->nvars->space[k] = (long) nvar_a;
    }
    
    k++;
  }
  
  if (j != k) { /* redundant nvar exists */
    avar->coeffs->num = k;
    avar->nvars->size = k;
  }
  
  if (avar->type == GE_c) 
    avar->constant = -avar->constant;
  else if (avar->type == LT_c) 
    avar->constant = avar->constant - sm->epsilon;     
  else if (avar->type == GT_c) 
    avar->constant = -avar->constant - sm->epsilon;
  
  if (k == 0) { /* avar -> bool */
    if (avar->constant >= 0) 
      return 1; /* true */
    else
      return 0; /* false */
  }

  if (k > 1) { /* sort nvar in avar->nvars for upcoming tableau gen */
    smt_sort_nvar_array_with_id(avar->nvars);
    for(j = 0; j < avar->coeffs->num; j++) {
      nvar_a = (smtNvar_t *) avar->nvars->space[j];
      coeff = coeffs[nvar_a->id];
      array_insert(double, avar->coeffs, j, coeff);
    }
  }

  return 2;
}

char *
smt_get_avar_name(smtManager_t * sm, smtAvar_t * avar)
{
  smtNvar_t * nvar, * lnvar, * rnvar;
  double coeff;
  char * str_a, * str_b, * str_c, * str_d, * avar_name;
  int i;

  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) {
    for(i = 0, lnvar = 0, rnvar = 0; i < avar->nvars->size; i++) {
      coeff = array_fetch(double, avar->coeffs, i);
      nvar = (smtNvar_t *) avar->nvars->space[i];
      if (coeff > 0) lnvar = nvar;
      else if (coeff < 0) rnvar = nvar;
      else exit(0);
    }

    assert(lnvar);
    assert(rnvar);

    str_a = (char *) malloc(sizeof(char) * 10);
    str_b = (char *) malloc(sizeof(char) * 10);
    str_c = (char *) malloc(sizeof(char) * 10);
    str_d = (char *) malloc(sizeof(char) * 10);

    sprintf(str_a, "%p", lnvar);
    sprintf(str_b, "%p", rnvar);
    sprintf(str_c, "%d", (int) avar->type);
    str_d = util_strcat3(str_a, str_b, str_c);
    sprintf(str_c, "%g", avar->constant);
    avar_name = util_strcat3(str_d, str_c, "");
    free(str_a);
    free(str_b);
    free(str_c);
    free(str_d);

  } else if (sm->flag & LIA_MASK) {
    /* later */
    avar_name = avar->name;
  } else
    avar_name = 0;

  return avar_name;
}

char *
smt_get_neg_avar_name(smtManager_t * sm, smtAvar_t * avar)
{
  smtNvar_t * nvar, * lnvar, * rnvar;
  double coeff;
  char * str_a, * str_b, * str_c, * str_d, * avar_name = 0;
  int i;

  if (sm->flag & IDL_MASK || sm->flag & RDL_MASK) {
    for(i = 0, lnvar = 0, rnvar = 0; i < avar->nvars->size; i++) {
      coeff = array_fetch(double, avar->coeffs, i);
      nvar = (smtNvar_t *) avar->nvars->space[i];
      if (coeff > 0) lnvar = nvar;
      else if (coeff < 0) rnvar = nvar;
      else exit(0);
    }

    assert(lnvar);
    assert(rnvar);

    str_a = (char *) malloc(sizeof(char) * 10);
    str_b = (char *) malloc(sizeof(char) * 10);
    str_c = (char *) malloc(sizeof(char) * 10);
    str_d = (char *) malloc(sizeof(char) * 10);
    
    sprintf(str_a, "%p", lnvar);
    sprintf(str_b, "%p", rnvar);

    if (avar->type == LE_c) 
      sprintf(str_c, "%d", GT_c);
    else if (avar->type == LT_c) 
      sprintf(str_c, "%d", GE_c);
    else if (avar->type == GE_c) 
      sprintf(str_c, "%d", LT_c);
    else if (avar->type == GT_c) 
      sprintf(str_c, "%d", LE_c);

    str_d = util_strcat3(str_a, str_b, str_c);
    sprintf(str_c, "%d", (int) avar->constant);
    avar_name = util_strcat3(str_d, str_c, "");
    free(str_a);
    free(str_b);
    free(str_c);
    free(str_d);

  } else if (sm->flag & LIA_MASK) {
    /* later */
    avar_name = avar->name;
  }

  return avar_name;
}

smtAvar_t *
smt_create_atom_variable(smtFml_t * avfml)
{
  smtAvar_t * avar = (smtAvar_t *) malloc(sizeof(smtAvar_t));

  avar->name = smt_convert_fml_to_string(avfml);
  avar->id = 0;
  avar->flag = 0;
  avar->type = avfml->type;
  avar->nvars = sat_array_alloc(4);
  avar->coeffs = array_alloc(double, 4);
  avar->sis_avars = 0;
  avar->constant = 0;

  smt_gather_atom_member(avar, avfml);

  if (avar->nvars->size == 1)
    avar->flag |= BOUND_MASK;
  else if ( !(avar->flag & LA_MASK) )
    avar->flag |= UNIT_LA_MASK;
    
  avar->aig_node = Aig_NULL;
  
  return avar;  
}

smtAvar_t *
smt_create_pure_atom_variable(void)
{
  smtAvar_t * avar = (smtAvar_t *) malloc(sizeof(smtAvar_t));

  avar->name = 0;
  avar->id = 0;
  avar->flag = 0;
  avar->coeffs = array_alloc(double, 4);
  avar->nvars = sat_array_alloc(4);
  avar->constant = 0;
  avar->aig_node = Aig_NULL;
  
  return avar;  
}

void
smt_init_atom_variable_values(smtManager_t * sm)
{
  int i, size;

  if (!sm->avarArr) return;

  size = sm->avarArr->size + 1;

  sm->avalues = (int *) malloc(sizeof(int) * size);

  for(i = 0; i < size; i++) {
    sm->avalues[i] = 2;
  }
}

void
smt_assign_boolean_variable_id(smtManager_t * sm)
{
  smtBvar_t * bvar;
  int id;
  int i;
  
  if (sm->avarArr)
    id = sm->avarArr->size + 1;
  else
    id = 1;

  for(i = 0; i < sm->bvarArr->size; i++) {
    bvar = (smtBvar_t *) sm->bvarArr->space[i];
    bvar->id = id;
    id++;
    sm->id2var = sat_array_insert(sm->id2var, (long) bvar);
  }  
}

void
smt_assign_numerical_variable_id(smtManager_t * sm)
{
  smtNvar_t * nvar;
  int i;
  
  for(i = 0; i < sm->nvarArr->size; i++) {
    nvar = (smtNvar_t *) sm->nvarArr->space[i];
    nvar->id = i + 1;
  }  
}

void
smt_assign_numerical_variable_id_in_array(satArray_t * nvarArr)
{
  smtNvar_t * nvar;
  int i;
  
  for(i = 0; i < nvarArr->size; i++) {
    nvar = (smtNvar_t *) nvarArr->space[i];
    nvar->id = i + 1;
  }  
}

void
smt_gather_atom_member(smtAvar_t * avar, smtFml_t * avfml)
{
  smtFml_t * lfml, * rfml;
  double coeff;
  int nminus;

  lfml = (smtFml_t *) avfml->subfmlArr->space[0];
  rfml = (smtFml_t *) avfml->subfmlArr->space[1];

  nminus = 0;
  coeff = 1;

  smt_gather_atom_member_in_fml(avar, lfml, nminus, coeff);
  
  nminus = 1;
  coeff = 1;

  smt_gather_atom_member_in_fml(avar, rfml, nminus, coeff);
}

void
smt_gather_atom_member_in_fml(
  smtAvar_t * avar,
  smtFml_t * fml,
  int nminus,
  double coeff)
{
  smtFml_t * lfml, * rfml, * tfml;
  char * str_a, * str_b;
  double value = 0, tcoeff = 0;
  int i;

  if (fml->type == FUN_c) {
    if (nminus%2 == 1)
      tcoeff = -coeff; 
    else if (nminus%2 == 0)
      tcoeff = coeff;

    array_insert_last(double, avar->coeffs, tcoeff);
    avar->nvars = sat_array_insert(avar->nvars, (long) fml->nvar);
    if (tcoeff > 1 || tcoeff < -1) 
      avar->flag |= LA_MASK;
    
  } else if (fml->type == NUM_c) {
    if(nminus%2 == 1)
      value = coeff * (double) fml->value;
    else
      value = -coeff * (double) fml->value;
    
    (avar->constant)+=(double) value;
    
  } else if (fml->type == MINUS_c) {
    nminus++;
    tfml = (smtFml_t *) fml->subfmlArr->space[0];
    smt_gather_atom_member_in_fml(avar, tfml, nminus, coeff);
    
  } else if (fml->type == SUB_c) {
    lfml = (smtFml_t *) fml->subfmlArr->space[0];
    rfml = (smtFml_t *) fml->subfmlArr->space[1];
    
    smt_gather_atom_member_in_fml(avar, lfml, nminus, coeff);
    smt_gather_atom_member_in_fml(avar, rfml, nminus + 1, coeff);

  } else if (fml->type == ADD_c) {
    for(i = 0; i < fml->subfmlArr->size; i++) {
      tfml = (smtFml_t *) fml->subfmlArr->space[i];
      smt_gather_atom_member_in_fml(avar, tfml, nminus, coeff);
    }
    
  } else if (fml->type == MUL_c) {
    lfml = (smtFml_t *) fml->subfmlArr->space[0];
    rfml = (smtFml_t *) fml->subfmlArr->space[1];

    if (lfml->type == NUM_c && rfml->type != NUM_c) {
      /** ex: 3 * (a + b + 2) **/
      tcoeff = coeff * (double) lfml->value;
      smt_gather_atom_member_in_fml(avar, rfml, nminus, tcoeff);

    } else if (lfml->type != NUM_c && rfml->type == NUM_c) {
      /** ex: (a + b + 2) * 3 **/
      tcoeff = coeff * (double) rfml->value;
      smt_gather_atom_member_in_fml(avar, lfml, nminus, tcoeff);
      
    } else if (lfml->type == MINUS_c && rfml->type != NUM_c) {
      /** ex: -3 * (a + b + 2) **/
      nminus++;
      tfml = (smtFml_t *) lfml->subfmlArr->space[0];
      tcoeff = coeff * (double) tfml->value;
      smt_gather_atom_member_in_fml(avar, rfml, nminus, tcoeff);

    } else if (lfml->type != NUM_c && rfml->type == MINUS_c) {
      /** ex: (a + b + 2) * -3 **/
      nminus++;
      tfml = (smtFml_t *) rfml->subfmlArr->space[0];
      tcoeff = coeff * (double) tfml->value;
      smt_gather_atom_member_in_fml(avar, lfml, nminus, tcoeff);
      
    } else if (lfml->type == NUM_c && rfml->type == NUM_c) {
      /** ex: 2 * 3 **/
      value = lfml->value * rfml->value;
	
      if(nminus%2 == 1)
	value = coeff * value;
      else
	value = -coeff * value;
      
      (avar->constant)+= value;
      
    } else if (lfml->type == FUN_c && rfml->type == FUN_c) {
      fprintf(stdout, "%s * %s: WRONG LINEAR ARITHMETIC ATOM TYPE\n", 
	      lfml->nvar->name, rfml->nvar->name);
      fprintf(stdout, "unknown\n");
      exit(0);
    } else { 
      fprintf(stdout, "ERROR: WRONG LINEAR ARITHMETIC ATOM TYPE\n");
      str_a = smt_convert_fml_to_string(lfml);
      str_b = smt_convert_fml_to_string(rfml);
      fprintf(stdout, "fml = %s * %s\n", str_a, str_b);
      fprintf(stdout, "unknown\n");
      exit(0);
    }

  } else if (fml->type == DIV_c) {
    lfml = (smtFml_t *) fml->subfmlArr->space[0];
    rfml = (smtFml_t *) fml->subfmlArr->space[1];
    
    if (lfml->type == NUM_c && rfml->type == NUM_c) {
      if (rfml->value != 0)
        value = lfml->value / rfml->value;
      
      if(nminus%2 == 1)
	value = coeff * value;
      else
	value = -coeff * value;
      
      (avar->constant)+= value;      
      
    } else { 
      fprintf(stdout, "ERROR: WRONG LINEAR ARITHMETIC ATOM TYPE\n");
      str_a = smt_convert_fml_to_string(lfml);
      str_b = smt_convert_fml_to_string(rfml);
      fprintf(stdout, "fml = %s * %s\n", str_a, str_b);
      fprintf(stdout, "unknown\n");
      exit(0);
    }
    
  } else {
    fprintf(stdout, "ERROR: WRONG LINEAR ARITHMETIC ATOM TYPE\n");
    fprintf(stdout, "unknown\n");
    exit(0);
  }

  return;
}

void
smt_assign_bool_var_flag(smtManager_t * sm)
{
  satManager_t * cm = sm->cm;
  smtNvar_t * bvar;
  int i;

  for(i = 0; i < sm->bvarArr->size; i++) {
    bvar = (smtNvar_t *) sm->bvarArr->space[i];
    cm->bvars[bvar->id] = 1;
  }
}

void
smt_sort_nvar_array_with_id(satArray_t * arr)
{
  /* decreasing */
  smt_sort_nvar_array_with_id_aux(&(arr->space[0]), arr->size);
}

void
smt_sort_nvar_array_with_id_aux(long * arr, long size)
{
  smtNvar_t * nvar_a, * nvar_b;
  long i, j, tmp, bi;
  long pivot;

  if (size <= 15) { 
    for(i = 0; i < size-1; i++) {
      bi = i;
      for(j = i+1; j < size; j++) {
	nvar_a = (smtNvar_t *) arr[j];
	nvar_b = (smtNvar_t *) arr[bi];
	if (nvar_a->id < nvar_b->id)
	  bi = j;
      }

      tmp = arr[i];
      arr[i] = arr[bi];
      arr[bi] = tmp;
    }
  } else {
    pivot = arr[size>>1];
    i = -1;
    j = size;

    while(1) {
      do {
	i++; 
	nvar_a = (smtNvar_t *) arr[i];
	nvar_b = (smtNvar_t *) pivot;
      } while(nvar_a->id > nvar_b->id);
      
      do {
	j--;
	nvar_a = (smtNvar_t *) arr[j];
	nvar_b = (smtNvar_t *) pivot;
      } while(nvar_b->id > nvar_a->id);

      if(i>=j)	break;
      tmp = arr[i];
      arr[i] = arr[j];
      arr[j] = tmp;
    }
    smt_sort_nvar_array_with_id_aux(arr, i);
    smt_sort_nvar_array_with_id_aux(&(arr[i]), size-i);
  }
}

smtQueue_t *
smt_create_queue(long MaxElements)
{
smtQueue_t *Q;

  Q = (smtQueue_t *) malloc(sizeof(smtQueue_t));
  if(Q == NULL)
    fprintf(stderr, "Out of space!!!\n" );

  Q->array = (long *) malloc(sizeof(long)*MaxElements);
  if(Q->array == NULL)
    fprintf(stderr, "Out of space!!!\n" );
  Q->max = MaxElements;
  Q->size = 0;
  Q->front = 1;
  Q->rear = 0;
  return Q;
}

void
smt_init_queue(smtQueue_t * Q)
{
  Q->size = 0;
  Q->front = 1;
  Q->rear = 0;
  return;
}

void
smt_free_queue(smtQueue_t * Q)
{
  if( Q != NULL ) {
    free(Q->array);
    free(Q);
  }
}

void
smt_enqueue(
  smtQueue_t * Q,
  long v)
{
long *arr, *oarr;
long rear;

  if(Q->size < Q->max) {
    Q->size++;
    rear = Q->rear;
    rear = (++(rear) == Q->max) ? 0 : rear;
    Q->array[rear] = v;
    Q->rear = rear;
  }
  else {
    arr = (long *) malloc(sizeof(long)*Q->size*2);
    if(arr == NULL )
      fprintf(stderr, "Out of space!!!\n" );
    oarr = Q->array;
    if(Q->front > Q->rear) {
      memcpy(&(arr[1]), &(oarr[Q->front]), 
	     sizeof(long) *(Q->max-Q->front));
      memcpy(&(arr[Q->size-Q->front+1]), &(oarr[0]), 
	     sizeof(long) *(Q->rear+1));
    }
    else if(Q->front < Q->rear) {
      memcpy(&(arr[1]), &(oarr[Q->front]), sizeof(long) *(Q->size));
    }
    free(oarr);
    Q->array = arr;
    Q->front = 1;
    Q->rear = Q->size;
    Q->max *= 2;
    
    Q->size++;
    rear = Q->rear;
    rear = (++(rear) == Q->max) ? 0 : rear;
    Q->array[rear] = v;
    Q->rear = rear;
  }
}

long
smt_dequeue(smtQueue_t * Q)
{
long front;
long v;

  if(Q->size > 0) {
    Q->size--;
    front = Q->front;
    v = Q->array[front];
    Q->front = (++(front) == Q->max) ? 0 : front;
    return v;
  }
  else
    return(0);
}

int
smt_timeout(int timeout)
{
  if (timeout > 0) {
    cusp_timeout = timeout;
    (void) signal(SIGALRM, 
		  (void(*)(int))smt_timeout_handle);
    (void) alarm(cusp_timeout);
    if (setjmp(timeout_env) > 0) {
      (void) fprintf(stdout, "cusp : timeout occurred after %d seconds.\n", 
		     cusp_timeout);      
      alarm(0);
    }
  }

  return 0;
}

void
smt_timeout_handle(void)
{
  int seconds = (int) ((util_cpu_ctime() - alarm_lap_time) / 1000);

  if (seconds < cusp_timeout) {
    unsigned slack = (unsigned) (cusp_timeout - seconds);
    (void) signal(SIGALRM, (void(*)(int)) smt_timeout_handle);
    (void) alarm(slack);
  } else {
    longjmp(timeout_env, 1);
  }
}

void
smt_none(void)
{
  return;
}

#endif