Theory Watched_Literals_List_Inprocessing
theory Watched_Literals_List_Inprocessing
imports Watched_Literals_List Watched_Literals_Algorithm_Reduce
begin
definition all_learned_lits_of_l :: ‹'v twl_st_l ⇒ 'v clause› where
‹all_learned_lits_of_l S' ≡ all_lits_of_mm (mset `# learned_clss_lf (get_clauses_l S') + get_unit_learned_clss_l S' +
get_subsumed_learned_clauses_l S' + get_learned_clauses0_l S')›
definition all_init_lits_of_l :: ‹'v twl_st_l ⇒ 'v clause› where
‹all_init_lits_of_l S' ≡ all_lits_of_mm (mset `# get_init_clss_l S' + get_unit_init_clauses_l S' +
get_subsumed_init_clauses_l S' + get_init_clauses0_l S')›
inductive cdcl_twl_subsumed_l :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
subsumed_II:
‹cdcl_twl_subsumed_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmdrop C' N, D, NE, UE, NEk, UEk, add_mset (mset (N ∝ C')) NS, US, N0, U0, {#}, Q)›
if ‹mset (N ∝ C) ⊆# mset (N ∝ C')› ‹C ∈# dom_m N› ‹C' ∈# dom_m N›
‹irred N C'› ‹irred N C› ‹C ≠ C'› ‹C' ∉ set (get_all_mark_of_propagated M)›|
subsumed_RR:
‹cdcl_twl_subsumed_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmdrop C' N, D, NE, UE, NEk, UEk, NS, add_mset (mset (N ∝ C')) US, N0, U0, {#}, Q)›
if ‹mset (N ∝ C) ⊆# mset (N ∝ C')› ‹C ∈# dom_m N› ‹C' ∈# dom_m N›
‹¬irred N C'› ‹¬irred N C›‹C ≠ C'› ‹C' ∉ set (get_all_mark_of_propagated M)›|
subsumed_IR:
‹cdcl_twl_subsumed_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmdrop C' N, D, NE, UE, NEk, UEk, NS, add_mset (mset (N ∝ C')) US, N0, U0, {#}, Q)›
if ‹mset (N ∝ C) ⊆# mset (N ∝ C')› ‹C ∈# dom_m N› ‹C' ∈# dom_m N›
‹irred N C› ‹¬irred N C'› ‹C' ∉ set (get_all_mark_of_propagated M)› |
subsumed_RI:
‹cdcl_twl_subsumed_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmupd C (N ∝ C, True) (fmdrop C' N), D, NE, UE, NEk, UEk, add_mset (mset (N ∝ C')) NS, US, N0, U0, {#}, Q)›
if ‹mset (N ∝ C) ⊆# mset (N ∝ C')› ‹C ∈# dom_m N› ‹C' ∈# dom_m N›
‹¬irred N C› ‹irred N C'› ‹C' ∉ set (get_all_mark_of_propagated M)›
‹¬tautology (mset (N ∝ C))›
‹distinct_mset (mset (N ∝ C))›
lemma convert_lits_l_drop:
‹C ∉ set (get_all_mark_of_propagated M) ⟹
(M, M') ∈ convert_lits_l (fmdrop C N) E ⟷ (M, M') ∈ convert_lits_l N E›
unfolding convert_lits_l_def list_rel_def in_pair_collect_simp
apply (rule iffI; (rule list.rel_mono_strong, assumption))
apply (auto simp: convert_lits_l_def list_rel_def p2rel_def convert_lit.simps
cdcl⇩W_restart_mset.in_get_all_mark_of_propagated_in_trail)
done
lemma convert_lits_l_update_sel:
‹C ∈# dom_m N ⟹ C' = N ∝ C ⟹
(M, M') ∈ convert_lits_l (fmupd C (C', b) N) E ⟷ (M, M') ∈ convert_lits_l N E›
unfolding convert_lits_l_def list_rel_def in_pair_collect_simp
apply (rule iffI; (rule list.rel_mono_strong, assumption))
apply (auto simp: convert_lits_l_def list_rel_def p2rel_def convert_lit.simps
cdcl⇩W_restart_mset.in_get_all_mark_of_propagated_in_trail)
done
lemma learned_clss_l_mapsto_upd_in_irrelev: ‹C ∈# dom_m N ⟹ ¬irred N C ⟹
learned_clss_l (fmupd C (C', True) N) = remove1_mset (N ∝ C, irred N C) (learned_clss_l N)›
by (auto simp: ran_m_mapsto_upd_notin ran_m_mapsto_upd)
lemma init_clss_l_mapsto_upd_irrelev:
‹C ∈# dom_m N ⟹ ¬irred N C ⟹
init_clss_l (fmupd C (C', True) N) = add_mset (C', True) ((init_clss_l N))›
by (auto simp: ran_m_mapsto_upd)
lemma cdcl_twl_subsumed_l_cdcl_twl_subsumed:
assumes ‹cdcl_twl_subsumed_l S T› and
SS': ‹(S, S') ∈ twl_st_l None›
shows ‹∃T'. (T, T') ∈ twl_st_l None ∧ cdcl_twl_subsumed S' T'›
proof -
obtain M' N' U' D' NE' UE' NS' US' WS' N0' U0' Q' where
S': ‹S' = (M', N', U', D', NE', UE',NS', US', N0', U0', WS', Q')›
by (cases S')
show ?thesis
using assms(1)
proof (cases rule: cdcl_twl_subsumed_l.cases)
case (subsumed_II N C C' M D NE UE NEk UEk NS US N0 U0 Q)
define N'' where ‹N'' = (N' - {#twl_clause_of (N ∝ C), twl_clause_of (N ∝ C')#})›
let ?E = ‹twl_clause_of (N ∝ C)›
let ?E' = ‹twl_clause_of (N ∝ C')›
have ‹(N ∝ C, irred N C) ∈# init_clss_l N› and
H: ‹(N ∝ C', irred N C') ∈# remove1_mset (N ∝ C, irred N C)(init_clss_l N)›
using subsumed_II
apply (auto dest!: multi_member_split simp: ran_m_def add_mset_eq_add_mset remove1_mset_add_mset_If
split: if_splits)
apply (metis prod.collapse)+
done
from multi_member_split[OF this(1)] multi_member_split[OF this(2)]
have ‹N' = N'' + {#twl_clause_of (N ∝ C), twl_clause_of (N ∝ C')#}›
using subsumed_II SS' unfolding N''_def
by (auto simp: ran_m_def S' twl_st_l_def add_mset_eq_add_mset dest!: multi_member_split)
then show ?thesis
using SS' subsumed_II H unfolding S'
apply (auto simp: add_mset_eq_add_mset image_mset_Diff conj_disj_distribL
conj_disj_distribR eq_commute[of ‹twl_clause_of _›] eq_commute[of ‹remove1_mset _ _›]
S' convert_lits_l_drop learned_clss_l_l_fmdrop_irrelev init_clss_l_fmdrop_irrelev image_mset_remove1_mset_if
eq_commute[of ‹add_mset _ (add_mset _ _)› ‹image_mset _ _›]
twl_st_l_def mset_take_mset_drop_mset' learned_clss_l_l_fmdrop_irrelev
simp del: twl_clause_of.simps
simp flip: twl_clause_of.simps
dest!: intro!: exI[of _ ‹get_trail S'›])
apply (auto simp: init_clss_l_fmdrop_irrelev image_mset_remove1_mset_if
eq_commute[of ‹add_mset _ (add_mset _ _)› ‹image_mset _ _›]
twl_st_l_def mset_take_mset_drop_mset' learned_clss_l_l_fmdrop_irrelev init_clss_l_fmdrop
intro!: cdcl_twl_subsumed_II_simp[where C = ?E and C' = ?E'])
done
next
case (subsumed_RR N C C' M D NE UE NEk UEk NS US N0 U0 Q)
define U'' where ‹U'' = (U' - {#twl_clause_of (N ∝ C), twl_clause_of (N ∝ C')#})›
let ?E = ‹twl_clause_of (N ∝ C)›
let ?E' = ‹twl_clause_of (N ∝ C')›
have ‹(N ∝ C, irred N C) ∈# learned_clss_l N› and
H: ‹(N ∝ C', irred N C') ∈# remove1_mset (N ∝ C, irred N C)(learned_clss_l N)›
using subsumed_RR
apply (auto dest!: multi_member_split simp: ran_m_def add_mset_eq_add_mset remove1_mset_add_mset_If
split: if_splits)
apply (metis prod.collapse)+
done
from multi_member_split[OF this(1)] multi_member_split[OF this(2)]
have ‹U' = U'' + {#twl_clause_of (N ∝ C), twl_clause_of (N ∝ C')#}›
using subsumed_RR SS' unfolding U''_def
by (auto simp: ran_m_def S' twl_st_l_def add_mset_eq_add_mset dest!: multi_member_split)
then show ?thesis
using SS' subsumed_RR H unfolding S'
apply (auto simp: add_mset_eq_add_mset image_mset_Diff conj_disj_distribL
conj_disj_distribR eq_commute[of ‹twl_clause_of _›] eq_commute[of ‹remove1_mset _ _›]
S' convert_lits_l_drop learned_clss_l_l_fmdrop_irrelev init_clss_l_fmdrop_irrelev image_mset_remove1_mset_if
eq_commute[of ‹add_mset _ (add_mset _ _)› ‹image_mset _ _›]
twl_st_l_def mset_take_mset_drop_mset'
simp del: twl_clause_of.simps
simp flip: twl_clause_of.simps
dest!: intro!: exI[of _ ‹get_trail S'›])
apply (auto simp: init_clss_l_fmdrop_irrelev image_mset_remove1_mset_if
eq_commute[of ‹add_mset _ (add_mset _ _)› ‹image_mset _ _›]
twl_st_l_def mset_take_mset_drop_mset' learned_clss_l_l_fmdrop_irrelev init_clss_l_fmdrop
learned_clss_l_l_fmdrop
cdcl_twl_subsumed_RR_simp[where C = ?E and C' = ?E'])
done
next
case (subsumed_IR N C C' M D NE UE NEk UEk NS US N0 U0 Q)
define U'' where ‹U'' = (U' - {#twl_clause_of (N ∝ C')#})›
define N'' where ‹N'' = (N' - {#twl_clause_of (N ∝ C)#})›
let ?E = ‹twl_clause_of (N ∝ C)›
let ?E' = ‹twl_clause_of (N ∝ C')›
have ‹(N ∝ C, irred N C) ∈# init_clss_l N› and
H: ‹(N ∝ C', irred N C') ∈# (learned_clss_l N)›
using subsumed_IR
apply (auto dest!: multi_member_split simp: ran_m_def add_mset_eq_add_mset remove1_mset_add_mset_If
split: if_splits)
apply (metis prod.collapse)+
done
from multi_member_split[OF this(1)] multi_member_split[OF this(2)]
have ‹U' = U'' + {#twl_clause_of (N ∝ C')#}› ‹N' = N'' + {#twl_clause_of (N ∝ C)#}›
using subsumed_IR SS' unfolding U''_def N''_def
by (auto simp: ran_m_def S' twl_st_l_def add_mset_eq_add_mset dest!: multi_member_split)
then show ?thesis
using SS' subsumed_IR H unfolding S'
apply (auto simp: add_mset_eq_add_mset image_mset_Diff conj_disj_distribL
conj_disj_distribR eq_commute[of ‹twl_clause_of _›] eq_commute[of ‹remove1_mset _ _›]
S' convert_lits_l_drop learned_clss_l_l_fmdrop_irrelev init_clss_l_fmdrop_irrelev image_mset_remove1_mset_if
eq_commute[of ‹add_mset _ (add_mset _ _)› ‹image_mset _ _›]
twl_st_l_def mset_take_mset_drop_mset'
simp del: twl_clause_of.simps
simp flip: twl_clause_of.simps
dest!: intro!: exI[of _ ‹get_trail S'›])
apply (auto simp: init_clss_l_fmdrop_irrelev image_mset_remove1_mset_if
eq_commute[of ‹add_mset _ (add_mset _ _)› ‹image_mset _ _›]
twl_st_l_def mset_take_mset_drop_mset' learned_clss_l_l_fmdrop_irrelev init_clss_l_fmdrop
learned_clss_l_l_fmdrop
cdcl_twl_subsumed_IR_simp[where C = ?E and C' = ?E'])
done
next
case (subsumed_RI N C C' M D NE UE NEk UEk NS US N0 U0 Q)
define U'' where ‹U'' = (U' - {#twl_clause_of (N ∝ C)#})›
define N'' where ‹N'' = (N' - {#twl_clause_of (N ∝ C')#})›
let ?E = ‹twl_clause_of (N ∝ C)›
let ?E' = ‹twl_clause_of (N ∝ C')›
have ‹(N ∝ C', irred N C') ∈# init_clss_l N› and
H: ‹(N ∝ C, irred N C) ∈# (learned_clss_l N)› and
[simp,iff]: ‹C ∈# remove1_mset C' (dom_m N)› ‹¬ irred (fmdrop C' N) C› ‹C ≠ C'›
‹(N ∝ C, False) ∈# learned_clss_l N›
using subsumed_RI
apply (auto dest!: multi_member_split simp: ran_m_def add_mset_eq_add_mset remove1_mset_add_mset_If
split: if_splits)
apply (metis prod.collapse)+
done
from multi_member_split[OF this(1)] multi_member_split[OF this(2)]
have ‹U' = U'' + {#twl_clause_of (N ∝ C)#}› ‹N' = N'' + {#twl_clause_of (N ∝ C')#}›
using subsumed_RI SS' unfolding U''_def N''_def
by (auto simp: ran_m_def S' twl_st_l_def add_mset_eq_add_mset dest!: multi_member_split)
then show ?thesis
using SS' subsumed_RI H unfolding S'
apply (auto simp: add_mset_eq_add_mset image_mset_Diff conj_disj_distribL
conj_disj_distribR eq_commute[of ‹twl_clause_of _›] eq_commute[of ‹remove1_mset _ _›]
S' convert_lits_l_drop learned_clss_l_l_fmdrop_irrelev init_clss_l_fmdrop_irrelev image_mset_remove1_mset_if
eq_commute[of ‹add_mset _ (add_mset _ _)› ‹image_mset _ _›] convert_lits_l_update_sel
twl_st_l_def mset_take_mset_drop_mset'
simp del: twl_clause_of.simps
simp flip: twl_clause_of.simps
dest!: intro!: exI[of _ ‹get_trail S'›])
apply (auto simp: init_clss_l_fmdrop_irrelev image_mset_remove1_mset_if
eq_commute[of ‹add_mset _ (add_mset _ _)› ‹image_mset _ _›]
twl_st_l_def mset_take_mset_drop_mset' learned_clss_l_l_fmdrop_irrelev init_clss_l_fmdrop
learned_clss_l_l_fmdrop convert_lits_l_drop learned_clss_l_mapsto_upd_in_irrelev
init_clss_l_mapsto_upd init_clss_l_mapsto_upd_irrelev
intro!: cdcl_twl_subsumed_RI_simp[where C = ?E and C' = ?E'])
done
qed
qed
lemma cdcl_twl_subsumed_l_list_invs:
‹cdcl_twl_subsumed_l S T ⟹ twl_list_invs S ⟹ twl_list_invs T›
apply (induction rule: cdcl_twl_subsumed_l.induct)
apply (auto simp: twl_list_invs_def cdcl⇩W_restart_mset.in_get_all_mark_of_propagated_in_trail
ran_m_mapsto_upd distinct_mset_remove1_All distinct_mset_dom
ran_m_lf_fmdrop
dest: in_diffD)
apply (subst (asm) ran_m_mapsto_upd)
apply (auto dest!: in_diffD simp: distinct_mset_remove1_All distinct_mset_dom
ran_m_lf_fmdrop)
done
inductive cdcl_twl_subresolution_l :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
twl_subresolution_II_nonunit:
‹cdcl_twl_subresolution_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmupd C' (E, True) N, None, NE, UE, NEk, UEk, add_mset (mset (N ∝ C')) NS, US, N0, U0, {#}, Q)›
if
‹C ∈# dom_m N›
‹C' ∈# dom_m N›
‹mset (N ∝ C) = add_mset L D›
‹mset (N ∝ C') = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'›
‹mset E = remdups_mset D'› ‹length E ≥ 2› ‹distinct E› ‹∀L ∈# mset E. undefined_lit M L›
‹C' ∉ set (get_all_mark_of_propagated M)› ‹irred N C› ‹irred N C'› |
twl_subresolution_II_unit:
‹cdcl_twl_subresolution_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(Propagated K 0 # M, fmdrop C' N, None, NE, UE, add_mset {#K#} NEk, UEk, add_mset (mset (N ∝ C')) NS, US, N0, U0, {#}, add_mset (-K) Q)›
if
‹C ∈# dom_m N›
‹C' ∈# dom_m N›
‹mset (N ∝ C) = add_mset L D›
‹mset (N ∝ C') = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'›
‹remdups_mset D' = {#K#}›
‹undefined_lit M K›
‹C' ∉ set (get_all_mark_of_propagated M)› ‹irred N C› ‹irred N C'› |
twl_subresolution_LL_nonunit:
‹cdcl_twl_subresolution_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmupd C' (E, False) N, None, NE, UE, NEk, UEk, NS, add_mset (mset (N ∝ C')) US, N0, U0, {#}, Q)›
if
‹C ∈# dom_m N›
‹C' ∈# dom_m N›
‹mset (N ∝ C) = add_mset L D›
‹mset (N ∝ C') = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'› ‹¬tautology (D + D')›
‹mset E = remdups_mset D'› ‹length E ≥ 2› ‹distinct E› ‹∀L ∈# mset E. undefined_lit M L›
‹C' ∉ set (get_all_mark_of_propagated M)› ‹¬irred N C› ‹¬irred N C'› |
twl_subresolution_LL_unit:
‹cdcl_twl_subresolution_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(Propagated K 0 # M, fmdrop C' N, None, NE, UE, NEk, add_mset {#K#} UEk, NS, add_mset (mset (N ∝ C')) US, N0, U0, {#}, add_mset (-K) Q)›
if
‹C ∈# dom_m N›
‹C' ∈# dom_m N›
‹mset (N ∝ C) = add_mset L D›
‹mset (N ∝ C') = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'›
‹remdups_mset D' = {#K#}›
‹undefined_lit M K›
‹C' ∉ set (get_all_mark_of_propagated M)› ‹¬irred N C› ‹¬irred N C'› |
twl_subresolution_LI_nonunit:
‹cdcl_twl_subresolution_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmupd C' (E, False) N, None, NE, UE, NEk, UEk, NS, add_mset (mset (N ∝ C')) US, N0, U0, {#}, Q)›
if
‹C ∈# dom_m N›
‹C' ∈# dom_m N›
‹mset (N ∝ C) = add_mset L D›
‹mset (N ∝ C') = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'›
‹mset E = remdups_mset D'› ‹length E ≥ 2› ‹distinct E› ‹∀L ∈# mset E. undefined_lit M L›
‹C' ∉ set (get_all_mark_of_propagated M)› ‹irred N C› ‹¬irred N C'› |
twl_subresolution_LI_unit:
‹cdcl_twl_subresolution_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(Propagated K 0 # M, fmdrop C' N, None, NE, UE, NEk, add_mset {#K#} UEk, NS, add_mset (mset (N ∝ C')) US, N0, U0, {#}, add_mset (-K) Q)›
if
‹C ∈# dom_m N›
‹C' ∈# dom_m N›
‹mset (N ∝ C) = add_mset L D›
‹mset (N ∝ C') = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'›
‹remdups_mset D' = {#K#}›
‹undefined_lit M K›
‹C' ∉ set (get_all_mark_of_propagated M)› ‹irred N C› ‹¬irred N C'› |
twl_subresolution_IL_nonunit:
‹cdcl_twl_subresolution_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmupd C' (E, True) N, None, NE, UE, NEk, UEk, add_mset (mset (N ∝ C')) NS, US, N0, U0, {#}, Q)›
if
‹C ∈# dom_m N›
‹C' ∈# dom_m N›
‹mset (N ∝ C) = add_mset L D›
‹mset (N ∝ C') = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'›
‹mset E = remdups_mset D'› ‹length E ≥ 2› ‹distinct E› ‹∀L ∈# mset E. undefined_lit M L›
‹C' ∉ set (get_all_mark_of_propagated M)› ‹¬irred N C› ‹irred N C'› |
twl_subresolution_IL_unit:
‹cdcl_twl_subresolution_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(Propagated K 0 # M, fmdrop C' N, None, NE, UE, add_mset {#K#} NEk, UEk, add_mset (mset (N ∝ C')) NS, US, N0, U0, {#}, add_mset (-K) Q)›
if
‹C ∈# dom_m N›
‹C' ∈# dom_m N›
‹mset (N ∝ C) = add_mset L D›
‹mset (N ∝ C') = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'›
‹remdups_mset D' = {#K#}›
‹undefined_lit M K›
‹C' ∉ set (get_all_mark_of_propagated M)› ‹¬irred N C› ‹irred N C'›
lemma convert_lits_l_update_sel2:
‹C ∈# dom_m N ⟹ C ∉ set (get_all_mark_of_propagated M) ⟹
(M, M') ∈ convert_lits_l (fmupd C (C', b) N) E ⟷ (M, M') ∈ convert_lits_l N E›
unfolding convert_lits_l_def list_rel_def in_pair_collect_simp
apply (rule iffI; (rule list.rel_mono_strong, assumption))
apply (auto simp: convert_lits_l_def list_rel_def p2rel_def convert_lit.simps
cdcl⇩W_restart_mset.in_get_all_mark_of_propagated_in_trail)
done
lemma twl_subresolution_II_nonunit_simps:
‹cdcl_twl_subresolution S T›
if
‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (M, add_mset E (remove1_mset C' N), U, None, NE, UE, add_mset (clause C') NS, US, N0, U0, {#}, Q)›
‹clause C = add_mset L D›
‹clause C' = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'› ‹¬tautology (D + D')›
‹clause E = remdups_mset D'› ‹size (watched E) = 2› ‹struct_wf_twl_cls E›
‹∀L ∈# clause E. undefined_lit M L›
‹C ∈# N›
‹C' ∈# N›
using cdcl_twl_subresolution.twl_subresolution_II_nonunit[of C L D C' D' M E ‹N - {#C, C'#}› U] that
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset add_mset_commute)
lemma twl_subresolution_II_unit_simps:
‹cdcl_twl_subresolution S T›
if
‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (Propagated K {#K#} # M, (remove1_mset C' N), U, None, add_mset {#K#} NE, UE, add_mset (clause C') NS, US, N0, U0, {#}, add_mset (-K) Q)›
‹clause C = add_mset L D›
‹clause C' = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'› ‹¬tautology (D + D')›
‹remdups_mset D' = {#K#}›
‹undefined_lit M K›
‹C ∈# N›
‹C' ∈# N›
using cdcl_twl_subresolution.twl_subresolution_II_unit[of C L D C' D' M K ‹N - {#C, C'#}› U] that
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset add_mset_commute)
lemma twl_subresolution_LL_nonunit_simps:
‹cdcl_twl_subresolution S T›
if
‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (M, N, add_mset E (remove1_mset C' U), None, NE, UE, NS, add_mset (clause C') US, N0, U0, {#}, Q)›
‹clause C = add_mset L D›
‹clause C' = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'› ‹¬tautology (D + D')›
‹clause E = remdups_mset D'› ‹size (watched E) = 2› ‹struct_wf_twl_cls E›
‹∀L ∈# clause E. undefined_lit M L›
‹C ∈# U›
‹C' ∈# U›
using cdcl_twl_subresolution.twl_subresolution_LL_nonunit[of C L D C' D' M E N ‹U - {#C, C'#}›] that
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset add_mset_commute)
lemma twl_subresolution_LL_unit_simps:
‹cdcl_twl_subresolution S T›
if
‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (Propagated K {#K#} # M, (N), remove1_mset C' U, None, NE, add_mset {#K#} UE,
NS, add_mset (clause C') US, N0, U0, {#}, add_mset (-K) Q)›
‹clause C = add_mset L D›
‹clause C' = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'› ‹¬tautology (D + D')›
‹remdups_mset D' = {#K#}›
‹undefined_lit M K›
‹C ∈# U›
‹C' ∈# U›
using cdcl_twl_subresolution.twl_subresolution_LL_unit[of C L D C' D' M K N ‹U - {#C, C'#}›] that
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset add_mset_commute)
lemma twl_subresolution_LI_nonunit_simps:
‹cdcl_twl_subresolution S T›
if
‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (M, N, add_mset E (remove1_mset C' U), None, NE, UE, NS, add_mset (clause C') US, N0, U0, {#}, Q)›
‹clause C = add_mset L D›
‹clause C' = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'› ‹¬tautology (D + D')›
‹clause E = remdups_mset D'› ‹size (watched E) = 2› ‹struct_wf_twl_cls E›
‹∀L ∈# clause E. undefined_lit M L›
‹C ∈# N›
‹C' ∈# U›
using cdcl_twl_subresolution.twl_subresolution_LI_nonunit[of C L D C' D' M E ‹N - {#C#}› ‹U - {#C'#}›] that
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset add_mset_commute)
lemma twl_subresolution_LI_unit_simps:
‹cdcl_twl_subresolution S T›
if
‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (Propagated K {#K#} # M, (N), remove1_mset C' U, None, NE, add_mset {#K#} UE,
NS, add_mset (clause C') US, N0, U0, {#}, add_mset (-K) Q)›
‹clause C = add_mset L D›
‹clause C' = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'› ‹¬tautology (D + D')›
‹remdups_mset D' = {#K#}›
‹undefined_lit M K›
‹C ∈# N›
‹C' ∈# U›
using cdcl_twl_subresolution.twl_subresolution_LI_unit[of C L D C' D' M K ‹N - {#C#}› ‹U - {#C'#}›] that
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset add_mset_commute)
lemma twl_subresolution_IL_nonunit_simps:
‹cdcl_twl_subresolution S T›
if
‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (M, add_mset E (remove1_mset C' N), U, None, NE, UE, add_mset (clause C') NS, US, N0, U0, {#}, Q)›
‹clause C = add_mset L D›
‹clause C' = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'› ‹¬tautology (D + D')›
‹clause E = remdups_mset D'› ‹size (watched E) = 2› ‹struct_wf_twl_cls E›
‹∀L ∈# clause E. undefined_lit M L›
‹C' ∈# N›
‹C ∈# U›
using cdcl_twl_subresolution.twl_subresolution_IL_nonunit[of C L D C' D' M E ‹N - {#C'#}› ‹U - {#C#}›] that
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset add_mset_commute)
lemma twl_subresolution_IL_unit_simps:
‹cdcl_twl_subresolution S T›
if
‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (Propagated K {#K#} # M, remove1_mset C' N, U, None, add_mset {#K#} NE, UE,
add_mset (clause C') NS, US, N0, U0, {#}, add_mset (-K) Q)›
‹clause C = add_mset L D›
‹clause C' = add_mset (-L) D'›
‹count_decided M = 0› ‹D ⊆# D'› ‹¬tautology (D + D')›
‹remdups_mset D' = {#K#}›
‹undefined_lit M K›
‹C' ∈# N›
‹C ∈# U›
using cdcl_twl_subresolution.twl_subresolution_IL_unit[of C L D C' D' M K ‹N - {#C'#}› ‹U - {#C#}›] that
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset add_mset_commute)
lemma cdcl_twl_subresolution_l_cdcl_twl_subresolution:
assumes ‹cdcl_twl_subresolution_l S T› and
SS': ‹(S, S') ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S›
shows ‹∃T'. (T, T') ∈ twl_st_l None ∧ cdcl_twl_subresolution S' T'›
proof -
have tauto: ‹∀C∈#dom_m (get_clauses_l S). ¬tautology (mset (get_clauses_l S ∝ C))›
using list_invs unfolding twl_list_invs_def
by (auto simp: dest!: multi_member_split)
have H1: ‹C ∈# dom_m N ⟹
C' ∈# dom_m N ⟹
mset (N ∝ C) = add_mset L D ⟹
mset (N ∝ C') = add_mset (- L) D' ⟹
D ⊆# D' ⟹
∀C∈#dom_m N. ¬ tautology (mset (N ∝ C)) ⟹ tautology (D + D') ⟹ False› for C C' L D N D'
by (metis mset_subset_eqD tautology_add_mset tautology_minus tautology_union)
from assms tauto show ?thesis
apply -
supply [simp] = convert_lits_l_update_sel2
apply (induction rule: cdcl_twl_subresolution_l.induct)
subgoal for C N C' L D D' M E NE UE NEk UEk NS US N0 U0 Q
using H1[of C N C' L D D']
apply (auto simp: twl_st_l_def)
apply (rule_tac x = x in exI)
apply auto
apply (rule twl_subresolution_II_nonunit_simps[where
C' = ‹(TWL_Clause (mset (watched_l (N ∝ C'))) (mset (unwatched_l (N ∝ C'))))› and
C = ‹(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C))))›])
apply (auto simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
)
done
subgoal for C N C' L D D' M K NE UE NS US N0 U0 Q
using H1[of C N C' L D D']
apply (auto simp: twl_st_l_def)
apply (rule_tac x = ‹Propagated K {#K#} # x› in exI)
apply (auto simp: convert_lit.simps convert_lits_l_drop convert_lits_l_add_mset)
apply (rule twl_subresolution_II_unit_simps[where
C' = ‹(TWL_Clause (mset (watched_l (N ∝ C'))) (mset (unwatched_l (N ∝ C'))))› and
C = ‹(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C))))›])
apply (auto simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev; fail
)+
done
subgoal for C N C' L D D' M E NE UE NS US N0 U0 Q
apply (auto simp: twl_st_l_def)
apply (rule_tac x = ‹x› in exI)
apply (auto simp: convert_lit.simps convert_lits_l_drop convert_lits_l_add_mset
intro!: twl_subresolution_LL_nonunit_simps[where
C' = ‹(TWL_Clause (mset (watched_l (N ∝ C'))) (mset (unwatched_l (N ∝ C'))))› and
C = ‹(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C))))›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev; fail
)+
done
subgoal for C N C' L D D' M K NE UE NS US N0 U0 Q
using H1[of C N C' L D D']
apply (auto simp: twl_st_l_def)
apply (rule_tac x = ‹Propagated K {#K#} # x› in exI)
apply (auto simp: convert_lit.simps convert_lits_l_drop convert_lits_l_add_mset
intro!: twl_subresolution_LL_unit_simps[where
C' = ‹(TWL_Clause (mset (watched_l (N ∝ C'))) (mset (unwatched_l (N ∝ C'))))› and
C = ‹(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C))))›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
)
done
subgoal for C N C' L D D' M E NE UE NS US N0 U0 Q
using H1[of C N C' L D D']
apply (auto simp: twl_st_l_def)
apply (rule_tac x = ‹get_trail S'› in exI)
apply (auto simp: convert_lit.simps convert_lits_l_drop convert_lits_l_add_mset
intro!: twl_subresolution_LI_nonunit_simps[where
C' = ‹(TWL_Clause (mset (watched_l (N ∝ C'))) (mset (unwatched_l (N ∝ C'))))› and
C = ‹(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C))))›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev; fail
)+
done
subgoal for C N C' L D D' M K NE UE NS US N0 U0 Q
using H1[of C N C' L D D']
apply (auto simp: twl_st_l_def)
apply (rule_tac x = ‹Propagated K {#K#} # x› in exI)
apply (auto simp: convert_lit.simps convert_lits_l_drop convert_lits_l_add_mset
intro!: twl_subresolution_LI_unit_simps[where
C' = ‹(TWL_Clause (mset (watched_l (N ∝ C'))) (mset (unwatched_l (N ∝ C'))))› and
C = ‹(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C))))›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
)
done
subgoal for C N C' L D D' M E NE UE NS US N0 U0 Q
using H1[of C N C' L D D']
apply (auto simp: twl_st_l_def)
apply (rule_tac x = ‹get_trail S'› in exI)
apply (auto simp: convert_lit.simps convert_lits_l_drop convert_lits_l_add_mset
intro!: twl_subresolution_IL_nonunit_simps[where
C' = ‹(TWL_Clause (mset (watched_l (N ∝ C'))) (mset (unwatched_l (N ∝ C'))))› and
C = ‹(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C))))›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev; fail
)+
done
subgoal for C N C' L D D' M K NE UE NS US N0 U0 Q
using H1[of C N C' L D D']
apply (auto simp: twl_st_l_def)
apply (rule_tac x = ‹Propagated K {#K#} # x› in exI)
apply (auto simp: convert_lit.simps convert_lits_l_drop convert_lits_l_add_mset
intro!: twl_subresolution_IL_unit_simps[where
C' = ‹(TWL_Clause (mset (watched_l (N ∝ C'))) (mset (unwatched_l (N ∝ C'))))› and
C = ‹(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C))))›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
)
done
done
qed
inductive cdcl_twl_unitres_true_l :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
‹cdcl_twl_unitres_true_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmdrop C N, None, add_mset (mset (N ∝ C)) NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)›
if ‹L ∈# mset (N ∝ C)› ‹get_level M L = 0› ‹L ∈ lits_of_l M›
‹C ∈# dom_m N› ‹irred N C›
‹C ∉ set (get_all_mark_of_propagated M)› |
‹cdcl_twl_unitres_true_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmdrop C N, None, NE, add_mset (mset (N ∝ C)) UE, NEk, UEk, NS, US, N0, U0, {#}, Q)›
if ‹L ∈# mset (N ∝ C)› ‹get_level M L = 0› ‹L ∈ lits_of_l M›
‹C ∈# dom_m N› ‹¬irred N C›
‹C ∉ set (get_all_mark_of_propagated M)›
lemma cdcl_twl_unitres_true_intro1:
‹cdcl_twl_unitres_true S T›
if ‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (M, remove1_mset C N, U, None, add_mset (clause C) NE, UE, NS, US, N0, U0, {#}, Q)›
‹L ∈# clause C› ‹get_level M L = 0› ‹L ∈ lits_of_l M› ‹C ∈# N›
using cdcl_twl_unitres_true.intros(1)[of L C M ‹N - {#C#}› U] that
by auto
lemma cdcl_twl_unitres_true_intro2:
‹cdcl_twl_unitres_true S T›
if ‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (M, N, remove1_mset C U, None, NE, add_mset (clause C) UE, NS, US, N0, U0, {#}, Q)›
‹L ∈# clause C› ‹get_level M L = 0› ‹L ∈ lits_of_l M› ‹C ∈# U›
using cdcl_twl_unitres_true.intros(2)[of L C M N ‹U - {#C#}›] that
by auto
lemma cdcl_twl_unitres_true_l_cdcl_twl_unitres_true:
assumes ‹cdcl_twl_unitres_true_l S T› and
SS': ‹(S, S') ∈ twl_st_l None›
shows ‹∃T'. (T, T') ∈ twl_st_l None ∧ cdcl_twl_unitres_true S' T'›
using assms
apply (induction rule: cdcl_twl_unitres_true_l.induct)
subgoal for L N C M NE UE NS US Q
apply (auto simp: twl_st_l_def)
apply (rule_tac x=x in exI)
apply (auto simp: convert_lit.simps convert_lits_l_drop convert_lits_l_add_mset
intro!: cdcl_twl_unitres_true_intro1[where
C = ‹(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C))))›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
learned_clss_l_mapsto_upd_irrel convert_lits_l_drop
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
)
done
subgoal for L N C M NE UE NS US N0 U0 Q
apply (auto simp: twl_st_l_def)
apply (rule_tac x=x in exI)
apply (auto simp: convert_lit.simps convert_lits_l_drop convert_lits_l_add_mset
intro!: cdcl_twl_unitres_true_intro2[where
C = ‹(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C))))›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
learned_clss_l_mapsto_upd_irrel convert_lits_l_drop
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev
)
done
done
lemma cdcl_twl_subresolution_l_list_invs:
‹cdcl_twl_subresolution_l S T ⟹ twl_list_invs S ⟹ twl_list_invs T›
using distinct_mset_dom[of ‹get_clauses_l S›] apply -
by (induction rule: cdcl_twl_subresolution_l.induct)
(auto simp: twl_list_invs_def cdcl⇩W_restart_mset.in_get_all_mark_of_propagated_in_trail
ran_m_mapsto_upd ran_m_def add_mset_eq_add_mset tautology_add_mset
dest: in_diffD dest!: multi_member_split)
lemma cdcl_twl_unitres_True_l_list_invs:
‹cdcl_twl_unitres_true_l S T ⟹ twl_list_invs S ⟹ twl_list_invs T›
by (induction rule: cdcl_twl_unitres_true_l.induct)
(auto simp: twl_list_invs_def cdcl⇩W_restart_mset.in_get_all_mark_of_propagated_in_trail
dest: in_diffD)
inductive cdcl_twl_unitres_l :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
‹cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmupd D (E, irred N D) N, None, NE, UE, NEk, UEk, add_mset (mset (N ∝ D)) NS, US, N0, U0, {#}, Q)›
if
‹D ∈# dom_m N›
‹count_decided M = 0› and
‹mset (N ∝ D) = C +C'›
‹(mset `# init_clss_lf N + NE + NEk + NS + N0) ⊨psm mset_set (CNot C')›
‹¬tautology C› ‹distinct_mset C›
‹struct_wf_twl_cls (twl_clause_of E)›
‹Multiset.Ball (mset E) (undefined_lit M)›
‹mset E = C›
‹D ∉ set (get_all_mark_of_propagated M)› ‹irred N D› |
‹cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(Propagated K 0 # M, fmdrop D N, None, NE, UE, add_mset {#K#} NEk, UEk, add_mset (mset (N ∝ D)) NS, US, N0, U0, {#}, add_mset (-K) Q)›
if
‹D ∈# dom_m N›
‹count_decided M = 0› and
‹mset (N ∝ D) = {#K#} +C'›
‹(mset `# init_clss_lf N + NE + NEk + NS + N0) ⊨psm mset_set (CNot C')›
‹D ∉ set (get_all_mark_of_propagated M)› ‹irred N D›
‹undefined_lit M K› |
‹cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmupd D (E, irred N D) N, None, NE, UE, NEk, UEk, NS, add_mset (mset (N ∝ D)) US, N0, U0, {#}, Q)›
if
‹D ∈# dom_m N›
‹count_decided M = 0› and
‹mset (N ∝ D) = C +C'›
‹(mset `# init_clss_lf N + NE + NEk + NS + N0) ⊨psm mset_set (CNot C')›
‹¬tautology C› ‹distinct_mset C›
‹struct_wf_twl_cls (twl_clause_of E)›
‹Multiset.Ball (mset E) (undefined_lit M)›
‹mset E = C›
‹D ∉ set (get_all_mark_of_propagated M)› ‹¬irred N D›
‹atms_of (mset E) ⊆ atms_of_mm (mset `# init_clss_lf N) ∪ atms_of_mm NE ∪ atms_of_mm NEk ∪
atms_of_mm NS ∪ atms_of_mm N0› |
‹cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(Propagated K 0 # M, fmdrop D N, None, NE, UE, NEk, add_mset {#K#} UEk, NS, add_mset (mset (N ∝ D)) US, N0, U0, {#}, add_mset (-K) Q)›
if
‹D ∈# dom_m N›
‹count_decided M = 0› and
‹mset (N ∝ D) = {#K#} +C'›
‹(mset `# init_clss_lf N + NE + NEk + NS + N0) ⊨psm mset_set (CNot C')›
‹D ∉ set (get_all_mark_of_propagated M)› ‹¬irred N D›
‹undefined_lit M K›
‹atm_of K ∈ atms_of_mm (mset `# init_clss_lf N) ∪ atms_of_mm NE ∪ atms_of_mm NEk ∪
atms_of_mm NS ∪ atms_of_mm N0› |
‹cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmdrop D N, Some {#}, NE, UE, NEk, UEk, NS, add_mset (mset (N ∝ D)) US, N0, add_mset {#} U0, {#}, {#})›
if
‹D ∈# dom_m N›
‹(mset `# init_clss_lf N + NE + NEk + NS + N0) ⊨psm mset_set (CNot (mset (N ∝ D)))›
‹¬irred N D›
‹count_decided M = 0›
‹D ∉ set (get_all_mark_of_propagated M)› |
‹cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmdrop D N, Some {#}, NE, UE, NEk, UEk, add_mset (mset (N ∝ D)) NS, US, add_mset {#} N0, U0, {#}, {#})›
if
‹D ∈# dom_m N›
‹(mset `# init_clss_lf N + NE + NEk + NS + N0) ⊨psm mset_set (CNot (mset (N ∝ D)))›
‹irred N D›
‹count_decided M = 0›
‹D ∉ set (get_all_mark_of_propagated M)›
lemma cdcl_twl_unitres_I1:
‹cdcl_twl_unitres S T›
if ‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (M, add_mset E (remove1_mset D N), U, None, NE, UE, add_mset (clause D) NS, US, N0, U0, {#}, Q)›
‹count_decided M = 0› and
‹D ∈# N›
‹clause D = C+C'›
‹(clauses N + NE + NS + N0) ⊨psm mset_set (CNot C')›
‹¬tautology C› ‹distinct_mset C›
‹struct_wf_twl_cls E›
‹Multiset.Ball (clause E) (undefined_lit M)›
‹clause E = C›
using that cdcl_twl_unitres.intros(1)[of M D C C' ‹N - {#D#}› NE NS N0 E U UE US U0 Q]
by (auto dest!: multi_member_split)
lemma cdcl_twl_unitres_I2:
‹cdcl_twl_unitres S T›
if ‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (Propagated K {#K#} # M, (remove1_mset D N), U, None, add_mset {#K#} NE, UE, add_mset (clause D) NS, US, N0, U0, {#}, add_mset (-K) Q)›
‹count_decided M = 0› and
‹D ∈# N›
‹clause D = {#K#}+C'›
‹(clauses N + NE + NS + N0) ⊨psm mset_set (CNot C')›
‹undefined_lit M K›
using that cdcl_twl_unitres.intros(2)[of M D ‹{#K#}› C' ‹N - {#D#}› NE NS N0 K U UE US U0 Q]
by (auto dest!: multi_member_split)
lemma cdcl_twl_unitres_I3:
‹cdcl_twl_unitres S T›
if ‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (M, N, add_mset E (remove1_mset D U), None, NE, UE, NS, add_mset (clause D) US, N0, U0, {#}, Q)›
‹count_decided M = 0› and
‹D ∈# U›
‹clause D = C+C'›
‹(clauses N + NE + NS + N0) ⊨psm mset_set (CNot C')›
‹¬tautology C› ‹distinct_mset C›
‹struct_wf_twl_cls E›
‹Multiset.Ball (clause E) (undefined_lit M)›
‹clause E = C›
‹atms_of C ⊆ atms_of_ms (clause ` set_mset N) ∪ atms_of_mm NE ∪ atms_of_mm NS ∪ atms_of_mm N0›
using that cdcl_twl_unitres.intros(3)[of M D C C' N NE NS N0 E ‹U - {#D#}› UE US U0 Q]
by (auto dest!: multi_member_split)
lemma cdcl_twl_unitres_I4:
‹cdcl_twl_unitres S T›
if ‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (Propagated K {#K#} # M, N, remove1_mset D U, None, NE, add_mset {#K#} UE, NS, add_mset (clause D) US, N0, U0, {#}, add_mset (-K) Q)›
‹count_decided M = 0› and
‹D ∈# U›
‹clause D = {#K#}+C'›
‹(clauses N + NE + NS + N0) ⊨psm mset_set (CNot C')›
‹undefined_lit M K›
‹atm_of K ∈ atms_of_ms (clause ` set_mset N) ∪ atms_of_mm NE ∪ atms_of_mm NS ∪ atms_of_mm N0›
using that cdcl_twl_unitres.intros(4)[of M D ‹{#K#}› C' N NE NS N0 K ‹U - {#D#}› UE US U0 Q]
by (auto dest!: multi_member_split)
lemma cdcl_twl_unitres_I5:
‹cdcl_twl_unitres S T›
if ‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (M, N, remove1_mset D U, Some {#}, NE, UE, NS, add_mset (clause D) US, N0, add_mset {#} U0, {#}, {#})›
‹count_decided M = 0› and
‹D ∈# U›
‹(clauses N + NE + NS + N0) ⊨psm mset_set (CNot (clause D))›
using that cdcl_twl_unitres.intros(5)[of M N NE NS N0 D ‹remove1_mset D U› UE US U0 Q]
by (auto dest!: multi_member_split)
lemma cdcl_twl_unitres_I6:
‹cdcl_twl_unitres S T›
if ‹S = (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
‹T = (M, remove1_mset D N, U, Some {#}, NE, UE, add_mset (clause D) NS, US, add_mset {#} N0, U0, {#}, {#})›
‹count_decided M = 0› and
‹D ∈# N›
‹(clauses (add_mset D N) + NE + NS + N0) ⊨psm mset_set (CNot (clause D))›
using that cdcl_twl_unitres.intros(6)[of M D ‹remove1_mset D N› NE NS N0 U UE US U0 Q]
by (auto dest!: multi_member_split)
lemma cdcl_twl_unitres_l_cdcl_twl_unitres:
assumes ‹cdcl_twl_unitres_l S T› and
SS': ‹(S, S') ∈ twl_st_l None›
shows ‹∃T'. (T, T') ∈ twl_st_l None ∧ cdcl_twl_unitres S' T'›
using assms
apply (induction rule: cdcl_twl_unitres_l.induct)
subgoal for D N M C C' NE NEk NS N0 E UE UEk US U0 Q
apply (auto simp: twl_st_l_def)[]
apply (rule_tac x=x in exI)
apply (auto simp: twl_st_l_def
intro!: cdcl_twl_unitres_I1[where E= ‹twl_clause_of E› and D = ‹twl_clause_of (N ∝ D)›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev Un_assoc
learned_clss_l_mapsto_upd_irrel convert_lits_l_drop
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop convert_lits_l_update_sel2
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev)[]
done
subgoal for D N M K C' NE NS N0 UE US U0 Q
apply (auto simp: twl_st_l_def)[]
apply (rule_tac x= ‹Propagated K {#K#} # x› in exI)
apply (auto simp: twl_st_l_def
intro!: cdcl_twl_unitres_I2[where K=K and D = ‹twl_clause_of (N ∝ D)›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev Un_assoc
learned_clss_l_mapsto_upd_irrel convert_lits_l_drop
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop convert_lits_l_update_sel2
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel convert_lits_l_add_mset
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd convert_lit.intros(3)
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev)[]
done
subgoal for D N M C C' NE NEk NS N0 E UE UEk US U0 Q
apply (auto simp: twl_st_l_def)[]
apply (rule_tac x=x in exI)
apply (auto 5 3 simp: twl_st_l_def
intro!: cdcl_twl_unitres_I3[where E= ‹twl_clause_of E› and D = ‹twl_clause_of (N ∝ D)›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev Un_assoc
learned_clss_l_mapsto_upd_irrel convert_lits_l_drop
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop convert_lits_l_update_sel2
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd image_image
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev)[]
done
subgoal for D N M K C' NE NS N0 UE US U0 Q
apply (auto simp: twl_st_l_def; rule_tac x= ‹Propagated K {#K#} # x› in exI)
apply (auto simp: twl_st_l_def
intro!: cdcl_twl_unitres_I4[where K=K and D = ‹twl_clause_of (N ∝ D)›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev image_image
learned_clss_l_mapsto_upd_irrel convert_lits_l_drop Un_assoc
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop convert_lits_l_update_sel2
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel convert_lits_l_add_mset
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd convert_lit.intros(3)
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev)
done
subgoal for D N NE NS N0 M UE US U0 Q
by (auto simp: twl_st_l_def; rule_tac x= ‹x› in exI)
(auto simp: twl_st_l_def
intro!: cdcl_twl_unitres_I5[where D = ‹twl_clause_of (N ∝ D)›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev image_image
learned_clss_l_mapsto_upd_irrel convert_lits_l_drop Un_assoc
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop convert_lits_l_update_sel2
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel convert_lits_l_add_mset
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd convert_lit.intros(3)
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev)
subgoal for D N NE NS N0 M UE US U0 Q
by (auto simp: twl_st_l_def; rule_tac x= ‹x› in exI)
(auto simp: twl_st_l_def
intro!: cdcl_twl_unitres_I6[where D = ‹twl_clause_of (N ∝ D)›]
simp: init_clss_l_mapsto_upd image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel
mset_take_mset_drop_mset'
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev image_image
learned_clss_l_mapsto_upd_irrel convert_lits_l_drop Un_assoc
mset_take_mset_drop_mset' init_clss_l_mapsto_upd_irrelev
init_clss_l_fmdrop_irrelev learned_clss_l_l_fmdrop convert_lits_l_update_sel2
init_clss_l_mapsto_upd_irrel_notin init_clss_l_mapsto_upd_irrel convert_lits_l_add_mset
learned_clss_l_fmupd_if learned_clss_l_mapsto_upd convert_lit.intros(3)
init_clss_l_fmdrop learned_clss_l_l_fmdrop_irrelev)
done
definition simplify_clause_with_unit :: ‹nat ⇒ ('v, nat) ann_lits ⇒ 'v clauses_l ⇒ (bool × bool × 'v clauses_l) nres› where
‹simplify_clause_with_unit = (λC M N. do {
SPEC(λ(unc, b, N'). fmdrop C N = fmdrop C N' ∧ mset (N' ∝ C) ⊆# mset (N ∝ C) ∧ C ∈# dom_m N' ∧
(¬b ⟶ (∀L ∈# mset (N' ∝ C). undefined_lit M L)) ∧
(∀L ∈# mset (N ∝ C) - mset (N' ∝ C). defined_lit M L) ∧
(irred N C = irred N' C) ∧
(b ⟷ (∃L. L ∈# mset (N ∝ C) ∧ L ∈ lits_of_l M)) ∧
(unc ⟶ (N = N' ∧ ¬b)))
})›
definition simplify_clause_with_unit_st_pre :: ‹nat ⇒ 'v twl_st_l ⇒ bool› where
‹simplify_clause_with_unit_st_pre = (λC S.
C ∈# dom_m (get_clauses_l S) ∧ count_decided (get_trail_l S) = 0 ∧ get_conflict_l S = None ∧ clauses_to_update_l S = {#} ∧
twl_list_invs S ∧
set (get_all_mark_of_propagated (get_trail_l S)) ⊆ {0} ∧
(∃T. (S, T) ∈ twl_st_l None ∧ twl_struct_invs T ∧
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init ((state⇩W_of T)))
)›
definition simplify_clause_with_unit_st :: ‹nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹simplify_clause_with_unit_st = (λC (M, N⇩0, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q). do {
ASSERT(simplify_clause_with_unit_st_pre C (M, N⇩0, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q));
ASSERT (C ∈# dom_m N⇩0 ∧ count_decided M = 0 ∧ D = None ∧ WS = {#} ∧ no_dup M ∧ C ≠ 0);
let S = (M, N⇩0, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q);
if False
then RETURN (M, N⇩0, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)
else do {
let E = mset (N⇩0 ∝ C);
let irr = irred N⇩0 C;
(unc, b, N) ← simplify_clause_with_unit C M N⇩0;
ASSERT(fmdrop C N = fmdrop C N⇩0 ∧ irred N C = irred N⇩0 C ∧ mset (N ∝ C) ⊆# mset (N⇩0 ∝ C) ∧
C ∈# dom_m N);
if unc then do {
ASSERT (N = N⇩0);
RETURN (M, N⇩0, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)
}
else if b then do {
let T = (M, fmdrop C N, D, (if irr then add_mset E else id) NE, (if ¬irr then add_mset E else id) UE, NEk, UEk, NS, US, N0, U0, WS, Q);
ASSERT (set_mset (all_init_lits_of_l T) = set_mset (all_init_lits_of_l S));
ASSERT (set_mset (all_learned_lits_of_l T) = set_mset (all_learned_lits_of_l S));
RETURN T
}
else if size (N ∝ C) = 1
then do {
let L = ((N ∝ C) ! 0);
let T = (Propagated L 0 # M, fmdrop C N, D, NE, UE, (if irr then add_mset {#L#} else id) NEk,
(if ¬irr then add_mset {#L#} else id)UEk, (if irr then add_mset E else id) NS,
(if ¬irr then add_mset E else id)US, N0, U0, WS, add_mset (-L) Q);
ASSERT (set_mset (all_init_lits_of_l T) = set_mset (all_init_lits_of_l S));
ASSERT (set_mset (all_learned_lits_of_l T) = set_mset (all_learned_lits_of_l S));
ASSERT (undefined_lit M L ∧ L ∈# all_init_lits_of_l S);
RETURN T}
else if size (N ∝ C) = 0
then do {
let T = (M, fmdrop C N, Some {#}, NE, UE, NEk, UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id) US, (if irr then add_mset {#} else id) N0, (if ¬irr then add_mset {#} else id)U0, WS, {#});
ASSERT (set_mset (all_init_lits_of_l T) = set_mset (all_init_lits_of_l S));
ASSERT (set_mset (all_learned_lits_of_l T) = set_mset (all_learned_lits_of_l S));
RETURN T
}
else do {
let T = (M, N, D, NE, UE, NEk, UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id) US, N0, U0, WS, Q);
ASSERT (set_mset (all_init_lits_of_l T) = set_mset (all_init_lits_of_l S));
ASSERT (set_mset (all_learned_lits_of_l T) = set_mset (all_learned_lits_of_l S));
RETURN T
}
}
})›
lemma true_clss_clss_def_more_atms:
‹N ⊨ps N' ⟷ (∀I. total_over_m I (N ∪ N' ∪ N'') ⟶ consistent_interp I ⟶ I ⊨s N ⟶ I ⊨s N')›
(is ‹?A ⟷ ?B›)
proof (rule iffI)
assume ?A
then show ?B
by (simp add: true_clss_clss_def)
next
assume ?B
show ?A
unfolding true_clss_clss_def
proof (intro allI impI)
fix I
assume tot: ‹total_over_m I (N ∪ N')› and
cons: ‹consistent_interp I› and
IN: ‹I ⊨s N›
let ?I = ‹I ∪ Pos ` {A. A ∈ atms_of_ms N'' ∧ A ∉ atm_of ` I}›
have ‹total_over_m ?I (N ∪ N' ∪ N'')›
using tot atms_of_s_def by (fastforce simp: total_over_m_def total_over_set_def)
moreover have ‹consistent_interp ?I›
using cons unfolding consistent_interp_def
by (force simp: uminus_lit_swap)
moreover have ‹?I ⊨s N›
using IN by auto
ultimately have ‹?I ⊨s N'›
using ‹?B› by blast
then show ‹I ⊨s N'›
by (smt atms_of_ms_mono atms_of_s_def imageE literal.sel(1) mem_Collect_eq
notin_vars_union_true_clss_true_clss subsetD sup_ge2 tot total_over_m_alt_def)
qed
qed
lemma true_clss_clss_def_iff_negation_in_model:
‹A ⊨ps CNot C' ⟷ (∀L ∈# C'. A ⊨ps {{#-L#}})›
apply (rule iffI)
subgoal
by (simp add: true_clss_clss_in_imp_true_clss_cls)
subgoal
apply (subst (asm)true_clss_clss_def_more_atms[of _ _ ‹{C'}›])
apply (auto simp: true_clss_clss_def true_clss_def_iff_negation_in_model
dest!: multi_member_split)
done
done
lemma
fixes M :: ‹('v, nat) ann_lit list› and N NE UE NS US N0 U0 Q NEk UEk
defines ‹S ≡ (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)›
assumes
‹D ∈# dom_m N›
‹count_decided M = 0› and
‹D ∉ set (get_all_mark_of_propagated M)› and
ST: ‹(S, T) ∈ twl_st_l None› and
st_invs: ‹twl_struct_invs T› and
dec: ‹count_decided (get_trail_l S) = 0› and
false: ‹∀L ∈# C'. ¬undefined_lit (get_trail_l S) L›
‹∀L ∈# C'. L ∉ lits_of_l (get_trail_l S)› and
ent: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of T)›
shows cdcl_twl_unitres_l_intros2':
‹irred N D ⟹ undefined_lit M K ⟹ mset (N ∝ D) = {#K#} +C' ⟹
cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(Propagated K 0 # M, fmdrop D N, None, NE, UE, add_mset {#K#} NEk, UEk, add_mset (mset (N ∝ D)) NS, US, N0, U0, {#}, add_mset (-K) Q)›
(is ‹?A ⟹ _ ⟹ _ ⟹ ?B›) and
cdcl_twl_unitres_l_intros4':
‹¬irred N D ⟹ undefined_lit M K ⟹ mset (N ∝ D) = {#K#} +C' ⟹
cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(Propagated K 0 # M, fmdrop D N, None, NE, UE, NEk, add_mset {#K#} UEk, NS, add_mset (mset (N ∝ D)) US, N0, U0, {#}, add_mset (-K) Q)›
(is ‹?A' ⟹ _ ⟹ _ ⟹ ?B'›) and
cdcl_twl_unitres_false_entailed:
‹(mset `# init_clss_lf (get_clauses_l S) + get_unit_init_clauses_l S + get_subsumed_init_clauses_l S + get_init_clauses0_l S) ⊨psm mset_set (CNot C')› and
cdcl_twl_unitres_l_intros5':
‹¬irred N D ⟹ mset (N ∝ D) = C' ⟹
cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmdrop D N, Some {#}, NE, UE, NEk, UEk, NS, add_mset (mset (N ∝ D)) US, N0,
add_mset {#} U0, {#}, {#})›
(is ‹?E ⟹ _ ⟹ ?F›) and
cdcl_twl_unitres_l_intros6':
‹irred N D ⟹ mset (N ∝ D) = C' ⟹
cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, fmdrop D N, Some {#}, NE, UE, NEk, UEk, add_mset (mset (N ∝ D)) NS, US, add_mset {#} N0,
U0, {#}, {#})›
(is ‹?E' ⟹ _ ⟹ ?F'›) and
cdcl_twl_unitres_l_intros1':
‹irred N D ⟹ mset (N ∝ D) = mset C +C' ⟹ length C ≥ 2 ⟹ ¬tautology (mset (N ∝ D)) ⟹
∀L∈set C. undefined_lit M L ⟹ N' = fmupd D (C, irred N D) N ⟹
cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, N', None, NE, UE, NEk, UEk, add_mset (mset (N ∝ D)) NS, US, N0, U0, {#}, Q)›
(is ‹?G ⟹ _ ⟹ _ ⟹ _ ⟹ _ ⟹ _ ⟹ ?H›) and
cdcl_twl_unitres_l_intros3':
‹¬irred N D ⟹ mset (N ∝ D) = mset C +C' ⟹ length C ≥ 2 ⟹ ¬tautology (mset (N ∝ D)) ⟹
∀L∈set C. undefined_lit M L ⟹ N' = fmupd D (C, irred N D) N ⟹
cdcl_twl_unitres_l (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, Q)
(M, N', None, NE, UE, NEk, UEk, NS, add_mset (mset (N ∝ D)) US, N0, U0, {#}, Q)›
(is ‹?G' ⟹ _ ⟹ _ ⟹ _ ⟹ _ ⟹ _ ⟹ ?H'›)
proof -
have ‹all_decomposition_implies_m (cdcl⇩W_restart_mset.clauses ((state⇩W_of T)))
(get_all_ann_decomposition (trail ((state⇩W_of T))))› and
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of T)› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of T)› and
tauto: ‹∀s∈#learned_clss (state⇩W_of T). ¬ tautology s› and
nd: ‹no_dup (trail (state_of (pstate⇩W_of T)))›
using st_invs unfolding twl_struct_invs_def unfolding pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def state⇩W_of_def pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by fast+
moreover have H: ‹(λx. mset (fst x)) ` {a. a ∈# ran_m b ∧ snd a} ∪ (set_mset d ∪ set_mset d') ∪ f ∪ h ∪ U⊨ps
unmark_l aa ⟹
(a, aa) ∈ convert_lits_l b (d' + e) ⟹
(λx. mset (fst x)) ` {a. a ∈# ran_m b ∧ snd a} ∪ (set_mset d ∪ set_mset d') ∪ f ∪ h ⊨ps U ⟹
- L ∈ lits_of_l a ⟹
(λx. mset (fst x)) ` {a. a ∈# ran_m b ∧ snd a} ∪ (set_mset d ∪ set_mset d') ∪ f ∪ h ⊨p {#- L#}›
for aa :: ‹('v, 'v clause) ann_lits› and a :: ‹('v, nat) ann_lit list› and b d e f L U h d'
by (smt in_unmark_l_in_lits_of_l_iff list_of_l_convert_lits_l
true_clss_clss_in_imp_true_clss_cls true_clss_clss_left_right
true_clss_clss_union_and)
moreover have false: ‹∀L ∈# C'. -L ∈ lits_of_l (get_trail_l S)›
using false nd by (auto dest!: multi_member_split
simp: Decided_Propagated_in_iff_in_lits_of_l)
ultimately show ent2: ‹(mset `# init_clss_lf (get_clauses_l S) + get_unit_init_clauses_l S + get_subsumed_init_clauses_l S + get_init_clauses0_l S) ⊨psm mset_set (CNot C')›
using dec ST false ent
by (cases S; cases T)
(auto simp: twl_st_l_def all_decomposition_implies_def clauses_def
get_all_ann_decomposition_count_decided0 image_image mset_take_mset_drop_mset'
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def true_clss_clss_def_iff_negation_in_model
dest!: multi_member_split)
moreover {
have ‹N ∝ D ∈# init_clss_lf N ∨ N ∝ D ∈# learned_clss_lf N›
using assms(1,2) by (auto simp: ran_m_def)
then have ‹atms_of (mset (N ∝ D)) ⊆ atms_of_mm (mset `# init_clss_lf N) ∪ atms_of_mm NE ∪ atms_of_mm NEk ∪ atms_of_mm NS ∪ atms_of_mm N0›
using alien assms(1) ST
by (fastforce simp: twl_st_l_def clauses_def mset_take_mset_drop_mset' image_image
cdcl⇩W_restart_mset.no_strange_atm_def conj_disj_distribR Collect_disj_eq Collect_conv_if
dest!: multi_member_split[of _ ‹ran_m N›])
} note H = this
ultimately show ‹?A ⟹ ?B› ‹?A' ⟹ undefined_lit M K ⟹ ?B'›
if ‹mset (N ∝ D) = {#K#} + C'› ‹undefined_lit M K›
using assms cdcl_twl_unitres_l.intros(2)[of D N M K C' NE NEk NS N0 UE UEk US U0 Q]
cdcl_twl_unitres_l.intros(4)[of D N M K C' NE NEk NS N0 UE UEk US U0 Q] that
by (auto simp: Un_assoc)
show ?F if ‹?E› ‹mset (N ∝ D) = C'›
proof -
have ‹mset `# init_clss_lf N + NE + NEk + NS + N0 ⊨psm mset_set (CNot (mset (N ∝ D)))›
using ent2 that assms by (auto simp: Un_assoc)
then show ?thesis
using cdcl_twl_unitres_l.intros(5)[of D N NE NEk NS N0 M UE UEk US U0 Q] assms that
by (auto simp: Un_assoc)
qed
show ?F' if ‹?E'› ‹mset (N ∝ D) = C'›
proof -
have ‹mset `# init_clss_lf N + NE + NEk + NS + N0 ⊨psm mset_set (CNot (mset (N ∝ D)))›
using ent2 that assms by (auto simp: Un_assoc)
then show ?thesis
using cdcl_twl_unitres_l.intros(6)[of D N NE NEk NS N0 M UE UEk US U0 Q] assms that
by auto
qed
show ?H if ?G ‹mset (N ∝ D) = mset C +C'› ‹length C ≥ 2› ‹∀L∈set C. undefined_lit M L›
‹¬tautology (mset (N ∝ D))› ‹N' = fmupd D (C, irred N D) N›
proof -
have dist_C: ‹distinct_mset (mset (N ∝ D))›
using that dist ST assms(2)
by (auto simp: twl_st_l_def cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def ran_m_def
S_def mset_take_mset_drop_mset'
dest!: multi_member_split)
moreover have ‹struct_wf_twl_cls (twl_clause_of C)› ‹distinct C›
using that distinct_mset_mono[of ‹mset C› ‹mset (N ∝ D)›] dist_C
by (auto simp: twl_st_l_def cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
mset_take_mset_drop_mset')
moreover have ‹¬tautology (mset C)›
using not_tautology_mono[of ‹mset C› ‹mset C + C'›] that assms by auto
ultimately show ?thesis
using cdcl_twl_unitres_l.intros(1)[of D N M ‹mset C› C' NE NEk NS N0 C UE UEk US U0] assms that ent2
by (auto simp: Un_assoc)
qed
show ?H' if ?G' ‹mset (N ∝ D) = mset C +C'› ‹length C ≥ 2› ‹∀L∈set C. undefined_lit M L›
‹¬tautology (mset (N ∝ D))› ‹N' = fmupd D (C, irred N D) N›
proof -
have dist_C: ‹distinct_mset (mset (N ∝ D))›
using that dist ST assms(2)
by (auto simp: twl_st_l_def cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def ran_m_def
S_def mset_take_mset_drop_mset'
dest!: multi_member_split)
moreover have ‹struct_wf_twl_cls (twl_clause_of C)› ‹distinct C›
using that distinct_mset_mono[of ‹mset C› ‹mset (N ∝ D)›] dist_C
by (auto simp: twl_st_l_def cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
mset_take_mset_drop_mset')
moreover have ‹¬tautology (mset C)›
using not_tautology_mono[of ‹mset C› ‹mset C + C'›] that assms by auto
ultimately show ?thesis
using cdcl_twl_unitres_l.intros(3)[of D N M ‹mset C› C' NE NEk NS N0 C UE UEk US U0] assms that ent2 H
by (auto simp: Un_assoc)
qed
qed
lemma fmdrop_eq_update_eq: ‹fmdrop C aa = fmdrop C bh ⟹ C ∈# dom_m bh ⟹
bh = fmupd C (bh ∝ C, irred bh C) aa›
apply (subst (asm) fmlookup_inject[symmetric])
apply (subst fmlookup_inject[symmetric])
apply (intro ext)
apply auto[]
by (metis fmlookup_drop)
lemma fmdrop_eq_update_eq2: ‹fmdrop C aa = fmdrop C bh ⟹ C ∈# dom_m bh ⟹ b = irred bh C ⟹
bh = fmupd C (bh ∝ C, b) aa›
using fmdrop_eq_update_eq by fast
lemma twl_st_l_struct_invs_distinct:
assumes
ST: ‹(S, T) ∈ twl_st_l b› and
C: ‹C ∈# dom_m (get_clauses_l S)› and
invs: ‹twl_struct_invs T›
shows ‹distinct (get_clauses_l S ∝ C)›
proof -
have ‹(∀C ∈# get_clauses T. struct_wf_twl_cls C)›
using invs unfolding twl_struct_invs_def by (cases T) (auto simp: twl_st_inv.simps)
moreover have ‹twl_clause_of (get_clauses_l S ∝ C) ∈# (get_clauses T)›
using ST C by (cases S; cases T) (auto simp: twl_st_l_def)
ultimately show ?thesis
by (auto dest!: multi_member_split simp: mset_take_mset_drop_mset')
qed
lemma list_length_2_isabelle_come_on:
‹length C ≠ Suc 0 ⟹ C ≠ [] ⟹ length C ≥ 2›
by (cases C; cases ‹tl C›) auto
lemma in_all_lits_of_mm_init_clss_l_single_out:
‹xa ∈# all_lits_of_m (mset (aa ∝ C)) ⟹
C ∈# dom_m aa ⟹ irred aa C ⟹ xa ∈# all_lits_of_mm {#mset (fst x). x ∈# init_clss_l aa#}› and
in_all_lits_of_mm_learned_clss_l_single_out:
‹xa ∈# all_lits_of_m (mset (aa ∝ C)) ⟹
C ∈# dom_m aa ⟹ ¬irred aa C ⟹ xa ∈# all_lits_of_mm {#mset (fst x). x ∈# learned_clss_l aa#}›
by (auto simp: ran_m_def all_lits_of_mm_add_mset dest!: multi_member_split)
lemma pget_all_learned_clss_get_all_learned_clss_l:
‹(S, x) ∈ twl_st_l b ⟹
pget_all_learned_clss (pstate⇩W_of x) = get_all_learned_clss_l S›
by (cases x; cases S)
(auto simp: get_learned_clss_l_def twl_st_l_def mset_take_mset_drop_mset')
lemma pget_all_init_clss_get_all_init_clss_l:
‹(S, x) ∈ twl_st_l b ⟹
pget_all_init_clss (pstate⇩W_of x) = get_all_init_clss_l S›
by (cases x; cases S)
(auto simp: get_init_clss_l_def twl_st_l_def mset_take_mset_drop_mset')
lemma simplify_clause_with_unit_st_spec:
assumes ‹simplify_clause_with_unit_st_pre C S›
shows ‹simplify_clause_with_unit_st C S ≤ ⇓Id (SPEC(λT.
(S = T ∨ cdcl_twl_unitres_l S T ∨ cdcl_twl_unitres_true_l S T) ∧
(set (get_all_mark_of_propagated (get_trail_l T)) ⊆
set (get_all_mark_of_propagated (get_trail_l S)) ∪ {0}) ∧
(dom_m (get_clauses_l T) = dom_m (get_clauses_l S) ∨
dom_m (get_clauses_l T) = remove1_mset C (dom_m (get_clauses_l S))) ∧
(∀C' ∈# dom_m (get_clauses_l T). C ≠ C' ⟶ fmlookup (get_clauses_l S) C' = fmlookup (get_clauses_l T) C') ∧
(C ∈# dom_m (get_clauses_l T) ⟶ (∀L∈set (get_clauses_l T ∝ C). undefined_lit (get_trail_l T) L))))›
proof -
obtain T where
C: ‹C ∈# dom_m (get_clauses_l S)› ‹count_decided (get_trail_l S) = 0› and
confl: ‹get_conflict_l S = None› and
clss: ‹clauses_to_update_l S = {#}› and
ST: ‹(S, T) ∈ twl_st_l None› and
st_invs: ‹twl_struct_invs T› and
list_invs: ‹twl_list_invs S› and
ent: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init ((state⇩W_of T))› and
annot: ‹set (get_all_mark_of_propagated (get_trail_l S)) ⊆ {0}›
using assms unfolding simplify_clause_with_unit_st_pre_def
by auto
have C0: ‹C ≠ 0› ‹C ∉ set (get_all_mark_of_propagated (get_trail_l S))›
using list_invs C annot
by (auto simp: twl_list_invs_def)
have add_new: ‹L ∈# all_init_lits_of_l S ⟷ L ∈# all_init_lits_of_l S + all_learned_lits_of_l S›
if ‹simplify_clause_with_unit_st_pre C S› for L S
using that unfolding simplify_clause_with_unit_st_pre_def twl_struct_invs_def
pcdcl_all_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.no_strange_atm_def state⇩W_of_def[symmetric] apply -
by normalize_goal+
(auto simp add: all_init_lits_of_l_def all_learned_lits_of_l_def
in_all_lits_of_mm_ain_atms_of_iff pget_all_learned_clss_get_all_learned_clss_l
pget_all_init_clss_get_all_init_clss_l image_Un get_learned_clss_l_def)
have [dest]: ‹fmdrop C aa = fmdrop C bj ⟹
remove1_mset C (dom_m bj) = remove1_mset C (dom_m aa)› for C ab bj aa
by (metis dom_m_fmdrop)
have n_d:‹no_dup (get_trail_l S)›
using ST st_invs unfolding twl_struct_invs_def pcdcl_all_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
have in_lits:
‹C ∈# dom_m aa ∧ count_decided a = 0 ∧ ab = None ∧ ci = {#} ∧ no_dup a ∧ C ≠ 0⟹
case x of
(unc, b, N') ⇒
fmdrop C aa = fmdrop C N' ∧
mset (N' ∝ C) ⊆# mset (aa ∝ C) ∧
C ∈# dom_m N' ∧
(¬ b ⟶ (∀L∈#mset (N' ∝ C). undefined_lit a L)) ∧
Multiset.Ball (mset (aa ∝ C) - mset (N' ∝ C)) (defined_lit a) ∧
irred aa C = irred N' C ∧ b = (∃L. L ∈# mset (aa ∝ C) ∧ L ∈ lits_of_l a) ∧
(unc ⟶ (aa = N' ∧ ¬b)) ⟹
fmdrop C bj = fmdrop C aa ∧ irred bj C = irred aa C ∧ mset (bj ∝ C) ⊆# mset (aa ∝ C) ∧ C ∈# dom_m bj ⟹
x = (unc, bj') ⟹
bj' = (aj, bj) ⟹
¬unc ⟹ aj ⟹
set_mset
(all_init_lits_of_l
(a, fmdrop C bj, ab, (if irred aa C then add_mset (mset (aa ∝ C)) else id) ac,
(if ¬ irred aa C then add_mset (mset (aa ∝ C)) else id) ad, ae, af, ag, ah, ai, bi, ci, di)) =
set_mset (all_init_lits_of_l (a, aa, ab, ac, ad, ae, af, ag, ah, ai, bi, ci, di))
›
‹C ∈# dom_m aa ∧ count_decided a = 0 ∧ ab = None ∧ ci = {#} ∧ no_dup a ∧ C ≠ 0 ⟹
case x of
(unc, b, N') ⇒
fmdrop C aa = fmdrop C N' ∧
mset (N' ∝ C) ⊆# mset (aa ∝ C) ∧
C ∈# dom_m N' ∧
(¬ b ⟶ (∀L∈#mset (N' ∝ C). undefined_lit a L)) ∧
Multiset.Ball (mset (aa ∝ C) - mset (N' ∝ C)) (defined_lit a) ∧
irred aa C = irred N' C ∧ b = (∃L. L ∈# mset (aa ∝ C) ∧ L ∈ lits_of_l a) ∧
(unc ⟶ (aa = N' ∧ ¬b)) ⟹
fmdrop C bj = fmdrop C aa ∧ irred bj C = irred aa C ∧ mset (bj ∝ C) ⊆# mset (aa ∝ C) ∧ C ∈# dom_m bj ⟹
x = (unc, bj') ⟹
bj' = (aj, bj) ⟹
¬unc ⟹ aj ⟹
set_mset
(all_learned_lits_of_l
(a, fmdrop C bj, ab, (if irred aa C then add_mset (mset (aa ∝ C)) else id) ac,
(if ¬ irred aa C then add_mset (mset (aa ∝ C)) else id) ad, ae, af, ag, ah, ai, bi, ci, di)) =
set_mset (all_learned_lits_of_l (a, aa, ab, ac, ad, ae, af, ag, ah, ai, bi, ci, di)) ›
for a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi x aj bj unc bj' ci di
using assms distinct_mset_dom[of bj] distinct_mset_dom[of aa]
apply (auto simp: all_init_lits_of_l_def get_init_clss_l_def ran_m_def
all_lits_of_mm_add_mset all_lits_of_mm_union
all_learned_lits_of_l_def get_learned_clss_l_def
dest!: multi_member_split[of _ ‹dom_m _›]
cong: )
apply (smt (verit, best) image_mset_cong2)+
done
have in_lits_prop:
‹C ∈# dom_m aa ∧ count_decided a = 0 ∧ ab = None ∧ di = {#} ∧ no_dup a ∧ C ≠ 0 ⟹
case x of
(unc, b, N') ⇒
fmdrop C aa = fmdrop C N' ∧
mset (N' ∝ C) ⊆# mset (aa ∝ C) ∧
C ∈# dom_m N' ∧
(¬ b ⟶ (∀L∈#mset (N' ∝ C). undefined_lit a L)) ∧
Multiset.Ball (mset (aa ∝ C) - mset (N' ∝ C)) (defined_lit a) ∧
irred aa C = irred N' C ∧ b = (∃L. L ∈# mset (aa ∝ C) ∧ L ∈ lits_of_l a) ∧
(unc ⟶ (aa = N'∧ ¬b)) ⟹
x = (unc, bj') ⟹
bj' = (aj, bj) ⟹
¬unc ⟹ ¬aj ⟹
fmdrop C bj = fmdrop C aa ∧ irred bj C = irred aa C ∧ mset (bj ∝ C) ⊆# mset (aa ∝ C) ∧ C ∈# dom_m bj ⟹
length (bj ∝ C) = 1 ⟹
set_mset
(all_init_lits_of_l
(Propagated (bj ∝ C ! 0) 0 # a, fmdrop C bj, ab, ah, ai, (if irred aa C then add_mset {#bj ∝ C ! 0#} else id) ac,
(if ¬ irred aa C then add_mset {#bj ∝ C ! 0#} else id) ad, (if irred aa C then add_mset (mset (aa ∝ C)) else id) ae,
(if ¬ irred aa C then add_mset (mset (aa ∝ C)) else id) af, ag, ci, di, add_mset (- bj ∝ C ! 0) bi)) =
set_mset (all_init_lits_of_l (a, aa, ab, ah, ai, ac, ad, ae, af, ag, ci, di, bi))
›
‹C ∈# dom_m aa ∧ count_decided a = 0 ∧ ab = None ∧ di = {#} ∧ no_dup a ∧ C ≠ 0 ⟹
case x of
(unc, b, N') ⇒
fmdrop C aa = fmdrop C N' ∧
mset (N' ∝ C) ⊆# mset (aa ∝ C) ∧
C ∈# dom_m N' ∧
(¬ b ⟶ (∀L∈#mset (N' ∝ C). undefined_lit a L)) ∧
Multiset.Ball (mset (aa ∝ C) - mset (N' ∝ C)) (defined_lit a) ∧
irred aa C = irred N' C ∧ b = (∃L. L ∈# mset (aa ∝ C) ∧ L ∈ lits_of_l a) ∧
(unc ⟶ (aa = N'∧ ¬b)) ⟹
x = (unc, bj') ⟹
bj' = (aj, bj) ⟹
¬unc ⟹ ¬aj ⟹
fmdrop C bj = fmdrop C aa ∧ irred bj C = irred aa C ∧ mset (bj ∝ C) ⊆# mset (aa ∝ C) ∧ C ∈# dom_m bj ⟹
length (bj ∝ C) = 1 ⟹
set_mset
(all_learned_lits_of_l
(Propagated (bj ∝ C ! 0) 0 # a, fmdrop C bj, ab, ah, ai, (if irred aa C then add_mset {#bj ∝ C ! 0#} else id) ac,
(if ¬ irred aa C then add_mset {#bj ∝ C ! 0#} else id) ad, (if irred aa C then add_mset (mset (aa ∝ C)) else id) ae,
(if ¬ irred aa C then add_mset (mset (aa ∝ C)) else id) af, ag, ci, di, add_mset (- bj ∝ C ! 0) bi)) =
set_mset (all_learned_lits_of_l (a, aa, ab, ah, ai, ac, ad, ae, af, ag, ci, di, bi))
›
for a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi x aj bj bj' unc ci di
subgoal
using assms distinct_mset_dom[of bj] distinct_mset_dom[of aa]
image_mset_cong2[of ‹dom_m (fmdrop C aa)›
‹λx. the (fmlookup (fmdrop C aa) x)› ‹λx. the (fmlookup aa x)› ‹dom_m (fmdrop C aa)›,
simplified]
apply (cases ‹bj ∝ C›)
apply (auto simp: all_init_lits_of_l_def get_init_clss_l_def ran_m_def
all_lits_of_mm_add_mset all_lits_of_mm_union all_lits_of_m_add_mset
all_learned_lits_of_l_def get_learned_clss_l_def
dest!: multi_member_split[of _ ‹dom_m _›]
cong: )
apply (metis in_clause_in_all_lits_of_m set_mset_mset)
apply (metis all_lits_of_m_add_mset member_add_mset multi_member_split set_mset_mset)
apply (smt (verit, best) image_mset_cong2)+
done
subgoal
using assms distinct_mset_dom[of bj] distinct_mset_dom[of aa]
image_mset_cong2[of ‹dom_m (fmdrop C aa)›
‹λx. the (fmlookup (fmdrop C aa) x)› ‹λx. the (fmlookup aa x)› ‹dom_m (fmdrop C aa)›,
simplified]
apply (cases ‹bj ∝ C›)
apply (auto simp: all_init_lits_of_l_def get_init_clss_l_def ran_m_def
all_lits_of_mm_add_mset all_lits_of_mm_union all_lits_of_m_add_mset
all_learned_lits_of_l_def get_learned_clss_l_def
dest!: multi_member_split[of _ ‹dom_m _›]
cong: )
apply (smt (verit, best) image_mset_cong2)+
apply (metis in_clause_in_all_lits_of_m set_mset_mset)
apply (metis all_lits_of_m_add_mset member_add_mset multi_member_split set_mset_mset)
apply (smt (verit, best) image_mset_cong2)+
done
done
have in_lits2: ‹mset (bj ∝ C) ⊆# mset (aa ∝ C) ⟹
C ∈# dom_m bj ⟹ C ∈# dom_m aa ⟹ length (bj ∝ C) > 0 ⟹
irred bj C ⟹ irred aa C ⟹ bj ∝ C ! 0 ∈# all_lits_of_mm {#mset (fst x). x ∈# init_clss_l aa#}› ‹mset (bj ∝ C) ⊆# mset (aa ∝ C) ⟹
C ∈# dom_m bj ⟹ C ∈# dom_m aa ⟹ length (bj ∝ C) > 0 ⟹
irred bj C ⟹ irred aa C ⟹ -bj ∝ C ! 0 ∈# all_lits_of_mm {#mset (fst x). x ∈# init_clss_l aa#}›
‹mset (bj ∝ C) ⊆# mset (aa ∝ C) ⟹
C ∈# dom_m bj ⟹ C ∈# dom_m aa ⟹ length (bj ∝ C) > 0 ⟹
¬irred bj C ⟹ ¬irred aa C ⟹ bj ∝ C ! 0 ∈# all_lits_of_mm {#mset (fst x). x ∈# learned_clss_l aa#}› ‹mset (bj ∝ C) ⊆# mset (aa ∝ C) ⟹
C ∈# dom_m bj ⟹ C ∈# dom_m aa ⟹ length (bj ∝ C) > 0 ⟹
¬irred bj C ⟹ ¬irred aa C ⟹ -bj ∝ C ! 0 ∈# all_lits_of_mm {#mset (fst x). x ∈# learned_clss_l aa#}›
‹mset (bj ∝ C) ⊆# mset (aa ∝ C) ⟹
fmdrop C bj = fmdrop C aa ⟹
C ∈# dom_m bj ⟹ irred bj C ⟹ irred aa C ⟹
C ∈# dom_m aa ⟹
xa ∈# all_lits_of_mm {#mset (fst x). x ∈# init_clss_l bj#} ⟹ xa ∈# all_lits_of_mm {#mset (fst x). x ∈# init_clss_l aa#}
›
‹mset (bj ∝ C) ⊆# mset (aa ∝ C) ⟹
fmdrop C bj = fmdrop C aa ⟹
C ∈# dom_m bj ⟹ ¬irred bj C ⟹ ¬irred aa C ⟹
C ∈# dom_m aa ⟹
xa ∈# all_lits_of_mm {#mset (fst x). x ∈# learned_clss_l bj#} ⟹ xa ∈# all_lits_of_mm {#mset (fst x). x ∈# learned_clss_l aa#}
›
for bj C aa xa
apply (auto 5 3 dest!: multi_member_split[of _ ‹dom_m _›] simp: ran_m_def all_lits_of_mm_add_mset
in_all_lits_of_mm_uminus_iff dest: all_lits_of_m_mono)
apply ((metis (no_types, lifting) in_clause_in_all_lits_of_m length_greater_0_conv mset_subset_eq_exists_conv nth_mem_mset union_iff)+)[4]
apply (blast dest: all_lits_of_m_mono)
apply (metis (no_types, lifting) add_mset_remove_trivial distinct_mset_add_mset distinct_mset_dom dom_m_fmdrop fmlookup_drop image_mset_cong2)
apply (blast dest: all_lits_of_m_mono)
by (metis (no_types, lifting) add_mset_remove_trivial distinct_mset_add_mset distinct_mset_dom dom_m_fmdrop fmlookup_drop image_mset_cong2)
have tauto: ‹¬tautology (mset ((get_clauses_l S) ∝ C))›
using list_invs C
by (auto simp: twl_list_invs_def)
then show ?thesis
supply [[goals_limit=1]]
using assms
unfolding simplify_clause_with_unit_st_def simplify_clause_with_unit_def Let_def
apply refine_vcg
subgoal using assms by blast
subgoal using C by auto
subgoal using C by auto
subgoal using confl by auto
subgoal using clss by auto
subgoal using n_d by simp
subgoal using C list_invs by (auto simp: twl_list_invs_def)
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal
by (rule in_lits)
subgoal
by (rule in_lits)
subgoal for a b aa ba ab bb ac bc ad bd ae be af bf ag bg x ah bh
supply[[goals_limit=1]]
using count_decided_ge_get_level[of ‹get_trail_l S›] C0
by (auto simp: cdcl_twl_unitres_true_l.simps
intro!: exI[of _ C])
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto (metis dom_m_fmdrop fmlookup_drop in_dom_m_lookup_iff)+
subgoal
by (rule in_lits_prop)
subgoal
by (rule in_lits_prop)
subgoal by (auto simp: all_init_lits_of_l_def)
subgoal
by (subst add_new, subst (asm) eq_commute[of ‹set_mset (all_init_lits_of_l _)›],
subst (asm) eq_commute[of ‹set_mset (all_learned_lits_of_l _)›])
(auto simp: all_init_lits_of_l_def get_init_clss_l_def
all_learned_lits_of_l_def
all_lits_of_mm_add_mset all_lits_of_m_add_mset)
subgoal for a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi x _ _ _ _ _ _ aj bj
using ST st_invs C0 ent apply -
apply (rule disjI2, rule disjI1)
apply (auto simp: length_list_Suc_0
dest: in_diffD
intro!: cdcl_twl_unitres_l_intros2' cdcl_twl_unitres_l_intros4'
intro: cdcl_twl_unitres_l_intros2'[where C' = ‹mset (get_clauses_l S ∝ C) - mset (bj ∝ C)›
and T = T]
cdcl_twl_unitres_l_intros4'[where C' = ‹mset (get_clauses_l S ∝ C) - mset (bj ∝ C)›
and T = T])
done
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto (metis dom_m_fmdrop fmlookup_drop in_dom_m_lookup_iff)+
subgoal using assms apply (auto simp: all_init_lits_of_l_def
all_lits_of_mm_union init_clss_l_fmdrop_if image_mset_remove1_mset_if
get_init_clss_l_def all_lits_of_mm_add_mset all_lits_of_m_add_mset
dest: all_lits_of_mm_diffD in_lits
intro: in_all_lits_of_mm_init_clss_l_single_out)
by (metis all_lits_of_mm_add_mset diff_single_trivial insert_DiffM union_iff)
subgoal using assms apply (auto simp: all_learned_lits_of_l_def
all_lits_of_mm_union learned_clss_l_fmdrop_if image_mset_remove1_mset_if
get_learned_clss_l_def all_lits_of_mm_add_mset all_lits_of_m_add_mset in_lits
dest: all_lits_of_mm_diffD
intro: in_all_lits_of_mm_learned_clss_l_single_out)
by (metis all_lits_of_mm_add_mset diff_single_trivial insert_DiffM union_iff)
subgoal for a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi x _ _ _ _ _ _ aj bj
using count_decided_ge_get_level[of ‹get_trail_l S›] ST st_invs C0 ent
cdcl_twl_unitres_false_entailed[of C ‹get_clauses_l S› ‹get_trail_l S›
‹get_unkept_init_clauses_l S› ‹get_unkept_learned_clss_l S›
‹get_kept_init_clauses_l S› ‹get_kept_learned_clss_l S›
‹get_subsumed_init_clauses_l S› ‹get_subsumed_learned_clauses_l S›
‹get_init_clauses0_l S› ‹get_learned_clauses0_l S›
‹literals_to_update_l S› T
‹mset (get_clauses_l S ∝ C) - mset (bj ∝ C)›]
twl_st_l_struct_invs_distinct[of S T None C]
apply (auto simp: cdcl_twl_unitres_true_l.simps cdcl_twl_unitres_l.simps Un_assoc
dest: distinct_mset_mono[of ‹mset _› ‹mset _›, unfolded distinct_mset_mset_distinct]
intro!: exI[of _ C])
done
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto (metis dom_m_fmdrop fmlookup_drop in_dom_m_lookup_iff)+
subgoal using assms apply (auto simp: all_init_lits_of_l_def
all_lits_of_mm_union init_clss_l_fmdrop_if image_mset_remove1_mset_if
get_init_clss_l_def all_lits_of_mm_add_mset all_lits_of_m_add_mset
dest: all_lits_of_mm_diffD in_lits2
intro: in_all_lits_of_mm_init_clss_l_single_out)
apply (smt (z3) Watched_Literals_Clauses.ran_m_mapsto_upd all_lits_of_mm_add_mset filter_mset_add_mset fmupd_same image_mset_add_mset prod.collapse ran_m_lf_fmdrop union_iff)+
done
subgoal using assms apply (auto simp: all_init_lits_of_l_def
all_lits_of_mm_union init_clss_l_fmdrop_if image_mset_remove1_mset_if
get_init_clss_l_def all_lits_of_mm_add_mset all_lits_of_m_add_mset
get_learned_clss_l_def all_learned_lits_of_l_def
dest: all_lits_of_mm_diffD in_lits2
intro: in_all_lits_of_mm_init_clss_l_single_out)
apply (smt (z3) Watched_Literals_Clauses.ran_m_mapsto_upd all_lits_of_mm_add_mset filter_mset_add_mset fmupd_same image_mset_add_mset prod.collapse ran_m_lf_fmdrop union_iff)+
done
subgoal for a b aa ba ab bb ac bc ad bd ae be af bf ag bg ah bh ai bi x _ _ _ _ _ _ aj bj
using assms
by (auto simp: list_length_2_isabelle_come_on twl_list_invs_def simplify_clause_with_unit_st_pre_def
intro!: cdcl_twl_unitres_l_intros3' cdcl_twl_unitres_l_intros1'
dest: distinct_mset_mono[of ‹mset _› ‹mset _›, unfolded distinct_mset_mset_distinct]
intro!: exI[of _ C] fmdrop_eq_update_eq2)
subgoal using assms apply (auto simp: all_init_lits_of_l_def
all_lits_of_mm_union init_clss_l_fmdrop_if image_mset_remove1_mset_if
get_init_clss_l_def all_lits_of_mm_add_mset all_lits_of_m_add_mset
dest: all_lits_of_mm_diffD in_lits2
intro: in_all_lits_of_mm_init_clss_l_single_out)
done
subgoal using assms by auto
(metis dom_m_fmdrop insert_DiffM)+
subgoal using assms apply auto
apply (metis fmlookup_drop)+
done
subgoal using assms by auto
done
qed
text ‹
We implement forward subsumption (even if it is not a complete algorithm...). We initially tried
to implement a very limited version similar to Splatz, i.e., putting all clauses in an array
sorted by length and checking for sub-res in that array. This is more efficient in the sense that
we know that all previous clauses are smaller... unless you want to strengthen binary clauses too.
In this case list have to resorted.
After some time, we decided to implement forward subsumption directly. The implementation works in
three steps:
▪ the ‹one-step› version tries to sub-res the clause with a given set of indices. Typically, one
entry in the watch list.
▪ then the ‹try_to_forward_subsume› iterates over multiple of whatever. Typically, the iteration
goes over all watch lists from the literals in the clause (and their negation) to find strengthening
clauses.
▪ finally, the ‹all› version goes over all clauses sorted in a set of indices.
After much thinking, we decided to follow the version from CaDiCaL that ignores all clauses that
contain a fixed literal. At first we tried to simplify the clauses, but this means that down in the
real implementation, sorting clauses does not work (because the units are removed).
›
definition forward_subsumption_one_pre :: ‹nat ⇒ nat multiset ⇒ 'v twl_st_l ⇒ bool› where
‹forward_subsumption_one_pre = (λC xs S.
∃T. C ≠ 0 ∧
(S, T) ∈ twl_st_l None ∧
twl_struct_invs T ∧
twl_list_invs S ∧
clauses_to_update_l S = {#} ∧
get_conflict_l S = None ∧
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of T) ∧
count_decided (get_trail_l S) = 0 ∧
set (get_all_mark_of_propagated (get_trail_l S)) ⊆ {0} ∧
C ∈# dom_m (get_clauses_l S) ∧
(∀L ∈# mset (get_clauses_l S ∝ C). undefined_lit (get_trail_l S) L) ∧
length (get_clauses_l S ∝ C) > 2)›