# HG changeset patch
# User boehmes
# Date 1337781818 -7200
# Node ID 8ba6438557bc64d00d9bf12039f3f1ed09d469ba
# Parent  b74655182ed6c226400c957ac839f127fe70438d
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0

diff -r b74655182ed6 -r 8ba6438557bc src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Wed May 23 15:40:10 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML	Wed May 23 16:03:38 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] =
diff -r b74655182ed6 -r 8ba6438557bc src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Wed May 23 15:40:10 2012 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed May 23 16:03:38 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)