#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"
#include "src/utils/Utils.hh"

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

bool read_Filename()
{
	if (!split.compare("nr") || !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;
	bool run_painless_directly = false;
	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) || (solver_name.compare("maple") == 0))
			run_painless_directly = true;

		read_Filename();

		if (env->max_vars == 0)
		{
			env->opf << "s UNSATISFIABLE" << endl;
			std::cout << "s UNSATISFIABLE" << endl;
			return true;
		}
		if (!run_painless_directly)
		{
			// Preprocess solvers (split problem, affect each partition to a solver,...)
			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);
		t1 = clock() - t1;

		env->opf << "c " << endl;
		env->opf << "c TOTAL RESOLUTION TIME : " << ((float)t1) / CLOCKS_PER_SEC << 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);
		}

		// 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;

		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-t int \t    : timeout (default none)." << std::endl;
		std::cout << "\t-max-memory : memory limit in Go (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    -k int \t    : Bound for the transition relation (bound 0 included : k+1)." << 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 (NOT WORKING),\
									\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} (NOT WORKING): " << std::endl;
		std::cout << "\t    -k int \t    : Bound for the transition relation (bound 0 included : k+1)." << 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 {periplo,desat,maple} : special solver name, default is maple." << std::endl;
		std::cout << "\t    -stats {1,2}   : 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 standard maple solvers (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 b)."
				  << std::endl;
		// std::cout << "\t    -f {P,M,J,PM,...,A,N}  \t : Filter shared Interpolants (N : Nothing to share, A : No filter, P : Property Interpolants, M : Model Interpolants, J : Junction Interpolants, default is N)." << std::endl;
		// std::cout << "\t    -shroot {-1,0,1} : Share conflict clauses (-1 : Nothing to share, 0 : LBD filter, 1 : Optimal configuration P0, default is -1)." << std::endl;
		// std::cout << "\t    -shr-solver {0,1,5} : Filter for Maple Solver (0 : LBD filter, 1 : Optimal configuration P0, 5 : LBD+P-LBD5, default is 0)." << std::endl;
		std::cout << "\t    -sat-heuristic {0,1,2} : SAT-BMC heuristics (0 : original approach (LBD<= 3), 1 : Linear programming approach, 2 : Structural approach, default is 0)." << std::endl;
		return 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", "");
	solver_name = Parameters::getParam("s", "maple");
	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 BMCTool0 strategies done successfully.\n";
		else if (run_Painless())
			std::cout << "c Run BMCTool strategies done successfully.\n";
		else
			std::cerr << "Run nothing..." << std::endl;
	}

	env->opf.close();

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