Theory IsaSAT_Watch_List_LLVM

theory IsaSAT_Watch_List_LLVM
  imports IsaSAT_Watch_List IsaSAT_Literals_LLVM IsaSAT_Arena_Sorting_LLVM
begin

type_synonym watched_wl_uint32 = ‹(64,(64 word × 32 word × 1 word),64)array_array_list›

abbreviation ‹watcher_fast_assn ≡ sint64_nat_assn ×⇩_a unat_lit_assn ×⇩_a bool1_assn   ›
abbreviation ‹watchlist_fast_assn ≡ aal_assn' TYPE(64) TYPE(64) watcher_fast_assn›

lemma [def_pat_rules]: ‹append_ll ≡ op_list_list_push_back›
  by (rule eq_reflection) (auto simp: append_ll_def fun_eq_iff)

sepref_register mop_append_ll mop_arena_length

sepref_def mop_append_ll_impl
  is ‹uncurry2 mop_append_ll›
  :: ‹[λ((W, i), _). length (W ! (nat_of_lit i)) < snat64_max]⇩_a
    watchlist_fast_assn⇧^d *⇩_a unat_lit_assn⇧^k *⇩_a watcher_fast_assn⇧^k → watchlist_fast_assn›
  unfolding mop_append_ll_def
  by sepref

sepref_def rewatch_heur_fast_code
  is ‹uncurry2 (rewatch_heur)›
  :: ‹[λ((vdom, arena), W). (∀x ∈ set vdom. x ≤ snat64_max) ∧ length arena ≤ snat64_max ∧
        length vdom ≤ snat64_max]⇩_a
        vdom_fast_assn⇧^k *⇩_a arena_fast_assn⇧^k *⇩_a watchlist_fast_assn⇧^d → watchlist_fast_assn›
  supply [[goals_limit=1]]
     arena_lit_pre_le_snat64_max[dest] arena_is_valid_clause_idx_le_unat64_max[dest]
  supply [simp] = append_ll_def
  supply [dest] = arena_lit_implI(1)
  unfolding rewatch_heur_alt_def Let_def PR_CONST_def
  unfolding while_eq_nfoldli[symmetric]
  apply (subst while_upt_while_direct, simp)
  unfolding if_not_swap
    FOREACH_cond_def FOREACH_body_def
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

lemma aal_gen_swap:
  ‹W[L := More_List.swap (W ! L) i j] = 
   (let x = W ! L ! i; y = W ! L ! j; W = op_list_list_upd W L j x; W = op_list_list_upd W L i y in W)›
  apply (auto simp: convert_swap More_List.swap_def)
  by (smt (verit, best) list_update_id' list_update_overwrite list_update_swap nth_list_update')

sepref_register watchlist_put_binaries_first_one watchlist_put_binaries_first
sepref_def watchlist_put_binaries_first_one_impl
  is ‹uncurry watchlist_put_binaries_first_one›
  :: ‹watchlist_fast_assn⇧^d *⇩_a sint64_nat_assn⇧^k →⇩_a watchlist_fast_assn›
   unfolding watchlist_put_binaries_first_one_def
   unfolding if_not_swap convert_swap fold_op_list_list_llen
   unfolding
     convert_swap aal_gen_swap fold_op_list_list_idx op_list_get_def
     op_list_set_def fold_op_list_list_upd
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref


sepref_def watchlist_put_binaries_first_impl
  is ‹watchlist_put_binaries_first›
  :: ‹watchlist_fast_assn⇧^d →⇩_a watchlist_fast_assn›
   unfolding watchlist_put_binaries_first_def
   unfolding if_not_swap convert_swap fold_op_list_list_llen
   unfolding
     convert_swap aal_gen_swap fold_op_list_list_idx op_list_get_def
     op_list_set_def  op_list_list_len_def[symmetric]
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

end