Theory IsaSAT_Trail_LLVM (Isabelle2019: June 2019)

theory IsaSAT_Trail_LLVM
imports IsaSAT_Literals_LLVM IsaSAT_Trail
begin


type_synonym tri_bool_assn = "8 word"

definition "tri_bool_rel_aux ≡ { (0::nat,None), (2,Some True), (3,Some False) }"
definition "tri_bool_rel ≡ unat_rel' TYPE(8) O tri_bool_rel_aux"
abbreviation "tri_bool_assn ≡ pure tri_bool_rel"
lemmas [fcomp_norm_unfold] = tri_bool_rel_def[symmetric]

lemma tri_bool_UNSET_refine_aux: "(0,UNSET)∈tri_bool_rel_aux"
  and tri_bool_SET_TRUE_refine_aux: "(2,SET_TRUE)∈tri_bool_rel_aux"
  and tri_bool_SET_FALSE_refine_aux: "(3,SET_FALSE)∈tri_bool_rel_aux"
  and tri_bool_eq_refine_aux: "((=),tri_bool_eq) ∈ tri_bool_rel_aux→tri_bool_rel_aux→bool_rel"
  by (auto simp: tri_bool_rel_aux_def tri_bool_eq_def)

sepref_def tri_bool_UNSET_impl is [] "uncurry0 (RETURN 0)" :: "unit_assn⇧^k →⇩_a unat_assn' TYPE(8)"
  apply (annot_unat_const "TYPE(8)")
  by sepref

sepref_def tri_bool_SET_TRUE_impl is [] "uncurry0 (RETURN 2)" :: "unit_assn⇧^k →⇩_a unat_assn' TYPE(8)"
  apply (annot_unat_const "TYPE(8)")
  by sepref

sepref_def tri_bool_SET_FALSE_impl is [] "uncurry0 (RETURN 3)" :: "unit_assn⇧^k →⇩_a unat_assn' TYPE(8)"
  apply (annot_unat_const "TYPE(8)")
  by sepref

sepref_def tri_bool_eq_impl [llvm_inline] is [] "uncurry (RETURN oo (=))" :: "(unat_assn' TYPE(8))⇧^k *⇩_a (unat_assn' TYPE(8))⇧^k →⇩_a bool1_assn"
  by sepref

lemmas [sepref_fr_rules] =
  tri_bool_UNSET_impl.refine[FCOMP tri_bool_UNSET_refine_aux]
  tri_bool_SET_TRUE_impl.refine[FCOMP tri_bool_SET_TRUE_refine_aux]
  tri_bool_SET_FALSE_impl.refine[FCOMP tri_bool_SET_FALSE_refine_aux]
  tri_bool_eq_impl.refine[FCOMP tri_bool_eq_refine_aux]

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›

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›


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 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 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

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

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

end

end