only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
authorboehmes
Sun Dec 19 17:55:56 2010 +0100 (2010-12-19)
changeset 41280a7de9d36f4f2
parent 41277 1369c27c6966
child 41281 679118e35378
only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
hide internal constants z3div and z3mod;
rewrite div/mod to z3div/z3mod instead of adding extra rules characterizing div/mod in terms of z3div/z3mod
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_builtin.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smt_utils.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
     1.1 --- a/src/HOL/SMT.thy	Sun Dec 19 00:13:25 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Sun Dec 19 17:55:56 2010 +0100
     1.3 @@ -130,21 +130,6 @@
     1.4  definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
     1.5    "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
     1.6  
     1.7 -lemma div_by_z3div:
     1.8 -  "\<forall>k l. k div l = (
     1.9 -    if k = 0 \<or> l = 0 then 0
    1.10 -    else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l
    1.11 -    else z3div (-k) (-l))"
    1.12 -  by (auto simp add: z3div_def trigger_def)
    1.13 -
    1.14 -lemma mod_by_z3mod:
    1.15 -  "\<forall>k l. k mod l = (
    1.16 -    if l = 0 then k
    1.17 -    else if k = 0 then 0
    1.18 -    else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l
    1.19 -    else - z3mod (-k) (-l))"
    1.20 -  by (auto simp add: z3mod_def trigger_def)
    1.21 -
    1.22  
    1.23  
    1.24  subsection {* Setup *}
    1.25 @@ -391,8 +376,8 @@
    1.26  
    1.27  hide_type term_bool
    1.28  hide_type (open) pattern
    1.29 -hide_const Pattern fun_app
    1.30 -hide_const (open) trigger pat nopat weight z3div z3mod
    1.31 +hide_const Pattern fun_app z3div z3mod
    1.32 +hide_const (open) trigger pat nopat weight
    1.33  
    1.34  
    1.35  
     2.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Sun Dec 19 00:13:25 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Sun Dec 19 17:55:56 2010 +0100
     2.3 @@ -188,17 +188,8 @@
     2.4    | SOME (_, Ext f) => f ctxt T ts
     2.5    | NONE => false)
     2.6  
     2.7 -(* FIXME: move this information to the interfaces *)
     2.8 -val only_partially_supported = [
     2.9 -  @{const_name times},
    2.10 -  @{const_name div_class.div},
    2.11 -  @{const_name div_class.mod},
    2.12 -  @{const_name inverse_class.divide} ]
    2.13 -
    2.14 -fun is_builtin_ext ctxt (c as (n, _)) ts =
    2.15 -  if member (op =) only_partially_supported n then false
    2.16 -  else
    2.17 -    is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) orelse 
    2.18 -    is_builtin_fun_ext ctxt c ts
    2.19 +fun is_builtin_ext ctxt c ts =
    2.20 +  is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) orelse 
    2.21 +  is_builtin_fun_ext ctxt c ts
    2.22  
    2.23  end
     3.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Sun Dec 19 00:13:25 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sun Dec 19 17:55:56 2010 +0100
     3.3 @@ -431,20 +431,27 @@
     3.4      "ALL i. i < 0 --> int (nat i) = 0"
     3.5      by simp_all}
     3.6  
     3.7 -  val nat_ops = [
     3.8 +  val simple_nat_ops = [
     3.9      @{const less (nat)}, @{const less_eq (nat)},
    3.10 -    @{const Suc}, @{const plus (nat)}, @{const minus (nat)},
    3.11 -    @{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
    3.12 +    @{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
    3.13 +
    3.14 +  val mult_nat_ops =
    3.15 +    [@{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
    3.16 +
    3.17 +  val nat_ops = simple_nat_ops @ mult_nat_ops
    3.18  
    3.19    val nat_consts = nat_ops @ [@{const number_of (nat)},
    3.20      @{const zero_class.zero (nat)}, @{const one_class.one (nat)}]
    3.21  
    3.22    val nat_int_coercions = [@{const of_nat (int)}, @{const nat}]
    3.23  
    3.24 -  val nat_ops' = nat_int_coercions @ nat_ops
    3.25 +  val builtin_nat_ops = nat_int_coercions @ simple_nat_ops
    3.26  
    3.27    val is_nat_const = member (op aconv) nat_consts
    3.28  
    3.29 +  fun is_nat_const' @{const of_nat (int)} = true
    3.30 +    | is_nat_const' t = is_nat_const t
    3.31 +
    3.32    val expands = map mk_meta_eq @{lemma
    3.33      "0 = nat 0"
    3.34      "1 = nat 1"
    3.35 @@ -494,16 +501,17 @@
    3.36          Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
    3.37      | @{const of_nat (int)} $ _ =>
    3.38          (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
    3.39 -        Conv.top_sweep_conv nat_conv ctxt        
    3.40 +        Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt        
    3.41      | _ => Conv.no_conv) ct
    3.42  
    3.43    and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
    3.44  
    3.45    and expand_conv ctxt =
    3.46 -    U.if_conv (not o is_nat_const o Term.head_of) Conv.no_conv
    3.47 +    U.if_conv (is_nat_const o Term.head_of)
    3.48        (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
    3.49 +      (int_conv ctxt)
    3.50  
    3.51 -  and nat_conv ctxt = U.if_exists_conv is_nat_const
    3.52 +  and nat_conv ctxt = U.if_exists_conv is_nat_const'
    3.53      (Conv.top_sweep_conv expand_conv ctxt)
    3.54  
    3.55    val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
    3.56 @@ -517,7 +525,7 @@
    3.57  
    3.58  val setup_nat_as_int =
    3.59    B.add_builtin_typ_ext (@{typ nat}, K true) #>
    3.60 -  fold (B.add_builtin_fun_ext' o Term.dest_Const) nat_ops'
    3.61 +  fold (B.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
    3.62  
    3.63  end
    3.64  
     4.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Sun Dec 19 00:13:25 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Sun Dec 19 17:55:56 2010 +0100
     4.3 @@ -12,6 +12,7 @@
     4.4  structure SMT_Real: SMT_REAL =
     4.5  struct
     4.6  
     4.7 +structure U = SMT_Utils
     4.8  structure B = SMT_Builtin
     4.9  
    4.10  
    4.11 @@ -29,18 +30,31 @@
    4.12    val smtlibC = SMTLIB_Interface.smtlibC
    4.13  
    4.14    fun real_num _ i = SOME (string_of_int i ^ ".0")
    4.15 +
    4.16 +  fun is_linear [t] = U.is_number t
    4.17 +    | is_linear [t, u] = U.is_number t orelse U.is_number u
    4.18 +    | is_linear _ = false
    4.19 +
    4.20 +  fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE
    4.21 +    | times _ _ _  = NONE
    4.22 +
    4.23 +  fun divide _ T (ts as [_, t]) =
    4.24 +        if U.is_number t then SOME ((("/", 2), T), ts, T) else NONE
    4.25 +    | divide _ _ _ = NONE
    4.26  in
    4.27  
    4.28  val setup_builtins =
    4.29    B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
    4.30    fold (B.add_builtin_fun' smtlibC) [
    4.31 +    (@{const less (real)}, "<"),
    4.32 +    (@{const less_eq (real)}, "<="),
    4.33      (@{const uminus (real)}, "~"),
    4.34      (@{const plus (real)}, "+"),
    4.35 -    (@{const minus (real)}, "-"),
    4.36 -    (@{const times (real)}, "*"),
    4.37 -    (@{const less (real)}, "<"),
    4.38 -    (@{const less_eq (real)}, "<=") ] #>
    4.39 -  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
    4.40 +    (@{const minus (real)}, "-") ] #>
    4.41 +  B.add_builtin_fun SMTLIB_Interface.smtlibC
    4.42 +    (Term.dest_Const @{const times (real)}, times) #>
    4.43 +  B.add_builtin_fun Z3_Interface.smtlib_z3C
    4.44 +    (Term.dest_Const @{const divide (real)}, divide)
    4.45  
    4.46  end
    4.47  
     5.1 --- a/src/HOL/Tools/SMT/smt_utils.ML	Sun Dec 19 00:13:25 2010 +0100
     5.2 +++ b/src/HOL/Tools/SMT/smt_utils.ML	Sun Dec 19 17:55:56 2010 +0100
     5.3 @@ -28,6 +28,7 @@
     5.4    val dest_conj: term -> term * term
     5.5    val dest_disj: term -> term * term
     5.6    val under_quant: (term -> 'a) -> term -> 'a
     5.7 +  val is_number: term -> bool
     5.8  
     5.9    (*patterns and instantiations*)
    5.10    val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
    5.11 @@ -132,6 +133,19 @@
    5.12    | Const (@{const_name Ex}, _) $ Abs (_, _, u) => under_quant f u
    5.13    | _ => f t)
    5.14  
    5.15 +val is_number =
    5.16 +  let
    5.17 +    fun is_num env (Const (@{const_name If}, _) $ _ $ t $ u) =
    5.18 +          is_num env t andalso is_num env u
    5.19 +      | is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) =
    5.20 +          is_num (t :: env) u
    5.21 +      | is_num env (Const (@{const_name uminus}, _) $ t) = is_num env t
    5.22 +      | is_num env (Const (@{const_name divide}, _) $ t $ u) =
    5.23 +          is_num env t andalso is_num env u
    5.24 +      | is_num env (Bound i) = i < length env andalso is_num env (nth env i)
    5.25 +      | is_num _ t = can HOLogic.dest_number t
    5.26 +  in is_num [] end
    5.27 +
    5.28  
    5.29  (* patterns and instantiations *)
    5.30  
     6.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sun Dec 19 00:13:25 2010 +0100
     6.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Sun Dec 19 17:55:56 2010 +0100
     6.3 @@ -16,6 +16,7 @@
     6.4  structure SMTLIB_Interface: SMTLIB_INTERFACE =
     6.5  struct
     6.6  
     6.7 +structure U = SMT_Utils
     6.8  structure B = SMT_Builtin
     6.9  structure N = SMT_Normalize
    6.10  structure T = SMT_Translate
    6.11 @@ -28,6 +29,12 @@
    6.12  local
    6.13    fun int_num _ i = SOME (string_of_int i)
    6.14  
    6.15 +  fun is_linear [t] = U.is_number t
    6.16 +    | is_linear [t, u] = U.is_number t orelse U.is_number u
    6.17 +    | is_linear _ = false
    6.18 +
    6.19 +  fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE
    6.20 +
    6.21    fun distinct _ (Type (_, [Type (_, [T]), _])) [t] =
    6.22          (case try HOLogic.dest_list t of
    6.23            SOME (ts as _ :: _) =>
    6.24 @@ -56,8 +63,8 @@
    6.25      (@{const less_eq (int)}, "<="),
    6.26      (@{const uminus (int)}, "~"),
    6.27      (@{const plus (int)}, "+"),
    6.28 -    (@{const minus (int)}, "-"),
    6.29 -    (@{const times (int)}, "*") ] #>
    6.30 +    (@{const minus (int)}, "-") ] #>
    6.31 +  B.add_builtin_fun smtlibC (Term.dest_Const @{const times (int)}, times) #>
    6.32    B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct)
    6.33  
    6.34  end
     7.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Sun Dec 19 00:13:25 2010 +0100
     7.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Sun Dec 19 17:55:56 2010 +0100
     7.3 @@ -44,17 +44,34 @@
     7.4          has_datatypes=true}
     7.5      end
     7.6  
     7.7 -  fun is_int_div_mod @{const div (int)} = true
     7.8 -    | is_int_div_mod @{const mod (int)} = true
     7.9 -    | is_int_div_mod _ = false
    7.10 +  fun is_div_mod (@{const div (int)} $ _ $ t) = U.is_number t
    7.11 +    | is_div_mod (@{const mod (int)} $ _ $ t) = U.is_number t
    7.12 +    | is_div_mod _ = false
    7.13 +
    7.14 +  val div_by_z3div = mk_meta_eq @{lemma
    7.15 +    "k div l = (
    7.16 +      if k = 0 | l = 0 then 0
    7.17 +      else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l
    7.18 +      else z3div (-k) (-l))"
    7.19 +    by (simp add: SMT.z3div_def)}
    7.20  
    7.21 -  val have_int_div_mod =
    7.22 -    exists (Term.exists_subterm is_int_div_mod o Thm.prop_of)
    7.23 +  val mod_by_z3mod = mk_meta_eq @{lemma
    7.24 +    "k mod l = (
    7.25 +      if l = 0 then k
    7.26 +      else if k = 0 then 0
    7.27 +      else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l
    7.28 +      else - z3mod (-k) (-l))"
    7.29 +    by (simp add: z3mod_def)}
    7.30  
    7.31 -  fun add_div_mod _ (thms, extra_thms) =
    7.32 -    if have_int_div_mod thms orelse have_int_div_mod extra_thms then
    7.33 -      (thms, @{thm div_by_z3div} :: @{thm mod_by_z3mod} :: extra_thms)
    7.34 -    else (thms, extra_thms)
    7.35 +  fun div_mod_conv _ =
    7.36 +    U.if_true_conv is_div_mod (Conv.rewrs_conv [div_by_z3div, mod_by_z3mod])
    7.37 +
    7.38 +  fun rewrite_div_mod ctxt thm =
    7.39 +    if Term.exists_subterm is_div_mod (Thm.prop_of thm) then
    7.40 +      Conv.fconv_rule (Conv.top_conv div_mod_conv ctxt) thm
    7.41 +    else thm
    7.42 +
    7.43 +  fun norm_div_mod ctxt = pairself (map (rewrite_div_mod ctxt))
    7.44  
    7.45    val setup_builtins =
    7.46      B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
    7.47 @@ -63,7 +80,7 @@
    7.48  
    7.49  val setup = Context.theory_map (
    7.50    setup_builtins #>
    7.51 -  SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #>
    7.52 +  SMT_Normalize.add_extra_norm (smtlib_z3C, norm_div_mod) #>
    7.53    SMT_Translate.add_config (smtlib_z3C, translate_config))
    7.54  
    7.55  end