# HG changeset patch
# User blanchet
# Date 1309969174 -3600
# Node ID 92f78a4a5628ad1f6fc10400c3564016c014fa67
# Parent  b8d79bd6029e97adac21220a280e89ffaa2ce3dc
better setup for experimental "z3_atp"

diff -r b8d79bd6029e -r 92f78a4a5628 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 06 17:58:03 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 06 17:19:34 2011 +0100
@@ -326,7 +326,10 @@
    formats = [FOF],
    best_slices =
      (* FUDGE (FIXME) *)
-     K [(1.0, (false, (250, "mangled_preds?", "")))]}
+     K [(0.5, (false, (250, "mangled_preds?", ""))),
+        (0.25, (false, (125, "mangled_preds?", ""))),
+        (0.125, (false, (62, "mangled_preds?", ""))),
+        (0.125, (false, (31, "mangled_preds?", "")))]}
 
 val z3_atp = (z3_atpN, z3_atp_config)
 
diff -r b8d79bd6029e -r 92f78a4a5628 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 06 17:58:03 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 06 17:19:34 2011 +0100
@@ -529,7 +529,7 @@
 
 (* Give the ATPs some slack before interrupting them the hard way. "z3_atp" on
    Linux appears to be the only ATP that does not honor its time limit. *)
-val atp_timeout_slack = seconds 5.0
+val atp_timeout_slack = seconds 1.0
 
 fun run_atp mode name
         ({exec, required_execs, arguments, proof_delims, known_failures,