Theory IsaSAT_Initialisation_State_LLVM

theory IsaSAT_Initialisation_State_LLVM
  imports IsaSAT_Initialisation Tuple15_LLVM IsaSAT_Setup_LLVM IsaSAT_Mark_LLVM
    IsaSAT_VMTF_LLVM Watched_Literals.Watched_Literals_Watch_List_Initialisation
    IsaSAT_Mark_LLVM
begin
hide_const (open) NEMonad.RETURN  NEMonad.ASSERT

type_synonym bump_heuristics_init_assn = ‹
  ((32 word ptr × 32 word ptr × 32 word ptr × 32 word ptr × 64 word ptr × 32 word) × 64 word,
  (64 word × 32 word × 32 word) ptr × 64 word × 32 word × 32 word × 32 word,
  1 word, (64 word × 64 word × 32 word ptr) × 1 word ptr) tuple4›

type_synonym vmtf_init = ‹(nat, nat) vmtf_node list × nat × nat option × nat option × nat option›
definition (in -) vmtf_init_assn :: ‹vmtf_init ⇒ _ ⇒ llvm_amemory ⇒ bool› where
  ‹vmtf_init_assn ≡ (array_assn vmtf_node_assn ×a uint64_nat_assn ×a
    atom.option_assn ×a atom.option_assn ×a atom.option_assn)›

type_synonym bump_heuristics_init = ‹((nat,nat)acids, vmtf_init, bool, nat list × bool list) tuple4›

abbreviation Bump_Heuristics_Init :: ‹_ ⇒ _ ⇒ _ ⇒ _ ⇒ bump_heuristics_init› where
  ‹Bump_Heuristics_Init a b c d ≡ Tuple4 a b c d›

definition heuristic_bump_init_assn :: ‹bump_heuristics_init ⇒ bump_heuristics_init_assn ⇒ _› where
  ‹heuristic_bump_init_assn = tuple4_assn acids_assn2 vmtf_init_assn bool1_assn distinct_atoms_assn›

definition bottom_atom where
  ‹bottom_atom = 0›

definition bottom_init_vmtf :: ‹vmtf_init› where
  ‹bottom_init_vmtf = (replicate 0 (VMTF_Node 0 None None), 0, None, None, None)›

definition extract_bump_stable where
  ‹extract_bump_stable = tuple4_state_ops.remove_a empty_acids›
definition extract_bump_focused where
  ‹extract_bump_focused = tuple4_state_ops.remove_b bottom_init_vmtf›

lemma [sepref_fr_rules]: ‹(uncurry0 (Mreturn 0), uncurry0 (RETURN bottom_atom)) ∈ unit_assnk →a atom_assn›
  unfolding bottom_atom_def
  apply sepref_to_hoare
  apply vcg
  apply (auto simp: atom_rel_def unat_rel_def unat.rel_def br_def entails_def ENTAILS_def)
  by (smt (verit, best) pure_true_conv rel_simps(51) sep.add_0)

sepref_def bottom_init_vmtf_code
  is ‹uncurry0 (RETURN bottom_init_vmtf)›
  :: ‹unit_assnk →a vmtf_init_assn›
  unfolding bottom_init_vmtf_def
  apply (rewrite in ‹((⌑, _, _, _, _))› array_fold_custom_replicate)
  unfolding
   atom.fold_option array_fold_custom_replicate vmtf_init_assn_def
    al_fold_custom_empty[where 'l=64]
  apply (rewrite at 0 in ‹VMTF_Node ⌑› unat_const_fold[where 'a=64])
  apply (rewrite at ‹(_, ⌑, _, _)› unat_const_fold[where 'a=64])
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

schematic_goal free_vmtf_remove_assn[sepref_frame_free_rules]: ‹MK_FREE vmtf_init_assn ?a›
  unfolding vmtf_init_assn_def
  by synthesize_free

sepref_def free_vmtf_remove
  is ‹mop_free›
  :: ‹vmtf_init_assnd →a unit_assn›
  by sepref

definition extract_bump_is_focused where
  ‹extract_bump_is_focused = tuple4_state_ops.remove_c False›

definition bottom_atms_hash where
  ‹bottom_atms_hash = ([], replicate 0 False)›

definition extract_bump_atms_to_bump where
  ‹extract_bump_atms_to_bump = tuple4_state_ops.remove_d bottom_atms_hash›

sepref_def bottom_atms_hash_code
  is ‹uncurry0 (RETURN bottom_atms_hash)›
  :: ‹unit_assnk →a distinct_atoms_assn›
  unfolding bottom_atms_hash_def
  unfolding
   atom.fold_option array_fold_custom_replicate
    al_fold_custom_empty[where 'l=64]
  apply (rewrite at ‹(⌑, _)› annotate_assn[where A =‹al_assn atom_assn›])
  apply (rewrite at ‹(_, ⌑)› annotate_assn[where A =‹atoms_hash_assn›])
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

lemma free_vmtf_init_assn_assn2: ‹MK_FREE vmtf_init_assn free_vmtf_remove›
  unfolding free_vmtf_remove_def
  by (rule back_subst[of ‹MK_FREE vmtf_init_assn›, OF free_vmtf_remove_assn])
    (auto intro!: ext)

global_interpretation Bump_Heur_Init: tuple4_state where
  a_assn = acids_assn2 and
  b_assn = vmtf_init_assn and
  c_assn = bool1_assn and
  d_assn = distinct_atoms_assn and
  a_default = empty_acids and
  a = ‹empty_acids_code› and
  a_free = free_acids and
  b_default = bottom_init_vmtf and
  b = ‹bottom_init_vmtf_code› and
  b_free = free_vmtf_remove and
  c_default = False and
  c = ‹bottom_focused› and
  c_free = free_focused and
  d_default = ‹bottom_atms_hash› and
  d = ‹bottom_atms_hash_code› and
  d_free = ‹free_atms_hash_code›
  rewrites
  ‹Bump_Heur_Init.tuple4_int_assn ≡ heuristic_bump_init_assn›and
  ‹Bump_Heur_Init.remove_a ≡ extract_bump_stable› and
  ‹Bump_Heur_Init.remove_b ≡ extract_bump_focused› and
  ‹Bump_Heur_Init.remove_c ≡ extract_bump_is_focused› and
  ‹Bump_Heur_Init.remove_d ≡ extract_bump_atms_to_bump›
  apply unfold_locales
  apply (rule bottom_init_vmtf_code.refine bottom_focused.refine free_acids_assn2
    bottom_atms_hash_code.refine free_vmtf_init_assn_assn2 free_focused_assn2
    free_distinct_atoms_assn2 empty_acids_code.refine free_acids_assn2')+
  subgoal unfolding heuristic_bump_init_assn_def tuple4_state_ops.tuple4_int_assn_def by auto
  subgoal unfolding extract_bump_stable_def by auto
  subgoal unfolding extract_bump_focused_def by auto
  subgoal unfolding extract_bump_is_focused_def by auto
  subgoal unfolding extract_bump_atms_to_bump_def by auto
  done

lemmas [unfolded Tuple4_LLVM.inline_direct_return_node_case, llvm_code] =
  Bump_Heur_Init.code_rules[unfolded Mreturn_comp_Tuple4]

lemmas [sepref_fr_rules] =
  Bump_Heur_Init.separation_rules


type_synonym (in -)twl_st_wll_trail_init =
  ‹(trail_pol_fast_assn, arena_assn, option_lookup_clause_assn,
    64 word, watched_wl_uint32, bump_heuristics_init_assn, phase_saver_assn,
    32 word, cach_refinement_l_assn, lbd_assn, vdom_fast_assn, vdom_fast_assn, 1 word,
  (64 word × 64 word × 64 word × 64 word × 64 word), mark_assn) tuple15›

definition isasat_init_assn
  :: ‹twl_st_wl_heur_init ⇒ twl_st_wll_trail_init ⇒ assn›
where
‹isasat_init_assn = tuple15_assn
  trail_pol_fast_assn arena_fast_assn
  conflict_option_rel_assn
  sint64_nat_assn
  watchlist_fast_assn
  heuristic_bump_init_assn phase_saver_assn
  uint32_nat_assn
  cach_refinement_l_assn
  lbd_assn
  vdom_fast_assn
  vdom_fast_assn
  bool1_assn lcount_assn
  marked_struct_assn›


definition bottom_vdom :: ‹_› where
  ‹bottom_vdom = []›


sepref_def bottom_vdom_code
  is ‹uncurry0 (RETURN bottom_vdom)›
  :: ‹unit_assnk →a vdom_fast_assn›
  supply [[goals_limit=1]]
  unfolding bottom_vdom_def
  unfolding al_fold_custom_empty[where 'l=64]
  by sepref

sepref_def free_vdom
  is ‹mop_free›
  :: ‹vdom_fast_assnd →a unit_assn›
  by sepref


schematic_goal free_vdom[sepref_frame_free_rules]: ‹MK_FREE vdom_fast_assn ?a›
  by synthesize_free

lemma free_vdom2: ‹MK_FREE vdom_fast_assn free_vdom›
  unfolding free_arena_fast_def
  by (rule back_subst[of ‹MK_FREE vdom_fast_assn›, OF free_vdom])
    (auto intro!: ext simp: free_vdom_def)

sepref_def free_phase_saver
  is ‹mop_free›
  :: ‹phase_saver_assnd →a unit_assn›
  by sepref

definition bottom_phase_saver :: ‹phase_saver› where
  ‹bottom_phase_saver = op_larray_custom_replicate 0 False›


sepref_def bottom_phase_saver_code
  is ‹uncurry0 (RETURN bottom_phase_saver)›
  :: ‹unit_assnk →a phase_saver_assn›
  supply [[goals_limit=1]]
  unfolding bottom_phase_saver_def
  unfolding larray_fold_custom_replicate
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

schematic_goal free_phase_saver[sepref_frame_free_rules]: ‹MK_FREE phase_saver_assn ?a›
  by synthesize_free

lemma free_phase_saver2: ‹MK_FREE phase_saver_assn free_phase_saver›
  unfolding free_arena_fast_def
  by (rule back_subst[of ‹MK_FREE phase_saver_assn›, OF free_phase_saver])
    (auto intro!: ext simp: free_phase_saver_def)

definition bottom_init_bump :: ‹bump_heuristics_init› where
  ‹bottom_init_bump = Bump_Heuristics_Init empty_acids bottom_init_vmtf False bottom_atms_hash›

schematic_goal free_vmtf_init_assn[sepref_frame_free_rules]: ‹MK_FREE heuristic_bump_init_assn ?a›
  unfolding heuristic_bump_init_assn_def
  by synthesize_free

sepref_def free_bottom_init_bump_code
  is ‹mop_free›
  :: ‹heuristic_bump_init_assnd →a unit_assn›
  by sepref


lemma free_vmtf_remove2: ‹MK_FREE heuristic_bump_init_assn free_bottom_init_bump_code›
  unfolding free_bottom_init_bump_code_def
  apply (rule back_subst[of ‹MK_FREE heuristic_bump_init_assn›, OF free_vmtf_init_assn])
  apply (auto intro!: ext simp: M_monad_laws)
  by (metis M_monad_laws(1))


definition op_empty_array where
  ‹op_empty_array ≡ []›

lemma [sepref_fr_rules]: ‹(uncurry0 (Mreturn null), uncurry0 (RETURN op_empty_array)) ∈ unit_assnk →a array_assn R›
  unfolding array_assn_def op_empty_array_def
  apply sepref_to_hoare
  apply vcg
  apply (auto simp: array_assn_def ENTAILS_def hr_comp_def[abs_def] Exists_eq_simp
    pure_true_conv narray_assn_null_init)
  done

sepref_def bottom_init_vmtf2_code
  is ‹uncurry0 (RETURN bottom_init_bump)›
  :: ‹unit_assnk →a heuristic_bump_init_assn›
  unfolding bottom_init_bump_def atom.fold_None
  unfolding al_fold_custom_empty[where 'l=64]
  by sepref

definition bottom_bool where
  ‹bottom_bool = False›

sepref_def bottom_bool_code
  is ‹uncurry0 (RETURN bottom_bool)›
  :: ‹unit_assnk →a bool1_assn›
  unfolding bottom_bool_def
  by sepref

sepref_def free_bool
  is ‹mop_free›
  :: ‹bool1_assnd →a unit_assn›
  by sepref

schematic_goal free_bool[sepref_frame_free_rules]: ‹MK_FREE bool1_assn ?a›
  by synthesize_free

lemma free_bool2: ‹MK_FREE bool1_assn free_bool›
  unfolding free_focused_def
  by (rule back_subst[of ‹MK_FREE bool1_assn›, OF free_bool])
    (auto intro!: ext simp: free_bool_def free_focused_def)

definition bottom_marked_struct :: ‹_› where
  ‹bottom_marked_struct = (0, [])›

sepref_def bottom_marked_struct_code
  is ‹uncurry0 (RETURN bottom_marked_struct)›
  :: ‹unit_assnk →a marked_struct_assn›
  unfolding bottom_marked_struct_def marked_struct_assn_def op_empty_array_def[symmetric]
  apply (annot_unat_const ‹TYPE(32)›)
  by sepref

sepref_def free_marked_struct_code
  is ‹mop_free›
  :: ‹marked_struct_assnd →a unit_assn›
  unfolding bottom_marked_struct_def marked_struct_assn_def
  by sepref

schematic_goal free_marked_struct[sepref_frame_free_rules]: ‹MK_FREE marked_struct_assn ?a›
  unfolding marked_struct_assn_def
  by synthesize_free

lemma free_marked_struct2: ‹MK_FREE marked_struct_assn free_marked_struct_code›
  unfolding free_arena_fast_def
  by (rule back_subst[of ‹MK_FREE marked_struct_assn›, OF free_marked_struct])
    (auto intro!: ext simp: free_marked_struct_code_def)

global_interpretation IsaSAT_Init: tuple15_state_ops where
  a_assn = trail_pol_fast_assn and
  b_assn = arena_fast_assn and
  c_assn = conflict_option_rel_assn and
  d_assn = sint64_nat_assn and
  e_assn = watchlist_fast_assn and
  f_assn = heuristic_bump_init_assn and
  g_assn = phase_saver_assn and
  h_assn = uint32_nat_assn and
  i_assn = cach_refinement_l_assn and
  j_assn = lbd_assn and
  k_assn = vdom_fast_assn and
  l_assn = vdom_fast_assn and
  m_assn = bool1_assn and
  n_assn = lcount_assn and
  o_assn = marked_struct_assn and
  a_default = bottom_trail and
  a = ‹bottom_trail_code› and
  b_default = bottom_arena and
  b = ‹bottom_arena_code› and
  c_default = bottom_conflict and
  c = ‹bottom_conflict_code› and
  d_default = ‹bottom_decision_level› and
  d = ‹(bottom_decision_level_code)› and
  e_default = bottom_watchlist and
  e = ‹bottom_watchlist_code› and
  f_default = bottom_init_bump and
  f = ‹bottom_init_vmtf2_code› and
  g_default = bottom_phase_saver and
  g = ‹bottom_phase_saver_code› and
  h_default = bottom_clvls and
  h = ‹bottom_clvls_code›and
  i_default = bottom_ccach and
  i = ‹bottom_ccach_code› and
  j_default = empty_lbd and
  j = ‹empty_lbd_code› and
  k_default = bottom_vdom and
  k = ‹bottom_vdom_code› and
  l_default = bottom_vdom and
  l = ‹bottom_vdom_code› and
  m_default = bottom_bool and
  m = ‹bottom_bool_code› and
  n_default = bottom_lcount and
  n = ‹bottom_lcount_code› and
  ko_default = bottom_marked_struct and
  ko = ‹bottom_marked_struct_code›
(*  rewrites
   ‹IsaSAT_Init.tuple15_int_assn ≡ isasat_init_assn›
  subgoal unfolding isasat_init_assn_def tuple15_state_ops.tuple15_int_assn_def .
*)  .

definition extract_trail_wl_heur_init where
  ‹extract_trail_wl_heur_init = IsaSAT_Init.remove_a›

definition extract_arena_wl_heur_init where
  ‹extract_arena_wl_heur_init = IsaSAT_Init.remove_b›

definition extract_conflict_wl_heur_init where
  ‹extract_conflict_wl_heur_init = IsaSAT_Init.remove_c›

definition extract_literals_to_update_wl_heur_init where
  ‹extract_literals_to_update_wl_heur_init = IsaSAT_Init.remove_d›

definition extract_watchlist_wl_heur_init where
  ‹extract_watchlist_wl_heur_init = IsaSAT_Init.remove_e›

definition extract_vmtf_wl_heur_init where
  ‹extract_vmtf_wl_heur_init = IsaSAT_Init.remove_f›

definition extract_phase_saver_wl_heur_init where
  ‹extract_phase_saver_wl_heur_init = IsaSAT_Init.remove_g›

definition extract_clvls_wl_heur_init where
  ‹extract_clvls_wl_heur_init = IsaSAT_Init.remove_h›

definition extract_ccach_wl_heur_init where
  ‹extract_ccach_wl_heur_init = IsaSAT_Init.remove_i›

definition extract_lbd_wl_heur_init where
  ‹extract_lbd_wl_heur_init = IsaSAT_Init.remove_j›

definition extract_vdom_wl_heur_init where
  ‹extract_vdom_wl_heur_init = IsaSAT_Init.remove_k›

definition extract_ivdom_wl_heur_init where
  ‹extract_ivdom_wl_heur_init = IsaSAT_Init.remove_l›

definition extract_failed_wl_heur_init where
  ‹extract_failed_wl_heur_init = IsaSAT_Init.remove_m›

definition extract_lcount_wl_heur_init where
  ‹extract_lcount_wl_heur_init = IsaSAT_Init.remove_n›

definition extract_marked_wl_heur_init where
  ‹extract_marked_wl_heur_init = IsaSAT_Init.remove_o›

global_interpretation IsaSAT_Init: tuple15_state where
  a_assn = trail_pol_fast_assn and
  b_assn = arena_fast_assn and
  c_assn = conflict_option_rel_assn and
  d_assn = sint64_nat_assn and
  e_assn = watchlist_fast_assn and
  f_assn = heuristic_bump_init_assn and
  g_assn = phase_saver_assn and
  h_assn = uint32_nat_assn and
  i_assn = cach_refinement_l_assn and
  j_assn = lbd_assn and
  k_assn = vdom_fast_assn and
  l_assn = vdom_fast_assn and
  m_assn = bool1_assn and
  n_assn = lcount_assn and
  o_assn = marked_struct_assn and
  a_default = bottom_trail and
  a = ‹bottom_trail_code› and
  a_free = free_trail_pol_fast and
  b_default = bottom_arena and
  b = ‹bottom_arena_code› and
  b_free = free_arena_fast and
  c_default = bottom_conflict and
  c = ‹bottom_conflict_code› and
  c_free = free_conflict_option_rel and
  d_default = ‹bottom_decision_level› and
  d = ‹bottom_decision_level_code› and
  d_free = ‹free_sint64_nat› and
  e_default = bottom_watchlist and
  e = ‹bottom_watchlist_code› and
  e_free = free_watchlist_fast and
  f_default = bottom_init_bump and
  f = ‹bottom_init_vmtf2_code› and
  f_free = free_bottom_init_bump_code and
  g_default = bottom_phase_saver and
  g = ‹bottom_phase_saver_code› and
  g_free = free_phase_saver and
  h_default = bottom_clvls and
  h = ‹bottom_clvls_code›and
  h_free = free_uint32_nat and
  i_default = bottom_ccach and
  i = ‹bottom_ccach_code› and
  i_free = free_cach_refinement_l and
  j_default = empty_lbd and
  j = ‹empty_lbd_code› and
  j_free = free_lbd and
  k_default = bottom_vdom and
  k = ‹bottom_vdom_code› and
  k_free = free_vdom and
  l_default = bottom_vdom and
  l = ‹bottom_vdom_code› and
  l_free = free_vdom and
  m_default = bottom_bool and
  m = ‹bottom_bool_code› and
  m_free = free_bool and
  n_default = bottom_lcount and
  n = ‹bottom_lcount_code› and
  n_free = free_lcount and
  ko_default = bottom_marked_struct and
  ko = ‹bottom_marked_struct_code› and
  o_free = free_marked_struct_code
  rewrites
    ‹IsaSAT_Init.tuple15_int_assn = isasat_init_assn›  and
    ‹IsaSAT_Init.remove_a = extract_trail_wl_heur_init› and
    ‹IsaSAT_Init.remove_b = extract_arena_wl_heur_init› and
    ‹IsaSAT_Init.remove_c = extract_conflict_wl_heur_init› and
    ‹IsaSAT_Init.remove_d = extract_literals_to_update_wl_heur_init› and
    ‹IsaSAT_Init.remove_e = extract_watchlist_wl_heur_init› and
    ‹IsaSAT_Init.remove_f = extract_vmtf_wl_heur_init› and
    ‹IsaSAT_Init.remove_g = extract_phase_saver_wl_heur_init› and
    ‹IsaSAT_Init.remove_h = extract_clvls_wl_heur_init› and
    ‹IsaSAT_Init.remove_i = extract_ccach_wl_heur_init› and
    ‹IsaSAT_Init.remove_j = extract_lbd_wl_heur_init› and
    ‹IsaSAT_Init.remove_k = extract_vdom_wl_heur_init› and
    ‹IsaSAT_Init.remove_l = extract_ivdom_wl_heur_init› and
    ‹IsaSAT_Init.remove_m = extract_failed_wl_heur_init› and
    ‹IsaSAT_Init.remove_n = extract_lcount_wl_heur_init› and
    ‹IsaSAT_Init.remove_o = extract_marked_wl_heur_init›
  apply unfold_locales
  subgoal by (rule bottom_trail_code.refine)
  subgoal by (rule bottom_arena_code.refine)
  subgoal by (rule bottom_conflict_code.refine)
  subgoal by (rule bottom_decision_level_code.refine)
  subgoal by (rule bottom_watchlist_code.refine)
  subgoal by (rule bottom_init_vmtf2_code.refine)
  subgoal by (rule bottom_phase_saver_code.refine)
  subgoal by (rule bottom_clvls_code.refine)
  subgoal by (rule bottom_ccach_code.refine)
  subgoal by (rule empty_lbd_hnr)
  subgoal by (rule bottom_vdom_code.refine)
  subgoal by (rule bottom_bool_code.refine)
  subgoal by (rule bottom_lcount_code.refine)
  subgoal by (rule bottom_marked_struct_code.refine)
  subgoal by (rule free_trail_pol_fast_assn2)
  subgoal by (rule free_arena_fast_assn2)
  subgoal by (rule free_conflict_option_rel_assn2)
  subgoal by (synthesize_free)
  subgoal by (synthesize_free)
  subgoal by (rule free_vmtf_remove2)
  subgoal by (rule free_phase_saver2)
  subgoal by (synthesize_free)
  subgoal by (synthesize_free)
  subgoal by (synthesize_free)
  subgoal by (rule free_vdom2)
  subgoal by (rule free_bool2)
  subgoal by (synthesize_free)
  subgoal by (rule free_marked_struct2)
  subgoal unfolding isasat_init_assn_def tuple15_state_ops.tuple15_int_assn_def ..
  subgoal unfolding extract_trail_wl_heur_init_def ..
  subgoal unfolding extract_arena_wl_heur_init_def ..
  subgoal unfolding extract_conflict_wl_heur_init_def ..
  subgoal unfolding extract_literals_to_update_wl_heur_init_def ..
  subgoal unfolding extract_watchlist_wl_heur_init_def ..
  subgoal unfolding extract_vmtf_wl_heur_init_def ..
  subgoal unfolding extract_phase_saver_wl_heur_init_def ..
  subgoal unfolding extract_clvls_wl_heur_init_def ..
  subgoal unfolding extract_ccach_wl_heur_init_def ..
  subgoal unfolding extract_lbd_wl_heur_init_def ..
  subgoal unfolding extract_vdom_wl_heur_init_def ..
  subgoal unfolding extract_ivdom_wl_heur_init_def ..
  subgoal unfolding extract_failed_wl_heur_init_def ..
  subgoal unfolding extract_lcount_wl_heur_init_def ..
  subgoal unfolding extract_marked_wl_heur_init_def ..
  done

lemmas [unfolded Tuple15_LLVM.inline_direct_return_node_case, llvm_code] =
  IsaSAT_Init.code_rules[unfolded Mreturn_comp_Tuple15]

lemmas [sepref_fr_rules] =
  IsaSAT_Init.separation_rules

lemmas isasat_init_getters_and_setters_def =
  IsaSAT_Init.setter_and_getters_def
  extract_trail_wl_heur_init_def
  extract_arena_wl_heur_init_def
  extract_conflict_wl_heur_init_def
  extract_literals_to_update_wl_heur_init_def
  extract_marked_wl_heur_init_def
  extract_lcount_wl_heur_init_def
  extract_failed_wl_heur_init_def
  extract_ivdom_wl_heur_init_def
  extract_vdom_wl_heur_init_def
  extract_lbd_wl_heur_init_def
  extract_ccach_wl_heur_init_def
  extract_clvls_wl_heur_init_def
  extract_phase_saver_wl_heur_init_def
  extract_vmtf_wl_heur_init_def
  extract_watchlist_wl_heur_init_def
  IsaSAT_Init.remove_a_def
  IsaSAT_Init.remove_b_def
  IsaSAT_Init.remove_c_def
  IsaSAT_Init.remove_d_def
  IsaSAT_Init.remove_e_def
  IsaSAT_Init.remove_f_def
  IsaSAT_Init.remove_g_def
  IsaSAT_Init.remove_h_def
  IsaSAT_Init.remove_i_def
  IsaSAT_Init.remove_j_def
  IsaSAT_Init.remove_k_def
  IsaSAT_Init.remove_l_def
  IsaSAT_Init.remove_m_def
  IsaSAT_Init.remove_n_def
  IsaSAT_Init.remove_o_def



lemma (in -) case_isasat_int_split_getter: ‹P 
  (Tuple15_a S)
  (Tuple15_b S)
  (Tuple15_c S)
  (Tuple15_d S)
  (Tuple15_e S)
  (Tuple15_f S)
  (Tuple15_g S)
  (Tuple15_h S)
  (Tuple15_i S)
  (Tuple15_j S)
  (Tuple15_k S)
  (Tuple15_l S)
  (Tuple15_m S)
  (Tuple15_n S)
  (Tuple15_o S) = case_tuple15 P S›
  by (auto split: tuple15.splits)


context tuple15_state
begin
context
  fixes
    f' :: ‹'s ⇒ 'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ 'g ⇒ 'h ⇒ 'i ⇒ 'j ⇒ 'k ⇒ 'l ⇒ 'm ⇒ 'n ⇒ 'o ⇒ 'x nres› and
    P  :: ‹'s ⇒ 'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e ⇒ 'f ⇒ 'g ⇒ 'h ⇒ 'i ⇒ 'j ⇒ 'k ⇒ 'l ⇒ 'm ⇒ 'n ⇒ 'o ⇒ bool›
begin
definition mop where
  ‹mop S C = do {
  ASSERT (P C
  (Tuple15_a S)
  (Tuple15_b S)
  (Tuple15_c S)
  (Tuple15_d S)
  (Tuple15_e S)
  (Tuple15_f S)
  (Tuple15_g S)
  (Tuple15_h S)
  (Tuple15_i S)
  (Tuple15_j S)
  (Tuple15_k S)
  (Tuple15_l S)
  (Tuple15_m S)
  (Tuple15_n S)
  (Tuple15_o S));
   read_all_st (f' C) S
  }›

context
  fixes R and kf and x_assn :: ‹'x ⇒ 'q ⇒ assn›
  assumes not_deleted_code_refine:
    ‹(uncurry15 (λa b c d e f g h i j k l m n ko C. kf C a b c d e f g h i j k l m n ko),
    uncurry15 (λa b c d e f g h i j k l m n ko C. f' C a b c d e f g h i j k l m n ko))
    ∈ [uncurry15 (λa b c d e f g h i j k l m n ko C. P C a b c d e f g h i j k l m n ko)]a
    a_assnk *a b_assnk *a c_assnk *a d_assnk *a
  e_assnk *a f_assnk *a g_assnk  *a h_assnk *a i_assnk *a
  j_assnk *a k_assnk *a l_assnk *a m_assnk *a
  n_assnk *a o_assnk *a (pure R)k → x_assn›
begin

context
begin
lemma not_deleted_code_refine_tmp:
  ‹⋀C C'. (C, C') ∈ R ⟹ (uncurry14 (kf C), uncurry14 (f' C')) ∈ [uncurry14 (P C')]a
    a_assnk *a b_assnk *a c_assnk *a d_assnk *a
  e_assnk *a f_assnk *a g_assnk  *a h_assnk *a i_assnk *a
  j_assnk *a k_assnk *a l_assnk *a m_assnk *a
  n_assnk *a o_assnk → x_assn›
  apply (rule remove_pure_parameter2'[where R=R])
  apply (rule hfref_cong[OF not_deleted_code_refine])
  apply (auto simp add: uncurry_def)
  done
end
lemma read_all_refine:
  ‹(uncurry (λN C. read_all_st_code (kf C) N),
    uncurry (λN C'. read_all_st (f' C') N))
  ∈ [uncurry (λS C. P C
  (Tuple15_a S)
  (Tuple15_b S)
  (Tuple15_c S)
  (Tuple15_d S)
  (Tuple15_e S)
  (Tuple15_f S)
  (Tuple15_g S)
  (Tuple15_h S)
  (Tuple15_i S)
  (Tuple15_j S)
  (Tuple15_k S)
  (Tuple15_l S)
  (Tuple15_m S)
  (Tuple15_n S)
  (Tuple15_o S))]a tuple15_int_assnk  *a (pure R)k→ x_assn›
  apply (rule add_pure_parameter2)
  unfolding tuple15.case_distrib case_isasat_int_split_getter
  apply (rule read_all_st_code_refine)
  apply (rule not_deleted_code_refine_tmp)
  apply assumption
  done

lemma read_all_mop_refine:
  ‹(uncurry (λN C. read_all_st_code (kf C) N),
    uncurry mop)
  ∈ tuple15_int_assnk  *a (pure R)k→a x_assn›
  unfolding mop_def
  apply (rule refine_ASSERT_move_to_pre)
  apply (rule read_all_refine)
  done
end
end

abbreviation read_trail_wl_heur_code :: ‹_› where
  ‹read_trail_wl_heur_code kf ≡ IsaSAT_Init.read_all_st_code  (λM _ _ _ _ _ _ _ _ _ _ _ _ _ _. kf M)›
abbreviation read_trail_wl_heur :: ‹_› where
  ‹read_trail_wl_heur kf ≡ IsaSAT_Init.read_all_st (λM _ _ _ _ _ _ _ _ _ _ _ _ _ _. kf M)›


context
  fixes R and kf and f' and x_assn :: ‹'r ⇒ 'q ⇒ assn› and P
  assumes not_deleted_code_refine: ‹(uncurry (λS C. kf C S), uncurry (λS C. f' C S)) ∈ [uncurry (λS C. P C S)]a a_assnk *a (pure R)k → x_assn›
begin
private lemma not_deleted_code_refine':
  ‹(uncurry15 (λM _ _ _ _ _ _ _ _ _ _ _ _ _ _ C. kf C M), uncurry15 (λM _ _ _ _ _ _ _ _ _ _ _ _ _ _ C'. f' C' M)) ∈ [uncurry15 (λM _ _ _ _ _ _ _ _ _ _ _ _ _ _ C. P C M)]a
   a_assnk *a b_assnk *a c_assnk *a d_assnk *a
  e_assnk *a f_assnk *a g_assnk  *a h_assnk *a i_assnk *a
  j_assnk *a k_assnk *a l_assnk *a m_assnk *a
  n_assnk *a o_assnk *a (pure R)k → x_assn›
  apply (insert not_deleted_code_refine)
  apply (drule remove_component_middle[where X = b_assn])
  apply (drule remove_component_middle[where X = c_assn])
  apply (drule remove_component_middle[where X = d_assn])
  apply (drule remove_component_middle[where X = e_assn])
  apply (drule remove_component_middle[where X = f_assn])
  apply (drule remove_component_middle[where X = g_assn])
  apply (drule remove_component_middle[where X = h_assn])
  apply (drule remove_component_middle[where X = i_assn])
  apply (drule remove_component_middle[where X = j_assn])
  apply (drule remove_component_middle[where X = k_assn])
  apply (drule remove_component_middle[where X = l_assn])
  apply (drule remove_component_middle[where X = m_assn])
  apply (drule remove_component_middle[where X = n_assn])
  apply (drule remove_component_middle[where X = o_assn])
  apply (rule hfref_cong, assumption)
  apply (auto simp add: uncurry_def)
  done

lemmas read_trail_refine = read_all_refine[OF not_deleted_code_refine']
lemmas mop_read_trail_refine = read_all_mop_refine[OF not_deleted_code_refine']
end


abbreviation read_conflict_wl_heur_code :: ‹_› where
  ‹read_conflict_wl_heur_code kf ≡ IsaSAT_Init.read_all_st_code  (λM _ _ _ _ _ _ _ _ _ _ _ _ _ _. kf M)›
abbreviation read_conflict_wl_heur :: ‹_› where
  ‹read_conflict_wl_heur kf ≡ IsaSAT_Init.read_all_st (λM _ _ _ _ _ _ _ _ _ _ _ _ _ _. kf M)›


context
  fixes R and kf and f' and x_assn :: ‹'r ⇒ 'q ⇒ assn› and P
  assumes not_deleted_code_refine: ‹(uncurry (λS C. kf C S), uncurry (λS C. f' C S)) ∈ [uncurry (λS C. P C S)]a c_assnk *a (pure R)k → x_assn›
begin
private lemma not_deleted_code_refine_conflict:
  ‹(uncurry15 (λ_ _ M _ _ _ _ _ _ _ _ _ _ _ _ C. kf C M), uncurry15 (λ_ _ M _ _ _ _ _ _ _ _ _ _ _ _ C'. f' C' M)) ∈ [uncurry15 (λ_ _ M _ _ _ _ _ _ _ _ _ _ _ _ C. P C M)]a
   a_assnk *a b_assnk *a c_assnk *a d_assnk *a
  e_assnk *a f_assnk *a g_assnk  *a h_assnk *a i_assnk *a
  j_assnk *a k_assnk *a l_assnk *a m_assnk *a
  n_assnk *a o_assnk *a (pure R)k → x_assn›
  apply (rule add_pure_parameter2)
  apply (drule remove_pure_parameter2'[where f =kf and f'=f', OF not_deleted_code_refine])
  apply (drule remove_component_left[where X = a_assn])
  apply (drule remove_component_middle[where X = b_assn])
  apply (drule remove_component_right[where X = d_assn])
  apply (drule remove_component_right[where X = e_assn])
  apply (drule remove_component_right[where X = f_assn])
  apply (drule remove_component_right[where X = g_assn])
  apply (drule remove_component_right[where X = h_assn])
  apply (drule remove_component_right[where X = i_assn])
  apply (drule remove_component_right[where X = j_assn])
  apply (drule remove_component_right[where X = k_assn])
  apply (drule remove_component_right[where X = l_assn])
  apply (drule remove_component_right[where X = m_assn])
  apply (drule remove_component_right[where X = n_assn])
  apply (drule remove_component_right[where X = o_assn])
  apply (rule hfref_cong, assumption)
  apply (auto simp add: uncurry_def)
  done

lemmas read_conflict_refine = read_all_refine[OF not_deleted_code_refine_conflict]
lemmas mop_read_conflict_refine = read_all_mop_refine[OF not_deleted_code_refine_conflict]
end

context
  fixes R and kf and f' and x_assn :: ‹'r ⇒ 'q ⇒ assn› and P
  assumes not_deleted_code_refine: ‹((λS. kf S), (λS. f' S)) ∈ [(λS. P S)]a c_assnk → x_assn›
begin

lemmas read_conflict_refine0 = read_conflict_refine[OF not_deleted_code_refine[THEN remove_component_right],
  THEN remove_unused_unit_parameter]
lemmas mop_read_conflict_refine0 = mop_read_conflict_refine[OF not_deleted_code_refine[THEN remove_component_right]]

end



abbreviation read_b_wl_heur_code :: ‹_› where
  ‹read_b_wl_heur_code kf ≡ IsaSAT_Init.read_all_st_code  (λ_ M _ _ _ _ _ _ _ _ _ _ _ _ _. kf M)›
abbreviation read_b_wl_heur :: ‹_› where
  ‹read_b_wl_heur kf ≡ IsaSAT_Init.read_all_st (λ_ M _ _ _ _ _ _ _ _ _ _ _ _ _. kf M)›



context
  fixes R and kf and f' and x_assn :: ‹'r ⇒ 'q ⇒ assn› and P
  assumes not_deleted_code_refine: ‹(uncurry (λS C. kf C S), uncurry (λS C. f' C S)) ∈ [uncurry (λS C. P C S)]a b_assnk *a (pure R)k → x_assn›
begin
private lemma not_deleted_code_refine_b:
  ‹(uncurry15 (λ_ M _ _ _ _ _ _ _ _ _ _ _ _ _ C. kf C M), uncurry15 (λ_ M _ _ _ _ _ _ _ _ _ _ _ _ _ C'. f' C' M)) ∈ [uncurry15 (λ_ M _ _ _ _ _ _ _ _ _ _ _ _ _ C. P C M)]a
   a_assnk *a b_assnk *a c_assnk *a d_assnk *a
  e_assnk *a f_assnk *a g_assnk  *a h_assnk *a i_assnk *a
  j_assnk *a k_assnk *a l_assnk *a m_assnk *a
  n_assnk *a o_assnk *a (pure R)k → x_assn›
  apply (rule add_pure_parameter2)
  apply (drule remove_pure_parameter2'[where f =kf and f'=f', OF not_deleted_code_refine])
  apply (drule remove_component_left[where X = a_assn])
  apply (drule remove_component_right[where X = c_assn])
  apply (drule remove_component_right[where X = d_assn])
  apply (drule remove_component_right[where X = e_assn])
  apply (drule remove_component_right[where X = f_assn])
  apply (drule remove_component_right[where X = g_assn])
  apply (drule remove_component_right[where X = h_assn])
  apply (drule remove_component_right[where X = i_assn])
  apply (drule remove_component_right[where X = j_assn])
  apply (drule remove_component_right[where X = k_assn])
  apply (drule remove_component_right[where X = l_assn])
  apply (drule remove_component_right[where X = m_assn])
  apply (drule remove_component_right[where X = n_assn])
  apply (drule remove_component_right[where X = o_assn])
  apply (rule hfref_cong, assumption)
  apply (auto simp add: uncurry_def)
  done

lemmas read_b_refine = read_all_refine[OF not_deleted_code_refine_b]
lemmas mop_read_b_refine = read_all_mop_refine[OF not_deleted_code_refine_b]
end


context
  fixes R and kf and f' and x_assn :: ‹'r ⇒ 'q ⇒ assn› and P
  assumes not_deleted_code_refine: ‹((λS. kf S), (λS. f' S)) ∈ [(λS. P S)]a b_assnk → x_assn›
begin

lemmas read_b_refine0 = read_b_refine[OF not_deleted_code_refine[THEN remove_component_right],
  THEN remove_unused_unit_parameter]
lemmas mop_read_b_refine0 = mop_read_b_refine[OF not_deleted_code_refine[THEN remove_component_right]]

end

  

context
  fixes R and kf and f' and x_assn :: ‹'r ⇒ 'q ⇒ assn› and P
  assumes not_deleted_code_refine: ‹(uncurry (λS C. kf C S), uncurry (λS C. f' C S)) ∈ [uncurry (λS C. P C S)]a n_assnk *a (pure R)k → x_assn›
begin
private lemma not_deleted_code_refine_n:
  ‹(uncurry15 (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _ C. kf C M), uncurry15 (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _ C'. f' C' M)) ∈ [uncurry15 (λ_ _ _ _ _ _ _ _ _ _ _ _ _ M _ C. P C M)]a
   a_assnk *a b_assnk *a c_assnk *a d_assnk *a
  e_assnk *a f_assnk *a g_assnk  *a h_assnk *a i_assnk *a
  j_assnk *a k_assnk *a l_assnk *a m_assnk *a
  n_assnk *a o_assnk *a (pure R)k → x_assn›
  apply (rule add_pure_parameter2)
  apply (drule remove_pure_parameter2'[where f =kf and f'=f', OF not_deleted_code_refine])
  apply (drule remove_component_left[where X = a_assn])
  apply (drule remove_component_middle[where X = b_assn])
  apply (drule remove_component_middle[where X = c_assn])
  apply (drule remove_component_middle[where X = d_assn])
  apply (drule remove_component_middle[where X = e_assn])
  apply (drule remove_component_middle[where X = f_assn])
  apply (drule remove_component_middle[where X = g_assn])
  apply (drule remove_component_middle[where X = h_assn])
  apply (drule remove_component_middle[where X = i_assn])
  apply (drule remove_component_middle[where X = j_assn])
  apply (drule remove_component_middle[where X = k_assn])
  apply (drule remove_component_middle[where X = l_assn])
  apply (drule remove_component_middle[where X = m_assn])
  apply (drule remove_component_right[where X = o_assn])
  apply (rule hfref_cong, assumption)
  apply (auto simp add: uncurry_def)
  done

lemmas read_n_refine = read_all_refine[OF not_deleted_code_refine_n]
lemmas mop_read_n_refine = read_all_mop_refine[OF not_deleted_code_refine_n]
end


context
  fixes R and kf and f' and x_assn :: ‹'r ⇒ 'q ⇒ assn› and P
  assumes not_deleted_code_refine: ‹((λS. kf S), (λS. f' S)) ∈ [(λS. P S)]a n_assnk → x_assn›
begin

lemmas read_n_refine0 = read_n_refine[OF not_deleted_code_refine[THEN remove_component_right],
  THEN remove_unused_unit_parameter]
lemmas mop_read_n_refine0 = mop_read_n_refine[OF not_deleted_code_refine[THEN remove_component_right]]

end


context
  fixes R and kf and f' and x_assn :: ‹'r ⇒ 'q ⇒ assn› and P
  assumes not_deleted_code_refine: ‹(uncurry (λS C. kf C S), uncurry (λS C. f' C S)) ∈ [uncurry (λS C. P C S)]a m_assnk *a (pure R)k → x_assn›
begin
private lemma not_deleted_code_refine_m:
  ‹(uncurry15 (λ_ _ _ _ _ _ _ _ _ _ _ _ M _ _ C. kf C M), uncurry15 (λ_ _ _ _ _ _ _ _ _ _ _ _ M _ _ C'. f' C' M)) ∈ [uncurry15 (λ_ _ _ _ _ _ _ _ _ _ _ _ M _ _ C. P C M)]a
   a_assnk *a b_assnk *a c_assnk *a d_assnk *a
  e_assnk *a f_assnk *a g_assnk  *a h_assnk *a i_assnk *a
  j_assnk *a k_assnk *a l_assnk *a m_assnk *a
  n_assnk *a o_assnk *a (pure R)k → x_assn›
  apply (rule add_pure_parameter2)
  apply (drule remove_pure_parameter2'[where f =kf and f'=f', OF not_deleted_code_refine])
  apply (drule remove_component_left[where X = a_assn])
  apply (drule remove_component_middle[where X = b_assn])
  apply (drule remove_component_middle[where X = c_assn])
  apply (drule remove_component_middle[where X = d_assn])
  apply (drule remove_component_middle[where X = e_assn])
  apply (drule remove_component_middle[where X = f_assn])
  apply (drule remove_component_middle[where X = g_assn])
  apply (drule remove_component_middle[where X = h_assn])
  apply (drule remove_component_middle[where X = i_assn])
  apply (drule remove_component_middle[where X = j_assn])
  apply (drule remove_component_middle[where X = k_assn])
  apply (drule remove_component_middle[where X = l_assn])
  apply (drule remove_component_right[where X = n_assn])
  apply (drule remove_component_right[where X = o_assn])
  apply (rule hfref_cong, assumption)
  apply (auto simp add: uncurry_def)
  done

lemmas read_m_refine = read_all_refine[OF not_deleted_code_refine_m]
lemmas mop_read_m_refine = read_all_mop_refine[OF not_deleted_code_refine_m]
end


context
  fixes R and kf and f' and x_assn :: ‹'r ⇒ 'q ⇒ assn› and P
  assumes not_deleted_code_refine: ‹((λS. kf S), (λS. f' S)) ∈ [(λS. P S)]a m_assnk → x_assn›
begin

lemmas read_m_refine0 = read_m_refine[OF not_deleted_code_refine[THEN remove_component_right],
  THEN remove_unused_unit_parameter]
lemmas mop_read_m_refine0 = mop_read_m_refine[OF not_deleted_code_refine[THEN remove_component_right]]

end
end
end