theory IsaSAT_Literals
imports Watched_Literals.WB_More_Refinement "HOL-Word.More_Word"
Watched_Literals.Watched_Literals_Watch_List
Entailment_Definition.Partial_Herbrand_Interpretation
Isabelle_LLVM.Bits_Natural
begin
chapter ‹Refinement of Literals›
section ‹Literals as Natural Numbers›
subsection ‹Definition›
lemma Pos_div2_iff:
‹Pos ((bb :: nat) div 2) = b ⟷ is_pos b ∧ (bb = 2 * atm_of b ∨ bb = 2 * atm_of b + 1)›
by (cases b) auto
lemma Neg_div2_iff:
‹Neg ((bb :: nat) div 2) = b ⟷ is_neg b ∧ (bb = 2 * atm_of b ∨ bb = 2 * atm_of b + 1)›
by (cases b) auto
text ‹
Modeling \<^typ>‹nat literal› via the transformation associating \<^term>‹2*n› or \<^term>‹2*n+1›
has some advantages over the transformation to positive or negative integers: 0 is not an issue.
It is also a bit faster according to Armin Biere.
›
fun nat_of_lit :: ‹nat literal ⇒ nat› where
‹nat_of_lit (Pos L) = 2*L›
| ‹nat_of_lit (Neg L) = 2*L + 1›
lemma nat_of_lit_def: ‹nat_of_lit L = (if is_pos L then 2 * atm_of L else 2 * atm_of L + 1)›
by (cases L) auto
fun literal_of_nat :: ‹nat ⇒ nat literal› where
‹literal_of_nat n = (if even n then Pos (n div 2) else Neg (n div 2))›
lemma lit_of_nat_nat_of_lit[simp]: ‹literal_of_nat (nat_of_lit L) = L›
by (cases L) auto
lemma nat_of_lit_lit_of_nat[simp]: ‹nat_of_lit (literal_of_nat n) = n›
by auto
lemma atm_of_lit_of_nat: ‹atm_of (literal_of_nat n) = n div 2›
by auto
text ‹There is probably a more ``closed'' form from the following theorem, but it is unclear if
that is useful or not.›
lemma uminus_lit_of_nat:
‹- (literal_of_nat n) = (if even n then literal_of_nat (n+1) else literal_of_nat (n-1))›
by (auto elim!: oddE)
lemma literal_of_nat_literal_of_nat_eq[iff]: ‹literal_of_nat x = literal_of_nat xa ⟷ x = xa›
by auto presburger+
definition nat_lit_rel :: ‹(nat × nat literal) set› where
‹nat_lit_rel = br literal_of_nat (λ_. True)›
lemma ex_literal_of_nat: ‹∃bb. b = literal_of_nat bb›
by (cases b)
(auto simp: nat_of_lit_def split: if_splits; presburger; fail)+
subsection ‹Lifting to annotated literals›
fun pair_of_ann_lit :: ‹('a, 'b) ann_lit ⇒ 'a literal × 'b option› where
‹pair_of_ann_lit (Propagated L D) = (L, Some D)›
| ‹pair_of_ann_lit (Decided L) = (L, None)›
fun ann_lit_of_pair :: ‹'a literal × 'b option ⇒ ('a, 'b) ann_lit› where
‹ann_lit_of_pair (L, Some D) = Propagated L D›
| ‹ann_lit_of_pair (L, None) = Decided L›
lemma ann_lit_of_pair_alt_def:
‹ann_lit_of_pair (L, D) = (if D = None then Decided L else Propagated L (the D))›
by (cases D) auto
lemma ann_lit_of_pair_pair_of_ann_lit: ‹ann_lit_of_pair (pair_of_ann_lit L) = L›
by (cases L) auto
lemma pair_of_ann_lit_ann_lit_of_pair: ‹pair_of_ann_lit (ann_lit_of_pair L) = L›
by (cases L; cases ‹snd L›) auto
lemma literal_of_neq_eq_nat_of_lit_eq_iff: ‹literal_of_nat b = L ⟷ b = nat_of_lit L›
by (auto simp del: literal_of_nat.simps)
lemma nat_of_lit_eq_iff[iff]: ‹nat_of_lit xa = nat_of_lit x ⟷ x = xa›
apply (cases x; cases xa) by auto presburger+
definition ann_lit_rel:: ‹('a × nat) set ⇒ ('b × nat option) set ⇒
(('a × 'b) × (nat, nat) ann_lit) set› where
ann_lit_rel_internal_def:
‹ann_lit_rel R R' = {(a, b). ∃c d. (fst a, c) ∈ R ∧ (snd a, d) ∈ R' ∧
b = ann_lit_of_pair (literal_of_nat c, d)}›
section ‹Conflict Clause›
definition the_is_empty where
‹the_is_empty D = Multiset.is_empty (the D)›
section ‹Atoms with bound›
definition uint32_max :: nat where
‹uint32_max ≡ 2^32-1›
definition uint64_max :: nat where
‹uint64_max ≡ 2^64-1›
definition sint32_max :: nat where
‹sint32_max ≡ 2^31-1›
definition sint64_max :: nat where
‹sint64_max ≡ 2^63-1›
lemma uint64_max_uint_def: ‹unat (-1 :: 64 Word.word) = uint64_max›
proof -
have ‹unat (-1 :: 64 Word.word) = unat (- Numeral1 :: 64 Word.word)›
unfolding numeral.numeral_One ..
also have ‹… = uint64_max›
unfolding unat_bintrunc_neg
apply (simp add: uint64_max_def)
apply (subst numeral_eq_Suc; subst bintrunc.Suc; simp)+
done
finally show ?thesis .
qed
section ‹Operations with set of atoms.›
context
fixes 𝒜⇩i⇩n :: ‹nat multiset›
begin
abbreviation D⇩0 :: ‹(nat × nat literal) set› where
‹D⇩0 ≡ (λL. (nat_of_lit L, L)) ` set_mset (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n)›
definition length_ll_f where
‹length_ll_f W L = length (W L)›
text ‹
The following lemma was necessary at some point to prove the existence of some
list.
›
lemma ex_list_watched:
fixes W :: ‹nat literal ⇒ 'a list›
shows ‹∃aa. ∀x∈#ℒ⇩a⇩l⇩l 𝒜⇩i⇩n. nat_of_lit x < length aa ∧ aa ! nat_of_lit x = W x›
(is ‹∃aa. ?P aa›)
proof -
define D' where ‹D' = D⇩0›
define ℒ⇩a⇩l⇩l' where ‹ℒ⇩a⇩l⇩l' = ℒ⇩a⇩l⇩l›
define D'' where ‹D'' = mset_set (snd ` D')›
let ?f = ‹(λL a. a[nat_of_lit L:= W L])›
interpret comp_fun_commute ?f
apply standard
apply (case_tac ‹y = x›)
apply (solves simp)
apply (intro ext)
apply (subst (asm) lit_of_nat_nat_of_lit[symmetric])
apply (subst (asm)(3) lit_of_nat_nat_of_lit[symmetric])
apply (clarsimp simp only: comp_def intro!: list_update_swap)
done
define aa where
‹aa ≡ fold_mset ?f (replicate (1+Max (nat_of_lit ` snd ` D')) []) (mset_set (snd ` D'))›
have length_fold: ‹length (fold_mset (λL a. a[nat_of_lit L := W L]) l M) = length l› for l M
by (induction M) auto
have length_aa: ‹length aa = Suc (Max (nat_of_lit ` snd ` D'))›
unfolding aa_def D''_def[symmetric] by (simp add: length_fold)
have H: ‹x ∈# ℒ⇩a⇩l⇩l' ⟹
length l ≥ Suc (Max (nat_of_lit ` set_mset (ℒ⇩a⇩l⇩l'))) ⟹
fold_mset (λL a. a[nat_of_lit L := W L]) l (remdups_mset (ℒ⇩a⇩l⇩l')) ! nat_of_lit x = W x›
for x l ℒ⇩a⇩l⇩l'
unfolding ℒ⇩a⇩l⇩l'_def[symmetric]
apply (induction ℒ⇩a⇩l⇩l' arbitrary: l)
subgoal by simp
subgoal for xa Ls l
apply (case_tac ‹(nat_of_lit ` set_mset Ls) = {}›)
apply (solves simp)
apply (auto simp: less_Suc_eq_le length_fold)
done
done
have H': ‹aa ! nat_of_lit x = W x› if ‹x ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n› for x
using that unfolding aa_def D'_def
by (auto simp: D'_def image_image remdups_mset_def[symmetric]
less_Suc_eq_le intro!: H)
have ‹?P aa›
by (auto simp: D'_def image_image remdups_mset_def[symmetric]
less_Suc_eq_le length_aa H')
then show ?thesis
by blast
qed
definition isasat_input_bounded where
[simp]: ‹isasat_input_bounded = (∀L ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n. nat_of_lit L ≤ uint32_max)›
definition isasat_input_nempty where
[simp]: ‹isasat_input_nempty = (set_mset 𝒜⇩i⇩n ≠ {})›
definition isasat_input_bounded_nempty where
‹isasat_input_bounded_nempty = (isasat_input_bounded ∧ isasat_input_nempty)›
section ‹Set of atoms with bound›
context
assumes in_ℒ⇩a⇩l⇩l_less_uint32_max: ‹isasat_input_bounded›
begin
lemma in_ℒ⇩a⇩l⇩l_less_uint32_max': ‹L ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n ⟹ nat_of_lit L ≤ uint32_max›
using in_ℒ⇩a⇩l⇩l_less_uint32_max by auto
lemma in_𝒜⇩i⇩n_less_than_uint32_max_div_2:
‹L ∈# 𝒜⇩i⇩n ⟹ L ≤ uint32_max div 2›
using in_ℒ⇩a⇩l⇩l_less_uint32_max'[of ‹Neg L›]
unfolding Ball_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
by (auto simp: uint32_max_def)
lemma simple_clss_size_upper_div2':
assumes
lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n C› and
dist: ‹distinct_mset C› and
tauto: ‹¬tautology C› and
in_ℒ⇩a⇩l⇩l_less_uint32_max: ‹∀L ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n. nat_of_lit L < uint32_max - 1›
shows ‹size C ≤ uint32_max div 2›
proof -
let ?C = ‹atm_of `# C›
have ‹distinct_mset ?C›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain K where ‹¬count (atm_of `# C) K ≤ Suc 0›
unfolding distinct_mset_count_less_1
by auto
then have ‹count (atm_of `# C) K ≥ 2›
by auto
then obtain L L' C' where
C: ‹C = {#L, L'#} + C'› and L_L': ‹atm_of L = atm_of L'›
by (auto dest!: count_image_mset_multi_member_split_2)
then show False
using dist tauto by (auto simp: atm_of_eq_atm_of tautology_add_mset)
qed
then have card: ‹size ?C = card (set_mset ?C)›
using distinct_mset_size_eq_card by blast
have size: ‹size ?C = size C›
using dist tauto
by (induction C) (auto simp: tautology_add_mset)
have m: ‹set_mset ?C ⊆ {0..<uint32_max div 2}›
proof
fix L
assume ‹L ∈ set_mset ?C›
then have ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n)›
using lits by (auto simp: literals_are_in_ℒ⇩i⇩n_def atm_of_lit_in_atms_of
in_all_lits_of_m_ain_atms_of_iff subset_iff)
then have ‹Pos L ∈# (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n)›
using lits by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
then have ‹nat_of_lit (Pos L) < uint32_max - 1›
using in_ℒ⇩a⇩l⇩l_less_uint32_max by (auto simp: atm_of_lit_in_atms_of
in_all_lits_of_m_ain_atms_of_iff subset_iff)
then have ‹L < uint32_max div 2›
by (auto simp: atm_of_lit_in_atms_of
in_all_lits_of_m_ain_atms_of_iff subset_iff uint32_max_def)
then show ‹L ∈ {0..<uint32_max div 2}›
by (auto simp: atm_of_lit_in_atms_of uint32_max_def
in_all_lits_of_m_ain_atms_of_iff subset_iff)
qed
moreover have ‹card … = uint32_max div 2›
by auto
ultimately have ‹card (set_mset ?C) ≤ uint32_max div 2›
using card_mono[OF _ m] by auto
then show ?thesis
unfolding card[symmetric] size .
qed
lemma simple_clss_size_upper_div2:
assumes
lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n C› and
dist: ‹distinct_mset C› and
tauto: ‹¬tautology C›
shows ‹size C ≤ 1 + uint32_max div 2›
proof -
let ?C = ‹atm_of `# C›
have ‹distinct_mset ?C›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain K where ‹¬count (atm_of `# C) K ≤ Suc 0›
unfolding distinct_mset_count_less_1
by auto
then have ‹count (atm_of `# C) K ≥ 2›
by auto
then obtain L L' C' where
C: ‹C = {#L, L'#} + C'› and L_L': ‹atm_of L = atm_of L'›
by (auto dest!: count_image_mset_multi_member_split_2)
then show False
using dist tauto by (auto simp: atm_of_eq_atm_of tautology_add_mset)
qed
then have card: ‹size ?C = card (set_mset ?C)›
using distinct_mset_size_eq_card by blast
have size: ‹size ?C = size C›
using dist tauto
by (induction C) (auto simp: tautology_add_mset)
have m: ‹set_mset ?C ⊆ {0..uint32_max div 2}›
proof
fix L
assume ‹L ∈ set_mset ?C›
then have ‹L ∈ atms_of (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n)›
using lits by (auto simp: literals_are_in_ℒ⇩i⇩n_def atm_of_lit_in_atms_of
in_all_lits_of_m_ain_atms_of_iff subset_iff)
then have ‹Neg L ∈# (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n)›
using lits by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff)
then have ‹nat_of_lit (Neg L) ≤ uint32_max›
using in_ℒ⇩a⇩l⇩l_less_uint32_max by (auto simp: atm_of_lit_in_atms_of
in_all_lits_of_m_ain_atms_of_iff subset_iff)
then have ‹L ≤ uint32_max div 2›
by (auto simp: atm_of_lit_in_atms_of
in_all_lits_of_m_ain_atms_of_iff subset_iff uint32_max_def)
then show ‹L ∈ {0 .. uint32_max div 2}›
by (auto simp: atm_of_lit_in_atms_of uint32_max_def
in_all_lits_of_m_ain_atms_of_iff subset_iff)
qed
moreover have ‹card … = 1 + uint32_max div 2›
by auto
ultimately have ‹card (set_mset ?C) ≤ 1 + uint32_max div 2›
using card_mono[OF _ m] by auto
then show ?thesis
unfolding card[symmetric] size .
qed
lemma clss_size_uint32_max:
assumes
lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n C› and
dist: ‹distinct_mset C›
shows ‹size C ≤ uint32_max + 2›
proof -
let ?posC = ‹filter_mset is_pos C›
let ?negC = ‹filter_mset is_neg C›
have C: ‹C = ?posC + ?negC›
apply (subst multiset_partition[of _ is_pos])
by auto
have ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n ?posC›
by (rule literals_are_in_ℒ⇩i⇩n_mono[OF lits]) auto
moreover have ‹distinct_mset ?posC›
by (rule distinct_mset_mono[OF _dist]) auto
ultimately have pos: ‹size ?posC ≤ 1 + uint32_max div 2›
by (rule simple_clss_size_upper_div2) (auto simp: tautology_decomp)
have ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n ?negC›
by (rule literals_are_in_ℒ⇩i⇩n_mono[OF lits]) auto
moreover have ‹distinct_mset ?negC›
by (rule distinct_mset_mono[OF _dist]) auto
ultimately have neg: ‹size ?negC ≤ 1 + uint32_max div 2›
by (rule simple_clss_size_upper_div2) (auto simp: tautology_decomp)
show ?thesis
apply (subst C)
apply (subst size_union)
using pos neg by linarith
qed
lemma clss_size_upper:
assumes
lits: ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n C› and
dist: ‹distinct_mset C› and
in_ℒ⇩a⇩l⇩l_less_uint32_max: ‹∀L ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n. nat_of_lit L < uint32_max - 1›
shows ‹size C ≤ uint32_max›
proof -
let ?A = ‹remdups_mset (atm_of `# C)›
have [simp]: ‹distinct_mset (poss ?A)› ‹distinct_mset (negs ?A)›
by (simp_all add: distinct_image_mset_inj inj_on_def)
have ‹C ⊆# poss ?A + negs ?A›
apply (rule distinct_subseteq_iff[THEN iffD1])
subgoal by (auto simp: dist distinct_mset_add disjunct_not_in)
subgoal by (auto simp: dist distinct_mset_add disjunct_not_in)
subgoal
apply rule
using literal.exhaust_sel by (auto simp: image_iff)
done
have [simp]: ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n (poss ?A)› ‹literals_are_in_ℒ⇩i⇩n 𝒜⇩i⇩n (negs ?A)›
using lits
by (auto simp: literals_are_in_ℒ⇩i⇩n_negs_remdups_mset literals_are_in_ℒ⇩i⇩n_poss_remdups_mset)
have ‹¬ tautology (poss ?A)› ‹¬ tautology (negs ?A)›
by (auto simp: tautology_decomp)
then have ‹size (poss ?A) ≤ uint32_max div 2› and ‹size (negs ?A) ≤ uint32_max div 2›
using simple_clss_size_upper_div2'[of ‹poss ?A›]
simple_clss_size_upper_div2'[of ‹negs ?A›] in_ℒ⇩a⇩l⇩l_less_uint32_max
by auto
then have ‹size C ≤ uint32_max div 2 + uint32_max div 2›
using ‹C ⊆# poss (remdups_mset (atm_of `# C)) + negs (remdups_mset (atm_of `# C))›
size_mset_mono by fastforce
then show ?thesis by (auto simp: uint32_max_def)
qed
lemma
assumes
lits: ‹literals_are_in_ℒ⇩i⇩n_trail 𝒜⇩i⇩n M› and
n_d: ‹no_dup M›
shows
literals_are_in_ℒ⇩i⇩n_trail_length_le_uint32_max:
‹length M ≤ Suc (uint32_max div 2)› and
literals_are_in_ℒ⇩i⇩n_trail_count_decided_uint32_max:
‹count_decided M ≤ Suc (uint32_max div 2)› and
literals_are_in_ℒ⇩i⇩n_trail_get_level_uint32_max:
‹get_level M L ≤ Suc (uint32_max div 2)›
proof -
have ‹length M = card (atm_of ` lits_of_l M)›
using no_dup_length_eq_card_atm_of_lits_of_l[OF n_d] .
moreover have ‹atm_of ` lits_of_l M ⊆ set_mset 𝒜⇩i⇩n›
using lits unfolding literals_are_in_ℒ⇩i⇩n_trail_atm_of by auto
ultimately have ‹length M ≤ card (set_mset 𝒜⇩i⇩n)›
by (simp add: card_mono)
moreover {
have ‹set_mset 𝒜⇩i⇩n ⊆ {0 ..< (uint32_max div 2) + 1}›
using in_𝒜⇩i⇩n_less_than_uint32_max_div_2 by (fastforce simp: in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff
Ball_def atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n uint32_max_def)
from subset_eq_atLeast0_lessThan_card[OF this] have ‹card (set_mset 𝒜⇩i⇩n) ≤ uint32_max div 2 + 1›
.
}
ultimately show ‹length M ≤ Suc (uint32_max div 2)›
by linarith
moreover have ‹count_decided M ≤ length M›
unfolding count_decided_def by auto
ultimately show ‹count_decided M ≤ Suc (uint32_max div 2)› by simp
then show ‹get_level M L ≤ Suc (uint32_max div 2)›
using count_decided_ge_get_level[of M L]
by simp
qed
lemma length_trail_uint32_max_div2:
fixes M :: ‹(nat, 'b) ann_lits›
assumes
M_ℒ⇩a⇩l⇩l: ‹∀L∈set M. lit_of L ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n› and
n_d: ‹no_dup M›
shows ‹length M ≤ uint32_max div 2 + 1›
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 𝒜⇩i⇩n)›
apply (subst distinct_subseteq_iff[THEN iffD1])
using assms dist_atm_M
by (auto 5 5 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 𝒜⇩i⇩n)))›
by (auto simp: inj_on_def)
have H: ‹xa ∈# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n ⟹ atm_of xa ≤ uint32_max div 2› for xa
using in_ℒ⇩a⇩l⇩l_less_uint32_max
by (cases xa) (auto simp: uint32_max_def)
have ‹remdups_mset (atm_of `# ℒ⇩a⇩l⇩l 𝒜⇩i⇩n) ⊆# 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 𝒜⇩i⇩n)) = size (remdups_mset (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n))›
by simp
ultimately have 2: ‹size (remdups_mset (atm_of `# (ℒ⇩a⇩l⇩l 𝒜⇩i⇩n))) ≤ 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 𝒜⇩i⇩n)))›
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
end
end
section ‹Instantion for code generation›
instantiation literal :: (default) default
begin
definition default_literal where
‹default_literal = Pos default›
instance by standard
end
instantiation fmap :: (type, type) default
begin
definition default_fmap where
‹default_fmap = fmempty›
instance by standard
end
subsection ‹Literals as Natural Numbers›
definition propagated where
‹propagated L C = (L, Some C)›
definition decided where
‹decided L = (L, None)›
definition uminus_lit_imp :: ‹nat ⇒ nat› where
‹uminus_lit_imp L = bitXOR L 1›
lemma uminus_lit_imp_uminus:
‹(RETURN o uminus_lit_imp, RETURN o uminus) ∈
nat_lit_rel →⇩f ⟨nat_lit_rel⟩nres_rel›
unfolding bitXOR_1_if_mod_2 uminus_lit_imp_def
by (intro frefI nres_relI) (auto simp: uminus_lit_imp_def case_prod_beta p2rel_def
br_def nat_lit_rel_def split: option.splits, presburger)
subsection ‹State Conversion›
subsubsection ‹Functions and Types:›
subsubsection ‹More Operations›
subsection ‹Code Generation›
subsubsection ‹More Operations›
definition literals_to_update_wl_empty :: ‹nat twl_st_wl ⇒ bool› where
‹literals_to_update_wl_empty = (λ(M, N, D, NE, UE, Q, W). Q = {#})›
lemma in_nat_list_rel_list_all2_in_set_iff:
‹(a, aa) ∈ nat_lit_rel ⟹
list_all2 (λx x'. (x, x') ∈ nat_lit_rel) b ba ⟹
a ∈ set b ⟷ aa ∈ set ba›
apply (subgoal_tac ‹length b = length ba›)
subgoal
apply (rotate_tac 2)
apply (induction b ba rule: list_induct2)
apply (solves simp)
apply (auto simp: p2rel_def nat_lit_rel_def br_def, presburger)[]
done
subgoal using list_all2_lengthD by auto
done
definition is_decided_wl where
‹is_decided_wl L ⟷ snd L = None›
lemma ann_lit_of_pair_if:
‹ann_lit_of_pair (L, D) = (if D = None then Decided L else Propagated L (the D))›
by (cases D) auto
definition get_maximum_level_remove where
‹get_maximum_level_remove M D L = get_maximum_level M (remove1_mset L D)›
lemma in_list_all2_ex_in: ‹a ∈ set xs ⟹ list_all2 R xs ys ⟹ ∃b ∈ set ys. R a b›
apply (subgoal_tac ‹length xs = length ys›)
apply (rotate_tac 2)
apply (induction xs ys rule: list_induct2)
apply ((solves auto)+)[2]
using list_all2_lengthD by blast
definition find_decomp_wl_imp :: ‹(nat, nat) ann_lits ⇒ nat clause ⇒ nat literal ⇒ (nat, nat) ann_lits nres› where
‹find_decomp_wl_imp = (λM⇩0 D L. do {
let lev = get_maximum_level M⇩0 (remove1_mset (-L) D);
let k = count_decided M⇩0;
(_, M) ←
WHILE⇩T⇗λ(j, M). j = count_decided M ∧ j ≥ lev ∧
(M = [] ⟶ j = lev) ∧
(∃M'. M⇩0 = M' @ M ∧ (j = lev ⟶ M' ≠ [] ∧ is_decided (last M')))⇖
(λ(j, M). j > lev)
(λ(j, M). do {
ASSERT(M ≠ []);
if is_decided (hd M)
then RETURN (j-1, tl M)
else RETURN (j, tl M)}
)
(k, M⇩0);
RETURN M
})›
lemma ex_decomp_get_ann_decomposition_iff:
‹(∃M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M)) ⟷
(∃M2. M = M2 @ Decided K # M1)›
using get_all_ann_decomposition_ex by fastforce
lemma count_decided_tl_if:
‹M ≠ [] ⟹ count_decided (tl M) = (if is_decided (hd M) then count_decided M - 1 else count_decided M)›
by (cases M) auto
lemma count_decided_butlast:
‹count_decided (butlast xs) = (if is_decided (last xs) then count_decided xs - 1 else count_decided xs)›
by (cases xs rule: rev_cases) (auto simp: count_decided_def)
definition find_decomp_wl' where
‹find_decomp_wl' =
(λ(M::(nat, nat) ann_lits) (D::nat clause) (L::nat literal).
SPEC(λM1. ∃K M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ∧
get_level M K = get_maximum_level M (D - {#-L#}) + 1))›
definition get_conflict_wl_is_None :: ‹nat twl_st_wl ⇒ bool› where
‹get_conflict_wl_is_None = (λ(M, N, D, NE, UE, Q, W). is_None D)›
lemma get_conflict_wl_is_None: ‹get_conflict_wl S = None ⟷ get_conflict_wl_is_None S›
by (cases S) (auto simp: get_conflict_wl_is_None_def split: option.splits)
lemma watched_by_nth_watched_app':
‹watched_by S K = ((snd o snd o snd o snd o snd o snd o snd o snd) S) K›
by (cases S) (auto)
lemma hd_decided_count_decided_ge_1:
‹x ≠ [] ⟹ is_decided (hd x) ⟹ Suc 0 ≤ count_decided x›
by (cases x) auto
definition (in -) find_decomp_wl_imp' :: ‹(nat, nat) ann_lits ⇒ nat clause_l list ⇒ nat ⇒
nat clause ⇒ nat clauses ⇒ nat clauses ⇒ nat lit_queue_wl ⇒
(nat literal ⇒ nat watched) ⇒ _ ⇒ (nat, nat) ann_lits nres› where
‹find_decomp_wl_imp' = (λM N U D NE UE W Q L. find_decomp_wl_imp M D L)›
definition is_decided_hd_trail_wl where
‹is_decided_hd_trail_wl S = is_decided (hd (get_trail_wl S))›
definition is_decided_hd_trail_wll :: ‹nat twl_st_wl ⇒ bool nres› where
‹is_decided_hd_trail_wll = (λ(M, N, D, NE, UE, Q, W).
RETURN (is_decided (hd M))
)›
lemma Propagated_eq_ann_lit_of_pair_iff:
‹Propagated x21 x22 = ann_lit_of_pair (a, b) ⟷ x21 = a ∧ b = Some x22›
by (cases b) auto
lemma set_mset_all_lits_of_mm_atms_of_ms_iff:
‹set_mset (all_lits_of_mm A) = set_mset (ℒ⇩a⇩l⇩l 𝒜) ⟷ atms_of_ms (set_mset A) = atms_of (ℒ⇩a⇩l⇩l 𝒜)›
by (force simp add: atms_of_s_def in_all_lits_of_mm_ain_atms_of_iff atms_of_ms_def
atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n atms_of_def atm_of_eq_atm_of uminus_𝒜⇩i⇩n_iff
eq_commute[of ‹set_mset (all_lits_of_mm _)› ‹set_mset (ℒ⇩a⇩l⇩l _)›]
dest: multi_member_split)
definition card_max_lvl where
‹card_max_lvl M C ≡ size (filter_mset (λL. get_level M L = count_decided M) C)›
lemma card_max_lvl_add_mset: ‹card_max_lvl M (add_mset L C) =
(if get_level M L = count_decided M then 1 else 0) +
card_max_lvl M C›
by (auto simp: card_max_lvl_def)
lemma card_max_lvl_empty[simp]: ‹card_max_lvl M {#} = 0›
by (auto simp: card_max_lvl_def)
lemma card_max_lvl_all_poss:
‹card_max_lvl M C = card_max_lvl M (poss (atm_of `# C))›
unfolding card_max_lvl_def
apply (induction C)
subgoal by auto
subgoal for L C
using get_level_uminus[of M L]
by (cases L) (auto)
done
lemma card_max_lvl_distinct_cong:
assumes
‹⋀L. get_level M (Pos L) = count_decided M ⟹ (L ∈ atms_of C) ⟹ (L ∈ atms_of C')› and
‹⋀L. get_level M (Pos L) = count_decided M ⟹ (L ∈ atms_of C') ⟹ (L ∈ atms_of C)› and
‹distinct_mset C› ‹¬tautology C› and
‹distinct_mset C'› ‹¬tautology C'›
shows ‹card_max_lvl M C = card_max_lvl M C'›
proof -
have [simp]: ‹NO_MATCH (Pos x) L ⟹ get_level M L = get_level M (Pos (atm_of L))› for x L
by (simp add: get_level_def)
have [simp]: ‹atm_of L ∉ atms_of C' ⟷ L ∉# C' ∧ -L ∉# C'› for L C'
by (cases L) (auto simp: atm_iff_pos_or_neg_lit)
then have [iff]: ‹atm_of L ∈ atms_of C' ⟷ L ∈# C' ∨ -L ∈# C'› for L C'
by blast
have H: ‹distinct_mset {#L ∈# poss (atm_of `# C). get_level M L = count_decided M#}›
if ‹distinct_mset C› ‹¬tautology C› for C
using that by (induction C) (auto simp: tautology_add_mset atm_of_eq_atm_of)
show ?thesis
apply (subst card_max_lvl_all_poss)
apply (subst (2) card_max_lvl_all_poss)
unfolding card_max_lvl_def
apply (rule arg_cong[of _ _ size])
apply (rule distinct_set_mset_eq)
subgoal by (rule H) (use assms in fast)+
subgoal by (rule H) (use assms in fast)+
subgoal using assms by (auto simp: atms_of_def imageI image_iff) blast+
done
qed
end