added timeout argument to TPTP tools
authorblanchet
Sun Apr 22 14:16:46 2012 +0200 (2012-04-22)
changeset 4767024babc4b1925
parent 47669 f3896a53043f
child 47671 ab44addc81e2
added timeout argument to TPTP tools
src/HOL/TPTP/ATP_Problem_Import.thy
src/HOL/TPTP/atp_problem_import.ML
src/HOL/TPTP/lib/Tools/tptp_isabelle
src/HOL/TPTP/lib/Tools/tptp_nitpick
src/HOL/TPTP/lib/Tools/tptp_refute
src/HOL/TPTP/lib/Tools/tptp_sledgehammer
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Apr 22 14:16:46 2012 +0200
     1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Sun Apr 22 14:16:46 2012 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  uses ("atp_problem_import.ML")
     1.5  begin
     1.6  
     1.7 +declare [[show_consts]] (* for Refute *)
     1.8 +
     1.9  typedecl iota (* for TPTP *)
    1.10  
    1.11  use "atp_problem_import.ML"
     2.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Sun Apr 22 14:16:46 2012 +0200
     2.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Sun Apr 22 14:16:46 2012 +0200
     2.3 @@ -7,10 +7,10 @@
     2.4  
     2.5  signature ATP_PROBLEM_IMPORT =
     2.6  sig
     2.7 -  val isabelle_tptp_file : string -> unit
     2.8 -  val nitpick_tptp_file : string -> unit
     2.9 -  val refute_tptp_file : string -> unit
    2.10 -  val sledgehammer_tptp_file : string -> unit
    2.11 +  val isabelle_tptp_file : int -> string -> unit
    2.12 +  val nitpick_tptp_file : int -> string -> unit
    2.13 +  val refute_tptp_file : int -> string -> unit
    2.14 +  val sledgehammer_tptp_file : int -> string -> unit
    2.15    val translate_tptp_file : string -> string -> string -> unit
    2.16  end;
    2.17  
    2.18 @@ -150,12 +150,12 @@
    2.19  
    2.20  (** Isabelle (combination of provers) **)
    2.21  
    2.22 -fun isabelle_tptp_file file_name = ()
    2.23 +fun isabelle_tptp_file timeout file_name = ()
    2.24  
    2.25  
    2.26  (** Nitpick (alias Nitrox) **)
    2.27  
    2.28 -fun nitpick_tptp_file file_name =
    2.29 +fun nitpick_tptp_file timeout file_name =
    2.30    let
    2.31      val (falsify, ts) = read_tptp_file @{theory} file_name
    2.32      val state = Proof.init @{context}
    2.33 @@ -172,8 +172,7 @@
    2.34         ("show_consts", "true"),
    2.35         ("format", "1000"),
    2.36         ("max_potential", "0"),
    2.37 -       ("timeout", "none"),
    2.38 -       ("expect", Nitpick.genuineN)]
    2.39 +       ("timeout", string_of_int timeout)]
    2.40        |> Nitpick_Isar.default_params @{theory}
    2.41      val i = 1
    2.42      val n = 1
    2.43 @@ -195,13 +194,11 @@
    2.44       "Unknown")
    2.45    |> writeln
    2.46  
    2.47 -fun refute_tptp_file file_name =
    2.48 +fun refute_tptp_file timeout file_name =
    2.49    let
    2.50      val (falsify, ts) = read_tptp_file @{theory} file_name
    2.51      val params =
    2.52 -      [("maxtime", "10000"),
    2.53 -       ("assms", "true"),
    2.54 -       ("expect", Nitpick.genuineN)]
    2.55 +      [("maxtime", string_of_int timeout)]
    2.56    in
    2.57      Refute.refute_term @{context} params ts @{prop False}
    2.58      |> print_szs_from_outcome falsify
    2.59 @@ -210,7 +207,7 @@
    2.60  
    2.61  (** Sledgehammer **)
    2.62  
    2.63 -fun sledgehammer_tptp_file file_name = ()
    2.64 +fun sledgehammer_tptp_file timeout file_name = ()
    2.65  
    2.66  
    2.67  (** Translator between TPTP(-like) file formats **)
     3.1 --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle	Sun Apr 22 14:16:46 2012 +0200
     3.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle	Sun Apr 22 14:16:46 2012 +0200
     3.3 @@ -9,9 +9,10 @@
     3.4  
     3.5  function usage() {
     3.6    echo
     3.7 -  echo "Usage: isabelle $PRG FILES"
     3.8 +  echo "Usage: isabelle $PRG TIMEOUT FILES"
     3.9    echo
    3.10    echo "  Runs a combination of Isabelle tactics on TPTP problems."
    3.11 +  echo "  Each problem is allocated at most TIMEOUT seconds."
    3.12    echo
    3.13    exit 1
    3.14  }
    3.15 @@ -20,10 +21,13 @@
    3.16  
    3.17  SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    3.18  
    3.19 +TIMEOUT=$1
    3.20 +shift
    3.21 +
    3.22  for FILE in "$@"
    3.23  do
    3.24    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    3.25 -ML {* ATP_Problem_Import.isabelle_tptp_file \"$FILE\" *} end;" \
    3.26 +ML {* ATP_Problem_Import.isabelle_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
    3.27      > /tmp/$SCRATCH.thy
    3.28    "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    3.29  done
     4.1 --- a/src/HOL/TPTP/lib/Tools/tptp_nitpick	Sun Apr 22 14:16:46 2012 +0200
     4.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick	Sun Apr 22 14:16:46 2012 +0200
     4.3 @@ -9,9 +9,10 @@
     4.4  
     4.5  function usage() {
     4.6    echo
     4.7 -  echo "Usage: isabelle $PRG FILES"
     4.8 +  echo "Usage: isabelle $PRG TIMEOUT FILES"
     4.9    echo
    4.10    echo "  Runs Nitpick on TPTP problems."
    4.11 +  echo "  Each problem is allocated at most TIMEOUT seconds."
    4.12    echo
    4.13    exit 1
    4.14  }
    4.15 @@ -20,10 +21,13 @@
    4.16  
    4.17  SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    4.18  
    4.19 +TIMEOUT=$1
    4.20 +shift
    4.21 +
    4.22  for FILE in "$@"
    4.23  do
    4.24    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    4.25 -ML {* ATP_Problem_Import.nitpick_tptp_file \"$FILE\" *} end;" \
    4.26 +ML {* ATP_Problem_Import.nitpick_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
    4.27      > /tmp/$SCRATCH.thy
    4.28    "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    4.29  done
     5.1 --- a/src/HOL/TPTP/lib/Tools/tptp_refute	Sun Apr 22 14:16:46 2012 +0200
     5.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_refute	Sun Apr 22 14:16:46 2012 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  
     5.5  function usage() {
     5.6    echo
     5.7 -  echo "Usage: isabelle $PRG FILES"
     5.8 +  echo "Usage: isabelle $PRG TIMEOUT FILES"
     5.9    echo
    5.10    echo "  Runs Refute on TPTP problems."
    5.11    echo
    5.12 @@ -20,10 +20,13 @@
    5.13  
    5.14  SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    5.15  
    5.16 +TIMEOUT=$1
    5.17 +shift
    5.18 +
    5.19  for FILE in "$@"
    5.20  do
    5.21    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    5.22 -ML {* ATP_Problem_Import.refute_tptp_file \"$FILE\" *} end;" \
    5.23 +ML {* ATP_Problem_Import.refute_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
    5.24      > /tmp/$SCRATCH.thy
    5.25    "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    5.26  done
     6.1 --- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Sun Apr 22 14:16:46 2012 +0200
     6.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Sun Apr 22 14:16:46 2012 +0200
     6.3 @@ -9,9 +9,10 @@
     6.4  
     6.5  function usage() {
     6.6    echo
     6.7 -  echo "Usage: isabelle $PRG FILES"
     6.8 +  echo "Usage: isabelle $PRG TIMEOUT FILES"
     6.9    echo
    6.10    echo "  Runs Sledgehammer on TPTP problems."
    6.11 +  echo "  Each problem is allocated at most TIMEOUT seconds."
    6.12    echo
    6.13    exit 1
    6.14  }
    6.15 @@ -20,10 +21,13 @@
    6.16  
    6.17  SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    6.18  
    6.19 +TIMEOUT=$1
    6.20 +shift
    6.21 +
    6.22  for FILE in "$@"
    6.23  do
    6.24    echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    6.25 -ML {* ATP_Problem_Import.sledgehammer_tptp_file \"$FILE\" *} end;" \
    6.26 +ML {* ATP_Problem_Import.sledgehammer_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
    6.27      > /tmp/$SCRATCH.thy
    6.28    "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    6.29  done
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Apr 22 14:16:46 2012 +0200
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Apr 22 14:16:46 2012 +0200
     7.3 @@ -1048,7 +1048,10 @@
     7.4  
     7.5  fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
     7.6                        step subst assm_ts orig_t =
     7.7 -  let val print_nt = if is_mode_nt mode then Output.urgent_message else K () in
     7.8 +  let
     7.9 +    val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
    7.10 +    val print_t = if mode = TPTP then Output.urgent_message else K ()
    7.11 +  in
    7.12      if getenv "KODKODI" = "" then
    7.13        (* The "expect" argument is deliberately ignored if Kodkodi is missing so
    7.14           that the "Nitpick_Examples" can be processed on any machine. *)
    7.15 @@ -1064,14 +1067,18 @@
    7.16                (pick_them_nits_in_term deadline state params mode i n step subst
    7.17                                        assm_ts) orig_t
    7.18            handle TOO_LARGE (_, details) =>
    7.19 -                 (print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
    7.20 +                 (print_t "% SZS status Unknown";
    7.21 +                  print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
    7.22                 | TOO_SMALL (_, details) =>
    7.23 -                 (print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
    7.24 +                 (print_t "% SZS status Unknown";
    7.25 +                  print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
    7.26                 | Kodkod.SYNTAX (_, details) =>
    7.27 -                 (print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
    7.28 +                 (print_t "% SZS status Unknown";
    7.29 +                  print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
    7.30                    unknown_outcome)
    7.31                 | TimeLimit.TimeOut =>
    7.32 -                 (print_nt "Nitpick ran out of time."; unknown_outcome)
    7.33 +                 (print_t "% SZS status TimedOut";
    7.34 +                  print_nt "Nitpick ran out of time."; unknown_outcome)
    7.35        in
    7.36          if expect = "" orelse outcome_code = expect then outcome
    7.37          else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")