Theory IsaSAT_Restart_Simp_Defs

theory IsaSAT_Restart_Simp_Defs
  imports IsaSAT_Restart_Heuristics_Defs IsaSAT_Other_Defs IsaSAT_Propagate_Conflict_Defs IsaSAT_Restart_Inprocessing_Defs
    Watched_Literals.Watched_Literals_Watch_List_Reduce
begin

chapter ‹Full CDCL with Restarts›


definition cdcl_twl_stgy_restart_abs_wl_heur_inv where
  ‹cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0 = (λ(brk, T, last_GC, last_Rephase).
    (∃S⇩0' T'. (S⇩0, S⇩0') ∈ twl_st_heur ∧ (T, T') ∈ twl_st_heur_loop ∧
      (¬brk ⟶ cdcl_twl_stgy_restart_abs_wl_inv S⇩0' (brk, T', last_GC, last_Rephase))))›

definition cdcl_twl_stgy_restart_abs_wl_heur_inv2 where
  ‹cdcl_twl_stgy_restart_abs_wl_heur_inv2 S⇩0 = (λ(brk, T, last_GC, last_Rephase).
    (∃S⇩0' T'. (S⇩0, S⇩0') ∈ twl_st_heur_loop ∧ (T, T') ∈ twl_st_heur_loop ∧
      (¬brk⟶cdcl_twl_stgy_restart_abs_wl_inv S⇩0' (brk, T', last_GC, last_Rephase))))›

text ‹It would be better to add a backtrack to level 0 before instead of delaying the restart.›
definition update_all_phases :: ‹isasat ⇒ (isasat) nres› where
  ‹update_all_phases = (λS. do {
     if (count_decided_st_heur S = 0) then do {
       let lcount = get_global_conflict_count S;
       end_of_restart_phase ← RETURN (end_of_restart_phase_st S);
       S ← (if end_of_restart_phase < lcount then update_restart_phases S else RETURN S);
       S ← (if end_of_rephasing_phase_st S < lcount then rephase_heur_st S else RETURN S);
       RETURN S
    }
    else RETURN S
  })›

definition isasat_fast_slow :: ‹isasat ⇒ isasat nres› where
   [simp]: ‹isasat_fast_slow S = RETURN S›

definition cdcl_twl_stgy_restart_prog_early_wl_heur
   :: ‹isasat ⇒ isasat nres›
where
  ‹cdcl_twl_stgy_restart_prog_early_wl_heur S⇩0 = do {
    ebrk ← RETURN (¬isasat_fast S⇩0);
    (ebrk, brk, T, n) ←
       WHILE⇩T⇗λ(ebrk, brk, T, last_GC, last_Restart, n).
       cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0 (brk, T, last_GC, last_Restart, n) ∧
        (¬ebrk ⟶isasat_fast T) ∧ length (get_clauses_wl_heur T) ≤ unat64_max⇖
      (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
      (λ(ebrk, brk, S, last_GC, last_Restart, n).
      do {
        ASSERT(¬brk ∧ ¬ebrk);
        ASSERT(length (get_clauses_wl_heur S) ≤ unat64_max);
        T ← unit_propagation_outer_loop_wl_D_heur S;
        ASSERT(length (get_clauses_wl_heur T) ≤ unat64_max);
        ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S));
        (brk, T) ← cdcl_twl_o_prog_wl_D_heur T;
        ASSERT(length (get_clauses_wl_heur T) ≤ unat64_max);
        (T, n) ← restart_prog_wl_D_heur T last_GC last_Restart n brk;
	ebrk ← RETURN (¬isasat_fast T);
        RETURN (ebrk, brk ∨ ¬get_conflict_wl_is_None_heur T, T, n)
      })
      (ebrk, False, S⇩0::isasat, learned_clss_count S⇩0, learned_clss_count S⇩0,  0);
    ASSERT(length (get_clauses_wl_heur T) ≤ unat64_max ∧
        get_old_arena T = []);
    if ¬brk then do {
       T ← isasat_fast_slow T;
       (brk, T, _) ← WHILE⇩T⇗cdcl_twl_stgy_restart_abs_wl_heur_inv2 T⇖
	         (λ(brk, _). ¬brk)
	         (λ(brk, S, last_GC, last_Restart, n).
	         do {
	           T ← unit_propagation_outer_loop_wl_D_heur S;
	           (brk, T) ← cdcl_twl_o_prog_wl_D_heur T;
	           (T, last_GC, last_Restart, n) ← restart_prog_wl_D_heur T last_GC last_Restart n brk;
	           RETURN (brk ∨ ¬get_conflict_wl_is_None_heur T, T, last_GC, last_Restart, n)
	         })
	         (False, T, n);
       RETURN T
    }
    else isasat_fast_slow T
  }›

definition cdcl_twl_stgy_restart_prog_bounded_wl_heur
   :: ‹isasat ⇒ (bool × isasat) nres›
where
  ‹cdcl_twl_stgy_restart_prog_bounded_wl_heur S⇩0 = do {
    ebrk ← RETURN (¬isasat_fast S⇩0);
    (ebrk, brk, T, n) ←
     WHILE⇩T⇗λ(ebrk, brk, T, last_GC, last_Restart, n). cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0 (brk, T, last_GC, last_Restart, n) ∧
        (¬ebrk ⟶isasat_fast T ∧ n < unat64_max) ∧
        (¬ebrk ⟶length (get_clauses_wl_heur T) ≤ snat64_max)⇖
      (λ(ebrk, brk, _). ¬brk ∧ ¬ebrk)
      (λ(ebrk, brk, S, last_GC, last_Restart, n).
      do {
        ASSERT(¬brk ∧ ¬ebrk);
        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;
        ASSERT(isasat_fast_relaxed2 T n);
        (T, last_GC, last_Restart, n) ← restart_prog_wl_D_heur T last_GC last_Restart n brk;
        T ← update_all_phases T;
        ASSERT(isasat_fast_relaxed T);
	      ebrk ← RETURN (¬(isasat_fast T ∧ n < unat64_max));
        RETURN (ebrk, brk ∨ ¬get_conflict_wl_is_None_heur T, T, last_GC, last_Restart, n)
      })
      (ebrk, False, S⇩0::isasat, learned_clss_count S⇩0, learned_clss_count S⇩0, 0);
    RETURN (ebrk, T)
  }›


definition cdcl_twl_stgy_restart_prog_wl_heur
   :: ‹isasat ⇒ isasat nres›
where
  ‹cdcl_twl_stgy_restart_prog_wl_heur S⇩0 = do {
    (brk, T, _) ← WHILE⇩T⇗cdcl_twl_stgy_restart_abs_wl_heur_inv S⇩0⇖
      (λ(brk, _). ¬brk)
      (λ(brk, S, last_GC, last_Rephase, n).
      do {
        T ← unit_propagation_outer_loop_wl_D_heur S;
        (brk, T) ← cdcl_twl_o_prog_wl_D_heur T;
        (T, last_GC, last_Rephase, n) ← restart_prog_wl_D_heur T last_GC last_Rephase n brk;
        RETURN (brk ∨ ¬get_conflict_wl_is_None_heur T, T, last_GC, last_Rephase, n)
      })
      (False, S⇩0::isasat, learned_clss_count S⇩0, learned_clss_count S⇩0, 0);
    RETURN T
  }›

end