#include "../include/Args.h"
#include "../include/TrimSubstitute.h"
#include "../include/WitnessSelect.h"
#include "../include/Mgr.h"

#include <iostream>
#include <fstream>
#include <chrono>
#include <random>

using namespace std;
using namespace chrono;
	
string Args::retrieve(string option)
{
	auto it = args.find(option);
	
	if (it == args.end())
		throw invalid_argument("No -" + option + " option provided");
		
	return it->second;
}

BDD Args::loadSpecification()
{
	string path = retrieve("s");
	
	if (path.compare(path.size() - 4, 4, ".bdd") == 0)
		return m.loadBDD(path);
	else if (path.compare(path.size() - 4, 4, ".cnf") == 0)
		return m.loadCNF(path);
	else
		throw invalid_argument("Input file must have .bdd or .cnf extension");
}

vector<int> Args::loadOutputIndices()
{
	string filename = retrieve("v");
	ifstream in(filename);
	
	if (!in.is_open())
		throw invalid_argument("Unable to open file " + filename);
		
	vector<int> outputIndex;
	int var;
		
	while (true)
	{
		in >> var;
		
		if (in.eof()) break;
		
		outputIndex.push_back(var);
	}
	
	in.close();
	
	return outputIndex;
}

Implementation Args::synthesize(const BDD& spec, const vector<int>& outputIndices)
{
	string methodName = retrieve("m");
	
	if (methodName == "realiz")
	{
		string qeMethod = retrieve("q");
		
		if (qeMethod == "selfsubst")
			return realizability(spec, outputIndices, selfSubstitution);
		else if (qeMethod == "shannon")
			return realizability(spec, outputIndices, shannonExpansion);
		else
			throw invalid_argument("Invalid quantifier elimination method: " + qeMethod);
	}
	else if (methodName == "funconstr")
	{
		string qeMethod = retrieve("q");
		int defaultValue = stoi(retrieve("d"));
		
		if (defaultValue != 0 && defaultValue != 1)
			throw invalid_argument("Default value must be 0 or 1");
		
		if (qeMethod == "selfsubst")
			return witnessSelect(spec, outputIndices, selfSubstitution, defaultValue);
		else if (qeMethod == "shannon")
			return witnessSelect(spec, outputIndices, shannonExpansion, defaultValue);
		else
			throw invalid_argument("Invalid quantifier elimination method: " + qeMethod);
	}
	else if (methodName == "trimsubst")
	{
		int defaultValue = stoi(retrieve("d"));
		
		if (defaultValue != 0 && defaultValue != 1)
			throw invalid_argument("Default value must be 0 or 1");
			
		return trimSubstitute(spec, outputIndices, defaultValue);
	}
	else
	{
		throw invalid_argument("Invalid synthesis method: " + methodName);
	}
}

void Args::experiment()
{
	BDD spec = loadSpecification();
	vector<int> outputIndex = loadOutputIndices();

	auto start = system_clock::now();
	
	Implementation implementation = synthesize(spec, outputIndex);
	
	auto duration = duration_cast<milliseconds>(system_clock::now() - start);

	cout << duration.count() << " " << implementation.nodeCount() << endl;
}

void Args::dumpDot()
{
	BDD spec = loadSpecification();
	vector<int> outputIndex = loadOutputIndices();
	Implementation implementation = synthesize(spec, outputIndex);

	m.dumpDot(spec);
	implementation.dumpDot();
}

Args::Args(int argc, char* argv[])
{
	for (int i = 0; i < argc; i += 2)
	{
		if (argv[i][0] != '-')
			throw invalid_argument("Argument " + string(argv[i]) + " not preceded by command-line option");
			
		string option(argv[i] + 1);
		
		if (i + 1 == argc)
			throw invalid_argument("Option " + option + " without argument");
		
		string arg(argv[i + 1]);
		
		args[option] = arg;
	}
}

void Args::execute()
{
	auto it = args.find("l");
	
	if (it != args.end())
	{
		const char* c_str = it->second.c_str();
		m.setMaxMemory(strtoul(c_str, NULL, 10));
	}

	string execMode = retrieve("x");
		
	if (execMode == "experiment") experiment();
	else if (execMode == "dump") dumpDot();
	else throw invalid_argument("Invalid execution mode: " + execMode);
}