added support for quantifier weight annotations
authorboehmes
Mon Nov 22 23:37:00 2010 +0100 (2010-11-22)
changeset 40664e023788a91a1
parent 40663 e080c9e68752
child 40665 1a65f0c74827
added support for quantifier weight annotations
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_builtin.ML
src/HOL/Tools/SMT/smt_translate.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
     1.1 --- a/src/HOL/SMT.thy	Mon Nov 22 15:45:43 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Nov 22 23:37:00 2010 +0100
     1.3 @@ -54,6 +54,33 @@
     1.4  
     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 non-negative.  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 +
    1.34  subsection {* Distinctness *}
    1.35  
    1.36  text {*
    1.37 @@ -342,7 +369,7 @@
    1.38  
    1.39  hide_type (open) pattern
    1.40  hide_const Pattern term_eq
    1.41 -hide_const (open) trigger pat nopat distinct fun_app z3div z3mod
    1.42 +hide_const (open) trigger pat nopat weight distinct fun_app z3div z3mod
    1.43  
    1.44  
    1.45  
     2.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Mon Nov 22 15:45:43 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Mon Nov 22 23:37:00 2010 +0100
     2.3 @@ -55,6 +55,7 @@
     2.4    (@{const_name SMT.pat}, K true),
     2.5    (@{const_name SMT.nopat}, K true),
     2.6    (@{const_name SMT.trigger}, K true),
     2.7 +  (@{const_name SMT.weight}, K true),
     2.8    (@{const_name SMT.fun_app}, K true),
     2.9    (@{const_name SMT.z3div}, K true),
    2.10    (@{const_name SMT.z3mod}, K true),
     3.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 15:45:43 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 23:37:00 2010 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4      SVar of int |
     3.5      SApp of string * sterm list |
     3.6      SLet of string * sterm * sterm |
     3.7 -    SQua of squant * string list * sterm spattern list * sterm
     3.8 +    SQua of squant * string list * sterm spattern list * int option * sterm
     3.9  
    3.10    (* configuration options *)
    3.11    type prefixes = {sort_prefix: string, func_prefix: string}
    3.12 @@ -65,7 +65,7 @@
    3.13    SVar of int |
    3.14    SApp of string * sterm list |
    3.15    SLet of string * sterm * sterm |
    3.16 -  SQua of squant * string list * sterm spattern list * sterm
    3.17 +  SQua of squant * string list * sterm spattern list * int option * sterm
    3.18  
    3.19  
    3.20  
    3.21 @@ -119,6 +119,10 @@
    3.22        if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
    3.23    | group_quant _ Ts t = (Ts, t)
    3.24  
    3.25 +fun dest_weight (@{const SMT.weight} $ w $ t) =
    3.26 +      (SOME (snd (HOLogic.dest_number w)), t)
    3.27 +  | dest_weight t = (NONE, t)
    3.28 +
    3.29  fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
    3.30    | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
    3.31    | dest_pat t = raise TERM ("dest_pat", [t])
    3.32 @@ -137,8 +141,9 @@
    3.33  fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
    3.34    let
    3.35      val (Ts, u) = group_quant qn [T] t
    3.36 -    val (ps, b) = dest_trigger u
    3.37 -  in (q, rev Ts, ps, b) end)
    3.38 +    val (ps, p) = dest_trigger u
    3.39 +    val (w, b) = dest_weight p
    3.40 +  in (q, rev Ts, ps, w, b) end)
    3.41  
    3.42  fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
    3.43    | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
    3.44 @@ -214,6 +219,9 @@
    3.45        | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
    3.46        | _ => t)
    3.47  
    3.48 +    and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
    3.49 +      | in_weight t = in_form t 
    3.50 +
    3.51      and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
    3.52        | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
    3.53        | in_pat t = raise TERM ("in_pat", [t])
    3.54 @@ -221,8 +229,8 @@
    3.55      and in_pats ps =
    3.56        in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
    3.57  
    3.58 -    and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
    3.59 -      | in_trig t = in_form t
    3.60 +    and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_weight t
    3.61 +      | in_trig t = in_weight t
    3.62  
    3.63      and in_form t =
    3.64        (case Term.strip_comb t of
    3.65 @@ -366,9 +374,9 @@
    3.66        (case Term.strip_comb t of
    3.67          (Const (qn, _), [Abs (_, T, t1)]) =>
    3.68            (case dest_quant qn T t1 of
    3.69 -            SOME (q, Ts, ps, b) =>
    3.70 +            SOME (q, Ts, ps, w, b) =>
    3.71                fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
    3.72 -              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
    3.73 +              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b'))
    3.74            | NONE => raise TERM ("intermediate", [t]))
    3.75        | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
    3.76            transT T ##>> trans t1 ##>> trans t2 #>>
     4.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Nov 22 15:45:43 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Nov 22 23:37:00 2010 +0100
     4.3 @@ -238,7 +238,7 @@
     4.4  fun sterm l (T.SVar i) = sep (var (l - i - 1))
     4.5    | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
     4.6    | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
     4.7 -  | sterm l (T.SQua (q, ss, ps, t)) =
     4.8 +  | sterm l (T.SQua (q, ss, ps, w, t)) =
     4.9        let
    4.10          val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
    4.11          val vs = map_index (apfst (Integer.add l)) ss
    4.12 @@ -247,7 +247,12 @@
    4.13          fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
    4.14          fun pats (T.SPat ts) = pat ":pat" ts
    4.15            | pats (T.SNoPat ts) = pat ":nopat" ts
    4.16 -      in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end
    4.17 +        fun weight NONE = I
    4.18 +          | weight (SOME i) =
    4.19 +              sep (add ":weight { " #> add (string_of_int i) #> add " }")
    4.20 +      in
    4.21 +        par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w)
    4.22 +      end
    4.23  
    4.24  fun ssort sorts = sort fast_string_ord sorts
    4.25  fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
     5.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 22 15:45:43 2010 +0100
     5.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 22 23:37:00 2010 +0100
     5.3 @@ -142,7 +142,11 @@
     5.4    val remove_trigger = @{lemma "trigger t p == p"
     5.5      by (rule eq_reflection, rule trigger_def)}
     5.6  
     5.7 -  val prep_rules = [@{thm Let_def}, remove_trigger, L.rewrite_true]
     5.8 +  val remove_weight = @{lemma "weight w p == p"
     5.9 +    by (rule eq_reflection, rule weight_def)}
    5.10 +
    5.11 +  val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
    5.12 +    L.rewrite_true]
    5.13  
    5.14    fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
    5.15      (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)