Theory IsaSAT_VMTF

theory IsaSAT_VMTF
imports Watched_Literals.WB_Sort IsaSAT_Setup Weidenbach_Book_Base.Explorer
begin


chapter ‹VMTF Decision Heuristic›

section ‹Code generation for the VMTF decision heuristic and the trail›
type_synonym (in -) isa_vmtf_remove_int = ‹vmtf × (nat list × bool list)›

definition update_next_search :: ‹nat option ⇒ vmtf ⇒ vmtf› where
  ‹update_next_search L = (λ(ns, m, fst_As, lst_As, next_search).
    ((ns, m, fst_As, lst_As, L)))›

definition vmtf_enqueue_pre where
  ‹vmtf_enqueue_pre =
     (λ((M, L),(ns,m,fst_As,lst_As, next_search)). L < length ns ∧
       (fst_As ≠ None ⟶ the fst_As < length ns) ∧
       (fst_As ≠ None ⟶ lst_As ≠ None) ∧
       m+1 ≤ unat64_max)›

definition isa_vmtf_enqueue :: ‹trail_pol ⇒ nat ⇒ vmtf_option_fst_As ⇒ vmtf nres› where
‹isa_vmtf_enqueue = (λM L (ns, m, fst_As, lst_As, next_search). do {
  ASSERT(defined_atm_pol_pre M L);
  de ← RETURN (defined_atm_pol M L);
  case fst_As of
    None ⇒RETURN ((ns[L := VMTF_Node m fst_As None], m+1, L, L,
            (if de then None else Some L)))
  | Some fst_As ⇒ do {
      let fst_As' = VMTF_Node (stamp (ns!fst_As)) (Some L) (get_next (ns!fst_As));
      RETURN (ns[L := VMTF_Node (m+1) None (Some fst_As), fst_As := fst_As'],
          m+1, L, the lst_As, (if de then next_search else Some L))
   }})›

lemma vmtf_enqueue_alt_def:
  ‹RETURN ooo vmtf_enqueue = (λM L (ns, m, fst_As, lst_As, next_search). do {
    let de = defined_lit M (Pos L);
    case fst_As of
      None ⇒ RETURN (ns[L := VMTF_Node m fst_As None], m+1, L, L,
	   (if de then None else Some L))
    | Some fst_As ⇒
       let fst_As' = VMTF_Node (stamp (ns!fst_As)) (Some L) (get_next (ns!fst_As)) in
       RETURN (ns[L := VMTF_Node (m+1) None (Some fst_As), fst_As := fst_As'],
	    m+1, L, the lst_As, (if de then next_search else Some L))})›
  unfolding vmtf_enqueue_def Let_def
  by (auto intro!: ext split: option.splits)

lemma isa_vmtf_enqueue:
  ‹(uncurry2 isa_vmtf_enqueue, uncurry2 (RETURN ooo vmtf_enqueue)) ∈
     [λ((M, L), _). L ∈# 𝒜]f (trail_pol 𝒜) ×f nat_rel ×f Id → ⟨Id⟩nres_rel›
proof -
  have defined_atm_pol: ‹(defined_atm_pol x1g x2f, defined_lit x1a (Pos x2)) ∈ Id›
    if
      ‹case y of (x, xa) ⇒ (case x of (M, L) ⇒ λ_. L ∈# 𝒜) xa› and
      ‹(x, y) ∈ trail_pol 𝒜 ×f nat_rel ×f Id› and    ‹x1 = (x1a, x2)› and
      ‹x2d = (x1e, x2e)› and
      ‹x2c = (x1d, x2d)› and
      ‹x2b = (x1c, x2c)› and
      ‹x2a = (x1b, x2b)› and
      ‹y = (x1, x2a)› and
      ‹x1f = (x1g, x2f)› and
      ‹x2j = (x1k, x2k)› and
      ‹x2i = (x1j, x2j)› and
      ‹x2h = (x1i, x2i)› and
      ‹x2g = (x1h, x2h)› and
      ‹x = (x1f, x2g)›
     for x y x1 x1a x2 x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x1g x2f x2g x1h x2h
       x1i x2i x1j x2j x1k x2k
  proof -
    have [simp]: ‹defined_lit x1a (Pos x2) ⟷ defined_atm x1a x2›
      using that by (auto simp: in_ℒall_atm_of_𝒜in trail_pol_def defined_atm_def)

    show ?thesis
      using undefined_atm_code[THEN fref_to_Down, unfolded uncurry_def, of 𝒜 ‹(x1a, x2)› ‹(x1g, x2f)›]
      that by (auto simp: in_ℒall_atm_of_𝒜in RETURN_def)
  qed

  show ?thesis
    unfolding isa_vmtf_enqueue_def vmtf_enqueue_alt_def uncurry_def
    apply (intro frefI nres_relI)
    apply (refine_rcg)
    subgoal by (rule defined_atm_pol_pre) auto
    apply (rule defined_atm_pol; assumption)
    apply (rule same_in_Id_option_rel)
    subgoal for x y x1 x1a x2 x2a x1b x2b x1c x2c x1d x2d x1e x2e x1f x1g x2f x2g x1h x2h
	 x1i x2i x1j x2j x1k x2k
      by auto
    subgoal by auto
    subgoal by auto
    done
qed

definition partition_vmtf_nth :: ‹nat_vmtf_node list  ⇒  nat ⇒ nat ⇒ nat list ⇒ (nat list × nat) nres› where
  ‹partition_vmtf_nth ns = partition_main (≤) (λn. stamp (ns ! n))›

definition partition_between_ref_vmtf :: ‹nat_vmtf_node list ⇒  nat ⇒ nat ⇒ nat list ⇒ (nat list × nat) nres› where
  ‹partition_between_ref_vmtf ns = partition_between_ref (≤) (λn. stamp (ns ! n))›

definition quicksort_vmtf_nth :: ‹nat_vmtf_node list × 'c ⇒ nat list ⇒ nat list nres› where
  ‹quicksort_vmtf_nth = (λ(ns, _). full_quicksort_ref (≤) (λn. stamp (ns ! n)))›

definition quicksort_vmtf_nth_ref:: ‹nat_vmtf_node list ⇒ nat ⇒ nat ⇒ nat list ⇒ nat list nres› where
  ‹quicksort_vmtf_nth_ref ns a b c =
     quicksort_ref (≤) (λn. stamp (ns ! n)) (a, b, c)›

lemma (in -) partition_vmtf_nth_code_helper:
  assumes ‹∀x∈set ba. x < length a›  and
      ‹b < length ba› and
     mset: ‹mset ba = mset a2'›  and
      ‹a1' < length a2'›
  shows ‹a2' ! b < length a›
  using nth_mem[of b a2'] mset_eq_setD[OF mset] mset_eq_length[OF mset] assms
  by (auto simp del: nth_mem)



lemma partition_vmtf_nth_code_helper3:
  ‹∀x∈set b. x < length a ⟹
       x'e < length a2' ⟹
       mset a2' = mset b ⟹
       a2' ! x'e < length a›
  using mset_eq_setD nth_mem by blast

definition (in -) isa_vmtf_en_dequeue :: ‹trail_pol ⇒ nat ⇒ vmtf ⇒ vmtf nres› where
‹isa_vmtf_en_dequeue = (λM L vm. isa_vmtf_enqueue M L (vmtf_dequeue L vm))›

lemma isa_vmtf_en_dequeue:
  ‹(uncurry2 isa_vmtf_en_dequeue, uncurry2 (RETURN ooo vmtf_en_dequeue)) ∈
     [λ((M, L), _). L ∈# 𝒜]f (trail_pol 𝒜) ×f nat_rel ×f Id → ⟨Id⟩nres_rel›
  unfolding isa_vmtf_en_dequeue_def vmtf_en_dequeue_def uncurry_def
  apply (intro frefI nres_relI)
  apply clarify
  subgoal for a aa ab ac ad b zeroed ba ae af ag ah bb ai bc aj ak al am bd
    by (rule order.trans,
      rule isa_vmtf_enqueue[of 𝒜, THEN fref_to_Down_curry2,
        of ai bc ‹vmtf_dequeue bc (aj, ak, al, am, bd)›])
      auto
  done

definition isa_vmtf_en_dequeue_pre :: ‹(trail_pol × nat) × vmtf ⇒ bool› where
  ‹isa_vmtf_en_dequeue_pre = (λ((M, L),(ns,m,fst_As, lst_As, next_search)).
       L < length ns ∧ vmtf_dequeue_pre (L, ns) ∧
       fst_As < length ns ∧ (get_next (ns ! fst_As) ≠ None ⟶ get_prev (ns ! lst_As) ≠ None) ∧
       (get_next (ns ! fst_As) = None ⟶ fst_As = lst_As) ∧
       m+1 ≤ unat64_max)›

lemma isa_vmtf_en_dequeue_preD:
  assumes ‹isa_vmtf_en_dequeue_pre ((M, ah), a, aa, ab, ac, b)›
  shows ‹ah < length a› and ‹vmtf_dequeue_pre (ah, a)›
  using assms by (auto simp: isa_vmtf_en_dequeue_pre_def)


lemma isa_vmtf_en_dequeue_pre_vmtf_enqueue_pre:
   ‹isa_vmtf_en_dequeue_pre ((M, L), a, st, fst_As, lst_As, next_search) ⟹
       vmtf_enqueue_pre ((M, L), vmtf_dequeue L (a, st, fst_As, lst_As, next_search))›
  unfolding vmtf_enqueue_pre_def
  apply clarify
  apply (intro conjI)
  subgoal
    by (auto simp: vmtf_dequeue_pre_def vmtf_enqueue_pre_def vmtf_dequeue_def
        ns_vmtf_dequeue_def Let_def isa_vmtf_en_dequeue_pre_def split: option.splits)[]
  subgoal
    by (auto simp: vmtf_dequeue_pre_def vmtf_enqueue_pre_def vmtf_dequeue_def
          isa_vmtf_en_dequeue_pre_def split: option.splits if_splits)[]
  subgoal
    by (auto simp: vmtf_dequeue_pre_def vmtf_enqueue_pre_def vmtf_dequeue_def
        Let_def isa_vmtf_en_dequeue_pre_def split: option.splits if_splits)[]
  subgoal
    by (auto simp: vmtf_dequeue_pre_def vmtf_enqueue_pre_def vmtf_dequeue_def
        Let_def isa_vmtf_en_dequeue_pre_def split: option.splits if_splits)[]
  done

lemma insert_sort_reorder_list:
  assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
  shows ‹(full_quicksort_ref R h, reorder_list vm) ∈ ⟨Id⟩list_rel →f ⟨Id⟩ nres_rel›
proof -
  show ?thesis
    apply (intro frefI nres_relI)
    apply (rule full_quicksort_ref_full_quicksort[THEN fref_to_Down, THEN order_trans])
    using assms apply fast
    using assms apply fast
    apply fast
     apply assumption
    using assms
    apply (auto 5 5 simp: reorder_list_def intro!: full_quicksort_correct[THEN order_trans])
    done
qed

lemma quicksort_vmtf_nth_reorder:
   ‹(uncurry quicksort_vmtf_nth, uncurry reorder_list) ∈
      Id ×r ⟨Id⟩list_rel →f ⟨Id⟩ nres_rel›
  apply (intro frefI nres_relI)
  subgoal for x y
    using insert_sort_reorder_list[unfolded fref_def nres_rel_def, of
     ‹(≤)› ‹(λn. stamp (fst (fst y) ! n) :: nat)› ‹fst y›]
    by (cases x, cases y)
      (fastforce simp: quicksort_vmtf_nth_def uncurry_def fref_def)
  done

lemma atoms_hash_del_op_set_delete:
  ‹(uncurry (RETURN oo atoms_hash_del),
    uncurry (RETURN oo Set.remove)) ∈
     nat_rel ×r atoms_hash_rel 𝒜 →f ⟨atoms_hash_rel 𝒜⟩nres_rel›
  by (intro frefI nres_relI)
    (force simp: atoms_hash_del_def atoms_hash_rel_def)


definition current_stamp where
  ‹current_stamp vm  = fst (snd vm)›

lemma current_stamp_alt_def:
  ‹current_stamp = (λ(_, m, _). m)›
  by (auto simp: current_stamp_def intro!: ext)

lemma vmtf_rescale_alt_def:
‹vmtf_rescale = (λ(ns, m, fst_As, lst_As :: nat, next_search). do {
    (ns, m, _) ← WHILET⇗λ_. True⇖
      (λ(ns, n, lst_As). lst_As ≠None)
      (λ(ns, n, a). do {
         ASSERT(a ≠ None);
         ASSERT(n+1 ≤ unat32_max);
         ASSERT(the a < length ns);
         let m = the a;
         let c = ns ! m;
         let nc = get_next c;
         let pc = get_prev c;
         RETURN (ns[m := VMTF_Node n pc nc], n + 1, pc)
      })
      (ns, 0, Some lst_As);
    RETURN ((ns, m, fst_As, lst_As, next_search))
  })›
  unfolding update_stamp.simps Let_def vmtf_rescale_def by auto

definition vmtf_reorder_list_raw where
  ‹vmtf_reorder_list_raw = (λvm to_remove. do {
    ASSERT(∀x∈set to_remove. x < length vm);
    reorder_list vm to_remove
  })›


definition vmtf_reorder_list :: ‹vmtf ⇒ nat list ⇒ nat list nres› where
  ‹vmtf_reorder_list = (λ(vm, _) to_remove. do {
    vmtf_reorder_list_raw vm to_remove
  })›

definition isa_vmtf_flush_int :: ‹trail_pol ⇒ vmtf ⇒ _ ⇒ (vmtf × _) nres› where
‹isa_vmtf_flush_int  = (λM vm (to_remove, h). do {
    ASSERT(∀x∈set to_remove. x < length (fst vm));
    ASSERT(length to_remove ≤ unat32_max);
    to_remove' ← vmtf_reorder_list vm to_remove;
    ASSERT(length to_remove' ≤ unat32_max);
    vm ← (if length to_remove' ≥ unat64_max - fst (snd vm)
      then vmtf_rescale vm else RETURN vm);
    ASSERT(length to_remove' + fst (snd vm) ≤ unat64_max);
    (_, vm, h) ← WHILET⇗λ(i, vm', h). i ≤ length to_remove' ∧ fst (snd vm') = i + fst (snd vm) ∧
          (i < length to_remove' ⟶ isa_vmtf_en_dequeue_pre ((M, to_remove'!i), vm'))⇖
      (λ(i, vm, h). i < length to_remove')
      (λ(i, vm, h). do {
         ASSERT(i < length to_remove');
	 ASSERT(isa_vmtf_en_dequeue_pre ((M, to_remove'!i), vm));
         vm ← isa_vmtf_en_dequeue M (to_remove'!i) vm;
	 ASSERT(atoms_hash_del_pre (to_remove'!i) h);
         RETURN (i+1, vm, atoms_hash_del (to_remove'!i) h)})
      (0, vm, h);
    RETURN (vm, (emptied_list to_remove', h))
  })›


lemma isa_vmtf_flush_int:
  ‹(uncurry2 isa_vmtf_flush_int, uncurry2 (vmtf_flush_int 𝒜)) ∈ trail_pol (𝒜::nat multiset) ×f Id ×f Id →f ⟨Id×f Id⟩nres_rel›
proof -
  have vmtf_flush_int_alt_def:
    ‹vmtf_flush_int 𝒜in = (λM vm (to_remove, h). do {
      ASSERT(∀x∈set to_remove. x < length (fst vm));
      ASSERT(length to_remove ≤ unat32_max);
      to_remove' ← reorder_list vm to_remove;
      ASSERT(length to_remove' ≤ unat32_max);
      vm ← (if length to_remove' + fst (snd vm) ≥ unat64_max
	then vmtf_rescale vm else RETURN vm);
      ASSERT(length to_remove' + fst (snd vm) ≤ unat64_max);
      (_, vm, h) ← WHILET⇗λ(i, vm', h). i ≤ length to_remove' ∧ fst (snd vm') = i + fst (snd vm) ∧
	    (i < length to_remove' ⟶ vmtf_en_dequeue_pre 𝒜in ((M, to_remove'!i), vm'))⇖
	(λ(i, vm, h). i < length to_remove')
	(λ(i, vm, h). do {
	   ASSERT(i < length to_remove');
	   ASSERT(to_remove'!i ∈# 𝒜in);
	   ASSERT(atoms_hash_del_pre (to_remove'!i) h);
	   vm ← RETURN(vmtf_en_dequeue M (to_remove'!i) vm);
	   RETURN (i+1, vm, atoms_hash_del (to_remove'!i) h)})
	(0, vm, h);
      RETURN (vm, (emptied_list to_remove', h))
    })› for 𝒜in
    unfolding vmtf_flush_int_def
    by auto

  have reorder_list: ‹vmtf_reorder_list x2c x1e
    ≤ ⇓ Id
    (reorder_list x2 x1b)›
    if
      ‹(x, y) ∈ trail_pol 𝒜 ×f Id ×f Id› and
      ‹x1 = (x1a, x2)› and
      ‹x2a = (x1b, x2b)› and
      ‹y = (x1, x2a)› and
      ‹x1c = (x1d, x2c)› and
      ‹x2d = (x1e, x2e)› and
      ‹x = (x1c, x2d)› and
      ‹∀x∈set x1b. x < length (fst x2)› and
      ‹length x1b ≤ unat32_max› and
      ‹∀x∈set x1e. x < length (fst x2c)› and
      ‹length x1e ≤ unat32_max›
    for x y x1 x1a x2 x2a x1b x2b x1c x1d x2c x2d x1e x2e
    using that unfolding vmtf_reorder_list_def by (cases x2)
      (auto intro!: ASSERT_leI simp: reorder_list_def vmtf_reorder_list_raw_def)

  have vmtf_rescale: ‹vmtf_rescale x2c
      ≤ ⇓ Id
          (vmtf_rescale x2)›
    if
      ‹(x, y) ∈ trail_pol 𝒜 ×f Id ×f Id› and
      ‹x1 = (x1a, x2)› and
      ‹x2a = (x1b, x2b)› and
      ‹y = (x1, x2a)› and
      ‹x1c = (x1d, x2c)› and
      ‹x2d = (x1e, x2e)› and
      ‹x = (x1c, x2d)› and
      ‹∀x∈set x1b. x < length (fst x2)› and
      ‹length x1b ≤ unat32_max› and
      ‹∀x∈set x1e. x < length (fst x2c)› and
      ‹length x1e ≤ unat32_max› and
      ‹(to_remove', to_remove'a) ∈ Id› and
      ‹length to_remove'a ≤ unat32_max› and
      ‹length to_remove' ≤ unat32_max› and
      ‹unat64_max - fst (snd x2c) ≤ length to_remove'› and
      ‹unat64_max ≤ length to_remove'a + fst (snd x2)›
    for x y x1 x1a x2 x2a x1b x2b x1c x1d x2c x2d x1e x2e
      to_remove' to_remove'a
    using that by auto
  have loop_rel: ‹((0, vm, x2e), 0, vma, x2b)
      ∈ Id›
    if 
      True and
      ‹(x, y) ∈ trail_pol 𝒜 ×f Id ×f Id› and
      ‹x1 = (x1a, x2)› and
      ‹x2a = (x1b, x2b)› and
      ‹y = (x1, x2a)› and
      ‹x1c = (x1d, x2c)› and
      ‹x2d = (x1e, x2e)› and
      ‹x = (x1c, x2d)› and
      ‹∀x∈set x1b. x < length (fst x2)› and
      ‹length x1b ≤ unat32_max› and
      ‹∀x∈set x1e. x < length (fst x2c)› and
      ‹length x1e ≤ unat32_max› and
      ‹(to_remove', to_remove'a) ∈ Id› and
      ‹length to_remove'a ≤ unat32_max› and
      ‹length to_remove' ≤ unat32_max› and
      ‹(vm, vma) ∈ Id› and
      ‹length to_remove'a + fst (snd vma) ≤ unat64_max› and
      ‹length to_remove' + fst (snd vm) ≤ unat64_max› and
      ‹case (0, vma, x2b) of
     (i, vm', h) ⇒
       i ≤ length to_remove'a ∧
       fst (snd vm') = i + fst (snd vma) ∧
       (i < length to_remove'a ⟶
        vmtf_en_dequeue_pre 𝒜 ((x1a, to_remove'a ! i), vm'))›
    for x y x1 x1a x2 x2a x1b x2b x1c x1d x2c x2d x1e x2e
      to_remove' to_remove'a vm vma
    using that by auto

  have isa_vmtf_en_dequeue_pre:
    ‹vmtf_en_dequeue_pre 𝒜 ((M, L), x) ⟹ isa_vmtf_en_dequeue_pre ((M', L), x)› for x M M' L
    unfolding vmtf_en_dequeue_pre_def isa_vmtf_en_dequeue_pre_def
    by auto

  have isa_vmtf_en_dequeue:
    ‹isa_vmtf_en_dequeue x1d (to_remove' ! x1h) x1i
      ≤ Refine_Basic.SPEC
          (λc. (c, vmtf_en_dequeue x1a (to_remove'a ! x1f) x1g)
               ∈ Id)›
    if
      ‹(x, y) ∈ trail_pol 𝒜 ×f Id ×f Id› and
      ‹x1 = (x1a, x2)› and
      ‹x2a = (x1b, x2b)› and
      ‹y = (x1, x2a)› and
      ‹x1c = (x1d, x2c)› and
      ‹x2d = (x1e, x2e)› and
      ‹x = (x1c, x2d)› and
      ‹∀x∈set x1b. x < length (fst x2)› and
      ‹length x1b ≤ unat32_max› and
      ‹∀x∈set x1e. x < length (fst x2c)› and
      ‹length x1e ≤ unat32_max› and
      ‹(to_remove', to_remove'a) ∈ Id› and
      ‹length to_remove'a ≤ unat32_max› and
      ‹length to_remove' ≤ unat32_max› and
      ‹(vm, vma) ∈ Id› and
      ‹length to_remove'a + fst (snd vma) ≤ unat64_max› and
      ‹length to_remove' + fst (snd vm) ≤ unat64_max› and
      ‹(xa, x') ∈ Id› and
      ‹case xa of (i, vm, h) ⇒ i < length to_remove'› and
      ‹case x' of (i, vm, h) ⇒ i < length to_remove'a› and
      ‹case xa of
     (i, vm', h) ⇒
       i ≤ length to_remove' ∧
       fst (snd vm') = i + fst (snd vm) ∧
       (i < length to_remove' ⟶
        isa_vmtf_en_dequeue_pre ((x1d, to_remove' ! i), vm'))› and
      ‹case x' of
     (i, vm', h) ⇒
       i ≤ length to_remove'a ∧
       fst (snd vm') = i + fst (snd vma) ∧
       (i < length to_remove'a ⟶
        vmtf_en_dequeue_pre 𝒜 ((x1a, to_remove'a ! i), vm'))› and
      ‹x2f = (x1g, x2g)› and
      ‹x' = (x1f, x2f)› and
      ‹x2h = (x1i, x2i)› and
      ‹xa = (x1h, x2h)› and
      ‹x1f < length to_remove'a› and
      ‹to_remove'a ! x1f ∈# 𝒜› and
      ‹atoms_hash_del_pre (to_remove'a ! x1f) x2g› and
      ‹x1h < length to_remove'› and
      ‹isa_vmtf_en_dequeue_pre ((x1d, to_remove' ! x1h), x1i)›
    for x y x1 x1a x2 x2a x1b x2b x1c x1d x2c x2d x1e
      x2e to_remove' to_remove'a vm vma xa x' x1f x2f x1g
      x2g x1h x2h x1i x2i
    using isa_vmtf_en_dequeue[of 𝒜, THEN fref_to_Down_curry2, of x1a ‹to_remove'a ! x1f› x1g
        x1d ‹to_remove' ! x1h› x1i] that
    by (auto simp: RETURN_def)

  show ?thesis
   unfolding isa_vmtf_flush_int_def uncurry_def vmtf_flush_int_alt_def
    apply (intro frefI nres_relI)
    apply (refine_rcg)
    subgoal
      by auto
    subgoal
      by auto
      apply (rule reorder_list; assumption)
    subgoal
      by auto
    subgoal
      by auto
    apply (rule vmtf_rescale; assumption)
    subgoal
      by auto
    subgoal
      by auto
    apply (rule loop_rel; assumption)
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by (auto intro!: isa_vmtf_en_dequeue_pre)
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    apply (rule isa_vmtf_en_dequeue; assumption)
    subgoal for x y x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e to_remove' to_remove'a vm
       vma xa x' x1f x2f x1g x2g x1h x2h x1i x2i vmb vmc
      by auto
    subgoal
      by auto
    subgoal
      by auto
    done
qed

lemma bounded_included_le:
   assumes bounded: ‹isasat_input_bounded 𝒜› and ‹distinct n› and
   ‹set n ⊆ set_mset 𝒜 ›
  shows ‹length n < unat32_max›  ‹length n ≤ 1 + unat32_max div 2›
proof -
  have lits: ‹literals_are_in_ℒin 𝒜 (Pos `# mset n)› and
    dist: ‹distinct n›
    using assms
    by (auto simp: literals_are_in_ℒin_alt_def distinct_atoms_rel_alt_def inj_on_def atms_of_ℒall_𝒜in)
   have dist: ‹distinct_mset (Pos `# mset n)›
    by (subst distinct_image_mset_inj)
      (use dist in ‹auto simp: inj_on_def›)
  have tauto: ‹¬ tautology (poss (mset n))›
    by (auto simp: tautology_decomp)

  show ‹length n < unat32_max›  ‹length n ≤ 1 + unat32_max div 2›
    using simple_clss_size_upper_div2[OF bounded lits dist tauto]
    by (auto simp: unat32_max_def)
qed


lemma atms_hash_insert_pre:
  assumes ‹L ∈# 𝒜› and ‹(x, x') ∈ distinct_atoms_rel 𝒜› and ‹isasat_input_bounded 𝒜›
  shows ‹atms_hash_insert_pre L x›
  using assms bounded_included_le[OF assms(3), of ‹L # fst x›]
  by (auto simp:  atoms_hash_insert_def atoms_hash_rel_def distinct_atoms_rel_alt_def
     atms_hash_insert_pre_def)


lemma atoms_hash_del_op_set_insert:
  ‹(uncurry (RETURN oo atoms_hash_insert), uncurry (RETURN oo insert)) ∈
     [λ(i, xs). i ∈# 𝒜in ∧ isasat_input_bounded 𝒜]f
     nat_rel ×r distinct_atoms_rel 𝒜in → ⟨distinct_atoms_rel 𝒜in⟩nres_rel›
  by (intro frefI nres_relI)
    (auto simp: atoms_hash_insert_def atoms_hash_rel_def distinct_atoms_rel_alt_def intro!: ASSERT_leI)


definition (in -) atoms_hash_set_member where
‹atoms_hash_set_member i xs =  do {ASSERT(i < length xs); RETURN (xs ! i)}›


definition isa_vmtf_mark_to_rescore
  :: ‹nat ⇒ vmtf ⇒ _ ⇒ isa_vmtf_remove_int›
where
  ‹isa_vmtf_mark_to_rescore L = (λ(ns, m, fst_As, next_search) to_remove.
     ((ns, m, fst_As, next_search), atoms_hash_insert L to_remove))›

definition isa_vmtf_mark_to_rescore_pre where
  ‹isa_vmtf_mark_to_rescore_pre = (λL ((ns, m, fst_As, next_search), to_remove).
     atms_hash_insert_pre L to_remove)›

lemma size_conflict_int_size_conflict:
  ‹(RETURN o size_conflict_int, RETURN o size_conflict) ∈ [λD. D ≠ None]f option_lookup_clause_rel 𝒜 →
     ⟨nat_rel⟩nres_rel›
  by (intro frefI nres_relI)
    (auto simp: size_conflict_int_def size_conflict_def option_lookup_clause_rel_def
      lookup_clause_rel_def)

definition rescore_clause
  :: ‹nat multiset ⇒ nat clause_l ⇒ (nat,nat)ann_lits ⇒ vmtf ⇒
    vmtf nres›
where
  ‹rescore_clause 𝒜 C M vm = SPEC (λ(vm'). vm' ∈ vmtf 𝒜 M)›


lemma isa_vmtf_unset_vmtf_unset:
  ‹(uncurry (RETURN oo isa_vmtf_unset), uncurry (RETURN oo vmtf_unset)) ∈
     nat_rel ×f (Id) →f
     ⟨(Id)⟩nres_rel›
  unfolding vmtf_unset_def isa_vmtf_unset_def uncurry_def
  by (intro frefI nres_relI) auto

lemma isa_vmtf_unset_isa_vmtf:
  assumes ‹vm ∈ vmtf 𝒜 M› and ‹L ∈# 𝒜›
  shows ‹isa_vmtf_unset L vm ∈ vmtf 𝒜 M›
proof -
  obtain vm0 to_remove to_remove' where
    vm: ‹vm = (vm0, to_remove)› and
    vm0: ‹(vm0, to_remove') ∈ vmtf 𝒜 M›
    using assms by (cases vm) (auto simp:)

  then show ?thesis
    using assms
      isa_vmtf_unset_vmtf_unset[THEN fref_to_Down_unRET_uncurry, of L vm L vm]
    using
      abs_vmtf_ns_unset_vmtf_unset[of ‹fst vm› ‹fst (snd vm)›  ‹fst (snd (snd vm))›
         ‹fst (snd (snd (snd vm)))› ‹snd (snd (snd (snd vm)))› 𝒜 M L]
    by (auto simp: vm atms_of_ℒall_𝒜in intro: elim!: prod_relE)
qed

lemma isa_vmtf_tl_isa_vmtf:
  assumes ‹vm ∈ vmtf 𝒜 M› and ‹M ≠ []› and ‹lit_of (hd M) ∈# ℒall 𝒜› and
    ‹L = (atm_of (lit_of (hd M)))›
  shows ‹isa_vmtf_unset L vm ∈ vmtf 𝒜 (tl M)›
proof -
  let ?L = ‹atm_of (lit_of (hd M))›
  obtain vm0 to_remove to_remove' where
    vm: ‹vm = (vm0, to_remove)› and
    vm0: ‹(vm0, to_remove') ∈ vmtf 𝒜 M›
    using assms by (cases vm) (auto simp:)

  then show ?thesis
    using assms
      isa_vmtf_unset_vmtf_unset[THEN fref_to_Down_unRET_uncurry, of ?L vm ?L vm]
    using vmtf_unset_vmtf_tl[of ‹fst vm› ‹fst (snd vm)›  ‹fst (snd (snd vm))›
         ‹fst (snd (snd (snd vm)))› ‹snd (snd (snd (snd vm)))› 𝒜 M]
    by (cases M)
     (auto simp: vm atms_of_ℒall_𝒜in in_ℒall_atm_of_𝒜in elim!: prod_relE)
qed

definition isa_vmtf_find_next_undef :: ‹vmtf ⇒ trail_pol ⇒ (nat option) nres› where
‹isa_vmtf_find_next_undef = (λ(ns, m, fst_As, lst_As, next_search) M. do {
    WHILET⇗λnext_search. next_search ≠ None ⟶ defined_atm_pol_pre M (the next_search)⇖
      (λnext_search. next_search ≠ None ∧ defined_atm_pol M (the next_search))
      (λnext_search. do {
         ASSERT(next_search ≠ None);
         let n = the next_search;
         ASSERT (n < length ns);
         RETURN (get_next (ns!n))
        }
      )
      next_search
  })›


lemma isa_vmtf_find_next_undef_vmtf_find_next_undef:
  ‹(uncurry isa_vmtf_find_next_undef, uncurry (vmtf_find_next_undef 𝒜)) ∈
      Id ×r trail_pol 𝒜  →f ⟨⟨nat_rel⟩option_rel⟩nres_rel ›
  unfolding isa_vmtf_find_next_undef_def vmtf_find_next_undef_def uncurry_def
    defined_atm_def[symmetric]
  apply (intro frefI nres_relI)
  apply refine_rcg
  subgoal by auto
  subgoal by (rule defined_atm_pol_pre) (auto simp: in_ℒall_atm_of_𝒜in)
  subgoal
    by (auto simp: undefined_atm_code[THEN fref_to_Down_unRET_uncurry_Id])
  subgoal by auto
  subgoal by auto
  subgoal by auto
  done


end