# HG changeset patch
# User boehmes
# Date 1288369029 -7200
# Node ID 0fc78bb54f18aa2e5cea31f85ad4625323bfd579
# Parent  4e3a3461c1a6689aead865c71759d0fcb1ebad0e
optionally drop assumptions which cannot be preprocessed

diff -r 4e3a3461c1a6 -r 0fc78bb54f18 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:08 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Oct 29 18:17:09 2010 +0200
@@ -19,7 +19,8 @@
 sig
   type extra_norm = bool -> (int * thm) list -> Proof.context ->
     (int * thm) list * Proof.context
-  val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
+  val normalize: (Proof.context -> (thm -> string) -> thm -> unit) -> bool ->
+    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
@@ -486,18 +487,28 @@
 
 fun with_context f irules ctxt = (f ctxt irules, ctxt)
 
-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_datatypes
-  |-> with_context (fn cx => map (apsnd (normalize_rule cx)))
-  |-> SMT_Monomorph.monomorph
-  |-> lift_lambdas
-  |-> with_context explicit_application
-  |-> (if with_datatypes then datatype_selectors else pair)
+fun normalize trace keep_assms extra_norm with_datatypes irules ctxt =
+  let
+    fun norm f ctxt' (i, thm) =
+      if keep_assms then SOME (i, f ctxt' thm)
+      else
+        (case try (f ctxt') thm of
+          SOME thm' => SOME (i, thm')
+        | NONE => (trace ctxt' (prefix ("SMT warning: " ^
+            "dropping assumption: ") o Display.string_of_thm ctxt') thm; NONE))
+  in
+    irules
+    |> trivial_distinct ctxt
+    |> rewrite_bool_cases ctxt
+    |> normalize_numerals ctxt
+    |> nat_as_int ctxt
+    |> rpair ctxt
+    |-> extra_norm with_datatypes
+    |-> with_context (map_filter o norm normalize_rule)
+    |-> SMT_Monomorph.monomorph
+    |-> lift_lambdas
+    |-> with_context explicit_application
+    |-> (if with_datatypes then datatype_selectors else pair)
+  end
 
 end
diff -r 4e3a3461c1a6 -r 0fc78bb54f18 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 29 18:17:08 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 29 18:17:09 2010 +0200
@@ -34,6 +34,7 @@
   val oracle: bool Config.T
   val filter_only: bool Config.T
   val datatypes: bool Config.T
+  val keep_assms: bool Config.T
   val timeout: int Config.T
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
   val traceN: string
@@ -123,6 +124,9 @@
 
 val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false)
 
+val (keep_assms, setup_keep_assms) =
+  Attrib.config_bool "smt_keep_assms" (K true)
+
 val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
 
 fun with_timeout ctxt f x =
@@ -294,9 +298,10 @@
     val (with_datatypes, translate') =
       set_has_datatypes (Config.get ctxt datatypes) translate
     val cmd = (rm, env_var, is_remote, name)
+    val keep = Config.get ctxt keep_assms
   in
     (irules, ctxt)
-    |-> SMT_Normalize.normalize extra_norm with_datatypes
+    |-> SMT_Normalize.normalize trace_msg keep extra_norm with_datatypes
     |-> invoke translate' name cmd more_options options
     |-> reconstruct
     |-> (fn (idxs, thm) => fn ctxt' => thm
@@ -431,6 +436,7 @@
       |> Config.put timeout (Time.toSeconds time_limit)
       |> Config.put oracle false
       |> Config.put filter_only true
+      |> Config.put keep_assms false
     val cprop =
       Thm.cprem_of goal i
       |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt
@@ -483,6 +489,7 @@
   setup_oracle #>
   setup_filter_only #>
   setup_datatypes #>
+  setup_keep_assms #>
   setup_timeout #>
   setup_trace #>
   setup_trace_used_facts #>