Theory IsaSAT

theory IsaSAT_LLVM imports IsaSAT_Print_LLVM IsaSAT_CDCL_LLVM IsaSAT_Initialisation_LLVM IsaSAT_Restart_Simp_LLVM Version IsaSAT_Defs begin hide_const (open)array_assn hide_const (open)IICF_Multiset.mset_rel hide_const (open) NEMonad.ASSERT NEMonad.RETURN lemma convert_state_hnr: ‹(uncurry (Mreturn oo (λ_ S. S)), uncurry (RETURN oo convert_state)) ∈ ghost_assn^k *_a (isasat_init_assn)^d →_a isasat_init_assn› unfolding convert_state_def by sepref_to_hoare vcg declare convert_state_hnr[sepref_fr_rules] chapter ‹Code of Full IsaSAT› abbreviation model_stat_assn where ‹model_stat_assn ≡ bool1_assn ×_a (arl64_assn unat_lit_assn) ×_a isasat_stats_assn› abbreviation model_stat_assn₀ :: ‹bool × nat literal list × isasat_stats ⇒ 1 word × (64 word × 64 word × 32 word ptr) × _ ⇒ llvm_amemory ⇒ bool› where ‹model_stat_assn₀ ≡ bool1_assn ×_a (al_assn unat_lit_assn) ×_a isasat_stats_assn› abbreviation lits_with_max_assn :: ‹nat multiset ⇒ (64 word × 64 word × 32 word ptr) × 32 word ⇒ llvm_amemory ⇒ bool› where ‹lits_with_max_assn ≡ hr_comp (arl64_assn atom_assn ×_a uint32_nat_assn) lits_with_max_rel› abbreviation lits_with_max_assn₀ :: ‹nat multiset ⇒ (64 word × 64 word × 32 word ptr) × 32 word ⇒ llvm_amemory ⇒ bool› where ‹lits_with_max_assn₀ ≡ hr_comp (al_assn atom_assn ×_a unat32_assn) lits_with_max_rel› lemma lits_with_max_assn_alt_def: ‹lits_with_max_assn = hr_comp (arl64_assn atom_assn ×_a uint32_nat_assn) (lits_with_max_rel O ⟨nat_rel⟩IICF_Multiset.mset_rel)› proof - have 1: ‹(lits_with_max_rel O ⟨nat_rel⟩IICF_Multiset.mset_rel) = lits_with_max_rel› by (auto simp: mset_rel_def p2rel_def rel2p_def[abs_def] br_def rel_mset_def lits_with_max_rel_def list_rel_def list_all2_op_eq_map_right_iff' list.rel_eq) show ?thesis unfolding 1 by auto qed lemma tuple15_rel_Id: ‹(⟨Id, Id, Id, nat_rel, ⟨⟨Id⟩list_rel⟩list_rel, Id, ⟨bool_rel⟩list_rel,nat_rel, Id, Id, Id, Id, Id, Id, Id⟩tuple15_rel) = Id› apply (standard; standard) apply (case_tac x) apply (auto simp: hr_comp_def[abs_def] tuple15_rel_def split: tuple15.splits) done lemma init_state_wl_D'_code_isasat: ‹hr_comp isasat_init_assn (⟨Id, Id, Id, nat_rel, ⟨⟨Id⟩list_rel⟩list_rel, Id, ⟨bool_rel⟩list_rel,nat_rel, Id, Id, Id, Id, Id, Id, Id⟩tuple15_rel) = isasat_init_assn› unfolding tuple15_rel_Id by (auto simp: split: tuple15.splits) definition split_trail where ‹split_trail x =x› sepref_def split_trail_impl is ‹RETURN o split_trail› :: ‹trail_pol_fast_assn^d →_a arl64_assn unat_lit_assn ×_a larray64_assn (tri_bool_assn) ×_a larray64_assn uint32_nat_assn ×_a larray64_assn sint64_nat_assn ×_a uint32_nat_assn ×_a arl64_assn uint32_nat_assn ×_a sint64_nat_assn› unfolding trail_pol_fast_assn_def split_trail_def by sepref lemma extract_model_of_state_stat_alt_def: ‹RETURN o extract_model_of_state_stat = (λS. case S of Tuple17 MM' N' D' j W' vm clvls cach lbd outl stats heur vdom lcount opts old_arena occs ⇒ do {_ ← print_trail2 (MM'); (M,M') ← RETURN (split_trail MM'); mop_free M'; mop_free N'; mop_free D'; mop_free j; mop_free W'; mop_free vm; mop_free clvls; mop_free cach; mop_free lbd; mop_free outl; mop_free heur; mop_free vdom; mop_free opts; mop_free old_arena; mop_free lcount; mop_free occs; RETURN (False, M, stats) })› by (auto simp: extract_model_of_state_stat_def mop_free_def print_trail2_def split_trail_def intro!: ext split: isasat_int_splits) schematic_goal mk_free_lbd_assn[sepref_frame_free_rules]: ‹MK_FREE aivdom_assn ?fr› unfolding aivdom_assn_def code_hider_assn_def by synthesize_free+ sepref_def extract_model_of_state_stat is ‹RETURN o extract_model_of_state_stat› :: ‹isasat_bounded_assn^d →_a model_stat_assn› supply [[goals_limit=1]] unfolding extract_model_of_state_stat_alt_def trail_pol_fast_assn_def by sepref lemma extract_state_stat_alt_def: ‹RETURN o extract_state_stat = (λS. case S of Tuple17 M N' D' j W' vm clvls cach lbd outl stats heur vdom lcount opts old_arena occs ⇒ do { mop_free M; mop_free N'; mop_free D'; mop_free j; mop_free W'; mop_free vm; mop_free clvls; mop_free cach; mop_free lbd; mop_free outl; mop_free heur; mop_free vdom; mop_free opts; mop_free old_arena; mop_free lcount; mop_free occs; RETURN (True, [], stats)})› by (auto simp: extract_state_stat_def mop_free_def split: isasat_int_splits intro!: ext) sepref_def extract_state_stat is ‹RETURN o extract_state_stat› :: ‹isasat_bounded_assn^d →_a model_stat_assn› supply [[goals_limit=1]] unfolding extract_state_stat_alt_def isasat_bounded_assn_def al_fold_custom_empty[where 'l=64] by sepref sepref_def empty_conflict_code' is ‹uncurry0 (empty_conflict_code)› :: ‹unit_assn^k →_a model_stat_assn› unfolding empty_conflict_code_def apply (rewrite in ‹let _ = ⌑ in _› al_fold_custom_empty[where 'l=64]) apply (rewrite in ‹let _ = ⌑ in _› annotate_assn[where A=‹arl64_assn unat_lit_assn›]) by sepref declare empty_conflict_code'.refine[sepref_fr_rules] sepref_def empty_init_code' is ‹uncurry0 (RETURN empty_init_code)› :: ‹unit_assn^k →_a model_stat_assn› unfolding empty_init_code_def al_fold_custom_empty[where 'l=64] apply (rewrite in ‹RETURN (_, ⌑,_)› annotate_assn[where A=‹arl64_assn unat_lit_assn›]) by sepref sepref_register init_dt_wl_heur_full sepref_register to_init_state from_init_state get_conflict_wl_is_None_init init_dt_wl_heur sepref_def isasat_fast_bound_impl is ‹uncurry0 (RETURN isasat_fast_bound)› :: ‹unit_assn^k →_a sint64_nat_assn› unfolding isasat_fast_bound_alt_def apply (annot_snat_const ‹TYPE(64)›) by sepref lemma isasat_fast_init_alt_def: ‹RETURN o isasat_fast_init = (λS. do{ let n = length (get_clauses_wl_heur_init S); let lcountUE = clss_size_lcountUE (get_learned_count_init S); let lcount = clss_size_lcount (get_learned_count_init S); let lcountUEk = clss_size_lcountUEk (get_learned_count_init S); let lcountUS = clss_size_lcountUS (get_learned_count_init S); let lcountU0 = clss_size_lcountU0 (get_learned_count_init S); ASSERT(18446744073709551615 ∈ unats LENGTH(64)); c ← RETURN 18446744073709551615; if ¬(n ≤ isasat_fast_bound ∧ lcount < c - lcountUE) then RETURN False else do { ASSERT(lcount + lcountUE ∈ unats LENGTH(64)); a ← RETURN (lcount + lcountUE); if ¬a < c - lcountUS then RETURN False else do { ASSERT(a + lcountUS ∈ unats LENGTH(64)); a ← RETURN (a + lcountUS); if ¬a < c - lcountU0 then RETURN False else do { ASSERT(a + lcountU0 ∈ unats LENGTH(64)); a ← RETURN (a + lcountU0); if ¬a < c - lcountUEk then RETURN False else do { ASSERT(a + lcountUEk ∈ unats LENGTH(64)); a ← RETURN (a + lcountUEk); RETURN(a < c) } } } }})› by (auto simp: isasat_fast_init_def unat64_max_def unat32_max_def isasat_fast_bound_def max_uint_def clss_size_lcountUS_def clss_size_lcountUE_def clss_size_lcount_def learned_clss_count_init_def unats_def clss_size_lcountU0_def clss_size_lcountUEk_def Let_def bind_ASSERT_eq_if split: if_splits intro!: ASSERT_leI intro!: ext) lemma isasat_fast_init_codeI: ‹(aa :: 64 word, b) ∈ unat_rel64 ⟹ b ≤ 18446744073709551615› using unat_lt_max_unat[of aa] by (auto simp: unat_rel_def unat.rel_def br_def max_unat_def) sepref_def isasat_fast_init_code is ‹RETURN o isasat_fast_init› :: ‹isasat_init_assn^k →_a bool1_assn› supply [[goals_limit=1]] supply [sepref_bounds_simps del] = max_snat_def max_unat_def max_sint_def min_sint_def supply [intro] = isasat_fast_init_codeI unfolding isasat_fast_init_alt_def if_not_swap isasat_fast_init_def clss_size_lcountUS_st_init_def[symmetric] clss_size_lcountUEk_st_init_def[symmetric] clss_size_lcountUE_st_init_def[symmetric] full_arena_length_st_init_def[symmetric] clss_size_lcount_st_init_def[symmetric] clss_size_lcountU0_st_init_def[symmetric] apply (rewrite at ‹RETURN ⌑› unat_const_fold[where 'a=64]) by sepref sepref_register cdcl_twl_stgy_restart_prog_wl_heur declare init_state_wl_D'_code.refine[FCOMP init_state_wl_D', unfolded lits_with_max_assn_alt_def[symmetric] init_state_wl_heur_fast_def[symmetric], unfolded init_state_wl_D'_code_isasat, sepref_fr_rules] lemma [sepref_fr_rules]: ‹(init_state_wl_D'_code, init_state_wl_heur_fast) ∈ [λx. distinct_mset x ∧ (∀L∈#ℒ_a_l_l x. nat_of_lit L ≤ unat32_max)]_a lits_with_max_assn^k → isasat_init_assn› using init_state_wl_D'_code.refine[FCOMP init_state_wl_D'] unfolding lits_with_max_assn_alt_def[symmetric] init_state_wl_D'_code_isasat init_state_wl_heur_fast_def by auto definition ghost_assn where ‹ghost_assn = hr_comp unit_assn virtual_copy_rel› lemma [sepref_fr_rules]: ‹(Mreturn o (λ_. ()), RETURN o virtual_copy) ∈ lits_with_max_assn^k →_a ghost_assn› proof - have [simp]: ‹(λs. (∃xa. (↑(xa = x)) s)) = (↑True)› for s :: ‹'b::sep_algebra› and x :: 'a by (auto simp: pred_lift_extract_simps) show ?thesis unfolding virtual_copy_def ghost_assn_def virtual_copy_rel_def apply sepref_to_hoare apply vcg' apply (auto simp: ENTAILS_def hr_comp_def snat_rel_def pure_true_conv) apply (rule Defer_Slot.remove_slot) done qed sepref_register virtual_copy empty_conflict_code empty_init_code isasat_fast_init is_failed_heur_init extract_model_of_state_stat extract_state_stat isasat_information_banner finalise_init_code IsaSAT_Initialisation.rewatch_heur_st_fast get_conflict_wl_is_None_heur cdcl_twl_stgy_prog_bounded_wl_heur get_conflict_wl_is_None_heur_init convert_state lemma isasat_information_banner_alt_def: ‹isasat_information_banner S = RETURN (())› by (auto simp: isasat_information_banner_def) schematic_goal mk_free_ghost_assn[sepref_frame_free_rules]: ‹MK_FREE ghost_assn ?fr› unfolding ghost_assn_def by synthesize_free lemma IsaSAT_bounded_heur_alt_def: ‹IsaSAT_bounded_heur opts CS = do{ _ ← RETURN (IsaSAT_Profile.start_initialisation); ASSERT(isasat_input_bounded (mset_set (extract_atms_clss CS {}))); ASSERT(∀C∈set CS. ∀L∈set C. nat_of_lit L ≤ unat32_max); let 𝒜_i_n' = mset_set (extract_atms_clss CS {}); ASSERT(isasat_input_bounded 𝒜_i_n'); ASSERT(distinct_mset 𝒜_i_n'); let 𝒜_i_n'' = virtual_copy 𝒜_i_n'; let b = opts_unbounded_mode opts; S ← init_state_wl_heur_fast 𝒜_i_n'; (T::twl_st_wl_heur_init) ← init_dt_wl_heur_b CS S; let T = convert_state 𝒜_i_n'' T; _ ← RETURN (IsaSAT_Profile.stop_initialisation); if isasat_fast_init T ∧ ¬is_failed_heur_init T then do { if ¬get_conflict_wl_is_None_heur_init T then RETURN (False, empty_init_code) else if CS = [] then do {mop_free CS; stat ← empty_conflict_code; RETURN (False, stat)} else do { _ ← RETURN (IsaSAT_Profile.start_initialisation); mop_free CS; ASSERT(𝒜_i_n'' ≠ {#}); ASSERT(isasat_input_bounded_nempty 𝒜_i_n''); _ ← isasat_information_banner T; ASSERT(rewatch_heur_st_fast_pre T); T ← rewatch_heur_st_init T; ASSERT(isasat_fast_init T); T ← finalise_init_code opts (T::twl_st_wl_heur_init); _ ← RETURN (IsaSAT_Profile.stop_initialisation); ASSERT(isasat_fast T); (b, U) ← cdcl_twl_stgy_restart_prog_bounded_wl_heur T; RETURN (b, if ¬b ∧ get_conflict_wl_is_None_heur U then IsaSAT_Defs.extract_model_of_state_stat U else IsaSAT_Defs.extract_state_stat U) } } else do {mop_free CS; RETURN (True, empty_init_code)} }› unfolding mop_free_def by (auto simp: IsaSAT_bounded_heur_def cong: if_cong) sepref_def IsaSAT_code is ‹uncurry IsaSAT_bounded_heur› :: ‹opts_assn^d *_a (clauses_ll_assn)^d →_a bool1_assn ×_a model_stat_assn› supply [[goals_limit=1]] isasat_fast_init_def[simp] unfolding IsaSAT_bounded_heur_alt_def empty_conflict_def[symmetric] get_conflict_wl_is_None (*extract_model_of_state_def[symmetric]*) (*extract_stats_def[symmetric]*) init_dt_wl_heur_b_def[symmetric] (*length_get_clauses_wl_heur_init_def[symmetric]*) init_dt_step_wl_heur_unb_def[symmetric] init_dt_wl_heur_unb_def[symmetric] length_0_conv[symmetric] op_list_list_len_def[symmetric] isasat_information_banner_alt_def supply get_conflict_wl_is_None_heur_init_def[simp] supply get_conflict_wl_is_None_def[simp] option.splits[split] (* extract_stats_def[simp del]*) apply (rewrite at ‹extract_atms_clss _ ⌑› op_extract_list_empty_def[symmetric]) apply (rewrite at ‹extract_atms_clss _ ⌑› op_extract_list_empty_def[symmetric]) apply (annot_snat_const ‹TYPE(64)›) by sepref sepref_register print_forward_rounds print_forward_subsumed print_forward_strengthened abbreviation (input) C_bool_to_bool :: ‹8 word ⇒ bool› where ‹C_bool_to_bool g ≡ g ≠ 0› definition IsaSAT_bounded_heur_wrapper :: ‹8 word ⇒ 8 word ⇒ 8 word ⇒ 64 word ⇒ 64 word ⇒ nat ⇒ 8 word ⇒ 64 word ⇒ 64 word ⇒ 64 word ⇒ 8 word ⇒ _ ⇒ (nat) nres›where ‹IsaSAT_bounded_heur_wrapper red res unbdd mini res1 res2 target_option fema sema units subsume C = do { let opts = IsaOptions (C_bool_to_bool red) (C_bool_to_bool res) (C_bool_to_bool unbdd) mini res1 res2 (if target_option = 2 then TARGET_ALWAYS else if target_option = 0 then TARGET_NEVER else TARGET_STABLE_ONLY) fema sema units (C_bool_to_bool subsume); (b, (b', _, stats)) ← IsaSAT_bounded_heur (opts) C; let (_ :: unit) = print_propa (stats_propagations stats); let (_ :: unit) = print_confl (stats_conflicts stats); let (_ :: unit) = print_dec (stats_decisions stats); let (_ :: unit) = print_res (stats_restarts stats) (stats_conflicts stats); let (_ :: unit) = print_lres (stats_reductions stats) (stats_conflicts stats); let (_ :: unit) = print_uset (stats_fixed stats); let (_ :: unit) = print_gcs (stats_gcs stats) (stats_conflicts stats); let (_ :: unit) = print_irred_clss (stats_irred stats); let (_ :: unit) = print_binary_unit (stats_binary_units stats); let (_ :: unit) = print_binary_red_removed (stats_binary_removed stats); let (_ :: unit) = print_purelit_elim (stats_pure_lits_removed stats); let (_ :: unit) = print_purelit_rounds (stats_pure_lits_rounds stats) (stats_conflicts stats); let (_ :: unit) = print_forward_rounds (stats_forward_rounds stats) (stats_conflicts stats); let (_ :: unit) = print_forward_tried (stats_forward_tried stats) (stats_forward_rounds stats); let (_ :: unit) = print_forward_subsumed (stats_forward_subsumed stats) (stats_forward_tried stats); let (_ :: unit) = print_forward_strengthened (stats_forward_strengthened stats) (stats_forward_tried stats); let (_ :: unit) = print_rephased (stats_rephase stats) (stats_conflicts stats); RETURN ((if b then 2 else 0) + (if b' then 1 else 0)) }› text ‹ The calling convention of LLVM and clang is not the same, so returning the model is currently unsupported. We return only the flags (as ints, not as bools) and the statistics. › sepref_register IsaSAT_bounded_heur default_opts abbreviation bool_C_assn where ‹bool_C_assn ≡ (word_assn' (TYPE(8)))› sepref_def IsaSAT_wrapped is ‹uncurry11 IsaSAT_bounded_heur_wrapper› :: ‹bool_C_assn^k *_a bool_C_assn^k *_a bool_C_assn^k *_a word64_assn^k *_a word64_assn^k *_a (snat_assn' (TYPE(64)))^k *_a bool_C_assn^k *_a word64_assn^k *_a word64_assn^k *_a word64_assn^k *_a bool_C_assn^k *_a (clauses_ll_assn)^d →_a sint64_nat_assn› supply [[goals_limit=1]] if_splits[split] unfolding IsaSAT_bounded_heur_wrapper_def apply (annot_snat_const ‹TYPE(64)›) by sepref text ‹The setup to transmit the version is a bit complicated, because Isabelle does not support direct export of string literals. Therefore, we actually convert the version to an array chars (more precisely, of machine words -- ended with 0) that can be read and printed by the C layer. Note the conversion must be automatic, because the version depends on the underlying git repository, hence the call to auto. › function array_of_version where ‹array_of_version i str arr = (if i ≥ length str then arr else array_of_version (i+1) str (arr[i := str ! i]))› by pat_completeness auto termination apply (relation ‹measure (λ(i,str, arr). length str - i)›) apply auto done text ‹Using this as version number makes our work on the cluster easier and makes the version checking slightly easier (because the git hash is never up-to-date).› definition internal_version :: ‹string› where ‹internal_version = ''0i''› sepref_definition llvm_version is ‹uncurry0 (RETURN ( let str = map (nat_of_integer o (of_char :: _ ⇒ integer)) (internal_version @ ''-'' @ String.explode Version.version) @ [0] in array_of_version 0 str (replicate (length str) 0)))› :: ‹unit_assn^k →_a IICF_Array.array_assn sint32_nat_assn› supply[[goals_limit=1]] unfolding Version.version_def String.explode_code internal_version_def String.asciis_of_Literal apply (simp add: String.asciis_of_Literal of_char_of char_of_char nat_of_integer_def del: list_update.simps replicate.simps) apply (annot_snat_const ‹TYPE(32)›) unfolding array_fold_custom_replicate unfolding hf_pres.simps[symmetric] by sepref experiment begin lemmas [llvm_code] = llvm_version_def lemmas [llvm_inline] = unit_propagation_inner_loop_body_wl_fast_heur_code_def FOCUSED_MODE_def DEFAULT_INIT_PHASE_def STABLE_MODE_def find_unwatched_wl_st_heur_fast_code_def update_clause_wl_fast_code_def lemmas [unfolded inline_direct_return_node_case, llvm_code] = units_since_last_GC_st_code_def[unfolded read_all_st_code_def] lemmas [llvm_code del] = units_since_last_GC_st_code_def export_llvm llvm_version is ‹STRING_VERSION llvm_version()› IsaSAT_code IsaSAT_wrapped (*is ‹int64_t IsaSAT_wrapped(CBOOL, CBOOL, CBOOL, int64_t, int64_t, int64_t, CBOOL, int64_t, int64_t, int64_t, CLAUSES)›*) IsaSAT_Profile_PROPAGATE is ‹PROFILE_CST IsaSAT_Profile_PROPAGATE()› IsaSAT_Profile_REDUCE is ‹PROFILE_CST IsaSAT_Profile_REDUCE()› IsaSAT_Profile_GC is ‹PROFILE_CST IsaSAT_Profile_GC()› IsaSAT_Profile_ANALYZE is ‹PROFILE_CST IsaSAT_Profile_ANALYZE()› IsaSAT_Profile_MINIMIZATION is ‹PROFILE_CST IsaSAT_Profile_MINIMIZATION()› IsaSAT_Profile_INITIALISATION is ‹PROFILE_CST IsaSAT_Profile_INITIALISATION()› IsaSAT_Profile_SUBSUMPTION is ‹PROFILE_CST IsaSAT_Profile_SUBSUMPTION()› IsaSAT_Profile_PURE_LITERAL is ‹PROFILE_CST IsaSAT_Profile_PURE_LITERAL()› IsaSAT_Profile_BINARY_SIMP is ‹PROFILE_CST IsaSAT_Profile_BINARY_SIMP()› defines ‹ typedef int8_t CBOOL; typedef int8_t PROFILE_CST; typedef struct {int64_t size; struct {int64_t used; uint32_t *clause;};} CLAUSE; typedef struct {int64_t num_clauses; CLAUSE *clauses;} CLAUSES; typedef int32_t* STRING_VERSION; › file ‹code/src/isasat_restart.ll› end end

Theory IsaSAT_LLVM