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

  FileName    [smtFml.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"

smtFml_t *
smt_create_formula(smtFmlType_t ftype, satArray_t * subfmlArr)
{
  smtFml_t * fml, * tfml;
  int i;

  /* check for redundant NOT type */
  if (ftype == NOT_c && subfmlArr->size == 1) {
    tfml = (smtFml_t *) subfmlArr->space[0];
    if (tfml->type == NOT_c) {
      fml = (smtFml_t *) tfml->subfmlArr->space[0];
      return fml;
    }     
  }

  fml = (smtFml_t *) malloc(sizeof(smtFml_t));
  fml->id = 0;
  fml->flag = 0;

  fml->type = ftype;
  
  if (subfmlArr == 0) {
    fml->subfmlArr = 0;
    return fml;
  }

  fml->subfmlArr = sat_array_alloc(subfmlArr->size);

  for(i = 0; i < subfmlArr->size; i++) {
    tfml = (smtFml_t *) subfmlArr->space[i];
    fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) tfml);
  }

  fml->aig_node = Aig_NULL;
  fml->avar = 0;
  fml->bvar = 0;
  fml->nvar = 0;
  fml->nNeg = 0;
  fml->ins = 0;
  fml->value = 0;

  if (gvar->fmlArr) {
    gvar->fmlArr = sat_array_insert(gvar->fmlArr, (long) fml);  
    fml->id = gvar->fmlArr->size;
  } 

  return fml;
}

void
smt_duplicate_formula(smtFml_t * new_fml, smtFml_t * org)
{
  smtFml_t * tfml;
  int i;

  /* this duplicates the elements of org to new_fml */

  new_fml->id = org->id;

  if (org->flag & TRUE_MASK)
    new_fml->flag |= TRUE_MASK;
  else if (org->flag & FALSE_MASK)
    new_fml->flag |= FALSE_MASK;

  new_fml->type = org->type;
  new_fml->subfmlArr->size = 0;

  for(i = 0; i < org->subfmlArr->size; i++) {
    tfml = (smtFml_t *) org->subfmlArr->space[i];
    new_fml->subfmlArr = sat_array_insert(new_fml->subfmlArr, (long) tfml);
  }
 
  new_fml->aig_node = org->aig_node;

  new_fml->avar = org->avar;
  new_fml->bvar = org->bvar;
  new_fml->nvar = org->nvar;
  new_fml->value = org->value;

  return;
}

smtFml_t *
smt_create_identical_formula(smtFml_t * fml)
{
  smtFml_t * new_fml, * subfml;
  int i;

  new_fml = (smtFml_t *) malloc(sizeof(smtFml_t));

  new_fml->id = fml->id;
  new_fml->flag = fml->flag;
  new_fml->type = fml->type;
  new_fml->subfmlArr = sat_array_alloc(fml->subfmlArr->size);

  for(i = 0; i < fml->subfmlArr->size; i++) {
    subfml = (smtFml_t *) fml->subfmlArr->space[i];
    new_fml->subfmlArr = sat_array_insert(new_fml->subfmlArr, (long)subfml);
  }

  new_fml->aig_node = fml->aig_node;

  new_fml->avar = fml->avar;
  new_fml->bvar = fml->bvar;
  new_fml->nvar = fml->nvar;
  
  new_fml->nNeg = fml->nNeg;
  new_fml->ins = fml->ins;
  new_fml->value = fml->value;

  return new_fml;
}

smtFml_t *
smt_simplify_formula(smtFml_t * fml)
{
  smtFml_t * rfml = 0;
  smtFml_t * tfml;
  int i;
  
  for(i = 0; i < fml->subfmlArr->size; i++) {
    tfml = (smtFml_t *) fml->subfmlArr->space[i];
    if (tfml->type != PRED_c && tfml->type != FVAR_c &&
	tfml->type != fml->type) {
      rfml = 0;
      break;
    }
    if (rfml == 0 && tfml->type == fml->type) 
      rfml = tfml;
  }

  if (rfml) {
    for(i = 0; i < fml->subfmlArr->size; i++) {
      tfml = (smtFml_t *) fml->subfmlArr->space[i];
      if (tfml != rfml) 
	rfml->subfmlArr = sat_array_insert(rfml->subfmlArr, (long) tfml);
    }
  } else {
    rfml = fml;
  }

  return rfml;
}

void
smt_increase_subfml_ins(smtFml_t * fml)
{
  smtFml_t * subfml;
  int i;

  for(i = 0; i < fml->subfmlArr->size; i++) {
    subfml = (smtFml_t *) fml->subfmlArr->space[i];
    subfml->ins++;
  }
}

void
smt_add_fml_to_array(smtFml_t * fml)
{
  if (!(fml->flag & IN_ARR_MASK)) {
    gvar->fmlArr = sat_array_insert(gvar->fmlArr, (long) fml);
    fml->flag |= IN_ARR_MASK;
  }
}

smtFml_t *
smt_create_returning_formula(smtFml_t * fml)
{
  smtFml_t * rfml;

  /* 
     returning formula is needed for getting parent formula earlier 
     this enables flet to to substitute a var with replace_formula
  */

  gvar->tfmlArr->size = 0;
  assert(fml->type!=NONE_c);
  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fml);
  rfml = smt_create_formula(NONE_c, gvar->tfmlArr);
 
  return rfml;
}

smtFml_t *
smt_create_function_symbol(char * fs_name)
{
  smtFml_t * fml;

  gvar->tfmlArr->size = 0;
  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fs_name); 
  fml = smt_create_formula(FUN_c, gvar->tfmlArr);

  return fml;
}

smtFml_t *
smt_create_predicate_symbol(char * ps_name)
{
  smtFml_t *fml;

  gvar->tfmlArr->size = 0;
  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) ps_name); 
  fml = smt_create_formula(PRED_c, gvar->tfmlArr);

  return fml;
}

smtFml_t *
smt_create_constant_predicate_symbol(char * ps_name, int value)
{
  smtFml_t *fml;

  gvar->tfmlArr->size = 0;
  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) ps_name); 
  fml = smt_create_formula(PRED_c, gvar->tfmlArr);

  if (value==1) fml->flag |= TRUE_MASK;
  else if (value==0) fml->flag |= FALSE_MASK;

  return fml;  
}

smtFml_t *
smt_create_fml_variable(char * fname)
{
  smtFml_t *fml;

  gvar->tfmlArr->size = 0;
  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fname); 
  fml = smt_create_formula(FVAR_c, gvar->tfmlArr);

  return fml;
}

smtFml_t *
smt_create_term_variable(char * fs_name)
{
  smtFml_t * fml;
 
  gvar->tfmlArr->size = 0;
  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fs_name); 
  fml = smt_create_formula(TVAR_c, gvar->tfmlArr);

  return fml;
}

smtFml_t *
smt_create_constant_formula(char * cname)
{
  smtFml_t * fml;
  long value;

  gvar->tfmlArr->size = 0;
  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) cname); 
  fml = smt_create_formula(NUM_c, gvar->tfmlArr);
  value = strtol(cname, 0, 10);

  if (errno == ERANGE || value > INT_MAX) {
    gvar->flag |= MP_CONST_MASK;
  } else {
    fml->value = (int) value;
  }

  return fml;
}

void
smt_simplify_term_fml(smtFml_t * fml, st_table * num_table)
{
  smtFml_t * subfml, * tfml;
  char * str;
  int value = 0;
  int i;

  if (fml->type == ADD_c) {
    for(i = 0; i < fml->subfmlArr->size; i++) {
      subfml = (smtFml_t *) fml->subfmlArr->space[i];
      if (subfml->type != NUM_c) return; 
      value += subfml->value;
    }
    str = (char *) malloc(sizeof(char) * 10);
    sprintf(str, "%d", value);
    /* e.g. : (3 + 4) = 7 */
    if (st_lookup(num_table, str, (char **)&(tfml))) {
      free(str);
      smt_duplicate_formula(fml, tfml);
    } else {
      fml->type = NUM_c;
      fml->subfmlArr->size = 0;
      fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) str);
      fml->value = value;
      st_insert(num_table, str, (char *) fml);
    }

  } else if (fml->type == SUB_c) {
    subfml = (smtFml_t *) fml->subfmlArr->space[0];
    if (subfml->type != NUM_c) return;
    value = subfml->value;
    subfml = (smtFml_t *) fml->subfmlArr->space[1];
    if (subfml->type != NUM_c) return;
    value = value - subfml->value;
    if (value < 0) {
      fprintf(stdout, "simplifier does not handle minus value\n");
      return;
    }
    str = (char *) malloc(sizeof(char) * 10);
    sprintf(str, "%d", value);
    /* e.g. : (5 - 4) = 7 */
    if (st_lookup(num_table, str, (char **)&(tfml))) {
      free(str);
      smt_duplicate_formula(fml, tfml);
    } else {
      fml->type = NUM_c;
      fml->subfmlArr->size = 0;
      fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) str);
      fml->value = value;
      st_insert(num_table, str, (char *) fml);
    }
  }

  return;
}

void
smt_save_flet_pair(smtFml_t * fvar_fml, smtFml_t * fml)
{
  smtFlet_t * flet = (smtFlet_t *) malloc(sizeof(smtFlet_t));

  flet->fvar_fml = fvar_fml;
  flet->fml = fml;

  gvar->fletArr = sat_array_insert(gvar->fletArr, (long) flet);
}

void
smt_init_formula_flag(smtManager_t * sm)
{
  smtFml_t * fml;
  int i;

  for(i = 0; i < sm->fmlArr->size; i++) {
    fml = (smtFml_t *) sm->fmlArr->space[i];
    fml->flag = 0;
  }
}

void
smt_init_fml_visited_flag(smtManager_t * sm)
{
  smtFml_t * fml;
  int i;

  for(i = 0; i < sm->fmlArr->size; i++) {
    fml = (smtFml_t *) sm->fmlArr->space[i];
    fml->flag &= RESET_FML_VISITED_MASK;
  }
}

void
smt_init_fml_queued_flag(smtManager_t * sm)
{
  smtFml_t * fml;
  int i;

  for(i = 0; i < sm->fmlArr->size; i++) {
    fml = (smtFml_t *) sm->fmlArr->space[i];
    fml->flag &= RESET_QUEUED_MASK;
  }
}

char *
smt_convert_fml_to_string(smtFml_t * fml) 
{
  smtFml_t * fml_a, * fml_b, * fml_c;
  char * str_a = 0;
  char * str_b = 0;
  char * str_c = 0; 
  char * tstr_a = 0;
  char * tstr_b = 0;
  char * tstr_c = 0;
  char * result = 0;
  char str_true[5] = "true";
  char str_false[6] = "false";
  int i;

  if (fml == 0) {
    return 0; 
  }
    
  if (smt_is_leaf_fml(fml)) {
    if (fml->flag & TRUE_MASK) 
      result = util_strsav(str_true);
    else if (fml->flag & FALSE_MASK) 
      result = util_strsav(str_false);
    else {
      fml_a = (smtFml_t *) fml->subfmlArr->space[0];
      result = util_strsav((char *) fml_a);
    }
  }
  else if (fml->type == FLET_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    fml_c = (smtFml_t *) fml->subfmlArr->space[2];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    str_c = smt_convert_fml_to_string(fml_c);

    tstr_a = util_strcat3("(flet ", "(", str_b);
    tstr_b = util_strcat3(tstr_a, " ", str_c);
    tstr_c = util_strcat3(tstr_b, ")", " ");
    result = util_strcat3(tstr_c, str_a, ")");
  }
  else if (fml->type == NOT_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];    
    str_a = smt_convert_fml_to_string(fml_a);
    tstr_a = util_strcat3("not ", str_a, "");
    result = util_strcat3("(", tstr_a, ")");
  }
  else if (fml->type == IMP_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3(" -> ", str_a, str_b);
    result = util_strcat3("(", tstr_a, ")"); 
  }
  else if (fml->type == IFF_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("iff ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == AND_c) {
    tstr_a = util_strcat3("and ", "", "");
    for(i = 0; i < fml->subfmlArr->size; i++) {
      fml_a = (smtFml_t *) fml->subfmlArr->space[i];
      str_a = smt_convert_fml_to_string(fml_a);
      tstr_b = tstr_a;
      tstr_a = util_strcat3(tstr_a, str_a, " ");
      free(tstr_b);
      free(str_a);
      tstr_b = 0;
      str_a = 0;
    }
    result = util_strcat3("(", tstr_a, ")");
  }
  else if (fml->type == OR_c) {
    tstr_a = util_strcat3("or ", "", "");
    for(i = 0; i < fml->subfmlArr->size; i++) {
      fml_a = (smtFml_t *) fml->subfmlArr->space[i];
      str_a = smt_convert_fml_to_string(fml_a);
      tstr_b = tstr_a;
      tstr_a = util_strcat3(tstr_a, str_a, " ");
      free(tstr_b);
      free(str_a);
      tstr_b=0;
      str_a=0;
    }
    result = util_strcat3("(", tstr_a, ")");
  }
  else if (fml->type == XOR_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("xor ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, " ");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == NAND_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("nand ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, " ");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == ITE_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    fml_c = (smtFml_t *) fml->subfmlArr->space[2];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    str_c = smt_convert_fml_to_string(fml_c);
    
    if ( smt_is_term_formula(fml_b) )
      tstr_a = util_strcat3("ite ", str_a, " ");
    else
      tstr_a = util_strcat3("if_then_else ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, " ");
    tstr_c = util_strcat3(tstr_b, str_c, "");
    result = util_strcat3("(", tstr_c, ")");
  }
  else if (fml->type == TITE_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    fml_c = (smtFml_t *) fml->subfmlArr->space[2];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    str_c = smt_convert_fml_to_string(fml_c);
    tstr_a = util_strcat3("if_then_else ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, " ");
    tstr_c = util_strcat3(tstr_b, str_c, "");
    result = util_strcat3("(", tstr_c, ")");
  }
  else if (fml->type == EQ_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("= ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == NEQ_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("!= ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == LT_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("< ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == GT_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("> ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == LE_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("<= ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == GE_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3(">= ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == MUL_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("* ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == DIV_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("/ ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == REM_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("% ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == ADD_c) {
    tstr_a = util_strcat3("+ ", "", "");
    for(i = 0; i < fml->subfmlArr->size; i++) {
      fml_a = (smtFml_t *) fml->subfmlArr->space[i];
      str_a = smt_convert_fml_to_string(fml_a);
      tstr_b = tstr_a;
      tstr_a = util_strcat3(tstr_a, str_a, " ");
      free(tstr_b);
      free(str_a);
      tstr_b = 0;
      str_a = 0;
    }
    result = util_strcat3("(", tstr_a, ")");
  }
  else if (fml->type == SUB_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    tstr_a = util_strcat3("- ", str_a, " ");
    tstr_b = util_strcat3(tstr_a, str_b, "");
    result = util_strcat3("(", tstr_b, ")");
  }
  else if (fml->type == MINUS_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    str_a = smt_convert_fml_to_string(fml_a);
    tstr_a = util_strcat3("~ ", str_a, "");
    result = util_strcat3("(", tstr_a, ")");
  }
  else if (fml->type == LET_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    fml_c = (smtFml_t *) fml->subfmlArr->space[2];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    str_c = smt_convert_fml_to_string(fml_c);
    tstr_a = util_strcat3("let (", str_b, " ");
    tstr_b = util_strcat3(tstr_a, str_c, ") ");
    tstr_c = util_strcat3(tstr_b, str_a, "");
    result = util_strcat3("(", tstr_c, ")");
  }
  else if (fml->type == FLET_c) {
    fml_a = (smtFml_t *) fml->subfmlArr->space[0];
    fml_b = (smtFml_t *) fml->subfmlArr->space[1];
    fml_c = (smtFml_t *) fml->subfmlArr->space[2];
    str_a = smt_convert_fml_to_string(fml_a);
    str_b = smt_convert_fml_to_string(fml_b);
    str_c = smt_convert_fml_to_string(fml_c);
    tstr_a = util_strcat3("flet (", str_b, " ");
    tstr_b = util_strcat3(tstr_a, str_c, ") ");
    tstr_c = util_strcat3(tstr_b, str_a, "");
    result = util_strcat3("(", tstr_c, ")");
  } else {
    fprintf(stdout, "ERROR: Wrong FORMULA Type: %d\n", (int) fml->type);
  }

  if (str_a != 0) {
    free(str_a);
  }

  if (str_b != 0) {
    free(str_b);
  }

  if (str_c != 0) {
    free(str_c);
  }

  if (tstr_a != 0) {
    free(tstr_a);
  }

  if (tstr_b != 0) {
    free(tstr_b);
  }

  if (tstr_c != 0) {
    free(tstr_c);
  }

  return result;
}

char *
smt_convert_fml_to_string_with_subfml(
  smtFmlType_t type, 
  satArray_t * subfmlArr)
{
  smtFml_t * subfml;
  char * str_a, * str_b, * str_c;
  int i;

  str_a = (char *) malloc(sizeof(char) * 10); 
  str_b = (char *) malloc(sizeof(char) * 10); 
  sprintf(str_a, "%d", (int) type);

  for(i = 0; i < subfmlArr->size; i++) {
    subfml = (smtFml_t *) subfmlArr->space[i];
    sprintf(str_b, "%p", subfml);
    str_c = str_a;
    str_a = util_strcat3(str_a, str_b, "");
    free(str_c);
  }

  free(str_b);

  return str_a;
}

int
smt_is_leaf_fml(smtFml_t * fml)
{
  int is_leaf;
 
  is_leaf = (fml->type == FUN_c) || (fml->type == PRED_c) ||
    (fml->type == FVAR_c) || (fml->type == TVAR_c) ||
    (fml->type == NUM_c) ;

  return is_leaf;
}

int
smt_is_abstract_leaf_fml(smtFml_t * fml)
{
  int is_leaf;
 
  is_leaf = (fml->type == PRED_c) || (fml->type == FVAR_c) ||
    (fml->type == EQ_c) || (fml->type == NEQ_c) || (fml->type == LT_c) ||
    (fml->type == GT_c) || (fml->type == LE_c) || (fml->type == GE_c);

  return is_leaf;
}

int
smt_is_negated_abstract_leaf_fml(smtFml_t * fml)
{
  smtFml_t * subfml;
  int is_leaf;

  if (fml->type != NOT_c) {
    return 0;
  } else {
    subfml = (smtFml_t *) fml->subfmlArr->space[0];
    is_leaf = (subfml->type == PRED_c) || (subfml->type == FVAR_c) ||
      (subfml->type == EQ_c) || (subfml->type == NEQ_c) ||
      (subfml->type == LT_c) || (subfml->type == GT_c) || (subfml->type == LE_c) ||
      (subfml->type == GE_c);
  }

  return is_leaf;
}

int
smt_is_ite_chain_fml(smtFml_t * fml, int num_fml)
{
  smtFml_t * subfml_a, * subfml_b, * subfml_c;
  smtQueue_t * Q;
  int i, is_ite_chain = 1;

  assert(fml->type == ITE_c);

  Q = smt_create_queue(num_fml);
  
  smt_enqueue(Q, (long) fml);
   
  while( (fml = (smtFml_t *) smt_dequeue(Q)) ) {

      if (fml->type == ITE_c) {
	subfml_a = (smtFml_t *) fml->subfmlArr->space[0];
	subfml_b = (smtFml_t *) fml->subfmlArr->space[1];
	subfml_c = (smtFml_t *) fml->subfmlArr->space[2];
	
	if (subfml_a->type == AND_c) { /* cond : leaf or AND */
#if 0
	  if (subfml_a->subfmlArr->size == 2) {
	    subfml_d = (smtFml_t *) subfml_a->subfmlArr->space[0];
	    subfml_e = (smtFml_t *) subfml_a->subfmlArr->space[1];
	    if (!smt_is_abstract_leaf_fml(subfml_d) || 
		!smt_is_abstract_leaf_fml(subfml_e)) {
	      is_ite_chain = 0;
	      break;
	    }
	      
	  } else {
	    is_ite_chain = 0;
	    break;
	  }
#endif
	  smt_enqueue(Q, (long) subfml_a);
	} else if (!smt_is_abstract_leaf_fml(subfml_a)) {
	  is_ite_chain = 0;
	  break;
	} 
	if (subfml_b->type == AND_c) { /* then : leaf or AND */
	  smt_enqueue(Q, (long) subfml_b);
	} else if (!smt_is_abstract_leaf_fml(subfml_b)) {
	  is_ite_chain = 0;
	  break;
	} 
	/* then : ITE or leaf or AND */
	if (subfml_c->type == ITE_c || subfml_c->type == AND_c) { 
	  smt_enqueue(Q, (long) subfml_c);
	} else if (!smt_is_abstract_leaf_fml(subfml_c)) {
	  is_ite_chain = 0;
	  break;
	} 

      } else if (fml->type == AND_c) {
	for(i = 0; i < fml->subfmlArr->size; i++) {
	  subfml_a = (smtFml_t *) fml->subfmlArr->space[i];

	  if (subfml_a->type == AND_c) {
	    smt_enqueue(Q, (long) subfml_a);
	  } else if (!smt_is_abstract_leaf_fml(subfml_a)) {
	    is_ite_chain = 0;
	    break;
	  }
	}
      } else {
	is_ite_chain = 0;
	break;
      }
      /* } */
  }
      
  smt_free_queue(Q);

  return is_ite_chain;
}

int
smt_is_atom_formula(smtFml_t * fml)
{
  int is_atom;
 
  is_atom = (fml->type == EQ_c) || (fml->type == NEQ_c) || 
    (fml->type == LT_c) || (fml->type == GT_c) || (fml->type == LE_c) || 
    (fml->type == GE_c);

  return is_atom;
}

int
smt_is_negated_atom_formula(smtFml_t * fml)
{
  smtFml_t * subfml;
  int is_atom;

  if (fml->type != NOT_c) {
    return 0;
  } else {
    subfml = (smtFml_t *) fml->subfmlArr->space[0];
    is_atom = (subfml->type == EQ_c) || (subfml->type == NEQ_c) ||
      (subfml->type == LT_c) || (subfml->type == GT_c) ||
      (subfml->type == LE_c) || (subfml->type == GE_c);
  }

  return is_atom;
}

int
smt_is_boolean_formula(smtFml_t * fml)
{
  int is_bool;
 
  is_bool = (fml->type == PRED_c) || (fml->type == FVAR_c);

  return is_bool;
}

int
smt_is_negated_boolean_formula(smtFml_t * fml)
{
  smtFml_t * subfml;
  int is_bool;

  if (fml->type != NOT_c) {
    return 0;
  } else {
    subfml = (smtFml_t *) fml->subfmlArr->space[0];
    is_bool = (subfml->type == PRED_c) || (subfml->type == FVAR_c);
  }

  return is_bool;
}

int
smt_is_arith_formula(smtFml_t * fml)
{
  if (fml->type == SUB_c || fml->type == ADD_c || fml->type == MUL_c ||
      fml->type == DIV_c || fml->type == MINUS_c)
    return 1;
  else
    return 0;
}

int
smt_is_multi_arith_formula(smtFml_t * fml)
{
  if (fml->type == ADD_c || fml->type == MUL_c)
    return 1;
  else
    return 0;
}

int
smt_is_binary_arith_formula(smtFml_t * fml)
{
  if (fml->type == SUB_c || fml->type == DIV_c)
    return 1;
  else
    return 0;
}

int
smt_is_unary_arith_formula(smtFml_t * fml)
{
  if (fml->type == MINUS_c)
    return 1;
  else
    return 0;
}

int
smt_is_term_formula(smtFml_t * fml)
{
  if ( smt_is_arith_formula(fml) || fml->type == FUN_c || 
       fml->type == NUM_c )
    return 1;
  else
    return 0;
}

int
smt_is_bool_atom_fml(smtFml_t * fml)
{
  smtFml_t * lfml, * rfml;
  int is_const = 2, is_true = 2, lvalue, rvalue;

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

  is_const = smt_get_constant_value_in_fml(lfml, &lvalue);
  
  if (is_const == 0) return 0;
  
  is_const = smt_get_constant_value_in_fml(rfml, &rvalue);

  if (is_const == 0) return 0;

  if (fml->type == EQ_c) {
    if (lvalue == rvalue) {
      is_true = 1; /* true */
    } else {
      is_true = 0; /* false */
    }
  } else if (fml->type == LE_c) {
    if (lvalue <= rvalue) {
      is_true = 1; /* true */
    } else {
      is_true = 0; /* false */
    }
  } else if (fml->type == LT_c) {
    if (lvalue < rvalue) {
      is_true = 1; /* true */
    } else {
      is_true = 0; /* false */
    }
  } else if (fml->type == GE_c) {
    if (lvalue >= rvalue) {
      is_true = 1; /* true */
    } else {
      is_true = 0; /* false */
    }
  } else if (fml->type == GT_c) {
    if (lvalue > rvalue) {
      is_true = 1; /* true */
    } else {
      is_true = 0; /* false */
    }
  }

  fml->type = PRED_c;

  assert(is_true != 2);

  if (is_true) {
    fml->flag |= TRUE_MASK;
  } else {
    fml->flag |= FALSE_MASK;
  }
  
  return 1;
}

int
smt_get_constant_value_in_fml(smtFml_t * fml, int * value)
{
  smtFml_t * lfml, * rfml, * tfml;
  int is_const, value_a, value_b;
  int i;

  if (fml->type == NUM_c) {
    *value = fml->value;
  } else if (fml->type == MINUS_c) {
    tfml = (smtFml_t *) fml->subfmlArr->space[0];
    is_const = smt_get_constant_value_in_fml(tfml, &value_a);
    if (is_const == 0) return 0;
    *value = -value_a;
  } else if (fml->type == SUB_c) {
    lfml = (smtFml_t *) fml->subfmlArr->space[0];
    rfml = (smtFml_t *) fml->subfmlArr->space[1];

    is_const = smt_get_constant_value_in_fml(lfml, &value_a);
    if (is_const == 0) return 0;
    is_const = smt_get_constant_value_in_fml(rfml, &value_b);
    if (is_const == 0) return 0;
    *value = value_a - value_b;
  } else if (fml->type == ADD_c) {
    for(i = 0, *value = 0; i < fml->subfmlArr->size; i++) {
      tfml = (smtFml_t *) fml->subfmlArr->space[i];
      is_const = smt_get_constant_value_in_fml(tfml, &value_a);
      if (is_const == 0) return 0;
      *value += value_a;
    }
  } else if (fml->type == MUL_c) {
    for(i = 0, *value = 1; i < fml->subfmlArr->size; i++) {
      tfml = (smtFml_t *) fml->subfmlArr->space[i];
      is_const = smt_get_constant_value_in_fml(tfml, &value_a);
      if (is_const == 0) return 0;
      *value *= value_a;
    }
  } else return 0;

  return 1;
}

void
smt_convert_eq_fml_to_ineq_fml(smtManager_t * sm)
{
  smtFml_t * avfml, * fml_a, * fml_b;
  satArray_t * avfmlArr = sat_array_alloc(sm->avfmlArr->size * 2);
  int existEq = 0;
  int i;
  
  for(i = 0; i < sm->avfmlArr->size; i++) {
    avfml = (smtFml_t *) sm->avfmlArr->space[i];
    if (avfml->type == EQ_c) {
      sm->stats->num_eq2ineq++;

      smt_convert_eq_fml_into_ineq_and_fml(sm, avfml);

      fml_a = (smtFml_t *) avfml->subfmlArr->space[0];
      fml_b = (smtFml_t *) avfml->subfmlArr->space[1];
      avfmlArr = sat_array_insert(avfmlArr, (long) fml_a);
      avfmlArr = sat_array_insert(avfmlArr, (long) fml_b);      
      existEq = 1;

    } else if (avfml->type == NEQ_c) {
      sm->stats->num_eq2ineq++;

      smt_convert_diseq_fml_into_ineq_or_fml(sm, avfml);

      fml_a = (smtFml_t *) avfml->subfmlArr->space[0];
      fml_b = (smtFml_t *) avfml->subfmlArr->space[1];
      avfmlArr = sat_array_insert(avfmlArr, (long) fml_a);
      avfmlArr = sat_array_insert(avfmlArr, (long) fml_b);
      existEq = 1;

    } else if ( smt_is_atom_formula(avfml) ) {
      avfmlArr = sat_array_insert(avfmlArr, (long) avfml);
    }
  }

  if (existEq) {
    free(sm->avfmlArr);
    sm->avfmlArr = avfmlArr;
  } else {
    free(avfmlArr);
  }
}

void
smt_add_flet_pair_formula(smtManager_t * sm)
{
  smtFml_t * root = sm->fml;
  smtFml_t * and_fml, * fvar_fml, * fml, * iff_fml;
  smtFlet_t * flet;
  int i;
  
  /* combine root with flet_pair formula */
  
  gvar->tfmlArr->size = 0;
  gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) root);
  and_fml = smt_create_formula(AND_c, gvar->tfmlArr);
  sm->fmlArr = sat_array_insert(sm->fmlArr, (long) and_fml);
   
  for(i = 0; i < sm->fletArr->size; i++) {
    flet = (smtFlet_t *) sm->fletArr->space[i]; 
    fvar_fml = flet->fvar_fml;
    fml = flet->fml;
    /* iff_fml = (fvar_fml <-> fml) */
    gvar->tfmlArr->size = 0;
    gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fvar_fml);
    gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fml);    
    iff_fml = smt_create_formula(IFF_c, gvar->tfmlArr); 
    and_fml->subfmlArr = sat_array_insert(and_fml->subfmlArr, (long) iff_fml);
    sm->fmlArr = sat_array_insert(sm->fmlArr, (long) iff_fml);
  } 
  
  sm->fml = and_fml;
}

void 
smt_convert_eq_fml_into_ineq_and_fml(smtManager_t * sm, smtFml_t * fml)
{
  smtFml_t * leq_fml, * geq_fml;

  assert(fml->type==EQ_c);

  /* ax + by + ... <= c */
  leq_fml = smt_create_identical_formula(fml);
  leq_fml->type = LE_c;
  sm->fmlArr = sat_array_insert(sm->fmlArr, (long) leq_fml);
  leq_fml->id = sm->fmlArr->size;
  leq_fml->ins = 1;
 
  /* ax + by + ... >= c */
  geq_fml = smt_create_identical_formula(fml);
  geq_fml->type = GE_c;
  sm->fmlArr = sat_array_insert(sm->fmlArr, (long) geq_fml);
  geq_fml->id = sm->fmlArr->size;
  geq_fml->ins = 1;
   
  /* leq_fml /\ geq_fml */
  fml->type = AND_c;
  fml->subfmlArr->size = 0;
  fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) leq_fml);
  fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) geq_fml);
}

void 
smt_convert_diseq_fml_into_ineq_or_fml(smtManager_t * sm, smtFml_t * fml)
{
  smtFml_t * lt_fml, * gt_fml;

  assert(fml->type==NEQ_c);

  /* ax + by + ... < c */
  lt_fml = smt_create_identical_formula(fml);
  lt_fml->type = LT_c;
  sm->fmlArr = sat_array_insert(sm->fmlArr, (long) lt_fml);
  lt_fml->id = sm->fmlArr->size;
  lt_fml->ins = 1;
 
  /* ax + by + ... > c */
  gt_fml = smt_create_identical_formula(fml);
  gt_fml->type = GT_c;
  sm->fmlArr = sat_array_insert(sm->fmlArr, (long) gt_fml);
  gt_fml->id = sm->fmlArr->size;
  gt_fml->ins = 1;
   
  /* lt_fml \/ gt_fml */
  fml->type = OR_c;
  fml->subfmlArr->size = 0;
  fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) lt_fml);
  fml->subfmlArr = sat_array_insert(fml->subfmlArr, (long) gt_fml);
}

satArray_t *
smt_gather_bvar_in_fml(smtManager_t * sm, smtFml_t * fml)
{
  smtFml_t * ufml, * tfml;
  smtQueue_t * Q;
  satArray_t * bvarArr;
  int * bflags;
  int i, is_leaf, init_id, flag;

  bvarArr = sat_array_alloc(sm->bvarArr->size);

  bflags = (int *) malloc(sizeof(int) * sm->bvarArr->size);
  
  memset(bflags, 0, sizeof(int) * sm->bvarArr->size);

  /* init_id = ((smtBvar_t *) sm->bvarArr->space[0])->id; */
  if (sm->avarArr) init_id = sm->avarArr->size + 1;
  else init_id = 1;

  Q = smt_create_queue(sm->fmlArr->size);
  
  smt_enqueue(Q, (long) fml);
   
  while( (ufml = (smtFml_t *) smt_dequeue(Q)) ) {

    is_leaf = smt_is_abstract_leaf_fml(ufml) || smt_is_leaf_fml(ufml);

    if ( (!is_leaf) ) {
      for(i = 0; i < ufml->subfmlArr->size; i++) {
	tfml = (smtFml_t *) ufml->subfmlArr->space[i];
	smt_enqueue(Q, (long) tfml);
      }
    } else {
      if (ufml->bvar) {
	flag = bflags[ufml->bvar->id - init_id];
	if (!flag) {
	  bvarArr = sat_array_insert(bvarArr, (long) ufml->bvar);
	  bflags[ufml->bvar->id - init_id] = 1;
	}
      }      
    }
  }

  if (Q) smt_free_queue(Q);

  if (bflags) free(bflags);

  return bvarArr;
}

void
smt_combine_root_fml_with_flet_fml(void)
{
  smtFml_t * subfml, * fvar_fml, * fml, * iff_fml;
  smtFlet_t * flet;
  satArray_t * subfmlArr;
  int i;

  subfmlArr = sat_array_alloc(gvar->fletArr->size * 2);

  if (gvar->fml->type == AND_c) {
    for(i = 0; i < gvar->fml->subfmlArr->size; i++) {
      subfml = (smtFml_t *) gvar->fml->subfmlArr->space[i];
      subfmlArr = sat_array_insert(subfmlArr, (long) subfml);
    }
  } else { 
    subfmlArr = sat_array_insert(subfmlArr, (long) gvar->fml);
  }
    
  for(i = 0; i < gvar->fletArr->size; i++) {
    flet = (smtFlet_t *) gvar->fletArr->space[i];
    fvar_fml = flet->fvar_fml;
    fml = flet->fml;

    /* iff_fml = (fvar_fml <-> fml) */
    gvar->tfmlArr->size = 0;
    gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fvar_fml);
    gvar->tfmlArr = sat_array_insert(gvar->tfmlArr, (long) fml);    
    iff_fml = smt_create_formula(IFF_c, gvar->tfmlArr); 
    subfmlArr = sat_array_insert(subfmlArr, (long) iff_fml);
    gvar->fmlArr = sat_array_insert(gvar->fmlArr, (long) iff_fml);    
  }

  if (gvar->fml->type == AND_c) {
    free(gvar->fml->subfmlArr);
    gvar->fml->subfmlArr = subfmlArr;
  } else {
    gvar->fml = smt_create_formula(AND_c, subfmlArr);
  }
}

#endif