Theory IsaSAT_Decide_Defs

theory IsaSAT_Decide_Defs
  imports IsaSAT_Setup IsaSAT_VMTF IsaSAT_Bump_Heuristics IsaSAT_Phasing
begin


chapter ‹Decide›

definition isa_bump_find_next_undef where ‹
  isa_bump_find_next_undef x M = (case x of Bump_Heuristics hstable focused foc tobmp ⇒
  if foc then do {
    L ← isa_vmtf_find_next_undef focused M;
    RETURN (L, Bump_Heuristics hstable (update_next_search L focused) foc tobmp)
    } else  do {
    (L, hstable) ← isa_acids_find_next_undef hstable M;
    RETURN (L, Bump_Heuristics hstable focused foc tobmp)
  })›

definition isa_vmtf_find_next_undef_upd
  :: ‹trail_pol ⇒ bump_heuristics ⇒
        ((trail_pol × bump_heuristics) × nat option)nres›
where
  ‹isa_vmtf_find_next_undef_upd = (λM vm. do{
      (L, vm) ← isa_bump_find_next_undef vm M;
      RETURN ((M, vm), L)
  })›

definition get_saved_phase_option_heur_pre :: ‹nat option ⇒ restart_heuristics ⇒ bool› where
  ‹get_saved_phase_option_heur_pre L = (λheur.
       L ≠ None ⟶ get_next_phase_heur_pre_stats True (the L) heur)›

definition lit_of_found_atm where
‹lit_of_found_atm φ L = SPEC (λK. (L = None ⟶ K = None) ∧
    (L ≠ None ⟶ K ≠ None ∧ atm_of (the K) = the L))›

definition find_unassigned_lit_wl_D_heur
  :: ‹isasat ⇒ (isasat × nat literal option) nres›
where
  ‹find_unassigned_lit_wl_D_heur = (λS. do {
      let M = get_trail_wl_heur S;
      let vm = get_vmtf_heur S;
      let heur = get_heur S;
      let heur = set_fully_propagated_heur heur;
      ((M, vm), L) ← isa_vmtf_find_next_undef_upd M vm;
      ASSERT(get_saved_phase_option_heur_pre (L) (get_content heur));
        L ← lit_of_found_atm heur L;
      let S = set_trail_wl_heur M S;
      let S = set_vmtf_wl_heur vm S;
      let S = set_heur_wl_heur heur S;
      RETURN (S, L)
    })›

definition decide_lit_wl_heur :: ‹nat literal ⇒ isasat ⇒ isasat nres› where
  ‹decide_lit_wl_heur = (λL' S. do {
      let M = get_trail_wl_heur S;
      let stats = get_stats_heur S;
      ASSERT(isa_length_trail_pre M);
      let j = isa_length_trail M;
      let S = set_literals_to_update_wl_heur j S;
      ASSERT(cons_trail_Decided_tr_pre (L', M));
      let M = cons_trail_Decided_tr L' M;
      let S = set_trail_wl_heur M S;
      let stats = incr_decision stats;
      let S = set_stats_wl_heur stats S;
      RETURN S})›

definition mop_get_saved_phase_heur_st :: ‹nat ⇒ isasat ⇒ bool nres› where
   ‹mop_get_saved_phase_heur_st = (λL S. mop_get_saved_phase_heur L (get_heur S))›

definition decide_wl_or_skip_D_heur
  :: ‹isasat ⇒ (bool × isasat) nres›
where
  ‹decide_wl_or_skip_D_heur S = (do {
    (S, L) ← find_unassigned_lit_wl_D_heur S;
    case L of
      None ⇒ RETURN (True, S)
    | Some L ⇒ do {
        T ← decide_lit_wl_heur L S;
        RETURN (False, T)}
  })
›

definition get_next_phase_st :: ‹bool ⇒ nat ⇒ isasat ⇒ (bool) nres› where
  ‹get_next_phase_st = (λb L S.
     (get_next_phase_heur b L (get_heur S)))›

definition find_unassigned_lit_wl_D_heur2
  :: ‹isasat ⇒ (isasat × nat option) nres›
where
  ‹find_unassigned_lit_wl_D_heur2 = (λS. do {
      ((M, vm), L) ← isa_vmtf_find_next_undef_upd (get_trail_wl_heur S) (get_vmtf_heur S);
      RETURN (set_heur_wl_heur (set_fully_propagated_heur (get_heur S)) (set_trail_wl_heur M (set_vmtf_wl_heur vm S)), L)
    })›

definition decide_wl_or_skip_D_heur' where
  ‹decide_wl_or_skip_D_heur' = (λS. do {
      (S, L) ← find_unassigned_lit_wl_D_heur2 S;
      ASSERT(get_saved_phase_option_heur_pre L (get_restart_heuristics (get_heur S)));
      case L of
       None ⇒ RETURN (True, S)
     | Some L ⇒ do {
        L ← do {
            b ← get_next_phase_st (get_target_opts S = TARGET_ALWAYS ∨
                   (get_target_opts S = TARGET_STABLE_ONLY ∧ get_restart_phase S = STABLE_MODE)) L S;
              RETURN (if b then Pos L else Neg L)};
        T ← decide_lit_wl_heur L S;
        RETURN (False, T)
      }
    })
›


lemma decide_wl_or_skip_D_heur'_decide_wl_or_skip_D_heur:
  ‹decide_wl_or_skip_D_heur' S ≤ ⇓Id (decide_wl_or_skip_D_heur S)›
proof -
  have [iff]:
    ‹{K. (∃y. K = Some y) ∧ atm_of (the K) = x2d} = {Some (Pos x2d), Some (Neg x2d)}› for x2d
    apply (auto simp: atm_of_eq_atm_of)
    apply (case_tac y)
    apply auto
    done
  have H: ‹do {
    L ←do {ASSERT φ; P};
    Q L} =
    do {ASSERT φ; L ← P; Q L} › for P Q φ
    by auto
  have H: ‹A ≤ ⇓Id B ⟹ B ≤ ⇓Id A ⟹A = B› for A B
    by auto
  have K: ‹RES {Some (Pos x2), Some (Neg x2)} ≤ ⇓ {(x, y). x = Some y} (RES {Pos x2, Neg x2})›
    ‹RES {(Pos x2), (Neg x2)} ≤ ⇓ {(y, x). x = Some y} (RES {Some (Pos x2), Some (Neg x2)})›  for x2
    by (auto intro!: RES_refine)
  have [simp]: ‹IsaSAT_Decide_Defs.get_saved_phase_option_heur_pre a (get_restart_heuristics (set_fully_propagated_heur (S))) =
    IsaSAT_Decide_Defs.get_saved_phase_option_heur_pre a (get_restart_heuristics (S))› for S a
    by (cases S)(auto simp: IsaSAT_Decide_Defs.get_saved_phase_option_heur_pre_def get_next_phase_heur_pre_stats_def
      get_next_phase_pre_def set_fully_propagated_heur_def set_fully_propagated_heur_stats_def)
  have S: ‹decide_wl_or_skip_D_heur S =
       (do {
                   ((M, vm), L) ← isa_vmtf_find_next_undef_upd (get_trail_wl_heur S) (get_vmtf_heur S);
                   ASSERT (IsaSAT_Decide_Defs.get_saved_phase_option_heur_pre L (get_restart_heuristics (get_heur S)));
                   case L of None ⇒ RETURN (True, set_heur_wl_heur (set_fully_propagated_heur (get_heur S)) (set_vmtf_wl_heur vm (set_trail_wl_heur M S)))
                     | Some L ⇒ do {
                       _ ← SPEC (λ_::bool. True);
                       L ←RES {Pos L, Neg L};
                      T ← decide_lit_wl_heur L (set_heur_wl_heur (set_fully_propagated_heur (get_heur S)) (set_vmtf_wl_heur vm (set_trail_wl_heur M S)));
                      RETURN (False, T)
                     }})› for S a b c d e f g h i  j k l m n p q r
     unfolding decide_wl_or_skip_D_heur_def find_unassigned_lit_wl_D_heur_def Let_def
     apply (auto intro!: bind_cong[OF refl] simp: lit_of_found_atm_def split: option.splits)
     apply (rule H)
     subgoal
       apply (refine_rcg K)
       apply auto
       done
     subgoal
       apply (refine_rcg K)
       apply auto
       done
     done
  have [refine]: ‹get_saved_phase_option_heur_pre x2c (get_restart_heuristics XX) ⟹
     x2c = Some x'a ⟹ XX=YY ⟹
    get_next_phase_heur b x'a YY ≤ (SPEC (λ_::bool. True))› for x'a x1d x1e x1f x1g x2g b XX x2c YY
    by (auto simp: get_next_phase_heur_def get_saved_phase_option_heur_pre_def get_next_phase_pre_def
      get_next_phase_heur_stats_def get_next_phase_stats_def get_next_phase_heur_pre_stats_def
      split: prod.splits)
  have [refine]: ‹xa =  x'a ⟹ RETURN (if xb then Pos xa else Neg xa)
       ≤ ⇓ Id (RES {Pos x'a, Neg x'a})› for xb x'a xa
    by auto
  have [refine]: ‹decide_lit_wl_heur L S
    ≤ ⇓ Id
        (decide_lit_wl_heur La Sa)› if ‹(L, La) ∈ Id› ‹(S, Sa) ∈ Id› for L La S Sa
    using that by auto
  have [intro!]: ‹get_saved_phase_option_heur_pre (snd pa) (get_restart_heuristics l) ⟹
    get_saved_phase_option_heur_pre (snd pa) (get_restart_heuristics (set_fully_propagated_heur l))› for pa l
    by (cases l; cases pa) (auto simp: get_saved_phase_option_heur_pre_def get_next_phase_heur_pre_stats_def
      get_next_phase_pre_def set_fully_propagated_heur_stats_def
      set_fully_propagated_heur_def)
  show ?thesis
    apply (cases S, simp only: S)
    unfolding find_unassigned_lit_wl_D_heur_def
      nres_monad3 prod.case find_unassigned_lit_wl_D_heur_def
      prod.case decide_wl_or_skip_D_heur'_def get_next_phase_st_def
      find_unassigned_lit_wl_D_heur2_def
      case_prod_beta snd_conv fst_conv bind_to_let_conv
    apply (subst Let_def)
    apply (refine_vcg
      same_in_Id_option_rel)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    apply assumption back
    subgoal by auto
    subgoal by (auto simp: set_fully_propagated_heur_def split: prod.splits)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    done
qed

end