Theory IsaSAT_Propagate_Conflict

theory IsaSAT_Propagate_Conflict_LLVM imports IsaSAT_Propagate_Conflict_Defs IsaSAT_Inner_Propagation_LLVM begin (*TODO Move*) lemma unit_propagation_inner_loop_wl_loop_D_heur_fast: ‹length (get_clauses_wl_heur b) ≤ snat64_max ⟹ unit_propagation_inner_loop_wl_loop_D_heur_inv b a (a1', a1'a, a2'a) ⟹ length (get_clauses_wl_heur a2'a) ≤ snat64_max› unfolding unit_propagation_inner_loop_wl_loop_D_heur_inv_def by auto sepref_def unit_propagation_inner_loop_wl_loop_D_fast is ‹uncurry unit_propagation_inner_loop_wl_loop_D_heur› :: ‹[λ(L, S). length (get_clauses_wl_heur S) ≤ snat64_max]_a unat_lit_assn^k *_a isasat_bounded_assn^d → sint64_nat_assn ×_a sint64_nat_assn ×_a isasat_bounded_assn› unfolding unit_propagation_inner_loop_wl_loop_D_heur_def PR_CONST_def unfolding watched_by_nth_watched_app watched_app_def[symmetric] length_ll_fs_heur_def[symmetric] unfolding delete_index_and_swap_update_def[symmetric] append_update_def[symmetric] is_None_def[symmetric] get_conflict_wl_is_None_heur_alt_def[symmetric] unfolding fold_tuple_optimizations supply [[goals_limit=1]] unit_propagation_inner_loop_wl_loop_D_heur_fast[intro] length_ll_fs_heur_def[simp] apply (annot_snat_const ‹TYPE (64)›) by sepref lemma le_unat64_max_minus_4_unat64_max: ‹a ≤ snat64_max - MIN_HEADER_SIZE ⟹ Suc a < max_snat 64› by (auto simp: snat64_max_def max_snat_def) definition cut_watch_list_heur2_inv where ‹cut_watch_list_heur2_inv L n = (λ(j, w, W). j ≤ w ∧ w ≤ n ∧ nat_of_lit L < length W)› lemma cut_watch_list_heur2_alt_def: ‹cut_watch_list_heur2 = (λj w L S₀. do { let (W, S) = extract_watchlist_wl_heur S₀; ASSERT (W = get_watched_wl_heur S₀); ASSERT(j ≤ length (W ! nat_of_lit L) ∧ j ≤ w ∧ nat_of_lit L < length W ∧ w ≤ length (W ! (nat_of_lit L))); let n = length (W!(nat_of_lit L)); (j, w, W) ← WHILE_T⇗cut_watch_list_heur2_inv L n⇖ (λ(j, w, W). w < n) (λ(j, w, W). do { ASSERT(w < length (W!(nat_of_lit L))); RETURN (j+1, w+1, W[nat_of_lit L := (W!(nat_of_lit L))[j := W!(nat_of_lit L)!w]]) }) (j, w, W); ASSERT(j ≤ length (W ! nat_of_lit L) ∧ nat_of_lit L < length W); let W = W[nat_of_lit L := take j (W ! nat_of_lit L)]; RETURN (update_watchlist_wl_heur W S) })› unfolding cut_watch_list_heur2_inv_def cut_watch_list_heur2_def by (auto simp: state_extractors Let_def intro!: ext split: isasat_int_splits) lemma cut_watch_list_heur2I: ‹length (a1'd ! nat_of_lit baa) ≤ snat64_max - MIN_HEADER_SIZE ⟹ cut_watch_list_heur2_inv baa (length (a1'd ! nat_of_lit baa)) (a1'e, a1'f, a2'f) ⟹ a1'f < length_ll a2'f (nat_of_lit baa) ⟹ ez ≤ bba ⟹ Suc a1'e < max_snat 64› ‹length (a1'd ! nat_of_lit baa) ≤ snat64_max - MIN_HEADER_SIZE ⟹ cut_watch_list_heur2_inv baa (length (a1'd ! nat_of_lit baa)) (a1'e, a1'f, a2'f) ⟹ a1'f < length_ll a2'f (nat_of_lit baa) ⟹ ez ≤ bba ⟹ Suc a1'f < max_snat 64› ‹cut_watch_list_heur2_inv baa (length (a1'd ! nat_of_lit baa)) (a1'e, a1'f, a2'f) ⟹ nat_of_lit baa < length a2'f› ‹cut_watch_list_heur2_inv baa (length (a1'd ! nat_of_lit baa)) (a1'e, a1'f, a2'f) ⟹ a1'f < length_ll a2'f (nat_of_lit baa) ⟹ a1'e < length (a2'f ! nat_of_lit baa)› by (auto simp: max_snat_def snat64_max_def cut_watch_list_heur2_inv_def length_ll_def) sepref_def cut_watch_list_heur2_fast_code is ‹uncurry3 cut_watch_list_heur2› :: ‹[λ(((j, w), L), S). length (watched_by_int S L) ≤ snat64_max-MIN_HEADER_SIZE]_a sint64_nat_assn^k *_a sint64_nat_assn^k *_a unat_lit_assn^k *_a isasat_bounded_assn^d → isasat_bounded_assn› supply [[goals_limit=1]] cut_watch_list_heur2I[intro] length_ll_def[simp] unfolding cut_watch_list_heur2_alt_def length_ll_def[symmetric] nth_rll_def[symmetric] watched_by_alt_def op_list_list_take_alt_def[symmetric] op_list_list_upd_alt_def[symmetric] apply (annot_snat_const ‹TYPE (64)›) by sepref sepref_def unit_propagation_inner_loop_wl_D_fast_code is ‹uncurry unit_propagation_inner_loop_wl_D_heur› :: ‹[λ(L, S). length (get_clauses_wl_heur S) ≤ snat64_max]_a unat_lit_assn^k *_a isasat_bounded_assn^d → isasat_bounded_assn› supply [[goals_limit=1]] unfolding PR_CONST_def unit_propagation_inner_loop_wl_D_heur_def by sepref lemma [sepref_fr_rules]: ‹(Mreturn o Tuple17_get_d, RETURN o literals_to_update_wl_heur) ∈ isasat_bounded_assn^k →_a sint64_nat_assn› supply [split] = isasat_int_splits unfolding isasat_bounded_assn_def by sepref_to_hoare vcg' lemma select_and_remove_from_literals_to_update_wl_heur_alt_def: ‹select_and_remove_from_literals_to_update_wl_heur S = do { ASSERT(literals_to_update_wl_heur S < length (fst (get_trail_wl_heur S))); ASSERT(literals_to_update_wl_heur S + 1 ≤ unat32_max); let (j, T) = extract_literals_to_update_wl_heur S; ASSERT (j = literals_to_update_wl_heur S); L ← isa_trail_nth (get_trail_wl_heur T) j; RETURN (update_literals_to_update_wl_heur (j + 1) T, -L) }› by (cases S) (auto simp: select_and_remove_from_literals_to_update_wl_heur_def state_extractors intro!: ext split: isasat_int_splits) sepref_def select_and_remove_from_literals_to_update_wlfast_code is ‹select_and_remove_from_literals_to_update_wl_heur› :: ‹isasat_bounded_assn^d →_a isasat_bounded_assn ×_a unat_lit_assn› supply [[goals_limit=1]] unfolding select_and_remove_from_literals_to_update_wl_heur_alt_def isasat_trail_nth_st_def[symmetric] unfolding fold_tuple_optimizations supply [[goals_limit = 1]] apply (annot_snat_const ‹TYPE (64)›) by sepref lemma unit_propagation_outer_loop_wl_D_heur_fast: ‹length (get_clauses_wl_heur x) ≤ snat64_max ⟹ unit_propagation_outer_loop_wl_D_heur_inv x s' ⟹ length (get_clauses_wl_heur a1') = length (get_clauses_wl_heur s') ⟹ length (get_clauses_wl_heur s') ≤ snat64_max› by (auto simp: unit_propagation_outer_loop_wl_D_heur_inv_def) lemma unit_propagation_outer_loop_wl_D_invI: ‹unit_propagation_outer_loop_wl_D_heur_inv S₀ S ⟹ isa_length_trail_pre (get_trail_wl_heur S)› unfolding unit_propagation_outer_loop_wl_D_heur_inv_def by blast sepref_def unit_propagation_outer_loop_wl_D_fast_code is ‹unit_propagation_outer_loop_wl_D_heur› :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max]_a isasat_bounded_assn^d → isasat_bounded_assn› supply [[goals_limit=1]] unit_propagation_outer_loop_wl_D_heur_fast[intro] of_nat_snat[sepref_import_param] unit_propagation_outer_loop_wl_D_invI[intro] unfolding unit_propagation_outer_loop_wl_D_heur_def isasat_length_trail_st_def[symmetric] by sepref sepref_register unit_propagation_outer_loop_wl_D_heur experiment begin export_llvm length_ll_fs_heur_fast_code unit_propagation_inner_loop_wl_loop_D_fast cut_watch_list_heur2_fast_code unit_propagation_inner_loop_wl_D_fast_code isa_trail_nth_fast_code select_and_remove_from_literals_to_update_wlfast_code unit_propagation_outer_loop_wl_D_fast_code end end

Theory IsaSAT_Propagate_Conflict_LLVM