Theory IsaSAT_Simplify_Pure_Literals_Defs

theory IsaSAT_Simplify_Pure_Literals_Defs
  imports IsaSAT_Setup
    IsaSAT_Restart_Defs
begin
  definition isa_pure_literal_count_occs_clause_wl_invs :: ‹_› where
  ‹isa_pure_literal_count_occs_clause_wl_invs C S occs =
  (λ(i, occs2, remaining). ∃S' r u occs' occs2'. (S, S') ∈ twl_st_heur_restart_ana' r u ∧
    (occs, occs') ∈ ⟨bool_rel⟩map_fun_rel (D⇩0 (all_init_atms_st S')) ∧
    (occs2, occs2') ∈ ⟨bool_rel⟩map_fun_rel (D⇩0 (all_init_atms_st S')) ∧
    pure_literal_count_occs_clause_wl_invs C S' occs' (i, occs2'))›

definition isa_pure_literal_count_occs_clause_wl_pre :: ‹_› where
  ‹isa_pure_literal_count_occs_clause_wl_pre C S occs =
  (∃S' r u occs'. (S, S') ∈ twl_st_heur_restart_ana' r u ∧
    (occs, occs') ∈ ⟨bool_rel⟩map_fun_rel (D⇩0 (all_init_atms_st S')) ∧
    pure_literal_count_occs_clause_wl_pre C S' occs')›

definition isa_pure_literal_count_occs_clause_wl :: ‹nat ⇒ isasat ⇒ _ ⇒ 64 word ⇒ _› where
  ‹isa_pure_literal_count_occs_clause_wl C S occs remaining = do {
    ASSERT (isa_pure_literal_count_occs_clause_wl_pre C S occs);
    m ← mop_arena_length_st S C;
    (i, occs, _) ← WHILE⇩T⇗isa_pure_literal_count_occs_clause_wl_invs C S occs⇖ (λ(i, occs, remaining). i < m)
      (λ(i, occs, remaining). do {
        ASSERT (i < m);
        L ← mop_access_lit_in_clauses_heur S C i;
        ASSERT (nat_of_lit L < length occs);
        ASSERT (nat_of_lit (-L) < length occs);
        let remaining = (if ¬occs!(nat_of_lit L) ∧ occs ! (nat_of_lit (-L)) then remaining-1 else remaining);
        let occs = occs [nat_of_lit L := True];
        RETURN (i+1, occs, remaining)
      })
      (0, occs, remaining);
   RETURN (occs, remaining)
 }›

definition isa_pure_literal_count_occs_wl :: ‹isasat ⇒ _› where
  ‹isa_pure_literal_count_occs_wl S = do {
  let xs = get_avdom S @ get_ivdom S;
  let m = length (xs);
  let remaining = ((of_nat (length (get_watched_wl_heur S)) :: 64 word) >> 1) - units_since_beginning_st S;
  let abort = (remaining ≤ 0);
  let occs = replicate (length (get_watched_wl_heur S)) False;
  ASSERT (m ≤ length (get_clauses_wl_heur S) - 2);
  (_, occs, abort) ← WHILE⇩T(λ(i, occs, remaining). i < m ∧ remaining > 0)
      (λ(i, occs, remaining). do {
        ASSERT (i ≤ length (get_clauses_wl_heur S) - 2);
        ASSERT ((i < length (get_avdom S) ⟶ access_avdom_at_pre S i) ∧
           (i ≥ length (get_avdom S) ⟶ access_ivdom_at_pre S (i - length_avdom S)));
        let C = (get_avdom S @ get_ivdom S) ! i;
        E ← mop_arena_status (get_clauses_wl_heur S) C;
        if (E = IRRED) then do {
          (occs, remaining) ← isa_pure_literal_count_occs_clause_wl C S occs remaining;
          let abort = (remaining ≤ 0);
          RETURN (i+1, occs, remaining)
        } else RETURN  (i+1, occs, remaining)
      })
      (0, occs, remaining);
   RETURN (abort ≤ 0, occs)
  }›


definition isa_pure_literal_elimination_round_wl_pre where
  ‹isa_pure_literal_elimination_round_wl_pre S ⟷
  (∃T r u. (S, T) ∈ twl_st_heur_restart_ana' r u ∧ pure_literal_elimination_round_wl_pre T)›

definition isa_pure_literal_deletion_wl_pre :: ‹_› where
  ‹isa_pure_literal_deletion_wl_pre S ⟷
  (∃T r u. (S, T) ∈ twl_st_heur_restart_ana' r u ∧ pure_literal_deletion_wl_pre T)›


definition isa_propagate_pure_bt_wl
  :: ‹nat literal ⇒ isasat ⇒ isasat nres›
  where
    ‹isa_propagate_pure_bt_wl = (λL S. do {
      let M = get_trail_wl_heur S;
      let stats = get_stats_heur S;
      ASSERT(0 ≠ DECISION_REASON);
      ASSERT(cons_trail_Propagated_tr_pre ((L, 0::nat), M));
      M ← cons_trail_Propagated_tr (L) 0 M;
      let stats = incr_units_since_last_GC (incr_uset (incr_purelit_elim stats));
      let S = set_stats_wl_heur stats S;
      let S = set_trail_wl_heur M S;
      RETURN S})
›



definition isa_pure_literal_deletion_wl_raw :: ‹bool list ⇒ isasat ⇒ (64 word × isasat) nres› where
  ‹isa_pure_literal_deletion_wl_raw occs S⇩0 = (do {
    ASSERT (isa_pure_literal_deletion_wl_pre S⇩0);
    (eliminated, S) ← iterate_over_VMTF
      (λA (eliminated, T). do {
         ASSERT (get_vmtf_heur_array S⇩0 = get_vmtf_heur_array T);
         ASSERT (nat_of_lit (Pos A) < length occs);
         ASSERT (nat_of_lit (Neg A) < length occs);
         let L = (if occs ! (nat_of_lit (Pos A)) ∧ ¬ occs ! (nat_of_lit (Neg A))
                  then Pos A else Neg A);
         ASSERT (nat_of_lit (-L) < length occs);
         val ← mop_polarity_pol (get_trail_wl_heur T) L;
         if ¬occs ! (nat_of_lit (-L)) ∧ val = None
         then do {S ← isa_propagate_pure_bt_wl L T;
          ASSERT (get_vmtf_heur_array S⇩0 = get_vmtf_heur_array S);
          RETURN (eliminated + 1, S)}
        else RETURN (eliminated, T)
      })
     (λ(_, S). get_vmtf_heur_array S⇩0 = (get_vmtf_heur_array S))
     (get_vmtf_heur_array S⇩0, Some (get_vmtf_heur_fst S⇩0)) (0 :: 64 word, S⇩0);
   RETURN (eliminated, S)
})›

definition isa_pure_literal_deletion_wl :: ‹bool list ⇒ isasat ⇒ (64 word × isasat) nres› where
  ‹isa_pure_literal_deletion_wl occs S⇩0 = (do {
  ASSERT (isa_pure_literal_deletion_wl_pre S⇩0);
  (_, eliminated, S) ← WHILE⇩T⇗λ(n, _, S). get_vmtf_heur_array S⇩0 = get_vmtf_heur_array S⇖ (λ(n, x). n ≠ None)
    (λ(n, eliminated, T). do {
       ASSERT (n ≠ None);
       let A = the n;
       ASSERT (A < length (get_vmtf_heur_array S⇩0));
       ASSERT (A ≤ unat32_max div 2);
       ASSERT (get_vmtf_heur_array S⇩0 = get_vmtf_heur_array T);
       ASSERT (nat_of_lit (Pos A) < length occs);
       ASSERT (nat_of_lit (Neg A) < length occs);
       let L = (if occs ! nat_of_lit (Pos A) ∧ ¬ occs ! nat_of_lit (Neg A) then Pos A else Neg A);
       ASSERT (nat_of_lit (- L) < length occs);
       val ← mop_polarity_pol (get_trail_wl_heur T) L;
       if ¬ occs ! nat_of_lit (- L) ∧ val = None then do {
          S ← isa_propagate_pure_bt_wl L T;
          ASSERT (get_vmtf_heur_array S⇩0 = get_vmtf_heur_array S);
          RETURN (get_next (get_vmtf_heur_array S ! A),eliminated + 1, S)
       }
       else RETURN (get_next (get_vmtf_heur_array T ! A),eliminated, T)
     })
    (Some (get_vmtf_heur_fst S⇩0), 0, S⇩0);
  RETURN (eliminated, S)
})›


end