re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
authorboehmes
Mon Dec 20 09:06:37 2010 +0100 (2010-12-20)
changeset 413020485186839a7
parent 41301 0a00fd2f5351
child 41303 939f647f0c9e
re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers)
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smt_utils.ML
src/HOL/Tools/SMT/z3_interface.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Mon Dec 20 08:45:27 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Mon Dec 20 09:06:37 2010 +0100
     1.3 @@ -39,12 +39,6 @@
     1.4  
     1.5    fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
     1.6      | times _ _ _  = NONE
     1.7 -
     1.8 -  fun mk_divide ts = Term.list_comb (@{const divide (real)}, ts)
     1.9 -
    1.10 -  fun divide _ T (ts as [_, t]) =
    1.11 -        if U.is_number t then SOME ("/", 2, ts, mk_divide) else NONE
    1.12 -    | divide _ _ _ = NONE
    1.13  in
    1.14  
    1.15  val setup_builtins =
    1.16 @@ -57,8 +51,8 @@
    1.17      (@{const minus (real)}, "-") ] #>
    1.18    B.add_builtin_fun SMTLIB_Interface.smtlibC
    1.19      (Term.dest_Const @{const times (real)}, times) #>
    1.20 -  B.add_builtin_fun Z3_Interface.smtlib_z3C
    1.21 -    (Term.dest_Const @{const divide (real)}, divide)
    1.22 +  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const times (real)}, "*") #>
    1.23 +  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
    1.24  
    1.25  end
    1.26  
     2.1 --- a/src/HOL/Tools/SMT/smt_utils.ML	Mon Dec 20 08:45:27 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_utils.ML	Mon Dec 20 09:06:37 2010 +0100
     2.3 @@ -141,8 +141,6 @@
     2.4        | is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) =
     2.5            is_num (t :: env) u
     2.6        | is_num env (Const (@{const_name uminus}, _) $ t) = is_num env t
     2.7 -      | is_num env (Const (@{const_name divide}, _) $ t $ u) =
     2.8 -          is_num env t andalso is_num env u
     2.9        | is_num env (Bound i) = i < length env andalso is_num env (nth env i)
    2.10        | is_num _ t = can HOLogic.dest_number t
    2.11    in is_num [] end
     3.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Mon Dec 20 08:45:27 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Mon Dec 20 09:06:37 2010 +0100
     3.3 @@ -44,43 +44,42 @@
     3.4          has_datatypes=true}
     3.5      end
     3.6  
     3.7 -  fun is_div_mod (@{const div (int)} $ _ $ t) = U.is_number t
     3.8 -    | is_div_mod (@{const mod (int)} $ _ $ t) = U.is_number t
     3.9 +  fun is_div_mod @{const div (int)} = true
    3.10 +    | is_div_mod @{const mod (int)} = true
    3.11      | is_div_mod _ = false
    3.12  
    3.13 -  val div_by_z3div = mk_meta_eq @{lemma
    3.14 -    "k div l = (
    3.15 +  val div_by_z3div = @{lemma
    3.16 +    "ALL k l. k div l = (
    3.17        if k = 0 | l = 0 then 0
    3.18        else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l
    3.19        else z3div (-k) (-l))"
    3.20      by (simp add: SMT.z3div_def)}
    3.21  
    3.22 -  val mod_by_z3mod = mk_meta_eq @{lemma
    3.23 -    "k mod l = (
    3.24 +  val mod_by_z3mod = @{lemma
    3.25 +    "ALL k l. k mod l = (
    3.26        if l = 0 then k
    3.27        else if k = 0 then 0
    3.28        else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l
    3.29        else - z3mod (-k) (-l))"
    3.30      by (simp add: z3mod_def)}
    3.31  
    3.32 -  fun div_mod_conv _ =
    3.33 -    U.if_true_conv is_div_mod (Conv.rewrs_conv [div_by_z3div, mod_by_z3mod])
    3.34 +  val have_int_div_mod =
    3.35 +    exists (Term.exists_subterm is_div_mod o Thm.prop_of)
    3.36  
    3.37 -  fun rewrite_div_mod ctxt thm =
    3.38 -    if Term.exists_subterm is_div_mod (Thm.prop_of thm) then
    3.39 -      Conv.fconv_rule (Conv.top_conv div_mod_conv ctxt) thm
    3.40 -    else thm
    3.41 -
    3.42 -  fun norm_div_mod ctxt = pairself (map (rewrite_div_mod ctxt))
    3.43 +  fun add_div_mod _ (thms, extra_thms) =
    3.44 +    if have_int_div_mod thms orelse have_int_div_mod extra_thms then
    3.45 +      (thms, div_by_z3div :: mod_by_z3mod :: extra_thms)
    3.46 +    else (thms, extra_thms)
    3.47  
    3.48    val setup_builtins =
    3.49 +    B.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #>
    3.50      B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
    3.51      B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
    3.52  in
    3.53  
    3.54  val setup = Context.theory_map (
    3.55    setup_builtins #>
    3.56 -  SMT_Normalize.add_extra_norm (smtlib_z3C, norm_div_mod) #>
    3.57 +  SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #>
    3.58    SMT_Translate.add_config (smtlib_z3C, translate_config))
    3.59  
    3.60  end