#include <iostream>
#include <cstdio>
#include <fstream>
#include <map>
#include <stdlib.h>
#include <set>
#include <string>
#include <queue>
#include <algorithm>
#include <math.h>
#include <vector>
#include <cstring>

using namespace std;

class Node
{	public:
	int target;
	set<int> dataset;
	set<int> unused;	
	set<int> used;
	string templ;

};

double h(double a,double b){
	double l1,l2;
	if (a==0)
		l1=0.0;	
	else
		l1=(-a)*log2(a);
	if(b==0)
		l2=0.0;
	else
		l2=(-b)*log2(b);
	return l1+l2;

	}


double cal(int d00,int d01,int d10,int d11){
	double total=d00+d01+d10+d11+0.0;
	double d0,d1,res;
    if ((d00+d01) > 0)
        d0=(d00+d01)*h(d00/(d00+d01+0.0),d01/(d00+d01+0.0))/(total);
    else
        d0=0.0;
    if ((d10+d11) > 0)
        d1=(d10+d11)*h(d10/(d10+d11+0.0),d11/(d10+d11+0.0))/(total);
    else
        d1=0.0;
    res=d0+d1;
	return res;

}
void get_intersection(set<int> a,set<int> b,set <int> &res){
	res.clear();
	set_intersection(a.begin(),a.end(),b.begin(),b.end(),inserter(res,res.begin()));
	

}
void get_union(set<int> a,set<int> b,set <int> &res){
	res.clear();
	set_union(a.begin(),a.end(),b.begin(),b.end(),inserter(res,res.begin()));
}
int finddigs(string x){
	int count=0;
	for(int i=0;i<x.length();i++){
		if(x[i]=='0'||x[i]=='1')
			count++;
	}	
	return count;
}
main(int argc, char *argv[]) {

	ifstream signals(argv[1]);
	ifstream trace(argv[2]);
	ifstream lookup(argv[3]);
	int depth=atoi(argv[4]);
	ifstream output(argv[5]);
	int varcount=atoi(argv[6]);
	int genprops=atoi(argv[7]);

	int linelength=varcount*depth;

	map< int, set<int> > zerotable;
	map< int, set<int> > onetable;
	vector<string> tracelines;

	int lineno=0;
	while(1){
		if(trace.eof())
			break;
		char temp[linelength+1];
		trace>>temp;
		if(strlen(temp)==0)
			continue;
		int i;
		for(i=0;i<linelength;i++){
			if(temp[i]=='0')
				zerotable[i].insert(lineno);
			else if(temp[i]=='1')
				onetable[i].insert(lineno);
		}
		string str(temp);
		tracelines.push_back(str);
		lineno++;

	}
	

	lineno=lineno-1;

	map<string,int> signal_dict;
	int i=0;

	vector<string> sig_list;
	while(1){
		if(signals.eof())
			break;

		string signame;
		signals>>signame;
		if(signame.length()==0)
			continue;
		signal_dict[signame]=i;
		i++;
		sig_list.push_back(signame);
	}
	set<int> lookup_vars;
	while(1){
		if(lookup.eof())
			break;
		string l;
		lookup>>l;
		if(l.length()==0)
			continue;
		
		int x=signal_dict[l];		
		
		for(i=x+varcount;i<linelength;i=i+varcount){
			lookup_vars.insert(i);
		}

	}
	queue<Node> nqueue;
	while(1){
		if(output.eof())
			break;
		string l;
		output>>l;		
		if(l.length()==0)
			continue;
		Node node;
		node.target=signal_dict[l];
		for(int i=0;i<lineno;i++){
			node.dataset.insert(i);
		}
		node.unused=lookup_vars;
		node.templ.assign(linelength,'.');
		nqueue.push(node);

	}
	vector<Node> leaf_nodes;

	while((nqueue.size()>0) && (leaf_nodes.size() < genprops)) {
		Node cur_node=nqueue.front();
		nqueue.pop();

		double gain=0.0;
		int best=-1;
		int m00=0;
		int m01=0;
		int m10=0;
		int m11=0;
		set<int> mdata00;
		set<int> mdata01;
		set<int> mdata10;
		set<int> mdata11;
		set<int> matched00;
		set<int> matched01;
		set<int> matched10;
		set<int> matched11;
		set<int> pos;
		set<int> neg;
		get_intersection(cur_node.dataset,zerotable[cur_node.target],pos);
		get_intersection(cur_node.dataset,onetable[cur_node.target],neg);

		if(pos.size()==0 && neg.size()==0)
			continue;

		if((pos.size()==0 || neg.size()==0) && (pos.size()!=0 || neg.size()!=0)) {
			if(pos.size()==0){
				cur_node.templ[cur_node.target]='1';
			}
			else
				cur_node.templ[cur_node.target]='0';
			if(cur_node.used.size()>0)
			leaf_nodes.push_back(cur_node);
			continue;
		}
		if(cur_node.unused.size()==0)
			continue;

		double ent=h((pos.size()/(pos.size()+neg.size()+0.0)),(neg.size()/(pos.size()+neg.size()+0.0)));

		for(set<int>::iterator it=cur_node.unused.begin();it!=cur_node.unused.end();it++){
			set<int> temp;
			get_intersection(zerotable[*it],zerotable[cur_node.target],temp);
			get_intersection(temp,cur_node.dataset,matched00);

			get_intersection(zerotable[*it],onetable[cur_node.target],temp);
			get_intersection(temp,cur_node.dataset,matched01);

			get_intersection(onetable[*it],zerotable[cur_node.target],temp);
			get_intersection(temp,cur_node.dataset,matched10);

			get_intersection(onetable[*it],onetable[cur_node.target],temp);
			get_intersection(temp,cur_node.dataset,matched11);
			
			
			if((matched00.size()+matched01.size()+matched10.size()+matched11.size())==0)
				continue;

			double entropy=cal(matched00.size(),matched01.size(),matched10.size(),matched11.size());
			if((ent-entropy)>gain){
				best=*it;
				m00=matched00.size();
				m01=matched01.size();
				m10=matched10.size();
				m11=matched11.size();
				mdata00=matched00;
				mdata01=matched01;
				mdata10=matched10;
				mdata11=matched11;
				gain=(ent-entropy);

			}
		}
		int p=m00+m10;
		int n=m01+m11;

		if (best != -1){
			if((m00+m01)>0){
				Node node0;
				get_union(mdata01,mdata00,node0.dataset);
				node0.target=cur_node.target;
				node0.templ=cur_node.templ;
				node0.templ[best]='0';
				node0.unused=cur_node.unused;
				node0.unused.erase(best);
				node0.used=cur_node.used;
				node0.used.insert(best%varcount);
				nqueue.push(node0);
			}

			if((m10+m11)>0){
				Node node1;
				get_union(mdata11,mdata10,node1.dataset);
				node1.target=cur_node.target;
				node1.templ=cur_node.templ;
				node1.templ[best]='1';
				node1.unused=cur_node.unused;
				node1.unused.erase(best);
				node1.used=cur_node.used;
				node1.used.insert(best%varcount);
				nqueue.push(node1);

			}
		}
	}

	ofstream propsfile("properties.txt");
	ofstream conffile("belief.txt");
	ofstream tempfile("template.txt");
	for(int it=0;it<leaf_nodes.size();it++){
		Node cur_node=leaf_nodes[it];
		int usedlen=cur_node.used.size();
		if(usedlen<1)
			continue;
		tempfile<<cur_node.templ<<endl;
		string assertion("");
		int level=0;
		int cur_level=depth-1;
		bool printed=false;
		bool first=true;
		assertion+="((";
		bool started=false;
		set<string> unique;
		for(set<int>::iterator ds=cur_node.dataset.begin();ds!=cur_node.dataset.end();ds++){
			string line("");
			for(int ind=varcount;ind<linelength;ind+=varcount){
				//set<int> used=sort(cur_node.used);
				for(set<int>::iterator usd=cur_node.used.begin();usd!=cur_node.used.end();usd++){
						line+=tracelines[*ds][*usd+ind];

				}

			}
			unique.insert(line);
		}
		int totalprops=(depth-1)*(cur_node.used.size()+1);
		int usedprops=finddigs(cur_node.templ);
		double conf=(unique.size()+0.0)/pow(2,(totalprops - usedprops ));
		conffile<<conf<<endl;

		for(int i=linelength-1;i>varcount;i--){
			if( i/varcount != cur_level){
				cur_level-=1;
				level+=1;
				printed=false;
				first=true;
			}
			if (cur_node.templ[i]!='.'){
				if(!printed&& cur_level!=depth-1 && started){
					
					assertion+="##"+string(1,(char)(level+48))+" " ;
					level=0;
					printed=true;
					first=true;
				}
				if(first){
					assertion+=string(sig_list[i%varcount])+"=="+string(1,cur_node.templ[i])+" ";
					first=false;
					started=true;
				}
				else{
					assertion+="&& "+string(sig_list[i%varcount])+"=="+string(1,cur_node.templ[i])+" ";
					started=true;
				}
			}
		}
		assertion+=") |=> ("+string(sig_list[cur_node.target])+"=="+string(1,cur_node.templ[cur_node.target])+"));";
		propsfile<<assertion<<endl;



	}


}