# HG changeset patch # User blanchet # Date 1334669143 -7200 # Node ID d52da3e7aa4cc199e2a67bbda87b27a59a75698d # Parent da72e05849ef0a9890ed4da0a85931a741462d68# Parent aa1b8a59017fd685ab19b4ecb55d08ebc6ef7545 merged diff -r aa1b8a59017f -r d52da3e7aa4c src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Tue Apr 17 14:56:38 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Apr 17 15:25:43 2012 +0200 @@ -109,7 +109,7 @@ "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^ " " -fun string_for_failure Unprovable = "The problem is unprovable." +fun string_for_failure Unprovable = "The generated problem is unprovable." | string_for_failure GaveUp = "The prover gave up." | string_for_failure ProofMissing = "The prover claims the conjecture is a theorem but did not provide a proof." @@ -128,7 +128,7 @@ | string_for_failure CantConnect = "Cannot connect to remote server." | string_for_failure TimedOut = "Timed out." | string_for_failure Inappropriate = - "The problem lies outside the prover's scope." + "The generated problem lies outside the prover's scope." | string_for_failure OutOfResources = "The prover ran out of resources." | string_for_failure NoPerl = "Perl" ^ missing_message_tail | string_for_failure NoLibwwwPerl = diff -r aa1b8a59017f -r d52da3e7aa4c src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Apr 17 14:56:38 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Apr 17 15:25:43 2012 +0200 @@ -253,9 +253,8 @@ (* supplied by Stephan Schulz *) "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ \--destructive-er-aggressive --destructive-er --presat-simplify \ - \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ - \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ - \-H'(4*" ^ + \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ + \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^ e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^ "(SimulateSOS, " ^ (e_selection_heuristic_case heuristic @@ -287,6 +286,8 @@ fun effective_e_selection_heuristic ctxt = if is_new_e_version () then Config.get ctxt e_selection_heuristic else e_autoN +fun e_kbo () = if is_new_e_version () then "KBO6" else "KBO" + val e_config : atp_config = {exec = (["E_HOME"], "eproof"), required_vars = [], @@ -296,7 +297,7 @@ "--tstp-in --tstp-out --output-level=5 --silent " ^ e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^ e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^ - "--term-ordering=" ^ (if is_lpo then "LPO4" else "KBO6") ^ " " ^ + "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout), proof_delims = tstp_proof_delims, known_failures = @@ -638,6 +639,7 @@ remote_atp waldmeisterN "Waldmeister" ["710"] [("#START OF PROOF", "Proved Goals:")] [(OutOfResources, "Too many function symbols"), + (Inappropriate, "**** Unexpected end of file."), (Crashed, "Unrecoverable Segmentation Fault")] Hypothesis Hypothesis (K ((50, CNF_UEQ, "mono_tags??", combsN, false), "") (* FUDGE *))