theory IsaSAT_Setup
imports
Watched_Literals_VMTF
Watched_Literals.Watched_Literals_Watch_List_Initialisation
IsaSAT_Lookup_Conflict
IsaSAT_Clauses IsaSAT_Arena IsaSAT_Watch_List LBD
begin
chapter ‹Complete state›
text ‹We here define the last step of our refinement: the step with all the heuristics and fully
deterministic code.
After the result of benchmarking, we concluded that the use of \<^typ>‹nat› leads to worse performance
than using ‹sint64›. As, however, the later is not complete, we do so with a switch: as long
as it fits, we use the faster (called 'bounded') version. After that we switch to the 'unbounded'
version (which is still bounded by memory anyhow) if we generate Standard ML code.
We have successfully killed all natural numbers when generating LLVM. However, the LLVM binding
does not have a binding to GMP integers.
›
section ‹Statistics›
text ‹
We do some statistics on the run.
NB: the statistics are not proven correct (especially they might
overflow), there are just there to look for regressions, do some comparisons (e.g., to conclude that
we are propagating slower than the other solvers), or to test different option combination.
›
type_synonym stats = ‹64 word × 64 word × 64 word × 64 word × 64 word × 64 word × 64 word × 64 word›
definition incr_propagation :: ‹stats ⇒ stats› where
‹incr_propagation = (λ(propa, confl, dec). (propa + 1, confl, dec))›
definition incr_conflict :: ‹stats ⇒ stats› where
‹incr_conflict = (λ(propa, confl, dec). (propa, confl + 1, dec))›
definition incr_decision :: ‹stats ⇒ stats› where
‹incr_decision = (λ(propa, confl, dec, res). (propa, confl, dec + 1, res))›
definition incr_restart :: ‹stats ⇒ stats› where
‹incr_restart = (λ(propa, confl, dec, res, lres). (propa, confl, dec, res + 1, lres))›
definition incr_lrestart :: ‹stats ⇒ stats› where
‹incr_lrestart = (λ(propa, confl, dec, res, lres, uset). (propa, confl, dec, res, lres + 1, uset))›
definition incr_uset :: ‹stats ⇒ stats› where
‹incr_uset = (λ(propa, confl, dec, res, lres, (uset, gcs)). (propa, confl, dec, res, lres, uset + 1, gcs))›
definition incr_GC :: ‹stats ⇒ stats› where
‹incr_GC = (λ(propa, confl, dec, res, lres, uset, gcs, lbds). (propa, confl, dec, res, lres, uset, gcs + 1, lbds))›
definition add_lbd :: ‹64 word ⇒ stats ⇒ stats› where
‹add_lbd lbd = (λ(propa, confl, dec, res, lres, uset, gcs, lbds). (propa, confl, dec, res, lres, uset, gcs, lbd + lbds))›
section ‹Moving averages›
text ‹We use (at least hopefully) the variant of EMA-14 implemented in Cadical, but with fixed-point
calculation (\<^term>‹1 :: nat› is \<^term>‹(1 :: nat) >> 32›).
Remark that the coefficient \<^term>‹β› already should not take care of the fixed-point conversion of the glue.
Otherwise, \<^term>‹value› is wrongly updated.
›
type_synonym ema = ‹64 word × 64 word × 64 word × 64 word × 64 word›
definition ema_bitshifting where
‹ema_bitshifting = (1 << 32)›
definition (in -) ema_update :: ‹nat ⇒ ema ⇒ ema› where
‹ema_update = (λlbd (value, α, β, wait, period).
let lbd = (of_nat lbd) * ema_bitshifting in
let value = if lbd > value then value + (β * (lbd - value) >> 32) else value - (β * (value - lbd) >> 32) in
if β ≤ α ∨ wait > 0 then (value, α, β, wait - 1, period)
else
let wait = 2 * period + 1 in
let period = wait in
let β = β >> 1 in
let β = if β ≤ α then α else β in
(value, α, β, wait, period))›
definition (in -) ema_update_ref :: ‹32 word ⇒ ema ⇒ ema› where
‹ema_update_ref = (λlbd (value, α, β, wait, period).
let lbd = ucast lbd * ema_bitshifting in
let value = if lbd > value then value + (β * (lbd - value) >> 32) else value - (β * (value - lbd) >> 32) in
if β ≤ α ∨ wait > 0 then (value, α, β, wait - 1, period)
else
let wait = 2 * period + 1 in
let period = wait in
let β = β >> 1 in
let β = if β ≤ α then α else β in
(value, α, β, wait, period))›
definition (in -) ema_init :: ‹64 word ⇒ ema› where
‹ema_init α = (0, α, ema_bitshifting, 0, 0)›
fun ema_reinit where
‹ema_reinit (value, α, β, wait, period) = (value, α, 1 << 32, 0, 0)›
fun ema_get_value :: ‹ema ⇒ 64 word› where
‹ema_get_value (v, _) = v›
text ‹We use the default values for Cadical: \<^term>‹(3 / 10 ^2)› and \<^term>‹(1 / 10 ^ 5)› in our fixed-point
version.
›
abbreviation ema_fast_init :: ema where
‹ema_fast_init ≡ ema_init (128849010)›
abbreviation ema_slow_init :: ema where
‹ema_slow_init ≡ ema_init 429450›
section ‹Information related to restarts›
definition NORMAL_PHASE :: ‹64 word› where
‹NORMAL_PHASE = 0›
definition QUIET_PHASE :: ‹64 word› where
‹QUIET_PHASE = 1›
definition DEFAULT_INIT_PHASE :: ‹64 word› where
‹DEFAULT_INIT_PHASE = 10000›
type_synonym restart_info = ‹64 word × 64 word × 64 word × 64 word × 64 word›
definition incr_conflict_count_since_last_restart :: ‹restart_info ⇒ restart_info› where
‹incr_conflict_count_since_last_restart = (λ(ccount, ema_lvl, restart_phase, end_of_phase, length_phase).
(ccount + 1, ema_lvl, restart_phase, end_of_phase, length_phase))›
definition restart_info_update_lvl_avg :: ‹32 word ⇒ restart_info ⇒ restart_info› where
‹restart_info_update_lvl_avg = (λlvl (ccount, ema_lvl). (ccount, ema_lvl))›
definition restart_info_init :: ‹restart_info› where
‹restart_info_init = (0, 0, NORMAL_PHASE, DEFAULT_INIT_PHASE, 1000)›
definition restart_info_restart_done :: ‹restart_info ⇒ restart_info› where
‹restart_info_restart_done = (λ(ccount, lvl_avg). (0, lvl_avg))›
section ‹Phase saving›
type_synonym phase_save_heur = ‹phase_saver × nat × phase_saver × nat × phase_saver × 64 word × 64 word × 64 word›
definition phase_save_heur_rel :: ‹nat multiset ⇒ phase_save_heur ⇒ bool› where
‹phase_save_heur_rel 𝒜 = (λ(φ, target_assigned, target, best_assigned, best,
end_of_phase, curr_phase). phase_saving 𝒜 φ ∧
phase_saving 𝒜 target ∧ phase_saving 𝒜 best ∧ length φ = length best ∧
length target = length best)›
definition end_of_rephasing_phase :: ‹phase_save_heur ⇒ 64 word› where
‹end_of_rephasing_phase = (λ(φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase,
length_phase). end_of_phase)›
definition phase_current_rephasing_phase :: ‹phase_save_heur ⇒ 64 word› where
‹phase_current_rephasing_phase =
(λ(φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase, length_phase). curr_phase)›
section ‹Heuristics›
type_synonym restart_heuristics = ‹ema × ema × restart_info × 64 word × phase_save_heur›
fun fast_ema_of :: ‹restart_heuristics ⇒ ema› where
‹fast_ema_of (fast_ema, slow_ema, restart_info, wasted, φ) = fast_ema›
fun slow_ema_of :: ‹restart_heuristics ⇒ ema› where
‹slow_ema_of (fast_ema, slow_ema, restart_info, wasted, φ) = slow_ema›
fun restart_info_of :: ‹restart_heuristics ⇒ restart_info› where
‹restart_info_of (fast_ema, slow_ema, restart_info, wasted, φ) = restart_info›
fun current_restart_phase :: ‹restart_heuristics ⇒ 64 word› where
‹current_restart_phase (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase), wasted, φ) =
restart_phase›
fun incr_restart_phase :: ‹restart_heuristics ⇒ restart_heuristics› where
‹incr_restart_phase (fast_ema, slow_ema, (ccount, ema_lvl, restart_phase, end_of_phase), wasted, φ) =
(fast_ema, slow_ema, (ccount, ema_lvl, restart_phase XOR 1, end_of_phase), wasted, φ)›
fun incr_wasted :: ‹64 word ⇒ restart_heuristics ⇒ restart_heuristics› where
‹incr_wasted waste (fast_ema, slow_ema, res_info, wasted, φ) =
(fast_ema, slow_ema, res_info, wasted + waste, φ)›
fun set_zero_wasted :: ‹restart_heuristics ⇒ restart_heuristics› where
‹set_zero_wasted (fast_ema, slow_ema, res_info, wasted, φ) =
(fast_ema, slow_ema, res_info, 0, φ)›
fun wasted_of :: ‹restart_heuristics ⇒ 64 word› where
‹wasted_of (fast_ema, slow_ema, res_info, wasted, φ) = wasted›
definition heuristic_rel :: ‹nat multiset ⇒ restart_heuristics ⇒ bool› where
‹heuristic_rel 𝒜 = (λ(fast_ema, slow_ema, res_info, wasted, φ). phase_save_heur_rel 𝒜 φ)›
definition save_phase_heur :: ‹nat ⇒ bool ⇒ restart_heuristics ⇒ restart_heuristics› where
‹save_phase_heur L b = (λ(fast_ema, slow_ema, res_info, wasted, (φ, target, best)).
(fast_ema, slow_ema, res_info, wasted, (φ[L := b], target, best)))›
definition save_phase_heur_pre :: ‹nat ⇒ bool ⇒ restart_heuristics ⇒ bool› where
‹save_phase_heur_pre L b = (λ(fast_ema, slow_ema, res_info, wasted, (φ, _)). L < length φ)›
definition mop_save_phase_heur :: ‹nat ⇒ bool ⇒ restart_heuristics ⇒ restart_heuristics nres› where
‹mop_save_phase_heur L b heur = do {
ASSERT(save_phase_heur_pre L b heur);
RETURN (save_phase_heur L b heur)
}›
definition get_saved_phase_heur_pre :: ‹nat ⇒ restart_heuristics ⇒ bool› where
‹get_saved_phase_heur_pre L = (λ(fast_ema, slow_ema, res_info, wasted, (φ, _)). L < length φ)›
definition get_saved_phase_heur :: ‹nat ⇒ restart_heuristics ⇒ bool› where
‹get_saved_phase_heur L = (λ(fast_ema, slow_ema, res_info, wasted, (φ, _)). φ!L)›
definition current_rephasing_phase :: ‹restart_heuristics ⇒ 64 word› where
‹current_rephasing_phase = (λ(fast_ema, slow_ema, res_info, wasted, φ). phase_current_rephasing_phase φ)›
definition mop_get_saved_phase_heur :: ‹nat ⇒ restart_heuristics ⇒ bool nres› where
‹mop_get_saved_phase_heur L heur = do {
ASSERT(get_saved_phase_heur_pre L heur);
RETURN (get_saved_phase_heur L heur)
}›
definition end_of_rephasing_phase_heur :: ‹restart_heuristics ⇒ 64 word› where
‹end_of_rephasing_phase_heur =
(λ(fast_ema, slow_ema, res_info, wasted, phasing). end_of_rephasing_phase phasing)›
lemma heuristic_relI[intro!]:
‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (incr_wasted wast heur)›
‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (set_zero_wasted heur)›
‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (incr_restart_phase heur)›
‹heuristic_rel 𝒜 heur ⟹ heuristic_rel 𝒜 (save_phase_heur L b heur)›
by (clarsimp_all simp: heuristic_rel_def save_phase_heur_def phase_save_heur_rel_def phase_saving_def)
lemma save_phase_heur_preI:
‹heuristic_rel 𝒜 heur ⟹ a ∈# 𝒜 ⟹ save_phase_heur_pre a b heur›
by (auto simp: heuristic_rel_def phase_saving_def save_phase_heur_pre_def
phase_save_heur_rel_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
section ‹VMTF›
type_synonym (in -) isa_vmtf_remove_int = ‹vmtf × (nat list × bool list)›
section ‹Options›
type_synonym opts = ‹bool × bool × bool›
definition opts_restart where
‹opts_restart = (λ(a, b, c). a)›
definition opts_reduce where
‹opts_reduce = (λ(a, b, c). b)›
definition opts_unbounded_mode where
‹opts_unbounded_mode = (λ(a, b, c). c)›
type_synonym out_learned = ‹nat clause_l›
type_synonym vdom = ‹nat list›
subsection ‹Conflict›
definition size_conflict_wl :: ‹nat twl_st_wl ⇒ nat› where
‹size_conflict_wl S = size (the (get_conflict_wl S))›
definition size_conflict :: ‹nat clause option ⇒ nat› where
‹size_conflict D = size (the D)›
definition size_conflict_int :: ‹conflict_option_rel ⇒ nat› where
‹size_conflict_int = (λ(_, n, _). n)›
section ‹Full state›
text ‹∗‹heur› stands for heuristic.›
paragraph ‹Definition›
type_synonym twl_st_wl_heur =
‹trail_pol × arena ×
conflict_option_rel × nat × (nat watcher) list list × isa_vmtf_remove_int ×
nat × conflict_min_cach_l × lbd × out_learned × stats × restart_heuristics ×
vdom × vdom × nat × opts × arena›
paragraph ‹Accessors›
fun get_clauses_wl_heur :: ‹twl_st_wl_heur ⇒ arena› where
‹get_clauses_wl_heur (M, N, D, _) = N›
fun get_trail_wl_heur :: ‹twl_st_wl_heur ⇒ trail_pol› where
‹get_trail_wl_heur (M, N, D, _) = M›
fun get_conflict_wl_heur :: ‹twl_st_wl_heur ⇒ conflict_option_rel› where
‹get_conflict_wl_heur (_, _, D, _) = D›
fun watched_by_int :: ‹twl_st_wl_heur ⇒ nat literal ⇒ nat watched› where
‹watched_by_int (M, N, D, Q, W, _) L = W ! nat_of_lit L›
fun get_watched_wl_heur :: ‹twl_st_wl_heur ⇒ (nat watcher) list list› where
‹get_watched_wl_heur (_, _, _, _, W, _) = W›
fun literals_to_update_wl_heur :: ‹twl_st_wl_heur ⇒ nat› where
‹literals_to_update_wl_heur (M, N, D, Q, W, _, _) = Q›
fun set_literals_to_update_wl_heur :: ‹nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur› where
‹set_literals_to_update_wl_heur i (M, N, D, _, W') = (M, N, D, i, W')›
definition watched_by_app_heur_pre where
‹watched_by_app_heur_pre = (λ((S, L), K). nat_of_lit L < length (get_watched_wl_heur S) ∧
K < length (watched_by_int S L))›
definition (in -) watched_by_app_heur :: ‹twl_st_wl_heur ⇒ nat literal ⇒ nat ⇒ nat watcher› where
‹watched_by_app_heur S L K = watched_by_int S L ! K›
definition (in -) mop_watched_by_app_heur :: ‹twl_st_wl_heur ⇒ nat literal ⇒ nat ⇒ nat watcher nres› where
‹mop_watched_by_app_heur S L K = do {
ASSERT(K < length (watched_by_int S L));
ASSERT(nat_of_lit L < length (get_watched_wl_heur S));
RETURN (watched_by_int S L ! K)}›
lemma watched_by_app_heur_alt_def:
‹watched_by_app_heur = (λ(M, N, D, Q, W, _) L K. W ! nat_of_lit L ! K)›
by (auto simp: watched_by_app_heur_def intro!: ext)
definition watched_by_app :: ‹nat twl_st_wl ⇒ nat literal ⇒ nat ⇒ nat watcher› where
‹watched_by_app S L K = watched_by S L ! K›
fun get_vmtf_heur :: ‹twl_st_wl_heur ⇒ isa_vmtf_remove_int› where
‹get_vmtf_heur (_, _, _, _, _, vm, _) = vm›
fun get_count_max_lvls_heur :: ‹twl_st_wl_heur ⇒ nat› where
‹get_count_max_lvls_heur (_, _, _, _, _, _, clvls, _) = clvls›
fun get_conflict_cach:: ‹twl_st_wl_heur ⇒ conflict_min_cach_l› where
‹get_conflict_cach (_, _, _, _, _, _, _, cach, _) = cach›
fun get_lbd :: ‹twl_st_wl_heur ⇒ lbd› where
‹get_lbd (_, _, _, _, _, _, _, _, lbd, _) = lbd›
fun get_outlearned_heur :: ‹twl_st_wl_heur ⇒ out_learned› where
‹get_outlearned_heur (_, _, _, _, _, _, _, _, _, out, _) = out›
fun get_fast_ema_heur :: ‹twl_st_wl_heur ⇒ ema› where
‹get_fast_ema_heur (_, _, _, _, _, _, _, _, _, _, _, heur, _) = fast_ema_of heur›
fun get_slow_ema_heur :: ‹twl_st_wl_heur ⇒ ema› where
‹get_slow_ema_heur (_, _, _, _, _, _, _, _, _, _, _, heur, _) = slow_ema_of heur›
fun get_conflict_count_heur :: ‹twl_st_wl_heur ⇒ restart_info› where
‹get_conflict_count_heur (_, _, _, _, _, _, _, _, _, _, _, heur, _) = restart_info_of heur›
fun get_vdom :: ‹twl_st_wl_heur ⇒ nat list› where
‹get_vdom (_, _, _, _, _, _, _, _, _, _, _, _, vdom, _) = vdom›
fun get_avdom :: ‹twl_st_wl_heur ⇒ nat list› where
‹get_avdom (_, _, _, _, _, _, _, _, _, _, _, _, _, vdom, _) = vdom›
fun get_learned_count :: ‹twl_st_wl_heur ⇒ nat› where
‹get_learned_count (_, _, _, _, _, _, _, _, _, _, _, _, _, _, lcount, _) = lcount›
fun get_ops :: ‹twl_st_wl_heur ⇒ opts› where
‹get_ops (_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, opts, _) = opts›
fun get_old_arena :: ‹twl_st_wl_heur ⇒ arena› where
‹get_old_arena (_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, old_arena) = old_arena›
section ‹Virtual domain›
text ‹The virtual domain is composed of the addressable (and accessible) elements, i.e.,
the domain and all the deleted clauses that are still present in the watch lists.
›
definition vdom_m :: ‹nat multiset ⇒ (nat literal ⇒ (nat × _) list) ⇒ (nat, 'b) fmap ⇒ nat set› where
‹vdom_m 𝒜 W N = ⋃(((`) fst) ` set ` W ` set_mset (ℒ⇩a⇩l⇩l 𝒜)) ∪ set_mset (dom_m N)›
lemma vdom_m_simps[simp]:
‹bh ∈# dom_m N ⟹ vdom_m 𝒜 W (N(bh ↪ C)) = vdom_m 𝒜 W N›
‹bh ∉# dom_m N ⟹ vdom_m 𝒜 W (N(bh ↪ C)) = insert bh (vdom_m 𝒜 W N)›
by (force simp: vdom_m_def split: if_splits)+
lemma vdom_m_simps2[simp]:
‹i ∈# dom_m N ⟹ vdom_m 𝒜 (W(L := W L @ [(i, C)])) N = vdom_m 𝒜 W N›
‹bi ∈# dom_m ax ⟹ vdom_m 𝒜 (bp(L:= bp L @ [(bi, av')])) ax = vdom_m 𝒜 bp ax›
by (force simp: vdom_m_def split: if_splits)+
lemma vdom_m_simps3[simp]:
‹fst biav' ∈# dom_m ax ⟹ vdom_m 𝒜 (bp(L:= bp L @ [biav'])) ax = vdom_m 𝒜 bp ax›
by (cases biav'; auto simp: dest: multi_member_split[of L] split: if_splits)
text ‹What is the difference with the next lemma?›
lemma [simp]:
‹bf ∈# dom_m ax ⟹ vdom_m 𝒜 bj (ax(bf ↪ C')) = vdom_m 𝒜 bj (ax)›
by (force simp: vdom_m_def split: if_splits)+
lemma vdom_m_simps4[simp]:
‹i ∈# dom_m N ⟹
vdom_m 𝒜 (W (L1 := W L1 @ [(i, C1)], L2 := W L2 @ [(i, C2)])) N = vdom_m 𝒜 W N›
by (auto simp: vdom_m_def image_iff dest: multi_member_split split: if_splits)
text ‹This is @{thm vdom_m_simps4} if the assumption of distinctness is not present in the context.›
lemma vdom_m_simps4'[simp]:
‹i ∈# dom_m N ⟹
vdom_m 𝒜 (W (L1 := W L1 @ [(i, C1), (i, C2)])) N = vdom_m 𝒜 W N›
by (auto simp: vdom_m_def image_iff dest: multi_member_split split: if_splits)
text ‹We add a spurious dependency to the parameter of the locale:›
definition empty_watched :: ‹nat multiset ⇒ nat literal ⇒ (nat × nat literal × bool) list› where
‹empty_watched 𝒜 = (λ_. [])›
lemma vdom_m_empty_watched[simp]:
‹vdom_m 𝒜 (empty_watched 𝒜') N = set_mset (dom_m N)›
by (auto simp: vdom_m_def empty_watched_def)
text ‹The following rule makes the previous one not applicable. Therefore, we do not mark this lemma as
simp.›
lemma vdom_m_simps5:
‹i ∉# dom_m N ⟹ vdom_m 𝒜 W (fmupd i C N) = insert i (vdom_m 𝒜 W N)›
by (force simp: vdom_m_def image_iff dest: multi_member_split split: if_splits)
lemma in_watch_list_in_vdom:
assumes ‹L ∈# ℒ⇩a⇩l⇩l 𝒜› and ‹w < length (watched_by S L)›
shows ‹fst (watched_by S L ! w) ∈ vdom_m 𝒜 (get_watched_wl S) (get_clauses_wl S)›
using assms
unfolding vdom_m_def
by (cases S) (auto dest: multi_member_split)
lemma in_watch_list_in_vdom':
assumes ‹L ∈# ℒ⇩a⇩l⇩l 𝒜› and ‹A ∈ set (watched_by S L)›
shows ‹fst A ∈ vdom_m 𝒜 (get_watched_wl S) (get_clauses_wl S)›
using assms
unfolding vdom_m_def
by (cases S) (auto dest: multi_member_split)
lemma in_dom_in_vdom[simp]:
‹x ∈# dom_m N ⟹ x ∈ vdom_m 𝒜 W N›
unfolding vdom_m_def
by (auto dest: multi_member_split)
lemma in_vdom_m_upd:
‹x1f ∈ vdom_m 𝒜 (g(x1e := (g x1e)[x2 := (x1f, x2f)])) b›
if ‹x2 < length (g x1e)› and ‹x1e ∈# ℒ⇩a⇩l⇩l 𝒜›
using that
unfolding vdom_m_def
by (auto dest!: multi_member_split intro!: set_update_memI img_fst)
lemma in_vdom_m_fmdropD:
‹x ∈ vdom_m 𝒜 ga (fmdrop C baa) ⟹ x ∈ (vdom_m 𝒜 ga baa)›
unfolding vdom_m_def
by (auto dest: in_diffD)
definition cach_refinement_empty where
‹cach_refinement_empty 𝒜 cach ⟷
(cach, λ_. SEEN_UNKNOWN) ∈ cach_refinement 𝒜›
paragraph ‹VMTF›
definition isa_vmtf where
‹isa_vmtf 𝒜 M =
((Id ×⇩r nat_rel ×⇩r nat_rel ×⇩r nat_rel ×⇩r ⟨nat_rel⟩option_rel) ×⇩f distinct_atoms_rel 𝒜)¯
`` vmtf 𝒜 M›
lemma isa_vmtfI:
‹(vm, to_remove') ∈ vmtf 𝒜 M ⟹ (to_remove, to_remove') ∈ distinct_atoms_rel 𝒜 ⟹
(vm, to_remove) ∈ isa_vmtf 𝒜 M›
by (auto simp: isa_vmtf_def Image_iff intro!: bexI[of _ ‹(vm, to_remove')›])
lemma isa_vmtf_consD:
‹((ns, m, fst_As, lst_As, next_search), remove) ∈ isa_vmtf 𝒜 M ⟹
((ns, m, fst_As, lst_As, next_search), remove) ∈ isa_vmtf 𝒜 (L # M)›
by (auto simp: isa_vmtf_def dest: vmtf_consD)
lemma isa_vmtf_consD2:
‹f ∈ isa_vmtf 𝒜 M ⟹
f ∈ isa_vmtf 𝒜 (L # M)›
by (auto simp: isa_vmtf_def dest: vmtf_consD)
text ‹\<^term>‹vdom› is an upper bound on all the address of the clauses that are used in the
state. \<^term>‹avdom› includes the active clauses.
›
definition twl_st_heur :: ‹(twl_st_wl_heur × nat twl_st_wl) set› where
‹twl_st_heur =
{((M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena),
(M, N, D, NE, UE, NS, US, Q, W)).
(M', M) ∈ trail_pol (all_atms N (NE + UE + NS + US)) ∧
valid_arena N' N (set vdom) ∧
(D', D) ∈ option_lookup_clause_rel (all_atms N (NE + UE + NS + US)) ∧
(D = None ⟶ j ≤ length M) ∧
Q = uminus `# lit_of `# mset (drop j (rev M)) ∧
(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms N (NE + UE + NS + US))) ∧
vm ∈ isa_vmtf (all_atms N (NE + UE + NS + US)) M ∧
no_dup M ∧
clvls ∈ counts_maximum_level M D ∧
cach_refinement_empty (all_atms N (NE + UE + NS + US)) cach ∧
out_learned M D outl ∧
lcount = size (learned_clss_lf N) ∧
vdom_m (all_atms N (NE + UE + NS + US)) W N ⊆ set vdom ∧
mset avdom ⊆# mset vdom ∧
distinct vdom ∧
isasat_input_bounded (all_atms N (NE + UE + NS + US)) ∧
isasat_input_nempty (all_atms N (NE + UE + NS + US)) ∧
old_arena = [] ∧
heuristic_rel (all_atms N (NE + UE + NS + US)) heur
}›
lemma twl_st_heur_state_simp:
assumes ‹(S, S') ∈ twl_st_heur›
shows
‹(get_trail_wl_heur S, get_trail_wl S') ∈ trail_pol (all_atms_st S')› and
twl_st_heur_state_simp_watched: ‹C ∈# ℒ⇩a⇩l⇩l (all_atms_st S') ⟹
watched_by_int S C = watched_by S' C› and
‹literals_to_update_wl S' =
uminus `# lit_of `# mset (drop (literals_to_update_wl_heur S) (rev (get_trail_wl S')))› and
twl_st_heur_state_simp_watched2: ‹C ∈# ℒ⇩a⇩l⇩l (all_atms_st S') ⟹
nat_of_lit C < length(get_watched_wl_heur S)›
using assms unfolding twl_st_heur_def by (auto simp: map_fun_rel_def ac_simps)
abbreviation twl_st_heur'''
:: ‹nat ⇒ (twl_st_wl_heur × nat twl_st_wl) set›
where
‹twl_st_heur''' r ≡ {(S, T). (S, T) ∈ twl_st_heur ∧
length (get_clauses_wl_heur S) = r}›
definition twl_st_heur' :: ‹nat multiset ⇒ (twl_st_wl_heur × nat twl_st_wl) set› where
‹twl_st_heur' N = {(S, S'). (S, S') ∈ twl_st_heur ∧ dom_m (get_clauses_wl S') = N}›
definition twl_st_heur_conflict_ana
:: ‹(twl_st_wl_heur × nat twl_st_wl) set›
where
‹twl_st_heur_conflict_ana =
{((M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur, vdom,
avdom, lcount, opts, old_arena),
(M, N, D, NE, UE, NS, US, Q, W)).
(M', M) ∈ trail_pol (all_atms N (NE + UE + NS + US)) ∧
valid_arena N' N (set vdom) ∧
(D', D) ∈ option_lookup_clause_rel (all_atms N (NE + UE + NS + US)) ∧
(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms N (NE + UE + NS + US))) ∧
vm ∈ isa_vmtf (all_atms N (NE + UE + NS + US)) M ∧
no_dup M ∧
clvls ∈ counts_maximum_level M D ∧
cach_refinement_empty (all_atms N (NE + UE + NS + US)) cach ∧
out_learned M D outl ∧
lcount = size (learned_clss_lf N) ∧
vdom_m (all_atms N (NE + UE + NS + US)) W N ⊆ set vdom ∧
mset avdom ⊆# mset vdom ∧
distinct vdom ∧
isasat_input_bounded (all_atms N (NE + UE + NS + US)) ∧
isasat_input_nempty (all_atms N (NE + UE + NS + US)) ∧
old_arena = [] ∧
heuristic_rel (all_atms N (NE + UE + NS + US)) heur
}›
lemma twl_st_heur_twl_st_heur_conflict_ana:
‹(S, T) ∈ twl_st_heur ⟹ (S, T) ∈ twl_st_heur_conflict_ana›
by (auto simp: twl_st_heur_def twl_st_heur_conflict_ana_def ac_simps)
lemma twl_st_heur_ana_state_simp:
assumes ‹(S, S') ∈ twl_st_heur_conflict_ana›
shows
‹(get_trail_wl_heur S, get_trail_wl S') ∈ trail_pol (all_atms_st S')› and
‹C ∈# ℒ⇩a⇩l⇩l (all_atms_st S') ⟹ watched_by_int S C = watched_by S' C›
using assms unfolding twl_st_heur_conflict_ana_def by (auto simp: map_fun_rel_def ac_simps)
text ‹This relations decouples the conflict that has been minimised and appears abstractly
from the refined state, where the conflict has been removed from the data structure to a
separate array.›
definition twl_st_heur_bt :: ‹(twl_st_wl_heur × nat twl_st_wl) set› where
‹twl_st_heur_bt =
{((M', N', D', Q', W', vm, clvls, cach, lbd, outl, stats, heur, vdom, avdom, lcount, opts,
old_arena),
(M, N, D, NE, UE, NS, US, Q, W)).
(M', M) ∈ trail_pol (all_atms N (NE + UE + NS + US)) ∧
valid_arena N' N (set vdom) ∧
(D', None) ∈ option_lookup_clause_rel (all_atms N (NE + UE + NS + US)) ∧
(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 (all_atms N (NE + UE + NS + US))) ∧
vm ∈ isa_vmtf (all_atms N (NE + UE + NS + US)) M ∧
no_dup M ∧
clvls ∈ counts_maximum_level M None ∧
cach_refinement_empty (all_atms N (NE + UE + NS + US)) cach ∧
out_learned M None outl ∧
lcount = size (learned_clss_l N) ∧
vdom_m (all_atms N (NE + UE + NS + US)) W N ⊆ set vdom ∧
mset avdom ⊆# mset vdom ∧
distinct vdom ∧
isasat_input_bounded (all_atms N (NE + UE + NS + US)) ∧
isasat_input_nempty (all_atms N (NE + UE + NS + US)) ∧
old_arena = [] ∧
heuristic_rel (all_atms N (NE + UE + NS + US)) heur
}›
text ‹
The difference between \<^term>‹isasat_unbounded_assn› and \<^term>‹isasat_bounded_assn› corresponds to the
following condition:
›
definition isasat_fast :: ‹twl_st_wl_heur ⇒ bool› where
‹isasat_fast S ⟷ (length (get_clauses_wl_heur S) ≤ sint64_max - (uint32_max div 2 + 6))›
lemma isasat_fast_length_leD: ‹isasat_fast S ⟹ length (get_clauses_wl_heur S) ≤ sint64_max›
by (cases S) (auto simp: isasat_fast_def)
section ‹Lift Operations to State›
definition polarity_st :: ‹'v twl_st_wl ⇒ 'v literal ⇒ bool option› where
‹polarity_st S = polarity (get_trail_wl S)›
definition get_conflict_wl_is_None_heur :: ‹twl_st_wl_heur ⇒ bool› where
‹get_conflict_wl_is_None_heur = (λ(M, N, (b, _), Q, W, _). b)›
lemma get_conflict_wl_is_None_heur_get_conflict_wl_is_None:
‹(RETURN o get_conflict_wl_is_None_heur, RETURN o get_conflict_wl_is_None) ∈
twl_st_heur →⇩f ⟨Id⟩nres_rel›
unfolding get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def comp_def
apply (intro WB_More_Refinement.frefI nres_relI) apply refine_rcg
by (auto simp: twl_st_heur_def get_conflict_wl_is_None_heur_def get_conflict_wl_is_None_def
option_lookup_clause_rel_def
split: option.splits)
lemma get_conflict_wl_is_None_heur_alt_def:
‹RETURN o get_conflict_wl_is_None_heur = (λ(M, N, (b, _), Q, W, _). RETURN b)›
unfolding get_conflict_wl_is_None_heur_def
by auto
definition count_decided_st :: ‹nat twl_st_wl ⇒ nat› where
‹count_decided_st = (λ(M, _). count_decided M)›
definition isa_count_decided_st :: ‹twl_st_wl_heur ⇒ nat› where
‹isa_count_decided_st = (λ(M, _). count_decided_pol M)›
lemma count_decided_st_count_decided_st:
‹(RETURN o isa_count_decided_st, RETURN o count_decided_st) ∈ twl_st_heur →⇩f ⟨nat_rel⟩nres_rel›
by (intro WB_More_Refinement.frefI nres_relI)
(auto simp: count_decided_st_def twl_st_heur_def isa_count_decided_st_def
count_decided_trail_ref[THEN fref_to_Down_unRET_Id])
lemma count_decided_st_alt_def: ‹count_decided_st S = count_decided (get_trail_wl S)›
unfolding count_decided_st_def
by (cases S) auto
definition (in -) is_in_conflict_st :: ‹nat literal ⇒ nat twl_st_wl ⇒ bool› where
‹is_in_conflict_st L S ⟷ is_in_conflict L (get_conflict_wl S)›
definition atm_is_in_conflict_st_heur :: ‹nat literal ⇒ twl_st_wl_heur ⇒ bool nres› where
‹atm_is_in_conflict_st_heur L = (λ(M, N, (_, D), _). do {
ASSERT (atm_in_conflict_lookup_pre (atm_of L) D); RETURN (¬atm_in_conflict_lookup (atm_of L) D) })›
lemma atm_is_in_conflict_st_heur_alt_def:
‹atm_is_in_conflict_st_heur = (λL (M, N, (_, (_, D)), _). do {ASSERT ((atm_of L) < length D); RETURN (D ! (atm_of L) = None)})›
unfolding atm_is_in_conflict_st_heur_def by (auto intro!: ext simp: atm_in_conflict_lookup_def atm_in_conflict_lookup_pre_def)
lemma atm_of_in_atms_of_iff: ‹atm_of x ∈ atms_of D ⟷ x ∈# D ∨ -x ∈# D›
by (cases x) (auto simp: atms_of_def dest!: multi_member_split)
lemma atm_is_in_conflict_st_heur_is_in_conflict_st:
‹(uncurry (atm_is_in_conflict_st_heur), uncurry (mop_lit_notin_conflict_wl)) ∈
[λ(L, S). True]⇩f
Id ×⇩r twl_st_heur → ⟨Id⟩ nres_rel›
proof -
have 1: ‹aaa ∈# ℒ⇩a⇩l⇩l A ⟹ atm_of aaa ∈ atms_of (ℒ⇩a⇩l⇩l A)› for aaa A
by (auto simp: atms_of_def)
show ?thesis
unfolding atm_is_in_conflict_st_heur_def twl_st_heur_def option_lookup_clause_rel_def uncurry_def comp_def
mop_lit_notin_conflict_wl_def
apply (intro frefI nres_relI)
apply refine_rcg
apply clarsimp
subgoal
apply (rule atm_in_conflict_lookup_pre)
unfolding ℒ⇩a⇩l⇩l_all_atms_all_lits[symmetric]
apply assumption+
apply (auto simp: ac_simps)
done
subgoal for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x1e x2d x2e
apply (subst atm_in_conflict_lookup_atm_in_conflict[THEN fref_to_Down_unRET_uncurry_Id, of ‹all_atms_st x2› ‹atm_of x1› ‹the (get_conflict_wl (snd y))›])
apply (simp add: ℒ⇩a⇩l⇩l_all_atms_all_lits atms_of_def)[]
apply (auto simp add: ℒ⇩a⇩l⇩l_all_atms_all_lits atms_of_def option_lookup_clause_rel_def
ac_simps)[]
apply (simp add: atm_in_conflict_def atm_of_in_atms_of_iff)
done
done
qed
abbreviation nat_lit_lit_rel where
‹nat_lit_lit_rel ≡ Id :: (nat literal × _) set›
section ‹More theorems›
lemma valid_arena_DECISION_REASON:
‹valid_arena arena NU vdom ⟹ DECISION_REASON ∉# dom_m NU›
using arena_lifting[of arena NU vdom DECISION_REASON]
by (auto simp: DECISION_REASON_def SHIFTS_def)
definition count_decided_st_heur :: ‹_ ⇒ _› where
‹count_decided_st_heur = (λ((_,_,_,_,n, _), _). n)›
lemma twl_st_heur_count_decided_st_alt_def:
fixes S :: twl_st_wl_heur
shows ‹(S, T) ∈ twl_st_heur ⟹ count_decided_st_heur S = count_decided (get_trail_wl T)›
unfolding count_decided_st_def twl_st_heur_def trail_pol_def
by (cases S) (auto simp: count_decided_st_heur_def)
lemma twl_st_heur_isa_length_trail_get_trail_wl:
fixes S :: twl_st_wl_heur
shows ‹(S, T) ∈ twl_st_heur ⟹ isa_length_trail (get_trail_wl_heur S) = length (get_trail_wl T)›
unfolding isa_length_trail_def twl_st_heur_def trail_pol_def
by (cases S) (auto dest: ann_lits_split_reasons_map_lit_of)
lemma trail_pol_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ trail_pol 𝒜 ⟹ L ∈ trail_pol ℬ›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
by (auto simp: trail_pol_def ann_lits_split_reasons_def)
lemma distinct_atoms_rel_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ distinct_atoms_rel 𝒜 ⟹ L ∈ distinct_atoms_rel ℬ›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
unfolding vmtf_def vmtf_ℒ⇩a⇩l⇩l_def distinct_atoms_rel_def distinct_hash_atoms_rel_def
atoms_hash_rel_def
by (auto simp: )
lemma phase_save_heur_rel_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ phase_save_heur_rel 𝒜 heur ⟹ phase_save_heur_rel ℬ heur›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
by (auto simp: phase_save_heur_rel_def phase_saving_def)
lemma heuristic_rel_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ heuristic_rel 𝒜 heur ⟹ heuristic_rel ℬ heur›
using phase_save_heur_rel_cong[of 𝒜 ℬ ‹(λ(_, _, _, _, a). a) heur›]
by (auto simp: heuristic_rel_def)
lemma vmtf_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ vmtf 𝒜 M ⟹ L ∈ vmtf ℬ M›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
unfolding vmtf_def vmtf_ℒ⇩a⇩l⇩l_def
by auto
lemma isa_vmtf_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ isa_vmtf 𝒜 M ⟹ L ∈ isa_vmtf ℬ M›
using vmtf_cong[of 𝒜 ℬ] distinct_atoms_rel_cong[of 𝒜 ℬ]
apply (subst (asm) isa_vmtf_def)
apply (cases L)
by (auto intro!: isa_vmtfI)
lemma option_lookup_clause_rel_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ L ∈ option_lookup_clause_rel 𝒜 ⟹ L ∈ option_lookup_clause_rel ℬ›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
unfolding option_lookup_clause_rel_def lookup_clause_rel_def
apply (cases L)
by (auto intro!: isa_vmtfI)
lemma D⇩0_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ D⇩0 𝒜 = D⇩0 ℬ›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
by auto
lemma phase_saving_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ phase_saving 𝒜 = phase_saving ℬ›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
by (auto simp: phase_saving_def)
lemma distinct_subseteq_iff2:
assumes dist: "distinct_mset M"
shows "set_mset M ⊆ set_mset N ⟷ M ⊆# N"
proof
assume "set_mset M ⊆ set_mset N"
then show "M ⊆# N"
using dist by (metis distinct_mset_set_mset_ident mset_set_subset_iff)
next
assume "M ⊆# N"
then show "set_mset M ⊆ set_mset N"
by (metis set_mset_mono)
qed
lemma cach_refinement_empty_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ cach_refinement_empty 𝒜 = cach_refinement_empty ℬ›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
by (force simp: cach_refinement_empty_def cach_refinement_alt_def
distinct_subseteq_iff2[symmetric] intro!: ext)
lemma vdom_m_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ vdom_m 𝒜 x y = vdom_m ℬ x y›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
by (auto simp: vdom_m_def intro!: ext)
lemma isasat_input_bounded_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ isasat_input_bounded 𝒜 = isasat_input_bounded ℬ›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
by (auto simp: intro!: ext)
lemma isasat_input_nempty_cong:
‹set_mset 𝒜 = set_mset ℬ ⟹ isasat_input_nempty 𝒜 = isasat_input_nempty ℬ›
using ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ] atms_of_ℒ⇩a⇩l⇩l_cong[of 𝒜 ℬ]
by (auto simp: intro!: ext)
section ‹Shared Code Equations›
definition clause_not_marked_to_delete where
‹clause_not_marked_to_delete S C ⟷ C ∈# dom_m (get_clauses_wl S)›
definition clause_not_marked_to_delete_pre where
‹clause_not_marked_to_delete_pre =
(λ(S, C). C ∈ vdom_m (all_atms_st S) (get_watched_wl S) (get_clauses_wl S))›
definition clause_not_marked_to_delete_heur_pre where
‹clause_not_marked_to_delete_heur_pre =
(λ(S, C). arena_is_valid_clause_vdom (get_clauses_wl_heur S) C)›
definition clause_not_marked_to_delete_heur :: ‹_ ⇒ nat ⇒ bool›
where
‹clause_not_marked_to_delete_heur S C ⟷
arena_status (get_clauses_wl_heur S) C ≠ DELETED›
lemma clause_not_marked_to_delete_rel:
‹(uncurry (RETURN oo clause_not_marked_to_delete_heur),
uncurry (RETURN oo clause_not_marked_to_delete)) ∈
[clause_not_marked_to_delete_pre]⇩f
twl_st_heur ×⇩f nat_rel → ⟨bool_rel⟩nres_rel›
by (intro WB_More_Refinement.frefI nres_relI)
(use arena_dom_status_iff in_dom_in_vdom in
‹auto 5 5 simp: clause_not_marked_to_delete_def twl_st_heur_def
clause_not_marked_to_delete_heur_def arena_dom_status_iff
clause_not_marked_to_delete_pre_def ac_simps›)
definition (in -) access_lit_in_clauses_heur_pre where
‹access_lit_in_clauses_heur_pre =
(λ((S, i), j).
arena_lit_pre (get_clauses_wl_heur S) (i+j))›
definition (in -) access_lit_in_clauses_heur where
‹access_lit_in_clauses_heur S i j = arena_lit (get_clauses_wl_heur S) (i + j)›
lemma access_lit_in_clauses_heur_alt_def:
‹access_lit_in_clauses_heur = (λ(M, N, _) i j. arena_lit N (i + j))›
by (auto simp: access_lit_in_clauses_heur_def intro!: ext)
definition (in -) mop_access_lit_in_clauses_heur where
‹mop_access_lit_in_clauses_heur S i j = mop_arena_lit2 (get_clauses_wl_heur S) i j›
lemma mop_access_lit_in_clauses_heur_alt_def:
‹mop_access_lit_in_clauses_heur = (λ(M, N, _) i j. mop_arena_lit2 N i j)›
by (auto simp: mop_access_lit_in_clauses_heur_def intro!: ext)
lemma access_lit_in_clauses_heur_fast_pre:
‹arena_lit_pre (get_clauses_wl_heur a) (ba + b) ⟹
isasat_fast a ⟹ ba + b ≤ sint64_max›
by (auto simp: arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
dest!: arena_lifting(10)
dest!: isasat_fast_length_leD)[]
lemma eq_insertD: ‹A = insert a B ⟹ a ∈ A ∧ B ⊆ A›
by auto
lemma ℒ⇩a⇩l⇩l_add_mset:
‹set_mset (ℒ⇩a⇩l⇩l (add_mset L C)) = insert (Pos L) (insert (Neg L) (set_mset (ℒ⇩a⇩l⇩l C)))›
by (auto simp: ℒ⇩a⇩l⇩l_def)
lemma correct_watching_dom_watched:
assumes ‹correct_watching S› and ‹⋀C. C ∈# ran_mf (get_clauses_wl S) ⟹ C ≠ []›
shows ‹set_mset (dom_m (get_clauses_wl S)) ⊆
⋃(((`) fst) ` set ` (get_watched_wl S) ` set_mset (ℒ⇩a⇩l⇩l (all_atms_st S)))›
(is ‹?A ⊆ ?B›)
proof
fix C
assume ‹C ∈ ?A›
then obtain D where
D: ‹D ∈# ran_mf (get_clauses_wl S)› and
D': ‹D = get_clauses_wl S ∝ C› and
C: ‹C ∈# dom_m (get_clauses_wl S)›
by auto
have ‹atm_of (hd D) ∈# atm_of `# all_lits_st S›
using D D' assms(2)[of D]
by (cases S; cases D)
(auto simp: all_lits_def
all_lits_of_mm_add_mset all_lits_of_m_add_mset
dest!: multi_member_split)
then show ‹C ∈ ?B›
using assms(1) assms(2)[of D] D D'
multi_member_split[OF C]
by (cases S; cases ‹get_clauses_wl S ∝ C›;
cases ‹hd (get_clauses_wl S ∝ C)›)
(auto simp: correct_watching.simps clause_to_update_def
all_lits_of_mm_add_mset all_lits_of_m_add_mset
ℒ⇩a⇩l⇩l_add_mset
eq_commute[of ‹_ # _›] atm_of_eq_atm_of
simp flip: all_atms_def
dest!: multi_member_split eq_insertD
dest!: arg_cong[of ‹filter_mset _ _› ‹add_mset _ _› set_mset])
qed
section ‹Rewatch›
definition rewatch_heur where
‹rewatch_heur vdom arena W = do {
let _ = vdom;
nfoldli [0..<length vdom] (λ_. True)
(λi W. do {
ASSERT(i < length vdom);
let C = vdom ! i;
ASSERT(arena_is_valid_clause_vdom arena C);
if arena_status arena C ≠ DELETED
then do {
L1 ← mop_arena_lit2 arena C 0;
L2 ← mop_arena_lit2 arena C 1;
n ← mop_arena_length arena C;
let b = (n = 2);
ASSERT(length (W ! (nat_of_lit L1)) < length arena);
W ← mop_append_ll W L1 (C, L2, b);
ASSERT(length (W ! (nat_of_lit L2)) < length arena);
W ← mop_append_ll W L2 (C, L1, b);
RETURN W
}
else RETURN W
})
W
}›
lemma rewatch_heur_rewatch:
assumes
valid: ‹valid_arena arena N vdom› and ‹set xs ⊆ vdom› and ‹distinct xs› and ‹set_mset (dom_m N) ⊆ set xs› and
‹(W, W') ∈ ⟨Id⟩map_fun_rel (D⇩0 𝒜)› and lall: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf N)› and
‹vdom_m 𝒜 W' N ⊆ set_mset (dom_m N)›
shows
‹rewatch_heur xs arena W ≤ ⇓ ({(W, W'). (W, W') ∈⟨Id⟩map_fun_rel (D⇩0 𝒜) ∧ vdom_m 𝒜 W' N ⊆ set_mset (dom_m N)}) (rewatch N W')›
proof -
have [refine0]: ‹(xs, xsa) ∈ Id ⟹
([0..<length xs], [0..<length xsa]) ∈ ⟨{(x, x'). x = x' ∧ x < length xsa ∧ xs!x ∈ vdom}⟩list_rel›
for xsa
using assms unfolding list_rel_def
by (auto simp: list_all2_same)
show ?thesis
unfolding rewatch_heur_def rewatch_def
apply (subst (2) nfoldli_nfoldli_list_nth)
apply (refine_vcg mop_arena_lit[OF valid] mop_append_ll[of 𝒜, THEN fref_to_Down_curry2, unfolded comp_def]
mop_arena_length[of vdom, THEN fref_to_Down_curry, unfolded comp_def])
subgoal
using assms by fast
subgoal
using assms by fast
subgoal
using assms by fast
subgoal by fast
subgoal by auto
subgoal
using assms
unfolding arena_is_valid_clause_vdom_def
by blast
subgoal
using assms
by (auto simp: arena_dom_status_iff)
subgoal for xsa xi x si s
using assms
by auto
subgoal by simp
subgoal by linarith
subgoal for xsa xi x si s
using assms
unfolding arena_lit_pre_def
by (auto)
subgoal by simp
subgoal by simp
subgoal by simp
subgoal for xsa xi x si s
using assms
unfolding arena_is_valid_clause_idx_and_access_def
arena_is_valid_clause_idx_def
by (auto simp: arena_is_valid_clause_idx_and_access_def
intro!: exI[of _ N] exI[of _ vdom])
subgoal for xsa xi x si s
using valid_arena_size_dom_m_le_arena[OF assms(1)] assms
literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[OF lall, of ‹xs ! xi› 0]
by (auto simp: map_fun_rel_def arena_lifting)
subgoal for xsa xi x si s
using valid_arena_size_dom_m_le_arena[OF assms(1)] assms
literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[OF lall, of ‹xs ! xi› 0]
by (auto simp: map_fun_rel_def arena_lifting)
subgoal using assms by (simp add: arena_lifting)
subgoal for xsa xi x si s
using literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[OF lall, of ‹xs ! xi› 1]
assms valid_arena_size_dom_m_le_arena[OF assms(1)]
by (auto simp: arena_lifting append_ll_def map_fun_rel_def)
subgoal for xsa xi x si s
using literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l[OF lall, of ‹xs ! xi› 1]
assms
by (auto simp: arena_lifting append_ll_def map_fun_rel_def)
subgoal for xsa xi x si s
using assms
by (auto simp: arena_lifting append_ll_def map_fun_rel_def)
subgoal for xsa xi x si s
using assms
by (auto simp: arena_lifting append_ll_def map_fun_rel_def)
done
qed
lemma rewatch_heur_alt_def:
‹rewatch_heur vdom arena W = do {
let _ = vdom;
nfoldli [0..<length vdom] (λ_. True)
(λi W. do {
ASSERT(i < length vdom);
let C = vdom ! i;
ASSERT(arena_is_valid_clause_vdom arena C);
if arena_status arena C ≠ DELETED
then do {
L1 ← mop_arena_lit2 arena C 0;
L2 ← mop_arena_lit2 arena C 1;
n ← mop_arena_length arena C;
let b = (n = 2);
ASSERT(length (W ! (nat_of_lit L1)) < length arena);
W ← mop_append_ll W L1 (C, L2, b);
ASSERT(length (W ! (nat_of_lit L2)) < length arena);
W ← mop_append_ll W L2 (C, L1, b);
RETURN W
}
else RETURN W
})
W
}›
unfolding Let_def rewatch_heur_def
by auto
lemma arena_lit_pre_le_sint64_max:
‹length ba ≤ sint64_max ⟹
arena_lit_pre ba a ⟹ a ≤ sint64_max›
using arena_lifting(10)[of ba _ _]
by (fastforce simp: arena_lifting arena_is_valid_clause_idx_def arena_lit_pre_def
arena_is_valid_clause_idx_and_access_def)
definition rewatch_heur_st
:: ‹twl_st_wl_heur ⇒ twl_st_wl_heur nres›
where
‹rewatch_heur_st = (λ(M, N0, D, Q, W, vm, clvls, cach, lbd, outl,
stats, heur, vdom, avdom, ccount, lcount). do {
ASSERT(length vdom ≤ length N0);
W ← rewatch_heur vdom N0 W;
RETURN (M, N0, D, Q, W, vm, clvls, cach, lbd, outl,
stats, heur, vdom, avdom, ccount, lcount)
})›
definition rewatch_heur_st_fast where
‹rewatch_heur_st_fast = rewatch_heur_st›
definition rewatch_heur_st_fast_pre where
‹rewatch_heur_st_fast_pre S =
((∀x ∈ set (get_vdom S). x ≤ sint64_max) ∧ length (get_clauses_wl_heur S) ≤ sint64_max)›
definition rewatch_st :: ‹'v twl_st_wl ⇒ 'v twl_st_wl nres› where
‹rewatch_st S = do{
(M, N, D, NE, UE, NS, US, Q, W) ← RETURN S;
W ← rewatch N W;
RETURN ((M, N, D, NE, UE, NS, US, Q, W))
}›
fun remove_watched_wl :: ‹'v twl_st_wl ⇒ _› where
‹remove_watched_wl (M, N, D, NE, UE, NS, US, Q, _) = (M, N, D, NE, UE, NS, US, Q)›
lemma rewatch_st_correctness:
assumes ‹get_watched_wl S = (λ_. [])› and
‹⋀x. x ∈# dom_m (get_clauses_wl S) ⟹
distinct ((get_clauses_wl S) ∝ x) ∧ 2 ≤ length ((get_clauses_wl S) ∝ x)›
shows ‹rewatch_st S ≤ SPEC (λT. remove_watched_wl S = remove_watched_wl T ∧
correct_watching_init T)›
apply (rule SPEC_rule_conjI)
subgoal
using rewatch_correctness[OF assms]
unfolding rewatch_st_def
apply (cases S, case_tac ‹rewatch b i›)
by (auto simp: RES_RETURN_RES)
subgoal
using rewatch_correctness[OF assms]
unfolding rewatch_st_def
apply (cases S, case_tac ‹rewatch b i›)
by (force simp: RES_RETURN_RES)+
done
section ‹Fast to slow conversion›
text ‹Setup to convert a list from \<^typ>‹64 word› to \<^typ>‹nat›.›
definition convert_wlists_to_nat_conv :: ‹'a list list ⇒ 'a list list› where
‹convert_wlists_to_nat_conv = id›
abbreviation twl_st_heur''
:: ‹nat multiset ⇒ nat ⇒ (twl_st_wl_heur × nat twl_st_wl) set›
where
‹twl_st_heur'' 𝒟 r ≡ {(S, T). (S, T) ∈ twl_st_heur' 𝒟 ∧
length (get_clauses_wl_heur S) = r}›
abbreviation twl_st_heur_up''
:: ‹nat multiset ⇒ nat ⇒ nat ⇒ nat literal ⇒ (twl_st_wl_heur × nat twl_st_wl) set›
where
‹twl_st_heur_up'' 𝒟 r s L ≡ {(S, T). (S, T) ∈ twl_st_heur'' 𝒟 r ∧
length (watched_by T L) = s ∧ s ≤ r}›
lemma length_watched_le:
assumes
prop_inv: ‹correct_watching x1› and
xb_x'a: ‹(x1a, x1) ∈ twl_st_heur'' 𝒟1 r› and
x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms_st x1)›
shows ‹length (watched_by x1 x2) ≤ r - 4›
proof -
have dist: ‹distinct_watched (watched_by x1 x2)›
using prop_inv x2 unfolding all_atms_def all_lits_def
by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps ac_simps)
then have dist: ‹distinct_watched (watched_by x1 x2)›
using xb_x'a
by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps)
have dist_vdom: ‹distinct (get_vdom x1a)›
using xb_x'a
by (cases x1)
(auto simp: twl_st_heur_def twl_st_heur'_def)
have x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms (get_clauses_wl x1)
(get_unit_clauses_wl x1 + get_subsumed_clauses_wl x1))›
using x2 xb_x'a unfolding all_atms_def
by auto
have
valid: ‹valid_arena (get_clauses_wl_heur x1a) (get_clauses_wl x1) (set (get_vdom x1a))›
using xb_x'a unfolding all_atms_def all_lits_def
by (cases x1)
(auto simp: twl_st_heur'_def twl_st_heur_def)
have ‹vdom_m (all_atms_st x1) (get_watched_wl x1) (get_clauses_wl x1) ⊆ set (get_vdom x1a)›
using xb_x'a
by (cases x1)
(auto simp: twl_st_heur_def twl_st_heur'_def ac_simps)
then have subset: ‹set (map fst (watched_by x1 x2)) ⊆ set (get_vdom x1a)›
using x2 unfolding vdom_m_def
by (cases x1)
(force simp: twl_st_heur'_def twl_st_heur_def
dest!: multi_member_split)
have watched_incl: ‹mset (map fst (watched_by x1 x2)) ⊆# mset (get_vdom x1a)›
by (rule distinct_subseteq_iff[THEN iffD1])
(use dist[unfolded distinct_watched_alt_def] dist_vdom subset in
‹simp_all flip: distinct_mset_mset_distinct›)
have vdom_incl: ‹set (get_vdom x1a) ⊆ {4..< length (get_clauses_wl_heur x1a)}›
using valid_arena_in_vdom_le_arena[OF valid] arena_dom_status_iff[OF valid] by auto
have ‹length (get_vdom x1a) ≤ length (get_clauses_wl_heur x1a) - 4›
by (subst distinct_card[OF dist_vdom, symmetric])
(use card_mono[OF _ vdom_incl] in auto)
then show ?thesis
using size_mset_mono[OF watched_incl] xb_x'a
by (auto intro!: order_trans[of ‹length (watched_by x1 x2)› ‹length (get_vdom x1a)›])
qed
lemma length_watched_le2:
assumes
prop_inv: ‹correct_watching_except i j L x1› and
xb_x'a: ‹(x1a, x1) ∈ twl_st_heur'' 𝒟1 r› and
x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms_st x1)› and diff: ‹L ≠ x2›
shows ‹length (watched_by x1 x2) ≤ r - 4›
proof -
from prop_inv diff have dist: ‹distinct_watched (watched_by x1 x2)›
using x2 unfolding all_atms_def all_lits_def
by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching_except.simps ac_simps)
then have dist: ‹distinct_watched (watched_by x1 x2)›
using xb_x'a
by (cases x1; auto simp: ℒ⇩a⇩l⇩l_atm_of_all_lits_of_mm correct_watching.simps)
have dist_vdom: ‹distinct (get_vdom x1a)›
using xb_x'a
by (cases x1)
(auto simp: twl_st_heur_def twl_st_heur'_def)
have x2: ‹x2 ∈# ℒ⇩a⇩l⇩l (all_atms (get_clauses_wl x1) (get_unit_clauses_wl x1 + get_subsumed_clauses_wl x1))›
using x2 xb_x'a
by (auto simp flip: all_atms_def all_lits_alt_def2 simp: ac_simps)
have
valid: ‹valid_arena (get_clauses_wl_heur x1a) (get_clauses_wl x1) (set (get_vdom x1a))›
using xb_x'a unfolding all_atms_def all_lits_def
by (cases x1)
(auto simp: twl_st_heur'_def twl_st_heur_def)
have ‹vdom_m (all_atms_st x1) (get_watched_wl x1) (get_clauses_wl x1) ⊆ set (get_vdom x1a)›
using xb_x'a
by (cases x1)
(auto simp: twl_st_heur_def twl_st_heur'_def ac_simps simp flip: all_atms_def)
then have subset: ‹set (map fst (watched_by x1 x2)) ⊆ set (get_vdom x1a)›
using x2 unfolding vdom_m_def
by (cases x1)
(force simp: twl_st_heur'_def twl_st_heur_def ac_simps simp flip: all_atms_def all_lits_alt_def2
dest!: multi_member_split)
have watched_incl: ‹mset (map fst (watched_by x1 x2)) ⊆# mset (get_vdom x1a)›
by (rule distinct_subseteq_iff[THEN iffD1])
(use dist[unfolded distinct_watched_alt_def] dist_vdom subset in
‹simp_all flip: distinct_mset_mset_distinct›)
have vdom_incl: ‹set (get_vdom x1a) ⊆ {4..< length (get_clauses_wl_heur x1a)}›
using valid_arena_in_vdom_le_arena[OF valid] arena_dom_status_iff[OF valid] by auto
have ‹length (get_vdom x1a) ≤ length (get_clauses_wl_heur x1a) - 4›
by (subst distinct_card[OF dist_vdom, symmetric])
(use card_mono[OF _ vdom_incl] in auto)
then show ?thesis
using size_mset_mono[OF watched_incl] xb_x'a
by (auto intro!: order_trans[of ‹length (watched_by x1 x2)› ‹length (get_vdom x1a)›])
qed
lemma atm_of_all_lits_of_m: ‹atm_of `# (all_lits_of_m C) = atm_of `# C + atm_of `# C›
‹atm_of ` set_mset (all_lits_of_m C) = atm_of `set_mset C ›
by (induction C; auto simp: all_lits_of_m_add_mset)+
lemma mop_watched_by_app_heur_mop_watched_by_at:
‹(uncurry2 mop_watched_by_app_heur, uncurry2 mop_watched_by_at) ∈
twl_st_heur ×⇩f nat_lit_lit_rel ×⇩f nat_rel →⇩f ⟨Id⟩nres_rel›
unfolding mop_watched_by_app_heur_def mop_watched_by_at_def uncurry_def all_lits_def[symmetric] all_lits_alt_def[symmetric]
by (intro frefI nres_relI, refine_rcg,
auto simp: twl_st_heur_def ℒ⇩a⇩l⇩l_all_atms_all_lits map_fun_rel_def
simp flip: all_lits_alt_def2)
(auto simp: add.assoc)
lemma mop_watched_by_app_heur_mop_watched_by_at'':
‹(uncurry2 mop_watched_by_app_heur, uncurry2 mop_watched_by_at) ∈
twl_st_heur_up'' 𝒟 r s K ×⇩f nat_lit_lit_rel ×⇩f nat_rel →⇩f ⟨Id⟩nres_rel›
by (rule fref_mono[THEN set_mp, OF _ _ _ mop_watched_by_app_heur_mop_watched_by_at])
(auto simp: ℒ⇩a⇩l⇩l_all_atms_all_lits twl_st_heur'_def map_fun_rel_def)
definition mop_polarity_pol :: ‹trail_pol ⇒ nat literal ⇒ bool option nres› where
‹mop_polarity_pol = (λM L. do {
ASSERT(polarity_pol_pre M L);
RETURN (polarity_pol M L)
})›
definition polarity_st_pre :: ‹nat twl_st_wl × nat literal ⇒ bool› where
‹polarity_st_pre ≡ λ(S, L). L ∈# ℒ⇩a⇩l⇩l (all_atms_st S)›
definition mop_polarity_st_heur :: ‹twl_st_wl_heur ⇒ nat literal ⇒ bool option nres› where
‹mop_polarity_st_heur S L = do {
mop_polarity_pol (get_trail_wl_heur S) L
}›
lemma mop_polarity_st_heur_alt_def: ‹mop_polarity_st_heur = (λ(M, _) L. do {
mop_polarity_pol M L
})›
by (auto simp: mop_polarity_st_heur_def intro!: ext)
lemma mop_polarity_st_heur_mop_polarity_wl:
‹(uncurry mop_polarity_st_heur, uncurry mop_polarity_wl) ∈
[λ_. True]⇩f twl_st_heur ×⇩r Id → ⟨⟨bool_rel⟩option_rel⟩nres_rel›
unfolding mop_polarity_wl_def mop_polarity_st_heur_def uncurry_def mop_polarity_pol_def
apply (intro frefI nres_relI)
apply (refine_rcg polarity_pol_polarity[of ‹all_atms _ _›, THEN fref_to_Down_unRET_uncurry])
apply (auto simp: twl_st_heur_def ℒ⇩a⇩l⇩l_all_atms_all_lits ac_simps
intro!: polarity_pol_pre simp flip: all_atms_def)
done
lemma mop_polarity_st_heur_mop_polarity_wl'':
‹(uncurry mop_polarity_st_heur, uncurry mop_polarity_wl) ∈
[λ_. True]⇩f twl_st_heur_up'' 𝒟 r s K ×⇩r Id → ⟨⟨bool_rel⟩option_rel⟩nres_rel›
by (rule fref_mono[THEN set_mp, OF _ _ _ mop_polarity_st_heur_mop_polarity_wl])
(auto simp: ℒ⇩a⇩l⇩l_all_atms_all_lits twl_st_heur'_def map_fun_rel_def)
lemma [simp,iff]: ‹literals_are_ℒ⇩i⇩n (all_atms_st S) S ⟷ blits_in_ℒ⇩i⇩n S›
unfolding literals_are_ℒ⇩i⇩n_def is_ℒ⇩a⇩l⇩l_def ℒ⇩a⇩l⇩l_all_atms_all_lits
by auto
definition length_avdom :: ‹twl_st_wl_heur ⇒ nat› where
‹length_avdom S = length (get_avdom S)›
lemma length_avdom_alt_def:
‹length_avdom = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount). length avdom)›
by (intro ext) (auto simp: length_avdom_def)
definition clause_is_learned_heur :: "twl_st_wl_heur ⇒ nat ⇒ bool"
where
‹clause_is_learned_heur S C ⟷ arena_status (get_clauses_wl_heur S) C = LEARNED›
lemma clause_is_learned_heur_alt_def:
‹clause_is_learned_heur = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats,
heur, vdom, lcount) C . arena_status N' C = LEARNED)›
by (intro ext) (auto simp: clause_is_learned_heur_def)
definition get_the_propagation_reason_heur
:: ‹twl_st_wl_heur ⇒ nat literal ⇒ nat option nres›
where
‹get_the_propagation_reason_heur S = get_the_propagation_reason_pol (get_trail_wl_heur S)›
lemma get_the_propagation_reason_heur_alt_def:
‹get_the_propagation_reason_heur = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats,
heur, vdom, lcount) L . get_the_propagation_reason_pol M' L)›
by (intro ext) (auto simp: get_the_propagation_reason_heur_def)
definition clause_lbd_heur :: "twl_st_wl_heur ⇒ nat ⇒ nat"
where
‹clause_lbd_heur S C = arena_lbd (get_clauses_wl_heur S) C›
definition (in -) access_length_heur where
‹access_length_heur S i = arena_length (get_clauses_wl_heur S) i›
lemma access_length_heur_alt_def:
‹access_length_heur = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur, vdom,
lcount) C. arena_length N' C)›
by (intro ext) (auto simp: access_length_heur_def arena_lbd_def)
definition marked_as_used_st where
‹marked_as_used_st T C =
marked_as_used (get_clauses_wl_heur T) C›
lemma marked_as_used_st_alt_def:
‹marked_as_used_st = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur, vdom,
lcount) C.
marked_as_used N' C)›
by (intro ext) (auto simp: marked_as_used_st_def)
definition access_vdom_at :: ‹twl_st_wl_heur ⇒ nat ⇒ nat› where
‹access_vdom_at S i = get_avdom S ! i›
lemma access_vdom_at_alt_def:
‹access_vdom_at = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur, vdom, avdom, lcount) i. avdom ! i)›
by (intro ext) (auto simp: access_vdom_at_def)
definition access_vdom_at_pre where
‹access_vdom_at_pre S i ⟷ i < length (get_avdom S)›
definition mark_garbage_heur :: ‹nat ⇒ nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur› where
‹mark_garbage_heur C i = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena).
(M', extra_information_mark_to_delete N' C, D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, delete_index_and_swap avdom i, lcount - 1, opts, old_arena))›
definition mark_garbage_heur2 :: ‹nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹mark_garbage_heur2 C = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts). do{
let st = arena_status N' C = IRRED;
ASSERT(¬st ⟶ lcount ≥ 1);
RETURN (M', extra_information_mark_to_delete N' C, D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, if st then lcount else lcount - 1, opts) })›
definition delete_index_vdom_heur :: ‹nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur›where
‹delete_index_vdom_heur = (λi (M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur, vdom, avdom, lcount).
(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur, vdom, delete_index_and_swap avdom i, lcount))›
lemma arena_act_pre_mark_used:
‹arena_act_pre arena C ⟹
arena_act_pre (mark_unused arena C) C›
unfolding arena_act_pre_def arena_is_valid_clause_idx_def
apply clarify
apply (rule_tac x=N in exI)
apply (rule_tac x=vdom in exI)
by (auto simp: arena_act_pre_def
simp: valid_arena_mark_unused)
definition mop_mark_garbage_heur :: ‹nat ⇒ nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹mop_mark_garbage_heur C i = (λS. do {
ASSERT(mark_garbage_pre (get_clauses_wl_heur S, C) ∧ get_learned_count S ≥ 1 ∧ i < length (get_avdom S));
RETURN (mark_garbage_heur C i S)
})›
definition mark_unused_st_heur :: ‹nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur› where
‹mark_unused_st_heur C = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl,
stats, heur, vdom, avdom, lcount, opts).
(M', arena_decr_act (mark_unused N' C) C, D', j, W', vm, clvls, cach,
lbd, outl, stats, heur,
vdom, avdom, lcount, opts))›
definition mop_mark_unused_st_heur :: ‹nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹mop_mark_unused_st_heur C T = do {
ASSERT(arena_act_pre (get_clauses_wl_heur T) C);
RETURN (mark_unused_st_heur C T)
}›
lemma mop_mark_garbage_heur_alt_def:
‹mop_mark_garbage_heur C i = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena). do {
ASSERT(mark_garbage_pre (get_clauses_wl_heur (M', N', D', j, W', vm, clvls, cach, lbd, outl,
stats, heur, vdom, avdom, lcount, opts, old_arena), C) ∧ lcount ≥ 1 ∧ i < length avdom);
RETURN (M', extra_information_mark_to_delete N' C, D', j, W', vm, clvls, cach, lbd, outl,
stats, heur,
vdom, delete_index_and_swap avdom i, lcount - 1, opts, old_arena)
})›
unfolding mop_mark_garbage_heur_def mark_garbage_heur_def
by (auto intro!: ext)
lemma mark_unused_st_heur_simp[simp]:
‹get_avdom (mark_unused_st_heur C T) = get_avdom T›
‹get_vdom (mark_unused_st_heur C T) = get_vdom T›
by (cases T; auto simp: mark_unused_st_heur_def; fail)+
lemma get_slow_ema_heur_alt_def:
‹RETURN o get_slow_ema_heur = (λ(M, N0, D, Q, W, vm, clvls, cach, lbd, outl,
stats, (fema, sema, _), lcount). RETURN sema)›
by auto
lemma get_fast_ema_heur_alt_def:
‹RETURN o get_fast_ema_heur = (λ(M, N0, D, Q, W, vm, clvls, cach, lbd, outl,
stats, (fema, sema, ccount), lcount). RETURN fema)›
by auto
fun get_conflict_count_since_last_restart_heur :: ‹twl_st_wl_heur ⇒ 64 word› where
‹get_conflict_count_since_last_restart_heur (_, _, _, _, _, _, _, _, _, _, _,
(_, _, (ccount, _), _), _)
= ccount›
lemma (in -) get_counflict_count_heur_alt_def:
‹RETURN o get_conflict_count_since_last_restart_heur = (λ(M, N0, D, Q, W, vm, clvls, cach, lbd,
outl, stats, (_, _, (ccount, _), _), lcount). RETURN ccount)›
by auto
lemma get_learned_count_alt_def:
‹RETURN o get_learned_count = (λ(M, N0, D, Q, W, vm, clvls, cach, lbd, outl,
stats, _, vdom, avdom, lcount, opts). RETURN lcount)›
by auto
text ‹
I also played with \<^term>‹ema_reinit fast_ema› and \<^term>‹ema_reinit slow_ema›. Currently removed,
to test the performance, I remove it.
›
definition incr_restart_stat :: ‹twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹incr_restart_stat = (λ(M, N, D, Q, W, vm, clvls, cach, lbd, outl, stats, (fast_ema, slow_ema,
res_info, wasted), vdom, avdom, lcount). do{
RETURN (M, N, D, Q, W, vm, clvls, cach, lbd, outl, incr_restart stats,
(fast_ema, slow_ema,
restart_info_restart_done res_info, wasted), vdom, avdom, lcount)
})›
definition incr_lrestart_stat :: ‹twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹incr_lrestart_stat = (λ(M, N, D, Q, W, vm, clvls, cach, lbd, outl, stats, (fast_ema, slow_ema,
res_info, wasted), vdom, avdom, lcount). do{
RETURN (M, N, D, Q, W, vm, clvls, cach, lbd, outl, incr_lrestart stats,
(fast_ema, slow_ema, restart_info_restart_done res_info, wasted),
vdom, avdom, lcount)
})›
definition incr_wasted_st :: ‹64 word ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur› where
‹incr_wasted_st = (λwaste (M, N, D, Q, W, vm, clvls, cach, lbd, outl, stats, (fast_ema, slow_ema,
res_info, wasted, φ), vdom, avdom, lcount). do{
(M, N, D, Q, W, vm, clvls, cach, lbd, outl, stats,
(fast_ema, slow_ema, res_info, wasted+waste, φ),
vdom, avdom, lcount)
})›
definition wasted_bytes_st :: ‹twl_st_wl_heur ⇒ 64 word› where
‹wasted_bytes_st = (λ(M, N, D, Q, W, vm, clvls, cach, lbd, outl, stats, (fast_ema, slow_ema,
res_info, wasted, φ), vdom, avdom, lcount).
wasted)›
definition opts_restart_st :: ‹twl_st_wl_heur ⇒ bool› where
‹opts_restart_st = (λ(M', N', D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, _). (opts_restart opts))›
definition opts_reduction_st :: ‹twl_st_wl_heur ⇒ bool› where
‹opts_reduction_st = (λ(M, N0, D, Q, W, vm, clvls, cach, lbd, outl,
stats, heur, vdom, avdom, lcount, opts, _). (opts_reduce opts))›
definition isasat_length_trail_st :: ‹twl_st_wl_heur ⇒ nat› where
‹isasat_length_trail_st S = isa_length_trail (get_trail_wl_heur S)›
lemma isasat_length_trail_st_alt_def:
‹isasat_length_trail_st = (λ(M, _). isa_length_trail M)›
by (auto simp: isasat_length_trail_st_def intro!: ext)
definition get_pos_of_level_in_trail_imp_st :: ‹twl_st_wl_heur ⇒ nat ⇒ nat nres› where
‹get_pos_of_level_in_trail_imp_st S = get_pos_of_level_in_trail_imp (get_trail_wl_heur S)›
lemma get_pos_of_level_in_trail_imp_alt_def:
‹get_pos_of_level_in_trail_imp_st = (λ(M, _) L. do {k ← get_pos_of_level_in_trail_imp M L; RETURN k})›
by (auto simp: get_pos_of_level_in_trail_imp_st_def intro!: ext)
definition mop_clause_not_marked_to_delete_heur :: ‹_ ⇒ nat ⇒ bool nres›
where
‹mop_clause_not_marked_to_delete_heur S C = do {
ASSERT(clause_not_marked_to_delete_heur_pre (S, C));
RETURN (clause_not_marked_to_delete_heur S C)
}›
definition mop_arena_lbd_st where
‹mop_arena_lbd_st S =
mop_arena_lbd (get_clauses_wl_heur S)›
lemma mop_arena_lbd_st_alt_def:
‹mop_arena_lbd_st = (λ(M', arena, D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena) C. do {
ASSERT(get_clause_LBD_pre arena C);
RETURN(arena_lbd arena C)
})›
unfolding mop_arena_lbd_st_def mop_arena_lbd_def
by (auto intro!: ext)
definition mop_arena_status_st where
‹mop_arena_status_st S =
mop_arena_status (get_clauses_wl_heur S)›
lemma mop_arena_status_st_alt_def:
‹mop_arena_status_st = (λ(M', arena, D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena) C. do {
ASSERT(arena_is_valid_clause_vdom arena C);
RETURN(arena_status arena C)
})›
unfolding mop_arena_status_st_def mop_arena_status_def
by (auto intro!: ext)
definition mop_marked_as_used_st :: ‹twl_st_wl_heur ⇒ nat ⇒ bool nres› where
‹mop_marked_as_used_st S =
mop_marked_as_used (get_clauses_wl_heur S)›
lemma mop_marked_as_used_st_alt_def:
‹mop_marked_as_used_st = (λ(M', arena, D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena) C. do {
ASSERT(marked_as_used_pre arena C);
RETURN(marked_as_used arena C)
})›
unfolding mop_marked_as_used_st_def mop_marked_as_used_def
by (auto intro!: ext)
definition mop_arena_length_st :: ‹twl_st_wl_heur ⇒ nat ⇒ nat nres› where
‹mop_arena_length_st S =
mop_arena_length (get_clauses_wl_heur S)›
lemma mop_arena_length_st_alt_def:
‹mop_arena_length_st = (λ(M', arena, D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena) C. do {
ASSERT(arena_is_valid_clause_idx arena C);
RETURN (arena_length arena C)
})›
unfolding mop_arena_length_st_def mop_arena_length_def
by (auto intro!: ext)
definition full_arena_length_st :: ‹twl_st_wl_heur ⇒ nat› where
‹full_arena_length_st = (λ(M', arena, D', j, W', vm, clvls, cach, lbd, outl, stats, heur,
vdom, avdom, lcount, opts, old_arena). length arena)›
definition (in -) access_lit_in_clauses where
‹access_lit_in_clauses S i j = (get_clauses_wl S) ∝ i ! j›
lemma twl_st_heur_get_clauses_access_lit[simp]:
‹(S, T) ∈ twl_st_heur ⟹ C ∈# dom_m (get_clauses_wl T) ⟹
i < length (get_clauses_wl T ∝ C) ⟹
get_clauses_wl T ∝ C ! i = access_lit_in_clauses_heur S C i›
for S T C i
by (cases S; cases T)
(auto simp: arena_lifting twl_st_heur_def access_lit_in_clauses_heur_def)
text ‹In an attempt to avoid using @{thm ac_simps} everywhere.›
lemma all_lits_simps[simp]:
‹all_lits N ((NE + UE) + (NS + US)) = all_lits N (NE + UE + NS + US)›
‹all_atms N ((NE + UE) + (NS + US)) = all_atms N (NE + UE + NS + US)›
by (auto simp: ac_simps)
lemma clause_not_marked_to_delete_heur_alt_def:
‹RETURN ∘∘ clause_not_marked_to_delete_heur = (λ(M, arena, D, oth) C.
RETURN (arena_status arena C ≠ DELETED))›
unfolding clause_not_marked_to_delete_heur_def by (auto intro!: ext)
end