Theory IsaSAT_Phasing

theory IsaSAT_Phasing
  imports IsaSAT_Literals
begin

subsection ‹Phase saving›

type_synonym phase_saver = ‹bool list›

definition phase_saving :: ‹nat multiset ⇒ phase_saver ⇒ bool› where
‹phase_saving 𝒜 φ ⟷ (∀L∈atms_of (ℒ⇩a⇩l⇩l 𝒜). L < length φ)›

text ‹Save phase as given (e.g. for literals in the trail):›
definition save_phase :: ‹nat literal ⇒ phase_saver ⇒ phase_saver› where
  ‹save_phase L φ = φ[atm_of L := is_pos L]›

lemma phase_saving_save_phase[simp]:
  ‹phase_saving 𝒜 (save_phase L φ) ⟷ phase_saving 𝒜 φ›
  by (auto simp: phase_saving_def save_phase_def)

text ‹Save opposite of the phase (e.g. for literals in the conflict clause):›
definition save_phase_inv :: ‹nat literal ⇒ phase_saver ⇒ phase_saver› where
  ‹save_phase_inv L φ = φ[atm_of L := ¬is_pos L]›
 
end