src/HOL/SMT/Tools/z3_model.ML

moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly

(*  Title:      HOL/SMT/Tools/z3_model.ML
    Author:     Sascha Boehme and Philipp Meyer, TU Muenchen

Parser for counterexamples generated by Z3.
*)

signature Z3_MODEL =
sig
  val parse_counterex: SMT_Translate.recon -> string list -> term list
end

structure Z3_Model: Z3_MODEL =
struct

(* parsing primitives *)

fun lift f (x, y) = apsnd (pair x) (f y)
fun lift' f v (x, y) = apsnd (rpair y) (f v x)

fun $$ s = lift (Scan.$$ s)
fun this s = lift (Scan.this_string s)

fun par scan = $$ "(" |-- scan --| $$ ")"

val digit = (fn
  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)

val nat_num = Scan.repeat1 (Scan.some digit) >>
  (fn ds => fold (fn d => fn i => i * 10 + d) ds 0)
val int_num = Scan.optional (Scan.$$ "-" >> K (fn i => ~i)) I :|--
  (fn sign => nat_num >> sign)

val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
val name = Scan.many1 is_char >> implode


(* parsing counterexamples *)

datatype context = Context of {
  ttab: term Symtab.table,
  nctxt: Name.context,
  vtab: term Inttab.table }

fun make_context (ttab, nctxt, vtab) =
  Context {ttab=ttab, nctxt=nctxt, vtab=vtab}

fun empty_context ({terms, ...} : SMT_Translate.recon) =
  let
    val ns = Symtab.fold (Term.add_free_names o snd) terms []
    val nctxt = Name.make_context ns
  in make_context (terms, nctxt, Inttab.empty) end

fun map_context f (Context {ttab, nctxt, vtab}) =
  make_context (f (ttab, nctxt, vtab))

fun fresh_name (cx as Context {nctxt, ...}) =
  let val (n, nctxt') = yield_singleton Name.variants "" nctxt
  in (n, map_context (fn (ttab, _, vtab) => (ttab, nctxt', vtab)) cx) end

fun ident name (cx as Context {ttab, ...}) = 
  (case Symtab.lookup ttab name of
    SOME t => (t, cx)
  | NONE =>
      let val (n, cx') = fresh_name cx
      in (Free (n, Term.dummyT), cx) end)

fun set_value t i = map_context (fn (ttab, nctxt, vtab) =>
  (ttab, nctxt, Inttab.update (i, t) vtab))

fun get_value T i (cx as Context {vtab, ...}) =
  (case Inttab.lookup vtab i of
    SOME t => (t, cx)
  | _ => cx |> fresh_name |-> (fn n =>
      let val t = Free (n, T)
      in set_value t i #> pair t end))


fun space s = lift (Scan.many Symbol.is_ascii_blank) s
fun spaced p = p --| space

val key = spaced (lift name) #-> lift' ident
fun mapping st = spaced (this "->") st
fun in_braces p = spaced ($$ "{") |-- p --| spaced ($$ "}")

fun bool_expr st =
 (this "true" >> K @{term True} ||
  this "false" >> K @{term False}) st

fun number_expr T =
  let
    val num = lift int_num >> HOLogic.mk_number T
    fun frac n d = Const (@{const_name divide}, T --> T --> T) $ n $ d
  in num :|-- (fn n => Scan.optional ($$ "/" |-- num >> frac n) n) end

fun value st = (this "val!" |-- lift nat_num) st
fun value_expr T = value #-> lift' (get_value T)

val domT = Term.domain_type
val ranT = Term.range_type
fun const_array T t = Abs ("x", T, t)
fun upd_array T ((a, t), u) =
  Const (@{const_name fun_upd}, [T, domT T, ranT T] ---> T) $ a $ t $ u
fun array_expr T st = if not (can domT T) then Scan.fail st else st |> (
  par (spaced (this "const") |-- expr (ranT T)) >> const_array (domT T) ||
  par (spaced (this "store") |-- spaced (array_expr T) --
    expr (Term.domain_type T) -- expr (Term.range_type T)) >> upd_array T)

and expr T st =
  spaced (bool_expr || number_expr T || value_expr T || array_expr T) st

fun const_val t =
  let fun rep u = spaced value #-> apfst o set_value u #> pair []
  in
    if can HOLogic.dest_number t then rep t
    else if t = @{term TT} then rep @{term True}
    else expr (Term.fastype_of t) >> (fn u => [HOLogic.mk_eq (t, u)])
  end

fun func_value T = mapping |-- expr T

fun first_pat T =
  let
    fun args T = if not (can domT T) then Scan.succeed [] else
      expr (domT T) ::: args (ranT T)
    fun value ts = func_value (snd (SMT_Translate.dest_funT (length ts) T))
  in args T :-- value end

fun func_pat (Ts, T) = fold_map expr Ts -- func_value T
fun else_pat (Ts, T) =
  let fun else_arg T cx = cx |> fresh_name |>> (fn n => Free (n, T))
  in
    fold_map (lift' else_arg) Ts ##>>
    spaced (this "else") |-- func_value T
  end
fun next_pats T (fts as (ts, _)) =
  let val Tps = SMT_Translate.dest_funT (length ts) T
  in Scan.repeat (func_pat Tps) @@@ (else_pat Tps >> single) >> cons fts end

fun mk_def' f (ts, t) = HOLogic.mk_eq (Term.list_comb (f, ts), t)
fun mk_def (Const (@{const_name apply}, _)) (u :: us, t) = mk_def' u (us, t)
  | mk_def f (ts, t) = mk_def' f (ts, t)
fun func_pats t =
  let val T = Term.fastype_of t
  in first_pat T :|-- next_pats T >> map (mk_def t) end

val assign =
  key --| mapping :|-- (fn t => in_braces (func_pats t) || const_val t)

val cex = space |-- Scan.repeat assign

fun parse_counterex recon ls =
  (empty_context recon, explode (cat_lines ls))
  |> Scan.catch (Scan.finite' Symbol.stopper (Scan.error cex))
  |> flat o fst

end