# HG changeset patch # User boehmes # Date 1292832397 -3600 # Node ID 0485186839a7b71f61313bb1b8fb4b61b820e384 # Parent 0a00fd2f535192c9ad5e5f05f9261896a52e782b re-introduced support for nonlinear multiplication in Z3 (overriding the built-in linear multiplication of the SMT-LIB class of solvers) diff -r 0a00fd2f5351 -r 0485186839a7 src/HOL/Tools/SMT/smt_real.ML --- a/src/HOL/Tools/SMT/smt_real.ML Mon Dec 20 08:45:27 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_real.ML Mon Dec 20 09:06:37 2010 +0100 @@ -39,12 +39,6 @@ fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE | times _ _ _ = NONE - - fun mk_divide ts = Term.list_comb (@{const divide (real)}, ts) - - fun divide _ T (ts as [_, t]) = - if U.is_number t then SOME ("/", 2, ts, mk_divide) else NONE - | divide _ _ _ = NONE in val setup_builtins = @@ -57,8 +51,8 @@ (@{const minus (real)}, "-") ] #> B.add_builtin_fun SMTLIB_Interface.smtlibC (Term.dest_Const @{const times (real)}, times) #> - B.add_builtin_fun Z3_Interface.smtlib_z3C - (Term.dest_Const @{const divide (real)}, divide) + B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const times (real)}, "*") #> + B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/") end diff -r 0a00fd2f5351 -r 0485186839a7 src/HOL/Tools/SMT/smt_utils.ML --- a/src/HOL/Tools/SMT/smt_utils.ML Mon Dec 20 08:45:27 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_utils.ML Mon Dec 20 09:06:37 2010 +0100 @@ -141,8 +141,6 @@ | is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) = is_num (t :: env) u | is_num env (Const (@{const_name uminus}, _) $ t) = is_num env t - | is_num env (Const (@{const_name divide}, _) $ t $ u) = - is_num env t andalso is_num env u | is_num env (Bound i) = i < length env andalso is_num env (nth env i) | is_num _ t = can HOLogic.dest_number t in is_num [] end diff -r 0a00fd2f5351 -r 0485186839a7 src/HOL/Tools/SMT/z3_interface.ML --- a/src/HOL/Tools/SMT/z3_interface.ML Mon Dec 20 08:45:27 2010 +0100 +++ b/src/HOL/Tools/SMT/z3_interface.ML Mon Dec 20 09:06:37 2010 +0100 @@ -44,43 +44,42 @@ has_datatypes=true} end - fun is_div_mod (@{const div (int)} $ _ $ t) = U.is_number t - | is_div_mod (@{const mod (int)} $ _ $ t) = U.is_number t + fun is_div_mod @{const div (int)} = true + | is_div_mod @{const mod (int)} = true | is_div_mod _ = false - val div_by_z3div = mk_meta_eq @{lemma - "k div l = ( + val div_by_z3div = @{lemma + "ALL k l. k div l = ( if k = 0 | l = 0 then 0 else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l else z3div (-k) (-l))" by (simp add: SMT.z3div_def)} - val mod_by_z3mod = mk_meta_eq @{lemma - "k mod l = ( + val mod_by_z3mod = @{lemma + "ALL k l. k mod l = ( if l = 0 then k else if k = 0 then 0 else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l else - z3mod (-k) (-l))" by (simp add: z3mod_def)} - fun div_mod_conv _ = - U.if_true_conv is_div_mod (Conv.rewrs_conv [div_by_z3div, mod_by_z3mod]) + val have_int_div_mod = + exists (Term.exists_subterm is_div_mod o Thm.prop_of) - fun rewrite_div_mod ctxt thm = - if Term.exists_subterm is_div_mod (Thm.prop_of thm) then - Conv.fconv_rule (Conv.top_conv div_mod_conv ctxt) thm - else thm - - fun norm_div_mod ctxt = pairself (map (rewrite_div_mod ctxt)) + fun add_div_mod _ (thms, extra_thms) = + if have_int_div_mod thms orelse have_int_div_mod extra_thms then + (thms, div_by_z3div :: mod_by_z3mod :: extra_thms) + else (thms, extra_thms) val setup_builtins = + B.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #> B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #> B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod") in val setup = Context.theory_map ( setup_builtins #> - SMT_Normalize.add_extra_norm (smtlib_z3C, norm_div_mod) #> + SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #> SMT_Translate.add_config (smtlib_z3C, translate_config)) end