1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 25 09:42:28 2010 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 25 17:49:52 2010 +0200
1.3 @@ -19,7 +19,7 @@
1.4 has_incomplete_mode: bool,
1.5 proof_delims: (string * string) list,
1.6 known_failures: (failure * string) list,
1.7 - default_max_relevant_per_iter: int,
1.8 + default_max_relevant: int,
1.9 default_theory_relevant: bool,
1.10 explicit_forall: bool,
1.11 use_conjecture_for_hypotheses: bool}
1.12 @@ -52,7 +52,7 @@
1.13 has_incomplete_mode: bool,
1.14 proof_delims: (string * string) list,
1.15 known_failures: (failure * string) list,
1.16 - default_max_relevant_per_iter: int,
1.17 + default_max_relevant: int,
1.18 default_theory_relevant: bool,
1.19 explicit_forall: bool,
1.20 use_conjecture_for_hypotheses: bool}
1.21 @@ -159,7 +159,7 @@
1.22 "# Cannot determine problem status within resource limit"),
1.23 (OutOfResources, "SZS status: ResourceOut"),
1.24 (OutOfResources, "SZS status ResourceOut")],
1.25 - default_max_relevant_per_iter = 80 (* FUDGE *),
1.26 + default_max_relevant = 500 (* FUDGE *),
1.27 default_theory_relevant = false,
1.28 explicit_forall = false,
1.29 use_conjecture_for_hypotheses = true}
1.30 @@ -186,7 +186,7 @@
1.31 (MalformedInput, "Undefined symbol"),
1.32 (MalformedInput, "Free Variable"),
1.33 (SpassTooOld, "tptp2dfg")],
1.34 - default_max_relevant_per_iter = 40 (* FUDGE *),
1.35 + default_max_relevant = 350 (* FUDGE *),
1.36 default_theory_relevant = true,
1.37 explicit_forall = true,
1.38 use_conjecture_for_hypotheses = true}
1.39 @@ -199,10 +199,11 @@
1.40 val vampire_config : prover_config =
1.41 {exec = ("VAMPIRE_HOME", "vampire"),
1.42 required_execs = [],
1.43 - arguments = fn _ => fn timeout =>
1.44 - "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
1.45 - " --thanks Andrei --input_file",
1.46 - has_incomplete_mode = false,
1.47 + arguments = fn complete => fn timeout =>
1.48 + ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
1.49 + " --thanks Andrei --input_file")
1.50 + |> not complete ? prefix "--sos on ",
1.51 + has_incomplete_mode = true,
1.52 proof_delims =
1.53 [("=========== Refutation ==========",
1.54 "======= End of refutation ======="),
1.55 @@ -215,7 +216,7 @@
1.56 (Unprovable, "Satisfiability detected"),
1.57 (Unprovable, "Termination reason: Satisfiable"),
1.58 (VampireTooOld, "not a valid option")],
1.59 - default_max_relevant_per_iter = 45 (* FUDGE *),
1.60 + default_max_relevant = 400 (* FUDGE *),
1.61 default_theory_relevant = false,
1.62 explicit_forall = false,
1.63 use_conjecture_for_hypotheses = true}
1.64 @@ -255,7 +256,7 @@
1.65 | SOME sys => sys
1.66
1.67 fun remote_config system_name system_versions proof_delims known_failures
1.68 - default_max_relevant_per_iter default_theory_relevant
1.69 + default_max_relevant default_theory_relevant
1.70 use_conjecture_for_hypotheses : prover_config =
1.71 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
1.72 required_execs = [],
1.73 @@ -267,26 +268,26 @@
1.74 known_failures =
1.75 known_failures @ known_perl_failures @
1.76 [(TimedOut, "says Timeout")],
1.77 - default_max_relevant_per_iter = default_max_relevant_per_iter,
1.78 + default_max_relevant = default_max_relevant,
1.79 default_theory_relevant = default_theory_relevant,
1.80 explicit_forall = true,
1.81 use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
1.82
1.83 fun remotify_config system_name system_versions
1.84 - ({proof_delims, known_failures, default_max_relevant_per_iter,
1.85 + ({proof_delims, known_failures, default_max_relevant,
1.86 default_theory_relevant, use_conjecture_for_hypotheses, ...}
1.87 : prover_config) : prover_config =
1.88 remote_config system_name system_versions proof_delims known_failures
1.89 - default_max_relevant_per_iter default_theory_relevant
1.90 + default_max_relevant default_theory_relevant
1.91 use_conjecture_for_hypotheses
1.92
1.93 val remotify_name = prefix "remote_"
1.94 fun remote_prover name system_name system_versions proof_delims known_failures
1.95 - default_max_relevant_per_iter default_theory_relevant
1.96 + default_max_relevant default_theory_relevant
1.97 use_conjecture_for_hypotheses =
1.98 (remotify_name name,
1.99 remote_config system_name system_versions proof_delims known_failures
1.100 - default_max_relevant_per_iter default_theory_relevant
1.101 + default_max_relevant default_theory_relevant
1.102 use_conjecture_for_hypotheses)
1.103 fun remotify_prover (name, config) system_name system_versions =
1.104 (remotify_name name, remotify_config system_name system_versions config)
1.105 @@ -294,11 +295,11 @@
1.106 val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
1.107 val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"]
1.108 val remote_sine_e =
1.109 - remote_prover "sine_e" "SInE" [] []
1.110 - [(Unprovable, "says Unknown")] 150 (* FUDGE *) false true
1.111 + remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
1.112 + 1000 (* FUDGE *) false true
1.113 val remote_snark =
1.114 remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
1.115 - 50 (* FUDGE *) false true
1.116 + 350 (* FUDGE *) false true
1.117
1.118 (* Setup *)
1.119