theory IsaSAT_Trail
imports IsaSAT_Literals
begin
chapter ‹Efficient Trail›
text ‹Our trail contains several additional information compared to the simple trail:
▪ the (reversed) trail in an array (i.e., the trail in the same order as presented in
``Automated Reasoning'');
▪ the mapping from any ∗‹literal› (and not an atom) to its polarity;
▪ the mapping from a ∗‹atom› to its level or reason (in two different arrays);
▪ the current level of the state;
▪ the control stack.
We copied the idea from the mapping from a literals to it polarity instead of an atom to its
polarity from a comment by Armin Biere in CaDiCal. We only observed a (at best) faint
performance increase, but as it seemed slightly faster and does not increase the length of the
formalisation, we kept it.
The control stack is the latest addition: it contains the positions of the decisions in the trail.
It is mostly to enable fast restarts (since it allows to directly iterate over all decision of the
trail), but might also slightly speed up backjumping (since we know how far we are going back in the
trail). Remark that the control stack contains is not updated during the backjumping, but only
∗‹after› doing it (as we keep only the the beginning of it).
›
section ‹Polarities›
type_synonym tri_bool = ‹bool option›
definition UNSET :: ‹tri_bool› where
[simp]: ‹UNSET = None›
definition SET_FALSE :: ‹tri_bool› where
[simp]: ‹SET_FALSE = Some False›
definition SET_TRUE :: ‹tri_bool› where
[simp]: ‹SET_TRUE = Some True›
definition (in -) tri_bool_eq :: ‹tri_bool ⇒ tri_bool ⇒ bool› where
‹tri_bool_eq = (=)›
section ‹Types›
type_synonym trail_pol =
‹nat literal list × tri_bool list × nat list × nat list × nat × nat list›
definition get_level_atm where
‹get_level_atm M L = get_level M (Pos L)›
definition polarity_atm where
‹polarity_atm M L =
(if Pos L ∈ lits_of_l M then SET_TRUE
else if Neg L ∈ lits_of_l M then SET_FALSE
else None)›
definition defined_atm :: ‹('v, nat) ann_lits ⇒ 'v ⇒ bool› where
‹defined_atm M L = defined_lit M (Pos L)›
abbreviation undefined_atm where
‹undefined_atm M L ≡ ¬defined_atm M L›
section ‹Control Stack›
inductive control_stack where
empty:
‹control_stack [] []› |
cons_prop:
‹control_stack cs M ⟹ control_stack cs (Propagated L C # M)› |
cons_dec:
‹control_stack cs M ⟹ n = length M ⟹ control_stack (cs @ [n]) (Decided L # M)›
inductive_cases control_stackE: ‹control_stack cs M›
lemma control_stack_length_count_dec:
‹control_stack cs M ⟹ length cs = count_decided M›
by (induction rule: control_stack.induct) auto
lemma control_stack_le_length_M:
‹control_stack cs M ⟹ c∈set cs ⟹ c < length M›
by (induction rule: control_stack.induct) auto
lemma control_stack_propa[simp]:
‹control_stack cs (Propagated x21 x22 # list) ⟷ control_stack cs list›
by (auto simp: control_stack.intros elim: control_stackE)
lemma control_stack_filter_map_nth:
‹control_stack cs M ⟹ filter is_decided (rev M) = map (nth (rev M)) cs›
apply (induction rule: control_stack.induct)
subgoal by auto
subgoal for cs M L C
using control_stack_le_length_M[of cs M]
by (auto simp: nth_append)
subgoal for cs M L
using control_stack_le_length_M[of cs M]
by (auto simp: nth_append)
done
lemma control_stack_empty_cs[simp]: ‹control_stack [] M ⟷ count_decided M = 0›
by (induction M rule:ann_lit_list_induct)
(auto simp: control_stack.empty control_stack.cons_prop elim: control_stackE)
text ‹This is an other possible definition. It is not inductive, which makes it easier to reason
about appending (or removing) some literals from the trail. It is however much less clear if the
definition is correct.›
definition control_stack' where
‹control_stack' cs M ⟷
(length cs = count_decided M ∧
(∀L∈set M. is_decided L ⟶ (cs ! (get_level M (lit_of L) - 1) < length M ∧
rev M!(cs ! (get_level M (lit_of L) - 1)) = L)))›
lemma control_stack_rev_get_lev:
‹control_stack cs M ⟹
no_dup M ⟹ L∈set M ⟹ is_decided L ⟹ rev M!(cs ! (get_level M (lit_of L) - 1)) = L›
apply (induction arbitrary: L rule: control_stack.induct)
subgoal by auto
subgoal for cs M L C La
using control_stack_le_length_M[of cs M] control_stack_length_count_dec[of cs M]
count_decided_ge_get_level[of M ‹lit_of La›]
apply (auto simp: get_level_cons_if nth_append atm_of_eq_atm_of undefined_notin)
by (metis Suc_count_decided_gt_get_level Suc_less_eq Suc_pred count_decided_0_iff diff_is_0_eq
le_SucI le_refl neq0_conv nth_mem)
subgoal for cs M L
using control_stack_le_length_M[of cs M] control_stack_length_count_dec[of cs M]
apply (auto simp: nth_append get_level_cons_if atm_of_eq_atm_of undefined_notin)
by (metis Suc_count_decided_gt_get_level Suc_less_eq Suc_pred count_decided_0_iff diff_is_0_eq
le_SucI le_refl neq0_conv)+
done
lemma control_stack_alt_def_imp:
‹no_dup M ⟹ (⋀L. L ∈set M ⟹ is_decided L ⟹ cs ! (get_level M (lit_of L) - 1) < length M ∧
rev M!(cs ! (get_level M (lit_of L) - 1)) = L) ⟹
length cs = count_decided M ⟹
control_stack cs M›
proof (induction M arbitrary: cs rule:ann_lit_list_induct)
case Nil
then show ?case by auto
next
case (Decided L M) note IH = this(1) and n_d = this(2) and dec = this(3) and length = this(4)
from length obtain cs' n where cs[simp]: ‹cs = cs' @ [n]›
using length by (cases cs rule: rev_cases) auto
have [simp]: ‹rev M ! n ∈ set M ⟹ is_decided (rev M ! n) ⟹ count_decided M ≠ 0›
by (auto simp: count_decided_0_iff)
have dec': ‹L'∈set M ⟹ is_decided L' ⟹ cs' ! (get_level M (lit_of L') - 1) < length M ∧
rev M ! (cs' ! (get_level M (lit_of L') - 1)) = L'› for L'
using dec[of L'] n_d length
count_decided_ge_get_level[of M ‹lit_of L'›]
apply (auto simp: get_level_cons_if atm_of_eq_atm_of undefined_notin
split: if_splits)
apply (auto simp: nth_append split: if_splits)
done
have le: ‹length cs' = count_decided M›
using length by auto
have [simp]: ‹n = length M›
using n_d dec[of ‹Decided L›] le undefined_notin[of M ‹rev M ! n›] nth_mem[of n ‹rev M›]
by (auto simp: nth_append split: if_splits)
show ?case
unfolding cs
apply (rule control_stack.cons_dec)
subgoal
apply (rule IH)
using n_d dec' le by auto
subgoal by auto
done
next
case (Propagated L m M) note IH = this(1) and n_d = this(2) and dec = this(3) and length = this(4)
have [simp]: ‹rev M ! n ∈ set M ⟹ is_decided (rev M ! n) ⟹ count_decided M ≠ 0› for n
by (auto simp: count_decided_0_iff)
have dec': ‹L'∈set M ⟹ is_decided L' ⟹ cs ! (get_level M (lit_of L') - 1) < length M ∧
rev M ! (cs ! (get_level M (lit_of L') - 1)) = L'› for L'
using dec[of L'] n_d length
count_decided_ge_get_level[of M ‹lit_of L'›]
apply (cases L')
apply (auto simp: get_level_cons_if atm_of_eq_atm_of undefined_notin
split: if_splits)
apply (auto simp: nth_append split: if_splits)
done
show ?case
apply (rule control_stack.cons_prop)
apply (rule IH)
subgoal using n_d by auto
subgoal using dec' by auto
subgoal using length by auto
done
qed
lemma control_stack_alt_def: ‹no_dup M ⟹ control_stack' cs M ⟷ control_stack cs M›
using control_stack_alt_def_imp[of M cs] control_stack_rev_get_lev[of cs M]
control_stack_length_count_dec[of cs M] control_stack_le_length_M[of cs M]
unfolding control_stack'_def apply -
apply (rule iffI)
subgoal by blast
subgoal
using count_decided_ge_get_level[of M]
by (metis One_nat_def Suc_count_decided_gt_get_level Suc_less_eq Suc_pred count_decided_0_iff
less_imp_diff_less neq0_conv nth_mem)
done
lemma control_stack_decomp:
assumes
decomp: ‹(Decided L # M1, M2) ∈ set (get_all_ann_decomposition M)› and
cs: ‹control_stack cs M› and
n_d: ‹no_dup M›
shows ‹control_stack (take (count_decided M1) cs) M1›
proof -
obtain M3 where M: ‹M = M3 @ M2 @ Decided L # M1›
using decomp by auto
define M2' where ‹M2' = M3 @ M2›
have M: ‹M = M2' @ Decided L # M1›
unfolding M M2'_def by auto
have n_d1: ‹no_dup M1›
using n_d no_dup_appendD unfolding M by auto
have ‹control_stack' cs M›
using cs
apply (subst (asm) control_stack_alt_def[symmetric])
apply (rule n_d)
apply assumption
done
then have
cs_M: ‹length cs = count_decided M› and
L: ‹⋀L. L∈set M ⟹ is_decided L ⟹
cs ! (get_level M (lit_of L) - 1) < length M ∧ rev M ! (cs ! (get_level M (lit_of L) - 1)) = L›
unfolding control_stack'_def by auto
have H: ‹L' ∈ set M1 ⟹ undefined_lit M2' (lit_of L') ∧ atm_of (lit_of L') ≠ atm_of L› for L'
using n_d unfolding M
by (metis atm_of_eq_atm_of defined_lit_no_dupD(1) defined_lit_uminus lit_of.simps(1)
no_dup_appendD no_dup_append_cons no_dup_cons undefined_notin)
have ‹distinct M›
using no_dup_imp_distinct[OF n_d] .
then have K: ‹L' ∈ set M1 ⟹ x < length M ⟹ rev M ! x = L' ⟹ x < length M1› for x L'
unfolding M apply (auto simp: nth_append nth_Cons split: if_splits nat.splits)
by (metis length_rev less_diff_conv local.H not_less_eq nth_mem set_rev undefined_notin)
have I: ‹L ∈ set M1 ⟹ is_decided L ⟹ get_level M1 (lit_of L) > 0› for L
using n_d unfolding M by (auto dest!: split_list)
have cs': ‹control_stack' (take (count_decided M1) cs) M1›
unfolding control_stack'_def
apply (intro conjI ballI impI)
subgoal using cs_M unfolding M by auto
subgoal for L using n_d L[of L] H[of L] K[of L ‹cs ! (get_level M1 (lit_of L) - Suc 0)›]
count_decided_ge_get_level[of ‹M1› ‹lit_of L›] I[of L]
unfolding M by auto
subgoal for L using n_d L[of L] H[of L] K[of L ‹cs ! (get_level M1 (lit_of L) - Suc 0)›]
count_decided_ge_get_level[of ‹M1› ‹lit_of L›] I[of L]
unfolding M by auto
done
show ?thesis
apply (subst control_stack_alt_def[symmetric])
apply (rule n_d1)
apply (rule cs')
done
qed
section ‹Encoding of the reasons›
definition DECISION_REASON :: nat where
‹DECISION_REASON = 1›
definition ann_lits_split_reasons where
‹ann_lits_split_reasons 𝒜 = {((M, reasons), M'). M = map lit_of (rev M') ∧
(∀L ∈ set M'. is_proped L ⟶
reasons ! (atm_of (lit_of L)) = mark_of L ∧ mark_of L ≠ DECISION_REASON) ∧
(∀L ∈ set M'. is_decided L ⟶ reasons ! (atm_of (lit_of L)) = DECISION_REASON) ∧
(∀L ∈# ℒ⇩a⇩l⇩l 𝒜. atm_of L < length reasons)
}›
definition trail_pol :: ‹nat multiset ⇒ (trail_pol × (nat, nat) ann_lits) set› where
‹trail_pol 𝒜 =
{((M', xs, lvls, reasons, k, cs), M). ((M', reasons), M) ∈ ann_lits_split_reasons 𝒜 ∧
no_dup M ∧
(∀L ∈# ℒ⇩a⇩l⇩l 𝒜. nat_of_lit L < length xs ∧ xs ! (nat_of_lit L) = polarity M L) ∧
(∀L ∈# ℒ⇩a⇩l⇩l 𝒜. atm_of L < length lvls ∧ lvls ! (atm_of L) = get_level M L) ∧
k = count_decided M ∧
(∀L∈set M. lit_of L ∈# ℒ⇩a⇩l⇩l 𝒜) ∧
control_stack cs M ∧
isasat_input_bounded 𝒜}›
section ‹Definition of the full trail›
lemma trail_pol_alt_def:
‹trail_pol 𝒜 = {((M', xs, lvls, reasons, k, cs), M).
((M', reasons), M) ∈ ann_lits_split_reasons 𝒜 ∧
no_dup M ∧
(∀L ∈# ℒ⇩a⇩l⇩l 𝒜. nat_of_lit L < length xs ∧ xs ! (nat_of_lit L) = polarity M L) ∧
(∀L ∈# ℒ⇩a⇩l⇩l 𝒜. atm_of L < length lvls ∧ lvls ! (atm_of L) = get_level M L) ∧
k = count_decided M ∧
(∀L∈set M. lit_of L ∈# ℒ⇩a⇩l⇩l 𝒜) ∧
control_stack cs M ∧ literals_are_in_ℒ⇩i⇩n_trail 𝒜 M ∧
length M < uint32_max ∧
length M ≤ uint32_max div 2 + 1 ∧
count_decided M < uint32_max ∧
length M' = length M ∧
M' = map lit_of (rev M) ∧
isasat_input_bounded 𝒜
}›
proof -
have [intro!]: ‹length M < n ⟹ count_decided M < n› for M n
using length_filter_le[of is_decided M]
by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def uint32_max_def count_decided_def
simp del: length_filter_le
dest: length_trail_uint32_max_div2)
show ?thesis
unfolding trail_pol_def
by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def uint32_max_def ann_lits_split_reasons_def
dest: length_trail_uint32_max_div2
simp del: isasat_input_bounded_def)
qed
section ‹Code generation›
subsection ‹Conversion between incomplete and complete mode›
definition trail_fast_of_slow :: ‹(nat, nat) ann_lits ⇒ (nat, nat) ann_lits› where
‹trail_fast_of_slow = id›
definition trail_pol_slow_of_fast :: ‹trail_pol ⇒ trail_pol› where
‹trail_pol_slow_of_fast =
(λ(M, val, lvls, reason, k, cs). (M, val, lvls, reason, k, cs))›
definition trail_slow_of_fast :: ‹(nat, nat) ann_lits ⇒ (nat, nat) ann_lits› where
‹trail_slow_of_fast = id›
definition trail_pol_fast_of_slow :: ‹trail_pol ⇒ trail_pol› where
‹trail_pol_fast_of_slow =
(λ(M, val, lvls, reason, k, cs). (M, val, lvls, reason, k, cs))›
lemma trail_pol_slow_of_fast_alt_def:
‹trail_pol_slow_of_fast M = M›
by (cases M)
(auto simp: trail_pol_slow_of_fast_def)
lemma trail_pol_fast_of_slow_trail_fast_of_slow:
‹(RETURN o trail_pol_fast_of_slow, RETURN o trail_fast_of_slow)
∈ [λM. (∀C L. Propagated L C ∈ set M ⟶ C < uint64_max)]⇩f
trail_pol 𝒜 → ⟨trail_pol 𝒜⟩ nres_rel›
by (intro frefI nres_relI)
(auto simp: trail_pol_def trail_pol_fast_of_slow_def
trail_fast_of_slow_def)
lemma trail_pol_slow_of_fast_trail_slow_of_fast:
‹(RETURN o trail_pol_slow_of_fast, RETURN o trail_slow_of_fast)
∈ trail_pol 𝒜 →⇩f ⟨trail_pol 𝒜⟩ nres_rel›
by (intro frefI nres_relI)
(auto simp: trail_pol_def trail_pol_fast_of_slow_def
trail_fast_of_slow_def trail_slow_of_fast_def
trail_pol_slow_of_fast_def)
lemma trail_pol_same_length[simp]: ‹(M', M) ∈ trail_pol 𝒜 ⟹ length (fst M') = length M›
by (auto simp: trail_pol_alt_def)
definition counts_maximum_level where
‹counts_maximum_level M C = {i. C ≠ None ⟶ i = card_max_lvl M (the C)}›
lemma counts_maximum_level_None[simp]: ‹counts_maximum_level M None = Collect (λ_. True)›
by (auto simp: counts_maximum_level_def)
subsection ‹Level of a literal›
definition get_level_atm_pol_pre where
‹get_level_atm_pol_pre = (λ((M, xs, lvls, k), L). L < length lvls)›
definition get_level_atm_pol :: ‹trail_pol ⇒ nat ⇒ nat› where
‹get_level_atm_pol = (λ(M, xs, lvls, k) L. lvls ! L)›
lemma get_level_atm_pol_pre:
assumes
‹Pos L ∈# ℒ⇩a⇩l⇩l 𝒜› and
‹(M', M) ∈ trail_pol 𝒜›
shows ‹get_level_atm_pol_pre (M', L)›
using assms
by (auto 5 5 simp: trail_pol_def nat_lit_rel_def
br_def get_level_atm_pol_pre_def intro!: ext)
lemma (in -) get_level_get_level_atm: ‹get_level M L = get_level_atm M (atm_of L)›
unfolding get_level_atm_def
by (cases L) (auto simp: get_level_Neg_Pos)
definition get_level_pol where
‹get_level_pol M L = get_level_atm_pol M (atm_of L)›
definition get_level_pol_pre where
‹get_level_pol_pre = (λ((M, xs, lvls, k), L). atm_of L < length lvls)›
lemma get_level_pol_pre:
assumes
‹L ∈# ℒ⇩a⇩l⇩l 𝒜› and
‹(M', M) ∈ trail_pol 𝒜›
shows ‹get_level_pol_pre (M', L)›
using assms
by (auto 5 5 simp: trail_pol_def nat_lit_rel_def
br_def get_level_pol_pre_def intro!: ext)
lemma get_level_get_level_pol:
assumes
‹(M', M) ∈ trail_pol 𝒜› and ‹L ∈# ℒ⇩a⇩l⇩l 𝒜›
shows ‹get_level M L = get_level_pol M' L›
using assms
by (auto simp: get_level_pol_def get_level_atm_pol_def trail_pol_def)
subsection ‹Current level›
definition (in -) count_decided_pol where
‹count_decided_pol = (λ(_, _, _, _, k, _). k)›
lemma count_decided_trail_ref:
‹(RETURN o count_decided_pol, RETURN o count_decided) ∈ trail_pol 𝒜 →⇩f ⟨nat_rel⟩nres_rel›
by (intro frefI nres_relI) (auto simp: trail_pol_def count_decided_pol_def)
subsection ‹Polarity›
definition (in -) polarity_pol :: ‹trail_pol ⇒ nat literal ⇒ bool option› where
‹polarity_pol = (λ(M, xs, lvls, k) L. do {
xs ! (nat_of_lit L)
})›
definition polarity_pol_pre where
‹polarity_pol_pre = (λ(M, xs, lvls, k) L. nat_of_lit L < length xs)›
lemma polarity_pol_polarity:
‹(uncurry (RETURN oo polarity_pol), uncurry (RETURN oo polarity)) ∈
[λ(M, L). L ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f trail_pol 𝒜 ×⇩f Id → ⟨⟨bool_rel⟩option_rel⟩nres_rel›
by (intro nres_relI frefI)
(auto simp: trail_pol_def polarity_def polarity_pol_def
dest!: multi_member_split)
lemma polarity_pol_pre:
‹(M', M) ∈ trail_pol 𝒜 ⟹ L ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ polarity_pol_pre M' L›
by (auto simp: trail_pol_def polarity_def polarity_pol_def polarity_pol_pre_def
dest!: multi_member_split)
subsection ‹Length of the trail›
definition (in -) isa_length_trail_pre where
‹isa_length_trail_pre = (λ (M', xs, lvls, reasons, k, cs). length M' ≤ uint32_max)›
definition (in -) isa_length_trail where
‹isa_length_trail = (λ (M', xs, lvls, reasons, k, cs). length_uint32_nat M')›
lemma isa_length_trail_pre:
‹(M, M') ∈ trail_pol 𝒜 ⟹ isa_length_trail_pre M›
by (auto simp: isa_length_trail_def trail_pol_alt_def isa_length_trail_pre_def)
lemma isa_length_trail_length_u:
‹(RETURN o isa_length_trail, RETURN o length_uint32_nat) ∈ trail_pol 𝒜 →⇩f ⟨nat_rel⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: isa_length_trail_def trail_pol_alt_def
intro!: ASSERT_leI)
subsection ‹Consing elements›
definition cons_trail_Propagated_tr_pre where
‹cons_trail_Propagated_tr_pre = (λ((L, C), (M, xs, lvls, reasons, k)). nat_of_lit L < length xs ∧
nat_of_lit (-L) < length xs ∧ atm_of L < length lvls ∧ atm_of L < length reasons ∧ length M < uint32_max)›
definition cons_trail_Propagated_tr :: ‹nat literal ⇒ nat ⇒ trail_pol ⇒ trail_pol nres› where
‹cons_trail_Propagated_tr = (λL C (M', xs, lvls, reasons, k, cs). do {
ASSERT(cons_trail_Propagated_tr_pre ((L, C), (M', xs, lvls, reasons, k, cs)));
RETURN (M' @ [L], let xs = xs[nat_of_lit L := SET_TRUE] in xs[nat_of_lit (-L) := SET_FALSE],
lvls[atm_of L := k], reasons[atm_of L:= C], k, cs)})›
lemma in_list_pos_neg_notD: ‹Pos (atm_of (lit_of La)) ∉ lits_of_l bc ⟹
Neg (atm_of (lit_of La)) ∉ lits_of_l bc ⟹
La ∈ set bc ⟹ False›
by (metis Neg_atm_of_iff Pos_atm_of_iff lits_of_def rev_image_eqI)
lemma cons_trail_Propagated_tr_pre:
assumes ‹(M', M) ∈ trail_pol 𝒜› and
‹undefined_lit M L› and
‹L ∈# ℒ⇩a⇩l⇩l 𝒜› and
‹C ≠ DECISION_REASON›
shows ‹cons_trail_Propagated_tr_pre ((L, C), M')›
using assms
by (auto simp: trail_pol_alt_def ann_lits_split_reasons_def uminus_𝒜⇩i⇩n_iff
cons_trail_Propagated_tr_pre_def
intro!: ext)
lemma cons_trail_Propagated_tr:
‹(uncurry2 (cons_trail_Propagated_tr), uncurry2 (cons_trail_propagate_l)) ∈
[λ((L, C), M). L ∈# ℒ⇩a⇩l⇩l 𝒜 ∧ C ≠ DECISION_REASON]⇩f
Id ×⇩f nat_rel ×⇩f trail_pol 𝒜 → ⟨trail_pol 𝒜⟩nres_rel›
unfolding cons_trail_Propagated_tr_def cons_trail_propagate_l_def
apply (intro frefI nres_relI)
subgoal for x y
using cons_trail_Propagated_tr_pre[of ‹snd (x)› ‹snd (y)› 𝒜 ‹fst (fst y)› ‹snd (fst y)›]
unfolding uncurry_def
apply refine_vcg
subgoal by auto
subgoal
by (cases ‹fst (fst y)›)
(auto simp add: trail_pol_def polarity_def uminus_lit_swap
cons_trail_Propagated_tr_def Decided_Propagated_in_iff_in_lits_of_l nth_list_update'
ann_lits_split_reasons_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n
uminus_𝒜⇩i⇩n_iff atm_of_eq_atm_of
intro!: ASSERT_refine_right
dest!: in_list_pos_neg_notD dest: pos_lit_in_atms_of neg_lit_in_atms_of dest!: multi_member_split
simp del: nat_of_lit.simps)
done
done
lemma cons_trail_Propagated_tr2:
‹(((L, C), M), ((L', C'), M')) ∈ Id ×⇩f Id ×⇩f trail_pol 𝒜 ⟹ L ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹
C ≠ DECISION_REASON ⟹
cons_trail_Propagated_tr L C M
≤ ⇓ ({(M'', M'''). (M'', M''') ∈ trail_pol 𝒜 ∧ M''' = Propagated L C # M' ∧ no_dup M'''})
(cons_trail_propagate_l L' C' M')›
using cons_trail_Propagated_tr[THEN fref_to_Down_curry2, of 𝒜 L' C' M' L C M]
unfolding cons_trail_Propagated_tr_def cons_trail_propagate_l_def
using cons_trail_Propagated_tr_pre[of M M' 𝒜 L C]
unfolding uncurry_def
apply refine_vcg
subgoal by auto
subgoal
by (auto simp: trail_pol_def)
done
lemma undefined_lit_count_decided_uint32_max:
assumes
M_ℒ⇩a⇩l⇩l: ‹∀L∈set M. lit_of L ∈# ℒ⇩a⇩l⇩l 𝒜› and n_d: ‹no_dup M› and
‹L ∈# ℒ⇩a⇩l⇩l 𝒜› and ‹undefined_lit M L› and
bounded: ‹isasat_input_bounded 𝒜›
shows ‹Suc (count_decided M) ≤ uint32_max›
proof -
have dist_atm_M: ‹distinct_mset {#atm_of (lit_of x). x ∈# mset M#}›
using n_d by (metis distinct_mset_mset_distinct mset_map no_dup_def)
have incl: ‹atm_of `# lit_of `# mset (Decided L # M) ⊆# remdups_mset (atm_of `# ℒ⇩a⇩l⇩l 𝒜)›
apply (subst distinct_subseteq_iff[THEN iffD1])
using assms dist_atm_M
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l lits_of_def no_dup_distinct
atm_of_eq_atm_of)
from size_mset_mono[OF this] have 1: ‹count_decided M + 1 ≤ size (remdups_mset (atm_of `# ℒ⇩a⇩l⇩l 𝒜))›
using length_filter_le[of is_decided M] unfolding uint32_max_def count_decided_def
by (auto simp del: length_filter_le)
have inj_on: ‹inj_on nat_of_lit (set_mset (remdups_mset (ℒ⇩a⇩l⇩l 𝒜)))›
by (auto simp: inj_on_def)
have H: ‹xa ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ atm_of xa ≤ uint32_max div 2› for xa
using bounded
by (cases xa) (auto simp: uint32_max_def)
have ‹remdups_mset (atm_of `# ℒ⇩a⇩l⇩l 𝒜) ⊆# mset [0..< 1 + (uint32_max div 2)]›
apply (subst distinct_subseteq_iff[THEN iffD1])
using H distinct_image_mset_inj[OF inj_on]
by (force simp del: literal_of_nat.simps simp: distinct_mset_mset_set
dest: le_neq_implies_less)+
note _ = size_mset_mono[OF this]
moreover have ‹size (nat_of_lit `# remdups_mset (ℒ⇩a⇩l⇩l 𝒜)) = size (remdups_mset (ℒ⇩a⇩l⇩l 𝒜))›
by simp
ultimately have 2: ‹size (remdups_mset (atm_of `# (ℒ⇩a⇩l⇩l 𝒜))) ≤ 1 + uint32_max div 2›
by auto
show ?thesis
using 1 2 by (auto simp: uint32_max_def)
from size_mset_mono[OF incl] have 1: ‹length M + 1 ≤ size (remdups_mset (atm_of `# ℒ⇩a⇩l⇩l 𝒜))›
unfolding uint32_max_def count_decided_def
by (auto simp del: length_filter_le)
with 2 have ‹length M ≤ uint32_max›
by auto
qed
lemma length_trail_uint32_max:
assumes
M_ℒ⇩a⇩l⇩l: ‹∀L∈set M. lit_of L ∈# ℒ⇩a⇩l⇩l 𝒜› and n_d: ‹no_dup M› and
bounded: ‹isasat_input_bounded 𝒜›
shows ‹length M ≤ uint32_max›
proof -
have dist_atm_M: ‹distinct_mset {#atm_of (lit_of x). x ∈# mset M#}›
using n_d by (metis distinct_mset_mset_distinct mset_map no_dup_def)
have incl: ‹atm_of `# lit_of `# mset M ⊆# remdups_mset (atm_of `# ℒ⇩a⇩l⇩l 𝒜)›
apply (subst distinct_subseteq_iff[THEN iffD1])
using assms dist_atm_M
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l lits_of_def no_dup_distinct
atm_of_eq_atm_of)
have inj_on: ‹inj_on nat_of_lit (set_mset (remdups_mset (ℒ⇩a⇩l⇩l 𝒜)))›
by (auto simp: inj_on_def)
have H: ‹xa ∈# ℒ⇩a⇩l⇩l 𝒜 ⟹ atm_of xa ≤ uint32_max div 2› for xa
using bounded
by (cases xa) (auto simp: uint32_max_def)
have ‹remdups_mset (atm_of `# ℒ⇩a⇩l⇩l 𝒜) ⊆# mset [0..< 1 + (uint32_max div 2)]›
apply (subst distinct_subseteq_iff[THEN iffD1])
using H distinct_image_mset_inj[OF inj_on]
by (force simp del: literal_of_nat.simps simp: distinct_mset_mset_set
dest: le_neq_implies_less)+
note _ = size_mset_mono[OF this]
moreover have ‹size (nat_of_lit `# remdups_mset (ℒ⇩a⇩l⇩l 𝒜)) = size (remdups_mset (ℒ⇩a⇩l⇩l 𝒜))›
by simp
ultimately have 2: ‹size (remdups_mset (atm_of `# ℒ⇩a⇩l⇩l 𝒜)) ≤ 1 + uint32_max div 2›
by auto
from size_mset_mono[OF incl] have 1: ‹length M ≤ size (remdups_mset (atm_of `# ℒ⇩a⇩l⇩l 𝒜))›
unfolding uint32_max_def count_decided_def
by (auto simp del: length_filter_le)
with 2 show ?thesis
by (auto simp: uint32_max_def)
qed
definition last_trail_pol_pre where
‹last_trail_pol_pre = (λ(M, xs, lvls, reasons, k). atm_of (last M) < length reasons ∧ M ≠ [])›
definition (in -) last_trail_pol :: ‹trail_pol ⇒ (nat literal × nat option)› where
‹last_trail_pol = (λ(M, xs, lvls, reasons, k).
let r = reasons ! (atm_of (last M)) in
(last M, if r = DECISION_REASON then None else Some r))›
definition tl_trailt_tr :: ‹trail_pol ⇒ trail_pol› where
‹tl_trailt_tr = (λ(M', xs, lvls, reasons, k, cs).
let L = last M' in
(butlast M',
let xs = xs[nat_of_lit L := None] in xs[nat_of_lit (-L) := None],
lvls[atm_of L := 0],
reasons, if reasons ! atm_of L = DECISION_REASON then k-1 else k,
if reasons ! atm_of L = DECISION_REASON then butlast cs else cs))›
definition tl_trailt_tr_pre where
‹tl_trailt_tr_pre = (λ(M, xs, lvls, reason, k, cs). M ≠ [] ∧ nat_of_lit(last M) < length xs ∧
nat_of_lit(-last M) < length xs ∧ atm_of (last M) < length lvls ∧
atm_of (last M) < length reason ∧
(reason ! atm_of (last M) = DECISION_REASON ⟶ k ≥ 1 ∧ cs ≠ []))›
lemma ann_lits_split_reasons_map_lit_of:
‹((M, reasons), M') ∈ ann_lits_split_reasons 𝒜 ⟹ M = map lit_of (rev M')›
by (auto simp: ann_lits_split_reasons_def)
lemma control_stack_dec_butlast:
‹control_stack b (Decided x1 # M's) ⟹ control_stack (butlast b) M's›
by (cases b rule: rev_cases) (auto dest: control_stackE)
lemma tl_trail_tr:
‹((RETURN o tl_trailt_tr), (RETURN o tl)) ∈
[λM. M ≠ []]⇩f trail_pol 𝒜 → ⟨trail_pol 𝒜⟩nres_rel›
proof -
show ?thesis
apply (intro frefI nres_relI, rename_tac x y, case_tac ‹y›)
subgoal by fast
subgoal for M M' L M's
unfolding trail_pol_def comp_def RETURN_refine_iff trail_pol_def Let_def
apply clarify
apply (intro conjI; clarify?; (intro conjI)?)
subgoal
by (auto simp: trail_pol_def polarity_atm_def tl_trailt_tr_def
ann_lits_split_reasons_def Let_def)
subgoal by (auto simp: trail_pol_def polarity_atm_def tl_trailt_tr_def)
subgoal by (auto simp: polarity_atm_def tl_trailt_tr_def Let_def)
subgoal
by (cases ‹lit_of L›)
(auto simp: polarity_def tl_trailt_tr_def Decided_Propagated_in_iff_in_lits_of_l
uminus_lit_swap Let_def
dest: ann_lits_split_reasons_map_lit_of)
subgoal
by (auto simp: polarity_atm_def tl_trailt_tr_def Let_def
atm_of_eq_atm_of get_level_cons_if)
subgoal
by (auto simp: polarity_atm_def tl_trailt_tr_def
atm_of_eq_atm_of get_level_cons_if Let_def
dest!: ann_lits_split_reasons_map_lit_of)
subgoal
by (cases ‹L›)
(auto simp: tl_trailt_tr_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff ann_lits_split_reasons_def
dest: no_dup_consistentD)
subgoal
by (auto simp: tl_trailt_tr_def)
subgoal
by (cases ‹L›)
(auto simp: tl_trailt_tr_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff ann_lits_split_reasons_def
control_stack_dec_butlast
dest: no_dup_consistentD)
done
done
qed
lemma tl_trailt_tr_pre:
assumes ‹M ≠ []›
‹(M', M) ∈ trail_pol 𝒜›
shows ‹tl_trailt_tr_pre M'›
proof -
have [simp]: ‹x ≠ [] ⟹ is_decided (last x) ⟹ Suc 0 ≤ count_decided x› for x
by (cases x rule: rev_cases) auto
show ?thesis
using assms
by (cases M; cases ‹hd M›)
(auto simp: trail_pol_def ann_lits_split_reasons_def uminus_𝒜⇩i⇩n_iff
rev_map[symmetric] hd_append hd_map tl_trailt_tr_pre_def simp del: rev_map
intro!: ext)
qed
definition tl_trail_propedt_tr :: ‹trail_pol ⇒ trail_pol› where
‹tl_trail_propedt_tr = (λ(M', xs, lvls, reasons, k, cs).
let L = last M' in
(butlast M',
let xs = xs[nat_of_lit L := None] in xs[nat_of_lit (-L) := None],
lvls[atm_of L := 0],
reasons, k, cs))›
definition tl_trail_propedt_tr_pre where
‹tl_trail_propedt_tr_pre =
(λ(M, xs, lvls, reason, k, cs). M ≠ [] ∧ nat_of_lit(last M) < length xs ∧
nat_of_lit(-last M) < length xs ∧ atm_of (last M) < length lvls ∧
atm_of (last M) < length reason)›
lemma tl_trail_propedt_tr_pre:
assumes ‹(M', M) ∈ trail_pol 𝒜› and
‹M ≠ []›
shows ‹tl_trail_propedt_tr_pre M'›
using assms
unfolding trail_pol_def comp_def RETURN_refine_iff trail_pol_def Let_def
tl_trail_propedt_tr_def tl_trail_propedt_tr_pre_def
apply clarify
apply (cases M; intro conjI; clarify?; (intro conjI)?)
subgoal
by (auto simp: trail_pol_def polarity_atm_def tl_trailt_tr_def
ann_lits_split_reasons_def Let_def)
subgoal
by (auto simp: polarity_atm_def tl_trailt_tr_def
atm_of_eq_atm_of get_level_cons_if Let_def
dest!: ann_lits_split_reasons_map_lit_of)
subgoal
by (cases ‹hd M›)
(auto simp: tl_trailt_tr_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff ann_lits_split_reasons_def
dest: no_dup_consistentD)
subgoal
by (cases ‹hd M›)
(auto simp: tl_trailt_tr_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff ann_lits_split_reasons_def
control_stack_dec_butlast
dest: no_dup_consistentD)
subgoal
by (cases ‹hd M›)
(auto simp: tl_trailt_tr_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff ann_lits_split_reasons_def
control_stack_dec_butlast
dest: no_dup_consistentD)
done
definition (in -) lit_of_hd_trail where
‹lit_of_hd_trail M = lit_of (hd M)›
definition (in -) lit_of_last_trail_pol where
‹lit_of_last_trail_pol = (λ(M, _). last M)›
lemma lit_of_last_trail_pol_lit_of_last_trail:
‹(RETURN o lit_of_last_trail_pol, RETURN o lit_of_hd_trail) ∈
[λS. S ≠ []]⇩f trail_pol 𝒜 → ⟨Id⟩nres_rel›
by (auto simp: lit_of_hd_trail_def trail_pol_def lit_of_last_trail_pol_def
ann_lits_split_reasons_def hd_map rev_map[symmetric] last_rev
intro!: frefI nres_relI)
subsection ‹Setting a new literal›
definition cons_trail_Decided :: ‹nat literal ⇒ (nat, nat) ann_lits ⇒ (nat, nat) ann_lits› where
‹cons_trail_Decided L M' = Decided L # M'›
definition cons_trail_Decided_tr :: ‹nat literal ⇒ trail_pol ⇒ trail_pol› where
‹cons_trail_Decided_tr = (λL (M', xs, lvls, reasons, k, cs). do{
let n = length M' in
(M' @ [L], let xs = xs[nat_of_lit L := SET_TRUE] in xs[nat_of_lit (-L) := SET_FALSE],
lvls[atm_of L := k+1], reasons[atm_of L := DECISION_REASON], k+1, cs @ [n])})›
definition cons_trail_Decided_tr_pre where
‹cons_trail_Decided_tr_pre =
(λ(L, (M, xs, lvls, reason, k, cs)). nat_of_lit L < length xs ∧ nat_of_lit (-L) < length xs ∧
atm_of L < length lvls ∧ atm_of L < length reason ∧ length cs < uint32_max ∧
Suc k ≤ uint32_max ∧ length M < uint32_max)›
lemma length_cons_trail_Decided[simp]:
‹length (cons_trail_Decided L M) = Suc (length M)›
by (auto simp: cons_trail_Decided_def)
lemma cons_trail_Decided_tr:
‹(uncurry (RETURN oo cons_trail_Decided_tr), uncurry (RETURN oo cons_trail_Decided)) ∈
[λ(L, M). undefined_lit M L ∧ L ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f Id ×⇩f trail_pol 𝒜 → ⟨trail_pol 𝒜⟩nres_rel›
by (intro frefI nres_relI, rename_tac x y, case_tac ‹fst x›)
(auto simp: trail_pol_def polarity_def cons_trail_Decided_def uminus_lit_swap
Decided_Propagated_in_iff_in_lits_of_l
cons_trail_Decided_tr_def nth_list_update' ann_lits_split_reasons_def
dest!: in_list_pos_neg_notD multi_member_split
intro: control_stack.cons_dec
simp del: nat_of_lit.simps)
lemma cons_trail_Decided_tr_pre:
assumes ‹(M', M) ∈ trail_pol 𝒜› and
‹L ∈# ℒ⇩a⇩l⇩l 𝒜› and ‹undefined_lit M L›
shows ‹cons_trail_Decided_tr_pre (L, M')›
using assms
by (auto simp: trail_pol_alt_def image_image ann_lits_split_reasons_def uminus_𝒜⇩i⇩n_iff
cons_trail_Decided_tr_pre_def control_stack_length_count_dec
intro!: ext undefined_lit_count_decided_uint32_max length_trail_uint32_max)
subsection ‹Polarity: Defined or Undefined›
definition (in -) defined_atm_pol_pre where
‹defined_atm_pol_pre = (λ(M, xs, lvls, k) L. 2*L < length xs ∧
2*L ≤ uint32_max)›
definition (in -) defined_atm_pol where
‹defined_atm_pol = (λ(M, xs, lvls, k) L. ¬((xs!(2*L)) = None))›
lemma undefined_atm_code:
‹(uncurry (RETURN oo defined_atm_pol), uncurry (RETURN oo defined_atm)) ∈
[λ(M, L). Pos L ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f trail_pol 𝒜 ×⇩r Id → ⟨bool_rel⟩ nres_rel› (is ?A) and
defined_atm_pol_pre:
‹(M', M) ∈ trail_pol 𝒜 ⟹ L ∈# 𝒜 ⟹ defined_atm_pol_pre M' L›
proof -
have H: ‹2*L < length xs› (is ‹?length›) and
none: ‹defined_atm M L ⟷ xs ! (2*L) ≠ None› (is ?undef) and
le: ‹2*L ≤ uint32_max› (is ?le)
if L_N: ‹Pos L ∈# ℒ⇩a⇩l⇩l 𝒜› and tr: ‹((M', xs, lvls, k), M) ∈ trail_pol 𝒜›
for M xs lvls k M' L
proof -
have
‹M' = map lit_of (rev M)› and
‹∀L∈#ℒ⇩a⇩l⇩l 𝒜. nat_of_lit L < length xs ∧ xs ! nat_of_lit L = polarity M L›
using tr unfolding trail_pol_def ann_lits_split_reasons_def by fast+
then have L: ‹nat_of_lit (Pos L) < length xs› and
xsL: ‹xs ! (nat_of_lit (Pos L)) = polarity M (Pos L)›
using L_N by (auto dest!: multi_member_split)
show ?length
using L by simp
show ?undef
using xsL by (auto simp: polarity_def defined_atm_def
Decided_Propagated_in_iff_in_lits_of_l split: if_splits)
show ‹2*L ≤ uint32_max›
using tr L_N unfolding trail_pol_def by auto
qed
show ?A
unfolding defined_atm_pol_def
by (intro frefI nres_relI) (auto 5 5 simp: none H le intro!: ASSERT_leI)
show ‹(M', M) ∈ trail_pol 𝒜 ⟹ L ∈# 𝒜 ⟹ defined_atm_pol_pre M' L›
using H le by (auto simp: defined_atm_pol_pre_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
qed
subsection ‹Reasons›
definition get_propagation_reason_pol :: ‹trail_pol ⇒ nat literal ⇒ nat option nres› where
‹get_propagation_reason_pol = (λ(_, _, _, reasons, _) L. do {
ASSERT(atm_of L < length reasons);
let r = reasons ! atm_of L;
RETURN (if r = DECISION_REASON then None else Some r)})›
lemma get_propagation_reason_pol:
‹(uncurry get_propagation_reason_pol, uncurry get_propagation_reason) ∈
[λ(M, L). L ∈ lits_of_l M]⇩f trail_pol 𝒜 ×⇩r Id → ⟨⟨nat_rel⟩option_rel⟩ nres_rel›
apply (intro frefI nres_relI)
unfolding lits_of_def
apply clarify
apply (rename_tac a aa ab ac b ba ad bb x, case_tac x)
by (auto simp: get_propagation_reason_def get_propagation_reason_pol_def
trail_pol_def ann_lits_split_reasons_def lits_of_def assert_bind_spec_conv)
definition get_propagation_reason_raw_pol :: ‹trail_pol ⇒ nat literal ⇒ nat nres› where
‹get_propagation_reason_raw_pol = (λ(_, _, _, reasons, _) L. do {
ASSERT(atm_of L < length reasons);
let r = reasons ! atm_of L;
RETURN r})›
text ‹The version \<^term>‹get_propagation_reason› can return the reason, but does not have to: it can be
more suitable for specification (like for the conflict minimisation, where finding the reason is
not mandatory).
The following version ∗‹always› returns the reasons if there is one. Remark that both functions
are linked to the same code (but \<^term>‹get_propagation_reason› can be called first with some additional
filtering later).
›
definition (in -) get_the_propagation_reason
:: ‹('v, 'mark) ann_lits ⇒ 'v literal ⇒ 'mark option nres›
where
‹get_the_propagation_reason M L = SPEC(λC.
(C ≠ None ⟷ Propagated L (the C) ∈ set M) ∧
(C = None ⟷ Decided L ∈ set M ∨ L ∉ lits_of_l M))›
lemma no_dup_Decided_PropedD:
‹no_dup ad ⟹ Decided L ∈ set ad ⟹ Propagated L C ∈ set ad ⟹ False›
by (metis annotated_lit.distinct(1) in_set_conv_decomp lit_of.simps(1) lit_of.simps(2)
no_dup_appendD no_dup_cons undefined_notin xy_in_set_cases)
definition get_the_propagation_reason_pol :: ‹trail_pol ⇒ nat literal ⇒ nat option nres› where
‹get_the_propagation_reason_pol = (λ(_, xs, _, reasons, _) L. do {
ASSERT(atm_of L < length reasons);
ASSERT(nat_of_lit L < length xs);
let r = reasons ! atm_of L;
RETURN (if xs ! nat_of_lit L = SET_TRUE ∧ r ≠ DECISION_REASON then Some r else None)})›
lemma get_the_propagation_reason_pol:
‹(uncurry get_the_propagation_reason_pol, uncurry get_the_propagation_reason) ∈
[λ(M, L). L ∈# ℒ⇩a⇩l⇩l 𝒜]⇩f trail_pol 𝒜 ×⇩r Id → ⟨⟨nat_rel⟩option_rel⟩ nres_rel›
proof -
have [dest]: ‹no_dup bb ⟹
SET_TRUE = polarity bb (Pos x1) ⟹ Pos x1 ∈ lits_of_l bb ∧ Neg x1 ∉ lits_of_l bb› for bb x1
by (auto simp: polarity_def split: if_splits dest: no_dup_consistentD)
show ?thesis
apply (intro frefI nres_relI)
unfolding lits_of_def get_the_propagation_reason_def uncurry_def get_the_propagation_reason_pol_def
apply clarify
apply (refine_vcg)
subgoal
by (auto simp: get_the_propagation_reason_def get_the_propagation_reason_pol_def Let_def
trail_pol_def ann_lits_split_reasons_def assert_bind_spec_conv
dest!: multi_member_split[of _ ‹ℒ⇩a⇩l⇩l 𝒜›])[]
subgoal
by (auto simp: get_the_propagation_reason_def get_the_propagation_reason_pol_def Let_def
trail_pol_def ann_lits_split_reasons_def assert_bind_spec_conv
dest!: multi_member_split[of _ ‹ℒ⇩a⇩l⇩l 𝒜›])[]
subgoal for a aa ab ac ad b ba ae bb
apply (cases ‹aa ! nat_of_lit ba ≠ SET_TRUE›)
apply (subgoal_tac ‹ba ∉ lits_of_l ae›)
prefer 2
subgoal
by (auto simp: get_the_propagation_reason_def get_the_propagation_reason_pol_def Let_def
trail_pol_def ann_lits_split_reasons_def assert_bind_spec_conv polarity_spec'(2)
dest: multi_member_split[of _ ‹ℒ⇩a⇩l⇩l 𝒜›])[]
subgoal
by (auto simp: lits_of_def dest: imageI[of _ _ lit_of])
apply (subgoal_tac ‹ba ∈ lits_of_l ae›)
prefer 2
subgoal
by (auto simp: get_the_propagation_reason_def get_the_propagation_reason_pol_def Let_def
trail_pol_def ann_lits_split_reasons_def assert_bind_spec_conv polarity_spec'(2)
dest: multi_member_split[of _ ‹ℒ⇩a⇩l⇩l 𝒜›])[]
subgoal
apply (auto simp: get_the_propagation_reason_def get_the_propagation_reason_pol_def Let_def
trail_pol_def ann_lits_split_reasons_def assert_bind_spec_conv lits_of_def
dest!: multi_member_split[of _ ‹ℒ⇩a⇩l⇩l 𝒜›])[]
apply (case_tac x; auto)
apply (case_tac x; auto)
done
done
done
qed
section ‹Direct access to elements in the trail›
definition (in -) rev_trail_nth where
‹rev_trail_nth M i = lit_of (rev M ! i)›
definition (in -) isa_trail_nth :: ‹trail_pol ⇒ nat ⇒ nat literal nres› where
‹isa_trail_nth = (λ(M, _) i. do {
ASSERT(i < length M);
RETURN (M ! i)
})›
lemma isa_trail_nth_rev_trail_nth:
‹(uncurry isa_trail_nth, uncurry (RETURN oo rev_trail_nth)) ∈
[λ(M, i). i < length M]⇩f trail_pol 𝒜 ×⇩r nat_rel → ⟨Id⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: isa_trail_nth_def rev_trail_nth_def trail_pol_def ann_lits_split_reasons_def
intro!: ASSERT_leI)
text ‹We here define a variant of the trail representation, where the the control stack is out of
sync of the trail (i.e., there are some leftovers at the end). This might make backtracking a
little faster.
›
definition trail_pol_no_CS :: ‹nat multiset ⇒ (trail_pol × (nat, nat) ann_lits) set›
where
‹trail_pol_no_CS 𝒜 =
{((M', xs, lvls, reasons, k, cs), M). ((M', reasons), M) ∈ ann_lits_split_reasons 𝒜 ∧
no_dup M ∧
(∀L ∈# ℒ⇩a⇩l⇩l 𝒜. nat_of_lit L < length xs ∧ xs ! (nat_of_lit L) = polarity M L) ∧
(∀L ∈# ℒ⇩a⇩l⇩l 𝒜. atm_of L < length lvls ∧ lvls ! (atm_of L) = get_level M L) ∧
(∀L∈set M. lit_of L ∈# ℒ⇩a⇩l⇩l 𝒜) ∧
isasat_input_bounded 𝒜 ∧
control_stack (take (count_decided M) cs) M
}›
definition tl_trailt_tr_no_CS :: ‹trail_pol ⇒ trail_pol› where
‹tl_trailt_tr_no_CS = (λ(M', xs, lvls, reasons, k, cs).
let L = last M' in
(butlast M',
let xs = xs[nat_of_lit L := None] in xs[nat_of_lit (-L) := None],
lvls[atm_of L := 0],
reasons, k, cs))›
definition tl_trailt_tr_no_CS_pre where
‹tl_trailt_tr_no_CS_pre = (λ(M, xs, lvls, reason, k, cs). M ≠ [] ∧ nat_of_lit(last M) < length xs ∧
nat_of_lit(-last M) < length xs ∧ atm_of (last M) < length lvls ∧
atm_of (last M) < length reason)›
lemma control_stack_take_Suc_count_dec_unstack:
‹control_stack (take (Suc (count_decided M's)) cs) (Decided x1 # M's) ⟹
control_stack (take (count_decided M's) cs) M's›
using control_stack_length_count_dec[of ‹take (Suc (count_decided M's)) cs› ‹Decided x1 # M's›]
by (auto simp: min_def take_Suc_conv_app_nth split: if_splits elim: control_stackE)
lemma tl_trailt_tr_no_CS_pre:
assumes ‹(M', M) ∈ trail_pol_no_CS 𝒜› and ‹M ≠ []›
shows ‹tl_trailt_tr_no_CS_pre M'›
proof -
have [simp]: ‹x ≠ [] ⟹ is_decided (last x) ⟹ Suc 0 ≤ count_decided x› for x
by (cases x rule: rev_cases) auto
show ?thesis
using assms
unfolding trail_pol_def comp_def RETURN_refine_iff trail_pol_no_CS_def Let_def
tl_trailt_tr_no_CS_def tl_trailt_tr_no_CS_pre_def
by (cases M; cases ‹hd M›)
(auto simp: trail_pol_no_CS_def ann_lits_split_reasons_def uminus_𝒜⇩i⇩n_iff
rev_map[symmetric] hd_append hd_map simp del: rev_map
intro!: ext)
qed
lemma tl_trail_tr_no_CS:
‹((RETURN o tl_trailt_tr_no_CS), (RETURN o tl)) ∈
[λM. M ≠ []]⇩f trail_pol_no_CS 𝒜 → ⟨trail_pol_no_CS 𝒜⟩nres_rel›
apply (intro frefI nres_relI, rename_tac x y, case_tac ‹y›)
subgoal by fast
subgoal for M M' L M's
unfolding trail_pol_def comp_def RETURN_refine_iff trail_pol_no_CS_def Let_def
tl_trailt_tr_no_CS_def
apply clarify
apply (intro conjI; clarify?; (intro conjI)?)
subgoal
by (auto simp: trail_pol_def polarity_atm_def tl_trailt_tr_def
ann_lits_split_reasons_def Let_def)
subgoal by (auto simp: trail_pol_def polarity_atm_def tl_trailt_tr_def)
subgoal by (auto simp: polarity_atm_def tl_trailt_tr_def Let_def)
subgoal
by (cases ‹lit_of L›)
(auto simp: polarity_def tl_trailt_tr_def Decided_Propagated_in_iff_in_lits_of_l
uminus_lit_swap Let_def
dest: ann_lits_split_reasons_map_lit_of)
subgoal
by (auto simp: polarity_atm_def tl_trailt_tr_def Let_def
atm_of_eq_atm_of get_level_cons_if)
subgoal
by (auto simp: polarity_atm_def tl_trailt_tr_def
atm_of_eq_atm_of get_level_cons_if Let_def
dest!: ann_lits_split_reasons_map_lit_of)
subgoal
by (cases ‹L›)
(auto simp: tl_trailt_tr_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff ann_lits_split_reasons_def
control_stack_dec_butlast
dest: no_dup_consistentD)
subgoal
by (cases ‹L›)
(auto simp: tl_trailt_tr_def in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff ann_lits_split_reasons_def
control_stack_dec_butlast control_stack_take_Suc_count_dec_unstack
dest: no_dup_consistentD ann_lits_split_reasons_map_lit_of)
done
done
definition trail_conv_to_no_CS :: ‹(nat, nat) ann_lits ⇒ (nat, nat) ann_lits› where
‹trail_conv_to_no_CS M = M›
definition trail_pol_conv_to_no_CS :: ‹trail_pol ⇒ trail_pol› where
‹trail_pol_conv_to_no_CS M = M›
lemma id_trail_conv_to_no_CS:
‹(RETURN o trail_pol_conv_to_no_CS, RETURN o trail_conv_to_no_CS) ∈ trail_pol 𝒜 →⇩f ⟨trail_pol_no_CS 𝒜⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: trail_pol_no_CS_def trail_conv_to_no_CS_def trail_pol_def
control_stack_length_count_dec trail_pol_conv_to_no_CS_def
intro: ext)
definition trail_conv_back :: ‹nat ⇒ (nat, nat) ann_lits ⇒ (nat, nat) ann_lits› where
‹trail_conv_back j M = M›
definition (in -) trail_conv_back_imp :: ‹nat ⇒ trail_pol ⇒ trail_pol nres› where
‹trail_conv_back_imp j = (λ(M, xs, lvls, reason, _, cs). do {
ASSERT(j ≤ length cs); RETURN (M, xs, lvls, reason, j, take (j) cs)})›
lemma trail_conv_back:
‹(uncurry trail_conv_back_imp, uncurry (RETURN oo trail_conv_back))
∈ [λ(k, M). k = count_decided M]⇩f nat_rel ×⇩f trail_pol_no_CS 𝒜 → ⟨trail_pol 𝒜⟩nres_rel›
by (intro frefI nres_relI)
(force simp: trail_pol_no_CS_def trail_conv_to_no_CS_def trail_pol_def
control_stack_length_count_dec trail_conv_back_def trail_conv_back_imp_def
intro: ext intro!: ASSERT_refine_left
dest: control_stack_length_count_dec multi_member_split)
definition (in -)take_arl where
‹take_arl = (λi (xs, j). (xs, i))›
lemma isa_trail_nth_rev_trail_nth_no_CS:
‹(uncurry isa_trail_nth, uncurry (RETURN oo rev_trail_nth)) ∈
[λ(M, i). i < length M]⇩f trail_pol_no_CS 𝒜 ×⇩r nat_rel → ⟨Id⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: isa_trail_nth_def rev_trail_nth_def trail_pol_def ann_lits_split_reasons_def
trail_pol_no_CS_def
intro!: ASSERT_leI)
lemma trail_pol_no_CS_alt_def:
‹trail_pol_no_CS 𝒜 =
{((M', xs, lvls, reasons, k, cs), M). ((M', reasons), M) ∈ ann_lits_split_reasons 𝒜 ∧
no_dup M ∧
(∀L ∈# ℒ⇩a⇩l⇩l 𝒜. nat_of_lit L < length xs ∧ xs ! (nat_of_lit L) = polarity M L) ∧
(∀L ∈# ℒ⇩a⇩l⇩l 𝒜. atm_of L < length lvls ∧ lvls ! (atm_of L) = get_level M L) ∧
(∀L∈set M. lit_of L ∈# ℒ⇩a⇩l⇩l 𝒜) ∧
control_stack (take (count_decided M) cs) M ∧ literals_are_in_ℒ⇩i⇩n_trail 𝒜 M ∧
length M < uint32_max ∧
length M ≤ uint32_max div 2 + 1 ∧
count_decided M < uint32_max ∧
length M' = length M ∧
isasat_input_bounded 𝒜 ∧
M' = map lit_of (rev M)
}›
proof -
have [intro!]: ‹length M < n ⟹ count_decided M < n› for M n
using length_filter_le[of is_decided M]
by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def uint32_max_def count_decided_def
simp del: length_filter_le
dest: length_trail_uint32_max_div2)
show ?thesis
unfolding trail_pol_no_CS_def
by (auto simp: literals_are_in_ℒ⇩i⇩n_trail_def uint32_max_def ann_lits_split_reasons_def
dest: length_trail_uint32_max_div2
simp del: isasat_input_bounded_def)
qed
lemma isa_length_trail_length_u_no_CS:
‹(RETURN o isa_length_trail, RETURN o length_uint32_nat) ∈ trail_pol_no_CS 𝒜 →⇩f ⟨nat_rel⟩nres_rel›
by (intro frefI nres_relI)
(auto simp: isa_length_trail_def trail_pol_no_CS_alt_def ann_lits_split_reasons_def
intro!: ASSERT_leI)
lemma control_stack_is_decided:
‹control_stack cs M ⟹ c∈set cs ⟹ is_decided ((rev M)!c)›
by (induction arbitrary: c rule: control_stack.induct) (auto simp: nth_append
dest: control_stack_le_length_M)
lemma control_stack_distinct:
‹control_stack cs M ⟹ distinct cs›
by (induction rule: control_stack.induct) (auto simp: nth_append
dest: control_stack_le_length_M)
lemma control_stack_level_control_stack:
assumes
cs: ‹control_stack cs M› and
n_d: ‹no_dup M› and
i: ‹i < length cs›
shows ‹get_level M (lit_of (rev M ! (cs ! i))) = Suc i›
proof -
define L where ‹L = rev M ! (cs ! i)›
have csi: ‹cs ! i < length M›
using cs i by (auto intro: control_stack_le_length_M)
then have L_M: ‹L ∈ set M›
using nth_mem[of ‹cs !i› ‹rev M›] unfolding L_def by (auto simp del: nth_mem)
have dec_L: ‹is_decided L›
using control_stack_is_decided[OF cs] i unfolding L_def by auto
then have ‹rev M!(cs ! (get_level M (lit_of L) - 1)) = L›
using control_stack_rev_get_lev[OF cs n_d L_M] by auto
moreover have ‹distinct M›
using no_dup_distinct[OF n_d] unfolding mset_map[symmetric] distinct_mset_mset_distinct
by (rule distinct_mapI)
moreover have lev0: ‹get_level M (lit_of L) ≥ 1›
using split_list[OF L_M] n_d dec_L by (auto simp: get_level_append_if)
moreover have ‹cs ! (get_level M (lit_of (rev M ! (cs ! i))) - Suc 0) < length M›
using control_stack_le_length_M[OF cs,
of ‹cs ! (get_level M (lit_of (rev M ! (cs ! i))) - Suc 0)›, OF nth_mem]
control_stack_length_count_dec[OF cs] count_decided_ge_get_level[of M
‹lit_of (rev M ! (cs ! i))›] lev0
by (auto simp: L_def)
ultimately have ‹cs ! (get_level M (lit_of L) - 1) = cs ! i›
using nth_eq_iff_index_eq[of ‹rev M›] csi unfolding L_def by auto
then have ‹i = get_level M (lit_of L) - 1›
using nth_eq_iff_index_eq[OF control_stack_distinct[OF cs], of i ‹get_level M (lit_of L) - 1›]
i lev0 count_decided_ge_get_level[of M ‹lit_of (rev M ! (cs ! i))›]
control_stack_length_count_dec[OF cs]
by (auto simp: L_def)
then show ?thesis using lev0 unfolding L_def[symmetric] by auto
qed
definition get_pos_of_level_in_trail where
‹get_pos_of_level_in_trail M⇩0 lev =
SPEC(λi. i < length M⇩0 ∧ is_decided (rev M⇩0!i) ∧ get_level M⇩0 (lit_of (rev M⇩0!i)) = lev+1)›
definition (in -) get_pos_of_level_in_trail_imp where
‹get_pos_of_level_in_trail_imp = (λ(M', xs, lvls, reasons, k, cs) lev. do {
ASSERT(lev < length cs);
RETURN (cs ! lev)
})›
definition get_pos_of_level_in_trail_pre where
‹get_pos_of_level_in_trail_pre = (λ(M, lev). lev < count_decided M)›
lemma get_pos_of_level_in_trail_imp_get_pos_of_level_in_trail:
‹(uncurry get_pos_of_level_in_trail_imp, uncurry get_pos_of_level_in_trail) ∈
[get_pos_of_level_in_trail_pre]⇩f trail_pol_no_CS 𝒜 ×⇩f nat_rel → ⟨nat_rel⟩nres_rel›
apply (intro nres_relI frefI)
unfolding get_pos_of_level_in_trail_imp_def uncurry_def get_pos_of_level_in_trail_def
get_pos_of_level_in_trail_pre_def
apply clarify
apply (rule ASSERT_leI)
subgoal
by (auto simp: trail_pol_no_CS_alt_def dest!: control_stack_length_count_dec)
subgoal for a aa ab ac ad b ba ae bb
by (auto simp: trail_pol_no_CS_def control_stack_length_count_dec in_set_take_conv_nth
intro!: control_stack_le_length_M control_stack_is_decided
dest: control_stack_level_control_stack)
done
lemma get_pos_of_level_in_trail_imp_get_pos_of_level_in_trail_CS:
‹(uncurry get_pos_of_level_in_trail_imp, uncurry get_pos_of_level_in_trail) ∈
[get_pos_of_level_in_trail_pre]⇩f trail_pol 𝒜 ×⇩f nat_rel → ⟨nat_rel⟩nres_rel›
apply (intro nres_relI frefI)
unfolding get_pos_of_level_in_trail_imp_def uncurry_def get_pos_of_level_in_trail_def
get_pos_of_level_in_trail_pre_def
apply clarify
apply (rule ASSERT_leI)
subgoal
by (auto simp: trail_pol_def dest!: control_stack_length_count_dec)
subgoal for a aa ab ac ad b ba ae bb
by (auto simp: trail_pol_def control_stack_length_count_dec in_set_take_conv_nth
intro!: control_stack_le_length_M control_stack_is_decided
dest: control_stack_level_control_stack)
done
lemma lit_of_last_trail_pol_lit_of_last_trail_no_CS:
‹(RETURN o lit_of_last_trail_pol, RETURN o lit_of_hd_trail) ∈
[λS. S ≠ []]⇩f trail_pol_no_CS 𝒜 → ⟨Id⟩nres_rel›
by (auto simp: lit_of_hd_trail_def trail_pol_no_CS_def lit_of_last_trail_pol_def
ann_lits_split_reasons_def hd_map rev_map[symmetric] last_rev
intro!: frefI nres_relI)
end