1# various attempts at gathering statistics
2
3from syntax import Expr, Type
4from rep_graph import vc_options
5from check import ProofNode
6
7from target_objects import pairings
8import check
9import search
10import logic
11import rep_graph
12
13def scan_proofs (res_f):
14	nm = None
15	proofs = {}
16	pairings_set = set ([p for f in pairings for p in pairings[f]])
17	pairings_names = dict ([(pair.name, pair) for pair in pairings_set])
18	for line in res_f:
19		if line.startswith ('Testing Function'):
20			(_, nm) = line.split (' pair ', 1)
21			nm = nm.strip ()
22			pair = pairings_names[nm]
23		if line.startswith ('ProofNode '):
24			pn = eval (line)
25			proofs[pair] = pn
26	res_f.close ()
27	return proofs
28
29def all_problems (proofs, filt = None):
30	problems = []
31	for (pair, proof) in proofs.iteritems ():
32		if filt != None:
33			if not [pn for pn in proof.all_subproofs ()
34					if filt (pn)]:
35				continue
36		p = check.build_problem (pair)
37		probs = proof.all_subproblems (p, (),
38			check.init_point_hyps (p), 'problem')
39		problems.extend ([(p, pn, restrs, hyps)
40			for (pn, restrs, hyps) in probs
41			if filt == None or filt (pn)])
42	return problems
43
44def filter_split_problems (problems):
45	return [(p, proofnode, restrs, hyps)
46		for (p, proofnode, restrs, hyps) in problems
47		if proofnode.kind == 'Split']
48
49def scan_split_problems (fname):
50	proofs = scan_proofs (open (fname))
51	problems = all_problems (proofs, filt = lambda pn: pn.kind == 'Split')
52	return problems
53
54def split_metrics (proofnode):
55	(l_start, l_step) = proofnode.split[0][1]
56	(r_start, r_step) = proofnode.split[1][1]
57	l_side = l_start + (l_step * 2) + 1
58	r_side = r_start + (r_step * 2) + 1
59	return (max (l_side, r_side), (l_start, l_step), (r_start, r_step))
60
61def has_linear_split ((info, p, pn, restrs, hyps)):
62	loop_head = pn.split[0][0]
63	nec = search.get_necessary_split_opts (p, loop_head,
64		restrs, hyps)
65	return nec != None
66
67def problems_with_linear_splits (split_problems):
68	probs = sorted ([(split_metrics (pn), p, pn, restrs, hyps)
69		for (p, pn, restrs, hyps) in split_problems])
70	data = []
71	for (i, (info, p, pn, restrs, hyps)) in enumerate (probs):
72		print 'Handling loop %d in %s' % (i, p.name)
73		h = has_linear_split ((info, p, pn, restrs, hyps))
74		data.append ((info, pn, h))
75	return data
76
77def tabulate_problems_with_linear_splits (data):
78	rows = {}
79	for (_, pn, has_nec) in data:
80		wsz = split_metrics (pn)[0]
81		rows.setdefault (wsz, [])
82		rows[wsz].append (has_nec)
83	print 'Breakdown of presence of necessary splits:'
84	for i in sorted (rows):
85		print 'Window size %d:' % i
86		tr = len ([v for v in rows[i] if v])
87		ln = len (rows[i])
88		print '  %d / %d (%0.1f%s)' % (tr, ln, (tr * 100.0) / ln, '%')
89
90def problem_var_analysis_nonempty ((p, pn, restrs, hyps)):
91	loop_head = pn.split[0][0]
92	va = search.get_loop_var_analysis_at (p, loop_head)
93	return bool ([v for (v, data) in va if data == 'LoopVariable'])
94
95def example_problems (split_problems, num):
96	probs = filter (problem_var_analysis_nonempty, split_problems)
97	probs = sorted ([(split_metrics (pn), p, pn, restrs, hyps)
98                for (p, pn, restrs, hyps) in probs])
99	prob_idxs = sorted (set ([int ((i * (len (probs) - 1)) * 1.0 / num)
100		for i in range (num)]))
101	return [probs[i] for i in prob_idxs]
102
103def big_example_problem (split_problems):
104	probs = filter (problem_var_analysis_nonempty, split_problems)
105	probs = sorted ([(split_metrics (pn), p, pn, restrs, hyps)
106		for (p, pn, restrs, hyps) in split_problems])
107	probs.reverse ()
108	probs_with_lin = (prob for prob in probs
109		if has_linear_split (prob))
110	return probs_with_lin.next ()
111
112def trace_split_loop_pairs_window (problem, window_size):
113	(_, p, pn, restrs, hyps) = problem
114	loop_head = pn.split[0][0]
115	if ('v_eqs', loop_head) in p.cached_analysis:
116		del p.cached_analysis[('v_eqs', loop_head)]
117
118	rep = rep_graph.mk_graph_slice (p, fast = True)
119	i_j_opts = search.mk_i_j_opts (unfold_limit = window_size)
120	(i_opts, j_opts) = i_j_opts[-1]
121	knowledge = search.setup_split_search (rep, loop_head, restrs, hyps,
122                i_opts, j_opts, unfold_limit = window_size)
123
124	res = search.split_search (loop_head, knowledge)
125	trace = list (knowledge.live_pairs_trace)
126	return (res, trace)
127
128def tabulate_example_traces (split_problems, data):
129	probs = example_problems (split_problems, 16)
130	ex_traces = [(prob[0][0] + 1,
131			trace_split_loop_pairs_window (prob, prob[0][0] + 1))
132		for prob in probs]
133
134	prob = big_example_problem (split_problems)
135	big_traces = []
136	for i in range (prob[0][0] + 2):
137		if not search.mk_i_j_opts (unfold_limit = i):
138			continue
139		(_, trace) = trace_split_loop_pairs_window (prob, i)
140		big_traces.append ((i, trace))
141
142	print 'Search pair decay in random examples (idx, window size, trace):'
143	for (i, (w, (_, trace))) in enumerate (ex_traces):
144		print '  %d: %d: %s' % (i, w, trace)
145
146	print 'Search pair decay in large problem, window sizes:'
147	for (w, trace) in big_traces:
148		print '  %d: %s' % (w, trace)
149
150	print 'Example again in gnuplot-happy format:'
151	for (w, (_, trace)) in ex_traces:
152		print
153		print
154		for v in trace:
155			print v
156
157	print 'Large example again:'
158	for (w, trace) in big_traces:
159		print
160		print
161		for v in trace:
162			print v
163
164def scan_times (res_f):
165	nm = None
166	times = {}
167	pairings_set = set ([p for f in pairings for p in pairings[f]])
168	pairings_names = dict ([(pair.name, pair) for pair in pairings_set])
169	for line in res_f:
170		if line.startswith ('Testing Function'):
171			(_, nm) = line.split (' pair ', 1)
172			nm = nm.strip ()
173			pair = pairings_names[nm]
174		if line.startswith ('Result ') and 'time taken:' in line:
175			(_, time) = line.split ('time taken:', 1)
176			time = time.strip ()
177			assert time[-1] == 's'
178			time = float (time[:-1])
179			times[pair] = time
180	res_f.close ()
181	return times
182
183def problem_difficult_estimate (p):
184	return (len (p.nodes), len (p.loop_heads ()),
185		len ([n for n in p.nodes if p.loop_id (n)]))
186
187def tabulate_timing_estimates (problems, proofs, times):
188	pair_probs = {}
189	for (p, _, _, _) in problems:
190		pair_probs[p.pairing] = p
191	print
192	print 'Timing estimate info: (nodes, loops, loop nodes, proof nodes, time)'
193	for pair in pair_probs:
194		time = times[pair]
195		p = pair_probs[pair]
196		print '  %d %d %d %d %0.2f' % (problem_difficult_estimate (p)
197			+ (len (proofs[pair].all_subproofs ()), )
198			+ (time, ))
199
200def print_total_time (times):
201	time_vals = sorted (times.values ())
202	import datetime
203	def strs (seconds):
204		return (seconds, str (datetime.timedelta (seconds = int (seconds))))
205	print 'Slowest problem: %ss (%s)' % strs (time_vals[-1])
206	print 'Total time: %ss (%s)' % strs (sum (time_vals))
207
208def do_all (fname):
209	proofs = scan_proofs (open (fname))
210	problems = all_problems (proofs)
211	times = scan_times (open (fname))
212
213	split_problems = filter_split_problems (problems)
214	data = problems_with_linear_splits (split_problems)
215
216	tabulate_example_traces (split_problems, data)
217	tabulate_problems_with_linear_splits (data)
218
219	print_total_time (times)
220
221	tabulate_timing_estimates (problems, proofs, times)
222
223
224