# HG changeset patch # User boehmes # Date 1288085966 -7200 # Node ID 539d07b00e5f04835e0715b1ef0ac5991be83d5c # Parent 53935145128618c87c4a2fa88306de3cd05568db keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs diff -r 539351451286 -r 539d07b00e5f src/HOL/Tools/SMT/cvc3_solver.ML --- a/src/HOL/Tools/SMT/cvc3_solver.ML Tue Oct 26 11:31:03 2010 +0200 +++ b/src/HOL/Tools/SMT/cvc3_solver.ML Tue Oct 26 11:39:26 2010 +0200 @@ -39,7 +39,7 @@ command = {env_var=env_var, remote_name=SOME solver_name}, arguments = options, interface = SMTLIB_Interface.interface, - reconstruct = pair o oracle } + reconstruct = pair o pair [] o oracle } val setup = Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => diff -r 539351451286 -r 539d07b00e5f src/HOL/Tools/SMT/smt_monomorph.ML --- a/src/HOL/Tools/SMT/smt_monomorph.ML Tue Oct 26 11:31:03 2010 +0200 +++ b/src/HOL/Tools/SMT/smt_monomorph.ML Tue Oct 26 11:39:26 2010 +0200 @@ -6,7 +6,8 @@ signature SMT_MONOMORPH = sig - val monomorph: thm list -> Proof.context -> thm list * Proof.context + val monomorph: (int * thm) list -> Proof.context -> + (int * thm) list * Proof.context end structure SMT_Monomorph: SMT_MONOMORPH = @@ -33,9 +34,11 @@ fun tvar_consts_of thm = collect_consts_if typ_has_tvars insert_const thm [] -fun incr_indexes thms = - let fun inc thm idx = (Thm.incr_indexes idx thm, Thm.maxidx_of thm + idx + 1) - in fst (fold_map inc thms 0) end +fun incr_indexes irules = + let + fun inc (i, thm) idx = + ((i, Thm.incr_indexes idx thm), Thm.maxidx_of thm + idx + 1) + in fst (fold_map inc irules 0) end (* Compute all substitutions from the types "Ts" to all relevant @@ -71,7 +74,7 @@ (without schematic types) which do not occur in any of the previous rounds. Note that thus no schematic type variables are shared among theorems. *) -fun specialize thy all_grounds new_grounds (thm, scs) = +fun specialize thy all_grounds new_grounds (irule, scs) = let fun spec (subst, consts) next_grounds = [subst] @@ -80,7 +83,7 @@ |-> fold_map (apply_subst all_grounds consts) in fold_map spec scs #>> (fn scss => - (thm, fold (fold (insert (eq_snd (op =)))) scss [])) + (irule, fold (fold (insert (eq_snd (op =)))) scss [])) end @@ -89,16 +92,16 @@ computation uses only the constants occurring with schematic type variables in the propositions. To ease comparisons, such sets of costants are always kept in their initial order. *) -fun incremental_monomorph thy limit all_grounds new_grounds ths = +fun incremental_monomorph thy limit all_grounds new_grounds irules = let val all_grounds' = Symtab.merge_list (op =) (all_grounds, new_grounds) val spec = specialize thy all_grounds' new_grounds - val (ths', new_grounds') = fold_map spec ths Symtab.empty + val (irs, new_grounds') = fold_map spec irules Symtab.empty in - if Symtab.is_empty new_grounds' then ths' + if Symtab.is_empty new_grounds' then irs else if limit > 0 - then incremental_monomorph thy (limit-1) all_grounds' new_grounds' ths' - else (warning "SMT: monomorphization limit reached"; ths') + then incremental_monomorph thy (limit-1) all_grounds' new_grounds' irs + else (warning "SMT: monomorphization limit reached"; irs) end @@ -137,9 +140,9 @@ fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T) - fun inst thm subst = + fun inst (i, thm) subst = let val cTs = Vartab.fold (cons o cert) (fold complete Tenv subst) [] - in Thm.instantiate (cTs, []) thm end + in (i, Thm.instantiate (cTs, []) thm) end in uncurry (map o inst) end @@ -147,7 +150,7 @@ fun mono_all ctxt _ [] monos = (monos, ctxt) | mono_all ctxt limit polys monos = let - fun invent_types thm ctxt = + fun invent_types (_, thm) ctxt = let val (vs, Ss) = split_list (Term.add_tvars (Thm.prop_of thm) []) in ctxt @@ -159,7 +162,7 @@ val thy = ProofContext.theory_of ctxt' val ths = polys - |> map (fn thm => (thm, [(Vartab.empty, tvar_consts_of thm)])) + |> map (fn (_, thm) => (thm, [(Vartab.empty, tvar_consts_of thm)])) (* all constant names occurring with schematic types *) val ns = fold (fold (fold (insert (op =) o fst) o snd) o snd) ths [] @@ -167,11 +170,11 @@ (* all known instances with non-schematic types *) val grounds = Symtab.make (map (rpair []) ns) - |> fold (add_consts (K true)) monos - |> fold (add_consts (not o typ_has_tvars)) polys + |> fold (add_consts (K true) o snd) monos + |> fold (add_consts (not o typ_has_tvars) o snd) polys in polys - |> map (fn thm => (thm, [(Vartab.empty, tvar_consts_of thm)])) + |> map (fn (i, thm) => ((i, thm), [(Vartab.empty, tvar_consts_of thm)])) |> incremental_monomorph thy limit Symtab.empty grounds |> map (apsnd (filter_most_specific thy)) |> flat o map2 (instantiate thy) Tenvs @@ -192,9 +195,9 @@ The initial set of theorems must not contain any schematic term variables, and the final list of theorems does not contain any schematic type variables anymore. *) -fun monomorph thms ctxt = - thms - |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of) +fun monomorph irules ctxt = + irules + |> List.partition (Term.exists_type typ_has_tvars o Thm.prop_of o snd) |>> incr_indexes |-> mono_all ctxt monomorph_limit diff -r 539351451286 -r 539d07b00e5f src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Tue Oct 26 11:31:03 2010 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Oct 26 11:39:26 2010 +0200 @@ -17,9 +17,10 @@ signature SMT_NORMALIZE = sig - type extra_norm = thm list -> Proof.context -> thm list * Proof.context - val normalize: extra_norm -> bool -> thm list -> Proof.context -> - thm list * Proof.context + type extra_norm = (int * thm) list -> Proof.context -> + (int * thm) list * Proof.context + val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context -> + (int * thm) list * Proof.context val atomize_conv: Proof.context -> conv val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv end @@ -52,8 +53,8 @@ if_true_conv is_trivial_distinct (Conv.rewrs_conv thms) in fun trivial_distinct ctxt = - map ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ?? - Conv.fconv_rule (Conv.top_conv distinct_conv ctxt)) + map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ?? + Conv.fconv_rule (Conv.top_conv distinct_conv ctxt))) end @@ -72,8 +73,8 @@ val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms) in fun rewrite_bool_cases ctxt = - map ((Term.exists_subterm is_bool_case o Thm.prop_of) ?? - Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt)) + map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ?? + Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt))) end @@ -108,8 +109,8 @@ Conv.no_conv in fun normalize_numerals ctxt = - map ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ?? - Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt)) + map (apsnd ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ?? + Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt))) end @@ -117,7 +118,7 @@ (* embedding of standard natural number operations into integer operations *) local - val nat_embedding = @{lemma + val nat_embedding = map (pair ~1) @{lemma "nat (int n) = n" "i >= 0 --> int (nat i) = i" "i < 0 --> int (nat i) = 0" @@ -179,8 +180,8 @@ Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}]) in fun nat_as_int ctxt = - map ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt)) #> - exists (uses_nat_int o Thm.prop_of) ?? append nat_embedding + map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #> + exists (uses_nat_int o Thm.prop_of o snd) ?? append nat_embedding end @@ -362,12 +363,13 @@ if not (has_free_lambdas (Thm.prop_of thm)) then (thm, cx) else cx |> f (Thm.cprop_of thm) |>> (fn thm' => Thm.equal_elim thm' thm) in -fun lift_lambdas thms ctxt = +fun lift_lambdas irules ctxt = let val cx = (ctxt, Termtab.empty) + val (idxs, thms) = split_list irules val (thms', (ctxt', defs)) = fold_map (lift_lm (traverse [])) thms cx val eqs = Termtab.fold (cons o normalize_rule ctxt' o snd) defs [] - in (eqs @ thms', ctxt') end + in (map (pair ~1) eqs @ (idxs ~~ thms'), ctxt') end end @@ -384,8 +386,8 @@ | (Free (n, _), ts) => add (free n) (length ts) #> fold traverse ts | (Abs (_, _, u), ts) => fold traverse (u :: ts) | (_, ts) => fold traverse ts) - val prune = (fn (n, (true, i)) => Symtab.update (n, i) | _ => I) - fun prune_tab tab = Symtab.fold prune tab Symtab.empty + fun prune tab = Symtab.fold (fn (n, (true, i)) => + Symtab.update (n, i) | _ => I) tab Symtab.empty fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2 fun nary_conv conv1 conv2 ct = @@ -395,7 +397,7 @@ in conv (Symtab.update (free n, 0) tb) cx end) val fun_app_rule = @{lemma "f x == fun_app f x" by (simp add: fun_app_def)} in -fun explicit_application ctxt thms = +fun explicit_application ctxt irules = let fun sub_conv tb ctxt ct = (case Term.strip_comb (Thm.term_of ct) of @@ -423,8 +425,8 @@ if not (needs_exp_app tab (Thm.prop_of thm)) then thm else Conv.fconv_rule (sub_conv tab ctxt) thm - val tab = prune_tab (fold (traverse o Thm.prop_of) thms Symtab.empty) - in map (rewrite tab ctxt) thms end + val tab = prune (fold (traverse o Thm.prop_of o snd) irules Symtab.empty) + in map (apsnd (rewrite tab ctxt)) irules end end @@ -465,11 +467,11 @@ end) in -fun datatype_selectors thms ctxt = +fun datatype_selectors irules ctxt = let - val ns = Symtab.keys (fold (collect o Thm.prop_of) thms Symtab.empty) + val ns = Symtab.keys (fold (collect o Thm.prop_of o snd) irules Symtab.empty) val cs = fold (add_constructors (ProofContext.theory_of ctxt)) ns [] - in (thms, fold add_selector cs ctxt) end + in (irules, fold add_selector cs ctxt) end (* FIXME: also generate hypothetical definitions for the selectors *) end @@ -478,19 +480,20 @@ (* combined normalization *) -type extra_norm = thm list -> Proof.context -> thm list * Proof.context +type extra_norm = (int * thm) list -> Proof.context -> + (int * thm) list * Proof.context -fun with_context f thms ctxt = (f ctxt thms, ctxt) +fun with_context f irules ctxt = (f ctxt irules, ctxt) -fun normalize extra_norm with_datatypes thms ctxt = - thms +fun normalize extra_norm with_datatypes irules ctxt = + irules |> trivial_distinct ctxt |> rewrite_bool_cases ctxt |> normalize_numerals ctxt |> nat_as_int ctxt |> rpair ctxt |-> extra_norm - |-> with_context (fn cx => map (normalize_rule cx)) + |-> with_context (fn cx => map (apsnd (normalize_rule cx))) |-> SMT_Monomorph.monomorph |-> lift_lambdas |-> with_context explicit_application diff -r 539351451286 -r 539d07b00e5f src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 26 11:31:03 2010 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Oct 26 11:39:26 2010 +0200 @@ -17,7 +17,7 @@ arguments: string list, interface: interface, reconstruct: (string list * SMT_Translate.recon) -> Proof.context -> - thm * Proof.context } + (int list * thm) * Proof.context } (*options*) val timeout: int Config.T @@ -30,7 +30,7 @@ val select_certificates: string -> Context.generic -> Context.generic (*solvers*) - type solver = Proof.context -> thm list -> thm + type solver = Proof.context -> (int * thm) list -> int list * thm type solver_info = Context.generic -> Pretty.T list val add_solver: string * (Proof.context -> solver_config) -> Context.generic -> Context.generic @@ -41,6 +41,10 @@ val select_solver: string -> Context.generic -> Context.generic val solver_of: Context.generic -> solver + (*solver*) + val smt_solver: Proof.context -> ('a * thm) list -> 'a list * thm + val smt_filter: Proof.context -> ('a * thm) list -> 'a list * string + (*tactic*) val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic @@ -66,7 +70,7 @@ arguments: string list, interface: interface, reconstruct: (string list * SMT_Translate.recon) -> Proof.context -> - thm * Proof.context } + (int list * thm) * Proof.context } @@ -177,8 +181,8 @@ Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) () end -fun invoke translate_config comments command arguments thms ctxt = - thms +fun invoke translate_config comments command arguments irules ctxt = + irules |> SMT_Translate.translate translate_config ctxt comments ||> tap (trace_recon_data ctxt) |>> run_solver ctxt command arguments @@ -202,16 +206,17 @@ |-> SMT_Normalize.normalize extra_norm has_datatypes |-> invoke translate comments command arguments |-> reconstruct - |-> (fn thm => fn ctxt' => thm + |-> (fn (idxs, thm) => fn ctxt' => thm |> singleton (ProofContext.export ctxt' ctxt) - |> discharge_definitions) + |> discharge_definitions + |> pair idxs) end (* solver store *) -type solver = Proof.context -> thm list -> thm +type solver = Proof.context -> (int * thm) list -> int list * thm type solver_info = Context.generic -> Pretty.T list structure Solvers = Generic_Data @@ -259,6 +264,29 @@ +(* SMT solver *) + +val has_topsort = Term.exists_type (Term.exists_subtype (fn + TFree (_, []) => true + | TVar (_, []) => true + | _ => false)) + +fun smt_solver ctxt xrules = + (* without this test, we would run into problems when atomizing the rules: *) + if exists (has_topsort o Thm.prop_of o snd) xrules + then raise SMT "proof state contains the universal sort {}" + else + split_list xrules + ||>> solver_of (Context.Proof ctxt) ctxt o map_index I + |>> uncurry (map_filter o try o nth) o apsnd (distinct (op =)) + +fun smt_filter ctxt xrules = + (fst (smt_solver ctxt xrules), "") + handle SMT msg => ([], "SMT: " ^ msg) + | SMT_COUNTEREXAMPLE _ => ([], "SMT: potential counterexample") + + + (* SMT tactic *) local @@ -279,25 +307,13 @@ else (tac ctxt i st handle SMT msg => fail_tac (trace_msg ctxt (prefix "SMT: ")) msg st | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st) - - fun smt_solver rules ctxt = solver_of (Context.Proof ctxt) ctxt rules - - val has_topsort = Term.exists_type (Term.exists_subtype (fn - TFree (_, []) => true - | TVar (_, []) => true - | _ => false)) in fun smt_tac' pass_exns ctxt rules = CONVERSION (SMT_Normalize.atomize_conv ctxt) THEN' Tactic.rtac @{thm ccontr} THEN' SUBPROOF (fn {context, prems, ...} => - let val thms = rules @ prems - in - if exists (has_topsort o Thm.prop_of) thms - then fail_tac (trace_msg context I) - "SMT: proof state contains the universal sort {}" - else SAFE pass_exns (Tactic.rtac o smt_solver thms) context 1 - end) ctxt + let fun solve cx = snd (smt_solver cx (map (pair ()) (rules @ prems))) + in SAFE pass_exns (Tactic.rtac o solve) context 1 end) ctxt val smt_tac = smt_tac' false end @@ -357,7 +373,8 @@ val _ = Outer_Syntax.improper_command "smt_status" - "show the available SMT solvers and the currently selected solver" Keyword.diag + "show the available SMT solvers and the currently selected solver" + Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state => print_setup (Context.Proof (Toplevel.context_of state))))) diff -r 539351451286 -r 539d07b00e5f src/HOL/Tools/SMT/smt_translate.ML --- a/src/HOL/Tools/SMT/smt_translate.ML Tue Oct 26 11:31:03 2010 +0200 +++ b/src/HOL/Tools/SMT/smt_translate.ML Tue Oct 26 11:39:26 2010 +0200 @@ -43,9 +43,9 @@ typs: typ Symtab.table, terms: term Symtab.table, unfolds: thm list, - assms: thm list } + assms: (int * thm) list } - val translate: config -> Proof.context -> string list -> thm list -> + val translate: config -> Proof.context -> string list -> (int * thm) list -> string * recon end @@ -101,7 +101,7 @@ typs: typ Symtab.table, terms: term Symtab.table, unfolds: thm list, - assms: thm list } + assms: (int * thm) list } @@ -244,8 +244,9 @@ else as_term (in_term t) | _ => as_term (in_term t)) in - map (normalize ctxt) #> (fn thms => ((unfold_rules, term_bool' :: thms), - map (in_form o prop_of) (term_bool :: thms))) + map (apsnd (normalize ctxt)) #> (fn irules => + ((unfold_rules, (~1, term_bool') :: irules), + map (in_form o prop_of o snd) ((~1, term_bool) :: irules))) end @@ -318,7 +319,7 @@ (nth Tds i, map (mk_constructor ctxt (Tds, Tfs) (nth Tds i)) cs)) end) -fun relaxed thms = (([], thms), map prop_of thms) +fun relaxed irules = (([], irules), map (prop_of o snd) irules) fun with_context header f (ths, ts) = let val (us, context) = fold_map f ts empty_context diff -r 539351451286 -r 539d07b00e5f src/HOL/Tools/SMT/smtlib_interface.ML --- a/src/HOL/Tools/SMT/smtlib_interface.ML Tue Oct 26 11:31:03 2010 +0200 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Tue Oct 26 11:39:26 2010 +0200 @@ -30,7 +30,7 @@ (** facts about uninterpreted constants **) infix 2 ?? -fun (ex ?? f) thms = if exists (ex o Thm.prop_of) thms then f thms else thms +fun (ex ?? f) irules = irules |> exists (ex o Thm.prop_of o snd) irules ? f (* pairs *) @@ -40,7 +40,7 @@ val pair_type = (fn Type (@{type_name Product_Type.prod}, _) => true | _ => false) val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type) -val add_pair_rules = exists_pair_type ?? append pair_rules +val add_pair_rules = exists_pair_type ?? append (map (pair ~1) pair_rules) (* function update *) @@ -50,7 +50,7 @@ val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false) val exists_fun_upd = Term.exists_subterm is_fun_upd -val add_fun_upd_rules = exists_fun_upd ?? append fun_upd_rules +val add_fun_upd_rules = exists_fun_upd ?? append (map (pair ~1) fun_upd_rules) (* abs/min/max *) @@ -88,11 +88,11 @@ (* include additional facts *) -fun extra_norm has_datatypes thms ctxt = - thms +fun extra_norm has_datatypes irules ctxt = + irules |> not has_datatypes ? add_pair_rules |> add_fun_upd_rules - |> map (unfold_abs_min_max_defs ctxt) + |> map (apsnd (unfold_abs_min_max_defs ctxt)) |> rpair ctxt diff -r 539351451286 -r 539d07b00e5f src/HOL/Tools/SMT/yices_solver.ML --- a/src/HOL/Tools/SMT/yices_solver.ML Tue Oct 26 11:31:03 2010 +0200 +++ b/src/HOL/Tools/SMT/yices_solver.ML Tue Oct 26 11:39:26 2010 +0200 @@ -35,7 +35,7 @@ command = {env_var=env_var, remote_name=NONE}, arguments = options, interface = SMTLIB_Interface.interface, - reconstruct = pair o oracle } + reconstruct = pair o pair [] o oracle } val setup = Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) => diff -r 539351451286 -r 539d07b00e5f src/HOL/Tools/SMT/z3_interface.ML --- a/src/HOL/Tools/SMT/z3_interface.ML Tue Oct 26 11:31:03 2010 +0200 +++ b/src/HOL/Tools/SMT/z3_interface.ML Tue Oct 26 11:39:26 2010 +0200 @@ -74,13 +74,13 @@ | is_int_div_mod @{term "op mod :: int => _"} = true | is_int_div_mod _ = false - fun add_div_mod thms = - if exists (Term.exists_subterm is_int_div_mod o Thm.prop_of) thms - then [@{thm div_by_z3div}, @{thm mod_by_z3mod}] @ thms - else thms + fun add_div_mod irules = + if exists (Term.exists_subterm is_int_div_mod o Thm.prop_of o snd) irules + then [(~1, @{thm div_by_z3div}), (~1, @{thm mod_by_z3mod})] @ irules + else irules - fun extra_norm' has_datatypes thms = - SMTLIB_Interface.extra_norm has_datatypes (add_div_mod thms) + fun extra_norm' has_datatypes = + SMTLIB_Interface.extra_norm has_datatypes o add_div_mod fun z3_builtin_fun' _ (@{const_name z3div}, _) ts = SOME ("div", ts) | z3_builtin_fun' _ (@{const_name z3mod}, _) ts = SOME ("mod", ts) diff -r 539351451286 -r 539d07b00e5f src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Oct 26 11:31:03 2010 +0200 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Oct 26 11:39:26 2010 +0200 @@ -9,7 +9,7 @@ val add_z3_rule: thm -> Context.generic -> Context.generic val trace_assms: bool Config.T val reconstruct: string list * SMT_Translate.recon -> Proof.context -> - thm * Proof.context + (int list * thm) * Proof.context val setup: theory -> theory end @@ -750,7 +750,7 @@ fun prove ctxt unfolds assms vars = let - val assms' = prepare_assms ctxt unfolds assms + val assms' = prepare_assms ctxt unfolds (map snd assms) (* FIXME *) val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt) fun step r ps ct (cxp as (cx, ptab)) = @@ -821,7 +821,7 @@ | SOME (Proved p) => (p, cxp) | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx))) - fun result (p, (cx, _)) = (thm_of p, cx) + fun result (p, (cx, _)) = (([], thm_of p), cx) (*FIXME*) in (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map (K Unproved) ptab))) end diff -r 539351451286 -r 539d07b00e5f src/HOL/Tools/SMT/z3_solver.ML --- a/src/HOL/Tools/SMT/z3_solver.ML Tue Oct 26 11:31:03 2010 +0200 +++ b/src/HOL/Tools/SMT/z3_solver.ML Tue Oct 26 11:39:26 2010 +0200 @@ -72,7 +72,8 @@ {command = {env_var=env_var, remote_name=SOME solver_name}, arguments = cmdline_options ctxt, interface = Z3_Interface.interface with_datatypes, - reconstruct = if with_proof then prover else (fn r => `(oracle o pair r))} + reconstruct = + if with_proof then prover else (fn r => `(pair [] o oracle o pair r))} end val setup =