#include <cerrno>
#include <string>
#include <math.h>

#include "bmctool.hh"
#include "painless/painless-src/utils/Parameters.h"
#include "painless/painless-src/painless.h"
#include "src/solver/Preprocessor.hh"
#include "src/mc/NuSMV.hh"
#include "src/utils/trace.hh"


// Global main variables
int k;
string split;
int nb_leaf;
string tool;
string infile;
const char * filename_char;
EnvBMC * env;
SplitBMCFormula *splitter =  new SplitBMCFormula(env);


bool read_Filename()
{
	if( !split.compare("nr") )
	{
		splitter->read_dimacs_file( filename_char, env->opf );
	}
	else if ( !split.compare("b")   || !split.compare("br")  || !split.compare("bu") ||
				!split.compare("btn") || !split.compare("ntb") || !split.compare("n") )
	{
		splitter->read_NuSMV_dimacs_file(filename_char);
	}
	else
	{
		std::cerr << "c split parameter value is unknown. Couldn't read input file." << std::endl;
		exit(1);
	}
	return true;
}

bool run_Conversion(bool store_in_splitter=false)
{
	int prop_verify = Parameters::getIntParam("prop",2);

	// with .smv extension
	if( (tool.compare("c") == 0) )
	{
		assert(k > 0);

		// Remove filename extension smv extension if exists
		Parameters::removeExtensionFromFilename(".smv");

		// Create Model
		ModelChecker* mctool;
		mctool = new NuSMV(filename_char, env, store_in_splitter ? splitter : nullptr);

		// Convert SMV instance to CNF formula
		clock_t t1 = clock();
		mctool->generate_cnf_formula(k, prop_verify);
		t1 = clock() - t1;

		env->opf << "c CONVERSION TO CNF FORMAT : " << ((float)t1)/CLOCKS_PER_SEC << endl;

		std::cout<< "s SATISFIABLE" << std::endl;

		delete mctool;

		return true;
	}
	return false;
}

bool run_Painless()
{
	// int nb_simp_solvers = Parameters::getIntParam("nsolvers",0);
	std::vector< std::vector< SolverInterface *> > special_solvers;

	if ( (tool.compare("p") == 0) &&
	         ((infile.find(".cnf")    != std::string::npos) ||
		      (infile.find(".dimacs") != std::string::npos)) )
	{
		// Extract k value from input filename
		if( k == -1 )
		{
			k = getKinString(infile);
			Parameters::setIntParam("k",k);
		}
		if( k == 0 )
		{
			std::cerr << "c Bound k was not provided." << std::endl;
			exit(3);
		}
		if( nb_leaf == -1 )
		{
			nb_leaf = ceil(k/3.);
			Parameters::setIntParam("nleafs",nb_leaf);
		}

		read_Filename();

		if( env->max_vars == 0 )
		{
			env->opf  << "s UNSATISFIABLE\n" << endl;
			std::cout << "s UNSATISFIABLE\n" << endl;
			return true;
		}

		// Preprocess solvers (split problem, affect each partition to a solver,...)
		// env->preprocess = new Preprocessor(env, splitter, false);
		Preprocessor::preprocessing(splitter, false);
		// If preprocessing didn't terminate well
		if( globalEnding )
		{
			env->opf  << "s UNSATISFIABLE\n" << endl;
			std::cout << "s UNSATISFIABLE\n" << endl;
			return true;
		}
		else
		{
			// Get solvers that has been created
			special_solvers = Preprocessor::getSolvers();
		}

		clock_t t1 = clock();
		run_painless_strategy(special_solvers, env->opf);
		t1 = clock() - t1;

		env->opf <<"c "<< endl;
		env->opf <<"c TOTAL RESOLUTION TIME : " << ((float)t1)/CLOCKS_PER_SEC << endl << endl;

		Preprocessor::cleanAll(splitter);
		return true;
	}

	return false;
}


bool run_BMCStrat()
{
	// BMCTOOL
	if( tool.compare("b") == 0 )
	{
		// .smv input file
		if( run_Conversion(true) )
		{
			std::cout << "c Conversion done successfully.\n";
		}
		// .cnf or .dimacs input file
		else if( (infile.find(".cnf") != std::string::npos) || (infile.find(".dimacs") != std::string::npos) )
		{
			splitter->read_dimacs_file(filename_char, env->opf );
		}

		// DIMACS variables is empty, nusmv has already deduce UNSATisfiability
		if( env->max_vars == 0 )
		{
			env->opf << "s UNSATISFIABLE\n" << endl;
			std::cout << "c Problem is already unsatisfiable : variables set is empty\n";
			std::cout << "s UNSATISFIABLE" << std::endl;
			return true;
		}

		// Preprocess solvers (split problem, affect each partition to a solver,...)
		Preprocessor::preprocessing(splitter, true);
		WorkingStrategy *wk_bmc = Preprocessor::getWorkingStratBMC();
		// Start resolution
		clock_t t1 = clock();
		run_bmc_strategy(wk_bmc, env->opf);
		t1 = clock() - t1;

		env->opf <<"c "<< endl;
		env->opf <<"c TOTAL RESOLUTION TIME : " << ((float)t1)/CLOCKS_PER_SEC << endl << endl;

		Preprocessor::cleanAll(splitter);
		return true;
	}
	return false;
}



int main(int argc, char ** argv)
{
	// Init parameters
	Parameters::init(argc,argv);

	if( argc < 2 || Parameters::isSet("h") )
	{
	    std::cerr << "Missing parameters. At least provide : " << std::endl;
		std::cout << "USAGE: " << argv[0] << " -k= [parameters] filename" << std::endl;
		std::cout << "Parameters:" << std::endl;
		std::cout << "\tfilename    : Filename problem without extension." << std::endl;
		std::cout << "\t-k int \t    : Bound for the transition relation (bound 0 included : k+1)." << std::endl;
		std::cout << "\t-t int \t    : timeout (default none)." << std::endl;
		std::cout << "\t-max-memory : memory limit (default none)." << std::endl;
		std::cout << "\t-tool       : " << std::endl;
		std::cout << "\t    c : Convert SMV instance into DIMACS. " << std::endl;
		std::cout << "\t    b : Run BMCTool strategies." << std::endl;
		std::cout << "\t    p : Run Painless strategies" << std::endl;
		std::cout << std::endl;
		std::cout << "\t Only {c} : " << std::endl;
		std::cout << "\t    -conv int \t   : Conversion algorithm (0 : Tseitin, 1 : Sheridan, default is 0)." << std::endl;
		std::cout << "\t    -prop int \t   : Property to verify   (0 : TRUE property,\
									\n\t\t\t\t\t\t   1 : random property,\
									\n\t\t\t\t\t\t   2 actual property in .smv file,\
									\n\t\t\t\t\t\t   default is 2)." << std::endl;

		std::cout << "\t Only {b} : " << std::endl;
		std::cout << "\t    -strategy int   : BMC Working strategy (0 : CONTINUE EVEN IF CHILD RETURNS UNSAT,\
									\n\t\t\t\t\t\t    1 : STOP WHEN CHILDREN OF SAME LEVEL RETURN UNSAT,\
									\n\t\t\t\t\t\t    2 : STOP AT FIRST UNSAT CHILD,\
									\n\t\t\t\t\t\t    3 : RUN HAMMADI WITH PAINLESS VERSION,\
									\n\t\t\t\t\t\t    default is 0)." << std::endl;

		std::cout << "\t Only {b,p} : " << std::endl;
		std::cout << "\t    -nleafs int    : Number of leafs/partitions (default is 1)." << std::endl;
		std::cout << "\t    -c int \t   : Number of cpus (default is 1)." << std::endl;
		std::cout << "\t    -s int \t   : special solver name (periplo, desat)." << std::endl;
		std::cout << "\t    -stats int \t   : Statitics (1 : decomposition, 2 : output filtered clause interpolation, default is 0 for off)." << std::endl;
		std::cout << "\t    -o 	 \t   : output file of the form  filename_k_X.out" << std::endl;
		std::cout << "\t    -ns int \t   : Number of solvers when running portfolio, (default is 0)." << std::endl;
		std::cout << "\t    -split int \t   : Decomposition strategy (b : Binary tree w BMC decomposition,\
									\n\t\t\t\t\t\t     bu : Binary tree w unbalanced decomposition,\
									\n\t\t\t\t\t\t     br : Binary tree w random decomposition,\
									\n\t\t\t\t\t\t     n  : N-ary tree w BMC decomposition,\
									\n\t\t\t\t\t\t     nr : N-ary tree decomposition (Hammadi algo),\
									\n\t\t\t\t\t\t     btn : Binary to n-ary tree decomposition,\
									\n\t\t\t\t\t\t     ntb : N-ary to binary tree decomposition,\
									\n\t\t\t\t\t\t     default is 0)." << std::endl;
	    return 0;
	}
	srand(0);

	// Initialize variables
	int stats_on		   = Parameters::getIntParam("stats",0);
	k 			  		   = Parameters::getIntParam("k", -1);
	split				   = Parameters::getParam("split", "b");
	nb_leaf 	 		   = Parameters::getIntParam("nleafs", 1);
	tool 			   	   = Parameters::getParam("tool","");
	infile   	   	 	   = Parameters::getFilename();
	filename_char 		   = infile.c_str();
	env 				   = new EnvBMC();
	splitter 			   = new SplitBMCFormula(env);

	// Set stdout
	if( stats_on )
	{
		string ouputname = infile+"_n"+to_string(nb_leaf)+"_sp"+split+".info";
		env->opf.open(ouputname);
	}
	else if ( Parameters::isSet("o") )
	{
		string ouputname = infile+"_n"+to_string(nb_leaf)+"_sp"+split+".time";

		env->opf.open(ouputname, ios_base::app);
	}
	// Otherwise let standard cout output
	else if ( !Parameters::isSet("o") )
	{
		env->opf.copyfmt(std::cout);									 //1
		env->opf.clear(std::cout.rdstate());                          //2
		env->opf.basic_ios<char>::rdbuf(std::cout.rdbuf());           //3
	}

	// Print parameters
	Parameters::printParams(env->opf);

	if ( run_Conversion() )
	{
		std::cout << "c Conversion done successfully.\n";
	}

	else
	{
		env->set_split_strat(split);

		if ( run_BMCStrat() )
		{
			std::cout << "c Run BMCTool strategies done successfully.\n";
		}
		else if ( run_Painless() )
		{
			std::cout << "c Run Painless strategies done successfully.\n";
		}
		else
		{
			std::cerr << "Run nothing..." << std::endl;
		}
	}

	env->opf.close();

	delete env;
	delete splitter;
	std::cout << "c Done." << std::endl;
	return finalResult;
}