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