1.1 --- a/src/HOL/Tools/SMT/smt_failure.ML Tue Nov 30 00:12:29 2010 +0100
1.2 +++ b/src/HOL/Tools/SMT/smt_failure.ML Tue Nov 30 18:22:43 2010 +0100
1.3 @@ -6,12 +6,17 @@
1.4
1.5 signature SMT_FAILURE =
1.6 sig
1.7 + type counterexample = {
1.8 + is_real_cex: bool,
1.9 + free_constraints: term list,
1.10 + const_defs: term list}
1.11 datatype failure =
1.12 - Counterexample of bool * term list |
1.13 + Counterexample of counterexample |
1.14 Time_Out |
1.15 Out_Of_Memory |
1.16 Abnormal_Termination of int |
1.17 Other_Failure of string
1.18 + val pretty_counterexample: Proof.context -> counterexample -> Pretty.T
1.19 val string_of_failure: Proof.context -> failure -> string
1.20 exception SMT of failure
1.21 end
1.22 @@ -19,23 +24,32 @@
1.23 structure SMT_Failure: SMT_FAILURE =
1.24 struct
1.25
1.26 +type counterexample = {
1.27 + is_real_cex: bool,
1.28 + free_constraints: term list,
1.29 + const_defs: term list}
1.30 +
1.31 datatype failure =
1.32 - Counterexample of bool * term list |
1.33 + Counterexample of counterexample |
1.34 Time_Out |
1.35 Out_Of_Memory |
1.36 Abnormal_Termination of int |
1.37 Other_Failure of string
1.38
1.39 -fun string_of_failure ctxt (Counterexample (real, ex)) =
1.40 - let
1.41 - val msg =
1.42 - if real then "Counterexample found (possibly spurious)"
1.43 - else "Potential counterexample found"
1.44 - in
1.45 - if null ex then msg
1.46 - else Pretty.string_of (Pretty.big_list (msg ^ ":")
1.47 - (map (Syntax.pretty_term ctxt) ex))
1.48 - end
1.49 +fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} =
1.50 + let
1.51 + val msg =
1.52 + if is_real_cex then "Counterexample found (possibly spurious)"
1.53 + else "Potential counterexample found"
1.54 + in
1.55 + if null free_constraints andalso null const_defs then Pretty.str msg
1.56 + else
1.57 + Pretty.big_list (msg ^ ":")
1.58 + (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs))
1.59 + end
1.60 +
1.61 +fun string_of_failure ctxt (Counterexample cex) =
1.62 + Pretty.string_of (pretty_counterexample ctxt cex)
1.63 | string_of_failure _ Time_Out = "Timed out"
1.64 | string_of_failure _ Out_Of_Memory = "Ran out of memory"
1.65 | string_of_failure _ (Abnormal_Termination err) =
2.1 --- a/src/HOL/Tools/SMT/smt_solver.ML Tue Nov 30 00:12:29 2010 +0100
2.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Nov 30 18:22:43 2010 +0100
2.3 @@ -19,7 +19,7 @@
2.4 interface: interface,
2.5 outcome: string -> string list -> outcome * string list,
2.6 cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
2.7 - term list) option,
2.8 + term list * term list) option,
2.9 reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
2.10 (int list * thm) * Proof.context) option }
2.11
2.12 @@ -65,7 +65,7 @@
2.13 interface: interface,
2.14 outcome: string -> string list -> outcome * string list,
2.15 cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
2.16 - term list) option,
2.17 + term list * term list) option,
2.18 reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
2.19 (int list * thm) * Proof.context) option }
2.20
2.21 @@ -260,9 +260,14 @@
2.22 then the reconstruct ctxt recon ls
2.23 else (([], ocl ()), ctxt)
2.24 | (result, ls) =>
2.25 - let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => [])
2.26 - in
2.27 - raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
2.28 + let
2.29 + val (ts, us) =
2.30 + (case cex_parser of SOME f => f ctxt recon ls | _ => ([], []))
2.31 + in
2.32 + raise SMT_Failure.SMT (SMT_Failure.Counterexample {
2.33 + is_real_cex = (result = Sat),
2.34 + free_constraints = ts,
2.35 + const_defs = us})
2.36 end)
2.37
2.38 val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
2.39 @@ -351,15 +356,14 @@
2.40 let
2.41 fun solve irules = snd (smt_solver NONE ctxt' irules)
2.42 val tag = "Solver " ^ C.solver_of ctxt' ^ ": "
2.43 - val str_of = SMT_Failure.string_of_failure ctxt'
2.44 + val str_of = prefix tag o SMT_Failure.string_of_failure ctxt'
2.45 fun safe_solve irules =
2.46 if pass_exns then SOME (solve irules)
2.47 else (SOME (solve irules)
2.48 handle
2.49 SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
2.50 - (C.verbose_msg ctxt' (prefix tag o str_of) fail; NONE)
2.51 - | SMT_Failure.SMT fail =>
2.52 - (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE))
2.53 + (C.verbose_msg ctxt' str_of fail; NONE)
2.54 + | SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE))
2.55 in
2.56 safe_solve (map (pair ~1) (rules @ prems))
2.57 |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
3.1 --- a/src/HOL/Tools/SMT/z3_model.ML Tue Nov 30 00:12:29 2010 +0100
3.2 +++ b/src/HOL/Tools/SMT/z3_model.ML Tue Nov 30 18:22:43 2010 +0100
3.3 @@ -7,7 +7,7 @@
3.4 signature Z3_MODEL =
3.5 sig
3.6 val parse_counterex: Proof.context -> SMT_Translate.recon -> string list ->
3.7 - term list
3.8 + term list * term list
3.9 end
3.10
3.11 structure Z3_Model: Z3_MODEL =
3.12 @@ -70,117 +70,51 @@
3.13 val cex = space |--
3.14 Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
3.15
3.16 -fun read_cex ls =
3.17 +fun resolve terms ((n, k), cases) =
3.18 + (case Symtab.lookup terms n of
3.19 + NONE => NONE
3.20 + | SOME t => SOME ((t, k), cases))
3.21 +
3.22 +fun annotate _ (_, []) = NONE
3.23 + | annotate terms (n, [([], c)]) = resolve terms ((n, 0), (c, []))
3.24 + | annotate _ (_, [_]) = NONE
3.25 + | annotate terms (n, cases as (args, _) :: _) =
3.26 + let val (cases', (_, else_case)) = split_last cases
3.27 + in resolve terms ((n, length args), (else_case, cases')) end
3.28 +
3.29 +fun read_cex terms ls =
3.30 maps (cons "\n" o raw_explode) ls
3.31 |> try (fst o Scan.finite Symbol.stopper cex)
3.32 |> the_default []
3.33 -
3.34 -
3.35 -(* normalization *)
3.36 -
3.37 -local
3.38 - fun matches terms f n =
3.39 - (case Symtab.lookup terms n of
3.40 - NONE => false
3.41 - | SOME t => f t)
3.42 -
3.43 - fun subst f (n, cases) = (n, map (fn (args, v) => (map f args, f v)) cases)
3.44 -in
3.45 -
3.46 -fun reduce_function (n, [c]) = SOME ((n, 0), [c])
3.47 - | reduce_function (n, cases) =
3.48 - let val (patterns, else_case as (_, e)) = split_last cases
3.49 - in
3.50 - (case patterns of
3.51 - [] => NONE
3.52 - | (args, _) :: _ => SOME ((n, length args),
3.53 - filter_out (equal e o snd) patterns @ [else_case]))
3.54 - end
3.55 -
3.56 -fun drop_skolem_constants terms = filter (Symtab.defined terms o fst o fst)
3.57 -
3.58 -fun substitute_constants terms =
3.59 - let
3.60 - fun check vs1 [] = rev vs1
3.61 - | check vs1 ((v as ((n, k), [([], Value i)])) :: vs2) =
3.62 - if matches terms (fn Free _ => true | _ => false) n orelse k > 0
3.63 - then check (v :: vs1) vs2
3.64 - else
3.65 - let
3.66 - fun sub (e as Value j) = if i = j then App (n, []) else e
3.67 - | sub e = e
3.68 - in check (map (subst sub) vs1) (map (subst sub) vs2) end
3.69 - | check vs1 (v :: vs2) = check (v :: vs1) vs2
3.70 - in check [] end
3.71 -
3.72 -fun remove_int_nat_coercions terms vs =
3.73 - let
3.74 - fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
3.75 -
3.76 - val (default_int, ints) =
3.77 - (case find_first (match [@{const of_nat (int)}]) vs of
3.78 - NONE => (NONE, [])
3.79 - | SOME (_, cases) =>
3.80 - let val (cs, (_, e)) = split_last cases
3.81 - in (SOME e, map (apfst hd) cs) end)
3.82 -
3.83 - fun nat_of @{typ nat} (v as Value _) =
3.84 - AList.lookup (op =) ints v |> the_default (the_default v default_int)
3.85 - | nat_of _ e = e
3.86 -
3.87 - fun subst_nat T k ([], e) =
3.88 - let fun app f i = if i <= 0 then I else app f (i-1) o f
3.89 - in ([], nat_of (app Term.range_type k T) e) end
3.90 - | subst_nat T k (arg :: args, e) =
3.91 - subst_nat (Term.range_type T) (k-1) (args, e)
3.92 - |> apfst (cons (nat_of (Term.domain_type T) arg))
3.93 -
3.94 - fun subst_nats (v as ((n, k), cases)) =
3.95 - (case Symtab.lookup terms n of
3.96 - NONE => v
3.97 - | SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
3.98 - in
3.99 - map subst_nats vs
3.100 - |> filter_out (match [@{const of_nat (int)}, @{const nat}])
3.101 - end
3.102 -
3.103 -fun filter_valid_valuations terms = map_filter (fn
3.104 - (_, []) => NONE
3.105 - | ((n, i), cases) =>
3.106 - let
3.107 - fun valid_expr (Array a) = valid_array a
3.108 - | valid_expr (App (n, es)) =
3.109 - Symtab.defined terms n andalso forall valid_expr es
3.110 - | valid_expr _ = true
3.111 - and valid_array (Fresh e) = valid_expr e
3.112 - | valid_array (Store ((a, e1), e2)) =
3.113 - valid_array a andalso valid_expr e1 andalso valid_expr e2
3.114 - fun valid_case (es, e) = forall valid_expr (e :: es)
3.115 - in
3.116 - if not (forall valid_case cases) then NONE
3.117 - else Option.map (rpair cases o rpair i) (Symtab.lookup terms n)
3.118 - end)
3.119 -
3.120 -end
3.121 + |> map_filter (annotate terms)
3.122
3.123
3.124 (* translation into terms *)
3.125
3.126 -fun with_context ctxt terms f vs =
3.127 - fst (fold_map f vs (ctxt, terms, Inttab.empty))
3.128 +fun max_value vs =
3.129 + let
3.130 + fun max_val_expr (Value i) = Integer.max i
3.131 + | max_val_expr (App (_, es)) = fold max_val_expr es
3.132 + | max_val_expr (Array a) = max_val_array a
3.133 + | max_val_expr _ = I
3.134
3.135 -fun fresh_term T (ctxt, terms, values) =
3.136 - let val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
3.137 - in (Free (n, T), (ctxt', terms, values)) end
3.138 + and max_val_array (Fresh e) = max_val_expr e
3.139 + | max_val_array (Store ((a, e1), e2)) =
3.140 + max_val_array a #> max_val_expr e1 #> max_val_expr e2
3.141
3.142 -fun term_of_value T i (cx as (_, _, values)) =
3.143 - (case Inttab.lookup values i of
3.144 - SOME t => (t, cx)
3.145 + fun max_val (_, (ec, cs)) =
3.146 + max_val_expr ec #> fold (fn (es, e) => fold max_val_expr (e :: es)) cs
3.147 +
3.148 + in fold max_val vs ~1 end
3.149 +
3.150 +fun with_context terms f vs = fst (fold_map f vs (terms, max_value vs + 1))
3.151 +
3.152 +fun get_term n T es (cx as (terms, next_val)) =
3.153 + (case Symtab.lookup terms n of
3.154 + SOME t => ((t, es), cx)
3.155 | NONE =>
3.156 - let val (t, (ctxt', terms', values')) = fresh_term T cx
3.157 - in (t, (ctxt', terms', Inttab.update (i, t) values')) end)
3.158 -
3.159 -fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
3.160 + let val t = Var (("fresh", next_val), T)
3.161 + in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end)
3.162
3.163 fun trans_expr _ True = pair @{const True}
3.164 | trans_expr _ False = pair @{const False}
3.165 @@ -188,18 +122,16 @@
3.166 | trans_expr T (Number (i, SOME j)) =
3.167 pair (Const (@{const_name divide}, [T, T] ---> T) $
3.168 HOLogic.mk_number T i $ HOLogic.mk_number T j)
3.169 - | trans_expr T (Value i) = term_of_value T i
3.170 + | trans_expr T (Value i) = pair (Var (("value", i), T))
3.171 | trans_expr T (Array a) = trans_array T a
3.172 - | trans_expr _ (App (n, es)) =
3.173 - let val get_Ts = take (length es) o Term.binder_types o Term.fastype_of
3.174 + | trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') =>
3.175 + let val Ts = fst (U.dest_funT (length es') (Term.fastype_of t))
3.176 in
3.177 - get_term n #-> (fn t =>
3.178 - fold_map (uncurry trans_expr) (get_Ts t ~~ es) #>>
3.179 - Term.list_comb o pair t)
3.180 - end
3.181 + fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t
3.182 + end)
3.183
3.184 and trans_array T a =
3.185 - let val dT = Term.domain_type T and rT = Term.range_type T
3.186 + let val (dT, rT) = U.split_type T
3.187 in
3.188 (case a of
3.189 Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
3.190 @@ -232,35 +164,131 @@
3.191 fun mk_lambda Ts (t, pats) =
3.192 fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats
3.193
3.194 -fun translate' T i [([], e)] =
3.195 - if i = 0 then trans_expr T e
3.196 - else
3.197 - let val ((Us1, Us2), U) = Term.strip_type T |>> chop i
3.198 - in trans_expr (Us2 ---> U) e #>> mk_lambda Us1 o rpair [] end
3.199 - | translate' T i cases =
3.200 - let
3.201 - val (pat_cases, def) = split_last cases |> apsnd snd
3.202 - val ((Us1, Us2), U) = Term.strip_type T |>> chop i
3.203 - in
3.204 - trans_expr (Us2 ---> U) def ##>>
3.205 - fold_map (trans_pattern T) pat_cases #>>
3.206 - mk_lambda Us1
3.207 - end
3.208 +fun translate ((t, k), (e, cs)) =
3.209 + let
3.210 + val T = Term.fastype_of t
3.211 + val (Us, U) = U.dest_funT k (Term.fastype_of t)
3.212
3.213 -fun translate ((t, i), cases) =
3.214 - translate' (Term.fastype_of t) i cases #>> HOLogic.mk_eq o pair t
3.215 + fun mk_full_def u' pats =
3.216 + pats
3.217 + |> filter_out (fn (_, u) => u aconv u')
3.218 + |> HOLogic.mk_eq o pair t o mk_lambda Us o pair u'
3.219 +
3.220 + fun mk_eq (us, u) = HOLogic.mk_eq (Term.list_comb (t, us), u)
3.221 + fun mk_eqs u' [] = [HOLogic.mk_eq (t, u')]
3.222 + | mk_eqs _ pats = map mk_eq pats
3.223 + in
3.224 + trans_expr U e ##>>
3.225 + (if k = 0 then pair [] else fold_map (trans_pattern T) cs) #>>
3.226 + (fn (u', pats) => (mk_eqs u' pats, mk_full_def u' pats))
3.227 + end
3.228 +
3.229 +
3.230 +(* normalization *)
3.231 +
3.232 +fun partition_eqs f =
3.233 + let
3.234 + fun part t (xs, ts) =
3.235 + (case try HOLogic.dest_eq t of
3.236 + SOME (l, r) => (case f l r of SOME x => (x::xs, ts) | _ => (xs, t::ts))
3.237 + | NONE => (xs, t :: ts))
3.238 + in (fn ts => fold part ts ([], [])) end
3.239 +
3.240 +fun replace_vars tab =
3.241 + let
3.242 + fun replace (v as Var _) = the_default v (AList.lookup (op aconv) tab v)
3.243 + | replace t = t
3.244 + in map (Term.map_aterms replace) end
3.245 +
3.246 +fun remove_int_nat_coercions (eqs, defs) =
3.247 + let
3.248 + fun mk_nat_num t i =
3.249 + (case try HOLogic.dest_number i of
3.250 + SOME (_, n) => SOME (t, HOLogic.mk_number @{typ nat} n)
3.251 + | NONE => NONE)
3.252 + fun nat_of (@{const of_nat (int)} $ (t as Var _)) i = mk_nat_num t i
3.253 + | nat_of (@{const nat} $ i) (t as Var _) = mk_nat_num t i
3.254 + | nat_of _ _ = NONE
3.255 + val (nats, eqs') = partition_eqs nat_of eqs
3.256 +
3.257 + fun is_coercion t =
3.258 + (case try HOLogic.dest_eq t of
3.259 + SOME (@{const of_nat (int)}, _) => true
3.260 + | SOME (@{const nat}, _) => true
3.261 + | _ => false)
3.262 + in pairself (replace_vars nats) (eqs', filter_out is_coercion defs) end
3.263 +
3.264 +fun unfold_funapp (eqs, defs) =
3.265 + let
3.266 + fun unfold_app (Const (@{const_name SMT.fun_app}, _) $ f $ t) = f $ t
3.267 + | unfold_app t = t
3.268 + fun unfold_eq ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =
3.269 + eq $ unfold_app t $ u
3.270 + | unfold_eq t = t
3.271 +
3.272 + fun is_fun_app t =
3.273 + (case try HOLogic.dest_eq t of
3.274 + SOME (Const (@{const_name SMT.fun_app}, _), _) => true
3.275 + | _ => false)
3.276 +
3.277 + in (map unfold_eq eqs, filter_out is_fun_app defs) end
3.278 +
3.279 +fun unfold_simple_eqs (eqs, defs) =
3.280 + let
3.281 + fun add_rewr (l as Const _) (r as Var _) = SOME (r, l)
3.282 + | add_rewr (l as Free _) (r as Var _) = SOME (r, l)
3.283 + | add_rewr _ _ = NONE
3.284 + val (rs, eqs') = partition_eqs add_rewr eqs
3.285 +
3.286 + fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u
3.287 + | is_trivial _ = false
3.288 + in pairself (replace_vars rs #> filter_out is_trivial) (eqs', defs) end
3.289 +
3.290 +fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) =
3.291 + eq $ u $ t
3.292 + | swap_free t = t
3.293 +
3.294 +fun frees_for_vars ctxt (eqs, defs) =
3.295 + let
3.296 + fun fresh_free i T (cx as (frees, ctxt)) =
3.297 + (case Inttab.lookup frees i of
3.298 + SOME t => (t, cx)
3.299 + | NONE =>
3.300 + let
3.301 + val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
3.302 + val t = Free (n, T)
3.303 + in (t, (Inttab.update (i, t) frees, ctxt')) end)
3.304 +
3.305 + fun repl_var (Var ((_, i), T)) = fresh_free i T
3.306 + | repl_var (t $ u) = repl_var t ##>> repl_var u #>> op $
3.307 + | repl_var (Abs (n, T, t)) = repl_var t #>> (fn t' => Abs (n, T, t'))
3.308 + | repl_var t = pair t
3.309 + in
3.310 + (Inttab.empty, ctxt)
3.311 + |> fold_map repl_var eqs
3.312 + ||>> fold_map repl_var defs
3.313 + |> fst
3.314 + end
3.315
3.316
3.317 (* overall procedure *)
3.318
3.319 +val is_free_constraint = Term.exists_subterm (fn Free _ => true | _ => false)
3.320 +
3.321 +fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true
3.322 + | is_const_def _ = false
3.323 +
3.324 fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls =
3.325 - read_cex ls
3.326 - |> map_filter reduce_function
3.327 - |> drop_skolem_constants terms
3.328 - |> substitute_constants terms
3.329 - |> remove_int_nat_coercions terms
3.330 - |> filter_valid_valuations terms
3.331 - |> with_context ctxt terms translate
3.332 + read_cex terms ls
3.333 + |> with_context terms translate
3.334 + |> apfst flat o split_list
3.335 + |> remove_int_nat_coercions
3.336 + |> unfold_funapp
3.337 + |> unfold_simple_eqs
3.338 + |>> map swap_free
3.339 + |>> filter is_free_constraint
3.340 + |> frees_for_vars ctxt
3.341 + ||> filter is_const_def
3.342
3.343 end
3.344