# HG changeset patch
# User boehmes
# Date 1290465420 -3600
# Node ID e023788a91a1ae57beed53028e01481cfa4d75e2
# Parent  e080c9e68752e4d9c7fb4e422ac2f6bb1974c9d0
added support for quantifier weight annotations

diff -r e080c9e68752 -r e023788a91a1 src/HOL/SMT.thy
--- 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
 
 
 
diff -r e080c9e68752 -r e023788a91a1 src/HOL/Tools/SMT/smt_builtin.ML
--- 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),
diff -r e080c9e68752 -r e023788a91a1 src/HOL/Tools/SMT/smt_translate.ML
--- 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 #>>
diff -r e080c9e68752 -r e023788a91a1 src/HOL/Tools/SMT/smtlib_interface.ML
--- 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
diff -r e080c9e68752 -r e023788a91a1 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- 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)