Theory IsaSAT_Options

theory IsaSAT_Options_LLVM imports IsaSAT_Options IsaSAT_Literals_LLVM begin type_synonym opts_assn = ‹1 word × 1 word × 1 word × 64 word × 64 word × 64 word × 3 word × 64 word × 64 word × 64 word × 1 word› definition opts_rel_assn :: ‹opts_ref ⇒ _ ⇒ assn› where ‹opts_rel_assn = bool1_assn ×_a bool1_assn ×_a bool1_assn ×_a word_assn ×_a word_assn ×_a snat_assn' TYPE(64) ×_a word_assn' TYPE(3) ×_a word64_assn ×_a word64_assn ×_a word64_assn ×_a bool1_assn› sepref_def opts_rel_restart_code is ‹RETURN o opts_rel_restart› :: ‹opts_rel_assn^k →_a bool1_assn› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref sepref_def opts_rel_reduce_code is ‹RETURN o opts_rel_reduce› :: ‹opts_rel_assn^k →_a bool1_assn› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref sepref_def opts_rel_unbounded_mode_code is ‹RETURN o opts_rel_unbounded_mode› :: ‹opts_rel_assn^k →_a bool1_assn› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref sepref_def opts_rel_miminum_between_restart_code is ‹RETURN o opts_rel_miminum_between_restart› :: ‹opts_rel_assn^k →_a word_assn› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref sepref_def opts_rel_restart_coeff1_code is ‹RETURN o opts_rel_restart_coeff1› :: ‹opts_rel_assn^k →_a word_assn› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref sepref_def opts_rel_restart_coeff2_code is ‹RETURN o opts_rel_restart_coeff2› :: ‹opts_rel_assn^k →_a snat_assn' TYPE(64)› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref sepref_def opts_rel_target_code is ‹RETURN o opts_rel_target› :: ‹opts_rel_assn^k →_a word_assn' TYPE(3)› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref sepref_def opts_rel_fema_code is ‹RETURN o opts_rel_fema› :: ‹opts_rel_assn^k →_a word64_assn› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref sepref_def opts_rel_sema_code is ‹RETURN o opts_rel_sema› :: ‹opts_rel_assn^k →_a word64_assn› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref sepref_def opts_rel_GC_units_lim_code is ‹RETURN o opts_rel_GC_units_lim› :: ‹opts_rel_assn^k →_a word64_assn› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref sepref_def opts_rel_subsumption_code is ‹RETURN o opts_rel_subsumption› :: ‹opts_rel_assn^k →_a bool1_assn› unfolding opts_rel_alt_defs opts_rel_assn_def by sepref definition opts_assn :: ‹opts ⇒ opts_assn ⇒ assn› where ‹opts_assn = hr_comp opts_rel_assn opts_rel› lemmas opts_refine[sepref_fr_rules] = opts_rel_restart_code.refine[FCOMP opts_rel_restart, unfolded opts_assn_def[symmetric]] opts_rel_reduce_code.refine[FCOMP opts_rel_reduce, unfolded opts_assn_def[symmetric]] opts_rel_unbounded_mode_code.refine[FCOMP opts_rel_unbounded_mode, unfolded opts_assn_def[symmetric]] opts_rel_miminum_between_restart_code.refine[FCOMP opts_rel_miminum_between_restart, unfolded opts_assn_def[symmetric]] opts_rel_restart_coeff1_code.refine[FCOMP opts_rel_restart_coeff1, unfolded opts_assn_def[symmetric]] opts_rel_restart_coeff2_code.refine[FCOMP opts_rel_restart_coeff2, unfolded opts_assn_def[symmetric]] opts_rel_target_code.refine[FCOMP opts_rel_target, unfolded opts_assn_def[symmetric]] opts_rel_fema_code.refine[FCOMP opts_rel_fema, unfolded opts_assn_def[symmetric]] opts_rel_sema_code.refine[FCOMP opts_rel_sema, unfolded opts_assn_def[symmetric]] opts_rel_GC_units_lim_code.refine[FCOMP opts_GC_units_lim, unfolded opts_assn_def[symmetric]] opts_rel_subsumption_code.refine[FCOMP opts_subsumption, unfolded opts_assn_def[symmetric]] sepref_register opts_restart opts_reduce opts_minimum_between_restart opts_restart_coeff1 opts_restart_coeff2 opts_target opts_fema opts_sema opts_subsumption lemma opts_assn_assn_pure[safe_constraint_rules]: ‹CONSTRAINT is_pure opts_assn› unfolding opts_assn_def opts_rel_assn_def by solve_constraint lemmas [sepref_frame_free_rules] = mk_free_is_pure[OF opts_assn_assn_pure[unfolded CONSTRAINT_def]] definition default_opts :: opts where ‹default_opts = IsaOptions True True True 50 11 4 1 128849010 429450 15 True› definition default_opts2 :: opts_ref where ‹default_opts2 = (True, True, True, 50, 11, 4, 2, 128849010, 429450, 15, True)› definition IsaOptions_rel :: ‹bool ⇒ bool ⇒ bool ⇒ 64 word ⇒ 64 word ⇒ nat ⇒ opts_target ⇒ 64 word ⇒ 64 word ⇒ 64 word ⇒ bool ⇒ opts_ref› where ‹IsaOptions_rel a b c d e f g h i j k = (a, b, c, d, e, f, g, h, i, j, k)› lemma IsaOptions_rel: ‹(uncurry10 (RETURN o₁₁ IsaOptions_rel), uncurry10 (RETURN o₁₁ IsaOptions)) ∈ bool_rel ×_f bool_rel ×_f bool_rel ×_f word_rel ×_f word_rel ×_f nat_rel ×_f word_rel ×_f word_rel ×_f word_rel ×_f word_rel ×_f bool_rel → ⟨opts_rel⟩nres_rel› by (auto intro!: frefI nres_relI simp: opts_rel_def IsaOptions_rel_def) sepref_def IsaOptions_rel_impl is ‹uncurry10 (RETURN o₁₁ IsaOptions_rel)› :: ‹bool1_assn^k *_a bool1_assn^k *_a bool1_assn^k *_a word_assn^k *_a word_assn^k *_a (snat_assn' (TYPE(64)))^k *_a (word_assn' (TYPE(3)))^k *_a word_assn^k *_a word_assn^k *_a word_assn^k *_a bool1_assn^k →_a opts_rel_assn› unfolding IsaOptions_rel_def opts_rel_assn_def by sepref sepref_register IsaOptions lemmas [sepref_fr_rules] = IsaOptions_rel_impl.refine[FCOMP IsaOptions_rel, unfolded opts_assn_def[symmetric]] lemma [sepref_import_param]: ‹(0, TARGET_NEVER) ∈ word_rel› ‹(1, TARGET_STABLE_ONLY) ∈ word_rel› ‹(2, TARGET_ALWAYS) ∈ word_rel› by (auto simp: TARGET_NEVER_def TARGET_ALWAYS_def TARGET_STABLE_ONLY_def) experiment begin export_llvm opts_rel_restart_code opts_rel_reduce_code end end

Theory IsaSAT_Options_LLVM