1# 2# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3# 4# SPDX-License-Identifier: BSD-2-Clause 5# 6 7# a collection of commands that are useful to copy into 8# the python interpreter to diagnose issues 9 10 11# pick out the last problem 12 13p = problem.last_problem[0] 14p.save_graph ('diagram.dot') 15import os 16os.spawnvp (os.P_WAIT, 'dot', ['dot', '-Tsvg', 'diagram.dot', '-o', 'diagram.svg']) 17 18# pick out a model for the last failure 19 20rep = rep_graph.mk_graph_slice (p) 21(fld_hyp, assum_hyps, requests) = rep_graph.last_failed_test[0] 22rep_graph.run_requests (rep, requests) 23m = {} 24assert not rep.test_hyp_whyps (fld_hyp, assum_hyps, model = m) 25sat_hyps = solver.last_satisfiable_hyps[0] 26 27# trace a model 28 29import debug 30for tag in reversed (p.pairing.tags): 31 print 'Debug walk for %s' % tag 32 debug.walk_model (rep, tag, m) 33 34debug.trace_model (rep, m) 35debug.trace_mems (rep, m) 36debug.investigate_funcalls (rep, m) 37 38# investigate a proof failure more broadly 39 40proof = search.last_proof[0] 41checks = check.proof_checks (p, proof) 42failed = [(hyps, hyp, nm) for (hyps, hyp, nm) in checks 43 if not rep.test_hyp_imp (hyps, hyp)] 44check.failed_test_sets (p, checks) 45 46# investigate a loop search failure 47 48knowledge = search.last_knowledge[0] 49(rep,(restrs, loop_elts, cand_r_loop_elts, premise), (pairs, vs), facts) = knowledge 50 51calc = search.problem_calculation(knowledge) 52 53# load and reload bits 54 55from syntax import Expr, Type 56 57import logic, stack_logic 58mods = [logic, problem, solver, rep_graph, check, search, stack_logic] 59map (reload, mods) 60 61# try to split the sole loop pair in a problem 62 63assert len (p.loop_heads ()) == 2 64[asm_head] = [sp for sp in p.loop_heads () if p.node_tags[sp][0] == 'ASM'] 65rep = rep_graph.mk_graph_slice (p) 66search.find_split (rep, asm_head, (), check.init_point_hyps(p), [(0, 1)], [(0, 1)], 4) 67if search.last_failed_pairings: 68 fails = dict (search.last_failed_pairings[-1]) 69 70# 'inductive' failures are near-misses in the loop process, 71# created by proof failures. investigate these failures. 72 73ind_fails = [pair for pair in fails if str (fails[pair][1]) == 'InductFailed'] 74if ind_fails: 75 pair = ind_fails[0] 76 (_, _, eqs) = fails[pair] 77 split = search.v_eqs_to_split (p, pair, eqs, (), check.init_point_hyps(p)) 78 check.check_split_induct_step_group (rep, (), check.init_point_hyps(p), split) 79 80 81