theory Watched_Literals_List_Restart
imports Watched_Literals_List Watched_Literals_Algorithm_Restart
begin
text ‹
Unlike most other refinements steps we have done, we don't try to refine our
specification to our code directly: We first introduce an intermediate transition system which
is closer to what we want to implement. Then we refine it to code.
›
text ‹
This invariant abstract over the restart operation on the trail. There can be a backtracking on
the trail and there can be a renumbering of the indexes.
›
inductive valid_trail_reduction for M M' :: ‹('v ,'c) ann_lits› where
backtrack_red:
‹valid_trail_reduction M M'›
if
‹(Decided K # M'', M2) ∈ set (get_all_ann_decomposition M)› and
‹map lit_of M'' = map lit_of M'› and
‹map is_decided M'' = map is_decided M'› |
keep_red:
‹valid_trail_reduction M M'›
if
‹map lit_of M = map lit_of M'› and
‹map is_decided M = map is_decided M'›
lemma valid_trail_reduction_simps: ‹valid_trail_reduction M M' ⟷
((∃K M'' M2. (Decided K # M'', M2) ∈ set (get_all_ann_decomposition M) ∧
map lit_of M'' = map lit_of M' ∧ map is_decided M'' = map is_decided M' ∧
length M' = length M'') ∨
map lit_of M = map lit_of M' ∧ map is_decided M = map is_decided M' ∧ length M = length M')›
apply (auto simp: valid_trail_reduction.simps dest: arg_cong[of ‹map lit_of _› _ length])
apply (force dest: arg_cong[of ‹map lit_of _› _ length])+
done
lemma trail_changes_same_decomp:
assumes
M'_lit: ‹map lit_of M' = map lit_of ysa @ L # map lit_of zsa› and
M'_dec: ‹map is_decided M' = map is_decided ysa @ False # map is_decided zsa›
obtains C' M2 M1 where ‹M' = M2 @ Propagated L C' # M1› and
‹map lit_of M2 = map lit_of ysa›and
‹map is_decided M2 = map is_decided ysa› and
‹map lit_of M1 = map lit_of zsa› and
‹map is_decided M1 = map is_decided zsa›
proof -
define M1 M2 K where ‹M1 ≡ drop (Suc (length ysa)) M'› and ‹M2 ≡ take (length ysa) M'› and
‹K ≡ hd (drop (length ysa) M')›
have
M': ‹M' = M2 @ K # M1›
using arg_cong[OF M'_lit, of length] unfolding M1_def M2_def K_def
by (simp add: Cons_nth_drop_Suc hd_drop_conv_nth)
have [simp]:
‹length M2 = length ysa›
‹length M1 = length zsa›
using arg_cong[OF M'_lit, of length] unfolding M1_def M2_def K_def by auto
obtain C' where
[simp]: ‹K = Propagated L C'›
using M'_lit M'_dec unfolding M'
by (cases K) auto
show ?thesis
using that[of M2 C' M1] M'_lit M'_dec unfolding M'
by auto
qed
lemma
assumes
‹map lit_of M = map lit_of M'› and
‹map is_decided M = map is_decided M'›
shows
trail_renumber_count_dec:
‹count_decided M = count_decided M'› and
trail_renumber_get_level:
‹get_level M L = get_level M' L›
proof -
have [dest]: ‹count_decided M = count_decided M'›
if ‹map is_decided M = map is_decided M'› for M M'
using that
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: get_level_cons_if)
subgoal for L C M M'
by (cases M')
(auto simp: get_level_cons_if)
done
then show ‹count_decided M = count_decided M'› using assms by blast
show ‹get_level M L = get_level M' L›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M'; cases ‹hd M'›)
(auto simp: get_level_cons_if)
subgoal for L C M M'
by (cases M')
(auto simp: get_level_cons_if)
done
qed
lemma valid_trail_reduction_Propagated_inD:
‹valid_trail_reduction M M' ⟹ Propagated L C ∈ set M' ⟹ ∃C'. Propagated L C' ∈ set M›
by (induction rule: valid_trail_reduction.induct)
(force dest!: get_all_ann_decomposition_exists_prepend
dest!: split_list[of ‹Propagated L C›] elim!: trail_changes_same_decomp)+
lemma valid_trail_reduction_Propagated_inD2:
‹valid_trail_reduction M M' ⟹ length M = length M' ⟹ Propagated L C ∈ set M ⟹
∃C'. Propagated L C' ∈ set M'›
apply (induction rule: valid_trail_reduction.induct)
apply (auto dest!: get_all_ann_decomposition_exists_prepend
dest!: split_list[of ‹Propagated L C›] elim!: trail_changes_same_decomp)+
apply (metis add_Suc_right le_add2 length_Cons length_append length_map not_less_eq_eq)
by (metis (no_types, lifting) in_set_conv_decomp trail_changes_same_decomp)
lemma get_all_ann_decomposition_change_annotation_exists:
assumes
‹(Decided K # M', M2') ∈ set (get_all_ann_decomposition M2)› and
‹map lit_of M1 = map lit_of M2› and
‹map is_decided M1 = map is_decided M2›
shows ‹∃M'' M2'. (Decided K # M'', M2') ∈ set (get_all_ann_decomposition M1) ∧
map lit_of M'' = map lit_of M' ∧ map is_decided M'' = map is_decided M'›
using assms
proof (induction M1 arbitrary: M2 M2' rule: ann_lit_list_induct)
case Nil
then show ?case by auto
next
case (Decided L xs M2)
then show ?case
by (cases M2; cases ‹hd M2›) fastforce+
next
case (Propagated L m xs M2) note IH = this(1) and prems = this(2-)
show ?case
using IH[of _ ‹tl M2›] prems get_all_ann_decomposition_decomp[of xs]
get_all_ann_decomposition_decomp[of M2 ‹Decided K # M'›]
by (cases M2; cases ‹hd M2›; cases ‹(get_all_ann_decomposition (tl M2))›;
cases ‹hd (get_all_ann_decomposition xs)›; cases ‹get_all_ann_decomposition xs›)
fastforce+
qed
lemma valid_trail_reduction_trans:
assumes
M1_M2: ‹valid_trail_reduction M1 M2› and
M2_M3: ‹valid_trail_reduction M2 M3›
shows ‹valid_trail_reduction M1 M3›
proof -
consider
(same) ‹map lit_of M2 = map lit_of M3› and
‹map is_decided M2 = map is_decided M3› ‹length M2 = length M3› |
(decomp_M1) K M'' M2' where
‹(Decided K # M'', M2') ∈ set (get_all_ann_decomposition M2)› and
‹map lit_of M'' = map lit_of M3› and
‹map is_decided M'' = map is_decided M3› and
‹length M3 = length M''›
using M2_M3 unfolding valid_trail_reduction_simps
by auto
note decomp_M2 = this
consider
(same) ‹map lit_of M1 = map lit_of M2› and
‹map is_decided M1 = map is_decided M2› ‹length M1 = length M2› |
(decomp_M1) K M'' M2' where
‹(Decided K # M'', M2') ∈ set (get_all_ann_decomposition M1)› and
‹map lit_of M'' = map lit_of M2› and
‹map is_decided M'' = map is_decided M2› and
‹length M2 = length M''›
using M1_M2 unfolding valid_trail_reduction_simps
by auto
then show ?thesis
proof cases
case same
from decomp_M2
show ?thesis
proof cases
case same': same
then show ?thesis
using same by (auto simp: valid_trail_reduction_simps)
next
case decomp_M1 note decomp = this(1) and eq = this(2,3) and [simp] = this(4)
obtain M4 M5 where
decomp45: ‹(Decided K # M4, M5) ∈ set (get_all_ann_decomposition M1)› and
M4_lit: ‹map lit_of M4 = map lit_of M''› and
M4_dec: ‹map is_decided M4 = map is_decided M''›
using get_all_ann_decomposition_change_annotation_exists[OF decomp, of M1] eq same
by (auto simp: valid_trail_reduction_simps)
show ?thesis
by (rule valid_trail_reduction.backtrack_red[OF decomp45])
(use M4_lit M4_dec eq same in auto)
qed
next
case decomp_M1 note decomp = this(1) and eq = this(2,3) and [simp] = this(4)
from decomp_M2
show ?thesis
proof cases
case same
obtain M4 M5 where
decomp45: ‹(Decided K # M4, M5) ∈ set (get_all_ann_decomposition M1)› and
M4_lit: ‹map lit_of M4 = map lit_of M''› and
M4_dec: ‹map is_decided M4 = map is_decided M''›
using get_all_ann_decomposition_change_annotation_exists[OF decomp, of M1] eq same
by (auto simp: valid_trail_reduction_simps)
show ?thesis
by (rule valid_trail_reduction.backtrack_red[OF decomp45])
(use M4_lit M4_dec eq same in auto)
next
case (decomp_M1 K' M''' M2''') note decomp' = this(1) and eq' = this(2,3) and [simp] = this(4)
obtain M4 M5 where
decomp45: ‹(Decided K' # M4, M5) ∈ set (get_all_ann_decomposition M'')› and
M4_lit: ‹map lit_of M4 = map lit_of M'''› and
M4_dec: ‹map is_decided M4 = map is_decided M'''›
using get_all_ann_decomposition_change_annotation_exists[OF decomp', of M''] eq
by (auto simp: valid_trail_reduction_simps)
obtain M6 where
decomp45: ‹(Decided K' # M4, M6) ∈ set (get_all_ann_decomposition M1)›
using get_all_ann_decomposition_exists_prepend[OF decomp45]
get_all_ann_decomposition_exists_prepend[OF decomp]
get_all_ann_decomposition_ex[of K' M4 ‹_ @ M2' @ Decided K # _ @ M5›]
by (auto simp: valid_trail_reduction_simps)
show ?thesis
by (rule valid_trail_reduction.backtrack_red[OF decomp45])
(use M4_lit M4_dec eq decomp_M1 in auto)
qed
qed
qed
lemma valid_trail_reduction_length_leD: ‹valid_trail_reduction M M' ⟹ length M' ≤ length M›
by (auto simp: valid_trail_reduction_simps)
lemma valid_trail_reduction_level0_iff:
assumes valid: ‹valid_trail_reduction M M'› and n_d: ‹no_dup M›
shows ‹(L ∈ lits_of_l M ∧ get_level M L = 0) ⟷ (L ∈ lits_of_l M' ∧ get_level M' L = 0)›
proof -
have H[intro]: ‹map lit_of M = map lit_of M' ⟹ L ∈ lits_of_l M ⟹ L ∈ lits_of_l M'› for M M'
by (metis lits_of_def set_map)
have [dest]: ‹undefined_lit c L ⟹ L ∈ lits_of_l c ⟹ False› for c
by (auto dest: in_lits_of_l_defined_litD)
show ?thesis
using valid
proof cases
case keep_red
then show ?thesis
by (metis H trail_renumber_get_level)
next
case (backtrack_red K M'' M2) note decomp = this(1) and eq = this(2,3)
obtain M3 where M: ‹M = M3 @ Decided K # M''›
using decomp by auto
have ‹(L ∈ lits_of_l M ∧ get_level M L = 0) ⟷
(L ∈ lits_of_l M'' ∧ get_level M'' L = 0)›
using n_d unfolding M
by (auto 4 4 simp: valid_trail_reduction_simps get_level_append_if get_level_cons_if
atm_of_eq_atm_of
dest: in_lits_of_l_defined_litD no_dup_append_in_atm_notin
split: if_splits)
also have ‹... ⟷ (L ∈ lits_of_l M' ∧ get_level M' L = 0)›
using eq by (metis local.H trail_renumber_get_level)
finally show ?thesis
by blast
qed
qed
lemma map_lit_of_eq_defined_litD: ‹map lit_of M = map lit_of M' ⟹ defined_lit M = defined_lit M'›
apply (induction M arbitrary: M')
subgoal by auto
subgoal for L M M'
by (cases M'; cases L; cases "hd M'")
(auto simp: defined_lit_cons)
done
lemma map_lit_of_eq_no_dupD: ‹map lit_of M = map lit_of M' ⟹ no_dup M = no_dup M'›
apply (induction M arbitrary: M')
subgoal by auto
subgoal for L M M'
by (cases M'; cases L; cases "hd M'")
(auto dest: map_lit_of_eq_defined_litD)
done
text ‹
Remarks about the predicate:
▪ The cases \<^term>‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ E = 0 ⟶
E' ≠ 0 ⟶ P› are already covered by the invariants (where \<^term>‹P› means that there is
clause which was already present before).
›
inductive cdcl_twl_restart_l :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
restart_trail:
‹cdcl_twl_restart_l (M, N, None, NE, UE, {#}, Q)
(M', N', None, NE + mset `# NE', UE + mset `# UE', {#}, Q')›
if
‹valid_trail_reduction M M'› and
‹init_clss_lf N = init_clss_lf N' + NE'› and
‹learned_clss_lf N' + UE' ⊆# learned_clss_lf N› and
‹∀E∈# (NE'+UE'). ∃L∈set E. L ∈ lits_of_l M ∧ get_level M L = 0› and
‹∀L E E' . Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ E > 0 ⟶ E' > 0 ⟶
E ∈# dom_m N' ∧ N' ∝ E = N ∝ E'› and
‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ E = 0 ⟶ E' ≠ 0 ⟶
mset (N ∝ E') ∈# NE + mset `# NE' + UE + mset `# UE'› and
‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ E' = 0 ⟶ E = 0› and
‹0 ∉# dom_m N'› and
‹if length M = length M' then Q = Q' else Q' = {#}›
lemma cdcl_twl_restart_l_list_invs:
assumes
‹cdcl_twl_restart_l S T› and
‹twl_list_invs S›
shows
‹twl_list_invs T›
using assms
proof (induction rule: cdcl_twl_restart_l.induct)
case (restart_trail M M' N N' NE' UE' NE UE Q Q') note red = this(1) and init = this(2) and
learned = this(3) and NUE = this(4) and tr_ge0 = this(5) and tr_new0 = this(6) and
tr_still0 = this(7) and dom0 = this(8) and QQ' = this(9) and list_invs = this(10)
let ?S = ‹(M, N, None, NE, UE, {#}, Q)›
let ?T = ‹(M', N', None, NE + mset `# NE', UE + mset `# UE', {#}, Q')›
show ?case
unfolding twl_list_invs_def
proof (intro conjI impI allI ballI)
fix C
assume ‹C ∈# clauses_to_update_l ?T›
then show ‹C ∈# dom_m (get_clauses_l ?T)›
by simp
next
show ‹0 ∉# dom_m (get_clauses_l ?T)›
using dom0 by simp
next
fix L C
assume LC: ‹Propagated L C ∈ set (get_trail_l ?T)› and C0: ‹0 < C›
then obtain C' where LC': ‹Propagated L C' ∈ set (get_trail_l ?S)›
using red by (auto dest!: valid_trail_reduction_Propagated_inD)
moreover have C'0: ‹C' ≠ 0›
apply (rule ccontr)
using C0 tr_still0 LC LC'
by (auto simp: twl_list_invs_def
dest!: valid_trail_reduction_Propagated_inD)
ultimately have C_dom: ‹C ∈# dom_m (get_clauses_l ?T)› and NCC': ‹N' ∝ C = N ∝ C'›
using tr_ge0 C0 LC by auto
show ‹C ∈# dom_m (get_clauses_l ?T)›
using C_dom .
have
L_watched: ‹L ∈ set (watched_l (get_clauses_l ?S ∝ C'))› and
L_C'0: ‹length (get_clauses_l ?S ∝ C') > 2 ⟹ L = get_clauses_l ?S ∝ C' ! 0›
using list_invs C'0 LC' unfolding twl_list_invs_def
by auto
show ‹L ∈ set (watched_l (get_clauses_l ?T ∝ C))›
using L_watched NCC' by simp
show ‹length (get_clauses_l ?T ∝ C) > 2 ⟹ L = get_clauses_l ?T ∝ C ! 0›
using L_C'0 NCC' by simp
next
show ‹distinct_mset (clauses_to_update_l ?T)›
by auto
qed
qed
lemma rtranclp_cdcl_twl_restart_l_list_invs:
assumes
‹cdcl_twl_restart_l⇧*⇧* S T› and
‹twl_list_invs S›
shows
‹twl_list_invs T›
using assms by induction (auto intro: cdcl_twl_restart_l_list_invs)
lemma cdcl_twl_restart_l_cdcl_twl_restart:
assumes ST: ‹(S, T) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S› and
struct_invs: ‹twl_struct_invs T›
shows ‹SPEC (cdcl_twl_restart_l S) ≤ ⇓ {(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧
clauses_to_update_l S = {#}}
(SPEC (cdcl_twl_restart T))›
proof -
have [simp]: ‹set (watched_l x) ∪ set (unwatched_l x) = set x› for x
by (metis append_take_drop_id set_append)
have ‹∃T'. cdcl_twl_restart T T' ∧ (S', T') ∈ twl_st_l None›
if ‹cdcl_twl_restart_l S S'› for S'
using that ST struct_invs
proof (induction rule: cdcl_twl_restart_l.induct)
case (restart_trail M M' N N' NE' UE' NE UE Q Q') note red = this(1) and init = this(2) and
learned = this(3) and NUE = this(4) and tr_ge0 = this(5) and tr_new0 = this(6) and
tr_still0 = this(7) and dom0 = this(8) and QQ' = this(9) and ST = this(10) and
struct_invs = this(11)
let ?T' = ‹(drop (length M - length M') (get_trail T), twl_clause_of `# init_clss_lf N',
twl_clause_of `# learned_clss_lf N', None, NE+mset `# NE', UE+mset `# UE', {#}, Q')›
have [intro]: ‹Q ≠ Q' ⟹ Q' = {#}›
using QQ' by (auto split: if_splits)
obtain TM where
T: ‹T = (TM, twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N, None,
NE, UE, {#}, Q)› and
M_TM: ‹(M, TM) ∈ convert_lits_l N (NE+UE)›
using ST
by (cases T) (auto simp: twl_st_l_def)
have ‹no_dup TM›
using struct_invs unfolding T twl_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (simp add: trail.simps)
then have n_d: ‹no_dup M›
using M_TM by auto
have ‹cdcl_twl_restart T ?T'›
using red
proof (induction)
case keep_red
from arg_cong[OF this(1), of length] have [simp]: ‹length M = length M'› by simp
have [simp]: ‹Q = Q'›
using QQ' by simp
have annot_in_clauses: ‹∀L E. Propagated L E ∈ set TM ⟶
E ∈# clauses
(twl_clause_of `# init_clss_lf N +
twl_clause_of `# learned_clss_lf N') +
NE +
UE +
clauses (twl_clause_of `# UE')›
proof (intro allI impI conjI)
fix L E
assume ‹Propagated L E ∈ set TM›
then obtain E' where LE'_M: ‹Propagated L E' ∈ set M› and
E_E': ‹convert_lit N (NE+UE) (Propagated L E') (Propagated L E)›
using in_convert_lits_lD[OF _ M_TM, of ‹Propagated L E›]
by (auto simp: convert_lit.simps)
then obtain E'' where LE''_M: ‹Propagated L E'' ∈ set M'›
using valid_trail_reduction_Propagated_inD2[OF red, of L E'] by auto
consider
‹E' = 0› and ‹E'' = 0› |
‹E' > 0› and ‹E'' = 0› and ‹mset (N ∝ E') ∈# NE + mset `# NE' + UE + mset `# UE'› |
‹E' > 0› and ‹E'' > 0› and ‹E'' ∈# dom_m N'› and ‹N ∝ E' = N' ∝ E''›
using tr_ge0 tr_new0 tr_still0 LE'_M LE''_M E_E'
by (cases ‹E''>0›; cases ‹E' > 0›) auto
then show ‹E ∈# clauses
(twl_clause_of `# init_clss_lf N +
twl_clause_of `# learned_clss_lf N') +
NE +
UE +
clauses (twl_clause_of `# UE')›
apply cases
subgoal
using E_E'
by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
subgoal
using E_E' init
by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
subgoal
using E_E' init
by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
done
qed
have ‹cdcl_twl_restart
(TM, twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N, None,
NE, UE, {#}, Q)
(TM, twl_clause_of `# init_clss_lf N', twl_clause_of `# learned_clss_lf N', None,
NE + clauses (twl_clause_of `# NE'), UE + clauses (twl_clause_of `# UE'), {#},
Q)› (is ‹cdcl_twl_restart ?A ?B›)
apply (rule cdcl_twl_restart.restart_clauses)
subgoal
using learned by (auto dest: image_mset_subseteq_mono)
subgoal unfolding init image_mset_union by auto
subgoal using NUE M_TM by auto
subgoal by (rule annot_in_clauses)
done
moreover have ‹?A = T›
unfolding T by simp
moreover have ‹?B = ?T'›
by (auto simp: T mset_take_mset_drop_mset')
ultimately show ?case
by argo
next
case (backtrack_red K M2 M'') note decomp = this(1)
have [simp]: ‹length M2 = length M'›
using arg_cong[OF backtrack_red(2), of length] by simp
have M_TM: ‹(drop (length M - length M') M, drop (length M - length M') TM) ∈
convert_lits_l N (NE+UE)›
using M_TM unfolding convert_lits_l_def list_rel_def by auto
have red: ‹valid_trail_reduction (drop (length M - length M') M) M'›
using red backtrack_red by (auto simp: valid_trail_reduction.simps)
have annot_in_clauses: ‹∀L E. Propagated L E ∈ set (drop (length M - length M') TM) ⟶
E ∈# clauses
(twl_clause_of `# init_clss_lf N +
twl_clause_of `# learned_clss_lf N') +
NE +
UE +
clauses (twl_clause_of `# UE')›
proof (intro allI impI conjI)
fix L E
assume ‹Propagated L E ∈ set (drop (length M - length M') TM)›
then obtain E' where LE'_M: ‹Propagated L E' ∈ set (drop (length M - length M') M)› and
E_E': ‹convert_lit N (NE+UE) (Propagated L E') (Propagated L E)›
using in_convert_lits_lD[OF _ M_TM, of ‹Propagated L E›]
by (auto simp: convert_lit.simps)
then have ‹Propagated L E' ∈ set M2›
using decomp by (auto dest!: get_all_ann_decomposition_exists_prepend)
then obtain E'' where LE''_M: ‹Propagated L E'' ∈ set M'›
using valid_trail_reduction_Propagated_inD2[OF red, of L E'] decomp
by (auto dest!: get_all_ann_decomposition_exists_prepend)
consider
‹E' = 0› and ‹E'' = 0› |
‹E' > 0› and ‹E'' = 0› and ‹mset (N ∝ E') ∈# NE + mset `# NE' + UE + mset `# UE'› |
‹E' > 0› and ‹E'' > 0› and ‹E'' ∈# dom_m N'› and ‹N ∝ E' = N' ∝ E''›
using tr_ge0 tr_new0 tr_still0 LE'_M LE''_M E_E' decomp
by (cases ‹E''>0›; cases ‹E' > 0›)
(auto 5 5 dest!: get_all_ann_decomposition_exists_prepend
simp: convert_lit.simps)
then show ‹E ∈# clauses
(twl_clause_of `# init_clss_lf N +
twl_clause_of `# learned_clss_lf N') +
NE +
UE +
clauses (twl_clause_of `# UE')›
apply cases
subgoal
using E_E'
by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
subgoal
using E_E' init
by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
subgoal
using E_E' init
by (auto simp: mset_take_mset_drop_mset' convert_lit.simps)
done
qed
have lits_of_M2_M': ‹lits_of_l M2 = lits_of_l M'›
using arg_cong[OF backtrack_red(2), of set] by (auto simp: lits_of_def)
have lev_M2_M': ‹get_level M2 L = get_level M' L› for L
using trail_renumber_get_level[OF backtrack_red(2-3)] by (auto simp: )
have drop_M_M2: ‹drop (length M - length M') M = M2›
using backtrack_red(1) by auto
have H: ‹L ∈ lits_of_l (drop (length M - length M') TM) ∧
get_level (drop (length M - length M') TM) L = 0›
if ‹L ∈ lits_of_l M ∧ get_level M L = 0› for L
proof -
have ‹L ∈ lits_of_l M2 ∧ get_level M2 L = 0›
using decomp that n_d
by (auto dest!: get_all_ann_decomposition_exists_prepend
dest: in_lits_of_l_defined_litD
simp: get_level_append_if get_level_cons_if split: if_splits)
then show ?thesis
using M_TM
by (auto dest!: simp: drop_M_M2)
qed
have
‹∃M2. (Decided K # drop (length M - length M') TM, M2) ∈ set (get_all_ann_decomposition TM)›
using convert_lits_l_decomp_ex[OF decomp ‹(M, TM) ∈ convert_lits_l N (NE + UE)›]
‹(M, TM) ∈ convert_lits_l N (NE + UE)›
by (simp add: convert_lits_l_imp_same_length)
then obtain TM2 where decomp_TM:
‹(Decided K # drop (length M - length M') TM, TM2) ∈ set (get_all_ann_decomposition TM)›
by blast
have ‹cdcl_twl_restart
(TM, twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N, None,
NE, UE, {#}, Q)
(drop (length M - length M') TM, twl_clause_of `# init_clss_lf N',
twl_clause_of `# learned_clss_lf N', None,
NE + clauses (twl_clause_of `# NE'), UE + clauses (twl_clause_of `# UE'), {#},
{#})› (is ‹cdcl_twl_restart ?A ?B›)
apply (rule cdcl_twl_restart.restart_trail)
apply (rule decomp_TM)
subgoal
using learned by (auto dest: image_mset_subseteq_mono)
subgoal unfolding init image_mset_union by auto
subgoal using NUE M_TM H by fastforce
subgoal by (rule annot_in_clauses)
done
moreover have ‹?A = T›
unfolding T by auto
moreover have ‹?B = ?T'›
using QQ' decomp unfolding T by (auto simp: mset_take_mset_drop_mset')
ultimately show ?case
by argo
qed
moreover {
have ‹(M', drop (length M - length M') TM) ∈ convert_lits_l N' (NE + mset `# NE' + (UE + mset `# UE'))›
proof (rule convert_lits_lI)
show ‹length M' = length (drop (length M - length M') TM)›
using M_TM red by (auto simp: valid_trail_reduction.simps T
dest: convert_lits_l_imp_same_length
dest!: arg_cong[of ‹map lit_of _› _ length] get_all_ann_decomposition_exists_prepend)
fix i
assume i_M': ‹i < length M'›
then have MM'_IM: ‹length M - length M' + i < length M› ‹length M - length M' + i < length TM›
using M_TM red by (auto simp: valid_trail_reduction.simps T
dest: convert_lits_l_imp_same_length
dest!: arg_cong[of ‹map lit_of _› _ length] get_all_ann_decomposition_exists_prepend)
then have ‹convert_lit N (NE + UE) (drop (length M - length M') M ! i)
(drop (length M - length M') TM ! i)›
using M_TM list_all2_nthD[of ‹convert_lit N (NE + UE)› M TM ‹length M - length M' + i›] i_M'
unfolding convert_lits_l_def list_rel_def p2rel_def
by auto
moreover
have ‹lit_of (drop (length M - length M') M!i) = lit_of (M'!i)› and
‹is_decided (drop (length M - length M') M!i) = is_decided (M'!i)›
using red i_M' MM'_IM
by (auto 5 5 simp:valid_trail_reduction_simps nth_append
dest: map_eq_nth_eq[of _ _ _ i]
dest!: get_all_ann_decomposition_exists_prepend)
moreover have ‹M'!i ∈ set M'›
using i_M' by auto
moreover have ‹drop (length M - length M') M!i ∈ set M›
using MM'_IM by auto
ultimately show ‹convert_lit N' (NE + mset `# NE' + (UE + mset `# UE')) (M' ! i)
(drop (length M - length M') TM ! i)›
using tr_new0 tr_still0 tr_ge0
by (cases ‹M'!i›) (fastforce simp: convert_lit.simps)+
qed
then have ‹((M', N', None, NE + mset `# NE', UE + mset `# UE', {#}, Q'), ?T')
∈ twl_st_l None›
using M_TM by (auto simp: twl_st_l_def T)
}
ultimately show ?case
by fast
qed
moreover have ‹cdcl_twl_restart_l S S' ⟹ twl_list_invs S'› for S'
by (rule cdcl_twl_restart_l_list_invs) (use list_invs in fast)+
moreover have ‹cdcl_twl_restart_l S S' ⟹ clauses_to_update_l S' = {#}› for S'
by (auto simp: cdcl_twl_restart_l.simps)
ultimately show ?thesis
by (blast intro!: RES_refine)
qed
definition (in -) restart_abs_l_pre :: ‹'v twl_st_l ⇒ bool ⇒ bool› where
‹restart_abs_l_pre S brk ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧ restart_prog_pre S' brk
∧ twl_list_invs S ∧ clauses_to_update_l S = {#})›
context twl_restart_ops
begin
definition restart_required_l :: "'v twl_st_l ⇒ nat ⇒ bool nres" where
‹restart_required_l S n = SPEC (λb. b ⟶ size (get_learned_clss_l S) > f n)›
definition restart_abs_l
:: "'v twl_st_l ⇒ nat ⇒ bool ⇒ ('v twl_st_l × nat) nres"
where
‹restart_abs_l S n brk = do {
ASSERT(restart_abs_l_pre S brk);
b ← restart_required_l S n;
b2 ← SPEC (λ(_ ::bool). True);
if b ∧ b2 ∧ ¬brk then do {
T ← SPEC(λT. cdcl_twl_restart_l S T);
RETURN (T, n + 1)
}
else
if b ∧ ¬brk then do {
T ← SPEC(λT. cdcl_twl_restart_l S T);
RETURN (T, n + 1)
}
else
RETURN (S, 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:
‹(uncurry restart_required_l, uncurry restart_required) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S} ×⇩f nat_rel →⇩f
⟨bool_rel⟩ nres_rel›
unfolding restart_required_l_def restart_required_def uncurry_def
by (intro frefI nres_relI) (auto simp: twl_st_l_def get_learned_clss_l_def)
lemma restart_abs_l_restart_prog:
‹(uncurry2 restart_abs_l, uncurry2 restart_prog) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}}
×⇩f nat_rel ×⇩f bool_rel →⇩f
⟨{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}}
×⇩f nat_rel⟩ nres_rel›
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_curry]
cdcl_twl_restart_l_cdcl_twl_restart)
subgoal for Snb Snb'
unfolding restart_abs_l_pre_def
by (rule exI[of _ ‹fst (fst (Snb'))›]) simp
subgoal by simp
subgoal by auto
subgoal by simp
subgoal by simp
subgoal unfolding restart_prog_pre_def by meson
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal unfolding restart_prog_pre_def by meson
subgoal by auto
subgoal by auto
done
definition cdcl_twl_stgy_restart_abs_l_inv where
‹cdcl_twl_stgy_restart_abs_l_inv S⇩0 brk T n ≡
(∃S⇩0' T'.
(S⇩0, S⇩0') ∈ twl_st_l None ∧
(T, T') ∈ twl_st_l None ∧
cdcl_twl_stgy_restart_prog_inv S⇩0' brk T' 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⇩0 =
do {
(brk, T, _) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_abs_l_inv S⇩0 brk T n⇖
(λ(brk, _). ¬brk)
(λ(brk, S, n).
do {
T ← unit_propagation_outer_loop_l S;
(brk, T) ← cdcl_twl_o_prog_l T;
(T, n) ← restart_abs_l T n brk;
RETURN (brk, T, n)
})
(False, S⇩0, 0);
RETURN T
}›
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, 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 = ‹{((brk :: bool, S, n :: nat), (brk', S', n')).
(S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ brk = brk' ∧ n = n' ∧
clauses_to_update_l S = {#}}›]
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])
subgoal by simp
subgoal for x y xa x' x1 x2 x1a x2a
unfolding cdcl_twl_stgy_restart_abs_l_inv_def
apply (rule_tac x=y in exI)
apply (rule_tac x=‹fst (snd x')› in exI)
by auto
subgoal by fast
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
done
end
text ‹
We here start the refinement towards an executable version of the restarts. The idea of the
restart is the following:
▸ We backtrack to level 0. This simplifies further steps.
▸ We first move all clause annotating a literal to \<^term>‹NE› or \<^term>‹UE›.
▸ Then, we move remaining clauses that are watching the some literal at level 0.
▸ Now we can safely deleting any remaining learned clauses.
▸ Once all that is done, we have to recalculate the watch lists (and can on the way GC the set of
clauses).
›
subsubsection ‹Handle true clauses from the trail›
lemma in_set_mset_eq_in:
‹i ∈ set A ⟹ mset A = B ⟹ i ∈# B›
by fastforce
text ‹Our transformation will be chains of a weaker version of restarts, that don't update the
watch lists and only keep partial correctness of it.
›
lemma cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l:
assumes
ST: ‹cdcl_twl_restart_l S T› and TU: ‹cdcl_twl_restart_l T U› and
n_d: ‹no_dup (get_trail_l S)›
shows ‹cdcl_twl_restart_l S U›
using assms
proof -
obtain M M' N N' NE' UE' NE UE Q Q' W' W where
S: ‹S = (M, N, None, NE, UE, W, Q)› and
T: ‹T = (M', N', None, NE + mset `# NE', UE + mset `# UE', W', Q')› and
tr_red: ‹valid_trail_reduction M M'› and
init: ‹init_clss_lf N = init_clss_lf N' + NE'› and
learned: ‹learned_clss_lf N' + UE' ⊆# learned_clss_lf N› and
NUE: ‹∀E∈#NE' + UE'. ∃L∈set E. L ∈ lits_of_l M ∧ get_level M L = 0› and
ge0: ‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ 0 < E ⟶ 0 < E' ⟶
E ∈# dom_m N' ∧ N' ∝ E = N ∝ E'› and
new0: ‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶ E = 0 ⟶
E' ≠ 0 ⟶ mset (N ∝ E') ∈# NE + mset `# NE' + UE + mset `# UE'› and
still0: ‹∀L E E'. Propagated L E ∈ set M' ⟶ Propagated L E' ∈ set M ⟶
E' = 0 ⟶ E = 0› and
dom0: ‹0 ∉# dom_m N'› and
QQ': ‹if length M = length M' then Q = Q' else Q' = {#}› and
W: ‹W = {#}›
using ST unfolding cdcl_twl_restart_l.simps
apply -
apply normalize_goal+
by blast
obtain M'' N'' NE'' UE'' Q'' W'' where
U: ‹U = (M'', N'', None, NE + mset `# NE' + mset `# NE'', UE + mset `# UE' + mset `# UE'', W'',
Q'')› and
tr_red': ‹valid_trail_reduction M' M''› and
init': ‹init_clss_lf N' = init_clss_lf N'' + NE''› and
learned': ‹learned_clss_lf N'' + UE'' ⊆# learned_clss_lf N'› and
NUE': ‹∀E∈#NE'' + UE''.
∃L∈set E.
L ∈ lits_of_l M' ∧
get_level M' L = 0› and
ge0': ‹∀L E E'.
Propagated L E ∈ set M'' ⟶
Propagated L E' ∈ set M' ⟶
0 < E ⟶
0 < E' ⟶
E ∈# dom_m N'' ∧ N'' ∝ E = N' ∝ E'› and
new0': ‹∀L E E'.
Propagated L E ∈ set M'' ⟶
Propagated L E' ∈ set M' ⟶
E = 0 ⟶
E' ≠ 0 ⟶
mset (N' ∝ E')
∈# NE + mset `# NE' + mset `# NE'' +
(UE + mset `# UE') +
mset `# UE''› and
still0': ‹∀L E E'.
Propagated L E ∈ set M'' ⟶
Propagated L E' ∈ set M' ⟶
E' = 0 ⟶ E = 0› and
dom0': ‹0 ∉# dom_m N''› and
Q'Q'': ‹if length M' = length M'' then Q' = Q'' else Q'' = {#}› and
W': ‹W' = {#}› and
W'': ‹W'' = {#}›
using TU unfolding cdcl_twl_restart_l.simps T apply -
apply normalize_goal+
by blast
have U': ‹U = (M'', N'', None, NE + mset `# (NE' + NE''), UE + mset `# (UE' + UE''), W'',
Q'')›
unfolding U by simp
show ?thesis
unfolding S U' W W' W''
apply (rule cdcl_twl_restart_l.restart_trail)
subgoal using valid_trail_reduction_trans[OF tr_red tr_red'] .
subgoal using init init' by auto
subgoal using learned learned' subset_mset.dual_order.trans by fastforce
subgoal using NUE NUE' valid_trail_reduction_level0_iff[OF tr_red] n_d unfolding S by auto
subgoal using ge0 ge0' tr_red' init learned NUE ge0 still0'
apply (auto dest: valid_trail_reduction_Propagated_inD)
apply (blast dest: valid_trail_reduction_Propagated_inD)+
apply (metis neq0_conv still0' valid_trail_reduction_Propagated_inD)+
done
subgoal using new0 new0' tr_red' init learned NUE ge0
apply (auto dest: valid_trail_reduction_Propagated_inD)
by (smt neq0_conv valid_trail_reduction_Propagated_inD)
subgoal using still0 still0' tr_red' by (fastforce dest: valid_trail_reduction_Propagated_inD)
subgoal using dom0' .
subgoal using QQ' Q'Q'' valid_trail_reduction_length_leD[OF tr_red]
valid_trail_reduction_length_leD[OF tr_red']
by (auto split: if_splits)
done
qed
lemma rtranclp_cdcl_twl_restart_l_no_dup:
assumes
ST: ‹cdcl_twl_restart_l⇧*⇧* S T› and
n_d: ‹no_dup (get_trail_l S)›
shows ‹no_dup (get_trail_l T)›
using assms
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal
by (auto simp: cdcl_twl_restart_l.simps valid_trail_reduction_simps
dest: map_lit_of_eq_no_dupD dest!: no_dup_appendD get_all_ann_decomposition_exists_prepend)
done
lemma tranclp_cdcl_twl_restart_l_cdcl_is_cdcl_twl_restart_l:
assumes
ST: ‹cdcl_twl_restart_l⇧+⇧+ S T› and
n_d: ‹no_dup (get_trail_l S)›
shows ‹cdcl_twl_restart_l S T›
using assms
apply (induction rule: tranclp_induct)
subgoal by auto
subgoal
using cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l
rtranclp_cdcl_twl_restart_l_no_dup by blast
done
lemma valid_trail_reduction_refl: ‹valid_trail_reduction a a›
by (auto simp: valid_trail_reduction.simps)
paragraph ‹Auxilary definition›
text ‹
This definition states that the domain of the clauses is reduced, but the remaining clauses
are not changed.
›
definition reduce_dom_clauses where
‹reduce_dom_clauses N N' ⟷
(∀C. C ∈# dom_m N' ⟶ C ∈# dom_m N ∧ fmlookup N C = fmlookup N' C)›
lemma reduce_dom_clauses_fdrop[simp]: ‹reduce_dom_clauses N (fmdrop C N)›
using distinct_mset_dom[of N]
by (auto simp: reduce_dom_clauses_def dest: in_diffD multi_member_split
distinct_mem_diff_mset)
lemma reduce_dom_clauses_refl[simp]: ‹reduce_dom_clauses N N›
by (auto simp: reduce_dom_clauses_def)
lemma reduce_dom_clauses_trans:
‹reduce_dom_clauses N N' ⟹ reduce_dom_clauses N' N'a ⟹ reduce_dom_clauses N N'a›
by (auto simp: reduce_dom_clauses_def)
definition valid_trail_reduction_eq where
‹valid_trail_reduction_eq M M' ⟷ valid_trail_reduction M M' ∧ length M = length M'›
lemma valid_trail_reduction_eq_alt_def:
‹valid_trail_reduction_eq M M' ⟷ map lit_of M = map lit_of M' ∧
map is_decided M = map is_decided M'›
by (auto simp: valid_trail_reduction_eq_def valid_trail_reduction.simps
dest!: get_all_ann_decomposition_exists_prepend
dest: map_eq_imp_length_eq trail_renumber_get_level)
lemma valid_trail_reduction_change_annot:
‹valid_trail_reduction (M @ Propagated L C # M')
(M @ Propagated L 0 # M')›
by (auto simp: valid_trail_reduction_eq_def valid_trail_reduction.simps)
lemma valid_trail_reduction_eq_change_annot:
‹valid_trail_reduction_eq (M @ Propagated L C # M')
(M @ Propagated L 0 # M')›
by (auto simp: valid_trail_reduction_eq_def valid_trail_reduction.simps)
lemma valid_trail_reduction_eq_refl: ‹valid_trail_reduction_eq M M›
by (auto simp: valid_trail_reduction_eq_def valid_trail_reduction_refl)
lemma valid_trail_reduction_eq_get_level:
‹valid_trail_reduction_eq M M' ⟹ get_level M = get_level M'›
by (intro ext)
(auto simp: valid_trail_reduction_eq_def valid_trail_reduction.simps
dest!: get_all_ann_decomposition_exists_prepend
dest: map_eq_imp_length_eq trail_renumber_get_level)
lemma valid_trail_reduction_eq_lits_of_l:
‹valid_trail_reduction_eq M M' ⟹ lits_of_l M = lits_of_l M'›
apply (auto simp: valid_trail_reduction_eq_def valid_trail_reduction.simps
dest!: get_all_ann_decomposition_exists_prepend
dest: map_eq_imp_length_eq trail_renumber_get_level)
apply (metis image_set lits_of_def)+
done
lemma valid_trail_reduction_eq_trans:
‹valid_trail_reduction_eq M M' ⟹ valid_trail_reduction_eq M' M'' ⟹
valid_trail_reduction_eq M M''›
unfolding valid_trail_reduction_eq_alt_def
by auto
definition no_dup_reasons_invs_wl where
‹no_dup_reasons_invs_wl S ⟷
(distinct_mset (mark_of `# filter_mset (λC. is_proped C ∧ mark_of C > 0) (mset (get_trail_l S))))›
inductive different_annot_all_killed where
propa_changed:
‹different_annot_all_killed N NUE (Propagated L C) (Propagated L C')›
if ‹C ≠ C'› and ‹C' = 0› and
‹C ∈# dom_m N ⟹ mset (N∝C) ∈# NUE› |
propa_not_changed:
‹different_annot_all_killed N NUE (Propagated L C) (Propagated L C)› |
decided_not_changed:
‹different_annot_all_killed N NUE (Decided L) (Decided L)›
lemma different_annot_all_killed_refl[iff]:
‹different_annot_all_killed N NUE z z ⟷ is_proped z ∨ is_decided z›
by (cases z) (auto simp: different_annot_all_killed.simps)
abbreviation different_annots_all_killed where
‹different_annots_all_killed N NUE ≡ list_all2 (different_annot_all_killed N NUE)›
lemma different_annots_all_killed_refl:
‹different_annots_all_killed N NUE M M›
by (auto intro!: list.rel_refl_strong simp: count_decided_0_iff is_decided_no_proped_iff)
paragraph ‹Refinement towards code›
text ‹
Once of the first thing we do, is removing clauses we know to be true. We do in two ways:
▪ along the trail (at level 0); this makes sure that annotations are kept;
▪ then along the watch list.
This is (obviously) not complete but is faster by avoiding iterating over all clauses. Here are
the rules we want to apply for our very limited inprocessing:
›
inductive remove_one_annot_true_clause :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
remove_irred_trail:
‹remove_one_annot_true_clause (M @ Propagated L C # M', N, D, NE, UE, W, Q)
(M @ Propagated L 0 # M', fmdrop C N, D, add_mset (mset (N∝C)) NE, UE, W, Q)›
if
‹get_level (M @ Propagated L C # M') L = 0› and
‹C > 0› and
‹C ∈# dom_m N› and
‹irred N C› |
remove_red_trail:
‹remove_one_annot_true_clause (M @ Propagated L C # M', N, D, NE, UE, W, Q)
(M @ Propagated L 0 # M', fmdrop C N, D, NE, add_mset (mset (N∝C)) UE, W, Q)›
if
‹get_level (M @ Propagated L C # M') L = 0› and
‹C > 0› and
‹C ∈# dom_m N› and
‹¬irred N C› |
remove_irred:
‹remove_one_annot_true_clause (M, N, D, NE, UE, W, Q)
(M, fmdrop C N, D, add_mset (mset (N∝C))NE, UE, W, Q)›
if
‹L ∈ lits_of_l M› and
‹get_level M L = 0› and
‹C ∈# dom_m N› and
‹L ∈ set (N∝C)› and
‹irred N C› and
‹∀L. Propagated L C ∉ set M› |
delete:
‹remove_one_annot_true_clause (M, N, D, NE, UE, W, Q)
(M, fmdrop C N, D, NE, UE, W, Q)›
if
‹C ∈# dom_m N› and
‹¬irred N C› and
‹∀L. Propagated L C ∉ set M›
text ‹Remarks:
▸ \<^term>‹∀L. Propagated L C ∉ set M› is overkill. However, I am currently unsure how I want to
handle it (either as \<^term>‹Propagated (N∝C!0) C ∉ set M› or as ``the trail contains only zero
anyway'').›
lemma Ex_ex_eq_Ex: ‹(∃NE'. (∃b. NE' = {#b#} ∧ P b NE') ∧ Q NE') ⟷
(∃b. P b {#b#} ∧ Q {#b#})›
by auto
lemma in_set_definedD:
‹Propagated L' C ∈ set M' ⟹ defined_lit M' L'›
‹Decided L' ∈ set M' ⟹ defined_lit M' L'›
by (auto simp: defined_lit_def)
lemma (in conflict_driven_clause_learning⇩W) trail_no_annotation_reuse:
assumes
struct_invs: ‹cdcl⇩W_all_struct_inv S› and
LC: ‹Propagated L C ∈ set (trail S)› and
LC': ‹Propagated L' C ∈ set (trail S)›
shows "L = L'"
proof -
have
confl: ‹cdcl⇩W_conflicting S› and
n_d: ‹no_dup (trail S)›
using struct_invs unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
by fast+
find_theorems "_ @ _#_ = _ @ _ # _"
have H: ‹L = L'› if ‹trail S = ysa @ Propagated L' C # c21 @ Propagated L C # zs›
for ysa xsa c21 zs L L'
proof -
have 1: ‹c21 @ Propagated L C # zs ⊨as CNot (remove1_mset L' C) ∧ L' ∈# C›
using confl unfolding cdcl⇩W_conflicting_def that
by (auto)
have that': ‹trail S = (ysa @ Propagated L' C # c21) @ Propagated L C # zs›
unfolding that by auto
have 2: ‹zs ⊨as CNot (remove1_mset L C) ∧ L ∈# C›
using confl unfolding cdcl⇩W_conflicting_def that'
by blast
show ‹L = L'›
using 1 2 n_d unfolding that
by (auto dest!: multi_member_split
simp: true_annots_true_cls_def_iff_negation_in_model add_mset_eq_add_mset
Decided_Propagated_in_iff_in_lits_of_l)
qed
show ?thesis
using H[of _ L _ L'] H[of _ L' _ L]
using split_list[OF LC] split_list[OF LC']
by (force elim!: list_match_lel_lel)
qed
lemma remove_one_annot_true_clause_cdcl_twl_restart_l:
assumes
rem: ‹remove_one_annot_true_clause S T› and
lst_invs: ‹twl_list_invs S› and
SS': ‹(S, S') ∈ twl_st_l None› and
struct_invs: ‹twl_struct_invs S'› and
confl: ‹get_conflict_l S = None› and
upd: ‹clauses_to_update_l S = {#}› and
n_d: ‹no_dup (get_trail_l S)›
shows ‹cdcl_twl_restart_l S T›
using assms
proof -
have dist_N: ‹distinct_mset (dom_m (get_clauses_l S))›
by (rule distinct_mset_dom)
then have C_notin_rem: ‹C ∉# remove1_mset C (dom_m (get_clauses_l S))› for C
by (simp add: distinct_mset_remove1_All)
have
‹∀C∈#clauses_to_update_l S. C ∈# dom_m (get_clauses_l S)› and
dom0: ‹0 ∉# dom_m (get_clauses_l S)› and
annot: ‹⋀L C. Propagated L C ∈ set (get_trail_l S) ⟹
0 < C ⟹
(C ∈# dom_m (get_clauses_l S) ∧
L ∈ set (watched_l (get_clauses_l S ∝ C)) ∧
(length (get_clauses_l S ∝ C) > 2 ⟶ L = get_clauses_l S ∝ C ! 0))› and
‹distinct_mset (clauses_to_update_l S)›
using lst_invs unfolding twl_list_invs_def apply -
by fast+
have struct_S': ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of S')›
using struct_invs unfolding twl_struct_invs_def by fast
show ?thesis
using rem
proof (cases rule: remove_one_annot_true_clause.cases)
case (remove_irred_trail M L C M' N D NE UE W Q) note S = this(1) and T = this(2) and
lev_L = this(3) and C0 = this(4) and C_dom = this(5) and irred = this(6)
have D: ‹D = None› and W: ‹W = {#}›
using confl upd unfolding S by auto
have NE: ‹add_mset (mset (N ∝ C)) NE = NE + mset `# {#N∝C#}›
by simp
have UE: ‹UE = UE + mset `# {#}›
by simp
have new_NUE: ‹∀E∈#{#N ∝ C#} + {#}.
∃La∈set E.
La ∈ lits_of_l (M @ Propagated L C # M') ∧
get_level (M @ Propagated L C # M') La = 0›
apply (intro ballI impI)
apply (rule_tac x=L in bexI)
using lev_L annot[of L _] C0 by (auto simp: S dest: in_set_takeD[of _ 2])
have [simp]: ‹Propagated L E' ∉ set M'› ‹Propagated L E' ∉ set M› for E'
using n_d lst_invs
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E'› M]
split_list[of ‹Propagated L E'› M'])
have [simp]: ‹Propagated L' C ∉ set M'› ‹Propagated L' C ∉ set M› for L'
using SS' n_d C0 struct_S'
cdcl⇩W_restart_mset.trail_no_annotation_reuse[of ‹state⇩W_of S'› L ‹(mset (N ∝ C))› L']
apply (auto simp: S twl_st_l_def convert_lits_l_imp_same_length trail.simps
)
apply (auto simp: list_rel_append1 list_rel_split_right_iff convert_lits_l_def
p2rel_def)
apply (case_tac y)
apply (auto simp: list_rel_append1 list_rel_split_right_iff defined_lit_convert_lits_l
simp flip: p2rel_def convert_lits_l_def dest: in_set_definedD(1)[of _ _ M'])
apply (auto simp: list_rel_append1 list_rel_split_right_iff convert_lits_l_def
p2rel_def convert_lit.simps
dest!: split_list[of ‹Propagated L' C› M']
split_list[of ‹Propagated L' C› M])
done
have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M ⟹ E=E'› for L E E'
using n_d
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E› M]
split_list[of ‹Propagated L E'› M]
elim!: list_match_lel_lel)
have propa_M'M': ‹Propagated L E ∈ set M' ⟹ Propagated L E' ∈ set M' ⟹ E=E'› for L E E'
using n_d
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E› M']
split_list[of ‹Propagated L E'› M']
elim!: list_match_lel_lel)
have propa_MM': ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M' ⟹ False› for L E E'
using n_d
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E› M]
split_list[of ‹Propagated L E'› M']
elim!: list_match_lel_lel)
have propa_M'_nC_dom: ‹Propagated La E ∈ set M' ⟹ E ≠ C ∧ (E > 0 ⟶ E ∈# dom_m N)› for La E
using annot[of La E] unfolding S by auto
have propa_M_nC_dom: ‹Propagated La E ∈ set M ⟹ E ≠ C ∧ (E > 0 ⟶ E ∈# dom_m N)› for La E
using annot[of La E] unfolding S by auto
show ?thesis
unfolding S T D W NE
apply (subst (2) UE)
apply (rule cdcl_twl_restart_l.intros)
subgoal by (auto simp: valid_trail_reduction_change_annot)
subgoal using C_dom irred by auto
subgoal using irred by auto
subgoal using new_NUE .
subgoal
apply (intro conjI allI impI)
subgoal for La E E'
using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
propa_M_nC_dom[of La E]
unfolding S by auto
subgoal for La E E'
using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
unfolding S by auto
done
subgoal
apply (intro allI impI)
subgoal for La E E'
using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
by auto
done
subgoal
apply (intro allI impI)
subgoal for La E E'
using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
by auto
done
subgoal using dom0 unfolding S by (auto dest: in_diffD)
subgoal by auto
done
next
case (remove_red_trail M L C M' N D NE UE W Q) note S =this(1) and T = this(2) and
lev_L = this(3) and C0 = this(4) and C_dom = this(5) and irred = this(6)
have D: ‹D = None› and W: ‹W = {#}›
using confl upd unfolding S by auto
have UE: ‹add_mset (mset (N ∝ C)) UE = UE + mset `# {#N∝C#}›
by simp
have NE: ‹NE = NE + mset `# {#}›
by simp
have new_NUE: ‹∀E∈#{#} + {#N ∝ C#}.
∃La∈set E.
La ∈ lits_of_l (M @ Propagated L C # M') ∧
get_level (M @ Propagated L C # M') La = 0›
apply (intro ballI impI)
apply (rule_tac x=L in bexI)
using lev_L annot[of L _] C0 by (auto simp: S dest: in_set_takeD[of _ 2])
have [simp]: ‹Propagated L E' ∉ set M'› ‹Propagated L E' ∉ set M› for E'
using n_d lst_invs
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E'› M]
split_list[of ‹Propagated L E'› M'])
have [simp]: ‹Propagated L' C ∉ set M'› ‹Propagated L' C ∉ set M› for L'
using SS' n_d C0 struct_S'
cdcl⇩W_restart_mset.trail_no_annotation_reuse[of ‹state⇩W_of S'› L ‹(mset (N ∝ C))› L']
apply (auto simp: S twl_st_l_def convert_lits_l_imp_same_length trail.simps
)
apply (auto simp: list_rel_append1 list_rel_split_right_iff convert_lits_l_def
p2rel_def)
apply (case_tac y)
apply (auto simp: list_rel_append1 list_rel_split_right_iff defined_lit_convert_lits_l
simp flip: p2rel_def convert_lits_l_def dest: in_set_definedD(1)[of _ _ M'])
apply (auto simp: list_rel_append1 list_rel_split_right_iff convert_lits_l_def
p2rel_def convert_lit.simps
dest!: split_list[of ‹Propagated L' C› M']
split_list[of ‹Propagated L' C› M])
done
have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M ⟹ E=E'› for L E E'
using n_d
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E› M]
split_list[of ‹Propagated L E'› M]
elim!: list_match_lel_lel)
have propa_M'M': ‹Propagated L E ∈ set M' ⟹ Propagated L E' ∈ set M' ⟹ E=E'› for L E E'
using n_d
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E› M']
split_list[of ‹Propagated L E'› M']
elim!: list_match_lel_lel)
have propa_MM': ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M' ⟹ False› for L E E'
using n_d
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E› M]
split_list[of ‹Propagated L E'› M']
elim!: list_match_lel_lel)
have propa_M'_nC_dom: ‹Propagated La E ∈ set M' ⟹ E ≠ C ∧ (E > 0 ⟶ E ∈# dom_m N)› for La E
using annot[of La E] unfolding S by auto
have propa_M_nC_dom: ‹Propagated La E ∈ set M ⟹ E ≠ C ∧ (E > 0 ⟶ E ∈# dom_m N)› for La E
using annot[of La E] unfolding S by auto
show ?thesis
unfolding S T D W UE
apply (subst (2) NE)
apply (rule cdcl_twl_restart_l.intros)
subgoal by (auto simp: valid_trail_reduction_change_annot)
subgoal using C_dom irred by auto
subgoal using C_dom irred by auto
subgoal using new_NUE .
subgoal
apply (intro conjI allI impI)
subgoal for La E E'
using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
propa_M_nC_dom[of La E]
unfolding S by auto
subgoal for La E E'
using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
unfolding S by auto
done
subgoal
apply (intro allI impI)
subgoal for La E E'
using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
by auto
done
subgoal
apply (intro allI impI)
subgoal for La E E'
using C_notin_rem propa_MM[of La E E'] propa_MM'[of La E E'] propa_M'_nC_dom[of La E]
propa_M_nC_dom[of La E] propa_MM'[of La E' E] propa_M'M'[of La E' E]
by auto
done
subgoal using dom0 unfolding S by (auto dest: in_diffD)
subgoal by auto
done
next
case (remove_irred L M C N D NE UE W Q) note S =this(1) and T = this(2) and
L_M = this(3) and lev_L = this(4) and C_dom = this(5) and watched_L = this(6) and
irred = this(7) and L_notin_M = this(8)
have NE: ‹add_mset (mset (N ∝ C)) NE = NE + mset `# {#N∝C#}›
by simp
have UE: ‹UE = UE + mset `# {#}›
by simp
have D: ‹D = None› and W: ‹W = {#}›
using confl upd unfolding S by auto
have new_NUE: ‹∀E∈#{#N ∝ C#} + {#}.
∃La∈set E.
La ∈ lits_of_l M ∧
get_level M La = 0›
apply (intro ballI impI)
apply (rule_tac x=L in bexI)
using lev_L annot[of L _] L_M watched_L by (auto simp: S dest: in_set_takeD[of _ 2])
have C0: ‹C > 0›
using dom0 C_dom unfolding S by (auto dest!: multi_member_split)
have [simp]: ‹Propagated La C ∉ set M› for La
using annot[of La C] dom0 n_d L_notin_M C0 unfolding S
by auto
have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M ⟹ E=E'› for L E E'
using n_d
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E› M]
split_list[of ‹Propagated L E'› M]
elim!: list_match_lel_lel)
show ?thesis
unfolding S T D W NE
apply (subst (2) UE)
apply (rule cdcl_twl_restart_l.intros)
subgoal by (auto simp: valid_trail_reduction_refl)
subgoal using C_dom irred by auto
subgoal using C_dom irred by auto
subgoal using new_NUE .
subgoal
using n_d L_notin_M C_notin_rem annot propa_MM unfolding S by force
subgoal
using propa_MM by auto
subgoal
using propa_MM by auto
subgoal using dom0 C_dom unfolding S by (auto dest: in_diffD)
subgoal by auto
done
next
case (delete C N M D NE UE W Q) note S = this(1) and T = this(2) and C_dom = this(3) and
irred = this(4) and L_notin_M = this(5)
have D: ‹D = None› and W: ‹W = {#}›
using confl upd unfolding S by auto
have UE: ‹UE = UE + mset `# {#}›
by simp
have NE: ‹NE = NE + mset `# {#}›
by simp
have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M ⟹ E=E'› for L E E'
using n_d
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E› M]
split_list[of ‹Propagated L E'› M]
elim!: list_match_lel_lel)
show ?thesis
unfolding S T D W
apply (subst (2) NE)
apply (subst (2) UE)
apply (rule cdcl_twl_restart_l.intros)
subgoal by (auto simp: valid_trail_reduction_refl)
subgoal using C_dom irred by auto
subgoal using C_dom irred by auto
subgoal by simp
subgoal
apply (intro conjI impI allI)
subgoal for L E E'
using n_d L_notin_M C_notin_rem annot propa_MM[of L E E'] unfolding S
by (metis dom_m_fmdrop get_clauses_l.simps get_trail_l.simps in_remove1_msetI)
subgoal for L E E'
using n_d L_notin_M C_notin_rem annot propa_MM[of L E E'] unfolding S
by auto
done
subgoal
using propa_MM by auto
subgoal
using propa_MM by auto
subgoal using dom0 C_dom unfolding S by (auto dest: in_diffD)
subgoal by auto
done
qed
qed
lemma is_annot_iff_annotates_first:
assumes
ST: ‹(S, T) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S› and
struct_invs: ‹twl_struct_invs T› and
C0: ‹C > 0›
shows
‹(∃L. Propagated L C ∈ set (get_trail_l S)) ⟷
((length (get_clauses_l S ∝ C) > 2 ⟶
Propagated (get_clauses_l S ∝ C ! 0) C ∈ set (get_trail_l S)) ∧
((length (get_clauses_l S ∝ C) ≤ 2 ⟶
Propagated (get_clauses_l S ∝ C ! 0) C ∈ set (get_trail_l S) ∨
Propagated (get_clauses_l S ∝ C ! 1) C ∈ set (get_trail_l S))))›
(is ‹?A ⟷ ?B›)
proof (rule iffI)
assume ?B
then show ?A by auto
next
assume ?A
then obtain L where
LC: ‹Propagated L C ∈ set (get_trail_l S)›
by blast
then have
C: ‹C ∈# dom_m (get_clauses_l S)› and
L_w: ‹L ∈ set (watched_l (get_clauses_l S ∝ C))› and
L: ‹length (get_clauses_l S ∝ C) > 2 ⟹ L = get_clauses_l S ∝ C ! 0›
using list_invs C0 unfolding twl_list_invs_def by blast+
have ‹twl_st_inv T›
using struct_invs unfolding twl_struct_invs_def by fast
then have le2: ‹length (get_clauses_l S ∝ C) ≥ 2›
using C ST multi_member_split[OF C] unfolding twl_struct_invs_def
by (cases S; cases T)
(auto simp: twl_st_inv.simps twl_st_l_def
image_Un[symmetric])
show ?B
proof (cases ‹length (get_clauses_l S ∝ C) > 2›)
case True
show ?thesis
using L True LC by auto
next
case False
then show ?thesis
using LC le2 L_w
by (cases ‹get_clauses_l S ∝ C›;
cases ‹tl (get_clauses_l S ∝ C)›)
auto
qed
qed
lemma trail_length_ge2:
assumes
ST: ‹(S, T) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S› and
struct_invs: ‹twl_struct_invs T› and
LaC: ‹Propagated L C ∈ set (get_trail_l S)› and
C0: ‹C > 0›
shows
‹length (get_clauses_l S ∝ C) ≥ 2›
proof -
have conv:
‹(get_trail_l S, get_trail T) ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)›
using ST unfolding twl_st_l_def by auto
have ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of T)› and
lev_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T)›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have n_d: ‹no_dup (get_trail_l S)›
using ST lev_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: twl_st_l twl_st)
have
C: ‹C ∈# dom_m (get_clauses_l S)›
using list_invs C0 LaC by (auto simp: twl_list_invs_def all_conj_distrib)
have ‹twl_st_inv T›
using struct_invs unfolding twl_struct_invs_def by fast
then show le2: ‹length (get_clauses_l S ∝ C) ≥ 2›
using C ST multi_member_split[OF C] unfolding twl_struct_invs_def
by (cases S; cases T)
(auto simp: twl_st_inv.simps twl_st_l_def
image_Un[symmetric])
qed
lemma is_annot_no_other_true_lit:
assumes
ST: ‹(S, T) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S› and
struct_invs: ‹twl_struct_invs T› and
C0: ‹C > 0› and
LaC: ‹Propagated La C ∈ set (get_trail_l S)› and
LC: ‹L ∈ set (get_clauses_l S ∝ C)› and
L: ‹L ∈ lits_of_l (get_trail_l S)›
shows
‹La = L› and
‹length (get_clauses_l S ∝ C) > 2 ⟹ L = get_clauses_l S ∝ C ! 0›
proof -
have conv:
‹(get_trail_l S, get_trail T) ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)›
using ST unfolding twl_st_l_def by auto
obtain M2 M1 where
tr_S: ‹get_trail_l S = M2 @ Propagated La C # M1›
using split_list[OF LaC] by blast
then obtain M2' M1' where
tr_T: ‹get_trail T = M2' @ Propagated La (mset (get_clauses_l S ∝ C)) # M1'› and
M2: ‹(M2, M2') ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)› and
M1: ‹(M1, M1') ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)›
using conv C0 by (auto simp: list_all2_append1 list_all2_append2 list_all2_Cons1 list_all2_Cons2
convert_lits_l_def list_rel_def convert_lit.simps dest!: p2relD)
have ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of T)› and
lev_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T)›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then have ‹La ∈# mset (get_clauses_l S ∝ C)› and
‹M1' ⊨as CNot (remove1_mset La (mset (get_clauses_l S ∝ C)))›
using tr_T
unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (auto 5 5 simp: twl_st twl_st_l)
then have
‹M1 ⊨as CNot (remove1_mset La (mset (get_clauses_l S ∝ C)))›
using M1 convert_lits_l_true_clss_clss by blast
then have all_false: ‹-K ∈ lits_of_l (get_trail_l S)›
if ‹K ∈# remove1_mset La (mset (get_clauses_l S ∝ C))›
for K
using that tr_S unfolding true_annots_true_cls_def_iff_negation_in_model
by (auto dest!: multi_member_split)
have La0: ‹length (get_clauses_l S ∝ C) > 2 ⟹ La = get_clauses_l S ∝ C ! 0› and
C: ‹C ∈# dom_m (get_clauses_l S)› and
‹La ∈ set (watched_l (get_clauses_l S ∝ C))›
using list_invs tr_S C0 by (auto simp: twl_list_invs_def all_conj_distrib)
have n_d: ‹no_dup (get_trail_l S)›
using ST lev_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: twl_st_l twl_st)
show ‹La = L›
proof (rule ccontr)
assume ‹¬?thesis›
then have ‹L ∈# remove1_mset La (mset (get_clauses_l S ∝ C))›
using LC by auto
from all_false[OF this] show False
using L n_d by (auto dest: no_dup_consistentD)
qed
then show ‹length (get_clauses_l S ∝ C) > 2 ⟹ L = get_clauses_l S ∝ C ! 0›
using La0 by simp
qed
lemma remove_one_annot_true_clause_cdcl_twl_restart_l2:
assumes
rem: ‹remove_one_annot_true_clause S T› and
lst_invs: ‹twl_list_invs S› and
confl: ‹get_conflict_l S = None› and
upd: ‹clauses_to_update_l S = {#}› and
n_d: ‹(S, T') ∈ twl_st_l None› ‹twl_struct_invs T'›
shows ‹cdcl_twl_restart_l S T›
proof -
have n_d: ‹no_dup (get_trail_l S)›
using n_d 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
by (auto simp: twl_st twl_st_l)
show ?thesis
apply (rule remove_one_annot_true_clause_cdcl_twl_restart_l[OF _ _ ‹(S, T') ∈ twl_st_l None›])
subgoal using rem .
subgoal using lst_invs .
subgoal using ‹twl_struct_invs T'› .
subgoal using confl .
subgoal using upd .
subgoal using n_d .
done
qed
lemma remove_one_annot_true_clause_get_conflict_l:
‹remove_one_annot_true_clause S T ⟹ get_conflict_l T = get_conflict_l S›
by (auto simp: remove_one_annot_true_clause.simps)
lemma rtranclp_remove_one_annot_true_clause_get_conflict_l:
‹remove_one_annot_true_clause⇧*⇧* S T ⟹ get_conflict_l T = get_conflict_l S›
by (induction rule: rtranclp_induct) (auto simp: remove_one_annot_true_clause_get_conflict_l)
lemma remove_one_annot_true_clause_clauses_to_update_l:
‹remove_one_annot_true_clause S T ⟹ clauses_to_update_l T = clauses_to_update_l S›
by (auto simp: remove_one_annot_true_clause.simps)
lemma rtranclp_remove_one_annot_true_clause_clauses_to_update_l:
‹remove_one_annot_true_clause⇧*⇧* S T ⟹ clauses_to_update_l T = clauses_to_update_l S›
by (induction rule: rtranclp_induct) (auto simp: remove_one_annot_true_clause_clauses_to_update_l)
lemma cdcl_twl_restart_l_invs:
assumes ST: ‹(S, T) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S› and
struct_invs: ‹twl_struct_invs T› and ‹cdcl_twl_restart_l S S'›
shows ‹∃T'. (S', T') ∈ twl_st_l None ∧ twl_list_invs S' ∧
clauses_to_update_l S' = {#} ∧ cdcl_twl_restart T T' ∧ twl_struct_invs T'›
using cdcl_twl_restart_l_cdcl_twl_restart[OF ST list_invs struct_invs]
cdcl_twl_restart_twl_struct_invs[OF _ struct_invs]
by (smt RETURN_ref_SPECD RETURN_rule assms(4) in_pair_collect_simp order_trans)
lemma rtranclp_cdcl_twl_restart_l_invs:
assumes
‹cdcl_twl_restart_l⇧*⇧* S S'› and
ST: ‹(S, T) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S› and
struct_invs: ‹twl_struct_invs T› and
‹clauses_to_update_l S = {#}›
shows ‹∃T'. (S', T') ∈ twl_st_l None ∧ twl_list_invs S' ∧
clauses_to_update_l S' = {#} ∧ cdcl_twl_restart⇧*⇧* T T' ∧ twl_struct_invs T'›
using assms(1)
apply (induction rule: rtranclp_induct)
subgoal
using assms(2-) apply - by (rule exI[of _ T]) auto
subgoal for T U
using cdcl_twl_restart_l_invs[of T _ U] assms
by (meson rtranclp.rtrancl_into_rtrancl)
done
lemma rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2:
assumes
rem: ‹remove_one_annot_true_clause⇧*⇧* S T› and
lst_invs: ‹twl_list_invs S› and
confl: ‹get_conflict_l S = None› and
upd: ‹clauses_to_update_l S = {#}› and
n_d: ‹(S, S') ∈ twl_st_l None› ‹twl_struct_invs S'›
shows ‹∃T'. cdcl_twl_restart_l⇧*⇧* S T ∧ (T, T') ∈ twl_st_l None ∧ cdcl_twl_restart⇧*⇧* S' T' ∧
twl_struct_invs T'›
using rem
proof (induction)
case base
then show ?case
using assms apply - by (rule_tac x=S' in exI) auto
next
case (step U V) note st = this(1) and step = this(2) and IH = this(3)
obtain U' where
IH: ‹cdcl_twl_restart_l⇧*⇧* S U› and
UT': ‹(U, U') ∈ twl_st_l None› and
S'U': ‹cdcl_twl_restart⇧*⇧* S' U'›
using IH by blast
have ‹twl_list_invs U›
using rtranclp_cdcl_twl_restart_l_list_invs[OF IH lst_invs] .
have ‹get_conflict_l U = None›
using rtranclp_remove_one_annot_true_clause_get_conflict_l[OF st] confl
by auto
have ‹clauses_to_update_l U = {#}›
using rtranclp_remove_one_annot_true_clause_clauses_to_update_l[OF st] upd
by auto
have ‹twl_struct_invs U'›
by (metis (no_types, hide_lams) ‹cdcl_twl_restart⇧*⇧* S' U'›
cdcl_twl_restart_twl_struct_invs n_d(2) rtranclp_induct)
have ‹cdcl_twl_restart_l U V›
apply (rule remove_one_annot_true_clause_cdcl_twl_restart_l2[of _ _ U'])
subgoal using step .
subgoal using ‹twl_list_invs U› .
subgoal using ‹get_conflict_l U = None› .
subgoal using ‹clauses_to_update_l U = {#}› .
subgoal using UT' .
subgoal using ‹twl_struct_invs U'› .
done
moreover obtain V' where
UT': ‹(V, V') ∈ twl_st_l None› and
‹cdcl_twl_restart U' V'› and
‹twl_struct_invs V'›
using cdcl_twl_restart_l_invs[OF UT' _ _ ‹cdcl_twl_restart_l U V›] ‹twl_list_invs U›
‹twl_struct_invs U'›
by blast
ultimately show ?case
using S'U' IH by fastforce
qed
definition drop_clause_add_move_init where
‹drop_clause_add_move_init = (λ(M, N0, D, NE0, UE, Q, W) C.
(M, fmdrop C N0, D, add_mset (mset (N0 ∝ C)) NE0, UE, Q, W))›
lemma [simp]:
‹get_trail_l (drop_clause_add_move_init V C) = get_trail_l V›
by (cases V) (auto simp: drop_clause_add_move_init_def)
definition drop_clause where
‹drop_clause = (λ(M, N0, D, NE0, UE, Q, W) C.
(M, fmdrop C N0, D, NE0, UE, Q, W))›
lemma [simp]:
‹get_trail_l (drop_clause V C) = get_trail_l V›
by (cases V) (auto simp: drop_clause_def)
definition remove_all_annot_true_clause_one_imp
where
‹remove_all_annot_true_clause_one_imp = (λ(C, S). do {
if C ∈# dom_m (get_clauses_l S) then
if irred (get_clauses_l S) C
then RETURN (drop_clause_add_move_init S C)
else RETURN (drop_clause S C)
else do {
RETURN S
}
})›
definition remove_one_annot_true_clause_imp_inv where
‹remove_one_annot_true_clause_imp_inv S =
(λ(i, T). remove_one_annot_true_clause⇧*⇧* S T ∧ twl_list_invs S ∧ i ≤ length (get_trail_l S) ∧
twl_list_invs S ∧
clauses_to_update_l S = clauses_to_update_l T ∧
literals_to_update_l S = literals_to_update_l T ∧
get_conflict_l T = None ∧
(∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S') ∧
get_conflict_l S = None ∧ clauses_to_update_l S = {#} ∧
length (get_trail_l S) = length (get_trail_l T) ∧
(∀j<i. is_proped (rev (get_trail_l T) ! j) ∧ mark_of (rev (get_trail_l T) ! j) = 0))›
definition remove_all_annot_true_clause_imp_inv where
‹remove_all_annot_true_clause_imp_inv S xs =
(λ(i, T). remove_one_annot_true_clause⇧*⇧* S T ∧ twl_list_invs S ∧ i ≤ length xs ∧
twl_list_invs S ∧ get_trail_l S = get_trail_l T ∧
(∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S') ∧
get_conflict_l S = None ∧ clauses_to_update_l S = {#})›
definition remove_all_annot_true_clause_imp_pre where
‹remove_all_annot_true_clause_imp_pre L S ⟷
(twl_list_invs S ∧ twl_list_invs S ∧
(∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S') ∧
get_conflict_l S = None ∧ clauses_to_update_l S = {#} ∧ L ∈ lits_of_l (get_trail_l S))›
definition remove_all_annot_true_clause_imp
:: ‹'v literal ⇒ 'v twl_st_l ⇒ ('v twl_st_l) nres›
where
‹remove_all_annot_true_clause_imp = (λL S. do {
ASSERT(remove_all_annot_true_clause_imp_pre L S);
xs ← SPEC(λxs.
(∀x∈set xs. x ∈# dom_m (get_clauses_l S) ⟶ L ∈ set ((get_clauses_l S)∝x)));
(_, T) ← WHILE⇩T⇗λ(i, T). remove_all_annot_true_clause_imp_inv S xs (i, T)⇖
(λ(i, T). i < length xs)
(λ(i, T). do {
ASSERT(i < length xs);
if xs!i ∈# dom_m (get_clauses_l T) ∧ length ((get_clauses_l T) ∝ (xs!i)) ≠ 2
then do {
T ← remove_all_annot_true_clause_one_imp (xs!i, T);
ASSERT(remove_all_annot_true_clause_imp_inv S xs (i, T));
RETURN (i+1, T)
}
else
RETURN (i+1, T)
})
(0, S);
RETURN T
})›
definition remove_one_annot_true_clause_one_imp_pre where
‹remove_one_annot_true_clause_one_imp_pre i T ⟷
(twl_list_invs T ∧ i < length (get_trail_l T) ∧
twl_list_invs T ∧
(∃S'. (T, S') ∈ twl_st_l None ∧ twl_struct_invs S') ∧
get_conflict_l T = None ∧ clauses_to_update_l T = {#})›
definition replace_annot_l where
‹replace_annot_l L C =
(λ(M, N, D, NE, UE, Q, W).
RES {(M', N, D, NE, UE, Q, W)| M'.
(∃M2 M1 C. M = M2 @ Propagated L C # M1 ∧ M' = M2 @ Propagated L 0 # M1)})›
definition remove_and_add_cls_l where
‹remove_and_add_cls_l C =
(λ(M, N, D, NE, UE, Q, W).
RETURN (M, fmdrop C N, D,
(if irred N C then add_mset (mset (N∝C)) else id) NE,
(if ¬irred N C then add_mset (mset (N∝C)) else id) UE, Q, W))›
text ‹The following progrom removes all clauses that are annotations. However, this is not compatible
with binary clauses, since we want to make sure that they should not been deleted.
›
term remove_all_annot_true_clause_imp
definition remove_one_annot_true_clause_one_imp
where
‹remove_one_annot_true_clause_one_imp = (λi S. do {
ASSERT(remove_one_annot_true_clause_one_imp_pre i S);
ASSERT(is_proped ((rev (get_trail_l S))!i));
(L, C) ← SPEC(λ(L, C). (rev (get_trail_l S))!i = Propagated L C);
ASSERT(Propagated L C ∈ set (get_trail_l S));
if C = 0 then RETURN (i+1, S)
else do {
ASSERT(C ∈# dom_m (get_clauses_l S));
S ← replace_annot_l L C S;
S ← remove_and_add_cls_l C S;
⌦‹S ← remove_all_annot_true_clause_imp L S;›
RETURN (i+1, S)
}
})›
definition remove_one_annot_true_clause_imp :: ‹'v twl_st_l ⇒ ('v twl_st_l) nres›
where
‹remove_one_annot_true_clause_imp = (λS. do {
k ← SPEC(λk. (∃M1 M2 K. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S)) ∧
count_decided M1 = 0 ∧ k = length M1)
∨ (count_decided (get_trail_l S) = 0 ∧ k = length (get_trail_l S)));
(_, S) ← WHILE⇩T⇗remove_one_annot_true_clause_imp_inv S⇖
(λ(i, S). i < k)
(λ(i, S). remove_one_annot_true_clause_one_imp i S)
(0, S);
RETURN S
})›
lemma remove_one_annot_true_clause_imp_same_length:
‹remove_one_annot_true_clause S T ⟹ length (get_trail_l S) = length (get_trail_l T)›
by (induction rule: remove_one_annot_true_clause.induct) (auto simp: )
lemma rtranclp_remove_one_annot_true_clause_imp_same_length:
‹remove_one_annot_true_clause⇧*⇧* S T ⟹ length (get_trail_l S) = length (get_trail_l T)›
by (induction rule: rtranclp_induct) (auto simp: remove_one_annot_true_clause_imp_same_length)
lemma remove_one_annot_true_clause_map_is_decided_trail:
‹remove_one_annot_true_clause S U ⟹
map is_decided (get_trail_l S) = map is_decided (get_trail_l U)›
by (induction rule: remove_one_annot_true_clause.induct)
auto
lemma remove_one_annot_true_clause_map_mark_of_same_or_0:
‹remove_one_annot_true_clause S U ⟹
mark_of (get_trail_l S ! i) = mark_of (get_trail_l U ! i) ∨ mark_of (get_trail_l U ! i) = 0›
by (induction rule: remove_one_annot_true_clause.induct)
(auto simp: nth_append nth_Cons split: nat.split)
lemma remove_one_annot_true_clause_imp_inv_trans:
‹remove_one_annot_true_clause_imp_inv S (i, T) ⟹ remove_one_annot_true_clause_imp_inv T U ⟹
remove_one_annot_true_clause_imp_inv S U›
using rtranclp_remove_one_annot_true_clause_imp_same_length[of S T]
by (auto simp: remove_one_annot_true_clause_imp_inv_def)
lemma rtranclp_remove_one_annot_true_clause_map_is_decided_trail:
‹remove_one_annot_true_clause⇧*⇧* S U ⟹
map is_decided (get_trail_l S) = map is_decided (get_trail_l U)›
by (induction rule: rtranclp_induct)
(auto simp: remove_one_annot_true_clause_map_is_decided_trail)
lemma rtranclp_remove_one_annot_true_clause_map_mark_of_same_or_0:
‹remove_one_annot_true_clause⇧*⇧* S U ⟹
mark_of (get_trail_l S ! i) = mark_of (get_trail_l U ! i) ∨ mark_of (get_trail_l U ! i) = 0›
by (induction rule: rtranclp_induct)
(auto dest!: remove_one_annot_true_clause_map_mark_of_same_or_0)
lemma remove_one_annot_true_clause_map_lit_of_trail:
‹remove_one_annot_true_clause S U ⟹
map lit_of (get_trail_l S) = map lit_of (get_trail_l U)›
by (induction rule: remove_one_annot_true_clause.induct)
auto
lemma rtranclp_remove_one_annot_true_clause_map_lit_of_trail:
‹remove_one_annot_true_clause⇧*⇧* S U ⟹
map lit_of (get_trail_l S) = map lit_of (get_trail_l U)›
by (induction rule: rtranclp_induct)
(auto simp: remove_one_annot_true_clause_map_lit_of_trail)
lemma remove_one_annot_true_clause_reduce_dom_clauses:
‹remove_one_annot_true_clause S U ⟹
reduce_dom_clauses (get_clauses_l S) (get_clauses_l U)›
by (induction rule: remove_one_annot_true_clause.induct)
auto
lemma rtranclp_remove_one_annot_true_clause_reduce_dom_clauses:
‹remove_one_annot_true_clause⇧*⇧* S U ⟹
reduce_dom_clauses (get_clauses_l S) (get_clauses_l U)›
by (induction rule: rtranclp_induct)
(auto dest!: remove_one_annot_true_clause_reduce_dom_clauses intro: reduce_dom_clauses_trans)
lemma decomp_nth_eq_lit_eq:
assumes
‹M = M2 @ Propagated L C' # M1› and
‹rev M ! i = Propagated L C› and
‹no_dup M› and
‹i < length M›
shows ‹length M1 = i› and ‹C = C'›
proof -
have [simp]: ‹defined_lit M1 (lit_of (M1 ! i))› if ‹i < length M1› for i
using that by (simp add: in_lits_of_l_defined_litD lits_of_def)
have[simp]: ‹undefined_lit M2 L ⟹
k < length M2 ⟹
M2 ! k ≠ Propagated L C› for k
using defined_lit_def nth_mem by fastforce
have[simp]: ‹undefined_lit M1 L ⟹
k < length M1 ⟹
M1 ! k ≠ Propagated L C› for k
using defined_lit_def nth_mem by fastforce
have ‹M ! (length M - Suc i) ∈ set M›
apply (rule nth_mem)
using assms by auto
from split_list[OF this] show ‹length M1 = i› and ‹C = C'›
using assms
by (auto simp: nth_append nth_Cons nth_rev split: if_splits nat.splits
elim!: list_match_lel_lel)
qed
lemma
assumes ‹no_dup M›
shows
no_dup_same_annotD:
‹Propagated L C ∈ set M ⟹ Propagated L C' ∈ set M ⟹ C = C'› and
no_dup_no_propa_and_dec:
‹Propagated L C ∈ set M ⟹ Decided L ∈ set M ⟹ False›
using assms
by (auto dest!: split_list elim: list_match_lel_lel)
lemma remove_one_annot_true_clause_imp_inv_spec:
assumes
annot: ‹remove_one_annot_true_clause_imp_inv S (i+1, U)› and
i_le: ‹i < length (get_trail_l S)› and
L: ‹L ∈ lits_of_l (get_trail_l S)› and
lev0: ‹get_level (get_trail_l S) L = 0› and
LC: ‹Propagated L 0 ∈ set (get_trail_l U)›
shows ‹remove_all_annot_true_clause_imp L U
≤ SPEC (λSa. RETURN (i + 1, Sa)
≤ SPEC (λs'. remove_one_annot_true_clause_imp_inv S s' ∧
(s', (i, T))
∈ measure
(λ(i, _). length (get_trail_l S) - i)))›
proof -
obtain M N D NE UE WS Q where
U: ‹U = (M, N, D, NE, UE, WS, Q)›
by (cases U)
obtain x where
SU: ‹remove_one_annot_true_clause⇧*⇧* S (M, N, D, NE, UE, WS, Q)› and
‹twl_list_invs S› and
‹i + 1 ≤ length (get_trail_l S)› and
‹twl_list_invs S› and
‹get_conflict_l S = None› and
‹(S, x) ∈ twl_st_l None› and
‹twl_struct_invs x› and
‹clauses_to_update_l S = {#}› and
level0: ‹∀j<i + 1. is_proped (rev (get_trail_l (M, N, D, NE, UE, WS, Q)) ! j)›and
mark0: ‹∀j<i + 1. mark_of (rev (get_trail_l (M, N, D, NE, UE, WS, Q)) ! j) = 0›
using annot unfolding U prod.case remove_one_annot_true_clause_imp_inv_def
by blast
obtain U' where
‹cdcl_twl_restart_l⇧*⇧* S U› and
U'V': ‹(U, U') ∈ twl_st_l None› and
‹cdcl_twl_restart⇧*⇧* x U'› and
struvt_invs_V': ‹twl_struct_invs U'›
using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF SU ‹twl_list_invs S›
‹get_conflict_l S = None› ‹clauses_to_update_l S = {#}› ‹(S, x) ∈ twl_st_l None›
‹twl_struct_invs x›] unfolding U
by auto
moreover have ‹twl_list_invs U›
using ‹twl_list_invs S› calculation(1) rtranclp_cdcl_twl_restart_l_list_invs by blast
ultimately have rem_U_U: ‹remove_one_annot_true_clause_imp_inv U (i + 1, U)›
using level0 rtranclp_remove_one_annot_true_clause_clauses_to_update_l[OF SU]
rtranclp_remove_one_annot_true_clause_get_conflict_l[OF SU] mark0
‹clauses_to_update_l S = {#}› ‹get_conflict_l S = None› i_le
arg_cong[OF rtranclp_remove_one_annot_true_clause_map_lit_of_trail[OF SU], of length]
unfolding remove_one_annot_true_clause_imp_inv_def unfolding U
by (cases U') fastforce
then have rem_true_U_U: ‹remove_all_annot_true_clause_imp_inv U xs (0, U)› for xs
using level0 rtranclp_remove_one_annot_true_clause_clauses_to_update_l[OF SU]
rtranclp_remove_one_annot_true_clause_get_conflict_l[OF SU] ‹twl_list_invs U›
‹clauses_to_update_l S = {#}› ‹get_conflict_l S = None› i_le
arg_cong[OF rtranclp_remove_one_annot_true_clause_map_lit_of_trail[OF SU], of length]
unfolding U remove_all_annot_true_clause_imp_inv_def remove_one_annot_true_clause_imp_inv_def
by (cases U') blast
moreover have L_M: ‹L ∈ lits_of_l M›
using L arg_cong[OF rtranclp_remove_one_annot_true_clause_map_lit_of_trail[OF SU], of set]
by (simp add: lits_of_def)
ultimately have pre: ‹remove_all_annot_true_clause_imp_pre L U›
unfolding remove_all_annot_true_clause_imp_pre_def remove_all_annot_true_clause_imp_inv_def
prod.case U by force
have remove_all_annot_true_clause_one_imp:
‹remove_all_annot_true_clause_one_imp (xs ! k, V)
≤ SPEC
(λT. do {
_ ← ASSERT (remove_all_annot_true_clause_imp_inv U xs (k, T));
RETURN (k + 1, T)
} ≤ SPEC
(λs'. (case s' of
(i, T) ⇒
remove_all_annot_true_clause_imp_inv U xs (i, T)) ∧
(case s' of
(uu_, W) ⇒
remove_one_annot_true_clause_imp_inv U (i + 1, W)) ∧
(s', s) ∈ measure (λ(i, _). length xs - i)))›
if
xs: ‹xs ∈ {xs.
∀x∈set xs.
x ∈# dom_m (get_clauses_l U) ⟶ L ∈ set (get_clauses_l U ∝ x)}› and
I': ‹case s of (i, T) ⇒ remove_all_annot_true_clause_imp_inv U xs (i, T)› and
I: ‹case s of (uu_, W) ⇒ remove_one_annot_true_clause_imp_inv U (i + 1, W)› and
cond: ‹case s of (i, T) ⇒ i < length xs› and
s: ‹s = (k, V)› and
k_le: ‹k < length xs› and
dom: ‹xs ! k ∈# dom_m (get_clauses_l V) ∧
length (get_clauses_l V ∝ (xs ! k)) ≠ 2›
for s k V xs
proof -
obtain x where
UU': ‹remove_one_annot_true_clause⇧*⇧* U V› and
i_le: ‹i + 1 ≤ length (get_trail_l U)› and
list_invs: ‹twl_list_invs U› and
confl: ‹get_conflict_l U = None› and
Ux: ‹(U, x) ∈ twl_st_l None› and
struct_x: ‹twl_struct_invs x› and
upd: ‹clauses_to_update_l U = {#}› and
all_level0: ‹∀j<i + 1. is_proped (rev (get_trail_l V) ! j)› and
all_mark0: ‹∀j<i + 1. mark_of (rev (get_trail_l V) ! j) = 0› and
lits_upd: ‹literals_to_update_l U = literals_to_update_l V› and
clss_upd: ‹clauses_to_update_l U = clauses_to_update_l V› and
confl_V: ‹get_conflict_l V = None› and
tr: ‹get_trail_l U = get_trail_l V›
using I' I unfolding s prod.case remove_one_annot_true_clause_imp_inv_def
remove_all_annot_true_clause_imp_inv_def
by blast
have n_d: ‹no_dup (get_trail_l U)›
using Ux struct_x 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
by (auto simp: twl_st twl_st_l)
have SU': ‹remove_one_annot_true_clause⇧*⇧* S V›
using SU UU' unfolding U by simp
have ‹get_level M L = 0›
using lev0 rtranclp_remove_one_annot_true_clause_map_is_decided_trail[OF SU]
rtranclp_remove_one_annot_true_clause_map_lit_of_trail[OF SU]
U trail_renumber_get_level[of ‹get_trail_l S› ‹get_trail_l U› L]
by force
have red: ‹reduce_dom_clauses (get_clauses_l U)
(get_clauses_l V)›
using rtranclp_remove_one_annot_true_clause_reduce_dom_clauses[OF UU'] unfolding U
by simp
then have [simp]: ‹N ∝ (xs ! k) = get_clauses_l V ∝ (xs ! k)› and
dom_VU: ‹⋀C. C ∈# dom_m (get_clauses_l V) ⟶ C ∈# dom_m (get_clauses_l U)›
using dom unfolding reduce_dom_clauses_def U by simp_all
obtain V' where
‹cdcl_twl_restart_l⇧*⇧* U V› and
U'V': ‹(V, V') ∈ twl_st_l None› and
‹cdcl_twl_restart⇧*⇧* x V'› and
struvt_invs_V': ‹twl_struct_invs V'›
using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF UU' ‹twl_list_invs U›
‹get_conflict_l U = None› ‹clauses_to_update_l U = {#}› ‹(U, x) ∈ twl_st_l None›
‹twl_struct_invs x›]
by auto
have list_invs_U': ‹twl_list_invs V›
using ‹cdcl_twl_restart_l⇧*⇧* U V› ‹twl_list_invs U›
rtranclp_cdcl_twl_restart_l_list_invs by blast
have dom_N: ‹xs ! k ∈# dom_m (get_clauses_l V)›
using dom red unfolding s
by (auto simp del: nth_mem simp: reduce_dom_clauses_def)
have xs_k_0: ‹0 < xs ! k›
apply (rule ccontr)
using dom list_invs_U' by (auto simp: twl_list_invs_def)
have L_set: ‹L ∈ set (get_clauses_l V ∝ (xs!k))›
using xs cond nth_mem[of k xs] dom_N dom_VU[of ‹xs!k›] unfolding s U
by (auto simp del: nth_mem)
have ‹no_dup M›
using n_d unfolding U by simp
then have no_already_annot: ‹Propagated Laa (xs ! k) ∈ set (get_trail_l V) ⟹ False› for Laa
using is_annot_iff_annotates_first[OF U'V' list_invs_U' struvt_invs_V' xs_k_0] LC
is_annot_no_other_true_lit[OF U'V' list_invs_U' struvt_invs_V' xs_k_0, of Laa L]
L_set L_M xs_k_0 tr unfolding U
by (auto dest: no_dup_same_annotD)
let ?U' = ‹(M, N, D, NE, UE, WS, Q)›
have V: ‹V = (M, get_clauses_l V, D, get_unit_init_clauses_l V,
get_unit_learned_clauses_l V, WS, Q)›
using confl upd lits_upd tr clss_upd confl_V unfolding U
by (cases V) auto
let ?V = ‹(M, N, D, NE, UE, WS, Q)›
let ?Vt = ‹drop_clause_add_move_init V (xs!k)›
let ?Vf = ‹drop_clause V (xs!k)›
have ‹remove_one_annot_true_clause V ?Vt›
if ‹irred (get_clauses_l V) (xs ! k)›
apply (subst (2) V)
apply (subst V)
unfolding drop_clause_add_move_init_def prod.case
apply (rule remove_one_annot_true_clause.remove_irred[of L])
subgoal using ‹L ∈ lits_of_l M› .
subgoal using ‹get_level M L = 0› .
subgoal using dom by simp
subgoal using L_set by auto
subgoal using that .
subgoal using no_already_annot tr unfolding U by auto
done
then have UV_irred: ‹remove_one_annot_true_clause⇧*⇧* U ?Vt›
if ‹irred (get_clauses_l V) (xs ! k)›
using UU' that by simp
have ‹remove_one_annot_true_clause V ?Vf›
if ‹¬irred (get_clauses_l V) (xs ! k)›
apply (subst (2) V)
apply (subst V)
unfolding drop_clause_def prod.case
apply (rule remove_one_annot_true_clause.delete)
subgoal using dom by simp
subgoal using that .
subgoal using no_already_annot tr unfolding U by auto
done
then have UV_red: ‹remove_one_annot_true_clause⇧*⇧* U ?Vf›
if ‹¬irred (get_clauses_l V) (xs ! k)›
using UU' that by simp
have i_le: ‹Suc i ≤ length M›
using annot assms(2) unfolding U remove_one_annot_true_clause_imp_inv_def
by auto
have 1: ‹remove_one_annot_true_clause_imp_inv U (Suc i, ?Vt)›
if ‹irred (get_clauses_l V) (xs ! k)›
using UV_irred that ‹twl_list_invs U› i_le all_level0 all_mark0
‹get_conflict_l U = None› ‹clauses_to_update_l U = {#}› ‹(U, x) ∈ twl_st_l None›
‹twl_struct_invs x› unfolding U
unfolding remove_one_annot_true_clause_imp_inv_def prod.case
apply (intro conjI)
subgoal by auto
subgoal by auto
subgoal using i_le by auto
subgoal using tr by (cases V) (auto simp: drop_clause_add_move_init_def U)
subgoal using clss_upd by (cases V) (auto simp: drop_clause_add_move_init_def U)
subgoal using lits_upd by (cases V) (auto simp: drop_clause_add_move_init_def U)
subgoal using confl_V by (cases V) (auto simp: drop_clause_add_move_init_def U)
subgoal by blast
subgoal by auto
subgoal by auto
subgoal using tr by (cases V) (auto simp: drop_clause_add_move_init_def U)
subgoal using tr by (cases V) (auto simp: drop_clause_add_move_init_def U)
done
have 2: ‹remove_one_annot_true_clause_imp_inv U (Suc i, ?Vf)›
if ‹¬irred (get_clauses_l V) (xs ! k)›
using UV_red that ‹twl_list_invs U› i_le all_level0 all_mark0
‹get_conflict_l U = None› ‹clauses_to_update_l U = {#}› ‹(U, x) ∈ twl_st_l None›
‹twl_struct_invs x› unfolding U
unfolding remove_one_annot_true_clause_imp_inv_def prod.case
apply (intro conjI)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using tr by (cases V) (auto simp: drop_clause_def U)
subgoal using clss_upd by (cases V) (auto simp: drop_clause_def U)
subgoal using lits_upd by (cases V) (auto simp: drop_clause_def U)
subgoal using confl_V by (cases V) (auto simp: drop_clause_def U)
subgoal by blast
subgoal by auto
subgoal by auto
subgoal using tr by (cases V) (auto simp: drop_clause_def U)
subgoal using tr by (cases V) (auto simp: drop_clause_def U)
done
have ‹remove_all_annot_true_clause_imp_inv U xs
(k, ?Vt)›
if ‹irred (get_clauses_l V) (xs ! k)›
proof -
have "∃p. (U, p) ∈ twl_st_l None ∧ twl_struct_invs p"
using Ux struct_x
by meson
then show ?thesis
using that Ux struct_x list_invs i_le confl upd UV_irred cond tr
unfolding remove_all_annot_true_clause_imp_inv_def prod.case s
by (simp add: less_imp_le_nat)
qed
moreover have ‹remove_all_annot_true_clause_imp_inv U xs
(k, ?Vf)›
if ‹¬irred (get_clauses_l V) (xs ! k)›
proof -
have "∃p. (U, p) ∈ twl_st_l None ∧ twl_struct_invs p"
using Ux struct_x
by meson
then show ?thesis
using that Ux struct_x list_invs i_le confl upd UV_red cond tr
unfolding remove_all_annot_true_clause_imp_inv_def prod.case
by (simp add: less_imp_le_nat s)
qed
ultimately show ?thesis
using dom 1 2 cond
unfolding remove_all_annot_true_clause_one_imp_def s
by (auto simp:
Suc_le_eq remove_all_annot_true_clause_imp_inv_def)
qed
have remove_all_annot_true_clause_imp_inv_Suc:
‹remove_all_annot_true_clause_imp_inv S xs (Suc i, T)›
if ‹remove_all_annot_true_clause_imp_inv S xs (i, T)› and
‹i < length xs›
for xs
using that
by (auto simp: remove_all_annot_true_clause_imp_inv_def)
have one_all: ‹remove_one_annot_true_clause_imp_inv S (Suc i, T) ⟹
remove_all_annot_true_clause_imp_inv S xs (a, T) ⟹
Suc a ≤ length xs ⟹
remove_all_annot_true_clause_imp_inv S xs (Suc a, T)› for S T a xs
unfolding remove_one_annot_true_clause_imp_inv_def remove_all_annot_true_clause_imp_inv_def
by auto
show ?thesis
unfolding remove_all_annot_true_clause_imp_def prod.case assert_bind_spec_conv
apply (subst intro_spec_refine_iff[of _ _ Id, simplified])
apply (intro ballI conjI)
subgoal using pre unfolding U .
subgoal for xs
apply (refine_vcg
WHILEIT_rule_stronger_inv[where
R = ‹measure (λ(i, _). length xs - i)› and
I' = ‹λ(_, W). remove_one_annot_true_clause_imp_inv U (i+1, W)›])
subgoal by auto
subgoal using rem_true_U_U unfolding U by auto
subgoal using rem_U_U unfolding U by auto
subgoal by simp
apply (rule remove_all_annot_true_clause_one_imp; assumption)
subgoal by (auto simp: remove_all_annot_true_clause_imp_inv_Suc U one_all)
subgoal by (auto simp: remove_all_annot_true_clause_imp_inv_Suc U one_all)
subgoal by (auto simp: remove_all_annot_true_clause_imp_inv_Suc U one_all)
subgoal
apply (rule remove_one_annot_true_clause_imp_inv_trans[OF annot])
apply auto
done
subgoal using i_le by auto
done
done
qed
lemma RETURN_le_RES_no_return:
‹f ≤ SPEC (λS. g S ∈ Φ) ⟹ do {S ← f; RETURN (g S)} ≤ RES Φ›
by (cases f) (auto simp: RES_RETURN_RES)
lemma remove_one_annot_true_clause_one_imp_spec:
assumes
I: ‹remove_one_annot_true_clause_imp_inv S iT› and
cond: ‹case iT of (i, S) ⇒ i < length (get_trail_l S)› and
iT: ‹iT = (i, T)› and
proped: ‹is_proped (rev (get_trail_l S) ! i)›
shows ‹remove_one_annot_true_clause_one_imp i T
≤ SPEC (λs'. remove_one_annot_true_clause_imp_inv S s' ∧
(s', iT) ∈ measure (λ(i, _). length (get_trail_l S) - i))›
proof -
obtain M N D NE UE WS Q where T: ‹T = (M, N, D, NE, UE, WS, Q)›
by (cases T)
obtain x where
ST: ‹remove_one_annot_true_clause⇧*⇧* S T› and
‹twl_list_invs S› and
‹i ≤ length (get_trail_l S)› and
‹twl_list_invs S› and
‹(S, x) ∈ twl_st_l None› and
‹twl_struct_invs x› and
confl: ‹get_conflict_l S = None› and
upd: ‹clauses_to_update_l S = {#}› and
level0: ‹∀j<i. is_proped (rev (get_trail_l T) ! j)› and
mark0: ‹∀j<i. mark_of (rev (get_trail_l T) ! j) = 0› and
le: ‹length (get_trail_l S) = length (get_trail_l T)› and
clss_upd: ‹clauses_to_update_l S = clauses_to_update_l T› and
lits_upd: ‹literals_to_update_l S = literals_to_update_l T›
using I unfolding remove_one_annot_true_clause_imp_inv_def iT prod.case by blast
then have list_invs_T: ‹twl_list_invs T›
by (meson rtranclp_cdcl_twl_restart_l_list_invs
rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2)
obtain x' where
Tx': ‹(T, x') ∈ twl_st_l None› and
struct_invs_T: ‹twl_struct_invs x'›
using ‹(S, x) ∈ twl_st_l None› ‹twl_list_invs S› ‹twl_struct_invs x› confl
rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2 ST upd by blast
then have n_d: ‹no_dup (get_trail_l T)›
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
by (auto simp: twl_st twl_st_l)
have D: ‹D = None› and WS: ‹WS = {#}›
using confl upd rtranclp_remove_one_annot_true_clause_clauses_to_update_l[OF ST]
using rtranclp_remove_one_annot_true_clause_get_conflict_l[OF ST] unfolding T by auto
have lits_of_ST: ‹lits_of_l (get_trail_l S) = lits_of_l (get_trail_l T)›
using arg_cong[OF rtranclp_remove_one_annot_true_clause_map_lit_of_trail[OF ST], of set]
by (simp add: lits_of_def)
have rem_one_annot_i_T: ‹remove_one_annot_true_clause_one_imp_pre i T›
using Tx' struct_invs_T level0 cond list_invs_T D WS
unfolding remove_one_annot_true_clause_one_imp_pre_def iT T prod.case
by fastforce
have
annot_in_dom: ‹C ∈# dom_m (get_clauses_l T)› (is ?annot)
if
‹case LC of (L, C) ⇒ rev (get_trail_l T) ! i = Propagated L C› and
‹LC = (L, C)› and
‹¬(C = 0)›
for LC L C
proof -
have ‹rev (get_trail_l T)!i ∈ set (get_trail_l T)›
using list_invs_T assms le unfolding T
by (auto simp: twl_list_invs_def rev_nth)
then show ?annot
using list_invs_T that le unfolding T
by (auto simp: twl_list_invs_def simp del: nth_mem)
qed
have replace_annot_l:
‹replace_annot_l L C T
≤ SPEC
(λSa. do {
S ← remove_and_add_cls_l C Sa;
RETURN (i + 1, S)
} ≤ SPEC
(λs'. remove_one_annot_true_clause_imp_inv S s' ∧
(s', iT)
∈ measure (λ(i, _). length (get_trail_l S) - i)))›
if
rem_one: ‹remove_one_annot_true_clause_one_imp_pre i T› and
‹is_proped (rev (get_trail_l T) ! i)› and
LC_d: ‹case LC of (L, C) ⇒ rev (get_trail_l T) ! i = Propagated L C› and
LC: ‹LC = (L, C)› and
LC_T: ‹Propagated L C ∈ set (get_trail_l T)› and
‹C ≠ 0› and
dom: ‹C ∈# dom_m (get_clauses_l T)›
for LC C L
proof -
have ‹i < length M›
using rem_one unfolding remove_one_annot_true_clause_one_imp_pre_def T by auto
{
fix M2 Ca M1
assume M: ‹M = M2 @ Propagated L Ca # M1› and ‹irred N Ca›
have n_d: ‹no_dup M›
using n_d unfolding T by auto
then have [simp]: ‹Ca = C›
using LC_T
by (auto simp: T M dest!: in_set_definedD)
have ‹Ca > 0›
using that(6) by auto
let ?U = ‹(M2 @ Propagated L 0 # M1, fmdrop Ca N, D, add_mset (mset (N ∝ Ca)) NE, UE, WS, Q)›
have lev: ‹get_level (M2 @ Propagated L C # M1) L = 0› and
M1: ‹length M1 = i›
using n_d level0 LC_d decomp_nth_eq_lit_eq(1)[OF M
LC_d[unfolded T get_trail_l.simps LC prod.case]
n_d ‹i < length M›]
unfolding M T
apply (auto simp: count_decided_0_iff nth_append nth_Cons is_decided_no_proped_iff
in_set_conv_nth rev_nth
split: if_splits)
by (metis diff_less gr_implies_not0 linorder_neqE_nat nth_rev_alt rev_nth zero_less_Suc)
have TU: ‹remove_one_annot_true_clause T ?U›
unfolding T M
apply (rule remove_one_annot_true_clause.remove_irred_trail)
using ‹irred N Ca› ‹Ca > 0› dom lev
by (auto simp: T M)
moreover {
have ‹length (get_trail_l ?U) = length (get_trail_l T)›
using TU by (auto simp: remove_one_annot_true_clause.simps T M)
then have ‹j<i ⟹ is_proped (rev (get_trail_l ?U) ! j)› for j
using arg_cong[OF remove_one_annot_true_clause_map_is_decided_trail[OF TU],
of ‹λxs. xs ! (length (get_trail_l ?U) - Suc j)›] level0 ‹i < length M›
by (auto simp: rev_nth T is_decided_no_proped_iff M
nth_append nth_Cons split: nat.splits)
}
moreover {
have ‹length (get_trail_l ?U) = length (get_trail_l T)›
using TU by (auto simp: remove_one_annot_true_clause.simps T M)
then have ‹j<i ⟹ mark_of (rev (get_trail_l ?U) ! j) = 0› for j
using remove_one_annot_true_clause_map_mark_of_same_or_0[OF TU,
of ‹(length (get_trail_l ?U) - Suc j)›] mark0 ‹i < length M›
by (auto simp: rev_nth T is_decided_no_proped_iff M
nth_append nth_Cons split: nat.splits)
}
moreover have ‹length (get_trail_l S) = length (get_trail_l ?U)›
using le TU by (auto simp: T M split: if_splits)
moreover have ‹∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S'›
by (rule exI[of _ x])
(use ‹(S, x) ∈ twl_st_l None› ‹twl_struct_invs x› in blast)
ultimately have 1: ‹remove_one_annot_true_clause_imp_inv S (Suc i, ?U)›
using ‹twl_list_invs S› ‹i ≤ length (get_trail_l S)›
‹(S, x) ∈ twl_st_l None› and
‹twl_struct_invs x› and
‹get_conflict_l S = None› and
‹clauses_to_update_l S = {#}› and
‹∀j<i. is_proped (rev (get_trail_l T) ! j)› and
‹∀j<i. mark_of (rev (get_trail_l T) ! j) = 0› and
le T clss_upd lits_upd ST TU D M1 ‹i < length M›
unfolding remove_one_annot_true_clause_imp_inv_def prod.case
by (auto simp: less_Suc_eq nth_append)
have 2: ‹length (get_trail_l S) - Suc i < length (get_trail_l S) - i›
by (simp add: T ‹i < length M› diff_less_mono2 le)
note 1 2
}
moreover {
fix M2 Ca M1
assume M: ‹M = M2 @ Propagated L Ca # M1› and ‹¬irred N Ca›
have n_d: ‹no_dup M›
using n_d unfolding T by auto
then have [simp]: ‹Ca = C›
using LC_T
by (auto simp: T M dest!: in_set_definedD)
have ‹Ca > 0›
using that(6) by auto
let ?U = ‹(M2 @ Propagated L 0 # M1, fmdrop Ca N, D, NE,
add_mset (mset (N ∝ Ca)) UE, WS, Q)›
have lev: ‹get_level (M2 @ Propagated L C # M1) L = 0› and
M1: ‹length M1 = i›
using n_d level0 LC_d decomp_nth_eq_lit_eq(1)[OF M
LC_d[unfolded T get_trail_l.simps LC prod.case]
n_d ‹i < length M›]
unfolding M T
apply (auto simp: count_decided_0_iff nth_append nth_Cons is_decided_no_proped_iff
in_set_conv_nth rev_nth
split: if_splits)
by (metis diff_less gr_implies_not0 linorder_neqE_nat nth_rev_alt rev_nth zero_less_Suc)
have TU: ‹remove_one_annot_true_clause T ?U›
unfolding T M
apply (rule remove_one_annot_true_clause.remove_red_trail)
using ‹¬irred N Ca› ‹Ca > 0› dom lev
by (auto simp: T M)
moreover {
have ‹length (get_trail_l ?U) = length (get_trail_l T)›
using TU by (auto simp: remove_one_annot_true_clause.simps T M)
then have ‹j<i ⟹ is_proped (rev (get_trail_l ?U) ! j)› for j
using arg_cong[OF remove_one_annot_true_clause_map_is_decided_trail[OF TU],
of ‹λxs. xs ! (length (get_trail_l ?U) - Suc j)›] level0 ‹i < length M›
by (auto simp: rev_nth T is_decided_no_proped_iff M
nth_append nth_Cons split: nat.splits)
}
moreover {
have ‹length (get_trail_l ?U) = length (get_trail_l T)›
using TU by (auto simp: remove_one_annot_true_clause.simps T M)
then have ‹j<i ⟹ mark_of (rev (get_trail_l ?U) ! j) = 0› for j
using remove_one_annot_true_clause_map_mark_of_same_or_0[OF TU,
of ‹(length (get_trail_l ?U) - Suc j)›] mark0 ‹i < length M›
by (auto simp: rev_nth T is_decided_no_proped_iff M
nth_append nth_Cons split: nat.splits)
}
moreover have ‹length (get_trail_l S) = length (get_trail_l ?U)›
using le TU by (auto simp: T M split: if_splits)
moreover have ‹∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S'›
by (rule exI[of _ x])
(use ‹(S, x) ∈ twl_st_l None› ‹twl_struct_invs x› in blast)
ultimately have 1: ‹remove_one_annot_true_clause_imp_inv S (Suc i, ?U)›
using ‹twl_list_invs S› ‹i ≤ length (get_trail_l S)›
‹(S, x) ∈ twl_st_l None› and
‹twl_struct_invs x› and
‹get_conflict_l S = None› and
‹clauses_to_update_l S = {#}› and
‹∀j<i. is_proped (rev (get_trail_l T) ! j)› and
‹∀j<i. mark_of (rev (get_trail_l T) ! j) = 0› and
le T clss_upd lits_upd ST TU D cond ‹i < length M› M1
unfolding remove_one_annot_true_clause_imp_inv_def prod.case
by (auto simp: less_Suc_eq nth_append)
have 2: ‹length (get_trail_l S) - Suc i < length (get_trail_l S) - i›
by (simp add: T ‹i < length M› diff_less_mono2 le)
note 1 2
}
moreover have ‹C = Ca› if ‹M = M2 @ Propagated L Ca # M1› for M1 M2 Ca
using LC_T n_d
by (auto simp: T that dest!: in_set_definedD)
ultimately show ?thesis
using dom cond
by (auto simp: remove_and_add_cls_l_def
replace_annot_l_def T iT
intro!: RETURN_le_RES_no_return)
qed
have rev_set: ‹rev (get_trail_l T) ! i ∈ set (get_trail_l T)›
using assms
by (metis length_rev nth_mem rem_one_annot_i_T
remove_one_annot_true_clause_one_imp_pre_def set_rev)
show ?thesis
unfolding remove_one_annot_true_clause_one_imp_def
apply refine_vcg
subgoal using rem_one_annot_i_T unfolding iT T by simp
subgoal using proped I le
rtranclp_remove_one_annot_true_clause_map_is_decided_trail[of S T,
THEN arg_cong, of ‹λxs. (rev xs) ! i›]
unfolding iT T remove_one_annot_true_clause_imp_inv_def
remove_one_annot_true_clause_one_imp_pre_def
by (auto simp add: All_less_Suc rev_map is_decided_no_proped_iff)
subgoal
using rev_set unfolding T
by auto
subgoal using I le unfolding iT T remove_one_annot_true_clause_imp_inv_def
remove_one_annot_true_clause_one_imp_pre_def
by (auto simp add: All_less_Suc)
subgoal using cond le unfolding iT T remove_one_annot_true_clause_one_imp_pre_def by auto
subgoal by (rule annot_in_dom)
subgoal for LC L C
by (rule replace_annot_l)
done
qed
lemma remove_one_annot_true_clause_count_dec: ‹remove_one_annot_true_clause S b ⟹
count_decided (get_trail_l S) = count_decided (get_trail_l b)›
by (auto simp: remove_one_annot_true_clause.simps)
lemma rtranclp_remove_one_annot_true_clause_count_dec:
‹remove_one_annot_true_clause⇧*⇧* S b ⟹
count_decided (get_trail_l S) = count_decided (get_trail_l b)›
by (induction rule: rtranclp_induct)
(auto simp: remove_one_annot_true_clause_count_dec)
lemma remove_one_annot_true_clause_imp_spec:
assumes
ST: ‹(S, T) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S› and
struct_invs: ‹twl_struct_invs T› and
‹get_conflict_l S = None› and
‹clauses_to_update_l S = {#}›
shows ‹remove_one_annot_true_clause_imp S ≤ SPEC(λT. remove_one_annot_true_clause⇧*⇧* S T)›
unfolding remove_one_annot_true_clause_imp_def
apply (refine_vcg WHILEIT_rule[where R=‹measure (λ(i, _). length (get_trail_l S) - i)› and
I=‹remove_one_annot_true_clause_imp_inv S›]
remove_one_annot_true_clause_imp_inv_spec)
subgoal by auto
subgoal using assms unfolding remove_one_annot_true_clause_imp_inv_def by blast
apply (rule remove_one_annot_true_clause_one_imp_spec[of _ _ ])
subgoal unfolding remove_one_annot_true_clause_imp_inv_def by auto
subgoal unfolding remove_one_annot_true_clause_imp_inv_def by auto
subgoal
by (auto dest!: get_all_ann_decomposition_exists_prepend
simp: count_decided_0_iff rev_nth is_decided_no_proped_iff)
subgoal
by (auto dest!: get_all_ann_decomposition_exists_prepend
simp: count_decided_0_iff rev_nth is_decided_no_proped_iff)
subgoal unfolding remove_one_annot_true_clause_imp_inv_def by auto
done
lemma remove_one_annot_true_clause_imp_spec_lev0:
assumes
ST: ‹(S, T) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S› and
struct_invs: ‹twl_struct_invs T› and
‹get_conflict_l S = None› and
‹clauses_to_update_l S = {#}› and
‹count_decided (get_trail_l S) = 0›
shows ‹remove_one_annot_true_clause_imp S ≤ SPEC(λT. remove_one_annot_true_clause⇧*⇧* S T ∧
count_decided (get_trail_l T) = 0 ∧ (∀L ∈ set (get_trail_l T). mark_of L = 0) ∧
length (get_trail_l S) = length (get_trail_l T)) ›
proof -
have H: ‹∀j<a. is_proped (rev (get_trail_l b) ! j) ∧
mark_of (rev (get_trail_l b) ! j) = 0 ⟹ ¬ a < length (get_trail_l b) ⟹
∀x ∈ set (get_trail_l b). is_proped x ∧ mark_of x = 0› for a b
apply (rule ballI)
apply (subst (asm) set_rev[symmetric])
apply (subst (asm) in_set_conv_nth)
apply auto
done
have K: ‹a < length (get_trail_l b) ⟹ is_decided (get_trail_l b ! a) ⟹
count_decided (get_trail_l b) ≠ 0› for a b
using count_decided_0_iff nth_mem by blast
show ?thesis
unfolding remove_one_annot_true_clause_imp_def
apply (refine_vcg WHILEIT_rule[where
R=‹measure (λ(i, _::'a twl_st_l). length (get_trail_l S) - i)› and
I=‹remove_one_annot_true_clause_imp_inv S›]
remove_one_annot_true_clause_one_imp_spec)
subgoal by auto
subgoal using assms unfolding remove_one_annot_true_clause_imp_inv_def by blast
subgoal using assms unfolding remove_one_annot_true_clause_imp_inv_def by auto
subgoal using assms by (auto simp: count_decided_0_iff is_decided_no_proped_iff
rev_nth)
subgoal
using assms(6) unfolding remove_one_annot_true_clause_imp_inv_def
by (auto dest: H K)
subgoal using assms unfolding remove_one_annot_true_clause_imp_inv_def
by (auto simp: rtranclp_remove_one_annot_true_clause_count_dec)
subgoal
using assms(6) unfolding remove_one_annot_true_clause_imp_inv_def
by (auto dest: H K)
subgoal
using assms(6) unfolding remove_one_annot_true_clause_imp_inv_def
by (auto dest: H K)
done
qed
definition collect_valid_indices :: ‹_ ⇒ nat list nres› where
‹collect_valid_indices S = SPEC (λN. True)›
definition mark_to_delete_clauses_l_inv
:: ‹'v twl_st_l ⇒ nat list ⇒ nat × 'v twl_st_l × nat list ⇒ bool›
where
‹mark_to_delete_clauses_l_inv = (λS xs0 (i, T, xs).
remove_one_annot_true_clause⇧*⇧* S T ∧
get_trail_l S = get_trail_l T ∧
(∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S') ∧
twl_list_invs S ∧
get_conflict_l S = None ∧
clauses_to_update_l S = {#})›
definition mark_to_delete_clauses_l_pre
:: ‹'v twl_st_l ⇒ bool›
where
‹mark_to_delete_clauses_l_pre S ⟷
(∃T. (S, T) ∈ twl_st_l None ∧ twl_struct_invs T ∧ twl_list_invs S)›
definition mark_garbage_l:: ‹nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹mark_garbage_l = (λC (M, N0, D, NE, UE, WS, Q). (M, fmdrop C N0, D, NE, UE, WS, Q))›
definition can_delete where
‹can_delete S C b = (b ⟶
(length (get_clauses_l S ∝ C) = 2 ⟶
(Propagated (get_clauses_l S ∝ C ! 0) C ∉ set (get_trail_l S)) ∧
(Propagated (get_clauses_l S ∝ C ! 1) C ∉ set (get_trail_l S))) ∧
(length (get_clauses_l S ∝ C) > 2 ⟶
(Propagated (get_clauses_l S ∝ C ! 0) C ∉ set (get_trail_l S))) ∧
¬irred (get_clauses_l S) C)›
definition mark_to_delete_clauses_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹mark_to_delete_clauses_l = (λS. do {
ASSERT(mark_to_delete_clauses_l_pre S);
xs ← collect_valid_indices S;
to_keep ← SPEC(λ_::nat. True); ― ‹the minimum number of clauses that should be kept.›
(_, S, _) ← WHILE⇩T⇗mark_to_delete_clauses_l_inv S xs⇖
(λ(i, S, xs). i < length xs)
(λ(i, S, xs). do {
if(xs!i ∉# dom_m (get_clauses_l S)) then RETURN (i, S, delete_index_and_swap xs i)
else do {
ASSERT(0 < length (get_clauses_l S∝(xs!i)));
can_del ← SPEC (can_delete S (xs!i));
ASSERT(i < length xs);
if can_del
then
RETURN (i, mark_garbage_l (xs!i) S, delete_index_and_swap xs i)
else
RETURN (i+1, S, xs)
}
})
(to_keep, S, xs);
RETURN S
})›
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 = {#})›
lemma mark_to_delete_clauses_l_spec:
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 = {#}›
shows ‹mark_to_delete_clauses_l S ≤ ⇓ Id (SPEC(λT. remove_one_annot_true_clause⇧*⇧* S T ∧
get_trail_l S = get_trail_l T))›
proof -
define I where
‹I (xs :: nat list) ≡ (λ(i :: nat, T, xs :: nat list). remove_one_annot_true_clause⇧*⇧* S T)› for xs
have mark0: ‹mark_to_delete_clauses_l_pre S›
using ST list_invs struct_invs unfolding mark_to_delete_clauses_l_pre_def
by blast
have I0: ‹I xs (l, S, xs')›
for xs xs' :: ‹nat list› and l :: nat
proof -
show ?thesis
unfolding I_def
by auto
qed
have mark_to_delete_clauses_l_inv_notin:
‹mark_to_delete_clauses_l_inv S xs0 (a, aa, delete_index_and_swap xs' a)›
if
‹mark_to_delete_clauses_l_pre S› and
‹xs0 ∈ {N. True}› and
‹mark_to_delete_clauses_l_inv S xs0 s› and
‹I xs0 s› and
‹case s of (i, S, xs) ⇒ i < length xs› and
‹aa' = (aa, xs')› and
‹s = (a, aa')› and
‹ba ! a ∉# dom_m (get_clauses_l aa)›
for s a aa ba xs0 aa' xs'
proof -
show ?thesis
using that
unfolding mark_to_delete_clauses_l_inv_def
by auto
qed
have I_notin: ‹I xs0 (a, aa, delete_index_and_swap xs' a)›
if
‹mark_to_delete_clauses_l_pre S› and
‹xs0 ∈ {N. True}› and
‹mark_to_delete_clauses_l_inv S xs0 s› and
‹I xs0 s› and
‹case s of (i, S, xs) ⇒ i < length xs› and
‹aa' = (aa, xs')› and
‹s = (a, aa')› and
‹ba ! a ∉# dom_m (get_clauses_l aa)›
for s a aa ba xs0 aa' xs'
proof -
show ?thesis
using that
unfolding I_def
by auto
qed
have length_ge0: ‹0 < length (get_clauses_l aa ∝ (xs ! a))›
if
inv: ‹mark_to_delete_clauses_l_inv S xs0 s› and
I: ‹I xs0 s› and
cond: ‹case s of (i, S, xs0) ⇒ i < length xs0› and
st:
‹aa' = (aa, xs)›
‹s = (a, aa')› and
xs: ‹¬ xs ! a ∉# dom_m (get_clauses_l aa)›
for s a b aa xs0 aa' xs
proof -
have
rem: ‹remove_one_annot_true_clause⇧*⇧* S aa›
using I unfolding I_def st prod.case by blast+
then obtain T' where
T': ‹(aa, T') ∈ twl_st_l None› and
‹twl_struct_invs T'›
using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF rem list_invs confl upd
ST struct_invs] by blast
then have ‹Multiset.Ball (get_clauses T') struct_wf_twl_cls›
unfolding twl_struct_invs_def twl_st_inv_alt_def
by fast
then have ‹∀x∈#ran_m (get_clauses_l aa). 2 ≤ length (fst x)›
using xs T' by (auto simp: twl_st_l)
then show ?thesis
using xs by (auto simp: ran_m_def)
qed
have mark_to_delete_clauses_l_inv_del:
‹mark_to_delete_clauses_l_inv S xs0 (i, mark_garbage_l (xs ! i) T, delete_index_and_swap xs i)› and
I_del: ‹I xs0 (i, mark_garbage_l (xs ! i) T, delete_index_and_swap xs i)›
if
‹mark_to_delete_clauses_l_pre S› and
‹xs0 ∈ {N. True}› and
inv: ‹mark_to_delete_clauses_l_inv S xs0 s› and
I: ‹I xs0 s› and
i_le: ‹case s of (i, S, xs) ⇒ i < length xs› and
st: ‹sT = (T, xs)›
‹s = (i, sT)› and
in_dom: ‹¬ xs ! i ∉# dom_m (get_clauses_l T)› and
‹0 < length (get_clauses_l T ∝ (xs ! i))› and
can_del: ‹can_delete T (xs ! i) b› and
‹i < length xs› and
[simp]: ‹b›
for x s i T b xs0 sT xs
proof -
obtain M N D NE UE WS Q where S: ‹S = (M, N, D, NE, UE, WS, Q)›
by (cases S)
obtain M' N' D' NE' UE' WS' Q' where T: ‹T = (M', N', D', NE', UE', WS', Q')›
by (cases T)
have
rem: ‹remove_one_annot_true_clause⇧*⇧* S T›
using I unfolding I_def st prod.case by blast+
obtain V where
SU: ‹cdcl_twl_restart_l⇧*⇧* S T› and
UV: ‹(T, V) ∈ twl_st_l None› and
TV: ‹cdcl_twl_restart⇧*⇧* S' V› and
struct_invs_V: ‹twl_struct_invs V›
using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF rem list_invs confl upd
ST struct_invs]
by auto
have list_invs_U': ‹twl_list_invs T›
using SU list_invs rtranclp_cdcl_twl_restart_l_list_invs by blast
have ‹xs ! i > 0›
apply (rule ccontr)
using in_dom list_invs_U' unfolding twl_list_invs_def by (auto dest: multi_member_split)
have ‹N' ∝ (xs ! i) ! 0 ∈ lits_of_l M'›
if ‹Propagated (N' ∝ (xs ! i) ! 0) (xs0 ! i) ∈ set M'›
using that by (auto dest!: split_list)
then have not_annot: ‹Propagated Laa (xs ! i) ∈ set M' ⟹ False› for Laa
using is_annot_iff_annotates_first[OF UV list_invs_U' struct_invs_V ‹xs ! i > 0›]
is_annot_no_other_true_lit[OF UV list_invs_U' struct_invs_V ‹xs ! i > 0›, of Laa ‹
N' ∝ (xs !i) ! 0›] can_del
trail_length_ge2[OF UV list_invs_U' struct_invs_V _ ‹xs ! i > 0›, of Laa]
unfolding S T can_delete_def
by (auto dest: no_dup_same_annotD)
have star: ‹remove_one_annot_true_clause T (mark_garbage_l (xs ! i) T)›
unfolding st T mark_garbage_l_def prod.simps
apply (rule remove_one_annot_true_clause.delete)
subgoal using in_dom i_le unfolding st prod.case T by auto
subgoal using can_del unfolding T can_delete_def by auto
subgoal using not_annot unfolding T by auto
done
moreover have ‹get_trail_l (mark_garbage_l (xs ! i) T) = get_trail_l T›
by (cases T) (auto simp: mark_garbage_l_def)
ultimately show ‹mark_to_delete_clauses_l_inv S xs0
(i, mark_garbage_l (xs ! i) T, delete_index_and_swap xs i)›
using inv
unfolding mark_to_delete_clauses_l_inv_def prod.simps st
by force
show ‹I xs0 (i, mark_garbage_l (xs ! i) T, delete_index_and_swap xs i)›
using rem star unfolding st I_def by simp
qed
have
mark_to_delete_clauses_l_inv_keep:
‹mark_to_delete_clauses_l_inv S xs0 (i + 1, T, xs)› and
I_keep: ‹I xs0 (i + 1, T, xs)›
if
‹mark_to_delete_clauses_l_pre S› and
inv: ‹mark_to_delete_clauses_l_inv S xs0 s› and
I: ‹I xs0 s› and
cond: ‹case s of (i, S, xs) ⇒ i < length xs› and
st: ‹sT = (T, xs)›
‹s = (i, sT)› and
dom: ‹¬ xs ! i ∉# dom_m (get_clauses_l T)› and
‹0 < length (get_clauses_l T ∝ (xs ! i))› and
‹can_delete T (xs ! i) b› and
‹i < length xs› and
‹¬ b›
for x s i T b xs0 sT xs
proof -
show ‹mark_to_delete_clauses_l_inv S xs0 (i + 1, T, xs)›
using inv
unfolding mark_to_delete_clauses_l_inv_def prod.simps st
by fast
show ‹I xs0 (i + 1, T, xs)›
using I unfolding I_def st prod.simps .
qed
show ?thesis
unfolding mark_to_delete_clauses_l_def collect_valid_indices_def
apply (rule ASSERT_refine_left)
apply (rule mark0)
apply (subst intro_spec_iff)
apply (intro ballI)
subgoal for xs0
apply (refine_vcg
WHILEIT_rule_stronger_inv[where I'=‹I xs0› and
R= ‹measure (λ(i :: nat, N, xs0). Suc (length xs0) - i)›])
subgoal by auto
subgoal using list_invs confl upd ST struct_invs unfolding mark_to_delete_clauses_l_inv_def
by (cases S') force
subgoal by (rule I0)
subgoal
by (rule mark_to_delete_clauses_l_inv_notin)
subgoal
by (rule I_notin)
subgoal
by auto
subgoal
by (rule length_ge0)
subgoal
by auto
subgoal
by (rule mark_to_delete_clauses_l_inv_del)
subgoal
by (rule I_del)
subgoal
by auto
subgoal
by (rule mark_to_delete_clauses_l_inv_keep)
subgoal
by (rule I_keep)
subgoal
by auto
subgoal
unfolding I_def by blast
subgoal
unfolding mark_to_delete_clauses_l_inv_def by auto
done
done
qed
definition GC_clauses :: ‹nat clauses_l ⇒ nat clauses_l ⇒ (nat clauses_l × (nat ⇒ nat option)) nres› where
‹GC_clauses N N' = do {
xs ← SPEC(λxs. set_mset (dom_m N) ⊆ set xs);
(N, N', m) ← nfoldli
xs
(λ(N, N', m). True)
(λC (N, N', m).
if C ∈# dom_m N
then do {
C' ← SPEC(λi. i ∉# dom_m N' ∧ i ≠ 0);
RETURN (fmdrop C N, fmupd C' (N ∝ C, irred N C) N', m(C ↦ C'))
}
else
RETURN (N, N', m))
(N, N', (λ_. None));
RETURN (N', m)
}›
inductive GC_remap
:: ‹('a, 'b) fmap × ('a ⇒ 'c option) × ('c, 'b) fmap ⇒ ('a, 'b) fmap × ('a ⇒ 'c option) × ('c, 'b) fmap ⇒ bool›
where
remap_cons:
‹GC_remap (N, m, new) (fmdrop C N, m(C ↦ C'), fmupd C' (the (fmlookup N C)) new)›
if ‹C' ∉# dom_m new› and
‹C ∈# dom_m N› and
‹C ∉ dom m› and
‹C' ∉ ran m›
lemma GC_remap_ran_m_old_new:
‹GC_remap (old, m, new) (old', m', new') ⟹ ran_m old + ran_m new = ran_m old' + ran_m new'›
by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin)
lemma GC_remap_init_clss_l_old_new:
‹GC_remap (old, m, new) (old', m', new') ⟹
init_clss_l old + init_clss_l new = init_clss_l old' + init_clss_l new'›
by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin split: if_splits)
lemma GC_remap_learned_clss_l_old_new:
‹GC_remap (old, m, new) (old', m', new') ⟹
learned_clss_l old + learned_clss_l new = learned_clss_l old' + learned_clss_l new'›
by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin split: if_splits)
lemma GC_remap_ran_m_remap:
‹GC_remap (old, m, new) (old', m', new') ⟹ C ∈# dom_m old ⟹ C ∉# dom_m old' ⟹
m' C ≠ None ∧
fmlookup new' (the (m' C)) = fmlookup old C›
by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin)
lemma GC_remap_ran_m_no_rewrite_map:
‹GC_remap (old, m, new) (old', m', new') ⟹ C ∉# dom_m old ⟹ m' C = m C›
by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin split: if_splits)
lemma GC_remap_ran_m_no_rewrite_fmap:
‹GC_remap (old, m, new) (old', m', new') ⟹ C ∈# dom_m new ⟹
C ∈# dom_m new' ∧ fmlookup new C = fmlookup new' C›
by (induction "(old, m, new)" "(old', m', new')" rule: GC_remap.induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin)
lemma rtranclp_GC_remap_init_clss_l_old_new:
‹GC_remap⇧*⇧* S S' ⟹
init_clss_l (fst S) + init_clss_l (snd (snd S)) = init_clss_l (fst S') + init_clss_l (snd (snd S'))›
by (induction rule: rtranclp_induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin split: if_splits
dest: GC_remap_init_clss_l_old_new)
lemma rtranclp_GC_remap_learned_clss_l_old_new:
‹GC_remap⇧*⇧* S S' ⟹
learned_clss_l (fst S) + learned_clss_l (snd (snd S)) =
learned_clss_l (fst S') + learned_clss_l (snd (snd S'))›
by (induction rule: rtranclp_induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin split: if_splits
dest: GC_remap_learned_clss_l_old_new)
lemma rtranclp_GC_remap_ran_m_no_rewrite_fmap:
‹GC_remap⇧*⇧* S S' ⟹ C ∈# dom_m (snd (snd S)) ⟹
C ∈# dom_m (snd (snd S')) ∧ fmlookup (snd (snd S)) C = fmlookup (snd (snd S')) C›
by (induction rule: rtranclp_induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin dest: GC_remap_ran_m_no_rewrite_fmap)
lemma GC_remap_ran_m_no_rewrite:
‹GC_remap S S' ⟹ C ∈# dom_m (fst S) ⟹ C ∈# dom_m (fst S') ⟹
fmlookup (fst S) C = fmlookup (fst S') C›
by (induction rule: GC_remap.induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin distinct_mset_dom
distinct_mset_set_mset_remove1_mset
dest: GC_remap_ran_m_remap)
lemma GC_remap_ran_m_lookup_kept:
assumes
‹GC_remap⇧*⇧* S y› and
‹GC_remap y z› and
‹C ∈# dom_m (fst S)› and
‹C ∈# dom_m (fst z)› and
‹C ∉# dom_m (fst y)›
shows ‹fmlookup (fst S) C = fmlookup (fst z) C›
using assms by (smt GC_remap.cases fmlookup_drop fst_conv in_dom_m_lookup_iff)
lemma rtranclp_GC_remap_ran_m_no_rewrite:
‹GC_remap⇧*⇧* S S' ⟹ C ∈# dom_m (fst S) ⟹ C ∈# dom_m (fst S') ⟹
fmlookup (fst S) C = fmlookup (fst S') C›
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for y z
by (cases ‹C ∈# dom_m (fst y)›)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin dest: GC_remap_ran_m_remap GC_remap_ran_m_no_rewrite
intro: GC_remap_ran_m_lookup_kept)
done
lemma GC_remap_ran_m_no_lost:
‹GC_remap S S' ⟹ C ∈# dom_m (fst S') ⟹ C ∈# dom_m (fst S)›
by (induction rule: GC_remap.induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin distinct_mset_dom distinct_mset_set_mset_remove1_mset
dest: GC_remap_ran_m_remap)
lemma rtranclp_GC_remap_ran_m_no_lost:
‹GC_remap⇧*⇧* S S' ⟹ C ∈# dom_m (fst S') ⟹ C ∈# dom_m (fst S)›
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for y z
by (cases ‹C ∈# dom_m (fst y)›)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin
dest: GC_remap_ran_m_remap GC_remap_ran_m_no_rewrite
intro: GC_remap_ran_m_lookup_kept GC_remap_ran_m_no_lost)
done
lemma GC_remap_ran_m_no_new_lost:
‹GC_remap S S' ⟹ dom (fst (snd S)) ⊆ set_mset (dom_m (fst S)) ⟹
dom (fst (snd S')) ⊆ set_mset (dom_m (fst S))›
by (induction rule: GC_remap.induct)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin distinct_mset_dom
distinct_mset_set_mset_remove1_mset
dest: GC_remap_ran_m_remap)
lemma rtranclp_GC_remap_ran_m_no_new_lost:
‹GC_remap⇧*⇧* S S' ⟹ dom (fst (snd S)) ⊆ set_mset (dom_m (fst S)) ⟹
dom (fst (snd S')) ⊆ set_mset (dom_m (fst S))›
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for y z
apply (cases ‹C ∈# dom_m (fst y)›)
apply (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin
dest: GC_remap_ran_m_remap GC_remap_ran_m_no_rewrite
intro: GC_remap_ran_m_lookup_kept GC_remap_ran_m_no_lost)
apply (smt GC_remap_ran_m_no_rewrite_map contra_subsetD domI prod.collapse rtranclp_GC_remap_ran_m_no_lost)
apply (smt GC_remap_ran_m_no_rewrite_map contra_subsetD domI prod.collapse rtranclp_GC_remap_ran_m_no_lost)
done
done
lemma rtranclp_GC_remap_map_ran:
assumes
‹GC_remap⇧*⇧* S S'› and
‹(the ∘∘ fst) (snd S) `# mset_set (dom (fst (snd S))) = dom_m (snd (snd S))› and
‹finite (dom (fst (snd S)))›
shows ‹finite (dom (fst (snd S'))) ∧
(the ∘∘ fst) (snd S') `# mset_set (dom (fst (snd S'))) = dom_m (snd (snd S'))›
using assms
proof (induction rule: rtranclp_induct)
case base
then show ?case by auto
next
case (step y z) note star = this(1) and st = this(2) and IH = this(3) and H = this(4-)
from st
show ?case
proof cases
case (remap_cons C' new C N m)
have ‹C ∉ dom m›
using step remap_cons by auto
then have [simp]: ‹{#the (if x = C then Some C' else m x). x ∈# mset_set (dom m)#} =
{#the (m x). x ∈# mset_set (dom m)#}›
apply (auto intro!: image_mset_cong split: if_splits)
by (metis empty_iff finite_set_mset_mset_set local.remap_cons(5) mset_set.infinite set_mset_empty)
show ?thesis
using step remap_cons
by (auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin
dest: GC_remap_ran_m_remap GC_remap_ran_m_no_rewrite
intro: GC_remap_ran_m_lookup_kept GC_remap_ran_m_no_lost dest: )
qed
qed
lemma rtranclp_GC_remap_ran_m_no_new_map:
‹GC_remap⇧*⇧* S S' ⟹ C ∈# dom_m (fst S') ⟹ C ∈# dom_m (fst S)›
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for y z
by (cases ‹C ∈# dom_m (fst y)›)
(auto simp: ran_m_lf_fmdrop ran_m_mapsto_upd_notin dest: GC_remap_ran_m_remap GC_remap_ran_m_no_rewrite
intro: GC_remap_ran_m_lookup_kept GC_remap_ran_m_no_lost)
done
lemma rtranclp_GC_remap_learned_clss_lD:
‹GC_remap⇧*⇧* (N, x, m) (N', x', m') ⟹ learned_clss_l N + learned_clss_l m = learned_clss_l N' + learned_clss_l m'›
by (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
(auto dest: GC_remap_learned_clss_l_old_new)
lemma rtranclp_GC_remap_learned_clss_l:
‹GC_remap⇧*⇧* (x1a, Map.empty, fmempty) (fmempty, m, x1ad) ⟹ learned_clss_l x1ad = learned_clss_l x1a›
by (auto dest!: rtranclp_GC_remap_learned_clss_lD[of _ _ _ _ _ _])
lemma remap_cons2:
assumes
‹C' ∉# dom_m new› and
‹C ∈# dom_m N› and
‹(the ∘∘ fst) (snd (N, m, new)) `# mset_set (dom (fst (snd (N, m, new)))) =
dom_m (snd (snd (N, m, new)))› and
‹⋀x. x ∈# dom_m (fst (N, m, new)) ⟹ x ∉ dom (fst (snd (N, m, new)))› and
‹finite (dom m)›
shows
‹GC_remap (N, m, new) (fmdrop C N, m(C ↦ C'), fmupd C' (the (fmlookup N C)) new)›
proof -
have 3: ‹C ∈ dom m ⟹ False›
apply (drule mk_disjoint_insert)
using assms
apply (auto 5 5 simp: ran_def)
done
have 4: ‹False› if C': ‹C' ∈ ran m›
proof -
obtain a where a: ‹a ∈ dom m› and [simp]: ‹m a = Some C'›
using that C' unfolding ran_def
by auto
show False
using mk_disjoint_insert[OF a] assms by (auto simp: union_single_eq_member)
qed
show ?thesis
apply (rule remap_cons)
apply (rule assms(1))
apply (rule assms(2))
apply (use 3 in fast)
apply (use 4 in fast)
done
qed
inductive_cases GC_remapE: ‹GC_remap S T›
lemma rtranclp_GC_remap_finite_map:
‹GC_remap⇧*⇧* S S' ⟹ finite (dom (fst (snd S))) ⟹ finite (dom (fst (snd S')))›
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for y z
by (auto elim: GC_remapE)
done
lemma rtranclp_GC_remap_old_dom_map:
‹GC_remap⇧*⇧* R S ⟹ (⋀x. x ∈# dom_m (fst R) ⟹ x ∉ dom (fst (snd R))) ⟹
(⋀x. x ∈# dom_m (fst S) ⟹ x ∉ dom (fst (snd S)))›
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for y z x
by (fastforce elim!: GC_remapE simp: distinct_mset_dom distinct_mset_set_mset_remove1_mset)
done
lemma remap_cons2_rtranclp:
assumes
‹(the ∘∘ fst) (snd R) `# mset_set (dom (fst (snd R))) = dom_m (snd (snd R))› and
‹⋀x. x ∈# dom_m (fst R) ⟹ x ∉ dom (fst (snd R))› and
‹finite (dom (fst (snd R)))› and
st: ‹GC_remap⇧*⇧* R S› and
C': ‹C' ∉# dom_m (snd (snd S))› and
C: ‹C ∈# dom_m (fst S)›
shows
‹GC_remap⇧*⇧* R (fmdrop C (fst S), (fst (snd S))(C ↦ C'), fmupd C' (the (fmlookup (fst S) C)) (snd (snd S)))›
proof -
have
1: ‹(the ∘∘ fst) (snd S) `# mset_set (dom (fst (snd S))) = dom_m (snd (snd S))› and
2: ‹⋀x. x ∈# dom_m (fst S) ⟹ x ∉ dom (fst (snd S))› and
3: ‹finite (dom (fst (snd S)))›
using assms(1) assms(3) assms(4) rtranclp_GC_remap_map_ran apply blast
apply (meson assms(2) assms(4) rtranclp_GC_remap_old_dom_map)
using assms(3) assms(4) rtranclp_GC_remap_finite_map by blast
have 5: ‹GC_remap S
(fmdrop C (fst S), (fst (snd S))(C ↦ C'), fmupd C' (the (fmlookup (fst S) C)) (snd (snd S)))›
using remap_cons2[OF C' C, of ‹(fst (snd S))›] 1 2 3 by (cases S) auto
show ?thesis
using 5 st by simp
qed
lemma (in -) fmdom_fmrestrict_set: ‹fmdrop xa (fmrestrict_set s N) = fmrestrict_set (s - {xa}) N›
by (rule fmap_ext_fmdom)
(auto simp: fset_fmdom_fmrestrict_set fmember.rep_eq notin_fset)
lemma (in -) GC_clauses_GC_remap:
‹GC_clauses N fmempty ≤ SPEC(λ(N'', m). GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, m, N'') ∧
0 ∉# dom_m N'')›
proof -
let ?remap = ‹(GC_remap)⇧*⇧* (N, λ_. None, fmempty)›
note remap = remap_cons2_rtranclp[of ‹(N, λ_. None, fmempty)›, of ‹(a, b, c)› for a b c, simplified]
define I where
‹I a b ≡ (λ(old :: nat clauses_l, new :: nat clauses_l, m :: nat ⇒ nat option).
?remap (old, m, new) ∧ 0 ∉# dom_m new ∧
set_mset (dom_m old) ⊆ set b)›
for a b :: ‹nat list›
have I0: ‹set_mset (dom_m N) ⊆ set x ⟹ I [] x (N, fmempty, λ_. None)› for x
unfolding I_def
by (auto intro!: fmap_ext_fmdom simp: fset_fmdom_fmrestrict_set fmember.rep_eq
notin_fset dom_m_def)
have I_drop: ‹I (l1 @ [xa]) l2
(fmdrop xa a, fmupd xb (a ∝ xa, irred a xa) aa, ba(xa ↦ xb))›
if
‹set_mset (dom_m N) ⊆ set x› and
‹x = l1 @ xa # l2› and
‹I l1 (xa # l2) σ› and
‹case σ of (N, N', m) ⇒ True› and
‹σ = (a, b)› and
‹b = (aa, ba)› and
‹xa ∈# dom_m a› and
‹xb ∉# dom_m aa ∧ xb ≠ 0›
for x xa l1 l2 σ a b aa ba xb
proof -
have ‹insert xa (set l2) - set l1 - {xa} = set l2 - insert xa (set l1)›
by auto
have ‹GC_remap⇧*⇧* (N, Map.empty, fmempty)
(fmdrop xa a, ba(xa ↦ xb), fmupd xb (the (fmlookup a xa)) aa)›
by (rule remap)
(use that in ‹auto simp: I_def›)
then show ?thesis
using that distinct_mset_dom[of a] distinct_mset_dom[of aa] unfolding I_def prod.simps
apply (auto dest!: mset_le_subtract[of ‹dom_m _› _ ‹{#xa#}›] simp: mset_set.insert_remove)
by (metis Diff_empty Diff_insert0 add_mset_remove_trivial finite_set_mset
finite_set_mset_mset_set insert_subset_eq_iff mset_set.remove set_mset_mset subseteq_remove1)
qed
have I_notin: ‹I (l1 @ [xa]) l2 (a, aa, ba)›
if
‹set_mset (dom_m N) ⊆ set x› and
‹x = l1 @ xa # l2› and
‹I l1 (xa # l2) σ› and
‹case σ of (N, N', m) ⇒ True› and
‹σ = (a, b)› and
‹b = (aa, ba)› and
‹xa ∉# dom_m a›
for x xa l1 l2 σ a b aa ba
proof -
show ?thesis
using that unfolding I_def
by (auto dest!: multi_member_split)
qed
have early_break: ‹GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, x2, x1)›
if
‹set_mset (dom_m N) ⊆ set x› and
‹x = l1 @ l2› and
‹I l1 l2 σ› and
‹¬ (case σ of (N, N', m) ⇒ True)› and
‹σ = (a, b)› and
‹b = (aa, ba)› and
‹(aa, ba) = (x1, x2)›
for x l1 l2 σ a b aa ba x1 x2
proof -
show ?thesis using that by auto
qed
have final_rel: ‹GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, x2, x1)›
if
‹set_mset (dom_m N) ⊆ set x› and
‹I x [] σ› and
‹case σ of (N, N', m) ⇒ True› and
‹σ = (a, b)› and
‹b = (aa, ba)› and
‹(aa, ba) = (x1, x2)›
proof -
show ‹GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, x2, x1)›
using that
by (auto simp: I_def)
qed
have final_rel: ‹GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, x2, x1)› ‹0 ∉# dom_m x1›
if
‹set_mset (dom_m N) ⊆ set x› and
‹I x [] σ› and
‹case σ of (N, N', m) ⇒ True› and
‹σ = (a, b)› and
‹b = (aa, ba)› and
‹(aa, ba) = (x1, x2)›
for x σ a b aa ba x1 x2
using that
by (auto simp: I_def)
show ?thesis
unfolding GC_clauses_def
apply (refine_vcg nfoldli_rule[where I = I])
subgoal by (rule I0)
subgoal by (rule I_drop)
subgoal by (rule I_notin)
subgoal for x l1 l2 σ a b aa ba x1 x2
by (rule early_break)
subgoal
by (auto simp: I_def)
subgoal
by (rule final_rel) assumption+
subgoal
by (rule final_rel) assumption+
done
qed
definition cdcl_twl_full_restart_l_prog where
‹cdcl_twl_full_restart_l_prog S = do {
― ‹ \<^term>‹remove_one_annot_true_clause_imp S››
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
}›
lemma cdcl_twl_restart_l_refl:
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_restart_l S S›
proof -
obtain M N D NE UE WS Q where S: ‹S = (M, N, D, NE, UE, WS, Q)›
by (cases S)
have [simp]: ‹Propagated L E ∈ set M ⟹ 0 < E ⟹E ∈# dom_m N› for L E
using list_invs unfolding S twl_list_invs_def
by auto
have [simp]: ‹0 ∉# dom_m N›
using list_invs unfolding S twl_list_invs_def
by auto
have n_d: ‹no_dup (get_trail_l S)›
using ST struct_invs 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
by (simp add: twl_st twl_st_l)
have [intro]: ‹Propagated L E ∈ set M ⟹
Propagated L E' ∈ set M ⟹ 0 < E ⟹ 0 < E' ⟹ N ∝ E = N ∝ E'› for L E E'
using n_d unfolding S
by (auto dest!: split_list elim!: list_match_lel_lel)
have [dest]: ‹Propagated L 0 ∈ set M ⟹
Propagated L E' ∈ set M ⟹
0 < E' ⟹ False› for E E' L
using n_d unfolding S
by (auto dest!: split_list elim!: list_match_lel_lel)
show ?thesis
using confl upd
by (auto simp: S cdcl_twl_restart_l.simps valid_trail_reduction_refl)
qed
definition cdcl_GC_clauses_pre :: ‹'v twl_st_l ⇒ bool› where
‹cdcl_GC_clauses_pre S ⟷ (
∃T. (S, T) ∈ twl_st_l None ∧
twl_list_invs S ∧ twl_struct_invs T ∧
get_conflict_l S = None ∧ clauses_to_update_l S = {#} ∧
count_decided (get_trail_l S) = 0 ∧ (∀L∈set (get_trail_l S). mark_of L = 0)
) ›
definition cdcl_GC_clauses :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹cdcl_GC_clauses = (λ(M, N, D, NE, UE, WS, Q). do {
ASSERT(cdcl_GC_clauses_pre (M, N, D, NE, UE, WS, Q));
b ← SPEC(λb. True);
if b then do {
(N', _) ← SPEC (λ(N'', m). GC_remap⇧*⇧* (N, Map.empty, fmempty) (fmempty, m, N'') ∧
0 ∉# dom_m N'');
RETURN (M, N', D, NE, UE, WS, Q)
}
else RETURN (M, N, D, NE, UE, WS, Q)})›
lemma cdcl_GC_clauses_cdcl_twl_restart_l:
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 = {#}› and
count_dec: ‹count_decided (get_trail_l S) = 0› and
mark: ‹∀L∈set (get_trail_l S). mark_of L = 0›
shows ‹cdcl_GC_clauses S ≤ SPEC (λT. cdcl_twl_restart_l S T ∧
get_trail_l S = get_trail_l T)›
proof -
show ?thesis
unfolding cdcl_GC_clauses_def
apply refine_vcg
subgoal using assms unfolding cdcl_GC_clauses_pre_def by blast
subgoal using confl upd count_dec mark by (auto simp: cdcl_twl_restart_l.simps
valid_trail_reduction_refl
dest: rtranclp_GC_remap_init_clss_l_old_new rtranclp_GC_remap_learned_clss_l_old_new)
subgoal
using cdcl_twl_restart_l_refl[OF assms(1-5)] by simp
subgoal
using cdcl_twl_restart_l_refl[OF assms(1-5)] by simp
subgoal
using cdcl_twl_restart_l_refl[OF assms(1-5)] by simp
done
qed
lemma remove_one_annot_true_clause_cdcl_twl_restart_l_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 ‹SPEC(remove_one_annot_true_clause⇧*⇧* S) ≤ SPEC(cdcl_twl_restart_l S)›
proof -
have ‹cdcl_twl_restart_l S U'›
if rem: ‹remove_one_annot_true_clause⇧*⇧* S U'› for U'
proof -
have n_d: ‹no_dup (get_trail_l S)›
using ST struct_invs 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
by (simp add: twl_st twl_st_l)
have ‹cdcl_twl_restart_l⇧*⇧* S U'›
using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[of S U' T, OF rem list_invs
confl upd ST struct_invs]
apply -
apply normalize_goal+
by auto
then show ‹cdcl_twl_restart_l S U'›
using cdcl_twl_restart_l_refl[OF ST list_invs struct_invs confl upd]
tranclp_cdcl_twl_restart_l_cdcl_is_cdcl_twl_restart_l[of S U', OF _ n_d]
by (meson rtranclp_into_tranclp2)
qed
then show ?thesis
by auto
qed
definition (in -) cdcl_twl_local_restart_l_spec :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹cdcl_twl_local_restart_l_spec = (λ(M, N, D, NE, UE, W, Q). do {
(M, Q) ← SPEC(λ(M', Q'). (∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧
Q' = {#}) ∨ (M' = M ∧ Q' = Q));
RETURN (M, N, D, NE, UE, W, Q)
})›
definition cdcl_twl_restart_l_prog where
‹cdcl_twl_restart_l_prog S = do {
b ← SPEC(λ_. True);
if b then cdcl_twl_local_restart_l_spec S else cdcl_twl_full_restart_l_prog S
}›
lemma cdcl_twl_local_restart_l_spec_cdcl_twl_restart_l:
assumes inv: ‹restart_abs_l_pre S False›
shows ‹cdcl_twl_local_restart_l_spec S ≤ SPEC (cdcl_twl_restart_l S)›
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 unfolding restart_abs_l_pre_def restart_prog_pre_def
apply - apply normalize_goal+
by (auto simp: twl_st_l twl_st)
have S: ‹S = (get_trail_l S, snd S)›
by (cases S) auto
obtain M N D NE UE W Q where
S: ‹S = (M, N, D, NE, UE, W, Q)›
by (cases S)
have restart: ‹cdcl_twl_restart_l S (M', N, D, NE, UE, W, Q')›
if decomp': ‹(∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧
Q' = {#}) ∨ (M' = M ∧ Q' = Q)›
for M' K M2 Q'
proof -
consider
(nope) ‹M = M'› and ‹Q' = Q› |
(decomp) K M2 where ‹(Decided K # M', M2) ∈ set (get_all_ann_decomposition M)› and
‹Q' = {#}›
using decomp' by auto
then show ?thesis
proof cases
case [simp]: nope
have valid: ‹valid_trail_reduction M M'›
by (use valid_trail_reduction.keep_red[of M'] in ‹auto simp: S›)
have
S1: ‹S = (M, N, None, NE, UE, {#}, Q)› and
S2 : ‹(M', N, D, NE, UE, W, Q') = (M', N, None, NE + mset `# {#}, UE + mset `# {#}, {#}, Q)›
using confl upd unfolding S
by auto
have
‹∀C∈#clauses_to_update_l S. C ∈# dom_m (get_clauses_l S)› and
dom0: ‹0 ∉# dom_m (get_clauses_l S)› and
annot: ‹⋀L C. Propagated L C ∈ set (get_trail_l S) ⟹
0 < C ⟹
(C ∈# dom_m (get_clauses_l S) ∧
L ∈ set (watched_l (get_clauses_l S ∝ C)) ∧
(length (get_clauses_l S ∝ C) > 2 ⟶ L = get_clauses_l S ∝ C ! 0))› and
‹distinct_mset (clauses_to_update_l S)›
using list_invs unfolding twl_list_invs_def S[symmetric] by auto
have n_d: ‹no_dup M›
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 by (auto simp: twl_st_l twl_st S)
have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M' ⟹ E=E'› for L E E'
using n_d
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E› M]
split_list[of ‹Propagated L E'› M]
dest: no_dup_same_annotD
elim!: list_match_lel_lel)
show ?thesis
unfolding S[symmetric] S1 S2
apply (rule cdcl_twl_restart_l.intros)
subgoal by (rule valid)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using propa_MM annot unfolding S by fastforce
subgoal using propa_MM annot unfolding S by fastforce
subgoal using propa_MM annot unfolding S by fastforce
subgoal using dom0 unfolding S by auto
subgoal by auto
done
next
case decomp note decomp = this(1) and Q = this(2)
have valid: ‹valid_trail_reduction M M'›
by (use valid_trail_reduction.backtrack_red[OF decomp, of M'] in ‹auto simp: S›)
have
‹∀C∈#clauses_to_update_l S. C ∈# dom_m (get_clauses_l S)› and
dom0: ‹0 ∉# dom_m (get_clauses_l S)› and
annot: ‹⋀L C. Propagated L C ∈ set (get_trail_l S) ⟹
0 < C ⟹
(C ∈# dom_m (get_clauses_l S) ∧
L ∈ set (watched_l (get_clauses_l S ∝ C)) ∧
(length (get_clauses_l S ∝ C) > 2 ⟶ L = get_clauses_l S ∝ C ! 0))› and
‹distinct_mset (clauses_to_update_l S)›
using list_invs unfolding twl_list_invs_def S[symmetric] by auto
obtain M3 where M: ‹M = M3 @ Decided K # M'›
using decomp by auto
have n_d: ‹no_dup M›
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 by (auto simp: twl_st_l twl_st S)
have
S1: ‹S = (M, N, None, NE, UE, {#}, Q)› and
S2 : ‹(M', N, D, NE, UE, W, Q') = (M', N, None, NE + mset `# {#}, UE + mset `# {#}, {#}, {#})›
using confl upd unfolding S Q
by auto
have propa_MM: ‹Propagated L E ∈ set M ⟹ Propagated L E' ∈ set M' ⟹ E=E'› for L E E'
using n_d unfolding M
by (auto simp: S twl_list_invs_def
dest!: split_list[of ‹Propagated L E› M]
split_list[of ‹Propagated L E'› M]
dest: no_dup_same_annotD
elim!: list_match_lel_lel)
show ?thesis
unfolding S[symmetric] S1 S2
apply (rule cdcl_twl_restart_l.intros)
subgoal by (rule valid)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using propa_MM annot unfolding S by fastforce
subgoal using propa_MM annot unfolding S by fastforce
subgoal using propa_MM annot unfolding S by fastforce
subgoal using dom0 unfolding S by auto
subgoal using decomp unfolding S by auto
done
qed
qed
show ?thesis
apply (subst S)
unfolding cdcl_twl_local_restart_l_spec_def prod.case RES_RETURN_RES2 less_eq_nres.simps
uncurry_def
apply clarify
apply (rule restart)
apply assumption
done
qed
definition (in -) cdcl_twl_local_restart_l_spec0 :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹cdcl_twl_local_restart_l_spec0 = (λ(M, N, D, NE, UE, W, Q). do {
(M, Q) ← SPEC(λ(M', Q'). (∃K M2. (Decided K # M', M2) ∈ set (get_all_ann_decomposition M) ∧
Q' = {#} ∧ count_decided M' = 0) ∨ (M' = M ∧ Q' = Q ∧ count_decided M' = 0));
RETURN (M, N, D, NE, UE, W, Q)
})›
lemma cdcl_twl_local_restart_l_spec0_cdcl_twl_local_restart_l_spec:
‹cdcl_twl_local_restart_l_spec0 S ≤ ⇓{(S, S'). S = S' ∧ count_decided (get_trail_l S) = 0}
(cdcl_twl_local_restart_l_spec S)›
unfolding cdcl_twl_local_restart_l_spec0_def
cdcl_twl_local_restart_l_spec_def
by refine_vcg (auto simp: RES_RETURN_RES2)
definition cdcl_twl_full_restart_l_GC_prog_pre
:: ‹'v twl_st_l ⇒ bool›
where
‹cdcl_twl_full_restart_l_GC_prog_pre S ⟷
(∃T. (S, T) ∈ twl_st_l None ∧ twl_struct_invs T ∧ twl_list_invs S ∧
get_conflict T = None)›
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_pre T);
U ← mark_to_delete_clauses_l T;
V ← cdcl_GC_clauses U;
ASSERT(cdcl_twl_restart_l S V);
RETURN V
}›
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 [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
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
unfolding mark_to_delete_clauses_l_pre_def
by (force intro: rtranclp_cdcl_twl_restart_l_list_invs)
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
lemma valid_trail_reduction_count_dec_ge:
‹valid_trail_reduction M M' ⟹ count_decided M ≥ count_decided M'›
apply (induction rule: valid_trail_reduction.induct)
subgoal for K M M'
using trail_renumber_count_dec
by (fastforce simp: dest!: get_all_ann_decomposition_exists_prepend)
subgoal by (auto dest: trail_renumber_count_dec)
done
lemma cdcl_twl_restart_l_count_dec_ge:
‹cdcl_twl_restart_l S T ⟹ count_decided (get_trail_l S) ≥ count_decided (get_trail_l T)›
by (induction rule: cdcl_twl_restart_l.induct)
(auto dest!: valid_trail_reduction_count_dec_ge)
lemma valid_trail_reduction_lit_of_nth:
‹valid_trail_reduction M M' ⟹ length M = length M' ⟹ i < length M ⟹
lit_of (M ! i) = lit_of (M' ! i)›
apply (induction rule: valid_trail_reduction.induct)
subgoal premises p for K M'' M2
using arg_cong[OF p(2), of length] p(1) arg_cong[OF p(2), of ‹λxs. xs ! i›] p(4)
by (auto simp: nth_map nth_append nth_Cons split: if_splits
dest!: get_all_ann_decomposition_exists_prepend)
subgoal premises p
using arg_cong[OF p(1), of length] p(3) arg_cong[OF p(1), of ‹λxs. xs ! i›] p(4)
by (auto simp: nth_map nth_append nth_Cons split: if_splits
dest!: get_all_ann_decomposition_exists_prepend)
done
lemma cdcl_twl_restart_l_lit_of_nth:
‹cdcl_twl_restart_l S U ⟹ i < length (get_trail_l U) ⟹ is_proped (get_trail_l U ! i) ⟹
length (get_trail_l S) = length (get_trail_l U) ⟹
lit_of (get_trail_l S ! i) = lit_of (get_trail_l U ! i)›
apply (induction rule: cdcl_twl_restart_l.induct)
subgoal for M M' N N' NE' UE' NE UE Q Q'
using valid_trail_reduction_length_leD[of M M']
valid_trail_reduction_lit_of_nth[of M M' i]
by auto
done
lemma valid_trail_reduction_is_decided_nth:
‹valid_trail_reduction M M' ⟹ length M = length M' ⟹ i < length M ⟹
is_decided (M ! i) = is_decided (M' ! i)›
apply (induction rule: valid_trail_reduction.induct)
subgoal premises p for K M'' M2
using arg_cong[OF p(2), of length] p(1) arg_cong[OF p(3), of ‹λxs. xs ! i›] p(4)
by (auto simp: nth_map nth_append nth_Cons split: if_splits
dest!: get_all_ann_decomposition_exists_prepend)
subgoal premises p
using arg_cong[OF p(1), of length] p(3) arg_cong[OF p(2), of ‹λxs. xs ! i›] p(4)
by (auto simp: nth_map nth_append nth_Cons split: if_splits
dest!: get_all_ann_decomposition_exists_prepend)
done
lemma cdcl_twl_restart_l_mark_of_same_or_0:
‹cdcl_twl_restart_l S U ⟹ i < length (get_trail_l U) ⟹ is_proped (get_trail_l U ! i) ⟹
length (get_trail_l S) = length (get_trail_l U) ⟹
(mark_of (get_trail_l U ! i) > 0 ⟹ mark_of (get_trail_l S ! i) > 0 ⟹
mset (get_clauses_l S ∝ mark_of (get_trail_l S ! i))
= mset (get_clauses_l U ∝ mark_of (get_trail_l U ! i)) ⟹ P) ⟹
(mark_of (get_trail_l U ! i) = 0 ⟹ P) ⟹ P›
apply (induction rule: cdcl_twl_restart_l.induct)
subgoal for M M' N N' NE' UE' NE UE Q Q'
using valid_trail_reduction_length_leD[of M M']
valid_trail_reduction_lit_of_nth[of M M' i]
valid_trail_reduction_is_decided_nth[of M M' i]
split_list[of ‹M ! i› M, OF nth_mem] split_list[of ‹M' ! i› M', OF nth_mem]
by (cases ‹M ! i›; cases ‹M' ! i›)
(force simp: all_conj_distrib)+
done
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'›
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' ∧ count_decided (get_trail_l S') = 0›
let ?f2 = ‹λ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
by (simp add: twl_st)
then have alt_def: ‹SPEC (?f S) ≥ do {
S' ← SPEC (λS'. ?f1 S S');
T ← SPEC (?f2 S');
U ← SPEC (?f2 T);
V ← SPEC (?f2 U);
RETURN V
}›
using cdcl_twl_restart_l_refl[OF assms(1-4)]
apply (auto simp: RES_RES_RETURN_RES)
by (meson cdcl_twl_restart_l_cdcl_twl_restart_l_is_cdcl_twl_restart_l)
have 1: ‹remove_one_annot_true_clause_imp T ≤ SPEC (?f2 U)›
if
‹(T, U) ∈ Id› and
‹U ∈ Collect (λS'. ?f1 S S')›
for T U
proof -
have ‹T = U› and ‹?f 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›
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'›
using cdcl_twl_restart_l_invs[OF assms(1-3) ‹?f 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 ‹cdcl_twl_restart_l 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_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›
using that by auto
then have ‹?f 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›
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'›
using cdcl_twl_restart_l_invs[OF assms(1-3) ‹?f S U›] by blast
then show ?thesis
unfolding mark_to_delete_clauses_l_pre_def
by blast
qed
have 2: ‹mark_to_delete_clauses_l U ≤ SPEC (?f2 U')›
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_pre U›
for T T' U U'
proof -
have ‹T = T'› ‹U = U'› and ‹?f T U› and ‹?f 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_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'
by (auto simp: cdcl_twl_restart_l.simps)
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)
qed
have 3: ‹cdcl_GC_clauses V ≤ SPEC (?f2 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_pre U› and
‹(V, V') ∈ Id› and
‹V' ∈ Collect (?f2 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› and ‹?f T U› and ‹?f 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
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 (elim cdcl_twl_restart_l_mark_of_same_or_0[OF ‹?f U V›, of i])
(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_ge[OF ‹?f U V›] that
by auto
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_pre U› and
‹(V, V') ∈ Id› and
‹V' ∈ Collect (?f2 U')› and
‹(W, W') ∈ Id› and
‹W' ∈ Collect (?f2 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
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
by fastforce
subgoal
by (rule cdcl_twl_local_restart_l_spec0_cdcl_twl_local_restart_l_spec[THEN order_trans],
subst (3) Down_id_eq[symmetric],
rule order_trans,
rule ref_two_step',
rule cdcl_twl_local_restart_l_spec_cdcl_twl_restart_l,
unfold restart_abs_l_pre_def, rule exI[of _ S'])
(use assms in ‹auto simp: restart_prog_pre_def conc_fun_RES›)
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
context twl_restart_ops
begin
definition restart_prog_l
:: "'v twl_st_l ⇒ nat ⇒ bool ⇒ ('v twl_st_l × nat) nres"
where
‹restart_prog_l S n brk = do {
ASSERT(restart_abs_l_pre S brk);
b ← restart_required_l S n;
b2 ← SPEC(λ_. True);
if b2 ∧ b ∧ ¬brk then do {
T ← cdcl_twl_full_restart_l_GC_prog S;
RETURN (T, n + 1)
}
else if b ∧ ¬brk then do {
T ← cdcl_twl_restart_l_prog S;
RETURN (T, n + 1)
}
else
RETURN (S, n)
}›
lemma restart_prog_l_restart_abs_l:
‹(uncurry2 restart_prog_l, uncurry2 restart_abs_l) ∈ Id ×⇩f nat_rel ×⇩f bool_rel →⇩f ⟨Id⟩nres_rel›
proof -
have cdcl_twl_full_restart_l_prog: ‹cdcl_twl_full_restart_l_prog S ≤ SPEC (cdcl_twl_restart_l S)›
if
inv: ‹restart_abs_l_pre S brk› and
‹(b, ba) ∈ bool_rel› and
‹b ∈ {b. b ⟶ f n < size (get_learned_clss_l S)}› and
‹ba ∈ {b. b ⟶ f n < size (get_learned_clss_l S)}› and
brk: ‹¬brk›
for b ba S brk n
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 brk› and
brk: ‹ba ∧ b2a ∧ ¬ brk›
for ba b2a brk S
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
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])
qed
have ‹restart_prog_l S n brk ≤ ⇓ Id (restart_abs_l S n brk)› for S n brk
unfolding restart_prog_l_def restart_abs_l_def restart_required_l_def cdcl_twl_restart_l_prog_def
apply (refine_vcg)
subgoal by auto
subgoal by (rule cdcl_twl_full_restart_l_GC_prog)
subgoal by auto
subgoal by auto
subgoal by (rule cdcl_twl_local_restart_l_spec_cdcl_twl_restart_l) auto
subgoal by (rule cdcl_twl_full_restart_l_prog) auto
subgoal by auto
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⇩0 =
do {
ebrk ← RES UNIV;
(_, brk, T, n) ← WHILE⇩T⇗λ(ebrk, brk, T, n). cdcl_twl_stgy_restart_abs_l_inv S⇩0 brk T n⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(_, brk, S, n).
do {
T ← unit_propagation_outer_loop_l S;
(brk, T) ← cdcl_twl_o_prog_l T;
(T, n) ← restart_abs_l 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_abs_l_inv S⇩0 brk T n⇖
(λ(brk, _). ¬brk)
(λ(brk, S, n).
do {
T ← unit_propagation_outer_loop_l S;
(brk, T) ← cdcl_twl_o_prog_l T;
(T, n) ← restart_abs_l T n brk;
RETURN (brk, T, n)
})
(False, T, 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⇩0 =
do {
ebrk ← RES UNIV;
(_, brk, T, n) ← WHILE⇩T⇗λ(ebrk, brk, T, n). cdcl_twl_stgy_restart_abs_l_inv S⇩0 brk T n⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(_, brk, S, n).
do {
T ← unit_propagation_outer_loop_l S;
(brk, T) ← cdcl_twl_o_prog_l T;
(T, n) ← restart_abs_l T n brk;
ebrk ← RES UNIV;
RETURN (ebrk, brk, T, n)
})
(ebrk, False, S⇩0, 0);
RETURN (brk, 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⇩0 =
do {
(brk, T, n) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_abs_l_inv S⇩0 brk T n⇖
(λ(brk, _). ¬brk)
(λ(brk, S, n).
do {
T ← unit_propagation_outer_loop_l S;
(brk, T) ← cdcl_twl_o_prog_l T;
(T, n) ← restart_prog_l T n brk;
RETURN (brk, T, n)
})
(False, S⇩0, 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⇩0 =
do {
ebrk ← RES UNIV;
(ebrk, brk, T, n) ← WHILE⇩T⇗λ(ebrk, brk, T, n). cdcl_twl_stgy_restart_abs_l_inv S⇩0 brk T n⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(ebrk, brk, S, n).
do {
T ← unit_propagation_outer_loop_l S;
(brk, T) ← cdcl_twl_o_prog_l T;
(T, n) ← restart_prog_l T n brk;
ebrk ← RES UNIV;
RETURN (ebrk, brk, T, n)
})
(ebrk, False, S⇩0, 0);
if ¬brk then do {
(brk, T, n) ← WHILE⇩T⇗λ(brk, T, n). cdcl_twl_stgy_restart_abs_l_inv S⇩0 brk T n⇖
(λ(brk, _). ¬brk)
(λ(brk, S, n).
do {
T ← unit_propagation_outer_loop_l S;
(brk, T) ← cdcl_twl_o_prog_l T;
(T, n) ← restart_prog_l T n brk;
RETURN (brk, T, n)
})
(False, T, 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 = ‹{((brk :: bool, S, n :: nat), (brk', S', n')).
(S, S') ∈ Id ∧ brk = brk' ∧ n = n'}›]
WHILEIT_refine[where R = ‹{((ebrk :: bool, brk :: bool, S, n :: nat), (ebrk', brk', S', n')).
(S, S') ∈ Id ∧ brk = brk' ∧ n = n' ∧ ebrk = ebrk'}› ]
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_l[THEN fref_to_Down_curry2])
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
subgoal by auto
done
qed
lemma cdcl_twl_stgy_restart_abs_early_l_cdcl_twl_stgy_restart_abs_early_l:
‹(cdcl_twl_stgy_restart_abs_early_l, cdcl_twl_stgy_restart_prog_early) ∈
{(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›
unfolding cdcl_twl_stgy_restart_abs_early_l_def cdcl_twl_stgy_restart_prog_early_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg WHILEIT_refine[where R = ‹{((brk :: bool, S, n :: nat), (brk', S', n')).
(S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ brk = brk' ∧ n = n' ∧
clauses_to_update_l S = {#}}›]
WHILEIT_refine[where R = ‹{((ebrk :: bool, brk :: bool, S, n :: nat), (ebrk' :: bool, brk', S', n')).
(S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ brk = brk' ∧ n = n' ∧ ebrk = ebrk' ∧
clauses_to_update_l S = {#}}›]
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])
subgoal by simp
subgoal for x y _ _ xa x' x1 x2 x1a x2a
unfolding cdcl_twl_stgy_restart_abs_l_inv_def
apply (rule_tac x=y in exI)
apply (rule_tac x=‹fst (snd (snd x'))› in exI)
by auto
subgoal by fast
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 _ _ xa x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e xb x'a x1f x2f x1g
unfolding cdcl_twl_stgy_restart_abs_l_inv_def
apply (rule_tac x=y in exI)
apply (rule_tac x=‹fst (snd x'a)› in exI)
by auto
subgoal by auto
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
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
lemma (in twl_restart) cdcl_twl_stgy_restart_prog_early_l_cdcl_twl_stgy_restart_prog_early:
‹(cdcl_twl_stgy_restart_prog_early_l, cdcl_twl_stgy_restart_prog_early)
∈ {(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_early_l_cdcl_twl_stgy_restart_abs_early_l[THEN fref_to_Down])
apply fast
apply assumption
apply (rule cdcl_twl_stgy_restart_prog_early_l_cdcl_twl_stgy_restart_abs_early_l[THEN fref_to_Down,
simplified])
apply simp
done
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 = ‹{((brk :: bool, S, n :: nat), (brk', S', n')).
(S, S') ∈ Id ∧ brk = brk' ∧ n = n'}›]
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_l[THEN fref_to_Down_curry2])
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
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⇩0 =
do {
ebrk ← RES UNIV;
(ebrk, brk, T, n) ← WHILE⇩T⇗λ(ebrk, brk, T, n). cdcl_twl_stgy_restart_abs_l_inv S⇩0 brk T n⇖
(λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
(λ(ebrk, brk, S, n).
do {
T ← unit_propagation_outer_loop_l S;
(brk, T) ← cdcl_twl_o_prog_l T;
(T, n) ← restart_prog_l T n brk;
ebrk ← RES UNIV;
RETURN (ebrk, brk, T, n)
})
(ebrk, False, S⇩0, 0);
RETURN (brk, T)
}›
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, 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 = ‹{((ebrk :: bool, brk :: bool, S, n :: nat), (ebrk' :: bool, brk', S', n')).
(S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ brk = brk' ∧ n = n' ∧ ebrk = ebrk' ∧
clauses_to_update_l S = {#}}›]
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])
subgoal by simp
subgoal for x y _ _ xa x' x1 x2 x1a x2a
unfolding cdcl_twl_stgy_restart_abs_l_inv_def
apply (rule_tac x=y in exI)
apply (rule_tac x=‹fst (snd (snd x'))› in exI)
by auto
subgoal by fast
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
done
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, 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_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 = ‹{((brk :: bool, S, n :: nat), (brk', S', n')).
(S, S') ∈ Id ∧ brk = brk' ∧ n = n'}›]
WHILEIT_refine[where R = ‹{((ebrk :: bool, brk :: bool, S, n :: nat), (ebrk', brk', S', n')).
(S, S') ∈ Id ∧ brk = brk' ∧ n = n' ∧ ebrk = ebrk'}› ]
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_l[THEN fref_to_Down_curry2])
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
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