src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML

 *)
 (* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *)
 
 val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*)
 val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*)
-val force_sosK = "force_sos" (*=BOOL: use set-of-support (in Vampire)*)
 val keep_probsK = "keep_probs" (*=BOOL: keep temporary problem files created by sledgehammer*)
 val keep_proofsK = "keep_proofs" (*=BOOL: keep temporary proof files created by ATPs*)
 val proof_methodK = "proof_method" (*=STRING: how to reconstruct proofs (e.g. using metis)*)
 val term_orderK = "term_order" (*=STRING: term order (in E)*)
 

     else
       "smt")
 
 local
 
-fun run_sh params e_selection_heuristic term_order force_sos keep pos state =
+fun run_sh params e_selection_heuristic term_order keep pos state =
   let
     fun set_file_name (SOME (dir, keep_probs, keep_proofs)) =
         let
           val filename = "prob_" ^
             StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^

       |> Proof.map_context
            (set_file_name keep
             #> (Option.map (Config.put Sledgehammer_ATP_Systems.e_selection_heuristic)
                   e_selection_heuristic |> the_default I)
             #> (Option.map (Config.put Sledgehammer_ATP_Systems.term_order)
-                  term_order |> the_default I)
-            #> (Option.map (Config.put Sledgehammer_ATP_Systems.force_sos)
-                  force_sos |> the_default I))
+                  term_order |> the_default I))
 
     val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () =>
       Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1
         Sledgehammer_Fact.no_fact_override state') ()
   in

   | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0)
 
 in
 
 fun run_sledgehammer (params as {provers, ...}) output_dir e_selection_heuristic term_order
-  force_sos keep_probs keep_proofs proof_method_from_msg thy_index trivial pos st =
+  keep_probs keep_proofs proof_method_from_msg thy_index trivial pos st =
   let
     val thy = Proof.theory_of st
     val thy_name = Context.theory_name thy
     val triv_str = if trivial then "[T] " else ""
     val keep =

         end
       else
         NONE
     val prover_name = hd provers
     val (sledgehamer_outcome, msg, cpu_time) =
-      run_sh params e_selection_heuristic term_order force_sos keep pos st
+      run_sh params e_selection_heuristic term_order keep pos st
     val (time_prover, change_data, proof_method_and_used_thms) =
       (case sledgehamer_outcome of
         Sledgehammer.SH_Some {used_facts, run_time, ...} =>
         let
           val num_used_facts = length used_facts

       Mirabelle.get_bool_argument arguments (check_trivialK, check_trivial_default)
     val keep_probs = Mirabelle.get_bool_argument arguments (keep_probsK, keep_probs_default)
     val keep_proofs = Mirabelle.get_bool_argument arguments (keep_proofsK, keep_proofs_default)
     val e_selection_heuristic = AList.lookup (op =) arguments e_selection_heuristicK
     val term_order = AList.lookup (op =) arguments term_orderK
-    val force_sos = AList.lookup (op =) arguments force_sosK
-      |> Option.map (curry (op <>) "false")
     val proof_method_from_msg = proof_method_from_msg arguments
 
     (* Parse Sledgehammer parameters *)
     val params = Sledgehammer_Commands.default_params \<^theory> arguments
       |> (fn (params as {provers, ...}) =>

         else
           let
             val trivial = check_trivial andalso try0 pre handle Timeout.TIMEOUT _ => false
             val (outcome, log1, change_data1, proof_method_and_used_thms) =
               run_sledgehammer params output_dir e_selection_heuristic term_order
-                force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial pos pre
+                keep_probs keep_proofs proof_method_from_msg theory_index trivial pos pre
             val (log2, change_data2) =
               (case proof_method_and_used_thms of
                 SOME (proof_method, used_thms) =>
                 run_proof_method trivial false name proof_method used_thms timeout pos pre
                 |> apfst (prefix (proof_method ^ " (sledgehammer): "))