theory IsaSAT_Initialisation
imports Watched_Literals.Watched_Literals_Watch_List_Initialisation IsaSAT_Setup IsaSAT_VMTF
Automatic_Refinement.Relators
begin
chapter ‹Initialisation›
lemma bitXOR_1_if_mod_2_int: ‹bitOR L 1 = (if L mod 2 = 0 then L + 1 else L)› for L :: int
apply (rule bin_rl_eqI)
unfolding bin_rest_OR bin_last_OR
apply (auto simp: bin_rest_def bin_last_def)
done
lemma bitOR_1_if_mod_2_nat:
‹bitOR L 1 = (if L mod 2 = 0 then L + 1 else L)›
‹bitOR L (Suc 0) = (if L mod 2 = 0 then L + 1 else L)› for L :: nat
proof -
have H: ‹bitOR L 1 = L + (if bin_last (int L) then 0 else 1)›
unfolding bitOR_nat_def
apply (auto simp: bitOR_nat_def bin_last_def
bitXOR_1_if_mod_2_int)
done
show ‹bitOR L 1 = (if L mod 2 = 0 then L + 1 else L)›
unfolding H
apply (auto simp: bitOR_nat_def bin_last_def)
apply presburger+
done
then show ‹bitOR L (Suc 0) = (if L mod 2 = 0 then L + 1 else L)›
by simp
qed
section ‹Code for the initialisation of the Data Structure›
text ‹The initialisation is done in three different steps:
▸ First, we extract all the atoms that appear in the problem and initialise the state with empty values.
This part is called ∗‹initialisation› below.
▸ Then, we go over all clauses and insert them in our memory module. We call this phase ∗‹parsing›.
▸ Finally, we calculate the watch list.
Splitting the second from the third step makes it easier to add preprocessing and more important
to add a bounded mode.
›
subsection ‹Initialisation of the state›
definition (in -) atoms_hash_empty where
[simp]: ‹atoms_hash_empty _ = {}›
definition (in -) atoms_hash_int_empty where
‹atoms_hash_int_empty n = RETURN (replicate n False)›
lemma atoms_hash_int_empty_atoms_hash_empty:
‹(atoms_hash_int_empty, RETURN o atoms_hash_empty) ∈
[λn. (∀L∈#ℒ⇩a⇩l⇩l 𝒜. atm_of L < n)]⇩f nat_rel → ⟨atoms_hash_rel 𝒜⟩nres_rel›
by (intro frefI nres_relI)
(use Max_less_iff in ‹auto simp: atoms_hash_rel_def atoms_hash_int_empty_def atoms_hash_empty_def
in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff Ball_def
dest: spec[of _ "Pos _"]›)
definition (in -) distinct_atms_empty where
‹distinct_atms_empty _ = {}›
definition (in -) distinct_atms_int_empty where
‹distinct_atms_int_empty n = RETURN ([], replicate n False)›
lemma distinct_atms_int_empty_distinct_atms_empty:
‹(distinct_atms_int_empty, RETURN o distinct_atms_empty) ∈
[λn. (∀L∈#ℒ⇩a⇩l⇩l 𝒜. atm_of L < n)]⇩f nat_rel → ⟨distinct_atoms_rel 𝒜⟩nres_rel›
apply (intro frefI nres_relI)
apply (auto simp: distinct_atoms_rel_alt_def distinct_atms_empty_def distinct_atms_int_empty_def)
by (metis atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n atms_of_def imageE)
type_synonym vmtf_remove_int_option_fst_As = ‹vmtf_option_fst_As × nat set›
type_synonym isa_vmtf_remove_int_option_fst_As = ‹vmtf_option_fst_As × nat list × bool list›
definition vmtf_init
:: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ vmtf_remove_int_option_fst_As set›
where
‹vmtf_init 𝒜⇩i⇩n M = {((ns, m, fst_As, lst_As, next_search), to_remove).
𝒜⇩i⇩n ≠ {#} ⟶ (fst_As ≠ None ∧ lst_As ≠ None ∧ ((ns, m, the fst_As, the lst_As, next_search),
to_remove) ∈ vmtf 𝒜⇩i⇩n M)}›
definition isa_vmtf_init where
‹isa_vmtf_init 𝒜 M =
((Id ×⇩r nat_rel ×⇩r ⟨nat_rel⟩option_rel ×⇩r ⟨nat_rel⟩option_rel ×⇩r ⟨nat_rel⟩option_rel) ×⇩f
distinct_atoms_rel 𝒜)¯
`` vmtf_init 𝒜 M›
lemma isa_vmtf_initI:
‹(vm, to_remove') ∈ vmtf_init 𝒜 M ⟹ (to_remove, to_remove') ∈ distinct_atoms_rel 𝒜 ⟹
(vm, to_remove) ∈ isa_vmtf_init 𝒜 M›
by (auto simp: isa_vmtf_init_def Image_iff intro!: bexI[of _ ‹(vm, to_remove')›])
lemma isa_vmtf_init_consD:
‹((ns, m, fst_As, lst_As, next_search), remove) ∈ isa_vmtf_init 𝒜 M ⟹
((ns, m, fst_As, lst_As, next_search), remove) ∈ isa_vmtf_init 𝒜 (L # M)›
by (auto simp: isa_vmtf_init_def vmtf_init_def dest: vmtf_consD)
lemma vmtf_init_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ vmtf_init 𝒜 M ⟹ L ∈ vmtf_init ℬ M›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] vmtf_cong[of 𝒜 ℬ]
unfolding vmtf_init_def vmtf_ℒ⇩a⇩l⇩l_def
by auto
lemma isa_vmtf_init_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ isa_vmtf_init 𝒜 M ⟹ L ∈ isa_vmtf_init ℬ M›
using vmtf_init_cong[of 𝒜 ℬ] distinct_atoms_rel_cong[of 𝒜 ℬ]
apply (subst (asm) isa_vmtf_init_def)
by (cases L) (auto intro!: isa_vmtf_initI)
type_synonym (in -) twl_st_wl_heur_init =
‹trail_pol × arena × conflict_option_rel × nat ×
(nat × nat literal × bool) list list × isa_vmtf_remove_int_option_fst_As × bool list ×
nat × conflict_min_cach_l × lbd × vdom × bool›
type_synonym (in -) twl_st_wl_heur_init_full =
‹trail_pol × arena × conflict_option_rel × nat ×
(nat × nat literal × bool) list list × isa_vmtf_remove_int_option_fst_As × bool list ×
nat × conflict_min_cach_l × lbd × vdom × bool›
text ‹The initialisation relation is stricter in the sense that it already includes the relation
of atom inclusion.
Remark that we replace \<^term>‹(D = None ⟶ j ≤ length M)› by \<^term>‹j ≤ length M›: this simplifies the
proofs and does not make a difference in the generated code, since there are no conflict analysis
at that level anyway.
›
text ‹KILL duplicates below, but difference:
vmtf vs vmtf\_init
watch list vs no WL
OC vs non-OC
›
definition twl_st_heur_parsing_no_WL
:: ‹nat multiset ⇒ bool ⇒ (twl_st_wl_heur_init × nat twl_st_wl_init) set›
where
‹twl_st_heur_parsing_no_WL 𝒜 unbdd =
{((M', N', D', j, W', vm, φ, clvls, cach, lbd, vdom, failed), ((M, N, D, NE, UE, NS, US, Q), OC)).
(unbdd ⟶ ¬failed) ∧
((unbdd ∨ ¬failed) ⟶
(valid_arena N' N (set vdom) ∧
set_mset
(all_lits_of_mm
({#mset (fst x). x ∈# ran_m N#} + NE + UE + NS + US)) ⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜) ∧
mset vdom = dom_m N)) ∧
(M', M) ∈ trail_pol 𝒜 ∧
(D', D) ∈ option_lookup_clause_rel 𝒜 ∧
j ≤ length M ∧
Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
vm ∈ isa_vmtf_init 𝒜 M ∧
phase_saving 𝒜 φ ∧
no_dup M ∧
cach_refinement_empty 𝒜 cach ∧
(W', empty_watched 𝒜) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜) ∧
isasat_input_bounded 𝒜 ∧
distinct vdom
}›
definition twl_st_heur_parsing
:: ‹nat multiset ⇒ bool ⇒ (twl_st_wl_heur_init × (nat twl_st_wl × nat clauses)) set›
where
‹twl_st_heur_parsing 𝒜 unbdd =
{((M', N', D', j, W', vm, φ, clvls, cach, lbd, vdom, failed), ((M, N, D, NE, UE, NS, US, Q, W), OC)).
(unbdd ⟶ ¬failed) ∧
((unbdd ∨ ¬failed) ⟶
((M', M) ∈ trail_pol 𝒜 ∧
valid_arena N' N (set vdom) ∧
(D', D) ∈ option_lookup_clause_rel 𝒜 ∧
j ≤ length M ∧
Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
vm ∈ isa_vmtf_init 𝒜 M ∧
phase_saving 𝒜 φ ∧
no_dup M ∧
cach_refinement_empty 𝒜 cach ∧
mset vdom = dom_m N ∧
vdom_m 𝒜 W N = set_mset (dom_m N) ∧
set_mset
(all_lits_of_mm
({#mset (fst x). x ∈# ran_m N#} + NE + UE + NS + US)) ⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜) ∧
(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜) ∧
isasat_input_bounded 𝒜 ∧
distinct vdom))
}›
definition twl_st_heur_parsing_no_WL_wl :: ‹nat multiset ⇒ bool ⇒ (_ × nat twl_st_wl_init') set› where
‹twl_st_heur_parsing_no_WL_wl 𝒜 unbdd =
{((M', N', D', j, W', vm, φ, clvls, cach, lbd, vdom, failed), (M, N, D, NE, UE, NS, US, Q)).
(unbdd ⟶ ¬failed) ∧
((unbdd ∨ ¬failed) ⟶
(valid_arena N' N (set vdom) ∧ set_mset (dom_m N) ⊆ set vdom)) ∧
(M', M) ∈ trail_pol 𝒜 ∧
(D', D) ∈ option_lookup_clause_rel 𝒜 ∧
j ≤ length M ∧
Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
vm ∈ isa_vmtf_init 𝒜 M ∧
phase_saving 𝒜 φ ∧
no_dup M ∧
cach_refinement_empty 𝒜 cach ∧
set_mset (all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + NE + UE + NS + US))
⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜) ∧
(W', empty_watched 𝒜) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜) ∧
isasat_input_bounded 𝒜 ∧
distinct vdom
}›
definition twl_st_heur_parsing_no_WL_wl_no_watched :: ‹nat multiset ⇒ bool ⇒ (twl_st_wl_heur_init_full × nat twl_st_wl_init) set› where
‹twl_st_heur_parsing_no_WL_wl_no_watched 𝒜 unbdd =
{((M', N', D', j, W', vm, φ, clvls, cach, lbd, vdom, failed), ((M, N, D, NE, UE, NS, US, Q), OC)).
(unbdd ⟶ ¬failed) ∧
((unbdd ∨ ¬failed) ⟶
(valid_arena N' N (set vdom) ∧ set_mset (dom_m N) ⊆ set vdom)) ∧ (M', M) ∈ trail_pol 𝒜 ∧
(D', D) ∈ option_lookup_clause_rel 𝒜 ∧
j ≤ length M ∧
Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
vm ∈ isa_vmtf_init 𝒜 M ∧
phase_saving 𝒜 φ ∧
no_dup M ∧
cach_refinement_empty 𝒜 cach ∧
set_mset (all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + NE + UE + NS + US))
⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜) ∧
(W', empty_watched 𝒜) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜) ∧
isasat_input_bounded 𝒜 ∧
distinct vdom
}›
definition twl_st_heur_post_parsing_wl :: ‹bool ⇒ (twl_st_wl_heur_init_full × nat twl_st_wl) set› where
‹twl_st_heur_post_parsing_wl unbdd =
{((M', N', D', j, W', vm, φ, clvls, cach, lbd, vdom, failed), (M, N, D, NE, UE, NS, US, Q, W)).
(unbdd ⟶ ¬failed) ∧
((unbdd ∨ ¬failed) ⟶
((M', M) ∈ trail_pol (all_atms N (NE + UE + NS + US)) ∧
set_mset (dom_m N) ⊆ set vdom ∧
valid_arena N' N (set vdom))) ∧
(D', D) ∈ option_lookup_clause_rel (all_atms N (NE + UE + NS + US)) ∧
j ≤ length M ∧
Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
vm ∈ isa_vmtf_init (all_atms N (NE + UE + NS + US)) M ∧
phase_saving (all_atms N (NE + UE + NS + US)) φ ∧
no_dup M ∧
cach_refinement_empty (all_atms N (NE + UE + NS + US)) cach ∧
vdom_m (all_atms N (NE + UE + NS + US)) W N ⊆ set vdom ∧
set_mset (all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + NE + UE + NS + US))
⊆ set_mset (ℒ⇩a⇩l⇩l (all_atms N (NE + UE + NS + US))) ∧
(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms N (NE + UE + NS + US))) ∧
isasat_input_bounded (all_atms N (NE + UE + NS + US)) ∧
distinct vdom
}›
subsubsection ‹VMTF›
definition initialise_VMTF :: ‹nat list ⇒ nat ⇒ isa_vmtf_remove_int_option_fst_As nres› where
‹initialise_VMTF N n = do {
let A = replicate n (VMTF_Node 0 None None);
to_remove ← distinct_atms_int_empty n;
ASSERT(length N ≤ uint32_max);
(n, A, cnext) ← WHILE⇩T
(λ(i, A, cnext). i < length_uint32_nat N)
(λ(i, A, cnext). do {
ASSERT(i < length_uint32_nat N);
let L = (N ! i);
ASSERT(L < length A);
ASSERT(cnext ≠ None ⟶ the cnext < length A);
ASSERT(i + 1 ≤ uint32_max);
RETURN (i + 1, vmtf_cons A L cnext (i), Some L)
})
(0, A, None);
RETURN ((A, n, cnext, (if N = [] then None else Some ((N!0))), cnext), to_remove)
}›
lemma initialise_VMTF:
shows ‹(uncurry initialise_VMTF, uncurry (λN n. RES (vmtf_init N []))) ∈
[λ(N,n). (∀L∈# N. L < n) ∧ (distinct_mset N) ∧ size N < uint32_max ∧ set_mset N = set_mset 𝒜]⇩f
(⟨nat_rel⟩list_rel_mset_rel) ×⇩f nat_rel →
⟨(⟨Id⟩list_rel ×⇩r nat_rel ×⇩r ⟨nat_rel⟩ option_rel ×⇩r ⟨nat_rel⟩ option_rel ×⇩r ⟨nat_rel⟩ option_rel)
×⇩r distinct_atoms_rel 𝒜⟩nres_rel›
(is ‹(?init, ?R) ∈ _›)
proof -
have vmtf_ns_notin_empty: ‹vmtf_ns_notin [] 0 (replicate n (VMTF_Node 0 None None))› for n
unfolding vmtf_ns_notin_def
by auto
have K2: ‹distinct N ⟹ fst_As < length N ⟹ N!fst_As ∈ set (take fst_As N) ⟹ False›
for fst_As x N
by (metis (no_types, lifting) in_set_conv_nth length_take less_not_refl min_less_iff_conj
nth_eq_iff_index_eq nth_take)
have W_ref: ‹WHILE⇩T (λ(i, A, cnext). i < length_uint32_nat N')
(λ(i, A, cnext). do {
_ ← ASSERT (i < length_uint32_nat N');
let L = (N' ! i);
_ ← ASSERT (L < length A);
_ ← ASSERT (cnext ≠ None ⟶ the cnext < length A);
_ ← ASSERT (i + 1 ≤ uint32_max);
RETURN
(i + 1,
vmtf_cons A L cnext (i), Some L)
})
(0, replicate n' (VMTF_Node 0 None None),
None)
≤ SPEC(λ(i, A', cnext).
vmtf_ns (rev ((take i N'))) i A'
∧ cnext = (option_last (take i N')) ∧ i = length N' ∧
length A' = n ∧ vmtf_ns_notin (rev ((take i N'))) i A'
)›
(is ‹_ ≤ SPEC ?P›)
if H: ‹case y of (N, n) ⇒(∀L∈# N. L < n) ∧ distinct_mset N ∧ size N < uint32_max ∧
set_mset N = set_mset 𝒜› and
ref: ‹(x, y) ∈ ⟨Id⟩list_rel_mset_rel ×⇩f nat_rel› and
st[simp]: ‹x = (N', n')› ‹y = (N, n)›
for N N' n n' A x y
proof -
have [simp]: ‹n = n'› and NN': ‹(N', N) ∈ ⟨Id⟩list_rel_mset_rel›
using ref unfolding st by auto
then have dist: ‹distinct N'›
using NN' H by (auto simp: list_rel_def br_def list_mset_rel_def list.rel_eq
list_all2_op_eq_map_right_iff' distinct_image_mset_inj list_rel_mset_rel_def)
have L_N: ‹∀L∈set N'. L < n›
using H ref by (auto simp: list_rel_def br_def list_mset_rel_def
list_all2_op_eq_map_right_iff' list_rel_mset_rel_def list.rel_eq)
let ?Q = ‹λ(i, A', cnext).
vmtf_ns (rev ((take i N'))) i A' ∧ i ≤ length N' ∧
cnext = (option_last (take i N')) ∧
length A' = n ∧ vmtf_ns_notin (rev ((take i N'))) i A'›
show ?thesis
apply (refine_vcg WHILET_rule[where R = ‹measure (λ(i, _). length N' + 1 - i)› and I = ‹?Q›])
subgoal by auto
subgoal by (auto intro: vmtf_ns.intros)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for S N' x2 A'
unfolding assert_bind_spec_conv vmtf_ns_notin_def
using L_N dist
by (auto 5 5 simp: take_Suc_conv_app_nth hd_drop_conv_nth nat_shiftr_div2
option_last_def hd_rev last_map intro!: vmtf_cons dest: K2)
subgoal by auto
subgoal
using L_N dist
by (auto simp: take_Suc_conv_app_nth hd_drop_conv_nth nat_shiftr_div2
option_last_def hd_rev last_map)
subgoal
using L_N dist
by (auto simp: last_take_nth_conv option_last_def)
subgoal
using H dist ref
by (auto simp: last_take_nth_conv option_last_def list_rel_mset_rel_imp_same_length)
subgoal
using L_N dist
by (auto 5 5 simp: take_Suc_conv_app_nth option_last_def hd_rev last_map intro!: vmtf_cons
dest: K2)
subgoal by (auto simp: take_Suc_conv_app_nth)
subgoal by (auto simp: take_Suc_conv_app_nth)
subgoal by auto
subgoal
using L_N dist
by (auto 5 5 simp: take_Suc_conv_app_nth hd_rev last_map option_last_def
intro!: vmtf_notin_vmtf_cons dest: K2 split: if_splits)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
have [simp]: ‹vmtf_ℒ⇩a⇩l⇩l n' [] ((set N, {}), {})›
if ‹(N, n') ∈ ⟨Id⟩list_rel_mset_rel› for N N' n'
using that unfolding vmtf_ℒ⇩a⇩l⇩l_def
by (auto simp: ℒ⇩a⇩l⇩l_def atms_of_def image_image image_Un list_rel_def
br_def list_mset_rel_def list_all2_op_eq_map_right_iff'
list_rel_mset_rel_def list.rel_eq)
have in_N_in_N1: ‹L ∈ set N' ⟹ L ∈ atms_of (ℒ⇩a⇩l⇩l N)›
if ‹(N', N) ∈ list_mset_rel› for L N N' y
using that by (auto simp: ℒ⇩a⇩l⇩l_def atms_of_def image_image image_Un list_rel_def
list.rel_eq br_def list_mset_rel_def list_all2_op_eq_map_right_iff')
have length_ba: ‹∀L∈# N. L < length ba ⟹ L ∈ atms_of (ℒ⇩a⇩l⇩l N) ⟹
L < length ba›
if ‹(N', y) ∈ ⟨Id⟩list_rel_mset_rel›
for L ba N N' y
using that
by (auto simp: ℒ⇩a⇩l⇩l_def nat_shiftr_div2 list.rel_eq
atms_of_def image_image image_Un split: if_splits)
show ?thesis
supply list.rel_eq[simp]
apply (intro frefI nres_relI)
unfolding initialise_VMTF_def uncurry_def conc_Id id_def vmtf_init_def
distinct_atms_int_empty_def nres_monad1
apply (refine_rcg)
subgoal by (auto dest: list_rel_mset_rel_imp_same_length)
apply (rule specify_left)
apply (rule W_ref; assumption?)
subgoal for N' N'n' n' Nn N n st
apply (case_tac st)
apply clarify
apply (subst RETURN_RES_refine_iff)
apply (auto dest: list_rel_mset_rel_imp_same_length)
apply (rule exI[of _ ‹{}›])
apply (auto simp: distinct_atoms_rel_alt_def list_rel_mset_rel_def list_mset_rel_def
br_def; fail)
apply (rule exI[of _ ‹{}›])
unfolding vmtf_def in_pair_collect_simp prod.case
apply (intro conjI impI)
apply (rule exI[of _ ‹(rev (fst N'))›])
apply (rule_tac exI[of _ ‹[]›])
apply (intro conjI impI)
subgoal
by (auto simp: rev_map[symmetric] vmtf_def option_last_def last_map
hd_rev list_rel_mset_rel_def br_def list_mset_rel_def)
subgoal by (auto simp: rev_map[symmetric] vmtf_def option_hd_rev
map_option_option_last hd_map hd_conv_nth rev_nth last_conv_nth
list_rel_mset_rel_def br_def list_mset_rel_def)
subgoal by (auto simp: rev_map[symmetric] vmtf_def option_hd_rev
map_option_option_last hd_map last_map hd_conv_nth rev_nth last_conv_nth
list_rel_mset_rel_def br_def list_mset_rel_def)
subgoal by (auto simp: rev_map[symmetric] vmtf_def option_hd_rev
map_option_option_last hd_rev last_map distinct_atms_empty_def)
subgoal by (auto simp: rev_map[symmetric] vmtf_def option_hd_rev
map_option_option_last list_rel_mset_rel_def)
subgoal by (auto simp: rev_map[symmetric] vmtf_def option_hd_rev
map_option_option_last dest: length_ba)
subgoal by (auto simp: rev_map[symmetric] vmtf_def option_hd_rev
map_option_option_last hd_map hd_conv_nth rev_nth last_conv_nth
list_rel_mset_rel_def br_def list_mset_rel_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
subgoal by (auto simp: rev_map[symmetric] vmtf_def option_hd_rev
map_option_option_last list_rel_mset_rel_def dest: in_N_in_N1)
subgoal by (auto simp: distinct_atoms_rel_alt_def list_rel_mset_rel_def list_mset_rel_def
br_def)
done
done
qed
subsection ‹Parsing›
fun (in -)get_conflict_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ conflict_option_rel› where
‹get_conflict_wl_heur_init (_, _, D, _) = D›
fun (in -)get_clauses_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ arena› where
‹get_clauses_wl_heur_init (_, N, _) = N›
fun (in -) get_trail_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ trail_pol› where
‹get_trail_wl_heur_init (M, _, _, _, _, _, _) = M›
fun (in -) get_vdom_heur_init :: ‹twl_st_wl_heur_init ⇒ nat list› where
‹get_vdom_heur_init (_, _, _, _, _, _, _, _, _, _, vdom, _) = vdom›
fun (in -) is_failed_heur_init :: ‹twl_st_wl_heur_init ⇒ bool› where
‹is_failed_heur_init (_, _, _, _, _, _, _, _, _, _, _, failed) = failed›
definition propagate_unit_cls
:: ‹nat literal ⇒ nat twl_st_wl_init ⇒ nat twl_st_wl_init›
where
‹propagate_unit_cls = (λL ((M, N, D, NE, UE, Q), OC).
((Propagated L 0 # M, N, D, add_mset {#L#} NE, UE, Q), OC))›
definition propagate_unit_cls_heur
:: ‹nat literal ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹propagate_unit_cls_heur = (λL (M, N, D, Q). do {
M ← cons_trail_Propagated_tr L 0 M;
RETURN (M, N, D, Q)})›
fun get_unit_clauses_init_wl :: ‹'v twl_st_wl_init ⇒ 'v clauses› where
‹get_unit_clauses_init_wl ((M, N, D, NE, UE, Q), OC) = NE + UE›
fun get_subsumed_clauses_init_wl :: ‹'v twl_st_wl_init ⇒ 'v clauses› where
‹get_subsumed_clauses_init_wl ((M, N, D, NE, UE, NS, US, Q), OC) = NS + US›
fun get_subsumed_init_clauses_init_wl :: ‹'v twl_st_wl_init ⇒ 'v clauses› where
‹get_subsumed_init_clauses_init_wl ((M, N, D, NE, UE, NS, US, Q), OC) = NS›
abbreviation all_lits_st_init :: ‹'v twl_st_wl_init ⇒ 'v literal multiset› where
‹all_lits_st_init S ≡ all_lits (get_clauses_init_wl S)
(get_unit_clauses_init_wl S + get_subsumed_init_clauses_init_wl S)›
definition all_atms_init :: ‹_ ⇒ _ ⇒ 'v multiset› where
‹all_atms_init N NUE = atm_of `# all_lits N NUE›
abbreviation all_atms_st_init :: ‹'v twl_st_wl_init ⇒ 'v multiset› where
‹all_atms_st_init S ≡ atm_of `# all_lits_st_init S›
lemma DECISION_REASON0[simp]: ‹DECISION_REASON ≠ 0›
by (auto simp: DECISION_REASON_def)
lemma propagate_unit_cls_heur_propagate_unit_cls:
‹(uncurry propagate_unit_cls_heur, uncurry (propagate_unit_init_wl)) ∈
[λ(L, S). undefined_lit (get_trail_init_wl S) L ∧ L ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f
Id ×⇩r twl_st_heur_parsing_no_WL 𝒜 unbdd → ⟨twl_st_heur_parsing_no_WL 𝒜 unbdd⟩ nres_rel›
unfolding twl_st_heur_parsing_no_WL_def propagate_unit_cls_heur_def propagate_unit_init_wl_def
nres_monad3
apply (intro frefI nres_relI)
apply (clarsimp simp add: propagate_unit_init_wl.simps cons_trail_Propagated_tr_def[symmetric] comp_def
curry_def all_atms_def[symmetric] intro!: ASSERT_leI)
apply (refine_rcg cons_trail_Propagated_tr2[where 𝒜 = 𝒜])
subgoal by auto
subgoal by auto
subgoal by (auto intro!: isa_vmtf_init_consD
simp: all_lits_of_mm_add_mset all_lits_of_m_add_mset uminus_𝒜⇩i⇩n_iff)
done
definition already_propagated_unit_cls
:: ‹nat literal ⇒ nat twl_st_wl_init ⇒ nat twl_st_wl_init›
where
‹already_propagated_unit_cls = (λL ((M, N, D, NE, UE, Q), OC).
((M, N, D, add_mset {#L#} NE, UE, Q), OC))›
definition already_propagated_unit_cls_heur
:: ‹nat clause_l ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹already_propagated_unit_cls_heur = (λL (M, N, D, Q, oth).
RETURN (M, N, D, Q, oth))›
lemma already_propagated_unit_cls_heur_already_propagated_unit_cls:
‹(uncurry already_propagated_unit_cls_heur, uncurry (RETURN oo already_propagated_unit_init_wl)) ∈
[λ(C, S). literals_are_in_ℒ⇩i⇩n 𝒜 C]⇩f
list_mset_rel ×⇩r twl_st_heur_parsing_no_WL 𝒜 unbdd → ⟨twl_st_heur_parsing_no_WL 𝒜 unbdd⟩ nres_rel›
by (intro frefI nres_relI)
(auto simp: twl_st_heur_parsing_no_WL_def already_propagated_unit_cls_heur_def
already_propagated_unit_init_wl_def all_lits_of_mm_add_mset all_lits_of_m_add_mset
literals_are_in_ℒ⇩i⇩n_def)
definition (in -) set_conflict_unit :: ‹nat literal ⇒ nat clause option ⇒ nat clause option› where
‹set_conflict_unit L _ = Some {#L#}›
definition set_conflict_unit_heur where
‹set_conflict_unit_heur = (λ L (b, n, xs). RETURN (False, 1, xs[atm_of L := Some (is_pos L)]))›
lemma set_conflict_unit_heur_set_conflict_unit:
‹(uncurry set_conflict_unit_heur, uncurry (RETURN oo set_conflict_unit)) ∈
[λ(L, D). D = None ∧ L ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f Id ×⇩f option_lookup_clause_rel 𝒜 →
⟨option_lookup_clause_rel 𝒜⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: twl_st_heur_def set_conflict_unit_heur_def set_conflict_unit_def
option_lookup_clause_rel_def lookup_clause_rel_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
intro!: mset_as_position.intros)
definition conflict_propagated_unit_cls
:: ‹nat literal ⇒ nat twl_st_wl_init ⇒ nat twl_st_wl_init›
where
‹conflict_propagated_unit_cls = (λL ((M, N, D, NE, UE, NS, US, Q), OC).
((M, N, set_conflict_unit L D, add_mset {#L#} NE, UE, NS, US, {#}), OC))›
definition conflict_propagated_unit_cls_heur
:: ‹nat literal ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹conflict_propagated_unit_cls_heur = (λL (M, N, D, Q, oth). do {
ASSERT(atm_of L < length (snd (snd D)));
D ← set_conflict_unit_heur L D;
ASSERT(isa_length_trail_pre M);
RETURN (M, N, D, isa_length_trail M, oth)
})›
lemma conflict_propagated_unit_cls_heur_conflict_propagated_unit_cls:
‹(uncurry conflict_propagated_unit_cls_heur, uncurry (RETURN oo set_conflict_init_wl)) ∈
[λ(L, S). L ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ get_conflict_init_wl S = None]⇩f
nat_lit_lit_rel ×⇩r twl_st_heur_parsing_no_WL 𝒜 unbdd → ⟨twl_st_heur_parsing_no_WL 𝒜 unbdd⟩ nres_rel›
proof -
have set_conflict_init_wl_alt_def:
‹RETURN oo set_conflict_init_wl = (λL ((M, N, D, NE, UE, NS, US, Q), OC). do {
D ← RETURN (set_conflict_unit L D);
RETURN ((M, N, Some {#L#}, add_mset {#L#} NE, UE, NS, US, {#}), OC)
})›
by (auto intro!: ext simp: set_conflict_init_wl_def)
have [refine0]: ‹D = None ∧ L ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ (y, None) ∈ option_lookup_clause_rel 𝒜 ⟹ L = L' ⟹
set_conflict_unit_heur L' y ≤ ⇓ {(D, D'). (D, D') ∈ option_lookup_clause_rel 𝒜 ∧ D' = Some {#L#}}
(RETURN (set_conflict_unit L D))›
for L D y L'
apply (rule order_trans)
apply (rule set_conflict_unit_heur_set_conflict_unit[THEN fref_to_Down_curry,
unfolded comp_def, of 𝒜 L D L' y])
subgoal
by auto
subgoal
by auto
subgoal
unfolding conc_fun_RETURN
by (auto simp: set_conflict_unit_def)
done
show ?thesis
supply RETURN_as_SPEC_refine[refine2 del]
unfolding set_conflict_init_wl_alt_def conflict_propagated_unit_cls_heur_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg)
subgoal
by (auto simp: twl_st_heur_parsing_no_WL_def option_lookup_clause_rel_def
lookup_clause_rel_def atms_of_def)
subgoal
by auto
subgoal
by auto
subgoal
by (auto simp: twl_st_heur_parsing_no_WL_def conflict_propagated_unit_cls_heur_def conflict_propagated_unit_cls_def
image_image set_conflict_unit_def
intro!: set_conflict_unit_heur_set_conflict_unit[THEN fref_to_Down_curry])
subgoal
by auto
subgoal
by (auto simp: twl_st_heur_parsing_no_WL_def conflict_propagated_unit_cls_heur_def
conflict_propagated_unit_cls_def
intro!: isa_length_trail_pre)
subgoal
by (auto simp: twl_st_heur_parsing_no_WL_def conflict_propagated_unit_cls_heur_def
conflict_propagated_unit_cls_def
image_image set_conflict_unit_def all_lits_of_mm_add_mset all_lits_of_m_add_mset uminus_𝒜⇩i⇩n_iff
isa_length_trail_length_u[THEN fref_to_Down_unRET_Id]
intro!: set_conflict_unit_heur_set_conflict_unit[THEN fref_to_Down_curry]
isa_length_trail_pre)
done
qed
definition add_init_cls_heur
:: ‹bool ⇒ nat clause_l ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹add_init_cls_heur unbdd = (λC (M, N, D, Q, W, vm, φ, clvls, cach, lbd, vdom, failed). do {
let C = C;
ASSERT(length C ≤ uint32_max + 2);
ASSERT(length C ≥ 2);
if unbdd ∨ (length N ≤ sint64_max - length C - 5 ∧ ¬failed)
then do {
ASSERT(length vdom ≤ length N);
(N, i) ← fm_add_new True C N;
RETURN (M, N, D, Q, W, vm, φ, clvls, cach, lbd, vdom @ [i], failed)
} else RETURN (M, N, D, Q, W, vm, φ, clvls, cach, lbd, vdom, True)})›
definition add_init_cls_heur_unb :: ‹nat clause_l ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹add_init_cls_heur_unb = add_init_cls_heur True›
definition add_init_cls_heur_b :: ‹nat clause_l ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹add_init_cls_heur_b = add_init_cls_heur False›
definition add_init_cls_heur_b' :: ‹nat literal list list ⇒ nat ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹add_init_cls_heur_b' C i = add_init_cls_heur False (C!i)›
lemma length_C_nempty_iff: ‹length C ≥ 2 ⟷ C ≠ [] ∧ tl C ≠ []›
by (cases C; cases ‹tl C›) auto
context
fixes unbdd :: bool and 𝒜 :: ‹nat multiset› and
CT :: ‹nat clause_l × twl_st_wl_heur_init› and
CSOC :: ‹nat clause_l × nat twl_st_wl_init› and
SOC :: ‹nat twl_st_wl_init› and
C C' :: ‹nat clause_l› and
S :: ‹nat twl_st_wl_init'› and x1a and N :: ‹nat clauses_l› and
D :: ‹nat cconflict› and x2b and NE UE NS US :: ‹nat clauses› and
M :: ‹(nat,nat) ann_lits› and
a b c d e f m p q r s t u v w x y and
Q and
x2e :: ‹nat lit_queue_wl› and OC :: ‹nat clauses› and
T :: twl_st_wl_heur_init and
M' :: ‹trail_pol› and N' :: arena and
D' :: conflict_option_rel and
j' :: nat and
W' :: ‹_› and
vm :: ‹isa_vmtf_remove_int_option_fst_As› and
clvls :: nat and
cach :: conflict_min_cach_l and
lbd :: lbd and
vdom :: vdom and
failed :: bool and
φ :: phase_saver
assumes
pre: ‹case CSOC of
(C, S) ⇒ 2 ≤ length C ∧ literals_are_in_ℒ⇩i⇩n 𝒜 (mset C) ∧ distinct C› and
xy: ‹(CT, CSOC) ∈ Id ×⇩f twl_st_heur_parsing_no_WL 𝒜 unbdd› and
st:
‹CSOC = (C, SOC)›
‹SOC = (S, OC)›
‹S = (M, a)›
‹a = (N, b)›
‹b = (D, c)›
‹c = (NE, d)›
‹d = (UE, e)›
‹e = (NS, f)›
‹f = (US, Q)›
‹CT = (C', T)›
‹T = (M', m)›
‹m = (N', p)›
‹p = (D', q)›
‹q = (j', r)›
‹r = (W', s)›
‹s = (vm, t)›
‹t = (φ, u)›
‹u = (clvls, v)›
‹v = (cach, w)›
‹w = (lbd, x)›
‹x = (vdom, failed)›
begin
lemma add_init_pre1: ‹length C' ≤ uint32_max + 2›
using pre clss_size_uint32_max[of 𝒜 ‹mset C›] xy st
by (auto simp: twl_st_heur_parsing_no_WL_def)
lemma add_init_pre2: ‹2 ≤ length C'›
using pre xy st by (auto simp: )
private lemma
x1g_x1: ‹C' = C› and
‹(M', M) ∈ trail_pol 𝒜› and
valid: ‹valid_arena N' N (set vdom)› and
‹(D', D) ∈ option_lookup_clause_rel 𝒜› and
‹j' ≤ length M› and
Q: ‹Q = {#- lit_of x. x ∈# mset (drop j' (rev M))#}› and
‹vm ∈ isa_vmtf_init 𝒜 M› and
‹phase_saving 𝒜 φ› and
‹no_dup M› and
‹cach_refinement_empty 𝒜 cach› and
vdom: ‹mset vdom = dom_m N› and
var_incl:
‹set_mset (all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + NE + NS + UE + US))
⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜)› and
watched: ‹(W', empty_watched 𝒜) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜)› and
bounded: ‹isasat_input_bounded 𝒜›
if ‹¬failed ∨ unbdd›
using that xy unfolding st twl_st_heur_parsing_no_WL_def
by (auto simp: ac_simps)
lemma init_fm_add_new:
‹¬failed ∨ unbdd ⟹ fm_add_new True C' N'
≤ ⇓ {((arena, i), (N'', i')). valid_arena arena N'' (insert i (set vdom)) ∧ i = i' ∧
i ∉# dom_m N ∧ i = length N' + header_size C ∧
i ∉ set vdom}
(SPEC
(λ(N', ia).
0 < ia ∧ ia ∉# dom_m N ∧ N' = fmupd ia (C, True) N))›
(is ‹_ ⟹ _ ≤ ⇓ ?qq _›)
unfolding x1g_x1
apply (rule order_trans)
apply (rule fm_add_new_append_clause)
using valid vdom pre xy valid_arena_in_vdom_le_arena[OF valid] arena_lifting(2)[OF valid]
valid unfolding st
by (fastforce simp: x1g_x1 vdom_m_def
intro!: RETURN_RES_refine valid_arena_append_clause)
lemma add_init_cls_final_rel:
fixes nN'j' :: ‹arena_el list × nat› and
nNj :: ‹(nat, nat literal list × bool) fmap × nat› and
nN :: ‹_› and
k :: ‹nat› and nN' :: ‹arena_el list› and
k' :: ‹nat›
assumes
‹(nN'j', nNj) ∈ {((arena, i), (N'', i')). valid_arena arena N'' (insert i (set vdom)) ∧ i = i' ∧
i ∉# dom_m N ∧ i = length N' + header_size C ∧
i ∉ set vdom}› and
‹nNj ∈ Collect (λ(N', ia).
0 < ia ∧ ia ∉# dom_m N ∧ N' = fmupd ia (C, True) N)›
‹nN'j' = (nN', k')› and
‹nNj = (nN, k)›
shows ‹((M', nN', D', j', W', vm, φ, clvls, cach, lbd, vdom @ [k'], failed),
(M, nN, D, NE, UE, NS, US, Q), OC)
∈ twl_st_heur_parsing_no_WL 𝒜 unbdd›
proof -
show ?thesis
using assms xy pre unfolding st
apply (auto simp: twl_st_heur_parsing_no_WL_def ac_simps
intro!: )
apply (auto simp: vdom_m_simps5 ran_m_mapsto_upd_notin all_lits_of_mm_add_mset
literals_are_in_ℒ⇩i⇩n_def)
done
qed
end
lemma add_init_cls_heur_add_init_cls:
‹(uncurry (add_init_cls_heur unbdd), uncurry (add_to_clauses_init_wl)) ∈
[λ(C, S). length C ≥ 2 ∧ literals_are_in_ℒ⇩i⇩n 𝒜 (mset C) ∧ distinct C]⇩f
Id ×⇩r twl_st_heur_parsing_no_WL 𝒜 unbdd → ⟨twl_st_heur_parsing_no_WL 𝒜 unbdd⟩ nres_rel›
proof -
have ‹42 + Max_mset (add_mset 0 (x1c)) ∉# x1c› and ‹42 + Max_mset (add_mset (0 :: nat) (x1c)) ≠ 0› for x1c
apply (cases ‹x1c›) apply (auto simp: max_def)
apply (metis Max_ge add.commute add.right_neutral add_le_cancel_left finite_set_mset le_zero_eq set_mset_add_mset_insert union_single_eq_member zero_neq_numeral)
by (smt Max_ge Set.set_insert add.commute add.right_neutral add_mset_commute antisym diff_add_inverse diff_le_self finite_insert finite_set_mset insert_DiffM insert_commute set_mset_add_mset_insert union_single_eq_member zero_neq_numeral)
then have [iff]: ‹(∀b. b = (0::nat) ∨ b ∈# x1c) ⟷ False› ‹∃b>0. b ∉# x1c›for x1c
by blast+
have add_to_clauses_init_wl_alt_def:
‹add_to_clauses_init_wl = (λi ((M, N, D, NE, UE, NS, US, Q), OC). do {
let b = (length i = 2);
(N', ia) ← SPEC (λ(N', ia). ia > 0 ∧ ia ∉# dom_m N ∧ N' = fmupd ia (i, True) N);
RETURN ((M, N', D, NE, UE, NS, US, Q), OC)
})›
by (auto simp: add_to_clauses_init_wl_def get_fresh_index_def Let_def
RES_RES2_RETURN_RES RES_RES_RETURN_RES2 RES_RETURN_RES uncurry_def image_iff
intro!: ext)
show ?thesis
unfolding add_init_cls_heur_def add_to_clauses_init_wl_alt_def uncurry_def Let_def
apply (intro frefI nres_relI)
apply (refine_vcg init_fm_add_new)
subgoal
by (rule add_init_pre1)
subgoal
by (rule add_init_pre2)
apply (rule lhs_step_If)
apply (refine_rcg)
subgoal unfolding twl_st_heur_parsing_no_WL_def
by (force dest!: valid_arena_vdom_le(2) simp: distinct_card)
apply (rule init_fm_add_new)
apply assumption+
subgoal by auto
subgoal by (rule add_init_cls_final_rel)
subgoal unfolding RES_RES2_RETURN_RES RETURN_def
apply simp
unfolding RETURN_def apply (rule RES_refine)
by (auto simp: twl_st_heur_parsing_no_WL_def RETURN_def intro!: RES_refine)
done
qed
definition already_propagated_unit_cls_conflict
:: ‹nat literal ⇒ nat twl_st_wl_init ⇒ nat twl_st_wl_init›
where
‹already_propagated_unit_cls_conflict = (λL ((M, N, D, NE, UE, NS, US, Q), OC).
((M, N, D, add_mset {#L#} NE, UE, NS, US, {#}), OC))›
definition already_propagated_unit_cls_conflict_heur
:: ‹nat literal ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹already_propagated_unit_cls_conflict_heur = (λL (M, N, D, Q, oth). do {
ASSERT (isa_length_trail_pre M);
RETURN (M, N, D, isa_length_trail M, oth)
})›
lemma already_propagated_unit_cls_conflict_heur_already_propagated_unit_cls_conflict:
‹(uncurry already_propagated_unit_cls_conflict_heur,
uncurry (RETURN oo already_propagated_unit_cls_conflict)) ∈
[λ(L, S). L ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f Id ×⇩r twl_st_heur_parsing_no_WL 𝒜 unbdd →
⟨twl_st_heur_parsing_no_WL 𝒜 unbdd⟩ nres_rel›
by (intro frefI nres_relI)
(auto simp: twl_st_heur_parsing_no_WL_def already_propagated_unit_cls_conflict_heur_def
already_propagated_unit_cls_conflict_def all_lits_of_mm_add_mset
all_lits_of_m_add_mset uminus_𝒜⇩i⇩n_iff isa_length_trail_length_u[THEN fref_to_Down_unRET_Id]
intro: vmtf_consD
intro!: ASSERT_leI isa_length_trail_pre)
definition (in -) set_conflict_empty :: ‹nat clause option ⇒ nat clause option› where
‹set_conflict_empty _ = Some {#}›
definition (in -) lookup_set_conflict_empty :: ‹conflict_option_rel ⇒ conflict_option_rel› where
‹lookup_set_conflict_empty = (λ(b, s) . (False, s))›
lemma lookup_set_conflict_empty_set_conflict_empty:
‹(RETURN o lookup_set_conflict_empty, RETURN o set_conflict_empty) ∈
[λD. D = None]⇩f option_lookup_clause_rel 𝒜 → ⟨option_lookup_clause_rel 𝒜⟩nres_rel›
by (intro frefI nres_relI) (auto simp: set_conflict_empty_def
lookup_set_conflict_empty_def option_lookup_clause_rel_def
lookup_clause_rel_def)
definition set_empty_clause_as_conflict_heur
:: ‹twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹set_empty_clause_as_conflict_heur = (λ (M, N, (_, (n, xs)), Q, WS). do {
ASSERT(isa_length_trail_pre M);
RETURN (M, N, (False, (n, xs)), isa_length_trail M, WS)})›
lemma set_empty_clause_as_conflict_heur_set_empty_clause_as_conflict:
‹(set_empty_clause_as_conflict_heur, RETURN o add_empty_conflict_init_wl) ∈
[λS. get_conflict_init_wl S = None]⇩f
twl_st_heur_parsing_no_WL 𝒜 unbdd → ⟨twl_st_heur_parsing_no_WL 𝒜 unbdd⟩ nres_rel›
by (intro frefI nres_relI)
(auto simp: set_empty_clause_as_conflict_heur_def add_empty_conflict_init_wl_def
twl_st_heur_parsing_no_WL_def set_conflict_empty_def option_lookup_clause_rel_def
lookup_clause_rel_def isa_length_trail_length_u[THEN fref_to_Down_unRET_Id]
intro!: isa_length_trail_pre ASSERT_leI)
definition (in -) add_clause_to_others_heur
:: ‹nat clause_l ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹add_clause_to_others_heur = (λ _ (M, N, D, Q, NS, US, WS).
RETURN (M, N, D, Q, NS, US, WS))›
lemma add_clause_to_others_heur_add_clause_to_others:
‹(uncurry add_clause_to_others_heur, uncurry (RETURN oo add_to_other_init)) ∈
⟨Id⟩list_rel ×⇩r twl_st_heur_parsing_no_WL 𝒜 unbdd →⇩f ⟨twl_st_heur_parsing_no_WL 𝒜 unbdd⟩ nres_rel›
by (intro frefI nres_relI)
(auto simp: add_clause_to_others_heur_def add_to_other_init.simps
twl_st_heur_parsing_no_WL_def)
definition (in -)list_length_1 where
[simp]: ‹list_length_1 C ⟷ length C = 1›
definition (in -)list_length_1_code where
‹list_length_1_code C ⟷ (case C of [_] ⇒ True | _ ⇒ False)›
definition (in -) get_conflict_wl_is_None_heur_init :: ‹twl_st_wl_heur_init ⇒ bool› where
‹get_conflict_wl_is_None_heur_init = (λ(M, N, (b, _), Q, _). b)›
definition init_dt_step_wl_heur
:: ‹bool ⇒ nat clause_l ⇒ twl_st_wl_heur_init ⇒ (twl_st_wl_heur_init) nres›
where
‹init_dt_step_wl_heur unbdd C S = do {
if get_conflict_wl_is_None_heur_init S
then do {
if is_Nil C
then set_empty_clause_as_conflict_heur S
else if list_length_1 C
then do {
ASSERT (C ≠ []);
let L = C ! 0;
ASSERT(polarity_pol_pre (get_trail_wl_heur_init S) L);
let val_L = polarity_pol (get_trail_wl_heur_init S) L;
if val_L = None
then propagate_unit_cls_heur L S
else
if val_L = Some True
then already_propagated_unit_cls_heur C S
else conflict_propagated_unit_cls_heur L S
}
else do {
ASSERT(length C ≥ 2);
add_init_cls_heur unbdd C S
}
}
else add_clause_to_others_heur C S
}›
named_theorems twl_st_heur_parsing_no_WL
lemma [twl_st_heur_parsing_no_WL]:
assumes ‹(S, T) ∈ twl_st_heur_parsing_no_WL 𝒜 unbdd›
shows ‹(get_trail_wl_heur_init S, get_trail_init_wl T) ∈ trail_pol 𝒜›
using assms
by (cases S; auto simp: twl_st_heur_parsing_no_WL_def; fail)+
definition get_conflict_wl_is_None_init :: ‹nat twl_st_wl_init ⇒ bool› where
‹get_conflict_wl_is_None_init = (λ((M, N, D, NE, UE, Q), OC). is_None D)›
lemma get_conflict_wl_is_None_init_alt_def:
‹get_conflict_wl_is_None_init S ⟷ get_conflict_init_wl S = None›
by (cases S) (auto simp: get_conflict_wl_is_None_init_def split: option.splits)
lemma get_conflict_wl_is_None_heur_get_conflict_wl_is_None_init:
‹(RETURN o get_conflict_wl_is_None_heur_init, RETURN o get_conflict_wl_is_None_init) ∈
twl_st_heur_parsing_no_WL 𝒜 unbdd →⇩f ⟨Id⟩nres_rel›
apply (intro frefI nres_relI)
apply (rename_tac x y, case_tac x, case_tac y)
by (auto simp: twl_st_heur_parsing_no_WL_def get_conflict_wl_is_None_heur_init_def option_lookup_clause_rel_def
get_conflict_wl_is_None_init_def split: option.splits)
definition (in -) get_conflict_wl_is_None_init' where
‹get_conflict_wl_is_None_init' = get_conflict_wl_is_None›
lemma init_dt_step_wl_heur_init_dt_step_wl:
‹(uncurry (init_dt_step_wl_heur unbdd), uncurry init_dt_step_wl) ∈
[λ(C, S). literals_are_in_ℒ⇩i⇩n 𝒜 (mset C) ∧ distinct C]⇩f
Id ×⇩f twl_st_heur_parsing_no_WL 𝒜 unbdd → ⟨twl_st_heur_parsing_no_WL 𝒜 unbdd⟩ nres_rel›
supply [[goals_limit=1]]
unfolding init_dt_step_wl_heur_def init_dt_step_wl_def uncurry_def
option.case_eq_if get_conflict_wl_is_None_init_alt_def[symmetric]
supply RETURN_as_SPEC_refine[refine2 del]
apply (intro frefI nres_relI)
apply (refine_vcg
set_empty_clause_as_conflict_heur_set_empty_clause_as_conflict[THEN fref_to_Down,
unfolded comp_def]
propagate_unit_cls_heur_propagate_unit_cls[THEN fref_to_Down_curry, unfolded comp_def]
already_propagated_unit_cls_heur_already_propagated_unit_cls[THEN fref_to_Down_curry,
unfolded comp_def]
conflict_propagated_unit_cls_heur_conflict_propagated_unit_cls[THEN fref_to_Down_curry,
unfolded comp_def]
add_init_cls_heur_add_init_cls[THEN fref_to_Down_curry,
unfolded comp_def]
add_clause_to_others_heur_add_clause_to_others[THEN fref_to_Down_curry,
unfolded comp_def])
subgoal by (auto simp: get_conflict_wl_is_None_heur_get_conflict_wl_is_None_init[THEN fref_to_Down_unRET_Id])
subgoal by (auto simp: twl_st_heur_parsing_no_WL_def is_Nil_def split: list.splits)
subgoal by (simp add: get_conflict_wl_is_None_init_alt_def)
subgoal by auto
subgoal by simp
subgoal by simp
subgoal by (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset
twl_st_heur_parsing_no_WL_def intro!: polarity_pol_pre split: list.splits)
subgoal for C'S CT C T C' S
by (subst polarity_pol_polarity[of 𝒜, unfolded option_rel_id_simp,
THEN fref_to_Down_unRET_uncurry_Id,
of ‹get_trail_init_wl T› ‹hd C›])
(auto simp: polarity_def twl_st_heur_parsing_no_WL_def
polarity_pol_polarity[of 𝒜, unfolded option_rel_id_simp, THEN fref_to_Down_unRET_uncurry_Id]
literals_are_in_ℒ⇩i⇩n_add_mset
split: list.splits)
subgoal by (auto simp: twl_st_heur_parsing_no_WL_def)
subgoal by (auto simp: twl_st_heur_parsing_no_WL_def literals_are_in_ℒ⇩i⇩n_add_mset
split: list.splits)
subgoal by (auto simp: twl_st_heur_parsing_no_WL_def hd_conv_nth)
subgoal for C'S CT C T C' S
by (subst polarity_pol_polarity[of 𝒜, unfolded option_rel_id_simp,
THEN fref_to_Down_unRET_uncurry_Id,
of ‹get_trail_init_wl T› ‹hd C›])
(auto simp: polarity_def twl_st_heur_parsing_no_WL_def
polarity_pol_polarity[of 𝒜, unfolded option_rel_id_simp, THEN fref_to_Down_unRET_uncurry_Id]
literals_are_in_ℒ⇩i⇩n_add_mset
split: list.splits)
subgoal by simp
subgoal by (auto simp: list_mset_rel_def br_def)
subgoal by (simp add: literals_are_in_ℒ⇩i⇩n_add_mset
split: list.splits)
subgoal by (simp add: get_conflict_wl_is_None_init_alt_def)
subgoal by (simp add: hd_conv_nth)
subgoal
by (auto simp: twl_st_heur_parsing_no_WL_def map_fun_rel_def literals_are_in_ℒ⇩i⇩n_add_mset
split: list.splits)
subgoal by simp
subgoal
by (auto simp: twl_st_heur_parsing_no_WL_def map_fun_rel_def literals_are_in_ℒ⇩i⇩n_add_mset
split: list.splits)
subgoal for x y x1 x2 C x2a
by (cases C; cases ‹tl C›)
(auto simp: twl_st_heur_parsing_no_WL_def map_fun_rel_def literals_are_in_ℒ⇩i⇩n_add_mset
split: list.splits)
subgoal by simp
subgoal by simp
subgoal by simp
done
lemma (in -) get_conflict_wl_is_None_heur_init_alt_def:
‹RETURN o get_conflict_wl_is_None_heur_init = (λ(M, N, (b, _), Q, W, _). RETURN b)›
by (auto simp: get_conflict_wl_is_None_heur_init_def intro!: ext)
definition polarity_st_heur_init :: ‹twl_st_wl_heur_init ⇒ _ ⇒ bool option› where
‹polarity_st_heur_init = (λ(M, _) L. polarity_pol M L)›
lemma polarity_st_heur_init_alt_def:
‹polarity_st_heur_init S L = polarity_pol (get_trail_wl_heur_init S) L›
by (cases S) (auto simp: polarity_st_heur_init_def)
definition polarity_st_init :: ‹'v twl_st_wl_init ⇒ 'v literal ⇒ bool option› where
‹polarity_st_init S = polarity (get_trail_init_wl S)›
lemma get_conflict_wl_is_None_init:
‹get_conflict_init_wl S = None ⟷ get_conflict_wl_is_None_init S›
by (cases S) (auto simp: get_conflict_wl_is_None_init_def split: option.splits)
definition init_dt_wl_heur
:: ‹bool ⇒ nat clause_l list ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹init_dt_wl_heur unbdd CS S = nfoldli CS (λ_. True)
(λC S. do {
init_dt_step_wl_heur unbdd C S}) S›
definition init_dt_step_wl_heur_unb :: ‹nat clause_l ⇒ twl_st_wl_heur_init ⇒ (twl_st_wl_heur_init) nres› where
‹init_dt_step_wl_heur_unb = init_dt_step_wl_heur True›
definition init_dt_wl_heur_unb :: ‹nat clause_l list ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹init_dt_wl_heur_unb = init_dt_wl_heur True›
definition init_dt_step_wl_heur_b :: ‹nat clause_l ⇒ twl_st_wl_heur_init ⇒ (twl_st_wl_heur_init) nres› where
‹init_dt_step_wl_heur_b = init_dt_step_wl_heur False›
definition init_dt_wl_heur_b :: ‹nat clause_l list ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹init_dt_wl_heur_b = init_dt_wl_heur False›
subsection ‹Extractions of the atoms in the state›
definition init_valid_rep :: "nat list ⇒ nat set ⇒ bool" where
‹init_valid_rep xs l ⟷
(∀L∈l. L < length xs) ∧
(∀L ∈ l. (xs ! L) mod 2 = 1) ∧
(∀L. L < length xs ⟶ (xs ! L) mod 2 = 1 ⟶ L ∈ l)›
definition isasat_atms_ext_rel :: ‹((nat list × nat × nat list) × nat set) set› where
‹isasat_atms_ext_rel = {((xs, n, atms), l).
init_valid_rep xs l ∧
n = Max (insert 0 l) ∧
length xs < uint32_max ∧
(∀s∈set xs. s ≤ uint64_max) ∧
finite l ∧
distinct atms ∧
set atms = l ∧
length xs ≠ 0
}›
lemma distinct_length_le_Suc_Max:
assumes ‹distinct (b :: nat list)›
shows ‹length b ≤ Suc (Max (insert 0 (set b)))›
proof -
have ‹set b ⊆ {0 ..< Suc (Max (insert 0 (set b)))}›
by (cases ‹set b = {}›)
(auto simp add: le_imp_less_Suc)
from card_mono[OF _ this] show ?thesis
using distinct_card[OF assms(1)] by auto
qed
lemma isasat_atms_ext_rel_alt_def:
‹isasat_atms_ext_rel = {((xs, n, atms), l).
init_valid_rep xs l ∧
n = Max (insert 0 l) ∧
length xs < uint32_max ∧
(∀s∈set xs. s ≤ uint64_max) ∧
finite l ∧
distinct atms ∧
set atms = l ∧
length xs ≠ 0 ∧
length atms ≤ Suc n
}›
by (auto simp: isasat_atms_ext_rel_def distinct_length_le_Suc_Max)
definition in_map_atm_of :: ‹'a ⇒ 'a list ⇒ bool› where
‹in_map_atm_of L N ⟷ L ∈ set N›
definition (in -) init_next_size where
‹init_next_size L = 2 * L›
lemma init_next_size: ‹L ≠ 0 ⟹ L + 1 ≤ uint32_max ⟹ L < init_next_size L›
by (auto simp: init_next_size_def uint32_max_def)
definition add_to_atms_ext where
‹add_to_atms_ext = (λi (xs, n, atms). do {
ASSERT(i ≤ uint32_max div 2);
ASSERT(length xs ≤ uint32_max);
ASSERT(length atms ≤ Suc n);
let n = max i n;
(if i < length_uint32_nat xs then do {
ASSERT(xs!i ≤ uint64_max);
let atms = (if xs!i AND 1 = 1 then atms else atms @ [i]);
RETURN (xs[i := 1], n, atms)
}
else do {
ASSERT(i + 1 ≤ uint32_max);
ASSERT(length_uint32_nat xs ≠ 0);
ASSERT(i < init_next_size i);
RETURN ((list_grow xs (init_next_size i) 0)[i := 1], n,
atms @ [i])
})
})›
lemma init_valid_rep_upd_OR:
‹init_valid_rep (x1b[x1a := a OR 1]) x2 ⟷
init_valid_rep (x1b[x1a := 1]) x2 › (is ‹?A ⟷ ?B›)
proof
assume ?A
then have
1: ‹∀L∈x2. L < length (x1b[x1a := a OR 1])› and
2: ‹∀L∈x2. x1b[x1a := a OR 1] ! L mod 2 = 1› and
3: ‹∀L<length (x1b[x1a := a OR 1]).
x1b[x1a := a OR 1] ! L mod 2 = 1 ⟶
L ∈ x2›
unfolding init_valid_rep_def by fast+
have 1: ‹∀L∈x2. L < length (x1b[x1a := 1])›
using 1 by simp
then have 2: ‹∀L∈x2. x1b[x1a := 1] ! L mod 2 = 1›
using 2 by (auto simp: nth_list_update')
then have 3: ‹∀L<length (x1b[x1a := 1]).
x1b[x1a := 1] ! L mod 2 = 1 ⟶
L ∈ x2›
using 3 by (auto split: if_splits simp: bitOR_1_if_mod_2_nat)
show ?B
using 1 2 3
unfolding init_valid_rep_def by fast+
next
assume ?B
then have
1: ‹∀L∈x2. L < length (x1b[x1a := 1])› and
2: ‹∀L∈x2. x1b[x1a := 1] ! L mod 2 = 1› and
3: ‹∀L<length (x1b[x1a := 1]).
x1b[x1a := 1] ! L mod 2 = 1 ⟶
L ∈ x2›
unfolding init_valid_rep_def by fast+
have 1: ‹∀L∈x2. L < length (x1b[x1a := a OR 1])›
using 1 by simp
then have 2: ‹∀L∈x2. x1b[x1a := a OR 1] ! L mod 2 = 1›
using 2 by (auto simp: nth_list_update' bitOR_1_if_mod_2_nat)
then have 3: ‹∀L<length (x1b[x1a := a OR 1]).
x1b[x1a := a OR 1] ! L mod 2 = 1 ⟶
L ∈ x2›
using 3 by (auto split: if_splits simp: bitOR_1_if_mod_2_nat)
show ?A
using 1 2 3
unfolding init_valid_rep_def by fast+
qed
lemma init_valid_rep_insert:
assumes val: ‹init_valid_rep x1b x2› and le: ‹x1a < length x1b›
shows ‹init_valid_rep (x1b[x1a := Suc 0]) (insert x1a x2)›
proof -
have
1: ‹∀L∈x2. L < length x1b› and
2: ‹∀L∈x2. x1b ! L mod 2 = 1› and
3: ‹⋀L. L<length x1b ⟹ x1b ! L mod 2 = 1 ⟶ L ∈ x2›
using val unfolding init_valid_rep_def by fast+
have 1: ‹∀L∈insert x1a x2. L < length (x1b[x1a := 1])›
using 1 le by simp
then have 2: ‹∀L∈insert x1a x2. x1b[x1a := 1] ! L mod 2 = 1›
using 2 by (auto simp: nth_list_update')
then have 3: ‹∀L<length (x1b[x1a := 1]).
x1b[x1a := 1] ! L mod 2 = 1 ⟶
L ∈ insert x1a x2›
using 3 le by (auto split: if_splits simp: bitOR_1_if_mod_2_nat)
show ?thesis
using 1 2 3
unfolding init_valid_rep_def by auto
qed
lemma init_valid_rep_extend:
‹init_valid_rep (x1b @ replicate n 0) x2 ⟷ init_valid_rep (x1b) x2›
(is ‹?A ⟷ ?B› is ‹init_valid_rep ?x1b _ ⟷ _›)
proof
assume ?A
then have
1: ‹⋀L. L∈x2 ⟹ L < length ?x1b› and
2: ‹⋀L. L∈x2 ⟹ ?x1b ! L mod 2 = 1› and
3: ‹⋀L. L<length ?x1b ⟹ ?x1b ! L mod 2 = 1 ⟶ L ∈ x2›
unfolding init_valid_rep_def by fast+
have 1: ‹L∈x2 ⟹ L < length x1b› for L
using 3[of L] 2[of L] 1[of L]
by (auto simp: nth_append split: if_splits)
then have 2: ‹∀L∈x2. x1b ! L mod 2 = 1›
using 2 by (auto simp: nth_list_update')
then have 3: ‹∀L<length x1b. x1b ! L mod 2 = 1 ⟶ L ∈ x2›
using 3 by (auto split: if_splits simp: bitOR_1_if_mod_2_nat)
show ?B
using 1 2 3
unfolding init_valid_rep_def by fast
next
assume ?B
then have
1: ‹⋀L. L∈x2 ⟹ L < length x1b› and
2: ‹⋀L. L∈x2 ⟹ x1b ! L mod 2 = 1› and
3: ‹⋀L. L<length x1b ⟶ x1b ! L mod 2 = 1 ⟶ L ∈ x2›
unfolding init_valid_rep_def by fast+
have 10: ‹∀L∈x2. L < length ?x1b›
using 1 by fastforce
then have 20: ‹L∈x2 ⟹ ?x1b ! L mod 2 = 1› for L
using 1[of L] 2[of L] 3[of L] by (auto simp: nth_list_update' bitOR_1_if_mod_2_nat nth_append)
then have 30: ‹L<length ?x1b ⟹ ?x1b ! L mod 2 = 1 ⟶ L ∈ x2›for L
using 1[of L] 2[of L] 3[of L]
by (auto split: if_splits simp: bitOR_1_if_mod_2_nat nth_append)
show ?A
using 10 20 30
unfolding init_valid_rep_def by fast+
qed
lemma init_valid_rep_in_set_iff:
‹init_valid_rep x1b x2 ⟹ x ∈ x2 ⟷ (x < length x1b ∧ (x1b!x) mod 2 = 1)›
unfolding init_valid_rep_def
by auto
lemma add_to_atms_ext_op_set_insert:
‹(uncurry add_to_atms_ext, uncurry (RETURN oo Set.insert))
∈ [λ(n, l). n ≤ uint32_max div 2]⇩f nat_rel ×⇩f isasat_atms_ext_rel → ⟨isasat_atms_ext_rel⟩nres_rel›
proof -
have H: ‹finite x2 ⟹ Max (insert x1 (insert 0 x2)) = Max (insert x1 x2)›
‹finite x2 ⟹ Max (insert 0 (insert x1 x2)) = Max (insert x1 x2)›
for x1 and x2 :: ‹nat set›
by (subst insert_commute) auto
have [simp]: ‹(a OR Suc 0) mod 2 = Suc 0› for a
by (auto simp add: bitOR_1_if_mod_2_nat)
show ?thesis
apply (intro frefI nres_relI)
unfolding isasat_atms_ext_rel_def add_to_atms_ext_def uncurry_def
apply (refine_vcg lhs_step_If)
subgoal by auto
subgoal by auto
subgoal unfolding isasat_atms_ext_rel_def[symmetric] isasat_atms_ext_rel_alt_def by auto
subgoal by auto
subgoal for x y x1 x2 x1a x2a x1b x2b
unfolding comp_def
apply (rule RETURN_refine)
apply (subst in_pair_collect_simp)
apply (subst prod.case)+
apply (intro conjI impI allI)
subgoal by (simp add: init_valid_rep_upd_OR init_valid_rep_insert
del: )
subgoal by (auto simp: H Max_insert[symmetric] simp del: Max_insert)
subgoal by auto
subgoal
unfolding bitOR_1_if_mod_2_nat
by (auto simp del: simp: uint64_max_def
elim!: in_set_upd_cases)
subgoal
unfolding bitAND_1_mod_2
by (auto simp add: init_valid_rep_in_set_iff)
subgoal
unfolding bitAND_1_mod_2
by (auto simp add: init_valid_rep_in_set_iff)
subgoal
unfolding bitAND_1_mod_2
by (auto simp add: init_valid_rep_in_set_iff)
subgoal
by (auto simp add: init_valid_rep_in_set_iff)
done
subgoal by (auto simp: uint32_max_def)
subgoal by (auto simp: uint32_max_def)
subgoal by (auto simp: uint32_max_def init_next_size_def elim: neq_NilE)
subgoal
unfolding comp_def list_grow_def
apply (rule RETURN_refine)
apply (subst in_pair_collect_simp)
apply (subst prod.case)+
apply (intro conjI impI allI)
subgoal
unfolding init_next_size_def
apply (simp del: )
apply (subst init_valid_rep_insert)
apply (auto elim: neq_NilE)
apply (subst init_valid_rep_extend)
apply (auto elim: neq_NilE)
done
subgoal by (auto simp: H Max_insert[symmetric] simp del: Max_insert)
subgoal by (auto simp: init_next_size_def uint32_max_def)
subgoal
unfolding bitOR_1_if_mod_2_nat
by (auto simp: uint64_max_def
elim!: in_set_upd_cases)
subgoal by (auto simp: init_valid_rep_in_set_iff)
subgoal by (auto simp add: init_valid_rep_in_set_iff)
subgoal by (auto simp add: init_valid_rep_in_set_iff)
subgoal by (auto simp add: init_valid_rep_in_set_iff)
done
done
qed
definition extract_atms_cls :: ‹'a clause_l ⇒ 'a set ⇒ 'a set› where
‹extract_atms_cls C 𝒜⇩i⇩n = fold (λL 𝒜⇩i⇩n. insert (atm_of L) 𝒜⇩i⇩n) C 𝒜⇩i⇩n›
definition extract_atms_cls_i :: ‹nat clause_l ⇒ nat set ⇒ nat set nres› where
‹extract_atms_cls_i C 𝒜⇩i⇩n = nfoldli C (λ_. True)
(λL 𝒜⇩i⇩n. do {
ASSERT(atm_of L ≤ uint32_max div 2);
RETURN(insert (atm_of L) 𝒜⇩i⇩n)})
𝒜⇩i⇩n›
lemma fild_insert_insert_swap:
‹fold (λL. insert (f L)) C (insert a 𝒜⇩i⇩n) = insert a (fold (λL. insert (f L)) C 𝒜⇩i⇩n)›
by (induction C arbitrary: a 𝒜⇩i⇩n) (auto simp: extract_atms_cls_def)
lemma extract_atms_cls_alt_def: ‹extract_atms_cls C 𝒜⇩i⇩n = 𝒜⇩i⇩n ∪ atm_of ` set C›
by (induction C) (auto simp: extract_atms_cls_def fild_insert_insert_swap)
lemma extract_atms_cls_i_extract_atms_cls:
‹(uncurry extract_atms_cls_i, uncurry (RETURN oo extract_atms_cls))
∈ [λ(C, 𝒜⇩i⇩n). ∀L∈set C. nat_of_lit L ≤ uint32_max]⇩f
⟨Id⟩list_rel ×⇩f Id → ⟨Id⟩nres_rel›
proof -
have H1: ‹(x1a, x1) ∈ ⟨{(L, L'). L = L' ∧ nat_of_lit L ≤ uint32_max}⟩list_rel›
if
‹case y of (C, 𝒜⇩i⇩n) ⇒ ∀L∈set C. nat_of_lit L ≤ uint32_max› and
‹(x, y) ∈ ⟨nat_lit_lit_rel⟩list_rel ×⇩f Id› and
‹y = (x1, x2)› and
‹x = (x1a, x2a)›
for x :: ‹nat literal list × nat set› and y :: ‹nat literal list × nat set› and
x1 :: ‹nat literal list› and x2 :: ‹nat set› and x1a :: ‹nat literal list› and x2a :: ‹nat set›
using that by (auto simp: list_rel_def list_all2_conj list.rel_eq list_all2_conv_all_nth)
have atm_le: ‹nat_of_lit xa ≤ uint32_max ⟹ atm_of xa ≤ uint32_max div 2› for xa
by (cases xa) (auto simp: uint32_max_def)
show ?thesis
supply RETURN_as_SPEC_refine[refine2 del]
unfolding extract_atms_cls_i_def extract_atms_cls_def uncurry_def comp_def
fold_eq_nfoldli
apply (intro frefI nres_relI)
apply (refine_rcg H1)
apply assumption+
subgoal by auto
subgoal by auto
subgoal by (auto simp: atm_le)
subgoal by auto
done
qed
definition extract_atms_clss:: ‹'a clause_l list ⇒ 'a set ⇒ 'a set› where
‹extract_atms_clss N 𝒜⇩i⇩n = fold extract_atms_cls N 𝒜⇩i⇩n›
definition extract_atms_clss_i :: ‹nat clause_l list ⇒ nat set ⇒ nat set nres› where
‹extract_atms_clss_i N 𝒜⇩i⇩n = nfoldli N (λ_. True) extract_atms_cls_i 𝒜⇩i⇩n›
lemma extract_atms_clss_i_extract_atms_clss:
‹(uncurry extract_atms_clss_i, uncurry (RETURN oo extract_atms_clss))
∈ [λ(N, 𝒜⇩i⇩n). ∀C∈set N. ∀L∈set C. nat_of_lit L ≤ uint32_max]⇩f
⟨Id⟩list_rel ×⇩f Id → ⟨Id⟩nres_rel›
proof -
have H1: ‹(x1a, x1) ∈ ⟨{(C, C'). C = C' ∧ (∀L∈set C. nat_of_lit L ≤ uint32_max)}⟩list_rel›
if
‹case y of (N, 𝒜⇩i⇩n) ⇒ ∀C∈set N. ∀L∈set C. nat_of_lit L ≤ uint32_max› and
‹(x, y) ∈ ⟨Id⟩list_rel ×⇩f Id› and
‹y = (x1, x2)› and
‹x = (x1a, x2a)›
for x :: ‹nat literal list list × nat set› and y :: ‹nat literal list list × nat set› and
x1 :: ‹nat literal list list› and x2 :: ‹nat set› and x1a :: ‹nat literal list list›
and x2a :: ‹nat set›
using that by (auto simp: list_rel_def list_all2_conj list.rel_eq list_all2_conv_all_nth)
show ?thesis
supply RETURN_as_SPEC_refine[refine2 del]
unfolding extract_atms_clss_i_def extract_atms_clss_def comp_def fold_eq_nfoldli uncurry_def
apply (intro frefI nres_relI)
apply (refine_vcg H1 extract_atms_cls_i_extract_atms_cls[THEN fref_to_Down_curry,
unfolded comp_def])
apply assumption+
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma fold_extract_atms_cls_union_swap:
‹fold extract_atms_cls N (𝒜⇩i⇩n ∪ a) = fold extract_atms_cls N 𝒜⇩i⇩n ∪ a›
by (induction N arbitrary: a 𝒜⇩i⇩n) (auto simp: extract_atms_cls_alt_def)
lemma extract_atms_clss_alt_def:
‹extract_atms_clss N 𝒜⇩i⇩n = 𝒜⇩i⇩n ∪ ((⋃C∈set N. atm_of ` set C))›
by (induction N)
(auto simp: extract_atms_clss_def extract_atms_cls_alt_def
fold_extract_atms_cls_union_swap)
lemma finite_extract_atms_clss[simp]: ‹finite (extract_atms_clss CS' {})› for CS'
by (auto simp: extract_atms_clss_alt_def)
definition op_extract_list_empty where
‹op_extract_list_empty = {}›
definition extract_atms_clss_imp_empty_rel where
‹extract_atms_clss_imp_empty_rel = (RETURN (replicate 1024 0, 0, []))›
lemma extract_atms_clss_imp_empty_rel:
‹(λ_. extract_atms_clss_imp_empty_rel, λ_. (RETURN op_extract_list_empty)) ∈
unit_rel →⇩f ⟨isasat_atms_ext_rel⟩ nres_rel›
by (intro frefI nres_relI)
(simp add: op_extract_list_empty_def uint32_max_def
isasat_atms_ext_rel_def init_valid_rep_def extract_atms_clss_imp_empty_rel_def
del: replicate_numeral)
lemma extract_atms_cls_Nil[simp]:
‹extract_atms_cls [] 𝒜⇩i⇩n = 𝒜⇩i⇩n›
unfolding extract_atms_cls_def fold.simps by simp
lemma extract_atms_clss_Cons[simp]:
‹extract_atms_clss (C # Cs) N = extract_atms_clss Cs (extract_atms_cls C N)›
by (simp add: extract_atms_clss_def)
definition (in -) all_lits_of_atms_m :: ‹'a multiset ⇒ 'a clause› where
‹all_lits_of_atms_m N = poss N + negs N›
lemma (in -) all_lits_of_atms_m_nil[simp]: ‹all_lits_of_atms_m {#} = {#}›
unfolding all_lits_of_atms_m_def by auto
definition (in -) all_lits_of_atms_mm :: ‹'a multiset multiset ⇒ 'a clause› where
‹all_lits_of_atms_mm N = poss (⋃# N) + negs (⋃# N)›
lemma all_lits_of_atms_m_all_lits_of_m:
‹all_lits_of_atms_m N = all_lits_of_m (poss N)›
unfolding all_lits_of_atms_m_def all_lits_of_m_def
by (induction N) auto
subsubsection ‹Creation of an initial state›
definition init_dt_wl_heur_spec
:: ‹bool ⇒ nat multiset ⇒ nat clause_l list ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init ⇒ bool›
where
‹init_dt_wl_heur_spec unbdd 𝒜 CS T TOC ⟷
(∃T' TOC'. (TOC, TOC') ∈ twl_st_heur_parsing_no_WL 𝒜 unbdd ∧ (T, T') ∈ twl_st_heur_parsing_no_WL 𝒜 unbdd ∧
init_dt_wl_spec CS T' TOC')›
definition init_state_wl :: ‹nat twl_st_wl_init'› where
‹init_state_wl = ([], fmempty, None, {#}, {#}, {#}, {#}, {#})›
definition init_state_wl_heur :: ‹nat multiset ⇒ twl_st_wl_heur_init nres› where
‹init_state_wl_heur 𝒜 = do {
M ← SPEC(λM. (M, []) ∈ trail_pol 𝒜);
D ← SPEC(λD. (D, None) ∈ option_lookup_clause_rel 𝒜);
W ← SPEC (λW. (W, empty_watched 𝒜) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜));
vm ← RES (isa_vmtf_init 𝒜 []);
φ ← SPEC (phase_saving 𝒜);
cach ← SPEC (cach_refinement_empty 𝒜);
let lbd = empty_lbd;
let vdom = [];
RETURN (M, [], D, 0, W, vm, φ, 0, cach, lbd, vdom, False)}›
definition init_state_wl_heur_fast where
‹init_state_wl_heur_fast = init_state_wl_heur›
lemma init_state_wl_heur_init_state_wl:
‹(λ_. (init_state_wl_heur 𝒜), λ_. (RETURN init_state_wl)) ∈
[λ_. isasat_input_bounded 𝒜]⇩f unit_rel → ⟨twl_st_heur_parsing_no_WL_wl 𝒜 unbdd⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: init_state_wl_heur_def init_state_wl_def
RES_RETURN_RES bind_RES_RETURN_eq RES_RES_RETURN_RES RETURN_def
twl_st_heur_parsing_no_WL_wl_def vdom_m_def empty_watched_def valid_arena_empty
intro!: RES_refine)
definition (in -)to_init_state :: ‹nat twl_st_wl_init' ⇒ nat twl_st_wl_init› where
‹to_init_state S = (S, {#})›
definition (in -) from_init_state :: ‹nat twl_st_wl_init_full ⇒ nat twl_st_wl› where
‹from_init_state = fst›
definition (in -) to_init_state_code where
‹to_init_state_code = id›
definition from_init_state_code where
‹from_init_state_code = id›
definition (in -) conflict_is_None_heur_wl where
‹conflict_is_None_heur_wl = (λ(M, N, U, D, _). is_None D)›
definition (in -) finalise_init where
‹finalise_init = id›
subsection ‹Parsing›
lemma init_dt_wl_heur_init_dt_wl:
‹(uncurry (init_dt_wl_heur unbdd), uncurry init_dt_wl) ∈
[λ(CS, S). (∀C ∈ set CS. literals_are_in_ℒ⇩i⇩n 𝒜 (mset C)) ∧ distinct_mset_set (mset ` set CS)]⇩f
⟨Id⟩list_rel ×⇩f twl_st_heur_parsing_no_WL 𝒜 unbdd → ⟨twl_st_heur_parsing_no_WL 𝒜 unbdd⟩ nres_rel›
proof -
have H: ‹⋀x y x1 x2 x1a x2a.
(∀C∈set x1. literals_are_in_ℒ⇩i⇩n 𝒜 (mset C)) ∧ distinct_mset_set (mset ` set x1) ⟹
(x1a, x1) ∈ ⟨Id⟩list_rel ⟹
(x1a, x1) ∈ ⟨{(C, C'). C = C' ∧ literals_are_in_ℒ⇩i⇩n 𝒜 (mset C) ∧
distinct C}⟩list_rel›
apply (auto simp: list_rel_def list_all2_conj)
apply (auto simp: list_all2_conv_all_nth distinct_mset_set_def)
done
show ?thesis
unfolding init_dt_wl_heur_def init_dt_wl_def uncurry_def
apply (intro frefI nres_relI)
apply (case_tac y rule: prod.exhaust)
apply (case_tac x rule: prod.exhaust)
apply (simp only: prod.case prod_rel_iff)
apply (refine_vcg init_dt_step_wl_heur_init_dt_step_wl[THEN fref_to_Down_curry] H)
apply normalize_goal+
subgoal by fast
subgoal by fast
subgoal by simp
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: twl_st_heur_parsing_no_WL_def)
done
qed
definition rewatch_heur_st
:: ‹twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹rewatch_heur_st = (λ(M', N', D', j, W, vm, φ, clvls, cach, lbd, vdom, failed). do {
ASSERT(length vdom ≤ length N');
W ← rewatch_heur vdom N' W;
RETURN (M', N', D', j, W, vm, φ, clvls, cach, lbd, vdom, failed)
})›
lemma rewatch_heur_st_correct_watching:
assumes
‹(S, T) ∈ twl_st_heur_parsing_no_WL 𝒜 unbdd› and failed: ‹¬is_failed_heur_init S›
‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf (get_clauses_init_wl T))› and
‹⋀x. x ∈# dom_m (get_clauses_init_wl T) ⟹ distinct (get_clauses_init_wl T ∝ x) ∧
2 ≤ length (get_clauses_init_wl T ∝ x)›
shows ‹rewatch_heur_st S ≤ ⇓ (twl_st_heur_parsing 𝒜 unbdd)
(SPEC (λ((M,N, D, NE, UE, NS, US, Q, W), OC). T = ((M,N,D,NE,UE,NS, US, Q), OC)∧
correct_watching (M, N, D, NE, UE, NS, US, Q, W)))›
proof -
obtain M N D NE UE NS US Q OC where
T: ‹T = ((M,N, D, NE, UE, NS, US, Q), OC)›
by (cases T) auto
obtain M' N' D' j W vm φ clvls cach lbd vdom where
S: ‹S = (M', N', D', j, W, vm, φ, clvls, cach, lbd, vdom, False)›
using failed by (cases S) auto
have valid: ‹valid_arena N' N (set vdom)› and
dist: ‹distinct vdom› and
dom_m_vdom: ‹set_mset (dom_m N) ⊆ set vdom› and
W: ‹(W, empty_watched 𝒜) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜)› and
lits: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N)›
using assms distinct_mset_dom[of N] apply (auto simp: twl_st_heur_parsing_no_WL_def S T
simp flip: distinct_mset_mset_distinct)
by (metis distinct_mset_set_mset_ident set_mset_mset subset_mset.eq_iff)+
have H: ‹RES ({(W, W').
(W, W') ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜) ∧ vdom_m 𝒜 W' N ⊆ set_mset (dom_m N)}¯ ``
{W. Watched_Literals_Watch_List_Initialisation.correct_watching_init
(M, N, D, NE, UE, NS, US, Q, W)})
≤ RES ({(W, W').
(W, W') ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜) ∧ vdom_m 𝒜 W' N ⊆ set_mset (dom_m N)}¯ ``
{W. Watched_Literals_Watch_List_Initialisation.correct_watching_init
(M, N, D, NE, UE, NS, US, Q, W)})›
for W'
by (rule order.refl)
have eq: ‹Watched_Literals_Watch_List_Initialisation.correct_watching_init
(M, N, None, NE, UE, NS, US, {#}, xa) ⟹
vdom_m 𝒜 xa N = set_mset (dom_m N)› for xa
by (auto 5 5 simp: Watched_Literals_Watch_List_Initialisation.correct_watching_init.simps
vdom_m_def)
show ?thesis
supply [[goals_limit=1]]
using assms
unfolding rewatch_heur_st_def T S
apply clarify
apply (rule ASSERT_leI)
subgoal by (auto dest: valid_arena_vdom_subset simp: twl_st_heur_parsing_no_WL_def)
apply (rule bind_refine_res)
prefer 2
apply (rule order.trans)
apply (rule rewatch_heur_rewatch[OF valid _ dist dom_m_vdom W lits])
apply (solves simp)
apply (solves simp)
apply (rule order_trans[OF ref_two_step'])
apply (rule rewatch_correctness)
apply (rule empty_watched_def)
subgoal
using assms
by (auto simp: twl_st_heur_parsing_no_WL_def)
apply (subst conc_fun_RES)
apply (rule H) apply (rule RETURN_RES_refine)
apply (auto simp: twl_st_heur_parsing_def twl_st_heur_parsing_no_WL_def all_atms_def[symmetric]
intro!: exI[of _ N] exI[of _ D] exI[of _ M]
intro!: )
apply (rule_tac x=W' in exI)
apply (auto simp: eq correct_watching_init_correct_watching dist)
apply (rule_tac x=W' in exI)
apply (auto simp: eq correct_watching_init_correct_watching dist)
done
qed
subsubsection ‹Full Initialisation›
definition rewatch_heur_st_fast where
‹rewatch_heur_st_fast = rewatch_heur_st›
definition rewatch_heur_st_fast_pre where
‹rewatch_heur_st_fast_pre S =
((∀x ∈ set (get_vdom_heur_init S). x ≤ sint64_max) ∧ length (get_clauses_wl_heur_init S) ≤ sint64_max)›
definition init_dt_wl_heur_full
:: ‹bool ⇒ _ ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹init_dt_wl_heur_full unb CS S = do {
S ← init_dt_wl_heur unb CS S;
ASSERT(¬is_failed_heur_init S);
rewatch_heur_st S
}›
definition init_dt_wl_heur_full_unb
:: ‹_ ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹init_dt_wl_heur_full_unb = init_dt_wl_heur_full True›
lemma init_dt_wl_heur_full_init_dt_wl_full:
assumes
‹init_dt_wl_pre CS T› and
‹∀C∈set CS. literals_are_in_ℒ⇩i⇩n 𝒜 (mset C)› and
‹distinct_mset_set (mset ` set CS)› and
‹(S, T) ∈ twl_st_heur_parsing_no_WL 𝒜 True›
shows ‹init_dt_wl_heur_full True CS S
≤ ⇓ (twl_st_heur_parsing 𝒜 True) (init_dt_wl_full CS T)›
proof -
have H: ‹valid_arena x1g x1b (set x1p)› ‹set x1p ⊆ set x1p› ‹set_mset (dom_m x1b) ⊆ set x1p›
‹distinct x1p› ‹(x1j, λ_. []) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜)›
if
xx': ‹(x, x') ∈ twl_st_heur_parsing_no_WL 𝒜 True› and
st: ‹x2c = (x1e, x2d)›
‹x2b = (x1d, x2c)›
‹x2a = (x1c, x2b)›
‹x2 = (x1b, x2a)›
‹x1 = (x1a, x2)›
‹x' = (x1, x2e)›
‹x2o = (x1p, x2p)›
‹x2n = (x1o, x2o)›
‹x2m = (x1n, x2n)›
‹x2l = (x1m, x2m)›
‹x2k = (x1l, x2l)›
‹x2j = (x1k, x2k)›
‹x2i = (x1j, x2j)›
‹x2h = (x1i, x2i)›
‹x2g = (x1h, x2h)›
‹x2f = (x1g, x2g)›
‹x = (x1f, x2f)›
for x x' x1 x1a x2 x1b x2a x1c x2b x1d x2c x1e x2d x2e x1f x2f x1g x2g x1h x2h
x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m x1n x2n x1o x2o x1p x2p
proof -
show ‹valid_arena x1g x1b (set x1p)› ‹set x1p ⊆ set x1p› ‹set_mset (dom_m x1b) ⊆ set x1p›
‹distinct x1p› ‹(x1j, λ_. []) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜)›
using xx' distinct_mset_dom[of x1b] unfolding st
by (auto simp: twl_st_heur_parsing_no_WL_def empty_watched_def
simp flip: set_mset_mset distinct_mset_mset_distinct)
qed
show ?thesis
unfolding init_dt_wl_heur_full_def init_dt_wl_full_def rewatch_heur_st_def
apply (refine_rcg rewatch_heur_rewatch[of _ _ _ _ _ _ 𝒜]
init_dt_wl_heur_init_dt_wl[of True 𝒜, THEN fref_to_Down_curry])
subgoal using assms by fast
subgoal using assms by fast
subgoal using assms by auto
subgoal by (auto simp: twl_st_heur_parsing_def twl_st_heur_parsing_no_WL_def)
subgoal by (auto dest: valid_arena_vdom_subset simp: twl_st_heur_parsing_no_WL_def)
apply ((rule H; assumption)+)[5]
subgoal
by (auto simp: twl_st_heur_parsing_def twl_st_heur_parsing_no_WL_def
literals_are_in_ℒ⇩i⇩n_mm_def all_lits_of_mm_union)
subgoal by (auto simp: twl_st_heur_parsing_def twl_st_heur_parsing_no_WL_def
empty_watched_def[symmetric] map_fun_rel_def vdom_m_def)
subgoal by (auto simp: twl_st_heur_parsing_def twl_st_heur_parsing_no_WL_def
empty_watched_def[symmetric])
done
qed
lemma init_dt_wl_heur_full_init_dt_wl_spec_full:
assumes
‹init_dt_wl_pre CS T› and
‹∀C∈set CS. literals_are_in_ℒ⇩i⇩n 𝒜 (mset C)› and
‹distinct_mset_set (mset ` set CS)› and
‹(S, T) ∈ twl_st_heur_parsing_no_WL 𝒜 True›
shows ‹init_dt_wl_heur_full True CS S
≤ ⇓ (twl_st_heur_parsing 𝒜 True) (SPEC (init_dt_wl_spec_full CS T))›
apply (rule order.trans)
apply (rule init_dt_wl_heur_full_init_dt_wl_full[OF assms])
apply (rule ref_two_step')
apply (rule init_dt_wl_full_init_dt_wl_spec_full[OF assms(1)])
done
subsection ‹Conversion to normal state›
definition extract_lits_sorted where
‹extract_lits_sorted = (λ(xs, n, vars). do {
vars ← ―‹insert\_sort\_nth2 xs vars›RETURN vars;
RETURN (vars, n)
})›
definition lits_with_max_rel where
‹lits_with_max_rel = {((xs, n), 𝒜⇩i⇩n). mset xs = 𝒜⇩i⇩n ∧ n = Max (insert 0 (set xs)) ∧
length xs < uint32_max}›
lemma extract_lits_sorted_mset_set:
‹(extract_lits_sorted, RETURN o mset_set)
∈ isasat_atms_ext_rel →⇩f ⟨lits_with_max_rel⟩nres_rel›
proof -
have K: ‹RETURN o mset_set = (λv. do {v' ← SPEC(λv'. v' = mset_set v); RETURN v'})›
by auto
have K': ‹length x2a < uint32_max› if ‹distinct b› ‹init_valid_rep x1 (set b)›
‹length x1 < uint32_max› ‹mset x2a = mset b›for x1 x2a b
proof -
have ‹distinct x2a›
by (simp add: same_mset_distinct_iff that(1) that(4))
have ‹length x2a = length b› ‹set x2a = set b›
using ‹mset x2a = mset b› apply (metis size_mset)
using ‹mset x2a = mset b› by (rule mset_eq_setD)
then have ‹set x2a ⊆ {0..<uint32_max - 1}›
using that by (auto simp: init_valid_rep_def)
from card_mono[OF _ this] show ?thesis
using ‹distinct x2a› by (auto simp: uint32_max_def distinct_card)
qed
have H_simple: ‹RETURN x2a
≤ ⇓ (list_mset_rel ∩ {(v, v'). length v < uint32_max})
(SPEC (λv'. v' = mset_set y))›
if
‹(x, y) ∈ isasat_atms_ext_rel› and
‹x2 = (x1a, x2a)› and
‹x = (x1, x2)›
for x :: ‹nat list × nat × nat list› and y :: ‹nat set› and x1 :: ‹nat list› and
x2 :: ‹nat × nat list› and x1a :: ‹nat› and x2a :: ‹nat list›
using that mset_eq_length by (auto simp: isasat_atms_ext_rel_def list_mset_rel_def br_def
mset_set_set RETURN_def intro: K' intro!: RES_refine dest: mset_eq_length)
show ?thesis
unfolding extract_lits_sorted_def reorder_list_def K
apply (intro frefI nres_relI)
apply (refine_vcg H_simple)
apply assumption+
by (auto simp: lits_with_max_rel_def isasat_atms_ext_rel_def mset_set_set list_mset_rel_def
br_def dest!: mset_eq_setD)
qed
text ‹TODO Move›
text ‹The value 160 is random (but larger than the default 16 for array lists).›
definition finalise_init_code :: ‹opts ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur nres› where
‹finalise_init_code opts =
(λ(M', N', D', Q', W', ((ns, m, fst_As, lst_As, next_search), to_remove), φ, clvls, cach,
lbd, vdom, _). do {
ASSERT(lst_As ≠ None ∧ fst_As ≠ None);
let init_stats = (0::64 word, 0::64 word, 0::64 word, 0::64 word, 0::64 word, 0::64 word, 0::64 word, 0::64 word);
let fema = ema_fast_init;
let sema = ema_slow_init;
let ccount = restart_info_init;
let lcount = 0;
RETURN (M', N', D', Q', W', ((ns, m, the fst_As, the lst_As, next_search), to_remove),
clvls, cach, lbd, take 1(replicate 160 (Pos 0)), init_stats,
(fema, sema, ccount, 0, φ, 0, replicate (length φ) False, 0, replicate (length φ) False, 10000, 1000, 1), vdom, [], lcount, opts, [])
})›
lemma isa_vmtf_init_nemptyD: ‹((ak, al, am, an, bc), ao, bd)
∈ isa_vmtf_init 𝒜 au ⟹ 𝒜 ≠ {#} ⟹ ∃y. an = Some y›
‹((ak, al, am, an, bc), ao, bd)
∈ isa_vmtf_init 𝒜 au ⟹ 𝒜 ≠ {#} ⟹ ∃y. am = Some y›
by (auto simp: isa_vmtf_init_def vmtf_init_def)
lemma isa_vmtf_init_isa_vmtf: ‹𝒜 ≠ {#} ⟹ ((ak, al, Some am, Some an, bc), ao, bd)
∈ isa_vmtf_init 𝒜 au ⟹ ((ak, al, am, an, bc), ao, bd)
∈ isa_vmtf 𝒜 au›
by (auto simp: isa_vmtf_init_def vmtf_init_def Image_iff intro!: isa_vmtfI)
lemma heuristic_rel_initI:
‹phase_saving 𝒜 φ ⟹ length φ' = length φ ⟹ length φ'' = length φ ⟹ heuristic_rel 𝒜 (fema, sema, ccount, 0, (φ,a, φ',b,φ'',c,d))›
by (auto simp: heuristic_rel_def phase_save_heur_rel_def phase_saving_def)
lemma finalise_init_finalise_init_full:
‹get_conflict_wl S = None ⟹
all_atms_st S ≠ {#} ⟹ size (learned_clss_l (get_clauses_wl S)) = 0 ⟹
((ops', T), ops, S) ∈ Id ×⇩f twl_st_heur_post_parsing_wl True ⟹
finalise_init_code ops' T ≤ ⇓ {(S', T'). (S', T') ∈ twl_st_heur ∧
get_clauses_wl_heur_init T = get_clauses_wl_heur S'} (RETURN (finalise_init S))›
apply (cases S; cases T)
apply (simp add: finalise_init_code_def)
apply (auto simp: finalise_init_def twl_st_heur_def twl_st_heur_parsing_no_WL_def
twl_st_heur_parsing_no_WL_wl_def
finalise_init_code_def out_learned_def all_atms_def
twl_st_heur_post_parsing_wl_def
intro!: ASSERT_leI intro!: isa_vmtf_init_isa_vmtf heuristic_rel_initI
dest: isa_vmtf_init_nemptyD)
done
lemma finalise_init_finalise_init:
‹(uncurry finalise_init_code, uncurry (RETURN oo (λ_. finalise_init))) ∈
[λ(_, S::nat twl_st_wl). get_conflict_wl S = None ∧ all_atms_st S ≠ {#} ∧
size (learned_clss_l (get_clauses_wl S)) = 0]⇩f Id ×⇩r
twl_st_heur_post_parsing_wl True → ⟨twl_st_heur⟩nres_rel›
apply (intro frefI nres_relI)
subgoal for x y
using finalise_init_finalise_init_full[of ‹snd y› ‹fst x› ‹snd x› ‹fst y›]
by (cases x; cases y)
(auto intro: "weaken_⇓'")
done
definition (in -) init_rll :: ‹nat ⇒ (nat, 'v clause_l × bool) fmap› where
‹init_rll n = fmempty›
definition (in -) init_aa :: ‹nat ⇒ 'v list› where
‹init_aa n = []›
definition (in -) init_aa' :: ‹nat ⇒ (clause_status × nat × nat) list› where
‹init_aa' n = []›
definition init_trail_D :: ‹nat list ⇒ nat ⇒ nat ⇒ trail_pol nres› where
‹init_trail_D 𝒜⇩i⇩n n m = do {
let M0 = [];
let cs = [];
let M = replicate m UNSET;
let M' = replicate n 0;
let M'' = replicate n 1;
RETURN ((M0, M, M', M'', 0, cs))
}›
definition init_trail_D_fast where
‹init_trail_D_fast = init_trail_D›
definition init_state_wl_D' :: ‹nat list × nat ⇒ (trail_pol × _ × _) nres› where
‹init_state_wl_D' = (λ(𝒜⇩i⇩n, n). do {
ASSERT(Suc (2 * (n)) ≤ uint32_max);
let n = Suc (n);
let m = 2 * n;
M ← init_trail_D 𝒜⇩i⇩n n m;
let N = [];
let D = (True, 0, replicate n NOTIN);
let WS = replicate m [];
vm ← initialise_VMTF 𝒜⇩i⇩n n;
let φ = replicate n False;
let cach = (replicate n SEEN_UNKNOWN, []);
let lbd = empty_lbd;
let vdom = [];
RETURN (M, N, D, 0, WS, vm, φ, 0, cach, lbd, vdom, False)
})›
lemma init_trail_D_ref:
‹(uncurry2 init_trail_D, uncurry2 (RETURN ooo (λ _ _ _. []))) ∈ [λ((N, n), m). mset N = 𝒜⇩i⇩n ∧
distinct N ∧ (∀L∈set N. L < n) ∧ m = 2 * n ∧ isasat_input_bounded 𝒜⇩i⇩n]⇩f
⟨Id⟩list_rel ×⇩f nat_rel ×⇩f nat_rel →
⟨trail_pol 𝒜⇩i⇩n⟩ nres_rel›
proof -
have K: ‹(∀L∈set N. L < n) ⟷
(∀L ∈# (ℒ⇩a⇩l⇩l (mset N)). atm_of L < n)› for N n
apply (rule iffI)
subgoal by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
subgoal by (metis (full_types) image_eqI in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n literal.sel(1)
set_image_mset set_mset_mset)
done
have K': ‹(∀L∈set N. L < n) ⟹
(∀L ∈# (ℒ⇩a⇩l⇩l (mset N)). nat_of_lit L < 2 * n)›
(is ‹?A ⟹ ?B›) for N n
proof -
assume ?A
then show ?B
apply (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
apply (case_tac L)
apply auto
done
qed
show ?thesis
unfolding init_trail_D_def
apply (intro frefI nres_relI)
unfolding uncurry_def Let_def comp_def trail_pol_def
apply clarify
unfolding RETURN_refine_iff
apply clarify
apply (intro conjI)
subgoal
by (auto simp: ann_lits_split_reasons_def
list_mset_rel_def Collect_eq_comp list_rel_def
list_all2_op_eq_map_right_iff' Id_def
br_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n
dest: multi_member_split)
subgoal
by auto
subgoal using K' by (auto simp: polarity_def)
subgoal
by (auto simp:
nat_shiftr_div2 in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
polarity_atm_def trail_pol_def K
phase_saving_def list_rel_mset_rel_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n
list_rel_def Id_def br_def list_all2_op_eq_map_right_iff'
ann_lits_split_reasons_def
list_mset_rel_def Collect_eq_comp)
subgoal
by auto
subgoal
by auto
subgoal
by (auto simp: control_stack.empty)
subgoal by auto
done
qed
definition [to_relAPP]: "mset_rel A ≡ p2rel (rel_mset (rel2p A))"
lemma in_mset_rel_eq_f_iff:
‹(a, b) ∈ ⟨{(c, a). a = f c}⟩mset_rel ⟷ b = f `# a›
using ex_mset[of a]
by (auto simp: mset_rel_def br_def rel2p_def[abs_def] p2rel_def rel_mset_def
list_all2_op_eq_map_right_iff' cong: ex_cong)
lemma in_mset_rel_eq_f_iff_set:
‹⟨{(c, a). a = f c}⟩mset_rel = {(b, a). a = f `# b}›
using in_mset_rel_eq_f_iff[of _ _ f] by blast
lemma init_state_wl_D0:
‹(init_state_wl_D', init_state_wl_heur) ∈
[λN. N = 𝒜⇩i⇩n ∧ distinct_mset 𝒜⇩i⇩n ∧ isasat_input_bounded 𝒜⇩i⇩n]⇩f
lits_with_max_rel O ⟨Id⟩mset_rel →
⟨Id ×⇩r Id ×⇩r
Id ×⇩r nat_rel ×⇩r ⟨⟨Id⟩list_rel⟩list_rel ×⇩r
Id ×⇩r ⟨bool_rel⟩list_rel ×⇩r Id ×⇩r Id ×⇩r Id⟩nres_rel›
(is ‹?C ∈ [?Pre]⇩f ?arg → ⟨?im⟩nres_rel›)
proof -
have init_state_wl_heur_alt_def: ‹init_state_wl_heur 𝒜⇩i⇩n = do {
M ← SPEC (λM. (M, []) ∈ trail_pol 𝒜⇩i⇩n);
N ← RETURN [];
D ← SPEC (λD. (D, None) ∈ option_lookup_clause_rel 𝒜⇩i⇩n);
W ← SPEC (λW. (W, empty_watched 𝒜⇩i⇩n ) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜⇩i⇩n));
vm ← RES (isa_vmtf_init 𝒜⇩i⇩n []);
φ ← SPEC (phase_saving 𝒜⇩i⇩n);
cach ← SPEC (cach_refinement_empty 𝒜⇩i⇩n);
let lbd = empty_lbd;
let vdom = [];
RETURN (M, N, D, 0, W, vm, φ, 0, cach, lbd, vdom, False)}› for 𝒜⇩i⇩n
unfolding init_state_wl_heur_def Let_def by auto
have tr: ‹distinct_mset 𝒜⇩i⇩n ∧ (∀L∈#𝒜⇩i⇩n. L < b) ⟹
(𝒜⇩i⇩n', 𝒜⇩i⇩n) ∈ ⟨Id⟩list_rel_mset_rel ⟹ isasat_input_bounded 𝒜⇩i⇩n ⟹
b' = 2 * b ⟹
init_trail_D 𝒜⇩i⇩n' b (2 * b) ≤ ⇓ (trail_pol 𝒜⇩i⇩n) (RETURN [])› for b' b 𝒜⇩i⇩n 𝒜⇩i⇩n' x
by (rule init_trail_D_ref[unfolded fref_def nres_rel_def, simplified, rule_format])
(auto simp: list_rel_mset_rel_def list_mset_rel_def br_def)
have [simp]: ‹comp_fun_idem (max :: 'a :: {zero,linorder} ⇒ _)›
unfolding comp_fun_idem_def comp_fun_commute_def comp_fun_idem_axioms_def
by (auto simp: max_def[abs_def] intro!: ext)
have [simp]: ‹fold max x a = Max (insert a (set x))› for x and a :: ‹'a :: {zero,linorder}›
by (auto simp: Max.eq_fold comp_fun_idem.fold_set_fold)
have in_N0: ‹L ∈ set 𝒜⇩i⇩n ⟹ L < Suc ((Max (insert 0 (set 𝒜⇩i⇩n))))›
for L 𝒜⇩i⇩n
using Max_ge[of ‹insert 0 (set 𝒜⇩i⇩n)› L]
by (auto simp del: Max_ge simp: nat_shiftr_div2)
define P where ‹P x = {(a, b). b = [] ∧ (a, b) ∈ trail_pol x}› for x
have P: ‹(c, []) ∈ P x ⟷ (c, []) ∈ trail_pol x› for c x
unfolding P_def by auto
have [simp]: ‹{p. ∃x. p = (x, x)} = {(y, x). x = y}›
by auto
have [simp]: ‹⋀a 𝒜⇩i⇩n. (a, 𝒜⇩i⇩n) ∈ ⟨nat_rel⟩mset_rel ⟷ 𝒜⇩i⇩n = a›
by (auto simp: Id_def br_def in_mset_rel_eq_f_iff list_rel_mset_rel_def
in_mset_rel_eq_f_iff)
have [simp]: ‹(a, mset a) ∈ ⟨Id⟩list_rel_mset_rel› for a
unfolding list_rel_mset_rel_def
by (rule relcompI [of _ ‹a›])
(auto simp: list_rel_def Id_def br_def list_all2_op_eq_map_right_iff'
list_mset_rel_def)
have init: ‹init_trail_D x1 (Suc (x2))
(2 * Suc (x2)) ≤
SPEC (λc. (c, []) ∈ trail_pol 𝒜⇩i⇩n)›
if ‹distinct_mset 𝒜⇩i⇩n› and x: ‹(𝒜⇩i⇩n', 𝒜⇩i⇩n) ∈ ?arg› and
‹𝒜⇩i⇩n' = (x1, x2)› and ‹isasat_input_bounded 𝒜⇩i⇩n›
for 𝒜⇩i⇩n 𝒜⇩i⇩n' x1 x2
unfolding x P
by (rule tr[unfolded conc_fun_RETURN])
(use that in ‹auto simp: lits_with_max_rel_def dest: in_N0›)
have H:
‹(replicate (2 * Suc (b)) [], empty_watched 𝒜⇩i⇩n)
∈ ⟨Id⟩map_fun_rel ((λL. (nat_of_lit L, L)) ` set_mset (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n))›
if ‹(x, 𝒜⇩i⇩n) ∈ ?arg› and
‹x = (a, b)›
for 𝒜⇩i⇩n x a b
using that unfolding map_fun_rel_def
by (auto simp: empty_watched_def ℒ⇩a⇩l⇩l_def
lits_with_max_rel_def
intro!: nth_replicate dest!: in_N0
simp del: replicate.simps)
have initialise_VMTF: ‹(∀L∈#aa. L < b) ∧ distinct_mset aa ∧ (a, aa) ∈
⟨Id⟩list_rel_mset_rel ∧ size aa < uint32_max ⟹
initialise_VMTF a b ≤ RES (isa_vmtf_init aa [])›
for aa b a
using initialise_VMTF[of aa, THEN fref_to_Down_curry, of aa b a b]
by (auto simp: isa_vmtf_init_def conc_fun_RES)
have [simp]: ‹(x, y) ∈ ⟨Id⟩list_rel_mset_rel ⟹ L ∈# y ⟹
L < Suc ((Max (insert 0 (set x))))›
for x y L
by (auto simp: list_rel_mset_rel_def br_def list_rel_def Id_def
list_all2_op_eq_map_right_iff' list_mset_rel_def dest: in_N0)
have initialise_VMTF: ‹initialise_VMTF a (Suc (b)) ≤
⇓ Id (RES (isa_vmtf_init y []))›
if ‹(x, y) ∈ ?arg› and ‹distinct_mset y› and ‹length a < uint32_max› and ‹x = (a, b)› for x y a b
using that
by (auto simp: P_def lits_with_max_rel_def intro!: initialise_VMTF in_N0)
have K[simp]: ‹(x, 𝒜⇩i⇩n) ∈ ⟨Id⟩list_rel_mset_rel ⟹
L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n) ⟹ L < Suc ((Max (insert 0 (set x))))›
for x L 𝒜⇩i⇩n
unfolding atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n
by (auto simp: list_rel_mset_rel_def br_def list_rel_def Id_def
list_all2_op_eq_map_right_iff' list_mset_rel_def)
have cach: ‹RETURN (replicate (Suc (b)) SEEN_UNKNOWN, [])
≤ ⇓ Id
(SPEC (cach_refinement_empty y))›
if
‹y = 𝒜⇩i⇩n ∧ distinct_mset 𝒜⇩i⇩n› and
‹(x, y) ∈ ?arg› and
‹x = (a, b)›
for M W vm vma φ x y a b
proof -
show ?thesis
unfolding cach_refinement_empty_def RETURN_RES_refine_iff
cach_refinement_alt_def Bex_def
by (rule exI[of _ ‹(replicate (Suc (b)) SEEN_UNKNOWN, [])›]) (use that in
‹auto simp: map_fun_rel_def empty_watched_def ℒ⇩a⇩l⇩l_def
list_mset_rel_def lits_with_max_rel_def
simp del: replicate_Suc
dest!: in_N0 intro: K›)
qed
have conflict: ‹RETURN (True, 0, replicate (Suc (b)) NOTIN)
≤ SPEC (λD. (D, None) ∈ option_lookup_clause_rel 𝒜⇩i⇩n)›
if
‹y = 𝒜⇩i⇩n ∧ distinct_mset 𝒜⇩i⇩n ∧ isasat_input_bounded 𝒜⇩i⇩n› and
‹((a, b), 𝒜⇩i⇩n) ∈ lits_with_max_rel O ⟨Id⟩mset_rel› and
‹x = (a, b)›
for a b x y
proof -
have ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n) ⟹
L < Suc (b)› for L
using that in_N0 by (auto simp: atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n
lits_with_max_rel_def)
then show ?thesis
by (auto simp: option_lookup_clause_rel_def
lookup_clause_rel_def simp del: replicate_Suc
intro: mset_as_position.intros)
qed
have [simp]:
‹NO_MATCH 0 a1 ⟹ max 0 (Max (insert a1 (set a2))) = max a1 (Max (insert 0 (set a2)))›
for a1 :: nat and a2
by (metis (mono_tags, lifting) List.finite_set Max_insert all_not_in_conv finite_insert insertI1 insert_commute)
have le_uint32: ‹∀L∈#ℒ⇩a⇩l⇩l (mset a). nat_of_lit L ≤ uint32_max ⟹
Suc (2 * (Max (insert 0 (set a)))) ≤ uint32_max› for a
apply (induction a)
apply (auto simp: uint32_max_def)
apply (auto simp: max_def ℒ⇩a⇩l⇩l_add_mset)
done
show ?thesis
apply (intro frefI nres_relI)
subgoal for x y
unfolding init_state_wl_heur_alt_def init_state_wl_D'_def
apply (rewrite in ‹let _ = Suc _in _› Let_def)
apply (rewrite in ‹let _ = 2 * _in _› Let_def)
apply (cases x; simp only: prod.case)
apply (refine_rcg init[of y x] initialise_VMTF cach)
subgoal for a b by (auto simp: lits_with_max_rel_def intro: le_uint32)
subgoal by (auto intro!: K[of _ 𝒜⇩i⇩n] simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n
lits_with_max_rel_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (rule conflict)
subgoal by (rule RETURN_rule) (rule H; simp only:)
apply assumption
subgoal by fast
subgoal by (auto simp: lits_with_max_rel_def P_def)
subgoal by simp
subgoal unfolding phase_saving_def lits_with_max_rel_def by (auto intro!: K)
subgoal by fast
subgoal by fast
apply assumption
apply (rule refl)
subgoal by (auto simp: P_def init_rll_def option_lookup_clause_rel_def
lookup_clause_rel_def lits_with_max_rel_def
simp del: replicate.simps
intro!: mset_as_position.intros K)
done
done
qed
lemma init_state_wl_D':
‹(init_state_wl_D', init_state_wl_heur) ∈
[λ𝒜⇩i⇩n. distinct_mset 𝒜⇩i⇩n ∧ isasat_input_bounded 𝒜⇩i⇩n]⇩f
lits_with_max_rel O ⟨Id⟩mset_rel →
⟨Id ×⇩r Id ×⇩r
Id ×⇩r nat_rel ×⇩r ⟨⟨Id⟩list_rel⟩list_rel ×⇩r
Id ×⇩r ⟨bool_rel⟩list_rel ×⇩r Id ×⇩r Id ×⇩r Id ×⇩r Id⟩nres_rel›
apply -
apply (intro frefI nres_relI)
by (rule init_state_wl_D0[THEN fref_to_Down, THEN order_trans]) auto
lemma init_state_wl_heur_init_state_wl':
‹(init_state_wl_heur, RETURN o (λ_. init_state_wl))
∈ [λN. N = 𝒜⇩i⇩n ∧ isasat_input_bounded 𝒜⇩i⇩n]⇩f Id → ⟨twl_st_heur_parsing_no_WL_wl 𝒜⇩i⇩n True⟩nres_rel›
apply (intro frefI nres_relI)
unfolding comp_def
using init_state_wl_heur_init_state_wl[THEN fref_to_Down, of 𝒜⇩i⇩n ‹()› ‹()›]
by auto
lemma all_blits_are_in_problem_init_blits_in: ‹all_blits_are_in_problem_init S ⟹ blits_in_ℒ⇩i⇩n S›
unfolding blits_in_ℒ⇩i⇩n_def
by (cases S)
(auto simp: all_blits_are_in_problem_init.simps ac_simps
ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm all_lits_def)
lemma correct_watching_init_blits_in_ℒ⇩i⇩n:
assumes ‹correct_watching_init S›
shows ‹blits_in_ℒ⇩i⇩n S›
proof -
show ?thesis
using assms
by (cases S)
(auto simp: all_blits_are_in_problem_init_blits_in
correct_watching_init.simps)
qed
fun append_empty_watched where
‹append_empty_watched ((M, N, D, NE, UE, NS, US, Q), OC) = ((M, N, D, NE, UE, NS, US, Q, (λ_. [])), OC)›
fun remove_watched :: ‹'v twl_st_wl_init_full ⇒ 'v twl_st_wl_init› where
‹remove_watched ((M, N, D, NE, UE, NS, US, Q, _), OC) = ((M, N, D, NE, UE, NS, US, Q), OC)›
definition init_dt_wl' :: ‹'v clause_l list ⇒ 'v twl_st_wl_init ⇒ 'v twl_st_wl_init_full nres› where
‹init_dt_wl' CS S = do{
S ← init_dt_wl CS S;
RETURN (append_empty_watched S)
}›
lemma init_dt_wl'_spec: ‹init_dt_wl_pre CS S ⟹ init_dt_wl' CS S ≤ ⇓
({(S :: 'v twl_st_wl_init_full, S' :: 'v twl_st_wl_init).
remove_watched S = S'}) (SPEC (init_dt_wl_spec CS S))›
unfolding init_dt_wl'_def
by (refine_vcg bind_refine_spec[OF _ init_dt_wl_init_dt_wl_spec])
(auto intro!: RETURN_RES_refine)
lemma init_dt_wl'_init_dt:
‹init_dt_wl_pre CS S ⟹ (S, S') ∈ state_wl_l_init ⟹ ∀C∈set CS. distinct C ⟹
init_dt_wl' CS S ≤ ⇓
({(S :: 'v twl_st_wl_init_full, S' :: 'v twl_st_wl_init).
remove_watched S = S'} O state_wl_l_init) (init_dt CS S')›
unfolding init_dt_wl'_def
apply (refine_vcg bind_refine[of _ _ _ _ _ ‹RETURN›, OF init_dt_wl_init_dt, simplified])
subgoal for S T
by (cases S; cases T)
auto
done
definition isasat_init_fast_slow :: ‹twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹isasat_init_fast_slow =
(λ(M', N', D', j, W', vm, φ, clvls, cach, lbd, vdom, failed).
RETURN (trail_pol_slow_of_fast M', N', D', j, convert_wlists_to_nat_conv W', vm, φ,
clvls, cach, lbd, vdom, failed))›
lemma isasat_init_fast_slow_alt_def:
‹isasat_init_fast_slow S = RETURN S›
unfolding isasat_init_fast_slow_def trail_pol_slow_of_fast_alt_def
convert_wlists_to_nat_conv_def
by auto
end