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