Theory IsaSAT_Restart_Reduce_LLVM

theory IsaSAT_Restart_Reduce_LLVM
  imports IsaSAT_Restart_Reduce_Defs IsaSAT_Setup_LLVM IsaSAT_VMTF_State_LLVM
begin


lemma schedule_next_reduce_st_alt_def:
  ‹schedule_next_reduce_st b S = (let (heur, S) = extract_heur_wl_heur S; heur = schedule_next_reduce b heur in update_heur_wl_heur heur S)›
  by (auto simp: schedule_next_reduce_st_def state_extractors Let_def intro!: ext split: isasat_int_splits)

sepref_def schedule_next_reduce_st_impl
  is ‹uncurry (RETURN oo schedule_next_reduce_st)›
  :: ‹word64_assn⇧k *⇩a isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  unfolding schedule_next_reduce_st_alt_def
  by sepref

lemmas [sepref_fr_rules] = irredandant_count.refine
lemmas [unfolded inline_direct_return_node_case, llvm_code] =
  get_irredundant_count_st_code_def[unfolded read_all_st_code_def]

lemma schedule_next_reduction_stI: ‹¬a < (10 :: 64 word) ⟹ a > 0›
  unfolding word_le_not_less[symmetric]
  apply (rule order.strict_trans2)
  prefer 2
  apply assumption
  by auto

sepref_def reduceint_impl
  is ‹uncurry0 (RETURN reduceint)›
  :: ‹unit_assn⇧k →⇩a word64_assn›
  unfolding reduceint_def
  by sepref

lemma schedule_next_reduction_stI2:
  ‹1 ≤ a ⟹ 0 < a› for a :: ‹64 word›
  unfolding word_le_not_less[symmetric]
  apply (rule order.strict_trans2)
  prefer 2
  apply assumption
  by auto

lemma schedule_next_reduction_stI3: ‹word_log2 n div 2 < 64› for n :: ‹64 word›
  using word_log2_max[of n] unfolding size_word_def
  by auto

sepref_def schedule_next_reduction_st_impl
  is ‹RETURN o schedule_next_reduction_st›
  :: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  supply [[goals_limit=1]]
  supply [simp] = schedule_next_reduction_stI schedule_next_reduction_stI3
  supply [intro] = schedule_next_reduction_stI2
  supply [split] = if_splits
  supply of_nat_snat[sepref_import_param]
  unfolding schedule_next_reduction_st_def max_def
  apply (rewrite in ‹_ >> ⌑› snat_const_fold[where 'a=64])

  apply (annot_unat_const ‹TYPE(64)›)
  by sepref

definition vmtf_array_nxt_score :: ‹vmtf ⇒ _› where ‹vmtf_array_nxt_score x = fst (snd x)›

lemma ‹current_vmtf_array_nxt_score x = (case x of Bump_Heuristics a b c d ⇒
  (vmtf_array_nxt_score b))›
  by (cases x) (auto simp: vmtf_array_nxt_score_def current_vmtf_array_nxt_score_def
    bump_get_heuristics_def)

lemma vmtf_array_nxt_score_alt_def: ‹RETURN o vmtf_array_nxt_score = (λ(a,b,c,d,e) . let b' = COPY b in RETURN b)›
  by (auto intro!: ext simp: vmtf_array_nxt_score_def)

find_theorems hn_refine PASS
sepref_def vmtf_array_nxt_score_code
  is ‹RETURN o vmtf_array_nxt_score›
  :: ‹vmtf_assn⇧k →⇩a uint64_nat_assn›
  unfolding vmtf_array_nxt_score_alt_def vmtf_assn_def
  by sepref

lemma current_vmtf_array_nxt_score_alt_def: ‹RETURN o current_vmtf_array_nxt_score = (λx. case x of Bump_Heuristics hstable focused foc a ⇒
    RETURN (vmtf_array_nxt_score focused))›
    by (auto intro!: ext simp: bump_get_heuristics_def current_vmtf_array_nxt_score_def vmtf_array_nxt_score_def
      split: bump_heuristics_splits)

sepref_def current_vmtf_array_nxt_score_code
  is ‹RETURN o current_vmtf_array_nxt_score›
  :: ‹heuristic_bump_assn⇧k →⇩a uint64_nat_assn›
  unfolding current_vmtf_array_nxt_score_alt_def
  by sepref


sepref_def find_local_restart_target_level_fast_code
  is ‹uncurry find_local_restart_target_level_int›
  :: ‹trail_pol_fast_assn⇧k *⇩a heuristic_bump_assn⇧k →⇩a uint32_nat_assn›
  supply [[goals_limit=1]] length_rev[simp del]
  unfolding find_local_restart_target_level_int_def find_local_restart_target_level_int_inv_def
    length_uint32_nat_def trail_pol_fast_assn_def
  apply (annot_unat_const ‹TYPE(32)›)
   apply (rewrite in ‹(_ ! _)› annot_unat_snat_upcast[where 'l=64])
   apply (rewrite in ‹(_ ! ⌑)› annot_unat_snat_upcast[where 'l=64])
   apply (rewrite in ‹(⌑ < length _)› annot_unat_snat_upcast[where 'l=64])
  by sepref


definition find_local_restart_target_level_st_fast_code :: ‹twl_st_wll_trail_fast2 ⇒ _› where
  ‹find_local_restart_target_level_st_fast_code = (read_all_st_code (λM _ _ _ _ N _ _ _ _ _ _ _ _ _ _ _. find_local_restart_target_level_fast_code M N))›

global_interpretation find_restart_lvl: read_trail_vmtf_param_adder0 where
  P = ‹λ_ _. True› and
  f' = ‹find_local_restart_target_level_int› and
  f = ‹find_local_restart_target_level_fast_code› and
  x_assn = ‹uint32_nat_assn›
  rewrites
    ‹(read_all_st (λM _ _ _ _ N _ _ _ _ _ _ _ _ _ _ _. find_local_restart_target_level_int M N)) = find_local_restart_target_level_st› and
    ‹(read_all_st_code (λM _ _ _ _ N _ _ _ _ _ _ _ _ _ _ _. find_local_restart_target_level_fast_code M N)) = find_local_restart_target_level_st_fast_code›
  apply unfold_locales
  apply (subst lambda_comp_true)
  apply (rule find_local_restart_target_level_fast_code.refine)
  subgoal by (auto simp: read_all_st_def find_local_restart_target_level_st_def
    intro!: ext split: isasat_int_splits)
  subgoal by (auto simp: find_local_restart_target_level_st_fast_code_def)
  done

lemmas [sepref_fr_rules] = find_restart_lvl.refine
lemmas [unfolded inline_direct_return_node_case, llvm_code] = find_local_restart_target_level_st_fast_code_def[unfolded read_all_st_code_def]

lemma empty_Q_alt_def:
  ‹empty_Q = (λS. do{
  let (M, S) = extract_trail_wl_heur S;
  let (heur, S) = extract_heur_wl_heur S;
  j ← mop_isa_length_trail M;
  RETURN (update_heur_wl_heur (restart_info_restart_done_heur heur) (update_literals_to_update_wl_heur j (update_trail_wl_heur M S)))
    })›
  by (auto simp: state_extractors empty_Q_def intro!: ext split: isasat_int_splits)

sepref_def empty_Q_fast_code
  is ‹empty_Q›
  :: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding empty_Q_alt_def
  by sepref

sepref_register cdcl_twl_local_restart_wl_D_heur
    empty_Q find_decomp_wl_st_int

sepref_def cdcl_twl_local_restart_wl_D_heur_fast_code
  is ‹cdcl_twl_local_restart_wl_D_heur›
  :: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn›
  unfolding cdcl_twl_local_restart_wl_D_heur_def PR_CONST_def
  supply [[goals_limit = 1]]
  by sepref

definition lbd_sort_clauses_raw :: ‹arena ⇒ vdom ⇒ nat ⇒ nat ⇒ nat list nres› where
  ‹lbd_sort_clauses_raw arena N = pslice_sort_spec idx_cdom clause_score_less arena N›

definition lbd_sort_clauses_avdom :: ‹arena ⇒ vdom ⇒ nat list nres› where
  ‹lbd_sort_clauses_avdom arena N = lbd_sort_clauses_raw arena N 0 (length N)›

lemmas LBD_introsort[sepref_fr_rules] =
  LBD_it.introsort_param_impl_correct[unfolded lbd_sort_clauses_raw_def[symmetric] PR_CONST_def]

sepref_register lbd_sort_clauses_raw
sepref_def lbd_sort_clauses_avdom_impl
  is ‹uncurry lbd_sort_clauses_avdom›
  :: ‹arena_fast_assn⇧k *⇩a vdom_fast_assn⇧d →⇩a vdom_fast_assn›
  supply[[goals_limit=1]]
  unfolding lbd_sort_clauses_avdom_def
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

sepref_register remove_deleted_clauses_from_avdom arena_status DELETED
lemma mark_to_delete_clauses_wl_D_heur_is_Some_iff:
  ‹D = Some C ⟷ D ≠ None ∧ ((the D) = C)›
  by auto

sepref_def mop_marked_as_used_impl
  is ‹uncurry mop_marked_as_used›
  :: ‹arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a unat_assn' TYPE(2)›
  supply [[goals_limit=1]]
  unfolding mop_marked_as_used_def
  by sepref

sepref_def MINIMUM_DELETION_LBD_impl
  is ‹uncurry0 (RETURN MINIMUM_DELETION_LBD)›
  :: ‹unit_assn⇧k →⇩a uint32_nat_assn›
  unfolding MINIMUM_DELETION_LBD_def
  apply (annot_unat_const ‹TYPE(32)›)
  by sepref

sepref_def isa_is_candidate_for_removal_impl
  is ‹uncurry2 isa_is_candidate_for_removal›
  :: ‹trail_pol_fast_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a arena_fast_assn⇧k →⇩a bool1_assn›
  unfolding isa_is_candidate_for_removal_def
  unfolding
    access_avdom_at_def[symmetric] length_avdom_def[symmetric]
    get_the_propagation_reason_heur_def[symmetric]
    clause_is_learned_heur_def[symmetric]
    clause_lbd_heur_def[symmetric]
    access_length_heur_def[symmetric]
    mark_to_delete_clauses_wl_D_heur_is_Some_iff
    marked_as_used_st_def[symmetric] if_conn(4)
    fold_tuple_optimizations
  supply [[goals_limit = 1]] of_nat_snat[sepref_import_param]
      length_avdom_def[symmetric, simp] access_avdom_at_def[simp]
  apply (rewrite in ‹let _ = ⌑ in _› short_circuit_conv)+
  apply (rewrite in ‹_ = 0› unat_const_fold[where 'a=2])
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

sepref_register isa_is_candidate_for_removal

sepref_def remove_deleted_clauses_from_avdom_fast_code
  is ‹uncurry2 isa_gather_candidates_for_reduction›
  :: ‹[λ((M, N), vdom). length (get_vdom_aivdom vdom) ≤ snat64_max]⇩a
  trail_pol_fast_assn⇧k *⇩a arena_fast_assn⇧d *⇩a aivdom_assn⇧d →
  arena_fast_assn ×⇩a aivdom_assn›
  supply [[goals_limit=1]]
  supply [simp] = length_avdom_aivdom_def
  unfolding isa_gather_candidates_for_reduction_def
    convert_swap gen_swap if_conn(4) length_avdom_aivdom_def[symmetric]
    avdom_aivdom_at_def[symmetric]
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref


definition lbd_sort_clauses :: ‹arena ⇒ aivdom2 ⇒ aivdom2 nres› where
  ‹lbd_sort_clauses arena N = map_tvdom_aivdom_int (lbd_sort_clauses_avdom arena) N›

sepref_def lbd_sort_clauses_impl
  is ‹uncurry lbd_sort_clauses›
  :: ‹[λ(N, vdom). length (fst vdom) ≤ snat64_max]⇩a arena_fast_assn⇧k *⇩a aivdom_int_assn⇧d → aivdom_int_assn›
  unfolding lbd_sort_clauses_def map_tvdom_aivdom_int_def
  by sepref

lemma
  map_vdom_aivdom_int2:
  ‹(uncurry (λarena. map_vdom_aivdom_int (f arena)), uncurry (λarena. map_vdom_aivdom (f arena)))
  ∈ Id ×⇩r aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel›
  apply (intro frefI nres_relI)
  subgoal for x y
    using map_vdom_aivdom_int[of ‹f (fst x)›]
    apply (cases x; cases y)
    apply (auto intro!: frefI nres_relI simp: fref_def nres_rel_def)
    done
  done

lemma get_aivdom_eq_aivdom_iff:
  ‹IsaSAT_VDom.get_aivdom b = (x1, a, aa, ba) ⟷ b = AIvdom (x1, a, aa, ba)›
  by (cases b) auto

lemma quicksort_clauses_by_score_sort:
  ‹(uncurry lbd_sort_clauses, uncurry sort_clauses_by_score) ∈
  Id ×⇩r aivdom_rel →⇩f ⟨aivdom_rel⟩nres_rel›
  apply (intro fun_relI nres_relI frefI)
  subgoal for arena arena'
    unfolding uncurry_def lbd_sort_clauses_def map_tvdom_aivdom_int_def
      lbd_sort_clauses_avdom_def lbd_sort_clauses_raw_def sort_clauses_by_score_def
    apply (refine_vcg)
    apply (rule specify_left)
    apply (auto simp: lbd_sort_clauses_def lbd_sort_clauses_raw_def
      pslice_sort_spec_def le_ASSERT_iff idx_cdom_def slice_rel_def br_def uncurry_def
      conc_fun_RES sort_spec_def map_vdom_aivdom_int_def lbd_sort_clauses_avdom_def
      code_hider_rel_def
      split:prod.splits
      intro!: ASSERT_leI 
      )
    apply (case_tac x2; auto)

    apply (rule order_trans)
    apply (rule slice_sort_spec_refine_sort)
    apply (auto simp: lbd_sort_clauses_def lbd_sort_clauses_raw_def
      pslice_sort_spec_def le_ASSERT_iff idx_cdom_def slice_rel_def br_def uncurry_def
      conc_fun_RES sort_spec_def map_vdom_aivdom_int_def lbd_sort_clauses_avdom_def
      code_hider_rel_def
      split:prod.splits
      intro!: ASSERT_leI 
      )
    apply (case_tac x2; auto simp: get_aivdom_eq_aivdom_iff)
    apply (rule_tac x = ‹AIvdom (x1a, ac, ad, x)› in exI)
    apply auto
    by (metis slice_complete)
  done

context
  notes [fcomp_norm_unfold] = aivdom_assn_alt_def[symmetric] aivdom_assn_def[symmetric]
begin

lemma lbd_sort_clauses_impl_lbd_sort_clauses[sepref_fr_rules]:
  ‹(uncurry lbd_sort_clauses_impl, uncurry sort_clauses_by_score)
  ∈ [λ(N, vdom). length (get_avdom_aivdom vdom) ≤ snat64_max]⇩a (al_assn arena_el_impl_assn)⇧k *⇩a aivdom_assn⇧d → aivdom_assn›
  (is ‹?c ∈ [?pre]⇩a ?im → ?f›)
proof -
  have H: ‹?c
∈ [comp_PRE (Id ×⇩f aivdom_rel) (λ_. True) (λx y. case y of (N, vdom) ⇒ length (fst vdom) ≤ snat64_max)
   (λx. nofail (uncurry sort_clauses_by_score x))]⇩a ?im → ?f›
    (is ‹_ ∈ [?pre']⇩a ?im' → _›)
    using hfref_compI_PRE[OF lbd_sort_clauses_impl.refine,
  OF quicksort_clauses_by_score_sort, unfolded fcomp_norm_unfold] by blast
  have pre: ‹?pre' x› if ‹?pre x› for x
    using that 
    by (case_tac x, case_tac ‹snd x›)
      (auto simp: comp_PRE_def code_hider_rel_def)
  show ?thesis
    apply (rule hfref_weaken_pre[OF ])
     defer
    using H apply assumption
    using pre ..
qed

end

lemma sort_vdom_heur_alt_def:
  ‹sort_vdom_heur = (λS⇩0. do {
    let (vdom, S) = extract_vdom_wl_heur S⇩0;
    ASSERT (vdom = get_aivdom S⇩0);
    let (M', S) = extract_trail_wl_heur S;
    ASSERT (M' = get_trail_wl_heur S⇩0);
    let (arena, S) = extract_arena_wl_heur S;
    ASSERT (arena = get_clauses_wl_heur S⇩0);
    ASSERT(length (get_avdom_aivdom vdom) ≤ length arena);
    ASSERT(length (get_vdom_aivdom vdom) ≤ length arena);
    (arena', vdom) ← isa_gather_candidates_for_reduction M' arena vdom;
    ASSERT(valid_sort_clause_score_pre arena (get_vdom_aivdom vdom));
    ASSERT(EQ (length arena) (length arena'));
    ASSERT(length (get_avdom_aivdom vdom) ≤ length arena);
    vdom ← sort_clauses_by_score arena' vdom;
    RETURN (update_arena_wl_heur arena' (update_vdom_wl_heur vdom (update_trail_wl_heur M' S)))
    })›
   by (auto intro!: ext split: isasat_int_splits simp: sort_vdom_heur_def state_extractors)

sepref_def sort_vdom_heur_fast_code
  is ‹sort_vdom_heur›
  :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max]⇩aisasat_bounded_assn⇧d → isasat_bounded_assn›
  supply [[goals_limit=1]]
  unfolding sort_vdom_heur_alt_def EQ_def
  by sepref

sepref_def find_largest_lbd_and_size_impl
  is ‹uncurry find_largest_lbd_and_size›
  :: ‹sint64_nat_assn⇧k *⇩a isasat_bounded_assn⇧k →⇩a uint32_nat_assn ×⇩a sint64_nat_assn›
  supply [simp] = length_tvdom_def[symmetric]
  supply [dest] = isasat_bounded_assn_length_arenaD
  unfolding find_largest_lbd_and_size_def access_tvdom_at_def[symmetric]
    length_tvdom_def[symmetric] max_def
  apply (rewrite at ‹(_, _, ⌑)› snat_const_fold[where 'a=64])
  apply (rewrite at ‹(⌑, _)› snat_const_fold[where 'a=64])
  apply (rewrite at ‹(_, ⌑, _)› unat_const_fold[where 'a=32])
  apply (annot_snat_const ‹TYPE(64)›)
  by sepref

experiment
begin
  export_llvm sort_vdom_heur_fast_code remove_deleted_clauses_from_avdom_fast_code
end

end