theory IsaSAT_Decide
imports IsaSAT_Setup IsaSAT_VMTF
begin
chapter ‹Decide›
lemma (in -)not_is_None_not_None: ‹¬is_None s ⟹ s ≠ None›
by (auto split: option.splits)
definition vmtf_find_next_undef_upd
:: ‹nat multiset ⇒ (nat,nat)ann_lits ⇒ vmtf_remove_int ⇒
(((nat,nat)ann_lits × vmtf_remove_int) × nat option)nres›
where
‹vmtf_find_next_undef_upd 𝒜 = (λM vm. do{
L ← vmtf_find_next_undef 𝒜 vm M;
RETURN ((M, update_next_search L vm), L)
})›
definition isa_vmtf_find_next_undef_upd
:: ‹trail_pol ⇒ isa_vmtf_remove_int ⇒
((trail_pol × isa_vmtf_remove_int) × nat option)nres›
where
‹isa_vmtf_find_next_undef_upd = (λM vm. do{
L ← isa_vmtf_find_next_undef vm M;
RETURN ((M, update_next_search L vm), L)
})›
lemma isa_vmtf_find_next_undef_vmtf_find_next_undef:
‹(uncurry isa_vmtf_find_next_undef_upd, uncurry (vmtf_find_next_undef_upd 𝒜)) ∈
trail_pol 𝒜 ×⇩r (Id ×⇩r distinct_atoms_rel 𝒜) →⇩f
⟨trail_pol 𝒜 ×⇩f (Id ×⇩r distinct_atoms_rel 𝒜) ×⇩f ⟨nat_rel⟩option_rel⟩nres_rel ›
unfolding isa_vmtf_find_next_undef_upd_def vmtf_find_next_undef_upd_def uncurry_def
defined_atm_def[symmetric]
apply (intro frefI nres_relI)
apply (refine_rcg isa_vmtf_find_next_undef_vmtf_find_next_undef[THEN fref_to_Down_curry])
subgoal by auto
subgoal by (auto simp: update_next_search_def split: prod.splits)
done
definition lit_of_found_atm where
‹lit_of_found_atm φ L = SPEC (λK. (L = None ⟶ K = None) ∧
(L ≠ None ⟶ K ≠ None ∧ atm_of (the K) = the L))›
definition find_undefined_atm
:: ‹nat multiset ⇒ (nat,nat) ann_lits ⇒ vmtf_remove_int ⇒
(((nat,nat) ann_lits × vmtf_remove_int) × nat option) nres›
where
‹find_undefined_atm 𝒜 M _ = SPEC(λ((M', vm), L).
(L ≠ None ⟶ Pos (the L) ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ undefined_atm M (the L)) ∧
(L = None ⟶ (∀K∈# ℒ⇩a⇩l⇩l 𝒜. defined_lit M K)) ∧ M = M' ∧ vm ∈ vmtf 𝒜 M)›
definition lit_of_found_atm_D_pre where
‹lit_of_found_atm_D_pre = (λ(φ, L). L ≠ None ⟶ (the L < length φ ∧ the L ≤ uint32_max div 2))›
definition find_unassigned_lit_wl_D_heur
:: ‹twl_st_wl_heur ⇒ (twl_st_wl_heur × nat literal option) nres›
where
‹find_unassigned_lit_wl_D_heur = (λ(M, N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena). do {
((M, vm), L) ← isa_vmtf_find_next_undef_upd M vm;
ASSERT(L ≠ None ⟶ get_saved_phase_heur_pre (the L) heur);
L ← lit_of_found_atm heur L;
RETURN ((M, N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena), L)
})›
lemma lit_of_found_atm_D_pre:
‹heuristic_rel 𝒜 heur ⟹ isasat_input_bounded 𝒜 ⟹ (L ≠ None ⟹ the L ∈# 𝒜) ⟹
L ≠ None ⟹ get_saved_phase_heur_pre (the L) heur›
by (auto simp: lit_of_found_atm_D_pre_def phase_saving_def heuristic_rel_def phase_save_heur_rel_def
get_saved_phase_heur_pre_def
atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff dest: bspec[of _ _ ‹Pos (the L)›])
definition find_unassigned_lit_wl_D_heur_pre where
‹find_unassigned_lit_wl_D_heur_pre S ⟷
(
∃T U.
(S, T) ∈ state_wl_l None ∧
(T, U) ∈ twl_st_l None ∧
twl_struct_invs U ∧
literals_are_ℒ⇩i⇩n (all_atms_st S) S ∧
get_conflict_wl S = None
)›
lemma vmtf_find_next_undef_upd:
‹(uncurry (vmtf_find_next_undef_upd 𝒜), uncurry (find_undefined_atm 𝒜)) ∈
[λ(M, vm). vm ∈ vmtf 𝒜 M]⇩f Id ×⇩f Id → ⟨Id ×⇩f Id ×⇩f ⟨nat_rel⟩option_rel⟩nres_rel›
unfolding vmtf_find_next_undef_upd_def find_undefined_atm_def
update_next_search_def uncurry_def
apply (intro frefI nres_relI)
apply (clarify)
apply (rule bind_refine_spec)
prefer 2
apply (rule vmtf_find_next_undef_ref[simplified])
by (auto intro!: RETURN_SPEC_refine simp: image_image defined_atm_def[symmetric])
lemma find_unassigned_lit_wl_D'_find_unassigned_lit_wl_D:
‹(find_unassigned_lit_wl_D_heur, find_unassigned_lit_wl) ∈
[find_unassigned_lit_wl_D_heur_pre]⇩f
twl_st_heur''' r → ⟨{((T, L), (T', L')). (T, T') ∈ twl_st_heur''' r ∧ L = L' ∧
(L ≠ None ⟶ undefined_lit (get_trail_wl T') (the L) ∧ the L ∈# ℒ⇩a⇩l⇩l (all_atms_st T')) ∧
get_conflict_wl T' = None}⟩nres_rel›
proof -
have [simp]: ‹undefined_lit M (Pos (atm_of y)) = undefined_lit M y› for M y
by (auto simp: defined_lit_map)
have [simp]: ‹defined_atm M (atm_of y) = defined_lit M y› for M y
by (auto simp: defined_lit_map defined_atm_def)
have ID_R: ‹Id ×⇩r ⟨Id⟩option_rel = Id›
by auto
have atms: ‹atms_of (ℒ⇩a⇩l⇩l (all_atms_st (M, N, D, NE, UE, NS, US, WS, Q))) =
atms_of_mm (mset `# init_clss_lf N) ∪
atms_of_mm NE ∪ atms_of_mm NS ∧ D = None› (is ?A) and
atms_2: ‹set_mset (ℒ⇩a⇩l⇩l (all_atms N (NE + UE + NS + US))) = set_mset (ℒ⇩a⇩l⇩l (all_atms N (NE+NS)))› (is ?B) and
atms_3: ‹y ∈ atms_of_ms ((λx. mset (fst x)) ` set_mset (ran_m N)) ⟹
y ∉ atms_of_mm NE ⟹ y ∉ atms_of_mm NS ⟹
y ∈ atms_of_ms ((λx. mset (fst x)) ` {a. a ∈# ran_m N ∧ snd a})› (is ‹?C1 ⟹ ?C2 ⟹?C3 ⟹ ?C›)
if inv: ‹find_unassigned_lit_wl_D_heur_pre (M, N, D, NE, UE, NS, US, WS, Q)›
for M N D NE UE WS Q y NS US
proof -
obtain T U where
S_T: ‹((M, N, D, NE, UE, NS, US, WS, Q), T) ∈ state_wl_l None› and
T_U: ‹(T, U) ∈ twl_st_l None› and
inv: ‹twl_struct_invs U› and
𝒜⇩i⇩n : ‹literals_are_ℒ⇩i⇩n (all_atms_st (M, N, D, NE, UE, NS, US, WS, Q)) (M, N, D, NE, UE, NS, US, WS, Q)› and
confl: ‹get_conflict_wl (M, N, D, NE, UE, NS, US, WS, Q) = None›
using inv unfolding find_unassigned_lit_wl_D_heur_pre_def
apply - apply normalize_goal+
by blast
have ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of U)› and
unit: ‹entailed_clss_inv U›
using inv unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then show ?A
using 𝒜⇩i⇩n confl S_T T_U unfolding is_ℒ⇩a⇩l⇩l_alt_def state_wl_l_def twl_st_l_def
literals_are_ℒ⇩i⇩n_def all_atms_def all_lits_def
apply -
apply (subst (asm) all_clss_l_ran_m[symmetric], subst (asm) image_mset_union)+
apply (subst all_clss_l_ran_m[symmetric], subst image_mset_union)
by (auto simp: cdcl⇩W_restart_mset.no_strange_atm_def entailed_clss_inv.simps
mset_take_mset_drop_mset mset_take_mset_drop_mset' atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n all_lits_def
clauses_def all_lits_of_mm_union atm_of_all_lits_of_mm
simp del: entailed_clss_inv.simps)
then show ?B and ‹?C1 ⟹ ?C2 ⟹ ?C3 ⟹ ?C›
apply -
unfolding atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n all_atms_def all_lits_def
apply (subst (asm) all_clss_l_ran_m[symmetric], subst (asm) image_mset_union)+
apply (subst all_clss_l_ran_m[symmetric], subst image_mset_union)+
by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n all_atms_def all_lits_def in_all_lits_of_mm_ain_atms_of_iff
all_lits_of_mm_union atms_of_def ℒ⇩a⇩l⇩l_union image_Un atm_of_eq_atm_of
atm_of_all_lits_of_mm atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
qed
define unassigned_atm where
‹unassigned_atm S L ≡ ∃ M N D NE UE NS US WS Q.
S = (M, N, D, NE, UE, NS, US, WS, Q) ∧
(L ≠ None ⟶
undefined_lit M (the L) ∧ the L ∈# ℒ⇩a⇩l⇩l (all_atms_st S) ∧
atm_of (the L) ∈ atms_of_mm (mset `# ran_mf N + (NE+UE) + (NS+US))) ∧
(L = None ⟶ (∄L'. undefined_lit M L' ∧
atm_of L' ∈ atms_of_mm (mset `# ran_mf N + (NE+UE) + (NS+US))))›
for L :: ‹nat literal option› and S :: ‹nat twl_st_wl›
have unassigned_atm_alt_def:
‹unassigned_atm S L ⟷ (∃ M N D NE UE NS US WS Q.
S = (M, N, D, NE, UE, NS, US, WS, Q) ∧
(L ≠ None ⟶
undefined_lit M (the L) ∧ the L ∈# ℒ⇩a⇩l⇩l (all_atms_st S) ∧
atm_of (the L) ∈# all_atms_st S) ∧
(L = None ⟶ (∄L'. undefined_lit M L' ∧
atm_of L' ∈# all_atms_st S)))›
for L :: ‹nat literal option› and S :: ‹nat twl_st_wl›
unfolding find_unassigned_lit_wl_def RES_RES_RETURN_RES unassigned_atm_def
RES_RES_RETURN_RES all_lits_def in_all_lits_of_mm_ain_atms_of_iff
in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n in_set_all_atms_iff
by (cases S) auto
have find_unassigned_lit_wl_D_alt_def:
‹find_unassigned_lit_wl S = do {
L ← SPEC(unassigned_atm S);
L ← RES {L, map_option uminus L};
SPEC(λ((M, N, D, NE, UE, WS, Q), L').
S = (M, N, D, NE, UE, WS, Q) ∧ L = L')
}› for S
unfolding find_unassigned_lit_wl_def RES_RES_RETURN_RES unassigned_atm_def
RES_RES_RETURN_RES all_lits_def in_all_lits_of_mm_ain_atms_of_iff
in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n in_set_all_atms_iff
by (cases S) auto
have isa_vmtf_find_next_undef_upd:
‹isa_vmtf_find_next_undef_upd (a, aa, ab, ac, ad, b)
((aj, ak, al, am, bb), an, bc)
≤ ⇓ {(((M, vm), A), L). A = map_option atm_of L ∧
unassigned_atm (bt, bu, bv, bw, bx, by, bz, baa, bab) L ∧
vm ∈ isa_vmtf (all_atms_st (bt, bu, bv, bw, bx, by, bz, baa, bab)) bt ∧
(L ≠ None ⟶ the A ∈# all_atms_st (bt, bu, bv, bw, bx, by, bz, baa, bab)) ∧
(M, bt) ∈ trail_pol (all_atms_st (bt, bu, bv, bw, bx, by, bz, baa, bab))}
(SPEC (unassigned_atm (bt, bu, bv, bw, bx, by, bz, baa, bab)))›
(is ‹_ ≤ ⇓ ?find _›)
if
pre: ‹find_unassigned_lit_wl_D_heur_pre (bt, bu, bv, bw, bx, by, bz, baa, bab)› and
T: ‹(((a, aa, ab, ac, ad, b), ae, (af, ag, ba), ah, ai,
((aj, ak, al, am, bb), an, bc), ao, (aq, bd), ar, as,
(at, au, av, aw, be), heur, bo, bp, bq, br, bs),
bt, bu, bv, bw, bx, by, bz, baa, bab)
∈ twl_st_heur› and
‹r =
length
(get_clauses_wl_heur
((a, aa, ab, ac, ad, b), ae, (af, ag, ba), ah, ai,
((aj, ak, al, am, bb), an, bc), ao, (aq, bd), ar, as,
(at, au, av, aw, be), heur, bo, bp, bq, br, bs))›
for a aa ab ac ad b ae af ag ba ah ai aj ak al am bb an bc ao ap aq bd ar as at
au av aw be ax ay az bf bg bh bi bj bk bl bm bn bo bp bq br bs bt bu bv
bw bx "by" bz heur baa bab
proof -
let ?𝒜 = ‹all_atms_st (bt, bu, bv, bw, bx, by, bz, baa, bab)›
have pol:
‹((a, aa, ab, ac, ad, b), bt) ∈ trail_pol (all_atms bu (bw + bx + by + bz))›
using that by (cases bz; auto simp: twl_st_heur_def all_atms_def[symmetric])
obtain vm0 where
vm0: ‹((an, bc), vm0) ∈ distinct_atoms_rel (all_atms bu (bw + bx + by + bz))› and
vm: ‹((aj, ak, al, am, bb), vm0) ∈ vmtf (all_atms bu (bw + bx + by + bz)) bt›
using T by (cases bz; auto simp: twl_st_heur_def all_atms_def[symmetric] isa_vmtf_def)
have [intro]:
‹Multiset.Ball (ℒ⇩a⇩l⇩l (all_atms bu (bw + bx + by + bz))) (defined_lit bt) ⟹
atm_of L' ∈# all_atms bu (bw + bx + by + bz) ⟹
undefined_lit bt L'⟹ False› for L'
by (auto simp: atms_of_ms_def
all_lits_of_mm_union ran_m_def all_lits_of_mm_add_mset ℒ⇩a⇩l⇩l_union
eq_commute[of _ ‹the (fmlookup _ _)›] ℒ⇩a⇩l⇩l_atm_of_all_lits_of_m
atms_of_def ℒ⇩a⇩l⇩l_add_mset
dest!: multi_member_split
)
show ?thesis
apply (rule order.trans)
apply (rule isa_vmtf_find_next_undef_vmtf_find_next_undef[of ?𝒜, THEN fref_to_Down_curry,
of _ _ bt ‹((aj, ak, al, am, bb), vm0)›])
subgoal by fast
subgoal
using pol vm0 by (auto simp: twl_st_heur_def all_atms_def[symmetric])
apply (rule order.trans)
apply (rule ref_two_step')
apply (rule vmtf_find_next_undef_upd[THEN fref_to_Down_curry, of ?𝒜 bt ‹((aj, ak, al, am, bb), vm0)›])
subgoal using vm by (auto simp: all_atms_def)
subgoal by auto
subgoal using vm vm0 pre
apply (auto 5 0 simp: find_undefined_atm_def unassigned_atm_alt_def conc_fun_RES all_atms_def[symmetric]
mset_take_mset_drop_mset' atms_2 defined_atm_def
intro!: RES_refine intro: isa_vmtfI)
apply (auto intro: isa_vmtfI simp: defined_atm_def atms_2)
apply (rule_tac x = ‹Some (Pos y)› in exI)
apply (auto intro: isa_vmtfI simp: defined_atm_def atms_2 in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n
in_set_all_atms_iff atms_3)
done
done
qed
have lit_of_found_atm: ‹lit_of_found_atm ao' x2a
≤ ⇓ {(L, L'). L = L' ∧ map_option atm_of L = x2a}
(RES {L, map_option uminus L})›
if
‹find_unassigned_lit_wl_D_heur_pre (bt, bu, bv, bw, bx, by, bz, baa, bab)› and
‹(((a, aa, ab, ac, ad, b), ae, (af, ag, ba), ah, ai,
((aj, ak, al, am, bb), an, bc), ao, (aq, bd), ar, as,
(at, au, av, aw, be), heur, bo, bp, bq, br, bs),
bt, bu, bv, bw, bx, by, bz, baa, bab)
∈ twl_st_heur› and
‹r =
length
(get_clauses_wl_heur
((a, aa, ab, ac, ad, b), ae, (af, ag, ba), ah, ai,
((aj, ak, al, am, bb), an, bc), ao, (aq, bd), ar, as,
(at, au, av, aw, be), heur, bo, bp, bq, br, bs))› and
‹(x, L) ∈ ?find bt bu bv bw bx by bz baa bab› and
‹x1 = (x1a, x2)› and
‹x = (x1, x2a)›
for a aa ab ac ad b ae af ag ba ah ai aj ak al am bb an bc ao ap aq bd ar as at
au av aw be ax ay az bf bg bh bi bj bk bl bm bn bo bp bq br bs bt bu bv
bw bx "by" bz x L x1 x1a x2 x2a heur baa bab ao'
proof -
show ?thesis
using that unfolding lit_of_found_atm_def
by (auto simp: atm_of_eq_atm_of twl_st_heur_def intro!: RES_refine)
qed
show ?thesis
unfolding find_unassigned_lit_wl_D_heur_def find_unassigned_lit_wl_D_alt_def find_undefined_atm_def
ID_R
apply (intro frefI nres_relI)
apply clarify
apply refine_vcg
apply (rule isa_vmtf_find_next_undef_upd; assumption)
subgoal
by (rule lit_of_found_atm_D_pre)
(auto simp add: twl_st_heur_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff Ball_def image_image
mset_take_mset_drop_mset' atms all_atms_def[symmetric] unassigned_atm_def
simp del: twl_st_of_wl.simps dest!: atms intro!: RETURN_RES_refine)
apply (rule lit_of_found_atm; assumption)
subgoal for a aa ab ac ad b ae af ag ba ah ai aj ak al am bb an bc ao ap aq bd ar
as at au av aw ax ay az be bf bg bh bi bj bk bl bm bn bo bp bq br bs
bt bu bv bw bx _ _ _ _ _ _ _ "by" bz ca cb cc cd ce cf cg ch ci _ _ x L x1 x1a x2 x2a La Lb
by (cases L)
(clarsimp_all simp: twl_st_heur_def unassigned_atm_def atm_of_eq_atm_of uminus_𝒜⇩i⇩n_iff
simp del: twl_st_of_wl.simps dest!: atms intro!: RETURN_RES_refine;
auto simp: atm_of_eq_atm_of uminus_𝒜⇩i⇩n_iff)+
done
qed
definition lit_of_found_atm_D
:: ‹bool list ⇒ nat option ⇒ (nat literal option)nres› where
‹lit_of_found_atm_D = (λ(φ::bool list) L. do{
case L of
None ⇒ RETURN None
| Some L ⇒ do {
ASSERT (L<length φ);
if φ!L then RETURN (Some (Pos L)) else RETURN (Some (Neg L))
}
})›
lemma lit_of_found_atm_D_lit_of_found_atm:
‹(uncurry lit_of_found_atm_D, uncurry lit_of_found_atm) ∈
[lit_of_found_atm_D_pre]⇩f Id ×⇩f Id → ⟨Id⟩nres_rel›
apply (intro frefI nres_relI)
unfolding lit_of_found_atm_D_def lit_of_found_atm_def
by (auto split: option.splits if_splits simp: pw_le_iff refine_pw_simps lit_of_found_atm_D_pre_def)
definition decide_lit_wl_heur :: ‹nat literal ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹decide_lit_wl_heur = (λL' (M, N, D, Q, W, vmtf, clvls, cach, lbd, outl, stats, fema, sema). do {
ASSERT(isa_length_trail_pre M);
let j = isa_length_trail M;
ASSERT(cons_trail_Decided_tr_pre (L', M));
RETURN (cons_trail_Decided_tr L' M, N, D, j, W, vmtf, clvls, cach, lbd, outl, incr_decision stats,
fema, sema)})›
definition mop_get_saved_phase_heur_st :: ‹nat ⇒ twl_st_wl_heur ⇒ bool nres› where
‹mop_get_saved_phase_heur_st =
(λL (M', N', D', Q', W', vm, clvls, cach, lbd, outl, stats, heur, vdom, avdom, lcount, opts,
old_arena).
mop_get_saved_phase_heur L heur)›
definition decide_wl_or_skip_D_heur
:: ‹twl_st_wl_heur ⇒ (bool × twl_st_wl_heur) nres›
where
‹decide_wl_or_skip_D_heur S = (do {
(S, L) ← find_unassigned_lit_wl_D_heur S;
case L of
None ⇒ RETURN (True, S)
| Some L ⇒ do {
T ← decide_lit_wl_heur L S;
RETURN (False, T)}
})
›
lemma decide_wl_or_skip_D_heur_decide_wl_or_skip_D:
‹(decide_wl_or_skip_D_heur, decide_wl_or_skip) ∈ twl_st_heur''' r →⇩f ⟨bool_rel ×⇩f twl_st_heur''' r⟩ nres_rel›
proof -
have [simp]:
‹rev (cons_trail_Decided L M) = rev M @ [Decided L]›
‹no_dup (cons_trail_Decided L M) = no_dup (Decided L # M)›
‹isa_vmtf 𝒜 (cons_trail_Decided L M) = isa_vmtf 𝒜 (Decided L # M)›
for M L 𝒜
by (auto simp: cons_trail_Decided_def)
have final: ‹decide_lit_wl_heur xb x1a
≤ SPEC
(λT. do {
RETURN (False, T)}
≤ SPEC
(λc. (c, False, decide_lit_wl x'a x1)
∈ bool_rel ×⇩f twl_st_heur''' r))›
if
‹(x, y) ∈ twl_st_heur''' r› and
‹(xa, x')
∈ {((T, L), T', L').
(T, T') ∈ twl_st_heur''' r ∧
L = L' ∧
(L ≠ None ⟶
undefined_lit (get_trail_wl T') (the L) ∧
the L ∈# ℒ⇩a⇩l⇩l (all_atms_st T')) ∧
get_conflict_wl T' = None}› and
st:
‹x' = (x1, x2)›
‹xa = (x1a, x2a)›
‹x2a = Some xb›
‹x2 = Some x'a› and
‹(xb, x'a) ∈ nat_lit_lit_rel›
for x y xa x' x1 x2 x1a x2a xb x'a
proof -
show ?thesis
unfolding decide_lit_wl_heur_def
decide_lit_wl_def
apply (cases x1a)
apply refine_vcg
subgoal
by (rule isa_length_trail_pre[of _ ‹get_trail_wl x1› ‹all_atms_st x1›])
(use that(2) in ‹auto simp: twl_st_heur_def st all_atms_def[symmetric]›)
subgoal
by (rule cons_trail_Decided_tr_pre[of _ ‹get_trail_wl x1› ‹all_atms_st x1›])
(use that(2) in ‹auto simp: twl_st_heur_def st all_atms_def[symmetric]›)
subgoal
using that(2) unfolding cons_trail_Decided_def[symmetric] st
apply (auto simp: twl_st_heur_def)[]
apply (clarsimp simp add: twl_st_heur_def all_atms_def[symmetric]
isa_length_trail_length_u[THEN fref_to_Down_unRET_Id] out_learned_def
intro!: cons_trail_Decided_tr[THEN fref_to_Down_unRET_uncurry]
isa_vmtf_consD2)
by (auto simp add: twl_st_heur_def all_atms_def[symmetric]
isa_length_trail_length_u[THEN fref_to_Down_unRET_Id] out_learned_def
intro!: cons_trail_Decided_tr[THEN fref_to_Down_unRET_uncurry]
isa_vmtf_consD2)
done
qed
have decide_wl_or_skip_alt_def: ‹decide_wl_or_skip S = (do {
ASSERT(decide_wl_or_skip_pre S);
(S, L) ← find_unassigned_lit_wl S;
case L of
None ⇒ RETURN (True, S)
| Some L ⇒ RETURN (False, decide_lit_wl L S)
})› for S
unfolding decide_wl_or_skip_def by auto
show ?thesis
supply [[goals_limit=1]]
unfolding decide_wl_or_skip_D_heur_def decide_wl_or_skip_alt_def decide_wl_or_skip_pre_def
decide_l_or_skip_pre_def twl_st_of_wl.simps[symmetric]
apply (intro nres_relI frefI same_in_Id_option_rel)
apply (refine_vcg find_unassigned_lit_wl_D'_find_unassigned_lit_wl_D[of r, THEN fref_to_Down])
subgoal for x y
unfolding decide_wl_or_skip_pre_def find_unassigned_lit_wl_D_heur_pre_def
decide_wl_or_skip_pre_def decide_l_or_skip_pre_def decide_or_skip_pre_def
apply normalize_goal+
apply (rule_tac x = xa in exI)
apply (rule_tac x = xb in exI)
apply auto
done
apply (rule same_in_Id_option_rel)
subgoal by (auto simp del: simp: twl_st_heur_def)
subgoal by (auto simp del: simp: twl_st_heur_def)
apply (rule final; assumption?)
done
qed
lemma bind_triple_unfold:
‹do {
((M, vm), L) ← (P :: _ nres);
f ((M, vm), L)
} =
do {
x ← P;
f x
}›
by (intro bind_cong) auto
definition decide_wl_or_skip_D_heur' where
‹decide_wl_or_skip_D_heur' = (λ(M, N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena). do {
((M, vm), L) ← isa_vmtf_find_next_undef_upd M vm;
ASSERT(L ≠ None ⟶ get_saved_phase_heur_pre (the L) heur);
case L of
None ⇒ RETURN (True, (M, N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena))
| Some L ⇒ do {
b ← mop_get_saved_phase_heur L heur;
let L = (if b then Pos L else Neg L);
T ← decide_lit_wl_heur L (M, N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena);
RETURN (False, T)
}
})
›
lemma decide_wl_or_skip_D_heur'_decide_wl_or_skip_D_heur:
‹decide_wl_or_skip_D_heur' S ≤ ⇓Id (decide_wl_or_skip_D_heur S)›
proof -
have [iff]:
‹{K. (∃y. K = Some y) ∧ atm_of (the K) = x2d} = {Some (Pos x2d), Some (Neg x2d)}› for x2d
apply (auto simp: atm_of_eq_atm_of)
apply (case_tac y)
apply auto
done
show ?thesis
apply (cases S, simp only:)
unfolding decide_wl_or_skip_D_heur_def find_unassigned_lit_wl_D_heur_def
nres_monad3 prod.case decide_wl_or_skip_D_heur'_def
apply (subst (3) bind_triple_unfold[symmetric])
unfolding decide_wl_or_skip_D_heur_def find_unassigned_lit_wl_D_heur_def
nres_monad3 prod.case lit_of_found_atm_def mop_get_saved_phase_heur_def
apply refine_vcg
subgoal by fast
subgoal
by (auto split: option.splits simp: bind_RES)
done
qed
lemma decide_wl_or_skip_D_heur'_decide_wl_or_skip_D_heur2:
‹(decide_wl_or_skip_D_heur', decide_wl_or_skip_D_heur) ∈ Id →⇩f ⟨Id⟩nres_rel›
by (intro frefI nres_relI) (use decide_wl_or_skip_D_heur'_decide_wl_or_skip_D_heur in auto)
end