theory IsaSAT_Other_LLVM imports IsaSAT_Other_Defs IsaSAT_Conflict_Analysis_LLVM IsaSAT_Backtrack_LLVM IsaSAT_Decide_LLVM begin sepref_register get_conflict_wl_is_None decide_wl_or_skip_D_heur skip_and_resolve_loop_wl_D_heur backtrack_wl_D_nlit_heur isasat_current_status count_decided_st_heur get_conflict_wl_is_None_heur lemma cdcl_twl_o_prog_wl_D_heurI1: ‹get_learned_count x = get_learned_count xc ⟹ learned_clss_count x < unat64_max ⟹ learned_clss_count xc ≤ unat64_max› using get_learned_count_learned_clss_countD2[of xc x] by (auto dest: get_learned_count_learned_clss_countD2) lemma cdcl_twl_o_prog_wl_D_heurI: ‹ get_learned_count x = get_learned_count xc ⟹ learned_clss_count x < unat64_max ⟹ learned_clss_count xc < unat64_max› using get_learned_count_learned_clss_countD2[of xc x] by auto sepref_def cdcl_twl_o_prog_wl_D_fast_code is ‹cdcl_twl_o_prog_wl_D_heur› :: ‹[isasat_fast]⇩a isasat_bounded_assn⇧d → bool1_assn ×⇩a isasat_bounded_assn› unfolding cdcl_twl_o_prog_wl_D_heur_def PR_CONST_def unfolding get_conflict_wl_is_None get_conflict_wl_is_None_heur_alt_def[symmetric] supply [[goals_limit = 1]] isasat_fast_def[simp] cdcl_twl_o_prog_wl_D_heurI[intro] apply (annot_unat_const ‹TYPE(32)›) by sepref declare cdcl_twl_o_prog_wl_D_fast_code.refine[sepref_fr_rules] sepref_register cdcl_twl_o_prog_wl_D_heur lemma isasat_fast_alt_def: ‹isasat_fast S = (length_clauses_heur S ≤ 9223372034707292156 ∧ clss_size_lcount (get_learned_count S) < 18446744073709551615 - clss_size_lcountUE (get_learned_count S) ∧ clss_size_lcount (get_learned_count S) + clss_size_lcountUE (get_learned_count S) < 18446744073709551615 - clss_size_lcountUS (get_learned_count S) ∧ clss_size_lcount (get_learned_count S) + clss_size_lcountUE (get_learned_count S) + clss_size_lcountUS (get_learned_count S) < 18446744073709551615 - clss_size_lcountU0 (get_learned_count S) ∧ clss_size_lcount (get_learned_count S) + clss_size_lcountUE (get_learned_count S) + clss_size_lcountUS (get_learned_count S) + clss_size_lcountU0 (get_learned_count S) < 18446744073709551615 - clss_size_lcountUEk (get_learned_count S)∧ clss_size_lcount (get_learned_count S) + clss_size_lcountUE (get_learned_count S) + clss_size_lcountUS (get_learned_count S) + clss_size_lcountU0 (get_learned_count S) + clss_size_lcountUEk (get_learned_count S) < 18446744073709551615)› by (cases S; auto simp: isasat_fast_def snat64_max_def unat32_max_def length_clauses_heur_def unat64_max_def learned_clss_count_def clss_size_lcountU0_def) sepref_def isasat_fast_impl is ‹RETURN o isasat_fast› :: ‹isasat_bounded_assn⇧k →⇩a bool1_assn› unfolding isasat_fast_alt_def short_circuit_conv apply (rewrite at ‹_ < ⌑› unat_const_fold[where 'a=64])+ apply (rewrite at ‹_ < ⌑ - _› unat_const_fold[where 'a=64])+ apply (annot_snat_const ‹TYPE(64)›) by sepref end