src/HOL/TPTP/atp_problem_import.ML
author blanchet
Wed, 31 Oct 2012 11:23:21 +0100
changeset 49985 5b4b0e4e5205
parent 49983 33e18e9916a8
child 51552 c713c9505f68
permissions -rw-r--r--
moved Refute to "HOL/Library" to speed up building "Main" even more
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/TPTP/atp_problem_import.ML
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
47845
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    10
  val read_tptp_file :
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    11
    theory -> (term -> term) -> string
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    12
    -> term list * (term list * term 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
    13
  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
    14
  val refute_tptp_file : theory -> int -> string -> unit
47845
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    15
  val can_tac : Proof.context -> tactic -> term -> bool
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    16
  val SOLVE_TIMEOUT :  int -> string -> tactic -> tactic
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    17
  val atp_tac :
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
    18
    Proof.context -> int -> (string * string) list -> int -> string -> int
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
    19
    -> tactic
47845
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    20
  val smt_solver_tac : string -> Proof.context -> int -> tactic
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    21
  val freeze_problem_consts : theory -> term -> term
2a2bc13669bd export more symbols
blanchet
parents: 47832
diff changeset
    22
  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
    23
  val sledgehammer_tptp_file : theory -> int -> string -> unit
48083
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
    24
  val isabelle_tptp_file : theory -> int -> string -> unit
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
    25
  val isabelle_hot_tptp_file : theory -> int -> string -> unit
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    26
  val translate_tptp_file : string -> string -> string -> unit
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    27
end;
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    28
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    29
structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    30
struct
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    31
47643
e33c2be488fe reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents: 47565
diff changeset
    32
open ATP_Util
e33c2be488fe reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents: 47565
diff changeset
    33
open ATP_Problem
e33c2be488fe reintroduced old FOF and CNF parsers, to work around TPTP_Parser failures
blanchet
parents: 47565
diff changeset
    34
open ATP_Proof
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
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
    42
fun read_tptp_file thy postproc file_name =
47644
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    43
  let
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    44
    fun has_role role (_, role', _, _) = (role' = role)
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
    45
    fun get_prop (_, _, P, _) =
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
    46
      P |> Logic.varify_global |> close_form |> postproc
47644
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    47
    val path =
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    48
      Path.explode file_name
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    49
      |> (fn path =>
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    50
             path |> not (Path.is_absolute path)
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    51
                     ? Path.append (Path.explode "$PWD"))
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
    52
    val ((_, _, problem), thy) =
48829
6ed588c4f963 look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents: 48143
diff changeset
    53
      TPTP_Interpret.interpret_file true [Path.dir path, Path.explode "$TPTP"]
6ed588c4f963 look in current directory first before looking up includes in the TPTP directory, as required by Geoff
blanchet
parents: 48143
diff changeset
    54
                                    path [] [] thy
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    55
    val (conjs, defs_and_nondefs) =
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    56
      problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture)
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    57
              ||> List.partition (has_role TPTP_Syntax.Role_Definition)
47644
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    58
  in
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    59
    (map get_prop conjs, pairself (map get_prop) defs_and_nondefs,
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
    60
     thy |> Theory.checkpoint |> Proof_Context.init_global)
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
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    64
(** Nitpick (alias Nitrox) **)
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
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
    69
fun nitpick_tptp_file thy timeout file_name =
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    70
  let
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
    71
    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
    72
    val thy = Proof_Context.theory_of ctxt
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
    73
    val (defs, pseudo_defs) =
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
    74
      defs |> map (ATP_Util.abs_extensionalize_term ctxt
49985
5b4b0e4e5205 moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents: 49983
diff changeset
    75
                   #> aptrueprop (hol_open_form I))
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
    76
           |> List.partition (ATP_Util.is_legitimate_tptp_def
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
    77
                              o perhaps (try HOLogic.dest_Trueprop)
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
    78
                              o ATP_Util.unextensionalize_def)
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
    79
    val nondefs = pseudo_defs @ nondefs
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
    80
    val state = Proof.init ctxt
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    81
    val params =
47557
32f35b3d9e42 started integrating Nik's parser into TPTP command-line tools
blanchet
parents: 46325
diff changeset
    82
      [("card", "1\<emdash>100"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    83
       ("box", "false"),
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    84
       ("max_threads", "1"),
47791
c17cc1380642 smaller batches, to play safe
blanchet
parents: 47788
diff changeset
    85
       ("batch_size", "5"),
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    86
       ("falsify", if null conjs then "false" else "true"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    87
       ("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
    88
       ("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
    89
       ("overlord", if overlord then "true" else "false"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    90
       ("show_consts", "true"),
47755
df437d1bf8db tweak TPTP Nitpick's output
blanchet
parents: 47718
diff changeset
    91
       ("format", "1"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    92
       ("max_potential", "0"),
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    93
       ("timeout", string_of_int timeout),
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    94
       ("tac_timeout", string_of_int ((timeout + 49) div 50))]
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
    95
      |> Nitpick_Isar.default_params thy
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    96
    val i = 1
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    97
    val n = 1
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    98
    val step = 0
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    99
    val subst = []
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   100
  in
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47714
diff changeset
   101
    Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   102
        defs nondefs (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
   103
    ()
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   104
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   105
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   106
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   107
(** Refute **)
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   108
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   109
fun refute_tptp_file thy timeout file_name =
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   110
  let
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   111
    fun print_szs_from_outcome falsify s =
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   112
      "% SZS status " ^
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   113
      (if s = "genuine" then
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   114
         if falsify then "CounterSatisfiable" else "Satisfiable"
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   115
       else
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   116
         "Unknown")
47788
blanchet
parents: 47785
diff changeset
   117
      |> Output.urgent_message
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   118
    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   119
    val params =
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
   120
      [("maxtime", string_of_int timeout),
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
   121
       ("maxvars", "100000")]
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   122
  in
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
   123
    Refute.refute_term ctxt params (defs @ nondefs)
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   124
        (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
   125
    |> print_szs_from_outcome (not (null conjs))
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   126
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   127
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   128
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   129
(** Sledgehammer and Isabelle (combination of provers) **)
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   130
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   131
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
   132
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   133
fun SOLVE_TIMEOUT seconds name tac st =
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   134
  let
47788
blanchet
parents: 47785
diff changeset
   135
    val _ = Output.urgent_message ("running " ^ name ^ " for " ^
blanchet
parents: 47785
diff changeset
   136
                                   string_of_int seconds ^ " s")
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   137
    val result =
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   138
      TimeLimit.timeLimit (Time.fromSeconds seconds)
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   139
        (fn () => SINGLE (SOLVE tac) st) ()
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   140
      handle TimeLimit.TimeOut => NONE
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   141
        | ERROR _ => NONE
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   142
  in
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   143
    case result of
47788
blanchet
parents: 47785
diff changeset
   144
      NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty)
blanchet
parents: 47785
diff changeset
   145
    | 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
   146
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   147
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   148
fun nitpick_finite_oracle_tac ctxt timeout i th =
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   149
  let
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   150
    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
   151
      | is_safe @{typ prop} = true
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   152
      | is_safe @{typ bool} = true
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   153
      | is_safe _ = false
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   154
    val conj = Thm.term_of (Thm.cprem_of th i)
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   155
  in
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   156
    if exists_type (not o is_safe) conj then
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   157
      Seq.empty
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   158
    else
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   159
      let
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   160
        val thy = Proof_Context.theory_of ctxt
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   161
        val state = Proof.init ctxt
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   162
        val params =
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   163
          [("box", "false"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   164
           ("max_threads", "1"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   165
           ("verbose", "true"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   166
           ("debug", if debug then "true" else "false"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   167
           ("overlord", if overlord then "true" else "false"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   168
           ("max_potential", "0"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   169
           ("timeout", string_of_int timeout)]
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   170
          |> Nitpick_Isar.default_params thy
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   171
        val i = 1
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   172
        val n = 1
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   173
        val step = 0
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   174
        val subst = []
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   175
        val (outcome, _) =
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   176
          Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   177
                                    [] [] conj
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   178
      in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   179
  end
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   180
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   181
fun atp_tac ctxt completeness override_params timeout 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
   182
  let
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
   183
    val ctxt =
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   184
      ctxt |> Config.put Sledgehammer_Provers.completish (completeness > 0)
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
   185
  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
   186
    Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
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
   187
        ([("debug", if debug then "true" else "false"),
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
   188
          ("overlord", if overlord then "true" else "false"),
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
   189
          ("provers", prover),
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
   190
          ("timeout", string_of_int timeout)] @
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   191
         (if completeness > 0 then
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
   192
            [("type_enc",
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   193
              if completeness = 1 then "mono_native" else "poly_guards??"),
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
   194
             ("slicing", "false")]
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
          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
   196
            []) @
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
   197
         override_params)
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
   198
        {add = [(Facts.named (Thm.derivation_name ext), [])],
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
   199
         del = [], only = true}
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
   200
  end
47765
18f37b7aa6a6 more work on CASC setup
blanchet
parents: 47755
diff changeset
   201
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   202
fun sledgehammer_tac demo ctxt timeout i =
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   203
  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
   204
    val frac = if demo then 16 else 12
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   205
    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
   206
      SOLVE_TIMEOUT (mult * timeout div frac)
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
          (prover ^
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   208
           (if completeness > 0 then "(" ^ string_of_int completeness ^ ")"
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
   209
            else ""))
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   210
          (atp_tac ctxt completeness [] (mult * timeout div frac) prover i)
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   211
  in
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
   212
    slice 2 0 ATP_Systems.spassN
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
    ORELSE slice 2 0 ATP_Systems.vampireN
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
   214
    ORELSE slice 2 0 ATP_Systems.eN
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
   215
    ORELSE slice 2 0 ATP_Systems.z3_tptpN
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
   216
    ORELSE slice 1 1 ATP_Systems.spassN
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
   217
    ORELSE slice 1 2 ATP_Systems.eN
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
   218
    ORELSE slice 1 1 ATP_Systems.vampireN
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
   219
    ORELSE slice 1 2 ATP_Systems.vampireN
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
   220
    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
   221
      (if demo then
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
   222
         slice 2 0 ATP_Systems.satallaxN
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
   223
         ORELSE slice 2 0 ATP_Systems.leo2N
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
   224
       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
   225
         no_tac)
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   226
  end
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   227
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   228
fun smt_solver_tac solver ctxt =
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   229
  let
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   230
    val ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver solver)
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   231
  in SMT_Solver.smt_tac ctxt [] end
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   232
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   233
fun auto_etc_tac ctxt timeout i =
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   234
  SOLVE_TIMEOUT (timeout div 20) "nitpick"
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   235
      (nitpick_finite_oracle_tac ctxt (timeout div 20) i)
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
   236
  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   237
      (asm_full_simp_tac (simpset_of ctxt) i)
47788
blanchet
parents: 47785
diff changeset
   238
  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
   239
  ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   240
      (auto_tac ctxt
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
   241
       THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) ATP_Systems.spassN))
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
   242
  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
   243
  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
   244
  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
   245
  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
   246
  ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   247
  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
   248
  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
   249
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   250
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
   251
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   252
(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   253
   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
   254
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
   255
  let val is_problem_const = String.isPrefix (problem_const_prefix thy) in
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   256
    map_aterms (fn t as Const (s, T) =>
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   257
                   if is_problem_const s then Free (Long_Name.base_name s, T)
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   258
                   else t
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   259
                 | t => t)
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   260
  end
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   261
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
   262
fun make_conj (defs, nondefs) conjs =
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
  Logic.list_implies (rev defs @ rev nondefs,
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
   264
                      case conjs of conj :: _ => conj | [] => @{prop False})
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   265
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   266
fun print_szs_from_success conjs success =
47788
blanchet
parents: 47785
diff changeset
   267
  Output.urgent_message ("% SZS status " ^
blanchet
parents: 47785
diff changeset
   268
                         (if success then
blanchet
parents: 47785
diff changeset
   269
                            if null conjs then "Unsatisfiable" else "Theorem"
blanchet
parents: 47785
diff changeset
   270
                          else
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
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
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   275
    val (conjs, assms, ctxt) =
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   276
      read_tptp_file thy (freeze_problem_consts thy) file_name
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
   277
    val conj = make_conj assms conjs
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   278
  in
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   279
    can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   280
    |> print_szs_from_success conjs
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
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   285
    val (conjs, assms, ctxt) =
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   286
      read_tptp_file thy (freeze_problem_consts thy) file_name
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
   287
    val conj = make_conj assms conjs
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   288
    val (last_hope_atp, last_hope_completeness) =
48082
d7a6ad5d27bf don't use aggressive with HO ATP
blanchet
parents: 47991
diff changeset
   289
      if demo then (ATP_Systems.satallaxN, 0) else (ATP_Systems.vampireN, 2)
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   290
  in
47811
1e8eb643540d add extensionality to first-order provers
blanchet
parents: 47794
diff changeset
   291
    (can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   292
     can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
48082
d7a6ad5d27bf don't use aggressive with HO ATP
blanchet
parents: 47991
diff changeset
   293
     can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
48143
0186df5074c8 renamed experimental option
blanchet
parents: 48086
diff changeset
   294
         (atp_tac ctxt last_hope_completeness [] timeout last_hope_atp 1)) conj)
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   295
    |> print_szs_from_success conjs
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   296
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   297
48083
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
   298
val isabelle_tptp_file = generic_isabelle_tptp_file false
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
   299
val isabelle_hot_tptp_file = generic_isabelle_tptp_file true
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   300
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   301
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   302
(** Translator between TPTP(-like) file formats **)
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   303
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   304
fun translate_tptp_file format in_file_name out_file_name = ()
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   305
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   306
end;