theory IsaSAT_Restart imports IsaSAT_Restart_Heuristics IsaSAT_CDCL begin chapter ‹Full CDCL with Restarts› definition cdcl_twl_stgy_restart_abs_wl_heur_inv where ‹cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0 brk T n ⟷ (∃S⇩0' T'. (S⇩0, S⇩0') ∈ twl_st_heur ∧ (T, T') ∈ twl_st_heur ∧ cdcl_twl_stgy_restart_abs_wl_inv S⇩0' brk T' n)› definition cdcl_twl_stgy_restart_prog_wl_heur :: "twl_st_wl_heur ⇒ twl_st_wl_heur nres" where ‹cdcl_twl_stgy_restart_prog_wl_heur S⇩0 = do { (brk, T, _) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0 brk T n⇖ (λ(brk, _). ¬brk) (λ(brk, S, n). do { T ← unit_propagation_outer_loop_wl_D_heur S; (brk, T) ← cdcl_twl_o_prog_wl_D_heur T; (T, n) ← restart_prog_wl_D_heur T n brk; RETURN (brk, T, n) }) (False, S⇩0::twl_st_wl_heur, 0); RETURN T }› lemma cdcl_twl_stgy_restart_prog_wl_heur_cdcl_twl_stgy_restart_prog_wl_D: ‹(cdcl_twl_stgy_restart_prog_wl_heur, cdcl_twl_stgy_restart_prog_wl) ∈ twl_st_heur →⇩f ⟨twl_st_heur⟩nres_rel› proof - show ?thesis unfolding cdcl_twl_stgy_restart_prog_wl_heur_def cdcl_twl_stgy_restart_prog_wl_def apply (intro frefI nres_relI) apply (refine_rcg restart_prog_wl_D_heur_restart_prog_wl_D2[THEN fref_to_Down_curry2] cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D2[THEN fref_to_Down] cdcl_twl_stgy_prog_wl_D_heur_cdcl_twl_stgy_prog_wl_D[THEN fref_to_Down] unit_propagation_outer_loop_wl_D_heur_unit_propagation_outer_loop_wl_D[THEN fref_to_Down] WHILEIT_refine[where R = ‹bool_rel ×⇩r twl_st_heur ×⇩r nat_rel›]) subgoal by auto subgoal unfolding cdcl_twl_stgy_restart_abs_wl_heur_inv_def by fastforce subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed definition fast_number_of_iterations :: ‹_ ⇒ bool› where ‹fast_number_of_iterations n ⟷ n < uint64_max >> 1› definition isasat_fast_slow :: ‹twl_st_wl_heur ⇒ twl_st_wl_heur nres› where [simp]: ‹isasat_fast_slow S = RETURN S› definition cdcl_twl_stgy_restart_prog_early_wl_heur :: "twl_st_wl_heur ⇒ twl_st_wl_heur nres" where ‹cdcl_twl_stgy_restart_prog_early_wl_heur S⇩0 = do { ebrk ← RETURN (¬isasat_fast S⇩0); (ebrk, brk, T, n) ← WHILE⇩T⇗λ(ebrk, brk, T, n). cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0 brk T n ∧ (¬ebrk ⟶isasat_fast T) ∧ length (get_clauses_wl_heur T) ≤ uint64_max⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(ebrk, brk, S, n). do { ASSERT(¬brk ∧ ¬ebrk); ASSERT(length (get_clauses_wl_heur S) ≤ uint64_max); T ← unit_propagation_outer_loop_wl_D_heur S; ASSERT(length (get_clauses_wl_heur T) ≤ uint64_max); ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S)); (brk, T) ← cdcl_twl_o_prog_wl_D_heur T; ASSERT(length (get_clauses_wl_heur T) ≤ uint64_max); (T, n) ← restart_prog_wl_D_heur T n brk; ebrk ← RETURN (¬isasat_fast T); RETURN (ebrk, brk, T, n) }) (ebrk, False, S⇩0::twl_st_wl_heur, 0); ASSERT(length (get_clauses_wl_heur T) ≤ uint64_max ∧ get_old_arena T = []); if ¬brk then do { T ← isasat_fast_slow T; (brk, T, _) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0 brk T n⇖ (λ(brk, _). ¬brk) (λ(brk, S, n). do { T ← unit_propagation_outer_loop_wl_D_heur S; (brk, T) ← cdcl_twl_o_prog_wl_D_heur T; (T, n) ← restart_prog_wl_D_heur T n brk; RETURN (brk, T, n) }) (False, T, n); RETURN T } else isasat_fast_slow T }› lemma cdcl_twl_stgy_restart_prog_early_wl_heur_cdcl_twl_stgy_restart_prog_early_wl_D: assumes r: ‹r ≤ uint64_max› shows ‹(cdcl_twl_stgy_restart_prog_early_wl_heur, cdcl_twl_stgy_restart_prog_early_wl) ∈ twl_st_heur''' r →⇩f ⟨twl_st_heur⟩nres_rel› proof - have cdcl_twl_stgy_restart_prog_early_wl_alt_def: ‹cdcl_twl_stgy_restart_prog_early_wl S⇩0 = do { ebrk ← RES UNIV; (ebrk, brk, T, n) ← WHILE⇩T⇗λ(_, brk, T, n). cdcl_twl_stgy_restart_abs_wl_inv S⇩0 brk T n⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(_, brk, S, n). do { T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, n) ← restart_prog_wl T n brk; ebrk ← RES UNIV; RETURN (ebrk, brk, T, n) }) (ebrk, False, S⇩0::nat twl_st_wl, 0); if ¬brk then do { T ← RETURN T; (brk, T, _) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_abs_wl_inv S⇩0 brk T n⇖ (λ(brk, _). ¬brk) (λ(brk, S, n). do { T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, n) ← restart_prog_wl T n brk; RETURN (brk, T, n) }) (False, T::nat twl_st_wl, n); RETURN T } else RETURN T }› for S⇩0 unfolding cdcl_twl_stgy_restart_prog_early_wl_def nres_monad1 by auto have [refine0]: ‹RETURN (¬isasat_fast x) ≤ ⇓ {(b, b'). b = b' ∧ (b = (¬isasat_fast x))} (RES UNIV)› for x by (auto intro: RETURN_RES_refine) have [refine0]: ‹isasat_fast_slow x1e ≤ ⇓ {(S, S'). S = x1e ∧ S' = x1b} (RETURN x1b)› for x1e x1b proof - show ?thesis unfolding isasat_fast_slow_def by auto qed have twl_st_heur'': ‹(x1e, x1b) ∈ twl_st_heur ⟹ (x1e, x1b) ∈ twl_st_heur'' (dom_m (get_clauses_wl x1b)) (length (get_clauses_wl_heur x1e))› for x1e x1b by (auto simp: twl_st_heur'_def) have twl_st_heur''': ‹(x1e, x1b) ∈ twl_st_heur'' 𝒟 r ⟹ (x1e, x1b) ∈ twl_st_heur''' r› for x1e x1b r 𝒟 by (auto simp: twl_st_heur'_def) have H: ‹(xb, x'a) ∈ bool_rel ×⇩f twl_st_heur'''' (length (get_clauses_wl_heur x1e) + 6 + uint32_max div 2) ⟹ x'a = (x1f, x2f) ⟹ xb = (x1g, x2g) ⟹ (x1g, x1f) ∈ bool_rel ⟹ (x2e, x2b) ∈ nat_rel ⟹ (((x2g, x2e), x1g), (x2f, x2b), x1f) ∈ twl_st_heur''' (length (get_clauses_wl_heur x2g)) ×⇩f nat_rel ×⇩f bool_rel› for x y ebrk ebrka xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e T Ta xb x'a x1f x2f x1g x2g by auto have abs_inv: ‹(x, y) ∈ twl_st_heur''' r ⟹ (ebrk, ebrka) ∈ {(b, b'). b = b' ∧ b = (¬ isasat_fast x)} ⟹ (xb, x'a) ∈ bool_rel ×⇩f (twl_st_heur ×⇩f nat_rel) ⟹ case x'a of (brk, xa, xb) ⇒ cdcl_twl_stgy_restart_abs_wl_inv y brk xa xb ⟹ x2f = (x1g, x2g) ⟹ xb = (x1f, x2f) ⟹ cdcl_twl_stgy_restart_abs_wl_heur_inv x x1f x1g x2g› for x y ebrk ebrka xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e T Ta xb x'a x1f x2f x1g x2g unfolding cdcl_twl_stgy_restart_abs_wl_heur_inv_def by fastforce show ?thesis supply[[goals_limit=1]] isasat_fast_length_leD[dest] twl_st_heur'_def[simp] unfolding cdcl_twl_stgy_restart_prog_early_wl_heur_def cdcl_twl_stgy_restart_prog_early_wl_alt_def apply (intro frefI nres_relI) apply (refine_rcg restart_prog_wl_D_heur_restart_prog_wl_D[THEN fref_to_Down_curry2] cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D[THEN fref_to_Down] unit_propagation_outer_loop_wl_D_heur_unit_propagation_outer_loop_wl_D'[THEN fref_to_Down] WHILEIT_refine[where R = ‹bool_rel ×⇩r twl_st_heur ×⇩r nat_rel›] WHILEIT_refine[where R = ‹{((ebrk, brk, T,n), (ebrk', brk', T', n')). (ebrk = ebrk') ∧ (brk = brk') ∧ (T, T') ∈ twl_st_heur ∧ n = n' ∧ (¬ebrk ⟶ isasat_fast T) ∧ length (get_clauses_wl_heur T) ≤ uint64_max}›]) subgoal using r by auto subgoal unfolding cdcl_twl_stgy_restart_abs_wl_heur_inv_def by fast subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by fast subgoal by auto apply (rule twl_st_heur''; auto; fail) subgoal by auto subgoal by auto apply (rule twl_st_heur'''; assumption) subgoal by (auto simp: isasat_fast_def uint64_max_def sint64_max_def uint32_max_def) apply (rule H; assumption?) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (subst (asm)(2) twl_st_heur_def) force subgoal by auto subgoal by auto subgoal by (rule abs_inv) subgoal by auto apply (rule twl_st_heur''; auto; fail) apply (rule twl_st_heur'''; assumption) apply (rule H; assumption?) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: isasat_fast_slow_def) done qed lemma mark_unused_st_heur: assumes ‹(S, T) ∈ twl_st_heur_restart› and ‹C ∈# dom_m (get_clauses_wl T)› shows ‹(mark_unused_st_heur C S, T) ∈ twl_st_heur_restart› using assms apply (cases S; cases T) apply (simp add: twl_st_heur_restart_def mark_unused_st_heur_def all_init_atms_def[symmetric]) apply (auto simp: twl_st_heur_restart_def mark_garbage_heur_def mark_garbage_wl_def learned_clss_l_l_fmdrop size_remove1_mset_If simp: all_init_atms_def all_init_lits_def simp del: all_init_atms_def[symmetric] intro!: valid_arena_mark_unused valid_arena_arena_decr_act dest!: in_set_butlastD in_vdom_m_fmdropD elim!: in_set_upd_cases) done lemma mark_to_delete_clauses_wl_D_heur_is_Some_iff: ‹D = Some C ⟷ D ≠ None ∧ ((the D) = C)› by auto lemma (in -) isasat_fast_alt_def: ‹RETURN o isasat_fast = (λ(M, N, _). RETURN (length N ≤ sint64_max - (uint32_max div 2 + 6)))› unfolding isasat_fast_def by (auto intro!:ext) definition cdcl_twl_stgy_restart_prog_bounded_wl_heur :: "twl_st_wl_heur ⇒ (bool × twl_st_wl_heur) nres" where ‹cdcl_twl_stgy_restart_prog_bounded_wl_heur S⇩0 = do { ebrk ← RETURN (¬isasat_fast S⇩0); (ebrk, brk, T, n) ← WHILE⇩T⇗λ(ebrk, brk, T, n). cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0 brk T n ∧ (¬ebrk ⟶isasat_fast T ∧ n < uint64_max) ∧ (¬ebrk ⟶length (get_clauses_wl_heur T) ≤ sint64_max)⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(ebrk, brk, S, n). do { ASSERT(¬brk ∧ ¬ebrk); ASSERT(length (get_clauses_wl_heur S) ≤ sint64_max); T ← unit_propagation_outer_loop_wl_D_heur S; ASSERT(length (get_clauses_wl_heur T) ≤ sint64_max); ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S)); (brk, T) ← cdcl_twl_o_prog_wl_D_heur T; ASSERT(length (get_clauses_wl_heur T) ≤ sint64_max); (T, n) ← restart_prog_wl_D_heur T n brk; ebrk ← RETURN (¬(isasat_fast T ∧ n < uint64_max)); RETURN (ebrk, brk, T, n) }) (ebrk, False, S⇩0::twl_st_wl_heur, 0); RETURN (brk, T) }› lemma cdcl_twl_stgy_restart_prog_bounded_wl_heur_cdcl_twl_stgy_restart_prog_bounded_wl_D: assumes r: ‹r ≤ uint64_max› shows ‹(cdcl_twl_stgy_restart_prog_bounded_wl_heur, cdcl_twl_stgy_restart_prog_bounded_wl) ∈ twl_st_heur''' r →⇩f ⟨bool_rel ×⇩r twl_st_heur⟩nres_rel› proof - have cdcl_twl_stgy_restart_prog_bounded_wl_alt_def: ‹cdcl_twl_stgy_restart_prog_bounded_wl S⇩0 = do { ebrk ← RES UNIV; (ebrk, brk, T, n) ← WHILE⇩T⇗λ(_, brk, T, n). cdcl_twl_stgy_restart_abs_wl_inv S⇩0 brk T n⇖ (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk) (λ(_, brk, S, n). do { T ← unit_propagation_outer_loop_wl S; (brk, T) ← cdcl_twl_o_prog_wl T; (T, n) ← restart_prog_wl T n brk; ebrk ← RES UNIV; RETURN (ebrk, brk, T, n) }) (ebrk, False, S⇩0::nat twl_st_wl, 0); RETURN (brk, T) }› for S⇩0 unfolding cdcl_twl_stgy_restart_prog_bounded_wl_def nres_monad1 by auto have [refine0]: ‹RETURN (¬(isasat_fast x ∧ n < uint64_max)) ≤ ⇓ {(b, b'). b = b' ∧ (b = (¬(isasat_fast x ∧ n < uint64_max)))} (RES UNIV)› ‹RETURN (¬isasat_fast x) ≤ ⇓ {(b, b'). b = b' ∧ (b = (¬(isasat_fast x ∧ 0 < uint64_max)))} (RES UNIV)› for x n by (auto intro: RETURN_RES_refine simp: uint64_max_def) have [refine0]: ‹isasat_fast_slow x1e ≤ ⇓ {(S, S'). S = x1e ∧ S' = x1b} (RETURN x1b)› for x1e x1b proof - show ?thesis unfolding isasat_fast_slow_def by auto qed have twl_st_heur'': ‹(x1e, x1b) ∈ twl_st_heur ⟹ (x1e, x1b) ∈ twl_st_heur'' (dom_m (get_clauses_wl x1b)) (length (get_clauses_wl_heur x1e))› for x1e x1b by (auto simp: twl_st_heur'_def) have twl_st_heur''': ‹(x1e, x1b) ∈ twl_st_heur'' 𝒟 r ⟹ (x1e, x1b) ∈ twl_st_heur''' r› for x1e x1b r 𝒟 by (auto simp: twl_st_heur'_def) have H: ‹(xb, x'a) ∈ bool_rel ×⇩f twl_st_heur'''' (length (get_clauses_wl_heur x1e) + 6 + uint32_max div 2) ⟹ x'a = (x1f, x2f) ⟹ xb = (x1g, x2g) ⟹ (x1g, x1f) ∈ bool_rel ⟹ (x2e, x2b) ∈ nat_rel ⟹ (((x2g, x2e), x1g), (x2f, x2b), x1f) ∈ twl_st_heur''' (length (get_clauses_wl_heur x2g)) ×⇩f nat_rel ×⇩f bool_rel› for x y ebrk ebrka xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e T Ta xb x'a x1f x2f x1g x2g by auto have abs_inv: ‹(x, y) ∈ twl_st_heur''' r ⟹ (ebrk, ebrka) ∈ {(b, b'). b = b' ∧ b = (¬ isasat_fast x ∧ x2g < uint64_max)} ⟹ (xb, x'a) ∈ bool_rel ×⇩f (twl_st_heur ×⇩f nat_rel) ⟹ case x'a of (brk, xa, xb) ⇒ cdcl_twl_stgy_restart_abs_wl_inv y brk xa xb ⟹ x2f = (x1g, x2g) ⟹ xb = (x1f, x2f) ⟹ cdcl_twl_stgy_restart_abs_wl_heur_inv x x1f x1g x2g› for x y ebrk ebrka xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e T Ta xb x'a x1f x2f x1g x2g unfolding cdcl_twl_stgy_restart_abs_wl_heur_inv_def apply (rule_tac x=y in exI) by fastforce show ?thesis supply[[goals_limit=1]] isasat_fast_length_leD[dest] twl_st_heur'_def[simp] unfolding cdcl_twl_stgy_restart_prog_bounded_wl_heur_def cdcl_twl_stgy_restart_prog_bounded_wl_alt_def apply (intro frefI nres_relI) apply (refine_rcg restart_prog_wl_D_heur_restart_prog_wl_D[THEN fref_to_Down_curry2] cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D[THEN fref_to_Down] unit_propagation_outer_loop_wl_D_heur_unit_propagation_outer_loop_wl_D'[THEN fref_to_Down] WHILEIT_refine[where R = ‹{((ebrk, brk, T,n), (ebrk', brk', T', n')). (ebrk = ebrk') ∧ (brk = brk') ∧ (T, T') ∈ twl_st_heur ∧ n = n' ∧ (¬ebrk ⟶ isasat_fast T ∧ n < uint64_max) ∧ (¬ebrk ⟶ length (get_clauses_wl_heur T) ≤ sint64_max)}›]) subgoal using r by (auto simp: sint64_max_def isasat_fast_def uint32_max_def) subgoal unfolding cdcl_twl_stgy_restart_abs_wl_heur_inv_def by fast subgoal by auto subgoal by auto subgoal by (auto simp: sint64_max_def isasat_fast_def uint32_max_def) subgoal by auto subgoal by fast subgoal by auto subgoal by auto apply (rule twl_st_heur''; auto; fail) subgoal by auto subgoal by auto apply (rule twl_st_heur'''; assumption) subgoal by (auto simp: isasat_fast_def uint64_max_def uint32_max_def sint64_max_def) apply (rule H; assumption?) subgoal by auto subgoal by auto subgoal by auto subgoal by auto done qed end