Theory IsaSAT_Bump_Heuristics
theory IsaSAT_Bump_Heuristics
imports Watched_Literals_VMTF
IsaSAT_VMTF
Tuple4
IsaSAT_Bump_Heuristics_State
begin
section ‹Bumping›
thm isa_vmtf_find_next_undef_def
term isa_acids_find_next_undef
definition isa_acids_find_next_undef :: ‹(nat, nat) acids ⇒ trail_pol ⇒ (nat option × (nat, nat) acids) nres› where
‹isa_acids_find_next_undef = (λac M. do {
WHILE⇩T⇗λ(L, ac). True⇖
(λ(nxt, ac). nxt = None ∧ acids_mset ac ≠ {#})
(λ(a, ac). do {
ASSERT (a = None);
(L, ac) ← acids_pop_min ac;
ASSERT (defined_atm_pol_pre M L);
if defined_atm_pol M L then RETURN (None, ac)
else RETURN (Some L, ac)
}
)
(None, ac)
})›
lemma isa_acids_find_next_undef_acids_find_next_undef:
‹(uncurry isa_acids_find_next_undef, uncurry (acids_find_next_undef 𝒜)) ∈
Id ×⇩r trail_pol 𝒜 →⇩f ⟨⟨nat_rel⟩option_rel ×⇩r Id⟩nres_rel ›
proof -
have [refine]: ‹a=b⟹ acids_pop_min a ≤ ⇓ Id (acids_pop_min b)›for a b
by auto
show ?thesis
unfolding isa_acids_find_next_undef_def acids_find_next_undef_def uncurry_def
defined_atm_def[symmetric]
apply (intro frefI nres_relI)
apply refine_rcg
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (rule defined_atm_pol_pre) (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
subgoal
by (auto simp: undefined_atm_code[THEN fref_to_Down_unRET_uncurry_Id])
subgoal by auto
subgoal by auto
done
qed
definition vmtf_rescore_body
:: ‹nat multiset ⇒ nat clause_l ⇒ (nat,nat) ann_lits ⇒ bump_heuristics ⇒
(nat × bump_heuristics) nres›
where
‹vmtf_rescore_body 𝒜⇩i⇩n C _ vm = do {
WHILE⇩T⇗λ(i, vm). i ≤ length C⇖
(λ(i, vm). i < length C)
(λ(i, vm). do {
ASSERT(i < length C);
ASSERT(atm_of (C!i) ∈# 𝒜⇩i⇩n);
vm' ← isa_bump_mark_to_rescore (atm_of (C!i)) vm;
RETURN(i+1, vm')
})
(0, vm)
}›
definition vmtf_rescore
:: ‹nat multiset ⇒ nat clause_l ⇒ (nat,nat) ann_lits ⇒ bump_heuristics ⇒
(bump_heuristics) nres›
where
‹vmtf_rescore 𝒜⇩i⇩n C M vm = do {
(_, vm) ← vmtf_rescore_body 𝒜⇩i⇩n C M vm;
RETURN (vm)
}›
definition isa_bump_rescore_body
:: ‹nat clause_l ⇒ trail_pol ⇒ bump_heuristics ⇒
(nat × bump_heuristics) nres›
where
‹isa_bump_rescore_body C _ vm = do {
WHILE⇩T⇗λ(i, vm). i ≤ length C⇖
(λ(i, vm). i < length C)
(λ(i, vm). do {
ASSERT(i < length C);
vm' ← isa_bump_mark_to_rescore (atm_of (C!i)) vm;
RETURN(i+1, vm')
})
(0, vm)
}›
definition isa_bump_rescore
:: ‹nat clause_l ⇒ trail_pol ⇒ bump_heuristics ⇒ bump_heuristics nres›
where
‹isa_bump_rescore C M vm = do {
(_, vm) ← isa_bump_rescore_body C M vm;
RETURN (vm)
}›
definition isa_rescore_clause
:: ‹nat multiset ⇒ nat clause_l ⇒ (nat,nat)ann_lits ⇒ bump_heuristics ⇒
bump_heuristics nres›
where
‹isa_rescore_clause 𝒜 C M vm = SPEC (λ(vm'). vm' ∈ bump_heur 𝒜 M)›
lemma isa_bump_mark_to_rescore:
assumes
‹L ∈# 𝒜› ‹b ∈ bump_heur 𝒜 M› ‹length (fst (get_bumped_variables b)) < Suc (Suc (unat32_max div 2))›
shows ‹
isa_bump_mark_to_rescore L b ≤ SPEC (λvm'. vm' ∈ bump_heur 𝒜 M)›
proof -
have [simp]: ‹(atoms_hash_insert L x, set (fst (atoms_hash_insert L x))) ∈ distinct_atoms_rel 𝒜›
if ‹(x, set (fst x)) ∈ distinct_atoms_rel 𝒜›
for x
unfolding distinct_atoms_rel_def
apply (rule relcompI[of _ ‹(fst (atoms_hash_insert L x), insert L (set (fst x)))›])
using that assms(1)
by (auto simp: distinct_atoms_rel_def atoms_hash_rel_def atoms_hash_insert_def
distinct_hash_atoms_rel_def split: if_splits)
show ?thesis
using assms
unfolding isa_bump_mark_to_rescore_def
apply (auto split: bump_heuristics_splits simp: atms_hash_insert_pre_def
intro!: ASSERT_leI)
apply (auto simp: bump_heur_def distinct_atoms_rel_def atoms_hash_rel_def atoms_hash_insert_def
distinct_hash_atoms_rel_def intro: relcompI dest!: multi_member_split[of L])[]
apply (auto simp: bump_heur_def intro: dest!: multi_member_split[of L])
done
qed
lemma length_get_bumped_variables_le:
assumes ‹vm ∈ bump_heur 𝒜 M› ‹isasat_input_bounded 𝒜›
shows ‹length (fst (get_bumped_variables vm)) < Suc (Suc (unat32_max div 2))›
using assms bounded_included_le[of 𝒜 ‹fst (get_bumped_variables vm)›]
by (cases vm)
(auto simp: bump_heur_def distinct_atoms_rel_def distinct_hash_atoms_rel_def
atoms_hash_rel_def)
lemma vmtf_rescore_score_clause:
‹(uncurry2 (vmtf_rescore 𝒜), uncurry2 (isa_rescore_clause 𝒜)) ∈
[λ((C, M), vm). literals_are_in_ℒ⇩i⇩n 𝒜 (mset C) ∧ vm ∈ bump_heur 𝒜 M ∧ isasat_input_bounded 𝒜]⇩f
⟨Id⟩list_rel ×⇩f Id ×⇩f Id → ⟨Id⟩ nres_rel›
proof -
have H: ‹vmtf_rescore_body 𝒜 C M vm ≤
SPEC (λ(n :: nat, vm'). vm' ∈ bump_heur 𝒜 M)›
if M: ‹vm ∈ bump_heur 𝒜 M› and C: ‹∀c∈set C. atm_of c ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)› and
bounded: ‹isasat_input_bounded 𝒜›
for C vm φ M
unfolding vmtf_rescore_body_def
apply (refine_vcg WHILEIT_rule_stronger_inv[where R = ‹measure (λ(i, _). length C - i)› and
I' = ‹λ(i, vm'). vm' ∈ bump_heur 𝒜 M›] isa_bump_mark_to_rescore[where 𝒜=𝒜 and M=M])
subgoal by auto
subgoal by auto
subgoal using C M by (auto simp: vmtf_def phase_saving_def)
subgoal using C M by auto
subgoal using C by (auto simp: atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
subgoal using C by auto
subgoal using C length_get_bumped_variables_le[OF _ bounded] by auto
subgoal using C by auto
subgoal using C by auto
subgoal by auto
done
have K: ‹((a, b),(a', b')) ∈ A ×⇩f B ⟷ (a, a') ∈ A ∧ (b, b') ∈ B› for a b a' b' A B
by auto
show ?thesis
unfolding vmtf_rescore_def rescore_clause_def uncurry_def
apply (intro frefI nres_relI)
apply clarify
apply (rule bind_refine_spec)
prefer 2
apply (subst (asm) K)
apply (rule H; auto)
subgoal
by (meson atm_of_lit_in_atms_of contra_subsetD in_all_lits_of_m_ain_atms_of_iff
in_multiset_in_set literals_are_in_ℒ⇩i⇩n_def)
subgoal by (auto simp: isa_rescore_clause_def)
done
qed
lemma isa_vmtf_rescore_body:
‹(uncurry2 (isa_bump_rescore_body), uncurry2 (vmtf_rescore_body 𝒜)) ∈ [λ_. isasat_input_bounded 𝒜]⇩f
(Id ×⇩f trail_pol 𝒜 ×⇩f Id) → ⟨Id ×⇩r Id⟩ nres_rel›
proof -
show ?thesis
unfolding isa_bump_rescore_body_def vmtf_rescore_body_def uncurry_def
apply (intro frefI nres_relI)
apply refine_rcg
subgoal by auto
subgoal by auto
subgoal for x y x1 x1a x1b x2 x2a x2b x1c x1d x1e x2c x1g x2g
by (cases x2g) auto
subgoal by auto
apply (rule refine_IdI[OF eq_refl])
subgoal by auto
subgoal by auto
done
qed
lemma isa_vmtf_rescore:
‹(uncurry2 (isa_bump_rescore), uncurry2 (vmtf_rescore 𝒜)) ∈ [λ_. isasat_input_bounded 𝒜]⇩f
(Id ×⇩f trail_pol 𝒜 ×⇩f (Id)) → ⟨(Id)⟩ nres_rel›
proof -
show ?thesis
unfolding isa_bump_rescore_def vmtf_rescore_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg isa_vmtf_rescore_body[THEN fref_to_Down_curry2])
subgoal by auto
subgoal by auto
done
qed
definition vmtf_mark_to_rescore_clause where
‹vmtf_mark_to_rescore_clause 𝒜⇩i⇩n arena C vm = do {
ASSERT(arena_is_valid_clause_idx arena C);
nfoldli
([C..<C + (arena_length arena C)])
(λ_. True)
(λi vm. do {
ASSERT(i < length arena);
ASSERT(arena_lit_pre arena i);
ASSERT(atm_of (arena_lit arena i) ∈# 𝒜⇩i⇩n);
isa_bump_mark_to_rescore (atm_of (arena_lit arena i)) vm
})
vm
}›
definition isa_bump_mark_to_rescore_clause where
‹isa_bump_mark_to_rescore_clause arena C vm = do {
ASSERT(arena_is_valid_clause_idx arena C);
nfoldli
([C..<C + (arena_length arena C)])
(λ_. True)
(λi vm. do {
ASSERT(i < length arena);
ASSERT(arena_lit_pre arena i);
isa_bump_mark_to_rescore (atm_of (arena_lit arena i)) vm
})
vm
}›
lemma isa_bump_mark_to_rescore_clause_vmtf_mark_to_rescore_clause:
‹(uncurry2 isa_bump_mark_to_rescore_clause, uncurry2 (vmtf_mark_to_rescore_clause 𝒜)) ∈ [λ_. isasat_input_bounded 𝒜]⇩f
Id ×⇩f nat_rel ×⇩f (Id) → ⟨Id⟩nres_rel›
unfolding isa_bump_mark_to_rescore_clause_def vmtf_mark_to_rescore_clause_def
uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg nfoldli_refine[where R = ‹Id› and S = Id])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for x y x1 x1a x2 x2a x1b x1c x2b x2c xi xa si s
by (cases s)
(auto simp: isa_vmtf_mark_to_rescore_pre_def
intro!: atms_hash_insert_pre)
done
lemma vmtf_mark_to_rescore_clause_spec:
‹vm ∈ bump_heur 𝒜 M ⟹ valid_arena arena N vdom ⟹ C ∈# dom_m N ⟹ isasat_input_bounded 𝒜 ⟹
(∀C ∈ set [C..<C + arena_length arena C]. arena_lit arena C ∈# ℒ⇩a⇩l⇩l 𝒜) ⟹
vmtf_mark_to_rescore_clause 𝒜 arena C vm ≤ RES (bump_heur 𝒜 M)›
unfolding vmtf_mark_to_rescore_clause_def
apply (subst RES_SPEC_conv)
apply (refine_vcg nfoldli_rule[where I = ‹λ_ _ vm. vm ∈ bump_heur 𝒜 M›])
subgoal
unfolding arena_lit_pre_def arena_is_valid_clause_idx_def
apply (rule exI[of _ N])
apply (rule exI[of _ vdom])
apply (fastforce simp: arena_lifting)
done
subgoal for x it σ
using arena_lifting(7)[of arena N vdom C ‹x - C›]
by (auto simp: arena_lifting(1-6) dest!: in_list_in_setD)
subgoal for x it σ
unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
apply (rule exI[of _ C])
apply (intro conjI)
apply (solves ‹auto dest: in_list_in_setD›)
apply (rule exI[of _ N])
apply (rule exI[of _ vdom])
apply (fastforce simp: arena_lifting dest: in_list_in_setD)
done
subgoal for x it σ
by fastforce
subgoal for x it _ σ
using length_get_bumped_variables_le[of _ 𝒜]
by (cases σ)
(auto intro!: isa_bump_mark_to_rescore[THEN order_trans] simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
dest: in_list_in_setD)
done
definition vmtf_mark_to_rescore_also_reasons
:: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ arena ⇒ nat literal list ⇒ nat literal ⇒ _ ⇒_› where
‹vmtf_mark_to_rescore_also_reasons 𝒜 M arena outl L vm = do {
ASSERT(length outl ≤ unat32_max);
nfoldli
([0..<length outl])
(λ_. True)
(λi vm. do {
ASSERT(i < length outl); ASSERT(length outl ≤ unat32_max);
ASSERT(-outl ! i ∈# ℒ⇩a⇩l⇩l 𝒜);
if(outl!i = L)
then
RETURN vm
else do {
C ← get_the_propagation_reason M (-(outl ! i));
case C of
None ⇒ isa_bump_mark_to_rescore (atm_of (outl ! i)) vm
| Some C ⇒ if C = 0 then RETURN vm else vmtf_mark_to_rescore_clause 𝒜 arena C vm}
})
vm
}›
definition isa_vmtf_mark_to_rescore_also_reasons
:: ‹trail_pol ⇒ arena ⇒ nat literal list ⇒ nat literal ⇒ _ ⇒_› where
‹isa_vmtf_mark_to_rescore_also_reasons M arena outl L vm = do {
ASSERT(length outl ≤ unat32_max);
nfoldli
([0..<length outl])
(λ_. True)
(λi vm. do {
ASSERT(i < length outl); ASSERT(length outl≤ unat32_max);
if(outl!i = L)
then
RETURN vm
else do {
C ← get_the_propagation_reason_pol M (-(outl ! i));
case C of
None ⇒ do {
isa_bump_mark_to_rescore (atm_of (outl ! i)) vm
}
| Some C ⇒ if C = 0 then RETURN vm else isa_bump_mark_to_rescore_clause arena C vm
}
})
vm
}›
lemma isa_vmtf_mark_to_rescore_also_reasons_vmtf_mark_to_rescore_also_reasons:
‹(uncurry4 isa_vmtf_mark_to_rescore_also_reasons, uncurry4 (vmtf_mark_to_rescore_also_reasons 𝒜)) ∈
[λ_. isasat_input_bounded 𝒜]⇩f
trail_pol 𝒜 ×⇩f Id ×⇩f Id ×⇩f Id ×⇩f Id → ⟨Id⟩nres_rel›
unfolding isa_vmtf_mark_to_rescore_also_reasons_def vmtf_mark_to_rescore_also_reasons_def
uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg nfoldli_refine[where R = ‹Id› and S = Id]
get_the_propagation_reason_pol[of 𝒜, THEN fref_to_Down_curry]
isa_bump_mark_to_rescore[of _ 𝒜]
isa_bump_mark_to_rescore_clause_vmtf_mark_to_rescore_clause[of 𝒜, THEN fref_to_Down_curry2])
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 assumption
subgoal for x y x1 x1a _ _ _ x1b x2 x2a x2b x1c x1d x1e x2c x2d x2e xi xa si s xb x'
by (cases xb)
(auto simp: isa_vmtf_mark_to_rescore_pre_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
intro!: atms_hash_insert_pre[of _ 𝒜])
subgoal by auto
subgoal by auto
done
lemma vmtf_mark_to_rescore_also_reasons_spec:
‹vm ∈ bump_heur 𝒜 M ⟹ valid_arena arena N vdom ⟹ length outl ≤ unat32_max ⟹ isasat_input_bounded 𝒜 ⟹
(∀L ∈ set outl. L ∈# ℒ⇩a⇩l⇩l 𝒜) ⟹
(∀L ∈ set outl. ∀C. (Propagated (-L) C ∈ set M ⟶ C ≠ 0 ⟶ (C ∈# dom_m N ∧
(∀C ∈ set [C..<C + arena_length arena C]. arena_lit arena C ∈# ℒ⇩a⇩l⇩l 𝒜)))) ⟹
vmtf_mark_to_rescore_also_reasons 𝒜 M arena outl L vm ≤ RES (bump_heur 𝒜 M)›
unfolding vmtf_mark_to_rescore_also_reasons_def
apply (subst RES_SPEC_conv)
apply (refine_vcg nfoldli_rule[where I = ‹λ_ _ vm. vm ∈ bump_heur 𝒜 M›]
isa_bump_mark_to_rescore[of _ 𝒜])
subgoal by (auto dest: in_list_in_setD)
subgoal for x l1 l2 σ
unfolding all_set_conv_nth
by (auto simp: uminus_𝒜⇩i⇩n_iff dest!: in_list_in_setD)
subgoal for x l1 l2 σ
unfolding get_the_propagation_reason_def
apply (rule SPEC_rule)
apply (rename_tac reason, case_tac reason; simp only: option.simps RES_SPEC_conv[symmetric])
subgoal
using length_get_bumped_variables_le[of _ 𝒜 M]
by (auto intro!: isa_bump_mark_to_rescore[where M=M and 𝒜=𝒜, THEN order_trans]
simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff[symmetric])
apply (rename_tac D, case_tac ‹D = 0›; simp)
subgoal
by (rule vmtf_mark_to_rescore_clause_spec, assumption, assumption)
fastforce+
done
done
definition vmtf_mark_to_rescore_also_reasons_cl
:: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ arena ⇒ nat ⇒ nat literal ⇒ _ ⇒_› where
‹vmtf_mark_to_rescore_also_reasons_cl 𝒜 M arena C L vm = do {
ASSERT(arena_is_valid_clause_idx arena C);
nfoldli
([0..<arena_length arena C])
(λ_. True)
(λi vm. do {
K ← mop_arena_lit2 arena C i;
ASSERT(-K ∈# ℒ⇩a⇩l⇩l 𝒜);
if(K = L)
then
RETURN vm
else do {
C ← get_the_propagation_reason M (-K);
case C of
None ⇒ isa_bump_mark_to_rescore (atm_of K) vm
| Some C ⇒ if C = 0 then RETURN vm else vmtf_mark_to_rescore_clause 𝒜 arena C vm}
})
vm
}›
definition isa_vmtf_bump_to_rescore_also_reasons_cl
:: ‹trail_pol ⇒ arena ⇒ nat ⇒ nat literal ⇒ _ ⇒_› where
‹isa_vmtf_bump_to_rescore_also_reasons_cl M arena C L vm = do {
ASSERT(arena_is_valid_clause_idx arena C);
nfoldli
([0..<arena_length arena C])
(λ_. True)
(λi vm. do {
K ← mop_arena_lit2 arena C i;
if(K = L)
then
RETURN vm
else do {
C ← get_the_propagation_reason_pol M (-K);
case C of
None ⇒ do {
isa_bump_mark_to_rescore (atm_of K) vm
}
| Some C ⇒ if C = 0 then RETURN vm else isa_bump_mark_to_rescore_clause arena C vm
}
})
vm
}›
lemma isa_vmtf_bump_to_rescore_also_reasons_cl_vmtf_mark_to_rescore_also_reasons_cl:
‹(uncurry4 isa_vmtf_bump_to_rescore_also_reasons_cl, uncurry4 (vmtf_mark_to_rescore_also_reasons_cl 𝒜)) ∈
[λ_. isasat_input_bounded 𝒜]⇩f
trail_pol 𝒜 ×⇩f Id ×⇩f Id ×⇩f Id ×⇩f (Id) → ⟨Id⟩nres_rel›
proof -
have H: ‹f = g ⟹ (f,g) ∈ Id› for f g
by auto
show ?thesis
unfolding isa_vmtf_bump_to_rescore_also_reasons_cl_def vmtf_mark_to_rescore_also_reasons_cl_def
uncurry_def mop_arena_lit2_def
apply (intro frefI nres_relI)
apply (refine_rcg nfoldli_refine[where R = ‹Id› and S = Id]
get_the_propagation_reason_pol[of 𝒜, THEN fref_to_Down_curry]
isa_bump_mark_to_rescore_clause_vmtf_mark_to_rescore_clause[of 𝒜, THEN fref_to_Down_curry2])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply (rule H)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply assumption
subgoal for x y x1 x1a _ _ _ x1b x2 x2a x2b x1c x1d x1e x2c x2d x2e xi xa si s xb x'
by (cases xb)
(auto simp: isa_vmtf_mark_to_rescore_pre_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
intro!: atms_hash_insert_pre[of _ 𝒜])
subgoal by auto
subgoal by auto
done
qed
lemma arena_lifting_list:
‹valid_arena arena N vdom ⟹ C ∈# dom_m N ⟹
N ∝ C = map (λi. arena_lit arena (C+i)) [0..<arena_length arena C]›
by (subst list_eq_iff_nth_eq)
(auto simp: arena_lifting)
lemma vmtf_mark_to_rescore_also_reasons_cl_spec:
‹vm ∈ bump_heur 𝒜 M ⟹ valid_arena arena N vdom ⟹ C ∈# dom_m N ⟹ isasat_input_bounded 𝒜 ⟹
(∀L ∈ set (N ∝ C). L ∈# ℒ⇩a⇩l⇩l 𝒜) ⟹
(∀L ∈ set (N ∝ C). ∀C. (Propagated (-L) C ∈ set M ⟶ C ≠ 0 ⟶ (C ∈# dom_m N ∧
(∀C ∈ set [C..<C + arena_length arena C]. arena_lit arena C ∈# ℒ⇩a⇩l⇩l 𝒜)))) ⟹
vmtf_mark_to_rescore_also_reasons_cl 𝒜 M arena C L vm ≤ RES (bump_heur 𝒜 M)›
unfolding vmtf_mark_to_rescore_also_reasons_cl_def mop_arena_lit2_def
apply (subst RES_SPEC_conv)
apply (refine_vcg nfoldli_rule[where I = ‹λ_ _ vm. vm ∈ bump_heur 𝒜 M›])
subgoal by (auto simp: arena_is_valid_clause_idx_def)
subgoal for x l1 l2 σ by (auto simp: arena_lit_pre_def arena_lifting
arena_is_valid_clause_idx_and_access_def intro!: exI[of _ C] exI[of _ N]
dest: in_list_in_setD)
subgoal by (auto simp: arena_lifting arena_lifting_list image_image uminus_𝒜⇩i⇩n_iff)
subgoal for x l1 l2 σ
unfolding get_the_propagation_reason_def
apply (rule SPEC_rule)
apply (rename_tac reason, case_tac reason; simp only: option.simps RES_SPEC_conv[symmetric])
subgoal
using length_get_bumped_variables_le[of _ 𝒜]
by (auto intro!: isa_bump_mark_to_rescore[where 𝒜=𝒜 and M=M, THEN order_trans]
simp: arena_lifting_list in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff[symmetric])
apply (rename_tac D, case_tac ‹D = 0›; simp)
subgoal
by (rule vmtf_mark_to_rescore_clause_spec, assumption, assumption)
(auto simp: arena_lifting arena_lifting_list image_image uminus_𝒜⇩i⇩n_iff)
done
done
section ‹Backtrack level for Restarts›
hide_const (open) find_decomp_wl_imp
lemma isa_bump_unset_pre:
assumes
‹x ∈ bump_heur 𝒜 M› and
‹L ∈# 𝒜›
shows ‹isa_bump_unset_pre L x›
using assms vmtf_unset_pre_vmtf[where 𝒜=𝒜 and M=M and L=L]
acids_tl[where 𝒜=𝒜 and M=M and L=L]
by (cases ‹get_focused_heuristics x›)
(auto simp: isa_bump_unset_pre_def bump_heur_def acids_tl_pre_def
atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n acids_def)
definition isa_acids_flush_int :: ‹trail_pol ⇒ (nat, nat)acids ⇒ _ ⇒ ((nat, nat)acids × _) nres› where
‹isa_acids_flush_int = (λM vm (to_remove, h). do {
ASSERT(length to_remove ≤ unat32_max);
(_, vm, h) ← WHILE⇩T⇗λ(i, vm', h). i ≤ length to_remove⇖
(λ(i, vm, h). i < length to_remove)
(λ(i, vm, h). do {
ASSERT(i < length to_remove);
vm ← acids_push_literal (to_remove!i) vm;
ASSERT(atoms_hash_del_pre (to_remove!i) h);
RETURN (i+1, vm, atoms_hash_del (to_remove!i) h)})
(0, vm, h);
RETURN (vm, (emptied_list to_remove, h))
})›
lemma isa_acids_flush_int:
‹(uncurry2 isa_acids_flush_int, uncurry2 (acids_flush_int 𝒜)) ∈ trail_pol (𝒜::nat multiset) ×⇩f Id ×⇩f Id →⇩f ⟨Id×⇩f Id⟩nres_rel›
proof -
have [refine]: ‹x2c=x2 ⟹ x2e=x2b ⟹ ((0, x2c::(nat, nat)acids, x2e), 0, x2, x2b) ∈ nat_rel ×⇩r Id ×⇩r Id›
for x2c x2 x2e x2b
by auto
have [refine]: ‹(a,a')∈Id⟹(b,b')∈Id ⟹ acids_push_literal a b ≤⇓Id (acids_push_literal a' b')› for a a' b b'
by auto
show ?thesis
unfolding isa_acids_flush_int_def acids_flush_int_def uncurry_def
apply (intro frefI nres_relI)
apply refine_vcg
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
done
qed
definition isa_acids_incr_score :: ‹(nat, nat)acids ⇒ (nat, nat)acids› where
‹isa_acids_incr_score = (λ(a, m). (a, if m < unat64_max then m+1 else m))›
lemma isa_acids_incr_score: ‹ac ∈ acids 𝒜 M ⟹ isa_acids_incr_score ac ∈ acids 𝒜 M›
by (auto simp: isa_acids_incr_score_def acids_def)
definition isa_bump_heur_flush where
‹isa_bump_heur_flush M x = (case x of Tuple4 stabl focused foc bumped ⇒ do {
(stable, bumped) ← (if foc then RETURN (stabl, bumped) else isa_acids_flush_int M (isa_acids_incr_score stabl) bumped);
(focused, bumped) ← (if ¬foc then RETURN (focused, bumped) else isa_vmtf_flush_int M focused bumped);
RETURN (Tuple4 stable focused foc bumped)})›
definition isa_bump_flush
:: ‹nat multiset ⇒ (nat,nat) ann_lits ⇒ bump_heuristics ⇒ (bump_heuristics) nres›
where
‹isa_bump_flush 𝒜⇩i⇩n = (λM vm. SPEC (λx. x ∈ bump_heur 𝒜⇩i⇩n M))›
lemma in_distinct_atoms_rel_in_atmsD: ‹(ba, y) ∈ distinct_atoms_rel 𝒜 ⟹
xa ∈ set (fst ba) ⟹ xa ∈# 𝒜› and
distinct_atoms_rel_emptiedI: ‹((ae, baa), {}) ∈ distinct_atoms_rel 𝒜 ⟹
((ae, baa), set ae) ∈ distinct_atoms_rel 𝒜›
by (auto simp: distinct_atoms_rel_def distinct_hash_atoms_rel_def)
lemma acids_change_to_remove_order':
‹(uncurry2 (acids_flush_int 𝒜⇩i⇩n), uncurry2 (acids_flush 𝒜⇩i⇩n)) ∈
[λ((M, vm), to_r). vm ∈ acids 𝒜⇩i⇩n M ∧ isasat_input_bounded 𝒜⇩i⇩n ∧ isasat_input_nempty 𝒜⇩i⇩n ∧ to_r ⊆ set_mset 𝒜⇩i⇩n]⇩f
Id ×⇩f Id ×⇩f distinct_atoms_rel 𝒜⇩i⇩n → ⟨(Id ×⇩r distinct_atoms_rel 𝒜⇩i⇩n)⟩ nres_rel›
by (intro frefI nres_relI)
(use in ‹auto intro!: acids_change_to_remove_order›)
lemma isa_bump_heur_flush_isa_bump_flush:
‹(uncurry (isa_bump_heur_flush), uncurry (isa_bump_flush 𝒜))
∈ [λ(M, vm). vm ∈ bump_heur 𝒜 M ∧ isasat_input_bounded 𝒜 ∧
isasat_input_nempty 𝒜]⇩f trail_pol 𝒜 ×⇩f Id → ⟨Id⟩nres_rel›
unfolding isa_bump_heur_flush_def isa_bump_flush_def uncurry_def
apply (intro frefI nres_relI)
apply (case_tac x, case_tac ‹snd x›, simp only: snd_conv case_prod_beta tuple4.case)
apply refine_vcg
subgoal by fast
subgoal for x y a b x1 x2 x3 x4 aa ba
apply (cases y)
apply (auto split: bump_heuristics_splits simp: bump_heur_def vmtf_flush_def
conc_fun_RES distinct_atoms_rel_emptiedI
intro!: isa_vmtf_flush_int[where 𝒜=𝒜, THEN fref_to_Down_curry2, of _ _ _ , THEN order_trans]
vmtf_change_to_remove_order'[THEN fref_to_Down_curry2, of 𝒜 ‹fst y›, THEN order_trans]
dest: in_distinct_atoms_rel_in_atmsD
)
apply (auto split: bump_heuristics_splits simp: bump_heur_def vmtf_flush_def
conc_fun_RES distinct_atoms_rel_emptiedI
intro!: isa_vmtf_flush_int[where 𝒜=𝒜, THEN fref_to_Down_curry2, of _ _ _ , THEN order_trans]
vmtf_change_to_remove_order'[THEN fref_to_Down_curry2, of 𝒜 ‹fst y›, THEN order_trans]
dest: in_distinct_atoms_rel_in_atmsD
)
done
subgoal for x y a b x1 x2 x3 x4
apply (cases y)
apply (auto split: bump_heuristics_splits simp: bump_heur_def vmtf_flush_def
conc_fun_RES distinct_atoms_rel_emptiedI
intro!: isa_acids_flush_int[where 𝒜=𝒜, THEN fref_to_Down_curry2, of _ _ _ , THEN order_trans]
acids_change_to_remove_order'[THEN fref_to_Down_curry2, of 𝒜 ‹fst y›, THEN order_trans]
dest!: isa_acids_incr_score[of x1]
dest: in_distinct_atoms_rel_in_atmsD
)
apply (auto split: bump_heuristics_splits simp: bump_heur_def acids_flush_def
conc_fun_RES distinct_atoms_rel_emptiedI
dest: in_distinct_atoms_rel_in_atmsD)
done
done
text ‹
We here find out how many decisions can be reused. Remark that since VMTF does not reuse many levels anyway,
the implementation might be mostly useless, but I was not aware of that when I implemented it.
›
definition find_decomp_w_ns_pre where
‹find_decomp_w_ns_pre 𝒜 = (λ((M, highest), vm).
no_dup M ∧
highest < count_decided M ∧
isasat_input_bounded 𝒜 ∧
literals_are_in_ℒ⇩i⇩n_trail 𝒜 M ∧
vm ∈ bump_heur 𝒜 M)›
definition find_decomp_wl_imp
:: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ nat ⇒ bump_heuristics ⇒
((nat, nat) ann_lits × bump_heuristics) nres›
where
‹find_decomp_wl_imp 𝒜 = (λM⇩0 lev vm. do {
let k = count_decided M⇩0;
let M⇩0 = trail_conv_to_no_CS M⇩0;
let n = length M⇩0;
pos ← get_pos_of_level_in_trail M⇩0 lev;
ASSERT((n - pos) ≤ unat32_max);
ASSERT(n ≥ pos);
let target = n - pos;
(_, M, vm') ←
WHILE⇩T⇗λ(j, M, vm'). j ≤ target ∧
M = drop j M⇩0 ∧ target ≤ length M⇩0 ∧
vm' ∈ bump_heur 𝒜 M ∧ literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset M)⇖
(λ(j, M, vm). j < target)
(λ(j, M, vm). do {
ASSERT (count_decided M > lev);
ASSERT(M ≠ []);
ASSERT(Suc j ≤ unat32_max);
let L = atm_of (lit_of_hd_trail M);
ASSERT(L ∈# 𝒜);
vm ←isa_bump_unset L vm;
RETURN (j + 1, tl M, vm)
})
(0, M⇩0, vm);
ASSERT(lev = count_decided M);
let M = trail_conv_back lev M;
RETURN (M, vm')
})›
definition isa_find_decomp_wl_imp
:: ‹trail_pol ⇒ nat ⇒ bump_heuristics ⇒ (trail_pol × bump_heuristics) nres›
where
‹isa_find_decomp_wl_imp = (λM⇩0 lev vm. do {
let k = count_decided_pol M⇩0;
let M⇩0 = trail_pol_conv_to_no_CS M⇩0;
ASSERT(isa_length_trail_pre M⇩0);
let n = isa_length_trail M⇩0;
pos ← get_pos_of_level_in_trail_imp M⇩0 lev;
ASSERT((n - pos) ≤ unat32_max);
ASSERT(n ≥ pos);
let target = n - pos;
(_, M, vm') ←
WHILE⇩T⇗λ(j, M, vm'). j ≤ target⇖
(λ(j, M, vm). j < target)
(λ(j, M, vm). do {
ASSERT(Suc j ≤ unat32_max);
ASSERT(case M of (M, _) ⇒ M ≠ []);
ASSERT(tl_trailt_tr_no_CS_pre M);
let L = atm_of (lit_of_last_trail_pol M);
ASSERT(isa_bump_unset_pre L vm);
vm ← isa_bump_unset L vm;
RETURN (j + 1, tl_trailt_tr_no_CS M, vm)
})
(0, M⇩0, vm);
M ← trail_conv_back_imp lev M;
RETURN (M, vm')
})›
abbreviation find_decomp_w_ns_prop where
‹find_decomp_w_ns_prop 𝒜 ≡
(λ(M::(nat, nat) ann_lits) highest _.
(λ(M1, vm). ∃K M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
get_level M K = Suc highest ∧ vm ∈ bump_heur 𝒜 M1))›
definition find_decomp_w_ns where
‹find_decomp_w_ns 𝒜 =
(λ(M::(nat, nat) ann_lits) highest vm.
SPEC(find_decomp_w_ns_prop 𝒜 M highest vm))›
lemma isa_find_decomp_wl_imp_find_decomp_wl_imp:
‹(uncurry2 isa_find_decomp_wl_imp, uncurry2 (find_decomp_wl_imp 𝒜)) ∈
[λ((M, lev), vm). lev < count_decided M]⇩f trail_pol 𝒜 ×⇩f nat_rel ×⇩f Id →
⟨trail_pol 𝒜 ×⇩r (Id)⟩nres_rel›
proof -
have [intro]: ‹(M', M) ∈ trail_pol 𝒜 ⟹ (M', M) ∈ trail_pol_no_CS 𝒜› for M' M
by (auto simp: trail_pol_def trail_pol_no_CS_def control_stack_length_count_dec[symmetric])
have loop_init[refine0]: ‹⋀x y x1 x1a x2 x2a x1b x1c x2b x2c pos posa.
case y of (x, xa) ⇒ (case x of (M, lev) ⇒ λvm. lev < count_decided M) xa ⟹
(x, y) ∈ trail_pol 𝒜 ×⇩f nat_rel ×⇩f Id ⟹
x1 = (x1a, x2) ⟹
y = (x1, x2a) ⟹
x1b = (x1c, x2b) ⟹
x = (x1b, x2c) ⟹
isa_length_trail_pre (trail_pol_conv_to_no_CS x1c) ⟹
(pos, posa) ∈ nat_rel ⟹
length (trail_conv_to_no_CS x1a) - posa ≤ unat32_max ⟹
posa ≤ length (trail_conv_to_no_CS x1a) ⟹
isa_length_trail (trail_pol_conv_to_no_CS x1c) - pos ≤ unat32_max ⟹
pos ≤ isa_length_trail (trail_pol_conv_to_no_CS x1c) ⟹
case (0, trail_conv_to_no_CS x1a, x2a) of
(j, M, vm') ⇒
j ≤ length (trail_conv_to_no_CS x1a) - posa ∧
M = drop j (trail_conv_to_no_CS x1a) ∧
length (trail_conv_to_no_CS x1a) - posa
≤ length (trail_conv_to_no_CS x1a) ∧
vm' ∈ bump_heur 𝒜 M ∧ literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset M) ⟹
((0, trail_pol_conv_to_no_CS x1c, x2c), 0, trail_conv_to_no_CS x1a, x2a)
∈ nat_rel ×⇩r trail_pol_no_CS 𝒜 ×⇩r Id›
supply trail_pol_conv_to_no_CS_def[simp] trail_conv_to_no_CS_def[simp]
by auto
have trail_pol_empty: ‹(([], x2g), M) ∈ trail_pol_no_CS 𝒜 ⟹ M = []› for M x2g
by (auto simp: trail_pol_no_CS_def ann_lits_split_reasons_def)
have trail_pol_no_CS_last_hd:
‹((x1h, t), M) ∈ trail_pol_no_CS 𝒜 ⟹ M ≠ [] ⟹ (last x1h) = lit_of (hd M)›
for x1h t M
by (auto simp: trail_pol_no_CS_def ann_lits_split_reasons_def last_map last_rev)
have trail_conv_back: ‹trail_conv_back_imp x2b x1g
≤ SPEC
(λc. (c, trail_conv_back x2 x1e)
∈ trail_pol 𝒜)›
if
‹case y of (x, xa) ⇒ (case x of (M, lev) ⇒ λvm. lev < count_decided M) xa› and
‹(x, y) ∈ trail_pol 𝒜 ×⇩f nat_rel ×⇩f Id› and
‹x1 = (x1a, x2)› and
‹y = (x1, x2a)› and
‹x1b = (x1c, x2b)› and
‹x = (x1b, x2c)› and
‹isa_length_trail_pre (trail_pol_conv_to_no_CS x1c)› and
‹(pos, posa) ∈ nat_rel› and
‹length (trail_conv_to_no_CS x1a) - posa ≤ unat32_max› and
‹isa_length_trail (trail_pol_conv_to_no_CS x1c) - pos ≤ unat32_max› and
‹(xa, x') ∈ nat_rel ×⇩r trail_pol_no_CS 𝒜 ×⇩r Id› and
‹x2d = (x1e, x2e)› and
‹x' = (x1d, x2d)› and
‹x2f = (x1g, x2g)› and
‹xa = (x1f, x2f)› and
‹x2 = count_decided x1e›
for x y x1 x1a x2 x2a x1b x1c x2b x2c pos posa xa x' x1d x2d x1e x2e x1f x2f
x1g x2g
apply (rule trail_conv_back[THEN fref_to_Down_curry, THEN order_trans])
using that by (auto simp: conc_fun_RETURN)
have bump: ‹(a,a')∈Id ⟹ (b,b')∈Id ⟹ isa_bump_unset a b ≤⇓Id (isa_bump_unset a' b')› for a a' b b'
by auto
show ?thesis
supply [refine del] = refine(13)
supply trail_pol_conv_to_no_CS_def[simp] trail_conv_to_no_CS_def[simp]
unfolding isa_find_decomp_wl_imp_def find_decomp_wl_imp_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_vcg bump
id_trail_conv_to_no_CS[THEN fref_to_Down, unfolded comp_def]
get_pos_of_level_in_trail_imp_get_pos_of_level_in_trail[of 𝒜, THEN fref_to_Down_curry])
subgoal
by (rule isa_length_trail_pre) auto
subgoal
by (auto simp: get_pos_of_level_in_trail_pre_def)
subgoal
by auto
subgoal
by (subst isa_length_trail_length_u_no_CS[THEN fref_to_Down_unRET_Id]) auto
subgoal
by (subst isa_length_trail_length_u_no_CS[THEN fref_to_Down_unRET_Id]) auto
apply (assumption+)[10]
subgoal
by (subst isa_length_trail_length_u_no_CS[THEN fref_to_Down_unRET_Id]) auto
subgoal
by auto
subgoal
by (subst isa_length_trail_length_u_no_CS[THEN fref_to_Down_unRET_Id]) auto
subgoal
by (subst isa_length_trail_length_u_no_CS[THEN fref_to_Down_unRET_Id]) auto
subgoal
by auto
subgoal
by (auto dest!: trail_pol_empty)
subgoal for x y x1 x1a x2 x2a x1b x1c x2b x2c pos posa
by (rule tl_trailt_tr_no_CS_pre) auto
subgoal for x y x1 x1a x2 x2a x1b x1c x2b x2c pos posa xa x' x1d x2d x1e x2e x1f x2f
x1g x1h x2g x2h
by (cases x1g, cases x2h)
(auto intro!: isa_bump_unset_pre[of _ 𝒜 ‹drop x1d x1a›]
simp: lit_of_last_trail_pol_def trail_pol_no_CS_last_hd lit_of_hd_trail_def)
subgoal
by (auto simp: lit_of_last_trail_pol_def trail_pol_no_CS_last_hd lit_of_hd_trail_def
intro!: tl_trail_tr_no_CS[THEN fref_to_Down_unRET]
isa_vmtf_unset_vmtf_unset[THEN fref_to_Down_unRET_uncurry])
subgoal
by (auto simp: lit_of_last_trail_pol_def trail_pol_no_CS_last_hd lit_of_hd_trail_def
intro!: tl_trail_tr_no_CS[THEN fref_to_Down_unRET]
isa_vmtf_unset_vmtf_unset[THEN fref_to_Down_unRET_uncurry])
subgoal
by (auto simp: lit_of_last_trail_pol_def trail_pol_no_CS_last_hd lit_of_hd_trail_def
intro!: tl_trail_tr_no_CS[THEN fref_to_Down_unRET]
isa_vmtf_unset_vmtf_unset[THEN fref_to_Down_unRET_uncurry])
apply (rule trail_conv_back; assumption)
subgoal
by auto
done
qed
definition (in -) find_decomp_wl_st :: ‹nat literal ⇒ nat twl_st_wl ⇒ nat twl_st_wl nres› where
‹find_decomp_wl_st = (λL (M, N, D, oth). do{
M' ← find_decomp_wl' M (the D) L;
RETURN (M', N, D, oth)
})›
definition find_decomp_wl_st_int :: ‹nat ⇒ isasat ⇒ isasat nres› where
‹find_decomp_wl_st_int = (λhighest S. do{
let M = get_trail_wl_heur S;
let vm = get_vmtf_heur S;
(M', vm) ← isa_find_decomp_wl_imp M highest vm;
let S = set_trail_wl_heur M' S;
let S = set_vmtf_wl_heur vm S;
RETURN S
})›
lemma
assumes
vm: ‹vm ∈ bump_heur 𝒜 M⇩0› and
lits: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M⇩0› and
target: ‹highest < count_decided M⇩0› and
n_d: ‹no_dup M⇩0› and
bounded: ‹isasat_input_bounded 𝒜› and
count:‹count_decided M⇩0 > 0›
shows
find_decomp_wl_imp_le_find_decomp_wl':
‹find_decomp_wl_imp 𝒜 M⇩0 highest vm ≤ find_decomp_w_ns 𝒜 M⇩0 highest vm›
(is ?decomp)
proof -
have length_M0: ‹length M⇩0 ≤ unat32_max div 2 + 1›
using length_trail_unat32_max_div2[of 𝒜 M⇩0, OF bounded]
n_d literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[of 𝒜, OF lits]
by (auto simp: lits_of_def)
have 1: ‹((count_decided x1g, x1g), count_decided x1, x1) ∈ Id›
if ‹x1g = x1› for x1g x1 :: ‹(nat, nat) ann_lits›
using that by auto
have [simp]: ‹∃M'a. M' @ x2g = M'a @ tl x2g› for M' x2g :: ‹(nat, nat) ann_lits›
by (rule exI[of _ ‹M' @ (if x2g = [] then [] else [hd x2g])›]) auto
have butlast_nil_iff: ‹butlast xs = [] ⟷ xs = [] ∨ (∃a. xs = [a])› for xs :: ‹(nat, nat) ann_lits›
by (cases xs) auto
have butlast1: ‹tl x2g = drop (Suc (length x1) - length x2g) x1› (is ‹?G1›)
if ‹x2g = drop (length x1 - length x2g) x1› for x2g x1 :: ‹'a list›
proof -
have [simp]: ‹Suc (length x1 - length x2g) = Suc (length x1) - length x2g›
by (metis Suc_diff_le diff_le_mono2 diff_zero length_drop that zero_le)
show ?G1
by (subst that) (auto simp: butlast_conv_take tl_drop_def)[]
qed
have butlast2: ‹tl x2g = drop (length x1 - (length x2g - Suc 0)) x1› (is ‹?G2›)
if ‹x2g = drop (length x1 - length x2g) x1› and x2g: ‹x2g ≠ []› for x2g x1 :: ‹'a list›
proof -
have [simp]: ‹Suc (length x1 - length x2g) = Suc (length x1) - length x2g›
by (metis Suc_diff_le diff_le_mono2 diff_zero length_drop that(1) zero_le)
have [simp]: ‹Suc (length x1) - length x2g = length x1 - (length x2g - Suc 0)›
using x2g by auto
show ?G2
by (subst that) (auto simp: butlast_conv_take tl_drop_def)[]
qed
note butlast = butlast1 butlast2
have count_decided_not_Nil[simp]: ‹0 < count_decided M ⟹ M ≠ []› for M :: ‹(nat, nat) ann_lits›
by auto
have get_lev_last: ‹get_level (M' @ M) (lit_of (last M')) = Suc (count_decided M)›
if ‹M⇩0 = M' @ M› and ‹M' ≠ []› and ‹is_decided (last M')› for M' M
apply (cases M' rule: rev_cases)
using that apply (solves simp)
using n_d that by auto
have atm_of_N:
‹literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset aa) ⟹ aa ≠ [] ⟹ atm_of (lit_of (hd aa)) ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
for aa
by (cases aa) (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
have Lin_drop_tl: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset (drop b M⇩0)) ⟹
literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset (tl (drop b M⇩0)))› for b
apply (rule literals_are_in_ℒ⇩i⇩n_mono)
apply assumption
by (cases ‹drop b M⇩0›) auto
have highest: ‹highest = count_decided M› and
ex_decomp: ‹∃K M2.
(Decided K # M, M2)
∈ set (get_all_ann_decomposition M⇩0) ∧
get_level M⇩0 K = Suc highest ∧ vm ∈ bump_heur 𝒜 M›
if
pos: ‹pos < length M⇩0 ∧ is_decided (rev M⇩0 ! pos) ∧ get_level M⇩0 (lit_of (rev M⇩0 ! pos)) =
highest + 1› and
‹length M⇩0 - pos ≤ unat32_max› and
inv: ‹case s of (j, M, vm') ⇒
j ≤ length M⇩0 - pos ∧
M = drop j M⇩0 ∧
length M⇩0 - pos ≤ length M⇩0 ∧
vm' ∈ bump_heur 𝒜 M ∧
literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset M)› and
cond: ‹¬ (case s of
(j, M, vm) ⇒ j < length M⇩0 - pos)› and
s: ‹s = (j, s')› ‹s' = (M, vm)›
for pos s j s' M vm
proof -
have
‹j = length M⇩0 - pos› and
M: ‹M = drop (length M⇩0 - pos) M⇩0› and
vm: ‹vm ∈ bump_heur 𝒜 (drop (length M⇩0 - pos) M⇩0)› and
‹literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset (drop (length M⇩0 - pos) M⇩0))›
using cond inv unfolding s
by auto
define M2 and L where ‹M2 = take (length M⇩0 - Suc pos) M⇩0› and ‹L = rev M⇩0 ! pos›
have le_Suc_pos: ‹length M⇩0 - pos = Suc (length M⇩0 - Suc pos)›
using pos by auto
have 1: ‹take (length M⇩0 - pos) M⇩0 = take (length M⇩0 - Suc pos) M⇩0 @ [rev M⇩0 ! pos]›
unfolding le_Suc_pos
apply (subst take_Suc_conv_app_nth)
using pos by (auto simp: rev_nth)
have M⇩0: ‹M⇩0 = M2 @ L # M›
apply (subst append_take_drop_id[symmetric, of _ ‹length M⇩0 - pos›])
unfolding M L_def M2_def 1
by auto
have L': ‹Decided (lit_of L) = L›
using pos unfolding L_def[symmetric] by (cases L) auto
then have M⇩0': ‹M⇩0 = M2 @ Decided (lit_of L) # M›
unfolding M⇩0 by auto
have ‹highest = count_decided M› and ‹get_level M⇩0 (lit_of L) = Suc highest› and ‹is_decided L›
using n_d pos unfolding L_def[symmetric] unfolding M⇩0
by (auto simp: get_level_append_if split: if_splits)
then show
‹∃K M2.
(Decided K # M, M2)
∈ set (get_all_ann_decomposition M⇩0) ∧
get_level M⇩0 K = Suc highest ∧ vm ∈ bump_heur 𝒜 M›
using get_all_ann_decomposition_ex[of ‹lit_of L› M M2] vm unfolding M⇩0'[symmetric] M[symmetric]
by blast
show ‹highest = count_decided M›
using ‹highest = count_decided M› .
qed
have count_dec_larger: ‹highest < count_decided M›
if
pos: ‹pos < length M⇩0 ∧ is_decided (rev M⇩0 ! pos) ∧ get_level M⇩0 (lit_of (rev M⇩0 ! pos)) =
highest + 1› and
‹length M⇩0 - pos ≤ unat32_max› and
inv: ‹case s of (j, M, vm') ⇒
j ≤ length M⇩0 - pos ∧
M = drop j M⇩0 ∧
length M⇩0 - pos ≤ length M⇩0 ∧
vm' ∈ bump_heur 𝒜 M ∧
literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset M)› and
cond: ‹(case s of
(j, M, vm) ⇒ j < length M⇩0 - pos)› and
s: ‹s = (j, s')› ‹s' = (M, vm)›
for pos s j s' M vm
proof -
define M2 and L where ‹M2 = take (length M⇩0 - Suc pos) M⇩0› and ‹L = rev M⇩0 ! pos›
have le_Suc_pos: ‹length M⇩0 - pos = Suc (length M⇩0 - Suc pos)›
using pos by auto
have 1: ‹take (length M⇩0 - pos) M⇩0 = take (length M⇩0 - Suc pos) M⇩0 @ [rev M⇩0 ! pos]›
unfolding le_Suc_pos
apply (subst take_Suc_conv_app_nth)
using pos by (auto simp: rev_nth)
have ‹L ∈ set M›
using that inv L_def apply auto
by (metis bot_nat_0.not_eq_extremum diff_Suc_less in_set_dropI le_Suc_pos minus_eq nat.simps(3) nat_Suc_less_le_imp rev_nth)
moreover have ‹count_decided M ≥ get_level M (lit_of L)›
using count_decided_ge_get_level by blast
moreover have ‹get_level M⇩0 (lit_of L) = Suc highest› and ‹is_decided L›
using n_d pos unfolding L_def[symmetric]
by (auto simp: get_level_append_if split: if_splits)
moreover have ‹get_level M⇩0 (lit_of L) = get_level M (lit_of L)›
using n_d
apply (subst append_take_drop_id[symmetric, of M⇩0 j], subst (asm)append_take_drop_id[symmetric, of M⇩0 j])
using that ‹L ∈ set M› apply (auto simp del: append_take_drop_id simp: get_level_append_if
dest: defined_lit_no_dupD undefined_notin)
using defined_lit_no_dupD(1) undefined_notin by blast
ultimately show ?thesis
by auto
qed
find_theorems isa_bump_unset bump_heur
show ?decomp
unfolding find_decomp_wl_imp_def Let_def find_decomp_w_ns_def trail_conv_to_no_CS_def
get_pos_of_level_in_trail_def trail_conv_back_def
apply (refine_vcg 1 WHILEIT_rule[where R=‹measure (λ(_, M, _). length M)›]
isa_bump_unset_vmtf_tl[unfolded lit_of_hd_trail_def[symmetric], of _ 𝒜, THEN order_trans])
subgoal using length_M0 unfolding unat32_max_def by simp
subgoal by auto
subgoal by auto
subgoal using target by (auto simp: count_decided_ge_get_maximum_level)
subgoal by auto
subgoal by auto
subgoal using vm by auto
subgoal using lits unfolding literals_are_in_ℒ⇩i⇩n_trail_lit_of_mset by auto
subgoal by (rule count_dec_larger)
subgoal for target s j b M vm by simp
subgoal using length_M0 unfolding unat32_max_def by simp
subgoal for x s a ab aa bb
by (cases ‹drop a M⇩0›)
(auto simp: lit_of_hd_trail_def literals_are_in_ℒ⇩i⇩n_add_mset)
subgoal by auto
subgoal by (auto simp: drop_Suc drop_tl atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
subgoal by auto
subgoal for s a b aa ba vm x2 x1a x2a
using target
by (cases vm)
(auto intro!: isa_bump_unset_vmtf_tl atm_of_N drop_tl simp: lit_of_hd_trail_def)
subgoal for s a b aa ba x1 x2 x1a x2a
using lits by (auto intro: Lin_drop_tl simp: drop_Suc tl_drop)
subgoal by auto
subgoal by auto
subgoal for s a b aa ba x1 x2 x1a x2a
using lits by (auto intro: Lin_drop_tl)
subgoal by auto
subgoal by (rule highest)
subgoal by (rule ex_decomp) (assumption+, auto)
done
qed
lemma find_decomp_wl_imp_find_decomp_wl':
‹(uncurry2 (find_decomp_wl_imp 𝒜), uncurry2 (find_decomp_w_ns 𝒜)) ∈
[find_decomp_w_ns_pre 𝒜]⇩f Id ×⇩f Id ×⇩f Id → ⟨Id ×⇩f Id⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: find_decomp_w_ns_pre_def simp del: twl_st_of_wl.simps
intro!: find_decomp_wl_imp_le_find_decomp_wl')
lemma find_decomp_wl_imp_code_conbine_cond:
‹(λ((b, a), c). find_decomp_w_ns_pre 𝒜 ((b, a), c) ∧ a < count_decided b) = (λ((b, a), c).
find_decomp_w_ns_pre 𝒜 ((b, a), c))›
by (auto intro!: ext simp: find_decomp_w_ns_pre_def)
end