# HG changeset patch
# User blanchet
# Date 1401723265 -7200
# Node ID 3546a67226eaeb76437e901811c6fbc1502e4e26
# Parent  5c59114ff0cbafba97f472c833c43f70998c829d
removed counterexample parser (obsolete and useless in practice)

diff -r 5c59114ff0cb -r 3546a67226ea src/HOL/SMT2.thy
--- a/src/HOL/SMT2.thy	Mon Jun 02 16:19:37 2014 +0200
+++ b/src/HOL/SMT2.thy	Mon Jun 02 17:34:25 2014 +0200
@@ -148,7 +148,6 @@
 ML_file "Tools/SMT2/smt2_translate.ML"
 ML_file "Tools/SMT2/smtlib2.ML"
 ML_file "Tools/SMT2/smtlib2_interface.ML"
-ML_file "Tools/SMT2/z3_new_model.ML"
 ML_file "Tools/SMT2/z3_new_proof.ML"
 ML_file "Tools/SMT2/smt2_solver.ML"
 ML_file "Tools/SMT2/z3_new_isar.ML"
diff -r 5c59114ff0cb -r 3546a67226ea src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Mon Jun 02 16:19:37 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Mon Jun 02 17:34:25 2014 +0200
@@ -17,8 +17,6 @@
     default_max_relevant: int,
     can_filter: bool,
     outcome: string -> string list -> outcome * string list,
-    cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
-      term list * term list) option,
     replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
       ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option}
 
@@ -144,8 +142,6 @@
   default_max_relevant: int,
   can_filter: bool,
   outcome: string -> string list -> outcome * string list,
-  cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
-    term list * term list) option,
   replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
     ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option}
 
@@ -180,7 +176,7 @@
 )
 
 local
-  fun finish outcome cex_parser replay ocl outer_ctxt
+  fun finish outcome replay ocl outer_ctxt
       (replay_data as {context = ctxt, ...} : SMT2_Translate.replay_data) output =
     (case outcome output of
       (Unsat, ls) =>
@@ -188,25 +184,22 @@
         then the replay outer_ctxt replay_data ls
         else (([], []), ocl ())
     | (result, ls) =>
-        let val (ts, us) = (case cex_parser of SOME f => f ctxt replay_data ls | _ => ([], []))
-        in
-          raise SMT2_Failure.SMT (SMT2_Failure.Counterexample {
-            is_real_cex = (result = Sat),
-            free_constraints = ts,
-            const_defs = us})
-        end)
+        raise SMT2_Failure.SMT (SMT2_Failure.Counterexample {
+          is_real_cex = (result = Sat),
+          free_constraints = [],
+          const_defs = []}))
 
   val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
 in
 
 fun add_solver ({name, class, avail, command, options, default_max_relevant, can_filter,
-    outcome, cex_parser, replay} : solver_config) =
+    outcome, replay} : solver_config) =
   let
     fun solver ocl = {
       command = command,
       default_max_relevant = default_max_relevant,
       can_filter = can_filter,
-      finish = finish (outcome name) cex_parser replay ocl}
+      finish = finish (outcome name) replay ocl}
 
     val info = {name = name, class = class, avail = avail, options = options}
   in
diff -r 5c59114ff0cb -r 3546a67226ea src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Mon Jun 02 16:19:37 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Mon Jun 02 17:34:25 2014 +0200
@@ -58,7 +58,6 @@
   can_filter = false,
   outcome =
     on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
-  cex_parser = NONE,
   replay = NONE }
 
 end
@@ -79,7 +78,6 @@
   default_max_relevant = 350 (* FUDGE *),
   can_filter = false,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
-  cex_parser = NONE,
   replay = NONE }
 
 
@@ -145,7 +143,6 @@
   default_max_relevant = 350 (* FUDGE *),
   can_filter = true,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
-  cex_parser = SOME Z3_New_Model.parse_counterex,
   replay = SOME Z3_New_Replay.replay }
 
 end
diff -r 5c59114ff0cb -r 3546a67226ea src/HOL/Tools/SMT2/z3_new_model.ML
--- a/src/HOL/Tools/SMT2/z3_new_model.ML	Mon Jun 02 16:19:37 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,334 +0,0 @@
-(*  Title:      HOL/Tools/SMT2/z3_new_model.ML
-    Author:     Sascha Boehme and Philipp Meyer, TU Muenchen
-
-Parser for counterexamples generated by Z3.
-*)
-
-signature Z3_NEW_MODEL =
-sig
-  val parse_counterex: Proof.context -> SMT2_Translate.replay_data -> string list ->
-    term list * term list
-end
-
-structure Z3_New_Model: Z3_NEW_MODEL =
-struct
-
-(* 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 (SMT2_Util.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) (absdummy dT' (Const ("_", rT')))
-      end
-
-fun mk_lambda Ts (t, pats) =
-  fold_rev absdummy Ts t |> fold mk_update pats
-
-fun translate ((t, k), (e, cs)) =
-  let
-    val T = Term.fastype_of t
-    val (Us, U) = SMT2_Util.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 (pred o HOLogic.dest_eq) t of
-            SOME (SOME lr) => SOME (lr, fold cons us ts)
-          | _ => part (t :: us) ts)
-  in (fn ts => part [] ts) end
-
-fun replace_vars tab =
-  let
-    fun repl v = the_default v (AList.lookup (op aconv) tab v)
-    fun replace (v as Var _) = repl v
-      | replace (v as Free _) = repl 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 SMT2.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 SMT2.fun_app}, _), _) => true
-      | _ => false)
-
-  in (map unfold_eq eqs, filter_out is_fun_app defs) end
-
-val unfold_eqs =
-  let
-    val is_ground = not o Term.exists_subterm Term.is_Var
-    fun is_non_rec (v, t) = not (Term.exists_subterm (equal v) t)
-
-    fun rewr_var (l as Var _, r) = if is_ground r then SOME (l, r) else NONE
-      | rewr_var (r, l as Var _) = if is_ground r then SOME (l, r) else NONE
-      | rewr_var _ = NONE
-
-    fun rewr_free' e = if is_non_rec e then SOME e else NONE
-    fun rewr_free (e as (Free _, _)) = rewr_free' e
-      | rewr_free (e as (_, Free _)) = rewr_free' (swap e)
-      | rewr_free _ = NONE
-
-    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_vars (es, ds) =
-      (case first_eq rewr_var es of
-        SOME (lr, es') => unfold_vars (pairself (replace lr) (es', ds))
-      | NONE => (es, ds))
-
-    fun unfold_frees ues (es, ds) =
-      (case first_eq rewr_free es of
-        SOME (lr, es') =>
-          pairself (replace lr) (es', ds)
-          |> unfold_frees (HOLogic.mk_eq lr :: replace lr ues)
-      | NONE => (ues @ es, ds))
-
-  in unfold_vars #> unfold_frees [] 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_free_def (Const (@{const_name HOL.eq}, _) $ Free _ $ _) = true
-  | is_free_def _ = false
-
-fun defined tp =
-  try (pairself (fst o HOLogic.dest_eq)) tp
-  |> the_default false o Option.map (op aconv)
-
-fun add_free_defs free_cs defs =
-  let val (free_defs, defs') = List.partition is_free_def defs
-  in (free_cs @ filter_out (member defined free_cs) free_defs, defs') end
-
-fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true
-  | is_const_def _ = false
-
-(* TODO: Adapt parser to SMT-LIB 2 format for models *)
-fun parse_counterex ctxt ({terms, ...} : SMT2_Translate.replay_data) 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
-  |-> add_free_defs
-  |> frees_for_vars ctxt
-  ||> filter is_const_def
-
-end