Theory IsaSAT_Sorting

theory IsaSAT_Sorting
  imports IsaSAT_Setup
begin

chapter ‹Sorting of clauses›

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

text ‹
For the ordering, we prefer low lbds. If equal we take lower size. Then for tie, clauses 
derived later are preferred because they are not redundant. The last condition ensures that we do not
depend on the order of the clauses in the array.
›
definition clause_score_ordering where
  ‹clause_score_ordering = (λ(lbd, size, idx) (lbd', size', idx'). lbd < lbd' ∨ (lbd = lbd' ∧ (size < size' ∨ (size = size' ∧ idx > idx'))))›

definition (in -) clause_score_extract :: ‹arena ⇒ nat ⇒ nat × nat × nat› where
  ‹clause_score_extract arena C = (
     if arena_status arena C = DELETED
     then (unat32_max, snat64_max, snat64_max) ― ‹deleted elements are the
        largest possible›
     else
       let lbd = arena_lbd arena C;
           len = arena_length arena C in
       (lbd, len, C)
  )›

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