Theory Watched_Literals_Transition_System_Restart

theory Watched_Literals_Transition_System_Restart
imports CDCL.Pragmatic_CDCL_Restart Watched_Literals_Transition_System
  Watched_Literals_Transition_System_Inprocessing
begin


text ‹
  Unlike the basic CDCL, it does not make any sense to fully restart the trail:
  the part propagated at level 0 (only the part due to unit clauses) has to be kept.
  Therefore, we allow fast restarts (i.e. a restart where part of the trail is reused).

  There are two cases:
    ▪ either the trail is strictly decreasing;
    ▪ or it is kept and the number of clauses is strictly decreasing.

  This ensures that ∗‹something› changes to prove termination.

  In practice, there are two types of restarts that are done:
    ▪ First, a restart can be done to enforce that the SAT solver goes more into the direction
      expected by the decision heuristics.
    ▪ Second, a full restart can be done to simplify inprocessing and garbage collection of the memory:
      instead of properly updating the trail, we restart the search. This is not necessary (i.e.,
      glucose and minisat do not do it), but it simplifies the proofs by allowing to move clauses
      without taking care of updating references in the trail. Moreover, as this happens ``rarely''
      (around once every few thousand conflicts), it should not matter too much.

  Restarts are the ``local search'' part of all modern SAT solvers.
›

inductive cdcl_twl_restart :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
restart_trail:
   ‹cdcl_twl_restart (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
        (M', N', U', None, NE + clauses NE', UE'', NS, {#},N0, {#}, 
           {#}, {#})›
  if
    ‹(Decided K # M', M2) ∈ set (get_all_ann_decomposition M)› and
    ‹U' + UE' ⊆# U› and
    ‹N = N' + NE'› and
    ‹∀E∈#NE'+UE'. ∃L∈#clause E. L ∈ lits_of_l M' ∧ get_level M' L = 0›
    ‹∀L E. Propagated L E ∈ set M' ⟶ E ∈# clause `# (N + U') + (NE+ clauses NE') + UE''›
    ‹UE'' ⊆#  UE + clauses UE'› |
restart_clauses:
   ‹cdcl_twl_restart (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
      (M, N', U', None, NE + clauses NE', UE'', NS, US', N0, {#}, {#}, Q)›
  if
    ‹U' + UE' ⊆# U› and
    ‹N = N' + NE'› and
    ‹∀E∈#NE'+UE'. ∃L∈#clause E. L ∈ lits_of_l M ∧ get_level M L = 0›
    ‹∀L E. Propagated L E ∈ set M ⟶ E ∈# clause `# (N + U') + (NE+ clauses NE') + UE''›
    ‹US' = {#}›
    ‹UE'' ⊆#  UE + clauses UE'›

inductive_cases cdcl_twl_restartE: ‹cdcl_twl_restart S T›


inductive cdcl_twl_restart_only :: ‹'v twl_st ⇒ 'v twl_st ⇒ bool› where
restart_trail:
  ‹cdcl_twl_restart_only (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
  (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})›
  if
    ‹(Decided K # M', M2) ∈ set (get_all_ann_decomposition M)› |
norestart_trail:
  ‹cdcl_twl_restart_only (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)
    (M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›


lemma past_invs_simps_emptyU0:
  ‹past_invs (M, N, U, D, NE, UE, NS, US, N0, U0, WS, Q) ⟷
    (∀M1 M2 K. M = M2 @ Decided K # M1 ⟶ (
      (∀C ∈# N + U. twl_lazy_update M1 C ∧
        watched_literals_false_of_max_level M1 C ∧
        twl_exception_inv (M1, N, U, None, NE, UE, NS, US, N0, {#}, {#}, {#}) C) ∧
      confl_cands_enqueued (M1, N, U, None, NE, UE, NS, US, N0, {#}, {#}, {#}) ∧
      propa_cands_enqueued (M1, N, U, None, NE, UE, NS, US, N0, {#}, {#}, {#}) ∧
  clauses_to_update_inv (M1, N, U, None, NE, UE, NS, US, N0, {#}, {#}, {#})))›
  unfolding past_invs.simps by (auto simp: twl_exception_inv.simps)

lemma cdcl_twl_restart_pcdcl: ‹cdcl_twl_restart S T ⟹ pcdcl_restart (pstate⇩W_of S) (pstate⇩W_of T)›
  by (induction rule: cdcl_twl_restart.induct)
   (auto simp add: pcdcl_restart.simps dest: image_mset_subseteq_mono
      intro!: exI[of _ ‹clauses _›])

lemma cdcl_twl_restart_twl_struct_invs:
  assumes
    ‹cdcl_twl_restart S T› and
    ‹twl_struct_invs S›
  shows ‹twl_struct_invs T›
  using assms cdcl_twl_restart_pcdcl[OF assms(1)]
proof (induction rule: cdcl_twl_restart.induct)
  case (restart_trail K M' M2 M U' UE' U N N' NE' NE UE'' UE NS US N0 U0 Q)
  note decomp = this(1) and learned' = this(2) and N = this(3) and
    has_true = this(4) and kept = this(5) and incl = this(6) and inv = this(7) and st' = this(8)
  let ?S = ‹(M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
  let ?S' = ‹(M', N', U', None, NE+ clauses NE', UE'', NS, {#}, N0, {#}, {#}, {#})›
  have learned: ‹U' ⊆# U›
    using learned' by (rule mset_le_decr_left1)
  have
    twl_st_inv: ‹twl_st_inv ?S› and
    ‹valid_enqueued ?S› and
    struct_inv: ‹pcdcl_all_struct_invs (pstate⇩W_of ?S)› and
    smaller: ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S)› and
    ‹twl_st_exception_inv ?S› and
    no_dup_q: ‹no_duplicate_queued ?S› and
    dist: ‹distinct_queued ?S› and
    ‹confl_cands_enqueued ?S› and
    ‹propa_cands_enqueued ?S› and
    ‹get_conflict ?S ≠ None ⟶
     clauses_to_update ?S = {#} ∧
     literals_to_update ?S = {#}› and
    to_upd: ‹clauses_to_update_inv ?S› and
    past: ‹past_invs ?S›
    using inv unfolding twl_struct_invs_def pcdcl_all_struct_invs_def by clarsimp+
  have
    ex: ‹(∀C∈#N + U. twl_lazy_update M' C ∧
           watched_literals_false_of_max_level M' C ∧
           twl_exception_inv (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#}) C)› and
     conf_cands: ‹confl_cands_enqueued (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})› and
     propa_cands: ‹propa_cands_enqueued (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})› and
     clss_to_upd: ‹clauses_to_update_inv (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})›
     using past get_all_ann_decomposition_exists_prepend[OF decomp] unfolding past_invs.simps
     by force+

   have excp_inv: ‹twl_st_exception_inv (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})›
     using ex unfolding twl_st_exception_inv.simps by blast+
   have twl_st_inv': ‹twl_st_inv (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})›
     using ex learned twl_st_inv
     unfolding twl_st_exception_inv.simps twl_st_inv.simps
     by auto
   have n_d: ‹no_dup M›
     using struct_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
       cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def pcdcl_all_struct_invs_def
     by (auto simp: trail.simps)
   obtain M3 where
     M: ‹M = M3 @ M2 @ Decided K # M'›
     using decomp by blast
   define M3' where ‹M3' = M3 @ M2›
   then have M3': ‹M = M3' @ Decided K # M'›
     unfolding M by auto
   have a: ‹N ⊆# N› and NN': ‹N' ⊆# N› using N by auto
   have past_invs: ‹past_invs ?S'›
     unfolding past_invs.simps
   proof (intro conjI impI allI)
     fix M1 M2 K'
     assume H:‹M' = M2 @ Decided K' # M1›
     let ?U = ‹(M1, N, U, None, NE, UE, NS, US, N0, {#}, {#}, {#})›
     let ?U' = ‹(M1, N', U', None, NE+clauses NE', UE'', NS, {#}, N0, {#}, {#}, {#})›
     have ‹M = (M3' @ Decided K # M2) @ Decided K' # M1›
       using H M3' by simp
     then have
       1: ‹∀C∈#N + U.
           twl_lazy_update M1 C ∧
           watched_literals_false_of_max_level M1 C ∧
           twl_exception_inv ?U C› and
       2: ‹confl_cands_enqueued ?U› and
       3: ‹propa_cands_enqueued ?U› and
       4: ‹clauses_to_update_inv ?U›
       using past unfolding past_invs_simps_emptyU0 by blast+
     show ‹∀C∈#N' + U'.
          twl_lazy_update M1 C ∧
          watched_literals_false_of_max_level M1 C ∧
          twl_exception_inv ?U' C›
       using 1 learned twl_st_exception_inv_mono[OF learned NN', of M1 None NE ‹UE›
           NS US N0 ‹{#}› ‹{#}› ‹{#}› ‹NE+clauses NE'› ‹UE''›] N
         twl_st_exception_inv_U0_mono[OF _ twl_st_exception_inv_subsumed_mono[of  ‹{#}› US M1 N' U' None ‹NE+clauses NE'›
           ‹UE''› NS N0 ‹{#}› ‹{#}› ‹{#}›]]
        by auto

     show ‹confl_cands_enqueued ?U'›
       by (rule confl_cands_enqueued_subsumed_mono[OF _ confl_cands_enqueued_mono[OF learned NN' 2]])
         auto
     show ‹propa_cands_enqueued ?U'›
       by (rule propa_cands_enqueued_subsumed_mono[OF _ propa_cands_enqueued_mono[OF learned NN' 3]])
         auto
     show ‹clauses_to_update_inv ?U'›
       using 4 learned by (auto simp add: filter_mset_empty_conv N)
   qed
   have clss_to_upd: ‹clauses_to_update_inv ?S'›
     using clss_to_upd learned by (auto simp add: filter_mset_empty_conv N)

   have struct_inv': ‹pcdcl_all_struct_invs (pstate⇩W_of ?S')›
     using pcdcl_restart_pcdcl_all_struct_invs[OF st' struct_inv] by simp
   have smaller': ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S')›
     using pcdcl_restart_no_smaller_propa'[OF st'] smaller by simp
   show ?case
     unfolding twl_struct_invs_def
     apply (intro conjI)
     subgoal
       using twl_st_inv_subsumed_mono[OF _ twl_st_inv_mono[OF learned NN' twl_st_inv']]
       by (auto simp: ac_simps N)
     subgoal by simp
     subgoal by (rule struct_inv')
     subgoal by (rule smaller')
     subgoal by (rule twl_st_exception_inv_U0_mono[OF _ twl_st_exception_inv_subsumed_mono[OF _ twl_st_exception_inv_mono[OF learned NN' excp_inv]]])
       auto
     subgoal using no_dup_q by auto
     subgoal using dist by auto
     subgoal
       by (rule confl_cands_enqueued_U0_mono[OF _ confl_cands_enqueued_subsumed_mono[OF _ confl_cands_enqueued_mono[OF learned NN' conf_cands]]])
         auto
     subgoal by (rule propa_cands_enqueued_U0_mono[OF _ propa_cands_enqueued_subsumed_mono[OF _ propa_cands_enqueued_mono[OF learned NN' propa_cands]]])
       auto
     subgoal by simp
     subgoal by (rule clss_to_upd)
     subgoal by (rule past_invs)
     done
next
  case (restart_clauses U' UE' U N N' NE' M NE UE'' US' UE NS US N0 U0 Q)
  note learned' = this(1) and N = this(2) and has_true = this(3) and kept = this(4) and
    US = this(5) and incl = this(6) and invs = this(7) and st' = this(8)
  let ?S = ‹(M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
  let ?T = ‹(M, N', U', None, NE+clauses NE', UE'', NS, US', N0, {#}, {#}, Q)›
  have learned: ‹U' ⊆# U›
    using learned' by (rule mset_le_decr_left1)
  have
    twl_st_inv: ‹twl_st_inv ?S› and
    valid: ‹valid_enqueued ?S› and
    struct_inv: ‹pcdcl_all_struct_invs (pstate⇩W_of ?S)› and
    smaller: ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S)› and
    excp_inv: ‹twl_st_exception_inv ?S› and
    no_dup_q: ‹no_duplicate_queued ?S› and
    dist: ‹distinct_queued ?S› and
    confl_cands: ‹confl_cands_enqueued ?S› and
    propa_cands: ‹propa_cands_enqueued ?S› and
    ‹get_conflict ?S ≠ None ⟶
     clauses_to_update ?S = {#} ∧
     literals_to_update ?S = {#}› and
    to_upd: ‹clauses_to_update_inv ?S› and
    past: ‹past_invs ?S›
    using invs unfolding twl_struct_invs_def by clarify+
   have n_d: ‹no_dup M›
     using struct_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
       cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def pcdcl_all_struct_invs_def by (auto simp: trail.simps)
   have valid': ‹valid_enqueued ?T›
     using valid by auto

   have NN': ‹N' ⊆# N› unfolding N by auto
   have past_invs: ‹past_invs ?T›
     using past unfolding past_invs.simps
   proof (intro conjI impI allI)
     fix M1 M2 K'
     assume H:‹M = M2 @ Decided K' # M1›
     let ?U = ‹(M1, N, U, None, NE, UE, NS, US, N0, {#}, {#}, {#})›
     let ?U' = ‹(M1, N', U', None, NE+clauses NE', UE'', NS, US', N0, {#}, {#}, {#})›
     have
       1: ‹∀C∈#N + U.
           twl_lazy_update M1 C ∧
           watched_literals_false_of_max_level M1 C ∧
           twl_exception_inv ?U C› and
       2: ‹confl_cands_enqueued ?U› and
       3: ‹propa_cands_enqueued ?U› and
       4: ‹clauses_to_update_inv ?U›
       using H past unfolding past_invs_simps_emptyU0 by blast+
     show ‹∀C∈#N' + U'.
          twl_lazy_update M1 C ∧
          watched_literals_false_of_max_level M1 C ∧
          twl_exception_inv ?U' C›
       using 1 learned twl_st_exception_inv_subsumed_mono[OF _
              twl_st_exception_inv_mono[OF learned NN', of M1 None NE UE NS US N0 ‹{#}› ‹{#}› ‹{#}›
              ‹NE + clauses NE'› ‹UE''›], of ‹US'›] N US
       by (auto split: if_splits)
     show ‹confl_cands_enqueued ?U'›
       by (rule confl_cands_enqueued_subsumed_mono[OF _ confl_cands_enqueued_mono[OF learned NN' 2]])
         (use US in ‹auto split: if_splits›)
     show ‹propa_cands_enqueued ?U'›
       by (rule propa_cands_enqueued_subsumed_mono[OF _ propa_cands_enqueued_mono[OF learned NN' 3]])
         (use US in ‹auto split: if_splits›)
     show ‹clauses_to_update_inv ?U'›
       using 4 learned by (auto simp add: filter_mset_empty_conv N)
   qed

   let ?S' = ‹(M, N', U', None, NE + clauses NE', UE'', NS, US', N0, {#}, {#}, Q)›
   have struct_inv': ‹pcdcl_all_struct_invs (pstate⇩W_of ?S')›
     using pcdcl_restart_pcdcl_all_struct_invs[OF st' struct_inv] by simp
   have smaller': ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S')›
     using pcdcl_restart_no_smaller_propa'[OF st'] smaller by simp

   have clss_to_upd: ‹clauses_to_update_inv ?T›
     using to_upd learned by (auto simp add: filter_mset_empty_conv N ac_simps)


   show ?case
    unfolding twl_struct_invs_def
    apply (intro conjI)
    subgoal using twl_st_inv_U0_subsumed_mono[OF _
      twl_st_inv_subsumed_mono[OF _ twl_st_inv_mono[OF learned NN' twl_st_inv]]] US
      by (auto simp: ac_simps N split: if_splits)
    subgoal by (rule valid')
    subgoal by (rule struct_inv')
    subgoal by (rule smaller')
    subgoal by (rule twl_st_exception_inv_U0_mono[OF _
      twl_st_exception_inv_subsumed_mono[OF _ twl_st_exception_inv_mono[OF learned NN' excp_inv]]])
      (use US in ‹auto split: if_splits›)
    subgoal using no_dup_q by auto
    subgoal using dist by auto
    subgoal by (rule confl_cands_enqueued_U0_mono[OF _ confl_cands_enqueued_subsumed_mono[OF _ confl_cands_enqueued_mono[OF learned NN' confl_cands]]])
       (use US in ‹auto split: if_splits›)
    subgoal by (rule propa_cands_enqueued_U0_mono [
      OF _ propa_cands_enqueued_subsumed_mono[OF _ propa_cands_enqueued_mono[OF learned NN' propa_cands]]])
      (use US in ‹auto split: if_splits›)
    subgoal by simp
    subgoal by (rule clss_to_upd)
    subgoal by (rule past_invs)
    done
qed

lemma in_multiset_subsetD:
  ‹A ∈# B ⟹ B ⊆# C + D ⟹ A ∈# C ∨ A ∈# D›
  by auto
  
lemma rtranclp_cdcl_twl_restart_twl_struct_invs:
  assumes
    ‹cdcl_twl_restart⇧*⇧* S T› and
    ‹twl_struct_invs S›
  shows ‹twl_struct_invs T›
  using assms by (induction rule: rtranclp_induct) (auto simp: cdcl_twl_restart_twl_struct_invs)

lemma cdcl_twl_restart_twl_stgy_invs:
  assumes
    ‹cdcl_twl_restart S T› and ‹twl_stgy_invs S›
  shows ‹twl_stgy_invs T›
  using assms
  by (induction rule: cdcl_twl_restart.induct)
   (auto 4 3 simp: twl_stgy_invs_def cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
        cdcl⇩W_restart_mset.conflict_non_zero_unless_level_0_def
        conflicting.simps cdcl⇩W_restart_mset.no_smaller_confl_def clauses_def trail.simps
      dest: in_multiset_subsetD
      dest!: get_all_ann_decomposition_exists_prepend
    split: if_splits)

lemma rtranclp_cdcl_twl_restart_twl_stgy_invs:
  assumes
    ‹cdcl_twl_restart⇧*⇧* S T› and
    ‹twl_stgy_invs S›
  shows ‹twl_stgy_invs T›
  using assms by (induction rule: rtranclp_induct) (auto simp: cdcl_twl_restart_twl_stgy_invs)

lemma cdcl_twl_restart_only_cdcl: ‹cdcl_twl_restart_only T U ⟹
  pcdcl_restart_only (pstate⇩W_of T) (pstate⇩W_of U)›
  by (auto 5 3 simp: cdcl_twl_restart_only.simps pcdcl_restart_only.simps)

lemma cdcl_twl_restart_only_twl_struct_invs:
  assumes
    ‹cdcl_twl_restart_only S T› and
    ‹twl_struct_invs S›
  shows ‹twl_struct_invs T›
  using assms cdcl_twl_restart_only_cdcl[OF assms(1)]
proof (induction rule: cdcl_twl_restart_only.induct)
  case (norestart_trail M N U NE UE NS US Q)
  note invs = this(1) and st' = this(2)
  then show ?case
    by simp
next
  case (restart_trail K M' M2 M N U NE UE NS US N0 U0 Q)
  note decomp = this(1) and inv = this(2) and st' = this(3)
  let ?S = ‹(M, N, U, None, NE, UE, NS, US, N0, U0, {#}, Q)›
  let ?T = ‹(M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})›
  have
    twl_st_inv: ‹twl_st_inv ?S› and
    ‹valid_enqueued ?S› and
    struct_inv: ‹pcdcl_all_struct_invs (pstate⇩W_of ?S)› and
    smaller: ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?S)› and
    excep: ‹twl_st_exception_inv ?S› and
    no_dup_q: ‹no_duplicate_queued ?S› and
    dist: ‹distinct_queued ?S› and
    confl: ‹confl_cands_enqueued ?S› and
    propa: ‹propa_cands_enqueued ?S› and
    ‹get_conflict ?S ≠ None ⟶
     clauses_to_update ?S = {#} ∧
     literals_to_update ?S = {#}› and
    to_upd: ‹clauses_to_update_inv ?S› and
    past: ‹past_invs ?S›
    using inv unfolding twl_struct_invs_def pcdcl_all_struct_invs_def by clarsimp+
  have
    ex: ‹(∀C∈#N + U. twl_lazy_update M' C ∧
           watched_literals_false_of_max_level M' C ∧
           twl_exception_inv (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#}) C)› and
     conf_cands: ‹confl_cands_enqueued (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})› and
     propa_cands: ‹propa_cands_enqueued (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})› and
     clss_to_upd: ‹clauses_to_update_inv (M', N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})›
    using past get_all_ann_decomposition_exists_prepend[OF decomp]
      confl propa to_upd excep
    unfolding past_invs.simps
    by force+

   have excp_inv: ‹twl_st_exception_inv ?T›
     using ex unfolding twl_st_exception_inv.simps by blast+
   have twl_st_inv': ‹twl_st_inv ?T›
     using ex twl_st_inv
     unfolding twl_st_exception_inv.simps twl_st_inv.simps
     by auto
   have n_d: ‹no_dup M›
     using struct_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
       cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def pcdcl_all_struct_invs_def
     by (auto simp: trail.simps)
   obtain M3 where
     M: ‹M = M3 @ M2 @ Decided K # M'›
     using decomp by blast
   define M3' where ‹M3' = M3 @ M2›
   then have M3': ‹M = M3' @ Decided K # M'›
     unfolding M by auto
   have past_invs: ‹past_invs ?T›
     unfolding past_invs.simps
   proof (intro conjI impI allI)
     fix M1 M2 K'
     assume H:‹M' = M2 @ Decided K' # M1›
     let ?U = ‹(M1, N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})›
     let ?U' = ‹(M1, N, U, None, NE, UE, NS, US, N0, U0, {#}, {#})›
     have ‹M = (M3' @ Decided K # M2) @ Decided K' # M1›
       using H M3' by simp
     then show
       1: ‹∀C∈#N + U.
           twl_lazy_update M1 C ∧
           watched_literals_false_of_max_level M1 C ∧
           twl_exception_inv ?U C› and
       2: ‹confl_cands_enqueued ?U› and
       3: ‹propa_cands_enqueued ?U› and
       4: ‹clauses_to_update_inv ?U›
       using past unfolding past_invs.simps by blast+
   qed
   have clss_to_upd: ‹clauses_to_update_inv ?T›
     using clss_to_upd by (auto simp add: filter_mset_empty_conv)

   have struct_inv': ‹pcdcl_all_struct_invs (pstate⇩W_of ?T)›
     using pcdcl_restart_only_pcdcl_all_struct_invs st' struct_inv by fastforce
   have smaller': ‹cdcl⇩W_restart_mset.no_smaller_propa (state⇩W_of ?T)›
     using pcdcl_restart_only_no_smaller_propa smaller st' state⇩W_of_def struct_inv by force
   show ?case
     unfolding twl_struct_invs_def
     apply (intro conjI)
     subgoal
       using twl_st_inv' by (auto simp: ac_simps)
     subgoal by simp
     subgoal by (rule struct_inv')
     subgoal by (rule smaller')
     subgoal using excp_inv by auto
     subgoal using no_dup_q by auto
     subgoal using dist by auto
     subgoal using conf_cands by auto

     subgoal using propa_cands by auto
     subgoal by simp
     subgoal by (rule clss_to_upd)
     subgoal by (rule past_invs)
     done
qed

definition pcdcl_twl_final_state :: ‹'v twl_st ⇒ bool› where
  ‹pcdcl_twl_final_state S ⟷ no_step cdcl_twl_stgy S ∨
  (count_decided (get_trail S) = 0 ∧ get_conflict S ≠ None)›

end