Untitled

#include <iostream>
#include <fstream>
#include <string>
#include <vector>
#include <cmath>

using namespace std;

class Node
{
public:
	Node() {}
	int else_edge, then_edge = 0;
	string Variable = "";
	bool redundent = false;
};

class ROBDD
{
public:
	int PLA_i, PLA_p;
	vector<string> names;
	vector<string> terms;
	Node* BinaryTree = nullptr;
	int size;
	void Output()
	{
		// 創一顆binary tree
		size = pow(2, PLA_i) + 1;
		BinaryTree = new Node[size];
		BinaryTree[0].Variable = "0";
		BinaryTree[size - 1].Variable = "1";

		for (int i = 0; i < PLA_i; i++)
		{
			for (int j = pow(2, i); j < pow(2, i + 1); j++)
			{
				BinaryTree[j].Variable = names[i];
				BinaryTree[j].redundent = false;
				if (i == PLA_i - 1)
				{
					continue;
				}
				else
				{
					BinaryTree[j].else_edge = 2 * j;
					BinaryTree[j].then_edge = 2 * j + 1;
				}
			}
		}

		for (int i = pow(2, PLA_i - 1), j = 0; i < pow(2, PLA_i); i++, j += 2)
		{
			if (IsBooleanTrue(j))
			{
				BinaryTree[i].else_edge = size - 1;
			}
			else
			{
				BinaryTree[i].else_edge = 0;
			}
			if (IsBooleanTrue(j + 1))
			{
				BinaryTree[i].then_edge = size - 1;
			}
			else
			{
				BinaryTree[i].then_edge = 0;
			}
		}
	}

	void Reduced(int PLA_i)
	{
		cout << "index" << "\t\t" << "Variable" << "\t" << "Else-edge" << "\t" << "Then-edge" << "\t" << "Comment" << endl;
		cout << "0\t\t-\t\t-\t\t-\t\tBoolean 0" << endl;
		for (int i = 1; i < pow(2, PLA_i); i++) {
			cout << i << "\t\t" << BinaryTree[i].Variable << "\t\t" << BinaryTree[i].else_edge << "\t\t" << BinaryTree[i].then_edge << "\t\t";
			if (BinaryTree[i].redundent)
			{
				cout << "redundent" << endl;
			}
			else
			{
				cout << endl;
			}
		}
		cout << pow(2, PLA_i) << " \t\t-\t\t-\t\t-\t\tBoolean 1" << endl;
		cout << "--------------------------------------------------------------------------" << endl;

		for (int i = PLA_i - 1; i >= 0; i--)
		{
			bool changed = false;
			for (int j = pow(2, i); j < pow(2, i + 1); j++)
			{
				if (BinaryTree[j].redundent)
				{
					continue;
				}
				if (BinaryTree[j].else_edge == BinaryTree[j].then_edge)
				{
					if (j % 2 == 0)
					{
						BinaryTree[j / 2].else_edge = BinaryTree[j].then_edge;
					}
					else
					{
						BinaryTree[j / 2].then_edge = BinaryTree[j].else_edge;
					}
					BinaryTree[j].redundent = true;
					changed = true;
					continue;
				}
				for (int k = j + 1; k < pow(2, i + 1); k++)
				{
					if (BinaryTree[k].redundent)
					{
						continue;
					}
					if (BinaryTree[j].else_edge == BinaryTree[k].else_edge && BinaryTree[j].then_edge == BinaryTree[k].then_edge && BinaryTree[j].Variable == BinaryTree[k].Variable)
					{
						if (k % 2 == 0)
						{
							BinaryTree[k / 2].else_edge = j;
						}
						else
						{
							BinaryTree[k / 2].then_edge = j;
						}
						BinaryTree[k].redundent = true;
						changed = true;
					}
				}
			}
			if (changed)
			{
				cout << "index" << "\t\t" << "Variable" << "\t" << "Else-edge" << "\t" << "Then-edge" << "\t" << "Comment" << endl;
				cout << "0\t\t-\t\t-\t\t-\t\tBoolean 0" << endl;
				for (int i = 1; i < pow(2, PLA_i); i++) {
					cout << i << "\t\t" << BinaryTree[i].Variable << "\t\t" << BinaryTree[i].else_edge << "\t\t" << BinaryTree[i].then_edge << "\t\t";
					if (BinaryTree[i].redundent)
					{
						cout << "redundent" << endl;
					}
					else
					{
						cout << endl;
					}
				}
				cout << pow(2, PLA_i) << " \t\t-\t\t-\t\t-\t\tBoolean 1" << endl;
				cout << "--------------------------------------------------------------------------" << endl;
			}
		}
	}

	bool IsBooleanTrue(int num)
	{
		string BinaryNum;

		for (int i = PLA_i - 1; i >= 0; i--)
		{
			if (num >= pow(2, i))
			{
				BinaryNum += '1';
				num -= 1 << i;
			}
			else
			{
				BinaryNum += '0';
			}
		}

		for (int i = 0; i < PLA_p; i++)
		{
			bool Flag = true;
			for (int j = 0; j < PLA_i; j++)
			{
				if (terms[i][j] != '-' && BinaryNum[j] != terms[i][j])
				{
					Flag = false;
					break;
				}
			}
			if (Flag)
			{
				return true;
			}
		}
		return false;
	}

	void outputFile(ostream& obdd, ostream& robdd_file)
	{
		obdd << "digraph OBDD" << endl << "{" << endl;
		for (int i = 0; i < PLA_i; i++)
		{
			obdd << "\t{rank=same";
			for (int j = pow(2, i); j < pow(2, i + 1); j++)
			{
				if (BinaryTree[j].redundent)
				{
					continue;
				}
				else
				{
					obdd << " " << j;
				}
			}
			obdd << "}" << endl;
		}
		obdd << endl;
		obdd << "\t0 [label=\"0\", shape = box]" << endl;
		for (int i = 1; i < size - 1; i++)
		{
			if (BinaryTree[i].redundent) continue;
			obdd << "\t" << i << " [label=\"" << BinaryTree[i].Variable << "\"]" << endl;
		}
		obdd << "\t" << size - 1 << " [label = \"1\", shape = box]" << endl;

		obdd << endl;
		for (int i = 1; i < size - 1; i++)
		{
			if (BinaryTree[i].redundent) continue;
			obdd << "\t" << i << " -> " << BinaryTree[i].else_edge << " [label=\"0\", style=dotted]" << endl;
			obdd << "\t" << i << " -> " << BinaryTree[i].then_edge << " [label=\"1\", style=solid]" << endl;
		}
		obdd << "}" << endl;

		Reduced(PLA_i);

		robdd_file << "digraph ROBDD" << endl << "{" << endl;
		for (int i = 0; i < PLA_i; i++)
		{
			robdd_file << "\t{rank=same";
			for (int j = pow(2, i); j < pow(2, i + 1); j++)
			{
				if (BinaryTree[j].redundent)
				{
					continue;
				}
				else
				{
					robdd_file << " " << j;
				}
			}
			robdd_file << "}" << endl;
		}
		robdd_file << endl;
		robdd_file << "\t0 [label=\"0\", shape = box]" << endl;
		for (int i = 1; i < size - 1; i++)
		{
			if (BinaryTree[i].redundent) continue;
			robdd_file << "\t" << i << " [label=\"" << BinaryTree[i].Variable << "\"]" << endl;
		}
		robdd_file << "\t" << size - 1 << " [label = \"1\", shape = box]" << endl;

		robdd_file << endl;
		for (int i = 1; i < size - 1; i++)
		{
			if (BinaryTree[i].redundent) continue;
			robdd_file << "\t" << i << " -> " << BinaryTree[i].else_edge << " [label=\"0\", style=dotted]" << endl;
			robdd_file << "\t" << i << " -> " << BinaryTree[i].then_edge << " [label=\"1\", style=solid]" << endl;
		}
		robdd_file << "}" << endl;
	}
};






int main(int argc, char* argv[])
{
	ifstream input(argv[1]);
	ofstream obdd(argv[2]);
	ofstream robdd_file(argv[3]);

	string command;

	ROBDD robdd;
	
	while (input >> command)
	{
		if (command == ".i")
		{
			input >> robdd.PLA_i;
		}
		else if (command == ".o")
		{
			int temp;
			input >> temp;
		}
		else if (command == ".ilb")
		{
			for (int i = 0; i < robdd.PLA_i; i++)
			{
				string name;
				input >> name;
				robdd.names.push_back(name);
			}
		}
		else if (command == ".ob")
		{
			string temp;
			input >> temp;
		}
		else if (command == ".p")
		{
			input >> robdd.PLA_p;
			for (int i = 0; i < robdd.PLA_p; i++)
			{
				int temp;
				string term;
				input >> term >> temp;
				robdd.terms.push_back(term);
			}
		}
		else if (command == ".e")
		{
			break;
		}
		else
		{
			cout << "error" << endl;
			exit(1);
		}
	}
	robdd.Output();
	robdd.outputFile(obdd, robdd_file);

	input.close();
	obdd.close();
	robdd_file.close();
	return 0;
}