Theory IsaSAT_Simplify_Forward_Subsumption
theory IsaSAT_Simplify_Forward_Subsumption
imports IsaSAT_Setup
Watched_Literals.Watched_Literals_Watch_List_Inprocessing
More_Refinement_Libs.WB_More_Refinement_Loops
IsaSAT_Restart
IsaSAT_Simplify_Forward_Subsumption_Defs
begin
lemma subsume_clauses_match2_subsume_clauses_match:
assumes
‹(C, E) ∈ nat_rel›
‹(C', F) ∈ nat_rel› and
DG: ‹(D, G) ∈ clause_hash_ref (all_init_atms_st S)› and
N: ‹N = get_clauses_wl S› and
G: ‹G = mset (get_clauses_wl S ∝ C')› and
lin: ‹literals_are_ℒ⇩i⇩n' S›
shows ‹subsume_clauses_match2 C C' S D ≤ ⇓Id (subsume_clauses_match E F N)›
proof -
have eq: ‹E = C› ‹F = C'›
using assms by auto
have [simp]: ‹set_mset (all_init_atms_st S) = set_mset (all_atms_st S)›
using lin unfolding literals_are_ℒ⇩i⇩n'_def all_atms_st_alt_def
by (metis Un_subset_iff ℒ⇩a⇩l⇩l_all_atms ℒ⇩a⇩l⇩l_all_init_atms(2) all_atms_st_alt_def_sym
all_lits_st_init_learned atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n atms_of_cong_set_mset dual_order.antisym subset_refl)
have [intro!]: ‹C ∈# dom_m (get_clauses_wl S) ⟹ x1a < length (get_clauses_wl S ∝ C) ⟹
atm_of (get_clauses_wl S ∝ C ! x1a) ∈# all_atms_st S› for x1a
unfolding all_atms_st_alt_def
by (auto intro!: nth_in_all_lits_stI simp del: all_atms_st_alt_def[symmetric])
have [refine]: ‹((0, SUBSUMED_BY C), 0, SUBSUMED_BY C) ∈ nat_rel ×⇩f Id›
by auto
have subsume_clauses_match_alt_def:
‹subsume_clauses_match C C' N = do {
ASSERT (subsume_clauses_match_pre C C' N);
(i, st) ← WHILE⇩T⇗ λ(i,s). try_to_subsume C' C (N (C ↪ take i (N ∝ C))) s⇖ (λ(i, st). i < length (N ∝ C) ∧ st ≠ NONE)
(λ(i, st). do {
let L = N ∝ C ! i;
let lin = L ∈# mset (N ∝ C');
if lin
then RETURN (i+1, st)
else let lin = -L ∈# mset (N ∝ C') in
if lin
then if is_subsumed st
then RETURN (i+1, STRENGTHENED_BY L C)
else RETURN (i+1, NONE)
else RETURN (i+1, NONE)
})
(0, SUBSUMED_BY C);
RETURN st
}› for C C' N
unfolding subsume_clauses_match_def Let_def by (auto cong: if_cong)
have [refine]: ‹(x1a, x1) ∈ nat_rel ⟹ (get_clauses_wl S ∝ C ! x1a, get_clauses_wl S ∝ C ! x1) ∈ Id› for x1 x1a
by auto
show ?thesis
unfolding N subsume_clauses_match2_def subsume_clauses_match_alt_def Let_def[of ‹length _›] eq
mop_clauses_at_def nres_monad3
apply (refine_rcg DG[unfolded G] mop_ch_in)
subgoal using DG G unfolding subsume_clauses_match2_pre_def clause_hash_ref_def
by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: subsume_clauses_match_pre_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: subsume_clauses_match_pre_def)
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
qed
definition forward_subsumption_one_wl2_rel where
‹forward_subsumption_one_wl2_rel S⇩0 occs cands n C D = {((S, changed, occs', D'), (T, changed')). (¬changed ⟶ C ∈# dom_m (get_clauses_wl S)) ∧
changed = changed' ∧ set_mset (all_init_atms_st S) = set_mset (all_init_atms_st S⇩0) ∧
(changed ⟶ (D', {#}) ∈ clause_hash_ref (all_init_atms_st S)) ∧
(¬changed ⟶ D' = D ∧ occs' = occs ∧ get_clauses_wl S ∝ C = get_clauses_wl S⇩0 ∝ C) ∧
correct_occurence_list S occs' (if changed then remove1_mset C cands else cands)
(if changed then size (get_clauses_wl S⇩0 ∝ C) else n) ∧
all_occurrences (all_init_atms_st S) occs' ⊆# add_mset C (all_occurrences (all_init_atms_st S) occs) ∧
(S,T)∈Id
}›
lemma literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def:
‹literals_are_ℒ⇩i⇩n' S ⟹
set_mset (all_init_atms_st S) = set_mset (all_atms_st S)›
unfolding literals_are_ℒ⇩i⇩n'_def all_atms_st_alt_def
by (metis Un_subset_iff ℒ⇩a⇩l⇩l_all_atms ℒ⇩a⇩l⇩l_all_init_atms(2) all_atms_st_alt_def_sym
all_lits_st_init_learned atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n atms_of_cong_set_mset dual_order.antisym subset_refl)
lemma
inter_mset_empty_remove1_msetI:
‹A ∩# B = {#} ⟹ A ∩# remove1_mset c B = {#}› and
inter_mset_empty_removeAll_msetI:
‹A ∩# B = {#} ⟹ A ∩# removeAll_mset c B = {#}›
apply (meson disjunct_not_in in_diffD)
by (metis count_le_replicate_mset_subset_eq dual_order.refl inter_mset_empty_distrib_right
subset_mset.diff_add)
lemma push_to_occs_list2:
assumes occs: ‹correct_occurence_list S occs cands n›
‹C ∈# dom_m (get_clauses_wl S)›
‹2 ≤ length (get_clauses_wl S ∝ C)› and
lin: ‹literals_are_ℒ⇩i⇩n' S› and
undef: ‹∀L∈set (get_clauses_wl S ∝ C). undefined_lit (get_trail_wl S) L› and
notin: ‹C ∉# all_occurrences (mset_set (fst occs)) occs›
shows ‹push_to_occs_list2 C S occs ≤ SPEC (λc. (c, ()) ∈ {(occs', occs'').
all_occurrences (all_init_atms_st S) occs' = add_mset C (all_occurrences (all_init_atms_st S) occs) ∧
correct_occurence_list S occs' (remove1_mset C cands) (max n (length (get_clauses_wl S ∝ C))) ∧ fst occs = fst occs'})›
proof -
have 1: ‹atm_of ` set (get_clauses_wl S ∝ C) ⊆ set_mset (all_atms_st S)›
using nth_in_all_lits_stI[of C S] assms(2)
unfolding all_atms_st_alt_def
by (auto simp del: all_atms_st_alt_def[symmetric] simp: in_set_conv_nth)
moreover have ‹atm_of ` set (get_clauses_wl S ∝ C) ⊆ set_mset (all_init_atms_st S)›
using 1 lin unfolding literals_are_ℒ⇩i⇩n'_def by (simp add: lin literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def)
moreover have ‹L ∈ set (get_clauses_wl S ∝ C) ⟹
L ∈# all_init_lits_of_wl S› for L
by (metis ℒ⇩a⇩l⇩l_all_init_atms(2) calculation(2) image_subset_iff in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
ultimately show ?thesis
using literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def[OF lin]
unfolding push_to_occs_list2_def
apply (refine_vcg mop_occ_list_append[THEN order_trans])
subgoal using assms unfolding push_to_occs_list2_pre_def correct_occurence_list_def by fast
subgoal using assms unfolding occ_list_append_pre_def correct_occurence_list_def
by auto
subgoal for L occs'
using multi_member_split[of ‹atm_of L› ‹all_init_atms_st S›]
apply (subgoal_tac ‹atm_of L ∈# all_init_atms_st S›)
apply (cases occs)
by (use assms literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def[OF lin] in
‹auto 4 2 simp: occ_list_append_def correct_occurence_list_def
all_occurrences_add_mset occ_list_def all_occurrences_insert_lit
all_occurrences_occ_list_append_r distinct_mset_remove1_All all_init_atms_st_alt_def
intro: inter_mset_empty_removeAll_msetI›)
done
qed
lemma maybe_push_to_occs_list2:
assumes occs: ‹correct_occurence_list S occs cands n›
‹C ∈# dom_m (get_clauses_wl S)›
‹2 ≤ length (get_clauses_wl S ∝ C)› and
lin: ‹literals_are_ℒ⇩i⇩n' S› and
undef: ‹∀L∈set (get_clauses_wl S ∝ C). undefined_lit (get_trail_wl S) L› and
notin: ‹C ∉# all_occurrences (mset_set (fst occs)) occs›
shows ‹maybe_push_to_occs_list2 C S occs ≤ SPEC (λc. (c, ()) ∈ {(occs', occs'').
(all_occurrences (all_init_atms_st S) occs' = add_mset C (all_occurrences (all_init_atms_st S) occs) ∨
all_occurrences (all_init_atms_st S) occs' = all_occurrences (all_init_atms_st S) occs) ∧
correct_occurence_list S occs' (remove1_mset C cands) (max n (length (get_clauses_wl S ∝ C))) ∧ fst occs = fst occs'})›
proof -
have 1: ‹atm_of ` set (get_clauses_wl S ∝ C) ⊆ set_mset (all_atms_st S)›
using nth_in_all_lits_stI[of C S] assms(2)
unfolding all_atms_st_alt_def
by (auto simp del: all_atms_st_alt_def[symmetric] simp: in_set_conv_nth)
moreover have ‹atm_of ` set (get_clauses_wl S ∝ C) ⊆ set_mset (all_init_atms_st S)›
using 1 lin unfolding literals_are_ℒ⇩i⇩n'_def by (simp add: lin literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def)
moreover have ‹L ∈ set (get_clauses_wl S ∝ C) ⟹
L ∈# all_init_lits_of_wl S› for L
by (metis ℒ⇩a⇩l⇩l_all_init_atms(2) calculation(2) image_subset_iff in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
ultimately show ?thesis
using literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def[OF lin]
unfolding maybe_push_to_occs_list2_def
apply (refine_vcg mop_occ_list_append[THEN order_trans])
subgoal using assms unfolding push_to_occs_list2_pre_def correct_occurence_list_def by fast
subgoal using assms unfolding occ_list_append_pre_def correct_occurence_list_def
by auto
subgoal for keep L occs'
using multi_member_split[of ‹atm_of L› ‹all_init_atms_st S›]
apply (subgoal_tac ‹atm_of L ∈# all_init_atms_st S›)
apply (cases occs)
by (use assms literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def[OF lin] in
‹auto 4 2 simp: occ_list_append_def correct_occurence_list_def
all_occurrences_add_mset occ_list_def all_occurrences_insert_lit
all_occurrences_occ_list_append_r distinct_mset_remove1_All all_init_atms_st_alt_def
intro: inter_mset_empty_removeAll_msetI›)
subgoal for keep
using assms by (auto 4 2 simp: occ_list_append_def correct_occurence_list_def
all_occurrences_add_mset occ_list_def all_occurrences_insert_lit
all_occurrences_occ_list_append_r distinct_mset_remove1_All all_init_atms_st_alt_def
intro: inter_mset_empty_removeAll_msetI)
done
qed
definition forward_subsumption_one_wl2 :: ‹nat ⇒ nat multiset ⇒ nat literal ⇒ occurences ⇒ clause_hash ⇒
nat twl_st_wl ⇒ (nat twl_st_wl × bool × occurences × clause_hash) nres› where
‹forward_subsumption_one_wl2 = (λC cands L occs D S. do {
ASSERT (forward_subsumption_one_wl2_pre C cands L S);
ASSERT (atm_of L ∈ fst occs);
let ys = occ_list occs L;
let n = length ys;
(_, s) ←
WHILE⇩T⇗ forward_subsumption_one_wl2_inv S C cands ys ⇖ (λ(i, s). i < n ∧ s = NONE)
(λ(i, s). do {
C' ← mop_occ_list_at occs L i;
if C' ∉# dom_m (get_clauses_wl S)
then RETURN (i+1, s)
else do {
s ← subsume_clauses_match2 C' C S D;
RETURN (i+1, s)
}
})
(0, NONE);
D ← (if s ≠ NONE then mop_ch_remove_all (mset (get_clauses_wl S ∝ C)) D else RETURN D);
occs ← (if is_strengthened s then maybe_push_to_occs_list2 C S occs else RETURN occs);
S ← subsume_or_strengthen_wl C s S;
RETURN (S, s ≠ NONE, occs, D)
})›
lemma case_wl_split:
‹(case T of (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W) ⇒ P M N D NE UE NEk UEk NS US N0 U0 Q W) =
P (get_trail_wl T) (get_clauses_wl T) (get_conflict_wl T) (IsaSAT_Setup.get_unkept_unit_init_clss_wl T)
(IsaSAT_Setup.get_unkept_unit_learned_clss_wl T) (IsaSAT_Setup.get_kept_unit_init_clss_wl T)
(IsaSAT_Setup.get_kept_unit_learned_clss_wl T) (get_subsumed_init_clauses_wl T)
(get_subsumed_learned_clauses_wl T) (get_init_clauses0_wl T) (get_learned_clauses0_wl T)
(literals_to_update_wl T) (get_watched_wl T)› and
state_wl_recompose:
‹(get_trail_wl T, get_clauses_wl T, get_conflict_wl T, IsaSAT_Setup.get_unkept_unit_init_clss_wl T,
IsaSAT_Setup.get_unkept_unit_learned_clss_wl T, IsaSAT_Setup.get_kept_unit_init_clss_wl T,
IsaSAT_Setup.get_kept_unit_learned_clss_wl T, get_subsumed_init_clauses_wl T,
get_subsumed_learned_clauses_wl T, get_init_clauses0_wl T, get_learned_clauses0_wl T,
literals_to_update_wl T, get_watched_wl T) = T›
by (cases T; auto; fail)+
lemma clause_hash_ref_cong: ‹set_mset A = set_mset B ⟹ clause_hash_ref A = clause_hash_ref B› for A B
unfolding clause_hash_ref_def
by auto
lemma remdups_mset_set_mset_cong: ‹set_mset A = set_mset B ⟹ remdups_mset A = remdups_mset B› for A B
by (simp add: remdups_mset_def)
lemma all_occurrences_cong: ‹set_mset A = set_mset B ⟹ all_occurrences A = all_occurrences B› for A B
using remdups_mset_set_mset_cong[of A B]
unfolding all_occurrences_def
by auto
lemma correct_occurence_list_mono_candsI:
‹correct_occurence_list Sa occs (cands) n ⟹
correct_occurence_list Sa occs (remove1_mset C cands) n›
unfolding correct_occurence_list_def
by (auto intro: inter_mset_empty_remove1_msetI)
lemma correct_occurence_list_mono_candsI2:
‹correct_occurence_list Sa occs (add_mset C cands) n ⟹
correct_occurence_list Sa occs (cands) n›
unfolding correct_occurence_list_def
by auto
lemma correct_occurence_list_size_mono:
‹correct_occurence_list x1h occs cands n ⟹ m ≥ n ⟹
correct_occurence_list x1h occs cands m›
by (auto simp: correct_occurence_list_def ball_conj_distrib dest!: multi_member_split)
lemma all_occurrences_remove_dups_atms[simp]:
‹set_mset (all_occurrences (mset_set (set_mset (all_init_atms_st S⇩0))) occs) =
set_mset (all_occurrences (all_init_atms_st S⇩0) occs)›
unfolding all_occurrences_def
by (cases occs) auto
lemma forward_subsumption_one_wl2_forward_subsumption_one_wl:
fixes S⇩0 C
defines G: ‹G ≡ mset (get_clauses_wl S⇩0 ∝ C)›
assumes
‹(C, E) ∈ nat_rel› and
DG: ‹(D, G) ∈ clause_hash_ref (all_init_atms_st S⇩0)› and
occs: ‹correct_occurence_list S⇩0 occs cands n› and
n: ‹n≤ size (get_clauses_wl S⇩0 ∝ C)› and
C_occs: ‹C ∉# all_occurrences (all_init_atms_st S⇩0) occs› and
L: ‹atm_of L ∈# all_init_atms_st S⇩0› and
‹(S⇩0, T⇩0) ∈ Id›
‹(cands, cands') ∈ Id›
shows ‹forward_subsumption_one_wl2 C cands L occs D S⇩0 ≤ ⇓
(forward_subsumption_one_wl2_rel S⇩0 occs cands n C D)
(forward_subsumption_one_wl E cands' T⇩0)›
proof -
have ‹cands ∩# mset (occ_list occs L) = {#}›
using occs L n unfolding correct_occurence_list_def
by (auto simp: all_occurrences_add_mset inter_mset_empty_distrib_right subset_mset.inf.commute
dest!: multi_member_split[of ‹atm_of L›])
then have [refine]:
‹RETURN (occ_list occs L)
≤ ⇓ list_mset_rel (SPEC (forward_subsumption_one_wl_select C cands S⇩0))›
using occs C_occs L n unfolding forward_subsumption_one_wl_select_def
by (auto simp: correct_occurence_list_def all_occurrences_add_mset
forward_subsumption_one_select_def list_mset_rel_def br_def
dest!: multi_member_split
intro!: RETURN_RES_refine
intro: le_trans[OF _ n])
have [refine]: ‹(occ_list occs L, ys) ∈ list_mset_rel ⟹
((0, NONE), ys, NONE) ∈ {(n, z). z = mset (drop n (occ_list occs L))} ×⇩f Id› for ys
by (auto simp: list_mset_rel_def br_def)
define ISABELLE_YOU_ARE_SO_STUPID :: ‹nat multiset ⇒ _› where
‹ISABELLE_YOU_ARE_SO_STUPID xs = SPEC (λC'. C' ∈# xs)› for xs
have H: ‹(if s ≠ NONE then RETURN ({#} :: nat clause) else RETURN G) =
RETURN ((if s ≠ NONE then ({#} :: nat clause) else G))› for s
by auto
have forward_subsumption_one_wl_alt_def:
‹forward_subsumption_one_wl = (λC cands S⇩0. do {
ASSERT (forward_subsumption_one_wl_pre C cands S⇩0);
ys ← SPEC (forward_subsumption_one_wl_select C cands S⇩0);
let _ = size ys;
(xs, s) ←
WHILE⇩T⇗ forward_subsumption_one_wl_inv S⇩0 C ys ⇖ (λ(xs, s). xs ≠ {#} ∧ s = NONE)
(λ(xs, s). do {
C' ←ISABELLE_YOU_ARE_SO_STUPID xs;
if C' ∉# dom_m (get_clauses_wl S⇩0)
then RETURN (remove1_mset C' xs, s)
else do {
s ← subsume_clauses_match C' C (get_clauses_wl S⇩0);
RETURN (remove1_mset C' xs, s)
}
})
(ys, NONE);
_ ← RETURN (if s ≠ NONE then ({#} :: nat clause) else G);
let _ = (if is_strengthened s then () else ());
S ← subsume_or_strengthen_wl C s S⇩0;
ASSERT
(literals_are_ℒ⇩i⇩n' S ∧
set_mset (all_init_lits_of_wl S) = set_mset (all_init_lits_of_wl S⇩0));
RETURN (S, s ≠ NONE)
})›
unfolding forward_subsumption_one_wl_def ISABELLE_YOU_ARE_SO_STUPID_def bind_to_let_conv H
by (auto split: intro!: bind_cong[OF refl] ext)
have ISABELLE_YOU_ARE_SO_STUPID: ‹(x, x') ∈ {(n, z). z = mset (drop n (occ_list occs L))} ×⇩f Id ⟹
case x of (i, s) ⇒ i < length (occ_list occs L) ∧ s = NONE ⟹
x' = (x1, x2) ⟹
x = (x1a, x2a) ⟹
SPEC (λc. (c, occ_list_at occs L x1a) ∈ nat_rel)
≤ ⇓ {(a,b). a = b ∧ b = occ_list_at occs L x1a}
(ISABELLE_YOU_ARE_SO_STUPID x1)› for x1 x1a x x' x2 x2a
by (cases occs, auto simp: ISABELLE_YOU_ARE_SO_STUPID_def occ_list_at_def occ_list_def
RES_refine
intro!: in_set_dropI RES_refine)
have H: ‹is_strengthened x2a ⟹
(xa, ()) ∈ R ⟹
(xa, if is_strengthened x2 then () else ()) ∈ (if ¬is_strengthened x2a then {(a,b). a = occs} else R)› for xa x2 x2a R
by auto
have itself: ‹subsume_or_strengthen_wl C s S ≤⇓{(x,y). x = y ∧
get_trail_wl x = get_trail_wl S ∧ (¬is_subsumed s ⟶ C∈#dom_m (get_clauses_wl x)) ∧
(s = NONE ⟶ x = S) ∧
(dom_m (get_clauses_wl x) ⊆# dom_m (get_clauses_wl S)) ∧
(∀Ca∈#dom_m (get_clauses_wl x). Ca∈#dom_m (get_clauses_wl S) ∧ length (get_clauses_wl x ∝ Ca) ≤ length (get_clauses_wl S ∝ Ca)) ∧
(∀Ca∈#dom_m (get_clauses_wl x). Ca∈#dom_m (get_clauses_wl S) ∧ set (get_clauses_wl x ∝ Ca) ⊆ set (get_clauses_wl S ∝ Ca))
} b› if b: ‹b = subsume_or_strengthen_wl C s S› and
S: ‹forward_subsumption_one_wl_pre C ys S›
for a b s S ys
proof -
have [simp]: ‹x1 ∈# dom_m b ⟹ {#mset (fst x). x ∈# ran_m (fmupd x1 (b ∝ x1, True) b)#} =
{#mset (fst x). x ∈# ran_m b#}› for b x1
by (auto simp: ran_m_def dest!: multi_member_split intro: image_mset_cong)
have [simp]:
‹get_conflict_wl S = None ⟹ (get_trail_wl S, get_clauses_wl S, None, IsaSAT_Setup.get_unkept_unit_init_clss_wl S,
IsaSAT_Setup.get_unkept_unit_learned_clss_wl S, IsaSAT_Setup.get_kept_unit_init_clss_wl S,
IsaSAT_Setup.get_kept_unit_learned_clss_wl S, get_subsumed_init_clauses_wl S,
get_subsumed_learned_clauses_wl S, get_init_clauses0_wl S, get_learned_clauses0_wl S,
literals_to_update_wl S, get_watched_wl S) = S› for S
by (cases S) auto
have [simp]: ‹C ∉# remove1_mset C (dom_m S)› for C S
using distinct_mset_dom[of ‹S›]
by (cases ‹C ∈# dom_m S›) (auto dest!: multi_member_split)
have H: ‹mset Ea = remove1_mset (- x21) (mset (get_clauses_wl S ∝ C)) ⟹
length (get_clauses_wl S ∝ C) = length (get_clauses_wl S ∝ x22) ⟹
length Ea ≤ length (get_clauses_wl S ∝ x22)›for Ea x21 S C x22
by (metis size_Diff1_le size_mset)
have H2: ‹mset Ea = remove1_mset (- x21) (mset (get_clauses_wl S ∝ C)) ⟹
x ∈ set Ea ⟹ x ∈ set (get_clauses_wl S ∝ C)›for Ea x21 S C x22 x
by (metis in_diffD in_multiset_in_set)
show ?thesis
unfolding subsume_or_strengthen_wl_def b strengthen_clause_wl_def case_wl_split
state_wl_recompose
apply refine_vcg
subgoal
using S unfolding forward_subsumption_one_wl_pre_def forward_subsumption_one_pre_def
subsume_or_strengthen_wl_pre_def subsume_or_strengthen_pre_def
apply -
apply normalize_goal+
subgoal for T U
apply (simp only: split: subsumption.splits)
apply (intro conjI)
subgoal
by refine_vcg
(auto split: subsumption.splits simp: state_wl_recompose)
subgoal
by (auto split: subsumption.splits simp: state_wl_recompose)
subgoal
by (auto split: subsumption.splits simp: state_wl_recompose)
subgoal
by refine_vcg
(auto split: subsumption.splits simp: state_wl_recompose
intro: H H2)
subgoal
by (auto split: subsumption.splits simp: state_wl_recompose)
done
done
done
qed
have mop_ch_remove_all2:
‹mop_ch_remove_all D C ≤ SPEC(λc. (c, {#}) ∈ clause_hash_ref 𝒜)›
if ‹(C, D) ∈ clause_hash_ref 𝒜› for C D 𝒜
using that unfolding mop_ch_remove_all_def
apply refine_vcg
subgoal by (auto simp: clause_hash_ref_def ch_remove_all_def)
subgoal by (auto simp: clause_hash_ref_def ch_remove_all_def dest!: multi_member_split)
subgoal by (auto simp: clause_hash_ref_def ch_remove_all_def)
done
have K: ‹(xa, {#}) ∈ clause_hash_ref (all_init_atms_st S⇩0) ⟹ x2 ≠ NONE ⟹
(xa, if x2 ≠ NONE then {#} else G) ∈
{(xa, b). if x2 ≠ NONE then b = {#} ∧ (xa, b)∈ clause_hash_ref (all_init_atms_st S⇩0)
else (xa,b) = (D,G)}› for xa x2
by auto
have correct_occurence_list_cong:
‹correct_occurence_list T occs ys (length (get_clauses_wl S⇩0 ∝ C)) ⟹
set_mset (all_init_atms_st T) = set_mset (all_init_atms_st U) ⟹
get_trail_wl T = get_trail_wl U ⟹
dom_m (get_clauses_wl U) ⊆# dom_m (get_clauses_wl T) ⟹
(∀Ca∈#dom_m (get_clauses_wl U). Ca∈#dom_m (get_clauses_wl T) ∧ length (get_clauses_wl U ∝ Ca) ≤ length (get_clauses_wl T ∝ Ca)) ⟹
(∀Ca∈#dom_m (get_clauses_wl U). Ca∈#dom_m (get_clauses_wl T) ∧ set (get_clauses_wl U ∝ Ca) ⊆ set (get_clauses_wl T ∝ Ca)) ⟹
correct_occurence_list U occs ys (length (get_clauses_wl S⇩0 ∝ C))› for T U occs ys
using remdups_mset_set_mset_cong[of ‹all_init_atms_st T› ‹all_init_atms_st U›]
all_occurrences_cong[of ‹all_init_atms_st T› ‹all_init_atms_st U›] n
unfolding correct_occurence_list_def
apply (cases occs)
apply (auto)
apply (meson mset_subset_eqD order_trans)
apply (meson mset_subset_eqD subsetD)
done
have eq: ‹T⇩0 = S⇩0› ‹E = C› ‹cands' = cands›
using assms by auto
show ?thesis
unfolding forward_subsumption_one_wl2_def eq
forward_subsumption_one_wl_alt_def
apply (refine_vcg mop_occ_list_at[THEN order_trans] DG mop_ch_remove_all2 occs
subsume_clauses_match2_subsume_clauses_match maybe_push_to_occs_list2 DG[unfolded G])
subgoal
using assms ℒ⇩a⇩l⇩l_all_init_atms(2) in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n
unfolding forward_subsumption_one_wl2_pre_def by blast
subgoal
using assms occs
by (auto simp: correct_occurence_list_def)
subgoal for ys x x'
unfolding forward_subsumption_one_wl2_inv_def
by (cases x') (auto simp: list_mset_rel_def br_def)
subgoal by auto
subgoal using occs L unfolding occ_list_at_pre_def correct_occurence_list_def
by (cases occs, auto simp: occ_list_def)
apply (rule ISABELLE_YOU_ARE_SO_STUPID)
apply assumption+
subgoal by (cases occs, auto simp: occ_list_at_def occ_list_def in_set_dropI)
subgoal by (auto simp flip: Cons_nth_drop_Suc occ_list_at_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using G by auto
subgoal unfolding forward_subsumption_one_wl_pre_def by blast
subgoal by (auto simp flip: Cons_nth_drop_Suc occ_list_at_def)
apply (rule K; assumption?)
subgoal by auto
subgoal by auto
subgoal unfolding forward_subsumption_one_wl_pre_def forward_subsumption_one_pre_def
by normalize_goal+ simp
subgoal unfolding forward_subsumption_one_wl_pre_def forward_subsumption_one_pre_def
by normalize_goal+ simp
subgoal unfolding forward_subsumption_one_wl_pre_def by blast
subgoal unfolding forward_subsumption_one_wl_pre_def forward_subsumption_one_pre_def
by normalize_goal+ simp
subgoal using C_occs occs unfolding correct_occurence_list_def by auto
apply (rule H; assumption)
subgoal by auto
apply (rule itself)
subgoal by auto
apply assumption
subgoal for ys x x' x1 x2 x1a x2a Da _ occsa S Sa
using occs n
clause_hash_ref_cong[of ‹all_init_atms_st S⇩0› ‹atm_of `# all_init_lits_of_wl Sa›]
all_occurrences_cong[of ‹all_init_atms_st S⇩0› ‹atm_of `# all_init_lits_of_wl Sa›]
by (auto simp: forward_subsumption_one_wl2_rel_def all_init_atms_st_alt_def
correct_occurence_list_cong[of S⇩0]
intro: correct_occurence_list_size_mono intro!: correct_occurence_list_mono_candsI
simp del: multiset.set_map
intro: correct_occurence_list_cong
split: if_splits)
done
qed
definition try_to_forward_subsume_wl2 :: ‹nat ⇒ occurences ⇒ nat multiset ⇒ clause_hash ⇒ nat multiset ⇒ nat twl_st_wl ⇒ (occurences × clause_hash × nat multiset × nat twl_st_wl) nres› where
‹try_to_forward_subsume_wl2 C occs cands D shrunken S = do {
ASSERT (try_to_forward_subsume_wl2_pre C cands shrunken S);
let n = length (get_clauses_wl S ∝ C);
let n = 2 * n;
ebreak ← RES {_::bool. True};
(_, changed, _, occs, D, S) ← WHILE⇩T⇗ try_to_forward_subsume_wl2_inv S cands C⇖
(λ(i, changed, break, occs, D, S). ¬break ∧ i < n)
(λ(i, changed, break, occs, D, S). do {
L ← mop_clauses_at (get_clauses_wl S) C (i div 2);
let L = (if i mod 2 = 0 then L else - L);
(S, subs, occs, D) ← forward_subsumption_one_wl2 C cands L occs D S;
ebreak ← RES {_::bool. True};
RETURN (i+1, subs, subs ∨ ebreak, occs, D, S)
})
(0, False, ebreak, occs, D, S);
ASSERT (¬changed ⟶ C ∈# dom_m (get_clauses_wl S));
D ← (if ¬changed then mop_ch_remove_all (mset (get_clauses_wl S ∝ C)) D else RETURN D);
add_to_shrunken ← RES (UNIV :: bool set);
let shrunken = (if add_to_shrunken then add_mset C shrunken else shrunken);
RETURN (occs, D, shrunken, S)
}›
definition try_to_forward_subsume_wl2_pre0 :: ‹_› where
‹try_to_forward_subsume_wl2_pre0 G C occs cands D S⇩0 n ⟷
correct_occurence_list S⇩0 occs cands n ∧
n≤ length (get_clauses_wl S⇩0 ∝ C) ∧
C ∉# all_occurrences (all_init_atms_st S⇩0) occs ∧
distinct_mset cands ∧
C ∈# dom_m (get_clauses_wl S⇩0) ∧
G = mset (get_clauses_wl S⇩0 ∝ C)›
definition try_to_forward_subsume_wl_rel :: ‹_› where
‹try_to_forward_subsume_wl_rel S⇩0 C cands occs n shrunken ≡
{((occs', D', shrunken', T), U). (T, U) ∈ Id ∧ (D', {#}) ∈ clause_hash_ref (all_init_atms_st T) ∧
correct_occurence_list U occs' (remove1_mset C cands) (max (length (get_clauses_wl S⇩0 ∝ C)) n) ∧
shrunken' ⊆# add_mset C shrunken ∧
all_occurrences (all_init_atms_st U) occs' ⊆# add_mset C (all_occurrences (all_init_atms_st S⇩0) occs)}›
lemma try_to_forward_subsume_wl2_try_to_forward_subsume_wl:
assumes ‹(C, E) ∈ nat_rel› and
DG: ‹(D, G) ∈ clause_hash_ref (all_init_atms_st T⇩0)› and
pre: ‹try_to_forward_subsume_wl2_pre0 G C occs cands D S⇩0 n› and
‹(S⇩0, T⇩0) ∈ Id›
‹(cands, cands') ∈ Id›
shows ‹try_to_forward_subsume_wl2 C occs cands D shrunken S⇩0 ≤
⇓(try_to_forward_subsume_wl_rel S⇩0 C cands occs n shrunken)
(try_to_forward_subsume_wl E cands' T⇩0)›
proof -
have eq: ‹T⇩0 = S⇩0› ‹E = C› ‹cands' = cands›
using assms by auto
have
occs: ‹correct_occurence_list S⇩0 occs cands n› and
n: ‹n≤ length (get_clauses_wl S⇩0 ∝ C)› and
C_occs: ‹C ∉# all_occurrences (all_init_atms_st T⇩0) occs› and
‹distinct_mset cands› and
G: ‹G = mset (get_clauses_wl S⇩0 ∝ C)›
using pre unfolding try_to_forward_subsume_wl2_pre0_def eq
by auto
have try_to_forward_subsume_wl_alt_def:
‹try_to_forward_subsume_wl C cands S = do {
ASSERT (try_to_forward_subsume_wl_pre C cands S);
n ← RES {_::nat. True};
ebreak ← RES {_::bool. True};
(_, _, S) ← WHILE⇩T⇗ try_to_forward_subsume_wl_inv S cands C⇖
(λ(i, break, S). ¬break ∧ i < n)
(λ(i, break, S). do {
_ ← SPEC (λL :: nat literal. True);
(S, subs) ← forward_subsumption_one_wl C cands S;
ebreak ← RES {_::bool. True};
RETURN (i+1, subs ∨ ebreak, S)
})
(0, ebreak, S);
_ ← RETURN ({#} :: nat clause);
RETURN S
}
› for S
unfolding try_to_forward_subsume_wl_def nres_monad3
by auto
have [refine]: ‹(ebreak, ebreaka) ∈ bool_rel ⟹ try_to_forward_subsume_wl_pre C cands S⇩0 ⟹
((0, False, ebreak, occs, D, S⇩0), 0, ebreaka, S⇩0) ∈
{((p, changed, ebreak, occs', D', U), (q, ebreak', V)). (p,q)∈nat_rel ∧ (¬changed ⟶ C∈#dom_m (get_clauses_wl U)) ∧
(¬changed ⟶ (D', mset (get_clauses_wl U ∝ C)) ∈ clause_hash_ref (all_init_atms_st U)) ∧
(changed ⟶ ebreak ∧ (D', {#}) ∈ clause_hash_ref (all_init_atms_st U)) ∧
(ebreak, ebreak') ∈ bool_rel ∧
(¬changed ⟶ correct_occurence_list U occs' cands n ∧ occs' = occs ∧ get_clauses_wl U ∝ C = get_clauses_wl S⇩0 ∝ C ∧
all_occurrences (all_init_atms_st V) occs' = all_occurrences (all_init_atms_st S⇩0) occs) ∧
(changed ⟶ correct_occurence_list U occs' (remove1_mset C cands) (max (length (get_clauses_wl S⇩0 ∝ C)) n) ∧
all_occurrences (all_init_atms_st V) occs' ⊆# add_mset C (all_occurrences (all_init_atms_st S⇩0) occs)) ∧
U = V}› (is ‹_ ⟹ _ ⟹ _ ∈ ?R›)
for ebreak ebreaka
using assms unfolding try_to_forward_subsume_wl_pre_def try_to_forward_subsume_pre_def
by - (normalize_goal+; simp add: try_to_forward_subsume_wl2_pre0_def try_to_forward_subsume_wl_pre_def)
have try_to_forward_subsume_wl2_invD:
‹try_to_forward_subsume_wl2_inv S⇩0 cands C x ⟹ set_mset (all_init_atms_st (snd (snd (snd (snd (snd x)))))) = set_mset
(all_init_atms_st S⇩0)› for x
unfolding try_to_forward_subsume_wl2_inv_def
try_to_forward_subsume_wl_inv_def
try_to_forward_subsume_inv_def case_prod_beta
apply normalize_goal+
apply (frule rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l)
by (simp add: all_init_atms_st_alt_def)
have H: ‹C ∈# dom_m (get_clauses_wl x2a) ⟹ x1 < 2 * length (get_clauses_wl x2a ∝ C) ⟹
atm_of (get_clauses_wl x2a ∝ C ! (x1 div 2))
∈ atm_of `
(set_mset (all_lits_of_m (mset (get_clauses_wl x2a ∝ C))))› for x1 x2a
by (rule imageI)
(auto intro!: in_clause_in_all_lits_of_m nth_mem)
have K: ‹try_to_forward_subsume_wl_inv S⇩0 cands C (x1, False, x2a) ⟹
x1 < 2 * length (get_clauses_wl x2a ∝ C) ⟹
atm_of (get_clauses_wl x2a ∝ C ! (x1 div 2)) ∈# all_init_atms_st x2a› for x1 x2a
using H[of x2a x1]
unfolding try_to_forward_subsume_wl_inv_def prod.simps try_to_forward_subsume_inv_def
literals_are_ℒ⇩i⇩n'_def apply -
apply normalize_goal+
apply (frule rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l,
frule rtranclp_cdcl_twl_inprocessing_l_all_learned_lits_of_l)
apply (simp add: all_init_atms_st_alt_def)
apply (auto simp: all_init_atms_st_def ran_m_def all_init_atms_alt_def all_init_atms_def
all_init_lits_of_wl_def
all_init_lits_def all_lits_of_mm_add_mset all_learned_lits_of_wl_def
dest!: multi_member_split[of C]
simp del: all_init_atms_def[symmetric] all_init_lits_of_wl_def[symmetric])
by blast
have K0: ‹try_to_forward_subsume_wl_inv S⇩0 cands C (x1, False, x2a) ⟹
atm_of ` set (get_clauses_wl x2a ∝ C) ⊆ set_mset (all_init_atms_st x2a)› for x1 x2a
unfolding try_to_forward_subsume_wl_inv_def prod.simps try_to_forward_subsume_inv_def
literals_are_ℒ⇩i⇩n'_def apply -
apply normalize_goal+
apply (frule rtranclp_cdcl_twl_inprocessing_l_all_init_lits_of_l,
frule rtranclp_cdcl_twl_inprocessing_l_all_learned_lits_of_l)
apply (simp add: all_init_atms_st_alt_def)
apply (auto simp: all_init_atms_st_def ran_m_def all_init_atms_alt_def all_init_atms_def
all_init_lits_of_wl_def
all_init_lits_def all_lits_of_mm_add_mset all_learned_lits_of_wl_def in_clause_in_all_lits_of_m
dest!: multi_member_split[of C]
simp del: all_init_atms_def[symmetric] all_init_lits_of_wl_def[symmetric])
by (meson image_eqI in_clause_in_all_lits_of_m in_multiset_in_set subsetD)
have mop_ch_remove_all2:
‹(x, x') ∈ ?R ⟹
x2 = (x1a, x2a) ⟹
x' = (x1, x2) ⟹
x2e = (x1f, x2f) ⟹
x2d = (x1e, x2e) ⟹
x2c = (x1d, x2d) ⟹
x2b = (x1c, x2c) ⟹
x = (x1b, x2b) ⟹ ¬x1c ⟹
mop_ch_remove_all (mset (get_clauses_wl x2f ∝ C)) x1f ≤ SPEC(λc. (c, {#}) ∈ {(a,b). b = {#} ∧ (a,b) ∈ clause_hash_ref (all_init_atms_st x2f)})›
for na ebreak ebreaka x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f
unfolding mop_ch_remove_all_def
apply refine_vcg
subgoal
using DG G
by (auto simp: clause_hash_ref_def ch_remove_all_def)
subgoal by (auto 5 3 simp add: clause_hash_ref_def)
subgoal
by (auto simp: clause_hash_ref_def ch_remove_all_def)
done
show ?thesis
unfolding try_to_forward_subsume_wl2_def try_to_forward_subsume_wl_alt_def eq mop_clauses_at_def
nres_monad3 bind_to_let_conv try_to_forward_subsume_wl_rel_def
apply (subst Let_def[of ‹get_clauses_wl _ ∝ _ ! _›])
apply (subst Let_def[of ‹length (get_clauses_wl _ ∝ _)›])
apply (refine_vcg DG[unfolded G]
forward_subsumption_one_wl2_forward_subsumption_one_wl[where n=n])
subgoal using assms unfolding try_to_forward_subsume_wl2_pre_def try_to_forward_subsume_wl2_pre0_def by fast
subgoal by fast
subgoal using G unfolding try_to_forward_subsume_wl2_inv_def by auto
subgoal by auto
subgoal unfolding try_to_forward_subsume_wl_inv_def case_prod_beta try_to_forward_subsume_inv_def
by normalize_goal+ auto
subgoal by auto
subgoal by fast
subgoal by fast
subgoal by fast
subgoal by auto
subgoal using n by auto
subgoal using C_occs by (auto dest: all_occurrences_cong[OF try_to_forward_subsume_wl2_invD] simp: eq)
subgoal for a ebreak ebreaka x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f
using K[of x1 x2a] by auto
subgoal by auto
subgoal by auto
subgoal for na ebreak ebreaka x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f uu_ xa x'a x1g x2g x1h x2h x1i x2i
x1j x2j ebreakb ebreakc
apply (frule all_occurrences_cong[OF try_to_forward_subsume_wl2_invD])
apply (clarsimp simp add: forward_subsumption_one_wl2_rel_def)
apply (auto dest:
intro: correct_occurence_list_size_mono[of _ _ _ _ ‹(max (length (get_clauses_wl S⇩0 ∝ C)) n)›]
simp: clause_hash_ref_cong[of ‹all_init_atms_st x1g›]
all_occurrences_cong[of ‹all_init_atms_st x1g› ‹all_init_atms_st x2a›]
forward_subsumption_one_wl2_rel_def
simp: )
done
subgoal
apply simp
by auto
apply (rule mop_ch_remove_all2; assumption)
subgoal by auto
subgoal for na ebreak ebreaka x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f
using n by (auto simp: eq intro: correct_occurence_list_size_mono correct_occurence_list_mono_candsI)
done
qed
definition populate_occs_spec where
‹populate_occs_spec S = (λ(occs, cands).
all_occurrences (all_init_atms_st S) occs + mset cands ⊆# dom_m (get_clauses_wl S) ∧
distinct cands ∧ sorted_wrt (λa b. length (get_clauses_wl S ∝ a) ≤ length (get_clauses_wl S ∝ b)) cands ∧
correct_occurence_list S occs (mset cands) 2 ∧
(∀C∈set cands. ∀L∈ set (get_clauses_wl S ∝ C). undefined_lit (get_trail_wl S) L) ∧
(∀C∈set cands. length (get_clauses_wl S ∝ C) > 2))›
definition all_lit_clause_unset :: ‹_› where
‹all_lit_clause_unset S C = do {
ASSERT (forward_subsumption_all_wl_pre S);
let b = C ∈# dom_m (get_clauses_wl S);
if ¬b then RETURN False
else do {
let n = length (get_clauses_wl S ∝ C);
(i, all_undef) ← WHILE⇩T (λ(i, all_undef). i < n ∧ all_undef)
(λ(i, _). do {
ASSERT (i<n);
L ← mop_clauses_at (get_clauses_wl S) C i;
ASSERT (L ∈# ℒ⇩a⇩l⇩l (all_init_atms_st S));
val ← mop_polarity_wl S L;
RETURN (i+1, val = None)
}) (0, True);
other ← SPEC (λ_. True);
RETURN (all_undef ∧ other)
}
}›
lemma forward_subsumption_all_wl_preD: ‹forward_subsumption_all_wl_pre S ⟹ no_dup (get_trail_wl S)›
unfolding forward_subsumption_all_wl_pre_def
forward_subsumption_all_pre_def twl_list_invs_def
twl_struct_invs_def pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by normalize_goal+ simp
lemma all_lit_clause_unset_spec:
‹forward_subsumption_all_wl_pre S ⟹
all_lit_clause_unset S C ≤ SPEC (λb. b ⟶ C∈#dom_m (get_clauses_wl S) ∧ (∀L∈set (get_clauses_wl S ∝ C). undefined_lit (get_trail_wl S) L))›
unfolding all_lit_clause_unset_def mop_clauses_at_def nres_monad3 mop_polarity_wl_def
apply (refine_vcg WHILET_rule[where R=‹measure (λ(i,_). length (get_clauses_wl S ∝ C) -i)› and
I=‹λ(i, all_undef). i ≤ length (get_clauses_wl S ∝ C) ∧
(all_undef ⟷ (∀L∈set (take i (get_clauses_wl S ∝ C)). undefined_lit (get_trail_wl S) L))›])
subgoal by fast
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal
using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(3)[of S, THEN ℒ⇩a⇩l⇩l_cong]
unfolding forward_subsumption_all_wl_pre_def
forward_subsumption_all_pre_def apply -
by normalize_goal+
(simp add: ℒ⇩a⇩l⇩l_all_atms)
subgoal by auto
subgoal by (auto dest: forward_subsumption_all_wl_preD)
subgoal by (auto dest: forward_subsumption_all_wl_preD)
subgoal by (auto simp: take_Suc_conv_app_nth polarity_def split: if_splits)
subgoal by auto
subgoal by auto
subgoal by auto
done
definition populate_occs :: ‹nat twl_st_wl ⇒ _ nres› where
‹populate_occs S = do {
ASSERT (forward_subsumption_all_wl_pre S);
xs ← SPEC (λxs. distinct xs);
let n = size xs;
occs ← mop_occ_list_create (set_mset (all_init_atms_st S));
let cands = [];
(_, occs, cands) ← WHILE⇩T⇗populate_occs_inv S xs⇖ (λ(i, occs, cands). i < n)
(λ(i, occs, cands). do {
let C = xs ! i;
ASSERT (C ∉ set cands);
all_undef ← all_lit_clause_unset S C;
if ¬all_undef then
RETURN (i+1, occs, cands)
else do {
ASSERT(C ∈# dom_m (get_clauses_wl S));
let le = length (get_clauses_wl S ∝ C) in
if le = 2 then do {
occs ← push_to_occs_list2 C S occs;
RETURN (i+1, occs, cands)
}
else do {
ASSERT(C ∈# dom_m (get_clauses_wl S));
cand ← RES (UNIV::bool set);
if cand then RETURN (i+1, occs, cands @ [C])
else RETURN (i+1, occs, cands)
}
}
}
)
(0, occs, cands);
ASSERT (∀C∈set cands. C∈#dom_m(get_clauses_wl S) ∧ C∈set xs∧ length (get_clauses_wl S ∝ C) > 2);
cands ← SPEC (λcands'. mset cands' = mset cands ∧ sorted_wrt (λa b. length (get_clauses_wl S ∝ a) ≤ length (get_clauses_wl S ∝ b)) cands');
RETURN (occs, cands)
}›
lemma forward_subsumption_all_wl_pre_length_ge2:
‹forward_subsumption_all_wl_pre S ⟹ C ∈#dom_m (get_clauses_wl S) ⟹ length (get_clauses_wl S ∝ C) ≥ 2›
unfolding forward_subsumption_all_wl_pre_def forward_subsumption_all_pre_def
twl_struct_invs_def twl_st_inv_alt_def
by normalize_goal+
simp
lemma populate_occs_populate_occs_spec:
assumes ‹literals_are_ℒ⇩i⇩n' S› ‹forward_subsumption_all_wl_pre S›
shows ‹populate_occs S ≤ ⇓Id (SPEC(populate_occs_spec S))›
proof -
have [refine]: ‹distinct xs ⟹wf (measure (λ(i, occs, cands). length xs - i))› for xs
by auto
have correct_occurence_list: ‹⋀x xa s a b aa ba.
distinct x ⟹
populate_occs_inv S x s ⟹
s = (a, b) ⟹
b = (aa, ba) ⟹
correct_occurence_list S aa (mset (drop a x)) 2›
by (auto simp: populate_occs_inv_def)
have G0: ‹A ⊆# B ⟹ a ∉# A ⟹ a ∈# B ⟹ add_mset a A ⊆# B› for A B :: ‹nat multiset› and a
by (metis add_mset_remove_trivial_eq insert_subset_eq_iff subset_add_mset_notin_subset_mset)
have G: ‹distinct x ⟹
a < length x ⟹
all_occurrences (all_init_atms_st S) aa + mset ba ⊆# mset (take a x) ⟹
x ! a ∈# dom_m (get_clauses_wl S) ⟹
all_occurrences (all_init_atms_st S) xc = add_mset (x ! a) (all_occurrences (all_init_atms_st S) aa) ⟹
all_occurrences (all_init_atms_st S) aa + mset ba ⊆# dom_m (get_clauses_wl S) ⟹
distinct ba ⟹
correct_occurence_list S aa (add_mset (x ! a) (mset (drop (Suc a) x))) 2 ⟹
add_mset (x ! a) (all_occurrences (all_init_atms_st S) aa + mset ba) ⊆# dom_m (get_clauses_wl S)›
for x xa s a b aa ba xb xc
apply (rule G0)
apply auto
apply (meson correct_occurence_list_def disjunct_not_in union_single_eq_member)
by (meson distinct_in_set_take_iff in_multiset_in_set less_Suc_eq mset_le_decr_left2 mset_subset_eqD not_less_eq)
have G': ‹distinct x ⟹
a < length x ⟹
all_occurrences (all_init_atms_st S) aa + mset ba ⊆# mset (take a x) ⟹
x ! a ∈# dom_m (get_clauses_wl S) ⟹
all_occurrences (all_init_atms_st S) aa + mset ba ⊆# dom_m (get_clauses_wl S) ⟹
distinct ba ⟹
correct_occurence_list S aa (add_mset (x ! a) (mset (drop (Suc a) x))) 2 ⟹
add_mset (x ! a) (all_occurrences (all_init_atms_st S) aa + mset ba) ⊆# dom_m (get_clauses_wl S)›
‹distinct x ⟹
a < length x ⟹
all_occurrences (all_init_atms_st S) aa + mset ba ⊆# mset (take a x) ⟹
x ! a ∈# dom_m (get_clauses_wl S) ⟹
all_occurrences (all_init_atms_st S) aa + mset ba ⊆# dom_m (get_clauses_wl S) ⟹
distinct ba ⟹
correct_occurence_list S aa (add_mset (x ! a) (mset (drop (Suc a) x))) 2 ⟹ x ! a ∈ set ba ⟹ False›
for x xa s a b aa ba xb xc
apply (rule G0)
apply (auto simp add: correct_occurence_list_def)
by (smt (verit, ccfv_threshold) distinct_in_set_take_iff in_multiset_in_set nat_in_between_eq(2) not_less_eq set_mset_mono subsetD union_iff)+
show ?thesis
unfolding populate_occs_def Let_def
apply (refine_vcg mop_occ_list_create[THEN order_trans] push_to_occs_list2 all_lit_clause_unset_spec)
subgoal using assms(2) by fast
apply assumption
subgoal unfolding populate_occs_inv_def by (auto simp: occurrence_list_def all_occurrences_def correct_occurence_list_def)
subgoal
unfolding populate_occs_inv_def by (auto simp: occurrence_list_def take_Suc_conv_app_nth Cons_nth_drop_Suc[symmetric]
dest: subset_mset_imp_subset_add_mset intro: correct_occurence_list_mono_candsI2 intro: G')
subgoal unfolding populate_occs_inv_def by (auto simp: occurrence_list_def take_Suc_conv_app_nth Cons_nth_drop_Suc[symmetric]
dest: subset_mset_imp_subset_add_mset intro: correct_occurence_list_mono_candsI2)
subgoal by auto
subgoal by auto
apply (rule correct_occurence_list; assumption)
subgoal by auto
subgoal using assms by auto
subgoal by auto
subgoal unfolding populate_occs_inv_def
apply auto
by (metis add.commute distinct_in_set_take_iff mset_subset_eqD mset_subset_eq_add_right nat_neq_iff set_mset_mset)
subgoal for x xa s a b aa ba xb xc
unfolding populate_occs_inv_def apply simp
by (auto simp: take_Suc_conv_app_nth Cons_nth_drop_Suc[symmetric] intro: G)
subgoal by auto
subgoal for x xa s a b aa ba xb xc
unfolding populate_occs_inv_def by (auto simp: take_Suc_conv_app_nth Cons_nth_drop_Suc[symmetric]
intro: correct_occurence_list_mono_candsI2 dest: forward_subsumption_all_wl_pre_length_ge2 intro!: G')
subgoal by auto
subgoal unfolding populate_occs_inv_def by (auto simp: take_Suc_conv_app_nth Cons_nth_drop_Suc[symmetric]
intro: correct_occurence_list_mono_candsI2 dest: subset_mset_imp_subset_add_mset)
subgoal by auto
subgoal by (auto simp: populate_occs_inv_def populate_occs_spec_def correct_occurence_list_def
dest: mset_eq_setD simp flip: distinct_mset_mset_distinct)
subgoal by (auto simp: populate_occs_inv_def populate_occs_spec_def correct_occurence_list_def
dest: mset_eq_setD simp flip: distinct_mset_mset_distinct)
done
qed
definition forward_subsumption_all_wl2 :: ‹nat twl_st_wl ⇒ _ nres› where
‹forward_subsumption_all_wl2 = (λS. do {
ASSERT (forward_subsumption_all_wl_pre S);
(occs, xs) ← SPEC (populate_occs_spec S);
let m = length xs;
D ← mop_ch_create (set_mset (all_init_atms_st S));
let shrunken = {#};
(_, occs, D, S, _, shrunken) ←
WHILE⇩T⇗ forward_subsumption_all_wl2_inv S xs ⇖ (λ(i, occs, D, S, n, shrunken). i < m ∧ get_conflict_wl S = None)
(λ(i, occs, D, S, n, shrunken). do {
let C = xs!i;
ASSERT(C∈#dom_m (get_clauses_wl S));
D ← mop_ch_add_all (mset (get_clauses_wl S ∝ C)) D;
(occs, D, shrunken, T) ← try_to_forward_subsume_wl2 C occs (mset (drop (i) xs)) D shrunken S;
RETURN (i+1, occs, D, T, (length (get_clauses_wl S ∝ C)), shrunken)
})
(0, occs, D, S, 2, shrunken);
ASSERT (fst occs = set_mset (all_init_atms_st S));
ASSERT (shrunken ⊆# mset xs);
ASSERT (literals_are_ℒ⇩i⇩n' S);
RETURN S
}
)›
lemma forward_subsumption_all_wl2_forward_subsumption_all_wl:
‹forward_subsumption_all_wl2 S ≤ ⇓Id (forward_subsumption_all_wl S)›
proof -
have forward_subsumption_all_wl_alt_def:
‹forward_subsumption_all_wl = (λS. do {
ASSERT (forward_subsumption_all_wl_pre S);
xs ← SPEC (forward_subsumption_wl_all_cands S);
let _ = size xs;
D ← RETURN ({#} :: nat clause);
let _ = ({#} :: nat multiset);
ASSERT (D = {#});
(xs, S) ←
WHILE⇩T⇗ forward_subsumption_all_wl_inv S xs ⇖ (λ(xs, S). xs ≠ {#} ∧ get_conflict_wl S = None)
(λ(xs, S). do {
C ← SPEC (λC. C ∈# xs);
let _ = mset (get_clauses_wl S ∝ C) + {#};
T ← try_to_forward_subsume_wl C xs S;
ASSERT (∀D∈#remove1_mset C xs. get_clauses_wl T ∝ D = get_clauses_wl S ∝ D);
RETURN (remove1_mset C xs, T)
})
(xs, S);
RETURN S
}
)›
unfolding forward_subsumption_all_wl_def Let_def by (auto intro!: ext)
have [refine]: ‹SPEC
(λxs. mset xs ⊆# dom_m (get_clauses_wl S) ∧
sorted_wrt (λa b. length (get_clauses_wl S ∝ a) ≤ length (get_clauses_wl S ∝ b)) xs)
≤ ⇓ {(xs,ys). mset xs = ys ∧ mset xs ⊆# dom_m (get_clauses_wl S) ∧
sorted_wrt (λa b. length (get_clauses_wl S ∝ a) ≤ length (get_clauses_wl S ∝ b)) xs}
(SPEC (λxs. xs ⊆# dom_m (get_clauses_wl S)))›
by (auto intro!: RES_refine)
have [refine]: ‹SPEC (populate_occs_spec S) ≤ ⇓ {((occs,xs), ys). ys = mset xs ∧ populate_occs_spec S (occs, xs)}(SPEC (forward_subsumption_wl_all_cands S))›
(is ‹_ ≤ ⇓ ?populate _›)
unfolding populate_occs_spec_def prod.simps forward_subsumption_wl_all_cands_def
by (rule RES_refine)
(auto dest: mset_le_decr_left2 mset_le_decr_left1)
define loop_inv where ‹loop_inv xs = {((i, occs', D :: clause_hash, U, n, shrunken :: nat multiset), (xsa, V)). (U,V)∈Id ∧ i ≤ length xs ∧
(D, {#}) ∈ clause_hash_ref (all_init_atms_st V) ∧ shrunken ⊆# mset (take i xs) ∧
(i < length xs ⟶ length (get_clauses_wl U ∝ (xs!i)) ≥ n)∧
correct_occurence_list U occs' xsa n ∧ xsa = mset (drop i xs)}› for xs
have loop_init: ‹(occsxs, xsa) ∈ ?populate ⟹
occsxs = (occs, xs) ⟹
(D, D') ∈ clause_hash_ref (all_init_atms_st S) ⟹
D' = {#} ⟹
forward_subsumption_all_wl_inv S (xsa) (xsa, S) ⟹ ((0, occs, D, S, 2, {#}), xsa, S) ∈ loop_inv xs›
(is ‹_ ⟹ _ ⟹ _ ⟹_ ⟹ _ ⟹ _ ∈ ?loopinv›) for D occs xsa aa xs occsxs uu D'
by (cases xs) (auto simp: populate_occs_spec_def loop_inv_def)
have [refine]: ‹(a,b) ∈ Id ⟹ (c, d) ∈ Id ⟹ simplify_clause_with_unit_st_wl a c ≤⇓Id (simplify_clause_with_unit_st_wl b d)› for a b c d
by auto
have try_to_forward_subsume_wl2_pre0: ‹⋀x xs x1 x2 D Da xa x' x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e C Db shrunken x2d'.
forward_subsumption_all_wl_pre S ⟹
(x, xs) ∈ ?populate ⟹
x = (x1, x2) ⟹
(D, Da) ∈ clause_hash_ref (all_init_atms_st S) ⟹
Da = {#} ⟹
(xa, x') ∈ loop_inv x2 ⟹
(case xa of (i, occs, D, S, n, shrunken) ⇒ i < length x2 ∧ get_conflict_wl S = None) ⟹
(case x' of (xs, S) ⇒ xs ≠ {#} ∧ get_conflict_wl S = None) ⟹
forward_subsumption_all_wl2_inv S x2 xa ⟹
forward_subsumption_all_wl_inv S xs x' ⟹
x' = (x1a, x2a) ⟹
x2d' = (x2e, shrunken) ⟹
x2d = (x1e, x2d') ⟹
x2c = (x1d, x2d) ⟹
x2b = (x1c, x2c) ⟹
xa = (x1b, x2b) ⟹
(x2 ! x1b, C) ∈ nat_rel ⟹
(Db, mset (get_clauses_wl x2a ∝ C) + {#}) ∈ clause_hash_ref (all_init_atms_st x1e) ⟹
try_to_forward_subsume_wl2_pre0 (mset (get_clauses_wl x2a ∝ C) + {#}) (x2 ! x1b) x1c (mset (drop x1b x2)) Db x1e x2e›
unfolding forward_subsumption_all_inv_def forward_subsumption_all_wl_inv_def
forward_subsumption_all_wl2_inv_def loop_inv_def
apply (hypsubst, unfold prod.simps, normalize_goal+)
subgoal for x xs x1 x2 D Da xa x' x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e C Db xb xc
apply (auto simp add: try_to_forward_subsume_wl2_pre0_def populate_occs_spec_def drop_Suc_nth)
apply (metis add_mset_disjoint(2) correct_occurence_list_def insert_DiffM union_single_eq_member)
by (metis add_mset_add_mset_same_iff correct_occurence_list_def distinct_mem_diff_mset
insert_DiffM set_mset_mset union_single_eq_member)
done
have subsumed_postinv: ‹
forward_subsumption_all_wl_pre S ⟹
(x, xs) ∈ ?populate ⟹
x ∈ Collect (populate_occs_spec S) ⟹
xs ∈ Collect (forward_subsumption_wl_all_cands S) ⟹
x = (x1, x2) ⟹
(xa, x') ∈ loop_inv x2 ⟹
case xa of (i, occs, D, S, n, shrunken) ⇒ i < length x2 ∧ get_conflict_wl S = None ⟹
case x' of (xs, S) ⇒ xs ≠ {#} ∧ get_conflict_wl S = None ⟹
forward_subsumption_all_wl2_inv S x2 xa ⟹
forward_subsumption_all_wl_inv S xs x' ⟹
x' = (x1a, x2a) ⟹
x2d' = (x2e, shrunken) ⟹
x2d = (x1e, x2d') ⟹
x2c = (x1d, x2d) ⟹
x2b = (x1c, x2c) ⟹
xa = (x1b, x2b) ⟹
(x2 ! x1b, C) ∈ nat_rel ⟹
x2 ! x1b ∈# dom_m (get_clauses_wl x1e) ⟹
inres (mop_ch_add_all (mset (get_clauses_wl x1e ∝ (x2 ! x1b))) x1d) Db ⟹
(Db, mset (get_clauses_wl x2a ∝ C) + {#}) ∈ clause_hash_ref (all_init_atms_st x1e) ⟹
(xb, Sa) ∈ try_to_forward_subsume_wl_rel x1e (x2 ! x1b) (mset (drop x1b x2)) x1c x2e shrunken ⟹
∀D∈#remove1_mset C x1a. get_clauses_wl Sa ∝ D = get_clauses_wl x2a ∝ D ⟹
xb = (a, b) ⟹
b = (aa, ba) ⟹
ba = (ab, bb) ⟹
((x1b + 1, a, aa, bb, length (get_clauses_wl x1e ∝ (x2 ! x1b)), ab), remove1_mset C x1a, Sa)
∈ loop_inv x2›
for x xs x1 x2 D Da xa x' x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e C Db xb Sa a b aa ba shrunken x2d' ab bb
unfolding forward_subsumption_all_inv_def forward_subsumption_all_wl_inv_def
forward_subsumption_all_wl2_inv_def loop_inv_def populate_occs_spec_def mem_Collect_eq
try_to_forward_subsume_wl_rel_def
apply (hypsubst, unfold prod.simps, normalize_goal+)
apply (auto simp add: try_to_forward_subsume_wl2_pre0_def populate_occs_spec_def drop_Suc_nth take_Suc_conv_app_nth
dest: sorted_wrt_nth_less[of _ _ x1b ‹Suc x1b›] intro: subset_mset_imp_subset_add_mset)
by (meson mset_subset_eq_add_mset_cancel subset_mset.dual_order.trans)
have in_all_lits_in_cls: ‹xaa ∈ set (get_clauses_wl S ∝ C) ⟹ C ∈# dom_m (get_clauses_wl S) ⟹
xaa ∈# all_lits_st S› for C S xaa
by (auto simp: all_lits_st_def all_lits_def ran_m_def all_lits_of_mm_add_mset in_clause_in_all_lits_of_m
dest!: multi_member_split)
have in_atms: ‹forward_subsumption_all_wl_pre S ⟹
forward_subsumption_all_wl_pre S ⟹
(x, xs) ∈ {((occs, xs), ys). ys = mset xs ∧ populate_occs_spec S (occs, xs)} ⟹
x ∈ Collect (populate_occs_spec S) ⟹
xs ∈ Collect (forward_subsumption_wl_all_cands S) ⟹
x = (x1, x2) ⟹
(D, Da) ∈ clause_hash_ref (all_init_atms_st S) ⟹
Da = {#} ⟹
(xa, x') ∈ loop_inv x2 ⟹
case xa of (i, occs, D, S, n, shrunken) ⇒ i < length x2 ∧ get_conflict_wl S = None ⟹
case x' of (xs, S) ⇒ xs ≠ {#} ∧ get_conflict_wl S = None ⟹
forward_subsumption_all_wl2_inv S x2 xa ⟹
forward_subsumption_all_wl_inv S xs x' ⟹
x' = (x1a, x2a) ⟹
x2d = (x1e, x2d') ⟹
x2c = (x1d, x2d) ⟹
x2b = (x1c, x2c) ⟹
xa = (x1b, x2b) ⟹
(x2 ! x1b, C) ∈ nat_rel ⟹
atms_of (mset (get_clauses_wl x1e ∝ (x2 ! x1b))) ⊆ set_mset (all_init_atms_st x1e)›
for x xs x1 x2 D Da xa x' x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e C x2d' shrunken
unfolding forward_subsumption_all_inv_def forward_subsumption_all_wl_inv_alt_def
forward_subsumption_all_wl2_inv_def loop_inv_def populate_occs_spec_def mem_Collect_eq
all_init_atms_st_alt_def atms_of_def
apply (cases x2d', hypsubst, unfold prod.simps, normalize_goal+)
apply (frule literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def[of x1e])
subgoal
by (auto simp: all_init_atms_st_alt_def all_atms_st_alt_def drop_Suc_nth
simp del: all_atms_st_alt_def[symmetric] intro!: imageI
in_all_lits_in_cls[of _ _ ‹x2 ! x1b›])
done
have distinct: ‹forward_subsumption_all_wl_pre S ⟹
forward_subsumption_all_wl_inv S xs x' ⟹
x' = (x1a, x2a) ⟹
(C', C) ∈ nat_rel ⟹
C' ∈# dom_m (get_clauses_wl x2a) ⟹
distinct_mset (mset (get_clauses_wl x2a ∝ C))›
for x' x1a x2a xa x1b x2b x1c x2c x1d x2d x1e x2e x2 C xs C'
unfolding forward_subsumption_all_wl_inv_alt_def case_prod_beta
forward_subsumption_all_inv_def
apply normalize_goal+
apply (elim rtranclp_cdcl_twl_inprocessing_l_twl_st_l)
apply assumption+
unfolding twl_struct_invs_def twl_st_inv_alt_def
by (simp add: mset_take_mset_drop_mset')
show ?thesis
unfolding forward_subsumption_all_wl_alt_def forward_subsumption_all_wl2_def
apply (rewrite at ‹let _ = length _ in _› Let_def)
apply (refine_vcg mop_occ_list_create mop_ch_create mop_ch_add_all
try_to_forward_subsume_wl2_try_to_forward_subsume_wl
WHILEIT_refine_with_inv)
apply (rule loop_init; assumption)
subgoal unfolding forward_subsumption_all_wl2_inv_def loop_inv_def by auto
subgoal by (auto simp: loop_inv_def)
subgoal by (auto simp: in_set_dropI loop_inv_def)
subgoal
unfolding loop_inv_def populate_occs_spec_def mem_Collect_eq
forward_subsumption_all_inv_def forward_subsumption_all_wl_inv_alt_def
forward_subsumption_all_wl2_inv_def case_prod_beta apply normalize_goal+
by (auto simp add: forward_subsumption_wl_all_cands_def
simp flip: Cons_nth_drop_Suc dest: mset_subset_eq_insertD)
apply (solves ‹auto simp: loop_inv_def›)
subgoal by (rule in_atms)
subgoal by (auto simp: loop_inv_def)
subgoal by auto
subgoal apply (rule distinct)
by assumption+ (simp add: loop_inv_def case_prod_beta)
apply (subst clause_hash_ref_cong)
defer apply assumption
apply (rule try_to_forward_subsume_wl2_pre0; assumption?)
subgoal by (auto simp: loop_inv_def)
subgoal by (auto simp: loop_inv_def)
subgoal for x xs x1 x2 D Da xa x' x1a x2a x1b x2b x1c x2c x1d x2d x1e x2d' x2e shrunken C Db
xb Sa a b aa ba
by (rule subsumed_postinv)
subgoal by (auto simp: loop_inv_def correct_occurence_list_def)
subgoal by (auto simp: loop_inv_def intro: subset_mset.dual_order.trans[OF mset_take_subseteq])
subgoal by (auto simp: forward_subsumption_all_wl2_inv_def
dest!: forward_subsumption_all_wl_inv_literals_are_ℒ⇩i⇩n'D)
subgoal by (auto simp: loop_inv_def)
subgoal by (auto simp: loop_inv_def)
done
qed
subsection ‹Refinement to isasat.›
definition is_candidate_forward_subsumption where
‹is_candidate_forward_subsumption C N = do {
ASSERT (C ∈# dom_m N);
SPEC (λb :: bool. b ⟶ ¬irred N C ∧ length (N ∝ C) ≠ 2)
}›
lemma incr_forward_rounds_st:
‹(S, S') ∈ twl_st_heur_restart_occs' r u ⟹
(incr_forward_rounds_st S, S') ∈ twl_st_heur_restart_occs' r u›
by (simp add: IsaSAT_Restart.all_init_atms_alt_def twl_st_heur_restart_occs_def incr_forward_rounds_st_def)
lemma red_in_dom_number_of_learned_ge1_twl_st_heur_restart_occs:
assumes ‹(S,T) ∈ twl_st_heur_restart_occs' r u› and
‹C ∈# dom_m (get_clauses_wl T)›
‹arena_status (get_clauses_wl_heur S) C ≠ IRRED›
shows ‹1 ≤ get_learned_count_number S›
proof -
have ‹clss_size_corr_restart (get_clauses_wl T) (IsaSAT_Setup.get_unkept_unit_init_clss_wl T) {#}
(IsaSAT_Setup.get_kept_unit_init_clss_wl T) (IsaSAT_Setup.get_kept_unit_learned_clss_wl T)
(get_subsumed_init_clauses_wl T) {#} (get_init_clauses0_wl T) {#} (get_learned_count S)› and
‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl T) (set (get_vdom S))›
using assms(1) unfolding twl_st_heur_restart_occs_def Let_def by auto
then show ?thesis
using assms(2-) red_in_dom_number_of_learned_ge1[of C ‹get_clauses_wl T›]
by (auto simp: clss_size_corr_restart_def clss_size_def clss_size_lcount_def
arena_lifting)
qed
lemma red_in_dom_number_of_learned_ge1_twl_st_heur_restart_occs2:
assumes ‹(S,T) ∈ twl_st_heur_restart_occs' r u› and
‹C ∈# dom_m (get_clauses_wl T)›
‹¬irred (get_clauses_wl T) C›
shows ‹1 ≤ get_learned_count_number S›
proof -
have ‹clss_size_corr_restart (get_clauses_wl T) (IsaSAT_Setup.get_unkept_unit_init_clss_wl T) {#}
(IsaSAT_Setup.get_kept_unit_init_clss_wl T) (IsaSAT_Setup.get_kept_unit_learned_clss_wl T)
(get_subsumed_init_clauses_wl T) {#} (get_init_clauses0_wl T) {#} (get_learned_count S)›
using assms(1) unfolding twl_st_heur_restart_occs_def Let_def by auto
then show ?thesis
using assms(2-) red_in_dom_number_of_learned_ge1[of C ‹get_clauses_wl T›]
by (auto simp: clss_size_corr_restart_def clss_size_def clss_size_lcount_def
arena_lifting)
qed
lemma mop_cch_remove_one_mop_ch_remove_one:
assumes
‹(L,L')∈Id› and
DD': ‹(D,D')∈clause_hash›
shows ‹mop_cch_remove_one L D
≤ ⇓ clause_hash
(mop_ch_remove L' D')›
using assms
unfolding mop_cch_remove_one_def mop_ch_remove_def
apply (refine_vcg,
auto simp: ch_remove_pre_def clause_hash_def ch_remove_def distinct_mset_remove1_All
dest: bspec[of _ _ L])
apply (cases L; auto)
done
lemma mop_arena_status2:
assumes ‹(C,C')∈nat_rel› ‹C ∈ vdom›
‹valid_arena arena N vdom›
shows
‹mop_arena_status arena C
≤ SPEC
(λc. (c, C' ∈# dom_m N)
∈ {(a,b). (b ⟶ (a = IRRED ⟷ irred N C) ∧ (a = LEARNED ⟷ ¬irred N C)) ∧ (a = DELETED ⟷ ¬b)})›
using assms arena_dom_status_iff[of arena N vdom C] unfolding mop_arena_status_def
by (cases ‹C ∈# dom_m N›)
(auto intro!: ASSERT_leI simp: arena_is_valid_clause_vdom_def
arena_lifting)
lemma isa_subsume_clauses_match2_subsume_clauses_match2:
assumes
SS': ‹(S, S') ∈ twl_st_heur_restart_occs' r u› and
CC': ‹(C,C')∈nat_rel› and
EE': ‹(E,E')∈nat_rel› and
DD': ‹(D,D')∈clause_hash›
shows
‹isa_subsume_clauses_match2 C E S D
≤ ⇓ Id
(subsume_clauses_match2 C' E' S' D')›
proof -
have [refine]: ‹((0, SUBSUMED_BY C), 0, SUBSUMED_BY C') ∈ nat_rel ×⇩r Id›
using assms by auto
show ?thesis
unfolding isa_subsume_clauses_match2_def subsume_clauses_match2_def mop_arena_length_st_def
Let_def[of ‹mark_literal_for_unit_deletion _›]
apply (refine_vcg mop_arena_length[where vdom=‹set (get_vdom S)›, THEN fref_to_Down_curry, unfolded comp_def]
mop_arena_lit2[where vdom=‹set (get_vdom S)›] mop_cch_in_mop_ch_in)
subgoal using assms unfolding isa_subsume_clauses_match2_pre_def by fast
subgoal unfolding subsume_clauses_match2_pre_def subsume_clauses_match_pre_def
by auto
subgoal using SS' CC' EE' by (auto simp: twl_st_heur_restart_occs_def)
subgoal using SS' CC' arena_lifting(10)[of ‹get_clauses_wl_heur S› ‹get_clauses_wl S'› ‹set (get_vdom S)› C] apply -
unfolding isa_subsume_clauses_match2_pre_def subsume_clauses_match2_pre_def subsume_clauses_match_pre_def
by normalize_goal+ (simp add: twl_st_heur_restart_occs_def)
subgoal using EE' by auto
subgoal by auto
subgoal by auto
subgoal using SS' CC' by (auto simp: twl_st_heur_restart_occs_def)
subgoal using CC' by auto
subgoal by auto
subgoal using DD' by auto
subgoal by auto
subgoal by auto
subgoal using DD' by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using CC' by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma valid_occs_in_vdomI:
‹valid_occs occs (get_aivdom S) ⟹ x1 < length (occs ! nat_of_lit L) ⟹
nat_of_lit L < length occs ⟹ cocc_list_at occs L x1 ∈ set (get_vdom S)›
apply (drule nth_mem)
unfolding valid_occs_def cocc_list_at_def Union_eq subset_iff
by (auto dest: spec[of _ ‹occs ! nat_of_lit L ! x1›] simp: cocc_content_set_def)
definition mop_ch_remove_all_clauses where
‹mop_ch_remove_all_clauses C D = do {
(_, D) ← WHILE⇩T (λ(C, D). C ≠ {#})
(λ(C, D). do {L ← SPEC (λL. L ∈# C); D ← mop_ch_remove L D; RETURN (remove1_mset L C, D)})
(C, D);
RETURN D
} ›
lemma diff_mono_mset: "a ⊆# b ⟹ a - c ⊆# b - c"
by (meson subset_eq_diff_conv subset_mset.dual_order.eq_iff subset_mset.dual_order.trans)
lemma mop_ch_remove_all_clauses_mop_ch_remove_all:
‹mop_ch_remove_all_clauses C D ≤ ⇓Id (mop_ch_remove_all C D)›
unfolding mop_ch_remove_all_clauses_def mop_ch_remove_all_def mop_ch_remove_def nres_monad3
apply (refine_vcg WHILET_rule[where R = ‹measure (λ(i, _). size i)› and
I = ‹ λ(C', D'). C' ⊆# C ∧ C' ⊆# snd D' ∧ snd D = snd D' + C - C' ∧ fst D = fst D'›])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for s x b unfolding ch_remove_pre_def by force
subgoal by auto
subgoal unfolding ch_remove_def by (auto simp: case_prod_beta diff_mono_mset)
subgoal
by (drule multi_member_split)
(clarsimp simp: ch_remove_def case_prod_beta ch_remove_pre_def)
subgoal by (auto simp: ch_remove_def case_prod_beta)
subgoal by (clarsimp dest!: multi_member_split simp: size_Diff_singleton_if)
subgoal for s a b by (cases b) (auto simp: ch_remove_all_def case_prod_beta)
done
lemma mop_cch_remove_all_clauses_mop_ch_remove_all_clauses:
assumes
SS': ‹(S, S') ∈ twl_st_heur_restart_occs' r u›and
‹(C,C')∈nat_rel› and
DD': ‹(D,D')∈clause_hash› and
C: ‹C ∈# dom_m (get_clauses_wl S')›
shows ‹mop_cch_remove_all_clauses S C D
≤ ⇓ clause_hash
(mop_ch_remove_all (mset (get_clauses_wl S' ∝ C')) D')›
proof -
define f where "f C = SPEC (λL. L ∈# C)" for C :: ‹nat clause›
have eq[simp]: ‹C' = C›
using assms by auto
have valid: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl S') (set (get_vdom S))›
using SS' C unfolding arena_is_valid_clause_idx_and_access_def arena_is_valid_clause_idx_def twl_st_heur_restart_occs_def
by (auto simp: arena_lifting)
have f: ‹(x, x')
∈ {((n, D), m, D'). (D, D') ∈ clause_hash ∧ m = mset (drop n (get_clauses_wl S' ∝ C))} ⟹
case x of (i, D) ⇒ i < arena_length (get_clauses_wl_heur S) C ⟹
case x' of (C, D) ⇒ C ≠ {#} ⟹
x' = (x1, x2) ⟹
x = (x1a, x2a) ⟹SPEC (λc. (c, get_clauses_wl S' ∝ C ! x1a) ∈ nat_lit_lit_rel)
≤ ⇓ {(a,b). a = b ∧ a = get_clauses_wl S' ∝ C ! x1a} (f x1)› for x1 x1a x2 x2a x x'
unfolding f_def by (auto intro!: RES_refine in_set_dropI)
show ?thesis
apply (rule ref_two_step[OF _ mop_ch_remove_all_clauses_mop_ch_remove_all[unfolded Down_id_eq]])
unfolding mop_cch_remove_all_clauses_def mop_ch_remove_all_clauses_def mop_arena_length_def
nres_monad3 bind_to_let_conv f_def[symmetric]
apply (subst Let_def[of ‹arena_length _ _›])
apply (refine_vcg WHILET_refine[where R = ‹{((n, D), (m, D')). (D,D')∈ clause_hash ∧
m = mset (drop n (get_clauses_wl S' ∝ C))}›] mop_cch_remove_one_mop_ch_remove_one)
subgoal using valid C unfolding arena_is_valid_clause_idx_def twl_st_heur_restart_occs_def apply -
by (rule exI[of _ ‹get_clauses_wl S'›], auto intro!: exI[of _ ‹get_vdom S›])
subgoal using DD' by auto
subgoal using valid by (auto simp: arena_lifting C)
subgoal using valid arena_lifting(4,7)[OF valid C] by (force simp: C)
apply (rule mop_arena_lit[THEN order_trans])
apply (rule valid)
apply (rule C)
subgoal by auto
apply (rule refl)
subgoal using valid by (auto simp: arena_lifting C)
apply (rule f; assumption)
subgoal by (auto intro!: in_set_dropI)
subgoal using DD' by auto
subgoal by (auto simp flip: Cons_nth_drop_Suc add_mset_remove_trivial_If)
subgoal by auto
done
qed
lemma find_best_subsumption_candidate:
assumes
SS': ‹(S, S') ∈ twl_st_heur_restart_occs' r u› and
pre0: ‹push_to_occs_list2_pre C S' occs› and
occs: ‹(get_occs S, occs) ∈ occurrence_list_ref› and
le_bound: ‹length (get_clauses_wl S' ∝ C) ≤ Suc (unat32_max div 2)›
shows ‹find_best_subsumption_candidate C S ≤ SPEC (λL. L ∈# mset (get_clauses_wl S' ∝ C))›
proof -
have valid: ‹valid_occs (get_occs S) (get_aivdom S)› and
arena: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl S') (set (get_vdom S))›
using SS' by (auto simp: twl_st_heur_restart_occs_def)
have
C: ‹C ∈# dom_m (get_clauses_wl S')› and
le: ‹2 ≤ length (get_clauses_wl S' ∝ C)› and
fst: ‹fst occs = set_mset (all_init_atms_st S')› and
lits: ‹atm_of ` set (get_clauses_wl S' ∝ C) ⊆ set_mset (all_init_atms_st S')›
using pre0 unfolding push_to_occs_list2_pre_def by blast+
have pre2: ‹arena_lit_pre (get_clauses_wl_heur S) (C+i)›
if ‹i < length (get_clauses_wl S' ∝ C)› for i
using that unfolding arena_lit_pre_def apply -
by (rule exI[of _ C])
(use SS' arena C le in ‹auto simp: arena_is_valid_clause_idx_and_access_def intro!: exI[of _ ‹get_clauses_wl S'›] exI[of _ ‹set (get_vdom S)›]›)
have pre: ‹arena_lit_pre (get_clauses_wl_heur S) C›
unfolding arena_lit_pre_def
by (rule exI[of _ C])
(use SS' arena C le in ‹auto simp: arena_is_valid_clause_idx_and_access_def intro!: exI[of _ ‹get_clauses_wl S'›] exI[of _ ‹set (get_vdom S)›]›)
have lit[simp]: ‹arena_lit (get_clauses_wl_heur S) (C + i) = get_clauses_wl S' ∝ C ! i›
if ‹i < length (get_clauses_wl S' ∝ C)› for i
using that C arena by (auto simp: arena_lifting)
from this[of 0] have [simp]: ‹arena_lit (get_clauses_wl_heur S) C = get_clauses_wl S' ∝ C ! 0›
using le by fastforce
have [simp]: ‹arena_length (get_clauses_wl_heur S) C = length (get_clauses_wl S' ∝ C)›
using arena C by (auto simp: arena_lifting)
have H[intro]: ‹ba ∈ set (get_clauses_wl S' ∝ C) ⟹ nat_of_lit ba < length (get_occs S)› for ba
using lits occs by (cases ba) (auto simp: map_fun_rel_def occurrence_list_ref_def
dest!: bspec[of _ _ ‹ba›] simp flip: fst)
have [intro]: ‹nat_of_lit (get_clauses_wl S' ∝ C ! i) < length (get_occs S)›
if ‹i < length (get_clauses_wl S' ∝ C)› for i
by (rule H) (metis (no_types, opaque_lifting) access_lit_in_clauses_def nth_mem that)
show ?thesis
using le
unfolding find_best_subsumption_candidate_def mop_arena_lit_def nres_monad3 mop_arena_length_st_def
mop_arena_length_def mop_arena_lit2_def mop_cocc_list_length_def
apply (refine_vcg arena WHILET_rule[where R = ‹measure (λ(i, _). length (get_clauses_wl S' ∝ C) - i)› and
I = ‹ λ(i, score, L). L ∈ set (get_clauses_wl S' ∝ C)›])
subgoal using pre by auto
subgoal by auto
subgoal unfolding cocc_list_length_pre_def by auto
subgoal using C arena unfolding arena_is_valid_clause_idx_def by fast
subgoal by auto
subgoal by (use le in ‹auto intro!: nth_mem›)
subgoal using le_bound by auto
subgoal by (auto intro!: pre2)
subgoal by auto
subgoal unfolding cocc_list_length_pre_def by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma find_best_subsumption_candidate_and_push:
assumes
SS': ‹(S, S') ∈ twl_st_heur_restart_occs' r u› and
pre0: ‹push_to_occs_list2_pre C S' occs› and
occs: ‹(get_occs S, occs) ∈ occurrence_list_ref› and
le_bound: ‹length (get_clauses_wl S' ∝ C) ≤ Suc (unat32_max div 2)›
shows ‹find_best_subsumption_candidate_and_push C S ≤ SPEC (λ(L, push). L ∈# mset (get_clauses_wl S' ∝ C))›
proof -
have valid: ‹valid_occs (get_occs S) (get_aivdom S)› and
arena: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl S') (set (get_vdom S))› and
heur: ‹heuristic_rel (all_init_atms_st S') (get_heur S)›
using SS' by (auto simp: twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def)
have
C: ‹C ∈# dom_m (get_clauses_wl S')› and
le: ‹2 ≤ length (get_clauses_wl S' ∝ C)› and
fst: ‹fst occs = set_mset (all_init_atms_st S')› and
lits: ‹atm_of ` set (get_clauses_wl S' ∝ C) ⊆ set_mset (all_init_atms_st S')›
using pre0 unfolding push_to_occs_list2_pre_def by blast+
have pre2: ‹arena_lit_pre (get_clauses_wl_heur S) (C+i)›
if ‹i < length (get_clauses_wl S' ∝ C)› for i
using that unfolding arena_lit_pre_def apply -
by (rule exI[of _ C])
(use SS' arena C le in ‹auto simp: arena_is_valid_clause_idx_and_access_def intro!: exI[of _ ‹get_clauses_wl S'›] exI[of _ ‹set (get_vdom S)›]›)
have pre: ‹arena_lit_pre (get_clauses_wl_heur S) C›
unfolding arena_lit_pre_def
by (rule exI[of _ C])
(use SS' arena C le in ‹auto simp: arena_is_valid_clause_idx_and_access_def intro!: exI[of _ ‹get_clauses_wl S'›] exI[of _ ‹set (get_vdom S)›]›)
have lit[simp]: ‹arena_lit (get_clauses_wl_heur S) (C + i) = get_clauses_wl S' ∝ C ! i›
if ‹i < length (get_clauses_wl S' ∝ C)› for i
using that C arena by (auto simp: arena_lifting)
from this[of 0] have [simp]: ‹arena_lit (get_clauses_wl_heur S) C = get_clauses_wl S' ∝ C ! 0›
using le by fastforce
have [simp]: ‹arena_length (get_clauses_wl_heur S) C = length (get_clauses_wl S' ∝ C)›
using arena C by (auto simp: arena_lifting)
have H[intro]: ‹ba ∈ set (get_clauses_wl S' ∝ C) ⟹ nat_of_lit ba < length (get_occs S)› for ba
using lits occs by (cases ba) (auto simp: map_fun_rel_def occurrence_list_ref_def
dest!: bspec[of _ _ ‹ba›] simp flip: fst)
have [intro]: ‹nat_of_lit (get_clauses_wl S' ∝ C ! i) < length (get_occs S)›
if ‹i < length (get_clauses_wl S' ∝ C)› for i
by (rule H) (metis (no_types, opaque_lifting) access_lit_in_clauses_def nth_mem that)
have [intro!]: ‹is_marked_added_heur_pre (get_heur S) (atm_of L)›
if ‹L ∈ set (get_clauses_wl S' ∝ C)› for L
proof -
have ‹atm_of L ∈ atm_of ` set (get_clauses_wl S' ∝ C)›
using that by auto
then have ‹atm_of L ∈# all_init_atms_st S'›
using lits by auto
then show ?thesis
using heur lits that
unfolding is_marked_added_heur_pre_def
by (auto simp: is_marked_added_heur_pre_stats_def heuristic_rel_def phase_saving_def
ℒ⇩a⇩l⇩l_add_mset atms_of_def
heuristic_rel_stats_def dest!: multi_member_split)
qed
show ?thesis
using le
unfolding find_best_subsumption_candidate_and_push_def mop_arena_lit_def nres_monad3 mop_arena_length_st_def
mop_arena_length_def mop_arena_lit2_def mop_cocc_list_length_def mop_is_marked_added_heur_def
apply (refine_vcg arena WHILET_rule[where R = ‹measure (λ(i, _). length (get_clauses_wl S' ∝ C) - i)› and
I = ‹ λ(i, score, L, _). L ∈ set (get_clauses_wl S' ∝ C)›])
subgoal using pre by auto
subgoal by auto
subgoal unfolding cocc_list_length_pre_def by auto
subgoal using C arena unfolding arena_is_valid_clause_idx_def by fast
subgoal by auto
subgoal by (use le in ‹auto intro!: nth_mem›)
subgoal using le_bound by auto
subgoal by (auto intro!: pre2)
subgoal by auto
subgoal unfolding cocc_list_length_pre_def by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma twl_st_heur_restart_occs_set_occsI:
‹(S,S')∈twl_st_heur_restart_occs ⟹ valid_occs occs (get_aivdom S) ⟹ (set_occs_wl_heur occs S, S') ∈ twl_st_heur_restart_occs›
by (auto simp: twl_st_heur_restart_occs_def)
lemma valid_occs_append:
‹C ∈ set (get_vdom_aivdom vdm) ⟹
C ∉# cocc_content coccs ⟹ valid_occs coccs vdm ⟹ nat_of_lit La < length coccs ⟹ valid_occs (cocc_list_append C coccs La) vdm›
by (auto simp: valid_occs_def in_set_upd_eq[of ‹nat_of lit La› coccs])
lemma in_cocc_content_iff: ‹C ∈# cocc_content occs ⟷ (∃xs. xs ∈ set occs ∧ C ∈ set xs)›
by (induction occs) auto
lemma notin_all_occurrences_notin_cocc: ‹(occs, occs') ∈ occurrence_list_ref ⟹ finite (fst occs') ⟹ C ∉# all_occurrences (mset_set (fst occs')) occs' ⟹ C ∉# cocc_content occs›
apply (auto simp: occurrence_list_ref_def all_occurrences_def image_Un map_fun_rel_def image_image
in_cocc_content_iff in_set_conv_nth)
apply (subgoal_tac ‹ia div 2 ∈ x›)
defer
subgoal for x y i ia
by (drule_tac x=‹ia› in spec) auto
subgoal for x y i ia
apply (drule_tac x= ‹if even ia then (ia, Pos (ia div 2)) else (ia, Neg (ia div 2))› in bspec)
apply auto
apply (rule_tac x=‹ia div 2› in image_eqI)
apply auto
by (auto split: if_splits dest: spec[of _ ia])
done
lemma set_mset_cocc_content_set[simp]: ‹set_mset (cocc_content occs) = cocc_content_set occs›
by (auto simp: cocc_content_set_def in_mset_sum_list_iff)
lemma isa_push_to_occs_list_st_push_to_occs_list2:
assumes
SS': ‹(S, S') ∈ twl_st_heur_restart_occs' r u› and
CC': ‹(C,C')∈nat_rel›and
occs: ‹(get_occs S, occs) ∈ occurrence_list_ref› and
C: ‹C ∈ set (get_vdom S)› and
length: ‹length (get_clauses_wl S' ∝ C) ≤ Suc (unat32_max div 2)›
shows ‹isa_push_to_occs_list_st C S
≤ ⇓ {(U, occs'). (get_occs U, occs') ∈ occurrence_list_ref ∧ (U, S') ∈ twl_st_heur_restart_occs' r u ∧ get_aivdom U = get_aivdom S} (push_to_occs_list2 C' S' occs)›
proof -
have eq: ‹C' = C›
using CC' by auto
have push_to_occs_list2_alt_def:
‹push_to_occs_list2 C S occs = do {
ASSERT (push_to_occs_list2_pre C S occs);
L ← SPEC (λL. L ∈# mset (get_clauses_wl S ∝ C));
ASSERT (occ_list_append_pre occs L);
occs ← mop_occ_list_append C occs L;
RETURN occs
}› for C S occs
unfolding push_to_occs_list2_def mop_occ_list_append_def
apply (subst (3)conj_absorb[symmetric])
unfolding summarize_ASSERT_conv[symmetric] by auto
have valid: ‹valid_occs (get_occs S) (get_aivdom S)›
using SS' unfolding twl_st_heur_restart_occs_def by auto
have length_bounded: ‹length (get_occs S ! nat_of_lit L) < length (get_clauses_wl_heur S)›
if
push: ‹push_to_occs_list2_pre C S' occs› and
‹(L, La) ∈ nat_lit_lit_rel› and
‹La ∈ {L. L ∈# mset (get_clauses_wl S' ∝ C)}› and
pre: ‹occ_list_append_pre occs La›
for L La
proof -
define n where ‹n = get_occs S ! nat_of_lit L›
have arena: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl S') (set (get_vdom S))› and
occs: ‹valid_occs (get_occs S) (get_aivdom S)› and
aivdom: ‹aivdom_inv_dec (get_aivdom S) (dom_m (get_clauses_wl S'))›
using SS' unfolding twl_st_heur_restart_occs_def
by fast+
have H: ‹add_mset C (cocc_content (get_occs S)) ⊆# mset (get_vdom S)›
using occs notin_all_occurrences_notin_cocc[OF assms(3), of C] unfolding valid_occs_def apply -
by (subst distinct_subseteq_iff[symmetric])
(use push C in ‹auto simp: push_to_occs_list2_pre_def›)
have ‹nat_of_lit L < length (get_occs S)›
using pre that(2) assms(3) unfolding occ_list_append_pre_def by (cases L) (auto simp: occurrence_list_ref_def map_fun_rel_def
dest!: bspec[of _ _ L])
from nth_mem[OF this] have ‹length (get_occs S ! nat_of_lit L) < length (get_vdom S)›
using multi_member_split[of ‹get_occs S ! nat_of_lit L› ‹mset (get_occs S)›] H[THEN size_mset_mono]
by (auto dest!: split_list simp: n_def[symmetric])
moreover have ‹length (get_vdom S) ≤ length (get_clauses_wl_heur S)›
using valid_arena_vdom_le(2)[OF arena] aivdom unfolding aivdom_inv_dec_alt_def
by (simp add: distinct_card)
finally show ?thesis .
qed
show ?thesis
unfolding isa_push_to_occs_list_st_def push_to_occs_list2_alt_def eq
apply (refine_vcg find_best_subsumption_candidate[OF SS' _ occs]
mop_cocc_list_append_mop_occ_list_append occs)
subgoal using length by auto
subgoal by (rule length_bounded)
subgoal by auto
subgoal using SS' C valid notin_all_occurrences_notin_cocc[OF occs, of C]
by (auto 9 2 intro!: twl_st_heur_restart_occs_set_occsI
intro!: valid_occs_append
simp: push_to_occs_list2_pre_def)
done
qed
lemma isa_maybe_push_to_occs_list_st_push_to_occs_list2:
assumes
SS': ‹(S, S') ∈ twl_st_heur_restart_occs' r u› and
CC': ‹(C,C')∈nat_rel›and
occs: ‹(get_occs S, occs) ∈ occurrence_list_ref› and
C: ‹C ∈ set (get_vdom S)› and
length: ‹length (get_clauses_wl S' ∝ C) ≤ Suc (unat32_max div 2)›
shows ‹isa_maybe_push_to_occs_list_st C S
≤ ⇓ {(U, occs'). (get_occs U, occs') ∈ occurrence_list_ref ∧ (U, S') ∈ twl_st_heur_restart_occs' r u ∧ get_aivdom U = get_aivdom S} (maybe_push_to_occs_list2 C' S' occs)›
proof -
have eq: ‹C' = C›
using CC' by auto
have maybe_push_to_occs_list2_alt_def:
‹maybe_push_to_occs_list2 C S occs = do {
ASSERT (push_to_occs_list2_pre C S occs);
b ← SPEC (λ_. True);
if b then do {
L ← SPEC (λL. L ∈# mset (get_clauses_wl S ∝ C));
ASSERT (occ_list_append_pre occs L);
occs ← mop_occ_list_append C occs L;
RETURN occs
} else RETURN occs
}› for C S occs
unfolding maybe_push_to_occs_list2_def mop_occ_list_append_def
apply (subst (3)conj_absorb[symmetric])
unfolding nres_monad3
unfolding summarize_ASSERT_conv[symmetric]
by (auto cong: if_cong intro: bind_cong[OF refl] simp: bind_ASSERT_eq_if)
have valid: ‹valid_occs (get_occs S) (get_aivdom S)›
using SS' unfolding twl_st_heur_restart_occs_def by auto
have length_bounded: ‹length (get_occs S ! nat_of_lit L) < length (get_clauses_wl_heur S)›
if
push: ‹push_to_occs_list2_pre C S' occs› and
‹(L, La) ∈ nat_lit_lit_rel› and
‹(x, b) ∈ {((L, push), push'). L ∈# mset (get_clauses_wl S' ∝ C) ∧ push = push'}›
‹x = (L, x2)› and
pre: ‹occ_list_append_pre occs La›
for L La x1 b x2 x
proof -
define n where ‹n = get_occs S ! nat_of_lit L›
have arena: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl S') (set (get_vdom S))› and
occs: ‹valid_occs (get_occs S) (get_aivdom S)› and
aivdom: ‹aivdom_inv_dec (get_aivdom S) (dom_m (get_clauses_wl S'))›
using SS' unfolding twl_st_heur_restart_occs_def
by fast+
have H: ‹add_mset C (cocc_content (get_occs S)) ⊆# mset (get_vdom S)›
using occs notin_all_occurrences_notin_cocc[OF assms(3), of C] unfolding valid_occs_def apply -
by (subst distinct_subseteq_iff[symmetric])
(use push C in ‹auto simp: push_to_occs_list2_pre_def›)
have ‹nat_of_lit L < length (get_occs S)›
using pre that(2) assms(3) unfolding occ_list_append_pre_def by (cases L) (auto simp: occurrence_list_ref_def map_fun_rel_def
dest!: bspec[of _ _ L])
from nth_mem[OF this] have ‹length (get_occs S ! nat_of_lit L) < length (get_vdom S)›
using multi_member_split[of ‹get_occs S ! nat_of_lit L› ‹mset (get_occs S)›] H[THEN size_mset_mono]
by (auto dest!: split_list simp: n_def[symmetric])
moreover have ‹length (get_vdom S) ≤ length (get_clauses_wl_heur S)›
using valid_arena_vdom_le(2)[OF arena] aivdom unfolding aivdom_inv_dec_alt_def
by (simp add: distinct_card)
finally show ?thesis .
qed
have find_best_subsumption_candidate_and_push:
‹find_best_subsumption_candidate_and_push C S ≤ ⇓ {((L, push), push'). L ∈# mset (get_clauses_wl S' ∝ C)∧ push = push'} (SPEC (λ_. True))›
if
SS': ‹(S, S') ∈ twl_st_heur_restart_occs' r u› and
pre0: ‹push_to_occs_list2_pre C S' occs› and
occs: ‹(get_occs S, occs) ∈ occurrence_list_ref› and
le_bound: ‹length (get_clauses_wl S' ∝ C) ≤ Suc (unat32_max div 2)›
by (rule find_best_subsumption_candidate_and_push[OF that, THEN order_trans]) (auto simp: conc_fun_RES)
show ?thesis
unfolding isa_maybe_push_to_occs_list_st_def maybe_push_to_occs_list2_alt_def eq
apply (refine_vcg find_best_subsumption_candidate_and_push[OF SS' _ occs]
mop_cocc_list_append_mop_occ_list_append occs)
subgoal using length by auto
subgoal by auto
subgoal by auto
subgoal by (rule length_bounded)
subgoal by auto
subgoal using SS' C valid notin_all_occurrences_notin_cocc[OF occs, of C]
by (auto 9 2 intro!: twl_st_heur_restart_occs_set_occsI
intro!: valid_occs_append
simp: push_to_occs_list2_pre_def)
subgoal using SS' C valid occs by auto
done
qed
lemma subsumption_cases_lhs:
assumes
‹(a,a')∈Id›
‹⋀b b'. a = SUBSUMED_BY b ⟹ a' = SUBSUMED_BY b' ⟹ f b ≤ ⇓S (f' b')›
‹⋀b b' c c'. a = STRENGTHENED_BY b c ⟹ a' = STRENGTHENED_BY b' c' ⟹ g b c ≤ ⇓S (g' b' c')›
‹⋀b b' c c'. a = NONE ⟹ a' = NONE ⟹ h ≤ ⇓S h'›
shows ‹(case a of SUBSUMED_BY b ⇒ f b | STRENGTHENED_BY b c ⇒ g b c | NONE ⇒ h) ≤⇓ S
(case a' of SUBSUMED_BY b ⇒ f' b| STRENGTHENED_BY b c ⇒ g' b c | NONE ⇒ h')›
using assms by (auto split: subsumption.splits)
definition arena_promote_st_wl :: ‹'v twl_st_wl ⇒ nat ⇒ 'v twl_st_wl› where
‹arena_promote_st_wl = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) C.
(M, fmupd C (N ∝ C, True) N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q))›
lemma clss_size_corr_restart_promote:
‹clss_size_corr_restart b d {#} f g h {#} j {#} (lcount) ⟹
¬irred b C ⟹ C ∈# dom_m b ⟹
clss_size_corr_restart (fmupd C (b ∝ C, True) b) d {#} f g h {#} j {#}
(clss_size_decr_lcount (lcount))›
unfolding clss_size_corr_restart_def
by (auto simp: clss_size_decr_lcount_def clss_size_def
learned_clss_l_mapsto_upd_in_irrelev size_remove1_mset_If)
lemma vdom_m_promote_same:
‹C ∈# dom_m b ⟹ vdom_m A m (fmupd C (b ∝ C, True) b) = vdom_m A m ( b)›
by (auto simp: vdom_m_def)
lemma mop_arena_promote_st_spec:
assumes T: ‹(S, T) ∈ twl_st_heur_restart_occs' r u› and
C: ‹C ∈# dom_m (get_clauses_wl T)› and
irred: ‹¬irred (get_clauses_wl T) C› and
eq: ‹set_mset (all_init_atms_st (arena_promote_st_wl T C)) = set_mset (all_init_atms_st T)›
shows ‹mop_arena_promote_st S C ≤ SPEC (λU. (U, arena_promote_st_wl T C)∈{(U,V). (U,V)∈twl_st_heur_restart_occs' r u ∧ get_occs U = get_occs S ∧ get_aivdom U = get_aivdom S})›
proof -
have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x
by auto
have H': ‹A = B ⟹ A x ⟹ B x› for A B x
by auto
note cong = trail_pol_cong[of _ _ ‹(get_trail_wl_heur S, get_trail_wl T)›]
heuristic_rel_cong[of _ _ ‹get_heur S›]
option_lookup_clause_rel_cong[of _ _ ‹(get_conflict_wl_heur S, get_conflict_wl T)›]
isa_vmtf_cong[of _ _ ‹get_vmtf_heur S›]
vdom_m_cong[THEN H, of _ _ _ ‹get_watched_wl T› ‹get_clauses_wl (T)›]
isasat_input_nempty_cong[THEN iffD1]
isasat_input_bounded_cong[THEN iffD1]
cach_refinement_empty_cong[THEN H', of _ _ ‹get_conflict_cach S›]
phase_saving_cong[THEN H']
ℒ⇩a⇩l⇩l_cong[THEN H]
D⇩0_cong[THEN H]
map_fun_rel_D⇩0_cong[of _ _ ‹(get_watched_wl_heur S, get_watched_wl T)›]
vdom_m_cong[symmetric, of _ _ ‹get_watched_wl T› ‹get_clauses_wl (T)›]
ℒ⇩a⇩l⇩l_cong isasat_input_nempty_cong
note cong = cong[OF eq[symmetric]]
have valid: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl T) (set (get_vdom S))› and
size: ‹clss_size_corr_restart (get_clauses_wl T)
(IsaSAT_Setup.get_unkept_unit_init_clss_wl T) {#}
(IsaSAT_Setup.get_kept_unit_init_clss_wl T)
(IsaSAT_Setup.get_kept_unit_learned_clss_wl T) (get_subsumed_init_clauses_wl T) {#}
(get_init_clauses0_wl T) {#} (get_learned_count S)›
using T unfolding twl_st_heur_restart_occs_def by fast+
then have irred': ‹arena_status (get_clauses_wl_heur S) C ≠ IRRED›
using irred by (simp add: C arena_lifting(24))
have 1: ‹1 ≤ get_learned_count_number S›
by (rule red_in_dom_number_of_learned_ge1_twl_st_heur_restart_occs[OF T C irred'])
have 2: ‹arena_is_valid_clause_idx (get_clauses_wl_heur S) C›
using C valid unfolding arena_is_valid_clause_idx_def by auto
have valid': ‹valid_arena (arena_set_status (get_clauses_wl_heur S) C IRRED)
(fmupd C (get_clauses_wl T ∝ C, True) (get_clauses_wl T)) (set (get_vdom S))›
by (rule valid_arena_arena_set_status[OF valid])
(use C in auto)
show ?thesis
unfolding mop_arena_promote_st_def mop_arena_set_status_def
nres_monad3
apply refine_vcg
subgoal by (rule 1)
subgoal by (rule 2)
subgoal
apply (cases T)
using T C valid' irred vdom_m_promote_same cong[unfolded all_init_atms_st_def] cong[unfolded all_init_atms_st_def]
by (auto simp add: twl_st_heur_restart_occs_def arena_promote_st_wl_def
clss_size_corr_restart_promote vdom_m_promote_same simp flip: learned_clss_count_def)
done
qed
definition mark_garbage_wl2 :: ‹nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹mark_garbage_wl2 = (λC (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q).
(M, fmdrop C N, D, NE, UE, NEk, UEk, (if irred N C then add_mset (mset (N ∝ C)) else id) NS,
(if ¬irred N C then add_mset (mset (N ∝ C)) else id) US, N0, U0, WS, Q))›
definition mark_garbage_wl_no_learned_reset :: ‹nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹mark_garbage_wl_no_learned_reset = (λC (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q).
(M, fmdrop C N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q))›
definition add_clauses_to_subsumed_wl :: ‹nat ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹add_clauses_to_subsumed_wl = (λC (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q).
(M, N, D, NE, UE, NEk, UEk, (if irred N C then add_mset (mset (N ∝ C)) else id) NS,
(if ¬irred N C then add_mset (mset (N ∝ C)) else id) US, N0, U0, WS, Q))›
lemma subsume_or_strengthen_wl_alt_def[unfolded Down_id_eq]:
‹⇓Id (subsume_or_strengthen_wl C s T) ≥ do {
ASSERT(subsume_or_strengthen_wl_pre C s T);
(case s of
NONE ⇒ RETURN T
| SUBSUMED_BY C' ⇒ do {
let _ = C ∈#dom_m (get_clauses_wl T);
let _ = C' ∈#dom_m (get_clauses_wl T);
let _ = log_clause T C;
let U = mark_garbage_wl2 C T;
let V = (if ¬irred (get_clauses_wl T) C' ∧ irred (get_clauses_wl T) C then arena_promote_st_wl U C' else U);
ASSERT (set_mset (all_init_atms_st V) = set_mset (all_init_atms_st T));
let V = V;
RETURN V
}
| STRENGTHENED_BY L C' ⇒ strengthen_clause_wl C C' L T)
}›
proof -
have subsume_or_strengthen_wl_def:
‹subsume_or_strengthen_wl = (λC s (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do {
ASSERT(subsume_or_strengthen_wl_pre C s (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
(case s of
NONE ⇒ RETURN (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)
| SUBSUMED_BY C' ⇒ do {
let _ = ();
let T = (M, fmdrop C (if ¬irred N C' ∧ irred N C then fmupd C' (N ∝ C', True) N else N), D,
NE, UE, NEk, UEk, (if irred N C then add_mset (mset (N ∝ C)) else id) NS,
(if ¬irred N C then add_mset (mset (N ∝ C)) else id) US, N0, U0, Q, W);
ASSERT (set_mset (all_init_atms_st T) = set_mset (all_init_atms_st (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)));
RETURN T
}
| STRENGTHENED_BY L C' ⇒ strengthen_clause_wl C C' L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))
})›
unfolding subsume_or_strengthen_wl_def Let_def by auto
show ?thesis
unfolding subsume_or_strengthen_wl_def
case_wl_split state_wl_recompose
apply (refine_vcg subsumption_cases_lhs)
subgoal by auto
subgoal
by (cases T)
(auto simp: arena_promote_st_wl_def mark_garbage_wl2_def state_wl_l_def fmdrop_fmupd
subsume_or_strengthen_wl_pre_def subsume_or_strengthen_pre_def)
subgoal
by (cases T)
(auto simp: arena_promote_st_wl_def mark_garbage_wl2_def state_wl_l_def fmdrop_fmupd
subsume_or_strengthen_wl_pre_def subsume_or_strengthen_pre_def)
subgoal by auto
done
qed
lemma mark_garbage_wl2_simp[simp]:
‹get_trail_wl (mark_garbage_wl2 C S) = get_trail_wl S›
‹IsaSAT_Setup.get_unkept_unit_init_clss_wl (mark_garbage_wl2 C S) = IsaSAT_Setup.get_unkept_unit_init_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_init_clss_wl (mark_garbage_wl2 C S) = IsaSAT_Setup.get_kept_unit_init_clss_wl S›
‹irred (get_clauses_wl S) C ⟹
get_subsumed_init_clauses_wl (mark_garbage_wl2 C S) = add_mset (mset (get_clauses_wl S ∝ C)) (get_subsumed_init_clauses_wl S)›
‹¬irred (get_clauses_wl S) C ⟹
get_subsumed_init_clauses_wl (mark_garbage_wl2 C S) = (get_subsumed_init_clauses_wl S)›
‹IsaSAT_Setup.get_unkept_unit_learned_clss_wl (mark_garbage_wl2 C S) = IsaSAT_Setup.get_unkept_unit_learned_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_learned_clss_wl (mark_garbage_wl2 C S) = IsaSAT_Setup.get_kept_unit_learned_clss_wl S›
‹irred (get_clauses_wl S) C ⟹
get_subsumed_learned_clauses_wl (mark_garbage_wl2 C S) = (get_subsumed_learned_clauses_wl S)›
‹¬irred (get_clauses_wl S) C ⟹
get_subsumed_learned_clauses_wl (mark_garbage_wl2 C S) = add_mset (mset (get_clauses_wl S ∝ C)) (get_subsumed_learned_clauses_wl S)›
‹literals_to_update_wl (mark_garbage_wl2 C S) = literals_to_update_wl S›
‹get_watched_wl (mark_garbage_wl2 C S) = get_watched_wl S›
‹get_clauses_wl (mark_garbage_wl2 C S) = fmdrop C (get_clauses_wl S)›
‹get_init_clauses0_wl (mark_garbage_wl2 C S) = get_init_clauses0_wl (S)›
‹get_learned_clauses0_wl (mark_garbage_wl2 C S) = get_learned_clauses0_wl (S)›
‹get_conflict_wl (mark_garbage_wl2 C S) = get_conflict_wl S›
apply (solves ‹cases S; auto simp: mark_garbage_wl2_def›)+
done
lemma mark_garbage_wl2_simp2[simp]:
‹C ∈#dom_m (get_clauses_wl S) ⟹ all_init_atms_st (mark_garbage_wl2 C S) = all_init_atms_st (S)›
by (cases S)
(auto simp: mark_garbage_wl2_def all_init_atms_st_def all_init_atms_def all_init_lits_def
learned_clss_l_mapsto_upd_in_irrelev size_remove1_mset_If init_clss_l_fmdrop_if image_mset_remove1_mset_if
simp del: all_init_atms_def[symmetric]
cong: image_mset_cong2 filter_mset_cong2)
definition remove_lit_from_clause_wl :: ‹_› where
‹remove_lit_from_clause_wl C L' = (λ(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W).
(M, fmupd C (remove1 L' (N ∝ C), irred N C) N, D, NE, UE, NEk, UEk,
(if irred N C then add_mset (mset (N ∝ C)) else id) NS,
(if ¬irred N C then add_mset (mset (N ∝ C)) else id) US, N0, U0, Q, W))›
lemma remove_lit_from_clauses_wl_simp[simp]:
‹C ∈# dom_m (get_clauses_wl S) ⟹ dom_m (get_clauses_wl (remove_lit_from_clause_wl C L' S)) = dom_m (get_clauses_wl S)›
‹get_trail_wl (remove_lit_from_clause_wl C L' S) = get_trail_wl S›
‹IsaSAT_Setup.get_unkept_unit_init_clss_wl (remove_lit_from_clause_wl C L' S) = IsaSAT_Setup.get_unkept_unit_init_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_init_clss_wl (remove_lit_from_clause_wl C L' S) = IsaSAT_Setup.get_kept_unit_init_clss_wl S›
‹irred (get_clauses_wl S) C ⟹
get_subsumed_init_clauses_wl (remove_lit_from_clause_wl C L' S) = add_mset (mset (get_clauses_wl S ∝ C)) (get_subsumed_init_clauses_wl S)›
‹¬irred (get_clauses_wl S) C ⟹
get_subsumed_init_clauses_wl (remove_lit_from_clause_wl C L' S) = (get_subsumed_init_clauses_wl S)›
‹IsaSAT_Setup.get_unkept_unit_learned_clss_wl (remove_lit_from_clause_wl C L' S) = IsaSAT_Setup.get_unkept_unit_learned_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_learned_clss_wl (remove_lit_from_clause_wl C L' S) = IsaSAT_Setup.get_kept_unit_learned_clss_wl S›
‹irred (get_clauses_wl S) C ⟹
get_subsumed_learned_clauses_wl (remove_lit_from_clause_wl C L' S) = (get_subsumed_learned_clauses_wl S)›
‹¬irred (get_clauses_wl S) C ⟹
get_subsumed_learned_clauses_wl (remove_lit_from_clause_wl C L' S) = add_mset (mset (get_clauses_wl S ∝ C)) (get_subsumed_learned_clauses_wl S)›
‹literals_to_update_wl (remove_lit_from_clause_wl C L' S) = literals_to_update_wl S›
‹get_watched_wl (remove_lit_from_clause_wl C L' S) = get_watched_wl S›
‹get_clauses_wl (remove_lit_from_clause_wl C L' S) = (get_clauses_wl S) (C ↪ remove1 L' (get_clauses_wl S ∝ C))›
‹get_init_clauses0_wl (remove_lit_from_clause_wl C L' S) = get_init_clauses0_wl (S)›
‹get_learned_clauses0_wl (remove_lit_from_clause_wl C L' S) = get_learned_clauses0_wl (S)›
‹get_conflict_wl (remove_lit_from_clause_wl C L' S) = get_conflict_wl S›
by (solves ‹cases S; auto simp: remove_lit_from_clause_wl_def›)+
lemma in_all_lits_of_wl_ain_atms_of_iff: ‹L ∈# all_init_lits_of_wl N ⟷ atm_of L ∈# all_init_atms_st N›
using ℒ⇩a⇩l⇩l_all_init_atms(2) in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n by blast
lemma init_clss_lf_mapsto_upd_irrelev: ‹C ∈# dom_m N ⟹ ¬irred N C ⟹
init_clss_lf (fmupd C (D, True) N) = add_mset D (init_clss_lf N)›
by (simp add: init_clss_l_mapsto_upd_irrelev)
lemma arena_promote_dom_m_get_clauses_wl[simp]:
‹C ∈# dom_m (get_clauses_wl S) ⟹
dom_m (get_clauses_wl (arena_promote_st_wl S C)) = dom_m (get_clauses_wl S)›
by (cases S) (auto simp: arena_promote_st_wl_def)
text ‹
The assertions here are an artefact of how the refinement frameworks handles if-then-else. It splits
lhs ifs, but not rhs splits when they appear whithin an expression.
›
lemma strengthen_clause_wl_alt_def[unfolded Down_id_eq]:
‹⇓Id(strengthen_clause_wl C D L' S) ≥ do {
ASSERT (subsume_or_strengthen_wl_pre C (STRENGTHENED_BY L' D) S);
let m = length (get_clauses_wl S ∝ C);
let n = length (get_clauses_wl S ∝ D);
let E = remove1 (- L') (get_clauses_wl S ∝ C);
let _ = C ∈# dom_m (get_clauses_wl S);
let _ = D ∈# dom_m (get_clauses_wl S);
let T = remove_lit_from_clause_wl C (-L') S;
_ ← log_clause2 T C;
if False then RETURN T
else if m = n then do {
let T = add_clauses_to_subsumed_wl D (T);
ASSERT (set_mset (all_init_atms_st T) = set_mset (all_init_atms_st S));
ASSERT (set_mset (all_init_atms_st (if ¬irred (get_clauses_wl S) C ∧ irred (get_clauses_wl S) D then arena_promote_st_wl T C else T)) = set_mset (all_init_atms_st S));
let U = (if ¬irred (get_clauses_wl S) C ∧ irred (get_clauses_wl S) D then arena_promote_st_wl T C else T);
ASSERT (set_mset (all_init_atms_st (mark_garbage_wl_no_learned_reset D U)) = set_mset (all_init_atms_st S));
let U = mark_garbage_wl_no_learned_reset D U;
RETURN U
}
else RETURN T
}›
proof -
have le2: ‹length (get_clauses_wl S ∝ C) ≠ 2› and
CD: ‹C ≠ D› and
C_dom: ‹C ∈# dom_m (get_clauses_wl S)›and
D_dom: ‹D ∈# dom_m (get_clauses_wl S)› and
subs: ‹remove1_mset L' (mset (get_clauses_wl S ∝ D)) ⊆# remove1_mset (- L') (mset (get_clauses_wl S ∝ C))› and
eq_le: ‹length (get_clauses_wl S ∝ D) = length (get_clauses_wl S ∝ C) ⟹
remove1_mset L' (mset (get_clauses_wl S ∝ D)) = remove1_mset (- L') (mset (get_clauses_wl S ∝ C))›
if pre: ‹subsume_or_strengthen_wl_pre C (STRENGTHENED_BY L' D) S›
proof -
have
L: ‹-L' ∈# mset (get_clauses_wl S ∝ C)›
‹L' ∈# mset (get_clauses_wl S ∝ D)› and
‹remove1_mset L' (mset (get_clauses_wl S ∝ D)) ⊆# remove1_mset (- L') (mset (get_clauses_wl S ∝ C))›
‹¬ tautology (mset (get_clauses_wl S ∝ D))›
‹¬ tautology
(remove1_mset L' (mset (get_clauses_wl S ∝ D)) +
remove1_mset (- L') (mset (get_clauses_wl S ∝ C)))›
using that unfolding subsume_or_strengthen_wl_pre_def
subsume_or_strengthen_pre_def apply -
by (solves ‹normalize_goal+; clarsimp›)+
show ‹length (get_clauses_wl S ∝ C) ≠ 2› and ‹C ≠ D› and ‹C ∈# dom_m (get_clauses_wl S)› and
‹D ∈# dom_m (get_clauses_wl S)› and
subs: ‹remove1_mset L' (mset (get_clauses_wl S ∝ D)) ⊆# remove1_mset (- L') (mset (get_clauses_wl S ∝ C))›
using that unfolding subsume_or_strengthen_wl_pre_def
subsume_or_strengthen_pre_def apply -
by (solves ‹normalize_goal+; clarsimp›)+
show ‹remove1_mset L' (mset (get_clauses_wl S ∝ D)) = remove1_mset (- L') (mset (get_clauses_wl S ∝ C))›
if ‹length (get_clauses_wl S ∝ D) = length (get_clauses_wl S ∝ C)›
using multi_member_split[OF L(1)] multi_member_split[OF L(2)] subs that
by (auto simp del: size_mset simp flip: size_mset simp: subseteq_mset_size_eql_iff)
qed
have add_subsumed_same:
‹set_mset (all_init_atms_st (add_clauses_to_subsumed_wl D S)) = set_mset (all_init_atms_st S)›
if ‹D ∈# dom_m (get_clauses_wl S)› for S D
using that
apply (cases S)
apply (auto simp: all_init_atms_def all_init_atms_st_def add_clauses_to_subsumed_wl_def
all_init_lits_def ran_m_def all_lits_of_mm_add_mset
dest!: multi_member_split[of D]
simp del: all_init_atms_def[symmetric])
done
have H1: ‹set_mset (all_init_atms_st (arena_promote_st_wl S C)) = set_mset (all_init_atms_st S)›
if ‹set_mset (all_lits_of_m (mset (get_clauses_wl S ∝ C))) ⊆ set_mset (all_init_lits_of_wl S)› and
‹C ∈# dom_m (get_clauses_wl S)›
for C S
using that
apply (cases ‹irred (get_clauses_wl S) C›)
subgoal
using fmupd_same[of C ‹get_clauses_wl S›]
apply (cases S; cases ‹fmlookup (get_clauses_wl S) C›)
apply (auto simp: all_init_atms_st_def add_clauses_to_subsumed_wl_def
all_init_atms_def all_init_lits_def ran_m_def all_lits_of_mm_add_mset arena_promote_st_wl_def
remove_lit_from_clause_wl_def image_Un
dest!: multi_member_split[of D]
simp del: all_init_atms_def[symmetric] fmupd_same
cong: filter_mset_cong image_mset_cong2)
apply auto
done
subgoal
by (cases S)
(auto simp: all_init_atms_st_def add_clauses_to_subsumed_wl_def all_init_atms_def
all_init_lits_def all_lits_of_mm_add_mset arena_promote_st_wl_def init_clss_l_mapsto_upd
init_clss_l_mapsto_upd_irrelev all_init_lits_of_wl_def ac_simps
dest!: multi_member_split[of D]
simp del: all_init_atms_def[symmetric])
done
have K: ‹set_mset
(all_init_atms_st
(arena_promote_st_wl (add_clauses_to_subsumed_wl D (remove_lit_from_clause_wl C (- L') S)) C)) =
set_mset (all_init_atms_st S)› (is ?A) and
K2: ‹set_mset (all_init_atms_st (remove_lit_from_clause_wl C (- L') S)) = set_mset (all_init_atms_st S)› (is ?B) and
K3: ‹length (get_clauses_wl S ∝ C) = length (get_clauses_wl S ∝ D) ⟹
set_mset (all_init_atms_st (mark_garbage_wl_no_learned_reset D
(if ¬ irred (get_clauses_wl S) C ∧ irred (get_clauses_wl S) D
then arena_promote_st_wl (add_clauses_to_subsumed_wl D (remove_lit_from_clause_wl C (- L') S)) C
else add_clauses_to_subsumed_wl D (remove_lit_from_clause_wl C (- L') S)))) =
set_mset (all_init_atms_st S)› (is ‹_ ⟹ ?C›)
if pre: ‹subsume_or_strengthen_wl_pre C (STRENGTHENED_BY L' D) S›
proof -
obtain x xa where
Sx: ‹(S, x) ∈ state_wl_l None› and
‹2 < length (get_clauses_wl S ∝ C)› and
‹2 ≤ length (get_clauses_l x ∝ C)› and
‹C ∈# dom_m (get_clauses_l x)› and
‹count_decided (get_trail_l x) = 0› and
‹distinct (get_clauses_l x ∝ C)› and
‹∀L∈set (get_clauses_l x ∝ C). undefined_lit (get_trail_l x) L› and
‹get_conflict_l x = None› and
‹C ∉ set (get_all_mark_of_propagated (get_trail_l x))› and
‹clauses_to_update_l x = {#}› and
‹twl_list_invs x› and
xxa: ‹(x, xa) ∈ twl_st_l None› and
struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of xa)› and
inv: ‹twl_struct_invs xa› and
‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of xa)› and
‹L' ∈# mset (get_clauses_l x ∝ D)› and
‹- L' ∈# mset (get_clauses_l x ∝ C)› and
‹¬ tautology (mset (get_clauses_l x ∝ D))› and
‹D ≠ 0› and
‹remove1_mset L' (mset (get_clauses_l x ∝ D)) ⊆# remove1_mset (- L') (mset (get_clauses_l x ∝ C))› and
‹D ∈# dom_m (get_clauses_l x)› and
‹distinct (get_clauses_l x ∝ D)› and
‹D ∉ set (get_all_mark_of_propagated (get_trail_l x))› and
‹2 ≤ length (get_clauses_l x ∝ D)› and
‹¬ tautology
(remove1_mset L' (mset (get_clauses_l x ∝ D)) +
remove1_mset (- L') (mset (get_clauses_l x ∝ C)))›
using pre unfolding subsume_or_strengthen_wl_pre_def subsume_or_strengthen_pre_def subsumption.simps
apply - apply normalize_goal+ by blast
have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of xa)›
using struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast
then have ‹atms_of_mm (learned_clss (state⇩W_of xa)) ⊆ atms_of_mm (init_clss (state⇩W_of xa))›
unfolding cdcl⇩W_restart_mset.no_strange_atm_def by fast
then have lits_C_in_all:
‹set_mset (all_lits_of_m (mset (get_clauses_wl S ∝ C))) ⊆ set_mset (all_init_lits_of_wl S)›
if ‹¬irred (get_clauses_wl S) C›
using that C_dom[OF pre] Sx xxa unfolding set_eq_iff in_set_all_atms_iff
in_set_all_atms_iff in_set_all_init_atms_iff get_unit_clauses_wl_alt_def
by (cases xa; cases x; cases S)
(auto 4 3 simp: twl_st_l_def state_wl_l_def mset_take_mset_drop_mset' ran_m_def image_image
conj_disj_distribR Collect_disj_eq image_Un Collect_conv_if all_init_lits_of_wl_def
in_all_lits_of_mm_ain_atms_of_iff in_all_lits_of_m_ain_atms_of_iff atm_of_eq_atm_of
dest!: multi_member_split[of ‹C :: nat›])
have [simp]: ‹get_clauses_wl (add_clauses_to_subsumed_wl D (remove_lit_from_clause_wl C (- L') S)) ∝ C =
get_clauses_wl (remove_lit_from_clause_wl C (- L') S) ∝ C›
by (cases S) (auto simp: add_clauses_to_subsumed_wl_def remove_lit_from_clause_wl_def)
have init_decomp:
‹irred N D ⟹ D ∈# dom_m N ⟹ init_clss_l N = add_mset ((N ∝ D, irred N D)) (init_clss_l (fmdrop D N))› for D N
using distinct_mset_dom[of N] apply (cases ‹the (fmlookup N D)›)
by (auto simp: ran_m_def dest!: multi_member_split
intro!: image_mset_cong2 intro!: filter_mset_cong2)
have [simp]: ‹fmdrop C (fmdrop D (fmupd C E b)) = fmdrop C (fmdrop D b)› for E b
by (metis fmdrop_comm fmdrop_fmupd_same)
show ?A
using C_dom[OF that] D_dom[OF that] CD[OF that] subs[OF that]
all_lits_of_m_mono[of ‹mset (remove1 (-L') (get_clauses_wl S ∝ C))›
‹mset (get_clauses_wl S ∝ C)›, THEN set_mset_mono]
all_lits_of_m_mono[of ‹mset (remove1 (-L') (get_clauses_wl S ∝ D))›
‹mset (get_clauses_wl S ∝ D)›, THEN set_mset_mono]
apply (cases S)
apply (auto simp: remove_lit_from_clause_wl_def add_clauses_to_subsumed_wl_def
arena_promote_st_wl_def all_init_atms_def all_init_atms_st_def all_init_lits_def image_Un fmdrop_fmupd_same
all_lits_of_mm_add_mset init_clss_l_mapsto_upd init_decomp[of _ D] init_decomp[of ‹fmdrop D _› C]
init_clss_l_fmdrop_irrelev
simp del: all_init_atms_def[symmetric] dest!: multi_member_split[of D])
apply (auto simp: remove_lit_from_clause_wl_def add_clauses_to_subsumed_wl_def
arena_promote_st_wl_def all_init_atms_def all_init_atms_st_def all_init_lits_def image_Un fmdrop_fmupd_same
all_lits_of_mm_add_mset init_clss_l_mapsto_upd init_decomp[of _ D] init_decomp[of ‹_› C] init_clss_l_fmdrop_irrelev
simp del: all_init_atms_def[symmetric] dest!: multi_member_split[of D])
using lits_C_in_all[unfolded all_init_lits_of_wl_def, simplified]
apply (auto simp: remove_lit_from_clause_wl_def add_clauses_to_subsumed_wl_def
arena_promote_st_wl_def all_init_atms_def all_init_atms_st_def all_init_lits_def image_Un fmdrop_fmupd_same
all_lits_of_mm_add_mset init_clss_l_mapsto_upd init_decomp[of _ D] init_decomp[of ‹_› C] ac_simps
simp del: all_init_atms_def[symmetric] dest!: multi_member_split[of D])
done
show ?B
using C_dom[OF that] D_dom[OF that] CD[OF that] subs[OF that]
all_lits_of_m_mono[of ‹mset (remove1 (-L') (get_clauses_wl S ∝ C))›
‹mset (get_clauses_wl S ∝ C)›, THEN set_mset_mono]
all_lits_of_m_mono[of ‹mset (remove1 (-L') (get_clauses_wl S ∝ D))›
‹mset (get_clauses_wl S ∝ D)›, THEN set_mset_mono]
apply (cases S)
apply (auto simp: remove_lit_from_clause_wl_def add_clauses_to_subsumed_wl_def
arena_promote_st_wl_def all_init_atms_def all_init_atms_st_def all_init_lits_def image_Un fmdrop_fmupd_same
all_lits_of_mm_add_mset init_clss_l_mapsto_upd init_decomp[of _ D] init_decomp[of ‹fmdrop D _› C]
init_clss_l_fmdrop_irrelev
simp del: all_init_atms_def[symmetric] dest!: multi_member_split[of D])
apply (auto simp: remove_lit_from_clause_wl_def add_clauses_to_subsumed_wl_def
arena_promote_st_wl_def all_init_atms_def all_init_atms_st_def all_init_lits_def image_Un fmdrop_fmupd_same
all_lits_of_mm_add_mset init_clss_l_mapsto_upd init_decomp[of _ D] init_decomp[of ‹_› C] init_clss_l_fmdrop_irrelev init_clss_l_mapsto_upd_irrel
simp del: all_init_atms_def[symmetric] dest!: multi_member_split[of D])
done
have KK[simp]: ‹E ∈# b ⟹ add_mset (mset E) (mset `# remove1_mset E b + F) = mset `# b + F› for b E F
by (auto dest!: multi_member_split)
have 1: ‹set_mset (all_init_atms_st (mark_garbage_wl_no_learned_reset D (add_clauses_to_subsumed_wl D S))) =
set_mset (all_init_atms_st S)›
if ‹D ∈# dom_m (get_clauses_wl S)› for S
using that
apply (cases S)
apply (clarsimp simp only: remove_lit_from_clause_wl_def add_clauses_to_subsumed_wl_def
all_lits_of_mm_add_mset init_clss_l_mapsto_upd init_decomp[of _ D]
init_clss_l_fmdrop_irrelev mark_garbage_wl_no_learned_reset_def arena_promote_st_wl_def
all_init_atms_st_def all_init_atms_def get_clauses_wl.simps all_init_lits_def fmupd_idem
init_clss_l_mapsto_upd_irrel init_clss_lf_fmdrop_irrelev init_clss_lf_mapsto_upd_irrelev
split: if_splits intro!: impI conjI
simp del: all_init_atms_def[symmetric] dest!: multi_member_split[of D])
apply (intro conjI impI)
apply simp
apply simp
apply (subst (2)init_decomp[of _ D])
apply (auto simp add: all_lits_of_mm_add_mset)[3]
apply (subst (2)init_decomp[of _ D])
apply (auto simp add: all_lits_of_mm_add_mset)[3]
done
have 2: ‹set_mset (all_init_atms_st (remove_lit_from_clause_wl C (- L') S)) =
set_mset (all_init_atms_st S)› if ‹C ∈# dom_m (get_clauses_wl S)›for S
using that
all_lits_of_m_mono[of ‹mset (remove1 (-L') (get_clauses_wl S ∝ C))›
‹mset (get_clauses_wl S ∝ C)›, THEN set_mset_mono]
apply (cases S)
apply (auto simp: remove_lit_from_clause_wl_def add_clauses_to_subsumed_wl_def
arena_promote_st_wl_def all_init_atms_def all_init_atms_st_def all_init_lits_def image_Un fmdrop_fmupd_same
all_lits_of_mm_add_mset init_clss_l_mapsto_upd init_decomp[of _ C]
init_clss_l_fmdrop_irrelev init_clss_l_mapsto_upd_irrel
simp del: all_init_atms_def[symmetric] dest!: multi_member_split[of C])
done
have init_decomp:
‹NO_MATCH (fmdrop D N') N ⟹ irred N D ⟹ D ∈# dom_m N ⟹ init_clss_l N = add_mset ((N ∝ D, irred N D)) (init_clss_l (fmdrop D N))› for D N
using distinct_mset_dom[of N] apply (cases ‹the (fmlookup N D)›)
by (auto simp: ran_m_def dest!: multi_member_split
intro!: image_mset_cong2 intro!: filter_mset_cong2)
assume ‹length (get_clauses_wl S ∝ C) = length (get_clauses_wl S ∝ D)›
note eq = eq_le[OF pre this[symmetric]]
have 3: ‹irred (get_clauses_wl S) D ⟹
(mark_garbage_wl_no_learned_reset D
(arena_promote_st_wl (add_clauses_to_subsumed_wl D (remove_lit_from_clause_wl C (- L') S)) C)) =
(mark_garbage_wl_no_learned_reset D
(add_clauses_to_subsumed_wl D (arena_promote_st_wl (remove_lit_from_clause_wl C (- L') S) C)))›
apply (cases S)
apply (auto simp: mark_garbage_wl_no_learned_reset_def arena_promote_st_wl_def
add_clauses_to_subsumed_wl_def remove_lit_from_clause_wl_def)
done
have ‹set_mset (all_init_atms_st (arena_promote_st_wl (remove_lit_from_clause_wl C (- L') S) C)) =
set_mset (all_init_atms_st S)›
if ‹¬irred (get_clauses_wl S) C› ‹irred (get_clauses_wl S) D›
using that D_dom[OF pre] C_dom[OF pre] eq[symmetric]
all_lits_of_m_mono[of ‹mset (remove1 (L') (get_clauses_wl S ∝ D))›
‹mset (get_clauses_wl S ∝ D)›, THEN set_mset_mono]
apply (cases S)
apply (auto simp: remove_lit_from_clause_wl_def add_clauses_to_subsumed_wl_def
arena_promote_st_wl_def all_init_atms_def all_init_atms_st_def all_init_lits_def image_Un fmdrop_fmupd_same
all_lits_of_mm_add_mset init_clss_l_mapsto_upd init_clss_l_mapsto_upd_irrel
init_clss_l_fmdrop_irrelev init_clss_l_mapsto_upd_irrel all_init_atms_st_def
init_clss_l_mapsto_upd_irrel init_clss_lf_mapsto_upd_irrelev
simp del: all_init_atms_def[symmetric] dest!: )
apply (subst init_decomp[of D])
apply (auto simp add: all_lits_of_mm_add_mset image_Un)
done
then show ?C
using C_dom[OF that] D_dom[OF that] CD[OF that] subs[OF that]
all_lits_of_m_mono[of ‹mset (remove1 (-L') (get_clauses_wl S ∝ C))›
‹mset (get_clauses_wl S ∝ C)›, THEN set_mset_mono]
all_lits_of_m_mono[of ‹mset (remove1 (-L') (get_clauses_wl S ∝ D))›
‹mset (get_clauses_wl S ∝ D)›, THEN set_mset_mono]
apply (cases ‹¬ irred (get_clauses_wl S) C ∧ irred (get_clauses_wl S) D›)
subgoal
apply (simp only: if_True simp_thms)
apply (simp add: 1 2 3)
done
subgoal
apply (simp only: if_False 1)
apply (auto simp: 2 1)
done
done
qed
have strengthen_clause_wl_alt_def:
‹strengthen_clause_wl = (λC C' L (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do {
ASSERT (subsume_or_strengthen_wl_pre C (STRENGTHENED_BY L C') (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
E ← SPEC (λE. mset E = mset (remove1 (-L) (N ∝ C)));
let _ = ();
let _ = ();
let _ = ();
_ ← RETURN ();
if length (N ∝ C) = 2
then do {
ASSERT (length (remove1 (-L) (N ∝ C)) = 1);
let L = hd E;
RETURN (Propagated L 0 # M, fmdrop C' (fmdrop C N), D,
(if irred N C' then add_mset (mset (N ∝ C')) else id) NE,
(if ¬irred N C' then add_mset (mset (N ∝ C')) else id) UE,
(if irred N C then add_mset {#L#} else id) NEk, (if ¬irred N C then add_mset {#L#} else id) UEk,
((if irred N C then add_mset (mset (N ∝ C)) else id)) NS,
((if ¬irred N C then add_mset (mset (N ∝ C)) else id)) US,
N0, U0, add_mset (-L) Q, W)
}
else if length (N ∝ C) = length (N ∝ C')
then RETURN (M, fmdrop C' (fmupd C (E, irred N C ∨ irred N C') N), D, NE, UE, NEk, UEk,
((if irred N C' then add_mset (mset (N ∝ C')) else id) o (if irred N C then add_mset (mset (N ∝ C)) else id)) NS,
((if ¬irred N C' then add_mset (mset (N ∝ C')) else id) o (if ¬irred N C then add_mset (mset (N ∝ C)) else id)) US,
N0, U0, Q, W)
else RETURN (M, fmupd C (E, irred N C) N, D, NE, UE, NEk, UEk,
(if irred N C then add_mset (mset (N ∝ C)) else id) NS,
(if ¬irred N C then add_mset (mset (N ∝ C)) else id) US, N0, U0, Q, W)})›
unfolding strengthen_clause_wl_def Let_def by auto
have [refine0]: ‹subsume_or_strengthen_wl_pre C (STRENGTHENED_BY L' D) S ⟹
subsume_or_strengthen_wl_pre C (STRENGTHENED_BY L' D) S ⟹
(remove1 (- L') (get_clauses_wl S ∝ C), E) ∈ Id ⟹
log_clause2 (remove_lit_from_clause_wl C (- L') S) C
≤ Refine_Basic.SPEC (λc. (c, ()) ∈ Id)› for E
by (rule log_clause2_log_clause[THEN fref_to_Down_curry, THEN order_trans]) auto
show ?thesis
unfolding strengthen_clause_wl_alt_def case_wl_split state_wl_recompose Let_def [of ‹length _›]
apply (refine_vcg )
subgoal by auto
apply assumption
subgoal using le2 by blast
subgoal by auto
subgoal by auto
subgoal using D_dom by (clarsimp simp add: add_subsumed_same K K2)
subgoal using D_dom by (clarsimp simp add: add_subsumed_same K K2)
subgoal using D_dom by (clarsimp simp add: add_subsumed_same K3)
subgoal
using CD
by (cases S)
(auto simp: mark_garbage_wl_no_learned_reset_def add_clauses_to_subsumed_wl_def
arena_promote_st_wl_def remove_lit_from_clause_wl_def)
subgoal
by (cases S) (auto simp: remove_lit_from_clause_wl_def add_clauses_to_subsumed_wl_def)
done
qed
fun set_clauses_wl :: ‹_ ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹set_clauses_wl N (M, _, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) =
(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) ›
fun add_clause_to_subsumed :: ‹_ ⇒ _ ⇒ 'v twl_st_wl ⇒ 'v twl_st_wl› where
‹add_clause_to_subsumed b E (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, WS, Q) =
(M, N, D, NE, UE, NEk, UEk, (if b then add_mset E else id) NS,
(if ¬b then add_mset E else id) US, N0, U0, WS, Q) ›
lemma fmap_eq_iff_dom_m_lookup: ‹f = g ⟷ (dom_m f = dom_m g ∧ (∀k∈#dom_m f. fmlookup f k = fmlookup g k))›
by (metis fmap_ext in_dom_m_lookup_iff)
lemma mop_arena_shorten:
assumes ‹valid_arena N N' vdom› and
‹(i,j)∈nat_rel› and
‹(C,C')∈nat_rel› and
‹C ∈# dom_m N'› and
‹i≥2› ‹i ≤ length (N' ∝ C)›
shows
‹mop_arena_shorten C i N
≤ SPEC (λc. (c, N'(C' ↪ take j (N' ∝ C')))
∈ {(N⇩1,N⇩1'). valid_arena N⇩1 N⇩1' vdom ∧ length N⇩1 = length N})›
proof -
show ?thesis
unfolding mop_arena_shorten_def
apply refine_vcg
subgoal using assms unfolding arena_shorten_pre_def arena_is_valid_clause_idx_def
by (auto intro!: exI[of _ N'] simp: arena_lifting)
subgoal
using assms by (auto intro!: valid_arena_arena_shorten simp: arena_lifting)
done
qed
lemma count_list_distinct_If: ‹distinct xs ⟹ count_list xs x = (if x ∈ set xs then 1 else 0)›
by (simp add: count_mset_count_list distinct_count_atmost_1)
lemma set_clauses_wl_simp[simp]:
‹get_trail_wl (set_clauses_wl N S) = get_trail_wl S›
‹IsaSAT_Setup.get_unkept_unit_init_clss_wl (set_clauses_wl N S) = IsaSAT_Setup.get_unkept_unit_init_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_init_clss_wl (set_clauses_wl N S) = IsaSAT_Setup.get_kept_unit_init_clss_wl S›
‹get_subsumed_init_clauses_wl (set_clauses_wl N S) = (get_subsumed_init_clauses_wl S)›
‹get_subsumed_init_clauses_wl (set_clauses_wl N S) = (get_subsumed_init_clauses_wl S)›
‹IsaSAT_Setup.get_unkept_unit_learned_clss_wl (set_clauses_wl N S) = IsaSAT_Setup.get_unkept_unit_learned_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_learned_clss_wl (set_clauses_wl N S) = IsaSAT_Setup.get_kept_unit_learned_clss_wl S›
‹get_subsumed_learned_clauses_wl (set_clauses_wl N S) = (get_subsumed_learned_clauses_wl S)›
‹get_subsumed_learned_clauses_wl (set_clauses_wl N S) = (get_subsumed_learned_clauses_wl S)›
‹literals_to_update_wl (set_clauses_wl N S) = literals_to_update_wl S›
‹get_watched_wl (set_clauses_wl N S) = get_watched_wl S›
‹get_clauses_wl (set_clauses_wl N S) = N›
‹get_init_clauses0_wl (set_clauses_wl N S) = get_init_clauses0_wl (S)›
‹get_learned_clauses0_wl (set_clauses_wl N S) = get_learned_clauses0_wl (S)›
‹get_conflict_wl (set_clauses_wl N S) = get_conflict_wl S›
apply (solves ‹cases S; auto simp: ›)+
done
lemma add_clause_to_subsumed_simp[simp]:
‹get_trail_wl (add_clause_to_subsumed b N S) = get_trail_wl S›
‹IsaSAT_Setup.get_unkept_unit_init_clss_wl (add_clause_to_subsumed b N S) = IsaSAT_Setup.get_unkept_unit_init_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_init_clss_wl (add_clause_to_subsumed b N S) = IsaSAT_Setup.get_kept_unit_init_clss_wl S›
‹b ⟹ get_subsumed_init_clauses_wl (add_clause_to_subsumed b N S) = add_mset N (get_subsumed_init_clauses_wl S)›
‹¬b ⟹ get_subsumed_init_clauses_wl (add_clause_to_subsumed b N S) = (get_subsumed_init_clauses_wl S)›
‹IsaSAT_Setup.get_unkept_unit_learned_clss_wl (add_clause_to_subsumed b N S) = IsaSAT_Setup.get_unkept_unit_learned_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_learned_clss_wl (add_clause_to_subsumed b N S) = IsaSAT_Setup.get_kept_unit_learned_clss_wl S›
‹b ⟹
get_subsumed_learned_clauses_wl (add_clause_to_subsumed b N S) = (get_subsumed_learned_clauses_wl S)›
‹¬b ⟹ get_subsumed_learned_clauses_wl (add_clause_to_subsumed b N S) = add_mset N (get_subsumed_learned_clauses_wl S)›
‹literals_to_update_wl (add_clause_to_subsumed b N S) = literals_to_update_wl S›
‹get_watched_wl (add_clause_to_subsumed b N S) = get_watched_wl S›
‹get_clauses_wl (add_clause_to_subsumed b N S) = get_clauses_wl S›
‹get_init_clauses0_wl (add_clause_to_subsumed b N S) = get_init_clauses0_wl (S)›
‹get_learned_clauses0_wl (add_clause_to_subsumed b N S) = get_learned_clauses0_wl (S)›
‹get_conflict_wl (add_clause_to_subsumed b N S) = get_conflict_wl S›
apply (solves ‹cases S; auto simp: ›)+
done
lemma add_clauses_to_subsumed_wl_simp[simp]:
‹get_trail_wl (add_clauses_to_subsumed_wl N S) = get_trail_wl S›
‹IsaSAT_Setup.get_unkept_unit_init_clss_wl (add_clauses_to_subsumed_wl N S) = IsaSAT_Setup.get_unkept_unit_init_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_init_clss_wl (add_clauses_to_subsumed_wl N S) = IsaSAT_Setup.get_kept_unit_init_clss_wl S›
‹irred (get_clauses_wl S) N ⟹
get_subsumed_init_clauses_wl (add_clauses_to_subsumed_wl N S) = add_mset (mset (get_clauses_wl S ∝ N)) (get_subsumed_init_clauses_wl S)›
‹¬irred (get_clauses_wl S) N ⟹
get_subsumed_init_clauses_wl (add_clauses_to_subsumed_wl N S) = (get_subsumed_init_clauses_wl S)›
‹IsaSAT_Setup.get_unkept_unit_learned_clss_wl (add_clauses_to_subsumed_wl N S) = IsaSAT_Setup.get_unkept_unit_learned_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_learned_clss_wl (add_clauses_to_subsumed_wl N S) = IsaSAT_Setup.get_kept_unit_learned_clss_wl S›
‹irred (get_clauses_wl S) N ⟹
get_subsumed_learned_clauses_wl (add_clauses_to_subsumed_wl N S) = (get_subsumed_learned_clauses_wl S)›
‹¬irred (get_clauses_wl S) N ⟹ get_subsumed_learned_clauses_wl (add_clauses_to_subsumed_wl N S) = add_mset (mset (get_clauses_wl S ∝ N)) (get_subsumed_learned_clauses_wl S)›
‹literals_to_update_wl (add_clauses_to_subsumed_wl N S) = literals_to_update_wl S›
‹get_watched_wl (add_clauses_to_subsumed_wl N S) = get_watched_wl S›
‹get_clauses_wl (add_clauses_to_subsumed_wl N S) = get_clauses_wl S›
‹get_init_clauses0_wl (add_clauses_to_subsumed_wl N S) = get_init_clauses0_wl (S)›
‹get_learned_clauses0_wl (add_clauses_to_subsumed_wl N S) = get_learned_clauses0_wl (S)›
‹get_conflict_wl (add_clauses_to_subsumed_wl N S) = get_conflict_wl S›
apply (solves ‹cases S; auto simp: add_clauses_to_subsumed_wl_def›)+
done
lemma remove_lit_from_clause_st:
assumes
T: ‹(T, S) ∈ twl_st_heur_restart_occs' r u› and
LL': ‹(L,L')∈nat_lit_lit_rel› and
CC': ‹(C,C')∈nat_rel› and
C_dom: ‹C ∈# dom_m (get_clauses_wl S)› and
dist: ‹distinct (get_clauses_wl S ∝ C)›and
le: ‹length (get_clauses_wl S ∝ C) > 2›
shows
‹remove_lit_from_clause_st T C L
≤ SPEC (λc. (c, remove_lit_from_clause_wl C' L' S) ∈ {(U,V). (U,V)∈twl_st_heur_restart_occs' r u ∧ get_occs U = get_occs T ∧ get_aivdom U = get_aivdom T})›
proof -
define I where
‹I = (λ(i,j,N). dom_m N = dom_m (get_clauses_wl S) ∧
(∀D∈#dom_m (get_clauses_wl S). D ≠ C ⟶ fmlookup N D = fmlookup (get_clauses_wl S) D) ∧
(take i (N ∝ C) = (removeAll L (take j (get_clauses_wl S ∝ C')))) ∧
(∀k < length (N ∝ C). k ≥ j ⟶ (N ∝ C) !k = (get_clauses_wl S ∝ C') ! k) ∧
(length (N ∝ C) = length (get_clauses_wl S ∝ C')) ∧
irred N C = irred (get_clauses_wl S) C ∧
i ≤ j ∧ j ≤ length (get_clauses_wl S ∝ C'))›
define Φ where
‹Φ = (λ(i,j,N). dom_m N = dom_m (get_clauses_wl S) ∧
(∀D∈#dom_m (get_clauses_wl S). D ≠ C ⟶ fmlookup N D = fmlookup (get_clauses_wl S) D) ∧
j = length (get_clauses_wl S ∝ C') ∧
(take i (N ∝ C) = (removeAll L (get_clauses_wl S ∝ C'))) ∧
(length (N ∝ C) = length (get_clauses_wl S ∝ C')) ∧
irred N C = irred (get_clauses_wl S) C ∧ C' ∈# dom_m N ∧
i ≤ j ∧ j = length (get_clauses_wl S ∝ C'))›
have ge: ‹⇓Id (RETURN (remove_lit_from_clause_wl C' L' S)) ≥ do {
let n = length (get_clauses_wl S ∝ C');
(i, j, N) ← WHILE⇩T (λ(i, j, N). j < n)
(λ(i, j, N). do {
ASSERT (i < n);
ASSERT (j < n);
K ← mop_clauses_at N C j;
if K ≠ L then do {
N ← mop_clauses_swap N C i j;
RETURN (i+1, j+1, N)}
else RETURN (i, j+1, N)
}) (0, 0, get_clauses_wl S);
ASSERT (C' ∈# dom_m N);
ASSERT (i ≤ length (N ∝ C'));
ASSERT (i ≥ 2);
let N = N(C' ↪ take i (N ∝ C'));
ASSERT (N = (get_clauses_wl S)(C' ↪ removeAll L (get_clauses_wl S ∝ C')));
let N = N;
RETURN (set_clauses_wl N (add_clause_to_subsumed (irred (get_clauses_wl S) C') (mset (get_clauses_wl S ∝ C')) S))
}›
unfolding Let_def
apply (refine_vcg)
apply (rule WHILET_rule[where I= ‹I› and R = ‹measure (λ(i,j,N). length (get_clauses_wl S ∝ C') - j)› and Φ=Φ, THEN order_trans])
subgoal by auto
subgoal using CC' unfolding I_def by auto
subgoal
unfolding mop_clauses_at_def nres_monad3 mop_clauses_swap_def
apply (refine_vcg)
subgoal using C_dom by (auto simp: I_def)
subgoal using CC' by (auto simp: I_def)
subgoal using CC' C_dom by (auto simp: I_def)
subgoal using CC' by (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
subgoal using CC' by (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
subgoal unfolding I_def prod.simps apply (intro conjI)
subgoal using CC' by (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
subgoal using CC' by (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
subgoal
using CC' apply (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
by (metis order_mono_setup.refl take_update take_update_cancel)+
subgoal using CC' by (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
subgoal using CC' by (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
subgoal using CC' by (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
subgoal using CC' by (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
subgoal using CC' by (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
done
subgoal by (auto simp: I_def)
subgoal by (auto simp: I_def swap_only_first_relevant take_Suc_conv_app_nth)
subgoal by (auto simp: I_def)
done
subgoal using C_dom CC' unfolding Φ_def I_def by auto
subgoal using dist CC' LL' le
unfolding Φ_def by (cases S) (auto 4 4 simp: remove_lit_from_clause_wl_def distinct_remove1_removeAll
fmap_eq_iff_dom_m_lookup count_list_distinct_If length_removeAll_count_list
intro!: ASSERT_leI dest: arg_cong[of ‹take _ _› _ length])
done
have valid: ‹valid_arena (get_clauses_wl_heur T) (get_clauses_wl S) (set (get_vdom T))› and
corr: ‹clss_size_corr_restart (get_clauses_wl S)
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S) {#} (IsaSAT_Setup.get_kept_unit_init_clss_wl S)
(IsaSAT_Setup.get_kept_unit_learned_clss_wl S)
(get_subsumed_init_clauses_wl S)
{#} (get_init_clauses0_wl S) {#} (get_learned_count T)›
using T unfolding twl_st_heur_restart_occs_def by fast+
have [refine]: ‹((0, 0, get_clauses_wl_heur T), 0, 0, get_clauses_wl S) ∈ nat_rel ×⇩r nat_rel ×⇩r {(N,N'). valid_arena N N' (set (get_vdom T)) ∧ length N = length (get_clauses_wl_heur T)}›
using valid by auto
have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x
by auto
have H': ‹A = B ⟹ A x ⟹ B x› for A B x
by auto
note cong = trail_pol_cong heuristic_rel_cong
option_lookup_clause_rel_cong isa_vmtf_cong
vdom_m_cong[THEN H] isasat_input_nempty_cong[THEN iffD1]
isasat_input_bounded_cong[THEN iffD1]
cach_refinement_empty_cong[THEN H']
phase_saving_cong[THEN H']
ℒ⇩a⇩l⇩l_cong[THEN H]
D⇩0_cong[THEN H]
map_fun_rel_D⇩0_cong
vdom_m_cong[symmetric] ℒ⇩a⇩l⇩l_cong isasat_input_nempty_cong
have mset_removeAll_subseteq: ‹mset (removeAll L M) ⊆# mset M› for L M
by (subst mset_removeAll[symmetric]) (rule diff_subset_eq_self)
have [simp]: ‹ C' ∈# dom_m b ⟹ irred b C' ⟹
set_mset (all_lits_of_mm
(add_mset (mset (removeAll L (b ∝ C')))
({#mset (fst x). x ∈# init_clss_l b#} + dj))) =
set_mset (all_lits_of_mm
({#mset (fst x). x ∈# init_clss_l b#} + dj))› for b dj i
using all_lits_of_m_mono[of ‹mset (removeAll L (b ∝ C'))› ‹mset (b ∝ C')›]
by (auto simp: all_lits_of_mm_add_mset ran_m_def mset_take_subseteq mset_removeAll_subseteq
dest!: multi_member_split[of C'])
have ‹set_mset (all_init_atms_st (set_clauses_wl ((get_clauses_wl S)(C' ↪ removeAll L (get_clauses_wl S ∝ C')))
(add_clause_to_subsumed (irred (get_clauses_wl S) C') (mset (get_clauses_wl S ∝ C')) S))) =
set_mset (all_init_atms_st S)› for i
using C_dom CC'
by (cases S)
(auto simp: all_init_atms_st_def simp del: all_init_atms_def[symmetric]
simp: all_init_lits_def all_init_atms_def init_clss_l_fmdrop_if init_clss_l_mapsto_upd init_clss_l_clause_upd
image_mset_remove1_mset_if add_mset_commute[of _ ‹mset (removeAll _ _)›] init_clss_l_mapsto_upd_irrel)
note cong1 = cong[OF this(1)[symmetric]]
have [simp]: ‹clss_size_corr_restart ((get_clauses_wl S)(C' ↪ removeAll L (get_clauses_wl S ∝ C')))
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S) {#} (IsaSAT_Setup.get_kept_unit_init_clss_wl S)
(IsaSAT_Setup.get_kept_unit_learned_clss_wl S)
(get_subsumed_init_clauses_wl
(add_clause_to_subsumed (irred (get_clauses_wl S) C') (mset (get_clauses_wl S ∝ C')) S))
{#} (get_init_clauses0_wl S) {#} (get_learned_count T)›
using C_dom CC' corr by (auto simp: clss_size_corr_restart_def clss_size_def)
have[simp]:
‹vdom_m (all_init_atms_st S) (get_watched_wl S) ((get_clauses_wl S)(C' ↪ removeAll L (get_clauses_wl S ∝ C'))) =
vdom_m (all_init_atms_st S) (get_watched_wl S) ((get_clauses_wl S))›
using C_dom CC' by (auto simp: vdom_m_def)
have still_in_dom_after_shortening: ‹C' ∈# dom_m x2c ⟹
x1b ≤ length (x2c ∝ C') ⟹
TIER_ONE_MAXIMUM ≤ x1b ⟹
(xb, x2c(C' ↪ take x1b (x2c ∝ C')))
∈ {(N⇩1, N⇩1'). valid_arena N⇩1 N⇩1' (set (get_vdom T)) ∧ length N⇩1 = length x2a} ⟹
C ∈# dom_m (x2c(C' ↪ take x1b (x2c ∝ C')))›for x1b x2c xb x2a
using CC' by auto
have H: ‹(xb, x2c(C' ↪ take x1b (x2c ∝ C')))
∈ {(N⇩1, N⇩1'). valid_arena N⇩1 N⇩1' (set (get_vdom T)) ∧ length N⇩1 = length x2a} ⟹
(xc, x2c(C' ↪ take x1b (x2c ∝ C')))
∈ {(c, N').
N' = x2c(C' ↪ take x1b (x2c ∝ C')) ∧
valid_arena c (x2c(C' ↪ take x1b (x2c ∝ C'))) (set (get_vdom T)) ∧
length c = length xb} ⟹
(xc, x2c(C' ↪ take x1b (x2c ∝ C'))) ∈ {(c, N').
N' = x2c(C' ↪ take x1b (x2c ∝ C')) ∧
valid_arena c (x2c(C' ↪ take x1b (x2c ∝ C'))) (set (get_vdom T)) ∧
length c = length x2a}›for x1b xb x2a xc x2c
by auto
show ?thesis
unfolding conc_fun_RETURN[symmetric]
apply (rule ref_two_step)
defer apply (rule ge[unfolded Down_id_eq])
unfolding remove_lit_from_clause_st_def remove_lit_from_clause_def nres_monad3
apply (refine_vcg mop_arena_length[of ‹set (get_vdom T)›, THEN fref_to_Down_curry, unfolded comp_def]
mop_arena_lit2[of _ _ ‹set (get_vdom T)›] mop_arena_swap2[of _ _ ‹set (get_vdom T)›]
mop_arena_shorten[of _ _ _ _ _ C C'] update_lbd_shrunk_clause_valid[of _ _ _ ‹set (get_vdom T)›])
subgoal using C_dom CC' by auto
subgoal using CC' valid by auto
subgoal using CC' C_dom 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
subgoal by auto
subgoal by auto
subgoal by auto
apply (solves auto)[]
apply (solves auto)[]
subgoal using CC' by auto
subgoal using CC' by auto
subgoal by auto
subgoal using CC' by auto
apply (rule still_in_dom_after_shortening; assumption)
subgoal by auto
apply (rule H; assumption)
subgoal using T CC' C_dom
by (clarsimp simp add: twl_st_heur_restart_occs_def cong1 IsaSAT_Restart.all_init_atms_alt_def
simp del: isasat_input_nempty_def)
done
qed
lemma add_clauses_to_subsumed_wl_twl_st_heur_restart_occs:
assumes ‹(S, T) ∈ twl_st_heur_restart_occs' r u› and
D: ‹D ∈# dom_m (get_clauses_wl T)›
shows ‹(S, add_clauses_to_subsumed_wl D T) ∈ {(U,V). (U,V)∈twl_st_heur_restart_occs' r u ∧ get_occs U = get_occs S ∧ get_aivdom U = get_aivdom S}›
proof -
have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x
by auto
have H': ‹A = B ⟹ A x ⟹ B x› for A B x
by auto
note cong = trail_pol_cong heuristic_rel_cong
option_lookup_clause_rel_cong isa_vmtf_cong
vdom_m_cong[THEN H] isasat_input_nempty_cong[THEN iffD1]
isasat_input_bounded_cong[THEN iffD1]
cach_refinement_empty_cong[THEN H']
phase_saving_cong[THEN H']
ℒ⇩a⇩l⇩l_cong[THEN H]
D⇩0_cong[THEN H]
map_fun_rel_D⇩0_cong
vdom_m_cong[symmetric] ℒ⇩a⇩l⇩l_cong isasat_input_nempty_cong
have ‹set_mset (all_init_atms_st (add_clauses_to_subsumed_wl D T)) =
set_mset (all_init_atms_st T)›
using D by (cases T)
(auto simp: all_init_atms_st_def add_clauses_to_subsumed_wl_def all_init_atms_def
all_init_lits_def ran_m_def all_lits_of_mm_add_mset
dest!: multi_member_split[of ‹_ :: nat›]
simp del: all_init_atms_def[symmetric])
note cong1 = cong[OF this[symmetric]]
show ?thesis
using assms
unfolding twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def
by (cases ‹irred (get_clauses_wl T) D›)
(clarsimp_all simp add: cong1 simp del: isasat_input_bounded_def isasat_input_nempty_def)
qed
lemma mark_garbage_wl_no_learned_reset_simp[simp]:
‹get_trail_wl (mark_garbage_wl_no_learned_reset C S) = get_trail_wl S›
‹IsaSAT_Setup.get_unkept_unit_init_clss_wl (mark_garbage_wl_no_learned_reset C S) = IsaSAT_Setup.get_unkept_unit_init_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_init_clss_wl (mark_garbage_wl_no_learned_reset C S) = IsaSAT_Setup.get_kept_unit_init_clss_wl S›
‹get_subsumed_init_clauses_wl (mark_garbage_wl_no_learned_reset C S) = (get_subsumed_init_clauses_wl S)›
‹IsaSAT_Setup.get_unkept_unit_learned_clss_wl (mark_garbage_wl_no_learned_reset C S) = IsaSAT_Setup.get_unkept_unit_learned_clss_wl S›
‹IsaSAT_Setup.get_kept_unit_learned_clss_wl (mark_garbage_wl_no_learned_reset C S) = IsaSAT_Setup.get_kept_unit_learned_clss_wl S›
‹get_subsumed_learned_clauses_wl (mark_garbage_wl_no_learned_reset C S) = (get_subsumed_learned_clauses_wl S)›
‹literals_to_update_wl (mark_garbage_wl_no_learned_reset C S) = literals_to_update_wl S›
‹get_watched_wl (mark_garbage_wl_no_learned_reset C S) = get_watched_wl S›
‹get_clauses_wl (mark_garbage_wl_no_learned_reset C S) = fmdrop C (get_clauses_wl S)›
‹get_init_clauses0_wl (mark_garbage_wl_no_learned_reset C S) = get_init_clauses0_wl (S)›
‹get_learned_clauses0_wl (mark_garbage_wl_no_learned_reset C S) = get_learned_clauses0_wl (S)›
‹get_conflict_wl (mark_garbage_wl_no_learned_reset C S) = get_conflict_wl S›
apply (solves ‹cases S; auto simp: mark_garbage_wl_no_learned_reset_def›)+
done
lemma [simp]: ‹get_occs (incr_wasted_st b S) = get_occs S›
‹learned_clss_count (incr_wasted_st b S) = learned_clss_count S›
by (auto simp: incr_wasted_st_def)
lemma log_clause_heur_log_clause2_occs:
assumes ‹(S,T) ∈ twl_st_heur_restart_occs' r u› ‹(C,C') ∈ nat_rel›
shows ‹log_clause_heur S C ≤⇓unit_rel (log_clause2 T C')›
proof -
have [refine0]: ‹(0,0)∈nat_rel›
by auto
have length: ‹⇓ nat_rel ((RETURN ∘ (λc. length (get_clauses_wl T ∝ c))) C') ≤ SPEC (λc. (c, length (get_clauses_wl T ∝ C')) ∈ {(a,b). a=b ∧ a = length (get_clauses_wl T ∝ C)})›
by (use assms in auto)
show ?thesis
unfolding log_clause_heur_def log_clause2_def comp_def uncurry_def mop_arena_length_st_def
mop_access_lit_in_clauses_heur_def
apply (refine_vcg mop_arena_lit[where vdom = ‹set (get_vdom S)› and N = ‹get_clauses_wl T›, THEN order_trans]
mop_arena_length[where vdom = ‹set (get_vdom S)›, THEN fref_to_Down_curry, THEN order_trans, unfolded prod.simps])
apply assumption
subgoal using assms by (auto simp: twl_st_heur_restart_occs_def twl_st_heur_restart_def)
apply (rule length)
subgoal by (use assms in ‹auto simp: twl_st_heur_restart_occs_def twl_st_heur_restart_def dest: arena_lifting(10)›)
subgoal by auto
subgoal using assms by (auto simp: twl_st_heur_restart_occs_def twl_st_heur_restart_def)
apply assumption
subgoal by (use assms in auto)
apply (rule refl)
subgoal by auto
by auto
qed
lemma log_del_clause_heur_log_clause:
assumes ‹(S,T) ∈ twl_st_heur_restart_occs' r u› ‹(C,C') ∈ nat_rel› ‹C ∈# dom_m (get_clauses_wl T)›
shows ‹log_del_clause_heur S C ≤ SPEC (λc. (c, log_clause T C') ∈ unit_rel)›
unfolding log_del_clause_heur_alt_def
apply (rule log_clause_heur_log_clause2_occs[THEN order_trans, OF assms(1,2)])
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule log_clause2_log_clause[THEN fref_to_Down_curry])
using assms by auto
lemma mark_garbage_heur_as_subsumed:
assumes
T: ‹(S,T)∈ twl_st_heur_restart_occs' r u› and
D: ‹C ∈# dom_m (get_clauses_wl T)› and
‹(C',C)∈nat_rel› and
eq: ‹set_mset (all_init_atms_st (mark_garbage_wl_no_learned_reset C' T)) = set_mset (all_init_atms_st T)›
shows ‹mark_garbage_heur_as_subsumed C S ≤ SPEC (λc. (c, mark_garbage_wl_no_learned_reset C' T) ∈ {(U,V). (U,V)∈twl_st_heur_restart_occs' r u ∧ get_occs U = get_occs S ∧ get_aivdom U = get_aivdom S})›
proof -
have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x
by auto
have H': ‹A = B ⟹ A x ⟹ B x› for A B x
by auto
note cong = trail_pol_cong heuristic_rel_cong
option_lookup_clause_rel_cong isa_vmtf_cong
vdom_m_cong[THEN H] isasat_input_nempty_cong[THEN iffD1]
isasat_input_bounded_cong[THEN iffD1]
cach_refinement_empty_cong[THEN H']
phase_saving_cong[THEN H']
ℒ⇩a⇩l⇩l_cong[THEN H]
D⇩0_cong[THEN H]
map_fun_rel_D⇩0_cong
vdom_m_cong[symmetric] ℒ⇩a⇩l⇩l_cong isasat_input_nempty_cong
heuristic_rel_cong
have CC': ‹C' = C›
using assms by auto
note cong1 = cong[OF eq[unfolded CC', symmetric]]
have valid: ‹valid_occs (get_occs S) (get_aivdom S)› and
arena: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl T) (set (get_vdom S))›
using T by (auto simp: twl_st_heur_restart_occs_def)
have pre: ‹arena_is_valid_clause_idx (get_clauses_wl_heur S) C›
unfolding arena_is_valid_clause_idx_def
by (use T arena D in ‹auto simp: arena_is_valid_clause_idx_and_access_def intro!: exI[of _ ‹get_clauses_wl T›] exI[of _ ‹set (get_vdom S)›]›)
show ?thesis
using pre
unfolding twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def
mark_garbage_heur_as_subsumed_def mop_arena_length_def nres_monad3
apply (refine_vcg log_del_clause_heur_log_clause[where r=r and u=u and C'=C, THEN order_trans] T)
subgoal
using arena D unfolding arena_is_valid_clause_vdom_def by auto
subgoal by simp
subgoal using arena D by simp
subgoal using arena D unfolding mark_garbage_pre_def by simp
subgoal
using arena red_in_dom_number_of_learned_ge1[of C ‹get_clauses_wl T›] assms assms
red_in_dom_number_of_learned_ge1_twl_st_heur_restart_occs[of S T r u C]
by (cases ‹arena_status (get_clauses_wl_heur S) C›)
(auto simp add: arena_lifting)
subgoal
using assms pre
unfolding twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def
mark_garbage_heur_as_subsumed_def mop_arena_length_def nres_monad3
apply (clarsimp_all simp add: cong1 valid_arena_extra_information_mark_to_delete'
aivdom_inv_dec_remove_clause arena_lifting
simp del: isasat_input_bounded_def isasat_input_nempty_def
simp flip: learned_clss_count_def
)
apply (intro conjI impI)
subgoal
by (auto dest: in_vdom_m_fmdropD simp add: incr_wasted_st_def cong1 intro!: heuristic_relI)
subgoal
by (auto simp add: incr_wasted_st_def cong1 intro!: heuristic_relI)
subgoal
by (auto simp add: incr_wasted_st_def cong1 intro!: heuristic_relI)
subgoal
by (auto dest: in_vdom_m_fmdropD simp add: incr_wasted_st_def cong1 intro!: heuristic_relI)
subgoal
by (auto simp add: incr_wasted_st_def cong1 intro!: heuristic_relI)
subgoal
by (auto simp flip: learned_clss_count_def simp add: incr_wasted_st_def cong1 intro!: heuristic_relI)
done
done
qed
lemma twl_st_heur_restart_occs'_with_occs:
‹a∈{(U,V). (U,V)∈twl_st_heur_restart_occs' r u ∧ get_occs U = get_occs T ∧ get_aivdom U = get_aivdom S} ⟹
a ∈ twl_st_heur_restart_occs' r u›
by auto
lemma isa_strengthen_clause_wl2:
assumes
T: ‹(T, S) ∈ twl_st_heur_restart_occs' r u› and
CC': ‹(C,C')∈nat_rel›and
DD': ‹(D,D')∈nat_rel› and
LL': ‹(L,L')∈nat_lit_lit_rel›
shows ‹isa_strengthen_clause_wl2 C D L T
≤ ⇓ {(U,V). (U,V)∈twl_st_heur_restart_occs' r u ∧ get_occs U = get_occs T ∧ get_aivdom U = get_aivdom T}
(strengthen_clause_wl C' D' L' S)›
proof -
have arena: ‹((get_clauses_wl_heur T, C), get_clauses_wl S, C')
∈ {(N, N'). valid_arena N N' (set (get_vdom T))} ×⇩f nat_rel›
‹((get_clauses_wl_heur T, D), get_clauses_wl S, D')
∈ {(N, N'). valid_arena N N' (set (get_vdom T))} ×⇩f nat_rel›
using T CC' DD' unfolding twl_st_heur_restart_occs_def
by auto
have C': ‹C' ∈# dom_m (get_clauses_wl S)› and D': ‹D' ∈# dom_m (get_clauses_wl S)› and
C'_in_dom: ‹(get_clauses_wl S, C') = (x1, x2) ⟹ x2 ∈# dom_m x1› and
D'_in_dom: ‹(get_clauses_wl S, D') = (x1, x2) ⟹ x2 ∈# dom_m x1› and
C'_vdom: ‹C' ∈ set (get_vdom T)› and
D'_vdom: ‹D' ∈ set (get_vdom T)› and
C'_dist: ‹distinct (get_clauses_wl S ∝ C')› and
le2: ‹2 < length (get_clauses_wl S ∝ C')›
if pre: ‹subsume_or_strengthen_wl_pre C' (STRENGTHENED_BY L' D') S›
for x1 x2
proof -
show C': ‹C' ∈# dom_m (get_clauses_wl S)› and D': ‹D' ∈# dom_m (get_clauses_wl S)›
using pre unfolding subsume_or_strengthen_wl_pre_def subsume_or_strengthen_pre_def apply -
by (normalize_goal+; auto)+
then show ‹x2 ∈# dom_m x1› if ‹(get_clauses_wl S, C') = (x1, x2)›
using that by auto
show ‹x2 ∈# dom_m x1› if ‹(get_clauses_wl S, D') = (x1, x2)›
using D' that by auto
have
ai: ‹aivdom_inv_dec (get_aivdom T) (dom_m (get_clauses_wl S))›
using T unfolding twl_st_heur_restart_occs_def by auto
then have H: ‹C' ∈ set (get_vdom T)› if ‹C' ∈# dom_m (get_clauses_wl S)› for C'
using ai that
by (smt (verit, ccfv_threshold) UnE aivdom_inv_dec_alt_def2 in_multiset_in_set mset_subset_eqD subsetD)
show ‹C' ∈ set (get_vdom T)› and ‹D' ∈ set (get_vdom T)›
using H[OF C'] H[OF D'] CC' DD'
by auto
show ‹distinct (get_clauses_wl S ∝ C')› ‹2 < length (get_clauses_wl S ∝ C')›
using CC' pre unfolding subsume_or_strengthen_wl_pre_def subsume_or_strengthen_pre_def subsumption.simps apply -
by (solves ‹normalize_goal+; simp›)+
qed
have [refine]: ‹(Sa, U) ∈ {(U, V).
(U, V) ∈ twl_st_heur_restart_occs' r u ∧
get_occs U = get_occs T ∧ get_aivdom U = get_aivdom T} ⟹
(set_stats_wl_heur (incr_forward_strengethening (get_stats_heur Sa)) Sa, U)
∈ {(U, V).
(U, V) ∈ twl_st_heur_restart_occs' r u ∧
get_occs U = get_occs T ∧ get_aivdom U = get_aivdom T}› for Sa U
by (auto simp: twl_st_heur_restart_occs_def)
have H: ‹(x, y') ∈ R ⟹ y=y' ⟹ (x, y) ∈ R› for x y y' R
by auto
show ?thesis
unfolding isa_strengthen_clause_wl2_def
apply (rule ref_two_step[OF _ strengthen_clause_wl_alt_def])
unfolding if_False Let_def[of ‹remove1 _ _›]
log_new_clause_heur_alt_def
Let_def[of ‹mark_clause_for_unit_as_changed _›]
apply (refine_vcg mop_arena_length[of ‹set (get_vdom T)›, THEN fref_to_Down_curry, unfolded comp_def]
remove_lit_from_clause_st T mop_arena_status2[of _ _ ‹set (get_vdom T)›]
mop_arena_promote_st_spec[where r=r and u=u] mark_garbage_heur_as_subsumed)
subgoal by (rule C'_in_dom)
subgoal by (rule arena)
subgoal by (rule D'_in_dom)
subgoal by (rule arena)
subgoal using CC' by auto
subgoal using CC' C'_vdom by auto
subgoal using arena by auto
subgoal using DD' by auto
subgoal using DD' D'_vdom by auto
subgoal using arena by auto
subgoal using LL' by auto
subgoal using CC' by auto
subgoal using C' CC' by auto
subgoal using CC' C'_dist by fast
subgoal using CC' le2 by fast
apply (rule log_clause_heur_log_clause2_occs[where r=r and u=u])
subgoal by auto
subgoal using CC' by auto
subgoal by auto
apply (rule add_clauses_to_subsumed_wl_twl_st_heur_restart_occs[where r=r and u=u])
subgoal by simp
subgoal using DD' D' by auto
apply (rule twl_st_heur_restart_occs'_with_occs, assumption)
subgoal using CC' C' by auto
subgoal by auto
subgoal using DD' CC' C' D' arena by (clarsimp simp add: arena_lifting)
apply (rule H, assumption)
subgoal using DD' CC' by auto
subgoal using DD' CC' C' D' arena by (auto simp: arena_lifting)
apply (rule twl_st_heur_restart_occs'_with_occs, assumption)
subgoal using DD' D' by simp
subgoal using DD' by simp
subgoal premises p
using p(18,21) by simp
subgoal by simp
done
qed
lemma isa_subsume_or_strengthen_wl_subsume_or_strengthen_wl:
assumes
T: ‹(T, S) ∈ twl_st_heur_restart_occs' r u› and
x: ‹(x2a, x2) ∈ Id›
shows ‹isa_subsume_or_strengthen_wl C x2a T
≤ ⇓ {(U,V). (U,V)∈twl_st_heur_restart_occs' r u ∧ get_occs U = get_occs T ∧ get_aivdom U = get_aivdom T}
(subsume_or_strengthen_wl C x2 S)›
proof -
have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x
by auto
have H': ‹A = B ⟹ A x ⟹ B x› for A B x
by auto
note cong = trail_pol_cong heuristic_rel_cong
option_lookup_clause_rel_cong isa_vmtf_cong
vdom_m_cong[THEN H] isasat_input_nempty_cong[THEN iffD1]
isasat_input_bounded_cong[THEN iffD1]
cach_refinement_empty_cong[THEN H']
phase_saving_cong[THEN H']
ℒ⇩a⇩l⇩l_cong[THEN H]
D⇩0_cong[THEN H]
map_fun_rel_D⇩0_cong
vdom_m_cong[symmetric] ℒ⇩a⇩l⇩l_cong isasat_input_nempty_cong
have atms_eq[symmetric]: ‹C ∈# dom_m (get_clauses_wl S) ⟹
irred (get_clauses_wl S) C ⟹
set_mset (all_init_atms (fmdrop C (get_clauses_wl S))
(add_mset (mset (get_clauses_wl S ∝ C))
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S + IsaSAT_Setup.get_kept_unit_init_clss_wl S +
get_subsumed_init_clauses_wl S +
get_init_clauses0_wl S))) =
set_mset (all_init_atms (get_clauses_wl S)
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S + IsaSAT_Setup.get_kept_unit_init_clss_wl S +
get_subsumed_init_clauses_wl S +
get_init_clauses0_wl S))›
‹C ∈# dom_m (get_clauses_wl S) ⟹
¬irred (get_clauses_wl S) C ⟹
set_mset (all_init_atms (fmdrop C (get_clauses_wl S))
((IsaSAT_Setup.get_unkept_unit_init_clss_wl S + IsaSAT_Setup.get_kept_unit_init_clss_wl S +
get_subsumed_init_clauses_wl S +
get_init_clauses0_wl S))) =
set_mset (all_init_atms (get_clauses_wl S)
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S + IsaSAT_Setup.get_kept_unit_init_clss_wl S +
get_subsumed_init_clauses_wl S +
get_init_clauses0_wl S))›
by (simp_all add: all_init_atms_fmdrop_add_mset_unit)
note cong1 = cong[OF this(1)] cong[OF this(2)]
have H: ‹x2a = x2›
using x by auto
have C_vdom: ‹C ∈ set (get_vdom T)› and
C_dom: ‹C ∈# dom_m (get_clauses_wl S)› and
valid: ‹valid_arena (get_clauses_wl_heur T) (get_clauses_wl S) (set (get_vdom T))› and
C'_vdom: ‹x2 = SUBSUMED_BY C' ⟹ C' ∈ set (get_vdom T)› and
C'_dom: ‹x2 = SUBSUMED_BY C' ⟹ C' ∈# dom_m (get_clauses_wl S)› and
mark_garbage: ‹mark_garbage_heur2 C T
≤ SPEC (λc. (c, mark_garbage_wl2 C S) ∈ {(U,V). (U,V)∈twl_st_heur_restart_occs' r u ∧ get_occs U=get_occs T ∧ get_aivdom U = get_aivdom T})›
if ‹isa_subsume_or_strengthen_wl_pre C x2 T› and
pre2: ‹subsume_or_strengthen_wl_pre C x2 S›
for C'
proof -
show C: ‹C ∈# dom_m (get_clauses_wl S)›
using pre2 T unfolding isa_subsume_or_strengthen_wl_pre_def subsume_or_strengthen_wl_pre_def
subsume_or_strengthen_pre_def
apply - by normalize_goal+ simp
show valid: ‹valid_arena (get_clauses_wl_heur T) (get_clauses_wl S) (set (get_vdom T))›
using T unfolding twl_st_heur_restart_occs_def by auto
have
ai: ‹aivdom_inv_dec (get_aivdom T) (dom_m (get_clauses_wl S))›
using T unfolding twl_st_heur_restart_occs_def by auto
then have H: ‹C' ∈ set (get_vdom T)› if ‹C' ∈# dom_m (get_clauses_wl S)› for C'
using ai that
by (smt (verit, ccfv_threshold) UnE aivdom_inv_dec_alt_def2 in_multiset_in_set mset_subset_eqD subsetD)
show ‹C ∈ set (get_vdom T)›
by (rule H[OF C])
have [simp]: ‹(all_init_atms (fmdrop C (get_clauses_wl S))
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S +
IsaSAT_Setup.get_kept_unit_init_clss_wl S +
get_subsumed_init_clauses_wl (mark_garbage_wl2 C S) +
get_init_clauses0_wl S)) =
(all_init_atms ((get_clauses_wl S))
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S +
IsaSAT_Setup.get_kept_unit_init_clss_wl S +
get_subsumed_init_clauses_wl (S) +
get_init_clauses0_wl (mark_garbage_wl2 C S)))›
by (cases ‹irred (get_clauses_wl S) C›)
(use C in ‹auto simp: all_init_atms_def all_init_lits_def image_mset_remove1_mset_if
simp del: all_init_atms_def[symmetric]›)
have [simp]: ‹valid_arena (extra_information_mark_to_delete (get_clauses_wl_heur T) C)
(fmdrop C (get_clauses_wl S)) (set (get_vdom T))›
using valid C valid_arena_extra_information_mark_to_delete' by presburger
have [simp]: ‹arena_status (get_clauses_wl_heur T) C = IRRED ⟹
clss_size_corr_restart ((get_clauses_wl S))
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S) {#}
(IsaSAT_Setup.get_kept_unit_init_clss_wl S)
(IsaSAT_Setup.get_kept_unit_learned_clss_wl S)
(get_subsumed_init_clauses_wl (S)) {#}
(get_init_clauses0_wl S) {#} (get_learned_count T) ⟹
clss_size_corr_restart (fmdrop C (get_clauses_wl S))
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S) {#}
(IsaSAT_Setup.get_kept_unit_init_clss_wl S)
(IsaSAT_Setup.get_kept_unit_learned_clss_wl S)
(get_subsumed_init_clauses_wl (mark_garbage_wl2 C S)) {#}
(get_init_clauses0_wl S) {#} (get_learned_count T)›
‹arena_status (get_clauses_wl_heur T) C ≠ IRRED ⟹
clss_size_corr_restart ((get_clauses_wl S))
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S) {#}
(IsaSAT_Setup.get_kept_unit_init_clss_wl S)
(IsaSAT_Setup.get_kept_unit_learned_clss_wl S)
(get_subsumed_init_clauses_wl (S)) {#}
(get_init_clauses0_wl S) {#} (get_learned_count T) ⟹
clss_size_corr_restart (fmdrop C (get_clauses_wl S))
(IsaSAT_Setup.get_unkept_unit_init_clss_wl S) {#}
(IsaSAT_Setup.get_kept_unit_init_clss_wl S)
(IsaSAT_Setup.get_kept_unit_learned_clss_wl S)
(get_subsumed_init_clauses_wl (mark_garbage_wl2 C S)) {#}
(get_init_clauses0_wl S) {#} (clss_size_decr_lcount (get_learned_count T))›
using C arena_lifting(24)[OF valid C] by (auto simp add: clss_size_corr_restart_def clss_size_def
clss_size_decr_lcount_def size_remove1_mset_If split: prod.splits)
show ‹mark_garbage_heur2 C T ≤ SPEC(λc. (c, mark_garbage_wl2 C S) ∈ {(U,V). (U,V)∈twl_st_heur_restart_occs' r u ∧ get_occs U=get_occs T ∧ get_aivdom U = get_aivdom T})›
unfolding mark_garbage_heur2_def nres_monad3
apply refine_vcg
subgoal
using T C unfolding mark_garbage_pre_def arena_is_valid_clause_idx_def
by (auto simp add: twl_st_heur_restart_occs_def aivdom_inv_dec_remove_clause cong1
valid_arena_extra_information_mark_to_delete' arena_lifting clss_size_corr_restart_intro
simp flip: learned_clss_count_def learned_clss_count_def
simp del: isasat_input_nempty_def
dest: in_vdom_m_fmdropD)
subgoal by (rule red_in_dom_number_of_learned_ge1_twl_st_heur_restart_occs[OF T C])
subgoal
using T
by (auto simp add: twl_st_heur_restart_occs_def aivdom_inv_dec_remove_clause cong1
valid_arena_extra_information_mark_to_delete' arena_lifting clss_size_corr_restart_intro
simp flip: learned_clss_count_def learned_clss_count_def
simp del: isasat_input_nempty_def
dest: in_vdom_m_fmdropD)
done
assume ‹x2 = SUBSUMED_BY C'›
then show C': ‹C' ∈# dom_m (get_clauses_wl S)›
using pre2 T unfolding isa_subsume_or_strengthen_wl_pre_def subsume_or_strengthen_wl_pre_def
subsume_or_strengthen_pre_def
apply - by normalize_goal+ simp
show ‹C' ∈ set (get_vdom T)›
by (rule H[OF C'])
qed
have [refine, intro!]: ‹(Sa, U) ∈ {(U, V).
(U, V) ∈ twl_st_heur_restart_occs' r u ∧
get_occs U = get_occs T ∧ get_aivdom U = get_aivdom T} ⟹
(set_stats_wl_heur (incr_forward_subsumed (get_stats_heur Sa)) Sa, U)
∈ {(U, V).
(U, V) ∈ twl_st_heur_restart_occs' r u ∧
get_occs U = get_occs T ∧ get_aivdom U = get_aivdom T}› for Sa U
by (auto simp: twl_st_heur_restart_occs_def)
show ?thesis
apply (rule order_trans)
defer
apply (rule ref_two_step'[OF subsume_or_strengthen_wl_alt_def])
unfolding isa_subsume_or_strengthen_wl_def Let_def[of ‹If _ _ _›] Let_def[of ‹log_clause _ _›]
case_wl_split state_wl_recompose H
apply (refine_vcg subsumption_cases_lhs mop_arena_status2[where vdom = ‹set (get_vdom T)›]
mark_garbage mop_arena_promote_st_spec[where T=‹mark_garbage_wl2 C S› and r=r and u=u]
isa_strengthen_clause_wl2[where r=r and u=u]
log_del_clause_heur_log_clause[where r=r and u=u and T=S and C'=C] T)
subgoal using T unfolding isa_subsume_or_strengthen_wl_pre_def by fast
subgoal by auto
subgoal by auto
subgoal by (rule C_vdom)
subgoal by (rule valid)
subgoal by auto
subgoal by (rule C'_vdom)
subgoal by (rule valid)
subgoal by auto
subgoal using C'_dom C_dom by auto
subgoal by auto
subgoal by auto
subgoal using valid C'_dom C_dom by (auto simp add: arena_lifting)
subgoal using valid C'_dom C_dom by (auto simp add: arena_lifting)
subgoal using valid C'_dom C_dom by (auto simp add: arena_lifting)
subgoal using valid C'_dom C_dom by (auto simp add: arena_lifting)
subgoal by auto
subgoal using T by auto
done
qed
lemma isa_forward_subsumption_one_forward_subsumption_wl_one:
assumes
SS': ‹(S, S') ∈ twl_st_heur_restart_occs' r u› and
CC': ‹(C,C')∈nat_rel› and
DD': ‹(D,D')∈clause_hash› and
‹(L,L')∈Id› and
occs: ‹(get_occs S, occs) ∈ occurrence_list_ref›
shows ‹isa_forward_subsumption_one_wl C D L S ≤
⇓{((U, changed, E), (S', changed', occs', E')). (get_occs U, occs') ∈ occurrence_list_ref ∧
get_aivdom U = get_aivdom S ∧ changed' = (changed ≠ NONE) ∧
((U, E), (S', E')) ∈ twl_st_heur_restart_occs' r u ×⇩r clause_hash}
(forward_subsumption_one_wl2 C' cands L' occs D' S')›
proof -
have valid: ‹valid_occs (get_occs S) (get_aivdom S)› and
dom_m_incl: ‹set_mset (dom_m (get_clauses_wl S')) ⊆ set (get_vdom S)›
using SS' by (auto simp: twl_st_heur_restart_occs_def vdom_m_def)
have C_vdom: ‹C ∈set (get_vdom S)›
if ‹forward_subsumption_one_wl2_pre C cands L S'›
proof -
have ‹C ∈# dom_m (get_clauses_wl S')›
using that unfolding forward_subsumption_one_wl2_pre_def forward_subsumption_one_wl_pre_def
forward_subsumption_one_pre_def by - (normalize_goal+; simp)
then show ?thesis
using dom_m_incl by fast
qed
have lits: ‹literals_are_in_ℒ⇩i⇩n (all_init_atms_st S') (mset (get_clauses_wl S' ∝ C))› and
dist: ‹distinct_mset (mset (get_clauses_wl S' ∝ C))› and
tauto: ‹¬ tautology (mset (get_clauses_wl S' ∝ C))›
if ‹forward_subsumption_one_wl2_pre C' cands L' S'›
using that CC' unfolding forward_subsumption_one_wl2_pre_def forward_subsumption_one_wl_pre_def
forward_subsumption_one_pre_def
apply -
subgoal
apply normalize_goal+
apply (frule literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def)
apply (rule literals_are_in_ℒ⇩i⇩n_nth)
apply (simp add: literals_are_ℒ⇩i⇩n_def literals_are_ℒ⇩i⇩n'_def)
apply (simp add: literals_are_in_ℒ⇩i⇩n_nth literals_are_ℒ⇩i⇩n_cong
literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff)
done
subgoal
apply normalize_goal+
unfolding twl_struct_invs_def twl_st_inv_alt_def
by (simp add:mset_take_mset_drop_mset')
subgoal
apply normalize_goal+
unfolding twl_list_invs_def
by (simp add:mset_take_mset_drop_mset')
done
have forward_subsumption_one_wl2_alt_def:
‹forward_subsumption_one_wl2 = (λC cands L occs D S. do {
ASSERT (forward_subsumption_one_wl2_pre C cands L S);
ASSERT (atm_of L ∈ fst occs);
let ys = occ_list occs L;
let n = length ys;
(_, s) ←
WHILE⇩T⇗ forward_subsumption_one_wl2_inv S C cands ys ⇖ (λ(i, s). i < n ∧ s = NONE)
(λ(i, s). do {
C' ← mop_occ_list_at occs L i;
b ← RETURN (C' ∈# dom_m (get_clauses_wl S));
if ¬b
then RETURN (i+1, s)
else do {
s ← subsume_clauses_match2 C' C S D;
RETURN (i+1, s)
}
})
(0, NONE);
D ← (if s ≠ NONE then mop_ch_remove_all (mset (get_clauses_wl S ∝ C)) D else RETURN D);
occs ← (if is_strengthened s then maybe_push_to_occs_list2 C S occs else RETURN occs);
S ← subsume_or_strengthen_wl C s S;
RETURN (S, s ≠ NONE, occs, D)
})›
unfolding forward_subsumption_one_wl2_def by auto
have eq: ‹L' = L› ‹C' = C›
using assms by auto
have [refine]: ‹((0, NONE), 0, NONE) ∈ nat_rel ×⇩r Id›
by auto
have H[simp]: ‹forward_subsumption_one_wl2_pre C cands L S' ⟹ atm_of L ∈ fst occs ⟹
(occ_list occs L) = (get_occs S ! nat_of_lit L)›
using occs
by (cases L)
(auto simp: forward_subsumption_one_wl2_pre_def occ_list_def occurrence_list_ref_def map_fun_rel_def
dest: bspec[of _ _ L])
show ?thesis
unfolding isa_forward_subsumption_one_wl_def forward_subsumption_one_wl2_alt_def eq Let_def mop_cocc_list_length_def nres_monad3
cocc_list_length_def
bind_to_let_conv[of ‹length (get_occs _ ! _)›]
apply (refine_vcg mop_cocc_list_at_mop_occ_list_at occs mop_arena_status2[where arena=‹get_clauses_wl_heur S› and vdom=‹set (get_vdom S)› and
N=‹get_clauses_wl S'›] isa_subsume_clauses_match2_subsume_clauses_match2 SS' mop_cch_remove_all_clauses_mop_ch_remove_all_clauses CC' DD'
isa_maybe_push_to_occs_list_st_push_to_occs_list2
isa_subsume_or_strengthen_wl_subsume_or_strengthen_wl[where r=r and u=u])
subgoal using assms unfolding isa_forward_subsumption_one_wl_pre_def by fast
subgoal using occs by (cases L) (auto simp: occurrence_list_ref_def map_fun_rel_def dest: bspec[of _ _ ‹L›])
subgoal by (auto simp: cocc_list_length_pre_def)
subgoal using assms H unfolding isa_forward_subsumption_one_wl2_inv_def apply - by (rule exI[of _ S']) auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using valid occs by (auto simp: forward_subsumption_one_wl2_pre_def occurrence_list_ref_def all_init_atms_st_alt_def
all_occurrences_add_mset2 intro: valid_occs_in_vdomI)
subgoal using SS' by (auto simp: twl_st_heur_restart_occs_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using DD' by auto
subgoal by auto
subgoal by auto
subgoal unfolding forward_subsumption_one_wl2_pre_def forward_subsumption_one_wl_pre_def
forward_subsumption_one_pre_def
by normalize_goal+ auto
subgoal by auto
subgoal by auto
subgoal using C_vdom by fast
subgoal
using assms(1,2,3,4) simple_clss_size_upper_div2[of ‹all_init_atms_st S'› ‹mset (get_clauses_wl S' ∝ C)›, OF _ lits dist tauto]
by (auto simp del: isasat_input_bounded_def simp: clause_not_marked_to_delete_def
simp: twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def)
subgoal using SS' occs by auto
subgoal by auto
subgoal by auto
subgoal by (auto 4 3 simp: forward_subsumption_one_wl2_pre_def isa_forward_subsumption_one_wl_pre_def
forward_subsumption_one_wl_pre_def)
done
qed
lemma isa_try_to_forward_subsume_wl2_try_to_forward_subsume_wl2:
assumes
SS': ‹(S, S') ∈ twl_st_heur_restart_occs' r u› and
CC': ‹(C,C')∈nat_rel› and
DD': ‹(D,D')∈clause_hash› and
occs: ‹(get_occs S, occs) ∈ occurrence_list_ref› and
shrunken: ‹shrunken = mset shrunken'› and
cands: ‹Suc (length shrunken') ≤ length (get_tvdom S)›
shows ‹isa_try_to_forward_subsume_wl2 C D shrunken' S ≤
⇓{((D, shrunken, U), (occs, D', shrunken', S')). (D,D')∈clause_hash ∧ (get_occs U, occs) ∈ occurrence_list_ref ∧
(U, S') ∈ twl_st_heur_restart_occs' r u ∧ get_aivdom U = get_aivdom S ∧ shrunken' = mset shrunken}
(try_to_forward_subsume_wl2 C' occs cands D' shrunken S')›
proof -
have le: ‹length (get_clauses_wl S' ∝ C) ≤ Suc (unat32_max div 2)›
if ‹try_to_forward_subsume_wl2_pre C' cands shrunken S'›
proof -
have lits: ‹literals_are_in_ℒ⇩i⇩n (all_init_atms_st S') (mset (get_clauses_wl S' ∝ C'))› and
dist: ‹distinct_mset (mset (get_clauses_wl S' ∝ C'))› and
tauto: ‹¬ tautology (mset (get_clauses_wl S' ∝ C'))›
using that unfolding try_to_forward_subsume_wl2_pre_def try_to_forward_subsume_wl_pre_def
try_to_forward_subsume_pre_def
apply -
subgoal
apply normalize_goal+
apply (frule literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def)
apply (rule literals_are_in_ℒ⇩i⇩n_nth)
apply (simp add: literals_are_ℒ⇩i⇩n_def literals_are_ℒ⇩i⇩n'_def)
apply (simp add: literals_are_in_ℒ⇩i⇩n_nth literals_are_ℒ⇩i⇩n_cong
literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff)
done
subgoal
apply normalize_goal+
unfolding twl_struct_invs_def twl_st_inv_alt_def
by (simp add:mset_take_mset_drop_mset')
subgoal
apply normalize_goal+
unfolding twl_list_invs_def
by (simp add:mset_take_mset_drop_mset')
done
have ‹isasat_input_bounded (all_init_atms_st S')›
using SS' unfolding twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def
by (simp del: isasat_input_bounded_def)
then show ?thesis
using simple_clss_size_upper_div2[of ‹all_init_atms_st S'› ‹mset (get_clauses_wl S' ∝ C')›, OF _ lits dist tauto] CC'
by auto
qed
have loop_rel: ‹(ebreak, ebreaka) ∈ bool_rel ⟹
try_to_forward_subsume_wl2_inv S' cands C' (0, False, ebreaka, occs, D', S') ⟹
((0, NONE, ebreak, D, S), 0, False, ebreaka, occs, D', S') ∈
{((m, b, brk, D, U),(m', b', brk', occs, D', V)). (m,m')∈nat_rel ∧ b'=(b≠NONE) ∧ (brk,brk')∈bool_rel ∧
(D,D')∈clause_hash ∧ (get_occs U, occs) ∈ occurrence_list_ref ∧ (U, V) ∈ twl_st_heur_restart_occs' (length (get_clauses_wl_heur S)) (learned_clss_count S) ∧
get_aivdom U = get_aivdom S}›
for ebreak ebreaka
using assms by auto
have [refine]: ‹RETURN (is_strengthened x1f) ≤ ⇓ bool_rel (RES UNIV)› for x1f
by (auto simp:)
have [refine]: ‹isa_try_to_forward_subsume_wl2_break S ≤ SPEC (λ_. True)› for S
unfolding isa_try_to_forward_subsume_wl2_break_def by auto
show ?thesis
supply [[goals_limit=1]]
unfolding isa_try_to_forward_subsume_wl2_def
try_to_forward_subsume_wl2_def mop_arena_length_st_def Let_def[of ‹if _ then mark_clause_for_unit_as_unchanged _ else _›]
apply (refine_vcg mop_arena_lit[of ‹get_clauses_wl_heur S› _ ‹set (get_vdom S)› for S]
mop_arena_length[THEN fref_to_Down_curry, of _ _ _ _ ‹set (get_vdom S)›, unfolded comp_def] loop_rel
isa_forward_subsumption_one_forward_subsumption_wl_one[where r=‹length (get_clauses_wl_heur S)› and u=‹(learned_clss_count S)›]
mop_cch_remove_all_clauses_mop_ch_remove_all_clauses[where r=‹length (get_clauses_wl_heur S)› and u=‹(learned_clss_count S)›])
subgoal
using assms unfolding isa_try_to_forward_subsume_wl_pre_def apply -
by (rule exI[of _ S'], rule exI[of _ r], rule exI[of _ u], rule exI[of _ cands], rule exI[of _ occs])
auto
subgoal using SS' CC' unfolding isa_try_to_forward_subsume_wl_pre_def try_to_forward_subsume_wl2_pre_def try_to_forward_subsume_wl_pre_def
try_to_forward_subsume_pre_def
by - (normalize_goal+; auto)
subgoal using SS' CC' unfolding twl_st_heur_restart_occs_def by simp
subgoal using le CC' by auto
subgoal for n ebreak ebreaka x x' using CC' SS' unfolding isa_try_to_forward_subsume_wl_inv_def case_prod_beta apply -
by (rule exI[of _ S'], rule exI[of _ ‹snd (snd (snd (snd (snd (x')))))›],
rule exI[of _ cands], rule exI[of _ ‹fst ((snd (snd (snd (x')))))›], rule exI[of _ ‹fst (snd (snd (snd (snd (x')))))›]; cases x')
auto
subgoal by simp
subgoal by auto
subgoal for n ebreak ebreaka x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x2f x1g
x2g x1h x2h
by (auto simp: twl_st_heur_restart_occs_def)
subgoal using CC' by auto
subgoal by auto
subgoal by auto
subgoal using CC' by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using CC' by auto
subgoal by auto
subgoal using CC' by auto
subgoal by auto
subgoal using cands by auto
subgoal using SS' CC' shrunken by auto
done
qed
definition clause_not_marked_to_delete_init_pre where
‹clause_not_marked_to_delete_init_pre =
(λ(S, C). C ∈ vdom_m (all_init_atms_st S) (get_watched_wl S) (get_clauses_wl S))›
lemma clause_not_marked_to_delete_rel_occs:
‹(S,T)∈twl_st_heur_restart_occs ⟹ (C,C')∈nat_rel ⟹ C ∈ set(get_vdom S) ⟹
(clause_not_marked_to_delete_heur S C, clause_not_marked_to_delete T C') ∈ bool_rel›
by (cases S, cases T)
(use arena_dom_status_iff[of ‹get_clauses_wl_heur S› ‹get_clauses_wl T›
‹set (get_vdom S)› ‹C›] in_dom_in_vdom in
‹auto 5 5 simp: clause_not_marked_to_delete_def twl_st_heur_restart_occs_def Let_def
clause_not_marked_to_delete_heur_def all_init_atms_st_def
clause_not_marked_to_delete_init_pre_def ac_simps; blast›)
lemma mop_polarity_pol_mop_polarity_wl:
‹(S,T)∈twl_st_heur_restart_occs ⟹ (L,L')∈nat_lit_lit_rel⟹L'∈# ℒ⇩a⇩l⇩l (all_init_atms_st T)⟹
mop_polarity_pol (get_trail_wl_heur S) L ≤ ⇓Id (mop_polarity_wl T L')›
unfolding mop_polarity_pol_def mop_polarity_wl_def
apply refine_vcg
subgoal
by (rule polarity_pol_pre[of _ ‹get_trail_wl T› ‹all_init_atms_st T›])
(auto simp add: ℒ⇩a⇩l⇩l_all_atms twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def)
subgoal
by (auto intro!: polarity_pol_polarity[of ‹(all_init_atms_st T)›, unfolded option_rel_id_simp, THEN fref_to_Down_unRET_uncurry_Id] simp: ℒ⇩a⇩l⇩l_all_atms IsaSAT_Restart.all_init_atms_alt_def twl_st_heur_restart_occs_def)
done
lemma isa_all_lit_clause_unset_all_lit_clause_unset:
assumes ‹(S, T) ∈ twl_st_heur_restart_occs' r u› ‹(C,C')∈nat_rel› and
‹isa_all_lit_clause_unset_pre C S›
shows
‹isa_all_lit_clause_unset C S ≤ ⇓ bool_rel (all_lit_clause_unset T C')›
proof -
have [refine]: ‹((0,True, added), (0,True))∈{((a,b,c), (d,e)). ((a,b), (d,e))∈nat_rel ×⇩f bool_rel}› for added
by auto
have lits: ‹literals_are_in_ℒ⇩i⇩n (all_init_atms_st T) (mset (get_clauses_wl T ∝ C))› and
dist: ‹distinct_mset (mset (get_clauses_wl T ∝ C))› and
tauto: ‹¬ tautology (mset (get_clauses_wl T ∝ C))›
if ‹C ∈# dom_m (get_clauses_wl T)› ‹forward_subsumption_all_wl_pre T›
using that unfolding forward_subsumption_all_wl_pre_def forward_subsumption_all_pre_def
apply -
subgoal
apply normalize_goal+
apply (frule literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def)
apply (rule literals_are_in_ℒ⇩i⇩n_nth)
apply (simp add: literals_are_ℒ⇩i⇩n_def literals_are_ℒ⇩i⇩n'_def)
apply (simp add: literals_are_in_ℒ⇩i⇩n_nth literals_are_ℒ⇩i⇩n_cong
literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff)
done
subgoal
apply normalize_goal+
unfolding twl_struct_invs_def twl_st_inv_alt_def
by (simp add:mset_take_mset_drop_mset')
subgoal
apply normalize_goal+
unfolding twl_list_invs_def
by (simp add:mset_take_mset_drop_mset')
done
have ‹heuristic_rel (all_init_atms_st T) (get_heur S)›
using assms unfolding twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def by fast
then have is_marked_added_heur_pre_stats: ‹L ∈# ℒ⇩a⇩l⇩l (all_init_atms_st T) ⟹is_marked_added_heur_pre (get_heur S) (atm_of L)› for L
by (auto simp: is_marked_added_heur_pre_stats_def heuristic_rel_def heuristic_rel_stats_def phase_saving_def is_marked_added_heur_pre_def
dest!: multi_member_split)
show ?thesis
unfolding isa_all_lit_clause_unset_def all_lit_clause_unset_def mop_clause_not_marked_to_delete_heur_def
nres_monad3 clause_not_marked_to_delete_def[symmetric] mop_arena_length_st_def
mop_is_marked_added_heur_st_def mop_is_marked_added_heur_def
apply (refine_vcg clause_not_marked_to_delete_rel_occs mop_arena_lit[where vdom=‹set (get_vdom S)›]
mop_polarity_pol_mop_polarity_wl
mop_arena_length[THEN fref_to_Down_curry, unfolded comp_def, of _ _ ‹get_clauses_wl_heur S› _ ‹set (get_vdom S)› for S])
subgoal using assms by fast
subgoal using assms unfolding clause_not_marked_to_delete_heur_pre_def isa_all_lit_clause_unset_pre_def
by (auto simp: arena_is_valid_clause_vdom_def twl_st_heur_restart_occs_def
intro!: exI[of _ ‹get_clauses_wl T›]
exI[of _ ‹set (get_vdom S)›])
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms unfolding clause_not_marked_to_delete_init_pre_def
by (auto simp: isa_all_lit_clause_unset_pre_def)
subgoal using assms by auto
subgoal by (auto simp: clause_not_marked_to_delete_def)
subgoal using assms unfolding twl_st_heur_restart_occs_def by auto
subgoal by auto
subgoal
using assms(1,2) simple_clss_size_upper_div2[of ‹all_init_atms_st T› ‹mset (get_clauses_wl T ∝ C)›, OF _ lits dist tauto]
by (auto simp del: isasat_input_bounded_def simp: clause_not_marked_to_delete_def
simp: twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def)
subgoal by (auto simp: unat32_max_def)
subgoal using assms unfolding twl_st_heur_restart_occs_def by auto
subgoal using assms by fast
subgoal by auto
subgoal using assms by auto
subgoal by (rule is_marked_added_heur_pre_stats) auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma valid_occs_empty:
assumes ‹(occs, empty_occs_list A) ∈ occurrence_list_ref›
shows ‹valid_occs occs vdom› and ‹cocc_content_set occs = {}›
proof -
show ‹cocc_content_set occs = {}›
using assms
apply (auto simp: valid_occs_def empty_occs_list_def occurrence_list_ref_def
map_fun_rel_def cocc_content_set_def in_set_conv_nth)
by (smt (verit, del_insts) fst_conv image_iff)
then show ‹valid_occs occs vdom›
using in_cocc_content_iff by (fastforce simp: valid_occs_def empty_occs_list_def occurrence_list_ref_def
map_fun_rel_def cocc_content_set_def)
qed
lemma twl_st_heur_restart_occs'_avdom_nth_vdom:
‹(S, S') ∈ twl_st_heur_restart_occs' r u ⟹ i < length (get_avdom S) ⟹
get_avdom S ! i ∈ set (get_vdom S)› and
twl_st_heur_restart_occs'_ivdom_nth_vdom:
‹(S, S') ∈ twl_st_heur_restart_occs' r u ⟹ i < length (get_ivdom S) ⟹
get_ivdom S ! i ∈ set (get_vdom S)›
using nth_mem[of i ‹get_avdom S›] nth_mem[of i ‹get_ivdom S›]
by (auto simp: twl_st_heur_restart_occs_def aivdom_inv_dec_alt_def simp del: nth_mem)
lemma isa_is_candidate_forward_subsumption:
assumes S: ‹(S, S') ∈ twl_st_heur_restart_occs' r u› ‹C ∈# dom_m (get_clauses_wl S')› and
pre: ‹forward_subsumption_all_wl_pre S'›
shows ‹isa_is_candidate_forward_subsumption S C ≤ ⇓ bool_rel (RES UNIV)›
proof -
have 1: ‹⇓ bool_rel (RES UNIV) = SPEC (λ_::bool. True)›
by (auto)
have valid: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl S') (set (get_vdom S))› and
heur: ‹heuristic_rel (all_init_atms_st S') (get_heur S)› and
trail: ‹(get_trail_wl_heur S, get_trail_wl S') ∈ trail_pol (all_init_atms_st S')›
using assms unfolding twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def by fast+
have H: ‹is_marked_added_heur_pre (get_heur S)
(atm_of (arena_lit (get_clauses_wl_heur S) (C + a)))› and
H': ‹(atm_of (arena_lit (get_clauses_wl_heur S) (C + a))) ∈# all_init_atms_st S'›
if ‹a < arena_length (get_clauses_wl_heur S) C› for a
proof -
have no_alien: ‹set_mset (ℒ⇩a⇩l⇩l (all_init_atms_st S')) = set_mset (all_lits_st S')›
using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(3)[of S', THEN ℒ⇩a⇩l⇩l_cong] pre
unfolding forward_subsumption_all_wl_pre_def
forward_subsumption_all_pre_def apply -
by normalize_goal+
(simp add: ℒ⇩a⇩l⇩l_all_atms)
have ‹a < length (get_clauses_wl S' ∝ C)›
using valid assms that by (auto simp: arena_lifting)
then have ‹atm_of (get_clauses_wl S' ∝ C ! a) ∈# all_atms_st S'›
using assms that by (auto simp: arena_lifting all_lits_def ran_m_def all_lits_of_mm_add_mset image_Un atm_of_all_lits_of_m(2)
all_atms_st_def all_atms_def simp del: all_atms_def[symmetric] dest!: multi_member_split[of C])
then show ‹(atm_of (arena_lit (get_clauses_wl_heur S) (C + a))) ∈# all_init_atms_st S'›
using valid assms that no_alien apply (auto simp: arena_lifting)
using ℒ⇩a⇩l⇩l_all_atms in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n by blast
then show ‹is_marked_added_heur_pre (get_heur S) (atm_of (arena_lit (get_clauses_wl_heur S) (C + a)))›
using heur unfolding heuristic_rel_def
by (auto simp: is_marked_added_heur_pre_def is_marked_added_heur_pre_stats_def
heuristic_rel_stats_def phase_saving_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
qed
show ?thesis
using valid
unfolding isa_is_candidate_forward_subsumption_def
mop_arena_lbd_st_def mop_arena_lbd_def mop_arena_status_st_def nres_monad3
mop_arena_status_def bind_to_let_conv mop_arena_length_st_def
mop_arena_length_def 1 mop_arena_lit_def mop_arena_lit2_def
mop_is_marked_added_heur_def mop_polarity_st_heur_def mop_polarity_pol_def
apply (refine_vcg
WHILET_rule[where R = ‹measure (λ(i,_). length (get_clauses_wl S' ∝ C) - i)› and I = ‹λ(i,_). i ≤ length (get_clauses_wl S' ∝ C)›])
subgoal
using assms by (auto simp: arena_act_pre_def arena_is_valid_clause_idx_def)
subgoal
using assms by (auto simp: get_clause_LBD_pre_def arena_is_valid_clause_idx_def)
subgoal
using assms by (auto simp: arena_is_valid_clause_idx_def)
subgoal
using assms by (auto simp: arena_is_valid_clause_vdom_def)
subgoal using arena_lifting[OF valid, of C] assms by auto
subgoal
by (auto intro!: RETURN_SPEC_refine)
subgoal by auto
subgoal by auto
subgoal using assms by (auto simp: arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
arena_lifting
intro!: exI[of _ ‹get_clauses_wl S'›] exI[of _ C])
subgoal using assms by (auto intro: H)
subgoal using assms by (auto simp: arena_lifting)
subgoal using assms by (auto simp: arena_lifting)
subgoal by auto
done
qed
lemma valid_occs_push_to_tvdom[intro!]:
‹valid_occs occs aivdom ⟹ valid_occs occs (push_to_tvdom C aivdom)›
unfolding valid_occs_def by auto
lemma valid_occs_empty_vdom[intro!]:
‹valid_occs occs vdom ⟹ valid_occs occs (empty_tvdom vdom)›
by (auto simp: valid_occs_def)
lemma valid_arena_vdom_le_strong:
assumes ‹valid_arena arena N ovdm›
shows ‹card ovdm ≤ length arena - 2›
proof -
have incl: ‹ovdm ⊆ {MIN_HEADER_SIZE..< length arena}›
apply auto
using assms valid_arena_in_vdom_le_arena by blast+
from card_mono[OF _ this] show ‹card ovdm ≤ length arena - 2› by auto
qed
lemma
assumes SS': ‹(S, S') ∈ twl_st_heur_restart_occs' r u›
shows
twl_st_heur_restart_occs'_avdom_vdom: ‹x1 < length (get_avdom S) ⟹ get_avdom S ! x1 ∈ set (get_vdom S)› and
twl_st_heur_restart_occs'_ivdom_vdom: ‹x1 < length (get_ivdom S) ⟹ get_ivdom S ! x1 ∈ set (get_vdom S)› and
twl_st_heur_restart_occs'_length_vdom_clauses: ‹length (get_vdom S) ≤ length (get_clauses_wl_heur S)› and
twl_st_heur_restart_occs'_length_tvdom_clauses: ‹length (get_tvdom S) ≤ length (get_clauses_wl_heur S)› and
twl_st_heur_restart_occs'_length_tvdom_clauses_notin: ‹C ∈ set (get_vdom S) ⟹ Suc (length (get_tvdom S)) < length (get_clauses_wl_heur S)›
‹C ∈ set (get_vdom S) ⟹ (length (get_tvdom S)) < length (get_clauses_wl_heur S)› and
twl_st_heur_restart_occs'_length_avdom_ivdom: ‹length (get_avdom S @ get_ivdom S) ≤ length (get_vdom S)› and
twl_st_heur_restart_occs'_length_avdom_ivdom_clauses: ‹length (get_avdom S @ get_ivdom S) ≤ length (get_clauses_wl_heur S)›
proof -
have arena: ‹valid_arena (get_clauses_wl_heur S) (get_clauses_wl S') (set (get_vdom S))› and
aivdom: ‹aivdom_inv_dec (get_aivdom S) (dom_m (get_clauses_wl S'))›
using SS' unfolding twl_st_heur_restart_occs_def by fast+
show ‹x1 < length (get_avdom S) ⟹ get_avdom S ! x1 ∈ set (get_vdom S)›
using aivdom nth_mem[of x1 ‹get_avdom S›] unfolding aivdom_inv_dec_alt_def
by (auto simp add: distinct_card simp del: nth_mem)
show ‹x1 < length (get_ivdom S) ⟹ get_ivdom S ! x1 ∈ set (get_vdom S)›
using aivdom nth_mem[of x1 ‹get_ivdom S›] unfolding aivdom_inv_dec_alt_def
by (auto simp add: distinct_card simp del: nth_mem)
show 1: ‹length (get_vdom S) ≤ length (get_clauses_wl_heur S)›
using valid_arena_vdom_le_strong[OF arena] aivdom unfolding aivdom_inv_dec_alt_def
by (simp add: distinct_card)
show ‹length (get_tvdom S) ≤ length (get_clauses_wl_heur S)›
using valid_arena_vdom_le(2)[OF arena] aivdom unfolding aivdom_inv_dec_alt_def
by (auto simp add: distinct_card dest!: size_mset_mono)
have WTF: ‹a ≥1 ⟹ a ≤ b - 2 ⟹ Suc a < b› for a b :: nat
by auto
have ‹mset (get_avdom S @ get_ivdom S) ⊆# mset (get_vdom S)›
unfolding aivdom_inv_dec_alt_def2
apply (auto simp del: size_mset simp flip: size_mset)
by (smt (z3) List.finite_set Un_iff aivdom aivdom_inv_dec_alt_def2 mset_set_Union mset_set_set mset_set_subset_iff subset_iff)
from size_mset_mono[OF this] show 2: ‹length (get_avdom S @ get_ivdom S) ≤ length (get_vdom S)›
using aivdom distinct_mset_mono[of ‹mset (get_avdom S)› ‹mset (get_vdom S)›] distinct_mset_mono[of ‹mset (get_ivdom S)› ‹mset (get_vdom S)›]
unfolding aivdom_inv_dec_alt_def2
by (auto simp del: size_mset simp flip: size_mset)
show ‹length (get_avdom S @ get_ivdom S) ≤ length (get_clauses_wl_heur S)›
using 1 2 by linarith
assume ‹C ∈ set (get_vdom S)›
then have ‹get_vdom S ≠ []›
by auto
then show ‹C ∈ set (get_vdom S) ⟹ Suc (length (get_tvdom S)) < length (get_clauses_wl_heur S)›
‹C ∈ set (get_vdom S) ⟹ (length (get_tvdom S)) < length (get_clauses_wl_heur S)›
using valid_arena_vdom_le_strong[OF arena] aivdom WTF[of ‹length (get_vdom S)› ‹length (get_clauses_wl_heur S)›]
unfolding aivdom_inv_dec_alt_def
by (auto simp add: distinct_card dest!: size_mset_mono)
qed
lemma isa_populate_occs:
assumes SS': ‹(S, S') ∈ twl_st_heur_restart_ana' r u›
shows ‹isa_populate_occs S ≤ ⇓{(U,(occs, cands')). (U, S') ∈ twl_st_heur_restart_occs' r u ∧
(get_tvdom U, cands')∈Id ∧ get_vdom U = get_vdom S ∧ (get_occs U, occs) ∈ occurrence_list_ref} (populate_occs S')›
proof -
have SS'': ‹(S,S')∈twl_st_heur_restart_occs' r u› and
aivdom: ‹aivdom_inv_dec (get_aivdom S) (dom_m (get_clauses_wl S'))› and
occs: ‹(get_occs S, empty_occs_list (all_init_atms_st S')) ∈ occurrence_list_ref›
using SS' unfolding twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def
twl_st_heur_restart_ana_def case_wl_split state_wl_recompose twl_st_heur_restart_def
by (auto simp add: valid_occs_empty)
have [refine]: ‹RETURN (get_occs S) ≤ ⇓ occurrence_list_ref (mop_occ_list_create (set_mset (all_init_atms_st S')))›
using valid_occs_empty[OF occs] occs
by (auto simp: mop_occ_list_create_def empty_occs_list_def)
have [refine0]: ‹empty_tvdom_st S ≤ SPEC (λc. (c, []) ∈ {(V,cands). cands=[] ∧
(V,S')∈twl_st_heur_restart_occs' (length (get_clauses_wl_heur S)) (learned_clss_count S) ∧
get_tvdom V = [] ∧ get_occs V = get_occs S ∧ get_clauses_wl_heur V = get_clauses_wl_heur S ∧
get_vdom V = get_vdom S ∧ get_ivdom V = get_ivdom S∧ get_avdom V = get_avdom S})›
(is ‹_ ≤ SPEC (λc. (c, _) ∈ ?empty)›)
using SS'' unfolding empty_tvdom_st_def
by (auto simp add: twl_st_heur_restart_occs_def)
have [refine]: ‹(get_occs T, occs) ∈ occurrence_list_ref ⟹ (T, cands) ∈ ?empty ⟹
((0, T), 0, occs, []) ∈ {((w, U), (w', occs, cands')).
get_avdom U = get_avdom S ∧
get_ivdom U = get_ivdom S ∧
get_vdom U = get_vdom S ∧
(w,w')∈nat_rel ∧ (get_tvdom U, cands')∈Id ∧ (get_occs U, occs)∈occurrence_list_ref ∧
(U, S')∈twl_st_heur_restart_occs' (length (get_clauses_wl_heur S)) (learned_clss_count S)}› (is ‹_ ⟹ _ ⟹ _ ∈ ?loop›) for occs xs cands T
by simp
have sorted: ‹sort_cands_by_length x2b
≤ ⇓ {(U, cands). (U, S') ∈ twl_st_heur_restart_occs' (length (get_clauses_wl_heur S)) (learned_clss_count S) ∧ get_avdom U = get_avdom x2b ∧
get_ivdom U = get_ivdom x2b ∧ get_vdom U = get_vdom x2b ∧ get_occs U = get_occs x2b ∧
get_tvdom U = cands}
(SPEC
(λcands'.
mset cands' = mset x2a ∧
sorted_wrt (λa b. length (get_clauses_wl S' ∝ a) ≤ length (get_clauses_wl S' ∝ b))
cands'))›
if
H: ‹forward_subsumption_all_wl_pre S'›
‹(get_avdom S @ get_ivdom S, xs) ∈ Id›
‹(get_occs S, occs) ∈ occurrence_list_ref›
‹(x, x') ∈ ?loop›
‹x2 = (x1a, x2a)›
‹x' = (x1, x2)›
‹x = (x1b, x2b)›
‹(S⇩0, cands) ∈ ?empty›
‹∀C∈set x2a. C ∈# dom_m (get_clauses_wl S') ∧ C ∈ set xs ∧ 2 < length (get_clauses_wl S' ∝ C)›
for xs occs x x' x1 x2 x1a x2a x1b x2b cands S⇩0
proof -
have K: ‹sorted_wrt (λa b. length (get_clauses_wl S' ∝ a) ≤ length (get_clauses_wl S' ∝ b)) tvdom›
if ‹sorted_wrt (λa b. arena_length (get_clauses_wl_heur x2b) a ≤ arena_length (get_clauses_wl_heur x2b) b)
(tvdom)› and
‹mset tvdom = mset (get_tvdom x2b)›
for tvdom
apply (rule sorted_wrt_mono_rel[of _ ‹(λa b. arena_length (get_clauses_wl_heur x2b) a
≤ arena_length (get_clauses_wl_heur x2b) b)›
‹(λa b. length (get_clauses_wl S' ∝ a) ≤ length (get_clauses_wl S' ∝ b))›])
subgoal for a b
using H(1-7,9) mset_eq_setD[OF that(2)] by (auto simp: twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def
arena_lifting)
subgoal using that(1) . done
show ?thesis
using that unfolding sort_cands_by_length_def
apply refine_vcg
subgoal
by (auto intro!: ASSERT_leI
simp: arena_lifting twl_st_heur_restart_occs_def
arena_is_valid_clause_idx_def
intro!: exI[of _ ‹get_clauses_wl S'›] exI[of _ ‹set (get_vdom S)›]
dest: mset_eq_setD)
subgoal for tvdom
apply (subst RETURN_RES_refine_iff)
apply (rule_tac x=tvdom in bexI)
defer
subgoal
by (auto simp: twl_st_heur_restart_occs_def RETURN_RES_refine_iff valid_occs_def
aivdom_inv_dec_alt_def simp del: distinct_mset_mset_distinct
simp flip: distinct_mset_mset_distinct dest: mset_eq_setD
dest!: K)
subgoal
apply (clarsimp simp: twl_st_heur_restart_occs_def
aivdom_inv_dec_alt_def simp del: distinct_mset_mset_distinct
simp flip: distinct_mset_mset_distinct dest: mset_eq_setD)
apply (simp add: valid_occs_def)
done
done
done
qed
have [simp]: ‹¬ x1 < length (get_avdom S) ⟹ x1 - length (get_avdom S) < length (get_ivdom S) ⟷ x1 < length (get_avdom S) + length (get_ivdom S)› for x1
by linarith
show ?thesis
supply [[goals_limit=1]]
unfolding isa_populate_occs_def populate_occs_def mop_arena_length_st_def
push_to_tvdom_st_def Let_def[of ‹length (get_avdom S)›]
apply (refine_vcg isa_all_lit_clause_unset_all_lit_clause_unset[where r=‹length (get_clauses_wl_heur S)› and u=‹(learned_clss_count S)›]
mop_arena_length[where vdom=‹set(get_vdom S)›, THEN fref_to_Down_curry, unfolded comp_def]
isa_push_to_occs_list_st_push_to_occs_list2[where r=‹length (get_clauses_wl_heur S)› and u=‹learned_clss_count S›]
isa_is_candidate_forward_subsumption[where r=‹length (get_clauses_wl_heur S)› and u=‹learned_clss_count S›])
subgoal using twl_st_heur_restart_occs'_length_avdom_ivdom_clauses[OF SS''] by auto
subgoal using aivdom unfolding aivdom_inv_dec_alt_def by (auto dest: distinct_mset_mono)
subgoal by auto
apply assumption
subgoal for xs occs Sa x x' unfolding isa_populate_occs_inv_def case_prod_beta
by (rule exI[of _ S'], rule exI[of _ ‹S'›], rule exI[of _ ‹fst (snd (x'))›], cases x') (use SS'' in clarsimp)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: access_avdom_at_pre_def)
subgoal by (auto simp: access_ivdom_at_pre_def)
subgoal for xs occs T x x' x1 x2 x1a x2a x1b x2b
using
twl_st_heur_restart_occs'_avdom_vdom[of x2b S' _ ‹learned_clss_count S› x1]
twl_st_heur_restart_occs'_ivdom_vdom[of x2b S' _ ‹learned_clss_count S› ‹x1 - length (get_avdom S)›]
by (auto simp: nth_append)
subgoal by auto
subgoal by (auto simp: nth_append)
subgoal
using SS''
unfolding isa_all_lit_clause_unset_pre_def apply -
by (rule exI[of _ S'], rule exI[of _ ‹length (get_clauses_wl_heur S)›] , rule exI[of _ ‹learned_clss_count S›])
(simp add: twl_st_heur_restart_occs'_avdom_nth_vdom twl_st_heur_restart_occs'_ivdom_nth_vdom SS''
eq_commute[of ‹get_avdom S @ get_ivdom S›])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal premises p using p(2-) by (clarsimp simp add: twl_st_heur_restart_occs_def nth_append)
subgoal by auto
subgoal by auto
subgoal by (auto simp: nth_append)
subgoal by auto
subgoal by (auto simp: unat32_max_def nth_append)
subgoal by auto
apply (solves auto)
subgoal by (auto simp: nth_append)
subgoal by auto
subgoal by auto
subgoal for xs occs T x x' x1 x2 x1a x2a x1b x2b all_undef all_undefa n cand canda
using twl_st_heur_restart_occs'_length_vdom_clauses[of x2b S' _ ‹learned_clss_count S›] by simp
subgoal for xs occs T x x' x1 x2 x1a x2a x1b x2b all_undef all_undefa n cand canda
using twl_st_heur_restart_occs'_length_tvdom_clauses_notin[of x2b S' _ ‹learned_clss_count S› ‹xs ! x1›]
twl_st_heur_restart_occs'_avdom_vdom[of x2b S' _ ‹learned_clss_count S› x1]
twl_st_heur_restart_occs'_ivdom_vdom[of x2b S' _ ‹learned_clss_count S› ‹x1 - length (get_avdom S)›]
by (auto simp: nth_append)
subgoal premises p using p(2-) by (clarsimp intro!: aivdom_push_to_tvdom simp: nth_append twl_st_heur_restart_occs_def)
(intro conjI impI aivdom_push_to_tvdom; clarsimp)
subgoal by auto
apply (rule sorted; assumption)
subgoal for xs occs x x' x1 x2 x1a x2a x1b x2b V sorted_cands
using SS' by (auto simp: twl_st_heur_restart_ana_def)
done
qed
lemma empty_occs2_replicate_empty: ‹empty_occs2 occs ≤ SPEC (λc. (c, replicate (length occs) []) ∈ Id)›
proof -
show ?thesis
unfolding empty_occs2_def
apply (refine_vcg WHILET_rule[where R = ‹measure (λ(i,_). length occs -i)› and
I = ‹ λ(i, occs'). i ≤ length occs ∧ length occs = length occs' ∧ take i occs' = replicate i []›])
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 simp: take_Suc_conv_app_nth replicate_Suc_conv_snoc list_update_append simp del: replicate_Suc)
subgoal by auto
subgoal by auto
done
qed
lemma empty_occs2_st_empty_occs_st: ‹empty_occs2_st S ≤ ⇓Id (empty_occs_st S)›
unfolding empty_occs2_st_def empty_occs_st_def
by (refine_vcg empty_occs2_replicate_empty) auto
lemma empty_occs_st:
‹(S, S') ∈ twl_st_heur_restart_occs' r u ⟹
fst occs = set_mset (all_init_atms_st S') ⟹
(get_occs S, occs) ∈ occurrence_list_ref ⟹
empty_occs_st S≤SPEC(λc. (c,S')∈twl_st_heur_restart_ana' r u)›
unfolding empty_occs_st_def twl_st_heur_restart_occs_def twl_st_heur_restart_ana_def IsaSAT_Restart.all_init_atms_alt_def
twl_st_heur_restart_def occurrence_list_ref_def empty_occs_list_def
by (auto, auto simp: map_fun_rel_def)
lemma empty_occs2_st:
‹(S, S') ∈ twl_st_heur_restart_occs' r u ⟹
fst occs = set_mset (all_init_atms_st S') ⟹
(get_occs S, occs) ∈ occurrence_list_ref ⟹
empty_occs2_st S≤SPEC(λc. (c,S')∈twl_st_heur_restart_ana' r u)›
apply (rule order_trans[OF empty_occs2_st_empty_occs_st])
apply (subst Down_id_eq)
by (rule empty_occs_st)
lemma [intro!]: ‹heuristic_rel A heur ⟹ heuristic_rel A (reset_added_heur heur)›
by (auto simp: heuristic_rel_def heuristic_rel_stats_def reset_added_heur_def reset_added_heur_stats_def
schedule_next_pure_lits_stats_def phase_saving_def)
lemma mop_mark_added_heur_st_it:
assumes ‹(S,T) ∈ twl_st_heur_restart_occs' r u› and ‹A ∈# all_init_atms_st T›
shows ‹mop_mark_added_heur_st A S ≤ SPEC (λc. (c, T) ∈ {(U, V). (U, V) ∈ twl_st_heur_restart_occs' r u ∧ (get_clauses_wl_heur U) = get_clauses_wl_heur S ∧
learned_clss_count U = learned_clss_count S ∧ get_vdom U = get_vdom S ∧ get_occs U = get_occs S})›
proof -
have heur: ‹heuristic_rel (all_init_atms_st T) (get_heur S)›
using assms(1)
by (auto simp: twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def)
show ?thesis
unfolding mop_mark_added_heur_st_def mop_mark_added_heur_def
apply refine_vcg
subgoal
using heur assms(2)
unfolding mark_added_heur_pre_def mark_added_heur_pre_stats_def
by (auto simp: heuristic_rel_def heuristic_rel_stats_def
phase_saving_def ℒ⇩a⇩l⇩l_all_atms_all_lits atms_of_def ℒ⇩a⇩l⇩l_add_mset
dest!: multi_member_split)
subgoal by (use assms in ‹auto simp add: twl_st_heur_restart_occs_def›)
done
qed
lemma mark_added_clause_heur2_id:
assumes ‹(S,T) ∈ twl_st_heur_restart_occs' r u› and ‹C ∈# dom_m (get_clauses_wl T)› and
lits: ‹literals_are_ℒ⇩i⇩n' T›
shows ‹mark_added_clause_heur2 S C
≤ ⇓{(U, V). (U, V) ∈ twl_st_heur_restart_occs' r u ∧ (get_clauses_wl_heur U) = get_clauses_wl_heur S ∧
learned_clss_count U = learned_clss_count S ∧ get_vdom U = get_vdom S ∧
get_occs U = get_occs S} (RETURN T)› (is ‹_ ≤⇓?R _›)
proof -
have 1: ‹mark_added_clause2 T C ≤ ⇓Id (RETURN T)›
unfolding mark_added_clause2_def mop_clauses_at_def nres_monad3
apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(i,_). length (get_clauses_wl T ∝ C) -i)›])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (use assms in auto)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
have eq: ‹set_mset (all_init_atms_st T) = set_mset (all_atms_st T)›
using lits by (simp add: literals_are_ℒ⇩i⇩n'_all_init_atms_alt_def)
have [refine]: ‹y' ∈# dom_m x' ⟹
((x, y), x', y') ∈ {(N, N'). valid_arena N N' (set (get_vdom S))} ×⇩f nat_rel ⟹
mop_arena_length x y ≤ SPEC (λy. (y, length (x' ∝ y')) ∈ {(a,b). (a,b)∈nat_rel ∧ a = length (x' ∝ y')})› for x y x' y'
apply (rule mop_arena_length[THEN fref_to_Down_curry, of _ _ _ _ ‹set (get_vdom S)›, unfolded comp_def conc_fun_RETURN prod.simps, THEN order_trans])
apply assumption
apply assumption
by auto
have [refine]: ‹((0, S), 0, T) ∈ nat_rel ×⇩r ?R›
using assms by auto
have 2: ‹mark_added_clause_heur2 S C ≤ ⇓?R (mark_added_clause2 T C)›
unfolding mark_added_clause_heur2_def mop_arena_length_st_def mop_access_lit_in_clauses_heur_def
mark_added_clause2_def
apply (refine_vcg mop_mark_added_heur_st_it[where r=r and u=u])
subgoal by (use assms in auto)
subgoal by (use assms in ‹auto simp: twl_st_heur_restart_occs_def›)
subgoal using assms by (auto simp: twl_st_heur_restart_occs_def dest: arena_lifting(10))
subgoal by auto
subgoal by auto
apply (rule_tac vdom = ‹set (get_vdom (x2a))› in mop_arena_lit2)
subgoal by (use assms in ‹auto simp: twl_st_heur_restart_occs_def›)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (use assms in ‹auto simp: eq all_atms_st_def all_atms_def all_lits_def ran_m_def
all_lits_of_mm_add_mset image_Un atm_of_all_lits_of_m(2)
dest!: multi_member_split›)
subgoal by auto
subgoal by auto
done
show ?thesis
unfolding mop_arena_length_st_def mop_access_lit_in_clauses_heur_def
apply (rule order_trans[OF 2])
apply (rule ref_two_step')
apply (rule 1[unfolded Down_id_eq])
done
qed
lemma isa_forward_reset_added_and_stats:
‹(S, S') ∈ twl_st_heur_restart_occs' r u ⟹
(isa_forward_reset_added_and_stats S, S') ∈ twl_st_heur_restart_occs' r u›
by (auto simp add: IsaSAT_Restart.all_init_atms_alt_def twl_st_heur_restart_occs_def incr_forward_rounds_st_def
isa_forward_reset_added_and_stats_def)
lemma [intro!]: ‹heuristic_rel 𝒜 (get_heur S) ⟹ heuristic_rel 𝒜 (schedule_next_subsume delta (get_heur S))›
by (auto simp: schedule_next_subsume_def heuristic_rel_def heuristic_rel_stats_def
schedule_next_subsume_stats_def)
lemma schedule_next_subsume_st:
‹(S, S') ∈ twl_st_heur_restart_occs' r u ⟹
(schedule_next_subsume_st delta S, S') ∈ twl_st_heur_restart_occs' r u›
by (auto simp add: IsaSAT_Restart.all_init_atms_alt_def twl_st_heur_restart_occs_def incr_forward_rounds_st_def
schedule_next_subsume_st_def)
lemma
get_occs_schedule_next_subsume_st[simp]: ‹get_occs (schedule_next_subsume_st delta S) = get_occs S› and
get_vdom_schedule_next_subsume_st[simp]: ‹get_vdom (schedule_next_subsume_st delta S) = get_vdom S›
by (auto simp: schedule_next_subsume_st_def)
lemma forward_subsumption_finalize:
assumes
‹(S, S') ∈ twl_st_heur_restart_occs' r u›
‹fst occs = set_mset (all_init_atms_st S')›
‹(get_occs S, occs) ∈ occurrence_list_ref› and
shrunken: ‹∀C∈#mset shrunken. C ∈ set (get_vdom S)› and
lits: ‹literals_are_ℒ⇩i⇩n' S'›
shows ‹forward_subsumption_finalize shrunken S≤SPEC(λc. (c,S')∈twl_st_heur_restart_ana' r u)› (is ‹_ ≤ ?C›)
proof -
have
1: ‹(RETURN S') ≥ do {
let S = S;
let _ = True;
(_, S) ← WHILE⇩T⇗λ(i,S). i ≤ length shrunken ∧ S=S'⇖(λ(i,S). i < length shrunken) (λ(i,S). do {
ASSERT (i < length shrunken);
let C = shrunken ! i;
b ← RES (UNIV :: bool set);
let S = S';
RETURN (i+1, S)
}) (0, S');
ASSERT (S = S');
RETURN S
}›
apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(i,_). length shrunken - i)›])
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
have [refine]: ‹isasat_current_progress c (isa_forward_reset_added_and_stats (schedule_next_subsume_st delta S)) ≤ SPEC (λc. (c, True) ∈ UNIV)› for c delta
unfolding isasat_current_progress_def by auto
have [refine]: ‹((0, isa_forward_reset_added_and_stats (schedule_next_subsume_st delta S)), 0, S') ∈ nat_rel ×⇩r {(U,U'). (U,U') ∈ twl_st_heur_restart_occs' r u ∧ get_vdom U = get_vdom S ∧
get_occs U = get_occs S}› (is ‹_ ∈ _ ×⇩r ?state›) for delta
using assms isa_forward_reset_added_and_stats[of ‹schedule_next_subsume_st delta S› S' r u]
schedule_next_subsume_st[of S S' r u]
by (auto simp: isa_forward_reset_added_and_stats_def)
have [refine]: ‹RETURN (clause_not_marked_to_delete_heur x2a (shrunken ! x1a))
≤ ⇓ {(b,b'). b=b' ∧ b'=(shrunken!x1a∈#dom_m (get_clauses_wl S'))} (RES UNIV)›
if ‹(x2a, S') ∈ ?state› ‹x1a < length shrunken›
for x2a x1a
using that shrunken arena_dom_status_iff(1)[of ‹get_clauses_wl_heur x2a› ‹get_clauses_wl S'› ‹set (get_vdom x2a)› ‹shrunken ! x1a›]
by (auto simp: clause_not_marked_to_delete_heur_def IsaSAT_Restart.all_init_atms_alt_def
twl_st_heur_restart_occs_def conc_fun_RES)
show ?thesis
unfolding forward_subsumption_finalize_def
mop_clause_not_marked_to_delete_heur_def nres_monad3
conc_fun_RETURN[symmetric] Let_def[of ‹isasat_current_progress _ _›]
apply (rule ref_two_step[OF _ 1])
apply (refine_vcg clause_not_marked_to_delete_rel[THEN fref_to_Down_unRET_uncurry]
mark_added_clause_heur2_id[unfolded conc_fun_RETURN, of _ S' r u, THEN order_trans]
empty_occs2_st[where occs = occs])
subgoal by auto
subgoal by auto
subgoal using shrunken
by (auto simp: clause_not_marked_to_delete_heur_pre_def twl_st_heur_restart_occs_def
arena_is_valid_clause_vdom_def
intro!: exI[of _ ‹get_clauses_wl S'›] exI[of _ ‹set (get_vdom S)›])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using lits by auto
apply assumption
subgoal by auto
subgoal by auto
subgoal using assms by auto
subgoal using assms by (auto simp: isa_forward_reset_added_and_stats_def)
subgoal using assms by auto
done
qed
lemma all_init_lits_of_wl_Pos_Neg_def:
‹set_mset (all_init_lits_of_wl S') = Pos ` set_mset (all_init_atms_st S') ∪ Neg ` set_mset (all_init_atms_st S')›
apply (auto simp: all_init_atms_st_alt_def image_image)
using literal.exhaust_sel apply blast
apply (simp add: in_all_lits_of_wl_ain_atms_of_iff)
apply (simp add: in_all_lits_of_wl_ain_atms_of_iff)
done
lemma get_conflict_wl_is_None_heur_get_conflict_wl_is_None_restart_occs:
‹(RETURN o get_conflict_wl_is_None_heur, RETURN o get_conflict_wl_is_None) ∈
twl_st_heur_restart_occs →⇩f ⟨Id⟩nres_rel›
unfolding get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def comp_def
apply (intro frefI nres_relI) apply refine_rcg
by (auto simp: twl_st_heur_restart_occs_def get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def
option_lookup_clause_rel_def
split: option.splits)
lemma mop_cch_add_all_clause_mop_ch_add_all:
assumes ‹(S, S') ∈ twl_st_heur_restart_occs' r u› ‹(C,C')∈nat_rel›
‹(D, D')∈clause_hash› and ‹C'∈#dom_m (get_clauses_wl S')›
shows ‹mop_cch_add_all_clause S C D ≤ ⇓clause_hash (mop_ch_add_all (mset (get_clauses_wl S' ∝ C')) D')›
proof -
have 1: ‹mop_ch_add_all_clause S' C' D' ≤⇓Id (mop_ch_add_all (mset (get_clauses_wl S' ∝ C')) D')›
unfolding mop_ch_add_all_clause_def mop_ch_add_all_def mop_clauses_at_def mop_ch_add_def
apply (refine_vcg
WHILET_rule[where I=‹λ(i, D). i ≤ length (get_clauses_wl S' ∝ C') ∧
D=ch_add_all (mset (take i (get_clauses_wl S' ∝ C'))) D'› and
R = ‹measure (λ(i,_). length (get_clauses_wl S' ∝ C') - i)›])
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: ch_add_all_def)
subgoal by auto
subgoal unfolding ch_add_pre_def ch_add_all_pre_def ch_add_all_def
by (auto simp: take_Suc_conv_app_nth distinct_in_set_take_iff)
(meson disjunct_not_in nth_mem_mset)
subgoal by auto
subgoal by (auto simp: ch_add_all_def take_Suc_conv_app_nth ch_add_def case_prod_beta)
subgoal by auto
subgoal by auto
done
have [refine]: ‹((0, D), 0, D') ∈ nat_rel ×⇩r clause_hash›
using assms by auto
show ?thesis
apply (rule ref_two_step[OF _ 1[unfolded Down_id_eq]])
unfolding mop_cch_add_all_clause_def mop_ch_add_all_clause_def mop_arena_length_st_def
mark_literal_for_unit_deletion_def Let_def[of "()"]
apply (refine_vcg mop_arena_length[where vdom = ‹set (get_vdom S)›,THEN fref_to_Down_curry, unfolded comp_def, of ‹get_clauses_wl S'› C']
mop_arena_lit[where vdom=‹set (get_vdom S)›] mop_cch_add_mop_cch_add)
subgoal using assms by auto
subgoal using assms unfolding twl_st_heur_restart_occs_def by auto
subgoal
using arena_lifting(10)[of ‹get_clauses_wl_heur S› ‹get_clauses_wl S'› ‹set (get_vdom S)› C] assms
unfolding twl_st_heur_restart_occs_def by (auto simp: arena_lifting)
subgoal by auto
subgoal by auto
subgoal using assms unfolding twl_st_heur_restart_occs_def by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma get_occs_incr_forward_rounds_st[simp]: ‹get_occs (incr_forward_rounds_st S) = get_occs S›
‹get_occs (isa_forward_reset_added_and_stats S) = get_occs S›
‹get_clauses_wl_heur (incr_forward_tried_st S) = (get_clauses_wl_heur S)›
‹learned_clss_count (incr_forward_tried_st S) = learned_clss_count S›
‹get_aivdom (incr_forward_tried_st S) = get_aivdom S›
‹get_occs (incr_forward_tried_st S) = get_occs S›
by (auto simp: incr_forward_rounds_st_def isa_forward_reset_added_and_stats_def
incr_forward_tried_st_def)
lemma isa_forward_subsumption_all_forward_subsumption_wl_all2:
assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u›
shows ‹isa_forward_subsumption_all S ≤
⇓(twl_st_heur_restart_ana' r u) (forward_subsumption_all_wl2 S')›
proof -
have SS'': ‹(S,S')∈twl_st_heur_restart_occs' r u›
using assms unfolding twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def
twl_st_heur_restart_ana_def case_wl_split state_wl_recompose twl_st_heur_restart_def
by (auto simp add: valid_occs_empty)
have [refine]: ‹ (get_occs x2a, occs) ∈ occurrence_list_ref ∧ (D, D') ∈clause_hash ∧ (x2a, S') ∈ twl_st_heur_restart_occs' (length (get_clauses_wl_heur S)) (learned_clss_count S) ⟹
((0, D, [], x2a), 0, occs, D', S', 2, {#}) ∈
{((m, D, shrunken, U), (n, occs, D', U', _, shrunken')). (m,n)∈nat_rel ∧ (D,D')∈clause_hash ∧ (get_occs U, occs) ∈ occurrence_list_ref ∧
shrunken' = mset shrunken ∧
(U, U') ∈ twl_st_heur_restart_occs' (length (get_clauses_wl_heur S)) (learned_clss_count S)∧ get_aivdom U = get_aivdom x2a}› for x2a occs D D'
by auto
have H: ‹(S, S') ∈ twl_st_heur_restart_occs' r u ⟹
∀L∈fst ` D⇩1 (set_mset (all_init_atms_st S')). L < length (get_watched_wl_heur S)› for S S' r u
apply (intro ballI impI)
unfolding twl_st_heur_restart_occs_def map_fun_rel_def IsaSAT_Restart.all_init_atms_alt_def
in_pair_collect_simp ℒ⇩a⇩l⇩l_all_init_atms(2) all_init_lits_of_wl_Pos_Neg_def[symmetric]
by normalize_goal+ auto
have H2: ‹(Sa, U) ∈ twl_st_heur_restart_occs ⟹
(incr_forward_tried_st Sa, U) ∈ twl_st_heur_restart_occs› for Sa U
by (auto simp: twl_st_heur_restart_occs_def incr_forward_tried_st_def)
have H3: ‹C ∈ set x1h ⟹
(Sa, S') ∈ twl_st_heur_restart_occs ⟹
mset x1h ⊆# mset (get_tvdom Sa) ⟹
get_vdom Sa = get_vdom S ⟹
C ∈ set (get_vdom S)›
for C x1h Sa
using multi_member_split[of C ‹mset x1h›] multi_member_split[of C ‹mset (get_tvdom Sa)›]
unfolding twl_st_heur_restart_occs_def IsaSAT_Restart.all_init_atms_alt_def
aivdom_inv_dec_alt_def
by (auto dest: mset_subset_eqD dest!: mset_subset_eq_insertD)
show ?thesis
supply [[goals_limit=1]]
unfolding isa_forward_subsumption_all_def
forward_subsumption_all_wl2_def Let_def
apply (refine_vcg ref_two_step[OF isa_populate_occs populate_occs_populate_occs_spec,
unfolded Down_id_eq, of _ _ ‹length (get_clauses_wl_heur S)› ‹(learned_clss_count S)›]
forward_subsumption_finalize[where r=‹length (get_clauses_wl_heur S)› and u=‹(learned_clss_count S)›]
mop_cch_create_mop_cch_create
mop_cch_add_all_clause_mop_ch_add_all[where r=‹length (get_clauses_wl_heur S)› and u=‹(learned_clss_count S)›]
isa_try_to_forward_subsume_wl2_try_to_forward_subsume_wl2[where r=‹length (get_clauses_wl_heur S)› and u=‹(learned_clss_count S)›]
isa_forward_reset_added_and_stats[where r=‹length (get_clauses_wl_heur S)› and u=‹(learned_clss_count S)›])
subgoal using assms unfolding isa_forward_subsumption_pre_all_def by blast
subgoal using assms by (auto simp: twl_st_heur_restart_ana_def)
subgoal unfolding forward_subsumption_all_wl_pre_def by blast
subgoal by (auto simp: isasat_fast_relaxed_def)
subgoal by (rule H) auto
subgoal by auto
subgoal by auto
subgoal for Sa x' x1 x2 D Da x x'a
using SS'' unfolding isa_forward_subsumption_all_wl_inv_def apply (case_tac x, hypsubst, unfold prod.simps)
by (rule exI[of _ S'], rule exI[of _ S'], rule exI[of _ ‹fst (snd (snd (snd x'a)))›],
rule_tac x= ‹fst (snd (snd (x'a)))› in exI, rule_tac x= ‹fst (snd x'a)› in exI,
rule_tac x=‹fst (snd (snd (snd (snd x'a))))› in exI)
auto
subgoal by (subst get_conflict_wl_is_None_heur_get_conflict_wl_is_None_restart_occs[THEN fref_to_Down_unRET_Id])
(auto simp: get_conflict_wl_is_None_def)
subgoal by auto
subgoal by (auto simp: access_tvdom_at_pre_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by simp
subgoal by (clarsimp dest!: size_mset_mono simp add: forward_subsumption_all_wl2_inv_def)
subgoal by (auto simp add:H2)
subgoal by (clarsimp simp add: H3)
apply (solves auto)
apply assumption
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using assms by (auto simp: twl_st_heur_restart_ana_def)
done
qed
lemma isa_forward_subsumption_all_forward_subsumption_wl_all:
assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u›
shows ‹isa_forward_subsumption_all S ≤
⇓(twl_st_heur_restart_ana' r u) (forward_subsumption_all_wl S')›
apply (rule ref_two_step)
apply (rule isa_forward_subsumption_all_forward_subsumption_wl_all2)
apply (rule assms)
apply (rule forward_subsumption_all_wl2_forward_subsumption_all_wl[unfolded Down_id_eq])
done
lemma isa_forward_subsume_forward_subsume_wl:
assumes ‹(S, S') ∈ twl_st_heur_restart_ana' r u›
shows ‹isa_forward_subsume S ≤
⇓(twl_st_heur_restart_ana' r u) (forward_subsume_wl S')›
proof -
have [refine]: ‹RETURN (should_subsume_st S) ≤ ⇓ bool_rel (forward_subsume_wl_needed S')›
unfolding forward_subsume_wl_needed_def by auto
show ?thesis
using assms
unfolding forward_subsume_wl_def isa_forward_subsume_def
by (refine_vcg isa_forward_subsumption_all_forward_subsumption_wl_all) auto
qed
end