theory CDCL_W_Implementation
imports DPLL_CDCL_W_Implementation CDCL_W_Termination
begin
notation image_mset (infixr "`#" 90)
type_synonym 'a cdcl⇩W_mark = "'a clause"
type_synonym cdcl⇩W_decided_level = nat
type_synonym 'v cdcl⇩W_ann_literal = "('v, cdcl⇩W_decided_level, 'v cdcl⇩W_mark) ann_literal"
type_synonym 'v cdcl⇩W_ann_literals = "('v, cdcl⇩W_decided_level, 'v cdcl⇩W_mark) ann_literals"
type_synonym 'v cdcl⇩W_state =
"'v cdcl⇩W_ann_literals × 'v clauses × 'v clauses × nat × 'v clause option"
abbreviation trail :: "'a × 'b × 'c × 'd × 'e ⇒ 'a" where
"trail ≡ (λ(M, _). M)"
abbreviation cons_trail :: "'a ⇒ 'a list × 'b × 'c × 'd × 'e ⇒ 'a list × 'b × 'c × 'd × 'e"
where
"cons_trail ≡ (λL (M, S). (L#M, S))"
abbreviation tl_trail :: "'a list × 'b × 'c × 'd × 'e ⇒ 'a list × 'b × 'c × 'd × 'e" where
"tl_trail ≡ (λ(M, S). (tl M, S))"
abbreviation clss :: "'a × 'b × 'c × 'd × 'e ⇒ 'b" where
"clss ≡ λ(M, N, _). N"
abbreviation learned_clss :: "'a × 'b × 'c × 'd × 'e ⇒ 'c" where
"learned_clss ≡ λ(M, N, U, _). U"
abbreviation backtrack_lvl :: "'a × 'b × 'c × 'd × 'e ⇒ 'd" where
"backtrack_lvl ≡ λ(M, N, U, k, _). k"
abbreviation update_backtrack_lvl :: "'d ⇒ 'a × 'b × 'c × 'd × 'e ⇒ 'a × 'b × 'c × 'd × 'e"
where
"update_backtrack_lvl ≡ λk (M, N, U, _, S). (M, N, U, k, S)"
abbreviation conflicting :: "'a × 'b × 'c × 'd × 'e ⇒ 'e" where
"conflicting ≡ λ(M, N, U, k, D). D"
abbreviation update_conflicting :: "'e ⇒ 'a × 'b × 'c × 'd × 'e ⇒ 'a × 'b × 'c × 'd × 'e"
where
"update_conflicting ≡ λS (M, N, U, k, _). (M, N, U, k, S)"
abbreviation "S0_cdcl⇩W N ≡ (([], N, {#}, 0, None):: 'v cdcl⇩W_state)"
abbreviation add_learned_cls where
"add_learned_cls ≡ λC (M, N, U, S). (M, N, {#C#} + U, S)"
abbreviation remove_cls where
"remove_cls ≡ λC (M, N, U, S). (M, remove_mset C N, remove_mset C U, S)"
lemma trail_conv: "trail (M, N, U, k, D) = M" and
clauses_conv: "clss (M, N, U, k, D) = N" and
learned_clss_conv: "learned_clss (M, N, U, k, D) = U" and
conflicting_conv: "conflicting (M, N, U, k, D) = D" and
backtrack_lvl_conv: "backtrack_lvl (M, N, U, k, D) = k"
by auto
lemma state_conv:
"S = (trail S, clss S, learned_clss S, backtrack_lvl S, conflicting S)"
by (cases S) auto
interpretation state⇩W trail clss learned_clss backtrack_lvl conflicting
"λL (M, S). (L # M, S)"
"λ(M, S). (tl M, S)"
"λC (M, N, S). (M, {#C#} + N, S)"
"λC (M, N, U, S). (M, N, {#C#} + U, S)"
"λC (M, N, U, S). (M, remove_mset C N, remove_mset C U, S)"
"λ(k::nat) (M, N, U, _, D). (M, N, U, k, D)"
"λD (M, N, U, k, _). (M, N, U, k, D)"
"λN. ([], N, {#}, 0, None)"
"λ(_, N, U, _). ([], N, U, 0, None)"
by unfold_locales auto
interpretation cdcl⇩W trail clss learned_clss backtrack_lvl conflicting
"λL (M, S). (L # M, S)"
"λ(M, S). (tl M, S)"
"λC (M, N, S). (M, {#C#} + N, S)"
"λC (M, N, U, S). (M, N, {#C#} + U, S)"
"λC (M, N, U, S). (M, remove_mset C N, remove_mset C U, S)"
"λ(k::nat) (M, N, U, _, D). (M, N, U, k, D)"
"λD (M, N, U, k, _). (M, N, U, k, D)"
"λN. ([], N, {#}, 0, None)"
"λ(_, N, U, _). ([], N, U, 0, None)"
by unfold_locales auto
declare clauses_def[simp]
lemma cdcl⇩W_state_eq_equality[iff]: "state_eq S T ⟷ S = T"
unfolding state_eq_def by (cases S, cases T) auto
declare state_simp[simp del]
subsection ‹CDCL Implementation›
subsubsection ‹Definition of the rules›
paragraph ‹Types›
lemma true_clss_remdups[simp]:
"I ⊨s (mset ∘ remdups) ` N ⟷ I ⊨s mset ` N"
by (simp add: true_clss_def)
lemma satisfiable_mset_remdups[simp]:
"satisfiable ((mset ∘ remdups) ` N) ⟷ satisfiable (mset ` N)"
unfolding satisfiable_carac[symmetric] by simp
value "backtrack_split [Decided (Pos (Suc 0)) ()]"
value "∃C ∈ set [[Pos (Suc 0), Neg (Suc 0)]]. (∀c ∈ set C. -c ∈ lits_of [Decided (Pos (Suc 0)) ()])"
type_synonym cdcl⇩W_state_inv_st = "(nat, nat, nat literal list) ann_literal list ×
nat literal list list × nat literal list list × nat × nat literal list option"
text ‹We need some functions to convert between our abstract state @{typ "nat cdcl⇩W_state"} and the
concrete state @{typ "cdcl⇩W_state_inv_st"}.›
fun convert :: "('a, 'b, 'c list) ann_literal ⇒ ('a, 'b, 'c multiset) ann_literal" where
"convert (Propagated L C) = Propagated L (mset C)" |
"convert (Decided K i) = Decided K i"
abbreviation convertC :: "'a list option ⇒ 'a multiset option" where
"convertC ≡ map_option mset"
lemma convert_Propagated[elim!]:
"convert z = Propagated L C ⟹ (∃C'. z = Propagated L C' ∧ C = mset C')"
by (cases z) auto
lemma get_rev_level_map_convert:
"get_rev_level (map convert M) n x = get_rev_level M n x"
by (induction M arbitrary: n rule: ann_literal_list_induct) auto
lemma get_level_map_convert[simp]:
"get_level (map convert M) = get_level M"
using get_rev_level_map_convert[of "rev M"] by (simp add: rev_map)
lemma get_maximum_level_map_convert[simp]:
"get_maximum_level (map convert M) D = get_maximum_level M D"
by (induction D)
(auto simp add: get_maximum_level_plus)
lemma get_all_levels_of_decided_map_convert[simp]:
"get_all_levels_of_decided (map convert M) = (get_all_levels_of_decided M)"
by (induction M rule: ann_literal_list_induct) auto
text ‹Conversion function›
fun toS :: "cdcl⇩W_state_inv_st ⇒ nat cdcl⇩W_state" where
"toS (M, N, U, k, C) = (map convert M, mset (map mset N), mset (map mset U), k, convertC C)"
text ‹Definition an abstract type›
typedef cdcl⇩W_state_inv = "{S::cdcl⇩W_state_inv_st. cdcl⇩W_all_struct_inv (toS S)}"
morphisms rough_state_of state_of
proof
show "([],[], [], 0, None) ∈ {S. cdcl⇩W_all_struct_inv (toS S)}"
by (auto simp add: cdcl⇩W_all_struct_inv_def)
qed
instantiation cdcl⇩W_state_inv :: equal
begin
definition equal_cdcl⇩W_state_inv :: "cdcl⇩W_state_inv ⇒ cdcl⇩W_state_inv ⇒ bool" where
"equal_cdcl⇩W_state_inv S S' = (rough_state_of S = rough_state_of S')"
instance
by standard (simp add: rough_state_of_inject equal_cdcl⇩W_state_inv_def)
end
lemma lits_of_map_convert[simp]: "lits_of (map convert M) = lits_of M"
by (induction M rule: ann_literal_list_induct) simp_all
lemma undefined_lit_map_convert[iff]:
"undefined_lit (map convert M) L ⟷ undefined_lit M L"
by (auto simp add: Decided_Propagated_in_iff_in_lits_of)
lemma true_annot_map_convert[simp]: "map convert M ⊨a N ⟷ M ⊨a N"
by (induction M rule: ann_literal_list_induct) (simp_all add: true_annot_def)
lemma true_annots_map_convert[simp]: "map convert M ⊨as N ⟷ M ⊨as N"
unfolding true_annots_def by auto
lemmas propagateE
lemma find_first_unit_clause_some_is_propagate:
assumes H: "find_first_unit_clause (N @ U) M = Some (L, C)"
shows "propagate (toS (M, N, U, k, None)) (toS (Propagated L C # M, N, U, k, None))"
using assms
by (auto dest!: find_first_unit_clause_some simp add: propagate.simps
intro!: exI[of _ "mset C - {#L#}"])
subsubsection ‹The Transitions›
paragraph ‹Propagate›
definition do_propagate_step where
"do_propagate_step S =
(case S of
(M, N, U, k, None) ⇒
(case find_first_unit_clause (N @ U) M of
Some (L, C) ⇒ (Propagated L C # M, N, U, k, None)
| None ⇒ (M, N, U, k, None))
| S ⇒ S)"
lemma do_propgate_step:
"do_propagate_step S ≠ S ⟹ propagate (toS S) (toS (do_propagate_step S))"
apply (cases S, cases "conflicting S")
using find_first_unit_clause_some_is_propagate[of "clss S" "learned_clss S" "trail S" _ _
"backtrack_lvl S"]
by (auto simp add: do_propagate_step_def split: option.splits)
lemma do_propagate_step_option[simp]:
"conflicting S ≠ None ⟹ do_propagate_step S = S"
unfolding do_propagate_step_def by (cases S, cases "conflicting S") auto
lemma do_propagate_step_no_step:
assumes dist: "∀c∈set (clss S @ learned_clss S). distinct c" and
prop_step: "do_propagate_step S = S"
shows "no_step propagate (toS S)"
proof (standard, standard)
fix T
assume "propagate (toS S) T"
then obtain M N U k C L where
toSS: "toS S = (M, N, U, k, None)" and
T: "T = (Propagated L (C + {#L#}) # M, N, U, k, None)" and
MC: "M ⊨as CNot C" and
undef: "undefined_lit M L" and
CL: "C + {#L#} ∈# N + U"
apply - by (cases "toS S") auto
let ?M = "trail S"
let ?N = "clss S"
let ?U = "learned_clss S"
let ?k = "backtrack_lvl S"
let ?D = "None"
have S: "S = (?M, ?N, ?U, ?k, ?D)"
using toSS by (cases S, cases "conflicting S") simp_all
have S: "toS S = toS (?M, ?N, ?U, ?k, ?D)"
unfolding S[symmetric] by simp
have
M: "M = map convert ?M" and
N: "N = mset (map mset ?N)" and
U: "U = mset (map mset ?U)"
using toSS[unfolded S] by auto
obtain D where
DCL: "mset D = C + {#L#}" and
D: "D ∈ set (?N @ ?U)"
using CL unfolding N U by auto
obtain C' L' where
setD: "set D = set (L' # C')" and
C': "mset C' = C" and
L: "L = L'"
using DCL by (metis ex_mset mset.simps(2) mset_eq_setD)
have "find_first_unit_clause (?N @ ?U) ?M ≠ None"
apply (rule dist find_first_unit_clause_none[of D "?N @ ?U" ?M L, OF _ D ])
using D assms(1) apply auto[1]
using MC setD DCL M MC unfolding C'[symmetric] apply auto[1]
using M undef apply auto[1]
unfolding setD L by auto
then show False using prop_step S unfolding do_propagate_step_def by (cases S) auto
qed
paragraph ‹Conflict›
fun find_conflict where
"find_conflict M [] = None" |
"find_conflict M (N # Ns) = (if (∀c ∈ set N. -c ∈ lits_of M) then Some N else find_conflict M Ns)"
lemma find_conflict_Some:
"find_conflict M Ns = Some N ⟹ N ∈ set Ns ∧ M ⊨as CNot (mset N)"
by (induction Ns rule: find_conflict.induct)
(auto split: split_if_asm)
lemma find_conflict_None:
"find_conflict M Ns = None ⟷ (∀N ∈ set Ns. ¬M ⊨as CNot (mset N))"
by (induction Ns) auto
lemma find_conflict_None_no_confl:
"find_conflict M (N@U) = None ⟷ no_step conflict (toS (M, N, U, k, None))"
by (auto simp add: find_conflict_None conflict.simps)
definition do_conflict_step where
"do_conflict_step S =
(case S of
(M, N, U, k, None) ⇒
(case find_conflict M (N @ U) of
Some a ⇒ (M, N, U, k, Some a)
| None ⇒ (M, N, U, k, None))
| S ⇒ S)"
lemma do_conflict_step:
"do_conflict_step S ≠ S ⟹ conflict (toS S) (toS (do_conflict_step S))"
apply (cases S, cases "conflicting S")
unfolding conflict.simps do_conflict_step_def
by (auto dest!:find_conflict_Some split: option.splits)
lemma do_conflict_step_no_step:
"do_conflict_step S = S ⟹ no_step conflict (toS S)"
apply (cases S, cases "conflicting S")
unfolding do_conflict_step_def
using find_conflict_None_no_confl[of "trail S" "clss S" "learned_clss S"
"backtrack_lvl S"]
by (auto split: option.splits)
lemma do_conflict_step_option[simp]:
"conflicting S ≠ None ⟹ do_conflict_step S = S"
unfolding do_conflict_step_def by (cases S, cases "conflicting S") auto
lemma do_conflict_step_conflicting[dest]:
"do_conflict_step S ≠ S ⟹ conflicting (do_conflict_step S) ≠ None"
unfolding do_conflict_step_def by (cases S, cases "conflicting S") (auto split: option.splits)
definition do_cp_step where
"do_cp_step S =
(do_propagate_step o do_conflict_step) S"
lemma cp_step_is_cdcl⇩W_cp:
assumes H: "do_cp_step S ≠ S"
shows "cdcl⇩W_cp (toS S) (toS (do_cp_step S))"
proof -
show ?thesis
proof (cases "do_conflict_step S ≠ S")
case True
then show ?thesis
by (auto simp add: do_conflict_step do_conflict_step_conflicting do_cp_step_def)
next
case False
then have confl[simp]: "do_conflict_step S = S" by simp
show ?thesis
proof (cases "do_propagate_step S = S")
case True
then show ?thesis
using H by (simp add: do_cp_step_def)
next
case False
let ?S = "toS S"
let ?T = "toS (do_propagate_step S)"
let ?U = "toS (do_conflict_step (do_propagate_step S))"
have propa: "propagate (toS S) ?T" using False do_propgate_step by blast
moreover have ns: "no_step conflict (toS S)" using confl do_conflict_step_no_step by blast
ultimately show ?thesis
using cdcl⇩W_cp.intros(2)[of ?S ?T] confl unfolding do_cp_step_def by auto
qed
qed
qed
lemma do_cp_step_eq_no_prop_no_confl:
"do_cp_step S = S ⟹ do_conflict_step S = S ∧ do_propagate_step S = S"
by (cases S, cases "conflicting S")
(auto simp add: do_conflict_step_def do_propagate_step_def do_cp_step_def split: option.splits)
lemma no_cdcl⇩W_cp_iff_no_propagate_no_conflict:
"no_step cdcl⇩W_cp S ⟷ no_step propagate S ∧ no_step conflict S"
by (auto simp: cdcl⇩W_cp.simps)
lemma do_cp_step_eq_no_step:
assumes H: "do_cp_step S = S" and "∀c ∈ set (clss S @ learned_clss S). distinct c"
shows "no_step cdcl⇩W_cp (toS S)"
unfolding no_cdcl⇩W_cp_iff_no_propagate_no_conflict
using assms apply (cases S, cases "conflicting S")
using do_propagate_step_no_step[of S]
by (auto dest!: do_cp_step_eq_no_prop_no_confl[simplified] do_conflict_step_no_step
split: option.splits)
lemma cdcl⇩W_cp_cdcl⇩W_st: "cdcl⇩W_cp S S' ⟹ cdcl⇩W⇧*⇧* S S'"
by (simp add: cdcl⇩W_cp_tranclp_cdcl⇩W tranclp_into_rtranclp)
lemma cdcl⇩W_cp_wf_all_inv:
"wf {(S', S::'v::linorder cdcl⇩W_state). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_cp S S'}"
(is "wf ?R")
proof (rule wf_bounded_measure[of _ "λS. card (atms_of_msu (clss S))+1"
"λS. length (trail S) + (if conflicting S = None then 0 else 1)"], goal_cases)
case (1 S S')
then have "cdcl⇩W_all_struct_inv S" and "cdcl⇩W_cp S S'" by auto
moreover then have "cdcl⇩W_all_struct_inv S'"
using rtranclp_cdcl⇩W_all_struct_inv_inv cdcl⇩W_cp_cdcl⇩W_st by blast
ultimately show ?case
by (auto simp:cdcl⇩W_cp.simps elim!: conflictE propagateE
dest: length_model_le_vars_all_inv)
qed
lemma cdcl⇩W_all_struct_inv_rough_state[simp]: "cdcl⇩W_all_struct_inv (toS (rough_state_of S))"
using rough_state_of by auto
lemma [simp]: "cdcl⇩W_all_struct_inv (toS S) ⟹ rough_state_of (state_of S) = S"
by (simp add: state_of_inverse)
lemma rough_state_of_state_of_do_cp_step[simp]:
"rough_state_of (state_of (do_cp_step (rough_state_of S))) = do_cp_step (rough_state_of S)"
proof -
have "cdcl⇩W_all_struct_inv (toS (do_cp_step (rough_state_of S)))"
apply (cases "do_cp_step (rough_state_of S) = (rough_state_of S)")
apply simp
using cp_step_is_cdcl⇩W_cp[of "rough_state_of S"] cdcl⇩W_all_struct_inv_rough_state[of S]
cdcl⇩W_cp_cdcl⇩W_st rtranclp_cdcl⇩W_all_struct_inv_inv by blast
then show ?thesis by auto
qed
paragraph ‹Skip›
fun do_skip_step :: "cdcl⇩W_state_inv_st ⇒ cdcl⇩W_state_inv_st" where
"do_skip_step (Propagated L C # Ls,N,U,k, Some D) =
(if -L ∉ set D ∧ D ≠ []
then (Ls, N, U, k, Some D)
else (Propagated L C #Ls, N, U, k, Some D))" |
"do_skip_step S = S"
lemma do_skip_step:
"do_skip_step S ≠ S ⟹ skip (toS S) (toS (do_skip_step S))"
apply (induction S rule: do_skip_step.induct)
by (auto simp add: skip.simps)
lemma do_skip_step_no:
"do_skip_step S = S ⟹ no_step skip (toS S)"
by (induction S rule: do_skip_step.induct)
(auto simp add: other split: split_if_asm)
lemma do_skip_step_trail_is_None[iff]:
"do_skip_step S = (a, b, c, d, None) ⟷ S = (a, b, c, d, None)"
by (cases S rule: do_skip_step.cases) auto
paragraph ‹Resolve›
fun maximum_level_code:: "'a literal list ⇒ ('a, nat, 'a literal list) ann_literal list ⇒ nat"
where
"maximum_level_code [] _ = 0" |
"maximum_level_code (L # Ls) M = max (get_level M L) (maximum_level_code Ls M)"
lemma maximum_level_code_eq_get_maximum_level[code, simp]:
"maximum_level_code D M = get_maximum_level M (mset D)"
by (induction D) (auto simp add: get_maximum_level_plus)
fun do_resolve_step :: "cdcl⇩W_state_inv_st ⇒ cdcl⇩W_state_inv_st" where
"do_resolve_step (Propagated L C # Ls, N, U, k, Some D) =
(if -L ∈ set D ∧ maximum_level_code (remove1 (-L) D) (Propagated L C # Ls) = k
then (Ls, N, U, k, Some (remdups (remove1 L C @ remove1 (-L) D)))
else (Propagated L C # Ls, N, U, k, Some D))" |
"do_resolve_step S = S"
lemma do_resolve_step:
"cdcl⇩W_all_struct_inv (toS S) ⟹ do_resolve_step S ≠ S
⟹ resolve (toS S) (toS (do_resolve_step S))"
proof (induction S rule: do_resolve_step.induct)
case (1 L C M N U k D)
then have
"- L ∈ set D" and
M: "maximum_level_code (remove1 (-L) D) (Propagated L C # M) = k"
by (cases "mset D - {#- L#} = {#}",
auto dest!: get_maximum_level_exists_lit_of_max_level[of _ "Propagated L C # M"]
split: split_if_asm)+
have "every_mark_is_a_conflict (toS (Propagated L C # M, N, U, k, Some D))"
using 1(1) unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def by fast
then have "L ∈ set C" by fastforce
then obtain C' where C: "mset C = C' + {#L#}"
by (metis add.commute in_multiset_in_set insert_DiffM)
obtain D' where D: "mset D = D' + {#-L#}"
using ‹- L ∈ set D› by (metis add.commute in_multiset_in_set insert_DiffM)
have D'L: "D' + {#- L#} - {#-L#} = D'" by (auto simp add: multiset_eq_iff)
have CL: "mset C - {#L#} + {#L#} = mset C" using ‹L ∈ set C› by (auto simp add: multiset_eq_iff)
have "get_maximum_level (Propagated L (C' + {#L#}) # map convert M) D' = k"
using M[simplified] unfolding maximum_level_code_eq_get_maximum_level C[symmetric] CL
by (metis D D'L convert.simps(1) get_maximum_level_map_convert list.simps(9))
then have
"resolve
(map convert (Propagated L C # M), mset `# mset N, mset `# mset U, k, Some (mset D))
(map convert M, mset `# mset N, mset `# mset U, k,
Some (((mset D - {#-L#}) #∪ (mset C - {#L#}))))"
unfolding resolve.simps
by (simp add: C D)
moreover have
"(map convert (Propagated L C # M), mset `# mset N, mset `# mset U, k, Some (mset D))
= toS (Propagated L C # M, N, U, k, Some D)"
by (auto simp: mset_map)
moreover
have "distinct_mset (mset C)" and "distinct_mset (mset D)"
using ‹cdcl⇩W_all_struct_inv (toS (Propagated L C # M, N, U, k, Some D))›
unfolding cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def
by auto
then have "(mset C - {#L#}) #∪ (mset D - {#- L#}) =
remdups_mset (mset C - {#L#} + (mset D - {#- L#}))"
by (auto simp: distinct_mset_rempdups_union_mset)
then have "(map convert M, mset `# mset N, mset `# mset U, k,
Some ((mset D - {#- L#}) #∪ (mset C - {#L#})))
= toS (do_resolve_step (Propagated L C # M, N, U, k, Some D))"
using ‹- L ∈ set D› M by (auto simp:ac_simps mset_map)
ultimately show ?case
by simp
qed auto
lemma do_resolve_step_no:
"do_resolve_step S = S ⟹ no_step resolve (toS S)"
apply (cases S; cases "hd (trail S)"; cases "conflicting S")
by (auto
elim!: resolveE split: split_if_asm
dest!: union_single_eq_member
simp del: in_multiset_in_set get_maximum_level_map_convert
simp: in_multiset_in_set[symmetric] get_maximum_level_map_convert[symmetric])
lemma rough_state_of_state_of_resolve[simp]:
"cdcl⇩W_all_struct_inv (toS S) ⟹ rough_state_of (state_of (do_resolve_step S)) = do_resolve_step S"
apply (rule state_of_inverse)
apply (cases "do_resolve_step S = S")
apply simp
by (blast dest: other resolve bj do_resolve_step cdcl⇩W_all_struct_inv_inv)
lemma do_resolve_step_trail_is_None[iff]:
"do_resolve_step S = (a, b, c, d, None) ⟷ S = (a, b, c, d, None)"
by (cases S rule: do_resolve_step.cases) auto
paragraph ‹Backjumping›
fun find_level_decomp where
"find_level_decomp M [] D k = None" |
"find_level_decomp M (L # Ls) D k =
(case (get_level M L, maximum_level_code (D @ Ls) M) of
(i, j) ⇒ if i = k ∧ j < i then Some (L, j) else find_level_decomp M Ls (L#D) k
)"
lemma find_level_decomp_some:
assumes "find_level_decomp M Ls D k = Some (L, j)"
shows "L ∈ set Ls ∧ get_maximum_level M (mset (remove1 L (Ls @ D))) = j ∧ get_level M L = k"
using assms
proof (induction Ls arbitrary: D)
case Nil
then show ?case by simp
next
case (Cons L' Ls) note IH = this(1) and H = this(2)
def find ≡ "(if get_level M L' ≠ k ∨ ¬ get_maximum_level M (mset D + mset Ls) < get_level M L'
then find_level_decomp M Ls (L' # D) k
else Some (L', get_maximum_level M (mset D + mset Ls)))"
have a1: "⋀D. find_level_decomp M Ls D k = Some (L, j) ⟹
L ∈ set Ls ∧ get_maximum_level M (mset Ls + mset D - {#L#}) = j ∧ get_level M L = k"
using IH by simp
have a2: "find = Some (L, j)"
using H unfolding find_def by (auto split: split_if_asm)
{ assume "Some (L', get_maximum_level M (mset D + mset Ls)) ≠ find"
then have f3: "L ∈ set Ls" and "get_maximum_level M (mset Ls + mset (L' # D) - {#L#}) = j"
using a1 IH a2 unfolding find_def by meson+
moreover then have "mset Ls + mset D - {#L#} + {#L'#} = {#L'#} + mset D + (mset Ls - {#L#})"
by (auto simp: ac_simps multiset_eq_iff Suc_leI)
ultimately have f4: "get_maximum_level M (mset Ls + mset D - {#L#} + {#L'#}) = j"
by (metis (no_types) diff_union_single_conv mem_set_multiset_eq mset.simps(2) union_commute)
} note f4 = this
have "{#L'#} + (mset Ls + mset D) = mset Ls + (mset D + {#L'#})"
by (auto simp: ac_simps)
then have
"(L = L' ⟶ get_maximum_level M (mset Ls + mset D) = j ∧ get_level M L' = k)" and
"(L ≠ L' ⟶ L ∈ set Ls ∧ get_maximum_level M (mset Ls + mset D - {#L#} + {#L'#}) = j ∧
get_level M L = k)"
using f4 a2 a1[of "L' # D"] unfolding find_def by (metis (no_types) add_diff_cancel_left'
mset.simps(2) option.inject prod.inject union_commute)+
then show ?case by simp
qed
lemma find_level_decomp_none:
assumes "find_level_decomp M Ls E k = None" and "mset (L#D) = mset (Ls @ E)"
shows "¬(L ∈ set Ls ∧ get_maximum_level M (mset D) < k ∧ k = get_level M L)"
using assms
proof (induction Ls arbitrary: E L D)
case Nil
then show ?case by simp
next
case (Cons L' Ls) note IH = this(1) and find_none = this(2) and LD = this(3)
have "mset D + {#L'#} = mset E + (mset Ls + {#L'#}) ⟹ mset D = mset E + mset Ls"
by (metis add_right_imp_eq union_assoc)
then show ?case
using find_none IH[of "L' # E" L D] LD by (auto simp add: ac_simps split: split_if_asm)
qed
fun bt_cut where
"bt_cut i (Propagated _ _ # Ls) = bt_cut i Ls" |
"bt_cut i (Decided K k # Ls) = (if k = Suc i then Some (Decided K k # Ls) else bt_cut i Ls)" |
"bt_cut i [] = None"
lemma bt_cut_some_decomp:
"bt_cut i M = Some M' ⟹ ∃K M2 M1. M = M2 @ M' ∧ M' = Decided K (i+1) # M1"
by (induction i M rule: bt_cut.induct) (auto split: split_if_asm)
lemma bt_cut_not_none: "M = M2 @ Decided K (Suc i) # M' ⟹ bt_cut i M ≠ None"
by (induction M2 arbitrary: M rule: ann_literal_list_induct) auto
lemma get_all_decided_decomposition_ex:
"∃N. (Decided K (Suc i) # M', N) ∈ set (get_all_decided_decomposition (M2@Decided K (Suc i) # M'))"
apply (induction M2 rule: ann_literal_list_induct)
apply auto[2]
by (rename_tac L m xs, case_tac "get_all_decided_decomposition (xs @ Decided K (Suc i) # M')")
auto
lemma bt_cut_in_get_all_decided_decomposition:
"bt_cut i M = Some M' ⟹ ∃M2. (M', M2) ∈ set (get_all_decided_decomposition M)"
by (auto dest!: bt_cut_some_decomp simp add: get_all_decided_decomposition_ex)
fun do_backtrack_step where
"do_backtrack_step (M, N, U, k, Some D) =
(case find_level_decomp M D [] k of
None ⇒ (M, N, U, k, Some D)
| Some (L, j) ⇒
(case bt_cut j M of
Some (Decided _ _ # Ls) ⇒ (Propagated L D # Ls, N, D # U, j, None)
| _ ⇒ (M, N, U, k, Some D))
)" |
"do_backtrack_step S = S"
lemma get_all_decided_decomposition_map_convert:
"(get_all_decided_decomposition (map convert M)) =
map (λ(a, b). (map convert a, map convert b)) (get_all_decided_decomposition M)"
apply (induction M rule: ann_literal_list_induct)
apply simp
by (rename_tac L l xs, case_tac "get_all_decided_decomposition xs"; auto)+
lemma do_backtrack_step:
assumes
db: "do_backtrack_step S ≠ S" and
inv: "cdcl⇩W_all_struct_inv (toS S)"
shows "backtrack (toS S) (toS (do_backtrack_step S))"
proof (cases S, cases "conflicting S", goal_cases)
case (1 M N U k E)
then show ?case using db by auto
next
case (2 M N U k E C) note S = this(1) and confl = this(2)
have E: "E = Some C" using S confl by auto
obtain L j where fd: "find_level_decomp M C [] k = Some (L, j)"
using db unfolding S E by (cases C) (auto split: split_if_asm option.splits)
have "L ∈ set C" and "get_maximum_level M (mset (remove1 L C)) = j" and
levL: "get_level M L = k"
using find_level_decomp_some[OF fd] by auto
obtain C' where C: "mset C = mset C' + {#L#}"
using ‹L ∈ set C› by (metis add.commute ex_mset in_multiset_in_set insert_DiffM)
obtain M⇩2 where M⇩2: "bt_cut j M = Some M⇩2"
using db fd unfolding S E by (auto split: option.splits)
obtain M1 K where M1: "M⇩2 = Decided K (Suc j) # M1"
using bt_cut_some_decomp[OF M⇩2] by (cases M⇩2) auto
obtain c where c: "M = c @ Decided K (Suc j) # M1"
using bt_cut_in_get_all_decided_decomposition[OF M⇩2]
unfolding M1 by fastforce
have "get_all_levels_of_decided (map convert M) = rev [1..<Suc k]"
using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def S by auto
from arg_cong[OF this, of "λa. Suc j ∈ set a"] have "j ≤ k" unfolding c by auto
have max_l_j: "maximum_level_code C' M = j"
using db fd M⇩2 C unfolding S E by (auto
split: option.splits list.splits ann_literal.splits
dest!: find_level_decomp_some)[1]
have "get_maximum_level M (mset C) ≥ k"
using ‹L ∈ set C› get_maximum_level_ge_get_level levL by blast
moreover have "get_maximum_level M (mset C) ≤ k"
using get_maximum_level_exists_lit_of_max_level[of "mset C" M] inv
cdcl⇩W_M_level_inv_get_level_le_backtrack_lvl[of "toS S"]
unfolding C cdcl⇩W_all_struct_inv_def S by (auto dest: sym[of "get_level _ _"])
ultimately have "get_maximum_level M (mset C) = k" by auto
obtain M2 where M2: "(M⇩2, M2) ∈ set (get_all_decided_decomposition M)"
using bt_cut_in_get_all_decided_decomposition[OF M⇩2] by metis
have H: "(reduce_trail_to (map convert M1)
(add_learned_cls (mset C' + {#L#})
(map convert M, mset (map mset N), mset (map mset U), j, None))) =
(map convert M1, mset (map mset N), {#mset C' + {#L#}#} + mset (map mset U), j, None)"
apply (subst state_conv[of "reduce_trail_to _ _"])
using M2 unfolding M1 by auto
have
"backtrack
(map convert M, mset `# mset N, mset `# mset U, k, Some (mset C))
(Propagated L (mset C) # map convert M1, mset `# mset N, mset `# mset U + {#mset C#}, j,
None)"
apply (rule backtrack_rule)
unfolding C apply simp
using Set.imageI[of "(M⇩2, M2)" "set (get_all_decided_decomposition M)"
"(λ(a, b). (map convert a, map convert b))"] M2
apply (auto simp: get_all_decided_decomposition_map_convert M1)[1]
using max_l_j levL ‹j ≤ k› apply (simp add: get_maximum_level_plus)
using C ‹get_maximum_level M (mset C) = k› levL apply auto[1]
using max_l_j apply simp
apply (cases "reduce_trail_to (map convert M1)
(add_learned_cls (mset C' + {#L#})
(map convert M, mset (map mset N), mset (map mset U), j, None))")
using M2 M1 H by (auto simp: ac_simps mset_map)
then show ?case
using M⇩2 fd unfolding S E M1 by (auto simp: mset_map)
obtain M2 where "(M⇩2, M2) ∈ set (get_all_decided_decomposition M)"
using bt_cut_in_get_all_decided_decomposition[OF M⇩2] by metis
qed
lemma do_backtrack_step_no:
assumes db: "do_backtrack_step S = S"
and inv: "cdcl⇩W_all_struct_inv (toS S)"
shows "no_step backtrack (toS S)"
proof (rule ccontr, cases S, cases "conflicting S", goal_cases)
case 1
then show ?case using db by (auto split: option.splits)
next
case (2 M N U k E C) note bt = this(1) and S = this(2) and confl = this(3)
obtain D L K b z M1 j where
levL: "get_level M L = get_maximum_level M (D + {#L#})" and
k: "k = get_maximum_level M (D + {#L#})" and
j: "j = get_maximum_level M D" and
CE: "convertC E = Some (D + {#L#})" and
decomp: "(z # M1, b) ∈ set (get_all_decided_decomposition M)" and
z: "Decided K (Suc j) = convert z" using bt unfolding S
by (auto split: option.splits elim!: backtrackE
simp: get_all_decided_decomposition_map_convert)
have z: "z = Decided K (Suc j)" using z by (cases z) auto
obtain c where c: "M = c @ b @ Decided K (Suc j) # M1"
using decomp unfolding z by blast
have "get_all_levels_of_decided (map convert M) = rev [1..<Suc k]"
using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def S by auto
from arg_cong[OF this, of "λa. Suc j ∈ set a"] have "k > j" unfolding c by auto
obtain C D' where
E: "E = Some C" and
C: "mset C = mset (L # D')"
using CE apply (cases E)
apply simp
by (metis ex_mset mset.simps(2) option.inject option.simps(9))
have D'D: "mset D' = D"
using C CE E by auto
have "find_level_decomp M C [] k ≠ None"
apply rule
apply (drule find_level_decomp_none[of _ _ _ _ L D'])
using C ‹k > j› mset_eq_setD unfolding k[symmetric] D'D j[symmetric] levL by fastforce+
then obtain L' j' where fd_some: "find_level_decomp M C [] k = Some (L', j')"
by (cases "find_level_decomp M C [] k") auto
have L': "L' = L"
proof (rule ccontr)
assume "¬ ?thesis"
then have "L' ∈# D"
by (metis C D'D fd_some find_level_decomp_some in_multiset_in_set insert_iff list.simps(15))
then have "get_level M L' ≤ get_maximum_level M D"
using get_maximum_level_ge_get_level by blast
then show False using ‹k > j› j find_level_decomp_some[OF fd_some] by auto
qed
then have j': "j' = j" using find_level_decomp_some[OF fd_some] j C D'D by auto
have btc_none: "bt_cut j M ≠ None"
apply (rule bt_cut_not_none[of M "_ @ _"])
using c by simp
show ?case using db unfolding S E
by (auto split: option.splits list.splits ann_literal.splits
simp add: fd_some L' j' btc_none
dest: bt_cut_some_decomp)
qed
lemma rough_state_of_state_of_backtrack[simp]:
assumes inv: "cdcl⇩W_all_struct_inv (toS S)"
shows "rough_state_of (state_of (do_backtrack_step S))= do_backtrack_step S"
proof (rule state_of_inverse)
have f2: "backtrack (toS S) (toS (do_backtrack_step S)) ∨ do_backtrack_step S = S"
using do_backtrack_step inv by blast
have "⋀p. ¬ cdcl⇩W_o (toS S) p ∨ cdcl⇩W_all_struct_inv p"
using inv cdcl⇩W_all_struct_inv_inv other by blast
then have "do_backtrack_step S = S ∨ cdcl⇩W_all_struct_inv (toS (do_backtrack_step S))"
using f2 by blast
then show "do_backtrack_step S ∈ {S. cdcl⇩W_all_struct_inv (toS S)}"
using inv by fastforce
qed
paragraph ‹Decide›
fun do_decide_step where
"do_decide_step (M, N, U, k, None) =
(case find_first_unused_var N (lits_of M) of
None ⇒ (M, N, U, k, None)
| Some L ⇒ (Decided L (Suc k) # M, N, U, k+1, None))" |
"do_decide_step S = S"
lemma do_decide_step:
"do_decide_step S ≠ S ⟹ decide (toS S) (toS (do_decide_step S))"
apply (cases S, cases "conflicting S")
defer
apply (auto split: option.splits simp add: decide.simps Decided_Propagated_in_iff_in_lits_of
dest: find_first_unused_var_undefined find_first_unused_var_Some
intro: atms_of_atms_of_ms_mono)[1]
proof -
fix a :: "(nat, nat, nat literal list) ann_literal list" and
b :: "nat literal list list" and c :: "nat literal list list" and
d :: nat and e :: "nat literal list option"
{
fix a :: "(nat, nat, nat literal list) ann_literal list" and
b :: "nat literal list list" and c :: "nat literal list list" and
d :: nat and x2 :: "nat literal" and m :: "nat literal list"
assume a1: "m ∈ set b"
assume "x2 ∈ set m"
then have f2: "atm_of x2 ∈ atms_of (mset m)"
by simp
have "⋀f. (f m::nat literal multiset) ∈ f ` set b"
using a1 by blast
then have "⋀f. (atms_of (f m)::nat set) ⊆ atms_of_ms (f ` set b)"
using atms_of_atms_of_ms_mono by blast
then have "⋀n f. (n::nat) ∈ atms_of_ms (f ` set b) ∨ n ∉ atms_of (f m)"
by (meson contra_subsetD)
then have "atm_of x2 ∈ atms_of_ms (mset ` set b)"
using f2 by blast
} note H = this
{
fix m :: "nat literal list" and x2
have "m ∈ set b ⟹ x2 ∈ set m ⟹ x2 ∉ lits_of a ⟹ - x2 ∉ lits_of a ⟹
∃aa∈set b. ¬ atm_of ` set aa ⊆ atm_of ` lits_of a"
by (meson atm_of_in_atm_of_set_in_uminus contra_subsetD rev_image_eqI)
} note H' = this
assume "do_decide_step S ≠ S" and
"S = (a, b, c, d, e)" and
"conflicting S = None"
then show "decide (toS S) (toS (do_decide_step S))"
using H H' by (auto split: option.splits simp: decide.simps Decided_Propagated_in_iff_in_lits_of
dest!: find_first_unused_var_Some)
qed
lemma do_decide_step_no:
"do_decide_step S = S ⟹ no_step decide (toS S)"
by (cases S, cases "conflicting S")
(fastforce simp: atms_of_ms_mset_unfold atm_of_eq_atm_of Decided_Propagated_in_iff_in_lits_of
split: option.splits)+
lemma rough_state_of_state_of_do_decide_step[simp]:
"cdcl⇩W_all_struct_inv (toS S) ⟹ rough_state_of (state_of (do_decide_step S)) = do_decide_step S"
proof (subst state_of_inverse, goal_cases)
case 1
then show ?case
by (cases "do_decide_step S = S")
(auto dest: do_decide_step decide other intro: cdcl⇩W_all_struct_inv_inv)
qed simp
lemma rough_state_of_state_of_do_skip_step[simp]:
"cdcl⇩W_all_struct_inv (toS S) ⟹ rough_state_of (state_of (do_skip_step S)) = do_skip_step S"
apply (subst state_of_inverse, cases "do_skip_step S = S")
apply simp
by (blast dest: other skip bj do_skip_step cdcl⇩W_all_struct_inv_inv)+
subsubsection ‹Code generation›
paragraph ‹Type definition›
text ‹There are two invariants: one while applying conflict and propagate and one for the other
rules›
declare rough_state_of_inverse[simp add]
definition Con where
"Con xs = state_of (if cdcl⇩W_all_struct_inv (toS (fst xs, snd xs)) then xs
else ([], [], [], 0, None))"
lemma [code abstype]:
"Con (rough_state_of S) = S"
using rough_state_of[of S] unfolding Con_def by simp
definition do_cp_step' where
"do_cp_step' S = state_of (do_cp_step (rough_state_of S))"
typedef cdcl⇩W_state_inv_from_init_state = "{S::cdcl⇩W_state_inv_st. cdcl⇩W_all_struct_inv (toS S)
∧ cdcl⇩W_stgy⇧*⇧* (S0_cdcl⇩W (clss (toS S))) (toS S)}"
morphisms rough_state_from_init_state_of state_from_init_state_of
proof
show "([],[], [], 0, None) ∈ {S. cdcl⇩W_all_struct_inv (toS S)
∧ cdcl⇩W_stgy⇧*⇧* (S0_cdcl⇩W (clss (toS S))) (toS S)}"
by (auto simp add: cdcl⇩W_all_struct_inv_def)
qed
instantiation cdcl⇩W_state_inv_from_init_state :: equal
begin
definition equal_cdcl⇩W_state_inv_from_init_state :: "cdcl⇩W_state_inv_from_init_state ⇒
cdcl⇩W_state_inv_from_init_state ⇒ bool" where
"equal_cdcl⇩W_state_inv_from_init_state S S' ⟷
(rough_state_from_init_state_of S = rough_state_from_init_state_of S')"
instance
by standard (simp add: rough_state_from_init_state_of_inject
equal_cdcl⇩W_state_inv_from_init_state_def)
end
definition ConI where
"ConI S = state_from_init_state_of (if cdcl⇩W_all_struct_inv (toS (fst S, snd S))
∧ cdcl⇩W_stgy⇧*⇧* (S0_cdcl⇩W (clss (toS S))) (toS S) then S else ([], [], [], 0, None))"
lemma [code abstype]:
"ConI (rough_state_from_init_state_of S) = S"
using rough_state_from_init_state_of[of S] unfolding ConI_def
by (simp add: rough_state_from_init_state_of_inverse)
definition id_of_I_to:: "cdcl⇩W_state_inv_from_init_state ⇒ cdcl⇩W_state_inv" where
"id_of_I_to S = state_of (rough_state_from_init_state_of S)"
lemma [code abstract]:
"rough_state_of (id_of_I_to S) = rough_state_from_init_state_of S"
unfolding id_of_I_to_def using rough_state_from_init_state_of by auto
paragraph ‹Conflict and Propagate›
function do_full1_cp_step :: "cdcl⇩W_state_inv ⇒ cdcl⇩W_state_inv" where
"do_full1_cp_step S =
(let S' = do_cp_step' S in
if S = S' then S else do_full1_cp_step S')"
by auto
termination
proof (relation "{(T', T). (rough_state_of T', rough_state_of T) ∈ {(S', S).
(toS S', toS S) ∈ {(S', S). cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_cp S S'}}}", goal_cases)
case 1
show ?case
using wf_if_measure_f[OF wf_if_measure_f[OF cdcl⇩W_cp_wf_all_inv, of "toS"], of rough_state_of] .
next
case (2 S' S)
then show ?case
unfolding do_cp_step'_def
apply simp
by (metis cp_step_is_cdcl⇩W_cp rough_state_of_inverse)
qed
lemma do_full1_cp_step_fix_point_of_do_full1_cp_step:
"do_cp_step(rough_state_of (do_full1_cp_step S)) = (rough_state_of (do_full1_cp_step S))"
by (rule do_full1_cp_step.induct[of "λS. do_cp_step(rough_state_of (do_full1_cp_step S))
= (rough_state_of (do_full1_cp_step S))"])
(metis (full_types) do_full1_cp_step.elims rough_state_of_state_of_do_cp_step do_cp_step'_def)
lemma in_clauses_rough_state_of_is_distinct:
"c∈set (clss (rough_state_of S) @ learned_clss (rough_state_of S)) ⟹ distinct c"
apply (cases "rough_state_of S")
using rough_state_of[of S] by (auto simp add: distinct_mset_set_distinct cdcl⇩W_all_struct_inv_def
distinct_cdcl⇩W_state_def)
lemma do_full1_cp_step_full:
"full cdcl⇩W_cp (toS (rough_state_of S))
(toS (rough_state_of (do_full1_cp_step S)))"
unfolding full_def
proof (rule conjI, induction S rule: do_full1_cp_step.induct)
case (1 S)
then have f1:
"cdcl⇩W_cp⇧*⇧* (toS (do_cp_step (rough_state_of S))) (
toS (rough_state_of (do_full1_cp_step (state_of (do_cp_step (rough_state_of S))))))
∨ state_of (do_cp_step (rough_state_of S)) = S"
using do_cp_step'_def rough_state_of_state_of_do_cp_step by fastforce
have f2: "⋀c. (if c = state_of (do_cp_step (rough_state_of c))
then c else do_full1_cp_step (state_of (do_cp_step (rough_state_of c))))
= do_full1_cp_step c"
by (metis (full_types) do_cp_step'_def do_full1_cp_step.simps)
have f3: "¬ cdcl⇩W_cp (toS (rough_state_of S)) (toS (do_cp_step (rough_state_of S)))
∨ state_of (do_cp_step (rough_state_of S)) = S
∨ cdcl⇩W_cp⇧+⇧+ (toS (rough_state_of S))
(toS (rough_state_of (do_full1_cp_step (state_of (do_cp_step (rough_state_of S))))))"
using f1 by (meson rtranclp_into_tranclp2)
{ assume "do_full1_cp_step S ≠ S"
then have "do_cp_step (rough_state_of S) = rough_state_of S
⟶ cdcl⇩W_cp⇧*⇧* (toS (rough_state_of S)) (toS (rough_state_of (do_full1_cp_step S)))
∨ do_cp_step (rough_state_of S) ≠ rough_state_of S
∧ state_of (do_cp_step (rough_state_of S)) ≠ S"
using f2 f1 by (metis (no_types))
then have "do_cp_step (rough_state_of S) ≠ rough_state_of S
∧ state_of (do_cp_step (rough_state_of S)) ≠ S
∨ cdcl⇩W_cp⇧*⇧* (toS (rough_state_of S)) (toS (rough_state_of (do_full1_cp_step S)))"
by (metis rough_state_of_state_of_do_cp_step)
then have "cdcl⇩W_cp⇧*⇧* (toS (rough_state_of S)) (toS (rough_state_of (do_full1_cp_step S)))"
using f3 f2 by (metis (no_types) cp_step_is_cdcl⇩W_cp tranclp_into_rtranclp) }
then show ?case
by fastforce
next
show "no_step cdcl⇩W_cp (toS (rough_state_of (do_full1_cp_step S)))"
apply (rule do_cp_step_eq_no_step[OF do_full1_cp_step_fix_point_of_do_full1_cp_step[of S]])
using in_clauses_rough_state_of_is_distinct unfolding do_cp_step'_def by blast
qed
lemma [code abstract]:
"rough_state_of (do_cp_step' S) = do_cp_step (rough_state_of S)"
unfolding do_cp_step'_def by auto
paragraph ‹The other rules›
fun do_other_step where
"do_other_step S =
(let T = do_skip_step S in
if T ≠ S
then T
else
(let U = do_resolve_step T in
if U ≠ T
then U else
(let V = do_backtrack_step U in
if V ≠ U then V else do_decide_step V)))"
lemma do_other_step:
assumes inv: "cdcl⇩W_all_struct_inv (toS S)" and
st: "do_other_step S ≠ S"
shows "cdcl⇩W_o (toS S) (toS (do_other_step S))"
using st inv by (auto split: split_if_asm
simp add: Let_def
intro: do_skip_step do_resolve_step do_backtrack_step do_decide_step)
lemma do_other_step_no:
assumes inv: "cdcl⇩W_all_struct_inv (toS S)" and
st: "do_other_step S = S"
shows "no_step cdcl⇩W_o (toS S)"
using st inv by (auto split: split_if_asm elim: cdcl⇩W_bjE
simp add: Let_def cdcl⇩W_bj.simps elim!: cdcl⇩W_o.cases
dest!: do_skip_step_no do_resolve_step_no do_backtrack_step_no do_decide_step_no)
lemma rough_state_of_state_of_do_other_step[simp]:
"rough_state_of (state_of (do_other_step (rough_state_of S))) = do_other_step (rough_state_of S)"
proof (cases "do_other_step (rough_state_of S) = rough_state_of S")
case True
then show ?thesis by simp
next
case False
have "cdcl⇩W_o (toS (rough_state_of S)) (toS (do_other_step (rough_state_of S)))"
by (metis False cdcl⇩W_all_struct_inv_rough_state do_other_step["of" "rough_state_of S"])
then have "cdcl⇩W_all_struct_inv (toS (do_other_step (rough_state_of S)))"
using cdcl⇩W_all_struct_inv_inv cdcl⇩W_all_struct_inv_rough_state other by blast
then show ?thesis
by (simp add: CollectI state_of_inverse)
qed
definition do_other_step' where
"do_other_step' S =
state_of (do_other_step (rough_state_of S))"
lemma rough_state_of_do_other_step'[code abstract]:
"rough_state_of (do_other_step' S) = do_other_step (rough_state_of S)"
apply (cases "do_other_step (rough_state_of S) = rough_state_of S")
unfolding do_other_step'_def apply simp
using do_other_step[of "rough_state_of S"] by (auto intro: cdcl⇩W_all_struct_inv_inv
cdcl⇩W_all_struct_inv_rough_state other state_of_inverse)
definition do_cdcl⇩W_stgy_step where
"do_cdcl⇩W_stgy_step S =
(let T = do_full1_cp_step S in
if T ≠ S
then T
else
(let U = (do_other_step' T) in
(do_full1_cp_step U))) "
definition do_cdcl⇩W_stgy_step' where
"do_cdcl⇩W_stgy_step' S = state_from_init_state_of (rough_state_of (do_cdcl⇩W_stgy_step (id_of_I_to S)))"
lemma toS_do_full1_cp_step_not_eq: "do_full1_cp_step S ≠ S ⟹
toS (rough_state_of S) ≠ toS (rough_state_of (do_full1_cp_step S))"
proof -
assume a1: "do_full1_cp_step S ≠ S"
then have "S ≠ do_cp_step' S"
by fastforce
then show ?thesis
by (metis (no_types) cp_step_is_cdcl⇩W_cp do_cp_step'_def do_cp_step_eq_no_step
do_full1_cp_step_fix_point_of_do_full1_cp_step in_clauses_rough_state_of_is_distinct
rough_state_of_inverse)
qed
text ‹@{term do_full1_cp_step} should not be unfolded anymore:›
declare do_full1_cp_step.simps[simp del]
paragraph ‹Correction of the transformation›
lemma do_cdcl⇩W_stgy_step:
assumes "do_cdcl⇩W_stgy_step S ≠ S"
shows "cdcl⇩W_stgy (toS (rough_state_of S)) (toS (rough_state_of (do_cdcl⇩W_stgy_step S)))"
proof (cases "do_full1_cp_step S = S")
case False
then show ?thesis
using assms do_full1_cp_step_full[of S] unfolding full_unfold do_cdcl⇩W_stgy_step_def
by (auto intro!: cdcl⇩W_stgy.intros dest: toS_do_full1_cp_step_not_eq)
next
case True
have "cdcl⇩W_o (toS (rough_state_of S)) (toS (rough_state_of (do_other_step' S)))"
by (smt True assms cdcl⇩W_all_struct_inv_rough_state do_cdcl⇩W_stgy_step_def do_other_step
rough_state_of_do_other_step' rough_state_of_inverse)
moreover
have
np: "no_step propagate (toS (rough_state_of S))" and
nc: "no_step conflict (toS (rough_state_of S))"
apply (metis True do_cp_step_eq_no_prop_no_confl
do_full1_cp_step_fix_point_of_do_full1_cp_step do_propagate_step_no_step
in_clauses_rough_state_of_is_distinct)
by (metis True do_conflict_step_no_step do_cp_step_eq_no_prop_no_confl
do_full1_cp_step_fix_point_of_do_full1_cp_step)
then have "no_step cdcl⇩W_cp (toS (rough_state_of S))"
by (simp add: cdcl⇩W_cp.simps)
moreover have "full cdcl⇩W_cp (toS (rough_state_of (do_other_step' S)))
(toS (rough_state_of (do_full1_cp_step (do_other_step' S))))"
using do_full1_cp_step_full by auto
ultimately show ?thesis
using assms True unfolding do_cdcl⇩W_stgy_step_def
by (auto intro!: cdcl⇩W_stgy.other' dest: toS_do_full1_cp_step_not_eq)
qed
lemma length_trail_toS[simp]:
"length (trail (toS S)) = length (trail S)"
by (cases S) auto
lemma conflicting_noTrue_iff_toS[simp]:
"conflicting (toS S) ≠ None ⟷ conflicting S ≠ None"
by (cases S) auto
lemma trail_toS_neq_imp_trail_neq:
"trail (toS S) ≠ trail (toS S') ⟹ trail S ≠ trail S'"
by (cases S, cases S') auto
lemma do_skip_step_trail_changed_or_conflict:
assumes d: "do_other_step S ≠ S"
and inv: "cdcl⇩W_all_struct_inv (toS S)"
shows "trail S ≠ trail (do_other_step S)"
proof -
have M: "⋀M K M1 c. M = c @ K # M1 ⟹ Suc (length M1) ≤ length M"
by auto
have "cdcl⇩W_M_level_inv (toS S)"
using inv unfolding cdcl⇩W_all_struct_inv_def by auto
have "cdcl⇩W_o (toS S) (toS (do_other_step S))" using do_other_step[OF inv d] .
then show ?thesis
using ‹cdcl⇩W_M_level_inv (toS S)›
proof (induction "toS (do_other_step S)" rule: cdcl⇩W_o_induct_lev2)
case decide
then show ?thesis
by (auto simp add: trail_toS_neq_imp_trail_neq)[]
next
case (skip)
then show ?case
by (cases S; cases "do_other_step S") force
next
case (resolve)
then show ?case
by (cases S, cases "do_other_step S") force
next
case (backtrack K i M1 M2 L D) note decomp = this(1) and confl_S = this(3) and undef = this(6)
and U = this(7)
have [simp]: "cons_trail (Propagated L (D + {#L#}))
(reduce_trail_to M1
(add_learned_cls (D + {#L#})
(update_backtrack_lvl (get_maximum_level (trail (toS S)) D)
(update_conflicting None (toS S)))))
=
(Propagated L (D + {#L#})# M1,mset (map mset (clss S)),
{#D + {#L#}#} + mset (map mset (learned_clss S)),
get_maximum_level (trail (toS S)) D, None)"
apply (subst state_conv[of "cons_trail _ _"])
using decomp undef by (cases S) auto
then show ?case
apply (cases "do_other_step S")
apply (auto split: split_if_asm simp: Let_def)
apply (cases S rule: do_skip_step.cases; auto split: split_if_asm)
apply (cases S rule: do_skip_step.cases; auto split: split_if_asm)
apply (cases S rule: do_backtrack_step.cases;
auto split: split_if_asm option.splits list.splits ann_literal.splits
dest!: bt_cut_some_decomp simp: Let_def)
using d apply (cases S rule: do_decide_step.cases; auto split: option.splits)[]
done
qed
qed
lemma do_full1_cp_step_induct:
"(⋀S. (S ≠ do_cp_step' S ⟹ P (do_cp_step' S)) ⟹ P S) ⟹ P a0"
using do_full1_cp_step.induct by metis
lemma do_cp_step_neq_trail_increase:
"∃c. trail (do_cp_step S) = c @ trail S ∧(∀m ∈ set c. ¬ is_decided m)"
by (cases S, cases "conflicting S")
(auto simp add: do_cp_step_def do_conflict_step_def do_propagate_step_def split: option.splits)
lemma do_full1_cp_step_neq_trail_increase:
"∃c. trail (rough_state_of (do_full1_cp_step S)) = c @ trail (rough_state_of S)
∧ (∀m ∈ set c. ¬ is_decided m)"
apply (induction rule: do_full1_cp_step_induct)
apply (rename_tac S, case_tac "do_cp_step' S = S")
apply (simp add: do_full1_cp_step.simps)
by (smt Un_iff append_assoc do_cp_step'_def do_cp_step_neq_trail_increase do_full1_cp_step.simps
rough_state_of_state_of_do_cp_step set_append)
lemma do_cp_step_conflicting:
"conflicting (rough_state_of S) ≠ None ⟹ do_cp_step' S = S"
unfolding do_cp_step'_def do_cp_step_def by simp
lemma do_full1_cp_step_conflicting:
"conflicting (rough_state_of S) ≠ None ⟹ do_full1_cp_step S = S"
unfolding do_cp_step'_def do_cp_step_def
apply (induction rule: do_full1_cp_step_induct)
by (rename_tac S, case_tac "S ≠ do_cp_step' S")
(auto simp add: do_full1_cp_step.simps do_cp_step_conflicting)
lemma do_decide_step_not_conflicting_one_more_decide:
assumes
"conflicting S = None" and
"do_decide_step S ≠ S"
shows "Suc (length (filter is_decided (trail S)))
= length (filter is_decided (trail (do_decide_step S)))"
using assms unfolding do_other_step'_def
by (cases S) (auto simp: Let_def split: split_if_asm option.splits
dest!: find_first_unused_var_Some_not_all_incl)
lemma do_decide_step_not_conflicting_one_more_decide_bt:
assumes "conflicting S ≠ None" and
"do_decide_step S ≠ S"
shows "length (filter is_decided (trail S)) < length (filter is_decided (trail (do_decide_step S)))"
using assms unfolding do_other_step'_def by (cases S, cases "conflicting S")
(auto simp add: Let_def split: split_if_asm option.splits)
lemma do_other_step_not_conflicting_one_more_decide_bt:
assumes
"conflicting (rough_state_of S) ≠ None" and
"conflicting (rough_state_of (do_other_step' S)) = None" and
"do_other_step' S ≠ S"
shows "length (filter is_decided (trail (rough_state_of S)))
> length (filter is_decided (trail (rough_state_of (do_other_step' S))))"
proof (cases S, goal_cases)
case (1 y) note S = this(1) and inv = this(2)
obtain M N U k E where y: "y = (M, N, U, k, Some E)"
using assms(1) S inv by (cases y, cases "conflicting y") auto
have M: "rough_state_of (state_of (M, N, U, k, Some E)) = (M, N, U, k, Some E)"
using inv y by (auto simp add: state_of_inverse)
have bt: "do_other_step' S = state_of (do_backtrack_step (rough_state_of S))"
proof (cases "rough_state_of S" rule: do_decide_step.cases)
case 1
then show ?thesis
using assms(1,2) by auto[]
next
case (2 v vb vd vf vh)
have f3: "⋀c. (if do_skip_step (rough_state_of c) ≠ rough_state_of c
then do_skip_step (rough_state_of c)
else if do_resolve_step (do_skip_step (rough_state_of c)) ≠ do_skip_step (rough_state_of c)
then do_resolve_step (do_skip_step (rough_state_of c))
else if do_backtrack_step (do_resolve_step (do_skip_step (rough_state_of c)))
≠ do_resolve_step (do_skip_step (rough_state_of c))
then do_backtrack_step (do_resolve_step (do_skip_step (rough_state_of c)))
else do_decide_step (do_backtrack_step (do_resolve_step
(do_skip_step (rough_state_of c)))))
= rough_state_of (do_other_step' c)"
by (simp add: rough_state_of_do_other_step')
have "(trail (rough_state_of (do_other_step' S)), clss (rough_state_of (do_other_step' S)),
learned_clss (rough_state_of (do_other_step' S)),
backtrack_lvl (rough_state_of (do_other_step' S)), None)
= rough_state_of (do_other_step' S)"
using assms(2) by (metis (no_types) state_conv)
then show ?thesis
using f3 2 by (metis (no_types) do_decide_step.simps(2) do_resolve_step_trail_is_None
do_skip_step_trail_is_None rough_state_of_inverse)
qed
show ?case
using assms(2) S unfolding bt y inv
apply simp
by (auto simp add: M bt_cut_not_none
split: option.splits
dest!: bt_cut_some_decomp)
qed
lemma do_other_step_not_conflicting_one_more_decide:
assumes "conflicting (rough_state_of S) = None" and
"do_other_step' S ≠ S"
shows "1 + length (filter is_decided (trail (rough_state_of S)))
= length (filter is_decided (trail (rough_state_of (do_other_step' S))))"
proof (cases S, goal_cases)
case (1 y) note S = this(1) and inv = this(2)
obtain M N U k where y: "y = (M, N, U, k, None)" using assms(1) S inv by (cases y) auto
have M: "rough_state_of (state_of (M, N, U, k, None)) = (M, N, U, k, None)"
using inv y by (auto simp add: state_of_inverse)
have "state_of (do_decide_step (M, N, U, k, None)) ≠ state_of (M, N, U, k, None)"
using assms(2) unfolding do_other_step'_def y inv S by (auto simp add: M)
then have f4: "do_skip_step (rough_state_of S) = rough_state_of S"
unfolding S M y by (metis (full_types) do_skip_step.simps(4))
have f5: "do_resolve_step (rough_state_of S) = rough_state_of S"
unfolding S M y by (metis (no_types) do_resolve_step.simps(4))
have f6: "do_backtrack_step (rough_state_of S) = rough_state_of S"
unfolding S M y by (metis (no_types) do_backtrack_step.simps(2))
have "do_other_step (rough_state_of S) ≠ rough_state_of S"
using assms(2) unfolding S M y do_other_step'_def by (metis (no_types))
then show ?case
using f6 f5 f4 by (simp add: assms(1) do_decide_step_not_conflicting_one_more_decide
do_other_step'_def)
qed
lemma rough_state_of_state_of_do_skip_step_rough_state_of[simp]:
"rough_state_of (state_of (do_skip_step (rough_state_of S))) = do_skip_step (rough_state_of S)"
by (smt do_other_step.simps rough_state_of_inverse rough_state_of_state_of_do_other_step)
lemma conflicting_do_resolve_step_iff[iff]:
"conflicting (do_resolve_step S) = None ⟷ conflicting S = None"
by (cases S rule: do_resolve_step.cases)
(auto simp add: Let_def split: option.splits)
lemma conflicting_do_skip_step_iff[iff]:
"conflicting (do_skip_step S) = None ⟷ conflicting S = None"
by (cases S rule: do_skip_step.cases)
(auto simp add: Let_def split: option.splits)
lemma conflicting_do_decide_step_iff[iff]:
"conflicting (do_decide_step S) = None ⟷ conflicting S = None"
by (cases S rule: do_decide_step.cases)
(auto simp add: Let_def split: option.splits)
lemma conflicting_do_backtrack_step_imp[simp]:
"do_backtrack_step S ≠ S ⟹ conflicting (do_backtrack_step S) = None"
by (cases S rule: do_backtrack_step.cases)
(auto simp add: Let_def split: list.splits option.splits ann_literal.splits)
lemma do_skip_step_eq_iff_trail_eq:
"do_skip_step S = S ⟷ trail (do_skip_step S) = trail S"
by (cases S rule: do_skip_step.cases) auto
lemma do_decide_step_eq_iff_trail_eq:
"do_decide_step S = S ⟷ trail (do_decide_step S) = trail S"
by (cases S rule: do_decide_step.cases) (auto split: option.split)
lemma do_backtrack_step_eq_iff_trail_eq:
"do_backtrack_step S = S ⟷ trail (do_backtrack_step S) = trail S"
by (cases S rule: do_backtrack_step.cases)
(auto split: option.split list.splits ann_literal.splits
dest!: bt_cut_in_get_all_decided_decomposition)
lemma do_resolve_step_eq_iff_trail_eq:
"do_resolve_step S = S ⟷ trail (do_resolve_step S) = trail S"
by (cases S rule: do_resolve_step.cases) auto
lemma do_other_step_eq_iff_trail_eq:
"trail (do_other_step S) = trail S ⟷ do_other_step S = S"
by (auto simp add: Let_def do_skip_step_eq_iff_trail_eq[symmetric]
do_decide_step_eq_iff_trail_eq[symmetric] do_backtrack_step_eq_iff_trail_eq[symmetric]
do_resolve_step_eq_iff_trail_eq[symmetric])
lemma do_full1_cp_step_do_other_step'_normal_form[dest!]:
assumes H: "do_full1_cp_step (do_other_step' S) = S"
shows "do_other_step' S = S ∧ do_full1_cp_step S = S"
proof -
let ?T = "do_other_step' S"
{ assume confl: "conflicting (rough_state_of ?T) ≠ None"
then have tr: "trail (rough_state_of (do_full1_cp_step ?T)) = trail (rough_state_of ?T)"
using do_full1_cp_step_conflicting by auto
have "trail (rough_state_of (do_full1_cp_step (do_other_step' S))) = trail (rough_state_of S)"
using arg_cong[OF H, of "λS. trail (rough_state_of S)"] .
then have "trail (rough_state_of (do_other_step' S)) = trail (rough_state_of S)"
by (auto simp add: do_full1_cp_step_conflicting confl)
then have "do_other_step' S = S"
by (simp add: do_other_step_eq_iff_trail_eq do_other_step'_def
del: do_other_step.simps)
}
moreover {
assume eq[simp]: "do_other_step' S = S"
obtain c where c: "trail (rough_state_of (do_full1_cp_step S)) = c @ trail (rough_state_of S)"
using do_full1_cp_step_neq_trail_increase by auto
moreover have "trail (rough_state_of (do_full1_cp_step S)) = trail (rough_state_of S)"
using arg_cong[OF H, of "λS. trail (rough_state_of S)"] by simp
finally have "c = []" by blast
then have "do_full1_cp_step S = S" using assms by auto
}
moreover {
assume confl: "conflicting (rough_state_of ?T) = None" and neq: "do_other_step' S ≠ S"
obtain c where
c: "trail (rough_state_of (do_full1_cp_step ?T)) = c @ trail (rough_state_of ?T)" and
nm: "∀m∈set c. ¬ is_decided m"
using do_full1_cp_step_neq_trail_increase by auto
have "length (filter is_decided (trail (rough_state_of (do_full1_cp_step ?T))))
= length (filter is_decided (trail (rough_state_of ?T)))" using nm unfolding c by force
moreover have "length (filter is_decided (trail (rough_state_of S)))
≠ length (filter is_decided (trail (rough_state_of ?T)))"
using do_other_step_not_conflicting_one_more_decide[OF _ neq]
do_other_step_not_conflicting_one_more_decide_bt[of S, OF _ confl neq]
by linarith
finally have False unfolding H by blast
}
ultimately show ?thesis by blast
qed
lemma do_cdcl⇩W_stgy_step_no:
assumes S: "do_cdcl⇩W_stgy_step S = S"
shows "no_step cdcl⇩W_stgy (toS (rough_state_of S))"
proof -
{
fix S'
assume "full1 cdcl⇩W_cp (toS (rough_state_of S)) S'"
then have False
using do_full1_cp_step_full[of S] unfolding full_def S rtranclp_unfold full1_def
by (smt assms do_cdcl⇩W_stgy_step_def tranclpD)
}
moreover {
fix S' S''
assume " cdcl⇩W_o (toS (rough_state_of S)) S'" and
"no_step propagate (toS (rough_state_of S))" and
"no_step conflict (toS (rough_state_of S))" and
"full cdcl⇩W_cp S' S''"
then have False
using assms unfolding do_cdcl⇩W_stgy_step_def
by (smt cdcl⇩W_all_struct_inv_rough_state do_full1_cp_step_do_other_step'_normal_form
do_other_step_no rough_state_of_do_other_step')
}
ultimately show ?thesis using assms by (force simp: cdcl⇩W_cp.simps cdcl⇩W_stgy.simps)
qed
lemma toS_rough_state_of_state_of_rough_state_from_init_state_of[simp]:
"toS (rough_state_of (state_of (rough_state_from_init_state_of S)))
= toS (rough_state_from_init_state_of S)"
using rough_state_from_init_state_of[of S] by (auto simp add: state_of_inverse)
lemma cdcl⇩W_cp_is_rtranclp_cdcl⇩W: "cdcl⇩W_cp S T ⟹ cdcl⇩W⇧*⇧* S T"
apply (induction rule: cdcl⇩W_cp.induct)
using conflict apply blast
using propagate by blast
lemma rtranclp_cdcl⇩W_cp_is_rtranclp_cdcl⇩W: "cdcl⇩W_cp⇧*⇧* S T ⟹ cdcl⇩W⇧*⇧* S T"
apply (induction rule: rtranclp_induct)
apply simp
by (fastforce dest!: cdcl⇩W_cp_is_rtranclp_cdcl⇩W)
lemma cdcl⇩W_stgy_is_rtranclp_cdcl⇩W:
"cdcl⇩W_stgy S T ⟹ cdcl⇩W⇧*⇧* S T"
apply (induction rule: cdcl⇩W_stgy.induct)
using cdcl⇩W_stgy.conflict' rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W apply blast
unfolding full_def by (fastforce dest!:other rtranclp_cdcl⇩W_cp_is_rtranclp_cdcl⇩W)
lemma cdcl⇩W_stgy_init_clss: "cdcl⇩W_stgy S T ⟹ cdcl⇩W_M_level_inv S ⟹ clss S = clss T"
using rtranclp_cdcl⇩W_init_clss cdcl⇩W_stgy_is_rtranclp_cdcl⇩W by fast
lemma clauses_toS_rough_state_of_do_cdcl⇩W_stgy_step[simp]:
"clss (toS (rough_state_of (do_cdcl⇩W_stgy_step (state_of (rough_state_from_init_state_of S)))))
= clss (toS (rough_state_from_init_state_of S))" (is "_ = clss (toS ?S)")
apply (cases "do_cdcl⇩W_stgy_step (state_of ?S) = state_of ?S")
apply simp
by (smt cdcl⇩W_all_struct_inv_def cdcl⇩W_all_struct_inv_rough_state cdcl⇩W_stgy_no_more_init_clss
do_cdcl⇩W_stgy_step toS_rough_state_of_state_of_rough_state_from_init_state_of)
lemma rough_state_from_init_state_of_do_cdcl⇩W_stgy_step'[code abstract]:
"rough_state_from_init_state_of (do_cdcl⇩W_stgy_step' S) =
rough_state_of (do_cdcl⇩W_stgy_step (id_of_I_to S))"
proof -
let ?S = "(rough_state_from_init_state_of S)"
have "cdcl⇩W_stgy⇧*⇧* (S0_cdcl⇩W (clss (toS (rough_state_from_init_state_of S))))
(toS (rough_state_from_init_state_of S))"
using rough_state_from_init_state_of[of S] by auto
moreover have "cdcl⇩W_stgy⇧*⇧*
(toS (rough_state_from_init_state_of S))
(toS (rough_state_of (do_cdcl⇩W_stgy_step
(state_of (rough_state_from_init_state_of S)))))"
using do_cdcl⇩W_stgy_step[of "state_of ?S"]
by (cases "do_cdcl⇩W_stgy_step (state_of ?S) = state_of ?S") auto
ultimately show ?thesis
unfolding do_cdcl⇩W_stgy_step'_def id_of_I_to_def
by (auto intro!: state_from_init_state_of_inverse)
qed
paragraph ‹All rules together›
function do_all_cdcl⇩W_stgy where
"do_all_cdcl⇩W_stgy S =
(let T = do_cdcl⇩W_stgy_step' S in
if T = S then S else do_all_cdcl⇩W_stgy T)"
by fast+
termination
proof (relation "{(T, S).
(cdcl⇩W_measure (toS (rough_state_from_init_state_of T)),
cdcl⇩W_measure (toS (rough_state_from_init_state_of S)))
∈ lexn {(a, b). a < b} 3}", goal_cases)
case 1
show ?case by (rule wf_if_measure_f) (auto intro!: wf_lexn wf_less)
next
case (2 S T) note T = this(1) and ST = this(2)
let ?S = "rough_state_from_init_state_of S"
have S: "cdcl⇩W_stgy⇧*⇧* (S0_cdcl⇩W (clss (toS ?S))) (toS ?S)"
using rough_state_from_init_state_of[of S] by auto
moreover have "cdcl⇩W_stgy (toS (rough_state_from_init_state_of S))
(toS (rough_state_from_init_state_of T))"
proof -
have "⋀c. rough_state_of (state_of (rough_state_from_init_state_of c)) =
rough_state_from_init_state_of c"
using rough_state_from_init_state_of by force
then have "do_cdcl⇩W_stgy_step (state_of (rough_state_from_init_state_of S))
≠ state_of (rough_state_from_init_state_of S)"
using ST T by (metis (no_types) id_of_I_to_def rough_state_from_init_state_of_inject
rough_state_from_init_state_of_do_cdcl⇩W_stgy_step')
then show ?thesis
using do_cdcl⇩W_stgy_step id_of_I_to_def rough_state_from_init_state_of_do_cdcl⇩W_stgy_step' T
by fastforce
qed
moreover
have "cdcl⇩W_all_struct_inv (toS (rough_state_from_init_state_of S))"
using rough_state_from_init_state_of[of S] by auto
then have "cdcl⇩W_all_struct_inv (S0_cdcl⇩W (clss (toS (rough_state_from_init_state_of S))))"
by (cases "rough_state_from_init_state_of S")
(auto simp add: cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def)
ultimately show ?case
by (auto intro!: cdcl⇩W_stgy_step_decreasing[of _ _ "S0_cdcl⇩W (clss (toS ?S))"]
simp del: cdcl⇩W_measure.simps)
qed
thm do_all_cdcl⇩W_stgy.induct
lemma do_all_cdcl⇩W_stgy_induct:
"(⋀S. (do_cdcl⇩W_stgy_step' S ≠ S ⟹ P (do_cdcl⇩W_stgy_step' S)) ⟹ P S) ⟹ P a0"
using do_all_cdcl⇩W_stgy.induct by metis
lemma no_step_cdcl⇩W_stgy_cdcl⇩W_all:
"no_step cdcl⇩W_stgy (toS (rough_state_from_init_state_of (do_all_cdcl⇩W_stgy S)))"
apply (induction S rule:do_all_cdcl⇩W_stgy_induct)
apply (rename_tac S, case_tac "do_cdcl⇩W_stgy_step' S ≠ S")
proof -
fix Sa :: cdcl⇩W_state_inv_from_init_state
assume a1: "¬ do_cdcl⇩W_stgy_step' Sa ≠ Sa"
{ fix pp
have "(if True then Sa else do_all_cdcl⇩W_stgy Sa) = do_all_cdcl⇩W_stgy Sa"
using a1 by auto
then have "¬ cdcl⇩W_stgy (toS (rough_state_from_init_state_of (do_all_cdcl⇩W_stgy Sa))) pp"
using a1 by (metis (no_types) do_cdcl⇩W_stgy_step_no id_of_I_to_def
rough_state_from_init_state_of_do_cdcl⇩W_stgy_step' rough_state_of_inverse) }
then show "no_step cdcl⇩W_stgy (toS (rough_state_from_init_state_of (do_all_cdcl⇩W_stgy Sa)))"
by fastforce
next
fix Sa :: cdcl⇩W_state_inv_from_init_state
assume a1: "do_cdcl⇩W_stgy_step' Sa ≠ Sa
⟹ no_step cdcl⇩W_stgy (toS (rough_state_from_init_state_of
(do_all_cdcl⇩W_stgy (do_cdcl⇩W_stgy_step' Sa))))"
assume a2: "do_cdcl⇩W_stgy_step' Sa ≠ Sa"
have "do_all_cdcl⇩W_stgy Sa = do_all_cdcl⇩W_stgy (do_cdcl⇩W_stgy_step' Sa)"
by (metis (full_types) do_all_cdcl⇩W_stgy.simps)
then show "no_step cdcl⇩W_stgy (toS (rough_state_from_init_state_of (do_all_cdcl⇩W_stgy Sa)))"
using a2 a1 by presburger
qed
lemma do_all_cdcl⇩W_stgy_is_rtranclp_cdcl⇩W_stgy:
"cdcl⇩W_stgy⇧*⇧* (toS (rough_state_from_init_state_of S))
(toS (rough_state_from_init_state_of (do_all_cdcl⇩W_stgy S)))"
proof (induction S rule: do_all_cdcl⇩W_stgy_induct)
case (1 S) note IH = this(1)
show ?case
proof (cases "do_cdcl⇩W_stgy_step' S = S")
case True
then show ?thesis by simp
next
case False
have f2: "do_cdcl⇩W_stgy_step (id_of_I_to S) = id_of_I_to S ⟶
rough_state_from_init_state_of (do_cdcl⇩W_stgy_step' S)
= rough_state_of (state_of (rough_state_from_init_state_of S))"
using id_of_I_to_def rough_state_from_init_state_of_do_cdcl⇩W_stgy_step' by presburger
have f3: "do_all_cdcl⇩W_stgy S = do_all_cdcl⇩W_stgy (do_cdcl⇩W_stgy_step' S)"
by (metis (full_types) do_all_cdcl⇩W_stgy.simps)
have "cdcl⇩W_stgy (toS (rough_state_from_init_state_of S))
(toS (rough_state_from_init_state_of (do_cdcl⇩W_stgy_step' S)))
= cdcl⇩W_stgy (toS (rough_state_of (id_of_I_to S)))
(toS (rough_state_of (do_cdcl⇩W_stgy_step (id_of_I_to S))))"
using id_of_I_to_def rough_state_from_init_state_of_do_cdcl⇩W_stgy_step'
toS_rough_state_of_state_of_rough_state_from_init_state_of by presburger
then show ?thesis
using f3 f2 IH do_cdcl⇩W_stgy_step by fastforce
qed
qed
text ‹Final theorem:›
lemma DPLL_tot_correct:
assumes
r: "rough_state_from_init_state_of (do_all_cdcl⇩W_stgy (state_from_init_state_of
(([], map remdups N, [], 0, None)))) = S" and
S: "(M', N', U', k, E) = toS S"
shows "(E ≠ Some {#} ∧ satisfiable (set (map mset N)))
∨ (E = Some {#} ∧ unsatisfiable (set (map mset N)))"
proof -
let ?N = "map remdups N"
have inv: "cdcl⇩W_all_struct_inv (toS ([], map remdups N, [], 0, None))"
unfolding cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def distinct_mset_set_def by auto
then have S0: "rough_state_of (state_of ([], map remdups N, [], 0, None))
= ([], map remdups N, [], 0, None)" by simp
have 1: "full cdcl⇩W_stgy (toS ([], ?N, [], 0, None)) (toS S)"
unfolding full_def apply rule
using do_all_cdcl⇩W_stgy_is_rtranclp_cdcl⇩W_stgy[of
"state_from_init_state_of ([], map remdups N, [], 0, None)"] inv
no_step_cdcl⇩W_stgy_cdcl⇩W_all
by (auto simp del: do_all_cdcl⇩W_stgy.simps simp: state_from_init_state_of_inverse
r[symmetric])+
moreover have 2: "finite (set (map mset ?N))" by auto
moreover have 3: "distinct_mset_set (set (map mset ?N))"
unfolding distinct_mset_set_def by auto
moreover
have "cdcl⇩W_all_struct_inv (toS S)"
by (metis (no_types) cdcl⇩W_all_struct_inv_rough_state r
toS_rough_state_of_state_of_rough_state_from_init_state_of)
then have cons: "consistent_interp (lits_of M')"
unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def S[symmetric] by auto
moreover
have "clss (toS ([], ?N, [], 0, None)) = clss (toS S)"
apply (rule rtranclp_cdcl⇩W_init_clss)
using 1 unfolding full_def by (auto simp add: rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W)
then have N': "mset (map mset ?N) = N'"
using S[symmetric] by auto
have "(E ≠ Some {#} ∧ satisfiable (set (map mset ?N)))
∨ (E = Some {#} ∧ unsatisfiable (set (map mset ?N)))"
using full_cdcl⇩W_stgy_final_state_conclusive unfolding N' apply rule
using 1 apply simp
using 2 apply simp
using 3 apply simp
using S[symmetric] N' apply auto[1]
using S[symmetric] N' cons by (fastforce simp: true_annots_true_cls)
then show ?thesis by auto
qed
paragraph ‹The Code›
text ‹The SML code is skipped in the documentation, but stays to ensure that some version of the
exported code is working. The only difference between the generated code and the one used here is
the export of the constructor ConI.›
fun gene where
"gene 0 = [[Pos 0], [Neg 0]]" |
"gene (Suc n) = map (op # (Pos (Suc n))) (gene n) @ map (op # (Neg (Suc n))) (gene n)"
value "gene 1"
export_code do_all_cdcl⇩W_stgy gene in SML
ML ‹
structure HOL : sig
type 'a equal
val equal : 'a equal -> 'a -> 'a -> bool
val eq : 'a equal -> 'a -> 'a -> bool
end = struct
type 'a equal = {equal : 'a -> 'a -> bool};
val equal = #equal : 'a equal -> 'a -> 'a -> bool;
fun eq A_ a b = equal A_ a b;
end; (*struct HOL*)
structure List : sig
val equal_list : 'a HOL.equal -> ('a list) HOL.equal
val fold : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val rev : 'a list -> 'a list
val find : ('a -> bool) -> 'a list -> 'a option
val null : 'a list -> bool
val filter : ('a -> bool) -> 'a list -> 'a list
val member : 'a HOL.equal -> 'a list -> 'a -> bool
val remdups : 'a HOL.equal -> 'a list -> 'a list
val remove1 : 'a HOL.equal -> 'a -> 'a list -> 'a list
val map : ('a -> 'b) -> 'a list -> 'b list
val list_all : ('a -> bool) -> 'a list -> bool
end = struct
fun equal_lista A_ [] (x21 :: x22) = false
| equal_lista A_ (x21 :: x22) [] = false
| equal_lista A_ (x21 :: x22) (y21 :: y22) =
HOL.eq A_ x21 y21 andalso equal_lista A_ x22 y22
| equal_lista A_ [] [] = true;
fun equal_list A_ = {equal = equal_lista A_} : ('a list) HOL.equal;
fun fold f (x :: xs) s = fold f xs (f x s)
| fold f [] s = s;
fun rev xs = fold (fn a => fn b => a :: b) xs [];
fun find uu [] = NONE
| find p (x :: xs) = (if p x then SOME x else find p xs);
fun null [] = true
| null (x :: xs) = false;
fun filter p [] = []
| filter p (x :: xs) = (if p x then x :: filter p xs else filter p xs);
fun member A_ [] y = false
| member A_ (x :: xs) y = HOL.eq A_ x y orelse member A_ xs y;
fun remdups A_ [] = []
| remdups A_ (x :: xs) =
(if member A_ xs x then remdups A_ xs else x :: remdups A_ xs);
fun remove1 A_ x [] = []
| remove1 A_ x (y :: xs) =
(if HOL.eq A_ x y then xs else y :: remove1 A_ x xs);
fun map f [] = []
| map f (x21 :: x22) = f x21 :: map f x22;
fun list_all p [] = true
| list_all p (x :: xs) = p x andalso list_all p xs;
end; (*struct List*)
structure Set : sig
datatype 'a set = Set of 'a list | Coset of 'a list
val image : ('a -> 'b) -> 'a set -> 'b set
val member : 'a HOL.equal -> 'a -> 'a set -> bool
end = struct
datatype 'a set = Set of 'a list | Coset of 'a list;
fun image f (Set xs) = Set (List.map f xs);
fun member A_ x (Coset xs) = not (List.member A_ xs x)
| member A_ x (Set xs) = List.member A_ xs x;
end; (*struct Set*)
structure Orderings : sig
type 'a ord
val less_eq : 'a ord -> 'a -> 'a -> bool
val less : 'a ord -> 'a -> 'a -> bool
type 'a preorder
val ord_preorder : 'a preorder -> 'a ord
type 'a order
val preorder_order : 'a order -> 'a preorder
type 'a linorder
val order_linorder : 'a linorder -> 'a order
val max : 'a ord -> 'a -> 'a -> 'a
end = struct
type 'a ord = {less_eq : 'a -> 'a -> bool, less : 'a -> 'a -> bool};
val less_eq = #less_eq : 'a ord -> 'a -> 'a -> bool;
val less = #less : 'a ord -> 'a -> 'a -> bool;
type 'a preorder = {ord_preorder : 'a ord};
val ord_preorder = #ord_preorder : 'a preorder -> 'a ord;
type 'a order = {preorder_order : 'a preorder};
val preorder_order = #preorder_order : 'a order -> 'a preorder;
type 'a linorder = {order_linorder : 'a order};
val order_linorder = #order_linorder : 'a linorder -> 'a order;
fun max A_ a b = (if less_eq A_ a b then b else a);
end; (*struct Orderings*)
structure Arith : sig
datatype nat = Zero_nat | Suc of nat
val equal_nata : nat -> nat -> bool
val equal_nat : nat HOL.equal
val less_nat : nat -> nat -> bool
val linorder_nat : nat Orderings.linorder
val one_nat : nat
val plus_nat : nat -> nat -> nat
end = struct
datatype nat = Zero_nat | Suc of nat;
fun equal_nata Zero_nat (Suc x2) = false
| equal_nata (Suc x2) Zero_nat = false
| equal_nata (Suc x2) (Suc y2) = equal_nata x2 y2
| equal_nata Zero_nat Zero_nat = true;
val equal_nat = {equal = equal_nata} : nat HOL.equal;
fun less_eq_nat (Suc m) n = less_nat m n
| less_eq_nat Zero_nat n = true
and less_nat m (Suc n) = less_eq_nat m n
| less_nat n Zero_nat = false;
val ord_nat = {less_eq = less_eq_nat, less = less_nat} : nat Orderings.ord;
val preorder_nat = {ord_preorder = ord_nat} : nat Orderings.preorder;
val order_nat = {preorder_order = preorder_nat} : nat Orderings.order;
val linorder_nat = {order_linorder = order_nat} : nat Orderings.linorder;
val one_nat : nat = Suc Zero_nat;
fun plus_nat (Suc m) n = plus_nat m (Suc n)
| plus_nat Zero_nat n = n;
end; (*struct Arith*)
structure Option : sig
val equal_option : 'a HOL.equal -> ('a option) HOL.equal
end = struct
fun equal_optiona A_ NONE (SOME x2) = false
| equal_optiona A_ (SOME x2) NONE = false
| equal_optiona A_ (SOME x2) (SOME y2) = HOL.eq A_ x2 y2
| equal_optiona A_ NONE NONE = true;
fun equal_option A_ = {equal = equal_optiona A_} : ('a option) HOL.equal;
end; (*struct Option*)
structure Multiset : sig
datatype 'a multiset = Mset of 'a list
val single : 'a -> 'a multiset
val set_mset : 'a multiset -> 'a Set.set
val image_mset : ('a -> 'b) -> 'a multiset -> 'b multiset
val plus_multiset : 'a multiset -> 'a multiset -> 'a multiset
end = struct
datatype 'a multiset = Mset of 'a list;
fun single x = Mset [x];
fun set_mset (Mset x) = Set.Set x;
fun image_mset f (Mset xs) = Mset (List.map f xs);
fun plus_multiset (Mset xs) (Mset ys) = Mset (xs @ ys);
end; (*struct Multiset*)
structure Clausal_Logic : sig
datatype 'a literal = Pos of 'a | Neg of 'a
val equal_literala : 'a HOL.equal -> 'a literal -> 'a literal -> bool
val equal_literal : 'a HOL.equal -> 'a literal HOL.equal
val atm_of : 'a literal -> 'a
val uminus_literal : 'a literal -> 'a literal
end = struct
datatype 'a literal = Pos of 'a | Neg of 'a;
fun equal_literala A_ (Pos x1) (Neg x2) = false
| equal_literala A_ (Neg x2) (Pos x1) = false
| equal_literala A_ (Neg x2) (Neg y2) = HOL.eq A_ x2 y2
| equal_literala A_ (Pos x1) (Pos y1) = HOL.eq A_ x1 y1;
fun equal_literal A_ = {equal = equal_literala A_} : 'a literal HOL.equal;
fun atm_of (Pos x1) = x1
| atm_of (Neg x2) = x2;
fun is_pos (Pos x1) = true
| is_pos (Neg x2) = false;
fun uminus_literal l = (if is_pos l then Neg else Pos) (atm_of l);
end; (*struct Clausal_Logic*)
structure Partial_Annotated_Clausal_Logic : sig
datatype ('a, 'b, 'c) ann_literal = Decided of 'a Clausal_Logic.literal * 'b |
Propagated of 'a Clausal_Logic.literal * 'c
val equal_ann_literal :
'a HOL.equal -> 'b HOL.equal -> 'c HOL.equal ->
('a, 'b, 'c) ann_literal HOL.equal
val lits_of : ('a, 'b, 'c) ann_literal list -> 'a Clausal_Logic.literal Set.set
end = struct
datatype ('a, 'b, 'c) ann_literal = Decided of 'a Clausal_Logic.literal * 'b |
Propagated of 'a Clausal_Logic.literal * 'c;
fun equal_ann_literala A_ B_ C_ (Decided (x11, x12)) (Propagated (x21, x22)) =
false
| equal_ann_literala A_ B_ C_ (Propagated (x21, x22)) (Decided (x11, x12)) =
false
| equal_ann_literala A_ B_ C_ (Propagated (x21, x22)) (Propagated (y21, y22)) =
Clausal_Logic.equal_literala A_ x21 y21 andalso HOL.eq C_ x22 y22
| equal_ann_literala A_ B_ C_ (Decided (x11, x12)) (Decided (y11, y12)) =
Clausal_Logic.equal_literala A_ x11 y11 andalso HOL.eq B_ x12 y12;
fun equal_ann_literal A_ B_ C_ = {equal = equal_ann_literala A_ B_ C_} :
('a, 'b, 'c) ann_literal HOL.equal;
fun lit_of (Decided (x11, x12)) = x11
| lit_of (Propagated (x21, x22)) = x21;
fun lits_of ls = Set.image lit_of (Set.Set ls);
end; (*struct Partial_Annotated_Clausal_Logic*)
structure Lattices_Big : sig
val max : 'a Orderings.linorder -> 'a Set.set -> 'a
end = struct
fun max A_ (Set.Set (x :: xs)) =
List.fold
(Orderings.max
((Orderings.ord_preorder o Orderings.preorder_order o
Orderings.order_linorder)
A_))
xs x;
end; (*struct Lattices_Big*)
structure CDCL_W_Level : sig
val get_rev_level :
'a HOL.equal ->
('a, Arith.nat, 'b) Partial_Annotated_Clausal_Logic.ann_literal list ->
Arith.nat -> 'a Clausal_Logic.literal -> Arith.nat
val get_maximum_level :
'a HOL.equal ->
('a, Arith.nat, 'b) Partial_Annotated_Clausal_Logic.ann_literal list ->
'a Clausal_Logic.literal Multiset.multiset -> Arith.nat
end = struct
fun get_rev_level A_ [] uu uv = Arith.Zero_nat
| get_rev_level A_ (Partial_Annotated_Clausal_Logic.Decided (la, level) :: ls)
n l =
(if HOL.eq A_ (Clausal_Logic.atm_of la) (Clausal_Logic.atm_of l) then level
else get_rev_level A_ ls level l)
| get_rev_level A_ (Partial_Annotated_Clausal_Logic.Propagated (la, uw) :: ls)
n l =
(if HOL.eq A_ (Clausal_Logic.atm_of la) (Clausal_Logic.atm_of l) then n
else get_rev_level A_ ls n l);
fun get_maximum_level A_ m d =
Lattices_Big.max Arith.linorder_nat
(Multiset.set_mset
(Multiset.plus_multiset (Multiset.single Arith.Zero_nat)
(Multiset.image_mset (get_rev_level A_ (List.rev m) Arith.Zero_nat)
d)));
end; (*struct CDCL_W_Level*)
structure Product_Type : sig
val equal_proda : 'a HOL.equal -> 'b HOL.equal -> 'a * 'b -> 'a * 'b -> bool
val equal_prod : 'a HOL.equal -> 'b HOL.equal -> ('a * 'b) HOL.equal
end = struct
fun equal_proda A_ B_ (x1, x2) (y1, y2) =
HOL.eq A_ x1 y1 andalso HOL.eq B_ x2 y2;
fun equal_prod A_ B_ = {equal = equal_proda A_ B_} : ('a * 'b) HOL.equal;
end; (*struct Product_Type*)
structure DPLL_CDCL_W_Implementation : sig
val find_first_unused_var :
'a HOL.equal ->
('a Clausal_Logic.literal list) list ->
'a Clausal_Logic.literal Set.set -> 'a Clausal_Logic.literal option
val find_first_unit_clause :
'a HOL.equal ->
('a Clausal_Logic.literal list) list ->
('a, 'b, 'c) Partial_Annotated_Clausal_Logic.ann_literal list ->
('a Clausal_Logic.literal * 'a Clausal_Logic.literal list) option
end = struct
fun is_unit_clause_code A_ l m =
(case List.filter
(fn a =>
not (Set.member A_ (Clausal_Logic.atm_of a)
(Set.image Clausal_Logic.atm_of
(Partial_Annotated_Clausal_Logic.lits_of m))))
l
of [] => NONE
| [a] =>
(if List.list_all
(fn c =>
Set.member (Clausal_Logic.equal_literal A_)
(Clausal_Logic.uminus_literal c)
(Partial_Annotated_Clausal_Logic.lits_of m))
(List.remove1 (Clausal_Logic.equal_literal A_) a l)
then SOME a else NONE)
| _ :: _ :: _ => NONE);
fun is_unit_clause A_ l m = is_unit_clause_code A_ l m;
fun find_first_unused_var A_ (a :: l) m =
(case List.find
(fn lit =>
not (Set.member (Clausal_Logic.equal_literal A_) lit m) andalso
not (Set.member (Clausal_Logic.equal_literal A_)
(Clausal_Logic.uminus_literal lit) m))
a
of NONE => find_first_unused_var A_ l m | SOME aa => SOME aa)
| find_first_unused_var A_ [] uu = NONE;
fun find_first_unit_clause A_ (a :: l) m =
(case is_unit_clause A_ a m of NONE => find_first_unit_clause A_ l m
| SOME la => SOME (la, a))
| find_first_unit_clause A_ [] uu = NONE;
end; (*struct DPLL_CDCL_W_Implementation*)
structure CDCL_W_Implementation : sig
datatype cdcl_W_state_inv_from_init_state =
ConI of
((Arith.nat, Arith.nat, (Arith.nat Clausal_Logic.literal list))
Partial_Annotated_Clausal_Logic.ann_literal list *
((Arith.nat Clausal_Logic.literal list) list *
((Arith.nat Clausal_Logic.literal list) list *
(Arith.nat * (Arith.nat Clausal_Logic.literal list) option))));
val gene : Arith.nat -> (Arith.nat Clausal_Logic.literal list) list
val do_all_cdcl_W_stgy :
cdcl_W_state_inv_from_init_state -> cdcl_W_state_inv_from_init_state
end = struct
datatype cdcl_W_state_inv =
Con of
((Arith.nat, Arith.nat, (Arith.nat Clausal_Logic.literal list))
Partial_Annotated_Clausal_Logic.ann_literal list *
((Arith.nat Clausal_Logic.literal list) list *
((Arith.nat Clausal_Logic.literal list) list *
(Arith.nat * (Arith.nat Clausal_Logic.literal list) option))));
datatype cdcl_W_state_inv_from_init_state =
ConI of
((Arith.nat, Arith.nat, (Arith.nat Clausal_Logic.literal list))
Partial_Annotated_Clausal_Logic.ann_literal list *
((Arith.nat Clausal_Logic.literal list) list *
((Arith.nat Clausal_Logic.literal list) list *
(Arith.nat * (Arith.nat Clausal_Logic.literal list) option))));
fun gene Arith.Zero_nat =
[[Clausal_Logic.Pos Arith.Zero_nat], [Clausal_Logic.Neg Arith.Zero_nat]]
| gene (Arith.Suc n) =
List.map (fn a => Clausal_Logic.Pos (Arith.Suc n) :: a) (gene n) @
List.map (fn a => Clausal_Logic.Neg (Arith.Suc n) :: a) (gene n);
fun bt_cut i (Partial_Annotated_Clausal_Logic.Propagated (uu, uv) :: ls) =
bt_cut i ls
| bt_cut i (Partial_Annotated_Clausal_Logic.Decided (ka, k) :: ls) =
(if Arith.equal_nata k (Arith.Suc i)
then SOME (Partial_Annotated_Clausal_Logic.Decided (ka, k) :: ls)
else bt_cut i ls)
| bt_cut i [] = NONE;
fun do_propagate_step A_ s =
(case s
of (m, (n, (u, (k, NONE)))) =>
(case DPLL_CDCL_W_Implementation.find_first_unit_clause A_ (n @ u) m
of NONE => (m, (n, (u, (k, NONE))))
| SOME (l, c) =>
(Partial_Annotated_Clausal_Logic.Propagated (l, c) :: m,
(n, (u, (k, NONE)))))
| (m, (n, (u, (k, SOME ah)))) => (m, (n, (u, (k, SOME ah)))));
fun find_conflict A_ m [] = NONE
| find_conflict A_ m (n :: ns) =
(if List.list_all
(fn c =>
Set.member (Clausal_Logic.equal_literal A_)
(Clausal_Logic.uminus_literal c)
(Partial_Annotated_Clausal_Logic.lits_of m))
n
then SOME n else find_conflict A_ m ns);
fun do_conflict_step A_ s =
(case s
of (m, (n, (u, (k, NONE)))) =>
(case find_conflict A_ m (n @ u) of NONE => (m, (n, (u, (k, NONE))))
| SOME a => (m, (n, (u, (k, SOME a)))))
| (m, (n, (u, (k, SOME ah)))) => (m, (n, (u, (k, SOME ah)))));
fun do_cp_step A_ s = (do_propagate_step A_ o do_conflict_step A_) s;
fun rough_state_from_init_state_of (ConI x) = x;
fun id_of_I_to s = Con (rough_state_from_init_state_of s);
fun rough_state_of (Con x) = x;
fun do_cp_stepa s = Con (do_cp_step Arith.equal_nat (rough_state_of s));
fun do_skip_step
(Partial_Annotated_Clausal_Logic.Propagated (l, c) :: ls,
(n, (u, (k, SOME d))))
= (if not (List.member (Clausal_Logic.equal_literal Arith.equal_nat) d
(Clausal_Logic.uminus_literal l)) andalso
not (List.null d)
then (ls, (n, (u, (k, SOME d))))
else (Partial_Annotated_Clausal_Logic.Propagated (l, c) :: ls,
(n, (u, (k, SOME d)))))
| do_skip_step ([], va) = ([], va)
| do_skip_step (Partial_Annotated_Clausal_Logic.Decided (vd, ve) :: vc, va) =
(Partial_Annotated_Clausal_Logic.Decided (vd, ve) :: vc, va)
| do_skip_step (v, (vb, (vd, (vf, NONE)))) = (v, (vb, (vd, (vf, NONE))));
fun maximum_level_code A_ d m =
CDCL_W_Level.get_maximum_level A_ m (Multiset.Mset d);
fun find_level_decomp A_ m [] d k = NONE
| find_level_decomp A_ m (l :: ls) d k =
let
val (i, j) =
(CDCL_W_Level.get_rev_level A_ (List.rev m) Arith.Zero_nat l,
maximum_level_code A_ (d @ ls) m);
in
(if Arith.equal_nata i k andalso Arith.less_nat j i then SOME (l, j)
else find_level_decomp A_ m ls (l :: d) k)
end;
fun do_backtrack_step A_ (m, (n, (u, (k, SOME d)))) =
(case find_level_decomp A_ m d [] k of NONE => (m, (n, (u, (k, SOME d))))
| SOME (l, j) =>
(case bt_cut j m of NONE => (m, (n, (u, (k, SOME d))))
| SOME [] => (m, (n, (u, (k, SOME d))))
| SOME (Partial_Annotated_Clausal_Logic.Decided (_, _) :: ls) =>
(Partial_Annotated_Clausal_Logic.Propagated (l, d) :: ls,
(n, (d :: u, (j, NONE))))
| SOME (Partial_Annotated_Clausal_Logic.Propagated (_, _) :: _) =>
(m, (n, (u, (k, SOME d))))))
| do_backtrack_step A_ (v, (vb, (vd, (vf, NONE)))) =
(v, (vb, (vd, (vf, NONE))));
fun do_resolve_step
(Partial_Annotated_Clausal_Logic.Propagated (l, c) :: ls,
(n, (u, (k, SOME d))))
= (if List.member (Clausal_Logic.equal_literal Arith.equal_nat) d
(Clausal_Logic.uminus_literal l) andalso
Arith.equal_nata
(maximum_level_code Arith.equal_nat
(List.remove1 (Clausal_Logic.equal_literal Arith.equal_nat)
(Clausal_Logic.uminus_literal l) d)
(Partial_Annotated_Clausal_Logic.Propagated (l, c) :: ls))
k
then (ls, (n, (u, (k, SOME (List.remdups
(Clausal_Logic.equal_literal Arith.equal_nat)
(List.remove1
(Clausal_Logic.equal_literal
Arith.equal_nat)
l c @
List.remove1
(Clausal_Logic.equal_literal
Arith.equal_nat)
(Clausal_Logic.uminus_literal l) d))))))
else (Partial_Annotated_Clausal_Logic.Propagated (l, c) :: ls,
(n, (u, (k, SOME d)))))
| do_resolve_step ([], va) = ([], va)
| do_resolve_step (Partial_Annotated_Clausal_Logic.Decided (vd, ve) :: vc, va)
= (Partial_Annotated_Clausal_Logic.Decided (vd, ve) :: vc, va)
| do_resolve_step (v, (vb, (vd, (vf, NONE)))) = (v, (vb, (vd, (vf, NONE))));
fun do_decide_step A_ (m, (n, (u, (k, NONE)))) =
(case DPLL_CDCL_W_Implementation.find_first_unused_var A_ n
(Partial_Annotated_Clausal_Logic.lits_of m)
of NONE => (m, (n, (u, (k, NONE))))
| SOME l =>
(Partial_Annotated_Clausal_Logic.Decided (l, Arith.Suc k) :: m,
(n, (u, (Arith.plus_nat k Arith.one_nat, NONE)))))
| do_decide_step A_ (v, (vb, (vd, (vf, SOME vh)))) =
(v, (vb, (vd, (vf, SOME vh))));
fun do_other_step s =
let
val t = do_skip_step s;
in
(if not (Product_Type.equal_proda
(List.equal_list
(Partial_Annotated_Clausal_Logic.equal_ann_literal
Arith.equal_nat Arith.equal_nat
(List.equal_list
(Clausal_Logic.equal_literal Arith.equal_nat))))
(Product_Type.equal_prod
(List.equal_list
(List.equal_list
(Clausal_Logic.equal_literal Arith.equal_nat)))
(Product_Type.equal_prod
(List.equal_list
(List.equal_list
(Clausal_Logic.equal_literal Arith.equal_nat)))
(Product_Type.equal_prod Arith.equal_nat
(Option.equal_option
(List.equal_list
(Clausal_Logic.equal_literal Arith.equal_nat))))))
t s)
then t
else let
val u = do_resolve_step t;
in
(if not (Product_Type.equal_proda
(List.equal_list
(Partial_Annotated_Clausal_Logic.equal_ann_literal
Arith.equal_nat Arith.equal_nat
(List.equal_list
(Clausal_Logic.equal_literal Arith.equal_nat))))
(Product_Type.equal_prod
(List.equal_list
(List.equal_list
(Clausal_Logic.equal_literal Arith.equal_nat)))
(Product_Type.equal_prod
(List.equal_list
(List.equal_list
(Clausal_Logic.equal_literal Arith.equal_nat)))
(Product_Type.equal_prod Arith.equal_nat
(Option.equal_option
(List.equal_list
(Clausal_Logic.equal_literal
Arith.equal_nat))))))
u t)
then u
else let
val v = do_backtrack_step Arith.equal_nat u;
in
(if not (Product_Type.equal_proda
(List.equal_list
(Partial_Annotated_Clausal_Logic.equal_ann_literal
Arith.equal_nat Arith.equal_nat
(List.equal_list
(Clausal_Logic.equal_literal
Arith.equal_nat))))
(Product_Type.equal_prod
(List.equal_list
(List.equal_list
(Clausal_Logic.equal_literal
Arith.equal_nat)))
(Product_Type.equal_prod
(List.equal_list
(List.equal_list
(Clausal_Logic.equal_literal Arith.equal_nat)))
(Product_Type.equal_prod Arith.equal_nat
(Option.equal_option
(List.equal_list (Clausal_Logic.equal_literal Arith.equal_nat))))))
v u)
then v else do_decide_step Arith.equal_nat v)
end)
end)
end;
fun do_other_stepa s = Con (do_other_step (rough_state_of s));
fun equal_cdcl_W_state_inv sa s =
Product_Type.equal_proda
(List.equal_list
(Partial_Annotated_Clausal_Logic.equal_ann_literal Arith.equal_nat
Arith.equal_nat
(List.equal_list (Clausal_Logic.equal_literal Arith.equal_nat))))
(Product_Type.equal_prod
(List.equal_list
(List.equal_list (Clausal_Logic.equal_literal Arith.equal_nat)))
(Product_Type.equal_prod
(List.equal_list
(List.equal_list (Clausal_Logic.equal_literal Arith.equal_nat)))
(Product_Type.equal_prod Arith.equal_nat
(Option.equal_option
(List.equal_list (Clausal_Logic.equal_literal Arith.equal_nat))))))
(rough_state_of sa) (rough_state_of s);
fun do_full1_cp_step s =
let
val sa = do_cp_stepa s;
in
(if equal_cdcl_W_state_inv s sa then s else do_full1_cp_step sa)
end;
fun equal_cdcl_W_state_inv_from_init_state sa s =
Product_Type.equal_proda
(List.equal_list
(Partial_Annotated_Clausal_Logic.equal_ann_literal Arith.equal_nat
Arith.equal_nat
(List.equal_list (Clausal_Logic.equal_literal Arith.equal_nat))))
(Product_Type.equal_prod
(List.equal_list
(List.equal_list (Clausal_Logic.equal_literal Arith.equal_nat)))
(Product_Type.equal_prod
(List.equal_list
(List.equal_list (Clausal_Logic.equal_literal Arith.equal_nat)))
(Product_Type.equal_prod Arith.equal_nat
(Option.equal_option
(List.equal_list (Clausal_Logic.equal_literal Arith.equal_nat))))))
(rough_state_from_init_state_of sa) (rough_state_from_init_state_of s);
fun do_cdcl_W_stgy_step s =
let
val t = do_full1_cp_step s;
in
(if not (equal_cdcl_W_state_inv t s) then t
else let
val a = do_other_stepa t;
in
do_full1_cp_step a
end)
end;
fun do_cdcl_W_stgy_stepa s =
ConI (rough_state_of (do_cdcl_W_stgy_step (id_of_I_to s)));
fun do_all_cdcl_W_stgy s =
let
val t = do_cdcl_W_stgy_stepa s;
in
(if equal_cdcl_W_state_inv_from_init_state t s then s
else do_all_cdcl_W_stgy t)
end;
end; (*struct CDCL_W_Implementation*)
›
declare[[ML_print_depth=100]]
ML ‹
open Clausal_Logic;
open CDCL_W_Implementation;
open Arith;
let
val N = gene (Suc (Suc (Suc (((Suc Zero_nat))))))
val f = do_all_cdcl_W_stgy (CDCL_W_Implementation.ConI ([], (N, ([], (Zero_nat, NONE)))))
in
f
end
›
end