Theory Watched_Literals_List
theory Watched_Literals_List
imports More_Sepref.WB_More_Refinement_List Watched_Literals_Algorithm CDCL.DPLL_CDCL_W_Implementation
Watched_Literals_Clauses
begin
chapter ‹Second Refinement: Lists as Clause›
declare RETURN_as_SPEC_refine[refine2]
lemma mset_take_mset_drop_mset: ‹(λx. mset (take 2 x) + mset (drop 2 x)) = mset›
unfolding mset_append[symmetric] append_take_drop_id ..
lemma mset_take_mset_drop_mset': ‹mset (take 2 x) + mset (drop 2 x) = mset x›
unfolding mset_append[symmetric] append_take_drop_id ..
lemma uminus_lit_of_image_mset:
‹{#- lit_of x . x ∈# A#} = {#- lit_of x. x ∈# B#} ⟷
{#lit_of x . x ∈# A#} = {#lit_of x. x ∈# B#}›
for A :: ‹('a literal, 'a literal, 'b) annotated_lit multiset›
proof -
have 1: ‹(λx. -lit_of x) `# A = uminus `# lit_of `# A›
for A :: ‹('d::uminus, 'd, 'e) annotated_lit multiset›
by auto
show ?thesis
unfolding 1
by (rule inj_image_mset_eq_iff) (auto simp: inj_on_def)
qed
lemma twl_struct_invs_no_alien_in_trail:
assumes ‹twl_struct_invs S›
shows ‹L ∈ lits_of_l (get_trail S) ⟹ L ∈# all_lits_of_st S›
using assms by (cases S)
(auto simp: twl_struct_invs_def pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def all_lits_of_st_def
cdcl⇩W_restart_mset.no_strange_atm_def trail.simps
init_clss.simps learned_clss.simps
in_all_lits_of_mm_ain_atms_of_iff)
section ‹Types›
type_synonym 'v clauses_to_update_l = ‹nat multiset›
type_synonym 'v cconflict = ‹'v clause option›
type_synonym 'v cconflict_l = ‹'v literal list option›
type_synonym 'v twl_st_l =
‹('v, nat) ann_lits × 'v clauses_l × 'v cconflict × 'v clauses × 'v clauses × 'v clauses ×
'v clauses × 'v clauses × 'v clauses × 'v clauses × 'v clauses × 'v clauses_to_update_l × 'v lit_queue›
fun clauses_to_update_l :: ‹'v twl_st_l ⇒ 'v clauses_to_update_l› where
‹clauses_to_update_l (_, _, _, _, _, _, _, _, _,_, _, WS, _) = WS›
fun get_trail_l :: ‹'v twl_st_l ⇒ ('v, nat) ann_lit list› where
‹get_trail_l (M, _, _, _, _, _, _) = M›
fun set_clauses_to_update_l :: ‹'v clauses_to_update_l ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹set_clauses_to_update_l WS (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, _, Q) =
(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)›
fun literals_to_update_l :: ‹'v twl_st_l ⇒ 'v clause› where
‹literals_to_update_l (_, _, _, _, _, _, _, _, _, _, _, _,Q) = Q›
fun set_literals_to_update_l :: ‹'v clause ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹set_literals_to_update_l Q (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, _) =
(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)›
fun get_conflict_l :: ‹'v twl_st_l ⇒ 'v cconflict› where
‹get_conflict_l (_, _, D, _, _, _, _) = D›
fun get_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses_l› where
‹get_clauses_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = N›
fun get_unit_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unit_clauses_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = NE + NEk + UE + UEk›
fun get_kept_unit_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_kept_unit_clauses_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = NEk+ UEk›
fun get_unkept_unit_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unkept_unit_clauses_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = NE+ UE›
fun get_unit_init_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unit_init_clauses_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = NE + NEk›
fun get_unit_learned_clss_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unit_learned_clss_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = UE + UEk›
fun get_kept_init_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_kept_init_clauses_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = NEk›
fun get_kept_learned_clss_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_kept_learned_clss_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = UEk›
fun get_unkept_init_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unkept_init_clauses_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = NE›
fun get_unkept_learned_clss_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_unkept_learned_clss_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = UE›
fun get_init_clauses :: ‹'v twl_st ⇒ 'v twl_clss› where
‹get_init_clauses (M, N, U, D, NE, UE, NEk, UEk, NS, US, WS, Q) = N›
definition get_learned_clss_l :: ‹'v twl_st_l ⇒ 'v clause_l multiset› where
‹get_learned_clss_l S = learned_clss_lf (get_clauses_l S)›
definition get_init_clss_l :: ‹'v twl_st_l ⇒ 'v clause_l multiset› where
‹get_init_clss_l S = init_clss_lf (get_clauses_l S)›
fun get_subsumed_init_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_subsumed_init_clauses_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = NS›
fun get_subsumed_learned_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_subsumed_learned_clauses_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) = US›
fun get_subsumed_clauses_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_subsumed_clauses_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) = NS + US›
fun get_init_clauses0_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_init_clauses0_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) = N0›
fun get_learned_clauses0_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_learned_clauses0_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) = U0›
fun get_clauses0_l :: ‹'v twl_st_l ⇒ 'v clauses› where
‹get_clauses0_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) = N0 + U0›
abbreviation get_all_clss_l :: ‹'v twl_st_l ⇒ 'v clause multiset› where
‹get_all_clss_l S ≡
mset `# ran_mf (get_clauses_l S) + get_unit_clauses_l S + get_subsumed_clauses_l S + get_clauses0_l S›
abbreviation get_all_init_clss_l :: ‹'v twl_st_l ⇒ 'v clause multiset› where
‹get_all_init_clss_l S ≡ mset `# get_init_clss_l S + get_unit_init_clauses_l S +
get_subsumed_init_clauses_l S + get_init_clauses0_l S›
abbreviation get_all_learned_clss_l :: ‹'v twl_st_l ⇒ 'v clause multiset› where
‹get_all_learned_clss_l S ≡ mset `# get_learned_clss_l S + get_unit_learned_clss_l S +
get_subsumed_learned_clauses_l S + get_learned_clauses0_l S›
lemma state_decomp_to_state:
‹(case S of (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) ⇒ P M N U D NE UE NS US N0 U0 WS Q) =
P (get_trail S) (get_init_clauses S) (get_learned_clss S) (get_conflict S)
(unit_init_clauses S) (get_init_learned_clss S)
(subsumed_init_clauses S) (subsumed_learned_clauses S)
(get_init_clauses0 S) (get_learned_clauses0 S)
(clauses_to_update S)
(literals_to_update S)›
by (cases S) auto
lemma state_decomp_to_state_l:
‹(case S of (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) ⇒ P M N D NE UE NEk UEk NS US N0 U0 WS Q) =
P (get_trail_l S) (get_clauses_l S) (get_conflict_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)
(clauses_to_update_l S)
(literals_to_update_l S)›
by (cases S) auto
definition set_conflict' :: ‹'v clause option ⇒ 'v twl_st ⇒ 'v twl_st› where
‹set_conflict' = (λC (M, N, U, D, NE, UE, NS, US, WS, Q). (M, N, U, C, NE, UE, NS, US, WS, Q))›
definition all_lits_of_st_l :: ‹'v twl_st_l ⇒ 'v literal multiset› where
‹all_lits_of_st_l S = all_lits_of_mm (get_all_clss_l S)›
lemma get_unit_clauses_l_alt_def:
‹get_unit_clauses_l S = get_unkept_unit_clauses_l S + get_kept_unit_clauses_l S›
by (cases S) (auto)
inductive convert_lit
:: ‹'v clauses_l ⇒ 'v clauses ⇒ ('v, nat) ann_lit ⇒ ('v, 'v clause) ann_lit ⇒ bool›
where
‹convert_lit N E (Decided K) (Decided K)› |
‹convert_lit N E (Propagated K C) (Propagated K C')›
if ‹C' = mset (N ∝ C)› ‹C ∈# dom_m N› and ‹C ≠ 0› |
‹convert_lit N E (Propagated K C) (Propagated K C')›
if ‹C = 0› and ‹C' ∈# E›
definition convert_lits_l where
‹convert_lits_l N E = ⟨p2rel (convert_lit N E)⟩ list_rel›
lemma convert_lits_l_nil[simp]:
‹([], a) ∈ convert_lits_l N E ⟷ a = []›
‹(b, []) ∈ convert_lits_l N E ⟷ b = []›
by (auto simp: convert_lits_l_def)
lemma convert_lits_l_cons[simp]:
‹(L # M, L' # M') ∈ convert_lits_l N E ⟷
convert_lit N E L L' ∧ (M, M') ∈ convert_lits_l N E›
by (auto simp: convert_lits_l_def p2rel_def)
lemma take_convert_lits_lD:
‹(M, M') ∈ convert_lits_l N E ⟹
(take n M, take n M') ∈ convert_lits_l N E›
by (auto simp: convert_lits_l_def list_rel_def)
lemma convert_lits_l_consE:
‹(Propagated L C # M, x) ∈ convert_lits_l N E ⟹
(⋀L' C' M'. x = Propagated L' C' # M' ⟹ (M, M') ∈ convert_lits_l N E ⟹
convert_lit N E (Propagated L C) (Propagated L' C') ⟹ P) ⟹ P›
by (cases x) (auto simp: convert_lit.simps)
lemma convert_lits_l_append[simp]:
‹length M1 = length M1' ⟹
(M1 @ M2, M1' @ M2') ∈ convert_lits_l N E ⟷ (M1, M1') ∈ convert_lits_l N E ∧
(M2, M2') ∈ convert_lits_l N E ›
by (auto simp: convert_lits_l_def list_rel_append2 list_rel_imp_same_length)
lemma convert_lits_l_map_lit_of: ‹(ay, bq) ∈ convert_lits_l N e ⟹ map lit_of ay = map lit_of bq›
apply (induction ay arbitrary: bq)
subgoal by auto
subgoal for L M bq by (cases bq) (auto simp: convert_lit.simps)
done
lemma convert_lits_l_tlD:
‹(M, M') ∈ convert_lits_l N E ⟹
(tl M, tl M') ∈ convert_lits_l N E›
by (cases M; cases M') auto
lemma convert_lits_l_swap:
‹i < length (N ∝ C) ⟹ j < length (N ∝ C) ⟹ C ∈# dom_m N ⟹
(M, M') ∈ convert_lits_l (N(C ↪swap (N ∝ C) i j)) E ⟷
(M, M') ∈ convert_lits_l N E›
by (fastforce simp: convert_lits_l_def list_rel_def p2rel_def
convert_lit.simps list_all2_conv_all_nth)
lemma get_clauses_l_set_clauses_to_update_l[simp]:
‹get_clauses_l (set_clauses_to_update_l WC S) = get_clauses_l S›
by (cases S) auto
lemma get_trail_l_set_clauses_to_update_l[simp]:
‹get_trail_l (set_clauses_to_update_l WC S) = get_trail_l S›
by (cases S) auto
lemma get_trail_set_clauses_to_update[simp]:
‹get_trail (set_clauses_to_update WC S) = get_trail S›
by (cases S) auto
lemma convert_lits_l_add_mset:
‹(M, M') ∈ convert_lits_l N E ⟹
(M, M') ∈ convert_lits_l N (add_mset C E)›
by (fastforce simp: convert_lits_l_def list_rel_def p2rel_def
convert_lit.simps list_all2_conv_all_nth)
lemma convert_lit_bind_new:
‹C ∉# dom_m N ⟹ C > 0 ⟹
convert_lit N E L L'⟹
convert_lit (N(C ↪ C')) E L L'›
‹C ∉# dom_m N ⟹ C > 0 ⟹
convert_lit N E L L'⟹
convert_lit (fmupd C C'' N) E L L'›
by (auto simp: convert_lit.simps)
lemma convert_lits_l_bind_new:
‹C ∉# dom_m N ⟹ C > 0 ⟹
(M, M') ∈ convert_lits_l N E ⟹
(M, M') ∈ convert_lits_l (N(C ↪ C')) E›
‹C ∉# dom_m N ⟹ C > 0 ⟹
(M, M') ∈ convert_lits_l N E ⟹
(M, M') ∈ convert_lits_l (fmupd C C'' N) E›
by (auto simp: convert_lits_l_def list_rel_def p2rel_def
list_all2_conv_all_nth convert_lit_bind_new)
abbreviation resolve_cls_l where
‹resolve_cls_l L D' E ≡ union_mset_list (remove1 (-L) D') (remove1 L E)›
lemma mset_resolve_cls_l_resolve_cls[iff]:
‹mset (resolve_cls_l L D' E) = cdcl⇩W_restart_mset.resolve_cls L (mset D') (mset E)›
by (auto simp: union_mset_list[symmetric])
lemma resolve_cls_l_nil_iff:
‹resolve_cls_l L D' E = [] ⟷ cdcl⇩W_restart_mset.resolve_cls L (mset D') (mset E) = {#}›
by (metis mset_resolve_cls_l_resolve_cls mset_zero_iff)
lemma lit_of_convert_lit[simp]:
‹convert_lit N E L L' ⟹ lit_of L' = lit_of L›
by (auto simp: p2rel_def convert_lit.simps)
lemma is_decided_convert_lit[simp]:
‹convert_lit N E L L' ⟹ is_decided L' ⟷ is_decided L›
by (cases L) (auto simp: p2rel_def convert_lit.simps)
lemma defined_lit_convert_lits_l[simp]: ‹(M, M') ∈ convert_lits_l N E ⟹
defined_lit M' = defined_lit M›
apply (induction M arbitrary: M')
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: defined_lit_cons)
done
lemma no_dup_convert_lits_l[simp]: ‹(M, M') ∈ convert_lits_l N E ⟹
no_dup M' ⟷ no_dup M›
apply (induction M arbitrary: M')
subgoal by auto
subgoal for L M M'
by (cases M') auto
done
lemma
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
count_decided_convert_lits_l[simp]:
‹count_decided M' = count_decided M›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: convert_lits_l_def p2rel_def)
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def)
done
lemma
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
get_level_convert_lits_l[simp]:
‹get_level M' = get_level M›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(fastforce simp: convert_lits_l_def p2rel_def get_level_cons_if split: if_splits)+
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def get_level_cons_if)
done
lemma
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
get_maximum_level_convert_lits_l[simp]:
‹get_maximum_level M' = get_maximum_level M›
by (intro ext, rule get_maximum_level_cong)
(use assms in auto)
lemma list_of_l_convert_map_lit_of:
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
‹map lit_of M' = map lit_of M›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: convert_lits_l_def p2rel_def)
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def)
done
lemma list_of_l_convert_lits_l[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
‹lits_of_l M' = lits_of_l M›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: convert_lits_l_def p2rel_def)
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def)
done
lemma is_proped_hd_convert_lits_l[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E› and ‹M ≠ []›
shows ‹is_proped (hd M') ⟷ is_proped (hd M)›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: convert_lits_l_def p2rel_def)
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def convert_lit.simps)
done
lemma is_decided_hd_convert_lits_l[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E› and ‹M ≠ []›
shows
‹is_decided (hd M') ⟷ is_decided (hd M)›
by (meson assms(1) assms(2) is_decided_no_proped_iff is_proped_hd_convert_lits_l)
lemma lit_of_hd_convert_lits_l[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E› and ‹M ≠ []›
shows
‹lit_of (hd M') = lit_of (hd M)›
by (cases M; cases M') (use assms in auto)
lemma lit_of_l_convert_lits_l[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
‹lit_of ` set M' = lit_of ` set M›
using assms
apply (induction M arbitrary: M' rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M M'
by (cases M')
(auto simp: convert_lits_l_def p2rel_def)
subgoal for L C M M'
by (cases M') (auto simp: convert_lits_l_def p2rel_def)
done
text ‹The order of the assumption is important for simpler use.›
lemma convert_lits_l_extend_mono:
assumes ‹(a,b) ∈ convert_lits_l N E›
‹∀L i. Propagated L i ∈ set a ∧ i ∈# dom_m N ⟶
mset (N∝i) = mset (N'∝i) ∧ i ∈# dom_m N'› and
‹E ⊆# E'›
shows
‹(a,b) ∈ convert_lits_l N' E'›
using assms
apply (induction a arbitrary: b rule: ann_lit_list_induct)
subgoal by auto
subgoal for l A b
by (cases b)
(auto simp: convert_lits_l_def p2rel_def convert_lit.simps)
subgoal for l C A b
by (cases b)
(auto simp: convert_lits_l_def p2rel_def convert_lit.simps)
done
lemma convert_lits_l_nil_iff[simp]:
assumes ‹(M, M') ∈ convert_lits_l N E›
shows
‹M' = [] ⟷ M = []›
using assms by auto
lemma convert_lits_l_atm_lits_of_l:
assumes ‹(M, M') ∈ convert_lits_l N E›
shows ‹atm_of ` lits_of_l M = atm_of ` lits_of_l M'›
using assms by auto
lemma convert_lits_l_true_clss_clss[simp]:
‹(M, M') ∈ convert_lits_l N E ⟹ M' ⊨as C ⟷ M ⊨as C›
unfolding true_annots_true_cls
by (auto simp: p2rel_def)
lemma convert_lit_propagated_decided[iff]:
‹convert_lit b d (Propagated x21 x22) (Decided x1) ⟷ False›
by (auto simp: convert_lit.simps)
lemma convert_lit_decided[iff]:
‹convert_lit b d (Decided x1) (Decided x2) ⟷ x1 = x2›
by (auto simp: convert_lit.simps)
lemma convert_lit_decided_propagated[iff]:
‹convert_lit b d (Decided x1) (Propagated x21 x22) ⟷ False›
by (auto simp: convert_lit.simps)
lemma convert_lits_l_lit_of_mset[simp]:
‹(a, af) ∈ convert_lits_l N E ⟹ lit_of `# mset af = lit_of `# mset a›
apply (induction a arbitrary: af)
subgoal by auto
subgoal for L M af
by (cases af) auto
done
lemma convert_lits_l_imp_same_length:
‹(a, b) ∈ convert_lits_l N E ⟹ length a = length b›
by (auto simp: convert_lits_l_def list_rel_imp_same_length)
lemma convert_lits_l_decomp_ex:
assumes
H: ‹(Decided K # a, M2) ∈ set (get_all_ann_decomposition x)› and
xxa: ‹(x, xa) ∈ convert_lits_l aa ac›
shows ‹∃M2. (Decided K # drop (length xa - length a) xa, M2)
∈ set (get_all_ann_decomposition xa)› (is ?decomp) and
‹(a, drop (length xa - length a) xa) ∈ convert_lits_l aa ac› (is ?a)
proof -
from H obtain M3 where
x: ‹x = M3 @ M2 @ Decided K # a›
by blast
obtain M3' M2' a' where
xa: ‹xa = M3' @ M2' @ Decided K # a'› and
‹(M3, M3') ∈ convert_lits_l aa ac› and
‹(M2, M2') ∈ convert_lits_l aa ac› and
aa': ‹(a, a') ∈ convert_lits_l aa ac›
using xxa unfolding x
by (auto simp: list_rel_append1 convert_lits_l_def p2rel_def convert_lit.simps
list_rel_split_right_iff)
then have a': ‹a' = drop (length xa - length a) xa› and [simp]: ‹length xa ≥ length a›
unfolding xa by (auto simp: convert_lits_l_imp_same_length)
show ?decomp
using get_all_ann_decomposition_ex[of K a' ‹M3' @ M2'›]
unfolding xa
unfolding a'
by auto
show ?a
using aa' unfolding a' .
qed
lemma in_convert_lits_lD:
‹K ∈ set TM ⟹
(M, TM) ∈ convert_lits_l N NE ⟹
∃K'. K' ∈ set M ∧ convert_lit N NE K' K›
by (auto 5 5 simp: convert_lits_l_def list_rel_append2 dest!: split_list p2relD
elim!: list_relE)
lemma in_convert_lits_lD2:
‹K ∈ set M ⟹
(M, TM) ∈ convert_lits_l N NE ⟹
∃K'. K' ∈ set TM ∧ convert_lit N NE K K'›
by (auto 5 5 simp: convert_lits_l_def list_rel_append1 dest!: split_list p2relD
elim!: list_relE)
lemma convert_lits_l_filter_decided: ‹(S, S') ∈ convert_lits_l M N ⟹
map lit_of (filter is_decided S') = map lit_of (filter is_decided S)›
apply (induction S arbitrary: S')
subgoal by auto
subgoal for L S S'
by (cases S') auto
done
lemma convert_lits_lI:
‹length M = length M' ⟹ (⋀i. i < length M ⟹ convert_lit N NE (M!i) (M'!i)) ⟹
(M, M') ∈ convert_lits_l N NE›
by (auto simp: convert_lits_l_def list_rel_def p2rel_def list_all2_conv_all_nth)
fun get_learned_clauses_l :: ‹'v twl_st_l ⇒ 'v clause_l multiset› where
‹get_learned_clauses_l (M, N, D, NE, UE, WS, Q) = learned_clss_lf N›
lemma get_subsumed_clauses_l_simps[simp]:
‹get_subsumed_init_clauses_l (set_clauses_to_update_l K S) = get_subsumed_init_clauses_l S›
‹get_subsumed_learned_clauses_l (set_clauses_to_update_l K S) = get_subsumed_learned_clauses_l S›
‹get_subsumed_clauses_l (set_clauses_to_update_l K S) = get_subsumed_clauses_l S›
by (solves ‹cases S; auto›)+
definition twl_st_l :: ‹_ ⇒ ('v twl_st_l × 'v twl_st) set› where
‹twl_st_l L =
{((M, N, C, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q), (M', N', U', C', NE', UE', NS', US', N0', U0', WS', Q')).
(M, M') ∈ convert_lits_l N (NEk+UEk) ∧
N' = twl_clause_of `# init_clss_lf N ∧
U' = twl_clause_of `# learned_clss_lf N ∧
C' = C ∧
NE' = NE+NEk ∧
UE' = UE + UEk ∧
NS' = NS ∧
US' = US ∧
N0' = N0 ∧
U0' = U0 ∧
WS' = (case L of None ⇒ {#} | Some L ⇒ image_mset (λj. (L, twl_clause_of (N ∝ j))) WS) ∧
Q' = Q
}›
lemma clss_state⇩W_of[twl_st]:
assumes ‹(S, R) ∈ twl_st_l L›
shows
‹init_clss (state⇩W_of R) = 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›
‹learned_clss (state⇩W_of R) = 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›
using assms
by (cases S; cases R; cases L; auto simp: init_clss.simps learned_clss.simps twl_st_l_def
mset_take_mset_drop_mset')+
named_theorems twl_st_l ‹Conversions simp rules›
lemma [twl_st_l]:
assumes ‹(S, T) ∈ twl_st_l L›
shows
‹(get_trail_l S, get_trail T) ∈ convert_lits_l (get_clauses_l S) (get_kept_unit_clauses_l S)› and
‹get_clauses T = twl_clause_of `# fst `# ran_m (get_clauses_l S)› and
‹get_conflict T = get_conflict_l S› and
‹L = None ⟹ clauses_to_update T = {#}›
‹L ≠ None ⟹ clauses_to_update T =
(λj. (the L, twl_clause_of (get_clauses_l S ∝ j))) `# clauses_to_update_l S› and
‹literals_to_update T = literals_to_update_l S›
‹backtrack_lvl (state⇩W_of T) = count_decided (get_trail_l S)›
‹unit_clss T = get_unit_clauses_l S›
‹cdcl⇩W_restart_mset.clauses (state⇩W_of T) =
mset `# ran_mf (get_clauses_l S) + get_unit_clauses_l S + get_subsumed_clauses_l S +
get_clauses0_l S› and
‹no_dup (get_trail T) ⟷ no_dup (get_trail_l S)› and
‹lits_of_l (get_trail T) = lits_of_l (get_trail_l S)› and
‹count_decided (get_trail T) = count_decided (get_trail_l S)› and
‹get_trail T = [] ⟷ get_trail_l S = []› and
‹get_trail T ≠ [] ⟷ get_trail_l S ≠ []› and
‹get_trail T ≠ [] ⟹ is_proped (hd (get_trail T)) ⟷ is_proped (hd (get_trail_l S))›
‹get_trail T ≠ [] ⟹ is_decided (hd (get_trail T)) ⟷ is_decided (hd (get_trail_l S))›
‹get_trail T ≠ [] ⟹ lit_of (hd (get_trail T)) = lit_of (hd (get_trail_l S))›
‹get_level (get_trail T) = get_level (get_trail_l S)›
‹get_maximum_level (get_trail T) = get_maximum_level (get_trail_l S)›
‹get_trail T ⊨as D ⟷ get_trail_l S ⊨as D›
‹subsumed_init_clauses T = get_subsumed_init_clauses_l S›
‹subsumed_learned_clauses T = get_subsumed_learned_clauses_l S›
‹subsumed_clauses T = get_subsumed_clauses_l S›
‹get_all_clss T = get_all_clss_l S›
‹all_lits_of_st T = all_lits_of_st_l S›
using assms unfolding twl_st_l_def all_clss_lf_ran_m[symmetric]
apply (auto split: option.splits simp: clauses_def mset_take_mset_drop_mset'
all_lits_of_st_def all_lits_of_st_l_def; fail)+
using assms unfolding twl_st_l_def all_clss_lf_ran_m[symmetric]
all_lits_of_st_def all_lits_of_st_l_def image_mset_union
by (auto split: option.splits simp: clauses_def mset_take_mset_drop_mset'
all_lits_of_st_def all_lits_of_st_l_def; auto simp: ac_simps; fail)
lemma (in -) [twl_st_l]:
‹(S, T)∈twl_st_l b ⟹
get_all_init_clss T = mset `# init_clss_lf (get_clauses_l S) + get_unit_init_clauses_l S +
subsumed_init_clauses T + get_init_clauses0 T›
‹(S, T)∈twl_st_l b ⟹ get_all_learned_clss T = 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›
by (cases S; cases T; cases b; auto simp: twl_st_l_def mset_take_mset_drop_mset'; fail)+
lemma [twl_st_l]:
assumes ‹(S, T) ∈ twl_st_l L›
shows ‹lit_of ` set (get_trail T) = lit_of ` set (get_trail_l S)›
using twl_st_l[OF assms] unfolding lits_of_def
by simp
lemma [twl_st_l]:
‹get_trail_l (set_literals_to_update_l D S) = get_trail_l S›
by (cases S) auto
lemma [twl_st_l]: ‹(S, T) ∈ twl_st_l L ⟹ defined_lit (get_trail T) = defined_lit (get_trail_l S)›
by (cases S; cases L) (auto simp: twl_st_l_def)
fun remove_one_lit_from_wq :: ‹nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹remove_one_lit_from_wq L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) =
(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, remove1_mset L WS, Q)›
lemma [twl_st_l]: ‹get_conflict_l (set_clauses_to_update_l W S) = get_conflict_l S›
by (cases S) auto
lemma [twl_st_l]: ‹get_conflict_l (remove_one_lit_from_wq L S) = get_conflict_l S›
by (cases S) auto
lemma [twl_st_l]: ‹literals_to_update_l (set_clauses_to_update_l Cs S) = literals_to_update_l S›
by (cases S) auto
lemma [twl_st_l]: ‹get_unit_clauses_l (set_clauses_to_update_l Cs S) = get_unit_clauses_l S›
by (cases S) auto
lemma [twl_st_l]: ‹get_unit_clauses_l (remove_one_lit_from_wq L S) = get_unit_clauses_l S›
by (cases S) auto
lemma [twl_st_l]:
‹get_unit_init_clauses_l (set_clauses_to_update_l Cs S) = get_unit_init_clauses_l S›
by (cases S; auto; fail)+
lemma [twl_st_l]:
‹get_unit_init_clauses_l (remove_one_lit_from_wq L S) = get_unit_init_clauses_l S›
by (cases S; auto; fail)+
lemma [twl_st_l]:
‹get_clauses_l (remove_one_lit_from_wq L S) = get_clauses_l S›
‹get_trail_l (remove_one_lit_from_wq L S) = get_trail_l S›
by (cases S; auto; fail)+
lemma [twl_st_l]:
‹get_unit_learned_clss_l (set_clauses_to_update_l Cs S) = get_unit_learned_clss_l S›
by (cases S) auto
lemma [twl_st_l]:
‹get_unit_learned_clss_l (remove_one_lit_from_wq L S) = get_unit_learned_clss_l S›
by (cases S) auto
lemma literals_to_update_l_remove_one_lit_from_wq[simp]:
‹literals_to_update_l (remove_one_lit_from_wq L T) = literals_to_update_l T›
by (cases T) auto
lemma clauses_to_update_l_remove_one_lit_from_wq[simp]:
‹clauses_to_update_l (remove_one_lit_from_wq L T) = remove1_mset L (clauses_to_update_l T)›
by (cases T) auto
lemma get_clauses0[twl_st_l]:
‹get_all_clauses0 (set_clauses_to_update WS S) = get_all_clauses0 S›
‹get_init_clauses0 (set_clauses_to_update WS S) = get_init_clauses0 S›
‹get_learned_clauses0 (set_clauses_to_update WS S) = get_learned_clauses0 S›
by (cases S; auto; fail)+
lemma get_clauses0_l[twl_st_l]:
‹get_clauses0_l (set_clauses_to_update_l WS S) = get_clauses0_l S›
‹get_init_clauses0_l (set_clauses_to_update_l WS S) = get_init_clauses0_l S›
‹get_learned_clauses0_l (set_clauses_to_update_l WS S) = get_learned_clauses0_l S›
‹get_clauses0_l (set_literals_to_update_l WS' S) = get_clauses0_l S›
‹get_init_clauses0_l (set_literals_to_update_l WS' S) = get_init_clauses0_l S›
‹get_learned_clauses0_l (set_literals_to_update_l WS' S) = get_learned_clauses0_l S›
‹get_clauses0_l (remove_one_lit_from_wq L S) = get_clauses0_l S›
‹get_init_clauses0_l (remove_one_lit_from_wq L S) = get_init_clauses0_l S›
‹get_learned_clauses0_l (remove_one_lit_from_wq L S) = get_learned_clauses0_l S›
by (cases S; auto; fail)+
declare twl_st_l[simp]
lemma unit_init_clauses_get_unit_init_clauses_l[twl_st_l]:
‹(S, T) ∈ twl_st_l L ⟹ unit_init_clauses T = get_unit_init_clauses_l S› and
get_init_learned_clss_get_init_learned_clss_l[twl_st_l]:
‹(S, T) ∈ twl_st_l L ⟹ get_init_learned_clss T = get_unit_learned_clss_l S›
by (cases S) (auto simp: twl_st_l_def init_clss.simps)
lemma get_clauses0_l_get_clauses0[twl_st,simp]:
‹(S, T) ∈ twl_st_l L ⟹ get_all_clauses0 T = get_clauses0_l S›
‹(S, T) ∈ twl_st_l L ⟹ get_init_clauses0 T = get_init_clauses0_l S›
‹(S, T) ∈ twl_st_l L ⟹ get_learned_clauses0 T = get_learned_clauses0_l S›
by (cases S) (auto simp: twl_st_l_def init_clss.simps)
lemma clauses_state_to_l[twl_st_l]: ‹(S, S') ∈ twl_st_l L ⟹
cdcl⇩W_restart_mset.clauses (state⇩W_of S') = mset `# ran_mf (get_clauses_l S) +
get_unit_init_clauses_l S + get_unit_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›
apply (subst all_clss_l_ran_m[symmetric])
unfolding image_mset_union
by (cases S) (auto simp: twl_st_l_def init_clss.simps mset_take_mset_drop_mset' clauses_def)
lemma clauses_to_update_l_set_clauses_to_update_l[twl_st_l]:
‹clauses_to_update_l (set_clauses_to_update_l WS S) = WS›
by (cases S) auto
lemma hd_get_trail_twl_st_of_get_trail_l:
‹(S, T) ∈ twl_st_l L ⟹ get_trail_l S ≠ [] ⟹
lit_of (hd (get_trail T)) = lit_of (hd (get_trail_l S))›
by (cases S; cases ‹get_trail_l S›; cases ‹get_trail T›) (auto simp: twl_st_l_def)
lemma twl_st_l_mark_of_hd:
‹(x, y) ∈ twl_st_l b ⟹
get_trail_l x ≠ [] ⟹
is_proped (hd (get_trail_l x)) ⟹
mark_of (hd (get_trail_l x)) > 0 ⟹
mark_of (hd (get_trail y)) = mset (get_clauses_l x ∝ mark_of (hd (get_trail_l x)))›
by (cases ‹get_trail_l x›; cases ‹get_trail y›; cases ‹hd (get_trail_l x)›;
cases ‹hd (get_trail y)›)
(auto simp: twl_st_l_def convert_lit.simps)
lemma twl_st_l_lits_of_tl:
‹(x, y) ∈ twl_st_l b ⟹
lits_of_l (tl (get_trail y)) = (lits_of_l (tl (get_trail_l x)))›
by (cases ‹get_trail_l x›; cases ‹get_trail y›; cases ‹hd (get_trail_l x)›;
cases ‹hd (get_trail y)›)
(auto simp: twl_st_l_def convert_lit.simps)
lemma twl_st_l_mark_of_is_decided:
‹(x, y) ∈ twl_st_l b ⟹
get_trail_l x ≠ [] ⟹
is_decided (hd (get_trail y)) = is_decided (hd (get_trail_l x))›
by (cases ‹get_trail_l x›; cases ‹get_trail y›; cases ‹hd (get_trail_l x)›;
cases ‹hd (get_trail y)›)
(auto simp: twl_st_l_def convert_lit.simps)
lemma twl_st_l_mark_of_is_proped:
‹(x, y) ∈ twl_st_l b ⟹
get_trail_l x ≠ [] ⟹
is_proped (hd (get_trail y)) = is_proped (hd (get_trail_l x))›
by (cases ‹get_trail_l x›; cases ‹get_trail y›; cases ‹hd (get_trail_l x)›;
cases ‹hd (get_trail y)›)
(auto simp: twl_st_l_def convert_lit.simps)
lemma [simp]:
‹get_clauses_l (set_literals_to_update_l L T) = get_clauses_l T›
‹get_unit_clauses_l (set_literals_to_update_l L T) = get_unit_clauses_l T›
‹get_subsumed_clauses_l (set_literals_to_update_l L T) = get_subsumed_clauses_l T›
by (cases T; auto; fail)+
fun equality_except_trail :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
‹equality_except_trail (M, N, D, NE, UE, NS, US, WS, Q) (M', N', D', NE', UE', NS', US', WS', Q') ⟷
N = N' ∧ D = D' ∧ NE = NE' ∧ UE = UE' ∧ NS = NS' ∧ US = US' ∧ WS = WS' ∧ Q = Q'›
fun equality_except_conflict_l :: ‹'v twl_st_l ⇒ 'v twl_st_l ⇒ bool› where
‹equality_except_conflict_l (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) (M', N', D', NE', UE', NEk',
UEk', NS', US', WS', Q') ⟷
M = M' ∧ N = N' ∧ NE = NE' ∧ UE = UE' ∧ NEk = NEk' ∧ UEk = UEk' ∧ NS = NS' ∧ US = US' ∧ WS = WS' ∧ Q = Q'›
lemma equality_except_conflict_l_rewrite:
assumes ‹equality_except_conflict_l S T›
shows
‹get_trail_l S = get_trail_l T› and
‹get_clauses_l S = get_clauses_l T›
using assms by (cases S; cases T; auto; fail)+
lemma equality_except_conflict_l_alt_def:
‹equality_except_conflict_l S T ⟷
get_trail_l S = get_trail_l T ∧ get_clauses_l S = get_clauses_l T ∧
get_kept_init_clauses_l S = get_kept_init_clauses_l T ∧
get_kept_learned_clss_l S = get_kept_learned_clss_l T ∧
get_unkept_init_clauses_l S = get_unkept_init_clauses_l T ∧
get_unkept_learned_clss_l S = get_unkept_learned_clss_l T ∧
get_unit_learned_clss_l S = get_unit_learned_clss_l T ∧
literals_to_update_l S = literals_to_update_l T ∧
clauses_to_update_l S = clauses_to_update_l T ∧
get_subsumed_learned_clauses_l S = get_subsumed_learned_clauses_l T ∧
get_subsumed_init_clauses_l S = get_subsumed_init_clauses_l T ∧
get_init_clauses0_l S = get_init_clauses0_l T ∧
get_learned_clauses0_l S = get_learned_clauses0_l T›
by (cases S, cases T) auto
lemma equality_except_conflict_alt_def:
‹equality_except_conflict S T ⟷
get_trail S = get_trail T ∧ get_init_clauses S = get_init_clauses T ∧
get_learned_clss S = get_learned_clss T ∧
get_init_learned_clss S = get_init_learned_clss T ∧
unit_init_clauses S = unit_init_clauses T ∧
literals_to_update S = literals_to_update T ∧
clauses_to_update S = clauses_to_update T ∧
subsumed_learned_clauses S = subsumed_learned_clauses T ∧
subsumed_init_clauses S = subsumed_init_clauses T ∧
get_init_clauses0 S = get_init_clauses0 T ∧
get_learned_clauses0 S = get_learned_clauses0 T›
by (cases S, cases T) auto
lemma all_lits_of_st_simps[simp]:
‹all_lits_of_st (set_clauses_to_update C S)= all_lits_of_st S›
by (cases S; auto simp: all_lits_of_st_def)
lemma all_lits_of_st_l_simps[simp]:
‹all_lits_of_st_l (set_clauses_to_update_l C T)= all_lits_of_st_l T›
‹all_lits_of_st_l (set_literals_to_update_l C' T)= all_lits_of_st_l T›
‹all_lits_of_st_l (remove_one_lit_from_wq n T)= all_lits_of_st_l T›
‹-L ∈# all_lits_of_st_l T ⟷ L ∈# all_lits_of_st_l T›
by (cases T; auto simp: all_lits_of_st_l_def in_all_lits_of_mm_ain_atms_of_iff; fail)+
section ‹Additional Invariants and Definitions›
definition twl_list_invs where
‹twl_list_invs S ⟷
(∀C ∈# clauses_to_update_l S. C ∈# dom_m (get_clauses_l S)) ∧
0 ∉# dom_m (get_clauses_l S) ∧
(∀L C. Propagated L C ∈ set (get_trail_l S) ⟶ (C > 0 ⟶ C ∈# dom_m (get_clauses_l S) ∧
(C > 0 ⟶ L ∈ set (watched_l (get_clauses_l S ∝ C)) ∧
(length (get_clauses_l S ∝ C) > 2 ⟶ L = get_clauses_l S ∝ C ! 0)))) ∧
distinct_mset (clauses_to_update_l S) ∧
(∀C∈#ran_mf (get_clauses_l S). ¬tautology (mset C))›
definition polarity where
‹polarity M L =
(if undefined_lit M L then None else if L ∈ lits_of_l M then Some True else Some False)›
lemma polarity_None_undefined_lit: ‹is_None (polarity M L) ⟹ undefined_lit M L›
by (auto simp: polarity_def split: if_splits)
lemma polarity_spec:
assumes ‹no_dup M›
shows
‹RETURN (polarity M L) ≤ SPEC(λv. (v = None ⟷ undefined_lit M L) ∧
(v = Some True ⟷ L ∈ lits_of_l M) ∧ (v = Some False ⟷ -L ∈ lits_of_l M))›
unfolding polarity_def
by refine_vcg
(use assms in ‹auto simp: defined_lit_map lits_of_def atm_of_eq_atm_of uminus_lit_swap
no_dup_cannot_not_lit_and_uminus
split: option.splits›)
lemma polarity_spec':
assumes ‹no_dup M›
shows
‹polarity M L = None ⟷ undefined_lit M L› and
‹polarity M L = Some True ⟷ L ∈ lits_of_l M› and
‹polarity M L = Some False ⟷ -L ∈ lits_of_l M›
unfolding polarity_def
by (use assms in ‹auto simp: defined_lit_map lits_of_def atm_of_eq_atm_of uminus_lit_swap
no_dup_cannot_not_lit_and_uminus
split: option.splits›)
definition mop_polarity_l :: ‹'v twl_st_l ⇒ 'v literal ⇒ bool option nres› where
‹mop_polarity_l S L = do {
ASSERT(L ∈# all_lits_of_st_l S);
ASSERT(no_dup (get_trail_l S));
RETURN(polarity (get_trail_l S) L)
}›
definition find_unwatched_l :: ‹('v, _) ann_lits ⇒ _ ⇒ nat ⇒ nat option nres› where
‹find_unwatched_l M N C = do {
ASSERT(C ∈# dom_m N ∧ length (N ∝ C) ≥ 2 ∧ distinct (N ∝ C) ∧ no_dup M);
SPEC (λ(found).
(found = None ⟷ (∀L∈set (unwatched_l (N ∝ C)). -L ∈ lits_of_l M)) ∧
(∀j. found = Some j ⟶ (j < length (N ∝ C) ∧ (undefined_lit M (N ∝ C!j) ∨ N ∝ C!j ∈ lits_of_l M) ∧ j ≥ 2)))
}›
definition set_conflict_l_pre :: ‹nat ⇒ 'v twl_st_l ⇒ bool› where
‹set_conflict_l_pre C S ⟷
get_conflict_l S = None ∧ C ∈# dom_m (get_clauses_l S) ∧ ¬tautology (mset (get_clauses_l S ∝ C)) ∧ distinct (get_clauses_l S ∝ C) ∧
get_trail_l S ⊨as CNot (mset (get_clauses_l S ∝ C)) ∧ twl_list_invs S ∧
(∃S' b. (set_clauses_to_update_l (clauses_to_update_l S + {#C#}) S, S') ∈ twl_st_l b ∧ twl_struct_invs S' ∧ twl_stgy_invs S')›
definition set_conflict_l :: ‹nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹set_conflict_l = (λC (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q). do {
ASSERT(set_conflict_l_pre C (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q));
RETURN (M, N, Some (mset (N ∝ C)), NE, UE, NEk, UEk, NS, US, N0, U0, {#}, {#})
})›
definition cons_trail_propagate_l where
‹cons_trail_propagate_l L C M = do {
ASSERT(undefined_lit M L);
RETURN (Propagated L C # M)
}›
definition propagate_lit_l :: ‹'v literal ⇒ nat ⇒ nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹propagate_lit_l = (λL' C i (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q). do {
ASSERT(C ∈# dom_m N);
ASSERT(L' ∈# all_lits_of_st_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q));
ASSERT(i ≤ 1);
M ← cons_trail_propagate_l L' C M;
N ← (if length (N ∝ C) > 2 then mop_clauses_swap N C 0 (Suc 0 - i) else RETURN N);
RETURN (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, add_mset (-L') Q)})›
definition update_clause_l_pre :: ‹nat ⇒ nat ⇒ nat ⇒ 'v twl_st_l ⇒ bool› where
‹update_clause_l_pre C i f S ⟷
(∃S' L. (S, S') ∈ twl_st_l (Some L) ∧ C ∈# dom_m (get_clauses_l S) ∧
i < length (get_clauses_l S ∝ C) ∧ f < length (get_clauses_l S ∝ C) ∧
update_clauseS_pre (get_clauses_l S ∝ C ! i) (twl_clause_of (get_clauses_l S ∝ C)) S')›
definition update_clause_l :: ‹nat ⇒ nat ⇒ nat ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹update_clause_l = (λC i f (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q). do {
ASSERT(update_clause_l_pre C i f (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q));
N' ← mop_clauses_swap N C i f;
RETURN (M, N', D, NE, UE, NEk, UEk, NS, US, WS, Q)
})›
definition unit_propagation_inner_loop_body_l_inv
:: ‹'v literal ⇒ nat ⇒ 'v twl_st_l ⇒ bool›
where
‹unit_propagation_inner_loop_body_l_inv L C S ⟷
(∃S'. (set_clauses_to_update_l (clauses_to_update_l S + {#C#}) S, S') ∈ twl_st_l (Some L) ∧
twl_struct_invs S' ∧
twl_stgy_invs S' ∧
C ∈# dom_m (get_clauses_l S) ∧
C > 0 ∧
0 < length (get_clauses_l S ∝ C) ∧
no_dup (get_trail_l S) ∧
(if (get_clauses_l S ∝ C) ! 0 = L then 0 else 1) < length (get_clauses_l S ∝ C) ∧
1 - (if (get_clauses_l S ∝ C) ! 0 = L then 0 else 1) < length (get_clauses_l S ∝ C) ∧
L ∈ set (watched_l (get_clauses_l S ∝ C)) ∧
get_conflict_l S = None
)
›
definition pos_of_watched :: ‹'v clauses_l ⇒ nat ⇒ 'v literal ⇒ nat nres› where
‹pos_of_watched N C L = do {
ASSERT(length (N ∝ C) > 0 ∧ C ∈# dom_m N);
RETURN (if (N ∝ C) ! 0 = L then 0 else 1)
}›
definition other_watched_l :: ‹'v twl_st_l ⇒ 'v literal ⇒ nat ⇒ nat ⇒ 'v literal nres› where
‹other_watched_l S L C i = do {
ASSERT(get_clauses_l S ∝ C ! i = L ∧ i < length (get_clauses_l S ∝ C) ∧ i < 2 ∧
C ∈# dom_m (get_clauses_l S) ∧ 1-i < length (get_clauses_l S ∝ C));
mop_clauses_at (get_clauses_l S) C (1 - i)
}›
definition unit_propagation_inner_loop_body_l :: ‹'v literal ⇒ nat ⇒
'v twl_st_l ⇒ 'v twl_st_l nres› where
‹unit_propagation_inner_loop_body_l L C S = do {
ASSERT(unit_propagation_inner_loop_body_l_inv L C S);
K ← SPEC(λK. K ∈ set (get_clauses_l S ∝ C));
val_K ← mop_polarity_l S K;
if val_K = Some True
then RETURN S
else do {
i ← pos_of_watched (get_clauses_l S) C L;
L' ← other_watched_l S L C i;
val_L' ← mop_polarity_l S L';
if val_L' = Some True
then RETURN S
else do {
f ← find_unwatched_l (get_trail_l S) (get_clauses_l S) C;
case f of
None ⇒
if val_L' = Some False
then set_conflict_l C S
else propagate_lit_l L' C i S
| Some f ⇒ do {
ASSERT(f < length (get_clauses_l S ∝ C));
K ← mop_clauses_at (get_clauses_l S) C f;
val_K ← mop_polarity_l S K;
if val_K = Some True then
RETURN S
else
update_clause_l C i f S
}
}
}
}›
lemma refine_add_invariants:
assumes
‹(f S) ≤ SPEC(λS'. Q S')› and
‹y ≤ ⇓ {(S, S'). P S S'} (f S)›
shows ‹y ≤ ⇓ {(S, S'). P S S' ∧ Q S'} (f S)›
using assms unfolding pw_le_iff pw_conc_inres pw_conc_nofail by force
lemma clauses_tuple[simp]:
‹cdcl⇩W_restart_mset.clauses (M, {#f x . x ∈# init_clss_l N#} + NE,
{#f x . x ∈# learned_clss_l N#} + UE, D) = {#f x. x ∈# all_clss_l N#} + NE + UE›
by (auto simp: clauses_def simp flip: image_mset_union)
lemma valid_enqueued_alt_simps[simp]:
‹valid_enqueued S ⟷
(∀(L, C) ∈# clauses_to_update S. L ∈# watched C ∧ C ∈# get_clauses S ∧
-L ∈ lits_of_l (get_trail S) ∧ get_level (get_trail S) L = count_decided (get_trail S)) ∧
(∀L ∈# literals_to_update S.
-L ∈ lits_of_l (get_trail S) ∧ get_level (get_trail S) L = count_decided (get_trail S))›
by (cases S) auto
declare valid_enqueued.simps[simp del]
lemma unit_propagation_inner_loop_body_alt_def:
‹unit_propagation_inner_loop_body L C S = do {
bL' ← SPEC (λK. K ∈# clause C);
val_bL' ← mop_lit_is_pos bL' S;
if val_bL'
then RETURN S
else do {
i ← RETURN ();
L' ← SPEC (λK. K ∈# watched C - {#L#});
ASSERT (watched C = {#L, L'#});
val_L' ← mop_lit_is_pos L' S;
if val_L'
then RETURN S
else
if ∀L ∈# unwatched C. -L ∈ lits_of_l (get_trail S)
then
if -L' ∈ lits_of_l (get_trail S)
then do {mop_set_conflicting C S}
else do {mop_propagate_lit L' C S}
else do {
update_clauseS L C S
}
}
}›
unfolding unit_propagation_inner_loop_body_def bind_to_let_conv Let_def
by (auto intro!: ext)
lemma [twl_st, simp]:
‹get_clauses (set_clauses_to_update C S') = get_clauses S'›
‹unit_clss (set_clauses_to_update C S') = unit_clss S'›
‹(S, S') ∈ twl_st_l (Some L) ⟹
clauses (get_clauses S') = {#mset (fst x). x ∈# ran_m (get_clauses_l S)#}›
apply (cases S'; auto simp: twl_st_l_def clauses_def)
apply (cases S'; auto simp: twl_st_l_def clauses_def)
apply (cases S'; auto simp: twl_st_l_def clauses_def mset_take_mset_drop_mset'
simp flip: image_mset_union)
done
lemma in_set_takeI:
‹i < j ⟹ i < length xs ⟹ xs ! i ∈ set (take j xs)›
by (auto simp: in_set_take_conv_nth intro!: exI[of _ i])
lemma unit_propagation_inner_loop_body_l:
fixes i C :: nat and S :: ‹'v twl_st_l› and S' :: ‹'v twl_st› and L :: ‹'v literal›
defines
C'[simp]: ‹C' ≡ get_clauses_l S ∝ C›
assumes
SS': ‹(S, S') ∈ twl_st_l (Some L)› and
WS: ‹C ∈# clauses_to_update_l S› and
struct_invs: ‹twl_struct_invs S'› and
add_inv: ‹twl_list_invs S› and
stgy_inv: ‹twl_stgy_invs S'›
shows
‹unit_propagation_inner_loop_body_l L C
(set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S) ≤
⇓ {(S, S'). ((S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S) ∧
(twl_stgy_invs S' ∧ twl_struct_invs S')}
(unit_propagation_inner_loop_body L (twl_clause_of C')
(set_clauses_to_update (clauses_to_update (S') - {#(L, twl_clause_of C')#}) S'))›
(is ‹?A ≤ ⇓ _ ?B›)
proof -
have C_0: ‹C > 0› and C_neq_0[iff]: ‹C ≠ 0›
using assms(3,5) unfolding twl_list_invs_def by (auto dest!: multi_member_split)
have C_N_U: ‹C ∈# dom_m (get_clauses_l S)›
using add_inv WS SS' by (auto simp: twl_list_invs_def)
let ?S = ‹set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S›
define i :: nat where ‹i ≡ (if get_clauses_l S∝C!0 = L then 0 else 1)›
let ?L = ‹C' ! i›
let ?L' = ‹C' ! (Suc 0 - i)›
have inv: ‹twl_st_inv S'› and
cdcl_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of S')› and
valid: ‹valid_enqueued S'›
using struct_invs WS by (auto simp: twl_struct_invs_def pcdcl_all_struct_invs_def)
have
w_q_inv: ‹clauses_to_update_inv S'› and
dist: ‹distinct_queued S'› and
no_dup: ‹no_duplicate_queued S'› and
confl: ‹get_conflict S' ≠ None ⟹ clauses_to_update S' = {#} ∧ literals_to_update S' = {#}› and
st_inv: ‹twl_st_inv S'›
using struct_invs unfolding twl_struct_invs_def by fast+
have dist_C: ‹distinct (get_clauses_l S ∝ C)›
using cdcl_inv SS' C_N_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_alt_def pcdcl_all_struct_invs_def
by (auto simp: ran_m_def dest!: multi_member_split)
let ?M = ‹get_trail_l S›
let ?N = ‹get_clauses_l S›
let ?WS = ‹clauses_to_update_l S›
let ?Q = ‹literals_to_update_l S›
have n_d: ‹no_dup ?M› and confl_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of S')›
using cdcl_inv SS' unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: trail.simps comp_def twl_st)
then have consistent: ‹- L ∉ lits_of_l ?M› if ‹L ∈ lits_of_l ?M› for L
using consistent_interp_def distinct_consistent_interp that by blast
have cons_M: ‹consistent_interp (lits_of_l ?M)›
using n_d distinct_consistent_interp by fast
let ?C' = ‹twl_clause_of C'›
have C'_N_U_or: ‹?C' ∈# twl_clause_of `# (init_clss_lf ?N) ∨
?C' ∈# twl_clause_of `# learned_clss_lf ?N›
using WS valid SS'
unfolding union_iff[symmetric] image_mset_union[symmetric] mset_append[symmetric]
by (auto simp: twl_struct_invs_def
split: prod.splits simp del: twl_clause_of.simps)
have struct: ‹struct_wf_twl_cls ?C'›
using C_N_U inv SS' WS valid unfolding valid_enqueued_alt_simps
by (auto simp: twl_st_inv_alt_def Ball_ran_m_dom_struct_wf
simp del: twl_clause_of.simps)
have C'_N_U: ‹?C' ∈# twl_clause_of `# all_clss_lf ?N›
using C'_N_U_or
unfolding union_iff[symmetric] image_mset_union[symmetric] mset_append[symmetric] .
have watched_C': ‹mset (watched_l C') = {#?L, ?L'#}›
using struct i_def SS' by (cases C) (auto simp: length_list_2 take_2_if)
then have mset_watched_C: ‹mset (watched_l C') = {#watched_l C' ! i, watched_l C' ! (Suc 0 - i)#}›
using i_def by (cases ‹twl_clause_of (get_clauses_l S ∝ C)›) (auto simp: take_2_if)
have two_le_length_C: ‹2 ≤ length C'›
by (metis length_take linorder_not_le min_less_iff_conj numeral_2_eq_2 order_less_irrefl
size_add_mset size_eq_0_iff_empty size_mset watched_C')
then have i_le_length_C: ‹i < length C'›
by (auto simp: i_def)
obtain WS' where WS'_def: ‹?WS = add_mset C WS'›
using multi_member_split[OF WS] by auto
then have WS'_def': ‹?WS = add_mset C WS'›
by auto
have L: ‹L ∈ set (watched_l C')› and uL_M: ‹-L ∈ lits_of_l (get_trail_l S)›
using valid SS' by (auto simp: WS'_def)
have C'_i[simp]: ‹C'!i = L›
using L two_le_length_C by (auto simp: take_2_if i_def split: if_splits)
then have [simp]: ‹?N∝C!i = L›
by auto
have C_neq_0[iff]: ‹C ≠ 0›
using assms(3,5) unfolding twl_list_invs_def by (auto dest!: multi_member_split)
then have C_0: ‹C > 0›
by linarith
have pre_inv: ‹unit_propagation_inner_loop_body_l_inv L C ?S›
unfolding unit_propagation_inner_loop_body_l_inv_def
proof (rule exI[of _ S'], intro conjI)
have S_readd_C_S: ‹set_clauses_to_update_l (clauses_to_update_l ?S + {#C#}) ?S = S›
using WS by (cases S) auto
show ‹(set_clauses_to_update_l
(clauses_to_update_l ?S + {#C#})
(set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S),
S') ∈ twl_st_l (Some L)›
using SS' unfolding S_readd_C_S .
show ‹twl_stgy_invs S'› ‹twl_struct_invs S'›
using assms by fast+
show ‹C ∈# dom_m (get_clauses_l ?S)›
using assms C_N_U by auto
show ‹C > 0›
by (rule C_0)
show ‹(if get_clauses_l ?S ∝ C ! 0 = L then 0 else 1) < length (get_clauses_l ?S ∝ C)›
using two_le_length_C by auto
show ‹1 - (if get_clauses_l ?S ∝ C ! 0 = L then 0 else 1) < length (get_clauses_l ?S ∝ C)›
using two_le_length_C by auto
show ‹length (get_clauses_l ?S ∝ C) > 0›
using two_le_length_C by auto
show ‹no_dup (get_trail_l ?S)›
using n_d by auto
show ‹L ∈ set (watched_l (get_clauses_l ?S ∝ C))›
using L by auto
show ‹get_conflict_l ?S = None›
using confl SS' WS by (cases ‹get_conflict_l S›) (auto dest: in_diffD)
qed
define pol_spec where
‹pol_spec bL' = {(b, b'). (b = None ⟶ ¬b') ∧ (b = Some True ⟷ b') ∧
(b' ⟷ bL'
∈ lits_of_l
(get_trail
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C')
(clauses_to_update S'))
S'))) ∧
(b = Some False ⟷ -bL'
∈ lits_of_l
(get_trail
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C')
(clauses_to_update S'))
S')))}› for bL'
have [refine]: ‹mop_polarity_l
(set_clauses_to_update_l
(remove1_mset C (clauses_to_update_l S)) S)
K
≤ ⇓(pol_spec L')
(mop_lit_is_pos L'
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C')
(clauses_to_update S'))
S'))›
if ‹(K,L') ∈ Id› for K L'
using that SS' unfolding mop_polarity_l_def mop_lit_is_pos_def
by refine_rcg
(auto simp: polarity_def mop_polarity_l_def twl_st mset_take_mset_drop_mset'
Decided_Propagated_in_iff_in_lits_of_l pol_spec_def dest: no_dup_consistentD
intro!: ASSERT_leI)
let ?S = ‹set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S›
obtain M N D NE UE NEk UEk NS US N0 U0 WS Q where
S: ‹S = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)›
by (cases S) auto
have C_N_U: ‹C ∈# dom_m (get_clauses_l S)›
using add_inv WS SS' by (auto simp: twl_list_invs_def)
let ?M = ‹get_trail_l S›
let ?N = ‹get_clauses_l S›
let ?WS = ‹clauses_to_update_l S›
let ?Q = ‹literals_to_update_l S›
define i :: nat where ‹i ≡ (if get_clauses_l S∝C!0 = L then 0 else 1)›
let ?L = ‹C' ! i›
let ?L' = ‹C' ! (Suc 0 - i)›
have inv: ‹twl_st_inv S'› and
cdcl_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of S')› and
valid: ‹valid_enqueued S'›
using struct_invs WS by (auto simp: twl_struct_invs_def pcdcl_all_struct_invs_def)
have
w_q_inv: ‹clauses_to_update_inv S'› and
dist: ‹distinct_queued S'› and
no_dup: ‹no_duplicate_queued S'› and
confl: ‹get_conflict S' ≠ None ⟹ clauses_to_update S' = {#} ∧ literals_to_update S' = {#}› and
st_inv: ‹twl_st_inv S'›
using struct_invs unfolding twl_struct_invs_def by fast+
have dist_C: ‹distinct (get_clauses_l S ∝ C)›
using cdcl_inv SS' C_N_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_alt_def
by (auto simp: ran_m_def dest!: multi_member_split)
have n_d: ‹no_dup ?M› and confl_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of S')›
using cdcl_inv SS' unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: trail.simps comp_def twl_st)
then have consistent: ‹- L ∉ lits_of_l ?M› if ‹L ∈ lits_of_l ?M› for L
using consistent_interp_def distinct_consistent_interp that by blast
have cons_M: ‹consistent_interp (lits_of_l ?M)›
using n_d distinct_consistent_interp by fast
let ?C' = ‹twl_clause_of C'›
have C'_N_U_or: ‹?C' ∈# twl_clause_of `# (init_clss_lf ?N) ∨
?C' ∈# twl_clause_of `# learned_clss_lf ?N›
using WS valid SS'
unfolding union_iff[symmetric] image_mset_union[symmetric] mset_append[symmetric]
by (auto simp: twl_struct_invs_def
split: prod.splits simp del: twl_clause_of.simps)
have struct: ‹struct_wf_twl_cls ?C'›
using C_N_U inv SS' WS valid unfolding valid_enqueued_alt_simps
by (auto simp: twl_st_inv_alt_def Ball_ran_m_dom_struct_wf
simp del: twl_clause_of.simps)
have C'_N_U: ‹?C' ∈# twl_clause_of `# all_clss_lf ?N›
using C'_N_U_or
unfolding union_iff[symmetric] image_mset_union[symmetric] mset_append[symmetric] .
have watched_C': ‹mset (watched_l C') = {#?L, ?L'#}›
using struct i_def SS' by (cases C) (auto simp: length_list_2 take_2_if)
then have mset_watched_C: ‹mset (watched_l C') = {#watched_l C' ! i, watched_l C' ! (Suc 0 - i)#}›
using i_def by (cases ‹twl_clause_of (get_clauses_l S ∝ C)›) (auto simp: take_2_if)
have two_le_length_C: ‹2 ≤ length C'›
by (metis length_take linorder_not_le min_less_iff_conj numeral_2_eq_2 order_less_irrefl
size_add_mset size_eq_0_iff_empty size_mset watched_C')
then have i_le_length_C: ‹i < length C'›
by (auto simp: i_def)
obtain WS' where WS'_def: ‹?WS = add_mset C WS'›
using multi_member_split[OF WS] by auto
then have WS'_def': ‹WS = add_mset C WS'›
unfolding S by auto
have L: ‹L ∈ set (watched_l C')› and uL_M: ‹-L ∈ lits_of_l (get_trail_l S)›
using valid SS' by (auto simp: WS'_def)
have C'_i[simp]: ‹C'!i = L›
using L two_le_length_C by (auto simp: take_2_if i_def split: if_splits)
then have [simp]: ‹?N∝C!i = L›
by auto
have i_def': ‹i = (if get_clauses_l ?S ∝ C ! 0 = L then 0 else 1)›
unfolding i_def by auto
have ‹twl_list_invs ?S›
using add_inv C_N_U unfolding twl_list_invs_def S
by (auto dest: in_diffD)
then have upd_rel: ‹(?S,
set_clauses_to_update (remove1_mset (L, twl_clause_of C') (clauses_to_update S')) S')
∈ {(S, S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S}›
using SS' WS
by (auto simp: twl_st_l_def image_mset_remove1_mset_if)
have D_None: ‹get_conflict_l S = None›
using confl SS' by (cases ‹get_conflict_l S›) (auto simp: S WS'_def')
have [simp]: ‹twl_st_inv (set_conflicting C' (set_clauses_to_update
(remove1_mset LC (clauses_to_update S')) S'))›
if ‹twl_st_inv S'› for S' C' LC
using that
by (cases S') (auto simp: twl_st_inv.simps set_conflicting_def)
have pre: ‹set_conflict_l_pre C (M, N, None, NE, UE, NEk, UEk, NS, US, N0, U0, remove1_mset C WS, Q)›
if ‹M ⊨as CNot (mset (N ∝ C))›
using pre_inv C_N_U dist_C that assms(5)
unfolding set_conflict_l_pre_def unit_propagation_inner_loop_body_l_inv_def apply -
apply normalize_goal+
apply (intro conjI)
apply (auto simp: S true_annots_true_cls twl_list_invs_def dest: consistent_CNot_not_tautology distinct_consistent_interp dest: in_diffD)[6]
apply (rule_tac x=x in exI, rule_tac x = ‹Some L› in exI)
apply (simp add: S)
done
have ‹set_conflict_l C ?S ≤ SPEC twl_list_invs› if ‹M ⊨as CNot (mset (N ∝ C))›
using add_inv C_N_U D_None pre that unfolding twl_list_invs_def
by (auto dest: in_diffD simp: set_conflicting_def S
set_conflict_l_def mset_take_mset_drop_mset' intro!: ASSERT_leI)
then have confl_rel: ‹set_conflict_l C ?S ≤
⇓ {(S, S').
(S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S}
(mop_set_conflicting (twl_clause_of C')
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C')
(clauses_to_update S'))
S'))›
using SS' WS D_None C_N_U pre
by (auto simp: twl_st_l_def image_mset_remove1_mset_if set_conflicting_def S Let_def
set_conflict_l_def mset_take_mset_drop_mset' mop_set_conflicting_def set_conflict_pre_def
intro!: ASSERT_leI ASSERT_refine_right)
have propa_rel:
‹propagate_lit_l K C j
(set_clauses_to_update_l
(remove1_mset C (clauses_to_update_l S)) S)
≤ ⇓ {(S, S').
(S, S') ∈ twl_st_l (Some L) ∧
twl_list_invs S}
(mop_propagate_lit L' (twl_clause_of C')
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C')
(clauses_to_update S'))
S'))›
if
‹(K, L') ∈ Id› and ‹L' ∈ {K. K ∈# remove1_mset L {#L, L'a#}}› and
‹watched (twl_clause_of C') = {#L, L'a#}›
‹(j, j') ∈ {(j, j'). j = i ∧ i < 2}›
for L' K L'a j j'
unfolding S clauses_to_update_l.simps set_clauses_to_update_l.simps
propagate_lit_l_def mop_propagate_lit_def prod.case
proof refine_rcg
assume ‹propagate_lit_pre L' (twl_clause_of C')
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C') (clauses_to_update S'))
S')›
then have L'_undef: ‹- L' ∉ lits_of_l
(get_trail
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C') (clauses_to_update S')) S')) ›
‹L' ∉ lits_of_l
(get_trail
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C') (clauses_to_update S'))
S'))›
unfolding propagate_lit_pre_def Let_def
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l)
show ‹C ∈# dom_m N›
using C_N_U by (auto simp: S)
have [simp]: ‹L' = L'a› ‹K = L'› ‹L'a = (N ∝ C ! (Suc 0 - i))› ‹j = i›
using that two_le_length_C unfolding i_def
by (auto simp: take_2_if S add_mset_eq_add_mset split: if_splits)
have [simp]: ‹mset (swap (N ∝ C) 0 (Suc 0 - i)) = mset (N ∝ C)›
apply (subst swap_multiset)
using two_le_length_C unfolding i_def
by (auto simp: S)
have mset_un_watched_swap:
‹mset (watched_l (swap (N ∝ C) 0 (Suc 0 - i))) = mset (watched_l (N ∝ C))›
‹mset (unwatched_l (swap (N ∝ C) 0 (Suc 0 - i))) = mset (unwatched_l (N ∝ C))›
using two_le_length_C unfolding i_def
apply (auto simp: S take_2_if)
by (auto simp: S swap_def)
have irred_init: ‹irred N C ⟹ (N ∝ C, True) ∈# init_clss_l N›
using C_N_U by (auto simp: S ran_def)
have init_unchanged: ‹{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l (N(C ↪ swap (N ∝ C) 0 (Suc 0 - i)))#} =
{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l N#}›
using C_N_U
by (cases ‹irred N C›) (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
mset_un_watched_swap init_clss_l_mapsto_upd_irrel
dest: multi_member_split[OF irred_init])
have irred_init: ‹¬irred N C ⟹ (N ∝ C, False) ∈# learned_clss_l N›
using C_N_U by (auto simp: S ran_def)
have learned_unchanged: ‹{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# learned_clss_l (N(C ↪ swap (N ∝ C) 0 (Suc 0 - i)))#} =
{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# learned_clss_l N#}›
using C_N_U
by (cases ‹irred N C›) (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
mset_un_watched_swap learned_clss_l_mapsto_upd
learned_clss_l_mapsto_upd_irrel
dest: multi_member_split[OF irred_init])
have [simp]: ‹{#(L, TWL_Clause (mset (watched_l
(fst (the (if C = x
then Some (swap (N ∝ C) 0 (Suc 0 - i), irred N C)
else fmlookup N x)))))
(mset (unwatched_l
(fst (the (if C = x
then Some (swap (N ∝ C) 0 (Suc 0 - i), irred N C)
else fmlookup N x))))))
. x ∈# WS#} = {#(L, TWL_Clause (mset (watched_l (N ∝ x))) (mset (unwatched_l (N ∝ x))))
. x ∈# WS#}›
by (rule image_mset_cong) (auto simp: mset_un_watched_swap)
have C'_0i: ‹C' ! (Suc 0 - i) ∈ set (watched_l C')›
using two_le_length_C by (auto simp: take_2_if S i_def)
have nth_swap_isabelle: ‹length a ≥ 2 ⟹ swap a 0 (Suc 0 - i) ! 0 = a ! (Suc 0 - i)›
for a :: ‹'a list›
using two_le_length_C that apply (auto simp: swap_def S i_def)
by (metis (full_types) le0 neq0_conv not_less_eq_eq nth_list_update_eq numeral_2_eq_2)
have [simp]: ‹Propagated La C ∉ set M› for La
proof (rule ccontr)
assume H:‹¬ ?thesis›
then have ‹La ∈ set (watched_l (N ∝ C))› and
‹2 < length (N ∝ C) ⟶ La = N ∝ C ! 0›
using add_inv C_N_U two_le_length_C mset_un_watched_swap C'_0i
unfolding twl_list_invs_def S by auto
moreover have ‹La ∈ lits_of_l M›
using H by (force simp: lits_of_def)
ultimately show False
using L'_undef that SS' uL_M n_d C'_i S watched_C' two_le_length_C
apply (auto simp: S i_def dest: no_dup_consistentD split: if_splits)
apply (metis in_multiset_nempty member_add_mset no_dup_consistentD set_mset_mset)
by (metis (mono_tags) in_multiset_nempty member_add_mset no_dup_consistentD set_mset_mset)
qed
have ‹twl_list_invs
(Propagated (N ∝ C ! (Suc 0 - i)) C # M, N(C ↪ swap (N ∝ C) 0 (Suc 0 - i)),
D, NE, UE, NEk, UEk, NS, US, N0, U0, remove1_mset C WS, add_mset (- N ∝ C ! (Suc 0 - i)) Q)›
using add_inv C_N_U two_le_length_C mset_un_watched_swap C'_0i
unfolding twl_list_invs_def
by (auto dest: in_diffD simp: set_conflicting_def ran_m_clause_upd
set_conflict_l_def mset_take_mset_drop_mset' S nth_swap_isabelle
dest!: mset_eq_setD)
moreover have
‹convert_lit (N(C ↪ swap (N ∝ C) 0 (Suc 0 - i))) (NEk + UEk)
(Propagated (N ∝ C ! (Suc 0 - i)) C)
(Propagated (N ∝ C ! (Suc 0 - i)) (mset (N ∝ C)))›
by (auto simp: convert_lit.simps C_0)
moreover have ‹(M, x) ∈ convert_lits_l N (NEk + UEk) ⟹
(M, x) ∈ convert_lits_l (N(C ↪ swap (N ∝ C) 0 (Suc 0 - i))) (NEk + UEk)› for x
apply (rule convert_lits_l_extend_mono)
apply assumption
apply auto
done
moreover have
‹convert_lit N (NEk + UEk)
(Propagated (N ∝ C ! (Suc 0 - i)) C)
(Propagated (N ∝ C ! (Suc 0 - i)) (mset (N ∝ C)))›
using C_N_U by (auto simp: S convert_lit.simps C_0)
moreover have ‹twl_list_invs
(Propagated (N ∝ C ! (Suc 0 - i)) C # M, N, D, NE, UE, NEk, UEk,
NS, US, N0, U0, remove1_mset C WS, add_mset (- N ∝ C ! (Suc 0 - i)) Q)›
if ‹¬ 2 < length (N ∝ C)›
using add_inv C_N_U two_le_length_C mset_un_watched_swap C'_0i that
unfolding twl_list_invs_def
by (auto dest: in_diffD simp: set_conflicting_def
set_conflict_l_def mset_take_mset_drop_mset' S nth_swap_isabelle
dest!: mset_eq_setD)
moreover have ‹swap (N ∝ C) 0 (Suc 0) = swap (N ∝ C) i (1 -i)›
using i_def two_le_length_C by (cases ‹N ∝ C›)(auto simp: swap_def)
moreover have ‹i < length (N ∝ C)› ‹i ≤ 1›
using i_def two_le_length_C by (auto simp: S)
moreover have ‹undefined_lit M L'›
using L'_undef SS' by (auto simp: S Decided_Propagated_in_iff_in_lits_of_l)
moreover have ‹N ∝ C ! (Suc 0 - i)
∈# all_lits_of_st_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, remove1_mset C WS, Q)›
using C_N_U two_le_length_C by (auto simp: S ran_m_def all_lits_of_mm_add_mset i_def
all_lits_of_st_l_def
intro!: in_clause_in_all_lits_of_m nth_mem dest!: multi_member_split)
moreover have ‹add_mset L (add_mset (N ∝ C ! (Suc 0 - i)) (mset (unwatched_l (N ∝ C)))) =
mset (N ∝ C)›
apply (subst (4) append_take_drop_id[of 2, symmetric])
using that unfolding mset_append
by (auto simp: S)
ultimately show
‹K ∈# all_lits_of_st_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, remove1_mset C WS, Q)›
‹j ≤ 1›
‹do {
M ← cons_trail_propagate_l K C M;
N ← if 2 < length (N ∝ C)
then mop_clauses_swap N C 0 (Suc 0 - j) else RETURN N;
RETURN
(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, remove1_mset C WS,
add_mset (- K) Q)
} ≤ SPEC(λC.
(C,
(propagate_lit L' (twl_clause_of C')
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C')
(clauses_to_update S'))
S'))) ∈ {(S, S').
(S, S') ∈ twl_st_l (Some L) ∧
twl_list_invs S})›
using SS' WS C_N_U that unfolding propagate_lit_l_def apply (auto simp: S)
by (auto simp: twl_st_l_def image_mset_remove1_mset_if propagate_lit_def
propagate_lit_l_def mset_take_mset_drop_mset' S learned_unchanged mop_clauses_swap_def
cons_trail_propagate_l_def mop_propagate_lit_def
init_unchanged mset_un_watched_swap intro: convert_lit.intros
intro!: ASSERT_leI ASSERT_refine_right)
qed
have update_clause_rel: ‹do {
K' ← mop_clauses_at
(get_clauses_l
(set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S))
S))
C (the K);
val_K ← mop_polarity_l
(set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S) K';
(if val_K = Some True
then RETURN (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S)
else update_clause_l C j (the K) (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S))}
≤ ⇓ {(S, S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S}
(update_clauseS L (twl_clause_of C')
(set_clauses_to_update (remove1_mset (L, twl_clause_of C') (clauses_to_update S')) S'))›
(is ‹?update_clss ≤ ⇓ _ _›)
if
L': ‹L' ∈ {K. K ∈# clause (twl_clause_of C')}› and
K: ‹K ∈ {found. (found = None) =
(∀L∈set (unwatched_l (get_clauses_l ?S ∝ C)).
- L ∈ lits_of_l (get_trail_l ?S)) ∧
(∀j. found = Some j ⟶
j < length (get_clauses_l ?S ∝ C) ∧
(undefined_lit (get_trail_l ?S) (get_clauses_l ?S ∝ C ! j) ∨
get_clauses_l ?S ∝ C ! j ∈ lits_of_l (get_trail_l ?S)) ∧
2 ≤ j)}› and
K_None: ‹K ≠ None› and
‹watched (twl_clause_of C') = {#L, L'a#}› and
val: ‹(val_L', False) ∈ pol_spec L'a› and
‹(j, j') ∈ {(j, j'). j = i ∧ i < 2}›
for L' and K and L'a and j j' and val_L'
proof -
have L'a: ‹L'a
∉ lits_of_l
(get_trail
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C') (clauses_to_update S')) S'))›
using n_d val SS' by (auto simp: pol_spec_def dest: no_dup_consistentD)
have [simp]: ‹j = i›
using that by auto
obtain K' where [simp]: ‹K = Some K'›
using K_None by auto
have
K'_le: ‹K' < length (N ∝ C)› and
K'_2: ‹2 ≤ K'› and
K'_M: ‹undefined_lit M (N ∝ C ! K') ∨
N ∝ C ! K' ∈ lits_of_l (get_trail_l S) ›
using K by (auto simp: S)
have [simp]: ‹N ∝ C ! K' ∈ set (unwatched_l (N ∝ C))›
using K'_le K'_2 by (auto simp: set_drop_conv S)
have [simp]: ‹- N ∝ C ! K' ∉ lits_of_l M ›
using n_d K'_M by (auto simp: S Decided_Propagated_in_iff_in_lits_of_l
dest: no_dup_consistentD)
have irred_init: ‹irred N C ⟹ (N ∝ C, True) ∈# init_clss_l N›
using C_N_U by (auto simp: S)
have init_unchanged: ‹update_clauses
({#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l N#},
{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# learned_clss_l N#})
(TWL_Clause (mset (watched_l (N ∝ C))) (mset (unwatched_l (N ∝ C)))) L
(N ∝ C ! K')
({#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l (N(C ↪ swap (N ∝ C) i K'))#},
{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# learned_clss_l (N(C ↪ swap (N ∝ C) i K'))#})›
proof (cases ‹irred N C›)
case J_NE: True
have L_L'_UW_N: ‹C' ∈# init_clss_lf N›
using C_N_U J_NE unfolding take_set
by (auto simp: S ran_m_def)
let ?UW = ‹unwatched_l C'›
have TWL_L_L'_UW_N: ‹TWL_Clause {#?L, ?L'#} (mset ?UW) ∈# twl_clause_of `# init_clss_lf N›
using imageI[OF L_L'_UW_N, of twl_clause_of] watched_C' by force
let ?k' = ‹the K - 2›
have ‹?k' < length (unwatched_l C')›
using K'_le two_le_length_C K'_2 by (auto simp: S)
then have H0: ‹TWL_Clause {#?UW ! ?k', ?L'#} (mset (list_update ?UW ?k' ?L)) =
update_clause (TWL_Clause {#?L, ?L'#} (mset ?UW)) ?L (?UW ! ?k')›
by (auto simp: mset_update)
have H3: ‹{#L, C' ! (Suc 0 - i)#} = mset (watched_l (N ∝ C))›
using K'_2 K'_le ‹C > 0› C'_i by (auto simp: S take_2_if C_N_U nth_tl i_def)
have H4: ‹mset (unwatched_l C') = mset (unwatched_l (N ∝ C))›
by (auto simp: S take_2_if C_N_U nth_tl)
let ?New_C = ‹(TWL_Clause {#L, C' ! (Suc 0 - i)#} (mset (unwatched_l C')))›
have wo: "a = a' ⟹ b = b' ⟹ L = L' ⟹ K = K' ⟹ c = c' ⟹
update_clauses a K L b c ⟹
update_clauses a' K' L' b' c'" for a a' b b' K L K' L' c c'
by auto
have [simp]: ‹C' ∈ fst ` {a. a ∈# ran_m N ∧ snd a} ⟷ irred N C›
using C_N_U J_NE unfolding C' S ran_m_def
by auto
have C'_ran_N: ‹(C', True) ∈# ran_m N›
using C_N_U J_NE unfolding C' S S
by auto
have upd: ‹update_clauses
(twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N)
(TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#} (mset (unwatched_l C'))) (C' ! i) (C' ! the K)
(add_mset (update_clause (TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#}
(mset (unwatched_l C'))) (C' ! i) (C' ! the K))
(remove1_mset
(TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#} (mset (unwatched_l C')))
(twl_clause_of `# init_clss_lf N)), twl_clause_of `# learned_clss_lf N)›
by (rule update_clauses.intros(1)[OF TWL_L_L'_UW_N])
have K1: ‹mset (watched_l (swap (N∝C) i K')) = {#N∝C!K', N∝C!(1 - i)#}›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
take_2_if swap_def i_def)
have K2: ‹mset (unwatched_l (swap (N∝C) i K')) = add_mset (N∝C ! i)
(remove1_mset (N∝C ! K') (mset (unwatched_l (N∝C))))›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if mset_update
take_2_if swap_def i_def drop_upd_irrelevant drop_Suc drop_update_swap)
have K3: ‹mset (watched_l (N∝C)) = {#N∝C!i, N∝C!(1 - i)#}›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
take_2_if swap_def i_def)
show ?thesis
apply (rule wo[OF _ _ _ _ _ upd])
subgoal by auto
subgoal by (auto simp: S)
subgoal by auto
subgoal unfolding S H3[symmetric] H4[symmetric] by auto
subgoal
using J_NE C_N_U C' K'_2 K'_le two_le_length_C K1 K2 K3 C'_ran_N
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
learned_clss_l_mapsto_upd_irrel)
done
next
assume J_NE: ‹¬irred N C›
have L_L'_UW_N: ‹C' ∈# learned_clss_lf N›
using C_N_U J_NE unfolding take_set
by (auto simp: S ran_m_def)
let ?UW = ‹unwatched_l C'›
have TWL_L_L'_UW_N: ‹TWL_Clause {#?L, ?L'#} (mset ?UW) ∈# twl_clause_of `# learned_clss_lf N›
using imageI[OF L_L'_UW_N, of twl_clause_of] watched_C' by force
let ?k' = ‹the K - 2›
have ‹?k' < length (unwatched_l C')›
using K'_le two_le_length_C K'_2 by (auto simp: S)
then have H0: ‹TWL_Clause {#?UW ! ?k', ?L'#} (mset (list_update ?UW ?k' ?L)) =
update_clause (TWL_Clause {#?L, ?L'#} (mset ?UW)) ?L (?UW ! ?k')›
by (auto simp: mset_update)
have H3: ‹{#L, C' ! (Suc 0 - i)#} = mset (watched_l (N ∝ C))›
using K'_2 K'_le ‹C > 0› C'_i by (auto simp: S take_2_if C_N_U nth_tl i_def)
have H4: ‹mset (unwatched_l C') = mset (unwatched_l (N ∝ C))›
by (auto simp: S take_2_if C_N_U nth_tl)
let ?New_C = ‹(TWL_Clause {#L, C' ! (Suc 0 - i)#} (mset (unwatched_l C')))›
have wo: "a = a' ⟹ b = b' ⟹ L = L' ⟹ K = K' ⟹ c = c' ⟹
update_clauses a K L b c ⟹
update_clauses a' K' L' b' c'" for a a' b b' K L K' L' c c'
by auto
have [simp]: ‹C' ∈ fst ` {a. a ∈# ran_m N ∧ ¬snd a} ⟷ ¬irred N C›
using C_N_U J_NE unfolding C' S ran_m_def
by auto
have C'_ran_N: ‹(C', False) ∈# ran_m N›
using C_N_U J_NE unfolding C' S S
by auto
have upd: ‹update_clauses
(twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N)
(TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#} (mset (unwatched_l C'))) (C' ! i)
(C' ! the K)
(twl_clause_of `# init_clss_lf N,
add_mset
(update_clause
(TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#} (mset (unwatched_l C'))) (C' ! i)
(C' ! the K))
(remove1_mset
(TWL_Clause {#C' ! i, C' ! (Suc 0 - i)#} (mset (unwatched_l C')))
(twl_clause_of `# learned_clss_lf N)))
›
by (rule update_clauses.intros(2)[OF TWL_L_L'_UW_N])
have K1: ‹mset (watched_l (swap (N∝C) i K')) = {#N∝C!K', N∝C!(1 - i)#}›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
take_2_if swap_def i_def)
have K2: ‹mset (unwatched_l (swap (N∝C) i K')) = add_mset (N∝C ! i)
(remove1_mset (N∝C ! K') (mset (unwatched_l (N∝C))))›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if mset_update
take_2_if swap_def i_def drop_upd_irrelevant drop_Suc drop_update_swap)
have K3: ‹mset (watched_l (N∝C)) = {#N∝C!i, N∝C!(1 - i)#}›
using J_NE C_N_U C' K'_2 K'_le two_le_length_C
by (auto simp: init_clss_l_mapsto_upd S image_mset_remove1_mset_if
take_2_if swap_def i_def)
show ?thesis
apply (rule wo[OF _ _ _ _ _ upd])
subgoal by auto
subgoal by (auto simp: S)
subgoal by auto
subgoal unfolding S H3[symmetric] H4[symmetric] by auto
subgoal
using J_NE C_N_U C' K'_2 K'_le two_le_length_C K1 K2 K3 C'_ran_N
by (auto simp: learned_clss_l_mapsto_upd S image_mset_remove1_mset_if
init_clss_l_mapsto_upd_irrel)
done
qed
have ‹distinct_mset WS›
by (metis (full_types) WS'_def WS'_def' add_inv twl_list_invs_def)
then have [simp]: ‹C ∉# WS'›
by (auto simp: WS'_def')
have H: ‹{#(L, TWL_Clause
(mset (watched_l
(fst (the (if C = x then Some (swap (N ∝ C) i K', irred N C)
else fmlookup N x)))))
(mset (unwatched_l
(fst (the (if C = x then Some (swap (N ∝ C) i K', irred N C)
else fmlookup N x)))))). x ∈# WS'#} =
{#(L, TWL_Clause (mset (watched_l (N ∝ x))) (mset (unwatched_l (N ∝ x)))). x ∈# WS'#}›
by (rule image_mset_cong) auto
have [simp]: ‹Propagated La C ∉ set M› for La
proof (rule ccontr)
assume H:‹¬ ?thesis›
then have ‹length (N ∝ C) > 2 ⟹ La = N ∝ C ! 0› and
‹La ∈ set (watched_l (N ∝ C))›
using add_inv C_N_U two_le_length_C
unfolding twl_list_invs_def S by auto
moreover have ‹La ∈ lits_of_l M›
using H by (force simp: lits_of_def)
ultimately show False
using SS' uL_M n_d K'_2 K'_le two_le_length_C arg_cong[OF that(4), of set_mset] L'a
by (auto simp: S i_def polarity_spec' dest: no_dup_consistentD split: if_splits)
qed
have A: ‹?update_clss = do {x ← mop_clauses_at N C K';
if x ∈ lits_of_l (get_trail_l (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S))
then RETURN (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S)
else update_clause_l C i
(the K) (set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S)}›
using C_N_U K'_le n_d unfolding i_def
by (auto simp add: S i_def polarity_def mop_clauses_at_def mop_polarity_l_def all_lits_of_st_l_def
ran_m_def all_lits_of_mm_add_mset in_clause_in_all_lits_of_m dest!: multi_member_split[of C]
dest: in_lits_of_l_defined_litD)
have alt_defs: ‹C' = N ∝ C›
unfolding C' S by auto
have list_invs_blit: ‹twl_list_invs (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS', Q)›
using add_inv C_N_U two_le_length_C
unfolding twl_list_invs_def
by (auto dest: in_diffD simp: S WS'_def')
define pick_lit where
‹pick_lit a = SPEC (λL. L ∈# unwatched (twl_clause_of C') ∧ - L ∉ lits_of_l a)›
for a :: ‹('v, 'v clause) ann_lit list›
have [refine]:
‹a = get_trail S' ⟹ mop_clauses_at N C K' ≤ ⇓ {(L, L'). L = L' ∧ L' = op_clauses_at N C K'} (pick_lit a)› for a
using C_N_U K'_le K'_M n_d SS' unfolding C' S by (auto simp: mop_clauses_at_def twl_st_l_def pick_lit_def
RETURN_RES_refine_iff S op_clauses_at_def)
have ‹twl_list_invs (M, N(C ↪ swap (N ∝ C) i K'), D, NE, UE, NEk, UEk, NS, US, N0, U0, WS', Q)›
using add_inv C_N_U two_le_length_C i_le_length_C K'_le
unfolding twl_list_invs_def
by (auto dest: in_diffD simp: set_conflicting_def ran_m_clause_upd
set_conflict_l_def mset_take_mset_drop_mset' S WS'_def'
dest!: mset_eq_setD)
moreover have ‹(M, x) ∈ convert_lits_l N (NEk + UEk) ⟹
(M, x) ∈ convert_lits_l (N(C ↪ swap (N ∝ C) i K')) (NEk + UEk)› for x
apply (rule convert_lits_l_extend_mono)
by auto
ultimately show ?thesis
apply (cases S')
unfolding update_clauseS_def unfolding pick_lit_def[symmetric]
apply (clarsimp simp only: clauses_to_update.simps set_clauses_to_update.simps)
apply (subst A)
apply refine_vcg
subgoal using C_N_U K'_le K'_M n_d SS' unfolding C' S by (auto simp: mop_clauses_at_def twl_st_l_def)
subgoal using SS' K'_M unfolding C' S by (auto simp: twl_st_l_def)
subgoal using SS' K'_M add_inv list_invs_blit unfolding C' S
by (auto simp: twl_st_l_def WS'_def')
subgoal for a b c d e f g h x Ka
using SS' init_unchanged C_N_U i_le_length_C K'_le C'_i
unfolding i_def[symmetric] get_clauses_l_set_clauses_to_update_l
unfolding update_clause_l_pre_def
by (auto simp: S update_clause_l_def update_clauseS_def twl_st_l_def WS'_def'
RETURN_SPEC_refine RES_RES_RETURN_RES RETURN_def RES_RES2_RETURN_RES H
mop_clauses_swap_def op_clauses_at_def WS'_def' update_clause_l_pre_def
all_lits_of_st_l_def
intro!: RES_refine exI[of _ ‹N ∝ C ! the K›] ASSERT_leI
exI[of _ ‹set_clauses_to_update (remove1_mset (L, twl_clause_of (N ∝ C))
(clauses_to_update S')) S'›] exI[of _ L] image_mset_cong)
done
qed
have pos_of_watched: ‹unit_propagation_inner_loop_body_l_inv L C
(set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S) ⟹ pos_of_watched
(get_clauses_l
(set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S))
C L
≤ SPEC (λc. (c, ()) ∈ {(j, j'). j = i ∧ i < 2})›
unfolding pos_of_watched_def
by (auto simp: S unit_propagation_inner_loop_body_l_inv_def i_def
intro!: ASSERT_leI)
have [refine]: ‹unit_propagation_inner_loop_body_l_inv L C
(set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S) ⟹
(K, bL') ∈ Id ⟹
bL' ∈ { K. K∈# clause (twl_clause_of C')} ⟹
mop_polarity_l
(set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S)
K
≤ SPEC
(λ c. (c, bL'
∈ lits_of_l
(get_trail
(set_clauses_to_update
(remove1_mset (L, twl_clause_of C')
(clauses_to_update S'))
S')))
∈ pol_spec bL')› for bL' K
using assms n_d L C_N_U consistent unfolding pol_spec_def
by (auto simp: mop_polarity_l_def polarity_def ran_m_def all_lits_of_mm_add_mset
all_lits_of_st_l_def
true_annot_iff_decided_or_true_lit dest!: in_set_takeD in_set_dropD
dest!: multi_member_split[of C ‹dom_m (get_clauses_l S)›]
intro!: ASSERT_leI intro!: in_clause_in_all_lits_of_m)
have I: ‹(x, ()) ∈ {_. True}› for x
by auto
have L_i0: ‹L = get_clauses_l S ∝ C ! 0 ⟹ Suc 0 - i = Suc 0›
by (auto simp: i_def)
have other_watched_l: ‹(i', ia) ∈ {(j, j'). j = i ∧ i < 2} ⟹
other_watched_l
(set_clauses_to_update_l (remove1_mset C (clauses_to_update_l S)) S) L
C i'
≤ SPEC (λK. K ∈# remove1_mset L (watched (twl_clause_of C')))› for i' ia
unfolding other_watched_l_def
by (refine_vcg mop_clauses_at[THEN fref_to_Down_curry2, unfolded comp_def, THEN order_trans])
(use mset_watched_C pre_inv in ‹auto simp: op_clauses_at_def C_N_U
unit_propagation_inner_loop_body_l_inv_def L_i0
intro!: ASSERT_leI split: if_splits
intro!: mop_clauses_at[THEN fref_to_Down_curry2, unfolded comp_def, THEN order_trans]
simp: other_watched_l_def›)
have H: ‹?A ≤ ⇓ {(S, S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S} ?B›
unfolding unit_propagation_inner_loop_body_l_def unit_propagation_inner_loop_body_alt_def
option.case_eq_if find_unwatched_l_def op_clauses_at_def[symmetric]
nres_monad3
apply (refine_vcg pos_of_watched
case_prod_bind[of _ ‹If _ _›]; remove_dummy_vars)
subgoal by (rule pre_inv)
subgoal unfolding C' clause_twl_clause_of by auto
subgoal using SS' by (auto simp: pol_spec_def)
subgoal by (rule upd_rel)
subgoal
by (rule other_watched_l)
subgoal for L'
using assms by (auto simp: pol_spec_def)
subgoal by (rule upd_rel)
subgoal using SS' C_N_U by auto
subgoal using SS' C_N_U two_le_length_C by auto
subgoal using SS' C_N_U dist_C by auto
subgoal using SS' C_N_U dist_C n_d by auto
subgoal using SS' by auto
subgoal using SS' by (auto simp: pol_spec_def)
subgoal by (rule confl_rel)
subgoal for K bL' j j' L' L'a2 L'a3 unfolding i_def[symmetric] op_clauses_at_def i_def'[symmetric]
by (rule propa_rel)
subgoal by auto
subgoal for L' K unfolding i_def[symmetric] i_def'[symmetric] op_clauses_at_def Let_def
by (rule update_clause_rel)
done
have *: ‹unit_propagation_inner_loop_body (C' ! i) (twl_clause_of C')
(set_clauses_to_update (remove1_mset (C' ! i, twl_clause_of C') (clauses_to_update S')) S')
≤ SPEC (λS''. twl_struct_invs S'' ∧
twl_stgy_invs S'' ∧
cdcl_twl_cp⇧*⇧* S' S'' ∧
(S'', S') ∈ measure (size ∘ clauses_to_update))›
apply (rule unit_propagation_inner_loop_body(1)[of S' ‹C' ! i› ‹twl_clause_of C'›])
using imageI[OF WS, of ‹(λj. (L, twl_clause_of (N ∝ j)))›]
struct_invs stgy_inv C_N_U WS SS' D_None by auto
have H': ‹?B ≤ SPEC (λS'. twl_stgy_invs S' ∧ twl_struct_invs S')›
using *
by (simp add: weaken_SPEC)
have ‹?A
≤ ⇓ {(S, S'). ((S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S) ∧
(twl_stgy_invs S' ∧ twl_struct_invs S')}
?B›
apply (rule refine_add_invariants)
apply (rule H')
by (rule H)
then show ?thesis by simp
qed
lemma unit_propagation_inner_loop_body_l2:
assumes
SS': ‹(S, S') ∈ twl_st_l (Some L)› and
WS: ‹C ∈# clauses_to_update_l S› and
struct_invs: ‹twl_struct_invs S'› and
add_inv: ‹twl_list_invs S› and
stgy_inv: ‹twl_stgy_invs S'›
shows
‹(unit_propagation_inner_loop_body_l L C
(set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S),
unit_propagation_inner_loop_body L (twl_clause_of (get_clauses_l S ∝ C))
(set_clauses_to_update
(remove1_mset (L, twl_clause_of (get_clauses_l S ∝ C))
(clauses_to_update S')) S'))
∈ ⟨{(S, S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S ∧ twl_stgy_invs S' ∧
twl_struct_invs S'}⟩nres_rel›
using unit_propagation_inner_loop_body_l[OF assms]
by (auto simp: nres_rel_def)
text ‹This a work around equality: it allows to instantiate variables that appear in goals by
hand in a reasonable way (\<^text>‹rule\_tac I=x in EQI)›.›
definition EQ where
[simp]: ‹EQ = (=)›
lemma EQI: "EQ I I"
by auto
lemma unit_propagation_inner_loop_body_l_unit_propagation_inner_loop_body:
‹EQ L'' L'' ⟹
(uncurry2 unit_propagation_inner_loop_body_l, uncurry2 unit_propagation_inner_loop_body) ∈
{(((L, C), S0), ((L', C'), S0')). ∃S S'. L = L' ∧ C' = (twl_clause_of (get_clauses_l S ∝ C)) ∧
S0 = (set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S) ∧
S0' = (set_clauses_to_update
(remove1_mset (L, twl_clause_of (get_clauses_l S ∝ C))
(clauses_to_update S')) S') ∧
(S, S') ∈ twl_st_l (Some L) ∧ L = L'' ∧
C ∈# clauses_to_update_l S ∧ twl_struct_invs S' ∧ twl_list_invs S ∧ twl_stgy_invs S'} →⇩f
⟨{(S, S'). (S, S') ∈ twl_st_l (Some L'') ∧ twl_list_invs S ∧ twl_stgy_invs S' ∧
twl_struct_invs S'}⟩nres_rel›
apply (intro frefI nres_relI)
using unit_propagation_inner_loop_body_l
by fastforce
definition select_from_clauses_to_update :: ‹'v twl_st_l ⇒ ('v twl_st_l × nat) nres› where
‹select_from_clauses_to_update S = SPEC (λ(S', C). C ∈# clauses_to_update_l S ∧
S' = set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S)›
definition unit_propagation_inner_loop_l_inv where
‹unit_propagation_inner_loop_l_inv L = (λ(S, n).
(∃S'. (S, S') ∈ twl_st_l (Some L) ∧ twl_struct_invs S' ∧ twl_stgy_invs S' ∧
twl_list_invs S ∧ (clauses_to_update S' ≠ {#} ∨ n > 0 ⟶ get_conflict S' = None) ∧
-L ∈ lits_of_l (get_trail_l S)))›
definition unit_propagation_inner_loop_body_l_with_skip where
‹unit_propagation_inner_loop_body_l_with_skip L = (λ(S, n). do {
ASSERT (clauses_to_update_l S ≠ {#} ∨ n > 0);
ASSERT(unit_propagation_inner_loop_l_inv L (S, n));
b ← SPEC(λb. (b ⟶ n > 0) ∧ (¬b ⟶ clauses_to_update_l S ≠ {#}));
if ¬b then do {
ASSERT (clauses_to_update_l S ≠ {#});
(S', C) ← select_from_clauses_to_update S;
T ← unit_propagation_inner_loop_body_l L C S';
RETURN (T, if get_conflict_l T = None then n else 0)
} else RETURN (S, n-1)
})›
definition unit_propagation_inner_loop_l :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹unit_propagation_inner_loop_l L S⇩0 = do {
ASSERT(L ∈# all_lits_of_st_l S⇩0);
n ← SPEC(λ_::nat. True);
(S, n) ← WHILE⇩T⇗unit_propagation_inner_loop_l_inv L⇖
(λ(S, n). clauses_to_update_l S ≠ {#} ∨ n > 0)
(unit_propagation_inner_loop_body_l_with_skip L)
(S⇩0, n);
RETURN S
}›
lemma set_mset_clauses_to_update_l_set_mset_clauses_to_update_spec:
assumes ‹(S, S') ∈ twl_st_l (Some L)›
shows
‹RES (set_mset (clauses_to_update_l S)) ≤ ⇓ {(C, (L', C')). L' = L ∧
C' = twl_clause_of (get_clauses_l S ∝ C)}
(RES (set_mset (clauses_to_update S')))›
proof -
obtain M N D NE UE WS Q where
S: ‹S = (M, N, D, NE, UE, WS, Q)›
by (cases S) auto
show ?thesis
using assms unfolding S by (auto simp add: Bex_def twl_st_l_def intro!: RES_refine)
qed
lemma clauses_to_update_l_empty_tw_st_of_Some_None[simp]:
‹clauses_to_update_l S = {#} ⟹ (S, S')∈ twl_st_l (Some L) ⟷ (S, S') ∈ twl_st_l None›
by (cases S) (auto simp: twl_st_l_def)
lemma cdcl_twl_cp_in_trail_stays_in:
‹cdcl_twl_cp⇧*⇧* S' aa ⟹ - x1 ∈ lits_of_l (get_trail S') ⟹ - x1 ∈ lits_of_l (get_trail aa)›
by (induction rule: rtranclp_induct)
(auto elim!: cdcl_twl_cpE)
lemma cdcl_twl_cp_in_trail_stays_in_l:
‹(x2, S') ∈ twl_st_l (Some x1) ⟹ cdcl_twl_cp⇧*⇧* S' aa ⟹ - x1 ∈ lits_of_l (get_trail_l x2) ⟹
(a, aa) ∈ twl_st_l (Some x1) ⟹ - x1 ∈ lits_of_l (get_trail_l a)›
using cdcl_twl_cp_in_trail_stays_in[of S' aa ‹x1›]
by (auto simp: twl_st twl_st_l)
lemma unit_propagation_inner_loop_l:
‹(uncurry unit_propagation_inner_loop_l, unit_propagation_inner_loop) ∈
{((L, S), S'). (S, S') ∈ twl_st_l (Some L) ∧ twl_list_invs S ∧ -L ∈ lits_of_l (get_trail_l S) ∧
L ∈# all_lits_of_st_l S} →⇩f
⟨{(T, T'). (T, T') ∈ twl_st_l None ∧ clauses_to_update_l T = {#} ∧
twl_list_invs T}⟩ nres_rel›
(is ‹?unit_prop_inner ∈ ?A →⇩f ⟨?B⟩nres_rel›)
proof -
have SPEC_remove: ‹select_from_clauses_to_update S
≤ ⇓ {((T', C), C').
(T', set_clauses_to_update (clauses_to_update S'' - {#C'#}) S'') ∈ twl_st_l (Some L) ∧
T' = set_clauses_to_update_l (clauses_to_update_l S - {#C#}) S ∧
C' ∈# clauses_to_update S'' ∧
C ∈# clauses_to_update_l S ∧
snd C' = twl_clause_of (get_clauses_l S ∝ C)}
(SPEC (λC. C ∈# clauses_to_update S''))›
if ‹(S, S'') ∈ {(T, T'). (T, T') ∈ twl_st_l (Some L) ∧ twl_list_invs T}›
for S :: ‹'v twl_st_l› and S'' L
using that unfolding select_from_clauses_to_update_def
by (auto simp: conc_fun_def image_mset_remove1_mset_if twl_st_l_def)
show ?thesis
unfolding unit_propagation_inner_loop_l_def unit_propagation_inner_loop_def uncurry_def
unit_propagation_inner_loop_body_l_with_skip_def
apply (intro frefI nres_relI)
subgoal for LS S'
apply (rewrite in ‹let _ = set_clauses_to_update _ _ in _› Let_def)
apply (refine_vcg set_mset_clauses_to_update_l_set_mset_clauses_to_update_spec
WHILEIT_refine_genR[where
R = ‹{(T, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T ∧ clauses_to_update_l T = {#}}
×⇩f nat_rel› and
R' = ‹{(T, T'). (T, T') ∈ twl_st_l (Some (fst LS)) ∧ twl_list_invs T}
×⇩f nat_rel›]
unit_propagation_inner_loop_body_l_unit_propagation_inner_loop_body[THEN fref_to_Down_curry2]
SPEC_remove;
remove_dummy_vars)
subgoal for x1 x2
by (auto simp add: in_all_lits_of_mm_uminus_iff twl_st_l
mset_take_mset_drop_mset')
subgoal by simp
subgoal for x1 x2 n na x x' unfolding unit_propagation_inner_loop_l_inv_def
apply (case_tac x; case_tac x')
apply (simp only: prod.simps)
by (rule exI[of _ ‹fst x'›]) (auto intro: cdcl_twl_cp_in_trail_stays_in_l)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply (subst (asm) prod_rel_iff)
apply normalize_goal
apply assumption
apply (rule_tac I=x1 in EQI)
subgoal for x1 x2 n na x1a x2a x1b x2b b ba x1c x2c x1d x2d
apply (subst in_pair_collect_simp)
apply (subst prod.case)+
apply (rule_tac x = x1b in exI)
apply (rule_tac x = x1a in exI)
apply (intro conjI)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
done
qed
definition clause_to_update :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v clauses_to_update_l›where
‹clause_to_update L S =
filter_mset
(λC::nat. L ∈ set (watched_l (get_clauses_l S ∝ C)))
(dom_m (get_clauses_l S))›
lemma distinct_mset_clause_to_update: ‹distinct_mset (clause_to_update L C)›
unfolding clause_to_update_def
apply (rule distinct_mset_filter)
using distinct_mset_dom by blast
lemma in_clause_to_updateD: ‹b ∈# clause_to_update L' T ⟹ b ∈# dom_m (get_clauses_l T)›
by (auto simp: clause_to_update_def)
lemma in_clause_to_update_iff:
‹C ∈# clause_to_update L S ⟷
C ∈# dom_m (get_clauses_l S) ∧ L ∈ set (watched_l (get_clauses_l S ∝ C))›
by (auto simp: clause_to_update_def)
definition select_and_remove_from_literals_to_update :: ‹'v twl_st_l ⇒
('v twl_st_l × 'v literal) nres› where
‹select_and_remove_from_literals_to_update S = SPEC(λ(S', L). L ∈# literals_to_update_l S ∧
S' = set_clauses_to_update_l (clause_to_update L S)
(set_literals_to_update_l (literals_to_update_l S - {#L#}) S))›
definition unit_propagation_outer_loop_l_inv where
‹unit_propagation_outer_loop_l_inv S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧ twl_struct_invs S' ∧ twl_stgy_invs S' ∧
clauses_to_update_l S = {#})›
definition unit_propagation_outer_loop_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹unit_propagation_outer_loop_l S⇩0 =
WHILE⇩T⇗unit_propagation_outer_loop_l_inv⇖
(λS. literals_to_update_l S ≠ {#})
(λS. do {
ASSERT(literals_to_update_l S ≠ {#});
(S', L) ← select_and_remove_from_literals_to_update S;
unit_propagation_inner_loop_l L S'
})
(S⇩0 :: 'v twl_st_l)
›
lemma watched_twl_clause_of_watched: ‹watched (twl_clause_of x) = mset (watched_l x)›
by (cases x) auto
lemma twl_st_of_clause_to_update:
assumes
TT': ‹(T, T') ∈ twl_st_l None› and
‹twl_struct_invs T'›
shows
‹(set_clauses_to_update_l
(clause_to_update L' T)
(set_literals_to_update_l (remove1_mset L' (literals_to_update_l T)) T),
set_clauses_to_update
(Pair L' `# {#C ∈# get_clauses T'. L' ∈# watched C#})
(set_literals_to_update (remove1_mset L' (literals_to_update T'))
T'))
∈ twl_st_l (Some L')›
proof -
obtain M N D NE UE NEk UEk NS US N0 U0 WS Q where
T: ‹T = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)›
by (cases T) auto
have
‹{#(L', TWL_Clause (mset (watched_l (N ∝ x)))
(mset (unwatched_l (N ∝ x)))).
x ∈# {#C ∈# dom_m N. L' ∈ set (watched_l (N ∝ C))#}#} =
Pair L' `#
{#C ∈# {#TWL_Clause (mset (watched_l x)) (mset (unwatched_l x)). x ∈# init_clss_lf N#} +
{#TWL_Clause (mset (watched_l x)) (mset (unwatched_l x)). x ∈# learned_clss_lf N#}.
L' ∈# watched C#}›
(is ‹{#(L', ?C x). x ∈# ?S#} = Pair L' `# ?C'›)
proof -
have H: ‹{#f (N ∝ x). x ∈# {#x ∈# dom_m N. P (N ∝ x)#}#} =
{#f (fst x). x ∈# {#C ∈# ran_m N. P (fst C)#}#}› for P and f :: ‹'a literal list ⇒ 'b›
unfolding ran_m_def image_mset_filter_swap2 by auto
have H: ‹{#f (N∝x). x ∈# ?S#} =
{#f (fst x). x ∈# {#C ∈# init_clss_l N. L' ∈ set (watched_l (fst C))#}#} +
{#f (fst x). x ∈# {#C ∈# learned_clss_l N. L' ∈ set (watched_l (fst C))#}#}›
for f :: ‹'a literal list ⇒ 'b›
unfolding image_mset_union[symmetric] filter_union_mset[symmetric]
apply auto
apply (subst H)
..
have L'': ‹{#(L', ?C x). x ∈# ?S#} = Pair L' `# {#?C x. x ∈# ?S#}›
by auto
also have ‹… = Pair L' `# ?C'›
apply (rule arg_cong[of _ _ ‹(`#) (Pair L')›])
unfolding image_mset_union[symmetric] mset_append[symmetric] drop_Suc H
apply simp
apply (subst H)
unfolding image_mset_union[symmetric] mset_append[symmetric] drop_Suc H
filter_union_mset[symmetric] image_mset_filter_swap2
by auto
finally show ?thesis .
qed
then show ?thesis
using TT'
by (cases T') (auto simp del: filter_union_mset
simp: T split_beta clause_to_update_def twl_st_l_def
split: if_splits)
qed
lemma twl_list_invs_set_clauses_to_update_iff:
assumes ‹twl_list_invs T›
shows ‹twl_list_invs (set_clauses_to_update_l WS (set_literals_to_update_l Q T)) ⟷
((∀x∈#WS. case x of C ⇒ C ∈# dom_m (get_clauses_l T)) ∧
distinct_mset WS)›
proof -
obtain M N C NE UE NEk UEk WS NS US N0 U0 Q where
T: ‹T = (M, N, C, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q)›
by (cases T) auto
show ?thesis
using assms
unfolding twl_list_invs_def T by auto
qed
lemma unit_propagation_outer_loop_l_spec:
‹(unit_propagation_outer_loop_l, unit_propagation_outer_loop) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →⇩f
⟨{(S, S').
(S, S') ∈ twl_st_l None ∧
clauses_to_update_l S = {#} ∧
twl_list_invs S}⟩ nres_rel›
(is ‹_ ∈ ?R →⇩f ?I› is ‹_ ∈ _ →⇩f ⟨?B⟩ nres_rel›)
proof -
have twl_struct_invs_no_alien_in_trail: ‹unit_propagation_outer_loop_l_inv T ⟹
-x2a ∈ lits_of_l (get_trail_l T) ⟹
x2a ∈# all_lits_of_st_l T› for T x2a
unfolding unit_propagation_outer_loop_l_inv_def
apply normalize_goal+
by (drule twl_struct_invs_no_alien_in_trail[of _ ‹-x2a›])
(simp_all add: mset_take_mset_drop_mset' in_all_lits_of_mm_uminus_iff)
have H:
‹select_and_remove_from_literals_to_update x
≤ ⇓ {((S', L'), (L, S)). L = L' ∧ S' = set_clauses_to_update_l (clause_to_update L x)
(set_literals_to_update_l (remove1_mset L (literals_to_update_l x)) x) ∧
L' ∈# literals_to_update_l x ∧
S = set_clauses_to_update {#(L, C)|C ∈# get_clauses x'. L ∈# watched C#}
(set_literals_to_update (literals_to_update x' - {#L#}) x')}
(mop_pop_literal_to_update x')›
if ‹(x, x') ∈ twl_st_l None› for x :: ‹'v twl_st_l› and x' :: ‹'v twl_st›
using that unfolding select_and_remove_from_literals_to_update_def mop_pop_literal_to_update_def
Let_def RES_RETURN_RES
apply (cases x; cases x')
apply refine_rcg
by (clarsimp simp add: twl_st_l_def intro!: RES_refine)
have H': ‹unit_propagation_outer_loop_l_inv T ⟹
x2 ∈# literals_to_update_l T ⟹ - x2 ∈ lits_of_l (get_trail_l T)›
for S S' T T' L L' C x2
by (auto simp: unit_propagation_outer_loop_l_inv_def twl_st_l_def twl_struct_invs_def)
show H:
‹(unit_propagation_outer_loop_l, unit_propagation_outer_loop) ∈?R →⇩f
⟨{(S, S').
(S, S') ∈ twl_st_l None ∧
clauses_to_update_l S = {#} ∧
twl_list_invs S}⟩ nres_rel›
unfolding unit_propagation_outer_loop_l_def unit_propagation_outer_loop_def fref_param1[symmetric]
apply (refine_vcg unit_propagation_inner_loop_l[THEN fref_to_Down_curry_left]
H)
subgoal by simp
subgoal unfolding unit_propagation_outer_loop_l_inv_def by fastforce
subgoal by auto
subgoal by simp
subgoal for S S' T T' L L' C x2
by (auto simp add: twl_st_of_clause_to_update twl_list_invs_set_clauses_to_update_iff
intro: cdcl_twl_cp_twl_struct_invs cdcl_twl_cp_twl_stgy_invs
distinct_mset_clause_to_update H'
dest: in_clause_to_updateD)
subgoal for S S' T T' L L' C x2 x1a x2a
using twl_struct_invs_no_alien_in_trail[of T ‹snd L›] H'[of T ‹snd L›]
by (auto simp add: twl_st_of_clause_to_update twl_list_invs_set_clauses_to_update_iff
intro: cdcl_twl_cp_twl_struct_invs cdcl_twl_cp_twl_stgy_invs
distinct_mset_clause_to_update
dest: in_clause_to_updateD)
done
qed
lemma get_conflict_l_get_conflict_state_spec:
assumes ‹(S, S') ∈ twl_st_l None› and ‹twl_list_invs S› and ‹clauses_to_update_l S = {#}›
shows ‹((False, S), (False, S'))
∈ {((brk, S), (brk', S')). brk = brk' ∧ (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧
clauses_to_update_l S = {#}}›
using assms by auto
fun lit_and_ann_of_propagated where
‹lit_and_ann_of_propagated (Propagated L C) = (L, C)› |
‹lit_and_ann_of_propagated (Decided _) = undefined›
definition tl_state_l :: ‹'v twl_st_l ⇒ 'v twl_st_l› where
‹tl_state_l = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q). (tl M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q))›
definition resolve_cls_l' :: ‹'v twl_st_l ⇒ nat ⇒ 'v literal ⇒ 'v clause› where
‹resolve_cls_l' S C L =
remove1_mset L (remove1_mset (-L) (the (get_conflict_l S) ∪# mset (get_clauses_l S ∝ C)))›
definition update_confl_tl_l :: ‹'v literal ⇒ nat ⇒ 'v twl_st_l ⇒ bool × 'v twl_st_l› where
‹update_confl_tl_l = (λL C (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q).
let D = resolve_cls_l' (M, N, D, NE, UE, NEk, UEk, NS, US, WS, Q) C L in
(False, (tl M, N, Some D, NE, UE, NEk, UEk, NS, US, WS, Q)))›
definition update_confl_tl_l_pre :: ‹'v literal ⇒ nat ⇒ 'v twl_st_l ⇒ bool› where
‹update_confl_tl_l_pre L C S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧ update_confl_tl_pre L (mset (get_clauses_l S ∝ C)) S' ∧
twl_list_invs S ∧ C ∈# dom_m (get_clauses_l S) ∧ get_trail_l S ≠ [] ∧ hd (get_trail_l S) = Propagated L C ∧ C > 0)›
definition mop_update_confl_tl_l :: ‹'v literal ⇒ nat ⇒ 'v twl_st_l ⇒ (bool × 'v twl_st_l) nres› where
‹mop_update_confl_tl_l = (λL C S. do {
ASSERT(update_confl_tl_l_pre L C S);
RETURN (update_confl_tl_l L C S)})›
definition mop_hd_trail_l_pre :: ‹'v twl_st_l ⇒ bool› where
‹mop_hd_trail_l_pre S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧ mop_hd_trail_pre S' ∧
twl_list_invs S ∧ mark_of (hd (get_trail_l S)) > 0)›
definition mop_hd_trail_l :: ‹'v twl_st_l ⇒ ('v literal × nat) nres› where
‹mop_hd_trail_l S = do{
ASSERT(mop_hd_trail_l_pre S);
SPEC(λ(L, C). Propagated L C = hd (get_trail_l S))
}›
definition mop_lit_notin_conflict_l :: ‹'v literal ⇒ 'v twl_st_l ⇒ bool nres› where
‹mop_lit_notin_conflict_l L S = do {
ASSERT(get_conflict_l S ≠ None ∧ -L ∉# the (get_conflict_l S) ∧ L ∈# all_lits_of_st_l S);
RETURN (L ∉# the (get_conflict_l S))
}›
definition mop_tl_state_l_pre :: ‹'v twl_st_l ⇒ bool› where
‹mop_tl_state_l_pre S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧ mop_tl_state_pre S' ∧
twl_list_invs S)›
definition mop_tl_state_l :: ‹'v twl_st_l ⇒ (bool × 'v twl_st_l) nres› where
‹mop_tl_state_l = (λS. do {
ASSERT(mop_tl_state_l_pre S);
RETURN(False, tl_state_l S)})›
definition mop_maximum_level_removed_l_pre :: ‹'v literal ⇒ 'v twl_st_l ⇒ bool› where
‹mop_maximum_level_removed_l_pre L S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧ mop_maximum_level_removed_pre L S' ∧
twl_list_invs S)›
definition mop_maximum_level_removed_l :: ‹'v literal ⇒ 'v twl_st_l ⇒ bool nres› where
‹mop_maximum_level_removed_l L S = do {
ASSERT (mop_maximum_level_removed_l_pre L S);
RETURN (get_maximum_level (get_trail_l S) (remove1_mset (-L) (the (get_conflict_l S))) =
count_decided (get_trail_l S))
}›
definition skip_and_resolve_loop_inv_l where
‹skip_and_resolve_loop_inv_l S⇩0 brk S ⟷
(∃S' S⇩0'. (S, S') ∈ twl_st_l None ∧ (S⇩0, S⇩0') ∈ twl_st_l None ∧
skip_and_resolve_loop_inv S⇩0' (brk, S') ∧
twl_list_invs S ∧ clauses_to_update_l S = {#} ∧
(¬is_decided (hd (get_trail_l S)) ⟶ mark_of (hd(get_trail_l S)) > 0))›
definition skip_and_resolve_loop_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹skip_and_resolve_loop_l S⇩0 =
do {
ASSERT(get_conflict_l S⇩0 ≠ None);
(_, S) ←
WHILE⇩T⇗λ(brk, S). skip_and_resolve_loop_inv_l S⇩0 brk S⇖
(λ(brk, S). ¬brk ∧ ¬is_decided (hd (get_trail_l S)))
(λ(_, S).
do {
(L, C) ← mop_hd_trail_l S;
b ← mop_lit_notin_conflict_l (-L) S;
if b then
mop_tl_state_l S
else do {
b ← mop_maximum_level_removed_l L S;
if b
then
mop_update_confl_tl_l L C S
else
RETURN (True, S)
}
}
)
(False, S⇩0);
RETURN S
}
›
lemma get_level_same_lits_cong:
assumes
‹map (atm_of o lit_of) M = map (atm_of o lit_of) M'› and
‹map is_decided M = map is_decided M'›
shows ‹get_level M L = get_level M' L›
proof -
have [dest]: ‹map is_decided M = map is_decided zsa ⟹
length (filter is_decided M) = length (filter is_decided zsa)›
for M :: ‹('d, 'e, 'f) annotated_lit list› and zsa :: ‹('g, 'h, 'i) annotated_lit list›
by (induction M arbitrary: zsa) (auto simp: get_level_def)
show ?thesis
using assms
by (induction M arbitrary: M') (auto simp: get_level_def )
qed
lemma clauses_in_unit_clss_have_level0:
assumes
struct_invs: ‹twl_struct_invs T› and
C: ‹C ∈# unit_clss T› and
LC_T: ‹Propagated L C ∈ set (get_trail T)› and
count_dec: ‹0 < count_decided (get_trail T)›
shows
‹get_level (get_trail T) L = 0› (is ?lev_L) and
‹∀K∈# C. get_level (get_trail T) K = 0› (is ?lev_K)
proof -
have
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of T)› and
ent: ‹entailed_clss_inv (pstate⇩W_of T)›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
pcdcl_all_struct_invs_def state⇩W_of_def[symmetric]
by fast+
obtain K where
‹K ∈# C› and lev_K: ‹get_level (get_trail T) K = 0› and K_M: ‹K ∈ lits_of_l (get_trail T)›
using ent C count_dec by (cases T; cases ‹get_conflict T›) (auto simp: entailed_clss_inv.simps)
obtain M1 M2 where
M: ‹get_trail T = M2 @ Propagated L C # M1›
using LC_T by (blast elim: in_set_list_format)
have ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of T)› and
lev_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T) ›
using all_struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then have M1: ‹M1 ⊨as CNot (remove1_mset L C)› and ‹L ∈# C›
using M unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (auto simp: twl_st)
moreover have n_d: ‹no_dup (get_trail T)›
using lev_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by simp
ultimately have ‹L = K›
using ‹K ∈# C› M K_M
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset
dest: in_lits_of_l_defined_litD no_dup_uminus_append_in_atm_notin
no_dup_appendD no_dup_consistentD)
then show ?lev_L
using lev_K by simp
have count_dec_M1: ‹count_decided M1 = 0›
using M n_d ‹?lev_L› by auto
have ‹get_level (get_trail T) K = 0› if ‹K ∈# C› for K
proof -
have ‹-K ∈ lits_of_l (Propagated (-L) C # M1)›
using M1 M that by (auto simp: true_annots_true_cls_def_iff_negation_in_model remove1_mset_add_mset_If
dest!: multi_member_split dest: in_diffD split: if_splits)
then have ‹get_level (get_trail T) K = get_level (Propagated (-L) C # M1) K›
apply -
apply (subst (2) get_level_skip[symmetric, of M2])
using n_d M by (auto dest: no_dup_uminus_append_in_atm_notin
intro: get_level_same_lits_cong)
then show ?thesis
using count_decided_ge_get_level[of ‹Propagated (-L) C # M1› K] count_dec_M1
by (auto simp: get_level_cons_if split: if_splits)
qed
then show ?lev_K
by fast
qed
lemma clauses_clss_have_level1_notin_unit:
assumes
struct_invs: ‹twl_struct_invs T› and
LC_T: ‹Propagated L C ∈ set (get_trail T)› and
count_dec: ‹0 < count_decided (get_trail T)› and
‹get_level (get_trail T) L > 0›
shows
‹C ∉# unit_clss T›
using clauses_in_unit_clss_have_level0[of T C, OF struct_invs _ LC_T count_dec] assms
by linarith
lemma skip_and_resolve_loop_l_spec:
‹(skip_and_resolve_loop_l, skip_and_resolve_loop) ∈
{(S::'v twl_st_l, S'). (S, S') ∈ twl_st_l None ∧ twl_struct_invs S' ∧
twl_stgy_invs S' ∧
twl_list_invs S ∧ clauses_to_update_l S = {#} ∧ literals_to_update_l S = {#} ∧
get_conflict S' ≠ None ∧
0 < count_decided (get_trail_l S)} →⇩f
⟨{(T, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T ∧
(twl_struct_invs T' ∧ twl_stgy_invs T' ∧
no_step cdcl⇩W_restart_mset.skip (state⇩W_of T') ∧
no_step cdcl⇩W_restart_mset.resolve (state⇩W_of T') ∧
literals_to_update T' = {#} ∧
clauses_to_update_l T = {#} ∧ get_conflict T' ≠ None)}⟩ nres_rel›
(is ‹_ ∈ ?R →⇩f _›)
proof -
let ?R' = ‹{(T::'v twl_st_l, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T ∧
clauses_to_update_l T = {#}}›
have H: ‹((False, x), False, y) ∈ bool_rel ×⇩f ?R'› if ‹(x, y) ∈ ?R'› for x y
using that by auto
have
mark_ge_0: ‹0 < mark_of (hd (get_trail_l T))› (is ?ge) and
nempty: ‹get_trail_l T ≠ []› ‹get_trail (snd brkT') ≠ []› (is ?nempty)
if
SS': ‹(S, S') ∈ ?R› and
‹get_conflict_l S ≠ None› and
brk_TT': ‹(brkT, brkT')
∈ {((brk, S), brk', S'). brk = brk' ∧ (S, S') ∈ twl_st_l None ∧
twl_list_invs S ∧ clauses_to_update_l S = {#}}› (is ‹_ ∈ ?brk›) and
loop_inv: ‹skip_and_resolve_loop_inv S' brkT'› and
brkT: ‹brkT = (brk, T)› and
dec: ‹¬ is_decided (hd (get_trail_l T))›
for S S' brkT brkT' brk T
proof -
obtain brk' T' where brkT': ‹brkT' = (brk', T')› by (cases brkT')
have ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of T')› and
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of T')› and
tr: ‹get_trail T' ≠ []› ‹get_trail_l T ≠ []› and
count_dec: ‹count_decided (get_trail_l T) ≠ 0› ‹count_decided (get_trail T') ≠ 0› and
TT': ‹(T,T') ∈ twl_st_l None› and
struct_invs: ‹twl_struct_invs T'›
using loop_inv brk_TT' unfolding twl_struct_invs_def skip_and_resolve_loop_inv_def brkT brkT'
prod.simps state⇩W_of_def[symmetric] pcdcl_all_struct_invs_def
by auto
moreover have ‹Suc 0 ≤ backtrack_lvl (state⇩W_of T')›
using count_dec TT' by (auto simp: trail.simps)
moreover have proped: ‹is_proped (cdcl⇩W_restart_mset.hd_trail (state⇩W_of T'))›
using dec tr TT' by (cases ‹get_trail_l T›)
(auto simp: trail.simps is_decided_no_proped_iff twl_st)
moreover have ‹mark_of (hd (get_trail T')) ∉# get_kept_unit_clauses_l T›
using clauses_clss_have_level1_notin_unit(1)[of T' ‹lit_of (hd (get_trail T'))›
‹mark_of (hd (get_trail T'))›] dec struct_invs count_dec tr proped TT'
by (cases ‹get_trail T'›; cases ‹hd (get_trail T')›)
(auto simp: twl_st get_unit_clauses_l_alt_def)
moreover have ‹convert_lit (get_clauses_l T) (get_kept_unit_clauses_l T) (hd (get_trail_l T))
(hd (get_trail T'))›
using tr dec TT'
by (cases ‹get_trail T'›; cases ‹get_trail_l T›)
(auto simp: twl_st_l_def)
ultimately have ‹mark_of (hd (get_trail_l T)) = 0 ⟹ False›
using tr dec TT' apply (cases ‹get_trail_l T›; cases ‹hd (get_trail_l T)›)
by (auto simp: trail.simps twl_st convert_lit.simps)
then show ?ge by blast
show ‹get_trail_l T ≠ []› ‹get_trail (snd brkT') ≠ []›
using tr TT' brkT' by auto
qed
have mop_hd_trail_l:
‹mop_hd_trail_l S ≤ ⇓{((L, C), (L', C')). L = L' ∧
C' = mset (get_clauses_l S ∝ C) ∧ C ∈# dom_m (get_clauses_l S) ∧ get_trail_l S ≠ [] ∧
hd (get_trail_l S) = Propagated L C ∧ C > 0} (mop_hd_trail S')›
(is ‹_ ≤ ⇓ ?hd _›)
if ‹(brkS, brkS') ∈ bool_rel ×⇩f ?R'› and
‹case brkS of (brk, S) ⇒ skip_and_resolve_loop_inv_l S⇩0 brk S› and
‹case brkS of (brk, S) ⇒ ¬brk ∧ ¬ is_decided (hd (get_trail_l S))› and
‹brkS = (brk, S)› and
‹brkS' = (brk', S')›
for S S' S⇩0 brk brkS brkS' brk'
using that
unfolding mop_hd_trail_l_def mop_hd_trail_def
apply refine_rcg
subgoal unfolding mop_hd_trail_l_pre_def skip_and_resolve_loop_inv_l_def
mop_hd_trail_def
by (rule exI[of _ S']) auto
subgoal
apply (rule RES_refine)
using mark_ge_0[of S S' brkS brkS']
apply (cases ‹get_trail S'›; cases ‹get_trail_l S›;
cases ‹hd (get_trail S')›)
by (auto simp: mop_hd_trail_pre_def twl_st_l_def
convert_lit.simps mop_hd_trail_l_pre_def)
done
have mop_lit_notin_conflict_l:
‹mop_lit_notin_conflict_l (-L) S ≤ ⇓Id (mop_lit_notin_conflict (-L') S')›
if ‹(brkS, brkS') ∈ bool_rel ×⇩f ?R'› and
‹case brkS of (brk, S) ⇒ skip_and_resolve_loop_inv_l S⇩0 brk S› and
‹case brkS of (brk, S) ⇒ ¬brk ∧ ¬ is_decided (hd (get_trail_l S))› and
‹brkS = (brk, S)› and
‹brkS' = (brk', S')› and
‹LC = (L, C)› and
‹LC' = (L', C')› and
‹((LC), (LC')) ∈ ?hd S›
for S S' S⇩0 brk brkS brkS' brk' L L' C C' LC LC'
using that
unfolding mop_lit_notin_conflict_l_def mop_lit_notin_conflict_def
apply refine_rcg
subgoal
by auto
subgoal
by auto
subgoal
by (auto simp: mset_take_mset_drop_mset')
subgoal
by auto
done
have mop_maximum_level_removed_l:
‹mop_maximum_level_removed_l L S ≤ ⇓bool_rel (mop_maximum_level_removed L' S')›
if ‹(brkS, brkS') ∈ bool_rel ×⇩f ?R'› and
‹case brkS of (brk, S) ⇒ skip_and_resolve_loop_inv_l S⇩0 brk S› and
‹case brkS of (brk, S) ⇒ ¬brk ∧ ¬ is_decided (hd (get_trail_l S))› and
‹brkS = (brk, S)› and
‹brkS' = (brk', S')› and
‹LC = (L, C)› and
‹LC' = (L', C')› and
‹((LC), (LC')) ∈ ?hd S›
for S S' S⇩0 brk brkS brkS' brk' L L' C C' LC LC'
using that
unfolding mop_maximum_level_removed_l_def mop_maximum_level_removed_def
apply refine_rcg
subgoal
unfolding mop_maximum_level_removed_l_pre_def
by (rule exI[of _ ‹S'›]) auto
subgoal
by auto
done
have mop_tl_state_l:
‹mop_tl_state_l S ≤ ⇓ (bool_rel ×⇩f ?R') (mop_tl_state S')›
if ‹(brkS, brkS') ∈ bool_rel ×⇩f ?R'› and
‹case brkS of (brk, S) ⇒ skip_and_resolve_loop_inv_l S⇩0 brk S› and
‹case brkS of (brk, S) ⇒ ¬brk ∧ ¬ is_decided (hd (get_trail_l S))› and
‹brkS = (brk, S)› and
‹brkS' = (brk', S')› and
‹LC = (L, C)› and
‹LC' = (L', C')› and
‹((LC), (LC')) ∈ ?hd S›
for S S' S⇩0 brk brkS brkS' brk' L L' C C' LC LC'
using that unfolding mop_tl_state_l_def mop_tl_state_def
apply refine_rcg
subgoal
unfolding mop_tl_state_l_pre_def
by (rule exI[of _ ‹S'›]) auto
subgoal
by (cases S; cases S'; cases ‹get_trail_l S›; cases ‹get_trail S'›)
(auto simp: tl_state_l_def tl_state_def twl_st_l_def
convert_lits_l_tlD mop_tl_state_pre_def twl_list_invs_def)
done
have mop_update_confl_tl_l:
‹mop_update_confl_tl_l L C S ≤ ⇓ (bool_rel ×⇩f ?R') (mop_update_confl_tl L' C' S')›
if ‹(brkS, brkS') ∈ bool_rel ×⇩f ?R'› and
‹case brkS of (brk, S) ⇒ skip_and_resolve_loop_inv_l S⇩0 brk S› and
‹case brkS of (brk, S) ⇒ ¬brk ∧ ¬ is_decided (hd (get_trail_l S))› and
‹brkS = (brk, S)› and
‹brkS' = (brk', S')› and
‹LC = (L, C)› and
‹LC' = (L', C')› and
‹((LC), (LC')) ∈ ?hd S›
for S S' S⇩0 brk brkS brkS' brk' L L' C C' LC LC'
using that unfolding mop_update_confl_tl_l_def mop_update_confl_tl_def
apply refine_rcg
subgoal
unfolding update_confl_tl_l_pre_def
by (rule exI[of _ ‹S'›]) (auto simp: twl_struct_invs_def)
subgoal
by (cases S; cases S'; cases ‹get_trail_l S›; cases ‹get_trail S'›)
(auto simp: update_confl_tl_l_def update_confl_tl_def twl_st_l_def
convert_lits_l_tlD mop_tl_state_pre_def twl_list_invs_def resolve_cls_l'_def)
done
have H:
‹(skip_and_resolve_loop_l, skip_and_resolve_loop) ∈ ?R →⇩f
⟨{(T::'v twl_st_l, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T ∧
clauses_to_update_l T = {#}}⟩ nres_rel›
apply (intro frefI nres_relI)
unfolding skip_and_resolve_loop_l_def skip_and_resolve_loop_def
apply (refine_rcg H)
subgoal by auto
subgoal by auto
subgoal for x y xa x' x1 x2
unfolding skip_and_resolve_loop_inv_l_def
apply (cases x')
apply(rule exI[of _ ‹snd x'›])
apply(rule exI[of _ y])
apply (intro conjI impI)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (rule mark_ge_0) auto
done
subgoal by (auto simp: twl_st_l twl_st skip_and_resolve_loop_inv_def)
apply (rule mop_hd_trail_l; assumption)
apply (rule mop_lit_notin_conflict_l; assumption)
subgoal by auto
apply (rule mop_tl_state_l; assumption)
apply (rule mop_maximum_level_removed_l; assumption)
subgoal by auto
apply (rule mop_update_confl_tl_l; assumption)
subgoal by auto
subgoal by auto
done
have H: ‹(skip_and_resolve_loop_l, skip_and_resolve_loop)
∈ ?R →⇩f
⟨{(T::'v twl_st_l, T').
(T, T') ∈ {(T, T'). (T, T') ∈ twl_st_l None ∧ (twl_list_invs T ∧
clauses_to_update_l T = {#})} ∧
T' ∈ {T'. twl_struct_invs T' ∧ twl_stgy_invs T' ∧
(no_step cdcl⇩W_restart_mset.skip (state⇩W_of T')) ∧
(no_step cdcl⇩W_restart_mset.resolve (state⇩W_of T')) ∧
literals_to_update T' = {#} ∧
get_conflict T' ≠ None}}⟩nres_rel›
apply (rule refine_add_inv_generalised)
subgoal by (rule H)
subgoal for S S'
apply (rule order_trans)
apply (rule skip_and_resolve_loop_spec[of S'])
by auto
done
show ?thesis
using H apply -
apply (match_spec; (match_fun_rel; match_fun_rel?)+)
by blast+
qed
definition find_decomp :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹find_decomp = (λL (M, N, D, NE, NEk, UEk, UE, NS, US, WS, Q).
SPEC(λS. ∃K M2 M1. S = (M1, N, D, NE, NEk, UEk, UE, NS, US, WS, Q) ∧
(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
get_level M K = get_maximum_level M (the D - {#-L#}) + 1))›
lemma find_decomp_alt_def:
‹find_decomp L S =
SPEC(λT. ∃K M2 M1. equality_except_trail S T ∧ get_trail_l T = M1 ∧
(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (get_trail_l S)) ∧
get_level (get_trail_l S) K =
get_maximum_level (get_trail_l S) (the (get_conflict_l S) - {#-L#}) + 1)›
unfolding find_decomp_def
by (cases S) force
definition find_lit_of_max_level_l :: ‹'v twl_st_l ⇒ 'v literal ⇒ 'v literal nres› where
‹find_lit_of_max_level_l = (λ(M, N, D, NE, UE, NEk, UEk, WS, Q) L.
SPEC(λL'. L' ∈# the D - {#-L#} ∧ get_level M L' = get_maximum_level M (the D - {#-L#})))›
lemma find_lit_of_max_level_l_alt_def:
‹find_lit_of_max_level_l = (λS L.
SPEC(λL'. L' ∈# the (get_conflict_l S) - {#-L#} ∧
get_level (get_trail_l S) L' = get_maximum_level (get_trail_l S) (the (get_conflict_l S) - {#-L#})))›
by (auto simp: find_lit_of_max_level_l_def intro!: ext)
definition ex_decomp_of_max_lvl :: ‹('v, nat) ann_lits ⇒ 'v cconflict ⇒ 'v literal ⇒ bool› where
‹ex_decomp_of_max_lvl M D L ⟷
(∃K M1 M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
get_level M K = get_maximum_level M (remove1_mset (-L) (the D)) + 1)›
fun add_mset_list :: ‹'a list ⇒ 'a multiset multiset ⇒ 'a multiset multiset› where
‹add_mset_list L UE = add_mset (mset L) UE›
definition (in -)list_of_mset :: ‹'v clause ⇒ 'v clause_l nres› where
‹list_of_mset D = SPEC(λD'. D = mset D')›
:: ‹'v twl_st_l ⇒ bool› where
‹extract_shorter_conflict_l_pre S ⟷ (∃S'. (S, S') ∈ twl_st_l None ∧
extract_shorter_conflict_pre S')›
:: ‹'v twl_st_l ⇒ 'v twl_st_l nres›
where
‹extract_shorter_conflict_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) = do {
ASSERT(extract_shorter_conflict_l_pre (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q));
SPEC(λS.
∃D'. D' ⊆# the D ∧ S = (M, N, Some D', NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) ∧
clause `# twl_clause_of `# ran_mf N + (NE + NEk) + (UE + UEk) + NS + US + N0 + U0 ⊨pm D' ∧ -(lit_of (hd M)) ∈# D')
}›
declare extract_shorter_conflict_l.simps[simp del]
lemmas = extract_shorter_conflict_l.simps
lemma :
‹extract_shorter_conflict_l S = do {
ASSERT(extract_shorter_conflict_l_pre S);
SPEC(λT.
∃D'. D' ⊆# the (get_conflict_l S) ∧ equality_except_conflict_l S T ∧
get_conflict_l T = Some D' ∧
get_all_clss_l S ⊨pm D' ∧
-lit_of (hd (get_trail_l S)) ∈# D') }›
by (cases S) (auto simp: extract_shorter_conflict_l_def
mset_take_mset_drop_mset mset_take_mset_drop_mset' Un_assoc
intro: bind_cong)
definition backtrack_l_inv where
‹backtrack_l_inv S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧
backtrack_inv S' ∧
twl_list_invs S ∧
literals_to_update_l S = {#})
›
definition get_fresh_index :: ‹'v clauses_l ⇒ nat nres› where
‹get_fresh_index N = SPEC(λi. i > 0 ∧ i ∉# dom_m N)›
definition propagate_bt_l_pre where
‹propagate_bt_l_pre L L' S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧ propagate_bt_pre L L' S')›
definition propagate_bt_l :: ‹'v literal ⇒ 'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹propagate_bt_l = (λL L' (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q). do {
ASSERT(propagate_bt_l_pre L L' (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q));
ASSERT(L ∈# all_lits_of_st_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q));
ASSERT(L' ∈# all_lits_of_st_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q));
D'' ← list_of_mset (the D);
i ← get_fresh_index N;
M ← cons_trail_propagate_l (-L) i M;
RETURN (M,
fmupd i ([-L, L'] @ (remove1 (-L) (remove1 L' D'')), False) N,
None, NE, UE, NEk, UEk, NS, US, N0, U0, WS, {#L#})
})›
definition propagate_unit_bt_l_pre where
‹propagate_unit_bt_l_pre L S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧ propagate_unit_bt_pre L S')›
definition propagate_unit_bt_l :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l nres› where
‹propagate_unit_bt_l = (λL (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q). do {
ASSERT(L ∈# all_lits_of_st_l (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q));
ASSERT(propagate_unit_bt_l_pre L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q));
M ← cons_trail_propagate_l (-L) 0 M;
RETURN (M, N, None, NE, UE, NEk, add_mset (the D) UEk, NS, US, N0, U0, WS, {#L#})})›
definition mop_lit_hd_trail_l_pre :: ‹'v twl_st_l ⇒ bool› where
‹mop_lit_hd_trail_l_pre S ⟷
(∃S'. (S, S') ∈ twl_st_l None ∧ mop_lit_hd_trail_pre S' ∧
twl_list_invs S)›
definition mop_lit_hd_trail_l :: ‹'v twl_st_l ⇒ ('v literal) nres› where
‹mop_lit_hd_trail_l S = do{
ASSERT(mop_lit_hd_trail_l_pre S);
SPEC(λL. L = lit_of (hd (get_trail_l S)))
}›
definition backtrack_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹backtrack_l S =
do {
ASSERT(backtrack_l_inv S);
L ← mop_lit_hd_trail_l S;
S ← extract_shorter_conflict_l S;
S ← find_decomp L S;
if size (the (get_conflict_l S)) > 1
then do {
L' ← find_lit_of_max_level_l S L;
propagate_bt_l L L' S
}
else do {
propagate_unit_bt_l L S
}
}›
lemma backtrack_l_spec:
‹(backtrack_l, backtrack) ∈
{(S::'v twl_st_l, S'). (S, S') ∈ twl_st_l None ∧ get_conflict_l S ≠ None ∧
get_conflict_l S ≠ Some {#} ∧
clauses_to_update_l S = {#} ∧ literals_to_update_l S = {#} ∧ twl_list_invs S ∧
twl_struct_invs S' ∧ twl_stgy_invs S' ∧
no_step cdcl⇩W_restart_mset.skip (state⇩W_of S') ∧
no_step cdcl⇩W_restart_mset.resolve (state⇩W_of S')} →⇩f
⟨{(T::'v twl_st_l, T'). (T, T') ∈ twl_st_l None ∧ get_conflict_l T = None ∧ twl_list_invs T ∧
twl_struct_invs T' ∧ twl_stgy_invs T' ∧ clauses_to_update_l T = {#} ∧
literals_to_update_l T ≠ {#}}⟩ nres_rel›
(is ‹ _ ∈ ?R →⇩f ?I›)
proof -
let ?J = ‹{(T::'v twl_st_l, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T ∧
clauses_to_update_l T = {#} ∧ literals_to_update_l T ≠ {#}}›
let ?J' = ‹{(T::'v twl_st_l, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T ∧
clauses_to_update_l T = {#} ∧ literals_to_update_l T = {#}}›
have mop_lit_hd_trail_l:
‹mop_lit_hd_trail_l x ≤ ⇓ Id (mop_lit_hd_trail y)›
if ‹(x,y) ∈ ?R›
for x y
using that
unfolding mop_lit_hd_trail_l_def mop_lit_hd_trail_def
apply refine_vcg
subgoal
unfolding mop_lit_hd_trail_l_pre_def
by (rule exI[of _ y]) auto
subgoal by (auto simp: mop_lit_hd_trail_pre_def)
done
have [simp]: ‹(λx. mset (fst x)) ` {a. a ∈# ran_m aa ∧ snd a} ∪
(λx. mset (fst x)) ` {a. a ∈# ran_m aa ∧ ¬ snd a} ∪ A =
(λx. mset (fst x)) ` {a. a ∈# ran_m aa}∪ A› for aa A
by auto
have get_all_clss_alt_def:
‹get_all_clss y = clauses (get_clauses y) + unit_clss y + subsumed_clauses y + get_all_clauses0 y› for y
by (cases y) auto
have entailement_cong:‹(x,y) ∈ ?R ⟹ (get_all_clss_l x) ⊨pm D ⟷
(get_all_clss y) ⊨pm D› for x y D
by auto
have extract_shorter_conflict_l: ‹extract_shorter_conflict_l x
≤ ⇓ ?J'
(extract_shorter_conflict y)›
if ‹(x,y) ∈ ?R›
for x y
using that
unfolding extract_shorter_conflict_l_alt_def extract_shorter_conflict_alt_def
apply refine_vcg
subgoal
unfolding extract_shorter_conflict_l_pre_def
by (rule exI[of _ y]) auto
subgoal
unfolding get_all_clss_alt_def[symmetric]
apply (subst entailement_cong, assumption)
by (rule RES_refine, rule_tac x = ‹set_conflict (the (get_conflict_l s)) y› in bexI)
(clarsimp simp: twl_st_l_def image_image image_Un mset_take_mset_drop_mset'
extract_shorter_conflict_pre_def twl_list_invs_def
simp del: get_all_clss.simps)+
done
have find_decomp: ‹(L, La) ∈ Id ⟹
(S, Sa) ∈ ?J' ⟹
find_decomp L S
≤ ⇓ ?J' (reduce_trail_bt La Sa)› for L La S Sa
unfolding find_decomp_def reduce_trail_bt_def
RES_RETURN_RES
apply refine_vcg
subgoal for x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f
x1g x2g x1h x2h x1i x2i x1j x2j x1k x2k x1l x2l
apply (rule RES_refine)
apply (rule_tac x=‹(drop (length (get_trail Sa) - length (get_trail_l s)) (get_trail Sa),
x1a, x1b, x1c, x1d, x1e, x1f, x2f)› in bexI)
apply (auto simp: twl_st_l_def image_iff twl_list_invs_def
intro: convert_lits_l_decomp_ex)
apply (rule_tac x=K in exI)
apply (auto simp: twl_st_l_def image_image image_Un mset_take_mset_drop_mset'
extract_shorter_conflict_pre_def convert_lits_l_decomp_ex)
done
done
have find_lit_of_max_level_l: ‹(L, La) ∈ Id ⟹
(S, Sa) ∈ ?J' ⟹
(Sb, Sc) ∈ ?J' ⟹
find_lit_of_max_level_l Sb L
≤ ⇓ Id (find_lit_of_max_level Sc La)›
for L La S Sa Sb Sc
unfolding find_lit_of_max_level_l_alt_def
find_lit_of_max_level_def
by refine_rcg auto
have [intro!]: ‹mset x =
add_mset (La) (add_mset L'a (mset x - {#La, L'a#}))›
if ‹La ∈ set x› and ‹L'a ∈ set x› ‹La ≠ L'a› for x La L'a
using that
by (metis add_mset_add_single diff_diff_add_mset in_multiset_in_set mset_add
remove1_mset_add_mset_If)
have propagate_bt_l_preD:
‹ ¬tautology (add_mset (- L) (add_mset L' (the (get_conflict_l S) - {#- L, L'#})))›
if pre: ‹propagate_bt_l_pre L L' S› for L L' S
proof -
obtain M N U D NE UE NEk UEk NS US WS Q M' D' T where
T: ‹T = (M, N, U, Some D, NE, UE, NEk, UEk, NS, US, WS, Q)› and
struct: ‹twl_struct_invs (M' @ M, N, U, Some D', NE, UE, NEk, UEk, NS, US, WS, Q)› and
ST: ‹(S, T) ∈ twl_st_l None› and
DD': ‹D ⊆# D'› and
LL': ‹- L ∈# D ∧ L' ∈# remove1_mset (- L) D›
using pre that
unfolding propagate_bt_l_pre_def propagate_bt_pre_def
by auto
have ‹M' @ M ⊨as CNot D'› and ‹no_dup (M' @ M)›
using struct unfolding
pcdcl_all_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by simp_all
then have ‹¬tautology D'›
using consistent_CNot_not_tautology[of ‹lits_of_l (M'@M)› D']
by (auto simp: true_annots_true_cls dest: distinct_consistent_interp)
then show ‹?thesis›
using ST DD' LL' by (simp only: twl_st_l[symmetric], auto dest!: multi_member_split
simp add: T not_tautology_mono)
qed
have propagate_bt_l: ‹(Sb, Sc) ∈ ?J' ⟹
(L', L'a) ∈ Id ⟹
(L, La) ∈ Id ⟹
propagate_bt_l L L' Sb
≤ ⇓ ?J
(mop_propagate_bt La L'a Sc)›
for L La S Sa Sb Sc L' L'a
unfolding propagate_bt_l_def
mop_propagate_bt_def list_of_mset_def
get_fresh_index_def cons_trail_propagate_l_def
apply refine_vcg
subgoal unfolding propagate_bt_l_pre_def by fast
subgoal by (auto simp: propagate_bt_pre_def twl_st_l_def all_lits_of_st_def
all_lits_of_st_l_def mset_take_mset_drop_mset' simp flip: image_mset_union) (simp add: ac_simps)
subgoal by (auto simp: propagate_bt_pre_def twl_st_l_def all_lits_of_st_def
all_lits_of_st_l_def mset_take_mset_drop_mset' simp flip: image_mset_union) (simp add: ac_simps)
subgoal by (auto simp: propagate_bt_pre_def twl_st_l_def
mset_take_mset_drop_mset' simp flip: image_mset_union)
subgoal
apply (frule propagate_bt_l_preD)
by (clarsimp simp add: twl_list_invs_def propagate_bt_def twl_st_l_def
propagate_bt_pre_def init_clss_l_mapsto_upd_irrel_notin ran_m_mapsto_upd_notin
learned_clss_l_mapsto_upd_notin)
(auto 4 3 simp: twl_list_invs_def propagate_bt_def twl_st_l_def
propagate_bt_pre_def init_clss_l_mapsto_upd_irrel_notin
learned_clss_l_mapsto_upd_notin
intro!: convert_lit.intros(2)
intro!: convert_lits_l_bind_new
dest: in_diffD)
done
have propagate_unit_bt_l: ‹(Sb, Sc) ∈ ?J' ⟹
(L, La) ∈ Id ⟹
propagate_unit_bt_l L Sb
≤ ⇓ ?J
(mop_propagate_unit_bt La Sc)›
for L La S Sa Sb Sc L' L'a
unfolding propagate_unit_bt_l_def
mop_propagate_unit_bt_def cons_trail_propagate_l_def
apply refine_vcg
subgoal by (auto simp: propagate_unit_bt_pre_def twl_st_l_def all_lits_of_st_def
all_lits_of_st_l_def
mset_take_mset_drop_mset' simp flip: image_mset_union) (simp add: ac_simps)
subgoal
unfolding propagate_unit_bt_l_pre_def
by blast
subgoal by (auto simp: propagate_unit_bt_pre_def twl_st_l_def
mset_take_mset_drop_mset' simp flip: image_mset_union)
subgoal by (auto simp: twl_list_invs_def propagate_unit_bt_def twl_st_l_def
convert_lits_l_add_mset intro!: convert_lit.intros)
done
have bt: ‹(backtrack_l, backtrack) ∈
?R →⇩f ⟨?J⟩ nres_rel›
unfolding backtrack_l_def backtrack_def
apply (intro frefI nres_relI)
apply (refine_rcg mop_lit_hd_trail_l)
subgoal for x y
unfolding backtrack_l_inv_def
by (rule exI[of _ y]) auto
apply (rule extract_shorter_conflict_l; assumption)
apply (rule find_decomp; assumption)
subgoal by auto
apply (rule find_lit_of_max_level_l; assumption)
apply (rule propagate_bt_l; assumption)
apply (rule propagate_unit_bt_l; assumption)
done
have SPEC_Id: ‹SPEC Φ = ⇓ {(T, T'). Φ T} (SPEC Φ)› for Φ
unfolding conc_fun_RES
by auto
have ‹(backtrack_l S, backtrack S') ∈ ?I› if ‹(S, S') ∈ ?R› for S S'
proof -
have ‹backtrack_l S ≤ ⇓ ?J (backtrack S')›
by (rule bt[unfolded fref_param1[symmetric], "to_⇓", rule_format, of S S'])
(use that in auto)
moreover have ‹backtrack S' ≤ SPEC (λT. cdcl_twl_o S' T ∧
get_conflict T = None ∧
(∀S'. ¬ cdcl_twl_o T S') ∧
twl_struct_invs T ∧
twl_stgy_invs T ∧ clauses_to_update T = {#} ∧ literals_to_update T ≠ {#})›
by (rule backtrack_spec["to_⇓", of S']) (use that in ‹auto simp: twl_st_l›)
ultimately show ?thesis
apply -
apply (unfold refine_rel_defs nres_rel_def in_pair_collect_simp;
(unfold Ball2_split_def all_to_meta)?;
(intro allI impI)?)
apply (subst (asm) SPEC_Id)
apply unify_Down_invs2+
unfolding nofail_simps
apply unify_Down_invs2_normalisation_post
apply (rule "weaken_⇓")
prefer 2 apply assumption
subgoal premises p by (auto simp: twl_st_l_def)
done
qed
then show ?thesis
by (intro frefI)
qed
definition find_unassigned_lit_l :: ‹'v twl_st_l ⇒ 'v literal option nres› where
‹find_unassigned_lit_l = (λS.
SPEC (λL.
(L ≠ None ⟶
undefined_lit (get_trail_l S) (the L) ∧
(the L) ∈# all_lits_of_st_l S) ∧
(L = None ⟶ (∄L'. undefined_lit (get_trail_l S) L' ∧
L' ∈# all_lits_of_st_l S)))
)›
definition decide_l_or_skip_pre where
‹decide_l_or_skip_pre S ⟷ (∃S'. (S, S') ∈ twl_st_l None ∧
decide_or_skip_pre S' ∧
twl_list_invs S ∧
clauses_to_update_l S = {#} ∧
literals_to_update_l S = {#})
›
definition decide_lit_l :: ‹'v literal ⇒ 'v twl_st_l ⇒ 'v twl_st_l› where
‹decide_lit_l = (λL' (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q).
(Decided L' # M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, {#- L'#}))›
definition decide_l_or_skip :: ‹'v twl_st_l ⇒ (bool × 'v twl_st_l) nres› where
‹decide_l_or_skip S = (do {
ASSERT(decide_l_or_skip_pre S);
L ← find_unassigned_lit_l S;
case L of
None ⇒ RETURN (True, S)
| Some L ⇒ RETURN (False, decide_lit_l L S)
})
›
method "match_⇓" =
(match conclusion in ‹f ≤ ⇓ R g› for f :: ‹'a nres› and R :: ‹('a × 'b) set› and
g :: ‹'b nres› ⇒
‹match premises in
I[thin,uncurry]: ‹f ≤ ⇓ R' g› for R' :: ‹('a × 'b) set›
⇒ ‹rule refinement_trans_long[of f f g g R' R, OF refl refl _ I]›
¦ I[thin,uncurry]: ‹_ ⟹ f ≤ ⇓ R' g› for R' :: ‹('a × 'b) set›
⇒ ‹rule refinement_trans_long[of f f g g R' R, OF refl refl _ I]›
›)
lemma decide_l_or_skip_spec:
‹(decide_l_or_skip, decide_or_skip) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ get_conflict_l S = None ∧
clauses_to_update_l S = {#} ∧ literals_to_update_l S = {#} ∧ no_step cdcl_twl_cp S' ∧
twl_struct_invs S' ∧ twl_stgy_invs S' ∧ twl_list_invs S} →⇩f
⟨{((brk, T), (brk', T')). (T, T') ∈ twl_st_l None ∧ brk = brk' ∧ twl_list_invs T ∧
clauses_to_update_l T = {#} ∧
(get_conflict_l T ≠ None ⟶ get_conflict_l T = Some {#})∧
twl_struct_invs T' ∧ twl_stgy_invs T' ∧
(¬brk ⟶ literals_to_update_l T ≠ {#})∧
(brk ⟶ literals_to_update_l T = {#})}⟩ nres_rel›
(is ‹_ ∈ ?R →⇩f ⟨?S⟩nres_rel›)
proof -
have find_unassigned_lit_l: ‹find_unassigned_lit_l S ≤ ⇓ Id (find_unassigned_lit S')›
if SS': ‹(S, S') ∈ ?R›
for S S'
using that
unfolding find_unassigned_lit_l_def find_unassigned_lit_def state_decomp_to_state_l
by (auto simp:)
have I: ‹(x, x') ∈ Id ⟹ (x, x') ∈ ⟨Id⟩option_rel› for x x' by auto
have dec: ‹(decide_l_or_skip, decide_or_skip) ∈ ?R →
⟨{((brk, T), (brk', T')). (T, T') ∈ twl_st_l None ∧ brk = brk' ∧ twl_list_invs T ∧
clauses_to_update_l T = {#} ∧
(¬brk ⟶ literals_to_update_l T ≠ {#})∧
(brk ⟶ literals_to_update_l T = {#}) }⟩ nres_rel›
unfolding decide_l_or_skip_def decide_or_skip_def
apply (refine_vcg find_unassigned_lit_l I)
subgoal unfolding decide_l_or_skip_pre_def by (auto simp: twl_st_l_def)
subgoal by auto
subgoal for S S'
by (cases S)
(auto simp: decide_lit_l_def propagate_dec_def twl_list_invs_def twl_st_l_def)
done
have KK: ‹SPEC (λ(brk, T). cdcl_twl_o⇧*⇧* S' T ∧ P brk T) = ⇓ {(S, S'). snd S = S' ∧
P (fst S) (snd S)} (SPEC (cdcl_twl_o⇧*⇧* S'))›
for S' P
by (auto simp: conc_fun_def)
have nf: ‹nofail (SPEC (cdcl_twl_o⇧*⇧* S'))› ‹nofail (SPEC (cdcl_twl_o⇧*⇧* S'))› for S S'
by auto
have set: ‹{((a,b), (a', b')). P a b a' b'} = {(a, b). P (fst a) (snd a) (fst b) (snd b)}› for P
by auto
show ?thesis
proof (intro frefI nres_relI)
fix S S'
assume SS': ‹(S, S') ∈ ?R›
have ‹decide_l_or_skip S
≤ ⇓ {((brk, T), brk', T').
(T, T') ∈ twl_st_l None ∧
brk = brk' ∧
twl_list_invs T ∧
clauses_to_update_l T = {#} ∧
(¬ brk ⟶ literals_to_update_l T ≠ {#}) ∧ (brk ⟶ literals_to_update_l T = {#})}
(decide_or_skip S')›
apply (rule dec["to_⇓", of S S'])
using SS' by auto
moreover have ‹decide_or_skip S'
≤ ⇓ {(S, S'a).
snd S = S'a ∧
get_conflict (snd S) = None ∧
(∀S'. ¬ cdcl_twl_o (snd S) S') ∧
(fst S ⟶ (∀S'. ¬ cdcl_twl_stgy (snd S) S')) ∧
twl_struct_invs (snd S) ∧
twl_stgy_invs (snd S) ∧
clauses_to_update (snd S) = {#} ∧
(¬ fst S ⟶ literals_to_update (snd S) ≠ {#}) ∧
(¬ (∀S'a. ¬ cdcl_twl_o S' S'a) ⟶ cdcl_twl_o⇧+⇧+ S' (snd S))}
(SPEC (cdcl_twl_o⇧*⇧* S'))›
by (rule decide_or_skip_spec[of S', unfolded KK]) (use SS' in auto)
ultimately show ‹decide_l_or_skip S ≤ ⇓ ?S (decide_or_skip S')›
apply -
apply unify_Down_invs2+
apply (simp only: set nf)
apply ("match_⇓")
subgoal
apply (rule; rule)
apply (clarsimp simp: twl_st_l_def)
done
subgoal by fast
done
qed
qed
lemma refinement_trans_eq:
‹A = A' ⟹ B = B' ⟹ R' = R ⟹ A ≤ ⇓ R B ⟹ A' ≤ ⇓ R' B'›
by (auto simp: pw_ref_iff)
definition cdcl_twl_o_prog_l_pre where
‹cdcl_twl_o_prog_l_pre S ⟷
(∃S' . (S, S') ∈ twl_st_l None ∧
twl_struct_invs S' ∧
twl_stgy_invs S' ∧
twl_list_invs S)›
definition cdcl_twl_o_prog_l :: ‹'v twl_st_l ⇒ (bool × 'v twl_st_l) nres› where
‹cdcl_twl_o_prog_l S =
do {
ASSERT(cdcl_twl_o_prog_l_pre S);
do {
if get_conflict_l S = None
then decide_l_or_skip S
else if count_decided (get_trail_l S) > 0
then do {
T ← skip_and_resolve_loop_l S;
ASSERT(get_conflict_l T ≠ None ∧ get_conflict_l T ≠ Some {#});
U ← backtrack_l T;
RETURN (False, U)
}
else RETURN (True, S)
}
}
›
lemma twl_st_lE:
‹(⋀M N D NE UE WS Q. T = (M, N, D, NE, UE, WS, Q) ⟹ P (M, N, D, NE, UE, WS, Q)) ⟹ P T›
for T :: ‹'a twl_st_l›
by (cases T) auto
lemma "weaken_⇓'": ‹f ≤ ⇓ R' g ⟹ R' ⊆ R ⟹ f ≤ ⇓ R g›
by (meson pw_ref_iff subset_eq)
lemma cdcl_twl_o_prog_l_spec:
‹(cdcl_twl_o_prog_l, cdcl_twl_o_prog) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →⇩f
⟨{((brk, T), (brk', T')). (T, T') ∈ twl_st_l None ∧ brk = brk' ∧ twl_list_invs T ∧
clauses_to_update_l T = {#}}⟩ nres_rel›
(is ‹ _ ∈ ?R →⇩f ?I› is ‹ _ ∈ ?R →⇩f ⟨?J⟩nres_rel›)
proof -
show ?thesis
(is ‹_ ∈ _ →⇩f ⟨?I'⟩ nres_rel›)
supply [[goals_limit=3]]
unfolding cdcl_twl_o_prog_l_def cdcl_twl_o_prog_def
find_unassigned_lit_def fref_param1[symmetric]
apply (refine_vcg
decide_l_or_skip_spec[THEN fref_to_Down, THEN "weaken_⇓'"]
skip_and_resolve_loop_l_spec[THEN fref_to_Down]
backtrack_l_spec[THEN fref_to_Down]; remove_dummy_vars)
subgoal for S S'
unfolding cdcl_twl_o_prog_l_pre_def cdcl_twl_o_prog_pre_def by (rule exI[of _ S']) (force simp: twl_st_l)
subgoal by auto
subgoal unfolding cdcl_twl_o_prog_pre_def by auto
subgoal by auto
subgoal by auto
subgoal unfolding cdcl_twl_o_prog_pre_def by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
section ‹Full Strategy›
definition cdcl_twl_stgy_prog_l_inv :: ‹'v twl_st_l ⇒ bool × 'v twl_st_l ⇒ bool› where
‹cdcl_twl_stgy_prog_l_inv S⇩0 ≡ λ(brk, T). ∃S⇩0' T'. (T, T') ∈ twl_st_l None ∧
(S⇩0, S⇩0') ∈ twl_st_l None ∧
twl_struct_invs T' ∧
twl_stgy_invs T' ∧
(brk ⟶ final_twl_state T') ∧
cdcl_twl_stgy⇧*⇧* S⇩0' T' ∧
clauses_to_update_l T = {#} ∧
(¬brk ⟶ get_conflict_l T = None)›
definition cdcl_twl_stgy_prog_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹cdcl_twl_stgy_prog_l S⇩0 =
do {
do {
(brk, T) ← WHILE⇩T⇗cdcl_twl_stgy_prog_l_inv S⇩0⇖
(λ(brk, _). ¬brk)
(λ(brk, S).
do {
T ← unit_propagation_outer_loop_l S;
cdcl_twl_o_prog_l T
})
(False, S⇩0);
RETURN T
}
}
›
lemma cdcl_twl_stgy_prog_l_spec:
‹(cdcl_twl_stgy_prog_l, cdcl_twl_stgy_prog) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →⇩f
⟨{(T, T'). (T, T') ∈ {(T, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T} ∧ True}⟩ nres_rel›
(is ‹ _ ∈ ?R →⇩f ?I› is ‹ _ ∈ ?R →⇩f ⟨?J⟩nres_rel›)
proof -
have R: ‹(a, b) ∈ ?R ⟹
((False, a), (False, b)) ∈ {((brk, S), (brk', S')). brk = brk' ∧ (S, S') ∈ ?R}›
for a b by auto
show ?thesis
unfolding cdcl_twl_stgy_prog_l_def cdcl_twl_stgy_prog_def cdcl_twl_o_prog_l_spec
fref_param1[symmetric] cdcl_twl_stgy_prog_l_inv_def
apply (refine_rcg R cdcl_twl_o_prog_l_spec[THEN fref_to_Down, THEN "weaken_⇓'"]
unit_propagation_outer_loop_l_spec[THEN fref_to_Down]; remove_dummy_vars)
subgoal for S⇩0 S⇩0' T T'
apply (rule exI[of _ S⇩0'])
apply (rule exI[of _ ‹snd T›])
by (auto simp add: case_prod_beta)
subgoal by auto
subgoal by fastforce
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma refine_pair_to_SPEC:
fixes f :: ‹'s ⇒ 's nres› and g :: ‹'b ⇒ 'b nres›
assumes ‹(f, g) ∈ {(S, S'). (S, S') ∈ H ∧ R S S'} →⇩f ⟨{(S, S'). (S, S') ∈ H' ∧ P' S}⟩nres_rel›
(is ‹_ ∈ ?R →⇩f ?I›)
assumes ‹R S S'› and [simp]: ‹(S, S') ∈ H›
shows ‹f S ≤ ⇓ {(S, S'). (S, S') ∈ H' ∧ P' S} (g S')›
proof -
have ‹(f S, g S') ∈ ?I›
using assms unfolding fref_def nres_rel_def by auto
then show ?thesis
unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
by auto
qed
definition cdcl_twl_stgy_prog_l_pre where
‹cdcl_twl_stgy_prog_l_pre S S' ⟷
((S, S') ∈ twl_st_l None ∧ twl_struct_invs S' ∧ twl_stgy_invs S' ∧
clauses_to_update_l S = {#} ∧ get_conflict_l S = None ∧ twl_list_invs S ∧
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S'))›
lemma cdcl_twl_stgy_prog_l_spec_final:
assumes
‹cdcl_twl_stgy_prog_l_pre S S'›
shows
‹cdcl_twl_stgy_prog_l S ≤ ⇓ (twl_st_l None) (conclusive_TWL_norestart_run S')›
apply (rule order_trans[OF cdcl_twl_stgy_prog_l_spec[THEN refine_pair_to_SPEC,
of S S']])
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal
apply (rule ref_two_step)
prefer 2
apply (rule cdcl_twl_stgy_prog_spec)
using assms unfolding cdcl_twl_stgy_prog_l_pre_def by (auto intro: conc_fun_R_mono)
done
lemma cdcl_twl_stgy_prog_l_spec_final':
assumes
‹cdcl_twl_stgy_prog_l_pre S S'›
shows
‹cdcl_twl_stgy_prog_l S ≤ ⇓ {(S, T). (S, T) ∈ twl_st_l None ∧ twl_list_invs S ∧
twl_struct_invs S' ∧ twl_stgy_invs S'} (conclusive_TWL_norestart_run S')›
apply (rule order_trans[OF cdcl_twl_stgy_prog_l_spec[THEN refine_pair_to_SPEC,
of S S']])
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal
apply (rule ref_two_step)
prefer 2
apply (rule cdcl_twl_stgy_prog_spec)
using assms unfolding cdcl_twl_stgy_prog_l_pre_def by (auto intro: conc_fun_R_mono)
done
definition cdcl_twl_stgy_prog_break_l :: ‹'v twl_st_l ⇒ 'v twl_st_l nres› where
‹cdcl_twl_stgy_prog_break_l S⇩0 =
do {
b ← SPEC(λ_. True);
(b, brk, T) ← WHILE⇩T⇗λ(b, S). cdcl_twl_stgy_prog_l_inv S⇩0 S⇖
(λ(b, brk, _). b ∧ ¬brk)
(λ(_, brk, S). do {
T ← unit_propagation_outer_loop_l S;
T ← cdcl_twl_o_prog_l T;
b ← SPEC(λ_. True);
RETURN (b, T)
})
(b, False, S⇩0);
if brk then RETURN T
else cdcl_twl_stgy_prog_l T
}›
lemma cdcl_twl_stgy_prog_break_l_spec:
‹(cdcl_twl_stgy_prog_break_l, cdcl_twl_stgy_prog_break) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →⇩f
⟨{(T, T'). (T, T') ∈ {(T, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T} ∧ True}⟩ nres_rel›
(is ‹ _ ∈ ?R →⇩f ?I› is ‹ _ ∈ ?R →⇩f ⟨?J⟩nres_rel›)
proof -
have R: ‹(a, b) ∈ ?R ⟹ (bb, bb') ∈ bool_rel ⟹
((bb, False, a), (bb', False, b)) ∈ {((b, brk, S), (b', brk', S')). b = b' ∧ brk = brk' ∧
(S, S') ∈ ?R}›
for a b bb bb' by auto
show ?thesis
supply [[goals_limit=1]]
unfolding cdcl_twl_stgy_prog_break_l_def cdcl_twl_stgy_prog_break_def cdcl_twl_o_prog_l_spec
fref_param1[symmetric] cdcl_twl_stgy_prog_l_inv_def
apply (refine_rcg cdcl_twl_o_prog_l_spec[THEN fref_to_Down]
unit_propagation_outer_loop_l_spec[THEN fref_to_Down]
cdcl_twl_stgy_prog_l_spec[THEN fref_to_Down]; remove_dummy_vars)
apply (rule R)
subgoal by auto
subgoal by auto
subgoal for S⇩0 S⇩0' b b' T T'
apply (rule exI[of _ S⇩0'])
apply (rule exI[of _ ‹snd (snd T)›])
by (auto simp add: case_prod_beta)
subgoal
by auto
subgoal by fastforce
subgoal by (auto simp: twl_st_l)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma cdcl_twl_stgy_prog_break_l_spec_final:
assumes
‹cdcl_twl_stgy_prog_l_pre S S'›
shows
‹cdcl_twl_stgy_prog_break_l S ≤ ⇓ (twl_st_l None) (conclusive_TWL_norestart_run S')›
apply (rule order_trans[OF cdcl_twl_stgy_prog_break_l_spec[THEN refine_pair_to_SPEC,
of S S']])
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal
apply (rule ref_two_step)
prefer 2
apply (rule cdcl_twl_stgy_prog_break_spec)
using assms unfolding cdcl_twl_stgy_prog_l_pre_def
by (auto intro: conc_fun_R_mono)
done
definition cdcl_twl_stgy_prog_early_l :: ‹'v twl_st_l ⇒ (bool × 'v twl_st_l) nres› where
‹cdcl_twl_stgy_prog_early_l S⇩0 =
do {
b ← SPEC(λ_. True);
(b, brk, T) ← WHILE⇩T⇗λ(b, S). cdcl_twl_stgy_prog_l_inv S⇩0 S⇖
(λ(b, brk, _). b ∧ ¬brk)
(λ(_, brk, S). do {
T ← unit_propagation_outer_loop_l S;
T ← cdcl_twl_o_prog_l T;
b ← SPEC(λ_. True);
RETURN (b, T)
})
(b, False, S⇩0);
RETURN (brk, T)
}›
lemma cdcl_twl_stgy_prog_early_l_spec:
‹(cdcl_twl_stgy_prog_early_l, cdcl_twl_stgy_prog_early) ∈
{(S, S'). (S, S') ∈ twl_st_l None ∧ twl_list_invs S ∧ clauses_to_update_l S = {#}} →⇩f
⟨bool_rel ×⇩r {(T, T'). (T, T') ∈ {(T, T'). (T, T') ∈ twl_st_l None ∧ twl_list_invs T} ∧ True}⟩ nres_rel›
(is ‹ _ ∈ ?R →⇩f ?I› is ‹ _ ∈ ?R →⇩f ⟨?J⟩nres_rel›)
proof -
have R: ‹(a, b) ∈ ?R ⟹ (bb, bb') ∈ bool_rel ⟹
((bb, False, a), (bb', False, b)) ∈ {((b, brk, S), (b', brk', S')). b = b' ∧ brk = brk' ∧
(S, S') ∈ ?R}›
for a b bb bb' by auto
show ?thesis
supply [[goals_limit=1]]
unfolding cdcl_twl_stgy_prog_early_l_def cdcl_twl_stgy_prog_early_def cdcl_twl_o_prog_l_spec
fref_param1[symmetric] cdcl_twl_stgy_prog_l_inv_def
apply (refine_rcg cdcl_twl_o_prog_l_spec[THEN fref_to_Down]
unit_propagation_outer_loop_l_spec[THEN fref_to_Down]
cdcl_twl_stgy_prog_l_spec[THEN fref_to_Down]; remove_dummy_vars)
apply (rule R)
subgoal by auto
subgoal by auto
subgoal for S⇩0 S⇩0' b b' T T'
apply (rule exI[of _ S⇩0'])
apply (rule exI[of _ ‹snd (snd T)›])
by (auto simp add: case_prod_beta)
subgoal
by auto
subgoal by fastforce
subgoal by (auto simp: twl_st_l)
subgoal by auto
subgoal by auto
done
qed
lemma refine_pair_to_SPEC2:
fixes f :: ‹'s ⇒ _ nres› and g :: ‹'b ⇒ (_) nres›
assumes ‹(f, g) ∈ {(S, S'). (S, S') ∈ H ∧ R S S'} →⇩f ⟨Id ×⇩r {(S, S'). (S, S') ∈ H' ∧ P' S}⟩nres_rel›
(is ‹_ ∈ ?R →⇩f ?I›)
assumes ‹R S S'› and [simp]: ‹(S, S') ∈ H›
shows ‹f S ≤ ⇓ (Id ×⇩r {(S, S'). (S, S') ∈ H' ∧ P' S}) (g S')›
proof -
have ‹(f S, g S') ∈ ?I›
using assms unfolding fref_def nres_rel_def by auto
then show ?thesis
unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
by auto
qed
lemma cdcl_twl_stgy_prog_early_l_spec_final:
assumes
‹cdcl_twl_stgy_prog_l_pre S S'›
shows
‹cdcl_twl_stgy_prog_early_l S ≤ ⇓ (bool_rel ×⇩r twl_st_l None) (partial_conclusive_TWL_norestart_run S')›
apply (rule order_trans[OF cdcl_twl_stgy_prog_early_l_spec[THEN refine_pair_to_SPEC2,
of S S']])
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal using assms unfolding cdcl_twl_stgy_prog_l_pre_def by auto
subgoal
apply (rule ref_two_step)
prefer 2
apply (rule cdcl_twl_stgy_prog_early_spec)
using assms unfolding cdcl_twl_stgy_prog_l_pre_def
by (auto intro: conc_fun_R_mono)
done
end