theory IsaSAT
imports IsaSAT_Restart IsaSAT_Initialisation
begin
chapter ‹Full IsaSAT›
text ‹
We now combine all the previous definitions to prove correctness of the complete SAT
solver:
▸ We initialise the arena part of the state;
▸ Then depending on the options and the number of clauses, we either use the
bounded version or the unbounded version. Once have if decided which one,
we initiale the watch lists;
▸ After that, we can run the CDCL part of the SAT solver;
▸ Finally, we extract the trail from the state.
Remark that the statistics and the options are unchecked: the number of propagations
might overflows (but they do not impact the correctness of the whole solver). Similar
restriction applies on the options: setting the options might not do what you expect to
happen, but the result will still be correct.
›
section ‹Correctness Relation›
text ‹
We cannot use \<^term>‹cdcl_twl_stgy_restart› since we do not always end in a final state
for \<^term>‹cdcl_twl_stgy›.
›
definition conclusive_TWL_run :: ‹'v twl_st ⇒ 'v twl_st nres› where
‹conclusive_TWL_run S =
SPEC(λT. ∃n n'. cdcl_twl_stgy_restart_with_leftovers⇧*⇧* (S, n) (T, n') ∧ final_twl_state T)›
definition conclusive_TWL_run_bounded :: ‹'v twl_st ⇒ (bool × 'v twl_st) nres› where
‹conclusive_TWL_run_bounded S =
SPEC(λ(brk, T). ∃n n'. cdcl_twl_stgy_restart_with_leftovers⇧*⇧* (S, n) (T, n') ∧
(brk ⟶ final_twl_state T))›
text ‹To get a full CDCL run:
▪ either we fully apply \<^term>‹cdcl⇩W_restart_mset.cdcl⇩W_stgy› (up to restarts)
▪ or we can stop early.
›
definition conclusive_CDCL_run where
‹conclusive_CDCL_run CS T U ⟷
(∃n n'. cdcl⇩W_restart_mset.cdcl⇩W_restart_stgy⇧*⇧* (T, n) (U, n') ∧
no_step cdcl⇩W_restart_mset.cdcl⇩W (U)) ∨
(CS ≠ {#} ∧ conflicting U ≠ None ∧ count_decided (trail U) = 0 ∧
unsatisfiable (set_mset CS))›
lemma cdcl_twl_stgy_restart_restart_prog_spec: ‹twl_struct_invs S ⟹
twl_stgy_invs S ⟹
clauses_to_update S = {#} ⟹
get_conflict S = None ⟹
cdcl_twl_stgy_restart_prog S ≤ conclusive_TWL_run S›
apply (rule order_trans)
apply (rule cdcl_twl_stgy_restart_prog_spec; assumption?)
unfolding conclusive_TWL_run_def twl_restart_def
by auto
lemma cdcl_twl_stgy_restart_prog_bounded_spec: ‹twl_struct_invs S ⟹
twl_stgy_invs S ⟹
clauses_to_update S = {#} ⟹
get_conflict S = None ⟹
cdcl_twl_stgy_restart_prog_bounded S ≤ conclusive_TWL_run_bounded S›
apply (rule order_trans)
apply (rule cdcl_twl_stgy_prog_bounded_spec; assumption?)
unfolding conclusive_TWL_run_bounded_def twl_restart_def
by auto
lemma cdcl_twl_stgy_restart_restart_prog_early_spec: ‹twl_struct_invs S ⟹
twl_stgy_invs S ⟹
clauses_to_update S = {#} ⟹
get_conflict S = None ⟹
cdcl_twl_stgy_restart_prog_early S ≤ conclusive_TWL_run S›
apply (rule order_trans)
apply (rule cdcl_twl_stgy_prog_early_spec; assumption?)
unfolding conclusive_TWL_run_def twl_restart_def
by auto
lemma cdcl⇩W_ex_cdcl⇩W_stgy:
‹cdcl⇩W_restart_mset.cdcl⇩W S T ⟹ ∃U. cdcl⇩W_restart_mset.cdcl⇩W_stgy S U›
by (meson cdcl⇩W_restart_mset.cdcl⇩W.cases cdcl⇩W_restart_mset.cdcl⇩W_stgy.simps)
lemma rtranclp_cdcl⇩W_cdcl⇩W_init_state:
‹cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* (init_state {#}) S ⟷ S = init_state {#}›
unfolding rtranclp_unfold
by (subst tranclp_unfold_begin)
(auto simp: cdcl⇩W_stgy_cdcl⇩W_init_state_empty_no_step
cdcl⇩W_stgy_cdcl⇩W_init_state
simp del: init_state.simps
dest: cdcl⇩W_restart_mset.cdcl⇩W_stgy_cdcl⇩W cdcl⇩W_ex_cdcl⇩W_stgy)
definition init_state_l :: ‹'v twl_st_l_init› where
‹init_state_l = (([], fmempty, None, {#}, {#}, {#}, {#}, {#}, {#}), {#})›
definition to_init_state_l :: ‹nat twl_st_l_init ⇒ nat twl_st_l_init› where
‹to_init_state_l S = S›
definition init_state0 :: ‹'v twl_st_init› where
‹init_state0 = (([], {#}, {#}, None, {#}, {#}, {#}, {#}, {#}, {#}), {#})›
definition to_init_state0 :: ‹nat twl_st_init ⇒ nat twl_st_init› where
‹to_init_state0 S = S›
lemma init_dt_pre_init:
assumes dist: ‹Multiset.Ball (mset `# mset CS) distinct_mset›
shows ‹init_dt_pre CS (to_init_state_l init_state_l)›
using dist apply -
unfolding init_dt_pre_def to_init_state_l_def init_state_l_def
by (rule exI[of _ ‹(([], {#}, {#}, None, {#}, {#}, {#}, {#}, {#}, {#}), {#})›])
(auto simp: twl_st_l_init_def twl_init_invs)
text ‹This is the specification of the SAT solver:›
definition SAT :: ‹nat clauses ⇒ nat cdcl⇩W_restart_mset nres› where
‹SAT CS = do{
let T = init_state CS;
SPEC (conclusive_CDCL_run CS T)
}›
definition init_dt_spec0 :: ‹'v clause_l list ⇒ 'v twl_st_init ⇒ 'v twl_st_init ⇒ bool› where
‹init_dt_spec0 CS SOC T' ⟷
(
twl_struct_invs_init T' ∧
clauses_to_update_init T' = {#} ∧
(∀s∈set (get_trail_init T'). ¬is_decided s) ∧
(get_conflict_init T' = None ⟶
literals_to_update_init T' = uminus `# lit_of `# mset (get_trail_init T')) ∧
(mset `# mset CS + clause `# (get_init_clauses_init SOC) + other_clauses_init SOC +
get_unit_init_clauses_init SOC + get_subsumed_init_clauses_init SOC =
clause `# (get_init_clauses_init T') + other_clauses_init T' +
get_unit_init_clauses_init T' + get_subsumed_init_clauses_init T') ∧
get_learned_clauses_init SOC = get_learned_clauses_init T' ∧
get_subsumed_learned_clauses_init SOC = get_subsumed_learned_clauses_init T' ∧
get_unit_learned_clauses_init T' = get_unit_learned_clauses_init SOC ∧
twl_stgy_invs (fst T') ∧
(other_clauses_init T' ≠ {#} ⟶ get_conflict_init T' ≠ None) ∧
({#} ∈# mset `# mset CS ⟶ get_conflict_init T' ≠ None) ∧
(get_conflict_init SOC ≠ None ⟶ get_conflict_init SOC = get_conflict_init T'))›
section ‹Refinements of the Whole SAT Solver›
text ‹
We do not add the refinement steps in separate files, since the form is very specific
to the SAT solver we want to generate (and needs to be updated if it changes).
›
definition SAT0 :: ‹nat clause_l list ⇒ nat twl_st nres› where
‹SAT0 CS = do{
b ← SPEC(λ_::bool. True);
if b then do {
let S = init_state0;
T ← SPEC (init_dt_spec0 CS (to_init_state0 S));
let T = fst T;
if get_conflict T ≠ None
then RETURN T
else if CS = [] then RETURN (fst init_state0)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update T = {#});
ASSERT(clause `# (get_clauses T) + unit_clss T + subsumed_clauses T = mset `# mset CS);
ASSERT(get_learned_clss T = {#});
ASSERT(subsumed_learned_clss T = {#});
cdcl_twl_stgy_restart_prog T
}
}
else do {
let S = init_state0;
T ← SPEC (init_dt_spec0 CS (to_init_state0 S));
failed ← SPEC (λ_ :: bool. True);
if failed then do {
T ← SPEC (init_dt_spec0 CS (to_init_state0 S));
let T = fst T;
if get_conflict T ≠ None
then RETURN T
else if CS = [] then RETURN (fst init_state0)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update T = {#});
ASSERT(clause `# (get_clauses T) + unit_clss T + subsumed_clauses T = mset `# mset CS);
ASSERT(get_learned_clss T = {#});
cdcl_twl_stgy_restart_prog T
}
} else do {
let T = fst T;
if get_conflict T ≠ None
then RETURN T
else if CS = [] then RETURN (fst init_state0)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update T = {#});
ASSERT(clause `# (get_clauses T) + unit_clss T + subsumed_clauses T = mset `# mset CS);
ASSERT(get_learned_clss T = {#});
cdcl_twl_stgy_restart_prog_early T
}
}
}
}›
lemma SAT0_SAT:
assumes ‹Multiset.Ball (mset `# mset CS) distinct_mset›
shows ‹SAT0 CS ≤ ⇓ {(S, T). T = state⇩W_of S} (SAT (mset `# mset CS))›
proof -
have conflict_during_init: ‹RETURN (fst T)
≤ ⇓ {(S, T). T = state⇩W_of S}
(SPEC (conclusive_CDCL_run (mset `# mset CS)
(init_state (mset `# mset CS))))›
if
spec: ‹T ∈ Collect (init_dt_spec0 CS (to_init_state0 init_state0))› and
confl: ‹get_conflict (fst T) ≠ None›
for T
proof -
let ?CS = ‹mset `# mset CS›
have
struct_invs: ‹twl_struct_invs_init T› and
‹clauses_to_update_init T = {#}› and
count_dec: ‹∀s∈set (get_trail_init T). ¬ is_decided s› and
‹get_conflict_init T = None ⟶
literals_to_update_init T =
uminus `# lit_of `# mset (get_trail_init T)› and
clss: ‹mset `# mset CS +
clause `# get_init_clauses_init (to_init_state0 init_state0) +
other_clauses_init (to_init_state0 init_state0) +
get_unit_init_clauses_init (to_init_state0 init_state0) +
get_subsumed_init_clauses_init (to_init_state0 init_state0) =
clause `# get_init_clauses_init T + other_clauses_init T +
get_unit_init_clauses_init T + get_subsumed_init_clauses_init T› and
learned: ‹get_learned_clauses_init (to_init_state0 init_state0) =
get_learned_clauses_init T›
‹get_unit_learned_clauses_init T =
get_unit_learned_clauses_init (to_init_state0 init_state0)›
‹get_subsumed_learned_clauses_init T =
get_subsumed_learned_clauses_init (to_init_state0 init_state0)› and
‹twl_stgy_invs (fst T)› and
‹other_clauses_init T ≠ {#} ⟶ get_conflict_init T ≠ None› and
‹{#} ∈# mset `# mset CS ⟶ get_conflict_init T ≠ None› and
‹get_conflict_init (to_init_state0 init_state0) ≠ None ⟶
get_conflict_init (to_init_state0 init_state0) = get_conflict_init T›
using spec unfolding init_dt_wl_spec_def init_dt_spec0_def
Set.mem_Collect_eq apply -
apply normalize_goal+
by metis+
have count_dec: ‹count_decided (get_trail (fst T)) = 0›
using count_dec unfolding count_decided_0_iff by (auto simp: twl_st_init
twl_st_wl_init)
have le: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (state⇩W_of_init T)› and
all_struct_invs:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of_init T)›
using struct_invs unfolding twl_struct_invs_init_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of_init T)›
using struct_invs unfolding twl_struct_invs_init_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast
have ‹unsatisfiable (set_mset (mset `# mset (rev CS)))›
using conflict_of_level_unsatisfiable[OF all_struct_invs] count_dec confl
learned le clss
by (auto simp: clauses_def mset_take_mset_drop_mset' twl_st_init twl_st_wl_init
image_image to_init_state0_def init_state0_def ac_simps
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def ac_simps
twl_st_l_init)
then have unsat[simp]: ‹unsatisfiable (mset ` set CS)›
by auto
then have [simp]: ‹CS ≠ []›
by (auto simp del: unsat)
show ?thesis
unfolding conclusive_CDCL_run_def
apply (rule RETURN_SPEC_refine)
apply (rule exI[of _ ‹state⇩W_of (fst T)›])
apply (intro conjI)
subgoal
by auto
subgoal
apply (rule disjI2)
using struct_invs learned count_dec clss confl
by (clarsimp simp: twl_st_init twl_st_wl_init twl_st_l_init)
done
qed
have empty_clauses: ‹RETURN (fst init_state0)
≤ ⇓ {(S, T). T = state⇩W_of S}
(SPEC
(conclusive_CDCL_run (mset `# mset CS)
(init_state (mset `# mset CS))))›
if
‹T ∈ Collect (init_dt_spec0 CS (to_init_state0 init_state0))› and
‹¬ get_conflict (fst T) ≠ None› and
‹CS = []›
for T
proof -
have [dest]: ‹cdcl⇩W_restart_mset.cdcl⇩W ([], {#}, {#}, None) (a, aa, ab, b) ⟹ False›
for a aa ab b
by (metis cdcl⇩W_restart_mset.cdcl⇩W.cases cdcl⇩W_restart_mset.cdcl⇩W_stgy.conflict'
cdcl⇩W_restart_mset.cdcl⇩W_stgy.propagate' cdcl⇩W_restart_mset.other'
cdcl⇩W_stgy_cdcl⇩W_init_state_empty_no_step init_state.simps)
show ?thesis
by (rule RETURN_RES_refine, rule exI[of _ ‹init_state {#}›])
(use that in ‹auto simp: conclusive_CDCL_run_def init_state0_def›)
qed
have extract_atms_clss_nempty: ‹extract_atms_clss CS {} ≠ {}›
if
‹T ∈ Collect (init_dt_spec0 CS (to_init_state0 init_state0))› and
‹¬ get_conflict (fst T) ≠ None› and
‹CS ≠ []›
for T
proof -
show ?thesis
using that
by (cases T; cases CS)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
qed
have cdcl_twl_stgy_restart_prog: ‹cdcl_twl_stgy_restart_prog (fst T)
≤ ⇓ {(S, T). T = state⇩W_of S}
(SPEC
(conclusive_CDCL_run (mset `# mset CS)
(init_state (mset `# mset CS))))› (is ?G1) and
cdcl_twl_stgy_restart_prog_early: ‹cdcl_twl_stgy_restart_prog_early (fst T)
≤ ⇓ {(S, T). T = state⇩W_of S}
(SPEC
(conclusive_CDCL_run (mset `# mset CS)
(init_state (mset `# mset CS))))› (is ?G2)
if
spec: ‹T ∈ Collect (init_dt_spec0 CS (to_init_state0 init_state0))› and
confl: ‹¬ get_conflict (fst T) ≠ None› and
CS_nempty[simp]: ‹CS ≠ []› and
‹extract_atms_clss CS {} ≠ {}› and
‹clause `# get_clauses (fst T) + unit_clss (fst T) + subsumed_clauses (fst T) =
mset `# mset CS› and
‹get_learned_clss (fst T) = {#}›
for T
proof -
let ?CS = ‹mset `# mset CS›
have
struct_invs: ‹twl_struct_invs_init T› and
clss_to_upd: ‹clauses_to_update_init T = {#}› and
count_dec: ‹∀s∈set (get_trail_init T). ¬ is_decided s› and
‹get_conflict_init T = None ⟶
literals_to_update_init T =
uminus `# lit_of `# mset (get_trail_init T)› and
clss: ‹mset `# mset CS +
clause `# get_init_clauses_init (to_init_state0 init_state0) +
other_clauses_init (to_init_state0 init_state0) +
get_unit_init_clauses_init (to_init_state0 init_state0) +
get_subsumed_init_clauses_init (to_init_state0 init_state0) =
clause `# get_init_clauses_init T + other_clauses_init T +
get_unit_init_clauses_init T + get_subsumed_init_clauses_init T› and
learned: ‹get_learned_clauses_init (to_init_state0 init_state0) =
get_learned_clauses_init T›
‹get_unit_learned_clauses_init T =
get_unit_learned_clauses_init (to_init_state0 init_state0)›
‹get_subsumed_learned_clauses_init T =
get_subsumed_learned_clauses_init (to_init_state0 init_state0)› and
stgy_invs: ‹twl_stgy_invs (fst T)› and
oth: ‹other_clauses_init T ≠ {#} ⟶ get_conflict_init T ≠ None› and
‹{#} ∈# mset `# mset CS ⟶ get_conflict_init T ≠ None› and
‹get_conflict_init (to_init_state0 init_state0) ≠ None ⟶
get_conflict_init (to_init_state0 init_state0) = get_conflict_init T›
using spec unfolding init_dt_wl_spec_def init_dt_spec0_def
Set.mem_Collect_eq apply -
apply normalize_goal+
by metis+
have struct_invs: ‹twl_struct_invs (fst T)›
by (rule twl_struct_invs_init_twl_struct_invs)
(use struct_invs oth confl in ‹auto simp: twl_st_init›)
have clss_to_upd: ‹clauses_to_update (fst T) = {#}›
using clss_to_upd by (auto simp: twl_st_init)
have conclusive_le: ‹conclusive_TWL_run (fst T)
≤ ⇓ {(S, T). T = state⇩W_of S}
(SPEC
(conclusive_CDCL_run (mset `# mset CS) (init_state (mset `# mset CS))))›
unfolding IsaSAT.conclusive_TWL_run_def
proof (rule RES_refine)
fix Ta
assume s: ‹Ta ∈ {Ta.
∃n n'.
cdcl_twl_stgy_restart_with_leftovers⇧*⇧* (fst T, n) (Ta, n') ∧
final_twl_state Ta}›
then obtain n n' where
twl: ‹cdcl_twl_stgy_restart_with_leftovers⇧*⇧* (fst T, n) (Ta, n')› and
final: ‹final_twl_state Ta›
by blast
have stgy_T_Ta: ‹cdcl⇩W_restart_mset.cdcl⇩W_restart_stgy⇧*⇧* (state⇩W_of (fst T), n) (state⇩W_of Ta, n')›
using rtranclp_cdcl_twl_stgy_restart_with_leftovers_cdcl⇩W_restart_stgy[OF twl] struct_invs
stgy_invs by simp
have ‹cdcl⇩W_restart_mset.cdcl⇩W_restart_stgy⇧*⇧* (state⇩W_of (fst T), n) (state⇩W_of Ta, n')›
using rtranclp_cdcl_twl_stgy_restart_with_leftovers_cdcl⇩W_restart_stgy[OF twl] struct_invs
stgy_invs by simp
have struct_invs_x: ‹twl_struct_invs Ta›
using twl struct_invs rtranclp_cdcl_twl_stgy_restart_with_leftovers_twl_struct_invs[OF twl]
by simp
then have all_struct_invs_x: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of Ta)›
unfolding twl_struct_invs_def
by blast
have M_lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv ([], mset `# mset CS, {#}, None)›
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def)
have learned': ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause ([], mset `# mset CS, {#}, None)›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by auto
have ent: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init ([], mset `# mset CS, {#}, None)›
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def)
define MW where ‹MW ≡ get_trail_init T›
have CS_clss: ‹cdcl⇩W_restart_mset.clauses (state⇩W_of (fst T)) = mset `# mset CS›
using learned clss oth confl unfolding clauses_def to_init_state0_def init_state0_def
cdcl⇩W_restart_mset.clauses_def
by (cases T) auto
have n_d: ‹no_dup MW› and
propa: ‹⋀L mark a b. a @ Propagated L mark # b = MW ⟹
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› and
clss_in_clss: ‹set (get_all_mark_of_propagated MW) ⊆ set_mset ?CS›
using struct_invs unfolding twl_struct_invs_def twl_struct_invs_init_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
clauses_def MW_def clss to_init_state0_def init_state0_def CS_clss[symmetric]
by ((cases T; auto)+)[3]
have count_dec': ‹∀L∈set MW. ¬is_decided L›
using count_dec unfolding MW_def twl_st_init by auto
have st_W: ‹state⇩W_of (fst T) = (MW, ?CS, {#}, None)›
using clss learned confl oth
by (cases T) (auto simp: state_wl_l_init_def state_wl_l_def twl_st_l_init_def
mset_take_mset_drop_mset mset_take_mset_drop_mset' clauses_def MW_def
added_only_watched_def state_wl_l_init'_def
to_init_state0_def init_state0_def
simp del: all_clss_l_ran_m
simp: all_clss_lf_ran_m[symmetric])
have 0: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy⇧*⇧* ([], ?CS, {#}, None)
(MW, ?CS, {#}, None)›
using n_d count_dec' propa clss_in_clss
proof (induction MW)
case Nil
then show ?case by auto
next
case (Cons K MW) note IH = this(1) and H = this(2-) and n_d = this(2) and dec = this(3) and
propa = this(4) and clss_in_clss = this(5)
let ?init = ‹([], mset `# mset CS, {#}, None)›
let ?int = ‹(MW, mset `# mset CS, {#}, None)›
let ?final = ‹(K # MW, mset `# mset CS, {#}, None)›
obtain L C where
K: ‹K = Propagated L C›
using dec by (cases K) auto
term ?init
have 1: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy⇧*⇧* ?init ?int›
apply (rule IH)
subgoal using n_d by simp
subgoal using dec by simp
subgoal for M2 L' mark M1
using K propa[of ‹K # M2› L' mark M1]
by (auto split: if_splits)
subgoal using clss_in_clss by (auto simp: K)
done
have ‹MW ⊨as CNot (remove1_mset L C)› and ‹L ∈# C›
using propa[of ‹[]› L C ‹MW›]
by (auto simp: K)
moreover have ‹C ∈# cdcl⇩W_restart_mset.clauses (MW, mset `# mset CS, {#}, None)›
using clss_in_clss by (auto simp: K clauses_def split: if_splits)
ultimately have ‹cdcl⇩W_restart_mset.propagate ?int
(Propagated L C # MW, mset `# mset CS, {#}, None)›
using n_d apply -
apply (rule cdcl⇩W_restart_mset.propagate_rule[of _ ‹C› L])
by (auto simp: K)
then have 2: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy ?int ?final›
by (auto simp add: K dest!: cdcl⇩W_restart_mset.cdcl⇩W_stgy.propagate')
show ?case
apply (rule rtranclp.rtrancl_into_rtrancl[OF 1])
apply (rule 2)
.
qed
with cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_stgy_cdcl⇩W_restart_stgy[OF 0, of n]
have stgy: ‹cdcl⇩W_restart_mset.cdcl⇩W_restart_stgy⇧*⇧* (([], mset `# mset CS, {#}, None), n)
(state⇩W_of Ta, n')›
using stgy_T_Ta unfolding st_W by simp
have entailed: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of Ta)›
apply (rule cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_learned_clauses_entailed)
apply (rule cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_stgy_cdcl⇩W_restart[OF stgy, unfolded fst_conv])
apply (rule learned')
apply (rule M_lev)
apply (rule ent)
done
consider
(ns) ‹no_step cdcl_twl_stgy Ta› |
(stop) ‹get_conflict Ta ≠ None› and ‹count_decided (get_trail Ta) = 0›
using final unfolding final_twl_state_def by auto
then show ‹∃s'∈Collect (conclusive_CDCL_run (mset `# mset CS)
(init_state (mset `# mset CS))).
(Ta, s') ∈ {(S, T). T = state⇩W_of S}›
proof cases
case ns
from no_step_cdcl_twl_stgy_no_step_cdcl⇩W_stgy[OF this struct_invs_x]
have ‹no_step cdcl⇩W_restart_mset.cdcl⇩W (state⇩W_of Ta)›
by (blast dest: cdcl⇩W_ex_cdcl⇩W_stgy)
then show ?thesis
apply -
apply (rule bexI[of _ ‹state⇩W_of Ta›])
using twl stgy s
unfolding conclusive_CDCL_run_def
by auto
next
case stop
have ‹unsatisfiable (set_mset (init_clss (state⇩W_of Ta)))›
apply (rule conflict_of_level_unsatisfiable)
apply (rule all_struct_invs_x)
using entailed stop by (auto simp: twl_st)
then have ‹unsatisfiable (mset ` set CS)›
using cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_init_clss[symmetric, OF
cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_stgy_cdcl⇩W_restart[OF stgy]]
by auto
then show ?thesis
using stop
by (auto simp: twl_st_init twl_st conclusive_CDCL_run_def)
qed
qed
show ?G1
apply (rule cdcl_twl_stgy_restart_restart_prog_spec[THEN order_trans])
apply (rule struct_invs; fail)
apply (rule stgy_invs; fail)
apply (rule clss_to_upd; fail)
apply (use confl in fast; fail)
apply (rule conclusive_le)
done
show ?G2
apply (rule cdcl_twl_stgy_restart_restart_prog_early_spec[THEN order_trans])
apply (rule struct_invs; fail)
apply (rule stgy_invs; fail)
apply (rule clss_to_upd; fail)
apply (use confl in fast; fail)
apply (rule conclusive_le)
done
qed
show ?thesis
unfolding SAT0_def SAT_def
apply (refine_vcg lhs_step_If)
subgoal for b T
by (rule conflict_during_init)
subgoal by (rule empty_clauses)
subgoal for b T
by (rule extract_atms_clss_nempty)
subgoal for b T
by (cases T)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for b T
by (cases T)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for b T
by (cases T)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for b T
by (cases T)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for b T
by (rule cdcl_twl_stgy_restart_prog)
subgoal for b T
by (rule conflict_during_init)
subgoal by (rule empty_clauses)
subgoal for b T
by (rule extract_atms_clss_nempty)
subgoal premises p for b _ _ T
using p(6-)
by (cases T)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal premises p for b _ _ T
using p(6-)
by (cases T)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal premises p for b _ _ T
using p(6-)
by (cases T)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for b T
by (rule cdcl_twl_stgy_restart_prog)
subgoal for b T
by (rule conflict_during_init)
subgoal by (rule empty_clauses)
subgoal for b T
by (rule extract_atms_clss_nempty)
subgoal for b T
by (cases T)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for b T
by (cases T)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for b T
by (cases T)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for b T
by (rule cdcl_twl_stgy_restart_prog_early)
done
qed
definition SAT_l :: ‹nat clause_l list ⇒ nat twl_st_l nres› where
‹SAT_l CS = do{
b ← SPEC(λ_::bool. True);
if b then do {
let S = init_state_l;
T ← init_dt CS (to_init_state_l S);
let T = fst T;
if get_conflict_l T ≠ None
then RETURN T
else if CS = [] then RETURN (fst init_state_l)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update_l T = {#});
ASSERT(mset `# ran_mf (get_clauses_l T) + get_unit_clauses_l T +
get_subsumed_clauses_l T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_l T) = {#});
cdcl_twl_stgy_restart_prog_l T
}
}
else do {
let S = init_state_l;
T ← init_dt CS (to_init_state_l S);
failed ← SPEC (λ_ :: bool. True);
if failed then do {
T ← init_dt CS (to_init_state_l S);
let T = fst T;
if get_conflict_l T ≠ None
then RETURN T
else if CS = [] then RETURN (fst init_state_l)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update_l T = {#});
ASSERT(mset `# ran_mf (get_clauses_l T) + get_unit_clauses_l T +
get_subsumed_clauses_l T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_l T) = {#});
cdcl_twl_stgy_restart_prog_l T
}
} else do {
let T = fst T;
if get_conflict_l T ≠ None
then RETURN T
else if CS = [] then RETURN (fst init_state_l)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update_l T = {#});
ASSERT(mset `# ran_mf (get_clauses_l T) + get_unit_clauses_l T +
get_subsumed_clauses_l T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_l T) = {#});
cdcl_twl_stgy_restart_prog_early_l T
}
}
}
}›
lemma SAT_l_SAT0:
assumes dist: ‹Multiset.Ball (mset `# mset CS) distinct_mset›
shows ‹SAT_l CS ≤ ⇓ {(T,T'). (T, T') ∈ twl_st_l None} (SAT0 CS)›
proof -
have inj: ‹inj (uminus :: _ literal ⇒ _)›
by (auto simp: inj_on_def)
have [simp]: ‹{#- lit_of x. x ∈# A#} = {#- lit_of x. x ∈# B#} ⟷
{#lit_of x. x ∈# A#} = {#lit_of x. x ∈# B#}› for A B :: ‹(nat literal, nat literal,
nat) annotated_lit multiset›
unfolding multiset.map_comp[unfolded comp_def, symmetric]
apply (subst inj_image_mset_eq_iff[of uminus])
apply (rule inj)
by (auto simp: inj_on_def)[]
have get_unit_twl_st_l: ‹(s, x) ∈ twl_st_l_init ⟹ get_learned_unit_clauses_l_init s = {#} ⟹
learned_clss_l (get_clauses_l_init s) = {#} ⟹
get_subsumed_learned_clauses_l_init s = {#} ⟹
{#mset (fst x). x ∈# ran_m (get_clauses_l_init s)#} +
(get_unit_clauses_l_init s + get_subsumed_init_clauses_l_init s) =
clause `# get_init_clauses_init x + get_unit_init_clauses_init x +
get_subsumed_init_clauses_init x› for s x
apply (cases s; cases x)
apply (auto simp: twl_st_l_init_def mset_take_mset_drop_mset')
by (metis (mono_tags, lifting) add.right_neutral all_clss_l_ran_m)
have init_dt_pre: ‹init_dt_pre CS (to_init_state_l init_state_l)›
by (rule init_dt_pre_init) (use dist in auto)
have init_dt_spec0: ‹init_dt CS (to_init_state_l init_state_l)
≤ ⇓{((T),T'). (T, T') ∈ twl_st_l_init ∧ twl_list_invs (fst T) ∧
clauses_to_update_l (fst T) = {#}}
(SPEC (init_dt_spec0 CS (to_init_state0 init_state0)))›
apply (rule init_dt_full[THEN order_trans])
subgoal by (rule init_dt_pre)
subgoal
apply (rule RES_refine)
unfolding init_dt_spec_def Set.mem_Collect_eq init_dt_spec0_def
to_init_state_l_def init_state_l_def
to_init_state0_def init_state0_def
apply normalize_goal+
apply (rule_tac x=x in bexI)
subgoal for s x by (auto simp: twl_st_l_init)
subgoal for s x
unfolding Set.mem_Collect_eq
by (simp_all add: twl_st_init twl_st_l_init twl_st_l_init_no_decision_iff get_unit_twl_st_l)
done
done
have init_state0: ‹(fst init_state_l, fst init_state0) ∈ {(T, T'). (T, T') ∈ twl_st_l None}›
by (auto simp: twl_st_l_def init_state0_def init_state_l_def)
show ?thesis
unfolding SAT_l_def SAT0_def
apply (refine_vcg init_dt_spec0)
subgoal by auto
subgoal by (auto simp: twl_st_l_init twl_st_init)
subgoal by (auto simp: twl_st_l_init_alt_def)
subgoal by auto
subgoal by (rule init_state0)
subgoal for b ba T Ta
unfolding all_clss_lf_ran_m[symmetric] image_mset_union to_init_state0_def init_state0_def
by (cases T; cases Ta)
(auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset'
init_dt_spec0_def)
subgoal for b ba T Ta
unfolding all_clss_lf_ran_m[symmetric] image_mset_union
by (cases T; cases Ta)
(auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset')
subgoal for b ba T Ta
by (cases T; cases Ta)
(auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset')
subgoal for b ba T Ta
by (rule cdcl_twl_stgy_restart_prog_l_cdcl_twl_stgy_restart_prog[THEN fref_to_Down, of _ ‹fst Ta›,
THEN order_trans])
(auto simp: twl_st_l_init_alt_def mset_take_mset_drop_mset' intro!: conc_fun_R_mono)
subgoal by (auto simp: twl_st_l_init twl_st_init)
subgoal by (auto simp: twl_st_l_init twl_st_init)
subgoal by (auto simp: twl_st_l_init_alt_def)
subgoal by auto
subgoal by (rule init_state0)
subgoal for b ba _ _ _ _ T Ta
unfolding all_clss_lf_ran_m[symmetric] image_mset_union to_init_state0_def init_state0_def
by (cases T; cases Ta)
(auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset'
init_dt_spec0_def)
subgoal for b ba _ _ _ _ T Ta
unfolding all_clss_lf_ran_m[symmetric] image_mset_union
by (cases T; cases Ta) (auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset')
subgoal for b ba _ _ _ _ T Ta
by (cases T; cases Ta) (auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset')
subgoal for b ba _ _ _ _ T Ta
by (rule cdcl_twl_stgy_restart_prog_l_cdcl_twl_stgy_restart_prog[THEN fref_to_Down, of _ ‹fst Ta›,
THEN order_trans])
(auto simp: twl_st_l_init_alt_def intro!: conc_fun_R_mono)
subgoal by (auto simp: twl_st_l_init twl_st_init)
subgoal by (auto simp: twl_st_l_init_alt_def)
subgoal by auto
subgoal by (rule init_state0)
subgoal by auto
subgoal for b ba T Ta
unfolding all_clss_lf_ran_m[symmetric] image_mset_union
by (cases T; cases Ta) (auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset')
subgoal for b ba T Ta
by (cases T; cases Ta) (auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset')
subgoal for b ba T Ta
by (rule cdcl_twl_stgy_restart_prog_early_l_cdcl_twl_stgy_restart_prog_early[THEN fref_to_Down, of _ ‹fst Ta›,
THEN order_trans])
(auto simp: twl_st_l_init_alt_def intro!: conc_fun_R_mono)
done
qed
definition SAT_wl :: ‹nat clause_l list ⇒ nat twl_st_wl nres› where
‹SAT_wl CS = do{
ASSERT(isasat_input_bounded (mset_set (extract_atms_clss CS {})));
ASSERT(distinct_mset_set (mset ` set CS));
let 𝒜⇩i⇩n' = extract_atms_clss CS {};
b ← SPEC(λ_::bool. True);
if b then do {
let S = init_state_wl;
T ← init_dt_wl' CS (to_init_state S);
T ← rewatch_st (from_init_state T);
if get_conflict_wl T ≠ None
then RETURN T
else if CS = [] then RETURN (([], fmempty, None, {#}, {#}, {#}, {#}, {#}, λ_. undefined))
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT(isasat_input_bounded_nempty (mset_set 𝒜⇩i⇩n'));
ASSERT(mset `# ran_mf (get_clauses_wl T) + get_unit_clauses_wl T +
get_subsumed_clauses_wl T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_wl T) = {#});
cdcl_twl_stgy_restart_prog_wl (finalise_init T)
}
}
else do {
let S = init_state_wl;
T ← init_dt_wl' CS (to_init_state S);
let T = from_init_state T;
failed ← SPEC (λ_ :: bool. True);
if failed then do {
let S = init_state_wl;
T ← init_dt_wl' CS (to_init_state S);
T ← rewatch_st (from_init_state T);
if get_conflict_wl T ≠ None
then RETURN T
else if CS = [] then RETURN (([], fmempty, None, {#}, {#}, {#}, {#}, {#}, λ_. undefined))
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT(isasat_input_bounded_nempty (mset_set 𝒜⇩i⇩n'));
ASSERT(mset `# ran_mf (get_clauses_wl T) + get_unit_clauses_wl T +
get_subsumed_clauses_wl T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_wl T) = {#});
cdcl_twl_stgy_restart_prog_wl (finalise_init T)
}
} else do {
if get_conflict_wl T ≠ None
then RETURN T
else if CS = [] then RETURN (([], fmempty, None, {#}, {#}, {#}, {#}, {#}, λ_. undefined))
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT(isasat_input_bounded_nempty (mset_set 𝒜⇩i⇩n'));
ASSERT(mset `# ran_mf (get_clauses_wl T) + get_unit_clauses_wl T +
get_subsumed_clauses_wl T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_wl T) = {#});
T ← rewatch_st (finalise_init T);
cdcl_twl_stgy_restart_prog_early_wl T
}
}
}
}›
lemma SAT_l_alt_def:
‹SAT_l CS = do{
𝒜 ← RETURN (); ⌦‹atoms›
b ← SPEC(λ_::bool. True);
if b then do {
let S = init_state_l;
𝒜 ← RETURN (); ⌦‹initialisation›
T ← init_dt CS (to_init_state_l S); ⌦‹rewatch›
let T = fst T;
if get_conflict_l T ≠ None
then RETURN T
else if CS = [] then RETURN (fst init_state_l)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update_l T = {#});
ASSERT(mset `# ran_mf (get_clauses_l T) + get_unit_clauses_l T +
get_subsumed_clauses_l T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_l T) = {#});
cdcl_twl_stgy_restart_prog_l T
}
}
else do {
let S = init_state_l;
𝒜 ← RETURN (); ⌦‹initialisation›
T ← init_dt CS (to_init_state_l S);
failed ← SPEC (λ_ :: bool. True);
if failed then do {
let S = init_state_l;
𝒜 ← RETURN (); ⌦‹initialisation›
T ← init_dt CS (to_init_state_l S);
let T = T;
if get_conflict_l_init T ≠ None
then RETURN (fst T)
else if CS = [] then RETURN (fst init_state_l)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update_l (fst T) = {#});
ASSERT(mset `# ran_mf (get_clauses_l (fst T)) + get_unit_clauses_l (fst T) +
get_subsumed_clauses_l (fst T) = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_l (fst T)) = {#});
let T = fst T;
cdcl_twl_stgy_restart_prog_l T
}
} else do {
let T = T;
if get_conflict_l_init T ≠ None
then RETURN (fst T)
else if CS = [] then RETURN (fst init_state_l)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update_l (fst T) = {#});
ASSERT(mset `# ran_mf (get_clauses_l (fst T)) + get_unit_clauses_l (fst T) +
get_subsumed_clauses_l (fst T) = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_l (fst T)) = {#});
let T = fst T;
cdcl_twl_stgy_restart_prog_early_l T
}
}
}
}›
unfolding SAT_l_def by (auto cong: if_cong Let_def twl_st_l_init)
lemma init_dt_wl_full_init_dt_wl_spec_full:
assumes ‹init_dt_wl_pre CS S› and ‹init_dt_pre CS S'› and
‹(S, S') ∈ state_wl_l_init› and ‹∀C∈set CS. distinct C›
shows ‹init_dt_wl_full CS S ≤ ⇓ {(S, S'). (fst S, fst S') ∈ state_wl_l None} (init_dt CS S')›
proof -
have init_dt_wl: ‹init_dt_wl CS S ≤ SPEC (λT. RETURN T ≤ ⇓ state_wl_l_init (init_dt CS S') ∧
init_dt_wl_spec CS S T)›
apply (rule SPEC_rule_conjI)
apply (rule order_trans)
apply (rule init_dt_wl_init_dt[of S S'])
subgoal by (rule assms)
subgoal by (rule assms)
apply (rule no_fail_spec_le_RETURN_itself)
subgoal
apply (rule SPEC_nofail)
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule init_dt_full)
using assms by (auto simp: conc_fun_RES init_dt_wl_pre_def)
subgoal
apply (rule order_trans)
apply (rule init_dt_wl_init_dt_wl_spec)
apply (rule assms)
apply simp
done
done
show ?thesis
unfolding init_dt_wl_full_def
apply (rule specify_left)
apply (rule init_dt_wl)
subgoal for x
apply (cases x, cases ‹fst x›)
apply (simp only: prod.case fst_conv)
apply normalize_goal+
apply (rule specify_left)
apply (rule_tac M =aa and N=ba and C=c and NE=d and UE=e and NS=f and US=g and Q=h in
rewatch_correctness[OF _ init_dt_wl_spec_rewatch_pre])
subgoal by rule
apply (assumption)
apply (auto)[3]
apply (cases ‹init_dt CS S'›)
apply (auto simp: RETURN_RES_refine_iff state_wl_l_def state_wl_l_init_def
state_wl_l_init'_def)
done
done
qed
lemma init_dt_wl_pre:
assumes dist: ‹Multiset.Ball (mset `# mset CS) distinct_mset›
shows ‹init_dt_wl_pre CS (to_init_state init_state_wl)›
unfolding init_dt_wl_pre_def to_init_state_def init_state_wl_def
apply (rule exI[of _ ‹(([], fmempty, None, {#}, {#}, {#}, {#}, {#}, {#}), {#})›])
apply (intro conjI)
apply (auto simp: init_dt_pre_def state_wl_l_init_def state_wl_l_init'_def)[]
unfolding init_dt_pre_def
apply (rule exI[of _ ‹(([], {#}, {#}, None, {#}, {#}, {#}, {#}, {#}, {#}), {#})›])
using dist by (auto simp: init_dt_pre_def state_wl_l_init_def state_wl_l_init'_def
twl_st_l_init_def twl_init_invs)[]
lemma SAT_wl_SAT_l:
assumes
dist: ‹Multiset.Ball (mset `# mset CS) distinct_mset› and
bounded: ‹isasat_input_bounded (mset_set (⋃C∈set CS. atm_of ` set C))›
shows ‹SAT_wl CS ≤ ⇓ {(T,T'). (T, T') ∈ state_wl_l None} (SAT_l CS)›
proof -
have extract_atms_clss: ‹(extract_atms_clss CS {}, ()) ∈ {(x, _). x = extract_atms_clss CS {}}›
by auto
have init_dt_wl_pre: ‹init_dt_wl_pre CS (to_init_state init_state_wl)›
by (rule init_dt_wl_pre) (use dist in auto)
have init_rel: ‹(to_init_state init_state_wl, to_init_state_l init_state_l)
∈ state_wl_l_init›
by (auto simp: init_dt_pre_def state_wl_l_init_def state_wl_l_init'_def
twl_st_l_init_def twl_init_invs to_init_state_def init_state_wl_def
init_state_l_def to_init_state_l_def)[]
define init_dt_wl_rel where
‹init_dt_wl_rel S ≡ ({(T, T'). RETURN T ≤ init_dt_wl' CS S ∧ T' = ()})› for S
have init_dt_wl':
‹init_dt_wl' CS S ≤ SPEC (λc. (c, ()) ∈ (init_dt_wl_rel S))›
if
‹init_dt_wl_pre CS S› and
‹(S, S') ∈ state_wl_l_init› and
‹∀C∈set CS. distinct C›
for S S'
proof -
have [simp]: ‹(U, U') ∈ ({(T, T'). RETURN T ≤ init_dt_wl' CS S ∧ remove_watched T = T'} O
state_wl_l_init) ⟷ ((U, U') ∈ {(T, T'). remove_watched T = T'} O
state_wl_l_init ∧ RETURN U ≤ init_dt_wl' CS S)› for S S' U U'
by auto
have H: ‹A ≤ ⇓ ({(S, S'). P S S'}) B ⟷ A ≤ ⇓ ({(S, S'). RETURN S ≤ A ∧ P S S'}) B›
for A B P R
by (simp add: pw_conc_inres pw_conc_nofail pw_le_iff p2rel_def)
have nofail: ‹nofail (init_dt_wl' CS S)›
apply (rule SPEC_nofail)
apply (rule order_trans)
apply (rule init_dt_wl'_spec[unfolded conc_fun_RES])
using that by auto
have H: ‹A ≤ ⇓ ({(S, S'). P S S'} O R) B ⟷ A ≤ ⇓ ({(S, S'). RETURN S ≤ A ∧ P S S'} O R) B›
for A B P R
by (smt Collect_cong H case_prod_cong conc_fun_chain)
show ?thesis
unfolding init_dt_wl_rel_def
using that
by (auto simp: nofail no_fail_spec_le_RETURN_itself)
qed
have rewatch_st: ‹rewatch_st (from_init_state T) ≤
⇓ ({(S, S'). (S, fst S') ∈ state_wl_l None ∧ correct_watching S ∧
literals_are_ℒ⇩i⇩n (all_atms_st (finalise_init S)) (finalise_init S)})
(init_dt CS (to_init_state_l init_state_l))›
(is ‹_ ≤ ⇓ ?rewatch _›)
if ‹(extract_atms_clss CS {}, 𝒜) ∈ {(x, _). x = extract_atms_clss CS {}}› and
‹(T, Ta) ∈ init_dt_wl_rel (to_init_state init_state_wl)›
for T Ta and 𝒜 :: unit
proof -
have le_wa: ‹⇓ {(T, T'). T = append_empty_watched T'} A =
(do {S ← A; RETURN (append_empty_watched S)})› for A R
by (cases A)
(auto simp: conc_fun_RES RES_RETURN_RES image_iff)
have init': ‹init_dt_pre CS (to_init_state_l init_state_l)›
by (rule init_dt_pre_init) (use assms in auto)
have H: ‹do {T ← RETURN T; rewatch_st (from_init_state T)} ≤
⇓{(S', T'). S' = fst T'} (init_dt_wl_full CS (to_init_state init_state_wl))›
using that unfolding init_dt_wl_full_def init_dt_wl_rel_def init_dt_wl'_def apply -
apply (rule bind_refine[of _ ‹{(T', T''). T' = append_empty_watched T''}›])
apply (subst le_wa)
apply (auto simp: rewatch_st_def from_init_state_def intro!: bind_refine[of _ Id])
done
have [intro]: ‹correct_watching_init (af, ag, None, ai, aj, NS, US, {#}, ba) ⟹
blits_in_ℒ⇩i⇩n (af, ag, ah, ai, aj, NS, US, ak, ba)› for af ag ah ai aj ak ba NS US
by (auto simp: correct_watching_init.simps blits_in_ℒ⇩i⇩n_def
all_blits_are_in_problem_init.simps all_lits_def
in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n in_all_lits_of_mm_ain_atms_of_iff
atm_of_all_lits_of_mm)
have ‹rewatch_st (from_init_state T)
≤ ⇓ {(S, S'). (S, fst S') ∈ state_wl_l None}
(init_dt CS (to_init_state_l init_state_l))›
apply (rule H[simplified, THEN order_trans])
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule init_dt_wl_full_init_dt_wl_spec_full)
subgoal by (rule init_dt_wl_pre)
apply (rule init')
subgoal by (auto simp: to_init_state_def init_state_wl_def to_init_state_l_def
init_state_l_def state_wl_l_init_def state_wl_l_init'_def)
subgoal using assms by auto
by (auto intro!: conc_fun_R_mono simp: conc_fun_chain)
moreover have ‹rewatch_st (from_init_state T) ≤ SPEC (λS. correct_watching S ∧
literals_are_ℒ⇩i⇩n (all_atms_st (finalise_init S)) (finalise_init S))›
apply (rule H[simplified, THEN order_trans])
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule Watched_Literals_Watch_List_Initialisation.init_dt_wl_full_init_dt_wl_spec_full)
subgoal by (rule init_dt_wl_pre)
by (auto simp: conc_fun_RES init_dt_wl_spec_full_def correct_watching_init_correct_watching
finalise_init_def literals_are_ℒ⇩i⇩n_def is_ℒ⇩a⇩l⇩l_def ℒ⇩a⇩l⇩l_all_atms_all_lits)
ultimately show ?thesis
by (rule add_invar_refineI_P)
qed
have cdcl_twl_stgy_restart_prog_wl_D: ‹cdcl_twl_stgy_restart_prog_wl (finalise_init U)
≤ ⇓ {(T, T'). (T, T') ∈ state_wl_l None}
(cdcl_twl_stgy_restart_prog_l (fst U'))›
if
‹(extract_atms_clss CS {}, (𝒜::unit)) ∈ {(x, _). x = extract_atms_clss CS {}}› and
UU': ‹(U, U') ∈ ?rewatch› and
‹¬ get_conflict_wl U ≠ None› and
‹¬ get_conflict_l (fst U') ≠ None› and
‹CS ≠ []› and
‹CS ≠ []› and
‹extract_atms_clss CS {} ≠ {}› and
‹clauses_to_update_l (fst U') = {#}› and
‹mset `# ran_mf (get_clauses_l (fst U')) + get_unit_clauses_l (fst U') +
get_subsumed_clauses_l (fst U') =
mset `# mset CS› and
‹learned_clss_l (get_clauses_l (fst U')) = {#}› and
‹extract_atms_clss CS {} ≠ {}› and
‹isasat_input_bounded_nempty (mset_set (extract_atms_clss CS {}))› and
‹mset `# ran_mf (get_clauses_wl U) + get_unit_clauses_wl U + get_subsumed_clauses_wl U=
mset `# mset CS›
for 𝒜 T Ta U U'
proof -
have 1: ‹ {(T, T'). (T, T') ∈ state_wl_l None} = state_wl_l None›
by auto
have lits: ‹literals_are_ℒ⇩i⇩n (all_atms_st (finalise_init U)) (finalise_init U)›
using UU' by (auto simp: finalise_init_def)
show ?thesis
apply (rule cdcl_twl_stgy_restart_prog_wl_spec[unfolded fref_param1, THEN fref_to_Down, THEN order_trans])
apply fast
using UU' by (auto simp: finalise_init_def)
qed
have conflict_during_init:
‹(([], fmempty, None, {#}, {#}, {#}, {#}, {#}, λ_. undefined), fst init_state_l)
∈ {(T, T'). (T, T') ∈ state_wl_l None}›
by (auto simp: init_state_l_def state_wl_l_def)
have init_init_dt: ‹RETURN (from_init_state T)
≤ ⇓ ({(S, S'). S = fst S'} O {(S :: nat twl_st_wl_init_full, S' :: nat twl_st_wl_init).
remove_watched S = S'} O state_wl_l_init)
(init_dt CS (to_init_state_l init_state_l))›
(is ‹_ ≤ ⇓ ?init_dt _ ›)
if
‹(extract_atms_clss CS {}, (𝒜::unit)) ∈ {(x, _). x = extract_atms_clss CS {}}› and
‹(T, Ta) ∈ init_dt_wl_rel (to_init_state init_state_wl)›
for 𝒜 T Ta
proof -
have 1: ‹RETURN T ≤ init_dt_wl' CS (to_init_state init_state_wl)›
using that by (auto simp: init_dt_wl_rel_def from_init_state_def)
have 2: ‹RETURN (from_init_state T) ≤ ⇓ {(S, S'). S = fst S'} (RETURN T)›
by (auto simp: RETURN_refine from_init_state_def)
have 2: ‹RETURN (from_init_state T) ≤ ⇓ {(S, S'). S = fst S'} (init_dt_wl' CS (to_init_state init_state_wl))›
apply (rule 2[THEN order_trans])
apply (rule ref_two_step')
apply (rule 1)
done
show ?thesis
apply (rule order_trans)
apply (rule 2)
unfolding conc_fun_chain[symmetric]
apply (rule ref_two_step')
unfolding conc_fun_chain
apply (rule init_dt_wl'_init_dt)
apply (rule init_dt_wl_pre)
subgoal by (auto simp: to_init_state_def init_state_wl_def to_init_state_l_def
init_state_l_def state_wl_l_init_def state_wl_l_init'_def)
subgoal using assms by auto
done
qed
have rewatch_st_fst: ‹rewatch_st (finalise_init (from_init_state T))
≤ SPEC (λc. (c, fst Ta) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ⇩i⇩n S})›
(is ‹_ ≤ SPEC ?rewatch›)
if
‹(extract_atms_clss CS {}, 𝒜) ∈ {(x, _). x = extract_atms_clss CS {}}› and
T: ‹(T, 𝒜') ∈ init_dt_wl_rel (to_init_state init_state_wl)› and
T_Ta: ‹(from_init_state T, Ta)
∈ {(S, S'). S = fst S'} O
{(S, S'). remove_watched S = S'} O state_wl_l_init› and
‹¬ get_conflict_wl (from_init_state T) ≠ None› and
‹¬ get_conflict_l_init Ta ≠ None›
for 𝒜 b ba T 𝒜' Ta bb bc
proof -
have 1: ‹RETURN T ≤ init_dt_wl' CS (to_init_state init_state_wl)›
using T unfolding init_dt_wl_rel_def by auto
have 2: ‹RETURN T ≤ ⇓ {(S, S'). remove_watched S = S'}
(SPEC (init_dt_wl_spec CS (to_init_state init_state_wl)))›
using order_trans[OF 1 init_dt_wl'_spec[OF init_dt_wl_pre]] .
have empty_watched: ‹get_watched_wl (finalise_init (from_init_state T)) = (λ_. [])›
using 1 2 init_dt_wl'_spec[OF init_dt_wl_pre]
by (cases T; cases ‹init_dt_wl CS (init_state_wl, {#})›)
(auto simp: init_dt_wl_spec_def RETURN_RES_refine_iff
finalise_init_def from_init_state_def state_wl_l_init_def
state_wl_l_init'_def to_init_state_def to_init_state_l_def
init_state_l_def init_dt_wl'_def RES_RETURN_RES)
have 1: ‹length (aa ∝ x) ≥ 2› ‹distinct (aa ∝ x)›
if
struct: ‹twl_struct_invs_init
((af,
{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l aa#},
{#}, y, ac, {#}, NS, US, {#}, ae),
OC)› and
x: ‹x ∈# dom_m aa› and
learned: ‹learned_clss_l aa = {#}›
for af aa y ac ae x OC NS US
proof -
have irred: ‹irred aa x›
using that by (cases ‹fmlookup aa x›) (auto simp: ran_m_def dest!: multi_member_split
split: if_splits)
have ‹Multiset.Ball
({#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l aa#} +
{#})
struct_wf_twl_cls›
using struct unfolding twl_struct_invs_init_def fst_conv twl_st_inv.simps
by fast
then show ‹length (aa ∝ x) ≥ 2› ‹distinct (aa ∝ x)›
using x learned in_ran_mf_clause_inI[OF x, of True] irred
by (auto simp: mset_take_mset_drop_mset' dest!: multi_member_split[of x]
split: if_splits)
qed
have min_len: ‹x ∈# dom_m (get_clauses_wl (finalise_init (from_init_state T))) ⟹
distinct (get_clauses_wl (finalise_init (from_init_state T)) ∝ x) ∧
2 ≤ length (get_clauses_wl (finalise_init (from_init_state T)) ∝ x)›
for x
using 2
by (cases T)
(auto simp: init_dt_wl_spec_def RETURN_RES_refine_iff
finalise_init_def from_init_state_def state_wl_l_init_def
state_wl_l_init'_def to_init_state_def to_init_state_l_def
init_state_l_def init_dt_wl'_def RES_RETURN_RES
init_dt_spec_def init_state_wl_def twl_st_l_init_def
intro: 1)
show ?thesis
apply (rule rewatch_st_correctness[THEN order_trans])
subgoal by (rule empty_watched)
subgoal by (rule min_len)
subgoal using T_Ta by (auto simp: finalise_init_def
state_wl_l_init_def state_wl_l_init'_def state_wl_l_def
correct_watching_init_correct_watching
correct_watching_init_blits_in_ℒ⇩i⇩n)
done
qed
have cdcl_twl_stgy_restart_prog_wl_D2: ‹cdcl_twl_stgy_restart_prog_wl U'
≤ ⇓ {(T, T'). (T, T') ∈ state_wl_l None}
(cdcl_twl_stgy_restart_prog_l (fst T'))› (is ?A) and
cdcl_twl_stgy_restart_prog_early_wl_D2: ‹cdcl_twl_stgy_restart_prog_early_wl U'
≤ ⇓ {(T, T'). (T, T') ∈ state_wl_l None}
(cdcl_twl_stgy_restart_prog_early_l (fst T'))› (is ?B)
if
U': ‹(U', fst T') ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ⇩i⇩n S}›
for 𝒜 b b' T 𝒜' T' c c' U'
proof -
have 1: ‹ {(T, T'). (T, T') ∈ state_wl_l None} = state_wl_l None›
by auto
have lits: ‹literals_are_ℒ⇩i⇩n (all_atms_st (U')) (U')›
using U' by (auto simp: finalise_init_def correct_watching.simps)
show ?A
apply (rule cdcl_twl_stgy_restart_prog_wl_spec[unfolded fref_param1, THEN fref_to_Down, THEN order_trans])
apply fast
using U' by (auto simp: finalise_init_def)
show ?B
apply (rule cdcl_twl_stgy_restart_prog_early_wl_spec[unfolded fref_param1, THEN fref_to_Down, THEN order_trans])
apply fast
using U' by (auto simp: finalise_init_def)
qed
have all_le: ‹∀C∈set CS. ∀L∈set C. nat_of_lit L ≤ uint32_max›
proof (intro ballI)
fix C L
assume ‹C ∈ set CS› and ‹L ∈ set C›
then have ‹L ∈# ℒ⇩a⇩l⇩l (mset_set (⋃C∈set CS. atm_of ` set C))›
by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
then show ‹nat_of_lit L ≤ uint32_max›
using assms by auto
qed
have [simp]: ‹(Tc, fst Td) ∈ state_wl_l None ⟹
get_conflict_l_init Td = get_conflict_wl Tc› for Tc Td
by (cases Tc; cases Td; auto simp: state_wl_l_def)
show ?thesis
unfolding SAT_wl_def SAT_l_alt_def
apply (refine_vcg extract_atms_clss init_dt_wl' init_rel)
subgoal using assms unfolding extract_atms_clss_alt_def by auto
subgoal using assms unfolding distinct_mset_set_def by auto
subgoal by auto
subgoal by (rule init_dt_wl_pre)
subgoal using dist by auto
apply (rule rewatch_st; assumption)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (rule conflict_during_init)
subgoal using bounded by (auto simp: isasat_input_bounded_nempty_def extract_atms_clss_alt_def
simp del: isasat_input_bounded_def)
subgoal by auto
subgoal by auto
subgoal for 𝒜 b ba T Ta U U'
by (rule cdcl_twl_stgy_restart_prog_wl_D)
subgoal by (rule init_dt_wl_pre)
subgoal using dist by auto
apply (rule init_init_dt; assumption)
subgoal by auto
subgoal by (rule init_dt_wl_pre)
subgoal using dist by auto
apply (rule rewatch_st; assumption)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (rule conflict_during_init)
subgoal using bounded by (auto simp: isasat_input_bounded_nempty_def extract_atms_clss_alt_def
simp del: isasat_input_bounded_def)
subgoal by auto
subgoal by auto
subgoal for 𝒜 b ba T Ta U U'
unfolding twl_st_l_init[symmetric]
by (rule cdcl_twl_stgy_restart_prog_wl_D)
subgoal by (auto simp: from_init_state_def state_wl_l_init_def state_wl_l_init'_def)
subgoal for 𝒜 b ba T Ta U U'
by (cases U'; cases U)
(auto simp: from_init_state_def state_wl_l_init_def state_wl_l_init'_def
state_wl_l_def)
subgoal by (auto simp: from_init_state_def state_wl_l_init_def state_wl_l_init'_def)
subgoal by (rule conflict_during_init)
subgoal using bounded by (auto simp: isasat_input_bounded_nempty_def extract_atms_clss_alt_def
simp del: isasat_input_bounded_def)
subgoal for 𝒜 b ba U 𝒜' T' bb bc
by (cases U; cases T')
(auto simp: state_wl_l_init_def state_wl_l_init'_def)
subgoal for 𝒜 b ba T 𝒜' T' bb bc
by (auto simp: state_wl_l_init_def state_wl_l_init'_def)
apply (rule rewatch_st_fst; assumption)
subgoal by (rule cdcl_twl_stgy_restart_prog_early_wl_D2)
done
qed
definition extract_model_of_state where
‹extract_model_of_state U = Some (map lit_of (get_trail_wl U))›
definition extract_model_of_state_heur where
‹extract_model_of_state_heur U = Some (fst (get_trail_wl_heur U))›
definition extract_stats where
[simp]: ‹extract_stats U = None›
definition extract_stats_init where
[simp]: ‹extract_stats_init = None›
definition IsaSAT :: ‹nat clause_l list ⇒ nat literal list option nres› where
‹IsaSAT CS = do{
S ← SAT_wl CS;
RETURN (if get_conflict_wl S = None then extract_model_of_state S else extract_stats S)
}›
lemma IsaSAT_alt_def:
‹IsaSAT CS = do{
ASSERT(isasat_input_bounded (mset_set (extract_atms_clss CS {})));
ASSERT(distinct_mset_set (mset ` set CS));
let 𝒜⇩i⇩n' = extract_atms_clss CS {};
_ ← RETURN ();
b ← SPEC(λ_::bool. True);
if b then do {
let S = init_state_wl;
T ← init_dt_wl' CS (to_init_state S);
T ← rewatch_st (from_init_state T);
if get_conflict_wl T ≠ None
then RETURN (extract_stats T)
else if CS = [] then RETURN (Some [])
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT(isasat_input_bounded_nempty (mset_set 𝒜⇩i⇩n'));
ASSERT(mset `# ran_mf (get_clauses_wl T) + get_unit_clauses_wl T +
get_subsumed_clauses_wl T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_wl T) = {#});
T ← RETURN (finalise_init T);
S ← cdcl_twl_stgy_restart_prog_wl (T);
RETURN (if get_conflict_wl S = None then extract_model_of_state S else extract_stats S)
}
}
else do {
let S = init_state_wl;
T ← init_dt_wl' CS (to_init_state S);
failed ← SPEC (λ_ :: bool. True);
if failed then do {
let S = init_state_wl;
T ← init_dt_wl' CS (to_init_state S);
T ← rewatch_st (from_init_state T);
if get_conflict_wl T ≠ None
then RETURN (extract_stats T)
else if CS = [] then RETURN (Some [])
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT(isasat_input_bounded_nempty (mset_set 𝒜⇩i⇩n'));
ASSERT(mset `# ran_mf (get_clauses_wl T) + get_unit_clauses_wl T +
get_subsumed_clauses_wl T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_wl T) = {#});
let T = finalise_init T;
S ← cdcl_twl_stgy_restart_prog_wl T;
RETURN (if get_conflict_wl S = None then extract_model_of_state S else extract_stats S)
}
} else do {
let T = from_init_state T;
if get_conflict_wl T ≠ None
then RETURN (extract_stats T)
else if CS = [] then RETURN (Some [])
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT(isasat_input_bounded_nempty (mset_set 𝒜⇩i⇩n'));
ASSERT(mset `# ran_mf (get_clauses_wl T) + get_unit_clauses_wl T +
get_subsumed_clauses_wl T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_wl T) = {#});
T ← rewatch_st T;
T ← RETURN (finalise_init T);
S ← cdcl_twl_stgy_restart_prog_early_wl T;
RETURN (if get_conflict_wl S = None then extract_model_of_state S else extract_stats S)
}
}
}
}› (is ‹?A = ?B›) for CS opts
proof -
have H: ‹A = B ⟹ A ≤ ⇓ Id B› for A B
by auto
have 1: ‹?A ≤ ⇓ Id ?B›
unfolding IsaSAT_def SAT_wl_def nres_bind_let_law If_bind_distrib nres_monad_laws
Let_def finalise_init_def
apply (refine_vcg)
subgoal by auto
apply (rule H; solves auto)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: extract_model_of_state_def)
subgoal by auto
subgoal by auto
apply (rule H; solves auto)
subgoal by auto
subgoal by auto
apply (rule H; solves auto)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: extract_model_of_state_def)
subgoal by auto
subgoal by auto
apply (rule H; solves auto)
subgoal by (auto simp: extract_model_of_state_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: extract_model_of_state_def)
subgoal by auto
subgoal by auto
apply (rule H; solves auto)
apply (rule H; solves auto)
subgoal by auto
done
have 2: ‹?B ≤ ⇓ Id ?A›
unfolding IsaSAT_def SAT_wl_def nres_bind_let_law If_bind_distrib nres_monad_laws
Let_def finalise_init_def
apply (refine_vcg)
subgoal by auto
apply (rule H; solves auto)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: extract_model_of_state_def)
subgoal by auto
subgoal by auto
apply (rule H; solves auto)
subgoal by auto
subgoal by auto
apply (rule H; solves auto)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: extract_model_of_state_def)
subgoal by auto
subgoal by auto
apply (rule H; solves auto)
subgoal by (auto simp: extract_model_of_state_def)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: extract_model_of_state_def)
subgoal by auto
subgoal by auto
apply (rule H; solves auto)
apply (rule H; solves auto)
subgoal by auto
done
show ?thesis
using 1 2 by simp
qed
definition extract_model_of_state_stat :: ‹twl_st_wl_heur ⇒ bool × nat literal list × stats› where
‹extract_model_of_state_stat U =
(False, (fst (get_trail_wl_heur U)),
(λ(M, _, _, _, _ ,_ ,_ ,_, _, _, stat, _, _). stat) U)›
definition extract_state_stat :: ‹twl_st_wl_heur ⇒ bool × nat literal list × stats› where
‹extract_state_stat U =
(True, [],
(λ(M, _, _, _, _ ,_ ,_ ,_, _, _, stat, _, _). stat) U)›
definition empty_conflict :: ‹nat literal list option› where
‹empty_conflict = Some []›
definition empty_conflict_code :: ‹(bool × _ list × stats) nres› where
‹empty_conflict_code = do{
let M0 = [];
RETURN (False, M0, (0, 0, 0, 0, 0, 0, 0,
0))}›
definition empty_init_code :: ‹bool × _ list × stats› where
‹empty_init_code = (True, [], (0, 0, 0, 0,
0, 0, 0, 0))›
definition convert_state where
‹convert_state _ S = S›
definition IsaSAT_use_fast_mode where
‹IsaSAT_use_fast_mode = True›
definition isasat_fast_init :: ‹twl_st_wl_heur_init ⇒ bool› where
‹isasat_fast_init S ⟷ (length (get_clauses_wl_heur_init S) ≤ sint64_max - (uint32_max div 2 + 6))›
definition IsaSAT_heur :: ‹opts ⇒ nat clause_l list ⇒ (bool × nat literal list × stats) nres› where
‹IsaSAT_heur opts CS = do{
ASSERT(isasat_input_bounded (mset_set (extract_atms_clss CS {})));
ASSERT(∀C∈set CS. ∀L∈set C. nat_of_lit L ≤ uint32_max);
let 𝒜⇩i⇩n' = mset_set (extract_atms_clss CS {});
ASSERT(isasat_input_bounded 𝒜⇩i⇩n');
ASSERT(distinct_mset 𝒜⇩i⇩n');
let 𝒜⇩i⇩n'' = virtual_copy 𝒜⇩i⇩n';
let b = opts_unbounded_mode opts;
if b
then do {
S ← init_state_wl_heur 𝒜⇩i⇩n';
(T::twl_st_wl_heur_init) ← init_dt_wl_heur True CS S;
T ← rewatch_heur_st T;
let T = convert_state 𝒜⇩i⇩n'' T;
if ¬get_conflict_wl_is_None_heur_init T
then RETURN (empty_init_code)
else if CS = [] then empty_conflict_code
else do {
ASSERT(𝒜⇩i⇩n'' ≠ {#});
ASSERT(isasat_input_bounded_nempty 𝒜⇩i⇩n'');
_ ← isasat_information_banner T;
ASSERT((λ(M', N', D', Q', W', ((ns, m, fst_As, lst_As, next_search), to_remove), φ, clvls). fst_As ≠ None ∧
lst_As ≠ None) T);
T ← finalise_init_code opts (T::twl_st_wl_heur_init);
U ← cdcl_twl_stgy_restart_prog_wl_heur T;
RETURN (if get_conflict_wl_is_None_heur U then extract_model_of_state_stat U
else extract_state_stat U)
}
}
else do {
S ← init_state_wl_heur_fast 𝒜⇩i⇩n';
(T::twl_st_wl_heur_init) ← init_dt_wl_heur False CS S;
let failed = is_failed_heur_init T ∨ ¬isasat_fast_init T;
if failed then do {
let 𝒜⇩i⇩n' = mset_set (extract_atms_clss CS {});
S ← init_state_wl_heur 𝒜⇩i⇩n';
(T::twl_st_wl_heur_init) ← init_dt_wl_heur True CS S;
let T = convert_state 𝒜⇩i⇩n'' T;
T ← rewatch_heur_st T;
if ¬get_conflict_wl_is_None_heur_init T
then RETURN (empty_init_code)
else if CS = [] then empty_conflict_code
else do {
ASSERT(𝒜⇩i⇩n'' ≠ {#});
ASSERT(isasat_input_bounded_nempty 𝒜⇩i⇩n'');
_ ← isasat_information_banner T;
ASSERT((λ(M', N', D', Q', W', ((ns, m, fst_As, lst_As, next_search), to_remove), φ, clvls). fst_As ≠ None ∧
lst_As ≠ None) T);
T ← finalise_init_code opts (T::twl_st_wl_heur_init);
U ← cdcl_twl_stgy_restart_prog_wl_heur T;
RETURN (if get_conflict_wl_is_None_heur U then extract_model_of_state_stat U
else extract_state_stat U)
}
}
else do {
let T = convert_state 𝒜⇩i⇩n'' T;
if ¬get_conflict_wl_is_None_heur_init T
then RETURN (empty_init_code)
else if CS = [] then empty_conflict_code
else do {
ASSERT(𝒜⇩i⇩n'' ≠ {#});
ASSERT(isasat_input_bounded_nempty 𝒜⇩i⇩n'');
_ ← isasat_information_banner T;
ASSERT((λ(M', N', D', Q', W', ((ns, m, fst_As, lst_As, next_search), to_remove), φ, clvls). fst_As ≠ None ∧
lst_As ≠ None) T);
ASSERT(rewatch_heur_st_fast_pre T);
T ← rewatch_heur_st_fast T;
ASSERT(isasat_fast_init T);
T ← finalise_init_code opts (T::twl_st_wl_heur_init);
ASSERT(isasat_fast T);
U ← cdcl_twl_stgy_restart_prog_early_wl_heur T;
RETURN (if get_conflict_wl_is_None_heur U then extract_model_of_state_stat U
else extract_state_stat U)
}
}
}
}›
lemma fref_to_Down_unRET_uncurry0_SPEC:
assumes ‹(λ_. (f), λ_. (RETURN g)) ∈ [P]⇩f unit_rel → ⟨B⟩nres_rel› and ‹P ()›
shows ‹f ≤ SPEC (λc. (c, g) ∈ B)›
proof -
have [simp]: ‹RES (B¯ `` {g}) = SPEC (λc. (c, g) ∈ B)›
by auto
show ?thesis
using assms
unfolding fref_def uncurry_def nres_rel_def RETURN_def
by (auto simp: conc_fun_RES Image_iff)
qed
lemma fref_to_Down_unRET_SPEC:
assumes ‹(f, RETURN o g) ∈ [P]⇩f A → ⟨B⟩nres_rel› and
‹P y› and
‹(x, y) ∈ A›
shows ‹f x ≤ SPEC (λc. (c, g y) ∈ B)›
proof -
have [simp]: ‹RES (B¯ `` {g}) = SPEC (λc. (c, g) ∈ B)› for g
by auto
show ?thesis
using assms
unfolding fref_def uncurry_def nres_rel_def RETURN_def
by (auto simp: conc_fun_RES Image_iff)
qed
lemma fref_to_Down_unRET_curry_SPEC:
assumes ‹(uncurry f, uncurry (RETURN oo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel› and
‹P (x, y)› and
‹((x', y'), (x, y)) ∈ A›
shows ‹f x' y' ≤ SPEC (λc. (c, g x y) ∈ B)›
proof -
have [simp]: ‹RES (B¯ `` {g}) = SPEC (λc. (c, g) ∈ B)› for g
by auto
show ?thesis
using assms
unfolding fref_def uncurry_def nres_rel_def RETURN_def
by (auto simp: conc_fun_RES Image_iff)
qed
lemma all_lits_of_mm_empty_iff: ‹all_lits_of_mm A = {#} ⟷ (∀C ∈# A. C = {#})›
apply (induction A)
subgoal by auto
subgoal by (auto simp: all_lits_of_mm_add_mset)
done
lemma all_lits_of_mm_extract_atms_clss:
‹L ∈# (all_lits_of_mm (mset `# mset CS)) ⟷ atm_of L ∈ extract_atms_clss CS {}›
by (induction CS)
(auto simp: extract_atms_clss_alt_def all_lits_of_mm_add_mset
in_all_lits_of_m_ain_atms_of_iff)
lemma IsaSAT_heur_alt_def:
‹IsaSAT_heur opts CS = do{
ASSERT(isasat_input_bounded (mset_set (extract_atms_clss CS {})));
ASSERT(∀C∈set CS. ∀L∈set C. nat_of_lit L ≤ uint32_max);
let 𝒜⇩i⇩n' = mset_set (extract_atms_clss CS {});
ASSERT(isasat_input_bounded 𝒜⇩i⇩n');
ASSERT(distinct_mset 𝒜⇩i⇩n');
let 𝒜⇩i⇩n'' = virtual_copy 𝒜⇩i⇩n';
let b = opts_unbounded_mode opts;
if b
then do {
S ← init_state_wl_heur 𝒜⇩i⇩n';
(T::twl_st_wl_heur_init) ← init_dt_wl_heur True CS S;
T ← rewatch_heur_st T;
let T = convert_state 𝒜⇩i⇩n'' T;
if ¬get_conflict_wl_is_None_heur_init T
then RETURN (empty_init_code)
else if CS = [] then empty_conflict_code
else do {
ASSERT(𝒜⇩i⇩n'' ≠ {#});
ASSERT(isasat_input_bounded_nempty 𝒜⇩i⇩n'');
ASSERT((λ(M', N', D', Q', W', ((ns, m, fst_As, lst_As, next_search), to_remove), φ, clvls). fst_As ≠ None ∧
lst_As ≠ None) T);
T ← finalise_init_code opts (T::twl_st_wl_heur_init);
U ← cdcl_twl_stgy_restart_prog_wl_heur T;
RETURN (if get_conflict_wl_is_None_heur U then extract_model_of_state_stat U
else extract_state_stat U)
}
}
else do {
S ← init_state_wl_heur 𝒜⇩i⇩n';
(T::twl_st_wl_heur_init) ← init_dt_wl_heur False CS S;
failed ← RETURN (is_failed_heur_init T ∨ ¬isasat_fast_init T);
if failed then do {
S ← init_state_wl_heur 𝒜⇩i⇩n';
(T::twl_st_wl_heur_init) ← init_dt_wl_heur True CS S;
T ← rewatch_heur_st T;
let T = convert_state 𝒜⇩i⇩n'' T;
if ¬get_conflict_wl_is_None_heur_init T
then RETURN (empty_init_code)
else if CS = [] then empty_conflict_code
else do {
ASSERT(𝒜⇩i⇩n'' ≠ {#});
ASSERT(isasat_input_bounded_nempty 𝒜⇩i⇩n'');
ASSERT((λ(M', N', D', Q', W', ((ns, m, fst_As, lst_As, next_search), to_remove), φ, clvls). fst_As ≠ None ∧
lst_As ≠ None) T);
T ← finalise_init_code opts (T::twl_st_wl_heur_init);
U ← cdcl_twl_stgy_restart_prog_wl_heur T;
RETURN (if get_conflict_wl_is_None_heur U then extract_model_of_state_stat U
else extract_state_stat U)
}
}
else do {
let T = convert_state 𝒜⇩i⇩n'' T;
if ¬get_conflict_wl_is_None_heur_init T
then RETURN (empty_init_code)
else if CS = [] then empty_conflict_code
else do {
ASSERT(𝒜⇩i⇩n'' ≠ {#});
ASSERT(isasat_input_bounded_nempty 𝒜⇩i⇩n'');
ASSERT((λ(M', N', D', Q', W', ((ns, m, fst_As, lst_As, next_search), to_remove), φ, clvls). fst_As ≠ None ∧
lst_As ≠ None) T);
ASSERT(rewatch_heur_st_fast_pre T);
T ← rewatch_heur_st_fast T;
ASSERT(isasat_fast_init T);
T ← finalise_init_code opts (T::twl_st_wl_heur_init);
ASSERT(isasat_fast T);
U ← cdcl_twl_stgy_restart_prog_early_wl_heur T;
RETURN (if get_conflict_wl_is_None_heur U then extract_model_of_state_stat U
else extract_state_stat U)
}
}
}
}›
by (auto simp: init_state_wl_heur_fast_def IsaSAT_heur_def isasat_init_fast_slow_alt_def convert_state_def isasat_information_banner_def cong: if_cong)
abbreviation rewatch_heur_st_rewatch_st_rel where
‹rewatch_heur_st_rewatch_st_rel CS U V ≡
{(S,T). (S, T) ∈ twl_st_heur_parsing (mset_set (extract_atms_clss CS {})) True ∧
get_clauses_wl_heur_init S = get_clauses_wl_heur_init U ∧
get_conflict_wl_heur_init S = get_conflict_wl_heur_init U ∧
get_clauses_wl (fst T) = get_clauses_wl (fst V) ∧
get_conflict_wl (fst T) = get_conflict_wl (fst V) ∧
get_subsumed_init_clauses_wl (fst T) = get_subsumed_init_clauses_wl (fst V) ∧
get_subsumed_learned_clauses_wl (fst T) = get_subsumed_learned_clauses_wl (fst V) ∧
get_unit_init_clss_wl (fst T) = get_unit_init_clss_wl (fst V) ∧
get_unit_learned_clss_wl (fst T) = get_unit_learned_clss_wl (fst V) ∧
get_unit_clauses_wl (fst T) = get_unit_clauses_wl (fst V)} O {(S, T). S = (T, {#})}›
lemma rewatch_heur_st_rewatch_st:
assumes
UV: ‹(U, V)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}›
shows ‹rewatch_heur_st U ≤
⇓(rewatch_heur_st_rewatch_st_rel CS U V)
(rewatch_st (from_init_state V))›
proof -
let ?𝒜 = ‹(mset_set (extract_atms_clss CS {}))›
obtain M' arena D' j W' vm φ clvls cach lbd vdom M N D NE UE NS US Q W OC failed where
U: ‹U = ((M', arena, D', j, W', vm, φ, clvls, cach, lbd, vdom, failed))› and
V: ‹V = ((M, N, D, NE, UE, NS, US, Q, W), OC)›
by (cases U; cases V) auto
have valid: ‹valid_arena arena N (set vdom)› and
dist: ‹distinct vdom› and
vdom_N: ‹mset vdom = dom_m N› and
watched: ‹(W', W) ∈ ⟨Id⟩map_fun_rel (D⇩0 ?𝒜)› and
lall: ‹literals_are_in_ℒ⇩i⇩n_mm ?𝒜 (mset `# ran_mf N)› and
vdom: ‹vdom_m ?𝒜 W N ⊆ set_mset (dom_m N)›
using UV by (auto simp: twl_st_heur_parsing_no_WL_def U V distinct_mset_dom
empty_watched_def vdom_m_def literals_are_in_ℒ⇩i⇩n_mm_def
all_lits_of_mm_union
simp flip: distinct_mset_mset_distinct)
show ?thesis
using UV
unfolding rewatch_heur_st_def rewatch_st_def
apply (simp only: prod.simps from_init_state_def fst_conv nres_monad1 U V)
apply refine_vcg
subgoal by (auto simp: twl_st_heur_parsing_no_WL_def dest: valid_arena_vdom_subset)
apply (rule rewatch_heur_rewatch[OF valid _ dist _ watched lall])
subgoal by simp
subgoal using vdom_N[symmetric] by simp
subgoal by (auto simp: vdom_m_def)
subgoal by (auto simp: U V twl_st_heur_parsing_def Collect_eq_comp'
twl_st_heur_parsing_no_WL_def)
done
qed
lemma rewatch_heur_st_rewatch_st2:
assumes
T: ‹(U, V)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}›
shows ‹rewatch_heur_st_fast
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) U)
≤ ⇓ ({(S,T). (S, T) ∈ twl_st_heur_parsing (mset_set (extract_atms_clss CS {})) True ∧
get_clauses_wl_heur_init S = get_clauses_wl_heur_init U ∧
get_conflict_wl_heur_init S = get_conflict_wl_heur_init U ∧
get_clauses_wl (fst T) = get_clauses_wl (fst V) ∧
get_conflict_wl (fst T) = get_conflict_wl (fst V) ∧
get_unit_clauses_wl (fst T) = get_unit_clauses_wl (fst V)} O {(S, T). S = (T, {#})})
(rewatch_st (from_init_state V))›
proof -
have
UV: ‹(U, V)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}›
using T by (auto simp: twl_st_heur_parsing_no_WL_def)
then show ?thesis
unfolding convert_state_def finalise_init_def id_def rewatch_heur_st_fast_def
by (rule rewatch_heur_st_rewatch_st[of U V, THEN order_trans])
(auto intro!: conc_fun_R_mono simp: Collect_eq_comp'
twl_st_heur_parsing_def)
qed
lemma rewatch_heur_st_rewatch_st3:
assumes
T: ‹(U, V)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) False O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}› and
failed: ‹¬is_failed_heur_init U›
shows ‹rewatch_heur_st_fast
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) U)
≤ ⇓ (rewatch_heur_st_rewatch_st_rel CS U V)
(rewatch_st (from_init_state V))›
proof -
have
UV: ‹(U, V)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}›
using T failed by (fastforce simp: twl_st_heur_parsing_no_WL_def)
then show ?thesis
unfolding convert_state_def finalise_init_def id_def rewatch_heur_st_fast_def
by (rule rewatch_heur_st_rewatch_st[of U V, THEN order_trans])
(auto intro!: conc_fun_R_mono simp: Collect_eq_comp'
twl_st_heur_parsing_def)
qed
abbreviation option_with_bool_rel :: ‹((bool × 'a) × 'a option) set› where
‹option_with_bool_rel ≡ {((b, s), s'). (b = is_None s') ∧ (¬b ⟶ s = the s')}›
definition model_stat_rel :: ‹((bool × nat literal list × 'a) × nat literal list option) set› where
‹model_stat_rel = {((b, M', s), M). ((b, rev M'), M) ∈ option_with_bool_rel}›
lemma IsaSAT_heur_IsaSAT:
‹IsaSAT_heur b CS ≤ ⇓model_stat_rel (IsaSAT CS)›
proof -
have init_dt_wl_heur: ‹init_dt_wl_heur True CS S ≤
⇓(twl_st_heur_parsing_no_WL 𝒜 True O {(S, T). S = remove_watched T ∧
get_watched_wl (fst T) = (λ_. [])})
(init_dt_wl' CS T)›
if
‹case (CS, T) of
(CS, S) ⇒
(∀C∈set CS. literals_are_in_ℒ⇩i⇩n 𝒜 (mset C)) ∧
distinct_mset_set (mset ` set CS)› and
‹((CS, S), CS, T) ∈ ⟨Id⟩list_rel ×⇩f twl_st_heur_parsing_no_WL 𝒜 True›
for 𝒜 CS T S
proof -
show ?thesis
apply (rule init_dt_wl_heur_init_dt_wl[THEN fref_to_Down_curry, of 𝒜 CS T CS S,
THEN order_trans])
apply (rule that(1))
apply (rule that(2))
apply (cases ‹init_dt_wl CS T›)
apply (force simp: init_dt_wl'_def RES_RETURN_RES conc_fun_RES
Image_iff)+
done
qed
have init_dt_wl_heur_b: ‹init_dt_wl_heur False CS S ≤
⇓(twl_st_heur_parsing_no_WL 𝒜 False O {(S, T). S = remove_watched T ∧
get_watched_wl (fst T) = (λ_. [])})
(init_dt_wl' CS T)›
if
‹case (CS, T) of
(CS, S) ⇒
(∀C∈set CS. literals_are_in_ℒ⇩i⇩n 𝒜 (mset C)) ∧
distinct_mset_set (mset ` set CS)› and
‹((CS, S), CS, T) ∈ ⟨Id⟩list_rel ×⇩f twl_st_heur_parsing_no_WL 𝒜 True›
for 𝒜 CS T S
proof -
show ?thesis
apply (rule init_dt_wl_heur_init_dt_wl[THEN fref_to_Down_curry, of 𝒜 CS T CS S,
THEN order_trans])
apply (rule that(1))
using that(2) apply (force simp: twl_st_heur_parsing_no_WL_def)
apply (cases ‹init_dt_wl CS T›)
apply (force simp: init_dt_wl'_def RES_RETURN_RES conc_fun_RES
Image_iff)+
done
qed
have virtual_copy: ‹(virtual_copy 𝒜, ()) ∈ {(ℬ, c). c = () ∧ ℬ = 𝒜}› for ℬ 𝒜
by (auto simp: virtual_copy_def)
have input_le: ‹∀C∈set CS. ∀L∈set C. nat_of_lit L ≤ uint32_max›
if ‹isasat_input_bounded (mset_set (extract_atms_clss CS {}))›
proof (intro ballI)
fix C L
assume ‹C ∈ set CS› and ‹L ∈ set C›
then have ‹L ∈# ℒ⇩a⇩l⇩l (mset_set (extract_atms_clss CS {}))›
by (auto simp: extract_atms_clss_alt_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
then show ‹nat_of_lit L ≤ uint32_max›
using that by auto
qed
have lits_C: ‹literals_are_in_ℒ⇩i⇩n (mset_set (extract_atms_clss CS {})) (mset C)›
if ‹C ∈ set CS› for C CS
using that
by (force simp: literals_are_in_ℒ⇩i⇩n_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n
in_all_lits_of_m_ain_atms_of_iff extract_atms_clss_alt_def
atm_of_eq_atm_of)
have init_state_wl_heur: ‹isasat_input_bounded 𝒜 ⟹
init_state_wl_heur 𝒜 ≤ SPEC (λc. (c, init_state_wl) ∈
{(S, S'). (S, S') ∈ twl_st_heur_parsing_no_WL_wl 𝒜 True})› for 𝒜
apply (rule init_state_wl_heur_init_state_wl[THEN fref_to_Down_unRET_uncurry0_SPEC,
of 𝒜, THEN order_trans])
apply (auto)
done
let ?TT = ‹rewatch_heur_st_rewatch_st_rel CS›
have get_conflict_wl_is_None_heur_init: ‹(Tb, Tc) ∈ ?TT U V ⟹
(¬ get_conflict_wl_is_None_heur_init Tb) = (get_conflict_wl Tc ≠ None)› for Tb Tc U V
by (cases V) (auto simp: twl_st_heur_parsing_def Collect_eq_comp'
get_conflict_wl_is_None_heur_init_def
option_lookup_clause_rel_def)
have get_conflict_wl_is_None_heur_init3: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) False O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])} ⟹
(failed, faileda)
∈ {(b, b'). b = b' ∧ b = (is_failed_heur_init T ∨ ¬ isasat_fast_init T)} ⟹ ¬failed ⟹
(¬ get_conflict_wl_is_None_heur_init T) = (get_conflict_wl (fst Ta) ≠ None)› for T Ta failed faileda
by (cases T; cases Ta) (auto simp: twl_st_heur_parsing_no_WL_def
get_conflict_wl_is_None_heur_init_def
option_lookup_clause_rel_def)
have finalise_init_nempty: ‹x1i ≠ None› ‹x1j ≠ None›
if
T: ‹(Tb, Tc) ∈ ?TT U V› and
nempty: ‹extract_atms_clss CS {} ≠ {}› and
st:
‹x2g = (x1j, x2h)›
‹x2f = (x1i, x2g)›
‹x2e = (x1h, x2f)›
‹x1f = (x1g, x2e)›
‹x1e = (x1f, x2i)›
‹x2j = (x1k, x2k)›
‹x2d = (x1e, x2j)›
‹x2c = (x1d, x2d)›
‹x2b = (x1c, x2c)›
‹x2a = (x1b, x2b)›
‹x2 = (x1a, x2a)› and
conv: ‹convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) Tb =
(x1, x2)›
for ba S T Ta Tb Tc uu x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x1f
x1g x2e x1h x2f x1i x2g x1j x2h x2i x2j x1k x2k U V
proof -
show ‹x1i ≠ None›
using T conv nempty
unfolding st
by (cases x1i)
(auto simp: convert_state_def twl_st_heur_parsing_def
isa_vmtf_init_def vmtf_init_def mset_set_empty_iff)
show ‹x1j ≠ None›
using T conv nempty
unfolding st
by (cases x1i)
(auto simp: convert_state_def twl_st_heur_parsing_def
isa_vmtf_init_def vmtf_init_def mset_set_empty_iff)
qed
have banner: ‹isasat_information_banner
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) Tb)
≤ SPEC (λc. (c, ()) ∈ {(_, _). True})› for Tb
by (auto simp: isasat_information_banner_def)
have finalise_init_code: ‹finalise_init_code b
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) Tb)
≤ SPEC (λc. (c, finalise_init Tc) ∈ twl_st_heur)› (is ?A) and
finalise_init_code3: ‹finalise_init_code b Tb
≤ SPEC (λc. (c, finalise_init Tc) ∈ twl_st_heur)› (is ?B)
if
T: ‹(Tb, Tc) ∈ ?TT U V› and
confl: ‹¬ get_conflict_wl Tc ≠ None› and
nempty: ‹extract_atms_clss CS {} ≠ {}› and
clss_CS: ‹mset `# ran_mf (get_clauses_wl Tc) + get_unit_clauses_wl Tc + get_subsumed_clauses_wl Tc =
mset `# mset CS› and
learned: ‹learned_clss_l (get_clauses_wl Tc) = {#}›
for ba S T Ta Tb Tc u v U V
proof -
have 1: ‹get_conflict_wl Tc = None›
using confl by auto
have 2: ‹all_atms_st Tc ≠ {#}›
using clss_CS nempty unfolding all_lits_def add.assoc
by (auto simp flip: all_atms_def[symmetric] simp: all_lits_def
isasat_input_bounded_nempty_def extract_atms_clss_alt_def
all_lits_of_mm_empty_iff)
have 3: ‹set_mset (all_atms_st Tc) = set_mset (mset_set (extract_atms_clss CS {}))›
using clss_CS nempty unfolding all_lits_def add.assoc
by (auto simp flip: all_atms_def[symmetric] simp: all_lits_def
isasat_input_bounded_nempty_def
atm_of_all_lits_of_mm extract_atms_clss_alt_def atms_of_ms_def)
have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x
by auto
have H': ‹A = B ⟹ A x ⟹ B x› for A B x
by auto
note cong = trail_pol_cong heuristic_rel_cong
option_lookup_clause_rel_cong isa_vmtf_init_cong
vdom_m_cong[THEN H] isasat_input_nempty_cong[THEN iffD1]
isasat_input_bounded_cong[THEN iffD1]
cach_refinement_empty_cong[THEN H']
phase_saving_cong[THEN H']
ℒ⇩a⇩l⇩l_cong[THEN H]
D⇩0_cong[THEN H]
have 4: ‹(convert_state (mset_set (extract_atms_clss CS {})) Tb, Tc)
∈ twl_st_heur_post_parsing_wl True›
using T nempty
by (auto simp: twl_st_heur_parsing_def twl_st_heur_post_parsing_wl_def
convert_state_def eq_commute[of ‹mset _› ‹dom_m _›]
vdom_m_cong[OF 3[symmetric]] ℒ⇩a⇩l⇩l_cong[OF 3[symmetric]]
dest!: cong[OF 3[symmetric]])
(simp_all add: add.assoc ℒ⇩a⇩l⇩l_all_atms_all_lits
flip: all_lits_def all_lits_alt_def2 all_lits_alt_def)
show ?A
by (rule finalise_init_finalise_init[THEN fref_to_Down_unRET_curry_SPEC, of b])
(use 1 2 learned 4 in auto)
then show ?B unfolding convert_state_def by auto
qed
have get_conflict_wl_is_None_heur_init2: ‹(U, V)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])} ⟹
(¬ get_conflict_wl_is_None_heur_init
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) U)) =
(get_conflict_wl (from_init_state V) ≠ None)› for U V
by (auto simp: twl_st_heur_parsing_def Collect_eq_comp'
get_conflict_wl_is_None_heur_init_def twl_st_heur_parsing_no_WL_def
option_lookup_clause_rel_def convert_state_def from_init_state_def)
have finalise_init2: ‹x1i ≠ None› ‹x1j ≠ None›
if
T: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) b O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}› and
nempty: ‹extract_atms_clss CS {} ≠ {}› and
st:
‹x2g = (x1j, x2h)›
‹x2f = (x1i, x2g)›
‹x2e = (x1h, x2f)›
‹x1f = (x1g, x2e)›
‹x1e = (x1f, x2i)›
‹x2j = (x1k, x2k)›
‹x2d = (x1e, x2j)›
‹x2c = (x1d, x2d)›
‹x2b = (x1c, x2c)›
‹x2a = (x1b, x2b)›
‹x2 = (x1a, x2a)› and
conv: ‹convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) T =
(x1, x2)›
for uu ba S T Ta baa uua uub x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x1f
x1g x2e x1h x2f x1i x2g x1j x2h x2i x2j x1k x2k b
proof -
show ‹x1i ≠ None›
using T conv nempty
unfolding st
by (cases x1i)
(auto simp: convert_state_def twl_st_heur_parsing_def
twl_st_heur_parsing_no_WL_def
isa_vmtf_init_def vmtf_init_def mset_set_empty_iff)
show ‹x1j ≠ None›
using T conv nempty
unfolding st
by (cases x1i)
(auto simp: convert_state_def twl_st_heur_parsing_def
twl_st_heur_parsing_no_WL_def
isa_vmtf_init_def vmtf_init_def mset_set_empty_iff)
qed
have rewatch_heur_st_fast_pre: ‹rewatch_heur_st_fast_pre
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) T)›
if
T: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}› and
length_le: ‹¬¬isasat_fast_init (convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) T)›
for uu ba S T Ta baa uua uub
proof -
have ‹valid_arena (get_clauses_wl_heur_init T) (get_clauses_wl (fst Ta))
(set (get_vdom_heur_init T))›
using T by (auto simp: twl_st_heur_parsing_no_WL_def)
then show ?thesis
using length_le unfolding rewatch_heur_st_fast_pre_def convert_state_def
isasat_fast_init_def uint64_max_def uint32_max_def
by (auto dest: valid_arena_in_vdom_le_arena)
qed
have rewatch_heur_st_fast_pre2: ‹rewatch_heur_st_fast_pre
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) T)›
if
T: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) False O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}› and
length_le: ‹¬¬isasat_fast_init (convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) T)› and
failed: ‹¬is_failed_heur_init T›
for uu ba S T Ta baa uua uub
proof -
have
Ta: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}›
using failed T by (cases T; cases Ta) (fastforce simp: twl_st_heur_parsing_no_WL_def)
from rewatch_heur_st_fast_pre[OF this length_le]
show ?thesis .
qed
have finalise_init_code2: ‹finalise_init_code b Tb
≤ SPEC (λc. (c, finalise_init Tc) ∈ {(S', T').
(S', T') ∈ twl_st_heur ∧
get_clauses_wl_heur_init Tb = get_clauses_wl_heur S'})›
if
Ta: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) False O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}› and
confl: ‹¬ get_conflict_wl (from_init_state Ta) ≠ None› and
‹CS ≠ []› and
nempty: ‹extract_atms_clss CS {} ≠ {}› and
‹isasat_input_bounded_nempty (mset_set (extract_atms_clss CS {}))› and
clss_CS: ‹mset `# ran_mf (get_clauses_wl (from_init_state Ta)) +
get_unit_clauses_wl (from_init_state Ta) + get_subsumed_clauses_wl (from_init_state Ta) =
mset `# mset CS› and
learned: ‹learned_clss_l (get_clauses_wl (from_init_state Ta)) = {#}› and
‹virtual_copy (mset_set (extract_atms_clss CS {})) ≠ {#}› and
‹isasat_input_bounded_nempty
(virtual_copy (mset_set (extract_atms_clss CS {})))› and
‹case convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) T of
(M', N', D', Q', W', xa, xb) ⇒
(case xa of
(x, xa) ⇒
(case x of
(ns, m, fst_As, lst_As, next_search) ⇒
λto_remove (φ, clvls). fst_As ≠ None ∧ lst_As ≠ None)
xa)
xb› and
T: ‹(Tb, Tc) ∈ ?TT T Ta› and
failed: ‹¬is_failed_heur_init T›
for uu ba S T Ta baa uua uub V W b Tb Tc
proof -
have
Ta: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}›
using failed Ta by (cases T; cases Ta) (fastforce simp: twl_st_heur_parsing_no_WL_def)
have 1: ‹get_conflict_wl Tc = None›
using confl T by (auto simp: from_init_state_def)
have Ta_Tc: ‹all_atms_st Tc = all_atms_st (from_init_state Ta)›
using T Ta
unfolding all_lits_alt_def mem_Collect_eq prod.case relcomp.simps
all_atms_def add.assoc apply -
apply normalize_goal+
by (auto simp flip: all_atms_def[symmetric] simp: all_lits_def
twl_st_heur_parsing_no_WL_def twl_st_heur_parsing_def
from_init_state_def)
moreover have 3: ‹set_mset (all_atms_st (from_init_state Ta)) = set_mset (mset_set (extract_atms_clss CS {}))›
unfolding all_lits_alt_def mem_Collect_eq prod.case relcomp.simps
all_atms_def clss_CS[unfolded add.assoc] apply -
by (auto simp: extract_atms_clss_alt_def
atm_of_all_lits_of_mm atms_of_ms_def)
ultimately have 2: ‹all_atms_st Tc ≠ {#}›
using nempty
by auto
have 3: ‹set_mset (all_atms_st Tc) = set_mset (mset_set (extract_atms_clss CS {}))›
unfolding Ta_Tc 3 ..
have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x
by auto
have H': ‹A = B ⟹ A x ⟹ B x› for A B x
by auto
note cong = trail_pol_cong heuristic_rel_cong
option_lookup_clause_rel_cong isa_vmtf_init_cong
vdom_m_cong[THEN H] isasat_input_nempty_cong[THEN iffD1]
isasat_input_bounded_cong[THEN iffD1]
cach_refinement_empty_cong[THEN H']
phase_saving_cong[THEN H']
ℒ⇩a⇩l⇩l_cong[THEN H]
D⇩0_cong[THEN H]
have 4: ‹(convert_state (mset_set (extract_atms_clss CS {})) Tb, Tc)
∈ twl_st_heur_post_parsing_wl True›
using T nempty
by (auto simp: twl_st_heur_parsing_def twl_st_heur_post_parsing_wl_def
convert_state_def eq_commute[of ‹mset _› ‹dom_m _›]
vdom_m_cong[OF 3[symmetric]] ℒ⇩a⇩l⇩l_cong[OF 3[symmetric]]
dest!: cong[OF 3[symmetric]])
(simp_all add: add.assoc ℒ⇩a⇩l⇩l_all_atms_all_lits
flip: all_lits_def all_lits_alt_def2 all_lits_alt_def)
show ?thesis
apply (rule finalise_init_finalise_init_full[unfolded conc_fun_RETURN,
THEN order_trans])
by (use 1 2 learned 4 T in ‹auto simp: from_init_state_def convert_state_def›)
qed
have isasat_fast: ‹isasat_fast Td›
if
fast: ‹¬ ¬ isasat_fast_init
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {})))
T)› and
Tb: ‹(Tb, Tc) ∈ ?TT T Ta› and
Td: ‹(Td, Te)
∈ {(S', T').
(S', T') ∈ twl_st_heur ∧
get_clauses_wl_heur_init Tb = get_clauses_wl_heur S'}›
for uu ba S T Ta baa uua uub Tb Tc Td Te
proof -
show ?thesis
using fast Td Tb
by (auto simp: convert_state_def isasat_fast_init_def sint64_max_def
uint32_max_def uint64_max_def isasat_fast_def)
qed
define init_succesfull where ‹init_succesfull T = RETURN (is_failed_heur_init T ∨ ¬isasat_fast_init T)› for T
define init_succesfull2 where ‹init_succesfull2 = SPEC (λ_ :: bool. True)›
have [refine]: ‹init_succesfull T ≤ ⇓ {(b, b'). (b = b') ∧ (b ⟷ is_failed_heur_init T ∨ ¬isasat_fast_init T)}
init_succesfull2› for T
by (auto simp: init_succesfull_def init_succesfull2_def intro!: RETURN_RES_refine)
show ?thesis
supply [[goals_limit=1]]
unfolding IsaSAT_heur_alt_def IsaSAT_alt_def init_succesfull_def[symmetric]
apply (rewrite at ‹do {_ ← init_dt_wl' _ _; _ ← (⌑ :: bool nres); If _ _ _ }› init_succesfull2_def[symmetric])
apply (refine_vcg virtual_copy init_state_wl_heur banner
cdcl_twl_stgy_restart_prog_wl_heur_cdcl_twl_stgy_restart_prog_wl_D[THEN fref_to_Down])
subgoal by (rule input_le)
subgoal by (rule distinct_mset_mset_set)
subgoal by auto
subgoal by auto
apply (rule init_dt_wl_heur[of ‹mset_set (extract_atms_clss CS {})›])
subgoal by (auto simp: lits_C)
subgoal by (auto simp: twl_st_heur_parsing_no_WL_wl_def
twl_st_heur_parsing_no_WL_def to_init_state_def
init_state_wl_def init_state_wl_heur_def
inres_def RES_RES_RETURN_RES
RES_RETURN_RES)
apply (rule rewatch_heur_st_rewatch_st; assumption)
subgoal unfolding convert_state_def by (rule get_conflict_wl_is_None_heur_init)
subgoal by (auto simp add: empty_init_code_def model_stat_rel_def)
subgoal by simp
subgoal by (auto simp add: empty_conflict_code_def model_stat_rel_def)
subgoal by (simp add: mset_set_empty_iff extract_atms_clss_alt_def)
subgoal by simp
subgoal by (rule finalise_init_nempty)
subgoal by (rule finalise_init_nempty)
apply (rule finalise_init_code; assumption)
subgoal by fast
subgoal by fast
subgoal premises p for _ ba S T Ta Tb Tc u v
using p(27)
by (auto simp: twl_st_heur_def get_conflict_wl_is_None_heur_def
extract_stats_def extract_state_stat_def
option_lookup_clause_rel_def trail_pol_def
extract_model_of_state_def rev_map
extract_model_of_state_stat_def model_stat_rel_def
dest!: ann_lits_split_reasons_map_lit_of)
apply (rule init_dt_wl_heur_b[of ‹mset_set (extract_atms_clss CS {})›])
subgoal by (auto simp: lits_C)
subgoal by (auto simp: twl_st_heur_parsing_no_WL_wl_def
twl_st_heur_parsing_no_WL_def to_init_state_def
init_state_wl_def init_state_wl_heur_def
inres_def RES_RES_RETURN_RES
RES_RETURN_RES)
subgoal by fast
apply (rule init_dt_wl_heur[of ‹mset_set (extract_atms_clss CS {})›])
subgoal by (auto simp: lits_C)
subgoal by (auto simp: twl_st_heur_parsing_no_WL_wl_def
twl_st_heur_parsing_no_WL_def to_init_state_def
init_state_wl_def init_state_wl_heur_def
inres_def RES_RES_RETURN_RES
RES_RETURN_RES)
apply (rule rewatch_heur_st_rewatch_st; assumption)
subgoal unfolding convert_state_def by (rule get_conflict_wl_is_None_heur_init)
subgoal by (auto simp add: empty_init_code_def model_stat_rel_def)
subgoal by simp
subgoal by (simp add: empty_conflict_code_def model_stat_rel_def)
subgoal by (simp add: mset_set_empty_iff extract_atms_clss_alt_def)
subgoal by simp
subgoal by (rule finalise_init_nempty)
subgoal by (rule finalise_init_nempty)
apply (rule finalise_init_code; assumption)
subgoal by fast
subgoal by fast
subgoal premises p for _ ba S T Ta Tb Tc u v
using p(34)
by (auto simp: twl_st_heur_def get_conflict_wl_is_None_heur_def
extract_stats_def extract_state_stat_def
option_lookup_clause_rel_def trail_pol_def
extract_model_of_state_def rev_map
extract_model_of_state_stat_def model_stat_rel_def
dest!: ann_lits_split_reasons_map_lit_of)
subgoal unfolding from_init_state_def convert_state_def by (rule get_conflict_wl_is_None_heur_init3)
subgoal by (simp add: empty_init_code_def model_stat_rel_def)
subgoal by simp
subgoal by (simp add: empty_conflict_code_def model_stat_rel_def)
subgoal by (simp add: mset_set_empty_iff extract_atms_clss_alt_def)
subgoal by (simp add: mset_set_empty_iff extract_atms_clss_alt_def)
subgoal by (rule finalise_init2)
subgoal by (rule finalise_init2)
subgoal for uu ba S T Ta baa uua
by (rule rewatch_heur_st_fast_pre2; assumption?) (simp_all add: convert_state_def)
apply (rule rewatch_heur_st_rewatch_st3; assumption?)
subgoal by auto
subgoal by (clarsimp simp add: isasat_fast_init_def convert_state_def)
apply (rule finalise_init_code2; assumption?)
subgoal by clarsimp
subgoal by (clarsimp simp add: isasat_fast_def isasat_fast_init_def convert_state_def)
apply (rule_tac r1 = ‹length (get_clauses_wl_heur Td)› in cdcl_twl_stgy_restart_prog_early_wl_heur_cdcl_twl_stgy_restart_prog_early_wl_D[
THEN fref_to_Down])
subgoal by (auto simp: isasat_fast_def sint64_max_def uint64_max_def uint32_max_def)
subgoal by fast
subgoal by fast
subgoal premises p for _ ba S T Ta Tb Tc u v
using p(33)
by (auto simp: twl_st_heur_def get_conflict_wl_is_None_heur_def
extract_stats_def extract_state_stat_def
option_lookup_clause_rel_def trail_pol_def
extract_model_of_state_def rev_map
extract_model_of_state_stat_def model_stat_rel_def
dest!: ann_lits_split_reasons_map_lit_of)
done
qed
definition length_get_clauses_wl_heur_init where
‹length_get_clauses_wl_heur_init S = length (get_clauses_wl_heur_init S)›
lemma length_get_clauses_wl_heur_init_alt_def:
‹RETURN o length_get_clauses_wl_heur_init = (λ(_, N,_). RETURN (length N))›
unfolding length_get_clauses_wl_heur_init_def
by auto
definition model_if_satisfiable :: ‹nat clauses ⇒ nat literal list option nres› where
‹model_if_satisfiable CS = SPEC (λM.
if satisfiable (set_mset CS) then M ≠ None ∧ set (the M) ⊨sm CS else M = None)›
definition SAT' :: ‹nat clauses ⇒ nat literal list option nres› where
‹SAT' CS = do {
T ← SAT CS;
RETURN(if conflicting T = None then Some (map lit_of (trail T)) else None)
}
›
lemma SAT_model_if_satisfiable:
‹(SAT', model_if_satisfiable) ∈ [λCS. (∀C ∈# CS. distinct_mset C)]⇩f Id→ ⟨Id⟩nres_rel›
(is ‹_ ∈[λCS. ?P CS]⇩f Id → _›)
proof -
have H: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant (init_state CS)›
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (init_state CS)›
if ‹?P CS› for CS
using that by (auto simp:
twl_struct_invs_def twl_st_inv.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_alt_def cdcl⇩W_restart_mset.no_smaller_propa_def
past_invs.simps clauses_def twl_list_invs_def twl_stgy_invs_def clause_to_update_def
cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
cdcl⇩W_restart_mset.no_smaller_confl_def
distinct_mset_set_def)
have H: ‹s ∈ {M. if satisfiable (set_mset CS) then M ≠ None ∧ set (the M) ⊨sm CS else M = None}›
if
dist: ‹Multiset.Ball CS distinct_mset› and
[simp]: ‹CS' = CS› and
s: ‹s ∈ (λT. if conflicting T = None then Some (map lit_of (trail T)) else None) `
Collect (conclusive_CDCL_run CS' (init_state CS'))›
for s :: ‹nat literal list option› and CS CS'
proof -
obtain T where
s: ‹(s = Some (map lit_of (trail T)) ∧ conflicting T = None) ∨
(s = None ∧ conflicting T ≠ None)› and
conc: ‹conclusive_CDCL_run CS' ([], CS', {#}, None) T›
using s by auto force
consider
n n' where ‹cdcl⇩W_restart_mset.cdcl⇩W_restart_stgy⇧*⇧* (([], CS', {#}, None), n) (T, n')›
‹no_step cdcl⇩W_restart_mset.cdcl⇩W T› |
‹CS' ≠ {#}› and ‹conflicting T ≠ None› and ‹backtrack_lvl T = 0› and
‹unsatisfiable (set_mset CS')›
using conc unfolding conclusive_CDCL_run_def
by auto
then show ?thesis
proof cases
case (1 n n') note st = this(1) and ns = this(2)
have ‹no_step cdcl⇩W_restart_mset.cdcl⇩W_stgy T›
using ns cdcl⇩W_restart_mset.cdcl⇩W_stgy_cdcl⇩W by blast
then have full_T: ‹full cdcl⇩W_restart_mset.cdcl⇩W_stgy T T›
unfolding full_def by blast
have invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant T›
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv T›
using st cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_dcl⇩W_all_struct_inv[OF st]
cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_dcl⇩W_stgy_invariant[OF st]
H[OF dist] by auto
have res: ‹cdcl⇩W_restart_mset.cdcl⇩W_restart⇧*⇧* ([], CS', {#}, None) T›
using cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_stgy_cdcl⇩W_restart[OF st] by simp
have ent: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init T›
using cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_learned_clauses_entailed[OF res] H[OF dist]
unfolding ‹CS' = CS› cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by simp
have [simp]: ‹init_clss T = CS›
using cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_init_clss[OF res] by simp
show ?thesis
using cdcl⇩W_restart_mset.full_cdcl⇩W_stgy_inv_normal_form[OF full_T invs ent] s
by (auto simp: true_annots_true_cls lits_of_def)
next
case 2
moreover have ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (init_state CS)›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
by auto
ultimately show ?thesis
using H[OF dist] cdcl⇩W_restart_mset.full_cdcl⇩W_stgy_inv_normal_form[of ‹init_state CS›
‹init_state CS›] s
by auto
qed
qed
show ?thesis
unfolding SAT'_def model_if_satisfiable_def SAT_def Let_def
apply (intro frefI nres_relI)
subgoal for CS' CS
unfolding RES_RETURN_RES
apply (rule RES_refine)
unfolding pair_in_Id_conv bex_triv_one_point1 bex_triv_one_point2
by (rule H)
done
qed
lemma SAT_model_if_satisfiable':
‹(uncurry (λ_. SAT'), uncurry (λ_. model_if_satisfiable)) ∈
[λ(_, CS). (∀C ∈# CS. distinct_mset C)]⇩f Id ×⇩r Id→ ⟨Id⟩nres_rel›
using SAT_model_if_satisfiable by (auto simp: fref_def)
definition SAT_l' where
‹SAT_l' CS = do{
S ← SAT_l CS;
RETURN (if get_conflict_l S = None then Some (map lit_of (get_trail_l S)) else None)
}›
definition SAT0' where
‹SAT0' CS = do{
S ← SAT0 CS;
RETURN (if get_conflict S = None then Some (map lit_of (get_trail S)) else None)
}›
lemma twl_st_l_map_lit_of[twl_st_l, simp]:
‹(S, T) ∈ twl_st_l b ⟹ map lit_of (get_trail_l S) = map lit_of (get_trail T)›
by (auto simp: twl_st_l_def convert_lits_l_map_lit_of)
lemma ISASAT_SAT_l':
assumes ‹Multiset.Ball (mset `# mset CS) distinct_mset› and
‹isasat_input_bounded (mset_set (⋃C∈set CS. atm_of ` set C))›
shows ‹IsaSAT CS ≤ ⇓ Id (SAT_l' CS)›
unfolding IsaSAT_def SAT_l'_def
apply refine_vcg
apply (rule SAT_wl_SAT_l)
subgoal using assms by auto
subgoal using assms by auto
subgoal by (auto simp: extract_model_of_state_def)
done
lemma SAT_l'_SAT0':
assumes ‹Multiset.Ball (mset `# mset CS) distinct_mset›
shows ‹SAT_l' CS ≤ ⇓ Id (SAT0' CS)›
unfolding SAT_l'_def SAT0'_def
apply refine_vcg
apply (rule SAT_l_SAT0)
subgoal using assms by auto
subgoal by (auto simp: extract_model_of_state_def)
done
lemma SAT0'_SAT':
assumes ‹Multiset.Ball (mset `# mset CS) distinct_mset›
shows ‹SAT0' CS ≤ ⇓ Id (SAT' (mset `# mset CS))›
unfolding SAT'_def SAT0'_def
apply refine_vcg
apply (rule SAT0_SAT)
subgoal using assms by auto
subgoal by (auto simp: extract_model_of_state_def twl_st_l twl_st)
done
lemma IsaSAT_heur_model_if_sat:
assumes ‹∀C ∈# mset `# mset CS. distinct_mset C› and
‹isasat_input_bounded (mset_set (⋃C∈set CS. atm_of ` set C))›
shows ‹IsaSAT_heur opts CS ≤ ⇓ model_stat_rel (model_if_satisfiable (mset `# mset CS))›
apply (rule IsaSAT_heur_IsaSAT[THEN order_trans])
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule ISASAT_SAT_l')
subgoal using assms by auto
subgoal using assms by auto
unfolding conc_fun_chain
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule SAT_l'_SAT0')
subgoal using assms by auto
unfolding conc_fun_chain
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule SAT0'_SAT')
subgoal using assms by auto
unfolding conc_fun_chain
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule SAT_model_if_satisfiable[THEN fref_to_Down, of ‹mset `# mset CS›])
subgoal using assms by auto
subgoal using assms by auto
unfolding conc_fun_chain
apply (rule conc_fun_R_mono)
apply (auto simp: model_stat_rel_def)
done
lemma IsaSAT_heur_model_if_sat': ‹(uncurry IsaSAT_heur, uncurry (λ_. model_if_satisfiable)) ∈
[λ(_, CS). (∀C ∈# CS. distinct_mset C) ∧
(∀C∈#CS. ∀L∈#C. nat_of_lit L ≤ uint32_max)]⇩f
Id ×⇩r list_mset_rel O ⟨list_mset_rel⟩mset_rel → ⟨model_stat_rel⟩nres_rel›
proof -
have H: ‹isasat_input_bounded (mset_set (⋃C∈set CS. atm_of ` set C))›
if CS_p: ‹∀C∈#CS'. ∀L∈#C. nat_of_lit L ≤ uint32_max› and
‹(CS, CS') ∈ list_mset_rel O ⟨list_mset_rel⟩mset_rel›
for CS CS'
unfolding isasat_input_bounded_def
proof
fix L
assume L: ‹L ∈# ℒ⇩a⇩l⇩l (mset_set (⋃C∈set CS. atm_of ` set C))›
then obtain C where
L: ‹C∈set CS ∧ (L ∈set C ∨ - L ∈ set C)›
apply (cases L)
apply (auto simp: extract_atms_clss_alt_def uint32_max_def
ℒ⇩a⇩l⇩l_def)+
apply (metis literal.exhaust_sel)+
done
have ‹nat_of_lit L ≤ uint32_max ∨ nat_of_lit (-L) ≤ uint32_max›
using L CS_p that by (auto simp: list_mset_rel_def mset_rel_def br_def
br_def mset_rel_def p2rel_def rel_mset_def
rel2p_def[abs_def] list_all2_op_eq_map_right_iff')
then show ‹nat_of_lit L ≤ uint32_max›
using L
by (cases L) (auto simp: extract_atms_clss_alt_def uint32_max_def)
qed
show ?thesis
apply (intro frefI nres_relI)
unfolding uncurry_def
apply clarify
subgoal for o1 o2 o3 CS o1' o2' o3' CS'
apply (rule IsaSAT_heur_model_if_sat[THEN order_trans, of CS _ ‹(o1, o2, o3)›])
subgoal by (auto simp: list_mset_rel_def mset_rel_def br_def
br_def mset_rel_def p2rel_def rel_mset_def
rel2p_def[abs_def] list_all2_op_eq_map_right_iff')
subgoal by (rule H) auto
apply (auto simp: list_mset_rel_def mset_rel_def br_def
br_def mset_rel_def p2rel_def rel_mset_def
rel2p_def[abs_def] list_all2_op_eq_map_right_iff')
done
done
qed
section ‹Refinements of the Whole Bounded SAT Solver›
text ‹This is the specification of the SAT solver:›
definition SAT_bounded :: ‹nat clauses ⇒ (bool × nat cdcl⇩W_restart_mset) nres› where
‹SAT_bounded CS = do{
T ← SPEC(λT. T = init_state CS);
finished ← SPEC(λ_. True);
if ¬finished then
RETURN (finished, T)
else
SPEC (λ(b, U). b ⟶ conclusive_CDCL_run CS T U)
}›
definition SAT0_bounded :: ‹nat clause_l list ⇒ (bool × nat twl_st) nres› where
‹SAT0_bounded CS = do{
let (S :: nat twl_st_init) = init_state0;
T ← SPEC (λT. init_dt_spec0 CS (to_init_state0 S) T);
finished ← SPEC(λ_. True);
if ¬finished then do {
RETURN (False, fst init_state0)
} else do {
let T = fst T;
if get_conflict T ≠ None
then RETURN (True, T)
else if CS = [] then RETURN (True, fst init_state0)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update T = {#});
ASSERT(clause `# (get_clauses T) + unit_clss T + subsumed_clauses T = mset `# mset CS);
ASSERT(get_learned_clss T = {#});
cdcl_twl_stgy_restart_prog_bounded T
}
}
}›
lemma SAT0_bounded_SAT_bounded:
assumes ‹Multiset.Ball (mset `# mset CS) distinct_mset›
shows ‹SAT0_bounded CS ≤ ⇓ ({((b, S), (b', T)). b = b' ∧ (b ⟶ T = state⇩W_of S)}) (SAT_bounded (mset `# mset CS))›
(is ‹_ ≤ ⇓?A _›)
proof -
have conflict_during_init:
‹RETURN (True, fst T)
≤ ⇓ {((b, S), b', T). b = b' ∧ (b ⟶ T = state⇩W_of S)}
(SPEC (λ(b, U). b ⟶ conclusive_CDCL_run (mset `# mset CS) S U))›
if
TS: ‹(T, S)
∈ {(S, T).
(init_dt_spec0 CS (to_init_state0 init_state0) S) ∧
(T = init_state (mset `# mset CS))}› and
‹¬ ¬ failed'› and
‹¬ ¬ failed› and
confl: ‹get_conflict (fst T) ≠ None›
for bS bT failed T failed' S
proof -
let ?CS = ‹mset `# mset CS›
have failed[simp]: ‹failed› ‹failed'› ‹failed = True› ‹failed' = True›
using that
by auto
have
struct_invs: ‹twl_struct_invs_init T› and
‹clauses_to_update_init T = {#}› and
count_dec: ‹∀s∈set (get_trail_init T). ¬ is_decided s› and
‹get_conflict_init T = None ⟶
literals_to_update_init T =
uminus `# lit_of `# mset (get_trail_init T)› and
clss: ‹mset `# mset CS +
clause `# get_init_clauses_init (to_init_state0 init_state0) +
other_clauses_init (to_init_state0 init_state0) +
get_unit_init_clauses_init (to_init_state0 init_state0) +
get_subsumed_init_clauses_init (to_init_state0 init_state0) =
clause `# get_init_clauses_init T + other_clauses_init T +
get_unit_init_clauses_init T + get_subsumed_init_clauses_init T› and
learned: ‹get_learned_clauses_init (to_init_state0 init_state0) =
get_learned_clauses_init T›
‹get_unit_learned_clauses_init T =
get_unit_learned_clauses_init (to_init_state0 init_state0)›
‹get_subsumed_learned_clauses_init T =
get_subsumed_learned_clauses_init (to_init_state0 init_state0)› and
‹twl_stgy_invs (fst T)› and
‹other_clauses_init T ≠ {#} ⟶ get_conflict_init T ≠ None› and
‹{#} ∈# mset `# mset CS ⟶ get_conflict_init T ≠ None› and
‹get_conflict_init (to_init_state0 init_state0) ≠ None ⟶
get_conflict_init (to_init_state0 init_state0) = get_conflict_init T›
using TS unfolding init_dt_wl_spec_def init_dt_spec0_def
Set.mem_Collect_eq prod.case failed simp_thms apply -
apply normalize_goal+
by metis+
have count_dec: ‹count_decided (get_trail (fst T)) = 0›
using count_dec unfolding count_decided_0_iff by (auto simp: twl_st_init
twl_st_wl_init)
have le: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (state⇩W_of_init T)› and
all_struct_invs:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of_init T)›
using struct_invs unfolding twl_struct_invs_init_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (state⇩W_of_init T)›
using struct_invs unfolding twl_struct_invs_init_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast
have ‹unsatisfiable (set_mset (mset `# mset (rev CS)))›
using conflict_of_level_unsatisfiable[OF all_struct_invs] count_dec confl
learned le clss
by (auto simp: clauses_def mset_take_mset_drop_mset' twl_st_init twl_st_wl_init
image_image to_init_state0_def init_state0_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def ac_simps
twl_st_l_init)
then have unsat[simp]: ‹unsatisfiable (mset ` set CS)›
by auto
then have [simp]: ‹CS ≠ []›
by (auto simp del: unsat)
show ?thesis
unfolding conclusive_CDCL_run_def
apply (rule RETURN_SPEC_refine)
apply (rule exI[of _ ‹(True, state⇩W_of (fst T))›])
apply (intro conjI)
subgoal
by auto
subgoal
using struct_invs learned count_dec clss confl
by (clarsimp simp: twl_st_init twl_st_wl_init twl_st_l_init)
done
qed
have empty_clauses: ‹RETURN (True, fst init_state0)
≤ ⇓ ?A
(SPEC
(λ(b, U). b ⟶ conclusive_CDCL_run (mset `# mset CS) S U))›
if
TS: ‹(T, S)
∈ {(S, T).
(init_dt_spec0 CS (to_init_state0 init_state0) S) ∧
(T = init_state (mset `# mset CS))}› and
[simp]: ‹CS = []›
for bS bT failed T failed' S
proof -
let ?CS = ‹mset `# mset CS›
have [dest]: ‹cdcl⇩W_restart_mset.cdcl⇩W ([], {#}, {#}, None) (a, aa, ab, b) ⟹ False›
for a aa ab b
by (metis cdcl⇩W_restart_mset.cdcl⇩W.cases cdcl⇩W_restart_mset.cdcl⇩W_stgy.conflict'
cdcl⇩W_restart_mset.cdcl⇩W_stgy.propagate' cdcl⇩W_restart_mset.other'
cdcl⇩W_stgy_cdcl⇩W_init_state_empty_no_step init_state.simps)
show ?thesis
by (rule RETURN_RES_refine, rule exI[of _ ‹(True, init_state {#})›])
(use that in ‹auto simp: conclusive_CDCL_run_def init_state0_def›)
qed
have extract_atms_clss_nempty: ‹extract_atms_clss CS {} ≠ {}›
if
TS: ‹(T, S)
∈ {(S, T).
(init_dt_spec0 CS (to_init_state0 init_state0) S) ∧
(T = init_state (mset `# mset CS))}› and
‹CS ≠ []› and
‹¬get_conflict (fst T) ≠ None›
for bS bT failed T failed' S
proof -
show ?thesis
using that
by (cases T; cases CS)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
qed
have cdcl_twl_stgy_restart_prog: ‹cdcl_twl_stgy_restart_prog_bounded (fst T)
≤ ⇓ {((b, S), b', T). b = b' ∧ (b ⟶ T = state⇩W_of S)}
(SPEC (λ(b, U). b ⟶ conclusive_CDCL_run (mset `# mset CS) S U))› (is ?G1)
if
bT_bS: ‹(T, S)
∈ {(S, T).
(init_dt_spec0 CS (to_init_state0 init_state0) S) ∧
(T = init_state (mset `# mset CS))}› and
‹CS ≠ []› and
confl: ‹¬get_conflict (fst T) ≠ None› and
CS_nempty[simp]: ‹CS ≠ []› and
‹extract_atms_clss CS {} ≠ {}› and
‹clause `# get_clauses (fst T) + unit_clss (fst T) + subsumed_clauses (fst T) = mset `# mset CS› and
‹get_learned_clss (fst T) = {#}›
for bS bT failed T failed' S
proof -
let ?CS = ‹mset `# mset CS›
have
struct_invs: ‹twl_struct_invs_init T› and
clss_to_upd: ‹clauses_to_update_init T = {#}› and
count_dec: ‹∀s∈set (get_trail_init T). ¬ is_decided s› and
‹get_conflict_init T = None ⟶
literals_to_update_init T =
uminus `# lit_of `# mset (get_trail_init T)› and
clss: ‹mset `# mset CS +
clause `# get_init_clauses_init (to_init_state0 init_state0) +
other_clauses_init (to_init_state0 init_state0) +
get_unit_init_clauses_init (to_init_state0 init_state0) +
get_subsumed_init_clauses_init (to_init_state0 init_state0) =
clause `# get_init_clauses_init T + other_clauses_init T +
get_unit_init_clauses_init T + get_subsumed_init_clauses_init T› and
learned: ‹get_learned_clauses_init (to_init_state0 init_state0) =
get_learned_clauses_init T›
‹get_unit_learned_clauses_init T =
get_unit_learned_clauses_init (to_init_state0 init_state0)›
‹get_subsumed_learned_clauses_init T =
get_subsumed_learned_clauses_init (to_init_state0 init_state0)› and
stgy_invs: ‹twl_stgy_invs (fst T)› and
oth: ‹other_clauses_init T ≠ {#} ⟶ get_conflict_init T ≠ None› and
‹{#} ∈# mset `# mset CS ⟶ get_conflict_init T ≠ None› and
‹get_conflict_init (to_init_state0 init_state0) ≠ None ⟶
get_conflict_init (to_init_state0 init_state0) = get_conflict_init T›
using bT_bS unfolding init_dt_wl_spec_def init_dt_spec0_def
Set.mem_Collect_eq simp_thms prod.case apply -
apply normalize_goal+
by metis+
have struct_invs: ‹twl_struct_invs (fst T)›
by (rule twl_struct_invs_init_twl_struct_invs)
(use struct_invs oth confl in ‹auto simp: twl_st_init›)
have clss_to_upd: ‹clauses_to_update (fst T) = {#}›
using clss_to_upd by (auto simp: twl_st_init)
have conclusive_le: ‹conclusive_TWL_run (fst T)
≤ ⇓ {(S, T). T = state⇩W_of S}
(SPEC
(conclusive_CDCL_run (mset `# mset CS) (init_state (mset `# mset CS))))›
unfolding IsaSAT.conclusive_TWL_run_def
proof (rule RES_refine)
fix Ta
assume s: ‹Ta ∈ {Ta.
∃n n'.
cdcl_twl_stgy_restart_with_leftovers⇧*⇧* (fst T, n) (Ta, n') ∧
final_twl_state Ta}›
then obtain n n' where
twl: ‹cdcl_twl_stgy_restart_with_leftovers⇧*⇧* (fst T, n) (Ta, n')› and
final: ‹final_twl_state Ta›
by blast
have stgy_T_Ta: ‹cdcl⇩W_restart_mset.cdcl⇩W_restart_stgy⇧*⇧* (state⇩W_of (fst T), n) (state⇩W_of Ta, n')›
using rtranclp_cdcl_twl_stgy_restart_with_leftovers_cdcl⇩W_restart_stgy[OF twl] struct_invs
stgy_invs by simp
have ‹cdcl⇩W_restart_mset.cdcl⇩W_restart_stgy⇧*⇧* (state⇩W_of (fst T), n) (state⇩W_of Ta, n')›
using rtranclp_cdcl_twl_stgy_restart_with_leftovers_cdcl⇩W_restart_stgy[OF twl] struct_invs
stgy_invs by simp
have struct_invs_x: ‹twl_struct_invs Ta›
using twl struct_invs rtranclp_cdcl_twl_stgy_restart_with_leftovers_twl_struct_invs[OF twl]
by simp
then have all_struct_invs_x: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (state⇩W_of Ta)›
unfolding twl_struct_invs_def
by blast
have M_lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv ([], mset `# mset CS, {#}, None)›
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def)
have learned': ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause ([], mset `# mset CS, {#}, None)›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by auto
have ent: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init ([], mset `# mset CS, {#}, None)›
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def)
define MW where ‹MW ≡ get_trail_init T›
have CS_clss: ‹cdcl⇩W_restart_mset.clauses (state⇩W_of (fst T)) = mset `# mset CS›
using learned clss oth confl unfolding clauses_def to_init_state0_def init_state0_def
cdcl⇩W_restart_mset.clauses_def
by (cases T) auto
have n_d: ‹no_dup MW› and
propa: ‹⋀L mark a b. a @ Propagated L mark # b = MW ⟹
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› and
clss_in_clss: ‹set (get_all_mark_of_propagated MW) ⊆ set_mset ?CS›
using struct_invs unfolding twl_struct_invs_def twl_struct_invs_init_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
clauses_def MW_def clss to_init_state0_def init_state0_def CS_clss[symmetric]
by ((cases T; auto)+)[3]
have count_dec': ‹∀L∈set MW. ¬is_decided L›
using count_dec unfolding MW_def twl_st_init by auto
have st_W: ‹state⇩W_of (fst T) = (MW, ?CS, {#}, None)›
using clss learned confl oth
by (cases T) (auto simp: state_wl_l_init_def state_wl_l_def twl_st_l_init_def
mset_take_mset_drop_mset mset_take_mset_drop_mset' clauses_def MW_def
added_only_watched_def state_wl_l_init'_def
to_init_state0_def init_state0_def
simp del: all_clss_l_ran_m
simp: all_clss_lf_ran_m[symmetric])
have 0: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy⇧*⇧* ([], ?CS, {#}, None)
(MW, ?CS, {#}, None)›
using n_d count_dec' propa clss_in_clss
proof (induction MW)
case Nil
then show ?case by auto
next
case (Cons K MW) note IH = this(1) and H = this(2-) and n_d = this(2) and dec = this(3) and
propa = this(4) and clss_in_clss = this(5)
let ?init = ‹([], mset `# mset CS, {#}, None)›
let ?int = ‹(MW, mset `# mset CS, {#}, None)›
let ?final = ‹(K # MW, mset `# mset CS, {#}, None)›
obtain L C where
K: ‹K = Propagated L C›
using dec by (cases K) auto
term ?init
have 1: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy⇧*⇧* ?init ?int›
apply (rule IH)
subgoal using n_d by simp
subgoal using dec by simp
subgoal for M2 L' mark M1
using K propa[of ‹K # M2› L' mark M1]
by (auto split: if_splits)
subgoal using clss_in_clss by (auto simp: K)
done
have ‹MW ⊨as CNot (remove1_mset L C)› and ‹L ∈# C›
using propa[of ‹[]› L C ‹MW›]
by (auto simp: K)
moreover have ‹C ∈# cdcl⇩W_restart_mset.clauses (MW, mset `# mset CS, {#}, None)›
using clss_in_clss by (auto simp: K clauses_def split: if_splits)
ultimately have ‹cdcl⇩W_restart_mset.propagate ?int
(Propagated L C # MW, mset `# mset CS, {#}, None)›
using n_d apply -
apply (rule cdcl⇩W_restart_mset.propagate_rule[of _ ‹C› L])
by (auto simp: K)
then have 2: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy ?int ?final›
by (auto simp add: K dest!: cdcl⇩W_restart_mset.cdcl⇩W_stgy.propagate')
show ?case
apply (rule rtranclp.rtrancl_into_rtrancl[OF 1])
apply (rule 2)
.
qed
with cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_stgy_cdcl⇩W_restart_stgy[OF 0, of n]
have stgy: ‹cdcl⇩W_restart_mset.cdcl⇩W_restart_stgy⇧*⇧* (([], mset `# mset CS, {#}, None), n)
(state⇩W_of Ta, n')›
using stgy_T_Ta unfolding st_W by simp
have entailed: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of Ta)›
apply (rule cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_learned_clauses_entailed)
apply (rule cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_stgy_cdcl⇩W_restart[OF stgy, unfolded fst_conv])
apply (rule learned')
apply (rule M_lev)
apply (rule ent)
done
consider
(ns) ‹no_step cdcl_twl_stgy Ta› |
(stop) ‹get_conflict Ta ≠ None› and ‹count_decided (get_trail Ta) = 0›
using final unfolding final_twl_state_def by auto
then show ‹∃s'∈Collect (conclusive_CDCL_run (mset `# mset CS)
(init_state (mset `# mset CS))).
(Ta, s') ∈ {(S, T). T = state⇩W_of S}›
proof cases
case ns
from no_step_cdcl_twl_stgy_no_step_cdcl⇩W_stgy[OF this struct_invs_x]
have ‹no_step cdcl⇩W_restart_mset.cdcl⇩W (state⇩W_of Ta)›
by (blast dest: cdcl⇩W_ex_cdcl⇩W_stgy)
then show ?thesis
apply -
apply (rule bexI[of _ ‹state⇩W_of Ta›])
using twl stgy s
unfolding conclusive_CDCL_run_def
by auto
next
case stop
have ‹unsatisfiable (set_mset (init_clss (state⇩W_of Ta)))›
apply (rule conflict_of_level_unsatisfiable)
apply (rule all_struct_invs_x)
using entailed stop by (auto simp: twl_st)
then have ‹unsatisfiable (mset ` set CS)›
using cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_init_clss[symmetric, OF
cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_stgy_cdcl⇩W_restart[OF stgy]]
by auto
then show ?thesis
using stop
by (auto simp: twl_st_init twl_st conclusive_CDCL_run_def)
qed
qed
then have conclusive_le: ‹conclusive_TWL_run_bounded (fst T)
≤ ⇓ {((b, S), b', T). b = b' ∧ (b ⟶ T = state⇩W_of S)}
(SPEC (λ(b, U). b ⟶ conclusive_CDCL_run (mset `# mset CS) S U))›
using bT_bS
unfolding conclusive_TWL_run_bounded_def
conclusive_TWL_run_def conc_fun_RES
less_eq_nres.simps subset_iff apply -
apply (intro allI)
apply (rename_tac t)
apply (drule_tac x= ‹(snd t)› in spec)
by (fastforce)
show ?G1
apply (rule cdcl_twl_stgy_restart_prog_bounded_spec[THEN order_trans])
apply (rule struct_invs; fail)
apply (rule stgy_invs; fail)
apply (rule clss_to_upd; fail)
apply (use confl in ‹simp add: twl_st_init›; fail)
apply (rule conclusive_le)
done
qed
text ‹The following does not relate anything, because the initialisation is already
doing some steps.›
have [refine0]:
‹SPEC
(λT. init_dt_spec0 CS (to_init_state0 init_state0) T)
≤ ⇓ {(S, T).
(init_dt_spec0 CS (to_init_state0 init_state0) S) ∧
(T = init_state (mset `# mset CS))}
(SPEC (λT. T = init_state (mset `# mset CS)))›
by (rule RES_refine)
(auto simp: init_state0_def to_init_state0_def
extract_atms_clss_alt_def intro!: )[]
show ?thesis
unfolding SAT0_bounded_def SAT_bounded_def
apply (subst Let_def)
apply (refine_vcg)
subgoal by (auto simp: RETURN_def intro!: RES_refine)
subgoal by (auto simp: RETURN_def intro!: RES_refine)
apply (rule lhs_step_If)
subgoal
by (rule conflict_during_init)
apply (rule lhs_step_If)
subgoal
by (rule empty_clauses) assumption+
apply (intro ASSERT_leI)
subgoal for b T
by (rule extract_atms_clss_nempty)
subgoal for S T
by (cases S)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for S T
by (cases S)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for S T
by (cases S)
(auto simp: init_state0_def to_init_state0_def init_dt_spec0_def
extract_atms_clss_alt_def)
subgoal for S T
by (rule cdcl_twl_stgy_restart_prog)
done
qed
definition SAT_l_bounded :: ‹nat clause_l list ⇒ (bool × nat twl_st_l) nres› where
‹SAT_l_bounded CS = do{
let S = init_state_l;
T ← init_dt CS (to_init_state_l S);
finished ← SPEC (λ_ :: bool. True);
if ¬finished then do {
RETURN (False, fst init_state_l)
} else do {
let T = fst T;
if get_conflict_l T ≠ None
then RETURN (True, T)
else if CS = [] then RETURN (True, fst init_state_l)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update_l T = {#});
ASSERT(mset `# ran_mf (get_clauses_l T) + get_unit_clauses_l T + get_subsumed_clauses_l T= mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_l T) = {#});
cdcl_twl_stgy_restart_prog_bounded_l T
}
}
}›
lemma SAT_l_bounded_SAT0_bounded:
assumes dist: ‹Multiset.Ball (mset `# mset CS) distinct_mset›
shows ‹SAT_l_bounded CS ≤ ⇓ {((b, T),(b', T')). b=b' ∧ (b ⟶ (T, T') ∈ twl_st_l None)} (SAT0_bounded CS)›
proof -
have inj: ‹inj (uminus :: _ literal ⇒ _)›
by (auto simp: inj_on_def)
have [simp]: ‹{#- lit_of x. x ∈# A#} = {#- lit_of x. x ∈# B#} ⟷
{#lit_of x. x ∈# A#} = {#lit_of x. x ∈# B#}› for A B :: ‹(nat literal, nat literal,
nat) annotated_lit multiset›
unfolding multiset.map_comp[unfolded comp_def, symmetric]
apply (subst inj_image_mset_eq_iff[of uminus])
apply (rule inj)
by (auto simp: inj_on_def)[]
have get_unit_twl_st_l: ‹(s, x) ∈ twl_st_l_init ⟹ get_learned_unit_clauses_l_init s = {#} ⟹
learned_clss_l (get_clauses_l_init s) = {#} ⟹
{#mset (fst x). x ∈# ran_m (get_clauses_l_init s)#} +
(get_unit_clauses_l_init s + get_subsumed_init_clauses_l_init s) =
clause `# get_init_clauses_init x + (get_unit_init_clauses_init x +
get_subsumed_init_clauses_init x)› for s x
apply (cases s; cases x)
apply (auto simp: twl_st_l_init_def mset_take_mset_drop_mset')
by (metis (mono_tags, lifting) add.right_neutral all_clss_l_ran_m)
have init_dt_pre: ‹init_dt_pre CS (to_init_state_l init_state_l)›
by (rule init_dt_pre_init) (use dist in auto)
have init_dt_spec0: ‹init_dt CS (to_init_state_l init_state_l)
≤ ⇓{((T),T'). (T, T') ∈ twl_st_l_init ∧ twl_list_invs (fst T) ∧
clauses_to_update_l (fst T) = {#}}
(SPEC (init_dt_spec0 CS (to_init_state0 init_state0)))›
apply (rule init_dt_full[THEN order_trans])
subgoal by (rule init_dt_pre)
subgoal
apply (rule RES_refine)
unfolding init_dt_spec_def Set.mem_Collect_eq init_dt_spec0_def
to_init_state_l_def init_state_l_def
to_init_state0_def init_state0_def
apply normalize_goal+
apply (rule_tac x=x in bexI)
subgoal for s x by (auto simp: twl_st_l_init)
subgoal for s x
unfolding Set.mem_Collect_eq
by (simp_all add: twl_st_init twl_st_l_init twl_st_l_init_no_decision_iff get_unit_twl_st_l)
done
done
have init_state0: ‹ ((True, fst init_state_l), True, fst init_state0)
∈ {((b, T), b', T'). b=b' ∧ (b ⟶ (T, T') ∈ twl_st_l None)}›
by (auto simp: twl_st_l_def init_state0_def init_state_l_def)
show ?thesis
unfolding SAT_l_bounded_def SAT0_bounded_def
apply (refine_vcg init_dt_spec0)
subgoal by auto
subgoal by (auto simp: twl_st_l_init twl_st_init)
subgoal by (auto simp: twl_st_l_init_alt_def)
subgoal by (auto simp: twl_st_l_init_alt_def)
subgoal by auto
subgoal by (rule init_state0)
subgoal for b ba T Ta
unfolding all_clss_lf_ran_m[symmetric] image_mset_union to_init_state0_def init_state0_def
by (cases T; cases Ta)
(auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset'
init_dt_spec0_def)
subgoal for b ba T Ta
unfolding all_clss_lf_ran_m[symmetric] image_mset_union
by (cases T; cases Ta) (auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset')
subgoal for T Ta finished finisheda
by (cases T; cases Ta) (auto simp: twl_st_l_init twl_st_init twl_st_l_init_def mset_take_mset_drop_mset')
subgoal for T Ta finished finisheda
by (rule cdcl_twl_stgy_restart_prog_bounded_l_cdcl_twl_stgy_restart_prog_bounded[THEN fref_to_Down, of _ ‹fst Ta›,
THEN order_trans])
(auto simp: twl_st_l_init_alt_def mset_take_mset_drop_mset' intro!: conc_fun_R_mono)
done
qed
definition SAT_wl_bounded :: ‹nat clause_l list ⇒ (bool × nat twl_st_wl) nres› where
‹SAT_wl_bounded CS = do{
ASSERT(isasat_input_bounded (mset_set (extract_atms_clss CS {})));
ASSERT(distinct_mset_set (mset ` set CS));
let 𝒜⇩i⇩n' = extract_atms_clss CS {};
let S = init_state_wl;
T ← init_dt_wl' CS (to_init_state S);
let T = from_init_state T;
finished ← SPEC (λ_ :: bool. True);
if ¬finished then do {
RETURN(finished, T)
} else do {
if get_conflict_wl T ≠ None
then RETURN (True, T)
else if CS = [] then RETURN (True, ([], fmempty, None, {#}, {#}, {#}, {#}, {#}, λ_. undefined))
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT(isasat_input_bounded_nempty (mset_set 𝒜⇩i⇩n'));
ASSERT(mset `# ran_mf (get_clauses_wl T) + get_unit_clauses_wl T + get_subsumed_clauses_wl T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_wl T) = {#});
T ← rewatch_st (finalise_init T);
cdcl_twl_stgy_restart_prog_bounded_wl T
}
}
}›
lemma SAT_l_bounded_alt_def:
‹SAT_l_bounded CS = do{
𝒜 ← RETURN (); ⌦‹atoms›
let S = init_state_l;
𝒜 ← RETURN (); ⌦‹initialisation›
T ← init_dt CS (to_init_state_l S);
failed ← SPEC (λ_ :: bool. True);
if ¬failed then do {
RETURN(failed, fst init_state_l)
} else do {
let T = T;
if get_conflict_l_init T ≠ None
then RETURN (True, fst T)
else if CS = [] then RETURN (True, fst init_state_l)
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT (clauses_to_update_l (fst T) = {#});
ASSERT(mset `# ran_mf (get_clauses_l (fst T)) + get_unit_clauses_l (fst T) + get_subsumed_clauses_l (fst T) = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_l (fst T)) = {#});
let T = fst T;
cdcl_twl_stgy_restart_prog_bounded_l T
}
}
}›
unfolding SAT_l_bounded_def by (auto cong: if_cong Let_def twl_st_l_init)
lemma SAT_wl_bounded_SAT_l_bounded:
assumes
dist: ‹Multiset.Ball (mset `# mset CS) distinct_mset› and
bounded: ‹isasat_input_bounded (mset_set (⋃C∈set CS. atm_of ` set C))›
shows ‹SAT_wl_bounded CS ≤ ⇓ {((b, T),(b', T')). b =b' ∧ (b ⟶ (T, T') ∈ state_wl_l None)} (SAT_l_bounded CS)›
proof -
have extract_atms_clss: ‹(extract_atms_clss CS {}, ()) ∈ {(x, _). x = extract_atms_clss CS {}}›
by auto
have init_dt_wl_pre: ‹init_dt_wl_pre CS (to_init_state init_state_wl)›
by (rule init_dt_wl_pre) (use dist in auto)
have init_rel: ‹(to_init_state init_state_wl, to_init_state_l init_state_l)
∈ state_wl_l_init›
by (auto simp: init_dt_pre_def state_wl_l_init_def state_wl_l_init'_def
twl_st_l_init_def twl_init_invs to_init_state_def init_state_wl_def
init_state_l_def to_init_state_l_def)[]
define init_dt_wl_rel where
‹init_dt_wl_rel S ≡ ({(T, T'). RETURN T ≤ init_dt_wl' CS S ∧ T' = ()})› for S
have init_dt_wl':
‹init_dt_wl' CS S ≤ SPEC (λc. (c, ()) ∈ (init_dt_wl_rel S))›
if
‹init_dt_wl_pre CS S› and
‹(S, S') ∈ state_wl_l_init› and
‹∀C∈set CS. distinct C›
for S S'
proof -
have [simp]: ‹(U, U') ∈ ({(T, T'). RETURN T ≤ init_dt_wl' CS S ∧ remove_watched T = T'} O
state_wl_l_init) ⟷ ((U, U') ∈ {(T, T'). remove_watched T = T'} O
state_wl_l_init ∧ RETURN U ≤ init_dt_wl' CS S)› for S S' U U'
by auto
have H: ‹A ≤ ⇓ ({(S, S'). P S S'}) B ⟷ A ≤ ⇓ ({(S, S'). RETURN S ≤ A ∧ P S S'}) B›
for A B P R
by (simp add: pw_conc_inres pw_conc_nofail pw_le_iff p2rel_def)
have nofail: ‹nofail (init_dt_wl' CS S)›
apply (rule SPEC_nofail)
apply (rule order_trans)
apply (rule init_dt_wl'_spec[unfolded conc_fun_RES])
using that by auto
have H: ‹A ≤ ⇓ ({(S, S'). P S S'} O R) B ⟷ A ≤ ⇓ ({(S, S'). RETURN S ≤ A ∧ P S S'} O R) B›
for A B P R
by (smt Collect_cong H case_prod_cong conc_fun_chain)
show ?thesis
unfolding init_dt_wl_rel_def
using that
by (auto simp: nofail no_fail_spec_le_RETURN_itself)
qed
have conflict_during_init:
‹((True, ([], fmempty, None, {#}, {#}, {#}, {#}, {#}, λ_. undefined)), (True, fst init_state_l))
∈ {((b, T), b', T'). b = b' ∧ (b ⟶ (T, T') ∈ state_wl_l None)}›
by (auto simp: init_state_l_def state_wl_l_def)
have init_init_dt: ‹RETURN (from_init_state T)
≤ ⇓ ({(S, S'). S = fst S'} O {(S :: nat twl_st_wl_init_full, S' :: nat twl_st_wl_init).
remove_watched S = S'} O state_wl_l_init)
(init_dt CS (to_init_state_l init_state_l))›
(is ‹_ ≤ ⇓ ?init_dt _ ›)
if
‹(extract_atms_clss CS {}, (𝒜::unit)) ∈ {(x, _). x = extract_atms_clss CS {}}› and
‹(T, Ta) ∈ init_dt_wl_rel (to_init_state init_state_wl)›
for 𝒜 T Ta
proof -
have 1: ‹RETURN T ≤ init_dt_wl' CS (to_init_state init_state_wl)›
using that by (auto simp: init_dt_wl_rel_def from_init_state_def)
have 2: ‹RETURN (from_init_state T) ≤ ⇓ {(S, S'). S = fst S'} (RETURN T)›
by (auto simp: RETURN_refine from_init_state_def)
have 2: ‹RETURN (from_init_state T) ≤ ⇓ {(S, S'). S = fst S'} (init_dt_wl' CS (to_init_state init_state_wl))›
apply (rule 2[THEN order_trans])
apply (rule ref_two_step')
apply (rule 1)
done
show ?thesis
apply (rule order_trans)
apply (rule 2)
unfolding conc_fun_chain[symmetric]
apply (rule ref_two_step')
unfolding conc_fun_chain
apply (rule init_dt_wl'_init_dt)
apply (rule init_dt_wl_pre)
subgoal by (auto simp: to_init_state_def init_state_wl_def to_init_state_l_def
init_state_l_def state_wl_l_init_def state_wl_l_init'_def)
subgoal using assms by auto
done
qed
have cdcl_twl_stgy_restart_prog_wl_D2: ‹cdcl_twl_stgy_restart_prog_bounded_wl U'
≤ ⇓ {((b, T), (b', T')). b =b' ∧ (b ⟶ (T, T') ∈ state_wl_l None)}
(cdcl_twl_stgy_restart_prog_bounded_l (fst T'))› (is ?A)
if
U': ‹(U', fst T') ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ⇩i⇩n S}›
for 𝒜 b b' T 𝒜' T' c c' U'
proof -
have 1: ‹ {(T, T'). (T, T') ∈ state_wl_l None} = state_wl_l None›
by auto
have lits: ‹literals_are_ℒ⇩i⇩n (all_atms_st (U')) (U')›
using U' by (auto simp: finalise_init_def correct_watching.simps)
show ?A
apply (rule cdcl_twl_stgy_restart_prog_bounded_wl_spec[unfolded fref_param1, THEN fref_to_Down, THEN order_trans])
apply fast
using U' by (auto simp: finalise_init_def intro!: conc_fun_R_mono)
qed
have rewatch_st_fst: ‹rewatch_st (finalise_init (from_init_state T))
≤ SPEC (λc. (c, fst Ta) ∈ {(S, T). (S, T) ∈ state_wl_l None ∧ correct_watching S ∧ blits_in_ℒ⇩i⇩n S})›
(is ‹_ ≤ SPEC ?rewatch›)
if
‹(extract_atms_clss CS {}, 𝒜) ∈ {(x, _). x = extract_atms_clss CS {}}› and
T: ‹(T, 𝒜') ∈ init_dt_wl_rel (to_init_state init_state_wl)› and
T_Ta: ‹(from_init_state T, Ta)
∈ {(S, S'). S = fst S'} O
{(S, S'). remove_watched S = S'} O state_wl_l_init› and
‹¬ get_conflict_wl (from_init_state T) ≠ None› and
‹¬ get_conflict_l_init Ta ≠ None›
for 𝒜 b ba T 𝒜' Ta bb bc
proof -
have 1: ‹RETURN T ≤ init_dt_wl' CS (to_init_state init_state_wl)›
using T unfolding init_dt_wl_rel_def by auto
have 2: ‹RETURN T ≤ ⇓ {(S, S'). remove_watched S = S'}
(SPEC (init_dt_wl_spec CS (to_init_state init_state_wl)))›
using order_trans[OF 1 init_dt_wl'_spec[OF init_dt_wl_pre]] .
have empty_watched: ‹get_watched_wl (finalise_init (from_init_state T)) = (λ_. [])›
using 1 2 init_dt_wl'_spec[OF init_dt_wl_pre]
by (cases T; cases ‹init_dt_wl CS (init_state_wl, {#})›)
(auto simp: init_dt_wl_spec_def RETURN_RES_refine_iff
finalise_init_def from_init_state_def state_wl_l_init_def
state_wl_l_init'_def to_init_state_def to_init_state_l_def
init_state_l_def init_dt_wl'_def RES_RETURN_RES)
have 1: ‹length (aa ∝ x) ≥ 2› ‹distinct (aa ∝ x)›
if
struct: ‹twl_struct_invs_init
((af,
{#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l aa#},
{#}, y, ac, {#}, NS, US, {#}, ae),
OC)› and
x: ‹x ∈# dom_m aa› and
learned: ‹learned_clss_l aa = {#}›
for af aa y ac ae x OC NS US
proof -
have irred: ‹irred aa x›
using that by (cases ‹fmlookup aa x›) (auto simp: ran_m_def dest!: multi_member_split
split: if_splits)
have ‹Multiset.Ball
({#TWL_Clause (mset (watched_l (fst x))) (mset (unwatched_l (fst x)))
. x ∈# init_clss_l aa#} +
{#})
struct_wf_twl_cls›
using struct unfolding twl_struct_invs_init_def fst_conv twl_st_inv.simps
by fast
then show ‹length (aa ∝ x) ≥ 2› ‹distinct (aa ∝ x)›
using x learned in_ran_mf_clause_inI[OF x, of True] irred
by (auto simp: mset_take_mset_drop_mset' dest!: multi_member_split[of x]
split: if_splits)
qed
have min_len: ‹ x ∈# dom_m (get_clauses_wl (finalise_init (from_init_state T))) ⟹
distinct (get_clauses_wl (finalise_init (from_init_state T)) ∝ x) ∧
2 ≤ length (get_clauses_wl (finalise_init (from_init_state T)) ∝ x)›
for x
using 2
by (cases T)
(auto simp: init_dt_wl_spec_def RETURN_RES_refine_iff
finalise_init_def from_init_state_def state_wl_l_init_def
state_wl_l_init'_def to_init_state_def to_init_state_l_def
init_state_l_def init_dt_wl'_def RES_RETURN_RES
init_dt_spec_def init_state_wl_def twl_st_l_init_def
intro: 1)
show ?thesis
apply (rule rewatch_st_correctness[THEN order_trans])
subgoal by (rule empty_watched)
subgoal by (rule min_len)
subgoal using T_Ta by (auto simp: finalise_init_def
state_wl_l_init_def state_wl_l_init'_def state_wl_l_def
correct_watching_init_correct_watching
correct_watching_init_blits_in_ℒ⇩i⇩n)
done
qed
have all_le: ‹∀C∈set CS. ∀L∈set C. nat_of_lit L ≤ uint32_max›
proof (intro ballI)
fix C L
assume ‹C ∈ set CS› and ‹L ∈ set C›
then have ‹L ∈# ℒ⇩a⇩l⇩l (mset_set (⋃C∈set CS. atm_of ` set C))›
by (auto simp: in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
then show ‹nat_of_lit L ≤ uint32_max›
using assms by auto
qed
have [simp]: ‹(Tc, fst Td) ∈ state_wl_l None ⟹
get_conflict_l_init Td = get_conflict_wl Tc› for Tc Td
by (cases Tc; cases Td; auto simp: state_wl_l_def)
show ?thesis
unfolding SAT_wl_bounded_def SAT_l_bounded_alt_def
apply (refine_vcg extract_atms_clss init_dt_wl' init_rel)
subgoal using assms unfolding extract_atms_clss_alt_def by auto
subgoal using assms unfolding distinct_mset_set_def by auto
subgoal by (rule init_dt_wl_pre)
subgoal using dist by auto
apply (rule init_init_dt; assumption)
subgoal by auto
subgoal by auto
subgoal by (auto simp: from_init_state_def state_wl_l_init_def state_wl_l_init'_def)
subgoal by (auto simp: from_init_state_def state_wl_l_init_def state_wl_l_init'_def
state_wl_l_def)
subgoal by auto
subgoal by (rule conflict_during_init)
subgoal using bounded by (auto simp: isasat_input_bounded_nempty_def extract_atms_clss_alt_def
simp del: isasat_input_bounded_def)
subgoal by (auto simp: isasat_input_bounded_nempty_def extract_atms_clss_alt_def state_wl_l_init'_def
state_wl_l_init_def
simp del: isasat_input_bounded_def)
subgoal by (auto simp: isasat_input_bounded_nempty_def extract_atms_clss_alt_def state_wl_l_init'_def
state_wl_l_init_def
simp del: isasat_input_bounded_def)
apply (rule rewatch_st_fst; assumption)
subgoal for 𝒜 T 𝒜' Ta finished finished'
unfolding twl_st_l_init[symmetric]
by (rule cdcl_twl_stgy_restart_prog_wl_D2)
done
qed
definition SAT_bounded' :: ‹nat clauses ⇒ (bool × nat literal list option) nres› where
‹SAT_bounded' CS = do {
(b, T) ← SAT_bounded CS;
RETURN(b, if conflicting T = None then Some (map lit_of (trail T)) else None)
}
›
definition model_if_satisfiable_bounded :: ‹nat clauses ⇒ (bool × nat literal list option) nres› where
‹model_if_satisfiable_bounded CS = SPEC (λ(b, M). b ⟶
(if satisfiable (set_mset CS) then M ≠ None ∧ set (the M) ⊨sm CS else M = None))›
lemma SAT_bounded_model_if_satisfiable:
‹(SAT_bounded', model_if_satisfiable_bounded) ∈ [λCS. (∀C ∈# CS. distinct_mset C)]⇩f Id→
⟨{((b, S), (b', T)). b = b' ∧ (b ⟶ S = T)}⟩nres_rel›
(is ‹_ ∈[λCS. ?P CS]⇩f Id → _›)
proof -
have H: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant (init_state CS)›
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (init_state CS)›
if ‹?P CS› for CS
using that by (auto simp:
twl_struct_invs_def twl_st_inv.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_alt_def cdcl⇩W_restart_mset.no_smaller_propa_def
past_invs.simps clauses_def twl_list_invs_def twl_stgy_invs_def clause_to_update_def
cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
cdcl⇩W_restart_mset.no_smaller_confl_def
distinct_mset_set_def)
have H: ‹s ∈ {M. if satisfiable (set_mset CS) then M ≠ None ∧ set (the M) ⊨sm CS else M = None}›
if
dist: ‹Multiset.Ball CS distinct_mset› and
[simp]: ‹CS' = CS› and
s: ‹s ∈ (λT. if conflicting T = None then Some (map lit_of (trail T)) else None) `
Collect (conclusive_CDCL_run CS' (init_state CS'))›
for s :: ‹nat literal list option› and CS CS'
proof -
obtain T where
s: ‹(s = Some (map lit_of (trail T)) ∧ conflicting T = None) ∨
(s = None ∧ conflicting T ≠ None)› and
conc: ‹conclusive_CDCL_run CS' ([], CS', {#}, None) T›
using s by auto force
consider
n n' where ‹cdcl⇩W_restart_mset.cdcl⇩W_restart_stgy⇧*⇧* (([], CS', {#}, None), n) (T, n')›
‹no_step cdcl⇩W_restart_mset.cdcl⇩W T› |
‹CS' ≠ {#}› and ‹conflicting T ≠ None› and ‹backtrack_lvl T = 0› and
‹unsatisfiable (set_mset CS')›
using conc unfolding conclusive_CDCL_run_def
by auto
then show ?thesis
proof cases
case (1 n n') note st = this(1) and ns = this(2)
have ‹no_step cdcl⇩W_restart_mset.cdcl⇩W_stgy T›
using ns cdcl⇩W_restart_mset.cdcl⇩W_stgy_cdcl⇩W by blast
then have full_T: ‹full cdcl⇩W_restart_mset.cdcl⇩W_stgy T T›
unfolding full_def by blast
have invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant T›
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv T›
using st cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_dcl⇩W_all_struct_inv[OF st]
cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_dcl⇩W_stgy_invariant[OF st]
H[OF dist] by auto
have res: ‹cdcl⇩W_restart_mset.cdcl⇩W_restart⇧*⇧* ([], CS', {#}, None) T›
using cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_stgy_cdcl⇩W_restart[OF st] by simp
have ent: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init T›
using cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_learned_clauses_entailed[OF res] H[OF dist]
unfolding ‹CS' = CS› cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by simp
have [simp]: ‹init_clss T = CS›
using cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_restart_init_clss[OF res] by simp
show ?thesis
using cdcl⇩W_restart_mset.full_cdcl⇩W_stgy_inv_normal_form[OF full_T invs ent] s
by (auto simp: true_annots_true_cls lits_of_def)
next
case 2
moreover have ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (init_state CS)›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
by auto
ultimately show ?thesis
using H[OF dist] cdcl⇩W_restart_mset.full_cdcl⇩W_stgy_inv_normal_form[of ‹init_state CS›
‹init_state CS›] s
by auto
qed
qed
have H: ‹
∃s'∈{(b, M).
b ⟶
(if satisfiable (set_mset CS) then M ≠ None ∧ set (the M) ⊨sm CS
else M = None)}.
(s, s') ∈ {((b, S), b', T). b = b' ∧ (b ⟶ S = T)}›
if ‹Multiset.Ball CS' distinct_mset›
‹CS = CS'› and
‹s ∈ uncurry
(λb T. (b, if conflicting T = None then Some (map lit_of (trail T))
else None)) `
(if ¬ xb then {(xb, xa)}
else {(b, U). b ⟶ conclusive_CDCL_run CS' xa U})› and
‹xa ∈ {T. T = init_state CS'}›
for CS CS' :: ‹nat literal multiset multiset› and s and xa and xb :: bool
proof -
obtain b T where
s: ‹s = (b, T)› by (cases s)
have
‹¬xb ⟶ ¬b› and
b: ‹b ⟶ T ∈ (λT. if conflicting T = None then Some (map lit_of (trail T)) else None) `
Collect (conclusive_CDCL_run CS (init_state CS))›
using that(3,4)
by (force simp add: image_iff s that split: if_splits)+
show ?thesis
proof (cases b)
case True
then have T: ‹T ∈ (λT. if conflicting T = None then Some (map lit_of (trail T)) else None) `
Collect (conclusive_CDCL_run CS (init_state CS))›
using b by fast
show ?thesis
using H[OF that(1,2) T]
by (rule_tac x = ‹s› in bexI)
(auto simp add: s True that)
qed (auto simp: s)
qed
have if_RES: ‹(if xb then RETURN x
else RES P) = (RES (if xb then {x} else P))› for x xb P
by (auto simp: RETURN_def)
show ?thesis
unfolding SAT_bounded'_def model_if_satisfiable_bounded_def SAT_bounded_def Let_def
nres_monad3
apply (intro frefI nres_relI)
apply refine_vcg
subgoal for CS' CS
unfolding RES_RETURN_RES RES_RES_RETURN_RES2 if_RES
apply (rule RES_refine)
unfolding pair_in_Id_conv bex_triv_one_point1 bex_triv_one_point2
using H by presburger
done
qed
lemma SAT_bounded_model_if_satisfiable':
‹(uncurry (λ_. SAT_bounded'), uncurry (λ_. model_if_satisfiable_bounded)) ∈
[λ(_, CS). (∀C ∈# CS. distinct_mset C)]⇩f Id ×⇩r Id→ ⟨{((b, S), (b', T)). b = b' ∧ (b ⟶ S = T)}⟩nres_rel›
using SAT_bounded_model_if_satisfiable unfolding fref_def
by auto
definition SAT_l_bounded' where
‹SAT_l_bounded' CS = do{
(b, S) ← SAT_l_bounded CS;
RETURN (b, if b ∧ get_conflict_l S = None then Some (map lit_of (get_trail_l S)) else None)
}›
definition SAT0_bounded' where
‹SAT0_bounded' CS = do{
(b, S) ← SAT0_bounded CS;
RETURN (b, if b ∧ get_conflict S = None then Some (map lit_of (get_trail S)) else None)
}›
lemma SAT_l_bounded'_SAT0_bounded':
assumes ‹Multiset.Ball (mset `# mset CS) distinct_mset›
shows ‹SAT_l_bounded' CS ≤ ⇓ {((b, S), (b', T)). b = b' ∧ (b ⟶ S = T)} (SAT0_bounded' CS)›
unfolding SAT_l_bounded'_def SAT0_bounded'_def
apply refine_vcg
apply (rule SAT_l_bounded_SAT0_bounded)
subgoal using assms by auto
subgoal by (auto simp: extract_model_of_state_def)
done
lemma SAT0_bounded'_SAT_bounded':
assumes ‹Multiset.Ball (mset `# mset CS) distinct_mset›
shows ‹SAT0_bounded' CS ≤ ⇓ {((b, S), (b', T)). b = b' ∧ (b ⟶ S = T)} (SAT_bounded' (mset `# mset CS))›
unfolding SAT_bounded'_def SAT0_bounded'_def
apply refine_vcg
apply (rule SAT0_bounded_SAT_bounded)
subgoal using assms by auto
subgoal by (auto simp: extract_model_of_state_def twl_st_l twl_st)
done
definition IsaSAT_bounded :: ‹nat clause_l list ⇒ (bool × nat literal list option) nres› where
‹IsaSAT_bounded CS = do{
(b, S) ← SAT_wl_bounded CS;
RETURN (b, if b ∧ get_conflict_wl S = None then extract_model_of_state S else extract_stats S)
}›
lemma IsaSAT_bounded_alt_def:
‹IsaSAT_bounded CS = do{
ASSERT(isasat_input_bounded (mset_set (extract_atms_clss CS {})));
ASSERT(distinct_mset_set (mset ` set CS));
let 𝒜⇩i⇩n' = extract_atms_clss CS {};
S ← RETURN init_state_wl;
T ← init_dt_wl' CS (to_init_state S);
failed ← SPEC (λ_ :: bool. True);
if ¬failed then do {
RETURN (False, extract_stats init_state_wl)
} else do {
let T = from_init_state T;
if get_conflict_wl T ≠ None
then RETURN (True, extract_stats T)
else if CS = [] then RETURN (True, Some [])
else do {
ASSERT (extract_atms_clss CS {} ≠ {});
ASSERT(isasat_input_bounded_nempty (mset_set 𝒜⇩i⇩n'));
ASSERT(mset `# ran_mf (get_clauses_wl T) + get_unit_clauses_wl T + get_subsumed_clauses_wl T = mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_wl T) = {#});
T ← rewatch_st T;
T ← RETURN (finalise_init T);
(b, S) ← cdcl_twl_stgy_restart_prog_bounded_wl T;
RETURN (b, if b ∧ get_conflict_wl S = None then extract_model_of_state S else extract_stats S)
}
}
}› (is ‹?A = ?B›) for CS opts
proof -
have H: ‹A = B ⟹ A ≤ ⇓ Id B› for A B
by auto
have 1: ‹?A ≤ ⇓ Id ?B›
unfolding IsaSAT_bounded_def SAT_wl_bounded_def nres_bind_let_law If_bind_distrib nres_monad_laws
Let_def finalise_init_def
apply (refine_vcg)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: extract_model_of_state_def)
subgoal by (auto simp: extract_model_of_state_def)
subgoal by auto
subgoal by auto
apply (rule H; solves auto)
apply (rule H; solves auto)
subgoal by (auto simp: extract_model_of_state_def)
done
have 2: ‹?B ≤ ⇓ Id ?A›
unfolding IsaSAT_bounded_def SAT_wl_bounded_def nres_bind_let_law If_bind_distrib nres_monad_laws
Let_def finalise_init_def
apply (refine_vcg)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: extract_model_of_state_def)
subgoal by auto
subgoal by auto
apply (rule H; solves auto)
apply (rule H; solves auto)
subgoal by auto
done
show ?thesis
using 1 2 by simp
qed
definition IsaSAT_bounded_heur :: ‹opts ⇒ nat clause_l list ⇒ (bool × (bool × nat literal list × stats)) nres› where
‹IsaSAT_bounded_heur opts CS = do{
ASSERT(isasat_input_bounded (mset_set (extract_atms_clss CS {})));
ASSERT(∀C∈set CS. ∀L∈set C. nat_of_lit L ≤ uint32_max);
let 𝒜⇩i⇩n' = mset_set (extract_atms_clss CS {});
ASSERT(isasat_input_bounded 𝒜⇩i⇩n');
ASSERT(distinct_mset 𝒜⇩i⇩n');
let 𝒜⇩i⇩n'' = virtual_copy 𝒜⇩i⇩n';
let b = opts_unbounded_mode opts;
S ← init_state_wl_heur_fast 𝒜⇩i⇩n';
(T::twl_st_wl_heur_init) ← init_dt_wl_heur False CS S;
let T = convert_state 𝒜⇩i⇩n'' T;
if isasat_fast_init T ∧ ¬is_failed_heur_init T
then do {
if ¬get_conflict_wl_is_None_heur_init T
then RETURN (True, empty_init_code)
else if CS = [] then do {stat ← empty_conflict_code; RETURN (True, stat)}
else do {
ASSERT(𝒜⇩i⇩n'' ≠ {#});
ASSERT(isasat_input_bounded_nempty 𝒜⇩i⇩n'');
_ ← isasat_information_banner T;
ASSERT((λ(M', N', D', Q', W', ((ns, m, fst_As, lst_As, next_search), to_remove), φ, clvls). fst_As ≠ None ∧
lst_As ≠ None) T);
ASSERT(rewatch_heur_st_fast_pre T);
T ← rewatch_heur_st_fast T;
ASSERT(isasat_fast_init T);
T ← finalise_init_code opts (T::twl_st_wl_heur_init);
ASSERT(isasat_fast T);
(b, U) ← cdcl_twl_stgy_restart_prog_bounded_wl_heur T;
RETURN (b, if b ∧ get_conflict_wl_is_None_heur U then extract_model_of_state_stat U
else extract_state_stat U)
}
}
else RETURN (False, empty_init_code)
}›
definition empty_conflict_code' :: ‹(bool × _ list × stats) nres› where
‹empty_conflict_code' = do{
let M0 = [];
RETURN (False, M0, (0, 0, 0, 0, 0, 0, 0,
0))}›
lemma IsaSAT_bounded_heur_alt_def:
‹IsaSAT_bounded_heur opts CS = do{
ASSERT(isasat_input_bounded (mset_set (extract_atms_clss CS {})));
ASSERT(∀C∈set CS. ∀L∈set C. nat_of_lit L ≤ uint32_max);
let 𝒜⇩i⇩n' = mset_set (extract_atms_clss CS {});
ASSERT(isasat_input_bounded 𝒜⇩i⇩n');
ASSERT(distinct_mset 𝒜⇩i⇩n');
S ← init_state_wl_heur 𝒜⇩i⇩n';
(T::twl_st_wl_heur_init) ← init_dt_wl_heur False CS S;
failed ← RETURN ((isasat_fast_init T ∧ ¬is_failed_heur_init T));
if ¬failed
then do {
RETURN (False, empty_init_code)
} else do {
let T = convert_state 𝒜⇩i⇩n' T;
if ¬get_conflict_wl_is_None_heur_init T
then RETURN (True, empty_init_code)
else if CS = [] then do {stat ← empty_conflict_code; RETURN (True, stat)}
else do {
ASSERT(𝒜⇩i⇩n' ≠ {#});
ASSERT(isasat_input_bounded_nempty 𝒜⇩i⇩n');
ASSERT((λ(M', N', D', Q', W', ((ns, m, fst_As, lst_As, next_search), to_remove), φ, clvls). fst_As ≠ None ∧
lst_As ≠ None) T);
ASSERT(rewatch_heur_st_fast_pre T);
T ← rewatch_heur_st_fast T;
ASSERT(isasat_fast_init T);
T ← finalise_init_code opts (T::twl_st_wl_heur_init);
ASSERT(isasat_fast T);
(b, U) ← cdcl_twl_stgy_restart_prog_bounded_wl_heur T;
RETURN (b, if b ∧ get_conflict_wl_is_None_heur U then extract_model_of_state_stat U
else extract_state_stat U)
}
}
}›
unfolding Let_def IsaSAT_bounded_heur_def init_state_wl_heur_fast_def
bind_to_let_conv isasat_information_banner_def virtual_copy_def
id_apply
unfolding
convert_state_def de_Morgan_disj not_not if_not_swap
by (intro bind_cong[OF refl] if_cong[OF refl] refl)
lemma IsaSAT_heur_bounded_IsaSAT_bounded:
‹IsaSAT_bounded_heur b CS ≤ ⇓(bool_rel ×⇩f model_stat_rel) (IsaSAT_bounded CS)›
proof -
have init_dt_wl_heur: ‹init_dt_wl_heur True CS S ≤
⇓(twl_st_heur_parsing_no_WL 𝒜 True O {(S, T). S = remove_watched T ∧
get_watched_wl (fst T) = (λ_. [])})
(init_dt_wl' CS T)›
if
‹case (CS, T) of
(CS, S) ⇒
(∀C∈set CS. literals_are_in_ℒ⇩i⇩n 𝒜 (mset C)) ∧
distinct_mset_set (mset ` set CS)› and
‹((CS, S), CS, T) ∈ ⟨Id⟩list_rel ×⇩f twl_st_heur_parsing_no_WL 𝒜 True›
for 𝒜 CS T S
proof -
show ?thesis
apply (rule init_dt_wl_heur_init_dt_wl[THEN fref_to_Down_curry, of 𝒜 CS T CS S,
THEN order_trans])
apply (rule that(1))
apply (rule that(2))
apply (cases ‹init_dt_wl CS T›)
apply (force simp: init_dt_wl'_def RES_RETURN_RES conc_fun_RES
Image_iff)+
done
qed
have init_dt_wl_heur_b: ‹init_dt_wl_heur False CS S ≤
⇓(twl_st_heur_parsing_no_WL 𝒜 False O {(S, T). S = remove_watched T ∧
get_watched_wl (fst T) = (λ_. [])})
(init_dt_wl' CS T)›
if
‹case (CS, T) of
(CS, S) ⇒
(∀C∈set CS. literals_are_in_ℒ⇩i⇩n 𝒜 (mset C)) ∧
distinct_mset_set (mset ` set CS)› and
‹((CS, S), CS, T) ∈ ⟨Id⟩list_rel ×⇩f twl_st_heur_parsing_no_WL 𝒜 True›
for 𝒜 CS T S
proof -
show ?thesis
apply (rule init_dt_wl_heur_init_dt_wl[THEN fref_to_Down_curry, of 𝒜 CS T CS S,
THEN order_trans])
apply (rule that(1))
using that(2) apply (force simp: twl_st_heur_parsing_no_WL_def)
apply (cases ‹init_dt_wl CS T›)
apply (force simp: init_dt_wl'_def RES_RETURN_RES conc_fun_RES
Image_iff)+
done
qed
have virtual_copy: ‹(virtual_copy 𝒜, ()) ∈ {(ℬ, c). c = () ∧ ℬ = 𝒜}› for ℬ 𝒜
by (auto simp: virtual_copy_def)
have input_le: ‹∀C∈set CS. ∀L∈set C. nat_of_lit L ≤ uint32_max›
if ‹isasat_input_bounded (mset_set (extract_atms_clss CS {}))›
proof (intro ballI)
fix C L
assume ‹C ∈ set CS› and ‹L ∈ set C›
then have ‹L ∈# ℒ⇩a⇩l⇩l (mset_set (extract_atms_clss CS {}))›
by (auto simp: extract_atms_clss_alt_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n)
then show ‹nat_of_lit L ≤ uint32_max›
using that by auto
qed
have lits_C: ‹literals_are_in_ℒ⇩i⇩n (mset_set (extract_atms_clss CS {})) (mset C)›
if ‹C ∈ set CS› for C CS
using that
by (force simp: literals_are_in_ℒ⇩i⇩n_def in_ℒ⇩a⇩l⇩l_atm_of_𝒜⇩i⇩n
in_all_lits_of_m_ain_atms_of_iff extract_atms_clss_alt_def
atm_of_eq_atm_of)
have init_state_wl_heur: ‹isasat_input_bounded 𝒜 ⟹
init_state_wl_heur 𝒜 ≤ SPEC (λc. (c, init_state_wl) ∈
{(S, S'). (S, S') ∈ twl_st_heur_parsing_no_WL_wl 𝒜 True ∧
inres (init_state_wl_heur 𝒜) S})› for 𝒜
by (rule init_state_wl_heur_init_state_wl[THEN fref_to_Down_unRET_uncurry0_SPEC,
of 𝒜, THEN strengthen_SPEC, THEN order_trans])
auto
have get_conflict_wl_is_None_heur_init: ‹ (Tb, Tc)
∈ ({(S,T). (S, T) ∈ twl_st_heur_parsing (mset_set (extract_atms_clss CS {})) True ∧
get_clauses_wl_heur_init S = get_clauses_wl_heur_init U ∧
get_conflict_wl_heur_init S = get_conflict_wl_heur_init U ∧
get_clauses_wl (fst T) = get_clauses_wl (fst V) ∧
get_conflict_wl (fst T) = get_conflict_wl (fst V) ∧
get_unit_clauses_wl (fst T) = get_unit_clauses_wl (fst V)} O {(S, T). S = (T, {#})}) ⟹
(¬ get_conflict_wl_is_None_heur_init Tb) = (get_conflict_wl Tc ≠ None)› for Tb Tc U V
by (cases V) (auto simp: twl_st_heur_parsing_def Collect_eq_comp'
get_conflict_wl_is_None_heur_init_def
option_lookup_clause_rel_def)
have get_conflict_wl_is_None_heur_init3: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) False O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])} ⟹
(¬ get_conflict_wl_is_None_heur_init T) = (get_conflict_wl (fst Ta) ≠ None)› for T Ta failed faileda
by (cases T; cases Ta) (auto simp: twl_st_heur_parsing_no_WL_def
get_conflict_wl_is_None_heur_init_def
option_lookup_clause_rel_def)
have finalise_init_nempty: ‹x1i ≠ None› ‹x1j ≠ None›
if
T: ‹(Tb, Tc)
∈ ({(S,T). (S, T) ∈ twl_st_heur_parsing (mset_set (extract_atms_clss CS {})) True ∧
get_clauses_wl_heur_init S = get_clauses_wl_heur_init U ∧
get_conflict_wl_heur_init S = get_conflict_wl_heur_init U ∧
get_clauses_wl (fst T) = get_clauses_wl (fst V) ∧
get_conflict_wl (fst T) = get_conflict_wl (fst V) ∧
get_unit_clauses_wl (fst T) = get_unit_clauses_wl (fst V)} O {(S, T). S = (T, {#})})› and
nempty: ‹extract_atms_clss CS {} ≠ {}› and
st:
‹x2g = (x1j, x2h)›
‹x2f = (x1i, x2g)›
‹x2e = (x1h, x2f)›
‹x1f = (x1g, x2e)›
‹x1e = (x1f, x2i)›
‹x2j = (x1k, x2k)›
‹x2d = (x1e, x2j)›
‹x2c = (x1d, x2d)›
‹x2b = (x1c, x2c)›
‹x2a = (x1b, x2b)›
‹x2 = (x1a, x2a)› and
conv: ‹convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) Tb =
(x1, x2)›
for ba S T Ta Tb Tc uu x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x1f
x1g x2e x1h x2f x1i x2g x1j x2h x2i x2j x1k x2k U V
proof -
show ‹x1i ≠ None›
using T conv nempty
unfolding st
by (cases x1i)
(auto simp: convert_state_def twl_st_heur_parsing_def
isa_vmtf_init_def vmtf_init_def mset_set_empty_iff)
show ‹x1j ≠ None›
using T conv nempty
unfolding st
by (cases x1i)
(auto simp: convert_state_def twl_st_heur_parsing_def
isa_vmtf_init_def vmtf_init_def mset_set_empty_iff)
qed
have banner: ‹isasat_information_banner
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) Tb)
≤ SPEC (λc. (c, ()) ∈ {(_, _). True})› for Tb
by (auto simp: isasat_information_banner_def)
let ?TT = ‹rewatch_heur_st_rewatch_st_rel CS›
have finalise_init_code: ‹finalise_init_code b
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) Tb)
≤ SPEC (λc. (c, finalise_init Tc) ∈ twl_st_heur)› (is ?A) and
finalise_init_code3: ‹finalise_init_code b Tb
≤ SPEC (λc. (c, finalise_init Tc) ∈ twl_st_heur)› (is ?B)
if
T: ‹(Tb, Tc) ∈ ?TT U V› and
confl: ‹¬ get_conflict_wl Tc ≠ None› and
nempty: ‹extract_atms_clss CS {} ≠ {}› and
clss_CS: ‹mset `# ran_mf (get_clauses_wl Tc) + get_unit_clauses_wl Tc + get_subsumed_clauses_wl Tc =
mset `# mset CS› and
learned: ‹learned_clss_l (get_clauses_wl Tc) = {#}›
for ba S T Ta Tb Tc u v U V
proof -
have 1: ‹get_conflict_wl Tc = None›
using confl by auto
have 2: ‹all_atms_st Tc ≠ {#}›
using nempty unfolding all_atms_def all_lits_alt_def clss_CS[unfolded add.assoc]
by (auto simp: extract_atms_clss_alt_def
all_lits_of_mm_empty_iff)
have 3: ‹set_mset (all_atms_st Tc) = set_mset (mset_set (extract_atms_clss CS {}))›
using nempty unfolding all_atms_def all_lits_alt_def clss_CS[unfolded add.assoc]
apply (auto simp: extract_atms_clss_alt_def
all_lits_of_mm_empty_iff in_all_lits_of_mm_ain_atms_of_iff atms_of_ms_def)
by (metis (no_types, lifting) UN_iff atm_of_all_lits_of_mm(2) atm_of_lit_in_atms_of
atms_of_mmltiset atms_of_ms_mset_unfold in_set_mset_eq_in set_image_mset)
have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x
by auto
have H': ‹A = B ⟹ A x ⟹ B x› for A B x
by auto
note cong = trail_pol_cong heuristic_rel_cong
option_lookup_clause_rel_cong isa_vmtf_init_cong
vdom_m_cong[THEN H] isasat_input_nempty_cong[THEN iffD1]
isasat_input_bounded_cong[THEN iffD1]
cach_refinement_empty_cong[THEN H']
phase_saving_cong[THEN H']
ℒ⇩a⇩l⇩l_cong[THEN H]
D⇩0_cong[THEN H]
have 4: ‹(convert_state (mset_set (extract_atms_clss CS {})) Tb, Tc)
∈ twl_st_heur_post_parsing_wl True›
using T nempty
by (auto simp: twl_st_heur_parsing_def twl_st_heur_post_parsing_wl_def
convert_state_def eq_commute[of ‹mset _› ‹dom_m _›]
vdom_m_cong[OF 3[symmetric]] ℒ⇩a⇩l⇩l_cong[OF 3[symmetric]]
dest!: cong[OF 3[symmetric]])
(simp_all add: add.assoc ℒ⇩a⇩l⇩l_all_atms_all_lits
flip: all_lits_def all_lits_alt_def2 all_lits_alt_def)
show ?A
by (rule finalise_init_finalise_init[THEN fref_to_Down_unRET_curry_SPEC, of b])
(use 1 2 learned 4 in auto)
then show ?B unfolding convert_state_def by auto
qed
have get_conflict_wl_is_None_heur_init2: ‹(U, V)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])} ⟹
(¬ get_conflict_wl_is_None_heur_init
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) U)) =
(get_conflict_wl (from_init_state V) ≠ None)› for U V
by (auto simp: twl_st_heur_parsing_def Collect_eq_comp'
get_conflict_wl_is_None_heur_init_def twl_st_heur_parsing_no_WL_def
option_lookup_clause_rel_def convert_state_def from_init_state_def)
have finalise_init2: ‹x1i ≠ None› ‹x1j ≠ None›
if
T: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) b O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}› and
nempty: ‹extract_atms_clss CS {} ≠ {}› and
st:
‹x2g = (x1j, x2h)›
‹x2f = (x1i, x2g)›
‹x2e = (x1h, x2f)›
‹x1f = (x1g, x2e)›
‹x1e = (x1f, x2i)›
‹x2j = (x1k, x2k)›
‹x2d = (x1e, x2j)›
‹x2c = (x1d, x2d)›
‹x2b = (x1c, x2c)›
‹x2a = (x1b, x2b)›
‹x2 = (x1a, x2a)› and
conv: ‹convert_state ((mset_set (extract_atms_clss CS {}))) T =
(x1, x2)›
for uu ba S T Ta baa uua uub x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x1f
x1g x2e x1h x2f x1i x2g x1j x2h x2i x2j x1k x2k b
proof -
show ‹x1i ≠ None›
using T conv nempty
unfolding st
by (cases x1i)
(auto simp: convert_state_def twl_st_heur_parsing_def
twl_st_heur_parsing_no_WL_def
isa_vmtf_init_def vmtf_init_def mset_set_empty_iff)
show ‹x1j ≠ None›
using T conv nempty
unfolding st
by (cases x1i)
(auto simp: convert_state_def twl_st_heur_parsing_def
twl_st_heur_parsing_no_WL_def
isa_vmtf_init_def vmtf_init_def mset_set_empty_iff)
qed
have rewatch_heur_st_fast_pre: ‹rewatch_heur_st_fast_pre
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) T)›
if
T: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}› and
length_le: ‹¬¬isasat_fast_init (convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) T)›
for uu ba S T Ta baa uua uub
proof -
have ‹valid_arena (get_clauses_wl_heur_init T) (get_clauses_wl (fst Ta))
(set (get_vdom_heur_init T))›
using T by (auto simp: twl_st_heur_parsing_no_WL_def)
then show ?thesis
using length_le unfolding rewatch_heur_st_fast_pre_def convert_state_def
isasat_fast_init_def uint64_max_def uint32_max_def
by (auto dest: valid_arena_in_vdom_le_arena)
qed
have rewatch_heur_st_fast_pre2: ‹rewatch_heur_st_fast_pre
(convert_state (mset_set (extract_atms_clss CS {})) T)›
if
T: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) False O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}› and
length_le: ‹¬¬isasat_fast_init (convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) T)› and
failed: ‹¬is_failed_heur_init T›
for uu ba S T Ta baa uua uub
proof -
have
Ta: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}›
using failed T by (cases T; cases Ta) (fastforce simp: twl_st_heur_parsing_no_WL_def)
from rewatch_heur_st_fast_pre[OF this length_le]
show ?thesis by simp
qed
have finalise_init_code2: ‹finalise_init_code b Tb
≤ SPEC (λc. (c, finalise_init Tc) ∈ {(S', T').
(S', T') ∈ twl_st_heur ∧
get_clauses_wl_heur_init Tb = get_clauses_wl_heur S'})›
if
Ta: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) False O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}› and
confl: ‹¬ get_conflict_wl (from_init_state Ta) ≠ None› and
‹CS ≠ []› and
nempty: ‹extract_atms_clss CS {} ≠ {}› and
‹isasat_input_bounded_nempty (mset_set (extract_atms_clss CS {}))› and
clss_CS: ‹mset `# ran_mf (get_clauses_wl (from_init_state Ta)) +
get_unit_clauses_wl (from_init_state Ta) + get_subsumed_clauses_wl (from_init_state Ta) =
mset `# mset CS› and
learned: ‹learned_clss_l (get_clauses_wl (from_init_state Ta)) = {#}› and
‹virtual_copy (mset_set (extract_atms_clss CS {})) ≠ {#}› and
‹isasat_input_bounded_nempty
(virtual_copy (mset_set (extract_atms_clss CS {})))› and
‹case convert_state (virtual_copy (mset_set (extract_atms_clss CS {}))) T of
(M', N', D', Q', W', xa, xb) ⇒
(case xa of
(x, xa) ⇒
(case x of
(ns, m, fst_As, lst_As, next_search) ⇒
λto_remove (φ, clvls). fst_As ≠ None ∧ lst_As ≠ None)
xa)
xb› and
T: ‹(Tb, Tc) ∈ ?TT T Ta› and
failed: ‹¬is_failed_heur_init T›
for uu ba S T Ta baa uua uub V W b Tb Tc
proof -
have
Ta: ‹(T, Ta)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True O
{(S, T). S = remove_watched T ∧ get_watched_wl (fst T) = (λ_. [])}›
using failed Ta by (cases T; cases Ta) (fastforce simp: twl_st_heur_parsing_no_WL_def)
have 1: ‹get_conflict_wl Tc = None›
using confl T by (auto simp: from_init_state_def)
have Ta_Tc: ‹all_atms_st Tc = all_atms_st (from_init_state Ta)›
using T Ta
unfolding all_lits_alt_def mem_Collect_eq prod.case relcomp.simps
all_atms_def add.assoc apply -
apply normalize_goal+
by (auto simp flip: all_atms_def[symmetric] simp: all_lits_def
twl_st_heur_parsing_no_WL_def twl_st_heur_parsing_def
from_init_state_def)
moreover have 3: ‹set_mset (all_atms_st (from_init_state Ta)) = set_mset (mset_set (extract_atms_clss CS {}))›
unfolding all_lits_alt_def mem_Collect_eq prod.case relcomp.simps
all_atms_def clss_CS[unfolded add.assoc] apply -
by (auto simp: extract_atms_clss_alt_def
atm_of_all_lits_of_mm atms_of_ms_def)
ultimately have 2: ‹all_atms_st Tc ≠ {#}›
using nempty
by auto
have H: ‹A = B ⟹ x ∈ A ⟹ x ∈ B› for A B x
by auto
have H': ‹A = B ⟹ A x ⟹ B x› for A B x
by auto
note cong = trail_pol_cong heuristic_rel_cong
option_lookup_clause_rel_cong isa_vmtf_init_cong
vdom_m_cong[THEN H] isasat_input_nempty_cong[THEN iffD1]
isasat_input_bounded_cong[THEN iffD1]
cach_refinement_empty_cong[THEN H']
phase_saving_cong[THEN H']
ℒ⇩a⇩l⇩l_cong[THEN H]
D⇩0_cong[THEN H]
have 4: ‹(convert_state (mset_set (extract_atms_clss CS {})) Tb, Tc)
∈ twl_st_heur_post_parsing_wl True›
using T nempty
by (auto simp: twl_st_heur_parsing_def twl_st_heur_post_parsing_wl_def
convert_state_def eq_commute[of ‹mset _› ‹dom_m _›] from_init_state_def
vdom_m_cong[OF 3[symmetric]] ℒ⇩a⇩l⇩l_cong[OF 3[symmetric]]
dest!: cong[OF 3[symmetric]])
(simp_all add: add.assoc ℒ⇩a⇩l⇩l_all_atms_all_lits
flip: all_lits_def all_lits_alt_def2 all_lits_alt_def)
show ?thesis
apply (rule finalise_init_finalise_init_full[unfolded conc_fun_RETURN,
THEN order_trans])
by (use 1 2 learned 4 T in ‹auto simp: from_init_state_def convert_state_def›)
qed
have isasat_fast: ‹isasat_fast Td›
if
fast: ‹¬ ¬ isasat_fast_init
(convert_state (virtual_copy (mset_set (extract_atms_clss CS {})))
T)› and
Tb: ‹(Tb, Tc) ∈ ?TT T Ta› and
Td: ‹(Td, Te)
∈ {(S', T').
(S', T') ∈ twl_st_heur ∧
get_clauses_wl_heur_init Tb = get_clauses_wl_heur S'}›
for uu ba S T Ta baa uua uub Tb Tc Td Te
proof -
show ?thesis
using fast Td Tb
by (auto simp: convert_state_def isasat_fast_init_def sint64_max_def
uint32_max_def uint64_max_def isasat_fast_def)
qed
define init_succesfull where ‹init_succesfull T = RETURN ((isasat_fast_init T ∧ ¬ is_failed_heur_init T))› for T
define init_succesfull2 where ‹init_succesfull2 = SPEC (λ_ :: bool. True)›
have [refine]: ‹init_succesfull T ≤ ⇓ {(b, b'). (b = b') ∧ (b ⟷ (isasat_fast_init T ∧ ¬ is_failed_heur_init T))}
init_succesfull2› for T
by (auto simp: init_succesfull_def init_succesfull2_def intro!: RETURN_RES_refine)
show ?thesis
supply [[goals_limit=1]]
unfolding IsaSAT_bounded_heur_alt_def IsaSAT_bounded_alt_def init_succesfull_def[symmetric]
apply (rewrite at ‹do {_ ← init_dt_wl' _ _; _ ← (⌑ :: bool nres); If _ _ _ }› init_succesfull2_def[symmetric])
apply (refine_vcg virtual_copy init_state_wl_heur banner)
subgoal by (rule input_le)
subgoal by (rule distinct_mset_mset_set)
apply (rule init_dt_wl_heur_b[of ‹mset_set (extract_atms_clss CS {})›])
subgoal by (auto simp: lits_C)
subgoal by(auto simp: twl_st_heur_parsing_no_WL_wl_def
twl_st_heur_parsing_no_WL_def to_init_state_def
init_state_wl_def init_state_wl_heur_def
inres_def RES_RES_RETURN_RES
RES_RETURN_RES)
subgoal by auto
subgoal by (simp add: empty_conflict_code_def model_stat_rel_def
empty_init_code_def)
subgoal unfolding from_init_state_def convert_state_def
by (rule get_conflict_wl_is_None_heur_init3)
subgoal by (simp add: empty_init_code_def model_stat_rel_def)
subgoal by simp
subgoal by (simp add: empty_conflict_code_def model_stat_rel_def)
subgoal by (simp add: mset_set_empty_iff extract_atms_clss_alt_def)
subgoal by (rule finalise_init2)
subgoal by (rule finalise_init2)
subgoal for uu ba S T Ta baa
by (rule rewatch_heur_st_fast_pre2; assumption?)
(clarsimp_all simp add: convert_state_def)
apply (rule rewatch_heur_st_rewatch_st3[unfolded virtual_copy_def id_apply]; assumption?)
subgoal by auto
subgoal by (clarsimp simp add: isasat_fast_init_def convert_state_def)
apply (rule finalise_init_code2; assumption?)
subgoal by clarsimp
subgoal by (clarsimp simp add: isasat_fast_def isasat_fast_init_def convert_state_def)
subgoal by (clarsimp simp add: isasat_fast_def isasat_fast_init_def convert_state_def)
subgoal by clarsimp
subgoal by (clarsimp simp add: isasat_fast_def isasat_fast_init_def convert_state_def)
apply (rule_tac r1 = ‹length (get_clauses_wl_heur Td)› in
cdcl_twl_stgy_restart_prog_bounded_wl_heur_cdcl_twl_stgy_restart_prog_bounded_wl_D[THEN fref_to_Down])
subgoal by (simp add: isasat_fast_def sint64_max_def uint32_max_def
uint64_max_def)
subgoal by fast
subgoal by simp
subgoal premises p
using p(28-)
by (auto simp: twl_st_heur_def get_conflict_wl_is_None_heur_def
extract_stats_def extract_state_stat_def
option_lookup_clause_rel_def trail_pol_def
extract_model_of_state_def rev_map
extract_model_of_state_stat_def model_stat_rel_def
dest!: ann_lits_split_reasons_map_lit_of)
done
qed
lemma ISASAT_bounded_SAT_l_bounded':
assumes ‹Multiset.Ball (mset `# mset CS) distinct_mset› and
‹isasat_input_bounded (mset_set (⋃C∈set CS. atm_of ` set C))›
shows ‹IsaSAT_bounded CS ≤ ⇓ {((b, S), (b', S')). b = b' ∧ (b ⟶ S = S')} (SAT_l_bounded' CS)›
unfolding IsaSAT_bounded_def SAT_l_bounded'_def
apply refine_vcg
apply (rule SAT_wl_bounded_SAT_l_bounded)
subgoal using assms by auto
subgoal using assms by auto
subgoal by (auto simp: extract_model_of_state_def)
done
lemma IsaSAT_bounded_heur_model_if_sat:
assumes ‹∀C ∈# mset `# mset CS. distinct_mset C› and
‹isasat_input_bounded (mset_set (⋃C∈set CS. atm_of ` set C))›
shows ‹IsaSAT_bounded_heur opts CS ≤ ⇓ {((b, m), (b', m')). b=b' ∧ (b ⟶ (m,m') ∈ model_stat_rel)}
(model_if_satisfiable_bounded (mset `# mset CS))›
apply (rule IsaSAT_heur_bounded_IsaSAT_bounded[THEN order_trans])
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule ISASAT_bounded_SAT_l_bounded')
subgoal using assms by auto
subgoal using assms by auto
unfolding conc_fun_chain
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule SAT_l_bounded'_SAT0_bounded')
subgoal using assms by auto
unfolding conc_fun_chain
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule SAT0_bounded'_SAT_bounded')
subgoal using assms by auto
unfolding conc_fun_chain
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule SAT_bounded_model_if_satisfiable[THEN fref_to_Down, of ‹mset `# mset CS›])
subgoal using assms by auto
subgoal using assms by auto
unfolding conc_fun_chain
apply (rule conc_fun_R_mono)
apply standard
apply (clarsimp simp: model_stat_rel_def)
done
lemma IsaSAT_bounded_heur_model_if_sat':
‹(uncurry IsaSAT_bounded_heur, uncurry (λ_. model_if_satisfiable_bounded)) ∈
[λ(_, CS). (∀C ∈# CS. distinct_mset C) ∧
(∀C∈#CS. ∀L∈#C. nat_of_lit L ≤ uint32_max)]⇩f
Id ×⇩r list_mset_rel O ⟨list_mset_rel⟩mset_rel → ⟨{((b, m), (b', m')). b=b' ∧ (b ⟶ (m,m') ∈ model_stat_rel)}⟩nres_rel›
proof -
have H: ‹isasat_input_bounded (mset_set (⋃C∈set CS. atm_of ` set C))›
if CS_p: ‹∀C∈#CS'. ∀L∈#C. nat_of_lit L ≤ uint32_max› and
‹(CS, CS') ∈ list_mset_rel O ⟨list_mset_rel⟩mset_rel›
for CS CS'
unfolding isasat_input_bounded_def
proof
fix L
assume L: ‹L ∈# ℒ⇩a⇩l⇩l (mset_set (⋃C∈set CS. atm_of ` set C))›
then obtain C where
L: ‹C∈set CS ∧ (L ∈set C ∨ - L ∈ set C)›
apply (cases L)
apply (auto simp: extract_atms_clss_alt_def uint32_max_def
ℒ⇩a⇩l⇩l_def)+
apply (metis literal.exhaust_sel)+
done
have ‹nat_of_lit L ≤ uint32_max ∨ nat_of_lit (-L) ≤ uint32_max›
using L CS_p that by (auto simp: list_mset_rel_def mset_rel_def br_def
br_def mset_rel_def p2rel_def rel_mset_def
rel2p_def[abs_def] list_all2_op_eq_map_right_iff')
then show ‹nat_of_lit L ≤ uint32_max›
using L
by (cases L) (auto simp: extract_atms_clss_alt_def uint32_max_def)
qed
show ?thesis
apply (intro frefI nres_relI)
unfolding uncurry_def
apply clarify
subgoal for o1 o2 o3 CS o1' o2' o3' CS'
apply (rule IsaSAT_bounded_heur_model_if_sat[THEN order_trans, of CS _ ‹(o1, o2, o3)›])
subgoal by (auto simp: list_mset_rel_def mset_rel_def br_def
br_def mset_rel_def p2rel_def rel_mset_def
rel2p_def[abs_def] list_all2_op_eq_map_right_iff')
subgoal by (rule H) auto
apply (auto simp: list_mset_rel_def mset_rel_def br_def
br_def mset_rel_def p2rel_def rel_mset_def
rel2p_def[abs_def] list_all2_op_eq_map_right_iff')
done
done
qed
end