Theory IsaSAT_CDCL

theory IsaSAT_CDCL
  imports IsaSAT_Propagate_Conflict IsaSAT_Conflict_Analysis IsaSAT_Backtrack
    IsaSAT_Decide IsaSAT_Show
begin

chapter ‹Combining Together: the Other Rules›

definition cdcl_twl_o_prog_wl_D_heur
 :: ‹twl_st_wl_heur ⇒ (bool × twl_st_wl_heur) nres›
where
  ‹cdcl_twl_o_prog_wl_D_heur S =
    do {
      if get_conflict_wl_is_None_heur S
      then decide_wl_or_skip_D_heur S
      else do {
        if count_decided_st_heur S > 0
        then do {
          T ← skip_and_resolve_loop_wl_D_heur S;
          ASSERT(length (get_clauses_wl_heur S) = length (get_clauses_wl_heur T));
          U ← backtrack_wl_D_nlit_heur T;
          U ← isasat_current_status U; ― ‹Print some information every once in a while›
          RETURN (False, U)
        }
        else RETURN (True, S)
      }
    }
  ›

lemma twl_st_heur''D_twl_st_heurD:
  assumes H: ‹(⋀𝒟 r. f ∈ twl_st_heur'' 𝒟 r →⇩f ⟨twl_st_heur'' 𝒟 r⟩ nres_rel)›
  shows ‹f ∈ twl_st_heur →⇩f ⟨twl_st_heur⟩ nres_rel›  (is ‹_ ∈ ?A B›)
proof -
  obtain f1 f2 where f: ‹f = (f1, f2)›
    by (cases f) auto
  show ?thesis
    unfolding f
    apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
    apply (intro conjI impI allI)
    subgoal for x y
      using assms[of ‹dom_m (get_clauses_wl y)›  ‹length (get_clauses_wl_heur x)›,
        unfolded twl_st_heur'_def nres_rel_def in_pair_collect_simp f,
        rule_format] unfolding f
      apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
      apply (drule spec[of _ x])
      apply (drule spec[of _ y])
      apply simp
      apply (rule "weaken_⇓'"[of _ ‹twl_st_heur'' (dom_m (get_clauses_wl y))
         (length (get_clauses_wl_heur x))›])
      apply (fastforce simp: twl_st_heur'_def)+
      done
    done
qed


lemma twl_st_heur'''D_twl_st_heurD:
  assumes H: ‹(⋀r. f ∈ twl_st_heur''' r →⇩f ⟨twl_st_heur''' r⟩ nres_rel)›
  shows ‹f ∈ twl_st_heur →⇩f ⟨twl_st_heur⟩ nres_rel›  (is ‹_ ∈ ?A B›)
proof -
  obtain f1 f2 where f: ‹f = (f1, f2)›
    by (cases f) auto
  show ?thesis
    unfolding f
    apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
    apply (intro conjI impI allI)
    subgoal for x y
      using assms[of ‹length (get_clauses_wl_heur x)›,
        unfolded twl_st_heur'_def nres_rel_def in_pair_collect_simp f,
        rule_format] unfolding f
      apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
      apply (drule spec[of _ x])
      apply (drule spec[of _ y])
      apply simp
      apply (rule "weaken_⇓'"[of _ ‹twl_st_heur''' (length (get_clauses_wl_heur x))›])
      apply (fastforce simp: twl_st_heur'_def)+
      done
    done
qed


lemma twl_st_heur'''D_twl_st_heurD_prod:
  assumes H: ‹(⋀r. f ∈ twl_st_heur''' r →⇩f ⟨A ×⇩r twl_st_heur''' r⟩ nres_rel)›
  shows ‹f ∈ twl_st_heur →⇩f ⟨A ×⇩r twl_st_heur⟩ nres_rel›  (is ‹_ ∈ ?A B›)
proof -
  obtain f1 f2 where f: ‹f = (f1, f2)›
    by (cases f) auto
  show ?thesis
    unfolding f
    apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
    apply (intro conjI impI allI)
    subgoal for x y
      using assms[of ‹length (get_clauses_wl_heur x)›,
        unfolded twl_st_heur'_def nres_rel_def in_pair_collect_simp f,
        rule_format] unfolding f
      apply (simp only: fref_def twl_st_heur'_def nres_rel_def in_pair_collect_simp)
      apply (drule spec[of _ x])
      apply (drule spec[of _ y])
      apply simp
      apply (rule "weaken_⇓'"[of _ ‹A ×⇩r twl_st_heur''' (length (get_clauses_wl_heur x))›])
      apply (fastforce simp: twl_st_heur'_def)+
      done
    done
qed

lemma cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D:
  ‹(cdcl_twl_o_prog_wl_D_heur, cdcl_twl_o_prog_wl) ∈
   {(S, T). (S, T) ∈ twl_st_heur ∧ length (get_clauses_wl_heur S) = r} →⇩f
     ⟨bool_rel ×⇩f {(S, T). (S, T) ∈ twl_st_heur ∧
        length (get_clauses_wl_heur S) ≤ r + 6 + uint32_max div 2}⟩nres_rel›
proof -
  have H: ‹(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_conflict_ana ∧
               length (get_clauses_wl_heur S) =
               length (get_clauses_wl_heur 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_o_prog_wl_D_heur_def cdcl_twl_o_prog_wl_def
      get_conflict_wl_is_None
    apply (intro frefI nres_relI)
    apply (refine_vcg
        decide_wl_or_skip_D_heur_decide_wl_or_skip_D[where r=r, THEN fref_to_Down, THEN order_trans]
        skip_and_resolve_loop_wl_D_heur_skip_and_resolve_loop_wl_D[where r=r, THEN fref_to_Down]
        backtrack_wl_D_nlit_backtrack_wl_D[where r=r, THEN fref_to_Down]
        isasat_current_status_id[THEN fref_to_Down, THEN order_trans])
    subgoal
      by (auto simp: twl_st_heur_state_simp
          get_conflict_wl_is_None_heur_get_conflict_wl_is_None[THEN fref_to_Down_unRET_Id])
    apply (assumption)
    subgoal by (rule conc_fun_R_mono) auto
    subgoal by (auto simp: twl_st_heur_state_simp twl_st_heur_count_decided_st_alt_def)
    subgoal by (auto simp: twl_st_heur_state_simp twl_st_heur_twl_st_heur_conflict_ana)
    subgoal by (auto simp: twl_st_heur_state_simp)
    apply assumption
    subgoal by (auto simp: conc_fun_RES RETURN_def)
    subgoal by (auto simp: twl_st_heur_state_simp)
    done
qed

lemma cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D2:
  ‹(cdcl_twl_o_prog_wl_D_heur, cdcl_twl_o_prog_wl) ∈
   {(S, T). (S, T) ∈ twl_st_heur} →⇩f
     ⟨bool_rel ×⇩f {(S, T). (S, T) ∈ twl_st_heur}⟩nres_rel›
  apply (intro frefI nres_relI)
  apply (rule cdcl_twl_o_prog_wl_D_heur_cdcl_twl_o_prog_wl_D[THEN fref_to_Down, THEN order_trans])
  apply (auto intro!: conc_fun_R_mono)
  done


paragraph ‹Combining Together: Full Strategy›

definition  cdcl_twl_stgy_prog_wl_D_heur
   :: ‹twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
  ‹cdcl_twl_stgy_prog_wl_D_heur S⇩0 =
  do {
    do {
        (brk, T) ← WHILE⇩T
        (λ(brk, _). ¬brk)
        (λ(brk, S).
        do {
          T ← unit_propagation_outer_loop_wl_D_heur S;
          cdcl_twl_o_prog_wl_D_heur T
        })
        (False, S⇩0);
      RETURN T
    }
  }
  ›

theorem unit_propagation_outer_loop_wl_D_heur_unit_propagation_outer_loop_wl_D:
  ‹(unit_propagation_outer_loop_wl_D_heur, unit_propagation_outer_loop_wl) ∈
    twl_st_heur →⇩f ⟨twl_st_heur⟩ nres_rel›
  using twl_st_heur''D_twl_st_heurD[OF
     unit_propagation_outer_loop_wl_D_heur_unit_propagation_outer_loop_wl_D']
  .

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: ‹(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_conflict_ana ∧
               length (get_clauses_wl_heur S) =
               length (get_clauses_wl_heur 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


definition cdcl_twl_stgy_prog_break_wl_D_heur :: ‹twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
  ‹cdcl_twl_stgy_prog_break_wl_D_heur S⇩0 =
  do {
    b ← RETURN (isasat_fast S⇩0);
    (b, brk, T) ← WHILE⇩T⇗λ(b, brk, T). True⇖
        (λ(b, brk, _). b ∧ ¬brk)
        (λ(b, brk, S).
        do {
          ASSERT(isasat_fast S);
          T ← unit_propagation_outer_loop_wl_D_heur S;
          ASSERT(isasat_fast T);
          (brk, T) ← cdcl_twl_o_prog_wl_D_heur T;
          b ← RETURN (isasat_fast T);
          RETURN(b, brk, T)
        })
        (b, False, S⇩0);
    if brk then RETURN T
    else cdcl_twl_stgy_prog_wl_D_heur T
  }›


definition cdcl_twl_stgy_prog_bounded_wl_heur :: ‹twl_st_wl_heur ⇒ (bool × twl_st_wl_heur) nres›
where
  ‹cdcl_twl_stgy_prog_bounded_wl_heur S⇩0 =
  do {
    b ← RETURN (isasat_fast S⇩0);
    (b, brk, T) ← WHILE⇩T⇗λ(b, brk, T). True⇖
        (λ(b, brk, _). b ∧ ¬brk)
        (λ(b, brk, S).
        do {
          ASSERT(isasat_fast S);
          T ← unit_propagation_outer_loop_wl_D_heur S;
          ASSERT(isasat_fast T);
          (brk, T) ← cdcl_twl_o_prog_wl_D_heur T;
          b ← RETURN (isasat_fast T);
          RETURN(b, brk, T)
        })
        (b, False, S⇩0);
    RETURN (brk, T)
  }›


lemma cdcl_twl_stgy_restart_prog_early_wl_heur_cdcl_twl_stgy_restart_prog_early_wl_D:
  assumes r: ‹r ≤ sint64_max›
  shows ‹(cdcl_twl_stgy_prog_bounded_wl_heur, cdcl_twl_stgy_prog_early_wl) ∈
   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))›
    for x1e x1b
    by (auto simp: twl_st_heur'_def)
  have twl_st_heur''': ‹(x1e, x1b) ∈ twl_st_heur'' 𝒟 r ⟹
    (x1e, x1b)
    ∈ twl_st_heur''' r›
    for x1e x1b r 𝒟
    by (auto simp: twl_st_heur'_def)
  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) ≤ sint64_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)
    apply (rule twl_st_heur'''; assumption)
    subgoal by (auto simp: isasat_fast_def sint64_max_def uint32_max_def)
    subgoal by auto
    done
qed

end