theory IsaSAT_VMTF
imports Watched_Literals.WB_Sort IsaSAT_Setup
begin
chapter ‹Decision heuristic›
section ‹Code generation for the VMTF decision heuristic and the trail›
definition update_next_search where
‹update_next_search L = (λ((ns, m, fst_As, lst_As, next_search), to_remove).
((ns, m, fst_As, lst_As, L), to_remove))›
definition vmtf_enqueue_pre where
‹vmtf_enqueue_pre =
(λ((M, L),(ns,m,fst_As,lst_As, next_search)). L < length ns ∧
(fst_As ≠ None ⟶ the fst_As < length ns) ∧
(fst_As ≠ None ⟶ lst_As ≠ None) ∧
m+1 ≤ uint64_max)›
definition isa_vmtf_enqueue :: ‹trail_pol ⇒ nat ⇒ vmtf_option_fst_As ⇒ vmtf nres› where
‹isa_vmtf_enqueue = (λM L (ns, m, fst_As, lst_As, next_search). do {
ASSERT(defined_atm_pol_pre M L);
de ← RETURN (defined_atm_pol M L);
case fst_As of
None ⇒RETURN ((ns[L := VMTF_Node m fst_As None], m+1, L, L,
(if de then None else Some L)))
| Some fst_As ⇒ do {
let fst_As' = VMTF_Node (stamp (ns!fst_As)) (Some L) (get_next (ns!fst_As));
RETURN (ns[L := VMTF_Node (m+1) None (Some fst_As), fst_As := fst_As'],
m+1, L, the lst_As, (if de then next_search else Some L))
}})›
lemma vmtf_enqueue_alt_def:
‹RETURN ooo vmtf_enqueue = (λM L (ns, m, fst_As, lst_As, next_search). do {
let de = defined_lit M (Pos L);
case fst_As of
None ⇒ RETURN (ns[L := VMTF_Node m fst_As None], m+1, L, L,
(if de then None else Some L))
| Some fst_As ⇒
let fst_As' = VMTF_Node (stamp (ns!fst_As)) (Some L) (get_next (ns!fst_As)) in
RETURN (ns[L := VMTF_Node (m+1) None (Some fst_As), fst_As := fst_As'],
m+1, L, the lst_As, (if de then next_search else Some L))})›
unfolding vmtf_enqueue_def Let_def
by (auto intro!: ext split: option.splits)
lemma isa_vmtf_enqueue:
‹(uncurry2 isa_vmtf_enqueue, uncurry2 (RETURN ooo vmtf_enqueue)) ∈
[λ((M, L), _). L ∈# 𝒜]⇩f (trail_pol 𝒜) ×⇩f nat_rel ×⇩f Id → ⟨Id⟩nres_rel›
proof -
have defined_atm_pol: ‹(defined_atm_pol x1g x2f, defined_lit x1a (Pos x2)) ∈ Id›
if
‹case y of (x, xa) ⇒ (case x of (M, L) ⇒ λ_. L ∈# 𝒜) xa› and
‹(x, y) ∈ trail_pol 𝒜 ×⇩f nat_rel ×⇩f Id› and ‹x1 = (x1a, x2)› and
‹x2d = (x1e, x2e)› and
‹x2c = (x1d, x2d)› and
‹x2b = (x1c, x2c)› and
‹x2a = (x1b, x2b)› and
‹y = (x1, x2a)› and
‹x1f = (x1g, x2f)› and
‹x2j = (x1k, x2k)› and
‹x2i = (x1j, x2j)› and
‹x2h = (x1i, x2i)› and
‹x2g = (x1h, x2h)› and
‹x = (x1f, x2g)›
for x y x1 x1a x2 x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x1g x2f x2g x1h x2h
x1i x2i x1j x2j x1k x2k
proof -
have [simp]: ‹defined_lit x1a (Pos x2) ⟷ defined_atm x1a x2›
using that by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n trail_pol_def defined_atm_def)
show ?thesis
using undefined_atm_code[THEN fref_to_Down, unfolded uncurry_def, of 𝒜 ‹(x1a, x2)› ‹(x1g, x2f)›]
that by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n RETURN_def)
qed
show ?thesis
unfolding isa_vmtf_enqueue_def vmtf_enqueue_alt_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg)
subgoal by (rule defined_atm_pol_pre) auto
apply (rule defined_atm_pol; assumption)
apply (rule same_in_Id_option_rel)
subgoal for x y x1 x1a x2 x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x1g x2f x2g x1h x2h
x1i x2i x1j x2j x1k x2k
by auto
subgoal by auto
subgoal by auto
done
qed
definition partition_vmtf_nth :: ‹nat_vmtf_node list ⇒ nat ⇒ nat ⇒ nat list ⇒ (nat list × nat) nres› where
‹partition_vmtf_nth ns = partition_main (≤) (λn. stamp (ns ! n))›
definition partition_between_ref_vmtf :: ‹nat_vmtf_node list ⇒ nat ⇒ nat ⇒ nat list ⇒ (nat list × nat) nres› where
‹partition_between_ref_vmtf ns = partition_between_ref (≤) (λn. stamp (ns ! n))›
definition quicksort_vmtf_nth :: ‹nat_vmtf_node list × 'c ⇒ nat list ⇒ nat list nres› where
‹quicksort_vmtf_nth = (λ(ns, _). full_quicksort_ref (≤) (λn. stamp (ns ! n)))›
definition quicksort_vmtf_nth_ref:: ‹nat_vmtf_node list ⇒ nat ⇒ nat ⇒ nat list ⇒ nat list nres› where
‹quicksort_vmtf_nth_ref ns a b c =
quicksort_ref (≤) (λn. stamp (ns ! n)) (a, b, c)›
lemma (in -) partition_vmtf_nth_code_helper:
assumes ‹∀x∈set ba. x < length a› and
‹b < length ba› and
mset: ‹mset ba = mset a2'› and
‹a1' < length a2'›
shows ‹a2' ! b < length a›
using nth_mem[of b a2'] mset_eq_setD[OF mset] mset_eq_length[OF mset] assms
by (auto simp del: nth_mem)
lemma partition_vmtf_nth_code_helper3:
‹∀x∈set b. x < length a ⟹
x'e < length a2' ⟹
mset a2' = mset b ⟹
a2' ! x'e < length a›
using mset_eq_setD nth_mem by blast
definition (in -) isa_vmtf_en_dequeue :: ‹trail_pol ⇒ nat ⇒ vmtf ⇒ vmtf nres› where
‹isa_vmtf_en_dequeue = (λM L vm. isa_vmtf_enqueue M L (vmtf_dequeue L vm))›
lemma isa_vmtf_en_dequeue:
‹(uncurry2 isa_vmtf_en_dequeue, uncurry2 (RETURN ooo vmtf_en_dequeue)) ∈
[λ((M, L), _). L ∈# 𝒜]⇩f (trail_pol 𝒜) ×⇩f nat_rel ×⇩f Id → ⟨Id⟩nres_rel›
unfolding isa_vmtf_en_dequeue_def vmtf_en_dequeue_def uncurry_def
apply (intro frefI nres_relI)
apply clarify
subgoal for a aa ab ac ad b ba ae af ag ah bb ai bc aj ak al am bd
by (rule order.trans,
rule isa_vmtf_enqueue[of 𝒜, THEN fref_to_Down_curry2,
of ai bc ‹vmtf_dequeue bc (aj, ak, al, am, bd)›])
auto
done
definition isa_vmtf_en_dequeue_pre :: ‹(trail_pol × nat) × vmtf ⇒ bool› where
‹isa_vmtf_en_dequeue_pre = (λ((M, L),(ns,m,fst_As, lst_As, next_search)).
L < length ns ∧ vmtf_dequeue_pre (L, ns) ∧
fst_As < length ns ∧ (get_next (ns ! fst_As) ≠ None ⟶ get_prev (ns ! lst_As) ≠ None) ∧
(get_next (ns ! fst_As) = None ⟶ fst_As = lst_As) ∧
m+1 ≤ uint64_max)›
lemma isa_vmtf_en_dequeue_preD:
assumes ‹isa_vmtf_en_dequeue_pre ((M, ah), a, aa, ab, ac, b)›
shows ‹ah < length a› and ‹vmtf_dequeue_pre (ah, a)›
using assms by (auto simp: isa_vmtf_en_dequeue_pre_def)
lemma isa_vmtf_en_dequeue_pre_vmtf_enqueue_pre:
‹isa_vmtf_en_dequeue_pre ((M, L), a, st, fst_As, lst_As, next_search) ⟹
vmtf_enqueue_pre ((M, L), vmtf_dequeue L (a, st, fst_As, lst_As, next_search))›
unfolding vmtf_enqueue_pre_def
apply clarify
apply (intro conjI)
subgoal
by (auto simp: vmtf_dequeue_pre_def vmtf_enqueue_pre_def vmtf_dequeue_def
ns_vmtf_dequeue_def Let_def isa_vmtf_en_dequeue_pre_def split: option.splits)[]
subgoal
by (auto simp: vmtf_dequeue_pre_def vmtf_enqueue_pre_def vmtf_dequeue_def
isa_vmtf_en_dequeue_pre_def split: option.splits if_splits)[]
subgoal
by (auto simp: vmtf_dequeue_pre_def vmtf_enqueue_pre_def vmtf_dequeue_def
Let_def isa_vmtf_en_dequeue_pre_def split: option.splits if_splits)[]
subgoal
by (auto simp: vmtf_dequeue_pre_def vmtf_enqueue_pre_def vmtf_dequeue_def
Let_def isa_vmtf_en_dequeue_pre_def split: option.splits if_splits)[]
done
lemma insert_sort_reorder_list:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹(full_quicksort_ref R h, reorder_list vm) ∈ ⟨Id⟩list_rel →⇩f ⟨Id⟩ nres_rel›
proof -
show ?thesis
apply (intro frefI nres_relI)
apply (rule full_quicksort_ref_full_quicksort[THEN fref_to_Down, THEN order_trans])
using assms apply fast
using assms apply fast
apply fast
apply assumption
using assms
apply (auto 5 5 simp: reorder_list_def intro!: full_quicksort_correct[THEN order_trans])
done
qed
lemma quicksort_vmtf_nth_reorder:
‹(uncurry quicksort_vmtf_nth, uncurry reorder_list) ∈
Id ×⇩r ⟨Id⟩list_rel →⇩f ⟨Id⟩ nres_rel›
apply (intro WB_More_Refinement.frefI nres_relI)
subgoal for x y
using insert_sort_reorder_list[unfolded fref_def nres_rel_def, of
‹(≤)› ‹(λn. stamp (fst (fst y) ! n) :: nat)› ‹fst y›]
by (cases x, cases y)
(fastforce simp: quicksort_vmtf_nth_def uncurry_def WB_More_Refinement.fref_def)
done
lemma atoms_hash_del_op_set_delete:
‹(uncurry (RETURN oo atoms_hash_del),
uncurry (RETURN oo Set.remove)) ∈
nat_rel ×⇩r atoms_hash_rel 𝒜 →⇩f ⟨atoms_hash_rel 𝒜⟩nres_rel›
by (intro frefI nres_relI)
(force simp: atoms_hash_del_def atoms_hash_rel_def)
definition current_stamp where
‹current_stamp vm = fst (snd vm)›
lemma current_stamp_alt_def:
‹current_stamp = (λ(_, m, _). m)›
by (auto simp: current_stamp_def intro!: ext)
lemma vmtf_rescale_alt_def:
‹vmtf_rescale = (λ(ns, m, fst_As, lst_As :: nat, next_search). do {
(ns, m, _) ← WHILE⇩T⇗λ_. True⇖
(λ(ns, n, lst_As). lst_As ≠None)
(λ(ns, n, a). do {
ASSERT(a ≠ None);
ASSERT(n+1 ≤ uint32_max);
ASSERT(the a < length ns);
let m = the a;
let c = ns ! m;
let nc = get_next c;
let pc = get_prev c;
RETURN (ns[m := VMTF_Node n pc nc], n + 1, pc)
})
(ns, 0, Some lst_As);
RETURN ((ns, m, fst_As, lst_As, next_search))
})›
unfolding update_stamp.simps Let_def vmtf_rescale_def by auto
definition vmtf_reorder_list_raw where
‹vmtf_reorder_list_raw = (λvm to_remove. do {
ASSERT(∀x∈set to_remove. x < length vm);
reorder_list vm to_remove
})›
definition vmtf_reorder_list where
‹vmtf_reorder_list = (λ(vm, _) to_remove. do {
vmtf_reorder_list_raw vm to_remove
})›
definition isa_vmtf_flush_int :: ‹trail_pol ⇒ _ ⇒ _ nres› where
‹isa_vmtf_flush_int = (λM (vm, (to_remove, h)). do {
ASSERT(∀x∈set to_remove. x < length (fst vm));
ASSERT(length to_remove ≤ uint32_max);
to_remove' ← vmtf_reorder_list vm to_remove;
ASSERT(length to_remove' ≤ uint32_max);
vm ← (if length to_remove' ≥ uint64_max - fst (snd vm)
then vmtf_rescale vm else RETURN vm);
ASSERT(length to_remove' + fst (snd vm) ≤ uint64_max);
(_, vm, h) ← WHILE⇩T⇗λ(i, vm', h). i ≤ length to_remove' ∧ fst (snd vm') = i + fst (snd vm) ∧
(i < length to_remove' ⟶ isa_vmtf_en_dequeue_pre ((M, to_remove'!i), vm'))⇖
(λ(i, vm, h). i < length to_remove')
(λ(i, vm, h). do {
ASSERT(i < length to_remove');
ASSERT(isa_vmtf_en_dequeue_pre ((M, to_remove'!i), vm));
vm ← isa_vmtf_en_dequeue M (to_remove'!i) vm;
ASSERT(atoms_hash_del_pre (to_remove'!i) h);
RETURN (i+1, vm, atoms_hash_del (to_remove'!i) h)})
(0, vm, h);
RETURN (vm, (emptied_list to_remove', h))
})›
lemma isa_vmtf_flush_int:
‹(uncurry isa_vmtf_flush_int, uncurry (vmtf_flush_int 𝒜)) ∈ trail_pol 𝒜 ×⇩f Id →⇩f ⟨Id⟩nres_rel›
proof -
have vmtf_flush_int_alt_def:
‹vmtf_flush_int 𝒜⇩i⇩n = (λM (vm, (to_remove, h)). do {
ASSERT(∀x∈set to_remove. x < length (fst vm));
ASSERT(length to_remove ≤ uint32_max);
to_remove' ← reorder_list vm to_remove;
ASSERT(length to_remove' ≤ uint32_max);
vm ← (if length to_remove' + fst (snd vm) ≥ uint64_max
then vmtf_rescale vm else RETURN vm);
ASSERT(length to_remove' + fst (snd vm) ≤ uint64_max);
(_, vm, h) ← WHILE⇩T⇗λ(i, vm', h). i ≤ length to_remove' ∧ fst (snd vm') = i + fst (snd vm) ∧
(i < length to_remove' ⟶ vmtf_en_dequeue_pre 𝒜⇩i⇩n ((M, to_remove'!i), vm'))⇖
(λ(i, vm, h). i < length to_remove')
(λ(i, vm, h). do {
ASSERT(i < length to_remove');
ASSERT(to_remove'!i ∈# 𝒜⇩i⇩n);
ASSERT(atoms_hash_del_pre (to_remove'!i) h);
vm ← RETURN(vmtf_en_dequeue M (to_remove'!i) vm);
RETURN (i+1, vm, atoms_hash_del (to_remove'!i) h)})
(0, vm, h);
RETURN (vm, (emptied_list to_remove', h))
})› for 𝒜⇩i⇩n
unfolding vmtf_flush_int_def
by auto
have reorder_list: ‹vmtf_reorder_list x1d x1e
≤ ⇓ Id
(reorder_list x1a x1b)›
if
‹(x, y) ∈ trail_pol 𝒜 ×⇩f Id› and ‹x2a = (x1b, x2b)› and
‹x2 = (x1a, x2a)› and
‹y = (x1, x2)› and
‹x2d = (x1e, x2e)› and
‹x2c = (x1d, x2d)› and
‹x = (x1c, x2c)› and
‹∀x∈set x1b. x < length (fst x1a)› and
‹length x1b ≤ uint32_max› and
‹∀x∈set x1e. x < length (fst x1d)› and
‹length x1e ≤ uint32_max›
for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e
using that unfolding vmtf_reorder_list_def by (cases x1a)
(auto intro!: ASSERT_leI simp: reorder_list_def vmtf_reorder_list_raw_def)
have vmtf_rescale: ‹vmtf_rescale x1d
≤ ⇓ Id
(vmtf_rescale x1a)›
if
‹True› and
‹(x, y) ∈ trail_pol 𝒜 ×⇩f Id› and ‹x2a = (x1b, x2b)› and
‹x2 = (x1a, x2a)› and
‹y = (x1, x2)› and
‹x2d = (x1e, x2e)› and
‹x2c = (x1d, x2d)› and
‹x = (x1c, x2c)› and
‹∀x∈set x1b. x < length (fst x1a)› and
‹length x1b ≤ uint32_max› and
‹∀x∈set x1e. x < length (fst x1d)› and
‹length x1e ≤ uint32_max› and
‹(to_remove', to_remove'a) ∈ Id› and
‹length to_remove'a ≤ uint32_max› and
‹length to_remove' ≤ uint32_max› and
‹uint64_max ≤ length to_remove'a + fst (snd x1a)›
for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e to_remove' to_remove'a
using that by auto
have loop_rel: ‹((0, vm, x2e), 0, vma, x2b) ∈ Id›
if
‹(x, y) ∈ trail_pol 𝒜 ×⇩f Id› and
‹x2a = (x1b, x2b)› and
‹x2 = (x1a, x2a)› and
‹y = (x1, x2)› and
‹x2d = (x1e, x2e)› and
‹x2c = (x1d, x2d)› and
‹x = (x1c, x2c)› and
‹∀x∈set x1b. x < length (fst x1a)› and
‹length x1b ≤ uint32_max› and
‹∀x∈set x1e. x < length (fst x1d)› and
‹length x1e ≤ uint32_max› and
‹(to_remove', to_remove'a) ∈ Id› and
‹length to_remove'a ≤ uint32_max› and
‹length to_remove' ≤ uint32_max› and
‹(vm, vma) ∈ Id› and
‹length to_remove'a + fst (snd vma) ≤ uint64_max›
‹case (0, vma, x2b) of
(i, vm', h) ⇒
i ≤ length to_remove'a ∧
fst (snd vm') = i + fst (snd vma) ∧
(i < length to_remove'a ⟶
vmtf_en_dequeue_pre 𝒜 ((x1, to_remove'a ! i), vm'))›
for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e to_remove' to_remove'a vm
vma
using that by auto
have isa_vmtf_en_dequeue_pre:
‹vmtf_en_dequeue_pre 𝒜 ((M, L), x) ⟹ isa_vmtf_en_dequeue_pre ((M', L), x)› for x M M' L
unfolding vmtf_en_dequeue_pre_def isa_vmtf_en_dequeue_pre_def
by auto
have isa_vmtf_en_dequeue: ‹isa_vmtf_en_dequeue x1c (to_remove' ! x1h) x1i
≤ SPEC
(λc. (c, vmtf_en_dequeue x1 (to_remove'a ! x1f) x1g)
∈ Id)›
if
‹(x, y) ∈ trail_pol 𝒜 ×⇩f Id› and
‹∀x∈set x1b. x < length (fst x1a)› and
‹length x1b ≤ uint32_max› and
‹∀x∈set x1e. x < length (fst x1d)› and
‹length x1e ≤ uint32_max› and
‹length to_remove'a ≤ uint32_max› and
‹length to_remove' ≤ uint32_max› and
‹length to_remove'a + fst (snd vma) ≤ uint64_max› and
‹case xa of (i, vm, h) ⇒ i < length to_remove'› and
‹case x' of (i, vm, h) ⇒ i < length to_remove'a› and
‹case xa of
(i, vm', h) ⇒
i ≤ length to_remove' ∧
fst (snd vm') = i + fst (snd vm) ∧
(i < length to_remove' ⟶
isa_vmtf_en_dequeue_pre ((x1c, to_remove' ! i), vm'))› and
‹case x' of
(i, vm', h) ⇒
i ≤ length to_remove'a ∧
fst (snd vm') = i + fst (snd vma) ∧
(i < length to_remove'a ⟶
vmtf_en_dequeue_pre 𝒜 ((x1, to_remove'a ! i), vm'))› and
‹isa_vmtf_en_dequeue_pre ((x1c, to_remove' ! x1h), x1i)› and
‹x1f < length to_remove'a› and
‹to_remove'a ! x1f ∈# 𝒜› and
‹x1h < length to_remove'› and
‹x2a = (x1b, x2b)› and
‹x2 = (x1a, x2a)› and
‹y = (x1, x2)› and
‹x = (x1c, x2c)› and
‹x2d = (x1e, x2e)› and
‹x2c = (x1d, x2d)› and
‹x2f = (x1g, x2g)› and
‹x' = (x1f, x2f)› and
‹x2h = (x1i, x2i)› and
‹xa = (x1h, x2h)› and
‹(to_remove', to_remove'a) ∈ Id› and
‹(xa, x') ∈ Id› and
‹(vm, vma) ∈ Id›
for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e to_remove' to_remove'a vm
vma xa x' x1f x2f x1g x2g x1h x2h x1i and x2i :: ‹bool list›
using isa_vmtf_en_dequeue[of 𝒜, THEN fref_to_Down_curry2, of x1 ‹to_remove'a ! x1f› x1g
x1c ‹to_remove' ! x1h› x1i] that
by (auto simp: RETURN_def)
show ?thesis
unfolding isa_vmtf_flush_int_def uncurry_def vmtf_flush_int_alt_def
apply (intro frefI nres_relI)
apply (refine_rcg)
subgoal
by auto
subgoal
by auto
apply (rule reorder_list; assumption)
subgoal
by auto
subgoal
by auto
apply (rule vmtf_rescale; assumption)
subgoal
by auto
subgoal
by auto
apply (rule loop_rel; assumption)
subgoal
by auto
subgoal
by auto
subgoal
by (auto intro!: isa_vmtf_en_dequeue_pre)
subgoal
by auto
subgoal
by auto
subgoal
by auto
apply (rule isa_vmtf_en_dequeue; assumption)
subgoal for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e to_remove' to_remove'a vm
vma xa x' x1f x2f x1g x2g x1h x2h x1i x2i vmb vmc
by auto
subgoal
by auto
subgoal
by auto
done
qed
definition atms_hash_insert_pre :: ‹nat ⇒ nat list × bool list ⇒ bool› where
‹atms_hash_insert_pre i = (λ(n, xs). i < length xs ∧ (¬xs!i ⟶ length n < 2 + uint32_max div 2))›
definition atoms_hash_insert :: ‹nat ⇒ nat list × bool list ⇒ (nat list × bool list)› where
‹atoms_hash_insert i = (λ(n, xs). if xs ! i then (n, xs) else (n @ [i], xs[i := True]))›
lemma bounded_included_le:
assumes bounded: ‹isasat_input_bounded 𝒜› and ‹distinct n› and
‹set n ⊆ set_mset 𝒜 ›
shows ‹length n < uint32_max› ‹length n ≤ 1 + uint32_max div 2›
proof -
have lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (Pos `# mset n)› and
dist: ‹distinct n›
using assms
by (auto simp: literals_are_in_ℒ⇩i⇩n_alt_def distinct_atoms_rel_alt_def inj_on_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
have dist: ‹distinct_mset (Pos `# mset n)›
by (subst distinct_image_mset_inj)
(use dist in ‹auto simp: inj_on_def›)
have tauto: ‹¬ tautology (poss (mset n))›
by (auto simp: tautology_decomp)
show ‹length n < uint32_max› ‹length n ≤ 1 + uint32_max div 2›
using simple_clss_size_upper_div2[OF bounded lits dist tauto]
by (auto simp: uint32_max_def)
qed
lemma atms_hash_insert_pre:
assumes ‹L ∈# 𝒜› and ‹(x, x') ∈ distinct_atoms_rel 𝒜› and ‹isasat_input_bounded 𝒜›
shows ‹atms_hash_insert_pre L x›
using assms bounded_included_le[OF assms(3), of ‹L # fst x›]
by (auto simp: atoms_hash_insert_def atoms_hash_rel_def distinct_atoms_rel_alt_def
atms_hash_insert_pre_def)
lemma atoms_hash_del_op_set_insert:
‹(uncurry (RETURN oo atoms_hash_insert),
uncurry (RETURN oo insert)) ∈
[λ(i, xs). i ∈# 𝒜⇩i⇩n ∧ isasat_input_bounded 𝒜]⇩f
nat_rel ×⇩r distinct_atoms_rel 𝒜⇩i⇩n → ⟨distinct_atoms_rel 𝒜⇩i⇩n⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: atoms_hash_insert_def atoms_hash_rel_def distinct_atoms_rel_alt_def intro!: ASSERT_leI)
definition (in -) atoms_hash_set_member where
‹atoms_hash_set_member i xs = do {ASSERT(i < length xs); RETURN (xs ! i)}›
definition isa_vmtf_mark_to_rescore
:: ‹nat ⇒ isa_vmtf_remove_int ⇒ isa_vmtf_remove_int›
where
‹isa_vmtf_mark_to_rescore L = (λ((ns, m, fst_As, next_search), to_remove).
((ns, m, fst_As, next_search), atoms_hash_insert L to_remove))›
definition isa_vmtf_mark_to_rescore_pre where
‹isa_vmtf_mark_to_rescore_pre = (λL ((ns, m, fst_As, next_search), to_remove).
atms_hash_insert_pre L to_remove)›
lemma isa_vmtf_mark_to_rescore_vmtf_mark_to_rescore:
‹(uncurry (RETURN oo isa_vmtf_mark_to_rescore), uncurry (RETURN oo vmtf_mark_to_rescore)) ∈
[λ(L, vm). L∈# 𝒜⇩i⇩n ∧ isasat_input_bounded 𝒜⇩i⇩n]⇩f Id ×⇩f (Id ×⇩r distinct_atoms_rel 𝒜⇩i⇩n) →
⟨Id ×⇩r distinct_atoms_rel 𝒜⇩i⇩n⟩nres_rel›
unfolding isa_vmtf_mark_to_rescore_def vmtf_mark_to_rescore_def
by (intro frefI nres_relI)
(auto intro!: atoms_hash_del_op_set_insert[THEN fref_to_Down_unRET_uncurry])
definition (in -) isa_vmtf_unset :: ‹nat ⇒ isa_vmtf_remove_int ⇒ isa_vmtf_remove_int› where
‹isa_vmtf_unset = (λL ((ns, m, fst_As, lst_As, next_search), to_remove).
(if next_search = None ∨ stamp (ns ! (the next_search)) < stamp (ns ! L)
then ((ns, m, fst_As, lst_As, Some L), to_remove)
else ((ns, m, fst_As, lst_As, next_search), to_remove)))›
definition vmtf_unset_pre where
‹vmtf_unset_pre = (λL ((ns, m, fst_As, lst_As, next_search), to_remove).
L < length ns ∧ (next_search ≠ None ⟶ the next_search < length ns))›
lemma vmtf_unset_pre_vmtf:
assumes
‹((ns, m, fst_As, lst_As, next_search), to_remove) ∈ vmtf 𝒜 M› and
‹L ∈# 𝒜›
shows ‹vmtf_unset_pre L ((ns, m, fst_As, lst_As, next_search), to_remove)›
using assms
by (auto simp: vmtf_def vmtf_unset_pre_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
lemma vmtf_unset_pre:
assumes
‹((ns, m, fst_As, lst_As, next_search), to_remove) ∈ isa_vmtf 𝒜 M› and
‹L ∈# 𝒜›
shows ‹vmtf_unset_pre L ((ns, m, fst_As, lst_As, next_search), to_remove)›
using assms vmtf_unset_pre_vmtf[of ns m fst_As lst_As next_search _ 𝒜 M L]
unfolding isa_vmtf_def vmtf_unset_pre_def
by auto
lemma vmtf_unset_pre':
assumes
‹vm ∈ isa_vmtf 𝒜 M› and
‹L ∈# 𝒜›
shows ‹vmtf_unset_pre L vm›
using assms by (cases vm) (auto dest: vmtf_unset_pre)
definition isa_vmtf_mark_to_rescore_and_unset :: ‹nat ⇒ isa_vmtf_remove_int ⇒ isa_vmtf_remove_int›
where
‹isa_vmtf_mark_to_rescore_and_unset L M = isa_vmtf_mark_to_rescore L (isa_vmtf_unset L M)›
definition isa_vmtf_mark_to_rescore_and_unset_pre where
‹isa_vmtf_mark_to_rescore_and_unset_pre = (λ(L, ((ns, m, fst_As, lst_As, next_search), tor)).
vmtf_unset_pre L ((ns, m, fst_As, lst_As, next_search), tor) ∧
atms_hash_insert_pre L tor)›
lemma size_conflict_int_size_conflict:
‹(RETURN o size_conflict_int, RETURN o size_conflict) ∈ [λD. D ≠ None]⇩f option_lookup_clause_rel 𝒜 →
⟨nat_rel⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: size_conflict_int_def size_conflict_def option_lookup_clause_rel_def
lookup_clause_rel_def)
definition rescore_clause
:: ‹nat multiset ⇒ nat clause_l ⇒ (nat,nat)ann_lits ⇒ vmtf_remove_int ⇒
(vmtf_remove_int) nres›
where
‹rescore_clause 𝒜 C M vm = SPEC (λ(vm'). vm' ∈ vmtf 𝒜 M)›
lemma isa_vmtf_unset_vmtf_unset:
‹(uncurry (RETURN oo isa_vmtf_unset), uncurry (RETURN oo vmtf_unset)) ∈
nat_rel ×⇩f (Id ×⇩r distinct_atoms_rel 𝒜) →⇩f
⟨(Id ×⇩r distinct_atoms_rel 𝒜)⟩nres_rel›
unfolding vmtf_unset_def isa_vmtf_unset_def uncurry_def
by (intro frefI nres_relI) auto
lemma isa_vmtf_unset_isa_vmtf:
assumes ‹vm ∈ isa_vmtf 𝒜 M› and ‹L ∈# 𝒜›
shows ‹isa_vmtf_unset L vm ∈ isa_vmtf 𝒜 M›
proof -
obtain vm0 to_remove to_remove' where
vm: ‹vm = (vm0, to_remove)› and
vm0: ‹(vm0, to_remove') ∈ vmtf 𝒜 M› and
‹(to_remove, to_remove') ∈ distinct_atoms_rel 𝒜›
using assms by (cases vm) (auto simp: isa_vmtf_def)
then show ?thesis
using assms
isa_vmtf_unset_vmtf_unset[of 𝒜, THEN fref_to_Down_unRET_uncurry, of L vm L ‹(vm0, to_remove')›]
abs_vmtf_ns_unset_vmtf_unset[of ‹fst vm0› ‹fst (snd vm0)› ‹fst (snd (snd vm0))›
‹fst (snd (snd (snd vm0)))› ‹snd (snd (snd (snd vm0)))› to_remove' 𝒜 M L to_remove']
by (auto simp: vm atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n intro: isa_vmtfI elim!: prod_relE)
qed
lemma isa_vmtf_tl_isa_vmtf:
assumes ‹vm ∈ isa_vmtf 𝒜 M› and ‹M ≠ []› and ‹lit_of (hd M) ∈# ℒ⇩a⇩l⇩l 𝒜› and
‹L = (atm_of (lit_of (hd M)))›
shows ‹isa_vmtf_unset L vm ∈ isa_vmtf 𝒜 (tl M)›
proof -
let ?L = ‹atm_of (lit_of (hd M))›
obtain vm0 to_remove to_remove' where
vm: ‹vm = (vm0, to_remove)› and
vm0: ‹(vm0, to_remove') ∈ vmtf 𝒜 M› and
‹(to_remove, to_remove') ∈ distinct_atoms_rel 𝒜›
using assms by (cases vm) (auto simp: isa_vmtf_def)
then show ?thesis
using assms
isa_vmtf_unset_vmtf_unset[of 𝒜, THEN fref_to_Down_unRET_uncurry, of ?L vm ?L ‹(vm0, to_remove')›]
vmtf_unset_vmtf_tl[of ‹fst vm0› ‹fst (snd vm0)› ‹fst (snd (snd vm0))›
‹fst (snd (snd (snd vm0)))› ‹snd (snd (snd (snd vm0)))› to_remove' 𝒜 M]
by (cases M)
(auto simp: vm atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n intro: isa_vmtfI elim!: prod_relE)
qed
definition isa_vmtf_find_next_undef :: ‹isa_vmtf_remove_int ⇒ trail_pol ⇒ (nat option) nres› where
‹isa_vmtf_find_next_undef = (λ((ns, m, fst_As, lst_As, next_search), to_remove) M. do {
WHILE⇩T⇗λnext_search. next_search ≠ None ⟶ defined_atm_pol_pre M (the next_search)⇖
(λnext_search. next_search ≠ None ∧ defined_atm_pol M (the next_search))
(λnext_search. do {
ASSERT(next_search ≠ None);
let n = the next_search;
ASSERT (n < length ns);
RETURN (get_next (ns!n))
}
)
next_search
})›
lemma isa_vmtf_find_next_undef_vmtf_find_next_undef:
‹(uncurry isa_vmtf_find_next_undef, uncurry (vmtf_find_next_undef 𝒜)) ∈
(Id ×⇩r distinct_atoms_rel 𝒜) ×⇩r trail_pol 𝒜 →⇩f ⟨⟨nat_rel⟩option_rel⟩nres_rel ›
unfolding isa_vmtf_find_next_undef_def vmtf_find_next_undef_def uncurry_def
defined_atm_def[symmetric]
apply (intro frefI nres_relI)
apply refine_rcg
subgoal by auto
subgoal by (rule defined_atm_pol_pre) (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
subgoal
by (auto simp: undefined_atm_code[THEN fref_to_Down_unRET_uncurry_Id])
subgoal by auto
subgoal by auto
subgoal by auto
done
section ‹Bumping›
definition vmtf_rescore_body
:: ‹nat multiset ⇒ nat clause_l ⇒ (nat,nat) ann_lits ⇒ vmtf_remove_int ⇒
(nat × vmtf_remove_int) nres›
where
‹vmtf_rescore_body 𝒜⇩i⇩n C _ vm = do {
WHILE⇩T⇗λ(i, vm). i ≤ length C ∧
(∀c ∈ set C. atm_of c < length (fst (fst vm)))⇖
(λ(i, vm). i < length C)
(λ(i, vm). do {
ASSERT(i < length C);
ASSERT(atm_of (C!i) ∈# 𝒜⇩i⇩n);
let vm' = vmtf_mark_to_rescore (atm_of (C!i)) vm;
RETURN(i+1, vm')
})
(0, vm)
}›
definition vmtf_rescore
:: ‹nat multiset ⇒ nat clause_l ⇒ (nat,nat) ann_lits ⇒ vmtf_remove_int ⇒
(vmtf_remove_int) nres›
where
‹vmtf_rescore 𝒜⇩i⇩n C M vm = do {
(_, vm) ← vmtf_rescore_body 𝒜⇩i⇩n C M vm;
RETURN (vm)
}›
find_theorems isa_vmtf_mark_to_rescore
definition isa_vmtf_rescore_body
:: ‹nat clause_l ⇒ trail_pol ⇒ isa_vmtf_remove_int ⇒
(nat × isa_vmtf_remove_int) nres›
where
‹isa_vmtf_rescore_body C _ vm = do {
WHILE⇩T⇗λ(i, vm). i ≤ length C ∧
(∀c ∈ set C. atm_of c < length (fst (fst vm)))⇖
(λ(i, vm). i < length C)
(λ(i, vm). do {
ASSERT(i < length C);
ASSERT(isa_vmtf_mark_to_rescore_pre (atm_of (C!i)) vm);
let vm' = isa_vmtf_mark_to_rescore (atm_of (C!i)) vm;
RETURN(i+1, vm')
})
(0, vm)
}›
definition isa_vmtf_rescore
:: ‹nat clause_l ⇒ trail_pol ⇒ isa_vmtf_remove_int ⇒
(isa_vmtf_remove_int) nres›
where
‹isa_vmtf_rescore C M vm = do {
(_, vm) ← isa_vmtf_rescore_body C M vm;
RETURN (vm)
}›
lemma vmtf_rescore_score_clause:
‹(uncurry2 (vmtf_rescore 𝒜), uncurry2 (rescore_clause 𝒜)) ∈
[λ((C, M), vm). literals_are_in_ℒ⇩i⇩n 𝒜 (mset C) ∧ vm ∈ vmtf 𝒜 M]⇩f
(⟨Id⟩list_rel ×⇩f Id ×⇩f Id) → ⟨Id⟩ nres_rel›
proof -
have H: ‹vmtf_rescore_body 𝒜 C M vm ≤
SPEC (λ(n :: nat, vm'). vm' ∈ vmtf 𝒜 M)›
if M: ‹vm ∈ vmtf 𝒜 M› and C: ‹∀c∈set C. atm_of c ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
for C vm φ M
unfolding vmtf_rescore_body_def vmtf_mark_to_rescore_def
apply (refine_vcg WHILEIT_rule_stronger_inv[where R = ‹measure (λ(i, _). length C - i)› and
I' = ‹λ(i, vm'). vm' ∈ vmtf 𝒜 M›])
subgoal by auto
subgoal by auto
subgoal using C M by (auto simp: vmtf_def phase_saving_def)
subgoal using C M by auto
subgoal using M by auto
subgoal using C by (auto simp: atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n)
subgoal using C by auto
subgoal using C by auto
subgoal using C by (auto simp: vmtf_append_remove_iff')
subgoal by auto
done
have K: ‹((a, b),(a', b')) ∈ A ×⇩f B ⟷ (a, a') ∈ A ∧ (b, b') ∈ B› for a b a' b' A B
by auto
show ?thesis
unfolding vmtf_rescore_def rescore_clause_def uncurry_def
apply (intro frefI nres_relI)
apply clarify
apply (rule bind_refine_spec)
prefer 2
apply (subst (asm) K)
apply (rule H; auto)
subgoal
by (meson atm_of_lit_in_atms_of contra_subsetD in_all_lits_of_m_ain_atms_of_iff
in_multiset_in_set literals_are_in_ℒ⇩i⇩n_def)
subgoal by auto
done
qed
lemma isa_vmtf_rescore_body:
‹(uncurry2 (isa_vmtf_rescore_body), uncurry2 (vmtf_rescore_body 𝒜)) ∈ [λ_. isasat_input_bounded 𝒜]⇩f
(Id ×⇩f trail_pol 𝒜 ×⇩f (Id ×⇩f distinct_atoms_rel 𝒜)) → ⟨Id ×⇩r (Id ×⇩f distinct_atoms_rel 𝒜)⟩ nres_rel›
proof -
show ?thesis
unfolding isa_vmtf_rescore_body_def vmtf_rescore_body_def uncurry_def
apply (intro frefI nres_relI)
apply refine_rcg
subgoal by auto
subgoal by auto
subgoal for x y x1 x1a x1b x2 x2a x2b x1c x1d x1e x2c x1g x2g
by (cases x2g) auto
subgoal by auto
subgoal by auto
subgoal for x y x1 x1a x1b x2 x2a x2b x1c x1d x1e x2c x2d x2e x1g x2g
unfolding isa_vmtf_mark_to_rescore_pre_def
by (cases x2e)
(auto intro!: atms_hash_insert_pre)
subgoal
by (auto intro!: isa_vmtf_mark_to_rescore_vmtf_mark_to_rescore[THEN fref_to_Down_unRET_uncurry])
done
qed
lemma isa_vmtf_rescore:
‹(uncurry2 (isa_vmtf_rescore), uncurry2 (vmtf_rescore 𝒜)) ∈ [λ_. isasat_input_bounded 𝒜]⇩f
(Id ×⇩f trail_pol 𝒜 ×⇩f (Id ×⇩f distinct_atoms_rel 𝒜)) → ⟨(Id ×⇩f distinct_atoms_rel 𝒜)⟩ nres_rel›
proof -
show ?thesis
unfolding isa_vmtf_rescore_def vmtf_rescore_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg isa_vmtf_rescore_body[THEN fref_to_Down_curry2])
subgoal by auto
subgoal by auto
done
qed
definition vmtf_mark_to_rescore_clause where
‹vmtf_mark_to_rescore_clause 𝒜⇩i⇩n arena C vm = do {
ASSERT(arena_is_valid_clause_idx arena C);
nfoldli
([C..<C + (arena_length arena C)])
(λ_. True)
(λi vm. do {
ASSERT(i < length arena);
ASSERT(arena_lit_pre arena i);
ASSERT(atm_of (arena_lit arena i) ∈# 𝒜⇩i⇩n);
RETURN (vmtf_mark_to_rescore (atm_of (arena_lit arena i)) vm)
})
vm
}›
definition isa_vmtf_mark_to_rescore_clause where
‹isa_vmtf_mark_to_rescore_clause arena C vm = do {
ASSERT(arena_is_valid_clause_idx arena C);
nfoldli
([C..<C + (arena_length arena C)])
(λ_. True)
(λi vm. do {
ASSERT(i < length arena);
ASSERT(arena_lit_pre arena i);
ASSERT(isa_vmtf_mark_to_rescore_pre (atm_of (arena_lit arena i)) vm);
RETURN (isa_vmtf_mark_to_rescore (atm_of (arena_lit arena i)) vm)
})
vm
}›
lemma isa_vmtf_mark_to_rescore_clause_vmtf_mark_to_rescore_clause:
‹(uncurry2 isa_vmtf_mark_to_rescore_clause, uncurry2 (vmtf_mark_to_rescore_clause 𝒜)) ∈ [λ_. isasat_input_bounded 𝒜]⇩f
Id ×⇩f nat_rel ×⇩f (Id ×⇩r distinct_atoms_rel 𝒜) → ⟨Id ×⇩r distinct_atoms_rel 𝒜⟩nres_rel›
unfolding isa_vmtf_mark_to_rescore_clause_def vmtf_mark_to_rescore_clause_def
uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg nfoldli_refine[where R = ‹Id ×⇩r distinct_atoms_rel 𝒜› and S = Id])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal for x y x1 x1a x2 x2a x1b x1c x2b x2c xi xa si s
by (cases s)
(auto simp: isa_vmtf_mark_to_rescore_pre_def
intro!: atms_hash_insert_pre)
subgoal
by (rule isa_vmtf_mark_to_rescore_vmtf_mark_to_rescore[THEN fref_to_Down_unRET_uncurry])
auto
done
lemma vmtf_mark_to_rescore_clause_spec:
‹vm ∈ vmtf 𝒜 M ⟹ valid_arena arena N vdom ⟹ C ∈# dom_m N ⟹
(∀C ∈ set [C..<C + arena_length arena C]. arena_lit arena C ∈# ℒ⇩a⇩l⇩l 𝒜) ⟹
vmtf_mark_to_rescore_clause 𝒜 arena C vm ≤ RES (vmtf 𝒜 M)›
unfolding vmtf_mark_to_rescore_clause_def
apply (subst RES_SPEC_conv)
apply (refine_vcg nfoldli_rule[where I = ‹λ_ _ vm. vm ∈ vmtf 𝒜 M›])
subgoal
unfolding arena_lit_pre_def arena_is_valid_clause_idx_def
apply (rule exI[of _ N])
apply (rule exI[of _ vdom])
apply (fastforce simp: arena_lifting)
done
subgoal for x it σ
using arena_lifting(7)[of arena N vdom C ‹x - C›]
by (auto simp: arena_lifting(1-6) dest!: in_list_in_setD)
subgoal for x it σ
unfolding arena_lit_pre_def arena_is_valid_clause_idx_and_access_def
apply (rule exI[of _ C])
apply (intro conjI)
apply (solves ‹auto dest: in_list_in_setD›)
apply (rule exI[of _ N])
apply (rule exI[of _ vdom])
apply (fastforce simp: arena_lifting dest: in_list_in_setD)
done
subgoal for x it σ
by fastforce
subgoal for x it _ σ
by (cases σ)
(auto intro!: vmtf_mark_to_rescore simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
dest: in_list_in_setD)
done
definition vmtf_mark_to_rescore_also_reasons
:: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ arena ⇒ nat literal list ⇒ _ ⇒_› where
‹vmtf_mark_to_rescore_also_reasons 𝒜 M arena outl vm = do {
ASSERT(length outl ≤ uint32_max);
nfoldli
([0..<length outl])
(λ_. True)
(λi vm. do {
ASSERT(i < length outl); ASSERT(length outl ≤ uint32_max);
ASSERT(-outl ! i ∈# ℒ⇩a⇩l⇩l 𝒜);
C ← get_the_propagation_reason M (-(outl ! i));
case C of
None ⇒ RETURN (vmtf_mark_to_rescore (atm_of (outl ! i)) vm)
| Some C ⇒ if C = 0 then RETURN vm else vmtf_mark_to_rescore_clause 𝒜 arena C vm
})
vm
}›
definition isa_vmtf_mark_to_rescore_also_reasons
:: ‹trail_pol ⇒ arena ⇒ nat literal list ⇒ _ ⇒_› where
‹isa_vmtf_mark_to_rescore_also_reasons M arena outl vm = do {
ASSERT(length outl ≤ uint32_max);
nfoldli
([0..<length outl])
(λ_. True)
(λi vm. do {
ASSERT(i < length outl); ASSERT(length outl≤ uint32_max);
C ← get_the_propagation_reason_pol M (-(outl ! i));
case C of
None ⇒ do {
ASSERT (isa_vmtf_mark_to_rescore_pre (atm_of (outl ! i)) vm);
RETURN (isa_vmtf_mark_to_rescore (atm_of (outl ! i)) vm)
}
| Some C ⇒ if C = 0 then RETURN vm else isa_vmtf_mark_to_rescore_clause arena C vm
})
vm
}›
lemma isa_vmtf_mark_to_rescore_also_reasons_vmtf_mark_to_rescore_also_reasons:
‹(uncurry3 isa_vmtf_mark_to_rescore_also_reasons, uncurry3 (vmtf_mark_to_rescore_also_reasons 𝒜)) ∈
[λ_. isasat_input_bounded 𝒜]⇩f
trail_pol 𝒜 ×⇩f Id ×⇩f Id ×⇩f (Id ×⇩r distinct_atoms_rel 𝒜) → ⟨Id ×⇩r distinct_atoms_rel 𝒜⟩nres_rel›
unfolding isa_vmtf_mark_to_rescore_also_reasons_def vmtf_mark_to_rescore_also_reasons_def
uncurry_def
apply (intro frefI nres_relI)
apply (refine_rcg nfoldli_refine[where R = ‹Id ×⇩r distinct_atoms_rel 𝒜› and S = Id]
get_the_propagation_reason_pol[of 𝒜, THEN fref_to_Down_curry]
isa_vmtf_mark_to_rescore_clause_vmtf_mark_to_rescore_clause[of 𝒜, THEN fref_to_Down_curry2])
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply assumption
subgoal for x y x1 x1a x1b x2 x2a x2b x1c x1d x1e x2c x2d x2e xi xa si s xb x'
by (cases s)
(auto simp: isa_vmtf_mark_to_rescore_pre_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
intro!: atms_hash_insert_pre[of _ 𝒜])
subgoal
by (rule isa_vmtf_mark_to_rescore_vmtf_mark_to_rescore[THEN fref_to_Down_unRET_uncurry])
(auto simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
subgoal by auto
subgoal by auto
done
lemma vmtf_mark_to_rescore':
‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜) ⟹ vm ∈ vmtf 𝒜 M ⟹ vmtf_mark_to_rescore L vm ∈ vmtf 𝒜 M›
by (cases vm) (auto intro: vmtf_mark_to_rescore)
lemma vmtf_mark_to_rescore_also_reasons_spec:
‹vm ∈ vmtf 𝒜 M ⟹ valid_arena arena N vdom ⟹ length outl ≤ uint32_max ⟹
(∀L ∈ set outl. L ∈# ℒ⇩a⇩l⇩l 𝒜) ⟹
(∀L ∈ set outl. ∀C. (Propagated (-L) C ∈ set M ⟶ C ≠ 0 ⟶ (C ∈# dom_m N ∧
(∀C ∈ set [C..<C + arena_length arena C]. arena_lit arena C ∈# ℒ⇩a⇩l⇩l 𝒜)))) ⟹
vmtf_mark_to_rescore_also_reasons 𝒜 M arena outl vm ≤ RES (vmtf 𝒜 M)›
unfolding vmtf_mark_to_rescore_also_reasons_def
apply (subst RES_SPEC_conv)
apply (refine_vcg nfoldli_rule[where I = ‹λ_ _ vm. vm ∈ vmtf 𝒜 M›])
subgoal by (auto dest: in_list_in_setD)
subgoal for x l1 l2 σ
unfolding all_set_conv_nth
by (auto simp: uminus_𝒜⇩i⇩n_iff dest!: in_list_in_setD)
subgoal for x l1 l2 σ
unfolding get_the_propagation_reason_def
apply (rule SPEC_rule)
apply (rename_tac reason, case_tac reason; simp only: option.simps RES_SPEC_conv[symmetric])
subgoal
by (auto simp: vmtf_mark_to_rescore'
in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff[symmetric])
apply (rename_tac D, case_tac ‹D = 0›; simp)
subgoal
by (rule vmtf_mark_to_rescore_clause_spec, assumption, assumption)
fastforce+
done
done
section ‹Backtrack level for Restarts›
text ‹
We here find out how many decisions can be reused. Remark that since VMTF does not reuse many levels anyway,
the implementation might be mostly useless, but I was not aware of that when I implemented it.
›
definition find_decomp_w_ns_pre where
‹find_decomp_w_ns_pre 𝒜 = (λ((M, highest), vm).
no_dup M ∧
highest < count_decided M ∧
isasat_input_bounded 𝒜 ∧
literals_are_in_ℒ⇩i⇩n_trail 𝒜 M ∧
vm ∈ vmtf 𝒜 M)›
definition find_decomp_wl_imp
:: ‹nat multiset ⇒ (nat, nat) ann_lits ⇒ nat ⇒ vmtf_remove_int ⇒
((nat, nat) ann_lits × vmtf_remove_int) nres›
where
‹find_decomp_wl_imp 𝒜 = (λM⇩0 lev vm. do {
let k = count_decided M⇩0;
let M⇩0 = trail_conv_to_no_CS M⇩0;
let n = length M⇩0;
pos ← get_pos_of_level_in_trail M⇩0 lev;
ASSERT((n - pos) ≤ uint32_max);
ASSERT(n ≥ pos);
let target = n - pos;
(_, M, vm') ←
WHILE⇩T⇗λ(j, M, vm'). j ≤ target ∧
M = drop j M⇩0 ∧ target ≤ length M⇩0 ∧
vm' ∈ vmtf 𝒜 M ∧ literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset M)⇖
(λ(j, M, vm). j < target)
(λ(j, M, vm). do {
ASSERT(M ≠ []);
ASSERT(Suc j ≤ uint32_max);
let L = atm_of (lit_of_hd_trail M);
ASSERT(L ∈# 𝒜);
RETURN (j + 1, tl M, vmtf_unset L vm)
})
(0, M⇩0, vm);
ASSERT(lev = count_decided M);
let M = trail_conv_back lev M;
RETURN (M, vm')
})›
definition isa_find_decomp_wl_imp
:: ‹trail_pol ⇒ nat ⇒ isa_vmtf_remove_int ⇒ (trail_pol × isa_vmtf_remove_int) nres›
where
‹isa_find_decomp_wl_imp = (λM⇩0 lev vm. do {
let k = count_decided_pol M⇩0;
let M⇩0 = trail_pol_conv_to_no_CS M⇩0;
ASSERT(isa_length_trail_pre M⇩0);
let n = isa_length_trail M⇩0;
pos ← get_pos_of_level_in_trail_imp M⇩0 lev;
ASSERT((n - pos) ≤ uint32_max);
ASSERT(n ≥ pos);
let target = n - pos;
(_, M, vm') ←
WHILE⇩T⇗λ(j, M, vm'). j ≤ target⇖
(λ(j, M, vm). j < target)
(λ(j, M, vm). do {
ASSERT(Suc j ≤ uint32_max);
ASSERT(case M of (M, _) ⇒ M ≠ []);
ASSERT(tl_trailt_tr_no_CS_pre M);
let L = atm_of (lit_of_last_trail_pol M);
ASSERT(vmtf_unset_pre L vm);
RETURN (j + 1, tl_trailt_tr_no_CS M, isa_vmtf_unset L vm)
})
(0, M⇩0, vm);
M ← trail_conv_back_imp lev M;
RETURN (M, vm')
})›
abbreviation find_decomp_w_ns_prop where
‹find_decomp_w_ns_prop 𝒜 ≡
(λ(M::(nat, nat) ann_lits) highest _.
(λ(M1, vm). ∃K M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
get_level M K = Suc highest ∧ vm ∈ vmtf 𝒜 M1))›
definition find_decomp_w_ns where
‹find_decomp_w_ns 𝒜 =
(λ(M::(nat, nat) ann_lits) highest vm.
SPEC(find_decomp_w_ns_prop 𝒜 M highest vm))›
lemma isa_find_decomp_wl_imp_find_decomp_wl_imp:
‹(uncurry2 isa_find_decomp_wl_imp, uncurry2 (find_decomp_wl_imp 𝒜)) ∈
[λ((M, lev), vm). lev < count_decided M]⇩f trail_pol 𝒜 ×⇩f nat_rel ×⇩f (Id ×⇩r distinct_atoms_rel 𝒜) →
⟨trail_pol 𝒜 ×⇩r (Id ×⇩r distinct_atoms_rel 𝒜)⟩nres_rel›
proof -
have [intro]: ‹(M', M) ∈ trail_pol 𝒜 ⟹ (M', M) ∈ trail_pol_no_CS 𝒜› for M' M
by (auto simp: trail_pol_def trail_pol_no_CS_def control_stack_length_count_dec[symmetric])
have [refine0]: ‹((0, trail_pol_conv_to_no_CS x1c, x2c),
0, trail_conv_to_no_CS x1a, x2a)
∈ nat_rel ×⇩r trail_pol_no_CS 𝒜 ×⇩r (Id ×⇩r distinct_atoms_rel 𝒜)›
if
‹case y of
(x, xa) ⇒ (case x of (M, lev) ⇒ λ_. lev < count_decided M) xa› and
‹(x, y)
∈ trail_pol 𝒜 ×⇩f nat_rel ×⇩f (Id ×⇩f distinct_atoms_rel 𝒜)› and ‹x1 = (x1a, x2)› and
‹y = (x1, x2a)› and
‹x1b = (x1c, x2b)› and
‹x = (x1b, x2c)› and
‹isa_length_trail_pre (trail_pol_conv_to_no_CS x1c)› and
‹(pos, posa) ∈ nat_rel› and
‹length (trail_conv_to_no_CS x1a) - posa ≤ uint32_max› and
‹isa_length_trail (trail_pol_conv_to_no_CS x1c) - pos ≤ uint32_max› and
‹case (0, trail_conv_to_no_CS x1a, x2a) of
(j, M, vm') ⇒
j ≤ length (trail_conv_to_no_CS x1a) - posa ∧
M = drop j (trail_conv_to_no_CS x1a) ∧
length (trail_conv_to_no_CS x1a) - posa
≤ length (trail_conv_to_no_CS x1a) ∧
vm' ∈ vmtf 𝒜 M ∧ literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset M)›
for x y x1 x1a x2 x2a x1b x1c x2b x2c pos posa
proof -
show ?thesis
supply trail_pol_conv_to_no_CS_def[simp] trail_conv_to_no_CS_def[simp]
using that by auto
qed
have trail_pol_empty: ‹(([], x2g), M) ∈ trail_pol_no_CS 𝒜 ⟹ M = []› for M x2g
by (auto simp: trail_pol_no_CS_def ann_lits_split_reasons_def)
have isa_vmtf: ‹(x2c, x2a) ∈ Id ×⇩f distinct_atoms_rel 𝒜 ⟹
(((aa, ab, ac, ad, ba), baa, ca), x2e) ∈ Id ×⇩f distinct_atoms_rel 𝒜 ⟹
x2e ∈ vmtf 𝒜 (drop x1d x1a) ⟹
((aa, ab, ac, ad, ba), baa, ca) ∈ isa_vmtf 𝒜 (drop x1d x1a)›
for x y x1 x1a x2 x2a x1b x1c x2b x2c pos posa xa x' x1d x2d x1e x2e x1f x2f
x1g x1h x2g x2h aa ab ac ad ba baa ca
by (cases x2e)
(auto 6 6 simp: isa_vmtf_def Image_iff converse_iff prod_rel_iff
intro!: bexI[of _ x2e])
have trail_pol_no_CS_last_hd:
‹((x1h, t), M) ∈ trail_pol_no_CS 𝒜 ⟹ M ≠ [] ⟹ (last x1h) = lit_of (hd M)›
for x1h t M
by (auto simp: trail_pol_no_CS_def ann_lits_split_reasons_def last_map last_rev)
have trail_conv_back: ‹trail_conv_back_imp x2b x1g
≤ SPEC
(λc. (c, trail_conv_back x2 x1e)
∈ trail_pol 𝒜)›
if
‹case y of (x, xa) ⇒ (case x of (M, lev) ⇒ λvm. lev < count_decided M) xa› and
‹(x, y) ∈ trail_pol 𝒜 ×⇩f nat_rel ×⇩f (Id ×⇩f distinct_atoms_rel 𝒜)› and
‹x1 = (x1a, x2)› and
‹y = (x1, x2a)› and
‹x1b = (x1c, x2b)› and
‹x = (x1b, x2c)› and
‹isa_length_trail_pre (trail_pol_conv_to_no_CS x1c)› and
‹(pos, posa) ∈ nat_rel› and
‹length (trail_conv_to_no_CS x1a) - posa ≤ uint32_max› and
‹isa_length_trail (trail_pol_conv_to_no_CS x1c) - pos ≤ uint32_max› and
‹(xa, x') ∈ nat_rel ×⇩f (trail_pol_no_CS 𝒜 ×⇩f (Id ×⇩f distinct_atoms_rel 𝒜))› and
‹x2d = (x1e, x2e)› and
‹x' = (x1d, x2d)› and
‹x2f = (x1g, x2g)› and
‹xa = (x1f, x2f)› and
‹x2 = count_decided x1e›
for x y x1 x1a x2 x2a x1b x1c x2b x2c pos posa xa x' x1d x2d x1e x2e x1f x2f
x1g x2g
apply (rule trail_conv_back[THEN fref_to_Down_curry, THEN order_trans])
using that by (auto simp: conc_fun_RETURN)
show ?thesis
supply trail_pol_conv_to_no_CS_def[simp] trail_conv_to_no_CS_def[simp]
unfolding isa_find_decomp_wl_imp_def find_decomp_wl_imp_def uncurry_def
apply (intro frefI nres_relI)
apply (refine_vcg
id_trail_conv_to_no_CS[THEN fref_to_Down, unfolded comp_def]
get_pos_of_level_in_trail_imp_get_pos_of_level_in_trail[of 𝒜, THEN fref_to_Down_curry])
subgoal
by (rule isa_length_trail_pre) auto
subgoal
by (auto simp: get_pos_of_level_in_trail_pre_def)
subgoal
by auto
subgoal
by (subst isa_length_trail_length_u_no_CS[THEN fref_to_Down_unRET_Id]) auto
subgoal
by (subst isa_length_trail_length_u_no_CS[THEN fref_to_Down_unRET_Id]) auto
apply (assumption+)[10]
subgoal
by (subst isa_length_trail_length_u_no_CS[THEN fref_to_Down_unRET_Id]) auto
subgoal
by (subst isa_length_trail_length_u_no_CS[THEN fref_to_Down_unRET_Id]) auto
subgoal
by (auto dest!: trail_pol_empty)
subgoal
by (auto dest!: trail_pol_empty)
subgoal for x y x1 x1a x2 x2a x1b x1c x2b x2c pos posa
by (rule tl_trailt_tr_no_CS_pre) auto
subgoal for x y x1 x1a x2 x2a x1b x1c x2b x2c pos posa xa x' x1d x2d x1e x2e x1f x2f
x1g x1h x2g x2h
by (cases x1g, cases x2h)
(auto intro!: vmtf_unset_pre[of _ _ _ _ _ _ 𝒜 ‹drop x1d x1a›] isa_vmtf
simp: lit_of_last_trail_pol_def trail_pol_no_CS_last_hd lit_of_hd_trail_def)
subgoal
by (auto simp: lit_of_last_trail_pol_def trail_pol_no_CS_last_hd lit_of_hd_trail_def
intro!: tl_trail_tr_no_CS[THEN fref_to_Down_unRET]
isa_vmtf_unset_vmtf_unset[THEN fref_to_Down_unRET_uncurry])
apply (rule trail_conv_back; assumption)
subgoal
by auto
done
qed
definition (in -) find_decomp_wl_st :: ‹nat literal ⇒ nat twl_st_wl ⇒ nat twl_st_wl nres› where
‹find_decomp_wl_st = (λL (M, N, D, oth). do{
M' ← find_decomp_wl' M (the D) L;
RETURN (M', N, D, oth)
})›
definition find_decomp_wl_st_int :: ‹nat ⇒ twl_st_wl_heur ⇒ twl_st_wl_heur nres› where
‹find_decomp_wl_st_int = (λhighest (M, N, D, Q, W, vm, φ, clvls, cach, lbd, stats). do{
(M', vm) ← isa_find_decomp_wl_imp M highest vm;
RETURN (M', N, D, Q, W, vm, φ, clvls, cach, lbd, stats)
})›
lemma
assumes
vm: ‹vm ∈ vmtf 𝒜 M⇩0› and
lits: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜 M⇩0› and
target: ‹highest < count_decided M⇩0› and
n_d: ‹no_dup M⇩0› and
bounded: ‹isasat_input_bounded 𝒜›
shows
find_decomp_wl_imp_le_find_decomp_wl':
‹find_decomp_wl_imp 𝒜 M⇩0 highest vm ≤ find_decomp_w_ns 𝒜 M⇩0 highest vm›
(is ?decomp)
proof -
have length_M0: ‹length M⇩0 ≤ uint32_max div 2 + 1›
using length_trail_uint32_max_div2[of 𝒜 M⇩0, OF bounded]
n_d literals_are_in_ℒ⇩i⇩n_trail_in_lits_of_l[of 𝒜, OF lits]
by (auto simp: lits_of_def)
have 1: ‹((count_decided x1g, x1g), count_decided x1, x1) ∈ Id›
if ‹x1g = x1› for x1g x1 :: ‹(nat, nat) ann_lits›
using that by auto
have [simp]: ‹∃M'a. M' @ x2g = M'a @ tl x2g› for M' x2g :: ‹(nat, nat) ann_lits›
by (rule exI[of _ ‹M' @ (if x2g = [] then [] else [hd x2g])›]) auto
have butlast_nil_iff: ‹butlast xs = [] ⟷ xs = [] ∨ (∃a. xs = [a])› for xs :: ‹(nat, nat) ann_lits›
by (cases xs) auto
have butlast1: ‹tl x2g = drop (Suc (length x1) - length x2g) x1› (is ‹?G1›)
if ‹x2g = drop (length x1 - length x2g) x1› for x2g x1 :: ‹'a list›
proof -
have [simp]: ‹Suc (length x1 - length x2g) = Suc (length x1) - length x2g›
by (metis Suc_diff_le diff_le_mono2 diff_zero length_drop that zero_le)
show ?G1
by (subst that) (auto simp: butlast_conv_take tl_drop_def)[]
qed
have butlast2: ‹tl x2g = drop (length x1 - (length x2g - Suc 0)) x1› (is ‹?G2›)
if ‹x2g = drop (length x1 - length x2g) x1› and x2g: ‹x2g ≠ []› for x2g x1 :: ‹'a list›
proof -
have [simp]: ‹Suc (length x1 - length x2g) = Suc (length x1) - length x2g›
by (metis Suc_diff_le diff_le_mono2 diff_zero length_drop that(1) zero_le)
have [simp]: ‹Suc (length x1) - length x2g = length x1 - (length x2g - Suc 0)›
using x2g by auto
show ?G2
by (subst that) (auto simp: butlast_conv_take tl_drop_def)[]
qed
note butlast = butlast1 butlast2
have count_decided_not_Nil[simp]: ‹0 < count_decided M ⟹ M ≠ []› for M :: ‹(nat, nat) ann_lits›
by auto
have get_lev_last: ‹get_level (M' @ M) (lit_of (last M')) = Suc (count_decided M)›
if ‹M⇩0 = M' @ M› and ‹M' ≠ []› and ‹is_decided (last M')› for M' M
apply (cases M' rule: rev_cases)
using that apply (solves simp)
using n_d that by auto
have atm_of_N:
‹literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset aa) ⟹ aa ≠ [] ⟹ atm_of (lit_of (hd aa)) ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜)›
for aa
by (cases aa) (auto simp: literals_are_in_ℒ⇩i⇩n_add_mset in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
have Lin_drop_tl: ‹literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset (drop b M⇩0)) ⟹
literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset (tl (drop b M⇩0)))› for b
apply (rule literals_are_in_ℒ⇩i⇩n_mono)
apply assumption
by (cases ‹drop b M⇩0›) auto
have highest: ‹highest = count_decided M› and
ex_decomp: ‹∃K M2.
(Decided K # M, M2)
∈ set (get_all_ann_decomposition M⇩0) ∧
get_level M⇩0 K = Suc highest ∧ vm ∈ vmtf 𝒜 M›
if
pos: ‹pos < length M⇩0 ∧ is_decided (rev M⇩0 ! pos) ∧ get_level M⇩0 (lit_of (rev M⇩0 ! pos)) =
highest + 1› and
‹length M⇩0 - pos ≤ uint32_max› and
inv: ‹case s of (j, M, vm') ⇒
j ≤ length M⇩0 - pos ∧
M = drop j M⇩0 ∧
length M⇩0 - pos ≤ length M⇩0 ∧
vm' ∈ vmtf 𝒜 M ∧
literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset M)› and
cond: ‹¬ (case s of
(j, M, vm) ⇒ j < length M⇩0 - pos)› and
s: ‹s = (j, s')› ‹s' = (M, vm)›
for pos s j s' M vm
proof -
have
‹j = length M⇩0 - pos› and
M: ‹M = drop (length M⇩0 - pos) M⇩0› and
vm: ‹vm ∈ vmtf 𝒜 (drop (length M⇩0 - pos) M⇩0)› and
‹literals_are_in_ℒ⇩i⇩n 𝒜 (lit_of `# mset (drop (length M⇩0 - pos) M⇩0))›
using cond inv unfolding s
by auto
define M2 and L where ‹M2 = take (length M⇩0 - Suc pos) M⇩0› and ‹L = rev M⇩0 ! pos›
have le_Suc_pos: ‹length M⇩0 - pos = Suc (length M⇩0 - Suc pos)›
using pos by auto
have 1: ‹take (length M⇩0 - pos) M⇩0 = take (length M⇩0 - Suc pos) M⇩0 @ [rev M⇩0 ! pos]›
unfolding le_Suc_pos
apply (subst take_Suc_conv_app_nth)
using pos by (auto simp: rev_nth)
have M⇩0: ‹M⇩0 = M2 @ L # M›
apply (subst append_take_drop_id[symmetric, of _ ‹length M⇩0 - pos›])
unfolding M L_def M2_def 1
by auto
have L': ‹Decided (lit_of L) = L›
using pos unfolding L_def[symmetric] by (cases L) auto
then have M⇩0': ‹M⇩0 = M2 @ Decided (lit_of L) # M›
unfolding M⇩0 by auto
have ‹highest = count_decided M› and ‹get_level M⇩0 (lit_of L) = Suc highest› and ‹is_decided L›
using n_d pos unfolding L_def[symmetric] unfolding M⇩0
by (auto simp: get_level_append_if split: if_splits)
then show
‹∃K M2.
(Decided K # M, M2)
∈ set (get_all_ann_decomposition M⇩0) ∧
get_level M⇩0 K = Suc highest ∧ vm ∈ vmtf 𝒜 M›
using get_all_ann_decomposition_ex[of ‹lit_of L› M M2] vm unfolding M⇩0'[symmetric] M[symmetric]
by blast
show ‹highest = count_decided M›
using ‹highest = count_decided M› .
qed
show ?decomp
unfolding find_decomp_wl_imp_def Let_def find_decomp_w_ns_def trail_conv_to_no_CS_def
get_pos_of_level_in_trail_def trail_conv_back_def
apply (refine_vcg 1 WHILEIT_rule[where R=‹measure (λ(_, M, _). length M)›])
subgoal using length_M0 unfolding uint32_max_def by simp
subgoal by auto
subgoal by auto
subgoal using target by (auto simp: count_decided_ge_get_maximum_level)
subgoal by auto
subgoal by auto
subgoal using vm by auto
subgoal using lits unfolding literals_are_in_ℒ⇩i⇩n_trail_lit_of_mset by auto
subgoal for target s j b M vm by simp
subgoal using length_M0 unfolding uint32_max_def by simp
subgoal for x s a ab aa bb
by (cases ‹drop a M⇩0›)
(auto simp: lit_of_hd_trail_def literals_are_in_ℒ⇩i⇩n_add_mset)
subgoal by auto
subgoal by (auto simp: drop_Suc drop_tl)
subgoal by auto
subgoal for s a b aa ba vm x2 x1a x2a
by (cases vm)
(auto intro!: vmtf_unset_vmtf_tl atm_of_N drop_tl simp: lit_of_hd_trail_def)
subgoal for s a b aa ba x1 x2 x1a x2a
using lits by (auto intro: Lin_drop_tl)
subgoal by auto
subgoal by (rule highest)
subgoal by (rule ex_decomp) (assumption+, auto)
done
qed
lemma find_decomp_wl_imp_find_decomp_wl':
‹(uncurry2 (find_decomp_wl_imp 𝒜), uncurry2 (find_decomp_w_ns 𝒜)) ∈
[find_decomp_w_ns_pre 𝒜]⇩f Id ×⇩f Id ×⇩f Id → ⟨Id ×⇩f Id⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: find_decomp_w_ns_pre_def simp del: twl_st_of_wl.simps
intro!: find_decomp_wl_imp_le_find_decomp_wl')
lemma find_decomp_wl_imp_code_conbine_cond:
‹(λ((b, a), c). find_decomp_w_ns_pre 𝒜 ((b, a), c) ∧ a < count_decided b) = (λ((b, a), c).
find_decomp_w_ns_pre 𝒜 ((b, a), c))›
by (auto intro!: ext simp: find_decomp_w_ns_pre_def)
end