Lines Matching refs:tag
76 tag = p.node_tags[n][0]
77 trace ('Finding split limit: %d (%s)' % (n, tag))
95 epc = rep.get_pc (('Err', restrs3), tag = tag)
113 trace ('No split limit found for %d (%s).' % (n, tag))
146 err_pc_hyps = [rep_graph.pc_false_hyp ((('Err', no_loop_restrs), tag))
147 for tag in p.pairing.tags]
174 err_pc_hyps = [rep_graph.pc_false_hyp ((('Err', no_loop_restrs), tag))
175 for tag in p.pairing.tags]
963 for (tag, n, vc) in rep.node_pc_env_order
964 if tag == l_tag
1038 nrerr_pc = mk_not (rep.get_pc (('Err', err_restrs), tag = r_tag))
1244 [tag, _] = knowledge.tags
1246 hyps + [rep_graph.pc_true_hyp ((n_vc, tag)) for n_vc in n_vcs],
1263 [tag, _] = knowledge.tags
1265 tag, m, head)), m)
1291 def eval_pc (rep, m, n_vc, tag = None):
1292 hit = eval_model_expr (m, rep.solv, rep.get_pc (n_vc, tag = tag))
1296 def entry_path (rep, tag, m, head):
1301 if tag2 != tag:
1303 if eval_pc (rep, m, (n, vc), tag):
1307 def entry_path_no_loops (rep, tag, m, head = None):
1308 n_vcs = entry_path (rep, tag, m, head)
1321 tag = rep.p.node_tags[n_vcs[0][0]][0]
1324 mk_thyps = lambda n_vcs: [rep_graph.pc_true_hyp ((n_vc, tag))
1341 return ('CaseSplit', ((n, tag), [n]))
1485 (tag, _) = p.node_tags[split]
1486 checks = (check.single_loop_rev_induct_checks (p, restrs, hyps, tag,
1489 tag, split, large, eqs_assume, pred))
1654 ret_cond = rep.get_pc (('Ret', restrs2), tag = other_tag)