theory IsaSAT_Clauses_LLVM imports IsaSAT_Clauses IsaSAT_Arena_LLVM begin sepref_register is_short_clause header_size fm_add_new_fast fm_mv_clause_to_new_arena abbreviation clause_ll_assn :: ‹nat clause_l ⇒ _ ⇒ assn› where ‹clause_ll_assn ≡ larray64_assn unat_lit_assn› sepref_def is_short_clause_code is ‹RETURN o is_short_clause› :: ‹ clause_ll_assn⇧k →⇩a bool1_assn› unfolding is_short_clause_def by sepref sepref_def header_size_code is ‹RETURN o header_size› :: ‹clause_ll_assn⇧k →⇩a sint64_nat_assn› unfolding header_size_def apply (annot_snat_const "TYPE(64)") by sepref lemma header_size_bound: "header_size x ≤ 5" by (auto simp: header_size_def) lemma fm_add_new_bounds1: "⟦ length a2' < header_size baa + length b + length baa; length b + length baa + 5 ≤ sint64_max ⟧ ⟹ Suc (length a2') < max_snat 64" "length b + length baa + 5 ≤ sint64_max ⟹ length b + header_size baa < max_snat 64" using header_size_bound[of baa] by (auto simp: max_snat_def sint64_max_def) sepref_def append_and_length_fast_code is ‹uncurry2 fm_add_new_fast› :: ‹[append_and_length_fast_code_pre]⇩a bool1_assn⇧k *⇩a clause_ll_assn⇧k *⇩a (arena_fast_assn)⇧d → arena_fast_assn ×⇩a sint64_nat_assn› unfolding fm_add_new_fast_def fm_add_new_def append_and_length_fast_code_pre_def apply (rewrite at "AActivity ⌑" unat_const_fold[where 'a=32])+ apply (rewrite at "APos ⌑" unat_const_fold[where 'a=32])+ apply (rewrite at "length _ - 2" annot_snat_unat_downcast[where 'l=32]) supply [simp] = fm_add_new_bounds1[simplified] apply (annot_snat_const "TYPE(64)") by sepref sepref_def fm_mv_clause_to_new_arena_fast_code is ‹uncurry2 fm_mv_clause_to_new_arena› :: ‹[λ((n, arena⇩o), arena). length arena⇩o ≤ sint64_max ∧ length arena + arena_length arena⇩o n + (if arena_length arena⇩o n ≤ 4 then 4 else 5) ≤ sint64_max]⇩a sint64_nat_assn⇧k *⇩a arena_fast_assn⇧k *⇩a arena_fast_assn⇧d → arena_fast_assn› supply [[goals_limit=1]] if_splits[split] unfolding fm_mv_clause_to_new_arena_def apply (annot_snat_const "TYPE(64)") by sepref experiment begin export_llvm is_short_clause_code header_size_code append_and_length_fast_code fm_mv_clause_to_new_arena_fast_code end end