src/HOL/TPTP/atp_problem_import.ML
author wenzelm
Sun, 05 Oct 2014 22:18:40 +0200
changeset 58550 f65911a725ba
parent 57812 8dc9dc241973
child 58843 521cea5fa777
permissions -rw-r--r--
more explicit syntax, to avoid misunderstanding of foo-bar as 3 separate arguments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55208
11dd3d1da83b compile
blanchet
parents: 55201
diff changeset
     1
(*  Title:      HOL/TPTP/atp_problem_import.ML
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
     3
    Copyright   2012
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
     4
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
     5
Import TPTP problems as Isabelle terms or goals.
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
     6
*)
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
     7
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
     8
signature ATP_PROBLEM_IMPORT =
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
     9
sig
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
    10
  val read_tptp_file : theory -> (string * term -> 'a) -> string ->
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
    11
    'a list * ('a list * 'a list) * Proof.context
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
    12
  val nitpick_tptp_file : theory -> int -> string -> unit
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
    13
  val refute_tptp_file : theory -> int -> string -> unit
47845
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    14
  val can_tac : Proof.context -> tactic -> term -> bool
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    15
  val SOLVE_TIMEOUT :  int -> string -> tactic -> tactic
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
    16
  val atp_tac : Proof.context -> int -> (string * string) list -> int -> term list -> string ->
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
    17
    int -> tactic
47845
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    18
  val smt_solver_tac : string -> Proof.context -> int -> tactic
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    19
  val freeze_problem_consts : theory -> term -> term
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    20
  val make_conj : term list * term list -> term list -> term
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
    21
  val sledgehammer_tptp_file : theory -> int -> string -> unit
48083
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
    22
  val isabelle_tptp_file : theory -> int -> string -> unit
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
    23
  val isabelle_hot_tptp_file : theory -> int -> string -> unit
54472
073f041d83ae send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents: 54434
diff changeset
    24
  val translate_tptp_file : theory -> string -> string -> unit
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    25
end;
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    26
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    27
structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    28
struct
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    29
47643
e33c2be488fe reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents: 47565
diff changeset
    30
open ATP_Util
e33c2be488fe reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents: 47565
diff changeset
    31
open ATP_Problem
e33c2be488fe reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents: 47565
diff changeset
    32
open ATP_Proof
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
    33
open ATP_Problem_Generate
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
    34
open ATP_Systems
47643
e33c2be488fe reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents: 47565
diff changeset
    35
47776
024cf0f7fb6d further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents: 47771
diff changeset
    36
val debug = false
024cf0f7fb6d further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents: 47771
diff changeset
    37
val overlord = false
024cf0f7fb6d further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents: 47771
diff changeset
    38
47643
e33c2be488fe reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents: 47565
diff changeset
    39
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
    40
(** TPTP parsing **)
47643
e33c2be488fe reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents: 47565
diff changeset
    41
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
    42
fun exploded_absolute_path file_name =
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
    43
  Path.explode file_name
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
    44
  |> (fn path => path |> not (Path.is_absolute path) ? Path.append (Path.explode "$PWD"))
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
    45
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
    46
fun read_tptp_file thy postproc file_name =
47644
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    47
  let
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    48
    fun has_role role (_, role', _, _) = (role' = role)
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    49
    fun get_prop f (name, _, P, _) = P |> f |> close_form |> pair name |> postproc
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    50
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
    51
    val path = exploded_absolute_path file_name
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
    52
    val ((_, _, problem), thy) =
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    53
      TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"] path [] [] thy
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    54
    val (conjs, defs_and_nondefs) = problem
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    55
      |> List.partition (has_role TPTP_Syntax.Role_Conjecture)
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    56
      ||> List.partition (has_role TPTP_Syntax.Role_Definition)
47644
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    57
  in
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    58
    (map (get_prop I) conjs,
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    59
     pairself (map (get_prop Logic.varify_global)) defs_and_nondefs,
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
    60
     Named_Target.theory_init thy)
47557
32f35b3d9e42 started integrating Nik's parser into TPTP command-line tools
blanchet
parents: 46325
diff changeset
    61
  end
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    62
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
    63
57547
677b07d777c3 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents: 57268
diff changeset
    64
(** Nitpick **)
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    65
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    66
fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    67
  | aptrueprop f t = f t
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    68
57547
677b07d777c3 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents: 57268
diff changeset
    69
fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t
677b07d777c3 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents: 57268
diff changeset
    70
  | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
677b07d777c3 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents: 57268
diff changeset
    71
    (is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u)
677b07d777c3 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents: 57268
diff changeset
    72
  | is_legitimate_tptp_def _ = false
677b07d777c3 don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
blanchet
parents: 57268
diff changeset
    73
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
    74
fun nitpick_tptp_file thy timeout file_name =
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    75
  let
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
    76
    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
    77
    val thy = Proof_Context.theory_of ctxt
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    78
    val (defs, pseudo_defs) = defs
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    79
      |> map (ATP_Util.abs_extensionalize_term ctxt #> aptrueprop (hol_open_form I))
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    80
      |> List.partition (is_legitimate_tptp_def o perhaps (try HOLogic.dest_Trueprop)
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
    81
        o ATP_Util.unextensionalize_def)
47991
3eb598b044ad make Nitpick's handling of definitions more robust in the face of formulas that don't have the expected format (needed for soundness, cf. RNG100+1)
blanchet
parents: 47957
diff changeset
    82
    val nondefs = pseudo_defs @ nondefs
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
    83
    val state = Proof.init ctxt
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    84
    val params =
47557
32f35b3d9e42 started integrating Nik's parser into TPTP command-line tools
blanchet
parents: 46325
diff changeset
    85
      [("card", "1\<emdash>100"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    86
       ("box", "false"),
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    87
       ("max_threads", "1"),
47791
c17cc1380642 smaller batches, to play safe
blanchet
parents: 47788
diff changeset
    88
       ("batch_size", "5"),
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    89
       ("falsify", if null conjs then "false" else "true"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    90
       ("verbose", "true"),
47776
024cf0f7fb6d further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents: 47771
diff changeset
    91
       ("debug", if debug then "true" else "false"),
024cf0f7fb6d further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents: 47771
diff changeset
    92
       ("overlord", if overlord then "true" else "false"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    93
       ("show_consts", "true"),
47755
df437d1bf8db tweak TPTP Nitpick's output
blanchet
parents: 47718
diff changeset
    94
       ("format", "1"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    95
       ("max_potential", "0"),
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    96
       ("timeout", string_of_int timeout),
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    97
       ("tac_timeout", string_of_int ((timeout + 49) div 50))]
55199
ba93ef2c0d27 tuned ML file name
blanchet
parents: 54547
diff changeset
    98
      |> Nitpick_Commands.default_params thy
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    99
    val i = 1
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   100
    val n = 1
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   101
    val step = 0
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   102
    val subst = []
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   103
  in
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   104
    Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst defs nondefs
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   105
      (case conjs of conj :: _ => conj | [] => @{prop True});
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
   106
    ()
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   107
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   108
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   109
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   110
(** Refute **)
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   111
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   112
fun refute_tptp_file thy timeout file_name =
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   113
  let
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51717
diff changeset
   114
    fun print_szs_of_outcome falsify s =
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   115
      "% SZS status " ^
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   116
      (if s = "genuine" then
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   117
         if falsify then "CounterSatisfiable" else "Satisfiable"
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   118
       else
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   119
         "Unknown")
47788
blanchet
parents: 47785
diff changeset
   120
      |> Output.urgent_message
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   121
    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   122
    val params =
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
   123
      [("maxtime", string_of_int timeout),
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
   124
       ("maxvars", "100000")]
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   125
  in
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
   126
    Refute.refute_term ctxt params (defs @ nondefs)
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   127
      (case conjs of conj :: _ => conj | [] => @{prop True})
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51717
diff changeset
   128
    |> print_szs_of_outcome (not (null conjs))
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   129
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   130
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   131
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   132
(** Sledgehammer and Isabelle (combination of provers) **)
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   133
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   134
fun can_tac ctxt tactic conj = can (Goal.prove ctxt [] [] conj) (K tactic)
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   135
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   136
fun SOLVE_TIMEOUT seconds name tac st =
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   137
  let
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   138
    val _ = Output.urgent_message ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   139
    val result =
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   140
      TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   141
      handle
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   142
        TimeLimit.TimeOut => NONE
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   143
      | ERROR _ => NONE
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   144
  in
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   145
    (case result of
47788
blanchet
parents: 47785
diff changeset
   146
      NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty)
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   147
    | SOME st' => (Output.urgent_message ("SUCCESS: " ^ name); Seq.single st'))
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   148
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   149
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   150
fun nitpick_finite_oracle_tac ctxt timeout i th =
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   151
  let
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   152
    fun is_safe (Type (@{type_name fun}, Ts)) = forall is_safe Ts
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   153
      | is_safe @{typ prop} = true
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   154
      | is_safe @{typ bool} = true
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   155
      | is_safe _ = false
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   156
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   157
    val conj = Thm.term_of (Thm.cprem_of th i)
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   158
  in
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   159
    if exists_type (not o is_safe) conj then
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   160
      Seq.empty
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   161
    else
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   162
      let
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   163
        val thy = Proof_Context.theory_of ctxt
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   164
        val state = Proof.init ctxt
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   165
        val params =
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   166
          [("box", "false"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   167
           ("max_threads", "1"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   168
           ("verbose", "true"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   169
           ("debug", if debug then "true" else "false"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   170
           ("overlord", if overlord then "true" else "false"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   171
           ("max_potential", "0"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   172
           ("timeout", string_of_int timeout)]
55199
ba93ef2c0d27 tuned ML file name
blanchet
parents: 54547
diff changeset
   173
          |> Nitpick_Commands.default_params thy
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   174
        val i = 1
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   175
        val n = 1
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   176
        val step = 0
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   177
        val subst = []
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   178
        val (outcome, _) =
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   179
          Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst [] [] conj
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   180
      in
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   181
        if outcome = "none" then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   182
      end
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   183
  end
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   184
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   185
fun atp_tac ctxt completeness override_params timeout assms prover =
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   186
  let
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   187
    val thy = Proof_Context.theory_of ctxt
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   188
    val assm_ths0 = map (Skip_Proof.make_thm thy) assms
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   189
    val ((assm_name, _), ctxt) = ctxt
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   190
      |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   191
      |> Local_Theory.note ((@{binding thms}, []), assm_ths0)
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   192
52071
0e70511cbba9 made "completish" mode a bit more complete
blanchet
parents: 52031
diff changeset
   193
    fun ref_of th = (Facts.named (Thm.derivation_name th), [])
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   194
    val ref_of_assms = (Facts.named assm_name, [])
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   195
  in
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   196
    Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   197
      ([("debug", if debug then "true" else "false"),
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   198
        ("overlord", if overlord then "true" else "false"),
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   199
        ("provers", prover),
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   200
        ("timeout", string_of_int timeout)] @
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   201
       (if completeness > 0 then
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   202
          [("type_enc", if completeness = 1 then "mono_native" else "poly_tags")]
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   203
        else
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   204
          []) @
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   205
       override_params)
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   206
      {add = ref_of_assms :: map ref_of [ext, @{thm someI}], del = [], only = true} []
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   207
  end
47765
18f37b7aa6a6 more work on CASC setup
blanchet
parents: 47755
diff changeset
   208
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   209
fun sledgehammer_tac demo ctxt timeout assms i =
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   210
  let
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   211
    val frac = if demo then 16 else 12
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   212
    fun slice mult completeness prover =
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   213
      SOLVE_TIMEOUT (mult * timeout div frac)
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   214
        (prover ^ (if completeness > 0 then "(" ^ string_of_int completeness ^ ")" else ""))
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   215
        (atp_tac ctxt completeness [] (mult * timeout div frac) assms prover i)
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   216
  in
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   217
    slice 2 0 ATP_Proof.spassN
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   218
    ORELSE slice 2 0 ATP_Proof.vampireN
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   219
    ORELSE slice 2 0 ATP_Proof.eN
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   220
    ORELSE slice 2 0 ATP_Proof.z3_tptpN
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   221
    ORELSE slice 1 1 ATP_Proof.spassN
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   222
    ORELSE slice 1 2 ATP_Proof.eN
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   223
    ORELSE slice 1 1 ATP_Proof.vampireN
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   224
    ORELSE slice 1 2 ATP_Proof.vampireN
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   225
    ORELSE
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   226
      (if demo then
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   227
         slice 2 0 ATP_Proof.satallaxN
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   228
         ORELSE slice 2 0 ATP_Proof.leo2N
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   229
       else
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   230
         no_tac)
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   231
  end
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   232
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   233
fun smt_solver_tac solver ctxt =
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   234
  let
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   235
    val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   236
  in SMT_Solver.smt_tac ctxt [] end
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   237
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   238
fun auto_etc_tac ctxt timeout assms i =
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   239
  SOLVE_TIMEOUT (timeout div 20) "nitpick" (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   240
  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp" (asm_full_simp_tac ctxt i)
47788
blanchet
parents: 47785
diff changeset
   241
  ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   242
  ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   243
    (auto_tac ctxt THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) assms ATP_Proof.spassN))
47946
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   244
  ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   245
  ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
33afcfad3f8d add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
blanchet
parents: 47845
diff changeset
   246
  ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i)
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   247
  ORELSE SOLVE_TIMEOUT (timeout div 20) "best" (best_tac ctxt i)
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   248
  ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   249
  ORELSE SOLVE_TIMEOUT (timeout div 10) "meson" (Meson.meson_tac ctxt [] i)
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   250
  ORELSE SOLVE_TIMEOUT (timeout div 10) "fastforce" (fast_force_tac ctxt i)
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   251
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   252
fun problem_const_prefix thy = Context.theory_name thy ^ Long_Name.separator
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   253
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   254
(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   255
   unfold "definitions" of free variables than of constants (cf. PUZ107^5). *)
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   256
fun freeze_problem_consts thy =
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   257
  let val is_problem_const = String.isPrefix (problem_const_prefix thy) in
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   258
    map_aterms
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   259
      (fn t as Const (s, T) => if is_problem_const s then Free (Long_Name.base_name s, T) else t
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   260
        | t => t)
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   261
  end
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   262
47776
024cf0f7fb6d further tweaking for Satallax, so that TPTP problems before parsing and after generation are as similar as possible/practical
blanchet
parents: 47771
diff changeset
   263
fun make_conj (defs, nondefs) conjs =
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   264
  Logic.list_implies (rev defs @ rev nondefs, case conjs of conj :: _ => conj | [] => @{prop False})
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   265
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51717
diff changeset
   266
fun print_szs_of_success conjs success =
47788
blanchet
parents: 47785
diff changeset
   267
  Output.urgent_message ("% SZS status " ^
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   268
    (if success then
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   269
       if null conjs then "Unsatisfiable" else "Theorem"
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   270
     else
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   271
       "Unknown"))
47765
18f37b7aa6a6 more work on CASC setup
blanchet
parents: 47755
diff changeset
   272
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   273
fun sledgehammer_tptp_file thy timeout file_name =
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   274
  let
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   275
    val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   276
    val conj = make_conj ([], []) conjs
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   277
    val assms = op @ assms
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   278
  in
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   279
    can_tac ctxt (sledgehammer_tac true ctxt timeout assms 1) conj
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51717
diff changeset
   280
    |> print_szs_of_success conjs
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   281
  end
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   282
48083
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
   283
fun generic_isabelle_tptp_file demo thy timeout file_name =
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   284
  let
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   285
    val (conjs, assms, ctxt) = read_tptp_file thy (freeze_problem_consts thy o snd) file_name
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   286
    val conj = make_conj ([], []) conjs
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   287
    val full_conj = make_conj assms conjs
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   288
    val assms = op @ assms
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   289
    val (last_hope_atp, last_hope_completeness) =
57154
f0eff6393a32 basic setup for zipperposition prover
fleury
parents: 55212
diff changeset
   290
      if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   291
  in
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   292
    (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) assms 1) full_conj orelse
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   293
     can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) assms 1) conj orelse
48082
d7a6ad5d27bf don't use aggressive with HO ATP
blanchet
parents: 47991
diff changeset
   294
     can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
57812
8dc9dc241973 make TPTP tools work on polymorphic (TFF1) problems as well
blanchet
parents: 57809
diff changeset
   295
       (atp_tac ctxt last_hope_completeness [] timeout assms last_hope_atp 1)) full_conj)
52031
9a9238342963 tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents: 51717
diff changeset
   296
    |> print_szs_of_success conjs
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   297
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   298
48083
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
   299
val isabelle_tptp_file = generic_isabelle_tptp_file false
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
   300
val isabelle_hot_tptp_file = generic_isabelle_tptp_file true
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   301
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   302
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   303
(** Translator between TPTP(-like) file formats **)
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   304
54472
073f041d83ae send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents: 54434
diff changeset
   305
fun translate_tptp_file thy format_str file_name =
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   306
  let
54472
073f041d83ae send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents: 54434
diff changeset
   307
    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   308
    val conj = make_conj ([], []) (map snd conjs)
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   309
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   310
    val (format, type_enc, lam_trans) =
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   311
      (case format_str of
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   312
        "FOF" => (FOF, "mono_guards??", liftingN)
54547
c999e2533487 renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy
blanchet
parents: 54472
diff changeset
   313
      | "TF0" => (TFF Monomorphic, "mono_native", liftingN)
c999e2533487 renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy
blanchet
parents: 54472
diff changeset
   314
      | "TH0" => (THF (Monomorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN)
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   315
      | "DFG" => (DFG Monomorphic, "mono_native", liftingN)
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   316
      | _ => error ("Unknown format " ^ quote format_str ^
54547
c999e2533487 renamed TFF0/THF0 to three-letter acronyms, in keeping with new TPTP policy
blanchet
parents: 54472
diff changeset
   317
        " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   318
    val uncurried_aliases = false
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   319
    val readable_names = true
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   320
    val presimp = true
57809
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   321
    val facts =
a7345fae237b treat variables as frees in 'conjecture's
blanchet
parents: 57547
diff changeset
   322
      map (apfst (rpair (Global, Non_Rec_Def))) defs @
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   323
      map (apfst (rpair (Global, General))) nondefs
57268
027feff882c4 compile
blanchet
parents: 57154
diff changeset
   324
    val (atp_problem, _, _, _) =
027feff882c4 compile
blanchet
parents: 57154
diff changeset
   325
      generate_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   326
        lam_trans uncurried_aliases readable_names presimp [] conj facts
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   327
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   328
    val ord = effective_term_order ctxt spassN
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   329
    val ord_info = K []
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   330
    val lines = lines_of_atp_problem format ord ord_info atp_problem
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   331
  in
54472
073f041d83ae send output of "tptp_translate" to standard output, to simplify Geoff Sutcliffe's life
blanchet
parents: 54434
diff changeset
   332
    List.app Output.physical_stdout lines
54434
e275d520f49d implemented 'tptp_translate'
blanchet
parents: 52788
diff changeset
   333
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   334
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   335
end;