src/HOL/Tools/res_atp.ML
changeset 17690 8ba7c3cd24a8
parent 17525 ae5bb6001afb
child 17717 7c6a96cbc966
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Sep 28 11:15:33 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Sep 28 11:16:27 2005 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    val destdir: string ref
     1.5    val hook_count: int ref
     1.6    val problem_name: string ref
     1.7 +  val time_limit: int ref
     1.8  end;
     1.9  
    1.10  structure ResAtp: RES_ATP =
    1.11 @@ -19,11 +20,11 @@
    1.12  
    1.13  val call_atp = ref false;
    1.14  val hook_count = ref 0;
    1.15 +val time_limit = ref 60;
    1.16  
    1.17  val prover = ref "E";   (* use E as the default prover *)
    1.18  val custom_spass =   (*specialized options for SPASS*)
    1.19 -      ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
    1.20 -           "-DocProof","-TimeLimit=60"];
    1.21 +      ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    1.22  
    1.23  val destdir = ref "";   (*Empty means write files to /tmp*)
    1.24  val problem_name = ref "prob";
    1.25 @@ -104,6 +105,7 @@
    1.26              val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
    1.27  
    1.28              val probfile = prob_pathname() ^ "_" ^ Int.toString n
    1.29 +            val time = Int.toString (!time_limit)
    1.30              val _ = debug ("problem file in watcher_call_provers is " ^ probfile)
    1.31            in
    1.32              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    1.33 @@ -114,8 +116,9 @@
    1.34  		      if !AtpCommunication.reconstruct 
    1.35  		          (*Proof reconstruction works for only a limited set of 
    1.36  		            inference rules*)
    1.37 -                      then "-" ^ space_implode "%-" (!custom_spass)
    1.38 -                      else "-DocProof%-TimeLimit=60%-SOS%-FullRed=0" (*Auto mode*)
    1.39 +                      then space_implode "%" (!custom_spass) ^
    1.40 +                           "%-DocProof%-TimeLimit=" ^ time
    1.41 +                      else "-DocProof%-SOS%-FullRed=0%-TimeLimit=" ^ time (*Auto mode*)
    1.42                    val _ = debug ("SPASS option string is " ^ optionline)
    1.43                    val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    1.44                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
    1.45 @@ -129,7 +132,7 @@
    1.46  	    then 
    1.47                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
    1.48                in
    1.49 -                ([("vampire", goalstring, vampire, "-t 60%-m 100000", probfile)] @
    1.50 +                ([("vampire", goalstring, vampire, "-m 100000%-t " ^ time, probfile)] @
    1.51                   (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
    1.52                end
    1.53        	     else if !prover = "E"
    1.54 @@ -137,7 +140,7 @@
    1.55  	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
    1.56  	       in
    1.57  		  ([("E", goalstring, Eprover, 
    1.58 -		     "--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
    1.59 +		     "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
    1.60  		     probfile)] @
    1.61  		   (make_atp_list xs (n+1)))
    1.62  	       end
    1.63 @@ -237,7 +240,7 @@
    1.64      hook_count := !hook_count +1;
    1.65      debug ("in hook for time: " ^(Int.toString (!hook_count)) );
    1.66      ResClause.init thy;
    1.67 -    if !destdir = "" then isar_atp (ctxt, goal)
    1.68 +    if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
    1.69      else isar_atp_writeonly (ctxt, goal)
    1.70    end);
    1.71