fixed the "expect" mechanism of Refute in the face of timeouts
authorblanchet
Wed Oct 21 16:54:04 2009 +0200 (2009-10-21)
changeset 33054dd1192a96968
parent 33053 dabf9d1bb552
child 33055 5a733f325939
fixed the "expect" mechanism of Refute in the face of timeouts
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Oct 21 16:53:00 2009 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed Oct 21 16:54:04 2009 +0200
     1.3 @@ -1145,6 +1145,10 @@
     1.4    fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver,
     1.5      expect} t negate =
     1.6    let
     1.7 +    (* string -> unit *)
     1.8 +    fun check_expect outcome_code =
     1.9 +      if expect = "" orelse outcome_code = expect then ()
    1.10 +      else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    1.11      (* unit -> unit *)
    1.12      fun wrapper () =
    1.13      let
    1.14 @@ -1237,8 +1241,7 @@
    1.15            "unknown")
    1.16          val outcome_code = find_model_loop (first_universe types sizes minsize)
    1.17        in
    1.18 -        if expect = "" orelse outcome_code = expect then ()
    1.19 -        else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
    1.20 +        check_expect outcome_code
    1.21        end
    1.22      in
    1.23        (* some parameter sanity checks *)
    1.24 @@ -1261,9 +1264,10 @@
    1.25          TimeLimit.timeLimit (Time.fromSeconds maxtime)
    1.26            wrapper ()
    1.27          handle TimeLimit.TimeOut =>
    1.28 -          priority ("Search terminated, time limit (" ^
    1.29 -            string_of_int maxtime
    1.30 -            ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.")
    1.31 +          (priority ("Search terminated, time limit (" ^
    1.32 +              string_of_int maxtime
    1.33 +              ^ (if maxtime=1 then " second" else " seconds") ^ ") exceeded.");
    1.34 +           check_expect "unknown")
    1.35        ) else
    1.36          wrapper ()
    1.37      end;