Theory IsaSAT_Initialisation
theory IsaSAT_Initialisation
imports Watched_Literals.Watched_Literals_Watch_List_Initialisation
IsaSAT_Setup IsaSAT_VMTF WB_More_Word
IsaSAT_Mark Tuple15
IsaSAT_Bump_Heuristics_Init_State
Automatic_Refinement.Relators
begin
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
chapter ‹Initialisation›
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 _›]›)
type_synonym (in -) twl_st_wl_heur_init =
‹(trail_pol, arena, conflict_option_rel, nat,
(nat × nat literal × bool) list list, bump_heuristics_init, bool list,
nat, conflict_min_cach_l, lbd, vdom, vdom, bool, clss_size, lookup_clause_rel) tuple15›
type_synonym (in -) twl_st_wl_heur_init_full =
‹(trail_pol, arena, conflict_option_rel, nat,
(nat × nat literal × bool) list list, bump_heuristics_init, bool list,
nat, conflict_min_cach_l, lbd, vdom, vdom, bool, clss_size, lookup_clause_rel) tuple15›
abbreviation get_trail_init_wl_heur :: ‹twl_st_wl_heur_init ⇒ trail_pol› where
‹get_trail_init_wl_heur ≡ Tuple15_a›
abbreviation set_trail_init_wl_heur :: ‹trail_pol ⇒ _ ⇒ twl_st_wl_heur_init› where
‹set_trail_init_wl_heur ≡ Tuple15.set_a›
abbreviation get_clauses_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ arena› where
‹get_clauses_wl_heur_init ≡ Tuple15_b›
abbreviation set_clauses_wl_heur_init :: ‹arena ⇒ _ ⇒ twl_st_wl_heur_init› where
‹set_clauses_wl_heur_init ≡ Tuple15.set_b›
abbreviation get_conflict_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ conflict_option_rel› where
‹get_conflict_wl_heur_init ≡ Tuple15_c›
abbreviation set_conflict_wl_heur_init :: ‹conflict_option_rel ⇒ _ ⇒ twl_st_wl_heur_init› where
‹set_conflict_wl_heur_init ≡ Tuple15.set_c›
abbreviation get_literals_to_update_wl_init :: ‹twl_st_wl_heur_init ⇒ nat› where
‹get_literals_to_update_wl_init ≡ Tuple15_d›
abbreviation set_literals_to_update_wl_init :: ‹nat ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init› where
‹set_literals_to_update_wl_init ≡ Tuple15.set_d›
abbreviation get_watchlist_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ (nat × nat literal × bool) list list› where
‹get_watchlist_wl_heur_init ≡ Tuple15_e›
abbreviation set_watchlist_wl_heur_init :: ‹(nat × nat literal × bool) list list ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init› where
‹set_watchlist_wl_heur_init ≡ Tuple15.set_e›
abbreviation get_vmtf_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ bump_heuristics_init› where
‹get_vmtf_wl_heur_init ≡ Tuple15_f›
abbreviation set_vmtf_wl_heur_init :: ‹bump_heuristics_init ⇒ twl_st_wl_heur_init ⇒ _› where
‹set_vmtf_wl_heur_init ≡ Tuple15.set_f›
abbreviation get_phases_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ bool list› where
‹get_phases_wl_heur_init ≡ Tuple15_g›
abbreviation set_phases_wl_heur_init :: ‹bool list ⇒ twl_st_wl_heur_init ⇒ _› where
‹set_phases_wl_heur_init ≡ Tuple15.set_g›
abbreviation get_clvls_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ nat› where
‹get_clvls_wl_heur_init ≡ Tuple15_h›
abbreviation set_clvls_wl_heur_init :: ‹nat ⇒ twl_st_wl_heur_init ⇒ _› where
‹set_clvls_wl_heur_init ≡ Tuple15.set_h›
abbreviation get_cach_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ conflict_min_cach_l› where
‹get_cach_wl_heur_init ≡ Tuple15_i›
abbreviation set_cach_wl_heur_init :: ‹conflict_min_cach_l ⇒ twl_st_wl_heur_init ⇒ _› where
‹set_cach_wl_heur_init ≡ Tuple15.set_i›
abbreviation get_lbd_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ lbd› where
‹get_lbd_wl_heur_init ≡ Tuple15_j›
abbreviation set_lbd_wl_heur_init :: ‹lbd ⇒ twl_st_wl_heur_init ⇒ _› where
‹set_lbd_wl_heur_init ≡ Tuple15.set_j›
abbreviation get_vdom_heur_init :: ‹twl_st_wl_heur_init ⇒ vdom› where
‹get_vdom_heur_init ≡ Tuple15_k›
abbreviation set_vdom_heur_init :: ‹vdom ⇒ twl_st_wl_heur_init ⇒ _› where
‹set_vdom_heur_init ≡ Tuple15.set_k›
abbreviation get_ivdom_heur_init :: ‹twl_st_wl_heur_init ⇒ vdom› where
‹get_ivdom_heur_init ≡ Tuple15_l›
abbreviation set_ivdom_heur_init :: ‹vdom ⇒ twl_st_wl_heur_init ⇒ _› where
‹set_ivdom_heur_init ≡ Tuple15.set_l›
abbreviation is_failed_heur_init :: ‹twl_st_wl_heur_init ⇒ bool› where
‹is_failed_heur_init ≡ Tuple15_m›
abbreviation set_failed_heur_init :: ‹bool ⇒ twl_st_wl_heur_init ⇒ _› where
‹set_failed_heur_init ≡ Tuple15.set_m›
abbreviation get_learned_count_init :: ‹twl_st_wl_heur_init ⇒ clss_size› where
‹get_learned_count_init ≡ Tuple15_n›
abbreviation set_learned_count_init :: ‹clss_size ⇒ twl_st_wl_heur_init ⇒ _› where
‹set_learned_count_init ≡ Tuple15.set_n›
abbreviation get_mark_wl_heur_init :: ‹twl_st_wl_heur_init ⇒ lookup_clause_rel› where
‹get_mark_wl_heur_init ≡ Tuple15_o›
abbreviation set_mark_wl_heur_init :: ‹lookup_clause_rel ⇒ twl_st_wl_heur_init ⇒ _› where
‹set_mark_wl_heur_init ≡ Tuple15.set_o›
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
[unfolded Let_def]: ‹twl_st_heur_parsing_no_WL 𝒜 unbdd =
{(S,
((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q), OC)).
let M' = get_trail_init_wl_heur S; N' = get_clauses_wl_heur_init S; failed = is_failed_heur_init S;
vdom = get_vdom_heur_init S; ivdom = get_ivdom_heur_init S; D' = get_conflict_wl_heur_init S; vm = get_vmtf_wl_heur_init S;
mark = get_mark_wl_heur_init S; lcount = get_learned_count_init S; W' = get_watchlist_wl_heur_init S;
φ = get_phases_wl_heur_init S; cach = get_cach_wl_heur_init S; lbd = get_lbd_wl_heur_init S;
j = get_literals_to_update_wl_init S
in
(unbdd ⟶ ¬failed) ∧
((unbdd ∨ ¬failed) ⟶
(valid_arena N' N (set vdom) ∧
set_mset
(all_lits_of_mm
({#mset (fst x). x ∈# ran_m N#} + NE+NEk + UE + UEk + NS + US + N0 + U0)) ⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜) ∧
mset vdom = dom_m N ∧ ivdom = vdom)) ∧
(M', M) ∈ trail_pol 𝒜 ∧
(D', D) ∈ option_lookup_clause_rel 𝒜 ∧
j ≤ length M ∧
Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
vm ∈ bump_heur_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 ∧
clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount ∧
(mark, {#}) ∈ lookup_clause_rel 𝒜
}›
definition twl_st_heur_parsing
:: ‹nat multiset ⇒ bool ⇒ (twl_st_wl_heur_init × (nat twl_st_wl × nat clauses)) set›
where
[unfolded Let_def]: ‹twl_st_heur_parsing 𝒜 unbdd =
{(S,
((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0,Q, W), OC)).
let M' = get_trail_init_wl_heur S; N' = get_clauses_wl_heur_init S; failed = is_failed_heur_init S;
vdom = get_vdom_heur_init S; ivdom = get_ivdom_heur_init S; D' = get_conflict_wl_heur_init S; vm = get_vmtf_wl_heur_init S;
mark = get_mark_wl_heur_init S; lcount = get_learned_count_init S; W' = get_watchlist_wl_heur_init S;
φ = get_phases_wl_heur_init S; cach = get_cach_wl_heur_init S; lbd = get_lbd_wl_heur_init S;
j = get_literals_to_update_wl_init S
in
(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 ∈ bump_heur_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+NEk) + (UE+UEk) + NS + US + N0 + U0)) ⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜) ∧
(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜) ∧
isasat_input_bounded 𝒜 ∧
distinct vdom ∧
ivdom = vdom ∧
clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount ∧
(mark, {#}) ∈ lookup_clause_rel 𝒜))
}›
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 =
{(S,
(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0,Q)).
let M' = get_trail_init_wl_heur S; N' = get_clauses_wl_heur_init S; failed = is_failed_heur_init S;
vdom = get_vdom_heur_init S; ivdom = get_ivdom_heur_init S; D' = get_conflict_wl_heur_init S; vm = get_vmtf_wl_heur_init S;
mark = get_mark_wl_heur_init S; lcount = get_learned_count_init S; W' = get_watchlist_wl_heur_init S;
φ = get_phases_wl_heur_init S; cach = get_cach_wl_heur_init S; lbd = get_lbd_wl_heur_init S;
j = get_literals_to_update_wl_init S
in
(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 ∈ bump_heur_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+NEk) + (UE+UEk) + NS + US + N0 + U0))
⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜) ∧
(W', empty_watched 𝒜) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜) ∧
isasat_input_bounded 𝒜 ∧
distinct vdom ∧ ivdom = vdom ∧
clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount ∧
(mark, {#}) ∈ lookup_clause_rel 𝒜
}›
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 =
{(S,
((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0,Q), OC)).
let M' = get_trail_init_wl_heur S; N' = get_clauses_wl_heur_init S; failed = is_failed_heur_init S;
vdom = get_vdom_heur_init S; ivdom = get_ivdom_heur_init S; D' = get_conflict_wl_heur_init S; vm = get_vmtf_wl_heur_init S;
mark = get_mark_wl_heur_init S; lcount = get_learned_count_init S; W' = get_watchlist_wl_heur_init S;
φ = get_phases_wl_heur_init S; cach = get_cach_wl_heur_init S; lbd = get_lbd_wl_heur_init S;
j = get_literals_to_update_wl_init S
in
(unbdd ⟶ ¬failed) ∧
((unbdd ∨ ¬failed) ⟶
(valid_arena N' N (set vdom) ∧ set_mset (dom_m N) ⊆ set vdom) ∧ ivdom = vdom) ∧ (M', M) ∈ trail_pol 𝒜 ∧
(D', D) ∈ option_lookup_clause_rel 𝒜 ∧
j ≤ length M ∧
Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
vm ∈ bump_heur_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+NEk) + (UE+UEk) + NS + US + N0 + U0))
⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜) ∧
(W', empty_watched 𝒜) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜) ∧
isasat_input_bounded 𝒜 ∧
distinct vdom ∧
clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount ∧
(mark, {#}) ∈ lookup_clause_rel 𝒜
}›
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 =
{(S,
(M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W)).
let M' = get_trail_init_wl_heur S; N' = get_clauses_wl_heur_init S; failed = is_failed_heur_init S;
vdom = get_vdom_heur_init S; ivdom = get_ivdom_heur_init S; D' = get_conflict_wl_heur_init S; vm = get_vmtf_wl_heur_init S;
mark = get_mark_wl_heur_init S; lcount = get_learned_count_init S; W' = get_watchlist_wl_heur_init S;
φ = get_phases_wl_heur_init S; cach = get_cach_wl_heur_init S; lbd = get_lbd_wl_heur_init S;
j = get_literals_to_update_wl_init S
in
(unbdd ⟶ ¬failed) ∧
((unbdd ∨ ¬failed) ⟶
((M', M) ∈ trail_pol (all_atms N ((NE+NEk) + (UE+UEk) + NS + US + N0 + U0)) ∧
set_mset (dom_m N) ⊆ set vdom ∧
valid_arena N' N (set vdom) ∧ ivdom=vdom)) ∧
(D', D) ∈ option_lookup_clause_rel (all_atms N ((NE+NEk) + (UE+UEk) + NS + US + N0 + U0)) ∧
j ≤ length M ∧
Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
vm ∈ bump_heur_init (all_atms N ((NE+NEk) + (UE+UEk) + NS + US + N0 + U0)) M ∧
phase_saving (all_atms N ((NE+NEk) + (UE+UEk) + NS + US + N0 + U0)) φ ∧
no_dup M ∧
cach_refinement_empty (all_atms N ((NE+NEk) + (UE+UEk) + NS + US + N0 + U0)) cach ∧
vdom_m (all_atms N ((NE+NEk) + (UE+UEk) + NS + US + N0 + U0)) W N ⊆ set vdom ∧
set_mset (all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE+NEk) + (UE+UEk) + NS + US + N0 + U0))
⊆ set_mset (ℒ⇩a⇩l⇩l (all_atms N ((NE+NEk) + (UE+UEk) + NS + US + N0 + U0))) ∧
(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms N ((NE+NEk) + (UE+UEk) + NS + US + N0 + U0))) ∧
isasat_input_bounded (all_atms N ((NE+NEk) + (UE+UEk) + NS + US + N0 + U0)) ∧
distinct vdom ∧
clss_size_corr N NE UE NEk UEk NS US N0 U0 lcount ∧
(mark, {#}) ∈ lookup_clause_rel (all_atms N ((NE+NEk) + (UE+UEk) + NS + US + N0 + U0))
}›
subsection ‹Parsing›
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
:: ‹bool ⇒ nat literal ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹propagate_unit_cls_heur = (λunbdd L S.
do {
M ← cons_trail_Propagated_tr L 0 (get_trail_init_wl_heur S);
RETURN (set_trail_init_wl_heur M S)
})›
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, N0, U0,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, N0, U0,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 unbdd), 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!: bump_heur_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
:: ‹bool ⇒ nat clause_l ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹already_propagated_unit_cls_heur = (λunbdd L S.
RETURN S)›
lemma already_propagated_unit_cls_heur_already_propagated_unit_cls:
‹(uncurry (already_propagated_unit_cls_heur unbdd), 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, NEk, UEk, NS, US, N0, U0,Q), OC).
((M, N, set_conflict_unit L D, add_mset {#L#} NE, UE, NEk, UEk, NS, US, N0, U0,{#}), OC))›
definition conflict_propagated_unit_cls_heur
:: ‹bool ⇒ nat literal ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹conflict_propagated_unit_cls_heur = (λunbdd L S.
do {
ASSERT(atm_of L < length (snd (snd (get_conflict_wl_heur_init S))));
D ← set_conflict_unit_heur L (get_conflict_wl_heur_init S);
ASSERT(isa_length_trail_pre (get_trail_init_wl_heur S));
let j = isa_length_trail (get_trail_init_wl_heur S);
RETURN (set_literals_to_update_wl_init j (set_conflict_wl_heur_init D S))
})›
definition conflict_propagated_unit_cls_heur_b :: ‹_› where
‹conflict_propagated_unit_cls_heur_b = conflict_propagated_unit_cls_heur False›
lemma conflict_propagated_unit_cls_heur_conflict_propagated_unit_cls:
‹(uncurry (conflict_propagated_unit_cls_heur unbdd), 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, NEk, UEk, NS, US, N0, U0,Q), OC). do {
D ← RETURN (set_conflict_unit L D);
RETURN ((M, N, Some {#L#}, add_mset {#L#} NE, UE, NEk, UEk, NS, US, N0, U0,{#}), 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 lhs_step_If)
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 S. do {
let C = C;
ASSERT(length C ≤ unat32_max + 2);
ASSERT(length C ≥ 2);
let N = get_clauses_wl_heur_init S;
let failed = is_failed_heur_init S;
if unbdd ∨ (length N ≤ snat64_max - length C - 5 ∧ ¬failed)
then do {
let vdom = get_vdom_heur_init S;
let ivdom = get_ivdom_heur_init S;
ASSERT(length vdom ≤ length N ∧ vdom = ivdom);
(N, i) ← fm_add_new True C N;
let vdom = vdom @ [i];
let ivdom = ivdom @ [i];
RETURN (set_clauses_wl_heur_init N (set_vdom_heur_init vdom (set_ivdom_heur_init ivdom S)))
} else RETURN (set_failed_heur_init True S)})›
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 N0 U0 NEk UEk :: ‹nat clauses› and
M :: ‹(nat,nat) ann_lits› and
a b c d e1 e2 e3 f m p q r s t u v w x y ua ub z 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 :: ‹bump_heuristics_option_fst_As› and
clvls :: nat and
cach :: conflict_min_cach_l and
lbd :: lbd and
ivdom vdom :: vdom and
failed :: bool and
lcount :: clss_size and
φ :: phase_saver and
mark :: ‹lookup_clause_rel›
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, e1)›
‹e1 = (NEk, e2)›
‹e2 = (UEk, e3)›
‹e3 = (NS, f)›
‹f = (US, ua)›
‹ua = (N0, ub)›
‹ub = (U0, Q)›
‹CT = (C', T)›
begin
lemma add_init_pre1: ‹length C' ≤ unat32_max + 2›
using pre clss_size_unat32_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
‹(get_trail_init_wl_heur T, M) ∈ trail_pol 𝒜› and
valid: ‹valid_arena (get_clauses_wl_heur_init T) N (set (get_vdom_heur_init T))› and
‹(get_conflict_wl_heur_init T, D) ∈ option_lookup_clause_rel 𝒜› and
‹get_literals_to_update_wl_init T ≤ length M› and
Q: ‹Q = {#- lit_of x. x ∈# mset (drop (get_literals_to_update_wl_init T) (rev M))#}› and
‹get_vmtf_wl_heur_init T ∈ bump_heur_init 𝒜 M› and
‹phase_saving 𝒜 (get_phases_wl_heur_init T)› and
‹no_dup M› and
‹cach_refinement_empty 𝒜 (get_cach_wl_heur_init T)› and
vdom: ‹mset (get_vdom_heur_init T) = dom_m N› and
ivdom: ‹(get_ivdom_heur_init T) = (get_vdom_heur_init T)› and
var_incl:
‹set_mset (all_lits_of_mm ({#mset (fst x). x ∈# ran_m N#} + (NE+NEk) + NS + (UE+UEk) + US + N0 + U0))
⊆ set_mset (ℒ⇩a⇩l⇩l 𝒜)› and
watched: ‹(get_watchlist_wl_heur_init T, empty_watched 𝒜) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜)› and
bounded: ‹isasat_input_bounded 𝒜› and
dcount: ‹clss_size_corr N NE UE NEk UEk NS US N0 U0 (get_learned_count_init T)›
if ‹¬(is_failed_heur_init T) ∨ unbdd›
using that xy unfolding st twl_st_heur_parsing_no_WL_def
by (auto simp: ac_simps)
lemma init_fm_add_new:
‹¬is_failed_heur_init T ∨ unbdd ⟹ fm_add_new True C' (get_clauses_wl_heur_init T)
≤ ⇓ {((arena, i), (N'', i')). valid_arena arena N'' (insert i (set (get_vdom_heur_init T))) ∧ i = i' ∧
i ∉# dom_m N ∧ i = length (get_clauses_wl_heur_init T) + header_size C ∧
i ∉ set (get_vdom_heur_init T)}
(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 (get_vdom_heur_init T))) ∧ i = i' ∧
i ∉# dom_m N ∧ i = length (get_clauses_wl_heur_init T) + header_size C ∧
i ∉ set (get_vdom_heur_init T)}› 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 ‹((set_clauses_wl_heur_init nN' (set_vdom_heur_init (get_vdom_heur_init T @ [k']) (set_ivdom_heur_init (get_ivdom_heur_init T @ [k']) T))),
(M, nN, D, NE, UE, NEk, UEk, NS, US, N0, U0, 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 learned_clss_l_fmupd_if_in:
assumes ‹C' ∈# dom_m new›
shows
‹learned_clss_l (fmupd C' D new) = (if ¬snd D then add_mset D else id)(if ¬irred new C' then (remove1_mset (the (fmlookup new C')) (learned_clss_l new)) else learned_clss_l new)›
proof -
define new' where ‹new' = fmdrop C' new›
define E where ‹E = the (fmlookup new C')›
then have new: ‹new = fmupd C' E new'› and [simp]: ‹C' ∉# dom_m new'›
using assms distinct_mset_dom[of new]
by (auto simp: fmdrop_fmupd new'_def intro!: fmlookup_inject[THEN iffD1] ext
dest: multi_member_split)
show ?thesis
unfolding new
by (auto simp: learned_clss_l_mapsto_upd_irrel learned_clss_l_fmupd_if
dest!: multi_member_split)
qed
lemma clss_size_new_irredI:
‹ clss_size_corr x1c x1e x1f x1g x1h x2h x2i x2j x2k (au, av, aw, ax, be) ⟹
clss_size_corr (fmupd b (x1, True) x1c) x1e x1f x1g x1h x2h x2i x2j x2k (au, av, aw, ax, be) ⟷
b ∉#dom_m x1c ∨ irred x1c b
›
apply (cases ‹b ∈#dom_m x1c›)
apply (rule iffI)
apply (auto simp: clss_size_corr_def clss_size_def
clss_size_def learned_clss_l_fmupd_if_in size_remove1_mset_If
learned_clss_l_mapsto_upd_notin_irrelev dest: learned_clss_l_mapsto_upd learned_clss_l_update
split: if_splits)
using learned_clss_l_mapsto_upd learned_clss_l_update by fastforce
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 [iff]: ‹(∀b. b = 0 ∨ b ∈# dom_m x1c ∨ b ∈# dom_m x1c ∧ ¬ irred x1c b) ⟷ False› for x1c
apply (intro iffI impI, auto)
apply (drule spec[of _ ‹Max_dom x1c + 1›])
by (auto simp: ge_Max_dom_notin_dom_m)
have [iff]: ‹∃b>0. b ∉# dom_m x1c ∧ (b ∈# dom_m x1c ⟶ irred x1c b)› for x1c x1
by (rule exI[of _ ‹Max_dom x1c + 1›])
(auto simp: ge_Max_dom_notin_dom_m)
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, NEk, UEk, NS, US, N0, U0, 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, NEk, UEk, NS, US, N0, U0, 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)
subgoal by (auto simp: twl_st_heur_parsing_no_WL_def)
apply (rule init_fm_add_new)
apply assumption+
subgoal by auto
subgoal by (rule add_init_cls_final_rel)
subgoal for x y x1 x2 x1a x1b x2a x1c x2b x1d x2c x1e x2d x1f x2e x1g x2f x1h x2g
x2h x1i x2i x1j x2j x1k x2k x1l x2l x1m x2m
unfolding RES_RES2_RETURN_RES RETURN_def
apply simp
unfolding RETURN_def apply (rule RES_refine)
apply (auto simp: twl_st_heur_parsing_no_WL_def clss_size_new_irredI RETURN_def intro!: RES_refine)
apply (meson ‹⋀x1c. (∀b. b = 0 ∨ b ∈# x1c) = False› clss_size_corr_simp(4))
apply (metis (no_types, opaque_lifting) ‹⋀x1c. ∃b>0. b ∉# x1c› clss_size_corr_simp(4))
apply (meson ‹⋀x1c. (∀b. b = 0 ∨ b ∈# x1c) = False› clss_size_corr_simp(4))
apply (metis (no_types, opaque_lifting) ‹⋀x1c. ∃b>0. b ∉# x1c› clss_size_corr_simp(4))
done
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, NEk, UEk, NS, US, N0, U0, Q), OC).
((M, N, D, add_mset {#L#} NE, UE, NEk, UEk, NS, US, N0, U0, {#}), OC))›
definition already_propagated_unit_cls_conflict_heur
:: ‹bool ⇒ nat literal ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹already_propagated_unit_cls_conflict_heur = (λunbdd L S. do {
ASSERT (isa_length_trail_pre (get_trail_init_wl_heur S));
RETURN (set_literals_to_update_wl_init (isa_length_trail (get_trail_init_wl_heur S)) S)
})›
lemma already_propagated_unit_cls_conflict_heur_already_propagated_unit_cls_conflict:
‹(uncurry (already_propagated_unit_cls_conflict_heur unbdd),
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 = (λS. do {
let M = get_trail_init_wl_heur S;
let (_, (n, xs)) = get_conflict_wl_heur_init S;
ASSERT(isa_length_trail_pre M);
let j = isa_length_trail M;
RETURN (set_conflict_wl_heur_init ((False, (n, xs))) (set_literals_to_update_wl_init j S))
})›
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›
unfolding set_empty_clause_as_conflict_heur_def add_empty_conflict_init_wl_def
twl_st_heur_parsing_no_WL_def Let_def
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]
all_lits_of_mm_add_mset all_atms_st_def clss_size_def
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 = (λ _ S. RETURN S)›
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 -) add_tautology_to_clauses
:: ‹nat clause_l ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹add_tautology_to_clauses = (λ _ S. RETURN S)›
lemma add_tautology_to_clauses_add_tautology_init_wl:
‹(uncurry add_tautology_to_clauses, uncurry (RETURN oo add_to_tautology_init_wl)) ∈
[λ(C, _). literals_are_in_ℒ⇩i⇩n 𝒜 (mset C) ]⇩f
⟨Id⟩list_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: add_to_other_init.simps all_lits_of_m_remdups_mset
add_to_tautology_init_wl.simps add_tautology_to_clauses_def
twl_st_heur_parsing_no_WL_def all_lits_of_mm_add_mset
literals_are_in_ℒ⇩i⇩n_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 = (λS. fst (get_conflict_wl_heur_init S))›
definition pre_simplify_clause_lookup_st
:: ‹nat clause_l ⇒ nat clause_l ⇒ twl_st_wl_heur_init ⇒ (bool × _ × twl_st_wl_heur_init) nres›
where
‹pre_simplify_clause_lookup_st = (λC E S. do {
(tauto, C, mark) ← pre_simplify_clause_lookup C E (get_mark_wl_heur_init S);
RETURN (tauto, C, (set_mark_wl_heur_init mark S))
})›
definition init_dt_step_wl_heur
:: ‹bool ⇒ nat clause_l ⇒ twl_st_wl_heur_init × nat clause_l ⇒
(twl_st_wl_heur_init × nat clause_l) nres›
where
‹init_dt_step_wl_heur unbdd C⇩0 = (λ(S, C). do {
if get_conflict_wl_is_None_heur_init S
then do {
(tauto, C, S) ← pre_simplify_clause_lookup_st C⇩0 C S;
if tauto
then do {T ← add_tautology_to_clauses C⇩0 S; RETURN (T, take 0 C)}
else if is_Nil C
then do {T ← set_empty_clause_as_conflict_heur S; RETURN (T, take 0 C)}
else if list_length_1 C
then do {
ASSERT (C ≠ []);
let L = C ! 0;
ASSERT(polarity_pol_pre (get_trail_init_wl_heur S) L);
let val_L = polarity_pol (get_trail_init_wl_heur S) L;
if val_L = None
then do {T ← propagate_unit_cls_heur unbdd L S; RETURN (T, take 0 C)}
else
if val_L = Some True
then do {T ← already_propagated_unit_cls_heur unbdd C S; RETURN (T, take 0 C)}
else do {T ← conflict_propagated_unit_cls_heur unbdd L S; RETURN (T, take 0 C)}
}
else do {
ASSERT(length C ≥ 2);
T ← add_init_cls_heur unbdd C S;
RETURN (T, take 0 C)
}
}
else do {T ← add_clause_to_others_heur C⇩0 S; RETURN (T, take 0 C)}
})›
lemma init_dt_step_wl_heur_alt_def:
‹init_dt_step_wl_heur unbdd C⇩0 = (λ(S,D). do {
if get_conflict_wl_is_None_heur_init S
then do {
(tauto, C, S) ← pre_simplify_clause_lookup_st C⇩0 D S;
if tauto
then do {T ← add_tautology_to_clauses C⇩0 S; RETURN (T, take 0 C)}
else do {
C ← RETURN C;
if is_Nil C
then do {T ← set_empty_clause_as_conflict_heur S; RETURN (T, take 0 C)}
else if list_length_1 C
then do {
ASSERT (C ≠ []);
let L = C ! 0;
ASSERT(polarity_pol_pre (get_trail_init_wl_heur S) L);
let val_L = polarity_pol (get_trail_init_wl_heur S) L;
if val_L = None
then do {T ← propagate_unit_cls_heur unbdd L S; RETURN (T, take 0 C)}
else
if val_L = Some True
then do {T ← already_propagated_unit_cls_heur unbdd C S; RETURN (T, take 0 C)}
else do {T ← conflict_propagated_unit_cls_heur unbdd L S; RETURN (T, take 0 C)}
}
else do {
ASSERT(length C ≥ 2);
T ← add_init_cls_heur unbdd C S;
RETURN (T, take 0 C)
}
} }
else do {T ← add_clause_to_others_heur C⇩0 S; RETURN (T, take 0 C)}
})›
unfolding nres_monad1 init_dt_step_wl_heur_def by auto
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_init_wl_heur 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›
definition pre_simplify_clause_lookup_st_rel where
‹pre_simplify_clause_lookup_st_rel 𝒜 unbdd C T = {((tauto, C', S'), tauto').
tauto' = tauto ∧
(tauto ⟷ tautology (mset C)) ∧
(¬tauto ⟶ remdups_mset (mset C) = mset C') ∧
(S', T) ∈ twl_st_heur_parsing_no_WL 𝒜 unbdd}›
lemma pre_simplify_clause_lookup_st_rel_alt_def:
‹pre_simplify_clause_lookup_st_rel 𝒜 unbdd C T = {((tauto, C', S'), tauto').
tauto' = tauto ∧
(tauto ⟷ tautology (mset C)) ∧
(¬tauto ⟶ remdups_mset (mset C) = mset C' ∧ distinct C') ∧
(S', T) ∈ twl_st_heur_parsing_no_WL 𝒜 unbdd}›
by (auto simp: pre_simplify_clause_lookup_st_rel_def eq_commute[of _ ‹mset _›]
simp del: distinct_mset_mset_distinct
simp flip: distinct_mset_mset_distinct)
lemma pre_simplify_clause_lookup_st_remdups_clause:
fixes D :: ‹nat clause_l›
assumes ‹(C, C') ∈ Id› ‹(S, T) ∈ twl_st_heur_parsing_no_WL 𝒜 unbdd›
‹literals_are_in_ℒ⇩i⇩n 𝒜 (mset C)› ‹isasat_input_bounded 𝒜› and [simp]: ‹D = []›
shows
‹pre_simplify_clause_lookup_st C D S ≤ ⇓ (pre_simplify_clause_lookup_st_rel 𝒜 unbdd C T)
(RETURN (tautology (mset C')))›
proof -
have ‹mset (remdups C') = remdups_mset (mset C')›
by auto
then have [iff]: ‹(∀x. mset x ≠ remdups_mset (mset C')) ⟷ False›
by blast
show ?thesis
using assms
unfolding pre_simplify_clause_lookup_st_def remdups_clause_def conc_fun_RES
RETURN_def
apply (cases S)
apply clarify
apply (subst bind_rule_complete_RES)
apply (refine_vcg bind_rule_complete_RES
pre_simplify_clause_lookup_pre_simplify_clause[of _ 𝒜, THEN order_trans])
subgoal by (auto simp: twl_st_heur_parsing_no_WL_def)
subgoal by (auto simp: literals_are_in_ℒ⇩i⇩n_alt_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
subgoal by (auto simp: twl_st_heur_parsing_no_WL_def)
subgoal
by (rule order_trans, rule ref_two_step', rule pre_simplify_clause_spec)
(auto simp: pre_simplify_clause_spec_def conc_fun_RES
twl_st_heur_parsing_no_WL_def pre_simplify_clause_lookup_st_rel_def)
done
qed
definition RETURN2 where ‹RETURN2 = RETURN›
lemma init_dt_step_wl_alt_def:
‹init_dt_step_wl C S =
(case get_conflict_init_wl S of
None ⇒
let B = tautology (mset C) in
if B
then do {T ← RETURN (add_to_tautology_init_wl C S); RETURN T}
else
do {
C ← remdups_clause C;
if length C = 0
then do {T ← RETURN (add_empty_conflict_init_wl S); RETURN T}
else if length C = 1
then
let L = hd C in
if undefined_lit (get_trail_init_wl S) L
then do {T ← propagate_unit_init_wl L S; RETURN T}
else if L ∈ lits_of_l (get_trail_init_wl S)
then do {T ← RETURN (already_propagated_unit_init_wl (mset C) S); RETURN T}
else do {T ← RETURN (set_conflict_init_wl L S); RETURN T}
else do {T ← add_to_clauses_init_wl C S; RETURN T}
}
| Some D ⇒
do {T ← RETURN (add_to_other_init C S); RETURN T})›
unfolding init_dt_step_wl_def Let_def nres_monad1 while.imonad2 RETURN2_def by auto
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)]⇩f
Id ×⇩f {((S, C), T). C = [] ∧ (S,T)∈ twl_st_heur_parsing_no_WL 𝒜 unbdd} →
⟨{((S, C), T). C = [] ∧ (S,T)∈twl_st_heur_parsing_no_WL 𝒜 unbdd}⟩ nres_rel›
proof -
have remdups: ‹
(x', tautology (mset x1))
∈ pre_simplify_clause_lookup_st_rel 𝒜 unbdd x1a T ⟹
x2b = (x1c, x2c) ⟹
x' = (x1b, x2b) ⟹
¬ x1b ⟹
¬ tautology (mset x1) ⟹ (x1a, x1) ∈ Id ⟹
RETURN x1c ≤ ⇓ {(a,b). a = b ∧ set b ⊆ set x1 ∧ x1c = b} (remdups_clause x1)›
for x1 x1a x1c x2 x2b x2c x' x1b T
apply (auto simp: remdups_clause_def pre_simplify_clause_lookup_st_rel_def
intro!: RETURN_RES_refine)
by (metis set_mset_mset set_mset_remdups_mset)
show ?thesis
supply [[goals_limit=1]]
unfolding init_dt_step_wl_alt_def uncurry_def
option.case_eq_if get_conflict_wl_is_None_init_alt_def[symmetric]
apply (subst init_dt_step_wl_heur_alt_def)
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[where 𝒜 = 𝒜 and unbdd = unbdd,
THEN fref_to_Down, unfolded comp_def]
propagate_unit_cls_heur_propagate_unit_cls[where 𝒜 = 𝒜 and unbdd = unbdd,THEN fref_to_Down_curry, unfolded comp_def]
already_propagated_unit_cls_heur_already_propagated_unit_cls[where 𝒜 = 𝒜 and unbdd = unbdd,THEN fref_to_Down_curry,
unfolded comp_def]
conflict_propagated_unit_cls_heur_conflict_propagated_unit_cls[where 𝒜 = 𝒜 and unbdd = unbdd,THEN fref_to_Down_curry,
unfolded comp_def]
add_init_cls_heur_add_init_cls[where 𝒜 = 𝒜 and unbdd = unbdd, THEN fref_to_Down_curry,
unfolded comp_def]
add_clause_to_others_heur_add_clause_to_others[where 𝒜 = 𝒜 and unbdd = unbdd,THEN fref_to_Down_curry,
unfolded comp_def]
pre_simplify_clause_lookup_st_remdups_clause[where 𝒜 = 𝒜 and unbdd = unbdd]
add_tautology_to_clauses_add_tautology_init_wl[where 𝒜 = 𝒜 and unbdd = unbdd,
THEN fref_to_Down_curry, unfolded comp_def]
remdups)
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)
apply auto[]
subgoal by simp
subgoal by (clarsimp simp add: twl_st_heur_parsing_no_WL_def)
subgoal by simp
subgoal by (simp only: prod.case in_pair_collect_simp pre_simplify_clause_lookup_st_rel_def)
subgoal by simp
subgoal by (auto simp: pre_simplify_clause_lookup_st_rel_def)
subgoal by auto
apply assumption
apply assumption
apply assumption
apply assumption
subgoal by auto
subgoal by (auto split: list.splits)
subgoal by (simp add: get_conflict_wl_is_None_init_alt_def)
subgoal by (auto simp: pre_simplify_clause_lookup_st_rel_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for x y x1 T x1a x2a x1b x2b x' x1c x1d x2d S'' D Ca
by (rule polarity_pol_pre[of ‹get_trail_init_wl_heur S''› ‹get_trail_init_wl T› 𝒜 ‹D!0›])
(auto simp: pre_simplify_clause_lookup_st_rel_def twl_st_heur_parsing_no_WL
literals_are_in_ℒ⇩i⇩n_add_mset dest!: split_list
split: list.splits)
subgoal for x y x1 T x1a x2a x1b x2b x' x1c x1d x2d S'' D Ca
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 D›])
(auto simp: pre_simplify_clause_lookup_st_rel_def twl_st_heur_parsing_no_WL
polarity_pol_polarity[of 𝒜, unfolded option_rel_id_simp, THEN fref_to_Down_unRET_uncurry_Id]
polarity_def
literals_are_in_ℒ⇩i⇩n_add_mset dest: split_list split: list.splits)
subgoal by auto
subgoal by (auto simp: pre_simplify_clause_lookup_st_rel_def twl_st_heur_parsing_no_WL
polarity_pol_polarity[of 𝒜, unfolded option_rel_id_simp, THEN fref_to_Down_unRET_uncurry_Id]
polarity_def
literals_are_in_ℒ⇩i⇩n_add_mset dest: split_list split: list.splits)
subgoal by (auto split: list.splits simp: pre_simplify_clause_lookup_st_rel_def)
subgoal by auto
subgoal for x y x1 T x1a x2a x1b x2b x' x1c x1d x2d S'' D Ca
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 D›])
(auto simp: pre_simplify_clause_lookup_st_rel_def twl_st_heur_parsing_no_WL
polarity_pol_polarity[of 𝒜, unfolded option_rel_id_simp, THEN fref_to_Down_unRET_uncurry_Id]
polarity_def
literals_are_in_ℒ⇩i⇩n_add_mset dest: split_list split: list.splits)
subgoal by (fastforce simp: literals_are_in_ℒ⇩i⇩n_alt_def)
subgoal by (auto simp: pre_simplify_clause_lookup_st_rel_def list_mset_rel_def br_def)
subgoal by auto
subgoal by (auto simp: literals_are_in_ℒ⇩i⇩n_alt_def
in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
split: list.splits)
subgoal by (simp add: get_conflict_wl_is_None_init_alt_def)
subgoal by (simp add: hd_conv_nth pre_simplify_clause_lookup_st_rel_def)
subgoal
by (auto split: list.splits)
subgoal
by (auto split: list.splits)
subgoal by auto
subgoal by (fastforce simp: literals_are_in_ℒ⇩i⇩n_alt_def)
subgoal by (auto simp: pre_simplify_clause_lookup_st_rel_alt_def)
subgoal by (simp add: pre_simplify_clause_lookup_st_rel_def)
subgoal by (simp add: pre_simplify_clause_lookup_st_rel_def)
subgoal by fast
subgoal by (simp add: pre_simplify_clause_lookup_st_rel_def)
subgoal by auto
done
qed
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 × nat clause_l ⇒ (twl_st_wl_heur_init × nat clause_l) 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 CS S = do { (S, _) ← init_dt_wl_heur True CS (S, []); RETURN S}›
definition propagate_unit_cls_heur_b :: ‹nat literal ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹propagate_unit_cls_heur_b = propagate_unit_cls_heur False›
definition already_propagated_unit_cls_conflict_heur_b :: ‹nat literal ⇒ twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres› where
‹already_propagated_unit_cls_conflict_heur_b = already_propagated_unit_cls_conflict_heur False›
definition init_dt_step_wl_heur_b :: ‹nat clause_l ⇒ twl_st_wl_heur_init × nat clause_l ⇒
(twl_st_wl_heur_init × nat clause_l) 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 CS S = do { (S, _) ← init_dt_wl_heur False CS (S, []); RETURN S}›
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 < unat32_max ∧
(∀s∈set xs. s ≤ unat64_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 < unat32_max ∧
(∀s∈set xs. s ≤ unat64_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 ≤ unat32_max ⟹ L < init_next_size L›
by (auto simp: init_next_size_def unat32_max_def)
definition add_to_atms_ext where
‹add_to_atms_ext = (λi (xs, n, atms). do {
ASSERT(i ≤ unat32_max div 2);
ASSERT(length xs ≤ unat32_max);
ASSERT(length atms ≤ Suc n);
let n = max i n;
(if i < length_uint32_nat xs then do {
ASSERT(xs!i ≤ unat64_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 ≤ unat32_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 ≤ unat32_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: unat64_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: unat32_max_def)
subgoal by (auto simp: unat32_max_def)
subgoal by (auto simp: unat32_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 unat32_max_def)
subgoal
unfolding bitOR_1_if_mod_2_nat
by (auto simp: unat64_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
:: ‹'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›
:: ‹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 ≤ unat32_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 C 𝒜⇩i⇩n = 𝒜⇩i⇩n ∪ atm_of ` set C›
by (induction C) (auto simp: extract_atms_cls_def fild_insert_insert_swap)
lemma :
‹(uncurry extract_atms_cls_i, uncurry (RETURN oo extract_atms_cls))
∈ [λ(C, 𝒜⇩i⇩n). ∀L∈set C. nat_of_lit L ≤ unat32_max]⇩f
⟨Id⟩list_rel ×⇩f Id → ⟨Id⟩nres_rel›
proof -
have H1: ‹(x1a, x1) ∈ ⟨{(L, L'). L = L' ∧ nat_of_lit L ≤ unat32_max}⟩list_rel›
if
‹case y of (C, 𝒜⇩i⇩n) ⇒ ∀L∈set C. nat_of_lit L ≤ unat32_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 ≤ unat32_max ⟹ atm_of xa ≤ unat32_max div 2› for xa
by (cases xa) (auto simp: unat32_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
:: ‹'a clause_l list ⇒ 'a set ⇒ 'a set› where
‹extract_atms_clss N 𝒜⇩i⇩n = fold extract_atms_cls N 𝒜⇩i⇩n›
:: ‹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 :
‹(uncurry extract_atms_clss_i, uncurry (RETURN oo extract_atms_clss))
∈ [λ(N, 𝒜⇩i⇩n). ∀C∈set N. ∀L∈set C. nat_of_lit L ≤ unat32_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 ≤ unat32_max)}⟩list_rel›
if
‹case y of (N, 𝒜⇩i⇩n) ⇒ ∀C∈set N. ∀L∈set C. nat_of_lit L ≤ unat32_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 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 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 [simp]: ‹finite (extract_atms_clss CS' {})› for CS'
by (auto simp: extract_atms_clss_alt_def)
where
‹op_extract_list_empty = {}›
where
‹extract_atms_clss_imp_empty_rel = (RETURN (replicate 1024 0, 0, []))›
lemma :
‹(λ_. 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 unat32_max_def
isasat_atms_ext_rel_def init_valid_rep_def extract_atms_clss_imp_empty_rel_def
del: replicate_numeral)
lemma [simp]:
‹extract_atms_cls [] 𝒜⇩i⇩n = 𝒜⇩i⇩n›
unfolding extract_atms_cls_def fold.simps by simp
lemma [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 𝒜);
mark ← SPEC(λD. (D, {#}) ∈ lookup_clause_rel 𝒜);
W ← SPEC (λW. (W, empty_watched 𝒜) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜));
vm ← RES (bump_heur_init 𝒜 []);
φ ← SPEC (phase_saving 𝒜);
cach ← SPEC (cach_refinement_empty 𝒜);
let lbd = empty_lbd;
let vdom = [];
let ivdom = [];
let lcount = (0,0,0,0,0);
RETURN (Tuple15 M [] D 0 W vm φ 0 cach lbd vdom ivdom False lcount mark)}›
definition init_state_wl_heur_fast where
‹init_state_wl_heur_fast = init_state_wl_heur›
lemma clss_size_empty [simp]: ‹clss_size fmempty {#} {#} {#} {#} {#} {#} {#} {#} = (0, 0 ,0, 0, 0)›
by (auto simp: clss_size_def)
lemma clss_size_corr_empty [simp]: ‹clss_size_corr fmempty {#} {#} {#} {#} {#} {#} {#} {#} (0, 0 ,0, 0, 0)›
by (auto simp: clss_size_corr_def)
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))]⇩f
⟨Id⟩list_rel ×⇩f {((S, C), T). C = [] ∧ (S,T) ∈ twl_st_heur_parsing_no_WL 𝒜 unbdd} →
⟨{((S, C), T). C = [] ∧ (S,T) ∈ 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)) ⟹
(x1a, x1) ∈ ⟨Id⟩list_rel ⟹
(x1a, x1) ∈ ⟨{(C, C'). C = C' ∧ literals_are_in_ℒ⇩i⇩n 𝒜 (mset 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
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 ≤ snat64_max) ∧ length (get_clauses_wl_heur_init S) ≤ snat64_max)›
definition rewatch_heur_st_init
:: ‹twl_st_wl_heur_init ⇒ twl_st_wl_heur_init nres›
where
‹rewatch_heur_st_init = (λS. do {
ASSERT(length ((get_vdom_heur_init S)) ≤ length (get_clauses_wl_heur_init S));
W ← rewatch_heur ((get_vdom_heur_init S)) (get_clauses_wl_heur_init S) (get_watchlist_wl_heur_init S);
RETURN (set_watchlist_wl_heur_init W S)
})›
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, C) ← init_dt_wl_heur unb CS (S, []);
ASSERT(¬is_failed_heur_init S);
rewatch_heur_st_init 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)›
‹(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 (get_clauses_wl_heur_init x) x1b (set (get_vdom_heur_init x))›
‹set (get_vdom_heur_init x) ⊆ set (get_vdom_heur_init x)› ‹set_mset (dom_m x1b) ⊆ set (get_vdom_heur_init x)›
‹distinct (get_vdom_heur_init x)› ‹(get_watchlist_wl_heur_init x, λ_. []) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜)›
if
xx': ‹(xa, x') ∈ {((S, C), T). C = [] ∧ (S,T) ∈ twl_st_heur_parsing_no_WL 𝒜 True}› and
st: ‹xa = (x, a)›
‹x2c = (x1e, x2d)›
‹x2b = (x1d, x2c)›
‹x2a = (x1c, x2b)›
‹x2 = (x1b, x2a)›
‹x1 = (x1a, x2)›
‹x' = (x1, x2e)›
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 xa a
proof -
show ‹valid_arena (get_clauses_wl_heur_init x) x1b (set (get_vdom_heur_init x))›
‹set (get_vdom_heur_init x) ⊆ set (get_vdom_heur_init x)› ‹set_mset (dom_m x1b) ⊆ set (get_vdom_heur_init x)›
‹distinct (get_vdom_heur_init x)› ‹(get_watchlist_wl_heur_init x, λ_. []) ∈ ⟨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_init_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 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] ac_simps)
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
‹(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›
where
‹extract_lits_sorted = (λ(xs, n, vars). do {
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 < unat32_max}›
lemma :
‹(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 < unat32_max› if ‹distinct b› ‹init_valid_rep x1 (set b)›
‹length x1 < unat32_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..<unat32_max - 1}›
using that by (auto simp: init_valid_rep_def)
from card_mono[OF _ this] show ?thesis
using ‹distinct x2a› by (auto simp: unat32_max_def distinct_card)
qed
have H_simple: ‹RETURN x2a
≤ ⇓ (list_mset_rel ∩ {(v, v'). length v < unat32_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›
definition reduce_interval_init :: ‹64 word› where ‹reduce_interval_init = 300›
text ‹This value is taken from CaDiCaL.›
definition inprocessing_interval_init :: ‹64 word› where ‹inprocessing_interval_init = 100000›
definition rephasing_initial_phase :: ‹64 word› where ‹rephasing_initial_phase = 10›
definition rephasing_end_of_initial_phase :: ‹64 word› where ‹rephasing_end_of_initial_phase = 10000›
definition subsuming_length_initial_phase :: ‹64 word› where ‹subsuming_length_initial_phase = 10000›
definition finalize_vmtf_init where ‹
finalize_vmtf_init = (λ(ns, m, fst_As, lst_As, next_search). do {
ASSERT (fst_As ≠ None);
ASSERT (lst_As ≠ None);
RETURN (ns, m, the fst_As, the lst_As, next_search)})›
definition finalize_bump_init :: ‹bump_heuristics_init ⇒ bump_heuristics nres› where
‹finalize_bump_init = (λx. case x of Tuple4 hstable focused foc to_remove ⇒ do {
focused ← finalize_vmtf_init focused;
RETURN (Tuple4 hstable focused foc to_remove)
})›
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 ⇒ isasat nres› where
‹finalise_init_code opts =
(λS. case S of Tuple15 M' N' D' Q' W' bmp φ clvls cach
lbd vdom ivdom _ lcount mark ⇒ do {
let init_stats = empty_stats_clss (of_nat (length ivdom));
let fema = ema_init (opts_fema opts);
let sema = ema_init (opts_sema opts);
let other_fema = ema_init (opts_fema opts);
let other_sema = ema_init (opts_sema opts);
let ccount = restart_info_init;
let heur = Restart_Heuristics ((fema, sema, ccount, 0, (φ, 0, replicate (length φ) False, 0, replicate (length φ) False, rephasing_end_of_initial_phase, 0, rephasing_initial_phase), reluctant_init, False, replicate (length φ) False, (inprocessing_interval_init, reduce_interval_init, subsuming_length_initial_phase), other_fema, other_sema));
let vdoms = AIvdom_init vdom [] ivdom;
let occs = replicate (length W') [];
bmp ← finalize_bump_init bmp;
RETURN (IsaSAT M' N' D' Q' W' bmp
clvls cach lbd (take 1 (replicate 160 (Pos 0))) init_stats
heur vdoms lcount opts [] occs)
})›
lemma isa_vmtf_init_nemptyD:
‹((ak, al, am, an, bc)) ∈ isa_vmtf_init 𝒜 au ⟹ 𝒜 ≠ {#} ⟹ ∃y. an = Some y›
‹((ak, al, am, an, bc)) ∈ isa_vmtf_init 𝒜 au ⟹ 𝒜 ≠ {#} ⟹ ∃y. am = Some y›
by (auto simp: isa_vmtf_init_def bump_heur_init_def)
lemma isa_vmtf_init_isa_vmtf: ‹𝒜 ≠ {#} ⟹ ((ak, al, Some am, Some an, bc))
∈ isa_vmtf_init 𝒜 au ⟹ ((ak, al, am, an, bc))
∈ vmtf 𝒜 au›
by (auto simp: isa_vmtf_init_def Image_iff)
lemma bump_heur_init_isa_vmtf: ‹𝒜 ≠ {#} ⟹ x ∈ bump_heur_init 𝒜 M ⟹ finalize_bump_init x ≤ ⇓Id (SPEC (λx. x ∈ bump_heur 𝒜 M))›
unfolding finalize_bump_init_def bump_heur_init_def bump_heur_def finalize_vmtf_init_def
nres_monad3
apply (cases x, hypsubst, simp)
apply refine_vcg
by (auto dest: isa_vmtf_init_nemptyD intro!: isa_vmtf_init_isa_vmtf)
lemma heuristic_rel_initI:
‹phase_saving 𝒜 φ ⟹ length φ' = length φ ⟹ length φ'' = length φ ⟹ phase_saving 𝒜 g ⟹
heuristic_rel 𝒜 (Restart_Heuristics ((fema, sema, ccount, 0, (φ,a, φ',b,φ'',c,d), e, f, g, h)))›
by (auto simp: heuristic_rel_def phase_save_heur_rel_def phase_saving_def heuristic_rel_stats_def)
lemma init_empty_occ_list_from_WL_length: ‹(x5, m) ∈ ⟨Id⟩map_fun_rel (D⇩0 A) ⟹
(replicate (length x5) [], empty_occs_list A) ∈ occurrence_list_ref›
by (auto simp: occurrence_list_ref_def map_fun_rel_def empty_occs_list_def ℒ⇩a⇩l⇩l_add_mset
dest!: multi_member_split)
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' ∧
aivdom_inv_strong_dec (get_aivdom S') (dom_m (get_clauses_wl T')) ∧
get_learned_count_init T = get_learned_count S'} (RETURN (finalise_init S))›
apply (cases S; cases T)
apply (simp add: finalise_init_code_def aivdom_inv_strong_dec_def2 split:prod.splits)
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 distinct_mset_dom AIvdom_init_def
finalise_init_code_def out_learned_def all_lits_st_alt_def[symmetric]
twl_st_heur_post_parsing_wl_def all_atms_st_def aivdom_inv_dec_def
intro!: ASSERT_leI intro!: heuristic_rel_initI
specify_left_RES[OF bump_heur_init_isa_vmtf[where 𝒜= ‹all_atms_st S› and M=‹get_trail_wl S›, unfolded conc_fun_RES]]
intro: )
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 distinct_mset_dom AIvdom_init_def init_empty_occ_list_from_WL_length
finalise_init_code_def out_learned_def all_lits_st_alt_def[symmetric] phase_saving_def
twl_st_heur_post_parsing_wl_def all_atms_st_def aivdom_inv_dec_def ac_simps
intro!: ASSERT_leI intro!: heuristic_rel_initI
intro: )
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, 0))
}›
definition init_trail_D_fast where
‹init_trail_D_fast = init_trail_D›
definition init_state_wl_D' :: ‹nat list × nat ⇒ (twl_st_wl_heur_init) nres› where
‹init_state_wl_D' = (λ(𝒜⇩i⇩n, n). do {
ASSERT(Suc (2 * (n)) ≤ unat32_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 mark = (0, replicate n None);
let WS = replicate m [];
vm ← initialize_Bump_Init 𝒜⇩i⇩n n;
let φ = replicate n False;
let cach = (replicate n SEEN_UNKNOWN, []);
let lbd = empty_lbd;
let vdom = [];
let ivdom = [];
let lcount = (0, 0, 0, 0, 0);
RETURN (Tuple15 M N D 0 WS vm φ 0 cach lbd vdom ivdom False lcount mark)
})›
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 simp: zeroed_trail_def)
subgoal by auto
done
qed
fun to_tuple where
‹to_tuple (Tuple15 a b c d e f g h i j k l m n ko) = (a, b, c, d, e, f, g, h, i, j, k, l, m, n, ko)›
definition tuple15_rel where tuple15_rel_internal_def:
‹tuple15_rel A B C D E F G H I J K L M N KO = {(S,T).
(case (S, T) of
(Tuple15 a b c d e f g h i j k l m n ko,
Tuple15 a' b' c' d' e' f' g' h' i' j' k' l' m' n' ko') ⇒
(a, a') ∈ A ∧ (b,b') ∈ B ∧ (c,c') ∈ C ∧ (d,d')∈D ∧ (e,e')∈E ∧
(f,f')∈F ∧ (g,g') ∈ G ∧ (h,h')∈H ∧ (i,i')∈I ∧ (j,j') ∈ J ∧ (k,k')∈K ∧
(l,l')∈L ∧ (m,m')∈M ∧ (n,n')∈N ∧ (ko,ko')∈KO)}›
lemma tuple15_rel_def:
‹⟨A,B,C,D,E,F,G,H,I,J,K,L,M,N,KO⟩tuple15_rel ≡ {(a,b). case (a,b) of
(Tuple15 a b c d e f g h i j k l m n ko,
Tuple15 a' b' c' d' e' f' g' h' i' j' k' l' m' n' ko') ⇒
(a, a') ∈ A ∧ (b,b') ∈ B ∧ (c,c') ∈ C ∧ (d,d')∈D ∧ (e,e')∈E ∧
(f,f')∈F ∧ (g,g') ∈ G ∧ (h,h')∈H ∧ (i,i')∈I ∧ (j,j') ∈ J ∧ (k,k')∈K ∧
(l,l')∈L ∧ (m,m')∈M ∧ (n,n')∈N ∧ (ko,ko')∈KO}›
by (simp add: tuple15_rel_internal_def relAPP_def)
lemma to_tuple_eq_iff[iff]: ‹to_tuple S = to_tuple T ⟷ S = T›
by (cases S; cases T) auto
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, Id, Id, nat_rel, ⟨⟨Id⟩list_rel⟩list_rel,
Id, ⟨bool_rel⟩list_rel, Id, Id, Id, Id, Id, Id, Id, Id⟩tuple15_rel⟩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);
mark ← SPEC (λD. (D, {#}) ∈ lookup_clause_rel 𝒜⇩i⇩n);
W ← SPEC (λW. (W, empty_watched 𝒜⇩i⇩n ) ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜⇩i⇩n));
vm ← RES (bump_heur_init 𝒜⇩i⇩n []);
φ ← SPEC (phase_saving 𝒜⇩i⇩n);
cach ← SPEC (cach_refinement_empty 𝒜⇩i⇩n);
let lbd = empty_lbd;
let vdom = [];
let ivdom = [];
let lcount = (0, 0, 0, 0, 0);
RETURN (Tuple15 M N D 0 W vm φ 0 cach lbd vdom ivdom False lcount mark)}› 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 :: 'b :: {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 :: ‹'b :: {zero,linorder}›
by (auto simp flip: Max.eq_fold Max.set_eq_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 [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 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: ›)
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 mark: ‹RETURN (0, replicate (Suc (b)) None)
≤ SPEC (λD. (D, {#}) ∈ 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 ≤ unat32_max ⟹
Suc (2 * (Max (insert 0 (set a)))) ≤ unat32_max› for a
apply (induction a)
apply (auto simp: unat32_max_def)
apply (auto simp: max_def ℒ⇩a⇩l⇩l_add_mset)
done
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)
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] initialize_Bump_Init[where 𝒜=𝒜⇩i⇩n, THEN fref_to_Down_curry, of _ ‹Suc (snd x)›] cach)
subgoal for a b by (auto simp: lits_with_max_rel_def intro: le_uint32)
subgoal by (auto intro!: 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 mark)
subgoal by (rule RETURN_rule) (rule H; simp only:)
subgoal using in_N0 by (auto simp: lits_with_max_rel_def P_def)
subgoal by simp
subgoal by (auto simp: lits_with_max_rel_def)
subgoal by (auto simp: lits_with_max_rel_def)
subgoal by (auto simp: lits_with_max_rel_def)
subgoal unfolding phase_saving_def lits_with_max_rel_def by (auto intro!: K)
subgoal by fast
subgoal by (auto simp: lits_with_max_rel_def)
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 tuple15_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, Id, Id, nat_rel, ⟨⟨Id⟩list_rel⟩list_rel,
Id, ⟨bool_rel⟩list_rel, Id, Id, Id, Id, Id, Id, Id, Id⟩tuple15_rel⟩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 all_lits_st_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, NEk, UEk, NS, US, N0, U0, Q), OC) = ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, (λ_. [])), OC)›
fun remove_watched :: ‹'v twl_st_wl_init_full ⇒ 'v twl_st_wl_init› where
‹remove_watched ((M, N, D, NE, UE, NEk, UEk, NNS, US, N0, U0, Q, _), OC) = ((M, N, D, NE, UE, NEk, UEk, NNS, US, N0, U0, 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 ⟹
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 =
(λS::twl_st_wl_heur_init. case S of Tuple15 M' N' D' j W' vm φ clvls cach lbd vdom failed x y z ⇒
RETURN (Tuple15 (trail_pol_slow_of_fast M') N' D' j (convert_wlists_to_nat_conv W') vm φ
clvls cach lbd vdom failed x y z))›
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 (cases S) auto
end