Theory IsaSAT_Sorting

theory IsaSAT_Sorting
  imports IsaSAT_Setup
begin

chapter ‹Sorting of clauses›

text ‹We use the sort function developped by Peter Lammich.›

definition clause_score_ordering where
  ‹clause_score_ordering = (λ(lbd, act) (lbd', act'). lbd < lbd' ∨ (lbd = lbd' ∧ act < act'))›

definition (in -) clause_score_extract :: ‹arena ⇒ nat ⇒ nat × nat› where
  ‹clause_score_extract arena C = (
     if arena_status arena C = DELETED
     then (uint32_max, 0) ― ‹deleted elements are the
        largest possible›
     else
       let lbd = arena_lbd arena C in
       let act = arena_act arena C in
       (lbd, act)
  )›

definition valid_sort_clause_score_pre_at where
  ‹valid_sort_clause_score_pre_at arena C ⟷
    (∃i vdom. C = vdom ! i ∧ arena_is_valid_clause_vdom arena (vdom!i) ∧
          (arena_status arena (vdom!i) ≠ DELETED ⟶
             (get_clause_LBD_pre arena (vdom!i) ∧ arena_act_pre arena (vdom!i)))
          ∧ i < length vdom)›

definition (in -)valid_sort_clause_score_pre where
  ‹valid_sort_clause_score_pre arena vdom ⟷
    (∀C ∈ set vdom. arena_is_valid_clause_vdom arena C ∧
        (arena_status arena C ≠ DELETED ⟶
             (get_clause_LBD_pre arena C ∧ arena_act_pre arena C)))›


definition clause_score_less :: "arena ⇒ nat ⇒ nat ⇒ bool" where
  "clause_score_less arena i j ⟷
     clause_score_ordering (clause_score_extract arena i) (clause_score_extract arena j)"

definition idx_cdom :: "arena ⇒ nat set" where
 "idx_cdom arena ≡ {i. valid_sort_clause_score_pre_at arena i}"

definition mop_clause_score_less where
  ‹mop_clause_score_less arena i j = do {
    ASSERT(valid_sort_clause_score_pre_at arena i);
    ASSERT(valid_sort_clause_score_pre_at arena j);
    RETURN (clause_score_ordering (clause_score_extract arena i) (clause_score_extract arena j))
  }›

end