removed SMT weights -- their impact was very inconclusive anyway
authorblanchet
Tue Jun 03 11:43:07 2014 +0200 (2014-06-03)
changeset 571657b1bf424ec5f
parent 57164 eb5f27ec3987
child 57166 5cfcc616d485
child 57167 d42a5c885cd5
removed SMT weights -- their impact was very inconclusive anyway
src/HOL/SMT2.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/Tools/SMT2/smt2_normalize.ML
src/HOL/Tools/SMT2/smt2_solver.ML
src/HOL/Tools/SMT2/smt2_translate.ML
src/HOL/Tools/SMT2/smtlib2_interface.ML
src/HOL/Tools/SMT2/z3_new_replay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
     1.1 --- a/src/HOL/SMT2.thy	Tue Jun 03 10:35:51 2014 +0200
     1.2 +++ b/src/HOL/SMT2.thy	Tue Jun 03 11:43:07 2014 +0200
     1.3 @@ -40,32 +40,6 @@
     1.4  definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P"
     1.5  
     1.6  
     1.7 -subsection {* Quantifier weights *}
     1.8 -
     1.9 -text {*
    1.10 -Weight annotations to quantifiers influence the priority of quantifier
    1.11 -instantiations.  They should be handled with care for solvers, which support
    1.12 -them, because incorrect choices of weights might render a problem unsolvable.
    1.13 -*}
    1.14 -
    1.15 -definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
    1.16 -
    1.17 -text {*
    1.18 -Weights must be nonnegative.  The value @{text 0} is equivalent to providing
    1.19 -no weight at all.
    1.20 -
    1.21 -Weights should only be used at quantifiers and only inside triggers (if the
    1.22 -quantifier has triggers).  Valid usages of weights are as follows:
    1.23 -
    1.24 -\begin{itemize}
    1.25 -\item
    1.26 -@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
    1.27 -\item
    1.28 -@{term "\<forall>x. weight 3 (P x)"}
    1.29 -\end{itemize}
    1.30 -*}
    1.31 -
    1.32 -
    1.33  subsection {* Higher-order encoding *}
    1.34  
    1.35  text {*
    1.36 @@ -430,6 +404,6 @@
    1.37  
    1.38  hide_type (open) pattern
    1.39  hide_const fun_app z3div z3mod
    1.40 -hide_const (open) trigger pat nopat weight
    1.41 +hide_const (open) trigger pat nopat
    1.42  
    1.43  end
     2.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Jun 03 10:35:51 2014 +0200
     2.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Jun 03 11:43:07 2014 +0200
     2.3 @@ -184,7 +184,7 @@
     2.4    by smt2+
     2.5  
     2.6  
     2.7 -section {* Guidance for quantifier heuristics: patterns and weights *}
     2.8 +section {* Guidance for quantifier heuristics: patterns *}
     2.9  
    2.10  lemma
    2.11    assumes "\<forall>x. SMT2.trigger [[SMT2.pat (f x)]] (f x = x)"
    2.12 @@ -216,18 +216,6 @@
    2.13    shows "R t"
    2.14    using assms by smt2
    2.15  
    2.16 -lemma
    2.17 -  assumes "ALL x. SMT2.trigger [[SMT2.pat (P x)]] (SMT2.weight 2 (P x --> Q x))"
    2.18 -  and "P t"
    2.19 -  shows "Q t"
    2.20 -  using assms by smt2
    2.21 -
    2.22 -lemma
    2.23 -  assumes "ALL x. SMT2.weight 1 (P x --> Q x)"
    2.24 -  and "P t"
    2.25 -  shows "Q t"
    2.26 -  using assms by smt2
    2.27 -
    2.28  
    2.29  section {* Meta-logical connectives *}
    2.30  
     3.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Tue Jun 03 10:35:51 2014 +0200
     3.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Tue Jun 03 11:43:07 2014 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4  
     3.5    type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
     3.6    val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
     3.7 -  val normalize: Proof.context -> (int option * thm) list -> (int * thm) list
     3.8 +  val normalize: Proof.context -> thm list -> (int * thm) list
     3.9  end
    3.10  
    3.11  structure SMT2_Normalize: SMT2_NORMALIZE =
    3.12 @@ -239,79 +239,25 @@
    3.13  end
    3.14  
    3.15  
    3.16 -(** adding quantifier weights **)
    3.17 -
    3.18 -local
    3.19 -  (*** check weight syntax ***)
    3.20 -
    3.21 -  val has_no_weight =
    3.22 -    not o Term.exists_subterm (fn @{const SMT2.weight} => true | _ => false)
    3.23 -
    3.24 -  fun is_weight (@{const SMT2.weight} $ w $ t) =
    3.25 -        (case try HOLogic.dest_number w of
    3.26 -          SOME (_, i) => i >= 0 andalso has_no_weight t
    3.27 -        | _ => false)
    3.28 -    | is_weight t = has_no_weight t
    3.29 -
    3.30 -  fun proper_trigger (@{const SMT2.trigger} $ _ $ t) = is_weight t
    3.31 -    | proper_trigger t = is_weight t 
    3.32 -
    3.33 -  fun check_weight_error ctxt t =
    3.34 -    error ("SMT weight must be a non-negative number and must only occur " ^
    3.35 -      "under the top-most quantifier and an optional trigger: " ^
    3.36 -      Syntax.string_of_term ctxt t)
    3.37 -
    3.38 -  fun check_weight_conv ctxt ct =
    3.39 -    if SMT2_Util.under_quant proper_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
    3.40 -    else check_weight_error ctxt (Thm.term_of ct)
    3.41 -
    3.42 -
    3.43 -  (*** insertion of weights ***)
    3.44 -
    3.45 -  fun under_trigger_conv cv ct =
    3.46 -    (case Thm.term_of ct of
    3.47 -      @{const SMT2.trigger} $ _ $ _ => Conv.arg_conv cv
    3.48 -    | _ => cv) ct
    3.49 -
    3.50 -  val weight_eq = mk_meta_eq @{lemma "p = SMT2.weight i p" by (simp add: weight_def)}
    3.51 -  fun mk_weight_eq w =
    3.52 -    let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq)
    3.53 -    in Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq end
    3.54 -
    3.55 -  fun add_weight_conv NONE _ = Conv.all_conv
    3.56 -    | add_weight_conv (SOME weight) ctxt =
    3.57 -        let val cv = Conv.rewr_conv (mk_weight_eq weight)
    3.58 -        in SMT2_Util.under_quant_conv (K (under_trigger_conv cv)) ctxt end
    3.59 -in
    3.60 -
    3.61 -fun weight_conv weight ctxt = 
    3.62 -  SMT2_Util.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
    3.63 -
    3.64 -val setup_weight = SMT2_Builtin.add_builtin_fun_ext'' @{const_name SMT2.weight}
    3.65 -
    3.66 -end
    3.67 -
    3.68 -
    3.69  (** combined general normalizations **)
    3.70  
    3.71 -fun gen_normalize1_conv ctxt weight =
    3.72 +fun gen_normalize1_conv ctxt =
    3.73    atomize_conv ctxt then_conv
    3.74    unfold_special_quants_conv ctxt then_conv
    3.75    Thm.beta_conversion true then_conv
    3.76 -  trigger_conv ctxt then_conv
    3.77 -  weight_conv weight ctxt
    3.78 +  trigger_conv ctxt
    3.79  
    3.80 -fun gen_normalize1 ctxt weight =
    3.81 +fun gen_normalize1 ctxt =
    3.82    instantiate_elim #>
    3.83    norm_def #>
    3.84    Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) #>
    3.85    Drule.forall_intr_vars #>
    3.86 -  Conv.fconv_rule (gen_normalize1_conv ctxt weight) #>
    3.87 +  Conv.fconv_rule (gen_normalize1_conv ctxt) #>
    3.88    (* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *)
    3.89    Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]}
    3.90  
    3.91 -fun gen_norm1_safe ctxt (i, (weight, thm)) =
    3.92 -  (case try (gen_normalize1 ctxt weight) thm of
    3.93 +fun gen_norm1_safe ctxt (i, thm) =
    3.94 +  (case try (gen_normalize1 ctxt) thm of
    3.95      SOME thm' => SOME (i, thm')
    3.96    | NONE => (drop_fact_warning ctxt thm; NONE))
    3.97  
    3.98 @@ -576,7 +522,6 @@
    3.99    setup_atomize #>
   3.100    setup_unfolded_quants #>
   3.101    setup_trigger #>
   3.102 -  setup_weight #>
   3.103    setup_case_bool #>
   3.104    setup_abs_min_max #>
   3.105    setup_nat_as_int))
     4.1 --- a/src/HOL/Tools/SMT2/smt2_solver.ML	Tue Jun 03 10:35:51 2014 +0200
     4.2 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Tue Jun 03 11:43:07 2014 +0200
     4.3 @@ -32,9 +32,8 @@
     4.4    val default_max_relevant: Proof.context -> string -> int
     4.5  
     4.6    (*filter*)
     4.7 -  val smt2_filter: Proof.context -> thm ->
     4.8 -    ((string * ATP_Problem_Generate.stature) * (int option * thm)) list -> int -> Time.time ->
     4.9 -    parsed_proof
    4.10 +  val smt2_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list ->
    4.11 +    int -> Time.time -> parsed_proof
    4.12  
    4.13    (*tactic*)
    4.14    val smt2_tac: Proof.context -> thm list -> int -> tactic
    4.15 @@ -235,17 +234,17 @@
    4.16  
    4.17  val default_max_relevant = #default_max_relevant oo get_info
    4.18  
    4.19 -fun apply_solver_and_replay ctxt wthms0 =
    4.20 +fun apply_solver_and_replay ctxt thms0 =
    4.21    let
    4.22 -    val wthms = map (apsnd (check_topsort ctxt)) wthms0
    4.23 +    val thms = map (check_topsort ctxt) thms0
    4.24      val (name, {command, replay, ...}) = name_and_info_of ctxt
    4.25 -    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt
    4.26 +    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt thms) ctxt
    4.27    in replay ctxt replay_data output end
    4.28  
    4.29  
    4.30  (* filter *)
    4.31  
    4.32 -fun smt2_filter ctxt0 goal xwfacts i time_limit =
    4.33 +fun smt2_filter ctxt0 goal xfacts i time_limit =
    4.34    let
    4.35      val ctxt = ctxt0 |> Config.put SMT2_Config.timeout (Time.toReal time_limit)
    4.36  
    4.37 @@ -256,15 +255,13 @@
    4.38          SOME ct => ct
    4.39        | NONE => raise SMT2_Failure.SMT (SMT2_Failure.Other_Failure "goal is not a HOL term"))
    4.40  
    4.41 -    val wconjecture = (NONE, Thm.assume cprop)
    4.42 -    val wprems = map (pair NONE) prems
    4.43 -    val wfacts = map snd xwfacts
    4.44 -    val xfacts = map (apsnd snd) xwfacts
    4.45 -    val wthms = wconjecture :: wprems @ wfacts
    4.46 -    val wthms' = map (apsnd (check_topsort ctxt)) wthms
    4.47 +    val conjecture = Thm.assume cprop
    4.48 +    val facts = map snd xfacts
    4.49 +    val thms = conjecture :: prems @ facts
    4.50 +    val thms' = map (check_topsort ctxt) thms
    4.51  
    4.52      val (name, {command, parse_proof, ...}) = name_and_info_of ctxt
    4.53 -    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms') ctxt
    4.54 +    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt thms') ctxt
    4.55    in
    4.56      parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output
    4.57    end
    4.58 @@ -277,7 +274,7 @@
    4.59    fun str_of ctxt fail =
    4.60      "Solver " ^ SMT2_Config.solver_of ctxt ^ ": " ^ SMT2_Failure.string_of_failure fail
    4.61  
    4.62 -  fun safe_solve ctxt wfacts = SOME (apply_solver_and_replay ctxt wfacts)
    4.63 +  fun safe_solve ctxt facts = SOME (apply_solver_and_replay ctxt facts)
    4.64      handle
    4.65        SMT2_Failure.SMT (fail as SMT2_Failure.Counterexample _) =>
    4.66          (SMT2_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
    4.67 @@ -293,8 +290,7 @@
    4.68    fun tac prove ctxt rules =
    4.69      CONVERSION (SMT2_Normalize.atomize_conv ctxt)
    4.70      THEN' rtac @{thm ccontr}
    4.71 -    THEN' SUBPROOF (fn {context = ctxt, prems, ...} =>
    4.72 -      resolve (prove ctxt (map (pair NONE) (rules @ prems)))) ctxt
    4.73 +    THEN' SUBPROOF (fn {context = ctxt, prems, ...} => resolve (prove ctxt (rules @ prems))) ctxt
    4.74  in
    4.75  
    4.76  val smt2_tac = tac safe_solve
     5.1 --- a/src/HOL/Tools/SMT2/smt2_translate.ML	Tue Jun 03 10:35:51 2014 +0200
     5.2 +++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Tue Jun 03 11:43:07 2014 +0200
     5.3 @@ -13,7 +13,7 @@
     5.4      SVar of int |
     5.5      SApp of string * sterm list |
     5.6      SLet of string * sterm * sterm |
     5.7 -    SQua of squant * string list * sterm spattern list * int option * sterm
     5.8 +    SQua of squant * string list * sterm spattern list * sterm
     5.9  
    5.10    (*translation configuration*)
    5.11    type sign = {
    5.12 @@ -51,7 +51,7 @@
    5.13    SVar of int |
    5.14    SApp of string * sterm list |
    5.15    SLet of string * sterm * sterm |
    5.16 -  SQua of squant * string list * sterm spattern list * int option * sterm
    5.17 +  SQua of squant * string list * sterm spattern list * sterm
    5.18  
    5.19  
    5.20  
    5.21 @@ -196,9 +196,8 @@
    5.22        | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
    5.23        | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t
    5.24        | expand (q as Const (@{const_name Ex}, T)) = exp2 T q
    5.25 -      | expand ((l as Const (@{const_name Let}, _)) $ t $ Abs a) = expand (Term.betapply (Abs a, t))
    5.26 -      | expand ((l as Const (@{const_name Let}, T)) $ t $ u) = expand (u $ t)
    5.27 -      | expand ((l as Const (@{const_name Let}, T)) $ t) =
    5.28 +      | expand (Const (@{const_name Let}, _) $ t $ u) = expand (Term.betapply (u, t))
    5.29 +      | expand (Const (@{const_name Let}, T) $ t) =
    5.30            let val U = Term.domain_type (Term.range_type T)
    5.31            in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end
    5.32        | expand (Const (@{const_name Let}, T)) =
    5.33 @@ -290,15 +289,13 @@
    5.34        | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
    5.35        | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
    5.36        | (u, ts) => traverses Ts u ts)
    5.37 -    and in_trigger Ts ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats Ts p $ in_weight Ts t
    5.38 -      | in_trigger Ts t = in_weight Ts t
    5.39 +    and in_trigger Ts ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats Ts p $ traverse Ts t
    5.40 +      | in_trigger Ts t = traverse Ts t
    5.41      and in_pats Ts ps =
    5.42        in_list @{typ "SMT2.pattern list"} (in_list @{typ SMT2.pattern} (in_pat Ts)) ps
    5.43      and in_pat Ts ((p as Const (@{const_name SMT2.pat}, _)) $ t) = p $ traverse Ts t
    5.44        | in_pat Ts ((p as Const (@{const_name SMT2.nopat}, _)) $ t) = p $ traverse Ts t
    5.45        | in_pat _ t = raise TERM ("bad pattern", [t])
    5.46 -    and in_weight Ts ((c as @{const SMT2.weight}) $ w $ t) = c $ w $ traverse Ts t
    5.47 -      | in_weight Ts t = traverse Ts t 
    5.48      and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
    5.49    in map (traverse []) ts end
    5.50  
    5.51 @@ -344,9 +341,6 @@
    5.52        | (Free c, ts) => Term.list_comb (Free c, map (in_term pat) ts)
    5.53        | _ => t)
    5.54  
    5.55 -    and in_weight ((c as @{const SMT2.weight}) $ w $ t) = c $ w $ in_form t
    5.56 -      | in_weight t = in_form t 
    5.57 -
    5.58      and in_pat ((p as Const (@{const_name SMT2.pat}, _)) $ t) =
    5.59            p $ in_term true t
    5.60        | in_pat ((p as Const (@{const_name SMT2.nopat}, _)) $ t) =
    5.61 @@ -356,8 +350,8 @@
    5.62      and in_pats ps =
    5.63        in_list @{typ "SMT2.pattern list"} (SOME o in_list @{typ SMT2.pattern} (try in_pat)) ps
    5.64  
    5.65 -    and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats p $ in_weight t
    5.66 -      | in_trigger t = in_weight t
    5.67 +    and in_trigger ((c as @{const SMT2.trigger}) $ p $ t) = c $ in_pats p $ in_form t
    5.68 +      | in_trigger t = in_form t
    5.69  
    5.70      and in_form t =
    5.71        (case Term.strip_comb t of
    5.72 @@ -393,9 +387,6 @@
    5.73        if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
    5.74    | group_quant _ Ts t = (Ts, t)
    5.75  
    5.76 -fun dest_weight (@{const SMT2.weight} $ w $ t) = (SOME (snd (HOLogic.dest_number w)), t)
    5.77 -  | dest_weight t = (NONE, t)
    5.78 -
    5.79  fun dest_pat (Const (@{const_name SMT2.pat}, _) $ t) = (t, true)
    5.80    | dest_pat (Const (@{const_name SMT2.nopat}, _) $ t) = (t, false)
    5.81    | dest_pat t = raise TERM ("bad pattern", [t])
    5.82 @@ -415,8 +406,7 @@
    5.83    let
    5.84      val (Ts, u) = group_quant qn [T] t
    5.85      val (ps, p) = dest_trigger u
    5.86 -    val (w, b) = dest_weight p
    5.87 -  in (q, rev Ts, ps, w, b) end)
    5.88 +  in (q, rev Ts, ps, p) end)
    5.89  
    5.90  fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
    5.91    | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
    5.92 @@ -439,9 +429,9 @@
    5.93        (case Term.strip_comb t of
    5.94          (Const (qn, _), [Abs (_, T, t1)]) =>
    5.95            (case dest_quant qn T t1 of
    5.96 -            SOME (q, Ts, ps, w, b) =>
    5.97 +            SOME (q, Ts, ps, b) =>
    5.98                fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
    5.99 -              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b'))
   5.100 +              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
   5.101            | NONE => raise TERM ("unsupported quantifier", [t]))
   5.102        | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
   5.103            transT T ##>> trans t1 ##>> trans t2 #>> (fn ((U, u1), u2) => SLet (U, u1, u2))
     6.1 --- a/src/HOL/Tools/SMT2/smtlib2_interface.ML	Tue Jun 03 10:35:51 2014 +0200
     6.2 +++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML	Tue Jun 03 11:43:07 2014 +0200
     6.3 @@ -89,7 +89,7 @@
     6.4        SMTLIB2.S (SMTLIB2.Sym n :: map (tree_of_sterm l) ts)
     6.5    | tree_of_sterm _ (SMT2_Translate.SLet _) =
     6.6        raise Fail "SMT-LIB: unsupported let expression"
     6.7 -  | tree_of_sterm l (SMT2_Translate.SQua (q, ss, pats, w, t)) =
     6.8 +  | tree_of_sterm l (SMT2_Translate.SQua (q, ss, pats, t)) =
     6.9        let
    6.10          val l' = l + length ss
    6.11  
    6.12 @@ -100,18 +100,15 @@
    6.13            [SMTLIB2.Key keyword, (case map (tree_of_sterm l') ps of [t] => t | ts => SMTLIB2.S ts)]
    6.14          fun trees_of_pat (SMT2_Translate.SPat ps) = gen_trees_of_pat "pattern" ps
    6.15            | trees_of_pat (SMT2_Translate.SNoPat ps) = gen_trees_of_pat "no-pattern" ps
    6.16 -        fun trees_of_weight NONE = []
    6.17 -          | trees_of_weight (SOME i) = [SMTLIB2.Key "weight", SMTLIB2.Num i]
    6.18 -        fun tree_of_pats_weight [] NONE t = t
    6.19 -          | tree_of_pats_weight pats w t =
    6.20 -            SMTLIB2.S (SMTLIB2.Sym "!" :: t :: maps trees_of_pat pats @ trees_of_weight w)
    6.21 +        fun tree_of_pats [] t = t
    6.22 +          | tree_of_pats pats t = SMTLIB2.S (SMTLIB2.Sym "!" :: t :: maps trees_of_pat pats)
    6.23  
    6.24          val vs = map_index (fn (i, ty) =>
    6.25            SMTLIB2.S [SMTLIB2.Sym (var (l + i)), SMTLIB2.Sym ty]) ss
    6.26  
    6.27          val body = t
    6.28            |> tree_of_sterm l'
    6.29 -          |> tree_of_pats_weight pats w
    6.30 +          |> tree_of_pats pats
    6.31        in
    6.32          SMTLIB2.S [SMTLIB2.Sym (quant_name q), SMTLIB2.S vs, body]
    6.33        end
     7.1 --- a/src/HOL/Tools/SMT2/z3_new_replay.ML	Tue Jun 03 10:35:51 2014 +0200
     7.2 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML	Tue Jun 03 11:43:07 2014 +0200
     7.3 @@ -72,14 +72,13 @@
     7.4  
     7.5  local
     7.6    val remove_trigger = mk_meta_eq @{thm SMT2.trigger_def}
     7.7 -  val remove_weight = mk_meta_eq @{thm SMT2.weight_def}
     7.8    val remove_fun_app = mk_meta_eq @{thm SMT2.fun_app_def}
     7.9  
    7.10    fun rewrite_conv _ [] = Conv.all_conv
    7.11      | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
    7.12  
    7.13 -  val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
    7.14 -    remove_fun_app, Z3_New_Replay_Literals.rewrite_true]
    7.15 +  val prep_rules = [@{thm Let_def}, remove_trigger, remove_fun_app,
    7.16 +    Z3_New_Replay_Literals.rewrite_true]
    7.17  
    7.18    fun rewrite _ [] = I
    7.19      | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Tue Jun 03 10:35:51 2014 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Tue Jun 03 11:43:07 2014 +0200
     8.3 @@ -14,12 +14,6 @@
     8.4  
     8.5    val smt2_builtins : bool Config.T
     8.6    val smt2_triggers : bool Config.T
     8.7 -  val smt2_weights : bool Config.T
     8.8 -  val smt2_weight_min_facts : int Config.T
     8.9 -  val smt2_min_weight : int Config.T
    8.10 -  val smt2_max_weight : int Config.T
    8.11 -  val smt2_max_weight_index : int Config.T
    8.12 -  val smt2_weight_curve : (int -> int) Unsynchronized.ref
    8.13    val smt2_max_slices : int Config.T
    8.14    val smt2_slice_fact_frac : real Config.T
    8.15    val smt2_slice_time_frac : real Config.T
    8.16 @@ -44,35 +38,9 @@
    8.17  
    8.18  val smt2_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt2_builtins} (K true)
    8.19  val smt2_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt2_triggers} (K true)
    8.20 -val smt2_weights = Attrib.setup_config_bool @{binding sledgehammer_smt2_weights} (K true)
    8.21 -val smt2_weight_min_facts =
    8.22 -  Attrib.setup_config_int @{binding sledgehammer_smt2_weight_min_facts} (K 20)
    8.23  
    8.24  val is_smt2_prover = member (op =) o SMT2_Config.available_solvers_of
    8.25  
    8.26 -(* FUDGE *)
    8.27 -val smt2_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_min_weight} (K 0)
    8.28 -val smt2_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight} (K 10)
    8.29 -val smt2_max_weight_index =
    8.30 -  Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight_index} (K 200)
    8.31 -val smt2_weight_curve = Unsynchronized.ref (fn x : int => x * x)
    8.32 -
    8.33 -fun smt2_fact_weight ctxt j num_facts =
    8.34 -  if Config.get ctxt smt2_weights andalso num_facts >= Config.get ctxt smt2_weight_min_facts then
    8.35 -    let
    8.36 -      val min = Config.get ctxt smt2_min_weight
    8.37 -      val max = Config.get ctxt smt2_max_weight
    8.38 -      val max_index = Config.get ctxt smt2_max_weight_index
    8.39 -      val curve = !smt2_weight_curve
    8.40 -    in
    8.41 -      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
    8.42 -    end
    8.43 -  else
    8.44 -    NONE
    8.45 -
    8.46 -fun weight_smt2_fact ctxt num_facts ((info, th), j) =
    8.47 -  (info, (smt2_fact_weight ctxt j num_facts, th))
    8.48 -
    8.49  (* "SMT2_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
    8.50     properly in the SMT module, we must interpret these here. *)
    8.51  val z3_failures =
    8.52 @@ -128,8 +96,7 @@
    8.53      val ctxt = Proof.context_of state
    8.54      val max_slices = if slice then Config.get ctxt smt2_max_slices else 1
    8.55  
    8.56 -    fun do_slice timeout slice outcome0 time_so_far
    8.57 -        (weighted_factss as (fact_filter, weighted_facts) :: _) =
    8.58 +    fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) =
    8.59        let
    8.60          val timer = Timer.startRealTimer ()
    8.61          val slice_timeout =
    8.62 @@ -141,7 +108,7 @@
    8.63              end
    8.64            else
    8.65              timeout
    8.66 -        val num_facts = length weighted_facts
    8.67 +        val num_facts = length facts
    8.68          val _ =
    8.69            if debug then
    8.70              quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
    8.71 @@ -152,7 +119,7 @@
    8.72          val birth = Timer.checkRealTimer timer
    8.73  
    8.74          val filter_result as {outcome, ...} =
    8.75 -          SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout
    8.76 +          SMT2_Solver.smt2_filter ctxt goal facts i slice_timeout
    8.77            handle exn =>
    8.78              if Exn.is_interrupt exn orelse debug then
    8.79                reraise exn
    8.80 @@ -179,8 +146,8 @@
    8.81            let
    8.82              val new_num_facts =
    8.83                Real.ceil (Config.get ctxt smt2_slice_fact_frac * Real.fromInt num_facts)
    8.84 -            val weighted_factss as (new_fact_filter, _) :: _ =
    8.85 -              weighted_factss
    8.86 +            val factss as (new_fact_filter, _) :: _ =
    8.87 +              factss
    8.88                |> (fn (x :: xs) => xs @ [x])
    8.89                |> app_hd (apsnd (take new_num_facts))
    8.90              val show_filter = fact_filter <> new_fact_filter
    8.91 @@ -200,11 +167,11 @@
    8.92                else
    8.93                  ()
    8.94            in
    8.95 -            do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
    8.96 +            do_slice timeout (slice + 1) outcome0 time_so_far factss
    8.97            end
    8.98          else
    8.99            {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result,
   8.100 -           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
   8.101 +           used_from = facts, run_time = time_so_far}
   8.102        end
   8.103    in
   8.104      do_slice timeout 1 NONE Time.zeroTime
   8.105 @@ -217,16 +184,8 @@
   8.106      val thy = Proof.theory_of state
   8.107      val ctxt = Proof.context_of state
   8.108  
   8.109 -    val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
   8.110 -
   8.111 -    fun weight_facts facts =
   8.112 -      let val num_facts = length facts in
   8.113 -        map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
   8.114 -      end
   8.115 -
   8.116 -    val weighted_factss = map (apsnd weight_facts) factss
   8.117      val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
   8.118 -      smt2_filter_loop name params state goal subgoal weighted_factss
   8.119 +      smt2_filter_loop name params state goal subgoal factss
   8.120      val used_named_facts = map snd fact_ids
   8.121      val used_facts = map fst used_named_facts
   8.122      val outcome = Option.map failure_of_smt2_failure outcome