Theory IsaSAT_LBD_LLVM

theory IsaSAT_LBD_LLVM
  imports IsaSAT_LBD IsaSAT_Setup0_LLVM
begin

sepref_register mark_lbd_from_clause_heur get_level_pol mark_lbd_from_list_heur
  mark_lbd_from_conflict mop_arena_status

sepref_def mark_lbd_from_clause_heur_impl
  is ‹uncurry3 mark_lbd_from_clause_heur›
  :: ‹trail_pol_fast_assn⇧k *⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a lbd_assn⇧d →⇩a lbd_assn›
  unfolding mark_lbd_from_clause_heur_def nfoldli_upt_by_while
  apply (rewrite at ‹_ = ⌑› unat_const_fold[where 'a=32])
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

sepref_def calculate_LBD_heur_st_impl
  is ‹uncurry3 calculate_LBD_heur_st›
  :: ‹trail_pol_fast_assn⇧k *⇩a arena_fast_assn⇧d *⇩a lbd_assn⇧d *⇩a sint64_nat_assn⇧k →⇩a
     arena_fast_assn ×⇩a lbd_assn›
  supply [[goals_limit=1]]
  unfolding calculate_LBD_heur_st_def isasat_bounded_assn_def
    fold_tuple_optimizations
  apply (annot_unat_const ‹TYPE(32)›)
  by sepref

sepref_def mark_lbd_from_list_heur_impl
  is ‹uncurry2 mark_lbd_from_list_heur›
  :: ‹trail_pol_fast_assn⇧k *⇩a out_learned_assn⇧k *⇩a lbd_assn⇧d →⇩a lbd_assn›
  supply [[goals_limit=1]]
  unfolding mark_lbd_from_list_heur_def nfoldli_upt_by_while
  apply (rewrite at ‹_ = ⌑› unat_const_fold[where 'a=32])
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref


lemma mark_lbd_from_conflict_alt_def:
  ‹mark_lbd_from_conflict = (λS. do{
     let (M, S) = extract_trail_wl_heur S;
     let (outl, S) = extract_outl_wl_heur S;
     let (lbd, S) = extract_lbd_wl_heur S;
     lbd ← mark_lbd_from_list_heur M outl lbd;
     RETURN (update_lbd_wl_heur lbd (update_trail_wl_heur M (update_outl_wl_heur outl S)))
    })›
  by (auto simp: state_extractors mark_lbd_from_conflict_def split: isasat_int_splits)

sepref_def mark_lbd_from_conflict_impl
  is ‹mark_lbd_from_conflict›
  :: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding mark_lbd_from_conflict_alt_def
  by sepref

lemma update_lbd_pre_arena_act_preD:
  ‹update_lbd_pre ((a, ba), b) ⟹
  arena_act_pre (update_lbd a ba b) a›
  unfolding update_lbd_pre_def arena_act_pre_def prod.simps
  by (auto simp: arena_is_valid_clause_idx_def intro!: valid_arena_update_lbd)

sepref_register update_lbd_and_mark_used
sepref_def update_lbd_and_mark_used_impl
  is ‹uncurry2 (RETURN ooo update_lbd_and_mark_used)›
    :: ‹[update_lbd_pre]⇩a sint64_nat_assn⇧k *⇩a uint32_nat_assn⇧k *⇩a arena_fast_assn⇧d  → arena_fast_assn›
  unfolding update_lbd_and_mark_used_def LBD_SHIFT_def
  supply [dest] = update_lbd_pre_arena_act_preD
  apply (annot_unat_const ‹TYPE(32)›)
  by sepref

sepref_def update_lbd_shrunk_clause_impl
  is ‹uncurry update_lbd_shrunk_clause›
  :: ‹sint64_nat_assn⇧k *⇩a arena_fast_assn⇧d →⇩a arena_fast_assn›
  unfolding update_lbd_shrunk_clause_def
  apply (rewrite  at ‹If (⌑ ≤ _)› annot_unat_snat_upcast[where 'l=64])
  apply (rewrite at ‹If (_ ≤ (_ - ⌑))› snat_const_fold[where 'a=64])
  apply (rewrite at ‹If (_ ≤ _) _ (⌑ - _)› annot_snat_unat_conv)
  apply (rewrite  at ‹If (_ ≤ _) _ (⌑ - _)› annot_unat_unat_downcast[where 'l=32])
  apply (annot_unat_const ‹TYPE(32)›)
  by sepref

end