Theory IsaSAT_Defs

theory IsaSAT_Defs
  imports IsaSAT_CDCL_Defs IsaSAT_Restart_Simp_Defs IsaSAT_Initialisation
begin

chapter ‹Full IsaSAT›

text ‹
  We now combine all the previous definitions to prove correctness of the complete SAT
  solver:
  ▸ We initialise the arena part of the state;
  ▸ Then depending on the options and the number of clauses, we either use the
    bounded version or the unbounded version. Once have if decided which one,
    we initiale the watch lists;
  ▸ After that, we can run the CDCL part of the SAT solver;
  ▸ Finally, we extract the trail from the state.

  Remark that the statistics and the options are unchecked: the number of propagations
  might overflows (but they do not impact the correctness of the whole solver). Similar
  restriction applies on the options: setting the options might not do what you expect to
  happen, but the result will still be correct.
›


definition extract_model_of_state_heur where
  ‹extract_model_of_state_heur U = Some (fst (get_trail_wl_heur U))›


definition convert_state where
  ‹convert_state _ S = S›

definition learned_clss_count_init :: ‹twl_st_wl_heur_init ⇒ nat› where
  ‹learned_clss_count_init S = clss_size_lcount (get_learned_count_init S) +
    clss_size_lcountUE (get_learned_count_init S) + 
    clss_size_lcountUEk (get_learned_count_init S) + clss_size_lcountUS (get_learned_count_init S) +
    clss_size_lcountU0 (get_learned_count_init S)›

definition isasat_fast_init :: ‹twl_st_wl_heur_init ⇒ bool› where
  ‹isasat_fast_init S ⟷
      (length (get_clauses_wl_heur_init S) ≤ snat64_max - (unat32_max div 2 + MAX_HEADER_SIZE+1) ∧
       learned_clss_count_init S < unat64_max)›

definition empty_init_code :: ‹bool × _ list × isasat_stats› where
  ‹empty_init_code = (True, [], empty_stats)›

definition empty_conflict_code :: ‹(bool × _ list × isasat_stats) nres› where
  ‹empty_conflict_code = do{
     let M0 = [];
     RETURN (False, M0, empty_stats)}›

definition extract_model_of_state_stat :: ‹isasat ⇒ bool × nat literal list × isasat_stats› where
  ‹extract_model_of_state_stat U =
     (False, (fst (get_trail_wl_heur U)), (get_stats_heur U))›

definition extract_state_stat :: ‹isasat ⇒ bool × nat literal list × isasat_stats› where
  ‹extract_state_stat U =
     (True, [], (get_stats_heur U))›

definition empty_conflict :: ‹nat literal list option› where
  ‹empty_conflict = Some []›

definition IsaSAT_bounded_heur :: ‹opts ⇒ nat clause_l list ⇒ (bool × (bool × nat literal list × isasat_stats)) nres› where
  ‹IsaSAT_bounded_heur opts CS = do{
    _ ← RETURN (IsaSAT_Profile.start_initialisation);
    ASSERT(isasat_input_bounded (mset_set (extract_atms_clss CS {})));
    ASSERT(∀C∈set CS. ∀L∈set C. nat_of_lit L ≤ unat32_max);
    let 𝒜in' = mset_set (extract_atms_clss CS {});
    ASSERT(isasat_input_bounded 𝒜in');
    ASSERT(distinct_mset 𝒜in');
    let 𝒜in'' = virtual_copy 𝒜in';
    let b = opts_unbounded_mode opts;
    S ← init_state_wl_heur_fast 𝒜in';
    (T::twl_st_wl_heur_init) ← init_dt_wl_heur_b CS S;
    let T = convert_state 𝒜in'' T;
    _ ← RETURN (IsaSAT_Profile.stop_initialisation);
    if isasat_fast_init T ∧ ¬is_failed_heur_init T
    then do {
      if ¬get_conflict_wl_is_None_heur_init T
      then RETURN (False, empty_init_code)
      else if CS = [] then do {stat ← empty_conflict_code; RETURN (False, stat)}
      else do {
        _ ← RETURN (IsaSAT_Profile.start_initialisation);
        ASSERT(𝒜in'' ≠ {#});
        ASSERT(isasat_input_bounded_nempty 𝒜in'');
        _ ← isasat_information_banner T;
        ASSERT(rewatch_heur_st_fast_pre T);
        T ← rewatch_heur_st_init T;
        ASSERT(isasat_fast_init T);
        T ← finalise_init_code opts (T::twl_st_wl_heur_init);
        _ ← RETURN (IsaSAT_Profile.stop_initialisation);
        ASSERT(isasat_fast T);
        (b, U) ← cdcl_twl_stgy_restart_prog_bounded_wl_heur T;
        RETURN (b, if ¬b ∧ get_conflict_wl_is_None_heur U then extract_model_of_state_stat U
          else extract_state_stat U)
      }
    }
    else RETURN (True, empty_init_code)
  }›


end