Lines Matching defs:hit
507 This is the 'hit list' for the new clause generated by (l,s). If we
508 ever see the same hit list for another new clause C generated by an
515 have two kinds of hits: one as before (called an Id hit); and one for
516 when we get a hit by applying symmetry to the (dis)equality literal
517 (called a Sym hit). So now we get a list like:
521 But this gives the same new clause as the hit list
525 so we always normalize the hit list by flipping Ids and Syms (if
526 necessary) to make the first hit an Id.
531 clause. If M was the largest, then keep the first hit an Id. If N was
532 the largest, then make the first hit a Sym. If in the previous step we
533 had to flip all the hits to make the first hit an Id, then flip this
534 first hit too.
538 datatype hit = Id | Sym | Miss;
543 fun hit _ [] _ = Miss | hit a (h :: t) x = if h = x then a else hit Sym t x;
550 fun calc_hits lr targs lits = norm_hits lr (map (hit Id targs) lits);