keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
authorblanchet
Fri Jul 23 21:29:29 2010 +0200 (2010-07-23)
changeset 37962d7dbe01f48d7
parent 37961 6a48c85a211a
child 37963 61887e5b3d1d
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.
src/HOL/Tools/ATP_Manager/SPASS_TPTP
src/HOL/Tools/ATP_Manager/atp_systems.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/ATP_Manager/SPASS_TPTP	Fri Jul 23 21:29:29 2010 +0200
     1.3 @@ -0,0 +1,18 @@
     1.4 +#!/usr/bin/env bash
     1.5 +#
     1.6 +# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
     1.7 +# Isar proof reconstruction)
     1.8 +#
     1.9 +# Author: Jasmin Blanchette, TU Muenchen
    1.10 +
    1.11 +options=${@:1:$(($#-1))}
    1.12 +name=${@:$(($#)):1}
    1.13 +
    1.14 +$SPASS_HOME/tptp2dfg $name $name.fof.dfg
    1.15 +$SPASS_HOME/SPASS -Flotter $name.fof.dfg \
    1.16 +    | sed 's/description({$/description({*/' \
    1.17 +    > $name.cnf.dfg
    1.18 +rm -f $name.fof.dfg
    1.19 +cat $name.cnf.dfg
    1.20 +$SPASS_HOME/SPASS $options $name.cnf.dfg
    1.21 +rm -f $name.cnf.dfg
     2.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jul 23 15:04:49 2010 +0200
     2.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jul 23 21:29:29 2010 +0200
     2.3 @@ -239,6 +239,43 @@
     2.4         class_rel_clauses, arity_clauses))
     2.5    end
     2.6  
     2.7 +fun extract_clause_sequence output =
     2.8 +  let
     2.9 +    val tokens_of = String.tokens (not o Char.isAlphaNum)
    2.10 +    fun extract_num ("clause" :: (ss as _ :: _)) =
    2.11 +    Int.fromString (List.last ss)
    2.12 +      | extract_num _ = NONE
    2.13 +  in output |> split_lines |> map_filter (extract_num o tokens_of) end
    2.14 +
    2.15 +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
    2.16 +
    2.17 +val parse_clause_formula_pair =
    2.18 +  $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
    2.19 +  --| Scan.option ($$ ",")
    2.20 +val parse_clause_formula_relation =
    2.21 +  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
    2.22 +  |-- Scan.repeat parse_clause_formula_pair
    2.23 +val extract_clause_formula_relation =
    2.24 +  Substring.full
    2.25 +  #> Substring.position set_ClauseFormulaRelationN
    2.26 +  #> snd #> Substring.string #> strip_spaces #> explode
    2.27 +  #> parse_clause_formula_relation #> fst
    2.28 +
    2.29 +fun repair_theorem_names output thm_names =
    2.30 +  if String.isSubstring set_ClauseFormulaRelationN output then
    2.31 +    let
    2.32 +      val seq = extract_clause_sequence output
    2.33 +      val name_map = extract_clause_formula_relation output
    2.34 +    in
    2.35 +      seq |> map (the o AList.lookup (op =) name_map)
    2.36 +          |> map (fn s => case try (unprefix axiom_prefix) s of
    2.37 +                            SOME s' => undo_ascii_of s'
    2.38 +                          | NONE => "")
    2.39 +          |> Vector.fromList
    2.40 +    end
    2.41 +  else
    2.42 +    thm_names
    2.43 +
    2.44  
    2.45  (* generic TPTP-based provers *)
    2.46  
    2.47 @@ -298,15 +335,7 @@
    2.48          (if Config.get ctxt measure_runtime then
    2.49             "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
    2.50           else
    2.51 -           "exec " ^ core) ^ " 2>&1" ^
    2.52 -        (if overlord then
    2.53 -           " | sed 's/,/, /g' \
    2.54 -           \| sed 's/\\([^!=<]\\)\\([=|]\\)\\([^=>]\\)/\\1 \\2 \\3/g' \
    2.55 -           \| sed 's/  / /g' | sed 's/| |/||/g' \
    2.56 -           \| sed 's/ = = =/===/g' \
    2.57 -           \| sed 's/= = /== /g'"
    2.58 -         else
    2.59 -           "")
    2.60 +           "exec " ^ core) ^ " 2>&1"
    2.61        end
    2.62      fun split_time s =
    2.63        let
    2.64 @@ -320,7 +349,9 @@
    2.65          val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
    2.66        in (output, as_time t) end;
    2.67      fun run_on probfile =
    2.68 -      if File.exists command then
    2.69 +      if home = "" then
    2.70 +        error ("The environment variable " ^ quote home_var ^ " is not set.")
    2.71 +      else if File.exists command then
    2.72          let
    2.73            fun do_run complete =
    2.74              let
    2.75 @@ -350,8 +381,6 @@
    2.76                            (output, msecs0 + msecs, proof, outcome))
    2.77                   | result => result)
    2.78          in ((pool, conjecture_shape), result) end
    2.79 -      else if home = "" then
    2.80 -        error ("The environment variable " ^ quote home_var ^ " is not set.")
    2.81        else
    2.82          error ("Bad executable: " ^ Path.implode command ^ ".");
    2.83  
    2.84 @@ -367,6 +396,7 @@
    2.85  
    2.86      val ((pool, conjecture_shape), (output, msecs, proof, outcome)) =
    2.87        with_path cleanup export run_on (prob_pathname subgoal)
    2.88 +    val internal_thm_names = repair_theorem_names output internal_thm_names
    2.89  
    2.90      val (message, relevant_thm_names) =
    2.91        case outcome of
    2.92 @@ -417,11 +447,11 @@
    2.93  (* The "-VarWeight=3" option helps the higher-order problems, probably by
    2.94     counteracting the presence of "hAPP". *)
    2.95  val spass_config : prover_config =
    2.96 -  {home_var = "SPASS_HOME",
    2.97 -   executable = "SPASS",
    2.98 +  {home_var = "ISABELLE_ATP_MANAGER",
    2.99 +   executable = "SPASS_TPTP",
   2.100     (* "div 2" accounts for the fact that SPASS is often run twice. *)
   2.101     arguments = fn complete => fn timeout =>
   2.102 -     ("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   2.103 +     ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   2.104        \-VarWeight=3 -TimeLimit=" ^
   2.105        string_of_int (to_generous_secs timeout div 2))
   2.106       |> not complete ? prefix "-SOS=1 ",
   2.107 @@ -432,8 +462,7 @@
   2.108        (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
   2.109        (MalformedInput, "Undefined symbol"),
   2.110        (MalformedInput, "Free Variable"),
   2.111 -      (OldSpass, "unrecognized option `-TPTP'"),
   2.112 -      (OldSpass, "Unrecognized option TPTP")],
   2.113 +      (OldSpass, "tptp2dfg")],
   2.114     max_axiom_clauses = 40,
   2.115     prefers_theory_relevant = true}
   2.116  val spass = tptp_prover "spass" spass_config
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jul 23 15:04:49 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jul 23 21:29:29 2010 +0200
     3.3 @@ -33,12 +33,11 @@
     3.4  
     3.5  type minimize_command = string list -> string
     3.6  
     3.7 -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
     3.8 -fun is_head_digit s = Char.isDigit (String.sub (s, 0))
     3.9 -
    3.10  val index_in_shape : int -> int list list -> int =
    3.11    find_index o exists o curry (op =)
    3.12 -fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
    3.13 +fun is_axiom_clause_number thm_names num =
    3.14 +  num > 0 andalso num <= Vector.length thm_names andalso
    3.15 +  Vector.sub (thm_names, num - 1) <> ""
    3.16  fun is_conjecture_clause_number conjecture_shape num =
    3.17    index_in_shape num conjecture_shape >= 0
    3.18  
    3.19 @@ -57,23 +56,6 @@
    3.20  
    3.21  (**** PARSING OF TSTP FORMAT ****)
    3.22  
    3.23 -fun strip_spaces_in_list [] = ""
    3.24 -  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
    3.25 -  | strip_spaces_in_list [c1, c2] =
    3.26 -    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
    3.27 -  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
    3.28 -    if Char.isSpace c1 then
    3.29 -      strip_spaces_in_list (c2 :: c3 :: cs)
    3.30 -    else if Char.isSpace c2 then
    3.31 -      if Char.isSpace c3 then
    3.32 -        strip_spaces_in_list (c1 :: c3 :: cs)
    3.33 -      else
    3.34 -        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
    3.35 -        strip_spaces_in_list (c3 :: cs)
    3.36 -    else
    3.37 -      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
    3.38 -val strip_spaces = strip_spaces_in_list o String.explode
    3.39 -
    3.40  (* Syntax trees, either term list or formulae *)
    3.41  datatype node = IntLeaf of int | StrNode of string * node list
    3.42  
    3.43 @@ -85,9 +67,6 @@
    3.44  (*Strings enclosed in single quotes, e.g. filenames*)
    3.45  val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
    3.46  
    3.47 -(*Integer constants, typically proof line numbers*)
    3.48 -val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
    3.49 -
    3.50  val parse_dollar_name =
    3.51    Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
    3.52  
    3.53 @@ -102,7 +81,7 @@
    3.54     forever at compile time. *)
    3.55  fun parse_term pool x =
    3.56       (parse_quoted >> str_leaf
    3.57 -   || parse_integer >> IntLeaf
    3.58 +   || scan_integer >> IntLeaf
    3.59     || (parse_dollar_name >> repair_name pool)
    3.60        -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
    3.61     || $$ "(" |-- parse_term pool --| $$ ")"
    3.62 @@ -149,11 +128,11 @@
    3.63  fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
    3.64  fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
    3.65  fun parse_tstp_line pool =
    3.66 -     ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
    3.67 +     ((Scan.this_string "fof" -- $$ "(") |-- scan_integer --| $$ ","
    3.68         --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
    3.69         --| parse_tstp_annotations --| $$ ")" --| $$ "."
    3.70        >> finish_tstp_definition_line)
    3.71 -  || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
    3.72 +  || ((Scan.this_string "cnf" -- $$ "(") |-- scan_integer --| $$ ","
    3.73         --| Symbol.scan_id --| $$ "," -- parse_clause pool
    3.74         -- parse_tstp_annotations --| $$ ")" --| $$ "."
    3.75        >> finish_tstp_inference_line)
    3.76 @@ -162,7 +141,7 @@
    3.77  
    3.78  (* SPASS returns clause references of the form "x.y". We ignore "y", whose role
    3.79     is not clear anyway. *)
    3.80 -val parse_dot_name = parse_integer --| $$ "." --| parse_integer
    3.81 +val parse_dot_name = scan_integer --| $$ "." --| scan_integer
    3.82  
    3.83  val parse_spass_annotations =
    3.84    Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
    3.85 @@ -185,7 +164,7 @@
    3.86     <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
    3.87  fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
    3.88  fun parse_spass_line pool =
    3.89 -  parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
    3.90 +  scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
    3.91    -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
    3.92    >> finish_spass_line
    3.93  
    3.94 @@ -535,7 +514,7 @@
    3.95     extracted. *)
    3.96  fun extract_formula_numbers_in_atp_proof atp_proof =
    3.97    let
    3.98 -    val tokens_of = String.tokens (not o is_ident_char)
    3.99 +    val tokens_of = String.tokens (not o Char.isAlphaNum)
   3.100      fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num
   3.101        | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
   3.102        | extract_num _ = NONE
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Fri Jul 23 15:04:49 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Fri Jul 23 21:29:29 2010 +0200
     4.3 @@ -11,6 +11,7 @@
     4.4    type arity_clause = Metis_Clauses.arity_clause
     4.5    type fol_clause = Metis_Clauses.fol_clause
     4.6  
     4.7 +  val axiom_prefix : string
     4.8    val write_tptp_file :
     4.9      theory -> bool -> bool -> bool -> Path.T
    4.10      -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
    4.11 @@ -136,11 +137,11 @@
    4.12  
    4.13  (** Sledgehammer stuff **)
    4.14  
    4.15 -val clause_prefix = "cls_"
    4.16 +val axiom_prefix = "ax_"
    4.17 +val conjecture_prefix = "conj_"
    4.18  val arity_clause_prefix = "clsarity_"
    4.19  
    4.20 -fun hol_ident axiom_name clause_id =
    4.21 -  clause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id
    4.22 +fun hol_ident prefix axiom_name = prefix ^ ascii_of axiom_name
    4.23  
    4.24  fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
    4.25  
    4.26 @@ -189,8 +190,8 @@
    4.27    |> formula_for_fo_literals
    4.28  
    4.29  fun problem_line_for_axiom full_types
    4.30 -        (clause as FOLClause {axiom_name, clause_id, kind, ...}) =
    4.31 -  Fof (hol_ident axiom_name clause_id, kind,
    4.32 +        (clause as FOLClause {axiom_name, kind, ...}) =
    4.33 +  Fof (hol_ident axiom_prefix axiom_name, kind,
    4.34         formula_for_axiom full_types clause)
    4.35  
    4.36  fun problem_line_for_class_rel_clause
    4.37 @@ -213,8 +214,8 @@
    4.38         |> formula_for_fo_literals)
    4.39  
    4.40  fun problem_line_for_conjecture full_types
    4.41 -        (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) =
    4.42 -  Fof (hol_ident axiom_name clause_id, kind,
    4.43 +        (clause as FOLClause {axiom_name, kind, literals, ...}) =
    4.44 +  Fof (hol_ident conjecture_prefix axiom_name, kind,
    4.45         map (fo_literal_for_literal full_types) literals
    4.46         |> formula_for_fo_literals |> mk_anot)
    4.47  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 23 15:04:49 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 23 21:29:29 2010 +0200
     5.3 @@ -9,8 +9,10 @@
     5.4    val plural_s : int -> string
     5.5    val serial_commas : string -> string list -> string list
     5.6    val timestamp : unit -> string
     5.7 +  val strip_spaces : string -> string
     5.8    val parse_bool_option : bool -> string -> string -> bool option
     5.9    val parse_time_option : string -> string -> Time.time option
    5.10 +  val scan_integer : string list -> int * string list
    5.11    val nat_subscript : int -> string
    5.12    val unyxml : string -> string
    5.13    val maybe_quote : string -> string
    5.14 @@ -31,6 +33,25 @@
    5.15  
    5.16  val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
    5.17  
    5.18 +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    5.19 +
    5.20 +fun strip_spaces_in_list [] = ""
    5.21 +  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
    5.22 +  | strip_spaces_in_list [c1, c2] =
    5.23 +    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
    5.24 +  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
    5.25 +    if Char.isSpace c1 then
    5.26 +      strip_spaces_in_list (c2 :: c3 :: cs)
    5.27 +    else if Char.isSpace c2 then
    5.28 +      if Char.isSpace c3 then
    5.29 +        strip_spaces_in_list (c1 :: c3 :: cs)
    5.30 +      else
    5.31 +        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
    5.32 +        strip_spaces_in_list (c3 :: cs)
    5.33 +    else
    5.34 +      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
    5.35 +val strip_spaces = strip_spaces_in_list o String.explode
    5.36 +
    5.37  fun parse_bool_option option name s =
    5.38    (case s of
    5.39       "smart" => if option then NONE else raise Option
    5.40 @@ -61,6 +82,9 @@
    5.41          SOME (Time.fromMilliseconds msecs)
    5.42      end
    5.43  
    5.44 +fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    5.45 +val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
    5.46 +
    5.47  val subscript = implode o map (prefix "\<^isub>") o explode
    5.48  fun nat_subscript n =
    5.49    n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript