# HG changeset patch
# User blanchet
# Date 1335533077 -7200
# Node ID 4ad62c5f9f88b963219d324eca0fdfcf4ae79728
# Parent  02bdd591eb8f94134a09d0454628c787e2877352
thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)

diff -r 02bdd591eb8f -r 4ad62c5f9f88 src/HOL/TPTP/ATP_Problem_Import.thy
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Apr 27 15:24:37 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Fri Apr 27 15:24:37 2012 +0200
@@ -6,7 +6,7 @@
 theory ATP_Problem_Import
 imports Complex_Main TPTP_Interpret
 uses "sledgehammer_tactics.ML"
-     "atp_problem_import.ML"
+     ("atp_problem_import.ML")
 begin
 
 ML {* Proofterm.proofs := 0 *}
@@ -14,8 +14,14 @@
 declare [[show_consts]] (* for Refute *)
 declare [[smt_oracle]]
 
+declare [[unify_search_bound = 60]]
+declare [[unify_trace_bound = 60]]
+
+use "atp_problem_import.ML"
+
 (*
-ML {* ATP_Problem_Import.isabelle_tptp_file 300 "$TPTP/Problems/PUZ/PUZ107^5.p" *}
+ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} 50
+          "$TPTP/Problems/PUZ/PUZ107^5.p" *}
 *)
 
 end
diff -r 02bdd591eb8f -r 4ad62c5f9f88 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 15:24:37 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Apr 27 15:24:37 2012 +0200
@@ -7,10 +7,10 @@
 
 signature ATP_PROBLEM_IMPORT =
 sig
-  val nitpick_tptp_file : int -> string -> unit
-  val refute_tptp_file : int -> string -> unit
-  val sledgehammer_tptp_file : int -> string -> unit
-  val isabelle_tptp_file : int -> string -> unit
+  val nitpick_tptp_file : theory -> int -> string -> unit
+  val refute_tptp_file : theory -> int -> string -> unit
+  val sledgehammer_tptp_file : theory -> int -> string -> unit
+  val isabelle_tptp_file : theory -> int -> string -> unit
   val translate_tptp_file : string -> string -> string -> unit
 end;
 
@@ -59,9 +59,9 @@
 fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1
   | aptrueprop f t = f t
 
-fun nitpick_tptp_file timeout file_name =
+fun nitpick_tptp_file thy timeout file_name =
   let
-    val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} I file_name
+    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
     val thy = Proof_Context.theory_of ctxt
     val defs = defs |> map (ATP_Util.extensionalize_term ctxt
                             #> aptrueprop (open_form I))
@@ -95,7 +95,7 @@
 
 (** Refute **)
 
-fun refute_tptp_file timeout file_name =
+fun refute_tptp_file thy timeout file_name =
   let
     fun print_szs_from_outcome falsify s =
       "% SZS status " ^
@@ -104,7 +104,7 @@
        else
          "Unknown")
       |> Output.urgent_message
-    val (conjs, (defs, nondefs), ctxt) = read_tptp_file @{theory} I file_name
+    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
     val params =
       [("maxtime", string_of_int timeout),
        ("maxvars", "100000")]
@@ -117,9 +117,6 @@
 
 (** Sledgehammer and Isabelle (combination of provers) **)
 
-val cvc3N = "cvc3"
-val z3N = "z3"
-
 fun can_tac ctxt tactic conj = can (Goal.prove ctxt [] [] conj) (K tactic)
 
 fun SOLVE_TIMEOUT seconds name tac st =
@@ -149,40 +146,39 @@
   let
     fun slice overload_params fraq prover =
       SOLVE_TIMEOUT (timeout div fraq) prover
-                    (atp_tac ctxt overload_params timeout prover i)
+                    (atp_tac ctxt overload_params (timeout div fraq) prover i)
   in
-    slice [] 7 ATP_Systems.satallaxN
-    ORELSE slice [] 7 ATP_Systems.leo2N
-    ORELSE slice [] 7 ATP_Systems.spassN
-    ORELSE slice [] 7 z3N
-    ORELSE slice [] 7 ATP_Systems.vampireN
-    ORELSE slice [] 7 ATP_Systems.eN
-    ORELSE slice [] 7 cvc3N
+    slice [] 5 ATP_Systems.satallaxN
+    ORELSE slice [] 5 ATP_Systems.leo2N
+    ORELSE slice [] 5 ATP_Systems.spassN
+    ORELSE slice [] 5 ATP_Systems.vampireN
+    ORELSE slice [] 5 ATP_Systems.eN
   end
 
 fun auto_etc_tac ctxt timeout i =
   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 20) "auto+spass"
+  ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
       (auto_tac ctxt
-       THEN ALLGOALS (atp_tac ctxt [] (timeout div 20) ATP_Systems.spassN))
-  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 20) "force" (force_tac ctxt i)
-  ORELSE SOLVE_TIMEOUT (timeout div 20) "arith" (Arith_Data.arith_tac ctxt i)
+       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 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)
 
-val problem_const_prefix = Context.theory_name @{theory} ^ Long_Name.separator
+fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
 
 (* Isabelle's standard automatic tactics ("auto", etc.) are more eager to
    unfold "definitions" of free variables than of constants (cf. PUZ107^5). *)
-val freeze_problem_consts =
-  map_aterms (fn t as Const (s, T) =>
-                 if String.isPrefix problem_const_prefix s then
-                   Free (Long_Name.base_name s, T)
-                 else
-                   t
-               | t => t)
+fun freeze_problem_consts thy =
+  let val is_problem_const = String.isPrefix (problem_const_prefix thy) in
+    map_aterms (fn t as Const (s, T) =>
+                   if is_problem_const s then Free (Long_Name.base_name s, T)
+                   else t
+                 | t => t)
+  end
 
 fun make_conj (defs, nondefs) conjs =
   Logic.list_implies (rev defs @ rev nondefs,
@@ -193,22 +189,22 @@
                          (if success then
                             if null conjs then "Unsatisfiable" else "Theorem"
                           else
-                            "% SZS status Unknown"))
+                            "Unknown"))
 
-fun sledgehammer_tptp_file timeout file_name =
+fun sledgehammer_tptp_file thy timeout file_name =
   let
     val (conjs, assms, ctxt) =
-      read_tptp_file @{theory} freeze_problem_consts file_name
+      read_tptp_file thy (freeze_problem_consts thy) file_name
     val conj = make_conj assms conjs
   in
     can_tac ctxt (sledgehammer_tac ctxt timeout 1) conj
     |> print_szs_from_success conjs
   end
 
-fun isabelle_tptp_file timeout file_name =
+fun isabelle_tptp_file thy timeout file_name =
   let
     val (conjs, assms, ctxt) =
-      read_tptp_file @{theory} freeze_problem_consts file_name
+      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
diff -r 02bdd591eb8f -r 4ad62c5f9f88 src/HOL/TPTP/lib/Tools/tptp_isabelle
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle	Fri Apr 27 15:24:37 2012 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle	Fri Apr 27 15:24:37 2012 +0200
@@ -27,7 +27,7 @@
 for FILE in "$@"
 do
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.isabelle_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
     > /tmp/$SCRATCH.thy
   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
 done
diff -r 02bdd591eb8f -r 4ad62c5f9f88 src/HOL/TPTP/lib/Tools/tptp_nitpick
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick	Fri Apr 27 15:24:37 2012 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick	Fri Apr 27 15:24:37 2012 +0200
@@ -27,7 +27,7 @@
 for FILE in "$@"
 do
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.nitpick_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
     > /tmp/$SCRATCH.thy
   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
 done
diff -r 02bdd591eb8f -r 4ad62c5f9f88 src/HOL/TPTP/lib/Tools/tptp_refute
--- a/src/HOL/TPTP/lib/Tools/tptp_refute	Fri Apr 27 15:24:37 2012 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute	Fri Apr 27 15:24:37 2012 +0200
@@ -26,7 +26,7 @@
 for FILE in "$@"
 do
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.refute_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
     > /tmp/$SCRATCH.thy
   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
 done
diff -r 02bdd591eb8f -r 4ad62c5f9f88 src/HOL/TPTP/lib/Tools/tptp_sledgehammer
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Fri Apr 27 15:24:37 2012 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Fri Apr 27 15:24:37 2012 +0200
@@ -27,7 +27,7 @@
 for FILE in "$@"
 do
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.sledgehammer_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
     > /tmp/$SCRATCH.thy
   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
 done
diff -r 02bdd591eb8f -r 4ad62c5f9f88 src/HOL/TPTP/sledgehammer_tactics.ML
--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Apr 27 15:24:37 2012 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Apr 27 15:24:37 2012 +0200
@@ -24,12 +24,12 @@
 
 fun run_prover override_params relevance_override i n ctxt goal =
   let
+    val mode = Sledgehammer_Provers.Normal
     val chained_ths = [] (* a tactic has no chained ths *)
     val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
       Sledgehammer_Isar.default_params ctxt override_params
     val name = hd provers
-    val prover =
-      Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
+    val prover = Sledgehammer_Provers.get_prover ctxt mode name
     val default_max_relevant =
       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
     val is_built_in_const =