Theory IsaSAT_Trail_LLVM

theory IsaSAT_Trail_LLVM
imports IsaSAT_Literals_LLVM IsaSAT_Trail
begin

hide_const (open) NEMonad.ASSERT NEMonad.RETURN

type_synonym trail_pol_fast_assn =
   ‹32 word array_list64 × tri_bool_assn larray64 × 32 word larray64 ×
     64 word larray64 × 32 word ×
     32 word array_list64 × 64 word›

sepref_def DECISION_REASON_impl is ‹uncurry0 (RETURN DECISION_REASON)›
  :: ‹unit_assn⇧k →⇩a sint64_nat_assn›
  unfolding DECISION_REASON_def apply (annot_snat_const ‹TYPE(64)›) by sepref


definition trail_pol_fast_assn :: ‹trail_pol ⇒ trail_pol_fast_assn ⇒ assn› where
  ‹trail_pol_fast_assn ≡
    arl64_assn unat_lit_assn ×⇩a larray64_assn (tri_bool_assn) ×⇩a
    larray64_assn uint32_nat_assn ×⇩a
    larray64_assn sint64_nat_assn ×⇩a uint32_nat_assn ×⇩a
    arl64_assn uint32_nat_assn ×⇩a sint64_nat_assn›


paragraph ‹Code generation›

subparagraph ‹Conversion between incomplete and complete mode›


sepref_def count_decided_pol_impl is ‹RETURN o count_decided_pol› :: ‹trail_pol_fast_assn⇧k →⇩a uint32_nat_assn›
  unfolding trail_pol_fast_assn_def count_decided_pol_def
  by sepref


sepref_def get_level_atm_fast_code
  is ‹uncurry (RETURN oo get_level_atm_pol)›
  :: ‹[get_level_atm_pol_pre]⇩a
  trail_pol_fast_assn⇧k *⇩a atom_assn⇧k → uint32_nat_assn›
  unfolding get_level_atm_pol_def nat_shiftr_div2[symmetric]
     get_level_atm_pol_pre_def trail_pol_fast_assn_def
  supply [[eta_contract = false, show_abbrevs=false]]
  apply (rewrite at ‹nth _› eta_expand)
  apply (rewrite at ‹nth _ _› annot_index_of_atm)
  by sepref


sepref_def get_level_fast_code
  is ‹uncurry (RETURN oo get_level_pol)›
  :: ‹[get_level_pol_pre]⇩a
      trail_pol_fast_assn⇧k *⇩a unat_lit_assn⇧k → uint32_nat_assn›
  unfolding get_level_get_level_atm nat_shiftr_div2[symmetric]
  get_level_pol_pre_def get_level_pol_def
  supply [[goals_limit = 1]] image_image[simp] in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff[simp]
    get_level_atm_pol_pre_def[simp]
  by sepref


sepref_def polarity_pol_fast_code
  is ‹uncurry (RETURN oo polarity_pol)›
  :: ‹[uncurry polarity_pol_pre]⇩a trail_pol_fast_assn⇧k *⇩a unat_lit_assn⇧k → tri_bool_assn›
  unfolding polarity_pol_def option.case_eq_if polarity_pol_pre_def
    trail_pol_fast_assn_def
  supply [[goals_limit = 1]]
  by sepref

sepref_def polarity_pol_fast
  is ‹uncurry (mop_polarity_pol)›
  :: ‹trail_pol_fast_assn⇧k *⇩a unat_lit_assn⇧k →⇩a tri_bool_assn›
  unfolding mop_polarity_pol_def trail_pol_fast_assn_def
    polarity_pol_def polarity_pol_pre_def
  by sepref


sepref_register isa_length_trail
sepref_def isa_length_trail_fast_code
  is ‹RETURN o isa_length_trail›
  :: ‹[λ_. True]⇩a trail_pol_fast_assn⇧k → snat_assn' TYPE(64)›
  unfolding isa_length_trail_def isa_length_trail_pre_def length_uint32_nat_def
    trail_pol_fast_assn_def
  by sepref

sepref_def mop_isa_length_trail_fast_code
  is ‹mop_isa_length_trail›
  :: ‹trail_pol_fast_assn⇧k →⇩a snat_assn' TYPE(64)›
  unfolding mop_isa_length_trail_def isa_length_trail_pre_def length_uint32_nat_def
  by sepref


sepref_def cons_trail_Propagated_tr_fast_code
  is ‹uncurry2 (cons_trail_Propagated_tr)›
  :: ‹unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a trail_pol_fast_assn⇧d →⇩a trail_pol_fast_assn›
  unfolding cons_trail_Propagated_tr_def cons_trail_Propagated_tr_def
    SET_TRUE_def[symmetric] SET_FALSE_def[symmetric] cons_trail_Propagated_tr_pre_def
  unfolding trail_pol_fast_assn_def prod.case
  apply (subst (3)annot_index_of_atm)
  apply (subst (4)annot_index_of_atm)
  (*unfolding ins_idx_upcast64  *)
  supply [[goals_limit = 1]]
(*   unfolding fold_tuple_optimizations *)
  by sepref

(*
sepref_def (in -)last_trail_fast_code
  is ‹RETURN o last_trail_pol›
  :: ‹[last_trail_pol_pre]⇩a
       trail_pol_fast_assn⇧k → unat_lit_assn ×⇩a option_assn uint64_nat_assn›
  unfolding last_trail_pol_def nth_u_def[symmetric] zero_uint64_nat_def[symmetric]
    last_trail_pol_pre_def
  supply [[goals_limit = 1]]
  by sepref

declare last_trail_fast_code.refine[sepref_fr_rules]
*)


sepref_def tl_trail_tr_fast_code
  is ‹RETURN o tl_trailt_tr›
  :: ‹[tl_trailt_tr_pre]⇩a
        trail_pol_fast_assn⇧d → trail_pol_fast_assn›
  supply if_splits[split] option.splits[split]
  unfolding tl_trailt_tr_def UNSET_def[symmetric] tl_trailt_tr_pre_def
  unfolding trail_pol_fast_assn_def
  apply (annot_unat_const ‹TYPE(32)›)
  supply [[goals_limit = 1]]
  unfolding fold_tuple_optimizations
  by sepref

sepref_def tl_trail_proped_tr_fast_code
  is ‹RETURN o tl_trail_propedt_tr›
  :: ‹[tl_trail_propedt_tr_pre]⇩a
        trail_pol_fast_assn⇧d → trail_pol_fast_assn›
  supply if_splits[split] option.splits[split]
  unfolding tl_trail_propedt_tr_def UNSET_def[symmetric]
    tl_trail_propedt_tr_pre_def
  unfolding (*ins_idx_upcast64[where i=‹atm_of _›]*) trail_pol_fast_assn_def
  apply (annot_unat_const ‹TYPE(32)›)
  supply [[goals_limit = 1]]
  by sepref


sepref_def lit_of_last_trail_fast_code
  is ‹RETURN o lit_of_last_trail_pol›
  :: ‹[λ(M, _). M ≠ []]⇩a trail_pol_fast_assn⇧k → unat_lit_assn›
  unfolding lit_of_last_trail_pol_def trail_pol_fast_assn_def
  by sepref


sepref_def cons_trail_Decided_tr_fast_code
  is ‹uncurry (RETURN oo cons_trail_Decided_tr)›
  :: ‹[cons_trail_Decided_tr_pre]⇩a
       unat_lit_assn⇧k *⇩a trail_pol_fast_assn⇧d → trail_pol_fast_assn›
  unfolding cons_trail_Decided_tr_def cons_trail_Decided_tr_def trail_pol_fast_assn_def
    SET_TRUE_def[symmetric] SET_FALSE_def[symmetric] cons_trail_Decided_tr_pre_def
  (*unfolding annot_index_atm_of*)
  apply (annot_unat_const ‹TYPE(32)›)
  apply (rewrite at ‹_@[⌑]› in ‹(_,⌑)› annot_snat_unat_downcast[where 'l=‹32›])
  supply [[goals_limit = 1]]
  unfolding fold_tuple_optimizations
  by sepref


sepref_def defined_atm_fast_code
  is ‹uncurry (RETURN oo defined_atm_pol)›
  :: ‹[uncurry defined_atm_pol_pre]⇩a trail_pol_fast_assn⇧k *⇩a atom_assn⇧k → bool1_assn›
  unfolding defined_atm_pol_def UNSET_def[symmetric] tri_bool_eq_def[symmetric]
    defined_atm_pol_pre_def trail_pol_fast_assn_def Pos_rel_def[symmetric]
  unfolding ins_idx_upcast64
  supply Pos_impl.refine[sepref_fr_rules]
  supply UNSET_def[simp del]
  by sepref


sepref_register get_propagation_reason_raw_pol
sepref_def get_propagation_reason_fast_code
  is ‹uncurry get_propagation_reason_raw_pol›
  :: ‹trail_pol_fast_assn⇧k *⇩a unat_lit_assn⇧k →⇩a sint64_nat_assn›
  unfolding get_propagation_reason_raw_pol_def trail_pol_fast_assn_def
    (*annot_index_atm_of*)
  by sepref


(*
sepref_definition get_propagation_reason_fast_code
  is ‹uncurry get_propagation_reason_pol›
  :: ‹trail_pol_fast_assn⇧k *⇩a unat_lit_assn⇧k →⇩a option_assn uint64_nat_assn›
  unfolding get_propagation_reason_pol_def
   zero_uint64_nat_def[symmetric]
  by sepref

declare get_propagation_reason_fast_code.refine[sepref_fr_rules]
  get_propagation_reason_code.refine[sepref_fr_rules]


sepref_definition get_the_propagation_reason_code
  is ‹uncurry get_the_propagation_reason_pol›
  :: ‹trail_pol_assn⇧k *⇩a unat_lit_assn⇧k →⇩a option_assn nat_assn›
  unfolding get_the_propagation_reason_pol_def
    tri_bool_eq_def[symmetric]
  by sepref

sepref_definition (in -) get_the_propagation_reason_fast_code
  is ‹uncurry get_the_propagation_reason_pol›
  :: ‹trail_pol_fast_assn⇧k *⇩a unat_lit_assn⇧k →⇩a option_assn uint64_nat_assn›
  unfolding get_the_propagation_reason_pol_def
    tri_bool_eq_def[symmetric]
  by sepref

declare get_the_propagation_reason_fast_code.refine[sepref_fr_rules]
  get_the_propagation_reason_code.refine[sepref_fr_rules]
*)
sepref_register isa_trail_nth trail_height_before_conflict

sepref_def isa_trail_nth_fast_code
  is ‹uncurry isa_trail_nth›
  :: ‹trail_pol_fast_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a unat_lit_assn›
  unfolding isa_trail_nth_def trail_pol_fast_assn_def
  by sepref

sepref_def tl_trail_tr_no_CS_fast_code
  is ‹RETURN o tl_trailt_tr_no_CS›
  :: ‹[tl_trailt_tr_no_CS_pre]⇩a
        trail_pol_fast_assn⇧d → trail_pol_fast_assn›
  supply if_splits[split] option.splits[split]
  unfolding tl_trailt_tr_no_CS_def UNSET_def[symmetric] tl_trailt_tr_no_CS_pre_def
  unfolding (*annot_index_atm_of*) trail_pol_fast_assn_def
  apply (annot_unat_const ‹TYPE(32)›)
  supply [[goals_limit = 1]]
  by sepref


sepref_def trail_conv_back_imp_fast_code
  is ‹uncurry trail_conv_back_imp›
  :: ‹uint32_nat_assn⇧k *⇩a trail_pol_fast_assn⇧d →⇩a trail_pol_fast_assn›
  supply [[goals_limit=1]]
  unfolding trail_conv_back_imp_def trail_pol_fast_assn_def
  apply (rewrite at ‹take ⌑› annot_unat_snat_upcast[where 'l=64])
  by sepref


sepref_def get_pos_of_level_in_trail_imp_fast_code
  is ‹uncurry get_pos_of_level_in_trail_imp›
  :: ‹trail_pol_fast_assn⇧k *⇩a uint32_nat_assn⇧k →⇩a uint32_nat_assn›
  unfolding get_pos_of_level_in_trail_imp_def trail_pol_fast_assn_def
  apply (rewrite at ‹_ ! ⌑› annot_unat_snat_upcast[where 'l=64])
  by sepref

sepref_def get_the_propagation_reason_fast_code
  is ‹uncurry get_the_propagation_reason_pol›
  :: ‹trail_pol_fast_assn⇧k *⇩a unat_lit_assn⇧k →⇩a snat_option_assn' TYPE(64)›
  unfolding get_the_propagation_reason_pol_def trail_pol_fast_assn_def
    tri_bool_eq_def[symmetric]
  by sepref

sepref_def trail_height_before_conflict_impl
  is ‹trail_height_before_conflict›
  :: ‹trail_pol_fast_assn⇧k →⇩a uint32_nat_assn›
  unfolding trail_height_before_conflict_def trail_pol_fast_assn_def
  apply (annot_unat_const ‹TYPE(32)›)
  apply (rewrite at ‹_ ! ⌑› annot_unat_snat_upcast[where 'l=64])
  supply [[goals_limit = 1]]
  by sepref

sepref_def trail_zeroed_until_impl
  is ‹RETURN o trail_zeroed_until›
  :: ‹trail_pol_fast_assn⇧k →⇩a sint64_nat_assn›
  unfolding trail_zeroed_until_def trail_pol_fast_assn_def
  by sepref

sepref_def trail_set_zeroed_until_impl
  is ‹uncurry (RETURN oo trail_set_zeroed_until)›
  :: ‹sint64_nat_assn⇧k *⇩a trail_pol_fast_assn⇧d →⇩a trail_pol_fast_assn›
  unfolding trail_set_zeroed_until_def trail_pol_fast_assn_def
  by sepref


schematic_goal mk_free_trail_pol_fast_assn[sepref_frame_free_rules]: ‹MK_FREE trail_pol_fast_assn ?fr›
  unfolding trail_pol_fast_assn_def
  by synthesize_free


experiment begin

export_llvm
  tri_bool_UNSET_impl
  tri_bool_SET_TRUE_impl
  tri_bool_SET_FALSE_impl
  DECISION_REASON_impl
  count_decided_pol_impl
  get_level_atm_fast_code
  get_level_fast_code
  polarity_pol_fast_code
  isa_length_trail_fast_code
  cons_trail_Propagated_tr_fast_code
  tl_trail_tr_fast_code
  tl_trail_proped_tr_fast_code
  lit_of_last_trail_fast_code
  cons_trail_Decided_tr_fast_code
  defined_atm_fast_code
  get_propagation_reason_fast_code
  isa_trail_nth_fast_code
  tl_trail_tr_no_CS_fast_code
  trail_conv_back_imp_fast_code
  get_pos_of_level_in_trail_imp_fast_code
  get_the_propagation_reason_fast_code
  trail_height_before_conflict_impl
  trail_set_zeroed_until_impl
  trail_zeroed_until_impl
end

end