Theory IsaSAT_Restart_Inprocessing_Defs

(*TODO Rename to IsaSAT_Inprocessing*)
theory IsaSAT_Restart_Inprocessing_Defs
  imports IsaSAT_Setup
    IsaSAT_Simplify_Units_Defs
    Watched_Literals.Watched_Literals_Watch_List_Inprocessing
    More_Refinement_Libs.WB_More_Refinement_Loops
    IsaSAT_Restart_Defs
    IsaSAT_Simplify_Binaries_Defs
    IsaSAT_Simplify_Pure_Literals_Defs
    IsaSAT_Simplify_Forward_Subsumption_Defs
begin

definition isa_pure_literal_elimination_round_wl where
  ‹isa_pure_literal_elimination_round_wl S⇩0 = do {
    ASSERT (isa_pure_literal_elimination_round_wl_pre S⇩0);
    S ← isa_simplify_clauses_with_units_st_wl2 S⇩0;
    ASSERT (length (get_clauses_wl_heur S) = length (get_clauses_wl_heur S⇩0));
    ASSERT (learned_clss_count S ≤ learned_clss_count S⇩0);
    if get_conflict_wl_is_None_heur S
    then do {
     (abort, occs) ← isa_pure_literal_count_occs_wl (S);
      if ¬abort then isa_pure_literal_deletion_wl occs S
      else RETURN (0, S)}
    else RETURN (0, S)
}›



definition isa_pure_literal_elimination_wl_pre :: ‹_› where
  ‹isa_pure_literal_elimination_wl_pre S = (∃T u r.
    (S, T) ∈ twl_st_heur_restart_ana' r u ∧ pure_literal_elimination_wl_pre T)›

definition isa_pure_literal_elimination_wl_inv :: ‹_› where
  ‹isa_pure_literal_elimination_wl_inv S max_rounds = (λ(T,m,abort). ∃S' T' u r.
  (S, S') ∈ twl_st_heur_restart_ana' r u ∧
  (T, T') ∈ twl_st_heur_restart_ana' r u ∧ pure_literal_elimination_wl_inv S' max_rounds (T', m, abort))›

definition isa_pure_literal_elimination_wl :: ‹isasat ⇒ isasat nres› where
  ‹isa_pure_literal_elimination_wl S⇩0 = do {
    ASSERT (isa_pure_literal_elimination_wl_pre S⇩0);
     max_rounds ← RETURN (3::nat);
    (S, _, _) ← WHILE⇩T⇗isa_pure_literal_elimination_wl_inv S⇩0 max_rounds⇖ (λ(S, m, abort). m < max_rounds ∧ ¬abort)
     (λ(S, m, abort). do {
         ASSERT (m ≤ max_rounds);
         ASSERT (length (get_clauses_wl_heur S) = length (get_clauses_wl_heur S⇩0));
         ASSERT (learned_clss_count S ≤ learned_clss_count S⇩0);
         let S = incr_purelit_rounds_st S;
         (elim, S) ← isa_pure_literal_elimination_round_wl S;
         abort ← RETURN (elim = 0);
         RETURN (S, m+1, abort)
       })
    (S⇩0, 0, False);
   RETURN (schedule_next_pure_lits_st S)
  }›

definition isa_pure_literal_eliminate :: ‹isasat ⇒ isasat nres› where
  ‹isa_pure_literal_eliminate S = do {
    let b = should_eliminate_pure_st S;
    if b then isa_pure_literal_elimination_wl S else RETURN S
}›

end