# HG changeset patch # User blanchet # Date 1279913369 -7200 # Node ID d7dbe01f48d7abf366e0f8cea0f7ebcebf0cbd05 # Parent 6a48c85a211ad36ccf488d1ee9b7d13a8c587739 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; this is rather involved because the Flotter FOF-to-CNF translator is normally implicit. We must make this an explicit step and parse the Flotter output to find out which clauses correspond to which formulas. diff -r 6a48c85a211a -r d7dbe01f48d7 src/HOL/Tools/ATP_Manager/SPASS_TPTP --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP_Manager/SPASS_TPTP Fri Jul 23 21:29:29 2010 +0200 @@ -0,0 +1,18 @@ +#!/usr/bin/env bash +# +# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for +# Isar proof reconstruction) +# +# Author: Jasmin Blanchette, TU Muenchen + +options=${@:1:$(($#-1))} +name=${@:$(($#)):1} + +$SPASS_HOME/tptp2dfg $name $name.fof.dfg +$SPASS_HOME/SPASS -Flotter $name.fof.dfg \ + | sed 's/description({$/description({*/' \ + > $name.cnf.dfg +rm -f $name.fof.dfg +cat $name.cnf.dfg +$SPASS_HOME/SPASS $options $name.cnf.dfg +rm -f $name.cnf.dfg diff -r 6a48c85a211a -r d7dbe01f48d7 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jul 23 15:04:49 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jul 23 21:29:29 2010 +0200 @@ -239,6 +239,43 @@ class_rel_clauses, arity_clauses)) end +fun extract_clause_sequence output = + let + val tokens_of = String.tokens (not o Char.isAlphaNum) + fun extract_num ("clause" :: (ss as _ :: _)) = + Int.fromString (List.last ss) + | extract_num _ = NONE + in output |> split_lines |> map_filter (extract_num o tokens_of) end + +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" + +val parse_clause_formula_pair = + $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")" + --| Scan.option ($$ ",") +val parse_clause_formula_relation = + Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" + |-- Scan.repeat parse_clause_formula_pair +val extract_clause_formula_relation = + Substring.full + #> Substring.position set_ClauseFormulaRelationN + #> snd #> Substring.string #> strip_spaces #> explode + #> parse_clause_formula_relation #> fst + +fun repair_theorem_names output thm_names = + if String.isSubstring set_ClauseFormulaRelationN output then + let + val seq = extract_clause_sequence output + val name_map = extract_clause_formula_relation output + in + seq |> map (the o AList.lookup (op =) name_map) + |> map (fn s => case try (unprefix axiom_prefix) s of + SOME s' => undo_ascii_of s' + | NONE => "") + |> Vector.fromList + end + else + thm_names + (* generic TPTP-based provers *) @@ -298,15 +335,7 @@ (if Config.get ctxt measure_runtime then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" else - "exec " ^ core) ^ " 2>&1" ^ - (if overlord then - " | sed 's/,/, /g' \ - \| sed 's/\\([^!=<]\\)\\([=|]\\)\\([^=>]\\)/\\1 \\2 \\3/g' \ - \| sed 's/ / /g' | sed 's/| |/||/g' \ - \| sed 's/ = = =/===/g' \ - \| sed 's/= = /== /g'" - else - "") + "exec " ^ core) ^ " 2>&1" end fun split_time s = let @@ -320,7 +349,9 @@ val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; in (output, as_time t) end; fun run_on probfile = - if File.exists command then + if home = "" then + error ("The environment variable " ^ quote home_var ^ " is not set.") + else if File.exists command then let fun do_run complete = let @@ -350,8 +381,6 @@ (output, msecs0 + msecs, proof, outcome)) | result => result) in ((pool, conjecture_shape), result) end - else if home = "" then - error ("The environment variable " ^ quote home_var ^ " is not set.") else error ("Bad executable: " ^ Path.implode command ^ "."); @@ -367,6 +396,7 @@ val ((pool, conjecture_shape), (output, msecs, proof, outcome)) = with_path cleanup export run_on (prob_pathname subgoal) + val internal_thm_names = repair_theorem_names output internal_thm_names val (message, relevant_thm_names) = case outcome of @@ -417,11 +447,11 @@ (* The "-VarWeight=3" option helps the higher-order problems, probably by counteracting the presence of "hAPP". *) val spass_config : prover_config = - {home_var = "SPASS_HOME", - executable = "SPASS", + {home_var = "ISABELLE_ATP_MANAGER", + executable = "SPASS_TPTP", (* "div 2" accounts for the fact that SPASS is often run twice. *) arguments = fn complete => fn timeout => - ("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ + ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout div 2)) |> not complete ? prefix "-SOS=1 ", @@ -432,8 +462,7 @@ (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), - (OldSpass, "unrecognized option `-TPTP'"), - (OldSpass, "Unrecognized option TPTP")], + (OldSpass, "tptp2dfg")], max_axiom_clauses = 40, prefers_theory_relevant = true} val spass = tptp_prover "spass" spass_config diff -r 6a48c85a211a -r d7dbe01f48d7 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jul 23 15:04:49 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jul 23 21:29:29 2010 +0200 @@ -33,12 +33,11 @@ type minimize_command = string list -> string -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" -fun is_head_digit s = Char.isDigit (String.sub (s, 0)) - val index_in_shape : int -> int list list -> int = find_index o exists o curry (op =) -fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names +fun is_axiom_clause_number thm_names num = + num > 0 andalso num <= Vector.length thm_names andalso + Vector.sub (thm_names, num - 1) <> "" fun is_conjecture_clause_number conjecture_shape num = index_in_shape num conjecture_shape >= 0 @@ -57,23 +56,6 @@ (**** PARSING OF TSTP FORMAT ****) -fun strip_spaces_in_list [] = "" - | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1 - | strip_spaces_in_list [c1, c2] = - strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2] - | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) = - if Char.isSpace c1 then - strip_spaces_in_list (c2 :: c3 :: cs) - else if Char.isSpace c2 then - if Char.isSpace c3 then - strip_spaces_in_list (c1 :: c3 :: cs) - else - str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^ - strip_spaces_in_list (c3 :: cs) - else - str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs) -val strip_spaces = strip_spaces_in_list o String.explode - (* Syntax trees, either term list or formulae *) datatype node = IntLeaf of int | StrNode of string * node list @@ -85,9 +67,6 @@ (*Strings enclosed in single quotes, e.g. filenames*) val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode; -(*Integer constants, typically proof line numbers*) -val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) - val parse_dollar_name = Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s) @@ -102,7 +81,7 @@ forever at compile time. *) fun parse_term pool x = (parse_quoted >> str_leaf - || parse_integer >> IntLeaf + || scan_integer >> IntLeaf || (parse_dollar_name >> repair_name pool) -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode || $$ "(" |-- parse_term pool --| $$ ")" @@ -149,11 +128,11 @@ fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us) fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps) fun parse_tstp_line pool = - ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ "," + ((Scan.this_string "fof" -- $$ "(") |-- scan_integer --| $$ "," --| Scan.this_string "definition" --| $$ "," -- parse_definition pool --| parse_tstp_annotations --| $$ ")" --| $$ "." >> finish_tstp_definition_line) - || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ "," + || ((Scan.this_string "cnf" -- $$ "(") |-- scan_integer --| $$ "," --| Symbol.scan_id --| $$ "," -- parse_clause pool -- parse_tstp_annotations --| $$ ")" --| $$ "." >> finish_tstp_inference_line) @@ -162,7 +141,7 @@ (* SPASS returns clause references of the form "x.y". We ignore "y", whose role is not clear anyway. *) -val parse_dot_name = parse_integer --| $$ "." --| parse_integer +val parse_dot_name = scan_integer --| $$ "." --| scan_integer val parse_spass_annotations = Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name @@ -185,7 +164,7 @@ || -> . *) fun finish_spass_line ((num, deps), us) = Inference (num, us, deps) fun parse_spass_line pool = - parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id + scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "." >> finish_spass_line @@ -535,7 +514,7 @@ extracted. *) fun extract_formula_numbers_in_atp_proof atp_proof = let - val tokens_of = String.tokens (not o is_ident_char) + val tokens_of = String.tokens (not o Char.isAlphaNum) fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num | extract_num _ = NONE diff -r 6a48c85a211a -r d7dbe01f48d7 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Fri Jul 23 15:04:49 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Fri Jul 23 21:29:29 2010 +0200 @@ -11,6 +11,7 @@ type arity_clause = Metis_Clauses.arity_clause type fol_clause = Metis_Clauses.fol_clause + val axiom_prefix : string val write_tptp_file : theory -> bool -> bool -> bool -> Path.T -> fol_clause list * fol_clause list * fol_clause list * fol_clause list @@ -136,11 +137,11 @@ (** Sledgehammer stuff **) -val clause_prefix = "cls_" +val axiom_prefix = "ax_" +val conjecture_prefix = "conj_" val arity_clause_prefix = "clsarity_" -fun hol_ident axiom_name clause_id = - clause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id +fun hol_ident prefix axiom_name = prefix ^ ascii_of axiom_name fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) @@ -189,8 +190,8 @@ |> formula_for_fo_literals fun problem_line_for_axiom full_types - (clause as FOLClause {axiom_name, clause_id, kind, ...}) = - Fof (hol_ident axiom_name clause_id, kind, + (clause as FOLClause {axiom_name, kind, ...}) = + Fof (hol_ident axiom_prefix axiom_name, kind, formula_for_axiom full_types clause) fun problem_line_for_class_rel_clause @@ -213,8 +214,8 @@ |> formula_for_fo_literals) fun problem_line_for_conjecture full_types - (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) = - Fof (hol_ident axiom_name clause_id, kind, + (clause as FOLClause {axiom_name, kind, literals, ...}) = + Fof (hol_ident conjecture_prefix axiom_name, kind, map (fo_literal_for_literal full_types) literals |> formula_for_fo_literals |> mk_anot) diff -r 6a48c85a211a -r d7dbe01f48d7 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 23 15:04:49 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 23 21:29:29 2010 +0200 @@ -9,8 +9,10 @@ val plural_s : int -> string val serial_commas : string -> string list -> string list val timestamp : unit -> string + val strip_spaces : string -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option + val scan_integer : string list -> int * string list val nat_subscript : int -> string val unyxml : string -> string val maybe_quote : string -> string @@ -31,6 +33,25 @@ val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" + +fun strip_spaces_in_list [] = "" + | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1 + | strip_spaces_in_list [c1, c2] = + strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2] + | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) = + if Char.isSpace c1 then + strip_spaces_in_list (c2 :: c3 :: cs) + else if Char.isSpace c2 then + if Char.isSpace c3 then + strip_spaces_in_list (c1 :: c3 :: cs) + else + str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^ + strip_spaces_in_list (c3 :: cs) + else + str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs) +val strip_spaces = strip_spaces_in_list o String.explode + fun parse_bool_option option name s = (case s of "smart" => if option then NONE else raise Option @@ -61,6 +82,9 @@ SOME (Time.fromMilliseconds msecs) end +fun is_head_digit s = Char.isDigit (String.sub (s, 0)) +val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) + val subscript = implode o map (prefix "\<^isub>") o explode fun nat_subscript n = n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript