src/HOL/Tools/ATP_Manager/atp_systems.ML
changeset 36382 b90fc0d75bca
parent 36377 b3dce4c715d0
child 36393 be73a2b2443b
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Apr 23 19:26:39 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Apr 23 19:36:49 2010 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4     arguments: Time.time -> string,
     1.5     proof_delims: (string * string) list,
     1.6     known_failures: (failure * string) list,
     1.7 -   max_new_clauses: int,
     1.8 +   max_axiom_clauses: int,
     1.9     prefers_theory_relevant: bool};
    1.10  
    1.11  
    1.12 @@ -175,7 +175,8 @@
    1.13        if File.exists command then
    1.14          write_file full_types explicit_apply probfile clauses
    1.15          |> pair (apfst split_time' (bash_output (command_line probfile)))
    1.16 -      else error ("Bad executable: " ^ Path.implode command ^ ".");
    1.17 +      else
    1.18 +        error ("Bad executable: " ^ Path.implode command ^ ".");
    1.19  
    1.20      (* If the problem file has not been exported, remove it; otherwise, export
    1.21         the proof file too. *)
    1.22 @@ -217,14 +218,14 @@
    1.23  
    1.24  fun generic_tptp_prover
    1.25          (name, {home, executable, arguments, proof_delims, known_failures,
    1.26 -                max_new_clauses, prefers_theory_relevant})
    1.27 +                max_axiom_clauses, prefers_theory_relevant})
    1.28          (params as {debug, overlord, respect_no_atp, relevance_threshold,
    1.29                      convergence, theory_relevant, higher_order, follow_defs,
    1.30                      isar_proof, ...})
    1.31          minimize_command timeout =
    1.32    generic_prover overlord
    1.33        (get_relevant_facts respect_no_atp relevance_threshold convergence
    1.34 -                          higher_order follow_defs max_new_clauses
    1.35 +                          higher_order follow_defs max_axiom_clauses
    1.36                            (the_default prefers_theory_relevant theory_relevant))
    1.37        (prepare_clauses higher_order false)
    1.38        (write_tptp_file (debug andalso overlord andalso not isar_proof)) home
    1.39 @@ -236,7 +237,7 @@
    1.40  
    1.41  (** common provers **)
    1.42  
    1.43 -fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000
    1.44 +fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
    1.45  
    1.46  (* Vampire *)
    1.47  
    1.48 @@ -245,15 +246,16 @@
    1.49  val vampire_config : prover_config =
    1.50    {home = getenv "VAMPIRE_HOME",
    1.51     executable = "vampire",
    1.52 -   arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
    1.53 -                              string_of_int (generous_to_secs timeout)),
    1.54 +   arguments = fn timeout =>
    1.55 +     "--output_syntax tptp --mode casc -t " ^
    1.56 +     string_of_int (to_generous_secs timeout),
    1.57     proof_delims = [("=========== Refutation ==========",
    1.58                      "======= End of refutation =======")],
    1.59     known_failures =
    1.60       [(Unprovable, "Satisfiability detected"),
    1.61        (OutOfResources, "CANNOT PROVE"),
    1.62        (OutOfResources, "Refutation not found")],
    1.63 -   max_new_clauses = 60,
    1.64 +   max_axiom_clauses = 60,
    1.65     prefers_theory_relevant = false}
    1.66  val vampire = tptp_prover "vampire" vampire_config
    1.67  
    1.68 @@ -266,9 +268,9 @@
    1.69  val e_config : prover_config =
    1.70    {home = getenv "E_HOME",
    1.71     executable = "eproof",
    1.72 -   arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
    1.73 -                              \-tAutoDev --silent --cpu-limit=" ^
    1.74 -                              string_of_int (generous_to_secs timeout)),
    1.75 +   arguments = fn timeout =>
    1.76 +     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
    1.77 +     string_of_int (to_generous_secs timeout),
    1.78     proof_delims = [tstp_proof_delims],
    1.79     known_failures =
    1.80       [(Unprovable, "SZS status: Satisfiable"),
    1.81 @@ -279,7 +281,7 @@
    1.82         "# Cannot determine problem status within resource limit"),
    1.83        (OutOfResources, "SZS status: ResourceOut"),
    1.84        (OutOfResources, "SZS status ResourceOut")],
    1.85 -   max_new_clauses = 100,
    1.86 +   max_axiom_clauses = 100,
    1.87     prefers_theory_relevant = false}
    1.88  val e = tptp_prover "e" e_config
    1.89  
    1.90 @@ -288,13 +290,13 @@
    1.91  
    1.92  fun generic_dfg_prover
    1.93          (name, {home, executable, arguments, proof_delims, known_failures,
    1.94 -                max_new_clauses, prefers_theory_relevant})
    1.95 +                max_axiom_clauses, prefers_theory_relevant})
    1.96          (params as {overlord, respect_no_atp, relevance_threshold, convergence,
    1.97                      theory_relevant, higher_order, follow_defs, ...})
    1.98          minimize_command timeout =
    1.99    generic_prover overlord
   1.100        (get_relevant_facts respect_no_atp relevance_threshold convergence
   1.101 -                          higher_order follow_defs max_new_clauses
   1.102 +                          higher_order follow_defs max_axiom_clauses
   1.103                            (the_default prefers_theory_relevant theory_relevant))
   1.104        (prepare_clauses higher_order true) write_dfg_file home executable
   1.105        (arguments timeout) proof_delims known_failures name params
   1.106 @@ -307,15 +309,15 @@
   1.107  val spass_config : prover_config =
   1.108    {home = getenv "SPASS_HOME",
   1.109     executable = "SPASS",
   1.110 -   arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
   1.111 -     " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^
   1.112 -     string_of_int (generous_to_secs timeout)),
   1.113 +   arguments = fn timeout =>
   1.114 +     "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   1.115 +     \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout),
   1.116     proof_delims = [("Here is a proof", "Formulae used in the proof")],
   1.117     known_failures =
   1.118       [(Unprovable, "SPASS beiseite: Completion found"),
   1.119        (TimedOut, "SPASS beiseite: Ran out of time"),
   1.120        (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded")],
   1.121 -   max_new_clauses = 40,
   1.122 +   max_axiom_clauses = 40,
   1.123     prefers_theory_relevant = true}
   1.124  val spass = dfg_prover "spass" spass_config
   1.125  
   1.126 @@ -336,7 +338,7 @@
   1.127       #known_failures spass_config @
   1.128       [(OldSpass, "unrecognized option `-TPTP'"),
   1.129        (OldSpass, "Unrecognized option TPTP")],
   1.130 -   max_new_clauses = #max_new_clauses spass_config,
   1.131 +   max_axiom_clauses = #max_axiom_clauses spass_config,
   1.132     prefers_theory_relevant = #prefers_theory_relevant spass_config}
   1.133  val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config
   1.134  
   1.135 @@ -367,17 +369,17 @@
   1.136    [(TimedOut, "says Timeout"),
   1.137     (MalformedOutput, "Remote script could not extract proof")]
   1.138  
   1.139 -fun remote_prover_config prover_prefix args
   1.140 -        ({proof_delims, known_failures, max_new_clauses,
   1.141 +fun remote_prover_config atp_prefix args
   1.142 +        ({proof_delims, known_failures, max_axiom_clauses,
   1.143            prefers_theory_relevant, ...} : prover_config) : prover_config =
   1.144    {home = getenv "ISABELLE_ATP_MANAGER",
   1.145     executable = "SystemOnTPTP",
   1.146 -   arguments = (fn timeout =>
   1.147 -     args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^
   1.148 -     the_system prover_prefix),
   1.149 +   arguments = fn timeout =>
   1.150 +     args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
   1.151 +     the_system atp_prefix,
   1.152     proof_delims = insert (op =) tstp_proof_delims proof_delims,
   1.153     known_failures = remote_known_failures @ known_failures,
   1.154 -   max_new_clauses = max_new_clauses,
   1.155 +   max_axiom_clauses = max_axiom_clauses,
   1.156     prefers_theory_relevant = prefers_theory_relevant}
   1.157  
   1.158  val remote_vampire =