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