Theory IsaSAT_Simplify_Units_Defs

theory IsaSAT_Simplify_Units_Defs
  imports IsaSAT_Setup
    Watched_Literals.Watched_Literals_Watch_List_Inprocessing
    More_Refinement_Libs.WB_More_Refinement_Loops
    IsaSAT_Proofs
begin

definition simplify_clause_with_unit2_pre where
  ‹simplify_clause_with_unit2_pre C M N ⟷
     C ∈# dom_m N ∧ no_dup M›

definition simplify_clause_with_unit2 where
  ‹simplify_clause_with_unit2 C M N0 = do {
        ASSERT(C ∈# dom_m N0);
        let l = length (N0 ∝ C);
        (i, j, N, del, is_true) ← WHILET⇗(λ(i, j, N, del, b). C ∈# dom_m N)⇖
        (λ(i, j, N, del, b). ¬b ∧ j < l)
        (λ(i, j, N, del, is_true). do {
           ASSERT(i < length (N ∝ C) ∧ j < length (N ∝ C) ∧ C ∈# dom_m N ∧ i ≤ j);
           let L = N ∝ C ! j;
           ASSERT(L ∈ set (N0 ∝ C));
           let val = polarity M L;
           if val = Some True then RETURN (i, j+1, N, add_mset L del, True)
           else if val = Some False
           then RETURN (i, j+1, N, add_mset L del, False)
           else RETURN (i+1, j+1, N(C ↪ ((N ∝ C)[i := L])), del, False)
        })
         (0, 0, N0, {#}, False);
    ASSERT(C ∈# dom_m N ∧ i ≤ length (N ∝ C));
    ASSERT(is_true ∨ j = l);
    let L = N ∝ C ! 0;
    if is_true ∨ i ≤ 1
    then RETURN (False, fmdrop C N, L, is_true, i)
    else if i = j ∧ ¬is_true then RETURN (True, N, L, is_true, i)
    else do {
      RETURN (False, N(C ↪ (take i (N ∝ C))), L, is_true, i)
    }
  }›




definition simplify_clause_with_unit_st2 :: ‹nat ⇒ nat twl_st_wl ⇒ nat twl_st_wl nres› where
  ‹simplify_clause_with_unit_st2 =  (λC (M, N0, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W). do {
    ASSERT(simplify_clause_with_unit_st_wl_pre C (M, N0, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W));
    ASSERT (C ∈# dom_m N0 ∧ count_decided M = 0 ∧ D = None);
    let S =  (M, N0, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W);
    let E = mset (N0 ∝ C);
    let irr = irred N0 C;
    (unc, N, L, b, i) ← simplify_clause_with_unit2 C M N0;
    ASSERT(dom_m N ⊆# dom_m N0);
      if unc then do {
      ASSERT(N = N0);
      let T = (M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W);
      RETURN T
    }
    else if b then do {
       let T = (M, N, D, (if irr then add_mset E else id) NE, (if ¬irr then add_mset E else id) UE, NEk, UEk, NS, US, N0, U0, Q, W);
      ASSERT (set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S));
      ASSERT (set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S));
      ASSERT (set_mset (all_atms_st T) = set_mset (all_atms_st S));
      ASSERT (size (learned_clss_lf N) = size (learned_clss_lf N0) - (if irr then 0 else 1));
      ASSERT(¬irr ⟶ size (learned_clss_lf N0) ≥ 1);
      RETURN T
    }
    else if i = 1
    then do {
      ASSERT (undefined_lit M L ∧ L ∈# ℒall (all_atms_st S));
      M ← cons_trail_propagate_l L 0 M;
      let T = (M, N, D, NE, UE, (if irr then add_mset {#L#} else id) NEk, (if ¬irr then add_mset {#L#} else id)UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id)US, N0, U0, add_mset (-L) Q, W);
      ASSERT (set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S));
      ASSERT (set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S));
      ASSERT (set_mset (all_atms_st T) = set_mset (all_atms_st S));
      ASSERT (size (learned_clss_lf N) = size (learned_clss_lf N0) - (if irr then 0 else 1));
      ASSERT(¬irr ⟶ size (learned_clss_lf N0) ≥ 1);
      RETURN T
   }
    else if i = 0
    then do {
      let j = length M;
      let T = (M, N, Some {#}, NE, UE, NEk, UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id) US, (if irr then add_mset {#} else id) N0, (if ¬irr then add_mset {#} else id)U0, {#}, W);
      ASSERT (set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S));
      ASSERT (set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S));
      ASSERT (set_mset (all_atms_st T) = set_mset (all_atms_st S));
      ASSERT (size (learned_clss_lf N) = size (learned_clss_lf N0) - (if irr then 0 else 1));
      ASSERT(¬irr ⟶ size (learned_clss_lf N0) ≥ 1);
      RETURN T
    }
    else do {
      let T = (M, N, D, NE, UE, NEk, UEk, (if irr then add_mset E else id) NS, (if ¬irr then add_mset E else id) US, N0, U0, Q, W);
      ASSERT (set_mset (all_learned_lits_of_wl T) = set_mset (all_learned_lits_of_wl S));
      ASSERT (set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S));
      ASSERT (set_mset (all_atms_st T) = set_mset (all_atms_st S));
      ASSERT (size (learned_clss_lf N) = size (learned_clss_lf N0));
      ASSERT (C ∈# dom_m N);
      RETURN T
    }
        })›

definition simplify_clauses_with_unit_st2 :: ‹nat twl_st_wl ⇒ nat twl_st_wl nres›  where
  ‹simplify_clauses_with_unit_st2 S =
  do {
  ASSERT (simplify_clauses_with_unit_st_wl_pre S);
  xs ← SPEC(λxs. finite xs);
  T ← FOREACHci(λit T. simplify_clauses_with_unit_st_wl_inv S it T)
  (xs)
  (λS. get_conflict_wl S = None)
  (λi S. if i ∈# dom_m (get_clauses_wl S)
            then simplify_clause_with_unit_st2 i S else RETURN S)
  S;
  ASSERT(set_mset (all_learned_lits_of_wl T) ⊆ set_mset (all_learned_lits_of_wl S));
  ASSERT(set_mset (all_init_lits_of_wl T) = set_mset (all_init_lits_of_wl S));
  RETURN T
  }›

definition isa_simplify_clause_with_unit2 where
  ‹isa_simplify_clause_with_unit2 C M N = do {
     l ← mop_arena_length N C;
    ASSERT(l < length N ∧ l ≤ Suc (unat32_max div 2));
    (i, j, N::arena, is_true) ← WHILET(λ(i, j, N::arena, b). ¬b ∧ j < l)
    (λ(i, j, N, is_true). do {
      ASSERT(i ≤ j ∧ j < l);
      L ← mop_arena_lit2 N C j;
      val ← mop_polarity_pol M L;
      if val = Some True then RETURN (i, j+1, N,True)
      else if val = Some False
      then RETURN (i, j+1, N,  False)
        else do {
        N ← mop_arena_update_lit C i L N;
        RETURN (i+1, j+1, N, False)}
    })
      (0, 0, N, False);
   L ← mop_arena_lit2 N C 0;
   if is_true ∨ i ≤ 1
   then do {
     ASSERT(mark_garbage_pre (N, C));
     RETURN (False, extra_information_mark_to_delete N C, L, is_true, i)}
   else if i = j then RETURN (True, N, L, is_true, i)
   else do {
      N ← mop_arena_shorten C i N;
      RETURN (False, N, L, is_true, i)}
    }›

definition set_conflict_to_false :: ‹conflict_option_rel ⇒ conflict_option_rel› where
  ‹set_conflict_to_false = (λ(b, n, xs). (False, 0, xs))›

text ‹We butcher our statistics here, but the clauses are deleted later anyway.›
definition isa_simplify_clause_with_unit_st2 :: ‹nat ⇒ isasat ⇒ isasat nres› where
  ‹isa_simplify_clause_with_unit_st2 =  (λC S. do {
   let lcount = get_learned_count S; let N = get_clauses_wl_heur S; let M = get_trail_wl_heur S;
   E ← mop_arena_status N C;
   ASSERT(E = LEARNED ⟶ 1 ≤ clss_size_lcount lcount);
   (unc, N, L, b, i) ← isa_simplify_clause_with_unit2 C M N;
   ASSERT (length N ≤ length (get_clauses_wl_heur S));
   if unc then RETURN (set_clauses_wl_heur N S)
   else if b then
   RETURN  (set_clauses_wl_heur N
     (set_stats_wl_heur (if E=LEARNED then (get_stats_heur S) else (decr_irred_clss (get_stats_heur S)))
     (set_learned_count_wl_heur (if E = LEARNED then clss_size_decr_lcount (lcount) else lcount)
     S)))
   else if i = 1
   then do {
     M ← cons_trail_Propagated_tr L 0 M;
     RETURN (set_clauses_wl_heur N
     (set_trail_wl_heur M
     (set_stats_wl_heur (if E=LEARNED then incr_uset (get_stats_heur S) else incr_uset (decr_irred_clss (get_stats_heur S)))
     (set_learned_count_wl_heur (if E = LEARNED then clss_size_decr_lcount (clss_size_incr_lcountUEk lcount) else lcount)
     S)))) }
   else if i = 0
   then do {
     j ← mop_isa_length_trail M;
     RETURN (set_clauses_wl_heur N
     (set_conflict_wl_heur (set_conflict_to_false (get_conflict_wl_heur S))
     (set_count_max_wl_heur 0
     (set_literals_to_update_wl_heur j
     (set_stats_wl_heur (if E=LEARNED then get_stats_heur S else decr_irred_clss (get_stats_heur S))
     (set_learned_count_wl_heur (if E = LEARNED then clss_size_decr_lcount lcount else lcount)
     S))))))
   }
   else do {
       let S = (set_clauses_wl_heur N S);
       _ ← log_new_clause_heur S C;
       RETURN S
     }
   })›

definition isa_simplify_clauses_with_unit_st2 :: ‹isasat ⇒ isasat nres›  where
  ‹isa_simplify_clauses_with_unit_st2 S =
  do {
     xs ← RETURN (get_avdom S @ get_ivdom S);
    ASSERT(length xs ≤ length (get_vdom S) ∧ length (get_vdom S) ≤ length (get_clauses_wl_heur S));
    (_, T) ← WHILET
      (λ(i, T). i < length xs ∧ get_conflict_wl_is_None_heur T)
      (λ(i,T). do {
           ASSERT((i < length (get_avdom T) ⟶ access_avdom_at_pre T i) ∧
           (i ≥ length (get_avdom T) ⟶ access_ivdom_at_pre T (i - length_avdom S)) ∧
           length_avdom T = length_avdom S ∧
           length (get_clauses_wl_heur T) = length (get_clauses_wl_heur S) ∧
            learned_clss_count T ≤ learned_clss_count S);
          let C = (if i < length (get_avdom S) then access_avdom_at T i else access_ivdom_at T (i - length_avdom S));
          E ← mop_arena_status (get_clauses_wl_heur T) C;
          if E ≠ DELETED then do {
          T ← isa_simplify_clause_with_unit_st2 C T;
          ASSERT(i < length xs);
          RETURN (i+1, T)
        }
        else do {ASSERT(i < length xs); RETURN (i+1,T)}
      })
     (0, S);
    RETURN (reset_units_since_last_GC_st T)
  }›

definition simplify_clauses_with_units_st_wl2 :: ‹_› where
  ‹simplify_clauses_with_units_st_wl2 S = do {
  b ← SPEC(λb::bool. b ⟶ get_conflict_wl S =None);
  if b then simplify_clauses_with_unit_st2 S else RETURN S
  }›

definition isa_simplify_clauses_with_units_st_wl2 :: ‹_› where
  ‹isa_simplify_clauses_with_units_st_wl2 S = do {
  b ← RETURN (get_conflict_wl_is_None_heur S ∧ units_since_last_GC_st S > 0);
  if b then isa_simplify_clauses_with_unit_st2 S else RETURN S
  }›

end