Theory IsaSAT_Restart_Heuristics_Defs

theory IsaSAT_Restart_Heuristics_Defs
imports
  IsaSAT_Restart_Reduce_Defs IsaSAT_Restart_Inprocessing_Defs
begin

text ‹

  For simplification in our proofs, our inprocessing contains both inprocessing (currently:
  deduplication of binary clauses) and removal of unit clauses. We leave the concrete schedule
  to the inprocessing function.
›
definition should_inprocess_or_unit_reduce_st :: ‹isasat ⇒ bool ⇒ bool› where
  ‹should_inprocess_or_unit_reduce_st S should_GC ⟷
      (should_GC ∧ units_since_last_GC_st S > 0) ∨
      should_inprocess_st S ∨
      GC_units_required S›

definition restart_required_heur :: ‹isasat ⇒ nat ⇒ nat ⇒ nat ⇒ 8 word nres› where
  ‹restart_required_heur S last_GC last_Restart n = do {
    ASSERT(learned_clss_count S ≥ last_Restart);
    ASSERT(learned_clss_count S ≥ last_GC);
    let opt_red = opts_reduction_st S;
    let opt_res = opts_restart_st S;
    let curr_phase = get_restart_phase S;
    let can_res = (learned_clss_count S > last_Restart);
    let can_GC = (learned_clss_count S - last_GC> n);
    let fully_proped = is_fully_propagated_heur_st S;
    let should_reduce = (opt_red ∧ upper_restart_bound_reached S ∧ can_GC);
    should_GC ← GC_required_heur S n;
    let should_inprocess = should_inprocess_or_unit_reduce_st S should_GC;

    if (¬can_res ∧ ¬can_GC) ∨ ¬opt_res ∨ ¬opt_red ∨ ¬fully_proped then RETURN FLAG_no_restart
    else if curr_phase = STABLE_MODE
    then do {
      if should_reduce
      then if should_inprocess
      then RETURN FLAG_Inprocess_restart
      else if should_GC then RETURN FLAG_GC_restart else RETURN FLAG_Reduce_restart
      else if heuristic_reluctant_triggered2_st S ∧ can_res
        then RETURN FLAG_restart
        else RETURN FLAG_no_restart
    }
    else do {
      let sema = ema_get_value (get_slow_ema_heur S);
      let limit = (opts_restart_coeff1_st S) * (shiftr (sema) 4);
      let fema = ema_get_value (get_fast_ema_heur S);
      let ccount = get_conflict_count_since_last_restart_heur S;
      let min_reached = (ccount > opts_minimum_between_restart_st S);
      let level = count_decided_st_heur S;
      let should_restart = ((opt_res) ∧
         limit > fema ∧ min_reached ∧ can_res ∧
        level ≥ 1  ⌦‹This comment from Marijn Heule seems not to help:
        \<^term>‹∧ level < max_restart_decision_lvl››
          ⌦‹this was taken from Lingeling IIRC
           \<^term>‹∧ of_nat level > (shiftr fema 32)››);
      if should_reduce
        then if should_inprocess
        then RETURN FLAG_Inprocess_restart
        else if should_GC
        then RETURN FLAG_GC_restart
        else RETURN FLAG_Reduce_restart
      else if should_restart
      then RETURN FLAG_restart
      else RETURN FLAG_no_restart
     }
   }›


(*TODO Move clean: cdcl_twl_local_restart_wl_spec0 vs cdcl_twl_local_restart_wl_spec is mess*)


definition cdcl_twl_full_restart_wl_D_GC_heur_prog where
‹cdcl_twl_full_restart_wl_D_GC_heur_prog S0 = do {
    _ ← RETURN (IsaSAT_Profile.start_GC);
    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 (IsaSAT_Profile.stop_GC);
    RETURN (clss_size_resetUS0_st V)
  }›


definition cdcl_twl_full_restart_wl_D_inprocess_heur_prog where
‹cdcl_twl_full_restart_wl_D_inprocess_heur_prog S0 = do {
    _ ← RETURN (IsaSAT_Profile.start_reduce);
    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;
    _ ← RETURN (IsaSAT_Profile.stop_reduce);
    ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S0));
        ASSERT(learned_clss_count T ≤ learned_clss_count S0);
    _ ← RETURN (IsaSAT_Profile.start_binary_simp);
    T ← isa_mark_duplicated_binary_clauses_as_garbage_wl2 T;
    _ ← RETURN (IsaSAT_Profile.stop_binary_simp);
    ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S0));
        ASSERT(learned_clss_count T ≤ learned_clss_count S0);
    _ ← RETURN (IsaSAT_Profile.start_subsumption);
    T ← isa_forward_subsume T;
    _ ← RETURN (IsaSAT_Profile.stop_subsumption);
    ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S0));
        ASSERT(learned_clss_count T ≤ learned_clss_count S0);
    _ ← RETURN (IsaSAT_Profile.start_pure_literal);
    T ← isa_pure_literal_eliminate T;
    _ ← RETURN (IsaSAT_Profile.stop_pure_literal);
    ASSERT(length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S0));
    ASSERT(learned_clss_count T ≤ learned_clss_count S0);
    _ ← RETURN (IsaSAT_Profile.start_reduce);
    T ← isa_simplify_clauses_with_units_st_wl2 T;
    _ ← RETURN (IsaSAT_Profile.stop_reduce);
    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 {
      _ ← RETURN (IsaSAT_Profile.start_GC);
      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 (IsaSAT_Profile.stop_GC);
      RETURN (clss_size_resetUS0_st V)
    }
  }›


definition restart_prog_wl_D_heur
  :: ‹isasat ⇒ nat ⇒ nat ⇒ nat ⇒ bool ⇒ (isasat × nat × nat × nat) nres›
where
  ‹restart_prog_wl_D_heur S last_GC last_Restart n brk = do {
   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 {
         if b = FLAG_Reduce_restart
         then do {
           T ← cdcl_twl_mark_clauses_to_delete 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_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)
    }
  }›

end