#include <vector>
#include <set>
#include <iostream>
#include <fstream>

#include "../include/Specification.h"
#include "../include/Ordering.h"
#include "../include/Mgr.h"

using namespace std;

void writeVars(const vector<vector<BDD>>& vars, const char filename[])
{
	set<int> outputIndices;
	
	for (size_t i = 0; i < vars.size(); i++)
	for (size_t j = 0; j < vars[i].size(); j++)
	{
		outputIndices.insert(vars[i][j].NodeReadIndex());
	}

	ofstream out(filename);

	for (auto it = outputIndices.begin(); it != outputIndices.end(); it++)
		out << *it << " ";
	
	out.close();
}

int main(int argc, char* argv[])
{
	if (argc < 5)
	{
		cout << "Expected format: genbenchmark <benchmark-class> <size> <output-format> <bdd-file> <vars-file>" << endl;
		return 0;
	}
	
	int n = atoi(argv[2]);
	
	if (n < 1)
	{
		cout << "Size must be an integer greater than 0" << endl;
		return 0;
	}
	
	string testCase(argv[1]);
	vector<vector<BDD>> vars;
	BDD bdd;
	vector<vector<BDD>> outputVars;
	
	if (testCase == "subtraction")
	{
		vars = interleaved(2, 1, decreasing(n));
		bdd = subtractionSpec(vars[0], vars[1], vars[2]);
		outputVars.push_back(vars[2]);
	}
	else if (testCase == "max")
	{
		vars = interleaved(2, 1, increasing(n));
		bdd = maxSpec(vars[0], vars[1], vars[2]);
		outputVars.push_back(vars[2]);
	}
	else if (testCase == "min")
	{
		vars = interleaved(2, 1, increasing(n));
		bdd = minSpec(vars[0], vars[1], vars[2]);
		outputVars.push_back(vars[2]);
	}
	else if (testCase == "avgceiling")
	{
		vars = interleaved(2, 1, decreasing(n));
		bdd = averageCeilingSpec(vars[0], vars[1], vars[2]);
		outputVars.push_back(vars[2]);
	}
	else if (testCase == "avgfloor")
	{
		vars = interleaved(2, 1, decreasing(n));
		bdd = averageFloorSpec(vars[0], vars[1], vars[2]);
		outputVars.push_back(vars[2]);
	}
	else if (testCase == "bitsort")
	{
		vars = inOrder(1, 1, increasing(n));
		bdd = sortingSpec(vars[0], vars[1]);
		outputVars.push_back(vars[1]);
	}
	else if (testCase == "decomposition")
	{
		vars = interleaved(1, 2, decreasing(n));
		bdd = decompositionSpec(vars[0], vars[1], vars[2]);
		outputVars.push_back(vars[1]);
		outputVars.push_back(vars[2]);
	}
	else if (testCase == "equalization")
	{
		vars = interleaved(2, 2, decreasing(n));
		bdd = equalizationSpec(vars[0], vars[1], vars[2], vars[3]);
		outputVars.push_back(vars[2]);
		outputVars.push_back(vars[3]);
	}
	else if (testCase == "intermediate")
	{
		vars = interleaved(2, 1, increasing(n));
		bdd = intermediateValueSpec(vars[0], vars[1], vars[2]);
		outputVars.push_back(vars[2]);
	}
	else
	{
		cout << "Invalid benchmark class: " << testCase << endl;
		return 0;
	}
	
	m.storeBDD(bdd, argv[3]);

	writeVars(outputVars, argv[4]);
}