Theory IsaSAT_VDom_LLVM

theory IsaSAT_VDom_LLVM
  imports IsaSAT_VDom IsaSAT_Stats_LLVM IsaSAT_Clauses_LLVM IsaSAT_Arena_Sorting_LLVM
begin
hide_const (open) NEMonad.ASSERT NEMonad.RETURN NEMonad.SPEC
type_synonym aivdom2 = ‹vdom × vdom × vdom›
abbreviation aivdom_int_rel :: ‹(aivdom2 × aivdom) set› where
  ‹aivdom_int_rel ≡ {(a, (_, a')). (a,a') ∈ ⟨nat_rel⟩list_rel ×⇩r ⟨nat_rel⟩list_rel ×⇩r ⟨nat_rel⟩list_rel}›

abbreviation aivdom_rel :: ‹(aivdom2 × isasat_aivdom) set› where
  ‹aivdom_rel ≡ ⟨aivdom_int_rel⟩code_hider_rel›

abbreviation aivdom_int_assn :: ‹aivdom2 ⇒ _ ⇒ assn› where
  ‹aivdom_int_assn ≡ LBD_it.arr_assn ×⇩a LBD_it.arr_assn  ×⇩a LBD_it.arr_assn›
type_synonym aivdom_assn = ‹vdom_fast_assn × vdom_fast_assn × vdom_fast_assn›
definition aivdom_assn :: ‹isasat_aivdom ⇒ _ ⇒ assn› where
  ‹aivdom_assn = code_hider_assn aivdom_int_assn aivdom_int_rel›

text ‹To keep my sanity, I use the same name, even if the function drops one component.›
definition add_learned_clause_aivdom_int where
  ‹add_learned_clause_aivdom_int = (λ C (avdom, ivdom). (avdom @ [C], ivdom))›

definition add_learned_clause_aivdom_strong_int where
  ‹add_learned_clause_aivdom_strong_int = (λ C (avdom, ivdom, tvdom). (avdom @ [C], ivdom, tvdom @ [C]))›

definition add_init_clause_aivdom_strong_int where
  ‹add_init_clause_aivdom_strong_int = (λ C (avdom, ivdom, tvdom). (avdom, ivdom @ [C], tvdom @ [C]))›

definition remove_inactive_aivdom_int :: ‹_ ⇒ aivdom2 ⇒ aivdom2› where
  ‹remove_inactive_aivdom_int = (λi (avdom, ivdom). (delete_index_and_swap avdom i, ivdom))›

definition remove_inactive_aivdom_tvdom_int :: ‹_ ⇒ aivdom2 ⇒ aivdom2› where
  ‹remove_inactive_aivdom_tvdom_int = (λi (avdom, ivdom, tvdom). (avdom, ivdom, delete_index_and_swap tvdom i))›

definition avdom_aivdom_at_int :: ‹aivdom2 ⇒ nat ⇒ nat› where
  ‹avdom_aivdom_at_int = (λ(b,c) C. b ! C)›

definition tvdom_aivdom_at_int :: ‹aivdom2 ⇒ nat ⇒ nat› where
  ‹tvdom_aivdom_at_int = (λ(b,c,d) C. d ! C)›


definition length_ivdom_aivdom_int :: ‹aivdom2 ⇒ nat› where
  ‹length_ivdom_aivdom_int = (λ(b,c,d). length c)›

definition ivdom_aivdom_at_int :: ‹aivdom2 ⇒ nat ⇒ nat› where
  ‹ivdom_aivdom_at_int = (λ(b,c,d) C. c ! C)›

definition length_tvdom_aivdom_int :: ‹aivdom2 ⇒ nat› where
  ‹length_tvdom_aivdom_int = (λ(b,c,d). length d)›

definition length_avdom_aivdom_int :: ‹aivdom2 ⇒ nat› where
  ‹length_avdom_aivdom_int = (λ(b,c,d). length b)›

definition AIVDom_int :: ‹_ ⇒ _ ⇒ _ ⇒ _ ⇒ aivdom2› where
  ‹AIVDom_int _ avdom ivdom tvdom = (avdom, ivdom, tvdom)›

definition swap_avdom_aivdom_int :: ‹aivdom2 ⇒ nat ⇒ nat ⇒ aivdom2› where
  ‹swap_avdom_aivdom_int = (λ(avdom, ivdom, tvdom) i j.
  (swap avdom i j, ivdom, tvdom))›

lemma swap_avdom_aivdom_alt_def:
  ‹swap_avdom_aivdom aivdom i j =
  (AIvdom (get_vdom_aivdom aivdom, swap (get_avdom_aivdom aivdom) i j, get_ivdom_aivdom aivdom, get_tvdom_aivdom aivdom))›
  by (cases aivdom) auto

definition take_avdom_aivdom_int :: ‹nat ⇒ aivdom2 ⇒ aivdom2› where
  ‹take_avdom_aivdom_int = (λi (avdom, ivdom, tvdom).
  (take i avdom, ivdom, tvdom))›

lemma take_avdom_aivdom_alt_def:
  ‹take_avdom_aivdom i aivdom =
  (AIvdom (get_vdom_aivdom aivdom, take i (get_avdom_aivdom aivdom), get_ivdom_aivdom aivdom, get_tvdom_aivdom aivdom))›
  by (cases aivdom) auto

definition map_vdom_aivdom_int :: ‹_ ⇒ aivdom2 ⇒ aivdom2 nres› where
  ‹map_vdom_aivdom_int f = (λ(avdom, ivdom, tvdom). do {
    avdom ← f avdom;
    RETURN ((avdom, ivdom, tvdom))
  })›

definition map_tvdom_aivdom_int :: ‹_ ⇒ aivdom2 ⇒ aivdom2 nres› where
  ‹map_tvdom_aivdom_int f = (λ(avdom, ivdom, tvdom). do {
    tvdom ← f tvdom;
    RETURN ((avdom, ivdom, tvdom))
  })›

definition empty_aivdom_int where
  ‹empty_aivdom_int = (λ(avdom, ivdom, tvdom). (take 0 avdom, take 0 ivdom, take 0 tvdom))›

definition AIvdom_init_int :: ‹nat list ⇒ nat list ⇒ nat list ⇒ aivdom2› where
   ‹AIvdom_init_int vdom avdom ivdom = (avdom, ivdom, vdom)›

definition empty_tvdom_int where
  ‹empty_tvdom_int = (λ(avdom, ivdom, tvdom). (avdom, ivdom, take 0 tvdom))›

definition push_to_tvdom_int :: ‹nat ⇒ aivdom2 ⇒ aivdom2› where
  ‹push_to_tvdom_int C =  (λ(avdom, ivdom, tvdom). (avdom, ivdom, tvdom @ [C]))›

lemma
  add_learned_clause_aivdom_int:
  ‹(uncurry (RETURN oo add_learned_clause_aivdom_int), uncurry (RETURN oo add_learned_clause_aivdom)) ∈ nat_rel ×⇩f aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel› and
  add_learned_clause_aivdom_strong_int:
  ‹(uncurry (RETURN oo add_learned_clause_aivdom_strong_int), uncurry (RETURN oo add_learned_clause_aivdom_strong)) ∈ nat_rel ×⇩f aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel› and
  add_init_clause_aivdom_strong_int:
  ‹(uncurry (RETURN oo add_init_clause_aivdom_strong_int), uncurry (RETURN oo add_init_clause_aivdom_strong)) ∈ nat_rel ×⇩f aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel› and
  remove_inactive_aivdom_int:
  ‹(uncurry (RETURN oo remove_inactive_aivdom_int), uncurry (RETURN oo remove_inactive_aivdom)) ∈ nat_rel ×⇩f aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel› and
  remove_inactive_aivdom_tvdom_int:
  ‹(uncurry (RETURN oo remove_inactive_aivdom_tvdom_int), uncurry (RETURN oo remove_inactive_aivdom_tvdom)) ∈ nat_rel ×⇩f aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel› and
  avdom_aivdom_at_int:
  ‹(uncurry (RETURN oo avdom_aivdom_at_int), uncurry (RETURN oo avdom_aivdom_at)) ∈ aivdom_rel ×⇩f nat_rel →⇩f ⟨nat_rel⟩nres_rel›and
  tvdom_aivdom_at_int:
  ‹(uncurry (RETURN oo tvdom_aivdom_at_int), uncurry (RETURN oo tvdom_aivdom_at)) ∈ aivdom_rel ×⇩f nat_rel →⇩f ⟨nat_rel⟩nres_rel›and
  ivdom_aivdom_at_int:
  ‹(uncurry (RETURN oo ivdom_aivdom_at_int), uncurry (RETURN oo ivdom_aivdom_at)) ∈ aivdom_rel ×⇩f nat_rel →⇩f ⟨nat_rel⟩nres_rel›and
  length_avdom_aivdom_int:
  ‹(RETURN o length_avdom_aivdom_int, RETURN o length_avdom_aivdom) ∈ aivdom_rel →⇩f ⟨nat_rel⟩nres_rel›and
  length_ivdom_aivdom_int:
  ‹(RETURN o length_ivdom_aivdom_int, RETURN o length_ivdom_aivdom) ∈ aivdom_rel →⇩f ⟨nat_rel⟩nres_rel› and
  length_tvdom_aivdom_int:
  ‹(RETURN o length_tvdom_aivdom_int, RETURN o length_tvdom_aivdom) ∈ aivdom_rel →⇩f ⟨nat_rel⟩nres_rel› and
  empty_aivdom_int:
  ‹(RETURN o empty_aivdom_int, RETURN o empty_aivdom) ∈ aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel› and
  empty_tvdom_int:
  ‹(RETURN o empty_tvdom_int, RETURN o empty_tvdom) ∈ aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel› and
  push_to_tvdom_int:
  ‹(uncurry (RETURN oo push_to_tvdom_int), uncurry (RETURN oo push_to_tvdom)) ∈ nat_rel ×⇩f aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel› and
  AIvdom_init_int:
  ‹(uncurry2 (RETURN ooo AIvdom_init_int), uncurry2 (RETURN ooo AIvdom_init)) ∈ ⟨nat_rel⟩list_rel ×⇩f ⟨nat_rel⟩list_rel ×⇩f ⟨nat_rel⟩list_rel  →⇩f ⟨aivdom_rel⟩nres_rel› and
  map_vdom_aivdom_int:
  ‹(map_vdom_aivdom_int f, map_vdom_aivdom f) ∈ aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel› and
  map_tvdom_aivdom_int:
  ‹(map_tvdom_aivdom_int f, map_tvdom_aivdom f) ∈ aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel› and
  swap_avdom_aivdom_int:
  ‹(uncurry2 (RETURN ooo swap_avdom_aivdom_int), uncurry2 (RETURN ooo swap_avdom_aivdom))
  ∈ aivdom_rel ×⇩f nat_rel ×⇩f nat_rel  →⇩f ⟨aivdom_rel⟩nres_rel› and
  take_avdom_aivdom_int:
  ‹(uncurry (RETURN oo take_avdom_aivdom_int), uncurry (RETURN oo take_avdom_aivdom))
  ∈ nat_rel ×⇩f aivdom_rel  →⇩f ⟨aivdom_rel⟩nres_rel›
  apply (auto intro!: frefI nres_relI simp: code_hider_rel_def add_learned_clause_aivdom_def remove_inactive_aivdom_def avdom_aivdom_at_alt_def
    ivdom_aivdom_at_alt_def vdom_aivdom_at_alt_def length_vdom_aivdom_alt_def length_avdom_aivdom_alt_def length_ivdom_aivdom_alt_def length_tvdom_aivdom_alt_def tvdom_aivdom_at_alt_def add_learned_clause_aivdom_int_def
    IsaSAT_VDom.add_learned_clause_aivdom_strong_int_def add_learned_clause_aivdom_strong_def add_learned_clause_aivdom_strong_int_def
    IsaSAT_VDom.add_init_clause_aivdom_strong_int_def add_init_clause_aivdom_strong_def add_init_clause_aivdom_strong_int_def
    add_init_clause_aivdom_def add_init_clause_aivdom_int_def
    IsaSAT_VDom.add_learned_clause_aivdom_int_def
    IsaSAT_VDom.remove_inactive_aivdom_int_def remove_inactive_aivdom_int_def
    IsaSAT_VDom.remove_inactive_aivdom_tvdom_int_def remove_inactive_aivdom_tvdom_int_def
      remove_inactive_aivdom_tvdom_def
    IsaSAT_VDom.avdom_aivdom_at_int_def avdom_aivdom_at_int_def
    IsaSAT_VDom.tvdom_aivdom_at_int_def tvdom_aivdom_at_int_def
    IsaSAT_VDom.ivdom_aivdom_at_int_def ivdom_aivdom_at_int_def
    IsaSAT_VDom.length_avdom_aivdom_int_def length_avdom_aivdom_int_def
    IsaSAT_VDom.length_ivdom_aivdom_int_def length_ivdom_aivdom_int_def
    IsaSAT_VDom.length_tvdom_aivdom_int_def length_tvdom_aivdom_int_def
    IsaSAT_VDom_LLVM.empty_aivdom_int_def empty_aivdom_def IsaSAT_VDom.empty_aivdom_int_def
    map_vdom_aivdom_def map_vdom_aivdom_int_def
    AIvdom_init_int_def AIvdom_init_def map_tvdom_aivdom_int_def map_tvdom_aivdom_def
    push_to_tvdom_int_def push_to_tvdom_def IsaSAT_VDom.push_to_tvdom_int_def
    swap_avdom_aivdom_alt_def empty_tvdom_def empty_tvdom_int_def)
  apply (case_tac y; case_tac "f ab"; auto simp: swap_avdom_aivdom_int_def take_avdom_aivdom_int_def
     RES_RETURN_RES conc_fun_RES)[]
  apply (case_tac y; case_tac "f ba"; auto simp: swap_avdom_aivdom_int_def take_avdom_aivdom_int_def
     RES_RETURN_RES conc_fun_RES)[]
   apply (case_tac ab; auto simp: swap_avdom_aivdom_int_def take_avdom_aivdom_int_def)
   apply (case_tac ba; auto simp: swap_avdom_aivdom_int_def take_avdom_aivdom_int_def)
   done

sepref_def add_learned_clause_aivdom_impl
  is ‹uncurry (RETURN oo add_learned_clause_aivdom_int)›
  :: ‹[λ(C,(a,b,c)). Suc (length (a)) < max_snat 64]⇩a sint64_nat_assn⇧k *⇩a aivdom_int_assn⇧d → aivdom_int_assn›
  unfolding add_learned_clause_aivdom_int_def
  by sepref

sepref_def add_learned_clause_aivdom_strong_impl
  is ‹uncurry (RETURN oo add_learned_clause_aivdom_strong_int)›
  :: ‹[λ(C,(a,b,c)). Suc (length (a)) < max_snat 64 ∧ Suc (length (c)) < max_snat 64]⇩a sint64_nat_assn⇧k *⇩a aivdom_int_assn⇧d → aivdom_int_assn›
  unfolding add_learned_clause_aivdom_strong_int_def
  by sepref

sepref_def add_init_clause_aivdom_strong_impl
  is ‹uncurry (RETURN oo add_init_clause_aivdom_strong_int)›
  :: ‹[λ(C,(a,b,c)). Suc (length (b)) < max_snat 64 ∧ Suc (length (c)) < max_snat 64]⇩a sint64_nat_assn⇧k *⇩a aivdom_int_assn⇧d → aivdom_int_assn›
  unfolding add_init_clause_aivdom_strong_int_def
  by sepref

sepref_def remove_inactive_aivdom_impl
  is ‹uncurry (RETURN oo remove_inactive_aivdom_int)›
  :: ‹[λ(C,(a,b,c)). C < (length a)]⇩a sint64_nat_assn⇧k *⇩a aivdom_int_assn⇧d → aivdom_int_assn›
  unfolding remove_inactive_aivdom_int_def
  by sepref

sepref_def remove_inactive_aivdom_tvdom_impl
  is ‹uncurry (RETURN oo remove_inactive_aivdom_tvdom_int)›
  :: ‹[λ(C,(a,b,c)). C < (length c)]⇩a sint64_nat_assn⇧k *⇩a aivdom_int_assn⇧d → aivdom_int_assn›
  unfolding remove_inactive_aivdom_tvdom_int_def
  by sepref

sepref_def ivdom_aivdom_at_impl
  is ‹uncurry (RETURN oo ivdom_aivdom_at_int)›
  :: ‹[λ((b,c,d), C). C < (length c)]⇩a aivdom_int_assn⇧k *⇩a sint64_nat_assn⇧k  → sint64_nat_assn›
  unfolding ivdom_aivdom_at_int_def
  by sepref

sepref_def avdom_aivdom_at_impl
  is ‹uncurry (RETURN oo avdom_aivdom_at_int)›
  :: ‹[λ((b,c), C). C < (length b)]⇩a aivdom_int_assn⇧k *⇩a sint64_nat_assn⇧k  → sint64_nat_assn›
  unfolding avdom_aivdom_at_int_def
  by sepref

sepref_def tvdom_aivdom_at_impl
  is ‹uncurry (RETURN oo tvdom_aivdom_at_int)›
  :: ‹[λ((b,c,d), C). C < (length d)]⇩a aivdom_int_assn⇧k *⇩a sint64_nat_assn⇧k  → sint64_nat_assn›
  unfolding tvdom_aivdom_at_int_def
  by sepref

sepref_def length_avdom_aivdom_impl
  is ‹RETURN o length_avdom_aivdom_int›
  :: ‹aivdom_int_assn⇧k →⇩a sint64_nat_assn›
  unfolding length_avdom_aivdom_int_def
  by sepref


definition workaround_RF where
  ‹workaround_RF xs = length xs›

sepref_def workaround_RF_code [llvm_inline]
  is ‹RETURN o workaround_RF›
  :: ‹vdom_fast_assn⇧k →⇩a sint64_nat_assn›
  unfolding workaround_RF_def
  by sepref


sepref_def length_ivdom_aivdom_impl
  is ‹RETURN o length_ivdom_aivdom_int›
  :: ‹aivdom_int_assn⇧k →⇩a sint64_nat_assn›
  unfolding length_ivdom_aivdom_int_def comp_def workaround_RF_def[symmetric]
  by sepref

sepref_def length_tvdom_aivdom_impl
  is ‹RETURN o length_tvdom_aivdom_int›
  :: ‹aivdom_int_assn⇧k →⇩a sint64_nat_assn›
  unfolding length_tvdom_aivdom_int_def comp_def workaround_RF_def[symmetric]
  by sepref

sepref_def swap_avdom_aivdom_impl
  is ‹uncurry2 (RETURN ooo swap_avdom_aivdom_int)›
  :: ‹[λ(((b,c,d),i), j). i < length b ∧ j < length b]⇩a aivdom_int_assn⇧d *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k → aivdom_int_assn›
  unfolding swap_avdom_aivdom_int_def convert_swap gen_swap
  by sepref

sepref_def take_avdom_aivdom_impl
  is ‹uncurry (RETURN oo take_avdom_aivdom_int)›
  :: ‹[λ(i, (b,c,d)). i ≤ length b]⇩a sint64_nat_assn⇧k *⇩a aivdom_int_assn⇧d → aivdom_int_assn›
  unfolding take_avdom_aivdom_int_def
  by sepref

sepref_def empty_aivdom_impl
  is ‹RETURN o empty_aivdom_int›
  :: ‹aivdom_int_assn⇧d →⇩a aivdom_int_assn›
  unfolding empty_aivdom_int_def
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

sepref_def AIvdom_init_impl
  is ‹uncurry2 (RETURN ooo AIvdom_init_int)›
  :: ‹vdom_fast_assn⇧d *⇩a vdom_fast_assn⇧d *⇩a vdom_fast_assn⇧d  →⇩a aivdom_int_assn›
  unfolding AIvdom_init_int_def
  by sepref

sepref_def empty_tvdom_impl
  is ‹RETURN o empty_tvdom_int›
  :: ‹aivdom_int_assn⇧d →⇩a aivdom_int_assn›
  unfolding empty_tvdom_int_def
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

sepref_def push_tvdom_impl
  is ‹uncurry (RETURN oo push_to_tvdom_int)›
  :: ‹[λ(C,(_,_,tv)). Suc (length tv) < max_snat 64]⇩a
  sint64_nat_assn⇧k *⇩a aivdom_int_assn⇧d → aivdom_int_assn›
  unfolding push_to_tvdom_int_def
  by sepref

lemma aivdom_assn_alt_def:
  ‹aivdom_assn = hr_comp aivdom_int_assn (⟨aivdom_int_rel⟩code_hider_rel)›
  unfolding aivdom_assn_def code_hider_assn_def by auto

context
  notes [fcomp_norm_unfold] = aivdom_assn_alt_def[symmetric] aivdom_assn_def[symmetric]
begin

theorem [sepref_fr_rules]:
  ‹(uncurry add_learned_clause_aivdom_impl, uncurry (RETURN ∘∘ add_learned_clause_aivdom))
∈ [λ(C,ai). Suc (length (get_avdom_aivdom ai)) < max_snat 64]⇩a snat_assn⇧k *⇩a aivdom_assn⇧d → aivdom_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE (nat_rel ×⇩f aivdom_rel) (λ_. True)
   (λx y. case y of (C, a, b, c) ⇒ Suc (length a) < max_snat 64)
   (λx. nofail (uncurry (RETURN ∘∘ add_learned_clause_aivdom) x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF add_learned_clause_aivdom_impl.refine
      add_learned_clause_aivdom_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]] by blast
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹snd x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed

theorem [sepref_fr_rules]:
  ‹(uncurry add_learned_clause_aivdom_strong_impl, uncurry (RETURN ∘∘ add_learned_clause_aivdom_strong))
∈ [λ(C,ai). Suc (length (get_avdom_aivdom ai)) < max_snat 64 ∧ Suc (length (get_tvdom_aivdom ai)) < max_snat 64]⇩a snat_assn⇧k *⇩a aivdom_assn⇧d → aivdom_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE (nat_rel ×⇩f aivdom_rel) (λ_. True)
   (λx y. case y of (C, a, b, c) ⇒ Suc (length a) < max_snat 64 ∧ Suc (length c) < max_snat 64)
   (λx. nofail (uncurry (RETURN ∘∘ add_learned_clause_aivdom_strong) x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF add_learned_clause_aivdom_strong_impl.refine
      add_learned_clause_aivdom_strong_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]] by blast
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹snd x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed

theorem [sepref_fr_rules]:
  ‹(uncurry add_init_clause_aivdom_strong_impl, uncurry (RETURN ∘∘ add_init_clause_aivdom_strong))
∈ [λ(C,ai). Suc (length (get_ivdom_aivdom ai)) < max_snat 64 ∧ Suc (length (get_tvdom_aivdom ai)) < max_snat 64]⇩a snat_assn⇧k *⇩a aivdom_assn⇧d → aivdom_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE (nat_rel ×⇩f aivdom_rel) (λ_. True)
   (λx y. case y of (C, a, b, c) ⇒ Suc (length b) < max_snat 64 ∧ Suc (length c) < max_snat 64)
   (λx. nofail (uncurry (RETURN ∘∘ add_init_clause_aivdom_strong) x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF add_init_clause_aivdom_strong_impl.refine
      add_init_clause_aivdom_strong_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]] by blast
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹snd x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed

theorem [sepref_fr_rules]:
  ‹(uncurry remove_inactive_aivdom_impl, uncurry (RETURN ∘∘ remove_inactive_aivdom))
∈ [λ(C,ai). C < (length (get_avdom_aivdom ai)) ]⇩a snat_assn⇧k *⇩a aivdom_assn⇧d → aivdom_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE
   (nat_rel ×⇩f aivdom_rel)
   (λ_. True) (λx y. case y of (C, a, b, c) ⇒ C < length a)
   (λx. nofail (uncurry (RETURN ∘∘ remove_inactive_aivdom) x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF remove_inactive_aivdom_impl.refine
      remove_inactive_aivdom_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]] by blast
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹snd x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed

theorem [sepref_fr_rules]:
  ‹(uncurry remove_inactive_aivdom_tvdom_impl, uncurry (RETURN ∘∘ remove_inactive_aivdom_tvdom))
∈ [λ(C,ai). C < (length (get_tvdom_aivdom ai))]⇩a snat_assn⇧k *⇩a aivdom_assn⇧d → aivdom_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE
   (nat_rel ×⇩f aivdom_rel)
   (λ_. True) (λx y. case y of (C, a, b, c) ⇒ C < length c)
   (λx. nofail (uncurry (RETURN ∘∘ remove_inactive_aivdom_tvdom) x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF remove_inactive_aivdom_tvdom_impl.refine
      remove_inactive_aivdom_tvdom_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]]
    by blast
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹snd x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed


theorem avdom_aivdom_at_impl_refine[sepref_fr_rules]:
  ‹(uncurry avdom_aivdom_at_impl, uncurry (RETURN ∘∘ avdom_aivdom_at))
∈ [λ(ai, C). C < (length (get_avdom_aivdom ai)) ]⇩a aivdom_assn⇧k *⇩a sint64_nat_assn⇧k → sint64_nat_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE
    (aivdom_rel ×⇩f nat_rel)
    (λ_. True) (λx y. case y of (x, xa) ⇒ (case x of (b, c) ⇒ λC. C < length b) xa)
    (λx. nofail
    (uncurry (RETURN ∘∘ avdom_aivdom_at) x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF avdom_aivdom_at_impl.refine
      avdom_aivdom_at_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]] by simp
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹fst x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed


theorem ivdom_aivdom_at_impl_refine[sepref_fr_rules]:
  ‹(uncurry ivdom_aivdom_at_impl, uncurry (RETURN ∘∘ ivdom_aivdom_at))
∈ [λ(ai, C). C < (length (get_ivdom_aivdom ai)) ]⇩a aivdom_assn⇧k *⇩a sint64_nat_assn⇧k → sint64_nat_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE
    (⟨aivdom_int_rel⟩code_hider_rel ×⇩f nat_rel)
    (λ_. True) (λx y. case y of (x, xa) ⇒ (case x of (b, c, d) ⇒ λC. C < length c) xa)
    (λx. nofail
    (uncurry (RETURN ∘∘ ivdom_aivdom_at) x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF ivdom_aivdom_at_impl.refine
      ivdom_aivdom_at_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]] by simp
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹fst x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed


theorem tvdom_aivdom_at_impl_refine[sepref_fr_rules]:
  ‹(uncurry tvdom_aivdom_at_impl, uncurry (RETURN ∘∘ tvdom_aivdom_at))
∈ [λ(ai, C). C < (length (get_tvdom_aivdom ai)) ]⇩a aivdom_assn⇧k *⇩a sint64_nat_assn⇧k → sint64_nat_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE
   (aivdom_rel ×⇩f nat_rel)
   (λ_. True) (λx y. case y of (x, xa) ⇒ (case x of (b, c, d) ⇒ λC. C < length d) xa)
   (λx. nofail
      (uncurry (RETURN ∘∘ tvdom_aivdom_at) x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF tvdom_aivdom_at_impl.refine
      tvdom_aivdom_at_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]] by blast
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹fst x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed


theorem [sepref_fr_rules]:
  ‹(uncurry take_avdom_aivdom_impl, uncurry (RETURN ∘∘ take_avdom_aivdom))
∈ [λ(C, ai). C ≤ length (get_avdom_aivdom ai)]⇩a sint64_nat_assn⇧k *⇩a aivdom_assn⇧d → aivdom_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE (nat_rel ×⇩f aivdom_rel) (λ_. True)
    (λx y. case y of (i, b, c, d) ⇒ i ≤ length b)
    (λx. nofail (uncurry (RETURN ∘∘ take_avdom_aivdom) x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF take_avdom_aivdom_impl.refine
      take_avdom_aivdom_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]] by blast
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹snd x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed


theorem push_tvdom_impl_refine[sepref_fr_rules]:
  ‹(uncurry push_tvdom_impl, uncurry (RETURN ∘∘ push_to_tvdom))
∈ [λ(C, ai). Suc (length (get_tvdom_aivdom ai)) < max_snat 64]⇩a sint64_nat_assn⇧k *⇩a aivdom_assn⇧d → aivdom_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE (nat_rel ×⇩f aivdom_rel) (λ_. True)
   (λx y. case y of (C, uu_, uua_, tv) ⇒ Suc (length tv) < max_snat 64)
   (λx. nofail (uncurry (RETURN ∘∘ push_to_tvdom) x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF push_tvdom_impl.refine
      push_to_tvdom_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]] by blast
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹snd x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed

theorem swap_avdom_aivdom_impl_refine[sepref_fr_rules]:
  ‹(uncurry2 swap_avdom_aivdom_impl, uncurry2 (RETURN ooo swap_avdom_aivdom))
  ∈ [λ((ai, i), j). i < length (get_avdom_aivdom ai) ∧ j < length (get_avdom_aivdom ai)]⇩a
  aivdom_assn⇧d   *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k → aivdom_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE (aivdom_rel ×⇩f nat_rel ×⇩f nat_rel) (λ_. True)
    (λx y. case y of
     (x, xa) ⇒
       (case x of
        (x, xa) ⇒
       (case x of
        (b, c, d) ⇒ λi j. i < length b ∧ j < length b)
        xa)
        xa)
    (λx. nofail
    (uncurry2 (RETURN ∘∘∘ swap_avdom_aivdom)
      x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a _ → _›)
    using hfref_compI_PRE[OF swap_avdom_aivdom_impl.refine
      swap_avdom_aivdom_int, unfolded fcomp_norm_unfold aivdom_assn_alt_def[symmetric]] by blast
  have pre: ‹?pre' = ?pre› for x h
    by (intro ext, rename_tac x, case_tac x, case_tac ‹fst (fst x)›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    using H
    unfolding pre
    by blast
qed

lemma aivdom_int_assn_alt_def:
  ‹aivdom_int_assn = hr_comp aivdom_int_assn
  (⟨nat_rel⟩list_rel ×⇩f (⟨nat_rel⟩list_rel ×⇩f ⟨nat_rel⟩list_rel))›
  by auto

sepref_register swap_avdom_aivdom take_avdom_aivdom add_init_clause_aivdom_strong add_learned_clause_aivdom_strong
  add_learned_clause_aivdom

lemma vdom_fast_assn_alt_def: ‹vdom_fast_assn = hr_comp LBD_it.arr_assn (⟨nat_rel⟩list_rel)›
  by auto

lemmas vdom_ref[sepref_fr_rules] =
  length_avdom_aivdom_impl.refine[FCOMP length_avdom_aivdom_int]
  length_ivdom_aivdom_impl.refine[FCOMP length_ivdom_aivdom_int]
  length_tvdom_aivdom_impl.refine[FCOMP length_tvdom_aivdom_int]
  hn_id[FCOMP Constructor_hnr[of aivdom_int_rel], of aivdom_int_assn,
  unfolded aivdom_assn_alt_def[symmetric] aivdom_assn_def[symmetric] aivdom_int_assn_alt_def[symmetric]]
    hn_id[FCOMP get_content_hnr[of aivdom_int_rel], of aivdom_int_assn,
  unfolded aivdom_assn_alt_def[symmetric] aivdom_assn_def[symmetric] aivdom_int_assn_alt_def[symmetric]]
  empty_aivdom_impl.refine[FCOMP empty_aivdom_int]
  AIvdom_init_impl.refine[FCOMP AIvdom_init_int, unfolded vdom_fast_assn_alt_def[symmetric]]
  empty_tvdom_impl.refine[FCOMP empty_tvdom_int]
end

end