theory IsaSAT_Propagate_Conflict_LLVM
imports IsaSAT_Propagate_Conflict IsaSAT_Inner_Propagation_LLVM
begin
lemma length_ll[def_pat_rules]: ‹length_ll$xs$i ≡ op_list_list_llen$xs$i›
by (auto simp: op_list_list_llen_def length_ll_def)
sepref_def length_ll_fs_heur_fast_code
is ‹uncurry (RETURN oo length_ll_fs_heur)›
:: ‹[λ(S, L). nat_of_lit L < length (get_watched_wl_heur S)]⇩a
isasat_bounded_assn⇧k *⇩a unat_lit_assn⇧k → sint64_nat_assn›
unfolding length_ll_fs_heur_alt_def get_watched_wl_heur_def isasat_bounded_assn_def
length_ll_def[symmetric]
supply [[goals_limit=1]]
by sepref
sepref_def mop_length_watched_by_int_impl [llvm_inline]
is ‹uncurry mop_length_watched_by_int›
:: ‹isasat_bounded_assn⇧k *⇩a unat_lit_assn⇧k →⇩a sint64_nat_assn›
unfolding mop_length_watched_by_int_alt_def isasat_bounded_assn_def
length_ll_def[symmetric]
supply [[goals_limit=1]]
by sepref
sepref_register unit_propagation_inner_loop_body_wl_heur
lemma unit_propagation_inner_loop_wl_loop_D_heur_fast:
‹length (get_clauses_wl_heur b) ≤ sint64_max ⟹
unit_propagation_inner_loop_wl_loop_D_heur_inv b a (a1', a1'a, a2'a) ⟹
length (get_clauses_wl_heur a2'a) ≤ sint64_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) ≤ sint64_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]
length_ll_fs_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_uint64_max_minus_4_uint64_max: ‹a ≤ sint64_max - 4 ⟹ Suc a < max_snat 64›
by (auto simp: sint64_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 (M, N, D, Q, W, oth). do {
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 (M, N, D, Q, W, oth)
})›
unfolding cut_watch_list_heur2_inv_def cut_watch_list_heur2_def
by auto
lemma cut_watch_list_heur2I:
‹length (a1'd ! nat_of_lit baa) ≤ sint64_max - 4 ⟹
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) ≤ sint64_max - 4 ⟹
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 sint64_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) ≤ sint64_max-4]⇩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 isasat_bounded_assn_def length_ll_def[symmetric]
nth_rll_def[symmetric]
op_list_list_take_alt_def[symmetric]
op_list_list_upd_alt_def[symmetric]
unfolding fold_tuple_optimizations
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) ≤ sint64_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
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_bounded_assn_def
unfolding fold_tuple_optimizations
supply [[goals_limit = 1]]
apply (annot_snat_const "TYPE (64)")
by sepref
sepref_def literals_to_update_wl_literals_to_update_wl_empty_fast_code
is ‹RETURN o literals_to_update_wl_literals_to_update_wl_empty›
:: ‹[λS. isa_length_trail_pre (get_trail_wl_heur S)]⇩a isasat_bounded_assn⇧k → bool1_assn›
unfolding literals_to_update_wl_literals_to_update_wl_empty_alt_def
isasat_bounded_assn_def
by sepref
sepref_register literals_to_update_wl_literals_to_update_wl_empty
select_and_remove_from_literals_to_update_wl_heur
lemma unit_propagation_outer_loop_wl_D_heur_fast:
‹length (get_clauses_wl_heur x) ≤ sint64_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') ≤ sint64_max›
by (auto simp: unit_propagation_outer_loop_wl_D_heur_inv_def)
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) ≤ sint64_max]⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
supply [[goals_limit=1]] unit_propagation_outer_loop_wl_D_heur_fast[intro]
unit_propagation_outer_loop_wl_D_invI[intro]
unfolding unit_propagation_outer_loop_wl_D_heur_def
literals_to_update_wl_literals_to_update_wl_empty_def[symmetric]
by sepref
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
literals_to_update_wl_literals_to_update_wl_empty_fast_code
unit_propagation_outer_loop_wl_D_fast_code
end
end