More blacklisting
authorpaulson
Wed Nov 01 15:39:20 2006 +0100 (2006-11-01)
changeset 2113288d1daae0319
parent 21131 a447addc14af
child 21133 de048d4968d9
More blacklisting
CASC mode now always on, due to switch to Vampire 8.1 (i.e. the 2006 version)
Now runs ATPs unless time_limit = 0.
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Nov 01 08:46:54 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Nov 01 15:39:20 2006 +0100
     1.3 @@ -302,6 +302,7 @@
     1.4    an attribute.*)
     1.5  val blacklist = ref
     1.6    ["Datatype.prod.size",
     1.7 +   "Datatype.unit.exhaust", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
     1.8     "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
     1.9     "Datatype.unit.inducts",
    1.10     "Datatype.unit.split_asm", 
    1.11 @@ -732,8 +733,7 @@
    1.12              else if !prover = "vampire"
    1.13  	    then 
    1.14                let val vampire = helper_path "VAMPIRE_HOME" "vampire"
    1.15 -                  val casc = if !time_limit > 70 then "--mode casc%" else ""
    1.16 -                  val vopts = casc ^ "-m 100000%-t " ^ time
    1.17 +                  val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
    1.18                in
    1.19                    ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
    1.20                end
    1.21 @@ -874,8 +874,8 @@
    1.22      Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
    1.23      ResClause.init thy;
    1.24      ResHolClause.init thy;
    1.25 -    if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
    1.26 -    else isar_atp_writeonly (ctxt, goal)
    1.27 +    if !time_limit > 0 then isar_atp (ctxt, goal)
    1.28 +    else (warning "Writing problem file only"; isar_atp_writeonly (ctxt, goal))
    1.29    end;
    1.30  
    1.31  val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep