Theory IsaSAT_Setup1

theory IsaSAT_Setup1_LLVM imports IsaSAT_Setup IsaSAT_Setup0_LLVM begin sepref_register arena_status DELETED sepref_definition not_deleted_code is ‹(uncurry (λN C'. do {status ← RETURN (arena_status N C'); RETURN (status ≠ DELETED)}))› :: ‹[uncurry (λN C'. arena_is_valid_clause_vdom N C')]_a arena_fast_assn^k *_a sint64_nat_assn^k → bool1_assn› by sepref lemma clause_not_marked_to_delete_heur_alt_def: ‹RETURN oo clause_not_marked_to_delete_heur = (λ S C'. read_arena_wl_heur (λN. do {status ← RETURN (arena_status N C'); RETURN (status ≠ DELETED)}) S)› by (auto intro!: ext simp: clause_not_marked_to_delete_heur_def read_all_st_def split: isasat_int_splits) definition clause_not_marked_to_delete_heur_code :: ‹twl_st_wll_trail_fast2 ⇒ _ ⇒ _› where ‹clause_not_marked_to_delete_heur_code S C' = read_arena_wl_heur_code (λN. not_deleted_code N C') S› global_interpretation arena_is_valid: read_arena_param_adder where R = ‹snat_rel' TYPE(64)› and f = ‹λC N. not_deleted_code N C› and f' = ‹(λC' N. do {status ← RETURN (arena_status N C'); RETURN (status ≠ DELETED)})› and x_assn = bool1_assn and P = ‹(λC S. arena_is_valid_clause_vdom S C)› rewrites ‹(λS C'. read_arena_wl_heur (λN. do {status ← RETURN (arena_status N C'); RETURN (status ≠ DELETED)}) S) = RETURN oo clause_not_marked_to_delete_heur› and ‹(λS C'. read_arena_wl_heur_code (λN. not_deleted_code N C') S) = clause_not_marked_to_delete_heur_code› and ‹(λS. arena_is_valid_clause_vdom (get_clauses_wl_heur S)) = curry clause_not_marked_to_delete_heur_pre› apply unfold_locales apply (rule not_deleted_code.refine) unfolding clause_not_marked_to_delete_heur_alt_def clause_not_marked_to_delete_heur_code_def apply (solves ‹rule refl›)+ subgoal by (auto simp: clause_not_marked_to_delete_heur_pre_def) done sepref_register clause_not_marked_to_delete_heur lemmas [sepref_fr_rules] = arena_is_valid.refine[unfolded uncurry_curry_id] lemmas [llvm_code] = clause_not_marked_to_delete_heur_code_def[unfolded read_all_st_code_def not_deleted_code_def] sepref_def mop_clause_not_marked_to_delete_heur_impl is ‹uncurry mop_clause_not_marked_to_delete_heur› :: ‹isasat_bounded_assn^k *_a sint64_nat_assn^k →_a bool1_assn› unfolding mop_clause_not_marked_to_delete_heur_def prod.case clause_not_marked_to_delete_heur_pre_def[symmetric] by sepref definition conflict_is_None :: ‹conflict_option_rel ⇒ bool nres› where ‹conflict_is_None =(λN. do {let (b, _) = N; RETURN b})› definition ‹conflict_is_None_code :: option_lookup_clause_assn ⇒ 1 word llM ≡ λ(a, _). do_M { return_M (a) }› lemma conflict_is_None_code_refine[sepref_fr_rules]: ‹(conflict_is_None_code, conflict_is_None) ∈ conflict_option_rel_assn^k →_a bool1_assn› unfolding conflict_is_None_code_def conflict_is_None_def Let_def conflict_option_rel_assn_def apply sepref_to_hoare apply vcg done lemma get_conflict_wl_is_None_heur_alt_def: ‹read_conflict_wl_heur conflict_is_None = RETURN ∘ get_conflict_wl_is_None_heur› by (auto simp: read_all_st_def get_conflict_wl_is_None_heur_def conflict_is_None_def intro!: ext split: isasat_int_splits) definition get_conflict_wl_is_None_heur2 where ‹get_conflict_wl_is_None_heur2 = RETURN o get_conflict_wl_is_None_heur› definition get_conflict_wl_is_None_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹get_conflict_wl_is_None_fast_code = read_conflict_wl_heur_code conflict_is_None_code› global_interpretation conflict_is_None: read_conflict_param_adder0 where f = ‹conflict_is_None_code› and f' = ‹conflict_is_None› and x_assn = bool1_assn and P = ‹(λS. True)› rewrites ‹(λS. read_conflict_wl_heur (conflict_is_None) S) = get_conflict_wl_is_None_heur2› and ‹(λS. read_conflict_wl_heur_code (conflict_is_None_code) S) = get_conflict_wl_is_None_fast_code› apply unfold_locales apply (rule conflict_is_None_code_refine; assumption) unfolding get_conflict_wl_is_None_heur2_def get_conflict_wl_is_None_fast_code_def by (solves ‹rule get_conflict_wl_is_None_heur_alt_def refl›)+ lemmas [sepref_fr_rules] = conflict_is_None.refine[unfolded get_conflict_wl_is_None_heur2_def] lemmas [llvm_code] = conflict_is_None_code_def lemmas [unfolded inline_direct_return_node_case, llvm_code] = get_conflict_wl_is_None_fast_code_def[unfolded read_all_st_code_def] lemma count_decided_st_heur_alt_def: ‹RETURN o count_decided_st_heur = read_trail_wl_heur (RETURN ∘ count_decided_pol)› by (auto intro!: ext simp: count_decided_st_heur_def count_decided_pol_def read_all_st_def split: isasat_int_splits) definition count_decided_st_heur_impl where ‹count_decided_st_heur_impl = read_trail_wl_heur_code count_decided_pol_impl› sepref_register extract_trail_wl_heur count_decided_pol count_decided_st_heur definition count_decided_st_heur_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹count_decided_st_heur_fast_code = read_trail_wl_heur_code count_decided_pol_impl› global_interpretation count_decided: read_trail_param_adder0 where f = ‹count_decided_pol_impl› and f' = ‹RETURN o count_decided_pol› and x_assn = uint32_nat_assn and P = ‹(λS. True)› rewrites ‹read_trail_wl_heur (RETURN o count_decided_pol) = RETURN o count_decided_st_heur› and ‹read_trail_wl_heur_code count_decided_pol_impl = count_decided_st_heur_fast_code› apply unfold_locales apply (rule count_decided_pol_impl.refine) subgoal by (auto simp: read_all_st_def count_decided_st_heur_def intro!: ext split: isasat_int_splits) subgoal by (auto simp: count_decided_st_heur_fast_code_def) done lemmas [sepref_fr_rules] = count_decided.refine[unfolded lambda_comp_true] lemmas [unfolded inline_direct_return_node_case, llvm_code] = count_decided_st_heur_fast_code_def[unfolded read_all_st_code_def] definition polarity_st_heur_pol_fast :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹polarity_st_heur_pol_fast = (λS C. read_trail_wl_heur_code (λL. polarity_pol_fast L C) S)› global_interpretation mop_count_decided: read_trail_param_adder where f = ‹λS L. polarity_pol_fast L S› and f' = ‹λS L. mop_polarity_pol L S› and x_assn = tri_bool_assn and P = ‹λS _. True› and R = ‹unat_lit_rel› rewrites ‹(λS C. read_trail_wl_heur_code (λL. polarity_pol_fast L C) S) = polarity_st_heur_pol_fast› and ‹(λS C'. read_trail_wl_heur (λL. mop_polarity_pol L C') S) = mop_polarity_st_heur› apply unfold_locales apply (subst lambda_comp_true) apply (rule polarity_pol_fast.refine) subgoal by (auto simp: polarity_st_heur_pol_fast_def) subgoal by (auto simp: mop_polarity_st_heur_def read_all_st_def split: isasat_int_splits intro!: ext) done lemmas [sepref_fr_rules] = mop_count_decided.refine[unfolded lambda_comp_true] lemmas [unfolded inline_direct_return_node_case, llvm_code] = polarity_st_heur_pol_fast_def[unfolded read_all_st_code_def] definition arena_lit2 where ‹arena_lit2 N i j = arena_lit N (i+j)› sepref_def arena_lit2_impl is ‹uncurry2 (RETURN ooo arena_lit2)› :: ‹[uncurry2 (λN i j. arena_lit_pre N (i+j) ∧ length N ≤ snat64_max)]_a arena_fast_assn^k *_a sint64_nat_assn^k *_a sint64_nat_assn^k → unat_lit_assn› supply [dest] = arena_lit_implI unfolding arena_lit_def arena_lit2_def by sepref lemma arena_lit2_impl_arena_lit: assumes ‹(C, C') ∈ snat_rel› and ‹(D, D') ∈ snat_rel› shows ‹(λS. arena_lit2_impl S C D, λS. RETURN (arena_lit S (C' + D'))) ∈ [λS. arena_lit_pre S (C' + D') ∧ length S ≤ snat64_max]_a (al_assn arena_el_impl_assn)^k → unat_lit_assn› proof - have arena_lit2: ‹RETURN ooo arena_lit2 = (λS C' D'. RETURN (arena_lit2 S C' D'))› for f by (auto intro!: ext) show ?thesis apply (rule remove_pure_parameter2_twoargs[where R = ‹snat_rel' TYPE(64)› and f = ‹λa C D. arena_lit2_impl a C D› and f' = ‹λS C' D'. RETURN (arena_lit S (C' + D'))›, OF _ assms]) unfolding arena_lit2_def[symmetric] arena_lit2[symmetric] by (rule arena_lit2_impl.refine) qed lemma access_lit_in_clauses_heur_alt_def: ‹RETURN ooo access_lit_in_clauses_heur = (λN C' D. read_arena_wl_heur (λN. RETURN (arena_lit N (C' + D))) N)› by (auto intro!: ext simp: read_all_st_def access_lit_in_clauses_heur_def split: isasat_int_splits) lemma access_lit_in_clauses_heur_pre: ‹uncurry2 (λS C D. arena_lit_pre (get_clauses_wl_heur S) (C + D) ∧ length (get_clauses_wl_heur S) ≤ snat64_max) = uncurry2 (λS i j. access_lit_in_clauses_heur_pre ((S, i), j) ∧ length (get_clauses_wl_heur S) ≤ snat64_max)› by (auto simp: access_lit_in_clauses_heur_pre_def) definition access_lit_in_clauses_heur_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _ ⇒ _ ⇒ _› where ‹access_lit_in_clauses_heur_fast_code = (λN C D. read_arena_wl_heur_code (λN. arena_lit2_impl N C D) N)› definition mop_arena_lit2_st where ‹mop_arena_lit2_st S = mop_arena_lit2 (get_clauses_wl_heur S)› global_interpretation access_arena: read_arena_param_adder2_twoargs where R = ‹(snat_rel' TYPE(64))› and R' = ‹snat_rel' TYPE(64)› and f' = ‹λi j N. RETURN (arena_lit N (i+j))› and f = ‹λi j N. arena_lit2_impl N i j› and x_assn = unat_lit_assn and P = ‹(λi j S. arena_lit_pre (S) (i+j) ∧ length S ≤ snat64_max)› rewrites ‹(λN C' D. read_arena_wl_heur (λN. RETURN (arena_lit N (C' + D))) N) = RETURN ooo access_lit_in_clauses_heur› and ‹(λN C D. read_arena_wl_heur_code (λN. arena_lit2_impl N C D) N) = access_lit_in_clauses_heur_fast_code› and ‹uncurry2 (λS C D. arena_lit_pre (get_clauses_wl_heur S) (C + D) ∧ length (get_clauses_wl_heur S) ≤ snat64_max) = uncurry2 (λS i j. access_lit_in_clauses_heur_pre ((S, i), j) ∧ length (get_clauses_wl_heur S) ≤ snat64_max)› apply unfold_locales apply (rule arena_lit2_impl.refine[unfolded comp_def arena_lit2_def]) apply (subst access_lit_in_clauses_heur_alt_def; rule refl) apply (subst access_lit_in_clauses_heur_fast_code_def; rule refl) apply (rule access_lit_in_clauses_heur_pre) done lemma refine_ASSERT_move_to_pre2': ‹(uncurry2 g, uncurry2 h) ∈ [uncurry2 (λa b c. P a b c ∧ Q a b c)]_a A *_a B *_a C → x_assn ⟷ (uncurry2 g, uncurry2 (λN C D. do {ASSERT (P N C D); h N C D})) ∈ [uncurry2 Q]_a A *_a B *_a C → x_assn› apply (rule iffI) subgoal premises p apply sepref_to_hoare apply vcg apply (subst POSTCOND_def hn_ctxt_def sep_conj_empty' pure_true_conv EXTRACT_def)+ apply (auto simp: nofail_ASSERT_bind hn_ctxt_def ) apply (rule p[to_hnr, simplified, unfolded hn_ctxt_def hn_refine_def htriple_def sep_conj_empty' pure_true_conv sep.add_assoc, rule_format]) apply auto done subgoal premises p apply sepref_to_hoare apply vcg subgoal for b bi ba bia a ai asf s apply (subst POSTCOND_def hn_ctxt_def sep_conj_empty' pure_true_conv EXTRACT_def)+ using p[to_hnr, simplified, unfolded hn_ctxt_def hn_refine_def htriple_def sep_conj_empty' pure_true_conv sep.add_assoc, rule_format, of a ba b] apply auto done done done lemma arena_lit_arena_lit_read_arena_wl_heur_arena_lit: ‹RETURN (arena_lit (get_clauses_wl_heur N) (C + C')) = read_arena_wl_heur (λN. RETURN (arena_lit N (C + C'))) N› by (auto intro!: ext simp: read_all_st_def access_lit_in_clauses_heur_def split: isasat_int_splits) sepref_register mop_access_lit_in_clauses_heur lemma mop_access_lit_in_clauses_heur_refine[sepref_fr_rules]: ‹(uncurry2 access_lit_in_clauses_heur_fast_code, uncurry2 mop_access_lit_in_clauses_heur) ∈ [uncurry2 (λS i j. length (get_clauses_wl_heur S) ≤ snat64_max)]_a isasat_bounded_assn^k *_a snat_assn^k *_a snat_assn^k → unat_lit_assn› using access_arena.mop_refine[unfolded access_arena.mop_def refine_ASSERT_move_to_pre2'[symmetric, where Q = ‹λ_ _ _. True›, unfolded simp_thms lambda_comp_true]] unfolding mop_access_lit_in_clauses_heur_def mop_access_lit_in_clauses_heur_def mop_arena_lit2_def Let_def access_arena.mop_def refine_ASSERT_move_to_pre2'[symmetric] access_lit_in_clauses_heur_alt_def arena_lit_arena_lit_read_arena_wl_heur_arena_lit[symmetric] by auto lemma al_assn_boundD2: ‹al_assn arena_el_impl_assn x2 (d:: 'a :: len2 word × 'a word × 32 word ptr) c ⟹ length x2 < max_snat LENGTH('a)› using al_assn_boundD[unfolded rdomp_def, of arena_el_impl_assn ‹x2›, where 'l = 'a] by (cases d) auto lemma isasat_bounded_assn_length_arenaD: ‹rdomp isasat_bounded_assn a ⟹ length (get_clauses_wl_heur a) ≤ snat64_max› apply - unfolding rdomp_def apply normalize_goal+ by (cases a, case_tac xa) (auto simp: isasat_bounded_assn_def rdomp_def snat64_max_def max_snat_def split: isasat_int_splits dest!: al_assn_boundD2 mod_starD) sepref_def mop_access_lit_in_clauses_heur_impl is ‹uncurry2 mop_access_lit_in_clauses_heur› :: ‹isasat_bounded_assn^k *_a sint64_nat_assn^k *_a sint64_nat_assn^k →_a unat_lit_assn› supply [dest] = isasat_bounded_assn_length_arenaD by sepref lemmas [sepref_fr_rules] = access_arena.refine lemmas [unfolded inline_direct_return_node_case, llvm_code] = access_lit_in_clauses_heur_fast_code_def[unfolded read_all_st_code_def] sepref_register mop_arena_lit2 mop_arena_length mop_append_ll sepref_def rewatch_heur_vdom_fast_code is ‹uncurry2 (rewatch_heur_vdom)› :: ‹[λ((vdom, arena), W). (∀x ∈ set (get_tvdom_aivdom vdom). x ≤ snat64_max) ∧ length arena ≤ snat64_max ∧ length (get_tvdom_aivdom vdom) ≤ snat64_max]_a aivdom_assn^k *_a arena_fast_assn^k *_a watchlist_fast_assn^d → watchlist_fast_assn› supply [[goals_limit=1]] arena_lit_pre_le_snat64_max[dest] arena_is_valid_clause_idx_le_unat64_max[dest] supply [simp] = append_ll_def length_tvdom_aivdom_def supply [dest] = arena_lit_implI(1) unfolding rewatch_heur_alt_def Let_def PR_CONST_def rewatch_heur_vdom_def tvdom_aivdom_at_def[symmetric] length_tvdom_aivdom_def[symmetric] unfolding while_eq_nfoldli[symmetric] apply (subst while_upt_while_direct, simp) unfolding if_not_swap FOREACH_cond_def FOREACH_body_def apply (annot_snat_const ‹TYPE(64)›) by sepref lemma rewatch_heur_st_fast_alt_def: ‹rewatch_heur_st_fast = (λS₀. do { let (N, S) = extract_arena_wl_heur S₀; let (W, S) = extract_watchlist_wl_heur S; let (vdom, S) = extract_vdom_wl_heur S; ASSERT(length (get_tvdom_aivdom vdom) ≤ length N); ASSERT (vdom = get_aivdom S₀); ASSERT (N = get_clauses_wl_heur S₀); ASSERT (W = get_watched_wl_heur S₀); W ← rewatch_heur (get_tvdom_aivdom vdom) N W; let S = update_arena_wl_heur N S; let S = update_watchlist_wl_heur W S; let S = update_vdom_wl_heur vdom S; RETURN S })› by (auto simp: rewatch_heur_st_fast_def rewatch_heur_st_def state_extractors split: isasat_int_splits intro!: ext) sepref_def rewatch_heur_st_fast_code is ‹(rewatch_heur_st_fast)› :: ‹[rewatch_heur_st_fast_pre]_a isasat_bounded_assn^d → isasat_bounded_assn› supply [[goals_limit=1]] unfolding rewatch_heur_st_fast_alt_def rewatch_heur_st_def rewatch_heur_vdom_def[symmetric] rewatch_heur_st_fast_pre_def by sepref definition length_ivdom_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹length_ivdom_fast_code = read_vdom_wl_heur_code length_ivdom_aivdom_impl› global_interpretation length_ivdom_aivdom: read_vdom_param_adder0 where f = ‹length_ivdom_aivdom_impl› and f' = ‹RETURN o length_ivdom_aivdom› and x_assn = sint64_nat_assn and P = ‹(λS. True)› rewrites ‹read_vdom_wl_heur (RETURN o length_ivdom_aivdom) = RETURN o length_ivdom› and ‹read_vdom_wl_heur_code length_ivdom_aivdom_impl = length_ivdom_fast_code› apply unfold_locales apply (rule vdom_ref) subgoal by (auto simp: read_all_st_def length_ivdom_aivdom_def length_ivdom_def intro!: ext split: isasat_int_splits) subgoal by (auto simp: length_ivdom_fast_code_def) done definition length_avdom_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹length_avdom_fast_code = read_vdom_wl_heur_code length_avdom_aivdom_impl› global_interpretation length_avdom_aivdom: read_vdom_param_adder0 where f = ‹length_avdom_aivdom_impl› and f' = ‹RETURN o length_avdom_aivdom› and x_assn = sint64_nat_assn and P = ‹(λS. True)› rewrites ‹read_vdom_wl_heur (RETURN o length_avdom_aivdom) = RETURN o length_avdom› and ‹read_vdom_wl_heur_code length_avdom_aivdom_impl = length_avdom_fast_code› apply unfold_locales apply (rule vdom_ref) subgoal by (auto simp: read_all_st_def length_avdom_aivdom_def length_avdom_def intro!: ext split: isasat_int_splits) subgoal by (auto simp: length_avdom_fast_code_def) done definition length_tvdom_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹length_tvdom_fast_code = read_vdom_wl_heur_code length_tvdom_aivdom_impl› global_interpretation length_tvdom_aivdom: read_vdom_param_adder0 where f = ‹length_tvdom_aivdom_impl› and f' = ‹RETURN o length_tvdom_aivdom› and x_assn = sint64_nat_assn and P = ‹(λS. True)› rewrites ‹read_vdom_wl_heur (RETURN o length_tvdom_aivdom) = RETURN o length_tvdom› and ‹read_vdom_wl_heur_code length_tvdom_aivdom_impl = length_tvdom_fast_code› apply unfold_locales apply (rule vdom_ref) subgoal by (auto simp: read_all_st_def length_tvdom_aivdom_def length_tvdom_def intro!: ext split: isasat_int_splits) subgoal by (auto simp: length_tvdom_fast_code_def) done lemmas [sepref_fr_rules] = length_ivdom_aivdom.refine[unfolded lambda_comp_true] length_avdom_aivdom.refine[unfolded lambda_comp_true] length_tvdom_aivdom.refine[unfolded lambda_comp_true] lemmas [unfolded inline_direct_return_node_case, llvm_code] = length_ivdom_fast_code_def[unfolded read_all_st_code_def] length_avdom_fast_code_def[unfolded read_all_st_code_def] length_tvdom_fast_code_def[unfolded read_all_st_code_def] sepref_register length_avdom length_ivdom length_tvdom definition is_learned where ‹is_learned N C = (arena_status N C = LEARNED)› sepref_definition is_learned_impl is ‹uncurry (RETURN oo is_learned)› :: ‹[uncurry arena_is_valid_clause_vdom]_a arena_fast_assn^k *_a sint64_nat_assn^k → bool1_assn› unfolding is_learned_def by sepref definition clause_is_learned_heur_code2 :: ‹twl_st_wll_trail_fast2 ⇒ _ ⇒ _› where ‹clause_is_learned_heur_code2 N C = read_arena_wl_heur_code (λCa. is_learned_impl Ca C) N› lemma clause_is_learned_heur_alt_def: ‹RETURN oo clause_is_learned_heur = (λN C'. read_arena_wl_heur (λC. (RETURN ∘∘ is_learned) C C') N)› by (auto simp: clause_is_learned_heur_def read_all_st_def is_learned_def intro!: ext split: isasat_int_splits) global_interpretation arena_is_learned: read_arena_param_adder where R = ‹(snat_rel' TYPE(64))› and f' = ‹λN C. (RETURN oo is_learned) C N› and f = ‹(λN C. is_learned_impl C N)› and x_assn = bool1_assn and P = ‹λC N. arena_is_valid_clause_vdom N C› rewrites ‹(λN C. read_arena_wl_heur_code (λCa. is_learned_impl Ca C) N) = clause_is_learned_heur_code2› and ‹(λN C'. read_arena_wl_heur (λC. (RETURN ∘∘ is_learned) C C') N) = RETURN oo clause_is_learned_heur› apply unfold_locales apply (rule is_learned_impl.refine) subgoal by (auto simp: clause_is_learned_heur_code2_def intro!: ext) subgoal by (subst clause_is_learned_heur_alt_def, rule refl) done definition clause_lbd_heur_code2 :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹clause_lbd_heur_code2 = (λN C. read_arena_wl_heur_code (λCa. arena_lbd_impl Ca C) N)› lemma clause_lbd_heur_alt_def: ‹RETURN ∘∘ clause_lbd_heur = (λN C'. read_arena_wl_heur (λC. (RETURN ∘∘ arena_lbd) C C') N)› by (auto simp: clause_lbd_heur_def read_all_st_def arena_lbd_def split: isasat_int_splits intro!: ext) global_interpretation arena_get_lbd: read_arena_param_adder where R = ‹(snat_rel' TYPE(64))› and f' = ‹λN C. (RETURN oo arena_lbd) C N› and f = ‹(λN C. arena_lbd_impl C N)› and x_assn = uint32_nat_assn and P = ‹λC N. get_clause_LBD_pre N C› rewrites ‹(λN C. read_arena_wl_heur_code (λCa. arena_lbd_impl Ca C) N) = clause_lbd_heur_code2› and ‹(λN C'. read_arena_wl_heur (λC. (RETURN ∘∘ arena_lbd) C C') N) = RETURN oo clause_lbd_heur› and ‹arena_get_lbd.mop = mop_arena_lbd_st› apply unfold_locales apply (rule arena_lbd_impl.refine) subgoal by (auto simp: clause_lbd_heur_code2_def intro!: ext) subgoal by (subst clause_lbd_heur_alt_def, rule refl) subgoal by (auto simp: mop_arena_lbd_st_def mop_arena_lbd_def read_arena_param_adder_ops.mop_def read_all_st_def split: isasat_int_splits intro!: ext) done definition clause_pos_heur_code2 :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹clause_pos_heur_code2 = (λN C. read_arena_wl_heur_code (λCa. arena_pos_impl Ca C) N)› definition mop_arena_pos_st :: ‹_› where ‹mop_arena_pos_st S = mop_arena_pos (get_clauses_wl_heur S)› global_interpretation arena_get_pos: read_arena_param_adder where R = ‹(snat_rel' TYPE(64))› and f' = ‹λN C. (RETURN oo arena_pos) C N› and f = ‹(λN C. arena_pos_impl C N)› and x_assn = sint64_nat_assn and P = ‹λC N. get_saved_pos_pre N C› rewrites ‹(λN C. read_arena_wl_heur_code (λCa. arena_pos_impl Ca C) N) = clause_pos_heur_code2› and ‹arena_get_pos.mop = mop_arena_pos_st› apply unfold_locales apply (rule arena_pos_impl.refine) subgoal by (subst clause_pos_heur_code2_def, rule refl) subgoal by (auto simp: mop_arena_pos_st_def mop_arena_pos_def read_arena_param_adder_ops.mop_def read_all_st_def split: isasat_int_splits intro!: ext) done lemmas [sepref_fr_rules] = arena_get_lbd.refine arena_get_pos.mop_refine arena_get_lbd.mop_refine lemmas [unfolded inline_direct_return_node_case, llvm_code] = clause_lbd_heur_code2_def[unfolded read_all_st_code_def] clause_is_learned_heur_code2_def[unfolded read_all_st_code_def] clause_pos_heur_code2_def[unfolded read_all_st_code_def] is_learned_impl_def sepref_register clause_lbd_heur sepref_register mark_garbage_heur lemma mop_mark_garbage_heur_alt_def: ‹mop_mark_garbage_heur C i = (λS₀. do { ASSERT(mark_garbage_pre (get_clauses_wl_heur S₀, C) ∧ clss_size_lcount (get_learned_count S₀) ≥ 1 ∧ i < length (get_avdom S₀)); let (N, S) = extract_arena_wl_heur S₀; ASSERT (N = get_clauses_wl_heur S₀); let N' = extra_information_mark_to_delete N C; let S = update_arena_wl_heur N' S; let (lcount, S) = extract_lcount_wl_heur S; ASSERT (lcount = get_learned_count S₀); let lcount = clss_size_decr_lcount (lcount); let (vdom, S) = extract_vdom_wl_heur S; ASSERT (vdom = get_aivdom S₀); let S = update_vdom_wl_heur (remove_inactive_aivdom i vdom) S; RETURN (update_lcount_wl_heur lcount S) })› unfolding mop_mark_garbage_heur_def mark_garbage_heur_def by (auto intro!: ext simp: state_extractors split: isasat_int_splits) sepref_def mop_mark_garbage_heur_impl is ‹uncurry2 mop_mark_garbage_heur› :: ‹[λ((C, i), S). length (get_clauses_wl_heur S) ≤ snat64_max]_a sint64_nat_assn^k *_a sint64_nat_assn^k *_a isasat_bounded_assn^d → isasat_bounded_assn› supply [[goals_limit=1]] unfolding mop_mark_garbage_heur_alt_def clause_not_marked_to_delete_heur_pre_def by sepref lemma mark_garbage_heur_alt_def: ‹RETURN ooo mark_garbage_heur = (λC i S₀. do { let (N, S) = extract_arena_wl_heur S₀; ASSERT (N = get_clauses_wl_heur S₀); let N' = extra_information_mark_to_delete N C; let S = update_arena_wl_heur N' S; let (lcount, S) = extract_lcount_wl_heur S; ASSERT (lcount = get_learned_count S₀); let lcount = clss_size_decr_lcount (lcount); let (vdom, S) = extract_vdom_wl_heur S; ASSERT (vdom = get_aivdom S₀); let S = update_vdom_wl_heur (remove_inactive_aivdom i vdom) S; RETURN (update_lcount_wl_heur lcount S)})› unfolding mop_mark_garbage_heur_def mark_garbage_heur_def by (auto intro!: ext simp: state_extractors split: isasat_int_splits) sepref_def mark_garbage_heur_code2 is ‹uncurry2 (RETURN ooo mark_garbage_heur)› :: ‹[λ((C, i), S). mark_garbage_pre (get_clauses_wl_heur S, C) ∧ i < length_avdom S ∧ clss_size_lcount (get_learned_count S) ≥ 1]_a sint64_nat_assn^k *_a sint64_nat_assn^k *_a isasat_bounded_assn^d → isasat_bounded_assn› supply [[goals_limit = 1]] unfolding mark_garbage_heur_alt_def length_avdom_def by sepref lemma mop_mark_garbage_heur3_alt_def: ‹mop_mark_garbage_heur3 C i = (λS₀. do { ASSERT(mark_garbage_pre (get_clauses_wl_heur S₀, C) ∧ clss_size_lcount (get_learned_count S₀) ≥ 1 ∧ i < length (get_tvdom S₀)); let (N, S) = extract_arena_wl_heur S₀; ASSERT (N = get_clauses_wl_heur S₀); let N' = extra_information_mark_to_delete N C; let S = update_arena_wl_heur N' S; let (vdom, S) = extract_vdom_wl_heur S; ASSERT (vdom = get_aivdom S₀); let vdom = remove_inactive_aivdom_tvdom i vdom; let S = update_vdom_wl_heur vdom S; let (lcount, S) = extract_lcount_wl_heur S; ASSERT (lcount = get_learned_count S₀); let lcount = clss_size_decr_lcount lcount; let S = update_lcount_wl_heur lcount S; RETURN S })› unfolding mop_mark_garbage_heur3_def mark_garbage_heur3_def by (auto intro!: ext simp: state_extractors split: isasat_int_splits) sepref_def mop_mark_garbage_heur3_impl is ‹uncurry2 mop_mark_garbage_heur3› :: ‹[λ((C, i), S). length (get_clauses_wl_heur S) ≤ snat64_max]_a sint64_nat_assn^k *_a sint64_nat_assn^k *_a isasat_bounded_assn^d → isasat_bounded_assn› supply [[goals_limit=1]] unfolding mop_mark_garbage_heur3_alt_def by sepref lemma delete_index_vdom_heur_alt_def: ‹RETURN oo delete_index_vdom_heur = (λi S₀. do { let (vdom, S) = extract_vdom_wl_heur S₀; ASSERT (vdom = get_aivdom S₀); let vdom = remove_inactive_aivdom_tvdom i vdom; RETURN (update_vdom_wl_heur vdom S) })› by (auto simp: state_extractors delete_index_vdom_heur_def intro!: ext split: isasat_int_splits) sepref_def delete_index_vdom_heur_fast_code2 is ‹uncurry (RETURN oo delete_index_vdom_heur)› :: ‹[λ(i, S). i < length_tvdom S]_a sint64_nat_assn^k *_a isasat_bounded_assn^d → isasat_bounded_assn› supply [[goals_limit = 1]] supply [simp] = length_tvdom_def unfolding delete_index_vdom_heur_alt_def by sepref lemma access_length_heur_alt_def: ‹RETURN oo access_length_heur = (λN C'. read_arena_wl_heur (λN. RETURN (arena_length N C')) N)› by (auto intro!: ext simp: read_all_st_def access_length_heur_def split: isasat_int_splits) definition access_length_heur_fast_code2 :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹access_length_heur_fast_code2 = (λN C. read_arena_wl_heur_code (λN. arena_length_impl N C) N)› global_interpretation arena_length: read_arena_param_adder where R = ‹snat_rel' TYPE(64)› and f' = ‹λC N. RETURN (arena_length N C)› and f = ‹(λC' N. arena_length_impl N C')› and x_assn = ‹snat_assn' TYPE(64)› and P = ‹(λC S. arena_is_valid_clause_idx S C)› rewrites ‹(λN C'. read_arena_wl_heur (λN. RETURN (arena_length N C')) N) = RETURN oo access_length_heur› and ‹(λN C. read_arena_wl_heur_code (λN. arena_length_impl N C) N) = access_length_heur_fast_code2› apply unfold_locales apply (rule arena_length_impl.refine[unfolded comp_def]) subgoal by (auto simp: access_length_heur_alt_def) subgoal by (auto simp: access_length_heur_fast_code2_def) done lemmas [sepref_fr_rules] = arena_length.refine lemmas [unfolded inline_direct_return_node_case, llvm_code] = access_length_heur_fast_code2_def[unfolded read_all_st_code_def] lemma get_slow_ema_heur_alt_def: ‹RETURN o get_slow_ema_heur = read_heur_wl_heur (RETURN o slow_ema_of)› and get_fast_ema_heur_alt_def: ‹RETURN o get_fast_ema_heur = read_heur_wl_heur (RETURN o fast_ema_of)› by (auto simp: read_all_st_def intro!: ext split: isasat_int_splits) definition get_slow_ema_heur_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹get_slow_ema_heur_fast_code = read_heur_wl_heur_code slow_ema_of_stats_impl› global_interpretation slow_ema: read_heur_param_adder0 where f' = ‹RETURN o slow_ema_of› and f = slow_ema_of_stats_impl and x_assn = ‹ema_assn› and P = ‹(λ_. True)› rewrites ‹read_heur_wl_heur (RETURN o slow_ema_of) = RETURN o get_slow_ema_heur› and ‹read_heur_wl_heur_code slow_ema_of_stats_impl = get_slow_ema_heur_fast_code› apply unfold_locales apply (rule heur_refine) subgoal by (auto simp: get_slow_ema_heur_alt_def) subgoal by (auto simp: get_slow_ema_heur_fast_code_def) done definition get_fast_ema_heur_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹get_fast_ema_heur_fast_code = read_heur_wl_heur_code fast_ema_of_stats_impl› global_interpretation fast_ema: read_heur_param_adder0 where f' = ‹RETURN o fast_ema_of› and f = fast_ema_of_stats_impl and x_assn = ‹ema_assn› and P = ‹(λ_. True)› rewrites ‹read_heur_wl_heur (RETURN o fast_ema_of) = RETURN o get_fast_ema_heur› and ‹read_heur_wl_heur_code fast_ema_of_stats_impl = get_fast_ema_heur_fast_code› apply unfold_locales apply (rule heur_refine) subgoal by (auto simp: get_fast_ema_heur_alt_def) subgoal by (auto simp: get_fast_ema_heur_fast_code_def) done thm get_conflict_count_since_last_restart_heur.simps find_theorems get_conflict_count_since_last_restart RETURN lemma get_conflict_count_since_last_restart_heur_alt_def: ‹RETURN o get_conflict_count_since_last_restart_heur = read_heur_wl_heur (RETURN ∘ get_conflict_count_since_last_restart)› by (auto simp: read_all_st_def intro!: ext split: isasat_int_splits) definition get_conflict_count_since_last_restart_heur_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹get_conflict_count_since_last_restart_heur_fast_code = read_heur_wl_heur_code get_conflict_count_since_last_restart_stats_impl› global_interpretation get_conflict_count_since_last_restart: read_heur_param_adder0 where f' = ‹RETURN o get_conflict_count_since_last_restart› and f = get_conflict_count_since_last_restart_stats_impl and x_assn = ‹word64_assn› and P = ‹(λ_. True)› rewrites ‹read_heur_wl_heur (RETURN o get_conflict_count_since_last_restart) = RETURN o get_conflict_count_since_last_restart_heur› and ‹read_heur_wl_heur_code get_conflict_count_since_last_restart_stats_impl = get_conflict_count_since_last_restart_heur_fast_code› apply unfold_locales apply (rule heur_refine) subgoal by (auto simp: get_conflict_count_since_last_restart_heur_alt_def) subgoal by (auto simp: get_conflict_count_since_last_restart_heur_fast_code_def) done lemma id_lcount_assn: ‹(Mreturn, RETURN) ∈ (lcount_assn)^k →_a lcount_assn› unfolding lcount_assn_def by sepref_to_hoare vcg lemma get_learned_count_alt_def: ‹RETURN o get_learned_count = read_lcount_wl_heur RETURN› by (auto simp: read_all_st_def intro!: ext split: isasat_int_splits) definition get_learned_count_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹get_learned_count_fast_code = read_lcount_wl_heur_code Mreturn› global_interpretation get_lcount: read_lcount_param_adder0 where f' = ‹RETURN› and f = ‹Mreturn› and x_assn = ‹lcount_assn› and P = ‹(λ_. True)› rewrites ‹read_lcount_wl_heur (RETURN) = RETURN o get_learned_count› and ‹read_lcount_wl_heur_code Mreturn = get_learned_count_fast_code› apply unfold_locales apply (rule id_lcount_assn) subgoal by (auto simp: get_learned_count_alt_def) subgoal by (auto simp: get_learned_count_fast_code_def) done definition get_learned_count_number_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹get_learned_count_number_fast_code = read_lcount_wl_heur_code clss_size_lcount_fast_code› global_interpretation get_learned_count_number: read_lcount_param_adder0 where f' = ‹RETURN o clss_size_lcount› and f = ‹clss_size_lcount_fast_code› and x_assn = ‹uint64_nat_assn› and P = ‹(λ_. True)› rewrites ‹read_lcount_wl_heur (RETURN o clss_size_lcount) = RETURN o get_learned_count_number› and ‹read_lcount_wl_heur_code clss_size_lcount_fast_code = get_learned_count_number_fast_code› apply unfold_locales apply (rule clss_size_lcount_fast_code.refine) subgoal by (auto simp: read_all_st_def split: isasat_int_splits intro!: ext) subgoal by (auto simp: get_learned_count_number_fast_code_def) done definition get_learned_count_number' :: ‹isasat ⇒ nat› where ‹get_learned_count_number' S ≡ get_learned_count_number S› lemma [def_pat_rules]: ‹get_learned_count_number$S≡get_learned_count_number'$S› by (auto simp: get_learned_count_number'_def) lemmas [sepref_fr_rules] = slow_ema.refine[unfolded lambda_comp_true] fast_ema.refine[unfolded lambda_comp_true] get_conflict_count_since_last_restart.refine[unfolded lambda_comp_true] get_lcount.refine[unfolded lambda_comp_true] get_learned_count_number.refine[unfolded lambda_comp_true get_learned_count_number'_def[symmetric]] lemmas [unfolded inline_direct_return_node_case, llvm_code] = get_slow_ema_heur_fast_code_def[unfolded read_all_st_code_def] get_fast_ema_heur_fast_code_def[unfolded read_all_st_code_def] get_conflict_count_since_last_restart_heur_fast_code_def[unfolded read_all_st_code_def] get_learned_count_fast_code_def[unfolded read_all_st_code_def] get_learned_count_number_fast_code_def[unfolded read_all_st_code_def] sepref_def learned_clss_count_fast_code is ‹RETURN o learned_clss_count› :: ‹[λS. learned_clss_count S ≤ unat64_max]_a isasat_bounded_assn^k → uint64_nat_assn› unfolding clss_size_allcount_alt_def learned_clss_count_def by sepref definition marked_as_used_st_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where ‹marked_as_used_st_fast_code = (λN C. read_arena_wl_heur_code (λN. marked_as_used_impl N C) N)› global_interpretation marked_used: read_arena_param_adder where R = ‹snat_rel' TYPE(64)› and f' = ‹λC N. RETURN (marked_as_used N C)› and f = ‹(λC' N. marked_as_used_impl N C')› and x_assn = ‹unat_assn' TYPE(2)› and P = ‹(λC S. marked_as_used_pre S C)› rewrites ‹(λN C'. read_arena_wl_heur (λN. RETURN (marked_as_used N C')) N) = RETURN oo marked_as_used_st› and ‹(λN C. read_arena_wl_heur_code (λN. marked_as_used_impl N C) N) = marked_as_used_st_fast_code› apply unfold_locales apply (rule marked_as_used_impl.refine[unfolded comp_def]) subgoal by (auto simp: marked_as_used_st_def read_all_st_def intro!: ext split: isasat_int_splits) subgoal by (auto simp: marked_as_used_st_fast_code_def) done lemmas [sepref_fr_rules] = marked_used.refine lemmas [unfolded inline_direct_return_node_case, llvm_code] = marked_as_used_st_fast_code_def[unfolded read_all_st_code_def] lemma mop_marked_as_used_st_alt_def: ‹mop_marked_as_used_st = marked_used.mop› by (auto intro!: ext split: isasat_int_splits simp: mop_marked_as_used_st_def marked_used.mop_def mop_marked_as_used_def read_all_st_def) lemmas [sepref_fr_rules] = marked_used.mop_refine[unfolded mop_marked_as_used_st_alt_def[symmetric]] sepref_register get_the_propagation_reason_heur delete_index_vdom_heur access_length_heur marked_as_used_st experiment begin export_llvm polarity_st_heur_pol_fast count_decided_st_heur_fast_code get_conflict_wl_is_None_fast_code clause_not_marked_to_delete_heur_code access_lit_in_clauses_heur_fast_code length_ivdom_fast_code length_avdom_fast_code length_tvdom_fast_code clause_is_learned_heur_code2 clause_lbd_heur_code2 mop_mark_garbage_heur_impl mark_garbage_heur_code2 mop_mark_garbage_heur3_impl delete_index_vdom_heur_fast_code2 access_length_heur_fast_code2 get_fast_ema_heur_fast_code get_slow_ema_heur_fast_code get_conflict_count_since_last_restart_heur_fast_code get_learned_count_fast_code end end

Theory IsaSAT_Setup1_LLVM