fork download
copy 
  1. #include <iostream>
  2. #include <cstdio>
  3. #include <fstream>
  4. #include <map>
  5. #include <stdlib.h>
  6. #include <set>
  7. #include <string>
  8. #include <queue>
  9. #include <algorithm>
  10. #include <math.h>
  11. #include <vector>
  12. #include <cstring>
  13.  
  14. using namespace std;
  15.  
  16. class Node
  17. {	public:
  18. 	int target;
  19. 	set<int> dataset;
  20. 	set<int> unused;	
  21. 	set<int> used;
  22. 	string templ;
  23.  
  24. };
  25.  
  26. double h(double a,double b){
  27. 	double l1,l2;
  28. 	if (a==0)
  29. 		l1=0.0;	
  30. 	else
  31. 		l1=(-a)*log2(a);
  32. 	if(b==0)
  33. 		l2=0.0;
  34. 	else
  35. 		l2=(-b)*log2(b);
  36. 	return l1+l2;
  37.  
  38. 	}
  39.  
  40.  
  41. double cal(int d00,int d01,int d10,int d11){
  42. 	double total=d00+d01+d10+d11+0.0;
  43. 	double d0,d1,res;
  44.     if ((d00+d01) > 0)
  45.         d0=(d00+d01)*h(d00/(d00+d01+0.0),d01/(d00+d01+0.0))/(total);
  46.     else
  47.         d0=0.0;
  48.     if ((d10+d11) > 0)
  49.         d1=(d10+d11)*h(d10/(d10+d11+0.0),d11/(d10+d11+0.0))/(total);
  50.     else
  51.         d1=0.0;
  52.     res=d0+d1;
  53. 	return res;
  54.  
  55. }
  56. void get_intersection(set<int> a,set<int> b,set <int> &res){
  57. 	res.clear();
  58. 	set_intersection(a.begin(),a.end(),b.begin(),b.end(),inserter(res,res.begin()));
  59.  
  60.  
  61. }
  62. void get_union(set<int> a,set<int> b,set <int> &res){
  63. 	res.clear();
  64. 	set_union(a.begin(),a.end(),b.begin(),b.end(),inserter(res,res.begin()));
  65. }
  66. int finddigs(string x){
  67. 	int count=0;
  68. 	for(int i=0;i<x.length();i++){
  69. 		if(x[i]=='0'||x[i]=='1')
  70. 			count++;
  71. 	}	
  72. 	return count;
  73. }
  74. main(int argc, char *argv[]) {
  75.  
  76. 	ifstream signals(argv[1]);
  77. 	ifstream trace(argv[2]);
  78. 	ifstream lookup(argv[3]);
  79. 	int depth=atoi(argv[4]);
  80. 	ifstream output(argv[5]);
  81. 	int varcount=atoi(argv[6]);
  82. 	int genprops=atoi(argv[7]);
  83.  
  84. 	int linelength=varcount*depth;
  85.  
  86. 	map< int, set<int> > zerotable;
  87. 	map< int, set<int> > onetable;
  88. 	vector<string> tracelines;
  89.  
  90. 	int lineno=0;
  91. 	while(1){
  92. 		if(trace.eof())
  93. 			break;
  94. 		char temp[linelength+1];
  95. 		trace>>temp;
  96. 		if(strlen(temp)==0)
  97. 			continue;
  98. 		int i;
  99. 		for(i=0;i<linelength;i++){
  100. 			if(temp[i]=='0')
  101. 				zerotable[i].insert(lineno);
  102. 			else if(temp[i]=='1')
  103. 				onetable[i].insert(lineno);
  104. 		}
  105. 		string str(temp);
  106. 		tracelines.push_back(str);
  107. 		lineno++;
  108.  
  109. 	}
  110.  
  111.  
  112. 	lineno=lineno-1;
  113.  
  114. 	map<string,int> signal_dict;
  115. 	int i=0;
  116.  
  117. 	vector<string> sig_list;
  118. 	while(1){
  119. 		if(signals.eof())
  120. 			break;
  121.  
  122. 		string signame;
  123. 		signals>>signame;
  124. 		if(signame.length()==0)
  125. 			continue;
  126. 		signal_dict[signame]=i;
  127. 		i++;
  128. 		sig_list.push_back(signame);
  129. 	}
  130. 	set<int> lookup_vars;
  131. 	while(1){
  132. 		if(lookup.eof())
  133. 			break;
  134. 		string l;
  135. 		lookup>>l;
  136. 		if(l.length()==0)
  137. 			continue;
  138.  
  139. 		int x=signal_dict[l];		
  140.  
  141. 		for(i=x+varcount;i<linelength;i=i+varcount){
  142. 			lookup_vars.insert(i);
  143. 		}
  144.  
  145. 	}
  146. 	queue<Node> nqueue;
  147. 	while(1){
  148. 		if(output.eof())
  149. 			break;
  150. 		string l;
  151. 		output>>l;		
  152. 		if(l.length()==0)
  153. 			continue;
  154. 		Node node;
  155. 		node.target=signal_dict[l];
  156. 		for(int i=0;i<lineno;i++){
  157. 			node.dataset.insert(i);
  158. 		}
  159. 		node.unused=lookup_vars;
  160. 		node.templ.assign(linelength,'.');
  161. 		nqueue.push(node);
  162.  
  163. 	}
  164. 	vector<Node> leaf_nodes;
  165.  
  166. 	while((nqueue.size()>0) && (leaf_nodes.size() < genprops)) {
  167. 		Node cur_node=nqueue.front();
  168. 		nqueue.pop();
  169.  
  170. 		double gain=0.0;
  171. 		int best=-1;
  172. 		int m00=0;
  173. 		int m01=0;
  174. 		int m10=0;
  175. 		int m11=0;
  176. 		set<int> mdata00;
  177. 		set<int> mdata01;
  178. 		set<int> mdata10;
  179. 		set<int> mdata11;
  180. 		set<int> matched00;
  181. 		set<int> matched01;
  182. 		set<int> matched10;
  183. 		set<int> matched11;
  184. 		set<int> pos;
  185. 		set<int> neg;
  186. 		get_intersection(cur_node.dataset,zerotable[cur_node.target],pos);
  187. 		get_intersection(cur_node.dataset,onetable[cur_node.target],neg);
  188.  
  189. 		if(pos.size()==0 && neg.size()==0)
  190. 			continue;
  191.  
  192. 		if((pos.size()==0 || neg.size()==0) && (pos.size()!=0 || neg.size()!=0)) {
  193. 			if(pos.size()==0){
  194. 				cur_node.templ[cur_node.target]='1';
  195. 			}
  196. 			else
  197. 				cur_node.templ[cur_node.target]='0';
  198. 			if(cur_node.used.size()>0)
  199. 			leaf_nodes.push_back(cur_node);
  200. 			continue;
  201. 		}
  202. 		if(cur_node.unused.size()==0)
  203. 			continue;
  204.  
  205. 		double ent=h((pos.size()/(pos.size()+neg.size()+0.0)),(neg.size()/(pos.size()+neg.size()+0.0)));
  206.  
  207. 		for(set<int>::iterator it=cur_node.unused.begin();it!=cur_node.unused.end();it++){
  208. 			set<int> temp;
  209. 			get_intersection(zerotable[*it],zerotable[cur_node.target],temp);
  210. 			get_intersection(temp,cur_node.dataset,matched00);
  211.  
  212. 			get_intersection(zerotable[*it],onetable[cur_node.target],temp);
  213. 			get_intersection(temp,cur_node.dataset,matched01);
  214.  
  215. 			get_intersection(onetable[*it],zerotable[cur_node.target],temp);
  216. 			get_intersection(temp,cur_node.dataset,matched10);
  217.  
  218. 			get_intersection(onetable[*it],onetable[cur_node.target],temp);
  219. 			get_intersection(temp,cur_node.dataset,matched11);
  220.  
  221.  
  222. 			if((matched00.size()+matched01.size()+matched10.size()+matched11.size())==0)
  223. 				continue;
  224.  
  225. 			double entropy=cal(matched00.size(),matched01.size(),matched10.size(),matched11.size());
  226. 			if((ent-entropy)>gain){
  227. 				best=*it;
  228. 				m00=matched00.size();
  229. 				m01=matched01.size();
  230. 				m10=matched10.size();
  231. 				m11=matched11.size();
  232. 				mdata00=matched00;
  233. 				mdata01=matched01;
  234. 				mdata10=matched10;
  235. 				mdata11=matched11;
  236. 				gain=(ent-entropy);
  237.  
  238. 			}
  239. 		}
  240. 		int p=m00+m10;
  241. 		int n=m01+m11;
  242.  
  243. 		if (best != -1){
  244. 			if((m00+m01)>0){
  245. 				Node node0;
  246. 				get_union(mdata01,mdata00,node0.dataset);
  247. 				node0.target=cur_node.target;
  248. 				node0.templ=cur_node.templ;
  249. 				node0.templ[best]='0';
  250. 				node0.unused=cur_node.unused;
  251. 				node0.unused.erase(best);
  252. 				node0.used=cur_node.used;
  253. 				node0.used.insert(best%varcount);
  254. 				nqueue.push(node0);
  255. 			}
  256.  
  257. 			if((m10+m11)>0){
  258. 				Node node1;
  259. 				get_union(mdata11,mdata10,node1.dataset);
  260. 				node1.target=cur_node.target;
  261. 				node1.templ=cur_node.templ;
  262. 				node1.templ[best]='1';
  263. 				node1.unused=cur_node.unused;
  264. 				node1.unused.erase(best);
  265. 				node1.used=cur_node.used;
  266. 				node1.used.insert(best%varcount);
  267. 				nqueue.push(node1);
  268.  
  269. 			}
  270. 		}
  271. 	}
  272.  
  273. 	ofstream propsfile("properties.txt");
  274. 	ofstream conffile("belief.txt");
  275. 	ofstream tempfile("template.txt");
  276. 	for(int it=0;it<leaf_nodes.size();it++){
  277. 		Node cur_node=leaf_nodes[it];
  278. 		int usedlen=cur_node.used.size();
  279. 		if(usedlen<1)
  280. 			continue;
  281. 		tempfile<<cur_node.templ<<endl;
  282. 		string assertion("");
  283. 		int level=0;
  284. 		int cur_level=depth-1;
  285. 		bool printed=false;
  286. 		bool first=true;
  287. 		assertion+="((";
  288. 		bool started=false;
  289. 		set<string> unique;
  290. 		for(set<int>::iterator ds=cur_node.dataset.begin();ds!=cur_node.dataset.end();ds++){
  291. 			string line("");
  292. 			for(int ind=varcount;ind<linelength;ind+=varcount){
  293. 				//set<int> used=sort(cur_node.used);
  294. 				for(set<int>::iterator usd=cur_node.used.begin();usd!=cur_node.used.end();usd++){
  295. 						line+=tracelines[*ds][*usd+ind];
  296.  
  297. 				}
  298.  
  299. 			}
  300. 			unique.insert(line);
  301. 		}
  302. 		int totalprops=(depth-1)*(cur_node.used.size()+1);
  303. 		int usedprops=finddigs(cur_node.templ);
  304. 		double conf=(unique.size()+0.0)/pow(2,(totalprops - usedprops ));
  305. 		conffile<<conf<<endl;
  306.  
  307. 		for(int i=linelength-1;i>varcount;i--){
  308. 			if( i/varcount != cur_level){
  309. 				cur_level-=1;
  310. 				level+=1;
  311. 				printed=false;
  312. 				first=true;
  313. 			}
  314. 			if (cur_node.templ[i]!='.'){
  315. 				if(!printed&& cur_level!=depth-1 && started){
  316.  
  317. 					assertion+="##"+string(1,(char)(level+48))+" " ;
  318. 					level=0;
  319. 					printed=true;
  320. 					first=true;
  321. 				}
  322. 				if(first){
  323. 					assertion+=string(sig_list[i%varcount])+"=="+string(1,cur_node.templ[i])+" ";
  324. 					first=false;
  325. 					started=true;
  326. 				}
  327. 				else{
  328. 					assertion+="&& "+string(sig_list[i%varcount])+"=="+string(1,cur_node.templ[i])+" ";
  329. 					started=true;
  330. 				}
  331. 			}
  332. 		}
  333. 		assertion+=") |=> ("+string(sig_list[cur_node.target])+"=="+string(1,cur_node.templ[cur_node.target])+"));";
  334. 		propsfile<<assertion<<endl;
  335.  
  336.  
  337.  
  338. 	}
  339.  
  340.  
  341. }
  342.  
Runtime error #stdin #stdout #stderr 2.99s 463168KB
comments (?)
stdin
copy 
Standard input is empty
stdout
copy 
Standard output is empty
stderr
copy 
terminate called after throwing an instance of 'std::bad_alloc'
  what():  std::bad_alloc
https://ideone.com/5Hpb9W
language:
C++14 (gcc 8.3)
created:
9 years ago
visibility:
public

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!