Theory IsaSAT_Restart_Reduce

theory IsaSAT_Restart_Reduce_Defs imports IsaSAT_Restart_Defs IsaSAT_Bump_Heuristics begin text ‹ We first fix the function that proves termination. We don't take the ``smallest'' function possible (other possibilites that are growing slower include term‹λ(n::nat). n >> 50›). › definition (in -) find_local_restart_target_level_int_inv where ‹find_local_restart_target_level_int_inv bmp cs = (λ(brk, i). i ≤ length cs ∧ length cs < unat32_max)› (*TODO fix*) definition find_local_restart_target_level_int :: ‹trail_pol ⇒ bump_heuristics ⇒ nat nres› where ‹find_local_restart_target_level_int = (λ(M, xs, lvls, reasons, k, cs, zeored) bmp. do { let m = current_vmtf_array_nxt_score bmp; (brk, i) ← WHILE_T⇗find_local_restart_target_level_int_inv bmp cs⇖ (λ(brk, i). ¬brk ∧ i < length cs) (λ(brk, i). do { ASSERT (i < length cs); let t = (cs ! i); ASSERT(t < length M); let L = atm_of (M ! t); u ← access_focused_vmtf_array bmp L; let brk = stamp u < m; RETURN (brk, if brk then i else i+1) }) (False, 0); RETURN i })› text ‹term‹find_decomp_wl_st_int› is the wrong function here, because unlike in the backtrack case, we also have to update the queue of literals to update. This is done in the function term‹empty_Q›. › definition find_local_restart_target_level_st :: ‹isasat ⇒ nat nres› where ‹find_local_restart_target_level_st S = do { find_local_restart_target_level_int (get_trail_wl_heur S) (get_vmtf_heur S) }› definition cdcl_twl_local_restart_wl_D_heur :: ‹isasat ⇒ isasat nres› where ‹cdcl_twl_local_restart_wl_D_heur = (λS. do { ASSERT(restart_abs_wl_heur_pre S False); lvl ← find_local_restart_target_level_st S; b ← RETURN (lvl = count_decided_st_heur S); if b then RETURN S else do { S ← find_decomp_wl_st_int lvl S; S ← empty_Q S; incr_restart_stat S } } )› definition reorder_vdom_wl :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where ‹reorder_vdom_wl S = do { ASSERT (mark_to_delete_clauses_wl_pre S); RETURN S }› definition sort_clauses_by_score :: ‹arena ⇒ isasat_aivdom ⇒ isasat_aivdom nres› where ‹sort_clauses_by_score arena vdom = do { ASSERT(∀i∈set (get_vdom_aivdom vdom). valid_sort_clause_score_pre_at arena i); ASSERT(∀i∈set (get_avdom_aivdom vdom). valid_sort_clause_score_pre_at arena i); ASSERT(∀i∈set (get_tvdom_aivdom vdom). valid_sort_clause_score_pre_at arena i); SPEC(λvdom'. mset (get_vdom_aivdom vdom) = mset (get_vdom_aivdom vdom') ∧ mset (get_avdom_aivdom vdom) = mset (get_avdom_aivdom vdom') ∧ mset (get_ivdom_aivdom vdom) = mset (get_ivdom_aivdom vdom') ∧ mset (get_tvdom_aivdom vdom) = mset (get_tvdom_aivdom vdom')) }› definition (in -) quicksort_clauses_by_score_avdom :: ‹arena ⇒ vdom ⇒ vdom nres› where ‹quicksort_clauses_by_score_avdom arena = (full_quicksort_ref clause_score_ordering (clause_score_extract arena))› definition remove_deleted_clauses_from_avdom_inv :: ‹_› where ‹remove_deleted_clauses_from_avdom_inv N avdom0 = (λ(i, j, avdom). i ≤ j ∧ j ≤ length (get_avdom_aivdom avdom0) ∧ length (get_avdom_aivdom avdom) = length (get_avdom_aivdom avdom0) ∧ mset (take i (get_avdom_aivdom avdom) @ drop j (get_avdom_aivdom avdom)) ⊆# mset (get_avdom_aivdom avdom0) ∧ mset (take i (get_avdom_aivdom avdom) @ drop j (get_avdom_aivdom avdom)) ∩# dom_m N = mset (get_avdom_aivdom avdom0) ∩# dom_m N ∧ get_vdom_aivdom avdom = get_vdom_aivdom avdom0 ∧ get_ivdom_aivdom avdom = get_ivdom_aivdom avdom0 ∧ distinct (get_tvdom_aivdom avdom) ∧ set (get_tvdom_aivdom avdom) ⊆ set (take i (get_avdom_aivdom avdom)) ∧ length (get_tvdom_aivdom avdom) ≤ i ∧ (∀C ∈ set (get_tvdom_aivdom avdom). C ∈# dom_m N ∧ ¬irred N C ∧ length (N ∝ C) ≠ 2))› definition is_candidate_for_removal where ‹is_candidate_for_removal C N = do { ASSERT (C ∈# dom_m N); SPEC (λb :: bool. b ⟶ ¬irred N C ∧ length (N ∝ C) ≠ 2) }› definition remove_deleted_clauses_from_avdom :: ‹_› where ‹remove_deleted_clauses_from_avdom N avdom0 = do { let n = length (get_avdom_aivdom avdom0); let avdom0' = get_avdom_aivdom avdom0; (i, j, avdom) ← WHILE_T⇗ remove_deleted_clauses_from_avdom_inv N avdom0⇖ (λ(i, j, avdom). j < n) (λ(i, j, avdom). do { ASSERT(j < length (get_avdom_aivdom avdom)); if (get_avdom_aivdom avdom ! j) ∈# dom_m N then do { let C = get_avdom_aivdom avdom ! j; let avdom = swap_avdom_aivdom avdom i j; should_push ← is_candidate_for_removal C N; if should_push then RETURN (i+1, j+1, push_to_tvdom C avdom) else RETURN (i+1, j+1, avdom) } else RETURN (i, j+1, avdom) }) (0, 0, empty_tvdom avdom0); ASSERT(i ≤ length (get_avdom_aivdom avdom)); RETURN (take_avdom_aivdom i avdom) }› definition isa_is_candidate_for_removal where ‹isa_is_candidate_for_removal M C arena = do { ASSERT(arena_act_pre arena C); L ← mop_arena_lit arena C; lbd ← mop_arena_lbd arena C; length ← mop_arena_length arena C; status ← mop_arena_status arena C; used ← mop_marked_as_used arena C; D ← get_the_propagation_reason_pol M L; let can_del = lbd > MINIMUM_DELETION_LBD ∧ status = LEARNED ∧ length ≠ 2 ∧ used = 0 ∧ (D ≠ Some C); RETURN can_del }› definition isa_gather_candidates_for_reduction :: ‹trail_pol ⇒ arena ⇒ _ ⇒ (arena × _) nres› where ‹isa_gather_candidates_for_reduction M arena avdom0 = do { ASSERT(length (get_avdom_aivdom avdom0) ≤ length arena); ASSERT(length (get_avdom_aivdom avdom0) ≤ length (get_vdom_aivdom avdom0)); let n = length (get_avdom_aivdom avdom0); (arena, i, j, avdom) ← WHILE_T⇗ λ(_, i, j, _). i ≤ j ∧ j ≤ n⇖ (λ(arena, i, j, avdom). j < n) (λ(arena, i, j, avdom). do { ASSERT(j < n); ASSERT(arena_is_valid_clause_vdom arena (get_avdom_aivdom avdom!j) ∧ j < length (get_avdom_aivdom avdom) ∧ i < length (get_avdom_aivdom avdom)); ASSERT (length (get_tvdom_aivdom avdom) ≤ i); if arena_status arena (get_avdom_aivdom avdom ! j) ≠ DELETED then do{ ASSERT(arena_act_pre arena (get_avdom_aivdom avdom ! j)); should_push ← isa_is_candidate_for_removal M (get_avdom_aivdom avdom ! j) arena; let arena = mark_unused arena (get_avdom_aivdom avdom ! j); if should_push then RETURN (arena, i+1, j+1, push_to_tvdom (get_avdom_aivdom avdom ! j) (swap_avdom_aivdom avdom i j)) else RETURN (arena, i+1, j+1, swap_avdom_aivdom avdom i j) } else RETURN (arena, i, j+1, avdom) }) (arena, 0, 0, empty_tvdom avdom0); ASSERT(i ≤ length (get_avdom_aivdom avdom)); RETURN (arena, take_avdom_aivdom i avdom) }› definition (in -) sort_vdom_heur :: ‹isasat ⇒ isasat nres› where ‹sort_vdom_heur = (λS. do { let vdom = get_aivdom S; let M' = get_trail_wl_heur S; let arena = get_clauses_wl_heur S; ASSERT(length (get_avdom_aivdom vdom) ≤ length arena); ASSERT(length (get_vdom_aivdom vdom) ≤ length arena); (arena', vdom) ← isa_gather_candidates_for_reduction M' arena vdom; ASSERT(valid_sort_clause_score_pre arena (get_vdom_aivdom vdom)); ASSERT(EQ (length arena) (length arena')); ASSERT(length (get_avdom_aivdom vdom) ≤ length arena); vdom ← sort_clauses_by_score arena' vdom; RETURN (set_clauses_wl_heur arena' (set_aivdom_wl_heur vdom S)) })› definition partition_main_clause where ‹partition_main_clause arena = partition_main clause_score_ordering (clause_score_extract arena)› definition partition_clause where ‹partition_clause arena = partition_between_ref clause_score_ordering (clause_score_extract arena)› definition mark_to_delete_clauses_wl_D_heur_pre :: ‹isasat ⇒ bool› where ‹mark_to_delete_clauses_wl_D_heur_pre S ⟷ (∃S'. (S, S') ∈ twl_st_heur_restart ∧ mark_to_delete_clauses_wl_pre S')› definition find_largest_lbd_and_size :: ‹nat ⇒ isasat ⇒ (nat × nat) nres› where ‹find_largest_lbd_and_size = (λl S. do { ASSERT(length (get_tvdom S) ≤ length (get_clauses_wl_heur S)); (i, lbd, sze) ← WHILE_T⇗λ(i, _ :: nat, _::nat). i ≤ length (get_tvdom S)⇖ (λ(i, lbd, sze). i < l ∧ i < length (get_tvdom S)) (λ(i, lbd, sze). do { ASSERT(i < length (get_tvdom S)); ASSERT(access_tvdom_at_pre S i); let C = get_tvdom S ! i; ASSERT(clause_not_marked_to_delete_heur_pre (S, C)); b ← mop_clause_not_marked_to_delete_heur S C; if ¬b then RETURN (i+1, lbd, sze) else do { lbd2 ← mop_arena_lbd_st S C; sze' ← mop_arena_length_st S C; RETURN (i+1, max lbd (lbd2), max sze sze') } }) (0, 0 :: nat , 0 :: nat); RETURN (lbd, sze) })› definition mark_to_delete_clauses_wl_D_heur :: ‹isasat ⇒ isasat nres› where ‹mark_to_delete_clauses_wl_D_heur = (λS0. do { ASSERT(mark_to_delete_clauses_wl_D_heur_pre S0); S ← sort_vdom_heur S0; l ← number_clss_to_keep S; (lbd, sze) ← find_largest_lbd_and_size l S; ASSERT(length (get_tvdom S) ≤ length (get_clauses_wl_heur S0)); (i, T) ← WHILE_T⇗λ_. True⇖ (λ(i, S). i < length (get_tvdom S)) (λ(i, T). do { ASSERT(i < length (get_tvdom T)); ASSERT(access_tvdom_at_pre T i); let C = get_tvdom T ! i; ASSERT(clause_not_marked_to_delete_heur_pre (T, C)); b ← mop_clause_not_marked_to_delete_heur T C; if ¬b then RETURN (i, delete_index_vdom_heur i T) else do { ASSERT(access_lit_in_clauses_heur_pre ((T, C), 0)); ASSERT(length (get_clauses_wl_heur T) ≤ length (get_clauses_wl_heur S0)); ASSERT(length (get_tvdom T) ≤ length (get_clauses_wl_heur T)); L ← mop_access_lit_in_clauses_heur T C 0; D ← get_the_propagation_reason_pol (get_trail_wl_heur T) L; length ← mop_arena_length (get_clauses_wl_heur T) C; let can_del = (D ≠ Some C) ∧ length ≠ 2; if can_del then do { wasted ← mop_arena_length_st T C; _ ← log_del_clause_heur T C; T ← mop_mark_garbage_heur3 C i (incr_wasted_st (of_nat wasted) T); RETURN (i, T) } else do { RETURN (i+1, T) } } }) (l, S); ASSERT(length (get_tvdom T) ≤ length (get_clauses_wl_heur S0)); incr_reduction_stat (set_stats_size_limit_st lbd sze T) })› definition mark_to_delete_clauses_GC_wl_D_heur_pre :: ‹isasat ⇒ bool› where ‹mark_to_delete_clauses_GC_wl_D_heur_pre S ⟷ (∃S'. (S, S') ∈ twl_st_heur_restart ∧ mark_to_delete_clauses_GC_wl_pre S')› text ‹ The duplication is unfortunate. The only difference is the precondition. › definition mark_to_delete_clauses_GC_wl_D_heur :: ‹isasat ⇒ isasat nres› where ‹mark_to_delete_clauses_GC_wl_D_heur = (λS0. do { ASSERT(mark_to_delete_clauses_GC_wl_D_heur_pre S0); S ← sort_vdom_heur S0; l ← number_clss_to_keep S; (lbd, sze) ← find_largest_lbd_and_size l S; ASSERT(length (get_tvdom S) ≤ length (get_clauses_wl_heur S0)); (i, T) ← WHILE_T⇗λ_. True⇖ (λ(i, S). i < length (get_tvdom S)) (λ(i, T). do { ASSERT(i < length (get_tvdom T)); ASSERT(access_tvdom_at_pre T i); let C = get_tvdom T ! i; ASSERT(clause_not_marked_to_delete_heur_pre (T, C)); b ← mop_clause_not_marked_to_delete_heur T C; if ¬b then RETURN (i, delete_index_vdom_heur i T) else do { ASSERT(access_lit_in_clauses_heur_pre ((T, C), 0)); ASSERT(length (get_clauses_wl_heur T) ≤ length (get_clauses_wl_heur S0)); ASSERT(length (get_tvdom T) ≤ length (get_clauses_wl_heur T)); length ← mop_arena_length (get_clauses_wl_heur T) C; let can_del = length ≠ 2; if can_del then do { wasted ← mop_arena_length_st T C; _ ← log_del_clause_heur T C; T ← mop_mark_garbage_heur3 C i (incr_wasted_st (of_nat wasted) T); RETURN (i, T) } else do { RETURN (i+1, T) } } }) (l, S); ASSERT(length (get_tvdom T) ≤ length (get_clauses_wl_heur S0)); incr_restart_stat (set_stats_size_limit_st lbd sze T) })› definition reduceint :: ‹64 word› where ‹reduceint = 1000› text ‹Approximatively @{term ‹sqrt(p)›} is @{term ‹2^((word_log2 p) >> 1)›}› definition schedule_next_reduction_st :: ‹isasat ⇒ isasat› where ‹schedule_next_reduction_st S = (let (delta :: 64 word) = 1 + 2 << (word_log2 (max 1 (get_reductions_count S)) >> 1); delta = delta * reduceint; irred = (get_irredundant_count_st S) >> 10; extra = if irred < 10 then 1 else of_nat (word_log2 (irred)) >> 1; delta = extra * delta in schedule_next_reduce_st delta S)› definition cdcl_twl_mark_clauses_to_delete where ‹cdcl_twl_mark_clauses_to_delete S = do { _ ← ASSERT (mark_to_delete_clauses_wl_D_heur_pre S); _ ← RETURN (IsaSAT_Profile.start_reduce); T ← mark_to_delete_clauses_wl_D_heur S; _ ← RETURN (IsaSAT_Profile.stop_reduce); RETURN (schedule_next_reduction_st (clss_size_resetUS0_st T)) }› (*TODO deduplicate*) definition cdcl_twl_restart_wl_heur where ‹cdcl_twl_restart_wl_heur S = do { cdcl_twl_local_restart_wl_D_heur S }› definition isasat_GC_clauses_prog_copy_wl_entry :: ‹arena ⇒ (nat watcher) list list ⇒ nat literal ⇒ (arena × isasat_aivdom) ⇒ (arena × (arena × isasat_aivdom)) nres› where ‹isasat_GC_clauses_prog_copy_wl_entry = (λN0 W A (N', aivdom). do { ASSERT(nat_of_lit A < length W); ASSERT(length (W ! nat_of_lit A) ≤ length N0); let le = length (W ! nat_of_lit A); (i, N, N', aivdom) ← WHILE_T (λ(i, N, N', aivdom). i < le) (λ(i, N, (N', aivdom)). do { ASSERT(i < length (W ! nat_of_lit A)); let C = fst (W ! nat_of_lit A ! i); ASSERT(arena_is_valid_clause_vdom N C); let st = arena_status N C; if st ≠ DELETED then do { ASSERT(arena_is_valid_clause_idx N C); ASSERT(length N' + (if arena_length N C > 4 then MAX_HEADER_SIZE else MIN_HEADER_SIZE) + arena_length N C ≤ length N0); ASSERT(length N = length N0); ASSERT(length (get_vdom_aivdom aivdom) < length N0); ASSERT(length (get_avdom_aivdom aivdom) < length N0); ASSERT(length (get_ivdom_aivdom aivdom) < length N0); ASSERT(length (get_tvdom_aivdom aivdom) < length N0); let D = length N' + (if arena_length N C > 4 then MAX_HEADER_SIZE else MIN_HEADER_SIZE); N' ← fm_mv_clause_to_new_arena C N N'; ASSERT(mark_garbage_pre (N, C)); RETURN (i+1, extra_information_mark_to_delete N C, N', (if st = LEARNED then add_learned_clause_aivdom_strong D aivdom else add_init_clause_aivdom_strong D aivdom)) } else RETURN (i+1, N, (N', aivdom)) }) (0, N0, (N', aivdom)); RETURN (N, (N', aivdom)) })› definition isasat_GC_clauses_prog_single_wl :: ‹arena ⇒ (arena × isasat_aivdom) ⇒ (nat watcher) list list ⇒ nat ⇒ (arena × (arena × isasat_aivdom) × (nat watcher) list list) nres› where ‹isasat_GC_clauses_prog_single_wl = (λN0 N' WS A. do { let L = Pos A; ⌦‹use phase saving instead› ASSERT(nat_of_lit L < length WS); ASSERT(nat_of_lit (-L) < length WS); (N, (N', aivdom)) ← isasat_GC_clauses_prog_copy_wl_entry N0 WS L N'; let WS = WS[nat_of_lit L := []]; ASSERT(length N = length N0); (N, N') ← isasat_GC_clauses_prog_copy_wl_entry N WS (-L) (N', aivdom); let WS = WS[nat_of_lit (-L) := []]; RETURN (N, N', WS) })› definition isasat_GC_clauses_prog_wl2 where ‹isasat_GC_clauses_prog_wl2 ≡ (λ(ns :: bump_heuristics) x0. do { (_, x) ← WHILE_T⇗λ(n, x). length (fst x) = length (fst x0)⇖ (λ(n, _). n ≠ None) (λ(n, x). do { ASSERT(n ≠ None); let A = the n; ASSERT (A < length_bumped_vmtf_array ns); ASSERT(A ≤ unat32_max div 2); x ← (λ(arena_o, arena, W). isasat_GC_clauses_prog_single_wl arena_o arena W A) x; n ← access_focused_vmtf_array ns A; RETURN (get_next n, x) }) (Some (bumped_vmtf_array_fst ns), x0); RETURN x })› definition isasat_GC_clauses_prog_wl :: ‹isasat ⇒ isasat nres› where ‹isasat_GC_clauses_prog_wl = (λS. do { let vm = get_vmtf_heur S; let N' = get_clauses_wl_heur S; let W' = get_watched_wl_heur S; let vdom = get_aivdom S; let old_arena = get_old_arena S; ASSERT(old_arena = []); (N, (N', vdom), WS) ← isasat_GC_clauses_prog_wl2 vm (N', (old_arena, empty_aivdom vdom), W'); let S = set_watched_wl_heur WS S; let S = set_clauses_wl_heur N' S; let S = set_old_arena_wl_heur (take 0 N) S; let S = set_vmtf_wl_heur vm S; let S = set_stats_wl_heur (incr_GC (get_stats_heur S)) S; let S = set_aivdom_wl_heur vdom S; let heur = get_heur S; let heur = heuristic_reluctant_untrigger (set_zero_wasted heur); let S = set_heur_wl_heur heur S; RETURN S })› definition isasat_GC_clauses_pre_wl_D :: ‹isasat ⇒ bool› where ‹isasat_GC_clauses_pre_wl_D S ⟷ ( ∃T. (S, T) ∈ twl_st_heur_restart ∧ cdcl_GC_clauses_pre_wl T )› definition isasat_GC_clauses_wl_D :: ‹bool ⇒ isasat ⇒ isasat nres› where ‹isasat_GC_clauses_wl_D = (λinprocessing S. do { ASSERT(isasat_GC_clauses_pre_wl_D S); let b = True; if b then do { T ← isasat_GC_clauses_prog_wl S; ASSERT(length (get_clauses_wl_heur T) ≤ length (get_clauses_wl_heur S)); ASSERT(∀i ∈ set (get_tvdom T). i < length (get_clauses_wl_heur S)); U ← rewatch_heur_and_reorder_st (empty_US_heur T); RETURN U } else RETURN S})› end

Theory IsaSAT_Restart_Reduce_Defs