Theory IsaSAT_Bump_Heuristics

theory IsaSAT_Bump_Heuristics_LLVM imports IsaSAT_Bump_Heuristics IsaSAT_VMTF_LLVM Tuple4_LLVM IsaSAT_Bump_Heuristics_State_LLVM IsaSAT_ACIDS_LLVM begin sepref_register isa_acids_flush_int isa_acids_find_next_undef acids_push_literal isa_acids_incr_score sepref_def isa_acids_incr_score_code is ‹RETURN o isa_acids_incr_score› :: ‹acids_assn2^d →_a acids_assn2› unfolding isa_acids_incr_score_def acids_assn2_def apply (annot_unat_const ‹TYPE(64)›) by sepref lemma isa_acids_flush_int_alt_def: ‹isa_acids_flush_int = (λM vm (to_remove, h). do { ASSERT(length to_remove ≤ unat32_max); let n = length to_remove; (_, vm, h) ← WHILE_T⇗λ(i, vm', h). i ≤ n⇖ (λ(i, vm, h). i < n) (λ(i, vm, h). do { ASSERT(i < length to_remove); let L = to_remove!i; vm ← acids_push_literal L vm; ASSERT(atoms_hash_del_pre L h); RETURN (i+1, vm, atoms_hash_del L h)}) (0, vm, h); RETURN (vm, (emptied_list to_remove, h)) })› unfolding isa_acids_flush_int_def Let_def by auto sepref_def acids_flush_int is ‹uncurry2 isa_acids_flush_int› :: ‹trail_pol_fast_assn^k *_a acids_assn2^d *_a distinct_atoms_assn^d →_a acids_assn2 ×_a distinct_atoms_assn › unfolding isa_acids_flush_int_alt_def emptied_list_alt_def apply (rewrite at ‹WHILEIT _ (λ(_, _, _)._ < ⌑)› annot_snat_unat_conv) apply (rewrite at ‹_ ! ⌑› annot_unat_snat_conv) apply (rewrite at ‹take ⌑ _› snat_const_fold[where 'a=64]) apply (annot_unat_const ‹TYPE(64)›) by sepref definition acids0_mset_empty where ‹acids0_mset_empty = (λ(_, b, _). b= {#})› definition hp_acids_empty where ‹hp_acids_empty = (λ(_, _, _, _, _, h). h = None)› lemma hp_acids_empty: ‹(RETURN o hp_acids_empty, RETURN o acids0_mset_empty) ∈ (((⟨⟨nat_rel⟩option_rel, ⟨nat_rel⟩option_rel⟩pairing_heaps_rel)) O acids_encoded_hmrel) →_f ⟨bool_rel⟩nres_rel› proof - have [intro!]: ‹Me ∈# {#} ⟹ False›for Me by auto have 1: ‹(({#}, (λ_. None, λ_. None, λ_. None, λ_. None, λ_. None), None), empty_acids0) ∈ acids_encoded_hmrel› by (auto simp: acids_encoded_hmrel_def bottom_acids0_def pairing_heaps_rel_def map_fun_rel_def ACIDS.hmrel_def encoded_hp_prop_list_conc_def encoded_hp_prop_def empty_outside_def empty_acids0_def intro!: relcompI) have H: ‹mset_nodes ya ≠ {#}› for ya by (cases ya) auto show ?thesis unfolding uncurry0_def by (intro frefI nres_relI) (auto simp add: acids_encoded_hmrel_def acids0_mset_empty_def encoded_hp_prop_def ACIDS.hmrel_def encoded_hp_prop_list_conc_def hp_acids_empty_def pairing_heaps_rel_def H split: option.splits) qed definition acids_mset_empty :: ‹_› where ‹acids_mset_empty x = (acids_mset x = {#})› lemma acids_mset_empty_alt_def: ‹acids_mset_empty = (λ(a, b). acids0_mset_empty a)› by (auto intro!: ext simp: acids_mset_empty_def acids0_mset_empty_def acids_mset_def) sepref_def hp_acids_empty_code is ‹RETURN o hp_acids_empty› :: ‹hp_assn^k →_a bool1_assn› unfolding hp_assn_def hp_acids_empty_def atom.fold_option by sepref lemmas [fcomp_norm_unfold] = acids_assn_def[symmetric] lemmas [sepref_fr_rules] = hp_acids_empty_code.refine[FCOMP hp_acids_empty, unfolded hr_comp_assoc[symmetric] acids_assn_def[symmetric] acids_assn2_def[symmetric]] sepref_def acids_mset_empty_code is ‹RETURN o acids_mset_empty› :: ‹acids_assn2^k →_a bool1_assn› unfolding acids_mset_empty_alt_def acids_assn2_def by sepref sepref_def acids_find_next_undef_impl is ‹uncurry isa_acids_find_next_undef› :: ‹acids_assn2^d *_a trail_pol_fast_assn^k →_a atom.option_assn ×_a acids_assn2› unfolding isa_acids_find_next_undef_def atom.fold_option acids_mset_empty_def[symmetric] by sepref (*TODO remove isa_vmtf_unset = vmtf_unset *) lemma isa_bump_unset_alt_def: ‹isa_bump_unset L vm = (case vm of Tuple4 (hstable) (focused) foc a ⇒ do { hstable ← (if ¬foc then acids_tl L hstable else RETURN hstable); let focused = (if foc then isa_vmtf_unset L focused else focused); RETURN (Tuple4 hstable focused foc a) })› unfolding isa_bump_unset_def isa_vmtf_unset_def vmtf_unset_def[symmetric] by (auto intro!: ext split: bump_heuristics_splits) sepref_register vmtf_unset case_tuple4 sepref_def isa_bump_unset_impl is ‹uncurry (isa_bump_unset)› :: ‹[uncurry isa_bump_unset_pre]_a atom_assn^k *_a heuristic_bump_assn^d → heuristic_bump_assn› unfolding isa_bump_unset_alt_def isa_bump_unset_pre_def by sepref sepref_def isa_find_decomp_wl_imp_impl is ‹uncurry2 isa_find_decomp_wl_imp› :: ‹trail_pol_fast_assn^d *_a uint32_nat_assn^k *_a heuristic_bump_assn^d →_a trail_pol_fast_assn ×_a heuristic_bump_assn› unfolding isa_find_decomp_wl_imp_def get_maximum_level_remove_def[symmetric] PR_CONST_def trail_pol_conv_to_no_CS_def supply trail_conv_to_no_CS_def[simp] lit_of_hd_trail_def[simp] supply [[goals_limit=1]] literals_are_in_ℒ_i_n_add_mset[simp] supply vmtf_unset_pre_def[simp] apply (rewrite at ‹let _ = _ - ⌑ in _› annot_unat_snat_upcast[where 'l=64]) apply (annot_snat_const ‹TYPE(64)›) by sepref sepref_register isa_bump_mark_to_rescore isa_find_decomp_wl_imp sepref_def isa_bump_mark_to_rescore_code is ‹uncurry (isa_bump_mark_to_rescore)› :: ‹atom_assn^k *_a heuristic_bump_assn^d →_a heuristic_bump_assn› supply [[goals_limit=1]] option.splits[split] vmtf_def[simp] in_ℒ_a_l_l_atm_of_in_atms_of_iff[simp] neq_NilE[elim!] literals_are_in_ℒ_i_n_add_mset[simp] unfolding isa_vmtf_mark_to_rescore_pre_def isa_vmtf_mark_to_rescore_def isa_bump_mark_to_rescore_def by sepref sepref_def isa_bump_mark_to_rescore_clause_fast_code is ‹uncurry2 (isa_bump_mark_to_rescore_clause)› :: ‹[λ((N, _), _). length N ≤ snat64_max]_a arena_fast_assn^k *_a sint64_nat_assn^k *_a heuristic_bump_assn^d → heuristic_bump_assn› supply [[goals_limit=1]] arena_is_valid_clause_idx_le_unat64_max[intro] unfolding isa_bump_mark_to_rescore_clause_def PR_CONST_def unfolding while_eq_nfoldli[symmetric] apply (subst while_upt_while_direct, simp) unfolding nres_monad3 apply (annot_snat_const ‹TYPE(64)›) by sepref sepref_def isa_bump_rescore_fast_code is ‹uncurry2 isa_bump_rescore› :: ‹clause_ll_assn^k *_a trail_pol_fast_assn^k *_a heuristic_bump_assn^d →_a heuristic_bump_assn› unfolding isa_bump_rescore_def[abs_def] PR_CONST_def isa_bump_rescore_body_def supply [[goals_limit = 1]] fold_is_None[simp] apply (annot_snat_const ‹TYPE(64)›) by sepref sepref_def vmtf_mark_to_rescore_also_reasons_fast_code is ‹uncurry4 (isa_vmtf_mark_to_rescore_also_reasons)› :: ‹[λ((((_, N), _), _), _). length N ≤ snat64_max]_a trail_pol_fast_assn^k *_a arena_fast_assn^k *_a out_learned_assn^k *_a unat_lit_assn^k *_a heuristic_bump_assn^d → heuristic_bump_assn› supply image_image[simp] uminus_𝒜_i_n_iff[iff] in_diffD[dest] option.splits[split] in_ℒ_a_l_l_atm_of_𝒜_i_n[simp] supply [[goals_limit=1]] unfolding isa_vmtf_mark_to_rescore_also_reasons_def PR_CONST_def unfolding while_eq_nfoldli[symmetric] apply (subst while_upt_while_direct, simp) apply (annot_snat_const ‹TYPE(64)›) unfolding nres_monad3 case_option_split by sepref sepref_register isa_vmtf_bump_to_rescore_also_reasons_cl isa_vmtf_mark_to_rescore_also_reasons isa_bump_heur_flush sepref_def isa_vmtf_bump_to_rescore_also_reasons_cl_impl is ‹uncurry4 (isa_vmtf_bump_to_rescore_also_reasons_cl)› :: ‹[λ((((_, N), _), _), _). length N ≤ snat64_max]_a trail_pol_fast_assn^k *_a arena_fast_assn^k *_a sint64_nat_assn^k *_a unat_lit_assn^k *_a heuristic_bump_assn^d → heuristic_bump_assn› supply image_image[simp] uminus_𝒜_i_n_iff[iff] in_diffD[dest] option.splits[split] in_ℒ_a_l_l_atm_of_𝒜_i_n[simp] supply [[goals_limit=1]] supply [dest] = isa_vmtf_bump_to_rescore_also_reasons_clD unfolding isa_vmtf_bump_to_rescore_also_reasons_cl_def PR_CONST_def unfolding while_eq_nfoldli[symmetric] apply (subst while_upt_while_direct, simp) apply (annot_snat_const ‹TYPE(64)›) unfolding nres_monad3 case_option_split by sepref sepref_def isa_bump_heur_flush_impl is ‹uncurry isa_bump_heur_flush› :: ‹trail_pol_fast_assn^k *_a heuristic_bump_assn^d →_a heuristic_bump_assn› unfolding isa_bump_heur_flush_def by sepref sepref_def isa_vmtf_heur_fst_code is ‹isa_vmtf_heur_fst› :: ‹heuristic_bump_assn^k →_a atom_assn› unfolding isa_vmtf_heur_fst_def by sepref definition isa_vmtf_heur_array_nth where ‹isa_vmtf_heur_array_nth x = vmtf_heur_array_nth (bump_get_heuristics x)› lemma isa_vmtf_heur_array_nth_alt_def: ‹isa_vmtf_heur_array_nth x i = (case x of Bump_Heuristics hstable focused foc _ ⇒ (vmtf_heur_array_nth focused i))› by (cases x) (auto simp: bump_get_heuristics_def isa_vmtf_heur_array_nth_def) sepref_register is_focused_heuristics vmtf_heur_array_nth sepref_def isa_vmtf_heur_array_nth_code is ‹uncurry isa_vmtf_heur_array_nth› :: ‹[λ(vm, i). i < length (fst (bump_get_heuristics vm))]_a heuristic_bump_assn^k *_a atom_assn^k → vmtf_node_assn› supply if_splits[split] unfolding isa_vmtf_heur_array_nth_alt_def bump_get_heuristics_def by sepref definition vmtf_array_fst :: ‹vmtf ⇒ nat› where ‹vmtf_array_fst = (λ(a, b, c, d, e). c)› lemma bumped_vmtf_array_fst_alt_def: ‹bumped_vmtf_array_fst x = (case x of Bump_Heuristics a b c d ⇒ (vmtf_array_fst b))› by (cases x) (auto simp: vmtf_array_fst_def current_vmtf_array_nxt_score_def bump_get_heuristics_def bumped_vmtf_array_fst_def) sepref_def vmtf_array_fst_code is ‹RETURN o vmtf_array_fst› :: ‹vmtf_assn^k →_a atom_assn› unfolding vmtf_assn_def vmtf_array_fst_def by sepref sepref_def bumped_vmtf_array_fst_code is ‹RETURN o bumped_vmtf_array_fst› :: ‹heuristic_bump_assn^k →_a atom_assn› unfolding bumped_vmtf_array_fst_alt_def by sepref sepref_register access_focused_vmtf_array definition access_vmtf_array :: ‹vmtf ⇒ nat ⇒ _ nres› where ‹access_vmtf_array = (λ(a, b, c, d, f) i. do { ASSERT (i < length a); RETURN (a ! i)})› lemma access_focused_vmtf_array_alt_def: ‹access_focused_vmtf_array x i = (case x of Bump_Heuristics a b c d ⇒ do { access_vmtf_array b i })› by (cases x) (auto simp: access_focused_vmtf_array_def access_vmtf_array_def bump_get_heuristics_def) sepref_def access_vmtf_array_code is ‹uncurry access_vmtf_array› :: ‹vmtf_assn^k *_a atom_assn^k →_a vmtf_node_assn› unfolding access_vmtf_array_def vmtf_assn_def apply (rewrite at ‹RETURN ⌑› annot_index_of_atm) by sepref sepref_register access_vmtf_array sepref_def access_focused_vmtf_array_code is ‹uncurry access_focused_vmtf_array› :: ‹heuristic_bump_assn^k *_a atom_assn^k →_a vmtf_node_assn› unfolding access_focused_vmtf_array_alt_def by sepref experiment begin export_llvm isa_vmtf_bump_to_rescore_also_reasons_cl_impl vmtf_mark_to_rescore_also_reasons_fast_code isa_bump_rescore_fast_code isa_bump_mark_to_rescore_clause_fast_code isa_bump_heur_flush_impl isa_vmtf_heur_array_nth_code end end

Theory IsaSAT_Bump_Heuristics_LLVM