Theory IsaSAT
theory IsaSAT
imports IsaSAT_CDCL IsaSAT_Restart_Simp IsaSAT_Initialisation
IsaSAT_Defs
begin
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›.
›
abbreviation conclusive_TWL_run_bounded where
‹conclusive_TWL_run_bounded S ≡ partial_conclusive_TWL_run S›
text ‹
Before introducing the pragmatic CDCL version, we expressed the specification all the level
up to Weidenbach's CDCL, but now we stop at the pragmatic CDCL. Technically, we could actually
skip the part on the calculus and simply use the conclusive part (no conflict and model,
conflict and unsat), but this version is nicer on paper to highlight the refinement approach.
›
definition conclusive_CDCL_state :: ‹'v clauses ⇒ 'v prag_st ⇒ 'v prag_st ⇒ bool› where
‹conclusive_CDCL_state CS T U ⟷
(pget_conflict U = None ⟶ (consistent_interp (lits_of_l (pget_trail U)) ∧
pget_trail U ⊨as (set_mset CS))) ∧
(pget_conflict U ≠ None ⟶ (CS ≠ {#} ∧ count_decided (pget_trail U) = 0 ∧
unsatisfiable (set_mset CS)))›
lemmas cdcl_twl_stgy_restart_restart_prog_spec = cdcl_twl_stgy_restart_prog_spec
lemmas cdcl_twl_stgy_restart_prog_bounded_spec = cdcl_twl_stgy_prog_bounded_spec
lemma rtranclp_pcdcl_satisfiable_iff:
assumes
‹pcdcl⇧*⇧* S T› and
‹pcdcl_all_struct_invs S› and
ent_init: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state_of S)›
shows
‹satisfiable (set_mset (pget_all_init_clss S)) ⟷ satisfiable (set_mset (pget_all_init_clss T))›
using assms
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal
by (auto dest!: pcdcl_satisfiable_iff intro: rtranclp_pcdcl_all_struct_invs
Pragmatic_CDCL.rtranclp_pcdcl_entailed_by_init)
done
lemma pcdcl_stgy_restart_satisfiable_iff:
‹pcdcl_stgy_restart (R1, R2, S, m, n, g) (R1', R2', T, m', n', g') ⟹
pcdcl_all_struct_invs S ⟹ cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state_of S) ⟹
satisfiable (set_mset (pget_all_init_clss T)) ⟷ satisfiable (set_mset (pget_all_init_clss S))›
apply (induction ‹(R1, R2, S, m, n, g)› ‹(R1', R2', T, m', n', g')› rule: pcdcl_stgy_restart.induct)
apply (auto dest: pcdcl_restart_only_entailed_iff pcdcl_restart_entailed_iff
dest: rtranclp_pcdcl_stgy_pcdcl pcdcl_tcore_stgy_pcdcl_stgy'
rtranclp_pcdcl_stgy_pcdcl rtranclp_pcdcl_satisfiable_iff)[]
apply (meson rtranclp_pcdcl_inprocessing_satisfiable_iff rtranclp_pcdcl_restart_inprocessing rtranclp_pcdcl_stgy_pcdcl rtranclp_trans)
apply (meson satisfiable_carac true_cls_mset_true_clss_iff(2) twl_restart_ops.pcdcl_restart_only_entailed_iff)
by simp
lemma rtranclp_pcdcl_restart_satisfiable_iff:
‹pcdcl_stgy_restart⇧*⇧* (R1, R2, S, m, n, g) (R1', R2', T, m', n', g') ⟹
pcdcl_all_struct_invs S ⟹ cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state_of S) ⟹
satisfiable (set_mset (pget_all_init_clss T)) ⟷ satisfiable (set_mset (pget_all_init_clss S))›
apply (induction rule: rtranclp_induct[of r ‹(_, _, _, _, _, _)› ‹(_, _, _, _, _, _)›, split_format(complete), of for r])
subgoal by auto
subgoal for T U
by (simp add: pcdcl_stgy_restart_satisfiable_iff pcdcl_stgy_restart_same_init_vars
rtranclp_pcdcl_stgy_restart_entailed_by_init rtranclp_pcdcl_stgy_restart_pcdcl_all_struct_invs)
done
fun pinit_state :: ‹'v clauses ⇒ 'v prag_st› where
‹pinit_state N = ([], N, {#}, None, {#}, {#}, {#}, {#}, {#}, {#})›
lemma get_all_clss_alt_def:
‹get_all_clss S = get_all_init_clss S + get_all_learned_clss S›
by (cases S) (auto simp: ac_simps clauses_def)
lemma conclusive_TWL_run_conclusive_CDCL_state:
assumes
struct: ‹twl_struct_invs S› and
stgy: ‹twl_stgy_invs S› and
init: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state⇩W_of S)›
shows ‹conclusive_TWL_run S
≤ ⇓ (br pstate⇩W_of (λ_. True))
(SPEC
(conclusive_CDCL_state (get_all_init_clss S) (pstate⇩W_of S)))›
unfolding conclusive_TWL_run_def
proof (rule RES_refine)
fix s
assume ‹s ∈ {Ta.
∃T0 T0' n' m⇩0 n⇩0.
cdcl_twl_stgy_restart⇧*⇧* (S, S, S, m⇩0, n⇩0, True) (T0, T0', Ta, n') ∧
final_twl_state Ta}›
then obtain T0 T0' m' n' f' m⇩0 n⇩0 where
st: ‹cdcl_twl_stgy_restart⇧*⇧* (S, S, S, m⇩0, n⇩0, True) (T0, T0', s, m', n', f')› and
final: ‹final_twl_state s›
by fast
have pcdcl_invs: ‹pcdcl_all_struct_invs (pstate⇩W_of S)›
using struct unfolding twl_struct_invs_def by auto
from rtranclp_cdcl_twl_stgy_restart_pcdcl[OF st struct struct struct init init init]
have pcdcl: ‹pcdcl_stgy_restart⇧*⇧* (pstate⇩W_of S, pstate⇩W_of S, pstate⇩W_of S, m⇩0, n⇩0, True)
(pstate⇩W_of T0, pstate⇩W_of T0', pstate⇩W_of s, m', n', f')› .
have struct_invs_s: ‹twl_struct_invs s›
using rtranclp_cdcl_twl_stgy_restart_twl_struct_invs[OF st] struct init
by auto
have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (state⇩W_of s)›
using struct_invs_s unfolding twl_struct_invs_def pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
then have atms_eq: ‹atms_of_mm (get_all_clss s) = atms_of_mm (pget_all_init_clss (pstate⇩W_of s))›
unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (cases s) (auto)
have pinvs: ‹pcdcl_all_struct_invs (pstate⇩W_of s)›
using struct_invs_s unfolding twl_struct_invs_def by auto
have stgy_invs_s: ‹twl_stgy_invs s›
using rtranclp_cdcl_twl_stgy_restart_twl_stgy_invs[OF st] stgy struct init
by (auto simp: twl_restart_inv_def pcdcl_stgy_restart_inv_def
twl_struct_invs_def)
have H1: ‹consistent_interp (lits_of_l (get_trail s))›
‹get_trail s ⊨asm get_all_init_clss S›
if confl: ‹get_conflict s = None›
proof -
have ‹no_step cdcl_twl_stgy s›
using confl final unfolding final_twl_state_def
by blast
then have ‹no_step pcdcl_core_stgy (pstate⇩W_of s)›
by (rule no_step_cdcl_twl_stgy_no_step_cdcl⇩W_stgy[OF _ struct_invs_s])
then have nss: ‹no_step cdcl⇩W_restart_mset.cdcl⇩W_stgy (state_of (pstate⇩W_of s))›
by (rule no_step_pcdcl_core_stgy_is_cdcl_stgy)
(use struct_invs_s in ‹auto simp: twl_struct_invs_def pcdcl_all_struct_invs_def›)
show ‹consistent_interp (lits_of_l (get_trail s))›
using struct_invs_s unfolding twl_struct_invs_def pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
moreover {
have nss': ‹no_step cdcl⇩W_restart_mset.cdcl⇩W (state⇩W_of s)›
using nss by (auto dest: cdcl⇩W_restart_mset.cdcl⇩W_Ex_cdcl⇩W_stgy)
have ‹total_over_set (lits_of_l (get_trail s))
(atms_of_mm (pget_all_init_clss (pstate⇩W_of s)))›
using cdcl⇩W_restart_mset.no_step_cdcl⇩W_total[of ‹(state⇩W_of s)›, OF nss']
confl struct_invs_s atms_eq unfolding twl_struct_invs_def pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def total_over_m_def
by auto
}
ultimately show ‹get_trail s ⊨asm get_all_init_clss S›
using struct_invs_s rtranclp_pcdcl_restart_entailed_iff[OF pcdcl, of ‹lits_of_l (get_trail s)›]
cdcl⇩W_restart_mset.cdcl⇩W_stgy_final_state_conclusive2[OF nss] confl init pcdcl_invs
unfolding twl_struct_invs_def pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by (auto simp: get_all_clss_alt_def true_annots_true_cls)
qed
have H2: ‹cdcl⇩W_restart_mset.clauses (state_of (pstate⇩W_of s)) ⊨pm T›
if ‹conflicting (state⇩W_of s) = Some T›
for T
using struct_invs_s that unfolding twl_struct_invs_def pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_def
by auto
then have H3: ‹get_conflict s ≠ None ⟹ get_all_init_clss s ≠ {#}›
using rtranclp_pcdcl_stgy_restart_entailed_by_init[OF pcdcl pcdcl_invs] init
alien
by (force simp: get_all_clss_alt_def cdcl⇩W_restart_mset.no_strange_atm_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def empty_entails_novars_iff)
have H4:
‹unsatisfiable (set_mset (get_all_init_clss S))›
if confl: ‹get_conflict s ≠ None› ‹count_decided (get_trail s) = 0›
proof -
have ‹unsatisfiable (set_mset (init_clss (state⇩W_of s)))›
by (rule conflict_of_level_unsatisfiable[of ‹state⇩W_of s›])
(use confl struct_invs_s init
rtranclp_pcdcl_stgy_restart_entailed_by_init[OF pcdcl pcdcl_invs]
in ‹auto simp: twl_struct_invs_def pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def›)
then show ‹unsatisfiable (set_mset (get_all_init_clss S))›
using rtranclp_pcdcl_restart_satisfiable_iff[OF pcdcl]
rtranclp_pcdcl_stgy_restart_same_init_vars[OF pcdcl] struct_invs_s init pcdcl_invs
by (auto simp: satisfiable_def total_over_m_def twl_struct_invs_def)
qed
have H5: False
if confl: ‹get_conflict s ≠ None› ‹count_decided (get_trail s) ≠ 0›
proof -
have ‹no_step cdcl_twl_stgy s›
using confl final unfolding final_twl_state_def
by auto
then have ‹no_step pcdcl_core_stgy (pstate⇩W_of s)›
by (rule no_step_cdcl_twl_stgy_no_step_cdcl⇩W_stgy[OF _ struct_invs_s])
then have nss: ‹no_step cdcl⇩W_restart_mset.cdcl⇩W_stgy (state_of (pstate⇩W_of s))›
by (rule no_step_pcdcl_core_stgy_is_cdcl_stgy)
(use struct_invs_s in ‹auto simp: twl_struct_invs_def pcdcl_all_struct_invs_def›)
show False
using struct_invs_s rtranclp_pcdcl_restart_entailed_iff[OF pcdcl, of ‹lits_of_l (get_trail s)›]
cdcl⇩W_restart_mset.cdcl⇩W_stgy_final_state_conclusive2[OF nss] confl
stgy_invs_s
unfolding twl_struct_invs_def pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def
by (auto simp: get_all_clss_alt_def true_annots_true_cls)
qed
show ‹∃s'∈Collect (conclusive_CDCL_state (get_all_init_clss S) (pstate⇩W_of S)).
(s, s') ∈ (br pstate⇩W_of (λ_. True))›
apply (rule_tac x = ‹pstate⇩W_of s› in bexI)
apply (solves ‹auto simp: br_def›)
unfolding conclusive_CDCL_state_def mem_Collect_eq
apply (cases ‹count_decided (get_trail s) = 0›)
apply (use H1 H2 H3 H4 H5 in force)+
done
qed
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:
shows ‹init_dt_pre CS (to_init_state_l init_state_l)›
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 prag_st nres› where
‹SAT CS = do{
let T = pinit_state CS;
SPEC (conclusive_CDCL_state 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')) ∧
(remdups_mset `# mset `# mset CS + clause `# (get_init_clauses_init SOC) + other_clauses_init SOC +
get_unit_init_clauses_init SOC + get_init_clauses0_init SOC + get_subsumed_init_clauses_init SOC +
get_init_clauses0_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_init_clauses0_init T') ∧
get_learned_clauses0_init SOC = get_learned_clauses0_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_learned_clauses0_init SOC = get_learned_clauses0_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 + get_all_clauses0 T =
remdups_mset `# 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 + get_all_clauses0 T =
remdups_mset `# 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 + get_all_clauses0 T =
remdups_mset `# mset `# mset CS);
ASSERT(get_learned_clss T = {#});
cdcl_twl_stgy_restart_prog_early T
}
}
}
}›
lemma pget_all_init_clss_pstate⇩W_of_init:
‹pget_all_init_clss (pstate⇩W_of_init T) = get_subsumed_init_clauses_init T +
get_unit_init_clauses_init T+
get_init_clauses0_init T +
other_clauses_init T+
clause `# (get_init_clauses_init T)›
by (cases T) auto
lemma [twl_st_init,simp]:
‹pget_trail (pstate⇩W_of_init T) = get_trail_init T›
‹pget_conflict (pstate⇩W_of_init T) = get_conflict_init T›
‹pget_all_learned_clss (pstate⇩W_of_init T) = clause `# get_learned_clauses_init T+ get_unit_learned_clauses_init T + get_learned_clauses0_init T +
get_subsumed_learned_clauses_init T›
‹get_init_learned_clss (fst T) = get_unit_learned_clauses_init T›
‹subsumed_learned_clauses (fst T) = get_subsumed_learned_clauses_init T›
‹get_learned_clss (fst T) = get_learned_clauses_init T›
‹get_conflict (fst T) = get_conflict_init T›
by (solves ‹cases T; auto›)+
lemma get_all_init_clss_alt_init_def:
‹get_all_init_clss (fst T) = clauses (get_init_clauses_init T) +
get_unit_init_clauses_init T + get_subsumed_init_clauses_init T + get_init_clauses0_init T›
by (cases T) (auto simp: )
lemma satisfiable_remdups_iff:
‹satisfiable ((λx. remdups_mset (mset x)) ` CS) ⟷ satisfiable (mset ` CS)›
by (auto simp flip: satisfiable_carac simp: true_clss_def)
lemma true_annots_remdups_mset:
‹I ⊨as remdups_mset ` C ⟷ I ⊨as C›
by (simp add: true_annot_def true_annots_def)
lemma SAT0_SAT:
shows ‹SAT0 CS ≤ ⇓ {(S, T). T = pstate⇩W_of S} (SAT (mset `# mset CS))›
proof -
have conflict_during_init: ‹RETURN (fst T)
≤ ⇓ {(S, T). T = pstate⇩W_of S}
(SPEC (conclusive_CDCL_state (mset `# mset CS)
(pinit_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 = ‹remdups_mset `# 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: ‹?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_init_clauses0_init (to_init_state0 init_state0) +
get_subsumed_init_clauses_init (to_init_state0 init_state0) +
get_init_clauses0_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 +
get_init_clauses0_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)›
‹get_learned_clauses0_init T =
get_learned_clauses0_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 pcdcl_all_struct_invs_def
state⇩W_of_init.simps[symmetric]
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 pcdcl_all_struct_invs_def
state⇩W_of_init.simps[symmetric]
by fast
have ‹unsatisfiable (set_mset (remdups_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 pcdcl_all_struct_invs_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def ac_simps
twl_st_l_init pget_all_init_clss_pstate⇩W_of_init)
then have unsat[simp]: ‹unsatisfiable (mset ` set CS)›
using satisfiable_remdups_iff[of ‹set CS›]
by auto
then have [simp]: ‹CS ≠ []›
by (auto simp del: unsat)
show ?thesis
unfolding conclusive_CDCL_state_def
apply (rule RETURN_SPEC_refine)
apply (rule exI[of _ ‹pstate⇩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)
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 (fst init_state0)
≤ ⇓ {(S, T). T = pstate⇩W_of S}
(SPEC
(conclusive_CDCL_state (mset `# mset CS)
(pinit_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)
(use that in ‹auto simp: conclusive_CDCL_state_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 = pstate⇩W_of S}
(SPEC
(conclusive_CDCL_state (mset `# mset CS)
(pinit_state (mset `# mset CS))))› (is ?G1) and
cdcl_twl_stgy_restart_prog_early: ‹cdcl_twl_stgy_restart_prog_early (fst T)
≤ ⇓ {(S, T). T = pstate⇩W_of S}
(SPEC
(conclusive_CDCL_state (mset `# mset CS)
(pinit_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) + get_all_clauses0 (fst T) =
remdups_mset `# mset `# mset CS› and
‹get_learned_clss (fst T) = {#}›
for T
proof -
let ?CS = ‹remdups_mset `# 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: ‹?CS +
clauses (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_init_clauses0_init (to_init_state0 init_state0) +
get_subsumed_init_clauses_init (to_init_state0 init_state0) +
get_init_clauses0_init (to_init_state0 init_state0) =
clauses (get_init_clauses_init T) + other_clauses_init T +
get_unit_init_clauses_init T +
get_subsumed_init_clauses_init T +
get_init_clauses0_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)›
‹get_learned_clauses0_init T =
get_learned_clauses0_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 init: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (state_of (pstate⇩W_of (fst T)))›
using learned
apply (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
get_all_learned_clss_alt_def init_state0_def to_init_state0_def)
by (smt add.right_neutral get_learned_clauses0.elims get_learned_clauses0_init.simps
get_unit_learned_clauses_init.elims prod.sel(1) set_mset_union union_trus_clss_clss)
have CS': ‹(λx. remdups_mset (mset x)) ` set CS = clause ` set_mset (get_init_clauses_init T) ∪ set_mset (get_unit_init_clauses_init T) ∪
set_mset (get_subsumed_init_clauses_init T) ∪ set_mset (get_init_clauses0_init T)›
using arg_cong[OF clss, of set_mset] oth confl
by (cases ‹other_clauses_init T = {#}›)
(auto 5 3 simp: init_state0_def to_init_state0_def)
have conclusive_le: ‹conclusive_TWL_run (fst T)
≤ ⇓ {(S, T). T = pstate⇩W_of S}
(SPEC
(conclusive_CDCL_state (mset `# mset CS) (pinit_state (mset `# mset CS))))›
using satisfiable_remdups_iff[of ‹set CS›]
apply -
apply (rule order_trans[OF conclusive_TWL_run_conclusive_CDCL_state[of ‹fst T›]])
using conclusive_TWL_run_conclusive_CDCL_state[of ‹fst T›] clss oth
apply (cases ‹other_clauses_init T = {#}›)
apply (auto simp: br_def struct_invs stgy_invs init get_all_init_clss_alt_init_def
to_init_state0_def init_state0_def conclusive_CDCL_state_def CS' true_clss_def
image_image true_annots_remdups_mset[of _ ‹mset ` set CS›, symmetric]
intro!: ref_two_step'')
done
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 init[unfolded state⇩W_of_def[symmetric]]; fail)
apply (rule conclusive_le)
done
show ?G2
apply (rule cdcl_twl_stgy_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 init[unfolded state⇩W_of_def[symmetric]]; 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 + get_clauses0_l T = remdups_mset `# 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 + get_clauses0_l T = remdups_mset `# 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 + get_clauses0_l T = remdups_mset `# mset `# mset CS);
ASSERT(learned_clss_l (get_clauses_l T) = {#});
cdcl_twl_stgy_restart_prog_early_l T
}
}
}
}›
lemma [twl_st_l_init, simp]:
assumes ‹(s, x) ∈ twl_st_l_init›
shows ‹get_learned_clauses0_init x = get_learned_clauses0_l_init s›
‹get_init_clauses0_init x = get_init_clauses0_l_init s›
using assms by (auto simp: twl_st_l_init_def)
lemma SAT_l_SAT0:
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)
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'
, auto simp: ac_simps)
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'
, auto simp: ac_simps)
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'
, auto simp: ac_simps)
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
apply (rule order_trans)
apply (rule cdcl_twl_stgy_restart_prog_early_l_cdcl_twl_stgy_restart_abs_early_l[THEN fref_to_Down, of _ ‹fst T›])
apply fast
apply (solves simp)
apply (subst Down_id_eq)
apply (rule cdcl_twl_stgy_restart_abs_early_l_cdcl_twl_stgy_restart_abs_early[THEN fref_to_Down, of _ ‹fst Ta›,
THEN order_trans])
apply (auto simp: twl_st_l_init_alt_def intro!: conc_fun_R_mono)
done
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 {})));
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 + get_clauses0_wl T = remdups_mset `# 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 + get_clauses0_wl T = remdups_mset `# 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 + get_clauses0_wl T = remdups_mset `# 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 ();
b ← SPEC(λ_::bool. True);
if b then do {
let S = init_state_l;
𝒜 ← RETURN ();
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 + get_clauses0_l T = remdups_mset `# 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 ();
T ← init_dt CS (to_init_state_l S);
failed ← SPEC (λ_ :: bool. True);
if failed then do {
let S = init_state_l;
𝒜 ← RETURN ();
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)+ get_clauses0_l (fst T) = remdups_mset `# 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) + get_clauses0_l (fst T) = remdups_mset `# 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›
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)
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 NEk=f and UEk=g and NS=h and
US=i and Q=l 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:
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, {#}, {#}, {#}, {#}, {#}, {#}, {#}, {#}), {#})›])
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
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)
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›
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)
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, NEk, UEk, NS, US, N0, U0, {#}, ba) ⟹
blits_in_ℒ⇩i⇩n (af, ag, ah, ai, aj, NEk, UEk, NS, US, N0, U0, ak, ba)› for af ag ah ai aj ak ba NS US N0 U0 NEk UEk
by (auto simp: correct_watching_init.simps blits_in_ℒ⇩i⇩n_def
all_blits_are_in_problem_init.simps all_lits_st_def 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)
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
simp flip: all_lits_st_alt_def IsaSAT_Setup.all_lits_st_alt_def)
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') + get_clauses0_l (fst U') =
remdups_mset `# 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 + get_clauses0_wl U =
remdups_mset `# 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)
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, N0, U0, {#}, ae),
OC)› and
x: ‹x ∈# dom_m aa› and
learned: ‹learned_clss_l aa = {#}›
for af aa y ac ae x OC NS US N0 U0
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 ≤ unat32_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 ≤ unat32_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 by auto
subgoal by (rule init_dt_wl_pre)
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)
apply (rule init_init_dt; assumption)
subgoal by auto
subgoal by (rule init_dt_wl_pre)
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
where
‹extract_model_of_state U = Some (map lit_of (get_trail_wl U))›
where
[simp]: ‹extract_stats U = None›
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 {})));
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 + get_clauses0_wl T = remdups_mset `# 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 + get_clauses0_wl T = remdups_mset `# 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 + get_clauses0_wl T = remdups_mset `# 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
lemma :
‹extract_model_of_state_stat U =
(let _ = print_trail_st2 U in
(False, (fst (get_trail_wl_heur U)), (get_stats_heur U)))›
unfolding extract_model_of_state_stat_def print_trail_st2_def
by auto
definition IsaSAT_use_fast_mode where
‹IsaSAT_use_fast_mode = True›
definition IsaSAT_heur :: ‹opts ⇒ nat clause_l list ⇒ (bool × nat literal list × isasat_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 ≤ unat32_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_init 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;
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_init 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;
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(rewatch_heur_st_fast_pre T);
T ← rewatch_heur_st_init 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 :
‹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 ≤ unat32_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_init 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'');
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_init 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'');
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(rewatch_heur_st_fast_pre T);
T ← rewatch_heur_st_init 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 IsaSAT_Profile.start_def IsaSAT_Profile.stop_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_learned_count_init S = get_learned_count_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_learned_clauses0_wl (fst T) = get_learned_clauses0_wl (fst V) ∧
get_unkept_unit_init_clss_wl (fst T) = get_unkept_unit_init_clss_wl (fst V) ∧
get_kept_unit_init_clss_wl (fst T) = get_kept_unit_init_clss_wl (fst V) ∧
get_unkept_unit_learned_clss_wl (fst T) = get_unkept_unit_learned_clss_wl (fst V) ∧
get_kept_unit_learned_clss_wl (fst T) = get_kept_unit_learned_clss_wl (fst V) ∧
get_unit_clauses_wl (fst T) = get_unit_clauses_wl (fst V) ∧
get_clauses0_wl (fst T) = get_clauses0_wl (fst V)} O {(S, T). S = (T, {#})}›
lemma rewatch_heur_st_rewatch_st:
assumes
‹(x, V)
∈ {((S, _), T).
(S, T)
∈ 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
‹x = (U, C)›
shows ‹rewatch_heur_st_init U ≤
⇓(rewatch_heur_st_rewatch_st_rel CS U V)
(rewatch_st (from_init_state V))›
proof -
let ?𝒜 = ‹(mset_set (extract_atms_clss CS {}))›
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 assms(1) unfolding assms(2) by simp
obtain M' arena D' j W' vm φ clvls cach lbd vdom M N D NE UE NS US Q W OC failed N0 U0 NEk UEk where
V: ‹V = ((M, N, D, NE, UE, NEk, UEk, NS, US, N0, U0, Q, W), OC)›
by (cases V) auto
let ?vdom = ‹(get_vdom_heur_init U)›
let ?W' = ‹get_watchlist_wl_heur_init U›
let ?arena = ‹get_clauses_wl_heur_init U›
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 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 rewatch_heur_st_init_def
apply (simp only: prod.simps from_init_state_def fst_conv nres_monad1 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: V twl_st_heur_parsing_def Collect_eq_comp'
twl_st_heur_parsing_no_WL_def ac_simps)
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_init
(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) ∈ {((S, _), T).
(S, T)
∈ 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_init
(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)
∈ {((S, _), T).
(S, T)
∈ 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 twl_st_heur_parsing_no_WL_wl_twl_st_heur_parsing_no_WL_init:
‹inres (init_state_wl_heur (mset_set (extract_atms_clss CS {}))) Sa ⟹
(Sa, init_state_wl)
∈ twl_st_heur_parsing_no_WL_wl (mset_set (extract_atms_clss CS {})) True ⟹
(Sa, to_init_state init_state_wl)
∈ twl_st_heur_parsing_no_WL (mset_set (extract_atms_clss CS {})) True›
apply (auto simp: twl_st_heur_parsing_no_WL_def
twl_st_heur_parsing_no_WL_wl_def inres_def to_init_state_def
init_state_wl_def init_state_wl_heur_def)
apply (auto simp add: RES_RES_RETURN_RES
RES_RETURN_RES)
done
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, []) ≤
⇓{((S, _), T). (S,T) ∈ 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))› 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 (use that(2) in auto; fail)
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, []) ≤
⇓{((S, _), T). (S,T) ∈ 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))› 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 ≤ unat32_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 ≤ unat32_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; cases ‹get_conflict_wl_heur_init U›) (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: ‹(TC, Ta)
∈ {((T,_), 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) = (λ_. [])}} ⟹
(failed, faileda)
∈ {(b, b'). b = b' ∧ b = (is_failed_heur_init T ∨ ¬ isasat_fast_init T)} ⟹ ¬failed ⟹
TC = (T, C) ⟹
(¬ get_conflict_wl_is_None_heur_init T) = (get_conflict_wl (fst Ta) ≠ None)› for TC C 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 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 + get_clauses0_wl Tc =
remdups_mset `# 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 ‹set_mset (all_atms_st Tc) ≠ {}›
using clss_CS nempty
unfolding all_atms_st_alt_def all_lits_def all_lits_st_def
by (auto simp flip: all_atms_def[symmetric] simp: all_lits_def all_atms_st_def
isasat_input_bounded_nempty_def extract_atms_clss_alt_def ac_simps
all_lits_of_mm_empty_iff)
then have 2: ‹all_atms_st Tc ≠ {#}›
by auto
have 3: ‹set_mset (all_atms_st Tc) = set_mset (mset_set (extract_atms_clss CS {}))›
using clss_CS nempty
unfolding all_atms_st_alt_def all_lits_def all_lits_st_def
by (auto simp flip: all_atms_def[symmetric] all_lits_alt_def simp: ac_simps
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
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]
lookup_clause_rel_cong
have 4: ‹(convert_state (mset_set (extract_atms_clss CS {})) Tb, Tc)
∈ twl_st_heur_post_parsing_wl True›
using T nempty
by (clarsimp simp: twl_st_heur_parsing_def twl_st_heur_post_parsing_wl_def
convert_state_def eq_commute[of ‹mset _› ‹dom_m _›] all_atms_st_def all_lits_st_alt_def[symmetric]
vdom_m_cong[OF 3[symmetric]] ℒ⇩a⇩l⇩l_cong[OF 3[symmetric]] bump_heur_init_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 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 unat64_max_def unat32_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' ∧
get_learned_count_init Tb = get_learned_count S'})›
(is ‹_ ≤ SPEC (λc. _ ∈ ?P)›)
if
Ta: ‹(TC, Ta)
∈ {((T, _), 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) +
get_clauses0_wl (from_init_state Ta) =
remdups_mset `# 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
T: ‹(Tb, Tc) ∈ ?TT T Ta› and
failed: ‹¬is_failed_heur_init T› and
TC: ‹TC = (T, C)›
for uu ba S T Ta baa uua uub V W b Tb Tc TC C
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 unfolding TC 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_atms_st_def all_lits_st_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 {}))›
using clss_CS
unfolding mem_Collect_eq prod.case relcomp.simps all_atms_st_def
all_atms_st_def all_atms_def all_lits_def
by (simp add: ac_simps 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
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]
lookup_clause_rel_cong
have 4: ‹(convert_state (mset_set (extract_atms_clss CS {})) Tb, Tc)
∈ twl_st_heur_post_parsing_wl True›
using T nempty
by (clarsimp simp: twl_st_heur_parsing_def twl_st_heur_post_parsing_wl_def all_atms_st_def
convert_state_def eq_commute[of ‹mset _› ‹dom_m _›] all_lits_st_alt_def[symmetric]
vdom_m_cong[OF 3[symmetric]] ℒ⇩a⇩l⇩l_cong[OF 3[symmetric]] bump_heur_init_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) ∈ (?P Tb)›
for uu ba S T Ta baa uua uub Tb Tc Td Te
proof -
have ‹get_learned_count_init Tb = get_learned_count Td ⟹
learned_clss_count_init Tb = learned_clss_count Td›
by (cases Tb; cases Td; auto simp: learned_clss_count_init_def
learned_clss_count_def clss_size_lcountU0_def clss_size_lcountUEk_def)
moreover have ‹get_learned_count Td = get_learned_count_init T ⟹
learned_clss_count Td = learned_clss_count_init T›
by (cases Td; cases T; auto simp: learned_clss_count_init_def
learned_clss_count_def clss_size_lcountUS_def clss_size_lcountUE_def
clss_size_lcount_def clss_size_lcountUEk_def)
ultimately show ?thesis
using fast Td Tb unfolding mem_Collect_eq prod.case isasat_fast_init_def
by (auto simp add: isasat_fast_def
convert_state_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 (simp add: twl_st_heur_parsing_no_WL_wl_twl_st_heur_parsing_no_WL_init)
apply (rule rewatch_heur_st_rewatch_st)
apply 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
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(26)
by (auto simp: twl_st_heur_loop_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 (simp add: twl_st_heur_parsing_no_WL_wl_twl_st_heur_parsing_no_WL_init)
subgoal by fast
apply (rule init_dt_wl_heur[of ‹mset_set (extract_atms_clss CS {})›])
subgoal by (auto simp: lits_C)
subgoal
by (simp add: twl_st_heur_parsing_no_WL_wl_twl_st_heur_parsing_no_WL_init)
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
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_loop_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 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 auto
subgoal by (clarsimp simp add: isasat_fast_init_def convert_state_def
learned_clss_count_init_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 ac_simps
learned_clss_count_init_def learned_clss_count_def)
apply (rule_tac r1 = ‹length (get_clauses_wl_heur Tc)› 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 snat64_max_def unat64_max_def unat32_max_def)
subgoal by fast
subgoal by fast
subgoal premises p for _ ba S T Ta Tb Tc u v
using p(32)
by (auto simp: twl_st_heur_loop_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)›
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 ∧ consistent_interp (set (the M)) ∧ 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 pget_conflict T = None then Some (map lit_of (pget_trail T)) else None)
}
›
lemma SAT_model_if_satisfiable:
‹(SAT', model_if_satisfiable) ∈ [λCS. True]⇩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› ‹∀C∈#CS. distinct_mset C› 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 ∧ consistent_interp (set (the M)) ∧ set (the M) ⊨sm CS else M = None}›
if
[simp]: ‹CS' = CS› and
s: ‹s ∈ (λT. if pget_conflict T = None then Some (map lit_of (pget_trail T)) else None) `
Collect (conclusive_CDCL_state CS' (pinit_state CS'))›
for s :: ‹nat literal list option› and CS CS'
proof -
obtain T where
s: ‹(s = Some (map lit_of (pget_trail T)) ∧ pget_conflict T = None) ∨
(s = None ∧ pget_conflict T ≠ None)› and
conc: ‹conclusive_CDCL_state CS' ([], CS', {#}, None, {#}, {#}, {#}, {#}, {#}, {#}) T›
using s by auto force
then show ?thesis
using conc
by (auto simp: conclusive_CDCL_state_def true_annots_true_cls lits_of_def)
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). True]⇩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
‹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 by (auto simp: extract_model_of_state_def)
done
lemma SAT_l'_SAT0':
shows ‹SAT_l' CS ≤ ⇓ Id (SAT0' CS)›
unfolding SAT_l'_def SAT0'_def
apply refine_vcg
apply (rule SAT_l_SAT0)
subgoal by (auto simp: extract_model_of_state_def)
done
lemma SAT0'_SAT':
shows ‹SAT0' CS ≤ ⇓ Id (SAT' (mset `# mset CS))›
unfolding SAT'_def SAT0'_def
apply refine_vcg
apply (rule SAT0_SAT)
subgoal by (auto simp: extract_model_of_state_def twl_st_l twl_st)
done
lemma IsaSAT_heur_model_if_sat:
assumes
‹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
unfolding conc_fun_chain
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule SAT_l'_SAT0')
unfolding conc_fun_chain
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule SAT0'_SAT')
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
unfolding conc_fun_chain
apply (auto simp: model_stat_rel_def)
done
lemma IsaSAT_heur_model_if_sat': ‹(uncurry IsaSAT_heur, uncurry (λ_. model_if_satisfiable)) ∈
[λ(_, CS). (∀C∈#CS. ∀L∈#C. nat_of_lit L ≤ unat32_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 ≤ unat32_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 unat32_max_def
ℒ⇩a⇩l⇩l_def)+
apply (metis literal.exhaust_sel)+
done
have ‹nat_of_lit L ≤ unat32_max ∨ nat_of_lit (-L) ≤ unat32_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 ≤ unat32_max›
using L
by (cases L) (auto simp: extract_atms_clss_alt_def unat32_max_def)
qed
show ?thesis
apply (intro frefI nres_relI)
unfolding uncurry_def
apply clarify
subgoal for opt1 CS opt2 CS'
apply (rule IsaSAT_heur_model_if_sat[THEN order_trans, of CS _ ‹opt1›])
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 prag_st) nres› where
‹SAT_bounded CS = do{
T ← SPEC(λT. T = pinit_state (remdups_mset `# CS));
finished ← SPEC(λ_. True);
if ¬finished then
RETURN (True, T)
else
SPEC (λ(b, U). ¬b ⟶ conclusive_CDCL_state 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 (True, fst init_state0)
} else do {
let T = fst T;
if get_conflict T ≠ None
then RETURN (False, T)
else if CS = [] then RETURN (False, 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 + get_all_clauses0 T = remdups_mset `# mset `# mset CS);
ASSERT(get_learned_clss T = {#});
cdcl_twl_stgy_restart_prog_bounded T
}
}
}›
lemma SAT0_bounded_SAT_bounded:
shows ‹SAT0_bounded CS ≤ ⇓ ({((b, S), (b', T)). b = b' ∧ (¬b ⟶ T = pstate⇩W_of S)}) (SAT_bounded (mset `# mset CS))›
(is ‹_ ≤ ⇓?A _›)
proof -
let ?CS = ‹remdups_mset `# mset `# mset CS›
have conflict_during_init:
‹RETURN (False, fst T)
≤ ⇓ {((b, S), b', T). b = b' ∧ (¬b ⟶ T = pstate⇩W_of S)}
(SPEC (λ(b, U). ¬b ⟶ conclusive_CDCL_state (mset `# mset CS) S U))›
if
TS: ‹(T, S)
∈ {(S, T).
(init_dt_spec0 CS (to_init_state0 init_state0) S) ∧
(T = pinit_state ?CS)}› and
‹¬ ¬ failed'› and
‹¬ ¬ failed› and
confl: ‹get_conflict (fst T) ≠ None›
for bS bT failed T failed' S
proof -
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: ‹?CS + clauses (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_init_clauses0_init (to_init_state0 init_state0) +
get_subsumed_init_clauses_init (to_init_state0 init_state0) +
get_init_clauses0_init (to_init_state0 init_state0) =
clauses (get_init_clauses_init T) + other_clauses_init T + get_unit_init_clauses_init T +
get_subsumed_init_clauses_init T +
get_init_clauses0_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)›
‹get_learned_clauses0_init T =
get_learned_clauses0_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
pcdcl_all_struct_invs_def state⇩W_of_init.simps[symmetric]
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
pcdcl_all_struct_invs_def state⇩W_of_init.simps[symmetric]
by fast
have ‹unsatisfiable (set_mset (remdups_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 pget_all_init_clss_pstate⇩W_of_init)
then have unsat[simp]: ‹unsatisfiable (mset ` set CS)›
using satisfiable_remdups_iff[of ‹set CS›]
by auto
then have [simp]: ‹CS ≠ []›
by (auto simp del: unsat)
show ?thesis
unfolding conclusive_CDCL_state_def
apply (rule RETURN_SPEC_refine)
apply (rule exI[of _ ‹(False, pstate⇩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 (False, fst init_state0)
≤ ⇓ ?A
(SPEC
(λ(b, U). ¬b ⟶ conclusive_CDCL_state (mset `# mset CS) S U))›
if
TS: ‹(T, S)
∈ {(S, T).
(init_dt_spec0 CS (to_init_state0 init_state0) S) ∧
(T = pinit_state (?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 _ ‹(False, pinit_state {#})›])
(use that in ‹auto simp: conclusive_CDCL_state_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 = pinit_state (?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 = pstate⇩W_of S)}
(SPEC (λ(b, U). ¬b ⟶ conclusive_CDCL_state (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 = pinit_state ?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) +
get_all_clauses0 (fst T) = ?CS› and
‹get_learned_clss (fst T) = {#}›
for bS bT failed T failed' S
proof -
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: ‹?CS + clauses (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_init_clauses0_init (to_init_state0 init_state0) +
get_subsumed_init_clauses_init (to_init_state0 init_state0) +
get_init_clauses0_init (to_init_state0 init_state0) =
clauses (get_init_clauses_init T) + other_clauses_init T + get_unit_init_clauses_init T +
get_subsumed_init_clauses_init T +
get_init_clauses0_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)›
‹get_learned_clauses0_init T =
get_learned_clauses0_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 init: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init
(state_of (pstate⇩W_of (fst T)))›
using learned
by (cases T)
(auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
to_init_state0_def init_state0_def get_all_init_clss_alt_init_def)
have If_RES_RES: ‹If b (RES (A)) (RES (B)) = RES ({x. (b ⟶ x ∈ A) ∧ (¬b ⟶ x ∈ B)})›
for A B b
by auto
have init: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init
(state_of (pstate⇩W_of (fst T)))›
using learned
by (cases T)
(auto simp:
to_init_state0_def init_state0_def get_all_init_clss_alt_init_def
conclusive_CDCL_state_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def)
have conclusive_le: ‹conclusive_TWL_run_bounded (fst T)
≤ ⇓ {((b, S), b', T). b = b' ∧ (¬b ⟶ T = pstate⇩W_of S)}
(SPEC (λ(b, U). ¬b ⟶ conclusive_CDCL_state (mset `# mset CS) S U))›
apply (rule order_trans[of _
‹do {
b ← SPEC (λ_ :: bool. True);
if ¬b then do {T ← conclusive_TWL_run (fst T); RETURN (False, T)}
else do {
T ← SPEC(λTa. ∃R1 R2 m m⇩0 n⇩0.
cdcl_twl_stgy_restart⇧*⇧* (fst T, fst T, fst T, m⇩0, n⇩0, True) (R1, R2, Ta, m));
RETURN (True, T)
}
}›])
subgoal
unfolding partial_conclusive_TWL_run_def conclusive_TWL_run_def RES_RETURN_RES
If_RES_RES RES_RES_RETURN_RES less_eq_nres.simps
apply (rule)
apply (drule Collect_case_prodD)
apply normalize_goal+
apply (rule_tac a = ‹fst x› in UN_I)
apply simp
apply (fastforce simp: pair_in_image_Pair)
done
subgoal
apply (refine_vcg
lhs_step_If)
subgoal
using satisfiable_remdups_iff[of ‹set CS›]
apply -
unfolding conc_fun_RES
apply (rule RETURN_le_RES_no_return)
apply (rule conclusive_TWL_run_conclusive_CDCL_state[THEN order_trans])
using clss arg_cong[OF clss, of set_mset, simplified] bT_bS confl oth init
by (auto simp: br_def conc_fun_RES struct_invs stgy_invs
to_init_state0_def init_state0_def get_all_init_clss_alt_init_def
conclusive_CDCL_state_def image_image
true_annots_remdups_mset[symmetric, of _ ‹mset ` set CS›])
subgoal
by (intro RETURN_RES_refine)
(auto simp: conclusive_CDCL_state_def)
done
done
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 init[unfolded state⇩W_of_def[symmetric]]; 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 = pinit_state ?CS)}
(SPEC (λT. T = pinit_state ?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 (True, fst init_state_l)
} else do {
let T = fst T;
if get_conflict_l T ≠ None
then RETURN (False, T)
else if CS = [] then RETURN (False, 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 + get_clauses0_l T = remdups_mset `# 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:
shows ‹SAT_l_bounded CS ≤ ⇓ {((b, T),(b', T')). b=b' ∧ (¬b ⟶ (T, T') ∈ twl_st_l None)} (SAT0_bounded CS)›
(is ‹_ ≤ ⇓ ?A _›)
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)
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: ‹ ((False, fst init_state_l), False, fst init_state0)
∈ ?A›
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 simp del: twl_st_init(42)
simp flip: twl_st_init(42))
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',
auto simp: ac_simps)
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 {})));
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 (False, T)
else if CS = [] then RETURN (False, ([], 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 + get_clauses0_wl T = remdups_mset `# 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 ();
let S = init_state_l;
𝒜 ← RETURN ();
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 (False, fst T)
else if CS = [] then RETURN (False, 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) + get_clauses0_l (fst T)= remdups_mset `# 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
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)
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›
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:
‹((False, ([], fmempty, None, {#}, {#}, {#}, {#}, {#}, {#}, {#}, {#}, {#}, λ_. undefined)),
(False, 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)
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, N0, U0, {#}, ae),
OC)› and
x: ‹x ∈# dom_m aa› and
learned: ‹learned_clss_l aa = {#}›
for af aa y ac ae x OC NS US N0 U0
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 ≤ unat32_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 ≤ unat32_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 by (rule init_dt_wl_pre)
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 pget_conflict T = None then Some (map lit_of (pget_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. True]⇩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› ‹∀C∈#CS. distinct_mset C›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
[simp]: ‹CS' = CS› and
s: ‹s ∈ (λT. if pget_conflict T = None then Some (map lit_of (pget_trail T)) else None) `
Collect (conclusive_CDCL_state CS' (pinit_state (remdups_mset `# CS')))›
for s :: ‹nat literal list option› and CS CS'
proof -
obtain T where
s: ‹(s = Some (map lit_of (pget_trail T)) ∧ pget_conflict T = None) ∨
(s = None ∧ pget_conflict T ≠ None)› and
conc: ‹conclusive_CDCL_state CS' ([], remdups_mset `# CS', {#}, None, {#}, {#}, {#}, {#}, {#}, {#}) T›
using s by auto force
show ?thesis
using s conc
by (auto simp: conclusive_CDCL_state_def lits_of_def true_annots_true_cls)
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
‹CS' = CS› and
‹xa ∈ {T. T = pinit_state (remdups_mset `# CS')}› and
‹xb ∈ {_. True}› and
‹s ∈ uncurry
(λb T. (b, if pget_conflict T = None
then Some (map lit_of (pget_trail T)) else None)) `
(if ¬ xb then {(True, xa)}
else {(b, U). ¬ b ⟶ conclusive_CDCL_state CS' xa U})›
for s :: ‹bool × nat literal list option› and
CS CS' :: ‹nat literal multiset multiset› and xa and xb :: bool
proof -
obtain b T where
s: ‹s = (b, T)› by (cases s)
have
b: ‹¬b ⟶ T ∈ (λT. if pget_conflict T = None then Some (map lit_of (pget_trail T)) else None) `
Collect (conclusive_CDCL_state CS (pinit_state (remdups_mset `# CS)))›
using that(2-4)
by (force simp add: image_iff s that split: if_splits)
show ?thesis
proof (cases b)
case False
then have T: ‹T ∈ (λT. if pget_conflict T = None then Some (map lit_of (pget_trail T)) else None) `
Collect (conclusive_CDCL_state CS' (pinit_state (remdups_mset `# CS')))›
using b unfolding that(1) by fast
show ?thesis
using H[OF that(1) T]
by (rule_tac x = ‹s› in bexI)
(auto simp add: s False 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). True]⇩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':
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 by (auto simp: extract_model_of_state_def)
done
lemma SAT0_bounded'_SAT_bounded':
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 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 {})));
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 (True, extract_stats init_state_wl)
} else do {
let T = from_init_state T;
if get_conflict_wl T ≠ None
then RETURN (False, extract_stats T)
else if CS = [] then RETURN (False, 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 + get_clauses0_wl T = remdups_mset `# 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 empty_conflict_code' :: ‹(bool × _ list × isasat_stats) nres› where
‹empty_conflict_code' = do{
let M0 = [];
RETURN (False, M0, empty_stats)}›
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 ≤ unat32_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_b CS S;
failed ← RETURN ((isasat_fast_init T ∧ ¬is_failed_heur_init T));
if ¬failed
then do {
RETURN (True, empty_init_code)
} else do {
let T = convert_state 𝒜⇩i⇩n' T;
if ¬get_conflict_wl_is_None_heur_init T
then RETURN (False, empty_init_code)
else if CS = [] then do {stat ← empty_conflict_code; RETURN (False, stat)}
else do {
ASSERT(𝒜⇩i⇩n' ≠ {#});
ASSERT(isasat_input_bounded_nempty 𝒜⇩i⇩n');
ASSERT(rewatch_heur_st_fast_pre T);
T ← rewatch_heur_st_init 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 IsaSAT_Profile.start_def IsaSAT_Profile.stop_def nres_monad1
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_unb 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))› and
‹((CS, S), CS, T) ∈ ⟨Id⟩list_rel ×⇩f twl_st_heur_parsing_no_WL 𝒜 True›
for 𝒜 CS T S
proof -
have H: ‹init_dt_wl' CS T = do {T ← init_dt_wl' CS T; RETURN T}›
by auto
have I: ‹⇓ {((S, C), T). C = [] ∧ (S, T) ∈ twl_st_heur_parsing_no_WL 𝒜 True} (init_dt_wl CS T)
≤ ⇓{((S, C), T). (S,T) ∈ twl_st_heur_parsing_no_WL 𝒜 True O {(S, T). S = remove_watched T ∧
get_watched_wl (fst T) = (λ_. [])}} (init_dt_wl' CS T)›
by (cases ‹init_dt_wl CS T›)
(force simp: init_dt_wl'_def RES_RETURN_RES conc_fun_RES
Image_iff)+
show ?thesis
unfolding init_dt_wl_heur_unb_def
apply (subst H)
apply (refine_rcg)
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 (use that(2) in auto)[]
apply (rule I)
apply auto
done
qed
have init_dt_wl_heur_b: ‹init_dt_wl_heur_b 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))› and
‹((CS, S), CS, T) ∈ ⟨Id⟩list_rel ×⇩f twl_st_heur_parsing_no_WL 𝒜 True›
for 𝒜 CS T S
proof -
have H: ‹init_dt_wl' CS T = do {T ← init_dt_wl' CS T; RETURN T}›
by auto
have I: ‹⇓ {((S, C), T). C = [] ∧ (S, T) ∈ twl_st_heur_parsing_no_WL 𝒜 False} (init_dt_wl CS T)
≤ ⇓{((S, C), T). (S,T) ∈ twl_st_heur_parsing_no_WL 𝒜 False O {(S, T). S = remove_watched T ∧
get_watched_wl (fst T) = (λ_. [])}} (init_dt_wl' CS T)›
by (cases ‹init_dt_wl CS T›)
(force simp: init_dt_wl'_def RES_RETURN_RES conc_fun_RES
Image_iff)+
show ?thesis
unfolding init_dt_wl_heur_b_def
apply (subst H)
apply (refine_rcg)
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 (rule I)
apply auto
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 ≤ unat32_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 ≤ unat32_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; cases ‹get_conflict_wl_heur_init U›) (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 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 + get_clauses0_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 clss_CS unfolding all_atms_def all_lits_alt_def all_atms_st_def
by (simp add: ac_simps 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 clss_CS unfolding all_atms_def all_atms_st_def all_lits_def
apply (auto simp: extract_atms_clss_alt_def ac_simps
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
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] lookup_clause_rel_cong
have 4: ‹(convert_state (mset_set (extract_atms_clss CS {})) Tb, Tc)
∈ twl_st_heur_post_parsing_wl True›
using T nempty
by (clarsimp simp: twl_st_heur_parsing_def twl_st_heur_post_parsing_wl_def
convert_state_def eq_commute[of ‹mset _› ‹dom_m _›] all_atms_st_def
vdom_m_cong[OF 3[symmetric]] ℒ⇩a⇩l⇩l_cong[OF 3[symmetric]] bump_heur_init_cong[OF 3[symmetric]]
dest!: cong[OF 3[symmetric]])
(simp_all add: add.assoc ℒ⇩a⇩l⇩l_all_atms_all_lits ac_simps
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 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 unat64_max_def unat32_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' ∧
get_learned_count_init Tb = get_learned_count S'})›
(is ‹_ ≤ SPEC (λc. _ ∈ ?P)›)
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)
+ get_clauses0_wl (from_init_state Ta) =
remdups_mset `# 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
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 all_atms_st_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 {}))›
using clss_CS unfolding all_lits_alt_def mem_Collect_eq prod.case relcomp.simps
all_atms_def all_atms_st_def apply -
by (auto simp: extract_atms_clss_alt_def ac_simps
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
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] lookup_clause_rel_cong
have 4: ‹(convert_state (mset_set (extract_atms_clss CS {})) Tb, Tc)
∈ twl_st_heur_post_parsing_wl True›
using T nempty
by (clarsimp simp: twl_st_heur_parsing_def twl_st_heur_post_parsing_wl_def all_atms_st_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]] bump_heur_init_cong[OF 3[symmetric]]
dest!: cong[OF 3[symmetric]])
(simp_all add: add.assoc ℒ⇩a⇩l⇩l_all_atms_all_lits ac_simps
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) ∈ ?P Tb›
for uu ba S T Ta baa uua uub Tb Tc Td Te
proof -
have ‹get_learned_count_init Tb = get_learned_count Td ⟹
learned_clss_count_init Tb = learned_clss_count Td›
by (cases Tb; cases Td; auto simp: learned_clss_count_init_def
learned_clss_count_def)
moreover have ‹get_learned_count Td = get_learned_count_init T ⟹
learned_clss_count Td = learned_clss_count_init T›
by (cases Td; cases T; auto simp: learned_clss_count_init_def
learned_clss_count_def clss_size_lcountUS_def clss_size_lcountUE_def
clss_size_lcount_def)
ultimately show ?thesis
using fast Td Tb unfolding mem_Collect_eq prod.case isasat_fast_init_def
by (auto simp add: isasat_fast_def
convert_state_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 (clarsimp 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)
(auto simp add: ac_simps)
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 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 learned_clss_count_init_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 simp add: isasat_fast_def isasat_fast_init_def convert_state_def ac_simps
learned_clss_count_init_def learned_clss_count_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 snat64_max_def unat32_max_def
unat64_max_def)
subgoal by fast
subgoal by simp
subgoal premises p
using p(26-)
by (auto simp: twl_st_heur_loop_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
‹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 by (auto simp: extract_model_of_state_def)
done
lemma IsaSAT_bounded_heur_model_if_sat:
assumes
‹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
unfolding conc_fun_chain
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule SAT_l_bounded'_SAT0_bounded')
unfolding conc_fun_chain
apply (rule order_trans)
apply (rule ref_two_step')
apply (rule SAT0_bounded'_SAT_bounded')
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
apply (rule IdI)
unfolding conc_fun_chain
apply (rule conc_fun_R_mono)
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. ∀L∈#C. nat_of_lit L ≤ unat32_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 ≤ unat32_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 unat32_max_def
ℒ⇩a⇩l⇩l_def)+
apply (metis literal.exhaust_sel)+
done
have ‹nat_of_lit L ≤ unat32_max ∨ nat_of_lit (-L) ≤ unat32_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 ≤ unat32_max›
using L
by (cases L) (auto simp: extract_atms_clss_alt_def unat32_max_def)
qed
show ?thesis
apply (intro frefI nres_relI)
unfolding uncurry_def
apply clarify
subgoal for opt1 CS opt2 CS'
apply (rule IsaSAT_bounded_heur_model_if_sat[THEN order_trans, of CS _ opt1])
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