# HG changeset patch
# User boehmes
# Date 1292427165 -3600
# Node ID 7c6178d45cc803a7674c348ff045b5dcc39fba27
# Parent  a17c2d669c4059f16fdc5a16ac63c6e33690b953
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)

diff -r a17c2d669c40 -r 7c6178d45cc8 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 16:29:56 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 16:32:45 2010 +0100
@@ -141,7 +141,7 @@
       "must have the same kind: " ^ Syntax.string_of_term ctxt t)
 
   fun check_trigger_conv ctxt ct =
-    if proper_quant false proper_trigger (Thm.term_of ct) then Conv.all_conv ct
+    if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct
     else check_trigger_error ctxt (Thm.term_of ct)
 
 
@@ -256,20 +256,20 @@
 
   fun is_weight (@{const SMT.weight} $ w $ t) =
         (case try HOLogic.dest_number w of
-          SOME (_, i) => i > 0 andalso has_no_weight t
+          SOME (_, i) => i >= 0 andalso has_no_weight t
         | _ => false)
     | is_weight t = has_no_weight t
 
   fun proper_trigger (@{const SMT.trigger} $ _ $ t) = is_weight t
-    | proper_trigger t = has_no_weight t
+    | proper_trigger t = is_weight t 
 
   fun check_weight_error ctxt t =
-    error ("SMT weight must be a positive number and must only occur " ^
+    error ("SMT weight must be a non-negative number and must only occur " ^
       "under the top-most quantifier and an optional trigger: " ^
       Syntax.string_of_term ctxt t)
 
   fun check_weight_conv ctxt ct =
-    if U.under_quant proper_trigger (Thm.term_of ct) then Conv.all_conv ct
+    if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct
     else check_weight_error ctxt (Thm.term_of ct)
 
 
diff -r a17c2d669c40 -r 7c6178d45cc8 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 16:29:56 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 16:32:45 2010 +0100
@@ -147,6 +147,8 @@
     fun mark t =
       (case Term.strip_comb t of
         (u as Const (@{const_name If}, _), ts) => marks u ts
+      | (u as @{const SMT.weight}, [t1, t2]) =>
+          mark t2 #>> (fn t2' => u $ t1 $ t2')
       | (u as Const c, ts) =>
           (case B.builtin_num ctxt t of
             SOME (n, T) =>
@@ -494,14 +496,7 @@
   | group_quant _ Ts t = (Ts, t)
 
 fun dest_weight (@{const SMT.weight} $ w $ t) =
-      ((SOME (snd (HOLogic.dest_number w)), t)
-       handle TERM _ =>
-                (case w of
-                  Var ((s, _), _) => (* FIXME: temporary workaround *)
-                    (case Int.fromString s of
-                      SOME n => (SOME n, t)
-                    | NONE => raise TERM ("bad weight", [w]))
-                 | _ => raise TERM ("bad weight", [w])))
+      (SOME (snd (HOLogic.dest_number w)), t)
   | dest_weight t = (NONE, t)
 
 fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)