theory Watched_Literals_Algorithm_Restart
imports Watched_Literals_Algorithm Watched_Literals_Transition_System_Restart
begin
context twl_restart_ops
begin
text ‹Restarts are never necessary›
definition restart_required :: "'v twl_st ⇒ nat ⇒ bool nres" where
‹restart_required S n = SPEC (λb. b ⟶ size (get_learned_clss S) > f n)›
definition (in -) restart_prog_pre :: ‹'v twl_st ⇒ bool ⇒ bool› where
‹restart_prog_pre S brk ⟷ twl_struct_invs S ∧ twl_stgy_invs S ∧
(¬brk ⟶ get_conflict S = None)›
definition restart_prog
:: "'v twl_st ⇒ nat ⇒ bool ⇒ ('v twl_st × nat) nres"
where
‹restart_prog S n brk = do {
ASSERT(restart_prog_pre S brk);
b ← restart_required S n;
b2 ← SPEC(λ_. True);
if b2 ∧ b ∧ ¬brk then do {
T ← SPEC(λT. cdcl_twl_restart S T);
RETURN (T, n + 1)
}
else
if b ∧ ¬brk then do {
T ← SPEC(λT. cdcl_twl_restart S T);
RETURN (T, n + 1)
}
else
RETURN (S, n)
}›
definition cdcl_twl_stgy_restart_prog_inv where
‹cdcl_twl_stgy_restart_prog_inv S⇩0 brk T n ≡ twl_struct_invs T ∧ twl_stgy_invs T ∧
(brk ⟶ final_twl_state T) ∧ cdcl_twl_stgy_restart_with_leftovers (S⇩0, 0) (T, n) ∧
clauses_to_update T = {#} ∧ (¬brk ⟶ get_conflict T = None)›
definition cdcl_twl_stgy_restart_prog :: "'v twl_st ⇒ 'v twl_st nres" where
‹cdcl_twl_stgy_restart_prog S⇩0 =
do {
(brk, T, _) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_prog_inv S⇩0 brk T n⇖
(λ(brk, _). ¬brk)
(λ(brk, S, n).
do {
T ← unit_propagation_outer_loop S;
(brk, T) ← cdcl_twl_o_prog T;
(T, n) ← restart_prog T n brk;
RETURN (brk, T, n)
})
(False, S⇩0, 0);
RETURN T
}›
lemma (in twl_restart)
assumes
inv: ‹case (brk, T, m) of (brk, T, m) ⇒ cdcl_twl_stgy_restart_prog_inv S brk T m› and
cond: ‹case (brk, T, m) of (brk, uu_) ⇒ ¬ brk› and
other_inv: ‹cdcl_twl_o_prog_spec S' (brk', U)› and
struct_invs_S: ‹twl_struct_invs S'› and
cp: ‹cdcl_twl_cp⇧*⇧* T S'› and
lits_to_update: ‹literals_to_update S' = {#}› and
‹∀S'a. ¬ cdcl_twl_cp S' S'a› and
‹twl_stgy_invs S'›
shows restart_prog_spec:
‹restart_prog U m brk'
≤ SPEC
(λx. (case x of
(T, na) ⇒ RETURN (brk', T, na))
≤ SPEC
(λs'. (case s' of
(brk, T, n) ⇒
twl_struct_invs T ∧
twl_stgy_invs T ∧
(brk ⟶ final_twl_state T) ∧
cdcl_twl_stgy_restart_with_leftovers (S, 0)
(T, n) ∧
clauses_to_update T = {#} ∧
(¬ brk ⟶ get_conflict T = None)) ∧
(s', brk, T, m)
∈ {((brkT, T, n), brkS, S, m).
twl_struct_invs S ∧
cdcl_twl_stgy_restart_with_leftovers1 (S, m)
(T, n)} ∪
{((brkT, T), brkS, S). S = T ∧ brkT ∧ ¬ brkS}))› (is ?A)
proof -
have struct_invs': ‹cdcl_twl_restart U T ⟹ twl_struct_invs T› for T
using assms(3) cdcl_twl_restart_twl_struct_invs by blast
have stgy_invs: ‹cdcl_twl_restart U V ⟹twl_stgy_invs V› for V
using assms(3) cdcl_twl_restart_twl_stgy_invs by blast
have res_no_clss_to_upd: ‹cdcl_twl_restart U V ⟹ clauses_to_update V = {#}› for V
by (auto simp: cdcl_twl_restart.simps)
have res_no_confl: ‹cdcl_twl_restart U V ⟹ get_conflict V = None› for V
by (auto simp: cdcl_twl_restart.simps)
have
struct_invs_T: ‹twl_struct_invs T› and
‹twl_stgy_invs T› and
‹brk ⟶ final_twl_state T› and
twl_res: ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (T, m)› and
‹clauses_to_update T = {#}› and
confl: ‹¬ brk ⟶ get_conflict T = None›
using inv unfolding cdcl_twl_stgy_restart_prog_inv_def by fast+
have
cdcl_o: ‹cdcl_twl_o⇧*⇧* S' U› and
conflict_U: ‹get_conflict U ≠ None ⟹ count_decided (get_trail U) = 0› and
brk'_no_step: ‹brk' ⟹ final_twl_state U› and
struct_invs_U: ‹twl_struct_invs U› and
stgy_invs_U: ‹twl_stgy_invs U› and
clss_to_upd_U: ‹clauses_to_update U = {#}› and
lits_to_upd_U: ‹¬ brk' ⟶ literals_to_update U ≠ {#}› and
confl_U: ‹¬ brk' ⟶ get_conflict U = None›
using other_inv unfolding final_twl_state_def by fast+
have ‹cdcl_twl_stgy⇧*⇧* T U›
by (meson ‹cdcl_twl_o⇧*⇧* S' U› assms(5) rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_o_stgyD
rtranclp_trans)
have
twl_restart_after_restart:
‹cdcl_twl_stgy_restart (T, m) (V, Suc m)› and
rtranclp_twl_restart_after_restart:
‹cdcl_twl_stgy_restart⇧*⇧* (S, 0) (V, m + 1)› and
cdcl_twl_stgy_restart_with_leftovers_after_restart:
‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (V, m + 1)› and
cdcl_twl_stgy_restart_with_leftovers_after_restart_T_V:
‹cdcl_twl_stgy_restart_with_leftovers (T, m) (V, Suc m)› and
cdcl_twl_stgy_restart_with_leftovers1_after_restart:
‹cdcl_twl_stgy_restart_with_leftovers1 (T, m) (V, Suc m)›
if
f: ‹True ⟶ f (snd (U, m)) < size (get_learned_clss (fst (U, m)))› and
res: ‹cdcl_twl_restart U V› and
[simp]: ‹brk' = False›
for V
proof -
have ‹S' ≠ U›
using lits_to_update lits_to_upd_U by auto
then have ‹cdcl_twl_o⇧+⇧+ S' U›
using ‹cdcl_twl_o⇧*⇧* S' U› unfolding rtranclp_unfold by auto
then have st: ‹cdcl_twl_stgy⇧+⇧+ T U›
by (meson local.cp rtranclp_cdcl_twl_cp_stgyD rtranclp_tranclp_tranclp
tranclp_cdcl_twl_o_stgyD)
show twl_res_T_V: ‹cdcl_twl_stgy_restart (T, m) (V, Suc m)›
apply (rule cdcl_twl_stgy_restart.restart_step[of _ U])
subgoal by (rule st)
subgoal using f by simp
subgoal by (rule res)
done
show ‹cdcl_twl_stgy_restart_with_leftovers (T, m) (V, Suc m)›
unfolding cdcl_twl_stgy_restart_with_leftovers_def
by (rule exI[of _ ‹V›])(auto simp: twl_res_T_V)
show ‹cdcl_twl_stgy_restart⇧*⇧* (S, 0) (V, m + 1)›
using twl_res twl_res_T_V
unfolding cdcl_twl_stgy_restart_with_leftovers_def
by (auto dest: cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart)
then show ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (V, m + 1)›
unfolding cdcl_twl_stgy_restart_with_leftovers_def apply -
by (rule exI[of _ V]) auto
show ‹cdcl_twl_stgy_restart_with_leftovers1 (T, m) (V, Suc m)›
using twl_res_T_V
unfolding cdcl_twl_stgy_restart_with_leftovers1_def
by fast
qed
have
rtranclp_twl_restart_after_restart_S_U:
‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (U, m)› and
rtranclp_twl_restart_after_restart_T_U:
‹cdcl_twl_stgy_restart_with_leftovers (T, m) (U, m)›
proof -
obtain Ta where
S_Ta: ‹cdcl_twl_stgy_restart⇧*⇧* (S, 0) (Ta, snd (T, m))›
‹cdcl_twl_stgy⇧*⇧* Ta (fst (T, m))›
using twl_res unfolding cdcl_twl_stgy_restart_with_leftovers_def
by auto
then have ‹cdcl_twl_stgy⇧*⇧* Ta (fst (U, m))›
using ‹cdcl_twl_stgy⇧*⇧* T U› by auto
then show ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (U, m)›
using S_Ta unfolding cdcl_twl_stgy_restart_with_leftovers_def
by fastforce
show ‹cdcl_twl_stgy_restart_with_leftovers (T, m) (U, m)›
using ‹cdcl_twl_stgy⇧*⇧* T U› unfolding cdcl_twl_stgy_restart_with_leftovers_def
by fastforce
qed
have
rtranclp_twl_restart_after_restart_brk:
‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (U, m)›
if
[simp]: ‹brk' = True›
proof -
have ‹full1 cdcl_twl_stgy T U ∨ T = U ∨ get_conflict U ≠ None›
using brk'_no_step ‹cdcl_twl_stgy⇧*⇧* T U›
unfolding rtranclp_unfold full1_def final_twl_state_def by auto
then consider
(step) ‹cdcl_twl_stgy_restart (T, m) (U, m)› |
(TU) ‹T = U› |
(final) ‹get_conflict U ≠ None›
by (auto dest!: cdcl_twl_stgy_restart.intros)
then show ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (U, m)›
proof cases
case step
then show ?thesis
using twl_res unfolding cdcl_twl_stgy_restart_with_leftovers_def
using cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart2[of T m U] apply -
by (rule exI[of _ U]) (fastforce dest!: )
next
case [simp]: TU
then show ?thesis
using twl_res unfolding cdcl_twl_stgy_restart_with_leftovers_def
using cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart2[of T m U] apply -
by fastforce
next
case final
then show ?thesis
using twl_res ‹cdcl_twl_stgy⇧*⇧* T U› unfolding cdcl_twl_stgy_restart_with_leftovers_def
using cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart2[of T m U] apply -
by fastforce
qed
qed
have cdcl_twl_stgy_restart_with_leftovers1_T_U:
‹cdcl_twl_stgy_restart_with_leftovers1 (T, m) (U, m) ⟷ T ≠ U›
proof -
have ‹cdcl_twl_stgy⇧+⇧+ T U ∨ T = U›
using ‹cdcl_twl_stgy⇧*⇧* T U› unfolding rtranclp_unfold by auto
then show ?thesis
using wf_not_refl[OF wf_cdcl_twl_stgy_restart, of ‹(U, m)›]
using wf_not_refl[OF tranclp_wf_cdcl_twl_stgy, of ‹U›]
struct_invs_U
unfolding cdcl_twl_stgy_restart_with_leftovers1_def by auto
qed
have brk'_eq: ‹¬cdcl_twl_stgy_restart_with_leftovers1 (T, m) (U, m) ⟹ brk'›
using cdcl_o lits_to_upd_U lits_to_update local.cp
unfolding cdcl_twl_stgy_restart_with_leftovers1_def
unfolding rtranclp_unfold
by (auto dest!: tranclp_cdcl_twl_o_stgyD tranclp_cdcl_twl_cp_stgyD
simp: rtranclp_unfold
dest: rtranclp_tranclp_tranclp tranclp_trans)
have [simp]: ‹brk = False›
using cond by auto
show ?A
unfolding restart_prog_def restart_required_def
apply (refine_vcg; remove_dummy_vars)
subgoal using struct_invs_U stgy_invs_U confl_U unfolding restart_prog_pre_def by fast
subgoal by (rule struct_invs')
subgoal by (rule stgy_invs)
subgoal by (rule cdcl_twl_stgy_restart_with_leftovers_after_restart) simp
subgoal by (rule res_no_clss_to_upd)
subgoal by (rule res_no_confl)
subgoal by (auto intro!: struct_invs_S struct_invs_T
cdcl_twl_stgy_restart_with_leftovers1_after_restart)
subgoal using struct_invs' by blast
subgoal using stgy_invs by blast
subgoal by (rule cdcl_twl_stgy_restart_with_leftovers_after_restart) simp
subgoal by (rule res_no_clss_to_upd)
subgoal by (rule res_no_confl)
subgoal by (auto intro!: struct_invs_S struct_invs_T
cdcl_twl_stgy_restart_with_leftovers1_after_restart)
subgoal by (rule struct_invs_U)
subgoal by (rule stgy_invs_U)
subgoal by (rule brk'_no_step) simp
subgoal
by (auto intro: rtranclp_twl_restart_after_restart_brk
rtranclp_twl_restart_after_restart_S_U)
subgoal by (rule clss_to_upd_U)
subgoal using struct_invs_U conflict_U lits_to_upd_U
by (cases ‹get_conflict U›)(auto simp: twl_struct_invs_def)
subgoal
using cdcl_twl_stgy_restart_with_leftovers1_T_U brk'_eq
by (auto simp: twl_restart_after_restart struct_invs_S struct_invs_T
cdcl_twl_stgy_restart_with_leftovers_after_restart_T_V struct_invs_U
rtranclp_twl_restart_after_restart_brk rtranclp_twl_restart_after_restart_T_U
cdcl_twl_stgy_restart_with_leftovers1_after_restart)
done
qed
lemma (in twl_restart)
assumes
inv: ‹case (ebrk, brk, T, m) of (ebrk, brk, T, m) ⇒ cdcl_twl_stgy_restart_prog_inv S brk T m› and
cond: ‹case (ebrk, brk, T, m) of (ebrk, brk, _) ⇒ ¬ brk ∧ ¬ebrk› and
other_inv: ‹cdcl_twl_o_prog_spec S' (brk', U)› and
struct_invs_S: ‹twl_struct_invs S'› and
cp: ‹cdcl_twl_cp⇧*⇧* T S'› and
lits_to_update: ‹literals_to_update S' = {#}› and
‹∀S'a. ¬ cdcl_twl_cp S' S'a› and
‹twl_stgy_invs S'›
shows restart_prog_early_spec:
‹restart_prog U m brk'
≤ SPEC
(λx. (case x of (T, n) ⇒ RES UNIV ⤜ (λebrk. RETURN (ebrk, brk', T, n)))
≤ SPEC
(λs'. (case s' of (ebrk, brk, x, xb) ⇒
cdcl_twl_stgy_restart_prog_inv S brk x xb) ∧
(s', ebrk, brk, T, m)
∈ {((ebrk, brkT, T, n), ebrk, brkS, S, m).
twl_struct_invs S ∧
cdcl_twl_stgy_restart_with_leftovers1 (S, m) (T, n)} ∪
{((ebrkT, brkT, T), ebrkS, brkS, S).
S = T ∧ (ebrkT ∨ brkT) ∧ ¬ brkS ∧ ¬ ebrkS}))› (is ‹?B›)
proof -
have struct_invs': ‹cdcl_twl_restart U T ⟹ twl_struct_invs T› for T
using assms(3) cdcl_twl_restart_twl_struct_invs by blast
have stgy_invs: ‹cdcl_twl_restart U V ⟹twl_stgy_invs V› for V
using assms(3) cdcl_twl_restart_twl_stgy_invs by blast
have res_no_clss_to_upd: ‹cdcl_twl_restart U V ⟹ clauses_to_update V = {#}› for V
by (auto simp: cdcl_twl_restart.simps)
have res_no_confl: ‹cdcl_twl_restart U V ⟹ get_conflict V = None› for V
by (auto simp: cdcl_twl_restart.simps)
have
struct_invs_T: ‹twl_struct_invs T› and
‹twl_stgy_invs T› and
‹brk ⟶ final_twl_state T› and
twl_res: ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (T, m)› and
‹clauses_to_update T = {#}› and
confl: ‹¬ brk ⟶ get_conflict T = None›
using inv unfolding cdcl_twl_stgy_restart_prog_inv_def by fast+
have
cdcl_o: ‹cdcl_twl_o⇧*⇧* S' U› and
conflict_U: ‹get_conflict U ≠ None ⟹ count_decided (get_trail U) = 0› and
brk'_no_step: ‹brk' ⟹ final_twl_state U› and
struct_invs_U: ‹twl_struct_invs U› and
stgy_invs_U: ‹twl_stgy_invs U› and
clss_to_upd_U: ‹clauses_to_update U = {#}› and
lits_to_upd_U: ‹¬ brk' ⟶ literals_to_update U ≠ {#}› and
confl_U: ‹¬ brk' ⟶ get_conflict U = None›
using other_inv unfolding final_twl_state_def by fast+
have ‹cdcl_twl_stgy⇧*⇧* T U›
by (meson ‹cdcl_twl_o⇧*⇧* S' U› assms(5) rtranclp_cdcl_twl_cp_stgyD rtranclp_cdcl_twl_o_stgyD
rtranclp_trans)
have
twl_restart_after_restart:
‹cdcl_twl_stgy_restart (T, m) (V, Suc m)› and
rtranclp_twl_restart_after_restart:
‹cdcl_twl_stgy_restart⇧*⇧* (S, 0) (V, m + 1)› and
cdcl_twl_stgy_restart_with_leftovers_after_restart:
‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (V, m + 1)› and
cdcl_twl_stgy_restart_with_leftovers_after_restart_T_V:
‹cdcl_twl_stgy_restart_with_leftovers (T, m) (V, Suc m)› and
cdcl_twl_stgy_restart_with_leftovers1_after_restart:
‹cdcl_twl_stgy_restart_with_leftovers1 (T, m) (V, Suc m)›
if
f: ‹True ⟶ f (snd (U, m)) < size (get_learned_clss (fst (U, m)))› and
res: ‹cdcl_twl_restart U V› and
[simp]: ‹brk' = False›
for V
proof -
have ‹S' ≠ U›
using lits_to_update lits_to_upd_U by auto
then have ‹cdcl_twl_o⇧+⇧+ S' U›
using ‹cdcl_twl_o⇧*⇧* S' U› unfolding rtranclp_unfold by auto
then have st: ‹cdcl_twl_stgy⇧+⇧+ T U›
by (meson local.cp rtranclp_cdcl_twl_cp_stgyD rtranclp_tranclp_tranclp
tranclp_cdcl_twl_o_stgyD)
show twl_res_T_V: ‹cdcl_twl_stgy_restart (T, m) (V, Suc m)›
apply (rule cdcl_twl_stgy_restart.restart_step[of _ U])
subgoal by (rule st)
subgoal using f by simp
subgoal by (rule res)
done
show ‹cdcl_twl_stgy_restart_with_leftovers (T, m) (V, Suc m)›
unfolding cdcl_twl_stgy_restart_with_leftovers_def
by (rule exI[of _ ‹V›])(auto simp: twl_res_T_V)
show ‹cdcl_twl_stgy_restart⇧*⇧* (S, 0) (V, m + 1)›
using twl_res twl_res_T_V
unfolding cdcl_twl_stgy_restart_with_leftovers_def
by (auto dest: cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart)
then show ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (V, m + 1)›
unfolding cdcl_twl_stgy_restart_with_leftovers_def apply -
by (rule exI[of _ V]) auto
show ‹cdcl_twl_stgy_restart_with_leftovers1 (T, m) (V, Suc m)›
using twl_res_T_V
unfolding cdcl_twl_stgy_restart_with_leftovers1_def
by fast
qed
have
rtranclp_twl_restart_after_restart_S_U:
‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (U, m)› and
rtranclp_twl_restart_after_restart_T_U:
‹cdcl_twl_stgy_restart_with_leftovers (T, m) (U, m)›
proof -
obtain Ta where
S_Ta: ‹cdcl_twl_stgy_restart⇧*⇧* (S, 0) (Ta, snd (T, m))›
‹cdcl_twl_stgy⇧*⇧* Ta (fst (T, m))›
using twl_res unfolding cdcl_twl_stgy_restart_with_leftovers_def
by auto
then have ‹cdcl_twl_stgy⇧*⇧* Ta (fst (U, m))›
using ‹cdcl_twl_stgy⇧*⇧* T U› by auto
then show ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (U, m)›
using S_Ta unfolding cdcl_twl_stgy_restart_with_leftovers_def
by fastforce
show ‹cdcl_twl_stgy_restart_with_leftovers (T, m) (U, m)›
using ‹cdcl_twl_stgy⇧*⇧* T U› unfolding cdcl_twl_stgy_restart_with_leftovers_def
by fastforce
qed
have
rtranclp_twl_restart_after_restart_brk:
‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (U, m)›
if
[simp]: ‹brk' = True›
proof -
have ‹full1 cdcl_twl_stgy T U ∨ T = U ∨ get_conflict U ≠ None›
using brk'_no_step ‹cdcl_twl_stgy⇧*⇧* T U›
unfolding rtranclp_unfold full1_def final_twl_state_def by auto
then consider
(step) ‹cdcl_twl_stgy_restart (T, m) (U, m)› |
(TU) ‹T = U› |
(final) ‹get_conflict U ≠ None›
by (auto dest!: cdcl_twl_stgy_restart.intros)
then show ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (U, m)›
proof cases
case step
then show ?thesis
using twl_res unfolding cdcl_twl_stgy_restart_with_leftovers_def
using cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart2[of T m U] apply -
by (rule exI[of _ U]) (fastforce dest!: )
next
case [simp]: TU
then show ?thesis
using twl_res unfolding cdcl_twl_stgy_restart_with_leftovers_def
using cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart2[of T m U] apply -
by fastforce
next
case final
then show ?thesis
using twl_res ‹cdcl_twl_stgy⇧*⇧* T U› unfolding cdcl_twl_stgy_restart_with_leftovers_def
using cdcl_twl_stgy_restart_cdcl_twl_stgy_cdcl_twl_stgy_restart2[of T m U] apply -
by fastforce
qed
qed
have cdcl_twl_stgy_restart_with_leftovers1_T_U:
‹cdcl_twl_stgy_restart_with_leftovers1 (T, m) (U, m) ⟷ T ≠ U›
proof -
have ‹cdcl_twl_stgy⇧+⇧+ T U ∨ T = U›
using ‹cdcl_twl_stgy⇧*⇧* T U› unfolding rtranclp_unfold by auto
then show ?thesis
using wf_not_refl[OF wf_cdcl_twl_stgy_restart, of ‹(U, m)›]
using wf_not_refl[OF tranclp_wf_cdcl_twl_stgy, of ‹U›]
struct_invs_U
unfolding cdcl_twl_stgy_restart_with_leftovers1_def by auto
qed
have brk'_eq: ‹¬cdcl_twl_stgy_restart_with_leftovers1 (T, m) (U, m) ⟹ brk'›
using cdcl_o lits_to_upd_U lits_to_update local.cp
unfolding cdcl_twl_stgy_restart_with_leftovers1_def
unfolding rtranclp_unfold
by (auto dest!: tranclp_cdcl_twl_o_stgyD tranclp_cdcl_twl_cp_stgyD
simp: rtranclp_unfold
dest: rtranclp_tranclp_tranclp tranclp_trans)
have H[simp]: ‹brk = False› ‹ebrk = False›
using cond by auto
show ?B
unfolding restart_prog_def restart_required_def
apply (refine_vcg; remove_dummy_vars)
subgoal using struct_invs_U stgy_invs_U confl_U
unfolding restart_prog_pre_def cdcl_twl_stgy_restart_prog_inv_def H by fast
subgoal
unfolding cdcl_twl_stgy_restart_prog_inv_def
apply (intro conjI)
subgoal by (rule struct_invs')
subgoal by (rule stgy_invs)
subgoal unfolding H by fast
subgoal by (rule cdcl_twl_stgy_restart_with_leftovers_after_restart) simp_all
subgoal by (rule res_no_clss_to_upd)
subgoal by (simp add: res_no_confl)
done
subgoal
using cdcl_twl_stgy_restart_with_leftovers1_T_U brk'_eq struct_invs_T
by (simp add: clss_to_upd_U confl_U rtranclp_twl_restart_after_restart_S_U
stgy_invs_U struct_invs_U twl_restart_ops.cdcl_twl_stgy_restart_prog_inv_def
cdcl_twl_stgy_restart_with_leftovers1_after_restart)
subgoal
unfolding cdcl_twl_stgy_restart_prog_inv_def
apply (intro conjI)
subgoal by (rule struct_invs')
subgoal by (rule stgy_invs)
subgoal unfolding H by fast
subgoal by (rule cdcl_twl_stgy_restart_with_leftovers_after_restart) simp_all
subgoal by (rule res_no_clss_to_upd)
subgoal by (simp add: res_no_confl)
done
subgoal
using cdcl_twl_stgy_restart_with_leftovers1_T_U brk'_eq
by (auto simp: twl_restart_after_restart struct_invs_S struct_invs_T
cdcl_twl_stgy_restart_with_leftovers_after_restart_T_V struct_invs_U
rtranclp_twl_restart_after_restart_brk rtranclp_twl_restart_after_restart_T_U
cdcl_twl_stgy_restart_with_leftovers1_after_restart
brk'_no_step clss_to_upd_U restart_prog_pre_def rtranclp_twl_restart_after_restart_S_U
twl_restart_ops.cdcl_twl_stgy_restart_prog_inv_def)
subgoal
using cdcl_twl_stgy_restart_with_leftovers1_T_U brk'_eq
by (auto simp: twl_restart_after_restart struct_invs_S struct_invs_T
cdcl_twl_stgy_restart_with_leftovers_after_restart_T_V struct_invs_U
rtranclp_twl_restart_after_restart_brk rtranclp_twl_restart_after_restart_T_U
cdcl_twl_stgy_restart_with_leftovers1_after_restart
brk'_no_step clss_to_upd_U restart_prog_pre_def rtranclp_twl_restart_after_restart_S_U
twl_restart_ops.cdcl_twl_stgy_restart_prog_inv_def)
subgoal
using cdcl_twl_stgy_restart_with_leftovers1_T_U brk'_eq
by (auto simp: twl_restart_after_restart struct_invs_S struct_invs_T
cdcl_twl_stgy_restart_with_leftovers_after_restart_T_V struct_invs_U
rtranclp_twl_restart_after_restart_brk rtranclp_twl_restart_after_restart_T_U
cdcl_twl_stgy_restart_with_leftovers1_after_restart)
done
qed
lemma cdcl_twl_stgy_restart_with_leftovers_refl: ‹cdcl_twl_stgy_restart_with_leftovers S S›
unfolding cdcl_twl_stgy_restart_with_leftovers_def
by (rule exI[of _ ‹fst S›]) auto
lemma (in twl_restart) cdcl_twl_stgy_restart_prog_spec:
assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
‹get_conflict S = None›
shows
‹cdcl_twl_stgy_restart_prog S ≤ SPEC(λT. ∃n. cdcl_twl_stgy_restart_with_leftovers (S, 0) (T, n) ∧
final_twl_state T)›
(is ‹_ ≤ SPEC(λT. ?P T)›)
proof -
have final_prop: ‹?P T›
if
inv: ‹case (brk, T, n) of (brk, T, m) ⇒ cdcl_twl_stgy_restart_prog_inv S brk T m› and
‹¬ (case (brk, T, n) of (brk, uu_) ⇒ ¬ brk)›
for brk T n
proof -
have
‹brk› and
‹twl_struct_invs T› and
‹twl_stgy_invs T› and
ns: ‹final_twl_state T› and
twl_left_overs: ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (T, n)› and
‹clauses_to_update T = {#}›
using that unfolding cdcl_twl_stgy_restart_prog_inv_def by auto
obtain S' where
st: ‹cdcl_twl_stgy_restart⇧*⇧* (S, 0) (S', n)› and
S'_T: ‹cdcl_twl_stgy⇧*⇧* S' T›
using twl_left_overs unfolding cdcl_twl_stgy_restart_with_leftovers_def by auto
then show ?thesis
using ns unfolding cdcl_twl_stgy_restart_with_leftovers_def apply -
apply (rule_tac x=n in exI)
apply (rule conjI)
subgoal by (rule_tac x=S' in exI) auto
subgoal by auto
done
qed
show ?thesis
supply RETURN_as_SPEC_refine[refine2 del]
unfolding cdcl_twl_stgy_restart_prog_def full_def cdcl_twl_stgy_restart_prog_inv_def
apply (refine_vcg WHILEIT_rule[where
R = ‹{((brkT, T, n), (brkS, S, m)).
twl_struct_invs S ∧ cdcl_twl_stgy_restart_with_leftovers1 (S, m) (T, n)} ∪
{((brkT, T), (brkS, S)). S = T ∧ brkT ∧ ¬brkS}›];
remove_dummy_vars)
subgoal by (rule wf_cdcl_twl_stgy_restart_measure)
subgoal using assms by fast
subgoal using assms by fast
subgoal using assms by fast
subgoal by (rule cdcl_twl_stgy_restart_with_leftovers_refl)
subgoal using assms by fast
subgoal using assms by fast
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by (simp add: no_step_cdcl_twl_cp_no_step_cdcl⇩W_cp)
subgoal by fast
subgoal by (rule restart_prog_spec[unfolded cdcl_twl_stgy_restart_prog_inv_def])
subgoal by (rule final_prop[unfolded cdcl_twl_stgy_restart_prog_inv_def])
done
qed
definition cdcl_twl_stgy_restart_prog_early :: "'v twl_st ⇒ 'v twl_st nres" where
‹cdcl_twl_stgy_restart_prog_early S⇩0 =
do {
ebrk ← RES UNIV;
(ebrk, brk, T, n) ← WHILE⇩T⇗λ(ebrk, brk, T, n). cdcl_twl_stgy_restart_prog_inv S⇩0 brk T n⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(ebrk, brk, S, n).
do {
T ← unit_propagation_outer_loop S;
(brk, T) ← cdcl_twl_o_prog T;
(T, n) ← restart_prog T n brk;
ebrk ← RES UNIV;
RETURN (ebrk, brk, T, n)
})
(ebrk, False, S⇩0, 0);
if ¬brk then do {
(brk, T, _) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_prog_inv S⇩0 brk T n⇖
(λ(brk, _). ¬brk)
(λ(brk, S, n).
do {
T ← unit_propagation_outer_loop S;
(brk, T) ← cdcl_twl_o_prog T;
(T, n) ← restart_prog T n brk;
RETURN (brk, T, n)
})
(False, T, n);
RETURN T
}
else RETURN T
}›
lemma (in twl_restart) cdcl_twl_stgy_prog_early_spec:
assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
‹get_conflict S = None›
shows
‹cdcl_twl_stgy_restart_prog_early S ≤ SPEC(λT. ∃n. cdcl_twl_stgy_restart_with_leftovers (S, 0) (T, n) ∧
final_twl_state T)›
(is ‹_ ≤ SPEC(λT. ?P T)›)
proof -
have final_prop: ‹?P T›
if
inv: ‹case (brk, T, n) of (brk, T, m) ⇒ cdcl_twl_stgy_restart_prog_inv S brk T m› and
‹¬ (case (brk, T, n) of (brk, uu_) ⇒ ¬ brk)›
for brk T n
proof -
have
‹brk› and
‹twl_struct_invs T› and
‹twl_stgy_invs T› and
ns: ‹final_twl_state T› and
twl_left_overs: ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (T, n)› and
‹clauses_to_update T = {#}›
using that unfolding cdcl_twl_stgy_restart_prog_inv_def by auto
obtain S' where
st: ‹cdcl_twl_stgy_restart⇧*⇧* (S, 0) (S', n)› and
S'_T: ‹cdcl_twl_stgy⇧*⇧* S' T›
using twl_left_overs unfolding cdcl_twl_stgy_restart_with_leftovers_def by auto
then show ?thesis
using ns unfolding cdcl_twl_stgy_restart_with_leftovers_def apply -
apply (rule_tac x=n in exI)
apply (rule conjI)
subgoal by (rule_tac x=S' in exI) auto
subgoal by auto
done
qed
show ?thesis
supply RETURN_as_SPEC_refine[refine2 del]
unfolding cdcl_twl_stgy_restart_prog_early_def full_def
apply (refine_vcg
WHILEIT_rule[where
R = ‹{((ebrk, brkT, T, n), (ebrk, brkS, S, m)).
twl_struct_invs S ∧ cdcl_twl_stgy_restart_with_leftovers1 (S, m) (T, n)} ∪
{((ebrkT, brkT, T), (ebrkS, brkS, S)). S = T ∧ (ebrkT ∨ brkT) ∧ (¬brkS ∧ ¬ebrkS)}›]
WHILEIT_rule[where
R = ‹{((brkT, T, n), (brkS, S, m)).
twl_struct_invs S ∧ cdcl_twl_stgy_restart_with_leftovers1 (S, m) (T, n)} ∪
{((brkT, T), (brkS, S)). S = T ∧ brkT ∧ ¬brkS}›];
remove_dummy_vars)
subgoal by (rule wf_cdcl_twl_stgy_restart_measure_early)
subgoal using assms unfolding cdcl_twl_stgy_restart_prog_inv_def
by (fast intro: cdcl_twl_stgy_restart_with_leftovers_refl)
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def
by (simp add: no_step_cdcl_twl_cp_no_step_cdcl⇩W_cp)
subgoal by fast
subgoal for ebrk brk T m x ac bc
by (rule restart_prog_early_spec)
subgoal by (rule wf_cdcl_twl_stgy_restart_measure)
subgoal by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def
by (simp add: no_step_cdcl_twl_cp_no_step_cdcl⇩W_cp)
subgoal by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def
by (rule restart_prog_spec[unfolded cdcl_twl_stgy_restart_prog_inv_def])
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def
by (rule final_prop[unfolded cdcl_twl_stgy_restart_prog_inv_def])
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def
by auto
done
qed
definition cdcl_twl_stgy_restart_prog_bounded :: "'v twl_st ⇒ (bool × 'v twl_st) nres" where
‹cdcl_twl_stgy_restart_prog_bounded S⇩0 =
do {
ebrk ← RES UNIV;
(ebrk, brk, T, n) ← WHILE⇩T⇗λ(ebrk, brk, T, n). cdcl_twl_stgy_restart_prog_inv S⇩0 brk T n⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(ebrk, brk, S, n).
do {
T ← unit_propagation_outer_loop S;
(brk, T) ← cdcl_twl_o_prog T;
(T, n) ← restart_prog T n brk;
ebrk ← RES UNIV;
RETURN (ebrk, brk, T, n)
})
(ebrk, False, S⇩0, 0);
RETURN (brk, T)
}›
lemma (in twl_restart) cdcl_twl_stgy_prog_bounded_spec:
assumes ‹twl_struct_invs S› and ‹twl_stgy_invs S› and ‹clauses_to_update S = {#}› and
‹get_conflict S = None›
shows
‹cdcl_twl_stgy_restart_prog_bounded S ≤ SPEC(λ(brk, T). ∃n. cdcl_twl_stgy_restart_with_leftovers (S, 0) (T, n) ∧
(brk ⟶ final_twl_state T))›
(is ‹_ ≤ SPEC ?P›)
proof -
have final_prop: ‹?P (brk, T)›
if
inv: ‹case (brk, T, n) of (brk, T, m) ⇒ cdcl_twl_stgy_restart_prog_inv S brk T m›
for brk T n
proof -
have
‹twl_struct_invs T› and
‹twl_stgy_invs T› and
ns: ‹brk ⟶ final_twl_state T› and
twl_left_overs: ‹cdcl_twl_stgy_restart_with_leftovers (S, 0) (T, n)› and
‹clauses_to_update T = {#}›
using that unfolding cdcl_twl_stgy_restart_prog_inv_def by auto
obtain S' where
st: ‹cdcl_twl_stgy_restart⇧*⇧* (S, 0) (S', n)› and
S'_T: ‹cdcl_twl_stgy⇧*⇧* S' T›
using twl_left_overs unfolding cdcl_twl_stgy_restart_with_leftovers_def by auto
then show ?thesis
using ns unfolding cdcl_twl_stgy_restart_with_leftovers_def prod.case apply -
apply (rule_tac x=n in exI)
apply (rule conjI)
subgoal by (rule_tac x=S' in exI) auto
subgoal by auto
done
qed
show ?thesis
supply RETURN_as_SPEC_refine[refine2 del]
unfolding cdcl_twl_stgy_restart_prog_bounded_def full_def
apply (refine_vcg
WHILEIT_rule[where
R = ‹{((ebrk, brkT, T, n), (ebrk, brkS, S, m)).
twl_struct_invs S ∧ cdcl_twl_stgy_restart_with_leftovers1 (S, m) (T, n)} ∪
{((ebrkT, brkT, T), (ebrkS, brkS, S)). S = T ∧ (ebrkT ∨ brkT) ∧ (¬brkS ∧ ¬ebrkS)}›];
remove_dummy_vars)
subgoal by (rule wf_cdcl_twl_stgy_restart_measure_early)
subgoal using assms unfolding cdcl_twl_stgy_restart_prog_inv_def
by (fast intro: cdcl_twl_stgy_restart_with_leftovers_refl)
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def by fast
subgoal unfolding cdcl_twl_stgy_restart_prog_inv_def
by (simp add: no_step_cdcl_twl_cp_no_step_cdcl⇩W_cp)
subgoal by fast
subgoal for ebrk brk T m x ac bc
by (rule restart_prog_early_spec)
subgoal
unfolding cdcl_twl_stgy_restart_prog_inv_def prod.case
by (rule final_prop[unfolded prod.case cdcl_twl_stgy_restart_prog_inv_def])
done
qed
end
end