src/HOL/Tools/res_atp.ML
changeset 24425 ca97c6f3d9cd
parent 24320 ea5be4be3bae
child 24546 c90cee3163b7
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Aug 24 14:15:58 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Aug 24 14:16:44 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature RES_ATP =
     1.6  sig
     1.7 -  val prover: string ref
     1.8 +  val prover: ResReconstruct.atp ref
     1.9    val destdir: string ref
    1.10    val helper_path: string -> string -> string
    1.11    val problem_name: string ref
    1.12 @@ -45,6 +45,8 @@
    1.13  structure ResAtp: RES_ATP =
    1.14  struct
    1.15  
    1.16 +structure Recon = ResReconstruct;
    1.17 +
    1.18  fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
    1.19  
    1.20  (********************************************************************)
    1.21 @@ -55,7 +57,7 @@
    1.22  (*** background linkup ***)
    1.23  val run_blacklist_filter = ref true;
    1.24  val time_limit = ref 60;
    1.25 -val prover = ref "";
    1.26 +val prover = ref Recon.E;
    1.27  
    1.28  (*** relevance filter parameters ***)
    1.29  val run_relevance_filter = ref true;
    1.30 @@ -70,15 +72,15 @@
    1.31        "e" =>
    1.32            (max_new := 100;
    1.33             theory_const := false;
    1.34 -           prover := "E")
    1.35 +           prover := Recon.E)
    1.36      | "spass" =>
    1.37            (max_new := 40;
    1.38             theory_const := true;
    1.39 -           prover := "spass")
    1.40 +           prover := Recon.SPASS)
    1.41      | "vampire" =>
    1.42            (max_new := 60;
    1.43             theory_const := false;
    1.44 -           prover := "vampire")
    1.45 +           prover := Recon.Vampire)
    1.46      | _ => error ("No such prover: " ^ atp);
    1.47  
    1.48  val _ = set_prover "E"; (* use E as the default prover *)
    1.49 @@ -822,30 +824,26 @@
    1.50            in
    1.51              Output.debug (fn () => "problem file in watcher_call_provers is " ^ probfile);
    1.52              (*options are separated by Watcher.setting_sep, currently #"%"*)
    1.53 -            if !prover = "spass"
    1.54 -            then
    1.55 -              let val spass = helper_path "SPASS_HOME" "SPASS"
    1.56 -                  val sopts =
    1.57 -   "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
    1.58 -              in
    1.59 -                  ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
    1.60 -              end
    1.61 -            else if !prover = "vampire"
    1.62 -            then
    1.63 -              let val vampire = helper_path "VAMPIRE_HOME" "vampire"
    1.64 -                  val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
    1.65 -              in
    1.66 -                  ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
    1.67 -              end
    1.68 -             else if !prover = "E"
    1.69 -             then
    1.70 -               let val Eprover = helper_path "E_HOME" "eproof"
    1.71 -               in
    1.72 -                  ("E", Eprover,
    1.73 -                     "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time, probfile) ::
    1.74 -                   make_atp_list xs (n+1)
    1.75 -               end
    1.76 -             else error ("Invalid prover name: " ^ !prover)
    1.77 +            case !prover of
    1.78 +                Recon.SPASS =>
    1.79 +		  let val spass = helper_path "SPASS_HOME" "SPASS"
    1.80 +		      val sopts =
    1.81 +       "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
    1.82 +		  in
    1.83 +		      ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
    1.84 +		  end
    1.85 +              | Recon.Vampire =>
    1.86 +		  let val vampire = helper_path "VAMPIRE_HOME" "vampire"
    1.87 +		      val vopts = "--mode casc%-t " ^ time  (*what about -m 100000?*)
    1.88 +		  in
    1.89 +		      ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
    1.90 +		  end
    1.91 +              | Recon.E =>
    1.92 +		  let val eproof = helper_path "E_HOME" "eproof"
    1.93 +                      val eopts = "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time
    1.94 +		  in
    1.95 +		     ("E", eproof, eopts, probfile) :: make_atp_list xs (n+1)
    1.96 +		  end
    1.97            end
    1.98  
    1.99      val atp_list = make_atp_list sg_terms 1
   1.100 @@ -885,7 +883,7 @@
   1.101        val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
   1.102        val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
   1.103                    axcls_list
   1.104 -      val writer = if !prover = "spass" then dfg_writer else tptp_writer
   1.105 +      val writer = if !prover = Recon.SPASS then dfg_writer else tptp_writer
   1.106        fun write_all [] [] _ = []
   1.107          | write_all (ccls::ccls_list) (axcls::axcls_list) k =
   1.108              let val fname = probfile k