Theory IsaSAT_Clauses_LLVM

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 ≤ MAX_HEADER_SIZE› by (auto simp: header_size_def)

lemma fm_add_new_bounds1: "⟦
  length a2' < header_size baa + length b + length baa;
  length b + length baa + MAX_HEADER_SIZE ≤ snat64_max   ⟧
  ⟹ Suc (length a2') < max_snat 64"

  ‹length b + length baa + MAX_HEADER_SIZE ≤ snat64_max ⟹ length b + header_size baa < max_snat 64›
  using header_size_bound[of baa]
  by (auto simp: max_snat_def snat64_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 ‹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] shorten_lbd_le
  apply (rewrite at ‹AStatus _ ⌑› unat_const_fold[where 'a=2])+
  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 ≤ snat64_max ∧ length arena + arena_length arena⇩o n +
         (if arena_length arena⇩o  n ≤ 4 then MIN_HEADER_SIZE else MAX_HEADER_SIZE) ≤ snat64_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