src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
changeset 56128 c106ac2ff76d
parent 56104 fd6e132ee4fb
child 56132 64eeda68e693
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Mar 14 11:05:45 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Mar 14 11:15:46 2014 +0100
     1.3 @@ -161,7 +161,8 @@
     1.4                reraise exn
     1.5              else
     1.6                {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
     1.7 -               conjecture_id = ~1, helper_ids = [], fact_ids = [], z3_proof = []}
     1.8 +               rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
     1.9 +               z3_proof = []}
    1.10  
    1.11          val death = Timer.checkRealTimer timer
    1.12          val outcome0 = if is_none outcome0 then SOME outcome else outcome0
    1.13 @@ -226,8 +227,9 @@
    1.14        end
    1.15  
    1.16      val weighted_factss = map (apsnd weight_facts) factss
    1.17 -    val {outcome, filter_result = {conjecture_id, helper_ids, fact_ids, z3_proof, ...},
    1.18 -         used_from, run_time} = smt2_filter_loop name params state goal subgoal weighted_factss
    1.19 +    val {outcome, filter_result = {conjecture_id, rewrite_rules, helper_ids, fact_ids, z3_proof,
    1.20 +           ...}, used_from, run_time} =
    1.21 +      smt2_filter_loop name params state goal subgoal weighted_factss
    1.22      val used_named_facts = map snd fact_ids
    1.23      val used_facts = map fst used_named_facts
    1.24      val outcome = Option.map failure_of_smt2_failure outcome
    1.25 @@ -243,7 +245,8 @@
    1.26                val fact_ids =
    1.27                  map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
    1.28                  map (fn (id, ((name, _), _)) => (id, name)) fact_ids
    1.29 -              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy conjecture_id fact_ids z3_proof
    1.30 +              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy rewrite_rules conjecture_id
    1.31 +                fact_ids z3_proof
    1.32                val isar_params =
    1.33                  K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
    1.34                     minimize <> SOME false, atp_proof, goal)