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

//---------------------------------------------------------------------------
#include "conf.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"


//---------------------------------------------------------------------------
#include "../modulemanager/modulemanager.h"
#include "../modulemanager/imodule.h"
#include "../modulemanager/messageclass.h"
#include "../modulemanager/varinst.h"
#include "../exceptions/exceptions.h"

string BoomLoader::name="boom";

Ptr<VarDef> BoomLoader::variables[]=
{
	new VarDef("FR","Define FC-Min:CD-search ratio n (0-100), 0 is default",VarDef::VAR_INT,"0"),
	new VarDef("DF","Define the FC-Min Depth Factor, 10 is default",VarDef::VAR_INT,"10"),
	new VarDef("DD","Define the FC-Min Depth Factor Direction\n0   DF = 1:n (from -DFn)\n1   DF = n:1 (from -DFn), default",VarDef::VAR_INT,"1"),
	new VarDef("CM","Define CD-search mutations ratio n (0-100)",VarDef::VAR_INT,"0"),
	new VarDef("RM","Define implicant reduction mutations ratio n (0-100)",VarDef::VAR_INT,"0"),
	new VarDef("E" ,"Select implicant expansion type:\n0   Sequential search\n1   Distributed multiple IE\n2   Distributed exhaustive IE\n3   Multiple IE (default)\n4   Exhaustive IE\n",VarDef::VAR_INT,"3"),
	new VarDef("CP","Select the covering problem solution algorithm:\n0   LCMC\n1   Contributive selection (default)\n2   Contributive removal\n3   Exact cover\n",VarDef::VAR_INT,"1"),
	new VarDef("SV","Define stopping on value n (default 1)",VarDef::VAR_INT,"1"),
	new VarDef("ST","Define type of stop\nt   stop after n seconds\ni   stop after n iterations (default)\nn   stopping interval equal to n\nq   stop when quality of solution meets n\n",VarDef::VAR_CHAR,"i"),
	new VarDef("Q","Define optimization criterion x:\nt   terms\nl   literals\no   output cost\nb   literals+output cost (default)\ng   number of gates\nG   number of gate equivalents",VarDef::VAR_CHAR,"b"),
	new VarDef("single","Single-output minimization",VarDef::VAR_BOOL),
	new VarDef("endcov","Cover at the end only",VarDef::VAR_BOOL),
	new VarDef("SD","Substitute output don't cares",VarDef::VAR_BOOL),
	new VarDef("O","Define output format\nP   PLA (default)\nV   VHDL\nv   Verilog\nB   BLIF\nE   Equations\nH   HTML (table)\n",VarDef::VAR_CHAR,"P"),
	new VarDef("nocheck","Don't check the input function for consistence",VarDef::VAR_BOOL),
	new VarDef("namevars","Implicitly name the variables",VarDef::VAR_BOOL),
	new VarDef("input","Defines input function",VarDef::VAR_STRING),
	new VarDef("output","Defines output name",VarDef::VAR_STRING),
	new VarDef("oper","Defines implicit operation :\n0 - default\n1 - info\n2 - nocheck\n3 - Tcheck\n4 - Tsplit\n5 - Tminterm\n",VarDef::VAR_INT,"0"),

/*
  fprintf( stderr, "Special Functions (cannot be combined with minimization):\n" );
  fprintf( stderr, "    -info        Prints the information about the PLA function (for fd type only)\n" );
  fprintf( stderr, "    -Tcheck      Checks the input function for consistence\n" );
  fprintf( stderr, "    -Tsplit      Splits intersecting terms\n" );
  fprintf( stderr, "    -Tminterm    Splits function into minterms\n" );
*/
	0
};

Ptr<Command> BoomLoader::commands[]=
{
	0
};

class MyButtonReleaseListener:public ButtonReleaseListener
{
	Ptr<TkEntry> entryInput,entryOutput;
public:
	MyButtonReleaseListener(TkEntry* entryInput,TkEntry* entryOutput)
	{
		this->entryInput=entryInput;
		this->entryOutput=entryOutput;
	}
	void onButtonRelease(EHeader& header,int button,const string& state,int x,int y,int x_root,int y_root)
	{
		if (header.source->getName()=="butInput")
		{
			entryInput->setText(TkDialogs::createOpenDialog(TclInterp::defaultInterp));
		}
		if (header.source->getName()=="butOutput")
		{
			map<string,string> types;

			types["PLA file"]=".pla";
			types["VHDL file"]=".vhdl";
			types["Verilog file"]=".v";
			types["BLIF file"]=".blif";
			types["Equations file"]=".equ";
			types["HTML table"]=".html";

			entryOutput->setText(TkDialogs::createSaveDialog(TclInterp::defaultInterp,".pla",types,"","Select file for output"));
		}
	}
};

class MyExpansionType:public TclVarListener
{
	Boom* boom;
	TkSpinBox* spinbox;
	VarInst* var;
public:
	MyExpansionType(Boom* boom,TkSpinBox* spinbox,VarInst* var):boom(boom),spinbox(spinbox),var(var)
	{
	}
	virtual void valueUpdated(TclVar* variable)
	{
		VarInteger* intVar=(VarInteger*)var;
		intVar->set(spinbox->getValuesIndex());
	}
};

class MySolutionAlgol:public TclVarListener
{
	Boom* boom;
	TkSpinBox* spinbox;
	VarInst* var;
public:
	MySolutionAlgol(Boom* boom,TkSpinBox* spinbox,VarInst* var):boom(boom),spinbox(spinbox),var(var)
	{
	}
	virtual void valueUpdated(TclVar* variable)
	{
		VarInteger* intVar=(VarInteger*)var;
		intVar->set(spinbox->getValuesIndex());
	}
};

class MyStopType:public TclVarListener
{
	Boom* boom;
	TkSpinBox* spinbox;
	VarInst* var;
public:
	MyStopType(Boom* boom,TkSpinBox* spinbox,VarInst* var):boom(boom),spinbox(spinbox),var(var)
	{
	}
	virtual void valueUpdated(TclVar* variable)
	{
		VarChar* varChar=(VarChar*)var;
		switch(spinbox->getValuesIndex())
		{
			case 0:
				varChar->set('t');
				break;
			case 1:
				varChar->set('i');
				break;
			case 2:
				varChar->set('n');
				break;
			case 3:
				varChar->set('q');
				break;
		}
	}
};

class MyOptiCriteriumType:public TclVarListener
{
	Boom* boom;
	TkSpinBox* spinbox;
	VarInst* var;
public:
	MyOptiCriteriumType(Boom* boom,TkSpinBox* spinbox,VarInst* var):boom(boom),spinbox(spinbox),var(var)
	{
	}
	virtual void valueUpdated(TclVar* variable)
	{
		VarChar* varChar=(VarChar*)var;
		switch(spinbox->getValuesIndex())
		{
			case 0:
				varChar->set('l');
				break;
			case 1:
				varChar->set('o');
				break;
			case 2:
				varChar->set('b');
				break;
			case 3:
				varChar->set('g');
				break;
			case 4:
				varChar->set('g');
				break;
		}
	}
};

class MyButtonOkListener:public ButtonReleaseListener
{
	Boom* boom;
public:
	MyButtonOkListener(Boom* boom)
	{
		this->boom=boom;
	}
	void onButtonRelease(EHeader& header,int button,const string& state,int x,int y,int x_root,int y_root)
	{
		boom->run();
	}
};


void Boom::afterInstantiate()
{
	Ptr<TkTopLevel> sourceWindow=getManager()->getGui()->getSourceForm("boom");
	if (sourceWindow.isNull()) return;
	window=(TkTopLevel*)sourceWindow->clone();
	window->create();
	window->doLayout();
	window->setWindowState(TkWinStateOption::normal);
	window->setTitle(string("boom ")+getName());
	window->attachToModule(this);

	TkEntry* entryInput=(TkEntry*)window->getChildByName("txtInput");
	TkEntry* entryOutput=(TkEntry*)window->getChildByName("txtOutput");

	TkButton* butInput=(TkButton*)window->getChildByName("butInput");
	TkButton* butOutput=(TkButton*)window->getChildByName("butOutput");

	MyButtonReleaseListener* rl=new MyButtonReleaseListener(entryInput,entryOutput);
	butInput->addButtonReleaseListener(rl);
	butOutput->addButtonReleaseListener(rl);

	TkSpinBox* expansionType=(TkSpinBox*)window->getChildByName("E");
	expansionType->addValueListener(new MyExpansionType(this,expansionType,getVariable("E")));
	
	TkSpinBox* solutionAlgol=(TkSpinBox*)window->getChildByName("CP");
	solutionAlgol->addValueListener(new MySolutionAlgol(this,solutionAlgol,getVariable("CP")));
	
	TkSpinBox* stopType=(TkSpinBox*)window->getChildByName("ST");
	stopType->addValueListener(new MyStopType(this,stopType,getVariable("ST")));
	
	TkSpinBox* optiCriterium=(TkSpinBox*)window->getChildByName("Q");
	optiCriterium->addValueListener(new MyOptiCriteriumType(this,optiCriterium,getVariable("Q")));

	TkRadioButton* dir1n=(TkRadioButton*)window->getChildByName("dir1n");
	TkRadioButton* dirn1=(TkRadioButton*)window->getChildByName("dirn1");

	TkButton* butOK=(TkButton*)window->getChildByName("butOk");
	butOK->addButtonReleaseListener(new MyButtonOkListener(this));
}

void Boom::receiveMessage(TObject* mesg)
{
	if (!mesg->typeOf(MesgVarChange::type)) return;
	const VarInst* varInst=((MesgVarChange*)mesg)->variable;
	const VarDef* varDef=varInst->getVarDef();

	
	if (strcmp(varDef->getName(),"FR")==0) mo->CD_FC=toInt(varInst);
	if (strcmp(varDef->getName(),"DF")==0) mo->FC_DF=toInt(varInst);
	if (strcmp(varDef->getName(),"DD")==0) mo->FC_DF_dir=toInt(varInst);
	if (strcmp(varDef->getName(),"SV")==0||strcmp(varDef->getName(),"ST")==0)
	{
		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;
		VarChar* varST=((VarChar*)(*this)["ST"]);
		int valST=toInt((*this)["SV"]);
		switch (varST->get())
		{
            case 't':
				mo->STOP_time = 1;
				mo->STOP_maxtime = valST;
			break;
			case 'i':
				mo->STOP_iterations = 1;
				mo->STOP_maxiterations = valST;
			break;
            case 'n':
				mo->STOP_improvement = 1;
				mo->STOP_improvementint = valST;
            break;
            case 'q':
				mo->STOP_optimization = 1;
				mo->STOP_optimizationval = valST;
            break;
            case 'D':
				mo->covopts->COV_substDC = 1;
            break;
		}
	}
	if (strcmp(varDef->getName(),"Q")==0)
	{
		switch(toChar(varInst))
		{
			case 't':
				mo->OPT_crit = 0;
			break;
			case 'l':
				mo->OPT_crit = 1;
            break;
            case 'o':
				mo->OPT_crit = 2;
            break;
            case 'b':
				mo->OPT_crit = 3;
            break;
            case 'g':
				mo->OPT_crit = 4;
            break;
            case 'G':
				mo->OPT_crit = 5;
            break;
		}
	}
	if (strcmp(varDef->getName(),"CM")==0) mo->cdopts->CD_mutations=toInt(varInst);
	if (strcmp(varDef->getName(),"CP")==0) mo->covopts->COV_type=toInt(varInst);
	int of=0;
	if (strcmp(varDef->getName(),"O")==0)
	{
		switch(toChar(varInst))
		{
			case 'P':
				of = 0;
            break;
            case 'V':
				of = 1;
            break;
            case 'v':
				of = 2;
            break;
            case 'B':
				of = 3;
            break;
            case 'E':
				of = 4;
            break;
            case 'H':
				of = 5;
            break;
            default:
				throw new Exception("boom","Invalid value %c",toChar(varInst));
			break;
		}
	}
	if (strcmp(varDef->getName(),"RM")==0)
	{
		mo->IR_mutations=toInt(varInst);
	}
	if (strcmp(varDef->getName(),"E")==0)
	{
		mo->IE_type=toInt(varInst);
	}
	if (strcmp(varDef->getName(),"endcov")==0)
	{
		mo->COV_end=toBool(varInst)?1:0;
	}
	if (strcmp(varDef->getName(),"single")==0)
	{
		mo->COV_somin=toBool(varInst)?1:0;
	}
	if (strcmp(varDef->getName(),"namevars")==0)
	{
		mo->savevarnames=toBool(varInst);
	}
	if (strcmp(varDef->getName(),"input")==0)
	{
		/// TOHLE BY MELA BYT STATICKA METODA TAKHLE JE TO DOST PRASARNA
		char* name=const_cast<char*>(::toString(varInst));
		if (name[0]=='\0') return;
		srcf=srcf->LoadFnct(name,gauge);
		if (srcf==0) throw new ExceptionIO(name,true);
	}
	if (strcmp(varDef->getName(),"oper")==0)
	{
		op=toInt(varInst);
	}
}

static void Save(TBoolFnct *srcf, const char *cfn, int of, TGauge gauge,Notation notation, bool savevarnames)
{
    char* fn=const_cast<char*>(cfn);
	switch (of)
    {
        case 0: srcf->SaveFnct(fn, gauge, savevarnames);
                break;
        case 1: srcf->SaveFnctAsVHDL(fn, gauge);
                break;
        case 2: srcf->SaveFnctAsVerilog(fn, gauge);
                break;
        case 3: srcf->SaveFnctAsBLIF(fn, gauge);
                break;
        case 4: srcf->SaveFnctAsSymbols(fn, gauge, notation);
                break;
        case 5: srcf->SaveFnctAsHTML(fn, gauge);
                break;
    }
}

void Boom::run()
{
	gauge.NewGauge = Boom::NewGauge;
	gauge.CloseGauge = Boom::CloseGauge;
	gauge.GaugeStep = Boom::GaugeStep;

	const char* onm=((VarString*)((*this)["output"]))->get().c_str();
	TBoolFnct* minf;
    InitDecompAss( srcf, mo->dopts->blocks );
    if ( srcf->type == 1 ) fprintf( stderr, "Function type: fr\n" );
    else
      fprintf( stderr, "Function type: fd\n" );
    fprintf( stderr, "Input variables: %i\n", srcf->inpvars );
    fprintf( stderr, "Output variables: %i\n", srcf->outvars );
    fprintf( stderr, "Defined terms: %i\n", srcf->terms );
    fprintf( stderr, "\n" );
    switch ( op )
    {
      case 0:
        if ( mo->CD_FC > 100 )
        {
          fprintf( stderr, "CD-Search:FC-Min ratio must be between 0-100\n" );
          exit( 1 );
        }
        if ( mo->FC_DF_dir > 1 )
        {
          fprintf( stderr, "FC-Min DF direction must be 0 or 1\n" );
          exit( 1 );
        }
        if ( mo->cdopts->CD_mutations > 100 )
        {
          fprintf( stderr, "Number of mutations must be less of equal to 100%\n" );
          exit( 1 );
        }
        if ( mo->IR_mutations > 100 )
        {
          fprintf( stderr, "Number of mutations must be less of equal to 100%\n" );
          exit( 1 );
        }
        if ( mo->covopts->COV_type > 100 )
        {
          fprintf( stderr, "Unknown CP solution method (%i)\n", mo->covopts->COV_type );
          exit( 1 );
        }
        if ( mo->IE_type > 100 )
        {
          fprintf( stderr, "Unknown IE method (%i)\n", mo->IE_type );
          exit( 1 );
        }
        if ( mo->OPT_crit > 5 )
        {
          fprintf( stderr, "Unknown optimization criterion (%i)\n", mo->OPT_crit );
          exit( 1 );
        }

        if ( mo->COV_end == 1 && ( mo->STOP_improvement == 1 || mo->STOP_optimization == 1 ) )
        {
          fprintf( stderr, "Cannot combine endcov parameter with optimization criteria based stopping condition\n" );
          exit( 0 );
        }
        if ( srcf->type != 1 )
        {
          fprintf( stderr, "Function must be fr type\n" );
          exit( 1 );
        }
        if ( mo->STOP_time == 0 && mo->STOP_iterations == 0 && mo->STOP_improvement == 0 && mo->STOP_optimization == 0 )
          mo->STOP_iterations = 1;

/*        if ( nocheck == 0 )
            if ( CheckConsist( srcf, gauge ) == 0 ) {
                fprintf( stderr, "Inconsistent function!\n" );
                return 1;
            }*/

        fprintf( stderr, "Minimizing...\n\n" );
        minf = Minimize( srcf );
        if ( minf == 0 )
        {
          fprintf( stderr, "Error occured during minimization\n" );
          return;
        }
        minf->GetInfo();
        fprintf( stderr, "Elapsed time: %.3f s\n", info.tm );
        fprintf( stderr, "Iterations: %i\n", info.cyc );
        fprintf( stderr, "Terms: %i\n", minf->info.groupterms );
        fprintf( stderr, "Literals: %i\n", minf->info.liters );
        fprintf( stderr, "Output cost: %i\n", minf->info.ON_terms );
        fprintf( stderr, "Gates: %i\n", minf->info.gates );
        fprintf( stderr, "GEs: %i\n", minf->info.GEs );
        fprintf( stderr, "\n" );
//        minf->SaveFnctAsBLIF_POS( onm );
//        srcf->SaveFnctAsBLIF( onm );
//        minf->SaveFnct( strcat(onm, ".pla"));
        Save(minf, onm, of, gauge, mo->notation, mo->savevarnames);
      break;
      case 1:
        srcf->GetInfo();
        printf( "Literals: %i\n", srcf->info.liters );
        printf( "Output cost: %i\n", srcf->info.ON_terms );
        if (srcf->type == 0) {
            printf( "Gates: %i\n", srcf->info.gates );
            printf( "GEs: %i\n", srcf->info.GEs );
        }
        printf( "\n" );
      break;
      case 2:
        if ( CheckConsist( srcf, gauge ) != 0 ) fprintf( stderr, "Function is consistent\n" );
        else
          fprintf( stderr, "Inconsistent function!\n" );
      break;
      case 3:
        if ( srcf->type != 1 )
        {
          fprintf( stderr, "Function must be fr type\n" );
          exit( 1 );
        }
        if ( NoIntersections( srcf, gauge ) == 0 )
        {
          fprintf( stderr, "Inconsistent function" );
          exit( 1 );
        }
        else
          fprintf( stderr, "OK\n" );
        Save(srcf, onm, of, gauge, mo->notation, mo->savevarnames);
      break;
      case 4:
        minf = SplitToMinterms( srcf, gauge);
        if ( minf == 0 )
        {
          fprintf( stderr, "Inconsistent function" );
          exit( 1 );
        }
        else
          fprintf( stderr, "OK\n" );
        Save(minf, onm, of, gauge, mo->notation, mo->savevarnames);
      break;
    }
}

Boom::Boom()
{
	gauge.NewGauge=Boom::NewGauge;
	gauge.CloseGauge=Boom::CloseGauge;
	gauge.GaugeStep=Boom::GaugeStep;
	r_buffer=0;
	
  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->notation.NOT_multiply, "." );
  strcpy( mo->notation.NOT_add, "+" );
  strcpy( mo->notation.NOT_neg, "'" );
  mo->notation.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->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;
}

