Theory IsaSAT_Mark_LLVM

theory IsaSAT_Mark_LLVM
  imports IsaSAT_Mark
    IsaSAT_Literals_LLVM
begin

type_synonym mark = ‹bool option›

definition mark_rel_aux :: ‹(int × mark) set› where
  ‹mark_rel_aux = {(0, None), (1, Some True), (-1, Some False)}›

definition mark_rel :: ‹(3 word × bool option) set› where
  ‹mark_rel = sint_rel' TYPE(3) O mark_rel_aux›

abbreviation mark_assn :: ‹mark ⇒ 3 word ⇒ assn› where
  ‹mark_assn ≡ pure mark_rel›

definition marked_struct_rel :: ‹(_ × lookup_clause_rel) set› where
  ‹marked_struct_rel = Id ×⇩r ⟨mark_rel_aux⟩list_rel›

type_synonym mark_assn = ‹32 word × 3 word ptr›
definition marked_struct_assn :: ‹lookup_clause_rel ⇒ mark_assn ⇒ assn› where
  ‹marked_struct_assn = uint32_nat_assn ×⇩a array_assn (pure mark_rel)›

definition Mark :: ‹bool ⇒ bool option› where [simp]: ‹Mark = Some›
definition NoMark :: ‹bool option› where [simp]: ‹NoMark = None›

lemmas mark_defs = Mark_def[symmetric] NoMark_def[symmetric]

lemmas [fcomp_norm_unfold] = mark_rel_aux_def[symmetric] mark_rel_def[symmetric]

sepref_def Mark_impl [llvm_inline]
  is [] ‹RETURN o (λb. if b then 1 else -1)› :: ‹bool1_assn⇧k →⇩a sint_assn' TYPE(3)›
  apply (annot_sint_const ‹TYPE(3)›)
  by sepref

sepref_def NoMark_impl [llvm_inline]
  is [] ‹uncurry0 (RETURN 0)› :: ‹unit_assn⇧k →⇩a sint_assn' TYPE(3)›
  apply (annot_sint_const ‹TYPE(3)›)
  by sepref

sepref_register Mark NoMark

lemma Mark_rel_aux: ‹(λb. if b then 1 :: int else -1, Mark) ∈ bool_rel → mark_rel_aux›
  by (auto intro: frefI split: if_splits simp: mark_rel_aux_def)

lemmas [sepref_fr_rules] =
  Mark_impl.refine[FCOMP Mark_rel_aux]

lemma NoMark_rel_aux: ‹(0, NoMark) ∈ mark_rel_aux›
  by (auto intro: frefI split: if_splits simp: mark_rel_aux_def)

lemmas [sepref_fr_rules] =
  NoMark_impl.refine[FCOMP NoMark_rel_aux]

lemma mark_rel_aux_eq:  ‹((=), (=)) ∈ mark_rel_aux → mark_rel_aux → bool_rel›
  by (auto intro!: frefI simp: mark_rel_aux_def)

sepref_def mark_eq_impl is
  ‹uncurry (RETURN oo (=))› :: ‹(sint_assn' TYPE(3))⇧d *⇩a (sint_assn' TYPE(3))⇧d →⇩a bool1_assn›
  unfolding mark_rel_aux_def
  by sepref

lemmas [sepref_fr_rules] = mark_eq_impl.refine[FCOMP mark_rel_aux_eq]

sepref_register ‹(=) :: mark ⇒ _ ⇒ _› lit_is_in_lookup delete_from_lookup_conflict unmark_clause
  add_to_lookup_conflict pre_simplify_clause_lookup

sepref_def lit_is_in_lookup_impl
  is ‹uncurry lit_is_in_lookup›
  :: ‹unat_lit_assn⇧k *⇩a marked_struct_assn⇧k →⇩a bool1_assn›
  unfolding lit_is_in_lookup_def mark_defs marked_struct_assn_def
    array_fold_custom_replicate
  apply (annot_all_atm_idxs)
  by sepref

sepref_def delete_from_lookup_conflict_impl
  is ‹uncurry delete_from_lookup_conflict›
  :: ‹unat_lit_assn⇧k *⇩a marked_struct_assn⇧d →⇩a marked_struct_assn›
  unfolding delete_from_lookup_conflict_def mark_defs marked_struct_assn_def
  apply (annot_unat_const ‹TYPE(32)›)
  apply (annot_all_atm_idxs)
  by sepref
abbreviation clause_ll_assn where
  ‹clause_ll_assn ≡ al_assn' TYPE(64) unat_lit_assn›

sepref_def unmark_clause_impl
  is ‹uncurry unmark_clause›
  :: ‹clause_ll_assn⇧k *⇩a marked_struct_assn⇧d →⇩a marked_struct_assn›
  unfolding unmark_clause_def
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

sepref_def add_to_lookup_conflict
  is ‹uncurry (RETURN oo add_to_lookup_conflict)›
  :: ‹[λ(L, n, D). atm_of L < length D ∧ n < unat32_max]⇩a
    unat_lit_assn⇧k *⇩a marked_struct_assn⇧d → marked_struct_assn›
  unfolding mark_defs marked_struct_assn_def add_to_lookup_conflict_def NOTIN_def ISIN_def
  apply (annot_unat_const ‹TYPE(32)›)
  apply (annot_all_atm_idxs)
  by sepref

sepref_def pre_simplify_clause_lookup_impl
  is ‹uncurry2 pre_simplify_clause_lookup›
  :: ‹clause_ll_assn⇧k *⇩a clause_ll_assn⇧d *⇩a marked_struct_assn⇧d →⇩a bool1_assn ×⇩a clause_ll_assn ×⇩a marked_struct_assn›
  unfolding pre_simplify_clause_lookup_def
  supply [[goals_limit=1]]
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

end