src/HOL/Tools/res_atp.ML
changeset 17317 3f12de2e2e6e
parent 17306 5cde710a8a23
child 17404 d16c3a62c396
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Sep 09 12:18:15 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Sep 09 17:47:37 2005 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5  val prover = ref "spass";   (* use spass as default prover *)
     1.6  val custom_spass =   (*specialized options for SPASS*)
     1.7 -      ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
     1.8 +      ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
     1.9             "-DocProof","-TimeLimit=60"];
    1.10  
    1.11  val axiom_file = File.tmp_path (Path.basic "axioms");
    1.12 @@ -147,6 +147,8 @@
    1.13              val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
    1.14              val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
    1.15            in
    1.16 +            (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    1.17 +              versions of Unix.execute treat them differently!*)
    1.18              if !prover = "spass"
    1.19              then
    1.20                let val optionline = 
    1.21 @@ -154,7 +156,7 @@
    1.22  		          (*Proof reconstruction works for only a limited set of 
    1.23  		            inference rules*)
    1.24                        then "-" ^ space_implode "%-" (!custom_spass)
    1.25 -                      else "-DocProof%-TimeLimit=60%-SOS" (*Auto mode*)
    1.26 +                      else "-DocProof%-TimeLimit=60%-SOS%-FullRed=0" (*Auto mode*)
    1.27                    val _ = debug ("SPASS option string is " ^ optionline)
    1.28                    val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    1.29                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
    1.30 @@ -168,7 +170,7 @@
    1.31  	    then 
    1.32                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    1.33                in
    1.34 -                ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
    1.35 +                ([("vampire", thmstr, goalstring, vampire, "-t60%-m100000",
    1.36                     axfile, hypsfile, probfile)] @
    1.37                   (make_atp_list xs sign (n+1)))
    1.38                end