merged
authorwenzelm
Fri, 27 Apr 2012 23:17:58 +0200
changeset 47817 5d2d63f4363e
parent 47812 bb477988edb4 (diff)
parent 47816 cd0dfb06b0c8 (current diff)
child 47818 151d137f1095
merged
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Apr 27 22:58:29 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Apr 27 23:17:58 2012 +0200
@@ -3,6 +3,7 @@
 *)
 
 header {* ATP Problem Importer *}
+
 theory ATP_Problem_Import
 imports Complex_Main TPTP_Interpret
 uses "sledgehammer_tactics.ML"
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 22:58:29 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 23:17:58 2012 +0200
@@ -69,7 +69,6 @@
     val params =
       [("card", "1\<emdash>100"),
        ("box", "false"),
-       ("sat_solver", "smart"),
        ("max_threads", "1"),
        ("batch_size", "5"),
        ("falsify", if null conjs then "false" else "true"),
@@ -134,13 +133,47 @@
     | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st')
   end
 
+fun nitpick_finite_oracle_tac ctxt timeout i th =
+  let
+    fun is_safe (Type (@{type_name fun}, Ts)) = forall is_safe Ts
+      | is_safe @{typ prop} = true
+      | is_safe @{typ bool} = true
+      | is_safe _ = false
+    val conj = Thm.term_of (Thm.cprem_of th i)
+  in
+    if exists_type (not o is_safe) conj then
+      Seq.empty
+    else
+      let
+        val thy = Proof_Context.theory_of ctxt
+        val state = Proof.init ctxt
+        val params =
+          [("box", "false"),
+           ("max_threads", "1"),
+           ("verbose", "true"),
+           ("debug", if debug then "true" else "false"),
+           ("overlord", if overlord then "true" else "false"),
+           ("max_potential", "0"),
+           ("timeout", string_of_int timeout)]
+          |> Nitpick_Isar.default_params thy
+        val i = 1
+        val n = 1
+        val step = 0
+        val subst = []
+        val (outcome, _) =
+          Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst
+                                    [] [] conj
+      in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end
+  end
+
 fun atp_tac ctxt override_params timeout prover =
   Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
       ([("debug", if debug then "true" else "false"),
         ("overlord", if overlord then "true" else "false"),
         ("provers", prover),
         ("timeout", string_of_int timeout)] @ override_params)
-      {add = [], del = [], only = true}
+      {add = [(Facts.named (Thm.derivation_name ext), [])],
+       del = [], only = true}
 
 fun sledgehammer_tac ctxt timeout i =
   let
@@ -156,17 +189,20 @@
   end
 
 fun auto_etc_tac ctxt timeout i =
-  SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac (simpset_of ctxt) i)
+  SOLVE_TIMEOUT (timeout div 20) "nitpick"
+      (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
+      (asm_full_simp_tac (simpset_of ctxt) i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
       (auto_tac ctxt
        THEN ALLGOALS (atp_tac ctxt [] (timeout div 5) ATP_Systems.spassN))
   ORELSE SOLVE_TIMEOUT (timeout div 5) "smt" (SMT_Solver.smt_tac ctxt [] i)
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "best" (best_tac ctxt i)
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "fast" (fast_tac ctxt i)
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
   ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 10) "arith" (Arith_Data.arith_tac ctxt i)
-  ORELSE SOLVE_TIMEOUT timeout "fastforce" (fast_force_tac ctxt i)
+  ORELSE SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i)
+  ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
 
 fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
 
@@ -207,8 +243,8 @@
       read_tptp_file thy (freeze_problem_consts thy) file_name
     val conj = make_conj assms conjs
   in
-    (can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
-     can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
+    (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
+     can_tac ctxt (sledgehammer_tac ctxt (timeout div 2) 1) conj orelse
      can_tac ctxt (atp_tac ctxt [] timeout ATP_Systems.satallaxN 1) conj)
     |> print_szs_from_success conjs
   end
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Apr 27 22:58:29 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Apr 27 23:17:58 2012 +0200
@@ -1681,7 +1681,7 @@
   level_of_type_enc type_enc <> No_Types andalso
   not (null (Term.hidden_polymorphism t))
 
-fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
+fun add_helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
   case unprefix_and_unascii const_prefix s of
     SOME mangled_s =>
     let
@@ -1705,20 +1705,20 @@
       val make_facts = map_filter (make_fact ctxt format type_enc false)
       val fairly_sound = is_type_enc_fairly_sound type_enc
     in
-      helper_table
-      |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
-                  if helper_s <> unmangled_s orelse
-                     (needs_fairly_sound andalso not fairly_sound) then
-                    []
-                  else
-                    ths ~~ (1 upto length ths)
-                    |> maps (dub_and_inst needs_fairly_sound)
-                    |> make_facts)
+      fold (fn ((helper_s, needs_fairly_sound), ths) =>
+               if helper_s <> unmangled_s orelse
+                  (needs_fairly_sound andalso not fairly_sound) then
+                 I
+               else
+                 ths ~~ (1 upto length ths)
+                 |> maps (dub_and_inst needs_fairly_sound)
+                 |> make_facts
+                 |> union (op = o pairself #iformula))
+           helper_table
     end
-  | NONE => []
+  | NONE => I
 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
-  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
-                  []
+  Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc) sym_tab []
 
 (***************************************************************)
 (* Type Classes Present in the Axiom or Conjecture Clauses     *)