--- a/src/HOL/Tools/SMT/smt_real.ML Wed May 23 16:53:12 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML Wed May 23 17:06:45 2012 +0200
@@ -67,8 +67,12 @@
if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
else NONE
+ fun mk_nary _ cu [] = cu
+ | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
+
val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)})
- val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
+ val add = Thm.cterm_of @{theory} @{const plus (real)}
+ val real0 = Numeral.mk_cnumber @{ctyp real} 0
val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
@@ -76,8 +80,8 @@
val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
- | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) [ct, cu] =
- SOME (mk_add ct cu)
+ | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts =
+ SOME (mk_nary add real0 cts)
| z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] =
SOME (mk_sub ct cu)
| z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] =
--- a/src/HOL/Tools/SMT/z3_interface.ML Wed May 23 16:53:12 2012 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed May 23 17:06:45 2012 +0200
@@ -184,7 +184,8 @@
end
val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
-val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
+val add = Thm.cterm_of @{theory} @{const plus (int)}
+val int0 = Numeral.mk_cnumber @{ctyp int} 0
val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)})
val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)})
val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div})
@@ -211,7 +212,7 @@
| (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
| _ =>
(case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
- (Sym ("+", _), SOME @{typ int}, [ct, cu]) => SOME (mk_add ct cu)
+ (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
| (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
| (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)
| (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu)