src/HOL/Tools/res_atp.ML
changeset 18700 f04a8755d6ca
parent 18680 677e2bdd75f0
child 18753 aa82bd41555d
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jan 16 21:55:17 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Jan 17 10:26:36 2006 +0100
     1.3 @@ -97,20 +97,15 @@
     1.4              (*options are separated by Watcher.setting_sep, currently #"%"*)
     1.5              if !prover = "spass"
     1.6              then
     1.7 -              let val optionline = 
     1.8 +              let val baseopts = "%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
     1.9 +              val infopts = 
    1.10  		      if !AtpCommunication.reconstruct 
    1.11 -		          (*Proof reconstruction works for only a limited set of 
    1.12 -		            inference rules*)
    1.13 -                      then space_implode "%" (!custom_spass) ^
    1.14 -                           "%-DocProof%-TimeLimit=" ^ time
    1.15 -                      else "-DocProof%-SOS%-FullRed=0%-TimeLimit=" ^ time (*Auto mode*)
    1.16 -                  val _ = Output.debug ("SPASS option string is " ^ optionline)
    1.17 -                  val _ = helper_path "SPASS_HOME" "SPASS"
    1.18 -                    (*We've checked that SPASS is there for ATP/spassshell to run.*)
    1.19 -              in 
    1.20 -                  ([("spass", 
    1.21 -                     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
    1.22 -                     optionline, probfile)] @ 
    1.23 +		          (*Proof reconstruction needs a limited set of inf rules*)
    1.24 +                      then space_implode "%" (!custom_spass)                           
    1.25 +                      else "-Auto%-SOS=1"
    1.26 +                  val spass = helper_path "SPASS_HOME" "SPASS"
    1.27 +            in 
    1.28 +                ([("spass", spass, infopts ^ baseopts, probfile)] @ 
    1.29                    (make_atp_list xs (n+1)))
    1.30                end
    1.31              else if !prover = "vampire"