#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;
}