src/HOL/Tools/SMT/z3_model.ML

rewrite Z3 model equations one-by-one (the previous approach led to loss of information)

(*  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: Proof.context -> SMT_Translate.recon -> string list ->
    term list * term list
end

structure Z3_Model: Z3_MODEL =
struct

structure U = SMT_Utils


(* counterexample expressions *)

datatype expr = True | False | Number of int * int option | Value of int |
  Array of array | App of string * expr list
and array = Fresh of expr | Store of (array * expr) * expr


(* parsing *)

val space = Scan.many Symbol.is_ascii_blank
fun spaced p = p --| space
fun in_parens p = spaced (Scan.$$ "(") |-- p --| spaced (Scan.$$ ")")
fun in_braces p = spaced (Scan.$$ "{") |-- p --| spaced (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 = spaced (Scan.repeat1 (Scan.some digit) >>
  (fn ds => fold (fn d => fn i => i * 10 + d) ds 0))
val int_num = spaced (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 =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
val name = spaced (Scan.many1 is_char >> implode)

fun $$$ s = spaced (Scan.this_string s)

fun array_expr st = st |> in_parens (
  $$$ "const" |-- expr >> Fresh ||
  $$$ "store" |-- array_expr -- expr -- expr >> Store)

and expr st = st |> (
  $$$ "true" >> K True ||
  $$$ "false" >> K False ||
  int_num -- Scan.option ($$$ "/" |-- int_num) >> Number ||
  $$$ "val!" |-- nat_num >> Value ||
  name >> (App o rpair []) ||
  array_expr >> Array ||
  in_parens (name -- Scan.repeat1 expr) >> App)

fun args st = ($$$ "->" >> K [] || expr ::: args) st
val args_case = args -- expr
val else_case = $$$ "else" -- $$$ "->" |-- expr >> 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 (name --| $$$ "->" -- (func || expr >> (single o pair [])))

fun resolve terms ((n, k), cases) =
  (case Symtab.lookup terms n of
    NONE => NONE
  | SOME t => SOME ((t, k), cases))

fun annotate _ (_, []) = NONE
  | annotate terms (n, [([], c)]) = resolve terms ((n, 0), (c, []))
  | annotate _ (_, [_]) = NONE
  | annotate terms (n, cases as (args, _) :: _) =
      let val (cases', (_, else_case)) = split_last cases
      in resolve terms ((n, length args), (else_case, cases')) end

fun read_cex terms ls =
  maps (cons "\n" o raw_explode) ls
  |> try (fst o Scan.finite Symbol.stopper cex)
  |> the_default []
  |> map_filter (annotate terms)


(* translation into terms *)

fun max_value vs =
  let
    fun max_val_expr (Value i) = Integer.max i
      | max_val_expr (App (_, es)) = fold max_val_expr es
      | max_val_expr (Array a) = max_val_array a
      | max_val_expr _ = I

    and max_val_array (Fresh e) = max_val_expr e
      | max_val_array (Store ((a, e1), e2)) =
          max_val_array a #> max_val_expr e1 #> max_val_expr e2

    fun max_val (_, (ec, cs)) =
      max_val_expr ec #> fold (fn (es, e) => fold max_val_expr (e :: es)) cs

  in fold max_val vs ~1 end

fun with_context terms f vs = fst (fold_map f vs (terms, max_value vs + 1))

fun get_term n T es (cx as (terms, next_val)) =
  (case Symtab.lookup terms n of
    SOME t => ((t, es), cx)
  | NONE =>
      let val t = Var (("skolem", next_val), T)
      in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end)

fun trans_expr _ True = pair @{const True}
  | trans_expr _ False = pair @{const 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) = pair (Var (("value", i), T))
  | trans_expr T (Array a) = trans_array T a
  | trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') =>
      let val Ts = fst (U.dest_funT (length es') (Term.fastype_of t))
      in
        fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t
      end)

and trans_array T a =
  let val (dT, rT) = Term.dest_funT 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_pattern T ([], e) = trans_expr T e #>> pair []
  | trans_pattern T (arg :: args, e) =
      trans_expr (Term.domain_type T) arg ##>>
      trans_pattern (Term.range_type T) (args, e) #>>
      (fn (arg', (args', e')) => (arg' :: args', e'))

fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)

fun mk_update ([], u) _ = u
  | mk_update ([t], u) f =
      uncurry mk_fun_upd (Term.dest_funT (Term.fastype_of f)) $ f $ t $ u
  | mk_update (t :: ts, u) f =
      let
        val (dT, rT) = Term.dest_funT (Term.fastype_of f)
        val (dT', rT') = Term.dest_funT rT
      in
        mk_fun_upd dT rT $ f $ t $
          mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
      end

fun mk_lambda Ts (t, pats) =
  fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats

fun translate ((t, k), (e, cs)) =
  let
    val T = Term.fastype_of t
    val (Us, U) = U.dest_funT k (Term.fastype_of t)

    fun mk_full_def u' pats =
      pats
      |> filter_out (fn (_, u) => u aconv u')
      |> HOLogic.mk_eq o pair t o mk_lambda Us o pair u'

    fun mk_eq (us, u) = HOLogic.mk_eq (Term.list_comb (t, us), u)
    fun mk_eqs u' [] = [HOLogic.mk_eq (t, u')]
      | mk_eqs _ pats = map mk_eq pats
  in
    trans_expr U e ##>>
    (if k = 0 then pair [] else fold_map (trans_pattern T) cs) #>>
    (fn (u', pats) => (mk_eqs u' pats, mk_full_def u' pats))
  end


(* normalization *)

fun partition_eqs f =
  let
    fun part t (xs, ts) =
      (case try HOLogic.dest_eq t of
        SOME (l, r) => (case f l r of SOME x => (x::xs, ts) | _ => (xs, t::ts))
      | NONE => (xs, t :: ts))
  in (fn ts => fold part ts ([], [])) end

fun first_eq pred =
  let
    fun part _ [] = NONE
      | part us (t :: ts) =
          (case try HOLogic.dest_eq t of
            SOME lr =>
              if pred lr then SOME (lr, fold cons us ts) else part (t :: us) ts
          | NONE => part (t :: us) ts)
  in (fn ts => part [] ts) end

fun replace_vars tab =
  let
    fun replace (v as Var _) = the_default v (AList.lookup (op aconv) tab v)
      | replace t = t
  in map (Term.map_aterms replace) end

fun remove_int_nat_coercions (eqs, defs) =
  let
    fun mk_nat_num t i =
      (case try HOLogic.dest_number i of
        SOME (_, n) => SOME (t, HOLogic.mk_number @{typ nat} n)
      | NONE => NONE)
    fun nat_of (@{const of_nat (int)} $ (t as Var _)) i = mk_nat_num t i
      | nat_of (@{const nat} $ i) (t as Var _) = mk_nat_num t i
      | nat_of _ _ = NONE
    val (nats, eqs') = partition_eqs nat_of eqs

    fun is_coercion t =
      (case try HOLogic.dest_eq t of
        SOME (@{const of_nat (int)}, _) => true
      | SOME (@{const nat}, _) => true
      | _ => false)
  in pairself (replace_vars nats) (eqs', filter_out is_coercion defs) end

fun unfold_funapp (eqs, defs) =
  let
    fun unfold_app (Const (@{const_name SMT.fun_app}, _) $ f $ t) = f $ t
      | unfold_app t = t
    fun unfold_eq ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =
          eq $ unfold_app t $ u
      | unfold_eq t = t

    fun is_fun_app t =
      (case try HOLogic.dest_eq t of
        SOME (Const (@{const_name SMT.fun_app}, _), _) => true
      | _ => false)

  in (map unfold_eq eqs, filter_out is_fun_app defs) end

fun unfold_eqs (eqs, defs) =
  let
    val is_ground = not o Term.exists_subterm Term.is_Var

    fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u
      | is_trivial _ = false

    fun replace r = replace_vars [r] #> filter_out is_trivial

    fun unfold (es, ds) =
      (case first_eq (fn (l, Var _) => is_ground l | _ => false) es of
        SOME ((l, r), es') => unfold (pairself (replace (r, l)) (es', ds))
      | NONE => (es, ds))

  in unfold (eqs, defs) end

fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) =
      eq $ u $ t
  | swap_free t = t

fun frees_for_vars ctxt (eqs, defs) =
  let
    fun fresh_free i T (cx as (frees, ctxt)) =
      (case Inttab.lookup frees i of
        SOME t => (t, cx)
      | NONE =>
          let
            val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
            val t = Free (n, T)
          in (t, (Inttab.update (i, t) frees, ctxt')) end)

    fun repl_var (Var ((_, i), T)) = fresh_free i T
      | repl_var (t $ u) = repl_var t ##>> repl_var u #>> op $
      | repl_var (Abs (n, T, t)) = repl_var t #>> (fn t' => Abs (n, T, t'))
      | repl_var t = pair t
  in
    (Inttab.empty, ctxt)
    |> fold_map repl_var eqs
    ||>> fold_map repl_var defs
    |> fst
  end


(* overall procedure *)

val is_free_constraint = Term.exists_subterm (fn Free _ => true | _ => false)

fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true
  | is_const_def _ = false

fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls =
  read_cex terms ls
  |> with_context terms translate
  |> apfst flat o split_list
  |> remove_int_nat_coercions
  |> unfold_funapp
  |> unfold_eqs
  |>> map swap_free
  |>> filter is_free_constraint
  |> frees_for_vars ctxt
  ||> filter is_const_def

end