Theory IsaSAT_Stats

theory IsaSAT_Stats_LLVM imports IsaSAT_Stats IsaSAT_EMA_LLVM IsaSAT_Rephase_LLVM IsaSAT_Reluctant_LLVM Tuple16_LLVM begin hide_const (open) NEMonad.RETURN NEMonad.ASSERT lemma Exists_eq_simp_sym: ‹(∃x. (P x ∧* ↑ (b = x)) s) ⟷ P b s› by (subst eq_commute[of b]) (rule Exists_eq_simp) definition code_hider_assn where ‹code_hider_assn R S = hr_comp R (⟨S⟩code_hider_rel)› lemma get_content_destroyed_kept[sepref_fr_rules]: ‹CONSTRAINT is_pure R ⟹ (Mreturn o id, RETURN o get_content) ∈ (code_hider_assn R S)^k →_a hr_comp R S› unfolding code_hider_assn_def code_hider_rel_def apply sepref_to_hoare apply vcg apply (auto simp: br_def ENTAILS_def Exists_eq_simp Exists_eq_simp_sym hr_comp_def pure_true_conv) by (smt (z3) Sep_Algebra_Add.pure_part_pure entails_def is_pure_conv pure_app_eq pure_partI sep.mult_assoc sep_conj_def split_conj_is_pure) lemma Constructor_assn_destroyed: ‹(Mreturn o id, RETURN o Constructor) ∈ (hr_comp R S)^d →_a code_hider_assn R S› unfolding code_hider_assn_def code_hider_rel_def apply sepref_to_hoare apply vcg by (auto simp: br_def ENTAILS_def Exists_eq_simp Exists_eq_simp_sym hr_comp_def pure_true_conv) lemma get_content_destroyed: ‹(Mreturn o id, RETURN o get_content) ∈ (code_hider_assn R S)^d →_a hr_comp R S› unfolding code_hider_assn_def code_hider_rel_def apply sepref_to_hoare apply vcg by (auto simp: br_def ENTAILS_def Exists_eq_simp Exists_eq_simp_sym hr_comp_def pure_true_conv) lemma get_content_hnr[sepref_fr_rules]: ‹(id, get_content) ∈ ⟨S⟩code_hider_rel →_f S› unfolding code_hider_rel_def by (auto simp: intro!: frefI) lemma Constructor_hnr[sepref_fr_rules]: ‹(id, Constructor) ∈ S →_f ⟨S⟩code_hider_rel› unfolding code_hider_rel_def by (auto simp: intro!: frefI) definition search_stats_assn :: ‹search_stats ⇒ search_stats ⇒ _› where ‹search_stats_assn ≡ word64_assn ×_a word64_assn ×_a word64_assn ×_aword64_assn ×_a word64_assn ×_a word64_assn ×_aword64_assn ×_a word64_assn ×_a word64_assn ×_a word64_assn› definition subsumption_stats_assn :: ‹inprocessing_subsumption_stats ⇒ inprocessing_subsumption_stats ⇒ _› where ‹subsumption_stats_assn = word64_assn ×_a word64_assn ×_a word64_assn ×_a word64_assn ×_a word64_assn› definition binary_stats_assn :: ‹inprocessing_binary_stats ⇒ inprocessing_binary_stats ⇒ _› where ‹binary_stats_assn = word64_assn ×_a word64_assn ×_a word64_assn› definition pure_lits_stats_assn :: ‹inprocessing_pure_lits_stats ⇒ inprocessing_pure_lits_stats ⇒ _› where ‹pure_lits_stats_assn = word64_assn ×_a word64_assn› definition rephase_stats_assn :: ‹rephase_stats ⇒ rephase_stats ⇒ _› where ‹rephase_stats_assn ≡ word64_assn ×_a word64_assn ×_a word64_assn ×_aword64_assn ×_a word64_assn ×_a word64_assn› definition empty_search_stats where ‹empty_search_stats = (0,0,0,0,0,0,0,0,0,0)› sepref_def empty_search_stats_impl is ‹uncurry0 (RETURN empty_search_stats)› :: ‹unit_assn^k →_a search_stats_assn› unfolding search_stats_assn_def empty_search_stats_def by sepref definition empty_binary_stats :: ‹inprocessing_binary_stats› where ‹empty_binary_stats = (0,0,0)› sepref_def empty_binary_stats_impl is ‹uncurry0 (RETURN empty_binary_stats)› :: ‹unit_assn^k →_a binary_stats_assn› unfolding binary_stats_assn_def empty_binary_stats_def by sepref definition empty_subsumption_stats :: ‹inprocessing_subsumption_stats› where ‹empty_subsumption_stats = (0,0,0,0,0)› sepref_def empty_subsumption_stats_impl is ‹uncurry0 (RETURN empty_subsumption_stats)› :: ‹unit_assn^k →_a subsumption_stats_assn› unfolding subsumption_stats_assn_def empty_subsumption_stats_def by sepref definition empty_pure_lits_stats :: ‹inprocessing_pure_lits_stats› where ‹empty_pure_lits_stats = (0,0)› sepref_def empty_pure_lits_stats_impl is ‹uncurry0 (RETURN empty_pure_lits_stats)› :: ‹unit_assn^k →_a pure_lits_stats_assn› unfolding pure_lits_stats_assn_def empty_pure_lits_stats_def by sepref definition lbd_size_limit_assn where ‹lbd_size_limit_assn = uint32_nat_assn ×_a sint64_nat_assn› definition empty_lsize_limit_stats :: ‹lbd_size_limit_stats› where ‹empty_lsize_limit_stats = (0,0)› sepref_def empty_lsize_limit_stats_impl is ‹uncurry0 (RETURN empty_lsize_limit_stats)› :: ‹unit_assn^k →_a lbd_size_limit_assn› unfolding lbd_size_limit_assn_def empty_lsize_limit_stats_def apply (rewrite at ‹(_, ⌑)› snat_const_fold[where 'a=64]) apply (rewrite at ‹(⌑, _)› unat_const_fold[where 'a=32]) by sepref definition ema_init_bottom :: ‹ema› where ‹ema_init_bottom = ema_init 0› sepref_def ema_init_bottom_impl is ‹uncurry0 (RETURN ema_init_bottom)› :: ‹unit_assn^k →_a ema_assn› unfolding ema_init_bottom_def by sepref lemma stats_bottom: ‹(uncurry0 (return_M 0), uncurry0 (RETURN 0)) ∈ unit_assn^k →_a word64_assn› ‹(uncurry0 (return_M 0), uncurry0 (RETURN 0)) ∈ unit_assn^k →_a word32_assn› by (sepref_to_hoare; vcg; fail)+ definition empty_rephase_stats :: ‹rephase_stats› where ‹empty_rephase_stats = (0,0,0,0,0,0)› sepref_def empty_rephase_stats_impl is ‹uncurry0 (RETURN empty_rephase_stats)› :: ‹unit_assn^k →_a rephase_stats_assn› unfolding empty_rephase_stats_def rephase_stats_assn_def by sepref schematic_goal mk_free_search_stats_assn[sepref_frame_free_rules]: ‹MK_FREE search_stats_assn ?fr› and mk_free_binary_stats_assn[sepref_frame_free_rules]: ‹MK_FREE binary_stats_assn ?fr2› and mk_free_subsumption_stats_assn[sepref_frame_free_rules]: ‹MK_FREE subsumption_stats_assn ?fr3› and mk_free_ema_assn[sepref_frame_free_rules]: ‹MK_FREE ema_assn ?fr4›and mk_free_pure_lits_stats_assn[sepref_frame_free_rules]: ‹MK_FREE pure_lits_stats_assn ?fr5› and mk_free_rephase_stats_assn[sepref_frame_free_rules]: ‹MK_FREE rephase_stats_assn ?fr6› unfolding search_stats_assn_def binary_stats_assn_def subsumption_stats_assn_def pure_lits_stats_assn_def rephase_stats_assn_def by synthesize_free+ sepref_def free_search_stats_assn is ‹mop_free› :: ‹search_stats_assn^d →_a unit_assn› by sepref sepref_def free_binary_stats_assn is ‹mop_free› :: ‹binary_stats_assn^d →_a unit_assn› by sepref sepref_def free_subsumption_stats_assn is ‹mop_free› :: ‹subsumption_stats_assn^d →_a unit_assn› by sepref sepref_def free_pure_lits_stats_assn is ‹mop_free› :: ‹pure_lits_stats_assn^d →_a unit_assn› by sepref sepref_def free_ema_assn is ‹mop_free› :: ‹ema_assn^d →_a unit_assn› by sepref sepref_def free_word64_assn is ‹mop_free› :: ‹word64_assn^d →_a unit_assn› by sepref sepref_def free_word32_assn is ‹mop_free› :: ‹word32_assn^d →_a unit_assn› by sepref sepref_def free_lbd_size_limit_assn is ‹mop_free› :: ‹lbd_size_limit_assn^d →_a unit_assn› unfolding lbd_size_limit_assn_def by sepref sepref_def free_rephase_stats_assn is ‹mop_free› :: ‹rephase_stats_assn^d →_a unit_assn› by sepref lemma mop_free_hnr': ‹(f, mop_free) ∈ R^d →_a unit_assn ⟹ MK_FREE R f› unfolding mop_free_def apply (rule MK_FREEI) apply simp subgoal for a c apply (drule hfrefD[of _ _ _ _ _ _ _ a c]) apply (rule TrueI) apply (rule TrueI) apply (drule hn_refineD) apply simp apply (rule htriple_pure_preI[of ]) unfolding fst_conv snd_conv hf_pres.simps apply (clarsimp simp: hn_ctxt_def pure_def sep_algebra_simps invalid_assn_def) done done type_synonym isasat_stats_assn = ‹(search_stats, inprocessing_binary_stats, inprocessing_subsumption_stats, ema, inprocessing_pure_lits_stats, 32 word × 64 word, rephase_stats, 64 word, 64 word, 64 word,64 word, 64 word, 64 word, 64 word, 32 word, 64 word) tuple16› definition isasat_stats_assn :: ‹isasat_stats ⇒ isasat_stats_assn ⇒ _ ⇒ bool› where ‹isasat_stats_assn = tuple16_assn search_stats_assn binary_stats_assn subsumption_stats_assn ema_assn pure_lits_stats_assn lbd_size_limit_assn rephase_stats_assn word64_assn word64_assn word64_assn word64_assn word64_assn word64_assn word64_assn word32_assn word64_assn› definition extract_search_strategy_stats :: ‹isasat_stats ⇒ _› where ‹extract_search_strategy_stats = tuple16_ops.remove_a empty_search_stats› definition extract_binary_stats :: ‹isasat_stats ⇒ _› where ‹extract_binary_stats = tuple16_ops.remove_b empty_binary_stats› definition extract_subsumption_stats :: ‹isasat_stats ⇒ _› where ‹extract_subsumption_stats = tuple16_ops.remove_c empty_subsumption_stats› definition extract_avg_lbd :: ‹isasat_stats ⇒ _› where ‹extract_avg_lbd = tuple16_ops.remove_d ema_init_bottom› definition extract_pure_lits_stats :: ‹isasat_stats ⇒ _› where ‹extract_pure_lits_stats = tuple16_ops.remove_e empty_pure_lits_stats› definition extract_lbd_size_limit_stats :: ‹isasat_stats ⇒ _› where ‹extract_lbd_size_limit_stats = tuple16_ops.remove_f empty_lsize_limit_stats› definition extract_rephase_stats :: ‹isasat_stats ⇒ _› where ‹extract_rephase_stats = tuple16_ops.remove_g empty_rephase_stats› tuple16 where a_assn = search_stats_assn and b_assn = binary_stats_assn and c_assn = subsumption_stats_assn and d_assn = ema_assn and e_assn = pure_lits_stats_assn and f_assn = lbd_size_limit_assn and g_assn = rephase_stats_assn and h_assn = word64_assn and i_assn = word64_assn and j_assn = word64_assn and k_assn = word64_assn and l_assn = word64_assn and m_assn = word64_assn and n_assn = word64_assn and o_assn = word32_assn and p_assn = word64_assn and a_default = empty_search_stats and a = empty_search_stats_impl and b_default = empty_binary_stats and b = empty_binary_stats_impl and c_default = empty_subsumption_stats and c = empty_subsumption_stats_impl and d_default = ema_init_bottom and d = ema_init_bottom_impl and e_default = empty_pure_lits_stats and e = empty_pure_lits_stats_impl and f_default = ‹empty_lsize_limit_stats› and f = ‹empty_lsize_limit_stats_impl› and g_default = ‹empty_rephase_stats› and g = ‹empty_rephase_stats_impl› and h_default = ‹0› and h = ‹Mreturn 0› and i_default = ‹0› and i = ‹Mreturn 0› and j_default = ‹0› and j = ‹Mreturn 0› and k_default = ‹0› and k = ‹Mreturn 0› and l_default = ‹0› and l = ‹Mreturn 0› and m_default = ‹0› and m = ‹Mreturn 0› and n_default = ‹0› and n = ‹Mreturn 0› and ko_default = ‹0› and ko = ‹Mreturn 0› and p_default = ‹0› and p = ‹Mreturn 0› and a_free = free_search_stats_assn and b_free = free_binary_stats_assn and c_free = free_subsumption_stats_assn and d_free = free_ema_assn and e_free = free_pure_lits_stats_assn and f_free = free_lbd_size_limit_assn and g_free = free_rephase_stats_assn and h_free = free_word64_assn and i_free = free_word64_assn and j_free = free_word64_assn and k_free = free_word64_assn and l_free = free_word64_assn and m_free = free_word64_assn and n_free = free_word64_assn and o_free = free_word32_assn and p_free = free_word64_assn rewrites ‹isasat_assn = isasat_stats_assn› and ‹remove_a = extract_search_strategy_stats› and ‹remove_b = extract_binary_stats› and ‹remove_c = extract_subsumption_stats› and ‹remove_d = extract_avg_lbd› and ‹remove_e = extract_pure_lits_stats› and ‹remove_f = extract_lbd_size_limit_stats› and ‹remove_g = extract_rephase_stats› apply unfold_locales apply (rule empty_search_stats_impl.refine empty_binary_stats_impl.refine empty_subsumption_stats_impl.refine ema_init_bottom_impl.refine empty_pure_lits_stats_impl.refine stats_bottom free_search_stats_assn.refine[THEN mop_free_hnr'] free_binary_stats_assn.refine[THEN mop_free_hnr'] free_subsumption_stats_assn.refine[THEN mop_free_hnr'] free_ema_assn.refine[THEN mop_free_hnr'] free_pure_lits_stats_assn.refine[THEN mop_free_hnr'] empty_lsize_limit_stats_impl.refine free_pure_lits_stats_assn.refine[THEN mop_free_hnr', unfolded lbd_size_limit_assn_def[symmetric] pure_lits_stats_assn_def] free_word64_assn.refine[THEN mop_free_hnr'] free_word32_assn.refine[THEN mop_free_hnr'] free_lbd_size_limit_assn.refine[THEN mop_free_hnr'] free_rephase_stats_assn.refine[THEN mop_free_hnr'] empty_rephase_stats_impl.refine )+ subgoal unfolding isasat_stats_assn_def tuple16_ops.isasat_assn_def .. subgoal unfolding extract_search_strategy_stats_def .. subgoal unfolding extract_binary_stats_def .. subgoal unfolding extract_subsumption_stats_def .. subgoal unfolding extract_avg_lbd_def .. subgoal unfolding extract_pure_lits_stats_def .. subgoal unfolding extract_lbd_size_limit_stats_def .. subgoal unfolding extract_rephase_stats_def .. done sepref_register remove_a remove_b remove_c remove_d remove_e remove_f remove_g remove_h remove_i remove_j remove_k remove_l remove_m remove_n remove_o remove_p fun tuple16_rel :: ‹ ('a × _ ) set ⇒ ('b × _ ) set ⇒ ('c × _ ) set ⇒ ('d × _ ) set ⇒ ('e × _ ) set ⇒ ('f × _ ) set ⇒ ('g × _ ) set ⇒ ('h × _ ) set ⇒ ('i × _ ) set ⇒ ('j × _ ) set ⇒ ('k × _ ) set ⇒ ('l × _ ) set ⇒ ('m × _ ) set ⇒ ('n × _ ) set ⇒ ('o × _ ) set ⇒ ('p × _ ) set ⇒ (('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j, 'k, 'l, 'm, 'n, 'o, 'p) tuple16 × _)set› where ‹tuple16_rel a_assn b_assn' c_assn d_assn e_assn f_assn g_assn h_assn i_assn j_assn k_assn l_assn m_assn n_assn o_assn p_assn = {(S, T). case (S, T) of (Tuple16 M N D i W ivmtf icount ccach lbd outl heur stats aivdom clss opts arena, Tuple16 M' N' D' i' W' ivmtf' icount' ccach' lbd' outl' heur' stats' aivdom' clss' opts' arena') ⇒ ((M, M')∈a_assn ∧ (N, N')∈b_assn' ∧ (D, D')∈c_assn ∧ (i,i')∈d_assn ∧ (W, W')∈e_assn ∧ (ivmtf, ivmtf')∈f_assn ∧ (icount, icount')∈ g_assn ∧ (ccach,ccach')∈ h_assn∧ (lbd,lbd')∈i_assn ∧ (outl,outl')∈ j_assn∧ (heur,heur')∈k_assn ∧ (stats,stats')∈ l_assn∧ (aivdom,aivdom')∈ m_assn∧ (clss,clss')∈ n_assn∧ (opts,opts')∈o_assn ∧ (arena,arena')∈p_assn) }› lemma tuple16_assn_tuple16_rel: ‹tuple16_assn (pure A) (pure B)(pure C)(pure D)(pure E)(pure F)(pure G)(pure H)(pure I)(pure J)(pure K)(pure L)(pure M)(pure N)(pure KO)(pure P) = pure (tuple16_rel A B C D E F G H I J K L M N KO P)› by (auto intro!: ext simp: pure_def import_param_3(1) split: tuple16.splits) lemma pure_keep_detroy: "(pure R)^k = (pure R)^d" by (auto intro!: ext simp: invalid_pure_recover) lemma "is_pure R ⟹ R^k = R^d" by (metis is_pure_conv pure_keep_detroy) lemma isasat_stats_assn_pure_keep: ‹isasat_stats_assn^d = isasat_stats_assn^k› unfolding isasat_stats_assn_def tuple16_assn_tuple16_rel search_stats_assn_def lbd_size_limit_assn_def prod_assn_pure_conv pure_lits_stats_assn_def subsumption_stats_assn_def rephase_stats_assn_def binary_stats_assn_def pure_lits_stats_assn_def pure_keep_detroy .. lemmas [unfolded isasat_stats_assn_pure_keep, sepref_fr_rules] = remove_a_code.refine remove_b_code.refine remove_c_code.refine remove_d_code.refine remove_e_code.refine remove_f_code.refine remove_g_code.refine named_theorems stats_extractors ‹Definition of all functions modifying the state› lemmas [stats_extractors] = extract_search_strategy_stats_def extract_binary_stats_def extract_subsumption_stats_def extract_avg_lbd_def extract_pure_lits_stats_def tuple16_ops.remove_a_def tuple16_ops.remove_b_def tuple16_ops.remove_c_def tuple16_ops.remove_d_def tuple16_ops.remove_e_def tuple16_ops.remove_f_def tuple16_ops.remove_g_def tuple16_ops.update_a_def tuple16_ops.update_b_def tuple16_ops.update_c_def tuple16_ops.update_d_def tuple16_ops.update_e_def tuple16_ops.update_f_def tuple16_ops.update_g_def text ‹We do some cheating to simplify code generation, instead of using our alternative definitions as for the states.› lemma stats_code_unfold: ‹get_search_stats x = fst (extract_search_strategy_stats x)› ‹get_binary_stats x = fst (extract_binary_stats x)› ‹get_subsumption_stats x = fst (extract_subsumption_stats x)› ‹get_pure_lits_stats x = fst (extract_pure_lits_stats x)› ‹get_avg_lbd_stats x = fst (extract_avg_lbd x)› ‹get_lsize_limit_stats x = fst (extract_lbd_size_limit_stats x)› ‹get_rephase_stats x = fst (extract_rephase_stats x)› ‹set_propagation_stats a x = update_a a x› ‹set_binary_stats b x = update_b b x› ‹set_subsumption_stats c x = update_c c x› ‹set_avg_lbd_stats lbd x = update_d lbd x› ‹set_pure_lits_stats e x = update_e e x› ‹set_lsize_limit_stats f x = update_f f x› ‹set_rephase_stats g x = update_g g x› by (cases x; auto simp: get_search_stats_def get_avg_lbd_stats_def set_avg_lbd_stats_def set_propagation_stats_def set_binary_stats_def get_rephase_stats_def set_subsumption_stats_def set_pure_lits_stats_def get_lsize_limit_stats_def extract_lbd_size_limit_stats_def set_rephase_stats_def extract_rephase_stats_def get_subsumption_stats_def get_pure_lits_stats_def set_lsize_limit_stats_def get_binary_stats_def stats_extractors; fail)+ lemma Mreturn_comp_Tuple16: ‹(Mreturn o₁₆ Tuple16) a b c d e f g h i j k l m n ko p = Mreturn (Tuple16 a b c d e f g h i j k l m n ko p)› by auto lemmas [unfolded inline_direct_return_node_case, llvm_code] = remove_a_code_alt_def[unfolded tuple16.remove_a_code_alt_def Mreturn_comp_Tuple16] remove_b_code_alt_def[unfolded tuple16.remove_b_code_alt_def Mreturn_comp_Tuple16] remove_c_code_alt_def[unfolded tuple16.remove_c_code_alt_def Mreturn_comp_Tuple16] remove_d_code_alt_def[unfolded tuple16.remove_d_code_alt_def Mreturn_comp_Tuple16] remove_e_code_alt_def[unfolded tuple16.remove_e_code_alt_def Mreturn_comp_Tuple16] remove_f_code_alt_def[unfolded tuple16.remove_f_code_alt_def Mreturn_comp_Tuple16] remove_g_code_alt_def[unfolded tuple16.remove_g_code_alt_def Mreturn_comp_Tuple16] lemma [safe_constraint_rules]: ‹CONSTRAINT is_pure isasat_stats_assn› unfolding isasat_stats_assn_def tuple16_assn_tuple16_rel search_stats_assn_def prod_assn_pure_conv pure_lits_stats_assn_def subsumption_stats_assn_def lbd_size_limit_assn_def binary_stats_assn_def pure_lits_stats_assn_def pure_keep_detroy rephase_stats_assn_def by auto lemma id_unat[sepref_fr_rules]: ‹(Mreturn o id, RETURN o unat) ∈ word32_assn^k →_a uint32_nat_assn› apply sepref_to_hoare apply vcg by (auto simp: ENTAILS_def unat_rel_def unat.rel_def br_def pred_lift_merge_simps pred_lift_def pure_true_conv) lemma [sepref_fr_rules]: ‹CONSTRAINT is_pure B ⟹ (Mreturn o (λ(a,b). a), RETURN o fst) ∈ (A ×_a B)^d →_a A› apply sepref_to_hoare apply vcg apply (auto simp: ENTAILS_def) by (smt (verit, best) entails_def fri_startI_extended(3) is_pure_iff_pure_assn pure_part_pure_eq pure_part_split_conj pure_true_conv sep_conj_aci(5)) sepref_def Search_Stats_conflicts_impl is ‹RETURN o Search_Stats_conflicts› :: ‹search_stats_assn^k →_a word64_assn› unfolding search_stats_assn_def Search_Stats_conflicts_def by sepref sepref_def Search_Stats_units_since_gcs_impl is ‹RETURN o Search_Stats_units_since_gcs› :: ‹search_stats_assn^k →_a word64_assn› unfolding search_stats_assn_def Search_Stats_units_since_gcs_def by sepref sepref_def Search_Stats_reset_units_since_gc_impl is ‹RETURN o Search_Stats_reset_units_since_gc› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_reset_units_since_gc_def by sepref sepref_def Search_Stats_fixed_impl is ‹RETURN o Search_Stats_fixed› :: ‹search_stats_assn^k →_a word64_assn› unfolding search_stats_assn_def Search_Stats_fixed_def by sepref sepref_def add_lbd_stats_impl is ‹uncurry (RETURN oo add_lbd)› :: ‹word32_assn^k *_a isasat_stats_assn^d →_a isasat_stats_assn› unfolding add_lbd_def stats_code_unfold by sepref sepref_def get_conflict_count_stats_impl is ‹(RETURN o get_conflict_count)› :: ‹isasat_stats_assn^k →_a word_assn› unfolding stats_conflicts_def stats_code_unfold by sepref sepref_def units_since_last_GC_stats_impl is ‹(RETURN o units_since_last_GC)› :: ‹isasat_stats_assn^k →_a word_assn› unfolding units_since_last_GC_def stats_code_unfold by sepref sepref_def reset_units_since_last_GC_stats_impl is ‹(RETURN o reset_units_since_last_GC)› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding reset_units_since_last_GC_def stats_code_unfold by sepref sepref_def Search_Stats_incr_irred_impl is ‹RETURN o Search_Stats_incr_irred› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_irred_def by sepref sepref_def Search_Stats_decr_irred_impl is ‹RETURN o Search_Stats_decr_irred› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_decr_irred_def by sepref sepref_def Search_Stats_incr_propagation_impl is ‹RETURN o Search_Stats_incr_propagation› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_propagation_def by sepref sepref_def Search_Stats_incr_propagation_by_impl is ‹uncurry (RETURN oo Search_Stats_incr_propagation_by)› :: ‹word64_assn^k *_a search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_propagation_by_def by sepref sepref_def Search_Stats_set_not_conflict_until_impl is ‹uncurry (RETURN oo Search_Stats_set_no_conflict_until)› :: ‹word64_assn^k *_a search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_set_no_conflict_until_def by sepref sepref_def Search_Stats_no_conflict_until_impl is ‹RETURN o Search_Stats_no_conflict_until› :: ‹search_stats_assn^k →_a word64_assn› unfolding search_stats_assn_def Search_Stats_no_conflict_until_def by sepref sepref_def Search_Stats_incr_conflicts_impl is ‹RETURN o Search_Stats_incr_conflicts› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_conflicts_def by sepref sepref_def Search_Stats_incr_decisions_impl is ‹RETURN o Search_Stats_incr_decisions› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_decisions_def by sepref sepref_def Search_Stats_incr_restarts_impl is ‹RETURN o Search_Stats_incr_restarts› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_restarts_def by sepref sepref_def Search_Stats_incr_reductions_impl is ‹RETURN o Search_Stats_incr_reductions› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_reductions_def by sepref sepref_def Search_Stats_incr_fixed_impl is ‹RETURN o Search_Stats_incr_fixed› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_fixed_def by sepref sepref_def Search_Stats_incr_fixed_by_impl is ‹uncurry (RETURN oo Search_Stats_incr_fixed_by)› :: ‹word64_assn^k *_a search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_fixed_by_def by sepref sepref_def Search_Stats_incr_gcs_impl is ‹RETURN o Search_Stats_incr_gcs› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_gcs_def by sepref sepref_def Search_Stats_incr_gcs_by_impl is ‹uncurry (RETURN oo Search_Stats_incr_units_since_gc_by)› :: ‹word64_assn^k *_a search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_units_since_gc_by_def by sepref sepref_def Search_Stats_incr_units_since_gc_impl is ‹RETURN o Search_Stats_incr_units_since_gc› :: ‹search_stats_assn^k →_a search_stats_assn› unfolding search_stats_assn_def Search_Stats_incr_units_since_gc_def by sepref sepref_def Pure_lits_Stats_incr_rounds_impl is ‹RETURN o Pure_lits_Stats_incr_rounds› :: ‹pure_lits_stats_assn^k →_a pure_lits_stats_assn› unfolding pure_lits_stats_assn_def Pure_lits_Stats_incr_rounds_def by sepref sepref_def Pure_lits_Stats_incr_removed_impl is ‹RETURN o Pure_lits_Stats_incr_removed› :: ‹pure_lits_stats_assn^k →_a pure_lits_stats_assn› unfolding pure_lits_stats_assn_def Pure_lits_Stats_incr_removed_def by sepref sepref_def Binary_Stats_incr_units_impl is ‹RETURN o Binary_Stats_incr_units› :: ‹binary_stats_assn^k →_a binary_stats_assn› unfolding binary_stats_assn_def Binary_Stats_incr_units_def by sepref sepref_def Binary_Stats_incr_removed_def is ‹RETURN o Binary_Stats_incr_removed› :: ‹binary_stats_assn^k →_a binary_stats_assn› unfolding Binary_Stats_incr_removed_def binary_stats_assn_def by sepref sepref_def Search_Stats_restarts_impl is ‹RETURN o Search_Stats_restarts› :: ‹search_stats_assn^k →_a word64_assn› unfolding search_stats_assn_def Search_Stats_restarts_def by sepref sepref_def Search_Stats_reductions_impl is ‹RETURN o Search_Stats_reductions› :: ‹search_stats_assn^k →_a word64_assn› unfolding search_stats_assn_def Search_Stats_reductions_def by sepref sepref_def Search_Stats_irred_impl is ‹RETURN o Search_Stats_irred› :: ‹search_stats_assn^k →_a word64_assn› unfolding search_stats_assn_def Search_Stats_irred_def by sepref sepref_def Search_Stats_propagations_impl is ‹RETURN o Search_Stats_propagations› :: ‹search_stats_assn^k →_a word64_assn› unfolding search_stats_assn_def Search_Stats_propagations_def by sepref sepref_def Search_Stats_gcs_impl is ‹RETURN o Search_Stats_gcs› :: ‹search_stats_assn^k →_a word64_assn› unfolding search_stats_assn_def Search_Stats_gcs_def by sepref sepref_register Search_Stats_fixed Search_Stats_incr_irred Search_Stats_decr_irred Search_Stats_incr_propagation Search_Stats_incr_conflicts Search_Stats_incr_decisions Search_Stats_incr_restarts Search_Stats_incr_reductions Search_Stats_incr_fixed Search_Stats_incr_gcs Pure_lits_Stats_incr_rounds Pure_lits_Stats_incr_removed Binary_Stats_incr_removed Binary_Stats_incr_units Search_Stats_reductions Search_Stats_restarts Search_Stats_irred Search_Stats_propagations Search_Stats_gcs sepref_def Search_Stats_decisions_impl is ‹RETURN o Search_Stats_decisions› :: ‹search_stats_assn^k →_a word64_assn› unfolding search_stats_assn_def Search_Stats_decisions_def by sepref sepref_def Binary_stats_rounds_impl is ‹RETURN o Binary_Stats_rounds› :: ‹binary_stats_assn^k →_a word64_assn› unfolding binary_stats_assn_def Binary_Stats_rounds_def by sepref sepref_def Binary_stats_units_impl is ‹RETURN o Binary_Stats_units› :: ‹binary_stats_assn^k →_a word64_assn› unfolding binary_stats_assn_def Binary_Stats_units_def by sepref sepref_def Binary_stats_removed_impl is ‹RETURN o Binary_Stats_removed› :: ‹binary_stats_assn^k →_a word64_assn› unfolding binary_stats_assn_def Binary_Stats_removed_def by sepref sepref_def Pure_Lits_Stats_removed_impl is ‹RETURN o Pure_Lits_Stats_removed› :: ‹pure_lits_stats_assn^k →_a word64_assn› unfolding pure_lits_stats_assn_def Pure_Lits_Stats_removed_def by sepref sepref_def Pure_Lits_Stats_removed_rounds_impl is ‹RETURN o Pure_Lits_Stats_rounds› :: ‹pure_lits_stats_assn^k →_a word64_assn› unfolding pure_lits_stats_assn_def Pure_Lits_Stats_rounds_def by sepref sepref_def LSize_Stats_lbd_impl is ‹RETURN o LSize_Stats_lbd› :: ‹lbd_size_limit_assn^k →_a uint32_nat_assn› unfolding LSize_Stats_lbd_def lbd_size_limit_assn_def by sepref sepref_def LSize_Stats_size_impl is ‹RETURN o LSize_Stats_size› :: ‹lbd_size_limit_assn^k →_a sint64_nat_assn› unfolding LSize_Stats_size_def lbd_size_limit_assn_def by sepref sepref_def LSize_Stats_impl is ‹uncurry (RETURN oo LSize_Stats)› :: ‹uint32_nat_assn^k *_a sint64_nat_assn^k →_a lbd_size_limit_assn› unfolding LSize_Stats_def lbd_size_limit_assn_def by sepref sepref_register Search_Stats_decisions Pure_Lits_Stats_rounds Pure_Lits_Stats_removed Binary_Stats_removed Binary_Stats_rounds Binary_Stats_units sepref_def stats_decisions_impl is ‹RETURN o stats_decisions› :: ‹isasat_stats_assn^k →_a word64_assn› unfolding stats_decisions_def stats_code_unfold by sepref sepref_def stats_irred_impl is ‹RETURN o stats_irred› :: ‹isasat_stats_assn^k →_a word64_assn› unfolding stats_irred_def stats_code_unfold by sepref sepref_def stats_binary_units_impl is ‹RETURN o stats_binary_units› :: ‹isasat_stats_assn^k →_a word64_assn› unfolding stats_binary_units_def stats_code_unfold by sepref sepref_def stats_binary_removed_impl is ‹RETURN o stats_binary_removed› :: ‹isasat_stats_assn^k →_a word64_assn› unfolding stats_binary_removed_def stats_code_unfold by sepref sepref_def stats_binary_rounds_impl is ‹RETURN o stats_binary_rounds› :: ‹isasat_stats_assn^k →_a word64_assn› unfolding stats_binary_rounds_def stats_code_unfold by sepref sepref_def stats_pure_lits_rounds_impl is ‹RETURN o stats_pure_lits_rounds› :: ‹isasat_stats_assn^k →_a word64_assn› unfolding stats_pure_lits_rounds_def stats_code_unfold by sepref sepref_def stats_pure_lits_removed_impl is ‹RETURN o stats_pure_lits_removed› :: ‹isasat_stats_assn^k →_a word64_assn› unfolding stats_pure_lits_removed_def stats_code_unfold by sepref sepref_def units_since_beginning_stats_impl is ‹(RETURN o units_since_beginning)› :: ‹isasat_stats_assn^k →_a word_assn› unfolding units_since_beginning_def stats_code_unfold by sepref sepref_def incr_irred_clss_stats_impl is ‹RETURN o incr_irred_clss› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_irred_clss_def stats_code_unfold by sepref sepref_def decr_irred_clss_stats_impl is ‹RETURN o decr_irred_clss› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding decr_irred_clss_def stats_code_unfold by sepref sepref_def incr_propagation_stats_impl is ‹RETURN o incr_propagation› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_propagation_def stats_code_unfold by sepref sepref_def incr_propagation_by_stats_impl is ‹uncurry (RETURN oo incr_propagation_by)› :: ‹word64_assn^k *_a isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_propagation_by_def stats_code_unfold by sepref sepref_def set_not_conflict_until_stats_impl is ‹uncurry (RETURN oo set_no_conflict_until)› :: ‹word64_assn^k *_a isasat_stats_assn^d →_a isasat_stats_assn› unfolding set_no_conflict_until_def stats_code_unfold by sepref sepref_def no_conflict_until_stats_impl is ‹RETURN o no_conflict_until› :: ‹isasat_stats_assn^k →_a word64_assn› unfolding no_conflict_until_def stats_code_unfold by sepref sepref_def incr_conflict_stats_impl is ‹RETURN o incr_conflict› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_conflict_def stats_code_unfold by sepref sepref_def incr_decision_stats_impl is ‹RETURN o incr_decision› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_decision_def stats_code_unfold by sepref sepref_def incr_restart_stats_impl is ‹RETURN o incr_restart› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_restart_def stats_code_unfold by sepref sepref_def incr_reduction_stats_impl is ‹RETURN o incr_reduction› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_reduction_def stats_code_unfold by sepref sepref_def incr_uset_stats_impl is ‹RETURN o incr_uset› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_uset_def stats_code_unfold by sepref sepref_def incr_uset_by_stats_impl is ‹uncurry (RETURN oo incr_uset_by)› :: ‹word64_assn^k *_a isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_uset_by_def stats_code_unfold by sepref sepref_def incr_GC_stats_impl is ‹RETURN o incr_GC› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_GC_def stats_code_unfold by sepref sepref_def stats_conflicts_impl is ‹RETURN o stats_conflicts› :: ‹isasat_stats_assn^k →_a word_assn› unfolding stats_conflicts_def stats_code_unfold by sepref sepref_def incr_units_since_last_GC_impl is ‹RETURN o incr_units_since_last_GC› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_units_since_last_GC_def stats_code_unfold by sepref sepref_def incr_units_since_last_GC_by_impl is ‹uncurry (RETURN oo incr_units_since_last_GC_by)› :: ‹word64_assn^k *_a isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_units_since_last_GC_by_def stats_code_unfold by sepref sepref_def incr_purelit_rounds_impl is ‹RETURN o incr_purelit_rounds› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_purelit_rounds_def stats_code_unfold by sepref sepref_def incr_purelit_elim_stats_impl is ‹RETURN o incr_purelit_elim› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_purelit_elim_def stats_code_unfold by sepref sepref_def incr_binary_red_removed_impl is ‹RETURN o incr_binary_red_removed› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_binary_red_removed_def stats_code_unfold by sepref sepref_def incr_binary_unit_derived_impl is ‹RETURN o incr_binary_unit_derived› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_binary_unit_derived_def stats_code_unfold by sepref sepref_def get_reduction_count_impl is ‹RETURN o get_reduction_count› :: ‹isasat_stats_assn^k →_a word_assn› unfolding get_reduction_count_def stats_code_unfold by sepref sepref_def get_restart_count_impl is ‹RETURN o get_restart_count› :: ‹isasat_stats_assn^k →_a word_assn› unfolding get_restart_count_def stats_code_unfold by sepref sepref_def get_irredundant_count_impl is ‹RETURN o irredundant_clss› :: ‹isasat_stats_assn^k →_a word_assn› unfolding irredundant_clss_def stats_code_unfold by sepref sepref_def stats_propagations_impl is ‹RETURN o stats_propagations› :: ‹isasat_stats_assn^k →_a word_assn› unfolding stats_propagations_def stats_code_unfold by sepref sepref_def stats_restarts_impl is ‹RETURN o stats_restarts› :: ‹isasat_stats_assn^k →_a word_assn› unfolding stats_restarts_def stats_code_unfold by sepref sepref_def stats_reductions_impl is ‹RETURN o stats_reductions› :: ‹isasat_stats_assn^k →_a word_assn› unfolding stats_reductions_def stats_code_unfold by sepref sepref_def stats_fixed_impl is ‹RETURN o stats_fixed› :: ‹isasat_stats_assn^k →_a word_assn› unfolding stats_fixed_def stats_code_unfold by sepref sepref_def stats_gcs_impl is ‹RETURN o stats_gcs› :: ‹isasat_stats_assn^k →_a word_assn› unfolding stats_gcs_def stats_code_unfold by sepref sepref_def stats_avg_lbd_mpl is ‹RETURN o stats_avg_lbd› :: ‹isasat_stats_assn^k →_a ema_assn› unfolding stats_avg_lbd_def stats_code_unfold by sepref sepref_register LSize_Stats_lbd LSize_Stats_size LSize_Stats sepref_def stats_lbd_limit_impl is ‹RETURN o stats_lbd_limit› :: ‹isasat_stats_assn^k →_a uint32_nat_assn› unfolding stats_lbd_limit_def stats_code_unfold by sepref sepref_def stats_size_limit_impl is ‹RETURN o stats_size_limit› :: ‹isasat_stats_assn^k →_a sint64_nat_assn› unfolding stats_size_limit_def stats_code_unfold by sepref sepref_def Subsumption_Stats_incr_strengthening_impl is ‹RETURN o Subsumption_Stats_incr_strengthening› :: ‹subsumption_stats_assn^d →_a subsumption_stats_assn› unfolding Subsumption_Stats_incr_strengthening_def subsumption_stats_assn_def by sepref sepref_def incr_forward_strengethening_impl is ‹RETURN o incr_forward_strengethening› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_forward_strengethening_def stats_code_unfold by sepref sepref_def Subsumption_Stats_incr_subsumed_impl is ‹RETURN o Subsumption_Stats_incr_subsumed› :: ‹subsumption_stats_assn^d →_a subsumption_stats_assn› unfolding Subsumption_Stats_incr_subsumed_def subsumption_stats_assn_def by sepref sepref_def Subsumption_Stats_incr_tried_impl is ‹RETURN o Subsumption_Stats_incr_tried› :: ‹subsumption_stats_assn^d →_a subsumption_stats_assn› unfolding Subsumption_Stats_incr_tried_def subsumption_stats_assn_def by sepref sepref_def Subsumption_Stats_incr_rounds_impl is ‹RETURN o Subsumption_Stats_incr_rounds› :: ‹subsumption_stats_assn^d →_a subsumption_stats_assn› unfolding Subsumption_Stats_incr_rounds_def subsumption_stats_assn_def by sepref sepref_def incr_forward_subsumed_impl is ‹RETURN o incr_forward_subsumed› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_forward_subsumed_def stats_code_unfold by sepref sepref_def incr_forward_rounds_impl is ‹RETURN o incr_forward_rounds› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_forward_rounds_def stats_code_unfold by sepref sepref_def incr_forward_tried_impl is ‹RETURN o incr_forward_tried› :: ‹isasat_stats_assn^d →_a isasat_stats_assn› unfolding incr_forward_tried_def stats_code_unfold by sepref sepref_def Subsumption_Stats_rounds_impl is ‹RETURN o Subsumption_Stats_rounds› :: ‹subsumption_stats_assn^k →_a word64_assn› unfolding subsumption_stats_assn_def Subsumption_Stats_rounds_def by sepref sepref_def Subsumption_Stats_strengthened_impl is ‹RETURN o Subsumption_Stats_strengthened› :: ‹subsumption_stats_assn^k →_a word64_assn› unfolding subsumption_stats_assn_def Subsumption_Stats_strengthened_def by sepref sepref_def Subsumption_Stats_subsumed_impl is ‹RETURN o Subsumption_Stats_subsumed› :: ‹subsumption_stats_assn^k →_a word64_assn› unfolding subsumption_stats_assn_def Subsumption_Stats_subsumed_def by sepref sepref_def Subsumption_Stats_tried_impl is ‹RETURN o Subsumption_Stats_tried› :: ‹subsumption_stats_assn^k →_a word64_assn› unfolding subsumption_stats_assn_def Subsumption_Stats_tried_def by sepref sepref_def stats_forward_rounds_impl is ‹RETURN o stats_forward_rounds› :: ‹isasat_stats_assn^k →_a word64_assn› unfolding stats_forward_rounds_def stats_code_unfold by sepref sepref_def Rephase_Stats_incr_total_impl is ‹RETURN o Rephase_Stats_incr_total› :: ‹rephase_stats_assn^d →_a rephase_stats_assn› unfolding rephase_stats_assn_def Rephase_Stats_incr_total_def by sepref sepref_def Rephase_Stats_total_impl is ‹RETURN o Rephase_Stats_total› :: ‹rephase_stats_assn^d →_a word64_assn› unfolding rephase_stats_assn_def Rephase_Stats_total_def by sepref sepref_register stats_forward_tried stats_forward_subsumed stats_forward_strengthened sepref_def stats_forward_subsumed_impl is ‹RETURN o stats_forward_subsumed› :: ‹isasat_stats_assn^d →_a word64_assn› unfolding stats_forward_subsumed_def stats_code_unfold by sepref sepref_def stats_forward_tried_impl is ‹RETURN o stats_forward_tried› :: ‹isasat_stats_assn^d →_a word64_assn› unfolding stats_forward_tried_def stats_code_unfold by sepref sepref_def stats_forward_strengthened_impl is ‹RETURN o stats_forward_strengthened› :: ‹isasat_stats_assn^d →_a word64_assn› unfolding stats_forward_strengthened_def stats_code_unfold by sepref lemmas [llvm_inline] = Mreturn_comp_Tuple16 sepref_register empty_stats sepref_def empty_stats_impl is ‹uncurry0 (RETURN empty_stats)› :: ‹unit_assn^k →_a isasat_stats_assn› unfolding empty_stats_def empty_search_stats_def[symmetric] apply (subst empty_rephase_stats_def[symmetric]) unfolding empty_subsumption_stats_def[symmetric] unfolding empty_binary_stats_def[symmetric] apply (subst empty_pure_lits_stats_def[symmetric]) apply (subst empty_lsize_limit_stats_def[symmetric]) by sepref definition empty_search_stats_clss where ‹empty_search_stats_clss n = (0,0,0,0,0,0,0,0,n,0)› sepref_def empty_search_stats_clss_impl is ‹(RETURN o empty_search_stats_clss)› :: ‹word64_assn^k →_a search_stats_assn› unfolding search_stats_assn_def empty_search_stats_clss_def by sepref sepref_def empty_stats_clss_impl is ‹(RETURN o empty_stats_clss)› :: ‹word64_assn^k →_a isasat_stats_assn› unfolding empty_stats_clss_def empty_search_stats_clss_def[symmetric] apply (subst empty_rephase_stats_def[symmetric]) unfolding empty_subsumption_stats_def[symmetric] unfolding empty_binary_stats_def[symmetric] apply (subst empty_pure_lits_stats_def[symmetric]) apply (subst empty_lsize_limit_stats_def[symmetric]) by sepref sepref_register Rephase_Stats_incr_total Rephase_Stats_total stats_rephase incr_rephase_total sepref_def stats_rephase_impl is ‹RETURN o stats_rephase› :: ‹isasat_stats_assn^k →_a word64_assn› unfolding stats_rephase_def stats_code_unfold by sepref sepref_def incr_rephase_total_impl is ‹RETURN o incr_rephase_total› :: ‹isasat_stats_assn^k →_a isasat_stats_assn› unfolding incr_rephase_total_def stats_code_unfold by sepref export_llvm empty_stats_impl sepref_register unset_fully_propagated_heur is_fully_propagated_heur set_fully_propagated_heur abbreviation (input) ‹restart_info_rel ≡ word64_rel ×_r word64_rel ×_r word64_rel ×_r word64_rel ×_r word64_rel› abbreviation (input) restart_info_assn where ‹restart_info_assn ≡ word64_assn ×_a word64_assn ×_a word64_assn ×_a word64_assn ×_a word64_assn› lemma restart_info_params[sepref_import_param]: "(incr_conflict_count_since_last_restart,incr_conflict_count_since_last_restart) ∈ restart_info_rel → restart_info_rel" "(restart_info_update_lvl_avg,restart_info_update_lvl_avg) ∈ word32_rel → restart_info_rel → restart_info_rel" ‹(restart_info_init,restart_info_init) ∈ restart_info_rel› ‹(restart_info_restart_done,restart_info_restart_done) ∈ restart_info_rel → restart_info_rel› by auto lemmas [llvm_inline] = incr_conflict_count_since_last_restart_def restart_info_update_lvl_avg_def restart_info_init_def restart_info_restart_done_def abbreviation (input) ‹schedule_info_rel ≡ word64_rel ×_r word64_rel ×_r word64_rel› abbreviation (input) schedule_info_assn where ‹schedule_info_assn ≡ word64_assn ×_a word64_assn ×_a word64_assn› lemma schedule_info_params[sepref_import_param]: "(next_pure_lits_schedule_info, next_pure_lits_schedule_info) ∈ schedule_info_rel → word64_rel" "(schedule_next_pure_lits_info, schedule_next_pure_lits_info) ∈ schedule_info_rel → schedule_info_rel" "(next_reduce_schedule_info, next_reduce_schedule_info) ∈ schedule_info_rel → word64_rel" "(schedule_next_reduce_info, schedule_next_reduce_info) ∈ word64_rel → schedule_info_rel → schedule_info_rel" by (auto) sepref_register FOCUSED_MODE STABLE_MODE DEFAULT_INIT_PHASE sepref_def FOCUSED_MODE_impl is ‹uncurry0 (RETURN FOCUSED_MODE)› :: ‹unit_assn^k →_a word_assn› unfolding FOCUSED_MODE_def by sepref sepref_def STABLE_MODE_impl is ‹uncurry0 (RETURN STABLE_MODE)› :: ‹unit_assn^k →_a word_assn› unfolding STABLE_MODE_def by sepref definition lcount_assn :: ‹clss_size ⇒ _ ⇒ assn› where ‹lcount_assn ≡ uint64_nat_assn ×_a uint64_nat_assn ×_a uint64_nat_assn ×_a uint64_nat_assn ×_a uint64_nat_assn› lemma [safe_constraint_rules]: ‹CONSTRAINT Sepref_Basic.is_pure lcount_assn› unfolding lcount_assn_def by auto sepref_def clss_size_lcount_fast_code is ‹RETURN o clss_size_lcount› :: ‹lcount_assn^k →_a uint64_nat_assn› unfolding clss_size_lcount_def lcount_assn_def by sepref sepref_register clss_size_resetUS lemma clss_size_resetUS_alt_def: ‹RETURN o clss_size_resetUS = (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). RETURN (lcount, lcountUE, lcountUEk, 0, lcountU0))› by (auto simp: clss_size_resetUS_def) sepref_def clss_size_resetUS_fast_code is ‹RETURN o clss_size_resetUS› :: ‹lcount_assn^d →_a lcount_assn› unfolding clss_size_resetUS_alt_def lcount_assn_def apply (annot_unat_const ‹TYPE(64)›) by sepref lemma clss_size_incr_lcountUS_alt_def: ‹RETURN o clss_size_incr_lcountUS = (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). RETURN (lcount, lcountUE, lcountUEk, lcountUS + 1, lcountU0))› by (auto simp: clss_size_incr_lcountUS_def) sepref_def clss_size_incr_lcountUS_fast_code is ‹RETURN o clss_size_incr_lcountUS› :: ‹[λS. clss_size_lcountUS S < unat64_max]_a lcount_assn^d → lcount_assn› unfolding clss_size_incr_lcountUS_alt_def lcount_assn_def clss_size_lcountUS_def apply (annot_unat_const ‹TYPE(64)›) by sepref lemma clss_size_resetU0_alt_def: ‹RETURN o clss_size_resetU0 = (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). RETURN (lcount, lcountUE, lcountUEk, lcountUS, 0))› by (auto simp: clss_size_resetU0_def) sepref_def clss_size_resetU0_fast_code is ‹RETURN o clss_size_resetU0› :: ‹lcount_assn^d →_a lcount_assn› unfolding clss_size_resetU0_alt_def lcount_assn_def apply (annot_unat_const ‹TYPE(64)›) by sepref lemma clss_size_incr_lcountU0_alt_def: ‹RETURN o clss_size_incr_lcountU0 = (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). RETURN (lcount, lcountUE, lcountUEk, lcountUS, lcountU0+1))› by (auto simp: clss_size_incr_lcountU0_def) sepref_def clss_size_incr_lcountU0_fast_code is ‹RETURN o clss_size_incr_lcountU0› :: ‹[λS. clss_size_lcountU0 S < unat64_max]_a lcount_assn^d → lcount_assn› unfolding clss_size_incr_lcountU0_alt_def lcount_assn_def clss_size_lcountU0_def apply (annot_unat_const ‹TYPE(64)›) by sepref lemma clss_size_resetUE_alt_def: ‹RETURN o clss_size_resetUE = (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). RETURN (lcount, 0, lcountUEk, lcountUS, lcountU0))› by (auto simp: clss_size_resetUE_def) sepref_def clss_size_resetUE_fast_code is ‹RETURN o clss_size_resetUE› :: ‹lcount_assn^d →_a lcount_assn› unfolding clss_size_resetUE_alt_def lcount_assn_def apply (annot_unat_const ‹TYPE(64)›) by sepref lemma clss_size_incr_lcountUE_alt_def: ‹RETURN o clss_size_incr_lcountUE = (λ(lcount, lcountUE, lcountUS). RETURN (lcount, lcountUE + 1, lcountUS))› by (auto simp: clss_size_incr_lcountUE_def) sepref_def clss_size_incr_lcountUE_fast_code is ‹RETURN o clss_size_incr_lcountUE› :: ‹[λS. clss_size_lcountUE S < unat64_max]_a lcount_assn^d → lcount_assn› unfolding clss_size_incr_lcountUE_alt_def lcount_assn_def clss_size_lcountUE_def apply (annot_unat_const ‹TYPE(64)›) by sepref lemma clss_size_incr_lcountUEk_alt_def: ‹RETURN o clss_size_incr_lcountUEk = (λ(lcount, lcountUE, lcountUEk, lcountUS). RETURN (lcount, lcountUE, lcountUEk + 1, lcountUS))› by (auto simp: clss_size_incr_lcountUEk_def) sepref_def clss_size_incr_lcountUEk_fast_code is ‹RETURN o clss_size_incr_lcountUEk› :: ‹[λS. clss_size_lcountUEk S < unat64_max]_a lcount_assn^d → lcount_assn› unfolding clss_size_incr_lcountUEk_alt_def lcount_assn_def clss_size_lcountUEk_def apply (annot_unat_const ‹TYPE(64)›) by sepref schematic_goal mk_free_lookup_clause_rel_assn[sepref_frame_free_rules]: ‹MK_FREE lcount_assn ?fr› unfolding lcount_assn_def by (rule free_thms sepref_frame_free_rules)+ (* TODO: Write a method for that! *) lemma clss_size_lcountUE_alt_def: ‹RETURN o clss_size_lcountUE = (λ(lcount, lcountUE, lcountUS). RETURN lcountUE)› by (auto simp: clss_size_lcountUE_def) sepref_def clss_size_lcountUE_fast_code is ‹RETURN o clss_size_lcountUE› :: ‹lcount_assn^k →_a uint64_nat_assn› unfolding lcount_assn_def clss_size_lcountUE_alt_def clss_size_lcount_def by sepref lemma clss_size_lcountUS_alt_def: ‹RETURN o clss_size_lcountUS = (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). RETURN lcountUS)› by (auto simp: clss_size_lcountUS_def) sepref_def clss_size_lcountUSt_fast_code is ‹RETURN o clss_size_lcountUS› :: ‹lcount_assn^k →_a uint64_nat_assn› unfolding lcount_assn_def clss_size_lcountUS_alt_def clss_size_lcount_def by sepref lemma clss_size_lcountU0_alt_def: ‹RETURN o clss_size_lcountU0 = (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). RETURN lcountU0)› by (auto simp: clss_size_lcountU0_def) sepref_def clss_size_lcountU0_fast_code is ‹RETURN o clss_size_lcountU0› :: ‹lcount_assn^k →_a uint64_nat_assn› unfolding lcount_assn_def clss_size_lcountU0_alt_def clss_size_lcount_def by sepref lemma clss_size_incr_allcount_alt_def: ‹RETURN o clss_size_allcount = (λ(lcount, lcountUE, lcountUEk, lcountUS, lcountU0). RETURN (lcount + lcountUE + lcountUEk + lcountUS + lcountU0))› by (auto simp: clss_size_allcount_def) sepref_def clss_size_allcount_fast_code is ‹RETURN o clss_size_allcount› :: ‹[λS. clss_size_allcount S < max_snat 64]_a lcount_assn^d → uint64_nat_assn› unfolding clss_size_incr_allcount_alt_def lcount_assn_def clss_size_allcount_def by sepref lemma clss_size_decr_lcount_alt_def: ‹RETURN o clss_size_decr_lcount = (λ(lcount, lcountUE, lcountUS). RETURN (lcount - 1, lcountUE, lcountUS))› by (auto simp: clss_size_decr_lcount_def) sepref_def clss_size_decr_lcount_fast_code is ‹RETURN o clss_size_decr_lcount› :: ‹[λS. clss_size_lcount S ≥ 1]_a lcount_assn^d → lcount_assn› unfolding lcount_assn_def clss_size_decr_lcount_alt_def clss_size_lcount_def apply (annot_unat_const ‹TYPE(64)›) by sepref lemma emag_get_value_alt_def: ‹ema_get_value = (λ(a, b, c, d). a)› by auto sepref_def ema_get_value_impl is ‹RETURN o ema_get_value› :: ‹ema_assn^k →_a word_assn› unfolding emag_get_value_alt_def by sepref lemma emag_extract_value_alt_def: ‹ema_extract_value = (λ(a, b, c, d). a >> EMA_FIXPOINT_SIZE)› by auto sepref_def ema_extract_value_impl is ‹RETURN o ema_extract_value› :: ‹ema_assn^k →_a word_assn› unfolding emag_extract_value_alt_def EMA_FIXPOINT_SIZE_def apply (annot_snat_const ‹TYPE(64)›) by sepref sepref_def schedule_next_pure_lits_info_impl is ‹RETURN o schedule_next_pure_lits_info› :: ‹schedule_info_assn^k →_a schedule_info_assn› unfolding schedule_next_pure_lits_info_def apply (annot_snat_const ‹TYPE(64)›) by sepref sepref_def next_pure_lits_schedule_info_impl is ‹RETURN o next_pure_lits_schedule_info› :: ‹schedule_info_assn^k →_a word64_assn› unfolding next_pure_lits_schedule_info_def by sepref sepref_def schedule_next_reduce_info_impl is ‹uncurry (RETURN oo schedule_next_reduce_info)› :: ‹word64_assn^k *_a schedule_info_assn^k →_a schedule_info_assn› unfolding schedule_next_reduce_info_def by sepref sepref_def next_reduce_schedule_info_impl is ‹RETURN o next_reduce_schedule_info› :: ‹schedule_info_assn^k →_a word64_assn› unfolding next_reduce_schedule_info_def by sepref sepref_def schedule_next_subsume_info_impl is ‹uncurry (RETURN oo schedule_next_subsume_info)› :: ‹word64_assn^k *_a schedule_info_assn^k →_a schedule_info_assn› unfolding schedule_next_subsume_info_def by sepref sepref_def next_subsume_schedule_info_impl is ‹RETURN o next_subsume_schedule_info› :: ‹schedule_info_assn^k →_a word64_assn› unfolding next_subsume_schedule_info_def by sepref type_synonym heur_assn = ‹(ema × ema × restart_info × 64 word × (phase_saver_assn × 64 word × phase_saver'_assn × 64 word × phase_saver'_assn × 64 word × 64 word × 64 word) × reluctant_rel_assn × 1 word × phase_saver_assn × (64 word × 64 word × 64 word) × ema × ema)› definition heuristic_int_assn :: ‹restart_heuristics ⇒ heur_assn ⇒ assn› where ‹heuristic_int_assn = ema_assn ×_a ema_assn ×_a restart_info_assn ×_a word64_assn ×_a phase_heur_assn ×_a reluctant_assn ×_a bool1_assn ×_a phase_saver_assn ×_a schedule_info_assn ×_a ema_assn ×_a ema_assn› abbreviation heur_int_rel :: ‹(restart_heuristics × restart_heuristics) set› where ‹heur_int_rel ≡ Id› abbreviation heur_rel :: ‹(restart_heuristics × isasat_restart_heuristics) set› where ‹heur_rel ≡ ⟨heur_int_rel⟩code_hider_rel› definition heuristic_assn :: ‹isasat_restart_heuristics ⇒ _ ⇒ assn› where ‹heuristic_assn = code_hider_assn heuristic_int_assn heur_int_rel› lemma heuristic_assn_alt_def: ‹heuristic_assn = hr_comp heuristic_int_assn heur_rel› unfolding heuristic_assn_def code_hider_assn_def by auto context notes [fcomp_norm_unfold] = heuristic_assn_def[symmetric] heuristic_assn_alt_def[symmetric] begin lemma set_zero_wasted_stats_set_zero_wasted_stats: ‹(set_zero_wasted_stats, set_zero_wasted) ∈ heur_rel → heur_rel› and heuristic_reluctant_tick_stats_heuristic_reluctant_tick: ‹(heuristic_reluctant_tick_stats, heuristic_reluctant_tick) ∈ heur_rel → heur_rel› and heuristic_reluctant_enable_stats_heuristic_reluctant_enable: ‹(heuristic_reluctant_enable_stats,heuristic_reluctant_enable) ∈ heur_rel → heur_rel› and heuristic_reluctant_disable_stats_heuristic_reluctant_disable: ‹(heuristic_reluctant_disable_stats,heuristic_reluctant_disable) ∈ heur_rel → heur_rel› and heuristic_reluctant_triggered_stats_heuristic_reluctant_triggered: ‹(heuristic_reluctant_triggered_stats,heuristic_reluctant_triggered) ∈ heur_rel → heur_rel ×_f bool_rel› and heuristic_reluctant_triggered2_stats_heuristic_reluctant_triggered2: ‹(heuristic_reluctant_triggered2_stats,heuristic_reluctant_triggered2) ∈ heur_rel → bool_rel› and heuristic_reluctant_untrigger_stats_heuristic_reluctant_untrigger: ‹(heuristic_reluctant_untrigger_stats, heuristic_reluctant_untrigger) ∈ heur_rel → heur_rel› and end_of_rephasing_phase_heur_stats_end_of_rephasing_phase_heur: ‹(end_of_rephasing_phase_heur_stats, end_of_rephasing_phase_heur) ∈ heur_rel → word64_rel› and is_fully_propagated_heur_stats_is_fully_propagated_heur: ‹(is_fully_propagated_heur_stats, is_fully_propagated_heur) ∈ heur_rel → bool_rel› and set_fully_propagated_heur_stats_set_fully_propagated_heur: ‹(set_fully_propagated_heur_stats, set_fully_propagated_heur) ∈ heur_rel → heur_rel›and unset_fully_propagated_heur_stats_unset_fully_propagated_heur: ‹(unset_fully_propagated_heur_stats, unset_fully_propagated_heur) ∈ heur_rel → heur_rel› and restart_info_restart_done_heur_stats_restart_info_restart_done_heur: ‹(restart_info_restart_done_heur_stats, restart_info_restart_done_heur) ∈ heur_rel → heur_rel› and set_zero_wasted_stats_set_zero_wasted: ‹(set_zero_wasted_stats, set_zero_wasted) ∈ heur_rel → heur_rel› and wasted_of_stats_wasted_of: ‹(wasted_of_stats, wasted_of) ∈ heur_rel → word64_rel› and slow_ema_of_stats_slow_ema_of: ‹(slow_ema_of_stats, slow_ema_of) ∈ heur_rel → ema_rel› and fast_ema_of_stats_fast_ema_of: ‹(fast_ema_of_stats, fast_ema_of) ∈ heur_rel → ema_rel› and current_restart_phase_stats_current_restart_phase: ‹(current_restart_phase_stats, current_restart_phase) ∈ heur_rel → word_rel› and incr_wasted_stats_incr_wasted: ‹(incr_wasted_stats, incr_wasted) ∈ word_rel → heur_rel → heur_rel› and current_rephasing_phase_stats_current_rephasing_phase: ‹(current_rephasing_phase_stats, current_rephasing_phase) ∈ heur_rel → word_rel› and get_next_phase_heur_stats_get_next_phase_heur: ‹(uncurry2 (get_next_phase_heur_stats), uncurry2 (get_next_phase_heur)) ∈ Id ×_f Id ×_f heur_rel →_f ⟨bool_rel⟩nres_rel› and get_conflict_count_since_last_restart_stats_get_conflict_count_since_last_restart_stats: ‹(get_conflict_count_since_last_restart_stats, get_conflict_count_since_last_restart) ∈ heur_rel → word_rel› and schedule_next_pure_lits_stats_schedule_next_pure_lits: ‹(schedule_next_pure_lits_stats, schedule_next_pure_lits) ∈ heur_rel → heur_rel› and next_pure_lits_schedule_next_pure_lits_schedule_stats: ‹(next_pure_lits_schedule_info_stats, next_pure_lits_schedule) ∈ heur_rel → word64_rel› and schedule_next_reduce_stats_schedule_next_reduce: ‹(schedule_next_reduce_stats, schedule_next_reduce) ∈ word64_rel → heur_rel → heur_rel› and next_reduce_schedule_next_reduce_schedule_stats: ‹(next_reduce_schedule_info_stats, next_reduce_schedule) ∈ heur_rel → word64_rel› and schedule_next_subsume_stats_schedule_next_subsume: ‹(schedule_next_subsume_stats, schedule_next_subsume) ∈ word64_rel → heur_rel → heur_rel› and next_subsume_schedule_next_subsume_schedule_stats: ‹(next_subsume_schedule_info_stats, next_subsume_schedule) ∈ heur_rel → word64_rel› and swap_emas_stats_swap_emas: ‹(swap_emas_stats, swap_emas) ∈ heur_rel → heur_rel› by (auto simp: set_zero_wasted_def code_hider_rel_def heuristic_reluctant_tick_def heuristic_reluctant_enable_def heuristic_reluctant_triggered_def apfst_def map_prod_def heuristic_reluctant_disable_def heuristic_reluctant_triggered2_def is_fully_propagated_heur_def end_of_rephasing_phase_heur_def unset_fully_propagated_heur_def restart_info_restart_done_heur_def heuristic_reluctant_untrigger_def set_fully_propagated_heur_def wasted_of_def get_next_phase_heur_def slow_ema_of_def fast_ema_of_def current_restart_phase_def incr_wasted_def current_rephasing_phase_def get_conflict_count_since_last_restart_def next_pure_lits_schedule_def schedule_next_pure_lits_def schedule_next_pure_lits_stats_def next_reduce_schedule_def schedule_next_reduce_def schedule_next_reduce_stats_def next_subsume_schedule_def schedule_next_subsume_def schedule_next_subsume_stats_def swap_emas_def intro!: frefI nres_relI split: prod.splits) (*heuristic_reluctant_triggered*) lemma set_zero_wasted_stats_alt_def: ‹set_zero_wasted_stats= (λ(fast_ema, slow_ema, res_info, wasted, φ). (fast_ema, slow_ema, res_info, 0, φ))› by auto sepref_def set_zero_wasted_stats_impl is ‹RETURN o set_zero_wasted_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def set_zero_wasted_stats_alt_def by sepref sepref_def heuristic_reluctant_tick_stats_impl is ‹RETURN o heuristic_reluctant_tick_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def heuristic_reluctant_tick_stats_def by sepref sepref_def heuristic_reluctant_enable_stats_impl is ‹RETURN o heuristic_reluctant_enable_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def heuristic_reluctant_enable_stats_def by sepref sepref_def heuristic_reluctant_disable_stats_impl is ‹RETURN o heuristic_reluctant_disable_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def heuristic_reluctant_disable_stats_def by sepref sepref_def heuristic_reluctant_triggered_stats_impl is ‹RETURN o heuristic_reluctant_triggered_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn ×_a bool1_assn› unfolding heuristic_reluctant_triggered_stats_def heuristic_int_assn_def by sepref sepref_def heuristic_reluctant_triggered2_stats_impl is ‹RETURN o heuristic_reluctant_triggered2_stats› :: ‹heuristic_int_assn^k →_a bool1_assn› unfolding heuristic_reluctant_triggered2_stats_def heuristic_int_assn_def by sepref sepref_def heuristic_reluctant_untrigger_stats_impl is ‹RETURN o heuristic_reluctant_untrigger_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def heuristic_reluctant_untrigger_stats_def by sepref sepref_def end_of_rephasing_phase_impl [llvm_inline] is ‹RETURN o end_of_rephasing_phase› :: ‹phase_heur_assn^k →_a word64_assn› unfolding end_of_rephasing_phase_def phase_heur_assn_def by sepref sepref_def end_of_rephasing_phase_heur_stats_impl is ‹RETURN o end_of_rephasing_phase_heur_stats› :: ‹heuristic_int_assn^k →_a word64_assn› unfolding heuristic_int_assn_def end_of_rephasing_phase_heur_stats_def by sepref sepref_def is_fully_propagated_heur_stats_impl is ‹RETURN o is_fully_propagated_heur_stats› :: ‹heuristic_int_assn^k →_a bool1_assn› unfolding heuristic_int_assn_def is_fully_propagated_heur_stats_def by sepref sepref_def set_fully_propagated_heur_stats_impl is ‹RETURN o set_fully_propagated_heur_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def set_fully_propagated_heur_stats_def by sepref sepref_def unset_fully_propagated_heur_stats_impl is ‹RETURN o unset_fully_propagated_heur_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def unset_fully_propagated_heur_stats_def by sepref sepref_def restart_info_restart_done_heur_stats_impl is ‹RETURN o restart_info_restart_done_heur_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def restart_info_restart_done_heur_stats_def by sepref sepref_def set_zero_wasted_impl is ‹RETURN o set_zero_wasted_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def set_zero_wasted_stats_alt_def by sepref lemma wasted_of_stats_alt_def: ‹RETURN o wasted_of_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ). RETURN wasted)› by auto sepref_def wasted_of_stats_impl is ‹RETURN o wasted_of_stats› :: ‹heuristic_int_assn^k →_a word64_assn› unfolding heuristic_int_assn_def wasted_of_stats_alt_def by sepref lemma slow_ema_of_stats_alt_def: ‹RETURN o slow_ema_of_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ). RETURN slow_ema)› and fast_ema_of_stats_alt_def: ‹RETURN o fast_ema_of_stats = (λ(fast_ema, slow_ema, res_info, wasted, φ). RETURN fast_ema)› by auto sepref_def slow_ema_of_stats_impl is ‹RETURN o slow_ema_of_stats› :: ‹heuristic_int_assn^k →_a ema_assn› unfolding heuristic_int_assn_def slow_ema_of_stats_alt_def by sepref sepref_def fast_ema_of_stats_impl is ‹RETURN o fast_ema_of_stats› :: ‹heuristic_int_assn^k →_a ema_assn› unfolding heuristic_int_assn_def fast_ema_of_stats_alt_def by sepref lemma current_restart_phase_stats_alt_def: ‹RETURN o current_restart_phase_stats = (λ(fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase), wasted, φ). RETURN restart_phase)› by auto sepref_def current_restart_phase_impl is ‹RETURN o current_restart_phase_stats› :: ‹heuristic_int_assn^k →_a word_assn› unfolding heuristic_int_assn_def current_restart_phase_stats_alt_def by sepref lemma incr_wasted_stats_stats_alt_def: ‹RETURN oo incr_wasted_stats = (λwaste (fast_ema, slow_ema, res_info, wasted, φ). RETURN (fast_ema, slow_ema, res_info, wasted + waste, φ))› by (auto intro!: ext) sepref_def incr_wasted_stats_impl is ‹uncurry (RETURN oo incr_wasted_stats)› :: ‹word64_assn^k *_a heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def incr_wasted_stats_stats_alt_def by sepref sepref_def swap_emas_stats_impl is ‹RETURN o swap_emas_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def swap_emas_stats_def by sepref sepref_def current_rephasing_phase_stats_impl is ‹RETURN o current_rephasing_phase_stats› :: ‹heuristic_int_assn^k →_a word_assn› unfolding heuristic_int_assn_def current_rephasing_phase_stats_def phase_current_rephasing_phase_def phase_heur_assn_def by sepref sepref_def get_next_phase_heur_stats_impl is ‹uncurry2 get_next_phase_heur_stats› :: ‹bool1_assn^k *_a atom_assn^k *_a heuristic_int_assn^k →_a bool1_assn› unfolding get_next_phase_heur_stats_def heuristic_int_assn_def by sepref lemma get_conflict_count_since_last_restart_stats_alt_def: ‹get_conflict_count_since_last_restart_stats = (λ(fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase), wasted, φ). ccount)› by auto sepref_def get_conflict_count_since_last_restart_stats_impl is ‹RETURN o get_conflict_count_since_last_restart_stats› :: ‹heuristic_int_assn^k →_a word64_assn› unfolding get_conflict_count_since_last_restart_stats_alt_def heuristic_int_assn_def by sepref lemma next_pure_lits_schedule_info_stats_alt_def: ‹next_pure_lits_schedule_info_stats = (λ(fast_ema, slow_ema, _, wasted, φ, _,_,lits, (inprocess_schedule, _), other_fema, other_sema). inprocess_schedule)› unfolding next_pure_lits_schedule_info_stats_def next_pure_lits_schedule_info_def by auto sepref_def next_pure_lits_schedule_info_stats_impl is ‹RETURN o next_pure_lits_schedule_info_stats› :: ‹heuristic_int_assn^k →_a word64_assn› unfolding next_pure_lits_schedule_info_stats_alt_def heuristic_int_assn_def by sepref sepref_def schedule_next_pure_lits_stats_impl is ‹RETURN o schedule_next_pure_lits_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding schedule_next_pure_lits_stats_def heuristic_int_assn_def by sepref lemma next_reduce_schedule_info_stats_alt_def: ‹next_reduce_schedule_info_stats = (λ(fast_ema, slow_ema, _, wasted, φ, _,_,lits, (inprocess_schedule, reduce_schedule, _), _). reduce_schedule)› unfolding next_reduce_schedule_info_stats_def next_reduce_schedule_info_def by (auto intro!: ext) sepref_def next_reduce_schedule_info_stats_impl is ‹RETURN o next_reduce_schedule_info_stats› :: ‹heuristic_int_assn^k →_a word64_assn› unfolding next_reduce_schedule_info_stats_alt_def heuristic_int_assn_def by sepref sepref_def schedule_next_reduce_stats_impl is ‹uncurry (RETURN oo schedule_next_reduce_stats)› :: ‹word64_assn^k *_a heuristic_int_assn^d →_a heuristic_int_assn› unfolding schedule_next_reduce_stats_def heuristic_int_assn_def by sepref lemma next_subsume_schedule_info_stats_alt_def: ‹next_subsume_schedule_info_stats = (λ(fast_ema, slow_ema, _, wasted, φ, _,_,lits, (inprocess_schedule, reduce_schedule, subsume_schedule), _). subsume_schedule)› unfolding next_subsume_schedule_info_stats_def next_subsume_schedule_info_def by (auto intro!: ext) sepref_def next_subsume_schedule_info_stats_impl is ‹RETURN o next_subsume_schedule_info_stats› :: ‹heuristic_int_assn^k →_a word64_assn› unfolding next_subsume_schedule_info_stats_alt_def heuristic_int_assn_def by sepref sepref_def schedule_next_subsume_stats_impl is ‹uncurry (RETURN oo schedule_next_subsume_stats)› :: ‹word64_assn^k *_a heuristic_int_assn^d →_a heuristic_int_assn› unfolding schedule_next_subsume_stats_def heuristic_int_assn_def by sepref lemma hn_id_pure: ‹CONSTRAINT is_pure A ⟹ (Mreturn, RETURN o id) ∈ A^k →_a A› apply sepref_to_hoare apply vcg apply (auto simp: ENTAILS_def is_pure_conv pure_def) by (smt (z3) entails_def entails_lift_extract_simps(1) pure_true_conv sep_conj_empty') lemmas heur_refine[sepref_fr_rules] = set_zero_wasted_stats_impl.refine[FCOMP set_zero_wasted_stats_set_zero_wasted_stats] heuristic_reluctant_tick_stats_impl.refine[FCOMP heuristic_reluctant_tick_stats_heuristic_reluctant_tick] heuristic_reluctant_enable_stats_impl.refine[FCOMP heuristic_reluctant_enable_stats_heuristic_reluctant_enable] heuristic_reluctant_disable_stats_impl.refine[FCOMP heuristic_reluctant_disable_stats_heuristic_reluctant_disable] heuristic_reluctant_triggered_stats_impl.refine[FCOMP heuristic_reluctant_triggered_stats_heuristic_reluctant_triggered] heuristic_reluctant_triggered2_stats_impl.refine[FCOMP heuristic_reluctant_triggered2_stats_heuristic_reluctant_triggered2] heuristic_reluctant_untrigger_stats_impl.refine[FCOMP heuristic_reluctant_untrigger_stats_heuristic_reluctant_untrigger] end_of_rephasing_phase_heur_stats_impl.refine[FCOMP end_of_rephasing_phase_heur_stats_end_of_rephasing_phase_heur] is_fully_propagated_heur_stats_impl.refine[FCOMP is_fully_propagated_heur_stats_is_fully_propagated_heur] set_fully_propagated_heur_stats_impl.refine[FCOMP set_fully_propagated_heur_stats_set_fully_propagated_heur] unset_fully_propagated_heur_stats_impl.refine[FCOMP unset_fully_propagated_heur_stats_unset_fully_propagated_heur] restart_info_restart_done_heur_stats_impl.refine[FCOMP restart_info_restart_done_heur_stats_restart_info_restart_done_heur] set_zero_wasted_impl.refine[FCOMP set_zero_wasted_stats_set_zero_wasted] wasted_of_stats_impl.refine[FCOMP wasted_of_stats_wasted_of] current_restart_phase_impl.refine[FCOMP current_restart_phase_stats_current_restart_phase] slow_ema_of_stats_impl.refine[FCOMP slow_ema_of_stats_slow_ema_of] fast_ema_of_stats_impl.refine[FCOMP fast_ema_of_stats_fast_ema_of] incr_wasted_stats_impl.refine[FCOMP incr_wasted_stats_incr_wasted] swap_emas_stats_impl.refine[FCOMP swap_emas_stats_swap_emas] current_rephasing_phase_stats_impl.refine[FCOMP current_rephasing_phase_stats_current_rephasing_phase] get_next_phase_heur_stats_impl.refine[FCOMP get_next_phase_heur_stats_get_next_phase_heur] get_conflict_count_since_last_restart_stats_impl.refine[FCOMP get_conflict_count_since_last_restart_stats_get_conflict_count_since_last_restart_stats] schedule_next_pure_lits_stats_impl.refine[FCOMP schedule_next_pure_lits_stats_schedule_next_pure_lits] next_pure_lits_schedule_info_stats_impl.refine[FCOMP next_pure_lits_schedule_next_pure_lits_schedule_stats] schedule_next_reduce_stats_impl.refine[FCOMP schedule_next_reduce_stats_schedule_next_reduce] next_reduce_schedule_info_stats_impl.refine[FCOMP next_reduce_schedule_next_reduce_schedule_stats] schedule_next_subsume_stats_impl.refine[FCOMP schedule_next_subsume_stats_schedule_next_subsume] next_subsume_schedule_info_stats_impl.refine[FCOMP next_subsume_schedule_next_subsume_schedule_stats] hn_id[of heuristic_int_assn, FCOMP get_content_hnr[of heur_int_rel]] hn_id[of heuristic_int_assn, FCOMP Constructor_hnr[of heur_int_rel]] lemmas get_restart_heuristics_pure_rule = hn_id_pure[of heuristic_int_assn, FCOMP get_content_hnr[of heur_int_rel]] end sepref_register set_zero_wasted_stats save_phase_heur_stats heuristic_reluctant_tick_stats heuristic_reluctant_tick is_fully_propagated_heur_stats get_content next_pure_lits_schedule_info_stats schedule_next_pure_lits_stats lemma mop_save_phase_heur_stats_alt_def: ‹mop_save_phase_heur_stats = (λ L b (fast_ema, slow_ema, res_info, wasted, (φ, target, best), rel). do { ASSERT(L < length φ); RETURN (fast_ema, slow_ema, res_info, wasted, (φ[L := b], target, best), rel)})› unfolding mop_save_phase_heur_stats_def save_phase_heur_def save_phase_heur_pre_stats_def save_phase_heur_stats_def by (auto intro!: ext) sepref_def mop_save_phase_heur_stats_impl is ‹uncurry2 (mop_save_phase_heur_stats)› :: ‹atom_assn^k *_a bool1_assn^k *_a heuristic_int_assn^d →_a heuristic_int_assn› supply [[goals_limit=1]] unfolding mop_save_phase_heur_stats_alt_def save_phase_heur_stats_def save_phase_heur_pre_stats_def phase_heur_assn_def mop_save_phase_heur_def heuristic_int_assn_def apply annot_all_atm_idxs by sepref lemma mop_save_phase_heur_alt_def: ‹mop_save_phase_heur L b S = do { let S = get_restart_heuristics S; S ← mop_save_phase_heur_stats L b S; RETURN (Restart_Heuristics S) }› unfolding Let_def mop_save_phase_heur_def mop_save_phase_heur_def save_phase_heur_def mop_save_phase_heur_stats_def save_phase_heur_pre_def by auto sepref_def mop_save_phase_heur_impl is ‹uncurry2 (mop_save_phase_heur)› :: ‹atom_assn^k *_a bool1_assn^k *_a heuristic_assn^d →_a heuristic_assn› supply [[goals_limit=1]] unfolding mop_save_phase_heur_alt_def save_phase_heur_def save_phase_heur_pre_def phase_heur_assn_def mop_save_phase_heur_def apply annot_all_atm_idxs by sepref schematic_goal mk_free_heuristic_int_assn[sepref_frame_free_rules]: ‹MK_FREE heuristic_int_assn ?fr› unfolding heuristic_int_assn_def code_hider_assn_def by synthesize_free schematic_goal mk_free_heuristic_assn[sepref_frame_free_rules]: ‹MK_FREE heuristic_assn ?fr› unfolding heuristic_assn_def code_hider_assn_def by synthesize_free lemma [safe_constraint_rules]: ‹CONSTRAINT is_pure A ⟹ CONSTRAINT is_pure (code_hider_assn A B)› unfolding code_hider_assn_def by (auto simp: hr_comp_is_pure) lemma clss_size_incr_lcount_alt_def: ‹RETURN o clss_size_incr_lcount = (λ(lcount, lcountUE, lcountUS). RETURN (lcount + 1, lcountUE, lcountUS))› by (auto simp: clss_size_incr_lcount_def) lemma clss_size_lcountUEk_alt_def: ‹RETURN o clss_size_lcountUEk = (λ(lcount, lcountUE, lcountUEk, lcountUS). RETURN lcountUEk)› by (auto simp: clss_size_lcountUEk_def) sepref_def clss_size_lcountUEk_fast_code is ‹RETURN o clss_size_lcountUEk› :: ‹lcount_assn^k →_a uint64_nat_assn› unfolding lcount_assn_def clss_size_lcountUEk_alt_def clss_size_lcount_def by sepref sepref_register clss_size_incr_lcount sepref_def clss_size_incr_lcount_fast_code is ‹RETURN o clss_size_incr_lcount› :: ‹[λS. clss_size_lcount S ≤ max_snat 64]_a lcount_assn^d → lcount_assn› unfolding clss_size_incr_lcount_alt_def lcount_assn_def clss_size_lcount_def apply (annot_unat_const ‹TYPE(64)›) by sepref sepref_def end_of_restart_phase_impl is ‹RETURN o end_of_restart_phase_stats› :: ‹heuristic_int_assn^k →_a word_assn› unfolding end_of_restart_phase_stats_def heuristic_int_assn_def by sepref lemma end_of_restart_phase_stats_end_of_restart_phase: ‹(end_of_restart_phase_stats, end_of_restart_phase) ∈ heur_rel → word_rel› by (auto simp: end_of_restart_phase_def code_hider_rel_def) lemmas end_of_restart_phase_impl_refine[sepref_fr_rules] = end_of_restart_phase_impl.refine[FCOMP end_of_restart_phase_stats_end_of_restart_phase, unfolded heuristic_assn_alt_def[symmetric]] lemma incr_restart_phase_end_stats_alt_def: ‹incr_restart_phase_end_stats = (λend_of_phase (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, _, length_phase), wasted). (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase + length_phase, (length_phase * 3) >> 1), wasted))› by (auto intro!: ext) sepref_def incr_restart_phase_end_stats_impl [llvm_inline] is ‹uncurry (RETURN oo incr_restart_phase_end_stats)› :: ‹word64_assn^k *_a heuristic_int_assn^d →_a heuristic_int_assn› supply[[goals_limit=1]] unfolding heuristic_int_assn_def incr_restart_phase_end_stats_alt_def apply (annot_snat_const ‹TYPE(64)›) by sepref sepref_def incr_restart_phase_end_impl is ‹uncurry (RETURN oo incr_restart_phase_end)› :: ‹word64_assn^k *_a heuristic_assn^d →_a heuristic_assn› supply[[goals_limit=1]] unfolding incr_restart_phase_end_def by sepref lemma incr_restart_phase_stats_alt_def: ‹incr_restart_phase_stats = (λ(fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase), wasted, φ). (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase XOR 1, end_of_phase), wasted, φ))› by (auto) sepref_def incr_restart_phase_stats_impl is ‹RETURN o incr_restart_phase_stats› :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def incr_restart_phase_stats_alt_def by sepref sepref_def incr_restart_phase_impl is ‹RETURN o incr_restart_phase› :: ‹heuristic_assn^d →_a heuristic_assn› unfolding incr_restart_phase_def by sepref sepref_def reset_added_heur_stats2_impl is reset_added_heur_stats2 :: ‹heuristic_int_assn^d →_a heuristic_int_assn› unfolding reset_added_heur_stats2_def heuristic_int_assn_def apply (annot_snat_const ‹TYPE(64)›) by sepref lemma reset_added_heur_stats2_reset_added_heur_stats: ‹(reset_added_heur_stats2, RETURN o reset_added_heur_stats) ∈ heur_int_rel → ⟨heur_int_rel⟩nres_rel› unfolding fref_param1 apply (intro frefI fref_param1 nres_relI) apply (subst comp_def) apply (rule reset_added_heur_stats2_reset_added_heur_stats[THEN order_trans]) by simp lemmas reset_added_heur_stats_impl_refine[sepref_fr_rules] = reset_added_heur_stats2_impl.refine[FCOMP reset_added_heur_stats2_reset_added_heur_stats] sepref_register reset_added_heur mop_reset_added_heur is_marked_added_heur sepref_def is_marked_added_heur_stats_impl is ‹uncurry (mop_is_marked_added_heur_stats)› :: ‹heuristic_int_assn^k *_a atom_assn^k →_a bool1_assn› supply [[eta_contract=false]] unfolding is_marked_added_heur_stats_def is_marked_added_heur_pre_stats_def heuristic_int_assn_def mop_is_marked_added_heur_stats_def case_prod_app apply (rewrite at ‹_ ! _› annot_index_of_atm) by sepref lemma mop_mark_added_heur_stats_alt_def: ‹mop_mark_added_heur_stats L b =(λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st). do { ASSERT(mark_added_heur_pre_stats L b (fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st)); RETURN (mark_added_heur_stats L b (fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st)) })› by (auto simp: mop_mark_added_heur_stats_def) sepref_def mop_mark_added_heur_stats_impl is ‹uncurry2 mop_mark_added_heur_stats› :: ‹atom_assn^k *_a bool1_assn^k *_a heuristic_int_assn^d →_a heuristic_int_assn› unfolding heuristic_int_assn_def mop_mark_added_heur_stats_alt_def mark_added_heur_stats_def prod.simps mark_added_heur_pre_stats_def apply (rewrite at ‹_[_ := _]› annot_index_of_atm) by sepref lemma mop_is_marked_added_heur_stats_alt_def: ‹mop_is_marked_added_heur_stats =(λ(fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st, schedule) L. do { ASSERT(is_marked_added_heur_pre_stats (fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st, schedule) L); RETURN (is_marked_added_heur_stats (fast_ema, slow_ema, res_info, wasted, φ, reluctant, fully_proped, lits_st, schedule) L) })› by (auto simp: mop_is_marked_added_heur_stats_def intro!: ext) sepref_def mop_is_marked_added_heur_stats_impl is ‹uncurry mop_is_marked_added_heur_stats› :: ‹heuristic_int_assn^k *_a atom_assn^k →_a bool1_assn› unfolding heuristic_int_assn_def mop_is_marked_added_heur_stats_alt_def is_marked_added_heur_stats_def prod.simps is_marked_added_heur_pre_stats_def apply (rewrite at ‹_ ! _› annot_index_of_atm) by sepref context notes [fcomp_norm_unfold] = heuristic_assn_def[symmetric] heuristic_assn_alt_def[symmetric] begin lemma reset_added_heur_stats_reset_added_heur: ‹(reset_added_heur_stats, reset_added_heur) ∈ heur_rel → heur_rel› and is_marked_added_heur_stats_is_marked_added_heur: ‹(is_marked_added_heur_stats, is_marked_added_heur) ∈ heur_rel → nat_rel → bool_rel› by (auto simp: reset_added_heur_def code_hider_rel_def is_marked_added_heur_def mop_is_marked_added_heur_stats_def) lemmas reset_added_heur_refine[sepref_fr_rules] = reset_added_heur_stats_impl_refine[FCOMP reset_added_heur_stats_reset_added_heur] lemma mop_is_marked_added_heur_stats_is_marked_added_heur: ‹(uncurry mop_is_marked_added_heur_stats, uncurry (RETURN oo is_marked_added_heur)) ∈ [λ(S, l). is_marked_added_heur_pre_stats (get_restart_heuristics S) l]_f heur_rel ×_f nat_rel → ⟨bool_rel⟩nres_rel› and mop_mark_added_heur_stats_mop_mark_added_heur: ‹(uncurry2 mop_mark_added_heur_stats, uncurry2 (RETURN ooo mark_added_heur)) ∈ [λ((l,b), S). mark_added_heur_pre l b S]_f nat_rel ×_fbool_rel ×_f heur_rel → ⟨heur_rel⟩nres_rel› and mop_is_marked_added_heur_stats_mop_is_marked_added_heur: ‹(uncurry mop_is_marked_added_heur_stats, uncurry (RETURN oo is_marked_added_heur)) ∈ [λ(l, S). is_marked_added_heur_pre l S]_f heur_rel ×_f nat_rel → ⟨bool_rel⟩nres_rel› by (auto intro!: frefI nres_relI simp: reset_added_heur_def code_hider_rel_def is_marked_added_heur_def mop_mark_added_heur_stats_def mop_is_marked_added_heur_stats_def mop_is_marked_added_heur_stats_def is_marked_added_heur_pre_def mark_added_heur_pre_def mop_mark_added_heur_stats_def mark_added_heur_def) lemmas is_marked_added_heur_stats_impl_refine[refine] = is_marked_added_heur_stats_impl.refine[FCOMP mop_is_marked_added_heur_stats_is_marked_added_heur] lemmas mark_added_heur_impl_refine[refine] = mop_mark_added_heur_stats_impl.refine[FCOMP mop_mark_added_heur_stats_mop_mark_added_heur] lemmas is_marked_added_heur_refine[refine] = mop_is_marked_added_heur_stats_impl.refine[FCOMP mop_is_marked_added_heur_stats_mop_is_marked_added_heur] end sepref_def mop_reset_added_heur_impl is ‹mop_reset_added_heur› :: ‹heuristic_assn^d →_a heuristic_assn› unfolding mop_reset_added_heur_def by sepref end

Theory IsaSAT_Stats_LLVM