Theory IsaSAT_Reluctant

theory IsaSAT_Reluctant_LLVM imports IsaSAT_Reluctant WB_More_Word IsaSAT_Literals Watched_Literals.WB_More_IICF_LLVM IsaSAT_Literals_LLVM begin type_synonym reluctant_rel = ‹bool × bool × 64 word × 64 word × 64 word × 64 word × 64 word› type_synonym reluctant_rel_assn = ‹1 word × 1 word × 64 word × 64 word × 64 word × 64 word × 64 word› definition reluctant_rel_assn :: ‹reluctant_rel ⇒ reluctant_rel_assn⇒ assn›where ‹reluctant_rel_assn = bool1_assn ×_a bool1_assn ×_a word_assn ×_a word_assn ×_a word_assn ×_a word_assn ×_a word_assn› definition reluctant_rel :: ‹(reluctant_rel × reluctant) set› where ‹reluctant_rel = {((limited, trigger, u, v, period, wait, limit), r). limited = reluctant_limited r ∧ trigger = reluctant_trigger r ∧ u = reluctant_u r ∧ v = reluctant_v r ∧ period = reluctant_period r ∧ wait = reluctant_wait r ∧ limit = reluctant_limit r}› definition reluctant_assn where ‹reluctant_assn = hr_comp reluctant_rel_assn reluctant_rel› schematic_goal mk_free_reluctant_rel_assn[sepref_frame_free_rules]: ‹MK_FREE reluctant_rel_assn ?fr› unfolding reluctant_rel_assn_def by synthesize_free schematic_goal mk_free_reluctant_assn[sepref_frame_free_rules]: ‹MK_FREE reluctant_assn ?fr› unfolding reluctant_assn_def by synthesize_free lemma [safe_constraint_rules]: ‹CONSTRAINT Sepref_Basic.is_pure reluctant_rel_assn› ‹CONSTRAINT Sepref_Basic.is_pure reluctant_assn› unfolding reluctant_rel_assn_def reluctant_assn_def by (auto intro!: hr_comp_is_pure) definition reluctant_c :: ‹ _ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ _ ⇒ reluctant_rel›where ‹reluctant_c limited trigger u v period wait limit = (limited, trigger, u, v, period, wait, limit)› lemma reluctant_c_Reluctant: ‹(uncurry6 (RETURN ooooooo reluctant_c), uncurry6 (RETURN ooooooo Reluctant)) ∈ Id ×_f Id ×_f Id ×_f Id ×_f Id ×_f Id ×_f Id → ⟨reluctant_rel⟩nres_rel› by (auto simp: reluctant_c_def reluctant_rel_def intro!: frefI nres_relI) sepref_register reluctant_c sepref_def reluctant_impl is ‹uncurry6 (RETURN ooooooo reluctant_c)› :: ‹bool1_assn^k *_a bool1_assn^k *_a word_assn^k *_a word_assn^k *_a word_assn^k *_a word_assn^k *_a word_assn^k →_a reluctant_rel_assn› unfolding reluctant_c_def reluctant_rel_assn_def by sepref lemmas [sepref_fr_rules] = reluctant_impl.refine[FCOMP reluctant_c_Reluctant, unfolded reluctant_assn_def[symmetric]] definition reluctant_c_limited :: ‹reluctant_rel ⇒ bool›where ‹reluctant_c_limited = (λ(limited, trigger, u, v, period, wait, limit). limited)› definition reluctant_c_triggered :: ‹reluctant_rel ⇒ bool›where ‹reluctant_c_triggered = (λ(triggered, trigger, u, v, period, wait, limit). trigger)› definition reluctant_c_u :: ‹reluctant_rel ⇒ 64 word›where ‹reluctant_c_u = (λ(triggered, trigger, u, v, period, wait, limit). u)› definition reluctant_c_v :: ‹reluctant_rel ⇒ 64 word›where ‹reluctant_c_v = (λ(triggered, trigger, u, v, period, wait, limit). v)› definition reluctant_c_period :: ‹reluctant_rel ⇒ 64 word›where ‹reluctant_c_period = (λ(triggered, trigger, u, v, period, wait, limit). period)› definition reluctant_c_wait :: ‹reluctant_rel ⇒ 64 word›where ‹reluctant_c_wait = (λ(triggered, trigger, u, v, period, wait, limit). wait)› definition reluctant_c_limit :: ‹reluctant_rel ⇒ 64 word›where ‹reluctant_c_limit = (λ(triggered, trigger, u, v, period, wait, limit). limit)› sepref_def reluctant_limited_impl is ‹RETURN o reluctant_c_limited› :: ‹reluctant_rel_assn^k →_a bool1_assn› unfolding reluctant_c_limited_def reluctant_rel_assn_def by sepref sepref_def reluctant_triggered_impl is ‹RETURN o reluctant_c_triggered› :: ‹reluctant_rel_assn^k →_a bool1_assn› unfolding reluctant_c_triggered_def reluctant_rel_assn_def by sepref sepref_def reluctant_u_impl is ‹RETURN o reluctant_c_u› :: ‹reluctant_rel_assn^k →_a word64_assn› unfolding reluctant_c_u_def reluctant_rel_assn_def by sepref sepref_def reluctant_v_impl is ‹RETURN o reluctant_c_v› :: ‹reluctant_rel_assn^k →_a word64_assn› unfolding reluctant_c_v_def reluctant_rel_assn_def by sepref sepref_def reluctant_wait_impl is ‹RETURN o reluctant_c_wait› :: ‹reluctant_rel_assn^k →_a word64_assn› unfolding reluctant_c_wait_def reluctant_rel_assn_def by sepref sepref_def reluctant_period_impl is ‹RETURN o reluctant_c_period› :: ‹reluctant_rel_assn^k →_a word64_assn› unfolding reluctant_c_period_def reluctant_rel_assn_def by sepref sepref_def reluctant_limit_impl is ‹RETURN o reluctant_c_limit› :: ‹reluctant_rel_assn^k →_a word64_assn› unfolding reluctant_c_limit_def reluctant_rel_assn_def by sepref lemma reluctant_c_limited: ‹(reluctant_c_limited, reluctant_limited) ∈ reluctant_rel → Id› and reluctant_c_triggered: ‹(reluctant_c_triggered, reluctant_trigger) ∈ reluctant_rel → Id› and reluctant_c_u: ‹(reluctant_c_u, reluctant_u) ∈ reluctant_rel → Id› and reluctant_c_v: ‹(reluctant_c_v, reluctant_v) ∈ reluctant_rel → Id› and reluctant_c_wait: ‹(reluctant_c_wait, reluctant_wait) ∈ reluctant_rel → Id› and reluctant_c_period: ‹(reluctant_c_period, reluctant_period) ∈ reluctant_rel → Id› and reluctant_c_limit: ‹(reluctant_c_limit, reluctant_limit) ∈ reluctant_rel → Id› by (auto simp: reluctant_rel_def reluctant_c_limited_def reluctant_c_triggered_def reluctant_c_u_def reluctant_c_v_def reluctant_c_wait_def reluctant_c_period_def reluctant_c_limit_def intro!: frefI nres_relI) lemmas [sepref_fr_rules] = reluctant_limited_impl.refine[FCOMP reluctant_c_limited, unfolded reluctant_assn_def[symmetric]] reluctant_triggered_impl.refine[FCOMP reluctant_c_triggered, unfolded reluctant_assn_def[symmetric]] reluctant_u_impl.refine[FCOMP reluctant_c_u, unfolded reluctant_assn_def[symmetric]] reluctant_v_impl.refine[FCOMP reluctant_c_v, unfolded reluctant_assn_def[symmetric]] reluctant_wait_impl.refine[FCOMP reluctant_c_wait, unfolded reluctant_assn_def[symmetric]] reluctant_period_impl.refine[FCOMP reluctant_c_period, unfolded reluctant_assn_def[symmetric]] reluctant_limit_impl.refine[FCOMP reluctant_c_limit, unfolded reluctant_assn_def[symmetric]] sepref_register reluctant_impl reluctant_tick reluctant_enable reluctant_set_trigger reluctant_triggered reluctant_untrigger reluctant_triggered2 reluctant_init reluctant_disable lemma reluctant_tick_alt_def: ‹RETURN o reluctant_tick = (λr. let limited = reluctant_limited r; trigger = reluctant_trigger r; u = reluctant_u r; v = reluctant_v r; period = reluctant_period r; wait = reluctant_wait r; limit = reluctant_limit r in (if period = 0 ∨ trigger then RETURN (Reluctant limited trigger u v period (wait) limit) else if wait > 1 then RETURN (Reluctant limited trigger u v period (wait - 1) limit) else let zero = u-u; b = u AND (zero - u); (u, v) = (if b = v then (u+1, 1) else (u, 2 * v)); (u, v) = (if limited ∧ wait > limit then (1,1) else (u, v)); wait = v * period in RETURN (Reluctant limited True u v period wait limit)))› by (auto intro!: ext simp: reluctant_tick_def Let_def) sepref_register ‹(AND) :: 'a :: len word ⇒ _ ⇒ _› sepref_def reluctant_tick_impl is ‹RETURN o reluctant_tick› :: ‹reluctant_assn^k →_a reluctant_assn› unfolding reluctant_tick_alt_def by sepref export_llvm reluctant_tick_impl sepref_def reluctant_enable_impl is ‹uncurry (RETURN oo reluctant_enable)› :: ‹word_assn^k *_a word_assn^k →_a reluctant_assn› unfolding reluctant_enable_def by sepref sepref_def reluctant_set_trigger_impl is ‹uncurry (RETURN oo reluctant_set_trigger)› :: ‹bool1_assn^k *_a reluctant_assn^k →_a reluctant_assn› unfolding reluctant_set_trigger_def by sepref sepref_def reluctant_triggered_ether_impl is ‹(RETURN o reluctant_triggered)› :: ‹reluctant_assn^k →_a reluctant_assn ×_a bool1_assn› unfolding reluctant_triggered_def by sepref sepref_def reluctant_triggered2_impl is ‹(RETURN o reluctant_triggered2)› :: ‹reluctant_assn^k →_a bool1_assn› unfolding reluctant_triggered2_def by sepref sepref_def reluctant_untrigger_impl is ‹(RETURN o reluctant_untrigger)› :: ‹reluctant_assn^k →_a reluctant_assn› unfolding reluctant_untrigger_def by sepref sepref_def reluctant_disable_impl is ‹RETURN o reluctant_disable› :: ‹reluctant_assn^k →_a reluctant_assn› unfolding reluctant_disable_def by sepref sepref_def reluctant_init_impl is ‹uncurry0 (RETURN reluctant_init)› :: ‹unit_assn^k →_a reluctant_assn› unfolding reluctant_init_def apply (annot_snat_const ‹TYPE(64)›) by sepref experiment begin export_llvm reluctant_init_impl reluctant_enable_impl reluctant_disable_impl reluctant_triggered2_impl reluctant_triggered_impl reluctant_set_trigger_impl reluctant_enable_impl reluctant_triggered_ether_impl export_llvm reluctant_tick_impl end end

Theory IsaSAT_Reluctant_LLVM