theory IsaSAT_Inner_Propagation_LLVM
imports IsaSAT_Setup_LLVM
IsaSAT_Inner_Propagation
begin
sepref_register isa_save_pos
sepref_def isa_save_pos_fast_code
is ‹uncurry2 isa_save_pos›
:: ‹sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
supply
[[goals_limit=1]]
if_splits[split]
unfolding isa_save_pos_def PR_CONST_def isasat_bounded_assn_def
by sepref
lemma [def_pat_rules]: ‹nth_rll ≡ op_list_list_idx›
by (auto simp: nth_rll_def intro!: ext eq_reflection)
sepref_def watched_by_app_heur_fast_code
is ‹uncurry2 (RETURN ooo watched_by_app_heur)›
:: ‹[watched_by_app_heur_pre]⇩a
isasat_bounded_assn⇧k *⇩a unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k → watcher_fast_assn›
supply [[goals_limit=1]]
unfolding watched_by_app_heur_alt_def isasat_bounded_assn_def nth_rll_def[symmetric]
watched_by_app_heur_pre_def
by sepref
sepref_register isa_find_unwatched_wl_st_heur isa_find_unwatched_between isa_find_unset_lit
polarity_pol
sepref_register 0 1
sepref_def isa_find_unwatched_between_fast_code
is ‹uncurry4 isa_find_unset_lit›
:: ‹[λ((((M, N), _), _), _). length N ≤ sint64_max]⇩a
trail_pol_fast_assn⇧k *⇩a arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k →
snat_option_assn' TYPE(64)›
supply [[goals_limit = 3]]
unfolding isa_find_unset_lit_def isa_find_unwatched_between_def SET_FALSE_def[symmetric]
PR_CONST_def
apply (rewrite in ‹if ⌑ then _ else _› tri_bool_eq_def[symmetric])
apply (annot_snat_const "TYPE (64)")
by sepref
sepref_register mop_arena_pos mop_arena_lit2
sepref_def mop_arena_pos_impl
is ‹uncurry mop_arena_pos›
:: ‹arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a sint64_nat_assn›
unfolding mop_arena_pos_def
by sepref
sepref_def swap_lits_impl is "uncurry3 mop_arena_swap"
:: "sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a arena_fast_assn⇧d →⇩a arena_fast_assn"
unfolding mop_arena_swap_def swap_lits_pre_def
unfolding gen_swap
by sepref
sepref_def find_unwatched_wl_st_heur_fast_code
is ‹uncurry isa_find_unwatched_wl_st_heur›
:: ‹[(λ(S, C). length (get_clauses_wl_heur S) ≤ sint64_max)]⇩a
isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k → snat_option_assn' TYPE(64)›
supply [[goals_limit = 1]] isasat_fast_def[simp]
unfolding isa_find_unwatched_wl_st_heur_def PR_CONST_def
find_unwatched_def fmap_rll_def[symmetric] isasat_bounded_assn_def
length_uint32_nat_def[symmetric] isa_find_unwatched_def
case_tri_bool_If find_unwatched_wl_st_heur_pre_def
fmap_rll_u64_def[symmetric]
apply (subst isa_find_unset_lit_def[symmetric])
apply (subst isa_find_unset_lit_def[symmetric])
apply (subst isa_find_unset_lit_def[symmetric])
apply (annot_snat_const "TYPE (64)")
unfolding fold_tuple_optimizations
by sepref
sepref_register mop_access_lit_in_clauses_heur mop_watched_by_app_heur
sepref_def mop_access_lit_in_clauses_heur_impl
is ‹uncurry2 mop_access_lit_in_clauses_heur›
:: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a unat_lit_assn›
supply [[goals_limit=1]]
unfolding mop_access_lit_in_clauses_heur_alt_def isasat_bounded_assn_def
by sepref
lemma other_watched_wl_heur_alt_def:
‹other_watched_wl_heur = (λS. arena_other_watched (get_clauses_wl_heur S))›
apply (intro ext)
unfolding other_watched_wl_heur_def
arena_other_watched_def
mop_access_lit_in_clauses_heur_def
by auto argo
lemma other_watched_wl_heur_alt_def2:
‹other_watched_wl_heur = (λ(_, N, _). arena_other_watched N)›
by (auto intro!: ext simp: other_watched_wl_heur_alt_def)
sepref_def other_watched_wl_heur_impl
is ‹uncurry3 other_watched_wl_heur›
:: ‹isasat_bounded_assn⇧k *⇩a unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a
unat_lit_assn›
supply [[goals_limit=1]]
unfolding other_watched_wl_heur_alt_def2
isasat_bounded_assn_def
by sepref
sepref_register update_clause_wl_heur
setup ‹map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")›
lemma arena_lit_pre_le2: ‹
arena_lit_pre a i ⟹ length a ≤ sint64_max ⟹ i < max_snat 64›
using arena_lifting(7)[of a _ _] unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def sint64_max_def max_snat_def
by fastforce
lemma sint64_max_le_max_snat64: ‹a < sint64_max ⟹ Suc a < max_snat 64›
by (auto simp: max_snat_def sint64_max_def)
sepref_def update_clause_wl_fast_code
is ‹uncurry7 update_clause_wl_heur›
:: ‹[λ(((((((L, C), b), j), w), i), f), S). length (get_clauses_wl_heur S) ≤ sint64_max]⇩a
unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a bool1_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a
sint64_nat_assn⇧k
*⇩a isasat_bounded_assn⇧d → sint64_nat_assn ×⇩a sint64_nat_assn ×⇩a isasat_bounded_assn›
supply [[goals_limit=1]] arena_lit_pre_le2[intro] swap_lits_pre_def[simp]
sint64_max_le_max_snat64[intro]
unfolding update_clause_wl_heur_def isasat_bounded_assn_def
fmap_rll_def[symmetric] delete_index_and_swap_update_def[symmetric]
delete_index_and_swap_ll_def[symmetric] fmap_swap_ll_def[symmetric]
append_ll_def[symmetric] update_clause_wl_code_pre_def
fmap_rll_u64_def[symmetric]
fmap_swap_ll_u64_def[symmetric]
fmap_swap_ll_def[symmetric]
PR_CONST_def mop_arena_lit2'_def
apply (annot_snat_const "TYPE (64)")
unfolding fold_tuple_optimizations
by sepref
sepref_register mop_arena_swap
sepref_def propagate_lit_wl_fast_code
is ‹uncurry3 propagate_lit_wl_heur›
:: ‹[λ(((L, C), i), S). length (get_clauses_wl_heur S) ≤ sint64_max]⇩a
unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
unfolding PR_CONST_def propagate_lit_wl_heur_def
supply [[goals_limit=1]] swap_lits_pre_def[simp]
unfolding update_clause_wl_heur_def isasat_bounded_assn_def
propagate_lit_wl_heur_pre_def fmap_swap_ll_def[symmetric]
fmap_swap_ll_u64_def[symmetric]
save_phase_def
apply (rewrite at ‹count_decided_pol _ = ⌑› unat_const_fold[where 'a=32])
apply (annot_snat_const "TYPE (64)")
unfolding fold_tuple_optimizations
by sepref
sepref_def propagate_lit_wl_bin_fast_code
is ‹uncurry2 propagate_lit_wl_bin_heur›
:: ‹[λ((L, C), S). length (get_clauses_wl_heur S) ≤ sint64_max]⇩a
unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d →
isasat_bounded_assn›
unfolding PR_CONST_def propagate_lit_wl_heur_def
supply [[goals_limit=1]] length_ll_def[simp]
unfolding update_clause_wl_heur_def isasat_bounded_assn_def
propagate_lit_wl_heur_pre_def fmap_swap_ll_def[symmetric]
fmap_swap_ll_u64_def[symmetric]
save_phase_def propagate_lit_wl_bin_heur_def
apply (rewrite at ‹count_decided_pol _ = ⌑› unat_const_fold[where 'a=32])
unfolding fold_tuple_optimizations
by sepref
lemma op_list_list_upd_alt_def: ‹op_list_list_upd xss i j x = xss[i := (xss ! i)[j := x]]›
unfolding op_list_list_upd_def by auto
sepref_def update_blit_wl_heur_fast_code
is ‹uncurry6 update_blit_wl_heur›
:: ‹[λ((((((_, _), _), _), C), i), S). length (get_clauses_wl_heur S) ≤ sint64_max]⇩a
unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a bool1_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a
sint64_nat_assn⇧k *⇩a unat_lit_assn⇧k *⇩a isasat_bounded_assn⇧d →
sint64_nat_assn ×⇩a sint64_nat_assn ×⇩a isasat_bounded_assn›
supply [[goals_limit=1]] sint64_max_le_max_snat64[intro]
unfolding update_blit_wl_heur_def isasat_bounded_assn_def append_ll_def[symmetric]
op_list_list_upd_alt_def[symmetric]
apply (annot_snat_const "TYPE (64)")
by sepref
sepref_register keep_watch_heur
lemma op_list_list_take_alt_def: ‹op_list_list_take xss i l = xss[i := take l (xss ! i)]›
unfolding op_list_list_take_def by auto
sepref_def keep_watch_heur_fast_code
is ‹uncurry3 keep_watch_heur›
:: ‹unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
supply
[[goals_limit=1]]
unfolding keep_watch_heur_def PR_CONST_def
unfolding fmap_rll_def[symmetric] isasat_bounded_assn_def
unfolding
op_list_list_upd_alt_def[symmetric]
nth_rll_def[symmetric]
SET_FALSE_def[symmetric] SET_TRUE_def[symmetric]
by sepref
sepref_register isa_set_lookup_conflict_aa set_conflict_wl_heur
sepref_register arena_incr_act
sepref_def set_conflict_wl_heur_fast_code
is ‹uncurry set_conflict_wl_heur›
:: ‹[λ(C, S).
length (get_clauses_wl_heur S) ≤ sint64_max]⇩a
sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
supply [[goals_limit=1]]
unfolding set_conflict_wl_heur_def isasat_bounded_assn_def
set_conflict_wl_heur_pre_def PR_CONST_def
apply (annot_unat_const "TYPE (32)")
unfolding fold_tuple_optimizations
by sepref
sepref_register update_blit_wl_heur clause_not_marked_to_delete_heur
lemma mop_watched_by_app_heur_alt_def:
‹mop_watched_by_app_heur = (λ(M, N, D, Q, W, vmtf, φ, clvls, cach, lbd, outl, stats, fema, sema) L K. do {
ASSERT(K < length (W ! nat_of_lit L));
ASSERT(nat_of_lit L < length (W));
RETURN (W ! nat_of_lit L ! K)})›
by (intro ext; rename_tac S L K; case_tac S)
(auto simp: mop_watched_by_app_heur_def)
sepref_def mop_watched_by_app_heur_code
is ‹uncurry2 mop_watched_by_app_heur›
:: ‹isasat_bounded_assn⇧k *⇩a unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a watcher_fast_assn›
unfolding mop_watched_by_app_heur_alt_def isasat_bounded_assn_def
nth_rll_def[symmetric]
by sepref
lemma unit_propagation_inner_loop_wl_loop_D_heur_inv0D: ‹unit_propagation_inner_loop_wl_loop_D_heur_inv0 L (j, w, S0) ⟹
j ≤ length (get_clauses_wl_heur S0) - 4 ∧ w ≤ length (get_clauses_wl_heur S0) - 4›
unfolding unit_propagation_inner_loop_wl_loop_D_heur_inv0_def prod.case
unit_propagation_inner_loop_wl_loop_inv_def unit_propagation_inner_loop_l_inv_def
apply normalize_goal+
by (simp only: twl_st_l twl_st twl_st_wl
ℒ⇩a⇩l⇩l_all_atms_all_lits) linarith
sepref_def pos_of_watched_heur_impl
is ‹uncurry2 pos_of_watched_heur›
:: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a unat_lit_assn⇧k →⇩a sint64_nat_assn›
supply [[goals_limit=1]]
unfolding pos_of_watched_heur_def
apply (annot_snat_const "TYPE (64)")
by sepref
sepref_def unit_propagation_inner_loop_body_wl_fast_heur_code
is ‹uncurry3 unit_propagation_inner_loop_body_wl_heur›
:: ‹[λ((L, w), S). length (get_clauses_wl_heur S) ≤ sint64_max]⇩a
unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d →
sint64_nat_assn ×⇩a sint64_nat_assn ×⇩a isasat_bounded_assn›
supply [[goals_limit=1]]
if_splits[split] sint64_max_le_max_snat64[intro] unit_propagation_inner_loop_wl_loop_D_heur_inv0D[dest!]
unfolding unit_propagation_inner_loop_body_wl_heur_def PR_CONST_def
unfolding fmap_rll_def[symmetric]
unfolding option.case_eq_if is_None_alt[symmetric]
SET_FALSE_def[symmetric] SET_TRUE_def[symmetric] tri_bool_eq_def[symmetric]
apply (annot_snat_const "TYPE (64)")
by sepref
sepref_register unit_propagation_inner_loop_body_wl_heur
lemmas [llvm_inline] =
other_watched_wl_heur_impl_def
pos_of_watched_heur_impl_def
propagate_lit_wl_heur_def
clause_not_marked_to_delete_heur_fast_code_def
mop_watched_by_app_heur_code_def
keep_watch_heur_fast_code_def
nat_of_lit_rel_impl_def
experiment begin
export_llvm
isa_save_pos_fast_code
watched_by_app_heur_fast_code
isa_find_unwatched_between_fast_code
find_unwatched_wl_st_heur_fast_code
update_clause_wl_fast_code
propagate_lit_wl_fast_code
propagate_lit_wl_bin_fast_code
status_neq_impl
clause_not_marked_to_delete_heur_fast_code
update_blit_wl_heur_fast_code
keep_watch_heur_fast_code
set_conflict_wl_heur_fast_code
unit_propagation_inner_loop_body_wl_fast_heur_code
end
end