Theory IsaSAT_Conflict_Analysis_LLVM

theory IsaSAT_Conflict_Analysis_LLVM
imports IsaSAT_Conflict_Analysis IsaSAT_VMTF_LLVM IsaSAT_Setup_LLVM
begin
thm fold_tuple_optimizations
(*
lemma mark_of_refine[sepref_fr_rules]:
  ‹(return o (λC. the (snd C)), RETURN o mark_of) ∈
    [λC. is_proped C]⇩a pair_nat_ann_lit_assn⇧k → nat_assn›
  apply sepref_to_hoare
  apply (case_tac x; case_tac xi; case_tac ‹snd xi›)
  by (sep_auto simp: nat_ann_lit_rel_def)+


lemma mark_of_fast_refine[sepref_fr_rules]:
  ‹(return o (λC. the (snd C)), RETURN o mark_of) ∈
    [λC. is_proped C]⇩a pair_nat_ann_lit_fast_assn⇧k → uint64_nat_assn›
proof -
  have 1: ‹option_assn (λa c. ↑ ((c, a) ∈ uint64_nat_rel)) = pure (⟨uint64_nat_rel⟩option_rel)›
    unfolding option_assn_pure_conv[symmetric]
    by (auto simp: pure_def)
  show ?thesis
    apply sepref_to_hoare
    unfolding 1
    apply (case_tac x; case_tac xi; case_tac ‹snd xi›)
       apply (sep_auto simp: br_def)
      apply (sep_auto simp: nat_ann_lit_rel_def uint64_nat_rel_def br_def
        ann_lit_of_pair_if cong: )+
     apply (sep_auto simp: hr_comp_def)
    apply (sep_auto simp: hr_comp_def uint64_nat_rel_def br_def)
     apply (auto simp: nat_ann_lit_rel_def elim: option_relE)[]
    apply (auto simp: ent_refl_true)
    done
qed
*)

lemma get_count_max_lvls_heur_def:
   ‹get_count_max_lvls_heur = (λ(_, _, _, _, _, _, clvls, _). clvls)›
  by (auto intro!: ext)

sepref_def get_count_max_lvls_heur_impl
  is ‹RETURN o get_count_max_lvls_heur›
  :: ‹isasat_bounded_assn⇧k →⇩a uint32_nat_assn›
  unfolding get_count_max_lvls_heur_def isasat_bounded_assn_def
  by sepref

lemmas [sepref_fr_rules] = get_count_max_lvls_heur_impl.refine

sepref_def maximum_level_removed_eq_count_dec_fast_code
  is ‹uncurry (maximum_level_removed_eq_count_dec_heur)›
  :: ‹unat_lit_assn⇧k *⇩a isasat_bounded_assn⇧k →⇩a bool1_assn›
  unfolding maximum_level_removed_eq_count_dec_heur_def
  apply (annot_unat_const "TYPE(32)")
  by sepref

declare
  maximum_level_removed_eq_count_dec_fast_code.refine[sepref_fr_rules]

lemma is_decided_hd_trail_wl_heur_alt_def:
  ‹is_decided_hd_trail_wl_heur = (λ((M, xs, lvls, reasons, k), _).
      let r = reasons ! (atm_of (last M)) in
      r = DECISION_REASON)›
  unfolding is_decided_hd_trail_wl_heur_def last_trail_pol_def
  by (auto simp: is_decided_hd_trail_wl_heur_pre_def last_trail_pol_def
     Let_def intro!: ext split: if_splits)

sepref_def is_decided_hd_trail_wl_fast_code
  is ‹RETURN o is_decided_hd_trail_wl_heur›
  :: ‹[is_decided_hd_trail_wl_heur_pre]⇩a isasat_bounded_assn⇧k → bool1_assn›
  supply [[goals_limit=1]]
  unfolding is_decided_hd_trail_wl_heur_alt_def isasat_bounded_assn_def
    is_decided_hd_trail_wl_heur_pre_def last_trail_pol_def trail_pol_fast_assn_def
    last_trail_pol_pre_def
  by sepref

declare
  is_decided_hd_trail_wl_fast_code.refine[sepref_fr_rules]

sepref_def lit_and_ann_of_propagated_st_heur_fast_code
  is ‹lit_and_ann_of_propagated_st_heur›
  :: ‹[λ_. True]⇩a
       isasat_bounded_assn⇧k → (unat_lit_assn ×⇩a sint64_nat_assn)›
  supply [[goals_limit=1]]
  supply get_trail_wl_heur_def[simp]
  unfolding lit_and_ann_of_propagated_st_heur_def isasat_bounded_assn_def
    lit_and_ann_of_propagated_st_heur_pre_def trail_pol_fast_assn_def
  unfolding fold_tuple_optimizations
  by sepref

declare
  lit_and_ann_of_propagated_st_heur_fast_code.refine[sepref_fr_rules]

(*TODO Move or kill*)
definition is_UNSET where [simp]: ‹is_UNSET x ⟷ x = UNSET›
lemma tri_bool_is_UNSET_refine_aux:
  ‹(λx. x = 0, is_UNSET) ∈ tri_bool_rel_aux → bool_rel ›
  by (auto simp: tri_bool_rel_aux_def)

sepref_definition is_UNSET_impl
  is ‹RETURN o (λx. x= 0)›
  :: ‹(unat_assn' TYPE(8))⇧k →⇩a bool1_assn›
  apply (annot_unat_const "TYPE(8)")
  by sepref

(*lemmas [sepref_fr_rules] = is_UNSET_impl.refine[FCOMP tri_bool_is_UNSET_refine_aux]*)
(*END Move*)

(*TODO Move*)

sepref_def is_in_option_lookup_conflict_code
  is ‹uncurry (RETURN oo is_in_option_lookup_conflict)›
  :: ‹[λ(L, (c, n, xs)). atm_of L < length xs]⇩a
        unat_lit_assn⇧k *⇩a conflict_option_rel_assn⇧k → bool1_assn›
  unfolding is_in_option_lookup_conflict_alt_def is_in_lookup_conflict_def PROTECT_def
     is_NOTIN_alt_def[symmetric] conflict_option_rel_assn_def lookup_clause_rel_assn_def
  by sepref

sepref_def atm_is_in_conflict_st_heur_fast_code
  is ‹uncurry (atm_is_in_conflict_st_heur)›
  :: ‹[λ_. True]⇩a unat_lit_assn⇧k *⇩a isasat_bounded_assn⇧k → bool1_assn›
  supply [[goals_limit=1]]
  unfolding atm_is_in_conflict_st_heur_def atm_is_in_conflict_st_heur_pre_def isasat_bounded_assn_def
    atm_in_conflict_lookup_def trail_pol_fast_assn_def NOTIN_def[symmetric]
   is_NOTIN_def[symmetric] conflict_option_rel_assn_def lookup_clause_rel_assn_def
  unfolding fold_tuple_optimizations atm_in_conflict_lookup_pre_def
  by sepref

declare atm_is_in_conflict_st_heur_fast_code.refine[sepref_fr_rules]
(*END Move*)

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

declare lit_of_last_trail_fast_code.refine[sepref_fr_rules]

lemma tl_state_wl_heurI: ‹tl_state_wl_heur_pre (a, b) ⟹ fst a ≠ []›
  ‹tl_state_wl_heur_pre (a, b) ⟹ tl_trailt_tr_pre a›
  ‹tl_state_wl_heur_pre (a1', a1'a, a1'b, a1'c, a1'd, a1'e, a1'f, a2'f) ⟹
       vmtf_unset_pre (atm_of (lit_of_last_trail_pol a1')) a1'e›
  by (auto simp: tl_state_wl_heur_pre_def tl_trailt_tr_pre_def
    vmtf_unset_pre_def lit_of_last_trail_pol_def)

lemma tl_state_wl_heur_alt_def:
  ‹tl_state_wl_heur = (λ(M, N, D, WS, Q, vmtf, φ, clvls). do {
       ASSERT(tl_state_wl_heur_pre (M, N, D, WS, Q, vmtf, φ, clvls));
       let L = (atm_of (lit_of_last_trail_pol M));
       RETURN (False, (tl_trailt_tr M, N, D, WS, Q, isa_vmtf_unset L vmtf, φ, clvls))
  })›
  by (auto simp: tl_state_wl_heur_def)

sepref_def tl_state_wl_heur_fast_code
  is ‹tl_state_wl_heur›
  :: ‹[λ_. True]⇩a isasat_bounded_assn⇧d → bool1_assn ×⇩a isasat_bounded_assn›
  supply [[goals_limit=1]] if_splits[split] tl_state_wl_heurI[simp]
  unfolding tl_state_wl_heur_alt_def[abs_def] isasat_bounded_assn_def get_trail_wl_heur_def
    vmtf_unset_def bind_ref_tag_def short_circuit_conv
  unfolding fold_tuple_optimizations
  apply (rewrite in ‹ASSERT ⌑› fold_tuple_optimizations[symmetric])+
  by sepref

declare
  tl_state_wl_heur_fast_code.refine[sepref_fr_rules]

definition None_lookup_conflict :: ‹_ ⇒ _ ⇒ conflict_option_rel› where
‹None_lookup_conflict b xs = (b, xs)›


sepref_def None_lookup_conflict_impl
  is ‹uncurry (RETURN oo None_lookup_conflict)›
  :: ‹bool1_assn⇧k *⇩a lookup_clause_rel_assn⇧d →⇩a conflict_option_rel_assn›
  unfolding None_lookup_conflict_def conflict_option_rel_assn_def
    lookup_clause_rel_assn_def
  by sepref

sepref_register None_lookup_conflict
declare None_lookup_conflict_impl.refine[sepref_fr_rules]


definition extract_valuse_of_lookup_conflict :: ‹conflict_option_rel ⇒ bool› where
‹extract_valuse_of_lookup_conflict = (λ(b, (_, xs)). b)›


sepref_def extract_valuse_of_lookup_conflict_impl
  is ‹RETURN o extract_valuse_of_lookup_conflict›
  :: ‹conflict_option_rel_assn⇧k →⇩a bool1_assn›
  unfolding extract_valuse_of_lookup_conflict_def conflict_option_rel_assn_def
    lookup_clause_rel_assn_def
  by sepref

sepref_register extract_valuse_of_lookup_conflict
declare extract_valuse_of_lookup_conflict_impl.refine[sepref_fr_rules]

sepref_register isasat_lookup_merge_eq2 update_confl_tl_wl_heur

lemma update_confl_tl_wl_heur_alt_def:
  ‹update_confl_tl_wl_heur = (λL C (M, N, bnxs, Q, W, vm, clvls, cach, lbd, outl, stats). do {
      ASSERT (clvls ≥ 1);
      let L' = atm_of L;
      ASSERT(arena_is_valid_clause_idx N C);
      (bnxs, clvls, lbd, outl) ←
        if arena_length N C = 2 then isasat_lookup_merge_eq2 L M N C bnxs clvls lbd outl
        else isa_resolve_merge_conflict_gt2 M N C bnxs clvls lbd outl;
      let b = extract_valuse_of_lookup_conflict bnxs;
      let nxs = the_lookup_conflict bnxs;
      ASSERT(curry lookup_conflict_remove1_pre L nxs ∧ clvls ≥ 1);
      let nxs = lookup_conflict_remove1 L nxs;
      ASSERT(arena_act_pre N C);
      let N = mark_used N C;
      ASSERT(arena_act_pre N C);
      let N = arena_incr_act N C;
      ASSERT(vmtf_unset_pre L' vm);
      ASSERT(tl_trailt_tr_pre M);
      RETURN (False, (tl_trailt_tr M, N, (None_lookup_conflict b nxs), Q, W, isa_vmtf_unset L' vm,
          clvls - 1, cach, lbd, outl, stats))
   })›
  unfolding update_confl_tl_wl_heur_def
  by (auto intro!: ext bind_cong simp: None_lookup_conflict_def the_lookup_conflict_def
    extract_valuse_of_lookup_conflict_def Let_def)

sepref_def update_confl_tl_wl_fast_code
  is ‹uncurry2 update_confl_tl_wl_heur›
  :: ‹[λ((i, L), S). isasat_fast S]⇩a
   unat_lit_assn⇧k *⇩a sint64_nat_assn⇧k *⇩aisasat_bounded_assn⇧d → bool1_assn ×⇩a isasat_bounded_assn›
  supply [[goals_limit=1]] isasat_fast_length_leD[intro]
  unfolding update_confl_tl_wl_heur_alt_def isasat_bounded_assn_def
    PR_CONST_def
  apply (rewrite at ‹If (_ = ⌑)› snat_const_fold[where 'a=64])
  apply (annot_unat_const "TYPE (32)")
  unfolding fold_tuple_optimizations
  by sepref

declare update_confl_tl_wl_fast_code.refine[sepref_fr_rules]

sepref_register is_in_conflict_st atm_is_in_conflict_st_heur
sepref_def skip_and_resolve_loop_wl_D_fast
  is ‹skip_and_resolve_loop_wl_D_heur›
  :: ‹[λS. isasat_fast S]⇩a isasat_bounded_assn⇧d → isasat_bounded_assn›
  supply [[goals_limit=1]]
    skip_and_resolve_loop_wl_DI[intro]
    isasat_fast_after_skip_and_resolve_loop_wl_D_heur_inv[intro]
  unfolding skip_and_resolve_loop_wl_D_heur_def
  unfolding fold_tuple_optimizations
  apply (rewrite at ‹¬_ ∧ ¬ _› short_circuit_conv)
  by sepref (* slow *)

declare skip_and_resolve_loop_wl_D_fast.refine[sepref_fr_rules]

experiment
begin
  export_llvm
    get_count_max_lvls_heur_impl
    maximum_level_removed_eq_count_dec_fast_code
    is_decided_hd_trail_wl_fast_code
    lit_and_ann_of_propagated_st_heur_fast_code
    is_in_option_lookup_conflict_code
    atm_is_in_conflict_st_heur_fast_code
    lit_of_last_trail_fast_code
    tl_state_wl_heur_fast_code
    None_lookup_conflict_impl
    extract_valuse_of_lookup_conflict_impl
    update_confl_tl_wl_fast_code
    skip_and_resolve_loop_wl_D_fast

end



end