Theory Watched_Literals_List

theory Watched_Literals_List_Simp imports Watched_Literals_List_Reduce Watched_Literals_List_Inprocessing begin lemma cdcl_twl_inprocessing_l_count_dec: ‹cdcl_twl_inprocessing_l S T ⟹ count_decided (get_trail_l T) = count_decided (get_trail_l S)› by (induction rule: cdcl_twl_inprocessing_l.induct) (auto simp: cdcl_twl_unitres_l.simps cdcl_twl_unitres_true_l.simps cdcl_twl_subsumed_l.simps cdcl_twl_subresolution_l.simps cdcl_twl_pure_remove_l.simps) lemma rtranclp_cdcl_twl_inprocessing_l_count_dec: ‹cdcl_twl_inprocessing_l^*^* S T ⟹ count_decided (get_trail_l T) = count_decided (get_trail_l S)› by (induction rule: rtranclp_induct) (auto dest!: cdcl_twl_inprocessing_l_count_dec) inductive cdcl_twl_restart_l_inp for S T where ‹cdcl_twl_restart_l S T ⟹ cdcl_twl_restart_l_inp S T› | ‹cdcl_twl_inprocessing_l S T ⟹ cdcl_twl_restart_l_inp S T› lemma cdcl_twl_restart_l_inp_twl_list_invs: ‹cdcl_twl_restart_l_inp S T ⟹ twl_list_invs S ⟹ twl_list_invs T› apply (induction rule: cdcl_twl_restart_l_inp.induct) using cdcl_twl_restart_l_list_invs apply blast using cdcl_twl_inprocessing_l_twl_list_invs by blast lemma rtranclp_cdcl_twl_restart_l_inp_twl_list_invs: ‹cdcl_twl_restart_l_inp^*^* S T ⟹ twl_list_invs S ⟹ twl_list_invs T› by (induction rule: rtranclp_induct) (auto dest: cdcl_twl_restart_l_inp_twl_list_invs) lemma rtranclp_cdcl_twl_restart_l_inp_clauses_to_update_l: ‹cdcl_twl_restart_l_inp^*^* xa V⟹ clauses_to_update_l xa = {#} ⟹ clauses_to_update_l V = {#}› apply (induction rule: rtranclp_induct) subgoal by auto subgoal premises p using p(2) by (auto simp: cdcl_twl_restart_l_inp.simps cdcl_twl_restart_l.simps cdcl_twl_inprocessing_l.simps cdcl_twl_unitres_l.simps cdcl_twl_unitres_true_l.simps cdcl_twl_subsumed_l.simps cdcl_twl_subresolution_l.simps cdcl_twl_pure_remove_l.simps) done lemma rtranclp_cdcl_twl_inprocessing_l_cdcl_twl_l_inp: ‹cdcl_twl_inprocessing_l^*^* S T ⟹ cdcl_twl_restart_l_inp^*^* S T› by (induction rule: rtranclp_induct) (auto dest!: cdcl_twl_restart_l_inp.intros) lemma cdcl_twl_restart_l_inp_cdcl_twl_restart_inp: assumes ‹cdcl_twl_restart_l_inp S U› ‹(S, T) ∈ twl_st_l None› and ‹twl_list_invs S› and ‹twl_struct_invs T› obtains V where ‹(U, V) ∈ twl_st_l None› ‹cdcl_twl_inp T V› using assms apply (induction rule: cdcl_twl_restart_l_inp.induct) subgoal premises p using p apply - apply (drule cdcl_twl_restart_l_invs[OF assms(2,3,4), of U]) apply normalize_goal+ apply (rule p(2)) apply assumption by (auto dest!: cdcl_twl_inp.intros) subgoal apply (cases rule: cdcl_twl_inprocessing_l.cases, assumption) using cdcl_twl_inp.intros(3) cdcl_twl_unitres_l_cdcl_twl_unitres apply blast apply (meson cdcl_twl_inp.simps cdcl_twl_unitres_true_l_cdcl_twl_unitres_true) apply (meson cdcl_twl_inp.intros cdcl_twl_inprocessing_l_twl_st_l0) apply (meson cdcl_twl_inp.simps cdcl_twl_subresolution_l_cdcl_twl_subresolution) using cdcl_twl_inp.intros(6) cdcl_twl_pure_remove_l_cdcl_twl_pure_remove by blast done lemma rtranclp_cdcl_twl_restart_l_inp_cdcl_twl_restart_inp: assumes ‹cdcl_twl_restart_l_inp^*^* S U› ‹(S, T) ∈ twl_st_l None› and ‹twl_list_invs S› and ‹twl_struct_invs T› ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of T)› obtains V where ‹(U, V) ∈ twl_st_l None› and ‹cdcl_twl_inp^*^* T V› proof - have ‹∃V. (U, V) ∈ twl_st_l None ∧ cdcl_twl_inp^*^* T V› using assms(1) apply (induction arbitrary: rule: rtranclp_induct) subgoal by (rule exI[of _ T]) (use assms in auto) subgoal for x y apply normalize_goal+ apply (rule cdcl_twl_restart_l_inp_cdcl_twl_restart_inp[of ], assumption+) apply (smt (verit, ccfv_threshold) assms(3) rtranclp_cdcl_twl_restart_l_inp_twl_list_invs) using assms(4) assms(5) rtranclp_cdcl_twl_inp_invs(1) apply blast by force done then show ?thesis using that by blast qed definition mark_to_delete_clauses_l_post where ‹mark_to_delete_clauses_l_post S T ⟷ (∃S'. (S, S') ∈ twl_st_l None ∧ remove_one_annot_true_clause^*^* S T ∧ twl_list_invs S ∧ twl_struct_invs S' ∧ get_conflict_l S = None ∧ clauses_to_update_l S = {#} ∧ get_unkept_learned_clss_l T = {#} ∧ get_subsumed_learned_clauses_l T = {#} ∧ get_learned_clauses0_l T = {#})› definition cdcl_twl_full_restart_l_prog where ‹cdcl_twl_full_restart_l_prog S = do { ASSERT(mark_to_delete_clauses_l_pre S); T ← mark_to_delete_clauses_l S; ASSERT (mark_to_delete_clauses_l_post S T); RETURN T }› definition mark_duplicated_binary_clauses_as_garbage_l2 where ‹mark_duplicated_binary_clauses_as_garbage_l2 T = do { if get_conflict_l T ≠ None then RETURN T else mark_duplicated_binary_clauses_as_garbage T}› definition mark_to_delete_clauses_l_GC_pre :: ‹'v twl_st_l ⇒ bool› where ‹mark_to_delete_clauses_l_GC_pre S ⟷ (∃T. (S, T) ∈ twl_st_l None ∧ twl_struct_invs T ∧ twl_list_invs S ∧ set (get_all_mark_of_propagated (get_trail_l S)) ⊆ {0})› definition cdcl_twl_full_restart_inprocess_l where ‹cdcl_twl_full_restart_inprocess_l S = do { ASSERT(cdcl_twl_full_restart_l_GC_prog_pre S); S' ← cdcl_twl_local_restart_l_spec0 S; S' ← remove_one_annot_true_clause_imp S'; S' ← mark_duplicated_binary_clauses_as_garbage S'; S' ← forward_subsume_l S'; S' ← pure_literal_eliminate_l S'; S' ← simplify_clauses_with_units_st S'; if (get_conflict_l S' ≠ None) then do { ASSERT(cdcl_twl_restart_l_inp^*^* S S'); RETURN S' } else do { ASSERT(mark_to_delete_clauses_l_GC_pre S'); U ← mark_to_delete_clauses_l S'; V ← cdcl_GC_clauses U; ASSERT(cdcl_twl_restart_l_inp^*^* S V); RETURN V } }› definition cdcl_twl_full_restart_l_GC_prog where ‹cdcl_twl_full_restart_l_GC_prog S = do { ASSERT(cdcl_twl_full_restart_l_GC_prog_pre S); S' ← cdcl_twl_local_restart_l_spec0 S; T ← remove_one_annot_true_clause_imp S'; ASSERT(mark_to_delete_clauses_l_GC_pre T); U ← mark_to_delete_clauses_l T; V ← cdcl_GC_clauses U; ASSERT(cdcl_twl_restart_l S V); RETURN V }› context twl_restart_ops begin lemma cdcl_twl_full_restart_l_prog_spec: assumes ST: ‹(S, T) ∈ twl_st_l None› and list_invs: ‹twl_list_invs S› and struct_invs: ‹twl_struct_invs T› and confl: ‹get_conflict_l S = None› and upd: ‹clauses_to_update_l S = {#}› shows ‹cdcl_twl_full_restart_l_prog S ≤ ⇓ Id (SPEC(remove_one_annot_true_clause⁺⁺ S))› proof - have mark_to_delete_clauses_l: ‹mark_to_delete_clauses_l x ≤ SPEC (λT. ASSERT (mark_to_delete_clauses_l_post U T) ⤜ (λ_. RETURN T) ≤ SPEC (remove_one_annot_true_clause⁺⁺ U))› if Ux: ‹(x, U) ∈ Id› and U: ‹U ∈ Collect (remove_one_annot_true_clause^*^* S)› for x U proof - from U have SU: ‹remove_one_annot_true_clause^*^* S U› by simp have x: ‹x = U› using Ux by auto obtain V where SU': ‹cdcl_twl_restart_l^*^* S U› and UV: ‹(U, V) ∈ twl_st_l None› and TV: ‹cdcl_twl_restart^*^* T V› and struct_invs_V: ‹twl_struct_invs V› using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF SU list_invs confl upd ST struct_invs] by auto have confl_U: ‹get_conflict_l U = None› and upd_U: ‹clauses_to_update_l U = {#}› using rtranclp_remove_one_annot_true_clause_get_conflict_l[OF SU] rtranclp_remove_one_annot_true_clause_clauses_to_update_l[OF SU] confl upd by auto have list_U: ‹twl_list_invs U› using SU' list_invs rtranclp_cdcl_twl_restart_l_list_invs by blast have ‹remove_one_annot_true_clause⁺⁺ U V' ⟹ get_unkept_learned_clss_l V' = {#} ∧ get_subsumed_learned_clauses_l V' = {#} ∧ get_learned_clauses0_l V' = {#}› for V' by (subst (asm)tranclp_unfold_end) (auto simp: remove_one_annot_true_clause.simps) then have [simp]: ‹remove_one_annot_true_clause⁺⁺ U V' ⟹ mark_to_delete_clauses_l_post U V'› for V' unfolding mark_to_delete_clauses_l_post_def using UV struct_invs_V list_U confl_U upd_U by (blast dest: tranclp_into_rtranclp) show ?thesis unfolding x by (rule mark_to_delete_clauses_l_spec[OF UV list_U struct_invs_V confl_U upd_U, THEN order_trans]) (auto intro: RES_refine) qed have 1: ‹SPEC (remove_one_annot_true_clause^*^* S) = do { T ← SPEC (remove_one_annot_true_clause^*^* S); SPEC (remove_one_annot_true_clause^*^* T) }› by (auto simp: RES_RES_RETURN_RES) have H: ‹mark_to_delete_clauses_l_pre T› if ‹(T, U) ∈ Id› and ‹U ∈ Collect (remove_one_annot_true_clause^*^* S)› for T U proof - show ?thesis using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[of S U, OF _ list_invs confl upd ST struct_invs] that list_invs rtranclp_remove_one_annot_true_clause_get_all_mark_of_propagated[of S U] rtranclp_cdcl_twl_restart_l_list_invs[of S U] unfolding mark_to_delete_clauses_l_pre_def by (metis Un_absorb1 mem_Collect_eq pair_in_Id_conv) qed show ?thesis unfolding cdcl_twl_full_restart_l_prog_def apply (refine_vcg mark_to_delete_clauses_l) subgoal using assms unfolding mark_to_delete_clauses_l_pre_def by blast subgoal by auto subgoal by (auto simp: assert_bind_spec_conv) done qed definition GC_required_l :: "'v twl_st_l ⇒ nat ⇒ nat ⇒ bool nres" where ‹GC_required_l S m n = do { ASSERT(size (get_all_learned_clss_l S) ≥ m); SPEC (λb. b ⟶ size (get_all_learned_clss_l S) - m > f n) }› definition restart_required_l :: "'v twl_st_l ⇒ nat ⇒ nat ⇒ bool nres" where ‹restart_required_l S m n = do { ASSERT(size (get_all_learned_clss_l S) ≥ m); SPEC (λb. b ⟶ size (get_all_learned_clss_l S) > m) }› definition inprocessing_required_l :: "'v twl_st_l ⇒ bool nres" where ‹inprocessing_required_l S = do { SPEC (λb. True) }› lemma inprocessing_required_l_inprocessing_required: ‹(inprocessing_required_l, inprocessing_required) ∈ twl_st_l None →_f ⟨bool_rel⟩ nres_rel› by (intro frefI nres_relI) (auto simp: inprocessing_required_l_def inprocessing_required_def) definition restart_abs_l :: "'v twl_st_l ⇒ nat ⇒ nat ⇒ nat ⇒ bool ⇒ ('v twl_st_l × nat × nat × nat) nres" where ‹restart_abs_l S last_GC last_Restart n brk = do { ASSERT(restart_abs_l_pre S last_GC last_Restart brk); b ← GC_required_l S last_GC n; b2 ← restart_required_l S last_Restart n; if b2 ∧ ¬brk then do { T ← SPEC(λT. cdcl_twl_restart_only_l S T); RETURN (T, last_GC, size (get_all_learned_clss_l T), n) } else if b ∧ ¬brk then do { b ← inprocessing_required_l S; if ¬b then do { T ← SPEC(λT. cdcl_twl_restart_l S T); RETURN (T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), n + 1) } else do { T ← SPEC(λT. cdcl_twl_restart_l_inp^*^* S T ∧ count_decided (get_trail_l T) = 0); RETURN (T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), n + 1) } } else RETURN (S, last_GC, last_Restart, n) }› lemma (in -)[twl_st_l]: ‹(S, S') ∈ twl_st_l None ⟹ get_learned_clss S' = twl_clause_of `# (get_learned_clss_l S)› by (auto simp: get_learned_clss_l_def twl_st_l_def) lemma restart_required_l_restart_required: ‹(uncurry2 restart_required_l, uncurry2 restart_required) ∈ {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S} ×_f nat_rel ×_f nat_rel →_f ⟨bool_rel⟩ nres_rel› unfolding restart_required_l_def restart_required_def uncurry_def by (intro frefI nres_relI) (refine_rcg, auto simp: twl_st_l_def get_learned_clss_l_def) lemma GC_required_l_GC_required: ‹(uncurry2 GC_required_l, uncurry2 GC_required) ∈ {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S} ×_f nat_rel ×_f nat_rel →_f ⟨bool_rel⟩ nres_rel› unfolding GC_required_l_def GC_required_def uncurry_def by (intro frefI nres_relI) (refine_rcg, auto simp: twl_st_l_def get_learned_clss_l_def) lemma ‹size (get_learned_clss_l T) = size (learned_clss_l (get_clauses_l T))› by (auto simp: get_learned_clss_l_def) lemma restart_abs_l_restart_prog: ‹(uncurry4 restart_abs_l, uncurry4 restart_prog) ∈ {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} ×_f nat_rel ×_f nat_rel ×_f nat_rel ×_f bool_rel →_f ⟨{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} ×_r nat_rel ×_r nat_rel ×_r nat_rel⟩ nres_rel› proof - have [refine]: ‹RETURN T ≤ ⇓ ({(S, T). (S, T) ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#} ∧ get_conflict_l S = None}) (SPEC (λU. cdcl_twl_stgy^*^* Ta U ∧ clauses_to_update U = {#} ∧ get_conflict U = None))› if ‹(T, Ta) ∈ twl_st_l None› ‹clauses_to_update_l T = {#}› ‹get_conflict_l T = None› ‹twl_list_invs T› for T Ta using that apply - apply (rule RETURN_RES_refine) apply (rule_tac x=Ta in exI) apply (auto intro!: RETURN_RES_refine) done have [refine0]: ‹RETURN False ≤ ⇓ {(a,b). ¬a ∧ ¬b} (inprocessing_required S)› for S by (auto simp: inprocessing_required_def intro!: RETURN_RES_refine) have cdcl_twl_restart_l_inp: ‹(x, y) ∈ {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} ×_f nat_rel ×_f nat_rel ×_f nat_rel ×_f bool_rel ⟹ x1b = (x1c, x2) ⟹ x1a = (x1b, x2a) ⟹ x1 = (x1a, x2b) ⟹ y = (x1, x2c) ⟹ x1f = (x1g, x2d) ⟹ x1e = (x1f, x2e) ⟹ x1d = (x1e, x2f) ⟹ x = (x1d, x2g) ⟹ restart_prog_pre x1c x2 x2a x2c ⟹ restart_abs_l_pre x1g x2d x2e x2g ⟹ SPEC (cdcl_twl_restart_l_inp^*^* x1g) ≤ ⇓{(S, T). (S, T) ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} (SPEC (cdcl_twl_inp^*^* x1c))› for x y x1 x1a x1b x1c x2 x2a x2b x2c x1d x1e x1f x1g x2d x2e x2f x2g b ba b2 b2a bb bc supply [[goals_limit=1]] apply (rule RES_refine) apply (simp only: mem_Collect_eq prod.simps prod_rel_iff restart_abs_l_pre_def restart_prog_pre_def) apply (rule rtranclp_cdcl_twl_restart_l_inp_cdcl_twl_restart_inp) apply assumption+ apply normalize_goal+ apply assumption+ apply normalize_goal+ apply assumption+ apply normalize_goal+ apply assumption+ apply normalize_goal+ apply assumption+ apply (rule_tac x=V in bexI) apply simp apply (intro conjI) apply (meson rtranclp_cdcl_twl_restart_l_inp_twl_list_invs) apply (meson rtranclp_cdcl_twl_restart_l_inp_clauses_to_update_l) apply simp done have inprocess_refine: ‹SPEC (λT. cdcl_twl_restart_l_inp^*^* x1g T ∧ count_decided (get_trail_l T) = 0) ≤ ⇓ {(x,y). (x,y) ∈ twl_st_l None ∧ twl_list_invs x ∧ twl_struct_invs y} (SPEC (λT. cdcl_twl_inp^*^* x1c T ∧ count_decided (get_trail T) = 0))› if True and ‹(x, y) ∈ {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} ×_f nat_rel ×_f nat_rel ×_f nat_rel ×_f bool_rel› and ‹x1b = (x1c, x2)› and ‹x1a = (x1b, x2a)› and ‹x1 = (x1a, x2b)› and ‹y = (x1, x2c)› and ‹x1f = (x1g, x2d)› and ‹x1e = (x1f, x2e)› and ‹x1d = (x1e, x2f)› and ‹x = (x1d, x2g)› and ‹restart_prog_pre x1c x2 x2a x2c› and ‹restart_abs_l_pre x1g x2d x2e x2g› for x y x1 x1a x1b x1c x2 x2a x2b x2c x1d x1e x1f x1g x2d x2e x2f x2g b ba b2 b2a bb bc using that apply (simp only: in_pair_collect_simp prod_rel_iff restart_prog_pre_def) apply (rule RES_refine) unfolding mem_Collect_eq apply normalize_goal+ apply (rule rtranclp_cdcl_twl_restart_l_inp_cdcl_twl_restart_inp) apply assumption+ apply (rule_tac x=V in bexI) apply (auto intro: rtranclp_cdcl_twl_restart_l_inp_twl_list_invs rtranclp_cdcl_twl_inp_twl_struct_invs) done show ?thesis supply [[goals_limit=1]] unfolding restart_abs_l_def restart_prog_def uncurry_def apply (intro frefI nres_relI) apply (refine_rcg restart_required_l_restart_required[THEN fref_to_Down_curry2] GC_required_l_GC_required[THEN fref_to_Down_curry2] cdcl_twl_restart_only_l_cdcl_twl_restart_only cdcl_twl_restart_l_cdcl_twl_restart cdcl_twl_restart_only_l_cdcl_twl_restart_only_spec cdcl_twl_restart_l_inp inprocessing_required_l_inprocessing_required[THEN fref_to_Down] ) subgoal for Snb Snb' unfolding restart_abs_l_pre_def by (rule exI[of _ ‹fst (fst (fst (fst (Snb'))))›]) simp subgoal by auto subgoal by auto subgoal by auto ― ‹If condition› subgoal by simp subgoal unfolding restart_prog_pre_def by auto subgoal by (auto simp: get_learned_clss_l_def) subgoal by auto subgoal by auto subgoal for x y x1 x1a x1b x1c x2 x2a x2b x2c x1d x1e x1f x1g x2d x2e x2f x2g b ba b2 b2a bb bc by auto subgoal by auto subgoal by auto subgoal unfolding restart_prog_pre_def by auto subgoal by (auto simp: get_learned_clss_l_def) apply (rule inprocess_refine; assumption) subgoal by (auto simp: get_learned_clss_l_def rtranclp_cdcl_twl_restart_l_inp_clauses_to_update_l) subgoal by (auto simp: get_learned_clss_l_def) done qed definition cdcl_twl_stgy_restart_abs_l_inv :: ‹'v twl_st_l ⇒ bool × 'v twl_st_l × nat × nat × nat ⇒ bool› where ‹cdcl_twl_stgy_restart_abs_l_inv S₀ ≡ (λ(brk, T, last_GC, last_Restart, n). (∃S₀' T' n'. (T, T') ∈ twl_st_l None ∧ (S₀, S₀') ∈ twl_st_l None ∧ cdcl_twl_stgy_restart_prog_inv (S₀', n') (brk, T', last_GC, last_Restart, n) ∧ clauses_to_update_l T = {#} ∧ twl_list_invs T))› definition cdcl_twl_stgy_restart_abs_l :: "'v twl_st_l ⇒ 'v twl_st_l nres" where ‹cdcl_twl_stgy_restart_abs_l S₀ = do { (brk, T, _, _, _) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_l_inv S₀⇖ (λ(brk, _). ¬brk) (λ(brk, S, m, p, n). do { T ← unit_propagation_outer_loop_l S; (brk, T) ← cdcl_twl_o_prog_l T; (T, m, p, n) ← restart_abs_l T m p n brk; RETURN (brk ∨ get_conflict_l T ≠ None, T, m, p, n) }) (False, S₀, size (get_all_learned_clss_l S₀), size (get_all_learned_clss_l S₀), 0); RETURN T }› (* TODO Move *) lemma (in -)prod_rel_fst_snd_iff: ‹(x, y) ∈ A ×_r B ⟷ (fst x, fst y) ∈ A ∧ (snd x, snd y) ∈ B› by (cases x; cases y) auto lemma cdcl_twl_stgy_restart_abs_l_cdcl_twl_stgy_restart_abs_l: ‹(cdcl_twl_stgy_restart_abs_l, cdcl_twl_stgy_restart_prog) ∈ {(S :: 'v twl_st_l, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →_f ⟨{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S}⟩ nres_rel› unfolding cdcl_twl_stgy_restart_abs_l_def cdcl_twl_stgy_restart_prog_def uncurry_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R = ‹bool_rel ×_r {(S :: 'v twl_st_l, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} ×_r nat_rel ×_r nat_rel ×_r nat_rel›] unit_propagation_outer_loop_l_spec[THEN fref_to_Down] cdcl_twl_o_prog_l_spec[THEN fref_to_Down] restart_abs_l_restart_prog[THEN fref_to_Down_curry4]) subgoal by (auto simp add: get_learned_clss_l_def) subgoal for x y xa x' unfolding cdcl_twl_stgy_restart_abs_l_inv_def case_prod_beta apply (rule_tac x=y in exI) apply (rule_tac x=‹fst (snd x')› in exI) apply (rule_tac x=0 in exI) by (auto simp: prod_rel_fst_snd_iff) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done end lemma cdcl_twl_full_restart_l_GC_prog_cdcl_twl_restart_l: assumes ST: ‹(S, S') ∈ twl_st_l None› and list_invs: ‹twl_list_invs S› and struct_invs: ‹twl_struct_invs S'› and confl: ‹get_conflict_l S = None› and upd: ‹clauses_to_update_l S = {#}› and stgy_invs: ‹twl_stgy_invs S'› and abs_pre: ‹restart_prog_pre S' last_GC last_Restart brk› shows ‹cdcl_twl_full_restart_l_GC_prog S ≤ ⇓ Id (SPEC (λT. cdcl_twl_restart_l S T))› proof - let ?f = ‹(λS T. cdcl_twl_restart_l S T)› let ?f1 = ‹λS S'. (?f S S' ∨ S = S') ∧ count_decided (get_trail_l S') = 0› let ?f1' = ‹λS S'. (?f S S') ∧ count_decided (get_trail_l S') = 0› let ?f2 = ‹λS S'. ?f S S' ∧ (∀L ∈ set (get_trail_l S'). mark_of L = 0) ∧ length (get_trail_l S) = length (get_trail_l S')› let ?f3 = ‹λS S'. ?f1 S S' ∧ (∀L ∈ set (get_trail_l S'). mark_of L = 0) ∧ length (get_trail_l S) = length (get_trail_l S')› have n_d: ‹no_dup (get_trail_l S)› using struct_invs ST unfolding twl_struct_invs_def cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def pcdcl_all_struct_invs_def by (simp add: twl_st) then have alt_def: ‹SPEC (λT. cdcl_twl_restart_l S T) ≥ do { S' ← SPEC (λS'. ?f1 S S'); T ← SPEC (?f2 S'); U ← SPEC (?f3 T); V ← SPEC (λV. ?f3 U V); RETURN V }› unfolding RETURN_def RES_RES_RETURN_RES apply - apply (rule RES_rule) unfolding UN_iff apply (elim bexE)+ unfolding mem_Collect_eq by (metis (full_types) cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l singletonD) have 1: ‹remove_one_annot_true_clause_imp T ≤ SPEC (λV. ?f2 U V)› if ‹(T, U) ∈ Id› and ‹U ∈ Collect (λS'. ?f1 S S')› for T U proof - have ‹T = U› and ‹?f S T ∨ S = T› and count_0: ‹count_decided (get_trail_l T) = 0› using that by auto have confl: ‹get_conflict_l T = None› using ‹?f S T ∨ S = T› confl by (auto simp: cdcl_twl_restart_l.simps) obtain T' where TT': ‹(T, T') ∈ twl_st_l None› and list_invs: ‹twl_list_invs T› and struct_invs: ‹twl_struct_invs T'› and clss_upd: ‹clauses_to_update_l T = {#}› and ‹cdcl_twl_restart S' T' ∨ S' = T'› using cdcl_twl_restart_l_invs[OF assms(1-3), of T] assms ‹?f S T ∨ S = T› by blast show ?thesis unfolding ‹T = U›[symmetric] by (rule remove_one_annot_true_clause_imp_spec_lev0[OF TT' list_invs struct_invs confl clss_upd, THEN order_trans]) (use count_0 remove_one_annot_true_clause_cdcl_twl_restart_l_spec[OF TT' list_invs struct_invs confl clss_upd] n_d ‹?f S T ∨ S = T› remove_one_annot_true_clause_map_mark_of_same_or_0[of T] in ‹auto dest: cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l simp: rtranclp_remove_one_annot_true_clause_count_dec›) qed have mark_to_delete_clauses_l_pre: ‹mark_to_delete_clauses_l_GC_pre U› if ‹(T, T') ∈ Id› and ‹T' ∈ Collect (?f1 S)› and ‹(U, U') ∈ Id› and ‹U' ∈ Collect (?f2 T')› for T T' U U' proof - have ‹T = T'› ‹U = U'› and ‹?f T U› and ‹?f S T ∨ S = T› using that by auto then have ‹?f S U ∨ S = U› using n_d cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l by blast have confl: ‹get_conflict_l U = None› using ‹?f T U› ‹?f S T ∨ S = T› confl by (auto simp: cdcl_twl_restart_l.simps) obtain U' where TT': ‹(U, U') ∈ twl_st_l None› and list_invs: ‹twl_list_invs U› and struct_invs: ‹twl_struct_invs U'› and clss_upd: ‹clauses_to_update_l U = {#}› and ‹cdcl_twl_restart S' U' ∨ S' = U'› using cdcl_twl_restart_l_invs[OF assms(1-3), of U] ‹?f S U ∨ S = U› assms that[of S'] by blast moreover have ‹set (get_all_mark_of_propagated (get_trail_l U)) ⊆ {0}› using that rtranclp_remove_one_annot_true_clause_get_all_mark_of_propagated[of S U] apply simp by (metis annotated_lit.sel(3) cdcl_W_restart_mset.in_get_all_mark_of_propagated_in_trail singletonI subset_code(1)) ultimately show ?thesis unfolding mark_to_delete_clauses_l_GC_pre_def by blast qed have 2: ‹mark_to_delete_clauses_l U ≤ SPEC (λV. ?f3 U' V)› if ‹(T, T') ∈ Id› and ‹T' ∈ Collect (?f1 S)› and UU': ‹(U, U') ∈ Id› and U: ‹U' ∈ Collect (?f2 T')› and pre: ‹mark_to_delete_clauses_l_GC_pre U› for T T' U U' proof - have ‹T = T'› ‹U = U'› and ‹?f T U› and ‹?f S T ∨ S = T› using that by auto then have SU: ‹?f S U› using n_d cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l by blast obtain V where TV: ‹(U, V) ∈ twl_st_l None› and struct: ‹twl_struct_invs V› and list_invs: ‹twl_list_invs U› using pre unfolding mark_to_delete_clauses_l_GC_pre_def by auto have confl: ‹get_conflict_l U = None› and upd: ‹clauses_to_update_l U = {#}› and UU[simp]: ‹U' = U› using U UU' ‹?f T U› confl ‹?f S T ∨ S = T› assms by (auto simp: cdcl_twl_restart_l.simps) have annU: ‹set (get_all_mark_of_propagated (get_trail_l U)) ⊆ {0}› using that rtranclp_remove_one_annot_true_clause_get_all_mark_of_propagated[of S U] apply simp by (metis annotated_lit.sel(3) cdcl_W_restart_mset.in_get_all_mark_of_propagated_in_trail singletonI subset_code(1)) show ?thesis by (rule mark_to_delete_clauses_l_spec[OF TV list_invs struct confl upd, THEN order_trans], subst Down_id_eq) (use remove_one_annot_true_clause_cdcl_twl_restart_l_spec[OF TV list_invs struct confl upd] cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l[OF _ _ n_d, of T] that ST in ‹auto dest!: cdcl_twl_restart_l_count_dec›) qed have 3: ‹cdcl_GC_clauses V ≤ SPEC (?f3 V')› if ‹(T, T') ∈ Id› and ‹T' ∈ Collect (?f1 S)› and ‹(U, U') ∈ Id› and ‹U' ∈ Collect (?f2 T')› and ‹mark_to_delete_clauses_l_GC_pre U› and ‹(V, V') ∈ Id› and ‹V' ∈ Collect (?f3 U')› for T T' U U' V V' proof - have eq: ‹U' = U› using that by auto have st: ‹T = T'› ‹U = U'› ‹V = V'› and ‹?f S T ∨ S = T› and ‹?f T U› and ‹?f U V ∨ U = V› and le_UV: ‹length (get_trail_l U) = length (get_trail_l V)› and mark0: ‹∀L∈set (get_trail_l V'). mark_of L = 0› and count_dec: ‹count_decided (get_trail_l V') = 0› using that by (auto dest!: cdcl_twl_restart_l_count_dec) then have ‹?f S V› using n_d cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l by blast have mark: ‹mark_of (get_trail_l V ! i) = 0› if ‹i < length (get_trail_l V)› for i using that by (use st that le_UV count_dec mark0 in ‹auto simp: count_decided_0_iff is_decided_no_proped_iff›) then have count_dec: ‹count_decided (get_trail_l V') = 0› and mark: ‹⋀L. L ∈ set (get_trail_l V') ⟹ mark_of L = 0› using cdcl_twl_restart_l_count_dec[of U V] that ‹?f U V ∨ U = V› by (auto dest!: cdcl_twl_restart_l_count_dec) obtain W where UV: ‹(V, W) ∈ twl_st_l None› and list_invs: ‹twl_list_invs V› and clss: ‹clauses_to_update_l V = {#}› and ‹cdcl_twl_restart S' W› and struct: ‹twl_struct_invs W› using cdcl_twl_restart_l_invs[OF assms(1,2,3) ‹?f S V›] unfolding eq by blast have confl: ‹get_conflict_l V = None› using ‹?f S V› unfolding eq by (auto simp: cdcl_twl_restart_l.simps) show ?thesis unfolding eq by (rule cdcl_GC_clauses_cdcl_twl_restart_l[OF UV list_invs struct confl clss, THEN order_trans]) (use count_dec cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l[OF _ _ n_d, of U'] ‹?f S V› eq mark in ‹auto simp: ‹V = V'››) qed have cdcl_twl_restart_l: ‹cdcl_twl_restart_l S W› if ‹(T, T') ∈ Id› and ‹T' ∈ Collect (?f1 S)› and ‹(U, U') ∈ Id› and ‹U' ∈ Collect (?f2 T')› and ‹mark_to_delete_clauses_l_GC_pre U› and ‹(V, V') ∈ Id› and ‹V' ∈ Collect (?f3 U')› and ‹(W, W') ∈ Id› and ‹W' ∈ Collect (?f3 V')› for T T' U U' V V' W W' using n_d cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l[of S T U] cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l[of S U V] cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l[of S V W] that by fast have abs_pre: ‹restart_abs_l_pre S last_GC last_Restart False› using assms unfolding cdcl_twl_full_restart_l_GC_prog_pre_def restart_abs_l_pre_def restart_prog_pre_def apply - apply (rule exI[of _ S']) by auto show ?thesis unfolding cdcl_twl_full_restart_l_GC_prog_def apply (rule order_trans) prefer 2 apply (rule ref_two_step') apply (rule alt_def) apply refine_rcg subgoal using assms unfolding cdcl_twl_full_restart_l_GC_prog_pre_def restart_prog_pre_def by fastforce subgoal by (rule cdcl_twl_local_restart_l_spec0_cdcl_twl_restart_l[THEN order_trans, OF abs_pre]) auto subgoal by (rule 1) subgoal for T T' U U' by (rule mark_to_delete_clauses_l_pre) subgoal for T T' U U' by (rule 2) subgoal for T T' U U' V V' by (rule 3) subgoal for T T' U U' V V' W W' by (rule cdcl_twl_restart_l) done qed lemma cdcl_twl_full_restart_inprocess_l_cdcl_twl_restart_l: assumes ST: ‹(S, S') ∈ twl_st_l None› and list_invs: ‹twl_list_invs S› and struct_invs: ‹twl_struct_invs S'› and confl: ‹get_conflict_l S = None› and upd: ‹clauses_to_update_l S = {#}› and stgy_invs: ‹twl_stgy_invs S'› and abs_pre: ‹restart_prog_pre S' last_GC last_Restart brk› shows ‹cdcl_twl_full_restart_inprocess_l S ≤ ⇓ Id (SPEC (λT. cdcl_twl_restart_l_inp^*^* S T ∧ count_decided (get_trail_l T) = 0))› (is ‹_ ≤ ⇓ _ ?P›) proof - let ?f = ‹(λS T. cdcl_twl_restart_l S T)› let ?f1 = ‹λS S'. (?f S S' ∨ S = S') ∧ count_decided (get_trail_l S') = 0› let ?f1' = ‹λS S'. (?f S S') ∧ count_decided (get_trail_l S') = 0› let ?finp = ‹λS S'. cdcl_twl_restart_l_inp^*^* S S' ∧ count_decided (get_trail_l S') = 0 ∧ set (get_all_mark_of_propagated (get_trail_l S')) ⊆ {0}› let ?f2 = ‹λS S'. ?f S S' ∧ (∀L ∈ set (get_trail_l S'). mark_of L = 0) ∧ length (get_trail_l S) = length (get_trail_l S') ∧ set (get_all_mark_of_propagated (get_trail_l S')) ⊆ {0}› let ?f3 = ‹λS S'. ?f1 S S' ∧ (∀L ∈ set (get_trail_l S'). mark_of L = 0) ∧ length (get_trail_l S) = length (get_trail_l S')› have n_d: ‹no_dup (get_trail_l S)› using struct_invs ST unfolding twl_struct_invs_def cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def pcdcl_all_struct_invs_def by (simp add: twl_st) then have alt_def: ‹?P ≥ do { S' ← SPEC (?f1 S); T ← SPEC (?f2 S'); T ← SPEC (?finp T); T ← SPEC (?finp T); U ← SPEC (?finp T); U ← SPEC (?finp U); if(get_conflict_l U ≠ None) then RETURN U else do { U ← SPEC (?f3 U); V ← SPEC (λV. ?f3 U V); RETURN V } }› unfolding RETURN_def RES_RES_RETURN_RES apply - apply refine_vcg apply (metis (no_types, lifting) cdcl_twl_restart_l_inp.intros(1) converse_rtranclp_into_rtranclp rtranclp_trans singletonD) apply simp apply (elim UN_E)+ apply (auto dest!: cdcl_twl_restart_l_inp.intros) done have 1: ‹remove_one_annot_true_clause_imp T ≤ SPEC (?f2 T')› if ‹cdcl_twl_full_restart_l_GC_prog_pre S› and ‹T' ∈ Collect (?f1 S)› and ‹(T, T') ∈ Id› for T T' U U' proof - have ‹T = T'› and ‹?f S T ∨ S = T› and count_0: ‹count_decided (get_trail_l T') = 0› using that by auto have confl: ‹get_conflict_l T' = None› using ‹?f S T ∨ S = T› confl by (auto simp: cdcl_twl_restart_l.simps ‹T = T'›) obtain T'' where TT': ‹(T', T'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs T'› and struct_invs: ‹twl_struct_invs T''› and clss_upd: ‹clauses_to_update_l T' = {#}› and ‹cdcl_twl_restart S' T'' ∨ S' = T''› using cdcl_twl_restart_l_invs[OF assms(1-3), of T] assms ‹?f S T ∨ S = T› unfolding ‹T = T'› by blast have ent: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of T'')› using ‹cdcl_twl_restart S' T'' ∨ S' = T''› abs_pre cdcl_twl_inp.intros(5) cdcl_twl_inp_invs(3) restart_prog_pre_def by blast show ?thesis unfolding ‹T = T'› by (rule remove_one_annot_true_clause_imp_spec_lev0[OF TT' list_invs struct_invs confl clss_upd, THEN order_trans]) (use count_0 remove_one_annot_true_clause_cdcl_twl_restart_l_spec[OF TT' list_invs struct_invs _ clss_upd] n_d ‹?f S T ∨ S = T› count_0 confl remove_one_annot_true_clause_map_mark_of_same_or_0[of T] in ‹auto dest: cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l simp: rtranclp_remove_one_annot_true_clause_count_dec get_all_mark_of_propagated_alt_def›) qed have mark_to_delete_clauses_l_pre: ‹mark_to_delete_clauses_l_GC_pre V› (is ?A) and 2: ‹mark_to_delete_clauses_l V ≤ SPEC (?f3 V')› (is ?B) and 3: ‹W' ∈ Collect (?f3 V') ⟹ (W,W') ∈ Id ⟹ cdcl_GC_clauses W ≤ SPEC (?f3 W')› (is ‹_ ⟹ _ ⟹ ?C›) and cdcl_twl_restart_l: ‹W' ∈ Collect (?f3 V') ⟹ (W,W') ∈ Id ⟹ X' ∈ Collect (?f3 W') ⟹ (X,X') ∈ Id ⟹ cdcl_twl_restart_l_inp^*^* S X› (is ‹_ ⟹ _ ⟹ _ ⟹ _ ⟹ ?D›) if ‹T' ∈ Collect (?f1 S)› and ‹U' ∈ Collect (?f2 T')› and ‹U₁' ∈ Collect (?finp U')› and ‹U₂' ∈ Collect (?finp U₁')› and ‹V₀' ∈ Collect (?finp U₂')› and ‹V' ∈ Collect (?finp V₀')› and confl_U': ‹¬get_conflict_l V' ≠ None› and ‹(V, V') ∈ Id› and ‹(T, T') ∈ Id› and ‹(U, U') ∈ Id› and ‹(U₁, U₁') ∈ Id› and ‹(U₂, U₂') ∈ Id› for T T' U U' V V' W W' X X' U₀ U₀' V₀' U₁' U₁ U₂ U₂' proof - have ‹T = T'› ‹U=U'› ‹V'=V› ‹U₁' = U₁› ‹U₂' = U₂› and ‹?f S T ∨ S = T› and count_0: ‹count_decided (get_trail_l T) = 0› and T'U': ‹cdcl_twl_restart_l T' U'› and count_0_V: ‹count_decided (get_trail_l V') = 0› and confl_V': ‹get_conflict_l V' = None› and UV: ‹cdcl_twl_restart_l_inp^*^* U V› and ‹∀L∈set (get_trail_l U'). mark_of L = 0› and mark: ‹set (get_all_mark_of_propagated (get_trail_l V')) ⊆ {0}› using that by auto have confl: ‹get_conflict_l T = None› using ‹?f S T ∨ S = T› confl by (auto simp: cdcl_twl_restart_l.simps) obtain T'' where TT': ‹(T', T'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs T'› and struct_invs: ‹twl_struct_invs T''› and clss_upd: ‹clauses_to_update_l T' = {#}› and ‹cdcl_twl_restart S' T'' ∨ S' = T''› using cdcl_twl_restart_l_invs[OF assms(1-3), of T] assms ‹?f S T ∨ S = T› unfolding ‹T = T'› by blast have ent: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of T'')› using ‹cdcl_twl_restart S' T'' ∨ S' = T''› abs_pre cdcl_twl_inp.intros(5) cdcl_twl_inp_invs(3) restart_prog_pre_def by blast obtain U'' where UU'': ‹(U, U'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs U› and ‹clauses_to_update_l U = {#}› and ‹cdcl_twl_restart T'' U''› and struct_invs: ‹twl_struct_invs U''› using cdcl_twl_restart_l_invs[OF TT' list_invs struct_invs T'U'] unfolding ‹U=U'› by blast have ent: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of U'')› by (metis ‹cdcl_twl_restart T'' U''› cdcl_twl_restart_entailed_init ent state_W_of_def) obtain V'' where VV'': ‹(V, V'') ∈ twl_st_l None› and U''V'': ‹cdcl_twl_inp^*^* U'' V''› using rtranclp_cdcl_twl_restart_l_inp_cdcl_twl_restart_inp[OF UV UU'' list_invs struct_invs ent] unfolding ‹V'=V› by blast then have list_invs: ‹twl_list_invs V› and struct_invs: ‹twl_struct_invs V''› and clss_upd: ‹clauses_to_update_l V = {#}› using T'U' ent UV ‹V' = V› list_invs rtranclp_cdcl_twl_restart_l_inp_twl_list_invs ‹cdcl_twl_inp^*^* U'' V''› ent ‹clauses_to_update_l U = {#}› struct_invs rtranclp_cdcl_twl_restart_l_inp_clauses_to_update_l[OF UV] by (blast intro: rtranclp_cdcl_twl_restart_l_inp_twl_list_invs rtranclp_cdcl_twl_inp_invs)+ have H: ‹L ∈ set (get_trail_l V') ⟹ mark_of L = 0› for L using mark count_0_V by (cases L) (auto dest!: split_list) have annV: ‹set (get_all_mark_of_propagated (get_trail_l V)) ⊆ {0}› using that rtranclp_remove_one_annot_true_clause_get_all_mark_of_propagated[of S V] by simp then show ?A using VV'' U''V'' mark list_invs struct_invs clss_upd unfolding mark_to_delete_clauses_l_GC_pre_def ‹V'=V› by blast have confl: ‹get_conflict_l V = None› using U''V'' VV'' confl_V' UU'' by (auto simp: cdcl_twl_restart.simps ‹U=U'› ‹V'=V› twl_st_l_def) show ?B unfolding ‹V'=V› by (rule mark_to_delete_clauses_l_spec[OF VV'' list_invs struct_invs confl clss_upd, THEN order_trans], subst Down_id_eq) (use confl remove_one_annot_true_clause_cdcl_twl_restart_l_spec[OF VV'' list_invs struct_invs _ clss_upd] H cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l[OF _ _ n_d, of T] that ST in ‹auto dest!: cdcl_twl_restart_l_count_dec simp: ›) assume W': ‹W' ∈ Collect (?f3 V')› and ‹(W,W') ∈ Id› then have ‹W' = W› and VW: ‹?f V W ∨ V = W› and mark_W: ‹∀L∈set (get_trail_l W). mark_of L = 0› using ‹V'=V› by auto obtain W'' where VW'': ‹(W, W'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs W› and upd: ‹clauses_to_update_l W = {#}› and U''W'': ‹cdcl_twl_restart V'' W'' ∨ V = W› and struct_invs: ‹twl_struct_invs W''› using cdcl_twl_restart_l_invs[OF VV'' list_invs struct_invs, of W] list_invs struct_invs clss_upd VV'' VW unfolding ‹W' = W› by blast have confl_W: ‹get_conflict_l W = None› and count_0_W: ‹count_decided (get_trail_l W) = 0› by (use confl U''W'' VW'' VV'' count_0_V in ‹auto simp: ‹W' = W› ‹V'=V› twl_st_l_def cdcl_twl_restart.simps›)[] (use VW VV'' VW'' count_0_V in ‹auto dest!: cdcl_twl_restart_l_count_dec simp: ‹W' = W› ‹V'=V› ›) show ?C unfolding ‹W' = W› by (rule cdcl_GC_clauses_cdcl_twl_restart_l[OF VW'' list_invs struct_invs confl_W upd, THEN order_trans]) (use count_0_W mark_W cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l[OF _ _ n_d, of U'] in ‹auto simp: ‹V' = V››) assume W': ‹X' ∈ Collect (?f3 W')› and ‹(X,X') ∈ Id› then have ‹X' = X› and WX: ‹?f W X ∨ W = X› using ‹V'=V› ‹W'=W› by auto show ‹cdcl_twl_restart_l_inp^*^* S X› using that WX VW unfolding mem_Collect_eq by (auto dest!: cdcl_twl_restart_l_inp.intros) qed have abs_l_pre: ‹restart_abs_l_pre S last_GC last_Restart False› using assms unfolding restart_abs_l_pre_def restart_prog_pre_def apply - apply (rule exI[of _ S']) by auto have mark_duplicated_binary_clauses_as_garbage: ‹mark_duplicated_binary_clauses_as_garbage U ≤ SPEC (?finp U')› if pre: ‹cdcl_twl_full_restart_l_GC_prog_pre S› and ‹T' ∈ Collect (?f1 S)› ‹U' ∈ Collect (?f2 T')› and ‹(T, T') ∈ Id› and ‹(U, U') ∈ Id› for T T' U U' proof - have st: ‹T = T'› ‹U=U'› and ‹?f S T ∨ S = T› and count_0: ‹count_decided (get_trail_l T) = 0› and T'U': ‹cdcl_twl_restart_l T' U'› and mark: ‹∀L∈set (get_trail_l U'). mark_of L = 0› and lev0: ‹count_decided (get_trail_l T) = 0› using that by auto have confl: ‹get_conflict_l T = None› using ‹?f S T ∨ S = T› confl by (auto simp: cdcl_twl_restart_l.simps) obtain T'' where TT': ‹(T', T'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs T'› and struct_invs: ‹twl_struct_invs T''› and clss_upd: ‹clauses_to_update_l T' = {#}› and ‹cdcl_twl_restart S' T'' ∨ S' = T''› using cdcl_twl_restart_l_invs[OF assms(1-3), of T] assms ‹?f S T ∨ S = T› unfolding ‹T = T'› by blast have ent: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of T'')› using ‹cdcl_twl_restart S' T'' ∨ S' = T''› abs_pre cdcl_twl_inp.intros(5) cdcl_twl_inp_invs(3) restart_prog_pre_def by blast obtain U'' where UU'': ‹(U, U'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs U› and clss: ‹clauses_to_update_l U = {#}› and T''U'': ‹cdcl_twl_restart T'' U''› and struct_invs: ‹twl_struct_invs U''› using cdcl_twl_restart_l_invs[OF TT' list_invs struct_invs T'U'] unfolding ‹U=U'› by blast have ent: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of U'')› by (metis ‹cdcl_twl_restart T'' U''› cdcl_twl_restart_entailed_init ent state_W_of_def) have lev0: ‹count_decided (get_trail_l U) = 0› using T''U'' by (metis T'U' cdcl_twl_restart_l_count_dec le_zero_eq lev0 st(1) st(2)) have confl: ‹get_conflict_l U = None› using upd UU'' clss T'U' by (auto simp add: cdcl_twl_full_restart_l_GC_prog_pre_def cdcl_twl_restart_l.simps st twl_st_l_def) have pre: ‹mark_duplicated_binary_clauses_as_garbage_pre U› using ent clss lev0 mark apply - unfolding mark_duplicated_binary_clauses_as_garbage_pre_def ‹U= U'›[symmetric] by (rule exI[of _ U'']) (auto 4 3 simp: UU'' clss_upd list_invs struct_invs cdcl_W_restart_mset.in_get_all_mark_of_propagated_in_trail) show ?thesis apply (rule mark_duplicated_binary_clauses_as_garbage[THEN order_trans]) apply (rule pre) subgoal apply simp apply standard apply simp by (metis Un_absorb1 mark_duplicated_binary_clauses_as_garbage_pre_def pre rtranclp_cdcl_twl_inprocessing_l_cdcl_twl_l_inp rtranclp_cdcl_twl_inprocessing_l_count_decided rtranclp_cdcl_twl_inprocessing_l_get_all_mark_of_propagated st(2)) done qed have simplify_clauses_with_unit_st: ‹simplify_clauses_with_units_st V ≤ SPEC (?finp V')› if pre: ‹cdcl_twl_full_restart_l_GC_prog_pre S› and ‹T' ∈ Collect (?f1 S)› ‹U' ∈ Collect (?f2 T')› ‹U₂' ∈ Collect (?finp U')›and ‹U₃' ∈ Collect (?finp U₂')›and ‹V' ∈ Collect (?finp U₃')›and ‹(T, T') ∈ Id› and ‹(U, U') ∈ Id› and ‹(V, V') ∈ Id› and ‹(U₂, U₂') ∈ Id›and ‹(U₃, U₃') ∈ Id› for T T' U U' V V' U₂' U₂ U₃ U₃' proof - have st: ‹T = T'› ‹U=U'› ‹V'=V› ‹U₂' = U₂› and ‹?f S T ∨ S = T› and count_0: ‹count_decided (get_trail_l T) = 0› and T'U': ‹cdcl_twl_restart_l T' U'› and mark: ‹∀L∈set (get_trail_l U'). mark_of L = 0› and lev0: ‹count_decided (get_trail_l T) = 0› and UV': ‹cdcl_twl_restart_l_inp^*^* U' V'› and count_dec: ‹count_decided (get_trail_l V') = 0› and annot_V: ‹set (get_all_mark_of_propagated (get_trail_l V')) ⊆ {0}› using that by auto have confl: ‹get_conflict_l T = None› using ‹?f S T ∨ S = T› confl by (auto simp: cdcl_twl_restart_l.simps) obtain T'' where TT': ‹(T', T'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs T'› and struct_invs: ‹twl_struct_invs T''› and clss_upd: ‹clauses_to_update_l T' = {#}› and ‹cdcl_twl_restart S' T'' ∨ S' = T''› using cdcl_twl_restart_l_invs[OF assms(1-3), of T] assms ‹?f S T ∨ S = T› unfolding ‹T = T'› by blast have ent: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of T'')› using ‹cdcl_twl_restart S' T'' ∨ S' = T''› abs_pre cdcl_twl_inp.intros(5) cdcl_twl_inp_invs(3) restart_prog_pre_def by blast obtain U'' where UU'': ‹(U', U'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs U'› and clss: ‹clauses_to_update_l U' = {#}› and T''U'': ‹cdcl_twl_restart T'' U''› and struct_invs: ‹twl_struct_invs U''› using cdcl_twl_restart_l_invs[OF TT' list_invs struct_invs T'U'] unfolding ‹U=U'› by blast have ent_U'': ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of U'')› by (metis T''U'' cdcl_twl_restart_entailed_init ent state_W_of_def) then obtain V'' where VV'': ‹(V', V'') ∈ twl_st_l None› and U''V'': ‹cdcl_twl_inp^*^* U'' V''› using rtranclp_cdcl_twl_restart_l_inp_cdcl_twl_restart_inp[OF UV' UU'' list_invs struct_invs] by blast then have list_invs: ‹twl_list_invs V'› and clss_upd: ‹clauses_to_update_l V' = {#}› and struct_invs: ‹twl_struct_invs V''› using T'U' ent UV' ‹V' = V› list_invs rtranclp_cdcl_twl_restart_l_inp_twl_list_invs ‹cdcl_twl_inp^*^* U'' V''› ent ‹clauses_to_update_l U' = {#}› struct_invs rtranclp_cdcl_twl_restart_l_inp_clauses_to_update_l[OF UV'] rtranclp_cdcl_twl_inp_invs[OF U''V''] ent_U'' unfolding ‹V' = V› by (blast intro: rtranclp_cdcl_twl_restart_l_inp_twl_list_invs rtranclp_cdcl_twl_inp_invs)+ have ent_V'': ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of V'')› using ent_U'' U''V'' rtranclp_cdcl_twl_inp_entailed_init struct_invs using T''U'' ‹cdcl_twl_restart S' T'' ∨ S' = T''› assms(3) cdcl_twl_restart_twl_struct_invs by blast have pre: ‹mark_duplicated_binary_clauses_as_garbage_pre V› using annot_V count_dec ent_V'' apply - unfolding mark_duplicated_binary_clauses_as_garbage_pre_def ‹V' = V›[symmetric] by (rule exI[of _ V'']) (auto simp: VV'' clss_upd list_invs struct_invs) show ?thesis apply (rule simplify_clauses_with_units_st_spec[THEN order_trans, of _ V'']) apply (use lev0 UU'' struct_invs list_invs confl clss ent annot_V count_dec ent_V'' ‹V' = V›[symmetric] clss_upd VV'' in auto)[7] by (use mark count_dec annot_V in ‹auto 4 4 dest: rtranclp_cdcl_twl_inprocessing_l_cdcl_twl_l_inp rtranclp_cdcl_twl_inprocessing_l_count_dec simp: st lev0 get_all_mark_of_propagated_alt_def simplify_clauses_with_unit_st_inv_def simp flip: ‹U=U'› ‹V' = V››) qed have forward_subsumption_all: ‹forward_subsume_l V ≤ SPEC (?finp V')› if pre: ‹cdcl_twl_full_restart_l_GC_prog_pre S› and ‹T' ∈ Collect (?f1 S)› ‹U' ∈ Collect (?f2 T')› ‹V' ∈ Collect (?finp U')›and ‹(T, T') ∈ Id› and ‹(U, U') ∈ Id›and ‹(V, V') ∈ Id› for T T' U U' V V' proof - have st: ‹T = T'› ‹U=U'› ‹V'=V› and ‹?f S T ∨ S = T› and count_0: ‹count_decided (get_trail_l T) = 0› and T'U': ‹cdcl_twl_restart_l T' U'› and mark: ‹∀L∈set (get_trail_l U'). mark_of L = 0› and lev0: ‹count_decided (get_trail_l T) = 0› and UV': ‹cdcl_twl_restart_l_inp^*^* U' V'› and count_dec: ‹count_decided (get_trail_l V') = 0› and annot_V: ‹set (get_all_mark_of_propagated (get_trail_l V')) ⊆ {0}› using that by auto have confl: ‹get_conflict_l T = None› using ‹?f S T ∨ S = T› confl by (auto simp: cdcl_twl_restart_l.simps) obtain T'' where TT': ‹(T', T'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs T'› and struct_invs: ‹twl_struct_invs T''› and clss_upd: ‹clauses_to_update_l T' = {#}› and ‹cdcl_twl_restart S' T'' ∨ S' = T''› using cdcl_twl_restart_l_invs[OF assms(1-3), of T] assms ‹?f S T ∨ S = T› unfolding ‹T = T'› by blast have ent: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of T'')› using ‹cdcl_twl_restart S' T'' ∨ S' = T''› abs_pre cdcl_twl_inp.intros(5) cdcl_twl_inp_invs(3) restart_prog_pre_def by blast obtain U'' where UU'': ‹(U', U'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs U'› and clss: ‹clauses_to_update_l U' = {#}› and T''U'': ‹cdcl_twl_restart T'' U''› and struct_invs: ‹twl_struct_invs U''› using cdcl_twl_restart_l_invs[OF TT' list_invs struct_invs T'U'] unfolding ‹U=U'› by blast have ent_U'': ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of U'')› by (metis T''U'' cdcl_twl_restart_entailed_init ent state_W_of_def) then obtain V'' where VV'': ‹(V', V'') ∈ twl_st_l None› and U''V'': ‹cdcl_twl_inp^*^* U'' V''› using rtranclp_cdcl_twl_restart_l_inp_cdcl_twl_restart_inp[OF UV' UU'' list_invs struct_invs] by blast then have list_invs: ‹twl_list_invs V'› and clss_upd: ‹clauses_to_update_l V' = {#}› and struct_invs: ‹twl_struct_invs V''› using T'U' ent UV' ‹V' = V› list_invs rtranclp_cdcl_twl_restart_l_inp_twl_list_invs ‹cdcl_twl_inp^*^* U'' V''› ent ‹clauses_to_update_l U' = {#}› struct_invs rtranclp_cdcl_twl_restart_l_inp_clauses_to_update_l[OF UV'] rtranclp_cdcl_twl_inp_invs[OF U''V''] ent_U'' unfolding ‹V' = V› by (blast intro: rtranclp_cdcl_twl_restart_l_inp_twl_list_invs rtranclp_cdcl_twl_inp_invs)+ have ent_V'': ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of V'')› using ent_U'' U''V'' rtranclp_cdcl_twl_inp_entailed_init struct_invs using T''U'' ‹cdcl_twl_restart S' T'' ∨ S' = T''› assms(3) cdcl_twl_restart_twl_struct_invs by blast have pre: ‹forward_subsumption_all_pre V› unfolding forward_subsumption_all_pre_def using annot_V count_dec ent_V'' apply - unfolding mark_duplicated_binary_clauses_as_garbage_pre_def ‹V' = V›[symmetric] by (rule exI[of _ V'']) (auto simp: VV'' clss_upd list_invs struct_invs) show ?thesis by (rule forward_subsume_l[THEN order_trans, of ]) (use lev0 UU'' struct_invs list_invs confl clss ent annot_V count_dec ent_V'' ‹V' = V›[symmetric] clss_upd VV'' pre in ‹auto dest: rtranclp_cdcl_twl_inprocessing_l_cdcl_twl_l_inp rtranclp_cdcl_twl_inprocessing_l_count_decided rtranclp_cdcl_twl_inprocessing_l_get_all_mark_of_propagated›) qed have pure_literal_elimination_round: ‹pure_literal_eliminate_l V ≤ SPEC (?finp V')› if pre: ‹cdcl_twl_full_restart_l_GC_prog_pre S› and ‹T' ∈ Collect (?f1 S)› ‹U' ∈ Collect (?f2 T')› ‹U₁' ∈ Collect (?finp U')› ‹V' ∈ Collect (?finp U₁')› and ‹(T, T') ∈ Id› and ‹(U, U') ∈ Id›and ‹(U₁, U₁') ∈ Id›and ‹(V, V') ∈ Id› for T T' U U' V V' U₁ U₁' proof - have st: ‹T = T'› ‹U=U'› ‹V'=V› ‹U₁' = U₁› and ‹?f S T ∨ S = T› and count_0: ‹count_decided (get_trail_l T) = 0› and T'U': ‹cdcl_twl_restart_l T' U'› and mark: ‹∀L∈set (get_trail_l U'). mark_of L = 0› and lev0: ‹count_decided (get_trail_l T) = 0› and UV': ‹cdcl_twl_restart_l_inp^*^* U' V'› and count_dec: ‹count_decided (get_trail_l V') = 0› and annot_V: ‹set (get_all_mark_of_propagated (get_trail_l V')) ⊆ {0}› using that by auto have confl: ‹get_conflict_l T = None› using ‹?f S T ∨ S = T› confl by (auto simp: cdcl_twl_restart_l.simps) obtain T'' where TT': ‹(T', T'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs T'› and struct_invs: ‹twl_struct_invs T''› and clss_upd: ‹clauses_to_update_l T' = {#}› and ‹cdcl_twl_restart S' T'' ∨ S' = T''› using cdcl_twl_restart_l_invs[OF assms(1-3), of T] assms ‹?f S T ∨ S = T› unfolding ‹T = T'› by blast have ent: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of T'')› using ‹cdcl_twl_restart S' T'' ∨ S' = T''› abs_pre cdcl_twl_inp.intros(5) cdcl_twl_inp_invs(3) restart_prog_pre_def by blast obtain U'' where UU'': ‹(U', U'') ∈ twl_st_l None› and list_invs: ‹twl_list_invs U'› and clss: ‹clauses_to_update_l U' = {#}› and T''U'': ‹cdcl_twl_restart T'' U''› and struct_invs: ‹twl_struct_invs U''› using cdcl_twl_restart_l_invs[OF TT' list_invs struct_invs T'U'] unfolding ‹U=U'› by blast have ent_U'': ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of U'')› by (metis T''U'' cdcl_twl_restart_entailed_init ent state_W_of_def) then obtain V'' where VV'': ‹(V', V'') ∈ twl_st_l None› and U''V'': ‹cdcl_twl_inp^*^* U'' V''› using rtranclp_cdcl_twl_restart_l_inp_cdcl_twl_restart_inp[OF UV' UU'' list_invs struct_invs] by blast then have list_invs: ‹twl_list_invs V'› and clss_upd: ‹clauses_to_update_l V' = {#}› and struct_invs: ‹twl_struct_invs V''› using T'U' ent UV' ‹V' = V› list_invs rtranclp_cdcl_twl_restart_l_inp_twl_list_invs ‹cdcl_twl_inp^*^* U'' V''› ent ‹clauses_to_update_l U' = {#}› struct_invs rtranclp_cdcl_twl_restart_l_inp_clauses_to_update_l[OF UV'] rtranclp_cdcl_twl_inp_invs[OF U''V''] ent_U'' unfolding ‹V' = V› by (blast intro: rtranclp_cdcl_twl_restart_l_inp_twl_list_invs rtranclp_cdcl_twl_inp_invs)+ have ent_V'': ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of V'')› using ent_U'' U''V'' rtranclp_cdcl_twl_inp_entailed_init struct_invs using T''U'' ‹cdcl_twl_restart S' T'' ∨ S' = T''› assms(3) cdcl_twl_restart_twl_struct_invs by blast have pre: ‹pure_literal_elimination_l_pre V› unfolding pure_literal_elimination_l_pre_def using annot_V count_dec ent_V'' apply - unfolding mark_duplicated_binary_clauses_as_garbage_pre_def ‹V' = V›[symmetric] by (rule exI[of _ V'']) (auto simp: VV'' clss_upd list_invs struct_invs) show ?thesis by (rule pure_literal_eliminate_l[THEN order_trans, of ]) (use lev0 UU'' struct_invs list_invs confl clss ent annot_V count_dec ent_V'' ‹V' = V›[symmetric] clss_upd VV'' pre in ‹auto dest: rtranclp_cdcl_twl_inprocessing_l_cdcl_twl_l_inp rtranclp_cdcl_twl_inprocessing_l_count_decided rtranclp_cdcl_twl_inprocessing_l_get_all_mark_of_propagated›) qed show ?thesis unfolding cdcl_twl_full_restart_inprocess_l_def apply (rule order_trans) prefer 2 apply (rule ref_two_step') apply (rule alt_def) apply refine_rcg subgoal using assms unfolding cdcl_twl_full_restart_l_GC_prog_pre_def restart_prog_pre_def by fastforce subgoal by (rule cdcl_twl_local_restart_l_spec0_cdcl_twl_restart_l[THEN order_trans, OF abs_l_pre]) auto subgoal for T T' by (rule 1) subgoal by (rule mark_duplicated_binary_clauses_as_garbage) subgoal by (rule forward_subsumption_all) subgoal by (rule pure_literal_elimination_round) subgoal for T T' U U' by (rule simplify_clauses_with_unit_st) subgoal by auto subgoal by (auto 5 3 dest: cdcl_twl_restart_l_inp.intros) subgoal by (rule mark_to_delete_clauses_l_pre) subgoal for U U' by (rule 2) subgoal for U U' V V' W W' by (rule 3) subgoal for U U' V V' W W' by (rule cdcl_twl_restart_l) done qed context twl_restart_ops begin definition restart_prog_l :: "'v twl_st_l ⇒ nat ⇒ nat ⇒ nat ⇒ bool ⇒ ('v twl_st_l × nat × nat × nat) nres" where ‹restart_prog_l S last_GC last_Restart n brk = do { ASSERT(restart_abs_l_pre S last_GC last_Restart brk); b ← GC_required_l S last_GC n; b2 ← restart_required_l S last_Restart n; if b2 ∧ ¬brk then do { T ← cdcl_twl_restart_l_prog S; RETURN (T, last_GC, size (get_all_learned_clss_l T), n) } else if b ∧ ¬brk then do { inp ← inprocessing_required_l S; if ¬inp then do { b ← SPEC(λ_. True); T ← (if b then cdcl_twl_full_restart_l_prog S else cdcl_twl_full_restart_l_GC_prog S); RETURN (T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), n + 1) } else do { T ← cdcl_twl_full_restart_inprocess_l S; RETURN (T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), n + 1) } } else RETURN (S, last_GC, last_Restart, n) }› lemma restart_prog_l_alt_def: ‹restart_prog_l S last_GC last_Restart n brk = do { ASSERT(restart_abs_l_pre S last_GC last_Restart brk); b ← GC_required_l S last_GC n; b2 ← restart_required_l S last_Restart n; if b2 ∧ ¬brk then do { T ← cdcl_twl_restart_l_prog S; RETURN (T, last_GC, size (get_all_learned_clss_l T), n) } else if b ∧ ¬brk then do { inp ← inprocessing_required_l S; if ¬inp then do { b ← SPEC(λ_. True); T ← (if b then cdcl_twl_full_restart_l_prog S else cdcl_twl_full_restart_l_GC_prog S); RETURN (T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), n + 1) } else do { T ← cdcl_twl_full_restart_inprocess_l S; RETURN (T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), n + 1) } } else RETURN (S, last_GC, last_Restart, n) }› by (auto simp: restart_prog_l_def cong: if_cong) lemma restart_prog_l_restart_abs_l: ‹(uncurry4 restart_prog_l, uncurry4 restart_abs_l) ∈ {(S:: 'v twl_st_l, S'). (S, S') ∈ Id ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} ×_f nat_rel ×_f nat_rel×_f nat_rel ×_f bool_rel →_f ⟨{(S:: 'v twl_st_l, S'). (S, S') ∈ Id ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} ×_r nat_rel ×_r nat_rel ×_r nat_rel⟩nres_rel› (is ‹_ ∈ ?R ×_f nat_rel ×_f nat_rel×_f nat_rel ×_f bool_rel →_f _›) proof - have cdcl_twl_full_restart_l_prog: ‹cdcl_twl_full_restart_l_prog S ≤ SPEC (λT. cdcl_twl_restart_l S T)› if inv: ‹restart_abs_l_pre S last_GC last_Restart brk› and ‹(b, ba) ∈ bool_rel› and ‹b ∈ {b. b ⟶ f n < size ( S)}› and ‹ba ∈ {b. b ⟶ f n < size ( S)}› and brk: ‹¬brk› for b ba S brk n last_GC last_Restart proof - obtain T where ST: ‹(S, T) ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs T› and list_invs: ‹twl_list_invs S› and upd: ‹clauses_to_update_l S = {#}› and stgy_invs: ‹twl_stgy_invs T› and confl: ‹get_conflict_l S = None› using inv brk unfolding restart_abs_l_pre_def restart_prog_pre_def apply - apply normalize_goal+ by (auto simp: twl_st) show ?thesis using cdcl_twl_full_restart_l_prog_spec[OF ST list_invs struct_invs confl upd] remove_one_annot_true_clause_cdcl_twl_restart_l_spec[OF ST list_invs struct_invs confl upd] by (rule conc_trans_additional) qed have cdcl_twl_full_restart_l_GC_prog: ‹cdcl_twl_full_restart_l_GC_prog S ≤ SPEC (cdcl_twl_restart_l S)› if inv: ‹restart_abs_l_pre S last_GC last_Restart brk› and brk: ‹ba ∧ b2a ∧ ¬ brk› for ba b2a brk S last_GC last_Restart proof - obtain T where ST: ‹(S, T) ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs T› and list_invs: ‹twl_list_invs S› and upd: ‹clauses_to_update_l S = {#}› and stgy_invs: ‹twl_stgy_invs T› and confl: ‹get_conflict_l S = None› and inv2: ‹restart_prog_pre T last_GC last_Restart brk› and ent_init: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of T)› using inv brk unfolding restart_abs_l_pre_def restart_prog_pre_def apply - apply normalize_goal+ by (auto simp: twl_st) show ?thesis by (rule cdcl_twl_full_restart_l_GC_prog_cdcl_twl_restart_l[unfolded Down_id_eq, OF ST list_invs struct_invs confl upd stgy_invs inv2]) qed have restart_abs_l_alt_def: ‹restart_abs_l S last_GC last_Restart n brk = do { ASSERT(restart_abs_l_pre S last_GC last_Restart brk); b ← GC_required_l S last_GC n; b2 ← restart_required_l S last_Restart n; if b2 ∧ ¬brk then do { T ← SPEC(λT. cdcl_twl_restart_only_l S T); RETURN (T, last_GC, size (get_all_learned_clss_l T), n) } else if b ∧ ¬brk then do { inp ← inprocessing_required_l S; if ¬inp then do { _ ← SPEC(λ_::bool. True); T ← SPEC(λT. cdcl_twl_restart_l S T); RETURN (T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), n + 1) } else do { T ← SPEC (λT. cdcl_twl_restart_l_inp^*^* S T ∧ count_decided (get_trail_l T) = 0); RETURN (T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), n + 1) } } else RETURN (S, last_GC, last_Restart, n) }› for S last_GC last_Restart n brk unfolding restart_abs_l_def by (auto cong: if_cong) have cdcl_twl_full_restart_inprocess_l: ‹cdcl_twl_full_restart_inprocess_l S ≤ SPEC (λT. cdcl_twl_restart_l_inp^*^* S T ∧ count_decided (get_trail_l T) = 0)› if inv: ‹restart_abs_l_pre S last_GC last_Restart brk› and brk: ‹ba ∧ b2a ∧ ¬ brk› for ba b2a brk S last_GC last_Restart proof - obtain T where ST: ‹(S, T) ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs T› and list_invs: ‹twl_list_invs S› and upd: ‹clauses_to_update_l S = {#}› and stgy_invs: ‹twl_stgy_invs T› and confl: ‹get_conflict_l S = None› and inv2: ‹restart_prog_pre T last_GC last_Restart brk› and ent_init: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of T)› using inv brk unfolding restart_abs_l_pre_def restart_prog_pre_def apply - apply normalize_goal+ by (auto simp: twl_st) show ?thesis by (rule cdcl_twl_full_restart_inprocess_l_cdcl_twl_restart_l[THEN order_trans, OF ST list_invs struct_invs confl upd stgy_invs inv2]) auto qed have cdcl_twl_full_restart_inprocess_l: ‹cdcl_twl_full_restart_inprocess_l S ≤ SPEC (λT. cdcl_twl_restart_l_inp^*^* S T ∧ count_decided (get_trail_l T) = 0)› if inv: ‹restart_abs_l_pre S last_GC last_Restart brk› and brk: ‹b ∧ ¬ brk› for b ba b2 b2a inp inp' S last_GC last_Restart brk proof - obtain S' where SS': ‹(S, S') ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs S'› and list_invs: ‹twl_list_invs S› and upd: ‹clauses_to_update_l S = {#}› and stgy_invs: ‹twl_stgy_invs S'› and confl: ‹get_conflict_l S = None› and inv2: ‹restart_prog_pre S' last_GC last_Restart brk› and ent_init: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_W_of S')› using inv brk unfolding restart_abs_l_pre_def restart_prog_pre_def apply - apply normalize_goal+ by (auto simp: twl_st) show ?thesis by (rule cdcl_twl_full_restart_inprocess_l_cdcl_twl_restart_l[unfolded Down_id_eq, OF SS' list_invs struct_invs confl upd stgy_invs inv2]) qed have [simp]: ‹cdcl_twl_restart_only_l S Ta ⟹clauses_to_update_l Ta = {#}› for S Ta by (auto simp: cdcl_twl_restart_only_l.simps) have [simp]: ‹cdcl_twl_restart_l S Ta ⟹clauses_to_update_l Ta = {#}› for S Ta by (auto simp: cdcl_twl_restart_l.simps) have ‹restart_prog_l S p m n brk ≤ ⇓ (?R ×_r nat_rel ×_r nat_rel ×_r nat_rel) (restart_abs_l S p m n brk)› for S n brk p m unfolding restart_prog_l_alt_def restart_abs_l_alt_def restart_required_l_def cdcl_twl_restart_l_prog_def apply (refine_vcg) subgoal by auto subgoal by (rule cdcl_twl_local_restart_l_spec_cdcl_twl_restart_l[THEN order_trans]) (auto simp: conc_fun_RES) subgoal by (auto intro: cdcl_twl_restart_only_l_list_invs simp: restart_abs_l_pre_def) subgoal by auto subgoal by auto subgoal by (rule cdcl_twl_full_restart_l_prog) auto subgoal by (rule cdcl_twl_full_restart_l_GC_prog) auto subgoal by (auto simp: cdcl_twl_restart_l_list_invs simp: restart_abs_l_pre_def) subgoal for b ba b2 b2a inp inp' by (rule cdcl_twl_full_restart_inprocess_l) subgoal by (auto simp: restart_abs_l_pre_def dest: rtranclp_cdcl_twl_restart_l_inp_twl_list_invs rtranclp_cdcl_twl_restart_l_inp_clauses_to_update_l) subgoal by (auto simp: restart_abs_l_pre_def) done then show ?thesis apply - unfolding uncurry_def apply (intro frefI nres_relI) by force qed lemma restart_prog_l_restart_abs_l2: ‹(uncurry4 restart_prog_l, uncurry4 restart_abs_l) ∈ Id ×_f nat_rel ×_f nat_rel×_f nat_rel ×_f bool_rel →_f ⟨Id ×_r nat_rel ×_r nat_rel ×_r nat_rel⟩nres_rel› (is ‹_ ∈ ?R ×_f nat_rel ×_f nat_rel×_f nat_rel ×_f bool_rel →_f _›) proof - have cdcl_twl_full_restart_l_prog: ‹cdcl_twl_full_restart_l_prog S ≤ SPEC (λT. cdcl_twl_restart_l S T)› if inv: ‹restart_abs_l_pre S last_GC last_Restart brk› and ‹(b, ba) ∈ bool_rel› and ‹b ∈ {b. b ⟶ f n < size ( S)}› and ‹ba ∈ {b. b ⟶ f n < size ( S)}› and brk: ‹¬brk› for b ba S brk n last_GC last_Restart proof - obtain T where ST: ‹(S, T) ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs T› and list_invs: ‹twl_list_invs S› and upd: ‹clauses_to_update_l S = {#}› and stgy_invs: ‹twl_stgy_invs T› and confl: ‹get_conflict_l S = None› using inv brk unfolding restart_abs_l_pre_def restart_prog_pre_def apply - apply normalize_goal+ by (auto simp: twl_st) show ?thesis using cdcl_twl_full_restart_l_prog_spec[OF ST list_invs struct_invs confl upd] remove_one_annot_true_clause_cdcl_twl_restart_l_spec[OF ST list_invs struct_invs confl upd] by (rule conc_trans_additional) qed have cdcl_twl_full_restart_l_GC_prog: ‹cdcl_twl_full_restart_l_GC_prog S ≤ SPEC (cdcl_twl_restart_l S)› if inv: ‹restart_abs_l_pre S last_GC last_Restart brk› and brk: ‹ba ∧ b2a ∧ ¬ brk› for ba b2a brk S last_GC last_Restart proof - obtain T where ST: ‹(S, T) ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs T› and list_invs: ‹twl_list_invs S› and upd: ‹clauses_to_update_l S = {#}› and stgy_invs: ‹twl_stgy_invs T› and confl: ‹get_conflict_l S = None› and inv2: ‹restart_prog_pre T last_GC last_Restart brk› using inv brk unfolding restart_abs_l_pre_def restart_prog_pre_def apply - apply normalize_goal+ by (auto simp: twl_st) show ?thesis by (rule cdcl_twl_full_restart_l_GC_prog_cdcl_twl_restart_l[unfolded Down_id_eq, OF ST list_invs struct_invs confl upd stgy_invs inv2]) qed have cdcl_twl_full_restart_inprocess_l: ‹cdcl_twl_full_restart_inprocess_l S ≤ SPEC (λT. cdcl_twl_restart_l_inp^*^* S T ∧ count_decided (get_trail_l T) = 0)› if inv: ‹restart_abs_l_pre S last_GC last_Restart brk› and brk: ‹ba ∧ b2a ∧ ¬ brk› for ba b2a brk S last_GC last_Restart proof - obtain T where ST: ‹(S, T) ∈ twl_st_l None› and struct_invs: ‹twl_struct_invs T› and list_invs: ‹twl_list_invs S› and upd: ‹clauses_to_update_l S = {#}› and stgy_invs: ‹twl_stgy_invs T› and confl: ‹get_conflict_l S = None› and inv2: ‹restart_prog_pre T last_GC last_Restart brk› using inv brk unfolding restart_abs_l_pre_def restart_prog_pre_def apply - apply normalize_goal+ by (auto simp: twl_st) show ?thesis by (rule cdcl_twl_full_restart_inprocess_l_cdcl_twl_restart_l[unfolded Down_id_eq, OF ST list_invs struct_invs confl upd stgy_invs inv2]) qed have restart_abs_l_alt_def: ‹restart_abs_l S last_GC last_Restart n brk = do { ASSERT(restart_abs_l_pre S last_GC last_Restart brk); b ← GC_required_l S last_GC n; b2 ← restart_required_l S last_Restart n; if b2 ∧ ¬brk then do { T ← SPEC(λT. cdcl_twl_restart_only_l S T); RETURN (T, last_GC, size (get_all_learned_clss_l T), n) } else if b ∧ ¬brk then do { b ← inprocessing_required_l S; if ¬b then do { _ ← SPEC(λb :: bool. True); T ← SPEC(λT. cdcl_twl_restart_l S T); RETURN (T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), n + 1) } else do { T ← SPEC(λT. cdcl_twl_restart_l_inp^*^* S T ∧ count_decided (get_trail_l T) = 0); RETURN (T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), n + 1) } } else RETURN (S, last_GC, last_Restart, n) }› for S last_GC last_Restart n brk unfolding restart_abs_l_def by (auto cong: if_cong) have [simp]: ‹cdcl_twl_restart_only_l S Ta ⟹clauses_to_update_l Ta = {#}› for S Ta by (auto simp: cdcl_twl_restart_only_l.simps) have [simp]: ‹cdcl_twl_restart_l S Ta ⟹clauses_to_update_l Ta = {#}› for S Ta by (auto simp: cdcl_twl_restart_l.simps) have ‹restart_prog_l S p m n brk ≤ ⇓ (?R ×_r nat_rel ×_r nat_rel ×_r nat_rel) (restart_abs_l S p m n brk)› for S n brk p m unfolding restart_prog_l_def restart_abs_l_alt_def restart_required_l_def cdcl_twl_restart_l_prog_def apply (refine_vcg) subgoal by auto subgoal by (rule cdcl_twl_local_restart_l_spec_cdcl_twl_restart_l[THEN order_trans]) (auto simp: conc_fun_RES) subgoal by (auto intro: cdcl_twl_restart_only_l_list_invs simp: restart_abs_l_pre_def) subgoal by auto subgoal by auto subgoal by (rule cdcl_twl_full_restart_l_prog) auto subgoal by (rule cdcl_twl_full_restart_l_GC_prog) auto subgoal by (auto simp: cdcl_twl_restart_l_list_invs simp: restart_abs_l_pre_def) subgoal by (rule cdcl_twl_full_restart_inprocess_l) auto subgoal by (auto simp: cdcl_twl_restart_l_list_invs simp: restart_abs_l_pre_def) subgoal by (auto simp: cdcl_twl_restart_l_list_invs simp: restart_abs_l_pre_def) done then show ?thesis apply - unfolding uncurry_def apply (intro frefI nres_relI) by force qed definition cdcl_twl_stgy_restart_abs_early_l :: "'v twl_st_l ⇒ 'v twl_st_l nres" where ‹cdcl_twl_stgy_restart_abs_early_l S₀ = do { ebrk ← RES UNIV; (_, brk, T, last_GC, last_Restart, n) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_l_inv S₀ o snd⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(_, brk, S, last_GC, last_Restart,n). do { T ← unit_propagation_outer_loop_l S; (brk, T) ← cdcl_twl_o_prog_l T; (T, last_GC, last_Restart,n) ← restart_abs_l T last_GC last_Restart n brk; ebrk ← RES UNIV; RETURN (ebrk, brk ∨ get_conflict_l T ≠ None, T, last_GC, last_Restart,n) }) (ebrk, False, S₀, size (get_all_learned_clss_l S₀), size (get_all_learned_clss_l S₀), 0); if ¬brk then do { (brk, T, last_GC, last_Restart, _) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_l_inv T⇖ (λ(brk, _). ¬brk) (λ(brk, S, last_GC, last_Restart, n). do { T ← unit_propagation_outer_loop_l S; (brk, T) ← cdcl_twl_o_prog_l T; (T, last_GC, last_Restart,n) ← restart_abs_l T last_GC last_Restart n brk; RETURN (brk ∨ get_conflict_l T ≠ None, T, last_GC, last_Restart, n) }) (False, T, last_GC, last_Restart, n); RETURN T } else RETURN T }› definition cdcl_twl_stgy_restart_abs_bounded_l :: "'v twl_st_l ⇒ (bool × 'v twl_st_l) nres" where ‹cdcl_twl_stgy_restart_abs_bounded_l S₀ = do { ebrk ← RES UNIV; (ebrk, brk, T, n) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_l_inv S₀ o snd⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(_, brk, S, last_GC, last_Restart, n). do { T ← unit_propagation_outer_loop_l S; (brk, T) ← cdcl_twl_o_prog_l T; (T, last_GC, last_Restart, n) ← restart_abs_l T last_GC last_Restart n brk; ebrk ← RES UNIV; RETURN (ebrk, brk ∨ get_conflict_l T ≠ None, T, last_GC, last_Restart, n) }) (ebrk, False, S₀, size (get_all_learned_clss_l S₀), size (get_all_learned_clss_l S₀), 0); RETURN (ebrk, T) }› definition cdcl_twl_stgy_restart_prog_l :: "'v twl_st_l ⇒ 'v twl_st_l nres" where ‹cdcl_twl_stgy_restart_prog_l S₀ = do { (brk, T, last_GC, last_Restart, n) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_l_inv S₀⇖ (λ(brk, _). ¬brk) (λ(brk, S, last_GC, last_Restart, n). do { T ← unit_propagation_outer_loop_l S; (brk, T) ← cdcl_twl_o_prog_l T; (T, last_GC, last_Restart, n) ← restart_prog_l T last_GC last_Restart n brk; RETURN (brk ∨ get_conflict_l T ≠ None, T, last_GC, last_Restart, n) }) (False, S₀, size (get_all_learned_clss_l S₀), size (get_all_learned_clss_l S₀), 0); RETURN T }› definition cdcl_twl_stgy_restart_prog_early_l :: "'v twl_st_l ⇒ 'v twl_st_l nres" where ‹cdcl_twl_stgy_restart_prog_early_l S₀ = do { ebrk ← RES UNIV; (ebrk, brk, T, last_GC, last_Restart, n) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_l_inv S₀ o snd⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(ebrk, brk, S, last_GC, last_Restart, n). do { T ← unit_propagation_outer_loop_l S; (brk, T) ← cdcl_twl_o_prog_l T; (T, n) ← restart_prog_l T last_GC last_Restart n brk; ebrk ← RES UNIV; RETURN (ebrk, brk ∨ get_conflict_l T ≠ None, T, n) }) (ebrk, False, S₀, size (get_all_learned_clss_l S₀), size (get_all_learned_clss_l S₀), 0); if ¬brk then do { (brk, T, n) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_l_inv T⇖ (λ(brk, _). ¬brk) (λ(brk, S, last_GC, last_Restart, n). do { T ← unit_propagation_outer_loop_l S; (brk, T) ← cdcl_twl_o_prog_l T; (T, last_GC, last_Restart, n) ← restart_prog_l T last_GC last_Restart n brk; RETURN (brk ∨ get_conflict_l T ≠ None, T, last_GC, last_Restart, n) }) (False, T, last_GC, last_Restart, n); RETURN T } else RETURN T }› lemma cdcl_twl_stgy_restart_prog_early_l_cdcl_twl_stgy_restart_abs_early_l: ‹(cdcl_twl_stgy_restart_prog_early_l, cdcl_twl_stgy_restart_abs_early_l) ∈ {(S, S'). (S, S') ∈ Id ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →_f ⟨Id⟩ nres_rel› (is ‹_ ∈ ?R →_f _›) proof - have [refine0]: ‹((False, S, 0), (False, T , 0)) ∈ bool_rel ×_r ?R ×_r nat_rel› if ‹(S, T) ∈ ?R› for S T using that by auto have [refine0]: ‹unit_propagation_outer_loop_l x1c ≤ ⇓ Id (unit_propagation_outer_loop_l x1a)› if ‹(x1c, x1a) ∈ Id› for x1c x1a using that by auto have [refine0]: ‹cdcl_twl_o_prog_l x1c ≤ ⇓ Id (cdcl_twl_o_prog_l x1a)› if ‹(x1c, x1a) ∈ Id› for x1c x1a using that by auto show ?thesis unfolding cdcl_twl_stgy_restart_prog_early_l_def cdcl_twl_stgy_restart_prog_def uncurry_def cdcl_twl_stgy_restart_abs_early_l_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R = ‹bool_rel ×_r Id ×_r nat_rel ×_r nat_rel ×_r nat_rel›] WHILEIT_refine[where R = ‹bool_rel ×_r bool_rel ×_r Id ×_r nat_rel ×_r nat_rel ×_r nat_rel› ] unit_propagation_outer_loop_l_spec[THEN fref_to_Down] cdcl_twl_o_prog_l_spec[THEN fref_to_Down] restart_abs_l_restart_prog[THEN fref_to_Down_curry2] restart_prog_l_restart_abs_l2[THEN fref_to_Down_curry4]) subgoal by auto subgoal by auto subgoal for x y xa x' x1 x2 x1a x2a by fastforce subgoal by auto subgoal by (simp add: twl_st) subgoal by (auto simp: twl_st) subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def cdcl_twl_stgy_restart_abs_l_inv_def by (auto simp: twl_st) subgoal by auto subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def cdcl_twl_stgy_restart_abs_l_inv_def by (auto simp: twl_st) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed lemma cdcl_twl_stgy_restart_prog_l_cdcl_twl_stgy_restart_abs_l: ‹(cdcl_twl_stgy_restart_prog_l, cdcl_twl_stgy_restart_abs_l) ∈ {(S, S'). (S, S') ∈ Id ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →_f ⟨Id⟩ nres_rel› (is ‹_ ∈ ?R →_f _›) proof - have [refine0]: ‹((False, S, 0), (False, T , 0)) ∈ bool_rel ×_r ?R ×_r nat_rel› if ‹(S, T) ∈ ?R› for S T using that by auto have [refine0]: ‹unit_propagation_outer_loop_l x1c ≤ ⇓ Id (unit_propagation_outer_loop_l x1a)› if ‹(x1c, x1a) ∈ Id› for x1c x1a using that by auto have [refine0]: ‹cdcl_twl_o_prog_l x1c ≤ ⇓ Id (cdcl_twl_o_prog_l x1a)› if ‹(x1c, x1a) ∈ Id› for x1c x1a using that by auto show ?thesis unfolding cdcl_twl_stgy_restart_prog_l_def cdcl_twl_stgy_restart_prog_def uncurry_def cdcl_twl_stgy_restart_abs_l_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R = ‹bool_rel ×_r Id ×_r nat_rel ×_r nat_rel ×_r nat_rel›] unit_propagation_outer_loop_l_spec[THEN fref_to_Down] cdcl_twl_o_prog_l_spec[THEN fref_to_Down] restart_abs_l_restart_prog[THEN fref_to_Down_curry4] restart_prog_l_restart_abs_l2[THEN fref_to_Down_curry4]) subgoal by auto subgoal unfolding cdcl_twl_stgy_restart_abs_l_inv_def by (fastforce simp: prod_rel_fst_snd_iff) subgoal for x y xa x' x1 x2 x1a x2a by fastforce subgoal by auto subgoal by (auto simp add: twl_st) subgoal by (auto simp: twl_st) subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def cdcl_twl_stgy_restart_abs_l_inv_def by (auto simp: twl_st) done qed lemma (in twl_restart) cdcl_twl_stgy_restart_prog_l_cdcl_twl_stgy_restart_prog: ‹(cdcl_twl_stgy_restart_prog_l, cdcl_twl_stgy_restart_prog) ∈ {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →_f ⟨{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S}⟩nres_rel› apply (intro frefI nres_relI) apply (rule order_trans) defer apply (rule cdcl_twl_stgy_restart_abs_l_cdcl_twl_stgy_restart_abs_l[THEN fref_to_Down]) apply fast apply assumption apply (rule cdcl_twl_stgy_restart_prog_l_cdcl_twl_stgy_restart_abs_l[THEN fref_to_Down, simplified]) apply simp done definition cdcl_twl_stgy_restart_prog_bounded_l :: "'v twl_st_l ⇒ (bool × 'v twl_st_l) nres" where ‹cdcl_twl_stgy_restart_prog_bounded_l S₀ = do { ebrk ← RES UNIV; (ebrk, brk, T, last_GC, last_Restart, n) ← WHILE_T⇗cdcl_twl_stgy_restart_abs_l_inv S₀ o snd⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(ebrk, brk, S, last_GC, last_Restart, n). do { T ← unit_propagation_outer_loop_l S; (brk, T) ← cdcl_twl_o_prog_l T; (T, last_GC, last_Restart, n) ← restart_prog_l T last_GC last_Restart n brk; ebrk ← RES UNIV; RETURN (ebrk, brk ∨ get_conflict_l T ≠ None, T, last_GC, last_Restart, n) }) (ebrk, False, S₀, size (get_all_learned_clss_l S₀), size (get_all_learned_clss_l S₀), 0); RETURN (ebrk, T) }› lemma (in -) [simp]: ‹(S, T) ∈ twl_st_l b ⟹ size (get_learned_clss T) = size (get_learned_clss_l S)› ‹(S, T) ∈ twl_st_l b ⟹ (get_init_learned_clss T) = (get_unit_learned_clss_l S)› by (auto simp: twl_st_l_def get_learned_clss_l_def) lemma (in -) get_all_learned_clss_alt_def: ‹get_all_learned_clss S = clauses (get_learned_clss S) + get_init_learned_clss S + subsumed_learned_clauses S + get_learned_clauses0 S› by (cases S) auto lemma cdcl_twl_stgy_restart_abs_bounded_l_cdcl_twl_stgy_restart_abs_bounded_l: ‹(cdcl_twl_stgy_restart_abs_bounded_l, cdcl_twl_stgy_restart_prog_bounded) ∈ {(S :: 'v twl_st_l, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →_f ⟨bool_rel ×_r {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S}⟩ nres_rel› unfolding cdcl_twl_stgy_restart_abs_bounded_l_def cdcl_twl_stgy_restart_prog_bounded_def uncurry_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R = ‹bool_rel ×_r bool_rel ×_r {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} ×_r nat_rel ×_r nat_rel ×_r nat_rel›] unit_propagation_outer_loop_l_spec[THEN fref_to_Down] cdcl_twl_o_prog_l_spec[THEN fref_to_Down] restart_abs_l_restart_prog[THEN fref_to_Down_curry4]) subgoal by (auto simp add: get_all_learned_clss_alt_def) subgoal for x y ebrk ebrka xa x' unfolding cdcl_twl_stgy_restart_abs_l_inv_def comp_def case_prod_beta apply (rule_tac x=y in exI) apply (rule_tac x=‹fst (snd (snd x'))› in exI) by (auto simp: prod_rel_fst_snd_iff) subgoal by (auto simp: prod_rel_fst_snd_iff) subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def cdcl_twl_stgy_restart_abs_l_inv_def apply (simp only: prod.case) apply (normalize_goal)+ by (simp add: twl_st_l twl_st) subgoal by (auto simp: twl_st_l twl_st) subgoal by auto subgoal by (auto simp: twl_st_l twl_st) subgoal by (auto simp: prod_rel_fst_snd_iff) done lemma cdcl_twl_stgy_restart_abs_early_l_cdcl_twl_stgy_restart_abs_early: ‹(cdcl_twl_stgy_restart_abs_early_l, cdcl_twl_stgy_restart_prog_early) ∈ {(S :: 'v twl_st_l, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →_f ⟨twl_st_l None⟩nres_rel› proof - show ?thesis unfolding cdcl_twl_stgy_restart_abs_early_l_def cdcl_twl_stgy_restart_prog_early_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R = ‹bool_rel ×_r bool_rel ×_r {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} ×_r nat_rel ×_r nat_rel ×_r nat_rel›] unit_propagation_outer_loop_l_spec[THEN fref_to_Down] cdcl_twl_o_prog_l_spec[THEN fref_to_Down] restart_abs_l_restart_prog[THEN fref_to_Down_curry4] WHILEIT_refine[where R = ‹bool_rel ×_r {(S :: 'v twl_st_l, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} ×_r nat_rel ×_r nat_rel ×_r nat_rel›]) subgoal by (auto simp add: get_all_learned_clss_alt_def) subgoal for x y ebrk ebrka xa x' unfolding cdcl_twl_stgy_restart_abs_l_inv_def comp_def case_prod_beta apply (rule_tac x=y in exI) apply (rule_tac x=‹fst (snd (snd x'))› in exI) by (auto simp: prod_rel_fst_snd_iff) subgoal by (auto simp: prod_rel_fst_snd_iff) subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def cdcl_twl_stgy_restart_abs_l_inv_def apply (simp only: prod.case) apply (normalize_goal)+ by (simp add: twl_st_l twl_st) subgoal by (auto simp: twl_st_l twl_st) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal for x y ebrk ebrka xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g x1h x2h x1i x2i xb x'a unfolding cdcl_twl_stgy_restart_abs_l_inv_def comp_def case_prod_beta apply (rule_tac x= ‹x1b› in exI) apply (rule_tac x=‹fst (snd x'a)› in exI) apply (rule_tac x= ‹x2d› in exI) by (auto simp: prod_rel_fst_snd_iff) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed lemma cdcl_twl_stgy_restart_prog_bounded_l_cdcl_twl_stgy_restart_abs_bounded_l: ‹(cdcl_twl_stgy_restart_prog_bounded_l, cdcl_twl_stgy_restart_abs_bounded_l) ∈ {(S, S'). (S:: 'v twl_st_l, S') ∈ Id ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →_f ⟨Id⟩ nres_rel› (is ‹_ ∈ ?R →_f _›) proof - have [refine0]: ‹((ebrk, False, S, size (get_all_learned_clss_l S), size (get_all_learned_clss_l S), 0::nat), ebrka, False, T, size (get_all_learned_clss_l T), size (get_all_learned_clss_l T), 0::nat) ∈ bool_rel ×_r bool_rel ×_r ?R ×_r nat_rel ×_r nat_rel ×_r nat_rel› if ‹(S, T) ∈ ?R› ‹(ebrk, ebrka) ∈ bool_rel› for S T ebrk ebrka using that by auto have [refine0]: ‹unit_propagation_outer_loop_l x1c ≤ ⇓ Id (unit_propagation_outer_loop_l x1a)› if ‹(x1c, x1a) ∈ Id› for x1c x1a using that by auto have [refine0]: ‹cdcl_twl_o_prog_l x1c ≤ ⇓ Id (cdcl_twl_o_prog_l x1a)› if ‹(x1c, x1a) ∈ Id› for x1c x1a using that by auto show ?thesis supply [simp] = prod_rel_fst_snd_iff unfolding cdcl_twl_stgy_restart_prog_bounded_l_def cdcl_twl_stgy_restart_prog_def uncurry_def cdcl_twl_stgy_restart_abs_bounded_l_def apply (intro frefI nres_relI) apply (refine_rcg WHILEIT_refine[where R = ‹bool_rel ×_r bool_rel ×_r Id ×_r nat_rel ×_r nat_rel ×_r nat_rel›] WHILEIT_refine[where R = ‹bool_rel ×_r Id ×_r nat_rel ×_r nat_rel ×_r nat_rel› ] unit_propagation_outer_loop_l_spec[THEN fref_to_Down] cdcl_twl_o_prog_l_spec[THEN fref_to_Down] restart_prog_l_restart_abs_l2[THEN fref_to_Down_curry4]) subgoal by auto subgoal by fastforce subgoal by auto subgoal by (simp add: twl_st) subgoal by (auto simp: twl_st) subgoal by auto subgoal by auto done qed lemma (in twl_restart) cdcl_twl_stgy_restart_prog_bounded_l_cdcl_twl_stgy_restart_prog_bounded: ‹(cdcl_twl_stgy_restart_prog_bounded_l, cdcl_twl_stgy_restart_prog_bounded) ∈ {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →_f ⟨bool_rel ×_r {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S}⟩nres_rel› apply (intro frefI nres_relI) apply (rule order_trans) defer apply (rule cdcl_twl_stgy_restart_abs_bounded_l_cdcl_twl_stgy_restart_abs_bounded_l[THEN fref_to_Down]) apply fast apply assumption apply (rule cdcl_twl_stgy_restart_prog_bounded_l_cdcl_twl_stgy_restart_abs_bounded_l[THEN fref_to_Down, simplified]) apply simp done end end

Theory Watched_Literals_List_Simp