Lines Matching defs:moves
339 val moves = append_lists (map (pref o snd) ts)
340 in moves end;
343 fun iterated_register_coalescing graph moves freq is_colourable n = let
351 | move_related ((x,y)::moves) = x::y::move_related moves
356 fun merge_vertexes x y (graph,moves,joined) = let
362 val moves = filter (fn z => not (z = (x,y))) moves
363 val moves = map (fn (z1,z2) => (if z1 = y then x else z1,if z2 = y then x else z2)) moves
365 in (graph,moves,joined) end;
366 fun delete_vertex w (graph,moves,joined) = let
369 val moves = filter (fn (x,y) => not (x = w) andalso not (y = w)) moves
370 in (graph,moves,joined) end;
373 fun build_stack graph moves joined n result =
376 val ms = move_related moves
382 val (graph,moves,joined) = delete_vertex w (graph,moves,joined)
384 in build_stack graph moves joined n ((w,"r")::result) end handle HOL_ERR _ =>
385 (* coalescing: ?x y. (x,y) IN moves and degree (x UNION y) < n, then combine x,y *) let
388 val moves2 = filter (fn (x,y) => not (mem x (list_find y graph))) moves
395 val (graph,moves,joined) = merge_vertexes x y (graph,moves,joined)
397 in build_stack graph moves joined n result end handle HOL_ERR _ =>
399 val ((x,y),moves) = if moves = [] then fail () else (hd moves,tl moves)
401 in build_stack graph moves joined n result end handle HOL_ERR _ =>
407 val (graph,moves,joined) = delete_vertex w (graph,moves,joined)
409 in build_stack graph moves joined n ((w,"s")::result) end handle HOL_ERR _ =>
411 val (stack,joined) = build_stack graph moves [] n []
415 fun score c = foldr (op +) 0 (map (fn (x,y) => if c x = c y then 1 else 0) moves)
484 val moves = move_assignments ts graph
487 val colouring = iterated_register_coalescing graph moves freq is_colourable n
527 alternatively augment 'moves' to have artificial (x,y) edge
559 val moves = n_filter (i div max) edges
560 in (adj qs ts, moves) end;
563 val (graph,moves) = get_graph i
568 val ok = (iterated_register_coalescing graph moves freq is_colourable n; true)