Theory IsaSAT_Propagate_Conflict

theory IsaSAT_Propagate_Conflict
  imports IsaSAT_Setup IsaSAT_Inner_Propagation IsaSAT_Propagate_Conflict_Defs
begin


chapter ‹Propagation Loop And Conflict›

section ‹Unit Propagation, Inner Loop›

definition (in -) length_ll_fs :: ‹nat twl_st_wl ⇒ nat literal ⇒ nat› where
  ‹length_ll_fs = (λ(_, _, _, _, _, _, _, _, _, _, _, _, W) L. length (W L))›

definition (in -) length_ll_fs_heur :: ‹isasat ⇒ nat literal ⇒ nat› where
  ‹length_ll_fs_heur S L = length (watched_by_int S L)›


lemma unit_propagation_inner_loop_wl_loop_D_heur_fast:
  ‹length (get_clauses_wl_heur b) ≤ unat64_max ⟹
    unit_propagation_inner_loop_wl_loop_D_heur_inv b a (a1', a1'a, a2'a) ⟹
     length (get_clauses_wl_heur a2'a) ≤ unat64_max›
  unfolding unit_propagation_inner_loop_wl_loop_D_heur_inv_def
  by auto

lemma unit_propagation_inner_loop_wl_loop_D_heur_alt_def:
  ‹unit_propagation_inner_loop_wl_loop_D_heur L S⇩0 = do {
    ASSERT (length (watched_by_int S⇩0 L) ≤ length (get_clauses_wl_heur S⇩0));
    n ← mop_length_watched_by_int S⇩0 L;
    let b = (0, 0, S⇩0);
    WHILE⇩T⇗unit_propagation_inner_loop_wl_loop_D_heur_inv S⇩0 L⇖
      (λ(j, w, S). w < n ∧ get_conflict_wl_is_None_heur S)
      (λ(j, w, S). do {
        unit_propagation_inner_loop_body_wl_heur L j w S
      })
      b
  }›
  unfolding unit_propagation_inner_loop_wl_loop_D_heur_def Let_def
    IsaSAT_Profile.start_def IsaSAT_Profile.stop_def  ..


section ‹Unit propagation, Outer Loop›

lemma select_and_remove_from_literals_to_update_wl_heur_alt_def:
  ‹select_and_remove_from_literals_to_update_wl_heur =
   (λS. do {
      let j = literals_to_update_wl_heur S;
      ASSERT(j < length (fst (get_trail_wl_heur S)));
      ASSERT(j + 1 ≤ unat32_max);
      L ← isa_trail_nth (get_trail_wl_heur S) j;
      RETURN (set_literals_to_update_wl_heur (j+1) S, -L)
     })
    ›
  unfolding select_and_remove_from_literals_to_update_wl_heur_def
  apply (intro ext)
  apply (rename_tac S; case_tac S)
  by (auto intro!: ext simp: rev_trail_nth_def Let_def)

lemma unit_propagation_outer_loop_wl_D_heur_fast:
  ‹length (get_clauses_wl_heur x) ≤ unat64_max ⟹
       unit_propagation_outer_loop_wl_D_heur_inv x s' ⟹
       length (get_clauses_wl_heur a1') =
       length (get_clauses_wl_heur s') ⟹
       length (get_clauses_wl_heur s') ≤ unat64_max›
  by (auto simp: unit_propagation_outer_loop_wl_D_heur_inv_def)

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) ∈
    {(S, T). (S, T) ∈ twl_st_heur ∧ get_learned_count S = lcount} →⇩f
       ⟨{(S, T). (S, T) ∈ twl_st_heur ∧ get_learned_count S = lcount}⟩ nres_rel›
  using twl_st_heur''D_twl_st_heurD[OF
     unit_propagation_outer_loop_wl_D_heur_unit_propagation_outer_loop_wl_D']
  .

end