Theory IsaSAT_Restart_Heuristics

theory IsaSAT_Restart_Heuristics
imports
  IsaSAT_Restart_Heuristics_Defs
  IsaSAT_Restart_Reduce IsaSAT_Restart_Inprocessing
begin


lemma cdcl_twl_full_restart_wl_D_GC_heur_prog_alt_def:
  ‹cdcl_twl_full_restart_wl_D_GC_heur_prog S0 = do {
    S ← do {
    if count_decided_st_heur S0 > 0
    then do {
    S ← find_decomp_wl_st_int 0 S0;
    empty_Q (empty_US_heur S)
    } else RETURN (empty_US_heur S0)
    };
    ASSERT(length (get_clauses_wl_heur S) = length (get_clauses_wl_heur S0));
    ASSERT(learned_clss_count S ≤ learned_clss_count S0);
    T ← remove_one_annot_true_clause_imp_wl_D_heur S;
    ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S0));
    ASSERT(learned_clss_count T ≤ learned_clss_count S0);
    U ← mark_to_delete_clauses_GC_wl_D_heur T;
    ASSERT(length (get_clauses_wl_heur U) = length (get_clauses_wl_heur S0));
    ASSERT(learned_clss_count U ≤ learned_clss_count S0);
    V ← isasat_GC_clauses_wl_D False U;
    RETURN (clss_size_resetUS0_st V)
  }›
  unfolding cdcl_twl_full_restart_wl_D_GC_heur_prog_def IsaSAT_Profile.start_def
    IsaSAT_Profile.stop_def by auto

lemma twl_st_heur_twl_st_heur_loopD:
  ‹(S, T) ∈ twl_st_heur ⟹ (S, T) ∈ twl_st_heur_loop› and
  twl_st_heur_loop_twl_st_heurD:
  ‹(S, T) ∈ twl_st_heur_loop ⟹ get_conflict_wl T = None ⟹ (S, T) ∈ twl_st_heur›
  by (auto simp: twl_st_heur_loop_def twl_st_heur_def)

lemma
    cdcl_twl_full_restart_wl_GC_prog_pre_heur:
      ‹cdcl_twl_full_restart_wl_GC_prog_pre T ⟹
        (S, T) ∈ twl_st_heur''' r ⟹ (S, T) ∈ twl_st_heur_restart_ana r› (is ‹_ ⟹ ?Apre ⟹ ?A›) and
     cdcl_twl_full_restart_wl_D_GC_prog_post_heur:
       ‹cdcl_twl_full_restart_wl_GC_prog_post S0 T ⟹
       (S, T) ∈ twl_st_heur_restart ⟹ (clss_size_resetUS0_st S, T) ∈ twl_st_heur›  (is ‹_ ⟹ _?Bpre ⟹ ?B›) and
     cdcl_twl_full_restart_wl_D_GC_prog_post_confl_heur:
       ‹cdcl_twl_full_restart_wl_GC_prog_post_confl S0 T ⟹
      (S, T) ∈ twl_st_heur_restart ⟹ get_conflict_wl T ≠ None ⟹
     (S, T) ∈ twl_st_heur_loop›  (is ‹_ ⟹ ?Cpre ⟹ ?Cconfl ⟹ ?C›)
proof -
  note cong = trail_pol_cong heuristic_rel_cong
      option_lookup_clause_rel_cong D⇩0_cong isa_vmtf_cong phase_saving_cong
      cach_refinement_empty_cong vdom_m_cong isasat_input_nempty_cong
      isasat_input_bounded_cong empty_occs_list_cong

  show ‹cdcl_twl_full_restart_wl_GC_prog_pre T ⟹ ?Apre ⟹ ?A›
    supply [[goals_limit=1]]
    unfolding cdcl_twl_full_restart_wl_GC_prog_pre_def cdcl_twl_full_restart_l_GC_prog_pre_def
    apply normalize_goal+
    subgoal for U V
      using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(3)[of T U V]
        cong[of ‹all_atms_st T› ‹all_init_atms_st T›]
	vdom_m_cong[of ‹all_atms_st T› ‹all_init_atms_st T› ‹get_watched_wl T› ‹get_clauses_wl T›]
      apply -
      apply (simp_all del: isasat_input_nempty_def isasat_input_bounded_def)
      apply (cases S; cases T)
      by (auto simp add: twl_st_heur_def twl_st_heur_restart_ana_def all_atms_st_def
        clss_size_corr_restart_def clss_size_corr_def
        twl_st_heur_restart_def all_init_atms_st_def simp del: isasat_input_nempty_def)
    done
  show ‹cdcl_twl_full_restart_wl_GC_prog_post S0 T ⟹ ?Bpre ⟹ ?B›
    supply [[goals_limit=1]]
    unfolding cdcl_twl_full_restart_wl_GC_prog_post_def
       cdcl_twl_full_restart_wl_GC_prog_post_def
       cdcl_twl_full_restart_l_GC_prog_pre_def
    apply normalize_goal+
    subgoal for S0' T' S0''
      apply (rule rtranclp_cdcl_twl_restart_l_inp_cdcl_twl_restart_inp[of S0' T' S0''], assumption+)
      apply (frule rtranclp_cdcl_twl_inp_twl_struct_invs, assumption+)
      subgoal for V
        using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(3)[of T T']
          cong[of ‹all_init_atms_st T› ‹all_atms_st T›]
          vdom_m_cong[of ‹all_init_atms_st T› ‹all_atms_st T› ‹get_watched_wl T› ‹get_clauses_wl T›]
          cdcl_twl_restart_l_invs[of S0' S0'' T']
        apply -
        apply (cases S; cases T)
        by (auto simp add: twl_st_heur_def twl_st_heur_restart_def all_atms_st_def all_init_atms_st_def
            clss_size_resetUS0_st_def
          simp del: isasat_input_nempty_def intro: clss_size_corr_restart_clss_size_corr)
      done
    done
  show ‹cdcl_twl_full_restart_wl_GC_prog_post_confl S0 T ⟹ ?Cpre ⟹ ?Cconfl ⟹ ?C›
    supply [[goals_limit=1]]
    unfolding cdcl_twl_full_restart_wl_GC_prog_post_confl_def
       cdcl_twl_full_restart_wl_GC_prog_post_def
       cdcl_twl_full_restart_l_GC_prog_pre_def
    apply normalize_goal+
    subgoal for S0' T' S0''
      apply (rule rtranclp_cdcl_twl_restart_l_inp_cdcl_twl_restart_inp[of S0' T' S0''], assumption+)
      apply (frule rtranclp_cdcl_twl_inp_twl_struct_invs, assumption+)
      subgoal for V
        using literals_are_ℒ⇩i⇩n'_literals_are_ℒ⇩i⇩n_iff(3)[of T T']
          cong[of ‹all_init_atms_st T› ‹all_atms_st T›]
          vdom_m_cong[of ‹all_init_atms_st T› ‹all_atms_st T› ‹get_watched_wl T› ‹get_clauses_wl T›]
          cdcl_twl_restart_l_invs[of S0' S0'' T']
        apply -
        apply (cases S; cases T)
        by (clarsimp simp add: twl_st_heur_loop_def twl_st_heur_restart_def all_atms_st_def all_init_atms_st_def
          ac_simps
          simp del: isasat_input_nempty_def)
      done
    done
qed

lemma cdcl_twl_full_restart_wl_D_GC_heur_prog:
  ‹(cdcl_twl_full_restart_wl_D_GC_heur_prog, cdcl_twl_full_restart_wl_GC_prog) ∈
    twl_st_heur''''u r u →⇩f ⟨twl_st_heur''''uu r u⟩nres_rel›
proof -
  have H: ‹(S, S') ∈ twl_st_heur_restart_ana r ⟹
       (S, S')  ∈ twl_st_heur_restart_ana' r (learned_clss_count S)› for S S'
    by auto
  have H2: ‹(x, y) ∈ IsaSAT_Setup.twl_st_heur''''u r u ⟹
     cdcl_twl_full_restart_wl_GC_prog_pre y ⟹
    (x, y) ∈ twl_st_heur_restart_ana' r (learned_clss_count x)› for x y
    using cdcl_twl_full_restart_wl_GC_prog_pre_heur[of y x r]
    by auto
  have UUa: ‹(U, Ua) ∈ twl_st_heur_restart_ana' r u ⟹
    (U, Ua) ∈ twl_st_heur_restart'''u r u› for U Ua r u
    by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
  show ?thesis
    unfolding cdcl_twl_full_restart_wl_D_GC_heur_prog_alt_def
      cdcl_twl_full_restart_wl_GC_prog_def
    apply (intro frefI nres_relI)
    apply (refine_rcg cdcl_twl_local_restart_wl_spec0
      remove_one_annot_true_clause_imp_wl_D_heur_remove_one_annot_true_clause_imp_wl_D[where r=r, THEN fref_to_Down]
      mark_to_delete_clauses_wl_D_heur_mark_to_delete_clauses_GC_wl_D[where r=r, THEN fref_to_Down]
      isasat_GC_clauses_wl_D[where r=r, THEN fref_to_Down])
    apply (rule H2; assumption)
    subgoal
      unfolding cdcl_twl_full_restart_wl_GC_prog_pre_def
        cdcl_twl_full_restart_l_GC_prog_pre_def
      by normalize_goal+ auto
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    apply (assumption)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    apply (assumption)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    apply (rule UUa; assumption)
    subgoal for x y S S' T T' U U' V V'
      using learned_clss_count_clss_size_resetUS0_st_le[of V]
      unfolding mem_Collect_eq prod.case
      apply (intro conjI cdcl_twl_full_restart_wl_D_GC_prog_post_heur)
      apply assumption+
      by auto
    done
qed

lemma cdcl_twl_full_restart_wl_D_inprocess_heur_prog_alt_def:
‹cdcl_twl_full_restart_wl_D_inprocess_heur_prog S0 = do {
    S ← do {
      if count_decided_st_heur S0 > 0
      then do {
        S ← find_decomp_wl_st_int 0 S0;
        empty_Q (empty_US_heur S)
      } else RETURN (empty_US_heur S0)
    };
    ASSERT(length (get_clauses_wl_heur S) = length (get_clauses_wl_heur S0));
    ASSERT(learned_clss_count S ≤ learned_clss_count S0);
    T ← remove_one_annot_true_clause_imp_wl_D_heur S;
    ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S0));
        ASSERT(learned_clss_count T ≤ learned_clss_count S0);
    T ← isa_mark_duplicated_binary_clauses_as_garbage_wl2 T;
    ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S0));
        ASSERT(learned_clss_count T ≤ learned_clss_count S0);
    T ← isa_forward_subsume T;
    ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S0));
        ASSERT(learned_clss_count T ≤ learned_clss_count S0);
    T ← isa_pure_literal_eliminate T;
    ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S0));
    ASSERT(learned_clss_count T ≤ learned_clss_count S0);
    T ← isa_simplify_clauses_with_units_st_wl2 T;
    ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S0));
    ASSERT(learned_clss_count T ≤ learned_clss_count S0);
    if ¬get_conflict_wl_is_None_heur T then RETURN T
    else do {
      U ← mark_to_delete_clauses_GC_wl_D_heur T;
      ASSERT(length (get_clauses_wl_heur U) = length (get_clauses_wl_heur S0));
      ASSERT(learned_clss_count U ≤ learned_clss_count S0);
      V ← isasat_GC_clauses_wl_D True U;
      RETURN (clss_size_resetUS0_st V)
   }
  }›
  unfolding cdcl_twl_full_restart_wl_D_inprocess_heur_prog_def IsaSAT_Profile.start_def
    IsaSAT_Profile.stop_def by (auto intro!: bind_cong[OF refl])

text ‹We need the plus one if we derive the empty conflict...

  TODO: we don't care about that case and can live with an overflow!›
abbreviation twl_st_heur''''u'
   :: ‹nat ⇒ nat ⇒ (isasat × nat twl_st_wl) set›
where
‹twl_st_heur''''u' r u ≡ {(S, T). (S, T) ∈ twl_st_heur ∧
           length (get_clauses_wl_heur S) = r ∧
           (get_conflict_wl T = None ⟶ learned_clss_count S ≤ u) ∧
           (get_conflict_wl T ≠ None ⟶ learned_clss_count S ≤ u+1)}›


lemma isa_simplify_clauses_with_unit_st2_isa_simplify_clauses_with_unit_wl:
  assumes ‹(S,S') ∈ twl_st_heur_restart_ana' r u›
  shows
    ‹isa_simplify_clauses_with_units_st_wl2 S ≤ ⇓ (twl_st_heur_restart_ana' r u) (simplify_clauses_with_units_st_wl S')›
  apply (rule order_trans)
    defer
  apply (rule ref_two_step')
  apply (rule simplify_clauses_with_units_st_wl2_simplify_clauses_with_units_st_wl[unfolded Down_id_eq, of _ S'])
  subgoal by auto
  subgoal
    apply (rule isa_simplify_clauses_with_units_st2_simplify_clauses_with_units_st2[THEN order_trans, of _ S'])
    apply (rule assms)
    subgoal using assms by auto
    done
  done

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

lemma cdcl_twl_full_restart_wl_D_inprocess_heur_prog:
  ‹(cdcl_twl_full_restart_wl_D_inprocess_heur_prog, cdcl_twl_full_restart_inprocess_wl_prog) ∈
    twl_st_heur''''u r u →⇩f ⟨twl_st_heur_loop''''uu r u⟩nres_rel›
proof -
  have H: ‹(S, S') ∈ twl_st_heur_restart_ana r ⟹
       (S, S')  ∈ twl_st_heur_restart_ana' r (learned_clss_count S)› for S S'
    by auto
  have H2: ‹(x, y) ∈ IsaSAT_Setup.twl_st_heur''''u r u ⟹
     cdcl_twl_full_restart_wl_GC_prog_pre y ⟹
    (x, y) ∈ twl_st_heur_restart_ana' r (learned_clss_count x)› for x y
    using cdcl_twl_full_restart_wl_GC_prog_pre_heur[of y x r]
    by auto
  have UUa: ‹(U, Ua) ∈ twl_st_heur_restart_ana' r u ⟹
    (U, Ua) ∈ twl_st_heur_restart'''u r u› for U Ua r u
    by (auto simp: twl_st_heur_restart_ana_def twl_st_heur_restart_def)
  show ?thesis
    unfolding cdcl_twl_full_restart_wl_D_inprocess_heur_prog_alt_def
      cdcl_twl_full_restart_inprocess_wl_prog_def
    apply (intro frefI nres_relI)
    apply (refine_rcg cdcl_twl_local_restart_wl_spec0
      remove_one_annot_true_clause_imp_wl_D_heur_remove_one_annot_true_clause_imp_wl_D[where r=r, THEN fref_to_Down]
      mark_to_delete_clauses_wl_D_heur_mark_to_delete_clauses_GC_wl_D[where r=r, THEN fref_to_Down]
      isasat_GC_clauses_wl_D[where r=r, THEN fref_to_Down]
      isa_simplify_clauses_with_unit_st2_isa_simplify_clauses_with_unit_wl[where r=r]
      isa_mark_duplicated_binary_clauses_as_garbage_wl_mark_duplicated_binary_clauses_as_garbage_wl2[where r=r]
      isa_pure_literal_eliminate[where r=r]
      isa_forward_subsume_forward_subsume_wl[where r=r])
    apply (rule H2; assumption)
    subgoal
      unfolding cdcl_twl_full_restart_wl_GC_prog_pre_def
        cdcl_twl_full_restart_l_GC_prog_pre_def
      by normalize_goal+ auto
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    apply (assumption)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    apply (solves auto)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    apply (assumption)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    apply (assumption)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    apply (assumption)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal
      by (subst get_conflict_wl_is_None_heur_get_conflict_wl_is_None_ana[THEN fref_to_Down_unRET_Id])
        (auto simp: get_conflict_wl_is_None_def)
    subgoal for x y
      unfolding mem_Collect_eq prod.case
      apply (subst cdcl_twl_full_restart_wl_D_GC_prog_post_confl_heur)
      apply assumption
      by (auto simp: twl_st_heur_restart_ana_def)
    apply (assumption)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    subgoal by (auto simp: twl_st_heur_restart_ana_def)
    apply (rule UUa; assumption)
    subgoal for x y S S' T T' U U' V V' W W' X X' Y Y' Z Z'
      using learned_clss_count_clss_size_resetUS0_st_le[of Z]
      unfolding mem_Collect_eq prod.case
      apply (intro conjI )
      by (auto intro: twl_st_heur_twl_st_heur_loopD intro!: cdcl_twl_full_restart_wl_D_GC_prog_post_heur)
    done
qed

lemma restart_required_heur_restart_required_wl0:
  ‹(uncurry3 restart_required_heur, uncurry3 restart_required_wl) ∈
    [λ(((S, _), _), _). (get_init_clauses0_wl S = {#} ∧ get_learned_clauses0_wl S = {#})]⇩f
    twl_st_heur''' r ×⇩f nat_rel ×⇩f nat_rel ×⇩f nat_rel → ⟨restart_flag_rel⟩nres_rel›
    unfolding restart_required_heur_def restart_required_wl_def uncurry_def Let_def
      restart_flag_rel_def  FLAG_GC_restart_def FLAG_restart_def FLAG_no_restart_def
      GC_required_heur_def FLAG_Reduce_restart_def learned_clss_count_def
      FLAG_Inprocess_restart_def
    apply (intro frefI nres_relI)
    apply refine_rcg
    subgoal
      by
       (auto simp add: twl_st_heur_def get_learned_clss_wl_def clss_size_lcountU0_def
        clss_size_def clss_size_lcount_def clss_size_lcountUE_def clss_size_corr_def
        clss_size_lcountUS_def clss_size_lcountUEk_def get_unit_learned_clss_wl_alt_def)
    subgoal
      by
       (auto simp add: twl_st_heur_def get_learned_clss_wl_def clss_size_lcountU0_def
        clss_size_def clss_size_lcount_def clss_size_lcountUE_def clss_size_corr_def
        clss_size_lcountUS_def clss_size_lcountUEk_def get_unit_learned_clss_wl_alt_def)
    subgoal
      by (clarsimp split: if_splits simp add: twl_st_heur_def RETURN_RES_refine_iff)
        (clarsimp simp add: twl_st_heur_def get_learned_clss_wl_def clss_size_corr_def
          clss_size_def clss_size_lcount_def clss_size_lcountUE_def RETURN_RES_refine_iff
         clss_size_lcountUS_def clss_size_lcountU0_def clss_size_lcountUEk_def ac_simps
        get_unit_learned_clss_wl_alt_def)
   done

lemma restart_prog_wl_D_heur_alt_def:
  ‹restart_prog_wl_D_heur S last_GC last_Restart n brk =
    (if brk then RETURN (S, last_GC, last_Restart, n)
    else do {
    b ← restart_required_heur S last_GC last_Restart n;
    if b = FLAG_restart
    then do {
       T ← cdcl_twl_restart_wl_heur S;
       ASSERT(learned_clss_count T ≤ learned_clss_count S);
       RETURN (T, last_GC, learned_clss_count T, n)
    }
    else if b ≠ FLAG_no_restart
    then if b ≠ FLAG_Inprocess_restart then do {
       let b = b;
       T ← (if b = FLAG_Reduce_restart
          then cdcl_twl_mark_clauses_to_delete S
          else  cdcl_twl_full_restart_wl_D_GC_heur_prog S);
       ASSERT(learned_clss_count T ≤ learned_clss_count S);
       RETURN (T, learned_clss_count T, learned_clss_count T, n+1)
    }
    else do {
         T ← cdcl_twl_full_restart_wl_D_inprocess_heur_prog S;
         ASSERT(learned_clss_count T ≤ learned_clss_count S);
         RETURN (T, learned_clss_count T, learned_clss_count T, n+1)
     }
    else RETURN (S, last_GC, last_Restart, n)
  })›
   unfolding restart_prog_wl_D_heur_def Let_def
   by (auto intro: bind_cong[OF refl])


lemma cdcl_twl_mark_clauses_to_delete_cdcl_twl_full_restart_wl_prog_D2:
  ‹(cdcl_twl_mark_clauses_to_delete, cdcl_twl_full_restart_wl_prog) ∈
     twl_st_heur''''u r u →⇩f ⟨twl_st_heur''''uu r u⟩nres_rel›
  apply (intro frefI nres_relI)
  apply (rule order_trans[OF cdcl_twl_mark_clauses_to_delete_cdcl_twl_full_restart_wl_prog_D[THEN fref_to_Down]])
  apply fast
  apply assumption
  apply (rule conc_fun_R_mono)
  by auto

lemma restart_prog_wl_alt_def2:
  ‹restart_prog_wl S last_GC last_Restart n brk = do{
     ASSERT(restart_abs_wl_pre S last_GC last_Restart brk);
     ASSERT (last_GC
            ≤ size (get_learned_clss_wl S) + size (get_unit_learned_clss_wl S) +
              size (get_subsumed_learned_clauses_wl S) +
              size (get_learned_clauses0_wl S));
    ASSERT  (last_Restart
            ≤ size (get_learned_clss_wl S) + size (get_unit_learned_clss_wl S) +
              size (get_subsumed_learned_clauses_wl S) +
              size (get_learned_clauses0_wl S));
    if brk then RETURN (S, last_GC, last_Restart, n)
    else do {
     b ← restart_required_wl S last_GC last_Restart n;
     if b = RESTART ∧ ¬brk then do {
       T ← cdcl_twl_restart_wl_prog S;
       RETURN (T, last_GC, size (get_all_learned_clss_wl T), n)
     }
     else if (b = GC ∨ b = INPROCESS) ∧ ¬brk then
        if b ≠ INPROCESS then do {
          b ← SPEC(λ_. True);
          T ← (if b then cdcl_twl_full_restart_wl_prog S else cdcl_twl_full_restart_wl_GC_prog S);
          RETURN (T, size (get_all_learned_clss_wl T), size (get_all_learned_clss_wl T), n + 1)
        } else do {
          T ← cdcl_twl_full_restart_inprocess_wl_prog S;
          RETURN (T, size (get_all_learned_clss_wl T), size (get_all_learned_clss_wl T), n + 1)
       }
     else
       RETURN (S, last_GC, last_Restart, n)
   }}› (is ‹?A = ?B›)
proof -
  have ‹?A ≤ ⇓ Id ?B›
    unfolding restart_prog_wl_def restart_required_wl_def
    by refine_vcg
      (auto simp: restart_required_wl_def RES_RETURN_RES intro!: bind_cong[OF refl])
  moreover have ‹?B ≤ ⇓ Id ?A›
    unfolding restart_prog_wl_def restart_required_wl_def nres_monad3
    by refine_vcg
      (auto simp: restart_required_wl_def RES_RETURN_RES intro!: bind_cong[OF refl])
  ultimately show ?thesis by simp
qed

lemma restart_abs_wl_pre_emptyN0S:
  assumes ‹restart_abs_wl_pre S lastGC lastRestart C› and [simp]: ‹¬C›
  shows ‹get_init_clauses0_wl S = {#} ∧ get_learned_clauses0_wl S = {#}›
proof -
  obtain x xa where
    Sx: ‹(S, x) ∈ state_wl_l None› and
    ‹correct_watching S› and
    ‹blits_in_ℒ⇩i⇩n S› and
    xxa: ‹(x, xa) ∈ twl_st_l None› and
    struct: ‹twl_struct_invs xa› and
    ‹twl_list_invs x› and
    ‹clauses_to_update_l x = {#}› and
    ‹twl_stgy_invs xa› and
    ‹¬ C ⟶ get_conflict xa = None› and
    ‹lastRestart ≤ size (get_all_learned_clss xa)› and
    ‹lastGC ≤ size (get_all_learned_clss xa)›
    using assms unfolding restart_abs_wl_pre_def restart_abs_l_pre_def restart_prog_pre_def apply -
    apply normalize_goal+
    by fast

  then have ‹get_conflict xa = None›
    by simp
  moreover have ‹clauses0_inv (pstate⇩W_of xa)›
    using struct unfolding twl_struct_invs_def pcdcl_all_struct_invs_def by fast
  ultimately have ‹get_init_clauses0 xa = {#} ∧ get_learned_clauses0 xa = {#}›
    unfolding clauses0_inv_def
    by (cases xa; auto simp: clauses0_inv_def)
  then show ?thesis
    using Sx xxa by auto
qed

abbreviation restart_prog_wl_heur_rel :: ‹_› where
  ‹restart_prog_wl_heur_rel r u≡ {((T, a, b, c), (U, d, e, f)). 
  (T,U) ∈ twl_st_heur_loop''''uu r u ∧
  (get_conflict_wl U = None ⟶((a,b,c), (d,e,f)) ∈ nat_rel ×⇩r nat_rel ×⇩r nat_rel)}›

abbreviation restart_prog_wl_heur_rel2 :: ‹_› where
  ‹restart_prog_wl_heur_rel2≡ {((T, a, b, c), (U, d, e, f)). 
  (T,U) ∈ twl_st_heur_loop ∧
  (get_conflict_wl U = None ⟶((a,b,c), (d,e,f)) ∈ nat_rel ×⇩r nat_rel ×⇩r nat_rel)}›

lemma restart_prog_wl_D_heur_restart_prog_wl_D:
  ‹(uncurry4 restart_prog_wl_D_heur, uncurry4 restart_prog_wl) ∈
  twl_st_heur''''u r u ×⇩f nat_rel ×⇩f nat_rel ×⇩f nat_rel ×⇩f bool_rel  →⇩f
  ⟨restart_prog_wl_heur_rel r u⟩nres_rel›
proof -
  have [refine0]: ‹RETURN b ≤ ⇓{(c, c'). c' ⟷ (c = FLAG_Reduce_restart)} (SPEC (λ_::bool. True))› for b
    by (auto simp: GC_required_heur_def RETURN_RES_refine_iff)
  have H: ‹(x1g, x1c)
        ∈ twl_st_heur''''u r (learned_clss_count x1g)›
    if
      ‹(x, y)
       ∈ twl_st_heur''''u r u ×⇩f nat_rel ×⇩f nat_rel ×⇩f nat_rel ×⇩f bool_rel› and
      ‹x1b = (x1c, x2)› and
      ‹x1a = (x1b, x2a)› and
      ‹x1 = (x1a, x2b)› and
      ‹y = (x1, x2c)› and
      ‹x1f = (x1g, x2d)› and
      ‹x1e = (x1f, x2e)› and
      ‹x1d = (x1e, x2f)› and
      ‹x = (x1d, x2g)› 
    for x y x1 x1a x1b x1c x2 x2a x2b x2c x1d x1e x1f x1g x2d x2e x2f x2g b ba bb
    using that by auto

  show ?thesis
    supply RETURN_as_SPEC_refine[refine2 del] learned_clss_count_twl_st_heur[simp]
    unfolding restart_prog_wl_D_heur_alt_def restart_prog_wl_alt_def2 uncurry_def
    apply (intro frefI nres_relI)
    subgoal for x y
    apply (refine_rcg
      restart_required_heur_restart_required_wl0[where r=r, THEN fref_to_Down_curry3]
        cdcl_twl_restart_wl_heur_cdcl_twl_restart_wl_D_prog[where r=r, THEN fref_to_Down]
        cdcl_twl_full_restart_wl_D_GC_heur_prog[where r=r, THEN fref_to_Down, THEN order_trans]
      cdcl_twl_mark_clauses_to_delete_cdcl_twl_full_restart_wl_prog_D2[where r=r and
      u = ‹learned_clss_count (fst (fst (fst (fst x))))›, THEN fref_to_Down]
      cdcl_twl_full_restart_wl_D_inprocess_heur_prog[where r=r and
      u = ‹learned_clss_count (fst (fst (fst (fst x))))›, THEN fref_to_Down])
    subgoal by auto
    subgoal by (auto intro!: twl_st_heur_twl_st_heur_loopD)
    subgoal by (auto dest: restart_abs_wl_pre_emptyN0S)
    subgoal by (auto dest: restart_abs_wl_pre_emptyN0S)
    subgoal by auto
    subgoal by (auto simp: restart_flag_rel_def FLAG_GC_restart_def FLAG_restart_def
      FLAG_no_restart_def FLAG_Reduce_restart_def FLAG_Inprocess_restart_def)
    apply (rule twl_st_heur'''_twl_st_heur''''uD)
    subgoal by auto
    subgoal by auto
    subgoal by (auto intro!: twl_st_heur_twl_st_heur_loopD)
    subgoal by (auto simp: restart_flag_rel_def FLAG_GC_restart_def FLAG_restart_def
      FLAG_no_restart_def FLAG_Reduce_restart_def FLAG_Inprocess_restart_def)
    subgoal by (auto simp: restart_flag_rel_def FLAG_GC_restart_def FLAG_restart_def
      FLAG_no_restart_def FLAG_Reduce_restart_def FLAG_Inprocess_restart_def)
    subgoal by (auto simp: restart_flag_rel_def FLAG_GC_restart_def FLAG_restart_def
      FLAG_no_restart_def FLAG_Reduce_restart_def FLAG_Inprocess_restart_def)
    subgoal by auto
    apply (rule H; assumption)
    subgoal for x1 x1a x1b x1c x2 x2a x2b x2c x1d x1e x1f x1g x2d x2e x2f x2g b ba bb
      by (rule conc_fun_R_mono) auto
    subgoal
      by auto
    subgoal
      by (auto dest: restart_abs_wl_pre_emptyN0S intro!: twl_st_heur_twl_st_heur_loopD)
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by (auto dest: restart_abs_wl_pre_emptyN0S dest!: twl_st_heur_loop_twl_st_heurD)
    subgoal
      by (auto intro!: twl_st_heur_twl_st_heur_loopD)
    done
  done
 qed

lemma restart_prog_wl_D_heur_restart_prog_wl_D2:
  ‹(uncurry4 restart_prog_wl_D_heur, uncurry4 restart_prog_wl) ∈
  twl_st_heur ×⇩f nat_rel ×⇩f nat_rel ×⇩f nat_rel ×⇩f bool_rel →⇩f ⟨restart_prog_wl_heur_rel2⟩nres_rel›
  apply (intro frefI nres_relI)
  apply (rule_tac r3 = ‹length(get_clauses_wl_heur (fst (fst (fst (fst x)))))› and
       u4 = ‹learned_clss_count (fst (fst (fst (fst x))))› in
    order_trans[OF restart_prog_wl_D_heur_restart_prog_wl_D[THEN fref_to_Down]])
  apply fast
  apply (auto intro!: conc_fun_R_mono)
  done

end