Theory IsaSAT_All_LLVM

theory IsaSAT_All_LLVM
  imports IsaSAT_LLVM IsaSAT
begin

definition model_assn where
  ‹model_assn = hr_comp model_stat_assn model_stat_rel›

definition model_bounded_assn where
  ‹model_bounded_assn =
   hr_comp (bool1_assn ×⇩a model_stat_assn⇩0)
   {((b, m), (b', m')). b=b' ∧ (¬b ⟶ (m,m') ∈ model_stat_rel)}›

definition clauses_l_assn where
  ‹clauses_l_assn = hr_comp (IICF_Array_of_Array_List.aal_assn unat_lit_assn)
    (list_mset_rel O ⟨list_mset_rel⟩mset_rel)›

theorem IsaSAT_full_correctness:
  ‹(uncurry IsaSAT_code, uncurry (λ_. model_if_satisfiable_bounded))
     ∈ [λ(_, a). (∀C∈#a. ∀L∈#C. nat_of_lit L ≤ unat32_max)]⇩a opts_assn⇧d *⇩a clauses_l_assn⇧d →
      model_bounded_assn›
  using IsaSAT_code.refine[FCOMP IsaSAT_bounded_heur_model_if_sat']
  unfolding model_bounded_assn_def clauses_l_assn_def
  by auto

end