//---------------------------------------------------------------------------
#include <stdio.h>  // printf
#include <stdlib.h> // atoi
#include <string.h>
#include <limits.h> // INT_MAX
#include <time.h>
#include <sys/timeb.h>

//---------------------------------------------------------------------------
#include "main.h"
#include "tboolfnct.h"
#include "checks.h"
#include "decomp.h"
#include "cd.h"
#include "ie.h"
#include "ir.h"
#include "cover.h"
#include "bufferstruct.h"
#include "implcheck.h"
#include "fcmin.h"
#include "boom.h"


//---------------------------------------------------------------------------

Boom::Boom()
{
  this->mo = new MinimizeOptions;
  mo->STOP_time = 0;
  mo->STOP_iterations = 1;
  mo->STOP_optimization = 0;
  mo->STOP_improvement = 0;
  mo->STOP_maxtime = 1;
  mo->STOP_maxiterations = 1;
  mo->STOP_optimizationval = 0;
  mo->STOP_improvementint = 1;
  mo->OPT_crit = 1;
  mo->IE_type = 3;
  mo->IR_no = 0;
  mo->IR_mutations = 0;
  mo->COV_end = 0;
  mo->COV_somin = 0;
  mo->IC_type = 0;
  mo->IC_memory = 0;
  mo->OR_no = 0;
  mo->DOM_type = 2;
  mo->DECOMP_enable = 0;
  mo->DFT_enable = 0;
  strcpy( mo->not.NOT_multiply, "." );
  strcpy( mo->not.NOT_add, "+" );
  strcpy( mo->not.NOT_neg, "'" );
  mo->not.NOT_postneg = 1;
  mo->savevarnames = false;
  mo->dopts = new DecompositionOptions;
  mo->dopts->blocks = 1;
  mo->dopts->inps = new int[1];
  mo->dopts->inps[0] = INT_MAX;
  mo->dopts->outs = new int[1];
  mo->dopts->outs[0] = INT_MAX;
  mo->FC_DF_dir = 1;
  mo->FC_DF = 10;
  mo->CD_FC = 50;
  mo->cdopts = new CD_Opts;
  mo->CD_no = 0;
  mo->cdopts->CD_mutations = 0;
  mo->cdopts->CD_weights = 0;
  mo->cdopts->DECOMP_CDenable = 0;
  mo->cdopts->DECOMP_CD_force = 1;
  mo->cdopts->DECOMP_CD_loadforce = 0;
  mo->cdopts->DFT_CDenable = 0;
  mo->cdopts->DFT_CD_force = 1;
  mo->covopts = new Cov_Opts;
  mo->covopts->DECOMP_COVenable = 0;
  mo->covopts->DECOMP_COV_loadforce = 0;
  mo->covopts->DECOMP_COV_force = 1;
  mo->covopts->DFT_COVenable = 0;
  mo->covopts->DFT_COV_force = 1;
  mo->covopts->COV_type = 1;
  mo->covopts->endcov=0;
  mo->covopts->effort=5;
  mo->covopts->MaxRunTime = 0;
  mo->covopts->COV_substDC = 0;
}

Boom::~Boom()
{
    delete this->mo->cdopts;
    delete this->mo->covopts;
    delete this->mo->dopts;
    delete this->mo;
}


void Boom::InitBuffers( TBoolFnct * srcf )
{
  if ( mo->IC_type == 1 )
  {
    this->offtree = new TermTree * [srcf->outvars];
    for ( int i = 0; i < srcf->outvars; i++ ) this->offtree[i] = new TermTree( srcf );
  } else {
    this->offtree = new TermTree * [srcf->outvars];
    for ( int i = 0; i < srcf->outvars; i++ ) this->offtree[i] = 0;
  }
  if ( mo->IE_type > 0 )
  {
    this->i_buffer = new TermTree * [srcf->outvars];
    for ( int i = 0; i < srcf->outvars; i++ ) this->i_buffer[i] = new TermTree( srcf );
  }
  this->e_buffer = CreateHistory( srcf );
  this->primes_ie = new TermTree( srcf );
  this->imp_test = new TermTree * [srcf->outvars];
  for ( int i = 0; i < srcf->outvars; i++ ) this->imp_test[i] = new TermTree( srcf );

  if ( mo->IC_type == 1 )
    for ( int i = 0; i < srcf->outvars; i++ )
        offtree[i]->AddFnctToTreeHistory( srcf->offset[i] );
  this->r_buffer = NULL;
}

void Boom::DeleteBuffers( TBoolFnct * srcf )
{
  delete this->r_buffer;
  if ( mo->IE_type > 0 )
  {
    for (int i = 0; i < srcf->outvars; i++ ) delete this->i_buffer[i];
    delete this->i_buffer;
  }
  delete this->primes_ie;
  for (int i = 0; i < srcf->outvars; i++ )
  {
    delete this->imp_test[i];

  }
  delete this->imp_test;
  for (int i = 0; i < srcf->outvars; i++ ) delete this->offtree[i];
  delete this->offtree;
  delete this->e_buffer;
}

TBoolFnct * Boom::OneMinStep( TBoolFnct * srcf, TBoolFnct * allf )
{
//  fprintf ( stderr, "CDmin step started .. \n\n" );

  int i;
  TBoolFnct * minf1;

  gauge.NewGauge( "Processing output variables", srcf->outvars, 1 );

  for ( i = 0; i < srcf->outvars; i++ )
  {
#if (mintrck > 0)
    ftime( & tr_t );
#endif
    if ( mo->CD_no == 0 )
    {
      minf1 = CD_Min( srcf, i, mo->cdopts, mo->IC_memory, mo->IC_type, mo->IE_type, gauge, imp_test[i], offtree[i], i_buffer[i], e_buffer );
      delete minf1;
    }
    else if ( mo->IE_type == 0 || srcf->firstpass == 1 )
    {
      srcf->DumpOnset( e_buffer );
      srcf->firstpass = 0;
    }
#if (mintrck > 0)
    ftime( & tr_t1 );
    cd_time += ( ( double )tr_t1.time + ( double )tr_t1.millitm / 1000 )
         - ( ( double )tr_t.time + ( double )tr_t.millitm / 1000 );
    tr_t = tr_t1;
#endif
    minf1 = ImplExpand( e_buffer, i, mo->IE_type, mo->IC_memory, mo->IC_type, imp_test[i], offtree[i], primes_ie, gauge );
    #if (mintrck > 0)
    ftime( & tr_t1 );
    exp_time += ( ( double )tr_t1.time + ( double )tr_t1.millitm / 1000 )
         - ( ( double )tr_t.time + ( double )tr_t.millitm / 1000 );
    tr_t = tr_t1;
#endif
    ConstructValidOutputs( minf1, mo->IC_memory, mo->IC_type, imp_test, offtree );
#if (mintrck > 0)
    ftime( & tr_t );
#endif
    if ( minf1->outvars > 1 && mo->IR_no == 0 && mo->COV_somin == 0 ) MoReduce( minf1, gauge, mo->IR_mutations );
#if (mintrck > 0)
    ftime( & tr_t1 );
    red_time += ( ( double )tr_t1.time + ( double )tr_t1.millitm / 1000 )
         - ( ( double )tr_t.time + ( double )tr_t.millitm / 1000 );
    tr_t = tr_t1;
#endif
    FindCover( minf1, gauge );
    if ( mo->DOM_type > 0 ) SelfDominChk( minf1, gauge );
    //SaveFnct(minf1,"prim.pla");
    if ( allf == 0 )
    {
      allf = minf1;
      //allf = new TBoolFnct( minf1->inpvars, minf1->outvars, 0, minf1->type );
      //allf->operator=(*minf1);
    }
    else
    {
      if ( mo->DOM_type > 1 )
      {
        DominChk( allf, minf1, gauge );
        DominChk( minf1, allf, gauge );
      }
      allf->JoinFnct( minf1 );
      if ( mo->DOM_type == 1 ) DuplChk( allf, gauge );
    }
#if (mintrck > 0)
    ftime( & tr_t1 );
    dom_time += ( ( double )tr_t1.time + ( double )tr_t1.millitm / 1000 )
         - ( ( double )tr_t.time + ( double )tr_t.millitm / 1000 );
    tr_t = tr_t1;
#endif
    gauge.GaugeStep( i, 0 );
  }
  gauge.CloseGauge();
  return allf;
}
//---------------------------------------------------------------------------
TBoolFnct * Boom::OneFCMinStep( TBoolFnct * srcf, TBoolFnct * allf )
{
//  fprintf ( stderr, "FCmin step started .. \n\n" );

  TBoolFnct * minf1;

  minf1 = FCMinimize( srcf, mo->FC_DF_dir, mo->FC_DF, gauge );
  //  SubstOutDCs(minf1);
  FindCover( minf1, gauge );
  if ( allf == 0 )
  {
    allf = minf1;
  }
  else
  {
    if ( mo->DOM_type > 1 )
    {
      DominChk( allf, minf1, gauge );
      DominChk( minf1, allf, gauge );
    }
    allf->JoinFnct( minf1 );
    if ( mo->DOM_type == 1 ) DuplChk( allf, gauge );
  }
  return allf;
}

//---------------------------------------------------------------------------

TBoolFnct * Boom::Minimize( TBoolFnct * srcf )
{
  struct timeb t, t1;
  FnctInfo inf1;

  TBoolFnct * minf1, * minf;
  time_t tr;
  int stop;
  int crit;
  int lpass, lpass2;
  int dtrm;
  int i;
  int c1, c2, c3, st_tmp;

#if (mintrck > 0)
  int ch[30];
  FILE * f, * f1, * f2, * f3;
#endif

  // decomp
  mo->DECOMP_enable = 0;
  mo->cdopts->DECOMP_CDenable = 0;
  mo->covopts->DECOMP_COVenable = 0;
  InitDecompAss( srcf, mo->dopts->blocks );
    
  srand(static_cast<unsigned>(time(0)));
  //srand( ( unsigned )time( & tr ) );
  //srand(2);
#if (mintrck > 0)
  f = fopen( "mintrck.dat", "wt" );
  f1 = fopen( "mintrck1.dat", "wt" );
  f2 = fopen( "mintrck_comp.dat", "wt" );
  f3 = fopen( "mintrck_distr.dat", "wt" );
  fprintf( f, "Cycle CD_time IE_time IR_time DC_time CP_time Sp_time Time Lits OC Terms All_terms Sol_PIs\n" );
  fprintf( f1, "Cycle CD_time +IE_time +IR_time +DC_time +CP_time +Sp_time Time Lits OC Terms All_terms Sol_PIs\n" );
  fprintf( f2, "Cycle All_terms All_PIs All_FCs All_comms CurSol_terms CurSol_PIs CurSol_FCs CurSol_comms BestSol_terms BestSol_PIs BestSol_FCs BestSol_comms CurSol_lits CurSol_OC CurSol_GEs BestSol_lits BestSol_OC BestSol_GEs\n" );
  fprintf( f3, "Cycle [All terms] [Current Solution] [Best Solution]\n" );
  fprintf( f3, "BOOM_PIs common_PIs FC_PIs BOOM_npi common_npi FC_npi\n" );
  fprintf( f3, "allf_BOOM_PIs allf_common_PIs allf_FC_PIs allf_BOOM_npi allf_common_npi allf_FC_npi cursol_BOOM_PIs cursol_common_PIs cursol_FC_PIs cursol_BOOM_npi cursol_common_npi cursol_FC_npi bestsol_BOOM_PIs bestsol_common_PIs bestsol_FC_PIs bestsol_BOOM_npi bestsol_common_npi bestsol_FC_npi\n" );
#endif

  info.cyc = 0;

  minf = 0;

  srcf->SplitFnct();

  InitBuffers( srcf );

  //MinimizeOffset(ssrcf);
                        
  ftime( & t );
  lpass = 1;
  lpass2 = 1;
  srcf->firstpass = 1;
#if (mintrck > 0)
  cd_time = 0;
  exp_time = 0;
  red_time = 0;
  dom_time = 0;
  cov_time = 0;
  sprs_time = 0;
  ftime( & tr_t );
#endif
  if ( mo->DECOMP_enable == 1 )
    if ( AssignValidOutputs( srcf, mo->dopts ) == 1 ) return 0;

  if ( mo->STOP_time == 1 && mo->STOP_iterations == 0 )
    gauge.NewGauge( "Minimizing using BOOM...", mo->STOP_maxtime, 1 );
  else if ( mo->STOP_iterations == 1 && mo->STOP_time == 0 )
    gauge.NewGauge( "Minimizing...", mo->STOP_maxiterations, 1 );
  else
    gauge.NewGauge( "Minimizing...", 0, 1 );
  do
  {
    if ( mo->DECOMP_enable == 1 )
    {
      RandomAssignValidOutputs( srcf, mo->dopts );
      CleanInpAssignment( srcf );
    }
    info.cyc++;
    if ( r_buffer == 0 ) dtrm = 0;
    else dtrm = r_buffer->terms;
    if ( ( random( 100 ) + 1 ) > mo->CD_FC ) r_buffer = OneMinStep( srcf, r_buffer );
    else
      r_buffer = OneFCMinStep( srcf, r_buffer );
    dtrm = r_buffer->terms - dtrm;
#if (mintrck > 0)
    ftime( & tr_t );
#endif
    if ( mo->COV_end == 0 && dtrm > 0 )
    {
      if ( mo->DECOMP_enable == 1 ) minf1 = BlockCover( r_buffer, mo->covopts, gauge, mo->dopts->blocks );
      else
      {
        if ( mo->COV_somin == 0 ) minf1 = Cover( r_buffer, gauge, mo->covopts );
        else
          minf1 = SOCover( r_buffer, mo->covopts, gauge );
      }
    }
    info.tries = r_buffer->tries;
    info.F_hits = r_buffer->hits;
#if (mintrck > 0)
    ftime( & tr_t1 );
    cov_time += ( ( double )tr_t1.time + ( double )tr_t1.millitm / 1000 )
         - ( ( double )tr_t.time + ( double )tr_t.millitm / 1000 );
    tr_t = tr_t1;
#endif
    if ( mo->OR_no == 0 && srcf->outvars > 1 && mo->COV_end == 0 && mo->COV_somin == 0 && dtrm > 0 ) {
        SparseOutput( minf1, mo->covopts, gauge );
        SparseInput( minf1, mo->IC_memory, mo->IC_type, imp_test, offtree, gauge );
    }

#if (mintrck > 0)
    ftime( & tr_t1 );
    sprs_time += ( ( double )tr_t1.time + ( double )tr_t1.millitm / 1000 )
         - ( ( double )tr_t.time + ( double )tr_t.millitm / 1000 );
    tr_t = tr_t1;
#endif
    //EssentialCheck(minf1,i,mo);
/*
#if (mintrck > 0)
    if ( minf == 0 )
    {
      st_tmp = 1;
      minf = minf1;
    }
    else
      st_tmp = 0;
    if ( dtrm > 0 && info.cyc > 1 )
    {
      GetInfo( minf1 );
      GetInfo( minf );
      fprintf( f2, "%i %i %i %i %i %i %i %i %i %i %i %i %i %i %i %i %i %i %i\n", info.cyc, info.allf->terms, CountPrimes( info.allf->fnct ),
           CountFCs( info.allf->fnct ), CountCommons( info.allf->fnct ), minf1->terms, CountPrimes( minf1->fnct ), CountFCs( minf1->fnct ),
           CountCommons( minf1->fnct ), minf->terms, CountPrimes( minf->fnct ), CountFCs( minf->fnct ), CountCommons( minf->fnct ),
           minf1->info.liters, minf1->info.ON_terms, minf1->info.GEs, minf->info.liters, minf->info.ON_terms, minf->info.GEs );
      fflush( f2 );
      ch[1] = AdvCountPrimes( info.allf, 3 );
      ch[0] = AdvCountPrimes( buffers->r_buffer, 1 ) - ch[1];
      ch[2] = AdvCountPrimes( buffers->r_buffer, 2 ) - ch[1];
      ch[4] = CountCommons( buffers->r_buffer->fnct ) - ch[1];
      ch[5] = CountFCs( buffers->r_buffer->fnct ) - ch[1] - ch[2] - ch[4];
      ch[3] = buffers->r_buffer->terms - ch[0] - ch[1] - ch[2] - ch[4] - ch[5];
      ch[11] = AdvCountPrimes( minf1, 3 );
      ch[10] = AdvCountPrimes( minf1, 1 ) - ch[11];
      ch[12] = AdvCountPrimes( minf1, 2 ) - ch[11];
      ch[14] = CountCommons( minf1->fnct ) - ch[11];
      ch[15] = CountFCs( minf1->fnct ) - ch[11] - ch[12] - ch[14];
      ch[13] = minf1->terms - ch[10] - ch[11] - ch[12] - ch[14] - ch[15];
      ch[21] = AdvCountPrimes( minf, 3 );
      ch[20] = AdvCountPrimes( minf, 1 ) - ch[21];
      ch[22] = AdvCountPrimes( minf, 2 ) - ch[21];
      ch[24] = CountCommons( minf->fnct ) - ch[21];
      ch[25] = CountFCs( minf->fnct ) - ch[21] - ch[22] - ch[24];
      ch[23] = minf->terms - ch[20] - ch[21] - ch[22] - ch[24] - ch[25];
      fprintf( f3, "%i %i %i %i %i %i %i %i %i %i %i %i %i %i %i %i %i %i %i\n", info.cyc, ch[0], ch[1], ch[2], ch[3], ch[4],
           ch[5], ch[10], ch[11], ch[12], ch[13], ch[14], ch[15], ch[20], ch[21], ch[22], ch[23], ch[24], ch[25] );
      fflush( f3 );
    }
    if ( st_tmp ) minf = 0;
#endif
*/
    if ( mo->COV_end != 1 && dtrm > 0 )
    {
      minf1->GetInfo();
      minf1->GetOptVal( mo->OPT_crit );
      if ( minf == 0 )
      {
        minf = minf1;
        if ( mo->DECOMP_enable == 1 ) minf->decomp = DuplicateDecompAss( srcf, mo->dopts );
      }
      else
      {
        if ( minf1->optval < minf->optval )
        {
          if ( mo->DECOMP_enable == 1 ) DestroyDecompAss( minf );
          delete minf;
          minf = minf1;
          if ( mo->DECOMP_enable == 1 ) minf->decomp = DuplicateDecompAss( srcf, mo->dopts );
          lpass2 = info.cyc - lpass;
          lpass = info.cyc;
        }
        else
          delete minf1;
      }
    }
    ftime( & t1 );
    info.tm = ( ( double )t1.time + ( double )t1.millitm / 1000 ) - ( ( double )t.time + ( double )t.millitm / 1000 );
    stop = true;
    if ( stop && mo->STOP_time ) stop = ( info.tm <= mo->STOP_maxtime );
    if ( stop && mo->STOP_iterations ) stop = ( info.cyc < mo->STOP_maxiterations );
    if ( stop && mo->STOP_optimization ) stop = ( minf->optval > mo->STOP_optimizationval );
    if ( stop && mo->STOP_improvement ) stop = ( info.cyc < lpass + lpass2 * mo->STOP_improvementint );
    if ( mo->DECOMP_enable ) CountAssignment( minf );
#if (mintrck > 0)
    fprintf( f, "%i %.3f %.3f %.3f %.3f %.3f %.3f %.3f %i %i %i %i %i\n", info.cyc, cd_time, exp_time, red_time, dom_time,
         cov_time, sprs_time, info.tm, buffers->minf->info.liters, buffers->minf->info.ON_terms,
         buffers->minf->info.groupterms, buffers->r_buffer->terms, buffers->minf->info.primes );
    fprintf( f1, "%i %.3f %.3f %.3f %.3f %.3f %.3f %.3f %i %i %i %i %i\n", info.cyc, cd_time, cd_time + exp_time,
         cd_time + exp_time + red_time, cd_time + exp_time + red_time + dom_time,
         cd_time + exp_time + red_time + dom_time + cov_time, cd_time + exp_time + red_time + dom_time + cov_time + sprs_time,
         info.tm, buffers->minf->info.liters, buffers->minf->info.ON_terms, buffers->minf->info.groupterms,
         buffers->r_buffer->terms, buffers->minf->info.primes );
#endif
#if (mintrck == 2)
    cd_time = 0;
    exp_time = 0;
    red_time = 0;
    dom_time = 0;
    cov_time = 0;
    sprs_time = 0;
    ftime( & tr_t );
#endif

    if ( mo->STOP_time == 1 ) i = gauge.GaugeStep( info.tm, 1 );
    else if ( mo->STOP_iterations == 1 ) i = gauge.GaugeStep( info.cyc, 1 );
    else
      i = gauge.GaugeStep( 0, 1 );
    if ( i != 0 ) stop = false;
  }
  while ( stop );
  if ( mo->COV_end == 1 ) {
    if ( mo->covopts->DECOMP_COVenable == 1 ) minf = BlockCover( r_buffer, mo->covopts, gauge, mo->dopts->blocks );
    else if ( mo->COV_somin == 0 ) minf = Cover( r_buffer, gauge, mo->covopts );
    else
      minf1 = SOCover( r_buffer, mo->covopts, gauge );
    if ( mo->OR_no == 0 && srcf->outvars > 1 && mo->COV_somin == 0 ) {
        SparseOutput( minf, mo->covopts, gauge );
        SparseInput( minf, mo->IC_memory, mo->IC_type, imp_test, offtree, gauge );
    }
    minf->GetInfo();
  }

  DeleteBuffers( srcf );
#if (mintrck > 0)
  fclose( f );
  fclose( f1 );
  fclose( f2 );
  fclose( f3 );
#endif
  gauge.CloseGauge();

  //IsolateFunction(minf);

  return minf;
}

