# HG changeset patch # User blanchet # Date 1380747282 -7200 # Node ID 227908156cd2013f6ffbfe8d5acf49b9d6706a1d # Parent 04715fecbda6224712ee73e59d5dda8b84fa6acf make SMT integration slacker w.r.t. bad apples (facts) diff -r 04715fecbda6 -r 227908156cd2 src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML Wed Oct 02 22:54:42 2013 +0200 +++ b/src/HOL/Tools/SMT/smt_config.ML Wed Oct 02 22:54:42 2013 +0200 @@ -33,7 +33,6 @@ val monomorph_limit: int Config.T val monomorph_instances: int Config.T val infer_triggers: bool Config.T - val drop_bad_facts: bool Config.T val filter_only_facts: bool Config.T val debug_files: string Config.T @@ -161,7 +160,6 @@ val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10) val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500) val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false) -val drop_bad_facts = Attrib.setup_config_bool @{binding smt_drop_bad_facts} (K false) val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false) val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "") diff -r 04715fecbda6 -r 227908156cd2 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Oct 02 22:54:42 2013 +0200 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Oct 02 22:54:42 2013 +0200 @@ -6,6 +6,7 @@ signature SMT_NORMALIZE = sig + val drop_fact_warning: Proof.context -> thm -> unit val atomize_conv: Proof.context -> conv type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list val add_extra_norm: SMT_Utils.class * extra_norm -> Context.generic -> @@ -18,6 +19,10 @@ structure SMT_Normalize: SMT_NORMALIZE = struct +fun drop_fact_warning ctxt = + SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o + Display.string_of_thm ctxt) + (* general theorem normalizations *) @@ -329,16 +334,10 @@ |> Drule.forall_intr_vars |> Conv.fconv_rule (gen_normalize1_conv ctxt weight) -fun drop_fact_warning ctxt = - let val pre = prefix "Warning: dropping assumption: " - in SMT_Config.verbose_msg ctxt (pre o Display.string_of_thm ctxt) end - fun gen_norm1_safe ctxt (i, (weight, thm)) = - if Config.get ctxt SMT_Config.drop_bad_facts then - (case try (gen_normalize1 ctxt weight) thm of - SOME thm' => SOME (i, thm') - | NONE => (drop_fact_warning ctxt thm; NONE)) - else SOME (i, gen_normalize1 ctxt weight thm) + (case try (gen_normalize1 ctxt weight) thm of + SOME thm' => SOME (i, thm') + | NONE => (drop_fact_warning ctxt thm; NONE)) fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms diff -r 04715fecbda6 -r 227908156cd2 src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Wed Oct 02 22:54:42 2013 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Oct 02 22:54:42 2013 +0200 @@ -257,11 +257,13 @@ | _ => false)) (* without this test, we would run into problems when atomizing the rules: *) -fun check_topsort iwthms = - if exists (has_topsort o Thm.prop_of o snd o snd) iwthms then - raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^ - "contains the universal sort {}")) - else () +fun check_topsort ctxt thm = + if has_topsort (Thm.prop_of thm) then + (SMT_Normalize.drop_fact_warning ctxt thm; TrueI) + else + thm + +fun check_topsorts ctxt iwthms = map (apsnd (apsnd (check_topsort ctxt))) iwthms (* filter *) @@ -277,7 +279,6 @@ val ctxt = ctxt |> Config.put SMT_Config.oracle false - |> Config.put SMT_Config.drop_bad_facts true |> Config.put SMT_Config.filter_only_facts true val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal @@ -291,7 +292,7 @@ map snd xwthms |> map_index I |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) - |> tap check_topsort + |> check_topsorts ctxt' |> gen_preprocess ctxt' |> pair (map (apsnd snd) xwthms) end @@ -332,7 +333,7 @@ fun solve ctxt iwthms = iwthms - |> tap check_topsort + |> check_topsorts ctxt |> apply_solver ctxt |>> trace_assumptions ctxt iwthms |> snd