(*  Title:      HOL/Tools/SMT/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

 (* counterexample expressions *)

 datatype expr = True | False | Number of int * int option | Value of int |

   Array of array

 and array = Fresh of expr | Store of (array * expr) * expr

 (* parsing *)

 val space = Scan.many Symbol.is_ascii_blank

 fun in_parens p = Scan.$$ "(" |-- p --| Scan.$$ ")"

 fun in_braces p = (space -- Scan.$$ "{") |-- p --| (space -- 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 ($$ "-" >> 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

 fun array_expr st = st |>

   in_parens (space |-- (

   Scan.this_string "const" |-- expr >> Fresh ||

   Scan.this_string "store" -- space |-- array_expr -- expr -- expr >> Store))

 and expr st = st |> (space |-- (

   Scan.this_string "true" >> K True ||

   Scan.this_string "false" >> K False ||

   int_num -- Scan.option (Scan.$$ "/" |-- int_num) >> Number ||

   Scan.this_string "val!" |-- nat_num >> Value ||

   array_expr >> Array))

 val mapping = space -- Scan.this_string "->"

 val value = mapping |-- expr

 val args_case = Scan.repeat expr -- value

 val else_case = space -- Scan.this_string "else" |-- value >>

   pair ([] : expr list)

 val func =

   let fun cases st = (else_case >> single || args_case ::: cases) st

   in in_braces cases end

 val cex = space |-- Scan.repeat (space |-- name --| mapping --

   (func || expr >> (single o pair [])))

 fun read_cex ls =

   explode (cat_lines ls)

   |> try (fst o Scan.finite Symbol.stopper cex)

   |> the_default []

 (* translation into terms *)

 fun lookup_term tab (name, e) = Option.map (rpair e) (Symtab.lookup tab name)

 fun with_name_context tab f xs =

   let

     val ns = Symtab.fold (Term.add_free_names o snd) tab []

     val nctxt = Name.make_context ns

   in fst (fold_map f xs (Inttab.empty, nctxt)) end

 fun fresh_term T (tab, nctxt) =

   let val (n, nctxt') = yield_singleton Name.variants "" nctxt

   in (Free (n, T), (tab, nctxt')) end

 fun term_of_value T i (cx as (tab, _)) =

   (case Inttab.lookup tab i of

     SOME t => (t, cx)

   | NONE =>

       let val (t, (tab', nctxt')) = fresh_term T cx

       in (t, (Inttab.update (i, t) tab', nctxt')) end)

 fun trans_expr _ True = pair @{term True}

   | trans_expr _ False = pair @{term False}

   | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)

   | trans_expr T (Number (i, SOME j)) =

       pair (Const (@{const_name divide}, [T, T] ---> T) $

         HOLogic.mk_number T i $ HOLogic.mk_number T j)

   | trans_expr T (Value i) = term_of_value T i

   | trans_expr T (Array a) = trans_array T a

 and trans_array T a =

   let val dT = Term.domain_type T and rT = Term.range_type T

   in

     (case a of

       Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))

     | Store ((a', e1), e2) =>

         trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>>

         (fn ((m, k), v) =>

           Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v))

   end

 fun trans_pat i T f x =

   f (Term.domain_type T) ##>> trans (i-1) (Term.range_type T) x #>>

   (fn (u, (us, t)) => (u :: us, t))

 and trans i T ([], v) =

       if i > 0 then trans_pat i T fresh_term ([], v)

       else trans_expr T v #>> pair []

   | trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v)

 fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u)

 fun mk_eq (Const (@{const_name apply}, _)) (u' :: us', u) = mk_eq' u' us' u

   | mk_eq t (us, u) = mk_eq' t us u

 fun translate (t, cs) =

   let val T = Term.fastype_of t

   in

     (case (can HOLogic.dest_number t, cs) of

       (true, [c]) => trans 0 T c #>> (fn (_, u) => [mk_eq u ([], t)])

     | (_, (es, _) :: _) => fold_map (trans (length es) T) cs #>> map (mk_eq t)

     | _ => raise TERM ("translate: no cases", [t]))

   end

 (* overall procedure *)

 fun parse_counterex ({terms, ...} : SMT_Translate.recon) ls =

   read_cex ls

   |> map_filter (lookup_term terms)

   |> with_name_context terms translate

   |> flat

 end