Theory IsaSAT_Simplify_Pure_Literals

theory IsaSAT_Simplify_Pure_Literals_LLVM imports IsaSAT_Restart_Defs IsaSAT_Simplify_Pure_Literals_Defs IsaSAT_Setup_LLVM IsaSAT_Trail_LLVM IsaSAT_Proofs_LLVM begin sepref_register mop_arena_status_st isa_pure_literal_count_occs_clause_wl sepref_def isa_pure_literal_count_occs_clause_wl_code is ‹uncurry3 isa_pure_literal_count_occs_clause_wl› :: ‹[λ(((C, S), _), _). length (get_clauses_wl_heur S) ≤ snat64_max ∧ learned_clss_count S ≤ unat64_max]_a sint64_nat_assn^k *_a isasat_bounded_assn^k *_a (larray_assn' TYPE(64) bool1_assn)^d *_a word64_assn^d → larray_assn' TYPE(64) bool1_assn ×_a word64_assn› unfolding isa_pure_literal_count_occs_clause_wl_def apply (annot_snat_const ‹TYPE(64)›) by sepref sepref_register isa_pure_literal_count_occs_wl sepref_def isa_pure_literal_count_occs_wl_code is isa_pure_literal_count_occs_wl :: ‹[λS. length (get_clauses_wl_heur S) ≤ snat64_max ∧ learned_clss_count S ≤ unat64_max]_a isasat_bounded_assn^k → bool1_assn ×_a larray_assn' TYPE(64) bool1_assn› unfolding isa_pure_literal_count_occs_wl_def nth_append Let_def larray_fold_custom_replicate mop_arena_status_st_def[symmetric] access_ivdom_at_def[symmetric] length_avdom_def[symmetric] length_ivdom_def[symmetric] access_avdom_at_def[symmetric] length_watchlist_raw_def[symmetric] length_append supply of_nat_snat[sepref_import_param] apply (annot_snat_const ‹TYPE(64)›) by sepref lemma isa_propagate_pure_bt_wl_alt_def: ‹isa_propagate_pure_bt_wl = (λL S. do { let (M, S) = extract_trail_wl_heur S; let (stats, S) = extract_stats_wl_heur S; ASSERT(0 ≠ DECISION_REASON); ASSERT(cons_trail_Propagated_tr_pre ((L, 0::nat), M)); M ← cons_trail_Propagated_tr (L) 0 M; let stats = incr_units_since_last_GC (incr_uset (incr_purelit_elim stats)); let S = update_stats_wl_heur stats S; let S = update_trail_wl_heur M S; let _ = log_unit_clause L; RETURN S})› unfolding isa_propagate_pure_bt_wl_def log_unit_clause_def by (auto simp: empty_US_heur_def state_extractors Let_def intro!: ext split: isasat_int_splits) sepref_register isa_propagate_pure_bt_wl cons_trail_Propagated_tr sepref_def isa_propagate_pure_bt_wl_code is ‹uncurry isa_propagate_pure_bt_wl› :: ‹unat_lit_assn^k *_a isasat_bounded_assn^d →_a isasat_bounded_assn› unfolding isa_propagate_pure_bt_wl_alt_def apply (annot_snat_const ‹TYPE(64)›) by sepref lemma isa_pure_literal_deletion_wl_alt_def: ‹isa_pure_literal_deletion_wl occs S₀ = (do { ASSERT (isa_pure_literal_deletion_wl_pre S₀); (_, eliminated, S) ← WHILE_T⇗λ(n, _, S). get_vmtf_heur_array S₀ = get_vmtf_heur_array S⇖ (λ(n, x). n ≠ None) (λ(n, eliminated, T). do { ASSERT (n ≠ None); let A = the n; ASSERT (A < length (get_vmtf_heur_array S₀)); ASSERT (A ≤ unat32_max div 2); ASSERT (get_vmtf_heur_array S₀ = get_vmtf_heur_array T); ASSERT (nat_of_lit (Pos A) < length occs); ASSERT (nat_of_lit (Neg A) < length occs); let L = (if occs ! nat_of_lit (Pos A) ∧ ¬ occs ! nat_of_lit (Neg A) then Pos A else Neg A); ASSERT (nat_of_lit (- L) < length occs); val ← mop_polarity_pol (get_trail_wl_heur T) L; if ¬ occs ! nat_of_lit (- L) ∧ val = None then do { S ← isa_propagate_pure_bt_wl L T; ASSERT (get_vmtf_heur_array S₀ = get_vmtf_heur_array S); RETURN (get_next (get_vmtf_heur_array S ! A),eliminated + 1, S) } else RETURN (get_next (get_vmtf_heur_array T ! A),eliminated, T) }) (Some (get_vmtf_heur_fst S₀), 0, S₀); mop_free occs; RETURN (eliminated, S) })› unfolding isa_pure_literal_deletion_wl_def mop_free_def by auto sepref_def isa_pure_literal_deletion_wl_code is ‹uncurry isa_pure_literal_deletion_wl› :: ‹[λ(_, S). length (get_clauses_wl_heur S) ≤ snat64_max ∧ learned_clss_count S ≤ unat64_max]_a (larray_assn' TYPE(64) bool1_assn)^d *_a isasat_bounded_assn^d → word64_assn ×_a isasat_bounded_assn› unfolding isa_pure_literal_deletion_wl_alt_def nres_monad3 nres_monad2 get_bump_heur_array_nth_def[symmetric] UNSET_def[symmetric] atom.fold_option mop_polarity_st_heur_def[symmetric] tri_bool_eq_def[symmetric] get_bump_heur_array_nth_def[symmetric] prod.simps get_vmtf_heur_array_def[symmetric] by sepref end

Theory IsaSAT_Simplify_Pure_Literals_LLVM