Theory IsaSAT_Options

theory IsaSAT_Options
imports IsaSAT_Literals
begin

section ‹Options›

text ‹We define the options from our SAT solver. Using options has several advantages: it is much
  easier to change the value (instead of recompiling everything from scratch the complete Isabelle
  development) and it is easier to change.

  We hide the options inside a datatype to make sure Isabelle does not split the the component to
  make goals even less readable.
›

subsection ‹Definition›

type_synonym opts_target = ‹3 word›

datatype opts =
  IsaOptions (opts_restart: bool)
  (opts_reduce: bool)
  (opts_unbounded_mode: bool)
  (opts_minimum_between_restart: ‹64 word›)
  (opts_restart_coeff1: ‹64 word›)
  (opts_restart_coeff2: nat)
  (opts_target: ‹opts_target›)
  (opts_fema: ‹64 word›)
  (opts_sema: ‹64 word›)
  (opts_GC_units_lim: ‹64 word›)
  (opts_subsumption: bool)


definition TARGET_NEVER :: ‹opts_target› where
  ‹TARGET_NEVER = 0›

definition TARGET_STABLE_ONLY :: ‹opts_target› where
  ‹TARGET_STABLE_ONLY = 1›

definition TARGET_ALWAYS :: ‹opts_target› where
  ‹TARGET_ALWAYS = 2›


subsection ‹Refinement›

type_synonym opts_ref =
  ‹bool × bool × bool × 64 word × 64 word × nat × opts_target × 64 word × 64 word × 64 word × bool›

definition opts_rel :: ‹(opts_ref × opts) set› where
  ‹opts_rel = {(S, T). S = (opts_restart T, opts_reduce T, opts_unbounded_mode T,
      opts_minimum_between_restart T, opts_restart_coeff1 T, opts_restart_coeff2 T,
    opts_target T, opts_fema T, opts_sema T, opts_GC_units_lim T, opts_subsumption T)}›

fun opts_rel_restart :: ‹opts_ref ⇒ bool› where
  ‹opts_rel_restart (res, red, unbd, mini, res1, res2) = res›

lemma opts_rel_restart:
  ‹(opts_rel_restart, opts_restart) ∈ opts_rel → bool_rel›
  by (auto simp: opts_rel_def intro!: frefI)

fun opts_rel_reduce :: ‹opts_ref ⇒ bool› where
  ‹opts_rel_reduce (res, red, unbd, mini, res1, res2) = red›

lemma opts_rel_reduce:
  ‹(opts_rel_reduce, opts_reduce) ∈ opts_rel → bool_rel›
  by (auto simp: opts_rel_def intro!: frefI)

fun opts_rel_unbounded_mode :: ‹opts_ref ⇒ bool› where
  ‹opts_rel_unbounded_mode (res, red, unbd, mini, res1, res2) = unbd›

lemma opts_rel_unbounded_mode:
  ‹(opts_rel_unbounded_mode, opts_unbounded_mode) ∈ opts_rel → bool_rel›
  by (auto simp: opts_rel_def intro!: frefI)

fun opts_rel_miminum_between_restart :: ‹opts_ref ⇒ 64 word› where
  ‹opts_rel_miminum_between_restart (res, red, unbd, mini, res1, res2) = mini›

lemma opts_rel_miminum_between_restart:
  ‹(opts_rel_miminum_between_restart, opts_minimum_between_restart) ∈ opts_rel → Id›
  by (auto simp: opts_rel_def intro!: frefI)

fun opts_rel_restart_coeff1 :: ‹opts_ref ⇒ 64 word› where
  ‹opts_rel_restart_coeff1 (res, red, unbd, mini, res1, res2) = res1›

lemma opts_rel_restart_coeff1:
  ‹(opts_rel_restart_coeff1, opts_restart_coeff1) ∈ opts_rel → Id›
  by (auto simp: opts_rel_def intro!: frefI)

fun opts_rel_restart_coeff2 :: ‹opts_ref ⇒ nat› where
  ‹opts_rel_restart_coeff2 (res, red, unbd, mini, res1, res2, target) = res2›

lemma opts_rel_restart_coeff2:
  ‹(opts_rel_restart_coeff2, opts_restart_coeff2) ∈ opts_rel → Id›
  by (auto simp: opts_rel_def intro!: frefI)

fun opts_rel_target :: ‹opts_ref ⇒ 3 word› where
  ‹opts_rel_target (res, red, unbd, mini, res1, res2, target, fema, sema) = target›

lemma opts_rel_target:
  ‹(opts_rel_target, opts_target) ∈ opts_rel → Id›
  by (auto simp: opts_rel_def intro!: frefI)

fun opts_rel_fema :: ‹opts_ref ⇒ 64 word› where
  ‹opts_rel_fema (res, red, unbd, mini, res1, res2, target, fema, sema) = fema›

lemma opts_rel_fema:
  ‹(opts_rel_fema, opts_fema) ∈ opts_rel → Id›
  by (auto simp: opts_rel_def intro!: frefI)

fun opts_rel_sema :: ‹opts_ref ⇒ 64 word› where
  ‹opts_rel_sema (res, red, unbd, mini, res1, res2, target, fema, sema, units) = sema›
lemma opts_rel_sema:
  ‹(opts_rel_sema, opts_sema) ∈ opts_rel → Id›
  by (auto simp: opts_rel_def intro!: frefI)

fun opts_rel_GC_units_lim :: ‹opts_ref ⇒ 64 word› where
  ‹opts_rel_GC_units_lim (res, red, unbd, mini, res1, res2, target, fema, sema, units,_) = units›

fun opts_rel_subsumption :: ‹opts_ref ⇒ bool› where
  ‹opts_rel_subsumption (res, red, unbd, mini, res1, res2, target, fema, sema, units,subsume) = subsume›

lemma opts_GC_units_lim:
  ‹(opts_rel_GC_units_lim, opts_GC_units_lim) ∈ opts_rel → Id› and
  opts_subsumption:
  ‹(opts_rel_subsumption, opts_subsumption) ∈ opts_rel → Id›
  by (auto simp: opts_rel_def opts_GC_units_lim_def intro!: frefI)

lemma opts_rel_alt_defs:
  ‹RETURN o opts_rel_restart = (λ(res, red, unbd, mini, res1, res2). RETURN res)›
  ‹RETURN o opts_rel_reduce = (λ(res, red, unbd, mini, res1, res2). RETURN red)›
  ‹RETURN o opts_rel_unbounded_mode = (λ(res, red, unbd, mini, res1, res2). RETURN unbd)›
  ‹RETURN o opts_rel_miminum_between_restart = (λ(res, red, unbd, mini, res1, res2). RETURN mini)›
  ‹RETURN o opts_rel_restart_coeff1 = (λ(res, red, unbd, mini, res1, res2). RETURN res1)›
  ‹RETURN o opts_rel_restart_coeff2 = (λ(res, red, unbd, mini, res1, res2, _). RETURN res2)›
  ‹RETURN o opts_rel_target = (λ(res, red, unbd, mini, res1, res2, target, fema, semax). RETURN target)›
  ‹RETURN o opts_rel_fema = (λ(res, red, unbd, mini, res1, res2, target, fema, sema). RETURN fema)›
  ‹RETURN o opts_rel_sema = (λ(res, red, unbd, mini, res1, res2, target, fema, sema, units). RETURN sema)›
  ‹RETURN o opts_rel_GC_units_lim = (λ(res, red, unbd, mini, res1, res2, target, fema, sema, units, subsume). RETURN units)›
  ‹RETURN o opts_rel_subsumption = (λ(res, red, unbd, mini, res1, res2, target, fema, sema, units, subsume). RETURN subsume)›
  by (auto intro!: ext)

end