Theory IsaSAT_CDCL

theory IsaSAT_CDCL
  imports IsaSAT_Propagate_Conflict IsaSAT_Other IsaSAT_Show
    IsaSAT_CDCL_Defs
begin



paragraph ‹Combining Together: Full Strategy›

lemma cdcl_twl_stgy_prog_wl_D_heur_cdcl_twl_stgy_prog_wl_D:
  ‹(cdcl_twl_stgy_prog_wl_D_heur, cdcl_twl_stgy_prog_wl) ∈ twl_st_heur →⇩f ⟨twl_st_heur⟩nres_rel›
proof -
  have H[refine0]: ‹(x, y) ∈ {(S, T).
               (S, T) ∈ twl_st_heur ∧
               length (get_clauses_wl_heur S) =
               length (get_clauses_wl_heur x)} ⟹
           (x, y)
           ∈ {(S, T).
               (S, T) ∈ twl_st_heur ∧ get_learned_count S = get_learned_count x}› for x y
    by (auto simp: twl_st_heur_state_simp twl_st_heur_twl_st_heur_conflict_ana)
  show ?thesis
    unfolding cdcl_twl_stgy_prog_wl_D_heur_def cdcl_twl_stgy_prog_wl_def
    apply (intro frefI nres_relI)
    subgoal for x y
    apply (refine_vcg
        unit_propagation_outer_loop_wl_D_heur_unit_propagation_outer_loop_wl_D'[THEN twl_st_heur''D_twl_st_heurD, THEN fref_to_Down]
        cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D2[THEN fref_to_Down])
    subgoal by (auto simp: twl_st_heur_state_simp)
    subgoal by (auto simp: twl_st_heur_state_simp twl_st_heur'_def)
    subgoal by (auto simp: twl_st_heur'_def)
    subgoal by (auto simp: twl_st_heur_state_simp)
    subgoal by (auto simp: twl_st_heur_state_simp)
    done
    done
qed



lemma cdcl_twl_stgy_prog_early_wl_heur_cdcl_twl_stgy_prog_early_wl_D:
  assumes r: ‹r ≤ snat64_max›
  shows ‹(cdcl_twl_stgy_prog_bounded_wl_heur, cdcl_twl_stgy_prog_early_wl) ∈
    {(S,T). (S, T) ∈ twl_st_heur''' r} →⇩f
    ⟨bool_rel ×⇩r  twl_st_heur⟩nres_rel›
proof -
  have A[refine0]: ‹RETURN (isasat_fast x) ≤ ⇓
      {(b, b'). b = b' ∧ (b = (isasat_fast x))} (RES UNIV)›
    for x
    by (auto intro: RETURN_RES_refine)
  have twl_st_heur'': ‹(x1e, x1b) ∈ twl_st_heur ⟹
    (x1e, x1b)
    ∈ twl_st_heur''
        (dom_m (get_clauses_wl x1b))
        (length (get_clauses_wl_heur x1e))
        (get_learned_count x1e)›
    for x1e x1b
    by (auto simp: twl_st_heur'_def)
  have twl_st_heur''': ‹(x1e, x1b) ∈ twl_st_heur'' 𝒟 r lcount ⟹
    (x1e, x1b)
    ∈ {(S, Taa).
          (S, Taa) ∈ twl_st_heur ∧
          length (get_clauses_wl_heur S) = r ∧
          learned_clss_count S = (λ(a,b,c,d,e). a + b + c + d+e) (lcount)}›
    for x1e x1b r 𝒟 lcount
    by (auto simp: twl_st_heur'_def learned_clss_count_def clss_size_lcountUEk_def
      clss_size_lcountUE_def clss_size_lcountU0_def clss_size_lcount_def clss_size_lcountUS_def
      split: prod.splits)
  have H: ‹SPEC (λ_::bool. True) = RES UNIV› by auto
  show ?thesis
    supply[[goals_limit=1]] isasat_fast_length_leD[dest] twl_st_heur'_def[simp]
    unfolding cdcl_twl_stgy_prog_bounded_wl_heur_def
      cdcl_twl_stgy_prog_early_wl_def H
    apply (intro frefI nres_relI)
    apply (refine_rcg
        cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D[THEN fref_to_Down]
        unit_propagation_outer_loop_wl_D_heur_unit_propagation_outer_loop_wl_D'[THEN fref_to_Down]
        WHILEIT_refine[where R = ‹{((ebrk, brk, T), (ebrk', brk', T')).
	    (ebrk = ebrk') ∧ (brk = brk') ∧ (T, T')  ∈ twl_st_heur ∧
	      (ebrk ⟶ isasat_fast T) ∧ (length (get_clauses_wl_heur T) ≤ snat64_max)}›])
    subgoal using r by auto
    subgoal by fast
    subgoal by auto
    apply (rule twl_st_heur''; auto; fail)
    subgoal by (auto simp: isasat_fast_def dest: get_learned_count_learned_clss_countD)
    apply (rule twl_st_heur'''; assumption)
    subgoal
      apply clarsimp
      by (auto simp: isasat_fast_def snat64_max_def unat32_max_def
      dest: )
    subgoal by auto
    done
qed

end