# HG changeset patch # User boehmes # Date 1288086563 -7200 # Node ID 57f5db2a48a3d6c73e006f2d607bb396a3564a5f # Parent a462d5207aa6ead74bd6e128d6e18e168d60d56b added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed) diff -r a462d5207aa6 -r 57f5db2a48a3 src/HOL/Tools/SMT/smt_solver.ML --- 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 #> diff -r a462d5207aa6 -r 57f5db2a48a3 src/HOL/Tools/SMT/z3_proof_reconstruction.ML --- 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 diff -r a462d5207aa6 -r 57f5db2a48a3 src/HOL/Tools/SMT/z3_proof_tools.ML --- 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