theory IsaSAT_CDCL_LLVM imports IsaSAT_CDCL IsaSAT_Propagate_Conflict_LLVM IsaSAT_Conflict_Analysis_LLVM IsaSAT_Backtrack_LLVM IsaSAT_Decide_LLVM IsaSAT_Show_LLVM begin sepref_register get_conflict_wl_is_None decide_wl_or_skip_D_heur skip_and_resolve_loop_wl_D_heur backtrack_wl_D_nlit_heur isasat_current_status count_decided_st_heur get_conflict_wl_is_None_heur sepref_def cdcl_twl_o_prog_wl_D_fast_code is ‹cdcl_twl_o_prog_wl_D_heur› :: ‹[isasat_fast]⇩a isasat_bounded_assn⇧d → bool1_assn ×⇩a isasat_bounded_assn› unfolding cdcl_twl_o_prog_wl_D_heur_def PR_CONST_def unfolding get_conflict_wl_is_None get_conflict_wl_is_None_heur_alt_def[symmetric] supply [[goals_limit = 1]] isasat_fast_def[simp] apply (annot_unat_const "TYPE(32)") by sepref declare cdcl_twl_o_prog_wl_D_fast_code.refine[sepref_fr_rules] sepref_register unit_propagation_outer_loop_wl_D_heur cdcl_twl_o_prog_wl_D_heur definition length_clauses_heur where ‹length_clauses_heur S = length (get_clauses_wl_heur S)› lemma length_clauses_heur_alt_def: ‹length_clauses_heur = (λ(M, N, _). length N)› by (auto intro!: ext simp: length_clauses_heur_def) sepref_def length_clauses_heur_impl is ‹RETURN o length_clauses_heur› :: ‹isasat_bounded_assn⇧k →⇩a sint64_nat_assn› unfolding length_clauses_heur_alt_def isasat_bounded_assn_def by sepref declare length_clauses_heur_impl.refine [sepref_fr_rules] lemma isasat_fast_alt_def: ‹isasat_fast S = (length_clauses_heur S ≤ 9223372034707292154)› by (auto simp: isasat_fast_def sint64_max_def uint32_max_def length_clauses_heur_def) sepref_def isasat_fast_impl is ‹RETURN o isasat_fast› :: ‹isasat_bounded_assn⇧k →⇩a bool1_assn› unfolding isasat_fast_alt_def apply (annot_snat_const "TYPE(64)") by sepref declare isasat_fast_impl.refine[sepref_fr_rules] sepref_def cdcl_twl_stgy_prog_wl_D_code is ‹cdcl_twl_stgy_prog_bounded_wl_heur› :: ‹isasat_bounded_assn⇧d →⇩a bool1_assn ×⇩a isasat_bounded_assn› unfolding cdcl_twl_stgy_prog_bounded_wl_heur_def PR_CONST_def supply [[goals_limit = 1]] isasat_fast_length_leD[dest] by sepref declare cdcl_twl_stgy_prog_wl_D_code.refine[sepref_fr_rules] export_llvm cdcl_twl_stgy_prog_wl_D_code file "code/isasat.ll" end