Theory Watched_Literals_Watch_List_Reduce
theory Watched_Literals_Watch_List_Reduce
imports Watched_Literals_List_Simp Watched_Literals_List_Reduce Watched_Literals_Watch_List
Watched_Literals_Watch_List_Restart
begin
no_notation funcset (infixr "→" 60)
lemma GC_remap_all_init_atmsD:
‹GC_remap (N, x, m) (N', x', m') ⟹
all_init_atms N NE + all_init_atms m NE = all_init_atms N' NE + all_init_atms m' NE›
by (induction rule: GC_remap.induct[split_format(complete)])
(auto simp: all_init_atms_def all_init_lits_def init_clss_l_fmdrop_if
init_clss_l_fmupd_if image_mset_remove1_mset_if
simp del: all_init_atms_def[symmetric]
simp flip: image_mset_union all_lits_of_mm_add_mset all_lits_of_mm_union)
lemma rtranclp_GC_remap_all_init_atmsD:
‹GC_remap⇧*⇧* (N, x, m) (N', x', m') ⟹
all_init_atms N NE + all_init_atms m NE = all_init_atms N' NE + all_init_atms m' NE›
by (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
(auto dest: GC_remap_all_init_atmsD)
lemma rtranclp_GC_remap_all_init_atms:
‹GC_remap⇧*⇧* (x1a, Map.empty, fmempty) (fmempty, m, x1ad) ⟹
all_init_atms x1ad NE = all_init_atms x1a NE›
by (auto dest!: rtranclp_GC_remap_all_init_atmsD[of _ _ _ _ _ _ NE])
lemma GC_remap_all_init_lits:
‹GC_remap (N, m, new) (N', m', new') ⟹
all_init_lits N NE + all_init_lits new NE = all_init_lits N' NE + all_init_lits new' NE›
by (induction rule: GC_remap.induct[split_format(complete)])
(case_tac ‹irred N C› ; auto simp: all_init_lits_def init_clss_l_fmupd_if image_mset_remove1_mset_if
simp flip: all_lits_of_mm_union)
lemma rtranclp_GC_remap_all_init_lits:
‹GC_remap⇧*⇧* (N, m, new) (N', m', new') ⟹
all_init_lits N NE + all_init_lits new NE = all_init_lits N' NE + all_init_lits new' NE›
by (induction rule: rtranclp_induct[of r ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])
(auto dest: GC_remap_all_init_lits)
lemma subsumed_clauses_alt_def:
‹subsumed_clauses S = subsumed_init_clauses S + subsumed_learned_clauses S›
by (cases S) auto
definition drop_clause_add_move_init_wl :: ‹'v twl_st_wl ⇒ nat ⇒ 'v twl_st_wl› where
‹drop_clause_add_move_init_wl = (λ(M, N, D, NE0, UE, NEk, UEk, NS, US, N0, U0, Q, W) C.
(M, fmdrop C N, D, add_mset (mset (N ∝ C)) NE0, UE, NEk, UEk, NS, {#}, N0, U0, Q, W))›
definition drop_clause_wl :: ‹'v twl_st_wl ⇒ nat ⇒ 'v twl_st_wl› where
‹drop_clause_wl = (λ(M, N, D, NE0, UE, NS, US, N0, U0, Q, W) C.
(M, fmdrop C N, D, NE0, UE, NS, {#}, N0, U0, Q, W))›
lemma reduce_dom_clauses_fmdrop:
‹reduce_dom_clauses N0 N ⟹ reduce_dom_clauses N0 (fmdrop C N)›
using distinct_mset_dom[of N]
by (auto simp: reduce_dom_clauses_def distinct_mset_remove1_All)
lemma correct_watching_fmdrop:
assumes
irred: ‹¬ irred N C› and
C: ‹C ∈# dom_m N› and
‹correct_watching' (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› and
C2: ‹length (N ∝ C) ≠ 2› and
blit: ‹literals_are_ℒ⇩i⇩n' (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
shows ‹correct_watching' (M, fmdrop C N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W)› and
‹literals_are_ℒ⇩i⇩n' (M, fmdrop C N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W)›
proof -
let ?S = ‹(M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
have
Hdist: ‹⋀L i K b. L∈#all_init_lits_of_wl ?S ⟹
distinct_watched (W L)› and
H1: ‹⋀L i K b. L∈#all_init_lits_of_wl ?S ⟹
(i, K, b)∈#mset (W L) ⟹ i ∈# dom_m N ⟹ K ∈ set (N ∝ i) ∧ K ≠ L ∧
correctly_marked_as_binary N (i, K, b)› and
H1': ‹⋀L i K b. L∈#all_init_lits_of_wl ?S ⟹
(i, K, b)∈#mset (W L) ⟹ b ⟹ i ∈# dom_m N› and
H2: ‹⋀L. L∈# all_init_lits_of_wl ?S ⟹
{#i ∈# fst `# mset (W L). i ∈# dom_m N#} =
{#C ∈# dom_m (get_clauses_l (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#})).
L ∈ set (watched_l (get_clauses_l (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#}) ∝ C))#}›
using assms
unfolding correct_watching'.simps clause_to_update_def
by fast+
have 1: ‹{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (fmdrop C N ∝ Ca))#} =
{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (N ∝ Ca))#}› for L
apply (rule filter_mset_cong2)
using distinct_mset_dom[of N] C irred
by (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond dest: all_lits_of_mm_diffD
dest: multi_member_split)
have 2: ‹remove1_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#} =
removeAll_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#}› for L
apply (rule distinct_mset_remove1_All)
using distinct_mset_dom[of N]
by (auto intro: distinct_mset_filter)
have [simp]: ‹filter_mset (λi. i ≠ C ∧ i ∈# (dom_m N)) A =
removeAll_mset C (filter_mset (λi. i ∈# dom_m N) A)› for A
by (induction A)
(auto simp: distinct_mset_remove1_All distinct_mset_dom)
show ‹correct_watching' (M, fmdrop C N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W)›
unfolding correct_watching'.simps clause_to_update_def
apply (intro conjI impI ballI)
subgoal for L using Hdist[of L] distinct_mset_dom[of N]
H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred
H1'[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›]
apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
subgoal for L iK
using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred
H1'[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›]
apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
subgoal for L iK
using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred
H1'[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C2
apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
subgoal for L
using C irred apply -
unfolding get_clauses_l.simps
apply (subst 1)
by (auto 5 1 simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond 2 H2 dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
have [dest!]: ‹x ∈# all_learned_lits_of_wl ([], fmdrop C N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W) ⟹
x ∈# all_learned_lits_of_wl ([], N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› for x
using assms(1,2)
by (auto dest: all_lits_of_mm_diffD simp: all_learned_lits_of_wl_def all_lits_of_mm_union
image_mset_remove1_mset_if)
show ‹literals_are_ℒ⇩i⇩n' (M, fmdrop C N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W)›
using assms by (auto simp: blits_in_ℒ⇩i⇩n'_def image_mset_remove1_mset_if literals_are_ℒ⇩i⇩n'_def
all_init_lits_def all_lits_of_mm_union
dest: multi_member_split all_lits_of_mm_diffD)
qed
lemma correct_watching'_fmdrop:
assumes
irred: ‹¬ irred N C› and
C: ‹C ∈# dom_m N› and
‹correct_watching' (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› and
‹literals_are_ℒ⇩i⇩n' (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
shows ‹correct_watching'_nobin (M, fmdrop C N, D, NE, UE, NEk, UEk, NS, {#}, N0, U0, Q, W)›and
‹literals_are_ℒ⇩i⇩n' (M, fmdrop C N, D, NE, UE, NEk, UEk, NS, {#}, N0, U0, Q, W)›
proof -
let ?S = ‹(M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
let ?ℒ = ‹all_init_lits_of_wl ?S›
have
Hdist: ‹⋀L i K b. L∈#?ℒ ⟹
distinct_watched (W L)› and
H1: ‹⋀L i K b. L∈#?ℒ ⟹
(i, K, b)∈#mset (W L) ⟹ i ∈# dom_m N ⟹ K ∈ set (N ∝ i) ∧ K ≠ L ∧ correctly_marked_as_binary N (i, K, b)› and
H2: ‹⋀L. L∈#?ℒ ⟹
{#i ∈# fst `# mset (W L). i ∈# dom_m N#} =
{#C ∈# dom_m (get_clauses_l (M', N, D, NE, UE, NEk, UEk, NS, US,N0, U0, {#}, {#})).
L ∈ set (watched_l (get_clauses_l (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#}) ∝ C))#}›
using assms
unfolding correct_watching'.simps clause_to_update_def
by fast+
have 1: ‹{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (fmdrop C N ∝ Ca))#} =
{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (N ∝ Ca))#}› for L
apply (rule filter_mset_cong2)
using distinct_mset_dom[of N] C irred
by (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond dest: all_lits_of_mm_diffD
dest: multi_member_split)
have 2: ‹remove1_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#} =
removeAll_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#}› for L
apply (rule distinct_mset_remove1_All)
using distinct_mset_dom[of N]
by (auto intro: distinct_mset_filter)
have [simp]: ‹filter_mset (λi. i ≠ C ∧ i ∈# dom_m N) A =
removeAll_mset C (filter_mset (λi. i ∈# dom_m N) A)› for A
by (induction A)
(auto simp: distinct_mset_remove1_All distinct_mset_dom)
show ‹correct_watching'_nobin (M, fmdrop C N, D, NE, UE, NEk, UEk, NS, {#}, N0, U0, Q, W)›
unfolding correct_watching'_nobin.simps clause_to_update_def
apply (intro conjI impI ballI)
subgoal for L using Hdist[of L] distinct_mset_dom[of N]
H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred
apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
subgoal for L iK
using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred
apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
subgoal for L
using C irred apply -
unfolding get_clauses_l.simps
apply (subst 1)
by (auto 5 1 simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond 2 H2 dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
have [dest!]: ‹x ∈# all_learned_lits_of_wl ([], fmdrop C N, D, NE, UE, NEk, UEk, NS, {#}, N0, U0, Q, W) ⟹
x ∈# all_learned_lits_of_wl ([], N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› for x
using assms
by (auto dest: all_lits_of_mm_diffD simp: all_learned_lits_of_wl_def
all_lits_of_mm_union image_mset_remove1_mset_if)
show ‹literals_are_ℒ⇩i⇩n' (M, fmdrop C N, D, NE, UE, NEk, UEk, NS, {#}, N0, U0, Q, W)›
using assms by (auto simp: blits_in_ℒ⇩i⇩n'_def image_mset_remove1_mset_if literals_are_ℒ⇩i⇩n'_def
all_init_lits_def all_lits_of_mm_union
dest: multi_member_split all_lits_of_mm_diffD)
qed
lemma all_init_lits_of_wl_fmdrop_addNEk[simp]:
‹irred N C ⟹ C ∈# dom_m N ⟹
(all_init_lits_of_wl (M, fmdrop C N, D, NE, UE, add_mset (mset (N ∝ C)) NEk, UEk, NS, US, N0, U0, Q, W)) =
(all_init_lits_of_wl (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))›
using distinct_mset_dom[of N]
by (auto simp: all_init_lits_of_wl_def ran_m_def dest!: multi_member_split
intro!: arg_cong[of _ _ all_lits_of_mm]
intro!: filter_mset_cong2 image_mset_cong2)
lemma correct_watching'_fmdrop':
assumes
irred: ‹irred N C› and
C: ‹C ∈# dom_m N› and
‹correct_watching'_nobin (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›and
‹literals_are_ℒ⇩i⇩n' (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
shows ‹correct_watching'_nobin (M, fmdrop C N, D, NE, UE, add_mset (mset (N ∝ C)) NEk, UEk, NS, {#}, N0, U0, Q, W)› and
‹literals_are_ℒ⇩i⇩n' (M, fmdrop C N, D, NE, UE, add_mset (mset (N ∝ C)) NEk, UEk, NS, {#}, N0, U0, Q, W)›
proof -
let ?S = ‹(M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
let ?ℒ = ‹all_init_lits_of_wl ?S›
have
Hdist: ‹⋀L. L∈#?ℒ ⟹
distinct_watched (W L)› and
H1: ‹⋀L i K b. L∈#?ℒ ⟹
(i, K, b)∈#mset (W L) ⟹ i ∈# dom_m N ⟹
K ∈ set (N ∝ i) ∧ K ≠ L ∧ correctly_marked_as_binary N (i, K, b)› and
H2: ‹⋀L. L∈#?ℒ ⟹
{#i ∈# fst `# mset (W L). i ∈# dom_m N#} =
{#C ∈# dom_m (get_clauses_l (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#})).
L ∈ set (watched_l (get_clauses_l (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#}) ∝ C))#}›
using assms
unfolding correct_watching'_nobin.simps clause_to_update_def
by blast+
have 1: ‹{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (fmdrop C N ∝ Ca))#} =
{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (N ∝ Ca))#}› for L
apply (rule filter_mset_cong2)
using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹snd iK›] C irred
by (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond dest: all_lits_of_mm_diffD
dest: multi_member_split)
have 2: ‹remove1_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#} =
removeAll_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#}› for L
apply (rule distinct_mset_remove1_All)
using distinct_mset_dom[of N]
by (auto intro: distinct_mset_filter)
have [simp]: ‹filter_mset (λi. i ≠ C ∧ i ∈# (dom_m N)) A =
removeAll_mset C (filter_mset (λi. i ∈# dom_m N) A)› for A
by (induction A)
(auto simp: distinct_mset_remove1_All distinct_mset_dom)
show ‹correct_watching'_nobin (M, fmdrop C N, D, NE, UE, add_mset (mset (N ∝ C)) NEk, UEk, NS, {#}, N0, U0, Q, W)›
unfolding correct_watching'_nobin.simps clause_to_update_def
apply (intro conjI impI ballI)
subgoal for L
using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred
Hdist[of L] irred C
apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
subgoal for L iK
using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred
apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
subgoal for L
using C irred apply -
unfolding get_clauses_l.simps
apply (subst 1)
by (auto 5 1 simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond 2 H2 dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
have [dest!]: ‹x ∈# all_learned_lits_of_wl ([], N, D, NE, UE, add_mset (mset (N ∝ C)) NEk, UEk, NS, {#}, N0, U0, Q, W) ⟹
x ∈# all_learned_lits_of_wl ([], N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› for x
using assms
by (auto dest: all_lits_of_mm_diffD simp: all_learned_lits_of_wl_def
all_lits_of_mm_union image_mset_remove1_mset_if)
have ‹(N ∝ C, irred N C) ∈# (init_clss_l N)›
using assms by (auto simp: ran_m_def dest!: multi_member_split) (metis prod.collapse)
from multi_member_split[OF this]
show ‹literals_are_ℒ⇩i⇩n' (M, fmdrop C N, D, NE, UE, add_mset (mset (N ∝ C)) NEk, UEk, NS, {#}, N0, U0, Q, W)›
using distinct_mset_dom[of N]
using assms by (auto simp: blits_in_ℒ⇩i⇩n'_def image_mset_remove1_mset_if all_lits_of_mm_add_mset
all_lits_of_mm_union literals_are_ℒ⇩i⇩n'_def all_init_lits_def
dest: multi_member_split all_lits_of_mm_diffD)
qed
lemma correct_watching'_fmdrop'':
assumes
irred: ‹¬irred N C› and
C: ‹C ∈# dom_m N› and
‹correct_watching'_nobin (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› and
‹literals_are_ℒ⇩i⇩n' (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
shows ‹correct_watching'_nobin (M, fmdrop C N, D, NE, UE, NEk, add_mset (mset (N ∝ C)) UEk, NS, {#}, N0, U0, Q, W)› and
‹literals_are_ℒ⇩i⇩n' (M, fmdrop C N, D, NE, UE, NEk, add_mset (mset (N ∝ C)) UEk, NS, {#}, N0, U0, Q, W)›
proof -
let ?S = ‹(M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)›
let ?ℒ = ‹all_init_lits_of_wl ?S›
have
Hdist: ‹⋀L. L∈#?ℒ ⟹
distinct_watched (W L)› and
H1: ‹⋀L i K b. L∈#?ℒ ⟹
(i, K, b)∈#mset (W L) ⟹ i ∈# dom_m N ⟹ K ∈ set (N ∝ i) ∧ K ≠ L ∧ correctly_marked_as_binary N (i, K, b)› and
H2: ‹⋀L. L∈#?ℒ ⟹
{#i ∈# fst `# mset (W L). i ∈# dom_m N#} =
{#C ∈# dom_m (get_clauses_l (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#})).
L ∈ set (watched_l (get_clauses_l (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#}) ∝ C))#}›
using assms
unfolding correct_watching'_nobin.simps clause_to_update_def
by blast+
have 1: ‹{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (fmdrop C N ∝ Ca))#} =
{#Ca ∈# dom_m (fmdrop C N). L ∈ set (watched_l (N ∝ Ca))#}› for L
apply (rule filter_mset_cong2)
using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹snd iK›] C irred
by (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond dest: all_lits_of_mm_diffD
dest: multi_member_split)
have 2: ‹remove1_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#} =
removeAll_mset C {#Ca ∈# dom_m N. L ∈ set (watched_l (N ∝ Ca))#}› for L
apply (rule distinct_mset_remove1_All)
using distinct_mset_dom[of N]
by (auto intro: distinct_mset_filter)
have [simp]: ‹filter_mset (λi. i ≠ C ∧ i ∈# dom_m N) A =
removeAll_mset C (filter_mset (λi. i ∈# dom_m N) A)› for A
by (induction A)
(auto simp: distinct_mset_remove1_All distinct_mset_dom)
show ‹correct_watching'_nobin (M, fmdrop C N, D, NE, UE, NEk, add_mset (mset (N ∝ C)) UEk, NS, {#}, N0, U0, Q, W)›
unfolding correct_watching'_nobin.simps clause_to_update_def
apply (intro conjI impI ballI)
subgoal for L
using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred
Hdist[of L] assms
apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
subgoal for L iK
using distinct_mset_dom[of N] H1[of L ‹fst iK› ‹fst (snd iK)› ‹snd (snd iK)›] C irred
apply (auto simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond correctly_marked_as_binary.simps dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
subgoal for L
using C irred apply -
unfolding get_clauses_l.simps
apply (subst 1)
by (auto 5 1 simp: image_mset_remove1_mset_if clause_to_update_def image_filter_replicate_mset
distinct_mset_remove1_All filter_mset_neq_cond 2 H2 dest: all_lits_of_mm_diffD
dest: multi_member_split)
done
have [dest!]: ‹x ∈# all_learned_lits_of_wl ([], fmdrop C N, D, NE, UE, NEk, add_mset (mset (N ∝ C)) UEk, NS, {#}, N0, U0, Q, W) ⟹
x ∈# all_learned_lits_of_wl ([], N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)› for x
using assms
by (auto dest: all_lits_of_mm_diffD simp: all_learned_lits_of_wl_def
all_lits_of_mm_union image_mset_remove1_mset_if)
have ‹(N ∝ C, irred N C) ∈# (learned_clss_l N)›
using assms by (auto simp: ran_m_def dest!: multi_member_split) (metis prod.collapse)
from multi_member_split[OF this]
show ‹literals_are_ℒ⇩i⇩n' (M, fmdrop C N, D, NE, UE, NEk, add_mset (mset (N ∝ C)) UEk, NS, {#}, N0, U0, Q, W)›
using distinct_mset_dom[of N]
using assms by (auto simp: blits_in_ℒ⇩i⇩n'_def image_mset_remove1_mset_if all_lits_of_mm_add_mset
all_lits_of_mm_union literals_are_ℒ⇩i⇩n'_def all_init_lits_def
dest: multi_member_split all_lits_of_mm_diffD)
qed
definition remove_one_annot_true_clause_one_imp_wl_pre where
‹remove_one_annot_true_clause_one_imp_wl_pre i T ⟷
(∃T'. (T, T') ∈ state_wl_l None ∧
remove_one_annot_true_clause_one_imp_pre i T' ∧
correct_watching'_nobin T ∧ literals_are_ℒ⇩i⇩n' T)›
definition replace_annot_wl_pre :: ‹'v literal ⇒ nat ⇒ 'v twl_st_wl ⇒ bool› where
‹replace_annot_wl_pre L C S ⟷
(∃S'. (S, S') ∈ state_wl_l None ∧ L ∈# all_init_lits_of_wl S ∧
replace_annot_l_pre L C S' ∧ literals_are_ℒ⇩i⇩n' S ∧
correct_watching'_nobin S)›
definition replace_annot_wl :: ‹'v literal ⇒ nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹replace_annot_wl L C =
(λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do {
ASSERT(replace_annot_wl_pre L C (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
RES {(M', N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W)| M'.
(∃M2 M1 C. M = M2 @ Propagated L C # M1 ∧ M' = M2 @ Propagated L 0 # M1)}
})›
lemma replace_annot_l_pre_replace_annot_wl_pre: ‹(((L, C), S), (L', C'), S')
∈ Id ×⇩f nat_rel ×⇩f
{(S, T).
(S, T) ∈ state_wl_l None ∧
correct_watching'_nobin S ∧ literals_are_ℒ⇩i⇩n' S} ⟹
replace_annot_l_pre L' C' S' ⟹
replace_annot_wl_pre L C S›
unfolding replace_annot_wl_pre_def replace_annot_l_pre_alt_def
unfolding replace_annot_l_pre_def[symmetric]
by (rule exI[of _ ‹S'›])
(auto simp add: ac_simps all_init_lits_of_wl_def)
lemma all_learned_lits_of_wl_all_init_lits_of_wlD[intro]:
‹set_mset (all_learned_lits_of_wl (M, ab, ac, ad, ae, NEk, UEk, af, ag, ah, ai, aj, ba))
⊆ set_mset (all_init_lits_of_wl (M, ab, ac, ad, {#}, NEk, {#}, af, {#}, ah, {#}, aj, ba)) ⟹
x ∈# all_learned_lits_of_wl (M, ab, ac, ad, {#}, NEk, UEk, af, {#}, ah, {#}, aj, ba) ⟹
x ∈# all_init_lits_of_wl (M, ab, ac, ad, {#}, NEk, {#}, af, {#}, ah, {#}, aj, ba)›
by (auto simp: all_learned_lits_of_wl_def all_init_lits_of_wl_def
all_lits_of_mm_union)
lemma replace_annot_wl_replace_annot_l:
‹(uncurry2 replace_annot_wl, uncurry2 replace_annot_l) ∈
Id ×⇩f nat_rel ×⇩f {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_nobin S ∧
literals_are_ℒ⇩i⇩n' S} →⇩f
⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_nobin S ∧
literals_are_ℒ⇩i⇩n' S}⟩nres_rel›
unfolding replace_annot_wl_def replace_annot_l_def uncurry_def
apply (intro frefI nres_relI)
apply clarify
apply refine_rcg
subgoal for a b aa ab ac ad ae af ba ag bb ah ai aj ak al am bc
by (force intro!: replace_annot_l_pre_replace_annot_wl_pre)
subgoal
by (rule RES_refine)
(force simp: state_wl_l_def literals_are_ℒ⇩i⇩n'_def ac_simps
all_lits_of_mm_union
correct_watching'_nobin.simps clause_to_update_def blits_in_ℒ⇩i⇩n'_def)
done
definition remove_and_add_cls_wl :: ‹nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹remove_and_add_cls_wl C =
(λ(M, N, D, NE, UE, NEk, UEk, NS, US, Q, W). do {
ASSERT(C ∈# dom_m N);
RETURN (M, fmdrop C N, D, NE, UE,
(if irred N C then add_mset (mset (N∝C)) else id) NEk,
(if ¬irred N C then add_mset (mset (N∝C)) else id) UEk, NS, {#}, Q, W)
})›
definition remove_one_annot_true_clause_one_imp_wl
:: ‹nat ⇒ 'v twl_st_wl ⇒ (nat × 'v twl_st_wl) nres›
where
‹remove_one_annot_true_clause_one_imp_wl = (λi S. do {
ASSERT(remove_one_annot_true_clause_one_imp_wl_pre i S);
ASSERT(is_proped (rev (get_trail_wl S) ! i));
(L, C) ← SPEC(λ(L, C). (rev (get_trail_wl S))!i = Propagated L C);
ASSERT(Propagated L C ∈ set (get_trail_wl S));
ASSERT(L ∈# all_init_lits_of_wl S);
if C = 0 then RETURN (i+1, S)
else do {
ASSERT(C ∈# dom_m (get_clauses_wl S));
S ← replace_annot_wl L C S;
S ← remove_and_add_cls_wl C S;
RETURN (i+1, S)
}
})›
lemma
assumes
x2_T: ‹(x2, T) ∈ state_wl_l b› and
struct: ‹twl_struct_invs U› and
T_U: ‹(T, U) ∈ twl_st_l b'›
shows
literals_are_ℒ⇩i⇩n_literals_are_ℒ⇩i⇩n_trail_init:
‹literals_are_in_ℒ⇩i⇩n_trail (all_init_atms_st x2) (get_trail_wl x2)›
(is ‹?trail›)
proof -
have
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of U)› and
confl: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of U)› and
M_lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of U)› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of U)›
using struct unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
pcdcl_all_struct_invs_def state⇩W_of_def
by fast+
show lits_trail: ‹literals_are_in_ℒ⇩i⇩n_trail (all_init_atms_st x2) (get_trail_wl x2)›
using alien x2_T T_U unfolding is_ℒ⇩a⇩l⇩l_def
literals_are_in_ℒ⇩i⇩n_trail_def cdcl⇩W_restart_mset.no_strange_atm_def
literals_are_ℒ⇩i⇩n_def all_init_lits_of_wl_def all_atms_def ℒ⇩a⇩l⇩l_all_init_atms
by
(auto 5 2
simp del: all_clss_l_ran_m union_filter_mset_complement
simp: twl_st twl_st_l twl_st_wl all_lits_of_mm_union lits_of_def
convert_lits_l_def image_image in_all_lits_of_mm_ain_atms_of_iff
get_unit_clauses_wl_alt_def ℒ⇩a⇩l⇩l_all_init_atms all_init_lits_def)
qed
lemma remove_one_annot_true_clause_one_imp_wl_remove_one_annot_true_clause_one_imp:
‹(uncurry remove_one_annot_true_clause_one_imp_wl, uncurry remove_one_annot_true_clause_one_imp)
∈ nat_rel ×⇩f {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_nobin S ∧ literals_are_ℒ⇩i⇩n' S} →⇩f
⟨nat_rel ×⇩f {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_nobin S ∧ literals_are_ℒ⇩i⇩n' S}⟩nres_rel›
(is ‹_ ∈ _ ×⇩f ?A →⇩f _›)
proof -
have [refine0]: ‹remove_and_add_cls_wl C S ≤⇓ ?A (remove_and_add_cls_l C' S')›
if ‹(C, C') ∈ Id› and ‹(S, S') ∈ ?A›
for C C' S S'
using that unfolding remove_and_add_cls_l_def remove_and_add_cls_wl_def
by refine_rcg
(auto intro!: RES_refine simp: state_wl_l_def
intro: correct_watching'_fmdrop correct_watching'_fmdrop''
correct_watching'_fmdrop')
show ?thesis
unfolding remove_one_annot_true_clause_one_imp_wl_def remove_one_annot_true_clause_one_imp_def
uncurry_def
apply (intro frefI nres_relI)
apply (refine_vcg replace_annot_wl_replace_annot_l[THEN fref_to_Down_curry2])
subgoal for x y unfolding remove_one_annot_true_clause_one_imp_wl_pre_def
by (rule exI[of _ ‹snd y›]) auto
subgoal by (simp add: state_wl_l_def)
subgoal by (simp add: state_wl_l_def)
subgoal by (simp add: state_wl_l_def)
subgoal for x y x1 x2 x1a x2a xa x' x1b x2b x1c x2c
unfolding remove_one_annot_true_clause_one_imp_wl_pre_def
remove_one_annot_true_clause_one_imp_pre_def
apply normalize_goal+
subgoal for U S T
using literals_are_ℒ⇩i⇩n_literals_are_ℒ⇩i⇩n_trail_init[of x2a U None T None]
by (auto simp add: literals_are_in_ℒ⇩i⇩n_trail_def lits_of_def image_image
ℒ⇩a⇩l⇩l_all_init_atms)
done
subgoal by simp
subgoal by (simp add: state_wl_l_def)
subgoal by (simp add: state_wl_l_def)
subgoal by (simp add: state_wl_l_def)
subgoal by simp
subgoal by (simp add: state_wl_l_def)
done
qed
definition remove_one_annot_true_clause_imp_wl_inv where
‹remove_one_annot_true_clause_imp_wl_inv S = (λ(i, T).
(∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧
correct_watching'_nobin S ∧ correct_watching'_nobin T ∧ literals_are_ℒ⇩i⇩n' S ∧
literals_are_ℒ⇩i⇩n' T ∧
remove_one_annot_true_clause_imp_inv S' (i, T')))›
definition remove_all_learned_subsumed_clauses_wl :: ‹'v twl_st_wl ⇒ ('v twl_st_wl) nres› where
‹remove_all_learned_subsumed_clauses_wl = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W).
RETURN (M, N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, Q, W))›
definition remove_one_annot_true_clause_imp_wl :: ‹'v twl_st_wl ⇒ ('v twl_st_wl) nres›
where
‹remove_one_annot_true_clause_imp_wl = (λS. do {
k ← SPEC(λk. (∃M1 M2 K. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_wl S)) ∧
count_decided M1 = 0 ∧ k = length M1)
∨ (count_decided (get_trail_wl S) = 0 ∧ k = length (get_trail_wl S)));
start ← SPEC (λi. i ≤ k ∧ (∀j < i. is_proped (rev (get_trail_wl S) ! j) ∧ mark_of (rev (get_trail_wl S) ! j) = 0));
(i, T) ← WHILE⇩T⇗remove_one_annot_true_clause_imp_wl_inv S⇖
(λ(i, S). i < k)
(λ(i, S). remove_one_annot_true_clause_one_imp_wl i S)
(start, S);
ASSERT (remove_one_annot_true_clause_imp_wl_inv S (i, T));
remove_all_learned_subsumed_clauses_wl T
})›
lemma remove_all_learned_subsumed_clauses_wl_remove_all_learned_subsumed_clauses:
‹(remove_all_learned_subsumed_clauses_wl, remove_all_learned_subsumed_clauses)
∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_nobin S ∧ literals_are_ℒ⇩i⇩n' S} →⇩f
⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_nobin S ∧ literals_are_ℒ⇩i⇩n' S}⟩nres_rel›
apply (auto intro!: frefI nres_relI
simp: remove_all_learned_subsumed_clauses_wl_def remove_all_learned_subsumed_clauses_def
literals_are_ℒ⇩i⇩n'_def correct_watching'_nobin.simps state_wl_l_def all_init_learned_lits_simps_Q
clause_to_update_def all_lits_of_mm_union blits_in_ℒ⇩i⇩n'_def)
by (meson basic_trans_rules(31) in_all_learned_lits_of_wl_addUS)
lemma remove_one_annot_true_clause_imp_wl_remove_one_annot_true_clause_imp:
‹(remove_one_annot_true_clause_imp_wl, remove_one_annot_true_clause_imp)
∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_nobin S ∧ literals_are_ℒ⇩i⇩n' S} →⇩f
⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_nobin S ∧ literals_are_ℒ⇩i⇩n' S}⟩nres_rel›
proof -
show ?thesis
unfolding remove_one_annot_true_clause_imp_wl_def remove_one_annot_true_clause_imp_def
uncurry_def
apply (intro frefI nres_relI)
apply (refine_vcg
WHILEIT_refine[where
R = ‹nat_rel ×⇩f {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching'_nobin S ∧
literals_are_ℒ⇩i⇩n' S}›]
remove_one_annot_true_clause_one_imp_wl_remove_one_annot_true_clause_one_imp[THEN
fref_to_Down_curry]
remove_all_learned_subsumed_clauses_wl_remove_all_learned_subsumed_clauses[THEN
fref_to_Down])
subgoal by force
subgoal by auto
subgoal by force
subgoal by force
subgoal by force
subgoal for x y k ka xa start start' x'
unfolding remove_one_annot_true_clause_imp_wl_inv_def
apply (subst case_prod_beta)
apply (rule_tac x=‹y› in exI)
apply (rule_tac x=‹snd x'› in exI)
apply (subst (asm)(23) surjective_pairing)
apply (subst (asm)(28) surjective_pairing)
unfolding prod_rel_iff by simp
subgoal by auto
subgoal by auto
subgoal for x y k ka xa start start' x'
unfolding remove_one_annot_true_clause_imp_wl_inv_def
apply (subst case_prod_beta)
apply (rule_tac x=‹y› in exI)
apply (rule_tac x=‹snd x'› in exI)
apply (subst (asm)(23) surjective_pairing)
apply (subst (asm)(28) surjective_pairing)
unfolding prod_rel_iff by simp
subgoal by auto
done
qed
definition collect_valid_indices_wl :: ‹'v twl_st_wl ⇒ nat list nres› where
‹collect_valid_indices_wl S = SPEC (λN. True)›
definition mark_to_delete_clauses_wl_inv
:: ‹'v twl_st_wl ⇒ nat list ⇒ nat × 'v twl_st_wl× nat list ⇒ bool›
where
‹mark_to_delete_clauses_wl_inv = (λS xs0 (i, T, xs).
∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧
mark_to_delete_clauses_l_inv S' xs0 (i, T', xs) ∧
correct_watching' S∧ literals_are_ℒ⇩i⇩n' S ∧ literals_are_ℒ⇩i⇩n' T)›
definition mark_to_delete_clauses_wl_pre :: ‹'v twl_st_wl ⇒ bool›
where
‹mark_to_delete_clauses_wl_pre S ⟷
(∃T. (S, T) ∈ state_wl_l None ∧ mark_to_delete_clauses_l_pre T ∧ literals_are_ℒ⇩i⇩n' S)›
definition mark_garbage_wl:: ‹nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹mark_garbage_wl = (λC (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q).
(M, fmdrop C N, D, NE, {#}, NEk, UEk, NS, {#}, N0, {#}, WS, Q))›
definition mark_to_delete_clauses_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹mark_to_delete_clauses_wl = (λS. do {
ASSERT(mark_to_delete_clauses_wl_pre S);
xs ← collect_valid_indices_wl S;
l ← SPEC(λ_:: nat. True);
(_, S, _) ← WHILE⇩T⇗mark_to_delete_clauses_wl_inv S xs⇖
(λ(i, S, xs). i < length xs)
(λ(i, T, xs). do {
if(xs!i ∉# dom_m (get_clauses_wl T)) then RETURN (i, T, delete_index_and_swap xs i)
else do {
ASSERT(0 < length (get_clauses_wl T∝(xs!i)));
ASSERT (get_clauses_wl T ∝ (xs ! i) ! 0 ∈# ℒ⇩a⇩l⇩l (all_init_atms_st T));
can_del ← SPEC(λb. b ⟶
(Propagated (get_clauses_wl T∝(xs!i)!0) (xs!i) ∉ set (get_trail_wl T)) ∧
¬irred (get_clauses_wl T) (xs!i) ∧ length (get_clauses_wl T ∝ (xs!i)) ≠ 2);
ASSERT(i < length xs);
if can_del
then
RETURN (i, mark_garbage_wl (xs!i) T, delete_index_and_swap xs i)
else
RETURN (i+1, T, xs)
}
})
(l, S, xs);
remove_all_learned_subsumed_clauses_wl S
})›
lemma mark_to_delete_clauses_wl_invD1:
assumes ‹mark_to_delete_clauses_wl_inv S xs (i, T, ys)› and
‹C ∈# dom_m (get_clauses_wl T)› and
‹0 < length (get_clauses_wl T ∝ C)›
shows
‹get_clauses_wl T ∝ C ! 0 ∈# ℒ⇩a⇩l⇩l (all_init_atms_st T)›
proof -
have ‹literals_are_ℒ⇩i⇩n' T›
using assms unfolding mark_to_delete_clauses_wl_inv_def by blast
then have ‹get_clauses_wl T ∝ C ! 0 ∈# all_init_lits_of_wl T›
using nth_in_all_lits_stI[of C T 0]
using assms(2,3) by (auto simp del: nth_in_all_lits_stI
simp: all_lits_st_init_learned literals_are_ℒ⇩i⇩n'_def)
then show ‹?thesis›
by (simp add: ℒ⇩a⇩l⇩l_all_init_atms)
qed
lemma remove_all_learned_subsumed_clauses_wl_remove_all_learned_subsumed_clauses2:
‹(remove_all_learned_subsumed_clauses_wl, remove_all_learned_subsumed_clauses)
∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧ literals_are_ℒ⇩i⇩n' S} →⇩f
⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧ literals_are_ℒ⇩i⇩n' S}⟩nres_rel›
by (auto intro!: frefI nres_relI
simp: remove_all_learned_subsumed_clauses_wl_def remove_all_learned_subsumed_clauses_def
literals_are_ℒ⇩i⇩n'_def correct_watching'.simps state_wl_l_def all_init_learned_lits_simps_Q
clause_to_update_def all_lits_of_mm_union blits_in_ℒ⇩i⇩n'_def)
(meson basic_trans_rules(31) in_all_learned_lits_of_wl_addUS)
lemma mark_to_delete_clauses_wl_mark_to_delete_clauses_l:
‹(mark_to_delete_clauses_wl, mark_to_delete_clauses_l)
∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧ literals_are_ℒ⇩i⇩n' S} →⇩f
⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧ literals_are_ℒ⇩i⇩n' S}⟩nres_rel›
proof -
have [refine0]: ‹collect_valid_indices_wl S ≤ ⇓ Id (collect_valid_indices S')›
if ‹(S, S') ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧
mark_to_delete_clauses_wl_pre S}›
for S S'
using that by (auto simp: collect_valid_indices_wl_def collect_valid_indices_def)
have if_inv: ‹(if A then RETURN P else RETURN Q) = RETURN (if A then P else Q)› for A P Q
by auto
have Ball_range[simp]: ‹(∀x∈range f ∪ range g. P x)⟷(∀x. P (f x) ∧ P (g x))› for P f g
by auto
show ?thesis
unfolding mark_to_delete_clauses_wl_def mark_to_delete_clauses_l_def
uncurry_def
apply (intro frefI nres_relI)
apply (refine_vcg
WHILEIT_refine[where
R = ‹{((i, S, xs), (j, T, ys)). i = j ∧ (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧
xs = ys ∧ literals_are_ℒ⇩i⇩n' S}›]
remove_one_annot_true_clause_one_imp_wl_remove_one_annot_true_clause_one_imp[THEN
fref_to_Down_curry]
remove_all_learned_subsumed_clauses_wl_remove_all_learned_subsumed_clauses2[THEN
fref_to_Down])
subgoal unfolding mark_to_delete_clauses_wl_pre_def by blast
subgoal by auto
subgoal by (auto simp: state_wl_l_def)
subgoal unfolding mark_to_delete_clauses_wl_inv_def by fast
subgoal by auto
subgoal by (force simp: state_wl_l_def)
subgoal by auto
subgoal by (force simp: state_wl_l_def)
subgoal for x y xs xsa l to_keep xa x' x1 x2 x1a x2a x1b x2b x1c x2c
by (auto simp: mark_to_delete_clauses_wl_invD1)
subgoal by (auto simp: state_wl_l_def can_delete_def)
subgoal by auto
subgoal by (force simp: state_wl_l_def)
subgoal
by (auto simp: state_wl_l_def correct_watching_fmdrop mark_garbage_wl_def
mark_garbage_l_def ac_simps
split: prod.splits)
subgoal by (auto simp: state_wl_l_def)
subgoal by (auto simp: state_wl_l_def)
done
qed
text ‹
This is only a specification and must be implemented. There are two ways to do so:
▸ clean the watch lists and then iterate over all clauses to rebuild them.
▸ iterate over the watch list and check whether the clause index is in the domain or not.
It is not clear which is faster (but option 1 requires only 1 memory access per clause instead of
two). The first option is implemented in SPASS-SAT. The latter version (partly) in cadical.
›
definition rewatch_clauses :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹rewatch_clauses = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W).
SPEC(λ(M', N', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q', W').
(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q) = (M', N', D', NE', UE', NEk', UEk', NS', US', N0', U0', Q') ∧
correct_watching (M, N', D, NE, UE, NEk', UEk', NS', US', N0', U0', Q, W')))›
definition mark_to_delete_clauses_wl_post where
‹mark_to_delete_clauses_wl_post S T ⟷
(∃S' T'. (S, S') ∈ state_wl_l None ∧ (T, T') ∈ state_wl_l None ∧ blits_in_ℒ⇩i⇩n S ∧
mark_to_delete_clauses_l_post S' T' ∧ correct_watching S ∧ blits_in_ℒ⇩i⇩n T ∧
correct_watching T ∧ get_unkept_learned_clss_wl T = {#} ∧
get_subsumed_learned_clauses_wl T = {#} ∧ get_learned_clauses0_wl T = {#})›
definition cdcl_twl_full_restart_wl_prog :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹cdcl_twl_full_restart_wl_prog S = do {
ASSERT(mark_to_delete_clauses_wl_pre S);
T ← mark_to_delete_clauses_wl S;
ASSERT(mark_to_delete_clauses_wl_post S T);
RETURN T
}›
lemma correct_watching_correct_watching: ‹correct_watching S ⟹ correct_watching' S›
by (cases S, auto simp only: correct_watching.simps correct_watching'.simps all_lits_st_init_learned
image_mset_union)
lemma (in -) [twl_st_l, simp]:
‹(Sa, x) ∈ twl_st_l None ⟹ get_all_learned_clss x = mset `# (get_learned_clss_l Sa) + get_unit_learned_clss_l Sa + get_subsumed_learned_clauses_l Sa + get_learned_clauses0_l Sa›
by (cases Sa; cases x) (auto simp: twl_st_l_def get_learned_clss_l_def mset_take_mset_drop_mset')
lemma cdcl_twl_full_restart_wl_prog_final_rel:
assumes
S_Sa: ‹(S, Sa) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧ blits_in_ℒ⇩i⇩n S}› and
pre_Sa: ‹mark_to_delete_clauses_l_pre Sa› and
pre_S: ‹mark_to_delete_clauses_wl_pre S› and
T_Ta: ‹(T, Ta) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧ literals_are_ℒ⇩i⇩n' S}› and
pre_l: ‹mark_to_delete_clauses_l_post Sa Ta›
shows ‹mark_to_delete_clauses_wl_post S T›
proof -
obtain x where
Sa_x: ‹(Sa, x) ∈ twl_st_l None› and
st: ‹remove_one_annot_true_clause⇧*⇧* Sa Ta› and
list_invs: ‹twl_list_invs Sa› and
struct: ‹twl_struct_invs x› and
confl: ‹get_conflict_l Sa = None› and
upd: ‹clauses_to_update_l Sa = {#}› and
empty:
‹get_unkept_learned_clss_l Ta = {#}›
‹get_subsumed_learned_clauses_l Ta = {#}›
‹get_learned_clauses0_l Ta = {#}›
using pre_l
unfolding mark_to_delete_clauses_l_post_def by blast
have corr_S: ‹correct_watching' S› and corr_T: ‹correct_watching' T› and
blits_S: ‹blits_in_ℒ⇩i⇩n S› and
blits_T: ‹literals_are_ℒ⇩i⇩n' T› and
S_Sa: ‹(S, Sa) ∈ state_wl_l None› and
T_Ta: ‹(T, Ta) ∈ state_wl_l None›
using S_Sa T_Ta by auto
have ‹set_mset (all_init_lits_of_wl S) = set_mset (all_lits_st S)›
using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(4)[OF S_Sa Sa_x struct] .
then have corr_S': ‹correct_watching S›
using corr_S
by (cases S; simp only: correct_watching'.simps correct_watching.simps)
obtain y where
‹cdcl_twl_restart_l⇧*⇧* Sa Ta› and
Ta_y: ‹(Ta, y) ∈ twl_st_l None› and
‹cdcl_twl_restart⇧*⇧* x y› and
struct: ‹twl_struct_invs y›
using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF st list_invs confl upd Sa_x
struct]
by blast
have eq: ‹set_mset (all_init_lits_of_wl T) = set_mset (all_lits_st T)›
using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(4)[OF T_Ta Ta_y struct] .
then have corr_T': ‹correct_watching T›
using corr_T
by (cases T; simp only: correct_watching'.simps correct_watching.simps)
have ‹blits_in_ℒ⇩i⇩n T›
using blits_T eq
unfolding blits_in_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n'_def all_lits_def literals_are_ℒ⇩i⇩n'_def
all_init_lits_def
by (auto dest: multi_member_split simp: ac_simps)
moreover have ‹get_unkept_learned_clss_wl T = {#} ∧
get_subsumed_learned_clauses_wl T = {#} ∧
get_learned_clauses0_wl T = {#}›
using empty T_Ta by simp
ultimately show ?thesis
using S_Sa T_Ta corr_T' corr_S' pre_l blits_S
unfolding mark_to_delete_clauses_wl_post_def
by blast
qed
lemma cdcl_twl_full_restart_wl_prog_final_rel':
assumes
S_Sa: ‹(S, Sa) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ⇩i⇩n S}› and
pre_Sa: ‹mark_to_delete_clauses_l_pre Sa› and
pre_S: ‹mark_to_delete_clauses_wl_pre S› and
T_Ta: ‹(T, Ta) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching' S ∧ literals_are_ℒ⇩i⇩n' S}› and
pre_l: ‹mark_to_delete_clauses_l_post Sa Ta›
shows ‹mark_to_delete_clauses_wl_post S T›
proof -
obtain x where
Sa_x: ‹(Sa, x) ∈ twl_st_l None› and
st: ‹remove_one_annot_true_clause⇧*⇧* Sa Ta› and
list_invs: ‹twl_list_invs Sa› and
struct: ‹twl_struct_invs x› and
confl: ‹get_conflict_l Sa = None› and
upd: ‹clauses_to_update_l Sa = {#}› and
empty:
‹get_unkept_learned_clss_l Ta = {#}›
‹get_subsumed_learned_clauses_l Ta = {#}›
‹get_learned_clauses0_l Ta = {#}›
using pre_l
unfolding mark_to_delete_clauses_l_post_def by blast
have corr_S: ‹correct_watching S› and corr_T: ‹correct_watching' T› and
blits_T: ‹literals_are_ℒ⇩i⇩n' T› and
blits_S: ‹blits_in_ℒ⇩i⇩n S› and
S_Sa: ‹(S, Sa) ∈ state_wl_l None› and
T_Ta: ‹(T, Ta) ∈ state_wl_l None›
using S_Sa T_Ta by auto
have corr_S: ‹correct_watching' S›
using correct_watching_correct_watching[OF corr_S] .
have ‹set_mset (all_init_lits_of_wl S) = set_mset (all_lits_st S)›
using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(4)[OF S_Sa Sa_x struct] .
then have corr_S': ‹correct_watching S›
using corr_S
by (cases S; simp only: correct_watching'.simps correct_watching.simps)
obtain y where
‹cdcl_twl_restart_l⇧*⇧* Sa Ta› and
Ta_y: ‹(Ta, y) ∈ twl_st_l None› and
‹cdcl_twl_restart⇧*⇧* x y› and
struct: ‹twl_struct_invs y›
using rtranclp_remove_one_annot_true_clause_cdcl_twl_restart_l2[OF st list_invs confl upd Sa_x
struct]
by blast
have eq: ‹set_mset (all_init_lits_of_wl T) = set_mset (all_lits_st T)›
using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(4)[OF T_Ta Ta_y struct] .
then have corr_T': ‹correct_watching T›
using corr_T
by (cases T; simp only: correct_watching'.simps correct_watching.simps)
have ‹blits_in_ℒ⇩i⇩n T›
using blits_T eq
unfolding blits_in_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n'_def all_lits_def literals_are_ℒ⇩i⇩n'_def
all_init_lits_def
by (auto dest: multi_member_split simp: ac_simps)
moreover have ‹get_unkept_learned_clss_wl T = {#} ∧
get_subsumed_learned_clauses_wl T = {#} ∧
get_learned_clauses0_wl T = {#}›
using empty T_Ta by simp
ultimately show ?thesis
using S_Sa T_Ta corr_T' corr_S' pre_l blits_S
unfolding mark_to_delete_clauses_wl_post_def apply -
apply (rule exI[of _ Sa])
apply (rule exI[of _ Ta])
by blast
qed
lemma mark_to_delete_clauses_l_pre_blits_in_ℒ⇩i⇩n':
assumes
S_Sa: ‹(S, Sa) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ⇩i⇩n S}› and
pre_Sa: ‹mark_to_delete_clauses_l_pre Sa›
shows ‹literals_are_ℒ⇩i⇩n' S›
proof -
obtain x where
Sa_x: ‹(Sa, x) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs Sa› and
struct: ‹twl_struct_invs x›
using pre_Sa
unfolding mark_to_delete_clauses_l_pre_def by blast
have corr_S: ‹correct_watching S› and
blits_S: ‹blits_in_ℒ⇩i⇩n S› and
S_Sa: ‹(S, Sa) ∈ state_wl_l None›
using S_Sa by auto
have corr_S: ‹correct_watching' S›
using correct_watching_correct_watching[OF corr_S] .
have eq: ‹set_mset (all_init_lits_of_wl S) = set_mset (all_lits_st S)›
using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(4)[OF S_Sa Sa_x struct] .
then have corr_S': ‹correct_watching S›
using corr_S
by (cases S; simp only: correct_watching'.simps correct_watching.simps)
have ‹literals_are_ℒ⇩i⇩n' S›
using blits_S eq
unfolding blits_in_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n'_def all_lits_def literals_are_ℒ⇩i⇩n'_def
all_init_lits_def all_lits_st_init_learned[of S] by auto
then show ?thesis
using S_Sa corr_S' blits_S
unfolding mark_to_delete_clauses_wl_post_def
by blast
qed
lemma cdcl_twl_full_restart_wl_prog_cdcl_full_twl_restart_l_prog:
‹(cdcl_twl_full_restart_wl_prog, cdcl_twl_full_restart_l_prog)
∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ⇩i⇩n S} →⇩f
⟨{(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ⇩i⇩n S}⟩nres_rel›
unfolding cdcl_twl_full_restart_wl_prog_def cdcl_twl_full_restart_l_prog_def
rewatch_clauses_def
apply (intro frefI nres_relI)
apply (refine_vcg
mark_to_delete_clauses_wl_mark_to_delete_clauses_l[THEN fref_to_Down]
remove_one_annot_true_clause_imp_wl_remove_one_annot_true_clause_imp[THEN fref_to_Down])
subgoal unfolding mark_to_delete_clauses_wl_pre_def
by (blast intro: correct_watching_correct_watching mark_to_delete_clauses_l_pre_blits_in_ℒ⇩i⇩n')
subgoal unfolding mark_to_delete_clauses_wl_pre_def by (blast intro: correct_watching_correct_watching)
subgoal
by (rule cdcl_twl_full_restart_wl_prog_final_rel')
subgoal by (auto simp: state_wl_l_def mark_to_delete_clauses_wl_post_def)
done