Lines Matching defs:visit
339 visit = ((point, restrs), tag)
340 true_hyps = hyps + [pc_true_hyp (visit)]
341 false_hyps = hyps + [pc_false_hyp (visit)]
362 def split_visit_one_visit (tag, details, restrs, visit):
371 if visit.kind == 'Offset':
372 visit = vc_offs (visit.n * step)
374 visit = vc_num (seq_start + (visit.n * step))
376 visit = ((split, ((split, visit), ) + restrs), tag)
377 return visit
379 def split_visit_visits (tags, split, restrs, visit):
383 l_visit = split_visit_one_visit (ltag, l_details, restrs, visit)
384 r_visit = split_visit_one_visit (rtag, r_details, restrs, visit)
388 def split_hyps_at_visit (tags, split, restrs, visit):
393 (l_visit, r_visit) = split_visit_visits (tags, split, restrs, visit)
401 return logic.inst_eq_at_visit (exp, visit)
403 if visit.kind == 'Number':
404 lsub = mksub (mk_word32 (visit.n))
407 mk_word32 (visit.n)))
489 def visit (vc):
492 # this cannot be more uniform because the representation of visit
501 init_check = [(hyps, pc_true_hyp (visit (min_vc)),
508 # thus we show that this visit is impossible
510 top_check = (hyps, pc_false_hyp (visit (top_vc)),
533 'Induct check at visit %d: %s' % (i, desc)))
571 visit = split_visit_one_visit (tag, details, restrs, visit_num)
584 hyps = [(Hyp ('PCImp', visit, start), '%s pc imp' % tag)]
585 hyps += [(eq_hyp ((zsub (exp), start), (isub (exp), visit),
629 visit = split_visit_one_visit (tag, details, restrs, vc_offs (0))
630 return eq_hyp ((mk_var ('%n', word32T), visit),
631 (mk_word32 (n), visit), (split, 0))