use internal proof-producing SAT solver for more efficient SMT proof replay

--- a/src/HOL/Tools/SMT2/smt2_config.ML	Thu May 01 22:56:59 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_config.ML	Thu May 01 22:57:34 2014 +0200
@@ -34,6 +34,7 @@
   val infer_triggers: bool Config.T
   val filter_only_facts: bool Config.T
   val debug_files: string Config.T
+  val sat_solver: string Config.T
 
   (*tools*)
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
@@ -160,6 +161,7 @@
 val infer_triggers = Attrib.setup_config_bool @{binding smt2_infer_triggers} (K false)
 val filter_only_facts = Attrib.setup_config_bool @{binding smt2_filter_only_facts} (K false)
 val debug_files = Attrib.setup_config_string @{binding smt2_debug_files} (K "")
+val sat_solver = Attrib.setup_config_string @{binding smt2_sat_solver} (K "dpll_p")
 
 
 (* diagnostics *)

--- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu May 01 22:56:59 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Thu May 01 22:57:34 2014 +0200
@@ -182,7 +182,10 @@
       ((iidths, steps), TrueI)
     else
       let
-        val ctxt4 = put_simpset (Z3_New_Replay_Util.make_simpset ctxt3 []) ctxt3
+        val ctxt4 =
+          ctxt3
+          |> put_simpset (Z3_New_Replay_Util.make_simpset ctxt3 [])
+          |> Config.put SAT.solver (Config.get ctxt3 SMT2_Config.sat_solver)
         val proofs = fold (replay_step ctxt4 assumed) steps assumed
         val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps
         val thm = Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt4

--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu May 01 22:56:59 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Thu May 01 22:57:34 2014 +0200
@@ -62,7 +62,7 @@
 
 (* utility functions *)
 
-val trace = SMT2_Config.trace_msg
+fun trace ctxt f = SMT2_Config.trace_msg ctxt f ()
 
 fun pretty_thm ctxt thm = Syntax.pretty_term ctxt (Thm.concl_of thm)
 
@@ -137,7 +137,10 @@
 fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
 
 fun prop_tac ctxt prems =
-  Method.insert_tac prems THEN' (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt)
+  Method.insert_tac prems
+  THEN' SUBGOAL (fn (prop, i) =>
+    if Term.size_of_term prop > 100 then SAT.satx_tac ctxt i
+    else (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) i)
 
 fun quant_tac ctxt = Blast.blast_tac ctxt