optionally drop assumptions which cannot be preprocessed
authorboehmes
Fri Oct 29 18:17:09 2010 +0200 (2010-10-29)
changeset 402780fc78bb54f18
parent 40277 4e3a3461c1a6
child 40279 96365b4ae7b6
optionally drop assumptions which cannot be preprocessed
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_solver.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:08 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:09 2010 +0200
     1.3 @@ -19,7 +19,8 @@
     1.4  sig
     1.5    type extra_norm = bool -> (int * thm) list -> Proof.context ->
     1.6      (int * thm) list * Proof.context
     1.7 -  val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
     1.8 +  val normalize: (Proof.context -> (thm -> string) -> thm -> unit) -> bool ->
     1.9 +    extra_norm -> bool -> (int * thm) list -> Proof.context ->
    1.10      (int * thm) list * Proof.context
    1.11    val atomize_conv: Proof.context -> conv
    1.12    val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
    1.13 @@ -486,18 +487,28 @@
    1.14  
    1.15  fun with_context f irules ctxt = (f ctxt irules, ctxt)
    1.16  
    1.17 -fun normalize extra_norm with_datatypes irules ctxt =
    1.18 -  irules
    1.19 -  |> trivial_distinct ctxt
    1.20 -  |> rewrite_bool_cases ctxt
    1.21 -  |> normalize_numerals ctxt
    1.22 -  |> nat_as_int ctxt
    1.23 -  |> rpair ctxt
    1.24 -  |-> extra_norm with_datatypes
    1.25 -  |-> with_context (fn cx => map (apsnd (normalize_rule cx)))
    1.26 -  |-> SMT_Monomorph.monomorph
    1.27 -  |-> lift_lambdas
    1.28 -  |-> with_context explicit_application
    1.29 -  |-> (if with_datatypes then datatype_selectors else pair)
    1.30 +fun normalize trace keep_assms extra_norm with_datatypes irules ctxt =
    1.31 +  let
    1.32 +    fun norm f ctxt' (i, thm) =
    1.33 +      if keep_assms then SOME (i, f ctxt' thm)
    1.34 +      else
    1.35 +        (case try (f ctxt') thm of
    1.36 +          SOME thm' => SOME (i, thm')
    1.37 +        | NONE => (trace ctxt' (prefix ("SMT warning: " ^
    1.38 +            "dropping assumption: ") o Display.string_of_thm ctxt') thm; NONE))
    1.39 +  in
    1.40 +    irules
    1.41 +    |> trivial_distinct ctxt
    1.42 +    |> rewrite_bool_cases ctxt
    1.43 +    |> normalize_numerals ctxt
    1.44 +    |> nat_as_int ctxt
    1.45 +    |> rpair ctxt
    1.46 +    |-> extra_norm with_datatypes
    1.47 +    |-> with_context (map_filter o norm normalize_rule)
    1.48 +    |-> SMT_Monomorph.monomorph
    1.49 +    |-> lift_lambdas
    1.50 +    |-> with_context explicit_application
    1.51 +    |-> (if with_datatypes then datatype_selectors else pair)
    1.52 +  end
    1.53  
    1.54  end
     2.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 29 18:17:08 2010 +0200
     2.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 29 18:17:09 2010 +0200
     2.3 @@ -34,6 +34,7 @@
     2.4    val oracle: bool Config.T
     2.5    val filter_only: bool Config.T
     2.6    val datatypes: bool Config.T
     2.7 +  val keep_assms: bool Config.T
     2.8    val timeout: int Config.T
     2.9    val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
    2.10    val traceN: string
    2.11 @@ -123,6 +124,9 @@
    2.12  
    2.13  val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false)
    2.14  
    2.15 +val (keep_assms, setup_keep_assms) =
    2.16 +  Attrib.config_bool "smt_keep_assms" (K true)
    2.17 +
    2.18  val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
    2.19  
    2.20  fun with_timeout ctxt f x =
    2.21 @@ -294,9 +298,10 @@
    2.22      val (with_datatypes, translate') =
    2.23        set_has_datatypes (Config.get ctxt datatypes) translate
    2.24      val cmd = (rm, env_var, is_remote, name)
    2.25 +    val keep = Config.get ctxt keep_assms
    2.26    in
    2.27      (irules, ctxt)
    2.28 -    |-> SMT_Normalize.normalize extra_norm with_datatypes
    2.29 +    |-> SMT_Normalize.normalize trace_msg keep extra_norm with_datatypes
    2.30      |-> invoke translate' name cmd more_options options
    2.31      |-> reconstruct
    2.32      |-> (fn (idxs, thm) => fn ctxt' => thm
    2.33 @@ -431,6 +436,7 @@
    2.34        |> Config.put timeout (Time.toSeconds time_limit)
    2.35        |> Config.put oracle false
    2.36        |> Config.put filter_only true
    2.37 +      |> Config.put keep_assms false
    2.38      val cprop =
    2.39        Thm.cprem_of goal i
    2.40        |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt
    2.41 @@ -483,6 +489,7 @@
    2.42    setup_oracle #>
    2.43    setup_filter_only #>
    2.44    setup_datatypes #>
    2.45 +  setup_keep_assms #>
    2.46    setup_timeout #>
    2.47    setup_trace #>
    2.48    setup_trace_used_facts #>