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