Theory IsaSAT_Propagate_Conflict

theory IsaSAT_Propagate_Conflict
  imports IsaSAT_Setup IsaSAT_Inner_Propagation
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 :: ‹twl_st_wl_heur ⇒ nat literal ⇒ nat› where
  ‹length_ll_fs_heur S L = length (watched_by_int S L)›

lemma length_ll_fs_heur_alt_def:
  ‹length_ll_fs_heur = (λ(M, N, D, Q, W, _) L. length (W ! nat_of_lit L))›
  unfolding length_ll_fs_heur_def
  apply (intro ext)
  apply (case_tac S)
  by auto

lemma (in -) get_watched_wl_heur_def: ‹get_watched_wl_heur = (λ(M, N, D, Q, W, _). W)›
  by (intro ext, rename_tac x, case_tac x) auto


lemma unit_propagation_inner_loop_wl_loop_D_heur_fast:
  ‹length (get_clauses_wl_heur b) ≤ uint64_max ⟹
    unit_propagation_inner_loop_wl_loop_D_heur_inv b a (a1', a1'a, a2'a) ⟹
     length (get_clauses_wl_heur a2'a) ≤ uint64_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 ..


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 =
   (λ(M', N', D', j, W', vm, φ, clvls, cach, lbd, outl, stats, fast_ema, slow_ema, ccount,
       vdom, lcount). do {
      ASSERT(j < length (fst M'));
      ASSERT(j + 1 ≤ uint32_max);
      L ← isa_trail_nth M' j;
      RETURN ((M', N', D', j+1, W', vm, φ, clvls, cach, lbd, outl, stats, fast_ema, slow_ema, ccount,
       vdom, lcount), -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)

definition  literals_to_update_wl_literals_to_update_wl_empty :: ‹twl_st_wl_heur ⇒ bool› where
  ‹literals_to_update_wl_literals_to_update_wl_empty S ⟷
    literals_to_update_wl_heur S < isa_length_trail (get_trail_wl_heur S)›


lemma literals_to_update_wl_literals_to_update_wl_empty_alt_def:
  ‹literals_to_update_wl_literals_to_update_wl_empty =
    (λ(M', N', D', j, W', vm, φ, clvls, cach, lbd, outl, stats, fast_ema, slow_ema, ccount,
       vdom, lcount). j < isa_length_trail M')›
  unfolding literals_to_update_wl_literals_to_update_wl_empty_def isa_length_trail_def
  by (auto intro!: ext split: prod.splits)

lemma unit_propagation_outer_loop_wl_D_invI:
  ‹unit_propagation_outer_loop_wl_D_heur_inv S⇩0 S ⟹
    isa_length_trail_pre (get_trail_wl_heur S)›
  unfolding unit_propagation_outer_loop_wl_D_heur_inv_def
  by blast

lemma unit_propagation_outer_loop_wl_D_heur_fast:
  ‹length (get_clauses_wl_heur x) ≤ uint64_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') ≤ uint64_max›
  by (auto simp: unit_propagation_outer_loop_wl_D_heur_inv_def)

end