added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)

--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 11:46:19 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 11:49:23 2010 +0200
@@ -31,6 +31,7 @@
 
   (*options*)
   val oracle: bool Config.T
+  val filter_only: bool Config.T
   val datatypes: bool Config.T
   val timeout: int Config.T
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
@@ -53,8 +54,8 @@
   val solver_of: Context.generic -> solver
 
   (*filter*)
-  val smt_filter: Proof.state -> int -> ('a * thm) list ->
-    'a list * failure option
+  val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
+    {outcome: failure option, used_facts: 'a list, run_time_in_msecs: int}
 
   (*tactic*)
   val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
@@ -111,6 +112,9 @@
 
 val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true)
 
+val (filter_only, setup_filter_only) =
+  Attrib.config_bool "smt_filter_only" (K false)
+
 val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false)
 
 val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
@@ -248,6 +252,18 @@
       builtins=builtins', serialize=serialize}
   in (with_datatypes', translate') end
 
+fun trace_assumptions ctxt irules idxs =
+  let
+    val thms = filter (fn i => i >= 0) idxs
+      |> map_filter (AList.lookup (op =) irules)
+  in
+    if Config.get ctxt trace_used_facts andalso length thms > 0
+    then
+      tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
+        (map (Display.pretty_thm ctxt) thms)))
+    else ()
+  end
+
 fun gen_solver name info ctxt irules =
   let
     val {env_var, is_remote, options, more_options, interface, reconstruct} =
@@ -263,6 +279,7 @@
     |-> (fn (idxs, thm) => fn ctxt' => thm
     |> singleton (ProofContext.export ctxt' ctxt)
     |> discharge_definitions
+    |> tap (fn _ => trace_assumptions ctxt irules idxs)
     |> pair idxs)
   end
 
@@ -377,21 +394,26 @@
   then raise SMT (Other_Failure "proof state contains the universal sort {}")
   else solver_of (Context.Proof ctxt) ctxt irules
 
-fun smt_filter st i xrules =
+fun smt_filter remote time_limit st xrules i =
   let
     val {context, facts, goal} = Proof.goal st
+    val ctxt =
+      context
+      |> Config.put timeout (Time.toSeconds time_limit)
+      |> Config.put oracle false
+      |> Config.put filter_only true
     val cprop =
       Thm.cprem_of goal i
-      |> Thm.rhs_of o SMT_Normalize.atomize_conv context
+      |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt
       |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
     val irs = map (pair ~1) (Thm.assume cprop :: facts)
   in
     split_list xrules
-    ||>> solver_of (Context.Proof context) context o append irs o map_index I
-    |>> uncurry (map_filter o try o nth) o apsnd (distinct (op =))
-    |> rpair NONE o fst
+    ||> distinct (op =) o fst o smt_solver ctxt o append irs o map_index I
+    |-> map_filter o try o nth
+    |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs= ~1})
   end
-  handle SMT fail => ([], SOME fail)
+  handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs= ~1}
 
 
 
@@ -432,6 +454,7 @@
       (Thm.declaration_attribute o K o select_solver))
     "SMT solver configuration" #>
   setup_oracle #>
+  setup_filter_only #>
   setup_datatypes #>
   setup_timeout #>
   setup_trace #>

--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Oct 26 11:46:19 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Oct 26 11:49:23 2010 +0200
@@ -7,7 +7,6 @@
 signature Z3_PROOF_RECONSTRUCTION =
 sig
   val add_z3_rule: thm -> Context.generic -> Context.generic
-  val trace_assms: bool Config.T
   val reconstruct: Proof.context -> SMT_Translate.recon -> string list ->
     (int list * thm) * Proof.context
   val setup: theory -> theory
@@ -138,9 +137,6 @@
 
 (* assumption *)
 
-val (trace_assms, trace_assms_setup) =
-  Attrib.config_bool "z3_trace_assms" (K false)
-
 local
   val remove_trigger = @{lemma "trigger t p == p"
     by (rule eq_reflection, rule trigger_def)}
@@ -150,28 +146,28 @@
   fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
     (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
 
-  fun rewrites ctxt eqs = map (Conv.fconv_rule (rewrite_conv ctxt eqs))
+  fun rewrites f ctxt eqs = map (f (Conv.fconv_rule (rewrite_conv ctxt eqs)))
 
-  fun trace ctxt thm =
-    if Config.get ctxt trace_assms
-    then tracing (Display.string_of_thm ctxt thm)
-    else ()
-
+  fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
   fun lookup_assm ctxt assms ct =
-    (case T.net_instance assms ct of
-      SOME thm => (trace ctxt thm; thm)
+    (case T.net_instance' burrow_snd_option assms ct of
+      SOME ithm => ithm
     | _ => z3_exn ("not asserted: " ^
         quote (Syntax.string_of_term ctxt (Thm.term_of ct))))
 in
 fun prepare_assms ctxt unfolds assms =
   let
-    val unfolds' = rewrites ctxt [L.rewrite_true] unfolds
-    val assms' = rewrites ctxt (union Thm.eq_thm unfolds' prep_rules) assms
-  in (unfolds', T.thm_net_of assms') end
+    val unfolds' = rewrites I ctxt [L.rewrite_true] unfolds
+    val assms' =
+      rewrites apsnd ctxt (union Thm.eq_thm unfolds' prep_rules) assms
+  in (unfolds', T.thm_net_of snd assms') end
 
 fun asserted ctxt (unfolds, assms) ct =
   let val revert_conv = rewrite_conv ctxt unfolds
-  in Thm (T.with_conv revert_conv (lookup_assm ctxt assms) ct) end
+  in Thm (T.with_conv revert_conv (snd o lookup_assm ctxt assms) ct) end
+
+fun find_assm ctxt (unfolds, assms) ct =
+  fst (lookup_assm ctxt assms (Thm.rhs_of (rewrite_conv ctxt unfolds ct)))
 end
 
 
@@ -746,91 +742,115 @@
 
 (* overall reconstruction procedure *)
 
-fun not_supported r =
-  raise Fail ("Z3: proof rule not implemented: " ^ quote (P.string_of_rule r))
-
-fun prove ctxt unfolds assms vars =
-  let
-    val assms' = prepare_assms ctxt unfolds (map snd assms) (* FIXME *)
-    val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt)
+local
+  fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
+    quote (P.string_of_rule r))
 
-    fun step r ps ct (cxp as (cx, ptab)) =
-      (case (r, ps) of
-        (* core rules *)
-        (P.TrueAxiom, _) => (Thm L.true_thm, cxp)
-      | (P.Asserted, _) => (asserted cx assms' ct, cxp)
-      | (P.Goal, _) => (asserted cx assms' ct, cxp)
-      | (P.ModusPonens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
-      | (P.ModusPonensOeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
-      | (P.AndElim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx
-      | (P.NotOrElim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx
-      | (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
-      | (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
-      | (P.UnitResolution, (p, _) :: ps) =>
-          (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
-      | (P.IffTrue, [(p, _)]) => (iff_true (thm_of p), cxp)
-      | (P.IffFalse, [(p, _)]) => (iff_false (thm_of p), cxp)
-      | (P.Distributivity, _) => (distributivity cx ct, cxp)
-      | (P.DefAxiom, _) => (def_axiom cx ct, cxp)
-      | (P.IntroDef, _) => intro_def ct cx ||> rpair ptab
-      | (P.ApplyDef, [(p, _)]) => (apply_def (thm_of p), cxp)
-      | (P.IffOeq, [(p, _)]) => (p, cxp)
-      | (P.NnfPos, _) => (nnf cx vars (map fst ps) ct, cxp)
-      | (P.NnfNeg, _) => (nnf cx vars (map fst ps) ct, cxp)
+  fun step assms simpset vars r ps ct (cxp as (cx, ptab)) =
+    (case (r, ps) of
+      (* core rules *)
+      (P.TrueAxiom, _) => (Thm L.true_thm, cxp)
+    | (P.Asserted, _) => (asserted cx assms ct, cxp)
+    | (P.Goal, _) => (asserted cx assms ct, cxp)
+    | (P.ModusPonens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
+    | (P.ModusPonensOeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
+    | (P.AndElim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx
+    | (P.NotOrElim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx
+    | (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
+    | (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
+    | (P.UnitResolution, (p, _) :: ps) =>
+        (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
+    | (P.IffTrue, [(p, _)]) => (iff_true (thm_of p), cxp)
+    | (P.IffFalse, [(p, _)]) => (iff_false (thm_of p), cxp)
+    | (P.Distributivity, _) => (distributivity cx ct, cxp)
+    | (P.DefAxiom, _) => (def_axiom cx ct, cxp)
+    | (P.IntroDef, _) => intro_def ct cx ||> rpair ptab
+    | (P.ApplyDef, [(p, _)]) => (apply_def (thm_of p), cxp)
+    | (P.IffOeq, [(p, _)]) => (p, cxp)
+    | (P.NnfPos, _) => (nnf cx vars (map fst ps) ct, cxp)
+    | (P.NnfNeg, _) => (nnf cx vars (map fst ps) ct, cxp)
 
-        (* equality rules *)
-      | (P.Reflexivity, _) => (refl ct, cxp)
-      | (P.Symmetry, [(p, _)]) => (symm p, cxp)
-      | (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
-      | (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
-      | (P.Commutativity, _) => (commutativity ct, cxp)
+      (* equality rules *)
+    | (P.Reflexivity, _) => (refl ct, cxp)
+    | (P.Symmetry, [(p, _)]) => (symm p, cxp)
+    | (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
+    | (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
+    | (P.Commutativity, _) => (commutativity ct, cxp)
+
+      (* quantifier rules *)
+    | (P.QuantIntro, [(p, _)]) => (quant_intro vars p ct, cxp)
+    | (P.PullQuant, _) => (pull_quant cx ct, cxp)
+    | (P.PushQuant, _) => (push_quant cx ct, cxp)
+    | (P.ElimUnusedVars, _) => (elim_unused_vars cx ct, cxp)
+    | (P.DestEqRes, _) => (dest_eq_res cx ct, cxp)
+    | (P.QuantInst, _) => (quant_inst ct, cxp)
+    | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
+
+      (* theory rules *)
+    | (P.ThLemma, _) =>
+        (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
+    | (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp)
+    | (P.RewriteStar, ps) =>
+        (rewrite cx simpset (map fst ps) ct, cxp)
 
-        (* quantifier rules *)
-      | (P.QuantIntro, [(p, _)]) => (quant_intro vars p ct, cxp)
-      | (P.PullQuant, _) => (pull_quant cx ct, cxp)
-      | (P.PushQuant, _) => (push_quant cx ct, cxp)
-      | (P.ElimUnusedVars, _) => (elim_unused_vars cx ct, cxp)
-      | (P.DestEqRes, _) => (dest_eq_res cx ct, cxp)
-      | (P.QuantInst, _) => (quant_inst ct, cxp)
-      | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
+    | (P.NnfStar, _) => not_supported r
+    | (P.CnfStar, _) => not_supported r
+    | (P.TransitivityStar, _) => not_supported r
+    | (P.PullQuantStar, _) => not_supported r
 
-        (* theory rules *)
-      | (P.ThLemma, _) =>
-          (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
-      | (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp)
-      | (P.RewriteStar, ps) =>
-          (rewrite cx simpset (map fst ps) ct, cxp)
+    | _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^
+       " has an unexpected number of arguments."))
 
-      | (P.NnfStar, _) => not_supported r
-      | (P.CnfStar, _) => not_supported r
-      | (P.TransitivityStar, _) => not_supported r
-      | (P.PullQuantStar, _) => not_supported r
-
-      | _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^
-         " has an unexpected number of arguments."))
-
-    fun conclude idx rule prop (ps, cxp) =
-      trace_rule idx step rule ps prop cxp
-      |-> (fn p => apsnd (Inttab.update (idx, Proved p)) #> pair p)
+  fun prove ctxt assms vars =
+    let
+      val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt)
+ 
+      fun conclude idx rule prop (ps, cxp) =
+        trace_rule idx (step assms simpset vars) rule ps prop cxp
+        |-> (fn p => apsnd (Inttab.update (idx, Proved p)) #> pair p)
+ 
+      fun lookup idx (cxp as (_, ptab)) =
+        (case Inttab.lookup ptab idx of
+          SOME (Unproved (P.Proof_Step {rule, prems, prop})) =>
+            fold_map lookup prems cxp
+            |>> map2 rpair prems
+            |> conclude idx rule prop
+        | SOME (Proved p) => (p, cxp)
+        | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
+ 
+      fun result (p, (cx, _)) = (thm_of p, cx)
+    in
+      (fn idx => result o lookup idx o pair ctxt o Inttab.map (K Unproved))
+    end
 
-    fun lookup idx (cxp as (_, ptab)) =
-      (case Inttab.lookup ptab idx of
-        SOME (Unproved (P.Proof_Step {rule, prems, prop})) =>
-          fold_map lookup prems cxp
-          |>> map2 rpair prems
-          |> conclude idx rule prop
-      | SOME (Proved p) => (p, cxp)
-      | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
+  fun filter_assms ctxt assms ptab =
+    let
+      fun step r ct =
+        (case r of
+          P.Asserted => insert (op =) (find_assm ctxt assms ct)
+        | P.Goal => insert (op =) (find_assm ctxt assms ct)
+        | _ => I)
 
-    fun result (p, (cx, _)) = (([], thm_of p), cx) (*FIXME*)
+      fun lookup idx =
+        (case Inttab.lookup ptab idx of
+          SOME (P.Proof_Step {rule, prems, prop}) =>
+            fold lookup prems #> step rule prop
+        | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
+    in lookup end
+in
+
+fun reconstruct ctxt {typs, terms, unfolds, assms} output =
+  let
+    val (idx, (ptab, vars, cx)) = P.parse ctxt typs terms output
+    val assms' = prepare_assms cx unfolds assms
   in
-    (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map (K Unproved) ptab)))
+    if Config.get cx SMT_Solver.filter_only
+    then ((filter_assms cx assms' ptab idx [], @{thm TrueI}), cx)
+    else apfst (pair []) (prove cx assms' vars idx ptab)
   end
 
-fun reconstruct ctxt {typs, terms, unfolds, assms} output =
-  P.parse ctxt typs terms output
-  |> (fn (idx, (ptab, vars, cx)) => prove cx unfolds assms vars (idx, ptab))
+end
 
-val setup = trace_assms_setup #> z3_rules_setup #> Z3_Simps.setup
+val setup = z3_rules_setup #> Z3_Simps.setup
 
 end

--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Tue Oct 26 11:46:19 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Tue Oct 26 11:49:23 2010 +0200
@@ -13,7 +13,9 @@
   val as_meta_eq: cterm -> cterm
 
   (* theorem nets *)
-  val thm_net_of: thm list -> thm Net.net
+  val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
+  val net_instance': ((thm -> thm option) -> 'a -> 'a option) -> 'a Net.net ->
+    cterm -> 'a option
   val net_instance: thm Net.net -> cterm -> thm option
 
   (* proof combinators *)
@@ -67,16 +69,18 @@
 
 (* theorem nets *)
 
-fun thm_net_of thms =
-  let fun insert thm = Net.insert_term (K false) (Thm.prop_of thm, thm)
-  in fold insert thms Net.empty end
+fun thm_net_of f xthms =
+  let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
+  in fold insert xthms Net.empty end
 
 fun maybe_instantiate ct thm =
   try Thm.first_order_match (Thm.cprop_of thm, ct)
   |> Option.map (fn inst => Thm.instantiate inst thm)
 
-fun first_of thms ct = get_first (maybe_instantiate ct) thms
-fun net_instance net ct = first_of (Net.match_term net (Thm.term_of ct)) ct
+fun net_instance' f net ct =
+  let fun first_of f xthms ct = get_first (f (maybe_instantiate ct)) xthms 
+  in first_of f (Net.match_term net (Thm.term_of ct)) ct end
+val net_instance = net_instance' I