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

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

smtGlobalVar_t * gvar;

/**Function********************************************************************

  Synopsis    [Smt main function]
  
  Description []

  SideEffects []

  SeeAlso     []

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

int
smt_main(char * filename, int timeout, int is_model)
{
  smtManager_t * sm;
  long btime, etime;

  btime = util_cpu_time();
  
  /* read smt */
  smt_read(filename);

  /* init */
  sm = smt_init();

  if (sm == 0) {
    free(filename);
    return 0; /* simple aig case */
  }

  /* timeout */
  smt_timeout(timeout);
  
  /* preprocess */
  smt_preprocess(sm);
  
  /* solve */
  smt_solve(sm);

  etime = util_cpu_time();
  
  sm->stats->solve_time = (double)(etime - btime) / 1000.0;
  
  /* report */
  smt_report(sm, is_model);  
  
  /* postprocess */
  smt_postprocess(sm);

  free(filename);

  return 0;
}


/**Function********************************************************************

  Synopsis    [Parsing function for smt file]
  
  Description [Parse smt file and create formula structure for the parse tree]

  SideEffects []

  SeeAlso     []

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

void
smt_read(char * str)
{
  FILE * fp;
  char * filename;
  
  if (str) 
    filename = strdup(str);
  else
    filename = 0;

  if (filename) {
    if(!(fp = fopen(filename, "r"))) {
      fprintf(stderr, "ERROR : Can't open SMT file %s\n", filename);
      exit(0);
    }
  } else {
    if(!(fp = stdin)) {
      fprintf(stderr, "ERROR : Can't open SMT file %s\n", filename);
      exit(0);
    }
  }

  gvar = (smtGlobalVar_t *) malloc(sizeof(smtGlobalVar_t));
  
  smt_init_global_variable(filename);

  SmtFileSetup(fp);

  (void) SmtYyparse();

  if (gvar->fletArr->size)
    smt_combine_root_fml_with_flet_fml();

  return;
}

/**Function********************************************************************

  Synopsis    [Smt structure initialization]
   
  Description [Initialize smt structure]

  SideEffects []

  SeeAlso     []

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

smtManager_t *
smt_init(void)
{
  smtManager_t * sm;
  
  if (gvar->flag & IDL_MASK || gvar->flag & RDL_MASK)
    sm = smt_dl_init();
  else {
    fprintf(stdout, "ERROR : Unsupported logic\n");
    exit(0);
  }

  if ( !(sm->flag & CNF_MASK) ) {
    if (sm->obj == Aig_One || sm->obj == Aig_Zero) {
      /* root aig is either true or false */
      if (sm->obj == Aig_Zero) sm->flag &= RESET_SAT_MASK;

      smt_report(sm, 0);

      smt_postprocess(sm);

      return 0;
    }   
  }

  return sm;
}

/**Function********************************************************************

  Synopsis    [Difference logic structure initialization]
  
  Description [Initialize difference logic structure]

  SideEffects []

  SeeAlso     []

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

smtManager_t *
smt_dl_init(void)
{
  smtManager_t * sm;
  
  sm = smt_init_manager();
#if 1
  smt_convert_eq_fml_to_ineq_fml(sm);
#endif
  smt_create_dl_atom_variable_main(sm);
  
  smt_init_atom_variable_values(sm);

  smt_init_numerical_variable_values(sm);

#if 0
  smt_print_atomic_predicate_variable(sm);
  
  smt_print_boolean_variable(sm);

  smt_print_flet_pair(sm);
#endif

  smt_assign_boolean_variable_id(sm); 

  smt_assign_numerical_variable_id(sm);

  if (sm->flag & MP_CONST_MASK) {
    smt_mp_init(sm);
    smt_mp_assign_atom_constants(sm);
#if 0
    smt_mp_print_atom_constants(sm);
#endif
  }

  smt_generate_cnf_main(sm);

  return sm;
}

/**Function********************************************************************

  Synopsis    [Solving function]
  
  Description [Solve smt problem]

  SideEffects []

  SeeAlso     []

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

void
smt_solve(smtManager_t * sm)
{
  satManager_t * cm;

  smt_circus_interface(sm);

  cm = sm->cm;

  if (cm->simplify) {

    smt_assign_bool_var_flag(sm);

  } 

  if(cm->status == 2) {
    sat_circus_solve(cm);
  }
  
  assert(cm->status != 2);

  sat_report_result(cm);

  smt_check_result(sm);
}

/**Function********************************************************************

  Synopsis    [Result reporting function]
  
  Description [Print result of smt problem]

  SideEffects []

  SeeAlso     []

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

void
smt_report(smtManager_t * sm, int is_model)
{
  /* smt_check_result(sm); -> smt_solve */

  smt_report_result(sm, is_model);
}

/**Function********************************************************************

  Synopsis    [Post process]
  
  Description [Free global variable structure and smt structure]

  SideEffects []

  SeeAlso     []

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

void
smt_postprocess(smtManager_t * sm)
{
  smt_free_global_variable();

  smt_free_manager(sm);
}

/**Function********************************************************************

  Synopsis    [Global variable initialization]
  
  Description [Initialize global variable]

  SideEffects []

  SeeAlso     []

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

void
smt_init_global_variable(char * filename)
{
  gvar->fml = 0;
  gvar->tfml = 0;
  gvar->nvar = 0;

  gvar->fmlArr = sat_array_alloc(1000);
  gvar->tfmlArr = sat_array_alloc(4);
  gvar->avfmlArr = sat_array_alloc(1000);
  gvar->bvarArr = sat_array_alloc(1000);
  gvar->nvarArr = sat_array_alloc(1000);
  gvar->fletArr = sat_array_alloc(1000);

  gvar->epsilon = 0;
  gvar->epsilonless = 0;

  gvar->flag = 0;
  gvar->status = 2;
  gvar->filename = filename;
  gvar->str = 0;
  
  gvar->fun_table = st_init_table(strcmp, st_strhash);
  gvar->pred_table = st_init_table(strcmp, st_strhash);
  gvar->fml_var_table = st_init_table(strcmp, st_strhash);
  gvar->term_var_table = st_init_table(strcmp, st_strhash);
  gvar->term_table = st_init_table(strcmp, st_strhash);
  gvar->num_table = st_init_table(strcmp, st_strhash);
}

/**Function********************************************************************

  Synopsis    [Global variable structure freeing function]
  
  Description [Free global variable structure]

  SideEffects []

  SeeAlso     []

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

void
smt_free_global_variable(void)
{
  if (gvar->tfmlArr)
    free(gvar->tfmlArr);

  if (gvar->fun_table)
    st_free_table(gvar->fun_table);

  if (gvar->pred_table)
    st_free_table(gvar->pred_table);

  if (gvar->fml_var_table) {
    smt_free_key_in_table(gvar->fml_var_table);
    st_free_table(gvar->fml_var_table);
  }

  if (gvar->term_var_table) {
    smt_free_key_in_table(gvar->term_var_table);
    st_free_table(gvar->term_var_table);
  }

  if (gvar->term_table)
    st_free_table(gvar->term_table);

  if (gvar->num_table) {
    smt_free_key_in_table(gvar->num_table);
    st_free_table(gvar->num_table);
  }
  
}

/**Function********************************************************************

  Synopsis    [St_table key freeing function]
  
  Description [Free keys in st_table]

  SideEffects []

  SeeAlso     []

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

void
smt_free_key_in_table(st_table * table)
{
  st_generator * gen;
  char * key;

  st_foreach_item(table, gen, (char **)&key, 0) {
    free(key);
  }
  
  return;
}

/**Function********************************************************************

  Synopsis    [St_table key freeing function]
  
  Description [Free keys and arrays in st_table]

  SideEffects []

  SeeAlso     []

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

void
smt_free_key_with_array_in_table(st_table * table)
{
  st_generator * gen;
  array_t * arr;
  char * key;

  st_foreach_item(table, gen, (char **)&key, (char **)&arr) {
    free(key);
    array_free(arr);
  }
  
  return;
}

/**Function********************************************************************

  Synopsis    [Smt manager initialization]
  
  Description [Initialize smt manager structure]

  SideEffects []

  SeeAlso     []

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

smtManager_t *
smt_init_manager(void)
{
  smtManager_t * sm;

  sm = (smtManager_t *) malloc(sizeof(smtManager_t));

  sm->clsArr = sat_array_alloc(2000);
  sm->la_clsArr = 0;
  sm->avarArr = 0;
  sm->bvarArr = gvar->bvarArr;
  sm->nvarArr = gvar->nvarArr;
  sm->tmp_nvars = 0;
  sm->tab_avars = 0;
  sm->tab_nvars = 0;
  sm->slacks = 0;
  sm->basics = 0;
  sm->fmlArr = gvar->fmlArr;
  sm->avfmlArr = gvar->avfmlArr;
  sm->iff_fmlArr = sat_array_alloc(gvar->fmlArr->size);
  sm->ite_fmlArr = sat_array_alloc(gvar->fmlArr->size);
  sm->fletArr = gvar->fletArr;
  sm->id2var = 0;
  sm->id2slack = 0;
  sm->node2id = 0;
  sm->node2ins = 0;
  sm->node2fml = 0;
  sm->sis_table = 0;
  sm->fml_table = st_init_table(strcmp, st_strhash);
  
  gvar->bvarArr = 0;
  gvar->nvarArr = 0;
  gvar->fmlArr = 0;
  gvar->avfmlArr = 0;
  gvar->fletArr = 0;
 
  sm->fml = gvar->fml;
  sm->stats = smt_init_stats();
  sm->flag = gvar->flag;
  sm->flag |= SAT_MASK;
  
  gvar->fml = 0;
  gvar->flag = 0;

  if (sm->flag & IDL_MASK) {
    sm->epsilon = 1;
    sm->epsilonless = 0;
  } else { /* RDL */
    sm->epsilon = 0.000001;
    sm->epsilonless = 0.0000001;
  }

  sm->litArr = sat_array_alloc(sm->avfmlArr->size);
  sm->lemma = sat_array_alloc(32);
  sm->tplits = sat_array_alloc(32);
  
  sm->bm = 0;
  sm->cm = 0;
  sm->cG = 0;
  sm->mp = 0;
  sm->tab = 0;
  sm->bounds = 0;
  
  sm->filename = gvar->filename;
  gvar->filename = 0;

  sm->cur_index = 0;
  sm->limit = 300;
  
  return sm;
}

/**Function********************************************************************

  Synopsis    [Smt manager freeing function]
  
  Description [Free smt manager structure]

  SideEffects []

  SeeAlso     []

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

void
smt_free_manager(smtManager_t * sm)
{
  smt_free_clauses(sm->clsArr);
  smt_free_atom_variables(sm->avarArr);
  smt_free_bool_variables(sm->bvarArr);
  smt_free_numerical_variables(sm->nvarArr);
  smt_free_formulas(sm->fmlArr);
 
  if (sm->clsArr) free(sm->clsArr);
  if (sm->avarArr) free(sm->avarArr);
  if (sm->bvarArr) free(sm->bvarArr);
  if (sm->nvarArr) free(sm->nvarArr);
  if (sm->fmlArr) free(sm->fmlArr);
  if (sm->avfmlArr) free(sm->avfmlArr);
  if (sm->fletArr) free(sm->fletArr);
  if (sm->iff_fmlArr) free(sm->iff_fmlArr);
  if (sm->ite_fmlArr) free(sm->ite_fmlArr);
  if (sm->id2var) free(sm->id2var);
  if (sm->node2id) free(sm->node2id);
  if (sm->node2fml) free(sm->node2fml);
  if (sm->stats) free(sm->stats);
  if (sm->litArr) free(sm->litArr);
  if (sm->lemma) free(sm->lemma);
  if (sm->tplits) free(sm->tplits);
  if (sm->filename) free(sm->filename);
  
  if (sm->avalues) free(sm->avalues);
  if (sm->ivalues) free(sm->ivalues);
  if (sm->rvalues) free(sm->rvalues);
  if (sm->prvalues) free(sm->prvalues);
  if (sm->node2ins) free(sm->node2ins);
  if (sm->sis_table) {
    smt_free_key_with_array_in_table(sm->sis_table);
    st_free_table(sm->sis_table);  
  }
  if (sm->fml_table) {
    smt_free_key_in_table(sm->fml_table);
    st_free_table(sm->fml_table);  
  }

  if (sm->cm) sat_free_manager(sm->cm);
  if (sm->bm) Aig_quit(sm->bm);
  if (sm->mp) smt_mp_free(sm->mp);
  if (sm->cG) smt_free_constraint_graph(sm->cG);

  free(sm);
}

/**Function********************************************************************

  Synopsis    [Clauses freeing function]
  
  Description [Free clauses in clause array]

  SideEffects []

  SeeAlso     []

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

void
smt_free_clauses(satArray_t * clsArr) 
{
  smtCls_t * cls;
  int i;

  for(i = 0; i < clsArr->size; i++) {
    cls = (smtCls_t *) clsArr->space[i];
    free(cls->litArr);
    free(cls);
  }

  return;
}

/**Function********************************************************************

  Synopsis    [Atom variable freeing function]
  
  Description [Free atom variables in array]

  SideEffects []

  SeeAlso     []

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

void
smt_free_atom_variables(satArray_t * avarArr) 
{
  smtAvar_t * avar;
  int i;

  for(i = 0; i < avarArr->size; i++) {
    avar = (smtAvar_t *) avarArr->space[i];
    smt_free_atom_members(avar);
    free(avar);
  }

  return;
}

/**Function********************************************************************

  Synopsis    [Atom variable member freeing function]
  
  Description [Free atom variable members]

  SideEffects []

  SeeAlso     []

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

void
smt_free_atom_members(smtAvar_t * avar)
{
  free(avar->name);
  free(avar->nvars);
  array_free(avar->coeffs);
  
  return;
}

/**Function********************************************************************

  Synopsis    [Boolean variable freeing function]
  
  Description [Free boolean variables in array]

  SideEffects []

  SeeAlso     []

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

void
smt_free_bool_variables(satArray_t * bvarArr) 
{
  smtBvar_t * bvar;
  int i;

  for(i = 0; i < bvarArr->size; i++) {
    bvar = (smtBvar_t *) bvarArr->space[i];
    free(bvar->name);
    free(bvar);
  }

  return;
}

/**Function********************************************************************

  Synopsis    [Numerical variable freeing function]
  
  Description [Free numerical variables in array]

  SideEffects []

  SeeAlso     []

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

void
smt_free_numerical_variables(satArray_t * nvarArr) 
{
  smtNvar_t * nvar;
  int i;

  for(i = 0; i < nvarArr->size; i++) {
    nvar = (smtNvar_t *) nvarArr->space[i];
    free(nvar->name);
    free(nvar->avarArr);
    free(nvar);
  }

  return;
}

/**Function********************************************************************

  Synopsis    [Formula freeing function]
  
  Description [Free formula structure in array]

  SideEffects []

  SeeAlso     []

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

void
smt_free_formulas(satArray_t * fmlArr) 
{
  smtFml_t * fml;
  int i;

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

  return;
}

/**Function********************************************************************

  Synopsis    [Numerical variables' values initialization]
  
  Description [Initialize numerical variables' values]

  SideEffects []

  SeeAlso     []

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

void
smt_init_numerical_variable_values(smtManager_t * sm)
{
  smtNvar_t * nvar;
  satArray_t * new_nvarArr = sat_array_alloc(sm->nvarArr->size);
  int i, j, size;

  /* update nvarArr by checking unused nvar */
  for(i = 0, j = 1; i < sm->nvarArr->size; i++) {
    nvar = (smtNvar_t *) sm->nvarArr->space[i];
    if (nvar->avarArr) {
      nvar->id = j;
      new_nvarArr = sat_array_insert(new_nvarArr, (long) nvar);
      j++;
    } else {
      /* free(nvar) */
    }
  }

  free(sm->nvarArr);
  sm->nvarArr = new_nvarArr;

  if (sm->flag & IDL_MASK) {
    sm->ivalues = (int *) malloc(sizeof(int) * (sm->nvarArr->size+1));
    memset(sm->ivalues, 0, sizeof(int)*(sm->nvarArr->size));
    sm->rvalues = 0;
    sm->prvalues = 0;
  } else { /* RDL */
    sm->ivalues = 0;
    size = sm->nvarArr->size + 1;

    /* require update : may shrink later */
    sm->rvalues = (double *) malloc(sizeof(double) * size);
    memset(sm->rvalues, 0, sizeof(double) * size);    
    sm->prvalues = 0;
  }
  
  return;
}

/**Function********************************************************************

  Synopsis    [Statistics structure initialization]
  
  Description [Initialize statistics structure]

  SideEffects []

  SeeAlso     []

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

smtStats_t *
smt_init_stats(void)
{
  smtStats_t * stats;

  stats = (smtStats_t *)malloc(sizeof(smtStats_t));

  stats->solve_time = 0;
  stats->num_bf_call = 0;
  stats->num_bf_conf = 0;
  stats->num_assert_call = 0;
  stats->num_assert_conf = 0;
  stats->num_check_call = 0;
  stats->num_check_conf = 0;

  stats->num_tprop_call = 0;
  stats->num_tprop = 0;
  stats->num_simp_tprop_call = 0;
  stats->num_simp_tprop = 0;

  stats->num_avar = 0;
  stats->num_eq = 0;
  stats->num_ceq = 0;
  stats->num_ineq = 0;
  stats->num_eq2ineq = 0;
  stats->num_lzero_eq = 0;
  stats->num_lzero_ineq = 0;
  stats->num_inter_bvar = 0;
  stats->num_velm_cand = 0;
  stats->num_static_cls = 0;
  stats->num_static_pred = 0;
  stats->num_row = 0;
  stats->num_col = 0;

  return stats;
}

/**Function********************************************************************

  Synopsis    [Smt & Sat interface]
  
  Description [Generate sat structure with smt structure]

  SideEffects []

  SeeAlso     []

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

void
smt_circus_interface(smtManager_t * sm)
{
  satManager_t * cm = sat_init_manager();

  cm->SMTManager = (long *) sm;

  sm->cm = cm;

  cm->nClauses = sm->clsArr->size;

  cm->nVars = sm->num_var;

  sat_create_database(cm);

  smt_circus_cnf_interface(sm);
}

/**Function********************************************************************

  Synopsis    [Cnf Generating function]
  
  Description [Generate Cnf with smt structure]

  SideEffects []

  SeeAlso     []

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

void
smt_circus_cnf_interface(smtManager_t * sm)
{
  satManager_t *cm = sm->cm;
  smtCls_t *cls;
  satClause_t *c;
  satArray_t *clsArr = sm->clsArr;
  satArray_t *litArr = sat_array_alloc(100);
  long id, lit, sign;
  int i, j;

  for(i = 0; i < clsArr->size; i++) {
    litArr->size = 0; 
    cls = (smtCls_t *) sm->clsArr->space[i];

    for(j = 0; j < cls->litArr->size; j++) {
      lit = cls->litArr->space[j];
      if (lit==0) continue;
      sign = (lit<0) ? 1 : 0;
      id = (lit<0) ? -lit : lit;
      litArr = sat_array_insert(litArr, ((id<<1) + sign));
    }

    c = sat_add_clause(cm, litArr, 0);
    sat_init_variable_activity(cm, c);
  }
  
#if 1
  for(i = 1; i <= cm->nVars; i++) {
    sat_heap_insert(cm, cm->variableHeap, i);
  }
#else
  if (sm->flag & CNF_MASK) {
    for(i = 1; i <= cm->nVars; i++) {
      sat_heap_insert(cm, cm->variableHeap, i);
    }
  } else { /* somehow causes # of var reduction : no effect to efficiency */
    satArray_t * ordered = smt_get_decision_order(sm);
    for(i = 0; i <= ordered->size; i++) {
      id = (int) ordered->space[i];
      sat_heap_insert(cm, cm->variableHeap, i);
    }
  }
#endif
  
  free(litArr);
}

/**Function********************************************************************

  Synopsis    [Variable ording for sat decision]
  
  Description [Order variables for sat decision]

  SideEffects []

  SeeAlso     []

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

satArray_t *
smt_get_decision_order(smtManager_t * sm)
{
  satManager_t * cm = sm->cm;
  smtAvar_t * avar;
  smtBvar_t * bvar;
  satArray_t * idArr = sat_array_alloc(sm->id2var->size);
  int id, i;

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

  for(i = 0; i < sm->avarArr->size; i++) {
    avar = (smtAvar_t *) sm->avarArr->space[i];
    idArr = sat_array_insert(idArr, avar->id);
  }

  for(i = 0; i < idArr->size; i++) {
    id = (int) idArr->space[i];
    cm->activity[id] = (double) idArr->size-i;
  }

  return idArr;
}

#endif