Theory IsaSAT_Restart_Defs

theory IsaSAT_Restart_Defs
  imports
    Watched_Literals.WB_Sort Watched_Literals.Watched_Literals_Watch_List_Simp IsaSAT_Rephase_State
    IsaSAT_Setup IsaSAT_VMTF IsaSAT_Sorting IsaSAT_Proofs
begin

lemma unbounded_id: ‹unbounded (id :: nat ⇒ nat)›
  by (auto simp: bounded_def) presburger

global_interpretation twl_restart_ops id
  by unfold_locales

global_interpretation twl_restart id
  by standard (rule unbounded_id)



definition twl_st_heur_restart :: ‹(isasat × nat twl_st_wl) set› where
[unfolded Let_def]: ‹twl_st_heur_restart =
  {(S,T).
  let M' = get_trail_wl_heur S; N' = get_clauses_wl_heur S; D' = get_conflict_wl_heur S;
    W' = get_watched_wl_heur S; j = literals_to_update_wl_heur S; outl = get_outlearned_heur S;
    cach = get_conflict_cach S; clvls = get_count_max_lvls_heur S;
    vm = get_vmtf_heur S;
    vdom = get_aivdom S; heur = get_heur S; old_arena = get_old_arena S;
    lcount = get_learned_count S; occs = get_occs S in
    let M = get_trail_wl T; N = get_clauses_wl T;  D = get_conflict_wl T;
      Q = literals_to_update_wl T;
      W = get_watched_wl T; N0 = get_init_clauses0_wl T; U0 = get_learned_clauses0_wl T;
      NS = get_subsumed_init_clauses_wl T; US = get_subsumed_learned_clauses_wl T;
      NEk = get_kept_unit_init_clss_wl T; UEk = get_kept_unit_learned_clss_wl T;
      NE = get_unkept_unit_init_clss_wl T; UE = get_unkept_unit_learned_clss_wl T in
    (M', M) ∈ trail_pol (all_init_atms N (NE+NEk+NS+N0)) ∧
    valid_arena N' N (set (get_vdom_aivdom vdom)) ∧
    (D', D) ∈ option_lookup_clause_rel (all_init_atms N (NE+NEk+NS+N0)) ∧
    (D = None ⟶ j ≤ length M) ∧
    Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
    (W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_init_atms N (NE+NEk+NS+N0))) ∧
    vm ∈ bump_heur (all_init_atms N (NE+NEk+NS+N0)) M ∧
    no_dup M ∧
    clvls ∈ counts_maximum_level M D ∧
    cach_refinement_empty (all_init_atms N (NE+NEk+NS+N0)) cach ∧
    out_learned M D outl ∧
    clss_size_corr_restart N NE {#} NEk UEk NS {#} N0 {#} lcount ∧
    vdom_m (all_init_atms N (NE+NEk+NS+N0)) W N ⊆ set (get_vdom_aivdom vdom) ∧
    aivdom_inv_dec vdom (dom_m N) ∧
    isasat_input_bounded (all_init_atms N (NE+NEk+NS+N0)) ∧
    isasat_input_nempty (all_init_atms N (NE+NEk+NS+N0)) ∧
    old_arena = [] ∧
      heuristic_rel (all_init_atms N (NE+NEk+NS+N0)) heur ∧
    (occs, empty_occs_list (all_init_atms N (NE+NEk+NS+N0))) ∈ occurrence_list_ref
  }›


abbreviation twl_st_heur'''' where
  ‹twl_st_heur'''' r ≡ {(S, T). (S, T) ∈ twl_st_heur ∧ length (get_clauses_wl_heur S) ≤ r}›

abbreviation twl_st_heur''''uu where
  ‹twl_st_heur''''uu r u ≡ {(S, T). (S, T) ∈ twl_st_heur ∧ length (get_clauses_wl_heur S) ≤ r ∧
    learned_clss_count S ≤ u}›

abbreviation twl_st_heur_restart''' where
  ‹twl_st_heur_restart''' r ≡
    {(S, T). (S, T) ∈ twl_st_heur_restart ∧ length (get_clauses_wl_heur S) = r}›

abbreviation twl_st_heur_restart'''' where
  ‹twl_st_heur_restart'''' r ≡
    {(S, T). (S, T) ∈ twl_st_heur_restart ∧ length (get_clauses_wl_heur S) ≤ r}›

definition twl_st_heur_restart_ana :: ‹nat ⇒ (isasat × nat twl_st_wl) set› where
‹twl_st_heur_restart_ana r =
  {(S, T). (S, T) ∈ twl_st_heur_restart ∧ length (get_clauses_wl_heur S) = r}›

abbreviation twl_st_heur_restart_ana' :: ‹_› where
  ‹twl_st_heur_restart_ana' r u ≡
    {(S, T). (S, T) ∈ twl_st_heur_restart_ana r ∧ learned_clss_count S ≤ u}›

definition empty_Q :: ‹isasat ⇒ isasat nres› where
  ‹empty_Q = (λS. do{
  j ← mop_isa_length_trail (get_trail_wl_heur S);
  RETURN (set_heur_wl_heur (restart_info_restart_done_heur (get_heur S)) (set_literals_to_update_wl_heur j S))
  })›

definition remove_all_annot_true_clause_one_imp_heur
  :: ‹nat × clss_size × arena ⇒ (clss_size × arena) nres›
where
‹remove_all_annot_true_clause_one_imp_heur = (λ(C, j, N). do {
      case arena_status N C of
        DELETED ⇒ RETURN (j, N)
      | IRRED ⇒ RETURN (j, extra_information_mark_to_delete N C)
      | LEARNED ⇒ RETURN (clss_size_decr_lcount j, extra_information_mark_to_delete N C)
  })›

definition number_clss_to_keep :: ‹isasat ⇒ nat nres› where
  ‹number_clss_to_keep = (λS.
    RES UNIV)›

definition number_clss_to_keep_impl :: ‹isasat ⇒ nat nres› where
  ‹number_clss_to_keep_impl = (λS.
    RETURN (length_tvdom_aivdom (get_aivdom S) >> 2))›

(* TODO Missing : The sorting function + definition of l should depend on the number of initial
  clauses *)
definition (in -) MINIMUM_DELETION_LBD :: nat where
  ‹MINIMUM_DELETION_LBD = 3›

definition trail_update_reason_at :: ‹_ ⇒ _ ⇒ trail_pol ⇒ _› where
  ‹trail_update_reason_at ≡ (λL C (M, val, lvls, reason, k). (M, val, lvls, reason[atm_of L := C], k))›

abbreviation trail_get_reason :: ‹trail_pol ⇒ _› where
  ‹trail_get_reason ≡ (λ(M, val, lvls, reason, k). reason)›

definition replace_reason_in_trail :: ‹nat literal ⇒ _› where
  ‹replace_reason_in_trail L C = (λM. do {
    ASSERT(atm_of L < length (trail_get_reason M));
    RETURN (trail_update_reason_at L 0 M)
  })›

definition isasat_replace_annot_in_trail
  :: ‹nat literal ⇒ nat ⇒ isasat ⇒ isasat nres›
  where
  ‹isasat_replace_annot_in_trail L C = (λS. do {
    let lcount = clss_size_resetUS0 (get_learned_count S);
    M ← replace_reason_in_trail L C (get_trail_wl_heur S);
    RETURN (set_trail_wl_heur M (set_learned_count_wl_heur lcount S))
  })›

definition remove_one_annot_true_clause_one_imp_wl_D_heur
  :: ‹nat ⇒ isasat ⇒ (nat × isasat) nres›
where
‹remove_one_annot_true_clause_one_imp_wl_D_heur = (λi S⇩0. do {
      (L, C) ← do {
        L ← isa_trail_nth (get_trail_wl_heur S⇩0) i;
	C ← get_the_propagation_reason_pol (get_trail_wl_heur S⇩0) L;
	RETURN (L, C)};
      ASSERT(C ≠ None ∧ i + 1 ≤ Suc (unat32_max div 2));
      if the C = 0 then RETURN (i+1, S⇩0)
      else do {
        ASSERT(C ≠ None);
        S ← isasat_replace_annot_in_trail L (the C) S⇩0;
        log_del_clause_heur S (the C);
	ASSERT(mark_garbage_pre (get_clauses_wl_heur S, the C) ∧ arena_is_valid_clause_vdom (get_clauses_wl_heur S) (the C) ∧ learned_clss_count S ≤ learned_clss_count S⇩0);
        S ← mark_garbage_heur4 (the C) S;
        ― ‹\<^text>‹S ← remove_all_annot_true_clause_imp_wl_D_heur L S;››
        RETURN (i+1, S)
      }
  })›

definition cdcl_twl_full_restart_wl_D_GC_prog_heur_post :: ‹isasat ⇒ isasat ⇒ bool› where
‹cdcl_twl_full_restart_wl_D_GC_prog_heur_post S T ⟷
  (∃S' T'. (S, S') ∈ twl_st_heur_restart ∧ (T, T') ∈ twl_st_heur_restart ∧
    cdcl_twl_full_restart_wl_GC_prog_post S' T')›

definition remove_one_annot_true_clause_imp_wl_D_heur_inv
  :: ‹isasat ⇒ (nat × isasat) ⇒ bool› where
  ‹remove_one_annot_true_clause_imp_wl_D_heur_inv S = (λ(i, T).
    (∃S' T'. (S, S') ∈ twl_st_heur_restart ∧ (T, T') ∈ twl_st_heur_restart ∧
     remove_one_annot_true_clause_imp_wl_inv S' (i, T') ∧
     learned_clss_count T ≤ learned_clss_count S))›

definition empty_US  :: ‹'v twl_st_wl ⇒ 'v twl_st_wl› where
  ‹empty_US = (λ(M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W).
  (M', N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W))›


definition trail_zeroed_until_state where
  ‹trail_zeroed_until_state S = trail_zeroed_until (get_trail_wl_heur S)›

definition trail_set_zeroed_until_state where
  ‹trail_set_zeroed_until_state z S = (let M = get_trail_wl_heur S in set_trail_wl_heur (trail_set_zeroed_until z M) S)›

definition remove_one_annot_true_clause_imp_wl_D_heur :: ‹isasat ⇒ isasat nres›
where
‹remove_one_annot_true_clause_imp_wl_D_heur = (λS. do {
    ASSERT((isa_length_trail_pre o get_trail_wl_heur) S);
    k ← (if count_decided_st_heur S = 0
      then RETURN (isa_length_trail (get_trail_wl_heur S))
      else get_pos_of_level_in_trail_imp (get_trail_wl_heur S) 0);
    let start = trail_zeroed_until_state S;
    (i, T) ← WHILE⇩T⇗remove_one_annot_true_clause_imp_wl_D_heur_inv S⇖
      (λ(i, S). i < k)
      (λ(i, S). do { (j, S) ← remove_one_annot_true_clause_one_imp_wl_D_heur i S; RETURN (j, trail_set_zeroed_until_state j S)})
      (start, S);
    ASSERT (remove_one_annot_true_clause_imp_wl_D_heur_inv S (i, T));
    let T = trail_set_zeroed_until_state i T;
    RETURN (empty_US_heur T)
  })›

definition GC_units_required :: ‹isasat ⇒ bool› where
  ‹GC_units_required T ⟷ units_since_last_GC_st T ≥ get_GC_units_opt T›


definition FLAG_no_restart :: ‹8 word› where
  ‹FLAG_no_restart = 0›

definition FLAG_restart :: ‹8 word› where
  ‹FLAG_restart = 1›

definition FLAG_Reduce_restart :: ‹8 word› where
  ‹FLAG_Reduce_restart = 3›

definition FLAG_GC_restart :: ‹8 word› where
  ‹FLAG_GC_restart = 2›

definition FLAG_Inprocess_restart :: ‹8 word› where
  ‹FLAG_Inprocess_restart = 4›


definition max_restart_decision_lvl :: nat where
  ‹max_restart_decision_lvl = 300›

definition max_restart_decision_lvl_code :: ‹32 word› where
  ‹max_restart_decision_lvl_code = 300›

definition GC_required_heur :: ‹isasat ⇒ nat ⇒ bool nres› where
  ‹GC_required_heur S n = do {
    n ← RETURN (full_arena_length_st S);
    wasted ← RETURN (wasted_bytes_st S);
    RETURN (3*wasted > ((of_nat n)>>2))
 }›

definition minimum_number_between_restarts :: ‹64 word› where
  ‹minimum_number_between_restarts = 50›

definition upper_restart_bound_reached :: ‹isasat ⇒ bool› where
  ‹upper_restart_bound_reached = (λS. get_global_conflict_count S ≥ next_reduce_schedule_st S)›

definition should_subsume_st :: ‹isasat ⇒ bool› where
  ‹should_subsume_st S ⟷ get_subsumption_opts S ∧
      (get_global_conflict_count S > next_subsume_schedule_st S)›

definition should_eliminate_pure_st :: ‹isasat ⇒ bool› where
  ‹should_eliminate_pure_st S ⟷
      (get_global_conflict_count S > next_pure_lits_schedule_st S)›

definition should_inprocess_st :: ‹isasat ⇒ bool› where
  ‹should_inprocess_st S ⟷
      (should_subsume_st S ∨ should_eliminate_pure_st S)›

definition iterate_over_VMTFC where
  ‹iterate_over_VMTFC = (λf (I :: 'a ⇒ bool) P (ns :: (nat, nat) vmtf_node list, n) x. do {
      (_, x) ← WHILE⇩T⇗λ(n, x). I x⇖
        (λ(n, x). n ≠ None ∧ P x)
        (λ(n, x). do {
          ASSERT(n ≠ None);
          let A = the n;
          ASSERT(A < length ns);
          ASSERT(A ≤ unat32_max div 2);
          x ← f A x;
          RETURN (get_next ((ns ! A)), x)
        })
        (n, x);
      RETURN x
    })›

definition iterate_over_VMTF :: ‹_› where
  iterate_over_VMTF_alt_def: ‹iterate_over_VMTF f I  = iterate_over_VMTFC f I (λ_. True)›

definition arena_header_size :: ‹arena ⇒ nat ⇒ nat› where
  ‹arena_header_size arena C =
  (if arena_length arena C > 4 then MAX_HEADER_SIZE else MIN_HEADER_SIZE)›

definition update_restart_phases :: ‹isasat ⇒ isasat nres› where
  ‹update_restart_phases = (λS. do {
     let heur = get_heur S;
     let lcount = get_global_conflict_count S;
     let vm = get_vmtf_heur S;
     let vm = switch_bump_heur vm;
     heur ← RETURN (incr_restart_phase heur);
     heur ← RETURN (incr_restart_phase_end lcount heur);
     heur ← RETURN (if current_restart_phase heur = STABLE_MODE then heuristic_reluctant_enable heur else heuristic_reluctant_disable heur);
     heur ← RETURN (swap_emas heur);
     RETURN (set_heur_wl_heur heur (set_vmtf_wl_heur vm S))
  })›


(*TODO used: in Restart_Reduce_Defs only?*)
definition restart_abs_wl_heur_pre  :: ‹isasat ⇒ bool ⇒ bool› where
  ‹restart_abs_wl_heur_pre S brk  ⟷ (∃T last_GC last_Restart. (S, T) ∈ twl_st_heur ∧ restart_abs_wl_pre T last_GC last_Restart brk)›

lemma valid_arena_header_size:
  ‹valid_arena arena N vdom ⟹ C ∈# dom_m N ⟹ arena_header_size arena C = header_size (N ∝ C)›
  by (auto simp: arena_header_size_def header_size_def arena_lifting)


definition rewatch_heur_st_pre :: ‹isasat ⇒ bool› where
  ‹rewatch_heur_st_pre S ⟷ (∀i < length (get_tvdom S). get_tvdom S ! i ≤ snat64_max)›

lemma isasat_GC_clauses_wl_D_rewatch_pre:
  assumes
    ‹length (get_clauses_wl_heur x) ≤ snat64_max› and
    ‹length (get_clauses_wl_heur xc) ≤ length (get_clauses_wl_heur x)› and
    ‹∀i ∈ set (get_tvdom xc). i ≤ length (get_clauses_wl_heur x)›
  shows ‹rewatch_heur_st_pre xc›
  using assms
  unfolding rewatch_heur_st_pre_def all_set_conv_all_nth
  by auto

end