# HG changeset patch # User boehmes # Date 1398977854 -7200 # Node ID 2f3756ccba41bada37a2bf246072c99de4147bd7 # Parent 848d507584db59f3b39af6aa56e964dccdd1da68 use internal proof-producing SAT solver for more efficient SMT proof replay diff -r 848d507584db -r 2f3756ccba41 src/HOL/Tools/SMT2/smt2_config.ML --- 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 *) diff -r 848d507584db -r 2f3756ccba41 src/HOL/Tools/SMT2/z3_new_replay.ML --- 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 diff -r 848d507584db -r 2f3756ccba41 src/HOL/Tools/SMT2/z3_new_replay_methods.ML --- 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