theory IsaSAT_Show_LLVM imports IsaSAT_Show IsaSAT_Setup_LLVM begin sepref_register isasat_current_information print_c print_uint64 sepref_def print_c_impl is ‹RETURN o print_c› :: ‹word_assn⇧k →⇩a unit_assn› unfolding print_c_def by sepref sepref_def print_uint64_impl is ‹RETURN o print_uint64› :: ‹word_assn⇧k →⇩a unit_assn› unfolding print_uint64_def by sepref sepref_def print_open_colour_impl is ‹RETURN o print_open_colour› :: ‹word_assn⇧k →⇩a unit_assn› unfolding print_open_colour_def by sepref sepref_def print_close_colour_impl is ‹RETURN o print_close_colour› :: ‹word_assn⇧k →⇩a unit_assn› unfolding print_close_colour_def by sepref sepref_def print_char_impl is ‹RETURN o print_char› :: ‹word_assn⇧k →⇩a unit_assn› unfolding print_char_def by sepref sepref_def zero_some_stats_impl is ‹RETURN o zero_some_stats› :: ‹stats_assn⇧d →⇩a stats_assn› unfolding zero_some_stats_def by sepref sepref_def isasat_current_information_impl [llvm_code] is ‹uncurry2 (RETURN ooo isasat_current_information)› :: ‹word_assn⇧k *⇩a stats_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a stats_assn› unfolding isasat_current_information_def isasat_current_information_def by sepref declare isasat_current_information_impl.refine[sepref_fr_rules] lemma current_restart_phase_alt_def: ‹current_restart_phase = (λ(fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase), wasted, φ). restart_phase)› by (auto intro!: ext) sepref_def current_restart_phase_impl is ‹RETURN o current_restart_phase› :: ‹heuristic_assn⇧k →⇩a word_assn› unfolding current_restart_phase_alt_def heuristic_assn_def by sepref sepref_def isasat_current_status_fast_code is ‹isasat_current_status› :: ‹isasat_bounded_assn⇧d →⇩a isasat_bounded_assn› supply [[goals_limit=1]] unfolding isasat_bounded_assn_def isasat_current_status_def unfolding fold_tuple_optimizations by sepref sepref_def isasat_print_progress_impl is ‹uncurry3 (RETURN oooo isasat_print_progress)› :: ‹word_assn⇧k *⇩a word_assn⇧k *⇩a stats_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a unit_assn› unfolding isasat_print_progress_def by sepref term isasat_current_progress sepref_def isasat_current_progress_impl is ‹uncurry isasat_current_progress› :: ‹word_assn⇧k *⇩a isasat_bounded_assn⇧k →⇩a unit_assn› supply [[goals_limit=1]] unfolding isasat_bounded_assn_def isasat_current_progress_def unfolding fold_tuple_optimizations by sepref end