keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs
--- 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) =>
--- 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
--- 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
--- 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)))))
--- 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
--- 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
--- 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) =>
--- 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)
--- 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
--- 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 =