# HG changeset patch
# User blanchet
# Date 1312873679 -7200
# Node ID 10287833549fcb228f3f51e817eee6b1aa1dcf02
# Parent  3693baa6befb61073a58f26796474d2cf31debe6
added "sound" option to Mirabelle

diff -r 3693baa6befb -r 10287833549f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 09 09:05:22 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 09 09:07:59 2011 +0200
@@ -9,6 +9,7 @@
 val prover_timeoutK = "prover_timeout"
 val keepK = "keep"
 val type_encK = "type_enc"
+val soundK = "sound"
 val slicingK = "slicing"
 val lambda_translationK = "lambda_translation"
 val e_weight_methodK = "e_weight_method"
@@ -354,9 +355,9 @@
   SH_FAIL of int * int |
   SH_ERROR
 
-fun run_sh prover_name prover type_enc max_relevant slicing lambda_translation
-      e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout dir
-      st =
+fun run_sh prover_name prover type_enc sound max_relevant slicing
+        lambda_translation e_weight_method spass_force_sos vampire_force_sos
+        hard_timeout timeout dir st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
@@ -383,6 +384,7 @@
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
            ("type_enc", type_enc),
+           ("sound", sound),
            ("max_relevant", max_relevant),
            ("slicing", slicing),
            ("timeout", string_of_int timeout)]
@@ -458,6 +460,7 @@
     val _ = if trivial then () else change_data id inc_sh_nontriv_calls
     val (prover_name, prover) = get_prover (Proof.context_of st) args
     val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
+    val sound = AList.lookup (op =) args soundK |> the_default "false"
     val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
     val slicing = AList.lookup (op =) args slicingK |> the_default "true"
     val lambda_translation = AList.lookup (op =) args lambda_translationK
@@ -472,9 +475,9 @@
        minimizer has a chance to do its magic *)
     val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
-      run_sh prover_name prover type_enc max_relevant slicing lambda_translation
-        e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout
-        dir st
+      run_sh prover_name prover type_enc sound max_relevant slicing
+        lambda_translation e_weight_method spass_force_sos vampire_force_sos
+        hard_timeout timeout dir st
   in
     case result of
       SH_OK (time_isa, time_prover, names) =>
@@ -511,6 +514,7 @@
     val n0 = length (these (!named_thms))
     val (prover_name, _) = get_prover ctxt args
     val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
+    val sound = AList.lookup (op =) args soundK |> the_default "false"
     val timeout =
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
@@ -519,6 +523,7 @@
       [("provers", prover_name),
        ("verbose", "true"),
        ("type_enc", type_enc),
+       ("sound", sound),
        ("timeout", string_of_int timeout)]
     val minimize =
       Sledgehammer_Minimize.minimize_facts prover_name params