# HG changeset patch
# User blanchet
# Date 1292902397 -3600
# Node ID 0ea5b9c7d233952964b4dbfa352e881dd20fda32
# Parent  66edbd0f7a2e0e704bcb6bf8cb621fe907531233
proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them;
removed "is_builtin_ext", which is too limited an API to be useful in light of the aforementioned restriction

diff -r 66edbd0f7a2e -r 0ea5b9c7d233 src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Tue Dec 21 03:56:51 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Tue Dec 21 04:33:17 2010 +0100
@@ -41,7 +41,6 @@
   val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
   val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
   val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
-  val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
 end
 
 structure SMT_Builtin: SMT_BUILTIN =
@@ -219,8 +218,4 @@
   | SOME (_, Ext f) => f ctxt T ts
   | NONE => false)
 
-fun is_builtin_ext ctxt c ts =
-  is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) orelse 
-  is_builtin_fun_ext ctxt c ts
-
 end
diff -r 66edbd0f7a2e -r 0ea5b9c7d233 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Dec 21 03:56:51 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Dec 21 04:33:17 2010 +0100
@@ -40,7 +40,7 @@
     -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
   val relevant_facts :
     Proof.context -> bool -> real * real -> int
-    -> (string * typ -> term list -> bool) -> relevance_fudge
+    -> (string * typ -> term list -> bool * term list) -> relevance_fudge
     -> relevance_override -> thm list -> term list -> term
     -> ((string * locality) * thm) list
 end;
@@ -267,9 +267,11 @@
        prover, we introduce a fresh constant to simulate the effect of
        Skolemization. *)
     fun do_const const x ts =
-      (not (is_built_in_const x ts)
-       ? add_pconst_to_table also_skolems (rich_pconst thy const x))
-      #> fold do_term ts
+      let val (built_in, ts) = is_built_in_const x ts in
+        (not built_in
+         ? add_pconst_to_table also_skolems (rich_pconst thy const x))
+        #> fold do_term ts
+      end
     and do_term t =
       case strip_comb t of
         (Const x, ts) => do_const true x ts
@@ -503,7 +505,7 @@
         case t of
           t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
         | Const (x as (s, _)) =>
-          (if is_built_in_const x args then
+          (if is_built_in_const x args |> fst then
              SOME tab
            else case Symtab.lookup tab s of
              NONE => SOME (Symtab.update (s, length args) tab)
diff -r 66edbd0f7a2e -r 0ea5b9c7d233 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Dec 21 03:56:51 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Dec 21 04:33:17 2010 +0100
@@ -75,7 +75,7 @@
   val is_prover_installed : Proof.context -> string -> bool
   val default_max_relevant_for_prover : Proof.context -> string -> int
   val is_built_in_const_for_prover :
-    Proof.context -> string -> string * typ -> term list -> bool
+    Proof.context -> string -> string * typ -> term list -> bool * term list
   val atp_relevance_fudge : relevance_fudge
   val smt_relevance_fudge : relevance_fudge
   val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
@@ -165,9 +165,17 @@
 
 fun is_built_in_const_for_prover ctxt name =
   if is_smt_prover ctxt name then
-    ctxt |> select_smt_solver name |> SMT_Builtin.is_builtin_ext
+    let val ctxt = ctxt |> select_smt_solver name in
+      fn x => fn ts =>
+         if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then
+           (true, [])
+         else if SMT_Builtin.is_builtin_fun_ext ctxt x ts then
+           (true, ts)
+         else
+           (false, ts)
+    end
   else
-    K o member (op =) atp_irrelevant_consts o fst
+    fn (s, _) => fn ts => (member (op =) atp_irrelevant_consts s, ts)
 
 (* FUDGE *)
 val atp_relevance_fudge =