theory IsaSAT_CDCL_LLVM imports IsaSAT_CDCL_Defs IsaSAT_Propagate_Conflict_LLVM IsaSAT_Other_LLVM begin 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