theory IsaSAT_Backtrack
imports IsaSAT_Setup IsaSAT_VMTF IsaSAT_Rephase
begin
chapter ‹Backtrack›
text ‹
The backtrack function is highly complicated and tricky to maintain.
›
section ‹Backtrack with direct extraction of literal if highest level›
paragraph ‹Empty conflict›
definition (in -) empty_conflict_and_extract_clause
:: ‹(nat,nat) ann_lits ⇒ nat clause ⇒ nat clause_l ⇒
(nat clause option × nat clause_l × nat) nres›
where
‹empty_conflict_and_extract_clause M D outl =
SPEC(λ(D, C, n). D = None ∧ mset C = mset outl ∧ C!0 = outl!0 ∧
(length C > 1 ⟶ highest_lit M (mset (tl C)) (Some (C!1, get_level M (C!1)))) ∧
(length C > 1 ⟶ n = get_level M (C!1)) ∧
(length C = 1 ⟶ n = 0)
)›
definition empty_conflict_and_extract_clause_heur_inv where
‹empty_conflict_and_extract_clause_heur_inv M outl =
(λ(E, C, i). mset (take i C) = mset (take i outl) ∧
length C = length outl ∧ C ! 0 = outl ! 0 ∧ i ≥ 1 ∧ i ≤ length outl ∧
(1 < length (take i C) ⟶
highest_lit M (mset (tl (take i C)))
(Some (C ! 1, get_level M (C ! 1)))))›
definition empty_conflict_and_extract_clause_heur ::
"nat multiset ⇒ (nat, nat) ann_lits
⇒ lookup_clause_rel
⇒ nat literal list ⇒ (_ × nat literal list × nat) nres"
where
‹empty_conflict_and_extract_clause_heur 𝒜 M D outl = do {
let C = replicate (length outl) (outl!0);
(D, C, _) ← WHILE⇩T⇗empty_conflict_and_extract_clause_heur_inv M outl⇖
(λ(D, C, i). i < length_uint32_nat outl)
(λ(D, C, i). do {
ASSERT(i < length outl);
ASSERT(i < length C);
ASSERT(lookup_conflict_remove1_pre (outl ! i, D));
let D = lookup_conflict_remove1 (outl ! i) D;
let C = C[i := outl ! i];
ASSERT(C!i ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ C!1 ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ 1 < length C);
let C = (if get_level M (C!i) > get_level M (C!1) then swap C 1 i else C);
ASSERT(i+1 ≤ uint32_max);
RETURN (D, C, i+1)
})
(D, C, 1);
ASSERT(length outl ≠ 1 ⟶ length C > 1);
ASSERT(length outl ≠ 1 ⟶ C!1 ∈# ℒ⇩a⇩l⇩l 𝒜);
RETURN ((True, D), C, if length outl = 1 then 0 else get_level M (C!1))
}›
lemma empty_conflict_and_extract_clause_heur_empty_conflict_and_extract_clause:
assumes
D: ‹D = mset (tl outl)› and
outl: ‹outl ≠ []› and
dist: ‹distinct outl› and
lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset outl)› and
DD': ‹(D', D) ∈ lookup_clause_rel 𝒜› and
consistent: ‹¬ tautology (mset outl)› and
bounded: ‹isasat_input_bounded 𝒜›
shows
‹empty_conflict_and_extract_clause_heur 𝒜 M D' outl ≤ ⇓ (option_lookup_clause_rel 𝒜 ×⇩r Id ×⇩r Id)
(empty_conflict_and_extract_clause M D outl)›
proof -
have size_out: ‹size (mset outl) ≤ 1 + uint32_max div 2›
using simple_clss_size_upper_div2[OF bounded lits _ consistent]
‹distinct outl› by auto
have empty_conflict_and_extract_clause_alt_def:
‹empty_conflict_and_extract_clause M D outl = do {
(D', outl') ← SPEC (λ(E, F). E = {#} ∧ mset F = D);
SPEC
(λ(D, C, n).
D = None ∧
mset C = mset outl ∧
C ! 0 = outl ! 0 ∧
(1 < length C ⟶
highest_lit M (mset (tl C)) (Some (C ! 1, get_level M (C ! 1)))) ∧
(1 < length C ⟶ n = get_level M (C ! 1)) ∧ (length C = 1 ⟶ n = 0))
}› for M D outl
unfolding empty_conflict_and_extract_clause_def RES_RES2_RETURN_RES
by (auto simp: ex_mset)
define I where
‹I ≡ λ(E, C, i). mset (take i C) = mset (take i outl) ∧
(E, D - mset (take i outl)) ∈ lookup_clause_rel 𝒜 ∧
length C = length outl ∧ C ! 0 = outl ! 0 ∧ i ≥ 1 ∧ i ≤ length outl ∧
(1 < length (take i C) ⟶
highest_lit M (mset (tl (take i C)))
(Some (C ! 1, get_level M (C ! 1))))›
have I0: ‹I (D', replicate (length outl) (outl ! 0), 1)›
using assms by (cases outl) (auto simp: I_def)
have [simp]: ‹ba ≥ 1 ⟹ mset (tl outl) - mset (take ba outl) = mset ((drop ba outl))›
for ba
apply (subst append_take_drop_id[of ‹ba - 1›, symmetric])
using dist
unfolding mset_append
by (cases outl; cases ba)
(auto simp: take_tl drop_Suc[symmetric] remove_1_mset_id_iff_notin dest: in_set_dropD)
have empty_conflict_and_extract_clause_heur_inv:
‹empty_conflict_and_extract_clause_heur_inv M outl
(D', replicate (length outl) (outl ! 0), 1)›
using assms
unfolding empty_conflict_and_extract_clause_heur_inv_def
by (cases outl) auto
have I0: ‹I (D', replicate (length outl) (outl ! 0), 1)›
using assms
unfolding I_def
by (cases outl) auto
have
C1_L: ‹aa[ba := outl ! ba] ! 1 ∈# ℒ⇩a⇩l⇩l 𝒜› (is ?A1inL) and
ba_le: ‹ba + 1 ≤ uint32_max› (is ?ba_le) and
I_rec: ‹I (lookup_conflict_remove1 (outl ! ba) a,
if get_level M (aa[ba := outl ! ba] ! 1)
< get_level M (aa[ba := outl ! ba] ! ba)
then swap (aa[ba := outl ! ba]) 1 ba
else aa[ba := outl ! ba],
ba + 1)› (is ?I) and
inv: ‹empty_conflict_and_extract_clause_heur_inv M outl
(lookup_conflict_remove1 (outl ! ba) a,
if get_level M (aa[ba := outl ! ba] ! 1)
< get_level M (aa[ba := outl ! ba] ! ba)
then swap (aa[ba := outl ! ba]) 1 ba
else aa[ba := outl ! ba],
ba + 1)› (is ?inv)
if
‹empty_conflict_and_extract_clause_heur_inv M outl s› and
I: ‹I s› and
‹case s of (D, C, i) ⇒ i < length_uint32_nat outl› and
st:
‹s = (a, b)›
‹b = (aa, ba)› and
ba_le: ‹ba < length outl› and
‹ba < length aa› and
‹lookup_conflict_remove1_pre (outl ! ba, a)›
for s a b aa ba
proof -
have
mset_aa: ‹mset (take ba aa) = mset (take ba outl)› and
aD: ‹(a, D - mset (take ba outl)) ∈ lookup_clause_rel 𝒜› and
l_aa_outl: ‹length aa = length outl› and
aa0: ‹aa ! 0 = outl ! 0› and
ba_ge1: ‹1 ≤ ba› and
ba_lt: ‹ba ≤ length outl› and
highest: ‹1 < length (take ba aa) ⟶
highest_lit M (mset (tl (take ba aa)))
(Some (aa ! 1, get_level M (aa ! 1)))›
using I unfolding st I_def prod.case
by auto
have set_aa_outl: ‹set (take ba aa) = set (take ba outl)›
using mset_aa by (blast dest: mset_eq_setD)
show ?ba_le
using ba_le assms size_out
by (auto simp: uint32_max_def)
have ba_ge1_aa_ge: ‹ba > 1 ⟹ aa ! 1 ∈ set (take ba aa)›
using ba_ge1 ba_le l_aa_outl
by (auto simp: in_set_take_conv_nth intro!: bex_lessI[of _ ‹Suc 0›])
then have ‹aa[ba := outl ! ba] ! 1 ∈ set outl›
using ba_le l_aa_outl ba_ge1
unfolding mset_aa in_multiset_in_set[symmetric]
by (cases ‹ba > 1›)
(auto simp: mset_aa dest: in_set_takeD)
then show ?A1inL
using literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l[OF lits, of ‹aa[ba := outl ! ba] ! 1›] by auto
define aa2 where ‹aa2 ≡ tl (tl (take ba aa))›
have tl_take_nth_con: ‹tl (take ba aa) = aa ! Suc 0 # aa2› if ‹ba > Suc 0›
using ba_le ba_ge1 that l_aa_outl unfolding aa2_def
by (cases aa; cases ‹tl aa›; cases ba; cases ‹ba - 1›)
auto
have no_tauto_nth: ‹ i < length outl ⟹ - outl ! ba = outl ! i ⟹ False› for i
using consistent ba_le nth_mem
by (force simp: tautology_decomp' uminus_lit_swap)
have outl_ba__L: ‹outl ! ba ∈# ℒ⇩a⇩l⇩l 𝒜›
using ba_le literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l[OF lits, of ‹outl ! ba›] by auto
have ‹(lookup_conflict_remove1 (outl ! ba) a,
remove1_mset (outl ! ba) (D -(mset (take ba outl)))) ∈ lookup_clause_rel 𝒜›
by (rule lookup_conflict_remove1[THEN fref_to_Down_unRET_uncurry])
(use ba_ge1 ba_le aD outl_ba__L in
‹auto simp: D in_set_drop_conv_nth image_image dest: no_tauto_nth
intro!: bex_geI[of _ ba]›)
then have ‹(lookup_conflict_remove1 (outl ! ba) a,
D - mset (take (Suc ba) outl))
∈ lookup_clause_rel 𝒜›
using aD ba_le ba_ge1 ba_ge1_aa_ge aa0
by (auto simp: take_Suc_conv_app_nth)
moreover have ‹1 < length
(take (ba + 1)
(if get_level M (aa[ba := outl ! ba] ! 1)
< get_level M (aa[ba := outl ! ba] ! ba)
then swap (aa[ba := outl ! ba]) 1 ba
else aa[ba := outl ! ba])) ⟶
highest_lit M
(mset
(tl (take (ba + 1)
(if get_level M (aa[ba := outl ! ba] ! 1)
< get_level M (aa[ba := outl ! ba] ! ba)
then swap (aa[ba := outl ! ba]) 1 ba
else aa[ba := outl ! ba]))))
(Some
((if get_level M (aa[ba := outl ! ba] ! 1)
< get_level M (aa[ba := outl ! ba] ! ba)
then swap (aa[ba := outl ! ba]) 1 ba
else aa[ba := outl ! ba]) !
1,
get_level M
((if get_level M (aa[ba := outl ! ba] ! 1)
< get_level M (aa[ba := outl ! ba] ! ba)
then swap (aa[ba := outl ! ba]) 1 ba
else aa[ba := outl ! ba]) !
1)))›
using highest ba_le ba_ge1
by (cases ‹ba = Suc 0›)
(auto simp: highest_lit_def take_Suc_conv_app_nth l_aa_outl
get_maximum_level_add_mset swap_nth_relevant max_def take_update_swap
swap_only_first_relevant tl_update_swap mset_update nth_tl
get_maximum_level_remove_non_max_lvl tl_take_nth_con
aa2_def[symmetric])
moreover have ‹mset
(take (ba + 1)
(if get_level M (aa[ba := outl ! ba] ! 1)
< get_level M (aa[ba := outl ! ba] ! ba)
then swap (aa[ba := outl ! ba]) 1 ba
else aa[ba := outl ! ba])) =
mset (take (ba + 1) outl)›
using ba_le ba_ge1 ba_ge1_aa_ge aa0
unfolding mset_aa
by (cases ‹ba = 1›)
(auto simp: take_Suc_conv_app_nth l_aa_outl
take_swap_relevant swap_only_first_relevant mset_aa set_aa_outl
mset_update add_mset_remove_trivial_If)
ultimately show ?I
using ba_ge1 ba_le
unfolding I_def prod.simps
by (auto simp: l_aa_outl aa0)
then show ?inv
unfolding empty_conflict_and_extract_clause_heur_inv_def I_def
by (auto simp: l_aa_outl aa0)
qed
have mset_tl_out: ‹mset (tl outl) - mset outl = {#}›
by (cases outl) auto
have H1: ‹WHILE⇩T⇗empty_conflict_and_extract_clause_heur_inv M outl⇖
(λ(D, C, i). i < length_uint32_nat outl)
(λ(D, C, i). do {
_ ← ASSERT (i < length outl);
_ ← ASSERT (i < length C);
_ ← ASSERT (lookup_conflict_remove1_pre (outl ! i, D));
_ ← ASSERT
(C[i := outl ! i] ! i ∈# ℒ⇩a⇩l⇩l 𝒜 ∧
C[i := outl ! i] ! 1 ∈# ℒ⇩a⇩l⇩l 𝒜 ∧
1 < length (C[i := outl ! i]));
_ ← ASSERT (i + 1 ≤ uint32_max);
RETURN
(lookup_conflict_remove1 (outl ! i) D,
if get_level M (C[i := outl ! i] ! 1)
< get_level M (C[i := outl ! i] ! i)
then swap (C[i := outl ! i]) 1 i
else C[i := outl ! i],
i + 1)
})
(D', replicate (length outl) (outl ! 0), 1)
≤ ⇓ {((E, C, n), (E', F')). (E, E') ∈ lookup_clause_rel 𝒜 ∧ mset C = mset outl ∧
C ! 0 = outl ! 0 ∧
(1 < length C ⟶
highest_lit M (mset (tl C)) (Some (C ! 1, get_level M (C ! 1)))) ∧
n = length outl ∧
I (E, C, n)}
(SPEC (λ(E, F). E = {#} ∧ mset F = D))›
unfolding conc_fun_RES
apply (refine_vcg WHILEIT_rule_stronger_inv_RES[where R = ‹measure (λ(_, _, i). length outl - i)› and
I' = ‹I›])
subgoal by auto
subgoal by (rule empty_conflict_and_extract_clause_heur_inv)
subgoal by (rule I0)
subgoal using assms by (cases outl; auto)
subgoal
by (auto simp: I_def)
subgoal for s a b aa ba
using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l lits
unfolding lookup_conflict_remove1_pre_def prod.simps
by (auto simp: I_def empty_conflict_and_extract_clause_heur_inv_def
lookup_clause_rel_def D atms_of_def)
subgoal for s a b aa ba
using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l lits
unfolding lookup_conflict_remove1_pre_def prod.simps
by (auto simp: I_def empty_conflict_and_extract_clause_heur_inv_def
lookup_clause_rel_def D atms_of_def)
subgoal for s a b aa ba
by (rule C1_L)
subgoal for s a b aa ba
using literals_are_in_ℒ⇩i⇩n_in_ℒ⇩a⇩l⇩l lits
unfolding lookup_conflict_remove1_pre_def prod.simps
by (auto simp: I_def empty_conflict_and_extract_clause_heur_inv_def
lookup_clause_rel_def D atms_of_def)
subgoal for s a b aa ba
by (rule ba_le)
subgoal
by (rule inv)
subgoal
by (rule I_rec)
subgoal
by auto
subgoal for s
unfolding prod.simps
apply (cases s)
apply clarsimp
apply (intro conjI)
subgoal
by (rule ex_mset)
subgoal
using assms
by (auto simp: empty_conflict_and_extract_clause_heur_inv_def I_def mset_tl_out)
subgoal
using assms
by (auto simp: empty_conflict_and_extract_clause_heur_inv_def I_def mset_tl_out)
subgoal
using assms
by (auto simp: empty_conflict_and_extract_clause_heur_inv_def I_def mset_tl_out)
subgoal
using assms
by (auto simp: empty_conflict_and_extract_clause_heur_inv_def I_def mset_tl_out)
subgoal
using assms
by (auto simp: empty_conflict_and_extract_clause_heur_inv_def I_def mset_tl_out)
done
done
have x1b_lall: ‹x1b ! 1 ∈# ℒ⇩a⇩l⇩l 𝒜›
if
inv: ‹(x, x')
∈ {((E, C, n), E', F').
(E, E') ∈ lookup_clause_rel 𝒜 ∧
mset C = mset outl ∧
C ! 0 = outl ! 0 ∧
(1 < length C ⟶
highest_lit M (mset (tl C)) (Some (C ! 1, get_level M (C ! 1)))) ∧
n = length outl ∧
I (E, C, n)}› and
‹x' ∈ {(E, F). E = {#} ∧ mset F = D}› and
st:
‹x' = (x1, x2)›
‹x2a = (x1b, x2b)›
‹x = (x1a, x2a)› and
‹length outl ≠ 1 ⟶ 1 < length x1b› and
‹length outl ≠ 1›
for x x' x1 x2 x1a x2a x1b x2b
proof -
have
‹(x1a, x1) ∈ lookup_clause_rel 𝒜› and
‹mset x1b = mset outl› and
‹x1b ! 0 = outl ! 0› and
‹Suc 0 < length x1b ⟶
highest_lit M (mset (tl x1b))
(Some (x1b ! Suc 0, get_level M (x1b ! Suc 0)))› and
mset_aa: ‹mset (take x2b x1b) = mset (take x2b outl)› and
‹(x1a, D - mset (take x2b outl)) ∈ lookup_clause_rel 𝒜› and
l_aa_outl: ‹length x1b = length outl› and
‹x1b ! 0 = outl ! 0› and
ba_ge1: ‹Suc 0 ≤ x2b› and
ba_le: ‹x2b ≤ length outl› and
‹Suc 0 < length x1b ∧ Suc 0 < x2b ⟶
highest_lit M (mset (tl (take x2b x1b)))
(Some (x1b ! Suc 0, get_level M (x1b ! Suc 0)))›
using inv unfolding st I_def prod.case st
by auto
have set_aa_outl: ‹set (take x2b x1b) = set (take x2b outl)›
using mset_aa by (blast dest: mset_eq_setD)
have ba_ge1_aa_ge: ‹x2b > 1 ⟹ x1b ! 1 ∈ set (take x2b x1b)›
using ba_ge1 ba_le l_aa_outl
by (auto simp: in_set_take_conv_nth intro!: bex_lessI[of _ ‹Suc 0›])
then have ‹x1b ! 1 ∈ set outl›
using ba_le l_aa_outl ba_ge1 that
unfolding mset_aa in_multiset_in_set[symmetric]
by (cases ‹x2b > 1›)
(auto simp: mset_aa dest: in_set_takeD)
then show ?thesis
using literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l[OF lits, of ‹x1b ! 1›] by auto
qed
show ?thesis
unfolding empty_conflict_and_extract_clause_heur_def empty_conflict_and_extract_clause_alt_def
Let_def I_def[symmetric]
apply (subst empty_conflict_and_extract_clause_alt_def)
unfolding conc_fun_RES
apply (refine_vcg WHILEIT_rule_stronger_inv[where R = ‹measure (λ(_, _, i). length outl - i)› and
I' = ‹I›] H1)
subgoal using assms by (auto simp: I_def)
subgoal by (rule x1b_lall)
subgoal using assms
by (auto intro!: RETURN_RES_refine simp: option_lookup_clause_rel_def I_def)
done
qed
definition isa_empty_conflict_and_extract_clause_heur ::
"trail_pol ⇒ lookup_clause_rel ⇒ nat literal list ⇒ (_ × nat literal list × nat) nres"
where
‹isa_empty_conflict_and_extract_clause_heur M D outl = do {
let C = replicate (length outl) (outl!0);
(D, C, _) ← WHILE⇩T
(λ(D, C, i). i < length_uint32_nat outl)
(λ(D, C, i). do {
ASSERT(i < length outl);
ASSERT(i < length C);
ASSERT(lookup_conflict_remove1_pre (outl ! i, D));
let D = lookup_conflict_remove1 (outl ! i) D;
let C = C[i := outl ! i];
ASSERT(get_level_pol_pre (M, C!i));
ASSERT(get_level_pol_pre (M, C!1));
ASSERT(1 < length C);
let C = (if get_level_pol M (C!i) > get_level_pol M (C!1) then swap C 1 i else C);
ASSERT(i+1 ≤ uint32_max);
RETURN (D, C, i+1)
})
(D, C, 1);
ASSERT(length outl ≠ 1 ⟶ length C > 1);
ASSERT(length outl ≠ 1 ⟶ get_level_pol_pre (M, C!1));
RETURN ((True, D), C, if length outl = 1 then 0 else get_level_pol M (C!1))
}›
lemma isa_empty_conflict_and_extract_clause_heur_empty_conflict_and_extract_clause_heur:
‹(uncurry2 isa_empty_conflict_and_extract_clause_heur, uncurry2 (empty_conflict_and_extract_clause_heur 𝒜)) ∈
trail_pol 𝒜 ×⇩f Id ×⇩f Id →⇩f ⟨Id⟩nres_rel ›
proof -
have [refine0]: ‹((x2b, replicate (length x2c) (x2c ! 0), 1), x2,
replicate (length x2a) (x2a ! 0), 1)
∈ Id ×⇩f Id ×⇩f Id›
if
‹(x, y) ∈ trail_pol 𝒜 ×⇩f Id ×⇩f Id› and ‹x1 = (x1a, x2)› and
‹y = (x1, x2a)› and
‹x1b = (x1c, x2b)› and
‹x = (x1b, x2c)›
for x y x1 x1a x2 x2a x1b x1c x2b x2c
using that by auto
show ?thesis
supply [[goals_limit=1]]
unfolding isa_empty_conflict_and_extract_clause_heur_def empty_conflict_and_extract_clause_heur_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg)
apply (assumption+)[5]
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal
by (rule get_level_pol_pre) auto
subgoal
by (rule get_level_pol_pre) auto
subgoal by auto
subgoal by auto
subgoal
by (auto simp: get_level_get_level_pol[of _ _ 𝒜])
subgoal by auto
subgoal
by (rule get_level_pol_pre) auto
subgoal by (auto simp: get_level_get_level_pol[of _ _ 𝒜])
done
qed
definition extract_shorter_conflict_wl_nlit where
‹extract_shorter_conflict_wl_nlit K M NU D NE UE =
SPEC(λD'. D' ≠ None ∧ the D' ⊆# the D ∧ K ∈# the D' ∧
mset `# ran_mf NU + NE + UE ⊨pm the D')›
definition extract_shorter_conflict_wl_nlit_st
:: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres›
where
‹extract_shorter_conflict_wl_nlit_st =
(λ(M, N, D, NE, UE, WS, Q). do {
let K = -lit_of (hd M);
D ← extract_shorter_conflict_wl_nlit K M N D NE UE;
RETURN (M, N, D, NE, UE, WS, Q)})›
definition empty_lookup_conflict_and_highest
:: ‹'v twl_st_wl ⇒ ('v twl_st_wl × nat) nres›
where
‹empty_lookup_conflict_and_highest =
(λ(M, N, D, NE, UE, WS, Q). do {
let K = -lit_of (hd M);
let n = get_maximum_level M (remove1_mset K (the D));
RETURN ((M, N, D, NE, UE, WS, Q), n)})›
definition backtrack_wl_D_heur_inv where
‹backtrack_wl_D_heur_inv S ⟷ (∃S'. (S, S') ∈ twl_st_heur_conflict_ana ∧ backtrack_wl_inv S')›
definition extract_shorter_conflict_heur where
‹extract_shorter_conflict_heur = (λM NU NUE C outl. do {
let K = lit_of (hd M);
let C = Some (remove1_mset (-K) (the C));
C ← iterate_over_conflict (-K) M NU NUE (the C);
RETURN (Some (add_mset (-K) C))
})›
definition (in -) empty_cach where
‹empty_cach cach = (λ_. SEEN_UNKNOWN)›
definition empty_conflict_and_extract_clause_pre
:: ‹(((nat,nat) ann_lits × nat clause) × nat clause_l) ⇒ bool› where
‹empty_conflict_and_extract_clause_pre =
(λ((M, D), outl). D = mset (tl outl) ∧ outl ≠ [] ∧ distinct outl ∧
¬tautology (mset outl) ∧ length outl ≤ uint32_max)›
definition (in -) empty_cach_ref where
‹empty_cach_ref = (λ(cach, support). (replicate (length cach) SEEN_UNKNOWN, []))›
definition empty_cach_ref_set_inv where
‹empty_cach_ref_set_inv cach0 support =
(λ(i, cach). length cach = length cach0 ∧
(∀L ∈ set (drop i support). L < length cach) ∧
(∀L ∈ set (take i support). cach ! L = SEEN_UNKNOWN) ∧
(∀L < length cach. cach ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set (drop i support)))›
definition empty_cach_ref_set where
‹empty_cach_ref_set = (λ(cach0, support). do {
let n = length support;
ASSERT(n ≤ Suc (uint32_max div 2));
(_, cach) ← WHILE⇩T⇗empty_cach_ref_set_inv cach0 support⇖
(λ(i, cach). i < length support)
(λ(i, cach). do {
ASSERT(i < length support);
ASSERT(support ! i < length cach);
RETURN(i+1, cach[support ! i := SEEN_UNKNOWN])
})
(0, cach0);
RETURN (cach, emptied_list support)
})›
lemma empty_cach_ref_set_empty_cach_ref:
‹(empty_cach_ref_set, RETURN o empty_cach_ref) ∈
[λ(cach, supp). (∀L ∈ set supp. L < length cach) ∧ length supp ≤ Suc (uint32_max div 2) ∧
(∀L < length cach. cach ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set supp)]⇩f
Id → ⟨Id⟩ nres_rel›
proof -
have H: ‹WHILE⇩T⇗empty_cach_ref_set_inv cach0 support'⇖ (λ(i, cach). i < length support')
(λ(i, cach).
ASSERT (i < length support') ⤜
(λ_. ASSERT (support' ! i < length cach) ⤜
(λ_. RETURN (i + 1, cach[support' ! i := SEEN_UNKNOWN]))))
(0, cach0) ⤜
(λ(_, cach). RETURN (cach, emptied_list support'))
≤ ⇓ Id (RETURN (replicate (length cach0) SEEN_UNKNOWN, []))›
if
‹∀L∈set support'. L < length cach0› and
‹∀L<length cach0. cach0 ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set support'›
for cach support cach0 support'
proof -
have init: ‹empty_cach_ref_set_inv cach0 support' (0, cach0)›
using that unfolding empty_cach_ref_set_inv_def
by auto
have valid_length:
‹empty_cach_ref_set_inv cach0 support' s ⟹ case s of (i, cach) ⇒ i < length support' ⟹
s = (cach', sup') ⟹ support' ! cach' < length sup'› for s cach' sup'
using that unfolding empty_cach_ref_set_inv_def
by auto
have set_next: ‹empty_cach_ref_set_inv cach0 support' (i + 1, cach'[support' ! i := SEEN_UNKNOWN])›
if
inv: ‹empty_cach_ref_set_inv cach0 support' s› and
cond: ‹case s of (i, cach) ⇒ i < length support'› and
s: ‹s = (i, cach')› and
valid[simp]: ‹support' ! i < length cach'›
for s i cach'
proof -
have
le_cach_cach0: ‹length cach' = length cach0› and
le_length: ‹∀L∈set (drop i support'). L < length cach'› and
UNKNOWN: ‹∀L∈set (take i support'). cach' ! L = SEEN_UNKNOWN› and
support: ‹∀L<length cach'. cach' ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set (drop i support')› and
[simp]: ‹i < length support'›
using inv cond unfolding empty_cach_ref_set_inv_def s prod.case
by auto
show ?thesis
unfolding empty_cach_ref_set_inv_def
unfolding prod.case
apply (intro conjI)
subgoal by (simp add: le_cach_cach0)
subgoal using le_length by (simp add: Cons_nth_drop_Suc[symmetric])
subgoal using UNKNOWN by (auto simp add: take_Suc_conv_app_nth)
subgoal using support by (auto simp add: Cons_nth_drop_Suc[symmetric])
done
qed
have final: ‹((cach', emptied_list support'), replicate (length cach0) SEEN_UNKNOWN, []) ∈ Id›
if
inv: ‹empty_cach_ref_set_inv cach0 support' s› and
cond: ‹¬ (case s of (i, cach) ⇒ i < length support')› and
s: ‹s = (i, cach')›
for s cach' i
proof -
have
le_cach_cach0: ‹length cach' = length cach0› and
le_length: ‹∀L∈set (drop i support'). L < length cach'› and
UNKNOWN: ‹∀L∈set (take i support'). cach' ! L = SEEN_UNKNOWN› and
support: ‹∀L<length cach'. cach' ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set (drop i support')› and
i: ‹¬i < length support'›
using inv cond unfolding empty_cach_ref_set_inv_def s prod.case
by auto
have ‹∀L<length cach'. cach' ! L = SEEN_UNKNOWN›
using support i by auto
then have [dest]: ‹L ∈ set cach' ⟹ L = SEEN_UNKNOWN› for L
by (metis in_set_conv_nth)
then have [dest]: ‹SEEN_UNKNOWN ∉ set cach' ⟹ cach0 = [] ∧ cach' = []›
using le_cach_cach0 by (cases cach') auto
show ?thesis
by (auto simp: emptied_list_def list_eq_replicate_iff le_cach_cach0)
qed
show ?thesis
unfolding conc_Id id_def
apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(i, _). length support' - i)›])
subgoal by auto
subgoal by (rule init)
subgoal by auto
subgoal by (rule valid_length)
subgoal by (rule set_next)
subgoal by auto
subgoal using final by simp
done
qed
show ?thesis
unfolding empty_cach_ref_set_def empty_cach_ref_def Let_def comp_def
by (intro frefI nres_relI ASSERT_leI) (clarify intro!: H ASSERT_leI)
qed
lemma empty_cach_ref_empty_cach:
‹isasat_input_bounded 𝒜 ⟹ (RETURN o empty_cach_ref, RETURN o empty_cach) ∈ cach_refinement 𝒜 →⇩f ⟨cach_refinement 𝒜⟩ nres_rel›
by (intro frefI nres_relI)
(auto simp: empty_cach_def empty_cach_ref_def cach_refinement_alt_def cach_refinement_list_def
map_fun_rel_def intro: bounded_included_le)
definition empty_cach_ref_pre where
‹empty_cach_ref_pre = (λ(cach :: minimize_status list, supp :: nat list).
(∀L∈set supp. L < length cach) ∧
length supp ≤ Suc (uint32_max div 2) ∧
(∀L<length cach. cach ! L ≠ SEEN_UNKNOWN ⟶ L ∈ set supp))›
paragraph ‹Minimisation of the conflict›
definition extract_shorter_conflict_list_heur_st
:: ‹twl_st_wl_heur ⇒ (twl_st_wl_heur × _ × _) nres›
where
‹extract_shorter_conflict_list_heur_st = (λ(M, N, (_, D), Q', W', vm, clvls, cach, lbd, outl,
stats, ccont, vdom). do {
ASSERT(fst M ≠ []);
let K = lit_of_last_trail_pol M;
ASSERT(0 < length outl);
ASSERT(lookup_conflict_remove1_pre (-K, D));
let D = lookup_conflict_remove1 (-K) D;
let outl = outl[0 := -K];
vm ← isa_vmtf_mark_to_rescore_also_reasons M N outl vm;
(D, cach, outl) ← isa_minimize_and_extract_highest_lookup_conflict M N D cach lbd outl;
ASSERT(empty_cach_ref_pre cach);
let cach = empty_cach_ref cach;
ASSERT(outl ≠ [] ∧ length outl ≤ uint32_max);
(D, C, n) ← isa_empty_conflict_and_extract_clause_heur M D outl;
RETURN ((M, N, D, Q', W', vm, clvls, cach, lbd, take 1 outl, stats, ccont, vdom), n, C)
})›
lemma the_option_lookup_clause_assn:
‹(RETURN o snd, RETURN o the) ∈ [λD. D ≠ None]⇩f option_lookup_clause_rel 𝒜 → ⟨lookup_clause_rel 𝒜⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: option_lookup_clause_rel_def)
definition update_heuristics where
‹update_heuristics = (λglue (fema, sema, res_info, wasted).
(ema_update glue fema, ema_update glue sema,
incr_conflict_count_since_last_restart res_info, wasted))›
lemma heuristic_rel_update_heuristics[intro!]:
‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (update_heuristics glue heur)›
by (auto simp: heuristic_rel_def phase_save_heur_rel_def phase_saving_def
update_heuristics_def)
definition propagate_bt_wl_D_heur
:: ‹nat literal ⇒ nat clause_l ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹propagate_bt_wl_D_heur = (λL C (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur, vdom, avdom, lcount, opts). do {
ASSERT(length vdom ≤ length N0);
ASSERT(length avdom ≤ length N0);
ASSERT(nat_of_lit (C!1) < length W0 ∧ nat_of_lit (-L) < length W0);
ASSERT(length C > 1);
let L' = C!1;
ASSERT(length C ≤ uint32_max div 2 + 1);
vm ← isa_vmtf_rescore C M vm0;
glue ← get_LBD lbd;
let b = False;
let b' = (length C = 2);
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ append_and_length_fast_code_pre ((b, C), N0));
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ lcount < sint64_max);
(N, i) ← fm_add_new b C N0;
ASSERT(update_lbd_pre ((i, glue), N));
let N = update_lbd i glue N;
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ length_ll W0 (nat_of_lit (-L)) < sint64_max);
let W = W0[nat_of_lit (- L) := W0 ! nat_of_lit (- L) @ [(i, L', b')]];
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ length_ll W (nat_of_lit L') < sint64_max);
let W = W[nat_of_lit L' := W!nat_of_lit L' @ [(i, -L, b')]];
lbd ← lbd_empty lbd;
ASSERT(isa_length_trail_pre M);
let j = isa_length_trail M;
ASSERT(i ≠ DECISION_REASON);
ASSERT(cons_trail_Propagated_tr_pre ((-L, i), M));
M ← cons_trail_Propagated_tr (- L) i M;
vm ← isa_vmtf_flush_int M vm;
heur ← mop_save_phase_heur (atm_of L') (is_neg L') heur;
RETURN (M, N, D, j, W, vm, 0,
cach, lbd, outl, add_lbd (of_nat glue) stats, update_heuristics glue heur, vdom @ [ i],
avdom @ [i],
lcount + 1, opts)
})›
definition (in -) lit_of_hd_trail_st_heur :: ‹twl_st_wl_heur ⇒ nat literal nres› where
‹lit_of_hd_trail_st_heur S = do {ASSERT (fst (get_trail_wl_heur S) ≠ []); RETURN (lit_of_last_trail_pol (get_trail_wl_heur S))}›
definition remove_last
:: ‹nat literal ⇒ nat clause option ⇒ nat clause option nres›
where
‹remove_last _ _ = SPEC((=) None)›
definition propagate_unit_bt_wl_D_int
:: ‹nat literal ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
‹propagate_unit_bt_wl_D_int = (λL (M, N, D, Q, W, vm, clvls, cach, lbd, outl, stats,
heur, vdom). do {
vm ← isa_vmtf_flush_int M vm;
glue ← get_LBD lbd;
lbd ← lbd_empty lbd;
ASSERT(isa_length_trail_pre M);
let j = isa_length_trail M;
ASSERT(0 ≠ DECISION_REASON);
ASSERT(cons_trail_Propagated_tr_pre ((- L, 0::nat), M));
M ← cons_trail_Propagated_tr (- L) 0 M;
let stats = incr_uset stats;
RETURN (M, N, D, j, W, vm, clvls, cach, lbd, outl, stats,
(update_heuristics glue heur), vdom)})›
paragraph ‹Full function›
definition backtrack_wl_D_nlit_heur
:: ‹twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
‹backtrack_wl_D_nlit_heur S⇩0 =
do {
ASSERT(backtrack_wl_D_heur_inv S⇩0);
ASSERT(fst (get_trail_wl_heur S⇩0) ≠ []);
L ← lit_of_hd_trail_st_heur S⇩0;
(S, n, C) ← extract_shorter_conflict_list_heur_st S⇩0;
ASSERT(get_clauses_wl_heur S = get_clauses_wl_heur S⇩0);
S ← find_decomp_wl_st_int n S;
ASSERT(get_clauses_wl_heur S = get_clauses_wl_heur S⇩0);
if size C > 1
then do {
S ← propagate_bt_wl_D_heur L C S;
save_phase_st S
}
else do {
propagate_unit_bt_wl_D_int L S
}
}›
lemma get_all_ann_decomposition_get_level:
assumes
L': ‹L' = lit_of (hd M')› and
nd: ‹no_dup M'› and
decomp: ‹(Decided K # a, M2) ∈ set (get_all_ann_decomposition M')› and
lev_K: ‹get_level M' K = Suc (get_maximum_level M' (remove1_mset (- L') y))› and
L: ‹L ∈# remove1_mset (- lit_of (hd M')) y›
shows ‹get_level a L = get_level M' L›
proof -
obtain M3 where M3: ‹M' = M3 @ M2 @ Decided K # a›
using decomp by blast
from lev_K have lev_L: ‹get_level M' L < get_level M' K›
using get_maximum_level_ge_get_level[OF L, of M'] unfolding L'[symmetric] by auto
have [simp]: ‹get_level (M3 @ M2 @ Decided K # a) K = Suc (count_decided a)›
using nd unfolding M3 by auto
have undef:‹undefined_lit (M3 @ M2) L›
using lev_L get_level_skip_end[of ‹M3 @ M2› L ‹Decided K # a›] unfolding M3
by auto
then have ‹atm_of L ≠ atm_of K›
using lev_L unfolding M3 by auto
then show ?thesis
using undef unfolding M3 by (auto simp: get_level_cons_if)
qed
definition del_conflict_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl› where
‹del_conflict_wl = (λ(M, N, D, NE, UE, Q, W). (M, N, None, NE, UE, Q, W))›
lemma [simp]:
‹get_clauses_wl (del_conflict_wl S) = get_clauses_wl S›
by (cases S) (auto simp: del_conflict_wl_def)
lemma lcount_add_clause[simp]: ‹i ∉# dom_m N ⟹
size (learned_clss_l (fmupd i (C, False) N)) = Suc (size (learned_clss_l N))›
by (simp add: learned_clss_l_mapsto_upd_notin)
lemma length_watched_le:
assumes
prop_inv: ‹correct_watching x1› and
xb_x'a: ‹(x1a, x1) ∈ twl_st_heur_conflict_ana› and
x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms_st x1)›
shows ‹length (watched_by x1 x2) ≤ length (get_clauses_wl_heur x1a) - 2›
proof -
have ‹correct_watching x1›
using prop_inv unfolding unit_propagation_outer_loop_wl_inv_def
unit_propagation_outer_loop_wl_inv_def
by auto
then have dist: ‹distinct_watched (watched_by x1 x2)›
using x2 unfolding all_atms_def[symmetric] all_lits_alt_def[symmetric]
by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps
ℒ⇩a⇩l⇩l_all_atms_all_lits
simp flip: all_lits_alt_def2 all_lits_def all_atms_def)
then have dist: ‹distinct_watched (watched_by x1 x2)›
using xb_x'a
by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps)
have dist_vdom: ‹distinct (get_vdom x1a)›
using xb_x'a
by (cases x1)
(auto simp: twl_st_heur_conflict_ana_def twl_st_heur'_def)
have x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms_st x1)›
using x2 xb_x'a unfolding all_atms_def
by auto
have
valid: ‹valid_arena (get_clauses_wl_heur x1a) (get_clauses_wl x1) (set (get_vdom x1a))›
using xb_x'a unfolding all_atms_def all_lits_def
by (cases x1)
(auto simp: twl_st_heur'_def twl_st_heur_conflict_ana_def)
have ‹vdom_m (all_atms_st x1) (get_watched_wl x1) (get_clauses_wl x1) ⊆ set (get_vdom x1a)›
using xb_x'a
by (cases x1)
(auto simp: twl_st_heur_conflict_ana_def twl_st_heur'_def all_atms_def[symmetric])
then have subset: ‹set (map fst (watched_by x1 x2)) ⊆ set (get_vdom x1a)›
using x2 unfolding vdom_m_def
by (cases x1)
(force simp: twl_st_heur'_def twl_st_heur_def simp flip: all_atms_def
dest!: multi_member_split)
have watched_incl: ‹mset (map fst (watched_by x1 x2)) ⊆# mset (get_vdom x1a)›
by (rule distinct_subseteq_iff[THEN iffD1])
(use dist[unfolded distinct_watched_alt_def] dist_vdom subset in
‹simp_all flip: distinct_mset_mset_distinct›)
have vdom_incl: ‹set (get_vdom x1a) ⊆ {4..< length (get_clauses_wl_heur x1a)}›
using valid_arena_in_vdom_le_arena[OF valid] arena_dom_status_iff[OF valid] by auto
have ‹length (get_vdom x1a) ≤ length (get_clauses_wl_heur x1a) - 4›
by (subst distinct_card[OF dist_vdom, symmetric])
(use card_mono[OF _ vdom_incl] in auto)
then show ?thesis
using size_mset_mono[OF watched_incl] xb_x'a
by (auto intro!: order_trans[of ‹length (watched_by x1 x2)› ‹length (get_vdom x1a)›])
qed
definition single_of_mset where
‹single_of_mset D = SPEC(λL. D = mset [L])›
lemma length_list_ge2: ‹length S ≥ 2 ⟷ (∃a b S'. S = [a, b] @ S')›
apply (cases S)
apply (simp; fail)
apply (rename_tac a S')
apply (case_tac S')
by simp_all
lemma backtrack_wl_D_nlit_backtrack_wl_D:
‹(backtrack_wl_D_nlit_heur, backtrack_wl) ∈
{(S, T). (S, T) ∈ twl_st_heur_conflict_ana ∧ length (get_clauses_wl_heur S) = r} →⇩f
⟨{(S, T). (S, T) ∈ twl_st_heur ∧ length (get_clauses_wl_heur S) ≤ 6 + r + uint32_max div 2}⟩nres_rel›
(is ‹_ ∈ ?R →⇩f ⟨?S⟩nres_rel›)
proof -
have backtrack_wl_D_nlit_heur_alt_def: ‹backtrack_wl_D_nlit_heur S⇩0 =
do {
ASSERT(backtrack_wl_D_heur_inv S⇩0);
ASSERT(fst (get_trail_wl_heur S⇩0) ≠ []);
L ← lit_of_hd_trail_st_heur S⇩0;
(S, n, C) ← extract_shorter_conflict_list_heur_st S⇩0;
ASSERT(get_clauses_wl_heur S = get_clauses_wl_heur S⇩0);
S ← find_decomp_wl_st_int n S;
ASSERT(get_clauses_wl_heur S = get_clauses_wl_heur S⇩0);
if size C > 1
then do {
let _ = C ! 1;
S ← propagate_bt_wl_D_heur L C S;
save_phase_st S
}
else do {
propagate_unit_bt_wl_D_int L S
}
}› for S⇩0
unfolding backtrack_wl_D_nlit_heur_def Let_def
by auto
have inv: ‹backtrack_wl_D_heur_inv S'›
if
‹backtrack_wl_inv S› and
‹(S', S) ∈ ?R›
for S S'
using that unfolding backtrack_wl_D_heur_inv_def
by (cases S; cases S') (blast intro: exI[of _ S'])
have shorter:
‹extract_shorter_conflict_list_heur_st S'
≤ ⇓ {((T', n, C), T). (T', del_conflict_wl T) ∈ twl_st_heur_bt ∧
n = get_maximum_level (get_trail_wl T)
(remove1_mset (-lit_of(hd (get_trail_wl T))) (the (get_conflict_wl T))) ∧
mset C = the (get_conflict_wl T) ∧
get_conflict_wl T ≠ None∧
equality_except_conflict_wl T S ∧
get_clauses_wl_heur T' = get_clauses_wl_heur S' ∧
(1 < length C ⟶
highest_lit (get_trail_wl T) (mset (tl C))
(Some (C ! 1, get_level (get_trail_wl T) (C ! 1)))) ∧
C ≠ [] ∧ hd C = -lit_of(hd (get_trail_wl T)) ∧
mset C ⊆# the (get_conflict_wl S) ∧
distinct_mset (the (get_conflict_wl S)) ∧
literals_are_in_ℒ⇩i⇩n (all_atms_st S) (the (get_conflict_wl S)) ∧
literals_are_in_ℒ⇩i⇩n_trail (all_atms_st T) (get_trail_wl T) ∧
get_conflict_wl S ≠ None ∧
- lit_of (hd (get_trail_wl S)) ∈# ℒ⇩a⇩l⇩l (all_atms_st S) ∧
literals_are_ℒ⇩i⇩n (all_atms_st T) T ∧
n < count_decided (get_trail_wl T) ∧
get_trail_wl T ≠ [] ∧
¬ tautology (mset C) ∧
correct_watching S ∧ length (get_clauses_wl_heur T') = length (get_clauses_wl_heur S')}
(extract_shorter_conflict_wl S)›
(is ‹_ ≤ ⇓ ?shorter _›)
if
inv: ‹backtrack_wl_inv S› and
S'_S: ‹(S', S) ∈ ?R›
for S S'
proof -
obtain M N D NE UE NS US Q W where
S: ‹S = (M, N, D, NE, UE, NS, US, Q, W)›
by (cases S)
obtain M' W' vm clvls cach lbd outl stats heur avdom vdom lcount D' arena b Q' opts where
S': ‹S' = (M', arena, (b, D'), Q', W', vm, clvls, cach, lbd, outl, stats, heur, vdom,
avdom, lcount, opts)›
using S'_S by (cases S') (auto simp: twl_st_heur_conflict_ana_def S)
have
M'_M: ‹(M', M) ∈ trail_pol (all_atms_st S)› and
‹(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms_st S))› and
vm: ‹vm ∈ isa_vmtf (all_atms_st S) M› and
n_d: ‹no_dup M› and
‹clvls ∈ counts_maximum_level M D› and
cach_empty: ‹cach_refinement_empty (all_atms_st S) cach› and
outl: ‹out_learned M D outl› and
lcount: ‹lcount = size (learned_clss_l N)› and
‹vdom_m (all_atms_st S) W N ⊆ set vdom› and
D': ‹((b, D'), D) ∈ option_lookup_clause_rel (all_atms_st S)› and
arena: ‹valid_arena arena N (set vdom)› and
avdom: ‹mset avdom ⊆# mset vdom› and
bounded: ‹isasat_input_bounded (all_atms_st S)›
using S'_S unfolding S S' twl_st_heur_conflict_ana_def
by (auto simp: S all_atms_def[symmetric])
obtain T U where
ℒ⇩i⇩n :‹literals_are_ℒ⇩i⇩n (all_atms_st S) S› and
S_T: ‹(S, T) ∈ state_wl_l None› and
corr: ‹correct_watching S› and
T_U: ‹(T, U) ∈ twl_st_l None› and
trail_nempty: ‹get_trail_l T ≠ []› and
not_none: ‹get_conflict_l T ≠ None› and
struct_invs: ‹twl_struct_invs U› and
stgy_invs: ‹twl_stgy_invs U› and
list_invs: ‹twl_list_invs T› and
not_empty: ‹get_conflict_l T ≠ Some {#}› and
uL_D: ‹- lit_of (hd (get_trail_wl S)) ∈# the (get_conflict_wl S)› and
nss: ‹no_step cdcl⇩W_restart_mset.skip (state⇩W_of U)› and
nsr: ‹no_step cdcl⇩W_restart_mset.resolve (state⇩W_of U)›
using inv unfolding backtrack_wl_inv_def backtrack_wl_inv_def backtrack_l_inv_def backtrack_inv_def
apply -
apply normalize_goal+ by simp
have D_none: ‹D ≠ None›
using S_T not_none by (auto simp: S)
have b: ‹¬b›
using D' not_none S_T by (auto simp: option_lookup_clause_rel_def S state_wl_l_def)
have all_struct:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of U)›
using struct_invs
by (auto simp: twl_struct_invs_def)
have
‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of U)› and
lev_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of U)› and
‹∀s∈#learned_clss (state⇩W_of U). ¬ tautology s› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (state⇩W_of U)› and
confl: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of U)› and
‹all_decomposition_implies_m (cdcl⇩W_restart_mset.clauses (state⇩W_of U))
(get_all_ann_decomposition (trail (state⇩W_of U)))› and
learned: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (state⇩W_of U)›
using all_struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have n_d: ‹no_dup M›
using lev_inv S_T T_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: twl_st S)
have M_ℒ⇩i⇩n: ‹literals_are_in_ℒ⇩i⇩n_trail (all_atms_st S) (get_trail_wl S)›
apply (rule literals_are_ℒ⇩i⇩n_literals_are_ℒ⇩i⇩n_trail[OF S_T struct_invs T_U ℒ⇩i⇩n ]) .
have dist_D: ‹distinct_mset (the (get_conflict_wl S))›
using dist not_none S_T T_U unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def S
by (auto simp: twl_st)
have ‹the (conflicting (state⇩W_of U)) =
add_mset (- lit_of (cdcl⇩W_restart_mset.hd_trail (state⇩W_of U)))
{#L ∈# the (conflicting (state⇩W_of U)). get_level (trail (state⇩W_of U)) L
< backtrack_lvl (state⇩W_of U)#}›
apply (rule cdcl⇩W_restart_mset.no_skip_no_resolve_single_highest_level)
subgoal using nss unfolding S by simp
subgoal using nsr unfolding S by simp
subgoal using struct_invs unfolding twl_struct_invs_def S by simp
subgoal using stgy_invs unfolding twl_stgy_invs_def S by simp
subgoal using not_none S_T T_U by (simp add: twl_st)
subgoal using not_empty not_none S_T T_U by (auto simp add: twl_st)
done
then have D_filter: ‹the D = add_mset (- lit_of (hd M)) {#L ∈# the D. get_level M L < count_decided M#}›
using trail_nempty S_T T_U by (simp add: twl_st S)
have tl_outl_D: ‹mset (tl (outl[0 := - lit_of (hd M)])) = remove1_mset (outl[0 := - lit_of (hd M)] ! 0) (the D)›
using outl S_T T_U not_none
apply (subst D_filter)
by (cases outl) (auto simp: out_learned_def S)
let ?D = ‹remove1_mset (- lit_of (hd M)) (the D)›
have ℒ⇩i⇩n_S: ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S) (the (get_conflict_wl S))›
apply (rule literals_are_ℒ⇩i⇩n_literals_are_in_ℒ⇩i⇩n_conflict[OF S_T _ T_U])
using ℒ⇩i⇩n not_none struct_invs not_none S_T T_U by (auto simp: S)
then have ℒ⇩i⇩n_D: ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S) ?D›
unfolding S by (auto intro: literals_are_in_ℒ⇩i⇩n_mono)
have ℒ⇩i⇩n_NU: ‹literals_are_in_ℒ⇩i⇩n_mm (all_atms_st S) (mset `# ran_mf (get_clauses_wl S))›
by (auto simp: all_atms_def all_lits_def literals_are_in_ℒ⇩i⇩n_mm_def
ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm)
(simp add: all_lits_of_mm_union)
have tauto_confl: ‹¬ tautology (the (get_conflict_wl S))›
apply (rule conflict_not_tautology[OF S_T _ T_U])
using struct_invs not_none S_T T_U by (auto simp: twl_st)
from not_tautology_mono[OF _ this, of ?D] have tauto_D: ‹¬ tautology ?D›
by (auto simp: S)
have entailed:
‹mset `# ran_mf (get_clauses_wl S) + (get_unit_learned_clss_wl S + get_unit_init_clss_wl S) +
(get_subsumed_init_clauses_wl S + get_subsumed_learned_clauses_wl S)⊨pm
add_mset (- lit_of (hd (get_trail_wl S)))
(remove1_mset (- lit_of (hd (get_trail_wl S))) (the (get_conflict_wl S)))›
using uL_D learned not_none S_T T_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by (auto simp: ac_simps twl_st get_unit_clauses_wl_alt_def)
define cach' where ‹cach' = (λ_::nat. SEEN_UNKNOWN)›
have mini: ‹minimize_and_extract_highest_lookup_conflict (all_atms_st S) (get_trail_wl S) (get_clauses_wl S)
?D cach' lbd (outl[0 := - lit_of (hd M)])
≤ ⇓ {((E, s, outl), E'). E = E' ∧ mset (tl outl) = E ∧
outl ! 0 = - lit_of (hd M) ∧ E' ⊆# remove1_mset (- lit_of (hd M)) (the D) ∧
outl ≠ []}
(iterate_over_conflict (- lit_of (hd M)) (get_trail_wl S)
(mset `# ran_mf (get_clauses_wl S))
(get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
(get_subsumed_learned_clauses_wl S + get_subsumed_init_clauses_wl S))
?D)›
apply (rule minimize_and_extract_highest_lookup_conflict_iterate_over_conflict[of S T U
‹outl [0 := - lit_of (hd M)]›
‹remove1_mset _ (the D)› ‹all_atms_st S› cach' ‹-lit_of (hd M)› lbd])
subgoal using S_T .
subgoal using T_U .
subgoal using ‹out_learned M D outl› tl_outl_D
by (auto simp: out_learned_def)
subgoal using confl not_none S_T T_U unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (auto simp: true_annot_CNot_diff twl_st S)
subgoal
using dist not_none S_T T_U unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
by (auto simp: twl_st S)
subgoal using tauto_D .
subgoal using M_ℒ⇩i⇩n unfolding S by simp
subgoal using struct_invs unfolding S by simp
subgoal using list_invs unfolding S by simp
subgoal using M_ℒ⇩i⇩n cach_empty S_T T_U
unfolding cach_refinement_empty_def conflict_min_analysis_inv_def
by (auto dest: literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l_atms simp: cach'_def twl_st S)
subgoal using entailed unfolding S by (simp add: ac_simps)
subgoal using ℒ⇩i⇩n_D .
subgoal using ℒ⇩i⇩n_NU .
subgoal using ‹out_learned M D outl› tl_outl_D
by (auto simp: out_learned_def)
subgoal using ‹out_learned M D outl› tl_outl_D
by (auto simp: out_learned_def)
subgoal using bounded unfolding all_atms_def by (simp add: S)
done
then have mini: ‹minimize_and_extract_highest_lookup_conflict (all_atms_st S) M N
?D cach' lbd (outl[0 := - lit_of (hd M)])
≤ ⇓ {((E, s, outl), E'). E = E' ∧ mset (tl outl) = E ∧
outl ! 0 = - lit_of (hd M) ∧ E' ⊆# remove1_mset (- lit_of (hd M)) (the D) ∧
outl ≠ []}
(iterate_over_conflict (- lit_of (hd M)) (get_trail_wl S)
(mset `# ran_mf N)
(get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
(get_subsumed_learned_clauses_wl S +
get_subsumed_init_clauses_wl S)) ?D)›
unfolding S by auto
have mini: ‹minimize_and_extract_highest_lookup_conflict (all_atms_st S) M N
?D cach' lbd (outl[0 := - lit_of (hd M)])
≤ ⇓ {((E, s, outl), E'). E = E' ∧ mset (tl outl) = E ∧
outl ! 0 = - lit_of (hd M) ∧ E' ⊆# remove1_mset (- lit_of (hd M)) (the D) ∧
outl ≠ []}
(SPEC (λD'. D' ⊆# ?D ∧ mset `# ran_mf N +
(get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
(get_subsumed_learned_clauses_wl S +
get_subsumed_init_clauses_wl S)) ⊨pm add_mset (- lit_of (hd M)) D'))›
apply (rule order.trans)
apply (rule mini)
apply (rule ref_two_step')
apply (rule order.trans)
apply (rule iterate_over_conflict_spec)
subgoal using entailed by (auto simp: S ac_simps)
subgoal
using dist not_none S_T T_U unfolding S cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
by (auto simp: twl_st)
subgoal by (auto simp: ac_simps)
done
have uM_ℒ⇩a⇩l⇩l: ‹- lit_of (hd M) ∈# ℒ⇩a⇩l⇩l (all_atms_st S)›
using M_ℒ⇩i⇩n trail_nempty S_T T_U by (cases M)
(auto simp: literals_are_in_ℒ⇩i⇩n_trail_Cons uminus_𝒜⇩i⇩n_iff twl_st S)
have L_D: ‹lit_of (hd M) ∉# the D› and
tauto_confl': ‹¬tautology (remove1_mset (- lit_of (hd M)) (the D))›
using uL_D tauto_confl
by (auto dest!: multi_member_split simp: S add_mset_eq_add_mset tautology_add_mset)
then have pre1: ‹D ≠ None ∧ delete_from_lookup_conflict_pre (all_atms_st S) (- lit_of (hd M), the D)›
using not_none uL_D uM_ℒ⇩a⇩l⇩l S_T T_U unfolding delete_from_lookup_conflict_pre_def
by (auto simp: twl_st S)
have pre2: ‹literals_are_in_ℒ⇩i⇩n_trail (all_atms_st S) M ∧ literals_are_in_ℒ⇩i⇩n_mm (all_atms_st S) (mset `# ran_mf N) ≡ True›
and lits_N: ‹literals_are_in_ℒ⇩i⇩n_mm (all_atms_st S) (mset `# ran_mf N)›
using M_ℒ⇩i⇩n S_T T_U not_none ℒ⇩i⇩n
unfolding is_ℒ⇩a⇩l⇩l_def literals_are_in_ℒ⇩i⇩n_mm_def literals_are_ℒ⇩i⇩n_def all_atms_def all_lits_def
by (auto simp: twl_st S all_lits_of_mm_union)
have ‹0 < length outl›
using ‹out_learned M D outl›
by (auto simp: out_learned_def)
have trail_nempty: ‹M ≠ []›
using trail_nempty S_T T_U
by (auto simp: twl_st S)
have lookup_conflict_remove1_pre: ‹lookup_conflict_remove1_pre (-lit_of (hd M), D')›
using D' not_none not_empty S_T uM_ℒ⇩a⇩l⇩l
unfolding lookup_conflict_remove1_pre_def
by (cases ‹the D›)
(auto simp: option_lookup_clause_rel_def lookup_clause_rel_def S
state_wl_l_def atms_of_def)
then have lookup_conflict_remove1_pre: ‹lookup_conflict_remove1_pre (-lit_of_last_trail_pol M', D')›
by (subst lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id, of M M'])
(use M'_M trail_nempty in ‹auto simp: lit_of_hd_trail_def›)
have ‹- lit_of (hd M) ∈# (the D)›
using uL_D by (auto simp: S)
then have extract_shorter_conflict_wl_alt_def:
‹extract_shorter_conflict_wl (M, N, D, NE, UE, NS, US, Q, W) = do {
let K = lit_of (hd M);
let D = (remove1_mset (-K) (the D));
_ ← RETURN (); ⌦‹vmtf rescoring›
E' ← (SPEC
(λ(E'). E' ⊆# add_mset (-K) D ∧ - lit_of (hd M) :# E' ∧
mset `# ran_mf N +
(get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
(get_subsumed_learned_clauses_wl S +
get_subsumed_init_clauses_wl S)) ⊨pm E'));
D ← RETURN (Some E');
RETURN (M, N, D, NE, UE, NS, US, Q, W)
}›
unfolding extract_shorter_conflict_wl_def
by (auto simp: RES_RETURN_RES image_iff mset_take_mset_drop_mset' S union_assoc
Un_commute Let_def Un_assoc sup_left_commute)
have lookup_clause_rel_unique: ‹(D', a) ∈ lookup_clause_rel 𝒜 ⟹ (D', b) ∈ lookup_clause_rel 𝒜 ⟹ a = b›
for a b 𝒜
by (auto simp: lookup_clause_rel_def mset_as_position_right_unique)
have isa_minimize_and_extract_highest_lookup_conflict:
‹isa_minimize_and_extract_highest_lookup_conflict M' arena
(lookup_conflict_remove1 (-lit_of (hd M)) D') cach lbd (outl[0 := - lit_of (hd M)])
≤ ⇓ {((E, s, outl), E').
(E, mset (tl outl)) ∈ lookup_clause_rel (all_atms_st S) ∧
mset outl = E' ∧
outl ! 0 = - lit_of (hd M) ∧
E' ⊆# the D ∧ outl ≠ [] ∧ distinct outl ∧ literals_are_in_ℒ⇩i⇩n (all_atms_st S) (mset outl) ∧
¬tautology (mset outl) ∧
(∃cach'. (s, cach') ∈ cach_refinement (all_atms_st S))}
(SPEC (λE'. E' ⊆# add_mset (- lit_of (hd M)) (remove1_mset (- lit_of (hd M)) (the D)) ∧
- lit_of (hd M) ∈# E' ∧
mset `# ran_mf N +
(get_unit_learned_clss_wl S + get_unit_init_clss_wl S +
(get_subsumed_learned_clauses_wl S +
get_subsumed_init_clauses_wl S)) ⊨pm
E'))›
(is ‹_ ≤ ⇓ ?minimize (RES ?E)›)
apply (rule order_trans)
apply (rule
isa_minimize_and_extract_highest_lookup_conflict_minimize_and_extract_highest_lookup_conflict
[THEN fref_to_Down_curry5,
of ‹all_atms_st S› M N ‹remove1_mset (-lit_of (hd M)) (the D)› cach' lbd ‹outl[0 := - lit_of (hd M)]›
_ _ _ _ _ _ ‹set vdom›])
subgoal using bounded by (auto simp: S all_atms_def)
subgoal using tauto_confl' pre2 by auto
subgoal using D' not_none arena S_T uL_D uM_ℒ⇩a⇩l⇩l not_empty D' L_D b cach_empty M'_M unfolding all_atms_def
by (auto simp: option_lookup_clause_rel_def S state_wl_l_def image_image cach_refinement_empty_def cach'_def
intro!: lookup_conflict_remove1[THEN fref_to_Down_unRET_uncurry]
dest: multi_member_split lookup_clause_rel_unique)
apply (rule order_trans)
apply (rule mini[THEN ref_two_step'])
subgoal
using uL_D dist_D tauto_D ℒ⇩i⇩n_S ℒ⇩i⇩n_D tauto_D L_D
by (fastforce simp: conc_fun_chain conc_fun_RES image_iff S union_assoc insert_subset_eq_iff
neq_Nil_conv literals_are_in_ℒ⇩i⇩n_add_mset tautology_add_mset
intro: literals_are_in_ℒ⇩i⇩n_mono
dest: distinct_mset_mono not_tautology_mono
dest!: multi_member_split)
done
have empty_conflict_and_extract_clause_heur: ‹isa_empty_conflict_and_extract_clause_heur M' x1 x2a
≤ ⇓ ({((E, outl, n), E').
(E, None) ∈ option_lookup_clause_rel (all_atms_st S) ∧
mset outl = the E' ∧
outl ! 0 = - lit_of (hd M) ∧
the E' ⊆# the D ∧ outl ≠ [] ∧ E' ≠ None ∧
(1 < length outl ⟶
highest_lit M (mset (tl outl)) (Some (outl ! 1, get_level M (outl ! 1)))) ∧
(1 < length outl ⟶ n = get_level M (outl ! 1)) ∧ (length outl = 1 ⟶ n = 0)}) (RETURN (Some E'))›
(is ‹_ ≤ ⇓ ?empty_conflict _›)
if
‹M ≠ []› and
‹- lit_of (hd M) ∈# ℒ⇩a⇩l⇩l (all_atms_st S)› and
‹0 < length outl› and
‹lookup_conflict_remove1_pre (- lit_of (hd M), D')› and
‹(x, E') ∈ ?minimize› and
‹E' ∈ ?E› and
‹x2 = (x1a, x2a)› and
‹x = (x1, x2)›
for x :: ‹(nat × bool option list) × (minimize_status list × nat list) × nat literal list› and
E' :: ‹nat literal multiset› and
x1 :: ‹nat × bool option list› and
x2 :: ‹(minimize_status list × nat list) × nat literal list› and
x1a :: ‹minimize_status list × nat list› and
x2a :: ‹nat literal list›
proof -
show ?thesis
apply (rule order_trans)
apply (rule isa_empty_conflict_and_extract_clause_heur_empty_conflict_and_extract_clause_heur
[THEN fref_to_Down_curry2, of _ _ _ M x1 x2a ‹all_atms_st S›])
apply fast
subgoal using M'_M by auto
apply (subst Down_id_eq)
apply (rule order.trans)
apply (rule empty_conflict_and_extract_clause_heur_empty_conflict_and_extract_clause[of ‹mset (tl x2a)›])
subgoal by auto
subgoal using that by auto
subgoal using that by auto
subgoal using that by auto
subgoal using that by auto
subgoal using that by auto
subgoal using bounded unfolding S all_atms_def by simp
subgoal unfolding empty_conflict_and_extract_clause_def
using that
by (auto simp: conc_fun_RES RETURN_def)
done
qed
have final: ‹(((M', arena, x1b, Q', W', vm', clvls, empty_cach_ref x1a, lbd, take 1 x2a,
stats, heur, vdom, avdom, lcount, opts),
x2c, x1c),
M, N, Da, NE, UE, NS, US, Q, W)
∈ ?shorter›
if
‹M ≠ []› and
‹- lit_of (hd M) ∈# ℒ⇩a⇩l⇩l (all_atms_st S)› and
‹0 < length outl› and
‹lookup_conflict_remove1_pre (- lit_of (hd M), D')› and
mini: ‹(x, E') ∈ ?minimize› and
‹E' ∈ ?E› and
‹(xa, Da) ∈ ?empty_conflict› and
st[simp]:
‹x2b = (x1c, x2c)›
‹x2 = (x1a, x2a)›
‹x = (x1, x2)›
‹xa = (x1b, x2b)› and
vm': ‹(vm', uu) ∈ {(c, uu). c ∈ isa_vmtf (all_atms_st S) M}›
for x E' x1 x2 x1a x2a xa Da x1b x2b x1c x2c vm' uu
proof -
have x1b_None: ‹(x1b, None) ∈ option_lookup_clause_rel (all_atms_st S)›
using that apply (auto simp: S simp flip: all_atms_def)
done
have cach[simp]: ‹cach_refinement_empty (all_atms_st S) (empty_cach_ref x1a)›
using empty_cach_ref_empty_cach[of ‹all_atms_st S›, THEN fref_to_Down_unRET, of x1a]
mini bounded
by (auto simp add: cach_refinement_empty_def empty_cach_def cach'_def S
simp flip: all_atms_def)
have
out: ‹out_learned M None (take (Suc 0) x2a)› and
x1c_Da: ‹mset x1c = the Da› and
Da_None: ‹Da ≠ None› and
Da_D: ‹the Da ⊆# the D› and
x1c_D: ‹mset x1c ⊆# the D› and
x1c: ‹x1c ≠ []› and
hd_x1c: ‹hd x1c = - lit_of (hd M)› and
highest: ‹Suc 0 < length x1c ⟹ x2c = get_level M (x1c ! 1) ∧
highest_lit M (mset (tl x1c))
(Some (x1c ! Suc 0, get_level M (x1c ! Suc 0)))› and
highest2: ‹length x1c = Suc 0 ⟹ x2c = 0› and
‹E' = mset x2a› and
‹- lit_of (M ! 0) ∈ set x2a› and
‹(λx. mset (fst x)) ` set_mset (ran_m N) ∪
(set_mset (get_unit_learned_clss_wl S) ∪
set_mset (get_unit_init_clss_wl S)) ∪
(set_mset (get_subsumed_learned_clauses_wl S) ∪
set_mset (get_subsumed_init_clauses_wl S)) ⊨p
mset x2a› and
‹x2a ! 0 = - lit_of (M ! 0)› and
‹x1c ! 0 = - lit_of (M ! 0)› and
‹mset x2a ⊆# the D› and
‹mset x1c ⊆# the D› and
‹x2a ≠ []› and
x1c_nempty: ‹x1c ≠ []› and
‹distinct x2a› and
Da: ‹Da = Some (mset x1c)› and
‹literals_are_in_ℒ⇩i⇩n (all_atms_st S) (mset x2a)› and
‹¬ tautology (mset x2a)›
using that
unfolding out_learned_def
by (auto simp add: hd_conv_nth S ac_simps simp flip: all_atms_def)
have Da_D': ‹remove1_mset (- lit_of (hd M)) (the Da) ⊆# remove1_mset (- lit_of (hd M)) (the D)›
using Da_D mset_le_subtract by blast
have K: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant (state⇩W_of U)›
using stgy_invs unfolding twl_stgy_invs_def by fast
have ‹get_maximum_level M {#L ∈# the D. get_level M L < count_decided M#}
< count_decided M›
using cdcl⇩W_restart_mset.no_skip_no_resolve_level_get_maximum_lvl_le[OF nss nsr all_struct K]
not_none not_empty confl trail_nempty S_T T_U
unfolding get_maximum_level_def by (auto simp: twl_st S)
then have
‹get_maximum_level M (remove1_mset (- lit_of (hd M)) (the D)) < count_decided M›
by (subst D_filter) auto
then have max_lvl_le:
‹get_maximum_level M (remove1_mset (- lit_of (hd M)) (the Da)) < count_decided M›
using get_maximum_level_mono[OF Da_D', of M] by auto
have ‹((M', arena, x1b, Q', W', vm', clvls, empty_cach_ref x1a, lbd, take (Suc 0) x2a,
stats, heur, vdom, avdom, lcount, opts),
del_conflict_wl (M, N, Da, NE, UE, NS, US, Q, W))
∈ twl_st_heur_bt›
using S'_S x1b_None cach out vm' unfolding twl_st_heur_bt_def
by (auto simp: twl_st_heur_def del_conflict_wl_def S S' twl_st_heur_bt_def
twl_st_heur_conflict_ana_def S simp flip: all_atms_def)
moreover have x2c: ‹x2c = get_maximum_level M (remove1_mset (- lit_of (hd M)) (the Da))›
using highest highest2 x1c_nempty hd_x1c
by (cases ‹length x1c = Suc 0›; cases x1c)
(auto simp: highest_lit_def Da mset_tl)
moreover have ‹literals_are_ℒ⇩i⇩n (all_atms_st S) (M, N, Some (mset x1c), NE, UE, NS, US, Q, W)›
using ℒ⇩i⇩n
by (auto simp: S x2c literals_are_ℒ⇩i⇩n_def blits_in_ℒ⇩i⇩n_def simp flip: all_atms_def)
moreover have ‹¬tautology (mset x1c)›
using tauto_confl not_tautology_mono[OF x1c_D]
by (auto simp: S x2c S')
ultimately show ?thesis
using ℒ⇩i⇩n_S x1c_Da Da_None dist_D D_none x1c_D x1c hd_x1c highest uM_ℒ⇩a⇩l⇩l vm' M_ℒ⇩i⇩n
max_lvl_le corr trail_nempty unfolding literals_are_ℒ⇩i⇩n_def
by (simp add: S x2c S')
qed
have hd_M'_M: ‹lit_of_last_trail_pol M' = lit_of (hd M)›
by (subst lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id, of M M'])
(use M'_M trail_nempty in ‹auto simp: lit_of_hd_trail_def›)
have vmtf_mark_to_rescore_also_reasons:
‹isa_vmtf_mark_to_rescore_also_reasons M' arena (outl[0 := - lit_of (hd M)]) vm
≤ SPEC (λc. (c, ()) ∈ {(c, _). c ∈ isa_vmtf (all_atms_st S) M})›
if
‹M ≠ []› and
‹literals_are_in_ℒ⇩i⇩n_trail (all_atms_st S) M› and
‹- lit_of (hd M) ∈# ℒ⇩a⇩l⇩l (all_atms_st S)› and
‹0 < length outl› and
‹lookup_conflict_remove1_pre (- lit_of (hd M), D')›
proof -
have outl_hd_tl: ‹outl[0 := - lit_of (hd M)] = - lit_of (hd M) # tl (outl[0 := - lit_of (hd M)])› and
[simp]: ‹outl ≠ []›
using outl unfolding out_learned_def
by (cases outl; auto; fail)+
have uM_D: ‹- lit_of (hd M) ∈# the D›
by (subst D_filter) auto
have mset_outl_D: ‹mset (outl[0 := - lit_of (hd M)]) = (the D)›
by (subst outl_hd_tl, subst mset.simps, subst tl_outl_D, subst D_filter)
(use uM_D D_filter[symmetric] in auto)
from arg_cong[OF this, of set_mset] have set_outl_D: ‹set (outl[0 := - lit_of (hd M)]) = set_mset (the D)›
by auto
have outl_Lall: ‹∀L∈set (outl[0 := - lit_of (hd M)]). L ∈# ℒ⇩a⇩l⇩l (all_atms_st S)›
using ℒ⇩i⇩n_S unfolding set_outl_D
by (auto simp: S all_lits_of_m_add_mset
all_atms_def literals_are_in_ℒ⇩i⇩n_def literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l
dest: multi_member_split)
have ‹distinct (outl[0 := - lit_of (hd M)])› using dist_D by(auto simp: S mset_outl_D[symmetric])
then have length_outl: ‹length outl ≤ uint32_max›
using bounded tauto_confl ℒ⇩i⇩n_S simple_clss_size_upper_div2[OF bounded, of ‹mset (outl[0 := - lit_of (hd M)])›]
by (auto simp: out_learned_def S mset_outl_D[symmetric] uint32_max_def simp flip: all_atms_def)
have lit_annots: ‹∀L∈set (outl[0 := - lit_of (hd M)]).
∀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 (all_atms_st S))›
unfolding set_outl_D
apply (intro ballI allI impI conjI)
subgoal
using list_invs S_T unfolding twl_list_invs_def
by (auto simp: S)
subgoal for L C i
using list_invs S_T arena lits_N literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[of ‹(all_atms_st S)› N C ‹i - C›]
unfolding twl_list_invs_def
by (auto simp: S arena_lifting all_atms_def[symmetric])
done
obtain vm0 where
vm_vm0: ‹(vm, vm0) ∈ Id ×⇩f distinct_atoms_rel (all_atms_st S)› and
vm0: ‹vm0 ∈ vmtf (all_atms_st S) M›
using vm by (cases vm) (auto simp: isa_vmtf_def S simp flip: all_atms_def)
show ?thesis
apply (cases vm)
apply (rule order.trans,
rule isa_vmtf_mark_to_rescore_also_reasons_vmtf_mark_to_rescore_also_reasons[of ‹all_atms_st S›,
THEN fref_to_Down_curry3,
of _ _ _ vm M arena ‹outl[0 := - lit_of (hd M)]› vm0])
subgoal using bounded S by (auto simp: all_atms_def)
subgoal using vm arena M'_M vm_vm0 by (auto simp: isa_vmtf_def)[]
apply (rule order.trans, rule ref_two_step')
apply (rule vmtf_mark_to_rescore_also_reasons_spec[OF vm0 arena _ outl_Lall lit_annots])
subgoal using length_outl by auto
by (auto simp: isa_vmtf_def conc_fun_RES S all_atms_def)
qed
show ?thesis
unfolding extract_shorter_conflict_list_heur_st_def
empty_conflict_and_extract_clause_def S S' prod.simps hd_M'_M
apply (rewrite at ‹let _ = list_update _ _ _ in _ ›Let_def)
apply (rewrite at ‹let _ = empty_cach_ref _ in _ › Let_def)
apply (subst extract_shorter_conflict_wl_alt_def)
apply (refine_vcg isa_minimize_and_extract_highest_lookup_conflict
empty_conflict_and_extract_clause_heur)
subgoal using trail_nempty using M'_M by (auto simp: trail_pol_def ann_lits_split_reasons_def)
subgoal using ‹0 < length outl› .
subgoal unfolding hd_M'_M[symmetric] by (rule lookup_conflict_remove1_pre)
apply (rule vmtf_mark_to_rescore_also_reasons; assumption?)
subgoal using trail_nempty .
subgoal using pre2 by (auto simp: S all_atms_def)
subgoal using uM_ℒ⇩a⇩l⇩l by (auto simp: S all_atms_def)
subgoal premises p
using bounded p(5,7-) by (auto simp: S empty_cach_ref_pre_def cach_refinement_alt_def
intro!: IsaSAT_Lookup_Conflict.bounded_included_le simp: all_atms_def simp del: isasat_input_bounded_def)
subgoal by auto
subgoal using bounded pre2
by (auto dest!: simple_clss_size_upper_div2 simp: uint32_max_def S all_atms_def[symmetric]
simp del: isasat_input_bounded_def)
subgoal using trail_nempty by fast
subgoal using uM_ℒ⇩a⇩l⇩l .
apply assumption+
subgoal
using trail_nempty uM_ℒ⇩a⇩l⇩l
unfolding S[symmetric] S'[symmetric]
by (rule final)
done
qed
have find_decomp_wl_nlit: ‹find_decomp_wl_st_int n T
≤ ⇓ {(U, U''). (U, U'') ∈ twl_st_heur_bt ∧ equality_except_trail_wl U'' T' ∧
(∃K M2. (Decided K # (get_trail_wl U''), M2) ∈ set (get_all_ann_decomposition (get_trail_wl T')) ∧
get_level (get_trail_wl T') K = get_maximum_level (get_trail_wl T') (the (get_conflict_wl T') - {#-lit_of (hd (get_trail_wl T'))#}) + 1 ∧
get_clauses_wl_heur U = get_clauses_wl_heur S) ∧
(get_trail_wl U'', get_vmtf_heur U) ∈ (Id ×⇩f (Id ×⇩f (distinct_atoms_rel (all_atms_st T'))¯)) ``
(Collect (find_decomp_w_ns_prop (all_atms_st T') (get_trail_wl T') n (get_vmtf_heur T)))}
(find_decomp_wl LK' T')›
(is ‹_ ≤ ⇓ ?find_decomp _›)
if
‹(S, S') ∈ ?R› and
‹backtrack_wl_inv S'› and
‹backtrack_wl_D_heur_inv S› and
TT': ‹(TnC, T') ∈ ?shorter S' S› and
[simp]: ‹nC = (n, C)› and
[simp]: ‹TnC = (T, nC)› and
KK': ‹(LK, LK') ∈ {(L, L'). L = L' ∧ L = lit_of (hd (get_trail_wl S'))}›
for S S' TnC T' T nC n C LK LK'
proof -
obtain M N D NE UE NS US Q W where
T': ‹T' = (M, N, D, NE, UE, NS, US, Q, W)›
by (cases T')
obtain M' W' vm clvls cach lbd outl stats arena D' Q' where
T: ‹T = (M', arena, D', Q', W', vm, clvls, cach, lbd, outl, stats)›
using TT' by (cases T) (auto simp: twl_st_heur_bt_def T' del_conflict_wl_def)
have
vm: ‹vm ∈ isa_vmtf (all_atms_st T') M› and
M'M: ‹(M', M) ∈ trail_pol (all_atms_st T')› and
lits_trail: ‹literals_are_in_ℒ⇩i⇩n_trail (all_atms_st T') (get_trail_wl T')›
using TT' by (auto simp: twl_st_heur_bt_def del_conflict_wl_def
all_atms_def[symmetric] T T')
obtain vm0 where
vm: ‹(vm, vm0) ∈ Id ×⇩r distinct_atoms_rel (all_atms_st T')› and
vm0: ‹vm0 ∈ vmtf (all_atms_st T') M›
using vm unfolding isa_vmtf_def by (cases vm) auto
have [simp]:
‹LK' = lit_of (hd (get_trail_wl T'))›
‹LK = LK'›
using KK' TT' by (auto simp: equality_except_conflict_wl_get_trail_wl)
have n: ‹n = get_maximum_level M (remove1_mset (- lit_of (hd M)) (mset C))› and
eq: ‹equality_except_conflict_wl T' S'› and
‹the D = mset C› ‹D ≠ None› and
clss_eq: ‹get_clauses_wl_heur S = arena› and
n: ‹n < count_decided (get_trail_wl T')› and
bounded: ‹isasat_input_bounded (all_atms_st T')› and
T_T': ‹(T, del_conflict_wl T') ∈ twl_st_heur_bt› and
n2: ‹n = get_maximum_level M (remove1_mset (- lit_of (hd M)) (the D))›
using TT' KK' by (auto simp: T T' twl_st_heur_bt_def del_conflict_wl_def simp flip: all_atms_def
simp del: isasat_input_bounded_def)
have [simp]: ‹get_trail_wl S' = M›
using eq ‹the D = mset C› ‹D ≠ None› by (cases S'; auto simp: T')
have [simp]: ‹get_clauses_wl_heur S = arena›
using TT' by (auto simp: T T')
have n_d: ‹no_dup M›
using M'M unfolding trail_pol_def by auto
have [simp]: ‹NO_MATCH [] M ⟹ out_learned M None ai ⟷ out_learned [] None ai› for M ai
by (auto simp: out_learned_def)
show ?thesis
unfolding T' find_decomp_wl_st_int_def prod.case T
apply (rule bind_refine_res)
prefer 2
apply (rule order.trans)
apply (rule isa_find_decomp_wl_imp_find_decomp_wl_imp[THEN fref_to_Down_curry2, of M n vm0
_ _ _ ‹all_atms_st T'›])
subgoal using n by (auto simp: T')
subgoal using M'M vm by auto
apply (rule order.trans)
apply (rule ref_two_step')
apply (rule find_decomp_wl_imp_le_find_decomp_wl')
subgoal using vm0 .
subgoal using lits_trail by (auto simp: T')
subgoal using n by (auto simp: T')
subgoal using n_d .
subgoal using bounded .
unfolding find_decomp_w_ns_def conc_fun_RES
apply (rule order.refl)
using T_T' n_d
apply (cases ‹get_vmtf_heur T›)
apply (auto simp: find_decomp_wl_def twl_st_heur_bt_def T T' del_conflict_wl_def
dest: no_dup_appendD
simp flip: all_atms_def n2
intro!: RETURN_RES_refine
intro: isa_vmtfI)
apply (rule_tac x=an in exI)
apply (auto dest: no_dup_appendD intro: isa_vmtfI simp: T')
apply (auto simp: Image_iff T')
done
qed
have fst_find_lit_of_max_level_wl: ‹RETURN (C ! 1)
≤ ⇓ Id
(find_lit_of_max_level_wl U' LK')›
if
‹(S, S') ∈ ?R› and
‹backtrack_wl_inv S'› and
‹backtrack_wl_D_heur_inv S› and
TT': ‹(TnC, T') ∈ ?shorter S' S› and
[simp]: ‹nC = (n, C)› and
[simp]: ‹TnC = (T, nC)› and
find_decomp: ‹(U, U') ∈ ?find_decomp S T' n› and
size_C: ‹1 < length C› and
size_conflict_U': ‹1 < size (the (get_conflict_wl U'))› and
KK': ‹(LK, LK') ∈ {(L, L'). L = L' ∧ L = lit_of (hd (get_trail_wl S'))}›
for S S' TnC T' T nC n C U U' LK LK'
proof -
obtain M N NE UE Q W NS US where
T': ‹T' = (M, N, Some (mset C), NE, UE, NS, US, Q, W)› and
‹C ≠ []›
using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› find_decomp
apply (cases U'; cases T'; cases S')
by (auto simp: find_lit_of_max_level_wl_def)
obtain M' K M2 where
U': ‹U' = (M', N, Some (mset C), NE, UE, NS, US, Q, W)› and
decomp: ‹(Decided K # M', M2) ∈ set (get_all_ann_decomposition M)› and
lev_K: ‹get_level M K = Suc (get_maximum_level M (remove1_mset (- lit_of (hd M)) (the (Some (mset C)))))›
using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› find_decomp
by (cases U'; cases S')
(auto simp: find_lit_of_max_level_wl_def T')
have [simp]:
‹LK' = lit_of (hd (get_trail_wl T'))›
‹LK = LK'›
using KK' TT' by (auto simp: equality_except_conflict_wl_get_trail_wl)
have n_d: ‹no_dup (get_trail_wl S')›
using ‹(S, S') ∈ ?R›
by (auto simp: twl_st_heur_conflict_ana_def trail_pol_def)
have [simp]: ‹get_trail_wl S' = get_trail_wl T'›
using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› find_decomp
by (cases T'; cases S'; auto simp: find_lit_of_max_level_wl_def U'; fail)+
have [simp]: ‹remove1_mset (- lit_of (hd M)) (mset C) = mset (tl C)›
apply (subst mset_tl)
using ‹(TnC, T') ∈ ?shorter S' S›
by (auto simp: find_lit_of_max_level_wl_def U' highest_lit_def T')
have n_d: ‹no_dup M›
using ‹(TnC, T') ∈ ?shorter S' S› n_d unfolding T'
by (cases S') auto
have nempty[iff]: ‹remove1_mset (- lit_of (hd M)) (the (Some(mset C))) ≠ {#}›
using U' T' find_decomp size_C by (cases C) (auto simp: remove1_mset_empty_iff)
have H[simp]: ‹aa ∈# remove1_mset (- lit_of (hd M)) (the (Some(mset C))) ⟹
get_level M' aa = get_level M aa› for aa
apply (rule get_all_ann_decomposition_get_level[of ‹lit_of (hd M)› _ K _ M2 ‹the (Some(mset C))›])
subgoal ..
subgoal by (rule n_d)
subgoal by (rule decomp)
subgoal by (rule lev_K)
subgoal by simp
done
have ‹get_maximum_level M (remove1_mset (- lit_of (hd M)) (mset C)) =
get_maximum_level M' (remove1_mset (- lit_of (hd M)) (mset C))›
by (rule get_maximum_level_cong) auto
then show ?thesis
using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› hd_conv_nth[OF ‹C ≠ []›, symmetric]
by (auto simp: find_lit_of_max_level_wl_def U' highest_lit_def T')
qed
have propagate_bt_wl_D_heur: ‹propagate_bt_wl_D_heur LK C U
≤ ⇓ ?S (propagate_bt_wl LK' L' U')›
if
SS': ‹(S, S') ∈ ?R› and
‹backtrack_wl_inv S'› and
‹backtrack_wl_D_heur_inv S› and
‹(TnC, T') ∈ ?shorter S' S› and
[simp]: ‹nC = (n, C)› and
[simp]: ‹TnC = (T, nC)› and
find_decomp: ‹(U, U') ∈ ?find_decomp S T' n› and
le_C: ‹1 < length C› and
‹1 < size (the (get_conflict_wl U'))› and
C_L': ‹(C ! 1, L') ∈ nat_lit_lit_rel› and
KK': ‹(LK, LK') ∈ {(L, L'). L = L' ∧ L = lit_of (hd (get_trail_wl S'))}›
for S S' TnC T' T nC n C U U' L' LK LK'
proof -
have
TT': ‹(T, del_conflict_wl T') ∈ twl_st_heur_bt› and
n: ‹n = get_maximum_level (get_trail_wl T')
(remove1_mset (- lit_of (hd (get_trail_wl T'))) (mset C))› and
T_C: ‹get_conflict_wl T' = Some (mset C)› and
T'S': ‹equality_except_conflict_wl T' S'› and
C_nempty: ‹C ≠ []› and
hd_C: ‹hd C = - lit_of (hd (get_trail_wl T'))› and
highest: ‹highest_lit (get_trail_wl T') (mset (tl C))
(Some (C ! Suc 0, get_level (get_trail_wl T') (C ! Suc 0)))› and
incl: ‹mset C ⊆# the (get_conflict_wl S')› and
dist_S': ‹distinct_mset (the (get_conflict_wl S'))› and
list_confl_S': ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (the (get_conflict_wl S'))› and
‹get_conflict_wl S' ≠ None› and
uM_ℒ⇩a⇩l⇩l: ‹-lit_of (hd (get_trail_wl S')) ∈# ℒ⇩a⇩l⇩l (all_atms_st S')› and
lits: ‹literals_are_ℒ⇩i⇩n (all_atms_st T') T'› and
tr_nempty: ‹get_trail_wl T' ≠ []› and
r: ‹length (get_clauses_wl_heur S) = r› ‹length (get_clauses_wl_heur T) = r› and
corr: ‹correct_watching S'›
using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› ‹(S, S') ∈ ?R›
by auto
obtain K M2 where
UU': ‹(U, U') ∈ twl_st_heur_bt› and
U'U': ‹equality_except_trail_wl U' T'› and
lev_K: ‹get_level (get_trail_wl T') K = Suc (get_maximum_level (get_trail_wl T')
(remove1_mset (- lit_of (hd (get_trail_wl T')))
(the (get_conflict_wl T'))))› and
decomp: ‹(Decided K # get_trail_wl U', M2) ∈ set (get_all_ann_decomposition (get_trail_wl T'))› and
r': ‹length (get_clauses_wl_heur U) = r› and
S_arena: ‹get_clauses_wl_heur U = get_clauses_wl_heur S›
using find_decomp r
by auto
obtain M N NE UE Q NS US W where
T': ‹T' = (M, N, Some (mset C), NE, UE, NS, US, Q, W)› and
‹C ≠ []›
using TT' T_C ‹1 < length C›
apply (cases T'; cases S')
by (auto simp: find_lit_of_max_level_wl_def)
obtain D where
S': ‹S' = (M, N, D, NE, UE, NS, US, Q, W)›
using T'S' ‹1 < length C›
apply (cases S')
by (auto simp: find_lit_of_max_level_wl_def T' del_conflict_wl_def)
obtain M1 where
U': ‹U' = (M1, N, Some (mset C), NE, UE, NS, US, Q, W)› and
lits_confl: ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (mset C)› and
‹mset C ⊆# the (get_conflict_wl S')› and
tauto: ‹¬ tautology (mset C)›
using ‹(TnC, T') ∈ ?shorter S' S› ‹1 < length C› find_decomp
apply (cases U')
by (auto simp: find_lit_of_max_level_wl_def T' intro: literals_are_in_ℒ⇩i⇩n_mono)
obtain M1' vm' W' clvls cach lbd outl stats heur avdom vdom lcount arena D'
Q' opts
where
U: ‹U = (M1', arena, D', Q', W', vm', clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, [])›
using UU' find_decomp by (cases U) (auto simp: U' T' twl_st_heur_bt_def all_atms_def[symmetric])
have [simp]:
‹LK' = lit_of (hd M)›
‹LK = LK'›
using KK' SS' by (auto simp: equality_except_conflict_wl_get_trail_wl S')
have
M1'_M1: ‹(M1', M1) ∈ trail_pol (all_atms_st U')› and
W'W: ‹(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms_st U'))› and
vmtf: ‹vm' ∈ isa_vmtf (all_atms_st U') M1› and
n_d_M1: ‹no_dup M1› and
empty_cach: ‹cach_refinement_empty (all_atms_st U') cach› and
‹length outl = Suc 0› and
outl: ‹out_learned M1 None outl› and
vdom: ‹vdom_m (all_atms_st U') W N ⊆ set vdom› and
lcount: ‹lcount = size (learned_clss_l N)› and
vdom_m: ‹vdom_m (all_atms_st U') W N ⊆ set vdom› and
D': ‹(D', None) ∈ option_lookup_clause_rel (all_atms_st U')› and
valid: ‹valid_arena arena N (set vdom)› and
avdom: ‹mset avdom ⊆# mset vdom› and
bounded: ‹isasat_input_bounded (all_atms_st U')› and
nempty: ‹isasat_input_nempty (all_atms_st U')› and
dist_vdom: ‹distinct vdom› and
heur: ‹heuristic_rel (all_atms_st U') heur›
using UU' by (auto simp: out_learned_def twl_st_heur_bt_def U U' all_atms_def[symmetric])
have [simp]: ‹C ! 1 = L'› ‹C ! 0 = - lit_of (hd M)› and
n_d: ‹no_dup M›
using SS' C_L' hd_C ‹C ≠ []› by (auto simp: S' U' T' twl_st_heur_conflict_ana_def hd_conv_nth)
have undef: ‹undefined_lit M1 (lit_of (hd M))›
using decomp n_d
by (auto dest!: get_all_ann_decomposition_exists_prepend simp: T' hd_append U' neq_Nil_conv
split: if_splits)
have C_1_neq_hd: ‹C ! Suc 0 ≠ - lit_of (hd M)›
using distinct_mset_mono[OF incl dist_S'] C_L' ‹1 < length C› ‹C ! 0 = - lit_of (hd M)›
by (cases C; cases ‹tl C›) (auto simp del: ‹C ! 0 = - lit_of (hd M)›)
have H: ‹(RES ((λi. (fmupd i (C, False) N, i)) ` {i. 0 < i ∧ i ∉# dom_m N}) ⤜
(λ(N, i). ASSERT (i ∈# dom_m N) ⤜ (λ_. f N i))) =
(RES ((λi. (fmupd i (C, False) N, i)) ` {i. 0 < i ∧ i ∉# dom_m N}) ⤜
(λ(N, i). f N i))› (is ‹?A = ?B›) for f C N
proof -
have ‹?B ≤ ?A›
by (force intro: ext complete_lattice_class.Sup_subset_mono
simp: intro_spec_iff bind_RES)
moreover have ‹?A ≤ ?B›
by (force intro: ext complete_lattice_class.Sup_subset_mono
simp: intro_spec_iff bind_RES)
ultimately show ?thesis by auto
qed
have propagate_bt_wl_D_heur_alt_def:
‹propagate_bt_wl_D_heur = (λL C (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts). do {
ASSERT(length vdom ≤ length N0);
ASSERT(length avdom ≤ length N0);
ASSERT(nat_of_lit (C!1) < length W0 ∧ nat_of_lit (-L) < length W0);
ASSERT(length C > 1);
let L' = C!1;
ASSERT (length C ≤ uint32_max div 2 + 1);
vm ← isa_vmtf_rescore C M vm0;
glue ← get_LBD lbd;
let _ = C;
let b = False;
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ append_and_length_fast_code_pre ((b, C), N0));
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ lcount < sint64_max);
(N, i) ← fm_add_new b C N0;
ASSERT(update_lbd_pre ((i, glue), N));
let N = update_lbd i glue N;
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ length_ll W0 (nat_of_lit (-L)) < sint64_max);
let W = W0[nat_of_lit (- L) := W0 ! nat_of_lit (- L) @ [(i, L', length C = 2)]];
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ length_ll W (nat_of_lit L') < sint64_max);
let W = W[nat_of_lit L' := W!nat_of_lit L' @ [(i, -L, length C = 2)]];
lbd ← lbd_empty lbd;
ASSERT(isa_length_trail_pre M);
let j = isa_length_trail M;
ASSERT(i ≠ DECISION_REASON);
ASSERT(cons_trail_Propagated_tr_pre ((-L, i), M));
M ← cons_trail_Propagated_tr (- L) i M;
vm ← isa_vmtf_flush_int M vm;
heur ← mop_save_phase_heur (atm_of L') (is_neg L') heur;
RETURN (M, N, D, j, W, vm, 0,
cach, lbd, outl, add_lbd (of_nat glue) stats, update_heuristics glue heur, vdom @ [ i],
avdom @ [i], Suc lcount, opts)
})›
unfolding propagate_bt_wl_D_heur_def Let_def
by auto
have find_new_alt: ‹SPEC
(λ(N', i). N' = fmupd i (D'', False) N ∧ 0 < i ∧
i ∉# dom_m N ∧
(∀L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE) + (NS + US)).
i ∉ fst ` set (W L))) = do {
i ← SPEC
(λi. 0 < i ∧
i ∉# dom_m N ∧
(∀L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE) + (NS + US)).
i ∉ fst ` set (W L)));
N' ← RETURN (fmupd i (D'', False) N);
RETURN (N', i)
}› for D''
by (auto simp: RETURN_def RES_RES_RETURN_RES2
RES_RES_RETURN_RES)
have propagate_bt_wl_D_alt_def:
‹propagate_bt_wl LK' L' U' = do {
ASSERT (propagate_bt_wl_pre LK' L' (M1, N, Some (mset C), NE, UE, NS, US, Q, W));
_ ← RETURN (); ⌦‹phase saving›
_ ← RETURN (); ⌦‹LBD›
D'' ←
list_of_mset2 (- LK') L'
(the (Some (mset C)));
(N, i) ← SPEC
(λ(N', i). N' = fmupd i (D'', False) N ∧ 0 < i ∧
i ∉# dom_m N ∧
(∀L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE) + (NS + US)).
i ∉ fst ` set (W L)));
_ ← RETURN (); ⌦‹lbd empty›
_ ← RETURN (); ⌦‹lbd empty›
M2 ← cons_trail_propagate_l (- LK') i M1;
_ ← RETURN (); ⌦‹vmtf_flush›
_ ← RETURN (); ⌦‹heur›
RETURN
(M2,
N, None, NE, UE, NS, US, {#LK'#},
W(- LK' := W (- LK') @ [(i, L', length D'' = 2)],
L' := W L' @ [(i, - LK', length D'' = 2)]))
}›
unfolding propagate_bt_wl_def Let_def find_new_alt nres_monad3
U U' H get_fresh_index_wl_def prod.case
propagate_bt_wl_def Let_def rescore_clause_def
by (auto simp: U' RES_RES2_RETURN_RES RES_RETURN_RES uminus_𝒜⇩i⇩n_iff
uncurry_def RES_RES_RETURN_RES length_list_ge2 C_1_neq_hd
get_fresh_index_def RES_RETURN_RES2 RES_RES_RETURN_RES2 list_of_mset2_def
cons_trail_propagate_l_def
intro!: bind_cong[OF refl]
simp flip: all_lits_alt_def2 all_lits_alt_def all_lits_def)
have [refine0]: ‹SPEC (λ(vm'). vm' ∈ vmtf 𝒜 M1)
≤ ⇓{((vm'), ()). vm' ∈ vmtf 𝒜 M1 } (RETURN ())› for 𝒜
by (auto intro!: RES_refine simp: RETURN_def)
obtain vm0 where
vm: ‹(vm', vm0) ∈ Id ×⇩r distinct_atoms_rel (all_atms_st U')› and
vm0: ‹vm0 ∈ vmtf (all_atms_st U') M1›
using vmtf unfolding isa_vmtf_def by (cases vm') auto
have [refine0]:
‹isa_vmtf_rescore C M1' vm' ≤ SPEC (λc. (c, ()) ∈ {((vm), _).
vm ∈ isa_vmtf (all_atms_st U') M1})›
apply (rule order.trans)
apply (rule isa_vmtf_rescore[of ‹all_atms_st U'›, THEN fref_to_Down_curry2, of _ _ _ C M1 vm0])
subgoal using bounded by auto
subgoal using vm M1'_M1 by auto
apply (rule order.trans)
apply (rule ref_two_step')
apply (rule vmtf_rescore_score_clause[THEN fref_to_Down_curry2, of ‹all_atms_st U'› C M1 vm0])
subgoal using vm0 lits_confl by (auto simp: S' U')
subgoal using vm M1'_M1 by auto
subgoal by (auto simp: rescore_clause_def conc_fun_RES intro!: isa_vmtfI)
done
have [refine0]: ‹isa_vmtf_flush_int Ma vm ≤
SPEC(λc. (c, ()) ∈ {(vm', _). vm' ∈ isa_vmtf (all_atms_st U') M2})›
if vm: ‹vm ∈ isa_vmtf (all_atms_st U') M1› and
Ma: ‹(Ma, M2)
∈ {(M0, M0'').
(M0, M0'') ∈ trail_pol (all_atms_st U') ∧
M0'' = Propagated (- L) i # M1 ∧
no_dup M0''}›
for vm i L Ma M2
proof -
let ?M1' = ‹cons_trail_Propagated_tr L i M1'›
let ?M1 = ‹Propagated (-L) i # M1›
have M1'_M1: ‹(Ma, M2) ∈ trail_pol (all_atms_st U')›
using Ma by auto
have vm: ‹vm ∈ isa_vmtf (all_atms_st U') ?M1›
using vm by (auto simp: isa_vmtf_def dest: vmtf_consD)
obtain vm0 where
vm: ‹(vm, vm0) ∈ Id ×⇩r distinct_atoms_rel (all_atms_st U')› and
vm0: ‹vm0 ∈ vmtf (all_atms_st U') ?M1›
using vm unfolding isa_vmtf_def by (cases vm) auto
show ?thesis
apply (rule order.trans)
apply (rule isa_vmtf_flush_int[THEN fref_to_Down_curry, of _ _ ?M1 vm])
apply ((solves ‹use M1'_M1 Ma in auto›)+)[2]
apply (subst Down_id_eq)
apply (rule order.trans)
apply (rule vmtf_change_to_remove_order'[THEN fref_to_Down_curry, of ‹all_atms_st U'› ?M1 vm0 ?M1 vm])
subgoal using vm0 bounded nempty by auto
subgoal using vm by auto
subgoal using Ma by (auto simp: vmtf_flush_def conc_fun_RES RETURN_def intro: isa_vmtfI)
done
qed
have [refine0]: ‹(isa_length_trail M1', ()) ∈ {(j, _). j = length M1}›
by (subst isa_length_trail_length_u[THEN fref_to_Down_unRET_Id, OF _ M1'_M1]) auto
have [refine0]: ‹get_LBD lbd ≤ ⇓ {(_, _). True}(RETURN ())›
unfolding get_LBD_def by (auto intro!: RES_refine simp: RETURN_def)
have [refine0]: ‹RETURN C
≤ ⇓ Id
(list_of_mset2 (- LK') L'
(the (Some (mset C))))›
using that
by (auto simp: list_of_mset2_def S')
have [simp]: ‹0 < header_size D''› for D''
by (auto simp: header_size_def)
have [simp]: ‹length arena + header_size D'' ∉ set vdom›
‹length arena + header_size D'' ∉ vdom_m (all_atms_st U') W N›
‹length arena + header_size D'' ∉# dom_m N› for D''
using valid_arena_in_vdom_le_arena(1)[OF valid] vdom
by (auto 5 1 simp: vdom_m_def)
have add_new_alt_def: ‹(SPEC
(λ(N', i).
N' = fmupd i (D'', False) N ∧
0 < i ∧
i ∉# dom_m N ∧
(∀L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE) + (NS + US)).
i ∉ fst ` set (W L)))) =
(SPEC
(λ(N', i).
N' = fmupd i (D'', False) N ∧
0 < i ∧
i ∉ vdom_m (all_atms_st U') W N))› for D''
using lits
by (auto simp: T' vdom_m_def literals_are_ℒ⇩i⇩n_def is_ℒ⇩a⇩l⇩l_def U' all_atms_def
all_lits_def ac_simps)
have [refine0]: ‹fm_add_new False C arena
≤ ⇓ {((arena', i), (N', i')). valid_arena arena' N' (insert i (set vdom)) ∧ i = i' ∧
i ∉# dom_m N ∧ i ∉ set vdom ∧ length arena' = length arena + header_size D'' + length D''}
(SPEC
(λ(N', i).
N' = fmupd i (D'', False) N ∧
0 < i ∧
i ∉# dom_m N ∧
(∀L∈#all_lits_of_mm (mset `# ran_mf N + (NE + UE) + (NS + US)).
i ∉ fst ` set (W L))))›
if ‹(C, D'') ∈ Id› for D''
apply (subst add_new_alt_def)
apply (rule order_trans)
apply (rule fm_add_new_append_clause)
using that valid le_C vdom
by (auto simp: intro!: RETURN_RES_refine valid_arena_append_clause)
have [refine0]:
‹lbd_empty lbd ≤ SPEC (λc. (c, ()) ∈ {(c, _). c = replicate (length lbd) False})›
by (auto simp: lbd_empty_def)
have ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (mset C)›
using incl list_confl_S' literals_are_in_ℒ⇩i⇩n_mono by blast
then have C_Suc1_in: ‹C ! Suc 0 ∈# ℒ⇩a⇩l⇩l (all_atms_st S')›
using ‹1 < length C›
by (cases C; cases ‹tl C›) (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset)
then have ‹nat_of_lit (C ! Suc 0) < length W'› ‹nat_of_lit (- lit_of (hd (get_trail_wl S'))) < length W'› and
W'_eq: ‹W' ! (nat_of_lit (C ! Suc 0)) = W (C! Suc 0)›
‹W' ! (nat_of_lit (- lit_of (hd (get_trail_wl S')))) = W (- lit_of (hd (get_trail_wl S')))›
using uM_ℒ⇩a⇩l⇩l W'W unfolding map_fun_rel_def by (auto simp: image_image S' U')
have le_C_ge: ‹length C ≤ uint32_max div 2 + 1›
using clss_size_uint32_max[OF bounded, of ‹mset C›] ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (mset C)› list_confl_S'
dist_S' incl size_mset_mono[OF incl] distinct_mset_mono[OF incl]
simple_clss_size_upper_div2[OF bounded _ _ tauto]
by (auto simp: uint32_max_def S' U' all_atms_def[symmetric])
have tr_SS': ‹(get_trail_wl_heur S, M) ∈ trail_pol (all_atms_st S')›
using ‹(S, S') ∈ ?R› unfolding twl_st_heur_conflict_ana_def
by (auto simp: all_atms_def S')
have All_atms_rew: ‹set_mset (all_atms (fmupd x' (C', b) N) (NE + UE + NS + US)) =
set_mset (all_atms N (NE + UE + NS + US))› (is ?A)
‹trail_pol (all_atms (fmupd x' (C', b) N) (NE + UE + NS + US)) =
trail_pol (all_atms N (NE + UE + NS + US))› (is ?B)
‹isa_vmtf (all_atms (fmupd x' (C', b) N) (NE + UE + NS + US)) =
isa_vmtf (all_atms N (NE + UE + NS + US))› (is ?C)
‹option_lookup_clause_rel (all_atms (fmupd x' (C', b) N) (NE + UE + NS + US)) =
option_lookup_clause_rel (all_atms N (NE + UE + NS + US))› (is ?D)
‹⟨Id⟩map_fun_rel (D⇩0 (all_atms (fmupd x' (C', b) N) (NE + UE + NS + US))) =
⟨Id⟩map_fun_rel (D⇩0 (all_atms N (NE + UE + NS + US)))› (is ?E)
‹set_mset (ℒ⇩a⇩l⇩l (all_atms (fmupd x' (C', b) N) (NE + UE + NS + US))) =
set_mset (ℒ⇩a⇩l⇩l (all_atms N (NE + UE + NS + US)))›
‹phase_saving ((all_atms (fmupd x' (C', b) N) (NE + UE + NS + US))) =
phase_saving ((all_atms N (NE + UE + NS + US)))› (is ?F)
‹cach_refinement_empty ((all_atms (fmupd x' (C', b) N) (NE + UE + NS + US))) =
cach_refinement_empty ((all_atms N (NE + UE + NS + US)))› (is ?G)
‹cach_refinement_nonull ((all_atms (fmupd x' (C', b) N) (NE + UE + NS + US))) =
cach_refinement_nonull ((all_atms N (NE + UE + NS + US)))› (is ?G2)
‹vdom_m ((all_atms (fmupd x' (C', b) N) (NE + UE + NS + US))) =
vdom_m ((all_atms N (NE + UE + NS + US)))› (is ?H)
‹isasat_input_bounded ((all_atms (fmupd x' (C', b) N) (NE + UE + NS + US))) =
isasat_input_bounded ((all_atms N (NE + UE + NS + US)))› (is ?I)
‹isasat_input_nempty ((all_atms (fmupd x' (C', b) N) (NE + UE + NS + US))) =
isasat_input_nempty ((all_atms N (NE + UE + NS + US)))› (is ?J)
‹vdom_m (all_atms N (NE + UE + NS + US)) W (fmupd x' (C', b) N) =
insert x' (vdom_m (all_atms N (NE + UE + NS + US)) W N)› (is ?K)
‹heuristic_rel ((all_atms (fmupd x' (C', b) N) (NE + UE + NS + US))) =
heuristic_rel (all_atms N (NE + UE + NS + US))› (is ?L)
if ‹x' ∉# dom_m N› and C: ‹C' = C› for b x' C'
proof -
show A: ?A
using ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (mset C)› that
by (auto simp: all_atms_def all_lits_def ran_m_mapsto_upd_notin all_lits_of_mm_add_mset
U' S' in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n literals_are_in_ℒ⇩i⇩n_def ac_simps)
have A2: ‹set_mset (ℒ⇩a⇩l⇩l (all_atms (fmupd x' (C, b) N) (NE + UE + NS + US))) =
set_mset (ℒ⇩a⇩l⇩l (all_atms N (NE + UE + NS + US)))›
using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)
then show ‹set_mset (ℒ⇩a⇩l⇩l (all_atms (fmupd x' (C', b) N) (NE + UE + NS + US))) =
set_mset (ℒ⇩a⇩l⇩l (all_atms N (NE + UE + NS + US)))›
using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)
have A3: ‹set_mset (all_atms (fmupd x' (C, b) N) (NE + UE + NS + US)) =
set_mset (all_atms N (NE + UE + NS + US))›
using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)
show ?B and ?C and ?D and ?E and ?F and ?G and ?G2 and ?H and ?I and ?J and ?L
unfolding trail_pol_def A A2 ann_lits_split_reasons_def isasat_input_bounded_def
isa_vmtf_def vmtf_def distinct_atoms_rel_def vmtf_ℒ⇩a⇩l⇩l_def atms_of_def
distinct_hash_atoms_rel_def
atoms_hash_rel_def A A2 A3 C option_lookup_clause_rel_def
lookup_clause_rel_def phase_saving_def cach_refinement_empty_def
cach_refinement_def heuristic_rel_def
cach_refinement_list_def vdom_m_def
isasat_input_bounded_def
isasat_input_nempty_def cach_refinement_nonull_def
heuristic_rel_def phase_save_heur_rel_def
unfolding trail_pol_def[symmetric] ann_lits_split_reasons_def[symmetric]
isasat_input_bounded_def[symmetric]
vmtf_def[symmetric]
isa_vmtf_def[symmetric]
distinct_atoms_rel_def[symmetric]
vmtf_ℒ⇩a⇩l⇩l_def[symmetric] atms_of_def[symmetric]
distinct_hash_atoms_rel_def[symmetric]
atoms_hash_rel_def[symmetric]
option_lookup_clause_rel_def[symmetric]
lookup_clause_rel_def[symmetric]
phase_saving_def[symmetric] cach_refinement_empty_def[symmetric]
cach_refinement_def[symmetric] cach_refinement_nonull_def[symmetric]
cach_refinement_list_def[symmetric]
vdom_m_def[symmetric]
isasat_input_bounded_def[symmetric]
isasat_input_nempty_def[symmetric]
heuristic_rel_def[symmetric]
heuristic_rel_def[symmetric] phase_save_heur_rel_def[symmetric]
apply auto
done
show ?K
using that
by (auto simp: vdom_m_simps5 vdom_m_def)
qed
have [refine0]: ‹mop_save_phase_heur (atm_of (C ! 1)) (is_neg (C ! 1)) heur
≤ SPEC
(λc. (c, ())
∈ {(c, _). heuristic_rel (all_atms_st U') c})›
using heur uM_ℒ⇩a⇩l⇩l lits_confl le_C
literals_are_in_ℒ⇩i⇩n_in_mset_ℒ⇩a⇩l⇩l[of ‹all_atms_st S'› ‹mset C› ‹C!1›]
unfolding mop_save_phase_heur_def
by (auto intro!: ASSERT_leI save_phase_heur_preI simp: U' S')
have arena_le: ‹length arena + header_size C + length C ≤ 6 + r + uint32_max div 2›
using r r' le_C_ge by (auto simp: uint32_max_def header_size_def S' U)
have vm: ‹vm ∈ isa_vmtf (all_atms N (NE + UE)) M1 ⟹
vm ∈ isa_vmtf (all_atms N (NE + UE)) (Propagated (- lit_of (hd M)) x2a # M1)› for x2a vm
by (cases vm)
(auto intro!: vmtf_consD simp: isa_vmtf_def)
then show ?thesis
supply [[goals_limit=1]]
using empty_cach n_d_M1 C_L' W'W outl vmtf undef ‹1 < length C› lits
uM_ℒ⇩a⇩l⇩l vdom lcount vdom_m dist_vdom heur
apply (subst propagate_bt_wl_D_alt_def)
unfolding U U' H get_fresh_index_wl_def prod.case
propagate_bt_wl_D_heur_alt_def rescore_clause_def
apply (rewrite in ‹let _ = _!1 in _› Let_def)
apply (rewrite in ‹let _ = update_lbd _ _ _ in _› Let_def)
apply (rewrite in ‹let _ = list_update _ (nat_of_lit _) _ in _› Let_def)
apply (rewrite in ‹let _ = list_update _ (nat_of_lit _) _ in _› Let_def)
apply (rewrite in ‹let _ = False in _› Let_def)
apply (refine_rcg cons_trail_Propagated_tr2[of _ _ _ _ _ _ ‹all_atms_st U'›])
subgoal using valid by (auto dest!: valid_arena_vdom_subset)
subgoal using valid size_mset_mono[OF avdom] by (auto dest!: valid_arena_vdom_subset)
subgoal using ‹nat_of_lit (C ! Suc 0) < length W'› by simp
subgoal using ‹nat_of_lit (- lit_of (hd (get_trail_wl S'))) < length W'›
by (simp add: S' lit_of_hd_trail_def)
subgoal using le_C_ge .
subgoal by (auto simp: append_and_length_fast_code_pre_def isasat_fast_def
sint64_max_def uint32_max_def)
subgoal
using D' C_1_neq_hd vmtf avdom M1'_M1 size_learned_clss_dom_m[of N] valid_arena_size_dom_m_le_arena[OF valid]
by (auto simp: propagate_bt_wl_D_heur_def twl_st_heur_def lit_of_hd_trail_st_heur_def
phase_saving_def atms_of_def S' U' lit_of_hd_trail_def all_atms_def[symmetric] isasat_fast_def
sint64_max_def uint32_max_def)
subgoal for x uu x1 x2 vm uua_ glue uub D'' xa x'
by (auto simp: update_lbd_pre_def arena_is_valid_clause_idx_def)
subgoal using length_watched_le[of S' S ‹-lit_of_hd_trail M›] corr SS' uM_ℒ⇩a⇩l⇩l W'_eq S_arena
by (auto simp: isasat_fast_def length_ll_def S' U lit_of_hd_trail_def simp flip: all_atms_def)
subgoal using length_watched_le[of S' S ‹C ! Suc 0›] corr SS' W'_eq S_arena C_1_neq_hd C_Suc1_in
by (auto simp: length_ll_def S' U lit_of_hd_trail_def isasat_fast_def simp flip: all_atms_def)
subgoal
using M1'_M1 by (rule isa_length_trail_pre)
subgoal using D' C_1_neq_hd vmtf avdom
by (auto simp: DECISION_REASON_def
dest: valid_arena_one_notin_vdomD
intro!: vm)
subgoal
using M1'_M1
by (rule cons_trail_Propagated_tr_pre)
(use undef uM_ℒ⇩a⇩l⇩l in ‹auto simp: lit_of_hd_trail_def S' U' all_atms_def[symmetric]›)
subgoal using M1'_M1 by (auto simp: lit_of_hd_trail_def S' U' all_atms_def[symmetric])
subgoal using uM_ℒ⇩a⇩l⇩l by (auto simp: S' U' uminus_𝒜⇩i⇩n_iff lit_of_hd_trail_def)
subgoal
using D' C_1_neq_hd vmtf avdom
by (auto simp: propagate_bt_wl_D_heur_def twl_st_heur_def lit_of_hd_trail_st_heur_def
intro!: ASSERT_refine_left ASSERT_leI RES_refine exI[of _ C] valid_arena_update_lbd
dest: valid_arena_one_notin_vdomD
intro!: vm)
apply assumption
subgoal
supply All_atms_rew[simp]
unfolding twl_st_heur_def
using D' C_1_neq_hd vmtf avdom M1'_M1 bounded nempty r arena_le
by (clarsimp simp add: propagate_bt_wl_D_heur_def twl_st_heur_def
Let_def T' U' U rescore_clause_def S' map_fun_rel_def
list_of_mset2_def vmtf_flush_def RES_RES2_RETURN_RES RES_RETURN_RES uminus_𝒜⇩i⇩n_iff
get_fresh_index_def RES_RETURN_RES2 RES_RES_RETURN_RES2 lit_of_hd_trail_def
RES_RES_RETURN_RES lbd_empty_def get_LBD_def DECISION_REASON_def
all_atms_def[symmetric] All_atms_rew
intro!: valid_arena_update_lbd
simp del: isasat_input_bounded_def isasat_input_nempty_def
dest: valid_arena_one_notin_vdomD)
(intro conjI, clarsimp_all
intro!: valid_arena_update_lbd
simp del: isasat_input_bounded_def isasat_input_nempty_def
dest: valid_arena_one_notin_vdomD, auto simp:
dest: valid_arena_one_notin_vdomD
simp del: isasat_input_bounded_def isasat_input_nempty_def)
done
qed
have propagate_unit_bt_wl_D_int: ‹propagate_unit_bt_wl_D_int LK U
≤ ⇓ ?S
(propagate_unit_bt_wl LK' U')›
if
SS': ‹(S, S') ∈ ?R› and
‹backtrack_wl_inv S'› and
‹backtrack_wl_D_heur_inv S› and
‹(TnC, T') ∈ ?shorter S' S› and
[simp]: ‹nC = (n, C)› and
[simp]: ‹TnC = (T, nC)› and
find_decomp: ‹(U, U') ∈ ?find_decomp S T' n› and
‹¬ 1 < length C› and
‹¬ 1 < size (the (get_conflict_wl U'))› and
KK': ‹(LK, LK') ∈ {(L, L'). L = L' ∧ L = lit_of (hd (get_trail_wl S'))}›
for S S' TnC T' T nC n C U U' LK LK'
proof -
have
TT': ‹(T, del_conflict_wl T') ∈ twl_st_heur_bt› and
n: ‹n = get_maximum_level (get_trail_wl T')
(remove1_mset (- lit_of (hd (get_trail_wl T'))) (mset C))› and
T_C: ‹get_conflict_wl T' = Some (mset C)› and
T'S': ‹equality_except_conflict_wl T' S'› and
‹C ≠ []› and
hd_C: ‹hd C = - lit_of (hd (get_trail_wl T'))› and
incl: ‹mset C ⊆# the (get_conflict_wl S')› and
dist_S': ‹distinct_mset (the (get_conflict_wl S'))› and
list_confl_S': ‹literals_are_in_ℒ⇩i⇩n (all_atms_st S') (the (get_conflict_wl S'))› and
‹get_conflict_wl S' ≠ None› and
‹C ≠ []› and
uL_M: ‹- lit_of (hd (get_trail_wl S')) ∈# ℒ⇩a⇩l⇩l (all_atms_st S')› and
tr_nempty: ‹get_trail_wl T' ≠ []›
using ‹(TnC, T') ∈ ?shorter S' S› ‹~1 < length C›
by (auto)
obtain K M2 where
UU': ‹(U, U') ∈ twl_st_heur_bt› and
U'U': ‹equality_except_trail_wl U' T'› and
lev_K: ‹get_level (get_trail_wl T') K = Suc (get_maximum_level (get_trail_wl T')
(remove1_mset (- lit_of (hd (get_trail_wl T')))
(the (get_conflict_wl T'))))› and
decomp: ‹(Decided K # get_trail_wl U', M2) ∈ set (get_all_ann_decomposition (get_trail_wl T'))› and
r: ‹length (get_clauses_wl_heur S) = r›
using find_decomp SS'
by (auto)
obtain M N NE UE NS US Q W where
T': ‹T' = (M, N, Some (mset C), NE, UE, NS, US, Q, W)›
using TT' T_C ‹¬1 < length C›
apply (cases T'; cases S')
by (auto simp: find_lit_of_max_level_wl_def)
obtain D' where
S': ‹S' = (M, N, D', NE, UE, NS, US, Q, W)›
using T'S'
apply (cases S')
by (auto simp: find_lit_of_max_level_wl_def T' del_conflict_wl_def)
obtain M1 where
U': ‹U' = (M1, N, Some (mset C), NE, UE, NS, US, Q, W)›
using ‹(TnC, T') ∈ ?shorter S' S› find_decomp
apply (cases U')
by (auto simp: find_lit_of_max_level_wl_def T')
have [simp]:
‹LK' = lit_of (hd (get_trail_wl T'))›
‹LK = LK'›
using KK' SS' S' by (auto simp: T')
obtain vm' W' clvls cach lbd outl stats heur vdom avdom lcount arena D' Q' opts
M1'
where
U: ‹U = (M1', arena, D', Q', W', vm', clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, [])› and
avdom: ‹mset avdom ⊆# mset vdom› and
r': ‹length (get_clauses_wl_heur U) = r›
using UU' find_decomp r by (cases U) (auto simp: U' T' twl_st_heur_bt_def)
have
M'M: ‹(M1', M1) ∈ trail_pol (all_atms_st U')› and
W'W: ‹(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms_st U'))› and
vmtf: ‹vm' ∈ isa_vmtf (all_atms_st U') M1› and
n_d_M1: ‹no_dup M1› and
empty_cach: ‹cach_refinement_empty (all_atms_st U') cach› and
‹length outl = Suc 0› and
outl: ‹out_learned M1 None outl› and
lcount: ‹lcount = size (learned_clss_l N)› and
vdom: ‹vdom_m (all_atms_st U') W N ⊆ set vdom› and
valid: ‹valid_arena arena N (set vdom)› and
D': ‹(D', None) ∈ option_lookup_clause_rel (all_atms_st U')› and
bounded: ‹isasat_input_bounded (all_atms_st U')› and
nempty: ‹isasat_input_nempty (all_atms_st U')› and
dist_vdom: ‹distinct vdom› and
heur: ‹heuristic_rel (all_atms_st U') heur›
using UU' by (auto simp: out_learned_def twl_st_heur_bt_def U U' all_atms_def[symmetric])
have [simp]: ‹C ! 0 = - lit_of (hd M)› and
n_d: ‹no_dup M›
using SS' hd_C ‹C ≠ []› by (auto simp: S' U' T' twl_st_heur_conflict_ana_def hd_conv_nth)
have undef: ‹undefined_lit M1 (lit_of (hd M))›
using decomp n_d
by (auto dest!: get_all_ann_decomposition_exists_prepend simp: T' hd_append U' neq_Nil_conv
split: if_splits)
have C: ‹C = [- lit_of (hd M)]›
using ‹C ≠ []› ‹C ! 0 = - lit_of (hd M)› ‹¬1 < length C›
by (cases C) (auto simp del: ‹C ! 0 = - lit_of (hd M)›)
have propagate_unit_bt_wl_alt_def:
‹propagate_unit_bt_wl = (λL (M, N, D, NE, UE, NS, US, Q, W). do {
ASSERT(L ∈# all_lits_st (M, N, D, NE, UE, NS, US, Q, W));
ASSERT(propagate_unit_bt_wl_pre L (M, N, D, NE, UE, NS, US, Q, W));
_ ← RETURN ();
_ ← RETURN ();
_ ← RETURN ();
_ ← RETURN ();
M ← cons_trail_propagate_l (-L) 0 M;
RETURN (M, N, None, NE, add_mset (the D) UE, NS, US, {#L#}, W)
})›
unfolding propagate_unit_bt_wl_def Let_def by (auto intro!: ext bind_cong[OF refl]
simp: propagate_unit_bt_wl_pre_def propagate_unit_bt_l_pre_def
single_of_mset_def RES_RETURN_RES image_iff)
have [refine0]:
‹lbd_empty lbd ≤ SPEC (λc. (c, ()) ∈ {(c, _). c = replicate (length lbd) False})›
by (auto simp: lbd_empty_def)
have [refine0]: ‹(isa_length_trail M1', ()) ∈ {(j, _). j = length M1}›
by (subst isa_length_trail_length_u[THEN fref_to_Down_unRET_Id, OF _ M'M]) auto
have [refine0]: ‹isa_vmtf_flush_int M1' vm' ≤
SPEC(λc. (c, ()) ∈ {(vm', _). vm' ∈ isa_vmtf (all_atms_st U') M1})›
for vm i L
proof -
obtain vm0 where
vm: ‹(vm', vm0) ∈ Id ×⇩r distinct_atoms_rel (all_atms_st U')› and
vm0: ‹vm0 ∈ vmtf (all_atms_st U') M1›
using vmtf unfolding isa_vmtf_def by (cases vm') auto
show ?thesis
apply (rule order.trans)
apply (rule isa_vmtf_flush_int[THEN fref_to_Down_curry, of _ _ M1 vm'])
apply ((solves ‹use M'M in auto›)+)[2]
apply (subst Down_id_eq)
apply (rule order.trans)
apply (rule vmtf_change_to_remove_order'[THEN fref_to_Down_curry, of ‹all_atms_st U'› M1 vm0 M1 vm'])
subgoal using vm0 bounded nempty by auto
subgoal using vm by auto
subgoal by (auto simp: vmtf_flush_def conc_fun_RES RETURN_def intro: isa_vmtfI)
done
qed
have [refine0]: ‹get_LBD lbd ≤ SPEC(λc. (c, ()) ∈ UNIV)›
by (auto simp: get_LBD_def)
have tr_S: ‹(get_trail_wl_heur S, M) ∈ trail_pol (all_atms_st S')›
using SS' by (auto simp: S' twl_st_heur_conflict_ana_def all_atms_def)
have hd_SM: ‹lit_of_last_trail_pol (get_trail_wl_heur S) = lit_of (hd M)›
unfolding lit_of_hd_trail_def lit_of_hd_trail_st_heur_def
by (subst lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id])
(use M'M tr_S tr_nempty in ‹auto simp: lit_of_hd_trail_def T' S'›)
have uL_M: ‹- lit_of (hd (get_trail_wl S')) ∈# ℒ⇩a⇩l⇩l (all_atms_st U')›
using uL_M by (simp add: S' U')
let ?NE = ‹add_mset {#- lit_of (hd M)#} (NE + UE + NS + US)›
have All_atms_rew: ‹set_mset (all_atms (N) (?NE)) =
set_mset (all_atms N (NE + UE + NS + US))› (is ?A)
‹trail_pol (all_atms (N) (?NE)) =
trail_pol (all_atms N (NE + UE + NS + US))› (is ?B)
‹isa_vmtf (all_atms (N) (?NE)) =
isa_vmtf (all_atms N (NE + UE + NS + US))› (is ?C)
‹option_lookup_clause_rel (all_atms (N) (?NE)) =
option_lookup_clause_rel (all_atms N (NE + UE + NS + US))› (is ?D)
‹⟨Id⟩map_fun_rel (D⇩0 (all_atms (N) (?NE))) =
⟨Id⟩map_fun_rel (D⇩0 (all_atms N (NE + UE + NS + US)))› (is ?E)
‹set_mset (ℒ⇩a⇩l⇩l (all_atms (N) (?NE))) =
set_mset (ℒ⇩a⇩l⇩l (all_atms N (NE + UE + NS + US)))›
‹phase_saving ((all_atms (N) (?NE))) =
phase_saving ((all_atms N (NE + UE + NS + US)))› (is ?F)
‹cach_refinement_empty ((all_atms (N) (?NE))) =
cach_refinement_empty ((all_atms N (NE + UE + NS + US)))› (is ?G)
‹vdom_m ((all_atms (N) (?NE))) =
vdom_m ((all_atms N (NE + UE + NS + US)))› (is ?H)
‹isasat_input_bounded ((all_atms (N) (?NE))) =
isasat_input_bounded ((all_atms N (NE + UE + NS + US)))› (is ?I)
‹isasat_input_nempty ((all_atms (N) (?NE))) =
isasat_input_nempty ((all_atms N (NE + UE + NS + US)))› (is ?J)
‹vdom_m (all_atms N ?NE) W (N) =
(vdom_m (all_atms N (NE + UE + NS + US)) W N)› (is ?K)
‹heuristic_rel ((all_atms (N) (?NE))) =
heuristic_rel ((all_atms N (NE + UE + NS + US)))› (is ?L)
for b x' C'
proof -
show A: ?A
using uL_M
apply (cases ‹hd M›)
by (auto simp: all_atms_def all_lits_def ran_m_mapsto_upd_notin all_lits_of_mm_add_mset
U' S' in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n literals_are_in_ℒ⇩i⇩n_def atm_of_eq_atm_of
all_lits_of_m_add_mset ac_simps lits_of_def)
have A2: ‹set_mset (ℒ⇩a⇩l⇩l (all_atms N (?NE))) =
set_mset (ℒ⇩a⇩l⇩l (all_atms N (NE + UE + NS + US)))›
using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)
then show ‹set_mset (ℒ⇩a⇩l⇩l (all_atms (N) (?NE))) =
set_mset (ℒ⇩a⇩l⇩l (all_atms N (NE + UE + NS + US)))›
using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)
have A3: ‹set_mset (all_atms N (?NE)) =
set_mset (all_atms N (NE + UE + NS + US))›
using A unfolding ℒ⇩a⇩l⇩l_def C by (auto simp: A)
show ?B and ?C and ?D and ?E and ?F and ?G and ?H and ?I and ?J and ?K and ?L
unfolding trail_pol_def A A2 ann_lits_split_reasons_def isasat_input_bounded_def
isa_vmtf_def vmtf_def distinct_atoms_rel_def vmtf_ℒ⇩a⇩l⇩l_def atms_of_def
distinct_hash_atoms_rel_def
atoms_hash_rel_def A A2 A3 C option_lookup_clause_rel_def
lookup_clause_rel_def phase_saving_def cach_refinement_empty_def
cach_refinement_def
cach_refinement_list_def vdom_m_def
isasat_input_bounded_def heuristic_rel_def
isasat_input_nempty_def cach_refinement_nonull_def vdom_m_def
phase_save_heur_rel_def phase_saving_def
unfolding trail_pol_def[symmetric] ann_lits_split_reasons_def[symmetric]
isasat_input_bounded_def[symmetric]
vmtf_def[symmetric]
isa_vmtf_def[symmetric]
distinct_atoms_rel_def[symmetric]
vmtf_ℒ⇩a⇩l⇩l_def[symmetric] atms_of_def[symmetric]
distinct_hash_atoms_rel_def[symmetric]
atoms_hash_rel_def[symmetric]
option_lookup_clause_rel_def[symmetric]
lookup_clause_rel_def[symmetric]
phase_saving_def[symmetric] cach_refinement_empty_def[symmetric]
cach_refinement_def[symmetric]
cach_refinement_list_def[symmetric]
vdom_m_def[symmetric]
isasat_input_bounded_def[symmetric] cach_refinement_nonull_def[symmetric]
isasat_input_nempty_def[symmetric] heuristic_rel_def[symmetric]
phase_save_heur_rel_def[symmetric] phase_saving_def[symmetric]
apply auto
done
qed
show ?thesis
using empty_cach n_d_M1 W'W outl vmtf C undef uL_M vdom lcount valid D' avdom
unfolding U U' propagate_unit_bt_wl_D_int_def prod.simps hd_SM
propagate_unit_bt_wl_alt_def
apply (rewrite at ‹let _ = incr_uset _ in _› Let_def)
apply (refine_rcg cons_trail_Propagated_tr2[where 𝒜 = ‹all_atms_st U'›])
subgoal using M'M by (rule isa_length_trail_pre)
subgoal by (auto simp: DECISION_REASON_def)
subgoal
using M'M by (rule cons_trail_Propagated_tr_pre)
(use undef uL_M in ‹auto simp: hd_SM all_atms_def[symmetric] T'
lit_of_hd_trail_def S'›)
subgoal
using M'M by (auto simp: U U' lit_of_hd_trail_st_heur_def RETURN_def
single_of_mset_def vmtf_flush_def twl_st_heur_def lbd_empty_def get_LBD_def
RES_RES2_RETURN_RES RES_RETURN_RES S' uminus_𝒜⇩i⇩n_iff RES_RES_RETURN_RES
DECISION_REASON_def hd_SM lit_of_hd_trail_st_heur_def
intro!: ASSERT_refine_left RES_refine exI[of _ ‹-lit_of (hd M)›]
intro!: vmtf_consD
simp del: isasat_input_bounded_def isasat_input_nempty_def)
subgoal
by (auto simp: U U' lit_of_hd_trail_st_heur_def RETURN_def
single_of_mset_def vmtf_flush_def twl_st_heur_def lbd_empty_def get_LBD_def
RES_RES2_RETURN_RES RES_RETURN_RES S' uminus_𝒜⇩i⇩n_iff RES_RES_RETURN_RES
DECISION_REASON_def hd_SM T'
intro!: ASSERT_refine_left RES_refine exI[of _ ‹-lit_of (hd M)›]
intro!: vmtf_consD
simp del: isasat_input_bounded_def isasat_input_nempty_def)
subgoal
using bounded nempty dist_vdom r' heur
by (auto simp: U U' lit_of_hd_trail_st_heur_def RETURN_def
single_of_mset_def vmtf_flush_def twl_st_heur_def lbd_empty_def get_LBD_def
RES_RES2_RETURN_RES RES_RETURN_RES S' uminus_𝒜⇩i⇩n_iff RES_RES_RETURN_RES
DECISION_REASON_def hd_SM All_atms_rew all_atms_def[symmetric]
intro!: ASSERT_refine_left RES_refine exI[of _ ‹-lit_of (hd M)›]
intro!: isa_vmtf_consD2
simp del: isasat_input_bounded_def isasat_input_nempty_def)
done
qed
have trail_nempty: ‹fst (get_trail_wl_heur S) ≠ []›
if
‹(S, S') ∈ ?R› and
‹backtrack_wl_inv S'›
for S S'
proof -
show ?thesis
using that unfolding backtrack_wl_inv_def backtrack_wl_D_heur_inv_def backtrack_l_inv_def backtrack_inv_def
backtrack_l_inv_def apply -
by normalize_goal+
(auto simp: twl_st_heur_conflict_ana_def trail_pol_def ann_lits_split_reasons_def)
qed
have [refine]: ‹⋀x y. (x, y)
∈ {(S, T).
(S, T) ∈ twl_st_heur_conflict_ana ∧
length (get_clauses_wl_heur S) = r} ⟹
lit_of_hd_trail_st_heur x
≤ ⇓ {(L, L'). L = L' ∧ L = lit_of (hd (get_trail_wl y))} (mop_lit_hd_trail_wl y)›
unfolding mop_lit_hd_trail_wl_def lit_of_hd_trail_st_heur_def
apply refine_rcg
subgoal unfolding mop_lit_hd_trail_wl_pre_def mop_lit_hd_trail_l_pre_def mop_lit_hd_trail_pre_def
by (auto simp: twl_st_heur_conflict_ana_def mop_lit_hd_trail_wl_pre_def mop_lit_hd_trail_l_pre_def trail_pol_alt_def
mop_lit_hd_trail_pre_def state_wl_l_def twl_st_l_def lit_of_hd_trail_def RETURN_RES_refine_iff)
subgoal for x y
apply simp_all
by (subst lit_of_last_trail_pol_lit_of_last_trail[THEN fref_to_Down_unRET_Id, of ‹get_trail_wl y› ‹get_trail_wl_heur x› ‹all_atms_st y›])
(auto simp: twl_st_heur_conflict_ana_def mop_lit_hd_trail_wl_pre_def mop_lit_hd_trail_l_pre_def
mop_lit_hd_trail_pre_def state_wl_l_def twl_st_l_def lit_of_hd_trail_def RETURN_RES_refine_iff)
done
have backtrack_wl_alt_def:
‹backtrack_wl S =
do {
ASSERT(backtrack_wl_inv S);
L ← mop_lit_hd_trail_wl S;
S ← extract_shorter_conflict_wl S;
S ← find_decomp_wl L S;
if size (the (get_conflict_wl S)) > 1
then do {
L' ← find_lit_of_max_level_wl S L;
S ← propagate_bt_wl L L' S;
RETURN S
}
else do {
propagate_unit_bt_wl L S
}
}› for S
unfolding backtrack_wl_def while.imonad2
by auto
have save_phase_st: ‹(xb, x') ∈ ?S ⟹
save_phase_st xb
≤ SPEC
(λc. (c, x')
∈ {(S, T).
(S, T) ∈ twl_st_heur ∧
length (get_clauses_wl_heur S)
≤ 6 + r + uint32_max div 2})› for xb x'
unfolding save_phase_st_def
apply (refine_vcg save_phase_heur_spec[THEN order_trans, of ‹all_atms_st x'›])
subgoal
by (rule isa_length_trail_pre[of _ ‹get_trail_wl x'› ‹all_atms_st x'›])
(auto simp: twl_st_heur_def)
subgoal
by (auto simp: twl_st_heur_def)
subgoal
by (auto simp: twl_st_heur_def)
done
show ?thesis
supply [[goals_limit=1]]
apply (intro frefI nres_relI)
unfolding backtrack_wl_D_nlit_heur_alt_def backtrack_wl_alt_def
apply (refine_rcg shorter)
subgoal by (rule inv)
subgoal by (rule trail_nempty)
subgoal for x y xa S x1 x2 x1a x2a
by (auto simp: twl_st_heur_state_simp equality_except_conflict_wl_get_clauses_wl)
apply (rule find_decomp_wl_nlit; assumption)
subgoal by (auto simp: twl_st_heur_state_simp equality_except_conflict_wl_get_clauses_wl
equality_except_trail_wl_get_clauses_wl)
subgoal for x y L La xa S x1 x2 x1a x2a Sa Sb
by (auto simp: twl_st_heur_state_simp equality_except_trail_wl_get_conflict_wl)
apply (rule fst_find_lit_of_max_level_wl; solves assumption)
apply (rule propagate_bt_wl_D_heur; assumption)
apply (rule save_phase_st; assumption)
apply (rule propagate_unit_bt_wl_D_int; assumption)
done
qed
section ‹Backtrack with direct extraction of literal if highest level›
lemma le_uint32_max_div_2_le_uint32_max: ‹a ≤ uint32_max div 2 + 1 ⟹ a ≤ uint32_max›
by (auto simp: uint32_max_def sint64_max_def)
lemma propagate_bt_wl_D_heur_alt_def:
‹propagate_bt_wl_D_heur = (λL C (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts). do {
ASSERT(length vdom ≤ length N0);
ASSERT(length avdom ≤ length N0);
ASSERT(nat_of_lit (C!1) < length W0 ∧ nat_of_lit (-L) < length W0);
ASSERT(length C > 1);
let L' = C!1;
ASSERT(length C ≤ uint32_max div 2 + 1);
vm ← isa_vmtf_rescore C M vm0;
glue ← get_LBD lbd;
let b = False;
let b' = (length C = 2);
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ append_and_length_fast_code_pre ((b, C), N0));
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ lcount < sint64_max);
(N, i) ← fm_add_new_fast b C N0;
ASSERT(update_lbd_pre ((i, glue), N));
let N = update_lbd i glue N;
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ length_ll W0 (nat_of_lit (-L)) < sint64_max);
let W = W0[nat_of_lit (- L) := W0 ! nat_of_lit (- L) @ [(i, L', b')]];
ASSERT(isasat_fast (M, N0, D, Q, W0, vm0, y, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts) ⟶ length_ll W (nat_of_lit L') < sint64_max);
let W = W[nat_of_lit L' := W!nat_of_lit L' @ [(i, -L, b')]];
lbd ← lbd_empty lbd;
ASSERT(isa_length_trail_pre M);
let j = isa_length_trail M;
ASSERT(i ≠ DECISION_REASON);
ASSERT(cons_trail_Propagated_tr_pre ((-L, i), M));
M ← cons_trail_Propagated_tr (- L) i M;
vm ← isa_vmtf_flush_int M vm;
heur ← mop_save_phase_heur (atm_of L') (is_neg L') heur;
RETURN (M, N, D, j, W, vm, 0,
cach, lbd, outl, add_lbd (of_nat glue) stats, update_heuristics glue heur, vdom @ [i],
avdom @ [i],
lcount + 1, opts)
})›
unfolding propagate_bt_wl_D_heur_def Let_def by (auto intro!: ext)
lemma propagate_bt_wl_D_fast_code_isasat_fastI2: ‹isasat_fast b ⟹
b = (a1', a2') ⟹
a2' = (a1'a, a2'a) ⟹
a < length a1'a ⟹ a ≤ sint64_max›
by (cases b) (auto simp: isasat_fast_def)
lemma propagate_bt_wl_D_fast_code_isasat_fastI3: ‹isasat_fast b ⟹
b = (a1', a2') ⟹
a2' = (a1'a, a2'a) ⟹
a ≤ length a1'a ⟹ a < sint64_max›
by (cases b) (auto simp: isasat_fast_def sint64_max_def uint32_max_def)
lemma lit_of_hd_trail_st_heur_alt_def:
‹lit_of_hd_trail_st_heur = (λ(M, N, D, Q, W, vm, φ). do {ASSERT (fst M ≠ []); RETURN (lit_of_last_trail_pol M)})›
by (auto simp: lit_of_hd_trail_st_heur_def lit_of_hd_trail_def intro!: ext)
end