# HG changeset patch
# User desharna
# Date 1632307300 -7200
# Node ID fb8ce60904375d5026ba30c6572363ef2f4dc097
# Parent  d8dbe7525ff1f1d9eac3921e26d7117cd4881fb2
removed checks for non-commercial usage of Vampire as it is now under BSD licence

diff -r d8dbe7525ff1 -r fb8ce6090437 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Sep 22 12:25:09 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Sep 22 12:41:40 2021 +0200
@@ -159,9 +159,7 @@
 \begin{enum}
 \item[\labelitemi] If you installed an official Isabelle package, it should
 already include properly set up executables for CVC4, E, SPASS, Vampire, veriT,
-and Z3, ready to use. To use Vampire, you must confirm that you are a
-noncommercial user, as indicated by the message that is displayed when
-Sledgehammer is invoked the first time.
+and Z3, ready to use.
 
 \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4, E,
 SPASS, Vampire, veriT, and Z3 binary packages from \download. Extract the
diff -r d8dbe7525ff1 -r fb8ce6090437 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Sep 22 12:25:09 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Sep 22 12:41:40 2021 +0200
@@ -45,7 +45,6 @@
   val spass_H2NuVS0 : string
   val spass_H2NuVS0Red2 : string
   val spass_H2SOS : string
-  val is_vampire_noncommercial_license_accepted : unit -> bool option
   val isabelle_scala_function: string list * string list
   val remote_atp : string -> string -> string list -> (string * string) list ->
     (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) ->
@@ -452,31 +451,6 @@
 
 (* Vampire *)
 
-fun is_vampire_noncommercial_license_accepted () =
-  let
-    val flag = Options.default_string \<^system_option>\<open>vampire_noncommercial\<close>
-      |> String.map Char.toLower
-  in
-    if flag = "yes" then
-      SOME true
-    else if flag = "no" then
-      SOME false
-    else
-      NONE
-  end
-
-fun check_vampire_noncommercial () =
-  (case is_vampire_noncommercial_license_accepted () of
-    SOME true => ()
-  | SOME false =>
-    error (Pretty.string_of (Pretty.para
-      "The Vampire prover may be used only for noncommercial applications"))
-  | NONE =>
-    error (Pretty.string_of (Pretty.para
-      "The Vampire prover is not activated; to activate it, set the Isabelle system option \
-      \\"vampire_noncommercial\" to \"yes\" (e.g. via the Isabelle/jEdit menu Plugin Options \
-      \/ Isabelle / General)")))
-
 val vampire_basic_options =
   "--proof tptp --output_axiom_names on" ^
   (if ML_System.platform_is_windows
@@ -492,10 +466,9 @@
   in
     {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
-       (check_vampire_noncommercial ();
-        [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
+       [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
          " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
-         |> sos = sosN ? prefix "--sos on "]),
+         |> sos = sosN ? prefix "--sos on "],
      proof_delims =
        [("=========== Refutation ==========",
          "======= End of refutation =======")] @
diff -r d8dbe7525ff1 -r fb8ce6090437 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Sep 22 12:25:09 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Sep 22 12:41:40 2021 +0200
@@ -177,9 +177,7 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value mode ctxt =
-  [cvc4N] @
-  (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @
-  [z3N, eN, spassN, veritN]
+  [cvc4N, vampireN, z3N, eN, spassN, veritN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))
diff -r d8dbe7525ff1 -r fb8ce6090437 src/HOL/Tools/etc/options
--- a/src/HOL/Tools/etc/options	Wed Sep 22 12:25:09 2021 +0200
+++ b/src/HOL/Tools/etc/options	Wed Sep 22 12:41:40 2021 +0200
@@ -32,9 +32,6 @@
 public option sledgehammer_timeout : int = 30
   -- "provers will be interrupted after this time (in seconds)"
 
-public option vampire_noncommercial : string = "unknown"
-  -- "status of Vampire activation for noncommercial use (yes, no, unknown)"
-
 public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
   -- "URL for SystemOnTPTP service"