Theory IsaSAT_Restart_Simp
theory IsaSAT_Restart_Simp
imports IsaSAT_Restart_Heuristics IsaSAT_Other IsaSAT_Propagate_Conflict IsaSAT_Restart_Inprocessing
IsaSAT_Restart_Simp_Defs
begin
fun Pair4 :: ‹'a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'a × 'b × 'c × 'd› where
‹Pair4 a b c d = (a, b, c, d)›
lemma rephase_heur_st_spec:
‹(S, S') ∈ twl_st_heur_loop ⟹ rephase_heur_st S ≤ SPEC(λS. (S, S') ∈ twl_st_heur_loop)›
unfolding rephase_heur_st_def
apply (cases S')
apply (refine_vcg rephase_heur_spec[THEN order_trans, of ‹all_atms_st S'›])
apply (simp_all add: twl_st_heur_loop_def all_atms_st_def)
done
lemma update_all_phases_Pair:
‹(S, S') ∈ twl_st_heur_loop''''uu r u⟹
update_all_phases S ≤ ⇓ ({(T, T'). (T,T')∈twl_st_heur_loop''''uu r u ∧ T' = S'}) (RETURN (id S'))›
proof -
have [refine0]: ‹(S, S') ∈ twl_st_heur_loop''''uu r u ⟹ count_decided (get_trail_wl S') = 0 ⟹
update_restart_phases S ≤ SPEC(λS. (S, S') ∈ twl_st_heur_loop''''uu r u)›
for S :: isasat and S' :: ‹nat twl_st_wl›
unfolding update_all_phases_def update_restart_phases_def Let_def
by (auto simp: twl_st_heur'_def twl_st_heur_loop_def learned_clss_count_def
intro!: rephase_heur_st_spec[THEN order_trans] switch_bump_heur
simp del: incr_restart_phase_end_stats.simps incr_restart_phase_stats.simps)
have [refine0]: ‹(S, S') ∈ twl_st_heur_loop''''uu r u ⟹ rephase_heur_st S ≤ SPEC(λS. (S, S') ∈ twl_st_heur_loop''''uu r u)›
for S :: isasat and S' :: ‹nat twl_st_wl›
unfolding update_all_phases_def rephase_heur_st_def
apply (cases S')
apply (refine_vcg rephase_heur_spec[THEN order_trans, of ‹all_atms_st S'›])
apply (clarsimp simp: twl_st_heur'_def twl_st_heur_loop_def learned_clss_count_def)
apply (simp add: learned_clss_count_def)
apply (clarsimp simp add: twl_st_heur_loop_def learned_clss_count_def)
done
show ‹(S, S') ∈ twl_st_heur_loop''''uu r u⟹
update_all_phases S ≤ ⇓ ({(T, T'). (T,T')∈twl_st_heur_loop''''uu r u ∧ T' = S'}) (RETURN (id S'))› for S S'
unfolding update_all_phases_def
apply (subst (1) bind_to_let_conv)
apply (subst (1) Let_def)
apply (subst (1) Let_def)
apply refine_vcg
apply assumption
subgoal
using count_decided_trail_ref[THEN fref_to_Down_unRET_Id, of ‹get_trail_wl_heur S›
‹get_trail_wl S'› ‹all_atms_st S'›]
by (simp add: count_decided_st_def twl_st_heur_loop_def count_decided_st_heur_def Let_def)
apply assumption
subgoal by simp
subgoal by simp
apply assumption
subgoal by simp
subgoal by simp
subgoal by simp
done
qed
lemma cdcl_twl_stgy_restart_abs_wl_inv_NoneD:
‹cdcl_twl_stgy_restart_abs_wl_inv y (False, x1a, x1b, x1c, x2c) ⟹
get_conflict_wl x1a = None›
unfolding cdcl_twl_stgy_restart_abs_wl_inv_def cdcl_twl_stgy_restart_abs_l_inv_def
prod.simps cdcl_twl_stgy_restart_prog_inv_def cdcl_twl_stgy_restart_prog_int_inv_def
unfolding not_False_eq_True simp_thms
apply normalize_goal+
by simp
lemma get_conflict_wl_is_None_heur_get_conflict_wl_is_None:
‹(RETURN o get_conflict_wl_is_None_heur, RETURN o get_conflict_wl_is_None) ∈
twl_st_heur_loop →⇩f ⟨Id⟩nres_rel›
unfolding get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def comp_def
apply (intro frefI nres_relI) apply refine_rcg
by (auto simp: twl_st_heur_loop_def get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def
option_lookup_clause_rel_def
split: option.splits)
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_loop⟩nres_rel›
proof -
have [refine0]: ‹(x1e, x1a) ∈ twl_st_heur ⟹ (x1e, x1a)
∈ {(S, T).
(S, T) ∈ twl_st_heur ∧
get_learned_count S = get_learned_count x1e}› for x1e x1a
by auto
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_curry4]
cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D2[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 restart_prog_wl_heur_rel2›])
subgoal by (auto simp: learned_clss_count_twl_st_heur intro!: twl_st_heur_twl_st_heur_loopD)
subgoal for x y xa x'
using cdcl_twl_stgy_restart_abs_wl_inv_NoneD[of y ‹fst (snd x')›
‹fst (snd (snd x'))› ‹fst (snd (snd (snd x')))› ‹snd (snd (snd (snd x')))›] apply -
unfolding cdcl_twl_stgy_restart_abs_wl_heur_inv_def prod_rel_fst_snd_iff case_prod_beta
apply (rule_tac x = ‹y› in exI)
apply (rule_tac x = ‹fst (snd x')› in exI)
apply (cases x', cases xa)
by auto
subgoal by auto
subgoal
by (rule twl_st_heur_loop_twl_st_heurD)
(auto dest: cdcl_twl_stgy_restart_abs_wl_inv_NoneD)
subgoal by auto
subgoal by (auto dest!: cdcl_twl_stgy_restart_abs_wl_inv_NoneD)
subgoal unfolding get_conflict_wl_is_None
by (auto simp: get_conflict_wl_is_None_heur_get_conflict_wl_is_None[THEN fref_to_Down_unRET_Id])
subgoal by auto
done
qed
definition fast_number_of_iterations :: ‹_ ⇒ bool› where
‹fast_number_of_iterations n ⟷ n < unat64_max >> 1›
definition convert_to_full_state_wl_heur :: ‹isasat ⇒ isasat nres› where
[simp]: ‹convert_to_full_state_wl_heur S = RETURN S›
definition convert_to_full_state_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
[simp]: ‹convert_to_full_state_wl S = RETURN S›
lemma convert_to_full_state_wl_heur:
‹(S, T) ∈ twl_st_heur_loop ⟹ get_conflict_wl T = None ⟹
convert_to_full_state_wl_heur S ≤ ⇓(twl_st_heur''
(dom_m (get_clauses_wl T))
(length (get_clauses_wl_heur S))
(get_learned_count S)) (convert_to_full_state_wl T)›
by (auto intro!: nres_relI frefI twl_st_heur_loop_twl_st_heurD simp: twl_st_heur'_def)
lemma cdcl_twl_stgy_restart_prog_early_wl_heur_alt_def:
‹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, last_GC, last_Restart, n).
cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0 (brk, T, last_GC, last_Restart, n) ∧
(¬ebrk ⟶isasat_fast T) ∧ length (get_clauses_wl_heur T) ≤ unat64_max⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(ebrk, brk, S, last_GC, last_Restart, n).
do {
ASSERT(¬brk ∧ ¬ebrk);
ASSERT(length (get_clauses_wl_heur S) ≤ unat64_max);
S ← convert_to_full_state_wl_heur S;
T ← unit_propagation_outer_loop_wl_D_heur S;
ASSERT(length (get_clauses_wl_heur T) ≤ unat64_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) ≤ unat64_max);
(T, n) ← restart_prog_wl_D_heur T last_GC last_Restart n brk;
ebrk ← RETURN (¬isasat_fast T);
RETURN (ebrk, brk ∨ ¬get_conflict_wl_is_None_heur T, T, n)
})
(ebrk, False, S⇩0::isasat, learned_clss_count S⇩0, learned_clss_count S⇩0, 0);
ASSERT(length (get_clauses_wl_heur T) ≤ unat64_max ∧
get_old_arena T = []);
if ¬brk then do {
T ← isasat_fast_slow T;
(brk, T, _) ← WHILE⇩T⇗cdcl_twl_stgy_restart_abs_wl_heur_inv2 T⇖
(λ(brk, _). ¬brk)
(λ(brk, S, last_GC, last_Restart, n).
do {
S ← convert_to_full_state_wl_heur S;
T ← unit_propagation_outer_loop_wl_D_heur S;
(brk, T) ← cdcl_twl_o_prog_wl_D_heur T;
(T, last_GC, last_Restart, n) ← restart_prog_wl_D_heur T last_GC last_Restart n brk;
RETURN (brk ∨ ¬get_conflict_wl_is_None_heur T, T, last_GC, last_Restart, n)
})
(False, T, n);
RETURN T
}
else isasat_fast_slow T
}›
unfolding convert_to_full_state_wl_heur_def Let_def cdcl_twl_stgy_restart_prog_early_wl_heur_def
bind_to_let_conv
by auto
lemma cdcl_twl_stgy_restart_prog_early_wl_heur_cdcl_twl_stgy_restart_prog_early_wl_D:
assumes r: ‹r ≤ unat64_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_loop⟩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, last_GC, last_Res, n) ← WHILE⇩T⇗cdcl_twl_stgy_restart_abs_wl_inv S⇩0 o snd⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(_, brk, S, last_GC, last_Res, n).
do {
S ← convert_to_full_state_wl S;
T ← unit_propagation_outer_loop_wl S;
(brk, T) ← cdcl_twl_o_prog_wl T;
(T, last_GC, last_Res, n) ← restart_prog_wl T last_GC last_Res n brk;
ebrk ← RES UNIV;
RETURN (ebrk, brk ∨ get_conflict_wl T ≠ None, T, last_GC, last_Res, n)
})
(ebrk, False, S⇩0::nat twl_st_wl, size (get_all_learned_clss_wl S⇩0),
size (get_all_learned_clss_wl S⇩0),0);
if ¬brk then do {
T ← RETURN T;
(brk, T, _) ← WHILE⇩T⇗cdcl_twl_stgy_restart_abs_wl_inv T⇖
(λ(brk, _). ¬brk)
(λ(brk, S, last_GC, last_Res, n).
do {
S ← convert_to_full_state_wl S;
T ← unit_propagation_outer_loop_wl S;
(brk, T) ← cdcl_twl_o_prog_wl T;
(T, last_GC, last_Res, n) ← restart_prog_wl T last_GC last_Res n brk;
RETURN (brk ∨ get_conflict_wl T ≠ None, T, last_GC, last_Res, n)
})
(False, T::nat twl_st_wl, last_GC, last_Res, n);
RETURN T
}
else RETURN T
}› for S⇩0
unfolding cdcl_twl_stgy_restart_prog_early_wl_def nres_monad1 bind_to_let_conv
by (auto intro!: bind_cong)
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
let ?R = ‹{((ebrk, brk, T, last_GC, last_Rephase, n),
(ebrk', brk', T', last_GC', last_Rephase', n')).
(ebrk = ebrk') ∧ (brk = brk') ∧ (T, T') ∈ twl_st_heur_loop ∧
(¬brk ⟶ (n = n' ∧ last_GC' = last_GC ∧ last_Rephase' = last_Rephase)) ∧
(¬ebrk ⟶ isasat_fast T) ∧ length (get_clauses_wl_heur T) ≤ unat64_max}›
let ?S = ‹{((brk, T, last_GC, last_Rephase, n),
(brk', T', last_GC', last_Rephase', n')).
(brk = brk') ∧ (T, T') ∈ twl_st_heur_loop ∧
(¬brk ⟶ (n = n' ∧ last_GC' = last_GC ∧ last_Rephase' = last_Rephase))}›
have twl_st_heur'': ‹(x1e, x1b) ∈ twl_st_heur_loop ⟹ get_conflict_wl x1b = None ⟹
(convert_to_full_state_wl_heur x1e) ≤⇓
(twl_st_heur''
(dom_m (get_clauses_wl x1b))
(length (get_clauses_wl_heur x1e))
(get_learned_count x1e)) (convert_to_full_state_wl x1b)›
for x1e x1b
by (auto simp: twl_st_heur'_def intro!: nres_relI twl_st_heur_loop_twl_st_heurD)
have twl_st_heur''': ‹(x1e, x1b) ∈ twl_st_heur'' 𝒟 r lcount ⟹
(x1e, x1b)
∈ {(S, Taa).
(S, Taa) ∈ twl_st_heur ∧
length (get_clauses_wl_heur S) = r ∧
learned_clss_count S = clss_size_allcount lcount}›
for x1e x1b r 𝒟 lcount
by (auto simp: twl_st_heur'_def clss_size_allcount_def learned_clss_count_def clss_size_lcountU0_def
clss_size_lcount_def clss_size_lcountUE_def clss_size_lcountUS_def clss_size_lcountUEk_def
split: prod.splits)
have H: ‹(xb, x'a)
∈ bool_rel ×⇩f
twl_st_heur'''' (length (get_clauses_wl_heur x1e) + MAX_HEADER_SIZE+1 + unat32_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 H''':
‹⋀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 S Sa T Ta
xb x'a x1j x2j x1k x2k.
(xa, x') ∈ ?R ⟹
x2c = (x1d, x2d) ⟹
x2b = (x1c, x2c) ⟹
x2a = (x1b, x2b) ⟹
x2 = (x1a, x2a) ⟹
x' = (x1, x2) ⟹
x2h = (x1i, x2i) ⟹
x2g = (x1h, x2h) ⟹
x2f = (x1g, x2g) ⟹
x2e = (x1f, x2f) ⟹
xa = (x1e, x2e) ⟹
¬ x1f ∧ ¬ x1e ⟹
length (get_clauses_wl_heur x1g) ≤ unat64_max ⟹
(xb, x'a)
∈ bool_rel ×⇩f
twl_st_heur''''uu (length (get_clauses_wl_heur x1g) + 3 + 1 + unat32_max div 2)
(Suc (clss_size_allcount (get_learned_count x1g))) ⟹
x'a = (x1j, x2j) ⟹
xb = (x1k, x2k) ⟹
(((((x2k, x1h), x1i), x2i), x1k), (((x2j, x1c), x1d), x2d), x1j)
∈ twl_st_heur''''u (length (get_clauses_wl_heur x2k))
(Suc (clss_size_allcount (get_learned_count x1g))) ×⇩f nat_rel ×⇩f nat_rel ×⇩f nat_rel ×⇩f bool_rel›
by simp
have H4: ‹⋀x y ebrk ebrka xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g T Ta xb x'a x1h x2h
x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o S Sa Tb Tc xc x'b x1p x2p x1q x2q.
(xb, x'a) ∈ ?S ⟹
case xb of (brk, uu_) ⇒ ¬ brk ⟹
case x'a of (brk, uu_) ⇒ ¬ brk ⟹
cdcl_twl_stgy_restart_abs_wl_heur_inv2 T xb ⟹
cdcl_twl_stgy_restart_abs_wl_inv Ta x'a ⟹
x2j = (x1k, x2k) ⟹
x2i = (x1j, x2j) ⟹
x2h = (x1i, x2i) ⟹
x'a = (x1h, x2h) ⟹
x2n = (x1o, x2o) ⟹
x2m = (x1n, x2n) ⟹
x2l = (x1m, x2m) ⟹
xb = (x1l, x2l) ⟹
(S, Sa)
∈ twl_st_heur'' (dom_m (get_clauses_wl x1i)) (length (get_clauses_wl_heur x1m))
(get_learned_count x1m) ⟹
(Tb, Tc)
∈ twl_st_heur'' (dom_m (get_clauses_wl x1i)) (length (get_clauses_wl_heur x1m))
(get_learned_count x1m) ⟹
(xc, x'b)
∈ bool_rel ×⇩f
twl_st_heur''''uu (length (get_clauses_wl_heur x1m) + 3 + 1 + unat32_max div 2)
(Suc (clss_size_allcount (get_learned_count x1m))) ⟹
x'b = (x1p, x2p) ⟹
xc = (x1q, x2q) ⟹
(((((x2q, x1n), x1o), x2o), x1q), (((x2p, x1j), x1k), x2k), x1p)
∈ twl_st_heur''''u (length (get_clauses_wl_heur x2q)) (learned_clss_count x2q) ×⇩f
nat_rel ×⇩f
nat_rel ×⇩f
nat_rel ×⇩f
bool_rel›
by auto
show ?thesis
supply[[goals_limit=1]] isasat_fast_length_leD[dest] twl_st_heur'_def[simp] learned_clss_count_twl_st_heur[simp]
unfolding cdcl_twl_stgy_restart_prog_early_wl_heur_alt_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_curry4]
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 = ?S]
WHILEIT_refine[where R = ‹?R›])
subgoal using r by (auto intro!: twl_st_heur_twl_st_heur_loopD)
subgoal for x y ebrk ebrka xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d
using cdcl_twl_stgy_restart_abs_wl_inv_NoneD[of y ‹fst (snd (snd x'))›
‹fst (snd (snd (snd x')))› ‹fst (snd (snd (snd (snd x'))))› ‹snd (snd (snd (snd (snd x'))))›]
unfolding cdcl_twl_stgy_restart_abs_wl_heur_inv_def prod.case prod_rel_fst_snd_iff
apply (rule_tac x=y in exI)
apply (rule_tac x= ‹fst (snd (snd x'))› in exI)
apply (case_tac xa; case_tac x')
by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by fast
subgoal by auto
apply (rule twl_st_heur''; auto dest!: cdcl_twl_stgy_restart_abs_wl_inv_NoneD; fail)
apply assumption
subgoal by auto
subgoal by auto
apply (rule twl_st_heur'''; assumption)
subgoal by (auto simp: isasat_fast_def unat64_max_def snat64_max_def unat32_max_def)
apply (rule H'''; assumption)
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 S Sa
T Ta xb x'a x1j x2j x1k x2k xc x'b x1l x2l x1m x2m x1n x2n x1o x2o ebrkb ebrkc
unfolding get_conflict_wl_is_None
by (subst get_conflict_wl_is_None_heur_get_conflict_wl_is_None[THEN fref_to_Down_unRET_Id, of _ ‹x1l›])
clarsimp_all
subgoal by auto
subgoal by (subst (asm)twl_st_heur_loop_def) force
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 T Ta xb x'a
using cdcl_twl_stgy_restart_abs_wl_inv_NoneD[of y ‹fst (snd x'a)›
‹fst (snd (snd x'a))› ‹fst (snd (snd (snd x'a)))› ‹snd (snd (snd (snd x'a)))›]
unfolding cdcl_twl_stgy_restart_abs_wl_heur_inv2_def prod.case prod_rel_fst_snd_iff
case_prod_beta
apply (rule_tac x= ‹x1b› in exI)
apply (rule_tac x= ‹fst (snd x'a)› in exI)
apply (case_tac xb; case_tac x'a)
by auto
subgoal by auto
apply (rule twl_st_heur'')
subgoal by (auto dest!: cdcl_twl_stgy_restart_abs_wl_inv_NoneD)
subgoal by (auto dest!: cdcl_twl_stgy_restart_abs_wl_inv_NoneD)
apply assumption
apply (rule twl_st_heur'''; assumption)
apply (rule H4; assumption)
subgoal for x y ebrk ebrka xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g x2g T Ta xb x'a x1h x2h
x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o S Sa Tb Tc xc x'b x1p x2p x1q x2q xd x'c x1r
x2r x1s x2s x1t x2t x1u x2u x1v x2v x1w x2w
unfolding get_conflict_wl_is_None
by (subst get_conflict_wl_is_None_heur_get_conflict_wl_is_None[THEN fref_to_Down_unRET_Id, of _ x1r])
clarsimp_all
subgoal by auto
subgoal by auto
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
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 cdcl_twl_stgy_restart_prog_bounded_wl_heur_alt_def:
‹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, last_GC, last_Restart, n). cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0 (brk, T, last_GC, last_Restart, n) ∧
(¬ebrk ⟶isasat_fast T ∧ n < unat64_max) ∧
(¬ebrk ⟶length (get_clauses_wl_heur T) ≤ snat64_max)⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(ebrk, brk, S, last_GC, last_Restart, n).
do {
ASSERT(¬brk ∧ ¬ebrk);
ASSERT(isasat_fast S);
S ← convert_to_full_state_wl_heur S;
T ← unit_propagation_outer_loop_wl_D_heur S;
ASSERT(isasat_fast T);
(brk, T) ← cdcl_twl_o_prog_wl_D_heur T;
ASSERT(isasat_fast_relaxed2 T n);
(T, last_GC, last_Restart, n) ← restart_prog_wl_D_heur T last_GC last_Restart n brk;
T ← update_all_phases T;
ASSERT(isasat_fast_relaxed T);
ebrk ← RETURN (¬(isasat_fast T ∧ n < unat64_max));
RETURN (ebrk, brk ∨ ¬get_conflict_wl_is_None_heur T, T, last_GC, last_Restart, n)
})
(ebrk, False, S⇩0::isasat, learned_clss_count S⇩0, learned_clss_count S⇩0, 0);
RETURN (ebrk, T)
}›
unfolding cdcl_twl_stgy_restart_prog_bounded_wl_heur_def bind_to_let_conv Let_def
convert_to_full_state_wl_heur_def by auto
lemma cdcl_twl_stgy_restart_prog_bounded_wl_heur_cdcl_twl_stgy_restart_prog_bounded_wl_D:
assumes r: ‹r ≤ unat64_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_loop⟩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, last_GC, last_Restart, n) ← WHILE⇩T⇗cdcl_twl_stgy_restart_abs_wl_inv S⇩0 o snd⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(_, brk, S, last_GC, last_Restart,n).
do {
ASSERT (¬ brk);
S ← convert_to_full_state_wl S;
T ← unit_propagation_outer_loop_wl S;
(brk, T) ← cdcl_twl_o_prog_wl T;
(T, last_GC, last_Restart, n) ← restart_prog_wl T last_GC last_Restart n brk;
T ← RETURN (id T);
ebrk ← RES UNIV;
RETURN (ebrk, brk ∨ get_conflict_wl T ≠ None, T, last_GC, last_Restart, n)
})
(ebrk, False, S⇩0::nat twl_st_wl, size (get_all_learned_clss_wl S⇩0),
size (get_all_learned_clss_wl S⇩0), 0);
RETURN (ebrk, T)
}› for S⇩0
unfolding cdcl_twl_stgy_restart_prog_bounded_wl_def nres_monad1 Let_def bind_to_let_conv
convert_to_full_state_wl_def
by (auto intro!: bind_cong[OF refl])
have [refine0]: ‹RETURN (¬(isasat_fast x ∧ n < unat64_max)) ≤ ⇓
{(b, b'). b = b' ∧ (b = (¬(isasat_fast x ∧ n < unat64_max)))} (RES UNIV)›
‹RETURN (¬isasat_fast x) ≤ ⇓
{(b, b'). b = b' ∧ (b = (¬(isasat_fast x ∧ 0 < unat64_max)))} (RES UNIV)›
for x n
by (auto intro: RETURN_RES_refine simp: unat64_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))
(get_learned_count x1e)›
for x1e x1b
by (auto simp: twl_st_heur'_def)
have twl_st_heur''': ‹(x1e, x1b) ∈ twl_st_heur'' 𝒟 r lcount ⟹
(x1e, x1b)
∈ {(S, Taa).
(S, Taa) ∈ twl_st_heur ∧
length (get_clauses_wl_heur S) = r ∧
learned_clss_count S = clss_size_allcount lcount}›
for x1e x1b r 𝒟 lcount
by (auto simp: twl_st_heur'_def clss_size_allcount_def learned_clss_count_def clss_size_lcountU0_def
clss_size_lcount_def clss_size_lcountUE_def clss_size_lcountUS_def clss_size_lcountUEk_def
split: prod.splits)
have H: ‹(xb, x'a)
∈ bool_rel ×⇩f
twl_st_heur'''' (length (get_clauses_wl_heur x1e) + MAX_HEADER_SIZE+1 + unat32_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
let ?R = ‹{((ebrk, brk, T, last_GC, last_Rephase, n), ebrk', brk', T',
last_GC', last_Rephase', n').
ebrk = ebrk' ∧
brk = brk' ∧
(T, T') ∈ twl_st_heur_loop ∧
(¬brk ⟶ (n = n' ∧ last_GC' = last_GC ∧ last_Rephase' = last_Rephase)) ∧
(¬ ebrk ⟶ isasat_fast T ∧ n < unat64_max) ∧
length (get_clauses_wl_heur T) ≤ unat64_max}›
have H4: ‹⋀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 S Sa
T Ta xb x'a x1j x2j x1k x2k.
(x, y) ∈ twl_st_heur''' r ⟹
(xa, x') ∈ ?R ⟹
x2c = (x1d, x2d) ⟹
x2b = (x1c, x2c) ⟹
x2a = (x1b, x2b) ⟹
x2 = (x1a, x2a) ⟹
x' = (x1, x2) ⟹
x2h = (x1i, x2i) ⟹
x2g = (x1h, x2h) ⟹
x2f = (x1g, x2g) ⟹
x2e = (x1f, x2f) ⟹
xa = (x1e, x2e) ⟹
¬ x1a ⟹
¬ x1f ∧ ¬ x1e ⟹
isasat_fast x1g ⟹
(S, Sa)
∈ twl_st_heur'' (dom_m (get_clauses_wl x1b)) (length (get_clauses_wl_heur x1g))
(get_learned_count x1g) ⟹
(T, Ta)
∈ twl_st_heur'' (dom_m (get_clauses_wl Sa)) (length (get_clauses_wl_heur S)) (get_learned_count S) ⟹
isasat_fast T ⟹
(xb, x'a)
∈ bool_rel ×⇩f
twl_st_heur''''uu (length (get_clauses_wl_heur S) + 3 + 1 + unat32_max div 2)
(Suc (clss_size_allcount (get_learned_count S))) ⟹
x'a = (x1j, x2j) ⟹
xb = (x1k, x2k) ⟹
isasat_fast_relaxed2 x2k x2i ⟹
(((((x2k, x1h), x1i), x2i), x1k), (((x2j, x1c), x1d), x2d), x1j)
∈ twl_st_heur''''u (length (get_clauses_wl_heur x2k)) (learned_clss_count x2k) ×⇩f
nat_rel ×⇩f
nat_rel ×⇩f
nat_rel ×⇩f
bool_rel›
by simp
have H5:
‹(xc, x'b) ∈ restart_prog_wl_heur_rel (length (get_clauses_wl_heur x2k)) (learned_clss_count x2k) ⟹
x2m = (x1n, x2n) ⟹
x2l = (x1m, x2m) ⟹
x'b = (x1l, x2l) ⟹
x2p = (x1q, x2q) ⟹
x2o = (x1p, x2p) ⟹
xc = (x1o, x2o) ⟹
(x1o, x1l)
∈ twl_st_heur_loop''''uu (length (get_clauses_wl_heur x2k)) (learned_clss_count x2k)›
for x2k x2m x1n x2n x2l x1m x'b x1l x2p x1q x2q x2o x1o xc x1p
by auto
show ?thesis
supply[[goals_limit=1]] isasat_fast_length_leD[dest] twl_st_heur'_def[simp] learned_clss_count_twl_st_heur[simp]
unfolding cdcl_twl_stgy_restart_prog_bounded_wl_heur_alt_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_curry4]
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]
update_all_phases_Pair
convert_to_full_state_wl_heur
WHILEIT_refine[where R = ‹?R›])
subgoal using r by (auto simp: snat64_max_def isasat_fast_def unat32_max_def
dest: twl_st_heur_twl_st_heur_loopD)
subgoal for x y ebrk ebrka xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d
using cdcl_twl_stgy_restart_abs_wl_inv_NoneD[of y ‹fst (snd (snd x'))›
‹fst (snd (snd (snd x')))› ‹fst (snd (snd (snd (snd x'))))› ‹snd (snd (snd (snd (snd x'))))›]
unfolding cdcl_twl_stgy_restart_abs_wl_heur_inv_def prod.case prod_rel_fst_snd_iff
apply (rule_tac x=y in exI)
apply (rule_tac x= ‹fst (snd (snd x'))› in exI)
apply (case_tac xa; case_tac x')
by (auto intro!: twl_st_heur_twl_st_heur_loopD)
subgoal by auto
subgoal by auto
subgoal by (auto simp: snat64_max_def isasat_fast_def unat32_max_def)
subgoal by auto
subgoal by fast
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto dest!: cdcl_twl_stgy_restart_abs_wl_inv_NoneD)
apply (rule twl_st_heur'')
subgoal by simp
subgoal by (auto dest: get_learned_count_learned_clss_countD simp: isasat_fast_def)
apply (rule twl_st_heur'''; assumption)
subgoal by (auto simp: isasat_fast_def unat64_max_def unat32_max_def snat64_max_def
isasat_fast_relaxed_def isasat_fast_relaxed2_def)
apply (rule H4; assumption)
apply (rule H5; assumption)
subgoal
by (auto simp: isasat_fast_def unat64_max_def unat32_max_def snat64_max_def
isasat_fast_relaxed_def)
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 S Sa
T Ta xb x'a x1j x2j x1k x2k xc x'b x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p x1q x2q Tb Tc
unfolding get_conflict_wl_is_None
apply (subst get_conflict_wl_is_None_heur_get_conflict_wl_is_None[THEN fref_to_Down_unRET_Id, of _ Tc])
apply fast
by (auto simp: isasat_fast_def unat64_max_def unat32_max_def snat64_max_def
dest!: twl_st_heur_twl_st_heur_loopD)
subgoal by auto
done
qed
end