theory CDCL_Conflict_Minimisation
imports
Watched_Literals_Watch_List_Domain
WB_More_Refinement
WB_More_Refinement_List "List-Index.List_Index" "HOL-Imperative_HOL.Imperative_HOL"
begin
text ‹We implement the conflict minimisation as presented by Sörensson and Biere
(``Minimizing Learned Clauses''').
We refer to the paper for further details, but the general idea is to produce a series of resolution
steps such that eventually (i.e., after enough resolution steps) no new literals has been introduced
in the conflict clause.
The resolution steps are only done with the reasons of the of literals
appearing in the trail. Hence these steps are terminating: we are ``shortening'' the trail we have
to consider with each resolution step. Remark that the shortening refers to the length of the trail
we have to consider, not the levels.
The concrete proof was harder than we initially expected. Our first proof try was to certify the
resolution steps. While this worked out, adding caching on top of that turned to be rather hard,
since it is not obvious how to add resolution steps in the middle of the current proof if the
literal has already been removed (basically we would have to prove termination and confluence of the
rewriting system).
Therefore, we worked instead directly on the entailment of the literals of the conflict clause
(up to the point in the trail we currently considering, which is also the termination measure).
The previous try is still present in our formalisation (see \<^term>‹minimize_conflict_support›, which
we however only use for the termination proof).
The algorithm presented above does not distinguish between literals propagated at the same level:
we cannot reuse information about failures to cut branches. There is a variant of the algorithm
presented above that is able to do so (Van Gelder, ``Improved Conflict-Clause Minimization
Leads to Improved Propositional Proof Traces''). The algorithm is however more complicated and has
only be implemented in very few solvers (at least lingeling and cadical) and is especially not part
of glucose nor cryptominisat. Therefore, we have decided to not implement it: It is probably not
worth it and requires some additional data structures.
›
declare cdcl⇩W_restart_mset_state[simp]
type_synonym out_learned = ‹nat clause_l›
text ‹The data structure contains the (unique) literal of highest at position one. This is useful
since this is what we want to have at the end (propagation clause) and we can skip the first
literal when minimising the clause.
›
definition out_learned :: ‹(nat, nat) ann_lits ⇒ nat clause option ⇒ out_learned ⇒ bool› where
‹out_learned M D out ⟷
out ≠ [] ∧
(D = None ⟶ length out = 1) ∧
(D ≠ None ⟶ mset (tl out) = filter_mset (λL. get_level M L < count_decided M) (the D))›
definition out_learned_confl :: ‹(nat, nat) ann_lits ⇒ nat clause option ⇒ out_learned ⇒ bool› where
‹out_learned_confl M D out ⟷
out ≠ [] ∧ (D ≠ None ∧ mset out = the D)›
lemma out_learned_Cons_None[simp]:
‹out_learned (L # aa) None ao ⟷ out_learned aa None ao›
by (auto simp: out_learned_def)
lemma out_learned_tl_None[simp]:
‹out_learned (tl aa) None ao ⟷ out_learned aa None ao›
by (auto simp: out_learned_def)
definition index_in_trail :: ‹('v, 'a) ann_lits ⇒ 'v literal ⇒ nat› where
‹index_in_trail M L = index (map (atm_of o lit_of) (rev M)) (atm_of L)›
lemma Propagated_in_trail_entailed:
assumes
invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, N, U, D)› and
in_trail: ‹Propagated L C ∈ set M›
shows
‹M ⊨as CNot (remove1_mset L C)› and ‹L ∈# C› and ‹N + U ⊨pm C› and
‹K ∈# remove1_mset L C ⟹ index_in_trail M K < index_in_trail M L› and
‹¬tautology C› and ‹distinct_mset C›
proof -
obtain M2 M1 where
M: ‹M = M2 @ Propagated L C # M1›
using split_list[OF in_trail] by metis
have ‹a @ Propagated L mark # b = trail (M, N, U, D) ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (M, N, U, D)›
for L mark a b
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by fast+
then have L_E: ‹L ∈# C› and M1_E: ‹M1 ⊨as CNot (remove1_mset L C)›
unfolding M by force+
then have M_E: ‹M ⊨as CNot (remove1_mset L C)›
unfolding M by (simp add: true_annots_append_l)
show ‹M ⊨as CNot (remove1_mset L C)› and ‹L ∈# C›
using L_E M_E by fast+
have ‹set (get_all_mark_of_propagated (trail (M, N, U, D)))
⊆ set_mset (cdcl⇩W_restart_mset.clauses (M, N, U, D))›
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by fast
then have ‹C ∈# N + U›
using in_trail cdcl⇩W_restart_mset.in_get_all_mark_of_propagated_in_trail[of C M]
by (auto simp: clauses_def)
then show ‹N + U ⊨pm C› by auto
have n_d: ‹no_dup M›
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
show ‹index_in_trail M K < index_in_trail M L› if K_C: ‹K ∈# remove1_mset L C›
proof -
have
KL: ‹atm_of K ≠ atm_of L› and
uK_M1: ‹-K ∈ lits_of_l M1› and
L: ‹L ∉ lit_of ` (set M2 ∪ set M1)› ‹-L ∉ lit_of ` (set M2 ∪ set M1)›
using M1_E K_C n_d unfolding M true_annots_true_cls_def_iff_negation_in_model
by (auto dest!: multi_member_split simp: atm_of_eq_atm_of lits_of_def uminus_lit_swap
Decided_Propagated_in_iff_in_lits_of_l)
have L_M1: ‹atm_of L ∉ (atm_of ∘ lit_of) ` set M1›
using L by (auto simp: image_Un atm_of_eq_atm_of)
have K_M1: ‹atm_of K ∈ (atm_of ∘ lit_of) ` set M1›
using uK_M1 by (auto simp: lits_of_def image_image comp_def uminus_lit_swap)
show ?thesis
using KL L_M1 K_M1 unfolding index_in_trail_def M by (auto simp: index_append)
qed
have ‹¬tautology(remove1_mset L C)›
by (rule consistent_CNot_not_tautology[of ‹lits_of_l M1›])
(use n_d M1_E in ‹auto dest: distinct_consistent_interp no_dup_appendD
simp: true_annots_true_cls M›)
then show ‹¬tautology C›
using multi_member_split[OF L_E] M1_E n_d
by (auto simp: tautology_add_mset true_annots_true_cls_def_iff_negation_in_model M
dest!: multi_member_split in_lits_of_l_defined_litD)
show ‹distinct_mset (C)›
using dist ‹C ∈# N + U› unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
by (auto dest: multi_member_split)
qed
text ‹This predicate corresponds to one resolution step.›
inductive minimize_conflict_support :: ‹('v, 'v clause) ann_lits ⇒ 'v clause ⇒ 'v clause ⇒ bool›
for M where
resolve_propa:
‹minimize_conflict_support M (add_mset (-L) C) (C + remove1_mset L E)›
if ‹Propagated L E ∈ set M› |
remdups: ‹minimize_conflict_support M (add_mset L C) C›
lemma index_in_trail_uminus[simp]: ‹index_in_trail M (-L) = index_in_trail M L›
by (auto simp: index_in_trail_def)
text ‹This is the termination argument of the conflict minimisation: the multiset of the levels
decreases (for the multiset ordering).›
definition minimize_conflict_support_mes :: ‹('v, 'v clause) ann_lits ⇒ 'v clause ⇒ nat multiset›
where
‹minimize_conflict_support_mes M C = index_in_trail M `# C›
context
fixes M :: ‹('v, 'v clause) ann_lits› and N U :: ‹'v clauses› and
D :: ‹'v clause option›
assumes invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, N, U, D)›
begin
private lemma
no_dup: ‹no_dup M› and
consistent: ‹consistent_interp (lits_of_l M)›
using invs unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by simp_all
lemma minimize_conflict_support_entailed_trail:
assumes ‹minimize_conflict_support M C E› and ‹M ⊨as CNot C›
shows ‹M ⊨as CNot E›
using assms
proof (induction rule: minimize_conflict_support.induct)
case (resolve_propa L E C) note in_trail = this(1) and M_C = this(2)
then show ?case
using Propagated_in_trail_entailed[OF invs in_trail] by (auto dest!: multi_member_split)
next
case (remdups L C)
then show ?case
by auto
qed
lemma rtranclp_minimize_conflict_support_entailed_trail:
assumes ‹(minimize_conflict_support M)⇧*⇧* C E› and ‹M ⊨as CNot C›
shows ‹M ⊨as CNot E›
using assms apply (induction rule: rtranclp_induct)
subgoal by fast
subgoal using minimize_conflict_support_entailed_trail by fast
done
lemma minimize_conflict_support_mes:
assumes ‹minimize_conflict_support M C E›
shows ‹minimize_conflict_support_mes M E < minimize_conflict_support_mes M C›
using assms unfolding minimize_conflict_support_mes_def
proof (induction rule: minimize_conflict_support.induct)
case (resolve_propa L E C) note in_trail = this
let ?f = ‹λxa. index (map (λa. atm_of (lit_of a)) (rev M)) xa›
have ‹?f (atm_of x) < ?f (atm_of L)› if x: ‹x ∈# remove1_mset L E› for x
proof -
obtain M2 M1 where
M: ‹M = M2 @ Propagated L E # M1›
using split_list[OF in_trail] by metis
have ‹a @ Propagated L mark # b = trail (M, N, U, D) ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› for L mark a b
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by fast
then have L_E: ‹L ∈# E› and M_E: ‹M1 ⊨as CNot (remove1_mset L E)›
unfolding M by force+
then have ‹-x ∈ lits_of_l M1›
using x unfolding true_annots_true_cls_def_iff_negation_in_model by auto
then have ‹?f (atm_of x) < length M1›
using no_dup
by (auto simp: M lits_of_def index_append Decided_Propagated_in_iff_in_lits_of_l
uminus_lit_swap)
moreover have ‹?f (atm_of L) = length M1›
using no_dup unfolding M by (auto simp: index_append Decided_Propagated_in_iff_in_lits_of_l
atm_of_eq_atm_of lits_of_def)
ultimately show ?thesis by auto
qed
then show ?case by (auto simp: comp_def index_in_trail_def)
next
case (remdups L C)
then show ?case by auto
qed
lemma wf_minimize_conflict_support:
shows ‹wf {(C', C). minimize_conflict_support M C C'}›
apply (rule wf_if_measure_in_wf[of ‹{(C', C). C' < C}› _ ‹minimize_conflict_support_mes M›])
subgoal using wf .
subgoal using minimize_conflict_support_mes by auto
done
end
lemma conflict_minimize_step:
assumes
‹NU ⊨p add_mset L C› and
‹NU ⊨p add_mset (-L) D› and
‹⋀K'. K' ∈# C ⟹ NU ⊨p add_mset (-K') D›
shows ‹NU ⊨p D›
proof -
have ‹NU ⊨p D + C›
using assms(1,2) true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or by blast
then show ?thesis
using assms(3)
proof (induction C)
case empty
then show ?case
using true_clss_cls_in true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or by fastforce
next
case (add x C) note IH =this(1) and NU_DC = this(2) and entailed = this(3)
have ‹NU ⊨p D + C + D›
using entailed[of x] NU_DC
true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[of NU ‹-x› ‹D + C› D]
by auto
then have ‹NU ⊨p D + C›
by (metis add.comm_neutral diff_add_zero sup_subset_mset_def true_clss_cls_sup_iff_add)
from IH[OF this] entailed show ?case by auto
qed
qed
text ‹This function filters the clause by the levels up the level of the given literal. This is
the part the conflict clause that is considered when testing if the given literal is redundant.›
definition filter_to_poslev where
‹filter_to_poslev M L D = filter_mset (λK. index_in_trail M K < index_in_trail M L) D›
lemma filter_to_poslev_uminus[simp]:
‹filter_to_poslev M (-L) D = filter_to_poslev M L D›
by (auto simp: filter_to_poslev_def)
lemma filter_to_poslev_empty[simp]:
‹filter_to_poslev M L {#} = {#}›
by (auto simp: filter_to_poslev_def)
lemma filter_to_poslev_mono:
‹index_in_trail M K' ≤ index_in_trail M L ⟹
filter_to_poslev M K' D ⊆# filter_to_poslev M L D›
unfolding filter_to_poslev_def
by (auto simp: multiset_filter_mono2)
lemma filter_to_poslev_mono_entailement:
‹index_in_trail M K' ≤ index_in_trail M L ⟹
NU ⊨p filter_to_poslev M K' D ⟹ NU ⊨p filter_to_poslev M L D›
by (metis (full_types) filter_to_poslev_mono subset_mset.le_iff_add true_clss_cls_mono_r)
lemma filter_to_poslev_mono_entailement_add_mset:
‹index_in_trail M K' ≤ index_in_trail M L ⟹
NU ⊨p add_mset J (filter_to_poslev M K' D) ⟹ NU ⊨p add_mset J (filter_to_poslev M L D)›
by (metis filter_to_poslev_mono mset_subset_eq_add_mset_cancel subset_mset.le_iff_add
true_clss_cls_mono_r)
lemma conflict_minimize_intermediate_step:
assumes
‹NU ⊨p add_mset L C› and
K'_C: ‹⋀K'. K' ∈# C ⟹ NU ⊨p add_mset (-K') D ∨ K' ∈# D›
shows ‹NU ⊨p add_mset L D›
proof -
have ‹NU ⊨p add_mset L C + D›
using assms(1) true_clss_cls_mono_r by blast
then show ?thesis
using assms(2)
proof (induction C)
case empty
then show ?case
using true_clss_cls_in true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or by fastforce
next
case (add x C) note IH =this(1) and NU_DC = this(2) and entailed = this(3)
have 1: ‹NU ⊨p add_mset x (add_mset L (D + C))›
using NU_DC by (auto simp: add_mset_commute ac_simps)
moreover have 2: ‹remdups_mset (add_mset L (D + C + D)) = remdups_mset (add_mset L (C + D))›
by (auto simp: remdups_mset_def)
moreover have 3: ‹remdups_mset (D + C + D) = remdups_mset (D + C)›
by (auto simp: remdups_mset_def)
moreover have ‹x ∈# D ⟹ NU ⊨p add_mset L (D + C + D)›
using 1
apply (subst (asm) true_clss_cls_remdups_mset[symmetric])
apply (subst true_clss_cls_remdups_mset[symmetric])
by (auto simp: 2 3)
ultimately have ‹NU ⊨p add_mset L (D + C + D)›
using entailed[of x] NU_DC
true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[of NU ‹-x› ‹add_mset L D + C› D]
by auto
moreover have ‹remdups_mset (D + (C + D)) = remdups_mset (D + C)›
by (auto simp: remdups_mset_def)
ultimately have ‹NU ⊨p add_mset L C + D›
apply (subst true_clss_cls_remdups_mset[symmetric])
apply (subst (asm) true_clss_cls_remdups_mset[symmetric])
by (auto simp add: 3 2 add.commute simp del: true_clss_cls_remdups_mset)
from IH[OF this] entailed show ?case by auto
qed
qed
lemma conflict_minimize_intermediate_step_filter_to_poslev:
assumes
lev_K_L: ‹⋀K'. K' ∈# C ⟹ index_in_trail M K' < index_in_trail M L› and
NU_LC: ‹NU ⊨p add_mset L C› and
K'_C: ‹⋀K'. K' ∈# C ⟹ NU ⊨p add_mset (-K') (filter_to_poslev M L D) ∨
K' ∈# filter_to_poslev M L D›
shows ‹NU ⊨p add_mset L (filter_to_poslev M L D)›
proof -
have C_entailed: ‹K' ∈# C ⟹ NU ⊨p add_mset (-K') (filter_to_poslev M L D) ∨
K' ∈# filter_to_poslev M L D› for K'
using filter_to_poslev_mono[of M K' L D] lev_K_L[of K'] K'_C[of K']
true_clss_cls_mono_r[of _ ‹ add_mset (- K') (filter_to_poslev M K' D)› ]
by (auto simp: mset_subset_eq_exists_conv)
show ?thesis
using conflict_minimize_intermediate_step[OF NU_LC C_entailed] by fast
qed
datatype minimize_status = SEEN_FAILED | SEEN_REMOVABLE | SEEN_UNKNOWN
instance minimize_status :: heap
proof standard
let ?f = ‹λs. case s of SEEN_FAILED ⇒ (0 :: nat) | SEEN_REMOVABLE ⇒ 1 | SEEN_UNKNOWN ⇒ 2›
have ‹inj ?f›
by (auto simp: inj_def split: minimize_status.splits)
then show ‹∃to_nat. inj (to_nat :: minimize_status ⇒ nat)›
by blast
qed
instantiation minimize_status :: default
begin
definition default_minimize_status where
‹default_minimize_status = SEEN_UNKNOWN›
instance by standard
end
type_synonym 'v conflict_min_analyse = ‹('v literal × 'v clause) list›
type_synonym 'v conflict_min_cach = ‹'v ⇒ minimize_status›
definition get_literal_and_remove_of_analyse
:: ‹'v conflict_min_analyse ⇒ ('v literal × 'v conflict_min_analyse) nres› where
‹get_literal_and_remove_of_analyse analyse =
SPEC(λ(L, ana). L ∈# snd (hd analyse) ∧ tl ana = tl analyse ∧ ana ≠ [] ∧
hd ana = (fst (hd analyse), snd (hd (analyse)) - {#L#}))›
definition mark_failed_lits
:: ‹_ ⇒ 'v conflict_min_analyse ⇒ 'v conflict_min_cach ⇒ 'v conflict_min_cach nres›
where
‹mark_failed_lits NU analyse cach = SPEC(λcach'.
(∀L. cach' L = SEEN_REMOVABLE ⟶ cach L = SEEN_REMOVABLE))›
definition conflict_min_analysis_inv
:: ‹('v, 'a) ann_lits ⇒ 'v conflict_min_cach ⇒ 'v clauses ⇒ 'v clause ⇒ bool›
where
‹conflict_min_analysis_inv M cach NU D ⟷
(∀L. -L ∈ lits_of_l M ⟶ cach (atm_of L) = SEEN_REMOVABLE ⟶
set_mset NU ⊨p add_mset (-L) (filter_to_poslev M L D))›
lemma conflict_min_analysis_inv_update_removable:
‹no_dup M ⟹ -L ∈ lits_of_l M ⟹
conflict_min_analysis_inv M (cach(atm_of L := SEEN_REMOVABLE)) NU D ⟷
conflict_min_analysis_inv M cach NU D ∧ set_mset NU ⊨p add_mset (-L) (filter_to_poslev M L D)›
by (auto simp: conflict_min_analysis_inv_def atm_of_eq_atm_of dest: no_dup_consistentD)
lemma conflict_min_analysis_inv_update_failed:
‹conflict_min_analysis_inv M cach NU D ⟹
conflict_min_analysis_inv M (cach(L := SEEN_FAILED)) NU D›
by (auto simp: conflict_min_analysis_inv_def)
fun conflict_min_analysis_stack
:: ‹('v, 'a) ann_lits ⇒ 'v clauses ⇒ 'v clause ⇒ 'v conflict_min_analyse ⇒ bool›
where
‹conflict_min_analysis_stack M NU D [] ⟷ True› |
‹conflict_min_analysis_stack M NU D ((L, E) # []) ⟷ -L ∈ lits_of_l M› |
‹conflict_min_analysis_stack M NU D ((L, E) # (L', E') # analyse) ⟷
(∃C. set_mset NU ⊨p add_mset (-L') C ∧
(∀K∈#C-add_mset L E'. set_mset NU ⊨p (filter_to_poslev M L' D) + {#-K#} ∨
K ∈# filter_to_poslev M L' D) ∧
(∀K∈#C. index_in_trail M K < index_in_trail M L') ∧
E' ⊆# C) ∧
-L' ∈ lits_of_l M ∧
-L ∈ lits_of_l M ∧
index_in_trail M L < index_in_trail M L' ∧
conflict_min_analysis_stack M NU D ((L', E') # analyse)›
lemma conflict_min_analysis_stack_change_hd:
‹conflict_min_analysis_stack M NU D ((L, E) # ana) ⟹
conflict_min_analysis_stack M NU D ((L, E') # ana)›
by (cases ana, auto)
lemma conflict_min_analysis_stack_sorted:
‹conflict_min_analysis_stack M NU D analyse ⟹
sorted (map (index_in_trail M o fst) analyse)›
by (induction rule: conflict_min_analysis_stack.induct)
auto
lemma conflict_min_analysis_stack_sorted_and_distinct:
‹conflict_min_analysis_stack M NU D analyse ⟹
sorted (map (index_in_trail M o fst) analyse) ∧
distinct (map (index_in_trail M o fst) analyse)›
by (induction rule: conflict_min_analysis_stack.induct)
auto
lemma conflict_min_analysis_stack_distinct_fst:
assumes ‹conflict_min_analysis_stack M NU D analyse›
shows ‹distinct (map fst analyse)› and ‹distinct (map (atm_of o fst) analyse)›
proof -
have dist: ‹distinct (map (index_in_trail M ∘ fst) analyse)›
using conflict_min_analysis_stack_sorted_and_distinct[of M NU D analyse, OF assms]
by auto
then show ‹distinct (map fst analyse)›
by (auto simp: intro!: distinct_mapI[of ‹(index_in_trail M)›])
show ‹distinct (map (atm_of o fst) analyse)›
proof (rule ccontr)
assume ‹¬?thesis›
from not_distinct_decomp[OF this]
obtain xs L ys zs where ‹map (atm_of o fst) analyse = xs @ L # ys @ L # zs›
by auto
then show False
using dist
by (auto simp: map_eq_append_conv atm_of_eq_atm_of Int_Un_distrib image_Un)
qed
qed
lemma conflict_min_analysis_stack_neg:
‹conflict_min_analysis_stack M NU D analyse ⟹
M ⊨as CNot (fst `# mset analyse)›
by (induction M NU D analyse rule: conflict_min_analysis_stack.induct)
auto
fun conflict_min_analysis_stack_hd
:: ‹('v, 'a) ann_lits ⇒ 'v clauses ⇒ 'v clause ⇒ 'v conflict_min_analyse ⇒ bool›
where
‹conflict_min_analysis_stack_hd M NU D [] ⟷ True› |
‹conflict_min_analysis_stack_hd M NU D ((L, E) # _) ⟷
(∃C. set_mset NU ⊨p add_mset (-L) C ∧
(∀K∈#C. index_in_trail M K < index_in_trail M L) ∧ E ⊆# C ∧ -L ∈ lits_of_l M ∧
(∀K∈#C-E. set_mset NU ⊨p (filter_to_poslev M L D) + {#-K#} ∨ K ∈# filter_to_poslev M L D))›
lemma conflict_min_analysis_stack_tl:
‹conflict_min_analysis_stack M NU D analyse ⟹ conflict_min_analysis_stack M NU D (tl analyse)›
by (cases ‹(M, NU, D, analyse)› rule: conflict_min_analysis_stack.cases) auto
definition lit_redundant_inv
:: ‹('v, 'v clause) ann_lits ⇒ 'v clauses ⇒ 'v clause ⇒ 'v conflict_min_analyse ⇒
'v conflict_min_cach × 'v conflict_min_analyse × bool ⇒ bool› where
‹lit_redundant_inv M NU D init_analyse = (λ(cach, analyse, b).
conflict_min_analysis_inv M cach NU D ∧
(analyse ≠ [] ⟶ fst (hd init_analyse) = fst (last analyse)) ∧
(analyse = [] ⟶ b ⟶ cach (atm_of (fst (hd init_analyse))) = SEEN_REMOVABLE) ∧
conflict_min_analysis_stack M NU D analyse ∧
conflict_min_analysis_stack_hd M NU D analyse)›
definition lit_redundant_rec_loop_inv :: ‹('v, 'v clause) ann_lits ⇒
'v conflict_min_cach × 'v conflict_min_analyse × bool ⇒ bool› where
‹lit_redundant_rec_loop_inv M = (λ(cach, analyse, b).
(uminus o fst) `# mset analyse ⊆# lit_of `# mset M ∧
(∀L ∈ set analyse. cach (atm_of (fst L)) = SEEN_UNKNOWN))›
definition lit_redundant_rec :: ‹('v, 'v clause) ann_lits ⇒ 'v clauses ⇒ 'v clause ⇒
'v conflict_min_cach ⇒ 'v conflict_min_analyse ⇒
('v conflict_min_cach × 'v conflict_min_analyse × bool) nres›
where
‹lit_redundant_rec M NU D cach analysis =
WHILE⇩T⇗lit_redundant_rec_loop_inv M ⇖
(λ(cach, analyse, b). analyse ≠ [])
(λ(cach, analyse, b). do {
ASSERT(analyse ≠ []);
ASSERT(length analyse ≤ length M);
ASSERT(-fst (hd analyse) ∈ lits_of_l M);
if snd (hd analyse) = {#}
then
RETURN(cach (atm_of (fst (hd analyse)) := SEEN_REMOVABLE), tl analyse, True)
else do {
(L, analyse) ← get_literal_and_remove_of_analyse analyse;
ASSERT(-L ∈ lits_of_l M);
b ← RES UNIV;
if (get_level M L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE ∨ L ∈# D)
then RETURN (cach, analyse, False)
else if b ∨ cach (atm_of L) = SEEN_FAILED
then do {
cach ← mark_failed_lits NU analyse cach;
RETURN (cach, [], False)
}
else do {
ASSERT(cach (atm_of L) = SEEN_UNKNOWN);
C ← get_propagation_reason M (-L);
case C of
Some C ⇒ do {
ASSERT (distinct_mset C ∧ ¬tautology C);
RETURN (cach, (L, C - {#-L#}) # analyse, False)}
| None ⇒ do {
cach ← mark_failed_lits NU analyse cach;
RETURN (cach, [], False)
}
}
}
})
(cach, analysis, False)›
definition lit_redundant_rec_spec where
‹lit_redundant_rec_spec M NU D L =
SPEC(λ(cach, analysis, b). (b ⟶ NU ⊨pm add_mset (-L) (filter_to_poslev M L D)) ∧
conflict_min_analysis_inv M cach NU D)›
lemma WHILEIT_rule_stronger_inv_keepI':
assumes
‹wf R› and
‹I s› and
‹I' s› and
‹⋀s. I s ⟹ I' s ⟹ b s ⟹ f s ≤ SPEC (λs'. I' s')› and
‹⋀s. I s ⟹ I' s ⟹ b s ⟹ f s ≤ SPEC (λs'. I' s' ⟶ (I s' ∧ (s', s) ∈ R))› and
‹⋀s. I s ⟹ I' s ⟹ ¬ b s ⟹ Φ s›
shows ‹WHILE⇩T⇗I⇖ b f s ≤ SPEC Φ›
proof -
have A[iff]: ‹f s ≤ SPEC (λv. I' v ∧ I v ∧ (v, s) ∈ R) ⟷ f s ≤ SPEC (λs'. I s' ∧ I' s' ∧ (s', s) ∈ R)› for s
by (rule cong[of ‹ λn. f s ≤ n›]) auto
then have H: ‹I s ⟹ I' s ⟹ b s ⟹ f s ≤ SPEC (λs'. I s' ∧ I' s' ∧ (s', s) ∈ R)› for s
using SPEC_rule_conjI [OF assms(4,5)[of s]] by auto
have ‹WHILE⇩T⇗I⇖ b f s ≤ WHILE⇩T⇗λs. I s ∧ I' s⇖ b f s›
by (metis (mono_tags, lifting) WHILEIT_weaken)
also have ‹WHILE⇩T⇗λs. I s ∧ I' s⇖ b f s ≤ SPEC Φ›
by (rule WHILEIT_rule) (use assms H in ‹auto simp: ›)
finally show ?thesis .
qed
lemma lit_redundant_rec_spec:
fixes L :: ‹'v literal›
assumes invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, N + NE, U + UE, D')›
assumes
init_analysis: ‹init_analysis = [(L, C)]› and
in_trail: ‹Propagated (-L) (add_mset (-L) C) ∈ set M› and
‹conflict_min_analysis_inv M cach (N + NE + U + UE) D› and
L_D: ‹L ∈# D› and
M_D: ‹M ⊨as CNot D› and
unknown: ‹cach (atm_of L) = SEEN_UNKNOWN›
shows
‹lit_redundant_rec M (N + U) D cach init_analysis ≤
lit_redundant_rec_spec M (N + U + NE + UE) D L›
proof -
let ?N = ‹N + NE + U + UE›
obtain M2 M1 where
M: ‹M = M2 @ Propagated (- L) (add_mset (- L) C) # M1›
using split_list[OF in_trail] by (auto 5 5)
have ‹a @ Propagated L mark # b = trail (M, N + NE, U + UE, D') ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› for L mark a b
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by fast
then have ‹M1 ⊨as CNot C›
by (force simp: M)
then have M_C: ‹M ⊨as CNot C›
unfolding M by (simp add: true_annots_append_l)
have ‹set (get_all_mark_of_propagated (trail (M, N + NE, U + UE, D')))
⊆ set_mset (cdcl⇩W_restart_mset.clauses (M, N + NE, U + UE, D'))›
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by fast
then have ‹add_mset (-L) C ∈# ?N›
using in_trail cdcl⇩W_restart_mset.in_get_all_mark_of_propagated_in_trail[of ‹add_mset (-L) C› M]
by (auto simp: clauses_def)
then have NU_C: ‹?N ⊨pm add_mset (- L) C›
by auto
have n_d: ‹no_dup M›
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
let ?f = ‹λanalysis. fold_mset (+) D (snd `# mset analysis)›
define I' where
‹I' = (λ(cach :: 'v conflict_min_cach, analysis :: 'v conflict_min_analyse, b::bool).
lit_redundant_inv M ?N D init_analysis (cach, analysis, b) ∧ M ⊨as CNot (?f analysis) ∧
distinct (map (atm_of o fst) analysis))›
define R where
‹R = {((cach :: 'v conflict_min_cach, analysis :: 'v conflict_min_analyse, b::bool),
(cach' :: 'v conflict_min_cach, analysis' :: 'v conflict_min_analyse, b' :: bool)).
(analysis' ≠ [] ∧ (minimize_conflict_support M) (?f analysis') (?f analysis)) ∨
(analysis' ≠ [] ∧ analysis = tl analysis' ∧ snd (hd analysis') = {#}) ∨
(analysis' ≠ [] ∧ analysis = [])}›
have wf_R: ‹wf R›
proof -
have R: ‹R =
{((cach, analysis, b), (cach', analysis', b')).
analysis' ≠ [] ∧analysis = []} ∪
({((cach, analysis, b), (cach', analysis', b')).
analysis' ≠ [] ∧ (minimize_conflict_support M) (?f analysis') (?f analysis)} ∪
{((cach, analysis, b), (cach', analysis', b')).
analysis' ≠ [] ∧ analysis = tl analysis' ∧ snd (hd analysis') = {#}})›
(is ‹_ = ?end ∪ (?Min ∪ ?ana)›)
unfolding R_def by auto
have 1: ‹wf {((cach:: 'v conflict_min_cach, analysis:: 'v conflict_min_analyse, b::bool),
(cach':: 'v conflict_min_cach, analysis':: 'v conflict_min_analyse, b'::bool)).
length analysis < length analysis'}›
using wf_if_measure_f[of ‹measure length›, of ‹λ(_, xs, _). xs›] apply auto
apply (rule subst[of _ _ wf])
prefer 2 apply assumption
apply auto
done
have 2: ‹wf {(C', C).minimize_conflict_support M C C'}›
by (rule wf_minimize_conflict_support[OF invs])
from wf_if_measure_f[OF this, of ?f]
have 2: ‹wf {(C', C). minimize_conflict_support M (?f C) (?f C')}›
by auto
from wf_fst_wf_pair[OF this, where 'b = bool]
have ‹wf {((analysis':: 'v conflict_min_analyse, _ :: bool),
(analysis:: 'v conflict_min_analyse, _:: bool)).
(minimize_conflict_support M) (?f analysis) (?f analysis')}›
by blast
from wf_snd_wf_pair[OF this, where 'b = ‹'v conflict_min_cach›]
have ‹wf {((M' :: 'v conflict_min_cach, N'), Ma, N).
(case N' of
(analysis' :: 'v conflict_min_analyse, _ :: bool) ⇒
λ(analysis, _).
minimize_conflict_support M (fold_mset (+) D (snd `# mset analysis))
(fold_mset (+) D (snd `# mset analysis'))) N}›
by blast
then have wf_Min: ‹wf ?Min›
apply (rule wf_subset)
by auto
have wf_ana: ‹wf ?ana›
by (rule wf_subset[OF 1]) auto
have wf: ‹wf (?Min ∪ ?ana)›
apply (rule wf_union_compatible)
subgoal by (rule wf_Min)
subgoal by (rule wf_ana)
subgoal by (auto elim!: neq_NilE)
done
have wf_end: ‹wf ?end›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain f where f: ‹(f (Suc i), f i) ∈ ?end› for i
unfolding wf_iff_no_infinite_down_chain by auto
have ‹fst (snd (f (Suc 0))) = []›
using f[of 0] by auto
moreover have ‹fst (snd (f (Suc 0))) ≠ []›
using f[of 1] by auto
ultimately show False by blast
qed
show ?thesis
unfolding R
apply (rule wf_Un)
subgoal by (rule wf_end)
subgoal by (rule wf)
subgoal by auto
done
qed
have uL_M: ‹- L ∈ lits_of_l M›
using in_trail by (force simp: lits_of_def)
then have init_I: ‹lit_redundant_inv M ?N D init_analysis (cach, init_analysis, False)›
using assms NU_C Propagated_in_trail_entailed[OF invs in_trail]
unfolding lit_redundant_inv_def
by (auto simp: ac_simps)
have ‹(minimize_conflict_support M) D (remove1_mset L (C + D))›
using minimize_conflict_support.resolve_propa[OF in_trail, of ‹remove1_mset L D›] L_D
by (auto simp: ac_simps)
then have init_I': ‹I' (cach, init_analysis, False)›
using M_D L_D M_C init_I unfolding I'_def by (auto simp: init_analysis)
have hd_M: ‹- fst (hd analyse) ∈ lits_of_l M›
if
inv_I': ‹I' s› and
s: ‹s = (cach, s')› ‹s' = (analyse, ba)› and
nempty: ‹analyse ≠ []›
for analyse s s' ba cach
proof -
have
cach: ‹conflict_min_analysis_inv M cach ?N D› and
ana: ‹conflict_min_analysis_stack M ?N D analyse› and
stack: ‹conflict_min_analysis_stack M ?N D analyse› and
stack_hd: ‹conflict_min_analysis_stack_hd M ?N D analyse› and
last_analysis: ‹analyse ≠ [] ⟶ fst (last analyse) = fst (hd init_analysis)› and
b: ‹analyse = [] ⟶ ba ⟶ cach (atm_of (fst (hd init_analysis))) = SEEN_REMOVABLE›
using inv_I' unfolding lit_redundant_inv_def s I'_def by auto
show ?thesis
using stack_hd nempty by (cases analyse) auto
qed
have all_removed: ‹lit_redundant_inv M ?N D init_analysis
(cach(atm_of (fst (hd analysis)) := SEEN_REMOVABLE), tl analysis, True)› (is ?I) and
all_removed_I': ‹I' (cach(atm_of (fst (hd analysis)) := SEEN_REMOVABLE), tl analysis, True)›
(is ?I') and
all_removed_J: ‹lit_redundant_rec_loop_inv M (cach(atm_of (fst (hd analysis)) := SEEN_REMOVABLE), tl analysis, True)› (is ?J)
if
inv_I': ‹I' s› and inv_J: ‹lit_redundant_rec_loop_inv M s›
‹case s of (cach, analyse, b) ⇒ analyse ≠ []› and
s: ‹s = (cach, s')›
‹s' = (analysis, b)› and
nemtpy_stack: ‹analysis ≠ []› and
finished: ‹snd (hd analysis) = {#}›
for s cach s' analysis b
proof -
obtain L ana' where analysis: ‹analysis = (L, {#}) # ana'›
using nemtpy_stack finished by (cases analysis) auto
have
cach: ‹conflict_min_analysis_inv M cach ?N D› and
ana: ‹conflict_min_analysis_stack M ?N D analysis› and
stack: ‹conflict_min_analysis_stack M ?N D analysis› and
stack_hd: ‹conflict_min_analysis_stack_hd M ?N D analysis› and
last_analysis: ‹analysis ≠ [] ⟶ fst (last analysis) = fst (hd init_analysis)› and
b: ‹analysis = [] ⟶ b ⟶ cach (atm_of (fst (hd init_analysis))) = SEEN_REMOVABLE› and
dist: ‹distinct (map (atm_of o fst) analysis)›
using inv_I' unfolding lit_redundant_inv_def s I'_def by auto
obtain C where
NU_C: ‹?N ⊨pm add_mset (-L) C› and
IH: ‹⋀K. K ∈# C ⟹ ?N ⊨pm add_mset (-K) (filter_to_poslev M L D) ∨
K ∈# filter_to_poslev M L D› and
index_K: ‹K∈#C ⟹ index_in_trail M K < index_in_trail M L› and
L_M: ‹-L ∈ lits_of_l M› for K
using stack_hd unfolding analysis by auto
have NU_D: ‹?N ⊨pm add_mset (- fst (hd analysis)) (filter_to_poslev M (fst (hd analysis)) D)›
using conflict_minimize_intermediate_step_filter_to_poslev[OF _ NU_C, simplified, OF index_K]
IH
unfolding analysis by auto
have ana': ‹conflict_min_analysis_stack M ?N D (tl analysis)›
using ana by (auto simp: conflict_min_analysis_stack_tl)
have ‹-fst (hd analysis) ∈ lits_of_l M›
using L_M by (auto simp: analysis I'_def s ana)
then have cach':
‹conflict_min_analysis_inv M (cach(atm_of (fst (hd analysis)) := SEEN_REMOVABLE)) ?N D›
using NU_D n_d by (auto simp: conflict_min_analysis_inv_update_removable cach)
have stack_hd': ‹conflict_min_analysis_stack_hd M ?N D ana'›
proof (cases ‹ana' = []›)
case True
then show ?thesis by auto
next
case False
then obtain L' C' ana'' where ana'': ‹ana' = (L', C') # ana''›
by (cases ana'; cases ‹hd ana'›) auto
then obtain E' where
NU_E': ‹?N ⊨pm add_mset (- L') E'› and
‹∀K∈#E' - add_mset L C'. ?N ⊨pm add_mset (- K) (filter_to_poslev M L' D) ∨
K ∈# filter_to_poslev M L' D› and
index_C': ‹∀K∈#E'. index_in_trail M K < index_in_trail M L'› and
index_L'_L: ‹index_in_trail M L < index_in_trail M L'› and
C'_E': ‹C' ⊆# E'› and
uL'_M: ‹- L' ∈ lits_of_l M›
using stack by (auto simp: analysis ana'')
moreover have ‹?N ⊨pm add_mset (- L) (filter_to_poslev M L D)›
using NU_D analysis by auto
moreover have ‹K ∈# E' - C' ⟹ K ∈# E' - add_mset L C' ∨ K = L› for K
by (cases ‹L ∈# E'›)
(fastforce simp: minus_notin_trivial dest!: multi_member_split[of L]
dest: in_remove1_msetI)+
moreover have ‹K ∈# E' - C' ⟹ index_in_trail M K ≤ index_in_trail M L'› for K
by (meson in_diffD index_C' less_or_eq_imp_le)
ultimately have ‹K ∈# E' - C' ⟹ ?N ⊨pm add_mset (- K) (filter_to_poslev M L' D) ∨
K ∈# filter_to_poslev M L' D› for K
using filter_to_poslev_mono_entailement_add_mset[of M K L']
filter_to_poslev_mono[of M L L']
by fastforce
then show ?thesis
using NU_E' uL'_M index_C' C'_E' unfolding ana'' by (auto intro!: exI[of _ E'])
qed
have ‹fst (hd init_analysis) = fst (last (tl analysis))› if ‹tl analysis ≠ []›
using last_analysis tl_last[symmetric, OF that] that unfolding ana' by auto
then show ?I
using ana' cach' last_analysis stack_hd' dist unfolding lit_redundant_inv_def
by (cases ana'; auto simp: analysis atm_of_eq_atm_of split: if_splits)
then show I': ?I'
using inv_I' unfolding I'_def s by (auto simp: analysis)
have ‹distinct (map (λx. - fst x) (tl analysis))›
using dist distinct_mapI[of ‹atm_of o uminus› ‹map (uminus o fst) (tl analysis)›]
conflict_min_analysis_stack_neg[OF ana'] by (auto simp: comp_def map_tl
simp flip: distinct_mset_image_mset)
then show ?J
using inv_J unfolding lit_redundant_rec_loop_inv_def prod.case s
apply (subst distinct_subseteq_iff[symmetric])
using conflict_min_analysis_stack_neg[OF ana'] no_dup_distinct[OF n_d] dist
by (force simp: comp_def entails_CNot_negate_ann_lits negate_ann_lits_def
analysis ana'
simp flip: distinct_mset_image_mset)+
qed
have all_removed_R:
‹((cach(atm_of (fst (hd analyse)) := SEEN_REMOVABLE), tl analyse, True), s) ∈ R›
if
s: ‹s = (cach, s')› ‹s' = (analyse, b)› and
nempty: ‹analyse ≠ []› and
finished: ‹snd (hd analyse) = {#}›
for s cach s' analyse b
using nempty finished unfolding R_def s by auto
have
seen_removable_inv: ‹lit_redundant_inv M ?N D init_analysis (cach, ana, False)› (is ?I) and
seen_removable_I': ‹I' (cach, ana, False)› (is ?I') and
seen_removable_R: ‹((cach, ana, False), s) ∈ R› (is ?R) and
seen_removable_J: ‹lit_redundant_rec_loop_inv M (cach, ana, False)› (is ?J)
if
inv_I': ‹I' s› and inv_J: ‹lit_redundant_rec_loop_inv M s› and
cond: ‹case s of (cach, analyse, b) ⇒ analyse ≠ []› and
s: ‹s = (cach, s')› ‹s' = (analyse, b)› ‹x = (L, ana)› and
nemtpy_stack: ‹analyse ≠ []› and
‹snd (hd analyse) ≠ {#}› and
next_lit: ‹case x of
(L, ana) ⇒ L ∈# snd (hd analyse) ∧ tl ana = tl analyse ∧ ana ≠ [] ∧
hd ana = (fst (hd analyse), remove1_mset L (snd (hd analyse)))› and
lev0_removable: ‹get_level M L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE ∨ L ∈# D›
for s cach s' analyse b x L ana
proof -
obtain K C ana' where analysis: ‹analyse = (K, C) # ana'›
using nemtpy_stack by (cases analyse) auto
have ana': ‹ana = (K, remove1_mset L C) # ana'› and L_C: ‹L ∈# C›
using next_lit unfolding s by (cases ana; auto simp: analysis)+
have
cach: ‹conflict_min_analysis_inv M cach (?N) D› and
ana: ‹conflict_min_analysis_stack M ?N D analyse› and
stack: ‹conflict_min_analysis_stack M ?N D analyse› and
stack_hd: ‹conflict_min_analysis_stack_hd M ?N D analyse› and
last_analysis: ‹analyse ≠ [] ⟶ fst (last analyse) = fst (hd init_analysis)› and
b: ‹analyse = [] ⟶ b ⟶ cach (atm_of (fst (hd init_analysis))) = SEEN_REMOVABLE› and
dist: ‹distinct (map (atm_of ∘ fst) analyse)›
using inv_I' unfolding lit_redundant_inv_def s I'_def prod.case by auto
have last_analysis': ‹ana ≠ [] ⟹ fst (hd init_analysis) = fst (last ana)›
using last_analysis next_lit unfolding analysis s
by (cases ana) (auto split: if_splits)
have uL_M: ‹-L ∈ lits_of_l M›
using inv_I' L_C unfolding analysis ana s I'_def
by (auto dest!: multi_member_split)
have uK_M: ‹- K ∈ lits_of_l M›
using stack_hd unfolding analysis by auto
consider
(lev0) ‹get_level M L = 0› |
(Removable) ‹cach (atm_of L) = SEEN_REMOVABLE› |
(in_D) ‹L ∈# D›
using lev0_removable by fast
then have H: ‹∃CK. ?N ⊨pm add_mset (- K) CK ∧
(∀Ka∈#CK - remove1_mset L C. ?N ⊨pm (filter_to_poslev M K D) + {#- Ka#} ∨
Ka ∈# filter_to_poslev M K D) ∧
(∀Ka∈#CK. index_in_trail M Ka < index_in_trail M K) ∧
remove1_mset L C ⊆# CK›
(is ‹∃C. ?P C›)
proof cases
case Removable
then have L: ‹?N ⊨pm add_mset (- L) (filter_to_poslev M L D)›
using cach uL_M unfolding conflict_min_analysis_inv_def by auto
obtain CK where
‹?N ⊨pm add_mset (- K) CK› and
‹∀K'∈#CK - C. ?N ⊨pm (filter_to_poslev M K D) + {#- K'#} ∨ K' ∈# filter_to_poslev M K D› and
index_CK: ‹∀Ka∈#CK. index_in_trail M Ka < index_in_trail M K› and
C_CK: ‹C ⊆# CK›
using stack_hd unfolding analysis by auto
moreover have ‹remove1_mset L C ⊆# CK›
using C_CK by (meson diff_subset_eq_self subset_mset.dual_order.trans)
moreover have ‹index_in_trail M L < index_in_trail M K›
using index_CK C_CK L_C unfolding analysis ana' by auto
moreover have index_CK': ‹∀Ka∈#CK. index_in_trail M Ka ≤ index_in_trail M K›
using index_CK by auto
ultimately have ‹?P CK›
using filter_to_poslev_mono_entailement_add_mset[of M _ _]
filter_to_poslev_mono[of M K L]
using L L_C C_CK by (auto simp: minus_remove1_mset_if)
then show ?thesis by blast
next
assume lev0: ‹get_level M L = 0›
have ‹M ⊨as CNot (?f analyse)›
using inv_I' unfolding I'_def s by auto
then have ‹-L ∈ lits_of_l M›
using next_lit unfolding analysis s by (auto dest: multi_member_split)
then have ‹?N ⊨pm {#-L#}›
using lev0 cdcl⇩W_restart_mset.literals_of_level0_entailed[OF invs, of ‹-L›]
by (auto simp: clauses_def ac_simps)
moreover obtain CK where
‹?N ⊨pm add_mset (- K) CK› and
‹∀K'∈#CK - C. ?N ⊨pm (filter_to_poslev M K D) + {#- K'#} ∨ K' ∈# filter_to_poslev M K D› and
‹∀Ka∈#CK. index_in_trail M Ka < index_in_trail M K› and
C_CK: ‹C ⊆# CK›
using stack_hd unfolding analysis by auto
moreover have ‹remove1_mset L C ⊆# CK›
using C_CK by (meson diff_subset_eq_self subset_mset.order_trans)
ultimately have ‹?P CK›
by (auto simp: minus_remove1_mset_if intro: conflict_minimize_intermediate_step)
then show ?thesis by blast
next
case in_D
obtain CK where
‹?N ⊨pm add_mset (- K) CK› and
‹∀Ka∈#CK - C. ?N ⊨pm (filter_to_poslev M K D) + {#- Ka#} ∨ Ka ∈# filter_to_poslev M K D› and
index_CK: ‹∀Ka∈#CK. index_in_trail M Ka < index_in_trail M K› and
C_CK: ‹C ⊆# CK›
using stack_hd unfolding analysis by auto
moreover have ‹remove1_mset L C ⊆# CK›
using C_CK by (meson diff_subset_eq_self subset_mset.order_trans)
moreover have ‹L ∈# filter_to_poslev M K D›
using in_D L_C index_CK C_CK by (fastforce simp: filter_to_poslev_def)
ultimately have ‹?P CK›
using in_D
using filter_to_poslev_mono_entailement_add_mset[of M L K]
by (auto simp: minus_remove1_mset_if dest!:
intro: conflict_minimize_intermediate_step)
then show ?thesis by blast
qed note H = this
have stack': ‹conflict_min_analysis_stack M ?N D ana›
using stack unfolding ana' analysis by (cases ana') auto
have stack_hd': ‹conflict_min_analysis_stack_hd M ?N D ana›
using H uL_M uK_M unfolding ana' by auto
show ?I
using last_analysis' cach stack' stack_hd' unfolding lit_redundant_inv_def s
by auto
have ‹M ⊨as CNot (?f ana)›
using inv_I' unfolding I'_def s ana analysis ana'
by (cases ‹L ∈# C›) (auto dest!: multi_member_split)
then show ?I'
using inv_I' ‹?I› unfolding I'_def s by (auto simp: analysis ana')
show ?R
using next_lit
unfolding R_def s by (auto simp: ana' analysis dest!: multi_member_split
intro: minimize_conflict_support.intros)
have ‹distinct (map (λx. - fst x) ana)›
using dist distinct_mapI[of ‹atm_of o uminus› ‹map (uminus o fst) (tl analyse)›]
conflict_min_analysis_stack_neg[OF stack'] by (auto simp: comp_def map_tl
analysis ana'
simp flip: distinct_mset_image_mset)
then show ?J
using inv_J unfolding lit_redundant_rec_loop_inv_def prod.case s
apply (subst distinct_subseteq_iff[symmetric])
using conflict_min_analysis_stack_neg[OF stack'] no_dup_distinct[OF n_d]
apply (auto simp: comp_def entails_CNot_negate_ann_lits negate_ann_lits_def
simp flip: distinct_mset_image_mset)
apply (force simp add: analysis ana ana')
done
qed
have
failed_I: ‹lit_redundant_inv M ?N D init_analysis
(cach', [], False)› (is ?I) and
failed_I': ‹I' (cach', [], False)› (is ?I') and
failed_R: ‹((cach', [], False), s) ∈ R› (is ?R) and
failed_J: ‹lit_redundant_rec_loop_inv M (cach', [], False)› (is ?J)
if
inv_I': ‹I' s› and inv_J: ‹lit_redundant_rec_loop_inv M s› and
cond: ‹case s of (cach, analyse, b) ⇒ analyse ≠ []› and
s: ‹s = (cach, s')› ‹s' = (analyse, b)› and
nempty: ‹analyse ≠ []› and
‹snd (hd analyse) ≠ {#}› and
‹case x of (L, ana) ⇒ L ∈# snd (hd analyse) ∧ tl ana = tl analyse ∧
ana ≠ [] ∧ hd ana = (fst (hd analyse), remove1_mset L (snd (hd analyse)))› and
‹x = (L, ana)› and
‹¬ (get_level M L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE ∨ L ∈# D)› and
cach_update: ‹∀L. cach' L = SEEN_REMOVABLE ⟶ cach L = SEEN_REMOVABLE›
for s cach s' analyse b x L ana E cach'
proof -
have
cach: ‹conflict_min_analysis_inv M cach ?N D› and
ana: ‹conflict_min_analysis_stack M ?N D analyse› and
stack: ‹conflict_min_analysis_stack M ?N D analyse› and
last_analysis: ‹analyse ≠ [] ⟶ fst (last analyse) = fst (hd init_analysis)› and
b: ‹analyse = [] ⟶ b ⟶ cach (atm_of (fst (hd init_analysis))) = SEEN_REMOVABLE›
using inv_I' unfolding lit_redundant_inv_def s I'_def by auto
have ‹conflict_min_analysis_inv M cach' ?N D›
using cach cach_update by (auto simp: conflict_min_analysis_inv_def)
moreover have ‹conflict_min_analysis_stack M ?N D []›
by simp
ultimately show ?I
unfolding lit_redundant_inv_def by simp
then show ?I'
using M_D unfolding I'_def by auto
show ?R
using nempty unfolding R_def s by auto
show ?J
by (auto simp: lit_redundant_rec_loop_inv_def)
qed
have is_propagation_inv: ‹lit_redundant_inv M ?N D init_analysis
(cach, (L, remove1_mset (-L) E') # ana, False)› (is ?I) and
is_propagation_I': ‹I' (cach, (L, remove1_mset (-L) E') # ana, False)› (is ?I') and
is_propagation_R: ‹((cach, (L, remove1_mset (-L) E') # ana, False), s) ∈ R› (is ?R) and
is_propagation_dist: ‹distinct_mset E'› (is ?dist) and
is_propagation_tauto: ‹¬tautology E'› (is ?tauto) and
is_propagation_J': ‹lit_redundant_rec_loop_inv M (cach, (L, remove1_mset (-L) E') # ana, False)› (is ?J)
if
inv_I': ‹I' s› and inv_J: ‹lit_redundant_rec_loop_inv M s› and
‹case s of (cach, analyse, b) ⇒ analyse ≠ []› and
s: ‹s = (cach, s')› ‹s' = (analyse, b)› ‹x = (L, ana)› and
nemtpy_stack: ‹analyse ≠ []› and
‹snd (hd analyse) ≠ {#}› and
next_lit: ‹case x of (L, ana) ⇒
L ∈# snd (hd analyse) ∧
tl ana = tl analyse ∧
ana ≠ [] ∧
hd ana =
(fst (hd analyse),
remove1_mset L (snd (hd analyse)))› and
‹¬ (get_level M L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE ∨ L ∈# D)› and
E: ‹E ≠ None ⟶ Propagated (- L) (the E) ∈ set M› ‹E = Some E'› and
st: ‹cach (atm_of L) = SEEN_UNKNOWN›
for s cach s' analyse b x L ana E E'
proof -
obtain K C ana' where analysis: ‹analyse = (K, C) # ana'›
using nemtpy_stack by (cases analyse) auto
have ana': ‹ana = (K, remove1_mset L C) # ana'›
using next_lit unfolding s by (cases ana) (auto simp: analysis)
have
cach: ‹conflict_min_analysis_inv M cach ?N D› and
ana: ‹conflict_min_analysis_stack M ?N D analyse› and
stack: ‹conflict_min_analysis_stack M ?N D analyse› and
stack_hd: ‹conflict_min_analysis_stack_hd M ?N D analyse› and
last_analysis: ‹analyse ≠ [] ⟶ fst (last analyse) = fst (hd init_analysis)› and
b: ‹analyse = [] ⟶ b ⟶ cach (atm_of (fst (hd init_analysis))) = SEEN_REMOVABLE› and
dist_ana: ‹distinct (map (atm_of ∘ fst) analyse)›
using inv_I' unfolding lit_redundant_inv_def s I'_def by auto
have
NU_E: ‹?N ⊨pm add_mset (- L) (remove1_mset (-L) E')› and
uL_E: ‹-L ∈# E'› and
M_E': ‹M ⊨as CNot (remove1_mset (- L) E')› and
tauto: ‹¬ tautology E'› and
dist: ‹distinct_mset E'› and
lev_E': ‹K ∈# remove1_mset (- L) E' ⟹ index_in_trail M K < index_in_trail M (- L)› for K
using Propagated_in_trail_entailed[OF invs, of ‹-L› E'] E by (auto simp: ac_simps)
have uL_M: ‹- L ∈ lits_of_l M›
using next_lit inv_I' unfolding s analysis I'_def by (auto dest!: multi_member_split)
obtain C' where
‹?N ⊨pm add_mset (- K) C'› and
‹∀Ka∈#C'. index_in_trail M Ka < index_in_trail M K› and
‹C ⊆# C'› and
‹∀Ka∈#C' - C.
?N ⊨pm add_mset (- Ka) (filter_to_poslev M K D) ∨
Ka ∈# filter_to_poslev M K D› and
uK_M: ‹- K ∈ lits_of_l M›
using stack_hd
unfolding s ana'[symmetric]
by (auto simp: analysis ana' conflict_min_analysis_stack_change_hd)
then have cmas: ‹conflict_min_analysis_stack M ?N D ((L, remove1_mset (-L) E') # ana)›
using stack E next_lit NU_E uL_E uL_M
filter_to_poslev_mono_entailement_add_mset[of M _ _ ‹set_mset ?N› _ D]
filter_to_poslev_mono[of M ] uK_M
unfolding s ana'[symmetric] prod.case
by (auto simp: analysis ana' conflict_min_analysis_stack_change_hd)
moreover have ‹conflict_min_analysis_stack_hd M ?N D ((L, remove1_mset (- L) E') # ana)›
using NU_E lev_E' uL_M by (auto intro!:exI[of _ ‹remove1_mset (- L) E'›])
moreover have ‹fst (hd init_analysis) = fst (last ((L, remove1_mset (- L) E') # ana))›
using last_analysis unfolding analysis ana' by auto
ultimately show ?I
using cach b unfolding lit_redundant_inv_def analysis by auto
moreover have ‹L ≠ K›
using cmas
unfolding ana' conflict_min_analysis_stack.simps(3) by blast
moreover have ‹L ≠ -K›
using cmas
unfolding ana' conflict_min_analysis_stack.simps(3) by auto
ultimately show ?I'
using M_E' inv_I' conflict_min_analysis_stack_distinct_fst[OF cmas]
unfolding I'_def s ana analysis ana'
by (auto simp: true_annot_CNot_diff atm_of_eq_atm_of uminus_lit_swap)
have ‹L ∈# C› and in_trail: ‹Propagated (- L) (the E) ∈ set M› and EE': ‹the E = E'›
using next_lit E by (auto simp: analysis ana' s)
then obtain E'' C' where
E': ‹E' = add_mset (-L) E''› and
C: ‹C = add_mset L C'›
using uL_E by (blast dest: multi_member_split)
have ‹minimize_conflict_support M (C + fold_mset (+) D (snd `# mset ana'))
(remove1_mset (- L) E' + (remove1_mset L C + fold_mset (+) D (snd `# mset ana')))›
using minimize_conflict_support.resolve_propa[OF in_trail,
of ‹C' + fold_mset (+) D (snd `# mset ana')›]
unfolding C E' EE'
by (auto simp: ac_simps)
then show ?R
using nemtpy_stack unfolding s analysis ana' by (auto simp: R_def
intro: resolve_propa)
have ‹distinct (map (λx. - fst x) analyse)›
using dist_ana distinct_mapI[of ‹atm_of o uminus› ‹map (uminus o fst) analyse›]
conflict_min_analysis_stack_neg[OF cmas] unfolding analysis ana'
by (auto simp: comp_def map_tl
simp flip: distinct_mset_image_mset)
then show ?J
using inv_J st unfolding lit_redundant_rec_loop_inv_def prod.case s
apply (intro conjI)
apply (subst distinct_subseteq_iff[symmetric])
using conflict_min_analysis_stack_neg[OF cmas] no_dup_distinct[OF n_d] uL_M
‹L ≠ -K› ‹L ≠ K› conflict_min_analysis_stack_distinct_fst[OF cmas]
apply (auto simp: comp_def entails_CNot_negate_ann_lits
negate_ann_lits_def lits_of_def uminus_lit_swap
simp flip: distinct_mset_image_mset)[3]
apply (clarsimp_all simp add: analysis ana')[]
using that by (clarsimp_all simp add: analysis ana')[]
show ?tauto
using tauto .
show ?dist
using dist .
qed
have length_aa_le: ‹length aa ≤ length M›
if
‹I' s› and
‹case s of (cach, analyse, b) ⇒ analyse ≠ []› and
‹s = (a, b)› and
‹b = (aa, ba)› and
‹aa ≠ []› for s a b aa ba
proof -
have ‹M ⊨as CNot (fst `# mset aa)› and ‹distinct (map (atm_of o fst) aa)› and
‹distinct (map fst aa)› and
‹conflict_min_analysis_stack M (N + NE + U + UE) D aa›
using distinct_mapI[of ‹atm_of› ‹map fst aa›]
using that by (auto simp: I'_def lit_redundant_inv_def
dest: conflict_min_analysis_stack_neg)
then have ‹set (map fst aa) ⊆ uminus ` lits_of_l M›
by (auto simp: true_annots_true_cls_def_iff_negation_in_model lits_of_def image_image
uminus_lit_swap
dest!: multi_member_split)
from card_mono[OF _ this] have ‹length (map fst aa) ≤ length M›
using ‹distinct (map (fst) aa)› distinct_card[of ‹map fst aa›] n_d
by (auto simp: card_image[OF lit_of_inj_on_no_dup[OF n_d]] lits_of_def image_image
distinct_card[OF no_dup_imp_distinct])
then show ‹?thesis› by auto
qed
show ?thesis
unfolding lit_redundant_rec_def lit_redundant_rec_spec_def mark_failed_lits_def
get_literal_and_remove_of_analyse_def get_propagation_reason_def
apply (refine_vcg WHILEIT_rule_stronger_inv[where R = R and I' = I'])
subgoal by (rule wf_R)
subgoal using assms by (auto simp: lit_redundant_rec_loop_inv_def lits_of_def
dest!: multi_member_split)
subgoal by (rule init_I')
subgoal by auto
subgoal by (rule length_aa_le)
subgoal by (rule hd_M)
subgoal by (rule all_removed_J)
subgoal by (rule all_removed_I')
subgoal by (rule all_removed_R)
subgoal for s cach s' analyse ba
by (cases ‹analyse›) (auto simp: I'_def dest!: multi_member_split)
subgoal by (rule seen_removable_J)
subgoal by (rule seen_removable_I')
subgoal by (rule seen_removable_R)
subgoal by (rule failed_J)
subgoal by (rule failed_I')
subgoal by (rule failed_R)
subgoal for s a b aa ba x ab bb xa by (cases ‹a (atm_of ab)›) auto
subgoal by (rule failed_J)
subgoal by (rule failed_I')
subgoal by (rule failed_R)
subgoal by (rule is_propagation_dist)
subgoal by (rule is_propagation_tauto)
subgoal by (rule is_propagation_J')
subgoal by (rule is_propagation_I')
subgoal by (rule is_propagation_R)
subgoal
using uL_M by (auto simp: lit_redundant_inv_def conflict_min_analysis_inv_def init_analysis
I'_def ac_simps)
subgoal by (auto simp: lit_redundant_inv_def conflict_min_analysis_inv_def init_analysis
I'_def ac_simps)
done
qed
definition literal_redundant_spec where
‹literal_redundant_spec M NU D L =
SPEC(λ(cach, analysis, b). (b ⟶ NU ⊨pm add_mset (-L) (filter_to_poslev M L D)) ∧
conflict_min_analysis_inv M cach NU D)›
definition literal_redundant where
‹literal_redundant M NU D cach L = do {
ASSERT(-L ∈ lits_of_l M);
if get_level M L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE
then RETURN (cach, [], True)
else if cach (atm_of L) = SEEN_FAILED
then RETURN (cach, [], False)
else do {
C ← get_propagation_reason M (-L);
case C of
Some C ⇒ do{
ASSERT(distinct_mset C ∧ ¬tautology C);
lit_redundant_rec M NU D cach [(L, C - {#-L#})]}
| None ⇒ do {
RETURN (cach, [], False)
}
}
}›
lemma true_clss_cls_add_self: ‹NU ⊨p D' + D' ⟷ NU ⊨p D'›
by (metis subset_mset.sup_idem true_clss_cls_sup_iff_add)
lemma true_clss_cls_add_add_mset_self: ‹NU ⊨p add_mset L (D' + D') ⟷ NU ⊨p add_mset L D'›
using true_clss_cls_add_self true_clss_cls_mono_r by fastforce
lemma filter_to_poslev_remove1:
‹filter_to_poslev M L (remove1_mset K D) =
(if index_in_trail M K ≤ index_in_trail M L then remove1_mset K (filter_to_poslev M L D)
else filter_to_poslev M L D)›
unfolding filter_to_poslev_def
by (auto simp: multiset_filter_mono2)
lemma filter_to_poslev_add_mset:
‹filter_to_poslev M L (add_mset K D) =
(if index_in_trail M K < index_in_trail M L then add_mset K (filter_to_poslev M L D)
else filter_to_poslev M L D)›
unfolding filter_to_poslev_def
by (auto simp: multiset_filter_mono2)
lemma filter_to_poslev_conflict_min_analysis_inv:
assumes
L_D: ‹L ∈# D› and
NU_uLD: ‹N+U ⊨pm add_mset (-L) (filter_to_poslev M L D)› and
inv: ‹conflict_min_analysis_inv M cach (N + U) D›
shows ‹conflict_min_analysis_inv M cach (N + U) (remove1_mset L D)›
unfolding conflict_min_analysis_inv_def
proof (intro allI impI)
fix K
assume ‹-K ∈ lits_of_l M› and ‹cach (atm_of K) = SEEN_REMOVABLE›
then have K: ‹N + U ⊨pm add_mset (- K) (filter_to_poslev M K D)›
using inv unfolding conflict_min_analysis_inv_def by blast
obtain D' where D: ‹D = add_mset L D'›
using multi_member_split[OF L_D] by blast
have ‹N + U ⊨pm add_mset (- K) (filter_to_poslev M K D')›
proof (cases ‹index_in_trail M L < index_in_trail M K›)
case True
then have ‹N + U ⊨pm add_mset (- K) (add_mset L (filter_to_poslev M K D'))›
using K by (auto simp: filter_to_poslev_add_mset D)
then have 1: ‹N + U ⊨pm add_mset L (add_mset (-K) (filter_to_poslev M K D'))›
by (simp add: add_mset_commute)
have H: ‹index_in_trail M L ≤ index_in_trail M K›
using True by simp
have 2: ‹N+U ⊨pm add_mset (-L) (filter_to_poslev M K D')›
using filter_to_poslev_mono_entailement_add_mset[OF H] NU_uLD
by (metis (no_types, hide_lams) D NU_uLD filter_to_poslev_add_mset
order_less_irrefl)
show ?thesis
using true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[OF 2 1]
by (auto simp: true_clss_cls_add_add_mset_self)
next
case False
then show ?thesis using K by (auto simp: filter_to_poslev_add_mset D split: if_splits)
qed
then show ‹N + U ⊨pm add_mset (- K) (filter_to_poslev M K (remove1_mset L D))›
by (simp add: D)
qed
lemma can_filter_to_poslev_can_remove:
assumes
L_D: ‹L ∈# D› and
‹M ⊨as CNot D› and
NU_D: ‹NU ⊨pm D› and
NU_uLD: ‹NU ⊨pm add_mset (-L) (filter_to_poslev M L D)›
shows ‹NU ⊨pm remove1_mset L D›
proof -
obtain D' where
D: ‹D = add_mset L D'›
using multi_member_split[OF L_D] by blast
then have ‹filter_to_poslev M L D ⊆# D'›
by (auto simp: filter_to_poslev_def)
then have ‹NU ⊨pm add_mset (-L) D'›
using NU_uLD true_clss_cls_mono_r[of _ ‹ add_mset (- L) (filter_to_poslev M (-L) D)› ]
by (auto simp: mset_subset_eq_exists_conv)
from true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[OF this, of D']
show ‹NU ⊨pm remove1_mset L D›
using NU_D by (auto simp: D true_clss_cls_add_self)
qed
lemma literal_redundant_spec:
fixes L :: ‹'v literal›
assumes invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, N + NE, U + UE, D')›
assumes
inv: ‹conflict_min_analysis_inv M cach (N + NE + U + UE) D› and
L_D: ‹L ∈# D› and
M_D: ‹M ⊨as CNot D›
shows
‹literal_redundant M (N + U) D cach L ≤ literal_redundant_spec M (N + U + NE + UE) D L›
proof -
have lit_redundant_rec: ‹lit_redundant_rec M (N + U) D cach [(L, remove1_mset (- L) E')]
≤ literal_redundant_spec M (N + U + NE + UE) D L›
if
E: ‹E ≠ None ⟶ Propagated (- L) (the E) ∈ set M› and
E': ‹E = Some E'› and
failed: ‹¬ (get_level M L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE)›
‹cach (atm_of L) ≠ SEEN_FAILED›
for E E'
proof -
have
[simp]: ‹-L ∈# E'› and
in_trail: ‹Propagated (- L) (add_mset (-L) (remove1_mset (-L) E')) ∈ set M›
using Propagated_in_trail_entailed[OF invs, of ‹-L› E'] E E'
by auto
have H: ‹lit_redundant_rec_spec M (N + U + NE + UE) D L ≤
literal_redundant_spec M (N + U + NE + UE) D L›
by (auto simp: lit_redundant_rec_spec_def literal_redundant_spec_def ac_simps)
show ?thesis
apply (rule order.trans)
apply (rule lit_redundant_rec_spec[OF invs _ in_trail])
subgoal ..
subgoal by (rule inv)
subgoal using assms by fast
subgoal by (rule M_D)
subgoal using failed by (cases ‹cach (atm_of L)›) auto
subgoal unfolding literal_redundant_spec_def[symmetric] by (rule H)
done
qed
have
L_dist: ‹distinct_mset (C)› and
L_tauto: ‹¬tautology C›
if
in_trail: ‹Propagated (- L) C ∈ set M›
for C
using that
Propagated_in_trail_entailed[of M ‹N+NE› ‹U+UE› ‹D'› ‹-L› ‹C›] invs
by (auto simp: )
have uL_M: ‹-L ∈ lits_of_l M›
using L_D M_D by (auto dest!: multi_member_split)
show ?thesis
unfolding literal_redundant_def get_propagation_reason_def literal_redundant_spec_def
apply (refine_vcg)
subgoal using uL_M .
subgoal
using inv uL_M cdcl⇩W_restart_mset.literals_of_level0_entailed[OF invs, of ‹-L›]
true_clss_cls_mono_r'
by (fastforce simp: mark_failed_lits_def conflict_min_analysis_inv_def
clauses_def ac_simps)
subgoal using inv by (auto simp: ac_simps)
subgoal by auto
subgoal using inv by (auto simp: ac_simps)
subgoal using inv by (auto simp: mark_failed_lits_def conflict_min_analysis_inv_def)
subgoal using inv by (auto simp: mark_failed_lits_def conflict_min_analysis_inv_def ac_simps)
subgoal using L_dist by simp
subgoal using L_tauto by simp
subgoal for E E'
unfolding literal_redundant_spec_def[symmetric]
by (rule lit_redundant_rec)
done
qed
definition set_all_to_list where
‹set_all_to_list e ys = do {
S ← WHILE⇗λ(i, xs). i ≤ length xs ∧ (∀x ∈ set (take i xs). x = e) ∧ length xs = length ys⇖
(λ(i, xs). i < length xs)
(λ(i, xs). do {
ASSERT(i < length xs);
RETURN(i+1, xs[i := e])
})
(0, ys);
RETURN (snd S)
}›
lemma
‹set_all_to_list e ys ≤ SPEC(λxs. length xs = length ys ∧ (∀x ∈ set xs. x = e))›
unfolding set_all_to_list_def
apply (refine_vcg)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: take_Suc_conv_app_nth list_update_append)
subgoal by auto
subgoal by auto
subgoal by auto
done
definition get_literal_and_remove_of_analyse_wl
:: ‹'v clause_l ⇒ (nat × nat × nat × nat) list ⇒ 'v literal × (nat × nat × nat × nat) list› where
‹get_literal_and_remove_of_analyse_wl C analyse =
(let (i, k, j, ln) = last analyse in
(C ! j, analyse[length analyse - 1 := (i, k, j + 1, ln)]))›
definition mark_failed_lits_wl
where
‹mark_failed_lits_wl NU analyse cach = SPEC(λcach'.
(∀L. cach' L = SEEN_REMOVABLE ⟶ cach L = SEEN_REMOVABLE))›
definition lit_redundant_rec_wl_ref where
‹lit_redundant_rec_wl_ref NU analyse ⟷
(∀(i, k, j, ln) ∈ set analyse. j ≤ ln ∧ i ∈# dom_m NU ∧ i > 0 ∧
ln ≤ length (NU ∝ i) ∧ k < length (NU ∝ i) ∧
distinct (NU ∝ i) ∧
¬tautology (mset (NU ∝ i))) ∧
(∀(i, k, j, ln) ∈ set (butlast analyse). j > 0)›
definition lit_redundant_rec_wl_inv where
‹lit_redundant_rec_wl_inv M NU D = (λ(cach, analyse, b). lit_redundant_rec_wl_ref NU analyse)›
definition lit_redundant_reason_stack
:: ‹'v literal ⇒ 'v clauses_l ⇒ nat ⇒ (nat × nat × nat × nat)› where
‹lit_redundant_reason_stack L NU C' =
(if length (NU ∝ C') > 2 then (C', 0, 1, length (NU ∝ C'))
else if NU ∝ C' ! 0 = L then (C', 0, 1, length (NU ∝ C'))
else (C', 1, 0, 1))›
definition lit_redundant_rec_wl :: ‹('v, nat) ann_lits ⇒ 'v clauses_l ⇒ 'v clause ⇒
_ ⇒ _ ⇒ _ ⇒
(_ × _ × bool) nres›
where
‹lit_redundant_rec_wl M NU D cach analysis _ =
WHILE⇩T⇗lit_redundant_rec_wl_inv M NU D⇖
(λ(cach, analyse, b). analyse ≠ [])
(λ(cach, analyse, b). do {
ASSERT(analyse ≠ []);
ASSERT(length analyse ≤ length M);
let (C, k, i, ln) = last analyse;
ASSERT(C ∈# dom_m NU);
ASSERT(length (NU ∝ C) > k);
ASSERT(NU ∝ C!k ∈ lits_of_l M);
let C = NU ∝ C;
if i ≥ ln
then
RETURN(cach (atm_of (C ! k) := SEEN_REMOVABLE), butlast analyse, True)
else do {
let (L, analyse) = get_literal_and_remove_of_analyse_wl C analyse;
ASSERT(fst(snd(snd (last analyse))) ≠ 0);
ASSERT(-L ∈ lits_of_l M);
b ← RES (UNIV);
if (get_level M L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE ∨ L ∈# D)
then RETURN (cach, analyse, False)
else if b ∨ cach (atm_of L) = SEEN_FAILED
then do {
cach ← mark_failed_lits_wl NU analyse cach;
RETURN (cach, [], False)
}
else do {
ASSERT(cach (atm_of L) = SEEN_UNKNOWN);
C' ← get_propagation_reason M (-L);
case C' of
Some C' ⇒ do {
ASSERT(C' ∈# dom_m NU);
ASSERT(length (NU ∝ C') ≥ 2);
ASSERT (distinct (NU ∝ C') ∧ ¬tautology (mset (NU ∝ C')));
ASSERT(C' > 0);
RETURN (cach, analyse @ [lit_redundant_reason_stack (-L) NU C'], False)
}
| None ⇒ do {
cach ← mark_failed_lits_wl NU analyse cach;
RETURN (cach, [], False)
}
}
}
})
(cach, analysis, False)›
fun convert_analysis_l where
‹convert_analysis_l NU (i, k, j, le) = (-NU ∝ i ! k, mset (Misc.slice j le (NU ∝ i)))›
definition convert_analysis_list where
‹convert_analysis_list NU analyse = map (convert_analysis_l NU) (rev analyse)›
lemma convert_analysis_list_empty[simp]:
‹convert_analysis_list NU [] = []›
‹convert_analysis_list NU a = [] ⟷ a = []›
by (auto simp: convert_analysis_list_def)
lemma trail_length_ge2:
assumes
ST: ‹(S, T) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S› and
struct_invs: ‹twl_struct_invs T› and
LaC: ‹Propagated L C ∈ set (get_trail_l S)› and
C0: ‹C > 0›
shows
‹length (get_clauses_l S ∝ C) ≥ 2›
proof -
have conv:
‹(get_trail_l S, get_trail T) ∈ convert_lits_l (get_clauses_l S) (get_unit_clauses_l S)›
using ST unfolding twl_st_l_def by auto
have ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of T)› and
lev_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (state⇩W_of T)›
using struct_invs unfolding twl_struct_invs_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have n_d: ‹no_dup (get_trail_l S)›
using ST lev_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: twl_st_l twl_st)
have
C: ‹C ∈# dom_m (get_clauses_l S)›
using list_invs C0 LaC by (auto simp: twl_list_invs_def all_conj_distrib)
have ‹twl_st_inv T›
using struct_invs unfolding twl_struct_invs_def by fast
then show le2: ‹length (get_clauses_l S ∝ C) ≥ 2›
using C ST multi_member_split[OF C] unfolding twl_struct_invs_def
by (cases S; cases T)
(auto simp: twl_st_inv.simps twl_st_l_def
image_Un[symmetric])
qed
lemma clauses_length_ge2:
assumes
ST: ‹(S, T) ∈ twl_st_l None› and
list_invs: ‹twl_list_invs S› and
struct_invs: ‹twl_struct_invs T› and
C: ‹C ∈# dom_m (get_clauses_l S)›
shows
‹length (get_clauses_l S ∝ C) ≥ 2›
proof -
have ‹twl_st_inv T›
using struct_invs unfolding twl_struct_invs_def by fast
then show le2: ‹length (get_clauses_l S ∝ C) ≥ 2›
using C ST multi_member_split[OF C] unfolding twl_struct_invs_def
by (cases S; cases T)
(auto simp: twl_st_inv.simps twl_st_l_def
image_Un[symmetric])
qed
lemma lit_redundant_rec_wl:
fixes S :: ‹nat twl_st_wl› and S' :: ‹nat twl_st_l› and S'' :: ‹nat twl_st› and NU M analyse
defines
[simp]: ‹S''' ≡ state⇩W_of S''›
defines
‹M ≡ get_trail_wl S› and
M': ‹M' ≡ trail S'''› and
NU: ‹NU ≡ get_clauses_wl S› and
NU': ‹NU' ≡ mset `# ran_mf NU› and
‹analyse' ≡ convert_analysis_list NU analyse›
assumes
S_S': ‹(S, S') ∈ state_wl_l None› and
S'_S'': ‹(S', S'') ∈ twl_st_l None› and
bounds_init: ‹lit_redundant_rec_wl_ref NU analyse› and
struct_invs: ‹twl_struct_invs S''› and
add_inv: ‹twl_list_invs S'›
shows
‹lit_redundant_rec_wl M NU D cach analyse lbd ≤ ⇓
(Id ×⇩r {(analyse, analyse'). analyse' = convert_analysis_list NU analyse ∧
lit_redundant_rec_wl_ref NU analyse} ×⇩r bool_rel)
(lit_redundant_rec M' NU' D cach analyse')›
(is ‹_ ≤ ⇓ (_ ×⇩r ?A ×⇩r _) _› is ‹_ ≤ ⇓ ?R _›)
proof -
obtain D' NE UE Q W where
S: ‹S = (M, NU, D', NE, UE, Q, W)›
using M_def NU by (cases S) auto
have M'_def: ‹(M, M') ∈ convert_lits_l NU (NE + UE)›
using NU S_S' S'_S'' unfolding M' by (auto simp: S state_wl_l_def twl_st_l_def)
then have [simp]: ‹lits_of_l M' = lits_of_l M›
by auto
have [simp]: ‹fst (convert_analysis_l NU x) = -NU ∝ (fst x) ! (fst (snd x))› for x
by (cases x) auto
have [simp]: ‹snd (convert_analysis_l NU x) =
mset (Misc.slice (fst (snd (snd x))) (snd (snd (snd x))) (NU ∝ fst x))› for x
by (cases x) auto
have
no_smaller_propa: ‹cdcl⇩W_restart_mset.no_smaller_propa S'''› and
struct_invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv S'''›
using struct_invs unfolding twl_struct_invs_def S'''_def[symmetric]
by fast+
have annots: ‹set (get_all_mark_of_propagated (trail S''')) ⊆
set_mset (cdcl⇩W_restart_mset.clauses S''')›
using struct_invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by fast
have ‹no_dup (get_trail_wl S)›
using struct_invs S_S' S'_S'' unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: twl_st_wl twl_st_l twl_st)
then have n_d: ‹no_dup M›
by (auto simp: S)
then have n_d': ‹no_dup M'›
using M'_def by (auto simp: S)
let ?B = ‹{(analyse, analyse'). analyse' = convert_analysis_list NU analyse ∧
lit_redundant_rec_wl_ref NU analyse ∧ fst (snd (snd (last analyse))) > 0}›
have get_literal_and_remove_of_analyse_wl:
‹RETURN (get_literal_and_remove_of_analyse_wl (NU ∝ x1d) x1c)
≤ ⇓ (Id ×⇩r ?B)
(get_literal_and_remove_of_analyse x1a)›
if
xx': ‹(x, x') ∈ ?R› and
‹case x of (cach, analyse, b) ⇒ analyse ≠ []› and
‹case x' of (cach, analyse, b) ⇒ analyse ≠ []› and
‹lit_redundant_rec_wl_inv M NU D x› and
s: ‹x2 = (x1a, x2a)›
‹x' = (x1, x2)›
‹x2d = (x1f, x2e)›
‹x2c = (x1e, x2d)›
‹(fst (last x1c), fst (snd (last x1c)), fst (snd (snd (last x1c))),
snd (snd (snd (last x1c)))) =
(x1d, x2c)›
‹x2b = (x1c, x2f)›
‹x = (x1b, x2b)› and
‹x1a ≠ []› and
‹- fst (hd x1a) ∈ lits_of_l M'› and
x1c: ‹x1c ≠ []› and
‹x1d ∈# dom_m NU› and
‹x1e < length (NU ∝ x1d)› and
‹NU ∝ x1d ! x1e ∈ lits_of_l M› and
length: ‹¬ x2e ≤ x1f› and
‹snd (hd x1a) ≠ {#}›
for x x' x1 x2 x1a x2a x1b x2b x1c x1d x2c x1e x2d x1f x2e x2f
proof -
have x1d: ‹x1d = fst (last x1c)›
using s by auto
have ‹last x1c = (a, b, c, d) ⟹ d ≤ length (NU ∝ a)›
‹last x1c = (a, b, c, d) ⟹ c ≤ d› for aa ba list a b c d
using xx' x1c length unfolding s convert_analysis_list_def
lit_redundant_rec_wl_ref_def
by (cases x1c rule: rev_cases; auto; fail)+
then show ?thesis
supply convert_analysis_list_def[simp] hd_rev[simp] last_map[simp] rev_map[symmetric, simp]
using x1c xx' length s
using Cons_nth_drop_Suc[of ‹snd (snd (snd (last x1c)))› ‹NU ∝ fst (last x1c)›, symmetric]
unfolding lit_redundant_rec_wl_ref_def x1d
by (cases x1c; cases ‹last x1c›)
(auto simp: get_literal_and_remove_of_analyse_wl_def nth_in_sliceI mset_tl
get_literal_and_remove_of_analyse_def convert_analysis_list_def slice_Suc
slice_head
intro!: RETURN_SPEC_refine elim!: neq_Nil_revE split: if_splits)
qed
have get_propagation_reason: ‹get_propagation_reason M (- x1h)
≤ ⇓ (⟨{(C', C). C = mset (NU ∝ C') ∧ C' ≠ 0 ∧
Propagated (- x1g) (mset (NU∝C')) ∈ set M'
∧ Propagated (- x1g) C' ∈ set M ∧ C' ∈# dom_m NU ∧
length (NU ∝ C') ≥ 2}⟩
option_rel)
(get_propagation_reason M' (- x1g))›
(is ‹_ ≤ ⇓ (⟨?get_propagation_reason⟩option_rel) _›)
if
‹(x, x') ∈ ?R› and
‹case x of (cach, analyse, b) ⇒ analyse ≠ []› and
‹case x' of (cach, analyse, b) ⇒ analyse ≠ []› and
‹lit_redundant_rec_wl_inv M NU D x› and
st:
‹x2 = (x1a, x2a)›
‹x' = (x1, x2)›
‹x2d = (x1f, x2e)›
‹x2c = (x1e, x2d)›
‹(fst (last x1c), fst (snd (last x1c)), fst (snd (snd (last x1c))),
snd (snd (snd (last x1c)))) =
(x1d, x2c)›
‹x2b = (x1c, x2f)›
‹x = (x1b, x2b)›
‹x'a = (x1g, x2g)› and
‹x1a ≠ []› and
‹- fst (hd x1a) ∈ lits_of_l M'› and
‹x1c ≠ []› and
x1d: ‹x1d ∈# dom_m NU› and
‹x1e < length (NU ∝ x1d)› and
‹NU ∝ x1d ! x1e ∈ lits_of_l M› and
‹¬ x2e ≤ x1f› and
‹snd (hd x1a) ≠ {#}› and
H: ‹(get_literal_and_remove_of_analyse_wl (NU ∝ x1d) x1c, x'a)
∈ Id ×⇩f ?B›
‹get_literal_and_remove_of_analyse_wl (NU ∝ x1d) x1c = (x1h, x2h)› and
‹- x1g ∈ lits_of_l M'› and
‹- x1h ∈ lits_of_l M› and
‹(b, ba) ∈ bool_rel› and
‹b ∈ UNIV› and
‹ba ∈ UNIV› and
‹¬ (get_level M x1h = 0 ∨ x1b (atm_of x1h) = SEEN_REMOVABLE ∨ x1h ∈# D)› and
cond: ‹¬ (get_level M' x1g = 0 ∨ x1 (atm_of x1g) = SEEN_REMOVABLE ∨ x1g ∈# D)› and
‹¬ (b ∨ x1b (atm_of x1h) = SEEN_FAILED)› and
‹¬ (ba ∨ x1 (atm_of x1g) = SEEN_FAILED)›
for x x' x1 x2 x1a x2a x1b x2b x1c x1d x2c x1e x2d x1f x2e x2f x'a x1g x2g x1h
x2h b ba
proof -
have [simp]: ‹x1h = x1g›
using st H by auto
have le2: ‹length (NU ∝ x1d) ≥ 2›
using clauses_length_ge2[OF S'_S'' add_inv assms(10), of x1d] x1d st S_S'
by (auto simp: S)
have
‹Propagated (- x1g) (mset (NU ∝ a)) ∈ set M'› (is ?propa) and
‹a ≠ 0› (is ?a) and
‹a ∈# dom_m NU› (is ?L) and
‹length (NU ∝ a) ≥ 2› (is ?len)
if x1e_M: ‹Propagated (- x1g) a ∈ set M›
for a
proof -
have [simp]: ‹a ≠ 0›
proof
assume [simp]: ‹a = 0›
obtain E' where
x1d_M': ‹Propagated (- x1g) E' ∈ set M'› and
‹E' ∈# NE + UE›
using x1e_M M'_def by (auto dest: split_list simp: convert_lits_l_def p2rel_def
convert_lit.simps
elim!: list_rel_in_find_correspondanceE split: if_splits)
moreover have ‹unit_clss S'' = NE + UE›
using S_S' S'_S'' x1d_M' by (auto simp: S)
moreover have ‹Propagated (- x1g) E' ∈ set (get_trail S'')›
using S_S' S'_S'' x1d_M' by (auto simp: S state_wl_l_def twl_st_l_def M')
moreover have ‹0 < count_decided (get_trail S'')›
using cond S_S' S'_S'' count_decided_ge_get_level[of M ‹x1g›]
by (auto simp: S M' twl_st)
ultimately show False
using clauses_in_unit_clss_have_level0(1)[of S'' E' ‹- x1g›] cond ‹twl_struct_invs S''›
S_S' S'_S'' M'_def
by (auto simp: S)
qed
show ?propa and ?a
using that M'_def by (auto simp: convert_lits_l_def p2rel_def convert_lit.simps
elim!: list_rel_in_find_correspondanceE split: if_splits)
then show ?L
using that add_inv S_S' S'_S'' S unfolding twl_list_invs_def
by (auto 5 5 simp: state_wl_l_def twl_st_l_def)
show ?len
using trail_length_ge2[OF S'_S'' add_inv assms(10), of ‹- x1g› a] that S_S'
by (force simp: S)
qed
then show ?thesis
apply (auto simp: get_propagation_reason_def refine_rel_defs intro!: RES_refine)
apply (case_tac s)
by auto
qed
have resolve: ‹((x1b, x2h @ [lit_redundant_reason_stack (- x1h) NU xb], False), x1,
(x1g, remove1_mset (- x1g) x'c) # x2g, False)
∈ Id ×⇩f
({(analyse, analyse').
analyse' = convert_analysis_list NU analyse ∧
lit_redundant_rec_wl_ref NU analyse} ×⇩f
bool_rel)›
if
xx': ‹(x, x') ∈ Id ×⇩r ?A ×⇩r bool_rel› and
‹case x of (cach, analyse, b) ⇒ analyse ≠ []› and
‹case x' of (cach, analyse, b) ⇒ analyse ≠ []› and
‹lit_redundant_rec_wl_inv M NU D x› and
s:
‹x2 = (x1a, x2a)›
‹x' = (x1, x2)›
‹x2d = (x1f, x2e)›
‹x2c = (x1e, x2d)›
‹(fst (last x1c), fst (snd (last x1c)), fst (snd (snd (last x1c))),
snd (snd (snd (last x1c)))) =
(x1d, x2c)›
‹x2b = (x1c, x2f)›
‹x = (x1b, x2b)›
‹x'a = (x1g, x2g)› and
[simp]: ‹x1a ≠ []› and
‹- fst (hd x1a) ∈ lits_of_l M'› and
[simp]: ‹x1c ≠ []› and
‹x1d ∈# dom_m NU› and
‹x1e < length (NU ∝ x1d)› and
‹NU ∝ x1d ! x1e ∈ lits_of_l M› and
‹¬ x2e ≤ x1f› and
‹snd (hd x1a) ≠ {#}› and
get_literal_and_remove_of_analyse_wl:
‹(get_literal_and_remove_of_analyse_wl (NU ∝ x1d) x1c, x'a)
∈ Id ×⇩f
{(analyse, analyse').
analyse' = convert_analysis_list NU analyse ∧
lit_redundant_rec_wl_ref NU analyse ∧
0 < fst (snd (snd (last analyse)))}› and
get_lit: ‹get_literal_and_remove_of_analyse_wl (NU ∝ x1d) x1c = (x1h, x2h)› and
‹- x1g ∈ lits_of_l M'› and
‹fst (snd (snd (last x2h))) ≠ 0› and
‹- x1h ∈ lits_of_l M› and
bba: ‹(b, ba) ∈ bool_rel› and
‹¬ (get_level M x1h = 0 ∨ x1b (atm_of x1h) = SEEN_REMOVABLE ∨ x1h ∈# D)› and
‹¬ (get_level M' x1g = 0 ∨ x1 (atm_of x1g) = SEEN_REMOVABLE ∨ x1g ∈# D)› and
‹¬ (b ∨ x1b (atm_of x1h) = SEEN_FAILED)› and
‹¬ (ba ∨ x1 (atm_of x1g) = SEEN_FAILED)› and
xb_x'c: ‹(xa, x'b)
∈ ⟨?get_propagation_reason x1g⟩option_rel› and
xa: ‹xa = Some xb› ‹x'b = Some x'c› and
‹(xb, x'c)
∈ (?get_propagation_reason x1g)› and
dist_tauto: ‹distinct_mset x'c ∧ ¬ tautology x'c› and
‹xb ∈# dom_m NU› and
‹2 ≤ length (NU ∝ xb)›
for x x' x1 x2 x1a x2a x1b x2b x1c x1d x2c x1e x2d x1f x2e x2f x'a x1g x2g x1h
x2h b ba xa x'b xb x'c
proof -
have [simp]: ‹mset (tl C) = remove1_mset (C!0) (mset C)› for C
by (cases C) auto
have [simp]:
‹x2 = (x1a, x2a)›
‹x' = (x1, x1a, x2a)›
‹x2d = (x1f, x2e)›
‹x2c = (x1e, x1f, x2e)›
‹last x1c = (x1d, x1e, x1f, x2e)›
‹x2b = (x1c, x2f)›
‹x = (x1b, x1c, x2f)›
‹xa = Some xb›
‹x'b = Some x'c›
‹x'c = mset (NU ∝ xb)›
using s get_literal_and_remove_of_analyse_wl xa xb_x'c
unfolding get_lit convert_analysis_list_def
by auto
then have x1d0: ‹length (NU ∝ xb) > 2 ⟹ x1g = -NU ∝ xb ! 0› ‹NU ∝ xb ≠ []› and
x1d: ‹-x1g ∈ set (watched_l (NU ∝ xb))›
using add_inv xb_x'c S_S' S'_S'' S unfolding twl_list_invs_def
by (auto 5 5 simp: state_wl_l_def twl_st_l_def)
have le2: ‹length (NU ∝ xb) ≥ 2›
using clauses_length_ge2[OF S'_S'' add_inv assms(10)] xb_x'c S_S'
by (auto simp: S)
have 0: ‹case lit_redundant_reason_stack (-x1g) NU xb of (i, k, j, ln) ⇒
j ≤ ln ∧ i ∈# dom_m NU ∧ 0 ≤ j ∧ 0 < i ∧ ln ≤ length (NU ∝ i) ∧
k < length (NU ∝ i) ∧ distinct (NU ∝ i) ∧ ¬ tautology (mset (NU ∝ i))›
for i j ln k
using s xx' get_literal_and_remove_of_analyse_wl xb_x'c x1d le2 dist_tauto
unfolding get_lit convert_analysis_list_def lit_redundant_rec_wl_ref_def
lit_redundant_reason_stack_def
by (auto split: if_splits)
have ‹(x1g, remove1_mset (- x1g) (mset (NU ∝ xb))) =
convert_analysis_l NU (lit_redundant_reason_stack (- x1g) NU xb)›
using s xx' get_literal_and_remove_of_analyse_wl xb_x'c x1d le2
unfolding get_lit convert_analysis_list_def lit_redundant_rec_wl_ref_def
lit_redundant_reason_stack_def
by (auto split: simp: Misc.slice_def drop_Suc simp: x1d0(1)
dest!: list_decomp_2)
then show ?thesis
using s xx' get_literal_and_remove_of_analyse_wl xb_x'c x1d 0
unfolding get_lit convert_analysis_list_def lit_redundant_rec_wl_ref_def
by (cases x2h rule: rev_cases)
(auto simp: drop_Suc uminus_lit_swap butlast_append
dest: list_decomp_2)
qed
have mark_failed_lits_wl: ‹mark_failed_lits_wl NU x2e x1b ≤ ⇓ Id (mark_failed_lits NU' x2d x1)›
if
‹(x, x') ∈ ?R› and
‹x' = (x1, x2)› and
‹x = (x1b, x2b)›
for x x' x2e x1b x1 x2 x2b x2d
using that unfolding mark_failed_lits_wl_def mark_failed_lits_def by auto
have ana: ‹last analyse = (fst (last analyse), fst (snd (last analyse)),
fst (snd (snd (last analyse))), snd (snd (snd (last analyse))))› for analyse
by (cases ‹last analyse›) auto
show ?thesis
supply convert_analysis_list_def[simp] hd_rev[simp] last_map[simp] rev_map[symmetric, simp]
unfolding lit_redundant_rec_wl_def lit_redundant_rec_def
apply (rewrite at ‹let _ = _ ∝ _ in _› Let_def)
apply (rewrite in ‹let _ = _ in _› ana)
apply (rewrite at ‹let _ = (_, _, _) in _› Let_def)
apply refine_rcg
subgoal using bounds_init unfolding analyse'_def by auto
subgoal for x x'
by (cases x, cases x')
(auto simp: lit_redundant_rec_wl_inv_def lit_redundant_rec_wl_ref_def)
subgoal by auto
subgoal by auto
subgoal using M'_def by (auto dest: convert_lits_l_imp_same_length)
subgoal by (auto simp: lit_redundant_rec_wl_inv_def lit_redundant_rec_wl_ref_def
elim!: neq_Nil_revE)
subgoal by (auto simp: lit_redundant_rec_wl_inv_def lit_redundant_rec_wl_ref_def
elim!: neq_Nil_revE)
subgoal by (auto simp: map_butlast rev_butlast_is_tl_rev lit_redundant_rec_wl_ref_def
dest: in_set_butlastD)
subgoal by (auto simp: map_butlast rev_butlast_is_tl_rev lit_redundant_rec_wl_ref_def
Misc.slice_def
dest: in_set_butlastD
elim!: neq_Nil_revE)
subgoal by (auto simp: map_butlast rev_butlast_is_tl_rev lit_redundant_rec_wl_ref_def
Misc.slice_def
dest: in_set_butlastD
elim!: neq_Nil_revE)
apply (rule get_literal_and_remove_of_analyse_wl; assumption)
subgoal by auto
subgoal by auto
subgoal using M'_def by auto
subgoal by auto
subgoal by auto
apply (rule mark_failed_lits_wl; assumption)
subgoal by (auto simp: lit_redundant_rec_wl_ref_def)
subgoal by auto
apply (rule get_propagation_reason; assumption)
apply assumption
apply (rule mark_failed_lits_wl; assumption)
subgoal by (auto simp: lit_redundant_rec_wl_ref_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: lit_redundant_rec_wl_ref_def)
subgoal for x x' x1 x2 x1a x2a x1b x2b x1c x1d x2c x1e x2d x1f x2e x2f x'a x1g x2g x1h
x2h b ba xa x'b xb x'c
by (rule resolve)
done
qed
definition literal_redundant_wl where
‹literal_redundant_wl M NU D cach L lbd = do {
ASSERT(-L ∈ lits_of_l M);
if get_level M L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE
then RETURN (cach, [], True)
else if cach (atm_of L) = SEEN_FAILED
then RETURN (cach, [], False)
else do {
C ← get_propagation_reason M (-L);
case C of
Some C ⇒ do{
ASSERT(C ∈# dom_m NU);
ASSERT(length (NU ∝ C) ≥ 2);
ASSERT(distinct (NU ∝ C) ∧ ¬tautology (mset (NU ∝ C)));
lit_redundant_rec_wl M NU D cach [lit_redundant_reason_stack (-L) NU C] lbd
}
| None ⇒ do {
RETURN (cach, [], False)
}
}
}›
lemma literal_redundant_wl_literal_redundant:
fixes S :: ‹nat twl_st_wl› and S' :: ‹nat twl_st_l› and S'' :: ‹nat twl_st› and NU M
defines
[simp]: ‹S''' ≡ state⇩W_of S''›
defines
‹M ≡ get_trail_wl S› and
M': ‹M' ≡ trail S'''› and
NU: ‹NU ≡ get_clauses_wl S› and
NU': ‹NU' ≡ mset `# ran_mf NU›
assumes
S_S': ‹(S, S') ∈ state_wl_l None› and
S'_S'': ‹(S', S'') ∈ twl_st_l None› and
‹M ≡ get_trail_wl S› and
M': ‹M' ≡ trail S'''› and
NU: ‹NU ≡ get_clauses_wl S› and
NU': ‹NU' ≡ mset `# ran_mf NU›
assumes
struct_invs: ‹twl_struct_invs S''› and
add_inv: ‹twl_list_invs S'› and
L_D: ‹L ∈# D› and
M_D: ‹M ⊨as CNot D›
shows
‹literal_redundant_wl M NU D cach L lbd ≤ ⇓
(Id ×⇩r {(analyse, analyse'). analyse' = convert_analysis_list NU analyse ∧
lit_redundant_rec_wl_ref NU analyse} ×⇩r bool_rel)
(literal_redundant M' NU' D cach L)›
(is ‹_ ≤ ⇓ (_ ×⇩r ?A ×⇩r _) _› is ‹_ ≤ ⇓ ?R _›)
proof -
obtain D' NE UE Q W where
S: ‹S = (M, NU, D', NE, UE, Q, W)›
using M_def NU by (cases S) auto
have M'_def: ‹(M, M') ∈ convert_lits_l NU (NE+UE)›
using NU S_S' S'_S'' S M' by (auto simp: twl_st_l_def state_wl_l_def)
have [simp]: ‹lits_of_l M' = lits_of_l M›
using M'_def by auto
have
no_smaller_propa: ‹cdcl⇩W_restart_mset.no_smaller_propa S'''› and
struct_invs': ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv S'''›
using struct_invs unfolding twl_struct_invs_def S'''_def[symmetric]
by fast+
have annots: ‹set (get_all_mark_of_propagated (trail S''')) ⊆
set_mset (cdcl⇩W_restart_mset.clauses S''')›
using struct_invs'
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by fast
have n_d: ‹no_dup (get_trail_wl S)›
using struct_invs' S_S' S'_S'' unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: twl_st_wl twl_st_l twl_st)
then have n_d: ‹no_dup M›
by (auto simp: S)
then have n_d': ‹no_dup M'›
using M'_def by (auto simp: S)
have uL_M: ‹-L ∈ lits_of_l M›
using L_D M_D by (auto dest!: multi_member_split)
have H: ‹lit_redundant_rec_wl M NU D cach analyse lbd
≤ ⇓ ?R (lit_redundant_rec M' NU' D cach analyse')›
if ‹analyse' = convert_analysis_list NU analyse› and
‹lit_redundant_rec_wl_ref NU analyse›
for analyse analyse'
using lit_redundant_rec_wl[of S S' S'' analyse D cach lbd, unfolded S'''_def[symmetric],
unfolded
M_def[symmetric] M'[symmetric] NU[symmetric] NU'[symmetric],
OF S_S' S'_S'' _ struct_invs add_inv]
that by (auto simp: )
have get_propagation_reason: ‹get_propagation_reason M (-L)
≤ ⇓ (⟨{(C', C). C = mset (NU ∝ C') ∧ C' ≠ 0 ∧ Propagated (-L) (mset (NU∝C')) ∈ set M'
∧ Propagated (-L) C' ∈ set M ∧ length (NU∝C') ≥ 2}⟩
option_rel)
(get_propagation_reason M' (-L))›
(is ‹_ ≤ ⇓ (⟨?get_propagation_reason⟩option_rel) _› is ?G1) and
propagated_L:
‹Propagated (-L) a ∈ set M ⟹ a ≠ 0 ∧ Propagated (- L) (mset (NU ∝ a)) ∈ set M'›
(is ‹?H2 ⟹ ?G2›)
if
lev0_rem: ‹¬ (get_level M' L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE)› and
ux1e_M: ‹- L ∈ lits_of_l M›
for a
proof -
have ‹Propagated (- L) (mset (NU ∝ a)) ∈ set M'› (is ?propa) and
‹a ≠ 0› (is ?a) and
‹length (NU ∝ a) ≥ 2› (is ?len)
if L_M: ‹Propagated (-L) a ∈ set M›
for a
proof -
have [simp]: ‹a ≠ 0›
proof
assume [simp]: ‹a = 0›
obtain E' where
x1d_M': ‹Propagated (- L) E' ∈ set M'› and
‹E' ∈# NE + UE›
using L_M M'_def by (auto dest: split_list simp: convert_lits_l_def p2rel_def
convert_lit.simps
elim!: list_rel_in_find_correspondanceE split: if_splits)
moreover have ‹unit_clss S'' = NE + UE›
using S_S' S'_S'' x1d_M' by (auto simp: S)
moreover have ‹Propagated (- L) E' ∈ set (get_trail S'')›
using S_S' S'_S'' x1d_M' by (auto simp: S state_wl_l_def twl_st_l_def M')
moreover have ‹0 < count_decided (get_trail S'')›
using lev0_rem S_S' S'_S'' count_decided_ge_get_level[of M L]
by (auto simp: S M' twl_st)
ultimately show False
using clauses_in_unit_clss_have_level0(1)[of S'' E' ‹- L›] lev0_rem ‹twl_struct_invs S''›
S_S' S'_S'' M'_def
by (auto simp: S)
qed
show ?propa and ?a
using that M'_def by (auto simp: convert_lits_l_def p2rel_def convert_lit.simps
elim!: list_rel_in_find_correspondanceE split: if_splits)
show ?len
using trail_length_ge2[OF S'_S'' add_inv struct_invs, of ‹- L› a] that S_S'
by (force simp: S)
qed note H = this
show ‹?H2 ⟹ ?G2›
using H by auto
show ?G1
using H
apply (auto simp: get_propagation_reason_def refine_rel_defs
get_propagation_reason_def intro!: RES_refine)
apply (case_tac s)
by auto
qed
have S''': ‹S''' = (get_trail S'', get_all_init_clss S'', get_all_learned_clss S'',
get_conflict S'')›
by (cases S'') (auto simp: S'''_def)
have [simp]: ‹mset (tl C) = remove1_mset (C!0) (mset C)› for C
by (cases C) auto
have S''_M': ‹(get_trail S'') = M'›
using M' S''' by auto
have [simp]: ‹length (NU ∝ C) > 2 ⟹ NU ∝ C ! 0 = -L› and
L_watched: ‹-L ∈ set (watched_l (NU ∝ C))› and
L_dist: ‹distinct (NU ∝ C)› and
L_tauto: ‹¬tautology (mset (NU ∝ C))›
if
in_trail: ‹Propagated (- L) C ∈ set M› and
lev: ‹¬ (get_level M' L = 0 ∨ cach (atm_of L) = SEEN_REMOVABLE)›
for C
using add_inv that propagated_L[OF lev _ in_trail] uL_M S_S' S'_S''
Propagated_in_trail_entailed[of ‹get_trail S''› ‹get_all_init_clss S''› ‹get_all_learned_clss S''›
‹get_conflict S''› ‹-L› ‹mset (NU ∝ C)›] struct_invs' unfolding S'''[symmetric]
by (auto simp: S twl_list_invs_def S''_M'; fail)+
have [dest]: ‹C ≠ {#}› if ‹Propagated (- L) C ∈ set M'› for C
proof -
have ‹a @ Propagated L mark # b = trail S''' ⟹ b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark›
for L mark a b
using struct_invs' unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by fast
then show ?thesis
using that S_S' S'_S'' M'_def M'
by (fastforce simp: S state_wl_l_def
twl_st_l_def convert_lits_l_def convert_lit.simps
list_rel_append2 list_rel_append1
elim!: list_relE3 list_relE4
elim: list_rel_in_find_correspondanceE split: if_splits
dest!: split_list p2relD)
qed
have le2: ‹Propagated (- L) C ∈ set M ⟹ C > 0 ⟹ length (NU ∝ C) ≥ 2› for C
using trail_length_ge2[OF S'_S'' add_inv struct_invs, of _ C] S_S'
by (auto simp: S)
have [simp]: ‹Propagated (- L) C ∈ set M ⟹ C > 0 ⟹ C ∈# dom_m NU› for C
using add_inv S_S' S'_S'' propagated_L[of C]
by (auto simp: S twl_list_invs_def state_wl_l_def
twl_st_l_def)
show ?thesis
unfolding literal_redundant_wl_def literal_redundant_def
apply (refine_rcg H get_propagation_reason)
subgoal by simp
subgoal using M'_def by simp
subgoal using M'_def by (auto simp: lit_redundant_rec_wl_ref_def)
subgoal by simp
subgoal by (auto simp: lit_redundant_rec_wl_ref_def)
apply (assumption)
subgoal by (auto simp: lit_redundant_rec_wl_ref_def)
subgoal by simp
subgoal by simp
subgoal for x x' C x'a
using le2[of C] L_watched[of C] L_dist[of C] L_tauto[of C]
by (auto simp: convert_analysis_list_def drop_Suc slice_0
lit_redundant_reason_stack_def slice_Suc slice_head slice_end
dest!: list_decomp_2)
subgoal for x x' C x'a
using le2[of C] L_watched[of C] L_dist[of C] L_tauto[of C]
by (auto simp: convert_analysis_list_def drop_Suc slice_0
lit_redundant_reason_stack_def slice_Suc slice_head slice_end
dest!: list_decomp_2)
subgoal for x x' C x'a
using le2[of C] L_watched[of C] L_dist[of C] L_tauto[of C]
by (auto simp: convert_analysis_list_def drop_Suc slice_0
lit_redundant_reason_stack_def slice_Suc slice_head slice_end
dest!: list_decomp_2)
subgoal for x x' C x'a
using le2[of C] L_watched[of C] L_dist[of C] L_tauto[of C]
by (auto simp: lit_redundant_reason_stack_def lit_redundant_rec_wl_ref_def)
done
qed
definition mark_failed_lits_stack_inv where
‹mark_failed_lits_stack_inv NU analyse = (λcach.
(∀(i, k, j, len) ∈ set analyse. j ≤ len ∧ len ≤ length (NU ∝ i) ∧ i ∈# dom_m NU ∧
k < length (NU ∝ i) ∧ j > 0))›
text ‹We mark all the literals from the current literal stack as failed, since every minimisation
call will find the same minimisation problem.›
definition mark_failed_lits_stack where
‹mark_failed_lits_stack 𝒜⇩i⇩n NU analyse cach = do {
( _, cach) ← WHILE⇩T⇗λ(_, cach). mark_failed_lits_stack_inv NU analyse cach⇖
(λ(i, cach). i < length analyse)
(λ(i, cach). do {
ASSERT(i < length analyse);
let (cls_idx, _, idx, _) = analyse ! i;
ASSERT(atm_of (NU ∝ cls_idx ! (idx - 1)) ∈# 𝒜⇩i⇩n);
RETURN (i+1, cach (atm_of (NU ∝ cls_idx ! (idx - 1)) := SEEN_FAILED))
})
(0, cach);
RETURN cach
}›
lemma mark_failed_lits_stack_mark_failed_lits_wl:
shows
‹(uncurry2 (mark_failed_lits_stack 𝒜), uncurry2 mark_failed_lits_wl) ∈
[λ((NU, analyse), cach). literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf NU) ∧
mark_failed_lits_stack_inv NU analyse cach]⇩f
Id ×⇩f Id ×⇩f Id → ⟨Id⟩nres_rel›
proof -
have ‹mark_failed_lits_stack 𝒜 NU analyse cach ≤ (mark_failed_lits_wl NU analyse cach)›
if
NU_ℒ⇩i⇩n: ‹literals_are_in_ℒ⇩i⇩n_mm 𝒜 (mset `# ran_mf NU)› and
init: ‹mark_failed_lits_stack_inv NU analyse cach›
for NU analyse cach
proof -
define I where
‹I = (λ(i :: nat, cach'). (∀L. cach' L = SEEN_REMOVABLE ⟶ cach L = SEEN_REMOVABLE))›
have valid_atm: ‹atm_of (NU ∝ cls_idx ! (idx - 1)) ∈# 𝒜›
if
‹I s› and
‹case s of (i, cach) ⇒ i < length analyse› and
‹case s of (i, cach) ⇒ mark_failed_lits_stack_inv NU analyse cach› and
‹s = (i, cach)› and
i: ‹i < length analyse› and
‹analyse ! i = (cls_idx, k)› ‹k = (k0, k')› ‹k' = (idx, len)›
for s i cach cls_idx idx k len k' k'' k0
proof -
have [iff]: ‹(∀a b. (a, b) ∉ set analyse) ⟷ False›
using i by (cases analyse) auto
show ?thesis
unfolding in_ℒ⇩a⇩l⇩l_atm_of_in_atms_of_iff[symmetric] atms_of_ℒ⇩a⇩l⇩l_𝒜⇩i⇩n[symmetric]
apply (rule literals_are_in_ℒ⇩i⇩n_mm_in_ℒ⇩a⇩l⇩l)
using NU_ℒ⇩i⇩n that nth_mem[of i analyse]
by (auto simp: mark_failed_lits_stack_inv_def I_def)
qed
show ?thesis
unfolding mark_failed_lits_stack_def mark_failed_lits_wl_def
apply (refine_vcg WHILEIT_rule_stronger_inv[where R = ‹measure (λ(i, _). length analyse -i)›
and I' = I])
subgoal by auto
subgoal using init by simp
subgoal unfolding I_def by auto
subgoal by auto
subgoal for s i cach cls_idx idx
by (rule valid_atm)
subgoal unfolding mark_failed_lits_stack_inv_def by auto
subgoal unfolding I_def by auto
subgoal by auto
subgoal unfolding I_def by auto
done
qed
then show ?thesis
by (intro frefI nres_relI) auto
qed
end