merged
authorwenzelm
Tue, 14 Feb 2012 22:48:07 +0100
changeset 46482 f310e9eabf60
parent 46481 c7c85ff6de2a (diff)
parent 46476 dac966e4e51d (current diff)
child 46483 10a9c31a22b4
merged
--- a/src/HOL/Mutabelle/mutabelle.ML	Tue Feb 14 22:27:33 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Tue Feb 14 22:48:07 2012 +0100
@@ -43,14 +43,6 @@
  end;
 
 
-(*possibility to print a given term for debugging purposes*)
-
-fun prt x = Pretty.writeln (Syntax.pretty_term_global @{theory Main} x);
-
-val debug = (Unsynchronized.ref false);
-fun debug_msg mutterm = if (!debug) then (prt mutterm) else ();
-
-
 (*thrown in case the specified path doesn't exist in the specified term*)
 
 exception WrongPath of string;
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Feb 14 22:27:33 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Feb 14 22:48:07 2012 +0100
@@ -270,7 +270,8 @@
    proof_delims = tstp_proof_delims,
    known_failures =
      known_szs_status_failures @
-     [(TimedOut, "CPU time limit exceeded, terminating")],
+     [(TimedOut, "CPU time limit exceeded, terminating"),
+      (GaveUp, "No.of.Axioms")],
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
@@ -493,10 +494,15 @@
 fun the_system name versions =
   case get_system name versions of
     (SOME sys, _) => sys
-  | (NONE, []) => error ("SystemOnTPTP is currently not available.")
+  | (NONE, []) => error ("SystemOnTPTP is not available.")
   | (NONE, syss) =>
-    error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
-           "(Available systems: " ^ commas_quote syss ^ ".)")
+    case syss |> filter_out (String.isPrefix "%")
+              |> filter_out (curry (op =) "") of
+      [] => error ("SystemOnTPTP is not available.")
+    | [msg] => error ("SystemOnTPTP is not available: " ^ msg ^ ".")
+    | syss =>
+      error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
+             "(Available systems: " ^ commas_quote syss ^ ".)")
 
 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
 
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Feb 14 22:27:33 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Feb 14 22:48:07 2012 +0100
@@ -77,6 +77,7 @@
 fun test_term (name, (_, compile)) ctxt catch_code_errors (t, eval_terms) =
   let
     val genuine_only = Config.get ctxt Quickcheck.genuine_only
+    val abort_potential = Config.get ctxt Quickcheck.abort_potential
     val _ = check_test_term t
     val names = Term.add_free_names t []
     val current_size = Unsynchronized.ref 0
@@ -104,15 +105,17 @@
             NONE => with_size test_fun genuine_only (k + 1)
           | SOME (true, ts) => SOME (true, ts)
           | SOME (false, ts) =>
-            let
-              val (ts1, ts2) = chop (length names) ts
-              val (eval_terms', _) = chop (length ts2) eval_terms
-              val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
-            in
-              (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
-              Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
-              with_size test_fun true k)
-            end
+            if abort_potential then SOME (false, ts)
+            else
+              let
+                val (ts1, ts2) = chop (length names) ts
+                val (eval_terms', _) = chop (length ts2) eval_terms
+                val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
+              in
+                (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+                Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
+                with_size test_fun true k)
+              end
         end;
   in
     case test_fun of
@@ -169,6 +172,7 @@
 fun test_term_with_cardinality (name, (size_matters_for, compile)) ctxt catch_code_errors ts =
   let
     val genuine_only = Config.get ctxt Quickcheck.genuine_only
+    val abort_potential = Config.get ctxt Quickcheck.abort_potential
     val thy = Proof_Context.theory_of ctxt
     val (ts', eval_terms) = split_list ts
     val _ = map check_test_term ts'
@@ -209,14 +213,17 @@
           SOME ((card, _), (true, ts)) =>
             Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result
         | SOME ((card, size), (false, ts)) =>
-           let
-              val (ts1, ts2) = chop (length names) ts
-              val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
-              val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
-            in
-              (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
-              Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
-              test true (snd (take_prefix (fn x => not (x = (card, size))) enum)))
+            if abort_potential then
+              Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (false, ts)) current_result
+            else
+              let
+                val (ts1, ts2) = chop (length names) ts
+                val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
+                val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
+              in
+                (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+                Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
+                test true (snd (take_prefix (fn x => not (x = (card, size))) enum)))              
             end
         | NONE => ()
       in (test genuine_only enumeration_card_size; !current_result) end
--- a/src/Tools/quickcheck.ML	Tue Feb 14 22:27:33 2012 +0100
+++ b/src/Tools/quickcheck.ML	Tue Feb 14 22:48:07 2012 +0100
@@ -21,6 +21,7 @@
   val report : bool Config.T
   val timing : bool Config.T
   val genuine_only : bool Config.T
+  val abort_potential : bool Config.T  
   val quiet : bool Config.T
   val verbose : bool Config.T
   val timeout : real Config.T
@@ -177,6 +178,7 @@
 val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
 val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
 val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
+val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false)
 val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
 val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
 val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
@@ -433,6 +435,7 @@
   | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
   | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
   | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg))
+  | parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg))
   | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
   | parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
   | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))