# HG changeset patch # User boehmes # Date 1291137763 -3600 # Node ID 47ff261431c46a91cca93df91aabe2da16ff617e # Parent eeaa59fb5ad82346bdb9e9f88223b52e40080920 split up Z3 models into constraints on free variables and constant definitions; reduce Z3 models by replacing unknowns with free variables and constants from the goal; remove occurrences of the hidden constant fun_app from Z3 models diff -r eeaa59fb5ad8 -r 47ff261431c4 src/HOL/Tools/SMT/smt_failure.ML --- a/src/HOL/Tools/SMT/smt_failure.ML Tue Nov 30 00:12:29 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_failure.ML Tue Nov 30 18:22:43 2010 +0100 @@ -6,12 +6,17 @@ signature SMT_FAILURE = sig + type counterexample = { + is_real_cex: bool, + free_constraints: term list, + const_defs: term list} datatype failure = - Counterexample of bool * term list | + Counterexample of counterexample | Time_Out | Out_Of_Memory | Abnormal_Termination of int | Other_Failure of string + val pretty_counterexample: Proof.context -> counterexample -> Pretty.T val string_of_failure: Proof.context -> failure -> string exception SMT of failure end @@ -19,23 +24,32 @@ structure SMT_Failure: SMT_FAILURE = struct +type counterexample = { + is_real_cex: bool, + free_constraints: term list, + const_defs: term list} + datatype failure = - Counterexample of bool * term list | + Counterexample of counterexample | Time_Out | Out_Of_Memory | Abnormal_Termination of int | Other_Failure of string -fun string_of_failure ctxt (Counterexample (real, ex)) = - let - val msg = - if real then "Counterexample found (possibly spurious)" - else "Potential counterexample found" - in - if null ex then msg - else Pretty.string_of (Pretty.big_list (msg ^ ":") - (map (Syntax.pretty_term ctxt) ex)) - end +fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} = + let + val msg = + if is_real_cex then "Counterexample found (possibly spurious)" + else "Potential counterexample found" + in + if null free_constraints andalso null const_defs then Pretty.str msg + else + Pretty.big_list (msg ^ ":") + (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs)) + end + +fun string_of_failure ctxt (Counterexample cex) = + Pretty.string_of (pretty_counterexample ctxt cex) | string_of_failure _ Time_Out = "Timed out" | string_of_failure _ Out_Of_Memory = "Ran out of memory" | string_of_failure _ (Abnormal_Termination err) = diff -r eeaa59fb5ad8 -r 47ff261431c4 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Tue Nov 30 00:12:29 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Nov 30 18:22:43 2010 +0100 @@ -19,7 +19,7 @@ interface: interface, outcome: string -> string list -> outcome * string list, cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> - term list) option, + term list * term list) option, reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> (int list * thm) * Proof.context) option } @@ -65,7 +65,7 @@ interface: interface, outcome: string -> string list -> outcome * string list, cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> - term list) option, + term list * term list) option, reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> (int list * thm) * Proof.context) option } @@ -260,9 +260,14 @@ then the reconstruct ctxt recon ls else (([], ocl ()), ctxt) | (result, ls) => - let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => []) - in - raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts)) + let + val (ts, us) = + (case cex_parser of SOME f => f ctxt recon ls | _ => ([], [])) + in + raise SMT_Failure.SMT (SMT_Failure.Counterexample { + is_real_cex = (result = Sat), + free_constraints = ts, + const_defs = us}) end) val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False}) @@ -351,15 +356,14 @@ let fun solve irules = snd (smt_solver NONE ctxt' irules) val tag = "Solver " ^ C.solver_of ctxt' ^ ": " - val str_of = SMT_Failure.string_of_failure ctxt' + val str_of = prefix tag o SMT_Failure.string_of_failure ctxt' fun safe_solve irules = if pass_exns then SOME (solve irules) else (SOME (solve irules) handle SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => - (C.verbose_msg ctxt' (prefix tag o str_of) fail; NONE) - | SMT_Failure.SMT fail => - (C.trace_msg ctxt' (prefix tag o str_of) fail; NONE)) + (C.verbose_msg ctxt' str_of fail; NONE) + | SMT_Failure.SMT fail => (C.trace_msg ctxt' str_of fail; NONE)) in safe_solve (map (pair ~1) (rules @ prems)) |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac) diff -r eeaa59fb5ad8 -r 47ff261431c4 src/HOL/Tools/SMT/z3_model.ML --- a/src/HOL/Tools/SMT/z3_model.ML Tue Nov 30 00:12:29 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_model.ML Tue Nov 30 18:22:43 2010 +0100 @@ -7,7 +7,7 @@ signature Z3_MODEL = sig val parse_counterex: Proof.context -> SMT_Translate.recon -> string list -> - term list + term list * term list end structure Z3_Model: Z3_MODEL = @@ -70,117 +70,51 @@ val cex = space |-- Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair []))) -fun read_cex ls = +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 [] - - -(* normalization *) - -local - fun matches terms f n = - (case Symtab.lookup terms n of - NONE => false - | SOME t => f t) - - fun subst f (n, cases) = (n, map (fn (args, v) => (map f args, f v)) cases) -in - -fun reduce_function (n, [c]) = SOME ((n, 0), [c]) - | reduce_function (n, cases) = - let val (patterns, else_case as (_, e)) = split_last cases - in - (case patterns of - [] => NONE - | (args, _) :: _ => SOME ((n, length args), - filter_out (equal e o snd) patterns @ [else_case])) - end - -fun drop_skolem_constants terms = filter (Symtab.defined terms o fst o fst) - -fun substitute_constants terms = - let - fun check vs1 [] = rev vs1 - | check vs1 ((v as ((n, k), [([], Value i)])) :: vs2) = - if matches terms (fn Free _ => true | _ => false) n orelse k > 0 - then check (v :: vs1) vs2 - else - let - fun sub (e as Value j) = if i = j then App (n, []) else e - | sub e = e - in check (map (subst sub) vs1) (map (subst sub) vs2) end - | check vs1 (v :: vs2) = check (v :: vs1) vs2 - in check [] end - -fun remove_int_nat_coercions terms vs = - let - fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n - - val (default_int, ints) = - (case find_first (match [@{const of_nat (int)}]) vs of - NONE => (NONE, []) - | SOME (_, cases) => - let val (cs, (_, e)) = split_last cases - in (SOME e, map (apfst hd) cs) end) - - fun nat_of @{typ nat} (v as Value _) = - AList.lookup (op =) ints v |> the_default (the_default v default_int) - | nat_of _ e = e - - fun subst_nat T k ([], e) = - let fun app f i = if i <= 0 then I else app f (i-1) o f - in ([], nat_of (app Term.range_type k T) e) end - | subst_nat T k (arg :: args, e) = - subst_nat (Term.range_type T) (k-1) (args, e) - |> apfst (cons (nat_of (Term.domain_type T) arg)) - - fun subst_nats (v as ((n, k), cases)) = - (case Symtab.lookup terms n of - NONE => v - | SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases)) - in - map subst_nats vs - |> filter_out (match [@{const of_nat (int)}, @{const nat}]) - end - -fun filter_valid_valuations terms = map_filter (fn - (_, []) => NONE - | ((n, i), cases) => - let - fun valid_expr (Array a) = valid_array a - | valid_expr (App (n, es)) = - Symtab.defined terms n andalso forall valid_expr es - | valid_expr _ = true - and valid_array (Fresh e) = valid_expr e - | valid_array (Store ((a, e1), e2)) = - valid_array a andalso valid_expr e1 andalso valid_expr e2 - fun valid_case (es, e) = forall valid_expr (e :: es) - in - if not (forall valid_case cases) then NONE - else Option.map (rpair cases o rpair i) (Symtab.lookup terms n) - end) - -end + |> map_filter (annotate terms) (* translation into terms *) -fun with_context ctxt terms f vs = - fst (fold_map f vs (ctxt, terms, Inttab.empty)) +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 -fun fresh_term T (ctxt, terms, values) = - let val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt - in (Free (n, T), (ctxt', terms, values)) end + 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 term_of_value T i (cx as (_, _, values)) = - (case Inttab.lookup values i of - SOME t => (t, cx) + 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, (ctxt', terms', values')) = fresh_term T cx - in (t, (ctxt', terms', Inttab.update (i, t) values')) end) - -fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx) + let val t = Var (("fresh", 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} @@ -188,18 +122,16 @@ | 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 (Value i) = pair (Var (("value", i), T)) | trans_expr T (Array a) = trans_array T a - | trans_expr _ (App (n, es)) = - let val get_Ts = take (length es) o Term.binder_types o Term.fastype_of + | 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 - get_term n #-> (fn t => - fold_map (uncurry trans_expr) (get_Ts t ~~ es) #>> - Term.list_comb o pair t) - end + fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t + end) and trans_array T a = - let val dT = Term.domain_type T and rT = Term.range_type T + let val (dT, rT) = U.split_type T in (case a of Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t)) @@ -232,35 +164,131 @@ fun mk_lambda Ts (t, pats) = fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats -fun translate' T i [([], e)] = - if i = 0 then trans_expr T e - else - let val ((Us1, Us2), U) = Term.strip_type T |>> chop i - in trans_expr (Us2 ---> U) e #>> mk_lambda Us1 o rpair [] end - | translate' T i cases = - let - val (pat_cases, def) = split_last cases |> apsnd snd - val ((Us1, Us2), U) = Term.strip_type T |>> chop i - in - trans_expr (Us2 ---> U) def ##>> - fold_map (trans_pattern T) pat_cases #>> - mk_lambda Us1 - end +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 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 translate ((t, i), cases) = - translate' (Term.fastype_of t) i cases #>> HOLogic.mk_eq o pair t + 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_simple_eqs (eqs, defs) = + let + fun add_rewr (l as Const _) (r as Var _) = SOME (r, l) + | add_rewr (l as Free _) (r as Var _) = SOME (r, l) + | add_rewr _ _ = NONE + val (rs, eqs') = partition_eqs add_rewr eqs + + fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u + | is_trivial _ = false + in pairself (replace_vars rs #> filter_out is_trivial) (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 ls - |> map_filter reduce_function - |> drop_skolem_constants terms - |> substitute_constants terms - |> remove_int_nat_coercions terms - |> filter_valid_valuations terms - |> with_context ctxt terms translate + read_cex terms ls + |> with_context terms translate + |> apfst flat o split_list + |> remove_int_nat_coercions + |> unfold_funapp + |> unfold_simple_eqs + |>> map swap_free + |>> filter is_free_constraint + |> frees_for_vars ctxt + ||> filter is_const_def end