--- a/src/HOL/SMT.thy Mon Nov 22 15:45:43 2010 +0100
+++ b/src/HOL/SMT.thy Mon Nov 22 23:37:00 2010 +0100
@@ -54,6 +54,33 @@
+subsection {* Quantifier weights *}
+
+text {*
+Weight annotations to quantifiers influence the priority of quantifier
+instantiations. They should be handled with care for solvers, which support
+them, because incorrect choices of weights might render a problem unsolvable.
+*}
+
+definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
+
+text {*
+Weights must be non-negative. The value @{text 0} is equivalent to providing
+no weight at all.
+
+Weights should only be used at quantifiers and only inside triggers (if the
+quantifier has triggers). Valid usages of weights are as follows:
+
+\begin{itemize}
+\item
+@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
+\item
+@{term "\<forall>x. weight 3 (P x)"}
+\end{itemize}
+*}
+
+
+
subsection {* Distinctness *}
text {*
@@ -342,7 +369,7 @@
hide_type (open) pattern
hide_const Pattern term_eq
-hide_const (open) trigger pat nopat distinct fun_app z3div z3mod
+hide_const (open) trigger pat nopat weight distinct fun_app z3div z3mod
--- a/src/HOL/Tools/SMT/smt_builtin.ML Mon Nov 22 15:45:43 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Mon Nov 22 23:37:00 2010 +0100
@@ -55,6 +55,7 @@
(@{const_name SMT.pat}, K true),
(@{const_name SMT.nopat}, K true),
(@{const_name SMT.trigger}, K true),
+ (@{const_name SMT.weight}, K true),
(@{const_name SMT.fun_app}, K true),
(@{const_name SMT.z3div}, K true),
(@{const_name SMT.z3mod}, K true),
--- a/src/HOL/Tools/SMT/smt_translate.ML Mon Nov 22 15:45:43 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Mon Nov 22 23:37:00 2010 +0100
@@ -13,7 +13,7 @@
SVar of int |
SApp of string * sterm list |
SLet of string * sterm * sterm |
- SQua of squant * string list * sterm spattern list * sterm
+ SQua of squant * string list * sterm spattern list * int option * sterm
(* configuration options *)
type prefixes = {sort_prefix: string, func_prefix: string}
@@ -65,7 +65,7 @@
SVar of int |
SApp of string * sterm list |
SLet of string * sterm * sterm |
- SQua of squant * string list * sterm spattern list * sterm
+ SQua of squant * string list * sterm spattern list * int option * sterm
@@ -119,6 +119,10 @@
if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
| group_quant _ Ts t = (Ts, t)
+fun dest_weight (@{const SMT.weight} $ w $ t) =
+ (SOME (snd (HOLogic.dest_number w)), t)
+ | dest_weight t = (NONE, t)
+
fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
| dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
| dest_pat t = raise TERM ("dest_pat", [t])
@@ -137,8 +141,9 @@
fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
let
val (Ts, u) = group_quant qn [T] t
- val (ps, b) = dest_trigger u
- in (q, rev Ts, ps, b) end)
+ val (ps, p) = dest_trigger u
+ val (w, b) = dest_weight p
+ in (q, rev Ts, ps, w, b) end)
fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
| fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
@@ -214,6 +219,9 @@
| (h as Free _, ts) => Term.list_comb (h, map in_term ts)
| _ => t)
+ and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
+ | in_weight t = in_form t
+
and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
| in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
| in_pat t = raise TERM ("in_pat", [t])
@@ -221,8 +229,8 @@
and in_pats ps =
in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
- and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
- | in_trig t = in_form t
+ and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_weight t
+ | in_trig t = in_weight t
and in_form t =
(case Term.strip_comb t of
@@ -366,9 +374,9 @@
(case Term.strip_comb t of
(Const (qn, _), [Abs (_, T, t1)]) =>
(case dest_quant qn T t1 of
- SOME (q, Ts, ps, b) =>
+ SOME (q, Ts, ps, w, b) =>
fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
- trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
+ trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b'))
| NONE => raise TERM ("intermediate", [t]))
| (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
transT T ##>> trans t1 ##>> trans t2 #>>
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Mon Nov 22 15:45:43 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Mon Nov 22 23:37:00 2010 +0100
@@ -238,7 +238,7 @@
fun sterm l (T.SVar i) = sep (var (l - i - 1))
| sterm l (T.SApp (n, ts)) = app n (sterm l) ts
| sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
- | sterm l (T.SQua (q, ss, ps, t)) =
+ | sterm l (T.SQua (q, ss, ps, w, t)) =
let
val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
val vs = map_index (apfst (Integer.add l)) ss
@@ -247,7 +247,12 @@
fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
fun pats (T.SPat ts) = pat ":pat" ts
| pats (T.SNoPat ts) = pat ":nopat" ts
- in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end
+ fun weight NONE = I
+ | weight (SOME i) =
+ sep (add ":weight { " #> add (string_of_int i) #> add " }")
+ in
+ par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w)
+ end
fun ssort sorts = sort fast_string_ord sorts
fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Nov 22 15:45:43 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Nov 22 23:37:00 2010 +0100
@@ -142,7 +142,11 @@
val remove_trigger = @{lemma "trigger t p == p"
by (rule eq_reflection, rule trigger_def)}
- val prep_rules = [@{thm Let_def}, remove_trigger, L.rewrite_true]
+ val remove_weight = @{lemma "weight w p == p"
+ by (rule eq_reflection, rule weight_def)}
+
+ val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
+ L.rewrite_true]
fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
(Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)