Theory IsaSAT_Simplify_Forward_Subsumption_LLVM
theory IsaSAT_Simplify_Forward_Subsumption_LLVM
imports
IsaSAT_Simplify_Forward_Subsumption_Defs
IsaSAT_Setup_LLVM
IsaSAT_Trail_LLVM
IsaSAT_Proofs_LLVM
IsaSAT_Arena_Sorting_LLVM
IsaSAT_Show_LLVM
IsaSAT_LBD_LLVM
begin
lemma incr_forward_subsumed_st_alt_def: ‹incr_forward_subsumed_st S = (
let (stats, S) = extract_stats_wl_heur S; stats = incr_forward_subsumed stats in
update_stats_wl_heur stats S
)› and
incr_forward_strengthened_st_alt_def: ‹incr_forward_strengthened_st S = (
let (stats, S) = extract_stats_wl_heur S; stats = incr_forward_strengethening stats in
update_stats_wl_heur stats S
)› and
incr_forward_tried_st_alt_def: ‹incr_forward_tried_st S = (
let (stats, S) = extract_stats_wl_heur S; stats = incr_forward_tried stats in
update_stats_wl_heur stats S
)› and
incr_forward_rounds_st_alt_def: ‹incr_forward_rounds_st S = (
let (stats, S) = extract_stats_wl_heur S; stats = incr_forward_rounds stats in
update_stats_wl_heur stats S
)› and
isa_forward_reset_added_and_stats_alt_def: ‹isa_forward_reset_added_and_stats S = (
let (stats, S) = extract_stats_wl_heur S;
(heur, S) = extract_heur_wl_heur S;
stats = incr_forward_rounds stats;
heur = reset_added_heur heur in
update_stats_wl_heur stats (update_heur_wl_heur heur S))›
by (auto simp: isa_push_to_occs_list_st_def state_extractors incr_forward_subsumed_st_def
incr_forward_strengthened_st_def incr_forward_tried_st_def incr_forward_rounds_st_def
isa_forward_reset_added_and_stats_def
split: isasat_int_splits)
sepref_def incr_forward_strengthened_st_impl
is ‹RETURN o incr_forward_strengthened_st›
:: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
unfolding incr_forward_strengthened_st_alt_def
by sepref
sepref_def incr_forward_tried_st_impl
is ‹RETURN o incr_forward_tried_st›
:: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
unfolding incr_forward_tried_st_alt_def
by sepref
sepref_def incr_forward_rounds_st_impl
is ‹RETURN o incr_forward_rounds_st›
:: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
unfolding incr_forward_rounds_st_alt_def
by sepref
sepref_def incr_forward_subsumed_st_impl
is ‹RETURN o incr_forward_subsumed_st›
:: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
unfolding incr_forward_subsumed_st_alt_def
by sepref
sepref_def isa_forward_reset_added_and_stats_impl
is ‹RETURN o isa_forward_reset_added_and_stats›
:: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
unfolding isa_forward_reset_added_and_stats_alt_def
by sepref
sepref_register incr_forward_subsumed_st incr_forward_strengthened_st incr_forward_rounds_st incr_forward_tried_st
isa_forward_reset_added_and_stats
definition clause_size_sort_clauses_raw :: ‹arena ⇒ vdom ⇒ nat ⇒ nat ⇒ nat list nres› where
‹clause_size_sort_clauses_raw arena N = pslice_sort_spec idx_clause_cdom clause_size_less arena N›
definition clause_size_sort_clauses_avdom :: ‹arena ⇒ vdom ⇒ nat list nres› where
‹clause_size_sort_clauses_avdom arena N = clause_size_sort_clauses_raw arena N 0 (length N)›
lemmas Size_Ordering_introsort[sepref_fr_rules] =
Size_Ordering_it.introsort_param_impl_correct[unfolded clause_size_sort_clauses_raw_def[symmetric] PR_CONST_def]
sepref_register clause_size_sort_clauses_raw
sepref_def clause_size_sort_clauses_avdom_impl
is ‹uncurry clause_size_sort_clauses_avdom›
:: ‹arena_fast_assn⇧k *⇩a vdom_fast_assn⇧d →⇩a vdom_fast_assn›
supply[[goals_limit=1]]
unfolding clause_size_sort_clauses_avdom_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
definition clause_size_sort_clauses :: ‹arena ⇒ aivdom2 ⇒ aivdom2 nres› where
‹clause_size_sort_clauses arena N = map_tvdom_aivdom_int (clause_size_sort_clauses_avdom arena) N›
sepref_def clause_size_sort_clauses_impl
is ‹uncurry clause_size_sort_clauses›
:: ‹arena_fast_assn⇧k *⇩a aivdom_int_assn⇧d →⇩a aivdom_int_assn›
unfolding clause_size_sort_clauses_def map_tvdom_aivdom_int_def
by sepref
lemma
map_vdom_aivdom_int2:
‹(uncurry (λarena. map_vdom_aivdom_int (f arena)), uncurry (λarena. map_vdom_aivdom (f arena)))
∈ Id ×⇩r aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel›
apply (intro frefI nres_relI)
subgoal for x y
using map_vdom_aivdom_int[of ‹f (fst x)›]
apply (cases x; cases y)
apply (auto intro!: frefI nres_relI simp: fref_def nres_rel_def)
done
done
lemma get_aivdom_eq_aivdom_iff:
‹IsaSAT_VDom.get_aivdom b = (x1, a, aa, ba) ⟷ b = AIvdom (x1, a, aa, ba)›
by (cases b) auto
hide_const (open) NEMonad.ASSERT NEMonad.RETURN NEMonad.ASSERT NEMonad.SPEC
definition sort_cands_by_length2 :: ‹_ ⇒ isasat_aivdom ⇒ isasat_aivdom nres› where
‹sort_cands_by_length2 arena avdom = do {
ASSERT (∀i∈set (get_tvdom_aivdom avdom). arena_is_valid_clause_idx arena i);
SPEC (λcands'.
mset (get_tvdom_aivdom cands') = mset (get_tvdom_aivdom avdom) ∧
(get_avdom_aivdom cands') = (get_avdom_aivdom avdom) ∧
(get_ivdom_aivdom cands') = (get_ivdom_aivdom avdom) ∧
(get_vdom_aivdom cands') = (get_vdom_aivdom avdom) ∧
sorted_wrt (λa b. arena_length arena a ≤ arena_length arena b) (get_tvdom_aivdom cands'))
}›
lemma quicksort_clauses_by_score_sort:
‹(uncurry clause_size_sort_clauses, uncurry sort_cands_by_length2) ∈
Id ×⇩r aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel›
apply (intro fun_relI nres_relI frefI)
subgoal for arena arena'
unfolding uncurry_def sort_cands_by_length2_def map_tvdom_aivdom_int_def
clause_size_sort_clauses_def clause_size_sort_clauses_avdom_def
clause_size_sort_clauses_raw_def pslice_sort_spec_def nres_monad3
apply (refine_vcg)
subgoal for x1 x2 x1a x2a x1b x2b x1c x2c
by (cases x2) (auto simp: idx_clause_cdom_def code_hider_rel_def)
subgoal for x1 x2 x1a x2a x1b x2b x1c x2c
apply (rule specify_left)
apply (rule order_trans)
apply (rule slice_sort_spec_refine_sort)
apply (auto simp:
pslice_sort_spec_def le_ASSERT_iff idx_cdom_def slice_rel_def br_def uncurry_def
conc_fun_RES sort_spec_def map_vdom_aivdom_int_def
code_hider_rel_def
split:prod.splits
simp del: slice_complete
intro!: ASSERT_leI
)
subgoal for x1d x
using slice_complete[of x]
apply (rule_tac x = ‹AIvdom (x1d, x1b, x1c, x)› in exI)
apply (case_tac x2; auto simp: clause_size_less_def slice_complete
le_by_lt_def)
unfolding le_by_lt_def
apply (auto simp: clause_size_less_def
intro!: arg_cong[of ‹(λa b. ¬ arena_length x1 b < arena_length x1 a)› ‹(λa b. arena_length x1 a ≤ arena_length x1 b)› ‹λa. sorted_wrt a x›, THEN iffD1]ext
)
done
done
done
done
context
notes [fcomp_norm_unfold] = aivdom_assn_alt_def[symmetric] aivdom_assn_def[symmetric]
begin
lemma clause_size_sort_clauses_impl_sort_cands_by_length2[sepref_fr_rules]:
‹(uncurry clause_size_sort_clauses_impl, uncurry sort_cands_by_length2)
∈ (al_assn arena_el_impl_assn)⇧k *⇩a aivdom_assn⇧d →⇩a aivdom_assn›
(is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
have H: ‹?c
∈ [comp_PRE (Id ×⇩f aivdom_rel) (λ_. True) (λx y. True)
(λx. nofail (uncurry sort_cands_by_length2 x))]⇩a ?im → ?f›
(is ‹_ ∈ [?pre']⇩a ?im' → _›)
using hfref_compI_PRE[OF clause_size_sort_clauses_impl.refine,
OF quicksort_clauses_by_score_sort, unfolded fcomp_norm_unfold] by blast
have pre: ‹?pre' x› if ‹?pre x› for x
using that
by (case_tac x, case_tac ‹snd x›)
(auto simp: comp_PRE_def code_hider_rel_def)
show ?thesis
apply (rule hfref_weaken_pre[OF ])
defer
using H apply assumption
using pre ..
qed
end
lemma sort_cands_by_length_alt_def:
‹sort_cands_by_length S⇩0 = do {
let (aivdom, S) = extract_vdom_wl_heur S⇩0;
ASSERT (aivdom = get_aivdom S⇩0);
let (arena, S) = extract_arena_wl_heur S;
ASSERT (arena = get_clauses_wl_heur S⇩0);
aivdom ← sort_cands_by_length2 arena aivdom;
let S = update_arena_wl_heur arena S;
let S = update_vdom_wl_heur aivdom S;
RETURN S
}›
apply (auto simp: sort_cands_by_length_def sort_cands_by_length2_def state_extractors Let_def RES_RETURN_RES image_iff
intro!: bind_cong[OF refl]
split: isasat_int_splits)
apply (case_tac xb)
apply auto
done
sepref_def sort_cands_by_length_impl
is sort_cands_by_length
:: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
unfolding sort_cands_by_length_alt_def
by sepref
sepref_register mop_is_marked_added_heur_st
sepref_def isa_all_lit_clause_unset_impl
is ‹uncurry isa_all_lit_clause_unset›
:: ‹sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧k →⇩a bool1_assn›
supply [[goals_limit=1]]
unfolding isa_all_lit_clause_unset_def
mop_access_lit_in_clauses_heur_def[symmetric] mop_polarity_st_heur_def[symmetric]
tri_bool_eq_def[symmetric] UNSET_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma rdomp_aivdom_assn_length_avdomD: ‹rdomp aivdom_assn x ⟹ length (get_avdom_aivdom x) < max_snat 64›
unfolding isasat_bounded_assn_def
apply (cases x)
apply (auto simp: isasat_bounded_assn_def snat64_max_def max_snat_def length_avdom_def
aivdom_assn_def code_hider_assn_def hr_comp_def code_hider_rel_def
split: isasat_int_splits
dest: al_assn_boundD[of sint64_nat_assn] mod_starD)
done
lemma rdomp_isasat_bounded_assn_length_avdomD:
‹rdomp isasat_bounded_assn x ⟹ length_avdom x < max_snat 64›
using rdomp_aivdom_assn_length_avdomD[of ‹get_aivdom x›] apply -
unfolding isasat_bounded_assn_def rdomp_def
apply normalize_goal+
by (cases x)
(force simp: isasat_bounded_assn_def length_avdom_def
split: isasat_int_splits
dest!: rdomp_aivdom_assn_length_avdomD mod_starD)
sepref_register isa_all_lit_clause_unset isa_push_to_occs_list_st
find_best_subsumption_candidate find_best_subsumption_candidate_and_push sort_cands_by_length
sepref_def find_best_subsumption_candidate_code
is ‹uncurry find_best_subsumption_candidate›
:: ‹sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧k →⇩a unat_lit_assn›
supply [[goals_limit=1]]
unfolding find_best_subsumption_candidate_def
mop_access_lit_in_clauses_heur_def[symmetric]
tri_bool_eq_def[symmetric] UNSET_def[symmetric]
length_occs_def[symmetric]
get_occs_list_at_def[symmetric]
length_occs_at_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma isa_push_to_occs_list_st_alt_def:
‹isa_push_to_occs_list_st C S = do {
L ← find_best_subsumption_candidate C S;
let (occs, T) = extract_occs_wl_heur S;
ASSERT (length (occs ! nat_of_lit L) < length (get_clauses_wl_heur S));
occs ← mop_cocc_list_append C occs L;
RETURN (update_occs_wl_heur occs T)
}›
by (auto simp: isa_push_to_occs_list_st_def state_extractors
split: isasat_int_splits)
sepref_register mop_cocc_list_append
sepref_def mop_cocc_list_append_impl
is ‹uncurry2 mop_cocc_list_append›
:: ‹[λ((C,occs), L). Suc (length (occs ! nat_of_lit L)) < max_snat 64]⇩a
sint64_nat_assn⇧k *⇩a occs_assn⇧d *⇩a unat_lit_assn⇧k → occs_assn›
unfolding mop_cocc_list_append_def cocc_list_append_pre_def cocc_list_append_def
fold_op_list_list_push_back
by sepref
lemma empty_tvdom_st_alt_def:
‹empty_tvdom_st S = do {
let (aivdom, S) = extract_vdom_wl_heur S;
let aivdom = empty_tvdom aivdom;
RETURN (update_vdom_wl_heur aivdom S)
}›
by (auto simp: isa_push_to_occs_list_st_def state_extractors empty_tvdom_st_def
split: isasat_int_splits)
sepref_def empty_tvdom_st_impl
is empty_tvdom_st
:: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
supply [[goals_limit=1]]
unfolding empty_tvdom_st_alt_def
by sepref
sepref_register empty_tvdom_st
sepref_def isa_push_to_occs_list_st_impl
is ‹uncurry isa_push_to_occs_list_st›
:: ‹[λ(_, S). isasat_fast_relaxed S]⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
unfolding isa_push_to_occs_list_st_alt_def isasat_fast_relaxed_def
by sepref
sepref_def find_best_subsumption_candidate_and_push_code
is ‹uncurry find_best_subsumption_candidate_and_push›
:: ‹sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧k →⇩a unat_lit_assn ×⇩a bool1_assn›
supply [[goals_limit=1]]
unfolding find_best_subsumption_candidate_and_push_def
mop_access_lit_in_clauses_heur_def[symmetric]
tri_bool_eq_def[symmetric] UNSET_def[symmetric]
length_occs_def[symmetric]
get_occs_list_at_def[symmetric]
mop_is_marked_added_heur_st_def[symmetric]
length_occs_at_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma isa_maybe_push_to_occs_list_st_alt_def:
‹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 (occs, T) = extract_occs_wl_heur S;
ASSERT (length (occs ! nat_of_lit L) < length (get_clauses_wl_heur S));
occs ← mop_cocc_list_append C occs L;
RETURN (update_occs_wl_heur occs T)
} else RETURN S
}›
unfolding isa_maybe_push_to_occs_list_st_def Let_def
by (auto simp: state_extractors cong: if_cong split: isasat_int_splits)
sepref_def isa_maybe_push_to_occs_list_st_impl
is ‹uncurry isa_maybe_push_to_occs_list_st›
:: ‹[λ(_, S). isasat_fast_relaxed S]⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
unfolding isa_maybe_push_to_occs_list_st_alt_def isasat_fast_relaxed_def
by sepref
lemmas [sepref_fr_rules] = arena_get_lbd.mop_refine
sepref_def isa_is_candidate_forward_subsumption_impl
is ‹uncurry isa_is_candidate_forward_subsumption›
:: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a bool1_assn›
unfolding isa_is_candidate_forward_subsumption_def
mop_access_lit_in_clauses_heur_def[symmetric]
mop_is_marked_added_heur_st_def[symmetric]
mop_arena_lbd_st_def[symmetric]
mop_arena_length_st_def[symmetric]
mop_arena_status_st_def[symmetric]
UNSET_def[symmetric] tri_bool_eq_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma push_to_tvdom_st_alt_def:
‹push_to_tvdom_st C S = do {
let (av, T) = extract_vdom_wl_heur S;
ASSERT (length (get_vdom_aivdom av) ≤ length (get_clauses_wl_heur S));
ASSERT (length (get_tvdom_aivdom av) < length (get_clauses_wl_heur S));
let av = push_to_tvdom C av;
RETURN (update_vdom_wl_heur av T)
}›
by (auto simp: isa_push_to_occs_list_st_def state_extractors push_to_tvdom_st_def
split: isasat_int_splits)
sepref_def push_to_tvdom_st_impl
is ‹uncurry push_to_tvdom_st›
:: ‹[λ(_, S). isasat_fast_relaxed S]⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
supply [[goals_limit=1]]
unfolding push_to_tvdom_st_alt_def isasat_fast_relaxed_def
by sepref
lemma isa_populate_occs_inv_isasat_fast_relaxedI:
‹isa_populate_occs_inv x cands (a1', a2') ⟹ isasat_fast_relaxed x ⟹ isasat_fast_relaxed a2'›
by (auto simp: isa_populate_occs_inv_def isasat_fast_relaxed_def)
sepref_def isa_populate_occs_code
is isa_populate_occs
:: ‹[isasat_fast_relaxed]⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
supply [[goals_limit=1]]
supply [dest] = rdomp_isasat_bounded_assn_length_avdomD isasat_bounded_assn_length_arenaD
supply [intro] = isa_populate_occs_inv_isasat_fast_relaxedI
unfolding isa_populate_occs_def access_avdom_at_def[symmetric] length_avdom_def[symmetric] length_ivdom_def[symmetric]
al_fold_custom_empty[where 'l=64] Let_def[of ‹get_avdom _ @ get_ivdom _›] Let_def[of ‹get_occs _›]
Let_def[of ‹get_tvdom _›] nth_append length_append access_ivdom_at_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_register isa_forward_subsumption_all isa_populate_occs
sepref_register mop_cch_create mop_cch_add_all_clause mop_cch_add mop_cch_in
abbreviation cch_assn where
‹cch_assn ≡ IICF_Array.array_assn bool1_assn›
sepref_def mop_cch_create_impl
is mop_cch_create
:: ‹sint64_nat_assn⇧k →⇩a cch_assn›
unfolding mop_cch_create_def op_list_replicate_def[symmetric] array_fold_custom_replicate
by sepref
sepref_def mop_cch_add_impl
is ‹uncurry mop_cch_add›
:: ‹unat_lit_assn⇧k *⇩a cch_assn⇧d →⇩a cch_assn›
unfolding mop_cch_add_def cch_add_def cch_add_pre_def
by sepref
sepref_def mop_cch_in_impl
is ‹uncurry mop_cch_in›
:: ‹unat_lit_assn⇧k *⇩a cch_assn⇧k →⇩a bool1_assn›
unfolding mop_cch_in_def cch_in_def cch_in_pre_def
by sepref
sepref_def mop_cch_add_all_clause_impl
is ‹uncurry2 mop_cch_add_all_clause›
:: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a cch_assn⇧d →⇩a cch_assn›
unfolding mop_cch_add_all_clause_def
mop_access_lit_in_clauses_heur_def[symmetric]
supply [dest] = isasat_bounded_assn_length_arenaD
supply [[goals_limit=1]]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_register isa_try_to_forward_subsume_wl2
sepref_def isa_try_to_forward_subsume_wl2_break_impl
is isa_try_to_forward_subsume_wl2_break
:: ‹isasat_bounded_assn⇧k →⇩a bool1_assn›
unfolding isa_try_to_forward_subsume_wl2_break_def
by sepref
sepref_register isa_try_to_forward_subsume_wl2_break
definition subsumption_rel :: ‹('c × nat) set
⇒ ('b × 'd literal) set ⇒ ('c × nat) set ⇒ ((3 word × 'b × _) × 'd subsumption) set› where
subsumption_rel_internal_def: ‹subsumption_rel R1 R2 R3 = {((tag, x, y),b).
case b of NONE ⇒ tag = 0
| SUBSUMED_BY x' ⇒ (y, x') ∈ R1 ∧ tag = 1
| STRENGTHENED_BY x' y' ⇒ (x, x') ∈ R2 ∧ (y, y') ∈ R3 ∧ tag = 2}›
lemma subsumption_rel_def: ‹⟨R1,R2,R3⟩subsumption_rel = {((tag, x, y),b).
case b of NONE ⇒ tag = 0
| SUBSUMED_BY x' ⇒ (y, x') ∈ R1 ∧ tag = 1
| STRENGTHENED_BY x' y' ⇒ (x, x') ∈ R2 ∧ (y, y') ∈ R3 ∧ tag = 2}›
unfolding subsumption_rel_internal_def relAPP_def by auto
definition is_NONE where
‹is_NONE x ⟷ NONE = x›
lemma is_subsumption:
‹(λ(tag, _). tag = 0, is_NONE) ∈ ⟨R1,R2,R3⟩subsumption_rel → bool_rel›
‹(λ(tag, _). tag = 1, is_subsumed) ∈ ⟨R1,R2,R3⟩subsumption_rel → bool_rel›
‹(λ(tag, _). tag = 2, is_strengthened) ∈ ⟨R1,R2,R3⟩subsumption_rel → bool_rel›
‹((0, 0, 0), NONE) ∈ ⟨R1,R2,R3⟩subsumption_rel›
‹(λC. (1, 0, C), SUBSUMED_BY) ∈ R1 → ⟨R1,R2,R3⟩subsumption_rel›
‹(λC D. (2, C, D), STRENGTHENED_BY) ∈ R2 → R3 → ⟨R1,R2,R3⟩subsumption_rel›
‹(λ(tag, C, D). D, subsumed_by) ∈ [is_subsumed]⇩f ⟨R1,R2,R3⟩subsumption_rel → R1›
‹(λ(tag, C, D). D, strengthened_by) ∈ [is_strengthened]⇩f ⟨R1,R2,R3⟩subsumption_rel → R3›
‹(λ(tag, C, D). C, strengthened_on_lit) ∈ [is_strengthened]⇩f ⟨R1,R2,R3⟩subsumption_rel → R2›
unfolding subsumption_rel_def
by (auto simp: IS_LEFT_UNIQUE_def single_valued_def is_NONE_def
intro!: frefI
split: subsumption.splits)
abbreviation subsumption_raw_assn where
‹subsumption_raw_assn ≡ word_assn' TYPE(3) ×⇩a word_assn ×⇩a id_assn›
definition subsumption_assn where
‹subsumption_assn = hr_comp subsumption_raw_assn (⟨snat_rel' TYPE(64), unat_lit_rel,snat_rel' TYPE(64)⟩subsumption_rel)›
sepref_definition is_NONE_impl
is ‹RETURN o (λ(tag, _). tag = 0)›
:: ‹subsumption_raw_assn⇧k →⇩a bool1_assn›
by sepref
sepref_definition is_subsumed_impl
is ‹RETURN o (λ(tag, _). tag = 1)›
:: ‹subsumption_raw_assn⇧k →⇩a bool1_assn›
by sepref
sepref_definition is_strengthened_impl
is ‹RETURN o (λ(tag, _). tag = 2)›
:: ‹subsumption_raw_assn⇧k →⇩a bool1_assn›
by sepref
sepref_definition STRENGTHENED_BY_impl
is ‹uncurry (RETURN oo (λC D. (2, C, D)))›
:: ‹word_assn⇧k *⇩a id_assn⇧k →⇩a subsumption_raw_assn›
by sepref
sepref_definition SUBSUMED_BY_impl
is ‹RETURN o (λC. (1, 0, C))›
:: ‹word_assn⇧k →⇩a subsumption_raw_assn›
by sepref
sepref_definition NONE_impl
is ‹uncurry0 (RETURN (0, 0, 0::64 word))›
:: ‹unit_assn⇧k →⇩a subsumption_raw_assn›
by sepref
sepref_definition subsumed_by_impl
is ‹RETURN o (λ(tag, C, D). D)›
:: ‹subsumption_raw_assn⇧k →⇩a id_assn›
by sepref
sepref_definition strengthened_on_lit_impl
is ‹RETURN o (λ(tag, C, D). C)›
:: ‹subsumption_raw_assn⇧k →⇩a word_assn›
by sepref
sepref_register is_NONE is_subsumed is_strengthened STRENGTHENED_BY SUBSUMED_BY NONE subsumed_by strengthened_by strengthened_on_lit
lemmas [sepref_fr_rules] =
is_NONE_impl.refine[FCOMP is_subsumption(1), of ‹snat_rel' TYPE(64)› ‹unat_lit_rel› ‹snat_rel' TYPE(64)›, unfolded subsumption_assn_def[symmetric] is_NONE_def[symmetric]]
is_subsumed_impl.refine[FCOMP is_subsumption(2), of ‹snat_rel' TYPE(64)› ‹unat_lit_rel› ‹snat_rel' TYPE(64)›, unfolded subsumption_assn_def[symmetric]]
is_strengthened_impl.refine[FCOMP is_subsumption(3), of ‹snat_rel' TYPE(64)› ‹unat_lit_rel› ‹snat_rel' TYPE(64)›, unfolded subsumption_assn_def[symmetric]]
SUBSUMED_BY_impl.refine[FCOMP is_subsumption(5), of ‹snat_assn' TYPE(64)› unat_lit_rel ‹snat_rel' TYPE(64)›, unfolded the_pure_pure subsumption_assn_def[symmetric]]
STRENGTHENED_BY_impl.refine[FCOMP is_subsumption(6), of unat_lit_assn ‹snat_assn' TYPE(64)› ‹snat_rel' TYPE(64)›, unfolded the_pure_pure subsumption_assn_def[symmetric]]
NONE_impl.refine[FCOMP is_subsumption(4), of ‹snat_rel' TYPE(64)› unat_lit_rel ‹snat_rel' TYPE(64)›, unfolded the_pure_pure subsumption_assn_def[symmetric]]
subsumed_by_impl.refine[FCOMP is_subsumption(7), of ‹snat_assn' TYPE(64)› unat_lit_rel ‹snat_rel' TYPE(64)›, unfolded the_pure_pure subsumption_assn_def[symmetric]]
subsumed_by_impl.refine[FCOMP is_subsumption(8), of ‹snat_assn' TYPE(64)› ‹snat_rel' TYPE(64)› unat_lit_rel, unfolded the_pure_pure subsumption_assn_def[symmetric]]
strengthened_on_lit_impl.refine[FCOMP is_subsumption(9), of unat_lit_assn ‹snat_rel' TYPE(64)› ‹snat_rel' TYPE(64)›, unfolded the_pure_pure subsumption_assn_def[symmetric]]
lemma fold_is_NONE: ‹x = NONE ⟷ is_NONE x› ‹NONE = x ⟷ is_NONE x›
by (auto simp: is_NONE_def)
lemma isa_subsume_clauses_match2_alt_def:
‹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 {mop_free st; RETURN (i+1, STRENGTHENED_BY L C')}
else do {mop_free st; RETURN (i+1, NONE)}
else do {mop_free st; RETURN (i+1, NONE)}
}})
(0, SUBSUMED_BY C');
RETURN st
}›
unfolding isa_subsume_clauses_match2_def mop_free_def bind_to_let_conv Let_def
by auto
schematic_goal mk_free_lbd_assn[sepref_frame_free_rules]: ‹MK_FREE subsumption_assn ?fr›
unfolding subsumption_assn_def by synthesize_free+
lemma [safe_constraint_rules]: ‹CONSTRAINT is_pure subsumption_assn›
unfolding subsumption_assn_def by auto
sepref_register isa_subsume_clauses_match2
sepref_def isa_subsume_clauses_match2_impl
is ‹uncurry3 isa_subsume_clauses_match2›
:: ‹sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧k *⇩a cch_assn⇧k →⇩a subsumption_assn›
unfolding isa_subsume_clauses_match2_alt_def fold_is_NONE
mop_access_lit_in_clauses_heur_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_def mop_cch_remove_one_impl
is ‹uncurry mop_cch_remove_one›
:: ‹unat_lit_assn⇧k *⇩a cch_assn⇧d →⇩a cch_assn›
unfolding mop_cch_remove_one_def
by sepref
sepref_register mop_cch_remove_one mop_arena_status_st mop_arena_promote_st
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 mop_cch_remove_all_clauses_impl
is ‹uncurry2 mop_cch_remove_all_clauses›
:: ‹isasat_bounded_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a cch_assn⇧d →⇩a cch_assn›
unfolding mop_cch_remove_all_clauses_def mop_access_lit_in_clauses_heur_def[symmetric]
mop_arena_length_st_def[symmetric]
supply [dest] = isasat_bounded_assn_length_arenaD
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_register ASize
lemma arena_is_valid_clause_idxD:
assumes ‹arena_is_valid_clause_idx a b›
‹rdomp (al_assn arena_el_impl_assn) a›
‹j ≤ arena_length a b›
shows ‹j - 2 < max_unat 32›
proof -
obtain N vdom where
‹valid_arena a N vdom› and
‹b ∈# dom_m N›
using assms(1) unfolding arena_is_valid_clause_idx_def
by auto
then have eq: ‹length (N ∝ b) = arena_length a b› and
le: ‹b < length a› and
size: ‹is_Size (a ! (b - SIZE_SHIFT))›
by (auto simp: arena_lifting)
have ‹i<length a ⟹ rdomp arena_el_impl_assn (a ! i)› for i
using rdomp_al_dest'[OF assms(2)]
by auto
from this[of ‹b - SIZE_SHIFT›] have ‹rdomp arena_el_impl_assn (a ! (b - SIZE_SHIFT))›
using le by auto
then have ‹length (N ∝ b) ≤ unat32_max + 2›
using size eq unfolding rdomp_pure
apply (auto simp: rdomp_def arena_el_impl_rel_def is_Size_def
comp_def pure_def unat_rel_def unat.rel_def br_def arena_el_rel_def
arena_length_def unat32_max_def)
subgoal for x
using unat_lt_max_unat[of x]
apply (auto simp: max_unat_def)
done
done
then show ?thesis
using assms POS_SHIFT_def
unfolding isa_update_pos_pre_def
by (auto simp: arena_is_valid_clause_idx_def arena_lifting eq
unat32_max_def max_unat_def)
qed
lemma arena_is_valid_clause_idxD2: ‹arena_is_valid_clause_idx b a ⟹ a - Suc 0 < length b›
‹arena_is_valid_clause_idx b a ⟹ MAX_LENGTH_SHORT_CLAUSE < arena_length b a ⟹ 3 ≤ a›
‹arena_is_valid_clause_idx b a ⟹ MAX_LENGTH_SHORT_CLAUSE < arena_length b a ⟹ a - 3 < length b›
using arena_lengthI(2) less_imp_diff_less apply blast
apply (auto simp: arena_is_valid_clause_idx_def header_size_def arena_lifting split: if_splits dest: arena_lifting(1)[of _ _ _ a])
apply (metis arena_header_size_def arena_lifting(1) valid_arena_header_size)
using valid_arena_def by fastforce
sepref_def mop_arena_shorten_impl
is ‹uncurry2 mop_arena_shorten›
:: ‹sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a arena_fast_assn⇧d →⇩a arena_fast_assn›
unfolding mop_arena_shorten_def arena_shorten_def arena_shorten_pre_def SIZE_SHIFT_def POS_SHIFT_def
arena_is_valid_clause_idxD2
supply [intro] = arena_lengthI arena_is_valid_clause_idxD arena_is_valid_clause_idxD2
apply (rewrite at ‹APos ⌑› unat_const_fold[where 'a=32])
apply (annot_snat_const ‹TYPE(64)›)
apply (rewrite at ‹If _ (_[_ := ASize ⌑, _ := _]) _› annot_snat_unat_downcast[where 'l=32])
apply (rewrite at ‹If _ _ (_[_ := ASize ⌑])› annot_snat_unat_downcast[where 'l=32])
by sepref
sepref_def remove_lit_from_clause_impl
is ‹uncurry2 remove_lit_from_clause›
:: ‹arena_fast_assn⇧d *⇩a sint64_nat_assn⇧k *⇩a unat_lit_assn⇧k →⇩a arena_fast_assn›
unfolding remove_lit_from_clause_def if_not_swap
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma remove_lit_from_clause_st_alt_def: ‹remove_lit_from_clause_st S C L = do {
let (N, S) = extract_arena_wl_heur S;
N ← remove_lit_from_clause N C L;
RETURN (update_arena_wl_heur N S)
}›
by (auto simp: remove_lit_from_clause_st_def state_extractors push_to_tvdom_st_def
split: isasat_int_splits)
sepref_def remove_lit_from_clause_st_impl
is ‹uncurry2 remove_lit_from_clause_st›
:: ‹isasat_bounded_assn⇧d *⇩a sint64_nat_assn⇧k *⇩a unat_lit_assn⇧k →⇩a isasat_bounded_assn›
unfolding remove_lit_from_clause_st_alt_def
by sepref
sepref_register remove_lit_from_clause_st
lemma mark_garbage_heur_as_subsumed_alt_def:
‹mark_garbage_heur_as_subsumed C S⇩0 = (do{
ASSERT (arena_is_valid_clause_vdom (get_clauses_wl_heur S⇩0) C);
_ ← log_del_clause_heur S⇩0 C;
ASSERT (mark_garbage_pre (get_clauses_wl_heur S⇩0, C));
size ← mop_arena_length (get_clauses_wl_heur S⇩0) C;
let (N', S) = extract_arena_wl_heur S⇩0;
ASSERT (N' = get_clauses_wl_heur S⇩0);
let st = arena_status N' C = IRRED;
let N' = extra_information_mark_to_delete (N') C;
let (lcount, S) = extract_lcount_wl_heur S;
ASSERT(¬st ⟶ clss_size_lcount lcount ≥ 1);
let lcount = (if st then lcount else (clss_size_decr_lcount lcount));
let (stats, S) = extract_stats_wl_heur S;
let stats = (if st then decr_irred_clss stats else stats);
let S = update_arena_wl_heur N' S;
let S = update_lcount_wl_heur lcount S;
let S = update_stats_wl_heur stats S;
let S = incr_wasted_st (of_nat size) S;
RETURN S
})›
by (auto simp: mark_garbage_heur_as_subsumed_def Let_def state_extractors push_to_tvdom_st_def
intro!: bind_cong[OF refl]
split: isasat_int_splits)
sepref_def mark_garbage_heur_as_subsumed_impl
is ‹uncurry mark_garbage_heur_as_subsumed›
:: ‹sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
supply [[goals_limit=1]]
supply of_nat_snat[sepref_import_param]
unfolding mark_garbage_heur_as_subsumed_alt_def
mop_arena_length_st_def[symmetric]
by sepref
sepref_def isa_strengthen_clause_wl2_impl
is ‹uncurry3 isa_strengthen_clause_wl2›
:: ‹sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a unat_lit_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
unfolding isa_strengthen_clause_wl2_def mop_arena_status_st_def[symmetric]
mop_arena_length_st_def[symmetric]
apply (subst incr_forward_strengthened_st_def[symmetric])+
apply (annot_unat_const ‹TYPE(64)›)
by sepref
lemma subsumption_cases_split:
‹(case s of SUBSUMED_BY s ⇒ f s | STRENGTHENED_BY x y ⇒ g x y | NONE ⇒ h) =
(if is_NONE s then h else if is_subsumed s then f (subsumed_by s) else do {ASSERT (is_strengthened s); g (strengthened_on_lit s) (strengthened_by s)})›
by (auto simp: is_NONE_def split: subsumption.splits)
sepref_register isa_strengthen_clause_wl2 isa_subsume_or_strengthen_wl
sepref_def isa_subsume_or_strengthen_wl_impl
is ‹uncurry2 isa_subsume_or_strengthen_wl›
:: ‹sint64_nat_assn⇧k *⇩a subsumption_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
unfolding isa_subsume_or_strengthen_wl_def subsumption_cases_split mop_arena_status_st_def[symmetric]
incr_forward_subsumed_st_def[symmetric]
apply (annot_unat_const ‹TYPE(64)›)
by sepref
sepref_def isa_forward_subsumption_one_wl_impl
is ‹uncurry3 isa_forward_subsumption_one_wl›
:: ‹[λ((_, _), S). isasat_fast_relaxed S]⇩asint64_nat_assn⇧k *⇩a cch_assn⇧d *⇩a unat_lit_assn⇧k *⇩a isasat_bounded_assn⇧d → isasat_bounded_assn ×⇩a subsumption_assn ×⇩a cch_assn›
supply [dest] = rdomp_isasat_bounded_assn_length_avdomD isasat_bounded_assn_length_arenaD
supply [[goals_limit=1]]
unfolding isa_forward_subsumption_one_wl_def get_occs_list_at_def[symmetric] fold_is_NONE
mop_access_lit_in_clauses_heur_def[symmetric] length_occs_at_def[symmetric] mop_arena_status_st_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma isa_try_to_forward_subsume_wl_invI:
‹isa_try_to_forward_subsume_wl_inv S C (i, changed, break, D, T)⟹ isasat_fast_relaxed S ⟹ isasat_fast_relaxed T›
unfolding isa_try_to_forward_subsume_wl_inv_def prod.simps
by normalize_goal+ (auto simp add: isasat_fast_relaxed_def)
lemma isasat_bounded_assn_get_vdomD: ‹rdomp isasat_bounded_assn a ⟹ length (get_tvdom a) < max_snat 64›
using al_assn_boundD[of sint64_nat_assn, where 'l=‹64›, of ‹get_tvdom a›]
apply -
unfolding rdomp_def
apply normalize_goal+
apply (cases a, case_tac xa; cases ‹get_aivdom a›)
apply (auto 7 5 simp: isasat_bounded_assn_def snat64_max_def max_snat_def aivdom_assn_def
code_hider_assn_def hr_comp_def code_hider_rel_def import_param_3 pred_lift_def
split: isasat_int_splits
dest!: mod_starD al_assn_boundD[of sint64_nat_assn, where 'l=‹64›])
apply auto
done
sepref_def isa_try_to_forward_subsume_wl2_impl
is ‹uncurry3 isa_try_to_forward_subsume_wl2›
:: ‹[λ(((_, _), _), S). isasat_fast_relaxed S]⇩a sint64_nat_assn⇧k *⇩a cch_assn⇧d *⇩a (al_assn' TYPE(64) sint64_nat_assn)⇧d *⇩a isasat_bounded_assn⇧d →
cch_assn ×⇩a al_assn' TYPE(64) sint64_nat_assn ×⇩a isasat_bounded_assn›
unfolding isa_try_to_forward_subsume_wl2_def
mop_access_lit_in_clauses_heur_def[symmetric] Let_def[of ‹is_strengthened _›] fold_is_NONE
Let_def[of ‹if is_strengthened _ then _ else _›]
supply [[goals_limit=1]]
supply [intro] = isa_try_to_forward_subsume_wl_invI
supply [dest] = isasat_bounded_assn_get_vdomD
apply (rewrite at ‹if _ then mark_clause_for_unit_as_unchanged ⌑ else _› unat_const_fold[where 'a=‹64›])
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma empty_occs2_st_alt_def:
‹empty_occs2_st S = do {
let (occs, S) = extract_occs_wl_heur S;
occs ← empty_occs2 occs;
RETURN (update_occs_wl_heur occs S)
}›
by (auto simp: empty_occs2_st_def Let_def state_extractors
intro!: bind_cong[OF refl]
split: isasat_int_splits)
sepref_def empty_occs2_impl
is ‹empty_occs2›
:: ‹occs_assn⇧d →⇩a occs_assn›
unfolding empty_occs2_def fold_op_list_list_take op_list_list_len_def[symmetric]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_def empty_occs2_st_impl
is ‹empty_occs2_st›
:: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
unfolding empty_occs2_st_alt_def
by sepref
lemma isa_forward_subsumption_all_wl_invI:
‹isa_forward_subsumption_all_wl_inv R S (i, D, shrunken, T) ⟹ isasat_fast_relaxed R ⟹ isasat_fast_relaxed T›
unfolding isa_forward_subsumption_all_wl_inv_def prod.simps
apply normalize_goal+
by (auto simp: isasat_fast_relaxed_def)
sepref_register empty_occs2_st forward_subsumption_finalize schedule_next_subsume_st
sepref_def mark_added_clause_heur2_impl
is ‹uncurry mark_added_clause_heur2›
:: ‹isasat_bounded_assn⇧d *⇩a sint64_nat_assn⇧k →⇩a isasat_bounded_assn›
unfolding mark_added_clause_heur2_def
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma schedule_next_subsume_st_alt_def:
‹schedule_next_subsume_st b S = (let (heur, S) = extract_heur_wl_heur S;
heur = schedule_next_subsume b heur in
update_heur_wl_heur heur S)›
by (auto simp: schedule_next_subsume_st_def Let_def state_extractors
split: isasat_int_splits)
sepref_def schedule_next_subsume_st
is ‹uncurry (RETURN oo schedule_next_subsume_st)›
:: ‹word64_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
supply [[goals_limit=1]]
unfolding schedule_next_subsume_st_alt_def
by sepref
sepref_def forward_subsumption_finalize
is ‹uncurry forward_subsumption_finalize›
:: ‹(al_assn' TYPE(64) sint64_nat_assn)⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
unfolding forward_subsumption_finalize_def
supply [[goals_limit=1]]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
sepref_def isa_forward_subsumption_all_impl
is isa_forward_subsumption_all
:: ‹[isasat_fast_relaxed]⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
supply [[goals_limit=1]]
supply [intro] = isa_forward_subsumption_all_wl_invI
unfolding isa_forward_subsumption_all_def
access_tvdom_at_def[symmetric] length_tvdom_def[symmetric]
length_watchlist_raw_def[symmetric]
al_fold_custom_empty[where 'l=64]
apply (annot_snat_const ‹TYPE(64)›)
by sepref
lemma get_subsumption_opts_alt_def:
‹get_subsumption_opts S = (case S of IsaSAT M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts arena occs ⇒ opts_subsumption opts)›
by (cases S) (auto simp: get_subsumption_opts_def)
sepref_def get_subsumption_opts_impl
is ‹RETURN o get_subsumption_opts›
:: ‹isasat_bounded_assn⇧k →⇩a bool1_assn›
unfolding get_subsumption_opts_alt_def
by sepref
lemma next_subsume_schedule_st_def:
‹next_subsume_schedule_st S = (case S of IsaSAT M N D i W ivmtf icount ccach lbd outl stats heur aivdom clss opts arena occs ⇒ next_subsume_schedule heur)›
by (cases S) (auto simp: next_subsume_schedule_st_def)
sepref_def next_subsume_schedule_st_impl
is ‹RETURN o next_subsume_schedule_st›
:: ‹isasat_bounded_assn⇧k →⇩a word_assn›
unfolding next_subsume_schedule_st_def
by sepref
sepref_def should_subsume_st
is ‹RETURN o should_subsume_st›
:: ‹isasat_bounded_assn⇧k →⇩a bool1_assn›
unfolding should_subsume_st_def
by sepref
sepref_def isa_forward_subsume_impl
is isa_forward_subsume
:: ‹[isasat_fast_relaxed]⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
unfolding isa_forward_subsume_def
by sepref
end