Theory IsaSAT_Proofs

theory IsaSAT_Proofs
  imports IsaSAT_Setup
begin
section ‹DRAT proof generation›

text ‹We do not prove anything about the proof we generate. In particular, it could be incorrect,
because some clauses is not printed.›

definition log_literal :: ‹nat literal ⇒ unit› where
  ‹log_literal _ = ()›

definition log_start_new_clause :: ‹nat ⇒ unit› where
  ‹log_start_new_clause _ = ()›

definition log_start_del_clause :: ‹nat ⇒ unit› where
  ‹log_start_del_clause _ = ()›

definition log_end_clause :: ‹nat ⇒ unit› where
  ‹log_end_clause _ = ()›

definition log_clause_heur :: ‹isasat ⇒ nat ⇒ unit nres› where
  ‹log_clause_heur S C = do {
     i ← mop_arena_length_st S C;
     ASSERT (i ≤ length (get_clauses_wl_heur S));
     _ ← WHILET (λj. j < i)
       (λj. do{ ASSERT (j<i);
               L ← mop_access_lit_in_clauses_heur S C j;
               let _ = log_literal L;
               RETURN (j+1)
        })
      0;
    RETURN ()
}›

definition log_clause2 :: ‹nat twl_st_wl ⇒ nat ⇒ unit nres› where
  ‹log_clause2 S C = do {
     ASSERT (C ∈# dom_m (get_clauses_wl S));
     let i = length (get_clauses_wl S ∝ C);
     _ ← WHILET (λj. j < i)
       (λj. do{
            ASSERT (j < i);
            let L = get_clauses_wl S ∝ C ! j;
            let _ = log_literal L;
            RETURN (j+1)
        })
      0;
    RETURN ()
   }›

definition log_clause :: ‹'v twl_st_wl ⇒ nat ⇒ unit› where ‹log_clause S _ = ()›

lemma log_clause2_log_clause:
  ‹(uncurry log_clause2, uncurry (RETURN oo log_clause)) ∈
  [λ(S,C). C ∈# dom_m (get_clauses_wl S)]f Id ×r nat_rel → ⟨unit_rel⟩nres_rel›
proof -
  show ?thesis
    unfolding log_clause_def log_clause2_def comp_def uncurry_def mop_arena_length_st_def
    apply (intro frefI nres_relI)
    subgoal for x y
    apply (refine_vcg WHILET_rule[where I = ‹λ_. True› and R = ‹measure (λi. length (get_clauses_wl (fst y) ∝ snd y) - i)›])
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    done
  done
qed

lemma log_clause_heur_log_clause2:
  assumes ‹(S,T) ∈ twl_st_heur› ‹(C,C') ∈ nat_rel›
  shows ‹log_clause_heur S C ≤⇓unit_rel (log_clause2 T C')›
proof -
  have [refine0]: ‹(0,0)∈nat_rel›
    by auto
  have length: ‹⇓ nat_rel ((RETURN ∘ (λc. length (get_clauses_wl T ∝ c))) C') ≤ SPEC (λc. (c, length (get_clauses_wl T ∝ C')) ∈ {(a,b). a=b ∧ a = length (get_clauses_wl T ∝ C)})›
    by (use assms in auto)
  show ?thesis
    unfolding log_clause_heur_def log_clause2_def comp_def uncurry_def mop_arena_length_st_def
      mop_access_lit_in_clauses_heur_def
    apply (refine_vcg mop_arena_lit[where vdom = ‹set (get_vdom S)› and N = ‹get_clauses_wl T›, THEN order_trans] 
      mop_arena_length[where vdom = ‹set (get_vdom S)›, THEN fref_to_Down_curry, THEN order_trans, unfolded prod.simps])
    apply assumption
    subgoal using assms by (auto simp: twl_st_heur_def)
    apply (rule length)
    subgoal by (use assms in ‹auto simp: twl_st_heur_def dest: arena_lifting(10)›)
    subgoal by auto
    subgoal using assms by (auto simp: twl_st_heur_def)
    apply assumption
    subgoal by (use assms in auto)
    apply (rule refl)
    subgoal by auto
    by auto
qed


definition log_new_clause_heur :: ‹isasat ⇒ nat ⇒ unit nres› where
  ‹log_new_clause_heur S C = do {
    let _ = log_start_new_clause 0;
    log_clause_heur S C;
    let _ = log_end_clause 0;
    RETURN ()
  }›

lemma log_new_clause_heur_alt_def:
  ‹log_new_clause_heur = log_clause_heur›
  by (auto intro!: ext simp: log_new_clause_heur_def log_clause_heur_def)

definition log_del_clause_heur :: ‹isasat ⇒ nat ⇒ unit nres› where
  ‹log_del_clause_heur S C = do {
    let _ = log_start_del_clause 0;
    log_clause_heur S C;
    let _ = log_end_clause 0;
    RETURN ()
  }›

lemma log_del_clause_heur_alt_def:
  ‹log_del_clause_heur = log_clause_heur›
  by (auto intro!: ext simp: log_del_clause_heur_def log_clause_heur_def)

lemma log_new_clause_heur_log_clause:
  assumes ‹(S,T) ∈ twl_st_heur› ‹(C,C') ∈ nat_rel› ‹C ∈# dom_m (get_clauses_wl T)›
  shows ‹log_new_clause_heur S C ≤ SPEC (λc. (c, log_clause T C') ∈ unit_rel)›
    unfolding log_new_clause_heur_alt_def
    apply (rule log_clause_heur_log_clause2[THEN order_trans, OF assms(1,2)])
    apply (rule order_trans)
    apply (rule ref_two_step')
    apply (rule log_clause2_log_clause[THEN fref_to_Down_curry])
    using assms by auto

definition log_unit_clause where
  ‹log_unit_clause L =
    (let _ = log_start_new_clause 0;
      _ = log_literal L;
      _ = log_end_clause 0 in
     ()
  )›

definition log_del_binary_clause where
  ‹log_del_binary_clause L L' =
    (let _ = log_start_del_clause 0;
      _ = log_literal L;
      _ = log_literal L';
      _ = log_end_clause 0 in
     ()
  )›

text ‹For removing unit literals, we cheat as usual: we signal to the C side which literals are in
and flush the clause if need be (without effect on the Isabelle side, because we neither want nor care
about the proofs).›

definition mark_literal_for_unit_deletion :: ‹nat literal ⇒ unit› where
  ‹mark_literal_for_unit_deletion _ = ()›

definition mark_clause_for_unit_as_unchanged :: ‹nat ⇒ unit› where
  ‹mark_clause_for_unit_as_unchanged _ = ()›

definition mark_clause_for_unit_as_changed :: ‹nat ⇒ unit› where
  ‹mark_clause_for_unit_as_changed _ = ()›

end