theory Watched_Literals_Initialisation
imports Watched_Literals_List
begin
subsection ‹Initialise Data structure›
type_synonym 'v twl_st_init = ‹'v twl_st × 'v clauses›
fun get_trail_init :: ‹'v twl_st_init ⇒ ('v, 'v clause) ann_lit list› where
‹get_trail_init ((M, _, _, _, _, _, _), _) = M›
fun get_conflict_init :: ‹'v twl_st_init ⇒ 'v cconflict› where
‹get_conflict_init ((_, _, _, D, _, _, _, _), _) = D›
fun literals_to_update_init :: ‹'v twl_st_init ⇒ 'v clause› where
‹literals_to_update_init ((_, _, _, _, _, _, _, Q), _) = Q›
fun get_init_clauses_init :: ‹'v twl_st_init ⇒ 'v twl_cls multiset› where
‹get_init_clauses_init ((_, N, _, _, _, _, _, _), _) = N›
fun get_learned_clauses_init :: ‹'v twl_st_init ⇒ 'v twl_cls multiset› where
‹get_learned_clauses_init ((_, _, U, _, _, _, _, _), _) = U›
fun get_unit_init_clauses_init :: ‹'v twl_st_init ⇒ 'v clauses› where
‹get_unit_init_clauses_init ((_, _, _, _, NE, _, _, _), _) = NE›
fun get_unit_learned_clauses_init :: ‹'v twl_st_init ⇒ 'v clauses› where
‹get_unit_learned_clauses_init ((_, _, _, _, _, UE, _, _), _) = UE›
fun clauses_to_update_init :: ‹'v twl_st_init ⇒ ('v literal × 'v twl_cls) multiset› where
‹clauses_to_update_init ((_, _, _, _, _, _, WS, _), _) = WS›
fun other_clauses_init :: ‹'v twl_st_init ⇒ 'v clauses› where
‹other_clauses_init ((_, _, _, _, _, _, _), OC) = OC›
fun add_to_init_clauses :: ‹'v clause_l ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
‹add_to_init_clauses C ((M, N, U, D, NE, UE, WS, Q), OC) =
((M, add_mset (twl_clause_of C) N, U, D, NE, UE, WS, Q), OC)›
fun add_to_unit_init_clauses :: ‹'v clause ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
‹add_to_unit_init_clauses C ((M, N, U, D, NE, UE, WS, Q), OC) =
((M, N, U, D, add_mset C NE, UE, WS, Q), OC)›
fun set_conflict_init :: ‹'v clause_l ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
‹set_conflict_init C ((M, N, U, _, NE, UE, WS, Q), OC) =
((M, N, U, Some (mset C), add_mset (mset C) NE, UE, {#}, {#}), OC)›
fun propagate_unit_init :: ‹'v literal ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
‹propagate_unit_init L ((M, N, U, D, NE, UE, WS, Q), OC) =
((Propagated L {#L#} # M, N, U, D, add_mset {#L#} NE, UE, WS, add_mset (-L) Q), OC)›
fun add_empty_conflict_init :: ‹'v twl_st_init ⇒ 'v twl_st_init› where
‹add_empty_conflict_init ((M, N, U, D, NE, UE, WS, Q), OC) =
((M, N, U, Some {#}, NE, UE, WS, {#}), add_mset {#} OC)›
fun add_to_clauses_init :: ‹'v clause_l ⇒ 'v twl_st_init ⇒ 'v twl_st_init› where
‹add_to_clauses_init C ((M, N, U, D, NE, UE, WS, Q), OC) =
((M, add_mset (twl_clause_of C) N, U, D, NE, UE, WS, Q), OC)›
type_synonym 'v twl_st_l_init = ‹'v twl_st_l × 'v clauses›
fun get_trail_l_init :: ‹'v twl_st_l_init ⇒ ('v, nat) ann_lit list› where
‹get_trail_l_init ((M, _, _, _, _, _, _), _) = M›
fun get_conflict_l_init :: ‹'v twl_st_l_init ⇒ 'v cconflict› where
‹get_conflict_l_init ((_, _, D, _, _, _, _), _) = D›
fun get_unit_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
‹get_unit_clauses_l_init ((M, N, D, NE, UE, WS, Q), _) = NE + UE›
fun get_learned_unit_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
‹get_learned_unit_clauses_l_init ((M, N, D, NE, UE, WS, Q), _) = UE›
fun get_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses_l› where
‹get_clauses_l_init ((M, N, D, NE, UE, WS, Q), _) = N›
fun literals_to_update_l_init :: ‹'v twl_st_l_init ⇒ 'v clause› where
‹literals_to_update_l_init ((_, _, _, _, _, _, Q), _) = Q›
fun clauses_to_update_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses_to_update_l› where
‹clauses_to_update_l_init ((_, _, _, _, _, WS, _), _) = WS›
fun other_clauses_l_init :: ‹'v twl_st_l_init ⇒ 'v clauses› where
‹other_clauses_l_init ((_, _, _, _, _, _, _), OC) = OC›
fun state⇩W_of_init :: "'v twl_st_init ⇒ 'v cdcl⇩W_restart_mset" where
"state⇩W_of_init ((M, N, U, C, NE, UE, Q), OC) =
(M, clause `# N + NE + OC, clause `# U + UE, C)"
named_theorems twl_st_init ‹Convertion for inital theorems›
lemma [twl_st_init]:
‹get_conflict_init (S, QC) = get_conflict S›
‹get_trail_init (S, QC) = get_trail S›
‹clauses_to_update_init (S, QC) = clauses_to_update S›
‹literals_to_update_init (S, QC) = literals_to_update S›
by (solves ‹cases S; auto›)+
lemma [twl_st_init]:
‹clauses_to_update_init (add_to_unit_init_clauses (mset C) T) = clauses_to_update_init T›
‹literals_to_update_init (add_to_unit_init_clauses (mset C) T) = literals_to_update_init T›
‹get_conflict_init (add_to_unit_init_clauses (mset C) T) = get_conflict_init T›
apply (cases T; auto simp: twl_st_inv.simps; fail)+
done
lemma [twl_st_init]:
‹twl_st_inv (fst (add_to_unit_init_clauses (mset C) T)) ⟷ twl_st_inv (fst T)›
‹valid_enqueued (fst (add_to_unit_init_clauses (mset C) T)) ⟷ valid_enqueued (fst T)›
‹no_duplicate_queued (fst (add_to_unit_init_clauses (mset C) T)) ⟷ no_duplicate_queued (fst T)›
‹distinct_queued (fst (add_to_unit_init_clauses (mset C) T)) ⟷ distinct_queued (fst T)›
‹confl_cands_enqueued (fst (add_to_unit_init_clauses (mset C) T)) ⟷ confl_cands_enqueued (fst T)›
‹propa_cands_enqueued (fst (add_to_unit_init_clauses (mset C) T)) ⟷ propa_cands_enqueued (fst T)›
‹twl_st_exception_inv (fst (add_to_unit_init_clauses (mset C) T)) ⟷ twl_st_exception_inv (fst T)›
apply (cases T; auto simp: twl_st_inv.simps; fail)+
apply (cases ‹get_conflict_init T›; cases T;
auto simp: twl_st_inv.simps twl_exception_inv.simps; fail)+
done
lemma [twl_st_init]:
‹trail (state⇩W_of_init T) = get_trail_init T›
‹get_trail (fst T) = get_trail_init (T)›
‹conflicting (state⇩W_of_init T) = get_conflict_init T›
‹init_clss (state⇩W_of_init T) = clauses (get_init_clauses_init T) + get_unit_init_clauses_init T
+ other_clauses_init T›
‹learned_clss (state⇩W_of_init T) = clauses (get_learned_clauses_init T) +
get_unit_learned_clauses_init T›
‹conflicting (state⇩W_of (fst T)) = conflicting (state⇩W_of_init T)›
‹trail (state⇩W_of (fst T)) = trail (state⇩W_of_init T)›
‹clauses_to_update (fst T) = clauses_to_update_init T›
‹get_conflict (fst T) = get_conflict_init T›
‹literals_to_update (fst T) = literals_to_update_init T›
by (cases T; auto simp: cdcl⇩W_restart_mset_state; fail)+
definition twl_st_l_init :: ‹('v twl_st_l_init × 'v twl_st_init) set› where
‹twl_st_l_init = {(((M, N, C, NE, UE, WS, Q), OC), ((M', N', C', NE', UE', WS', Q'), OC')).
(M , M') ∈ convert_lits_l N (NE+UE) ∧
((N', C', NE', UE', WS', Q'), OC') =
((twl_clause_of `# init_clss_lf N, twl_clause_of `# learned_clss_lf N,
C, NE, UE, {#}, Q), OC)}›
lemma twl_st_l_init_alt_def:
‹(S, T) ∈ twl_st_l_init ⟷
(fst S, fst T) ∈ twl_st_l None ∧ other_clauses_l_init S = other_clauses_init T›
by (cases S; cases T) (auto simp: twl_st_l_init_def twl_st_l_def)
lemma [twl_st_init]:
assumes ‹(S, T) ∈ twl_st_l_init›
shows
‹get_conflict_init T = get_conflict_l_init S›
‹get_conflict (fst T) = get_conflict_l_init S›
‹literals_to_update_init T = literals_to_update_l_init S›
‹clauses_to_update_init T = {#}›
‹other_clauses_init T = other_clauses_l_init S›
‹lits_of_l (get_trail_init T) = lits_of_l (get_trail_l_init S)›
‹lit_of `# mset (get_trail_init T) = lit_of `# mset (get_trail_l_init S)›
by (use assms in ‹solves ‹cases S; auto simp: twl_st_l_init_def››)+
definition twl_struct_invs_init :: ‹'v twl_st_init ⇒ bool› where
‹twl_struct_invs_init S ⟷
(twl_st_inv (fst S) ∧
valid_enqueued (fst S) ∧
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of_init S) ∧
cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of_init S) ∧
twl_st_exception_inv (fst S) ∧
no_duplicate_queued (fst S) ∧
distinct_queued (fst S) ∧
confl_cands_enqueued (fst S) ∧
propa_cands_enqueued (fst S) ∧
(get_conflict_init S ≠ None ⟶ clauses_to_update_init S = {#} ∧ literals_to_update_init S = {#}) ∧
entailed_clss_inv (fst S) ∧
clauses_to_update_inv (fst S) ∧
past_invs (fst S))
›
lemma state⇩W_of_state⇩W_of_init:
‹other_clauses_init W = {#} ⟹ state⇩W_of (fst W) = state⇩W_of_init W›
by (cases W) auto
lemma twl_struct_invs_init_twl_struct_invs:
‹other_clauses_init W = {#} ⟹ twl_struct_invs_init W ⟹ twl_struct_invs (fst W)›
unfolding twl_struct_invs_def twl_struct_invs_init_def
apply (subst state⇩W_of_state⇩W_of_init; assumption?)+
apply (intro iffI impI conjI)
by (clarsimp simp: twl_st_init)+
lemma twl_struct_invs_init_add_mset:
assumes ‹twl_struct_invs_init (S, QC)› and [simp]: ‹distinct_mset C› and
count_dec: ‹count_decided (trail (state⇩W_of S)) = 0›
shows ‹twl_struct_invs_init (S, add_mset C QC)›
proof -
have
st_inv: ‹twl_st_inv S› and
valid: ‹valid_enqueued S› and
struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of_init (S, QC))› and
smaller: ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of_init (S, QC))› and
excep: ‹twl_st_exception_inv S› and
no_dup: ‹no_duplicate_queued S› and
dist: ‹distinct_queued S› and
cands_confl: ‹confl_cands_enqueued S› and
cands_propa: ‹propa_cands_enqueued S› and
confl: ‹get_conflict S ≠ None ⟶ clauses_to_update S = {#} ∧ literals_to_update S = {#}› and
unit: ‹entailed_clss_inv S› and
to_upd: ‹clauses_to_update_inv S› and
past: ‹past_invs S›
using assms unfolding twl_struct_invs_init_def fst_conv
by (auto simp add: twl_st_init)
show ?thesis
unfolding twl_struct_invs_init_def fst_conv
apply (intro conjI)
subgoal by (rule st_inv)
subgoal by (rule valid)
subgoal using struct count_dec no_dup
by (cases S)
(auto 5 5 simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def clauses_def
cdcl⇩W_restart_mset_state cdcl⇩W_restart_mset.no_strange_atm_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def cdcl⇩W_restart_mset.reasons_in_clauses_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def)
subgoal using smaller count_dec by (cases S)(auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def clauses_def
cdcl⇩W_restart_mset_state)
subgoal by (rule excep)
subgoal by (rule no_dup)
subgoal by (rule dist)
subgoal by (rule cands_confl)
subgoal by (rule cands_propa)
subgoal using confl by (auto simp: twl_st_init)
subgoal by (rule unit)
subgoal by (rule to_upd)
subgoal by (rule past)
done
qed
fun add_empty_conflict_init_l :: ‹'v twl_st_l_init ⇒ 'v twl_st_l_init› where
add_empty_conflict_init_l_def[simp del]:
‹add_empty_conflict_init_l ((M, N, D, NE, UE, WS, Q), OC) =
((M, N, Some {#}, NE, UE, WS, {#}), add_mset {#} OC)›
fun propagate_unit_init_l :: ‹'v literal ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init› where
propagate_unit_init_l_def[simp del]:
‹propagate_unit_init_l L ((M, N, D, NE, UE, WS, Q), OC) =
((Propagated L 0 # M, N, D, add_mset {#L#} NE, UE, WS, add_mset (-L) Q), OC)›
fun already_propagated_unit_init_l :: ‹'v clause ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init› where
already_propagated_unit_init_l_def[simp del]:
‹already_propagated_unit_init_l C ((M, N, D, NE, UE, WS, Q), OC) =
((M, N, D, add_mset C NE, UE, WS, Q), OC)›
fun set_conflict_init_l :: ‹'v clause_l ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init› where
set_conflict_init_l_def[simp del]:
‹set_conflict_init_l C ((M, N, _, NE, UE, WS, Q), OC) =
((M, N, Some (mset C), add_mset (mset C) NE, UE, {#}, {#}), OC)›
fun add_to_clauses_init_l :: ‹'v clause_l ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init nres› where
add_to_clauses_init_l_def[simp del]:
‹add_to_clauses_init_l C ((M, N, _, NE, UE, WS, Q), OC) = do {
i ← get_fresh_index N;
RETURN ((M, fmupd i (C, True) N, None, NE, UE, WS, Q), OC)
}›
fun add_to_other_init where
‹add_to_other_init C (S, OC) = (S, add_mset (mset C) OC)›
lemma fst_add_to_other_init [simp]: ‹fst (add_to_other_init a T) = fst T›
by (cases T) auto
definition init_dt_step :: ‹'v clause_l ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init nres› where
‹init_dt_step C S =
(case get_conflict_l_init S of
None ⇒
if length C = 0
then RETURN (add_empty_conflict_init_l S)
else if length C = 1
then
let L = hd C in
if undefined_lit (get_trail_l_init S) L
then RETURN (propagate_unit_init_l L S)
else if L ∈ lits_of_l (get_trail_l_init S)
then RETURN (already_propagated_unit_init_l (mset C) S)
else RETURN (set_conflict_init_l C S)
else
add_to_clauses_init_l C S
| Some D ⇒
RETURN (add_to_other_init C S))›
definition init_dt :: ‹'v clause_l list ⇒ 'v twl_st_l_init ⇒ 'v twl_st_l_init nres› where
‹init_dt CS S = nfoldli CS (λ_. True) init_dt_step S›
thm nfoldli.simps
definition init_dt_pre where
‹init_dt_pre CS SOC ⟷
(∃T. (SOC, T) ∈ twl_st_l_init ∧
(∀C ∈ set CS. distinct C) ∧
twl_struct_invs_init T ∧
clauses_to_update_l_init SOC = {#} ∧
(∀s∈set (get_trail_l_init SOC). ¬is_decided s) ∧
(get_conflict_l_init SOC = None ⟶
literals_to_update_l_init SOC = uminus `# lit_of `# mset (get_trail_l_init SOC)) ∧
twl_list_invs (fst SOC) ∧
twl_stgy_invs (fst T) ∧
(other_clauses_l_init SOC ≠ {#} ⟶ get_conflict_l_init SOC ≠ None))›
lemma init_dt_pre_ConsD: ‹init_dt_pre (a # CS) SOC ⟹ init_dt_pre CS SOC ∧ distinct a›
unfolding init_dt_pre_def
apply normalize_goal+
by fastforce
definition init_dt_spec where
‹init_dt_spec CS SOC SOC' ⟷
(∃T'. (SOC', T') ∈ twl_st_l_init ∧
twl_struct_invs_init T' ∧
clauses_to_update_l_init SOC' = {#} ∧
(∀s∈set (get_trail_l_init SOC'). ¬is_decided s) ∧
(get_conflict_l_init SOC' = None ⟶
literals_to_update_l_init SOC' = uminus `# lit_of `# mset (get_trail_l_init SOC')) ∧
(mset `# mset CS + mset `# ran_mf (get_clauses_l_init SOC) + other_clauses_l_init SOC +
get_unit_clauses_l_init SOC =
mset `# ran_mf (get_clauses_l_init SOC') + other_clauses_l_init SOC' +
get_unit_clauses_l_init SOC') ∧
learned_clss_lf (get_clauses_l_init SOC) = learned_clss_lf (get_clauses_l_init SOC') ∧
get_learned_unit_clauses_l_init SOC' = get_learned_unit_clauses_l_init SOC ∧
twl_list_invs (fst SOC') ∧
twl_stgy_invs (fst T') ∧
(other_clauses_l_init SOC' ≠ {#} ⟶ get_conflict_l_init SOC' ≠ None) ∧
({#} ∈# mset `# mset CS ⟶ get_conflict_l_init SOC' ≠ None) ∧
(get_conflict_l_init SOC ≠ None ⟶ get_conflict_l_init SOC = get_conflict_l_init SOC'))›
lemma twl_struct_invs_init_add_to_other_init:
assumes
dist: ‹distinct a› and
lev: ‹count_decided (get_trail (fst T)) = 0› and
invs: ‹twl_struct_invs_init T›
shows
‹twl_struct_invs_init (add_to_other_init a T)›
(is ?twl_struct_invs_init)
proof -
obtain M N U D NE UE Q OC WS where
T: ‹T = ((M, N, U, D, NE, UE, WS, Q), OC)›
by (cases T) auto
have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + NE + OC, clauses U + UE, D)›
using invs unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset (mset a) (clauses N + NE + OC), clauses U + UE, D)›
using dist
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
cdcl⇩W_restart_mset.reasons_in_clauses_def)
have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + NE + OC, clauses U + UE, D)›
using invs unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset (mset a) (clauses N + NE + OC),
clauses U + UE, D)›
using lev
by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
clauses_def T count_decided_0_iff)
show ?twl_struct_invs_init
using invs
unfolding twl_struct_invs_init_def T
unfolding fst_conv add_to_other_init.simps state⇩W_of_init.simps get_conflict.simps
by clarsimp
qed
lemma invariants_init_state:
assumes
lev: ‹count_decided (get_trail_init T) = 0› and
wf: ‹∀C ∈# get_clauses (fst T). struct_wf_twl_cls C› and
MQ: ‹literals_to_update_init T = uminus `# lit_of `# mset (get_trail_init T)› and
WS: ‹clauses_to_update_init T = {#}› and
n_d: ‹no_dup (get_trail_init T)›
shows ‹propa_cands_enqueued (fst T)› and ‹confl_cands_enqueued (fst T)› and ‹twl_st_inv (fst T)›
‹clauses_to_update_inv (fst T)› and ‹past_invs (fst T)› and ‹distinct_queued (fst T)› and
‹valid_enqueued (fst T)› and ‹twl_st_exception_inv (fst T)› and ‹no_duplicate_queued (fst T)›
proof -
obtain M N U NE UE OC D where
T: ‹T = ((M, N, U, D, NE, UE, {#}, uminus `# lit_of `# mset M), OC)›
using MQ WS by (cases T) auto
let ?Q = ‹uminus `# lit_of `# mset M›
have [iff]: ‹M = M' @ Decided K # Ma ⟷ False› for M' K Ma
using lev by (auto simp: count_decided_0_iff T)
have struct: ‹struct_wf_twl_cls C› if ‹C ∈# N + U› for C
using wf that by (simp add: T twl_st_inv.simps)
let ?T = ‹fst T›
have [simp]: ‹propa_cands_enqueued ?T› if D: ‹D = None›
unfolding propa_cands_enqueued.simps Ball_def T fst_conv D
apply - apply (intro conjI impI allI)
subgoal for x C
using struct[of C]
apply (case_tac C; auto simp: uminus_lit_swap lits_of_def size_2_iff
true_annots_true_cls_def_iff_negation_in_model Ball_def remove1_mset_add_mset_If
all_conj_distrib conj_disj_distribR ex_disj_distrib
split: if_splits)
done
done
then show ‹propa_cands_enqueued ?T›
by (cases D) (auto simp: T)
have [simp]: ‹confl_cands_enqueued ?T› if D: ‹D = None›
unfolding confl_cands_enqueued.simps Ball_def T D fst_conv
apply - apply (intro conjI impI allI)
subgoal for x
using struct[of x]
by (case_tac x; case_tac ‹watched x›; auto simp: uminus_lit_swap lits_of_def)
done
then show ‹confl_cands_enqueued ?T›
by (cases D) (auto simp: T)
have [simp]: ‹get_level M L = 0› for L
using lev by (auto simp: T count_decided_0_iff)
show [simp]: ‹twl_st_inv ?T›
unfolding T fst_conv twl_st_inv.simps Ball_def
apply - apply (intro conjI impI allI)
subgoal using wf by (auto simp: T)
subgoal for C
by (cases C)
(auto simp: T twl_st_inv.simps twl_lazy_update.simps twl_is_an_exception_def
lits_of_def uminus_lit_swap)
subgoal for C
using lev by (cases C)
(auto simp: T twl_st_inv.simps twl_lazy_update.simps)
done
have [simp]: ‹{#C ∈# N. clauses_to_update_prop {#- lit_of x. x ∈# mset M#} M (L, C)#} = {#}›
for L N
by (auto simp: filter_mset_empty_conv clauses_to_update_prop.simps lits_of_def
uminus_lit_swap)
have ‹clauses_to_update_inv ?T› if D: ‹D = None›
unfolding T D
by (auto simp: filter_mset_empty_conv lits_of_def uminus_lit_swap)
then show ‹clauses_to_update_inv (fst T)›
by (cases D) (auto simp: T)
show ‹past_invs ?T›
by (auto simp: T past_invs.simps)
show ‹distinct_queued ?T›
using WS n_d by (auto simp: T no_dup_distinct_uminus)
show ‹valid_enqueued ?T›
using lev by (auto simp: T lits_of_def)
show ‹twl_st_exception_inv (fst T)›
unfolding T fst_conv twl_st_exception_inv.simps Ball_def
apply - apply (intro conjI impI allI)
apply (case_tac x; cases D)
by (auto simp: T twl_exception_inv.simps lits_of_def uminus_lit_swap)
show ‹no_duplicate_queued (fst T)›
by (auto simp: T)
qed
lemma twl_struct_invs_init_init_state:
assumes
lev: ‹count_decided (get_trail_init T) = 0› and
wf: ‹∀C ∈# get_clauses (fst T). struct_wf_twl_cls C› and
MQ: ‹literals_to_update_init T = uminus `# lit_of `# mset (get_trail_init T)› and
WS: ‹clauses_to_update_init T = {#}› and
struct_invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of_init T)› and
‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of_init T)› and
‹entailed_clss_inv (fst T)› and
‹get_conflict_init T ≠ None ⟶ clauses_to_update_init T = {#} ∧ literals_to_update_init T = {#}›
shows ‹twl_struct_invs_init T›
proof -
have n_d: ‹no_dup (get_trail_init T)›
using struct_invs unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def by (cases T) (auto simp: trail.simps)
then show ?thesis
using invariants_init_state[OF lev wf MQ WS n_d] assms unfolding twl_struct_invs_init_def
by fast+
qed
lemma twl_struct_invs_init_add_to_unit_init_clauses:
assumes
dist: ‹distinct a› and
lev: ‹count_decided (get_trail (fst T)) = 0› and
invs: ‹twl_struct_invs_init T› and
ex: ‹∃L ∈ set a. L ∈ lits_of_l (get_trail_init T)›
shows
‹twl_struct_invs_init (add_to_unit_init_clauses (mset a) T)›
(is ?all_struct)
proof -
obtain M N U D NE UE Q OC WS where
T: ‹T = ((M, N, U, D, NE, UE, WS, Q), OC)›
by (cases T) auto
have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + NE + OC, clauses U + UE, D)›
using invs unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset (mset a) (clauses N + NE + OC), clauses U + UE, D)›
using twl_struct_invs_init_add_to_other_init[OF dist lev invs]
unfolding T twl_struct_invs_init_def
by simp
have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + NE + OC, clauses U + UE, D)›
using invs unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset (mset a) (clauses N + NE + OC),
clauses U + UE, D)›
using lev
by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
clauses_def T count_decided_0_iff)
have [simp]: ‹confl_cands_enqueued (M, N, U, D, add_mset (mset a) NE, UE, WS, Q) ⟷
confl_cands_enqueued (M, N, U, D, NE, UE, WS, Q)›
‹propa_cands_enqueued (M, N, U, D, add_mset (mset a) NE, UE, WS, Q) ⟷
propa_cands_enqueued (M, N, U, D, NE, UE, WS, Q)›
‹twl_st_inv (M, N, U, D, add_mset (mset a) NE, UE, WS, Q) ⟷
twl_st_inv (M, N, U, D, NE, UE, WS, Q)›
‹⋀x. twl_exception_inv (M, N, U, D, add_mset (mset a) NE, UE, WS, Q) x ⟷
twl_exception_inv (M, N, U, D, NE, UE, WS, Q) x›
‹clauses_to_update_inv (M, N, U, D, add_mset (mset a) NE, UE, WS, Q) ⟷
clauses_to_update_inv (M, N, U, D, NE, UE, WS, Q)›
‹past_invs (M, N, U, D, add_mset (mset a) NE, UE, WS, Q) ⟷
past_invs (M, N, U, D, NE, UE, WS, Q)›
by (cases D; auto simp: twl_st_inv.simps twl_exception_inv.simps past_invs.simps; fail)+
have [simp]: ‹entailed_clss_inv (M, N, U, D, add_mset (mset a) NE, UE, WS, Q) ⟷
entailed_clss_inv (M, N, U, D, NE, UE, WS, Q)›
using ex count_decided_ge_get_level[of M] lev by (cases D) (auto simp: T)
show ?all_struct
using invs ex
unfolding twl_struct_invs_init_def T
unfolding fst_conv add_to_other_init.simps state⇩W_of_init.simps get_conflict.simps
by (clarsimp simp del: entailed_clss_inv.simps)
qed
lemma twl_struct_invs_init_set_conflict_init:
assumes
dist: ‹distinct C› and
lev: ‹count_decided (get_trail (fst T)) = 0› and
invs: ‹twl_struct_invs_init T› and
ex: ‹∀L ∈ set C. -L ∈ lits_of_l (get_trail_init T)› and
nempty: ‹C ≠ []›
shows
‹twl_struct_invs_init (set_conflict_init C T)›
(is ?all_struct)
proof -
obtain M N U D NE UE Q OC WS where
T: ‹T = ((M, N, U, D, NE, UE, WS, Q), OC)›
by (cases T) auto
have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + NE + OC, clauses U + UE, D)›
using invs unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset (mset C) (clauses N + NE + OC),
clauses U + UE, Some (mset C))›
using dist ex
unfolding T twl_struct_invs_init_def
by (auto 5 5 simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
true_annots_true_cls_def_iff_negation_in_model)
have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + NE + OC, clauses U + UE, D)›
using invs unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset (mset C) (clauses N + NE + OC),
clauses U + UE, Some (mset C))›
using lev
by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
clauses_def T count_decided_0_iff)
let ?T = ‹(M, N, U, Some (mset C), add_mset (mset C) NE, UE, {#}, {#})›
have [simp]: ‹confl_cands_enqueued ?T›
‹propa_cands_enqueued ?T›
‹twl_st_inv (M, N, U, D, NE, UE, WS, Q) ⟹ twl_st_inv ?T›
‹⋀x. twl_exception_inv (M, N, U, D, NE, UE, WS, Q) x ⟹ twl_exception_inv ?T x›
‹clauses_to_update_inv (M, N, U, D, NE, UE, WS, Q) ⟹ clauses_to_update_inv ?T›
‹past_invs (M, N, U, D, NE, UE, WS, Q) ⟹ past_invs ?T›
by (auto simp: twl_st_inv.simps twl_exception_inv.simps past_invs.simps; fail)+
have [simp]: ‹entailed_clss_inv (M, N, U, D, NE, UE, WS, Q) ⟹ entailed_clss_inv ?T›
using ex count_decided_ge_get_level[of M] lev nempty by (auto simp: T)
show ?all_struct
using invs ex
unfolding twl_struct_invs_init_def T
unfolding fst_conv add_to_other_init.simps state⇩W_of_init.simps get_conflict.simps
by (clarsimp simp del: entailed_clss_inv.simps)
qed
lemma twl_struct_invs_init_propagate_unit_init:
assumes
lev: ‹count_decided (get_trail_init T) = 0› and
invs: ‹twl_struct_invs_init T› and
undef: ‹undefined_lit (get_trail_init T) L› and
confl: ‹get_conflict_init T = None› and
MQ: ‹literals_to_update_init T = uminus `# lit_of `# mset (get_trail_init T)› and
WS: ‹clauses_to_update_init T = {#}›
shows
‹twl_struct_invs_init (propagate_unit_init L T)›
(is ?all_struct)
proof -
obtain M N U NE UE OC WS where
T: ‹T = ((M, N, U, None, NE, UE, WS, uminus `# lit_of `# mset M), OC)›
using confl MQ by (cases T) auto
let ?Q = ‹uminus `# lit_of `# mset M›
have [iff]: ‹- L ∈ lits_of_l M ⟷ False›
using undef by (auto simp: T Decided_Propagated_in_iff_in_lits_of_l)
have [simp]: ‹get_all_ann_decomposition M = [([], M)]›
by (rule no_decision_get_all_ann_decomposition) (use lev in ‹auto simp: T count_decided_0_iff›)
have H: ‹a @ Propagated L' mark' # b = Propagated L mark # M ⟷
(a = [] ∧ L = L' ∧ mark = mark' ∧ b = M) ∨
(a ≠ [] ∧ hd a = Propagated L mark ∧ tl a @ Propagated L' mark' # b = M)›
for a mark mark' L' b
using undef by (cases a) (auto simp: T atm_of_eq_atm_of)
have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + NE + OC, clauses U + UE, None)› and
excep: ‹twl_st_exception_inv (M, N, U, None, NE, UE, WS, ?Q)› and
st_inv: ‹twl_st_inv (M, N, U, None, NE, UE, WS, ?Q)›
using invs confl unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset {#L#} (clauses N + NE + OC),
clauses U + UE, None)› and
n_d: ‹no_dup M›
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
cdcl⇩W_restart_mset.reasons_in_clauses_def)
then have [simp]:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (Propagated L {#L#} # M,
add_mset {#L#} (clauses N + NE + OC), clauses U + UE, None)›
using undef by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def T H
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
consistent_interp_insert_iff)
have [iff]: ‹Propagated L {#L#} # M = M' @ Decided K # Ma ⟷ False› for M' K Ma
using lev by (cases M') (auto simp: count_decided_0_iff T)
have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + NE + OC, clauses U + UE, None)›
using invs confl unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.no_smaller_propa (Propagated L {#L#} # M, add_mset {#L#} (clauses N + NE + OC),
clauses U + UE, None)›
using lev
by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
clauses_def T count_decided_0_iff)
have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + NE + OC, clauses U + UE, None)›
using invs confl unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.no_smaller_propa (Propagated L {#L#} # M, add_mset {#L#} (clauses N + NE + OC),
clauses U + UE, None)›
using lev
by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
clauses_def T count_decided_0_iff)
let ?S = ‹(M, N, U, None, NE, UE, WS, ?Q)›
let ?T = ‹(Propagated L {#L#} # M, N, U, None, add_mset {#L#} NE, UE, WS, add_mset (-L) ?Q)›
have struct: ‹struct_wf_twl_cls C› if ‹C ∈# N + U› for C
using st_inv that by (simp add: twl_st_inv.simps)
have ‹entailed_clss_inv (fst T)›
using invs unfolding T twl_struct_invs_init_def fst_conv by fast
then have ent: ‹entailed_clss_inv (fst (propagate_unit_init L T))›
using lev by (auto simp: T get_level_cons_if)
show ‹twl_struct_invs_init (propagate_unit_init L T)›
apply (rule twl_struct_invs_init_init_state)
subgoal using lev by (auto simp: T)
subgoal using struct by (auto simp: T)
subgoal using MQ by (auto simp: T)
subgoal using WS by (auto simp: T)
subgoal by (simp add: T)
subgoal by (auto simp: T)
subgoal by (rule ent)
subgoal by (auto simp: T)
done
qed
named_theorems twl_st_l_init
lemma [twl_st_l_init]:
‹clauses_to_update_l_init (already_propagated_unit_init_l C S) = clauses_to_update_l_init S›
‹get_trail_l_init (already_propagated_unit_init_l C S) = get_trail_l_init S›
‹get_conflict_l_init (already_propagated_unit_init_l C S) = get_conflict_l_init S›
‹other_clauses_l_init (already_propagated_unit_init_l C S) = other_clauses_l_init S›
‹clauses_to_update_l_init (already_propagated_unit_init_l C S) = clauses_to_update_l_init S›
‹literals_to_update_l_init (already_propagated_unit_init_l C S) = literals_to_update_l_init S›
‹get_clauses_l_init (already_propagated_unit_init_l C S) = get_clauses_l_init S›
‹get_unit_clauses_l_init (already_propagated_unit_init_l C S) = add_mset C (get_unit_clauses_l_init S)›
‹get_learned_unit_clauses_l_init (already_propagated_unit_init_l C S) =
get_learned_unit_clauses_l_init S›
‹get_conflict_l_init (T, OC) = get_conflict_l T›
by (solves ‹cases S; cases T; auto simp: already_propagated_unit_init_l_def›)+
lemma [twl_st_l_init]:
‹(V, W) ∈ twl_st_l_init ⟹
count_decided (get_trail_init W) = count_decided (get_trail_l_init V)›
by (auto simp: twl_st_l_init_def)
lemma [twl_st_l_init]:
‹get_conflict_l (fst T) = get_conflict_l_init T›
‹literals_to_update_l (fst T) = literals_to_update_l_init T›
‹clauses_to_update_l (fst T) = clauses_to_update_l_init T›
by (cases T; auto; fail)+
lemma entailed_clss_inv_add_to_unit_init_clauses:
‹count_decided (get_trail_init T) = 0 ⟹ C ≠ [] ⟹ hd C ∈ lits_of_l (get_trail_init T) ⟹
entailed_clss_inv (fst T) ⟹ entailed_clss_inv (fst (add_to_unit_init_clauses (mset C) T))›
using count_decided_ge_get_level[of ‹get_trail_init T›]
by (cases T; cases C; auto simp: twl_st_inv.simps twl_exception_inv.simps)
lemma convert_lits_l_no_decision_iff: ‹(S, T) ∈ convert_lits_l M N ⟹
(∀s∈set T. ¬ is_decided s) ⟷
(∀s∈set S. ¬ is_decided s)›
unfolding convert_lits_l_def
by (induction rule: list_rel_induct)
(auto simp: dest!: p2relD)
lemma twl_st_l_init_no_decision_iff:
‹(S, T) ∈ twl_st_l_init ⟹
(∀s∈set (get_trail_init T). ¬ is_decided s) ⟷
(∀s∈set (get_trail_l_init S). ¬ is_decided s)›
by (subst convert_lits_l_no_decision_iff[of _ _ ‹get_clauses_l_init S›
‹get_unit_clauses_l_init S›])
(auto simp: twl_st_l_init_def)
lemma twl_st_l_init_defined_lit[twl_st_l_init]:
‹(S, T) ∈ twl_st_l_init ⟹
defined_lit (get_trail_init T) = defined_lit (get_trail_l_init S)›
by (auto simp: twl_st_l_init_def)
lemma [twl_st_l_init]:
‹(S, T) ∈ twl_st_l_init ⟹ get_learned_clauses_init T = {#} ⟷ learned_clss_l (get_clauses_l_init S) = {#}›
‹(S, T) ∈ twl_st_l_init ⟹ get_unit_learned_clauses_init T = {#} ⟷ get_learned_unit_clauses_l_init S = {#}
›
by (cases S; cases T; auto simp: twl_st_l_init_def; fail)+
lemma init_dt_pre_already_propagated_unit_init_l:
assumes
hd_C: ‹hd C ∈ lits_of_l (get_trail_l_init S)› and
pre: ‹init_dt_pre CS S› and
nempty: ‹C ≠ []› and
dist_C: ‹distinct C› and
lev: ‹count_decided (get_trail_l_init S) = 0›
shows
‹init_dt_pre CS (already_propagated_unit_init_l (mset C) S)› (is ?pre) and
‹init_dt_spec [C] S (already_propagated_unit_init_l (mset C) S)› (is ?spec)
proof -
obtain T where
SOC_T: ‹(S, T) ∈ twl_st_l_init› and
dist: ‹Ball (set CS) distinct› and
inv: ‹twl_struct_invs_init T› and
WS: ‹clauses_to_update_l_init S = {#}› and
dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
in_literals_to_update: ‹get_conflict_l_init S = None ⟶
literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
add_inv: ‹twl_list_invs (fst S)› and
stgy_inv: ‹twl_stgy_invs (fst T)› and
OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None›
using pre unfolding init_dt_pre_def
apply -
apply normalize_goal+
by presburger
obtain M N D NE UE Q U OC where
S: ‹S = ((M, N, U, D, NE, UE, Q), OC)›
by (cases S) auto
have [simp]: ‹twl_list_invs (fst (already_propagated_unit_init_l (mset C) S))›
using add_inv by (auto simp: already_propagated_unit_init_l_def S
twl_list_invs_def)
have [simp]: ‹(already_propagated_unit_init_l (mset C) S, add_to_unit_init_clauses (mset C) T)
∈ twl_st_l_init›
using SOC_T by (cases S)
(auto simp: twl_st_l_init_def already_propagated_unit_init_l_def
convert_lits_l_extend_mono)
have dec': ‹∀s∈set (get_trail_init T). ¬ is_decided s›
using SOC_T dec by (subst twl_st_l_init_no_decision_iff)
have [simp]: ‹twl_stgy_invs (fst (add_to_unit_init_clauses (mset C) T))›
using stgy_inv dec' unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def cdcl⇩W_restart_mset.no_smaller_confl_def
by (cases T)
(auto simp: cdcl⇩W_restart_mset_state clauses_def)
note clauses_to_update_inv.simps[simp del] valid_enqueued_alt_simps[simp del]
have [simp]: ‹twl_struct_invs_init (add_to_unit_init_clauses (mset C) T)›
apply (rule twl_struct_invs_init_add_to_unit_init_clauses)
using inv hd_C nempty dist_C lev SOC_T dec'
by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff intro: bexI[of _ ‹hd C›])
show ?pre
unfolding init_dt_pre_def
apply (rule exI[of _ ‹add_to_unit_init_clauses (mset C) T›])
using dist WS dec in_literals_to_update OC'_empty by (auto simp: twl_st_init twl_st_l_init)
show ?spec
unfolding init_dt_spec_def
apply (rule exI[of _ ‹add_to_unit_init_clauses (mset C) T›])
using dist WS dec in_literals_to_update OC'_empty nempty
by (auto simp: twl_st_init twl_st_l_init)
qed
lemma (in -) twl_stgy_invs_backtrack_lvl_0:
‹count_decided (get_trail T) = 0 ⟹ twl_stgy_invs T›
using count_decided_ge_get_level[of ‹get_trail T›]
by (cases T)
(auto simp: twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
cdcl⇩W_restart_mset.no_smaller_confl_def cdcl⇩W_restart_mset_state
cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def)
lemma [twl_st_l_init]:
‹clauses_to_update_l_init (propagate_unit_init_l L S) = clauses_to_update_l_init S›
‹get_trail_l_init (propagate_unit_init_l L S) = Propagated L 0 # get_trail_l_init S›
‹literals_to_update_l_init (propagate_unit_init_l L S) =
add_mset (-L) (literals_to_update_l_init S)›
‹get_conflict_l_init (propagate_unit_init_l L S) = get_conflict_l_init S›
‹clauses_to_update_l_init (propagate_unit_init_l L S) = clauses_to_update_l_init S›
‹other_clauses_l_init (propagate_unit_init_l L S) = other_clauses_l_init S›
‹get_clauses_l_init (propagate_unit_init_l L S) = get_clauses_l_init S›
‹get_learned_unit_clauses_l_init (propagate_unit_init_l L S) = get_learned_unit_clauses_l_init S›
‹get_unit_clauses_l_init (propagate_unit_init_l L S) = add_mset {#L#} (get_unit_clauses_l_init S)›
by (cases S; auto simp: propagate_unit_init_l_def; fail)+
lemma init_dt_pre_propagate_unit_init:
assumes
hd_C: ‹undefined_lit (get_trail_l_init S) L› and
pre: ‹init_dt_pre CS S› and
lev: ‹count_decided (get_trail_l_init S) = 0› and
confl: ‹get_conflict_l_init S = None›
shows
‹init_dt_pre CS (propagate_unit_init_l L S)› (is ?pre) and
‹init_dt_spec [[L]] S (propagate_unit_init_l L S)› (is ?spec)
proof -
obtain T where
SOC_T: ‹(S, T) ∈ twl_st_l_init› and
dist: ‹Ball (set CS) distinct› and
inv: ‹twl_struct_invs_init T› and
WS: ‹clauses_to_update_l_init S = {#}› and
dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
in_literals_to_update: ‹get_conflict_l_init S = None ⟶
literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
add_inv: ‹twl_list_invs (fst S)› and
stgy_inv: ‹twl_stgy_invs (fst T)› and
OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None›
using pre unfolding init_dt_pre_def
apply -
apply normalize_goal+
by presburger
obtain M N D NE UE Q U OC where
S: ‹S = ((M, N, U, D, NE, UE, Q), OC)›
by (cases S) auto
have [simp]: ‹(propagate_unit_init_l L S, propagate_unit_init L T)
∈ twl_st_l_init›
using SOC_T by (cases S) (auto simp: twl_st_l_init_def propagate_unit_init_l_def
convert_lit.simps convert_lits_l_extend_mono)
have dec': ‹∀s∈set (get_trail_init T). ¬ is_decided s›
using SOC_T dec by (subst twl_st_l_init_no_decision_iff)
have [simp]: ‹twl_stgy_invs (fst (propagate_unit_init L T))›
apply (rule twl_stgy_invs_backtrack_lvl_0)
using lev SOC_T
by (cases S) (auto simp: cdcl⇩W_restart_mset_state clauses_def twl_st_l_init_def)
note clauses_to_update_inv.simps[simp del] valid_enqueued_alt_simps[simp del]
have [simp]: ‹twl_struct_invs_init (propagate_unit_init L T)›
apply (rule twl_struct_invs_init_propagate_unit_init)
subgoal
using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff)
subgoal
using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff)
subgoal
using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff)
subgoal
using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff)
subgoal
using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff uminus_lit_of_image_mset)
subgoal
using inv hd_C lev SOC_T dec' confl in_literals_to_update WS
by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff uminus_lit_of_image_mset)
done
have [simp]: ‹twl_list_invs (fst (propagate_unit_init_l L S))›
using add_inv
by (auto simp: S twl_list_invs_def propagate_unit_init_l_def)
show ?pre
unfolding init_dt_pre_def
apply (rule exI[of _ ‹propagate_unit_init L T›])
using dist WS dec in_literals_to_update OC'_empty confl
by (auto simp: twl_st_init twl_st_l_init)
show ?spec
unfolding init_dt_spec_def
apply (rule exI[of _ ‹propagate_unit_init L T›])
using dist WS dec in_literals_to_update OC'_empty confl
by (auto simp: twl_st_init twl_st_l_init)
qed
lemma [twl_st_l_init]:
‹get_trail_l_init (set_conflict_init_l C S) = get_trail_l_init S›
‹literals_to_update_l_init (set_conflict_init_l C S) = {#}›
‹clauses_to_update_l_init (set_conflict_init_l C S) = {#}›
‹get_conflict_l_init (set_conflict_init_l C S) = Some (mset C)›
‹get_unit_clauses_l_init (set_conflict_init_l C S) = add_mset (mset C) (get_unit_clauses_l_init S)›
‹get_learned_unit_clauses_l_init (set_conflict_init_l C S) = get_learned_unit_clauses_l_init S›
‹get_clauses_l_init (set_conflict_init_l C S) = get_clauses_l_init S›
‹other_clauses_l_init (set_conflict_init_l C S) = other_clauses_l_init S›
by (cases S; auto simp: set_conflict_init_l_def; fail)+
lemma init_dt_pre_set_conflict_init_l:
assumes
[simp]: ‹get_conflict_l_init S = None› and
pre: ‹init_dt_pre (C # CS) S› and
false: ‹∀L ∈ set C. -L ∈ lits_of_l (get_trail_l_init S)› and
nempty: ‹C ≠ []›
shows
‹init_dt_pre CS (set_conflict_init_l C S)› (is ?pre) and
‹init_dt_spec [C] S (set_conflict_init_l C S)› (is ?spec)
proof -
obtain T where
SOC_T: ‹(S, T) ∈ twl_st_l_init› and
dist: ‹Ball (set CS) distinct› and
dist_C: ‹distinct C› and
inv: ‹twl_struct_invs_init T› and
WS: ‹clauses_to_update_l_init S = {#}› and
dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
in_literals_to_update: ‹get_conflict_l_init S = None ⟶
literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
add_inv: ‹twl_list_invs (fst S)› and
stgy_inv: ‹twl_stgy_invs (fst T)› and
OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None›
using pre unfolding init_dt_pre_def
apply -
apply normalize_goal+
by force
obtain M N D NE UE Q U OC where
S: ‹S = ((M, N, U, D, NE, UE, Q), OC)›
by (cases S) auto
have [simp]: ‹twl_list_invs (fst (set_conflict_init_l C S))›
using add_inv by (auto simp: set_conflict_init_l_def S
twl_list_invs_def)
have [simp]: ‹(set_conflict_init_l C S, set_conflict_init C T)
∈ twl_st_l_init›
using SOC_T by (cases S) (auto simp: twl_st_l_init_def set_conflict_init_l_def convert_lit.simps
convert_lits_l_extend_mono)
have dec': ‹count_decided (get_trail_init T) = 0›
apply (subst count_decided_0_iff)
apply (subst twl_st_l_init_no_decision_iff)
using SOC_T dec SOC_T by (auto simp: twl_st_l_init twl_st_init convert_lits_l_def)
have [simp]: ‹twl_stgy_invs (fst (set_conflict_init C T))›
using stgy_inv dec' nempty count_decided_ge_get_level[of ‹get_trail_init T›]
unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def cdcl⇩W_restart_mset.no_smaller_confl_def
by (cases T; cases C)
(auto 5 5 simp: cdcl⇩W_restart_mset_state clauses_def)
note clauses_to_update_inv.simps[simp del] valid_enqueued_alt_simps[simp del]
have [simp]: ‹twl_struct_invs_init (set_conflict_init C T)›
apply (rule twl_struct_invs_init_set_conflict_init)
subgoal
using inv nempty dist_C SOC_T dec false nempty
by (auto simp: twl_st_init count_decided_0_iff)
subgoal
using inv nempty dist_C SOC_T dec' false nempty
by (auto simp: twl_st_init count_decided_0_iff)
subgoal
using inv nempty dist_C SOC_T dec false nempty
by (auto simp: twl_st_init count_decided_0_iff)
subgoal
using inv nempty dist_C SOC_T dec false nempty
by (auto simp: twl_st_init count_decided_0_iff)
subgoal
using inv nempty dist_C SOC_T dec false nempty
by (auto simp: twl_st_init count_decided_0_iff)
done
show ?pre
unfolding init_dt_pre_def
apply (rule exI[of _ ‹set_conflict_init C T›])
using dist WS dec in_literals_to_update OC'_empty by (auto simp: twl_st_init twl_st_l_init)
show ?spec
unfolding init_dt_spec_def
apply (rule exI[of _ ‹set_conflict_init C T›])
using dist WS dec in_literals_to_update OC'_empty by (auto simp: twl_st_init twl_st_l_init)
qed
lemma [twl_st_init]:
‹get_trail_init (add_empty_conflict_init T) = get_trail_init T›
‹get_conflict_init (add_empty_conflict_init T) = Some {#}›
‹ clauses_to_update_init (add_empty_conflict_init T) = clauses_to_update_init T›
‹literals_to_update_init (add_empty_conflict_init T) = {#}›
by (cases T; auto simp:; fail)+
lemma [twl_st_l_init]:
‹get_trail_l_init (add_empty_conflict_init_l T) = get_trail_l_init T›
‹get_conflict_l_init (add_empty_conflict_init_l T) = Some {#}›
‹clauses_to_update_l_init (add_empty_conflict_init_l T) = clauses_to_update_l_init T›
‹literals_to_update_l_init (add_empty_conflict_init_l T) = {#}›
‹get_unit_clauses_l_init (add_empty_conflict_init_l T) = get_unit_clauses_l_init T›
‹get_learned_unit_clauses_l_init (add_empty_conflict_init_l T) = get_learned_unit_clauses_l_init T›
‹get_clauses_l_init (add_empty_conflict_init_l T) = get_clauses_l_init T›
‹other_clauses_l_init (add_empty_conflict_init_l T) = add_mset {#} (other_clauses_l_init T)›
by (cases T; auto simp: add_empty_conflict_init_l_def; fail)+
lemma twl_struct_invs_init_add_empty_conflict_init_l:
assumes
lev: ‹count_decided (get_trail (fst T)) = 0› and
invs: ‹twl_struct_invs_init T› and
WS: ‹clauses_to_update_init T = {#}›
shows ‹twl_struct_invs_init (add_empty_conflict_init T)›
(is ?all_struct)
proof -
obtain M N U D NE UE Q OC where
T: ‹T = ((M, N, U, D, NE, UE, {#}, Q), OC)›
using WS by (cases T) auto
have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, clauses N + NE + OC, clauses U + UE, D)›
using invs unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset {#} (clauses N + NE + OC),
clauses U + UE, Some {#})›
unfolding T twl_struct_invs_init_def
by (auto 5 5 simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
true_annots_true_cls_def_iff_negation_in_model)
have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + NE + OC, clauses U + UE, D)›
using invs unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset {#} (clauses N + NE + OC),
clauses U + UE, Some {#})›
using lev
by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
clauses_def T count_decided_0_iff)
let ?T = ‹(M, N, U, Some {#}, NE, UE, {#}, {#})›
have [simp]: ‹confl_cands_enqueued ?T›
‹propa_cands_enqueued ?T›
‹twl_st_inv (M, N, U, D, NE, UE, {#}, Q) ⟹ twl_st_inv ?T›
‹⋀x. twl_exception_inv (M, N, U, D, NE, UE, {#}, Q) x ⟹ twl_exception_inv ?T x›
‹clauses_to_update_inv (M, N, U, D, NE, UE, {#}, Q) ⟹ clauses_to_update_inv ?T›
‹past_invs (M, N, U, D, NE, UE, {#}, Q) ⟹ past_invs ?T›
by (auto simp: twl_st_inv.simps twl_exception_inv.simps past_invs.simps; fail)+
have [simp]: ‹entailed_clss_inv (M, N, U, D, NE, UE, {#}, Q) ⟹ entailed_clss_inv ?T›
using count_decided_ge_get_level[of M] lev by (auto simp: T)
show ?all_struct
using invs
unfolding twl_struct_invs_init_def T
unfolding fst_conv add_to_other_init.simps state⇩W_of_init.simps get_conflict.simps
by (clarsimp simp del: entailed_clss_inv.simps)
qed
lemma init_dt_pre_add_empty_conflict_init_l:
assumes
confl[simp]: ‹get_conflict_l_init S = None› and
pre: ‹init_dt_pre ([] # CS) S›
shows
‹init_dt_pre CS (add_empty_conflict_init_l S)› (is ?pre)
‹init_dt_spec [[]] S (add_empty_conflict_init_l S)› (is ?spec)
proof -
obtain T where
SOC_T: ‹(S, T) ∈ twl_st_l_init› and
dist: ‹Ball (set CS) distinct› and
inv: ‹twl_struct_invs_init T› and
WS: ‹clauses_to_update_l_init S = {#}› and
dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
in_literals_to_update: ‹get_conflict_l_init S = None ⟶
literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
add_inv: ‹twl_list_invs (fst S)› and
stgy_inv: ‹twl_stgy_invs (fst T)› and
OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None›
using pre unfolding init_dt_pre_def
apply -
apply normalize_goal+
by force
obtain M N D NE UE Q U OC where
S: ‹S = ((M, N, U, D, NE, UE, Q), OC)›
by (cases S) auto
have [simp]: ‹twl_list_invs (fst (add_empty_conflict_init_l S))›
using add_inv by (auto simp: add_empty_conflict_init_l_def S
twl_list_invs_def)
have [simp]: ‹(add_empty_conflict_init_l S, add_empty_conflict_init T)
∈ twl_st_l_init›
using SOC_T by (cases S) (auto simp: twl_st_l_init_def add_empty_conflict_init_l_def)
have dec': ‹count_decided (get_trail_init T) = 0›
apply (subst count_decided_0_iff)
apply (subst twl_st_l_init_no_decision_iff)
using SOC_T dec SOC_T by (auto simp: twl_st_l_init twl_st_init convert_lits_l_def)
have [simp]: ‹twl_stgy_invs (fst (add_empty_conflict_init T))›
using stgy_inv dec' count_decided_ge_get_level[of ‹get_trail_init T›]
unfolding twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def cdcl⇩W_restart_mset.no_smaller_confl_def
by (cases T)
(auto 5 5 simp: cdcl⇩W_restart_mset_state clauses_def)
note clauses_to_update_inv.simps[simp del] valid_enqueued_alt_simps[simp del]
have [simp]: ‹twl_struct_invs_init (add_empty_conflict_init T)›
apply (rule twl_struct_invs_init_add_empty_conflict_init_l)
using inv SOC_T dec' WS
by (auto simp: twl_st_init twl_st_l_init count_decided_0_iff )
show ?pre
unfolding init_dt_pre_def
apply (rule exI[of _ ‹add_empty_conflict_init T›])
using dist WS dec in_literals_to_update OC'_empty by (auto simp: twl_st_init twl_st_l_init)
show ?spec
unfolding init_dt_spec_def
apply (rule exI[of _ ‹add_empty_conflict_init T›])
using dist WS dec in_literals_to_update OC'_empty by (auto simp: twl_st_init twl_st_l_init)
qed
lemma [twl_st_l_init]:
‹get_trail (fst (add_to_clauses_init a T)) = get_trail_init T›
by (cases T; auto; fail)
lemma [twl_st_l_init]:
‹other_clauses_l_init (T, OC) = OC›
‹clauses_to_update_l_init (T, OC) = clauses_to_update_l T›
by (cases T; auto; fail)+
lemma twl_struct_invs_init_add_to_clauses_init:
assumes
lev: ‹count_decided (get_trail_init T) = 0› and
invs: ‹twl_struct_invs_init T› and
confl: ‹get_conflict_init T = None› and
MQ: ‹literals_to_update_init T = uminus `# lit_of `# mset (get_trail_init T)› and
WS: ‹clauses_to_update_init T = {#}› and
dist_C: ‹distinct C› and
le_2: ‹length C ≥ 2›
shows
‹twl_struct_invs_init (add_to_clauses_init C T)›
(is ?all_struct)
proof -
obtain M N U NE UE OC WS where
T: ‹T = ((M, N, U, None, NE, UE, WS, uminus `# lit_of `# mset M), OC)›
using confl MQ by (cases T) auto
let ?Q = ‹uminus `# lit_of `# mset M›
have [simp]: ‹get_all_ann_decomposition M = [([], M)]›
by (rule no_decision_get_all_ann_decomposition) (use lev in ‹auto simp: T count_decided_0_iff›)
have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, (clauses N + NE + OC), clauses U + UE, None)› and
excep: ‹twl_st_exception_inv (M, N, U, None, NE, UE, WS, ?Q)› and
st_inv: ‹twl_st_inv (M, N, U, None, NE, UE, WS, ?Q)›
using invs confl unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, add_mset (mset C) (clauses N + NE + OC),
clauses U + UE, None)› and
n_d: ‹no_dup M›
using dist_C
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def all_decomposition_implies_def
clauses_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def)
have ‹cdcl⇩W_restart_mset.no_smaller_propa (M, clauses N + NE + OC, clauses U + UE, None)›
using invs confl unfolding T twl_struct_invs_init_def by auto
then have [simp]:
‹cdcl⇩W_restart_mset.no_smaller_propa (M, add_mset (mset C) (clauses N + NE + OC),
clauses U + UE, None)›
using lev
by (auto simp: cdcl⇩W_restart_mset.no_smaller_propa_def cdcl⇩W_restart_mset_state
clauses_def T count_decided_0_iff)
let ?S = ‹(M, N, U, None, NE, UE, WS, ?Q)›
have struct: ‹struct_wf_twl_cls C› if ‹C ∈# N + U› for C
using st_inv that by (simp add: twl_st_inv.simps)
have ‹entailed_clss_inv (fst T)›
using invs unfolding T twl_struct_invs_init_def fst_conv by fast
then have ent: ‹entailed_clss_inv (fst (add_to_clauses_init C T))›
using lev by (auto simp: T get_level_cons_if)
show ‹twl_struct_invs_init (add_to_clauses_init C T)›
apply (rule twl_struct_invs_init_init_state)
subgoal using lev by (auto simp: T)
subgoal using struct dist_C le_2 by (auto simp: T mset_take_mset_drop_mset')
subgoal using MQ by (auto simp: T)
subgoal using WS by (auto simp: T)
subgoal by (simp add: T mset_take_mset_drop_mset')
subgoal by (auto simp: T mset_take_mset_drop_mset')
subgoal by (rule ent)
subgoal by (auto simp: T)
done
qed
lemma get_trail_init_add_to_clauses_init[simp]:
‹get_trail_init (add_to_clauses_init a T) = get_trail_init T›
by (cases T) auto
lemma init_dt_pre_add_to_clauses_init_l:
assumes
D: ‹get_conflict_l_init S = None› and
a: ‹length a ≠ Suc 0› ‹a ≠ []› and
pre: ‹init_dt_pre (a # CS) S› and
‹∀s∈set (get_trail_l_init S). ¬ is_decided s›
shows
‹add_to_clauses_init_l a S ≤ SPEC (init_dt_pre CS)› (is ?pre) and
‹add_to_clauses_init_l a S ≤ SPEC (init_dt_spec [a] S)› (is ?spec)
proof -
obtain T where
SOC_T: ‹(S, T) ∈ twl_st_l_init› and
dist: ‹Ball (set (a # CS)) distinct› and
inv: ‹twl_struct_invs_init T› and
WS: ‹clauses_to_update_l_init S = {#}› and
dec: ‹∀s∈set (get_trail_l_init S). ¬ is_decided s› and
in_literals_to_update: ‹get_conflict_l_init S = None ⟶
literals_to_update_l_init S = uminus `# lit_of `# mset (get_trail_l_init S)› and
add_inv: ‹twl_list_invs (fst S)› and
stgy_inv: ‹twl_stgy_invs (fst T)› and
OC'_empty: ‹other_clauses_l_init S ≠ {#} ⟶ get_conflict_l_init S ≠ None›
using pre unfolding init_dt_pre_def
apply -
apply normalize_goal+
by force
have dec': ‹∀L ∈ set (get_trail_init T). ¬is_decided L›
using SOC_T dec apply -
apply (rule twl_st_l_init_no_decision_iff[THEN iffD2])
using SOC_T dec SOC_T by (auto simp: twl_st_l_init twl_st_init convert_lits_l_def)
obtain M N NE UE Q OC where
S: ‹S = ((M, N, None, NE, UE, {#}, Q), OC)›
using D WS by (cases S) auto
have le_2: ‹length a ≥ 2›
using a by (cases a) auto
have
‹init_dt_pre CS ((M, fmupd i (a, True) N, None, NE, UE, {#}, Q), OC)› (is ?pre1) and
‹init_dt_spec [a] S
((M, fmupd i (a, True) N, None, NE, UE, {#}, Q), OC)› (is ?spec1)
if
i_0: ‹0 < i› and
i_dom: ‹i ∉# dom_m N›
for i :: ‹nat›
proof -
let ?S = ‹((M, fmupd i (a, True) N, None, NE, UE, {#}, Q), OC)›
have ‹Propagated L i ∉ set M› for L
using add_inv i_dom i_0 unfolding S
by (auto simp: twl_list_invs_def)
then have ‹(?S, add_to_clauses_init a T) ∈ twl_st_l_init›
using SOC_T i_dom
by (auto simp: S twl_st_l_init_def init_clss_l_mapsto_upd_notin
learned_clss_l_mapsto_upd_notin_irrelev convert_lit.simps
intro!: convert_lits_l_extend_mono[of _ _ N ‹NE+UE› ‹fmupd i (a, True) N›])
moreover have ‹twl_struct_invs_init (add_to_clauses_init a T)›
apply (rule twl_struct_invs_init_add_to_clauses_init)
subgoal
apply (subst count_decided_0_iff)
apply (subst twl_st_l_init_no_decision_iff)
using SOC_T dec SOC_T by (auto simp: twl_st_l_init twl_st_init convert_lits_l_def)
subgoal by (use dec SOC_T in_literals_to_update dist in
‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
subgoal by (use dec SOC_T in_literals_to_update dist in
‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
subgoal by (use dec SOC_T in_literals_to_update dist in
‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
subgoal by (use dec SOC_T in_literals_to_update dist in
‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
subgoal by (use dec SOC_T in_literals_to_update dist in
‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
subgoal by (use dec SOC_T in_literals_to_update dist in
‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init le_2 inv›)
done
moreover have ‹twl_list_invs (M, fmupd i (a, True) N, None, NE, UE, {#}, Q)›
using add_inv i_dom i_0 by (auto simp: S twl_list_invs_def)
moreover have ‹twl_stgy_invs (fst (add_to_clauses_init a T))›
by (rule twl_stgy_invs_backtrack_lvl_0)
(use dec' SOC_T in ‹auto simp: S count_decided_0_iff twl_st_l_init twl_st_init
twl_st_l_init_def›)
ultimately show ?pre1 ?spec1
unfolding init_dt_pre_def init_dt_spec_def apply -
subgoal
apply (rule exI[of _ ‹add_to_clauses_init a T›])
using dist dec OC'_empty in_literals_to_update by (auto simp: S)
subgoal
apply (rule exI[of _ ‹add_to_clauses_init a T›])
using dist dec OC'_empty in_literals_to_update i_dom i_0 a
by (auto simp: S learned_clss_l_mapsto_upd_notin_irrelev ran_m_mapsto_upd_notin)
done
qed
then show ?pre ?spec
by (auto simp: S add_to_clauses_init_l_def get_fresh_index_def RES_RETURN_RES)
qed
lemma init_dt_pre_init_dt_step:
assumes pre: ‹init_dt_pre (a # CS) SOC›
shows ‹init_dt_step a SOC ≤ SPEC (λSOC'. init_dt_pre CS SOC' ∧ init_dt_spec [a] SOC SOC')›
proof -
obtain S OC where SOC: ‹SOC = (S, OC)›
by (cases SOC) auto
obtain T where
SOC_T: ‹((S, OC), T) ∈ twl_st_l_init› and
dist: ‹Ball (set (a # CS)) distinct› and
inv: ‹twl_struct_invs_init T› and
WS: ‹clauses_to_update_l_init (S, OC) = {#}› and
dec: ‹∀s∈set (get_trail_l_init (S, OC)). ¬ is_decided s› and
in_literals_to_update: ‹get_conflict_l_init (S, OC) = None ⟶
literals_to_update_l_init (S, OC) = uminus `# lit_of `# mset (get_trail_l_init (S, OC))› and
add_inv: ‹twl_list_invs (fst (S, OC))› and
stgy_inv: ‹twl_stgy_invs (fst T)› and
OC'_empty: ‹other_clauses_l_init (S, OC) ≠ {#} ⟶ get_conflict_l_init (S, OC) ≠ None›
using pre unfolding SOC init_dt_pre_def
apply -
apply normalize_goal+
by presburger
have dec': ‹∀s∈set (get_trail_init T). ¬ is_decided s›
using SOC_T dec by (rule twl_st_l_init_no_decision_iff[THEN iffD2])
obtain M N D NE UE Q where
S: ‹SOC = ((M, N, D, NE, UE, {#}, Q), OC)›
using WS by (cases SOC) (auto simp: SOC)
then have S': ‹S = (M, N, D, NE, UE, {#}, Q)›
using S unfolding SOC by auto
show ?thesis
proof (cases ‹get_conflict_l (fst SOC)›)
case None
then show ?thesis
using pre dec by (auto simp add: Let_def count_decided_0_iff SOC twl_st_l_init twl_st_init
true_annot_iff_decided_or_true_lit length_list_Suc_0
init_dt_step_def get_fresh_index_def RES_RETURN_RES
intro!: init_dt_pre_already_propagated_unit_init_l init_dt_pre_set_conflict_init_l
init_dt_pre_propagate_unit_init init_dt_pre_add_empty_conflict_init_l
init_dt_pre_add_to_clauses_init_l SPEC_rule_conjI
dest: init_dt_pre_ConsD in_lits_of_l_defined_litD)
next
case (Some D')
then have [simp]: ‹D = Some D'›
by (auto simp: S)
have [simp]:
‹(((M, N, Some D', NE, UE, {#}, Q), add_mset (mset a) OC), add_to_other_init a T)
∈ twl_st_l_init›
using SOC_T by (cases T; auto simp: S S' twl_st_l_init_def; fail)+
have ‹init_dt_pre CS ((M, N, Some D', NE, UE, {#}, Q), add_mset (mset a) OC)›
unfolding init_dt_pre_def
apply (rule exI[of _ ‹add_to_other_init a T›])
using dist inv WS dec' dec in_literals_to_update add_inv stgy_inv SOC_T
by (auto simp: S' count_decided_0_iff twl_st_init
intro!: twl_struct_invs_init_add_to_other_init)
moreover have ‹init_dt_spec [a] ((M, N, Some D', NE, UE, {#}, Q), OC)
((M, N, Some D', NE, UE, {#}, Q), add_mset (mset a) OC)›
unfolding init_dt_spec_def
apply (rule exI[of _ ‹add_to_other_init a T›])
using dist inv WS dec dec' in_literals_to_update add_inv stgy_inv SOC_T
by (auto simp: S' count_decided_0_iff twl_st_init
intro!: twl_struct_invs_init_add_to_other_init)
ultimately show ?thesis
by (auto simp: S init_dt_step_def)
qed
qed
lemma [twl_st_l_init]:
‹get_trail_l_init (S, OC) = get_trail_l S›
‹literals_to_update_l_init (S, OC) = literals_to_update_l S›
by (cases S; auto; fail)+
lemma init_dt_spec_append:
assumes
spec1: ‹init_dt_spec CS S T› and
spec: ‹init_dt_spec CS' T U›
shows ‹init_dt_spec (CS @ CS') S U›
proof -
obtain T' where
TT': ‹(T, T') ∈ twl_st_l_init› and
‹twl_struct_invs_init T'› and
‹clauses_to_update_l_init T = {#}› and
‹∀s∈set (get_trail_l_init T). ¬ is_decided s› and
‹get_conflict_l_init T = None ⟶
literals_to_update_l_init T = uminus `# lit_of `# mset (get_trail_l_init T)› and
clss: ‹mset `# mset CS + mset `# ran_mf (get_clauses_l_init S) + other_clauses_l_init S +
get_unit_clauses_l_init S =
mset `# ran_mf (get_clauses_l_init T) + other_clauses_l_init T + get_unit_clauses_l_init T› and
learned: ‹learned_clss_lf (get_clauses_l_init S) = learned_clss_lf (get_clauses_l_init T)› and
unit_le: ‹get_learned_unit_clauses_l_init T = get_learned_unit_clauses_l_init S› and
‹twl_list_invs (fst T)› and
‹twl_stgy_invs (fst T')› and
‹other_clauses_l_init T ≠ {#} ⟶ get_conflict_l_init T ≠ None› and
empty: ‹{#} ∈# mset `# mset CS ⟶ get_conflict_l_init T ≠ None› and
confl_kept: ‹get_conflict_l_init S ≠ None ⟶ get_conflict_l_init S = get_conflict_l_init T›
using spec1
unfolding init_dt_spec_def apply -
apply normalize_goal+
by metis
obtain U' where
UU': ‹(U, U') ∈ twl_st_l_init› and
struct_invs: ‹twl_struct_invs_init U'› and
WS: ‹clauses_to_update_l_init U = {#}› and
dec: ‹∀s∈set (get_trail_l_init U). ¬ is_decided s› and
confl: ‹get_conflict_l_init U = None ⟶
literals_to_update_l_init U = uminus `# lit_of `# mset (get_trail_l_init U)› and
clss': ‹mset `# mset CS' + mset `# ran_mf (get_clauses_l_init T) + other_clauses_l_init T +
get_unit_clauses_l_init T =
mset `# ran_mf (get_clauses_l_init U) + other_clauses_l_init U + get_unit_clauses_l_init U› and
learned': ‹learned_clss_lf (get_clauses_l_init T) = learned_clss_lf (get_clauses_l_init U)› and
unit_le': ‹get_learned_unit_clauses_l_init U = get_learned_unit_clauses_l_init T› and
list_invs: ‹twl_list_invs (fst U)› and
stgy_invs: ‹twl_stgy_invs (fst U')› and
oth: ‹other_clauses_l_init U ≠ {#} ⟶ get_conflict_l_init U ≠ None› and
empty': ‹{#} ∈# mset `# mset CS' ⟶ get_conflict_l_init U ≠ None› and
confl_kept': ‹get_conflict_l_init T ≠ None ⟶ get_conflict_l_init T = get_conflict_l_init U›
using spec
unfolding init_dt_spec_def apply -
apply normalize_goal+
by metis
show ?thesis
unfolding init_dt_spec_def apply -
apply (rule exI[of _ U'])
apply (intro conjI)
subgoal using UU' .
subgoal using struct_invs .
subgoal using WS .
subgoal using dec .
subgoal using confl .
subgoal using clss clss'
by (smt ab_semigroup_add_class.add.commute ab_semigroup_add_class.add.left_commute
image_mset_union mset_append)
subgoal using learned' learned by simp
subgoal using unit_le unit_le' by simp
subgoal using list_invs .
subgoal using stgy_invs .
subgoal using oth .
subgoal using empty empty' oth confl_kept' by auto
subgoal using confl_kept confl_kept' by auto
done
qed
lemma init_dt_full:
fixes CS :: ‹'v literal list list› and SOC :: ‹'v twl_st_l_init› and S'
defines
‹S ≡ fst SOC› and
‹OC ≡ snd SOC›
assumes
‹init_dt_pre CS SOC›
shows
‹init_dt CS SOC ≤ SPEC (init_dt_spec CS SOC)›
using assms unfolding S_def OC_def
proof (induction CS arbitrary: SOC)
case Nil
then obtain S OC where SOC: ‹SOC = (S, OC)›
by (cases SOC) auto
from Nil
obtain T where
T: ‹(SOC, T) ∈ twl_st_l_init›
‹Ball (set []) distinct›
‹twl_struct_invs_init T›
‹clauses_to_update_l_init SOC = {#}›
‹∀s∈set (get_trail_l_init SOC). ¬ is_decided s›
‹get_conflict_l_init SOC = None ⟶
literals_to_update_l_init SOC =
uminus `# lit_of `# mset (get_trail_l_init SOC)›
‹twl_list_invs (fst SOC)›
‹twl_stgy_invs (fst T)›
‹other_clauses_l_init SOC ≠ {#} ⟶ get_conflict_l_init SOC ≠ None›
unfolding init_dt_pre_def apply -
apply normalize_goal+
by auto
then show ?case
unfolding init_dt_def SOC init_dt_spec_def nfoldli_simps
apply (intro RETURN_rule)
unfolding prod.simps
apply (rule exI[of _ T])
using T by (auto simp: SOC twl_st_init twl_st_l_init)
next
case (Cons a CS) note IH = this(1) and pre = this(2)
note init_dt_step_def[simp]
have 1: ‹init_dt_step a SOC ≤ SPEC (λSOC'. init_dt_pre CS SOC' ∧ init_dt_spec [a] SOC SOC')›
by (rule init_dt_pre_init_dt_step[OF pre])
have 2: ‹init_dt_spec (a # CS) SOC UOC›
if spec: ‹init_dt_spec CS T UOC› and
spec': ‹init_dt_spec [a] SOC T› for T UOC
using init_dt_spec_append[OF spec' spec] by simp
show ?case
unfolding init_dt_def nfoldli_simps if_True
apply (rule specify_left)
apply (rule 1)
apply (rule order.trans)
unfolding init_dt_def[symmetric]
apply (rule IH)
apply (solves ‹simp›)
apply (rule SPEC_rule)
by (rule 2) fast+
qed
lemma init_dt_pre_empty_state:
‹init_dt_pre [] (([], fmempty, None, {#}, {#}, {#}, {#}), {#})›
unfolding init_dt_pre_def
by (auto simp: twl_st_l_init_def twl_struct_invs_init_def twl_st_inv.simps
twl_struct_invs_def twl_st_inv.simps cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def cdcl⇩W_restart_mset.no_smaller_propa_def
past_invs.simps clauses_def
cdcl⇩W_restart_mset_state twl_list_invs_def
twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
cdcl⇩W_restart_mset.no_smaller_confl_def
cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def)
lemma twl_init_invs:
‹twl_struct_invs_init (([], {#}, {#}, None, {#}, {#}, {#}, {#}), {#})›
‹twl_list_invs ([], fmempty, None, {#}, {#}, {#}, {#})›
‹twl_stgy_invs ([], {#}, {#}, None, {#}, {#}, {#}, {#})›
by (auto simp: twl_struct_invs_init_def twl_st_inv.simps twl_list_invs_def twl_stgy_invs_def
past_invs.simps
twl_struct_invs_def twl_st_inv.simps cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def cdcl⇩W_restart_mset.no_smaller_propa_def
past_invs.simps clauses_def
cdcl⇩W_restart_mset_state twl_list_invs_def
twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
cdcl⇩W_restart_mset.no_smaller_confl_def
cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def)
end