Theory TD_Solver_Bridge

theory TD_Solver_Bridge
  imports "TD.TD_side_Interface"
begin

section ‹The semantic boundary between Voblint and the vendored TD solver›

text ‹
  Voblint relies on the vendored TD solver only through the locale below, which
  packages the solver facts the analysis pipeline uses.
›

subsection ‹What a pipeline asks of its solver›

text ‹
  Four facts are everything the analysis pipeline uses about a solver: a solve in
  the solver's domain answers a partial post-solution over finitely many keys, and
  an answer of the executable solver ‹solve_c› places the query in that domain and
  is the solve itself. TD proves all four inside \<^locale>‹TD_side_upd_rule›
  (‹partial_post_solution›, ‹finite_stabl_solve›, ‹solve_dom_of_solve_c›,
  ‹solve_code_equation›).
  ‹certified_solver› names that contract once, over any equation system, so a
  pipeline assumes one locale instead of four facts and a solver discharges it
  once for all of its instances.
›

locale certified_solver =
  fixes solve :: "('x, 'g, 'd::bounded_semilattice_sup_bot) eqsT
                  ⇒ 'x ⇒ 'x set × ('x + 'g ⇒ 'd)"
    and solve_dom :: "('x, 'g, 'd) eqsT ⇒ 'x ⇒ bool"
    and solve_c :: "('x, 'g, 'd) eqsT ⇒ 'x ⇒ ('x set × ('x + 'g ⇒ 'd)) option"
  assumes solve_pp:
      "⋀eqs x. solve_dom eqs x
         ⟹ part_post_solution eqs x (snd (solve eqs x)) (fst (solve eqs x))"
    and solve_fin: "⋀eqs x. solve_dom eqs x ⟹ finite (fst (solve eqs x))"
    and dom_of_solve_c: "⋀eqs x. solve_c eqs x ≠ None ⟹ solve_dom eqs x"
    and solve_of_solve_c: "⋀eqs x sol. solve_c eqs x = Some sol ⟹ solve eqs x = sol"

end