Theory IsaSAT_Simplify_Forward_Subsumption

theory IsaSAT_Simplify_Forward_Subsumption_Defs imports IsaSAT_Setup IsaSAT_Occurence_List IsaSAT_Restart IsaSAT_LBD begin section ‹Forward subsumption› subsection ‹Algorithm› text ‹We first refine the algorithm to use occurence lists, while keeping as many things as possible abstract (like the candidate selection or the selection of the literal with the least number of occurrences). We also include the marking structure (at least abstractly, because why not) For simplicity, we keep the occurrence list outside of the state (unlike the current solver where this is part of the state.)› definition valid_occs where ‹valid_occs occs vdom ⟷ cocc_content_set occs ⊆ set (get_vdom_aivdom vdom) ∧ distinct_mset (cocc_content occs)› text ‹This version is equivalent to term‹twl_st_heur_restart›, without any information on the occurrence list.› definition twl_st_heur_restart_occs :: ‹(isasat × nat twl_st_wl) set› where [unfolded Let_def]: ‹twl_st_heur_restart_occs = {(S,T). let M' = get_trail_wl_heur S; N' = get_clauses_wl_heur S; D' = get_conflict_wl_heur S; W' = get_watched_wl_heur S; j = literals_to_update_wl_heur S; outl = get_outlearned_heur S; cach = get_conflict_cach S; clvls = get_count_max_lvls_heur S; vm = get_vmtf_heur S; vdom = get_aivdom S; heur = get_heur S; old_arena = get_old_arena S; lcount = get_learned_count S; occs = get_occs S in let M = get_trail_wl T; N = get_clauses_wl T; D = get_conflict_wl T; Q = literals_to_update_wl T; W = get_watched_wl T; N0 = get_init_clauses0_wl T; U0 = get_learned_clauses0_wl T; NS = get_subsumed_init_clauses_wl T; US = get_subsumed_learned_clauses_wl T; NEk = get_kept_unit_init_clss_wl T; UEk = get_kept_unit_learned_clss_wl T; NE = get_unkept_unit_init_clss_wl T; UE = get_unkept_unit_learned_clss_wl T in (M', M) ∈ trail_pol (all_init_atms N (NE+NEk+NS+N0)) ∧ valid_arena N' N (set (get_vdom_aivdom vdom)) ∧ (D', D) ∈ option_lookup_clause_rel (all_init_atms N (NE+NEk+NS+N0)) ∧ (D = None ⟶ j ≤ length M) ∧ Q = uminus `# lit_of `# mset (drop j (rev M)) ∧ (W', W) ∈ ⟨Id⟩map_fun_rel (D₀ (all_init_atms N (NE+NEk+NS+N0))) ∧ vm ∈ bump_heur (all_init_atms N (NE+NEk+NS+N0)) M ∧ no_dup M ∧ clvls ∈ counts_maximum_level M D ∧ cach_refinement_empty (all_init_atms N (NE+NEk+NS+N0)) cach ∧ out_learned M D outl ∧ clss_size_corr_restart N NE {#} NEk UEk NS {#} N0 {#} lcount ∧ vdom_m (all_init_atms N (NE+NEk+NS+N0)) W N ⊆ set (get_vdom_aivdom vdom) ∧ aivdom_inv_dec vdom (dom_m N) ∧ isasat_input_bounded (all_init_atms N (NE+NEk+NS+N0)) ∧ isasat_input_nempty (all_init_atms N (NE+NEk+NS+N0)) ∧ old_arena = [] ∧ heuristic_rel (all_init_atms N (NE+NEk+NS+N0)) heur ∧ valid_occs occs vdom }› abbreviation twl_st_heur_restart_occs' :: ‹_› where ‹twl_st_heur_restart_occs' r u ≡ {(S, T). (S, T) ∈ twl_st_heur_restart_occs ∧ length (get_clauses_wl_heur S) = r ∧ learned_clss_count S ≤ u}› definition subsume_clauses_match2_pre :: ‹nat ⇒ nat ⇒ _ ⇒ clause_hash ⇒ bool› where ‹subsume_clauses_match2_pre C C' N D ⟷ subsume_clauses_match_pre C C' (get_clauses_wl N) ∧ snd D = mset (get_clauses_wl N ∝ C')› definition subsume_clauses_match2 :: ‹nat ⇒ nat ⇒ _ ⇒ clause_hash ⇒ nat subsumption nres› where ‹subsume_clauses_match2 C C' N D = do { ASSERT (subsume_clauses_match2_pre C C' N D); let n = length (get_clauses_wl N ∝ C); (i, st) ← WHILE_T⇗ λ(i,s). try_to_subsume C' C ((get_clauses_wl N)(C ↪ take i (get_clauses_wl N ∝ C))) s⇖ (λ(i, st). i < n∧ st ≠ NONE) (λ(i, st). do { L ← mop_clauses_at (get_clauses_wl N) C i; lin ← mop_ch_in L D; if lin then RETURN (i+1, st) else do { lin ← mop_ch_in (-L) D; if lin then if is_subsumed st then RETURN (i+1, STRENGTHENED_BY L C) else RETURN (i+1, NONE) else RETURN (i+1, NONE) }}) (0, SUBSUMED_BY C); RETURN st }› definition push_to_occs_list2_pre :: ‹_› where ‹push_to_occs_list2_pre C S occs ⟷ (C ∈# dom_m (get_clauses_wl S) ∧ length (get_clauses_wl S ∝ C) ≥ 2 ∧ fst occs = set_mset (all_init_atms_st S) ∧ atm_of ` set (get_clauses_wl S ∝ C) ⊆ set_mset (all_init_atms_st S) ∧ C ∉# all_occurrences (mset_set (fst occs)) occs)› definition push_to_occs_list2 where ‹push_to_occs_list2 C S occs = do { ASSERT (push_to_occs_list2_pre C S occs); L ← SPEC (λL. L ∈# mset (get_clauses_wl S ∝ C)); mop_occ_list_append C occs L }› definition maybe_push_to_occs_list2 where ‹maybe_push_to_occs_list2 C S occs = do { ASSERT (push_to_occs_list2_pre C S occs); b ← SPEC (λ_. True); if b then do { L ← SPEC (λL. L ∈# mset (get_clauses_wl S ∝ C)); mop_occ_list_append C occs L } else RETURN occs }› definition isa_is_candidate_forward_subsumption where ‹isa_is_candidate_forward_subsumption S C = do { ASSERT(arena_act_pre (get_clauses_wl_heur S) C); lbd ← mop_arena_lbd (get_clauses_wl_heur S) C; sze ← mop_arena_length (get_clauses_wl_heur S) C; status ← mop_arena_status (get_clauses_wl_heur S) C; ASSERT (sze ≤ length (get_clauses_wl_heur S)); (_, added) ← WHILE_T (λ(i, added). i < sze ∧ added ≤ 2) (λ(i, added). do { ASSERT (i < sze); L ← mop_arena_lit2 (get_clauses_wl_heur S) C i; is_added ← mop_is_marked_added_heur (get_heur S) (atm_of L); RETURN (i+1, added + (if is_added then 1 else 0)) }) (0, 0 :: 64 word); let (lbd_limit, size_limit) = get_lsize_limit_stats_st S; let can_del = sze ≠ 2 ∧ (status = LEARNED ⟶ lbd ≤ lbd_limit ∧ sze ≤ size_limit) ∧ (added ≥ 2); RETURN can_del }› definition find_best_subsumption_candidate where ‹find_best_subsumption_candidate C S = do { L ← mop_arena_lit2 (get_clauses_wl_heur S) C 0; ASSERT (nat_of_lit L < length (get_occs S)); score ← mop_cocc_list_length (get_occs S) L; n ← mop_arena_length_st S C; (i,score,L) ← WHILE_T (λ(i,score,L). i < n) (λ(i,score,L). do { ASSERT (Suc i ≤ unat32_max); new_L ← mop_arena_lit2 (get_clauses_wl_heur S) C i; ASSERT (nat_of_lit L < length (get_occs S)); new_score ← mop_cocc_list_length (get_occs S) L; if new_score < score then RETURN (i+1, new_score, new_L) else RETURN (i+1, score, L) }) (1, score, L); RETURN L }› definition isa_push_to_occs_list_st where ‹isa_push_to_occs_list_st C S = do { L ← find_best_subsumption_candidate C S; ASSERT (length (get_occs S ! nat_of_lit L) < length (get_clauses_wl_heur S)); occs ← mop_cocc_list_append C (get_occs S) L; RETURN (set_occs_wl_heur occs S) }› definition find_best_subsumption_candidate_and_push where ‹find_best_subsumption_candidate_and_push C S = do { L ← mop_arena_lit2 (get_clauses_wl_heur S) C 0; ASSERT (nat_of_lit L < length (get_occs S)); score ← mop_cocc_list_length (get_occs S) L; n ← mop_arena_length_st S C; (i,score,L,push) ← WHILE_T (λ(i,score,L,push). i < n ∧ push) (λ(i,score,L,push). do { ASSERT (Suc i ≤ unat32_max); new_L ← mop_arena_lit2 (get_clauses_wl_heur S) C i; ASSERT (nat_of_lit L < length (get_occs S)); new_score ← mop_cocc_list_length (get_occs S) L; b ← mop_is_marked_added_heur (get_heur S) (atm_of L); if new_score < score then RETURN (i+1, new_score, new_L,b) else RETURN (i+1, score, L,b) }) (1, score, L, True); RETURN (L, push) }› definition isa_maybe_push_to_occs_list_st where ‹isa_maybe_push_to_occs_list_st C S = do { (L, push) ← find_best_subsumption_candidate_and_push C S; if push then do { let L = L; ASSERT (length (get_occs S ! nat_of_lit L) < length (get_clauses_wl_heur S)); occs ← mop_cocc_list_append C (get_occs S) L; RETURN (set_occs_wl_heur occs S) } else RETURN S }› definition forward_subsumption_one_wl2_pre :: ‹nat ⇒ nat multiset ⇒ nat literal ⇒ nat twl_st_wl ⇒ bool› where ‹forward_subsumption_one_wl2_pre = (λC cands L S. forward_subsumption_one_wl_pre C cands S ∧ L ∈# all_init_lits_of_wl S)› definition isa_forward_subsumption_one_wl_pre :: ‹_› where ‹isa_forward_subsumption_one_wl_pre C L S ⟷ (∃T r u cands. (S,T)∈twl_st_heur_restart_occs' r u ∧ forward_subsumption_one_wl2_pre C cands L T) › definition forward_subsumption_one_wl2_inv :: ‹'v twl_st_wl ⇒ nat ⇒ nat multiset ⇒ nat list ⇒ nat × 'v subsumption ⇒ bool› where ‹forward_subsumption_one_wl2_inv = (λS C cands ys (i, x). forward_subsumption_one_wl_inv S C (mset ys) (mset (drop i ys), x))› definition isa_forward_subsumption_one_wl2_inv :: ‹isasat ⇒ nat ⇒ nat literal ⇒ nat × nat subsumption ⇒ bool› where ‹isa_forward_subsumption_one_wl2_inv = (λS C L (ix). (∃T r u cands. (S,T)∈twl_st_heur_restart_occs' r u ∧ forward_subsumption_one_wl2_inv T C cands (get_occs S ! nat_of_lit L) (ix)))› definition isa_subsume_clauses_match2_pre :: ‹_› where ‹isa_subsume_clauses_match2_pre C C' S D ⟷ ( ∃T r u D'. (S,T)∈twl_st_heur_restart_occs' r u ∧ subsume_clauses_match2_pre C C' T D' ∧ (D,D') ∈ clause_hash) › definition isa_subsume_clauses_match2 :: ‹nat ⇒ nat ⇒ isasat ⇒ bool list ⇒ nat subsumption nres› where ‹isa_subsume_clauses_match2 C' C N D = do { ASSERT (isa_subsume_clauses_match2_pre C' C N D); n ← mop_arena_length_st N C'; ASSERT (n ≤ length (get_clauses_wl_heur N)); (i, st) ← WHILE_T⇗ λ(i,s). True⇖ (λ(i, st). i < n∧ st ≠ NONE) (λ(i, st). do { ASSERT (i < n); L ← mop_arena_lit2 (get_clauses_wl_heur N) C' i; lin ← mop_cch_in L D; if lin then RETURN (i+1, st) else do { lin ← mop_cch_in (-L) D; if lin then if is_subsumed st then do {RETURN (i+1, STRENGTHENED_BY L C')} else do {RETURN (i+1, NONE)} else do {RETURN (i+1, NONE)} }}) (0, SUBSUMED_BY C'); RETURN st }› definition isa_subsume_or_strengthen_wl_pre :: ‹_› where ‹isa_subsume_or_strengthen_wl_pre C s S ⟷ (∃T r u. (S,T)∈twl_st_heur_restart_occs' r u ∧ subsume_or_strengthen_wl_pre C s T)› definition remove_lit_from_clause where ‹remove_lit_from_clause N C L = do { n ← mop_arena_length N C; (i, j, N) ← WHILE_T (λ(i, j, N). j < n) (λ(i, j, N). do { ASSERT (i < n); ASSERT (j < n); K ← mop_arena_lit2 N C j; if K ≠ L then do { N ← mop_arena_swap C i j N; RETURN (i+1, j+1, N)} else RETURN (i, j+1, N) }) (0, 0, N); N ← mop_arena_shorten C i N; N ← update_lbd_shrunk_clause C N; RETURN N }› definition remove_lit_from_clause_st :: ‹_› where ‹remove_lit_from_clause_st T C L = do { N ← remove_lit_from_clause (get_clauses_wl_heur T) C L; RETURN (set_clauses_wl_heur N T) }› (* TODO the wasted bits should be incremented in the deletion functions TODO rename the mark_garbage_heurX functions with proper name like below *) definition mark_garbage_heur_as_subsumed :: ‹nat ⇒ isasat ⇒ isasat nres› where ‹mark_garbage_heur_as_subsumed C S = (do{ let N' = get_clauses_wl_heur S; ASSERT (arena_is_valid_clause_vdom N' C); _ ← log_del_clause_heur S C; let st = arena_status N' C = IRRED; ASSERT (mark_garbage_pre (N', C)); let N' = extra_information_mark_to_delete (N') C; size ← mop_arena_length (get_clauses_wl_heur S) C; let lcount = get_learned_count S; ASSERT(¬st ⟶ clss_size_lcount lcount ≥ 1); let lcount = (if st then lcount else (clss_size_decr_lcount lcount)); let stats = get_stats_heur S; let stats = (if st then decr_irred_clss stats else stats); let S = set_clauses_wl_heur N' S; let S = set_learned_count_wl_heur lcount S; let S = set_stats_wl_heur stats S; let S = incr_wasted_st (of_nat size) S; RETURN S })› definition isa_strengthen_clause_wl2 where ‹isa_strengthen_clause_wl2 C C' L S = do { m ← mop_arena_length (get_clauses_wl_heur S) C; n ← mop_arena_length (get_clauses_wl_heur S) C'; st1 ← mop_arena_status (get_clauses_wl_heur S) C; st2 ← mop_arena_status (get_clauses_wl_heur S) C'; S ← remove_lit_from_clause_st S C (-L); _ ← log_new_clause_heur S C; let _ = mark_clause_for_unit_as_changed 0; if m = n then do { S ← RETURN S; S ← (if st1 = LEARNED ∧ st2 = IRRED then mop_arena_promote_st S C else RETURN S); S ← mark_garbage_heur_as_subsumed C' S; RETURN (set_stats_wl_heur (incr_forward_strengethening (get_stats_heur S)) S) } else RETURN (set_stats_wl_heur (incr_forward_strengethening (get_stats_heur S)) S) }› definition incr_forward_subsumed_st :: ‹_› where ‹incr_forward_subsumed_st S = (set_stats_wl_heur (incr_forward_subsumed (get_stats_heur S)) S)› definition incr_forward_tried_st :: ‹_› where ‹incr_forward_tried_st S = (set_stats_wl_heur (incr_forward_tried (get_stats_heur S)) S)› definition incr_forward_rounds_st :: ‹_› where ‹incr_forward_rounds_st S = (set_stats_wl_heur (incr_forward_rounds (get_stats_heur S)) S)› definition incr_forward_strengthened_st :: ‹_› where ‹incr_forward_strengthened_st S = (set_stats_wl_heur (incr_forward_strengethening (get_stats_heur S)) S)› definition isa_subsume_or_strengthen_wl :: ‹nat ⇒ nat subsumption ⇒ isasat ⇒ isasat nres› where ‹isa_subsume_or_strengthen_wl = (λC s S. do { ASSERT(isa_subsume_or_strengthen_wl_pre C s S); (case s of NONE ⇒ RETURN S | SUBSUMED_BY C' ⇒ do { st1 ← mop_arena_status (get_clauses_wl_heur S) C; st2 ← mop_arena_status (get_clauses_wl_heur S) C'; S ← mark_garbage_heur2 C S; let _ = mark_clause_for_unit_as_changed 0; S ← (if st1 = IRRED ∧ st2 = LEARNED then mop_arena_promote_st S C' else RETURN S); let S = (set_stats_wl_heur (incr_forward_subsumed (get_stats_heur S)) S); RETURN S } | STRENGTHENED_BY L C' ⇒ isa_strengthen_clause_wl2 C C' L S) })› definition mop_cch_remove_one where ‹mop_cch_remove_one L D = do { ASSERT (nat_of_lit L < length D); RETURN (D[nat_of_lit L := False]) } › definition mop_cch_remove_all_clauses where ‹mop_cch_remove_all_clauses S C D = do { n ← mop_arena_length (get_clauses_wl_heur S) C; (_, D) ← WHILE_T (λ(i, D). i < n) (λ(i, D). do {ASSERT (i < length (get_clauses_wl_heur S)); L ← mop_arena_lit2 (get_clauses_wl_heur S) C i; D ← mop_cch_remove_one L D; RETURN (i+1, D)}) (0, D); RETURN D } › definition isa_forward_subsumption_one_wl :: ‹nat ⇒ bool list ⇒ nat literal ⇒ isasat ⇒ (isasat × nat subsumption × bool list) nres› where ‹isa_forward_subsumption_one_wl = (λC D L S. do { ASSERT (isa_forward_subsumption_one_wl_pre C L S); ASSERT (nat_of_lit L < length (get_occs S)); n ← mop_cocc_list_length (get_occs S) L; (_, s) ← WHILE_T⇗ isa_forward_subsumption_one_wl2_inv S C L ⇖ (λ(i, s). i < n ∧ s = NONE) (λ(i, s). do { ASSERT (i < n); C' ← mop_cocc_list_at (get_occs S) L i; status ← mop_arena_status (get_clauses_wl_heur S) C'; if status = DELETED then RETURN (i+1, s) else do { s ← isa_subsume_clauses_match2 C' C S D; RETURN (i+1, s) } }) (0, NONE); D ← (if s ≠ NONE then mop_cch_remove_all_clauses S C D else RETURN D); S ← (if is_strengthened s then isa_maybe_push_to_occs_list_st C S else RETURN S); S ← isa_subsume_or_strengthen_wl C s S; RETURN (S, s, D) })› definition try_to_forward_subsume_wl2_pre :: ‹_› where ‹try_to_forward_subsume_wl2_pre C cands shrunken S ⟷ distinct_mset cands ∧ try_to_forward_subsume_wl_pre C cands S› definition isa_try_to_forward_subsume_wl_pre :: ‹_› where ‹isa_try_to_forward_subsume_wl_pre C shrunken S ⟷ (∃T r u cands occs'. (S,T)∈twl_st_heur_restart_occs' r u ∧ (get_occs S, occs') ∈ occurrence_list_ref ∧ try_to_forward_subsume_wl2_pre C cands (mset shrunken) T)› definition try_to_forward_subsume_wl2_inv :: ‹_› where ‹try_to_forward_subsume_wl2_inv S cands C = (λ(i, changed, break, occs, D, T). try_to_forward_subsume_wl_inv S cands C (i, break, T) ∧ (¬changed ⟶ (D, mset (get_clauses_wl T ∝ C)) ∈ clause_hash_ref (all_init_atms_st T)) ∧ (changed ⟶ (D, {#}) ∈ clause_hash_ref (all_init_atms_st T)))› definition isa_try_to_forward_subsume_wl_inv :: ‹isasat ⇒ nat ⇒ nat × nat subsumption × bool × bool list × isasat ⇒ bool› where ‹isa_try_to_forward_subsume_wl_inv S C = (λ(i, changed, break, D, T). (∃S' T' cands occs' D'. (S,S')∈twl_st_heur_restart_occs' (length (get_clauses_wl_heur S)) (learned_clss_count S) ∧ (T,T')∈twl_st_heur_restart_occs' (length (get_clauses_wl_heur S)) (learned_clss_count S)∧ (get_occs T, occs') ∈ occurrence_list_ref ∧ (D,D') ∈clause_hash ∧ try_to_forward_subsume_wl2_inv S' cands C (i, changed ≠ NONE, break, occs', D', T')))› (*TODO: Missing ticks*) definition isa_try_to_forward_subsume_wl2_break :: ‹isasat ⇒ bool nres› where ‹isa_try_to_forward_subsume_wl2_break S = RETURN False› definition isa_try_to_forward_subsume_wl2 :: ‹nat ⇒ bool list ⇒ nat list ⇒ isasat ⇒ (bool list × nat list × isasat) nres› where ‹isa_try_to_forward_subsume_wl2 C D shrunken S = do { ASSERT (isa_try_to_forward_subsume_wl_pre C shrunken S); n ← mop_arena_length_st S C; ASSERT (n ≤ Suc (unat32_max div 2)); let n = 2 * n; ebreak ← isa_try_to_forward_subsume_wl2_break S; (_, changed, _, D, S) ← WHILE_T⇗ isa_try_to_forward_subsume_wl_inv S C⇖ (λ(i, changed, break, D, S). ¬break ∧ i < n) (λ(i, changed, break, D, S). do { ASSERT (i < n); L ← mop_arena_lit2 (get_clauses_wl_heur S) C (i div 2); let L = (if i mod 2 = 0 then L else - L); (S, subs, D) ← isa_forward_subsumption_one_wl C D L S; ebreak ← isa_try_to_forward_subsume_wl2_break S; RETURN (i+1, subs, (subs ≠ NONE) ∨ ebreak, D, S) }) (0, NONE, ebreak, D, S); D ← (if changed = NONE then mop_cch_remove_all_clauses S C D else RETURN D); let _ = (if changed = NONE then mark_clause_for_unit_as_unchanged 0 else ()); ASSERT (Suc (length shrunken) ≤ length (get_tvdom S)); let add_to_shunken = (is_strengthened changed); let shrunken = (if add_to_shunken then shrunken @ [C] else shrunken); RETURN (D, shrunken, S) }› definition isa_forward_subsumption_pre_all :: ‹_› where ‹isa_forward_subsumption_pre_all S ⟷ (∃T r u. (S,T)∈twl_st_heur_restart_ana' r u ∧ forward_subsumption_all_wl_pre T)› definition correct_occurence_list where ‹correct_occurence_list S occs cands n ⟷ distinct_mset cands ∧ all_occurrences (all_init_atms_st S) occs ∩# cands = {#} ∧ (∀C∈# all_occurrences (all_init_atms_st S) occs. C ∈# dom_m (get_clauses_wl S) ⟶ length (get_clauses_wl S ∝ C) ≤ n)∧ (∀C∈# all_occurrences (all_init_atms_st S) occs. C ∈# dom_m (get_clauses_wl S) ⟶ (∀L∈set (get_clauses_wl S ∝ C). undefined_lit (get_trail_wl S) L)) ∧ fst occs = set_mset (all_init_atms_st S)› definition populate_occs_inv where ‹populate_occs_inv S xs = (λ(i, occs, cands). all_occurrences (all_init_atms_st S) occs + mset cands ⊆# mset (take i xs) ∩# dom_m (get_clauses_wl S) ∧ distinct cands ∧ fst occs = set_mset (all_init_atms_st S) ∧ correct_occurence_list S occs (mset (drop i xs)) 2 ∧ all_occurrences (all_init_atms_st S) occs ∩# mset cands = {#} ∧ (∀C∈# all_occurrences (all_init_atms_st S) occs. C ∈# dom_m (get_clauses_wl S) ∧ (∀L∈set (get_clauses_wl S ∝ C). undefined_lit (get_trail_wl S) L) ∧ length (get_clauses_wl S ∝ C) = 2) ∧ (∀C∈set cands. C ∈# dom_m (get_clauses_wl S) ∧ length (get_clauses_wl S ∝ C) > 2 ∧ (∀L∈set (get_clauses_wl S ∝ C). undefined_lit (get_trail_wl S) L)))› definition isa_populate_occs_inv where ‹isa_populate_occs_inv S xs = (λ(i, U). (∃T U' occs. (S,T)∈twl_st_heur_restart_occs' (length (get_clauses_wl_heur S)) (learned_clss_count S) ∧ (get_occs U, occs) ∈ occurrence_list_ref ∧ (U,U')∈twl_st_heur_restart_occs' (length (get_clauses_wl_heur S)) (learned_clss_count S) ∧ populate_occs_inv T xs (i, occs, get_tvdom U)))› definition isa_all_lit_clause_unset_pre :: ‹_› where ‹isa_all_lit_clause_unset_pre C S ⟷ (∃T r u. (S,T)∈twl_st_heur_restart_occs' r u ∧ forward_subsumption_all_wl_pre T ∧ C∈set (get_vdom S)) › definition isa_all_lit_clause_unset where ‹isa_all_lit_clause_unset C S = do { ASSERT (isa_all_lit_clause_unset_pre C S); not_garbage ← mop_clause_not_marked_to_delete_heur S C; if ¬not_garbage then RETURN False else do { n ← mop_arena_length_st S C; (i, unset, added) ← WHILE_T (λ(i, unset, _). unset ∧ i < n) (λ(i, unset, added). do { ASSERT (i+1 ≤ Suc (unat32_max div 2)); ASSERT(Suc i ≤ unat32_max); L ← mop_arena_lit2 (get_clauses_wl_heur S) C i; val ← mop_polarity_pol (get_trail_wl_heur S) L; is_added ← mop_is_marked_added_heur_st S (atm_of L); RETURN (i+1, val = None, if is_added then added + 1 else added) }) (0, True, 0::64 word); let a = (added ≥ 2); RETURN (unset ∧ a) } }› definition forward_subsumption_all_wl2_inv :: ‹nat twl_st_wl ⇒ nat list ⇒ nat × _ × _ × nat twl_st_wl × nat × nat multiset ⇒ bool› where ‹forward_subsumption_all_wl2_inv = (λS xs (i, occs, D, s, n, shrunken). (D, {#}) ∈ clause_hash_ref (all_init_atms_st s) ∧ shrunken ⊆# mset (take i xs) ∧ forward_subsumption_all_wl_inv S (mset xs) (mset (drop i xs), s)) › definition sort_cands_by_length where ‹sort_cands_by_length S = do { let tvdom = get_tvdom S; let avdom = get_avdom S; let ivdom = get_ivdom S; let vdom = get_vdom S; ASSERT (∀i∈set tvdom. arena_is_valid_clause_idx (get_clauses_wl_heur S) i); tvdom ← SPEC (λcands'. mset cands' = mset tvdom ∧ sorted_wrt (λa b. arena_length (get_clauses_wl_heur S) a ≤ arena_length (get_clauses_wl_heur S) b) cands'); RETURN (set_aivdom_wl_heur (AIvdom (vdom, avdom, ivdom, tvdom)) S) }› definition push_to_tvdom_st :: ‹nat ⇒ isasat ⇒ isasat nres› where ‹push_to_tvdom_st C S = do { ASSERT (length (get_vdom S) ≤ length (get_clauses_wl_heur S)); ASSERT (length (get_tvdom S) < length (get_clauses_wl_heur S)); let av = get_aivdom S; let av = push_to_tvdom C av; RETURN (set_aivdom_wl_heur av S) }› definition empty_tvdom_st :: ‹isasat ⇒ isasat nres› where ‹empty_tvdom_st S = do { let aivdom = get_aivdom S; let aivdom = empty_tvdom aivdom; RETURN (set_aivdom_wl_heur aivdom S) }› text ‹Using term‹empty_tvdom_st› is mostly laziness: It should actually already be empty, but re-cleaning is not costing much anyhow.› definition isa_populate_occs :: ‹isasat ⇒ _ nres› where ‹isa_populate_occs S = do { ASSERT (length (get_avdom_aivdom (get_aivdom S) @ get_ivdom_aivdom (get_aivdom S)) ≤ length (get_clauses_wl_heur S)); let xs = get_avdom_aivdom (get_aivdom S) @ get_ivdom_aivdom (get_aivdom S); let m = size (get_avdom_aivdom (get_aivdom S)); let n = size xs; let occs = get_occs S; ASSERT (n ≤ length (get_clauses_wl_heur S)); T ← empty_tvdom_st S; (xs, S) ← WHILE_T⇗isa_populate_occs_inv S xs⇖ (λ(i, S). i < n) (λ(i, S). do { ASSERT (i < n); ASSERT (Suc i ≤ length (get_avdom_aivdom (get_aivdom S) @ get_ivdom_aivdom (get_aivdom S))); ASSERT (i < m ⟶ access_avdom_at_pre S i); ASSERT (i ≥ m ⟶ access_ivdom_at_pre S (i - m)); let C = (if i < m then get_avdom_aivdom (get_aivdom S) ! i else get_ivdom_aivdom (get_aivdom S) ! (i-m)); ASSERT (C ∈ set (get_vdom S)); all_undef ← isa_all_lit_clause_unset C S; if ¬all_undef then RETURN (i+1, S) else do { n ← mop_arena_length_st S C; if n = 2 then do { S ← isa_push_to_occs_list_st C S; RETURN (i+1, S) } else do { cand ← isa_is_candidate_forward_subsumption S C; if cand then do {S ← push_to_tvdom_st C S; RETURN (i+1, S)} else RETURN (i+1, S) } } } ) (0, T); T ← sort_cands_by_length S; RETURN T }› definition mop_cch_add_all_clause :: ‹_› where ‹mop_cch_add_all_clause S C D = do { n ← mop_arena_length_st S C; ASSERT (n ≤ length (get_clauses_wl_heur S)); (_, D) ← WHILE_T (λ(i, D). i < n) (λ(i,D). do { ASSERT (i < n); L ← mop_arena_lit2 (get_clauses_wl_heur S) C i; let _ = mark_literal_for_unit_deletion L; D ← mop_cch_add L D; RETURN (i+1, D) }) (0, D); RETURN D }› definition mop_ch_add_all_clause :: ‹_› where ‹mop_ch_add_all_clause S C D = do { ASSERT (C ∈# dom_m (get_clauses_wl S)); let n = length (get_clauses_wl S ∝ C); (_, D) ← WHILE_T (λ(i, D). i < n) (λ(i,D). do { L ← mop_clauses_at (get_clauses_wl S) C i; D ← mop_ch_add L D; RETURN (i+1, D) }) (0, D); RETURN D }› definition empty_occs_st :: ‹isasat ⇒ isasat nres› where ‹empty_occs_st S = do { let D = get_occs S; let D = replicate (length D) []; RETURN (set_occs_wl_heur D S) }› definition empty_occs2 where ‹empty_occs2 occs₀ = do { let n = length occs₀; (_, occs)← WHILE_T (λ(i,occs). i < n) (λ(i,occs). do { ASSERT (i < n ∧ length occs = length occs₀); RETURN (i+1, occs[i := take 0 (occs ! i)]) }) (0, occs₀); RETURN occs }› definition isa_forward_reset_added_and_stats where ‹isa_forward_reset_added_and_stats S = (let S = (set_stats_wl_heur (incr_forward_rounds (get_stats_heur S)) S) in set_heur_wl_heur (reset_added_heur (get_heur S)) S)› definition empty_occs2_st :: ‹isasat ⇒ isasat nres› where ‹empty_occs2_st S = do { let D = get_occs S; D ← empty_occs2 D; RETURN (set_occs_wl_heur D S) }› definition forward_subsumption_finalize :: ‹nat list ⇒ isasat ⇒ isasat nres› where ‹forward_subsumption_finalize shrunken S = do { let S = isa_forward_reset_added_and_stats (schedule_next_subsume_st ((1 + stats_forward_rounds_st S) * 10000) S); _ ← isasat_current_progress 115 S; (_, S) ← WHILE_T(λ(i,S). i < length shrunken) (λ(i,S). do { ASSERT (i < length shrunken); let C = shrunken ! i; not_garbage ← mop_clause_not_marked_to_delete_heur S C; S ← (if not_garbage then mark_added_clause_heur2 S C else RETURN S); RETURN (i+1, S) }) (0, S); empty_occs2_st S }› definition isa_forward_subsumption_all_wl_inv :: ‹_› where ‹isa_forward_subsumption_all_wl_inv R₀ S = (λ(i, D, shrunken, T). ∃R₀' S' T' D' occs' n. (R₀, R₀')∈twl_st_heur_restart_occs' (length (get_clauses_wl_heur R₀)) (learned_clss_count R₀) ∧ (S, S')∈twl_st_heur_restart_occs' (length (get_clauses_wl_heur R₀)) (learned_clss_count R₀) ∧ (T,T')∈twl_st_heur_restart_occs' (length (get_clauses_wl_heur R₀)) (learned_clss_count R₀) ∧ (get_occs T, occs') ∈ occurrence_list_ref ∧ (D, D') ∈ clause_hash ∧ forward_subsumption_all_wl2_inv S' (get_tvdom S) (i, occs', D', T', n, mset shrunken)) › definition isa_forward_subsumption_all :: ‹_ ⇒ _ nres› where ‹isa_forward_subsumption_all = (λS₀. do { ASSERT (isa_forward_subsumption_pre_all S₀); S ← isa_populate_occs S₀; ASSERT (isasat_fast_relaxed S₀ ⟶ isasat_fast_relaxed S); let m = length (get_tvdom S); D ← mop_cch_create (length (get_watched_wl_heur S)); let shrunken = []; (_, D, shrunken, S) ← WHILE_T⇗ isa_forward_subsumption_all_wl_inv S₀ S ⇖ (λ(i, D, shrunken, S). i < m ∧ get_conflict_wl_is_None_heur S) (λ(i, D, shrunken, S). do { ASSERT (i < m); ASSERT (access_tvdom_at_pre S i); let C = get_tvdom S!i; D ← mop_cch_add_all_clause S C D; (D, shrunken, T) ← isa_try_to_forward_subsume_wl2 C D shrunken S; RETURN (i+1, D, shrunken, incr_forward_tried_st T) }) (0, D, shrunken, S); ASSERT (∀C∈set shrunken. C ∈ set (get_vdom S)); forward_subsumption_finalize shrunken S } )› definition isa_forward_subsume :: ‹isasat ⇒ isasat nres› where ‹isa_forward_subsume S = do { let b = should_subsume_st S; if b then isa_forward_subsumption_all S else RETURN S }› end

Theory IsaSAT_Simplify_Forward_Subsumption_Defs