Theory IsaSAT_Bump_Heuristics_State

theory IsaSAT_Bump_Heuristics_State_LLVM imports IsaSAT_Bump_Heuristics_State IsaSAT_VMTF_Setup_LLVM Tuple4_LLVM IsaSAT_ACIDS_LLVM begin hide_const (open) NEMonad.ASSERT NEMonad.RETURN type_synonym bump_heuristics_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› definition heuristic_bump_assn :: ‹bump_heuristics ⇒ bump_heuristics_assn ⇒ _› where ‹heuristic_bump_assn = tuple4_assn acids_assn2 vmtf_assn bool1_assn distinct_atoms_assn› definition bottom_atom where ‹bottom_atom = 0› definition bottom_vmtf :: ‹vmtf› where ‹bottom_vmtf = ((replicate 0 (VMTF_Node 0 None None), 0, bottom_atom, bottom_atom, 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_vmtf› lemma [sepref_fr_rules]: ‹(uncurry0 (Mreturn 0), uncurry0 (RETURN bottom_atom)) ∈ unit_assn^k →_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_vmtf_code is ‹uncurry0 (RETURN bottom_vmtf)› :: ‹unit_assn^k →_a vmtf_assn› unfolding bottom_vmtf_def apply (rewrite in ‹((⌑, _, _, _, _))› array_fold_custom_replicate) unfolding atom.fold_option array_fold_custom_replicate vmtf_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_assn ?a› unfolding vmtf_assn_def by synthesize_free sepref_def free_vmtf_remove is ‹mop_free› :: ‹vmtf_assn^d →_a unit_assn› by sepref sepref_def bottom_focused is ‹uncurry0 (RETURN False)› :: ‹unit_assn^k →_a bool1_assn› by sepref sepref_def free_focused is ‹mop_free› :: ‹bool1_assn^d →_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_assn^k →_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 sepref_def free_atms_hash_code is ‹mop_free› :: ‹distinct_atoms_assn^d →_a unit_assn› by sepref lemma free_vmtf_assn_assn2: ‹MK_FREE vmtf_assn free_vmtf_remove› unfolding free_vmtf_remove_def by (rule back_subst[of ‹MK_FREE vmtf_assn›, OF free_vmtf_remove_assn]) (auto intro!: ext) schematic_goal free_focused_assn: ‹MK_FREE bool1_assn ?a› unfolding vmtf_assn_def by synthesize_free schematic_goal free_distinct_atoms_assn: ‹MK_FREE distinct_atoms_assn ?a› by synthesize_free lemma free_focused_assn2: ‹MK_FREE bool1_assn free_focused› unfolding free_focused_def by (rule back_subst[of ‹MK_FREE bool1_assn›, OF free_focused_assn]) (auto intro!: ext) lemma free_distinct_atoms_assn2: ‹MK_FREE (distinct_atoms_assn) free_atms_hash_code› unfolding free_atms_hash_code_def by (rule back_subst[of ‹MK_FREE distinct_atoms_assn›, OF free_distinct_atoms_assn]) (auto intro!: ext) global_interpretation Bump_Heur: tuple4_state where a_assn = acids_assn2 and b_assn = vmtf_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_vmtf and b = ‹bottom_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.tuple4_int_assn ≡ heuristic_bump_assn›and ‹Bump_Heur.remove_a ≡ extract_bump_stable› and ‹Bump_Heur.remove_b ≡ extract_bump_focused› and ‹Bump_Heur.remove_c ≡ extract_bump_is_focused› and ‹Bump_Heur.remove_d ≡ extract_bump_atms_to_bump› apply unfold_locales apply (rule bottom_vmtf_code.refine bottom_focused.refine empty_acids_code.refine bottom_atms_hash_code.refine free_vmtf_assn_assn2 free_focused_assn2 free_acids_assn2' free_distinct_atoms_assn2)+ subgoal unfolding heuristic_bump_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.code_rules[unfolded Mreturn_comp_Tuple4] lemmas [sepref_fr_rules] = Bump_Heur.separation_rules (*The if/then/else is a work-around for sepref...*) lemma switch_bump_heur_alt_def: ‹RETURN o switch_bump_heur = (λx. case x of Bump_Heuristics hstable focused foc b ⇒ do { f ← RETURN (¬foc); mop_free foc; RETURN (Bump_Heuristics hstable focused (f) b)})› by (auto intro!: ext simp: mop_free_def switch_bump_heur_def split: bump_heuristics_splits) sepref_def switch_bump_heur_code is ‹RETURN o switch_bump_heur› :: ‹heuristic_bump_assn^d →_a heuristic_bump_assn› unfolding switch_bump_heur_alt_def by sepref end

Theory IsaSAT_Bump_Heuristics_State_LLVM