Theory IsaSAT

theory IsaSAT_ACIDS imports IsaSAT_Literals Pairing_Heap_LLVM.Heaps_Abs Watched_Literals_VMTF begin text ‹Instead of using VSIDS (which requires float), we use the more stable ACIDS variant that works simply on integers and does not seem much worse. We use ACIDS in a practical way, i.e., when the weight reaches the maximum integer, we simply stop incrementing it. › (*TODO rename VSIDS to ACIDS even if the difference is simply the bumping score*) section ‹ACIDS› type_synonym ('a, 'v) acids = ‹('a multiset × 'a multiset × ('a ⇒ 'v)) × 'v› definition acids :: ‹'a multiset ⇒ ('a, 'ann) ann_lits ⇒ ('a, 'v::{zero,linorder}) acids set› where ‹acids 𝒜 M = {((ℬ, b, w), m). set_mset ℬ = set_mset 𝒜 ∧ b ⊆# 𝒜 ∧ Max ({0} ∪ w ` set_mset b) ≤ m ∧ (∀L ∈#𝒜. L ∉# b ⟶ defined_lit M (Pos L)) ∧ distinct_mset b}› lemma acids_prepend: ‹ac ∈ acids 𝒜 M ⟹ ac ∈ acids 𝒜 (L # M)› unfolding acids_def by (auto simp: defined_lit_map) ACIDS: hmstruct_with_prio where le = ‹(≥) :: nat ⇒ nat ⇒ bool› and lt = ‹(>)› apply unfold_locales subgoal by auto subgoal by auto subgoal by (auto simp: transp_def) subgoal by (auto simp: totalp_on_def) done definition acids_tl_pre :: ‹'a ⇒ ('a, 'v) acids ⇒ bool› where ‹acids_tl_pre L = (λ(ac, m). L ∈# fst ac)› definition acids_tl :: ‹'a ⇒ ('a, 'v::ord) acids ⇒ ('a, 'v) acids nres› where ‹acids_tl L = (λ(ac, m). do { ASSERT (acids_tl_pre L (ac, m)); ac ← ACIDS.mop_prio_insert_unchanged L ac; w ← ACIDS.mop_prio_old_weight L ac; RETURN (ac, max m w) })› lemma acids_tl: ‹ac ∈ acids 𝒜 M ⟹ L ∈# 𝒜 ⟹ M ≠ [] ⟹ L = atm_of (lit_of (hd M)) ⟹ acids_tl L ac ≤ RES (acids 𝒜 (tl M))› unfolding acids_tl_def ACIDS.mop_prio_insert_unchanged_def ACIDS.mop_prio_insert_raw_unchanged_def nres_monad3 ACIDS.mop_prio_is_in_def ACIDS.mop_prio_old_weight_def ACIDS.mop_prio_insert_def RES_RES_RETURN_RES RETURN_def ACIDS.mop_prio_old_weight_def case_prod_beta nres_monad1 apply (refine_vcg lhs_step_If) subgoal by (cases M) (auto simp: acids_def ACIDS.mop_prio_insert_unchanged_def insert_subset_eq_iff acids_tl_pre_def intro!: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def ACIDS.mop_prio_insert_unchanged_def insert_subset_eq_iff acids_tl_pre_def intro!: subset_add_mset_notin_subset) subgoal apply (auto simp: acids_def ACIDS.mop_prio_insert_unchanged_def RES_RES_RETURN_RES defined_lit_map acids_tl_pre_def dest: subset_add_mset_notin_subset dest: multi_member_split) apply (smt (verit, best) image_iff not_hd_in_tl) apply refine_vcg apply fastforce apply fastforce apply (smt (verit, del_insts) Union_iff imageE insert_DiffM insert_subset_eq_iff prod.simps(1) singletonD subset_add_mset_notin_subset_mset) apply (auto simp: max_def) apply fastforce by (smt (verit, best) image_iff not_hd_in_tl) done definition acids_get_min :: ‹('a, nat) acids ⇒ 'a nres› where ‹acids_get_min = (λ(ac, m). do { L ← ACIDS.mop_prio_peek_min ac; RETURN L })› definition acids_mset :: ‹('a, 'v) acids ⇒ _› where ‹acids_mset x = fst (snd (fst x))› lemma acids_get_min: ‹acids_mset x ≠ {#} ⟹ acids_get_min x ≤ SPEC (λv. ACIDS.prio_peek_min (fst x) v)› unfolding acids_get_min_def ACIDS.mop_prio_peek_min_def acids_mset_def by refine_vcg (auto simp: ACIDS.prio_peek_min_def) definition acids_pop_min :: ‹('a, nat) acids ⇒ ('a × ('a, nat) acids) nres› where ‹acids_pop_min = (λ(ac, m). do { (v, ac) ← ACIDS.mop_prio_pop_min ac; RETURN (v, (ac, m)) })› definition acids_find_next_undef :: ‹nat multiset ⇒ (nat, nat) acids ⇒ (nat, nat) ann_lits ⇒ (nat option × (nat, nat) acids) nres› where ‹acids_find_next_undef 𝒜 = (λac M. do { WHILE_T⇗(λ(L, ac). (L = None ⟶ ac ∈ acids 𝒜 M) ∧ (L ≠ None ⟶ ac ∈ acids 𝒜 (Decided (Pos (the L)) # M) ∧ Pos (the L) ∈# ℒ_a_l_l 𝒜 ∧ undefined_lit M (Pos (the L)))) ⇖ (λ(nxt, ac). nxt = None ∧ acids_mset ac ≠ {#}) (λ(a, ac). do { ASSERT (a = None); (L, ac) ← acids_pop_min ac; ASSERT(Pos L ∈# ℒ_a_l_l 𝒜); if defined_lit M (Pos L) then RETURN (None, ac) else RETURN (Some L, ac) } ) (None, ac) })› lemma acids_pop_min: ‹acids_mset x ≠ {#} ⟹ x ∈ acids 𝒜 M ⟹ acids_pop_min x ≤ SPEC (λ(v, ac). acids_mset ac = acids_mset x - {#v#} ∧ v ∈# acids_mset x ∧ ACIDS.prio_peek_min (fst x) v ∧ (defined_lit M (Pos v) ⟶ ac ∈ acids 𝒜 M) ∧ (undefined_lit M (Pos v) ⟶ ac ∈ acids 𝒜 (Decided (Pos v) # M)))› unfolding ACIDS.mop_prio_pop_min_def acids_pop_min_def ACIDS.mop_prio_peek_min_def ACIDS.mop_prio_del_def by refine_vcg (auto simp: acids_def ACIDS.prio_peek_min_def distinct_mset_remove1_All ACIDS.prio_del_def defined_lit_map acids_mset_def dest: in_diffD) lemma acids_find_next_undef: assumes vmtf: ‹ac ∈ acids 𝒜 M› shows ‹acids_find_next_undef 𝒜 ac M ≤ ⇓ Id (SPEC (λ(L, ac). (L = None ⟶ ac ∈ acids 𝒜 M ∧ (∀L∈#ℒ_a_l_l 𝒜. defined_lit M L)) ∧ (L ≠ None ⟶ ac ∈ acids 𝒜 (Decided (Pos (the L)) # M) ∧ Pos (the L) ∈# ℒ_a_l_l 𝒜 ∧ undefined_lit M (Pos (the L)))))› proof - have [refine0]: ‹wf (measure (λ(_, ac). size (acids_mset ac)))› by auto show ?thesis unfolding acids_find_next_undef_def apply (refine_vcg acids_pop_min[of _ 𝒜 M, THEN order_trans]) subgoal using assms by auto subgoal by auto subgoal by (auto simp: ACIDS.prio_peek_min_def acids_def acids_mset_def in_ℒ_a_l_l_atm_of_𝒜_i_n) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: acids_def ACIDS.prio_peek_min_def in_ℒ_a_l_l_atm_of_𝒜_i_n) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: ACIDS.prio_peek_min_def acids_mset_def dest: multi_member_split) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: ACIDS.prio_peek_min_def acids_mset_def dest: multi_member_split) subgoal by auto subgoal by (auto simp: ACIDS.prio_peek_min_def acids_mset_def acids_def in_ℒ_a_l_l_atm_of_𝒜_i_n dest!: multi_member_split[of ‹_ :: nat›]) subgoal by auto subgoal by auto subgoal by auto done qed definition acids_push_literal_pre where ‹acids_push_literal_pre 𝒜 L = (λac. L ∈# 𝒜)› definition acids_push_literal :: ‹'a ⇒ ('a, nat) acids ⇒ ('a, nat) acids nres› where ‹acids_push_literal L = (λ(ac, m). do { ASSERT (L ∈# fst ac); w ← ACIDS.mop_prio_old_weight L ac; let w = min m w; ASSERT (w ≤ m); ASSERT ((m - w) div 2 ≤ m); let w = m - ((m - w) div 2); ac ← ACIDS.mop_prio_insert_maybe L w ac; RETURN (ac, m) })› lemma acids_push_literal: ‹ac ∈ acids 𝒜 M ⟹ acids_push_literal_pre 𝒜 L ac ⟹ acids_push_literal L ac ≤ SPEC (λac. ac ∈ acids 𝒜 M)› unfolding acids_push_literal_def ACIDS.mop_prio_insert_maybe_def ACIDS.mop_prio_old_weight_def acids_push_literal_pre_def ACIDS.mop_prio_insert_def ACIDS.mop_prio_change_weight_def ACIDS.mop_prio_is_in_def apply refine_vcg subgoal by (auto simp: acids_def acids_mset_def) subgoal by (auto simp: acids_def dest!: multi_member_split) subgoal by (auto simp: ACIDS.mop_prio_change_weight_def acids_def dest!: multi_member_split) subgoal by (auto simp: acids_def dest!: multi_member_split) subgoal by (auto simp: acids_def acids_mset_def) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) subgoal by (auto simp: acids_def acids_mset_def dest!: multi_member_split dest: subset_add_mset_notin_subset) done definition acids_flush_int :: ‹nat multiset ⇒ (nat,nat) ann_lits ⇒ (nat, nat) acids ⇒ _ ⇒ ((nat, nat) acids × _)nres› where ‹acids_flush_int 𝒜_i_n = (λM vm (to_remove, h). do { ASSERT(length to_remove ≤ unat32_max); (_, vm, h) ← WHILE_T⇗λ(i, vm', h). i ≤ length to_remove ∧ (i < length to_remove ⟶ acids_push_literal_pre 𝒜_i_n (to_remove!i) (vm'))⇖ (λ(i, vm, h). i < length to_remove) (λ(i, vm, h). do { ASSERT(i < length to_remove); ASSERT(to_remove!i ∈# 𝒜_i_n); ASSERT(atoms_hash_del_pre (to_remove!i) h); vm ← acids_push_literal (to_remove!i) vm; RETURN (i+1, vm, atoms_hash_del (to_remove!i) h)}) (0, vm, h); RETURN (vm, (emptied_list to_remove, h)) })› definition acids_flush :: ‹nat multiset ⇒ (nat,nat) ann_lits ⇒ (nat, nat) acids ⇒ nat set ⇒ ((nat, nat) acids × nat set) nres› where ‹acids_flush 𝒜_i_n = (λM vm remove_int. SPEC (λx. (fst x) ∈ acids 𝒜_i_n M ∧ snd x = {}))› lemma acids_change_to_remove_order: assumes vmtf: ‹ac ∈ acids 𝒜_i_n M› and CD_rem: ‹((C, D), to_remove) ∈ distinct_atoms_rel 𝒜_i_n› and nempty: ‹isasat_input_nempty 𝒜_i_n› and bounded: ‹isasat_input_bounded 𝒜_i_n› and t: ‹to_remove ⊆ set_mset 𝒜_i_n› shows ‹acids_flush_int 𝒜_i_n M ac (C, D) ≤ ⇓(Id ×_r distinct_atoms_rel 𝒜_i_n) (acids_flush 𝒜_i_n M ac to_remove)› proof - have to_C: ‹to_remove = set C› using CD_rem by (auto simp: distinct_atoms_rel_def distinct_hash_atoms_rel_def) have length_le: ‹length (fst (C,D)) ≤ unat32_max› proof - have lits: ‹literals_are_in_ℒ_i_n 𝒜_i_n (Pos `# mset C)› and dist: ‹distinct C› using vmtf CD_rem t unfolding vmtf_def vmtf_ℒ_a_l_l_def apply (auto simp: literals_are_in_ℒ_i_n_alt_def distinct_atoms_rel_alt_def inj_on_def) by (metis atms_of_ℒ_a_l_l_𝒜_i_n in_mono) have dist: ‹distinct_mset (Pos `# mset C)› by (subst distinct_image_mset_inj) (use dist in ‹auto simp: inj_on_def›) have tauto: ‹¬ tautology (poss (mset C))› by (auto simp: tautology_decomp) show ?thesis using simple_clss_size_upper_div2[OF bounded lits dist tauto] by (auto simp: unat32_max_def) qed have acids_push_literal_pre: ‹acids_push_literal_pre 𝒜_i_n (C ! i) ac› if ‹i < length C› for i using t that CD_rem unfolding acids_push_literal_pre_def distinct_atoms_rel_def distinct_hash_atoms_rel_def by auto define I where ‹I ≡ λ(i::nat, vm'::(nat, nat)acids, h). vm' ∈ acids 𝒜_i_n M ∧ ((drop i C, h), to_remove - set (take i C)) ∈ distinct_atoms_rel 𝒜_i_n ∧ i ≤ length C› have sin: ‹fst s < length (fst (C, D)) ⟹ fst (C, D) ! fst s ∈# 𝒜_i_n› and atms: ‹I s ⟹ fst s < length (fst (C, D)) ⟹ atoms_hash_del_pre (fst (C, D) ! fst s) (snd (snd s))› for s using t CD_rem nth_mem[of ‹fst s› C] unfolding acids_push_literal_pre_def distinct_atoms_rel_def distinct_hash_atoms_rel_def I_def atoms_hash_del_pre_def atoms_hash_rel_def by (auto simp del: nth_mem) let ?R = ‹measure (λ(i, vm', h). length C - i)› have I_inv1_acids_push_literal_pre: ‹I s ⟹ fst (C, D) ! fst s ∈# 𝒜_i_n ⟹ x ∈ acids 𝒜_i_n M ⟹ fst (fst s + 1, x, atoms_hash_del (fst (C, D) ! fst s) (snd (snd s))) < length (fst (C, D)) ⟹ acids_push_literal_pre 𝒜_i_n (fst (C, D) ! fst (fst s + 1, x, atoms_hash_del (fst (C, D) ! fst s) (snd (snd s)))) (fst (snd (fst s + 1, x, atoms_hash_del (fst (C, D) ! fst s) (snd (snd s)))))› for s x using t CD_rem unfolding acids_push_literal_pre_def distinct_atoms_rel_def distinct_hash_atoms_rel_def by auto have I_Suc: ‹I s ⟹ fst s < length (fst (C, D)) ⟹ fst (C, D) ! fst s ∈# 𝒜_i_n ⟹ atoms_hash_del_pre (fst (C, D) ! fst s) (snd (snd s)) ⟹ x ∈ acids 𝒜_i_n M ⟹ I (fst s + 1, x, atoms_hash_del (fst (C, D) ! fst s) (snd (snd s)))› for s x apply (auto simp: I_def distinct_atoms_rel_def distinct_hash_atoms_rel_def intro!: relcompI[of _ ‹(drop (Suc (fst s)) C, (snd (snd s))[C ! (fst s) := False], to_remove - set (take (Suc (fst s)) C))›]) apply (rule relcompI[of _ ‹(drop (Suc (fst s)) C, to_remove - set (take (Suc (fst s)) C))›]) subgoal by (auto simp: atoms_hash_rel_def atoms_hash_del_def take_Suc_conv_app_nth) subgoal by (auto simp: take_Suc_conv_app_nth simp flip: Cons_nth_drop_Suc) done show ?thesis unfolding acids_flush_int_def acids_flush_def case_prod_beta apply (refine_vcg specify_left[OF WHILEIT_rule_stronger_inv[where Φ = ‹(λx. I x ∧ fst x =length (fst (C, D)))› and I' = ‹I› and R = ?R]] acids_push_literal[where 𝒜=𝒜_i_n and M=M]) subgoal by (rule length_le) subgoal by auto subgoal by auto subgoal by (auto intro!: acids_push_literal_pre) subgoal using assms by (auto simp: I_def) subgoal by (rule sin) subgoal by (rule atms) subgoal by (auto simp: I_def) subgoal by auto subgoal by auto subgoal for s x by (rule I_inv1_acids_push_literal_pre) subgoal by (rule I_Suc) subgoal for s x by (auto simp: I_def) subgoal by (auto simp: emptied_list_def conc_fun_RES I_def) subgoal by (auto simp add: emptied_list_def conc_fun_RES I_def Image_iff to_C) done qed end

Theory IsaSAT_ACIDS