src/HOL/TPTP/atp_problem_import.ML
author blanchet
Wed, 06 Jun 2012 10:35:05 +0200
changeset 48086 5b87cfc300f9
parent 48083 a4148c95134d
child 48143 0186df5074c8
permissions -rw-r--r--
add missing timeout multiplier
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
47565
762eb0dacaa6 remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents: 47562
diff changeset
    42
(* cf. "close_form" in "refute.ML" *)
762eb0dacaa6 remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents: 47562
diff changeset
    43
fun close_form t =
762eb0dacaa6 remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents: 47562
diff changeset
    44
  fold (fn ((s, i), T) => fn t' =>
762eb0dacaa6 remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents: 47562
diff changeset
    45
           Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
762eb0dacaa6 remove old TPTP CNF/FOF parser; always use Nik's new parser
blanchet
parents: 47562
diff changeset
    46
       (Term.add_vars t []) t
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    47
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
    48
fun read_tptp_file thy postproc file_name =
47644
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    49
  let
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    50
    fun has_role role (_, role', _, _) = (role' = role)
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
    51
    fun get_prop (_, _, P, _) =
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
    52
      P |> Logic.varify_global |> close_form |> postproc
47644
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    53
    val path =
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    54
      Path.explode file_name
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    55
      |> (fn path =>
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    56
             path |> not (Path.is_absolute path)
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    57
                     ? Path.append (Path.explode "$PWD"))
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
    58
    val ((_, _, problem), thy) =
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
    59
      TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    60
    val (conjs, defs_and_nondefs) =
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    61
      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
    62
              ||> List.partition (has_role TPTP_Syntax.Role_Definition)
47644
2d90e10f61f2 prepend PWD to relative paths
blanchet
parents: 47643
diff changeset
    63
  in
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    64
    (map get_prop conjs, pairself (map get_prop) defs_and_nondefs,
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
    65
     thy |> Theory.checkpoint |> Proof_Context.init_global)
47557
32f35b3d9e42 started integrating Nik's parser into TPTP command-line tools
blanchet
parents: 46325
diff changeset
    66
  end
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    67
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
    68
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    69
(** Nitpick (alias Nitrox) **)
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
    70
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    71
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
    72
  | aptrueprop f t = f t
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
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
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
    76
    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
    77
    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
    78
    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
    79
      defs |> map (ATP_Util.abs_extensionalize_term ctxt
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
    80
                   #> aptrueprop (open_form I))
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
    81
           |> 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
    82
                              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
    83
                              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
    84
    val nondefs = pseudo_defs @ nondefs
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
    85
    val state = Proof.init ctxt
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    86
    val params =
47557
32f35b3d9e42 started integrating Nik's parser into TPTP command-line tools
blanchet
parents: 46325
diff changeset
    87
      [("card", "1\<emdash>100"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    88
       ("box", "false"),
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    89
       ("max_threads", "1"),
47791
c17cc1380642 smaller batches, to play safe
blanchet
parents: 47788
diff changeset
    90
       ("batch_size", "5"),
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    91
       ("falsify", if null conjs then "false" else "true"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    92
       ("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
    93
       ("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
    94
       ("overlord", if overlord then "true" else "false"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    95
       ("show_consts", "true"),
47755
df437d1bf8db tweak TPTP Nitpick's output
blanchet
parents: 47718
diff changeset
    96
       ("format", "1"),
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
    97
       ("max_potential", "0"),
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    98
       ("timeout", string_of_int timeout),
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
    99
       ("tac_timeout", string_of_int ((timeout + 49) div 50))]
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
   100
      |> Nitpick_Isar.default_params thy
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   101
    val i = 1
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   102
    val n = 1
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   103
    val step = 0
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   104
    val subst = []
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   105
  in
47715
04400144c6fc handle TPTP definitions as definitions in Nitpick rather than as axioms
blanchet
parents: 47714
diff changeset
   106
    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
   107
        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
   108
    ()
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   109
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   110
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   111
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   112
(** Refute **)
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   113
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   114
fun refute_tptp_file thy timeout file_name =
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   115
  let
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   116
    fun print_szs_from_outcome falsify s =
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   117
      "% SZS status " ^
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   118
      (if s = "genuine" then
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   119
         if falsify then "CounterSatisfiable" else "Satisfiable"
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   120
       else
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   121
         "Unknown")
47788
blanchet
parents: 47785
diff changeset
   122
      |> 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
   123
    val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy I file_name
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   124
    val params =
47714
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
   125
      [("maxtime", string_of_int timeout),
d6683fe037b1 get rid of old parser, hopefully for good
blanchet
parents: 47670
diff changeset
   126
       ("maxvars", "100000")]
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   127
  in
47718
39229c760636 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels
blanchet
parents: 47715
diff changeset
   128
    Refute.refute_term ctxt params (defs @ nondefs)
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   129
        (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
   130
    |> print_szs_from_outcome (not (null conjs))
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   131
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   132
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   133
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   134
(** Sledgehammer and Isabelle (combination of provers) **)
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   135
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   136
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
   137
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   138
fun SOLVE_TIMEOUT seconds name tac st =
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   139
  let
47788
blanchet
parents: 47785
diff changeset
   140
    val _ = Output.urgent_message ("running " ^ name ^ " for " ^
blanchet
parents: 47785
diff changeset
   141
                                   string_of_int seconds ^ " s")
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   142
    val result =
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   143
      TimeLimit.timeLimit (Time.fromSeconds seconds)
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   144
        (fn () => SINGLE (SOLVE tac) st) ()
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   145
      handle TimeLimit.TimeOut => NONE
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   146
        | ERROR _ => NONE
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   147
  in
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   148
    case result of
47788
blanchet
parents: 47785
diff changeset
   149
      NONE => (Output.urgent_message ("FAILURE: " ^ name); Seq.empty)
blanchet
parents: 47785
diff changeset
   150
    | 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
   151
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   152
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   153
fun nitpick_finite_oracle_tac ctxt timeout i th =
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   154
  let
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   155
    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
   156
      | is_safe @{typ prop} = true
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   157
      | is_safe @{typ bool} = true
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   158
      | is_safe _ = false
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   159
    val conj = Thm.term_of (Thm.cprem_of th i)
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   160
  in
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   161
    if exists_type (not o is_safe) conj then
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   162
      Seq.empty
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   163
    else
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   164
      let
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   165
        val thy = Proof_Context.theory_of ctxt
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   166
        val state = Proof.init ctxt
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   167
        val params =
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   168
          [("box", "false"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   169
           ("max_threads", "1"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   170
           ("verbose", "true"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   171
           ("debug", if debug then "true" else "false"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   172
           ("overlord", if overlord then "true" else "false"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   173
           ("max_potential", "0"),
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   174
           ("timeout", string_of_int timeout)]
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   175
          |> Nitpick_Isar.default_params thy
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   176
        val i = 1
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   177
        val n = 1
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   178
        val step = 0
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   179
        val subst = []
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   180
        val (outcome, _) =
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   181
          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
   182
                                    [] [] conj
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   183
      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
   184
  end
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   185
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
fun atp_tac ctxt aggressivity override_params timeout 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
   187
  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
   188
    val 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
   189
      ctxt |> Config.put Sledgehammer_Provers.aggressive (aggressivity > 0)
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
  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
   191
    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
   192
        ([("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
   193
          ("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
   194
          ("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
   195
          ("timeout", string_of_int timeout)] @
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
         (if aggressivity > 0 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
   197
            [("type_enc",
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
              if aggressivity = 1 then "mono_native" else "poly_guards??"),
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
             ("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
   200
          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
   201
            []) @
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
   202
         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
   203
        {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
   204
         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
   205
  end
47765
18f37b7aa6a6 more work on CASC setup
blanchet
parents: 47755
diff changeset
   206
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   207
fun sledgehammer_tac demo ctxt timeout i =
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   208
  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
   209
    val frac = if demo then 16 else 12
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
   210
    fun slice mult aggressivity 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
   211
      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
   212
          (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
   213
           (if aggressivity > 0 then "(" ^ string_of_int aggressivity ^ ")"
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
            else ""))
48086
5b87cfc300f9 add missing timeout multiplier
blanchet
parents: 48083
diff changeset
   215
          (atp_tac ctxt aggressivity [] (mult * timeout div frac) prover i)
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   216
  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
   217
    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
   218
    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
   219
    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
   220
    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
   221
    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
   222
    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
   223
    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
   224
    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
   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
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
   227
         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
   228
         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
   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
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   238
fun auto_etc_tac ctxt timeout i =
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   239
  SOLVE_TIMEOUT (timeout div 20) "nitpick"
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   240
      (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
   241
  ORELSE SOLVE_TIMEOUT (timeout div 10) "simp"
47812
bb477988edb4 use Nitpick as an oracle for finite problems
blanchet
parents: 47811
diff changeset
   242
      (asm_full_simp_tac (simpset_of ctxt) i)
47788
blanchet
parents: 47785
diff changeset
   243
  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
   244
  ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   245
      (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
   246
       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
   247
  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
   248
  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
   249
  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
   250
  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
   251
  ORELSE SOLVE_TIMEOUT (timeout div 10) "force" (force_tac ctxt i)
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   252
  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
   253
  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
   254
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   255
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
   256
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   257
(* Isabelle's standard automatic tactics ("auto", etc.) are more eager to
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   258
   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
   259
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
   260
  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
   261
    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
   262
                   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
   263
                   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
   264
                 | 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
   265
  end
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   266
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
   267
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
   268
  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
   269
                      case conjs of conj :: _ => conj | [] => @{prop False})
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   270
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   271
fun print_szs_from_success conjs success =
47788
blanchet
parents: 47785
diff changeset
   272
  Output.urgent_message ("% SZS status " ^
blanchet
parents: 47785
diff changeset
   273
                         (if success then
blanchet
parents: 47785
diff changeset
   274
                            if null conjs then "Unsatisfiable" else "Theorem"
blanchet
parents: 47785
diff changeset
   275
                          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
   276
                            "Unknown"))
47765
18f37b7aa6a6 more work on CASC setup
blanchet
parents: 47755
diff changeset
   277
47794
4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug)
blanchet
parents: 47793
diff changeset
   278
fun sledgehammer_tptp_file thy timeout file_name =
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   279
  let
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   280
    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
   281
      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
   282
    val conj = make_conj assms conjs
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   283
  in
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   284
    can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   285
    |> print_szs_from_success conjs
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   286
  end
47766
9f7cdd5fff7c more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents: 47765
diff changeset
   287
48083
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
   288
fun generic_isabelle_tptp_file demo thy timeout file_name =
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   289
  let
47785
d27bb852c430 more tweaking of TPTP/CASC setup
blanchet
parents: 47776
diff changeset
   290
    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
   291
      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
   292
    val conj = make_conj assms conjs
48082
d7a6ad5d27bf don't use aggressive with HO ATP
blanchet
parents: 47991
diff changeset
   293
    val (last_hope_atp, last_hope_aggressive) =
d7a6ad5d27bf don't use aggressive with HO ATP
blanchet
parents: 47991
diff changeset
   294
      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
   295
  in
47811
1e8eb643540d add extensionality to first-order provers
blanchet
parents: 47794
diff changeset
   296
    (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
   297
     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
   298
     can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
d7a6ad5d27bf don't use aggressive with HO ATP
blanchet
parents: 47991
diff changeset
   299
         (atp_tac ctxt last_hope_aggressive [] timeout last_hope_atp 1)) conj)
47771
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   300
    |> print_szs_from_success conjs
ba321ce6f344 tuning; no need for relevance filter
blanchet
parents: 47766
diff changeset
   301
  end
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   302
48083
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
   303
val isabelle_tptp_file = generic_isabelle_tptp_file false
a4148c95134d renamed TPTP commands to agree with Sutcliffe's terminology
blanchet
parents: 48082
diff changeset
   304
val isabelle_hot_tptp_file = generic_isabelle_tptp_file true
47832
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   305
7df66b448c4a split into demo and competitive version
blanchet
parents: 47812
diff changeset
   306
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   307
(** Translator between TPTP(-like) file formats **)
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   308
46325
b170ab46513a implemented "tptp_refute" tool
blanchet
parents: 46324
diff changeset
   309
fun translate_tptp_file format in_file_name out_file_name = ()
46324
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   310
e4bccf5ec61e added problem importer
blanchet
parents:
diff changeset
   311
end;