Theory CDCL.Pragmatic

theory Pragmatic_CDCL imports CDCL.CDCL_W_Restart CDCL.CDCL_W_Abstract_State begin (*TODO Move*) lemma get_all_mark_of_propagated_alt_def: ‹set (get_all_mark_of_propagated M) = {C. ∃L. Propagated L C ∈ set M}› by (induction M rule: ann_lit_list_induct) auto chapter ‹Pragmatic CDCL› text ‹ The idea of this calculus is to sit between the nice and abstract CDCL calculus and the first step towards the implementation, TWL. Pragmatic is not used to mean incomplete as Jasmin Blanchette for his superposition, but to mean that it is closer to the idead behind SAT implementation. Therefore, the calculus will contain a few things that cannot be expressed in CDCL, but are important in a SAT solver: ▸ To make it possible to express subsumption, we split our clauses in two parts: the subsumed clauses and the non-subsumed clauses. The CDCL calculus sees both of them together, but we only need the latter. ▸ We also have components for special clauses that contains a literal set at level 0. We need that component anyway for clauses of length 1 when expressing two watched literals. ▸ Adding clauses: if an init clause is subsumed by a learned clauses, it is better to add that clauses to the set of init clauses Armin Biere calls the non-subsumed initial clauses ``irredundant'', because they cannot be removed anymore. The ``CDCL'' operates on the non-subsumed clauses and we show that this is enough to coonnect it to a CDCL that operates on all clauses. The drawback of this approach is that we cannot remove literals, even if they do not appear anymore in the non-subsumed clauses. However, as these atoms will never appear in a conflict clause, they will very soon be at the end of the decision heuristic and, therefore, will not interfere nor slow down the solving process too much (they still occupy some memory locations, hence a small impact). The second idea was already included in the formalization of TWL because of (i) clauses of length one do not have two literals to watch; (ii) moving them away makes garbage collecting easier, because no reason at level 0 on the trail is included in the set of clauses. We also started to implement the ideas one and three, but we realised while thinking about restarts that separate rules are needed to avoid a lot of copy-and-paste. It was also not clear how to add subsumption detection on the fly without restart (like done right after a backtrack in CaDiCaL or in SPASS). In the end, we decided to go for a separate calculus that incorporates all theses rules: The idea is to have CDCL as the core part of the calculus and other rules that are optional. Termination still comes from the CDCL calculus: We do not want to apply the other rules exhaustively. Non-satisfiability-preserving clause additions are possible if all models after adding a clause are also models from the set of clauses before adding that clause. The calculus as expressed here does not deal with global transformations, like renumbering of variables or symmetry breaking. It only supports clause addition. There are still a few things that are missing in this calculus and require further thinking: ▸ Non-satisfiability-preserving clause elimination (blocked clause elimination, covered clauses). These transformations requires to reconstruct the model, and it also not clear how to find these clauses efficiently. Reconstruction is not that easy to express, and it is not so clear how to implement it in the SAT solver. ▸ Variable Elimination. Here reconstruction is also required. This technique is however extremely powerful and likely a must for every SAT solver. For the calculus we have three layers: ▸ the core corresponds to the application to most CDCL rules. Correctness and completeness come from this level. The rules are applied until completion. ▸ the terminating core (tcore) additionally includes rule that makes it possible to handle clauses of length 1. Termination comes from this level. The rules are optional. ▸ the full calculus also includes rule to do inprocessing (and restarts). The rules are optional too. In order to keep the core small, if backtrack learns a unit clause, we use one step from the tcore. At this level of the presentation, the special case of the unit clause does not matter. However, it is important for the calculus with watched literals, since these clauses cannot be watched. TODO: ▪ model reconstruction › type_synonym 'v prag_st = ‹('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option × 'v clauses × 'v clauses × 'v clauses × 'v clauses × 'v clauses × 'v clauses› fun state_of :: ‹'v prag_st ⇒ 'v cdcl_W_restart_mset› where ‹state_of (M, N, U, C, NE, UE, NS, US, N0, U0) = (M, N + NE + NS + N0, U + UE + US + U0, C)› declare cdcl_W_restart_mset_state[simp] named_theorems ptwl ‹Theorems to simplify the state› section ‹Conversion› fun pget_trail :: ‹'v prag_st ⇒ ('v, 'v clause) ann_lit list› where ‹pget_trail (M, _, _, _, _, _, _, _) = M› fun set_conflict :: ‹'v clause ⇒ 'v prag_st ⇒ 'v prag_st› where ‹set_conflict D (M, N, U, _, NE, UE, NS, US) = (M, N, U, Some D, NE, UE, NS, US)› fun pget_conflict :: ‹'v prag_st ⇒ 'v clause option› where ‹pget_conflict (M, N, U, D, NE, UE, WS, Q) = D› fun pget_clauses :: ‹'v prag_st ⇒ 'v clauses› where ‹pget_clauses (M, N, U, D, NE, UE, NS, US) = N + U› fun pget_init_clauses :: ‹'v prag_st ⇒ 'v clauses› where ‹pget_init_clauses (M, N, U, D, NE, UE, NS, US) = N› fun punit_clss :: ‹'v prag_st ⇒ 'v clauses› where ‹punit_clss (M, N, U, D, NE, UE, NS, US) = NE + UE› fun punit_init_clauses :: ‹'v prag_st ⇒ 'v clauses› where ‹punit_init_clauses (M, N, U, D, NE, UE, NS, US) = NE› fun punit_clauses :: ‹'v prag_st ⇒ 'v clauses› where ‹punit_clauses (M, N, U, D, NE, UE, NS, US) = NE + UE› fun pclauses0 :: ‹'v prag_st ⇒ 'v clauses› where ‹pclauses0 (M, N, U, D, NE, UE, NS, US, N0, U0) = N0 + U0› fun pinit_clauses0 :: ‹'v prag_st ⇒ 'v clauses› where ‹pinit_clauses0 (M, N, U, D, NE, UE, NS, US,N0,U0) = N0› fun plearned_clauses0 :: ‹'v prag_st ⇒ 'v clauses› where ‹plearned_clauses0 (M, N, U, D, NE, UE, NS, US,N0,U0) = U0› fun psubsumed_learned_clss :: ‹'v prag_st ⇒ 'v clause multiset› where ‹psubsumed_learned_clss (M, N, U, D, NE, UE, NS, US, N0, U0) = US› fun psubsumed_init_clauses :: ‹'v prag_st ⇒ 'v clauses› where ‹psubsumed_init_clauses (M, N, U, D, NE, UE, NS, US) = NS› fun pget_all_init_clss :: ‹'v prag_st ⇒ 'v clause multiset› where ‹pget_all_init_clss (M, N, U, D, NE, UE, NS, US, N0, U0) = N + NE + NS + N0› fun pget_learned_clss :: ‹'v prag_st ⇒ 'v clauses› where ‹pget_learned_clss (M, N, U, D, NE, UE, NS, US) = U› fun psubsumed_learned_clauses :: ‹'v prag_st ⇒ 'v clauses› where ‹psubsumed_learned_clauses (M, N, U, D, NE, UE, NS, US, N0, U0) = US› fun psubsumed_clauses :: ‹'v prag_st ⇒ 'v clauses› where ‹psubsumed_clauses (M, N, U, D, NE, UE, NS, US, N0, U0) = NS + US› fun pget_init_learned_clss :: ‹'v prag_st ⇒ 'v clauses› where ‹pget_init_learned_clss (_, N, U, _, _, UE, NS, US) = UE› fun pget_all_learned_clss :: ‹'v prag_st ⇒ 'v clauses› where ‹pget_all_learned_clss (_, N, U, _, _, UE, NS, US, N0, U0) = U + UE + US + U0› fun pget_all_clss :: ‹'v prag_st ⇒ 'v clause multiset› where ‹pget_all_clss (M, N, U, D, NE, UE, NS, US, N0, U0) = N + NE + NS + N0 + U + UE + US + U0› lemma [ptwl]: ‹trail (state_of S) = pget_trail S› by (solves ‹cases S; auto›) declare ptwl[simp] section ‹The old rules› inductive cdcl_propagate :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where propagate: ‹cdcl_propagate (M, N, U, None, NE, UE, NS, US, N0, U0) (Propagated L' D # M, N, U, None, NE, UE, NS, US, N0, U0)› if ‹L' ∈# D› and ‹M ⊨as CNot (remove1_mset L' D)› and ‹undefined_lit M L'› ‹D ∈# N + U› inductive cdcl_conflict :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where conflict: ‹cdcl_conflict (M, N, U, None, NE, UE, NS, US, N0, U0) (M, N, U, Some D, NE, UE, NS, US, N0, U0)› if ‹M ⊨as CNot D› and ‹D ∈# N + U› inductive cdcl_decide :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where decide: ‹cdcl_decide (M, N, U, None, NE, UE, NS, US, N0, U0) (Decided L' # M, N, U, None, NE, UE, NS, US, N0, U0)› if ‹undefined_lit M L'› and ‹atm_of L' ∈ atms_of_mm (N + NE + NS + N0)› inductive cdcl_skip :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where skip: ‹cdcl_skip (Propagated L' C # M, N, U, Some D, NE, UE, NS, US, N0, U0) (M, N, U, Some D, NE, UE, NS, US, N0, U0)› if ‹-L' ∉# D› and ‹D ≠ {#}› inductive cdcl_resolve :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where resolve: ‹cdcl_resolve (Propagated L' C # M, N, U, Some D, NE, UE, NS, US, N0, U0) (M, N, U, Some (cdcl_W_restart_mset.resolve_cls L' D C), NE, UE, NS, US, N0, U0)› if ‹-L' ∈# D› and ‹get_maximum_level (Propagated L' C # M) (remove1_mset (-L') D) = count_decided M› and ‹L' ∈# C› inductive cdcl_backtrack :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where ‹cdcl_backtrack (M, N, U, Some (add_mset L D), NE, UE, NS, US, N0, U0) (Propagated L (add_mset L D') # M1, N, add_mset (add_mset L D') U, None, NE, UE, NS, US, N0, U0)› if ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M)› and ‹get_level M L = count_decided M› and ‹get_level M L = get_maximum_level M (add_mset L D')› and ‹get_maximum_level M D' ≡ i› and ‹get_level M K = i + 1› and ‹D' ⊆# D› and ‹N + U + NE + UE + NS + US + N0 + U0 ⊨pm add_mset L D'› text ‹ Restart are already slightly restricted: we cannot remove literals set at level 0. › inductive cdcl_restart :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where cdcl_restart: ‹cdcl_restart (M, N, U, None, NE, UE, NS, US, N0, U0) (M', N, U, None, NE, UE, NS, US, N0, U0)› if ‹(M2, Decided K # M1) ∈ set (get_all_ann_decomposition M)› inductive cdcl_forget :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where cdcl_forget: ‹cdcl_forget (M, N, add_mset C U, None, NE, UE, NS, US, N0, U0) (M', N, U, None, NE, UE, NS, US, N0, U0)› if ‹Propagated L C ∉ set M› | cdcl_forget_subsumed: ‹cdcl_forget (M, N, U, None, NE, UE, NS, add_mset C US, N0, U0) (M', N, U, None, NE, UE, NS, US, N0, U0)› inductive pcdcl_core :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› for S T :: ‹'v prag_st› where ‹cdcl_conflict S T ⟹ pcdcl_core S T› | ‹cdcl_propagate S T ⟹ pcdcl_core S T› | ‹cdcl_decide S T ⟹ pcdcl_core S T› | ‹cdcl_skip S T ⟹ pcdcl_core S T› | ‹cdcl_resolve S T ⟹ pcdcl_core S T› | ‹cdcl_backtrack S T ⟹ pcdcl_core S T› inductive pcdcl_core_stgy :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› for S T :: ‹'v prag_st› where ‹cdcl_conflict S T ⟹ pcdcl_core_stgy S T› | ‹cdcl_propagate S T ⟹ pcdcl_core_stgy S T› | ‹no_step cdcl_conflict S ⟹ no_step cdcl_propagate S ⟹ cdcl_decide S T ⟹ pcdcl_core_stgy S T› | ‹cdcl_skip S T ⟹ pcdcl_core_stgy S T› | ‹cdcl_resolve S T ⟹ pcdcl_core_stgy S T› | ‹cdcl_backtrack S T ⟹ pcdcl_core_stgy S T› section ‹The new rules› text ‹Now the different part› inductive cdcl_subsumed :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where subsumed_II: ‹cdcl_subsumed (M, N + {#C,C'#}, U, D, NE, UE, NS, US, N0, U0) (M, add_mset C N, U, D, NE, UE, add_mset C' NS, US, N0, U0)› if ‹C ⊆# C'› | subsumed_LL: ‹cdcl_subsumed (M, N, U + {#C,C'#}, D, NE, UE, NS, US, N0, U0) (M, N, add_mset C U, D, NE, UE, NS, add_mset C' US, N0, U0)› if ‹C ⊆# C'› | subsumed_IL: ‹cdcl_subsumed (M, add_mset C N, add_mset C' U, D, NE, UE, NS, US, N0, U0) (M, add_mset C N, U, D, NE, UE, NS, add_mset C' US, N0, U0)› if ‹C ⊆# C'› lemma state_of_cdcl_subsumed: ‹cdcl_subsumed S T ⟹ state_of S = state_of T› by (induction rule: cdcl_subsumed.induct) auto text ‹ Resolution requires to restart (or a very careful thinking where the clause can be used, so for now, we require level 0). The names 'I' and 'L' refers to 'irredundant' and 'learnt'. We need the assumption term‹¬tautology (C + C')› because learned clauses cannot be tautologies. › inductive cdcl_resolution :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where resolution_II: ‹cdcl_resolution (M, N + {#add_mset L C, add_mset (-L) C'#}, U, D, NE, UE, NS, US, N0, U0) (M, N + {#add_mset L C, add_mset (-L) C', remdups_mset (C + C')#}, U, D, NE, UE, NS, US, N0, U0)› if ‹count_decided M = 0› | resolution_LL: ‹cdcl_resolution (M, N, U + {#add_mset L C, add_mset (-L) C'#}, D, NE, UE, NS, US, N0, U0) (M, N, U + {#add_mset L C, add_mset (-L) C', remdups_mset (C + C')#}, D, NE, UE, NS, US, N0, U0)› if ‹count_decided M = 0› and ‹¬tautology (C + C')› | resolution_IL: ‹cdcl_resolution (M, N + {#add_mset L C#}, U + {#add_mset (-L) C'#}, D, NE, UE, NS, US, N0, U0) (M, N + {#add_mset L C#}, U + {#add_mset (-L) C', remdups_mset (C + C')#}, D, NE, UE, NS, US, N0, U0)› if ‹count_decided M = 0› and ‹¬tautology (C + C')› lemma cdcl_resolution_still_entailed: ‹cdcl_resolution S T ⟹ consistent_interp I ⟹ I ⊨m pget_all_init_clss S ⟹ I ⊨m pget_all_init_clss T› apply (induction rule: cdcl_resolution.induct) subgoal for M N L C C' U D NE UE NS US by (auto simp: consistent_interp_def) subgoal by auto subgoal by auto done text ‹ Tautologies are always entailed by the clause set, but not necessarily entailed by a non-total model of the clauses. Therefore, we do not learn tautologies. E.g.: term‹(A ∨ B) ∧ (A ∨ C)› entails the clause term‹(¬B ∨ B)›, but the model containing only the literal term‹A› does not entail the latter. This is also why this predicate is different from the previous one: in term‹cdcl_resolution› we can learn a tautology because we do not destroy models. This is not the case in this predicate. This function has nothing to with CDCL's learn: any clause can be learned by this function, including the empty clause. TODO: for clauses in U, drop entailement and level test! › inductive cdcl_learn_clause :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where learn_clause: ‹cdcl_learn_clause (M, N, U, D, NE, UE, NS, US, N0, U0) (M, add_mset C N, U, D, NE, UE, NS, US, N0, U0)› if ‹atms_of C ⊆ atms_of_mm (N + NE + NS + N0)› and ‹N +NE + NS + N0 ⊨pm C› and ‹¬tautology C› and ‹count_decided M = 0› and ‹distinct_mset C› | learn_clause_R: ‹cdcl_learn_clause (M, N, U, D, NE, UE, NS, US, N0, U0) (M, N, add_mset C U, D, NE, UE, NS, US, N0, U0)› if ‹atms_of C ⊆ atms_of_mm (N + NE + NS + N0)› and ‹N +NE + NS + N0 ⊨pm C› and ‹¬tautology C› and ‹count_decided M = 0› and ‹distinct_mset C› | promote_clause: ‹cdcl_learn_clause (M, N, add_mset C U, D, NE, UE, NS, US, N0, U0) (M, add_mset C N, U, D, NE, UE, NS, US, N0, U0)› if ‹¬tautology C› lemma cdcl_learn_clause_still_entailed: ‹cdcl_learn_clause S T ⟹ consistent_interp I ⟹ cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S) ⟹ I ⊨m pget_all_init_clss S ⟹ I ⊨m pget_all_init_clss T› apply (induction rule: cdcl_learn_clause.induct) subgoal for C N NE NS N0 M U D UE US U0 using true_clss_cls_true_clss_true_cls[of ‹set_mset (N+NE+NS+N0)› C I] by auto subgoal for C N NE NS N0 M U D UE US U0 by auto subgoal by (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def dest: true_clss_cls_true_clss_true_cls) done text ‹Detection and removal of pure literals.› inductive cdcl_pure_literal_remove :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where cdcl_pure_literal_remove: ‹cdcl_pure_literal_remove (M, N, U, None, NE, UE, NS, US, N0, U0) (Propagated L {#L#} # M, N, U, None, add_mset {#L#} NE, UE, NS, US, N0, U0)› if ‹-L ∉ ⋃(set_mset ` (set_mset N))› ‹atm_of L ∈ atms_of_mm (N+NE+NS+N0)› ‹undefined_lit M L› ‹count_decided M = 0› lemma pure_literal_can_be_removed: assumes ‹-L ∉ ⋃(set_mset ` (set_mset N))› and ‹I ⊨m N› shows ‹insert L (I - {-L}) ⊨m N› using assms by (induction N) (auto simp: true_cls_def) text ‹ Inprocessing version of propagate and conflict. The rules are very liberal to be used as freely as possible. They are similar to their CDCL counterpart, but do not cover exactly the same use-cases. › inductive cdcl_inp_propagate :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where propagate: ‹cdcl_inp_propagate (M, N, U, None, NE, UE, NS, US, N0, U0) (Propagated L' D # M, N, U, None, NE, UE, NS, US, N0, U0)› if ‹L' ∈# D› and ‹M ⊨as CNot (remove1_mset L' D)› and ‹undefined_lit M L'› ‹D ∈# N + U + NE + UE + NS + US› and ‹count_decided M = 0› inductive cdcl_inp_conflict :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where conflict: ‹cdcl_inp_conflict (M, N, U, None, NE, UE, NS, US, N0, U0) (M, N, U, Some {#}, NE, UE, NS, US, N0, U0)› if ‹N + NE + NS + N0 ⊨pm {#}› and ‹count_decided M = 0› inductive cdcl_flush_unit :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where learn_unit_clause_R: ‹cdcl_flush_unit (M, add_mset {#L#} N, U, D, NE, UE, NS, US, N0, U0) (M, N, U, D, add_mset {#L#} NE, UE, NS, US, N0, U0)› if ‹get_level M L = 0› ‹L ∈ lits_of_l M› | learn_unit_clause_I: ‹cdcl_flush_unit (M, N, add_mset {#L#} U, D, NE, UE, NS, US, N0, U0) (M, N, U, D, NE, add_mset {#L#} UE, NS, US, N0, U0)› if ‹get_level M L = 0› ‹L ∈ lits_of_l M› inductive cdcl_unitres_true :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where ‹cdcl_unitres_true (M, add_mset (add_mset L C) N, U, D, NE, UE, NS, US, N0, U0) (M, N, U, D, add_mset (add_mset L C) NE, UE, NS, US, N0, U0)› if ‹get_level M L = 0› ‹L ∈ lits_of_l M› | ‹cdcl_unitres_true (M, N, add_mset (add_mset L C) U, D, NE, UE, NS, US, N0, U0) (M, N, U, D, NE, add_mset (add_mset L C) UE, NS, US, N0, U0)› if ‹get_level M L = 0› ‹L ∈ lits_of_l M› text ‹Even if we don't generated tautologies in the learnt clauses, we still keep the possibility to remove them later› inductive cdcl_promote_false :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where ‹cdcl_promote_false (M, add_mset {#} N, U, D, NE, UE, NS, US, N0, U0) (M, N, U, Some {#}, NE, UE, NS, US, add_mset {#} N0, U0)› | ‹cdcl_promote_false (M, N, add_mset {#} U, D, NE, UE, NS, US, N0, U0) (M, N, U, Some {#}, NE, UE, NS, US, N0, add_mset {#} U0)› inductive pcdcl :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where ‹pcdcl_core S T ⟹ pcdcl S T› | ‹cdcl_learn_clause S T ⟹ pcdcl S T› | ‹cdcl_resolution S T ⟹ pcdcl S T› | ‹cdcl_subsumed S T ⟹ pcdcl S T› | ‹cdcl_flush_unit S T ⟹ pcdcl S T› | ‹cdcl_inp_propagate S T ⟹ pcdcl S T› | ‹cdcl_inp_conflict S T ⟹ pcdcl S T› | ‹cdcl_unitres_true S T ⟹ pcdcl S T› | ‹cdcl_promote_false S T ⟹ pcdcl S T› | ‹cdcl_pure_literal_remove S T ⟹ pcdcl S T› inductive pcdcl_stgy :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› for S T :: ‹'v prag_st› where ‹pcdcl_core_stgy S T ⟹ pcdcl_stgy S T› | ‹cdcl_learn_clause S T ⟹ pcdcl_stgy S T› | ‹cdcl_resolution S T ⟹ pcdcl_stgy S T› | ‹cdcl_subsumed S T ⟹ pcdcl_stgy S T›| ‹cdcl_flush_unit S T ⟹ pcdcl_stgy S T› | ‹cdcl_inp_propagate S T ⟹ pcdcl_stgy S T› | ‹cdcl_inp_conflict S T ⟹ pcdcl_stgy S T› | ‹cdcl_unitres_true S T ⟹ pcdcl_stgy S T› lemma pcdcl_core_stgy_pcdcl: ‹pcdcl_core_stgy S T ⟹ pcdcl_core S T› by (auto simp: pcdcl_core.simps pcdcl_core_stgy.simps) lemma pcdcl_stgy_pcdcl: ‹pcdcl_stgy S T ⟹ pcdcl S T› by (auto simp: pcdcl.simps pcdcl_stgy.simps pcdcl_core_stgy_pcdcl) lemma rtranclp_pcdcl_stgy_pcdcl: ‹pcdcl_stgy^*^* S T ⟹ pcdcl^*^* S T› by (induction rule: rtranclp_induct) (auto dest!: pcdcl_stgy_pcdcl) section ‹Invariants› text ‹ To avoid adding a new component, we store tautologies in the subsumed components, even though we could also store them separately. Finally, we really want to get rid of tautologies from the clause set. They require special cases in the arena module. › definition psubsumed_invs :: ‹'v prag_st ⇒ bool› where ‹psubsumed_invs S ⟷ (∀C∈#psubsumed_init_clauses S. tautology C ∨ (∃C'∈#pget_init_clauses S+punit_init_clauses S+pinit_clauses0 S. C' ⊆# C)) ∧ (∀C∈#psubsumed_learned_clauses S. tautology C ∨ (∃C'∈#pget_clauses S+punit_clauses S+pclauses0 S. C' ⊆# C))› text ‹ In the TWL version, we also had term‹(∀C ∈# NE + UE. (∃L. L ∈# C ∧ (D = None ∨ count_decided M > 0 ⟶ get_level M L = 0 ∧ L ∈ lits_of_l M)))› as definition. This make is possible to express the conflict analysis at level 0. However, it makes the code easier to not do this analysis, because we already know that we will derive the empty clause (but do not know what the trail will be). We could simplify the invariant to term‹(∀C ∈# NE + UE. (∃L. L ∈# C ∧ (get_level M L = 0 ∧ L ∈ lits_of_l M)))› at the price of an uglier correctness theorem. Final remark, we could simplify the invariant in another way: We could have term‹D={#L#}›. This, however, requires that we either remove all literals set at level 0, including in ∗‹reasons›, which we would rather avoid, or add the new clause term‹{#L#}› each time we propagate a clause at level 0 and change the reason to this new clause. In either cases, we could use the subsumed components to store the clauses. › fun entailed_clss_inv :: ‹'v prag_st ⇒ bool› where ‹entailed_clss_inv (M, N, U, D, NE, UE, NS, US) ⟷ (∀C ∈# NE + UE. (∃L. L ∈# C ∧ ((D = None ∨ count_decided M > 0) ⟶ (get_level M L = 0 ∧ L ∈ lits_of_l M))))› lemmas entailed_clss_inv_def = entailed_clss_inv.simps lemmas [simp del] = entailed_clss_inv.simps fun clauses0_inv :: ‹'v prag_st ⇒ bool› where ‹clauses0_inv (M, N, U, D, NE, UE, NS, US, N0, U0) ⟷ (∀C ∈# N0 + U0. C = {#}) ∧ ({#} ∈# N0 + U0 ⟶ D = Some {#})› lemma clauses0_inv_def: ‹clauses0_inv (M, N, U, D, NE, UE, NS, US, N0, U0) ⟷ (∀C ∈# N0 + U0. C = {#}) ∧ (N0 + U0 ≠ {#} ⟶ D = Some {#})› by (auto dest!: multi_member_split) lemmas [simp del] = clauses0_inv.simps section ‹Relation to CDCL› lemma cdcl_decide_is_decide: ‹cdcl_decide S T ⟹ cdcl_W_restart_mset.decide (state_of S) (state_of T)› apply (cases rule: cdcl_decide.cases, assumption) apply (rule_tac L=L' in cdcl_W_restart_mset.decide.intros) by auto lemma decide_is_cdcl_decide: ‹cdcl_W_restart_mset.decide (state_of S) T ⟹ Ex(cdcl_decide S)› apply (cases S, hypsubst) apply (cases rule: cdcl_W_restart_mset.decide.cases, assumption) apply (rule exI[of _ ‹(_, _, _, None, _, _, _, _)›]) by (auto intro!: cdcl_decide.intros) lemma cdcl_skip_is_skip: ‹cdcl_skip S T ⟹ cdcl_W_restart_mset.skip (state_of S) (state_of T)› apply (cases rule: cdcl_skip.cases, assumption) apply (rule_tac L=L' and C'=C and E=D and M=M in cdcl_W_restart_mset.skip.intros) by auto lemma skip_is_cdcl_skip: ‹cdcl_W_restart_mset.skip (state_of S) T ⟹ Ex(cdcl_skip S)› apply (cases rule: cdcl_W_restart_mset.skip.cases, assumption) apply (cases S) apply (auto simp: cdcl_skip.simps) done lemma cdcl_resolve_is_resolve: ‹cdcl_resolve S T ⟹ cdcl_W_restart_mset.resolve (state_of S) (state_of T)› apply (cases rule: cdcl_resolve.cases, assumption) apply (rule_tac L=L' and E=C in cdcl_W_restart_mset.resolve.intros) by auto lemma resolve_is_cdcl_resolve: ‹cdcl_W_restart_mset.resolve (state_of S) T ⟹ Ex(cdcl_resolve S)› apply (cases rule: cdcl_W_restart_mset.resolve.cases, assumption) apply (cases S; cases ‹pget_trail S›) apply (auto simp: cdcl_resolve.simps) done lemma cdcl_backtrack_is_backtrack: ‹cdcl_backtrack S T ⟹ cdcl_W_restart_mset.backtrack (state_of S) (state_of T)› apply (cases rule: cdcl_backtrack.cases, assumption) apply (rule_tac L=L and D'=D' and D=D and K=K in cdcl_W_restart_mset.backtrack.intros) by (auto simp: clauses_def ac_simps cdcl_W_restart_mset_reduce_trail_to) lemma backtrack_is_cdcl_backtrack: ‹cdcl_W_restart_mset.backtrack (state_of S) T ⟹ Ex(cdcl_backtrack S)› apply (cases rule: cdcl_W_restart_mset.backtrack.cases, assumption) apply (cases S; cases T) apply (simp add: cdcl_backtrack.simps clauses_def add_mset_eq_add_mset cdcl_W_restart_mset_reduce_trail_to conj_disj_distribR ex_disj_distrib cong: if_cong) apply (rule disjI1) apply (rule_tac x=K in exI) apply auto apply (rule_tac x=D' in exI) apply (auto simp: Un_commute Un_assoc) apply (rule back_subst[of ‹λa. a ⊨p _›]) apply assumption apply auto done lemma cdcl_conflict_is_conflict: ‹cdcl_conflict S T ⟹ cdcl_W_restart_mset.conflict (state_of S) (state_of T)› apply (cases rule: cdcl_conflict.cases, assumption) apply (rule_tac D=D in cdcl_W_restart_mset.conflict.intros) by (auto simp: clauses_def) lemma conflict_is_cdcl_conflictD: assumes confl: ‹cdcl_W_restart_mset.conflict (state_of S) T› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› and clss0: ‹clauses0_inv S› shows ‹Ex (cdcl_conflict S)› proof - obtain C where C: ‹C ∈# cdcl_W_restart_mset.clauses (state_of S)› and confl: ‹trail (state_of S) ⊨as CNot C› and conf: ‹conflicting (state_of S) = None› and ‹T ∼m update_conflicting (Some C) (state_of S)› using cdcl_W_restart_mset.conflictE[OF confl] by metis have p0: ‹pclauses0 S = {#}› using clss0 conf by (cases S; auto 4 3 simp: entailed_clss_inv_def cdcl_W_restart_mset_state clauses0_inv_def true_annots_true_cls dest!: multi_member_split dest: no_dup_consistentD) have n_d: ‹no_dup (pget_trail S)› 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 then have ‹C ∉# punit_clauses S› ‹C ∉# pclauses0 S› using ent confl conf clss0 consistent_CNot_not_tautology[of ‹lits_of_l (pget_trail S)› C] distinct_consistent_interp[OF n_d] by (cases S; auto 4 3 simp: entailed_clss_inv_def cdcl_W_restart_mset_state clauses0_inv_def true_annots_true_cls dest!: multi_member_split dest: no_dup_consistentD; fail)+ moreover have ‹C ∈# psubsumed_clauses S ⟹ ∃C' ∈# pget_clauses S. trail (state_of S) ⊨as CNot C'› using sub confl conf n_d ent p0 consistent_CNot_not_tautology[of ‹lits_of_l (pget_trail S)› C, OF distinct_consistent_interp] apply (cases S) apply (auto simp: psubsumed_invs_def true_annots_true_cls entailed_clss_inv_def insert_subset_eq_iff dest: distinct_consistent_interp mset_subset_eqD no_dup_consistentD dest!: multi_member_split) apply (auto simp add: mset_subset_eqD true_clss_def_iff_negation_in_model tautology_decomp' insert_subset_eq_iff dest: no_dup_consistentD) done ultimately show ?thesis using C confl conf by (cases S) (auto simp: cdcl_conflict.simps clauses_def) qed lemma cdcl_propagate_is_propagate: ‹cdcl_propagate S T ⟹ cdcl_W_restart_mset.propagate (state_of S) (state_of T)› apply (cases rule: cdcl_propagate.cases, assumption) apply (rule_tac L=L' and E=D in cdcl_W_restart_mset.propagate.intros) by (auto simp: clauses_def) lemma propagate_is_cdcl_propagateD: assumes confl: ‹cdcl_W_restart_mset.propagate (state_of S) T› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› and clss0: ‹clauses0_inv S› shows ‹Ex (cdcl_propagate S) ∨ Ex(cdcl_conflict S)› proof - obtain L C where C: ‹C ∈# cdcl_W_restart_mset.clauses (state_of S)› and conf: ‹conflicting (state_of S) = None› and confl: ‹trail (state_of S) ⊨as CNot (remove1_mset L C)› and LC: ‹L ∈# C› and undef: ‹undefined_lit (trail (state_of S)) L› and ‹T ∼m cons_trail (Propagated L C) (state_of S)› using cdcl_W_restart_mset.propagateE[OF confl] by metis have n_d: ‹no_dup (pget_trail S)› 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 then have ‹C ∉# punit_clauses S› ‹C ∉# pclauses0 S› using ent confl conf LC undef clss0 consistent_CNot_not_tautology[of ‹lits_of_l (pget_trail S)› ‹remove1_mset L C›] distinct_consistent_interp[OF n_d] by (cases S; auto 4 3 simp: entailed_clss_inv_def cdcl_W_restart_mset_state clauses0_inv_def true_annots_true_cls tautology_add_mset dest!: multi_member_split dest: no_dup_consistentD in_lits_of_l_defined_litD; fail)+ have p0: ‹pclauses0 S = {#}› using clss0 conf by (cases S; auto 4 3 simp: entailed_clss_inv_def cdcl_W_restart_mset_state clauses0_inv_def true_annots_true_cls dest!: multi_member_split dest: no_dup_consistentD) have tauto: ‹¬ tautology (remove1_mset L C)› using confl conf n_d ent consistent_CNot_not_tautology[of ‹lits_of_l (pget_trail S)› ‹remove1_mset L C›, OF distinct_consistent_interp] by (cases S) (auto simp: true_annots_true_cls entailed_clss_inv_def insert_subset_eq_iff dest: distinct_consistent_interp mset_subset_eqD no_dup_consistentD dest!: multi_member_split) have ‹(∃C' ∈# pget_clauses S. trail (state_of S) ⊨as CNot C') ∨ (∃C' ∈# pget_clauses S. L ∈# C' ∧ trail (state_of S) ⊨as CNot (remove1_mset L C'))› if C: ‹C ∈# psubsumed_clauses S› proof - have ‹¬tautology C› using confl undef tauto apply (auto simp: tautology_decomp' add_mset_eq_add_mset remove1_mset_add_mset_If dest!: multi_member_split dest: in_lits_of_l_defined_litD split: ) apply (case_tac ‹L = -La›) apply (auto dest: in_lits_of_l_defined_litD)[] apply (subst (asm) remove1_mset_add_mset_If) apply (case_tac ‹L = La›) apply (auto dest: in_lits_of_l_defined_litD)[] apply (auto dest: in_lits_of_l_defined_litD)[] done then consider C' where ‹C' ⊆# C› ‹C' ∈# pget_clauses S› | C' where ‹C' ⊆# C› ‹C' ∈# punit_clauses S› using sub C p0 by (cases S) (auto simp: psubsumed_invs_def dest!: multi_member_split) then show ?thesis proof cases case 2 then show ?thesis using ent confl undef conf n_d apply (cases S) apply (cases ‹L ∈# C'›) apply (auto simp: psubsumed_invs_def true_annots_true_cls entailed_clss_inv_def insert_subset_eq_iff remove1_mset_add_mset_If dest: distinct_consistent_interp mset_subset_eqD no_dup_consistentD dest!: multi_member_split) apply (auto simp add: mset_subset_eqD add_mset_eq_add_mset subset_mset.le_iff_add true_clss_def_iff_negation_in_model tautology_decomp' insert_subset_eq_iff dest: no_dup_consistentD in_lits_of_l_defined_litD dest!: multi_member_split[of _ C] split: if_splits) done next case 1 then show ?thesis using tauto confl undef conf n_d apply (cases S) apply (cases ‹L ∈# C'›) apply (auto simp: psubsumed_invs_def true_annots_true_cls entailed_clss_inv_def insert_subset_eq_iff dest: distinct_consistent_interp mset_subset_eqD no_dup_consistentD dest!: multi_member_split) apply (auto simp add: mset_subset_eqD add_mset_eq_add_mset true_clss_def_iff_negation_in_model tautology_decomp' insert_subset_eq_iff dest: no_dup_consistentD dest!: multi_member_split[of _ C] intro!: bexI[of _ C']) by (metis (no_types, opaque_lifting) in_multiset_minus_notin_snd insert_DiffM member_add_mset mset_subset_eqD multi_self_add_other_not_self zero_diff)+ qed qed then show ?thesis using C confl conf ‹C ∉# punit_clauses S› ‹C ∉# pclauses0 S› undef LC by (cases S) (auto simp: cdcl_propagate.simps clauses_def cdcl_conflict.simps intro!: exI[of _ L] intro: exI[of _ C]) qed lemma pcdcl_core_is_cdcl: ‹pcdcl_core S T ⟹ cdcl_W_restart_mset.cdcl_W (state_of S) (state_of T)› by (induction rule: pcdcl_core.induct) (blast intro: cdcl_W_restart_mset.cdcl_W.intros cdcl_conflict_is_conflict cdcl_propagate_is_propagate cdcl_propagate_is_propagate cdcl_decide_is_decide cdcl_propagate_is_propagate cdcl_W_restart_mset.cdcl_W_o.intros cdcl_skip_is_skip cdcl_resolve_is_resolve cdcl_backtrack_is_backtrack cdcl_W_restart_mset.cdcl_W_bj.intros)+ lemma rtranclp_pcdcl_core_is_cdcl: ‹pcdcl_core^*^* S T ⟹ cdcl_W_restart_mset.cdcl_W^*^* (state_of S) (state_of T)› by (induction rule: rtranclp_induct) (auto dest: pcdcl_core_is_cdcl) lemma pcdcl_core_stgy_is_cdcl_stgy: assumes confl: ‹pcdcl_core_stgy S T› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› and clss0: ‹clauses0_inv S› shows ‹cdcl_W_restart_mset.cdcl_W_stgy (state_of S) (state_of T)› using assms by (induction rule: pcdcl_core_stgy.induct) ((blast intro: cdcl_W_restart_mset.cdcl_W_stgy.intros cdcl_conflict_is_conflict cdcl_propagate_is_propagate cdcl_decide_is_decide cdcl_skip_is_skip cdcl_backtrack_is_backtrack cdcl_resolve_is_resolve cdcl_W_restart_mset.resolve cdcl_W_restart_mset.cdcl_W_bj_cdcl_W_stgy dest: conflict_is_cdcl_conflictD propagate_is_cdcl_propagateD)+)[6] lemma no_step_pcdcl_core_stgy_is_cdcl_stgy: assumes confl: ‹no_step pcdcl_core_stgy S› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and clss0: ‹clauses0_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› shows ‹no_step cdcl_W_restart_mset.cdcl_W_stgy (state_of S)› using assms apply - apply (rule ccontr) unfolding not_all not_not apply normalize_goal+ apply (cases rule: cdcl_W_restart_mset.cdcl_W_stgy.cases, assumption) using conflict_is_cdcl_conflictD pcdcl_core_stgy.intros(1) apply blast using pcdcl_core_stgy.intros(1) pcdcl_core_stgy.intros(2) propagate_is_cdcl_propagateD apply blast apply (cases rule: cdcl_W_restart_mset.cdcl_W_o.cases, assumption) using cdcl_conflict_is_conflict cdcl_propagate_is_propagate decide_is_cdcl_decide pcdcl_core_stgy.intros(3) apply blast apply (cases rule: cdcl_W_restart_mset.cdcl_W_bj.cases, assumption) apply (blast dest: resolve_is_cdcl_resolve backtrack_is_cdcl_backtrack pcdcl_core_stgy.intros skip_is_cdcl_skip)+ done lemma cdcl_resolution_psubsumed_invs: ‹cdcl_resolution S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› by (cases rule:cdcl_resolution.cases, assumption) (auto simp: psubsumed_invs_def) lemma cdcl_resolution_entailed_clss_inv: ‹cdcl_resolution S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› by (cases rule:cdcl_resolution.cases, assumption) (auto simp: entailed_clss_inv_def) lemma cdcl_pure_literal_remove_psubsumed_invs: ‹cdcl_pure_literal_remove S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› by (cases rule:cdcl_pure_literal_remove.cases, assumption) (auto simp: psubsumed_invs_def) lemma cdcl_pure_literal_remove_entailed_clss_inv: ‹cdcl_pure_literal_remove S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› by (cases rule:cdcl_pure_literal_remove.cases, assumption) (auto simp: entailed_clss_inv_def get_level_cons_if) lemma cdcl_subsumed_psubsumed_invs: ‹cdcl_subsumed S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› by (cases rule:cdcl_subsumed.cases, assumption) (auto simp: psubsumed_invs_def) lemma cdcl_subsumed_entailed_clss_inv: ‹cdcl_subsumed S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› by (cases rule:cdcl_subsumed.cases, assumption) (auto simp: entailed_clss_inv_def) lemma cdcl_learn_clause_psubsumed_invs: ‹cdcl_learn_clause S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› by (cases rule:cdcl_learn_clause.cases, assumption) (auto simp: psubsumed_invs_def) lemma cdcl_learn_clause_entailed_clss_inv: ‹cdcl_learn_clause S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› by (cases rule:cdcl_learn_clause.cases, assumption) (auto simp: entailed_clss_inv_def) lemma cdcl_learn_clause_all_struct_inv: assumes ‹cdcl_learn_clause S T› and ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of T)› using assms by (induction rule: cdcl_learn_clause.induct) (auto 8 3 simp: cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.no_strange_atm_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.cdcl_W_learned_clause_def cdcl_W_restart_mset.clauses_def cdcl_W_restart_mset.reasons_in_clauses_def intro: all_decomposition_implies_mono) lemma cdcl_subsumed_all_struct_inv: assumes ‹cdcl_subsumed S T› and ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of T)› using assms apply (induction rule: cdcl_subsumed.induct) subgoal for C C' by (auto simp: cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.no_strange_atm_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.cdcl_W_learned_clause_def cdcl_W_restart_mset.clauses_def cdcl_W_restart_mset.reasons_in_clauses_def insert_commute[of C C'] intro: all_decomposition_implies_mono) subgoal for C C' by (auto simp: cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.no_strange_atm_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.cdcl_W_learned_clause_def cdcl_W_restart_mset.clauses_def cdcl_W_restart_mset.reasons_in_clauses_def insert_commute[of C C'] intro: all_decomposition_implies_mono) subgoal for C C' by (auto simp: cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.no_strange_atm_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.cdcl_W_learned_clause_def cdcl_W_restart_mset.clauses_def cdcl_W_restart_mset.reasons_in_clauses_def insert_commute[of C C'] intro: all_decomposition_implies_mono) done lemma all_decomposition_implies_monoI: ‹all_decomposition_implies N M ⟹ N ⊆ N' ⟹ all_decomposition_implies N' M› by (metis all_decomposition_implies_union le_iff_sup) lemma cdcl_resolution_all_struct_inv: assumes ‹cdcl_resolution S T› and ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of T)› using assms apply (induction rule: cdcl_resolution.induct) subgoal for M N L C C' U D NE UE NS US by (auto simp: cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.no_strange_atm_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.cdcl_W_learned_clause_def cdcl_W_restart_mset.clauses_def cdcl_W_restart_mset.reasons_in_clauses_def insert_commute[of _ ‹remdups_mset (C + C')›] intro: all_decomposition_implies_monoI) subgoal for M C C' N U L D NE UE NS US by (auto simp: cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.no_strange_atm_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.cdcl_W_learned_clause_def cdcl_W_restart_mset.clauses_def cdcl_W_restart_mset.reasons_in_clauses_def insert_commute[of _ ‹remdups_mset (C + C')›] intro: all_decomposition_implies_monoI) subgoal for M C C' N L U D NE UE NS US by (auto simp: cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.no_strange_atm_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.cdcl_W_learned_clause_def cdcl_W_restart_mset.clauses_def cdcl_W_restart_mset.reasons_in_clauses_def insert_commute[of _ ‹remdups_mset (C + C')›] intro: all_decomposition_implies_monoI) done lemma cdcl_pure_literal_remove_all_struct_inv: assumes ‹cdcl_pure_literal_remove S T› and ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of T)› using assms proof (induction rule: cdcl_pure_literal_remove.induct) case (cdcl_pure_literal_remove L N NE NS N0 M U UE US U0) note IH = this(1-4) and all = this(5) let ?S = ‹state_of (M, N, U, None, NE, UE, NS, US, N0, U0)› let ?T = ‹state_of (Propagated L {#L#} # M, N, U, None, add_mset {#L#} NE, UE, NS, US, N0, U0)› have 1: ‹cdcl_W_restart_mset.no_strange_atm ?S› and 2: ‹cdcl_W_restart_mset.cdcl_W_M_level_inv ?S› and 3: ‹(∀s∈#learned_clss ?S. ¬ tautology s)› and 4: ‹cdcl_W_restart_mset.distinct_cdcl_W_state ?S› and 5: ‹cdcl_W_restart_mset.cdcl_W_conflicting ?S› and 6: ‹all_decomposition_implies_m (cdcl_W_restart_mset.clauses ?S) (get_all_ann_decomposition (trail ?S))› and 7: ‹cdcl_W_restart_mset.cdcl_W_learned_clause ?S› using all unfolding cdcl_W_restart_mset.cdcl_W_all_struct_inv_def by fast+ have 1: ‹cdcl_W_restart_mset.no_strange_atm ?T› using 1 by (auto simp: cdcl_W_restart_mset.no_strange_atm_def) moreover have 2: ‹cdcl_W_restart_mset.cdcl_W_M_level_inv ?T› using 2 IH by (auto simp: cdcl_W_restart_mset.cdcl_W_M_level_inv_def) moreover have 3: ‹(∀s∈#learned_clss ?T. ¬ tautology s)› using 3 by auto moreover have 4: ‹cdcl_W_restart_mset.distinct_cdcl_W_state ?T› using 4 by (auto simp: cdcl_W_restart_mset.distinct_cdcl_W_state_def) moreover have 5: ‹cdcl_W_restart_mset.cdcl_W_conflicting ?T› using 5 unfolding cdcl_W_restart_mset.cdcl_W_conflicting_def by (auto simp add: cdcl_W_restart_mset.cdcl_W_conflicting_def Cons_eq_append_conv eq_commute[of "_ @ _" "_ # _"]) moreover { have ‹all_decomposition_implies_m (cdcl_W_restart_mset.clauses ?T) (get_all_ann_decomposition (trail ?S))› by (rule all_decomposition_implies_monoI[OF 6, of ‹set_mset (cdcl_W_restart_mset.clauses ?T)›]) (auto simp: clauses_def) then have 6: ‹all_decomposition_implies_m (cdcl_W_restart_mset.clauses ?T) (get_all_ann_decomposition (trail ?T))› apply - by (use IH in ‹auto intro: simp: no_decision_get_all_ann_decomposition clauses_def count_decided_0_iff›) } moreover have 7: ‹cdcl_W_restart_mset.cdcl_W_learned_clause ?T› using 7 by (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clause_def cdcl_W_restart_mset.reasons_in_clauses_def clauses_def) ultimately show ?case unfolding cdcl_W_restart_mset.cdcl_W_all_struct_inv_def by fast qed lemma cdcl_flush_unit_unchanged: ‹cdcl_flush_unit S T ⟹ state_of S = state_of T› by (auto simp: cdcl_flush_unit.simps) lemma cdcl_inp_conflict_all_struct_inv: ‹cdcl_inp_conflict S T ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S) ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of T)› by (auto 4 4 simp: cdcl_inp_conflict.simps cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.no_strange_atm_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.cdcl_W_learned_clause_def cdcl_W_restart_mset.clauses_def cdcl_W_restart_mset.reasons_in_clauses_def) lemma cdcl_inp_propagate_is_propagate: ‹cdcl_inp_propagate S T ⟹ cdcl_W_restart_mset.propagate (state_of S) (state_of T)› by (force simp: cdcl_inp_propagate.simps cdcl_W_restart_mset.propagate.simps clauses_def) lemma cdcl_inp_propagate_all_struct_inv: ‹cdcl_inp_propagate S T ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S) ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of T)› using cdcl_W_restart_mset.cdcl_W_stgy.propagate' cdcl_W_restart_mset.cdcl_W_stgy_cdcl_W_all_struct_inv by (blast dest!: cdcl_inp_propagate_is_propagate) lemma cdcl_unitres_true_same: ‹cdcl_unitres_true S T ⟹ state_of S = state_of T› by (induction rule: cdcl_unitres_true.induct) auto lemma cdcl_promote_false_all_struct_inv: ‹cdcl_promote_false S T ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S) ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of T)› by (auto 4 4 simp: cdcl_promote_false.simps cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.no_strange_atm_def cdcl_W_restart_mset.cdcl_W_M_level_inv_def cdcl_W_restart_mset.distinct_cdcl_W_state_def cdcl_W_restart_mset.cdcl_W_conflicting_def cdcl_W_restart_mset.cdcl_W_learned_clause_def cdcl_W_restart_mset.reasons_in_clauses_def cdcl_W_restart_mset.clauses_def) lemma pcdcl_all_struct_inv: ‹pcdcl S T ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S) ⟹ cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of T)› by (induction rule: pcdcl.induct) (blast intro: cdcl_resolution_all_struct_inv cdcl_subsumed_all_struct_inv cdcl_learn_clause_all_struct_inv cdcl_W_restart_mset.cdcl_W_all_struct_inv_inv cdcl_inp_conflict_all_struct_inv cdcl_inp_propagate_all_struct_inv cdcl_pure_literal_remove_all_struct_inv dest!: cdcl_unitres_true_same[THEN arg_cong[of _ _ cdcl_W_restart_mset.cdcl_W_all_struct_inv], THEN iffD1] cdcl_promote_false_all_struct_inv pcdcl_core_is_cdcl subst[OF cdcl_flush_unit_unchanged] cdcl_W_restart_mset.cdcl_W_cdcl_W_restart)+ lemma cdcl_unitres_true_entailed_clss_inv: ‹cdcl_unitres_true S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› by (induction rule: cdcl_unitres_true.induct) (auto simp: entailed_clss_inv_def) lemma cdcl_unitres_true_psubsumed_invs: ‹cdcl_unitres_true S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› by (induction rule: cdcl_unitres_true.induct) (auto simp: psubsumed_invs_def) definition pcdcl_all_struct_invs :: ‹_› where ‹pcdcl_all_struct_invs S ⟷ cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S) ∧ entailed_clss_inv S ∧ psubsumed_invs S ∧ clauses0_inv S› lemma entailed_clss_inv_Propagated: assumes ‹entailed_clss_inv (M, N, U, None, NE, UE, NS, US)› and undef: ‹undefined_lit M L'› shows ‹entailed_clss_inv (Propagated L' D # M, N, U, None, NE, UE, NS, US)› unfolding entailed_clss_inv_def proof (intro conjI impI ballI) fix C assume ‹C ∈# NE + UE› then obtain L where LC: ‹L ∈# C› and dec: ‹get_level M L = 0 ∧ L ∈ lits_of_l M› using assms by (auto simp: entailed_clss_inv_def get_level_cons_if atm_of_eq_atm_of dest!: multi_member_split[of C] split: if_splits) show ‹∃L. L ∈# C ∧ (None = None ∨ 0 < count_decided (Propagated L' D # M) ⟶ get_level (Propagated L' D # M) L = 0 ∧ L ∈ lits_of_l (Propagated L' D # M))› apply (rule exI[of _ L]) apply (cases ‹count_decided M = 0›) using count_decided_ge_get_level[of M] using LC dec undef by (auto simp: entailed_clss_inv_def get_level_cons_if atm_of_eq_atm_of split: if_splits dest: in_lits_of_l_defined_litD) qed lemma entailed_clss_inv_skip: assumes ‹entailed_clss_inv (Propagated L' D'' # M, N, U, Some D, NE, UE, NS, US)› shows ‹entailed_clss_inv (M, N, U, Some D', NE, UE, NS, US)› using assms unfolding entailed_clss_inv_def by (auto 7 3 simp: get_level_cons_if atm_of_eq_atm_of dest!: multi_member_split[of _ NE] multi_member_split[of _ UE] dest: multi_member_split split: if_splits) lemma entailed_clss_inv_ConflictD: ‹entailed_clss_inv (M, N, U, None, NE, UE, NS, US) ⟹ entailed_clss_inv (M, N, U, Some D, NE, UE, NS, US)› by (auto simp: entailed_clss_inv_def) lemma entailed_clss_inv_Decided: assumes ‹entailed_clss_inv (M, N, U, None, NE, UE, NS, US)› and undef: ‹undefined_lit M L'› shows ‹entailed_clss_inv (Decided L' # M, N, U, None, NE, UE, NS, US)› using assms unfolding entailed_clss_inv_def by (auto 7 3 simp: entailed_clss_inv_def get_level_cons_if atm_of_eq_atm_of split: if_splits dest: in_lits_of_l_defined_litD dest!: multi_member_split[of _ ‹NE›] multi_member_split[of _ ‹UE›]) lemma get_all_ann_decomposition_lvl0_still: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M) ⟹ L ∈ lits_of_l M ⟹ get_level M L = 0 ⟹ L ∈ lits_of_l M1 ∧ get_level M1 L = 0› by (auto dest!: get_all_ann_decomposition_exists_prepend simp: get_level_append_if get_level_cons_if split: if_splits dest: in_lits_of_l_defined_litD) lemma cdcl_backtrack_entailed_clss_inv: ‹cdcl_backtrack S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› for S T :: ‹'v prag_st› apply (induction rule: cdcl_backtrack.induct) subgoal for K M1 M2 M L D' i D N U NE UE NS US unfolding entailed_clss_inv_def apply (clarsimp simp only: Set.ball_simps set_mset_add_mset_insert dest!: multi_member_split) apply (rename_tac C A La Aa, rule_tac x=La in exI) using get_all_ann_decomposition_lvl0_still[of K M1 M2 M] by (auto simp: cdcl_backtrack.simps entailed_clss_inv_def get_level_cons_if atm_of_eq_atm_of split: if_splits dest: in_lits_of_l_defined_litD) done lemma pcdcl_core_entails_clss_inv: ‹pcdcl_core S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› by (induction rule: pcdcl_core.induct) (auto simp: cdcl_conflict.simps cdcl_propagate.simps cdcl_decide.simps cdcl_skip.simps cdcl_resolve.simps get_level_cons_if atm_of_eq_atm_of entailed_clss_inv_Propagated entailed_clss_inv_ConflictD entailed_clss_inv_Decided intro: entailed_clss_inv_skip cdcl_backtrack_entailed_clss_inv split: if_splits) lemma pcdcl_core_clauses0_inv: ‹pcdcl_core S T ⟹ clauses0_inv S ⟹ clauses0_inv T› by (auto simp: clauses0_inv_def pcdcl_core.simps cdcl_conflict.simps cdcl_propagate.simps cdcl_decide.simps cdcl_backtrack.simps cdcl_skip.simps cdcl_resolve.simps) lemma cdcl_flush_unit_invs: ‹cdcl_flush_unit S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› ‹cdcl_flush_unit S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› ‹cdcl_flush_unit S T ⟹ cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of S) ⟹ cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of T)› ‹cdcl_flush_unit S T ⟹ clauses0_inv S ⟹ clauses0_inv T› by (auto simp: cdcl_flush_unit.simps psubsumed_invs_def entailed_clss_inv_def clauses0_inv_def dest!: multi_member_split dest: cdcl_flush_unit_unchanged) lemma cdcl_inp_propagate_invs: ‹cdcl_inp_propagate S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› ‹cdcl_inp_propagate S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› ‹cdcl_inp_propagate S T ⟹ clauses0_inv S ⟹ clauses0_inv T› using count_decided_ge_get_level[of ‹pget_trail S›] by (auto 5 5 simp: cdcl_inp_propagate.simps entailed_clss_inv_def clauses0_inv_def get_level_cons_if psubsumed_invs_def) lemma cdcl_inp_conflict_invs: ‹cdcl_inp_conflict S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› ‹cdcl_inp_conflict S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› ‹cdcl_inp_conflict S T ⟹ clauses0_inv S ⟹ clauses0_inv T› using count_decided_ge_get_level[of ‹pget_trail S›] by (auto 5 5 simp: cdcl_inp_conflict.simps entailed_clss_inv_def psubsumed_invs_def get_level_cons_if clauses0_inv_def) lemma cdcl_promote_false_invs: ‹cdcl_promote_false S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› ‹cdcl_promote_false S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› ‹cdcl_promote_false S T ⟹ clauses0_inv S ⟹ clauses0_inv T› using count_decided_ge_get_level[of ‹pget_trail S›] by (auto 4 4 simp: cdcl_promote_false.simps entailed_clss_inv_def psubsumed_invs_def get_level_cons_if clauses0_inv_def dest!: multi_member_split) lemma pcdcl_entails_clss_inv: ‹pcdcl S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› by (induction rule: pcdcl.induct) (simp_all add: pcdcl_core_entails_clss_inv cdcl_learn_clause_entailed_clss_inv cdcl_resolution_entailed_clss_inv cdcl_subsumed_entailed_clss_inv cdcl_pure_literal_remove_entailed_clss_inv cdcl_flush_unit_invs cdcl_inp_propagate_invs cdcl_inp_conflict_invs cdcl_unitres_true_entailed_clss_inv cdcl_promote_false_invs) lemma rtranclp_pcdcl_entails_clss_inv: ‹pcdcl^*^* S T ⟹ entailed_clss_inv S ⟹ entailed_clss_inv T› by (induction rule: rtranclp_induct) (simp_all add: pcdcl_entails_clss_inv) lemma pcdcl_core_psubsumed_invs: ‹pcdcl_core S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› by (induction rule: pcdcl_core.induct) (auto simp: cdcl_conflict.simps cdcl_backtrack.simps cdcl_propagate.simps cdcl_decide.simps cdcl_pure_literal_remove.simps cdcl_skip.simps cdcl_resolve.simps get_level_cons_if atm_of_eq_atm_of psubsumed_invs_def) lemma pcdcl_psubsumed_invs: ‹pcdcl S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› by (induction rule: pcdcl.induct) (simp_all add: pcdcl_core_psubsumed_invs cdcl_learn_clause_psubsumed_invs cdcl_resolution_psubsumed_invs cdcl_subsumed_psubsumed_invs cdcl_flush_unit_invs cdcl_pure_literal_remove_psubsumed_invs cdcl_inp_propagate_invs cdcl_inp_conflict_invs cdcl_promote_false_invs cdcl_unitres_true_psubsumed_invs) lemma rtranclp_pcdcl_psubsumed_invs: ‹pcdcl^*^* S T ⟹ psubsumed_invs S ⟹ psubsumed_invs T› by (induction rule: rtranclp_induct) (simp_all add: pcdcl_psubsumed_invs) lemma pcdcl_clauses0_inv: ‹pcdcl S T ⟹ clauses0_inv S ⟹ clauses0_inv T› by (induction rule: pcdcl.induct) (auto simp add: pcdcl_core_psubsumed_invs cdcl_learn_clause_psubsumed_invs cdcl_resolution_psubsumed_invs cdcl_subsumed_psubsumed_invs cdcl_flush_unit_invs cdcl_pure_literal_remove_psubsumed_invs cdcl_pure_literal_remove.simps cdcl_inp_propagate_invs cdcl_inp_conflict_invs pcdcl_core_clauses0_inv cdcl_learn_clause.simps clauses0_inv_def cdcl_resolution.simps cdcl_subsumed.simps cdcl_unitres_true.simps cdcl_promote_false.simps) lemma rtranclp_pcdcl_clauses0_inv: ‹pcdcl^*^* S T ⟹ clauses0_inv S ⟹ clauses0_inv T› by (induction rule: rtranclp_induct) (simp_all add: pcdcl_clauses0_inv) lemma rtranclp_pcdcl_core_stgy_pcdcl: ‹pcdcl_core_stgy^*^* S T ⟹ pcdcl^*^* S T› apply (induction rule: rtranclp_induct) apply (simp add: pcdcl_core_stgy_pcdcl) by (metis (no_types, opaque_lifting) converse_rtranclp_into_rtranclp pcdcl.intros(1) pcdcl_core_stgy_pcdcl r_into_rtranclp rtranclp_idemp) lemma rtranclp_pcdcl_core_stgy_is_cdcl_stgy: assumes confl: ‹pcdcl_core_stgy^*^* S T› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› and ‹clauses0_inv S› shows ‹cdcl_W_restart_mset.cdcl_W_stgy^*^* (state_of S) (state_of T)› using assms apply (induction rule: rtranclp_induct) subgoal by auto subgoal for T U using rtranclp_pcdcl_psubsumed_invs[of S T] rtranclp_pcdcl_core_stgy_pcdcl[of S T] rtranclp_pcdcl_entails_clss_inv[of S T] pcdcl_core_stgy_is_cdcl_stgy[of T U] rtranclp_pcdcl_clauses0_inv[of S T] by (auto simp add: cdcl_W_restart_mset.rtranclp_cdcl_W_stgy_cdcl_W_all_struct_inv) done lemma pcdcl_all_struct_invs: ‹pcdcl S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T› unfolding pcdcl_all_struct_invs_def by (intro conjI) (simp_all add: pcdcl_all_struct_inv pcdcl_entails_clss_inv pcdcl_psubsumed_invs pcdcl_clauses0_inv) lemma rtranclp_pcdcl_all_struct_invs: ‹pcdcl^*^* S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T› by (induction rule: rtranclp_induct) (auto simp: pcdcl_all_struct_invs) lemma cdcl_resolution_entailed_by_init: assumes ‹cdcl_resolution S T› and ‹pcdcl_all_struct_invs S› and ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of T)› using assms apply (induction rule: cdcl_resolution.induct) apply (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def) apply (metis (full_types) insert_commute true_clss_clss_insert_l) apply (metis (full_types) insert_commute true_clss_clss_insert_l) apply (metis (full_types) insert_commute true_clss_clss_insert_l) apply (metis (full_types) insert_commute true_clss_clss_insert_l) apply (metis add.commute true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or) by (metis Partial_Herbrand_Interpretation.uminus_lit_swap member_add_mset set_mset_add_mset_insert set_mset_union true_clss_cls_in true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or) lemma cdcl_pure_literal_remove_entailed_by_init: assumes ‹cdcl_pure_literal_remove S T› and ‹pcdcl_all_struct_invs S› and ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of T)› using assms by (induction rule: cdcl_pure_literal_remove.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def) lemma cdcl_subsumed_entailed_by_init: assumes ‹cdcl_subsumed S T› and ‹pcdcl_all_struct_invs S› and ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of T)› using assms by (induction rule: cdcl_subsumed.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def insert_commute) lemma cdcl_learn_clause_entailed_by_init: assumes ‹cdcl_learn_clause S T› and ‹pcdcl_all_struct_invs S› and ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of T)› using assms by (induction rule: cdcl_learn_clause.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def insert_commute) lemma cdcl_inp_propagate_entailed_by_init: assumes ‹cdcl_inp_propagate S T› and ‹pcdcl_all_struct_invs S› and ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of T)› using assms by (induction rule: cdcl_inp_propagate.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def insert_commute) lemma cdcl_inp_conflict_entailed_by_init: assumes ‹cdcl_inp_conflict S T› and ‹pcdcl_all_struct_invs S› and ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of T)› using assms by (induction rule: cdcl_inp_conflict.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def insert_commute) lemma cdcl_promote_false_entailed_by_init: assumes ‹cdcl_promote_false S T› and ‹pcdcl_all_struct_invs S› and ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of T)› using assms by (induction rule: cdcl_promote_false.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def insert_commute) lemma pcdcl_entailed_by_init: assumes ‹pcdcl S T› and ‹pcdcl_all_struct_invs S› and ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of T)› using assms apply (induction rule: pcdcl.induct) apply (meson cdcl_W_restart_mset.cdcl_W_all_struct_inv_def cdcl_W_restart_mset.cdcl_W_cdcl_W_restart cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed pcdcl_all_struct_invs_def pcdcl_core_is_cdcl) by (simp_all add: cdcl_learn_clause_entailed_by_init cdcl_subsumed_entailed_by_init cdcl_resolution_entailed_by_init cdcl_flush_unit_unchanged cdcl_pure_literal_remove_entailed_by_init cdcl_inp_conflict_entailed_by_init cdcl_inp_propagate_entailed_by_init cdcl_unitres_true_same cdcl_promote_false_entailed_by_init) lemma rtranclp_pcdcl_entailed_by_init: assumes ‹pcdcl^*^* S T› and ‹pcdcl_all_struct_invs S› and ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of T)› using assms by (induction rule: rtranclp_induct) (use pcdcl_entailed_by_init rtranclp_pcdcl_all_struct_invs in blast)+ lemma pcdcl_core_stgy_stgy_invs: assumes confl: ‹pcdcl_core_stgy S T› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› and ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of S)› and clss0: ‹clauses0_inv S› shows ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of T)› using assms by (meson cdcl_W_restart_mset.cdcl_W_stgy_cdcl_W_stgy_invariant pcdcl_core_stgy_is_cdcl_stgy) lemma cdcl_subsumed_stgy_stgy_invs: assumes confl: ‹cdcl_subsumed S T› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› and ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of T)› using assms by (induction rule: cdcl_subsumed.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_stgy_invariant_def cdcl_W_restart_mset.no_smaller_confl_def cdcl_W_restart_mset.clauses_def) lemma cdcl_resolution_stgy_stgy_invs: assumes confl: ‹cdcl_resolution S T› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› and ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of T)› using assms by (induction rule: cdcl_resolution.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_stgy_invariant_def cdcl_W_restart_mset.no_smaller_confl_def cdcl_W_restart_mset.clauses_def) lemma cdcl_pure_literal_remove_stgy_stgy_invs: assumes confl: ‹cdcl_pure_literal_remove S T› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› and ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of T)› using assms by (induction rule: cdcl_pure_literal_remove.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_stgy_invariant_def get_level_cons_if Cons_eq_append_conv cdcl_W_restart_mset.no_smaller_confl_def cdcl_W_restart_mset.clauses_def) lemma cdcl_learn_clause_stgy_stgy_invs: assumes confl: ‹cdcl_learn_clause S T› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› and ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of S)› shows ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of T)› using assms by (induction rule: cdcl_learn_clause.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_stgy_invariant_def cdcl_W_restart_mset.no_smaller_confl_def cdcl_W_restart_mset.clauses_def) lemma cdcl_inp_conflict_stgy_stgy_invs: assumes confl: ‹cdcl_inp_conflict S T› shows ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of T)› using assms by (induction rule: cdcl_inp_conflict.induct) (auto simp: cdcl_W_restart_mset.cdcl_W_stgy_invariant_def cdcl_W_restart_mset.no_smaller_confl_def cdcl_W_restart_mset.clauses_def) lemma pcdcl_stgy_stgy_invs: assumes confl: ‹pcdcl_stgy S T› and sub: ‹psubsumed_invs S› and ent: ‹entailed_clss_inv S› and invs: ‹cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S)› and ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of S)› and clss0: ‹clauses0_inv S› shows ‹cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of T)› using assms apply (induction rule: pcdcl_stgy.induct) subgoal using pcdcl_core_stgy_stgy_invs by blast subgoal using cdcl_learn_clause_stgy_stgy_invs by blast subgoal using cdcl_resolution_stgy_stgy_invs by blast subgoal using cdcl_subsumed_stgy_stgy_invs by blast subgoal by (simp add: cdcl_flush_unit_unchanged) subgoal using cdcl_W_restart_mset.cdcl_W_stgy.propagate' cdcl_W_restart_mset.cdcl_W_stgy_cdcl_W_stgy_invariant cdcl_inp_propagate_is_propagate by blast subgoal by (simp add: cdcl_inp_conflict_stgy_stgy_invs) subgoal by (simp add: cdcl_unitres_true_same) done section ‹Higher-level rules› subsection ‹Simplify unit clauses› text ‹ Initially, I wanted to remove the literals one at a time, but this has two disadvantages: ▪ more subsumed clauses are generated. ▪ it makes it possible to remove all literals making it much easier to express that the clause is correctly watched in the next refinement step. Undefined literals are correctly watched. Mixed situation are strange (we could watch two false clauses during the simplification only). As we only make the rule strictly more powerful and that the proof is not different, I changed the rule instead of doing any other solution. › inductive cdcl_unitres :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where cdcl_unitresI: ‹cdcl_unitres (M, N + {#C+C'#}, U, None, NE, UE, NS, US, N0, U0) (M, N + {#C#}, U, None, NE, UE, add_mset (C+C') NS, US, N0, U0)› if ‹count_decided M = 0› and ‹add_mset (C+C') (N + NE + NS + N0) ⊨psm mset_set (CNot C')› ‹¬tautology C› ‹distinct_mset C› | cdcl_unitresI_unit: ‹cdcl_unitres (M, N + {#C+C'#}, U, None, NE, UE, NS, US, N0, U0) (Propagated K C # M, N, U, None, NE + {#C#}, UE, add_mset (C+C') NS, US, N0, U0)› if ‹count_decided M = 0› and ‹add_mset (C+C') (N + NE + NS + N0) ⊨psm mset_set (CNot C')› ‹¬tautology C› ‹distinct_mset C› ‹C = {#K#}› ‹undefined_lit M K› | cdcl_unitresR: ‹cdcl_unitres (M, N, U + {#C+C'#}, None, NE, UE, NS, US, N0, U0) (M, N, U + {#C#}, None, NE, UE, NS, add_mset (C+C') US, N0, U0)› if ‹count_decided M = 0› and ‹(N + NE + NS + N0) ⊨psm mset_set (CNot C')› ‹¬tautology C› ‹distinct_mset C› ‹atms_of C ⊆ atms_of_mm (N+NE+NS+N0)›| cdcl_unitresR_unit: ‹cdcl_unitres (M, N, U + {#C+C'#}, None, NE, UE, NS, US, N0, U0) (Propagated K C # M, N, U, None, NE, UE + {#C#}, NS, add_mset (C+C') US, N0, U0)› if ‹count_decided M = 0› and ‹(N + NE + NS + N0) ⊨psm mset_set (CNot C')› ‹¬tautology C› ‹distinct_mset C› ‹atms_of C ⊆ atms_of_mm (N+NE+NS+N0)› ‹C = {#K#}› ‹undefined_lit M K› | cdcl_unitresR_empty: ‹cdcl_unitres (M, N, U + {#C'#}, None, NE, UE, NS, US, N0, U0) (M, N, U, Some {#}, NE, UE, NS, add_mset (C') US, N0, add_mset {#} U0)› if ‹count_decided M = 0› and ‹(N + NE + NS + N0) ⊨psm mset_set (CNot C')› | cdcl_unitresI_empty: ‹cdcl_unitres (M, N + {#C'#}, U, None, NE, UE, NS, US, N0, U0) (M, N, U, Some {#}, NE, UE, add_mset (C') NS, US, add_mset {#} N0, U0)› if ‹count_decided M = 0› and ‹(add_mset C' N + NE + NS + N0) ⊨psm mset_set (CNot C')› lemma true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or_generalise': ‹N ⊨ps CNot C' ⟹ N ⊨p C + C' ⟹ C'' ⊆# C' ⟹ N ⊨p (C + (C' - C''))› apply (induction C'') subgoal by auto subgoal for x C'' using true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[of ‹N› ‹x› ‹{#}› ‹C + (C' - add_mset x C'')›] apply (auto dest!: mset_subset_eq_insertD dest!: multi_member_split) by (smt Multiset.diff_right_commute add_mset_remove_trivial add_mset_remove_trivial_eq diff_single_trivial) done lemmas true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or_generalise = true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or_generalise'[of N C' C C' for C C' N, simplified] lemma cdcl_unitres_learn_subsumeE: assumes ‹cdcl_unitres S X› ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› obtains T U V W where ‹cdcl_learn_clause S T› ‹cdcl_subsumed T U› ‹cdcl_propagate^*^* U V› ‹cdcl_flush_unit^*^* V W› ‹cdcl_promote_false^*^* W X› subgoal premises noone_wants_that_premise using assms apply (cases rule: cdcl_unitres.cases) subgoal for M C C' N NE NS N0 U UE US U0 by (rule that[of ‹(M, N + {#C+C', C#}, U, None, NE, UE, NS, US, N0, U0)› X X]) (auto simp: cdcl_learn_clause.simps cdcl_subsumed.simps dest!: true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or_generalise) subgoal for M C C' N NE NS N0 K U UE US U0 by (rule that[of ‹(M, N + {#C+C', C#}, U, None, NE, UE, NS, US, N0, U0)› ‹(M, add_mset C N, U, None, NE, UE, add_mset (C+C')NS, US, N0, U0)› ‹(Propagated K C # M, add_mset C N, U, None, NE, UE, add_mset (C+C')NS, US, N0, U0)› X]) (auto simp: cdcl_learn_clause.simps cdcl_subsumed.simps cdcl_flush_unit.simps cdcl_propagate.simps dest!: true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or_generalise intro!: r_into_rtranclp) subgoal for M N NE NS N0 C' C U UE US U0 by (rule that[of ‹(M, N, U + {#C+C', C#}, None, NE, UE, NS, US, N0, U0)› X X X]) (auto simp: cdcl_learn_clause.simps cdcl_subsumed.simps cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def dest: true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or dest: true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or_generalise[of _ _ C]) subgoal for M N NE NS N0 C' C K U UE US U0 by (rule that[of ‹(M, N, U + {#C+C', C#}, None, NE, UE, NS, US, N0, U0)› ‹(M, N, add_mset C U, None, NE, UE, NS, add_mset (C+C')US, N0, U0)› ‹(Propagated K C # M, N, add_mset C U, None, NE, UE, NS, add_mset (C+C')US, N0, U0)› X]) (auto simp: cdcl_learn_clause.simps cdcl_subsumed.simps cdcl_flush_unit.simps cdcl_propagate.simps cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def dest!: true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or_generalise intro: r_into_rtranclp) subgoal for M N NE NS N0 C' U UE US U0 by (rule that[of ‹(M, N, U + {#C', {#}#}, None, NE, UE, NS, US, N0, U0)› ‹(M, N, add_mset {#} U, None, NE, UE, NS, add_mset (C')US, N0, U0)› ‹(M, N, add_mset {#} U, None, NE, UE, NS, add_mset (C')US, N0, U0)› ‹(M, N, add_mset {#} U, None, NE, UE, NS, add_mset (C')US, N0, U0)›]) (auto simp: cdcl_learn_clause.simps cdcl_subsumed.simps cdcl_flush_unit.simps cdcl_propagate.simps cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def cdcl_promote_false.simps dest!: true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or_generalise intro!: r_into_rtranclp) subgoal for M C' N NE NS N0 U UE US U0 using true_clss_clss_contradiction_true_clss_cls_false[of C' ‹insert C' (set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0)›] apply - by (rule that[of ‹(M, N + {#C', {#}#}, U, None, NE, UE, NS, US, N0, U0)› ‹(M, add_mset {#} N, U, None, NE, UE, add_mset (C')NS, US, N0, U0)› ‹(M, add_mset {#} N, U, None, NE, UE, add_mset (C')NS, US, N0, U0)› ‹(M, add_mset {#} N, U, None, NE, UE, add_mset (C')NS, US, N0, U0)›]) (auto simp: cdcl_learn_clause.simps cdcl_subsumed.simps cdcl_propagate.simps cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def cdcl_promote_false.simps dest: true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or_generalise intro!: r_into_rtranclp) done done lemma cdcl_unitres_learn_subsume: assumes ‹cdcl_unitres S U› ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of S)› shows ‹pcdcl^*^* S U› proof - have [dest!]: ‹cdcl_propagate^*^* S T ⟹ pcdcl^*^* S T› for S T by (rule mono_rtranclp[rule_format, of cdcl_propagate pcdcl]) (*Who is the idiot who wrote the theorem that way?*) (auto dest: pcdcl.intros pcdcl_core.intros) have [dest!]: ‹cdcl_flush_unit^*^* S T ⟹ pcdcl^*^* S T› for S T by (rule mono_rtranclp[rule_format, of cdcl_flush_unit pcdcl]) (auto dest: pcdcl.intros pcdcl_core.intros) have [dest!]: ‹cdcl_promote_false^*^* S T ⟹ pcdcl^*^* S T› for S T by (rule mono_rtranclp[rule_format, of cdcl_promote_false pcdcl]) (auto dest: pcdcl.intros pcdcl_core.intros) show ?thesis by (rule cdcl_unitres_learn_subsumeE[OF assms]) (auto dest!: pcdcl.intros pcdcl_core.intros) qed lemma get_all_ann_decomposition_count_decided0: ‹count_decided M = 0 ⟹ get_all_ann_decomposition M = [([], M)]› by (induction M rule: ann_lit_list_induct) auto text ‹The following two lemmas gives the nicer introduction rule that are what anyone expects from removing false literals.› lemma cdcl_unitresI1: assumes invs: ‹pcdcl_all_struct_invs (M, N, U + {#C+C'#}, None, NE, UE, NS, US, N0, U0)› and L: ‹∀L. L ∈# C' ⟶ -L ∈ lits_of_l M› and [simp]: ‹count_decided M = 0› and ‹¬ tautology C› and ent_init: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of (M, N, U + {#C+C'#}, None, NE, UE, NS, US, N0, U0))› shows ‹cdcl_unitres (M, N, U + {#C+C'#}, None, NE, UE, NS, US, N0, U0) (M, N, U + {#C#}, None, NE, UE, NS, add_mset (C+C') US, N0, U0)› (is ‹cdcl_unitres ?S ?T›) proof show ‹count_decided M = 0› and ‹¬ tautology C› by (rule assms)+ have ent: ‹all_decomposition_implies_m (cdcl_W_restart_mset.clauses (state_of ?S)) (get_all_ann_decomposition (trail (state_of ?S)))› and dist: ‹cdcl_W_restart_mset.distinct_cdcl_W_state (state_of ?S)› and alien: ‹cdcl_W_restart_mset.no_strange_atm (state_of ?S)› using invs unfolding pcdcl_all_struct_invs_def cdcl_W_restart_mset.cdcl_W_all_struct_inv_def by fast+ have [iff]: ‹insert (C+C') (set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0 ∪ (set_mset U ∪ set_mset UE ∪ set_mset US ∪ set_mset U0)) ⊨p NC ⟷ set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0 ⊨p NC› for NC using true_clss_clss_generalise_true_clss_clss[of ‹(set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0)› ‹insert (C+C') (set_mset U ∪ set_mset UE ∪ set_mset US ∪ set_mset U0)› ‹{NC}› ‹(set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0)›] ent_init by (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def) have ‹N + NE + NS + N0 ⊨psm mset_set (CNot (C''))› if ‹C'' ⊆# C'› for C'' using ent L ent_init that by (induction C'') (auto simp: clauses_def all_decomposition_implies_def lits_of_def uminus_lit_swap eq_commute[of ‹lit_of _›] cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def all_conj_distrib get_all_ann_decomposition_count_decided0 dest!: split_list mset_subset_eq_insertD) from this[of C'] show ‹N + NE + NS + N0 ⊨psm mset_set (CNot C')› by auto show ‹distinct_mset C› using dist by (auto simp: cdcl_W_restart_mset.distinct_cdcl_W_state_def dest: distinct_mset_union) show ‹atms_of C ⊆ atms_of_mm (N + NE + NS + N0)› using alien by (auto simp: cdcl_W_restart_mset.no_strange_atm_def) qed lemma cdcl_unitresI1_unit: fixes K :: ‹'v literal› defines ‹C ≡ {#K#}› assumes invs: ‹pcdcl_all_struct_invs (M, N, U + {#C+C'#}, None, NE, UE, NS, US, N0, U0)› and L: ‹∀L. L ∈# C' ⟶ -L ∈ lits_of_l M› and [simp]: ‹count_decided M = 0› and ‹¬ tautology C› and undef: ‹undefined_lit M K› and ent_init: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of (M, N, U + {#C+C'#}, None, NE, UE, NS, US, N0, U0))› shows ‹cdcl_unitres (M, N, U + {#C+C'#}, None, NE, UE, NS, US, N0, U0) (Propagated K C # M, N, U, None, NE, UE + {#C#}, NS, add_mset (C+C') US, N0, U0)› (is ‹cdcl_unitres ?S ?T›) proof show ‹count_decided M = 0› and ‹¬ tautology C› by (rule assms)+ have ent: ‹all_decomposition_implies_m (cdcl_W_restart_mset.clauses (state_of ?S)) (get_all_ann_decomposition (trail (state_of ?S)))› and dist: ‹cdcl_W_restart_mset.distinct_cdcl_W_state (state_of ?S)› and alien: ‹cdcl_W_restart_mset.no_strange_atm (state_of ?S)› using invs unfolding pcdcl_all_struct_invs_def cdcl_W_restart_mset.cdcl_W_all_struct_inv_def by fast+ have [iff]: ‹insert (C+C') (set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0 ∪ (set_mset U ∪ set_mset UE ∪ set_mset US∪ set_mset U0)) ⊨p NC ⟷ set_mset N ∪ set_mset NE ∪ set_mset NS∪ set_mset N0 ⊨p NC› for NC using true_clss_clss_generalise_true_clss_clss[of ‹(set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0)› ‹insert (C+C') (set_mset U ∪ set_mset UE ∪ set_mset US ∪ set_mset U0)› ‹{NC}› ‹(set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0)›] ent_init by (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def) have ‹N + NE + NS + N0 ⊨psm mset_set (CNot (C''))› if ‹C'' ⊆# C'› for C'' using ent L ent_init that by (induction C'') (auto simp: clauses_def all_decomposition_implies_def lits_of_def uminus_lit_swap eq_commute[of ‹lit_of _›] cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def all_conj_distrib get_all_ann_decomposition_count_decided0 dest!: split_list mset_subset_eq_insertD) from this[of C'] show ‹N + NE + NS + N0 ⊨psm mset_set (CNot C')› by auto show ‹distinct_mset C› using dist by (auto simp: cdcl_W_restart_mset.distinct_cdcl_W_state_def dest: distinct_mset_union) show ‹atms_of C ⊆ atms_of_mm (N + NE + NS + N0)› using alien by (auto simp: cdcl_W_restart_mset.no_strange_atm_def) show ‹C = {#K#}› unfolding C_def by auto show ‹undefined_lit M K› using undef by auto qed lemma cdcl_unitresI2: assumes invs: ‹pcdcl_all_struct_invs (M, N + {#C+C'#}, U, None, NE, UE, NS, US, N0, U0)› and L: ‹∀L. L ∈# C' ⟶ -L ∈ lits_of_l M› and [simp]: ‹count_decided M = 0› and ‹¬ tautology C› and ent_init: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of (M, N + {#C+C'#}, U, None, NE, UE, NS, US, N0, U0))› shows ‹cdcl_unitres (M, N + {#C+C'#}, U, None, NE, UE, NS, US, N0, U0) (M, N + {#C#}, U, None, NE, UE, add_mset (C+C') NS, US, N0, U0)› (is ‹cdcl_unitres ?S ?T›) proof show ‹count_decided M = 0› and ‹¬ tautology C› by (rule assms)+ have ent: ‹all_decomposition_implies_m (cdcl_W_restart_mset.clauses (state_of ?S)) (get_all_ann_decomposition (trail (state_of ?S)))› and dist: ‹cdcl_W_restart_mset.distinct_cdcl_W_state (state_of ?S)› and alien: ‹cdcl_W_restart_mset.no_strange_atm (state_of ?S)› using invs unfolding pcdcl_all_struct_invs_def cdcl_W_restart_mset.cdcl_W_all_struct_inv_def by fast+ have [iff]: ‹insert (C+C') (set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0 ∪ (set_mset U ∪ set_mset UE ∪ set_mset US ∪ set_mset U0)) ⊨p NC ⟷ insert (C+C') (set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0) ⊨p NC› for NC using true_clss_clss_generalise_true_clss_clss[of ‹insert (C+C') (set_mset N ∪ set_mset NE ∪ set_mset NS∪ set_mset N0)› ‹(set_mset U ∪ set_mset UE ∪ set_mset US∪ set_mset U0)› ‹{NC}› ‹insert (C+C') (set_mset N ∪ set_mset NE ∪ set_mset NS∪ set_mset N0)›] ent_init by (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def dest: true_clss_cs_mono_l) have ‹add_mset (C+C') (N + NE + NS + N0) ⊨psm mset_set (CNot C'')› if ‹C'' ⊆# C'› for C'' using that apply (induction C'') using ent L ent_init by (auto simp: clauses_def all_decomposition_implies_def lits_of_def uminus_lit_swap eq_commute[of _ ‹lit_of _›] cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def get_all_ann_decomposition_count_decided0 dest!: split_list mset_subset_eq_insertD) from this[of C'] show ‹add_mset (C+C') (N + NE + NS + N0) ⊨psm mset_set (CNot C')› by auto show ‹distinct_mset C› using dist by (auto simp: cdcl_W_restart_mset.distinct_cdcl_W_state_def dest: distinct_mset_union) qed lemma cdcl_unitresI2_unit: fixes K :: ‹'v literal› defines ‹C ≡ {#K#}› assumes invs: ‹pcdcl_all_struct_invs (M, N + {#C+C'#}, U, None, NE, UE, NS, US, N0, U0)› and L: ‹∀L. L ∈# C' ⟶ -L ∈ lits_of_l M› and [simp]: ‹count_decided M = 0› and ‹¬ tautology C› and undef: ‹undefined_lit M K› and ent_init: ‹cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init (state_of (M, N + {#C+C'#}, U, None, NE, UE, NS, US, N0, U0))› shows ‹cdcl_unitres (M, N + {#C+C'#}, U, None, NE, UE, NS, US, N0, U0) (Propagated K C # M, N, U, None, NE + {#C#}, UE, add_mset (C+C') NS, US, N0, U0)› (is ‹cdcl_unitres ?S ?T›) proof show ‹count_decided M = 0› and ‹¬ tautology C› and ‹undefined_lit M K› by (rule assms)+ show ‹C = {#K#}› unfolding C_def .. have ent: ‹all_decomposition_implies_m (cdcl_W_restart_mset.clauses (state_of ?S)) (get_all_ann_decomposition (trail (state_of ?S)))› and dist: ‹cdcl_W_restart_mset.distinct_cdcl_W_state (state_of ?S)› and alien: ‹cdcl_W_restart_mset.no_strange_atm (state_of ?S)› using invs unfolding pcdcl_all_struct_invs_def cdcl_W_restart_mset.cdcl_W_all_struct_inv_def by fast+ have [iff]: ‹insert (C+C') (set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0 ∪ (set_mset U ∪ set_mset UE ∪ set_mset US ∪ set_mset U0)) ⊨p NC ⟷ insert (C+C') (set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0) ⊨p NC› for NC using true_clss_clss_generalise_true_clss_clss[of ‹insert (C+C') (set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0)› ‹(set_mset U ∪ set_mset UE ∪ set_mset US ∪ set_mset U0)› ‹{NC}› ‹insert (C+C') (set_mset N ∪ set_mset NE ∪ set_mset NS ∪ set_mset N0)›] ent_init by (auto simp: cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def dest: true_clss_cs_mono_l) have ‹add_mset (C+C') (N + NE + NS + N0) ⊨psm mset_set (CNot C'')› if ‹C'' ⊆# C'› for C'' using that apply (induction C'') using ent L ent_init by (auto simp: clauses_def all_decomposition_implies_def lits_of_def uminus_lit_swap eq_commute[of _ ‹lit_of _›] cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def get_all_ann_decomposition_count_decided0 dest!: split_list mset_subset_eq_insertD) from this[of C'] show ‹add_mset (C+C') (N + NE + NS + N0) ⊨psm mset_set (CNot C')› by auto show ‹distinct_mset C› using dist by (auto simp: cdcl_W_restart_mset.distinct_cdcl_W_state_def dest: distinct_mset_union) qed subsection ‹Subsumption resolution› text ‹ Subsumption-Resolution rules are the composition of resolution, subsumption, learning of a clause, and potentially forget. However, we have decided to not model the forget, because we would like to map the calculus to a version without restarts. › inductive cdcl_subresolution :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where subresolution_II: ‹cdcl_subresolution (M, N + {#add_mset L C, add_mset (-L) C'#}, U, D, NE, UE, NS, US, N0, U0) (M, N + {#add_mset L C, remdups_mset C'#}, U, D, NE, UE, add_mset (add_mset (-L) C') NS, US, N0, U0)› if ‹count_decided M = 0› ‹C ⊆# C'›| subresolution_LL: ‹cdcl_subresolution (M, N, U + {#add_mset L C, add_mset (-L) C'#}, D, NE, UE, NS, US, N0, U0) (M, N, U + {#add_mset L C, remdups_mset (C')#}, D, NE, UE, NS, add_mset (add_mset (-L) C') US, N0, U0)› if ‹count_decided M = 0› and ‹¬tautology (C + C')› and ‹C ⊆# C'›| subresolution_LI: ‹cdcl_subresolution (M, N + {#add_mset L C#}, U + {#add_mset (-L) C'#}, D, NE, UE, NS, US, N0, U0) (M, N + {#add_mset L C#}, U + {#remdups_mset (C')#}, D, NE, UE, NS, add_mset (add_mset (-L) C') US, N0, U0)› if ‹count_decided M = 0› and ‹¬tautology (C + C')› and ‹C ⊆# C'›| subresolution_IL: ‹cdcl_subresolution (M, N + {#add_mset L C#}, U + {#add_mset (-L) C'#}, D, NE, UE, NS, US, N0, U0) (M, N + {#remdups_mset C#}, U + {#add_mset (-L) C'#}, D, NE, UE, add_mset (add_mset L C) NS, US, N0, U0)› if ‹count_decided M = 0› and ‹¬tautology (C + C')› and ‹C' ⊆# C› lemma cdcl_subresolution: assumes ‹cdcl_subresolution S T› shows ‹pcdcl^*^* S T› using assms proof (induction rule: cdcl_subresolution.induct) case (subresolution_II M C C' N L U D NE UE NS US N0 U0) then show ?case apply - apply (rule converse_rtranclp_into_rtranclp) apply (rule pcdcl.intros(3)) apply (rule cdcl_resolution.resolution_II, assumption) apply (rule r_into_rtranclp) apply (rule pcdcl.intros(4)) using cdcl_subsumed.intros(1)[of ‹remdups_mset (C + C')› ‹add_mset (- L) C'› M ‹N + {#add_mset L C#}› U D NE UE NS US N0 U0] apply (auto simp add: dest!: remdups_mset_sum_subset(1) simp: remdups_mset_subset_add_mset add_mset_commute) done next case (subresolution_LL M C C' N U L D NE UE NS US N0 U0) then show ?case apply - apply (rule converse_rtranclp_into_rtranclp) apply (rule pcdcl.intros(3)) apply (rule cdcl_resolution.resolution_LL, assumption, assumption) apply (rule r_into_rtranclp) apply (rule pcdcl.intros(4)) using cdcl_subsumed.intros(2)[of ‹remdups_mset (C + C')› ‹add_mset (- L) C'› M N ‹U + {#add_mset L C#}› D NE UE NS US] apply (auto dest!: remdups_mset_sum_subset(1) simp: remdups_mset_subset_add_mset add_mset_commute) done next case (subresolution_LI M C C' N L U D NE UE NS US) then show ?case apply - apply (rule converse_rtranclp_into_rtranclp) apply (rule pcdcl.intros(3)) apply (rule cdcl_resolution.resolution_IL, assumption, assumption) apply (rule r_into_rtranclp) apply (rule pcdcl.intros(4)) using cdcl_subsumed.intros(2)[of ‹remdups_mset (C + C')› ‹add_mset (- L) C'› M ‹N + {#add_mset L C#}› ‹U› D NE UE NS US] apply (auto simp add: dest!: remdups_mset_sum_subset(1) simp: remdups_mset_subset_add_mset add_mset_commute) done next case (subresolution_IL M C C' N L U D NE UE NS US N0 U0) then have [simp]: ‹remdups_mset (C + C') = remdups_mset C› and tauto: ‹¬ tautology (remdups_mset (C + C'))› using remdups_mset_sum_subset(2) by auto have [simp]: ‹remdups_mset C ⊆# add_mset L C› by (simp add: remdups_mset_subset_add_mset) have 1: ‹cdcl_resolution (M, N + {#add_mset L C#}, U + {#add_mset (- L) C'#}, D, NE, UE, NS, US, N0, U0) (M, N + {#add_mset L C#}, U + {#add_mset (- L) C', remdups_mset (C + C')#}, D, NE, UE, NS, US, N0, U0)› (is ‹cdcl_resolution ?A ?B›) using subresolution_IL apply - by (rule cdcl_resolution.resolution_IL, assumption, assumption) have ‹cdcl_learn_clause (M, add_mset (add_mset L C) N, add_mset (remdups_mset (C + C')) (U + {#add_mset (- L) C'#}), D, NE, UE, NS, US, N0, U0) (M, add_mset (remdups_mset (C + C')) (add_mset (add_mset L C) N), U + {#add_mset (- L) C'#}, D, NE, UE, NS, US, N0, U0)› (is ‹cdcl_learn_clause _ ?C›) by (rule cdcl_learn_clause.intros(3)[of ‹remdups_mset (C+C')›, OF tauto]) then have 2: ‹cdcl_learn_clause ?B ?C› by (auto simp: add_mset_commute) have 3: ‹cdcl_subsumed ?C (M, N + {#remdups_mset C#}, U + {#add_mset (- L) C'#}, D, NE, UE, add_mset (add_mset L C) NS, US, N0, U0)› using cdcl_subsumed.intros(1)[of ‹remdups_mset C› ‹add_mset L C› M] by (auto simp: add_mset_commute dest!: ) show ?case using subresolution_IL apply - apply (rule converse_rtranclp_into_rtranclp) apply (rule pcdcl.intros(3)[OF 1]) apply (rule converse_rtranclp_into_rtranclp) apply (rule pcdcl.intros(2)) apply (rule 2) apply (rule converse_rtranclp_into_rtranclp) apply (rule pcdcl.intros(4)) apply (rule 3) by auto qed section ‹Variable elimination› text ‹This is a very first attempt to definit Variable elimination in a very general way. However, it is not clear how to handle tautologies (because the variable is not elimination in this case).› definition elim_var :: ‹'v ⇒ 'v clauses ⇒ 'v clauses› where ‹elim_var L N = {#C ∈# N. L ∉ atms_of C#} + (λ(C, D). removeAll_mset (Pos L) (removeAll_mset (Neg L) (C + D))) `# ((filter_mset (λC. Pos L ∈# C) N) ×# (filter_mset (λC. Neg L ∈# C) N))› lemma ‹L ∉ atms_of_mm (elim_var L N)› unfolding elim_var_def apply (auto simp: atms_of_ms_def atms_of_def add_mset_eq_add_mset eq_commute[of ‹_ - _› ‹add_mset _ _›] in_diff_count dest!: multi_member_split) apply (auto dest!: union_single_eq_member simp: in_diff_count split: if_splits) using literal.exhaust_sel apply blast+ done section ‹Bactrack for unit clause› text ‹This is the specific case where we learn a new unit clause and directly add it to the right place.› inductive cdcl_backtrack_unit :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where ‹cdcl_backtrack_unit (M, N, U, Some (add_mset L D), NE, UE, NS, US, N0, U0) (Propagated L {#L#} # M1, N, U, None, NE, add_mset {#L#} UE, NS, US, N0, U0)› if ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition M)› and ‹get_level M L = count_decided M› and ‹get_level M L = get_maximum_level M {#L#}› and ‹get_level M K = 1› and ‹N + U + NE + UE + NS + US + N0 + U0 ⊨pm {#L#}› lemma cdcl_backtrack_unit_is_backtrack: assumes ‹cdcl_backtrack_unit S U› obtains T where ‹cdcl_backtrack S T› and ‹cdcl_flush_unit T U› using assms proof (induction rule: cdcl_backtrack_unit.induct) case (1 K M1 M2 M L N U NE UE NS US N0 U0 D) note H =this(1-5) and that = this(6) let ?T = ‹(Propagated L (add_mset L {#}) # M1, N, add_mset (add_mset L {#}) U, None, NE, UE, NS, US, N0, U0)› have ‹cdcl_backtrack (M, N, U, Some (add_mset L D), NE, UE, NS, US, N0, U0) ?T› apply (rule cdcl_backtrack.intros[of K M1 M2 _ _ _ 0]) using H by auto moreover have ‹cdcl_flush_unit ?T (Propagated L {#L#} # M1, N, U, None, NE, add_mset {#L#} UE, NS, US, N0, U0)› by (rule cdcl_flush_unit.intros(2)) (use H in ‹auto dest!: get_all_ann_decomposition_exists_prepend simp: get_level_append_if split: if_splits›) ultimately show ?case using that by blast qed lemma cdcl_backtrack_unit_pcdcl_all_struct_invs: ‹cdcl_backtrack_unit S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T› by (auto elim!: cdcl_backtrack_unit_is_backtrack intro: pcdcl_all_struct_invs dest!: pcdcl.intros(1) pcdcl.intros(5) pcdcl_core.intros(6)) lemma cdcl_backtrack_unit_is_CDCL_backtrack: ‹cdcl_backtrack_unit S T ⟹ cdcl_W_restart_mset.backtrack (state_of S) (state_of T)› unfolding cdcl_backtrack_unit.simps apply clarify apply (rule cdcl_W_restart_mset.backtrack.intros[of _ ‹lit_of (hd (pget_trail T))› ‹the (pget_conflict S) - {#lit_of (hd (pget_trail T))#}› _ _ _ ‹mark_of (hd (pget_trail T)) - {#lit_of (hd (pget_trail T))#}›]) by (auto simp: clauses_def ac_simps cdcl_W_restart_mset_reduce_trail_to) section ‹Subsume and promote› inductive cdcl_subsumed_RI :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› where cdcl_subsumed_RI: ‹cdcl_subsumed_RI (M, add_mset C' N, add_mset C U, D, NE, UE, NS, US, N0, U0) (M, add_mset C N, U, D, NE, UE, NS + {#C'#}, US, N0, U0)› if ‹C ⊆# C'› ‹¬tautology C› ‹distinct_mset C› lemma cdcl_subsumed_RID: assumes ‹cdcl_subsumed_RI S W› obtains T where ‹cdcl_learn_clause S T› and ‹cdcl_subsumed T W› using assms(1) proof (cases rule: cdcl_subsumed_RI.cases) case (cdcl_subsumed_RI C C' M N U D NE UE NS US N0 U0) let ?T = ‹(M, add_mset C (add_mset C' N), U, D, NE, UE, NS, US, N0, U0)› show ?thesis apply (rule that[of ?T]) subgoal using cdcl_subsumed_RI by (auto simp: cdcl_learn_clause.simps cdcl_W_restart_mset.cdcl_W_learned_clauses_entailed_by_init_def mset_subset_eq_exists_conv) subgoal using cdcl_subsumed_RI by (auto simp: cdcl_subsumed.simps) done qed lemma cdcl_subsumed_RI_pcdcl: assumes ‹cdcl_subsumed_RI S W› shows ‹pcdcl^*^* S W› by (rule cdcl_subsumed_RID[OF assms]) (metis pcdcl.intros(2,4) rtranclp.rtrancl_refl tranclp_into_rtranclp tranclp_unfold_end) section ‹Termination› text ‹ We here define the terminating fragment of our pragmatic CDCL. Basically, there is a design decision to take here. Either we decide to move term‹cdcl_backtrack_unit› into the term‹pcdcl_core› or we decide to define a larger terminating fragment. The first option is easier (even if we need a larger core), but we want to be able to add subsumption test after backtrack and this requires an extension of the core anyway. › inductive pcdcl_tcore :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› for S T :: ‹'v prag_st› where ‹pcdcl_core S T ⟹ pcdcl_tcore S T› | ‹cdcl_subsumed S T ⟹ pcdcl_tcore S T› | ‹cdcl_flush_unit S T ⟹ pcdcl_tcore S T› | ‹cdcl_backtrack_unit S T ⟹ pcdcl_tcore S T› inductive pcdcl_tcore_stgy :: ‹'v prag_st ⇒ 'v prag_st ⇒ bool› for S T :: ‹'v prag_st› where ‹pcdcl_core_stgy S T ⟹ pcdcl_tcore_stgy S T› | ‹cdcl_subsumed S T ⟹ pcdcl_tcore_stgy S T›| ‹cdcl_flush_unit S T ⟹ pcdcl_tcore_stgy S T› | ‹cdcl_backtrack_unit S T ⟹ pcdcl_tcore_stgy S T› lemma pcdcl_tcore_stgy_pcdcl_tcoreD: ‹pcdcl_tcore_stgy S T ⟹ pcdcl_tcore S T› using pcdcl_core_stgy_pcdcl pcdcl_tcore.simps pcdcl_tcore_stgy.simps by blast lemma rtranclp_pcdcl_tcore_stgy_pcdcl_tcoreD: ‹pcdcl_tcore_stgy^*^* S T ⟹ pcdcl_tcore^*^* S T› by (induction rule: rtranclp_induct) (auto dest: pcdcl_tcore_stgy_pcdcl_tcoreD) definition pcdcl_core_measure :: ‹_› where ‹pcdcl_core_measure = {(T, S). cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S) ∧ cdcl_W_restart_mset.cdcl_W (state_of S) (state_of T)} ∪ {(T, S). state_of S = state_of T ∧ size (pget_clauses S) > size (pget_clauses T)}› lemma wf_pcdcl_core_measure: ‹wf pcdcl_core_measure› unfolding pcdcl_core_measure_def proof (rule wf_union_compatible) let ?CDCL = ‹{(T, S). cdcl_W_restart_mset.cdcl_W_all_struct_inv (state_of S) ∧ cdcl_W_restart_mset.cdcl_W (state_of S) (state_of T)}› let ?P = ‹{(T, S). state_of S = state_of T ∧ size (pget_clauses S) > size (pget_clauses T)}› show ‹wf ?CDCL› using wf_if_measure_f[OF cdcl_W_restart_mset.wf_cdcl_W, of state_of] by auto show ‹wf ?P› by (rule wf_subset[of ‹{(T, S). size (pget_clauses S) > size (pget_clauses T)}›]) (use wf_if_measure_f[of less_than ‹size o pget_clauses›] in auto) show ‹?CDCL O ?P ⊆ ?CDCL› by auto qed lemma pcdcl_tcore_in_pcdcl_core_measure: ‹{(T, S). pcdcl_all_struct_invs S ∧ pcdcl_tcore S T} ⊆ pcdcl_core_measure› proof - have ‹pcdcl_tcore S T ⟹ pcdcl_all_struct_invs S ⟹ (T, S) ∈ pcdcl_core_measure› for S T apply (induction rule: pcdcl_tcore.induct) subgoal by (auto simp: pcdcl_core_measure_def pcdcl_all_struct_invs_def pcdcl_core_is_cdcl) subgoal by (auto simp: pcdcl_core_measure_def cdcl_subsumed.simps) subgoal by (auto simp: pcdcl_core_measure_def cdcl_flush_unit.simps) subgoal by (auto dest!: cdcl_backtrack_unit_is_CDCL_backtrack simp: pcdcl_all_struct_invs_def pcdcl_core_measure_def cdcl_W_restart_mset.cdcl_W_bj_cdcl_W_stgy cdcl_W_restart_mset.cdcl_W_bj.simps cdcl_W_restart_mset.cdcl_W_stgy_cdcl_W) done then show ‹?thesis› by force qed lemmas wf_pcdcl_tcore = wf_subset[OF wf_pcdcl_core_measure pcdcl_tcore_in_pcdcl_core_measure] lemma wf_pcdcl_tcore_stgy: ‹wf {(T, S). pcdcl_all_struct_invs S ∧ pcdcl_tcore_stgy S T}› by (rule wf_subset[OF wf_pcdcl_tcore]) (auto simp add: pcdcl_tcore_stgy_pcdcl_tcoreD) lemma pcdcl_tcore_pcdcl: ‹pcdcl_tcore S T ⟹ pcdcl^*^* S T› by (induction rule: pcdcl_tcore.induct) (fastforce dest: pcdcl.intros dest!: pcdcl_core.intros elim!: cdcl_backtrack_unit_is_backtrack)+ lemma pcdcl_tcore_pcdcl_all_struct_invs: ‹pcdcl_tcore S T ⟹ pcdcl_all_struct_invs S ⟹ pcdcl_all_struct_invs T› using cdcl_backtrack_unit_pcdcl_all_struct_invs pcdcl.intros(1) pcdcl.intros(4) pcdcl.intros(5) pcdcl_all_struct_invs pcdcl_tcore.simps by blast lemma pcdcl_core_stgy_no_smaller_propa: ‹pcdcl_core_stgy S T ⟹ pcdcl_all_struct_invs S ⟹ cdcl_W_restart_mset.no_smaller_propa (state_of S) ⟹ cdcl_W_restart_mset.no_smaller_propa (state_of T)› using pcdcl_core_stgy_is_cdcl_stgy[of S T] unfolding pcdcl_all_struct_invs_def by (auto dest: cdcl_W_restart_mset.cdcl_W_stgy_no_smaller_propa) lemma pcdcl_stgy_no_smaller_propa: ‹pcdcl_stgy S T ⟹ pcdcl_all_struct_invs S ⟹ cdcl_W_restart_mset.no_smaller_propa (state_of S) ⟹ cdcl_W_restart_mset.no_smaller_propa (state_of T)› apply (induction rule: pcdcl_stgy.induct) subgoal by (auto dest!: pcdcl_core_stgy_no_smaller_propa) subgoal by (auto simp: cdcl_W_restart_mset.no_smaller_propa_def cdcl_learn_clause.simps clauses_def) subgoal by (auto simp: cdcl_W_restart_mset.no_smaller_propa_def cdcl_resolution.simps) subgoal by (auto simp: cdcl_W_restart_mset.no_smaller_propa_def cdcl_subsumed.simps clauses_def) subgoal by (auto simp: cdcl_W_restart_mset.no_smaller_propa_def cdcl_flush_unit.simps) subgoal apply (auto simp: cdcl_W_restart_mset.no_smaller_propa_def cdcl_inp_propagate.simps) apply (case_tac M'; auto)+ done subgoal by (auto simp: cdcl_W_restart_mset.no_smaller_propa_def cdcl_inp_conflict.simps) subgoal by (auto simp: cdcl_unitres_true_same) done lemma rtranclp_pcdcl_stgy_no_smaller_propa: ‹pcdcl_stgy^*^* S T ⟹ pcdcl_all_struct_invs S ⟹ cdcl_W_restart_mset.no_smaller_propa (state_of S) ⟹ cdcl_W_restart_mset.no_smaller_propa (state_of T)› apply (induction rule: rtranclp_induct) subgoal by auto subgoal for T U using rtranclp_pcdcl_all_struct_invs[of S T] rtranclp_pcdcl_stgy_pcdcl[of S T] pcdcl_stgy_no_smaller_propa[of T U] by auto done lemma pcdcl_tcore_stgy_pcdcl_stgy: ‹pcdcl_tcore_stgy S T ⟹ pcdcl_stgy⁺⁺ S T› apply (auto simp: pcdcl_tcore_stgy.simps pcdcl_stgy.simps) by (metis cdcl_backtrack_unit_is_backtrack pcdcl_core_stgy.intros(6) pcdcl_stgy.intros(1) pcdcl_stgy.intros(5) tranclp.simps) lemma pcdcl_tcore_stgy_no_smaller_propa: ‹pcdcl_tcore_stgy S T ⟹ pcdcl_all_struct_invs S ⟹ cdcl_W_restart_mset.no_smaller_propa (state_of S) ⟹ cdcl_W_restart_mset.no_smaller_propa (state_of T)› using pcdcl_tcore_stgy_pcdcl_stgy[of S T] rtranclp_pcdcl_stgy_no_smaller_propa[of S T] by (auto simp: tranclp_into_rtranclp) lemma rtranclp_pcdcl_tcore_stgy_no_smaller_propa: ‹pcdcl_tcore_stgy^*^* S T ⟹ pcdcl_all_struct_invs S ⟹ cdcl_W_restart_mset.no_smaller_propa (state_of S) ⟹ cdcl_W_restart_mset.no_smaller_propa (state_of T)› by (metis (no_types, opaque_lifting) mono_rtranclp pcdcl_tcore_stgy_pcdcl_stgy rtranclp_idemp rtranclp_pcdcl_stgy_no_smaller_propa tranclp_into_rtranclp) lemma pcdcl_stgy_stgy_invariant: ‹pcdcl_stgy S T ⟹ pcdcl_all_struct_invs S ⟹ cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of S) ⟹ cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of T)› using pcdcl_all_struct_invs_def pcdcl_stgy_stgy_invs by blast lemma rtranclp_pcdcl_stgy_stgy_invariant: ‹pcdcl_stgy^*^* S T ⟹ pcdcl_all_struct_invs S ⟹ cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of S) ⟹ cdcl_W_restart_mset.cdcl_W_stgy_invariant (state_of T)› apply (induction rule: rtranclp_induct) apply auto[] by (metis (no_types, lifting) pcdcl_stgy_stgy_invariant rtranclp_pcdcl_all_struct_invs rtranclp_pcdcl_stgy_pcdcl) lemma pcdcl_tcore_nocp_pcdcl_tcore_stgy: ‹pcdcl_tcore S T ⟹ no_step cdcl_propagate S ⟹ no_step cdcl_conflict S ⟹ pcdcl_tcore_stgy S T› by (auto simp: pcdcl_tcore.simps pcdcl_tcore_stgy.simps pcdcl_core_stgy.simps pcdcl_core.simps) lemma pcdcl_tcore_stgy_pcdcl_stgy': ‹pcdcl_tcore_stgy S T ⟹ pcdcl_stgy^*^* S T› by (auto simp: pcdcl_stgy.simps pcdcl_tcore_stgy.simps pcdcl_tcore_stgy.simps pcdcl_tcore_stgy_pcdcl_stgy rtranclp_unfold) lemma rtranclp_pcdcl_tcore_stgy_pcdcl_stgy': ‹pcdcl_tcore_stgy^*^* S T ⟹ pcdcl_stgy^*^* S T› by (induction rule: rtranclp_induct) (auto dest!: pcdcl_tcore_stgy_pcdcl_stgy') lemma pcdcl_core_stgy_conflict_non_zero_unless_level_0: ‹pcdcl_core_stgy S T ⟹ pcdcl_all_struct_invs S ⟹ cdcl_W_restart_mset.no_false_clause (state_of S) ⟹ cdcl_W_restart_mset.conflict_non_zero_unless_level_0 (state_of S) ⟹ cdcl_W_restart_mset.conflict_non_zero_unless_level_0 (state_of T)› using pcdcl_core_stgy_is_cdcl_stgy[of S T] using cdcl_W_restart_mset.cdcl_W_restart_conflict_non_zero_unless_level_0[of ‹state_of S› ‹state_of T›] by (auto simp: pcdcl_all_struct_invs_def cdcl_W_restart_mset.cdcl_W_stgy_cdcl_W_restart) lemma pcdcl_stgy_conflict_non_zero_unless_level_0: ‹pcdcl_stgy S T ⟹ pcdcl_all_struct_invs S ⟹ cdcl_W_restart_mset.no_false_clause (state_of S) ⟹ cdcl_W_restart_mset.conflict_non_zero_unless_level_0 (state_of S) ⟹ cdcl_W_restart_mset.conflict_non_zero_unless_level_0 (state_of T)› apply (induction rule: pcdcl_stgy.induct) subgoal using pcdcl_core_stgy_conflict_non_zero_unless_level_0[of S T] by fast subgoal by (auto simp: cdcl_learn_clause.simps cdcl_W_restart_mset.conflict_non_zero_unless_level_0_def) subgoal by (auto simp: cdcl_resolution.simps cdcl_W_restart_mset.conflict_non_zero_unless_level_0_def) subgoal by (auto simp: cdcl_subsumed.simps cdcl_W_restart_mset.conflict_non_zero_unless_level_0_def) subgoal by (auto simp: cdcl_flush_unit.simps cdcl_W_restart_mset.conflict_non_zero_unless_level_0_def) subgoal by (auto simp: cdcl_inp_propagate.simps cdcl_W_restart_mset.conflict_non_zero_unless_level_0_def) subgoal by (auto simp: cdcl_inp_conflict.simps cdcl_W_restart_mset.conflict_non_zero_unless_level_0_def) subgoal by (auto simp: cdcl_unitres_true_same) done text ‹ TODO: rename to term‹full_t› or something along that line. › definition full2 :: ‹('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool› where ‹full2 transf transf2 = (λS S'. rtranclp transf S S' ∧ no_step transf2 S')› end

Theory CDCL.Pragmatic_CDCL