# HG changeset patch # User blanchet # Date 1409237907 -7200 # Node ID f050a297c9c30e599e2d5a9edc1a2b281f5e7400 # Parent fa0926e40759dfefc867cfd969fe223b1e029f86 try 'skolem' method first for Z3 diff -r fa0926e40759 -r f050a297c9c3 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 28 16:58:27 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 28 16:58:27 2014 +0200 @@ -137,7 +137,7 @@ basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods -val skolem_methods = basic_systematic_methods @ [Skolem_Method] +fun skolem_methods_of z3 = (basic_systematic_methods, [Skolem_Method]) |> z3 ? swap |> op @ fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = @@ -185,9 +185,12 @@ fun add_lemma ((l, t), rule) ctxt = let val (skos, meths) = - (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods) - else if is_arith_rule rule then ([], arith_methods) - else ([], rewrite_methods)) + (if is_skolemize_rule rule then + (skolems_of ctxt t, skolem_methods_of (rule = z3_skolemize_rule)) + else if is_arith_rule rule then + ([], arith_methods) + else + ([], rewrite_methods)) ||> massage_methods in (Prove ([], skos, l, t, [], ([], []), meths, ""), @@ -260,7 +263,7 @@ |> fold add_fact_of_dependencies gamma |> sort_facts val meths = - (if skolem then skolem_methods + (if skolem then skolem_methods_of (rule = z3_skolemize_rule) else if is_arith_rule rule then arith_methods else if is_datatype_rule rule then datatype_methods else systematic_methods')